More functionality for lifting list.cases and list.recs.
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"
text {* FIXME: auxiliary function *}
ML {*
val no_vars = Thm.rule_attribute (fn context => fn th =>
let
val ctxt = Variable.set_body false (Context.proof_of context);
val ((_, [th']), _) = Variable.import true [th] ctxt;
in th' end);
*}
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 {* REGULARIZE *}
(*
Regularizing a theorem 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
- Abstractions over a type that needs lifting are replaced
by bounded abstactions:
\<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P)
- Equalities over the type being lifted are replaced by
appropriate relations:
A = B \<Longrightarrow> A \<approx> B
Example with more complicated types of A, B:
A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B
Regularizing is done in 3 phases:
- First a regularized term is created
- Next we prove that the original theorem implies the new one
- Finally using MP we get the new theorem.
To prove that the old theorem implies the new one, we first
atomize it and then try:
- 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
*)
text {* tyRel takes a type and builds a relation that a quantifier over this
type needs to respect. *}
ML {*
fun tyRel ty rty rel lthy =
if Sign.typ_instance (ProofContext.theory_of lthy) (ty, rty)
then rel
else (case ty of
Type (s, tys) =>
let
val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
val ty_out = ty --> ty --> @{typ bool};
val tys_out = tys_rel ---> ty_out;
in
(case (maps_lookup (ProofContext.theory_of lthy) s) of
SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
| NONE => HOLogic.eq_const ty
)
end
| _ => HOLogic.eq_const ty)
*}
(* ML {* cterm_of @{theory} (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) *} *)
definition
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
where
"(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
(* TODO: Consider defining it with an "if"; sth like:
Babs p m = \<lambda>x. if x \<in> p then m x else undefined
*)
ML {*
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 mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})
*}
(* applies f to the subterm of an abstractions, otherwise to the given term *)
ML {*
fun apply_subt f trm =
case trm of
Abs (x, T, t) =>
let
val (x', t') = Term.dest_abs (x, T, t)
in
Term.absfree (x', T, f t')
end
| _ => f trm
*}
(* FIXME: if there are more than one quotient, then you have to look up the relation *)
ML {*
fun my_reg lthy rel rty trm =
case trm of
Abs (x, T, t) =>
if (needs_lift rty T) then
let
val rrel = tyRel T rty rel lthy
in
(mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm)
end
else
Abs(x, T, (apply_subt (my_reg lthy rel rty) t))
| Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) =>
let
val ty1 = domain_type ty
val ty2 = domain_type ty1
val rrel = tyRel T rty rel lthy
in
if (needs_lift rty T) then
(mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
else
Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t
end
| Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) =>
let
val ty1 = domain_type ty
val ty2 = domain_type ty1
val rrel = tyRel T rty rel lthy
in
if (needs_lift rty T) then
(mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
else
Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t
end
| Const (@{const_name "op ="}, ty) $ t =>
if needs_lift rty (fastype_of t) then
(tyRel (fastype_of t) rty rel lthy) $ t
else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)
| t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
| _ => trm
*}
ML {*
fun my_reg_inst lthy rel rty trm =
case rel of
Const (n, _) => Syntax.check_term lthy
(my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm)
*}
(*
ML {*
text {*val r = term_of @{cpat "R::?'a list \<Rightarrow> ?'a list \<Rightarrow>bool"};*}
val r = Free ("R", dummyT);
val t = (my_reg @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});
val t2 = Syntax.check_term @{context} t;
Toplevel.program (fn () => cterm_of @{theory} t2)
*}*)
text {* Assumes that the given theorem is atomized *}
ML {*
fun build_regularize_goal thm rty rel lthy =
Logic.mk_implies
((prop_of thm),
(my_reg_inst lthy rel rty (prop_of thm)))
*}
lemma universal_twice:
"(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
by auto
lemma implication_twice:
"(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
by auto
(*lemma equality_twice: "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
by auto*)
ML {*
fun regularize thm rty rel rel_eqv rel_refl lthy =
let
val goal = build_regularize_goal thm rty rel lthy;
fun tac ctxt =
(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},
(*rtac @{thm equality_twice},*)
EqSubst.eqsubst_tac ctxt [0]
[(@{thm equiv_res_forall} OF [rel_eqv]),
(@{thm equiv_res_exists} OF [rel_eqv])],
(rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
(rtac @{thm RIGHT_RES_FORALL_REGULAR})
]);
val cthm = Goal.prove lthy [] [] goal
(fn {context,...} => tac context 1);
in
cthm OF [thm]
end
*}
section {* RepAbs injection *}
(* Needed to have a meta-equality *)
lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
by (simp add: id_def)
(* 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 _ => ty (* for dest_Type *)
*}
(*consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
axioms Rl_eq: "EQUIV Rl"
quotient ql = "'a list" / "Rl"
by (rule Rl_eq)
ML {*
ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"});
ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"})
*}
*)
ML {*
fun negF absF = repF
| negF repF = absF
fun get_fun_noexchange flag (rty, qty) lthy ty =
let
fun get_fun_aux s fs_tys =
let
val (fs, tys) = split_list fs_tys
val (otys, ntys) = split_list tys
val oty = Type (s, otys)
val nty = Type (s, ntys)
val ftys = map (op -->) tys
in
(case (maps_lookup (ProofContext.theory_of lthy) s) of
SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty))
| NONE => error ("no map association for type " ^ s))
end
fun get_fun_fun fs_tys =
let
val (fs, tys) = split_list fs_tys
val ([oty1, oty2], [nty1, nty2]) = split_list tys
val oty = nty1 --> oty2
val nty = oty1 --> nty2
val ftys = map (op -->) tys
in
(list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
end
val thy = ProofContext.theory_of lthy
fun get_const flag (rty, qty) =
let
val qty_name = Long_Name.base_name (fst (dest_Type qty))
in
case flag of
absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty))
| repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))
end
fun mk_identity ty = Abs ("", ty, Bound 0)
in
if (Sign.typ_instance thy (ty, rty))
then (get_const flag (ty, (exchange_ty lthy rty qty ty)))
else (case ty of
TFree _ => (mk_identity ty, (ty, ty))
| Type (_, []) => (mk_identity ty, (ty, ty))
| Type ("fun" , [ty1, ty2]) =>
get_fun_fun [get_fun_noexchange (negF flag) (rty,qty) lthy ty1, get_fun_noexchange flag (rty,qty) lthy ty2]
| Type (s, tys) => get_fun_aux s (map (get_fun_noexchange flag (rty, qty) lthy) tys)
| _ => raise ERROR ("no type variables"))
end
*}
ML {*
fun old_get_fun flag rty qty lthy ty =
get_fun_noexchange flag (rty, qty) lthy ty
*}
ML {*
fun find_matching_types rty ty =
let val (s, tys) = dest_Type ty in
if Type.raw_instance (Logic.varifyT ty, rty)
then [ty]
else flat (map (find_matching_types rty) tys)
end
*}
ML {*
fun get_fun_new 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
*}
(*
consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
axioms Rl_eq: "EQUIV Rl"
quotient ql = "'a list" / "Rl"
by (rule Rl_eq)
ML {* val al = snd (dest_Free (term_of @{cpat "f :: ?'a list"})) *}
ML {* val aq = snd (dest_Free (term_of @{cpat "f :: ?'a ql"})) *}
ML {* val ttt = term_of @{cterm "f :: bool list \<Rightarrow> nat list"} *}
ML {*
fst (get_fun_noexchange absF (al, aq) @{context} (fastype_of ttt))
*}
ML {*
fst (get_fun_new absF al aq @{context} (fastype_of ttt))
*}
ML {*
fun mk_abs tm =
let
val ty = fastype_of tm
in fst (get_fun_noexchange absF (al, aq) @{context} ty) $ tm end
fun mk_repabs tm =
let
val ty = fastype_of tm
in fst (get_fun_noexchange repF (al, aq) @{context} ty) $ (mk_abs tm) end
*}
ML {*
cterm_of @{theory} (mk_repabs ttt)
*}
*)
text {* Does the same as 'subst' in a given prop or theorem *}
ML {*
fun eqsubst_prop ctxt thms t =
let
val goalstate = Goal.init (cterm_of (ProofContext.theory_of ctxt) t)
val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
NONE => error "eqsubst_prop"
| SOME th => cprem_of th 1
in term_of a' end
*}
ML {*
fun repeat_eqsubst_prop ctxt thms t =
repeat_eqsubst_prop ctxt thms (eqsubst_prop ctxt thms t)
handle _ => t
*}
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 cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))
val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));
in
@{thm Pure.equal_elim_rule1} OF [rt,thm]
end
*}
ML {*
fun repeat_eqsubst_thm ctxt thms thm =
repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)
handle _ => thm
*}
ML {*
fun build_repabs_term lthy thm constructors rty qty =
let
val rty = Logic.varifyT rty;
val qty = Logic.varifyT qty;
fun mk_abs tm =
let
val ty = fastype_of tm
in fst (get_fun_noexchange absF (rty, qty) lthy ty) $ tm end
fun mk_repabs tm =
let
val ty = fastype_of tm
in fst (get_fun_noexchange repF (rty, qty) lthy ty) $ (mk_abs tm) end
fun is_constructor (Const (x, _)) = member (op =) constructors x
| is_constructor _ = false;
fun build_aux lthy tm =
case tm of
Abs (a as (_, vty, _)) =>
let
val (vs, t) = Term.dest_abs a;
val v = Free(vs, vty);
val t' = lambda v (build_aux lthy t)
in
if (not (needs_lift rty (fastype_of tm))) then t'
else mk_repabs (
if not (needs_lift rty vty) then t'
else
let
val v' = mk_repabs v;
val t1 = Envir.beta_norm (t' $ v')
in
lambda v t1
end
)
end
| x =>
let
val (opp, tms0) = Term.strip_comb tm
val tms = map (build_aux lthy) tms0
val ty = fastype_of tm
in
if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false)
then (list_comb (opp, (hd tms0) :: (tl tms)))
else if (is_constructor opp andalso needs_lift rty ty) then
mk_repabs (list_comb (opp,tms))
else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
mk_repabs(list_comb(opp,tms))
else if tms = [] then opp
else list_comb(opp, tms)
end
in
repeat_eqsubst_prop lthy @{thms id_def_sym}
(build_aux lthy (Thm.prop_of thm))
end
*}
text {* Assumes that it is given a regularized theorem *}
ML {*
fun build_repabs_goal ctxt thm cons rty qty =
Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))
*}
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 quotient_tac quot_thm =
REPEAT_ALL_NEW (FIRST' [
rtac @{thm FUN_QUOTIENT},
rtac quot_thm,
rtac @{thm IDENTITY_QUOTIENT},
(fn i => CHANGED (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I}) i) THEN rtac @{thm IDENTITY_QUOTIENT} i)
])
*}
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 {*
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 res_forall_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
let
val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _)) = term_of concl
in
((simp_tac ((Simplifier.context ctxt 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 ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1
end
handle _ => no_tac
)
*}
ML {*
val res_exists_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
let
val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _)) = term_of concl
in
((simp_tac ((Simplifier.context ctxt 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 ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1
end
handle _ => no_tac
)
*}
ML {*
fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
(FIRST' [
(* rtac @{thm FUN_QUOTIENT},
rtac quot_thm,
rtac @{thm IDENTITY_QUOTIENT},*)
rtac trans_thm,
LAMBDA_RES_TAC ctxt,
res_forall_rsp_tac ctxt,
res_exists_rsp_tac ctxt,
FIRST' (map rtac rsp_thms),
(instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
rtac refl,
(* rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*)
(APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
Cong_Tac.cong_tac @{thm cong},
rtac @{thm ext},
rtac reflex_thm,
atac,
(
(simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
THEN_ALL_NEW (fn _ => no_tac)
),
WEAK_LAMBDA_RES_TAC ctxt,
(fn i => CHANGED (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}) i))
])
*}
ML {*
fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
let
val rt = build_repabs_term lthy thm constructors rty qty;
val rg = Logic.mk_equals ((Thm.prop_of thm), rt);
fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
(REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));
val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
in
@{thm Pure.equal_elim_rule1} OF [cthm, thm]
end
*}
section {* Cleaning the goal *}
lemma prod_fun_id: "prod_fun id id = id"
apply (simp add: prod_fun_def)
done
lemma map_id: "map id x = x"
apply (induct x)
apply (simp_all add: map.simps)
done
ML {*
fun simp_ids lthy thm =
thm
|> MetaSimplifier.rewrite_rule @{thms id_def_sym}
|> repeat_eqsubst_thm lthy @{thms FUN_MAP_I id_apply prod_fun_id map_id}
*}
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
*}
ML {*
fun findabs_all rty tm =
case tm of
Abs(_, T, b) =>
let
val b' = subst_bound ((Free ("x", T)), b);
val tys = findabs_all rty b'
val ty = fastype_of tm
in if needs_lift rty ty then (ty :: tys) else tys
end
| f $ a => (findabs_all rty f) @ (findabs_all rty a)
| _ => [];
fun findabs rty tm = distinct (op =) (findabs_all rty tm)
*}
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 make_simp_prs_thm lthy quot_thm thm typ =
let
val (_, [lty, rty]) = dest_Type typ;
val thy = ProofContext.theory_of lthy;
val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
val inst = [SOME lcty, NONE, SOME rcty];
val lpi = Drule.instantiate' inst [] thm;
val tac =
(compose_tac (false, lpi, 2)) THEN_ALL_NEW
(quotient_tac quot_thm);
val gc = Drule.strip_imp_concl (cprop_of lpi);
val t = Goal.prove_internal [] gc (fn _ => tac 1)
in
MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t
end
*}
ML {*
fun findallex_all rty qty tm =
case tm of
Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) =>
let
val (tya, tye) = findallex_all rty qty s
in if needs_lift rty T then
((T :: tya), tye)
else (tya, tye) end
| Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) =>
let
val (tya, tye) = findallex_all rty qty s
in if needs_lift rty T then
(tya, (T :: tye))
else (tya, tye) end
| Abs(_, T, b) =>
findallex_all rty qty (subst_bound ((Free ("x", T)), b))
| f $ a =>
let
val (a1, e1) = findallex_all rty qty f;
val (a2, e2) = findallex_all rty qty a;
in (a1 @ a2, e1 @ e2) end
| _ => ([], []);
*}
ML {*
fun findallex lthy rty qty tm =
let
val (a, e) = findallex_all rty qty tm;
val (ad, ed) = (map domain_type a, map domain_type e);
val (au, eu) = (distinct (op =) ad, distinct (op =) ed);
val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty)
in
(map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu)
end
*}
ML {*
fun make_allex_prs_thm lthy quot_thm thm typ =
let
val (_, [lty, rty]) = dest_Type typ;
val thy = ProofContext.theory_of lthy;
val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
val inst = [NONE, SOME lcty];
val lpi = Drule.instantiate' inst [] thm;
val tac =
(compose_tac (false, lpi, 1)) THEN_ALL_NEW
(quotient_tac quot_thm);
val gc = Drule.strip_imp_concl (cprop_of lpi);
val t = Goal.prove_internal [] gc (fn _ => tac 1)
val t_noid = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t;
val t_sym = @{thm "HOL.sym"} OF [t_noid];
val t_eq = @{thm "eq_reflection"} OF [t_sym]
in
t_eq
end
*}
ML {*
fun applic_prs 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 fst (get_fun_noexchange repF (rty, qty) lthy ty) $ tm end;
fun mk_abs tm =
let
val ty = fastype_of tm
in fst (get_fun_noexchange 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 = (Simplifier.context lthy' 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 matches (ty1, ty2) =
Type.raw_instance (ty1, Logic.varifyT ty2);
fun lookup_quot_data lthy qty =
let
val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy)
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
*}
ML {*
fun lift_thm lthy qty qty_name rsp_thms defs t = let
val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;
val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;
val consts = lookup_quot_consts defs;
val t_a = atomize_thm t;
val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
val (alls, exs) = findallex lthy rty qty (prop_of t_a);
val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls
val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs
val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
val abs = findabs rty (prop_of t_a);
val aps = findaps rty (prop_of t_a);
val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;
val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
val defs_sym = flat (map (add_lower_defs lthy) defs);
val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;
val t_id = simp_ids lthy t_l;
val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;
val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
val t_rv = ObjectLogic.rulify t_r
in
Thm.varifyT t_rv
end
*}
ML {*
fun lift_thm_note qty qty_name rsp_thms defs thm name lthy =
let
val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm;
val (_, lthy2) = note (name, lifted_thm) lthy;
in
lthy2
end;
*}
end