# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1294920767 0
# Node ID b4472ebd7fadab0123d48d411c938bc48a04c585
# Parent  1ea9c059fc0f77751f3b44efa92b303dfb19f357
added eqvt_lemmas for subset and psubset

diff -r 1ea9c059fc0f -r b4472ebd7fad Nominal/Nominal2_Eqvt.thy
--- a/Nominal/Nominal2_Eqvt.thy	Mon Jan 10 11:36:55 2011 +0000
+++ b/Nominal/Nominal2_Eqvt.thy	Thu Jan 13 12:12:47 2011 +0000
@@ -195,6 +195,16 @@
   unfolding Compl_eq_Diff_UNIV
   by (perm_simp) (rule refl)
 
+lemma subset_eqvt[eqvt]:
+  shows "p \<bullet> (S \<subseteq> T) \<longleftrightarrow> (p \<bullet> S) \<subseteq> (p \<bullet> T)"
+  unfolding subset_eq
+  by (perm_simp) (rule refl)
+
+lemma psubset_eqvt[eqvt]:
+  shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)"
+  unfolding psubset_eq
+  by (perm_simp) (rule refl)
+
 lemma image_eqvt:
   shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
   unfolding permute_set_eq_image