# HG changeset patch
# User urbanc
# Date 1170432976 -3600
# Node ID f76f187c91f969fe639decf8137a31802956909f
# Parent  bdec4a82f385e51a14c4b0147455df14f25535d6
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user

diff -r bdec4a82f385 -r f76f187c91f9 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Fri Feb 02 15:47:58 2007 +0100
+++ b/src/HOL/Nominal/Examples/Crary.thy	Fri Feb 02 17:16:16 2007 +0100
@@ -102,7 +102,7 @@
     v_nil[intro]:  "valid []"
   | v_cons[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
 
-lemma valid_eqvt:
+lemma valid_eqvt[eqvt]:
   fixes   pi:: "name prm"
   assumes a: "valid \<Gamma>"
   shows "valid (pi\<bullet>\<Gamma>)"
@@ -129,10 +129,10 @@
   using assms
   by (induct) (auto)
  
-lemma typing_eqvt :
+lemma typing_eqvt[eqvt]:
   fixes pi::"name prm"
   assumes "\<Gamma> \<turnstile> t : T"
-  shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : T"
+  shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : (pi\<bullet>T)"
   using assms
   apply(induct)
   apply(auto simp add: fresh_bij set_eqvt valid_eqvt) 
@@ -163,29 +163,28 @@
     and    x :: "'a::fs_name"
     assumes a: "\<Gamma> \<turnstile> e : T"
     and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T"
-    and a2: "\<And>\<Gamma> e1 T1 T2 e2 c. 
-             \<lbrakk>\<Gamma> \<turnstile> e1 : T1\<rightarrow>T2 ; \<And>c. P c \<Gamma> e1 (T1\<rightarrow>T2); \<Gamma> \<turnstile> e2 : T1 ; \<And>c. P c \<Gamma> e2 T1\<rbrakk> 
+    and a2: "\<And>\<Gamma> e1 T1 T2 e2 c. \<lbrakk>\<And>c. P c \<Gamma> e1 (T1\<rightarrow>T2); \<And>c. P c \<Gamma> e2 T1\<rbrakk> 
              \<Longrightarrow> P c \<Gamma> (App e1 e2) T2"
-    and a3: "\<And>x \<Gamma> T1 t T2 c.
-             \<lbrakk>x\<sharp>(\<Gamma>,c); (x,T1)#\<Gamma> \<turnstile> t : T2 ; \<And>c. P c ((x,T1)#\<Gamma>) t T2\<rbrakk>
+    and a3: "\<And>x \<Gamma> T1 t T2 c.\<lbrakk>x\<sharp>(\<Gamma>,c); \<And>c. P c ((x,T1)#\<Gamma>) t T2\<rbrakk>
              \<Longrightarrow> P c \<Gamma> (Lam [x].t) (T1\<rightarrow>T2)"
     and a4: "\<And>\<Gamma> n c. valid \<Gamma> \<Longrightarrow> P c \<Gamma> (Const n) TBase"
     and a5: "\<And>\<Gamma> c. valid \<Gamma> \<Longrightarrow> P c \<Gamma> Unit TUnit"
     shows "P c \<Gamma> e T"
 proof -
-  from a have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>e) T"
+  from a have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>e) (pi\<bullet>T)"
   proof (induct)
     case (t_Var \<Gamma> x T pi c)
     have "valid \<Gamma>" by fact
-    then have "valid (pi\<bullet>\<Gamma>)" by (simp only: valid_eqvt)
+    then have "valid (pi\<bullet>\<Gamma>)" by (simp only: eqvt)
     moreover
     have "(x,T)\<in>set \<Gamma>" by fact
     then have "pi\<bullet>(x,T)\<in>pi\<bullet>(set \<Gamma>)" by (simp only: pt_set_bij[OF pt_name_inst, OF at_name_inst])  
     then have "(pi\<bullet>x,T)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: set_eqvt)
-    ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Var x)) T" using a1 by simp
+    ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Var x)) (pi\<bullet>T)" using a1 by simp
   next
     case (t_App \<Gamma> e1 T1 T2 e2 pi c)
-    thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(App e1 e2)) T2" using a2 by (simp, blast intro: typing_eqvt)
+    thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(App e1 e2)) (pi\<bullet>T2)" using a2 
+      by (simp only: eqvt) (blast)
   next
     case (t_Lam x \<Gamma> T1 t T2 pi c)
     obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>\<Gamma>,pi\<bullet>t,c)" by (erule exists_fresh[OF fs_name1])
@@ -194,11 +193,8 @@
     have f0: "x\<sharp>\<Gamma>" by fact
     have f1: "(pi\<bullet>x)\<sharp>(pi\<bullet>\<Gamma>)" using f0 by (simp add: fresh_bij)
     have f2: "y\<sharp>?pi'\<bullet>\<Gamma>" by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp)
-    have pr1: "(x,T1)#\<Gamma> \<turnstile> t : T2" by fact
-    then have "(?pi'\<bullet>((x,T1)#\<Gamma>)) \<turnstile> (?pi'\<bullet>t) : T2" by (simp only: typing_eqvt)
-    moreover
-    have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>t) T2" by fact
-    ultimately have "P c (?pi'\<bullet>\<Gamma>) (Lam [y].(?pi'\<bullet>t)) (T1\<rightarrow>T2)" using fs f2 a3
+      have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>t) (?pi'\<bullet>T2)" by fact
+    then have "P c (?pi'\<bullet>\<Gamma>) (Lam [y].(?pi'\<bullet>t)) (T1\<rightarrow>T2)" using fs f2 a3
       by (simp add: calc_atm)
     then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t))) (T1\<rightarrow>T2)" 
       by (simp del: append_Cons add: calc_atm pt_name2)
@@ -206,18 +202,17 @@
       by (rule perm_fresh_fresh) (simp_all add: fs f1)
     moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t))) = Lam [(pi\<bullet>x)].(pi\<bullet>t)"
       by (rule perm_fresh_fresh) (simp_all add: fs f1 fresh_atm abs_fresh)
