# HG changeset patch
# User huffman
# Date 1316612494 25200
# Node ID 34e5fc15ea0231bc08e8ee0dd83f67f4b7061543
# Parent  5a4d62f9e88de2c37cc27fd8cdaf55b441ee2dd7# Parent  77c3e74bd954a8d6ea3d35fbbbfc6cff2284b64d
merged

diff -r 5a4d62f9e88d -r 34e5fc15ea02 NEWS
--- a/NEWS	Tue Sep 20 11:02:41 2011 -0700
+++ b/NEWS	Wed Sep 21 06:41:34 2011 -0700
@@ -76,6 +76,11 @@
 
 *** HOL ***
 
+* New proof method "induction" that gives induction hypotheses the name IH,
+thus distinguishing them from further hypotheses that come from rule
+induction.  The latter are still called "hyps".  Method "induction" is a thin
+wrapper around "induct" and follows the same syntax.
+
 * Class bot and top require underlying partial order rather than
 preorder: uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
 
@@ -91,8 +96,7 @@
 Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,
 INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,
 INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, INF_subset,
-UNION_eq_Union_image, Union_def, UN_singleton, UN_eq have been
-discarded.
+UNION_eq_Union_image, Union_def, UN_eq have been discarded.
 
 More consistent and comprehensive names:
 
diff -r 5a4d62f9e88d -r 34e5fc15ea02 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/doc-src/IsarRef/Thy/Proof.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -1259,10 +1259,12 @@
   \begin{matharray}{rcl}
     @{method_def cases} & : & @{text method} \\
     @{method_def induct} & : & @{text method} \\
+    @{method_def induction} & : & @{text method} \\
     @{method_def coinduct} & : & @{text method} \\
   \end{matharray}
 
-  The @{method cases}, @{method induct}, and @{method coinduct}
+  The @{method cases}, @{method induct}, @{method induction},
+  and @{method coinduct}
   methods provide a uniform interface to common proof techniques over
   datatypes, inductive predicates (or sets), recursive functions etc.
   The corresponding rules may be specified and instantiated in a
@@ -1277,11 +1279,15 @@
   and parameters separately).  This avoids cumbersome encoding of
   ``strengthened'' inductive statements within the object-logic.
 
+  Method @{method induction} differs from @{method induct} only in
+  the names of the facts in the local context invoked by the @{command "case"}
+  command.
+
   @{rail "
     @@{method cases} ('(' 'no_simp' ')')? \\
       (@{syntax insts} * @'and') rule?
     ;
-    @@{method induct} ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
+    (@@{method induct} | @@{method induction}) ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
     ;
     @@{method coinduct} @{syntax insts} taking rule?
     ;
@@ -1325,8 +1331,9 @@
   "(no_simp)"} option can be used to disable pre-simplification of
   cases (see the description of @{method induct} below for details).
 
-  \item @{method induct}~@{text "insts R"} is analogous to the
-  @{method cases} method, but refers to induction rules, which are
+  \item @{method induct}~@{text "insts R"} and
+  @{method induction}~@{text "insts R"} are analogous to the
+  @{method cases} method, but refer to induction rules, which are
   determined as follows:
 
   \medskip
@@ -1437,13 +1444,20 @@
   and definitions effectively participate in the inductive rephrasing
   of the original statement.
 
-  In induction proofs, local assumptions introduced by cases are split
+  In @{method induct} proofs, local assumptions introduced by cases are split
   into two different kinds: @{text hyps} stemming from the rule and
   @{text prems} from the goal statement.  This is reflected in the
   extracted cases accordingly, so invoking ``@{command "case"}~@{text
   c}'' will provide separate facts @{text c.hyps} and @{text c.prems},
   as well as fact @{text c} to hold the all-inclusive list.
 
+  In @{method induction} proofs, local assumptions introduced by cases are
+  split into three different kinds: @{text IH}, the induction hypotheses,
+  @{text hyps}, the remaining hypotheses stemming from the rule, and
+  @{text prems}, the assumptions from the goal statement. The names are
+  @{text c.IH}, @{text c.hyps} and @{text c.prems}, as above.
+
+
   \medskip Facts presented to either method are consumed according to
   the number of ``major premises'' of the rule involved, which is
   usually 0 for plain cases and induction rules of datatypes etc.\ and
