# HG changeset patch
# User wenzelm
# Date 1132781173 -3600
# Node ID afdba6b3e3833d9d6d7cee3034b86cf7edcfdb71
# Parent  3b72f559e9423e69811dd06ba5e501617e6fce7c
tuned induction proofs;

diff -r 3b72f559e942 -r afdba6b3e383 src/HOL/Isar_examples/Fibonacci.thy
--- a/src/HOL/Isar_examples/Fibonacci.thy	Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Isar_examples/Fibonacci.thy	Wed Nov 23 22:26:13 2005 +0100
@@ -124,7 +124,7 @@
 qed
 
 lemma gcd_fib_mod:
-  assumes m: "0 < m"
+  assumes "0 < m"
   shows "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
 proof (induct n rule: nat_less_induct)
   case (1 n) note hyp = this
@@ -137,7 +137,7 @@
       case True then show ?thesis by simp
     next
       case False then have "m <= n" by simp
-      from m and False have "n - m < n" by simp
+      from `0 < m` and False have "n - m < n" by simp
       with hyp have "gcd (fib m, fib ((n - m) mod m))
         = gcd (fib m, fib (n - m))" by simp
       also have "... = gcd (fib m, fib n)"
diff -r 3b72f559e942 -r afdba6b3e383 src/HOL/Isar_examples/Hoare.thy
--- a/src/HOL/Isar_examples/Hoare.thy	Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy	Wed Nov 23 22:26:13 2005 +0100
@@ -160,14 +160,15 @@
  semantics of \texttt{WHILE}.
 *}
 
-theorem while: "|- (P Int b) c P ==> |- P (While b X c) (P Int -b)"
+theorem while:
+  assumes body: "|- (P Int b) c P"
+  shows "|- P (While b X c) (P Int -b)"
 proof
-  assume body: "|- (P Int b) c P"
   fix s s' assume s: "s : P"
   assume "Sem (While b X c) s s'"
-  then obtain n where iter: "iter n b (Sem c) s s'" by auto
-  have "!!s. iter n b (Sem c) s s' ==> s : P ==> s' : P Int -b"
-  proof (induct n)
+  then obtain n where "iter n b (Sem c) s s'" by auto
+  from this and s show "s' : P Int -b"
+  proof (induct n fixing: s)
     case (0 s)
     thus ?case by auto
   next
@@ -179,7 +180,6 @@
     with body sem have "s'' : P" ..
     with iter show ?case by (rule Suc)
   qed
-  from this iter s show "s' : P Int -b" .
 qed
 
 
@@ -424,8 +424,8 @@
     \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
   by (auto simp: Valid_def)
 
-lemma iter_aux: "
-  \<forall>s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
+lemma iter_aux:
+  "\<forall>s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
        (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)"
   apply(induct n)
    apply clarsimp
diff -r 3b72f559e942 -r afdba6b3e383 src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Nov 23 22:26:13 2005 +0100
@@ -169,24 +169,21 @@
 qed
 
 lemma domino_singleton:
-  assumes "d : domino" and "b < 2"
-  shows "EX i j. evnodd d b = {(i, j)}"
-proof -
-  from `d : domino`
-  show ?thesis (is "?P d")
-  proof induct
-    from `b < 2` have b_cases: "b = 0 | b = 1" by arith
-    fix i j
-    note [simp] = evnodd_empty evnodd_insert mod_Suc
-    from b_cases show "?P {(i, j), (i, j + 1)}" by rule auto
-    from b_cases show "?P {(i, j), (i + 1, j)}" by rule auto
-  qed
+  assumes d: "d : domino" and "b < 2"
+  shows "EX i j. evnodd d b = {(i, j)}"  (is "?P d")
+  using d
+proof induct
+  from `b < 2` have b_cases: "b = 0 | b = 1" by arith
+  fix i j
+  note [simp] = evnodd_empty evnodd_insert mod_Suc
+  from b_cases show "?P {(i, j), (i, j + 1)}" by rule auto
+  from b_cases show "?P {(i, j), (i + 1, j)}" by rule auto
 qed
 
 lemma domino_finite:
-  assumes "d: domino"
+  assumes d: "d: domino"
   shows "finite d"
-  using prems
+  using d
 proof induct
   fix i j :: nat
   show "finite {(i, j), (i, j + 1)}" by (intro Finites.intros)
@@ -197,9 +194,9 @@
 subsection {* Tilings of dominoes *}
 
 lemma tiling_domino_finite:
-  assumes "t : tiling domino"  (is "t : ?T")
+  assumes t: "t : tiling domino"  (is "t : ?T")
   shows "finite t"  (is "?F t")
-  using `t : ?T`
+  using t
 proof induct
   show "?F {}" by (rule Finites.emptyI)
   fix a t assume "?F t"
@@ -208,9 +205,9 @@
 qed
 
 lemma tiling_domino_01:
-  assumes "t : tiling domino"  (is "t : ?T")
+  assumes t: "t : tiling domino"  (is "t : ?T")
   shows "card (evnodd t 0) = card (evnodd t 1)"
-  using `t : ?T`
+  using t
 proof induct
   case empty
   show ?case by (simp add: evnodd_def)