-    ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [x].t)) (T1\<rightarrow>T2)" 
-      by simp
+    ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [x].t)) (pi\<bullet>T1\<rightarrow>T2)" by simp
   next
     case (t_Const \<Gamma> n pi c)
-    thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Const n)) (TBase)" using a4 by (simp, blast intro: valid_eqvt)
+    thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Const n)) (pi\<bullet>TBase)" using a4 by (simp, blast intro: valid_eqvt)
   next
     case (t_Unit \<Gamma> pi c)
-    thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>Unit) (TUnit)" using a5 by (simp, blast intro: valid_eqvt)
+    thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>Unit) (pi\<bullet>TUnit)" using a5 by (simp, blast intro: valid_eqvt)
   qed 
-  then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>e) T" by blast
+  then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>e) (([]::name prm)\<bullet>T)" by blast
   then show "P c \<Gamma> e T" by simp
-qed 
+qed
 
 text {* capture-avoiding substitution *}
 
@@ -279,7 +274,7 @@
   and   "Unit [y::=t'] = Unit"
   by (simp_all add: fresh_list_cons fresh_list_nil)
 
-lemma subst_eqvt:
+lemma subst_eqvt[eqvt]:
   fixes pi::"name prm" 
   and   t::"trm"
   shows "pi\<bullet>(t[x::=t']) = (pi\<bullet>t)[(pi\<bullet>x)::=(pi\<bullet>t')]"
@@ -371,13 +366,13 @@
   shows "valid \<Gamma>"
 using assms by (induct,auto elim:typing_valid)
 
-lemma equiv_def_eqvt:
+lemma equiv_def_eqvt[eqvt]:
   fixes pi::"name prm"
   assumes a: "\<Gamma> \<turnstile> s == t : T"
-  shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) == (pi\<bullet>t) : T"
+  shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) == (pi\<bullet>t) : (pi\<bullet>T)"
 using a
 apply(induct)
-apply(auto intro: typing_eqvt valid_eqvt simp add: fresh_bij subst_eqvt)
+apply(auto intro: typing_eqvt valid_eqvt simp add: fresh_bij subst_eqvt simp del: perm_ty)
 apply(rule_tac x="pi\<bullet>x" in Q_Ext)
 apply(simp add: fresh_bij)+
 done
@@ -387,46 +382,39 @@
   fixes c::"'a::fs_name"
   assumes a0: "\<Gamma> \<turnstile> s == t : T" 
   and     a1: "\<And>\<Gamma> t T c.  \<Gamma> \<turnstile> t : T  \<Longrightarrow> P c \<Gamma> t t T"
-  and     a2: "\<And>\<Gamma> t s T c. \<lbrakk>\<Gamma> \<turnstile> t == s : T; \<And>d. P d \<Gamma> t s T\<rbrakk> \<Longrightarrow>  P c \<Gamma> s t T"
-  and     a3: "\<And>\<Gamma> s t T u c. 
-               \<lbrakk>\<Gamma> \<turnstile> s == t : T; \<And>d. P d \<Gamma> s t T; \<Gamma> \<turnstile> t == u : T; \<And>d. P d \<Gamma> t u T\<rbrakk> 
+  and     a2: "\<And>\<Gamma> t s T c. \<lbrakk>\<And>d. P d \<Gamma> t s T\<rbrakk> \<Longrightarrow>  P c \<Gamma> s t T"
+  and     a3: "\<And>\<Gamma> s t T u c. \<lbrakk>\<And>d. P d \<Gamma> s t T; \<And>d. P d \<Gamma> t u T\<rbrakk> 
                \<Longrightarrow> P c \<Gamma> s u T"
-  and     a4: "\<And>x \<Gamma> T1 s2 t2 T2 c. \<lbrakk>x\<sharp>\<Gamma>; x\<sharp>c; (x,T1)#\<Gamma> \<turnstile> s2 == t2 : T2; \<And>d. P d ((x,T1)#\<Gamma>) s2 t2 T2\<rbrakk>
+  and     a4: "\<And>x \<Gamma> T1 s2 t2 T2 c. \<lbrakk>x\<sharp>\<Gamma>; x\<sharp>c; \<And>d. P d ((x,T1)#\<Gamma>) s2 t2 T2\<rbrakk>
                \<Longrightarrow> P c \<Gamma> (Lam [x].s2) (Lam [x].t2) (T1\<rightarrow>T2)"
-  and     a5: "\<And>\<Gamma> s1 t1 T1 T2 s2 t2 c.
-               \<lbrakk>\<Gamma> \<turnstile> s1 == t1 : T1\<rightarrow>T2; \<And>d. P d \<Gamma> s1 t1 (T1\<rightarrow>T2); 
-                \<Gamma> \<turnstile> s2 == t2 : T1; \<And>d. P d \<Gamma> s2 t2 T1\<rbrakk> \<Longrightarrow> P c \<Gamma> (App s1 s2) (App t1 t2) T2"
+  and     a5: "\<And>\<Gamma> s1 t1 T1 T2 s2 t2 c. \<lbrakk>\<And>d. P d \<Gamma> s1 t1 (T1\<rightarrow>T2); \<And>d. P d \<Gamma> s2 t2 T1\<rbrakk> 
+               \<Longrightarrow> P c \<Gamma> (App s1 s2) (App t1 t2) T2"
   and     a6: "\<And>x \<Gamma> T1 s12 t12 T2 s2 t2 c.
