deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means

--- a/src/HOL/Nominal/Examples/Fsub.thy	Sat Apr 25 21:42:05 2009 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Sun Apr 26 00:42:49 2009 +0200
@@ -245,7 +245,7 @@
   apply (simp add: dj_perm_forget[OF dj_tyvrs_vrs])
   done
 
-lemma ty_vrs_fresh[fresh]:
+lemma ty_vrs_fresh:
   fixes x::"vrs"
   and   T::"ty"
   shows "x \<sharp> T"
@@ -422,7 +422,7 @@
   by (nominal_induct T avoiding: X T' rule: ty.strong_induct)
      (perm_simp add: fresh_left)+
 
-lemma type_subst_fresh[fresh]:
+lemma type_subst_fresh:
   fixes X::"tyvrs"
   assumes "X \<sharp> T" and "X \<sharp> P"
   shows   "X \<sharp> T[Y \<mapsto> P]\<^sub>\<tau>"
@@ -430,7 +430,7 @@
 by (nominal_induct T avoiding: X Y P rule:ty.strong_induct)
    (auto simp add: abs_fresh)
 
-lemma fresh_type_subst_fresh[fresh]:
+lemma fresh_type_subst_fresh:
     assumes "X\<sharp>T'"
     shows "X\<sharp>T[X \<mapsto> T']\<^sub>\<tau>"
 using assms 
@@ -458,18 +458,19 @@
 | "(VarB  X U)[Y \<mapsto> T]\<^sub>b =  VarB X (U[Y \<mapsto> T]\<^sub>\<tau>)"
 by auto
 
-lemma binding_subst_fresh[fresh]:
+lemma binding_subst_fresh:
   fixes X::"tyvrs"
   assumes "X \<sharp> a"
   and     "X \<sharp> P"
   shows "X \<sharp> a[Y \<mapsto> P]\<^sub>b"
 using assms
-by (nominal_induct a rule:binding.strong_induct)
-   (auto simp add: freshs)
+by (nominal_induct a rule: binding.strong_induct)
+   (auto simp add: type_subst_fresh)
 
-lemma binding_subst_identity: "X \<sharp> B \<Longrightarrow> B[X \<mapsto> U]\<^sub>b = B"
-  by (induct B rule: binding.induct)
-    (simp_all add: fresh_atm type_subst_identity)
+lemma binding_subst_identity: 
+  shows "X \<sharp> B \<Longrightarrow> B[X \<mapsto> U]\<^sub>b = B"
+by (induct B rule: binding.induct)
+   (simp_all add: fresh_atm type_subst_identity)
 
 consts 
   subst_tyc :: "env \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> env" ("_[_ \<mapsto> _]\<^sub>e" [100,100,100] 100)
@@ -478,14 +479,14 @@
 "([])[Y \<mapsto> T]\<^sub>e= []"
 "(B#\<Gamma>)[Y \<mapsto> T]\<^sub>e = (B[Y \<mapsto> T]\<^sub>b)#(\<Gamma>[Y \<mapsto> T]\<^sub>e)"
 
-lemma ctxt_subst_fresh'[fresh]:
+lemma ctxt_subst_fresh':
   fixes X::"tyvrs"
   assumes "X \<sharp> \<Gamma>"
   and     "X \<sharp> P"
   shows   "X \<sharp> \<Gamma>[Y \<mapsto> P]\<^sub>e"
 using assms
 by (induct \<Gamma>)
-   (auto simp add: fresh_list_cons freshs)
+   (auto simp add: fresh_list_cons binding_subst_fresh)
 
 lemma ctxt_subst_mem_TVarB: "TVarB X T \<in> set \<Gamma> \<Longrightarrow> TVarB X (T[Y \<mapsto> U]\<^sub>\<tau>) \<in> set (\<Gamma>[Y \<mapsto> U]\<^sub>e)"
   by (induct \<Gamma>) auto
@@ -1188,8 +1189,8 @@
 using assms by (induct, auto)
 
 nominal_inductive typing
-  by (auto dest!: typing_ok intro: closed_in_fresh fresh_domain
-    simp: abs_fresh fresh_prod fresh_atm freshs valid_ty_domain_fresh fresh_trm_domain)
+by (auto dest!: typing_ok intro: closed_in_fresh fresh_domain type_subst_fresh
+    simp: abs_fresh fresh_type_subst_fresh ty_vrs_fresh valid_ty_domain_fresh fresh_trm_domain)
 
 lemma ok_imp_VarB_closed_in:
   assumes ok: "\<turnstile> \<Gamma> ok"

--- a/src/HOL/Nominal/nominal_thmdecls.ML	Sat Apr 25 21:42:05 2009 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Sun Apr 26 00:42:49 2009 +0200
@@ -1,12 +1,12 @@
 (* Authors: Julien Narboux and Christian Urban
 
    This file introduces the infrastructure for the lemma
-   declaration "eqvts" "bijs" and "freshs".
+   collection "eqvts".
 
-   By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored
-   in a data-slot in the context. Possible modifiers
-   are [attribute add] and [attribute del] for adding and deleting,
-   respectively the lemma from the data-slot.
+   By attaching [eqvt], [eqvt_force] to a lemma, the lemma gets 
+   stored in a data-slot in the context. Possible modifiers
+   are [... add] and [... del] for adding and deleting, respectively 
+   the lemma from the data-slot.
 *)
 
 signature NOMINAL_THMDECLS =
@@ -17,9 +17,6 @@
   val eqvt_force_del: attribute
   val setup: theory -> theory
   val get_eqvt_thms: Proof.context -> thm list
-  val get_fresh_thms: Proof.context -> thm list
-  val get_bij_thms: Proof.context -> thm list
-
 
   val NOMINAL_EQVT_DEBUG : bool ref
 end;
@@ -29,13 +26,11 @@
 
 structure Data = GenericDataFun
 (
-  type T = {eqvts:thm list, freshs:thm list, bijs:thm list};
-  val empty = ({eqvts=[], freshs=[], bijs=[]}:T);
-  val extend = I;
-  fun merge _ (r1:T,r2:T) = {eqvts  = Thm.merge_thms (#eqvts r1, #eqvts r2),
-                             freshs = Thm.merge_thms (#freshs r1, #freshs r2),
-                             bijs   = Thm.merge_thms (#bijs r1, #bijs r2)}
-);
+  type T = thm list
+  val empty = []:T
+  val extend = I
+  fun merge _ (r1:T, r2:T) = Thm.merge_thms (r1, r2)
+)
 
 (* Exception for when a theorem does not conform with form of an equivariance lemma. *)
 (* There are two forms: one is an implication (for relations) and the other is an    *)
@@ -46,45 +41,40 @@
 (* the implicational case it is also checked that the variables and permutation fit  *)
 (* together, i.e. are of the right "pt_class", so that a stronger version of the     *)
 (* equality-lemma can be derived. *)
-exception EQVT_FORM of string;
-
-val get_eqvt_thms = Context.Proof #> Data.get #> #eqvts;
-val get_fresh_thms = Context.Proof #> Data.get #> #freshs;
-val get_bij_thms = Context.Proof #> Data.get #> #bijs;
+exception EQVT_FORM of string
 
 (* FIXME: should be a function in a library *)
-fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T));
+fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T))
 
