author | wenzelm |
Tue, 10 Nov 2009 15:33:35 +0100 | |
changeset 33552 | 506f80a9afe8 |
parent 32960 | 69916a850301 |
child 35048 | 82ab78fff970 |
permissions | -rw-r--r-- |
32479 | 1 |
(* Author: Thomas M. Rasmussen |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
2 |
Copyright 2000 University of Cambridge |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
3 |
*) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
4 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
5 |
header {* Wilson's Theorem according to Russinoff *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
6 |
|
16417 | 7 |
theory WilsonRuss imports EulerFermat begin |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
8 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
9 |
text {* |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
10 |
Wilson's Theorem following quite closely Russinoff's approach |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
11 |
using Boyer-Moore (using finite sets instead of lists, though). |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
12 |
*} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
13 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
14 |
subsection {* Definitions and lemmas *} |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
15 |
|
19670 | 16 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19670
diff
changeset
|
17 |
inv :: "int => int => int" where |
19670 | 18 |
"inv p a = (a^(nat (p - 2))) mod p" |
19 |
||
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
20 |
consts |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
21 |
wset :: "int * int => int set" |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
22 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
23 |
recdef wset |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
24 |
"measure ((\<lambda>(a, p). nat a) :: int * int => nat)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
25 |
"wset (a, p) = |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
26 |
(if 1 < a then |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
27 |
let ws = wset (a - 1, p) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
28 |
in (if a \<in> ws then ws else insert a (insert (inv p a) ws)) else {})" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
29 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
30 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
31 |
text {* \medskip @{term [source] inv} *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
32 |
|
13524 | 33 |
lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)" |
13833 | 34 |
by (subst int_int_eq [symmetric], auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
35 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
36 |
lemma inv_is_inv: |
16663 | 37 |
"zprime p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> [a * inv p a = 1] (mod p)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
38 |
apply (unfold inv_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
39 |
apply (subst zcong_zmod) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
40 |
apply (subst zmod_zmult1_eq [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
41 |
apply (subst zcong_zmod [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
42 |
apply (subst power_Suc [symmetric]) |
13524 | 43 |
apply (subst inv_is_inv_aux) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
44 |
apply (erule_tac [2] Little_Fermat) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
45 |
apply (erule_tac [2] zdvd_not_zless) |
13833 | 46 |
apply (unfold zprime_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
47 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
48 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
49 |
lemma inv_distinct: |
16663 | 50 |
"zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> a \<noteq> inv p a" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
51 |
apply safe |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
52 |
apply (cut_tac a = a and p = p in zcong_square) |
13833 | 53 |
apply (cut_tac [3] a = a and p = p in inv_is_inv, auto) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
54 |
apply (subgoal_tac "a = 1") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
55 |
apply (rule_tac [2] m = p in zcong_zless_imp_eq) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
56 |
apply (subgoal_tac [7] "a = p - 1") |
13833 | 57 |
apply (rule_tac [8] m = p in zcong_zless_imp_eq, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
58 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
59 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
60 |
lemma inv_not_0: |
16663 | 61 |
"zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> 0" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
62 |
apply safe |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
63 |
apply (cut_tac a = a and p = p in inv_is_inv) |
13833 | 64 |
apply (unfold zcong_def, auto) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
65 |
apply (subgoal_tac "\<not> p dvd 1") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
66 |
apply (rule_tac [2] zdvd_not_zless) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
67 |
apply (subgoal_tac "p dvd 1") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
68 |
prefer 2 |
30042 | 69 |
apply (subst dvd_minus_iff [symmetric], auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
70 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
71 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
72 |
lemma inv_not_1: |
16663 | 73 |
"zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> 1" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
74 |
apply safe |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
75 |
apply (cut_tac a = a and p = p in inv_is_inv) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
76 |
prefer 4 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
77 |
apply simp |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
78 |
apply (subgoal_tac "a = 1") |
13833 | 79 |
apply (rule_tac [2] zcong_zless_imp_eq, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
80 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
81 |
|
19670 | 82 |
lemma inv_not_p_minus_1_aux: |
83 |
"[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)" |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
84 |
apply (unfold zcong_def) |
14738 | 85 |
apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
86 |
apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) |
14271 | 87 |
apply (simp add: mult_commute) |
30042 | 88 |
apply (subst dvd_minus_iff) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
89 |
apply (subst zdvd_reduce) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
90 |
apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans) |
13833 | 91 |
apply (subst zdvd_reduce, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
92 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
93 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
94 |
lemma inv_not_p_minus_1: |
16663 | 95 |
"zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> p - 1" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
96 |
apply safe |
13833 | 97 |
apply (cut_tac a = a and p = p in inv_is_inv, auto) |
13524 | 98 |
apply (simp add: inv_not_p_minus_1_aux) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
99 |
apply (subgoal_tac "a = p - 1") |
13833 | 100 |
apply (rule_tac [2] zcong_zless_imp_eq, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
101 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
102 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
103 |
lemma inv_g_1: |
16663 | 104 |
"zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> 1 < inv p a" |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
105 |
apply (case_tac "0\<le> inv p a") |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
106 |
apply (subgoal_tac "inv p a \<noteq> 1") |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
107 |
apply (subgoal_tac "inv p a \<noteq> 0") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
108 |
apply (subst order_less_le) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
109 |
apply (subst zle_add1_eq_le [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
110 |
apply (subst order_less_le) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
111 |
apply (rule_tac [2] inv_not_0) |
13833 | 112 |
apply (rule_tac [5] inv_not_1, auto) |
113 |
apply (unfold inv_def zprime_def, simp) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
114 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
115 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
116 |
lemma inv_less_p_minus_1: |
16663 | 117 |
"zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a < p - 1" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
118 |
apply (case_tac "inv p a < p") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
119 |
apply (subst order_less_le) |
13833 | 120 |
apply (simp add: inv_not_p_minus_1, auto) |
121 |
apply (unfold inv_def zprime_def, simp) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
122 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
123 |
|
13524 | 124 |
lemma inv_inv_aux: "5 \<le> p ==> |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
125 |
nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
126 |
apply (subst int_int_eq [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
127 |
apply (simp add: zmult_int [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
128 |
apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
129 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
130 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
131 |
lemma zcong_zpower_zmult: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
132 |
"[x^y = 1] (mod p) \<Longrightarrow> [x^(y * z) = 1] (mod p)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
133 |
apply (induct z) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
134 |
apply (auto simp add: zpower_zadd_distrib) |
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15197
diff
changeset
|
135 |
apply (subgoal_tac "zcong (x^y * x^(y * z)) (1 * 1) p") |
13833 | 136 |
apply (rule_tac [2] zcong_zmult, simp_all) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
137 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
138 |
|
16663 | 139 |
lemma inv_inv: "zprime p \<Longrightarrow> |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
140 |
5 \<le> p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
141 |
apply (unfold inv_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
142 |
apply (subst zpower_zmod) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
143 |
apply (subst zpower_zpower) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
144 |
apply (rule zcong_zless_imp_eq) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
145 |
prefer 5 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
146 |
apply (subst zcong_zmod) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
147 |
apply (subst mod_mod_trivial) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
148 |
apply (subst zcong_zmod [symmetric]) |
13524 | 149 |
apply (subst inv_inv_aux) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
150 |
apply (subgoal_tac [2] |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
151 |
"zcong (a * a^(nat (p - 1) * nat (p - 3))) (a * 1) p") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
152 |
apply (rule_tac [3] zcong_zmult) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
153 |
apply (rule_tac [4] zcong_zpower_zmult) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
154 |
apply (erule_tac [4] Little_Fermat) |
13833 | 155 |
apply (rule_tac [4] zdvd_not_zless, simp_all) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
156 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
157 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
158 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
159 |
text {* \medskip @{term wset} *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
160 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
161 |
declare wset.simps [simp del] |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
162 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
163 |
lemma wset_induct: |
18369 | 164 |
assumes "!!a p. P {} a p" |
19670 | 165 |
and "!!a p. 1 < (a::int) \<Longrightarrow> |
166 |
P (wset (a - 1, p)) (a - 1) p ==> P (wset (a, p)) a p" |
|
18369 | 167 |
shows "P (wset (u, v)) u v" |
168 |
apply (rule wset.induct, safe) |
|
169 |
prefer 2 |
|
170 |
apply (case_tac "1 < a") |
|
171 |
apply (rule prems) |
|
172 |
apply simp_all |
|
173 |
apply (simp_all add: wset.simps prems) |
|
174 |
done |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
175 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
176 |
lemma wset_mem_imp_or [rule_format]: |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
177 |
"1 < a \<Longrightarrow> b \<notin> wset (a - 1, p) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
178 |
==> b \<in> wset (a, p) --> b = a \<or> b = inv p a" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
179 |
apply (subst wset.simps) |
13833 | 180 |
apply (unfold Let_def, simp) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
181 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
182 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
183 |
lemma wset_mem_mem [simp]: "1 < a ==> a \<in> wset (a, p)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
184 |
apply (subst wset.simps) |
13833 | 185 |
apply (unfold Let_def, simp) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
186 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
187 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
188 |
lemma wset_subset: "1 < a \<Longrightarrow> b \<in> wset (a - 1, p) ==> b \<in> wset (a, p)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
189 |
apply (subst wset.simps) |
13833 | 190 |
apply (unfold Let_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
191 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
192 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
193 |
lemma wset_g_1 [rule_format]: |
16663 | 194 |
"zprime p --> a < p - 1 --> b \<in> wset (a, p) --> 1 < b" |
13833 | 195 |
apply (induct a p rule: wset_induct, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
196 |
apply (case_tac "b = a") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
197 |
apply (case_tac [2] "b = inv p a") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
198 |
apply (subgoal_tac [3] "b = a \<or> b = inv p a") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
199 |
apply (rule_tac [4] wset_mem_imp_or) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
200 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
201 |
apply simp |
13833 | 202 |
apply (rule inv_g_1, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
203 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
204 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
205 |
lemma wset_less [rule_format]: |
16663 | 206 |
"zprime p --> a < p - 1 --> b \<in> wset (a, p) --> b < p - 1" |
13833 | 207 |
apply (induct a p rule: wset_induct, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
208 |
apply (case_tac "b = a") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
209 |
apply (case_tac [2] "b = inv p a") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
210 |
apply (subgoal_tac [3] "b = a \<or> b = inv p a") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
211 |
apply (rule_tac [4] wset_mem_imp_or) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
212 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
213 |
apply simp |
13833 | 214 |
apply (rule inv_less_p_minus_1, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
215 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
216 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
217 |
lemma wset_mem [rule_format]: |
16663 | 218 |
"zprime p --> |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
219 |
a < p - 1 --> 1 < b --> b \<le> a --> b \<in> wset (a, p)" |
13833 | 220 |
apply (induct a p rule: wset.induct, auto) |
15197 | 221 |
apply (rule_tac wset_subset) |
222 |
apply (simp (no_asm_simp)) |
|
223 |
apply auto |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
224 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
225 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
226 |
lemma wset_mem_inv_mem [rule_format]: |
16663 | 227 |
"zprime p --> 5 \<le> p --> a < p - 1 --> b \<in> wset (a, p) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
228 |
--> inv p b \<in> wset (a, p)" |
13833 | 229 |
apply (induct a p rule: wset_induct, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
230 |
apply (case_tac "b = a") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
231 |
apply (subst wset.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
232 |
apply (unfold Let_def) |
13833 | 233 |
apply (rule_tac [3] wset_subset, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
234 |
apply (case_tac "b = inv p a") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
235 |
apply (simp (no_asm_simp)) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
236 |
apply (subst inv_inv) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
237 |
apply (subgoal_tac [6] "b = a \<or> b = inv p a") |
13833 | 238 |
apply (rule_tac [7] wset_mem_imp_or, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
239 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
240 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
241 |
lemma wset_inv_mem_mem: |
16663 | 242 |
"zprime p \<Longrightarrow> 5 \<le> p \<Longrightarrow> a < p - 1 \<Longrightarrow> 1 < b \<Longrightarrow> b < p - 1 |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
243 |
\<Longrightarrow> inv p b \<in> wset (a, p) \<Longrightarrow> b \<in> wset (a, p)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
244 |
apply (rule_tac s = "inv p (inv p b)" and t = b in subst) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
245 |
apply (rule_tac [2] wset_mem_inv_mem) |
13833 | 246 |
apply (rule inv_inv, simp_all) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
247 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
248 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
249 |
lemma wset_fin: "finite (wset (a, p))" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
250 |
apply (induct a p rule: wset_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
251 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
252 |
apply (subst wset.simps) |
13833 | 253 |
apply (unfold Let_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
254 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
255 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
256 |
lemma wset_zcong_prod_1 [rule_format]: |
16663 | 257 |
"zprime p --> |
15392 | 258 |
5 \<le> p --> a < p - 1 --> [(\<Prod>x\<in>wset(a, p). x) = 1] (mod p)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
259 |
apply (induct a p rule: wset_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
260 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
261 |
apply (subst wset.simps) |
13833 | 262 |
apply (unfold Let_def, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
263 |
apply (subst setprod_insert) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
264 |
apply (tactic {* stac (thm "setprod_insert") 3 *}) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
265 |
apply (subgoal_tac [5] |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
266 |
"zcong (a * inv p a * (\<Prod>x\<in> wset(a - 1, p). x)) (1 * 1) p") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
267 |
prefer 5 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
268 |
apply (simp add: zmult_assoc) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
269 |
apply (rule_tac [5] zcong_zmult) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
270 |
apply (rule_tac [5] inv_is_inv) |
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
21404
diff
changeset
|
271 |
apply (tactic "clarify_tac @{claset} 4") |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
272 |
apply (subgoal_tac [4] "a \<in> wset (a - 1, p)") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
273 |
apply (rule_tac [5] wset_inv_mem_mem) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
274 |
apply (simp_all add: wset_fin) |
13833 | 275 |
apply (rule inv_distinct, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
276 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
277 |
|
16663 | 278 |
lemma d22set_eq_wset: "zprime p ==> d22set (p - 2) = wset (p - 2, p)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
279 |
apply safe |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
280 |
apply (erule wset_mem) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
281 |
apply (rule_tac [2] d22set_g_1) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
282 |
apply (rule_tac [3] d22set_le) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
283 |
apply (rule_tac [4] d22set_mem) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
284 |
apply (erule_tac [4] wset_g_1) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
285 |
prefer 6 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
286 |
apply (subst zle_add1_eq_le [symmetric]) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
287 |
apply (subgoal_tac "p - 2 + 1 = p - 1") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
288 |
apply (simp (no_asm_simp)) |
13833 | 289 |
apply (erule wset_less, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
290 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
291 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
292 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
293 |
subsection {* Wilson *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
294 |
|
16663 | 295 |
lemma prime_g_5: "zprime p \<Longrightarrow> p \<noteq> 2 \<Longrightarrow> p \<noteq> 3 ==> 5 \<le> p" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
296 |
apply (unfold zprime_def dvd_def) |
13833 | 297 |
apply (case_tac "p = 4", auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
298 |
apply (rule notE) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
299 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
300 |
apply assumption |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
301 |
apply (simp (no_asm)) |
13833 | 302 |
apply (rule_tac x = 2 in exI) |
303 |
apply (safe, arith) |
|
304 |
apply (rule_tac x = 2 in exI, auto) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
305 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
306 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
307 |
theorem Wilson_Russ: |
16663 | 308 |
"zprime p ==> [zfact (p - 1) = -1] (mod p)" |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
309 |
apply (subgoal_tac "[(p - 1) * zfact (p - 2) = -1 * 1] (mod p)") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
310 |
apply (rule_tac [2] zcong_zmult) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
311 |
apply (simp only: zprime_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
312 |
apply (subst zfact.simps) |
13833 | 313 |
apply (rule_tac t = "p - 1 - 1" and s = "p - 2" in subst, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
314 |
apply (simp only: zcong_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
315 |
apply (simp (no_asm_simp)) |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
316 |
apply (case_tac "p = 2") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
317 |
apply (simp add: zfact.simps) |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
318 |
apply (case_tac "p = 3") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
319 |
apply (simp add: zfact.simps) |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
320 |
apply (subgoal_tac "5 \<le> p") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
321 |
apply (erule_tac [2] prime_g_5) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
322 |
apply (subst d22set_prod_zfact [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
323 |
apply (subst d22set_eq_wset) |
13833 | 324 |
apply (rule_tac [2] wset_zcong_prod_1, auto) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
325 |
done |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
326 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
327 |
end |