--- a/Nominal/Ex/Foo2.thy	Mon Nov 29 05:17:41 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Mon Nov 29 08:01:09 2010 +0000
@@ -100,51 +100,47 @@
 apply(simp add: mem_permute_iff)
 done
 
-lemma yy1:
-  assumes "(p \<bullet> bs) \<sharp>* bs" "finite bs"
-  shows "p \<bullet> bs \<inter> bs = {}"
-using assms
-apply(auto simp add: fresh_star_def)
-apply(simp add: fresh_def supp_finite_atom_set)
-done
-
-lemma abs_rename_set:
+lemma Abs_rename_set:
   fixes x::"'a::fs"
-  assumes "(p \<bullet> bs) \<sharp>* x" "(p \<bullet> bs) \<sharp>* bs" "finite bs"
+  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
+  and     b: "finite bs"
   shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y"
-using yy assms
-apply -
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="bs" in meta_spec)
-apply(auto simp add: yy1)
-apply(rule_tac x="q \<bullet> x" in exI)
-apply(subgoal_tac "(q \<bullet> ([bs]set. x)) = [bs]set. x")
-apply(simp)
-apply(rule supp_perm_eq)
-apply(rule fresh_star_supp_conv)
-apply(simp add: fresh_star_def)
-apply(simp add: Abs_fresh_iff)
-apply(auto)
-done
+proof -
+  from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair)   
+  with yy obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
+  have "[bs]set. x =  q \<bullet> ([bs]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> bs]set. (q \<bullet> x)" by simp
+  also have "\<dots> = [p \<bullet> bs]set. (q \<bullet> x)" using * by simp
+  finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" .
+  then show "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y" by blast
+qed
 
-lemma abs_rename_res:
+lemma Abs_rename_res:
   fixes x::"'a::fs"
-  assumes "(p \<bullet> bs) \<sharp>* x" "(p \<bullet> bs) \<sharp>* bs" "finite bs"
+  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
+  and     b: "finite bs"
   shows "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y"
-using yy assms
-apply -
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="bs" in meta_spec)
-apply(auto simp add: yy1)
-apply(rule_tac x="q \<bullet> x" in exI)
-apply(subgoal_tac "(q \<bullet> ([bs]res. x)) = [bs]res. x")
-apply(simp)
-apply(rule supp_perm_eq)
-apply(rule fresh_star_supp_conv)
-apply(simp add: fresh_star_def)
-apply(simp add: Abs_fresh_iff)
-apply(auto)
-done
+proof -
+  from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair) 
+  with yy obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
+  have "[bs]res. x =  q \<bullet> ([bs]res. 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> bs]res. (q \<bullet> x)" by simp
+  also have "\<dots> = [p \<bullet> bs]res. (q \<bullet> x)" using * by simp
+  finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" .
+  then show "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" by blast
+qed
 
 lemma zz0:
   assumes "p \<bullet> bs = q \<bullet> bs"
@@ -155,7 +151,7 @@
 
 lemma zz:
   fixes bs::"atom list"
-  assumes "set bs \<inter> (p \<bullet> (set bs)) = {}"
+  assumes "(p \<bullet> (set bs)) \<inter> (set bs) = {}"
   shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))"
 using assms
 apply(induct bs)
@@ -195,39 +191,26 @@
 apply(auto simp add: fresh_def supp_of_atom_list)[1]
 done
 
-lemma zz1:
-  assumes "(p \<bullet> (set bs)) \<sharp>* bs" 
-  shows "(set bs) \<inter> (p \<bullet> (set bs)) = {}"
-using assms
-apply(auto simp add: fresh_star_def)
-apply(simp add: fresh_def supp_of_atom_list)
-done
-
-lemma abs_rename_list:
+lemma Abs_rename_list:
   fixes x::"'a::fs"
-  assumes "(p \<bullet> (set bs)) \<sharp>* x" "(p \<bullet> (set bs)) \<sharp>* bs" 
+  assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" 
   shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y"
