theory QuotMain+ −
imports QuotScript QuotList Prove+ −
uses ("quotient_info.ML") + −
("quotient.ML")+ −
begin+ −
+ −
ML {* Attrib.empty_binding *}+ −
+ −
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_info.ML"+ −
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 {*+ −
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 (op =) 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 (op =) 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 {*+ −
fun exchange_ty qenv ty =+ −
case (lookup_snd (op =) qenv ty) of+ −
SOME qty => qty+ −
| NONE =>+ −
(case ty of+ −
Type (s, tys) => Type (s, map (exchange_ty qenv) tys)+ −
| _ => ty+ −
)+ −
*}+ −
+ −
ML {* + −
fun ppair lthy (ty1, ty2) =+ −
"(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")"+ −
*}+ −
+ −
ML {*+ −
fun print_env qenv lthy =+ −
map (ppair lthy) qenv+ −
|> commas+ −
|> tracing+ −
*}+ −
+ −
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+ −
+ −
val _ = print_env qenv lthy+ −
val _ = Syntax.string_of_typ lthy otrm_ty |> tracing+ −
val _ = Syntax.string_of_typ lthy nconst_ty |> tracing+ −
val _ = Syntax.string_of_term lthy def_trm |> tracing+ −
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)+ −
val thy = ProofContext.theory_of lthy+ −
+ −
fun find_assoc ((qty', rty')::rest) qty =+ −
let + −
val inst = Sign.typ_match thy (qty', qty) Vartab.empty+ −
in+ −
(Envir.norm_type inst qty, Envir.norm_type inst rty')+ −
end+ −
| find_assoc [] qty =+ −
let + −
val qtystr = quote (Syntax.string_of_typ lthy qty)+ −
in+ −
error (implode ["Quotient type ", qtystr, " does not exists"])+ −
end+ −
in+ −
map (find_assoc qenv) qtys+ −
end+ −
*}+ −
+ −
+ −
ML {*+ −
fun quotdef_cmd qenv ((bind, qty_, mx), (attr, prop)) lthy =+ −
let + −
val (lhs_, rhs) = Logic.dest_equals prop+ −
in+ −
make_const_def bind rhs mx qenv lthy+ −
end+ −
*}+ −
+ −
ML {*+ −
val quotdef_parser = + −
Scan.option (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) --+ −
(SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- + −
OuterParse.prop)) >> OuterParse.triple2+ −
*}+ −
+ −
ML {*+ −
fun quotdef (qtystrs, (bind, tystr, mx), (attr, propstr)) lthy = + −
let+ −
val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) (the qtystrs)+ −
val qenv = build_qenv lthy qtys+ −
val qty = Option.map (Syntax.check_typ lthy o Syntax.parse_typ lthy) tystr+ −
val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy+ −
in+ −
quotdef_cmd qenv ((bind, qty, mx), (attr, prop)) lthy |> snd+ −
end+ −
*}+ −
+ −
ML {*+ −
val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"+ −
OuterKeyword.thy_decl (quotdef_parser >> quotdef)+ −
*}+ −
+ −
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 matches (ty1, ty2) =+ −
Type.raw_instance (ty1, Logic.varifyT ty2);+ −
+ −
fun tyRel ty rty rel lthy =+ −
if matches (rty, ty)+ −
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 {*+ −
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+ −
*}+ −
+ −
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 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 g = 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 (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),+ −
(rtac @{thm RIGHT_RES_FORALL_REGULAR})+ −
]);+ −
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+ −
*}+ −
+ −
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+ −
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+ −
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}+ −
])+ −
*}+ −
+ −
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+ −
])+ −
*}+ −
+ −
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+ −
+ −
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 id_apply prod_fun_id map_id} g+ −
in+ −
thm :: (add_lower_defs_aux ctxt h)+ −
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+ −
*}+ −
+ −
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 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)+ −
in+ −
(map (old_exchange_ty rty qty) au, map (old_exchange_ty 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+ −
fun absty ty =+ −
old_exchange_ty rty qty ty+ −
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;+ −
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 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 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 = add_lower_defs lthy defs;+ −
val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;+ −
val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l;+ −
val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;+ −
val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;+ −
in+ −
ObjectLogic.rulify t_r+ −
end+ −
*}+ −
+ −
+ −
end+ −
+ −