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"+ −
+ −
+ −
+ −
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 abstractions:+ −
\<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 (* FIXME: t should be regularised too *)+ −
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+ −
*}+ −
+ −
(* For polymorphic types we need to find the type of the Relation term. *)+ −
(* TODO: we assume that the relation is a Constant. Is this always true? *)+ −
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 {*+ −
val r = Free ("R", dummyT);+ −
val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});+ −
val t2 = Syntax.check_term @{context} t;+ −
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:+ −
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: "a \<Longrightarrow> b \<longrightarrow> d"+ −
shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"+ −
using a b 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},+ −
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})+ −
]);+ −
val cthm = Goal.prove lthy [] [] goal+ −
(fn {context, ...} => tac context 1);+ −
in+ −
cthm OF [thm]+ −
end+ −
*}+ −
+ −
section {* RepAbs injection *}+ −
(*+ −
+ −
RepAbs injection is done in the following phases:+ −
1) build_repabs_term inserts rep-abs pairs in the term+ −
2) we prove the equality between the original theorem and this one+ −
3) we use Pure.equal_elim_rule1 to get the new theorem.+ −
+ −
build_repabs_term does:+ −
+ −
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.+ −
+ −
+ −
To prove that the old theorem implies the new one, 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+ −
+ −
*)+ −
+ −
+ −
(* 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 *)+ −
*}+ −
+ −
(*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 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+ −
+ −
(* returns all subterms where two types differ *)+ −
fun diff (T, S) Ds =+ −
case (T, S) of+ −
(TVar v, TVar u) => if v = u then Ds else (T, S)::Ds + −
| (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds+ −
| (Type (a, Ts), Type (b, Us)) => + −
if a = b then diffs (Ts, Us) Ds else (T, S)::Ds+ −
| _ => (T, S)::Ds+ −
and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds)+ −
| diffs ([], []) Ds = Ds+ −
| diffs _ _ = error "Unequal length of type arguments"+ −
+ −
*}+ −
+ −
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+ −
*}+ −
+ −
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 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+ −
*}+ −
+ −
ML {*+ −
fun repeat_eqsubst_thm ctxt thms thm =+ −
repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)+ −
handle _ => thm+ −
*}+ −
+ −
(* Needed 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}) *}+ −
+ −
ML {*+ −
fun build_repabs_term lthy thm consts rty qty =+ −
let+ −
(* TODO: The rty and qty stored in the quotient_info should+ −
be varified, so this will soon not be needed *)+ −
val rty = Logic.varifyT rty;+ −
val qty = Logic.varifyT qty;+ −
+ −
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+ −
fun mk_repabs tm =+ −
let+ −
val ty = fastype_of tm+ −
in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end+ −
+ −
fun is_lifted_const (Const (x, _)) = member (op =) consts x+ −
| is_lifted_const _ = 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;+ −
(* TODO: I believe 'beta' is not needed any more *)+ −
val t1 = (* Envir.beta_norm *) (t' $ v')+ −
in+ −
lambda v t1+ −
end)+ −
end+ −
| x =>+ −
case Term.strip_comb tm of+ −
(Const(@{const_name Respects}, _), _) => tm+ −
| (opp, tms0) =>+ −
let+ −
val tms = map (build_aux lthy) tms0+ −
val ty = fastype_of tm+ −
in+ −
if (is_lifted_const 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 {* Builds provable goals for regularized theorems *}+ −
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 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 FUN_MAP_I})) THEN'+ −
rtac @{thm IDENTITY_QUOTIENT}+ −
)+ −
])+ −
*}+ −
+ −
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 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,+ −
ball_rsp_tac ctxt,+ −
bex_rsp_tac ctxt,+ −
FIRST' (map rtac rsp_thms),+ −
(instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),+ −
rtac refl,+ −
(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,+ −
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}))+ −
])+ −
*}+ −
+ −
ML {*+ −
fun repabs lthy thm consts rty qty quot_thm reflex_thm trans_thm rsp_thms =+ −
let+ −
val rt = build_repabs_term lthy thm consts 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 \<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+ −
*}+ −
+ −
ML {*+ −
fun simp_ids_trm trm =+ −
trm |>+ −
MetaSimplifier.rewrite false @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}+ −
|> cprop_of |> Thm.dest_equals |> snd+ −
+ −
*}+ −
+ −
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+ −
*}+ −
+ −
(* TODO: Check if it behaves properly with varifyed rty *)+ −
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)+ −
*}+ −
+ −
(* Currently useful only for LAMBDA_PRS *)+ −
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 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 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+ −
*}+ −
+ −
+ −
ML {*+ −
fun lift_thm lthy qty qty_name rsp_thms defs rthm = + −
let+ −
val _ = tracing ("raw theorem:\n" ^ Syntax.string_of_term lthy (prop_of rthm))+ −
+ −
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 rthm;+ −
+ −
val _ = tracing ("raw atomized theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_a))+ −
+ −
val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;+ −
+ −
val _ = tracing ("regularised theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_r))+ −
+ −
val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;+ −
+ −
val _ = tracing ("rep/abs injected theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_t))+ −
+ −
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 _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_a))+ −
+ −
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 _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_l))+ −
+ −
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 _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_id))+ −
+ −
val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;+ −
+ −
val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d0))+ −
+ −
val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;+ −
+ −
val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d))+ −
+ −
val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;+ −
+ −
val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_r))+ −
+ −
val t_rv = ObjectLogic.rulify t_r+ −
+ −
val _ = tracing ("lifted theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_rv))+ −
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+ −
*}+ −
+ −
(******************************************)+ −
(******************************************)+ −
(* version with explicit qtrm *)+ −
(******************************************)+ −
(******************************************)+ −
+ −
ML {*+ −
fun atomize_goal thy gl =+ −
let+ −
val vars = map Free (Term.add_frees gl []);+ −
val all = if fastype_of gl = @{typ bool} then HOLogic.all_const else Term.all;+ −
fun lambda_all (var as Free(_, T)) trm = (all T) $ lambda var trm;+ −
val glv = fold lambda_all vars gl+ −
val gla = (term_of o snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glv))+ −
val glf = Type.legacy_freeze gla+ −
in+ −
if fastype_of gl = @{typ bool} then @{term Trueprop} $ glf else glf+ −
end+ −
*}+ −
+ −
+ −
ML {* atomize_goal @{theory} @{term "x memb [] = False"} *}+ −
ML {* atomize_goal @{theory} @{term "x = xa \<Longrightarrow> a # x = a # xa"} *}+ −
+ −
+ −
ML {*+ −
(* builds the relation for 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 {*+ −
fun trm_lift_error lthy rtrm qtrm =+ −
let+ −
val rtrm_str = quote (Syntax.string_of_term lthy rtrm) + −
val qtrm_str = quote (Syntax.string_of_term lthy qtrm)+ −
val msg = ["The quotient theorem", qtrm_str, "and lifted theorem", rtrm_str, "do not match."]+ −
in+ −
raise LIFT_MATCH (space_implode " " msg)+ −
end + −
*}+ −
+ −
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) + −
*}+ −
+ −
(*+ −
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 {*+ −
(* 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 trm_lift_error lthy rtrm qtrm+ −
| (Bound i, Bound i') =>+ −
if i = i' + −
then rtrm + −
else trm_lift_error lthy rtrm qtrm+ −
| (Const (s, ty), Const (s', ty')) =>+ −
if s = s' andalso ty = ty'+ −
then rtrm+ −
else rtrm (* FIXME: check correspondence according to definitions *) + −
| _ => trm_lift_error lthy rtrm qtrm+ −
*}+ −
+ −
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 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+ −
+ −
*)+ −
+ −
lemma my_equiv_res_forall2:+ −
fixes P::"'a \<Rightarrow> bool"+ −
fixes Q::"'b \<Rightarrow> bool"+ −
assumes a: "(All Q) \<longrightarrow> (All P)"+ −
shows "(All Q) \<longrightarrow> Ball (Respects E) P"+ −
using a by auto+ −
+ −
lemma my_equiv_res_exists:+ −
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"+ −
apply(subst equiv_res_exists)+ −
apply(rule a)+ −
apply(rule b)+ −
done+ −
+ −
ML {*+ −
(* FIXME: get_rid of rel_refl rel_eqv *)+ −
fun REGULARIZE_tac lthy rel_refl rel_eqv =+ −
(REPEAT1 o FIRST1) + −
[rtac rel_refl,+ −
atac,+ −
rtac @{thm universal_twice},+ −
rtac @{thm impI} THEN' atac,+ −
rtac @{thm implication_twice},+ −
rtac @{thm my_equiv_res_forall2},+ −
rtac (rel_eqv RS @{thm my_equiv_res_exists}),+ −
(* 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}]+ −
*}+ −
+ −
(* 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_forall2}),+ −
DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_exists})),+ −
(* 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_prove rtrm qtrm rel_eqv rel_refl lthy =+ −
let+ −
val goal = mk_REGULARIZE_goal lthy rtrm qtrm+ −
in+ −
Goal.prove lthy [] [] goal + −
(fn {context, ...} => REGULARIZE_tac' context rel_refl rel_eqv)+ −
end+ −
*}+ −
+ −
(* rep-abs injection *)+ −
+ −
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')) + −
| _ => trm_lift_error lthy rtrm qtrm+ −
end+ −
end+ −
*}+ −
+ −
ML {*+ −
fun mk_inj_REPABS_goal lthy (rtrm, qtrm) =+ −
Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm)))+ −
*}+ −
+ −
(* Final wrappers *)+ −
+ −
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_goal lthy thm rel_eqv rel_refl qtrm =+ −
let+ −
val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm;+ −
fun tac lthy = regularize_tac lthy rel_eqv rel_refl;+ −
val cthm = Goal.prove lthy [] [] reg_trm+ −
(fn {context, ...} => tac context 1);+ −
in+ −
cthm OF [thm]+ −
end+ −
*}+ −
+ −
ML {*+ −
fun repabs_goal lthy thm rty quot_thm reflex_thm trans_thm rsp_thms qtrm =+ −
let+ −
val rg = Syntax.check_term lthy (mk_inj_REPABS_goal lthy ((prop_of thm), qtrm));+ −
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+ −
*}+ −
+ −
ML {*+ −
fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal =+ −
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 t_a = atomize_thm rthm;+ −
val goal_a = atomize_goal (ProofContext.theory_of lthy) goal;+ −
val t_r = regularize_goal lthy t_a rel_eqv rel_refl goal_a;+ −
val t_t = repabs_goal lthy t_r rty quot rel_refl trans2 rsp_thms goal_a;+ −
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_goal_note lthy qty qty_name rsp_thms defs thm name goal =+ −
let+ −
val lifted_thm = lift_thm_goal lthy qty qty_name rsp_thms defs thm goal;+ −
val (_, lthy2) = note (name, lifted_thm) lthy;+ −
in+ −
lthy2+ −
end+ −
*}+ −
+ −
+ −
end+ −
+ −
+ −