# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1325181913 0
# Node ID 09acd7e116e8c940da9f5a97a292f01ae7e75cae
# Parent  8779fb01d8b42c438857b7d490ae8c9b938821f5
added two eqvt lemmas for fset-operators

diff -r 8779fb01d8b4 -r 09acd7e116e8 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Thu Dec 29 15:56:54 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Thu Dec 29 18:05:13 2011 +0000
@@ -1,5 +1,5 @@
 (*  Title:      Nominal2_Base
-    Authors:    Brian Huffman, Christian Urban
+    Authors:    Christian Urban, Brian Huffman, Cezary Kaliszyk
 
     Basic definitions and lemma infrastructure for 
     Nominal Isabelle. 
@@ -1110,6 +1110,22 @@
   shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
   by (induct S) (simp_all)
 
+lemma inter_fset_eqvt [eqvt]:
+  shows "(p \<bullet> (S |\<inter>| T)) = ((p \<bullet> S) |\<inter>| (p \<bullet> T))"
+  apply(descending)
+  unfolding list_eq_def inter_list_def
+  apply(perm_simp)
+  apply(simp)
+  done
+
+lemma subset_fset_eqvt [eqvt]:
+  shows "(p \<bullet> (S |\<subseteq>| T)) = ((p \<bullet> S) |\<subseteq>| (p \<bullet> T))"
+  apply(descending)
+  unfolding sub_list_def
+  apply(perm_simp)
+  apply(simp)
+  done
+  
 lemma map_fset_eqvt [eqvt]: 
   shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
   by (lifting map_eqvt)