diff -r 3b72f559e942 -r afdba6b3e383 src/HOL/Lambda/Commutation.thy
--- a/src/HOL/Lambda/Commutation.thy	Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/Commutation.thy	Wed Nov 23 22:26:13 2005 +0100
@@ -197,11 +197,11 @@
     \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
   shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
                \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
-using wf
+  using wf
 proof induct
   case (less x b c)
-  have IH: "\<And>y b c. \<lbrakk>(y,x) \<in> R\<inverse>; (y,b) \<in> R\<^sup>*; (y,c) \<in> R\<^sup>*\<rbrakk>
-                     \<Longrightarrow> \<exists>d. (b,d) \<in> R\<^sup>* \<and> (c,d) \<in> R\<^sup>*" by(rule less)
+  note IH = `\<And>y b c. \<lbrakk>(y,x) \<in> R\<inverse>; (y,b) \<in> R\<^sup>*; (y,c) \<in> R\<^sup>*\<rbrakk>
+                     \<Longrightarrow> \<exists>d. (b,d) \<in> R\<^sup>* \<and> (c,d) \<in> R\<^sup>*`
   have xc: "(x, c) \<in> R\<^sup>*" .
   have xb: "(x, b) \<in> R\<^sup>*" .
   thus ?case
@@ -223,11 +223,11 @@
       assume y'c: "(y', c) \<in> R\<^sup>*"
       assume xy': "(x, y') \<in> R"
       with xy obtain u where u: "(y, u) \<in> R\<^sup>*" "(y', u) \<in> R\<^sup>*"
-	by (blast dest:lc)
+        by (blast dest: lc)
       from yb u y'c show ?thesis
