--- a/Nominal/Ex/Foo1.thy	Thu Dec 23 00:22:41 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Thu Dec 23 00:46:06 2010 +0000
@@ -44,6 +44,7 @@
 thm foo.induct
 thm foo.inducts
 thm foo.exhaust
+thm foo.strong_exhaust
 thm foo.fv_defs
 thm foo.bn_defs
 thm foo.perm_simps
@@ -56,62 +57,6 @@
 thm foo.fresh
 thm foo.bn_finite
 
-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>(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"
-oops
-
-
-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"
-oops
-
-lemma strong_exhaust1:
-  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"
-oops 
-
-lemma strong_exhaust2:
-  assumes "\<And>x y t. as = As x y t \<Longrightarrow> P" 
-  shows "P"
-apply(rule_tac y="as" in foo.exhaust(2))
-apply(rule assms(1))
-apply(assumption)
-done
-
-lemma strong_exhaust3:
-  assumes "as' = BNil \<Longrightarrow> P"
-  and "\<And>a as. as' = BAs a as \<Longrightarrow> P" 
-  shows "P"
-apply(rule_tac y="as'" in foo.exhaust(3))
-apply(rule assms(1))
-apply(assumption)
-apply(rule assms(2))
-apply(assumption)
-done
-
 lemma 
   fixes t::trm
   and   as::assg
@@ -128,20 +73,17 @@
   and     a9: "\<And>c. P3 c (BNil)"
   and     a10: "\<And>c a as. \<And>d. P3 d as \<Longrightarrow> P3 c (BAs a as)"
   shows "P1 c t" "P2 c as" "P3 c as'"
-oops
-(*
 using assms
 apply(induction_schema)
-apply(rule_tac y="t" and c="c" in strong_exhaust1)
+apply(rule_tac y="t" and c="c" in foo.strong_exhaust(1))
 apply(simp_all)[7]
-apply(rule_tac as="as" in strong_exhaust2)
-apply(simp)
-apply(rule_tac as'="as'" in strong_exhaust3)
+apply(rule_tac ya="as"in foo.strong_exhaust(2))
+apply(simp_all)[1]
+apply(rule_tac yb="as'" in foo.strong_exhaust(3))
 apply(simp_all)[2]
-apply(relation "measure (sum_case (size o snd) (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z))))")
+apply(relation "measure (sum_case (size o snd) (sum_case (size o snd) (size o snd)))")
 apply(simp_all add: foo.size)
 done
-*)
 
 end