# HG changeset patch
# User nipkow
# Date 1316490503 -7200
# Node ID fdac1e9880eb0664402e2c82793d54b82ea82170
# Parent  0e847655b2d87c33aa05e033ba82a4dc862b0949
Updated IMP to use new induction method

diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/AExp.thy
--- a/src/HOL/IMP/AExp.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/AExp.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -62,7 +62,7 @@
 
 theorem aval_asimp_const[simp]:
   "aval (asimp_const a) s = aval a s"
-apply(induct a)
+apply(induction a)
 apply (auto split: aexp.split)
 done
 
@@ -77,7 +77,7 @@
 
 lemma aval_plus[simp]:
   "aval (plus a1 a2) s = aval a1 s + aval a2 s"
-apply(induct a1 a2 rule: plus.induct)
+apply(induction a1 a2 rule: plus.induct)
 apply simp_all (* just for a change from auto *)
 done
 
@@ -94,7 +94,7 @@
 
 theorem aval_asimp[simp]:
   "aval (asimp a) s = aval a s"
-apply(induct a)
+apply(induction a)
 apply simp_all
 done
 
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/ASM.thy
--- a/src/HOL/IMP/ASM.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/ASM.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -29,7 +29,7 @@
 
 lemma aexec_append[simp]:
   "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
-apply(induct is1 arbitrary: stk)
+apply(induction is1 arbitrary: stk)
 apply (auto)
 done
 
@@ -44,7 +44,7 @@
 value "acomp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
 
 theorem aexec_acomp[simp]: "aexec (acomp a) s stk = aval a s # stk"
-apply(induct a arbitrary: stk)
+apply(induction a arbitrary: stk)
 apply (auto)
 done
 
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/AbsInt0.thy
--- a/src/HOL/IMP/AbsInt0.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/AbsInt0.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -38,7 +38,7 @@
 "AI (WHILE b DO c) S = pfp (AI c) S"
 
 lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
-proof(induct c arbitrary: s t S0)
+proof(induction c arbitrary: s t S0)
   case SKIP thus ?case by fastforce
 next
   case Assign thus ?case
@@ -52,10 +52,10 @@
   case (While b c)
   let ?P = "pfp (AI c) S0"
   { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
-    proof(induct "WHILE b DO c" s t rule: big_step_induct)
+    proof(induction "WHILE b DO c" s t rule: big_step_induct)
       case WhileFalse thus ?case by simp
     next
-      case WhileTrue thus ?case using While.hyps pfp astate_in_rep_le by metis
+      case WhileTrue thus ?case using While.IH pfp astate_in_rep_le by metis
     qed
   }
   with astate_in_rep_le[OF `s <: S0` above]
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/AbsInt0_fun.thy
--- a/src/HOL/IMP/AbsInt0_fun.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/AbsInt0_fun.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -36,7 +36,7 @@
 "iter (Suc n) f x = (if f x \<sqsubseteq> x then x else iter n f (f x))"
 
 lemma iter_pfp: "f(iter n f x) \<sqsubseteq> iter n f x"
-apply (induct n arbitrary: x)
+apply (induction n arbitrary: x)
  apply (simp)
 apply (simp)
 done
@@ -52,7 +52,7 @@
 point does @{const iter} yield? *}
 
 lemma iter_funpow: "iter n f x \<noteq> Top \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
-apply(induct n arbitrary: x)
+apply(induction n arbitrary: x)
  apply simp
 apply (auto)
  apply(metis funpow.simps(1) id_def)
@@ -69,7 +69,7 @@
     using iter_funpow[OF `iter n f x0 \<noteq> Top`] by blast
   moreover
   { fix n have "(f^^n) x0 \<sqsubseteq> p"
-    proof(induct n)
+    proof(induction n)
       case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
     next
       case (Suc n) thus ?case
@@ -155,7 +155,7 @@
 "AI (WHILE b DO c) S = pfp (AI c) S"
 
 lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
-proof(induct c arbitrary: s t S0)
+proof(induction c arbitrary: s t S0)
   case SKIP thus ?case by fastforce
 next
   case Assign thus ?case by (auto simp: aval'_sound)
@@ -167,10 +167,10 @@
   case (While b c)
   let ?P = "pfp (AI c) S0"
   { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
-    proof(induct "WHILE b DO c" s t rule: big_step_induct)
+    proof(induction "WHILE b DO c" s t rule: big_step_induct)
       case WhileFalse thus ?case by simp
     next
-      case WhileTrue thus ?case by(metis While.hyps pfp fun_in_rep_le)
+      case WhileTrue thus ?case by(metis While.IH pfp fun_in_rep_le)
     qed
   }
   with fun_in_rep_le[OF `s <: S0` above]
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/AbsInt1.thy
--- a/src/HOL/IMP/AbsInt1.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/AbsInt1.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -141,7 +141,7 @@
    in afilter e1 res1 (afilter e2 res2 S))"
 
 lemma afilter_sound: "s <:: S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:: afilter e a S"
-proof(induct e arbitrary: a S)
+proof(induction e arbitrary: a S)
   case N thus ?case by simp
 next
   case (V x)
@@ -158,7 +158,7 @@
 qed
 
 lemma bfilter_sound: "s <:: S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:: bfilter b bv S"
-proof(induct b arbitrary: S bv)
+proof(induction b arbitrary: S bv)
   case B thus ?case by simp
 next
   case (Not b) thus ?case by simp
@@ -181,7 +181,7 @@
   bfilter b False (pfp (\<lambda>S. AI c (bfilter b True S)) S)"
 
 lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S"
-proof(induct c arbitrary: s t S)
+proof(induction c arbitrary: s t S)
   case SKIP thus ?case by fastforce
 next
   case Assign thus ?case
@@ -196,12 +196,12 @@
   { fix s t
     have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <:: ?P \<Longrightarrow>
           t <:: bfilter b False ?P"
-    proof(induct "WHILE b DO c" s t rule: big_step_induct)
+    proof(induction "WHILE b DO c" s t rule: big_step_induct)
       case WhileFalse thus ?case by(metis bfilter_sound)
     next
       case WhileTrue show ?case
         by(rule WhileTrue, rule in_rep_up_trans[OF _ pfp],
-           rule While.hyps[OF WhileTrue(2)],
+           rule While.IH[OF WhileTrue(2)],
            rule bfilter_sound[OF WhileTrue.prems], simp add: WhileTrue(1))
     qed
   }
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/AbsInt2.thy
--- a/src/HOL/IMP/AbsInt2.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/AbsInt2.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -24,7 +24,7 @@
   (let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla> fx))"
 
 lemma iter_up_pfp: "f(iter_up f n x) \<sqsubseteq> iter_up f n x"