-using zz assms
-apply -
-apply(drule_tac x="bs" in meta_spec)
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac zz1)
-apply(auto)
-apply(rule_tac x="q \<bullet> x" in exI)
-apply(subgoal_tac "(q \<bullet> ([bs]lst. x)) = [bs]lst. x")
-apply(simp)
-apply(rule supp_perm_eq)
-apply(rule fresh_star_supp_conv)
-apply(simp add: fresh_star_def)
-apply(simp add: Abs_fresh_iff)
-apply(auto)
-done
-
-lemma fresh_star_list:
-  shows "as \<sharp>* (xs @ ys) \<longleftrightarrow> as \<sharp>* xs \<and> as \<sharp>* ys"
-  and   "as \<sharp>* (x # xs) \<longleftrightarrow> as \<sharp>* x \<and> as \<sharp>* xs"
-  and   "as \<sharp>* []"
-by (auto simp add: fresh_star_def fresh_Nil fresh_Cons fresh_append)
+proof -
+  from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter 
+    by (simp add: fresh_star_Pair fresh_star_set)
+  with zz obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis 
+  have "[bs]lst. x =  q \<bullet> ([bs]lst. 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> bs]lst. (q \<bullet> x)" by simp
+  also have "\<dots> = [p \<bullet> bs]lst. (q \<bullet> x)" using * by simp
+  finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" .
+  then show "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" by blast
+qed
 
 
 lemma test6:
@@ -248,15 +231,13 @@
 apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, [atom name], trm)")
 apply(erule exE)
 apply(rule assms(3))
-apply(insert abs_rename_list)[1]
+apply(insert Abs_rename_list)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="[atom name]" in meta_spec)
 apply(drule_tac x="trm" in meta_spec)
-apply(simp only: fresh_star_prod set.simps)
+apply(simp only: fresh_star_Pair set.simps)
 apply(drule meta_mp)
-apply(rule TrueI)
-apply(drule meta_mp)
-apply(rule TrueI)
+apply(simp)
 apply(erule exE)
 apply(rule exI)+
 apply(perm_simp)
@@ -272,27 +253,23 @@
 apply(rule assms(4))
 apply(simp only:)
 apply(simp only: foo.eq_iff)
-apply(insert abs_rename_list)[1]
+apply(insert Abs_rename_list)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="bn assg1" in meta_spec)
 apply(drule_tac x="trm1" in meta_spec)
-apply(insert abs_rename_list)[1]
+apply(insert Abs_rename_list)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="bn assg2" in meta_spec)
 apply(drule_tac x="trm2" in meta_spec)
 apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union)
-apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union)
+apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp)
 apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union)
-apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union)
+apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp)
 apply(erule exE)+
 apply(rule exI)+
 apply(perm_simp add: tt1)
 apply(rule conjI)
-apply(simp add: fresh_star_prod fresh_star_union)
+apply(simp add: fresh_star_Pair fresh_star_Un)
 apply(erule conjE)+
 apply(rule conjI)
 apply(assumption)
@@ -313,22 +290,26 @@
 apply(rule assms(5))
 apply(simp only:)
 apply(simp only: foo.eq_iff)
-apply(insert abs_rename_list)[1]
+apply(insert Abs_rename_list)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="[atom name1] @ [atom name2]" in meta_spec)
 apply(drule_tac x="trm1" in meta_spec)
-apply(insert abs_rename_list)[1]
+apply(insert Abs_rename_list)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="[atom name2]" in meta_spec)
 apply(drule_tac x="trm2" in meta_spec)
 apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_prod set.simps set_append fresh_star_union, simp)
-apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union)
+apply(simp only: union_eqvt fresh_star_Pair fresh_star_list fresh_star_Un, simp)
+apply(auto)[1]
+apply(perm_simp)
+apply(auto simp add: fresh_star_def)[1]
+apply(perm_simp)
+apply(auto simp add: fresh_star_def)[1]
+apply(perm_simp)
+apply(auto simp add: fresh_star_def)[1]
 apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union set_append fresh_star_list, simp)
-apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union set_append fresh_star_list, simp)
+apply(perm_simp)
+apply(auto simp add: fresh_star_def fresh_Pair fresh_Nil fresh_Cons)[1]
 apply(erule exE)+
 apply(rule exI)+
 apply(perm_simp add: tt1)
@@ -337,15 +318,13 @@
 apply(rule conjI)
 apply(assumption)
 apply(assumption)
-apply(simp add: fresh_star_prod)
+apply(simp add: fresh_star_Pair)
 apply(simp add: fresh_star_def)
 apply(rule at_set_avoiding1)
 apply(simp)
 apply(simp add: finite_supp)
 done
 
-
-
 lemma test5:
   fixes c::"'a::fs"
   assumes "\<And>name. y = Var name \<Longrightarrow> P"