-	by(blast del: rtrancl_refl
-		 intro:rtrancl_trans
-                 dest:IH[OF xy[symmetric]] IH[OF xy'[symmetric]])
+        by (blast del: rtrancl_refl
+            intro: rtrancl_trans
+            dest: IH [OF xy [symmetric]] IH [OF xy' [symmetric]])
     qed
   qed
 qed
diff -r 3b72f559e942 -r afdba6b3e383 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/Eta.thy	Wed Nov 23 22:26:13 2005 +0100
@@ -45,24 +45,20 @@
 
 subsection "Properties of eta, subst and free"
 
-lemma subst_not_free [rule_format, simp]:
-    "\<forall>i t u. \<not> free s i --> s[t/i] = s[u/i]"
-  apply (induct_tac s)
-    apply (simp_all add: subst_Var)
-  done
+lemma subst_not_free [simp]: "\<not> free s i \<Longrightarrow> s[t/i] = s[u/i]"
+  by (induct s fixing: i t u) (simp_all add: subst_Var)
 
 lemma free_lift [simp]:
-    "\<forall>i k. free (lift t k) i =
-      (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
-  apply (induct_tac t)
+    "free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
+  apply (induct t fixing: i k)
     apply (auto cong: conj_cong)
   apply arith
   done
 
 lemma free_subst [simp]:
-    "\<forall>i k t. free (s[t/k]) i =
+    "free (s[t/k]) i =
       (free s k \<and> free t i \<or> free s (if i < k then i else i + 1))"
-  apply (induct_tac s)
+  apply (induct s fixing: i k t)
     prefer 2
     apply simp
     apply blast
@@ -71,25 +67,19 @@
   apply (simp add: diff_Suc subst_Var split: nat.split)
   done
 
-lemma free_eta [rule_format]:
-    "s -e> t ==> \<forall>i. free t i = free s i"
-  apply (erule eta.induct)
-     apply (simp_all cong: conj_cong)
-  done
+lemma free_eta: "s -e> t ==> (!!i. free t i = free s i)"
+  by (induct set: eta) (simp_all cong: conj_cong)
 
 lemma not_free_eta:
     "[| s -e> t; \<not> free s i |] ==> \<not> free t i"
-  apply (simp add: free_eta)
-  done
+  by (simp add: free_eta)
 
-lemma eta_subst [rule_format, simp]:
-    "s -e> t ==> \<forall>u i. s[u/i] -e> t[u/i]"
-  apply (erule eta.induct)
-  apply (simp_all add: subst_subst [symmetric])
-  done
+lemma eta_subst [simp]:
+    "s -e> t ==> (!!u i. s[u/i] -e> t[u/i])"
+  by (induct set: eta) (simp_all add: subst_subst [symmetric])
 
-theorem lift_subst_dummy: "\<And>i dummy. \<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s"
-  by (induct s) simp_all
+theorem lift_subst_dummy: "\<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s"
+  by (induct s fixing: i dummy) simp_all
 
 
 subsection "Confluence of eta"
@@ -114,56 +104,40 @@
 subsection "Congruence rules for eta*"
 
 lemma rtrancl_eta_Abs: "s -e>> s' ==> Abs s -e>> Abs s'"
-  apply (erule rtrancl_induct)
-   apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
-  done
+  by (induct set: rtrancl)
+    (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
 
 lemma rtrancl_eta_AppL: "s -e>> s' ==> s \<degree> t -e>> s' \<degree> t"
-  apply (erule rtrancl_induct)
-   apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
-  done
+  by (induct set: rtrancl)
+    (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
 
 lemma rtrancl_eta_AppR: "t -e>> t' ==> s \<degree> t -e>> s \<degree> t'"
-  apply (erule rtrancl_induct)
-   apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
-  done
+  by (induct set: rtrancl) (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
 
 lemma rtrancl_eta_App:
     "[| s -e>> s'; t -e>> t' |] ==> s \<degree> t -e>> s' \<degree> t'"
-  apply (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans)
-  done
+  by (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans)
 
 
 subsection "Commutation of beta and eta"
 
-lemma free_beta [rule_format]:
-    "s -> t ==> \<forall>i. free t i --> free s i"
-  apply (erule beta.induct)
-     apply simp_all
-  done
+lemma free_beta:
+    "s -> t ==> (!!i. free t i \<Longrightarrow> free s i)"
+  by (induct set: beta) auto
 
-lemma beta_subst [rule_format, intro]:
-    "s -> t ==> \<forall>u i. s[u/i] -> t[u/i]"
-  apply (erule beta.induct)
-     apply (simp_all add: subst_subst [symmetric])
-  done
+lemma beta_subst [intro]: "s -> t ==> (!!u i. s[u/i] -> t[u/i])"
+  by (induct set: beta) (simp_all add: subst_subst [symmetric])
 
-lemma subst_Var_Suc [simp]: "\<forall>i. t[Var i/i] = t[Var(i)/i + 1]"
-  apply (induct_tac t)
-  apply (auto elim!: linorder_neqE simp: subst_Var)
-  done
+lemma subst_Var_Suc [simp]: "t[Var i/i] = t[Var(i)/i + 1]"
+  by (induct t fixing: i) (auto elim!: linorder_neqE simp: subst_Var)
 
-lemma eta_lift [rule_format, simp]:
-    "s -e> t ==> \<forall>i. lift s i -e> lift t i"
-  apply (erule eta.induct)
-     apply simp_all
-  done
+lemma eta_lift [simp]: "s -e> t ==> (!!i. lift s i -e> lift t i)"
+  by (induct set: eta) simp_all
 
-lemma rtrancl_eta_subst [rule_format]:
-    "\<forall>s t i. s -e> t --> u[s/i] -e>> u[t/i]"
-  apply (induct_tac u)
+lemma rtrancl_eta_subst: "s -e> t \<Longrightarrow> u[s/i] -e>> u[t/i]"
+  apply (induct u fixing: s t i)
     apply (simp_all add: subst_Var)
-    apply (blast)
+    apply blast
    apply (blast intro: rtrancl_eta_App)
   apply (blast intro!: rtrancl_eta_Abs eta_lift)
   done
@@ -191,11 +165,10 @@
 
 text {* @{term "Abs (lift s 0 \<degree> Var 0) -e> s"} *}
 
-lemma not_free_iff_lifted [rule_format]:
-    "\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)"
-  apply (induct_tac s)
+lemma not_free_iff_lifted:
+    "(\<not> free s i) = (\<exists>t. s = lift t i)"
+  apply (induct s fixing: i)
     apply simp
-    apply clarify
     apply (rule iffI)
      apply (erule linorder_neqE)
       apply (rule_tac x = "Var nat" in exI)
@@ -214,7 +187,6 @@
    apply simp
    apply (erule thin_rl)
    apply (erule thin_rl)
-   apply (rule allI)
    apply (rule iffI)
     apply (elim conjE exE)
     apply (rename_tac u1 u2)
@@ -229,7 +201,6 @@
    apply simp
   apply simp
   apply (erule thin_rl)
-  apply (rule allI)
   apply (rule iffI)
    apply (erule exE)
    apply (rule_tac x = "Abs t" in exI)
@@ -246,8 +217,7 @@
 theorem explicit_is_implicit:
   "(\<forall>s u. (\<not> free s 0) --> R (Abs (s \<degree> Var 0)) (s[u/0])) =
     (\<forall>s. R (Abs (lift s 0 \<degree> Var 0)) s)"
-  apply (auto simp add: not_free_iff_lifted)
-  done
+  by (auto simp add: not_free_iff_lifted)
 
 
 subsection {* Parallel eta-reduction *}
@@ -270,22 +240,23 @@
   app [simp, intro]: "s \<Rightarrow>\<^sub>\<eta> s' \<Longrightarrow> t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> s \<degree> t \<Rightarrow>\<^sub>\<eta> s' \<degree> t'"
   abs [simp, intro]: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> Abs s \<Rightarrow>\<^sub>\<eta> Abs t"
 
-lemma free_par_eta [simp]: assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
-  shows "\<And>i. free t i = free s i" using eta
-  by induct (simp_all cong: conj_cong)
+lemma free_par_eta [simp]:
+  assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
+  shows "free t i = free s i" using eta
+  by (induct fixing: i) (simp_all cong: conj_cong)
 
 lemma par_eta_refl [simp]: "t \<Rightarrow>\<^sub>\<eta> t"
   by (induct t) simp_all
 
 lemma par_eta_lift [simp]:
   assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
-  shows "\<And>i. lift s i \<Rightarrow>\<^sub>\<eta> lift t i" using eta
-  by induct simp_all
+  shows "lift s i \<Rightarrow>\<^sub>\<eta> lift t i" using eta
+  by (induct fixing: i) simp_all
 
 lemma par_eta_subst [simp]:
   assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
-  shows "\<And>u u' i. u \<Rightarrow>\<^sub>\<eta> u' \<Longrightarrow> s[u/i] \<Rightarrow>\<^sub>\<eta> t[u'/i]" using eta
-  by induct (simp_all add: subst_subst [symmetric] subst_Var)
+  shows "u \<Rightarrow>\<^sub>\<eta> u' \<Longrightarrow> s[u/i] \<Rightarrow>\<^sub>\<eta> t[u'/i]" using eta
+  by (induct fixing: u u' i) (simp_all add: subst_subst [symmetric] subst_Var)
 
 theorem eta_subset_par_eta: "eta \<subseteq> par_eta"
   apply (rule subsetI)
@@ -320,16 +291,16 @@
   eta_expand_Suc: "eta_expand (Suc n) t = Abs (lift (eta_expand n t) 0 \<degree> Var 0)"
 
 lemma eta_expand_Suc':
-  "\<And>t. eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 \<degree> Var 0))"
-  by (induct n) simp_all
+  "eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 \<degree> Var 0))"
+  by (induct n fixing: t) simp_all
 
 theorem lift_eta_expand: "lift (eta_expand k t) i = eta_expand k (lift t i)"
   by (induct k) (simp_all add: lift_lift)
 
 theorem eta_expand_beta:
   assumes u: "u => u'"
-  shows "\<And>t t'. t => t' \<Longrightarrow> eta_expand k (Abs t) \<degree> u => t'[u'/0]"
-proof (induct k)
+  shows "t => t' \<Longrightarrow> eta_expand k (Abs t) \<degree> u => t'[u'/0]"
+proof (induct k fixing: t t')
   case 0 with u show ?case by simp
 next
   case (Suc k)
@@ -343,8 +314,8 @@
   shows "eta_expand k t => eta_expand k t'"
   by (induct k) (simp_all add: t)
 
-theorem eta_expand_eta: "\<And>t t'. t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> eta_expand k t \<Rightarrow>\<^sub>\<eta> t'"
-proof (induct k)
+theorem eta_expand_eta: "t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> eta_expand k t \<Rightarrow>\<^sub>\<eta> t'"
+proof (induct k fixing: t t')
   case 0
   show ?case by simp
 next
@@ -358,9 +329,9 @@
 subsection {* Elimination rules for parallel eta reduction *}
 
 theorem par_eta_elim_app: assumes eta: "t \<Rightarrow>\<^sub>\<eta> u"
-  shows "\<And>u1' u2'. u = u1' \<degree> u2' \<Longrightarrow>
+  shows "u = u1' \<degree> u2' \<Longrightarrow>
     \<exists>u1 u2 k. t = eta_expand k (u1 \<degree> u2) \<and> u1 \<Rightarrow>\<^sub>\<eta> u1' \<and> u2 \<Rightarrow>\<^sub>\<eta> u2'" using eta
-proof induct
+proof (induct fixing: u1' u2')
   case (app s s' t t')
   have "s \<degree> t = eta_expand 0 (s \<degree> t)" by simp
   with app show ?case by blast
@@ -388,9 +359,9 @@
 qed
 
 theorem par_eta_elim_abs: assumes eta: "t \<Rightarrow>\<^sub>\<eta> t'"
-  shows "\<And>u'. t' = Abs u' \<Longrightarrow>
+  shows "t' = Abs u' \<Longrightarrow>
     \<exists>u k. t = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u'" using eta
-proof induct
+proof (induct fixing: u')
   case (abs s t)
   have "Abs s = eta_expand 0 (Abs s)" by simp
   with abs show ?case by blast
@@ -420,8 +391,9 @@
 Based on a proof by Masako Takahashi \cite{Takahashi-IandC}.
 *}
 
-theorem par_eta_beta: "\<And>s u. s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' \<Rightarrow>\<^sub>\<eta> u"
-proof (induct t rule: measure_induct [of size, rule_format])
+theorem par_eta_beta: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' \<Rightarrow>\<^sub>\<eta> u"
+proof (induct t fixing: s u
+    rule: measure_induct [of size, rule_format])
   case (1 t)
   from 1(3)
   show ?case
@@ -467,10 +439,10 @@
 qed
 
 theorem eta_postponement': assumes eta: "s -e>> t"
-  shows "\<And>u. t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' -e>> u"
+  shows "t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' -e>> u"
   using eta [simplified rtrancl_subset
     [OF eta_subset_par_eta par_eta_subset_eta, symmetric]]
-proof induct
+proof (induct fixing: u)
   case 1
   thus ?case by blast
 next
diff -r 3b72f559e942 -r afdba6b3e383 src/HOL/Lambda/InductTermi.thy
--- a/src/HOL/Lambda/InductTermi.thy	Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/InductTermi.thy	Wed Nov 23 22:26:13 2005 +0100
@@ -45,7 +45,7 @@
   done
 
 lemma IT_implies_termi: "t : IT ==> t : termi beta"
-  apply (erule IT.induct)
+  apply (induct set: IT)
     apply (drule rev_subsetD)
      apply (rule lists_mono)
      apply (rule Int_lower2)
@@ -63,16 +63,14 @@
 
 subsection {* Every terminating term is in IT *}
 
-declare Var_apps_neq_Abs_apps [THEN not_sym, simp]
+declare Var_apps_neq_Abs_apps [symmetric, simp]
 
 lemma [simp, THEN not_sym, simp]: "Var n \<degree>\<degree> ss \<noteq> Abs r \<degree> s \<degree>\<degree> ts"
-  apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
-  done
+  by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
 
 lemma [simp]:
   "(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')"
-  apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
-  done
+  by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
 
 inductive_cases [elim!]:
   "Var n \<degree>\<degree> ss : IT"
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
diff -r 3b72f559e942 -r afdba6b3e383 src/HOL/Lambda/ListApplication.thy
--- a/src/HOL/Lambda/ListApplication.thy	Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/ListApplication.thy	Wed Nov 23 22:26:13 2005 +0100
@@ -14,19 +14,14 @@
   "t \<degree>\<degree> ts" == "foldl (op \<degree>) t ts"
 
 lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)"
-  apply (induct_tac ts rule: rev_induct)
-   apply auto
-  done
+  by (induct ts rule: rev_induct) auto
 
-lemma Var_eq_apps_conv [iff]:
-    "\<And>s. (Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])"
-  apply (induct ss)
-   apply auto
-  done
+lemma Var_eq_apps_conv [iff]: "(Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])"
+  by (induct ss fixing: s) auto
 
 lemma Var_apps_eq_Var_apps_conv [iff]:
-    "\<And>ss. (Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)"
-  apply (induct rs rule: rev_induct)
+    "(Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)"
+  apply (induct rs fixing: ss rule: rev_induct)
    apply simp
    apply blast
   apply (induct_tac ss rule: rev_induct)
@@ -43,18 +38,14 @@
 
 lemma Abs_eq_apps_conv [iff]:
     "(Abs r = s \<degree>\<degree> ss) = (Abs r = s \<and> ss = [])"
-  apply (induct_tac ss rule: rev_induct)
-   apply auto
-  done
+  by (induct ss rule: rev_induct) auto
 
 lemma apps_eq_Abs_conv [iff]: "(s \<degree>\<degree> ss = Abs r) = (s = Abs r \<and> ss = [])"
-  apply (induct_tac ss rule: rev_induct)
-   apply auto
-  done
+  by (induct ss rule: rev_induct) auto
 
 lemma Abs_apps_eq_Abs_apps_conv [iff]:
-    "\<And>ss. (Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)"
-  apply (induct rs rule: rev_induct)
+    "(Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)"
+  apply (induct rs fixing: ss rule: rev_induct)
    apply simp
    apply blast
   apply (induct_tac ss rule: rev_induct)
@@ -62,14 +53,12 @@
   done
 
 lemma Abs_App_neq_Var_apps [iff]:
-    "\<forall>s t. Abs s \<degree> t ~= Var n \<degree>\<degree> ss"
-  apply (induct_tac ss rule: rev_induct)
-   apply auto
-  done
+    "Abs s \<degree> t ~= Var n \<degree>\<degree> ss"
+  by (induct ss fixing: s t rule: rev_induct) auto
 
 lemma Var_apps_neq_Abs_apps [iff]:
-    "\<And>ts. Var n \<degree>\<degree> ts ~= Abs r \<degree>\<degree> ss"
-  apply (induct ss rule: rev_induct)
+    "Var n \<degree>\<degree> ts ~= Abs r \<degree>\<degree> ss"
+  apply (induct ss fixing: ts rule: rev_induct)
    apply simp
   apply (induct_tac ts rule: rev_induct)
    apply auto
@@ -77,7 +66,7 @@
 
 lemma ex_head_tail:
   "\<exists>ts h. t = h \<degree>\<degree> ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))"
-  apply (induct_tac t)
+  apply (induct t)
     apply (rule_tac x = "[]" in exI)
     apply simp
    apply clarify
@@ -89,21 +78,18 @@
 
 lemma size_apps [simp]:
   "size (r \<degree>\<degree> rs) = size r + foldl (op +) 0 (map size rs) + length rs"
-  apply (induct_tac rs rule: rev_induct)
-   apply auto
-  done
+  by (induct rs rule: rev_induct) auto
 
 lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k"
-  apply simp
-  done
+  by simp
 
 lemma lift_map [simp]:
-    "\<And>t. lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts"
-  by (induct ts) simp_all
+    "lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts"
+  by (induct ts fixing: t) simp_all
 
 lemma subst_map [simp]:
-    "\<And>t. subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts"
-  by (induct ts) simp_all
+    "subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts"
+  by (induct ts fixing: t) simp_all
 
 lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])"
   by simp
@@ -111,60 +97,51 @@
 
 text {* \medskip A customized induction schema for @{text "\<degree>\<degree>"}. *}
 
-lemma lem [rule_format (no_asm)]:
-  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts);
-    !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)
-  |] ==> \<forall>t. size t = n --> P t"
-proof -
-  case rule_context
-  show ?thesis
-   apply (induct_tac n rule: nat_less_induct)
-   apply (rule allI)
-   apply (cut_tac t = t in ex_head_tail)
+lemma lem:
+  assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)"
+    and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)"
+  shows "size t = n \<Longrightarrow> P t"
+  apply (induct n fixing: t rule: nat_less_induct)
+  apply (cut_tac t = t in ex_head_tail)
+  apply clarify
+  apply (erule disjE)
+   apply clarify
+   apply (rule prems)
    apply clarify
-   apply (erule disjE)
-    apply clarify
-    apply (rule prems)
-    apply clarify
-    apply (erule allE, erule impE)
-      prefer 2
-      apply (erule allE, erule mp, rule refl)
-     apply simp
-     apply (rule lem0)
-      apply force
-     apply (rule elem_le_sum)
-     apply force
-    apply clarify
-    apply (rule prems)
-     apply (erule allE, erule impE)
-      prefer 2
-      apply (erule allE, erule mp, rule refl)
-     apply simp
-    apply clarify
-    apply (erule allE, erule impE)
-     prefer 2
-     apply (erule allE, erule mp, rule refl)
-    apply simp
-    apply (rule le_imp_less_Suc)
-    apply (rule trans_le_add1)
-    apply (rule trans_le_add2)
-    apply (rule elem_le_sum)
+   apply (erule allE, erule impE)
+    prefer 2
+    apply (erule allE, erule mp, rule refl)
+   apply simp
+   apply (rule lem0)
     apply force
-    done
-qed
+   apply (rule elem_le_sum)
+   apply force
+  apply clarify
+  apply (rule prems)
+   apply (erule allE, erule impE)
+    prefer 2
+    apply (erule allE, erule mp, rule refl)
+   apply simp
+  apply clarify
+  apply (erule allE, erule impE)
+   prefer 2
+   apply (erule allE, erule mp, rule refl)
+  apply simp
+  apply (rule le_imp_less_Suc)
+  apply (rule trans_le_add1)
+  apply (rule trans_le_add2)
+  apply (rule elem_le_sum)
+  apply force
+  done
 
 theorem Apps_dB_induct:
-  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts);
-    !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)
-  |] ==> P t"
-proof -
-  case rule_context
-  show ?thesis
-    apply (rule_tac t = t in lem)
-      prefer 3
-      apply (rule refl)
-     apply (assumption | rule prems)+
-    done
-qed
+  assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)"
+    and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)"
+  shows "P t"
+  apply (rule_tac t = t in lem)
+    prefer 3
+    apply (rule refl)
+   apply (assumption | rule prems)+
+  done
 
 end
