equal
deleted
inserted
replaced
249 5 \<le> p --> a < p - 1 --> [(\<Prod>x\<in>wset a p. x) = 1] (mod p)" |
249 5 \<le> p --> a < p - 1 --> [(\<Prod>x\<in>wset a p. x) = 1] (mod p)" |
250 apply (induct a p rule: wset_induct) |
250 apply (induct a p rule: wset_induct) |
251 prefer 2 |
251 prefer 2 |
252 apply (subst wset.simps) |
252 apply (subst wset.simps) |
253 apply (auto, unfold Let_def, auto) |
253 apply (auto, unfold Let_def, auto) |
254 apply (subst setprod_insert) |
254 apply (subst setprod.insert) |
255 apply (tactic {* stac @{thm setprod_insert} 3 *}) |
255 apply (tactic {* stac @{thm setprod.insert} 3 *}) |
256 apply (subgoal_tac [5] |
256 apply (subgoal_tac [5] |
257 "zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p") |
257 "zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p") |
258 prefer 5 |
258 prefer 5 |
259 apply (simp add: mult_assoc) |
259 apply (simp add: mult_assoc) |
260 apply (rule_tac [5] zcong_zmult) |
260 apply (rule_tac [5] zcong_zmult) |