equal
deleted
inserted
replaced
268 "zcong (a * inv p a * (\<Prod>x\<in> wset(a - 1, p). x)) (1 * 1) p") |
268 "zcong (a * inv p a * (\<Prod>x\<in> wset(a - 1, p). x)) (1 * 1) p") |
269 prefer 5 |
269 prefer 5 |
270 apply (simp add: zmult_assoc) |
270 apply (simp add: zmult_assoc) |
271 apply (rule_tac [5] zcong_zmult) |
271 apply (rule_tac [5] zcong_zmult) |
272 apply (rule_tac [5] inv_is_inv) |
272 apply (rule_tac [5] inv_is_inv) |
273 apply (tactic "Clarify_tac 4") |
273 apply (tactic "clarify_tac @{claset} 4") |
274 apply (subgoal_tac [4] "a \<in> wset (a - 1, p)") |
274 apply (subgoal_tac [4] "a \<in> wset (a - 1, p)") |
275 apply (rule_tac [5] wset_inv_mem_mem) |
275 apply (rule_tac [5] wset_inv_mem_mem) |
276 apply (simp_all add: wset_fin) |
276 apply (simp_all add: wset_fin) |
277 apply (rule inv_distinct, auto) |
277 apply (rule inv_distinct, auto) |
278 done |
278 done |