diff -r 3b72f559e942 -r afdba6b3e383 src/HOL/Lambda/ListBeta.thy
--- a/src/HOL/Lambda/ListBeta.thy	Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/ListBeta.thy	Wed Nov 23 22:26:13 2005 +0100
@@ -18,8 +18,8 @@
   "rs => ss" == "(rs, ss) : step1 beta"
 
 lemma head_Var_reduction_aux:
-  "v -> v' ==> \<forall>rs. v = Var n \<degree>\<degree> rs --> (\<exists>ss. rs => ss \<and> v' = Var n \<degree>\<degree> ss)"
-  apply (erule beta.induct)
+  "v -> v' ==> (\<forall>rs. v = Var n \<degree>\<degree> rs --> (\<exists>ss. rs => ss \<and> v' = Var n \<degree>\<degree> ss))"
+  apply (induct set: beta)
      apply simp
     apply (rule allI)
     apply (rule_tac xs = rs in rev_exhaust)
@@ -33,16 +33,14 @@
 
 lemma head_Var_reduction:
   "Var n \<degree>\<degree> rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss)"
-  apply (drule head_Var_reduction_aux)
-  apply blast
-  done
+  by (drule head_Var_reduction_aux) blast
 
 lemma apps_betasE_aux:
   "u -> u' ==> \<forall>r rs. u = r \<degree>\<degree> rs -->
     ((\<exists>r'. r -> r' \<and> u' = r' \<degree>\<degree> rs) \<or>
      (\<exists>rs'. rs => rs' \<and> u' = r \<degree>\<degree> rs') \<or>
      (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] \<degree>\<degree> ts))"
