# HG changeset patch
# User wenzelm
# Date 1132768320 -3600
# Node ID 5a124c76e92fd10dcfccf0ca5e83cd03cb839e5d
# Parent  bc367912603f9d2dc71788588413a169b16277b7
tuned;

diff -r bc367912603f -r 5a124c76e92f NEWS
--- a/NEWS	Wed Nov 23 18:51:59 2005 +0100
+++ b/NEWS	Wed Nov 23 18:52:00 2005 +0100
@@ -61,6 +61,48 @@
   have "!!x. P x ==> Q x" by fact  ==  note `!!x. P x ==> Q x`
   have "P a ==> Q a" by fact       ==  note `P a ==> Q a`
 
+* Provers/induct: improved internal context management to support
+local fixes and defines on-the-fly.  Thus explicit meta-level
+connectives !! and ==> are rarely required anymore in inductive goals
+(using object-logic connectives for this purpose has been long
+obsolete anyway).  The subsequent proof patterns illustrate advanced
+techniques of natural induction; general datatypes and inductive sets
+work analogously.
+
+This is how to ``strengthen'' an inductive goal wrt. certain
+parameters:
+
+  lemma
+    fixes n :: nat and x :: 'a
+    assumes a: "A n x"
+    shows "P n x"
+    using a                     -- {* make induct insert fact a *}
+  proof (induct n fixing: x)    -- {* generalize goal to "!!x. A n x ==> P n x" *}
+    case (0 x)
+    show ?case sorry
+  next
+    case (Suc n x)
+    note `!!x. A n x ==> P n x` -- {* induction hypotheses, according to induction rule *}
+    note `A (Suc n) x`          -- {* induction premises, stemming from fact a *}
+    show ?case sorry
+  qed
+
+This is how to perform induction over ``expressions of a certain
+form'', using a locally defined inductive parameter n == "a x"
+together with strengthening (the latter is usually required to
+sufficiently flexible induction hypotheses).
+
+  lemma
+    fixes a :: "'a => nat"
+    assumes a: "A (a x)"
+    shows "P (a x)"
+    using a
+  proof (induct n == "a x" fixing: x)
+    ...
+
+See also HOL/Isar_examples/Puzzle.thy for an application of the latter
+technique.
+
 * Input syntax now supports dummy variable binding "%_. b", where the
 body does not mention the bound variable.  Note that dummy patterns
 implicitly depend on their context of bounds, which makes "{_. _}"
diff -r bc367912603f -r 5a124c76e92f doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Wed Nov 23 18:51:59 2005 +0100
+++ b/doc-src/IsarRef/pure.tex	Wed Nov 23 18:52:00 2005 +0100
@@ -838,7 +838,7 @@
 corresponding number of sub-goals prior to an initial method application, via
 $\PROOFNAME$ (\S\ref{sec:proof-steps}) or $\APPLYNAME$
 (\S\ref{sec:tactic-commands}).  The $induct$ method covered in
-\S\ref{sec:cases-induct-meth} acts on multiple claims simultaneously.
+\S\ref{sec:cases-induct} acts on multiple claims simultaneously.
 
 Claims at the theory level may be either in short or long form.  A short goal
 merely consists of several simultaneous propositions (often just one).  A long