author urbanc Mon, 05 Jun 2006 19:09:40 +0200 changeset 19772 45897b49fdd2 parent 19771 b4a0da62126e child 19773 ebc3b67fbd2c
added some further lemmas that deal with permutations and set-operators
```--- 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"```