author | wenzelm |
Sun, 04 Feb 2001 19:31:13 +0100 | |
changeset 11049 | 7eef34adb852 |
parent 9508 | 4d01dbf6ded7 |
child 11549 | e7265e70fd7c |
permissions | -rw-r--r-- |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
1 |
(* Title: HOL/NumberTheory/WilsonRuss.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:
9508
diff
changeset
|
3 |
Author: Thomas M. Rasmussen |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
4 |
Copyright 2000 University of Cambridge |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
5 |
*) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
6 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
7 |
header {* Wilson's Theorem according to Russinoff *} |
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 |
theory WilsonRuss = EulerFermat: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
10 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
11 |
text {* |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
12 |
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
|
13 |
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
|
14 |
*} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
15 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
16 |
subsection {* Definitions and lemmas *} |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
17 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
18 |
consts |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
19 |
inv :: "int => int => int" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
20 |
wset :: "int * int => int set" |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
21 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
22 |
defs |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
23 |
inv_def: "inv p a == (a^(nat (p - #2))) mod p" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
24 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
25 |
recdef wset |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
26 |
"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
|
27 |
"wset (a, p) = |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
28 |
(if #1 < a then |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
29 |
let ws = wset (a - #1, p) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
30 |
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
|
31 |
|
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 |
text {* \medskip @{term [source] inv} *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
34 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
35 |
lemma aux: "#1 < m ==> Suc (nat (m - #2)) = nat (m - #1)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
36 |
apply (subst int_int_eq [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
37 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
38 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
39 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
40 |
lemma inv_is_inv: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
41 |
"p \<in> zprime \<Longrightarrow> #0 < a \<Longrightarrow> a < p ==> [a * inv p a = #1] (mod p)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
42 |
apply (unfold inv_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
43 |
apply (subst zcong_zmod) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
44 |
apply (subst zmod_zmult1_eq [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
45 |
apply (subst zcong_zmod [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
46 |
apply (subst power_Suc [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
47 |
apply (subst aux) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
48 |
apply (erule_tac [2] Little_Fermat) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
49 |
apply (erule_tac [2] zdvd_not_zless) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
50 |
apply (unfold zprime_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
51 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
52 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
53 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
54 |
lemma inv_distinct: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
55 |
"p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> a \<noteq> inv p a" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
56 |
apply safe |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
57 |
apply (cut_tac a = a and p = p in zcong_square) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
58 |
apply (cut_tac [3] 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
|
59 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
60 |
apply (subgoal_tac "a = #1") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
61 |
apply (rule_tac [2] m = p in zcong_zless_imp_eq) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
62 |
apply (subgoal_tac [7] "a = p - #1") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
63 |
apply (rule_tac [8] m = p in zcong_zless_imp_eq) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
64 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
65 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
66 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
67 |
lemma inv_not_0: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
68 |
"p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> inv p a \<noteq> #0" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
69 |
apply safe |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
70 |
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
|
71 |
apply (unfold zcong_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
72 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
73 |
apply (subgoal_tac "\<not> p dvd #1") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
74 |
apply (rule_tac [2] zdvd_not_zless) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
75 |
apply (subgoal_tac "p dvd #1") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
76 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
77 |
apply (subst zdvd_zminus_iff [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
78 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
79 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
80 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
81 |
lemma inv_not_1: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
82 |
"p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> inv p a \<noteq> #1" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
83 |
apply safe |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
84 |
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
|
85 |
prefer 4 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
86 |
apply simp |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
87 |
apply (subgoal_tac "a = #1") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
88 |
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
|
89 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
90 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
91 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
92 |
lemma aux: "[a * (p - #1) = #1] (mod p) = [a = p - #1] (mod p)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
93 |
apply (unfold zcong_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
94 |
apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
95 |
apply (rule_tac s = "p dvd -((a + #1) + (p * -a))" in trans) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
96 |
apply (simp add: zmult_commute zminus_zdiff_eq) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
97 |
apply (subst zdvd_zminus_iff) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
98 |
apply (subst zdvd_reduce) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
99 |
apply (rule_tac s = "p dvd (a + #1) + (p * -#1)" in trans) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
100 |
apply (subst zdvd_reduce) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
101 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
102 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
103 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
104 |
lemma inv_not_p_minus_1: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
105 |
"p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> inv p a \<noteq> p - #1" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
106 |
apply safe |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
107 |
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
|
108 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
109 |
apply (simp add: aux) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
110 |
apply (subgoal_tac "a = p - #1") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
111 |
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
|
112 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
113 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
114 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
115 |
lemma inv_g_1: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
116 |
"p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> #1 < inv p a" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
117 |
apply (case_tac "#0\<le> inv p a") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
118 |
apply (subgoal_tac "inv p a \<noteq> #1") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
119 |
apply (subgoal_tac "inv p a \<noteq> #0") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
120 |
apply (subst order_less_le) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
121 |
apply (subst zle_add1_eq_le [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
122 |
apply (subst order_less_le) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
123 |
apply (rule_tac [2] inv_not_0) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
124 |
apply (rule_tac [5] inv_not_1) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
125 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
126 |
apply (unfold inv_def zprime_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
127 |
apply (simp add: pos_mod_sign) |
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 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
130 |
lemma inv_less_p_minus_1: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
131 |
"p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> inv p a < p - #1" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
132 |
apply (case_tac "inv p a < p") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
133 |
apply (subst order_less_le) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
134 |
apply (simp add: inv_not_p_minus_1) |
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 |
apply (unfold inv_def zprime_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
137 |
apply (simp add: pos_mod_bound) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
138 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
139 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
140 |
lemma aux: "#5 \<le> p ==> |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
141 |
nat (p - #2) * nat (p - #2) = Suc (nat (p - #1) * nat (p - #3))" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
142 |
apply (subst int_int_eq [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
143 |
apply (simp add: zmult_int [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
144 |
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
|
145 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
146 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
147 |
lemma zcong_zpower_zmult: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
148 |
"[x^y = #1] (mod p) \<Longrightarrow> [x^(y * z) = #1] (mod p)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
149 |
apply (induct z) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
150 |
apply (auto simp add: zpower_zadd_distrib) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
151 |
apply (subgoal_tac "zcong (x^y * x^(y * n)) (#1 * #1) p") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
152 |
apply (rule_tac [2] zcong_zmult) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
153 |
apply simp_all |
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_inv: "p \<in> zprime \<Longrightarrow> |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
157 |
#5 \<le> p \<Longrightarrow> #0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
158 |
apply (unfold inv_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
159 |
apply (subst zpower_zmod) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
160 |
apply (subst zpower_zpower) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
161 |
apply (rule zcong_zless_imp_eq) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
162 |
prefer 5 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
163 |
apply (subst zcong_zmod) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
164 |
apply (subst mod_mod_trivial) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
165 |
apply (subst zcong_zmod [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
166 |
apply (subst aux) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
167 |
apply (subgoal_tac [2] |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
168 |
"zcong (a * a^(nat (p - #1) * nat (p - #3))) (a * #1) p") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
169 |
apply (rule_tac [3] zcong_zmult) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
170 |
apply (rule_tac [4] zcong_zpower_zmult) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
171 |
apply (erule_tac [4] Little_Fermat) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
172 |
apply (rule_tac [4] zdvd_not_zless) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
173 |
apply (simp_all add: pos_mod_bound pos_mod_sign) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
174 |
done |
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 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
177 |
text {* \medskip @{term wset} *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
178 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
179 |
declare wset.simps [simp del] |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
180 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
181 |
lemma wset_induct: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
182 |
"(!!a p. P {} a p) \<Longrightarrow> |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
183 |
(!!a p. #1 < (a::int) \<Longrightarrow> P (wset (a - #1, p)) (a - #1) p |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
184 |
==> P (wset (a, p)) a p) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
185 |
==> P (wset (u, v)) u v" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
186 |
proof - |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
187 |
case antecedent |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
188 |
show ?thesis |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
189 |
apply (rule wset.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
190 |
apply safe |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
191 |
apply (case_tac [2] "#1 < a") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
192 |
apply (rule_tac [2] antecedent) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
193 |
apply simp_all |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
194 |
apply (simp_all add: wset.simps antecedent) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
195 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
196 |
qed |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
197 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
198 |
lemma wset_mem_imp_or [rule_format]: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
199 |
"#1 < a \<Longrightarrow> b \<notin> wset (a - #1, p) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
200 |
==> 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
|
201 |
apply (subst wset.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
202 |
apply (unfold Let_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
203 |
apply simp |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
204 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
205 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
206 |
lemma wset_mem_mem [simp]: "#1 < a ==> a \<in> wset (a, p)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
207 |
apply (subst wset.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
208 |
apply (unfold Let_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
209 |
apply simp |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
210 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
211 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
212 |
lemma wset_subset: "#1 < a \<Longrightarrow> b \<in> wset (a - #1, p) ==> b \<in> wset (a, p)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
213 |
apply (subst wset.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
214 |
apply (unfold Let_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
215 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
216 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
217 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
218 |
lemma wset_g_1 [rule_format]: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
219 |
"p \<in> zprime --> a < p - #1 --> b \<in> wset (a, p) --> #1 < b" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
220 |
apply (induct a p rule: wset_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
221 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
222 |
apply (case_tac "b = a") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
223 |
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
|
224 |
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
|
225 |
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
|
226 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
227 |
apply simp |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
228 |
apply (rule inv_g_1) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
229 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
230 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
231 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
232 |
lemma wset_less [rule_format]: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
233 |
"p \<in> zprime --> a < p - #1 --> b \<in> wset (a, p) --> b < p - #1" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
234 |
apply (induct a p rule: wset_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
235 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
236 |
apply (case_tac "b = a") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
237 |
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
|
238 |
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
|
239 |
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
|
240 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
241 |
apply simp |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
242 |
apply (rule inv_less_p_minus_1) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
243 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
244 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
245 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
246 |
lemma wset_mem [rule_format]: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
247 |
"p \<in> zprime --> |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
248 |
a < p - #1 --> #1 < b --> b \<le> a --> b \<in> wset (a, p)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
249 |
apply (induct a p rule: wset.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
250 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
251 |
apply (subgoal_tac "b = a") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
252 |
apply (rule_tac [2] zle_anti_sym) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
253 |
apply (rule_tac [4] wset_subset) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
254 |
apply (simp (no_asm_simp)) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
255 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
256 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
257 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
258 |
lemma wset_mem_inv_mem [rule_format]: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
259 |
"p \<in> zprime --> #5 \<le> p --> a < p - #1 --> b \<in> wset (a, p) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
260 |
--> inv p b \<in> wset (a, p)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
261 |
apply (induct a p rule: wset_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
262 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
263 |
apply (case_tac "b = a") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
264 |
apply (subst wset.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
265 |
apply (unfold Let_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
266 |
apply (rule_tac [3] wset_subset) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
267 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
268 |
apply (case_tac "b = inv p a") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
269 |
apply (simp (no_asm_simp)) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
270 |
apply (subst inv_inv) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
271 |
apply (subgoal_tac [6] "b = a \<or> b = inv p a") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
272 |
apply (rule_tac [7] wset_mem_imp_or) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
273 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
274 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
275 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
276 |
lemma wset_inv_mem_mem: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
277 |
"p \<in> zprime \<Longrightarrow> #5 \<le> p \<Longrightarrow> a < p - #1 \<Longrightarrow> #1 < b \<Longrightarrow> b < p - #1 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
278 |
\<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
|
279 |
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
|
280 |
apply (rule_tac [2] wset_mem_inv_mem) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
281 |
apply (rule inv_inv) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
282 |
apply simp_all |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
283 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
284 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
285 |
lemma wset_fin: "finite (wset (a, p))" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
286 |
apply (induct a p rule: wset_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
287 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
288 |
apply (subst wset.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
289 |
apply (unfold Let_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
290 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
291 |
done |
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 |
lemma wset_zcong_prod_1 [rule_format]: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
294 |
"p \<in> zprime --> |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
295 |
#5 \<le> p --> a < p - #1 --> [setprod (wset (a, p)) = #1] (mod p)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
296 |
apply (induct a p rule: wset_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
297 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
298 |
apply (subst wset.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
299 |
apply (unfold Let_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
300 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
301 |
apply (subst setprod_insert) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
302 |
apply (tactic {* stac (thm "setprod_insert") 3 *}) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
303 |
apply (subgoal_tac [5] |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
304 |
"zcong (a * inv p a * setprod (wset (a - #1, p))) (#1 * #1) p") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
305 |
prefer 5 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
306 |
apply (simp add: zmult_assoc) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
307 |
apply (rule_tac [5] zcong_zmult) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
308 |
apply (rule_tac [5] inv_is_inv) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
309 |
apply (tactic "Clarify_tac 4") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
310 |
apply (subgoal_tac [4] "a \<in> wset (a - #1, p)") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
311 |
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
|
312 |
apply (simp_all add: wset_fin) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
313 |
apply (rule inv_distinct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
314 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
315 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
316 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
317 |
lemma d22set_eq_wset: "p \<in> zprime ==> d22set (p - #2) = wset (p - #2, p)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
318 |
apply safe |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
319 |
apply (erule wset_mem) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
320 |
apply (rule_tac [2] d22set_g_1) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
321 |
apply (rule_tac [3] d22set_le) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
322 |
apply (rule_tac [4] d22set_mem) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
323 |
apply (erule_tac [4] wset_g_1) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
324 |
prefer 6 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
325 |
apply (subst zle_add1_eq_le [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
326 |
apply (subgoal_tac "p - #2 + #1 = p - #1") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
327 |
apply (simp (no_asm_simp)) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
328 |
apply (erule wset_less) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
329 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
330 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
331 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
332 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
333 |
subsection {* Wilson *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
334 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
335 |
lemma prime_g_5: "p \<in> zprime \<Longrightarrow> p \<noteq> #2 \<Longrightarrow> p \<noteq> #3 ==> #5 \<le> p" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
336 |
apply (unfold zprime_def dvd_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
337 |
apply (case_tac "p = #4") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
338 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
339 |
apply (rule notE) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
340 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
341 |
apply assumption |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
342 |
apply (simp (no_asm)) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
343 |
apply (rule_tac x = "#2" in exI) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
344 |
apply safe |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
345 |
apply (rule_tac x = "#2" in exI) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
346 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
347 |
apply arith |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
348 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
349 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
350 |
theorem Wilson_Russ: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
351 |
"p \<in> zprime ==> [zfact (p - #1) = #-1] (mod p)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
352 |
apply (subgoal_tac "[(p - #1) * zfact (p - #2) = #-1 * #1] (mod p)") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
353 |
apply (rule_tac [2] zcong_zmult) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
354 |
apply (simp only: zprime_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
355 |
apply (subst zfact.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
356 |
apply (rule_tac t = "p - #1 - #1" and s = "p - #2" in subst) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
357 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
358 |
apply (simp only: zcong_def) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
359 |
apply (simp (no_asm_simp)) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
360 |
apply (case_tac "p = #2") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
361 |
apply (simp add: zfact.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
362 |
apply (case_tac "p = #3") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
363 |
apply (simp add: zfact.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
364 |
apply (subgoal_tac "#5 \<le> p") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
365 |
apply (erule_tac [2] prime_g_5) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
366 |
apply (subst d22set_prod_zfact [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
367 |
apply (subst d22set_eq_wset) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
368 |
apply (rule_tac [2] wset_zcong_prod_1) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
369 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
370 |
done |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
371 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
372 |
end |