# HG changeset patch
# User urbanc
# Date 1175938595 -7200
# Node ID c8b5133045f396a57ff8b729933bf03aabf36f92
# Parent  40ade470e3193dcaf2b1240c3aca001fac0d7c59
tuned slightly the previous commit

diff -r 40ade470e319 -r c8b5133045f3 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Sat Apr 07 11:05:25 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Sat Apr 07 11:36:35 2007 +0200
@@ -443,6 +443,14 @@
 (* 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)"
@@ -1090,20 +1098,6 @@
 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"
diff -r 40ade470e319 -r c8b5133045f3 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sat Apr 07 11:05:25 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Apr 07 11:36:35 2007 +0200
@@ -694,6 +694,7 @@
        val at_fresh            = thm "Nominal.at_fresh";
        val at_fresh_ineq       = thm "Nominal.at_fresh_ineq";
        val at_calc             = thms "Nominal.at_calc";
+       val at_swap_simps       = thms "Nominal.at_swap_simps";
        val swap_simp_a         = thm "swap_simp_a";
        val swap_simp_b         = thm "swap_simp_b";
        val at_supp             = thm "Nominal.at_supp";
@@ -787,6 +788,7 @@
 	    |>   PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
             ||>> PureThy.add_thmss [(("alpha'", inst_pt_at [abs_fun_eq']),[])]
             ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])]
+            ||>> PureThy.add_thmss [(("swap_simps", inst_at at_swap_simps),[])]	 
             ||>> PureThy.add_thmss 
 	      let val thms1 = inst_pt_at [pt_pi_rev];
 		  val thms2 = inst_pt_at [pt_rev_pi];
@@ -802,8 +804,6 @@
             ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
             ||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])]
             ||>> PureThy.add_thmss [(("exists_fresh'", inst_at [at_exists_fresh']),[])]
-            ||>> PureThy.add_thmss [(("swap_simp_a", inst_at [swap_simp_a]),[])]	 
-            ||>> PureThy.add_thmss [(("swap_simp_b", inst_at [swap_simp_b]),[])]
             ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[NominalThmDecls.eqvt_add])] 
             ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_add])]
             ||>> PureThy.add_thmss 
diff -r 40ade470e319 -r c8b5133045f3 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Sat Apr 07 11:05:25 2007 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Apr 07 11:36:35 2007 +0200
@@ -71,7 +71,6 @@
 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"]
@@ -153,8 +152,18 @@
     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","swap_simp_a","swap_simp_b"] (fn st => []);
-val eqvt_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_pi_simp"] eqvts_thms;
+val perm_simp = 
+    let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"]
+    in 
+	perm_simp_gen simps (fn st => [])
+    end;
+
+val eqvt_simp = 
+    let val simps = ["perm_swap","perm_fresh_fresh","perm_pi_simp"]
+	fun eqvts_thms st = NominalThmDecls.get_eqvt_thms (theory_of_thm st);
+    in 
+	perm_simp_gen simps eqvts_thms
+    end;
 
 (* FIXME removes the name lookup for these theorems use an ml value instead *)