# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1302392512 -28800
# Node ID 8f833ebc4b58e6a76314984bff9777ca1e3d3910
# Parent  aeda59ca0d4c4ecc3eb175edb9e2f0d4be093b36
eqvt of supp and fresh is proved using equivariance infrastructure

diff -r aeda59ca0d4c -r 8f833ebc4b58 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Sun Apr 10 04:07:15 2011 +0800
+++ b/Nominal/Nominal2_Base.thy	Sun Apr 10 07:41:52 2011 +0800
@@ -1092,36 +1092,21 @@
 
 subsection {* supp and fresh are equivariant *}
 
-lemma finite_Collect_bij:
-  assumes a: "bij f"
-  shows "finite {x. P (f x)} = finite {x. P x}"
-by (metis a finite_vimage_iff vimage_Collect_eq)
+
+lemma supp_eqvt [eqvt]:
+  shows "p \<bullet> (supp x) = supp (p \<bullet> x)"
+  unfolding supp_def
+  by (perm_simp)
+     (simp only: permute_eqvt[symmetric])
+
+lemma fresh_eqvt [eqvt]:
+  shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)"
+  unfolding fresh_def
+  by (perm_simp) (rule refl)
 
 lemma fresh_permute_iff:
   shows "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x"
-proof -
-  have "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> finite {b. (p \<bullet> a \<rightleftharpoons> b) \<bullet> p \<bullet> x \<noteq> p \<bullet> x}"
-    unfolding fresh_def supp_def by simp
-  also have "\<dots> \<longleftrightarrow> finite {b. (p \<bullet> a \<rightleftharpoons> p \<bullet> b) \<bullet> p \<bullet> x \<noteq> p \<bullet> x}"
-    using bij_permute by (rule finite_Collect_bij[symmetric])
-  also have "\<dots> \<longleftrightarrow> finite {b. p \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> p \<bullet> x}"
-    by (simp only: permute_eqvt [of p] swap_eqvt)
-  also have "\<dots> \<longleftrightarrow> finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"
-    by (simp only: permute_eq_iff)
-  also have "\<dots> \<longleftrightarrow> a \<sharp> x"
-    unfolding fresh_def supp_def by simp
-  finally show "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x" .
-qed
-
-lemma fresh_eqvt [eqvt]:
-  shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)"
-  unfolding permute_bool_def
-  by (simp add: fresh_permute_iff)
-
-lemma supp_eqvt [eqvt]:
-  shows "p \<bullet> (supp x) = supp (p \<bullet> x)"
-  unfolding supp_conv_fresh
-  by (perm_simp) (rule refl)
+  by (simp only: fresh_eqvt[symmetric] permute_bool_def)
 
 lemma fresh_permute_left:
   shows "a \<sharp> p \<bullet> x \<longleftrightarrow> - p \<bullet> a \<sharp> x"