doc-src/TutorialI/Inductive/Even.tex
changeset 10654 458068404143
parent 10520 bb9dfcc87951
child 10762 cd1a2bee5549
     1.1 --- a/doc-src/TutorialI/Inductive/Even.tex	Wed Dec 13 09:32:55 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Inductive/Even.tex	Wed Dec 13 09:39:53 2000 +0100
     1.3 @@ -179,8 +179,10 @@
     1.4  \ 2.\ \isasymAnd na.\ \isasymlbrakk na\ \isasymin \ even;\ n\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ n\ \isasymin \ even%
     1.5  \end{isabelle}
     1.6  The first one is hopeless.  In general, rule inductions involving
     1.7 -non-trivial terms will probably go wrong.  The solution is easy provided
     1.8 -we have the necessary inverses, here subtraction:
     1.9 +non-trivial terms will probably go wrong. How to deal with such situations
    1.10 +in general is described in {\S}\ref{sec:ind-var-in-prems} below.
    1.11 +In the current case the solution is easy because
    1.12 +we have the necessary inverse, subtraction:
    1.13  \begin{isabelle}
    1.14  \isacommand{lemma}\ even_imp_even_minus_2:\ "n\ \isasymin \ even\ \isasymLongrightarrow \ n-\#2\ \isasymin \ even"\isanewline
    1.15  \isacommand{apply}\ (erule\ even.induct)\isanewline