# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295456849 -3600
# Node ID 2873b3230c4403f913a4dc1545809f23320329d3
# Parent  0e4c5fa26fa1676b2c543d88e3bd6b422f75a7a6
added eqvt and supp lemma for removeAll (function from List.thy)

diff -r 0e4c5fa26fa1 -r 2873b3230c44 Nominal/Nominal2_Eqvt.thy
--- a/Nominal/Nominal2_Eqvt.thy	Wed Jan 19 17:54:50 2011 +0100
+++ b/Nominal/Nominal2_Eqvt.thy	Wed Jan 19 18:07:29 2011 +0100
@@ -244,6 +244,16 @@
   shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
   by (induct xs) (simp_all, simp only: permute_fun_app_eq)
 
+lemma removeAll_eqvt[eqvt]:
+  shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
+  by (induct xs) (auto)
+
+lemma supp_removeAll:
+  fixes x::"atom"
+  shows "supp (removeAll x xs) = supp xs - {x}"
+  by (induct xs)
+     (auto simp add: supp_Nil supp_Cons supp_atom)
+
 
 subsection {* Equivariance Finite-Set Operations *}