equal
deleted
inserted
replaced
30 in (if a \<in> ws then ws else insert a (insert (inv p a) ws)) else {})" |
30 in (if a \<in> ws then ws else insert a (insert (inv p a) ws)) else {})" |
31 |
31 |
32 |
32 |
33 text {* \medskip @{term [source] inv} *} |
33 text {* \medskip @{term [source] inv} *} |
34 |
34 |
35 lemma aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)" |
35 lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)" |
36 apply (subst int_int_eq [symmetric]) |
36 apply (subst int_int_eq [symmetric]) |
37 apply auto |
37 apply auto |
38 done |
38 done |
39 |
39 |
40 lemma inv_is_inv: |
40 lemma inv_is_inv: |
42 apply (unfold inv_def) |
42 apply (unfold inv_def) |
43 apply (subst zcong_zmod) |
43 apply (subst zcong_zmod) |
44 apply (subst zmod_zmult1_eq [symmetric]) |
44 apply (subst zmod_zmult1_eq [symmetric]) |
45 apply (subst zcong_zmod [symmetric]) |
45 apply (subst zcong_zmod [symmetric]) |
46 apply (subst power_Suc [symmetric]) |
46 apply (subst power_Suc [symmetric]) |
47 apply (subst aux) |
47 apply (subst inv_is_inv_aux) |
48 apply (erule_tac [2] Little_Fermat) |
48 apply (erule_tac [2] Little_Fermat) |
49 apply (erule_tac [2] zdvd_not_zless) |
49 apply (erule_tac [2] zdvd_not_zless) |
50 apply (unfold zprime_def) |
50 apply (unfold zprime_def) |
51 apply auto |
51 apply auto |
52 done |
52 done |
87 apply (subgoal_tac "a = 1") |
87 apply (subgoal_tac "a = 1") |
88 apply (rule_tac [2] zcong_zless_imp_eq) |
88 apply (rule_tac [2] zcong_zless_imp_eq) |
89 apply auto |
89 apply auto |
90 done |
90 done |
91 |
91 |
92 lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)" |
92 lemma inv_not_p_minus_1_aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)" |
93 apply (unfold zcong_def) |
93 apply (unfold zcong_def) |
94 apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2) |
94 apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2) |
95 apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) |
95 apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) |
96 apply (simp add: zmult_commute zminus_zdiff_eq) |
96 apply (simp add: zmult_commute zminus_zdiff_eq) |
97 apply (subst zdvd_zminus_iff) |
97 apply (subst zdvd_zminus_iff) |
104 lemma inv_not_p_minus_1: |
104 lemma inv_not_p_minus_1: |
105 "p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> p - 1" |
105 "p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> p - 1" |
106 apply safe |
106 apply safe |
107 apply (cut_tac a = a and p = p in inv_is_inv) |
107 apply (cut_tac a = a and p = p in inv_is_inv) |
108 apply auto |
108 apply auto |
109 apply (simp add: aux) |
109 apply (simp add: inv_not_p_minus_1_aux) |
110 apply (subgoal_tac "a = p - 1") |
110 apply (subgoal_tac "a = p - 1") |
111 apply (rule_tac [2] zcong_zless_imp_eq) |
111 apply (rule_tac [2] zcong_zless_imp_eq) |
112 apply auto |
112 apply auto |
113 done |
113 done |
114 |
114 |
135 apply auto |
135 apply auto |
136 apply (unfold inv_def zprime_def) |
136 apply (unfold inv_def zprime_def) |
137 apply (simp add: pos_mod_bound) |
137 apply (simp add: pos_mod_bound) |
138 done |
138 done |
139 |
139 |
140 lemma aux: "5 \<le> p ==> |
140 lemma inv_inv_aux: "5 \<le> p ==> |
141 nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))" |
141 nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))" |
142 apply (subst int_int_eq [symmetric]) |
142 apply (subst int_int_eq [symmetric]) |
143 apply (simp add: zmult_int [symmetric]) |
143 apply (simp add: zmult_int [symmetric]) |
144 apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2) |
144 apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2) |
145 done |
145 done |
161 apply (rule zcong_zless_imp_eq) |
161 apply (rule zcong_zless_imp_eq) |
162 prefer 5 |
162 prefer 5 |
163 apply (subst zcong_zmod) |
163 apply (subst zcong_zmod) |
164 apply (subst mod_mod_trivial) |
164 apply (subst mod_mod_trivial) |
165 apply (subst zcong_zmod [symmetric]) |
165 apply (subst zcong_zmod [symmetric]) |
166 apply (subst aux) |
166 apply (subst inv_inv_aux) |
167 apply (subgoal_tac [2] |
167 apply (subgoal_tac [2] |
168 "zcong (a * a^(nat (p - 1) * nat (p - 3))) (a * 1) p") |
168 "zcong (a * a^(nat (p - 1) * nat (p - 3))) (a * 1) p") |
169 apply (rule_tac [3] zcong_zmult) |
169 apply (rule_tac [3] zcong_zmult) |
170 apply (rule_tac [4] zcong_zpower_zmult) |
170 apply (rule_tac [4] zcong_zpower_zmult) |
171 apply (erule_tac [4] Little_Fermat) |
171 apply (erule_tac [4] Little_Fermat) |