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