# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1297865006 0
# Node ID e6bf6790da7d9c11ccfee1208dfa8ccba19516a7
# Parent  281ef8686654178bf645d28c27aec6fd8024c589
added eqvt lemmas for filter and distinct

diff -r 281ef8686654 -r e6bf6790da7d Nominal/Nominal2_Eqvt.thy
--- a/Nominal/Nominal2_Eqvt.thy	Mon Feb 07 16:00:24 2011 +0000
+++ b/Nominal/Nominal2_Eqvt.thy	Wed Feb 16 14:03:26 2011 +0000
@@ -260,6 +260,21 @@
   by (induct xs)
      (auto simp add: supp_Nil supp_Cons supp_atom)
 
+lemma filter_eqvt[eqvt]:
+  shows "p \<bullet> (filter f xs) = filter (p \<bullet> f) (p \<bullet> xs)"
+apply(induct xs)
+apply(simp)
+apply(simp only: filter.simps permute_list.simps if_eqvt)
+apply(simp only: permute_fun_app_eq)
+done
+
+lemma distinct_eqvt[eqvt]:
+  shows "p \<bullet> (distinct xs) = distinct (p \<bullet> xs)"
+apply(induct xs)
+apply(simp add: permute_bool_def)
+apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt)
+done
+
 
 subsection {* Equivariance Finite-Set Operations *}