45 lemmas inv_less = inv_correct [THEN conjunct2, THEN conjunct1] |
45 lemmas inv_less = inv_correct [THEN conjunct2, THEN conjunct1] |
46 lemmas inv_is_inv = inv_correct [THEN conjunct2, THEN conjunct2] |
46 lemmas inv_is_inv = inv_correct [THEN conjunct2, THEN conjunct2] |
47 |
47 |
48 lemma inv_not_0: |
48 lemma inv_not_0: |
49 "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 0" |
49 "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 0" |
50 -- \<open>same as @{text WilsonRuss}\<close> |
50 \<comment> \<open>same as \<open>WilsonRuss\<close>\<close> |
51 apply safe |
51 apply safe |
52 apply (cut_tac a = a and p = p in inv_is_inv) |
52 apply (cut_tac a = a and p = p in inv_is_inv) |
53 apply (unfold zcong_def) |
53 apply (unfold zcong_def) |
54 apply auto |
54 apply auto |
55 done |
55 done |
56 |
56 |
57 lemma inv_not_1: |
57 lemma inv_not_1: |
58 "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 1" |
58 "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 1" |
59 -- \<open>same as @{text WilsonRuss}\<close> |
59 \<comment> \<open>same as \<open>WilsonRuss\<close>\<close> |
60 apply safe |
60 apply safe |
61 apply (cut_tac a = a and p = p in inv_is_inv) |
61 apply (cut_tac a = a and p = p in inv_is_inv) |
62 prefer 4 |
62 prefer 4 |
63 apply simp |
63 apply simp |
64 apply (subgoal_tac "a = 1") |
64 apply (subgoal_tac "a = 1") |
65 apply (rule_tac [2] zcong_zless_imp_eq) |
65 apply (rule_tac [2] zcong_zless_imp_eq) |
66 apply auto |
66 apply auto |
67 done |
67 done |
68 |
68 |
69 lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)" |
69 lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)" |
70 -- \<open>same as @{text WilsonRuss}\<close> |
70 \<comment> \<open>same as \<open>WilsonRuss\<close>\<close> |
71 apply (unfold zcong_def) |
71 apply (unfold zcong_def) |
72 apply (simp add: diff_diff_eq diff_diff_eq2 right_diff_distrib) |
72 apply (simp add: diff_diff_eq diff_diff_eq2 right_diff_distrib) |
73 apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) |
73 apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) |
74 apply (simp add: algebra_simps) |
74 apply (simp add: algebra_simps) |
75 apply (subst dvd_minus_iff) |
75 apply (subst dvd_minus_iff) |
79 apply auto |
79 apply auto |
80 done |
80 done |
81 |
81 |
82 lemma inv_not_p_minus_1: |
82 lemma inv_not_p_minus_1: |
83 "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> p - 1" |
83 "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> p - 1" |
84 -- \<open>same as @{text WilsonRuss}\<close> |
84 \<comment> \<open>same as \<open>WilsonRuss\<close>\<close> |
85 apply safe |
85 apply safe |
86 apply (cut_tac a = a and p = p in inv_is_inv) |
86 apply (cut_tac a = a and p = p in inv_is_inv) |
87 apply auto |
87 apply auto |
88 apply (simp add: aux) |
88 apply (simp add: aux) |
89 apply (subgoal_tac "a = p - 1") |
89 apply (subgoal_tac "a = p - 1") |
91 apply auto |
91 apply auto |
92 done |
92 done |
93 |
93 |
94 text \<open> |
94 text \<open> |
95 Below is slightly different as we don't expand @{term [source] inv} |
95 Below is slightly different as we don't expand @{term [source] inv} |
96 but use ``@{text correct}'' theorems. |
96 but use ``\<open>correct\<close>'' theorems. |
97 \<close> |
97 \<close> |
98 |
98 |
99 lemma inv_g_1: "zprime p ==> 1 < a ==> a < p - 1 ==> 1 < inv p a" |
99 lemma inv_g_1: "zprime p ==> 1 < a ==> a < p - 1 ==> 1 < inv p a" |
100 apply (subgoal_tac "inv p a \<noteq> 1") |
100 apply (subgoal_tac "inv p a \<noteq> 1") |
101 apply (subgoal_tac "inv p a \<noteq> 0") |
101 apply (subgoal_tac "inv p a \<noteq> 0") |
109 apply auto |
109 apply auto |
110 done |
110 done |
111 |
111 |
112 lemma inv_less_p_minus_1: |
112 lemma inv_less_p_minus_1: |
113 "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a < p - 1" |
113 "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a < p - 1" |
114 -- \<open>ditto\<close> |
114 \<comment> \<open>ditto\<close> |
115 apply (subst order_less_le) |
115 apply (subst order_less_le) |
116 apply (simp add: inv_not_p_minus_1 inv_less) |
116 apply (simp add: inv_not_p_minus_1 inv_less) |
117 done |
117 done |
118 |
118 |
119 |
119 |