--- a/Nominal/Ex/Multi_Recs.thy	Sun Dec 19 07:50:37 2010 +0000
+++ b/Nominal/Ex/Multi_Recs.thy	Tue Dec 21 10:28:08 2010 +0000
@@ -50,30 +50,6 @@
 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)"
@@ -88,47 +64,36 @@
   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(subgoal_tac "\<exists>p. ((p \<bullet> (bs lrbs)) \<sharp>* (c, bs lrbs, lrbs, exp))")
 apply(erule exE)
 apply(simp add: fresh_star_Pair)
 apply(erule conjE)+
 apply(simp add: multi_recs.fv_bn_eqvt)
-(*
-using Abs_rename_set2
+using Abs_rename_set'
 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_tac x="(lrbs, exp)" 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(erule conjE)
+apply(rotate_tac 6)
+apply(drule sym)
 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(rule at_set_avoiding1)
 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