-               \<lbrakk>x\<sharp>(\<Gamma>,s2,t2); x\<sharp>c; (x,T1)#\<Gamma> \<turnstile> s12 == t12 : T2; \<And>d. P d ((x,T1)#\<Gamma>) s12 t12 T2;
-               \<Gamma> \<turnstile> s2 == t2 : T1; \<And>d. P d \<Gamma> s2 t2 T1\<rbrakk> 
+               \<lbrakk>x\<sharp>(\<Gamma>,s2,t2); x\<sharp>c; \<And>d. P d ((x,T1)#\<Gamma>) s12 t12 T2; \<And>d. P d \<Gamma> s2 t2 T1\<rbrakk> 
                \<Longrightarrow> P c \<Gamma> (App (Lam [x].s12) s2) (t12[x::=t2]) T2"
   and     a7: "\<And>x \<Gamma> s t T1 T2 c.
-               \<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T1)#\<Gamma> \<turnstile> App s (Var x) == App t (Var x) : T2;
-               \<And>d. P d ((x,T1)#\<Gamma>) (App s (Var x)) (App t (Var x)) T2\<rbrakk>
+               \<lbrakk>x\<sharp>(\<Gamma>,s,t); \<And>d. P d ((x,T1)#\<Gamma>) (App s (Var x)) (App t (Var x)) T2\<rbrakk>
                \<Longrightarrow> P c \<Gamma> s t (T1\<rightarrow>T2)"
  shows "P c \<Gamma>  s t T"
 proof -
-  from a0 have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) T" 
+  from a0 have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T)" 
     proof(induct)
       case (Q_Refl \<Gamma> t T pi c)
-      then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>t) (pi\<bullet>t) T" using a1 by (simp add: typing_eqvt)
+      then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>t) (pi\<bullet>t) (pi\<bullet>T)" using a1 by (simp only: eqvt)
     next
       case (Q_Symm \<Gamma> t s T pi c)
-      then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) T" using a2 by (simp only: equiv_def_eqvt)
+      then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T)" using a2 by (simp only: equiv_def_eqvt)
     next
       case (Q_Trans \<Gamma> s t T u pi c)
-      then show " P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>u) T" using a3 by (blast intro: equiv_def_eqvt)
+      then show " P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>u) (pi\<bullet>T)" using a3 by (blast intro: equiv_def_eqvt)
     next
       case (Q_App \<Gamma> s1 t1 T1 T2 s2 t2 pi c)
-      then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>App s1 s2) (pi\<bullet>App t1 t2) T2" using a5 
-	by (simp, blast intro: equiv_def_eqvt)
+      then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>App s1 s2) (pi\<bullet>App t1 t2) (pi\<bullet>T2)" using a5 
+	by (simp only: eqvt) (blast)
     next
       case (Q_Ext x \<Gamma> s t T1 T2 pi c)
-      then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (T1\<rightarrow>T2)"  
-	apply(auto intro!: a7 simp add: fresh_bij)
-	apply(drule equiv_def_eqvt)
-	apply(simp)
-	done
+      then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T1\<rightarrow>T2)"  
+	by (auto intro!: a7 simp add: fresh_bij)
     next
       case (Q_Abs x \<Gamma> T1 s2 t2 T2 pi c)
       obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>s2,pi\<bullet>t2,pi\<bullet>\<Gamma>,c)" by (rule exists_fresh[OF fs_name1])
@@ -435,13 +423,9 @@
       have f1: "x\<sharp>\<Gamma>" by fact
       have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>\<Gamma>)" using f1 by (simp add: fresh_bij)
       have f3: "y\<sharp>?pi'\<bullet>\<Gamma>" using f1 by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp)
-      have pr1: "(x,T1)#\<Gamma> \<turnstile> s2 == t2 : T2" by fact
-      then have "?pi'\<bullet>((x,T1)#\<Gamma>) \<turnstile> (?pi'\<bullet>s2) == (?pi'\<bullet>t2) : T2" by (rule equiv_def_eqvt)
-      then have "((y,T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>s2) == (?pi'\<bullet>t2) : T2" by (simp add: calc_atm)
-      moreover    
-      have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>s2) (?pi'\<bullet>t2) T2" by fact
+      have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>s2) (?pi'\<bullet>t2) (?pi'\<bullet>T2)" by fact
       then have "\<And>c. P c ((y,T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>s2) (?pi'\<bullet>t2) T2" by (simp add: calc_atm)
-      ultimately have "P c  (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>Lam [x].s2) (?pi'\<bullet>Lam [x].t2) (T1\<rightarrow>T2)" using a4 f3 fs
+      then have "P c  (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>Lam [x].s2) (?pi'\<bullet>Lam [x].t2) (T1\<rightarrow>T2)" using a4 f3 fs
 	by (simp add: calc_atm)
       then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>Lam [(pi\<bullet>x)].(pi\<bullet>s2)) (?sw\<bullet>Lam [(pi\<bullet>x)].(pi\<bullet>t2)) (T1\<rightarrow>T2)" 
 	by (simp del: append_Cons add: calc_atm pt_name2)
@@ -452,7 +436,7 @@
       moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t2))) = Lam [(pi\<bullet>x)].(pi\<bullet>t2)" 
 	by (rule perm_fresh_fresh) (simp_all add: fs f2 abs_fresh)
       ultimately have "P c (pi\<bullet>\<Gamma>) (Lam [(pi\<bullet>x)].(pi\<bullet>s2)) (Lam [(pi\<bullet>x)].(pi\<bullet>t2)) (T1\<rightarrow>T2)" by simp
-      then show  "P c (pi\<bullet>\<Gamma>) (pi\<bullet>Lam [x].s2) (pi\<bullet>Lam [x].t2) (T1\<rightarrow>T2)" by simp 
+      then show  "P c (pi\<bullet>\<Gamma>) (pi\<bullet>Lam [x].s2) (pi\<bullet>Lam [x].t2) (pi\<bullet>T1\<rightarrow>T2)" by simp 
     next 
       case (Q_Beta x \<Gamma> s2 t2 T1 s12 t12 T2 pi c) 
       obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>s12,pi\<bullet>t12,pi\<bullet>s2,pi\<bullet>t2,pi\<bullet>\<Gamma>,c)" 
