# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295367590 -3600
# Node ID 7e76628904773360f2f28b3ab9c3e3cf728802a8
# Parent  eef49daac6c8644abc2af9a8120537d9f00c413c
removed finiteness assumption from set_rename_perm

diff -r eef49daac6c8 -r 7e7662890477 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Tue Jan 18 22:11:49 2011 +0900
+++ b/Nominal/Nominal2_Base.thy	Tue Jan 18 17:19:50 2011 +0100
@@ -549,6 +549,21 @@
   shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
   unfolding permute_set_eq_image image_insert ..
 
+lemma Collect_eqvt:
+  shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
+  unfolding Collect_def permute_fun_def ..
+
+lemma inter_eqvt:
+  shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
+  unfolding Int_def
+  apply(simp add: Collect_eqvt)
+  apply(simp add: permute_fun_def)
+  apply(simp add: conj_eqvt)
+  apply(simp add: mem_eqvt)
+  apply(simp add: permute_fun_def)
+  done
+
+
 
 subsection {* Permutations for units *}
 
@@ -1997,7 +2012,29 @@
     by blast
 qed
 
-
+lemma set_renaming_perm2:
+  shows "\<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
+proof -
+  have "finite (bs \<inter> supp p)" by (simp add: finite_supp)
+  then obtain q 
+    where *: "\<forall>b \<in> bs \<inter> supp p. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> (bs \<inter> supp p) \<union> (p \<bullet> (bs \<inter> supp p))"
+    using set_renaming_perm by blast
+  from ** have "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by (auto simp add: inter_eqvt)
+  moreover
+  have "\<forall>b \<in> bs - supp p. q \<bullet> b = p \<bullet> b" 
+    apply(auto)
+    apply(subgoal_tac "b \<notin> supp q")
+    apply(simp add: fresh_def[symmetric])
+    apply(simp add: fresh_perm)
+    apply(clarify)
+    apply(rotate_tac 2)
+    apply(drule subsetD[OF **])
+    apply(simp add: inter_eqvt supp_eqvt permute_self)
+    done
+  ultimately have "(\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" using * by auto
+  then show "\<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
+qed
+    
 lemma list_renaming_perm:
   shows "\<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> (p \<bullet> set bs)"
 proof (induct bs)
diff -r eef49daac6c8 -r 7e7662890477 Nominal/Nominal2_Eqvt.thy
--- a/Nominal/Nominal2_Eqvt.thy	Tue Jan 18 22:11:49 2011 +0900
+++ b/Nominal/Nominal2_Eqvt.thy	Tue Jan 18 17:19:50 2011 +0100
@@ -36,7 +36,7 @@
   Pair_eqvt permute_list.simps permute_option.simps
 
   (* sets *)
-  mem_eqvt empty_eqvt insert_eqvt set_eqvt
+  mem_eqvt empty_eqvt insert_eqvt set_eqvt inter_eqvt
 
   (* fsets *)
   permute_fset fset_eqvt
@@ -173,11 +173,6 @@
   unfolding Un_def
   by (perm_simp) (rule refl)
 
-lemma inter_eqvt[eqvt]:
-  shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
-  unfolding Int_def 
-  by (perm_simp) (rule refl)
-
 lemma Diff_eqvt[eqvt]:
   fixes A B :: "'a::pt set"
   shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"