summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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