--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/QuotMain.thy Mon Dec 07 14:09:50 2009 +0100
@@ -0,0 +1,1191 @@
+theory QuotMain
+imports QuotScript QuotList QuotProd Prove
+uses ("quotient_info.ML")
+ ("quotient.ML")
+ ("quotient_def.ML")
+begin
+
+
+locale QUOT_TYPE =
+ fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
+ and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
+ assumes equivp: "equivp R"
+ and rep_prop: "\<And>y. \<exists>x. Rep y = R x"
+ and rep_inverse: "\<And>x. Abs (Rep x) = x"
+ and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
+ and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
+begin
+
+definition
+ ABS::"'a \<Rightarrow> 'b"
+where
+ "ABS x \<equiv> Abs (R x)"
+
+definition
+ REP::"'b \<Rightarrow> 'a"
+where
+ "REP a = Eps (Rep a)"
+
+lemma lem9:
+ shows "R (Eps (R x)) = R x"
+proof -
+ have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
+ then have "R x (Eps (R x))" by (rule someI)
+ then show "R (Eps (R x)) = R x"
+ using equivp unfolding equivp_def by simp
+qed
+
+theorem thm10:
+ shows "ABS (REP a) \<equiv> a"
+ apply (rule eq_reflection)
+ unfolding ABS_def REP_def
+proof -
+ from rep_prop
+ obtain x where eq: "Rep a = R x" by auto
+ have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
+ also have "\<dots> = Abs (R x)" using lem9 by simp
+ also have "\<dots> = Abs (Rep a)" using eq by simp
+ also have "\<dots> = a" using rep_inverse by simp
+ finally
+ show "Abs (R (Eps (Rep a))) = a" by simp
+qed
+
+lemma REP_refl:
+ shows "R (REP a) (REP a)"
+unfolding REP_def
+by (simp add: equivp[simplified equivp_def])
+
+lemma lem7:
+ shows "(R x = R y) = (Abs (R x) = Abs (R y))"
+apply(rule iffI)
+apply(simp)
+apply(drule rep_inject[THEN iffD2])
+apply(simp add: abs_inverse)
+done
+
+theorem thm11:
+ shows "R r r' = (ABS r = ABS r')"
+unfolding ABS_def
+by (simp only: equivp[simplified equivp_def] lem7)
+
+
+lemma REP_ABS_rsp:
+ shows "R f (REP (ABS g)) = R f g"
+ and "R (REP (ABS g)) f = R g f"
+by (simp_all add: thm10 thm11)
+
+lemma Quotient:
+ "Quotient R ABS REP"
+apply(unfold Quotient_def)
+apply(simp add: thm10)
+apply(simp add: REP_refl)
+apply(subst thm11[symmetric])
+apply(simp add: equivp[simplified equivp_def])
+done
+
+lemma R_trans:
+ assumes ab: "R a b"
+ and bc: "R b c"
+ shows "R a c"
+proof -
+ have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp
+ moreover have ab: "R a b" by fact
+ moreover have bc: "R b c" by fact
+ ultimately show "R a c" unfolding transp_def by blast
+qed
+
+lemma R_sym:
+ assumes ab: "R a b"
+ shows "R b a"
+proof -
+ have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp
+ then show "R b a" using ab unfolding symp_def by blast
+qed
+
+lemma R_trans2:
+ assumes ac: "R a c"
+ and bd: "R b d"
+ shows "R a b = R c d"
+using ac bd
+by (blast intro: R_trans R_sym)
+
+lemma REPS_same:
+ shows "R (REP a) (REP b) \<equiv> (a = b)"
+proof -
+ have "R (REP a) (REP b) = (a = b)"
+ proof
+ assume as: "R (REP a) (REP b)"
+ from rep_prop
+ obtain x y
+ where eqs: "Rep a = R x" "Rep b = R y" by blast
+ from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
+ then have "R x (Eps (R y))" using lem9 by simp
+ then have "R (Eps (R y)) x" using R_sym by blast
+ then have "R y x" using lem9 by simp
+ then have "R x y" using R_sym by blast
+ then have "ABS x = ABS y" using thm11 by simp
+ then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
+ then show "a = b" using rep_inverse by simp
+ next
+ assume ab: "a = b"
+ have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp
+ then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto
+ qed
+ then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
+qed
+
+end
+
+section {* type definition for the quotient type *}
+
+(* the auxiliary data for the quotient types *)
+use "quotient_info.ML"
+
+declare [[map list = (map, list_rel)]]
+declare [[map * = (prod_fun, prod_rel)]]
+declare [[map "fun" = (fun_map, fun_rel)]]
+
+(* identity quotient is not here as it has to be applied first *)
+lemmas [quotient_thm] =
+ fun_quotient list_quotient prod_quotient
+
+lemmas [quotient_rsp] =
+ quot_rel_rsp nil_rsp cons_rsp foldl_rsp pair_rsp
+
+(* fun_map is not here since equivp is not true *)
+(* TODO: option, ... *)
+lemmas [quotient_equiv] =
+ identity_equivp list_equivp prod_equivp
+
+
+ML {* maps_lookup @{theory} "List.list" *}
+ML {* maps_lookup @{theory} "*" *}
+ML {* maps_lookup @{theory} "fun" *}
+
+
+(* definition of the quotient types *)
+(* FIXME: should be called quotient_typ.ML *)
+use "quotient.ML"
+
+
+(* lifting of constants *)
+use "quotient_def.ML"
+
+section {* Simset setup *}
+
+(* since HOL_basic_ss is too "big", we need to set up *)
+(* our own minimal simpset *)
+ML {*
+fun mk_minimal_ss ctxt =
+ Simplifier.context ctxt empty_ss
+ setsubgoaler asm_simp_tac
+ setmksimps (mksimps [])
+*}
+
+section {* atomize *}
+
+lemma atomize_eqv[atomize]:
+ shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
+proof
+ assume "A \<equiv> B"
+ then show "Trueprop A \<equiv> Trueprop B" by unfold
+next
+ assume *: "Trueprop A \<equiv> Trueprop B"
+ have "A = B"
+ proof (cases A)
+ case True
+ have "A" by fact
+ then show "A = B" using * by simp
+ next
+ case False
+ have "\<not>A" by fact
+ then show "A = B" using * by auto
+ qed
+ then show "A \<equiv> B" by (rule eq_reflection)
+qed
+
+ML {*
+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
+*}
+
+section {* infrastructure about id *}
+
+lemma prod_fun_id: "prod_fun id id \<equiv> id"
+ by (rule eq_reflection) (simp add: prod_fun_def)
+
+lemma map_id: "map id \<equiv> id"
+ apply (rule eq_reflection)
+ apply (rule ext)
+ apply (rule_tac list="x" in list.induct)
+ apply (simp_all)
+ done
+
+lemmas id_simps =
+ fun_map_id[THEN eq_reflection]
+ id_apply[THEN eq_reflection]
+ id_def[THEN eq_reflection,symmetric]
+ prod_fun_id map_id
+
+ML {*
+fun simp_ids thm =
+ MetaSimplifier.rewrite_rule @{thms id_simps} thm
+*}
+
+section {* Debugging infrastructure for testing tactics *}
+
+ML {*
+fun my_print_tac ctxt s i thm =
+let
+ val prem_str = nth (prems_of thm) (i - 1)
+ |> Syntax.string_of_term ctxt
+ handle Subscript => "no subgoal"
+ val _ = tracing (s ^ "\n" ^ prem_str)
+in
+ Seq.single thm
+end *}
+
+ML {*
+fun DT ctxt s tac i thm =
+let
+ val before_goal = nth (prems_of thm) (i - 1)
+ |> Syntax.string_of_term ctxt
+ val before_msg = ["before: " ^ s, before_goal, "after: " ^ s]
+ |> cat_lines
+in
+ EVERY [tac i, my_print_tac ctxt before_msg i] thm
+end
+
+fun NDT ctxt s tac thm = tac thm
+*}
+
+section {* Matching of terms and types *}
+
+ML {*
+fun matches_typ (ty, ty') =
+ case (ty, ty') of
+ (_, TVar _) => true
+ | (TFree x, TFree x') => x = x'
+ | (Type (s, tys), Type (s', tys')) =>
+ s = s' andalso
+ if (length tys = length tys')
+ then (List.all matches_typ (tys ~~ tys'))
+ else false
+ | _ => false
+*}
+
+ML {*
+fun matches_term (trm, trm') =
+ case (trm, trm') of
+ (_, Var _) => true
+ | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty')
+ | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty')
+ | (Bound i, Bound j) => i = j
+ | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t')
+ | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s')
+ | _ => false
+*}
+
+section {* Infrastructure for collecting theorems for starting the lifting *}
+
+ML {*
+fun lookup_quot_data lthy qty =
+ let
+ val qty_name = fst (dest_Type qty)
+ val SOME quotdata = quotdata_lookup lthy qty_name
+ (* TODO: Should no longer be needed *)
+ val rty = Logic.unvarifyT (#rtyp quotdata)
+ val rel = #rel quotdata
+ val rel_eqv = #equiv_thm quotdata
+ val rel_refl = @{thm equivp_reflp} OF [rel_eqv]
+ in
+ (rty, rel, rel_refl, rel_eqv)
+ end
+*}
+
+ML {*
+fun lookup_quot_thms lthy qty_name =
+ let
+ val thy = ProofContext.theory_of lthy;
+ val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
+ val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
+ val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")
+ val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name)
+ in
+ (trans2, reps_same, absrep, quot)
+ end
+*}
+
+section {* Regularization *}
+
+(*
+Regularizing an rtrm means:
+ - quantifiers over a type that needs lifting are replaced by
+ bounded quantifiers, for example:
+ \<forall>x. P \<Longrightarrow> \<forall>x \<in> (Respects R). P / All (Respects R) P
+
+ the relation R is given by the rty and qty;
+
+ - abstractions over a type that needs lifting are replaced
+ by bounded abstractions:
+ \<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P)
+
+ - equalities over the type being lifted are replaced by
+ corresponding relations:
+ A = B \<Longrightarrow> A \<approx> B
+
+ example with more complicated types of A, B:
+ A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B
+*)
+
+ML {*
+(* builds the relation that is the argument of respects *)
+fun mk_resp_arg lthy (rty, qty) =
+let
+ val thy = ProofContext.theory_of lthy
+in
+ if rty = qty
+ then HOLogic.eq_const rty
+ else
+ case (rty, qty) of
+ (Type (s, tys), Type (s', tys')) =>
+ if s = s'
+ then let
+ val SOME map_info = maps_lookup thy s
+ val args = map (mk_resp_arg lthy) (tys ~~ tys')
+ in
+ list_comb (Const (#relfun map_info, dummyT), args)
+ end
+ else let
+ val SOME qinfo = quotdata_lookup_thy thy s'
+ (* FIXME: check in this case that the rty and qty *)
+ (* FIXME: correspond to each other *)
+ val (s, _) = dest_Const (#rel qinfo)
+ (* FIXME: the relation should only be the string *)
+ (* FIXME: and the type needs to be calculated as below; *)
+ (* FIXME: maybe one should actually have a term *)
+ (* FIXME: and one needs to force it to have this type *)
+ in
+ Const (s, rty --> rty --> @{typ bool})
+ end
+ | _ => HOLogic.eq_const dummyT
+ (* FIXME: check that the types correspond to each other? *)
+end
+*}
+
+ML {*
+val mk_babs = Const (@{const_name Babs}, dummyT)
+val mk_ball = Const (@{const_name Ball}, dummyT)
+val mk_bex = Const (@{const_name Bex}, dummyT)
+val mk_resp = Const (@{const_name Respects}, dummyT)
+*}
+
+ML {*
+(* - applies f to the subterm of an abstraction, *)
+(* otherwise to the given term, *)
+(* - used by regularize, therefore abstracted *)
+(* variables do not have to be treated specially *)
+
+fun apply_subt f trm1 trm2 =
+ case (trm1, trm2) of
+ (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t')
+ | _ => f trm1 trm2
+
+(* the major type of All and Ex quantifiers *)
+fun qnt_typ ty = domain_type (domain_type ty)
+*}
+
+ML {*
+(* produces a regularized version of rtm *)
+(* - the result is still not completely typed *)
+(* - does not need any special treatment of *)
+(* bound variables *)
+
+fun regularize_trm lthy rtrm qtrm =
+ case (rtrm, qtrm) of
+ (Abs (x, ty, t), Abs (x', ty', t')) =>
+ let
+ val subtrm = Abs(x, ty, regularize_trm lthy t t')
+ in
+ if ty = ty'
+ then subtrm
+ else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
+ end
+
+ | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
+ let
+ val subtrm = apply_subt (regularize_trm lthy) t t'
+ in
+ if ty = ty'
+ then Const (@{const_name "All"}, ty) $ subtrm
+ else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
+ end
+
+ | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
+ let
+ val subtrm = apply_subt (regularize_trm lthy) t t'
+ in
+ if ty = ty'
+ then Const (@{const_name "Ex"}, ty) $ subtrm
+ else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
+ end
+
+ | (* equalities need to be replaced by appropriate equivalence relations *)
+ (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
+ if ty = ty'
+ then rtrm
+ else mk_resp_arg lthy (domain_type ty, domain_type ty')
+
+ | (* in this case we check whether the given equivalence relation is correct *)
+ (rel, Const (@{const_name "op ="}, ty')) =>
+ let
+ val exc = LIFT_MATCH "regularise (relation mismatch)"
+ val rel_ty = (fastype_of rel) handle TERM _ => raise exc
+ val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty')
+ in
+ if rel' = rel
+ then rtrm
+ else raise exc
+ end
+ | (_, Const (s, _)) =>
+ let
+ fun same_name (Const (s, _)) (Const (s', _)) = (s = s')
+ | same_name _ _ = false
+ in
+ if same_name rtrm qtrm
+ then rtrm
+ else
+ let
+ fun exc1 s = LIFT_MATCH ("regularize (constant " ^ s ^ " not found)")
+ val exc2 = LIFT_MATCH ("regularize (constant mismatch)")
+ val thy = ProofContext.theory_of lthy
+ val rtrm' = (#rconst (qconsts_lookup thy s)) handle NotFound => raise (exc1 s)
+ in
+ if matches_term (rtrm, rtrm')
+ then rtrm
+ else raise exc2
+ end
+ end
+
+ | (t1 $ t2, t1' $ t2') =>
+ (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')
+
+ | (Free (x, ty), Free (x', ty')) =>
+ (* this case cannot arrise as we start with two fully atomized terms *)
+ raise (LIFT_MATCH "regularize (frees)")
+
+ | (Bound i, Bound i') =>
+ if i = i'
+ then rtrm
+ else raise (LIFT_MATCH "regularize (bounds mismatch)")
+
+ | (rt, qt) =>
+ raise (LIFT_MATCH "regularize (default)")
+*}
+
+ML {*
+fun equiv_tac ctxt =
+ REPEAT_ALL_NEW (FIRST'
+ [resolve_tac (equiv_rules_get ctxt)])
+*}
+
+ML {*
+fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
+val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
+*}
+
+ML {*
+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)
+*}
+
+ML {*
+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
+*}
+
+ML {*
+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 {context,...} => equiv_tac context 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 can be raised: matching_prs? *)
+*}
+
+ML {*
+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
+*}
+
+lemma eq_imp_rel:
+ shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
+by (simp add: equivp_reflp)
+
+(* FIXME/TODO: How does regularizing work? *)
+(* FIXME/TODO: needs to be adapted
+
+To prove that the raw theorem implies the regularised one,
+we try in order:
+
+ - Reflexivity of the relation
+ - Assumption
+ - Elimnating quantifiers on both sides of toplevel implication
+ - Simplifying implications on both sides of toplevel implication
+ - Ball (Respects ?E) ?P = All ?P
+ - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
+
+*)
+ML {*
+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}
+ addsimprocs [simproc] addSolver equiv_solver
+ (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
+ val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
+in
+ ObjectLogic.full_atomize_tac THEN'
+ simp_tac simpset THEN'
+ REPEAT_ALL_NEW (FIRST' [
+ rtac @{thm ball_reg_right},
+ rtac @{thm bex_reg_left},
+ resolve_tac (Inductive.get_monos ctxt),
+ rtac @{thm ball_all_comm},
+ rtac @{thm bex_ex_comm},
+ resolve_tac eq_eqvs,
+ simp_tac simpset])
+end
+*}
+
+section {* Injections of rep and abses *}
+
+(*
+Injecting repabs means:
+
+ For abstractions:
+ * If the type of the abstraction doesn't need lifting we recurse.
+ * If it does we add RepAbs around the whole term and check if the
+ variable needs lifting.
+ * If it doesn't then we recurse
+ * If it does we recurse and put 'RepAbs' around all occurences
+ of the variable in the obtained subterm. This in combination
+ with the RepAbs above will let us change the type of the
+ abstraction with rewriting.
+ For applications:
+ * If the term is 'Respects' applied to anything we leave it unchanged
+ * If the term needs lifting and the head is a constant that we know
+ how to lift, we put a RepAbs and recurse
+ * If the term needs lifting and the head is a free applied to subterms
+ (if it is not applied we treated it in Abs branch) then we
+ put RepAbs and recurse
+ * Otherwise just recurse.
+*)
+
+ML {*
+fun mk_repabs lthy (T, T') trm =
+ Quotient_Def.get_fun repF lthy (T, T')
+ $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
+*}
+
+ML {*
+(* bound variables need to be treated properly, *)
+(* as the type of subterms need to be calculated *)
+(* in the abstraction case *)
+
+fun inj_repabs_trm lthy (rtrm, qtrm) =
+ case (rtrm, qtrm) of
+ (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
+ Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
+
+ | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
+ Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
+
+ | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
+ Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
+
+ | (Abs (x, T, t), Abs (x', T', t')) =>
+ let
+ val rty = fastype_of rtrm
+ val qty = fastype_of qtrm
+ val (y, s) = Term.dest_abs (x, T, t)
+ val (_, s') = Term.dest_abs (x', T', t')
+ val yvar = Free (y, T)
+ val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))
+ in
+ if rty = qty
+ then result
+ else mk_repabs lthy (rty, qty) result
+ end
+
+ | (t $ s, t' $ s') =>
+ (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))
+
+ | (Free (_, T), Free (_, T')) =>
+ if T = T'
+ then rtrm
+ else mk_repabs lthy (T, T') rtrm
+
+ | (_, Const (@{const_name "op ="}, _)) => rtrm
+
+ (* FIXME: check here that rtrm is the corresponding definition for the const *)
+ | (_, Const (_, T')) =>
+ let
+ val rty = fastype_of rtrm
+ in
+ if rty = T'
+ then rtrm
+ else mk_repabs lthy (rty, T') rtrm
+ end
+
+ | _ => raise (LIFT_MATCH "injection")
+*}
+
+section {* RepAbs Injection Tactic *}
+
+ML {*
+fun quotient_tac ctxt =
+ REPEAT_ALL_NEW (FIRST'
+ [rtac @{thm identity_quotient},
+ resolve_tac (quotient_rules_get ctxt)])
+*}
+
+(* solver for the simplifier *)
+ML {*
+fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
+val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
+*}
+
+ML {*
+fun solve_quotient_assums ctxt thm =
+ let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in
+ thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)]
+ end
+ handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
+*}
+
+(* Not used *)
+(* It proves the Quotient assumptions by calling quotient_tac *)
+ML {*
+fun solve_quotient_assum i ctxt thm =
+ let
+ val tac =
+ (compose_tac (false, thm, i)) THEN_ALL_NEW
+ (quotient_tac ctxt);
+ val gc = Drule.strip_imp_concl (cprop_of thm);
+ in
+ Goal.prove_internal [] gc (fn _ => tac 1)
+ end
+ handle _ => error "solve_quotient_assum"
+*}
+
+definition
+ "QUOT_TRUE x \<equiv> True"
+
+ML {*
+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))) => (f, a)
+ | SOME _ => error "find_qt_asm: no pair"
+ | NONE => error "find_qt_asm: no assumption"
+ end
+*}
+
+(*
+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
+
+*)
+
+lemma quot_true_dests:
+ shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
+ and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
+ and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))"
+ and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
+apply(simp_all add: QUOT_TRUE_def ext)
+done
+
+lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P"
+by (simp add: QUOT_TRUE_def)
+
+lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
+by (simp add: QUOT_TRUE_def)
+
+ML {*
+fun quot_true_conv1 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
+*}
+
+ML {*
+fun quot_true_conv ctxt fnctn ctrm =
+ case (term_of ctrm) of
+ (Const (@{const_name QUOT_TRUE}, _) $ _) =>
+ quot_true_conv1 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
+*}
+
+ML {*
+fun quot_true_tac ctxt fnctn = CONVERSION
+ ((Conv.params_conv ~1 (fn ctxt =>
+ (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
+*}
+
+ML {* fun dest_comb (f $ a) = (f, a) *}
+ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *}
+(* TODO: Can this be done easier? *)
+ML {*
+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)))
+*}
+
+ML {*
+fun dest_fun_type (Type("fun", [T, S])) = (T, S)
+ | dest_fun_type _ = error "dest_fun_type"
+*}
+
+ML {*
+val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
+*}
+
+ML {*
+val apply_rsp_tac =
+ Subgoal.FOCUS (fn {concl, asms, context,...} =>
+ case ((HOLogic.dest_Trueprop (term_of concl))) of
+ ((R2 $ (f $ x) $ (g $ y))) =>
+ (let
+ val (asmf, asma) = find_qt_asm (map term_of asms);
+ in
+ if (fastype_of asmf) = (fastype_of f) then no_tac else let
+ val ty_a = fastype_of x;
+ val ty_b = fastype_of asma;
+ val ty_c = range_type (type_of f);
+ val thy = ProofContext.theory_of context;
+ val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c];
+ val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp}
+ val te = solve_quotient_assums context thm
+ val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
+ val thm = Drule.instantiate' [] t_inst te
+ in
+ compose_tac (false, thm, 2) 1
+ end
+ end
+ handle ERROR "find_qt_asm: no pair" => no_tac)
+ | _ => no_tac)
+*}
+ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+*}
+
+ML {*
+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 thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
+ val te = solve_quotient_assums ctxt thm
+ in
+ rtac te i
+ end
+ handle _ => no_tac)
+ | _ => no_tac)
+*}
+
+ML {*
+fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
+(case (bare_concl goal) of
+ (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
+ ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _))
+ => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+
+ (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
+| (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\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>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\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
+| 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\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>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]
+
+ (* reflexivity of operators arising from Cong_tac *)
+| Const (@{const_name "op ="},_) $ _ $ _
+ => rtac @{thm refl} ORELSE'
+ (resolve_tac trans2 THEN' RANGE [
+ quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
+
+(* TODO: These patterns should should be somehow combined and generalized... *)
+| (Const (@{const_name fun_rel}, _) $ _ $ _) $
+ (Const (@{const_name fun_rel}, _) $ _ $ _) $
+ (Const (@{const_name fun_rel}, _) $ _ $ _)
+ => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
+
+| (Const (@{const_name fun_rel}, _) $ _ $ _) $
+ (Const (@{const_name prod_rel}, _) $ _ $ _) $
+ (Const (@{const_name prod_rel}, _) $ _ $ _)
+ => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
+
+ (* 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 (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
+ (* observe ---> *)
+| _ $ _ $ _
+ => rep_abs_rsp_tac ctxt
+
+| _ => error "inj_repabs_tac not a relation"
+) i)
+*}
+
+ML {*
+fun inj_repabs_tac ctxt rel_refl trans2 =
+ (FIRST' [
+ inj_repabs_tac_match ctxt trans2,
+ (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *)
+ NDT ctxt "A" (apply_rsp_tac ctxt THEN'
+ (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+ (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *)
+ (* merge with previous tactic *)
+ NDT ctxt "B" (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 =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
+ NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
+ (* resolving with R x y assumptions *)
+ NDT ctxt "E" (atac),
+ (* reflexivity of the basic relations *)
+ (* R \<dots> \<dots> *)
+ NDT ctxt "D" (resolve_tac rel_refl)
+ ])
+*}
+
+ML {*
+fun all_inj_repabs_tac ctxt rel_refl trans2 =
+ REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
+*}
+
+section {* Cleaning of the theorem *}
+
+ML {*
+fun make_inst lhs t =
+ let
+ val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+ val _ $ (Abs (_, _, g)) = t;
+ fun mk_abs i t =
+ if incr_boundvars i u aconv t then Bound i
+ else (case t of
+ t1 $ t2 => mk_abs i t1 $ mk_abs i t2
+ | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
+ | Bound j => if i = j then error "make_inst" else t
+ | _ => t);
+ in (f, Abs ("x", T, mk_abs 0 g)) end;
+*}
+
+ML {*
+fun lambda_prs_simple_conv ctxt ctrm =
+ case (term_of ctrm) of
+ ((Const (@{const_name fun_map}, _) $ r1 $ (a2 as (Const (s,_)))) $ (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_assums ctxt (solve_quotient_assums ctxt lpi)]
+ val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
+ val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
+ val tl = Thm.lhs_of ts
+ val (insp, inst) = make_inst (term_of tl) (term_of ctrm)
+ val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
+ val _ = if not (s = @{const_name "id"}) then
+ (tracing "lambda_prs";
+ tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
+ tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi)));
+ tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
+ tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts)));
+ tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))
+ else ()
+ in
+ Conv.rewr_conv ti ctrm
+ end
+ | _ => Conv.all_conv ctrm
+*}
+
+ML {*
+val lambda_prs_conv =
+ More_Conv.top_conv lambda_prs_simple_conv
+
+fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
+*}
+
+(*
+ Cleaning the theorem consists of three rewriting steps.
+ The first two need to be done before fun_map is unfolded
+
+ 1) lambda_prs:
+ (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f
+
+ Implemented as conversion since it is not a pattern.
+
+ 2) all_prs (the same for exists):
+ Ball (Respects R) ((abs ---> id) f) ----> All f
+
+ Rewriting with definitions from the argument defs
+ (rep ---> abs) oldConst ----> newconst
+
+ 3) Quotient_rel_rep:
+ Rel (Rep x) (Rep y) ----> x = y
+
+ Quotient_abs_rep:
+ Abs (Rep x) ----> x
+
+ id_simps; fun_map.simps
+*)
+
+ML {*
+fun clean_tac lthy =
+ let
+ val thy = ProofContext.theory_of lthy;
+ val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
+ (* FIXME: shouldn't the definitions already be varified? *)
+ val thms1 = @{thms all_prs ex_prs} @ defs
+ val thms2 = @{thms eq_reflection[OF fun_map.simps]}
+ @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep}
+ fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
+ in
+ EVERY' [lambda_prs_tac lthy,
+ simp_tac (simps thms1),
+ simp_tac (simps thms2),
+ TRY o rtac refl]
+ end
+*}
+
+section {* Genralisation of free variables in a goal *}
+
+ML {*
+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)
+*}
+
+section {* General outline 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 *)
+(* *)
+(* - b is the regularization step *)
+(* - c is the rep/abs injection step *)
+(* - d is the cleaning part *)
+
+lemma lifting_procedure:
+ assumes a: "A"
+ and b: "A \<Longrightarrow> B"
+ and c: "B = C"
+ and d: "C = D"
+ shows "D"
+ using a b c d
+ by simp
+
+ML {*
+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 = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str,
+ "and the lifted theorem\n", rtrm_str, "do not match"]
+in
+ error (space_implode " " msg)
+end
+*}
+
+ML {*
+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 _ = warning "Regularization done."
+ 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
+ val _ = warning "RepAbs Injection done."
+in
+ Drule.instantiate' []
+ [SOME (cterm_of thy rtrm'),
+ SOME (cterm_of thy reg_goal),
+ SOME (cterm_of thy inj_goal)] @{thm lifting_procedure}
+end
+*}
+
+(* Left for debugging *)
+ML {*
+fun procedure_tac ctxt rthm =
+ ObjectLogic.full_atomize_tac
+ THEN' gen_frees_tac ctxt
+ THEN' CSUBGOAL (fn (gl, i) =>
+ let
+ val rthm' = atomize_thm rthm
+ val rule = procedure_inst ctxt (prop_of rthm') (term_of gl)
+ val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i}
+ in
+ (rtac rule THEN' RANGE [rtac rthm', (fn _ => all_tac), rtac thm]) i
+ end)
+*}
+
+ML {*
+(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
+
+fun lift_tac ctxt rthm =
+ ObjectLogic.full_atomize_tac
+ THEN' gen_frees_tac ctxt
+ THEN' CSUBGOAL (fn (gl, i) =>
+ let
+ val rthm' = atomize_thm rthm
+ val rule = procedure_inst ctxt (prop_of rthm') (term_of gl)
+ val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt)
+ val quotients = quotient_rules_get ctxt
+ val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients
+ val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i}
+ in
+ (rtac rule THEN'
+ RANGE [rtac rthm',
+ regularize_tac ctxt,
+ rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2,
+ clean_tac ctxt]) i
+ end)
+*}
+
+end
+