# HG changeset patch
# User urbanc
# Date 1149527380 -7200
# Node ID 45897b49fdd2980e3e05211706fac03b18e3d16f
# Parent  b4a0da62126e922c4834a7e16a527f52907b14d7
added some further lemmas that deal with permutations and set-operators

diff -r b4a0da62126e -r 45897b49fdd2 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Jun 05 18:38:41 2006 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Mon Jun 05 19:09:40 2006 +0200
@@ -985,15 +985,6 @@
 section {* further lemmas for permutation types *}
 (*==============================================*)
 
-lemma perm_diff:
-  fixes X::"'a set"
-  and   Y::"'a set"
-  and   pi::"'x prm"
-  assumes pt: "pt TYPE('a) TYPE('x)"
-  and     at: "at TYPE('x)"
-  shows "pi \<bullet> (X - Y) = (pi \<bullet> X) - (pi \<bullet> Y)"
-  by (auto simp add: perm_set_def pt_bij[OF pt, OF at])
-
 lemma pt_rev_pi:
   fixes pi :: "'x prm"
   and   x  :: "'a"
@@ -1171,6 +1162,16 @@
   thus "x\<in>(pi\<bullet>Y)" by (force simp add: pt_set_bij1a[OF pt, OF at])
 qed
 
+lemma pt_set_diff_eqvt:
+  fixes X::"'a set"
+  and   Y::"'a set"
+  and   pi::"'x prm"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  shows "pi \<bullet> (X - Y) = (pi \<bullet> X) - (pi \<bullet> Y)"
+  by (auto simp add: perm_set_def pt_bij[OF pt, OF at])
+
+
 -- "some helper lemmas for the pt_perm_supp_ineq lemma"
 lemma Collect_permI: 
   fixes pi :: "'x prm"