Merge + Added LarryInt & Fset3 to tests.
theory QuotMain+ −
imports QuotScript 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+ −
+ −
end+ −
+ −
section {* type definition for the quotient type *}+ −
+ −
(* the auxiliary data for the quotient types *)+ −
use "quotient_info.ML"+ −
+ −
ML {* print_mapsinfo @{context} *}+ −
+ −
declare [[map "fun" = (fun_map, fun_rel)]]+ −
+ −
lemmas [quot_thm] = fun_quotient + −
+ −
lemmas [quot_respect] = quot_rel_rsp+ −
+ −
(* fun_map is not here since equivp is not true *)+ −
lemmas [quot_equiv] = identity_equivp+ −
+ −
(* 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" for us, *)+ −
(* we set up our own minimal simpset. *)+ −
ML {*+ −
fun mk_minimal_ss ctxt =+ −
Simplifier.context ctxt empty_ss+ −
setsubgoaler asm_simp_tac+ −
setmksimps (mksimps [])+ −
*}+ −
+ −
ML {*+ −
fun OF1 thm1 thm2 = thm2 RS thm1+ −
*}+ −
+ −
section {* Atomize Infrastructure *}+ −
+ −
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 *}+ −
+ −
lemmas [id_simps] =+ −
fun_map_id[THEN eq_reflection]+ −
id_apply[THEN eq_reflection]+ −
id_def[THEN eq_reflection,symmetric]+ −
+ −
section {* Computation of the Regularize Goal *} + −
+ −
(*+ −
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 rtrm *)+ −
(* - the result is contains dummyT *)+ −
(* - 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, Type(st, _))) =>+ −
let + −
fun same_name (Const (s, _)) (Const (s', _)) = (s = s')+ −
| same_name _ _ = false+ −
in+ −
(* TODO/FIXME: This test is not enough *)+ −
if same_name rtrm qtrm then rtrm+ −
else + −
let + −
val exc1 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") not found)")+ −
val exc2 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") mismatch)")+ −
val thy = ProofContext.theory_of lthy+ −
val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1+ −
in + −
if Pattern.matches thy (rtrm', rtrm) then rtrm else+ −
let+ −
val _ = tracing ("rtrm := " ^ Syntax.string_of_term @{context} rtrm);+ −
val _ = tracing ("rtrm':= " ^ Syntax.string_of_term @{context} rtrm');+ −
in raise exc2 end+ −
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) =>+ −
let val (rts, qts) = (Syntax.string_of_term lthy rt, Syntax.string_of_term lthy qt) in+ −
raise (LIFT_MATCH ("regularize failed (default: " ^ rts ^ "," ^ qts ^ ")"))+ −
end+ −
*}+ −
+ −
section {* Regularize Tactic *}+ −
+ −
ML {*+ −
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+ −
*}+ −
+ −
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 is 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)+ −
+ −
(* Regularize Tactic *)+ −
+ −
(* 0. preliminary simplification step according to *)+ −
thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *)+ −
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 *)+ −
+ −
ML {*+ −
fun quotient_tac ctxt =+ −
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+ −
*}+ −
+ −
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 babs_reg_eqv babs_simp}+ −
addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver+ −
(* TODO: Make sure that there are no list_rel, pair_rel etc involved *)+ −
(* can this cause loops in equiv_tac ? *)+ −
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+ −
*}+ −
+ −
section {* Calculation of the Injected Goal *}+ −
+ −
(*+ −
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 _)) =>+ −
let+ −
val rty = fastype_of rtrm+ −
val qty = fastype_of qtrm+ −
in+ −
mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')))+ −
end+ −
+ −
| (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 *)+ −
(* Hasn't it already been checked in regularize? *)+ −
| (_, 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 {* Injection Tactic *}+ −
+ −
ML {*+ −
fun solve_quotient_assums ctxt thm =+ −
let + −
val goal = hd (Drule.strip_imp_prems (cprop_of thm)) + −
in+ −
thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)]+ −
end+ −
handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"+ −
*}+ −
+ −
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)"+ −
by (simp_all add: QUOT_TRUE_def ext)+ −
+ −
lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"+ −
by (simp add: QUOT_TRUE_def)+ −
+ −
lemma regularize_to_injection: "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"+ −
by(auto 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 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+ −
handle THM _ => K no_tac + −
| TYPE _ => K no_tac + −
| TERM _ => K 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 = 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]+ −
+ −
| 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 (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)+ −
(* observe ---> *)+ −
| _ $ _ $ _+ −
=> (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) ORELSE' rep_abs_rsp_tac ctxt+ −
+ −
| _ => error "inj_repabs_tac not a relation"+ −
) i)+ −
*}+ −
+ −
ML {*+ −
fun inj_repabs_step_tac ctxt rel_refl =+ −
(FIRST' [+ −
inj_repabs_tac_match ctxt,+ −
(* R (t $ \<dots>) (t' $ \<dots>) ----> 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 $ \<dots>) (t' $ \<dots>) ----> 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 =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)+ −
rtac @{thm ext} THEN' quot_true_tac ctxt unlam,+ −
+ −
(* resolving with R x y assumptions *)+ −
atac,+ −
+ −
(* reflexivity of the basic relations *)+ −
(* R \<dots> \<dots> *)+ −
resolve_tac rel_refl])+ −
*}+ −
+ −
ML {*+ −
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)+ −
*}+ −
+ −
section {* Cleaning of the Theorem *}+ −
+ −
ML {*+ −
fun fun_map_simple_conv xs ctxt 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 ctxt) 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)+ −
*}+ −
+ −
(* Since the patterns for the lhs are different; there are 2 different make-insts *)+ −
(* 1: does ? \<rightarrow> id *)+ −
(* 2: does ? \<rightarrow> non-id *)+ −
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 make_inst2 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) $ (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 ti =+ −
(let+ −
val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te+ −
val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)+ −
in+ −
Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts+ −
end handle _ => (* TODO handle only Bind | Error "make_inst" *)+ −
let+ −
val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te+ −
val _ = tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts)));+ −
val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));+ −
val (insp, inst) = make_inst2 (term_of (Thm.lhs_of ts)) (term_of ctrm)+ −
in+ −
Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts+ −
end handle _ => (* TODO handle only Bind | Error "make_inst" *)+ −
let+ −
val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm)+ −
val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te+ −
in+ −
MetaSimplifier.rewrite_rule (id_simps_get ctxt) td+ −
end);+ −
val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{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 ("ti rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))+ −
else ()+ −
+ −
in+ −
Conv.rewr_conv ti ctrm+ −
end+ −
handle _ => Conv.all_conv ctrm)+ −
| _ => 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)+ −
*}+ −
+ −
(* 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 *)+ −
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 *)+ −
+ −
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: 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+ −
*}+ −
+ −
section {* Tactic for 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 {* 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 *)+ −
+ −
ML {*+ −
val lifting_procedure = + −
@{lemma "\<lbrakk>A; A \<longrightarrow> B; QUOT_TRUE D \<Longrightarrow> B = C; C = D\<rbrakk> \<Longrightarrow> D" by (simp add: QUOT_TRUE_def)}+ −
*}+ −
+ −
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 = cat_lines [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, + −
"", "does not match with original theorem", rtrm_str]+ −
in+ −
error 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 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+ −
*}+ −
+ −
ML {*+ −
(* 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)+ −
*}+ −
+ −
section {* Automatic Proofs *}+ −
+ −
ML {*+ −
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)+ −
*}+ −
+ −
ML {*+ −
local+ −
+ −
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."+ −
+ −
in+ −
+ −
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+ −
*}+ −
+ −
section {* Methods / Interface *}+ −
+ −
ML {*+ −
fun mk_method1 tac thm ctxt =+ −
SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) + −
+ −
fun mk_method2 tac ctxt =+ −
SIMPLE_METHOD (HEADGOAL (tac ctxt)) + −
*}+ −
+ −
method_setup lifting =+ −
{* Attrib.thm >> (mk_method1 lift_tac) *}+ −
{* Lifting of theorems to quotient types. *}+ −
+ −
method_setup lifting_setup =+ −
{* Attrib.thm >> (mk_method1 procedure_tac) *}+ −
{* Sets up the three goals for the lifting procedure. *}+ −
+ −
method_setup regularize =+ −
{* Scan.succeed (mk_method2 regularize_tac) *}+ −
{* Proves automatically the regularization goals from the lifting procedure. *}+ −
+ −
method_setup injection =+ −
{* Scan.succeed (mk_method2 all_inj_repabs_tac) *}+ −
{* Proves automatically the rep/abs injection goals from the lifting procedure. *}+ −
+ −
method_setup cleaning =+ −
{* Scan.succeed (mk_method2 clean_tac) *}+ −
{* Proves automatically the cleaning goals from the lifting procedure. *}+ −
+ −
end+ −
+ −