theory QuotMainNew+ −
imports QuotScript QuotList 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 equiv: "EQUIV 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 equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)+ −
then have "R x (Eps (R x))" by (rule someI)+ −
then show "R (Eps (R x)) = R x"+ −
using equiv unfolding EQUIV_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: equiv[simplified EQUIV_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: equiv[simplified EQUIV_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: equiv[simplified EQUIV_def])+ −
done+ −
+ −
lemma R_trans:+ −
assumes ab: "R a b"+ −
and bc: "R b c"+ −
shows "R a c"+ −
proof -+ −
have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[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 TRANS_def by blast+ −
qed+ −
+ −
lemma R_sym:+ −
assumes ab: "R a b"+ −
shows "R b a"+ −
proof -+ −
have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp+ −
then show "R b a" using ab unfolding SYM_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 "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp+ −
then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto+ −
qed+ −
then show "R (REP a) (REP b) \<equiv> (a = b)" by simp+ −
qed+ −
+ −
end+ −
+ −
lemma equiv_trans2:+ −
assumes e: "EQUIV R"+ −
and ac: "R a c"+ −
and bd: "R b d"+ −
shows "R a b = R c d"+ −
using ac bd e+ −
unfolding EQUIV_REFL_SYM_TRANS TRANS_def SYM_def+ −
by (blast)+ −
+ −
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)]]+ −
+ −
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"+ −
+ −
(* TODO: Consider defining it with an "if"; sth like:+ −
Babs p m = \<lambda>x. if x \<in> p then m x else undefined+ −
*)+ −
definition+ −
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"+ −
where+ −
"(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"+ −
+ −
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_I[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 {* Infrastructure for special quotient identity *}+ −
+ −
definition+ −
"qid TYPE('a) TYPE('b) x \<equiv> x"+ −
+ −
ML {*+ −
fun get_typ_aux (Type ("itself", [T])) = T + −
fun get_typ (Const ("TYPE", T)) = get_typ_aux T+ −
fun get_tys (Const (@{const_name "qid"},_) $ ty1 $ ty2) =+ −
(get_typ ty1, get_typ ty2)+ −
+ −
fun is_qid (Const (@{const_name "qid"},_) $ _ $ _) = true+ −
| is_qid _ = false+ −
+ −
+ −
fun mk_itself ty = Type ("itself", [ty])+ −
fun mk_TYPE ty = Const ("TYPE", mk_itself ty)+ −
fun mk_qid (rty, qty, trm) = + −
Const (@{const_name "qid"}, [mk_itself rty, mk_itself qty, dummyT] ---> dummyT) + −
$ mk_TYPE rty $ mk_TYPE qty $ trm+ −
*}+ −
+ −
ML {*+ −
fun insertion_aux (rtrm, qtrm) =+ −
case (rtrm, qtrm) of+ −
(Abs (x, ty, t), Abs (x', ty', t')) =>+ −
let+ −
val (y, s) = Term.dest_abs (x, ty, t)+ −
val (_, s') = Term.dest_abs (x', ty', t')+ −
val yvar = Free (y, ty)+ −
val result = Term.lambda_name (y, yvar) (insertion_aux (s, s'))+ −
in + −
if ty = ty'+ −
then result+ −
else mk_qid (ty, ty', result)+ −
end+ −
| (_ $ _, _ $ _) =>+ −
let + −
val rty = fastype_of rtrm+ −
val qty = fastype_of qtrm+ −
val (rhead, rargs) = strip_comb rtrm+ −
val (qhead, qargs) = strip_comb qtrm+ −
val rargs' = map insertion_aux (rargs ~~ qargs)+ −
val rhead' = insertion_aux (rhead, qhead)+ −
val result = list_comb (rhead', rargs')+ −
in+ −
if rty = qty+ −
then result+ −
else mk_qid (rty, qty, result)+ −
end+ −
| (Free (_, ty), Free (_, ty')) =>+ −
if ty = ty'+ −
then rtrm + −
else mk_qid (ty, ty', rtrm)+ −
| (Const (s, ty), Const (s', ty')) =>+ −
if s = s'+ −
then rtrm+ −
else mk_qid (ty, ty', rtrm) + −
| (_, _) => raise (LIFT_MATCH "insertion")+ −
*}+ −
+ −
ML {*+ −
fun insertion ctxt rtrm qtrm = + −
Syntax.check_term ctxt (insertion_aux (rtrm, qtrm)) + −
*}+ −
+ −
+ −
fun+ −
intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)+ −
where+ −
"intrel (x, y) (u, v) = (x + v = u + y)"+ −
+ −
quotient my_int = "nat \<times> nat" / intrel+ −
apply(unfold EQUIV_def)+ −
apply(auto simp add: mem_def expand_fun_eq)+ −
done+ −
+ −
fun+ −
my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"+ −
where+ −
"my_plus (x, y) (u, v) = (x + u, y + v)"+ −
+ −
quotient_def + −
PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"+ −
where+ −
"PLUS \<equiv> my_plus"+ −
+ −
thm PLUS_def+ −
+ −
ML {* MetaSimplifier.rewrite_term *}+ −
+ −
ML {*+ −
let + −
val rtrm = @{term "\<forall>a b. my_plus a b \<approx> my_plus b a"}+ −
val qtrm = @{term "\<forall>a b. PLUS a b = PLUS b a"}+ −
val ctxt = @{context}+ −
in+ −
insertion ctxt rtrm qtrm+ −
(*|> Drule.term_rule @{theory} (MetaSimplifier.rewrite_rule [@{thm "qid_def"}])*)+ −
|> Syntax.string_of_term ctxt+ −
|> writeln+ −
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 trm =+ −
case trm of+ −
(Abs (x, T, t)) => Abs (x, T, f t)+ −
| _ => f trm+ −
+ −
(* the major type of All and Ex quantifiers *)+ −
fun qnt_typ ty = domain_type (domain_type ty) + −
*}+ −
+ −
ML {*+ −
(* produces a regularized version of trm *)+ −
(* - the result is still not completely typed *)+ −
(* - does not need any special treatment of *)+ −
(* bound variables *)+ −
+ −
fun regularize_trm lthy trm =+ −
case trm of+ −
(Const (@{const_name "qid"},_) $ rty' $ qty' $ Abs (x, ty, t)) =>+ −
let+ −
val rty = get_typ rty'+ −
val qty = get_typ qty'+ −
val subtrm = regularize_trm lthy t+ −
in + −
mk_qid (rty, qty, mk_babs $ (mk_resp $ mk_resp_arg lthy (rty, qty)) $ subtrm)+ −
end+ −
| (Const (@{const_name "qid"},_) $ rty' $ qty' $ (Const (@{const_name "All"}, ty) $ t)) => + −
let+ −
val subtrm = apply_subt (regularize_trm lthy) 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+ −
(* FIXME: Should = only be replaced, when fully applied? *) + −
(* Then there must be a 2nd argument *)+ −
| (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>+ −
let+ −
val subtrm = regularize_trm lthy t t'+ −
in+ −
if ty = ty'+ −
then Const (@{const_name "op ="}, ty) $ subtrm+ −
else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm+ −
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)")+ −
| (Const (s, ty), Const (s', ty')) =>+ −
if s = s' andalso ty = ty'+ −
then rtrm+ −
else rtrm (* FIXME: check correspondence according to definitions *) + −
| (rt, qt) => + −
raise (LIFT_MATCH "regularize (default)")+ −
*}+ −
+ −
(*+ −
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+ −
+ −
*)+ −
+ −
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 *)+ −
+ −
fun inj_repabs_trm lthy (rtrm, qtrm) =+ −
let+ −
val rty = fastype_of rtrm+ −
val qty = fastype_of qtrm+ −
in+ −
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') =>+ −
Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))+ −
| (Abs (x, T, t), Abs (x', T', t')) =>+ −
let+ −
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+ −
| _ =>+ −
(* FIXME / TODO: this is a case that needs to be looked at *)+ −
(* - variables get a rep-abs insde and outside an application *)+ −
(* - constants only get a rep-abs on the outside of the application *)+ −
(* - applications get a rep-abs insde and outside an application *)+ −
let+ −
val (rhead, rargs) = strip_comb rtrm+ −
val (qhead, qargs) = strip_comb qtrm+ −
val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs)+ −
in+ −
if rty = qty+ −
then+ −
case (rhead, qhead) of+ −
(Free (_, T), Free (_, T')) =>+ −
if T = T' then list_comb (rhead, rargs')+ −
else list_comb (mk_repabs lthy (T, T') rhead, rargs')+ −
| _ => list_comb (rhead, rargs')+ −
else+ −
case (rhead, qhead, length rargs') of+ −
(Const _, Const _, 0) => mk_repabs lthy (rty, qty) rhead+ −
| (Free (_, T), Free (_, T'), 0) => mk_repabs lthy (T, T') rhead+ −
| (Const _, Const _, _) => mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) + −
| (Free (x, T), Free (x', T'), _) => + −
mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs'))+ −
| (Abs _, Abs _, _ ) =>+ −
mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')) + −
| _ => raise (LIFT_MATCH "injection")+ −
end+ −
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 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),+ −
SOME (cterm_of thy inj_goal)] @{thm lifting_procedure}+ −
end+ −
*}+ −
+ −
(* Left for debugging *)+ −
ML {*+ −
fun procedure_tac lthy rthm =+ −
ObjectLogic.full_atomize_tac+ −
THEN' gen_frees_tac lthy+ −
THEN' Subgoal.FOCUS (fn {context, concl, ...} =>+ −
let+ −
val rthm' = atomize_thm rthm+ −
val rule = procedure_inst context (prop_of rthm') (term_of concl)+ −
in+ −
EVERY1 [rtac rule, rtac rthm']+ −
end) lthy+ −
*}+ −
+ −
ML {*+ −
(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)+ −
fun lift_tac lthy rthm rel_eqv rty quot defs =+ −
ObjectLogic.full_atomize_tac+ −
THEN' gen_frees_tac lthy+ −
THEN' Subgoal.FOCUS (fn {context, concl, ...} =>+ −
let+ −
val rthm' = atomize_thm rthm+ −
val rule = procedure_inst context (prop_of rthm') (term_of concl)+ −
val aps = find_aps (prop_of rthm') (term_of concl)+ −
val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv+ −
val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv+ −
in+ −
EVERY1+ −
[rtac rule, rtac rthm']+ −
end) lthy+ −
*}+ −
+ −
end+ −
+ −
+ −