@@ -463,19 +447,12 @@
       have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>(\<Gamma>,s2,t2))" using f1 by (simp add: fresh_bij)
       have f3: "y\<sharp>(?pi'\<bullet>(\<Gamma>,s2,t2))" using f1 
 	by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp fresh_prod)
-      have pr1: "(x,T1)#\<Gamma> \<turnstile> s12 == t12 : T2" by fact
-      then have "?pi'\<bullet>((x,T1)#\<Gamma>) \<turnstile> (?pi'\<bullet>s12) == (?pi'\<bullet>t12) : T2" by (rule equiv_def_eqvt)
-      then have "((y,T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>s12) == (?pi'\<bullet>t12) : T2" by (simp add: calc_atm)
-      moreover    
-      have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>s12) (?pi'\<bullet>t12) T2" by fact
-      then have "\<And>c. P c ((y,T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>s12) (?pi'\<bullet>t12) T2" by (simp add: calc_atm)
+      have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>s12) (?pi'\<bullet>t12) (?pi'\<bullet>T2)" by fact
+      then have "\<And>c. P c ((y,T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>s12) (?pi'\<bullet>t12) (?pi'\<bullet>T2)" by (simp add: calc_atm)
       moreover
-      have pr2: "\<Gamma> \<turnstile> s2 == t2 : T1" by fact
-      then have "(?pi'\<bullet>\<Gamma>) \<turnstile> (?pi'\<bullet>s2) == (?pi'\<bullet>t2) : T1" by (rule equiv_def_eqvt)
-      moreover    
-      have ih2: "\<And>c. P c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>s2) (?pi'\<bullet>t2) T1" by fact
-      ultimately have "P c  (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>(App (Lam [x].s12) s2)) (?pi'\<bullet>(t12[x::=t2])) T2" 
-	using a6 f3 fs by (simp add: subst_eqvt calc_atm)
+      have ih2: "\<And>c. P c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>s2) (?pi'\<bullet>t2) (?pi'\<bullet>T1)" by fact
+      ultimately have "P c  (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>(App (Lam [x].s12) s2)) (?pi'\<bullet>(t12[x::=t2])) (?pi'\<bullet>T2)" 
+	using a6 f3 fs by (force simp add: subst_eqvt calc_atm del: perm_ty)
       then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s2))) 
 	(?sw\<bullet>((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t2)])) T2" 
 	by (simp del: append_Cons add: calc_atm pt_name2 subst_eqvt)
@@ -488,9 +465,9 @@
 	   (simp_all add: fs[simplified] f2[simplified] fresh_subst fresh_subst'')
       ultimately have "P c (pi\<bullet>\<Gamma>) (App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s2)) ((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t2)]) T2"
 	by simp
-      then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>App (Lam [x].s12) s2) (pi\<bullet>t12[x::=t2]) T2" by (simp add: subst_eqvt)	
+      then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>App (Lam [x].s12) s2) (pi\<bullet>t12[x::=t2]) (pi\<bullet>T2)" by (simp add: subst_eqvt)
     qed
-  then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>s) (([]::name prm)\<bullet>t) T" by blast
+  then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>s) (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>T)" by blast
   then show "P c \<Gamma> s t T" by simp
 qed
 
@@ -538,7 +515,7 @@
 using a
 by (induct) (auto simp add: subst_eqvt fresh_bij)
 
-lemma whn_eqvt:
+lemma whn_eqvt[eqvt]:
   fixes pi::"name prm"
   assumes a: "t \<Down> t'"
   shows "(pi\<bullet>t) \<Down> (pi\<bullet>t')"
@@ -568,10 +545,10 @@
 | QAP_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T1 \<rightarrow> T2; \<Gamma> \<turnstile> s <=> t : T1 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App p s \<leftrightarrow> App q t : T2"
 | QAP_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n \<leftrightarrow> Const n : TBase"
 
-lemma alg_equiv_alg_path_equiv_eqvt:
+lemma alg_equiv_alg_path_equiv_eqvt[eqvt]:
   fixes pi::"name prm"
-  shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) <=> (pi\<bullet>t) : T" 
-  and   "\<Gamma> \<turnstile> p \<leftrightarrow> q : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>p) \<leftrightarrow> (pi\<bullet>q) : T"
+  shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) <=> (pi\<bullet>t) : (pi\<bullet>T)" 
+  and   "\<Gamma> \<turnstile> p \<leftrightarrow> q : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>p) \<leftrightarrow> (pi\<bullet>q) : (pi\<bullet>T)"
 apply(induct rule: alg_equiv_alg_path_equiv.inducts)
 apply(auto intro: whn_eqvt simp add: fresh_bij valid_eqvt)
 apply(rule_tac x="pi\<bullet>x" in  QAT_Arrow)
@@ -606,7 +583,7 @@
     then show "\<forall>c (pi::name prm). P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) TBase"
       apply(auto)
       apply(rule_tac p="pi\<bullet>q" and q="pi\<bullet>p" in  a1)
-      apply(simp_all add: whn_eqvt alg_equiv_alg_path_equiv_eqvt)
+      apply(simp_all add: whn_eqvt alg_equiv_alg_path_equiv_eqvt[simplified])
       done
   next
     case (QAT_Arrow x \<Gamma> s t T1 T2)
@@ -623,8 +600,8 @@
 	by (simp only: pt_name2 fresh_left, auto simp add: perm_pi_simp calc_atm)
       then have f3': "y\<sharp>?pi'\<bullet>\<Gamma>" "y\<sharp>?pi'\<bullet>s" "y\<sharp>?pi'\<bullet>t" by (auto simp add: fresh_prod)
       have pr1: "(x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App t (Var x) : T2" by fact