-  apply (erule beta.induct)
+  apply (induct set: beta)
      apply (clarify del: disjCI)
      apply (case_tac r)
        apply simp
@@ -70,38 +68,31 @@
   done
 
 lemma apps_betasE [elim!]:
-  "[| r \<degree>\<degree> rs -> s; !!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R;
-    !!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R;
-    !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R |]
-  ==> R"
-proof -
-  assume major: "r \<degree>\<degree> rs -> s"
-  case rule_context
-  show ?thesis
-    apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
-    apply (assumption | rule refl | erule prems exE conjE impE disjE)+
-    done
-qed
+  assumes major: "r \<degree>\<degree> rs -> s"
+    and "!!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R"
+    and "!!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R"
+    and "!!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R"
+  shows R
+  apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
+  apply (assumption | rule refl | erule prems exE conjE impE disjE)+
+  done
 
 lemma apps_preserves_beta [simp]:
     "r -> s ==> r \<degree>\<degree> ss -> s \<degree>\<degree> ss"
-  apply (induct_tac ss rule: rev_induct)
-  apply auto
-  done
+  by (induct ss rule: rev_induct) auto
 
 lemma apps_preserves_beta2 [simp]:
     "r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss"
-  apply (erule rtrancl_induct)
+  apply (induct set: rtrancl)
    apply blast
   apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
   done
 
