diff -r 3696659358c8 -r 6c4372a1f220 Nominal/Ex/Foo2.thy
--- a/Nominal/Ex/Foo2.thy	Wed Nov 24 02:36:21 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Thu Nov 25 01:18:24 2010 +0000
@@ -34,7 +34,7 @@
 thm foo.fv_defs
 thm foo.bn_defs
 thm foo.perm_simps
-thm foo.eq_iff
+thm foo.eq_iff(5)
 thm foo.fv_bn_eqvt
 thm foo.size_eqvt
 thm foo.supports
@@ -75,6 +75,43 @@
 apply(simp add: uu1)
 done
 
+lemma Let2_rename:
+  assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p" and "(supp ([[atom y]]lst. t2)) \<sharp>* p"
+  shows "Let2 x y t1 t2 = Let2 (p \<bullet> x) (p \<bullet> y) (p \<bullet> t1) (p \<bullet> t2)"
+  using assms
+  apply -
+  apply(drule supp_perm_eq[symmetric])
+  apply(drule supp_perm_eq[symmetric])
+  apply(simp only: foo.eq_iff)
+  apply(simp only: eqvts)
+  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 Let2_rename3:
+  assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p"
+  and "(supp ([[atom y]]lst. t2)) \<sharp>* p"
+  and "(atom x) \<sharp> p"
+  shows "Let2 x y t1 t2 = Let2 x (p \<bullet> y) (p \<bullet> t1) (p \<bullet> t2)"
+  using assms
+  apply -
+  apply(drule supp_perm_eq[symmetric])
+  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" 
@@ -82,7 +119,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))
@@ -130,27 +167,109 @@
 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(perm_simp)
+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
+
+lemma strong_exhaust2:
+  fixes c::"'a::fs"
+  assumes "\<And>name. y = Var name \<Longrightarrow> P" 
+  and     "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
+  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"
+  shows "P"
+  apply (rule strong_exhaust1)
+  apply (erule assms)
+  apply (erule assms)
+  apply (erule assms) apply assumption
+  apply (erule assms) apply assumption
+apply(case_tac "x1 = x2")
+apply(subgoal_tac 
+  "\<exists>q. (q \<bullet> {atom x1, atom x2}) \<sharp>* c \<and> (supp (([[atom x1, atom x2]]lst. trm1), ([[atom x2]]lst. trm2))) \<sharp>* q")
+apply(erule exE)+
+apply(erule conjE)+
+apply(perm_simp)
+apply(rule assms(5))
+apply assumption
+apply simp
+apply (rule Let2_rename)
+apply (simp only: supp_Pair)
+apply (simp only: fresh_star_Un_elim)
+apply (simp only: supp_Pair)
+apply (simp only: fresh_star_Un_elim)
+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 x2}) \<sharp>* c \<and> supp (([[atom x2]]lst. trm2), ([[atom x1, atom x2]]lst. trm1), (atom x1)) \<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(rotate_tac 2)
 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 Let2_rename3)
+apply (simp add: supp_Pair fresh_star_union)
+apply (simp add: supp_Pair fresh_star_union)
+apply (simp add: supp_Pair fresh_star_union)
+apply clarify
+apply (simp add: fresh_star_def supp_atom)
+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)
+done
 
 end