445 |
445 |
446 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))" |
446 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))" |
447 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *) |
447 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *) |
448 sorry |
448 sorry |
449 |
449 |
|
450 (* Always safe to apply, but not too helpful *) |
|
451 lemma app_prs2: |
|
452 assumes q1: "Quotient R1 abs1 rep1" |
|
453 and q2: "Quotient R2 abs2 rep2" |
|
454 shows "((abs1 ---> rep2) ((rep1 ---> abs2) f) (rep1 x)) = rep2 (((rep1 ---> abs2) f) x)" |
|
455 unfolding expand_fun_eq |
|
456 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] |
|
457 by simp |
|
458 |
450 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))" |
459 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))" |
451 sorry |
460 sorry |
452 |
461 |
453 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))" |
462 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))" |
454 apply(lifting_setup hard) |
463 apply(lifting_setup hard) |
455 defer |
464 defer |
456 apply(injection) |
465 apply(injection) |
457 apply(subst babs_prs) |
466 apply(subst babs_prs) |
458 defer defer |
467 apply(tactic {* quotient_tac @{context} 1 *}) |
|
468 apply(tactic {* quotient_tac @{context} 1 *}) |
459 apply(subst babs_prs) |
469 apply(subst babs_prs) |
460 defer defer |
470 apply(tactic {* quotient_tac @{context} 1 *}) |
|
471 apply(tactic {* quotient_tac @{context} 1 *}) |
461 apply(subst babs_prs) |
472 apply(subst babs_prs) |
462 defer defer |
473 apply(tactic {* quotient_tac @{context} 1 *}) |
|
474 apply(tactic {* quotient_tac @{context} 1 *}) |
463 apply(subst babs_prs) |
475 apply(subst babs_prs) |
464 defer defer |
476 apply(tactic {* quotient_tac @{context} 1 *}) |
|
477 apply(tactic {* quotient_tac @{context} 1 *}) |
|
478 apply(subst all_prs) |
|
479 apply(tactic {* quotient_tac @{context} 1 *}) |
465 apply(tactic {* lambda_prs_tac @{context} 1 *}) |
480 apply(tactic {* lambda_prs_tac @{context} 1 *}) |
466 (* Until here is ok *) |
481 apply(subst fun_map.simps) |
|
482 apply(tactic {* lambda_prs_tac @{context} 1 *}) |
|
483 apply(subst fun_map.simps) |
|
484 apply(subst fun_map.simps) |
|
485 apply(tactic {* lambda_prs_tac @{context} 1 *}) |
467 apply(cleaning) |
486 apply(cleaning) |
468 sorry |
487 sorry |
469 |
488 |
470 |
|
471 end |
489 end |