-lemma apps_preserves_betas [rule_format, simp]:
-    "\<forall>ss. rs => ss --> r \<degree>\<degree> rs -> r \<degree>\<degree> ss"
-  apply (induct_tac rs rule: rev_induct)
+lemma apps_preserves_betas [simp]:
+    "rs => ss \<Longrightarrow> r \<degree>\<degree> rs -> r \<degree>\<degree> ss"
+  apply (induct rs fixing: ss rule: rev_induct)
    apply simp
   apply simp
-  apply clarify
   apply (rule_tac xs = ss in rev_exhaust)
    apply simp
   apply simp
diff -r 3b72f559e942 -r afdba6b3e383 src/HOL/Lambda/ListOrder.thy
--- a/src/HOL/Lambda/ListOrder.thy	Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/ListOrder.thy	Wed Nov 23 22:26:13 2005 +0100
@@ -87,18 +87,17 @@
   apply blast
   done
 
-lemma Cons_acc_step1I [rule_format, intro!]:
-    "x \<in> acc r ==> \<forall>xs. xs \<in> acc (step1 r) --> x # xs \<in> acc (step1 r)"
-  apply (erule acc_induct)
+lemma Cons_acc_step1I [intro!]:
+    "x \<in> acc r ==> (!!xs. xs \<in> acc (step1 r) \<Longrightarrow> x # xs \<in> acc (step1 r))"
+  apply (induct set: acc)
   apply (erule thin_rl)
