557 definition |
557 definition |
558 "QUOT_TRUE x \<equiv> True" |
558 "QUOT_TRUE x \<equiv> True" |
559 |
559 |
560 ML {* |
560 ML {* |
561 fun find_qt_asm asms = |
561 fun find_qt_asm asms = |
562 let |
562 let |
563 fun find_fun trm = |
563 fun find_fun trm = |
564 case trm of |
564 case trm of |
565 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true |
565 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true |
566 | _ => false |
566 | _ => false |
567 in |
567 in |
568 case find_first find_fun asms of |
568 case find_first find_fun asms of |
569 SOME (_ $ (_ $ (f $ a))) => (f, a) |
569 SOME (_ $ (_ $ (f $ a))) => SOME (f, a) |
570 | SOME _ => error "find_qt_asm: no pair" |
570 | _ => NONE |
571 | NONE => error "find_qt_asm: no assumption" |
571 end |
572 end |
572 *} |
573 *} |
573 |
574 |
574 text {* |
575 (* |
|
576 To prove that the regularised theorem implies the abs/rep injected, |
575 To prove that the regularised theorem implies the abs/rep injected, |
577 we try: |
576 we try: |
578 |
577 |
579 1) theorems 'trans2' from the appropriate QUOT_TYPE |
578 1) theorems 'trans2' from the appropriate QUOT_TYPE |
580 2) remove lambdas from both sides: lambda_rsp_tac |
579 2) remove lambdas from both sides: lambda_rsp_tac |
590 (Lambdas under respects may have left us some assumptions) |
589 (Lambdas under respects may have left us some assumptions) |
591 C) proving obvious higher order equalities by simplifying fun_rel |
590 C) proving obvious higher order equalities by simplifying fun_rel |
592 (not sure if it is still needed?) |
591 (not sure if it is still needed?) |
593 D) unfolding lambda on one side |
592 D) unfolding lambda on one side |
594 E) simplifying (= ===> =) for simpler respectfulness |
593 E) simplifying (= ===> =) for simpler respectfulness |
595 |
594 *} |
596 *) |
|
597 |
595 |
598 lemma quot_true_dests: |
596 lemma quot_true_dests: |
599 shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" |
597 shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" |
600 and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P" |
598 and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P" |
601 and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))" |
599 and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))" |
659 |
657 |
660 ML {* |
658 ML {* |
661 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
659 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
662 *} |
660 *} |
663 |
661 |
664 thm apply_rsp |
662 ML {* |
665 |
663 (* FIXME / TODO: what is asmf and asma in the code below *) |
666 ML {* |
664 |
667 val apply_rsp_tac = |
665 val apply_rsp_tac = |
668 Subgoal.FOCUS (fn {concl, asms, context,...} => |
666 Subgoal.FOCUS (fn {concl, asms, context,...} => |
669 case (HOLogic.dest_Trueprop (term_of concl)) of |
667 let |
670 (R2 $ (f $ x) $ (g $ y)) => |
668 val bare_concl = HOLogic.dest_Trueprop (term_of concl) |
671 (let |
669 val qt_asm = find_qt_asm (map term_of asms) |
672 val (asmf, asma) = find_qt_asm (map term_of asms) |
670 in |
673 in |
671 case (bare_concl, qt_asm) of |
674 if (fastype_of asmf) = (fastype_of f) |
672 (R2 $ (f $ x) $ (g $ y), SOME (asmf, asma)) => |
675 then no_tac |
673 if (fastype_of asmf) = (fastype_of f) |
676 else |
674 then no_tac |
677 let |
675 else |
678 val ty_a = fastype_of x |
676 let |
679 val ty_b = fastype_of asma |
677 val ty_x = fastype_of x |
680 val ty_c = range_type (fastype_of f) |
678 val ty_b = fastype_of asma |
681 val thy = ProofContext.theory_of context |
679 val ty_f = range_type (fastype_of f) |
682 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c] |
680 val thy = ProofContext.theory_of context |
683 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
681 val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f] |
684 val thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} |
682 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
685 in |
683 val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} |
686 (rtac thm THEN' quotient_tac context) 1 |
684 in |
687 end |
685 (rtac inst_thm THEN' quotient_tac context) 1 |
688 end |
686 end |
689 handle ERROR "find_qt_asm: no pair" => no_tac) |
687 | _ => no_tac |
690 | _ => no_tac) |
688 end) |
691 *} |
689 *} |
692 |
690 |
693 ML {* |
691 ML {* |
694 fun equals_rsp_tac R ctxt = |
692 fun equals_rsp_tac R ctxt = |
695 let |
693 let |