diff -r 5a4d62f9e88d -r 34e5fc15ea02 doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Tue Sep 20 11:02:41 2011 -0700
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Wed Sep 21 06:41:34 2011 -0700
@@ -1700,10 +1700,12 @@
 \begin{matharray}{rcl}
     \indexdef{}{method}{cases}\hypertarget{method.cases}{\hyperlink{method.cases}{\mbox{\isa{cases}}}} & : & \isa{method} \\
     \indexdef{}{method}{induct}\hypertarget{method.induct}{\hyperlink{method.induct}{\mbox{\isa{induct}}}} & : & \isa{method} \\
+    \indexdef{}{method}{induction}\hypertarget{method.induction}{\hyperlink{method.induction}{\mbox{\isa{induction}}}} & : & \isa{method} \\
     \indexdef{}{method}{coinduct}\hypertarget{method.coinduct}{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}} & : & \isa{method} \\
   \end{matharray}
 
-  The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}
+  The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, \hyperlink{method.induction}{\mbox{\isa{induction}}},
+  and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}
   methods provide a uniform interface to common proof techniques over
   datatypes, inductive predicates (or sets), recursive functions etc.
   The corresponding rules may be specified and instantiated in a
@@ -1718,6 +1720,10 @@
   and parameters separately).  This avoids cumbersome encoding of
   ``strengthened'' inductive statements within the object-logic.
 
+  Method \hyperlink{method.induction}{\mbox{\isa{induction}}} differs from \hyperlink{method.induct}{\mbox{\isa{induct}}} only in
+  the names of the facts in the local context invoked by the \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}
+  command.
+
   \begin{railoutput}
 \rail@begin{6}{}
 \rail@term{\hyperlink{method.cases}{\mbox{\isa{cases}}}}[]
@@ -1742,7 +1748,11 @@
 \rail@endbar
 \rail@end
 \rail@begin{6}{}
+\rail@bar
 \rail@term{\hyperlink{method.induct}{\mbox{\isa{induct}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{method.induction}{\mbox{\isa{induction}}}}[]
+\rail@endbar
 \rail@bar
 \rail@nextbar{1}
 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
@@ -1872,8 +1882,9 @@
   last premise (it is usually the same for all cases).  The \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option can be used to disable pre-simplification of
   cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details).
 
-  \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} is analogous to the
-  \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are
+  \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} and
+  \hyperlink{method.induction}{\mbox{\isa{induction}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} are analogous to the
+  \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refer to induction rules, which are
   determined as follows:
 
   \medskip
@@ -1979,12 +1990,19 @@
   and definitions effectively participate in the inductive rephrasing
   of the original statement.
 
-  In induction proofs, local assumptions introduced by cases are split
+  In \hyperlink{method.induct}{\mbox{\isa{induct}}} proofs, local assumptions introduced by cases are split
   into two different kinds: \isa{hyps} stemming from the rule and
   \isa{prems} from the goal statement.  This is reflected in the
   extracted cases accordingly, so invoking ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' will provide separate facts \isa{c{\isaliteral{2E}{\isachardot}}hyps} and \isa{c{\isaliteral{2E}{\isachardot}}prems},
   as well as fact \isa{c} to hold the all-inclusive list.
 
+  In \hyperlink{method.induction}{\mbox{\isa{induction}}} proofs, local assumptions introduced by cases are
+  split into three different kinds: \isa{IH}, the induction hypotheses,
+  \isa{hyps}, the remaining hypotheses stemming from the rule, and
+  \isa{prems}, the assumptions from the goal statement. The names are
+  \isa{c{\isaliteral{2E}{\isachardot}}IH}, \isa{c{\isaliteral{2E}{\isachardot}}hyps} and \isa{c{\isaliteral{2E}{\isachardot}}prems}, as above.
+
+
   \medskip Facts presented to either method are consumed according to
   the number of ``major premises'' of the rule involved, which is
   usually 0 for plain cases and induction rules of datatypes etc.\ and
diff -r 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/Complete_Lattices.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -1012,6 +1012,9 @@
 lemma image_UN: "f ` UNION A B = (\<Union>x\<in>A. f ` B x)"
   by blast
 
+lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
+  by blast
+
 
 subsection {* Distributive laws *}
 
@@ -1131,11 +1134,6 @@
   "\<And>A B f. (\<Inter>a\<in>A. B (f a)) = (\<Inter>x\<in>f`A. B x)"
   by auto
 
-text {* Legacy names *}
-
-lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
-  by blast
-
 text {* Finally *}
 
 no_notation
diff -r 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/HOL.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -26,6 +26,7 @@
   ("Tools/simpdata.ML")
   "~~/src/Tools/atomize_elim.ML"
   "~~/src/Tools/induct.ML"
+  ("~~/src/Tools/induction.ML")
   ("~~/src/Tools/induct_tacs.ML")
   ("Tools/recfun_codegen.ML")
   ("Tools/cnf_funcs.ML")
@@ -1490,8 +1491,10 @@
 )
 *}
 
