# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1300116959 -3600
# Node ID 7085ab735de77a94cc35bd01bcd37e6bcefc73b0
# Parent  f1192e3474e02eb2cf394aa29a7fb16c407080db
equivariance for All and Ex can be proved in terms of their definition

diff -r f1192e3474e0 -r 7085ab735de7 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Fri Mar 11 08:51:39 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Mon Mar 14 16:35:59 2011 +0100
@@ -810,17 +810,17 @@
 
 declare imp_eqvt[folded induct_implies_def, eqvt]
 
+lemma all_eqvt [eqvt]:
+  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
+  unfolding All_def
+  by (perm_simp) (rule refl)
+
+declare all_eqvt[folded induct_forall_def, eqvt]
+
 lemma ex_eqvt [eqvt]:
   shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
-  unfolding permute_fun_def permute_bool_def
-  by (auto, rule_tac x="p \<bullet> x" in exI, simp)
-
-lemma all_eqvt [eqvt]:
-  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
-  unfolding permute_fun_def permute_bool_def
-  by (auto, drule_tac x="p \<bullet> x" in spec, simp)
-
-declare all_eqvt[folded induct_forall_def, eqvt]
+  unfolding Ex_def
+  by (perm_simp) (rule refl)
 
 lemma ex1_eqvt [eqvt]:
   shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
@@ -2559,6 +2559,13 @@
 apply(auto)
 done
 
+(* FIXME 
+lemma supp_cofinite_set_at_base:
+  assumes a: "finite (UNIV - S)"
+  shows "supp S = atom ` (UNIV - S)"
+apply(rule finite_supp_unique)
+*)
+
 lemma fresh_finite_set_at_base:
   fixes a::"'a::at_base"
   assumes a: "finite S"