--- a/Nominal/Ex/Foo1.thy	Fri Nov 26 22:43:26 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Sat Nov 27 22:55:29 2010 +0000
@@ -148,9 +148,58 @@
 using assms
 apply(simp only: foo.eq_iff uu1 tt1[symmetric] permute_Abs[symmetric])
 apply(simp del: permute_Abs)
-apply(rule at_set_avoiding3)
-apply(simp_all only: finite_supp Abs_fresh_star finite_set)
-done
+sorry
+
+lemma strong_exhaust1:
+  fixes c::"'a::fs"
+  assumes "\<exists>name. y = Var name \<Longrightarrow> P" 
+  and     "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
+  and     "\<exists>name trm. {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P" 
+  and     "\<exists>assn trm. set (bn1 assn) \<sharp>* c \<and> y = Let1 assn trm \<Longrightarrow> P"
+  and     "\<exists>assn trm. set (bn2 assn) \<sharp>* c \<and> y = Let2 assn trm \<Longrightarrow> P"
+  and     "\<exists>assn trm. set (bn3 assn) \<sharp>* c \<and> y = Let3 assn trm \<Longrightarrow> P"
+  and     "\<exists>assn' trm. (bn4 assn') \<sharp>* c \<and> y = Let4 assn' trm \<Longrightarrow> P"
+  shows "P"
+apply(rule_tac y="y" in foo.exhaust(1))
+apply(rule assms(1))
+apply(rule exI)
+apply(assumption)
+apply(rule assms(2))
+apply(rule exI)+
+apply(assumption)
+apply(rule assms(3))
+apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q")
+apply(erule exE)
+apply(erule conjE)
+apply(rule assms(3))
+apply(perm_simp)
+apply(assumption)
+apply(simp)
+apply(drule supp_perm_eq[symmetric])
+apply(perm_simp)
+apply(simp)
+apply(rule at_set_avoiding2)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: foo.fresh fresh_star_def)
+apply(drule Let1_rename_a)
+apply(erule exE)
+apply(erule conjE)
+apply(rule assms(4))
+apply(simp only: set_eqvt tt1)
+apply(assumption)
+(*
+apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q")
+apply(erule exE)
+apply(erule conjE)
+*)
+thm assms(5)
+apply(rule assms(5))
+prefer 2
+apply(clarify)
+unfolding foo.eq_iff
+apply
 
 lemma strong_exhaust1:
   fixes c::"'a::fs"
@@ -188,10 +237,24 @@
 apply(rule assms(4))
 apply(simp only: set_eqvt tt1)
 apply(assumption)
+(*
 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q")
 apply(erule exE)
 apply(erule conjE)
+*)
+thm assms(5)
 apply(rule assms(5))
+prefer 2
+apply(clarify)
+unfolding foo.eq_iff
+apply(rule conjI)
+prefer 2
+apply(rule uu2)
+apply(simp only: tt2[symmetric])
+prefer 2
+apply(simp only: tt2[symmetric])
+
+apply(simp_all only:)[2]
 apply(simp add: set_eqvt)
 apply(simp add: tt2)
 apply(simp add: foo.eq_iff)