# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1292745037 0
# Node ID d5713db7e146d01df1b7dc4d16c64b64a0119e53
# Parent  0d7a1703fe28b29dfa859cbbbafda2dac4fb372a
one interesting case done

diff -r 0d7a1703fe28 -r d5713db7e146 Nominal/Ex/Multi_Recs.thy
--- a/Nominal/Ex/Multi_Recs.thy	Sun Dec 19 07:43:32 2010 +0000
+++ b/Nominal/Ex/Multi_Recs.thy	Sun Dec 19 07:50:37 2010 +0000
@@ -43,6 +43,92 @@
 thm multi_recs.fsupp
 thm multi_recs.supp
 
+thm multi_recs.bn_defs
+thm multi_recs.permute_bn
+thm multi_recs.perm_bn_alpha
+thm multi_recs.perm_bn_simps
+thm multi_recs.bn_finite
+
+
+lemma Abs_rename_set2:
+  fixes x::"'a::fs"
+  assumes a: "(p \<bullet> cs) \<sharp>* (cs, x)" 
+  and     b: "finite cs"
+  shows "\<exists>q. [cs]set. x = [p \<bullet> cs]set. (q \<bullet> x) \<and> q \<bullet> cs = p \<bullet> cs \<and> supp q \<subseteq> cs \<union> (p \<bullet> cs)"
+proof -
+  from a b have "p \<bullet> cs \<inter> cs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair)   
+  with set_renaming_perm 
+  obtain q where *: "q \<bullet> cs = p \<bullet> cs" and **: "supp q \<subseteq> cs \<union> (p \<bullet> cs)" using b by metis
+  have "[cs]set. x =  q \<bullet> ([cs]set. x)"
+    apply(rule perm_supp_eq[symmetric])
+    using a **
+    unfolding fresh_star_Pair
+    unfolding Abs_fresh_star_iff
+    unfolding fresh_star_def
+    by auto
+  also have "\<dots> = [q \<bullet> cs]set. (q \<bullet> x)" by simp
+  also have "\<dots> = [p \<bullet> cs]set. (q \<bullet> x)" using * by simp
+  finally have "[cs]set. x = [p \<bullet> cs]set. (q \<bullet> x)" .
+  then show "\<exists>q. [cs]set. x = [p \<bullet> cs]set. (q \<bullet> x) \<and> q \<bullet> cs = p \<bullet> cs \<and> supp q \<subseteq> cs \<union> (p \<bullet> cs)"
+    using * **
+    by (blast)
+qed
+
+lemma at_set_avoiding5:
+  assumes "finite xs"
+  and     "finite (supp c)"
+  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp p = xs \<union> p \<bullet> xs"
+using assms
+apply(erule_tac c="c" in at_set_avoiding)
+apply(auto)
+done
+
+lemma
+  fixes c::"'a::fs"
+  assumes a:  "\<And>lrbs exp. \<lbrakk>bs lrbs \<sharp>* c; y = LetRec lrbs exp\<rbrakk> \<Longrightarrow> P"
+  shows "y = LetRec lrbs exp \<Longrightarrow> P"
+apply -
+apply(subgoal_tac "\<exists>p. ((p \<bullet> (bs lrbs)) \<sharp>* (c, bs lrbs, lrbs, exp)) \<and> supp p = bs lrbs \<union> (p \<bullet> (bs lrbs))")
+apply(erule exE)
+apply(simp add: fresh_star_Pair)
+apply(erule conjE)+
+apply(simp add: multi_recs.fv_bn_eqvt)
+(*
+using Abs_rename_set2
+apply -
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="bs lrbs" in meta_spec)
+apply(drule_tac x="lrbs" in meta_spec)
+apply(drule meta_mp)
+apply(simp add: multi_recs.fv_bn_eqvt fresh_star_Pair)
+apply(drule meta_mp)
+apply(simp add: multi_recs.bn_finite)
+apply(erule exE)
+apply(simp add: multi_recs.fv_bn_eqvt)
+*)
+apply(rule a)
+apply(assumption)
+apply(clarify)
+apply(simp (no_asm) only: multi_recs.eq_iff)
+apply(rule trans)
+apply(rule_tac p="p" in supp_perm_eq[symmetric])
+apply(rule fresh_star_supp_conv)
+apply(simp (no_asm_use) add: fresh_star_def)
+apply(simp (no_asm_use) add: Abs_fresh_iff)[1]
+apply(rule ballI)
+apply(auto simp add: fresh_Pair)[1]
+apply(simp (no_asm_use) only: permute_Abs)
+apply(simp (no_asm_use) only: multi_recs.fv_bn_eqvt)
+apply(simp)
+apply(rule at_set_avoiding5)
+apply(simp add: multi_recs.bn_finite)
+apply(simp add: supp_Pair finite_supp)
+apply(rule finite_sets_supp)
+apply(simp add: multi_recs.bn_finite)
+done
+
+
+
 end