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: "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 equiv 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 equiv 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: equiv[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: equiv[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: equiv[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 equiv 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 equiv 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 equiv 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)]]
lemmas [quotient_thm] =
fun_quotient list_quotient
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_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 {* 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 {*
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
*}
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
| (* 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)")
*}
(*
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
*)
(* FIXME: they should be in in the new Isabelle *)
lemma [mono]:
"(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
by blast
lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
by auto
(* FIXME: OPTION_equivp, PAIR_equivp, ... *)
ML {*
fun equiv_tac rel_eqvs =
REPEAT_ALL_NEW (FIRST'
[resolve_tac rel_eqvs,
rtac @{thm identity_equivp},
rtac @{thm list_equivp}])
*}
ML {*
fun ball_reg_eqv_simproc rel_eqvs ss redex =
let
val ctxt = Simplifier.the_context ss
val thy = ProofContext.theory_of ctxt
in
case redex of
(ogl as ((Const (@{const_name "Ball"}, _)) $
((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
(let
val gl = Const (@{const_name "equivp"}, dummyT) $ R;
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]);
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
in
SOME thm
end
handle _ => NONE
)
| _ => NONE
end
*}
ML {*
fun bex_reg_eqv_simproc rel_eqvs ss redex =
let
val ctxt = Simplifier.the_context ss
val thy = ProofContext.theory_of ctxt
in
case redex of
(ogl as ((Const (@{const_name "Bex"}, _)) $
((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
(let
val gl = Const (@{const_name "equivp"}, dummyT) $ R;
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]);
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
in
SOME thm
end
handle _ => NONE
)
| _ => NONE
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 ball_reg_eqv_range_simproc rel_eqvs ss redex =
let
val ctxt = Simplifier.the_context ss
val thy = ProofContext.theory_of ctxt
in
case redex of
(ogl as ((Const (@{const_name "Ball"}, _)) $
((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) =>
(let
val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
(* val _ = tracing (Syntax.string_of_term ctxt glc);*)
val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]);
val R1c = cterm_of thy R1;
val thmi = Drule.instantiate' [] [SOME R1c] thm;
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi));*)
val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); *)
in
SOME thm2
end
handle _ => NONE
)
| _ => NONE
end
*}
ML {*
fun bex_reg_eqv_range_simproc rel_eqvs ss redex =
let
val ctxt = Simplifier.the_context ss
val thy = ProofContext.theory_of ctxt
in
case redex of
(ogl as ((Const (@{const_name "Bex"}, _)) $
((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) =>
(let
val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
(* val _ = tracing (Syntax.string_of_term ctxt glc); *)
val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]);
val R1c = cterm_of thy R1;
val thmi = Drule.instantiate' [] [SOME R1c] thm;
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)
val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));*)
in
SOME thm2
end
handle _ => NONE
)
| _ => NONE
end
*}
lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
by (simp add: equivp_reflp)
ML {*
fun regularize_tac ctxt rel_eqvs =
let
val pat1 = [@{term "Ball (Respects R) P"}];
val pat2 = [@{term "Bex (Respects R) P"}];
val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}];
val thy = ProofContext.theory_of ctxt
val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs))
val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs))
val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs))
val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs))
val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4]
(* 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]) rel_eqvs
in
ObjectLogic.full_atomize_tac THEN'
simp_tac simp_ctxt 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 simp_ctxt
])
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 {*
fun strip_combn n u =
let fun stripc 0 x = x
| stripc n (f $ t, ts) = stripc (n - 1) (f, t::ts)
| stripc _ x = x
in stripc n (u, []) end
*}
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' as (Abs _)) =>
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
| _ =>
let
val (qhead, qargs) = strip_comb qtrm
val (rhead, rargs) = strip_combn (length qargs) rtrm
val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs)
in
case (rhead, qhead) of
(Const (s, T), Const (s', T')) =>
if T = T'
then list_comb (rhead, rargs')
else list_comb (mk_repabs lthy (T, T') rhead, rargs')
| (Free (x, T), Free (x', T')) =>
if T = T'
then list_comb (rhead, rargs')
else list_comb (mk_repabs lthy (T, T') rhead, rargs')
| (Abs _, Abs _) =>
list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')
(* FIXME: when there is an (op =), then lhs might have been a term *)
| (_, Const (@{const_name "op ="}, T)) =>
list_comb (rhead, rargs')
| _ => raise (LIFT_MATCH ("injection: rhead: " ^ (Syntax.string_of_term lthy rhead)
^ " qhead: " ^ (Syntax.string_of_term lthy qhead)))
end
end
*}
section {* RepAbs Injection Tactic *}
(* Not used anymore *)
(* FIXME/TODO: do not handle everything *)
ML {*
fun instantiate_tac thm =
Subgoal.FOCUS (fn {concl, ...} =>
let
val pat = Drule.strip_imp_concl (cprop_of thm)
val insts = Thm.first_order_match (pat, concl)
in
rtac (Drule.instantiate insts thm) 1
end
handle _ => no_tac)
*}
ML {*
fun quotient_tac ctxt =
REPEAT_ALL_NEW (FIRST'
[rtac @{thm identity_quotient},
resolve_tac (quotient_rules_get ctxt)])
*}
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)
| _ => error "find_qt_asm"
end
*}
(* 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"
*}
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"
*}
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
| _ => no_tac)
*}
ML {*
fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
*}
(*
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 {*
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 "op ="},_) $ _ $ _ =>
(* reflexivity of operators arising from Cong_tac *)
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)])
| _ $ _ $ _ =>
(* 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),
(* respectfulness of constants *)
NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt))
])
*}
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_allex_prs_simple_conv ctxt ctrm =
case (term_of ctrm) of
((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
let
val (ty_b, ty_a) = dest_fun_type (fastype_of r1);
val (ty_c, ty_d) = dest_fun_type (fastype_of a2);
val thy = ProofContext.theory_of ctxt;
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 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;
in
Conv.rewr_conv ti ctrm
end
| (Const (@{const_name Ball}, _) $ (Const (@{const_name Respects}, _) $ R) $
(((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) =>
let
val (ty_a, ty_b) = dest_fun_type (fastype_of absf);
val thy = ProofContext.theory_of ctxt;
val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
val thm = Drule.instantiate' tyinst tinst @{thm all_prs};
val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm];
in
Conv.rewr_conv ti ctrm
end
| (Const (@{const_name Bex}, _) $ (Const (@{const_name Respects}, _) $ R) $
(((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) =>
let
val (ty_a, ty_b) = dest_fun_type (fastype_of absf);
val thy = ProofContext.theory_of ctxt;
val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
val thm = Drule.instantiate' tyinst tinst @{thm ex_prs};
val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm];
in
Conv.rewr_conv ti ctrm
end
| _ => Conv.all_conv ctrm
*}
ML {*
val lambda_allex_prs_conv =
More_Conv.top_conv lambda_allex_prs_simple_conv
*}
ML {*
fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt)
*}
(*
Cleaning the theorem consists of 6 kinds of rewrites.
The first two need to be done before fun_map is unfolded
- lambda_prs:
(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f
- all_prs (and the same for exists: ex_prs)
\<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f
- Rewriting with definitions from the argument defs
NewConst ----> (rep ---> abs) oldConst
- Quotient_rel_rep:
Rel (Rep x) (Rep y) ----> x = y
- ABS_REP
Abs (Rep x) ----> x
- id_simps; fun_map.simps
The first one is implemented as a conversion (fast).
The second one is an EqSubst (slow).
The rest are a simp_tac and are fast.
*)
ML {* fun OF1 thm1 thm2 = thm2 RS thm1 *}
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 clean_tac lthy =
let
val thy = ProofContext.theory_of lthy;
val defs = map (Thm.varifyT o #def) (qconsts_dest thy)
val thms = @{thms eq_reflection[OF fun_map.simps]}
@ @{thms id_simps Quotient_abs_rep Quotient_rel_rep}
@ defs
val simp_ctxt = HOL_basic_ss addsimps thms addSolver quotient_solver
in
EVERY' [
(* (rep1 ---> abs2) (\<lambda>x. rep2 (f (abs1 x))) ----> f *)
(* Ball (Respects R) ((abs ---> id) f) ----> All f *)
NDT lthy "a" (TRY o lambda_allex_prs_tac lthy),
(* NewConst -----> (rep ---> abs) oldConst *)
(* abs (rep x) -----> x *)
(* R (Rep x) (Rep y) -----> x = y *)
(* id_simps; fun_map.simps *)
NDT lthy "c" (TRY o simp_tac simp_ctxt),
(* final step *)
NDT lthy "d" (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 _ = tracing "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 _ = tracing "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 rel_eqv =
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]) rel_eqv
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 rel_eqv,
rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2,
clean_tac ctxt]) i
end)
*}
end