tuned induction proofs;
authorwenzelm
Wed Nov 23 22:26:13 2005 +0100 (2005-11-23)
changeset 18241afdba6b3e383
parent 18240 3b72f559e942
child 18242 2215049cd29c
tuned induction proofs;
src/HOL/Isar_examples/Fibonacci.thy
src/HOL/Isar_examples/Hoare.thy
src/HOL/Isar_examples/MutilatedCheckerboard.thy
src/HOL/Lambda/Commutation.thy
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/InductTermi.thy
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/ListApplication.thy
src/HOL/Lambda/ListBeta.thy
src/HOL/Lambda/ListOrder.thy
src/HOL/Lambda/ParRed.thy
src/HOL/Lambda/Type.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/Library/Accessible_Part.thy
     1.1 --- a/src/HOL/Isar_examples/Fibonacci.thy	Wed Nov 23 22:23:52 2005 +0100
     1.2 +++ b/src/HOL/Isar_examples/Fibonacci.thy	Wed Nov 23 22:26:13 2005 +0100
     1.3 @@ -124,7 +124,7 @@
     1.4  qed
     1.5  
     1.6  lemma gcd_fib_mod:
     1.7 -  assumes m: "0 < m"
     1.8 +  assumes "0 < m"
     1.9    shows "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
    1.10  proof (induct n rule: nat_less_induct)
    1.11    case (1 n) note hyp = this
    1.12 @@ -137,7 +137,7 @@
    1.13        case True then show ?thesis by simp
    1.14      next
    1.15        case False then have "m <= n" by simp
    1.16 -      from m and False have "n - m < n" by simp
    1.17 +      from `0 < m` and False have "n - m < n" by simp
    1.18        with hyp have "gcd (fib m, fib ((n - m) mod m))
    1.19          = gcd (fib m, fib (n - m))" by simp
    1.20        also have "... = gcd (fib m, fib n)"
     2.1 --- a/src/HOL/Isar_examples/Hoare.thy	Wed Nov 23 22:23:52 2005 +0100
     2.2 +++ b/src/HOL/Isar_examples/Hoare.thy	Wed Nov 23 22:26:13 2005 +0100
     2.3 @@ -160,14 +160,15 @@
     2.4   semantics of \texttt{WHILE}.
     2.5  *}
     2.6  
     2.7 -theorem while: "|- (P Int b) c P ==> |- P (While b X c) (P Int -b)"
     2.8 +theorem while:
     2.9 +  assumes body: "|- (P Int b) c P"
    2.10 +  shows "|- P (While b X c) (P Int -b)"
    2.11  proof
    2.12 -  assume body: "|- (P Int b) c P"
    2.13    fix s s' assume s: "s : P"
    2.14    assume "Sem (While b X c) s s'"
    2.15 -  then obtain n where iter: "iter n b (Sem c) s s'" by auto
    2.16 -  have "!!s. iter n b (Sem c) s s' ==> s : P ==> s' : P Int -b"
    2.17 -  proof (induct n)
    2.18 +  then obtain n where "iter n b (Sem c) s s'" by auto
    2.19 +  from this and s show "s' : P Int -b"
    2.20 +  proof (induct n fixing: s)
    2.21      case (0 s)
    2.22      thus ?case by auto
    2.23    next
    2.24 @@ -179,7 +180,6 @@
    2.25      with body sem have "s'' : P" ..
    2.26      with iter show ?case by (rule Suc)
    2.27    qed
    2.28 -  from this iter s show "s' : P Int -b" .
    2.29  qed
    2.30  
    2.31  
    2.32 @@ -424,8 +424,8 @@
    2.33      \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
    2.34    by (auto simp: Valid_def)
    2.35  
    2.36 -lemma iter_aux: "
    2.37 -  \<forall>s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
    2.38 +lemma iter_aux:
    2.39 +  "\<forall>s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
    2.40         (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)"
    2.41    apply(induct n)
    2.42     apply clarsimp
     3.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Nov 23 22:23:52 2005 +0100
     3.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Nov 23 22:26:13 2005 +0100
     3.3 @@ -169,24 +169,21 @@
     3.4  qed
     3.5  
     3.6  lemma domino_singleton:
     3.7 -  assumes "d : domino" and "b < 2"
     3.8 -  shows "EX i j. evnodd d b = {(i, j)}"
     3.9 -proof -
    3.10 -  from `d : domino`
    3.11 -  show ?thesis (is "?P d")
    3.12 -  proof induct
    3.13 -    from `b < 2` have b_cases: "b = 0 | b = 1" by arith
    3.14 -    fix i j
    3.15 -    note [simp] = evnodd_empty evnodd_insert mod_Suc
    3.16 -    from b_cases show "?P {(i, j), (i, j + 1)}" by rule auto
    3.17 -    from b_cases show "?P {(i, j), (i + 1, j)}" by rule auto
    3.18 -  qed
    3.19 +  assumes d: "d : domino" and "b < 2"
    3.20 +  shows "EX i j. evnodd d b = {(i, j)}"  (is "?P d")
    3.21 +  using d
    3.22 +proof induct
    3.23 +  from `b < 2` have b_cases: "b = 0 | b = 1" by arith
    3.24 +  fix i j
    3.25 +  note [simp] = evnodd_empty evnodd_insert mod_Suc
    3.26 +  from b_cases show "?P {(i, j), (i, j + 1)}" by rule auto
    3.27 +  from b_cases show "?P {(i, j), (i + 1, j)}" by rule auto
    3.28  qed
    3.29  
    3.30  lemma domino_finite:
    3.31 -  assumes "d: domino"
    3.32 +  assumes d: "d: domino"
    3.33    shows "finite d"
    3.34 -  using prems
    3.35 +  using d
    3.36  proof induct
    3.37    fix i j :: nat
    3.38    show "finite {(i, j), (i, j + 1)}" by (intro Finites.intros)
    3.39 @@ -197,9 +194,9 @@
    3.40  subsection {* Tilings of dominoes *}
    3.41  
    3.42  lemma tiling_domino_finite:
    3.43 -  assumes "t : tiling domino"  (is "t : ?T")
    3.44 +  assumes t: "t : tiling domino"  (is "t : ?T")
    3.45    shows "finite t"  (is "?F t")
    3.46 -  using `t : ?T`
    3.47 +  using t
    3.48  proof induct
    3.49    show "?F {}" by (rule Finites.emptyI)
    3.50    fix a t assume "?F t"
    3.51 @@ -208,9 +205,9 @@
    3.52  qed
    3.53  
    3.54  lemma tiling_domino_01:
    3.55 -  assumes "t : tiling domino"  (is "t : ?T")
    3.56 +  assumes t: "t : tiling domino"  (is "t : ?T")
    3.57    shows "card (evnodd t 0) = card (evnodd t 1)"
    3.58 -  using `t : ?T`
    3.59 +  using t
    3.60  proof induct
    3.61    case empty
    3.62    show ?case by (simp add: evnodd_def)
     4.1 --- a/src/HOL/Lambda/Commutation.thy	Wed Nov 23 22:23:52 2005 +0100
     4.2 +++ b/src/HOL/Lambda/Commutation.thy	Wed Nov 23 22:26:13 2005 +0100
     4.3 @@ -197,11 +197,11 @@
     4.4      \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
     4.5    shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
     4.6                 \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
     4.7 -using wf
     4.8 +  using wf
     4.9  proof induct
    4.10    case (less x b c)
    4.11 -  have IH: "\<And>y b c. \<lbrakk>(y,x) \<in> R\<inverse>; (y,b) \<in> R\<^sup>*; (y,c) \<in> R\<^sup>*\<rbrakk>
    4.12 -                     \<Longrightarrow> \<exists>d. (b,d) \<in> R\<^sup>* \<and> (c,d) \<in> R\<^sup>*" by(rule less)
    4.13 +  note IH = `\<And>y b c. \<lbrakk>(y,x) \<in> R\<inverse>; (y,b) \<in> R\<^sup>*; (y,c) \<in> R\<^sup>*\<rbrakk>
    4.14 +                     \<Longrightarrow> \<exists>d. (b,d) \<in> R\<^sup>* \<and> (c,d) \<in> R\<^sup>*`
    4.15    have xc: "(x, c) \<in> R\<^sup>*" .
    4.16    have xb: "(x, b) \<in> R\<^sup>*" .
    4.17    thus ?case
    4.18 @@ -223,11 +223,11 @@
    4.19        assume y'c: "(y', c) \<in> R\<^sup>*"
    4.20        assume xy': "(x, y') \<in> R"
    4.21        with xy obtain u where u: "(y, u) \<in> R\<^sup>*" "(y', u) \<in> R\<^sup>*"
    4.22 -	by (blast dest:lc)
    4.23 +        by (blast dest: lc)
    4.24        from yb u y'c show ?thesis
    4.25 -	by(blast del: rtrancl_refl
    4.26 -		 intro:rtrancl_trans
    4.27 -                 dest:IH[OF xy[symmetric]] IH[OF xy'[symmetric]])
    4.28 +        by (blast del: rtrancl_refl
    4.29 +            intro: rtrancl_trans
    4.30 +            dest: IH [OF xy [symmetric]] IH [OF xy' [symmetric]])
    4.31      qed
    4.32    qed
    4.33  qed
     5.1 --- a/src/HOL/Lambda/Eta.thy	Wed Nov 23 22:23:52 2005 +0100
     5.2 +++ b/src/HOL/Lambda/Eta.thy	Wed Nov 23 22:26:13 2005 +0100
     5.3 @@ -45,24 +45,20 @@
     5.4  
     5.5  subsection "Properties of eta, subst and free"
     5.6  
     5.7 -lemma subst_not_free [rule_format, simp]:
     5.8 -    "\<forall>i t u. \<not> free s i --> s[t/i] = s[u/i]"
     5.9 -  apply (induct_tac s)
    5.10 -    apply (simp_all add: subst_Var)
    5.11 -  done
    5.12 +lemma subst_not_free [simp]: "\<not> free s i \<Longrightarrow> s[t/i] = s[u/i]"
    5.13 +  by (induct s fixing: i t u) (simp_all add: subst_Var)
    5.14  
    5.15  lemma free_lift [simp]:
    5.16 -    "\<forall>i k. free (lift t k) i =
    5.17 -      (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
    5.18 -  apply (induct_tac t)
    5.19 +    "free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
    5.20 +  apply (induct t fixing: i k)
    5.21      apply (auto cong: conj_cong)
    5.22    apply arith
    5.23    done
    5.24  
    5.25  lemma free_subst [simp]:
    5.26 -    "\<forall>i k t. free (s[t/k]) i =
    5.27 +    "free (s[t/k]) i =
    5.28        (free s k \<and> free t i \<or> free s (if i < k then i else i + 1))"
    5.29 -  apply (induct_tac s)
    5.30 +  apply (induct s fixing: i k t)
    5.31      prefer 2
    5.32      apply simp
    5.33      apply blast
    5.34 @@ -71,25 +67,19 @@
    5.35    apply (simp add: diff_Suc subst_Var split: nat.split)
    5.36    done
    5.37  
    5.38 -lemma free_eta [rule_format]:
    5.39 -    "s -e> t ==> \<forall>i. free t i = free s i"
    5.40 -  apply (erule eta.induct)
    5.41 -     apply (simp_all cong: conj_cong)
    5.42 -  done
    5.43 +lemma free_eta: "s -e> t ==> (!!i. free t i = free s i)"
    5.44 +  by (induct set: eta) (simp_all cong: conj_cong)
    5.45  
    5.46  lemma not_free_eta:
    5.47      "[| s -e> t; \<not> free s i |] ==> \<not> free t i"
    5.48 -  apply (simp add: free_eta)
    5.49 -  done
    5.50 +  by (simp add: free_eta)
    5.51  
    5.52 -lemma eta_subst [rule_format, simp]:
    5.53 -    "s -e> t ==> \<forall>u i. s[u/i] -e> t[u/i]"
    5.54 -  apply (erule eta.induct)
    5.55 -  apply (simp_all add: subst_subst [symmetric])
    5.56 -  done
    5.57 +lemma eta_subst [simp]:
    5.58 +    "s -e> t ==> (!!u i. s[u/i] -e> t[u/i])"
    5.59 +  by (induct set: eta) (simp_all add: subst_subst [symmetric])
    5.60  
    5.61 -theorem lift_subst_dummy: "\<And>i dummy. \<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s"
    5.62 -  by (induct s) simp_all
    5.63 +theorem lift_subst_dummy: "\<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s"
    5.64 +  by (induct s fixing: i dummy) simp_all
    5.65  
    5.66  
    5.67  subsection "Confluence of eta"
    5.68 @@ -114,56 +104,40 @@
    5.69  subsection "Congruence rules for eta*"
    5.70  
    5.71  lemma rtrancl_eta_Abs: "s -e>> s' ==> Abs s -e>> Abs s'"
    5.72 -  apply (erule rtrancl_induct)
    5.73 -   apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
    5.74 -  done
    5.75 +  by (induct set: rtrancl)
    5.76 +    (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
    5.77  
    5.78  lemma rtrancl_eta_AppL: "s -e>> s' ==> s \<degree> t -e>> s' \<degree> t"
    5.79 -  apply (erule rtrancl_induct)
    5.80 -   apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
    5.81 -  done
    5.82 +  by (induct set: rtrancl)
    5.83 +    (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
    5.84  
    5.85  lemma rtrancl_eta_AppR: "t -e>> t' ==> s \<degree> t -e>> s \<degree> t'"
    5.86 -  apply (erule rtrancl_induct)
    5.87 -   apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
    5.88 -  done
    5.89 +  by (induct set: rtrancl) (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
    5.90  
    5.91  lemma rtrancl_eta_App:
    5.92      "[| s -e>> s'; t -e>> t' |] ==> s \<degree> t -e>> s' \<degree> t'"
    5.93 -  apply (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans)
    5.94 -  done
    5.95 +  by (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans)
    5.96  
    5.97  
    5.98  subsection "Commutation of beta and eta"
    5.99  
   5.100 -lemma free_beta [rule_format]:
   5.101 -    "s -> t ==> \<forall>i. free t i --> free s i"
   5.102 -  apply (erule beta.induct)
   5.103 -     apply simp_all
   5.104 -  done
   5.105 +lemma free_beta:
   5.106 +    "s -> t ==> (!!i. free t i \<Longrightarrow> free s i)"
   5.107 +  by (induct set: beta) auto
   5.108  
   5.109 -lemma beta_subst [rule_format, intro]:
   5.110 -    "s -> t ==> \<forall>u i. s[u/i] -> t[u/i]"
   5.111 -  apply (erule beta.induct)
   5.112 -     apply (simp_all add: subst_subst [symmetric])
   5.113 -  done
   5.114 +lemma beta_subst [intro]: "s -> t ==> (!!u i. s[u/i] -> t[u/i])"
   5.115 +  by (induct set: beta) (simp_all add: subst_subst [symmetric])
   5.116  
   5.117 -lemma subst_Var_Suc [simp]: "\<forall>i. t[Var i/i] = t[Var(i)/i + 1]"
   5.118 -  apply (induct_tac t)
   5.119 -  apply (auto elim!: linorder_neqE simp: subst_Var)
   5.120 -  done
   5.121 +lemma subst_Var_Suc [simp]: "t[Var i/i] = t[Var(i)/i + 1]"
   5.122 +  by (induct t fixing: i) (auto elim!: linorder_neqE simp: subst_Var)
   5.123  
   5.124 -lemma eta_lift [rule_format, simp]:
   5.125 -    "s -e> t ==> \<forall>i. lift s i -e> lift t i"
   5.126 -  apply (erule eta.induct)
   5.127 -     apply simp_all
   5.128 -  done
   5.129 +lemma eta_lift [simp]: "s -e> t ==> (!!i. lift s i -e> lift t i)"
   5.130 +  by (induct set: eta) simp_all
   5.131  
   5.132 -lemma rtrancl_eta_subst [rule_format]:
   5.133 -    "\<forall>s t i. s -e> t --> u[s/i] -e>> u[t/i]"
   5.134 -  apply (induct_tac u)
   5.135 +lemma rtrancl_eta_subst: "s -e> t \<Longrightarrow> u[s/i] -e>> u[t/i]"
   5.136 +  apply (induct u fixing: s t i)
   5.137      apply (simp_all add: subst_Var)
   5.138 -    apply (blast)
   5.139 +    apply blast
   5.140     apply (blast intro: rtrancl_eta_App)
   5.141    apply (blast intro!: rtrancl_eta_Abs eta_lift)
   5.142    done
   5.143 @@ -191,11 +165,10 @@
   5.144  
   5.145  text {* @{term "Abs (lift s 0 \<degree> Var 0) -e> s"} *}
   5.146  
   5.147 -lemma not_free_iff_lifted [rule_format]:
   5.148 -    "\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)"
   5.149 -  apply (induct_tac s)
   5.150 +lemma not_free_iff_lifted:
   5.151 +    "(\<not> free s i) = (\<exists>t. s = lift t i)"
   5.152 +  apply (induct s fixing: i)
   5.153      apply simp
   5.154 -    apply clarify
   5.155      apply (rule iffI)
   5.156       apply (erule linorder_neqE)
   5.157        apply (rule_tac x = "Var nat" in exI)
   5.158 @@ -214,7 +187,6 @@
   5.159     apply simp
   5.160     apply (erule thin_rl)
   5.161     apply (erule thin_rl)
   5.162 -   apply (rule allI)
   5.163     apply (rule iffI)
   5.164      apply (elim conjE exE)
   5.165      apply (rename_tac u1 u2)
   5.166 @@ -229,7 +201,6 @@
   5.167     apply simp
   5.168    apply simp
   5.169    apply (erule thin_rl)
   5.170 -  apply (rule allI)
   5.171    apply (rule iffI)
   5.172     apply (erule exE)
   5.173     apply (rule_tac x = "Abs t" in exI)
   5.174 @@ -246,8 +217,7 @@
   5.175  theorem explicit_is_implicit:
   5.176    "(\<forall>s u. (\<not> free s 0) --> R (Abs (s \<degree> Var 0)) (s[u/0])) =
   5.177      (\<forall>s. R (Abs (lift s 0 \<degree> Var 0)) s)"
   5.178 -  apply (auto simp add: not_free_iff_lifted)
   5.179 -  done
   5.180 +  by (auto simp add: not_free_iff_lifted)
   5.181  
   5.182  
   5.183  subsection {* Parallel eta-reduction *}
   5.184 @@ -270,22 +240,23 @@
   5.185    app [simp, intro]: "s \<Rightarrow>\<^sub>\<eta> s' \<Longrightarrow> t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> s \<degree> t \<Rightarrow>\<^sub>\<eta> s' \<degree> t'"
   5.186    abs [simp, intro]: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> Abs s \<Rightarrow>\<^sub>\<eta> Abs t"
   5.187  
   5.188 -lemma free_par_eta [simp]: assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
   5.189 -  shows "\<And>i. free t i = free s i" using eta
   5.190 -  by induct (simp_all cong: conj_cong)
   5.191 +lemma free_par_eta [simp]:
   5.192 +  assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
   5.193 +  shows "free t i = free s i" using eta
   5.194 +  by (induct fixing: i) (simp_all cong: conj_cong)
   5.195  
   5.196  lemma par_eta_refl [simp]: "t \<Rightarrow>\<^sub>\<eta> t"
   5.197    by (induct t) simp_all
   5.198  
   5.199  lemma par_eta_lift [simp]:
   5.200    assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
   5.201 -  shows "\<And>i. lift s i \<Rightarrow>\<^sub>\<eta> lift t i" using eta
   5.202 -  by induct simp_all
   5.203 +  shows "lift s i \<Rightarrow>\<^sub>\<eta> lift t i" using eta
   5.204 +  by (induct fixing: i) simp_all
   5.205  
   5.206  lemma par_eta_subst [simp]:
   5.207    assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
   5.208 -  shows "\<And>u u' i. u \<Rightarrow>\<^sub>\<eta> u' \<Longrightarrow> s[u/i] \<Rightarrow>\<^sub>\<eta> t[u'/i]" using eta
   5.209 -  by induct (simp_all add: subst_subst [symmetric] subst_Var)
   5.210 +  shows "u \<Rightarrow>\<^sub>\<eta> u' \<Longrightarrow> s[u/i] \<Rightarrow>\<^sub>\<eta> t[u'/i]" using eta
   5.211 +  by (induct fixing: u u' i) (simp_all add: subst_subst [symmetric] subst_Var)
   5.212  
   5.213  theorem eta_subset_par_eta: "eta \<subseteq> par_eta"
   5.214    apply (rule subsetI)
   5.215 @@ -320,16 +291,16 @@
   5.216    eta_expand_Suc: "eta_expand (Suc n) t = Abs (lift (eta_expand n t) 0 \<degree> Var 0)"
   5.217  
   5.218  lemma eta_expand_Suc':
   5.219 -  "\<And>t. eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 \<degree> Var 0))"
   5.220 -  by (induct n) simp_all
   5.221 +  "eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 \<degree> Var 0))"
   5.222 +  by (induct n fixing: t) simp_all
   5.223  
   5.224  theorem lift_eta_expand: "lift (eta_expand k t) i = eta_expand k (lift t i)"
   5.225    by (induct k) (simp_all add: lift_lift)
   5.226  
   5.227  theorem eta_expand_beta:
   5.228    assumes u: "u => u'"
   5.229 -  shows "\<And>t t'. t => t' \<Longrightarrow> eta_expand k (Abs t) \<degree> u => t'[u'/0]"
   5.230 -proof (induct k)
   5.231 +  shows "t => t' \<Longrightarrow> eta_expand k (Abs t) \<degree> u => t'[u'/0]"
   5.232 +proof (induct k fixing: t t')
   5.233    case 0 with u show ?case by simp
   5.234  next
   5.235    case (Suc k)
   5.236 @@ -343,8 +314,8 @@
   5.237    shows "eta_expand k t => eta_expand k t'"
   5.238    by (induct k) (simp_all add: t)
   5.239  
   5.240 -theorem eta_expand_eta: "\<And>t t'. t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> eta_expand k t \<Rightarrow>\<^sub>\<eta> t'"
   5.241 -proof (induct k)
   5.242 +theorem eta_expand_eta: "t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> eta_expand k t \<Rightarrow>\<^sub>\<eta> t'"
   5.243 +proof (induct k fixing: t t')
   5.244    case 0
   5.245    show ?case by simp
   5.246  next
   5.247 @@ -358,9 +329,9 @@
   5.248  subsection {* Elimination rules for parallel eta reduction *}
   5.249  
   5.250  theorem par_eta_elim_app: assumes eta: "t \<Rightarrow>\<^sub>\<eta> u"
   5.251 -  shows "\<And>u1' u2'. u = u1' \<degree> u2' \<Longrightarrow>
   5.252 +  shows "u = u1' \<degree> u2' \<Longrightarrow>
   5.253      \<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
   5.254 -proof induct
   5.255 +proof (induct fixing: u1' u2')
   5.256    case (app s s' t t')
   5.257    have "s \<degree> t = eta_expand 0 (s \<degree> t)" by simp
   5.258    with app show ?case by blast
   5.259 @@ -388,9 +359,9 @@
   5.260  qed
   5.261  
   5.262  theorem par_eta_elim_abs: assumes eta: "t \<Rightarrow>\<^sub>\<eta> t'"
   5.263 -  shows "\<And>u'. t' = Abs u' \<Longrightarrow>
   5.264 +  shows "t' = Abs u' \<Longrightarrow>
   5.265      \<exists>u k. t = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u'" using eta
   5.266 -proof induct
   5.267 +proof (induct fixing: u')
   5.268    case (abs s t)
   5.269    have "Abs s = eta_expand 0 (Abs s)" by simp
   5.270    with abs show ?case by blast
   5.271 @@ -420,8 +391,9 @@
   5.272  Based on a proof by Masako Takahashi \cite{Takahashi-IandC}.
   5.273  *}
   5.274  
   5.275 -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"
   5.276 -proof (induct t rule: measure_induct [of size, rule_format])
   5.277 +theorem par_eta_beta: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' \<Rightarrow>\<^sub>\<eta> u"
   5.278 +proof (induct t fixing: s u
   5.279 +    rule: measure_induct [of size, rule_format])
   5.280    case (1 t)
   5.281    from 1(3)
   5.282    show ?case
   5.283 @@ -467,10 +439,10 @@
   5.284  qed
   5.285  
   5.286  theorem eta_postponement': assumes eta: "s -e>> t"
   5.287 -  shows "\<And>u. t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' -e>> u"
   5.288 +  shows "t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' -e>> u"
   5.289    using eta [simplified rtrancl_subset
   5.290      [OF eta_subset_par_eta par_eta_subset_eta, symmetric]]
   5.291 -proof induct
   5.292 +proof (induct fixing: u)
   5.293    case 1
   5.294    thus ?case by blast
   5.295  next
     6.1 --- a/src/HOL/Lambda/InductTermi.thy	Wed Nov 23 22:23:52 2005 +0100
     6.2 +++ b/src/HOL/Lambda/InductTermi.thy	Wed Nov 23 22:26:13 2005 +0100
     6.3 @@ -45,7 +45,7 @@
     6.4    done
     6.5  
     6.6  lemma IT_implies_termi: "t : IT ==> t : termi beta"
     6.7 -  apply (erule IT.induct)
     6.8 +  apply (induct set: IT)
     6.9      apply (drule rev_subsetD)
    6.10       apply (rule lists_mono)
    6.11       apply (rule Int_lower2)
    6.12 @@ -63,16 +63,14 @@
    6.13  
    6.14  subsection {* Every terminating term is in IT *}
    6.15  
    6.16 -declare Var_apps_neq_Abs_apps [THEN not_sym, simp]
    6.17 +declare Var_apps_neq_Abs_apps [symmetric, simp]
    6.18  
    6.19  lemma [simp, THEN not_sym, simp]: "Var n \<degree>\<degree> ss \<noteq> Abs r \<degree> s \<degree>\<degree> ts"
    6.20 -  apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
    6.21 -  done
    6.22 +  by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
    6.23  
    6.24  lemma [simp]:
    6.25    "(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')"
    6.26 -  apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
    6.27 -  done
    6.28 +  by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
    6.29  
    6.30  inductive_cases [elim!]:
    6.31    "Var n \<degree>\<degree> ss : IT"
     7.1 --- a/src/HOL/Lambda/Lambda.thy	Wed Nov 23 22:23:52 2005 +0100
     7.2 +++ b/src/HOL/Lambda/Lambda.thy	Wed Nov 23 22:26:13 2005 +0100
     7.3 @@ -86,21 +86,15 @@
     7.4  
     7.5  lemma rtrancl_beta_Abs [intro!]:
     7.6      "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
     7.7 -  apply (erule rtrancl_induct)
     7.8 -   apply (blast intro: rtrancl_into_rtrancl)+
     7.9 -  done
    7.10 +  by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
    7.11  
    7.12  lemma rtrancl_beta_AppL:
    7.13      "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t"
    7.14 -  apply (erule rtrancl_induct)
    7.15 -   apply (blast intro: rtrancl_into_rtrancl)+
    7.16 -  done
    7.17 +  by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
    7.18  
    7.19  lemma rtrancl_beta_AppR:
    7.20      "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'"
    7.21 -  apply (erule rtrancl_induct)
    7.22 -   apply (blast intro: rtrancl_into_rtrancl)+
    7.23 -  done
    7.24 +  by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
    7.25  
    7.26  lemma rtrancl_beta_App [intro]:
    7.27      "[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
    7.28 @@ -112,72 +106,51 @@
    7.29  subsection {* Substitution-lemmas *}
    7.30  
    7.31  lemma subst_eq [simp]: "(Var k)[u/k] = u"
    7.32 -  apply (simp add: subst_Var)
    7.33 -  done
    7.34 +  by (simp add: subst_Var)
    7.35  
    7.36  lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)"
    7.37 -  apply (simp add: subst_Var)
    7.38 -  done
    7.39 +  by (simp add: subst_Var)
    7.40  
    7.41  lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j"
    7.42 -  apply (simp add: subst_Var)
    7.43 -  done
    7.44 +  by (simp add: subst_Var)
    7.45  
    7.46 -lemma lift_lift [rule_format]:
    7.47 -    "\<forall>i k. i < k + 1 --> lift (lift t i) (Suc k) = lift (lift t k) i"
    7.48 -  apply (induct_tac t)
    7.49 -    apply auto
    7.50 -  done
    7.51 +lemma lift_lift:
    7.52 +    "i < k + 1 \<Longrightarrow> lift (lift t i) (Suc k) = lift (lift t k) i"
    7.53 +  by (induct t fixing: i k) auto
    7.54  
    7.55  lemma lift_subst [simp]:
    7.56 -    "\<forall>i j s. j < i + 1 --> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
    7.57 -  apply (induct_tac t)
    7.58 -    apply (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
    7.59 -  done
    7.60 +    "j < i + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
    7.61 +  by (induct t fixing: i j s)
    7.62 +    (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
    7.63  
    7.64  lemma lift_subst_lt:
    7.65 -    "\<forall>i j s. i < j + 1 --> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
    7.66 -  apply (induct_tac t)
    7.67 -    apply (simp_all add: subst_Var lift_lift)
    7.68 -  done
    7.69 +    "i < j + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
    7.70 +  by (induct t fixing: i j s) (simp_all add: subst_Var lift_lift)
    7.71  
    7.72  lemma subst_lift [simp]:
    7.73 -    "\<forall>k s. (lift t k)[s/k] = t"
    7.74 -  apply (induct_tac t)
    7.75 -    apply simp_all
    7.76 -  done
    7.77 +    "(lift t k)[s/k] = t"
    7.78 +  by (induct t fixing: k s) simp_all
    7.79  
    7.80 -lemma subst_subst [rule_format]:
    7.81 -    "\<forall>i j u v. i < j + 1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
    7.82 -  apply (induct_tac t)
    7.83 -    apply (simp_all
    7.84 -      add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
    7.85 +lemma subst_subst:
    7.86 +    "i < j + 1 \<Longrightarrow> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
    7.87 +  by (induct t fixing: i j u v)
    7.88 +    (simp_all add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
    7.89        split: nat.split)
    7.90 -  done
    7.91  
    7.92  
    7.93  subsection {* Equivalence proof for optimized substitution *}
    7.94  
    7.95 -lemma liftn_0 [simp]: "\<forall>k. liftn 0 t k = t"
    7.96 -  apply (induct_tac t)
    7.97 -    apply (simp_all add: subst_Var)
    7.98 -  done
    7.99 +lemma liftn_0 [simp]: "liftn 0 t k = t"
   7.100 +  by (induct t fixing: k) (simp_all add: subst_Var)
   7.101  
   7.102 -lemma liftn_lift [simp]:
   7.103 -    "\<forall>k. liftn (Suc n) t k = lift (liftn n t k) k"
   7.104 -  apply (induct_tac t)
   7.105 -    apply (simp_all add: subst_Var)
   7.106 -  done
   7.107 +lemma liftn_lift [simp]: "liftn (Suc n) t k = lift (liftn n t k) k"
   7.108 +  by (induct t fixing: k) (simp_all add: subst_Var)
   7.109  
   7.110 -lemma substn_subst_n [simp]:
   7.111 -    "\<forall>n. substn t s n = t[liftn n s 0 / n]"
   7.112 -  apply (induct_tac t)
   7.113 -    apply (simp_all add: subst_Var)
   7.114 -  done
   7.115 +lemma substn_subst_n [simp]: "substn t s n = t[liftn n s 0 / n]"
   7.116 +  by (induct t fixing: n) (simp_all add: subst_Var)
   7.117  
   7.118  theorem substn_subst_0: "substn t s 0 = t[s/0]"
   7.119 -  apply simp
   7.120 -  done
   7.121 +  by simp
   7.122  
   7.123  
   7.124  subsection {* Preservation theorems *}
   7.125 @@ -187,13 +160,11 @@
   7.126  
   7.127  theorem subst_preserves_beta [simp]:
   7.128      "r \<rightarrow>\<^sub>\<beta> s ==> (\<And>t i. r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i])"
   7.129 -  apply (induct set: beta)
   7.130 -     apply (simp_all add: subst_subst [symmetric])
   7.131 -  done
   7.132 +  by (induct set: beta) (simp_all add: subst_subst [symmetric])
   7.133  
   7.134  theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
   7.135 -  apply (erule rtrancl.induct)
   7.136 -  apply (rule rtrancl_refl)
   7.137 +  apply (induct set: rtrancl)
   7.138 +   apply (rule rtrancl_refl)
   7.139    apply (erule rtrancl_into_rtrancl)
   7.140    apply (erule subst_preserves_beta)
   7.141    done
   7.142 @@ -203,23 +174,22 @@
   7.143    by (induct set: beta) auto
   7.144  
   7.145  theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
   7.146 -  apply (erule rtrancl.induct)
   7.147 -  apply (rule rtrancl_refl)
   7.148 +  apply (induct set: rtrancl)
   7.149 +   apply (rule rtrancl_refl)
   7.150    apply (erule rtrancl_into_rtrancl)
   7.151    apply (erule lift_preserves_beta)
   7.152    done
   7.153  
   7.154 -theorem subst_preserves_beta2 [simp]:
   7.155 -    "\<And>r s i. r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
   7.156 -  apply (induct t)
   7.157 +theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
   7.158 +  apply (induct t fixing: r s i)
   7.159      apply (simp add: subst_Var r_into_rtrancl)
   7.160     apply (simp add: rtrancl_beta_App)
   7.161    apply (simp add: rtrancl_beta_Abs)
   7.162    done
   7.163  
   7.164  theorem subst_preserves_beta2': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
   7.165 -  apply (erule rtrancl.induct)
   7.166 -  apply (rule rtrancl_refl)
   7.167 +  apply (induct set: rtrancl)
   7.168 +   apply (rule rtrancl_refl)
   7.169    apply (erule rtrancl_trans)
   7.170    apply (erule subst_preserves_beta2)
   7.171    done
     8.1 --- a/src/HOL/Lambda/ListApplication.thy	Wed Nov 23 22:23:52 2005 +0100
     8.2 +++ b/src/HOL/Lambda/ListApplication.thy	Wed Nov 23 22:26:13 2005 +0100
     8.3 @@ -14,19 +14,14 @@
     8.4    "t \<degree>\<degree> ts" == "foldl (op \<degree>) t ts"
     8.5  
     8.6  lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)"
     8.7 -  apply (induct_tac ts rule: rev_induct)
     8.8 -   apply auto
     8.9 -  done
    8.10 +  by (induct ts rule: rev_induct) auto
    8.11  
    8.12 -lemma Var_eq_apps_conv [iff]:
    8.13 -    "\<And>s. (Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])"
    8.14 -  apply (induct ss)
    8.15 -   apply auto
    8.16 -  done
    8.17 +lemma Var_eq_apps_conv [iff]: "(Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])"
    8.18 +  by (induct ss fixing: s) auto
    8.19  
    8.20  lemma Var_apps_eq_Var_apps_conv [iff]:
    8.21 -    "\<And>ss. (Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)"
    8.22 -  apply (induct rs rule: rev_induct)
    8.23 +    "(Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)"
    8.24 +  apply (induct rs fixing: ss rule: rev_induct)
    8.25     apply simp
    8.26     apply blast
    8.27    apply (induct_tac ss rule: rev_induct)
    8.28 @@ -43,18 +38,14 @@
    8.29  
    8.30  lemma Abs_eq_apps_conv [iff]:
    8.31      "(Abs r = s \<degree>\<degree> ss) = (Abs r = s \<and> ss = [])"
    8.32 -  apply (induct_tac ss rule: rev_induct)
    8.33 -   apply auto
    8.34 -  done
    8.35 +  by (induct ss rule: rev_induct) auto
    8.36  
    8.37  lemma apps_eq_Abs_conv [iff]: "(s \<degree>\<degree> ss = Abs r) = (s = Abs r \<and> ss = [])"
    8.38 -  apply (induct_tac ss rule: rev_induct)
    8.39 -   apply auto
    8.40 -  done
    8.41 +  by (induct ss rule: rev_induct) auto
    8.42  
    8.43  lemma Abs_apps_eq_Abs_apps_conv [iff]:
    8.44 -    "\<And>ss. (Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)"
    8.45 -  apply (induct rs rule: rev_induct)
    8.46 +    "(Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)"
    8.47 +  apply (induct rs fixing: ss rule: rev_induct)
    8.48     apply simp
    8.49     apply blast
    8.50    apply (induct_tac ss rule: rev_induct)
    8.51 @@ -62,14 +53,12 @@
    8.52    done
    8.53  
    8.54  lemma Abs_App_neq_Var_apps [iff]:
    8.55 -    "\<forall>s t. Abs s \<degree> t ~= Var n \<degree>\<degree> ss"
    8.56 -  apply (induct_tac ss rule: rev_induct)
    8.57 -   apply auto
    8.58 -  done
    8.59 +    "Abs s \<degree> t ~= Var n \<degree>\<degree> ss"
    8.60 +  by (induct ss fixing: s t rule: rev_induct) auto
    8.61  
    8.62  lemma Var_apps_neq_Abs_apps [iff]:
    8.63 -    "\<And>ts. Var n \<degree>\<degree> ts ~= Abs r \<degree>\<degree> ss"
    8.64 -  apply (induct ss rule: rev_induct)
    8.65 +    "Var n \<degree>\<degree> ts ~= Abs r \<degree>\<degree> ss"
    8.66 +  apply (induct ss fixing: ts rule: rev_induct)
    8.67     apply simp
    8.68    apply (induct_tac ts rule: rev_induct)
    8.69     apply auto
    8.70 @@ -77,7 +66,7 @@
    8.71  
    8.72  lemma ex_head_tail:
    8.73    "\<exists>ts h. t = h \<degree>\<degree> ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))"
    8.74 -  apply (induct_tac t)
    8.75 +  apply (induct t)
    8.76      apply (rule_tac x = "[]" in exI)
    8.77      apply simp
    8.78     apply clarify
    8.79 @@ -89,21 +78,18 @@
    8.80  
    8.81  lemma size_apps [simp]:
    8.82    "size (r \<degree>\<degree> rs) = size r + foldl (op +) 0 (map size rs) + length rs"
    8.83 -  apply (induct_tac rs rule: rev_induct)
    8.84 -   apply auto
    8.85 -  done
    8.86 +  by (induct rs rule: rev_induct) auto
    8.87  
    8.88  lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k"
    8.89 -  apply simp
    8.90 -  done
    8.91 +  by simp
    8.92  
    8.93  lemma lift_map [simp]:
    8.94 -    "\<And>t. lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts"
    8.95 -  by (induct ts) simp_all
    8.96 +    "lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts"
    8.97 +  by (induct ts fixing: t) simp_all
    8.98  
    8.99  lemma subst_map [simp]:
   8.100 -    "\<And>t. subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts"
   8.101 -  by (induct ts) simp_all
   8.102 +    "subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts"
   8.103 +  by (induct ts fixing: t) simp_all
   8.104  
   8.105  lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])"
   8.106    by simp
   8.107 @@ -111,60 +97,51 @@
   8.108  
   8.109  text {* \medskip A customized induction schema for @{text "\<degree>\<degree>"}. *}
   8.110  
   8.111 -lemma lem [rule_format (no_asm)]:
   8.112 -  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts);
   8.113 -    !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)
   8.114 -  |] ==> \<forall>t. size t = n --> P t"
   8.115 -proof -
   8.116 -  case rule_context
   8.117 -  show ?thesis
   8.118 -   apply (induct_tac n rule: nat_less_induct)
   8.119 -   apply (rule allI)
   8.120 -   apply (cut_tac t = t in ex_head_tail)
   8.121 +lemma lem:
   8.122 +  assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)"
   8.123 +    and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)"
   8.124 +  shows "size t = n \<Longrightarrow> P t"
   8.125 +  apply (induct n fixing: t rule: nat_less_induct)
   8.126 +  apply (cut_tac t = t in ex_head_tail)
   8.127 +  apply clarify
   8.128 +  apply (erule disjE)
   8.129 +   apply clarify
   8.130 +   apply (rule prems)
   8.131     apply clarify
   8.132 -   apply (erule disjE)
   8.133 -    apply clarify
   8.134 -    apply (rule prems)
   8.135 -    apply clarify
   8.136 -    apply (erule allE, erule impE)
   8.137 -      prefer 2
   8.138 -      apply (erule allE, erule mp, rule refl)
   8.139 -     apply simp
   8.140 -     apply (rule lem0)
   8.141 -      apply force
   8.142 -     apply (rule elem_le_sum)
   8.143 -     apply force
   8.144 -    apply clarify
   8.145 -    apply (rule prems)
   8.146 -     apply (erule allE, erule impE)
   8.147 -      prefer 2
   8.148 -      apply (erule allE, erule mp, rule refl)
   8.149 -     apply simp
   8.150 -    apply clarify
   8.151 -    apply (erule allE, erule impE)
   8.152 -     prefer 2
   8.153 -     apply (erule allE, erule mp, rule refl)
   8.154 -    apply simp
   8.155 -    apply (rule le_imp_less_Suc)
   8.156 -    apply (rule trans_le_add1)
   8.157 -    apply (rule trans_le_add2)
   8.158 -    apply (rule elem_le_sum)
   8.159 +   apply (erule allE, erule impE)
   8.160 +    prefer 2
   8.161 +    apply (erule allE, erule mp, rule refl)
   8.162 +   apply simp
   8.163 +   apply (rule lem0)
   8.164      apply force
   8.165 -    done
   8.166 -qed
   8.167 +   apply (rule elem_le_sum)
   8.168 +   apply force
   8.169 +  apply clarify
   8.170 +  apply (rule prems)
   8.171 +   apply (erule allE, erule impE)
   8.172 +    prefer 2
   8.173 +    apply (erule allE, erule mp, rule refl)
   8.174 +   apply simp
   8.175 +  apply clarify
   8.176 +  apply (erule allE, erule impE)
   8.177 +   prefer 2
   8.178 +   apply (erule allE, erule mp, rule refl)
   8.179 +  apply simp
   8.180 +  apply (rule le_imp_less_Suc)
   8.181 +  apply (rule trans_le_add1)
   8.182 +  apply (rule trans_le_add2)
   8.183 +  apply (rule elem_le_sum)
   8.184 +  apply force
   8.185 +  done
   8.186  
   8.187  theorem Apps_dB_induct:
   8.188 -  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts);
   8.189 -    !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)
   8.190 -  |] ==> P t"
   8.191 -proof -
   8.192 -  case rule_context
   8.193 -  show ?thesis
   8.194 -    apply (rule_tac t = t in lem)
   8.195 -      prefer 3
   8.196 -      apply (rule refl)
   8.197 -     apply (assumption | rule prems)+
   8.198 -    done
   8.199 -qed
   8.200 +  assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)"
   8.201 +    and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)"
   8.202 +  shows "P t"
   8.203 +  apply (rule_tac t = t in lem)
   8.204 +    prefer 3
   8.205 +    apply (rule refl)
   8.206 +   apply (assumption | rule prems)+
   8.207 +  done
   8.208  
   8.209  end
     9.1 --- a/src/HOL/Lambda/ListBeta.thy	Wed Nov 23 22:23:52 2005 +0100
     9.2 +++ b/src/HOL/Lambda/ListBeta.thy	Wed Nov 23 22:26:13 2005 +0100
     9.3 @@ -18,8 +18,8 @@
     9.4    "rs => ss" == "(rs, ss) : step1 beta"
     9.5  
     9.6  lemma head_Var_reduction_aux:
     9.7 -  "v -> v' ==> \<forall>rs. v = Var n \<degree>\<degree> rs --> (\<exists>ss. rs => ss \<and> v' = Var n \<degree>\<degree> ss)"
     9.8 -  apply (erule beta.induct)
     9.9 +  "v -> v' ==> (\<forall>rs. v = Var n \<degree>\<degree> rs --> (\<exists>ss. rs => ss \<and> v' = Var n \<degree>\<degree> ss))"
    9.10 +  apply (induct set: beta)
    9.11       apply simp
    9.12      apply (rule allI)
    9.13      apply (rule_tac xs = rs in rev_exhaust)
    9.14 @@ -33,16 +33,14 @@
    9.15  
    9.16  lemma head_Var_reduction:
    9.17    "Var n \<degree>\<degree> rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss)"
    9.18 -  apply (drule head_Var_reduction_aux)
    9.19 -  apply blast
    9.20 -  done
    9.21 +  by (drule head_Var_reduction_aux) blast
    9.22  
    9.23  lemma apps_betasE_aux:
    9.24    "u -> u' ==> \<forall>r rs. u = r \<degree>\<degree> rs -->
    9.25      ((\<exists>r'. r -> r' \<and> u' = r' \<degree>\<degree> rs) \<or>
    9.26       (\<exists>rs'. rs => rs' \<and> u' = r \<degree>\<degree> rs') \<or>
    9.27       (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] \<degree>\<degree> ts))"
    9.28 -  apply (erule beta.induct)
    9.29 +  apply (induct set: beta)
    9.30       apply (clarify del: disjCI)
    9.31       apply (case_tac r)
    9.32         apply simp
    9.33 @@ -70,38 +68,31 @@
    9.34    done
    9.35  
    9.36  lemma apps_betasE [elim!]:
    9.37 -  "[| r \<degree>\<degree> rs -> s; !!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R;
    9.38 -    !!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R;
    9.39 -    !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R |]
    9.40 -  ==> R"
    9.41 -proof -
    9.42 -  assume major: "r \<degree>\<degree> rs -> s"
    9.43 -  case rule_context
    9.44 -  show ?thesis
    9.45 -    apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
    9.46 -    apply (assumption | rule refl | erule prems exE conjE impE disjE)+
    9.47 -    done
    9.48 -qed
    9.49 +  assumes major: "r \<degree>\<degree> rs -> s"
    9.50 +    and "!!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R"
    9.51 +    and "!!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R"
    9.52 +    and "!!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R"
    9.53 +  shows R
    9.54 +  apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
    9.55 +  apply (assumption | rule refl | erule prems exE conjE impE disjE)+
    9.56 +  done
    9.57  
    9.58  lemma apps_preserves_beta [simp]:
    9.59      "r -> s ==> r \<degree>\<degree> ss -> s \<degree>\<degree> ss"
    9.60 -  apply (induct_tac ss rule: rev_induct)
    9.61 -  apply auto
    9.62 -  done
    9.63 +  by (induct ss rule: rev_induct) auto
    9.64  
    9.65  lemma apps_preserves_beta2 [simp]:
    9.66      "r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss"
    9.67 -  apply (erule rtrancl_induct)
    9.68 +  apply (induct set: rtrancl)
    9.69     apply blast
    9.70    apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
    9.71    done
    9.72  
    9.73 -lemma apps_preserves_betas [rule_format, simp]:
    9.74 -    "\<forall>ss. rs => ss --> r \<degree>\<degree> rs -> r \<degree>\<degree> ss"
    9.75 -  apply (induct_tac rs rule: rev_induct)
    9.76 +lemma apps_preserves_betas [simp]:
    9.77 +    "rs => ss \<Longrightarrow> r \<degree>\<degree> rs -> r \<degree>\<degree> ss"
    9.78 +  apply (induct rs fixing: ss rule: rev_induct)
    9.79     apply simp
    9.80    apply simp
    9.81 -  apply clarify
    9.82    apply (rule_tac xs = ss in rev_exhaust)
    9.83     apply simp
    9.84    apply simp
    10.1 --- a/src/HOL/Lambda/ListOrder.thy	Wed Nov 23 22:23:52 2005 +0100
    10.2 +++ b/src/HOL/Lambda/ListOrder.thy	Wed Nov 23 22:26:13 2005 +0100
    10.3 @@ -87,18 +87,17 @@
    10.4    apply blast
    10.5    done
    10.6  
    10.7 -lemma Cons_acc_step1I [rule_format, intro!]:
    10.8 -    "x \<in> acc r ==> \<forall>xs. xs \<in> acc (step1 r) --> x # xs \<in> acc (step1 r)"
    10.9 -  apply (erule acc_induct)
   10.10 +lemma Cons_acc_step1I [intro!]:
   10.11 +    "x \<in> acc r ==> (!!xs. xs \<in> acc (step1 r) \<Longrightarrow> x # xs \<in> acc (step1 r))"
   10.12 +  apply (induct set: acc)
   10.13    apply (erule thin_rl)
   10.14 -  apply clarify
   10.15    apply (erule acc_induct)
   10.16    apply (rule accI)
   10.17    apply blast
   10.18    done
   10.19  
   10.20  lemma lists_accD: "xs \<in> lists (acc r) ==> xs \<in> acc (step1 r)"
   10.21 -  apply (erule lists.induct)
   10.22 +  apply (induct set: lists)
   10.23     apply (rule accI)
   10.24     apply simp
   10.25    apply (rule accI)
   10.26 @@ -114,7 +113,7 @@
   10.27    done
   10.28  
   10.29  lemma lists_accI: "xs \<in> acc (step1 r) ==> xs \<in> lists (acc r)"
   10.30 -  apply (erule acc_induct)
   10.31 +  apply (induct set: acc)
   10.32    apply clarify
   10.33    apply (rule accI)
   10.34    apply (drule ex_step1I, assumption)
    11.1 --- a/src/HOL/Lambda/ParRed.thy	Wed Nov 23 22:23:52 2005 +0100
    11.2 +++ b/src/HOL/Lambda/ParRed.thy	Wed Nov 23 22:26:13 2005 +0100
    11.3 @@ -43,13 +43,10 @@
    11.4  
    11.5  lemma par_beta_varL [simp]:
    11.6      "(Var n => t) = (t = Var n)"
    11.7 -  apply blast
    11.8 -  done
    11.9 +  by blast
   11.10  
   11.11  lemma par_beta_refl [simp]: "t => t"  (* par_beta_refl [intro!] causes search to blow up *)
   11.12 -  apply (induct_tac t)
   11.13 -    apply simp_all
   11.14 -  done
   11.15 +  by (induct t) simp_all
   11.16  
   11.17  lemma beta_subset_par_beta: "beta <= par_beta"
   11.18    apply (rule subsetI)
   11.19 @@ -70,17 +67,14 @@
   11.20  
   11.21  subsection {* Misc properties of par-beta *}
   11.22  
   11.23 -lemma par_beta_lift [rule_format, simp]:
   11.24 -    "\<forall>t' n. t => t' --> lift t n => lift t' n"
   11.25 -  apply (induct_tac t)
   11.26 -    apply fastsimp+
   11.27 -  done
   11.28 +lemma par_beta_lift [simp]:
   11.29 +    "t => t' \<Longrightarrow> lift t n => lift t' n"
   11.30 +  by (induct t fixing: t' n) fastsimp+
   11.31  
   11.32 -lemma par_beta_subst [rule_format]:
   11.33 -    "\<forall>s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"
   11.34 -  apply (induct_tac t)
   11.35 +lemma par_beta_subst:
   11.36 +    "s => s' \<Longrightarrow> t => t' \<Longrightarrow> t[s/n] => t'[s'/n]"
   11.37 +  apply (induct t fixing: s s' t' n)
   11.38      apply (simp add: subst_Var)
   11.39 -   apply (intro strip)
   11.40     apply (erule par_beta_cases)
   11.41      apply simp
   11.42     apply (simp add: subst_subst [symmetric])
   11.43 @@ -110,9 +104,8 @@
   11.44    "cd (Abs u \<degree> t) = (cd u)[cd t/0]"
   11.45    "cd (Abs s) = Abs (cd s)"
   11.46  
   11.47 -lemma par_beta_cd [rule_format]:
   11.48 -    "\<forall>t. s => t --> t => cd s"
   11.49 -  apply (induct_tac s rule: cd.induct)
   11.50 +lemma par_beta_cd: "s => t \<Longrightarrow> t => cd s"
   11.51 +  apply (induct s fixing: t rule: cd.induct)
   11.52        apply auto
   11.53    apply (fast intro!: par_beta_subst)
   11.54    done
    12.1 --- a/src/HOL/Lambda/Type.thy	Wed Nov 23 22:23:52 2005 +0100
    12.2 +++ b/src/HOL/Lambda/Type.thy	Wed Nov 23 22:26:13 2005 +0100
    12.3 @@ -94,8 +94,8 @@
    12.4  subsection {* Lists of types *}
    12.5  
    12.6  lemma lists_typings:
    12.7 -    "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
    12.8 -  apply (induct ts)
    12.9 +    "e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
   12.10 +  apply (induct ts fixing: Ts)
   12.11     apply (case_tac Ts)
   12.12       apply simp
   12.13       apply (rule lists.Nil)
   12.14 @@ -108,16 +108,16 @@
   12.15    apply blast
   12.16    done
   12.17  
   12.18 -lemma types_snoc: "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<tturnstile> ts @ [t] : Ts @ [T]"
   12.19 -  apply (induct ts)
   12.20 +lemma types_snoc: "e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<tturnstile> ts @ [t] : Ts @ [T]"
   12.21 +  apply (induct ts fixing: Ts)
   12.22    apply simp
   12.23    apply (case_tac Ts)
   12.24    apply simp+
   12.25    done
   12.26  
   12.27 -lemma types_snoc_eq: "\<And>Ts. e \<tturnstile> ts @ [t] : Ts @ [T] =
   12.28 +lemma types_snoc_eq: "e \<tturnstile> ts @ [t] : Ts @ [T] =
   12.29    (e \<tturnstile> ts : Ts \<and> e \<turnstile> t : T)"
   12.30 -  apply (induct ts)
   12.31 +  apply (induct ts fixing: Ts)
   12.32    apply (case_tac Ts)
   12.33    apply simp+
   12.34    apply (case_tac Ts)
   12.35 @@ -156,8 +156,8 @@
   12.36  subsection {* n-ary function types *}
   12.37  
   12.38  lemma list_app_typeD:
   12.39 -    "\<And>t T. e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
   12.40 -  apply (induct ts)
   12.41 +    "e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
   12.42 +  apply (induct ts fixing: t T)
   12.43     apply simp
   12.44    apply atomize
   12.45    apply simp
   12.46 @@ -176,8 +176,8 @@
   12.47    by (insert list_app_typeD) fast
   12.48  
   12.49  lemma list_app_typeI:
   12.50 -    "\<And>t T Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T"
   12.51 -  apply (induct ts)
   12.52 +    "e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T"
   12.53 +  apply (induct ts fixing: t T Ts)
   12.54     apply simp
   12.55    apply atomize
   12.56    apply (case_tac Ts)
   12.57 @@ -201,8 +201,8 @@
   12.58  *}
   12.59  
   12.60  theorem var_app_type_eq:
   12.61 -  "\<And>T U. e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U"
   12.62 -  apply (induct ts rule: rev_induct)
   12.63 +  "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U"
   12.64 +  apply (induct ts fixing: T U rule: rev_induct)
   12.65    apply simp
   12.66    apply (ind_cases "e \<turnstile> Var i : T")
   12.67    apply (ind_cases "e \<turnstile> Var i : T")
   12.68 @@ -220,9 +220,9 @@
   12.69    apply simp
   12.70    done
   12.71  
   12.72 -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>
   12.73 +lemma var_app_types: "e \<turnstile> Var i \<degree>\<degree> ts \<degree>\<degree> us : T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow>
   12.74    e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> \<exists>Us. U = Us \<Rrightarrow> T \<and> e \<tturnstile> us : Us"
   12.75 -  apply (induct us)
   12.76 +  apply (induct us fixing: ts Ts U)
   12.77    apply simp
   12.78    apply (erule var_app_type_eq)
   12.79    apply assumption
   12.80 @@ -292,8 +292,8 @@
   12.81    by (induct set: typing) auto
   12.82  
   12.83  lemma lift_types:
   12.84 -  "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
   12.85 -  apply (induct ts)
   12.86 +  "e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
   12.87 +  apply (induct ts fixing: Ts)
   12.88     apply simp
   12.89    apply (case_tac Ts)
   12.90     apply auto
   12.91 @@ -311,9 +311,9 @@
   12.92    done
   12.93  
   12.94  lemma substs_lemma:
   12.95 -  "\<And>Ts. e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow>
   12.96 +  "e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow>
   12.97       e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts"
   12.98 -  apply (induct ts)
   12.99 +  apply (induct ts fixing: Ts)
  12.100     apply (case_tac Ts)
  12.101      apply simp
  12.102     apply simp
  12.103 @@ -352,18 +352,16 @@
  12.104  subsection {* Alternative induction rule for types *}
  12.105  
  12.106  lemma type_induct [induct type]:
  12.107 +  assumes
  12.108    "(\<And>T. (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T1) \<Longrightarrow>
  12.109 -   (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T2) \<Longrightarrow> P T) \<Longrightarrow> P T"
  12.110 -proof -
  12.111 -  case rule_context
  12.112 -  show ?thesis
  12.113 -  proof (induct T)
  12.114 -    case Atom
  12.115 -    show ?case by (rule rule_context) simp_all
  12.116 -  next
  12.117 -    case Fun
  12.118 -    show ?case  by (rule rule_context) (insert Fun, simp_all)
  12.119 -  qed
  12.120 +    (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T2) \<Longrightarrow> P T)"
  12.121 +  shows "P T"
  12.122 +proof (induct T)
  12.123 +  case Atom
  12.124 +  show ?case by (rule prems) simp_all
  12.125 +next
  12.126 +  case Fun
  12.127 +  show ?case  by (rule prems) (insert Fun, simp_all)
  12.128  qed
  12.129  
  12.130  end
    13.1 --- a/src/HOL/Lambda/WeakNorm.thy	Wed Nov 23 22:23:52 2005 +0100
    13.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Wed Nov 23 22:26:13 2005 +0100
    13.3 @@ -52,14 +52,14 @@
    13.4    done
    13.5  
    13.6  lemma listall_conj1: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall P xs"
    13.7 -  by (induct xs) simp+
    13.8 +  by (induct xs) simp_all
    13.9  
   13.10  lemma listall_conj2: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall Q xs"
   13.11 -  by (induct xs) simp+
   13.12 +  by (induct xs) simp_all
   13.13  
   13.14  lemma listall_app: "listall P (xs @ ys) = (listall P xs \<and> listall P ys)"
   13.15    apply (induct xs)
   13.16 -  apply (rule iffI, simp, simp)
   13.17 +   apply (rule iffI, simp, simp)
   13.18    apply (rule iffI, simp, simp)
   13.19    done
   13.20  
    14.1 --- a/src/HOL/Library/Accessible_Part.thy	Wed Nov 23 22:23:52 2005 +0100
    14.2 +++ b/src/HOL/Library/Accessible_Part.thy	Wed Nov 23 22:26:13 2005 +0100
    14.3 @@ -32,19 +32,15 @@
    14.4  subsection {* Induction rules *}
    14.5  
    14.6  theorem acc_induct:
    14.7 -  "a \<in> acc r ==>
    14.8 -    (!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x) ==> P a"
    14.9 -proof -
   14.10 -  assume major: "a \<in> acc r"
   14.11 -  assume hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
   14.12 -  show ?thesis
   14.13 -    apply (rule major [THEN acc.induct])
   14.14 -    apply (rule hyp)
   14.15 -     apply (rule accI)
   14.16 -     apply fast
   14.17 -    apply fast
   14.18 -    done
   14.19 -qed
   14.20 +  assumes major: "a \<in> acc r"
   14.21 +  assumes hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
   14.22 +  shows "P a"
   14.23 +  apply (rule major [THEN acc.induct])
   14.24 +  apply (rule hyp)
   14.25 +   apply (rule accI)
   14.26 +   apply fast
   14.27 +  apply fast
   14.28 +  done
   14.29  
   14.30  theorems acc_induct_rule = acc_induct [rule_format, induct set: acc]
   14.31