theory QuotMain
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
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 Pure.equal_elim_rule1} OF [thm'', thm']
end
*}
ML {* atomize_thm @{thm list.induct} *}
section {* infrastructure about id *}
(* Need to have a meta-equality *)
lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
by (simp add: id_def)
(* TODO: can be also obtained with: *)
ML {* symmetric (eq_reflection OF @{thms id_def}) *}
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
ML {*
fun simp_ids lthy thm =
MetaSimplifier.rewrite_rule @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} thm
*}
section {* Does the same as 'subst' in a given theorem *}
ML {*
fun eqsubst_thm ctxt thms thm =
let
val goalstate = Goal.init (Thm.cprop_of thm)
val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
NONE => error "eqsubst_thm"
| SOME th => cprem_of th 1
val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a');
val cgoal = cterm_of (ProofContext.theory_of ctxt) goal
val rt = Goal.prove_internal [] cgoal (fn _ => tac);
in
@{thm Pure.equal_elim_rule1} OF [rt, thm]
end
*}
section {* Infrastructure about definitions *}
text {* expects atomized definition *}
ML {*
fun add_lower_defs_aux lthy thm =
let
val e1 = @{thm fun_cong} OF [thm];
val f = eqsubst_thm lthy @{thms fun_map.simps} e1;
val g = simp_ids lthy f
in
(simp_ids lthy thm) :: (add_lower_defs_aux lthy g)
end
handle _ => [simp_ids lthy thm]
*}
ML {*
fun add_lower_defs lthy def =
let
val def_pre_sym = symmetric def
val def_atom = atomize_thm def_pre_sym
val defs_all = add_lower_defs_aux lthy def_atom
in
map Thm.varifyT defs_all
end
*}
section {* infrastructure about collecting theorems for calling lifting *}
ML {*
fun lookup_quot_data lthy qty =
let
val qty_name = fst (dest_Type qty)
val SOME quotdata = quotdata_lookup lthy qty_name
(* cu: Changed the lookup\<dots>not sure whether this works *)
(* 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_pre = @{thm EQUIV_REFL} OF [rel_eqv]
val rel_refl = @{thm spec} OF [MetaSimplifier.rewrite_rule [@{thm REFL_def}] rel_refl_pre]
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
*}
ML {*
fun lookup_quot_consts defs =
let
fun dest_term (a $ b) = (a, b);
val def_terms = map (snd o Logic.dest_equals o concl_of) defs;
in
map (fst o dest_Const o snd o dest_term) def_terms
end
*}
(******************************************)
(******************************************)
(* version with explicit qtrm *)
(******************************************)
(******************************************)
ML {*
(*
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
*)
(* 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 *)
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 = REGULARIZE_trm lthy t t'
in
if ty = ty'
then Abs (x, ty, 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
(* 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')) =>
if x = x'
then rtrm (* FIXME: check whether types corresponds *)
else 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)")
*}
ML {*
fun mk_REGULARIZE_goal lthy rtrm qtrm =
Logic.mk_implies (rtrm, Syntax.check_term lthy (REGULARIZE_trm lthy rtrm qtrm))
*}
(*
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
*)
lemma my_equiv_res_forallR:
fixes P::"'a \<Rightarrow> bool"
fixes Q::"'b \<Rightarrow> bool"
assumes b: "(All Q) \<longrightarrow> (All P)"
shows "(All Q) \<longrightarrow> Ball (Respects E) P"
using b by auto
lemma my_equiv_res_forallL:
fixes P::"'a \<Rightarrow> bool"
fixes Q::"'b \<Rightarrow> bool"
assumes a: "EQUIV E"
assumes b: "(All Q) \<longrightarrow> (All P)"
shows "Ball (Respects E) P \<longrightarrow> (All P)"
using a b
unfolding EQUIV_def
by (metis IN_RESPECTS)
lemma my_equiv_res_existsR:
fixes P::"'a \<Rightarrow> bool"
fixes Q::"'b \<Rightarrow> bool"
assumes a: "EQUIV E"
and b: "(Ex Q) \<longrightarrow> (Ex P)"
shows "(Ex Q) \<longrightarrow> Bex (Respects E) P"
using a b
unfolding EQUIV_def
by (metis IN_RESPECTS)
lemma my_equiv_res_existsL:
fixes P::"'a \<Rightarrow> bool"
fixes Q::"'b \<Rightarrow> bool"
assumes b: "(Ex Q) \<longrightarrow> (Ex P)"
shows "Bex (Respects E) Q \<longrightarrow> (Ex P)"
using b
by (auto)
lemma universal_twice:
assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
using * by auto
lemma implication_twice:
assumes a: "c \<longrightarrow> a"
assumes b: "b \<longrightarrow> d"
shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
using a b by auto
(* version of REGULARIZE_tac including debugging information *)
ML {*
fun my_print_tac ctxt s thm =
let
val prems_str = prems_of thm
|> map (Syntax.string_of_term ctxt)
|> cat_lines
val _ = tracing (s ^ "\n" ^ prems_str)
in
Seq.single thm
end
fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))]
*}
ML {*
fun REGULARIZE_tac' lthy rel_refl rel_eqv =
(REPEAT1 o FIRST1)
[(K (print_tac "start")) THEN' (K no_tac),
DT lthy "1" (rtac rel_refl),
DT lthy "2" atac,
DT lthy "3" (rtac @{thm universal_twice}),
DT lthy "4" (rtac @{thm impI} THEN' atac),
DT lthy "5" (rtac @{thm implication_twice}),
DT lthy "6" (rtac @{thm my_equiv_res_forallR}),
DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_existsR})),
(* For a = b \<longrightarrow> a \<approx> b *)
DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})]
*}
ML {*
fun regularize_tac ctxt rel_eqv rel_refl =
(ObjectLogic.full_atomize_tac) THEN'
REPEAT_ALL_NEW (FIRST' [
rtac rel_refl,
atac,
rtac @{thm universal_twice},
rtac @{thm impI} THEN' atac,
rtac @{thm implication_twice},
EqSubst.eqsubst_tac ctxt [0]
[(@{thm equiv_res_forall} OF [rel_eqv]),
(@{thm equiv_res_exists} OF [rel_eqv])],
(* For a = b \<longrightarrow> a \<approx> b *)
(rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
(rtac @{thm RIGHT_RES_FORALL_REGULAR})
]);
*}
ML {*
fun regularize_tac ctxt rel_eqv rel_refl =
(ObjectLogic.full_atomize_tac) THEN'
REPEAT_ALL_NEW (FIRST'
[(K (print_tac "start")) THEN' (K no_tac),
DT ctxt "1" (rtac rel_refl),
DT ctxt "2" atac,
DT ctxt "3" (rtac @{thm universal_twice}),
DT ctxt "4" (rtac @{thm impI} THEN' atac),
DT ctxt "5" (rtac @{thm implication_twice}),
DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0]
[(@{thm equiv_res_forall} OF [rel_eqv]),
(@{thm equiv_res_exists} OF [rel_eqv])]),
(* For a = b \<longrightarrow> a \<approx> b *)
DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR})
]);
*}
thm RIGHT_RES_FORALL_REGULAR
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 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 lthy (t, t'))
| (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))
| (Const (@{const_name "Babs"}, T) $ r $ t, t') =>
Const (@{const_name "Babs"}, T) $ r $ (inj_REPABS 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 = lambda yvar (inj_REPABS 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 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 lthy (rhead, qhead), rargs'))
| _ => raise (LIFT_MATCH "injection")
end
end
*}
ML {*
fun mk_inj_REPABS_goal lthy (rtrm, qtrm) =
Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm)))
*}
section {* RepAbs injection tactic *}
(*
To prove that the regularised theorem implies the abs/rep injected, we first
atomize it and then try:
1) theorems 'trans2' from the appropriate QUOT_TYPE
2) remove lambdas from both sides (LAMBDA_RES_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
10) reflexivity of the relation
11) assumption
(Lambdas under respects may have left us some assumptions)
12) proving obvious higher order equalities by simplifying fun_rel
(not sure if it is still needed?)
13) unfolding lambda on one side
14) simplifying (= ===> =) for simpler respectfullness
*)
ML {*
fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
let
val pat = Drule.strip_imp_concl (cprop_of thm)
val insts = Thm.match (pat, concl)
in
rtac (Drule.instantiate insts thm) 1
end
handle _ => no_tac)
*}
ML {*
fun CHANGED' tac = (fn i => CHANGED (tac i))
*}
ML {*
fun quotient_tac quot_thm =
REPEAT_ALL_NEW (FIRST' [
rtac @{thm FUN_QUOTIENT},
rtac quot_thm,
rtac @{thm IDENTITY_QUOTIENT},
(* For functional identity quotients, (op = ---> op =) *)
CHANGED' (
(simp_tac (HOL_ss addsimps @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}
)))
])
*}
ML {*
fun LAMBDA_RES_TAC ctxt i st =
(case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
(_ $ (_ $ (Abs(_, _, _)) $ (Abs(_, _, _)))) =>
(EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
(rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
| _ => fn _ => no_tac) i st
*}
ML {*
fun WEAK_LAMBDA_RES_TAC ctxt i st =
(case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
(_ $ (_ $ _ $ (Abs(_, _, _)))) =>
(EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
(rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
| (_ $ (_ $ (Abs(_, _, _)) $ _)) =>
(EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
(rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
| _ => fn _ => no_tac) i st
*}
ML {* (* Legacy *)
fun needs_lift (rty as Type (rty_s, _)) ty =
case ty of
Type (s, tys) =>
(s = rty_s) orelse (exists (needs_lift rty) tys)
| _ => false
*}
ML {*
fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
let
val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
val insts = Thm.match (pat, concl)
in
if needs_lift rty (type_of f) then
rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
else no_tac
end
handle _ => no_tac)
*}
ML {*
val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
let
val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
(Const (@{const_name Ball}, _) $ _)) = term_of concl
in
((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
(simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
end
handle _ => no_tac)
*}
ML {*
val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
let
val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
(Const (@{const_name Bex}, _) $ _)) = term_of concl
in
((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
(simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
end
handle _ => no_tac)
*}
ML {*
fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
*}
ML {*
fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
(FIRST' [
rtac trans_thm,
LAMBDA_RES_TAC ctxt,
rtac @{thm RES_FORALL_RSP},
ball_rsp_tac ctxt,
rtac @{thm RES_EXISTS_RSP},
bex_rsp_tac ctxt,
FIRST' (map rtac rsp_thms),
rtac refl,
(instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm)])),
(APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])),
Cong_Tac.cong_tac @{thm cong},
rtac @{thm ext},
rtac reflex_thm,
atac,
SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
WEAK_LAMBDA_RES_TAC ctxt,
CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
])
*}
(****************************************)
(* cleaning of the theorem *)
(****************************************)
(* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)
ML {*
fun exchange_ty lthy rty qty ty =
let
val thy = ProofContext.theory_of lthy
in
if Sign.typ_instance thy (ty, rty) then
let
val inst = Sign.typ_match thy (rty, ty) Vartab.empty
in
Envir.subst_type inst qty
end
else
let
val (s, tys) = dest_Type ty
in
Type (s, map (exchange_ty lthy rty qty) tys)
end
end
handle TYPE _ => ty (* for dest_Type *)
*}
ML {*
fun find_matching_types rty ty =
if Type.raw_instance (Logic.varifyT ty, rty)
then [ty]
else
let val (s, tys) = dest_Type ty in
flat (map (find_matching_types rty) tys)
end
handle TYPE _ => []
*}
ML {*
fun negF absF = repF
| negF repF = absF
fun get_fun flag qenv lthy ty =
let
fun get_fun_aux s fs =
(case (maps_lookup (ProofContext.theory_of lthy) s) of
SOME info => list_comb (Const (#mapfun info, dummyT), fs)
| NONE => error ("no map association for type " ^ s))
fun get_const flag qty =
let
val thy = ProofContext.theory_of lthy
val qty_name = Long_Name.base_name (fst (dest_Type qty))
in
case flag of
absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)
| repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
end
fun mk_identity ty = Abs ("", ty, Bound 0)
in
if (AList.defined (op=) qenv ty)
then (get_const flag ty)
else (case ty of
TFree _ => mk_identity ty
| Type (_, []) => mk_identity ty
| Type ("fun" , [ty1, ty2]) =>
let
val fs_ty1 = get_fun (negF flag) qenv lthy ty1
val fs_ty2 = get_fun flag qenv lthy ty2
in
get_fun_aux "fun" [fs_ty1, fs_ty2]
end
| Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
| _ => error ("no type variables allowed"))
end
*}
ML {*
fun get_fun_OLD flag (rty, qty) lthy ty =
let
val tys = find_matching_types rty ty;
val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;
val xchg_ty = exchange_ty lthy rty qty ty
in
get_fun flag qenv lthy xchg_ty
end
*}
ML {*
fun applic_prs_old lthy rty qty absrep ty =
let
val rty = Logic.varifyT rty;
val qty = Logic.varifyT qty;
fun absty ty =
exchange_ty lthy rty qty ty
fun mk_rep tm =
let
val ty = exchange_ty lthy qty rty (fastype_of tm)
in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ tm) end;
fun mk_abs tm =
let
val ty = fastype_of tm
in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end
val (l, ltl) = Term.strip_type ty;
val nl = map absty l;
val vs = map (fn _ => "x") l;
val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
val args = map Free (vfs ~~ nl);
val lhs = list_comb((Free (fname, nl ---> ltl)), args);
val rargs = map mk_rep args;
val f = Free (fname, nl ---> ltl);
val rhs = mk_abs (list_comb((mk_rep f), rargs));
val eq = Logic.mk_equals (rhs, lhs);
val ceq = cterm_of (ProofContext.theory_of lthy') eq;
val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps});
val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t;
in
singleton (ProofContext.export lthy' lthy) t_id
end
*}
ML {*
fun applic_prs lthy absrep (rty, qty) =
let
fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm;
fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm;
val (raty, rgty) = Term.strip_type rty;
val (qaty, qgty) = Term.strip_type qty;
val vs = map (fn _ => "x") qaty;
val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
val f = Free (fname, qaty ---> qgty);
val args = map Free (vfs ~~ qaty);
val rhs = list_comb(f, args);
val largs = map2 mk_rep (raty ~~ qaty) args;
val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs));
val llhs = Syntax.check_term lthy lhs;
val eq = Logic.mk_equals (llhs, rhs);
val ceq = cterm_of (ProofContext.theory_of lthy') eq;
val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps map_id id_apply});
val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
val t_id = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply] id_def_sym} t;
in
singleton (ProofContext.export lthy' lthy) t_id
end
*}
ML {*
fun findaps_all rty tm =
case tm of
Abs(_, T, b) =>
findaps_all rty (subst_bound ((Free ("x", T)), b))
| (f $ a) => (findaps_all rty f @ findaps_all rty a)
| Free (_, (T as (Type ("fun", (_ :: _))))) =>
(if needs_lift rty T then [T] else [])
| _ => [];
fun findaps rty tm = distinct (op =) (findaps_all rty tm)
*}
ML {*
fun find_aps_all rtm qtm =
case (rtm, qtm) of
(Abs(_, T1, s1), Abs(_, T2, s2)) =>
find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2))
| (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) =>
let
val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2)
in
if T1 = T2 then sub else (T1, T2) :: sub
end
| ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2)
| _ => [];
fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)
*}
ML {*
(* FIXME: allex_prs and lambda_prs can be one function *)
fun allex_prs_tac lthy quot =
(EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
THEN' (quotient_tac quot);
*}
ML {*
let
val parser = Args.context -- Scan.lift Args.name_source
fun term_pat (ctxt, str) =
str |> ProofContext.read_term_pattern ctxt
|> ML_Syntax.print_term
|> ML_Syntax.atomic
in
ML_Antiquote.inline "term_pat" (parser >> term_pat)
end
*}
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 lambda_prs_conv1 ctxt quot ctrm =
case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
let
val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);
val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);
val thy = ProofContext.theory_of ctxt;
val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_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 tac =
(compose_tac (false, lpi, 2)) THEN_ALL_NEW
(quotient_tac quot);
val gc = Drule.strip_imp_concl (cprop_of lpi);
val t = Goal.prove_internal [] gc (fn _ => tac 1)
val te = @{thm eq_reflection} OF [t]
val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te
val tl = Thm.lhs_of ts
(* val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));*)
(* val _ = tracing (Syntax.string_of_term @{context} (term_of tl));*)
val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm);
val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts);
(* val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
in
Conv.rewr_conv ti ctrm
end
(* TODO: We can add a proper error message... *)
handle Bind => Conv.all_conv ctrm
*}
(* quot stands for the QUOTIENT theorems: *)
(* could be potentially all of them *)
ML {*
fun lambda_prs_conv ctxt quot ctrm =
case (term_of ctrm) of
(Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) =>
(Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt)
then_conv (lambda_prs_conv1 ctxt quot)) ctrm
| _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm
| Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm
| _ => Conv.all_conv ctrm
*}
ML {*
fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>
CONVERSION
(Conv.params_conv ~1 (fn ctxt =>
(Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv
Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
*}
ML {*
fun clean_tac lthy quot defs reps_same absrep aps =
let
val lower = flat (map (add_lower_defs lthy) defs)
val aps_thms = map (applic_prs lthy absrep) aps
in
EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
lambda_prs_tac lthy quot,
TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms),
TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower),
simp_tac (HOL_ss addsimps [reps_same])]
end
*}
(* Genralisation of free variables in a goal *)
ML {*
fun inst_spec ctrm =
let
val cty = ctyp_of_term ctrm
in
Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec}
end
fun inst_spec_tac ctrms =
EVERY' (map (dtac o inst_spec) ctrms)
fun abs_list (xs, t) =
fold (fn (x, T) => fn t' => HOLogic.all_const T $ (lambda (Free (x, T)) t')) xs t
fun gen_frees_tac ctxt =
SUBGOAL (fn (concl, i) =>
let
val thy = ProofContext.theory_of ctxt
val concl' = HOLogic.dest_Trueprop concl
val vrs = Term.add_frees concl' []
val cvrs = map (cterm_of thy o Free) vrs
val concl'' = HOLogic.mk_Trueprop (abs_list (vrs, concl'))
val goal = Logic.mk_implies (concl'', concl)
val rule = Goal.prove ctxt [] [] goal
(K ((inst_spec_tac (rev cvrs) THEN' atac) 1))
in
rtac rule i
end)
*}
(* 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 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_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_error ctxt s rtrm qtrm
val inj_goal =
Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))
handle (LIFT_MATCH s) => lift_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 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
rtac rule THEN' rtac rthm'
end 1) lthy
*}
ML {*
fun lift_tac lthy rthm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep 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)
in
rtac rule THEN' RANGE [
rtac rthm',
regularize_tac lthy rel_eqv rel_refl,
REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
clean_tac lthy quot defs reps_same absrep aps
]
end 1) lthy
*}
end