author | wenzelm |
Mon, 19 Jan 2015 20:39:01 +0100 | |
changeset 59409 | b7cfe12acf2e |
parent 58889 | 5b7a9633cfa8 |
child 59498 | 50b60f501b05 |
permissions | -rw-r--r-- |
38159 | 1 |
(* Title: HOL/Old_Number_Theory/WilsonBij.thy |
2 |
Author: Thomas M. Rasmussen |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
3 |
Copyright 2000 University of Cambridge |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
4 |
*) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
5 |
|
58889 | 6 |
section {* Wilson's Theorem using a more abstract approach *} |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
7 |
|
38159 | 8 |
theory WilsonBij |
9 |
imports BijectionRel IntFact |
|
10 |
begin |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
11 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
12 |
text {* |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
13 |
Wilson's Theorem using a more ``abstract'' approach based on |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
14 |
bijections between sets. Does not use Fermat's Little Theorem |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
15 |
(unlike Russinoff). |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
16 |
*} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
17 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
18 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
19 |
subsection {* Definitions and lemmas *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
20 |
|
38159 | 21 |
definition reciR :: "int => int => int => bool" |
22 |
where "reciR p = (\<lambda>a b. zcong (a * b) 1 p \<and> 1 < a \<and> a < p - 1 \<and> 1 < b \<and> b < p - 1)" |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19670
diff
changeset
|
23 |
|
38159 | 24 |
definition inv :: "int => int => int" where |
19670 | 25 |
"inv p a = |
26 |
(if zprime p \<and> 0 < a \<and> a < p then |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
27 |
(SOME x. 0 \<le> x \<and> x < p \<and> zcong (a * x) 1 p) |
19670 | 28 |
else 0)" |
11049
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 Inverse *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
32 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
33 |
lemma inv_correct: |
16663 | 34 |
"zprime p ==> 0 < a ==> a < p |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
35 |
==> 0 \<le> inv p a \<and> inv p a < p \<and> [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
|
36 |
apply (unfold inv_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
37 |
apply (simp (no_asm_simp)) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
38 |
apply (rule zcong_lineq_unique [THEN ex1_implies_ex, THEN someI_ex]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
39 |
apply (erule_tac [2] zless_zprime_imp_zrelprime) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
40 |
apply (unfold zprime_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
41 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
42 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
43 |
|
45605 | 44 |
lemmas inv_ge = inv_correct [THEN conjunct1] |
45 |
lemmas inv_less = inv_correct [THEN conjunct2, THEN conjunct1] |
|
46 |
lemmas inv_is_inv = inv_correct [THEN conjunct2, THEN conjunct2] |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
47 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
48 |
lemma inv_not_0: |
16663 | 49 |
"zprime p ==> 1 < a ==> 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
|
50 |
-- {* same as @{text WilsonRuss} *} |
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 inv_is_inv) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
53 |
apply (unfold zcong_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
54 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
55 |
done |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
56 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
57 |
lemma inv_not_1: |
16663 | 58 |
"zprime p ==> 1 < a ==> 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
|
59 |
-- {* same as @{text WilsonRuss} *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
60 |
apply safe |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
61 |
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
|
62 |
prefer 4 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
63 |
apply simp |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
64 |
apply (subgoal_tac "a = 1") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
65 |
apply (rule_tac [2] zcong_zless_imp_eq) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
66 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
67 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
68 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
69 |
lemma aux: "[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
|
70 |
-- {* same as @{text WilsonRuss} *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
71 |
apply (unfold zcong_def) |
44766 | 72 |
apply (simp add: diff_diff_eq diff_diff_eq2 right_diff_distrib) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
73 |
apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) |
35048 | 74 |
apply (simp add: algebra_simps) |
30042 | 75 |
apply (subst dvd_minus_iff) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
76 |
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
|
77 |
apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
78 |
apply (subst zdvd_reduce) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
79 |
apply auto |
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 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
82 |
lemma inv_not_p_minus_1: |
16663 | 83 |
"zprime p ==> 1 < a ==> 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
|
84 |
-- {* same as @{text WilsonRuss} *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
85 |
apply safe |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
86 |
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
|
87 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
88 |
apply (simp add: aux) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
89 |
apply (subgoal_tac "a = p - 1") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
90 |
apply (rule_tac [2] zcong_zless_imp_eq) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
91 |
apply auto |
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 |
text {* |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
95 |
Below is slightly different as we don't expand @{term [source] inv} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
96 |
but use ``@{text correct}'' theorems. |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
97 |
*} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
98 |
|
16663 | 99 |
lemma inv_g_1: "zprime p ==> 1 < a ==> 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
|
100 |
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
|
101 |
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
|
102 |
apply (subst order_less_le) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
103 |
apply (subst zle_add1_eq_le [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
104 |
apply (subst order_less_le) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
105 |
apply (rule_tac [2] inv_not_0) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
106 |
apply (rule_tac [5] inv_not_1) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
107 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
108 |
apply (rule inv_ge) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
109 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
110 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
111 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
112 |
lemma inv_less_p_minus_1: |
16663 | 113 |
"zprime p ==> 1 < a ==> 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
|
114 |
-- {* ditto *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
115 |
apply (subst order_less_le) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
116 |
apply (simp add: inv_not_p_minus_1 inv_less) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
117 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
118 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
119 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
120 |
text {* \medskip Bijection *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
121 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
122 |
lemma aux1: "1 < x ==> 0 \<le> (x::int)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
123 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
124 |
done |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
125 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
126 |
lemma aux2: "1 < x ==> 0 < (x::int)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
127 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
128 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
129 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
130 |
lemma aux3: "x \<le> p - 2 ==> x < (p::int)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
131 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
132 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
133 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
134 |
lemma aux4: "x \<le> p - 2 ==> x < (p::int) - 1" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
135 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
136 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
137 |
|
16663 | 138 |
lemma inv_inj: "zprime p ==> inj_on (inv p) (d22set (p - 2))" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
139 |
apply (unfold inj_on_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
140 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
141 |
apply (rule zcong_zless_imp_eq) |
39159 | 142 |
apply (tactic {* stac (@{thm zcong_cancel} RS sym) 5 *}) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
143 |
apply (rule_tac [7] zcong_trans) |
39159 | 144 |
apply (tactic {* stac @{thm zcong_sym} 8 *}) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
145 |
apply (erule_tac [7] inv_is_inv) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47268
diff
changeset
|
146 |
apply (tactic "asm_simp_tac @{context} 9") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
147 |
apply (erule_tac [9] inv_is_inv) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
148 |
apply (rule_tac [6] zless_zprime_imp_zrelprime) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
149 |
apply (rule_tac [8] inv_less) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
150 |
apply (rule_tac [7] inv_g_1 [THEN aux2]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
151 |
apply (unfold zprime_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
152 |
apply (auto intro: d22set_g_1 d22set_le |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
153 |
aux1 aux2 aux3 aux4) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
154 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
155 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
156 |
lemma inv_d22set_d22set: |
16663 | 157 |
"zprime p ==> inv p ` d22set (p - 2) = d22set (p - 2)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
158 |
apply (rule endo_inj_surj) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
159 |
apply (rule d22set_fin) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
160 |
apply (erule_tac [2] inv_inj) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
161 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
162 |
apply (rule d22set_mem) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
163 |
apply (erule inv_g_1) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
164 |
apply (subgoal_tac [3] "inv p xa < p - 1") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
165 |
apply (erule_tac [4] inv_less_p_minus_1) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
166 |
apply (auto intro: d22set_g_1 d22set_le aux4) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
167 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
168 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
169 |
lemma d22set_d22set_bij: |
16663 | 170 |
"zprime p ==> (d22set (p - 2), d22set (p - 2)) \<in> bijR (reciR p)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
171 |
apply (unfold reciR_def) |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
172 |
apply (rule_tac s = "(d22set (p - 2), inv p ` d22set (p - 2))" in subst) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
173 |
apply (simp add: inv_d22set_d22set) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
174 |
apply (rule inj_func_bijR) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
175 |
apply (rule_tac [3] d22set_fin) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
176 |
apply (erule_tac [2] inv_inj) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
177 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
178 |
apply (erule inv_is_inv) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
179 |
apply (erule_tac [5] inv_g_1) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
180 |
apply (erule_tac [7] inv_less_p_minus_1) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
181 |
apply (auto intro: d22set_g_1 d22set_le aux2 aux3 aux4) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
182 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
183 |
|
16663 | 184 |
lemma reciP_bijP: "zprime p ==> bijP (reciR p) (d22set (p - 2))" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
185 |
apply (unfold reciR_def bijP_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
186 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
187 |
apply (rule d22set_mem) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
188 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
189 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
190 |
|
16663 | 191 |
lemma reciP_uniq: "zprime p ==> uniqP (reciR p)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
192 |
apply (unfold reciR_def uniqP_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
193 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
194 |
apply (rule zcong_zless_imp_eq) |
39159 | 195 |
apply (tactic {* stac (@{thm zcong_cancel2} RS sym) 5 *}) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
196 |
apply (rule_tac [7] zcong_trans) |
39159 | 197 |
apply (tactic {* stac @{thm zcong_sym} 8 *}) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
198 |
apply (rule_tac [6] zless_zprime_imp_zrelprime) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
199 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
200 |
apply (rule zcong_zless_imp_eq) |
39159 | 201 |
apply (tactic {* stac (@{thm zcong_cancel} RS sym) 5 *}) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
202 |
apply (rule_tac [7] zcong_trans) |
39159 | 203 |
apply (tactic {* stac @{thm zcong_sym} 8 *}) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
204 |
apply (rule_tac [6] zless_zprime_imp_zrelprime) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
205 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
206 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
207 |
|
16663 | 208 |
lemma reciP_sym: "zprime p ==> symP (reciR p)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
209 |
apply (unfold reciR_def symP_def) |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
210 |
apply (simp add: mult.commute) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
211 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
212 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
213 |
|
16663 | 214 |
lemma bijER_d22set: "zprime p ==> d22set (p - 2) \<in> bijER (reciR p)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
215 |
apply (rule bijR_bijER) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
216 |
apply (erule d22set_d22set_bij) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
217 |
apply (erule reciP_bijP) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
218 |
apply (erule reciP_uniq) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
219 |
apply (erule reciP_sym) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
220 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
221 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
222 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
223 |
subsection {* Wilson *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
224 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
225 |
lemma bijER_zcong_prod_1: |
16663 | 226 |
"zprime p ==> A \<in> bijER (reciR p) ==> [\<Prod>A = 1] (mod p)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
227 |
apply (unfold reciR_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
228 |
apply (erule bijER.induct) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
229 |
apply (subgoal_tac [2] "a = 1 \<or> a = p - 1") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
230 |
apply (rule_tac [3] zcong_square_zless) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
231 |
apply auto |
57418 | 232 |
apply (subst setprod.insert) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
233 |
prefer 3 |
57418 | 234 |
apply (subst setprod.insert) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
235 |
apply (auto simp add: fin_bijER) |
15392 | 236 |
apply (subgoal_tac "zcong ((a * b) * \<Prod>A) (1 * 1) p") |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
237 |
apply (simp add: mult.assoc) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
238 |
apply (rule zcong_zmult) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
239 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
240 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
241 |
|
16663 | 242 |
theorem Wilson_Bij: "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
|
243 |
apply (subgoal_tac "zcong ((p - 1) * zfact (p - 2)) (-1 * 1) p") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
244 |
apply (rule_tac [2] zcong_zmult) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
245 |
apply (simp add: zprime_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
246 |
apply (subst zfact.simps) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
247 |
apply (rule_tac t = "p - 1 - 1" and s = "p - 2" in subst) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
248 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
249 |
apply (simp add: zcong_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
250 |
apply (subst d22set_prod_zfact [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
251 |
apply (rule bijER_zcong_prod_1) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
252 |
apply (rule_tac [2] bijER_d22set) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
253 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
254 |
done |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
255 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
256 |
end |