-  apply clarify
   apply (erule acc_induct)
   apply (rule accI)
   apply blast
   done
 
 lemma lists_accD: "xs \<in> lists (acc r) ==> xs \<in> acc (step1 r)"
-  apply (erule lists.induct)
+  apply (induct set: lists)
    apply (rule accI)
    apply simp
   apply (rule accI)
@@ -114,7 +113,7 @@
   done
 
 lemma lists_accI: "xs \<in> acc (step1 r) ==> xs \<in> lists (acc r)"
-  apply (erule acc_induct)
+  apply (induct set: acc)
   apply clarify
   apply (rule accI)
   apply (drule ex_step1I, assumption)
diff -r 3b72f559e942 -r afdba6b3e383 src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/ParRed.thy	Wed Nov 23 22:26:13 2005 +0100
@@ -43,13 +43,10 @@
 
 lemma par_beta_varL [simp]:
     "(Var n => t) = (t = Var n)"
-  apply blast
-  done
+  by blast
 
 lemma par_beta_refl [simp]: "t => t"  (* par_beta_refl [intro!] causes search to blow up *)
-  apply (induct_tac t)
-    apply simp_all
-  done
+  by (induct t) simp_all
 
 lemma beta_subset_par_beta: "beta <= par_beta"
   apply (rule subsetI)
@@ -70,17 +67,14 @@
 
 subsection {* Misc properties of par-beta *}
 
-lemma par_beta_lift [rule_format, simp]:
-    "\<forall>t' n. t => t' --> lift t n => lift t' n"
-  apply (induct_tac t)
-    apply fastsimp+
-  done
+lemma par_beta_lift [simp]:
+    "t => t' \<Longrightarrow> lift t n => lift t' n"
+  by (induct t fixing: t' n) fastsimp+
 
-lemma par_beta_subst [rule_format]:
-    "\<forall>s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"
-  apply (induct_tac t)
+lemma par_beta_subst:
+    "s => s' \<Longrightarrow> t => t' \<Longrightarrow> t[s/n] => t'[s'/n]"
+  apply (induct t fixing: s s' t' n)
     apply (simp add: subst_Var)
-   apply (intro strip)
    apply (erule par_beta_cases)
     apply simp
    apply (simp add: subst_subst [symmetric])
@@ -110,9 +104,8 @@
   "cd (Abs u \<degree> t) = (cd u)[cd t/0]"
   "cd (Abs s) = Abs (cd s)"
 
-lemma par_beta_cd [rule_format]:
-    "\<forall>t. s => t --> t => cd s"
-  apply (induct_tac s rule: cd.induct)
+lemma par_beta_cd: "s => t \<Longrightarrow> t => cd s"
+  apply (induct s fixing: t rule: cd.induct)
       apply auto
   apply (fast intro!: par_beta_subst)
   done
diff -r 3b72f559e942 -r afdba6b3e383 src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/Type.thy	Wed Nov 23 22:26:13 2005 +0100
@@ -94,8 +94,8 @@
 subsection {* Lists of types *}
 
 lemma lists_typings:
-    "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
-  apply (induct ts)
+    "e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
+  apply (induct ts fixing: Ts)
    apply (case_tac Ts)
      apply simp
      apply (rule lists.Nil)
@@ -108,16 +108,16 @@
   apply blast
   done
 
-lemma types_snoc: "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<tturnstile> ts @ [t] : Ts @ [T]"
-  apply (induct ts)
+lemma types_snoc: "e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<tturnstile> ts @ [t] : Ts @ [T]"
+  apply (induct ts fixing: Ts)
   apply simp
   apply (case_tac Ts)
   apply simp+
   done
 
-lemma types_snoc_eq: "\<And>Ts. e \<tturnstile> ts @ [t] : Ts @ [T] =
+lemma types_snoc_eq: "e \<tturnstile> ts @ [t] : Ts @ [T] =
   (e \<tturnstile> ts : Ts \<and> e \<turnstile> t : T)"
-  apply (induct ts)
+  apply (induct ts fixing: Ts)
   apply (case_tac Ts)
   apply simp+
   apply (case_tac Ts)
@@ -156,8 +156,8 @@
 subsection {* n-ary function types *}
 
 lemma list_app_typeD:
-    "\<And>t T. e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
-  apply (induct ts)
+    "e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
+  apply (induct ts fixing: t T)
    apply simp
   apply atomize
   apply simp
@@ -176,8 +176,8 @@
   by (insert list_app_typeD) fast
 
 lemma list_app_typeI:
-    "\<And>t T Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T"
-  apply (induct ts)
+    "e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T"
+  apply (induct ts fixing: t T Ts)
    apply simp
   apply atomize
   apply (case_tac Ts)
@@ -201,8 +201,8 @@
 *}
 
 theorem var_app_type_eq:
