equal
deleted
inserted
replaced
137 |
137 |
138 lemma inv_inj: "zprime p ==> inj_on (inv p) (d22set (p - 2))" |
138 lemma inv_inj: "zprime p ==> inj_on (inv p) (d22set (p - 2))" |
139 apply (unfold inj_on_def) |
139 apply (unfold inj_on_def) |
140 apply auto |
140 apply auto |
141 apply (rule zcong_zless_imp_eq) |
141 apply (rule zcong_zless_imp_eq) |
142 apply (tactic {* stac (@{thm zcong_cancel} RS sym) 5 *}) |
142 apply (tactic {* stac @{context} (@{thm zcong_cancel} RS sym) 5 *}) |
143 apply (rule_tac [7] zcong_trans) |
143 apply (rule_tac [7] zcong_trans) |
144 apply (tactic {* stac @{thm zcong_sym} 8 *}) |
144 apply (tactic {* stac @{context} @{thm zcong_sym} 8 *}) |
145 apply (erule_tac [7] inv_is_inv) |
145 apply (erule_tac [7] inv_is_inv) |
146 apply (tactic "asm_simp_tac @{context} 9") |
146 apply (tactic "asm_simp_tac @{context} 9") |
147 apply (erule_tac [9] inv_is_inv) |
147 apply (erule_tac [9] inv_is_inv) |
148 apply (rule_tac [6] zless_zprime_imp_zrelprime) |
148 apply (rule_tac [6] zless_zprime_imp_zrelprime) |
149 apply (rule_tac [8] inv_less) |
149 apply (rule_tac [8] inv_less) |
190 |
190 |
191 lemma reciP_uniq: "zprime p ==> uniqP (reciR p)" |
191 lemma reciP_uniq: "zprime p ==> uniqP (reciR p)" |
192 apply (unfold reciR_def uniqP_def) |
192 apply (unfold reciR_def uniqP_def) |
193 apply auto |
193 apply auto |
194 apply (rule zcong_zless_imp_eq) |
194 apply (rule zcong_zless_imp_eq) |
195 apply (tactic {* stac (@{thm zcong_cancel2} RS sym) 5 *}) |
195 apply (tactic {* stac @{context} (@{thm zcong_cancel2} RS sym) 5 *}) |
196 apply (rule_tac [7] zcong_trans) |
196 apply (rule_tac [7] zcong_trans) |
197 apply (tactic {* stac @{thm zcong_sym} 8 *}) |
197 apply (tactic {* stac @{context} @{thm zcong_sym} 8 *}) |
198 apply (rule_tac [6] zless_zprime_imp_zrelprime) |
198 apply (rule_tac [6] zless_zprime_imp_zrelprime) |
199 apply auto |
199 apply auto |
200 apply (rule zcong_zless_imp_eq) |
200 apply (rule zcong_zless_imp_eq) |
201 apply (tactic {* stac (@{thm zcong_cancel} RS sym) 5 *}) |
201 apply (tactic {* stac @{context} (@{thm zcong_cancel} RS sym) 5 *}) |
202 apply (rule_tac [7] zcong_trans) |
202 apply (rule_tac [7] zcong_trans) |
203 apply (tactic {* stac @{thm zcong_sym} 8 *}) |
203 apply (tactic {* stac @{context} @{thm zcong_sym} 8 *}) |
204 apply (rule_tac [6] zless_zprime_imp_zrelprime) |
204 apply (rule_tac [6] zless_zprime_imp_zrelprime) |
205 apply auto |
205 apply auto |
206 done |
206 done |
207 |
207 |
208 lemma reciP_sym: "zprime p ==> symP (reciR p)" |
208 lemma reciP_sym: "zprime p ==> symP (reciR p)" |