720 ML {* |
720 ML {* |
721 fun stripped_term_of ct = |
721 fun stripped_term_of ct = |
722 ct |> term_of |> HOLogic.dest_Trueprop |
722 ct |> term_of |> HOLogic.dest_Trueprop |
723 *} |
723 *} |
724 |
724 |
|
725 (* TODO: check if it still works with first_order_match *) |
725 ML {* |
726 ML {* |
726 fun instantiate_tac thm = |
727 fun instantiate_tac thm = |
727 Subgoal.FOCUS (fn {concl, ...} => |
728 Subgoal.FOCUS (fn {concl, ...} => |
728 let |
729 let |
729 val pat = Drule.strip_imp_concl (cprop_of thm) |
730 val pat = Drule.strip_imp_concl (cprop_of thm) |
845 and QT_appR: "QUOT_TRUE (A B) \<Longrightarrow> QUOT_TRUE B" |
846 and QT_appR: "QUOT_TRUE (A B) \<Longrightarrow> QUOT_TRUE B" |
846 and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))" |
847 and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))" |
847 apply(simp_all add: QUOT_TRUE_def) |
848 apply(simp_all add: QUOT_TRUE_def) |
848 done |
849 done |
849 |
850 |
|
851 lemma QUOT_TRUE_i: "(QUOT_TRUE a \<Longrightarrow> P) \<Longrightarrow> P" |
|
852 by (simp add: QUOT_TRUE_def) |
|
853 |
|
854 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<Longrightarrow> QUOT_TRUE b" |
|
855 by (simp add: QUOT_TRUE_def) |
|
856 |
|
857 ML {* |
|
858 fun quot_true_tac ctxt fnctn = |
|
859 SUBGOAL (fn (gl, _) => |
|
860 let |
|
861 val thy = ProofContext.theory_of ctxt; |
|
862 fun find_fun trm = |
|
863 case trm of |
|
864 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true |
|
865 | _ => false |
|
866 in |
|
867 case find_first find_fun (Logic.strip_imp_prems gl) of |
|
868 SOME (_ $ (_ $ x)) => |
|
869 let |
|
870 val fx = fnctn x; |
|
871 val ctrm1 = cterm_of thy x; |
|
872 val cty1 = ctyp_of thy (fastype_of x); |
|
873 val ctrm2 = cterm_of thy fx; |
|
874 val cty2 = ctyp_of thy (fastype_of fx); |
|
875 val thm = Drule.instantiate' [SOME cty1, SOME cty2] [SOME ctrm1, SOME ctrm2] @{thm QUOT_TRUE_imp} |
|
876 in |
|
877 dtac thm 1 |
|
878 end |
|
879 | NONE => error "quot_true_tac!" |
|
880 | _ => error "quot_true_tac!!" |
|
881 end) |
|
882 *} |
850 |
883 |
851 ML {* |
884 ML {* |
852 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
885 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
853 (FIRST' [ |
886 (FIRST' [ |
854 (* "cong" rule of the of the relation / transitivity*) |
887 (* "cong" rule of the of the relation / transitivity*) |