1 (* Author: Thomas Marthedal Rasmussen |
1 (* Title: HOL/Old_Number_Theory/Factorization.thy |
|
2 Author: Thomas Marthedal Rasmussen |
2 Copyright 2000 University of Cambridge |
3 Copyright 2000 University of Cambridge |
3 *) |
4 *) |
4 |
5 |
5 header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *} |
6 header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *} |
6 |
7 |
7 theory Factorization |
8 theory Factorization |
8 imports Main "~~/src/HOL/Old_Number_Theory/Primes" Permutation |
9 imports Primes Permutation |
9 begin |
10 begin |
10 |
11 |
11 |
12 |
12 subsection {* Definitions *} |
13 subsection {* Definitions *} |
13 |
14 |
14 definition |
15 definition primel :: "nat list => bool" |
15 primel :: "nat list => bool" where |
16 where "primel xs = (\<forall>p \<in> set xs. prime p)" |
16 "primel xs = (\<forall>p \<in> set xs. prime p)" |
17 |
17 |
18 primrec nondec :: "nat list => bool" |
18 consts |
19 where |
19 nondec :: "nat list => bool " |
|
20 prod :: "nat list => nat" |
|
21 oinsert :: "nat => nat list => nat list" |
|
22 sort :: "nat list => nat list" |
|
23 |
|
24 primrec |
|
25 "nondec [] = True" |
20 "nondec [] = True" |
26 "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)" |
21 | "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)" |
27 |
22 |
28 primrec |
23 primrec prod :: "nat list => nat" |
|
24 where |
29 "prod [] = Suc 0" |
25 "prod [] = Suc 0" |
30 "prod (x # xs) = x * prod xs" |
26 | "prod (x # xs) = x * prod xs" |
31 |
27 |
32 primrec |
28 primrec oinsert :: "nat => nat list => nat list" |
|
29 where |
33 "oinsert x [] = [x]" |
30 "oinsert x [] = [x]" |
34 "oinsert x (y # ys) = (if x \<le> y then x # y # ys else y # oinsert x ys)" |
31 | "oinsert x (y # ys) = (if x \<le> y then x # y # ys else y # oinsert x ys)" |
35 |
32 |
36 primrec |
33 primrec sort :: "nat list => nat list" |
|
34 where |
37 "sort [] = []" |
35 "sort [] = []" |
38 "sort (x # xs) = oinsert x (sort xs)" |
36 | "sort (x # xs) = oinsert x (sort xs)" |
39 |
37 |
40 |
38 |
41 subsection {* Arithmetic *} |
39 subsection {* Arithmetic *} |
42 |
40 |
43 lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> Suc 0 ==> Suc 0 < m" |
41 lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> Suc 0 ==> Suc 0 < m" |