-      then have "(?pi'\<bullet>((x,T1)#\<Gamma>)) \<turnstile> (?pi'\<bullet>(App s (Var x))) <=> (?pi'\<bullet>(App t (Var x))) : T2" 
-	by (simp only: alg_equiv_alg_path_equiv_eqvt)
+      then have "(?pi'\<bullet>((x,T1)#\<Gamma>)) \<turnstile> (?pi'\<bullet>(App s (Var x))) <=> (?pi'\<bullet>(App t (Var x))) : (?pi'\<bullet>T2)" 
+	by (rule alg_equiv_alg_path_equiv_eqvt)
       then have "(y,T1)#(?pi'\<bullet>\<Gamma>) \<turnstile> (App (?pi'\<bullet>s) (Var y)) <=> (App (?pi'\<bullet>t) (Var y)) : T2" 
 	by (simp add: calc_atm)
       moreover    
@@ -659,7 +636,7 @@
   next
     case (QAP_App \<Gamma> p q T1 T2 s t)
     then show "\<forall>c (pi::name prm). P2 c (pi\<bullet>\<Gamma>) (pi\<bullet>App p s) (pi\<bullet>App q t) T2"
-      by (auto intro!: a5 simp add: alg_equiv_alg_path_equiv_eqvt)
+      by (auto intro!: a5 simp add: alg_equiv_alg_path_equiv_eqvt[simplified])
   next
     case (QAP_Const \<Gamma> n)
     then show "\<forall>c (pi::name prm). P2 c (pi\<bullet>\<Gamma>) (pi\<bullet>Const n) (pi\<bullet>Const n) TBase"
@@ -724,7 +701,6 @@
 proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: \<Gamma>' rule: alg_equiv_alg_path_equiv_strong_inducts)
   case (QAT_Arrow x \<Gamma> s t T1 T2 \<Gamma>')
   have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact
-  have h1:"(x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App t (Var x) : T2" by fact
   have h2:"\<Gamma>\<lless>\<Gamma>'" by fact
   have ih:"\<And>\<Gamma>'. \<lbrakk>(x,T1)#\<Gamma> \<lless> \<Gamma>'\<rbrakk>  \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) <=> App t (Var x) : T2" by fact
   have "x\<sharp>\<Gamma>'" by fact
@@ -984,7 +960,8 @@
   have "(pi\<bullet>((x,T1)#\<Gamma>)) \<turnstile> pi \<bullet> (App s (Var x)) <=> pi \<bullet> (App t (Var x)) : T2" by fact
   then have "(pi\<bullet>((x,T1)#\<Gamma>)) \<turnstile> (App (pi\<bullet>s) (Var (pi\<bullet>x))) <=> (App (pi\<bullet>t) (Var (pi\<bullet>x))) : T2" by auto
   moreover have "pi\<bullet>((x,T1)#\<Gamma>) = (pi\<bullet>x,pi\<bullet>T1)#(pi\<bullet>\<Gamma>)" by auto
-  ultimately have "((pi\<bullet>x,T1)#(pi\<bullet>\<Gamma>))  \<turnstile> (App (pi\<bullet>s) (Var (pi\<bullet>x))) <=> (App (pi\<bullet>t) (Var (pi\<bullet>x))) : T2" using perm_ty by auto
+  ultimately have "((pi\<bullet>x,T1)#(pi\<bullet>\<Gamma>))  \<turnstile> (App (pi\<bullet>s) (Var (pi\<bullet>x))) <=> (App (pi\<bullet>t) (Var (pi\<bullet>x))) : T2" 
+    using perm_ty by auto
   then show ?case using h by auto
 qed (auto elim:whn_eqvt valid_eqvt)
  
@@ -1271,7 +1248,6 @@
   case (Q_Abs x \<Gamma> T1 s2 t2 T2 \<Gamma>' \<gamma> \<theta>)
   have fs:"x\<sharp>\<Gamma>" by fact
   have fs2: "x\<sharp>\<gamma>" "x\<sharp>\<theta>" by fact 
-  have h1:"(x,T1)#\<Gamma> \<turnstile> s2 == t2 : T2" by fact
   have h2:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact
   have ih:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s2> is \<theta><t2> : T2" by fact
   {
diff -r bdec4a82f385 -r f76f187c91f9 src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Fri Feb 02 15:47:58 2007 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Fri Feb 02 17:16:16 2007 +0100
@@ -32,7 +32,7 @@
     v1[intro]: "valid []"
   | v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
 
-lemma eqvt_valid:
+lemma eqvt_valid[eqvt]:
   fixes   pi:: "name prm"
   assumes a: "valid \<Gamma>"
   shows   "valid (pi\<bullet>\<Gamma>)"
@@ -40,6 +40,8 @@
 by (induct)
    (auto simp add: fresh_bij)
 
+thm eqvt
+
 text{* typing judgements *}
 inductive2
   typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) 
@@ -48,22 +50,22 @@
   | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
   | t_Lam[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
 
-lemma eqvt_typing: 
+lemma eqvt_typing[eqvt]: 
   fixes pi:: "name prm"
   assumes a: "\<Gamma> \<turnstile> t : \<tau>"
-  shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : \<tau>"
+  shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : (pi\<bullet>\<tau>)"
 using a
 proof (induct)
   case (t_Var \<Gamma> a \<tau>)
   have "valid (pi\<bullet>\<Gamma>)" by (rule eqvt_valid)
   moreover
   have "(pi\<bullet>(a,\<tau>))\<in>(pi\<bullet>set \<Gamma>)" by (rule pt_set_bij2[OF pt_name_inst, OF at_name_inst])
-  ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Var a) : \<tau>"
+  ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Var a) : (pi\<bullet>\<tau>)"
     using typing.intros by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
 next 
   case (t_Lam a \<Gamma> \<tau> t \<sigma>)
   moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij)
-  ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force 
+  ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :(pi\<bullet>\<tau>\<rightarrow>\<sigma>)" by force 
 qed (auto)
 
 text {* the strong induction principle needs to be derived manually *}
