equal
deleted
inserted
replaced
442 |
442 |
443 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))" |
443 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))" |
444 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *) |
444 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *) |
445 sorry |
445 sorry |
446 |
446 |
|
447 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))" |
|
448 sorry |
|
449 |
|
450 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))" |
|
451 apply(lifting_setup hard) |
|
452 defer |
|
453 apply(injection) |
|
454 apply(subst babs_prs) |
|
455 defer defer |
|
456 apply(subst babs_prs) |
|
457 defer defer |
|
458 apply(subst babs_prs) |
|
459 defer defer |
|
460 apply(subst babs_prs) |
|
461 defer defer |
|
462 apply(tactic {* lambda_prs_tac @{context} 1 *}) |
|
463 (* Until here is ok *) |
|
464 apply(cleaning) |
447 end |
465 end |