equal
deleted
inserted
replaced
341 apply(simp) |
341 apply(simp) |
342 apply(rule allI) |
342 apply(rule allI) |
343 apply(rule list_eq_refl) |
343 apply(rule list_eq_refl) |
344 done |
344 done |
345 |
345 |
346 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))" |
346 lemma ttt3: "(\<lambda>x. ((op @) x (e # []))) = (op #) e" |
347 sorry |
347 sorry |
348 |
348 |
349 |
349 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = INSERT e" |
350 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))" |
350 apply(lifting ttt3) |
351 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *) |
351 apply(regularize) |
352 sorry |
352 apply(auto simp add: cons_rsp) |
|
353 done |
353 |
354 |
354 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))" |
355 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))" |
355 sorry |
356 sorry |
356 |
357 |
357 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))" |
358 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))" |