summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Tue, 07 Nov 2000 18:38:24 +0100 | |

changeset 10419 | 1bfdd19c1d47 |

parent 10418 | bd1d199fc58e |

child 10420 | ef006735bee8 |

better discussion of rule induction

--- a/doc-src/TutorialI/Inductive/Even.tex Tue Nov 07 17:55:04 2000 +0100 +++ b/doc-src/TutorialI/Inductive/Even.tex Tue Nov 07 18:38:24 2000 +0100 @@ -1,4 +1,3 @@ -% ID: $Id$ \section{The set of even numbers} The set of even numbers can be inductively defined as the least set @@ -32,16 +31,12 @@ automatically-generated names. Here are two examples: % \begin{isabelle} +0\ \isasymin \ even +\rulename{even.zero} +\par\smallskip n\ \isasymin \ even\ \isasymLongrightarrow \ Suc\ (Suc\ n)\ \isasymin \ even% \rulename{even.step} -\par\medskip -\isasymlbrakk xa\ \isasymin \ even;\isanewline -\ P\ 0;\isanewline -\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ P\ n\isasymrbrakk \ -\isasymLongrightarrow \ P\ (Suc\ (Suc\ n))\isasymrbrakk\isanewline -\ \isasymLongrightarrow \ P\ xa% -\rulename{even.induct} \end{isabelle} The introduction rules can be given attributes. Here both rules are @@ -86,10 +81,31 @@ \subsection{Rule induction} -The other direction of this equivalence is proved by induction over the set -\isa{even}. This type of inductive argument is called \textbf{rule induction}. -It is the usual way of proving a property of the elements of an inductively -defined set. +From the definition of the set +\isa{even}, Isabelle has +generated an induction rule: +\begin{isabelle} +\isasymlbrakk xa\ \isasymin \ even;\isanewline +\ P\ 0;\isanewline +\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ P\ n\isasymrbrakk \ +\isasymLongrightarrow \ P\ (Suc\ (Suc\ n))\isasymrbrakk\isanewline +\ \isasymLongrightarrow \ P\ xa% +\rulename{even.induct} +\end{isabelle} +A property \isa{P} holds for every even number provided it +holds for~\isa{0} and is closed under the operation +\isa{Suc(Suc\(\cdots\))}. Then \isa{P} is closed under the introduction +rules for \isa{even}, which is the least set closed under those rules. +This type of inductive argument is called \textbf{rule induction}. + +Apart from the double application of \isa{Suc}, the induction rule above +resembles the familiar mathematical induction, which indeed is an instance +of rule induction; the natural numbers can be defined inductively to be +the least set containing \isa{0} and closed under~\isa{Suc}. + +Induction is the usual way of proving a property of the elements of an +inductively defined set. Let us prove that all members of the set +\isa{even} are multiples of two. \begin{isabelle} \isacommand{lemma}\ even_imp_dvd:\ "n\ \isasymin \ even\ \isasymLongrightarrow \ \#2\ dvd\ n"\isanewline \isacommand{apply}\ (erule\ even.induct)\isanewline @@ -196,5 +212,8 @@ \isacommand{lemma}\ [iff]:\ "((Suc\ (Suc\ n))\ \isasymin \ even)\ =\ (n\ \isasymin \ even)"\isanewline \isacommand{apply}\ (blast\ dest:\ Suc_Suc_even_imp_even)\isanewline -\isacommand{done}\isanewline +\isacommand{done} \end{isabelle} + +The even numbers example has shown how inductive definitions can be used. +Later examples will show that they are actually worth using.