# HG changeset patch
# User narboux
# Date 1175936725 -7200
# Node ID 40ade470e3193dcaf2b1240c3aca001fac0d7c59
# Parent  092a3353241ec90b4c83d5e3fb6892d3270ef1da
perm_simp can now simplify using the rules (a,b) o a = b  and (a,b) o b = a

diff -r 092a3353241e -r 40ade470e319 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Fri Apr 06 01:26:30 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Sat Apr 07 11:05:25 2007 +0200
@@ -318,8 +318,9 @@
 inductive_cases2 t_Lam_elim_auto[elim]: "\<Gamma> \<turnstile> Lam [x].t : T"
 inductive_cases2 t_Var_elim_auto[elim]: "\<Gamma> \<turnstile> Var x : T"
 inductive_cases2 t_App_elim_auto[elim]: "\<Gamma> \<turnstile> App x y : T"
-inductive_cases2  t_Const_elim_auto[elim]: "\<Gamma> \<turnstile> Const n : T"
-inductive_cases2  t_Unit_elim_auto[elim]: "\<Gamma> \<turnstile> Unit : TUnit"
+inductive_cases2 t_Const_elim_auto[elim]: "\<Gamma> \<turnstile> Const n : T"
+inductive_cases2 t_Unit_elim_auto[elim]: "\<Gamma> \<turnstile> Unit : TUnit"
+inductive_cases2 t_Unit_elim_auto'[elim]: "\<Gamma> \<turnstile> s : TUnit"
 
 declare trm.inject [simp del]
 declare ty.inject [simp del]
@@ -479,12 +480,6 @@
 declare trm.inject [simp del]
 declare ty.inject [simp del]
 
-(* FIXME this lemma should not be here *)
-lemma perm_basic[simp]:
- fixes x y::"name"
-shows "[(x,y)]\<bullet>y = x"
-using assms using calc_atm by perm_simp
-
 lemma Q_Arrow_strong_inversion:
   assumes fs: "x\<sharp>\<Gamma>" "x\<sharp>t" "x\<sharp>u" 
   and h: "\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2"
diff -r 092a3353241e -r 40ade470e319 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Fri Apr 06 01:26:30 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Sat Apr 07 11:05:25 2007 +0200
@@ -1090,6 +1090,20 @@
 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 092a3353241e -r 40ade470e319 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Fri Apr 06 01:26:30 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Apr 07 11:05:25 2007 +0200
@@ -694,6 +694,8 @@
        val at_fresh            = thm "Nominal.at_fresh";
        val at_fresh_ineq       = thm "Nominal.at_fresh_ineq";
        val at_calc             = thms "Nominal.at_calc";
+       val swap_simp_a         = thm "swap_simp_a";
+       val swap_simp_b         = thm "swap_simp_b";
        val at_supp             = thm "Nominal.at_supp";
        val dj_supp             = thm "Nominal.dj_supp";
        val fresh_left_ineq     = thm "Nominal.pt_fresh_left_ineq";
@@ -800,6 +802,8 @@
             ||>> 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 092a3353241e -r 40ade470e319 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Fri Apr 06 01:26:30 2007 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Apr 07 11:05:25 2007 +0200
@@ -153,7 +153,7 @@
     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"] (fn st => []);
+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;
 
 (* FIXME removes the name lookup for these theorems use an ml value instead *)