diff -r 78623a0f294b -r 8f5420681039 Nominal/Ex/Foo1.thy
--- a/Nominal/Ex/Foo1.thy	Sat Nov 27 23:00:16 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Sun Nov 28 16:37:34 2010 +0000
@@ -154,11 +154,11 @@
   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"
+  and     "\<exists>name trm.  {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P" 
+  and     "\<exists>(c::'a::fs) assn trm. set (bn1 assn) \<sharp>* c \<and> y = Let1 assn trm \<Longrightarrow> P"
+  and     "\<exists>(c::'a::fs) assn trm. set (bn2 assn) \<sharp>* c \<and> y = Let2 assn trm \<Longrightarrow> P"
+  and     "\<exists>(c::'a::fs) assn trm. set (bn3 assn) \<sharp>* c \<and> y = Let3 assn trm \<Longrightarrow> P"
+  and     "\<exists>(c::'a::fs) 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))
@@ -168,6 +168,115 @@
 apply(rule exI)+
 apply(assumption)
 apply(rule assms(3))
+apply(subgoal_tac "\<exists>p::perm. (p \<bullet> {atom name}) \<sharp>* (c, name, trm)")
+apply(erule exE)
+apply(perm_simp)
+apply(rule_tac exI)+
+apply(rule conjI)
+apply(simp add: fresh_star_prod)
+apply(erule conjE)+
+apply(assumption)
+apply(simp)
+apply(simp add: foo.eq_iff)
+(* HERE *)
+defer
+defer
+apply(rule assms(4))
+apply(subgoal_tac "\<exists>p::perm. (p \<bullet> (set (bn1 assg))) \<sharp>* (c, assg, trm)")
+apply(erule exE)
+apply(perm_simp add: tt1)
+apply(simp only: fresh_star_prod)
+apply(erule conjE)+
+apply(rule_tac exI)+
+apply(rule conjI)
+apply(assumption)
+apply(simp add: foo.eq_iff)
+apply(rule conjI)
+apply(simp only: tt1[symmetric])
+defer
+apply(rule uu1)
+defer
+apply(rule assms(5))
+apply(subgoal_tac "\<exists>p::perm. (p \<bullet> (set (bn2 assg))) \<sharp>* (c, assg, trm)")
+apply(erule exE)
+apply(perm_simp add: tt2)
+apply(simp only: fresh_star_prod)
+apply(erule conjE)+
+apply(rule_tac exI)+
+apply(rule conjI)
+apply(assumption)
+apply(simp add: foo.eq_iff)
+apply(rule conjI)
+apply(simp only: tt2[symmetric])
+defer
+apply(rule uu2)
+defer
+apply(rule refl)
+apply(subst (asm) fresh_star_supp_conv)
+apply(simp)
+
+
+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>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P"
+  and     "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P"
+  and     "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P"
+  and     "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+apply(rule strong_exhaust1[where y="y"])
+apply(erule exE)+
+apply(rule assms(1))
+apply(assumption)
+apply(erule exE)+
+apply(rule assms(2))
+apply(assumption)
+apply(erule exE | erule conjE)?
+apply(rule assms(3))
+apply(drule_tac x="c" in spec)
+apply(erule exE | erule conjE)+
+apply(assumption)+
+apply(drule_tac x="c" in spec)
+apply(erule exE | erule conjE)+
+apply(assumption)+
+apply(erule exE | erule conjE)+
+apply(rule assms(4))
+apply(assumption)+
+apply(erule exE | erule conjE)+
+apply(rule assms(5))
+apply(assumption)+
+apply(erule exE | erule conjE)+
+apply(rule assms(6))
+apply(assumption)+
+apply(erule exE | erule conjE)+
+apply(rule assms(7))
+apply(assumption)+
+done
+
+
+
+
+
+
+
+
+
+
+
+
+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(rule_tac p="p" in permute_boolE)
+apply(perm_simp)
+apply(simp)
 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q")
 apply(erule exE)
 apply(erule conjE)