# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1291007402 0
# Node ID 9781db0e21968ccf518b5e92fd4fea41b562d590
# Parent  8f542068103900f5caf4f3425feab11a20513260
completed proofs in Foo2

diff -r 8f5420681039 -r 9781db0e2196 Nominal/Ex/Foo2.thy
--- a/Nominal/Ex/Foo2.thy	Sun Nov 28 16:37:34 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Mon Nov 29 05:10:02 2010 +0000
@@ -26,7 +26,6 @@
 
 thm foo.perm_bn_simps
 
-
 thm foo.distinct
 thm foo.induct
 thm foo.inducts
@@ -246,7 +245,9 @@
 apply(rule conjI)
 apply(assumption)
 apply(simp add: foo.eq_iff)
-defer
+apply(rule at_set_avoiding1)
+apply(simp)
+apply(simp add: finite_supp)
 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)")
 apply(erule exE)
 apply(rule assms(4))
@@ -285,7 +286,9 @@
 apply(rule conjI)
 apply(assumption)
 apply(rule uu1)
-defer
+apply(rule at_set_avoiding1)
+apply(simp)
+apply(simp add: finite_supp)
 apply(subgoal_tac "\<exists>p. (p \<bullet> ({atom name1} \<union> {atom name2})) \<sharp>* (c, atom name1, atom name2, trm1, trm2)")
 apply(erule exE)
 apply(rule assms(5))
@@ -317,7 +320,10 @@
 apply(assumption)
 apply(simp add: fresh_star_prod)
 apply(simp add: fresh_star_def)
-sorry
+apply(rule at_set_avoiding1)
+apply(simp)
+apply(simp add: finite_supp)
+done
 
 
 
diff -r 8f5420681039 -r 9781db0e2196 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Sun Nov 28 16:37:34 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Mon Nov 29 05:10:02 2010 +0000
@@ -1589,6 +1589,15 @@
   using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"]
   unfolding fresh_star_def fresh_def by blast
 
+lemma at_set_avoiding1:
+  assumes "finite xs"
+  and     "finite (supp c)"
+  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c"
+using assms
+apply(erule_tac c="c" in at_set_avoiding)
+apply(auto)
+done
+
 lemma at_set_avoiding2:
   assumes "finite xs"
   and     "finite (supp c)" "finite (supp x)"