--- a/Quot/Nominal/nominal_thmdecls.ML	Wed Feb 24 17:32:43 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,134 +0,0 @@
-(*  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;