author | wenzelm |
Sat, 20 Aug 2011 23:36:18 +0200 | |
changeset 44339 | eda6aef75939 |
parent 40786 | 0a54cfc9add3 |
child 44766 | d4d33a4d7548 |
permissions | -rw-r--r-- |
38159 | 1 |
(* Title: HOL/Old_Number_Theory/EulerFermat.thy |
2 |
Author: Thomas M. Rasmussen |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
3 |
Copyright 2000 University of Cambridge |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
4 |
*) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
5 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
6 |
header {* Fermat's Little Theorem extended to Euler's Totient function *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
7 |
|
27556 | 8 |
theory EulerFermat |
9 |
imports BijectionRel IntFact |
|
10 |
begin |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
11 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
12 |
text {* |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
13 |
Fermat's Little Theorem extended to Euler's Totient function. More |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
14 |
abstract approach than Boyer-Moore (which seems necessary to achieve |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
15 |
the extended version). |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
16 |
*} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
17 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
18 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
19 |
subsection {* Definitions and lemmas *} |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
20 |
|
38159 | 21 |
inductive_set RsetR :: "int => int set set" for m :: int |
22 |
where |
|
23 |
empty [simp]: "{} \<in> RsetR m" |
|
24 |
| insert: "A \<in> RsetR m ==> zgcd a m = 1 ==> |
|
25 |
\<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m" |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
26 |
|
38159 | 27 |
fun BnorRset :: "int \<Rightarrow> int => int set" where |
35440 | 28 |
"BnorRset a m = |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
29 |
(if 0 < a then |
35440 | 30 |
let na = BnorRset (a - 1) m |
27556 | 31 |
in (if zgcd a m = 1 then insert a na else na) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
32 |
else {})" |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
33 |
|
38159 | 34 |
definition norRRset :: "int => int set" |
35 |
where "norRRset m = BnorRset (m - 1) m" |
|
19670 | 36 |
|
38159 | 37 |
definition noXRRset :: "int => int => int set" |
38 |
where "noXRRset m x = (\<lambda>a. a * x) ` norRRset m" |
|
19670 | 39 |
|
38159 | 40 |
definition phi :: "int => nat" |
41 |
where "phi m = card (norRRset m)" |
|
19670 | 42 |
|
38159 | 43 |
definition is_RRset :: "int set => int => bool" |
44 |
where "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)" |
|
19670 | 45 |
|
38159 | 46 |
definition RRset2norRR :: "int set => int => int => int" |
47 |
where |
|
48 |
"RRset2norRR A m a = |
|
49 |
(if 1 < m \<and> is_RRset A m \<and> a \<in> A then |
|
50 |
SOME b. zcong a b m \<and> b \<in> norRRset m |
|
51 |
else 0)" |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
52 |
|
38159 | 53 |
definition zcongm :: "int => int => int => bool" |
54 |
where "zcongm m = (\<lambda>a b. zcong a b m)" |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
55 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
56 |
lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
57 |
-- {* LCP: not sure why this lemma is needed now *} |
18369 | 58 |
by (auto simp add: abs_if) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
59 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
60 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
61 |
text {* \medskip @{text norRRset} *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
62 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
63 |
declare BnorRset.simps [simp del] |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
64 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
65 |
lemma BnorRset_induct: |
18369 | 66 |
assumes "!!a m. P {} a m" |
35440 | 67 |
and "!!a m :: int. 0 < a ==> P (BnorRset (a - 1) m) (a - 1) m |
68 |
==> P (BnorRset a m) a m" |
|
69 |
shows "P (BnorRset u v) u v" |
|
18369 | 70 |
apply (rule BnorRset.induct) |
35440 | 71 |
apply (case_tac "0 < a") |
72 |
apply (rule_tac assms) |
|
18369 | 73 |
apply simp_all |
35440 | 74 |
apply (simp_all add: BnorRset.simps assms) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
75 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
76 |
|
35440 | 77 |
lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset a m \<longrightarrow> b \<le> a" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
78 |
apply (induct a m rule: BnorRset_induct) |
18369 | 79 |
apply simp |
80 |
apply (subst BnorRset.simps) |
|
13833 | 81 |
apply (unfold Let_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
82 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
83 |
|
35440 | 84 |
lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset a m" |
18369 | 85 |
by (auto dest: Bnor_mem_zle) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
86 |
|
35440 | 87 |
lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset a m --> 0 < b" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
88 |
apply (induct a m rule: BnorRset_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
89 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
90 |
apply (subst BnorRset.simps) |
13833 | 91 |
apply (unfold Let_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
92 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
93 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
94 |
lemma Bnor_mem_if [rule_format]: |
35440 | 95 |
"zgcd b m = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset a m" |
13833 | 96 |
apply (induct a m rule: BnorRset.induct, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
97 |
apply (subst BnorRset.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
98 |
defer |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
99 |
apply (subst BnorRset.simps) |
13833 | 100 |
apply (unfold Let_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
101 |
done |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
102 |
|
35440 | 103 |
lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset a m \<in> RsetR m" |
13833 | 104 |
apply (induct a m rule: BnorRset_induct, simp) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
105 |
apply (subst BnorRset.simps) |
13833 | 106 |
apply (unfold Let_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
107 |
apply (rule RsetR.insert) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
108 |
apply (rule_tac [3] allI) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
109 |
apply (rule_tac [3] impI) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
110 |
apply (rule_tac [3] zcong_not) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
111 |
apply (subgoal_tac [6] "a' \<le> a - 1") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
112 |
apply (rule_tac [7] Bnor_mem_zle) |
13833 | 113 |
apply (rule_tac [5] Bnor_mem_zg, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
114 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
115 |
|
35440 | 116 |
lemma Bnor_fin: "finite (BnorRset a m)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
117 |
apply (induct a m rule: BnorRset_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
118 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
119 |
apply (subst BnorRset.simps) |
13833 | 120 |
apply (unfold Let_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
121 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
122 |
|
13524 | 123 |
lemma norR_mem_unique_aux: "a \<le> b - 1 ==> a < (b::int)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
124 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
125 |
done |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
126 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
127 |
lemma norR_mem_unique: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
128 |
"1 < m ==> |
27556 | 129 |
zgcd a m = 1 ==> \<exists>!b. [a = b] (mod m) \<and> b \<in> norRRset m" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
130 |
apply (unfold norRRset_def) |
13833 | 131 |
apply (cut_tac a = a and m = m in zcong_zless_unique, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
132 |
apply (rule_tac [2] m = m in zcong_zless_imp_eq) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
133 |
apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
134 |
order_less_imp_le norR_mem_unique_aux simp add: zcong_sym) |
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13833
diff
changeset
|
135 |
apply (rule_tac x = b in exI, safe) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
136 |
apply (rule Bnor_mem_if) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
137 |
apply (case_tac [2] "b = 0") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
138 |
apply (auto intro: order_less_le [THEN iffD2]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
139 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
140 |
apply (simp only: zcong_def) |
27556 | 141 |
apply (subgoal_tac "zgcd a m = m") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
142 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
143 |
apply (subst zdvd_iff_zgcd [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
144 |
apply (rule_tac [4] zgcd_zcong_zgcd) |
30042 | 145 |
apply (simp_all add: zcong_sym) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
146 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
147 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
148 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
149 |
text {* \medskip @{term noXRRset} *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
150 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
151 |
lemma RRset_gcd [rule_format]: |
27556 | 152 |
"is_RRset A m ==> a \<in> A --> zgcd a m = 1" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
153 |
apply (unfold is_RRset_def) |
27556 | 154 |
apply (rule RsetR.induct [where P="%A. a \<in> A --> zgcd a m = 1"], auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
155 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
156 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
157 |
lemma RsetR_zmult_mono: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
158 |
"A \<in> RsetR m ==> |
27556 | 159 |
0 < m ==> zgcd x m = 1 ==> (\<lambda>a. a * x) ` A \<in> RsetR m" |
13833 | 160 |
apply (erule RsetR.induct, simp_all) |
161 |
apply (rule RsetR.insert, auto) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
162 |
apply (blast intro: zgcd_zgcd_zmult) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
163 |
apply (simp add: zcong_cancel) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
164 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
165 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
166 |
lemma card_nor_eq_noX: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
167 |
"0 < m ==> |
27556 | 168 |
zgcd x m = 1 ==> card (noXRRset m x) = card (norRRset m)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
169 |
apply (unfold norRRset_def noXRRset_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
170 |
apply (rule card_image) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
171 |
apply (auto simp add: inj_on_def Bnor_fin) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
172 |
apply (simp add: BnorRset.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
173 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
174 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
175 |
lemma noX_is_RRset: |
27556 | 176 |
"0 < m ==> zgcd x m = 1 ==> is_RRset (noXRRset m x) m" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
177 |
apply (unfold is_RRset_def phi_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
178 |
apply (auto simp add: card_nor_eq_noX) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
179 |
apply (unfold noXRRset_def norRRset_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
180 |
apply (rule RsetR_zmult_mono) |
13833 | 181 |
apply (rule Bnor_in_RsetR, simp_all) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
182 |
done |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
183 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
184 |
lemma aux_some: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
185 |
"1 < m ==> is_RRset A m ==> a \<in> A |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
186 |
==> zcong a (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) m \<and> |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
187 |
(SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) \<in> norRRset m" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
188 |
apply (rule norR_mem_unique [THEN ex1_implies_ex, THEN someI_ex]) |
13833 | 189 |
apply (rule_tac [2] RRset_gcd, simp_all) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
190 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
191 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
192 |
lemma RRset2norRR_correct: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
193 |
"1 < m ==> is_RRset A m ==> a \<in> A ==> |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
194 |
[a = RRset2norRR A m a] (mod m) \<and> RRset2norRR A m a \<in> norRRset m" |
13833 | 195 |
apply (unfold RRset2norRR_def, simp) |
196 |
apply (rule aux_some, simp_all) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
197 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
198 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
199 |
lemmas RRset2norRR_correct1 = |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
200 |
RRset2norRR_correct [THEN conjunct1, standard] |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
201 |
lemmas RRset2norRR_correct2 = |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
202 |
RRset2norRR_correct [THEN conjunct2, standard] |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
203 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
204 |
lemma RsetR_fin: "A \<in> RsetR m ==> finite A" |
18369 | 205 |
by (induct set: RsetR) auto |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
206 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
207 |
lemma RRset_zcong_eq [rule_format]: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
208 |
"1 < m ==> |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
209 |
is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
210 |
apply (unfold is_RRset_def) |
26793
e36a92ff543e
Instantiated some rules to avoid problems with HO unification.
berghofe
parents:
23755
diff
changeset
|
211 |
apply (rule RsetR.induct [where P="%A. a \<in> A --> b \<in> A --> a = b"]) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
212 |
apply (auto simp add: zcong_sym) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
213 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
214 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
215 |
lemma aux: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
216 |
"P (SOME a. P a) ==> Q (SOME a. Q a) ==> |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
217 |
(SOME a. P a) = (SOME a. Q a) ==> \<exists>a. P a \<and> Q a" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
218 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
219 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
220 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
221 |
lemma RRset2norRR_inj: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
222 |
"1 < m ==> is_RRset A m ==> inj_on (RRset2norRR A m) A" |
13833 | 223 |
apply (unfold RRset2norRR_def inj_on_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
224 |
apply (subgoal_tac "\<exists>b. ([x = b] (mod m) \<and> b \<in> norRRset m) \<and> |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
225 |
([y = b] (mod m) \<and> b \<in> norRRset m)") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
226 |
apply (rule_tac [2] aux) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
227 |
apply (rule_tac [3] aux_some) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
228 |
apply (rule_tac [2] aux_some) |
13833 | 229 |
apply (rule RRset_zcong_eq, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
230 |
apply (rule_tac b = b in zcong_trans) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
231 |
apply (simp_all add: zcong_sym) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
232 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
233 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
234 |
lemma RRset2norRR_eq_norR: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
235 |
"1 < m ==> is_RRset A m ==> RRset2norRR A m ` A = norRRset m" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
236 |
apply (rule card_seteq) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
237 |
prefer 3 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
238 |
apply (subst card_image) |
15402 | 239 |
apply (rule_tac RRset2norRR_inj, auto) |
240 |
apply (rule_tac [3] RRset2norRR_correct2, auto) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
241 |
apply (unfold is_RRset_def phi_def norRRset_def) |
15402 | 242 |
apply (auto simp add: Bnor_fin) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
243 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
244 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
245 |
|
13524 | 246 |
lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A" |
13833 | 247 |
by (unfold inj_on_def, auto) |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
248 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
249 |
lemma Bnor_prod_power [rule_format]: |
35440 | 250 |
"x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset a m) = |
251 |
\<Prod>(BnorRset a m) * x^card (BnorRset a m)" |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
252 |
apply (induct a m rule: BnorRset_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
253 |
prefer 2 |
15481 | 254 |
apply (simplesubst BnorRset.simps) --{*multiple redexes*} |
13833 | 255 |
apply (unfold Let_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
256 |
apply (simp add: Bnor_fin Bnor_mem_zle_swap) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
257 |
apply (subst setprod_insert) |
13524 | 258 |
apply (rule_tac [2] Bnor_prod_power_aux) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
259 |
apply (unfold inj_on_def) |
40786
0a54cfc9add3
gave more standard finite set rules simp and intro attribute
nipkow
parents:
38159
diff
changeset
|
260 |
apply (simp_all add: zmult_ac Bnor_fin Bnor_mem_zle_swap) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
261 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
262 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
263 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
264 |
subsection {* Fermat *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
265 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
266 |
lemma bijzcong_zcong_prod: |
15392 | 267 |
"(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
268 |
apply (unfold zcongm_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
269 |
apply (erule bijR.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
270 |
apply (subgoal_tac [2] "a \<notin> A \<and> b \<notin> B \<and> finite A \<and> finite B") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
271 |
apply (auto intro: fin_bijRl fin_bijRr zcong_zmult) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
272 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
273 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
274 |
lemma Bnor_prod_zgcd [rule_format]: |
35440 | 275 |
"a < m --> zgcd (\<Prod>(BnorRset a m)) m = 1" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
276 |
apply (induct a m rule: BnorRset_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
277 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
278 |
apply (subst BnorRset.simps) |
13833 | 279 |
apply (unfold Let_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
280 |
apply (simp add: Bnor_fin Bnor_mem_zle_swap) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
281 |
apply (blast intro: zgcd_zgcd_zmult) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
282 |
done |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
283 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
284 |
theorem Euler_Fermat: |
27556 | 285 |
"0 < m ==> zgcd x m = 1 ==> [x^(phi m) = 1] (mod m)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
286 |
apply (unfold norRRset_def phi_def) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
287 |
apply (case_tac "x = 0") |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
288 |
apply (case_tac [2] "m = 1") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
289 |
apply (rule_tac [3] iffD1) |
35440 | 290 |
apply (rule_tac [3] k = "\<Prod>(BnorRset (m - 1) m)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
291 |
in zcong_cancel2) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
292 |
prefer 5 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
293 |
apply (subst Bnor_prod_power [symmetric]) |
13833 | 294 |
apply (rule_tac [7] Bnor_prod_zgcd, simp_all) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
295 |
apply (rule bijzcong_zcong_prod) |
35440 | 296 |
apply (fold norRRset_def, fold noXRRset_def) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
297 |
apply (subst RRset2norRR_eq_norR [symmetric]) |
13833 | 298 |
apply (rule_tac [3] inj_func_bijR, auto) |
13187 | 299 |
apply (unfold zcongm_def) |
300 |
apply (rule_tac [2] RRset2norRR_correct1) |
|
301 |
apply (rule_tac [5] RRset2norRR_inj) |
|
302 |
apply (auto intro: order_less_le [THEN iffD2] |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
303 |
simp add: noX_is_RRset) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
304 |
apply (unfold noXRRset_def norRRset_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
305 |
apply (rule finite_imageI) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
306 |
apply (rule Bnor_fin) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
307 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
308 |
|
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16663
diff
changeset
|
309 |
lemma Bnor_prime: |
35440 | 310 |
"\<lbrakk> zprime p; a < p \<rbrakk> \<Longrightarrow> card (BnorRset a p) = nat a" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
311 |
apply (induct a p rule: BnorRset.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
312 |
apply (subst BnorRset.simps) |
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16663
diff
changeset
|
313 |
apply (unfold Let_def, auto simp add:zless_zprime_imp_zrelprime) |
35440 | 314 |
apply (subgoal_tac "finite (BnorRset (a - 1) m)") |
315 |
apply (subgoal_tac "a ~: BnorRset (a - 1) m") |
|
13833 | 316 |
apply (auto simp add: card_insert_disjoint Suc_nat_eq_nat_zadd1) |
317 |
apply (frule Bnor_mem_zle, arith) |
|
318 |
apply (frule Bnor_fin) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
319 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
320 |
|
16663 | 321 |
lemma phi_prime: "zprime p ==> phi p = nat (p - 1)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
322 |
apply (unfold phi_def norRRset_def) |
13833 | 323 |
apply (rule Bnor_prime, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
324 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
325 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
326 |
theorem Little_Fermat: |
16663 | 327 |
"zprime p ==> \<not> p dvd x ==> [x^(nat (p - 1)) = 1] (mod p)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
328 |
apply (subst phi_prime [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
329 |
apply (rule_tac [2] Euler_Fermat) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
330 |
apply (erule_tac [3] zprime_imp_zrelprime) |
13833 | 331 |
apply (unfold zprime_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
332 |
done |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
333 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
334 |
end |