author | wenzelm |
Tue, 18 Dec 2007 00:17:00 +0100 | |
changeset 25687 | f92c9dfa7681 |
parent 25493 | 50d566776a26 |
child 26316 | 9e9e67e33557 |
permissions | -rw-r--r-- |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
1 |
(* Title: HOL/NumberTheory/Factorization.thy |
9944 | 2 |
ID: $Id$ |
3 |
Author: Thomas Marthedal Rasmussen |
|
4 |
Copyright 2000 University of Cambridge |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
5 |
*) |
9944 | 6 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
7 |
header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
8 |
|
16417 | 9 |
theory Factorization imports Primes Permutation begin |
9944 | 10 |
|
11 |
||
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
12 |
subsection {* Definitions *} |
9944 | 13 |
|
19670 | 14 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19670
diff
changeset
|
15 |
primel :: "nat list => bool" where |
19670 | 16 |
"primel xs = (\<forall>p \<in> set xs. prime p)" |
17 |
||
9944 | 18 |
consts |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
19 |
nondec :: "nat list => bool " |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
20 |
prod :: "nat list => nat" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
21 |
oinsert :: "nat => nat list => nat list" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
22 |
sort :: "nat list => nat list" |
9944 | 23 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
24 |
primrec |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
25 |
"nondec [] = True" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
26 |
"nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)" |
9944 | 27 |
|
28 |
primrec |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
29 |
"prod [] = Suc 0" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
30 |
"prod (x # xs) = x * prod xs" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
31 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
32 |
primrec |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
33 |
"oinsert x [] = [x]" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
34 |
"oinsert x (y # ys) = (if x \<le> y then x # y # ys else y # oinsert x ys)" |
9944 | 35 |
|
36 |
primrec |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
37 |
"sort [] = []" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
38 |
"sort (x # xs) = oinsert x (sort xs)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
39 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
40 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
41 |
subsection {* Arithmetic *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
42 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
43 |
lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> Suc 0 ==> Suc 0 < m" |
19670 | 44 |
apply (cases m) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
45 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
46 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
47 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
48 |
lemma one_less_k: "(m::nat) \<noteq> m * k ==> Suc 0 < m * k ==> Suc 0 < k" |
19670 | 49 |
apply (cases k) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
50 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
51 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
52 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
53 |
lemma mult_left_cancel: "(0::nat) < k ==> k * n = k * m ==> n = m" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
54 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
55 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
56 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
57 |
lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = Suc 0" |
19670 | 58 |
apply (cases n) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
59 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
60 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
61 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
62 |
lemma prod_mn_less_k: |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
63 |
"(0::nat) < n ==> 0 < k ==> Suc 0 < m ==> m * n = k ==> n < k" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
64 |
apply (induct m) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
65 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
66 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
67 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
68 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
69 |
subsection {* Prime list and product *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
70 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
71 |
lemma prod_append: "prod (xs @ ys) = prod xs * prod ys" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
72 |
apply (induct xs) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
73 |
apply (simp_all add: mult_assoc) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
74 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
75 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
76 |
lemma prod_xy_prod: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
77 |
"prod (x # xs) = prod (y # ys) ==> x * prod xs = y * prod ys" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
78 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
79 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
80 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
81 |
lemma primel_append: "primel (xs @ ys) = (primel xs \<and> primel ys)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
82 |
apply (unfold primel_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
83 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
84 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
85 |
|
16663 | 86 |
lemma prime_primel: "prime n ==> primel [n] \<and> prod [n] = n" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
87 |
apply (unfold primel_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
88 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
89 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
90 |
|
16663 | 91 |
lemma prime_nd_one: "prime p ==> \<not> p dvd Suc 0" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
92 |
apply (unfold prime_def dvd_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
93 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
94 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
95 |
|
23814 | 96 |
lemma hd_dvd_prod: "prod (x # xs) = prod ys ==> x dvd (prod ys)" |
97 |
by (metis dvd_mult_left dvd_refl prod.simps(2)) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
98 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
99 |
lemma primel_tl: "primel (x # xs) ==> primel xs" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
100 |
apply (unfold primel_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
101 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
102 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
103 |
|
16663 | 104 |
lemma primel_hd_tl: "(primel (x # xs)) = (prime x \<and> primel xs)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
105 |
apply (unfold primel_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
106 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
107 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
108 |
|
16663 | 109 |
lemma primes_eq: "prime p ==> prime q ==> p dvd q ==> p = q" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
110 |
apply (unfold prime_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
111 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
112 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
113 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
114 |
lemma primel_one_empty: "primel xs ==> prod xs = Suc 0 ==> xs = []" |
19670 | 115 |
apply (cases xs) |
116 |
apply (simp_all add: primel_def prime_def) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
117 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
118 |
|
16663 | 119 |
lemma prime_g_one: "prime p ==> Suc 0 < p" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
120 |
apply (unfold prime_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
121 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
122 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
123 |
|
16663 | 124 |
lemma prime_g_zero: "prime p ==> 0 < p" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
125 |
apply (unfold prime_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
126 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
127 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
128 |
|
19670 | 129 |
lemma primel_nempty_g_one: |
130 |
"primel xs \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> Suc 0 < prod xs" |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
131 |
apply (induct xs) |
19670 | 132 |
apply simp |
133 |
apply (fastsimp simp: primel_def prime_def elim: one_less_mult) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
134 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
135 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
136 |
lemma primel_prod_gz: "primel xs ==> 0 < prod xs" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
137 |
apply (induct xs) |
19670 | 138 |
apply (auto simp: primel_def prime_def) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
139 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
140 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
141 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
142 |
subsection {* Sorting *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
143 |
|
19670 | 144 |
lemma nondec_oinsert: "nondec xs \<Longrightarrow> nondec (oinsert x xs)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
145 |
apply (induct xs) |
19670 | 146 |
apply simp |
147 |
apply (case_tac xs) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
148 |
apply (simp_all cong del: list.weak_case_cong) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
149 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
150 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
151 |
lemma nondec_sort: "nondec (sort xs)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
152 |
apply (induct xs) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
153 |
apply simp_all |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
154 |
apply (erule nondec_oinsert) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
155 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
156 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
157 |
lemma x_less_y_oinsert: "x \<le> y ==> l = y # ys ==> x # l = oinsert x l" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
158 |
apply simp_all |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
159 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
160 |
|
19670 | 161 |
lemma nondec_sort_eq [rule_format]: "nondec xs \<longrightarrow> xs = sort xs" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
162 |
apply (induct xs) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
163 |
apply safe |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
164 |
apply simp_all |
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
11701
diff
changeset
|
165 |
apply (case_tac xs) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
166 |
apply simp_all |
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
11701
diff
changeset
|
167 |
apply (case_tac xs) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
168 |
apply simp |
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
11701
diff
changeset
|
169 |
apply (rule_tac y = aa and ys = list in x_less_y_oinsert) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
170 |
apply simp_all |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
171 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
172 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
173 |
lemma oinsert_x_y: "oinsert x (oinsert y l) = oinsert y (oinsert x l)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
174 |
apply (induct l) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
175 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
176 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
177 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
178 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
179 |
subsection {* Permutation *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
180 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
181 |
lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
182 |
apply (unfold primel_def) |
19670 | 183 |
apply (induct set: perm) |
16663 | 184 |
apply simp |
185 |
apply simp |
|
186 |
apply (simp (no_asm)) |
|
187 |
apply blast |
|
188 |
apply blast |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
189 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
190 |
|
19670 | 191 |
lemma perm_prod: "xs <~~> ys ==> prod xs = prod ys" |
192 |
apply (induct set: perm) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
193 |
apply (simp_all add: mult_ac) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
194 |
done |
9944 | 195 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
196 |
lemma perm_subst_oinsert: "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys" |
19670 | 197 |
apply (induct set: perm) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
198 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
199 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
200 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
201 |
lemma perm_oinsert: "x # xs <~~> oinsert x xs" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
202 |
apply (induct xs) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
203 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
204 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
205 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
206 |
lemma perm_sort: "xs <~~> sort xs" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
207 |
apply (induct xs) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
208 |
apply (auto intro: perm_oinsert elim: perm_subst_oinsert) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
209 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
210 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
211 |
lemma perm_sort_eq: "xs <~~> ys ==> sort xs = sort ys" |
19670 | 212 |
apply (induct set: perm) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
213 |
apply (simp_all add: oinsert_x_y) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
214 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
215 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
216 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
217 |
subsection {* Existence *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
218 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
219 |
lemma ex_nondec_lemma: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
220 |
"primel xs ==> \<exists>ys. primel ys \<and> nondec ys \<and> prod ys = prod xs" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
221 |
apply (blast intro: nondec_sort perm_prod perm_primel perm_sort perm_sym) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
222 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
223 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
224 |
lemma not_prime_ex_mk: |
16663 | 225 |
"Suc 0 < n \<and> \<not> prime n ==> |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
226 |
\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
227 |
apply (unfold prime_def dvd_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
228 |
apply (auto intro: n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
229 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
230 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
231 |
lemma split_primel: |
25687
f92c9dfa7681
split_primel: salvaged original proof after blow with sledghammer
wenzelm
parents:
25493
diff
changeset
|
232 |
"primel xs \<Longrightarrow> primel ys \<Longrightarrow> \<exists>l. primel l \<and> prod l = prod xs * prod ys" |
f92c9dfa7681
split_primel: salvaged original proof after blow with sledghammer
wenzelm
parents:
25493
diff
changeset
|
233 |
apply (rule exI) |
f92c9dfa7681
split_primel: salvaged original proof after blow with sledghammer
wenzelm
parents:
25493
diff
changeset
|
234 |
apply safe |
f92c9dfa7681
split_primel: salvaged original proof after blow with sledghammer
wenzelm
parents:
25493
diff
changeset
|
235 |
apply (rule_tac [2] prod_append) |
f92c9dfa7681
split_primel: salvaged original proof after blow with sledghammer
wenzelm
parents:
25493
diff
changeset
|
236 |
apply (simp add: primel_append) |
f92c9dfa7681
split_primel: salvaged original proof after blow with sledghammer
wenzelm
parents:
25493
diff
changeset
|
237 |
done |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
238 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
239 |
lemma factor_exists [rule_format]: "Suc 0 < n --> (\<exists>l. primel l \<and> prod l = n)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
240 |
apply (induct n rule: nat_less_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
241 |
apply (rule impI) |
16663 | 242 |
apply (case_tac "prime n") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
243 |
apply (rule exI) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
244 |
apply (erule prime_primel) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
245 |
apply (cut_tac n = n in not_prime_ex_mk) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
246 |
apply (auto intro!: split_primel) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
247 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
248 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
249 |
lemma nondec_factor_exists: "Suc 0 < n ==> \<exists>l. primel l \<and> nondec l \<and> prod l = n" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
250 |
apply (erule factor_exists [THEN exE]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
251 |
apply (blast intro!: ex_nondec_lemma) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
252 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
253 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
254 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
255 |
subsection {* Uniqueness *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
256 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
257 |
lemma prime_dvd_mult_list [rule_format]: |
16663 | 258 |
"prime p ==> p dvd (prod xs) --> (\<exists>m. m:set xs \<and> p dvd m)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
259 |
apply (induct xs) |
11364 | 260 |
apply (force simp add: prime_def) |
261 |
apply (force dest: prime_dvd_mult) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
262 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
263 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
264 |
lemma hd_xs_dvd_prod: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
265 |
"primel (x # xs) ==> primel ys ==> prod (x # xs) = prod ys |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
266 |
==> \<exists>m. m \<in> set ys \<and> x dvd m" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
267 |
apply (rule prime_dvd_mult_list) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
268 |
apply (simp add: primel_hd_tl) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
269 |
apply (erule hd_dvd_prod) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
270 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
271 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
272 |
lemma prime_dvd_eq: "primel (x # xs) ==> primel ys ==> m \<in> set ys ==> x dvd m ==> x = m" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
273 |
apply (rule primes_eq) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
274 |
apply (auto simp add: primel_def primel_hd_tl) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
275 |
done |
9944 | 276 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
277 |
lemma hd_xs_eq_prod: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
278 |
"primel (x # xs) ==> |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
279 |
primel ys ==> prod (x # xs) = prod ys ==> x \<in> set ys" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
280 |
apply (frule hd_xs_dvd_prod) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
281 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
282 |
apply (drule prime_dvd_eq) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
283 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
284 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
285 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
286 |
lemma perm_primel_ex: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
287 |
"primel (x # xs) ==> |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
288 |
primel ys ==> prod (x # xs) = prod ys ==> \<exists>l. ys <~~> (x # l)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
289 |
apply (rule exI) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
290 |
apply (rule perm_remove) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
291 |
apply (erule hd_xs_eq_prod) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
292 |
apply simp_all |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
293 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
294 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
295 |
lemma primel_prod_less: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
296 |
"primel (x # xs) ==> |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
297 |
primel ys ==> prod (x # xs) = prod ys ==> prod xs < prod ys" |
25180
16a99bc76717
avoid very slow metis invocation (saves 1min on 1.60 GHz machine);
wenzelm
parents:
25157
diff
changeset
|
298 |
by (metis Nat.less_asym linorder_neqE_nat mult_less_cancel2 nat_0_less_mult_iff |
16a99bc76717
avoid very slow metis invocation (saves 1min on 1.60 GHz machine);
wenzelm
parents:
25157
diff
changeset
|
299 |
nat_less_le nat_mult_1 prime_def primel_hd_tl primel_prod_gz prod.simps(2)) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
300 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
301 |
lemma prod_one_empty: |
16663 | 302 |
"primel xs ==> p * prod xs = p ==> prime p ==> xs = []" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
303 |
apply (auto intro: primel_one_empty simp add: prime_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
304 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
305 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
306 |
lemma uniq_ex_aux: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
307 |
"\<forall>m. m < prod ys --> (\<forall>xs ys. primel xs \<and> primel ys \<and> |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
308 |
prod xs = prod ys \<and> prod xs = m --> xs <~~> ys) ==> |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
309 |
primel list ==> primel x ==> prod list = prod x ==> prod x < prod ys |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
310 |
==> x <~~> list" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
311 |
apply simp |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
312 |
done |
9944 | 313 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
314 |
lemma factor_unique [rule_format]: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
315 |
"\<forall>xs ys. primel xs \<and> primel ys \<and> prod xs = prod ys \<and> prod xs = n |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
316 |
--> xs <~~> ys" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
317 |
apply (induct n rule: nat_less_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
318 |
apply safe |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
319 |
apply (case_tac xs) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
320 |
apply (force intro: primel_one_empty) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
321 |
apply (rule perm_primel_ex [THEN exE]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
322 |
apply simp_all |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
323 |
apply (rule perm.trans [THEN perm_sym]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
324 |
apply assumption |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
325 |
apply (rule perm.Cons) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
326 |
apply (case_tac "x = []") |
25493 | 327 |
apply (metis perm_prod perm_refl prime_primel primel_hd_tl primel_tl prod_one_empty) |
328 |
apply (metis nat_0_less_mult_iff nat_mult_eq_cancel1 perm_primel perm_prod primel_prod_gz primel_prod_less primel_tl prod.simps(2)) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
329 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
330 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
331 |
lemma perm_nondec_unique: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
332 |
"xs <~~> ys ==> nondec xs ==> nondec ys ==> xs = ys" |
23814 | 333 |
by (metis nondec_sort_eq perm_sort_eq) |
334 |
||
25493 | 335 |
theorem unique_prime_factorization [rule_format]: |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
336 |
"\<forall>n. Suc 0 < n --> (\<exists>!l. primel l \<and> nondec l \<and> prod l = n)" |
25493 | 337 |
by (metis factor_unique nondec_factor_exists perm_nondec_unique) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
338 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
339 |
end |