src/HOL/Nominal/Nominal.thy

   shows "swap (a,b) c = (if a=c then b else (if b=c then a else c))"
   using a by (simp only: at_def)
 
 (* rules to calculate simple premutations *)
 lemmas at_calc = at2 at1 at3
+
+lemma at_swap_simps:
+  fixes a ::"'x"
+  and   b ::"'x"
+  assumes a: "at TYPE('x)"
+  shows "[(a,b)]\<bullet>a = b"
+  and   "[(a,b)]\<bullet>b = a"
+  using a by (simp_all add: at_calc)
 
 lemma at4: 
   assumes a: "at TYPE('x)"
   shows "infinite (UNIV::'x set)"
   using a by (simp add: at_def)

 apply(simp_all add: pt3[OF pta])
 done
 
 section {* further lemmas for permutation types *}
 (*==============================================*)
-
-lemma swap_simp_a:
-  fixes a ::"'x"
-  and   b ::"'x"
-  assumes a: "at TYPE('x)"
-  shows "[(a,b)]\<bullet> a = b" 
-  using a by (auto simp add:at_calc)
-
-lemma swap_simp_b:
-  fixes a ::"'x"
-  and   b ::"'x"
-  assumes a: "at TYPE('x)"
-  shows "[(a,b)]\<bullet> b = a" 
-  using a by (auto simp add:at_calc)
 
 lemma pt_rev_pi:
   fixes pi :: "'x prm"
   and   x  :: "'a"
   assumes pt: "pt TYPE('a) TYPE('x)"