get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
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 -> tacticend;structure Quotient_Tacs: QUOTIENT_TACS =structopen Quotient_Info;open Quotient_Type;open Quotient_Term;(* 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_tacfun 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)endfun 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 thm2endhandle _ => 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 ssin 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 | _ => NONEend(* 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_tacfun 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 | _ => falsein case find_first find_fun asms of SOME (_ $ (_ $ (f $ a))) => SOME (f, a) | _ => NONEendfun 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 endfun 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 ctrmfun 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 ctxtend(* raised by instantiate' *)handle THM _ => K no_tac | TYPE _ => K no_tac | TERM _ => K no_tacfun 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 simp_tac ((mk_minimal_ss ctxt) addsimps (id_simps_get ctxt)) (* HACK? *) THEN' inj_repabs_step_tac ctxt rel_reflendfun 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 ctrmfun 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 ctrmfun 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))endfun 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 ctrmval lambda_prs_conv = More_Conv.top_conv lambda_prs_simple_convfun 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_aux 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] endfun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *)(* 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 trmfun apply_under_Trueprop f = HOLogic.dest_Trueprop #> f #> HOLogic.mk_Truepropfun 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 msgendfun 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 qtrmin Drule.instantiate' [] [SOME (cterm_of thy rtrm'), SOME (cterm_of thy reg_goal), NONE, SOME (cterm_of thy inj_goal)] lifting_procedureend(* 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; (* structure *)