1.1 --- a/doc-src/Nitpick/nitpick.tex	Sat Feb 13 11:56:06 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Sat Feb 13 15:04:09 2010 +0100
     1.3 @@ -1331,7 +1331,7 @@
     1.4  and this time \textit{arith} can finish off the subgoals.
     1.5  
     1.6  A similar technique can be employed for structural induction. The
     1.7 -following mini-formalization of full binary trees will serve as illustration:
     1.8 +following mini formalization of full binary trees will serve as illustration:
     1.9  
    1.10  \prew
    1.11  \textbf{datatype} $\kern1pt'a$~\textit{bin\_tree} = $\textit{Leaf}~{\kern1pt'a}$ $\mid$ $\textit{Branch}$ ``\kern1pt$'a$ \textit{bin\_tree}'' ``\kern1pt$'a$ \textit{bin\_tree}'' \\[2\smallskipamount]
    1.12 @@ -1350,8 +1350,7 @@
    1.13  obtained by swapping $a$ and $b$:
    1.14  
    1.15  \prew
    1.16 -\textbf{lemma} $``\lbrakk a \in \textit{labels}~t;\, b \in \textit{labels}~t;\, a \not= b\rbrakk {}$ \\
    1.17 -\phantom{\textbf{lemma} ``}$\,{\Longrightarrow}{\;\,} \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
    1.18 +\textbf{lemma} $``\{a, b\} \subseteq \textit{labels}~t \,\Longrightarrow\, \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
    1.19  \postw
    1.20  
    1.21  Nitpick can't find any counterexample, so we proceed with induction
    1.22 @@ -1370,29 +1369,29 @@
    1.23  \prew
    1.24  \slshape
    1.25  Hint: To check that the induction hypothesis is general enough, try this command:
    1.26 -\textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_consts}].
    1.27 +\textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_all}].
    1.28  \postw
    1.29  
    1.30  If we follow the hint, we get a ``nonstandard'' counterexample for the step:
    1.31  
    1.32  \prew
    1.33 -\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
    1.34 +\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 3: \\[2\smallskipamount]
    1.35  \hbox{}\qquad Free variables: \nopagebreak \\
    1.36  \hbox{}\qquad\qquad $a = a_1$ \\
    1.37  \hbox{}\qquad\qquad $b = a_2$ \\
    1.38  \hbox{}\qquad\qquad $t = \xi_1$ \\
    1.39  \hbox{}\qquad\qquad $u = \xi_2$ \\
    1.40 +\hbox{}\qquad Datatype: \nopagebreak \\
    1.41 +\hbox{}\qquad\qquad $\alpha~\textit{btree} = \{\xi_1 \mathbin{=} \textit{Branch}~\xi_1~\xi_1,\> \xi_2 \mathbin{=} \textit{Branch}~\xi_2~\xi_2,\> \textit{Branch}~\xi_1~\xi_2\}$ \\
    1.42  \hbox{}\qquad {\slshape Constants:} \nopagebreak \\
    1.43  \hbox{}\qquad\qquad $\textit{labels} = \undef
    1.44      (\!\begin{aligned}[t]%
    1.45 -    & \xi_1 := \{a_1, a_4, a_3^\Q\},\> \xi_2 := \{a_2, a_3^\Q\}, \\[-2pt] %% TYPESETTING
    1.46 -    & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_4, a_3^\Q\}, \\[-2pt]
    1.47 -    & \textit{Branch}~\xi_2~\xi_2 := \{a_2, a_3^\Q\})\end{aligned}$ \\
    1.48 +    & \xi_1 := \{a_2, a_3\},\> \xi_2 := \{a_1\},\> \\[-2pt]
    1.49 +    & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_3\})\end{aligned}$ \\
    1.50  \hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
    1.51      (\!\begin{aligned}[t]%
    1.52      & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
    1.53 -    & \textit{Branch}~\xi_1~\xi_2 := \textit{Branch}~\xi_2~\xi_2, \\[-2pt]
    1.54 -    & \textit{Branch}~\xi_2~\xi_2 := \textit{Branch}~\xi_2~\xi_2)\end{aligned}$ \\[2\smallskipamount]
    1.55 +    & \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount]
    1.56  The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
    1.57  even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
    1.58  \postw
    1.59 @@ -1408,9 +1407,9 @@
    1.60  \textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
    1.61  set of objects over which the induction is performed while doing the step
    1.62  in order to test the induction hypothesis's strength.}
    1.63 -The new trees are so nonstandard that we know nothing about them, except what
    1.64 -the induction hypothesis states and what can be proved about all trees without
    1.65 -relying on induction or case distinction. The key observation is,
    1.66 +Unlike standard trees, these new trees contain cycles. We will see later that
    1.67 +every property of acyclic trees that can be proved without using induction also
    1.68 +holds for cyclic trees. Hence,
    1.69  %
    1.70  \begin{quote}
    1.71  \textsl{If the induction
    1.72 @@ -1418,9 +1417,9 @@
    1.73  objects, and Nitpick won't find any nonstandard counterexample.}
    1.74  \end{quote}
    1.75  %
    1.76 -But here, Nitpick did find some nonstandard trees $t = \xi_1$
    1.77 -and $u = \xi_2$ such that $a \in \textit{labels}~t$, $b \notin
    1.78 -\textit{labels}~t$, $a \notin \textit{labels}~u$, and $b \in \textit{labels}~u$.
    1.79 +But here the tool find some nonstandard trees $t = \xi_1$
    1.80 +and $u = \xi_2$ such that $a \notin \textit{labels}~t$, $b \in
    1.81 +\textit{labels}~t$, $a \in \textit{labels}~u$, and $b \notin \textit{labels}~u$.
    1.82  Because neither tree contains both $a$ and $b$, the induction hypothesis tells
    1.83  us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
    1.84  and as a result we know nothing about the labels of the tree