-  "\<And>T U. e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U"
-  apply (induct ts rule: rev_induct)
+  "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U"
+  apply (induct ts fixing: T U rule: rev_induct)
   apply simp
   apply (ind_cases "e \<turnstile> Var i : T")
   apply (ind_cases "e \<turnstile> Var i : T")
@@ -220,9 +220,9 @@
   apply simp
   done
 
-lemma var_app_types: "\<And>ts Ts U. e \<turnstile> Var i \<degree>\<degree> ts \<degree>\<degree> us : T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow>
+lemma var_app_types: "e \<turnstile> Var i \<degree>\<degree> ts \<degree>\<degree> us : T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow>
   e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> \<exists>Us. U = Us \<Rrightarrow> T \<and> e \<tturnstile> us : Us"
-  apply (induct us)
+  apply (induct us fixing: ts Ts U)
   apply simp
   apply (erule var_app_type_eq)
   apply assumption
@@ -292,8 +292,8 @@
   by (induct set: typing) auto
 
 lemma lift_types:
-  "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
-  apply (induct ts)
+  "e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
+  apply (induct ts fixing: Ts)
    apply simp
   apply (case_tac Ts)
    apply auto
@@ -311,9 +311,9 @@
   done
 
 lemma substs_lemma:
-  "\<And>Ts. e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow>
+  "e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow>
      e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts"
-  apply (induct ts)
+  apply (induct ts fixing: Ts)
    apply (case_tac Ts)
     apply simp
    apply simp
@@ -352,18 +352,16 @@
 subsection {* Alternative induction rule for types *}
 
 lemma type_induct [induct type]:
+  assumes
   "(\<And>T. (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T1) \<Longrightarrow>
-   (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T2) \<Longrightarrow> P T) \<Longrightarrow> P T"
-proof -
-  case rule_context
-  show ?thesis
-  proof (induct T)
-    case Atom
-    show ?case by (rule rule_context) simp_all
-  next
-    case Fun
-    show ?case  by (rule rule_context) (insert Fun, simp_all)
-  qed
+    (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T2) \<Longrightarrow> P T)"
+  shows "P T"
+proof (induct T)
+  case Atom
+  show ?case by (rule prems) simp_all
+next
+  case Fun
+  show ?case  by (rule prems) (insert Fun, simp_all)
 qed
 
 end
diff -r 3b72f559e942 -r afdba6b3e383 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy	Wed Nov 23 22:26:13 2005 +0100
@@ -52,14 +52,14 @@
   done
 
 lemma listall_conj1: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall P xs"
-  by (induct xs) simp+
+  by (induct xs) simp_all
 
 lemma listall_conj2: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall Q xs"
-  by (induct xs) simp+
+  by (induct xs) simp_all
 
 lemma listall_app: "listall P (xs @ ys) = (listall P xs \<and> listall P ys)"
   apply (induct xs)
-  apply (rule iffI, simp, simp)
+   apply (rule iffI, simp, simp)
   apply (rule iffI, simp, simp)
   done
 
diff -r 3b72f559e942 -r afdba6b3e383 src/HOL/Library/Accessible_Part.thy
--- a/src/HOL/Library/Accessible_Part.thy	Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Library/Accessible_Part.thy	Wed Nov 23 22:26:13 2005 +0100
@@ -32,19 +32,15 @@
 subsection {* Induction rules *}
 
 theorem acc_induct:
-  "a \<in> acc r ==>
-    (!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x) ==> P a"
-proof -
-  assume major: "a \<in> acc r"
-  assume hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
-  show ?thesis
-    apply (rule major [THEN acc.induct])
-    apply (rule hyp)
-     apply (rule accI)
-     apply fast
-    apply fast
-    done
-qed
+  assumes major: "a \<in> acc r"
+  assumes hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
+  shows "P a"
+  apply (rule major [THEN acc.induct])
+  apply (rule hyp)
+   apply (rule accI)
+   apply fast
+  apply fast
+  done
 
 theorems acc_induct_rule = acc_induct [rule_format, induct set: acc]