equal
deleted
inserted
replaced
349 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = INSERT e" |
349 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = INSERT e" |
350 apply(lifting ttt3) |
350 apply(lifting ttt3) |
351 apply(regularize) |
351 apply(regularize) |
352 apply(auto simp add: cons_rsp) |
352 apply(auto simp add: cons_rsp) |
353 done |
353 done |
354 |
|
355 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))" |
354 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))" |
356 sorry |
355 sorry |
357 |
356 |
358 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)))" |
359 apply(lifting hard) |
358 apply(lifting hard) |
360 apply(regularize) |
359 apply(regularize) |
361 apply(auto) |
360 apply(rule fun_rel_id_asm) |
362 sorry |
361 apply(subst babs_simp) |
|
362 apply(tactic {* quotient_tac @{context} 1 *}) |
|
363 apply(rule fun_rel_id_asm) |
|
364 apply(rule impI) |
|
365 apply(rule mp[OF eq_imp_rel[OF fset_equivp]]) |
|
366 apply(drule fun_cong) |
|
367 apply(drule fun_cong) |
|
368 apply(assumption) |
|
369 done |
|
370 |
|
371 |
363 |
372 |
364 end |
373 end |