# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272633678 -3600
# Node ID 74d869595fed8e987e12cdf7f3ecb069d2136054
# Parent  bc075a4ef02f0d157e6e5e60c52a5333229f4649
added eqvt-lemmas for Bex, Ball and Union

diff -r bc075a4ef02f -r 74d869595fed Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Fri Apr 30 10:32:34 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Fri Apr 30 14:21:18 2010 +0100
@@ -156,6 +156,16 @@
   shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}"
   by (perm_simp add: permute_minus_cancel) (rule refl)
 
+lemma Bex_eqvt[eqvt]:
+  shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+  unfolding Bex_def
+  by (perm_simp) (rule refl)
+
+lemma Ball_eqvt[eqvt]:
+  shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+  unfolding Ball_def
+  by (perm_simp) (rule refl)
+
 lemma empty_eqvt[eqvt]:
   shows "p \<bullet> {} = {}"
   unfolding empty_def
@@ -206,6 +216,11 @@
   unfolding vimage_def
   by (perm_simp) (rule refl)
 
+lemma Union_eqvt[eqvt]:
+  shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
+  unfolding Union_eq 
+  by (perm_simp) (rule refl)
+
 lemma finite_permute_iff:
   shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
   unfolding permute_set_eq_vimage