(* Title: nominal_thmdecls.ML+ −
Author: Christian Urban+ −
+ −
Infrastructure for the lemma collection "eqvts".+ −
+ −
Provides the attributes [eqvt] and [eqvt_raw], and the theorem+ −
lists eqvts and eqvts_raw. The first attribute will store the + −
theorem in the eqvts list and also in the eqvts_raw list. For + −
the latter the theorem is expected to be of the form+ −
+ −
p o (c x1 x2 ...) = c (p o x1) (p o x2) ...+ −
+ −
and it is stored in the form+ −
+ −
p o c == c+ −
+ −
The [eqvt_raw] attribute just adds the theorem to eqvts_raw.+ −
+ −
TODO:+ −
+ −
- deal with eqvt-lemmas of the form + −
+ −
c x1 x2 ... ==> c (p o x1) (p o x2) ..+ −
*)+ −
+ −
signature NOMINAL_THMDECLS =+ −
sig+ −
val eqvt_add: attribute+ −
val eqvt_del: attribute+ −
val eqvt_raw_add: attribute+ −
val eqvt_raw_del: attribute+ −
val setup: theory -> theory+ −
val get_eqvts_thms: Proof.context -> thm list+ −
val get_eqvts_raw_thms: Proof.context -> thm list+ −
+ −
end;+ −
+ −
structure Nominal_ThmDecls: NOMINAL_THMDECLS =+ −
struct+ −
+ −
+ −
structure EqvtData = Generic_Data+ −
( type T = thm Item_Net.T;+ −
val empty = Thm.full_rules;+ −
val extend = I;+ −
val merge = Item_Net.merge );+ −
+ −
structure EqvtRawData = Generic_Data+ −
( type T = thm Item_Net.T;+ −
val empty = Thm.full_rules;+ −
val extend = I;+ −
val merge = Item_Net.merge );+ −
+ −
val eqvts = Item_Net.content o EqvtData.get;+ −
val eqvts_raw = Item_Net.content o EqvtRawData.get;+ −
+ −
val get_eqvts_thms = eqvts o Context.Proof; + −
val get_eqvts_raw_thms = eqvts_raw o Context.Proof; + −
+ −
val add_thm = EqvtData.map o Item_Net.update;+ −
val del_thm = EqvtData.map o Item_Net.remove;+ −
+ −
val add_raw_thm = EqvtRawData.map o Item_Net.update;+ −
val del_raw_thm = EqvtRawData.map o Item_Net.remove;+ −
+ −
fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)+ −
| dest_perm t = raise TERM("dest_perm", [t])+ −
+ −
fun mk_perm p trm =+ −
let+ −
val ty = fastype_of trm+ −
in+ −
Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm+ −
end+ −
+ −
fun eqvt_transform_tac thm = REPEAT o FIRST' + −
[CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}),+ −
rtac (thm RS @{thm trans}),+ −
rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]+ −
+ −
(* transform equations into the required form *)+ −
fun transform_eq ctxt thm lhs rhs = + −
let+ −
val (p, t) = dest_perm lhs+ −
val (c, args) = strip_comb t+ −
val (c', args') = strip_comb rhs + −
val eargs = map Envir.eta_contract args + −
val eargs' = map Envir.eta_contract args'+ −
val p_str = fst (fst (dest_Var p))+ −
val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c))+ −
in+ −
if c <> c' + −
then error "eqvt lemma is not of the right form (constants do not agree)"+ −
else if eargs' <> map (mk_perm p) eargs + −
then error "eqvt lemma is not of the right form (arguments do not agree)"+ −
else if args = [] + −
then thm+ −
else Goal.prove ctxt [p_str] [] goal+ −
(fn _ => eqvt_transform_tac thm 1)+ −
end+ −
+ −
fun transform addel_fun thm context = + −
let+ −
val ctxt = Context.proof_of context+ −
val trm = HOLogic.dest_Trueprop (prop_of thm)+ −
in+ −
case trm of+ −
Const (@{const_name "op ="}, _) $ lhs $ rhs =>+ −
let + −
val thm' = transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}+ −
in+ −
addel_fun thm' context+ −
end+ −
| _ => raise (error "only (op=) case implemented yet")+ −
end + −
+ −
val eqvt_add = Thm.declaration_attribute (fn thm => (add_thm thm) o (transform add_raw_thm thm));+ −
val eqvt_del = Thm.declaration_attribute (fn thm => (del_thm thm) o (transform del_raw_thm thm));+ −
+ −
val eqvt_raw_add = Thm.declaration_attribute add_raw_thm;+ −
val eqvt_raw_del = Thm.declaration_attribute del_raw_thm;+ −
+ −
val setup =+ −
Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) + −
(cat_lines ["declaration of equivariance lemmas - they will automtically be", + −
"brought into the form p o c = c"]) #>+ −
Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) + −
(cat_lines ["declaration of equivariance lemmas - no",+ −
"transformation is performed"]) #>+ −
PureThy.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>+ −
PureThy.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw);+ −
+ −
+ −
end;+ −