equal
deleted
inserted
replaced
357 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))" |
357 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))" |
358 apply(lifting hard) |
358 apply(lifting hard) |
359 apply(regularize) |
359 apply(regularize) |
360 apply(rule fun_rel_id_asm) |
360 apply(rule fun_rel_id_asm) |
361 apply(subst babs_simp) |
361 apply(subst babs_simp) |
362 apply(tactic {* quotient_tac @{context} 1 *}) |
362 apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
363 apply(rule fun_rel_id_asm) |
363 apply(rule fun_rel_id_asm) |
364 apply(rule impI) |
364 apply(rule impI) |
365 apply(rule mp[OF eq_imp_rel[OF fset_equivp]]) |
365 apply(rule mp[OF eq_imp_rel[OF fset_equivp]]) |
366 apply(drule fun_cong) |
366 apply(drule fun_cong) |
367 apply(drule fun_cong) |
367 apply(drule fun_cong) |