--- a/Nominal/Ex/Foo2.thy	Mon Nov 22 16:16:25 2010 +0900
+++ b/Nominal/Ex/Foo2.thy	Wed Nov 24 16:59:26 2010 +0900
@@ -87,6 +87,17 @@
   apply simp
   done
 
+lemma Let2_rename2:
+  assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p" and "(atom y) \<sharp> p"
+  shows "Let2 x y t1 t2 = Let2 (p \<bullet> x) y (p \<bullet> t1) t2"
+  using assms
+  apply -
+  apply(drule supp_perm_eq[symmetric])
+  apply(simp only: foo.eq_iff)
+  apply(simp only: eqvts)
+  apply simp
+  by (metis assms(2) atom_eqvt fresh_perm)
+
 lemma strong_exhaust1:
   fixes c::"'a::fs"
   assumes "\<And>name. y = Var name \<Longrightarrow> P" 
@@ -94,7 +105,7 @@
   and     "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
   and     "\<And>assn1 trm1 assn2 trm2. 
     \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 trm2\<rbrakk> \<Longrightarrow> P"
-  and     "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P"
+  and     "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P"
   shows "P"
 apply(rule_tac y="y" in foo.exhaust(1))
 apply(rule assms(1))
@@ -142,26 +153,47 @@
 apply(simp add: finite_supp)
 apply(simp add: finite_supp)
 apply(simp add: Abs_fresh_star)
-thm foo.eq_iff
+apply(case_tac "name1 = name2")
 apply(subgoal_tac 
-  "\<exists>q. (q \<bullet> {atom name1}) \<sharp>* c \<and> supp ([[atom name1]]lst. trm1) \<sharp>* q")
-apply(subgoal_tac 
-  "\<exists>q. (q \<bullet> {atom name2}) \<sharp>* c \<and> supp ([[atom name2]]lst. trm2) \<sharp>* q")
+  "\<exists>q. (q \<bullet> {atom name1, atom name2}) \<sharp>* c \<and> (supp (([[atom name1, atom name2]]lst. trm1), ([[atom name2]]lst. trm2))) \<sharp>* q")
 apply(erule exE)+
 apply(erule conjE)+
-apply(rule assms(5))
 apply(perm_simp)
-apply(simp (no_asm) add: fresh_star_insert)
-apply(rule conjI)
-apply(simp add: fresh_star_def)
-apply(rotate_tac 3)
-apply(simp add: fresh_star_def)
-apply(simp)
-apply(simp add: foo.eq_iff)
-apply(drule supp_perm_eq[symmetric])+
-apply(simp add: atom_eqvt)
-apply(rule conjI)
-oops
+apply(rule assms(5))
+
+apply (simp add: fresh_star_def eqvts)
+apply (simp only: supp_Pair)
+apply (simp only: fresh_star_Un_elim)
+apply (subst Let2_rename)
+apply assumption
+apply assumption
+apply (rule refl)
+apply(rule at_set_avoiding2)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply clarify
+apply (simp add: fresh_star_def)
+apply (simp add: fresh_def supp_Pair supp_Abs)
+apply(subgoal_tac
+  "\<exists>q. (q \<bullet> {atom name1}) \<sharp>* c \<and> (supp ((([[atom name1, atom name2]]lst. trm1)), (atom name2))) \<sharp>* q")
+prefer 2
+apply(rule at_set_avoiding2)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply (simp add: fresh_star_def)
+apply (simp add: fresh_def supp_Pair supp_Abs supp_atom)
+apply(erule exE)+
+apply(erule conjE)+
+apply(perm_simp)
+apply(rule assms(5))
+apply assumption
+apply clarify
+apply (rule_tac x="name1" and y="name2" and ?t1.0="trm1" and ?t2.0="trm2" in Let2_rename2)
+apply (simp_all add: fresh_star_Un_elim supp_Pair supp_Abs)
+apply (simp add: fresh_star_def supp_atom)
+done
 
 
 end