theory QuotMain+ −
imports QuotScript QuotList Prove+ −
uses ("quotient.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 *}+ −
+ −
use "quotient.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" *}+ −
+ −
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 {* lifting of constants *}+ −
+ −
ML {*+ −
(* whether ty1 is an instance of ty2 *)+ −
fun matches (ty1, ty2) =+ −
Type.raw_instance (ty1, Logic.varifyT ty2)+ −
+ −
fun lookup_snd _ [] _ = NONE+ −
| lookup_snd eq ((value, key)::xs) key' =+ −
if eq (key', key) then SOME value+ −
else lookup_snd eq xs key';+ −
+ −
fun lookup_qenv qenv qty =+ −
(case (AList.lookup matches qenv qty) of+ −
SOME rty => SOME (qty, rty)+ −
| NONE => NONE)+ −
*}+ −
+ −
ML {*+ −
(* calculates the aggregate abs and rep functions for a given type; + −
repF is for constants' arguments; absF is for constants;+ −
function types need to be treated specially, since repF and absF+ −
change+ −
*)+ −
datatype flag = absF | repF+ −
+ −
fun negF absF = repF+ −
| negF repF = absF+ −
+ −
fun get_fun flag qenv 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 => raise 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+ −
+ −
fun get_const flag (qty, rty) =+ −
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), 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 (AList.defined matches qenv ty)+ −
then (get_const flag (the (lookup_qenv qenv 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 (negF flag) qenv lthy ty1, get_fun flag qenv lthy ty2]+ −
| Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)+ −
| _ => raise ERROR ("no type variables")+ −
)+ −
end+ −
*}+ −
+ −
+ −
text {* produces the definition for a lifted constant *}+ −
+ −
ML {*+ −
fun get_const_def nconst otrm qenv lthy =+ −
let+ −
val ty = fastype_of nconst+ −
val (arg_tys, res_ty) = strip_type ty+ −
+ −
val rep_fns = map (fst o get_fun repF qenv lthy) arg_tys+ −
val abs_fn = (fst o get_fun absF qenv lthy) res_ty+ −
+ −
fun mk_fun_map (t1,t2) = Const (@{const_name "fun_map"}, dummyT) $ t1 $ t2+ −
+ −
val fns = Library.foldr mk_fun_map (rep_fns, abs_fn)+ −
|> Syntax.check_term lthy+ −
in+ −
fns $ otrm+ −
end+ −
*}+ −
+ −
ML {* lookup_snd *}+ −
+ −
ML {*+ −
fun exchange_ty qenv ty =+ −
case (lookup_snd matches qenv ty) of+ −
SOME qty => qty+ −
| NONE =>+ −
(case ty of+ −
Type (s, tys) => Type (s, map (exchange_ty qenv) tys)+ −
| _ => ty+ −
)+ −
*}+ −
+ −
ML {*+ −
fun make_const_def nconst_bname otrm mx qenv lthy =+ −
let+ −
val otrm_ty = fastype_of otrm+ −
val nconst_ty = exchange_ty qenv otrm_ty+ −
val nconst = Const (Binding.name_of nconst_bname, nconst_ty)+ −
val def_trm = get_const_def nconst otrm qenv lthy+ −
in+ −
define (nconst_bname, mx, def_trm) lthy+ −
end+ −
*}+ −
+ −
ML {*+ −
fun build_qenv lthy qtys = + −
let+ −
val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy)+ −
+ −
fun find_assoc qty =+ −
case (AList.lookup matches qenv qty) of+ −
SOME rty => (qty, rty)+ −
| NONE => error (implode + −
["Quotient type ", + −
quote (Syntax.string_of_typ lthy qty), + −
" does not exists"])+ −
in+ −
map find_assoc qtys+ −
end+ −
*}+ −
+ −
ML {*+ −
(* taken from isar_syn.ML *)+ −
val constdecl =+ −
OuterParse.binding --+ −
(OuterParse.where_ >> K (NONE, NoSyn) ||+ −
OuterParse.$$$ "::" |-- OuterParse.!!! ((OuterParse.typ >> SOME) -- + −
OuterParse.opt_mixfix' --| OuterParse.where_) ||+ −
Scan.ahead (OuterParse.$$$ "(") |-- + −
OuterParse.!!! (OuterParse.mixfix' --| OuterParse.where_ >> pair NONE))+ −
*}+ −
+ −
ML {*+ −
val qd_parser = + −
(Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) --+ −
(constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop))+ −
*}+ −
+ −
ML {* + −
fun pair lthy (ty1, ty2) =+ −
"(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")"+ −
*}+ −
+ −
ML {*+ −
fun parse_qd_spec (qtystrs, ((bind, (typstr__, mx)), (attr__, propstr))) lthy = + −
let+ −
val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystrs+ −
val qenv = build_qenv lthy qtys+ −
val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy+ −
val (lhs, rhs) = Logic.dest_equals prop+ −
in+ −
make_const_def bind rhs mx qenv lthy |> snd+ −
end+ −
*}+ −
+ −
ML {*+ −
val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"+ −
OuterKeyword.thy_decl (qd_parser >> parse_qd_spec)+ −
*}+ −
+ −
section {* ATOMIZE *}+ −
+ −
text {*+ −
Unabs_def converts a definition given as+ −
+ −
c \<equiv> %x. %y. f x y+ −
+ −
to a theorem of the form+ −
+ −
c x y \<equiv> f x y+ −
+ −
This function is needed to rewrite the right-hand+ −
side to the left-hand side.+ −
*}+ −
+ −
ML {*+ −
fun unabs_def ctxt def =+ −
let+ −
val (lhs, rhs) = Thm.dest_equals (cprop_of def)+ −
val xs = strip_abs_vars (term_of rhs)+ −
val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt+ −
+ −
val thy = ProofContext.theory_of ctxt'+ −
val cxs = map (cterm_of thy o Free) xs+ −
val new_lhs = Drule.list_comb (lhs, cxs)+ −
+ −
fun get_conv [] = Conv.rewr_conv def+ −
| get_conv (x::xs) = Conv.fun_conv (get_conv xs)+ −
in+ −
get_conv xs new_lhs |>+ −
singleton (ProofContext.export ctxt' ctxt)+ −
end+ −
*}+ −
+ −
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 *}+ −
+ −
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 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)+ −
*}+ −
+ −
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 {*+ −
(* trm \<Rightarrow> new_trm *)+ −
fun regularise trm rty rel lthy =+ −
case trm of+ −
Abs (x, T, t) =>+ −
if (needs_lift rty T) then let+ −
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;+ −
val v = Free (x', T);+ −
val t' = subst_bound (v, t);+ −
val rec_term = regularise t' rty rel lthy2;+ −
val lam_term = Term.lambda_name (x, v) rec_term;+ −
val sub_res_term = tyRel T rty rel lthy;+ −
val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});+ −
val res_term = respects $ sub_res_term;+ −
val ty = fastype_of trm;+ −
val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty);+ −
val rabs_term = (rabs $ res_term) $ lam_term;+ −
in+ −
rabs_term+ −
end else let+ −
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;+ −
val v = Free (x', T);+ −
val t' = subst_bound (v, t);+ −
val rec_term = regularise t' rty rel lthy2;+ −
in+ −
Term.lambda_name (x, v) rec_term+ −
end+ −
| ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) =>+ −
if (needs_lift rty T) then let+ −
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;+ −
val v = Free (x', T);+ −
val t' = subst_bound (v, t);+ −
val rec_term = regularise t' rty rel lthy2;+ −
val lam_term = Term.lambda_name (x, v) rec_term;+ −
val sub_res_term = tyRel T rty rel lthy;+ −
val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});+ −
val res_term = respects $ sub_res_term;+ −
val ty = fastype_of lam_term;+ −
val rall = Const (@{const_name Ball}, (fastype_of res_term) --> ty --> @{typ bool});+ −
val rall_term = (rall $ res_term) $ lam_term;+ −
in+ −
rall_term+ −
end else let+ −
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;+ −
val v = Free (x', T);+ −
val t' = subst_bound (v, t);+ −
val rec_term = regularise t' rty rel lthy2;+ −
val lam_term = Term.lambda_name (x, v) rec_term+ −
in+ −
Const(@{const_name "All"}, at) $ lam_term+ −
end+ −
| ((Const (@{const_name "All"}, at)) $ P) =>+ −
let+ −
val (_, [al, _]) = dest_Type (fastype_of P);+ −
val ([x], lthy2) = Variable.variant_fixes [""] lthy;+ −
val v = (Free (x, al));+ −
val abs = Term.lambda_name (x, v) (P $ v);+ −
in regularise ((Const (@{const_name "All"}, at)) $ abs) rty rel lthy2 end+ −
| ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) =>+ −
if (needs_lift rty T) then let+ −
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;+ −
val v = Free (x', T);+ −
val t' = subst_bound (v, t);+ −
val rec_term = regularise t' rty rel lthy2;+ −
val lam_term = Term.lambda_name (x, v) rec_term;+ −
val sub_res_term = tyRel T rty rel lthy;+ −
val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});+ −
val res_term = respects $ sub_res_term;+ −
val ty = fastype_of lam_term;+ −
val rall = Const (@{const_name Bex}, (fastype_of res_term) --> ty --> @{typ bool});+ −
val rall_term = (rall $ res_term) $ lam_term;+ −
in+ −
rall_term+ −
end else let+ −
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;+ −
val v = Free (x', T);+ −
val t' = subst_bound (v, t);+ −
val rec_term = regularise t' rty rel lthy2;+ −
val lam_term = Term.lambda_name (x, v) rec_term+ −
in+ −
Const(@{const_name "Ex"}, at) $ lam_term+ −
end+ −
| ((Const (@{const_name "Ex"}, at)) $ P) =>+ −
let+ −
val (_, [al, _]) = dest_Type (fastype_of P);+ −
val ([x], lthy2) = Variable.variant_fixes [""] lthy;+ −
val v = (Free (x, al));+ −
val abs = Term.lambda_name (x, v) (P $ v);+ −
in regularise ((Const (@{const_name "Ex"}, at)) $ abs) rty rel lthy2 end+ −
| a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy)+ −
| _ => trm+ −
+ −
*}+ −
+ −
(* my version of regularise *)+ −
(****************************)+ −
+ −
(* some helper functions *)+ −
+ −
+ −
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: assumes always the typ is qty! *)+ −
(* FIXME: if there are more than one quotient, then you have to look up the relation *)+ −
ML {*+ −
fun my_reg rel trm =+ −
case trm of+ −
Abs (x, T, t) =>+ −
let + −
val ty1 = fastype_of trm+ −
in+ −
(mk_babs ty1 T) $ (mk_resp T $ rel) $ (apply_subt (my_reg rel) trm) + −
end+ −
| Const (@{const_name "All"}, ty) $ t =>+ −
let + −
val ty1 = domain_type ty+ −
val ty2 = domain_type ty1+ −
in+ −
(mk_ball ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t) + −
end+ −
| Const (@{const_name "Ex"}, ty) $ t =>+ −
let + −
val ty1 = domain_type ty+ −
val ty2 = domain_type ty1+ −
in+ −
(mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t) + −
end+ −
| t1 $ t2 => (my_reg rel t1) $ (my_reg rel t2)+ −
| _ => trm+ −
*}+ −
+ −
+ −
(*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)+ −
trm == new_trm+ −
*)+ −
+ −
text {* Assumes that the given theorem is atomized *}+ −
ML {*+ −
fun build_regularize_goal thm rty rel lthy =+ −
Logic.mk_implies+ −
((prop_of thm),+ −
(regularise (prop_of thm) rty rel lthy))+ −
*}+ −
+ −
ML {*+ −
fun regularize thm rty rel rel_eqv lthy =+ −
let+ −
val g = build_regularize_goal thm rty rel lthy;+ −
fun tac ctxt =+ −
(asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps+ −
[(@{thm equiv_res_forall} OF [rel_eqv]),+ −
(@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW+ −
(((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'+ −
(MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt []));+ −
val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 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)+ −
+ −
ML {*+ −
fun old_exchange_ty rty qty ty =+ −
if ty = rty+ −
then qty+ −
else+ −
(case ty of+ −
Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys)+ −
| _ => ty+ −
)+ −
*}+ −
+ −
ML {*+ −
fun old_get_fun flag rty qty lthy ty =+ −
get_fun flag [(qty, rty)] lthy ty + −
+ −
fun old_make_const_def nconst_bname otrm mx rty qty lthy =+ −
make_const_def nconst_bname otrm mx [(qty, rty)] lthy+ −
*}+ −
+ −
ML {*+ −
fun build_repabs_term lthy thm constructors rty qty =+ −
let+ −
fun mk_rep tm =+ −
let+ −
val ty = old_exchange_ty rty qty (fastype_of tm)+ −
in fst (old_get_fun repF rty qty lthy ty) $ tm end+ −
+ −
fun mk_abs tm =+ −
let+ −
val ty = old_exchange_ty rty qty (fastype_of tm) in+ −
fst (old_get_fun absF rty qty lthy ty) $ 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_rep (mk_abs (+ −
if not (needs_lift rty vty) then t'+ −
else+ −
let+ −
val v' = mk_rep (mk_abs 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_rep (mk_abs (list_comb (opp,tms)))+ −
else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then+ −
mk_rep(mk_abs(list_comb(opp,tms)))+ −
else if tms = [] then opp+ −
else list_comb(opp, tms)+ −
end+ −
in+ −
MetaSimplifier.rewrite_term @{theory} @{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 res_forall_rsp_tac ctxt =+ −
(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}))+ −
*}+ −
+ −
ML {*+ −
fun res_exists_rsp_tac ctxt =+ −
(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}))+ −
*}+ −
+ −
+ −
ML {*+ −
fun quotient_tac quot_thm =+ −
REPEAT_ALL_NEW (FIRST' [+ −
rtac @{thm FUN_QUOTIENT},+ −
rtac quot_thm,+ −
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 {*+ −
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,+ −
(+ −
(simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms))+ −
THEN_ALL_NEW (fn _ => no_tac)+ −
),+ −
(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+ −
])+ −
*}+ −
+ −
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 *}+ −
+ −
text {* Does the same as 'subst' in a given theorem *}+ −
ML {*+ −
fun eqsubst_thm ctxt thms thm =+ −
let+ −
val goalstate = Goal.init (Thm.cprop_of thm)+ −
val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of+ −
NONE => error "eqsubst_thm"+ −
| SOME th => cprem_of th 1+ −
val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1+ −
val 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+ −
*}+ −
+ −
text {* expects atomized definition *}+ −
ML {*+ −
fun add_lower_defs_aux ctxt thm =+ −
let+ −
val e1 = @{thm fun_cong} OF [thm];+ −
val f = eqsubst_thm ctxt @{thms fun_map.simps} e1;+ −
val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f;+ −
val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I} g;+ −
val i = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] h+ −
in+ −
thm :: (add_lower_defs_aux ctxt i)+ −
end+ −
handle _ => [thm]+ −
*}+ −
+ −
ML {*+ −
fun add_lower_defs ctxt defs =+ −
let+ −
val defs_pre_sym = map symmetric defs+ −
val defs_atom = map atomize_thm defs_pre_sym+ −
val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom)+ −
in+ −
map Thm.varifyT defs_all+ −
end+ −
*}+ −
+ −
text {* the proper way to do it *}+ −
ML {*+ −
fun findabs rty tm =+ −
case tm of+ −
Abs(_, T, b) =>+ −
let+ −
val b' = subst_bound ((Free ("x", T)), b);+ −
val tys = findabs rty b'+ −
val ty = fastype_of tm+ −
in if needs_lift rty ty then (ty :: tys) else tys+ −
end+ −
| f $ a => (findabs rty f) @ (findabs rty a)+ −
| _ => []+ −
*}+ −
+ −
ML {*+ −
fun make_simp_lam_prs_thm lthy quot_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 LAMBDA_PRS};+ −
val tac =+ −
(compose_tac (false, @{thm LAMBDA_PRS}, 2)) THEN_ALL_NEW+ −
(quotient_tac quot_thm);+ −
val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1);+ −
val ts = @{thm HOL.sym} OF [t]+ −
in+ −
MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] ts+ −
end+ −
*}+ −
+ −
ML {*+ −
fun simp_allex_prs lthy quot thm =+ −
let+ −
val rwf = @{thm FORALL_PRS} OF [quot];+ −
val rwfs = @{thm "HOL.sym"} OF [rwf];+ −
val rwe = @{thm EXISTS_PRS} OF [quot];+ −
val rwes = @{thm "HOL.sym"} OF [rwe]+ −
in+ −
(simp_allex_prs lthy quot (eqsubst_thm lthy [rwfs, rwes] thm))+ −
end+ −
handle _ => thm+ −
*}+ −
+ −
ML {*+ −
fun lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t = let+ −
val t_a = atomize_thm t;+ −
val t_r = regularize t_a rty rel rel_eqv lthy;+ −
val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;+ −
val abs = findabs rty (prop_of t_a);+ −
val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs;+ −
val t_l = repeat_eqsubst_thm lthy simp_lam_prs_thms t_t;+ −
val t_a = simp_allex_prs lthy quot t_l;+ −
val t_defs_sym = add_lower_defs lthy t_defs;+ −
val t_d = repeat_eqsubst_thm lthy t_defs_sym t_a;+ −
val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;+ −
in+ −
ObjectLogic.rulify t_r+ −
end+ −
*}+ −
+ −
end+ −