author | paulson |
Wed, 26 Feb 2003 13:16:07 +0100 | |
changeset 13833 | f8dcb1d9ea68 |
parent 13524 | 604d0f3622d6 |
child 14174 | f3cafd2929d5 |
permissions | -rw-r--r-- |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
1 |
(* Title: HOL/NumberTheory/EulerFermat.thy |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
3 |
Author: Thomas M. Rasmussen |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
4 |
Copyright 2000 University of Cambridge |
13833 | 5 |
|
6 |
Changes by Jeremy Avigad, 2003/02/21: |
|
7 |
repaired proof of Bnor_prime (removed use of zprime_def) |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
8 |
*) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
9 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
10 |
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
|
11 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
12 |
theory EulerFermat = BijectionRel + IntFact: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
13 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
14 |
text {* |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
15 |
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
|
16 |
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
|
17 |
the extended version). |
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 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
20 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
21 |
subsection {* Definitions and lemmas *} |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
22 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
23 |
consts |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
24 |
RsetR :: "int => int set set" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
25 |
BnorRset :: "int * int => int set" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
26 |
norRRset :: "int => int set" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
27 |
noXRRset :: "int => int => int set" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
28 |
phi :: "int => nat" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
29 |
is_RRset :: "int set => int => bool" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
30 |
RRset2norRR :: "int set => int => int => int" |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
31 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
32 |
inductive "RsetR m" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
33 |
intros |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
34 |
empty [simp]: "{} \<in> RsetR m" |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
35 |
insert: "A \<in> RsetR m ==> zgcd (a, m) = 1 ==> |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
36 |
\<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
|
37 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
38 |
recdef BnorRset |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
39 |
"measure ((\<lambda>(a, m). nat a) :: int * int => nat)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
40 |
"BnorRset (a, m) = |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
41 |
(if 0 < a then |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
42 |
let na = BnorRset (a - 1, m) |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
43 |
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
|
44 |
else {})" |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
45 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
46 |
defs |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
47 |
norRRset_def: "norRRset m == BnorRset (m - 1, m)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
48 |
noXRRset_def: "noXRRset m x == (\<lambda>a. a * x) ` norRRset m" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
49 |
phi_def: "phi m == card (norRRset m)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
50 |
is_RRset_def: "is_RRset A m == A \<in> RsetR m \<and> card A = phi m" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
51 |
RRset2norRR_def: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
52 |
"RRset2norRR A m a == |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
53 |
(if 1 < m \<and> is_RRset A m \<and> a \<in> A then |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
54 |
SOME b. zcong a b m \<and> b \<in> norRRset m |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
55 |
else 0)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
56 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
57 |
constdefs |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
58 |
zcongm :: "int => int => int => bool" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
59 |
"zcongm m == \<lambda>a b. zcong a b m" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
60 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
61 |
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
|
62 |
-- {* LCP: not sure why this lemma is needed now *} |
13833 | 63 |
by (auto simp add: zabs_def) |
11049
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 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
66 |
text {* \medskip @{text norRRset} *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
67 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
68 |
declare BnorRset.simps [simp del] |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
69 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
70 |
lemma BnorRset_induct: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
71 |
"(!!a m. P {} a m) ==> |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
72 |
(!!a m. 0 < (a::int) ==> P (BnorRset (a - 1, m::int)) (a - 1) m |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
73 |
==> P (BnorRset(a,m)) a m) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
74 |
==> P (BnorRset(u,v)) u v" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
75 |
proof - |
11549 | 76 |
case rule_context |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
77 |
show ?thesis |
13833 | 78 |
apply (rule BnorRset.induct, safe) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
79 |
apply (case_tac [2] "0 < a") |
13833 | 80 |
apply (rule_tac [2] rule_context, simp_all) |
11549 | 81 |
apply (simp_all add: BnorRset.simps rule_context) |
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 |
qed |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
84 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
85 |
lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset (a, m) --> b \<le> a" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
86 |
apply (induct a m rule: BnorRset_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
87 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
88 |
apply (subst BnorRset.simps) |
13833 | 89 |
apply (unfold Let_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
90 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
91 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
92 |
lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset (a, m)" |
13833 | 93 |
by (auto dest: Bnor_mem_zle) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
94 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
95 |
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
|
96 |
apply (induct a m rule: BnorRset_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
97 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
98 |
apply (subst BnorRset.simps) |
13833 | 99 |
apply (unfold Let_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
100 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
101 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
102 |
lemma Bnor_mem_if [rule_format]: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
103 |
"zgcd (b, m) = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset (a, m)" |
13833 | 104 |
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
|
105 |
apply (case_tac "a = b") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
106 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
107 |
apply (simp add: order_less_le) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
108 |
apply (simp (no_asm_simp)) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
109 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
110 |
apply (subst BnorRset.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
111 |
defer |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
112 |
apply (subst BnorRset.simps) |
13833 | 113 |
apply (unfold Let_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
114 |
done |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
115 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
116 |
lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset (a, m) \<in> RsetR m" |
13833 | 117 |
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
|
118 |
apply (subst BnorRset.simps) |
13833 | 119 |
apply (unfold Let_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
120 |
apply (rule RsetR.insert) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
121 |
apply (rule_tac [3] allI) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
122 |
apply (rule_tac [3] impI) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
123 |
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
|
124 |
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
|
125 |
apply (rule_tac [7] Bnor_mem_zle) |
13833 | 126 |
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
|
127 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
128 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
129 |
lemma Bnor_fin: "finite (BnorRset (a, m))" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
130 |
apply (induct a m rule: BnorRset_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
131 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
132 |
apply (subst BnorRset.simps) |
13833 | 133 |
apply (unfold Let_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
134 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
135 |
|
13524 | 136 |
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
|
137 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
138 |
done |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
139 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
140 |
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
|
141 |
"1 < m ==> |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
142 |
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
|
143 |
apply (unfold norRRset_def) |
13833 | 144 |
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
|
145 |
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
|
146 |
apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans |
13524 | 147 |
order_less_imp_le norR_mem_unique_aux simp add: zcong_sym) |
13833 | 148 |
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
|
149 |
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
|
150 |
apply (case_tac [2] "b = 0") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
151 |
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
|
152 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
153 |
apply (simp only: zcong_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
154 |
apply (subgoal_tac "zgcd (a, m) = m") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
155 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
156 |
apply (subst zdvd_iff_zgcd [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
157 |
apply (rule_tac [4] zgcd_zcong_zgcd) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
158 |
apply (simp_all add: zdvd_zminus_iff zcong_sym) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
159 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
160 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
161 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
162 |
text {* \medskip @{term noXRRset} *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
163 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
164 |
lemma RRset_gcd [rule_format]: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
165 |
"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
|
166 |
apply (unfold is_RRset_def) |
13833 | 167 |
apply (rule RsetR.induct, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
168 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
169 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
170 |
lemma RsetR_zmult_mono: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
171 |
"A \<in> RsetR m ==> |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
172 |
0 < m ==> zgcd (x, m) = 1 ==> (\<lambda>a. a * x) ` A \<in> RsetR m" |
13833 | 173 |
apply (erule RsetR.induct, simp_all) |
174 |
apply (rule RsetR.insert, auto) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
175 |
apply (blast intro: zgcd_zgcd_zmult) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
176 |
apply (simp add: zcong_cancel) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
177 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
178 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
179 |
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
|
180 |
"0 < m ==> |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
181 |
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
|
182 |
apply (unfold norRRset_def noXRRset_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
183 |
apply (rule card_image) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
184 |
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
|
185 |
apply (simp add: BnorRset.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
186 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
187 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
188 |
lemma noX_is_RRset: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
189 |
"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
|
190 |
apply (unfold is_RRset_def phi_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
191 |
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
|
192 |
apply (unfold noXRRset_def norRRset_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
193 |
apply (rule RsetR_zmult_mono) |
13833 | 194 |
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
|
195 |
done |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
196 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
197 |
lemma aux_some: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
198 |
"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
|
199 |
==> 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
|
200 |
(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
|
201 |
apply (rule norR_mem_unique [THEN ex1_implies_ex, THEN someI_ex]) |
13833 | 202 |
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
|
203 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
204 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
205 |
lemma RRset2norRR_correct: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
206 |
"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
|
207 |
[a = RRset2norRR A m a] (mod m) \<and> RRset2norRR A m a \<in> norRRset m" |
13833 | 208 |
apply (unfold RRset2norRR_def, simp) |
209 |
apply (rule aux_some, simp_all) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
210 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
211 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
212 |
lemmas RRset2norRR_correct1 = |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
213 |
RRset2norRR_correct [THEN conjunct1, standard] |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
214 |
lemmas RRset2norRR_correct2 = |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
215 |
RRset2norRR_correct [THEN conjunct2, standard] |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
216 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
217 |
lemma RsetR_fin: "A \<in> RsetR m ==> finite A" |
13833 | 218 |
by (erule RsetR.induct, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
219 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
220 |
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
|
221 |
"1 < m ==> |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
222 |
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
|
223 |
apply (unfold is_RRset_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
224 |
apply (rule RsetR.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
225 |
apply (auto simp add: zcong_sym) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
226 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
227 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
228 |
lemma aux: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
229 |
"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
|
230 |
(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
|
231 |
apply auto |
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_inj: |
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 ==> inj_on (RRset2norRR A m) A" |
13833 | 236 |
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
|
237 |
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
|
238 |
([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
|
239 |
apply (rule_tac [2] aux) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
240 |
apply (rule_tac [3] aux_some) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
241 |
apply (rule_tac [2] aux_some) |
13833 | 242 |
apply (rule RRset_zcong_eq, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
243 |
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
|
244 |
apply (simp_all add: zcong_sym) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
245 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
246 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
247 |
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
|
248 |
"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
|
249 |
apply (rule card_seteq) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
250 |
prefer 3 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
251 |
apply (subst card_image) |
13833 | 252 |
apply (rule_tac [2] RRset2norRR_inj, auto) |
253 |
apply (rule_tac [4] RRset2norRR_correct2, auto) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
254 |
apply (unfold is_RRset_def phi_def norRRset_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
255 |
apply (auto simp add: RsetR_fin Bnor_fin) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
256 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
257 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
258 |
|
13524 | 259 |
lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A" |
13833 | 260 |
by (unfold inj_on_def, auto) |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
261 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
262 |
lemma Bnor_prod_power [rule_format]: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
263 |
"x \<noteq> 0 ==> a < m --> setprod ((\<lambda>a. a * x) ` BnorRset (a, m)) = |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
264 |
setprod (BnorRset(a, m)) * x^card (BnorRset (a, m))" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
265 |
apply (induct a m rule: BnorRset_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
266 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
267 |
apply (subst BnorRset.simps) |
13833 | 268 |
apply (unfold Let_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
269 |
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
|
270 |
apply (subst setprod_insert) |
13524 | 271 |
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
|
272 |
apply (unfold inj_on_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
273 |
apply (simp_all add: zmult_ac Bnor_fin finite_imageI |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
274 |
Bnor_mem_zle_swap) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
275 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
276 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
277 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
278 |
subsection {* Fermat *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
279 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
280 |
lemma bijzcong_zcong_prod: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
281 |
"(A, B) \<in> bijR (zcongm m) ==> [setprod A = setprod B] (mod m)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
282 |
apply (unfold zcongm_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
283 |
apply (erule bijR.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
284 |
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
|
285 |
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
|
286 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
287 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
288 |
lemma Bnor_prod_zgcd [rule_format]: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
289 |
"a < m --> zgcd (setprod (BnorRset (a, m)), m) = 1" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
290 |
apply (induct a m rule: BnorRset_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
291 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
292 |
apply (subst BnorRset.simps) |
13833 | 293 |
apply (unfold Let_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
294 |
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
|
295 |
apply (blast intro: zgcd_zgcd_zmult) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
296 |
done |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
297 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
298 |
theorem Euler_Fermat: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
299 |
"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
|
300 |
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
|
301 |
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
|
302 |
apply (case_tac [2] "m = 1") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
303 |
apply (rule_tac [3] iffD1) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
304 |
apply (rule_tac [3] k = "setprod (BnorRset (m - 1, m))" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
305 |
in zcong_cancel2) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
306 |
prefer 5 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
307 |
apply (subst Bnor_prod_power [symmetric]) |
13833 | 308 |
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
|
309 |
apply (rule bijzcong_zcong_prod) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
310 |
apply (fold norRRset_def noXRRset_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
311 |
apply (subst RRset2norRR_eq_norR [symmetric]) |
13833 | 312 |
apply (rule_tac [3] inj_func_bijR, auto) |
13187 | 313 |
apply (unfold zcongm_def) |
314 |
apply (rule_tac [2] RRset2norRR_correct1) |
|
315 |
apply (rule_tac [5] RRset2norRR_inj) |
|
316 |
apply (auto intro: order_less_le [THEN iffD2] |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
317 |
simp add: noX_is_RRset) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
318 |
apply (unfold noXRRset_def norRRset_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
319 |
apply (rule finite_imageI) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
320 |
apply (rule Bnor_fin) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
321 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
322 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
323 |
lemma Bnor_prime [rule_format (no_asm)]: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
324 |
"p \<in> zprime ==> |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
325 |
a < p --> (\<forall>b. 0 < b \<and> b \<le> a --> zgcd (b, p) = 1) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
326 |
--> card (BnorRset (a, p)) = nat a" |
13833 | 327 |
apply (auto simp add: zless_zprime_imp_zrelprime) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
328 |
apply (induct a p rule: BnorRset.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
329 |
apply (subst BnorRset.simps) |
13833 | 330 |
apply (unfold Let_def, auto) |
331 |
apply (subgoal_tac "finite (BnorRset (a - 1,m))") |
|
332 |
apply (subgoal_tac "a ~: BnorRset (a - 1,m)") |
|
333 |
apply (auto simp add: card_insert_disjoint Suc_nat_eq_nat_zadd1) |
|
334 |
apply (frule Bnor_mem_zle, arith) |
|
335 |
apply (frule Bnor_fin) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
336 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
337 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
338 |
lemma phi_prime: "p \<in> zprime ==> phi p = nat (p - 1)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
339 |
apply (unfold phi_def norRRset_def) |
13833 | 340 |
apply (rule Bnor_prime, auto) |
341 |
apply (erule zless_zprime_imp_zrelprime, simp_all) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
342 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
343 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
344 |
theorem Little_Fermat: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
345 |
"p \<in> zprime ==> \<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
|
346 |
apply (subst phi_prime [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
347 |
apply (rule_tac [2] Euler_Fermat) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
348 |
apply (erule_tac [3] zprime_imp_zrelprime) |
13833 | 349 |
apply (unfold zprime_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10834
diff
changeset
|
350 |
done |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
351 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
352 |
end |