# HG changeset patch
# User urbanc
# Date 1175017180 -7200
# Node ID cbee450f88a657fa818e8e023d3167e7a94f4387
# Parent  bd4b954e85ee29288edfb54cb6cf9f84685ebb14
added extended the lemma for equivariance of freshness

diff -r bd4b954e85ee -r cbee450f88a6 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Tue Mar 27 19:13:28 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Tue Mar 27 19:39:40 2007 +0200
@@ -1590,6 +1590,18 @@
   shows "c\<sharp>(pi\<bullet>x)"
 using a by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj])
 
+lemma pt_fresh_eqvt_ineq:
+  fixes pi::"'x prm"
+  and   c::"'y"
+  and   x::"'a"
+  assumes pta: "pt TYPE('a) TYPE('x)"
+  and     ptb: "pt TYPE('y) TYPE('x)"
+  and     at:  "at TYPE('x)"
+  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
+  and     dj:  "disjoint TYPE('y) TYPE('x)"
+  shows "pi\<bullet>(c\<sharp>x) = (pi\<bullet>c)\<sharp>(pi\<bullet>x)"
+by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool)
+
 -- "three helper lemmas for the perm_fresh_fresh-lemma"
 lemma comprehension_neg_UNIV: "{b. \<not> P b} = UNIV - {b. P b}"
   by (auto)
diff -r bd4b954e85ee -r cbee450f88a6 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Tue Mar 27 19:13:28 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Mar 27 19:39:40 2007 +0200
@@ -700,6 +700,7 @@
        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_eqvt            = thm "Nominal.pt_set_eqvt";
        val set_diff_eqvt       = thm "Nominal.pt_set_diff_eqvt";
        val in_eqvt             = thm "Nominal.pt_in_eqvt";
@@ -837,7 +838,8 @@
 	      in [(("fresh_bij", thms1 @ thms2),[])] end
             ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at [fresh_eqvt]
-	      in [(("fresh_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
+                  and thms2 = inst_pt_pt_at_cp_dj [fresh_eqvt_ineq]
+	      in [(("fresh_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end
             ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at [in_eqvt]
 	      in [(("in_eqvt", thms1),[NominalThmDecls.eqvt_add])] end