File ‹nominal_thmdecls.ML›
signature NOMINAL_THMDECLS =
sig
val nominal_eqvt_debug: bool Config.T
val eqvt_add: attribute
val eqvt_del: attribute
val eqvt_force_add: attribute
val eqvt_force_del: attribute
val setup: theory -> theory
val get_eqvt_thms: Proof.context -> thm list
end;
structure NominalThmDecls: NOMINAL_THMDECLS =
struct
structure Data = Generic_Data
(
type T = thm list
val empty = []
val merge = Thm.merge_thms
)
exception EQVT_FORM of string
val nominal_eqvt_debug = Attrib.setup_config_bool \<^binding>‹nominal_eqvt_debug› (K false);
fun tactic ctxt (msg, tac) =
if Config.get ctxt nominal_eqvt_debug
then tac THEN' (K (print_tac ctxt ("after " ^ msg)))
else tac
fun prove_eqvt_tac ctxt orig_thm pi pi' =
let
val thy = Proof_Context.theory_of ctxt
val T = fastype_of pi'
val mypifree = Thm.cterm_of ctxt (Const (\<^const_name>‹rev›, T --> T) $ pi')
val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"
in
EVERY1 [tactic ctxt ("iffI applied", resolve_tac ctxt @{thms iffI}),
tactic ctxt ("remove pi with perm_boolE", dresolve_tac ctxt @{thms perm_boolE}),
tactic ctxt ("solve with orig_thm", eresolve_tac ctxt [orig_thm]),
tactic ctxt ("applies orig_thm instantiated with rev pi",
dresolve_tac ctxt [infer_instantiate ctxt [(#1 (dest_Var pi), mypifree)] orig_thm]),
tactic ctxt ("getting rid of the pi on the right", resolve_tac ctxt @{thms perm_boolI}),
tactic ctxt ("getting rid of all remaining perms",
full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps perm_pi_simp))]
end;
fun get_derived_thm ctxt hyp concl orig_thm pi typi =
let
val pi' = Var (pi, typi);
val lhs = Const (\<^const_name>‹perm›, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
val ([goal_term, pi''], ctxt') = Variable.import_terms false
[HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt
val _ = writeln (Syntax.string_of_term ctxt' goal_term);
in
Goal.prove ctxt' [] [] goal_term
(fn _ => prove_eqvt_tac ctxt' orig_thm pi' pi'') |>
singleton (Proof_Context.export ctxt' ctxt)
end
fun apply_pi trm (pi, typi) =
let
fun replace n ty =
let
val c = Const (\<^const_name>‹perm›, typi --> ty --> ty)
val v1 = Var (pi, typi)
val v2 = Var (n, ty)
in
c $ v1 $ v2
end
in
map_aterms (fn Var (n, ty) => replace n ty | t => t) trm
end
fun get_pi t thy =
let fun get_pi_aux s =
(case s of
(Const (\<^const_name>‹perm› ,typrm) $
(Var (pi,typi as Type(\<^type_name>‹list›, [Type (\<^type_name>‹Product_Type.prod›, [Type (tyatm,[]),_])]))) $
(Var (n,ty))) =>
let
val class_name = (Long_Name.map_base_name (fn s => "pt_"^s) tyatm)
in
if (Sign.of_sort thy (ty,[class_name]))
then [(pi,typi)]
else raise
EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name)
end
| Abs (_,_,t1) => get_pi_aux t1
| (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2
| _ => [])
in
(case (distinct (op =) (get_pi_aux t)) of
[(pi,typi)] => (pi, typi)
| _ => raise EQVT_FORM "All permutation should be the same")
end;
fun eqvt_add_del_aux flag orig_thm context =
let
val thy = Context.theory_of context
val thms_to_be_added =
(case Thm.prop_of orig_thm of
(Const(\<^const_name>‹Pure.imp›, _) $ (Const (\<^const_name>‹Trueprop›,_) $ hyp) $ (Const (\<^const_name>‹Trueprop›,_) $ concl)) =>
let
val (pi,typi) = get_pi concl thy
in
if (apply_pi hyp (pi,typi) = concl)
then
(warning ("equivariance lemma of the relational form");
[orig_thm,
get_derived_thm (Context.proof_of context) hyp concl orig_thm pi typi])
else raise EQVT_FORM "Type Implication"
end
| (Const (\<^const_name>‹Trueprop›, _) $ (Const (\<^const_name>‹HOL.eq›, _) $
(Const (\<^const_name>‹perm›,typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
(if (apply_pi lhs (pi,typi)) = rhs
then [orig_thm]
else raise EQVT_FORM "Type Equality")
| _ => raise EQVT_FORM "Type unknown")
in
fold (fn thm => Data.map (flag thm)) thms_to_be_added context
end
handle EQVT_FORM s =>
error (Thm.string_of_thm (Context.proof_of context) orig_thm ^
" does not comply with the form of an equivariance lemma (" ^ s ^").")
val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (Thm.add_thm));
val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (Thm.del_thm));
val eqvt_force_add = Thm.declaration_attribute (Data.map o Thm.add_thm);
val eqvt_force_del = Thm.declaration_attribute (Data.map o Thm.del_thm);
val get_eqvt_thms = Context.Proof #> Data.get;
val setup =
Attrib.setup \<^binding>‹eqvt› (Attrib.add_del eqvt_add eqvt_del)
"equivariance theorem declaration" #>
Attrib.setup \<^binding>‹eqvt_force› (Attrib.add_del eqvt_force_add eqvt_force_del)
"equivariance theorem declaration (without checking the form of the lemma)" #>
Global_Theory.add_thms_dynamic (\<^binding>‹eqvts›, Data.get);
end;