-apply (induct n arbitrary: x)
+apply (induction n arbitrary: x)
  apply (simp)
 apply (simp add: Let_def)
 done
@@ -35,7 +35,7 @@
   (let y = x \<triangle> f x in if f y \<sqsubseteq> y then iter_down f n y else x)"
 
 lemma iter_down_pfp: "f x \<sqsubseteq> x \<Longrightarrow> f(iter_down f n x) \<sqsubseteq> iter_down f n x"
-apply (induct n arbitrary: x)
+apply (induction n arbitrary: x)
  apply (simp)
 apply (simp add: Let_def)
 done
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/BExp.thy
--- a/src/HOL/IMP/BExp.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/BExp.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -23,7 +23,7 @@
 "less a1 a2 = Less a1 a2"
 
 lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
-apply(induct a1 a2 rule: less.induct)
+apply(induction a1 a2 rule: less.induct)
 apply simp_all
 done
 
@@ -35,7 +35,7 @@
 "and b1 b2 = And b1 b2"
 
 lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)"
-apply(induct b1 b2 rule: and.induct)
+apply(induction b1 b2 rule: and.induct)
 apply simp_all
 done
 
@@ -45,7 +45,7 @@
 "not b = Not b"
 
 lemma bval_not[simp]: "bval (not b) s = (~bval b s)"
-apply(induct b rule: not.induct)
+apply(induction b rule: not.induct)
 apply simp_all
 done
 
@@ -62,7 +62,7 @@
 value "bsimp (And (Less (N 1) (N 0)) (B True))"
 
 theorem "bval (bsimp b) s = bval b s"
-apply(induct b)
+apply(induction b)
 apply simp_all
 done
 
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Big_Step.thy
--- a/src/HOL/IMP/Big_Step.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Big_Step.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -215,7 +215,7 @@
 
 text {* This proof is automatic. *}
 theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
-apply (induct arbitrary: u rule: big_step.induct)
+apply (induction arbitrary: u rule: big_step.induct)
 apply blast+
 done
 
@@ -225,7 +225,7 @@
 *}
 theorem
   "(c,s) \<Rightarrow> t  \<Longrightarrow>  (c,s) \<Rightarrow> t'  \<Longrightarrow>  t' = t"