-val NOMINAL_EQVT_DEBUG = ref false;
+val NOMINAL_EQVT_DEBUG = ref false
 
-fun tactic (msg,tac) =
-    if !NOMINAL_EQVT_DEBUG
-    then tac THEN print_tac ("after "^msg)
-    else tac
+fun tactic (msg, tac) =
+  if !NOMINAL_EQVT_DEBUG
+  then tac THEN' (K (print_tac ("after " ^ msg)))
+  else tac
 
 fun tactic_eqvt ctx orig_thm pi pi' =
-    let
-        val mypi = Thm.cterm_of ctx pi
-        val T = fastype_of pi'
-        val mypifree = Thm.cterm_of ctx (Const ("List.rev", T --> T) $ pi')
-        val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp"
-    in
-        EVERY [tactic ("iffI applied",rtac iffI 1),
-	       tactic ("remove pi with perm_boolE", (dtac @{thm perm_boolE} 1)),
-               tactic ("solve with orig_thm", (etac orig_thm 1)),
-               tactic ("applies orig_thm instantiated with rev pi",
-                          dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1),
-	       tactic ("getting rid of the pi on the right",
-                          (rtac @{thm perm_boolI} 1)),
-               tactic ("getting rid of all remaining perms",
-                          full_simp_tac (HOL_basic_ss addsimps perm_pi_simp) 1)]
-    end;
+let
+  val mypi = Thm.cterm_of ctx pi
+  val T = fastype_of pi'
+  val mypifree = Thm.cterm_of ctx (Const (@{const_name "List.rev"}, T --> T) $ pi')
+  val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp"
+in
+  EVERY1 [tactic ("iffI applied",rtac @{thm iffI}),
+	  tactic ("remove pi with perm_boolE", dtac @{thm perm_boolE}),
+          tactic ("solve with orig_thm", etac orig_thm),
+          tactic ("applies orig_thm instantiated with rev pi",
+                     dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)),
+	  tactic ("getting rid of the pi on the right", rtac @{thm perm_boolI}),
+          tactic ("getting rid of all remaining perms",
+                     full_simp_tac (HOL_basic_ss addsimps perm_pi_simp))]
+end;
 
 fun get_derived_thm ctxt hyp concl orig_thm pi typi =
   let
     val thy = ProofContext.theory_of ctxt;
     val pi' = Var (pi, typi);
-    val lhs = Const ("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
+    val lhs = Const (@{const_name "Nominal.perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
     val ([goal_term, pi''], ctxt') = Variable.import_terms false
       [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt
     val _ = Display.print_cterm (cterm_of thy goal_term)
@@ -95,23 +85,25 @@
   end
 
 (* replaces every variable x in t with pi o x *)
-fun apply_pi trm (pi,typi) =
-  let
-    fun only_vars t =
-       (case t of
-          Var (n,ty) => (Const ("Nominal.perm",typi --> ty --> ty) $ (Var (pi,typi)) $ (Var (n,ty)))
-        | _ => t)
-  in
-     map_aterms only_vars trm
-  end;
+fun apply_pi trm (pi, typi) =
+let
+  fun only_vars t =
+     (case t of
+         Var (n, ty) => 
+           (Const (@{const_name "Nominal.perm"}, typi --> ty --> ty) 
+                $ (Var (pi, typi)) $ (Var (n, ty)))
+       | _ => t)
+in
+    map_aterms only_vars trm
+end;
 
 (* returns *the* pi which is in front of all variables, provided there *)
 (* exists such a pi; otherwise raises EQVT_FORM                        *)
 fun get_pi t thy =
   let fun get_pi_aux s =
         (case s of
-          (Const ("Nominal.perm",typrm) $
-             (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $
+          (Const (@{const_name "Nominal.perm"} ,typrm) $
+             (Var (pi,typi as Type("List.list", [Type ("*", [Type (tyatm,[]),_])]))) $
                (Var (n,ty))) =>
              let
                 (* FIXME: this should be an operation the library *)
@@ -130,7 +122,7 @@
     (* to ensure that all pi's must have been the same, i.e. distinct returns  *)
     (* a singleton-list  *)
     (case (distinct (op =) (get_pi_aux t)) of
-      [(pi,typi)] => (pi,typi)
+      [(pi,typi)] => (pi, typi)
     | _ => raise EQVT_FORM "All permutation should be the same")
   end;
 
@@ -155,8 +147,8 @@
              else raise EQVT_FORM "Type Implication"
           end
        (* case: eqvt-lemma is of the equational form *)
-      | (Const ("Trueprop", _) $ (Const ("op =", _) $
-            (Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
+      | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $
+            (Const (@{const_name "Nominal.perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
            (if (apply_pi lhs (pi,typi)) = rhs
                then [orig_thm]
                else raise EQVT_FORM "Type Equality")
@@ -165,38 +157,26 @@
       fold (fn thm => Data.map (flag thm)) thms_to_be_added context
   end
   handle EQVT_FORM s =>
-      error (Display.string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").")
+      error (Display.string_of_thm orig_thm ^ 
+               " does not comply with the form of an equivariance lemma (" ^ s ^").")
 
-(* in cases of bij- and freshness, we just add the lemmas to the *)
-(* data-slot *)
 
-fun eqvt_map f (r:Data.T)  = {eqvts = f (#eqvts r), freshs = #freshs r, bijs = #bijs r};
-fun fresh_map f (r:Data.T) = {eqvts = #eqvts r, freshs = f (#freshs r), bijs = #bijs r};
-fun bij_map f (r:Data.T)   = {eqvts = #eqvts r, freshs = #freshs r, bijs = f (#bijs r)};
+fun eqvt_map f (r:Data.T)  = f r;
 
 val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.add_thm));
 val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.del_thm));
 
 val eqvt_force_add  = Thm.declaration_attribute (Data.map o eqvt_map o Thm.add_thm);
 val eqvt_force_del  = Thm.declaration_attribute (Data.map o eqvt_map o Thm.del_thm);
-val bij_add   = Thm.declaration_attribute (Data.map o bij_map o Thm.add_thm);
-val bij_del   = Thm.declaration_attribute (Data.map o bij_map o Thm.del_thm);
-val fresh_add = Thm.declaration_attribute (Data.map o fresh_map o Thm.add_thm);
-val fresh_del = Thm.declaration_attribute (Data.map o fresh_map o Thm.del_thm);
 
-
+val get_eqvt_thms = Context.Proof #> Data.get;
 
 val setup =
-  Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del)
-    "equivariance theorem declaration" #>
-  Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
-    "equivariance theorem declaration (without checking the form of the lemma)" #>
-  Attrib.setup @{binding fresh} (Attrib.add_del fresh_add fresh_del)
-    "freshness theorem declaration" #>
-  Attrib.setup @{binding "bij"} (Attrib.add_del bij_add bij_del)
-    "bijection theorem declaration" #>
-  PureThy.add_thms_dynamic (Binding.name "eqvts", #eqvts o Data.get) #>
-  PureThy.add_thms_dynamic (Binding.name "freshs", #freshs o Data.get) #>
-  PureThy.add_thms_dynamic (Binding.name "bijs", #bijs o Data.get);
+    Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del) 
+     "equivariance theorem declaration" 
+ #> Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
+     "equivariance theorem declaration (without checking the form of the lemma)" 
+ #> PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get) 
+
 
 end;