(* 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 listend;structure Nominal_ThmDecls: NOMINAL_THMDECLS =structstructure 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 trmin Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trmendfun 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)endfun 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;