-proof (induct arbitrary: t' rule: big_step.induct)
+proof (induction arbitrary: t' rule: big_step.induct)
   -- "the only interesting case, @{text WhileTrue}:"
   fix b c s s1 t t'
   -- "The assumptions of the rule:"
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Comp_Rev.thy
--- a/src/HOL/IMP/Comp_Rev.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Comp_Rev.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -196,13 +196,13 @@
   "0 \<le> i \<Longrightarrow>
   succs (bcomp b c i) n \<subseteq> {n .. n + isize (bcomp b c i)}
                            \<union> {n + i + isize (bcomp b c i)}" 
-proof (induct b arbitrary: c i n)
+proof (induction b arbitrary: c i n)
   case (And b1 b2)
   from And.prems
   show ?case 
     by (cases c)
-       (auto dest: And.hyps(1) [THEN subsetD, rotated] 
-                   And.hyps(2) [THEN subsetD, rotated])
+       (auto dest: And.IH(1) [THEN subsetD, rotated] 
+                   And.IH(2) [THEN subsetD, rotated])
 qed auto
 
 lemmas bcomp_succsD [dest!] = bcomp_succs [THEN subsetD, rotated]
@@ -219,7 +219,7 @@
 
 lemma ccomp_succs:
   "succs (ccomp c) n \<subseteq> {n..n + isize (ccomp c)}"
-proof (induct c arbitrary: n)
+proof (induction c arbitrary: n)
   case SKIP thus ?case by simp
 next
   case Assign thus ?case by simp
@@ -227,16 +227,16 @@
   case (Semi c1 c2)
   from Semi.prems
   show ?case 
-    by (fastforce dest: Semi.hyps [THEN subsetD])
+    by (fastforce dest: Semi.IH [THEN subsetD])
 next
   case (If b c1 c2)
   from If.prems
   show ?case
-    by (auto dest!: If.hyps [THEN subsetD] simp: isuccs_def succs_Cons)
+    by (auto dest!: If.IH [THEN subsetD] simp: isuccs_def succs_Cons)
 next
   case (While b c)
   from While.prems
-  show ?case by (auto dest!: While.hyps [THEN subsetD])
+  show ?case by (auto dest!: While.IH [THEN subsetD])
 qed
 
 lemma ccomp_exits:
@@ -264,7 +264,7 @@
                    i' \<in> exits c \<and> 
                    P @ c @ P' \<turnstile> (isize P + i', s'') \<rightarrow>^m (j, s') \<and>
                    n = k + m" 
-using assms proof (induct n arbitrary: i j s)
+using assms proof (induction n arbitrary: i j s)
   case 0
   thus ?case by simp
 next
@@ -289,7 +289,7 @@
   { assume "j0 \<in> {0 ..< isize c}"
     with j0 j rest c
     have ?case
-      by (fastforce dest!: Suc.hyps intro!: exec_Suc)
+      by (fastforce dest!: Suc.IH intro!: exec_Suc)
   } moreover {
     assume "j0 \<notin> {0 ..< isize c}"
     moreover
@@ -338,7 +338,7 @@
   assumes "P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk')"
           "isize P \<le> i" "exits P' \<subseteq> {0..}"
   shows "P' \<turnstile> (i - isize P, s, stk) \<rightarrow>^k (n - isize P, s', stk')"
-using assms proof (induct k arbitrary: i s stk)
+using assms proof (induction k arbitrary: i s stk)
   case 0 thus ?case by simp
 next
   case (Suc k)
@@ -357,7 +357,7 @@
   have "isize P \<le> i'" by (auto simp: exits_def)
   from rest this `exits P' \<subseteq> {0..}`     
   have "P' \<turnstile> (i' - isize P, s'', stk'') \<rightarrow>^k (n - isize P, s', stk')"
-    by (rule Suc.hyps)
+    by (rule Suc.IH)
   finally
   show ?case .
 qed
@@ -411,7 +411,7 @@
 lemma acomp_exec_n [dest!]:
   "acomp a \<turnstile> (0,s,stk) \<rightarrow>^n (isize (acomp a),s',stk') \<Longrightarrow> 
   s' = s \<and> stk' = aval a s#stk"
-proof (induct a arbitrary: n s' stk stk')
+proof (induction a arbitrary: n s' stk stk')
   case (Plus a1 a2)
   let ?sz = "isize (acomp a1) + (isize (acomp a2) + 1)"
   from Plus.prems
@@ -424,7 +424,7 @@
        "[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')"
     by (auto dest!: exec_n_split_full)
 
-  thus ?case by (fastforce dest: Plus.hyps simp: exec_n_simps)
+  thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps)
 qed (auto simp: exec_n_simps)
 
 lemma bcomp_split:
@@ -442,13 +442,13 @@
           "isize (bcomp b c j) \<le> i" "0 \<le> j"
   shows "i = isize(bcomp b c j) + (if c = bval b s then j else 0) \<and>
          s' = s \<and> stk' = stk"
-using assms proof (induct b arbitrary: c j i n s' stk')
+using assms proof (induction b arbitrary: c j i n s' stk')
   case B thus ?case 
     by (simp split: split_if_asm add: exec_n_simps)
 next
   case (Not b) 
   from Not.prems show ?case
-    by (fastforce dest!: Not.hyps) 
+    by (fastforce dest!: Not.IH) 
 next
   case (And b1 b2)
   
@@ -466,10 +466,10 @@
     by (auto dest!: bcomp_split dest: exec_n_drop_left)
   from b1 j
   have "i' = isize ?b1 + (if \<not>bval b1 s then ?m else 0) \<and> s'' = s \<and> stk'' = stk"
-    by (auto dest!: And.hyps)
+    by (auto dest!: And.IH)
   with b2 j
   show ?case 
-    by (fastforce dest!: And.hyps simp: exec_n_end split: split_if_asm)
+    by (fastforce dest!: And.IH simp: exec_n_end split: split_if_asm)
 next
   case Less
   thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps) (* takes time *) 
@@ -484,7 +484,7 @@
 lemma ccomp_exec_n:
   "ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (isize(ccomp c),t,stk')
   \<Longrightarrow> (c,s) \<Rightarrow> t \<and> stk'=stk"
-proof (induct c arbitrary: s t stk stk' n)
+proof (induction c arbitrary: s t stk stk' n)
   case SKIP
   thus ?case by auto
 next
@@ -496,7 +496,7 @@
   thus ?case by (fastforce dest!: exec_n_split_full)
 next
   case (If b c1 c2)
-  note If.hyps [dest!]
+  note If.IH [dest!]
 
   let ?if = "IF b THEN c1 ELSE c2"
   let ?cs = "ccomp ?if"
@@ -538,7 +538,7 @@
 
   from While.prems
   show ?case
-  proof (induct n arbitrary: s rule: nat_less_induct)
+  proof (induction n arbitrary: s rule: nat_less_induct)
     case (1 n)
     
     { assume "\<not> bval b s"
@@ -568,7 +568,7 @@
           "?cs \<turnstile> (0,s,stk) \<rightarrow>^m (isize (ccomp ?c0), t, stk')"
           "m < n"
           by (auto simp: exec_n_step [where k=k])
-        with "1.hyps"
+        with "1.IH"
         show ?case by blast
       next
         assume "ccomp c \<noteq> []"
@@ -581,14 +581,14 @@
           by (auto dest: exec_n_split [where i=0, simplified])
         from c
         have "(c,s) \<Rightarrow> s''" and stk: "stk'' = stk"
-          by (auto dest!: While.hyps)
+          by (auto dest!: While.IH)
         moreover
         from rest m k stk
         obtain k' where
           "?cs \<turnstile> (0, s'', stk) \<rightarrow>^k' (isize ?cs, t, stk')"
           "k' < n"
           by (auto simp: exec_n_step [where k=m])
-        with "1.hyps"
+        with "1.IH"
         have "(?c0, s'') \<Rightarrow> t \<and> stk' = stk" by blast
         ultimately
         show ?case using b by blast
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Compiler.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -222,7 +222,7 @@
   "0 \<le> n \<Longrightarrow>
   bcomp b c n \<turnstile>
  (0,s,stk)  \<rightarrow>*  (isize(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
-proof(induct b arbitrary: c n m)
+proof(induction b arbitrary: c n m)
   case Not
   from Not(1)[where c="~c"] Not(2) show ?case by fastforce
 next
@@ -256,17 +256,17 @@
 
 lemma ccomp_bigstep:
   "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk)"
-proof(induct arbitrary: stk rule: big_step_induct)
+proof(induction arbitrary: stk rule: big_step_induct)
   case (Assign x a s)
   show ?case by (fastforce simp:fun_upd_def cong: if_cong)
 next
   case (Semi c1 s1 s2 c2 s3)
   let ?cc1 = "ccomp c1"  let ?cc2 = "ccomp c2"
   have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)"
-    using Semi.hyps(2) by fastforce
+    using Semi.IH(1) by fastforce
   moreover
   have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)"
-    using Semi.hyps(4) by fastforce
+    using Semi.IH(2) by fastforce
   ultimately show ?case by simp (blast intro: exec_trans)
 next
   case (WhileTrue b s1 c s2 s3)
@@ -274,12 +274,12 @@
   let ?cb = "bcomp b False (isize ?cc + 1)"
   let ?cw = "ccomp(WHILE b DO c)"
   have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)"
-    using WhileTrue(1,3) by fastforce
+    using WhileTrue.IH(1) WhileTrue.hyps(1) by fastforce
   moreover
   have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
     by fastforce
   moreover
-  have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue(5))
+  have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue.IH(2))
   ultimately show ?case by(blast intro: exec_trans)
 qed fastforce+
 
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Def_Ass_Sound_Big.thy
--- a/src/HOL/IMP/Def_Ass_Sound_Big.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Def_Ass_Sound_Big.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -12,7 +12,7 @@
 theorem Sound:
   "\<lbrakk> (c,Some s) \<Rightarrow> s';  D A c A';  A \<subseteq> dom s \<rbrakk>
   \<Longrightarrow> \<exists> t. s' = Some t \<and> A' \<subseteq> dom t"
-proof (induct c "Some s" s' arbitrary: s A A' rule:big_step_induct)
+proof (induction c "Some s" s' arbitrary: s A A' rule:big_step_induct)
   case AssignNone thus ?case
     by auto (metis aval_Some option.simps(3) subset_trans)
 next
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Def_Ass_Sound_Small.thy
--- a/src/HOL/IMP/Def_Ass_Sound_Small.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Def_Ass_Sound_Small.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -7,7 +7,7 @@
 
 theorem progress:
   "D (dom s) c A' \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> EX cs'. (c,s) \<rightarrow> cs'"
-proof (induct c arbitrary: s A')
+proof (induction c arbitrary: s A')
   case Assign thus ?case by auto (metis aval_Some small_step.Assign)
 next
   case (If b c1 c2)
@@ -17,13 +17,13 @@
 qed (fastforce intro: small_step.intros)+
 
 lemma D_mono:  "D A c M \<Longrightarrow> A \<subseteq> A' \<Longrightarrow> EX M'. D A' c M' & M <= M'"
-proof (induct c arbitrary: A A' M)
+proof (induction c arbitrary: A A' M)
   case Semi thus ?case by auto (metis D.intros(3))
 next
   case (If b c1 c2)
   then obtain M1 M2 where "vars b \<subseteq> A" "D A c1 M1" "D A c2 M2" "M = M1 \<inter> M2"
     by auto
-  with If.hyps `A \<subseteq> A'` obtain M1' M2'
+  with If.IH `A \<subseteq> A'` obtain M1' M2'
     where "D A' c1 M1'" "D A' c2 M2'" and "M1 \<subseteq> M1'" "M2 \<subseteq> M2'" by metis
   hence "D A' (IF b THEN c1 ELSE c2) (M1' \<inter> M2')" and "M \<subseteq> M1' \<inter> M2'"
     using `vars b \<subseteq> A` `A \<subseteq> A'` `M = M1 \<inter> M2` by(fastforce intro: D.intros)+
@@ -34,7 +34,7 @@
 
 theorem D_preservation:
   "(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c A \<Longrightarrow> EX A'. D (dom s') c' A' & A <= A'"
-proof (induct arbitrary: A rule: small_step_induct)
+proof (induction arbitrary: A rule: small_step_induct)
   case (While b c s)
   then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
   moreover
@@ -49,7 +49,7 @@
 theorem D_sound:
   "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A' \<Longrightarrow> c' \<noteq> SKIP
    \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
-apply(induct arbitrary: A' rule:star_induct)
+apply(induction arbitrary: A' rule:star_induct)
 apply (metis progress)
 by (metis D_preservation)
 
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Denotation.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -32,7 +32,7 @@
 text{* Equivalence of denotational and big-step semantics: *}
 
 lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)"
-apply (induct rule: big_step_induct)
+apply (induction rule: big_step_induct)
 apply auto
 (* while *)
 apply (unfold Gamma_def)
@@ -43,7 +43,7 @@
 done
 
 lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t"
-apply (induct c arbitrary: s t)
+apply (induction c arbitrary: s t)
 apply auto 
 apply blast
 (* while *)
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Fold.thy
--- a/src/HOL/IMP/Fold.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Fold.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -81,7 +81,7 @@
 
 lemma defs_restrict:
   "defs c t |` (- lnames c) = t |` (- lnames c)"
-proof (induct c arbitrary: t)
+proof (induction c arbitrary: t)
   case (Semi c1 c2)
   hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
     by simp
@@ -114,7 +114,7 @@
 
 lemma big_step_pres_approx:
   "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (defs c t) s'"
-proof (induct arbitrary: t rule: big_step_induct)
+proof (induction arbitrary: t rule: big_step_induct)
   case Skip thus ?case by simp
 next
   case Assign
@@ -122,8 +122,8 @@
     by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
 next
   case (Semi c1 s1 s2 c2 s3)
-  have "approx (defs c1 t) s2" by (rule Semi(2) [OF Semi.prems])
-  hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi(4))
+  have "approx (defs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems])
+  hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi.IH(2))
   thus ?case by simp
 next
   case (IfTrue b s c1 s')
@@ -151,7 +151,7 @@
 
 lemma big_step_pres_approx_restrict:
   "(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lnames c)) s \<Longrightarrow> approx (t |` (-lnames c)) s'"
-proof (induct arbitrary: t rule: big_step_induct)
+proof (induction arbitrary: t rule: big_step_induct)
   case Assign
   thus ?case by (clarsimp simp: approx_def)
 next
@@ -190,7 +190,7 @@
 
 lemma approx_eq:
   "approx t \<Turnstile> c \<sim> fold c t"
-proof (induct c arbitrary: t)
+proof (induction c arbitrary: t)
   case SKIP show ?case by simp
 next
   case Assign
@@ -292,7 +292,7 @@
 
 lemma bdefs_restrict:
   "bdefs c t |` (- lnames c) = t |` (- lnames c)"
-proof (induct c arbitrary: t)
+proof (induction c arbitrary: t)
   case (Semi c1 c2)
   hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
     by simp
@@ -327,7 +327,7 @@
 
 lemma big_step_pres_approx_b:
   "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (bdefs c t) s'" 
-proof (induct arbitrary: t rule: big_step_induct)
+proof (induction arbitrary: t rule: big_step_induct)
   case Skip thus ?case by simp
 next
   case Assign
@@ -335,8 +335,8 @@
     by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
 next
   case (Semi c1 s1 s2 c2 s3)
-  have "approx (bdefs c1 t) s2" by (rule Semi(2) [OF Semi.prems])
-  hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi(4))
+  have "approx (bdefs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems])
+  hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi.IH(2))
   thus ?case by simp
 next
   case (IfTrue b s c1 s')
@@ -371,7 +371,7 @@
 
 lemma bfold_equiv: 
   "approx t \<Turnstile> c \<sim> bfold c t"
-proof (induct c arbitrary: t)
+proof (induction c arbitrary: t)
   case SKIP show ?case by simp
 next
   case Assign
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/HoareT.thy
--- a/src/HOL/IMP/HoareT.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/HoareT.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -88,7 +88,7 @@
   proof
     fix s
     show "P s \<longrightarrow> (\<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t)"
-    proof(induct "f s" arbitrary: s rule: less_induct)
+    proof(induction "f s" arbitrary: s rule: less_induct)
       case (less n)
       thus ?case by (metis While(2) WhileFalse WhileTrue)
     qed
@@ -137,7 +137,7 @@
 text{* The relation is in fact a function: *}
 
 lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'"
-proof(induct arbitrary: n' rule:Its.induct)
+proof(induction arbitrary: n' rule:Its.induct)
 (* new release:
   case Its_0 thus ?case by(metis Its.cases)
 next
@@ -160,7 +160,7 @@
 text{* For all terminating loops, @{const Its} yields a result: *}
 
 lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n"
-proof(induct "WHILE b DO c" s t rule: big_step_induct)
+proof(induction "WHILE b DO c" s t rule: big_step_induct)
   case WhileFalse thus ?case by (metis Its_0)
 next
   case WhileTrue thus ?case by (metis Its_Suc)
@@ -179,7 +179,7 @@
 by (metis its_def WHILE_Its Its.intros(2) Its_fun the_equality)
 
 lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
-proof (induct c arbitrary: Q)
+proof (induction c arbitrary: Q)
   case SKIP show ?case by simp (blast intro:hoaret.Skip)
 next
   case Assign show ?case by simp (blast intro:hoaret.Assign)
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Hoare_Examples.thy
--- a/src/HOL/IMP/Hoare_Examples.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Hoare_Examples.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -25,7 +25,7 @@
   
 lemma while_sum:
   "(w n, s) \<Rightarrow> t \<Longrightarrow> t ''x'' = s ''x'' + \<Sum> {s ''y'' + 1 .. n}"
-apply(induct "w n" s t rule: big_step_induct)
+apply(induction "w n" s t rule: big_step_induct)
 apply(auto simp add: setsum_head_plus_1)
 done
 
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Hoare_Sound_Complete.thy
--- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -9,11 +9,11 @@
 "\<Turnstile> {P}c{Q} = (\<forall>s t. (c,s) \<Rightarrow> t  \<longrightarrow>  P s \<longrightarrow>  Q t)"
 
 lemma hoare_sound: "\<turnstile> {P}c{Q}  \<Longrightarrow>  \<Turnstile> {P}c{Q}"
-proof(induct rule: hoare.induct)
+proof(induction rule: hoare.induct)
   case (While P b c)
   { fix s t
     have "(WHILE b DO c,s) \<Rightarrow> t  \<Longrightarrow>  P s \<longrightarrow> P t \<and> \<not> bval b t"
-    proof(induct "WHILE b DO c" s t rule: big_step_induct)
+    proof(induction "WHILE b DO c" s t rule: big_step_induct)
       case WhileFalse thus ?case by blast
     next
       case WhileTrue thus ?case
@@ -59,7 +59,7 @@
 subsection "Completeness"
 
 lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"
-proof(induct c arbitrary: Q)
+proof(induction c arbitrary: Q)
   case Semi thus ?case by(auto intro: Semi)
 next
   case (If b c1 c2)
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Live.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -44,17 +44,17 @@
 theorem L_sound:
   "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
   \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
-proof (induct arbitrary: X t rule: big_step_induct)
+proof (induction arbitrary: X t rule: big_step_induct)
   case Skip then show ?case by auto
 next
   case Assign then show ?case
     by (auto simp: ball_Un)
 next
   case (Semi c1 s1 s2 c2 s3 X t1)
-  from Semi(2,5) obtain t2 where
+  from Semi.IH(1) Semi.prems obtain t2 where
     t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
     by simp blast
-  from Semi(4)[OF s2t2] obtain t3 where
+  from Semi.IH(2)[OF s2t2] obtain t3 where
     t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
     by auto
   show ?case using t12 t23 s3t3 by auto
@@ -83,9 +83,9 @@
     by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
   have "s1 = t1 on L c (L ?w X)" using  L_While_subset WhileTrue.prems
     by (blast)
-  from WhileTrue(3)[OF this] obtain t2 where
+  from WhileTrue.IH(1)[OF this] obtain t2 where
     "(c, t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
-  from WhileTrue(5)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
+  from WhileTrue.IH(2)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
     by auto
   with `bval b t1` `(c, t1) \<Rightarrow> t2` show ?case by auto
 qed
@@ -108,17 +108,17 @@
 theorem bury_sound:
   "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
   \<exists> t'. (bury c X,t) \<Rightarrow> t' & s' = t' on X"
-proof (induct arbitrary: X t rule: big_step_induct)
+proof (induction arbitrary: X t rule: big_step_induct)
   case Skip then show ?case by auto
 next
   case Assign then show ?case
     by (auto simp: ball_Un)
 next
   case (Semi c1 s1 s2 c2 s3 X t1)
-  from Semi(2,5) obtain t2 where
+  from Semi.IH(1) Semi.prems obtain t2 where
     t12: "(bury c1 (L c2 X), t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
     by simp blast
-  from Semi(4)[OF s2t2] obtain t3 where
+  from Semi.IH(2)[OF s2t2] obtain t3 where
     t23: "(bury c2 X, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
     by auto
   show ?case using t12 t23 s3t3 by auto
@@ -147,9 +147,9 @@
     by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
   have "s1 = t1 on L c (L ?w X)"
     using L_While_subset WhileTrue.prems by blast
-  from WhileTrue(3)[OF this] obtain t2 where
+  from WhileTrue.IH(1)[OF this] obtain t2 where
     "(bury c (L ?w X), t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
-  from WhileTrue(5)[OF this(2)] obtain t3
+  from WhileTrue.IH(2)[OF this(2)] obtain t3
     where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X"
     by auto
   with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto
@@ -184,7 +184,7 @@
 theorem bury_sound2:
   "(bury c X,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
   \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
-proof (induct "bury c X" s s' arbitrary: c X t rule: big_step_induct)
+proof (induction "bury c X" s s' arbitrary: c X t rule: big_step_induct)
   case Skip then show ?case by auto
 next
   case Assign then show ?case
@@ -193,9 +193,10 @@
   case (Semi bc1 s1 s2 bc2 s3 c X t1)
   then obtain c1 c2 where c: "c = c1;c2"
     and bc2: "bc2 = bury c2 X" and bc1: "bc1 = bury c1 (L c2 X)" by auto
-  from Semi(2)[OF bc1, of t1] Semi.prems c obtain t2 where
+  note IH = Semi.hyps(2,4)
+  from IH(1)[OF bc1, of t1] Semi.prems c obtain t2 where
     t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X" by auto
-  from Semi(4)[OF bc2 s2t2] obtain t3 where
+  from IH(2)[OF bc2 s2t2] obtain t3 where
     t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
     by auto
   show ?case using c t12 t23 s3t3 by auto
@@ -205,7 +206,8 @@
     and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
   have "s = t on vars b" "s = t on L c1 X" using IfTrue.prems c by auto
   from bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
-  from IfTrue(3)[OF bc1 `s = t on L c1 X`] obtain t' where
+  note IH = IfTrue.hyps(3)
+  from IH[OF bc1 `s = t on L c1 X`] obtain t' where
     "(c1, t) \<Rightarrow> t'" "s' =t' on X" by auto
   thus ?case using c `bval b t` by auto
 next
@@ -214,7 +216,8 @@
     and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
   have "s = t on vars b" "s = t on L c2 X" using IfFalse.prems c by auto
   from bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
-  from IfFalse(3)[OF bc2 `s = t on L c2 X`] obtain t' where
+  note IH = IfFalse.hyps(3)
+  from IH[OF bc2 `s = t on L c2 X`] obtain t' where
     "(c2, t) \<Rightarrow> t'" "s' =t' on X" by auto
   thus ?case using c `~bval b t` by auto
 next
@@ -228,11 +231,12 @@
   let ?w = "WHILE b DO c'"
   from `bval b s1` WhileTrue.prems c have "bval b t1"
     by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
+  note IH = WhileTrue.hyps(3,5)
   have "s1 = t1 on L c' (L ?w X)"
     using L_While_subset WhileTrue.prems c by blast
-  with WhileTrue(3)[OF bc', of t1] obtain t2 where
+  with IH(1)[OF bc', of t1] obtain t2 where
     "(c', t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
-  from WhileTrue(5)[OF WhileTrue(6), of t2] c this(2) obtain t3
+  from IH(2)[OF WhileTrue.hyps(6), of t2] c this(2) obtain t3
     where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
     by auto
   with `bval b t1` `(c', t1) \<Rightarrow> t2` c show ?case by auto
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Poly_Types.thy
--- a/src/HOL/IMP/Poly_Types.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Poly_Types.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -45,12 +45,12 @@
 subsection{* Typing is Preserved by Substitution *}
 
 lemma subst_atyping: "E \<turnstile>p a : t \<Longrightarrow> tsubst S \<circ> E \<turnstile>p a : tsubst S t"
-apply(induct rule: atyping.induct)
+apply(induction rule: atyping.induct)
 apply(auto intro: atyping.intros)
 done
 
 lemma subst_btyping: "E \<turnstile>p (b::bexp) \<Longrightarrow> tsubst S \<circ> E \<turnstile>p b"
-apply(induct rule: btyping.induct)
+apply(induction rule: btyping.induct)
 apply(auto intro: btyping.intros)
 apply(drule subst_atyping[where S=S])
 apply(drule subst_atyping[where S=S])
@@ -58,7 +58,7 @@
 done
 
 lemma subst_ctyping: "E \<turnstile>p (c::com) \<Longrightarrow> tsubst S \<circ> E \<turnstile>p c"
-apply(induct rule: ctyping.induct)
+apply(induction rule: ctyping.induct)
 apply(auto intro: ctyping.intros)
 apply(drule subst_atyping[where S=S])
 apply(simp add: o_def ctyping.intros)
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Sec_Typing.thy
--- a/src/HOL/IMP/Sec_Typing.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Sec_Typing.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -30,7 +30,7 @@
 text{* An important property: anti-monotonicity. *}
 
 lemma anti_mono: "\<lbrakk> l \<turnstile> c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile> c"
-apply(induct arbitrary: l' rule: sec_type.induct)
+apply(induction arbitrary: l' rule: sec_type.induct)
 apply (metis sec_type.intros(1))
 apply (metis le_trans sec_type.intros(2))
 apply (metis sec_type.intros(3))
@@ -39,7 +39,7 @@
 done
 
 lemma confinement: "\<lbrakk> (c,s) \<Rightarrow> t;  l \<turnstile> c \<rbrakk> \<Longrightarrow> s = t (< l)"
-proof(induct rule: big_step_induct)
+proof(induction rule: big_step_induct)
   case Skip thus ?case by simp
 next
   case Assign thus ?case by auto
@@ -49,12 +49,12 @@
   case (IfTrue b s c1)
   hence "max (sec_bexp b) l \<turnstile> c1" by auto
   hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
-  thus ?case using IfTrue.hyps by metis
+  thus ?case using IfTrue.IH by metis
 next
   case (IfFalse b s c2)
   hence "max (sec_bexp b) l \<turnstile> c2" by auto
   hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
-  thus ?case using IfFalse.hyps by metis
+  thus ?case using IfFalse.IH by metis
 next
   case WhileFalse thus ?case by auto
 next
@@ -68,7 +68,7 @@
 theorem noninterference:
   "\<lbrakk> (c,s) \<Rightarrow> s'; (c,t) \<Rightarrow> t';  0 \<turnstile> c;  s = t (\<le> l) \<rbrakk>
    \<Longrightarrow> s' = t' (\<le> l)"
-proof(induct arbitrary: t t' rule: big_step_induct)
+proof(induction arbitrary: t t' rule: big_step_induct)
   case Skip thus ?case by auto
 next
   case (Assign x a s)
@@ -94,7 +94,7 @@
     assume "sec_bexp b \<le> l"
     hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
     hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le)
-    with IfTrue.hyps(3) IfTrue.prems(1,3) `sec_bexp b \<turnstile> c1`  anti_mono
+    with IfTrue.IH IfTrue.prems(1,3) `sec_bexp b \<turnstile> c1`  anti_mono
     show ?thesis by auto
   next
     assume "\<not> sec_bexp b \<le> l"
@@ -115,7 +115,7 @@
     assume "sec_bexp b \<le> l"
     hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
     hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
-    with IfFalse.hyps(3) IfFalse.prems(1,3) `sec_bexp b \<turnstile> c2` anti_mono
+    with IfFalse.IH IfFalse.prems(1,3) `sec_bexp b \<turnstile> c2` anti_mono
     show ?thesis by auto
   next
     assume "\<not> sec_bexp b \<le> l"
@@ -157,14 +157,14 @@
       using `bval b s1` by(simp add: bval_eq_if_eq_le)
     then obtain t2 where "(c,t1) \<Rightarrow> t2" "(?w,t2) \<Rightarrow> t3"
       using `(?w,t1) \<Rightarrow> t3` by auto
-    from WhileTrue.hyps(5)[OF `(?w,t2) \<Rightarrow> t3` `0 \<turnstile> ?w`
-      WhileTrue.hyps(3)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec_bexp b \<turnstile> c`]
+    from WhileTrue.IH(2)[OF `(?w,t2) \<Rightarrow> t3` `0 \<turnstile> ?w`
+      WhileTrue.IH(1)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec_bexp b \<turnstile> c`]
         `s1 = t1 (\<le> l)`]]
     show ?thesis by simp
   next
     assume "\<not> sec_bexp b \<le> l"
     have 1: "sec_bexp b \<turnstile> ?w" by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c`)
-    from confinement[OF big_step.WhileTrue[OF WhileTrue(1,2,4)] 1] `\<not> sec_bexp b \<le> l`
+    from confinement[OF big_step.WhileTrue[OF WhileTrue.hyps] 1] `\<not> sec_bexp b \<le> l`
     have "s1 = s3 (\<le> l)" by auto
     moreover
     from confinement[OF WhileTrue.prems(1) 1] `\<not> sec_bexp b \<le> l`
@@ -196,7 +196,7 @@
   "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
 
 lemma sec_type_sec_type': "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
-apply(induct rule: sec_type.induct)
+apply(induction rule: sec_type.induct)
 apply (metis Skip')
 apply (metis Assign')
 apply (metis Semi')
@@ -205,7 +205,7 @@
 
 
 lemma sec_type'_sec_type: "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
-apply(induct rule: sec_type'.induct)
+apply(induction rule: sec_type'.induct)
 apply (metis Skip)
 apply (metis Assign)
 apply (metis Semi)
@@ -230,7 +230,7 @@
 
 
 lemma sec_type2_sec_type': "\<turnstile> c : l \<Longrightarrow> l \<turnstile>' c"
-apply(induct rule: sec_type2.induct)
+apply(induction rule: sec_type2.induct)
 apply (metis Skip')
 apply (metis Assign' eq_imp_le)
 apply (metis Semi' anti_mono' min_max.inf.commute min_max.inf_le2)
@@ -238,7 +238,7 @@
 by (metis While')
 
 lemma sec_type'_sec_type2: "l \<turnstile>' c \<Longrightarrow> \<exists> l' \<ge> l. \<turnstile> c : l'"
-apply(induct rule: sec_type'.induct)
+apply(induction rule: sec_type'.induct)
 apply (metis Skip2 le_refl)
 apply (metis Assign2)
 apply (metis Semi2 min_max.inf_greatest)
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Sec_TypingT.thy
--- a/src/HOL/IMP/Sec_TypingT.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Sec_TypingT.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -23,7 +23,7 @@
 
 
 lemma anti_mono: "l \<turnstile> c \<Longrightarrow> l' \<le> l \<Longrightarrow> l' \<turnstile> c"
-apply(induct arbitrary: l' rule: sec_type.induct)
+apply(induction arbitrary: l' rule: sec_type.induct)
 apply (metis sec_type.intros(1))
 apply (metis le_trans sec_type.intros(2))
 apply (metis sec_type.intros(3))
@@ -32,7 +32,7 @@
 
 
 lemma confinement: "(c,s) \<Rightarrow> t \<Longrightarrow> l \<turnstile> c \<Longrightarrow> s = t (< l)"
-proof(induct rule: big_step_induct)
+proof(induction rule: big_step_induct)
   case Skip thus ?case by simp
 next
   case Assign thus ?case by auto
@@ -42,12 +42,12 @@
   case (IfTrue b s c1)
   hence "max (sec_bexp b) l \<turnstile> c1" by auto
   hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
-  thus ?case using IfTrue.hyps by metis
+  thus ?case using IfTrue.IH by metis
 next
   case (IfFalse b s c2)
   hence "max (sec_bexp b) l \<turnstile> c2" by auto
   hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
-  thus ?case using IfFalse.hyps by metis
+  thus ?case using IfFalse.IH by metis
 next
   case WhileFalse thus ?case by auto
 next
@@ -57,7 +57,7 @@
 qed
 
 lemma termi_if_non0: "l \<turnstile> c \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> \<exists> t. (c,s) \<Rightarrow> t"
-apply(induct arbitrary: s rule: sec_type.induct)
+apply(induction arbitrary: s rule: sec_type.induct)
 apply (metis big_step.Skip)
 apply (metis big_step.Assign)
 apply (metis big_step.Semi)
@@ -67,7 +67,7 @@
 
 theorem noninterference: "(c,s) \<Rightarrow> s' \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow>  s = t (\<le> l)
   \<Longrightarrow> \<exists> t'. (c,t) \<Rightarrow> t' \<and> s' = t' (\<le> l)"
-proof(induct arbitrary: t rule: big_step_induct)
+proof(induction arbitrary: t rule: big_step_induct)
   case Skip thus ?case by auto
 next
   case (Assign x a s)
@@ -152,9 +152,9 @@
   let ?w = "WHILE b DO c"
   from `0 \<turnstile> ?w` have [simp]: "sec_bexp b = 0" by auto
   have "0 \<turnstile> c" using WhileTrue.prems(1) by auto
-  from WhileTrue(3)[OF this WhileTrue.prems(2)]
+  from WhileTrue.IH(1)[OF this WhileTrue.prems(2)]
   obtain t'' where "(c,t) \<Rightarrow> t''" and "s'' = t'' (\<le>l)" by blast
-  from WhileTrue(5)[OF `0 \<turnstile> ?w` this(2)]
+  from WhileTrue.IH(2)[OF `0 \<turnstile> ?w` this(2)]
   obtain t' where "(?w,t'') \<Rightarrow> t'" and "s' = t' (\<le>l)" by blast
   from `bval b s` have "bval b t"
     using bval_eq_if_eq_le[OF `s = t (\<le>l)`] by auto
@@ -185,7 +185,7 @@
   "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
 
 lemma "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
-apply(induct rule: sec_type.induct)
+apply(induction rule: sec_type.induct)
 apply (metis Skip')
 apply (metis Assign')
 apply (metis Semi')
@@ -194,7 +194,7 @@
 
 
 lemma "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
-apply(induct rule: sec_type'.induct)
+apply(induction rule: sec_type'.induct)
 apply (metis Skip)
 apply (metis Assign)
 apply (metis Semi)
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Sem_Equiv.thy
--- a/src/HOL/IMP/Sem_Equiv.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Sem_Equiv.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -83,10 +83,9 @@
          P s \<Longrightarrow> 
          d = WHILE b DO c \<Longrightarrow> 
          (WHILE b' DO c', s) \<Rightarrow> s'"  
-proof (induct rule: big_step_induct)
+proof (induction rule: big_step_induct)
   case (WhileTrue b s1 c s2 s3)
-  note IH = WhileTrue.hyps(5) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
-  
+  note IH = WhileTrue.IH(2) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
   from WhileTrue.prems
   have "P \<Turnstile> b <\<sim>> b'" by simp
   with `bval b s1` `P s1`
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Small_Step.thy
--- a/src/HOL/IMP/Small_Step.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Small_Step.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -71,7 +71,7 @@
 text{* A simple property: *}
 lemma deterministic:
   "cs \<rightarrow> cs' \<Longrightarrow> cs \<rightarrow> cs'' \<Longrightarrow> cs'' = cs'"
-apply(induct arbitrary: cs'' rule: small_step.induct)
+apply(induction arbitrary: cs'' rule: small_step.induct)
 apply blast+
 done
 
@@ -79,7 +79,7 @@
 subsection "Equivalence with big-step semantics"
 
 lemma star_semi2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')"
-proof(induct rule: star_induct)
+proof(induction rule: star_induct)
   case refl thus ?case by simp
 next
   case step
@@ -98,7 +98,7 @@
 
 lemma big_to_small:
   "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
-proof (induct rule: big_step.induct)
+proof (induction rule: big_step.induct)
   fix s show "(SKIP,s) \<rightarrow>* (SKIP,s)" by simp
 next
   fix x a s show "(x ::= a,s) \<rightarrow>* (SKIP, s(x := aval a s))" by auto
@@ -140,7 +140,7 @@
 
 text{* Each case of the induction can be proved automatically: *}
 lemma  "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)"
-proof (induct rule: big_step.induct)
+proof (induction rule: big_step.induct)
   case Skip show ?case by blast
 next
   case Assign show ?case by blast
@@ -161,13 +161,13 @@
 
 lemma small1_big_continue:
   "cs \<rightarrow> cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
-apply (induct arbitrary: t rule: small_step.induct)
+apply (induction arbitrary: t rule: small_step.induct)
 apply auto
 done
 
 lemma small_big_continue:
   "cs \<rightarrow>* cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
-apply (induct rule: star.induct)
+apply (induction rule: star.induct)
 apply (auto intro: small1_big_continue)
 done
 
@@ -188,7 +188,7 @@
 
 lemma finalD: "final (c,s) \<Longrightarrow> c = SKIP"
 apply(simp add: final_def)
-apply(induct c)
+apply(induction c)
 apply blast+
 done
 
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Star.thy
--- a/src/HOL/IMP/Star.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Star.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -9,7 +9,7 @@
 
 lemma star_trans:
   "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
-proof(induct rule: star.induct)
+proof(induction rule: star.induct)
   case refl thus ?case .
 next
   case step thus ?case by (metis star.step)
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Types.thy
--- a/src/HOL/IMP/Types.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Types.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -119,28 +119,28 @@
 
 lemma apreservation:
   "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> taval a s v \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> type v = \<tau>"
-apply(induct arbitrary: v rule: atyping.induct)
+apply(induction arbitrary: v rule: atyping.induct)
 apply (fastforce simp: styping_def)+
 done
 
 lemma aprogress: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. taval a s v"
-proof(induct rule: atyping.induct)
+proof(induction rule: atyping.induct)
   case (Plus_ty \<Gamma> a1 t a2)
   then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast
   show ?case
   proof (cases v1)
     case Iv
-    with Plus_ty(1,3,5) v show ?thesis
+    with Plus_ty v show ?thesis
       by(fastforce intro: taval.intros(4) dest!: apreservation)
   next
     case Rv
-    with Plus_ty(1,3,5) v show ?thesis
+    with Plus_ty v show ?thesis
       by(fastforce intro: taval.intros(5) dest!: apreservation)
   qed
 qed (auto intro: taval.intros)
 
 lemma bprogress: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. tbval b s v"
-proof(induct rule: btyping.induct)
+proof(induction rule: btyping.induct)
   case (Less_ty \<Gamma> a1 t a2)
   then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2"
     by (metis aprogress)
@@ -158,7 +158,7 @@
 
 theorem progress:
   "\<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> \<exists>cs'. (c,s) \<rightarrow> cs'"
-proof(induct rule: ctyping.induct)
+proof(induction rule: ctyping.induct)
   case Skip_ty thus ?case by simp
 next
   case Assign_ty 
@@ -182,7 +182,7 @@
 
 theorem styping_preservation:
   "(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<Gamma> \<turnstile> s'"
-proof(induct rule: small_step_induct)
+proof(induction rule: small_step_induct)
   case Assign thus ?case
     by (auto simp: styping_def) (metis Assign(1,3) apreservation)
 qed auto
@@ -197,7 +197,7 @@
 theorem type_sound:
   "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c' \<noteq> SKIP
    \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
-apply(induct rule:star_induct)
+apply(induction rule:star_induct)
 apply (metis progress)
 by (metis styping_preservation ctyping_preservation)
 
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/VC.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -49,14 +49,14 @@
 subsection "Soundness"
 
 lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} astrip c {Q}"
-proof(induct c arbitrary: Q)
+proof(induction c arbitrary: Q)
   case (Awhile b I c)
   show ?case
   proof(simp, rule While')
     from `\<forall>s. vc (Awhile b I c) Q s`
     have vc: "\<forall>s. vc c I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and
          pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre c I s" by simp_all
-    have "\<turnstile> {pre c I} astrip c {I}" by(rule Awhile.hyps[OF vc])
+    have "\<turnstile> {pre c I} astrip c {I}" by(rule Awhile.IH[OF vc])
     with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} astrip c {I}"
       by(rule strengthen_pre)
     show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ)
@@ -72,20 +72,20 @@
 
 lemma pre_mono:
   "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre c P s \<Longrightarrow> pre c P' s"
-proof (induct c arbitrary: P P' s)
+proof (induction c arbitrary: P P' s)
   case Asemi thus ?case by simp metis
 qed simp_all
 
 lemma vc_mono:
   "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc c P s \<Longrightarrow> vc c P' s"
-proof(induct c arbitrary: P P')
+proof(induction c arbitrary: P P')
   case Asemi thus ?case by simp (metis pre_mono)
 qed simp_all
 
 lemma vc_complete:
  "\<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)"
   (is "_ \<Longrightarrow> \<exists>c'. ?G P c Q c'")
-proof (induct rule: hoare.induct)
+proof (induction rule: hoare.induct)
   case Skip
   show ?case (is "\<exists>ac. ?C ac")
   proof show "?C Askip" by simp qed
@@ -95,8 +95,8 @@
   proof show "?C(Aassign x a)" by simp qed
 next
   case (Semi P c1 Q c2 R)
-  from Semi.hyps obtain ac1 where ih1: "?G P c1 Q ac1" by blast
-  from Semi.hyps obtain ac2 where ih2: "?G Q c2 R ac2" by blast
+  from Semi.IH obtain ac1 where ih1: "?G P c1 Q ac1" by blast
+  from Semi.IH obtain ac2 where ih2: "?G Q c2 R ac2" by blast
   show ?case (is "\<exists>ac. ?C ac")
   proof
     show "?C(Asemi ac1 ac2)"
@@ -104,9 +104,9 @@
   qed
 next
   case (If P b c1 Q c2)
-  from If.hyps obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1"
+  from If.IH obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1"
     by blast
-  from If.hyps obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2"
+  from If.IH obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2"
     by blast
   show ?case (is "\<exists>ac. ?C ac")
   proof
@@ -114,7 +114,7 @@
   qed
 next
   case (While P b c)
-  from While.hyps obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast
+  from While.IH obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast
   show ?case (is "\<exists>ac. ?C ac")
   proof show "?C(Awhile b P ac)" using ih by simp qed
 next
diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Vars.thy
--- a/src/HOL/IMP/Vars.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/Vars.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -59,13 +59,13 @@
 
 lemma aval_eq_if_eq_on_vars[simp]:
   "s\<^isub>1 = s\<^isub>2 on vars a \<Longrightarrow> aval a s\<^isub>1 = aval a s\<^isub>2"
-apply(induct a)
+apply(induction a)
 apply simp_all
 done
 
 lemma bval_eq_if_eq_on_vars:
   "s\<^isub>1 = s\<^isub>2 on vars b \<Longrightarrow> bval b s\<^isub>1 = bval b s\<^isub>2"
-proof(induct b)
+proof(induction b)
   case (Less a1 a2)
   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
   thus ?case by simp