# HG changeset patch
# User narboux
# Date 1177427815 -7200
# Node ID d8d7a53ffb63032e487bc27331792e913fdff7d5
# Parent  fab155c8ce4678b5e6ac11ba5cd14652e765b283
fixes last commit

diff -r fab155c8ce46 -r d8d7a53ffb63 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Tue Apr 24 16:44:11 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Tue Apr 24 17:16:55 2007 +0200
@@ -1578,6 +1578,7 @@
 
 (* the next two lemmas are needed in the proof *)
 (* of the structural induction principle       *)
+
 lemma pt_fresh_aux:
   fixes a::"'x"
   and   b::"'x"
@@ -1589,7 +1590,24 @@
   shows "c\<sharp>([(a,b)]\<bullet>x)"
 using a1 a2 a3 by (simp_all add: pt_fresh_left[OF pt, OF at] at_calc[OF at])
 
-lemma pt_fresh_aux_ineq:
+lemma pt_fresh_perm_app:
+  fixes pi :: "'x prm" 
+  and   a  :: "'x"
+  and   x  :: "'y"
+  assumes pt: "pt TYPE('y) TYPE('x)"
+  and     at: "at TYPE('x)"
+  and     h1: "a \<sharp> pi"
+  and     h2: "a \<sharp> x"
+  shows "a \<sharp> (pi \<bullet> x)"
+using assms
+proof -
+  have "a \<sharp> rev pi"using h1 by (simp add: fresh_list_rev)
+  then have "(rev pi) \<bullet> a = a" by (simp add: at_prm_fresh[OF at])
+  then have "((rev pi) \<bullet> a) \<sharp> x" using h2 by simp
+  thus "a \<sharp> (pi \<bullet> x)"  by (simp add: pt_fresh_right[OF pt, OF at])
+qed
+
+lemma pt_fresh_perm_app_ineq:
   fixes pi::"'x prm"
   and   c::"'y"
   and   x::"'a"
@@ -3044,39 +3062,6 @@
   shows "((pi\<bullet>(\<lambda>x. f x))=y) = ((\<lambda>x. (pi\<bullet>(f ((rev pi)\<bullet>x))))=y)"
   by (simp add: perm_fun_def)
 
-lemma pt_perm_fresh_app:
-  fixes pi :: "'x prm" 
-  and   a  :: "'x"
-  and   x  :: "'y"
-  assumes at: "at TYPE('x)"
-  and     pt: "pt TYPE('y) TYPE('x)"
-  and     h1: "a \<sharp> pi"
-  and     h2: "a \<sharp> x"
-  shows "a \<sharp> (pi \<bullet> x)"
-using assms
-proof -
-  have "a \<sharp> rev pi"using h1 by (simp add: fresh_list_rev)
-  then have "(rev pi) \<bullet> a = a" by (simp add: at_prm_fresh[OF at])
-  then have "((rev pi) \<bullet> a) \<sharp> x" using h2 by simp
-  thus "a \<sharp> (pi \<bullet> x)"  by (simp add: pt_fresh_right[OF pt, OF at])
-qed
-
-lemma pt_perm_fresh_app_ineq:
-  fixes pi :: "'x prm" 
-  and   a  :: "'y"
-  and   x  :: "'z"
-  assumes pta: "pt TYPE('z) TYPE('x)" 
-  and     ptb: "pt TYPE('y) TYPE('x)"
-  and     at:  "at TYPE('x)"
-  and     cp:  "cp TYPE('z) TYPE('x) TYPE('y)"
-  and     dj:  "disjoint TYPE('y) TYPE('x)"
-  assumes h:"a \<sharp> x"
-  shows "a \<sharp> pi \<bullet> x"
-  apply -
-  apply (rule pt_fresh_left_ineq[THEN iffD2],assumption+)
-  apply (simp add: dj_perm_forget[OF dj],assumption)
-done
-
 section {* test *}
 lemma at_prm_eq_compose:
   fixes pi1 :: "'x prm"
diff -r fab155c8ce46 -r d8d7a53ffb63 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Tue Apr 24 16:44:11 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Apr 24 17:16:55 2007 +0200
@@ -703,8 +703,6 @@
        val fresh_right         = thm "Nominal.pt_fresh_right";
        val fresh_bij_ineq      = thm "Nominal.pt_fresh_bij_ineq";
        val fresh_bij           = thm "Nominal.pt_fresh_bij";
-       val fresh_aux_ineq      = thm "Nominal.pt_fresh_aux_ineq";
-       val fresh_aux           = thm "Nominal.pt_fresh_aux";
        val fresh_eqvt          = thm "Nominal.pt_fresh_eqvt";
        val fresh_eqvt_ineq     = thm "Nominal.pt_fresh_eqvt_ineq";
        val set_diff_eqvt       = thm "Nominal.pt_set_diff_eqvt";
@@ -716,9 +714,10 @@
        val pt_rev_pi           = thm "Nominal.pt_rev_pi";
        val at_exists_fresh     = thm "Nominal.at_exists_fresh";
        val at_exists_fresh'    = thm "Nominal.at_exists_fresh'";
-       val fresh_perm_app_ineq = thm "pt_fresh_perm_app_ineq";
-       val fresh_perm_app      = thm "pt_fresh_perm_app";	
-  
+       val fresh_perm_app_ineq = thm "Nominal.pt_fresh_perm_app_ineq";
+       val fresh_perm_app      = thm "Nominal.pt_fresh_perm_app";	
+       val fresh_aux           = thm "Nominal.pt_fresh_aux";  
+
        (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
        (* types; this allows for example to use abs_perm (which is a      *)
        (* collection of theorems) instead of thm abs_fun_pi with explicit *)
@@ -858,12 +857,12 @@
 	      in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
             ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at [fresh_aux]
-		  and thms2 = inst_pt_pt_at_cp_dj [fresh_aux_ineq]
-	      in [(("fresh_aux", thms1 @ thms2),[])] end  
+		  and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
+	      in  [(("fresh_aux", thms1 @ thms2),[])] end  
             ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at [fresh_perm_app]
-		  and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq]
-	      in [(("fresh_perm_app", thms1 @ thms2),[])] end
+		  and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
+	      in  [(("fresh_perm_app", thms1 @ thms2),[])] end  
             ||>> PureThy.add_thmss [(("fin_supp",fs_axs),[])]
 	   end;