diff -r 3b6a70e73006 -r cc5d23547341 Nominal/Ex/Foo1.thy
--- a/Nominal/Ex/Foo1.thy	Wed Sep 29 09:47:26 2010 -0400
+++ b/Nominal/Ex/Foo1.thy	Wed Sep 29 16:49:13 2010 -0400
@@ -157,26 +157,26 @@
 
 lemma strong_exhaust1:
   fixes c::"'a::fs"
-  assumes "\<And>name ca. \<lbrakk>c = ca; y = Var name\<rbrakk> \<Longrightarrow> P" 
-  and     "\<And>trm1 trm2 ca. \<lbrakk>c = ca; y = App trm1 trm2\<rbrakk> \<Longrightarrow> P"
-  and     "\<And>name trm ca. \<lbrakk>{atom name} \<sharp>* ca; c = ca; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
-  and     "\<And>assn trm ca. \<lbrakk>set (bn1 assn) \<sharp>* ca; c = ca; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P"
-  and     "\<And>assn trm ca. \<lbrakk>set (bn2 assn) \<sharp>* ca; c = ca; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P"
-  and     "\<And>assn trm ca. \<lbrakk>set (bn3 assn) \<sharp>* ca; c = ca; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P"
+  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"
   shows "P"
 apply(rule_tac y="y" in foo.exhaust(1))
 apply(rule assms(1))
-apply(auto)[2]
+apply(assumption)
 apply(rule assms(2))
-apply(auto)[2]
+apply(assumption)
 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(rule refl)
 apply(drule supp_perm_eq[symmetric])
+apply(perm_simp)
 apply(simp)
 apply(rule at_set_avoiding2)
 apply(simp add: finite_supp)
@@ -187,13 +187,10 @@
 apply(erule exE)
 apply(erule conjE)
 apply(rule assms(4))
-apply(simp add: set_eqvt)
-apply(simp add: tt1)
-apply(rule refl)
-apply(simp)
+apply(perm_simp add: tt1)
+apply(assumption)
+apply(drule supp_perm_eq[symmetric])
 apply(simp add: foo.eq_iff)
-apply(drule supp_perm_eq[symmetric])
-apply(simp)
 apply(simp add: tt1 uu1)
 apply(rule at_set_avoiding2)
 apply(simp add: finite_supp)
@@ -206,8 +203,6 @@
 apply(rule assms(5))
 apply(simp add: set_eqvt)
 apply(simp add: tt2)
-apply(rule refl)
-apply(simp)
 apply(simp add: foo.eq_iff)
 apply(drule supp_perm_eq[symmetric])
 apply(simp)
@@ -223,8 +218,6 @@
 apply(rule assms(6))
 apply(simp add: set_eqvt)
 apply(simp add: tt3)
-apply(rule refl)
-apply(simp)
 apply(simp add: foo.eq_iff)
 apply(drule supp_perm_eq[symmetric])
 apply(simp)
@@ -236,14 +229,12 @@
 apply(simp add: Abs_fresh_star)
 done
 
-thm foo.exhaust
-
 lemma strong_exhaust2:
-  assumes "\<And>x y t ca. \<lbrakk>c = ca; as = As x y t\<rbrakk> \<Longrightarrow> P" 
+  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(auto)[2]
+apply(assumption)
 done
 
 
@@ -261,17 +252,11 @@
   shows "P1 c t" "P2 c as"
 using assms
 apply(induction_schema)
-apply(rule_tac y="t" in strong_exhaust1)
-apply(blast)
-apply(blast)
-apply(blast)
-apply(blast)
-apply(blast)
-apply(blast)
+apply(rule_tac y="t" and c="c" in strong_exhaust1)
+apply(simp_all)[6]
 apply(rule_tac as="as" in strong_exhaust2)
-apply(blast)
+apply(simp)
 apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))")
-apply(auto)[1]
 apply(simp_all add: foo.size)
 done