# HG changeset patch
# User urbanc
# Date 1131973198 -3600
# Node ID 08282ca0402e7771e2b35a66885f8c74eb6e5ab7
# Parent  57cba2a340f2c6b46168ac8caf77351fa348dedf
added a few equivariance lemmas (they need to be automated
eventually)

diff -r 57cba2a340f2 -r 08282ca0402e src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Sun Nov 13 22:36:30 2005 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Mon Nov 14 13:59:58 2005 +0100
@@ -922,6 +922,27 @@
 apply(auto)
 done
 
+lemma pt_subseteq_eqvt:
+  fixes pi :: "'x prm"
+  and   Y  :: "'a set"
+  and   X  :: "'a set"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  shows "((pi\<bullet>X)\<subseteq>(pi\<bullet>Y)) = (X\<subseteq>Y)"
+proof (auto)
+  fix x::"'a"
+  assume a: "(pi\<bullet>X)\<subseteq>(pi\<bullet>Y)"
+  and    "x\<in>X"
+  hence  "(pi\<bullet>x)\<in>(pi\<bullet>X)" by (simp add: pt_set_bij[OF pt, OF at])
+  with a have "(pi\<bullet>x)\<in>(pi\<bullet>Y)" by force
+  thus "x\<in>Y" by (simp add: pt_set_bij[OF pt, OF at])
+next
+  fix x::"'a"
+  assume a: "X\<subseteq>Y"
+  and    "x\<in>(pi\<bullet>X)"
+  thus "x\<in>(pi\<bullet>Y)" by (force simp add: pt_set_bij1a[OF pt, OF at])
+qed
+
 lemma pt_list_set_pi:
   fixes pi :: "'x prm"
   and   xs :: "'a list"