@@ -76,26 +78,26 @@
   and    x :: "'a::fs_name"
   assumes a: "\<Gamma> \<turnstile> t : \<tau>"
   and a1:    "\<And>\<Gamma> a \<tau> x. \<lbrakk>valid \<Gamma>; (a,\<tau>) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P x \<Gamma> (Var a) \<tau>"
-  and a2:    "\<And>\<Gamma> \<tau> \<sigma> t1 t2 x. 
-              \<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; (\<And>z. P z \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>)); \<Gamma> \<turnstile> t2 : \<tau>; (\<And>z. P z \<Gamma> t2 \<tau>)\<rbrakk>
+  and a2:    "\<And>\<Gamma> \<tau> \<sigma> t1 t2 x. \<lbrakk>\<And>z. P z \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>); \<And>z. P z \<Gamma> t2 \<tau>\<rbrakk>
               \<Longrightarrow> P x \<Gamma> (App t1 t2) \<sigma>"
-  and a3:    "\<And>a \<Gamma> \<tau> \<sigma> t x. \<lbrakk>a\<sharp>x; a\<sharp>\<Gamma>; ((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>; (\<And>z. P z ((a,\<tau>)#\<Gamma>) t \<sigma>)\<rbrakk>
+  and a3:    "\<And>a \<Gamma> \<tau> \<sigma> t x. \<lbrakk>a\<sharp>x; a\<sharp>\<Gamma>; \<And>z. P z ((a,\<tau>)#\<Gamma>) t \<sigma>\<rbrakk>
               \<Longrightarrow> P x \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>)"
   shows "P x \<Gamma> t \<tau>"
 proof -
-  from a have "\<And>(pi::name prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>t) \<tau>"
+  from a have "\<And>(pi::name prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>t) (pi\<bullet>\<tau>)"
   proof (induct)
     case (t_Var \<Gamma> a \<tau>)
     have "valid \<Gamma>" by fact
-    then have "valid (pi\<bullet>\<Gamma>)" by (rule eqvt_valid)
+    then have "valid (pi\<bullet>\<Gamma>)" by (rule eqvt)
     moreover
     have "(a,\<tau>)\<in>set \<Gamma>" by fact
     then have "pi\<bullet>(a,\<tau>)\<in>pi\<bullet>(set \<Gamma>)" by (simp only: pt_set_bij[OF pt_name_inst, OF at_name_inst])  
     then have "(pi\<bullet>a,\<tau>)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_name_inst])
-    ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Var a)) \<tau>" using a1 by simp
+    ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Var a)) (pi\<bullet>\<tau>)" using a1 by simp
   next
     case (t_App \<Gamma> t1 \<tau> \<sigma> t2)
-    thus "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(App t1 t2)) \<sigma>" using a2 by (simp, blast intro: eqvt_typing)
+    thus "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(App t1 t2)) (pi\<bullet>\<sigma>)" using a2 
+      by (simp only: eqvt) (blast)
   next
     case (t_Lam a \<Gamma> \<tau> t \<sigma>)
     obtain c::"name" where fs: "c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)" by (rule exists_fresh[OF fs_name1])
@@ -104,22 +106,18 @@
     have f1: "a\<sharp>\<Gamma>" by fact
     have f2: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" using f1 by (simp add: fresh_bij)
     have f3: "c\<sharp>?pi'\<bullet>\<Gamma>" using f1 by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp)
-    have pr1: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact
-    then have "(?pi'\<bullet>((a,\<tau>)#\<Gamma>)) \<turnstile> (?pi'\<bullet>t) : \<sigma>" by (rule eqvt_typing)
-    then have "((c,\<tau>)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>t) : \<sigma>" by (simp add: calc_atm)
-    moreover    
-    have ih1: "\<And>x. P x (?pi'\<bullet>((a,\<tau>)#\<Gamma>)) (?pi'\<bullet>t) \<sigma>" by fact
-    then have "\<And>x. P x ((c,\<tau>)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>t) \<sigma>" by (simp add: calc_atm)
-    ultimately have "P x (?pi'\<bullet>\<Gamma>) (Lam [c].(?pi'\<bullet>t)) (\<tau> \<rightarrow> \<sigma>)" using a3 f3 fs by simp
-    then have "P x (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(Lam [(pi\<bullet>a)].(pi\<bullet>t))) (\<tau> \<rightarrow> \<sigma>)" 
+    have ih1: "\<And>x. P x (?pi'\<bullet>((a,\<tau>)#\<Gamma>)) (?pi'\<bullet>t) (?pi'\<bullet>\<sigma>)" by fact
+    then have "\<And>x. P x ((c,\<tau>)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>t) (?pi'\<bullet>\<sigma>)" by (simp add: calc_atm)
+    then have "P x (?pi'\<bullet>\<Gamma>) (Lam [c].(?pi'\<bullet>t)) (\<tau>\<rightarrow>\<sigma>)" using a3 f3 fs by simp
+    then have "P x (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(Lam [(pi\<bullet>a)].(pi\<bullet>t))) (\<tau>\<rightarrow>\<sigma>)" 
       by (simp del: append_Cons add: calc_atm pt_name2)
     moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" 
       by (rule perm_fresh_fresh) (simp_all add: fs f2)
     moreover have "(?sw\<bullet>(Lam [(pi\<bullet>a)].(pi\<bullet>t))) = Lam [(pi\<bullet>a)].(pi\<bullet>t)" 
       by (rule perm_fresh_fresh) (simp_all add: fs f2 abs_fresh)
-    ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [a].t)) (\<tau> \<rightarrow> \<sigma>)" by (simp only: , simp)
+    ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [a].t)) (pi\<bullet>\<tau>\<rightarrow>\<sigma>)" by (simp)
   qed
-  hence "P x (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>t) \<tau>" by blast
+  hence "P x (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>\<tau>)" by blast
   thus "P x \<Gamma> t \<tau>" by simp
 qed
 