+use "~~/src/Tools/induction.ML"
+
 setup {*
-  Induct.setup #>
+  Induct.setup #> Induction.setup #>
   Context.theory_map (Induct.map_simpset (fn ss => ss
     setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
       map (Simplifier.rewrite_rule (map Thm.symmetric
diff -r 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/AExp.thy
--- a/src/HOL/IMP/AExp.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/AExp.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/ASM.thy
--- a/src/HOL/IMP/ASM.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/ASM.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/AbsInt0.thy
--- a/src/HOL/IMP/AbsInt0.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/AbsInt0.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/AbsInt0_fun.thy
--- a/src/HOL/IMP/AbsInt0_fun.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/AbsInt0_fun.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/AbsInt1.thy
--- a/src/HOL/IMP/AbsInt1.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/AbsInt1.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -30,11 +30,11 @@
 
 locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep
   for rep :: "'a::L_top_bot \<Rightarrow> int set" and num' plus' +
-fixes inv_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
-and inv_less' :: "'a \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> 'a * 'a"
-assumes inv_plus': "inv_plus' a1 a2 a = (a1',a2') \<Longrightarrow>
+fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
+and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
+assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
   n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: a \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
-and inv_less': "inv_less' a1 a2 (n1<n2) = (a1',a2') \<Longrightarrow>
+and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
   n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
 
 datatype 'a up = bot | Up 'a
@@ -117,12 +117,12 @@
   let a' = lookup S x \<sqinter> a in
   if a' \<sqsubseteq> Bot then bot else Up(update S x a'))" |
 "afilter (Plus e1 e2) a S =
- (let (a1,a2) = inv_plus' (aval' e1 S) (aval' e2 S) a
+ (let (a1,a2) = filter_plus' a (aval' e1 S) (aval' e2 S)
   in afilter e1 a1 (afilter e2 a2 S))"
 
 text{* The test for @{const Bot} in the @{const V}-case is important: @{const
 Bot} indicates that a variable has no possible values, i.e.\ that the current
-program point is unreachable. But then the abstract state should collaps to
+program point is unreachable. But then the abstract state should collapse to
 @{const bot}. Put differently, we maintain the invariant that in an abstract
 state all variables are mapped to non-@{const Bot} values. Otherwise the
 (pointwise) join of two abstract states, one of which contains @{const Bot}
@@ -137,11 +137,11 @@
   (if res then bfilter b1 True (bfilter b2 True S)
    else bfilter b1 False S \<squnion> bfilter b2 False S)" |
 "bfilter (Less e1 e2) res S =
-  (let (res1,res2) = inv_less' (aval' e1 S) (aval' e2 S) res
+  (let (res1,res2) = filter_less' res (aval' e1 S) (aval' e2 S)
    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)
@@ -153,12 +153,12 @@
        (metis le_rep emptyE in_rep_meet rep_Bot subset_empty)
 next
   case (Plus e1 e2) thus ?case
-    using inv_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
+    using filter_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
     by (auto split: prod.split)
 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
@@ -167,7 +167,7 @@
 next
   case (Less e1 e2) thus ?case
     by (auto split: prod.split)
-       (metis afilter_sound inv_less' aval'_sound Less)
+       (metis afilter_sound filter_less' aval'_sound Less)
 qed
 
 fun AI :: "com \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/AbsInt1_ivl.thy
--- a/src/HOL/IMP/AbsInt1_ivl.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/AbsInt1_ivl.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -145,12 +145,13 @@
 by(auto simp add: minus_ivl_def rep_ivl_def split: ivl.splits option.splits)
 
 
-definition "inv_plus_ivl i1 i2 i = ((*if is_empty i then empty else*)
+definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
   i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
 
-fun inv_less_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> bool \<Rightarrow> ivl * ivl" where
-"inv_less_ivl (I l1 h1) (I l2 h2) res =
-  (if res
+fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
+"filter_less_ivl res (I l1 h1) (I l2 h2) =
+  ((*if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else*)
+   if res
    then (I l1 (min_option True h1 (h2 - Some 1)),
          I (max_option False (l1 + Some 1) l2) h2)
    else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
@@ -178,10 +179,10 @@
 qed
 
 interpretation
-  Val_abs1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl
+  Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
 proof
   case goal1 thus ?case
-    by(auto simp add: inv_plus_ivl_def)
+    by(auto simp add: filter_plus_ivl_def)
       (metis rep_minus_ivl add_diff_cancel add_commute)+
 next
   case goal2 thus ?case
@@ -190,7 +191,7 @@
 qed
 
 interpretation
-  Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter' 3)"
+  Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)"
 defines afilter_ivl is afilter
 and bfilter_ivl is bfilter
 and AI_ivl is AI
@@ -250,4 +251,10 @@
  DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
 value [code] "list_up(AI_ivl test4_ivl Top)"
 
+text{* Nontermination not detected: *}
+definition "test5_ivl =
+ ''x'' ::= N 0;
+ WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
+value [code] "list_up(AI_ivl test5_ivl Top)"
+
 end
diff -r 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/AbsInt2.thy
--- a/src/HOL/IMP/AbsInt2.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/AbsInt2.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -4,11 +4,41 @@
 imports AbsInt1_ivl
 begin
 
+context preord
+begin
+
+definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
+
+lemma monoD: "mono f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" by(simp add: mono_def)
+
+lemma mono_comp: "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (g o f)"
+by(simp add: mono_def)
+
+declare le_trans[trans]
+
+end
+
+
 subsection "Widening and Narrowing"
 
-text{* The assumptions about winden and narrow are merely sanity checks. They
-are only needed in case we want to prove termination of the fixedpoint
-iteration, which we do not --- we limit the number of iterations as before. *}
+text{* Jumping to the trivial post-fixed point @{const Top} in case @{text k}
+rounds of iteration did not reach a post-fixed point (as in @{const iter}) is
+a trivial widening step. We generalise this idea and complement it with
+narrowing, a process to regain precision.
+
+Class @{text WN} makes some assumptions about the widening and narrowing
+operators. The assumptions serve two purposes. Together with a further
+assumption that certain chains become stationary, they permit to prove
+termination of the fixed point iteration, which we do not --- we limit the
+number of iterations as before. The second purpose of the narrowing
+assumptions is to prove that the narrowing iteration keeps on producing
+post-fixed points and that it goes down. However, this requires the function
+being iterated to be monotone. Unfortunately, abstract interpretation with
+widening is not monotone. Hence the (recursive) abstract interpretation of a
+loop body that again contains a loop may result in a non-monotone
+function. Therefore our narrowing interation needs to check at every step
+that a post-fixed point is maintained, and we cannot prove that the precision
+increases. *}
 
 class WN = SL_top +
 fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
@@ -24,7 +54,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 +65,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
@@ -50,6 +80,44 @@
 using iter_up_pfp[of "\<lambda>x. x0 \<squnion> f x"] iter_down_pfp[of "\<lambda>x. x0 \<squnion> f x"]
 by(auto simp add: iter'_def Let_def)
 
+text{* This is how narrowing works on monotone functions: you just iterate. *}
+
+abbreviation iter_down_mono :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter_down_mono f n x == ((\<lambda>x. x \<triangle> f x)^^n) x"
+
+text{* Narrowing always yields a post-fixed point: *}
+
+lemma iter_down_mono_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0" 
+defines "x n == iter_down_mono f n x0"
+shows "f(x n) \<sqsubseteq> x n"
+proof (induction n)
+  case 0 show ?case by (simp add: x_def assms(2))
+next
+  case (Suc n)
+  have "f (x (Suc n)) = f(x n \<triangle> f(x n))" by(simp add: x_def)
+  also have "\<dots> \<sqsubseteq> f(x n)" by(rule monoD[OF `mono f` narrow2[OF Suc]])
+  also have "\<dots> \<sqsubseteq> x n \<triangle> f(x n)" by(rule narrow1[OF Suc])
+  also have "\<dots> = x(Suc n)" by(simp add: x_def)
+  finally show ?case .
+qed
+
+text{* Narrowing can only increase precision: *}
+
+lemma iter_down_down: assumes "mono f" and "f x0 \<sqsubseteq> x0" 
+defines "x n == iter_down_mono f n x0"
+shows "x n \<sqsubseteq> x0"
+proof (induction n)
+  case 0 show ?case by(simp add: x_def)
+next
+  case (Suc n)
+  have "x(Suc n) = x n \<triangle> f(x n)" by(simp add: x_def)
+  also have "\<dots> \<sqsubseteq> x n" unfolding x_def
+    by(rule narrow2[OF iter_down_mono_pfp[OF assms(1), OF assms(2)]])
+  also have "\<dots> \<sqsubseteq> x0" by(rule Suc)
+  finally show ?case .
+qed
+
+
 end
 
 
@@ -57,8 +125,7 @@
 begin
 
 definition "widen_ivl ivl1 ivl2 =
-  ((*if is_empty ivl1 then ivl2 else
-   if is_empty ivl2 then ivl1 else*)
+  ((*if is_empty ivl1 then ivl2 else if is_empty ivl2 then ivl1 else*)
      case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
        I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l2)
          (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h2))"
@@ -75,7 +142,7 @@
 
 end
 
-instantiation astate :: (WN)WN
+instantiation astate :: (WN) WN
 begin
 
 definition "widen_astate F1 F2 =
@@ -98,7 +165,7 @@
 
 end
 
-instantiation up :: (WN)WN
+instantiation up :: (WN) WN
 begin
 
 fun widen_up where
@@ -126,7 +193,7 @@
 end
 
 interpretation
-  Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter' 3 2)"
+  Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
 defines afilter_ivl' is afilter
 and bfilter_ivl' is bfilter
 and AI_ivl' is AI
@@ -135,5 +202,6 @@
 
 value [code] "list_up(AI_ivl' test3_ivl Top)"
 value [code] "list_up(AI_ivl' test4_ivl Top)"
+value [code] "list_up(AI_ivl' test5_ivl Top)"
 
 end
diff -r 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/BExp.thy
--- a/src/HOL/IMP/BExp.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/BExp.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Big_Step.thy
--- a/src/HOL/IMP/Big_Step.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Big_Step.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Comp_Rev.thy
--- a/src/HOL/IMP/Comp_Rev.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Comp_Rev.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Compiler.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Def_Ass_Sound_Big.thy
--- a/src/HOL/IMP/Def_Ass_Sound_Big.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Def_Ass_Sound_Big.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Def_Ass_Sound_Small.thy
--- a/src/HOL/IMP/Def_Ass_Sound_Small.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Def_Ass_Sound_Small.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Denotation.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Fold.thy
--- a/src/HOL/IMP/Fold.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Fold.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/HoareT.thy
--- a/src/HOL/IMP/HoareT.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/HoareT.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Hoare_Examples.thy
--- a/src/HOL/IMP/Hoare_Examples.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Hoare_Examples.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Hoare_Sound_Complete.thy
--- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Live.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Poly_Types.thy
--- a/src/HOL/IMP/Poly_Types.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Poly_Types.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Sec_Typing.thy
--- a/src/HOL/IMP/Sec_Typing.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Sec_Typing.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Sec_TypingT.thy
--- a/src/HOL/IMP/Sec_TypingT.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Sec_TypingT.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Sem_Equiv.thy
--- a/src/HOL/IMP/Sem_Equiv.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Sem_Equiv.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Small_Step.thy
--- a/src/HOL/IMP/Small_Step.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Small_Step.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Star.thy
--- a/src/HOL/IMP/Star.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Star.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Types.thy
--- a/src/HOL/IMP/Types.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Types.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/VC.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IMP/Vars.thy
--- a/src/HOL/IMP/Vars.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IMP/Vars.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -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
diff -r 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/IsaMakefile	Wed Sep 21 06:41:34 2011 -0700
@@ -145,6 +145,7 @@
   $(SRC)/Tools/eqsubst.ML \
   $(SRC)/Tools/induct.ML \
   $(SRC)/Tools/induct_tacs.ML \
+  $(SRC)/Tools/induction.ML \
   $(SRC)/Tools/intuitionistic.ML \
   $(SRC)/Tools/misc_legacy.ML \
   $(SRC)/Tools/nbe.ML \
@@ -514,7 +515,7 @@
 
 $(OUT)/HOL-IMP: $(OUT)/HOL IMP/AbsInt0_fun.thy IMP/Astate.thy \
   IMP/AbsInt0.thy IMP/AbsInt0_const.thy IMP/AbsInt1.thy IMP/AbsInt1_ivl.thy \
-  IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy	\
+  IMP/AbsInt2.thy IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy	\
   IMP/Big_Step.thy IMP/C_like.thy IMP/Com.thy IMP/Compiler.thy \
   IMP/Comp_Rev.thy IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \
   IMP/Def_Ass_Small.thy IMP/Def_Ass_Sound_Big.thy \
diff -r 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/Library/Executable_Set.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -101,12 +101,12 @@
 lemma insert_Set [code]:
   "insert x (Set xs) = Set (List.insert x xs)"
   "insert x (Coset xs) = Coset (removeAll x xs)"
-  by (simp_all add: set_insert)
+  by simp_all
 
 lemma remove_Set [code]:
   "remove x (Set xs) = Set (removeAll x xs)"
   "remove x (Coset xs) = Coset (List.insert x xs)"
-  by (auto simp add: set_insert remove_def)
+  by (auto simp add: remove_def)
 
 lemma image_Set [code]:
   "image f (Set xs) = Set (remdups (map f xs))"
@@ -254,12 +254,12 @@
 lemma Inf_inf [code]:
   "Inf (Set xs) = foldr inf xs (top :: 'a::complete_lattice)"
   "Inf (Coset []) = (bot :: 'a::complete_lattice)"
-  by (simp_all add: Inf_UNIV Inf_set_foldr)
+  by (simp_all add: Inf_set_foldr)
 
 lemma Sup_sup [code]:
   "Sup (Set xs) = foldr sup xs (bot :: 'a::complete_lattice)"
   "Sup (Coset []) = (top :: 'a::complete_lattice)"
-  by (simp_all add: Sup_UNIV Sup_set_foldr)
+  by (simp_all add: Sup_set_foldr)
 
 lemma Inter_inter [code]:
   "Inter (Set xs) = foldr inter xs (Coset [])"
@@ -279,50 +279,40 @@
 
 text {* Initially contributed by Tjark Weber. *}
 
-lemma bounded_Collect_code [code_unfold]:
-  "{x\<in>S. P x} = project P S"
-  by (auto simp add: project_def)
-
-lemma Id_on_code [code]:
-  "Id_on (Set xs) = Set [(x,x). x \<leftarrow> xs]"
-  by (auto simp add: Id_on_def)
-
-lemma Domain_fst [code]:
+lemma [code]:
   "Domain r = fst ` r"
-  by (auto simp add: image_def Bex_def)
+  by (fact Domain_fst)
 
-lemma Range_snd [code]:
+lemma [code]:
   "Range r = snd ` r"
-  by (auto simp add: image_def Bex_def)
+  by (fact Range_snd)
 
-lemma irrefl_code [code]:
-  "irrefl r \<longleftrightarrow> (\<forall>(x, y)\<in>r. x \<noteq> y)"
-  by (auto simp add: irrefl_def)
+lemma [code]:
+  "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
+  by (fact trans_join)
+
+lemma [code]:
+  "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
+  by (fact irrefl_distinct)
 
-lemma trans_def [code]:
-  "trans r \<longleftrightarrow> (\<forall>(x, y1)\<in>r. \<forall>(y2, z)\<in>r. y1 = y2 \<longrightarrow> (x, z)\<in>r)"
-  by (auto simp add: trans_def)
+lemma [code]:
+  "acyclic r \<longleftrightarrow> irrefl (r^+)"
+  by (fact acyclic_irrefl)
 
-definition "exTimes A B = Sigma A (%_. B)"
-
-lemma [code_unfold]:
-  "Sigma A (%_. B) = exTimes A B"
-  by (simp add: exTimes_def)
+lemma [code]:
+  "More_Set.product (Set xs) (Set ys) = Set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
+  by (unfold Set_def) (fact product_code)
 
-lemma exTimes_code [code]:
-  "exTimes (Set xs) (Set ys) = Set [(x,y). x \<leftarrow> xs, y \<leftarrow> ys]"
-  by (auto simp add: exTimes_def)
-
-lemma rel_comp_code [code]:
-  "(Set xys) O (Set yzs) = Set (remdups [(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
- by (auto simp add: Bex_def)
+lemma [code]:
+  "Id_on (Set xs) = Set [(x, x). x \<leftarrow> xs]"
+  by (unfold Set_def) (fact Id_on_set)
 
-lemma acyclic_code [code]:
-  "acyclic r = irrefl (r^+)"
-  by (simp add: acyclic_def irrefl_def)
+lemma [code]:
+  "Set xys O Set yzs = Set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
+  by (unfold Set_def) (fact set_rel_comp)
 
-lemma wf_code [code]:
+lemma [code]:
   "wf (Set xs) = acyclic (Set xs)"
-  by (simp add: wf_iff_acyclic_if_finite)
+  by (unfold Set_def) (fact wf_set)
 
 end
diff -r 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/Library/More_Set.thy
--- a/src/HOL/Library/More_Set.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/Library/More_Set.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -31,7 +31,20 @@
 qed
 
 definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
-  "project P A = {a\<in>A. P a}"
+  "project P A = {a \<in> A. P a}"
+
+lemma bounded_Collect_code [code_unfold_post]:
+  "{x \<in> A. P x} = project P A"
+  by (simp add: project_def)
+
+definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
+  "product A B = Sigma A (\<lambda>_. B)"
+
+hide_const (open) product
+
+lemma [code_unfold_post]:
+  "Sigma A (\<lambda>_. B) = More_Set.product A B"
+  by (simp add: product_def)
 
 
 subsection {* Basic set operations *}
@@ -75,7 +88,7 @@
   "set xs \<union> A = foldr Set.insert xs A"
 proof -
   have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
-    by (auto intro: ext)
+    by auto
   then show ?thesis by (simp add: union_set foldr_fold)
 qed
 
@@ -92,7 +105,7 @@
   "A - set xs = foldr remove xs A"
 proof -
   have "\<And>x y :: 'a. remove y \<circ> remove x = remove x \<circ> remove y"
-    by (auto simp add: remove_def intro: ext)
+    by (auto simp add: remove_def)
   then show ?thesis by (simp add: minus_set foldr_fold)
 qed
 
@@ -120,10 +133,22 @@
   by (auto simp add: project_def)
 
 
-subsection {* Various lemmas *}
+subsection {* Theorems on relations *}
+
+lemma product_code:
+  "More_Set.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
+  by (auto simp add: product_def)
 
-lemma not_set_compl:
-  "Not \<circ> set xs = - set xs"
-  by (simp add: fun_Compl_def comp_def fun_eq_iff)
+lemma Id_on_set:
+  "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
+  by (auto simp add: Id_on_def)
+
+lemma set_rel_comp:
+  "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
+  by (auto simp add: Bex_def)
+
+lemma wf_set:
+  "wf (set xs) = acyclic (set xs)"
+  by (simp add: wf_iff_acyclic_if_finite)
 
 end
diff -r 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/Relation.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -275,6 +275,10 @@
 
 subsection {* Transitivity *}
 
+lemma trans_join:
+  "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
+  by (auto simp add: trans_def)
+
 lemma transI:
   "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
 by (unfold trans_def) iprover
@@ -296,6 +300,10 @@
 
 subsection {* Irreflexivity *}
 
+lemma irrefl_distinct:
+  "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
+  by (auto simp add: irrefl_def)
+
 lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
 by(simp add:irrefl_def)
 
@@ -386,6 +394,10 @@
   "a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
 by (iprover dest!: iffD1 [OF Domain_iff])
 
+lemma Domain_fst:
+  "Domain r = fst ` r"
+  by (auto simp add: image_def Bex_def)
+
 lemma Domain_empty [simp]: "Domain {} = {}"
 by blast
 
@@ -440,6 +452,10 @@
 lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
 by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
 
+lemma Range_snd:
+  "Range r = snd ` r"
+  by (auto simp add: image_def Bex_def)
+
 lemma Range_empty [simp]: "Range {} = {}"
 by blast
 
diff -r 5a4d62f9e88d -r 34e5fc15ea02 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/HOL/Wellfounded.thy	Wed Sep 21 06:41:34 2011 -0700
@@ -387,6 +387,10 @@
 abbreviation acyclicP :: "('a => 'a => bool) => bool" where
   "acyclicP r == acyclic {(x, y). r x y}"
 
+lemma acyclic_irrefl:
+  "acyclic r \<longleftrightarrow> irrefl (r^+)"
+  by (simp add: acyclic_def irrefl_def)
+
 lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
   by (simp add: acyclic_def)
 
diff -r 5a4d62f9e88d -r 34e5fc15ea02 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/Tools/induct.ML	Wed Sep 21 06:41:34 2011 -0700
@@ -74,11 +74,21 @@
   val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
     thm list -> int -> cases_tactic
   val get_inductT: Proof.context -> term option list list -> thm list list
+  type case_data = (((string * string list) * string list) list * int) (* FIXME -> rule_cases.ML *)
+  val gen_induct_tac: (theory -> case_data * thm -> case_data * thm) ->
+    Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+    (string * typ) list list -> term option list -> thm list option ->
+    thm list -> int -> cases_tactic
   val induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
     (string * typ) list list -> term option list -> thm list option ->
     thm list -> int -> cases_tactic
   val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
     thm list -> int -> cases_tactic
+  val gen_induct_setup: binding ->
+   (Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+    (string * typ) list list -> term option list -> thm list option ->
+    thm list -> int -> cases_tactic) ->
+   theory -> theory
   val setup: theory -> theory
 end;
 
@@ -721,7 +731,9 @@
 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   | get_inductP _ _ = [];
 
-fun induct_tac ctxt simp def_insts arbitrary taking opt_rule facts =
+type case_data = (((string * string list) * string list) list * int)
+
+fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
   let
     val thy = Proof_Context.theory_of ctxt;
 
@@ -734,6 +746,7 @@
           (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
         |> maps (prep_inst ctxt align_right (atomize_term thy))
         |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
+      |> mod_cases thy
       |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
 
     val ruleq =
@@ -791,7 +804,7 @@
        THEN_ALL_NEW rulify_tac)
   end;
 
-
+val induct_tac = gen_induct_tac (K I);
 
 (** coinduct method **)
 
@@ -910,16 +923,18 @@
           (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
     "case analysis on types or predicates/sets";
 
-val induct_setup =
-  Method.setup @{binding induct}
+fun gen_induct_setup binding itac =
+  Method.setup binding
     (Args.mode no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
       (arbitrary -- taking -- Scan.option induct_rule)) >>
       (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
         RAW_METHOD_CASES (fn facts =>
           Seq.DETERM
-            (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
+            (HEADGOAL (itac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
     "induction on types or predicates/sets";
 
+val induct_setup = gen_induct_setup @{binding induct} induct_tac;
+
 val coinduct_setup =
   Method.setup @{binding coinduct}
     (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
diff -r 5a4d62f9e88d -r 34e5fc15ea02 src/Tools/induction.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/induction.ML	Wed Sep 21 06:41:34 2011 -0700
@@ -0,0 +1,43 @@
+signature INDUCTION =
+sig
+  val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+    (string * typ) list list -> term option list -> thm list option ->
+    thm list -> int -> cases_tactic
+  val setup: theory -> theory
+end
+
+structure Induction: INDUCTION =
+struct
+
+val ind_hypsN = "IH";
+
+fun preds_of t =
+ (case strip_comb t of
+    (p as Var _, _) => [p]
+  | (p as Free _, _) => [p]
+  | (_, ts) => flat(map preds_of ts))
+
+fun name_hyps thy (arg as ((cases,consumes),th)) =
+  if not(forall (null o #2 o #1) cases) then arg
+  else
+    let
+      val (prems, concl) = Logic.strip_horn (prop_of th);
+      val prems' = drop consumes prems;
+      val ps = preds_of concl;
+
+      fun hname_of t =
+        if exists_subterm (member (op =) ps) t
+        then ind_hypsN else Rule_Cases.case_hypsN
+
+      val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems'
+      val n = Int.min (length hnamess, length cases) 
+      val cases' = map (fn (((cn,_),concls),hns) => ((cn,hns),concls))
+        (take n cases ~~ take n hnamess)
+    in ((cases',consumes),th) end
+
+val induction_tac = Induct.gen_induct_tac name_hyps
+
+val setup = Induct.gen_induct_setup @{binding induction} induction_tac
+
+end
+
diff -r 5a4d62f9e88d -r 34e5fc15ea02 src/Tools/jEdit/etc/settings
--- a/src/Tools/jEdit/etc/settings	Tue Sep 20 11:02:41 2011 -0700
+++ b/src/Tools/jEdit/etc/settings	Wed Sep 21 06:41:34 2011 -0700
@@ -4,8 +4,8 @@
 JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
 
 JEDIT_OPTIONS="-reuseview -noserver -nobackground -log=9"
-JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss4m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
-#JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
+JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
+#JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss1m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
 JEDIT_SYSTEM_OPTIONS="-Dapple.laf.useScreenMenuBar=true -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit"
 
 JEDIT_STYLE_SHEETS="$ISABELLE_HOME/etc/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css"