restored the old behaviour of having an eqvts list; the transformed theorems are stored in eqvts_raw
(* Title: nominal_thmdecls.ML Author: Christian Urban Infrastructure for the lemma collection "eqvts". Provides the attributes [eqvt] and [eqvt_force], 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 is stored in the form p o c == c The [eqvt_force] attribute just adds the theorem to eqvts. 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_force_add: attribute val eqvt_force_del: attribute val setup: theory -> theory val get_eqvt_thms: Proof.context -> thm list val get_eqvt_raw_thms: Proof.context -> thm listend;structure Nominal_ThmDecls: NOMINAL_THMDECLS =structstructure EqvtData = Generic_Data( type T = (thm * thm option) Item_Net.T; val empty = Item_Net.init (eq_fst Thm.eq_thm_prop) (single o Thm.full_prop_of o fst) val extend = I; val merge = Item_Net.merge;);val eqvts = (map fst) o Item_Net.content o EqvtData.get;val eqvts_raw = (map_filter snd) o Item_Net.content o EqvtData.get;val get_eqvt_thms = eqvts o Context.Proof; val get_eqvt_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_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 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_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 => let val thm2 = transform_eq ctxt thm lhs rhs RS @{thm eq_reflection} in addel_fn (thm, SOME thm2) context end | _ => raise (error "only (op=) case implemented yet")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 o rpair NONE);val eqvt_force_del = Thm.declaration_attribute (del_force_thm o rpair NONE);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 - no", "transformation is performed"]) #> PureThy.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> PureThy.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw);end;