diff -r bdec4a82f385 -r f76f187c91f9 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Fri Feb 02 15:47:58 2007 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Fri Feb 02 17:16:16 2007 +0100
@@ -4,6 +4,7 @@
 imports Main Infinite_Set
 uses
   ("nominal_atoms.ML")
+  ("nominal_tags.ML")
   ("nominal_package.ML")
   ("nominal_induct.ML") 
   ("nominal_permeq.ML")
@@ -3006,22 +3007,19 @@
 (* setup for the individial atom-kinds *)
 (* and nominal datatypes               *)
 use "nominal_atoms.ML"
+setup "NominalAtoms.setup"
+
+(******************************************)
+(* Setup of the tags: eqvt, fresh and bij *)
+
+use "nominal_tags.ML"
+setup "EqvtRules.setup"
+setup "FreshRules.setup"
+setup "BijRules.setup"
+
+(*******************************)
 (* permutation equality tactic *)
 use "nominal_permeq.ML";
-use "nominal_package.ML"
-setup "NominalAtoms.setup"
-setup "NominalPackage.setup"
-
-(** primitive recursive functions on nominal datatypes **)
-use "nominal_primrec.ML"
-
-(*****************************************)
-(* setup for induction principles method *)
-
-use "nominal_induct.ML";
-method_setup nominal_induct =
-  {* NominalInduct.nominal_induct_method *}
-  {* nominal induction *}
 
 method_setup perm_simp =
   {* NominalPermeq.perm_eq_meth *}
@@ -3063,4 +3061,22 @@
   {* NominalPermeq.fresh_gs_meth_debug *}
   {* tactic for deciding whether an atom is fresh for something including debugging facilities *}
 
+(*********************************)
+(* nominal datatype construction *)
+use "nominal_package.ML"
+setup "NominalPackage.setup"
+
+(******************************************************)
+(* primitive recursive functions on nominal datatypes *)
+use "nominal_primrec.ML"
+
+(*****************************************)
+(* setup for induction principles method *)
+
+use "nominal_induct.ML";
+method_setup nominal_induct =
+  {* NominalInduct.nominal_induct_method *}
+  {* nominal induction *}
+
+
 end
diff -r bdec4a82f385 -r f76f187c91f9 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Fri Feb 02 15:47:58 2007 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Fri Feb 02 17:16:16 2007 +0100
@@ -1104,6 +1104,7 @@
       end) atoms;
 
     val simp_atts = replicate (length new_type_names) [Simplifier.simp_add];
+    val simp_eqvt_atts = replicate (length new_type_names) [Simplifier.simp_add,  EqvtRules.eqvt_add];
 
     val (_, thy9) = thy8 |>
       Theory.add_path big_name |>
@@ -1112,7 +1113,7 @@
       Theory.parent_path ||>>
       DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
       DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
-      DatatypeAux.store_thmss_atts "perm" new_type_names simp_atts perm_simps' ||>>
+      DatatypeAux.store_thmss_atts "perm" new_type_names simp_eqvt_atts perm_simps' ||>>
       DatatypeAux.store_thmss "inject" new_type_names inject_thms ||>>
       DatatypeAux.store_thmss "supp" new_type_names supp_thms ||>>
       DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms ||>
