equal
deleted
inserted
replaced
360 apply(regularize) |
360 apply(regularize) |
361 apply(auto simp add: cons_rsp) |
361 apply(auto simp add: cons_rsp) |
362 done |
362 done |
363 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))" |
363 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))" |
364 sorry |
364 sorry |
|
365 |
|
366 lemma eq_imp_rel: |
|
367 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
|
368 by (simp add: equivp_reflp) |
|
369 |
365 |
370 |
366 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))" |
371 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))" |
367 apply(lifting hard) |
372 apply(lifting hard) |
368 apply(regularize) |
373 apply(regularize) |
369 apply(rule fun_rel_id_asm) |
374 apply(rule fun_rel_id_asm) |