# HG changeset patch
# User narboux
# Date 1177425851 -7200
# Node ID fab155c8ce4678b5e6ac11ba5cd14652e765b283
# Parent  4637b69de71bcfec4e514e2babd0f74efcf1d1d1
add two lemmas dealing with freshness on permutations.

diff -r 4637b69de71b -r fab155c8ce46 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Tue Apr 24 15:19:33 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Tue Apr 24 16:44:11 2007 +0200
@@ -3044,6 +3044,39 @@
   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 4637b69de71b -r fab155c8ce46 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Tue Apr 24 15:19:33 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Apr 24 16:44:11 2007 +0200
@@ -716,8 +716,9 @@
        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";	
+  
        (* 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,7 +859,11 @@
             ||>> 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
+	      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
             ||>> PureThy.add_thmss [(("fin_supp",fs_axs),[])]
 	   end;