diff -r c129354f2ff6 -r 3104d62e7a16 Quot/quotient_tacs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/quotient_tacs.ML Thu Dec 17 14:58:33 2009 +0100 @@ -0,0 +1,619 @@ +signature QUOTIENT_TACS = +sig + val regularize_tac: Proof.context -> int -> tactic + val all_inj_repabs_tac: Proof.context -> int -> tactic + val clean_tac: Proof.context -> int -> tactic + val procedure_tac: Proof.context -> thm -> int -> tactic + val lift_tac: Proof.context ->thm -> int -> tactic + val quotient_tac: Proof.context -> int -> tactic +end; + +structure Quotient_Tacs: QUOTIENT_TACS = +struct + +(* Since HOL_basic_ss is too "big" for us, *) +(* we need to set up our own minimal simpset. *) +fun mk_minimal_ss ctxt = + Simplifier.context ctxt empty_ss + setsubgoaler asm_simp_tac + setmksimps (mksimps []) + + + +(* various helper functions *) +fun OF1 thm1 thm2 = thm2 RS thm1 + +(* makes sure a subgoal is solved *) +fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) + +(* prints warning, if goal is unsolved *) +fun WARN (tac, msg) i st = + case Seq.pull ((SOLVES' tac) i st) of + NONE => (warning msg; Seq.single st) + | seqcell => Seq.make (fn () => seqcell) + +fun RANGE_WARN xs = RANGE (map WARN xs) + +fun atomize_thm thm = +let + val thm' = Thm.freezeT (forall_intr_vars thm) + val thm'' = ObjectLogic.atomize (cprop_of thm') +in + @{thm equal_elim_rule1} OF [thm'', thm'] +end + + + + +(* Regularize Tactic *) + +fun equiv_tac ctxt = + REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) + +fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) +val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac + +fun prep_trm thy (x, (T, t)) = + (cterm_of thy (Var (x, T)), cterm_of thy t) + +fun prep_ty thy (x, (S, ty)) = + (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) + +fun matching_prs thy pat trm = +let + val univ = Unify.matchers thy [(pat, trm)] + val SOME (env, _) = Seq.pull univ + val tenv = Vartab.dest (Envir.term_env env) + val tyenv = Vartab.dest (Envir.type_env env) +in + (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) +end + +fun calculate_instance ctxt thm redex R1 R2 = +let + val thy = ProofContext.theory_of ctxt + val goal = Const (@{const_name "equivp"}, dummyT) $ R2 + |> Syntax.check_term ctxt + |> HOLogic.mk_Trueprop + val eqv_prem = Goal.prove ctxt [] [] goal (fn _ => equiv_tac ctxt 1) + val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]]) + val R1c = cterm_of thy R1 + val thmi = Drule.instantiate' [] [SOME R1c] thm + val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex + val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi) +in + SOME thm2 +end +handle _ => NONE +(* FIXME/TODO: what is the place where the exception is raised: matching_prs? *) + +fun ball_bex_range_simproc ss redex = +let + val ctxt = Simplifier.the_context ss +in + case redex of + (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ + (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => + calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2 + + | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ + (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => + calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2 + | _ => NONE +end + +(* test whether DETERM makes any difference *) +fun quotient_tac ctxt = SOLVES' + (REPEAT_ALL_NEW (FIRST' + [rtac @{thm identity_quotient}, + resolve_tac (quotient_rules_get ctxt)])) + +fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) +val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac + +fun solve_quotient_assum ctxt thm = + case Seq.pull (quotient_tac ctxt 1 thm) of + SOME (t, _) => t + | _ => error "solve_quotient_assum failed. Maybe a quotient_thm is missing" + + +(* 0. preliminary simplification step according to *) +(* thm ball_reg_eqv bex_reg_eqv babs_reg_eqv *) +(* ball_reg_eqv_range bex_reg_eqv_range *) +(* *) +(* 1. eliminating simple Ball/Bex instances *) +(* thm ball_reg_right bex_reg_left *) +(* *) +(* 2. monos *) +(* 3. commutation rules for ball and bex *) +(* thm ball_all_comm bex_ex_comm *) +(* *) +(* 4. then rel-equality (which need to be *) +(* instantiated to avoid loops) *) +(* thm eq_imp_rel *) +(* *) +(* 5. then simplification like 0 *) +(* *) +(* finally jump back to 1 *) + +fun regularize_tac ctxt = +let + val thy = ProofContext.theory_of ctxt + val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"} + val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} + val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) + val simpset = (mk_minimal_ss ctxt) + addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} + addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver + val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) +in + simp_tac simpset THEN' + REPEAT_ALL_NEW (CHANGED o FIRST' [ + resolve_tac @{thms ball_reg_right bex_reg_left}, + resolve_tac (Inductive.get_monos ctxt), + resolve_tac @{thms ball_all_comm bex_ex_comm}, + resolve_tac eq_eqvs, + simp_tac simpset]) +end + + + +(* Injection Tactic *) + +(* looks for QUOT_TRUE assumtions, and in case its parameter *) +(* is an application, it returns the function and the argument *) +fun find_qt_asm asms = +let + fun find_fun trm = + case trm of + (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true + | _ => false +in + case find_first find_fun asms of + SOME (_ $ (_ $ (f $ a))) => SOME (f, a) + | _ => NONE +end + +fun quot_true_simple_conv ctxt fnctn ctrm = + case (term_of ctrm) of + (Const (@{const_name QUOT_TRUE}, _) $ x) => + let + val fx = fnctn x; + val thy = ProofContext.theory_of ctxt; + val cx = cterm_of thy x; + val cfx = cterm_of thy fx; + val cxt = ctyp_of thy (fastype_of x); + val cfxt = ctyp_of thy (fastype_of fx); + val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp} + in + Conv.rewr_conv thm ctrm + end + +fun quot_true_conv ctxt fnctn ctrm = + case (term_of ctrm) of + (Const (@{const_name QUOT_TRUE}, _) $ _) => + quot_true_simple_conv ctxt fnctn ctrm + | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm + | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm + | _ => Conv.all_conv ctrm + +fun quot_true_tac ctxt fnctn = + CONVERSION + ((Conv.params_conv ~1 (fn ctxt => + (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) + +fun dest_comb (f $ a) = (f, a) +fun dest_bcomb ((_ $ l) $ r) = (l, r) + +(* TODO: Can this be done easier? *) +fun unlam t = + case t of + (Abs a) => snd (Term.dest_abs a) + | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) + +fun dest_fun_type (Type("fun", [T, S])) = (T, S) + | dest_fun_type _ = error "dest_fun_type" + +val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl + + +(* we apply apply_rsp only in case if the type needs lifting, *) +(* which is the case if the type of the data in the QUOT_TRUE *) +(* assumption is different from the corresponding type in the goal *) +val apply_rsp_tac = + Subgoal.FOCUS (fn {concl, asms, context,...} => + let + val bare_concl = HOLogic.dest_Trueprop (term_of concl) + val qt_asm = find_qt_asm (map term_of asms) + in + case (bare_concl, qt_asm) of + (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) => + if (fastype_of qt_fun) = (fastype_of f) + then no_tac + else + let + val ty_x = fastype_of x + val ty_b = fastype_of qt_arg + val ty_f = range_type (fastype_of f) + val thy = ProofContext.theory_of context + val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f] + val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; + val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} + in + (rtac inst_thm THEN' quotient_tac context) 1 + end + | _ => no_tac + end) + +fun equals_rsp_tac R ctxt = +let + val ty = domain_type (fastype_of R); + val thy = ProofContext.theory_of ctxt + val thm = Drule.instantiate' + [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp} +in + rtac thm THEN' quotient_tac ctxt +end +(* raised by instantiate' *) +handle THM _ => K no_tac + | TYPE _ => K no_tac + | TERM _ => K no_tac + + +fun rep_abs_rsp_tac ctxt = + SUBGOAL (fn (goal, i) => + case (bare_concl goal) of + (rel $ _ $ (rep $ (abs $ _))) => + (let + val thy = ProofContext.theory_of ctxt; + val (ty_a, ty_b) = dest_fun_type (fastype_of abs); + val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; + val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; + val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} + in + (rtac inst_thm THEN' quotient_tac ctxt) i + end + handle THM _ => no_tac | TYPE _ => no_tac) + | _ => no_tac) + + +(* FIXME /TODO needs to be adapted *) +(* +To prove that the regularised theorem implies the abs/rep injected, +we try: + + 1) theorems 'trans2' from the appropriate QUOT_TYPE + 2) remove lambdas from both sides: lambda_rsp_tac + 3) remove Ball/Bex from the right hand side + 4) use user-supplied RSP theorems + 5) remove rep_abs from the right side + 6) reflexivity of equality + 7) split applications of lifted type (apply_rsp) + 8) split applications of non-lifted type (cong_tac) + 9) apply extentionality + A) reflexivity of the relation + B) assumption + (Lambdas under respects may have left us some assumptions) + C) proving obvious higher order equalities by simplifying fun_rel + (not sure if it is still needed?) + D) unfolding lambda on one side + E) simplifying (= ===> =) for simpler respectfulness +*) + + +fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => +(case (bare_concl goal) of + (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *) + (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _) + => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam + + (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *) +| (Const (@{const_name "op ="},_) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) + => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} + + (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *) +| (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) + => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam + + (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *) +| Const (@{const_name "op ="},_) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) + => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} + + (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *) +| (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) + => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam + +| (_ $ + (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) + => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] + +| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => + (rtac @{thm refl} ORELSE' + (equals_rsp_tac R ctxt THEN' RANGE [ + quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])) + + (* reflexivity of operators arising from Cong_tac *) +| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl} + + (* respectfulness of constants; in particular of a simple relation *) +| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) + => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt + + (* R (...) (Rep (Abs ...)) ----> R (...) (...) *) + (* observe fun_map *) +| _ $ _ $ _ + => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) + ORELSE' rep_abs_rsp_tac ctxt + +| _ => K no_tac +) i) + +fun inj_repabs_step_tac ctxt rel_refl = + FIRST' [ + inj_repabs_tac_match ctxt, + (* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *) + + apply_rsp_tac ctxt THEN' + RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], + + (* (op =) (t $ ...) (t' $ ...) ----> Cong provided type of t does not need lifting *) + (* merge with previous tactic *) + Cong_Tac.cong_tac @{thm cong} THEN' + RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], + + (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *) + rtac @{thm ext} THEN' quot_true_tac ctxt unlam, + + (* resolving with R x y assumptions *) + atac, + + (* reflexivity of the basic relations *) + (* R ... ... *) + resolve_tac rel_refl] + +fun inj_repabs_tac ctxt = +let + val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) +in + inj_repabs_step_tac ctxt rel_refl +end + +fun all_inj_repabs_tac ctxt = + REPEAT_ALL_NEW (inj_repabs_tac ctxt) + + +(* Cleaning of the Theorem *) + + +(* expands all fun_maps, except in front of bound variables *) +fun fun_map_simple_conv xs ctrm = + case (term_of ctrm) of + ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => + if (member (op=) xs h) + then Conv.all_conv ctrm + else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm + | _ => Conv.all_conv ctrm + +fun fun_map_conv xs ctxt ctrm = + case (term_of ctrm) of + _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv + fun_map_simple_conv xs) ctrm + | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm + | _ => Conv.all_conv ctrm + +fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) + +fun mk_abs u i t = + if incr_boundvars i u aconv t then Bound i + else (case t of + t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2) + | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t') + | Bound j => if i = j then error "make_inst" else t + | _ => t) + +fun make_inst lhs t = +let + val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; + val _ $ (Abs (_, _, (_ $ g))) = t; +in + (f, Abs ("x", T, mk_abs u 0 g)) +end + +fun make_inst_id lhs t = +let + val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; + val _ $ (Abs (_, _, g)) = t; +in + (f, Abs ("x", T, mk_abs u 0 g)) +end + +(* Simplifies a redex using the 'lambda_prs' theorem. *) +(* First instantiates the types and known subterms. *) +(* Then solves the quotient assumptions to get Rep2 and Abs1 *) +(* Finally instantiates the function f using make_inst *) +(* If Rep2 is identity then the pattern is simpler and *) +(* make_inst_id is used *) +fun lambda_prs_simple_conv ctxt ctrm = + case (term_of ctrm) of + (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) => + (let + val thy = ProofContext.theory_of ctxt + val (ty_b, ty_a) = dest_fun_type (fastype_of r1) + val (ty_c, ty_d) = dest_fun_type (fastype_of a2) + val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] + val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] + val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} + val te = @{thm eq_reflection} OF [solve_quotient_assum ctxt (solve_quotient_assum ctxt lpi)] + val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te + val make_inst = if ty_c = ty_d then make_inst_id else make_inst + val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) + val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts + in + Conv.rewr_conv ti ctrm + end + handle _ => Conv.all_conv ctrm) + | _ => Conv.all_conv ctrm + +val lambda_prs_conv = + More_Conv.top_conv lambda_prs_simple_conv + +fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) + + +(* 1. folding of definitions and preservation lemmas; *) +(* and simplification with *) +(* thm babs_prs all_prs ex_prs *) +(* *) +(* 2. unfolding of ---> in front of everything, except *) +(* bound variables (this prevents lambda_prs from *) +(* becoming stuck *) +(* thm fun_map.simps *) +(* *) +(* 3. simplification with *) +(* thm lambda_prs *) +(* *) +(* 4. simplification with *) +(* thm Quotient_abs_rep Quotient_rel_rep id_simps *) +(* *) +(* 5. Test for refl *) + +fun clean_tac lthy = + let + val thy = ProofContext.theory_of lthy; + val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) + (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) + + val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs} + val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) + fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver + in + EVERY' [simp_tac (simps thms1), + fun_map_tac lthy, + lambda_prs_tac lthy, + simp_tac (simps thms2), + TRY o rtac refl] + end + + + +(* Tactic for Genralisation of Free Variables in a Goal *) + +fun inst_spec ctrm = + Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} + +fun inst_spec_tac ctrms = + EVERY' (map (dtac o inst_spec) ctrms) + +fun all_list xs trm = + fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm + +fun apply_under_Trueprop f = + HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop + +fun gen_frees_tac ctxt = + SUBGOAL (fn (concl, i) => + let + val thy = ProofContext.theory_of ctxt + val vrs = Term.add_frees concl [] + val cvrs = map (cterm_of thy o Free) vrs + val concl' = apply_under_Trueprop (all_list vrs) concl + val goal = Logic.mk_implies (concl', concl) + val rule = Goal.prove ctxt [] [] goal + (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) + in + rtac rule i + end) + + +(* The General Shape of the Lifting Procedure *) + +(* - A is the original raw theorem *) +(* - B is the regularized theorem *) +(* - C is the rep/abs injected version of B *) +(* - D is the lifted theorem *) +(* *) +(* - 1st prem is the regularization step *) +(* - 2nd prem is the rep/abs injection step *) +(* - 3rd prem is the cleaning part *) +(* *) +(* the QUOT_TRUE premise in 2 records the lifted theorem *) + +val lifting_procedure = + @{lemma "[|A; + A --> B; + QUOT_TRUE D ==> B = C; + C = D|] ==> D" + by (simp add: QUOT_TRUE_def)} + +fun lift_match_error ctxt fun_str rtrm qtrm = +let + val rtrm_str = Syntax.string_of_term ctxt rtrm + val qtrm_str = Syntax.string_of_term ctxt qtrm + val msg = cat_lines [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, + "", "does not match with original theorem", rtrm_str] +in + error msg +end + + +fun procedure_inst ctxt rtrm qtrm = +let + val thy = ProofContext.theory_of ctxt + val rtrm' = HOLogic.dest_Trueprop rtrm + val qtrm' = HOLogic.dest_Trueprop qtrm + val reg_goal = + Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') + handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm + val inj_goal = + Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) + handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm +in + Drule.instantiate' [] + [SOME (cterm_of thy rtrm'), + SOME (cterm_of thy reg_goal), + NONE, + SOME (cterm_of thy inj_goal)] lifting_procedure +end + + +(* the tactic leaves three subgoals to be proved *) +fun procedure_tac ctxt rthm = + ObjectLogic.full_atomize_tac + THEN' gen_frees_tac ctxt + THEN' CSUBGOAL (fn (goal, i) => + let + val rthm' = atomize_thm rthm + val rule = procedure_inst ctxt (prop_of rthm') (term_of goal) + in + (rtac rule THEN' rtac rthm') i + end) + + +(* Automatic Proofs *) + +val msg1 = "Regularize proof failed." +val msg2 = cat_lines ["Injection proof failed.", + "This is probably due to missing respects lemmas.", + "Try invoking the injection method manually to see", + "which lemmas are missing."] +val msg3 = "Cleaning proof failed." + +fun lift_tac ctxt rthm = + procedure_tac ctxt rthm + THEN' RANGE_WARN + [(regularize_tac ctxt, msg1), + (all_inj_repabs_tac ctxt, msg2), + (clean_tac ctxt, msg3)] + + + +end; \ No newline at end of file