diff -r 3b72f559e942 -r afdba6b3e383 src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/Lambda.thy	Wed Nov 23 22:26:13 2005 +0100
@@ -86,21 +86,15 @@
 
 lemma rtrancl_beta_Abs [intro!]:
     "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
-  apply (erule rtrancl_induct)
-   apply (blast intro: rtrancl_into_rtrancl)+
-  done
+  by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
 
 lemma rtrancl_beta_AppL:
     "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t"
-  apply (erule rtrancl_induct)
-   apply (blast intro: rtrancl_into_rtrancl)+
-  done
+  by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
 
 lemma rtrancl_beta_AppR:
     "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'"
-  apply (erule rtrancl_induct)
-   apply (blast intro: rtrancl_into_rtrancl)+
-  done
+  by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
 
 lemma rtrancl_beta_App [intro]:
     "[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
@@ -112,72 +106,51 @@
 subsection {* Substitution-lemmas *}
 
 lemma subst_eq [simp]: "(Var k)[u/k] = u"
-  apply (simp add: subst_Var)
-  done
+  by (simp add: subst_Var)
 
 lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)"
-  apply (simp add: subst_Var)
-  done
+  by (simp add: subst_Var)
 
 lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j"
-  apply (simp add: subst_Var)
-  done
+  by (simp add: subst_Var)
 
-lemma lift_lift [rule_format]:
-    "\<forall>i k. i < k + 1 --> lift (lift t i) (Suc k) = lift (lift t k) i"
-  apply (induct_tac t)
-    apply auto
-  done
+lemma lift_lift:
+    "i < k + 1 \<Longrightarrow> lift (lift t i) (Suc k) = lift (lift t k) i"
+  by (induct t fixing: i k) auto
 
 lemma lift_subst [simp]:
-    "\<forall>i j s. j < i + 1 --> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
-  apply (induct_tac t)
-    apply (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
-  done
+    "j < i + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
+  by (induct t fixing: i j s)
+    (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
 
 lemma lift_subst_lt:
-    "\<forall>i j s. i < j + 1 --> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
-  apply (induct_tac t)
-    apply (simp_all add: subst_Var lift_lift)
-  done
+    "i < j + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
+  by (induct t fixing: i j s) (simp_all add: subst_Var lift_lift)
 
 lemma subst_lift [simp]:
-    "\<forall>k s. (lift t k)[s/k] = t"
-  apply (induct_tac t)
-    apply simp_all
-  done
+    "(lift t k)[s/k] = t"
+  by (induct t fixing: k s) simp_all
 
-lemma subst_subst [rule_format]:
-    "\<forall>i j u v. i < j + 1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
-  apply (induct_tac t)
-    apply (simp_all
-      add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
+lemma subst_subst:
+    "i < j + 1 \<Longrightarrow> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
+  by (induct t fixing: i j u v)
+    (simp_all add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
       split: nat.split)
-  done
 
 
 subsection {* Equivalence proof for optimized substitution *}
 
-lemma liftn_0 [simp]: "\<forall>k. liftn 0 t k = t"
-  apply (induct_tac t)
-    apply (simp_all add: subst_Var)
-  done
+lemma liftn_0 [simp]: "liftn 0 t k = t"
+  by (induct t fixing: k) (simp_all add: subst_Var)
 
-lemma liftn_lift [simp]:
-    "\<forall>k. liftn (Suc n) t k = lift (liftn n t k) k"
-  apply (induct_tac t)
-    apply (simp_all add: subst_Var)
-  done
+lemma liftn_lift [simp]: "liftn (Suc n) t k = lift (liftn n t k) k"
+  by (induct t fixing: k) (simp_all add: subst_Var)
 
-lemma substn_subst_n [simp]:
-    "\<forall>n. substn t s n = t[liftn n s 0 / n]"
-  apply (induct_tac t)
-    apply (simp_all add: subst_Var)
-  done
+lemma substn_subst_n [simp]: "substn t s n = t[liftn n s 0 / n]"
+  by (induct t fixing: n) (simp_all add: subst_Var)
 
 theorem substn_subst_0: "substn t s 0 = t[s/0]"
-  apply simp
-  done
+  by simp
 
 
 subsection {* Preservation theorems *}
@@ -187,13 +160,11 @@
 
 theorem subst_preserves_beta [simp]:
     "r \<rightarrow>\<^sub>\<beta> s ==> (\<And>t i. r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i])"
-  apply (induct set: beta)
-     apply (simp_all add: subst_subst [symmetric])
-  done
+  by (induct set: beta) (simp_all add: subst_subst [symmetric])
 
 theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
-  apply (erule rtrancl.induct)
-  apply (rule rtrancl_refl)
+  apply (induct set: rtrancl)
+   apply (rule rtrancl_refl)
   apply (erule rtrancl_into_rtrancl)
   apply (erule subst_preserves_beta)
   done
@@ -203,23 +174,22 @@
   by (induct set: beta) auto
 
 theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
-  apply (erule rtrancl.induct)
-  apply (rule rtrancl_refl)
+  apply (induct set: rtrancl)
+   apply (rule rtrancl_refl)
   apply (erule rtrancl_into_rtrancl)
   apply (erule lift_preserves_beta)
   done
 
-theorem subst_preserves_beta2 [simp]:
-    "\<And>r s i. r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
-  apply (induct t)
+theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
+  apply (induct t fixing: r s i)
     apply (simp add: subst_Var r_into_rtrancl)
    apply (simp add: rtrancl_beta_App)
   apply (simp add: rtrancl_beta_Abs)
   done
 
 theorem subst_preserves_beta2': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
-  apply (erule rtrancl.induct)
-  apply (rule rtrancl_refl)
+  apply (induct set: rtrancl)
+   apply (rule rtrancl_refl)
   apply (erule rtrancl_trans)
   apply (erule subst_preserves_beta2)
   done