diff -r bdec4a82f385 -r f76f187c91f9 src/HOL/Nominal/nominal_tags.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/nominal_tags.ML	Fri Feb 02 17:16:16 2007 +0100
@@ -0,0 +1,267 @@
+(* ID: "$Id$"
+   Authors: Julien Narboux and Christian Urban
+
+   This file introduces the infrastructure for the lemma 
+   declaration "eqvt" "bij" and "fresh".
+
+   By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored 
+   in a data-slot in the theory context. Possible modifiers
+   are [tag add] and [tag del] for adding and deleting,
+   respectively the lemma from the data-slot.  
+*)
+
+signature EQVT_RULES =
+sig
+  val print_eqvtset: Proof.context -> unit
+  val eqvt_add: attribute
+  val eqvt_del: attribute
+  val setup: theory -> theory
+
+  val EQVT_DEBUG : bool ref
+end;
+
+structure EqvtRules: EQVT_RULES =
+struct
+
+structure Data = GenericDataFun
+(
+  val name = "HOL/Nominal/eqvt";
+  type T = thm list;
+  val empty = [];
+  val extend = I;
+  fun merge _ = Drule.merge_rules;
+  fun print context rules =
+    Pretty.writeln (Pretty.big_list "Equivariance lemmas:"
+      (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
+);
+
+(* 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    *)
+(* equality (for functions). In the implication-case, say P ==> Q, Q must be equal   *)
+(* to P except that every free variable of Q, say x, is replaced by pi o x. In the   *)
+(* equality case, say lhs = rhs, the lhs must be of the form pi o t and the rhs must *)
+(* be equal to t except that every free variable, say x, is replaced by pi o x. In   *)
+(* 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     *)
+(* eqality-lemma can be derived. *)
+exception EQVT_FORM;
+
+val print_eqvtset = Data.print o Context.Proof;
+
+(* FIXME: should be a function in a library *)
+fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T));
+
+val perm_bool = thm "perm_bool";
+
+val EQVT_DEBUG = ref false;
+
+fun tactic (msg,tac) = 
+    if !EQVT_DEBUG 
+    then (EVERY [tac, print_tac ("after "^msg)])
+    else tac 
+
+fun tactic_eqvt ctx orig_thm pi typi = 
+    let 
+        val mypi = Thm.cterm_of ctx (Var (pi,typi))
+        val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi))
+        val perm_pi_simp = PureThy.get_thms ctx (Name "perm_pi_simp")
+    in
+        EVERY [tactic ("iffI applied",rtac iffI 1), 
+               tactic ("simplifies with orig_thm and perm_bool", 
+                          asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1), 
+               tactic ("applies orig_thm instantiated with rev pi",
+                          dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1), 
+               tactic ("getting rid of all remaining perms",
+                          full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)] 
+    end;
+
+fun get_derived_thm thy hyp concl orig_thm pi typi =
+   let 
+       val lhs = (Const("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ Var(pi,typi) $ hyp)
+       val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl))) 
+       val _ = Display.print_cterm (cterm_of thy goal_term) 
+   in	
+     Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi)) 
+   end
+
+(* FIXME: something naughty here, but as long as there is no infrastructure to expose *)
+(* the eqvt_thm_list to the user, we have to manually update the context and the      *)
+(* thm-list eqvt *)
+fun update_context flag thms context =
+  let 
+     val context' = fold (fn thm => Data.map (flag thm)) thms context 
+  in 
+    Context.mapping (snd o PureThy.add_thmss [(("eqvt",Data.get context'),[])]) I context'
+  end;
+
+(* replaces every variable, say 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;
+
+(* 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,[]),_])]))) $ 
+               (Var (n,ty))) => 
+             let
+		(* FIXME: this should be an operation the library *)
+                val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm) 
+	     in 
+		if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name])) 
+                then [(pi,typi)] 
+                else raise EQVT_FORM 
+             end 
+        | Abs (_,_,t1) => get_pi_aux t1
+        | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2
+        | _ => [])  
+  in 
+    (* collect first all pi's in front of variables in t and then use distinct *)
+    (* 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)
+    | _ => raise EQVT_FORM)
+  end;
+
+(* Either adds a theorem (orig_thm) to or deletes one from the equivaraince *)
+(* lemma list depending on flag. To be added the lemma has to satisfy a     *)
+(* certain form. *) 
+fun eqvt_add_del_aux flag orig_thm context =
+  let 
+    val thy = Context.theory_of context
+    val thms_to_be_added = (case (prop_of orig_thm) of
+        (* case: eqvt-lemma is of the implicational form *) 
+        (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) =>
+          let  
+            val (pi,typi) = get_pi concl thy
+          in
+             if (apply_pi hyp (pi,typi) = concl)
+             then 
+               (warning ("equivariance lemma of the relational form");
+                [orig_thm, get_derived_thm thy hyp concl orig_thm pi typi])
+             else raise EQVT_FORM
+          end
+        (* case: eqvt-lemma is of the equational form *)  
+      | (Const ("Trueprop", _) $ (Const ("op =", _) $ 
+            (Const ("Nominal.perm",_) $ Var (pi,typi) $ lhs) $ rhs)) =>
+	      (if (apply_pi lhs (pi,typi)) = rhs 
+               then [orig_thm] 
+               else raise EQVT_FORM)
+      | _ => raise EQVT_FORM)
+  in 
+      update_context flag thms_to_be_added context
+  end
+  handle EQVT_FORM => 
+      error (string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma.")
+
+val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux Drule.add_rule); 
+val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux Drule.del_rule);
+
+val setup =
+  Data.init #>
+  Attrib.add_attributes [("eqvt", Attrib.add_del_args eqvt_add eqvt_del, "equivariance rules")];
+
+end;
+
+
+
+signature BIJ_RULES =
+sig
+  val print_bijset: Proof.context -> unit
+  val bij_add: attribute
+  val bij_del: attribute
+  val setup: theory -> theory
+end;
+
+structure BijRules: BIJ_RULES =
+struct
+
+structure Data = GenericDataFun
+(
+  val name = "HOL/Nominal/bij";
+  type T = thm list;
+  val empty = [];
+  val extend = I;
+  fun merge _ = Drule.merge_rules;
+  fun print context rules =
+    Pretty.writeln (Pretty.big_list "Bijection lemmas:"
+      (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
+);
+
+val print_bijset = Data.print o Context.Proof;
+
+fun bij_add_del_aux f = fn th => fn context =>
+   let val new_context = Data.map (f th) context
+   in 
+       Context.mapping (snd o PureThy.add_thmss [(("bij",Data.get new_context),[])]) I new_context
+   end
+
+val bij_add = Thm.declaration_attribute (bij_add_del_aux Drule.add_rule); 
+val bij_del = Thm.declaration_attribute (bij_add_del_aux Drule.del_rule);
+
+val setup =
+  Data.init #>
+  Attrib.add_attributes [("bij", Attrib.add_del_args bij_add bij_del, "bijection rules")];
+
+end;
+
+
+signature FRESH_RULES =
+sig
+  val print_freshset: Proof.context -> unit
+  val fresh_add: attribute
+  val fresh_del: attribute
+  val setup: theory -> theory
+end;
+
+structure FreshRules: FRESH_RULES =
+struct
+
+structure Data = GenericDataFun
+(
+  val name = "HOL/Nominal/fresh";
+  type T = thm list;
+  val empty = [];
+  val extend = I;
+  fun merge _ = Drule.merge_rules;
+  fun print context rules =
+    Pretty.writeln (Pretty.big_list "Freshness lemmas:"
+      (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
+);
+
+val print_freshset = Data.print o Context.Proof;
+
+fun fresh_add_del_aux f = fn th => fn context =>
+   let val new_context = Data.map (f th) context
+   in 
+       Context.mapping (snd o PureThy.add_thmss [(("fresh",Data.get new_context),[])]) I new_context
+   end
+
+val fresh_add = Thm.declaration_attribute (fresh_add_del_aux Drule.add_rule); 
+val fresh_del = Thm.declaration_attribute (fresh_add_del_aux Drule.del_rule);
+
+val setup =
+  Data.init #>
+  Attrib.add_attributes [("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness rules")];
+
+end;
+
+(* Thm.declaration_attribute is of type (thm -> Context.generic -> Context.generic) -> attribute *)
+
+(* Thm.declaration_attribute has type (thm -> Context.generic -> Context.generic) -> attribute *)
+
+(* Drule.add_rule has type thm -> thm list -> thm list *)
+
+(* Data.map has type thm list -> thm list -> Context.generic -> Context.generic *)
+
+(* add_del_args is of type attribute -> attribute -> src -> attribute *)
\ No newline at end of file