# HG changeset patch
# User narboux
# Date 1175549092 -7200
# Node ID 80b814fe284ba6d10c42d89f8e92c0d33a290875
# Parent  705d4fb9e628250adb080b008095b015987e3310
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name

diff -r 705d4fb9e628 -r 80b814fe284b src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Mon Apr 02 11:31:08 2007 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Mon Apr 02 23:24:52 2007 +0200
@@ -72,6 +72,7 @@
 fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) (Name name);
 fun dynamic_thm  st name = PureThy.get_thm  (theory_of_thm st) (Name name);
 
+fun eqvts_thms st = NominalThmDecls.get_eqvt_thms (theory_of_thm st);
 
 (* needed in the process of fully simplifying permutations *)
 val strong_congs = [thm "if_cong"]
@@ -131,7 +132,7 @@
    end
 
 (* function for simplyfying permutations *)
-fun perm_simp_gen dyn_thms ss i = 
+fun perm_simp_gen dyn_thms f ss i = 
     ("general simplification of permutations", fn st =>
     let
 
@@ -141,7 +142,7 @@
        val perm_sp_app = Simplifier.simproc (theory_of_thm st) "perm_simproc_app" 
 	                 ["Nominal.perm pi x"] (perm_simproc_app st);
 
-       val ss' = ss addsimps (List.concat (map (dynamic_thms st) dyn_thms))
+       val ss' = ss addsimps ((List.concat (map (dynamic_thms st) dyn_thms))@(f st))
                     delcongs weak_congs
                     addcongs strong_congs
                     addsimprocs [perm_sp_fun, perm_sp_app]
@@ -150,8 +151,10 @@
     end);
 
 (* general simplification of permutations and permutation that arose from eqvt-problems *)
-val perm_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp"];
-val eqvt_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_pi_simp","eqvts"];
+val perm_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp"] (fn st => []);
+val eqvt_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_pi_simp"] eqvts_thms;
+
+(* FIXME removes the name lookup for these theorems use an ml value instead *)
 
 (* main simplification tactics for permutations *)
 (* FIXME: perm_simp_tac should simplify more permutations *)
diff -r 705d4fb9e628 -r 80b814fe284b src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Mon Apr 02 11:31:08 2007 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Mon Apr 02 23:24:52 2007 +0200
@@ -2,7 +2,7 @@
    Authors: Julien Narboux and Christian Urban
 
    This file introduces the infrastructure for the lemma 
-   declaration "eqvt" "bij" and "fresh".
+   declaration "eqvts" "bijs" and "freshs".
 
    By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored 
    in a data-slot in the theory context. Possible modifiers
@@ -30,12 +30,12 @@
 structure Data = GenericDataFun
 (
   val name = "HOL/Nominal/eqvt";
-  type T = {eqvts:thm list, fresh:thm list, bij:thm list};
-  val empty = ({eqvts=[], fresh=[], bij=[]}:T);
+  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  = Drule.merge_rules (#eqvts r1, #eqvts r2), 
-                             fresh = Drule.merge_rules (#fresh r1, #fresh r2), 
-                             bij   = Drule.merge_rules (#bij r1, #bij r2)}
+                             freshs = Drule.merge_rules (#freshs r1, #freshs r2), 
+                             bijs   = Drule.merge_rules (#bijs r1, #bijs r2)}
   fun print context (data:T) =
     let 
        fun print_aux msg thms =
@@ -43,8 +43,8 @@
            (map (ProofContext.pretty_thm (Context.proof_of context)) thms))
     in
       (print_aux "Equivariance lemmas: " (#eqvts data);
-       print_aux "Freshness lemmas: " (#fresh data);
-       print_aux "Bijection lemmas: " (#bij data))
+       print_aux "Freshness lemmas: " (#freshs data);
+       print_aux "Bijection lemmas: " (#bijs data))
     end;
  
 );
@@ -62,8 +62,8 @@
 
 val print_data = Data.print o Context.Proof;
 val get_eqvt_thms = Context.Theory #> Data.get #> #eqvts;
-val get_fresh_thms = Context.Theory #> Data.get #> #fresh;
-val get_bij_thms = Context.Theory #> Data.get #> #bij;
+val get_fresh_thms = Context.Theory #> Data.get #> #freshs;
+val get_bij_thms = Context.Theory #> Data.get #> #bijs;
 
 (* FIXME: should be a function in a library *)
 fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T));
@@ -195,13 +195,13 @@
      Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context' 
    end
 
-fun bij_add_del_aux f   = simple_add_del_aux #bij "bij" f
-fun fresh_add_del_aux f = simple_add_del_aux #fresh "fresh" f
+fun bij_add_del_aux f   = simple_add_del_aux #bijs "bijs" f
+fun fresh_add_del_aux f = simple_add_del_aux #freshs "freshs" f
 fun eqvt_force_add_del_aux f = simple_add_del_aux #eqvts "eqvts" f
 
-fun eqvt_map f th (r:Data.T)  = {eqvts = (f th (#eqvts r)), fresh = #fresh r, bij = #bij r};
-fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, fresh = (f th (#fresh r)), bij = #bij r};
-fun bij_map f th (r:Data.T)   = {eqvts = #eqvts r, fresh = #fresh r, bij = (f th (#bij r))};
+fun eqvt_map f th (r:Data.T)  = {eqvts = (f th (#eqvts r)), freshs = #freshs r, bijs = #bijs r};
+fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = (f th (#freshs r)), bijs = #bijs r};
+fun bij_map f th (r:Data.T)   = {eqvts = #eqvts r, freshs = #freshs r, bijs = (f th (#bijs r))};
 
 val eqvt_add  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule)); 
 val eqvt_del  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule));