# HG changeset patch
# User nipkow
# Date 1385295779 -3600
# Node ID be1186cb03ce4264e8eba8449573951b88843946
# Parent  002b8729f22802d984a6255f267d8ed0ceb6a7c6
replaced bad example

diff -r 002b8729f228 -r be1186cb03ce src/Doc/ProgProve/Types_and_funs.thy
--- a/src/Doc/ProgProve/Types_and_funs.thy	Sun Nov 24 00:31:50 2013 +0000
+++ b/src/Doc/ProgProve/Types_and_funs.thy	Sun Nov 24 13:22:59 2013 +0100
@@ -171,16 +171,25 @@
 This customized induction rule can simplify inductive proofs. For example,
 *}
 
-lemma "div2(n+n) = n"
+lemma "div2(n) = n div 2"
 apply(induction n rule: div2.induct)
 
-txt{* yields the 3 subgoals
+txt{* (where the infix @{text div} is the predefined division operation)
+yields the 3 subgoals
 @{subgoals[display,margin=65]}
 An application of @{text auto} finishes the proof.
 Had we used ordinary structural induction on @{text n},
 the proof would have needed an additional
 case analysis in the induction step.
 
+This example leads to the following induction heuristic:
+\begin{quote}
+\emph{Let @{text f} be a recursive function.
+If the definition of @{text f} is more complicated
+than having one equation for each constructor of some datatype,
+then properties of @{text f} are best proved via @{text "f.induct"}.}
+\end{quote}
+
 The general case is often called \concept{computation induction},
 because the induction follows the (terminating!) computation.
 For every defining equation
@@ -223,8 +232,9 @@
 \end{exercise}
 
 \begin{exercise}
-Prove that @{const div2} defined above divides every number by @{text 2},
-not just those of the form @{text"n+n"}: @{prop "div2 n = n div 2"}.
+Define a function @{text "intersperse ::"} @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"}
+such that @{text "intersperse a [x\<^sub>1, ..., x\<^sub>n] = [x\<^sub>1, a, x\<^sub>2, a, ..., a, x\<^sub>n]"}.
+Now prove that @{prop "map f (intersperse a xs) = intersperse (f a) (map f xs)"}.
 \end{exercise}