Updated IMP to use new induction method
authornipkow
Tue Sep 20 05:48:23 2011 +0200 (2011-09-20)
changeset 45015fdac1e9880eb
parent 45014 0e847655b2d8
child 45016 a5d43ffc95eb
Updated IMP to use new induction method
src/HOL/IMP/AExp.thy
src/HOL/IMP/ASM.thy
src/HOL/IMP/AbsInt0.thy
src/HOL/IMP/AbsInt0_fun.thy
src/HOL/IMP/AbsInt1.thy
src/HOL/IMP/AbsInt2.thy
src/HOL/IMP/BExp.thy
src/HOL/IMP/Big_Step.thy
src/HOL/IMP/Comp_Rev.thy
src/HOL/IMP/Compiler.thy
src/HOL/IMP/Def_Ass_Sound_Big.thy
src/HOL/IMP/Def_Ass_Sound_Small.thy
src/HOL/IMP/Denotation.thy
src/HOL/IMP/Fold.thy
src/HOL/IMP/HoareT.thy
src/HOL/IMP/Hoare_Examples.thy
src/HOL/IMP/Hoare_Sound_Complete.thy
src/HOL/IMP/Live.thy
src/HOL/IMP/Poly_Types.thy
src/HOL/IMP/Sec_Typing.thy
src/HOL/IMP/Sec_TypingT.thy
src/HOL/IMP/Sem_Equiv.thy
src/HOL/IMP/Small_Step.thy
src/HOL/IMP/Star.thy
src/HOL/IMP/Types.thy
src/HOL/IMP/VC.thy
src/HOL/IMP/Vars.thy
     1.1 --- a/src/HOL/IMP/AExp.thy	Tue Sep 20 05:47:11 2011 +0200
     1.2 +++ b/src/HOL/IMP/AExp.thy	Tue Sep 20 05:48:23 2011 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4  
     1.5  theorem aval_asimp_const[simp]:
     1.6    "aval (asimp_const a) s = aval a s"
     1.7 -apply(induct a)
     1.8 +apply(induction a)
     1.9  apply (auto split: aexp.split)
    1.10  done
    1.11  
    1.12 @@ -77,7 +77,7 @@
    1.13  
    1.14  lemma aval_plus[simp]:
    1.15    "aval (plus a1 a2) s = aval a1 s + aval a2 s"
    1.16 -apply(induct a1 a2 rule: plus.induct)
    1.17 +apply(induction a1 a2 rule: plus.induct)
    1.18  apply simp_all (* just for a change from auto *)
    1.19  done
    1.20  
    1.21 @@ -94,7 +94,7 @@
    1.22  
    1.23  theorem aval_asimp[simp]:
    1.24    "aval (asimp a) s = aval a s"
    1.25 -apply(induct a)
    1.26 +apply(induction a)
    1.27  apply simp_all
    1.28  done
    1.29  
     2.1 --- a/src/HOL/IMP/ASM.thy	Tue Sep 20 05:47:11 2011 +0200
     2.2 +++ b/src/HOL/IMP/ASM.thy	Tue Sep 20 05:48:23 2011 +0200
     2.3 @@ -29,7 +29,7 @@
     2.4  
     2.5  lemma aexec_append[simp]:
     2.6    "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
     2.7 -apply(induct is1 arbitrary: stk)
     2.8 +apply(induction is1 arbitrary: stk)
     2.9  apply (auto)
    2.10  done
    2.11  
    2.12 @@ -44,7 +44,7 @@
    2.13  value "acomp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
    2.14  
    2.15  theorem aexec_acomp[simp]: "aexec (acomp a) s stk = aval a s # stk"
    2.16 -apply(induct a arbitrary: stk)
    2.17 +apply(induction a arbitrary: stk)
    2.18  apply (auto)
    2.19  done
    2.20  
     3.1 --- a/src/HOL/IMP/AbsInt0.thy	Tue Sep 20 05:47:11 2011 +0200
     3.2 +++ b/src/HOL/IMP/AbsInt0.thy	Tue Sep 20 05:48:23 2011 +0200
     3.3 @@ -38,7 +38,7 @@
     3.4  "AI (WHILE b DO c) S = pfp (AI c) S"
     3.5  
     3.6  lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
     3.7 -proof(induct c arbitrary: s t S0)
     3.8 +proof(induction c arbitrary: s t S0)
     3.9    case SKIP thus ?case by fastforce
    3.10  next
    3.11    case Assign thus ?case
    3.12 @@ -52,10 +52,10 @@
    3.13    case (While b c)
    3.14    let ?P = "pfp (AI c) S0"
    3.15    { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
    3.16 -    proof(induct "WHILE b DO c" s t rule: big_step_induct)
    3.17 +    proof(induction "WHILE b DO c" s t rule: big_step_induct)
    3.18        case WhileFalse thus ?case by simp
    3.19      next
    3.20 -      case WhileTrue thus ?case using While.hyps pfp astate_in_rep_le by metis
    3.21 +      case WhileTrue thus ?case using While.IH pfp astate_in_rep_le by metis
    3.22      qed
    3.23    }
    3.24    with astate_in_rep_le[OF `s <: S0` above]
     4.1 --- a/src/HOL/IMP/AbsInt0_fun.thy	Tue Sep 20 05:47:11 2011 +0200
     4.2 +++ b/src/HOL/IMP/AbsInt0_fun.thy	Tue Sep 20 05:48:23 2011 +0200
     4.3 @@ -36,7 +36,7 @@
     4.4  "iter (Suc n) f x = (if f x \<sqsubseteq> x then x else iter n f (f x))"
     4.5  
     4.6  lemma iter_pfp: "f(iter n f x) \<sqsubseteq> iter n f x"
     4.7 -apply (induct n arbitrary: x)
     4.8 +apply (induction n arbitrary: x)
     4.9   apply (simp)
    4.10  apply (simp)
    4.11  done
    4.12 @@ -52,7 +52,7 @@
    4.13  point does @{const iter} yield? *}
    4.14  
    4.15  lemma iter_funpow: "iter n f x \<noteq> Top \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
    4.16 -apply(induct n arbitrary: x)
    4.17 +apply(induction n arbitrary: x)
    4.18   apply simp
    4.19  apply (auto)
    4.20   apply(metis funpow.simps(1) id_def)
    4.21 @@ -69,7 +69,7 @@
    4.22      using iter_funpow[OF `iter n f x0 \<noteq> Top`] by blast
    4.23    moreover
    4.24    { fix n have "(f^^n) x0 \<sqsubseteq> p"
    4.25 -    proof(induct n)
    4.26 +    proof(induction n)
    4.27        case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
    4.28      next
    4.29        case (Suc n) thus ?case
    4.30 @@ -155,7 +155,7 @@
    4.31  "AI (WHILE b DO c) S = pfp (AI c) S"
    4.32  
    4.33  lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
    4.34 -proof(induct c arbitrary: s t S0)
    4.35 +proof(induction c arbitrary: s t S0)
    4.36    case SKIP thus ?case by fastforce
    4.37  next
    4.38    case Assign thus ?case by (auto simp: aval'_sound)
    4.39 @@ -167,10 +167,10 @@
    4.40    case (While b c)
    4.41    let ?P = "pfp (AI c) S0"
    4.42    { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
    4.43 -    proof(induct "WHILE b DO c" s t rule: big_step_induct)
    4.44 +    proof(induction "WHILE b DO c" s t rule: big_step_induct)
    4.45        case WhileFalse thus ?case by simp
    4.46      next
    4.47 -      case WhileTrue thus ?case by(metis While.hyps pfp fun_in_rep_le)
    4.48 +      case WhileTrue thus ?case by(metis While.IH pfp fun_in_rep_le)
    4.49      qed
    4.50    }
    4.51    with fun_in_rep_le[OF `s <: S0` above]
     5.1 --- a/src/HOL/IMP/AbsInt1.thy	Tue Sep 20 05:47:11 2011 +0200
     5.2 +++ b/src/HOL/IMP/AbsInt1.thy	Tue Sep 20 05:48:23 2011 +0200
     5.3 @@ -141,7 +141,7 @@
     5.4     in afilter e1 res1 (afilter e2 res2 S))"
     5.5  
     5.6  lemma afilter_sound: "s <:: S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:: afilter e a S"
     5.7 -proof(induct e arbitrary: a S)
     5.8 +proof(induction e arbitrary: a S)
     5.9    case N thus ?case by simp
    5.10  next
    5.11    case (V x)
    5.12 @@ -158,7 +158,7 @@
    5.13  qed
    5.14  
    5.15  lemma bfilter_sound: "s <:: S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:: bfilter b bv S"
    5.16 -proof(induct b arbitrary: S bv)
    5.17 +proof(induction b arbitrary: S bv)
    5.18    case B thus ?case by simp
    5.19  next
    5.20    case (Not b) thus ?case by simp
    5.21 @@ -181,7 +181,7 @@
    5.22    bfilter b False (pfp (\<lambda>S. AI c (bfilter b True S)) S)"
    5.23  
    5.24  lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S"
    5.25 -proof(induct c arbitrary: s t S)
    5.26 +proof(induction c arbitrary: s t S)
    5.27    case SKIP thus ?case by fastforce
    5.28  next
    5.29    case Assign thus ?case
    5.30 @@ -196,12 +196,12 @@
    5.31    { fix s t
    5.32      have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <:: ?P \<Longrightarrow>
    5.33            t <:: bfilter b False ?P"
    5.34 -    proof(induct "WHILE b DO c" s t rule: big_step_induct)
    5.35 +    proof(induction "WHILE b DO c" s t rule: big_step_induct)
    5.36        case WhileFalse thus ?case by(metis bfilter_sound)
    5.37      next
    5.38        case WhileTrue show ?case
    5.39          by(rule WhileTrue, rule in_rep_up_trans[OF _ pfp],
    5.40 -           rule While.hyps[OF WhileTrue(2)],
    5.41 +           rule While.IH[OF WhileTrue(2)],
    5.42             rule bfilter_sound[OF WhileTrue.prems], simp add: WhileTrue(1))
    5.43      qed
    5.44    }
     6.1 --- a/src/HOL/IMP/AbsInt2.thy	Tue Sep 20 05:47:11 2011 +0200
     6.2 +++ b/src/HOL/IMP/AbsInt2.thy	Tue Sep 20 05:48:23 2011 +0200
     6.3 @@ -24,7 +24,7 @@
     6.4    (let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla> fx))"
     6.5  
     6.6  lemma iter_up_pfp: "f(iter_up f n x) \<sqsubseteq> iter_up f n x"
     6.7 -apply (induct n arbitrary: x)
     6.8 +apply (induction n arbitrary: x)
     6.9   apply (simp)
    6.10  apply (simp add: Let_def)
    6.11  done
    6.12 @@ -35,7 +35,7 @@
    6.13    (let y = x \<triangle> f x in if f y \<sqsubseteq> y then iter_down f n y else x)"
    6.14  
    6.15  lemma iter_down_pfp: "f x \<sqsubseteq> x \<Longrightarrow> f(iter_down f n x) \<sqsubseteq> iter_down f n x"
    6.16 -apply (induct n arbitrary: x)
    6.17 +apply (induction n arbitrary: x)
    6.18   apply (simp)
    6.19  apply (simp add: Let_def)
    6.20  done
     7.1 --- a/src/HOL/IMP/BExp.thy	Tue Sep 20 05:47:11 2011 +0200
     7.2 +++ b/src/HOL/IMP/BExp.thy	Tue Sep 20 05:48:23 2011 +0200
     7.3 @@ -23,7 +23,7 @@
     7.4  "less a1 a2 = Less a1 a2"
     7.5  
     7.6  lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
     7.7 -apply(induct a1 a2 rule: less.induct)
     7.8 +apply(induction a1 a2 rule: less.induct)
     7.9  apply simp_all
    7.10  done
    7.11  
    7.12 @@ -35,7 +35,7 @@
    7.13  "and b1 b2 = And b1 b2"
    7.14  
    7.15  lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)"
    7.16 -apply(induct b1 b2 rule: and.induct)
    7.17 +apply(induction b1 b2 rule: and.induct)
    7.18  apply simp_all
    7.19  done
    7.20  
    7.21 @@ -45,7 +45,7 @@
    7.22  "not b = Not b"
    7.23  
    7.24  lemma bval_not[simp]: "bval (not b) s = (~bval b s)"
    7.25 -apply(induct b rule: not.induct)
    7.26 +apply(induction b rule: not.induct)
    7.27  apply simp_all
    7.28  done
    7.29  
    7.30 @@ -62,7 +62,7 @@
    7.31  value "bsimp (And (Less (N 1) (N 0)) (B True))"
    7.32  
    7.33  theorem "bval (bsimp b) s = bval b s"
    7.34 -apply(induct b)
    7.35 +apply(induction b)
    7.36  apply simp_all
    7.37  done
    7.38  
     8.1 --- a/src/HOL/IMP/Big_Step.thy	Tue Sep 20 05:47:11 2011 +0200
     8.2 +++ b/src/HOL/IMP/Big_Step.thy	Tue Sep 20 05:48:23 2011 +0200
     8.3 @@ -215,7 +215,7 @@
     8.4  
     8.5  text {* This proof is automatic. *}
     8.6  theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
     8.7 -apply (induct arbitrary: u rule: big_step.induct)
     8.8 +apply (induction arbitrary: u rule: big_step.induct)
     8.9  apply blast+
    8.10  done
    8.11  
    8.12 @@ -225,7 +225,7 @@
    8.13  *}
    8.14  theorem
    8.15    "(c,s) \<Rightarrow> t  \<Longrightarrow>  (c,s) \<Rightarrow> t'  \<Longrightarrow>  t' = t"
    8.16 -proof (induct arbitrary: t' rule: big_step.induct)
    8.17 +proof (induction arbitrary: t' rule: big_step.induct)
    8.18    -- "the only interesting case, @{text WhileTrue}:"
    8.19    fix b c s s1 t t'
    8.20    -- "The assumptions of the rule:"
     9.1 --- a/src/HOL/IMP/Comp_Rev.thy	Tue Sep 20 05:47:11 2011 +0200
     9.2 +++ b/src/HOL/IMP/Comp_Rev.thy	Tue Sep 20 05:48:23 2011 +0200
     9.3 @@ -196,13 +196,13 @@
     9.4    "0 \<le> i \<Longrightarrow>
     9.5    succs (bcomp b c i) n \<subseteq> {n .. n + isize (bcomp b c i)}
     9.6                             \<union> {n + i + isize (bcomp b c i)}" 
     9.7 -proof (induct b arbitrary: c i n)
     9.8 +proof (induction b arbitrary: c i n)
     9.9    case (And b1 b2)
    9.10    from And.prems
    9.11    show ?case 
    9.12      by (cases c)
    9.13 -       (auto dest: And.hyps(1) [THEN subsetD, rotated] 
    9.14 -                   And.hyps(2) [THEN subsetD, rotated])
    9.15 +       (auto dest: And.IH(1) [THEN subsetD, rotated] 
    9.16 +                   And.IH(2) [THEN subsetD, rotated])
    9.17  qed auto
    9.18  
    9.19  lemmas bcomp_succsD [dest!] = bcomp_succs [THEN subsetD, rotated]
    9.20 @@ -219,7 +219,7 @@
    9.21  
    9.22  lemma ccomp_succs:
    9.23    "succs (ccomp c) n \<subseteq> {n..n + isize (ccomp c)}"
    9.24 -proof (induct c arbitrary: n)
    9.25 +proof (induction c arbitrary: n)
    9.26    case SKIP thus ?case by simp
    9.27  next
    9.28    case Assign thus ?case by simp
    9.29 @@ -227,16 +227,16 @@
    9.30    case (Semi c1 c2)
    9.31    from Semi.prems
    9.32    show ?case 
    9.33 -    by (fastforce dest: Semi.hyps [THEN subsetD])
    9.34 +    by (fastforce dest: Semi.IH [THEN subsetD])
    9.35  next
    9.36    case (If b c1 c2)
    9.37    from If.prems
    9.38    show ?case
    9.39 -    by (auto dest!: If.hyps [THEN subsetD] simp: isuccs_def succs_Cons)
    9.40 +    by (auto dest!: If.IH [THEN subsetD] simp: isuccs_def succs_Cons)
    9.41  next
    9.42    case (While b c)
    9.43    from While.prems
    9.44 -  show ?case by (auto dest!: While.hyps [THEN subsetD])
    9.45 +  show ?case by (auto dest!: While.IH [THEN subsetD])
    9.46  qed
    9.47  
    9.48  lemma ccomp_exits:
    9.49 @@ -264,7 +264,7 @@
    9.50                     i' \<in> exits c \<and> 
    9.51                     P @ c @ P' \<turnstile> (isize P + i', s'') \<rightarrow>^m (j, s') \<and>
    9.52                     n = k + m" 
    9.53 -using assms proof (induct n arbitrary: i j s)
    9.54 +using assms proof (induction n arbitrary: i j s)
    9.55    case 0
    9.56    thus ?case by simp
    9.57  next
    9.58 @@ -289,7 +289,7 @@
    9.59    { assume "j0 \<in> {0 ..< isize c}"
    9.60      with j0 j rest c
    9.61      have ?case
    9.62 -      by (fastforce dest!: Suc.hyps intro!: exec_Suc)
    9.63 +      by (fastforce dest!: Suc.IH intro!: exec_Suc)
    9.64    } moreover {
    9.65      assume "j0 \<notin> {0 ..< isize c}"
    9.66      moreover
    9.67 @@ -338,7 +338,7 @@
    9.68    assumes "P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk')"
    9.69            "isize P \<le> i" "exits P' \<subseteq> {0..}"
    9.70    shows "P' \<turnstile> (i - isize P, s, stk) \<rightarrow>^k (n - isize P, s', stk')"
    9.71 -using assms proof (induct k arbitrary: i s stk)
    9.72 +using assms proof (induction k arbitrary: i s stk)
    9.73    case 0 thus ?case by simp
    9.74  next
    9.75    case (Suc k)
    9.76 @@ -357,7 +357,7 @@
    9.77    have "isize P \<le> i'" by (auto simp: exits_def)
    9.78    from rest this `exits P' \<subseteq> {0..}`     
    9.79    have "P' \<turnstile> (i' - isize P, s'', stk'') \<rightarrow>^k (n - isize P, s', stk')"
    9.80 -    by (rule Suc.hyps)
    9.81 +    by (rule Suc.IH)
    9.82    finally
    9.83    show ?case .
    9.84  qed
    9.85 @@ -411,7 +411,7 @@
    9.86  lemma acomp_exec_n [dest!]:
    9.87    "acomp a \<turnstile> (0,s,stk) \<rightarrow>^n (isize (acomp a),s',stk') \<Longrightarrow> 
    9.88    s' = s \<and> stk' = aval a s#stk"
    9.89 -proof (induct a arbitrary: n s' stk stk')
    9.90 +proof (induction a arbitrary: n s' stk stk')
    9.91    case (Plus a1 a2)
    9.92    let ?sz = "isize (acomp a1) + (isize (acomp a2) + 1)"
    9.93    from Plus.prems
    9.94 @@ -424,7 +424,7 @@
    9.95         "[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')"
    9.96      by (auto dest!: exec_n_split_full)
    9.97  
    9.98 -  thus ?case by (fastforce dest: Plus.hyps simp: exec_n_simps)
    9.99 +  thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps)
   9.100  qed (auto simp: exec_n_simps)
   9.101  
   9.102  lemma bcomp_split:
   9.103 @@ -442,13 +442,13 @@
   9.104            "isize (bcomp b c j) \<le> i" "0 \<le> j"
   9.105    shows "i = isize(bcomp b c j) + (if c = bval b s then j else 0) \<and>
   9.106           s' = s \<and> stk' = stk"
   9.107 -using assms proof (induct b arbitrary: c j i n s' stk')
   9.108 +using assms proof (induction b arbitrary: c j i n s' stk')
   9.109    case B thus ?case 
   9.110      by (simp split: split_if_asm add: exec_n_simps)
   9.111  next
   9.112    case (Not b) 
   9.113    from Not.prems show ?case
   9.114 -    by (fastforce dest!: Not.hyps) 
   9.115 +    by (fastforce dest!: Not.IH) 
   9.116  next
   9.117    case (And b1 b2)
   9.118    
   9.119 @@ -466,10 +466,10 @@
   9.120      by (auto dest!: bcomp_split dest: exec_n_drop_left)
   9.121    from b1 j
   9.122    have "i' = isize ?b1 + (if \<not>bval b1 s then ?m else 0) \<and> s'' = s \<and> stk'' = stk"
   9.123 -    by (auto dest!: And.hyps)
   9.124 +    by (auto dest!: And.IH)
   9.125    with b2 j
   9.126    show ?case 
   9.127 -    by (fastforce dest!: And.hyps simp: exec_n_end split: split_if_asm)
   9.128 +    by (fastforce dest!: And.IH simp: exec_n_end split: split_if_asm)
   9.129  next
   9.130    case Less
   9.131    thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps) (* takes time *) 
   9.132 @@ -484,7 +484,7 @@
   9.133  lemma ccomp_exec_n:
   9.134    "ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (isize(ccomp c),t,stk')
   9.135    \<Longrightarrow> (c,s) \<Rightarrow> t \<and> stk'=stk"
   9.136 -proof (induct c arbitrary: s t stk stk' n)
   9.137 +proof (induction c arbitrary: s t stk stk' n)
   9.138    case SKIP
   9.139    thus ?case by auto
   9.140  next
   9.141 @@ -496,7 +496,7 @@
   9.142    thus ?case by (fastforce dest!: exec_n_split_full)
   9.143  next
   9.144    case (If b c1 c2)
   9.145 -  note If.hyps [dest!]
   9.146 +  note If.IH [dest!]
   9.147  
   9.148    let ?if = "IF b THEN c1 ELSE c2"
   9.149    let ?cs = "ccomp ?if"
   9.150 @@ -538,7 +538,7 @@
   9.151  
   9.152    from While.prems
   9.153    show ?case
   9.154 -  proof (induct n arbitrary: s rule: nat_less_induct)
   9.155 +  proof (induction n arbitrary: s rule: nat_less_induct)
   9.156      case (1 n)
   9.157      
   9.158      { assume "\<not> bval b s"
   9.159 @@ -568,7 +568,7 @@
   9.160            "?cs \<turnstile> (0,s,stk) \<rightarrow>^m (isize (ccomp ?c0), t, stk')"
   9.161            "m < n"
   9.162            by (auto simp: exec_n_step [where k=k])
   9.163 -        with "1.hyps"
   9.164 +        with "1.IH"
   9.165          show ?case by blast
   9.166        next
   9.167          assume "ccomp c \<noteq> []"
   9.168 @@ -581,14 +581,14 @@
   9.169            by (auto dest: exec_n_split [where i=0, simplified])
   9.170          from c
   9.171          have "(c,s) \<Rightarrow> s''" and stk: "stk'' = stk"
   9.172 -          by (auto dest!: While.hyps)
   9.173 +          by (auto dest!: While.IH)
   9.174          moreover
   9.175          from rest m k stk
   9.176          obtain k' where
   9.177            "?cs \<turnstile> (0, s'', stk) \<rightarrow>^k' (isize ?cs, t, stk')"
   9.178            "k' < n"
   9.179            by (auto simp: exec_n_step [where k=m])
   9.180 -        with "1.hyps"
   9.181 +        with "1.IH"
   9.182          have "(?c0, s'') \<Rightarrow> t \<and> stk' = stk" by blast
   9.183          ultimately
   9.184          show ?case using b by blast
    10.1 --- a/src/HOL/IMP/Compiler.thy	Tue Sep 20 05:47:11 2011 +0200
    10.2 +++ b/src/HOL/IMP/Compiler.thy	Tue Sep 20 05:48:23 2011 +0200
    10.3 @@ -222,7 +222,7 @@
    10.4    "0 \<le> n \<Longrightarrow>
    10.5    bcomp b c n \<turnstile>
    10.6   (0,s,stk)  \<rightarrow>*  (isize(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
    10.7 -proof(induct b arbitrary: c n m)
    10.8 +proof(induction b arbitrary: c n m)
    10.9    case Not
   10.10    from Not(1)[where c="~c"] Not(2) show ?case by fastforce
   10.11  next
   10.12 @@ -256,17 +256,17 @@
   10.13  
   10.14  lemma ccomp_bigstep:
   10.15    "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk)"
   10.16 -proof(induct arbitrary: stk rule: big_step_induct)
   10.17 +proof(induction arbitrary: stk rule: big_step_induct)
   10.18    case (Assign x a s)
   10.19    show ?case by (fastforce simp:fun_upd_def cong: if_cong)
   10.20  next
   10.21    case (Semi c1 s1 s2 c2 s3)
   10.22    let ?cc1 = "ccomp c1"  let ?cc2 = "ccomp c2"
   10.23    have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)"
   10.24 -    using Semi.hyps(2) by fastforce
   10.25 +    using Semi.IH(1) by fastforce
   10.26    moreover
   10.27    have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)"
   10.28 -    using Semi.hyps(4) by fastforce
   10.29 +    using Semi.IH(2) by fastforce
   10.30    ultimately show ?case by simp (blast intro: exec_trans)
   10.31  next
   10.32    case (WhileTrue b s1 c s2 s3)
   10.33 @@ -274,12 +274,12 @@
   10.34    let ?cb = "bcomp b False (isize ?cc + 1)"
   10.35    let ?cw = "ccomp(WHILE b DO c)"
   10.36    have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)"
   10.37 -    using WhileTrue(1,3) by fastforce
   10.38 +    using WhileTrue.IH(1) WhileTrue.hyps(1) by fastforce
   10.39    moreover
   10.40    have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
   10.41      by fastforce
   10.42    moreover
   10.43 -  have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue(5))
   10.44 +  have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue.IH(2))
   10.45    ultimately show ?case by(blast intro: exec_trans)
   10.46  qed fastforce+
   10.47  
    11.1 --- a/src/HOL/IMP/Def_Ass_Sound_Big.thy	Tue Sep 20 05:47:11 2011 +0200
    11.2 +++ b/src/HOL/IMP/Def_Ass_Sound_Big.thy	Tue Sep 20 05:48:23 2011 +0200
    11.3 @@ -12,7 +12,7 @@
    11.4  theorem Sound:
    11.5    "\<lbrakk> (c,Some s) \<Rightarrow> s';  D A c A';  A \<subseteq> dom s \<rbrakk>
    11.6    \<Longrightarrow> \<exists> t. s' = Some t \<and> A' \<subseteq> dom t"
    11.7 -proof (induct c "Some s" s' arbitrary: s A A' rule:big_step_induct)
    11.8 +proof (induction c "Some s" s' arbitrary: s A A' rule:big_step_induct)
    11.9    case AssignNone thus ?case
   11.10      by auto (metis aval_Some option.simps(3) subset_trans)
   11.11  next
    12.1 --- a/src/HOL/IMP/Def_Ass_Sound_Small.thy	Tue Sep 20 05:47:11 2011 +0200
    12.2 +++ b/src/HOL/IMP/Def_Ass_Sound_Small.thy	Tue Sep 20 05:48:23 2011 +0200
    12.3 @@ -7,7 +7,7 @@
    12.4  
    12.5  theorem progress:
    12.6    "D (dom s) c A' \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> EX cs'. (c,s) \<rightarrow> cs'"
    12.7 -proof (induct c arbitrary: s A')
    12.8 +proof (induction c arbitrary: s A')
    12.9    case Assign thus ?case by auto (metis aval_Some small_step.Assign)
   12.10  next
   12.11    case (If b c1 c2)
   12.12 @@ -17,13 +17,13 @@
   12.13  qed (fastforce intro: small_step.intros)+
   12.14  
   12.15  lemma D_mono:  "D A c M \<Longrightarrow> A \<subseteq> A' \<Longrightarrow> EX M'. D A' c M' & M <= M'"
   12.16 -proof (induct c arbitrary: A A' M)
   12.17 +proof (induction c arbitrary: A A' M)
   12.18    case Semi thus ?case by auto (metis D.intros(3))
   12.19  next
   12.20    case (If b c1 c2)
   12.21    then obtain M1 M2 where "vars b \<subseteq> A" "D A c1 M1" "D A c2 M2" "M = M1 \<inter> M2"
   12.22      by auto
   12.23 -  with If.hyps `A \<subseteq> A'` obtain M1' M2'
   12.24 +  with If.IH `A \<subseteq> A'` obtain M1' M2'
   12.25      where "D A' c1 M1'" "D A' c2 M2'" and "M1 \<subseteq> M1'" "M2 \<subseteq> M2'" by metis
   12.26    hence "D A' (IF b THEN c1 ELSE c2) (M1' \<inter> M2')" and "M \<subseteq> M1' \<inter> M2'"
   12.27      using `vars b \<subseteq> A` `A \<subseteq> A'` `M = M1 \<inter> M2` by(fastforce intro: D.intros)+
   12.28 @@ -34,7 +34,7 @@
   12.29  
   12.30  theorem D_preservation:
   12.31    "(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c A \<Longrightarrow> EX A'. D (dom s') c' A' & A <= A'"
   12.32 -proof (induct arbitrary: A rule: small_step_induct)
   12.33 +proof (induction arbitrary: A rule: small_step_induct)
   12.34    case (While b c s)
   12.35    then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
   12.36    moreover
   12.37 @@ -49,7 +49,7 @@
   12.38  theorem D_sound:
   12.39    "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A' \<Longrightarrow> c' \<noteq> SKIP
   12.40     \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
   12.41 -apply(induct arbitrary: A' rule:star_induct)
   12.42 +apply(induction arbitrary: A' rule:star_induct)
   12.43  apply (metis progress)
   12.44  by (metis D_preservation)
   12.45  
    13.1 --- a/src/HOL/IMP/Denotation.thy	Tue Sep 20 05:47:11 2011 +0200
    13.2 +++ b/src/HOL/IMP/Denotation.thy	Tue Sep 20 05:48:23 2011 +0200
    13.3 @@ -32,7 +32,7 @@
    13.4  text{* Equivalence of denotational and big-step semantics: *}
    13.5  
    13.6  lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)"
    13.7 -apply (induct rule: big_step_induct)
    13.8 +apply (induction rule: big_step_induct)
    13.9  apply auto
   13.10  (* while *)
   13.11  apply (unfold Gamma_def)
   13.12 @@ -43,7 +43,7 @@
   13.13  done
   13.14  
   13.15  lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t"
   13.16 -apply (induct c arbitrary: s t)
   13.17 +apply (induction c arbitrary: s t)
   13.18  apply auto 
   13.19  apply blast
   13.20  (* while *)
    14.1 --- a/src/HOL/IMP/Fold.thy	Tue Sep 20 05:47:11 2011 +0200
    14.2 +++ b/src/HOL/IMP/Fold.thy	Tue Sep 20 05:48:23 2011 +0200
    14.3 @@ -81,7 +81,7 @@
    14.4  
    14.5  lemma defs_restrict:
    14.6    "defs c t |` (- lnames c) = t |` (- lnames c)"
    14.7 -proof (induct c arbitrary: t)
    14.8 +proof (induction c arbitrary: t)
    14.9    case (Semi c1 c2)
   14.10    hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
   14.11      by simp
   14.12 @@ -114,7 +114,7 @@
   14.13  
   14.14  lemma big_step_pres_approx:
   14.15    "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (defs c t) s'"
   14.16 -proof (induct arbitrary: t rule: big_step_induct)
   14.17 +proof (induction arbitrary: t rule: big_step_induct)
   14.18    case Skip thus ?case by simp
   14.19  next
   14.20    case Assign
   14.21 @@ -122,8 +122,8 @@
   14.22      by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
   14.23  next
   14.24    case (Semi c1 s1 s2 c2 s3)
   14.25 -  have "approx (defs c1 t) s2" by (rule Semi(2) [OF Semi.prems])
   14.26 -  hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi(4))
   14.27 +  have "approx (defs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems])
   14.28 +  hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi.IH(2))
   14.29    thus ?case by simp
   14.30  next
   14.31    case (IfTrue b s c1 s')
   14.32 @@ -151,7 +151,7 @@
   14.33  
   14.34  lemma big_step_pres_approx_restrict:
   14.35    "(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lnames c)) s \<Longrightarrow> approx (t |` (-lnames c)) s'"
   14.36 -proof (induct arbitrary: t rule: big_step_induct)
   14.37 +proof (induction arbitrary: t rule: big_step_induct)
   14.38    case Assign
   14.39    thus ?case by (clarsimp simp: approx_def)
   14.40  next
   14.41 @@ -190,7 +190,7 @@
   14.42  
   14.43  lemma approx_eq:
   14.44    "approx t \<Turnstile> c \<sim> fold c t"
   14.45 -proof (induct c arbitrary: t)
   14.46 +proof (induction c arbitrary: t)
   14.47    case SKIP show ?case by simp
   14.48  next
   14.49    case Assign
   14.50 @@ -292,7 +292,7 @@
   14.51  
   14.52  lemma bdefs_restrict:
   14.53    "bdefs c t |` (- lnames c) = t |` (- lnames c)"
   14.54 -proof (induct c arbitrary: t)
   14.55 +proof (induction c arbitrary: t)
   14.56    case (Semi c1 c2)
   14.57    hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
   14.58      by simp
   14.59 @@ -327,7 +327,7 @@
   14.60  
   14.61  lemma big_step_pres_approx_b:
   14.62    "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (bdefs c t) s'" 
   14.63 -proof (induct arbitrary: t rule: big_step_induct)
   14.64 +proof (induction arbitrary: t rule: big_step_induct)
   14.65    case Skip thus ?case by simp
   14.66  next
   14.67    case Assign
   14.68 @@ -335,8 +335,8 @@
   14.69      by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
   14.70  next
   14.71    case (Semi c1 s1 s2 c2 s3)
   14.72 -  have "approx (bdefs c1 t) s2" by (rule Semi(2) [OF Semi.prems])
   14.73 -  hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi(4))
   14.74 +  have "approx (bdefs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems])
   14.75 +  hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi.IH(2))
   14.76    thus ?case by simp
   14.77  next
   14.78    case (IfTrue b s c1 s')
   14.79 @@ -371,7 +371,7 @@
   14.80  
   14.81  lemma bfold_equiv: 
   14.82    "approx t \<Turnstile> c \<sim> bfold c t"
   14.83 -proof (induct c arbitrary: t)
   14.84 +proof (induction c arbitrary: t)
   14.85    case SKIP show ?case by simp
   14.86  next
   14.87    case Assign
    15.1 --- a/src/HOL/IMP/HoareT.thy	Tue Sep 20 05:47:11 2011 +0200
    15.2 +++ b/src/HOL/IMP/HoareT.thy	Tue Sep 20 05:48:23 2011 +0200
    15.3 @@ -88,7 +88,7 @@
    15.4    proof
    15.5      fix s
    15.6      show "P s \<longrightarrow> (\<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t)"
    15.7 -    proof(induct "f s" arbitrary: s rule: less_induct)
    15.8 +    proof(induction "f s" arbitrary: s rule: less_induct)
    15.9        case (less n)
   15.10        thus ?case by (metis While(2) WhileFalse WhileTrue)
   15.11      qed
   15.12 @@ -137,7 +137,7 @@
   15.13  text{* The relation is in fact a function: *}
   15.14  
   15.15  lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'"
   15.16 -proof(induct arbitrary: n' rule:Its.induct)
   15.17 +proof(induction arbitrary: n' rule:Its.induct)
   15.18  (* new release:
   15.19    case Its_0 thus ?case by(metis Its.cases)
   15.20  next
   15.21 @@ -160,7 +160,7 @@
   15.22  text{* For all terminating loops, @{const Its} yields a result: *}
   15.23  
   15.24  lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n"
   15.25 -proof(induct "WHILE b DO c" s t rule: big_step_induct)
   15.26 +proof(induction "WHILE b DO c" s t rule: big_step_induct)
   15.27    case WhileFalse thus ?case by (metis Its_0)
   15.28  next
   15.29    case WhileTrue thus ?case by (metis Its_Suc)
   15.30 @@ -179,7 +179,7 @@
   15.31  by (metis its_def WHILE_Its Its.intros(2) Its_fun the_equality)
   15.32  
   15.33  lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
   15.34 -proof (induct c arbitrary: Q)
   15.35 +proof (induction c arbitrary: Q)
   15.36    case SKIP show ?case by simp (blast intro:hoaret.Skip)
   15.37  next
   15.38    case Assign show ?case by simp (blast intro:hoaret.Assign)
    16.1 --- a/src/HOL/IMP/Hoare_Examples.thy	Tue Sep 20 05:47:11 2011 +0200
    16.2 +++ b/src/HOL/IMP/Hoare_Examples.thy	Tue Sep 20 05:48:23 2011 +0200
    16.3 @@ -25,7 +25,7 @@
    16.4    
    16.5  lemma while_sum:
    16.6    "(w n, s) \<Rightarrow> t \<Longrightarrow> t ''x'' = s ''x'' + \<Sum> {s ''y'' + 1 .. n}"
    16.7 -apply(induct "w n" s t rule: big_step_induct)
    16.8 +apply(induction "w n" s t rule: big_step_induct)
    16.9  apply(auto simp add: setsum_head_plus_1)
   16.10  done
   16.11  
    17.1 --- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Tue Sep 20 05:47:11 2011 +0200
    17.2 +++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Tue Sep 20 05:48:23 2011 +0200
    17.3 @@ -9,11 +9,11 @@
    17.4  "\<Turnstile> {P}c{Q} = (\<forall>s t. (c,s) \<Rightarrow> t  \<longrightarrow>  P s \<longrightarrow>  Q t)"
    17.5  
    17.6  lemma hoare_sound: "\<turnstile> {P}c{Q}  \<Longrightarrow>  \<Turnstile> {P}c{Q}"
    17.7 -proof(induct rule: hoare.induct)
    17.8 +proof(induction rule: hoare.induct)
    17.9    case (While P b c)
   17.10    { fix s t
   17.11      have "(WHILE b DO c,s) \<Rightarrow> t  \<Longrightarrow>  P s \<longrightarrow> P t \<and> \<not> bval b t"
   17.12 -    proof(induct "WHILE b DO c" s t rule: big_step_induct)
   17.13 +    proof(induction "WHILE b DO c" s t rule: big_step_induct)
   17.14        case WhileFalse thus ?case by blast
   17.15      next
   17.16        case WhileTrue thus ?case
   17.17 @@ -59,7 +59,7 @@
   17.18  subsection "Completeness"
   17.19  
   17.20  lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"
   17.21 -proof(induct c arbitrary: Q)
   17.22 +proof(induction c arbitrary: Q)
   17.23    case Semi thus ?case by(auto intro: Semi)
   17.24  next
   17.25    case (If b c1 c2)
    18.1 --- a/src/HOL/IMP/Live.thy	Tue Sep 20 05:47:11 2011 +0200
    18.2 +++ b/src/HOL/IMP/Live.thy	Tue Sep 20 05:48:23 2011 +0200
    18.3 @@ -44,17 +44,17 @@
    18.4  theorem L_sound:
    18.5    "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
    18.6    \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
    18.7 -proof (induct arbitrary: X t rule: big_step_induct)
    18.8 +proof (induction arbitrary: X t rule: big_step_induct)
    18.9    case Skip then show ?case by auto
   18.10  next
   18.11    case Assign then show ?case
   18.12      by (auto simp: ball_Un)
   18.13  next
   18.14    case (Semi c1 s1 s2 c2 s3 X t1)
   18.15 -  from Semi(2,5) obtain t2 where
   18.16 +  from Semi.IH(1) Semi.prems obtain t2 where
   18.17      t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
   18.18      by simp blast
   18.19 -  from Semi(4)[OF s2t2] obtain t3 where
   18.20 +  from Semi.IH(2)[OF s2t2] obtain t3 where
   18.21      t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
   18.22      by auto
   18.23    show ?case using t12 t23 s3t3 by auto
   18.24 @@ -83,9 +83,9 @@
   18.25      by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
   18.26    have "s1 = t1 on L c (L ?w X)" using  L_While_subset WhileTrue.prems
   18.27      by (blast)
   18.28 -  from WhileTrue(3)[OF this] obtain t2 where
   18.29 +  from WhileTrue.IH(1)[OF this] obtain t2 where
   18.30      "(c, t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
   18.31 -  from WhileTrue(5)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
   18.32 +  from WhileTrue.IH(2)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
   18.33      by auto
   18.34    with `bval b t1` `(c, t1) \<Rightarrow> t2` show ?case by auto
   18.35  qed
   18.36 @@ -108,17 +108,17 @@
   18.37  theorem bury_sound:
   18.38    "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
   18.39    \<exists> t'. (bury c X,t) \<Rightarrow> t' & s' = t' on X"
   18.40 -proof (induct arbitrary: X t rule: big_step_induct)
   18.41 +proof (induction arbitrary: X t rule: big_step_induct)
   18.42    case Skip then show ?case by auto
   18.43  next
   18.44    case Assign then show ?case
   18.45      by (auto simp: ball_Un)
   18.46  next
   18.47    case (Semi c1 s1 s2 c2 s3 X t1)
   18.48 -  from Semi(2,5) obtain t2 where
   18.49 +  from Semi.IH(1) Semi.prems obtain t2 where
   18.50      t12: "(bury c1 (L c2 X), t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
   18.51      by simp blast
   18.52 -  from Semi(4)[OF s2t2] obtain t3 where
   18.53 +  from Semi.IH(2)[OF s2t2] obtain t3 where
   18.54      t23: "(bury c2 X, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
   18.55      by auto
   18.56    show ?case using t12 t23 s3t3 by auto
   18.57 @@ -147,9 +147,9 @@
   18.58      by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
   18.59    have "s1 = t1 on L c (L ?w X)"
   18.60      using L_While_subset WhileTrue.prems by blast
   18.61 -  from WhileTrue(3)[OF this] obtain t2 where
   18.62 +  from WhileTrue.IH(1)[OF this] obtain t2 where
   18.63      "(bury c (L ?w X), t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
   18.64 -  from WhileTrue(5)[OF this(2)] obtain t3
   18.65 +  from WhileTrue.IH(2)[OF this(2)] obtain t3
   18.66      where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X"
   18.67      by auto
   18.68    with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto
   18.69 @@ -184,7 +184,7 @@
   18.70  theorem bury_sound2:
   18.71    "(bury c X,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
   18.72    \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
   18.73 -proof (induct "bury c X" s s' arbitrary: c X t rule: big_step_induct)
   18.74 +proof (induction "bury c X" s s' arbitrary: c X t rule: big_step_induct)
   18.75    case Skip then show ?case by auto
   18.76  next
   18.77    case Assign then show ?case
   18.78 @@ -193,9 +193,10 @@
   18.79    case (Semi bc1 s1 s2 bc2 s3 c X t1)
   18.80    then obtain c1 c2 where c: "c = c1;c2"
   18.81      and bc2: "bc2 = bury c2 X" and bc1: "bc1 = bury c1 (L c2 X)" by auto
   18.82 -  from Semi(2)[OF bc1, of t1] Semi.prems c obtain t2 where
   18.83 +  note IH = Semi.hyps(2,4)
   18.84 +  from IH(1)[OF bc1, of t1] Semi.prems c obtain t2 where
   18.85      t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X" by auto
   18.86 -  from Semi(4)[OF bc2 s2t2] obtain t3 where
   18.87 +  from IH(2)[OF bc2 s2t2] obtain t3 where
   18.88      t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
   18.89      by auto
   18.90    show ?case using c t12 t23 s3t3 by auto
   18.91 @@ -205,7 +206,8 @@
   18.92      and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
   18.93    have "s = t on vars b" "s = t on L c1 X" using IfTrue.prems c by auto
   18.94    from bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
   18.95 -  from IfTrue(3)[OF bc1 `s = t on L c1 X`] obtain t' where
   18.96 +  note IH = IfTrue.hyps(3)
   18.97 +  from IH[OF bc1 `s = t on L c1 X`] obtain t' where
   18.98      "(c1, t) \<Rightarrow> t'" "s' =t' on X" by auto
   18.99    thus ?case using c `bval b t` by auto
  18.100  next
  18.101 @@ -214,7 +216,8 @@
  18.102      and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
  18.103    have "s = t on vars b" "s = t on L c2 X" using IfFalse.prems c by auto
  18.104    from bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
  18.105 -  from IfFalse(3)[OF bc2 `s = t on L c2 X`] obtain t' where
  18.106 +  note IH = IfFalse.hyps(3)
  18.107 +  from IH[OF bc2 `s = t on L c2 X`] obtain t' where
  18.108      "(c2, t) \<Rightarrow> t'" "s' =t' on X" by auto
  18.109    thus ?case using c `~bval b t` by auto
  18.110  next
  18.111 @@ -228,11 +231,12 @@
  18.112    let ?w = "WHILE b DO c'"
  18.113    from `bval b s1` WhileTrue.prems c have "bval b t1"
  18.114      by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
  18.115 +  note IH = WhileTrue.hyps(3,5)
  18.116    have "s1 = t1 on L c' (L ?w X)"
  18.117      using L_While_subset WhileTrue.prems c by blast
  18.118 -  with WhileTrue(3)[OF bc', of t1] obtain t2 where
  18.119 +  with IH(1)[OF bc', of t1] obtain t2 where
  18.120      "(c', t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
  18.121 -  from WhileTrue(5)[OF WhileTrue(6), of t2] c this(2) obtain t3
  18.122 +  from IH(2)[OF WhileTrue.hyps(6), of t2] c this(2) obtain t3
  18.123      where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
  18.124      by auto
  18.125    with `bval b t1` `(c', t1) \<Rightarrow> t2` c show ?case by auto
    19.1 --- a/src/HOL/IMP/Poly_Types.thy	Tue Sep 20 05:47:11 2011 +0200
    19.2 +++ b/src/HOL/IMP/Poly_Types.thy	Tue Sep 20 05:48:23 2011 +0200
    19.3 @@ -45,12 +45,12 @@
    19.4  subsection{* Typing is Preserved by Substitution *}
    19.5  
    19.6  lemma subst_atyping: "E \<turnstile>p a : t \<Longrightarrow> tsubst S \<circ> E \<turnstile>p a : tsubst S t"
    19.7 -apply(induct rule: atyping.induct)
    19.8 +apply(induction rule: atyping.induct)
    19.9  apply(auto intro: atyping.intros)
   19.10  done
   19.11  
   19.12  lemma subst_btyping: "E \<turnstile>p (b::bexp) \<Longrightarrow> tsubst S \<circ> E \<turnstile>p b"
   19.13 -apply(induct rule: btyping.induct)
   19.14 +apply(induction rule: btyping.induct)
   19.15  apply(auto intro: btyping.intros)
   19.16  apply(drule subst_atyping[where S=S])
   19.17  apply(drule subst_atyping[where S=S])
   19.18 @@ -58,7 +58,7 @@
   19.19  done
   19.20  
   19.21  lemma subst_ctyping: "E \<turnstile>p (c::com) \<Longrightarrow> tsubst S \<circ> E \<turnstile>p c"
   19.22 -apply(induct rule: ctyping.induct)
   19.23 +apply(induction rule: ctyping.induct)
   19.24  apply(auto intro: ctyping.intros)
   19.25  apply(drule subst_atyping[where S=S])
   19.26  apply(simp add: o_def ctyping.intros)
    20.1 --- a/src/HOL/IMP/Sec_Typing.thy	Tue Sep 20 05:47:11 2011 +0200
    20.2 +++ b/src/HOL/IMP/Sec_Typing.thy	Tue Sep 20 05:48:23 2011 +0200
    20.3 @@ -30,7 +30,7 @@
    20.4  text{* An important property: anti-monotonicity. *}
    20.5  
    20.6  lemma anti_mono: "\<lbrakk> l \<turnstile> c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile> c"
    20.7 -apply(induct arbitrary: l' rule: sec_type.induct)
    20.8 +apply(induction arbitrary: l' rule: sec_type.induct)
    20.9  apply (metis sec_type.intros(1))
   20.10  apply (metis le_trans sec_type.intros(2))
   20.11  apply (metis sec_type.intros(3))
   20.12 @@ -39,7 +39,7 @@
   20.13  done
   20.14  
   20.15  lemma confinement: "\<lbrakk> (c,s) \<Rightarrow> t;  l \<turnstile> c \<rbrakk> \<Longrightarrow> s = t (< l)"
   20.16 -proof(induct rule: big_step_induct)
   20.17 +proof(induction rule: big_step_induct)
   20.18    case Skip thus ?case by simp
   20.19  next
   20.20    case Assign thus ?case by auto
   20.21 @@ -49,12 +49,12 @@
   20.22    case (IfTrue b s c1)
   20.23    hence "max (sec_bexp b) l \<turnstile> c1" by auto
   20.24    hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
   20.25 -  thus ?case using IfTrue.hyps by metis
   20.26 +  thus ?case using IfTrue.IH by metis
   20.27  next
   20.28    case (IfFalse b s c2)
   20.29    hence "max (sec_bexp b) l \<turnstile> c2" by auto
   20.30    hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
   20.31 -  thus ?case using IfFalse.hyps by metis
   20.32 +  thus ?case using IfFalse.IH by metis
   20.33  next
   20.34    case WhileFalse thus ?case by auto
   20.35  next
   20.36 @@ -68,7 +68,7 @@
   20.37  theorem noninterference:
   20.38    "\<lbrakk> (c,s) \<Rightarrow> s'; (c,t) \<Rightarrow> t';  0 \<turnstile> c;  s = t (\<le> l) \<rbrakk>
   20.39     \<Longrightarrow> s' = t' (\<le> l)"
   20.40 -proof(induct arbitrary: t t' rule: big_step_induct)
   20.41 +proof(induction arbitrary: t t' rule: big_step_induct)
   20.42    case Skip thus ?case by auto
   20.43  next
   20.44    case (Assign x a s)
   20.45 @@ -94,7 +94,7 @@
   20.46      assume "sec_bexp b \<le> l"
   20.47      hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
   20.48      hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le)
   20.49 -    with IfTrue.hyps(3) IfTrue.prems(1,3) `sec_bexp b \<turnstile> c1`  anti_mono
   20.50 +    with IfTrue.IH IfTrue.prems(1,3) `sec_bexp b \<turnstile> c1`  anti_mono
   20.51      show ?thesis by auto
   20.52    next
   20.53      assume "\<not> sec_bexp b \<le> l"
   20.54 @@ -115,7 +115,7 @@
   20.55      assume "sec_bexp b \<le> l"
   20.56      hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
   20.57      hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
   20.58 -    with IfFalse.hyps(3) IfFalse.prems(1,3) `sec_bexp b \<turnstile> c2` anti_mono
   20.59 +    with IfFalse.IH IfFalse.prems(1,3) `sec_bexp b \<turnstile> c2` anti_mono
   20.60      show ?thesis by auto
   20.61    next
   20.62      assume "\<not> sec_bexp b \<le> l"
   20.63 @@ -157,14 +157,14 @@
   20.64        using `bval b s1` by(simp add: bval_eq_if_eq_le)
   20.65      then obtain t2 where "(c,t1) \<Rightarrow> t2" "(?w,t2) \<Rightarrow> t3"
   20.66        using `(?w,t1) \<Rightarrow> t3` by auto
   20.67 -    from WhileTrue.hyps(5)[OF `(?w,t2) \<Rightarrow> t3` `0 \<turnstile> ?w`
   20.68 -      WhileTrue.hyps(3)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec_bexp b \<turnstile> c`]
   20.69 +    from WhileTrue.IH(2)[OF `(?w,t2) \<Rightarrow> t3` `0 \<turnstile> ?w`
   20.70 +      WhileTrue.IH(1)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec_bexp b \<turnstile> c`]
   20.71          `s1 = t1 (\<le> l)`]]
   20.72      show ?thesis by simp
   20.73    next
   20.74      assume "\<not> sec_bexp b \<le> l"
   20.75      have 1: "sec_bexp b \<turnstile> ?w" by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c`)
   20.76 -    from confinement[OF big_step.WhileTrue[OF WhileTrue(1,2,4)] 1] `\<not> sec_bexp b \<le> l`
   20.77 +    from confinement[OF big_step.WhileTrue[OF WhileTrue.hyps] 1] `\<not> sec_bexp b \<le> l`
   20.78      have "s1 = s3 (\<le> l)" by auto
   20.79      moreover
   20.80      from confinement[OF WhileTrue.prems(1) 1] `\<not> sec_bexp b \<le> l`
   20.81 @@ -196,7 +196,7 @@
   20.82    "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
   20.83  
   20.84  lemma sec_type_sec_type': "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
   20.85 -apply(induct rule: sec_type.induct)
   20.86 +apply(induction rule: sec_type.induct)
   20.87  apply (metis Skip')
   20.88  apply (metis Assign')
   20.89  apply (metis Semi')
   20.90 @@ -205,7 +205,7 @@
   20.91  
   20.92  
   20.93  lemma sec_type'_sec_type: "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
   20.94 -apply(induct rule: sec_type'.induct)
   20.95 +apply(induction rule: sec_type'.induct)
   20.96  apply (metis Skip)
   20.97  apply (metis Assign)
   20.98  apply (metis Semi)
   20.99 @@ -230,7 +230,7 @@
  20.100  
  20.101  
  20.102  lemma sec_type2_sec_type': "\<turnstile> c : l \<Longrightarrow> l \<turnstile>' c"
  20.103 -apply(induct rule: sec_type2.induct)
  20.104 +apply(induction rule: sec_type2.induct)
  20.105  apply (metis Skip')
  20.106  apply (metis Assign' eq_imp_le)
  20.107  apply (metis Semi' anti_mono' min_max.inf.commute min_max.inf_le2)
  20.108 @@ -238,7 +238,7 @@
  20.109  by (metis While')
  20.110  
  20.111  lemma sec_type'_sec_type2: "l \<turnstile>' c \<Longrightarrow> \<exists> l' \<ge> l. \<turnstile> c : l'"
  20.112 -apply(induct rule: sec_type'.induct)
  20.113 +apply(induction rule: sec_type'.induct)
  20.114  apply (metis Skip2 le_refl)
  20.115  apply (metis Assign2)
  20.116  apply (metis Semi2 min_max.inf_greatest)
    21.1 --- a/src/HOL/IMP/Sec_TypingT.thy	Tue Sep 20 05:47:11 2011 +0200
    21.2 +++ b/src/HOL/IMP/Sec_TypingT.thy	Tue Sep 20 05:48:23 2011 +0200
    21.3 @@ -23,7 +23,7 @@
    21.4  
    21.5  
    21.6  lemma anti_mono: "l \<turnstile> c \<Longrightarrow> l' \<le> l \<Longrightarrow> l' \<turnstile> c"
    21.7 -apply(induct arbitrary: l' rule: sec_type.induct)
    21.8 +apply(induction arbitrary: l' rule: sec_type.induct)
    21.9  apply (metis sec_type.intros(1))
   21.10  apply (metis le_trans sec_type.intros(2))
   21.11  apply (metis sec_type.intros(3))
   21.12 @@ -32,7 +32,7 @@
   21.13  
   21.14  
   21.15  lemma confinement: "(c,s) \<Rightarrow> t \<Longrightarrow> l \<turnstile> c \<Longrightarrow> s = t (< l)"
   21.16 -proof(induct rule: big_step_induct)
   21.17 +proof(induction rule: big_step_induct)
   21.18    case Skip thus ?case by simp
   21.19  next
   21.20    case Assign thus ?case by auto
   21.21 @@ -42,12 +42,12 @@
   21.22    case (IfTrue b s c1)
   21.23    hence "max (sec_bexp b) l \<turnstile> c1" by auto
   21.24    hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
   21.25 -  thus ?case using IfTrue.hyps by metis
   21.26 +  thus ?case using IfTrue.IH by metis
   21.27  next
   21.28    case (IfFalse b s c2)
   21.29    hence "max (sec_bexp b) l \<turnstile> c2" by auto
   21.30    hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
   21.31 -  thus ?case using IfFalse.hyps by metis
   21.32 +  thus ?case using IfFalse.IH by metis
   21.33  next
   21.34    case WhileFalse thus ?case by auto
   21.35  next
   21.36 @@ -57,7 +57,7 @@
   21.37  qed
   21.38  
   21.39  lemma termi_if_non0: "l \<turnstile> c \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> \<exists> t. (c,s) \<Rightarrow> t"
   21.40 -apply(induct arbitrary: s rule: sec_type.induct)
   21.41 +apply(induction arbitrary: s rule: sec_type.induct)
   21.42  apply (metis big_step.Skip)
   21.43  apply (metis big_step.Assign)
   21.44  apply (metis big_step.Semi)
   21.45 @@ -67,7 +67,7 @@
   21.46  
   21.47  theorem noninterference: "(c,s) \<Rightarrow> s' \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow>  s = t (\<le> l)
   21.48    \<Longrightarrow> \<exists> t'. (c,t) \<Rightarrow> t' \<and> s' = t' (\<le> l)"
   21.49 -proof(induct arbitrary: t rule: big_step_induct)
   21.50 +proof(induction arbitrary: t rule: big_step_induct)
   21.51    case Skip thus ?case by auto
   21.52  next
   21.53    case (Assign x a s)
   21.54 @@ -152,9 +152,9 @@
   21.55    let ?w = "WHILE b DO c"
   21.56    from `0 \<turnstile> ?w` have [simp]: "sec_bexp b = 0" by auto
   21.57    have "0 \<turnstile> c" using WhileTrue.prems(1) by auto
   21.58 -  from WhileTrue(3)[OF this WhileTrue.prems(2)]
   21.59 +  from WhileTrue.IH(1)[OF this WhileTrue.prems(2)]
   21.60    obtain t'' where "(c,t) \<Rightarrow> t''" and "s'' = t'' (\<le>l)" by blast
   21.61 -  from WhileTrue(5)[OF `0 \<turnstile> ?w` this(2)]
   21.62 +  from WhileTrue.IH(2)[OF `0 \<turnstile> ?w` this(2)]
   21.63    obtain t' where "(?w,t'') \<Rightarrow> t'" and "s' = t' (\<le>l)" by blast
   21.64    from `bval b s` have "bval b t"
   21.65      using bval_eq_if_eq_le[OF `s = t (\<le>l)`] by auto
   21.66 @@ -185,7 +185,7 @@
   21.67    "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
   21.68  
   21.69  lemma "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
   21.70 -apply(induct rule: sec_type.induct)
   21.71 +apply(induction rule: sec_type.induct)
   21.72  apply (metis Skip')
   21.73  apply (metis Assign')
   21.74  apply (metis Semi')
   21.75 @@ -194,7 +194,7 @@
   21.76  
   21.77  
   21.78  lemma "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
   21.79 -apply(induct rule: sec_type'.induct)
   21.80 +apply(induction rule: sec_type'.induct)
   21.81  apply (metis Skip)
   21.82  apply (metis Assign)
   21.83  apply (metis Semi)
    22.1 --- a/src/HOL/IMP/Sem_Equiv.thy	Tue Sep 20 05:47:11 2011 +0200
    22.2 +++ b/src/HOL/IMP/Sem_Equiv.thy	Tue Sep 20 05:48:23 2011 +0200
    22.3 @@ -83,10 +83,9 @@
    22.4           P s \<Longrightarrow> 
    22.5           d = WHILE b DO c \<Longrightarrow> 
    22.6           (WHILE b' DO c', s) \<Rightarrow> s'"  
    22.7 -proof (induct rule: big_step_induct)
    22.8 +proof (induction rule: big_step_induct)
    22.9    case (WhileTrue b s1 c s2 s3)
   22.10 -  note IH = WhileTrue.hyps(5) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
   22.11 -  
   22.12 +  note IH = WhileTrue.IH(2) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
   22.13    from WhileTrue.prems
   22.14    have "P \<Turnstile> b <\<sim>> b'" by simp
   22.15    with `bval b s1` `P s1`
    23.1 --- a/src/HOL/IMP/Small_Step.thy	Tue Sep 20 05:47:11 2011 +0200
    23.2 +++ b/src/HOL/IMP/Small_Step.thy	Tue Sep 20 05:48:23 2011 +0200
    23.3 @@ -71,7 +71,7 @@
    23.4  text{* A simple property: *}
    23.5  lemma deterministic:
    23.6    "cs \<rightarrow> cs' \<Longrightarrow> cs \<rightarrow> cs'' \<Longrightarrow> cs'' = cs'"
    23.7 -apply(induct arbitrary: cs'' rule: small_step.induct)
    23.8 +apply(induction arbitrary: cs'' rule: small_step.induct)
    23.9  apply blast+
   23.10  done
   23.11  
   23.12 @@ -79,7 +79,7 @@
   23.13  subsection "Equivalence with big-step semantics"
   23.14  
   23.15  lemma star_semi2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')"
   23.16 -proof(induct rule: star_induct)
   23.17 +proof(induction rule: star_induct)
   23.18    case refl thus ?case by simp
   23.19  next
   23.20    case step
   23.21 @@ -98,7 +98,7 @@
   23.22  
   23.23  lemma big_to_small:
   23.24    "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
   23.25 -proof (induct rule: big_step.induct)
   23.26 +proof (induction rule: big_step.induct)
   23.27    fix s show "(SKIP,s) \<rightarrow>* (SKIP,s)" by simp
   23.28  next
   23.29    fix x a s show "(x ::= a,s) \<rightarrow>* (SKIP, s(x := aval a s))" by auto
   23.30 @@ -140,7 +140,7 @@
   23.31  
   23.32  text{* Each case of the induction can be proved automatically: *}
   23.33  lemma  "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
   23.34 -proof (induct rule: big_step.induct)
   23.35 +proof (induction rule: big_step.induct)
   23.36    case Skip show ?case by blast
   23.37  next
   23.38    case Assign show ?case by blast
   23.39 @@ -161,13 +161,13 @@
   23.40  
   23.41  lemma small1_big_continue:
   23.42    "cs \<rightarrow> cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
   23.43 -apply (induct arbitrary: t rule: small_step.induct)
   23.44 +apply (induction arbitrary: t rule: small_step.induct)
   23.45  apply auto
   23.46  done
   23.47  
   23.48  lemma small_big_continue:
   23.49    "cs \<rightarrow>* cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
   23.50 -apply (induct rule: star.induct)
   23.51 +apply (induction rule: star.induct)
   23.52  apply (auto intro: small1_big_continue)
   23.53  done
   23.54  
   23.55 @@ -188,7 +188,7 @@
   23.56  
   23.57  lemma finalD: "final (c,s) \<Longrightarrow> c = SKIP"
   23.58  apply(simp add: final_def)
   23.59 -apply(induct c)
   23.60 +apply(induction c)
   23.61  apply blast+
   23.62  done
   23.63  
    24.1 --- a/src/HOL/IMP/Star.thy	Tue Sep 20 05:47:11 2011 +0200
    24.2 +++ b/src/HOL/IMP/Star.thy	Tue Sep 20 05:48:23 2011 +0200
    24.3 @@ -9,7 +9,7 @@
    24.4  
    24.5  lemma star_trans:
    24.6    "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
    24.7 -proof(induct rule: star.induct)
    24.8 +proof(induction rule: star.induct)
    24.9    case refl thus ?case .
   24.10  next
   24.11    case step thus ?case by (metis star.step)
    25.1 --- a/src/HOL/IMP/Types.thy	Tue Sep 20 05:47:11 2011 +0200
    25.2 +++ b/src/HOL/IMP/Types.thy	Tue Sep 20 05:48:23 2011 +0200
    25.3 @@ -119,28 +119,28 @@
    25.4  
    25.5  lemma apreservation:
    25.6    "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> taval a s v \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> type v = \<tau>"
    25.7 -apply(induct arbitrary: v rule: atyping.induct)
    25.8 +apply(induction arbitrary: v rule: atyping.induct)
    25.9  apply (fastforce simp: styping_def)+
   25.10  done
   25.11  
   25.12  lemma aprogress: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. taval a s v"
   25.13 -proof(induct rule: atyping.induct)
   25.14 +proof(induction rule: atyping.induct)
   25.15    case (Plus_ty \<Gamma> a1 t a2)
   25.16    then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast
   25.17    show ?case
   25.18    proof (cases v1)
   25.19      case Iv
   25.20 -    with Plus_ty(1,3,5) v show ?thesis
   25.21 +    with Plus_ty v show ?thesis
   25.22        by(fastforce intro: taval.intros(4) dest!: apreservation)
   25.23    next
   25.24      case Rv
   25.25 -    with Plus_ty(1,3,5) v show ?thesis
   25.26 +    with Plus_ty v show ?thesis
   25.27        by(fastforce intro: taval.intros(5) dest!: apreservation)
   25.28    qed
   25.29  qed (auto intro: taval.intros)
   25.30  
   25.31  lemma bprogress: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. tbval b s v"
   25.32 -proof(induct rule: btyping.induct)
   25.33 +proof(induction rule: btyping.induct)
   25.34    case (Less_ty \<Gamma> a1 t a2)
   25.35    then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2"
   25.36      by (metis aprogress)
   25.37 @@ -158,7 +158,7 @@
   25.38  
   25.39  theorem progress:
   25.40    "\<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> \<exists>cs'. (c,s) \<rightarrow> cs'"
   25.41 -proof(induct rule: ctyping.induct)
   25.42 +proof(induction rule: ctyping.induct)
   25.43    case Skip_ty thus ?case by simp
   25.44  next
   25.45    case Assign_ty 
   25.46 @@ -182,7 +182,7 @@
   25.47  
   25.48  theorem styping_preservation:
   25.49    "(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<Gamma> \<turnstile> s'"
   25.50 -proof(induct rule: small_step_induct)
   25.51 +proof(induction rule: small_step_induct)
   25.52    case Assign thus ?case
   25.53      by (auto simp: styping_def) (metis Assign(1,3) apreservation)
   25.54  qed auto
   25.55 @@ -197,7 +197,7 @@
   25.56  theorem type_sound:
   25.57    "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c' \<noteq> SKIP
   25.58     \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
   25.59 -apply(induct rule:star_induct)
   25.60 +apply(induction rule:star_induct)
   25.61  apply (metis progress)
   25.62  by (metis styping_preservation ctyping_preservation)
   25.63  
    26.1 --- a/src/HOL/IMP/VC.thy	Tue Sep 20 05:47:11 2011 +0200
    26.2 +++ b/src/HOL/IMP/VC.thy	Tue Sep 20 05:48:23 2011 +0200
    26.3 @@ -49,14 +49,14 @@
    26.4  subsection "Soundness"
    26.5  
    26.6  lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} astrip c {Q}"
    26.7 -proof(induct c arbitrary: Q)
    26.8 +proof(induction c arbitrary: Q)
    26.9    case (Awhile b I c)
   26.10    show ?case
   26.11    proof(simp, rule While')
   26.12      from `\<forall>s. vc (Awhile b I c) Q s`
   26.13      have vc: "\<forall>s. vc c I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and
   26.14           pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre c I s" by simp_all
   26.15 -    have "\<turnstile> {pre c I} astrip c {I}" by(rule Awhile.hyps[OF vc])
   26.16 +    have "\<turnstile> {pre c I} astrip c {I}" by(rule Awhile.IH[OF vc])
   26.17      with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} astrip c {I}"
   26.18        by(rule strengthen_pre)
   26.19      show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ)
   26.20 @@ -72,20 +72,20 @@
   26.21  
   26.22  lemma pre_mono:
   26.23    "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre c P s \<Longrightarrow> pre c P' s"
   26.24 -proof (induct c arbitrary: P P' s)
   26.25 +proof (induction c arbitrary: P P' s)
   26.26    case Asemi thus ?case by simp metis
   26.27  qed simp_all
   26.28  
   26.29  lemma vc_mono:
   26.30    "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc c P s \<Longrightarrow> vc c P' s"
   26.31 -proof(induct c arbitrary: P P')
   26.32 +proof(induction c arbitrary: P P')
   26.33    case Asemi thus ?case by simp (metis pre_mono)
   26.34  qed simp_all
   26.35  
   26.36  lemma vc_complete:
   26.37   "\<turnstile> {P}c{Q} \<Longrightarrow> \<exists>c'. astrip c' = c \<and> (\<forall>s. vc c' Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c' Q s)"
   26.38    (is "_ \<Longrightarrow> \<exists>c'. ?G P c Q c'")
   26.39 -proof (induct rule: hoare.induct)
   26.40 +proof (induction rule: hoare.induct)
   26.41    case Skip
   26.42    show ?case (is "\<exists>ac. ?C ac")
   26.43    proof show "?C Askip" by simp qed
   26.44 @@ -95,8 +95,8 @@
   26.45    proof show "?C(Aassign x a)" by simp qed
   26.46  next
   26.47    case (Semi P c1 Q c2 R)
   26.48 -  from Semi.hyps obtain ac1 where ih1: "?G P c1 Q ac1" by blast
   26.49 -  from Semi.hyps obtain ac2 where ih2: "?G Q c2 R ac2" by blast
   26.50 +  from Semi.IH obtain ac1 where ih1: "?G P c1 Q ac1" by blast
   26.51 +  from Semi.IH obtain ac2 where ih2: "?G Q c2 R ac2" by blast
   26.52    show ?case (is "\<exists>ac. ?C ac")
   26.53    proof
   26.54      show "?C(Asemi ac1 ac2)"
   26.55 @@ -104,9 +104,9 @@
   26.56    qed
   26.57  next
   26.58    case (If P b c1 Q c2)
   26.59 -  from If.hyps obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1"
   26.60 +  from If.IH obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1"
   26.61      by blast
   26.62 -  from If.hyps obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2"
   26.63 +  from If.IH obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2"
   26.64      by blast
   26.65    show ?case (is "\<exists>ac. ?C ac")
   26.66    proof
   26.67 @@ -114,7 +114,7 @@
   26.68    qed
   26.69  next
   26.70    case (While P b c)
   26.71 -  from While.hyps obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast
   26.72 +  from While.IH obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast
   26.73    show ?case (is "\<exists>ac. ?C ac")
   26.74    proof show "?C(Awhile b P ac)" using ih by simp qed
   26.75  next
    27.1 --- a/src/HOL/IMP/Vars.thy	Tue Sep 20 05:47:11 2011 +0200
    27.2 +++ b/src/HOL/IMP/Vars.thy	Tue Sep 20 05:48:23 2011 +0200
    27.3 @@ -59,13 +59,13 @@
    27.4  
    27.5  lemma aval_eq_if_eq_on_vars[simp]:
    27.6    "s\<^isub>1 = s\<^isub>2 on vars a \<Longrightarrow> aval a s\<^isub>1 = aval a s\<^isub>2"
    27.7 -apply(induct a)
    27.8 +apply(induction a)
    27.9  apply simp_all
   27.10  done
   27.11  
   27.12  lemma bval_eq_if_eq_on_vars:
   27.13    "s\<^isub>1 = s\<^isub>2 on vars b \<Longrightarrow> bval b s\<^isub>1 = bval b s\<^isub>2"
   27.14 -proof(induct b)
   27.15 +proof(induction b)
   27.16    case (Less a1 a2)
   27.17    hence "aval a1 s\<^isub>1 = aval a1 s\<^isub>2" and "aval a2 s\<^isub>1 = aval a2 s\<^isub>2" by simp_all
   27.18    thus ?case by simp