# HG changeset patch
# User paulson
# Date 1385298467 0
# Node ID d04e74341d433ee049628d275bbc67b083163947
# Parent  07864001495d8a5a6cbbc33f0f19e274855853b8# Parent  95a33ff3984bd78eb5b28c6dda13f689d6f55593
merged

diff -r 07864001495d -r d04e74341d43 src/Doc/ProgProve/Types_and_funs.thy
--- a/src/Doc/ProgProve/Types_and_funs.thy	Sun Nov 24 13:06:22 2013 +0000
+++ b/src/Doc/ProgProve/Types_and_funs.thy	Sun Nov 24 13:07:47 2013 +0000
@@ -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}
 
 
diff -r 07864001495d -r d04e74341d43 src/Doc/ProgProve/document/intro-isabelle.tex
--- a/src/Doc/ProgProve/document/intro-isabelle.tex	Sun Nov 24 13:06:22 2013 +0000
+++ b/src/Doc/ProgProve/document/intro-isabelle.tex	Sun Nov 24 13:07:47 2013 +0000
@@ -89,5 +89,6 @@
 \ifsem\else
 \paragraph{Acknowledgements}
 I wish to thank the following people for their comments on this document:
-Florian Haftmann, Ren\'{e} Thiemann, Sean Seefried and Christian Sternagel.
+Florian Haftmann, Ren\'{e} Thiemann, Sean Seefried, Christian Sternagel
+and Carl Witty.
 \fi
\ No newline at end of file