(* Title: nominal_thmdecls.ML+ −
Author: Christian Urban+ −
+ −
Infrastructure for the lemma collection "eqvts".+ −
+ −
Provides the attributes [eqvt] and [eqvt_force], and the theorem+ −
list eqvt. In contrast to eqvt-force, the eqvt-lemmas that will be + −
stored are expected to be of the form+ −
+ −
p o (c x1 x2 ...) = c (p o x1) (p o x2) ...+ −
+ −
and are transformed into the form+ −
+ −
p o c == c+ −
+ −
TODO+ −
+ −
- deal with eqvt-lemmas of the for + −
+ −
c x1 x2 ... ==> c (p o x1) (p o x2) ..+ −
*)+ −
+ −
signature NOMINAL_THMDECLS =+ −
sig+ −
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 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;+ −
);+ −
+ −
val content = Item_Net.content o EqvtData.get;+ −
val get_eqvt_thms = content o Context.Proof; + −
+ −
val add_thm = EqvtData.map o Item_Net.update;+ −
val del_thm = EqvtData.map o Item_Net.remove;+ −
+ −
val add_force_thm = EqvtData.map o Item_Net.update;+ −
val del_force_thm = EqvtData.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_fn 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 => + −
addel_fn (transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}) context+ −
| _ => raise (error "no other cases yet implemented")+ −
end + −
+ −
+ −
val eqvt_add = Thm.declaration_attribute (transform add_thm);+ −
val eqvt_del = Thm.declaration_attribute (transform del_thm);+ −
+ −
val eqvt_force_add = Thm.declaration_attribute add_force_thm;+ −
val eqvt_force_del = Thm.declaration_attribute del_force_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_force"} (Attrib.add_del eqvt_force_add eqvt_force_del) + −
(cat_lines ["declaration of equivariance lemmas - they will will be", + −
"added/deleted directly to the eqvt thm-list"]) #>+ −
PureThy.add_thms_dynamic (@{binding "eqvt"}, content);+ −
+ −
+ −
end;+ −