# HG changeset patch # User paulson # Date 979312173 -3600 # Node ID ca2b00c4bba7adc223dda4606be88bb894a3fe0c # Parent b254d5ad6dd4f5f49222dc85f68d6b644fa6e74f renaming to avoid clashes diff -r b254d5ad6dd4 -r ca2b00c4bba7 doc-src/TutorialI/Inductive/Advanced.tex --- a/doc-src/TutorialI/Inductive/Advanced.tex Fri Jan 12 16:07:20 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,431 +0,0 @@ - -This section describes advanced features of inductive definitions. -The premises of introduction rules may contain universal quantifiers and -monotonic functions. Theorems may be proved by rule inversion. - -\subsection{Universal quantifiers in introduction rules} -\label{sec:gterm-datatype} - -As a running example, this section develops the theory of \textbf{ground -terms}: terms constructed from constant and function -symbols but not variables. To simplify matters further, we regard a -constant as a function applied to the null argument list. Let us declare a -datatype \isa{gterm} for the type of ground terms. It is a type constructor -whose argument is a type of function symbols. -\begin{isabelle} -\isacommand{datatype}\ 'f\ gterm\ =\ Apply\ 'f\ "'f\ gterm\ list" -\end{isabelle} -To try it out, we declare a datatype of some integer operations: -integer constants, the unary minus operator and the addition -operator. -\begin{isabelle} -\isacommand{datatype}\ integer_op\ =\ Number\ int\ |\ UnaryMinus\ |\ Plus -\end{isabelle} -Now the type \isa{integer\_op gterm} denotes the ground -terms built over those symbols. - -The type constructor \texttt{gterm} can be generalized to a function -over sets. It returns -the set of ground terms that can be formed over a set \isa{F} of function symbols. For -example, we could consider the set of ground terms formed from the finite -set {\isa{\{Number 2, UnaryMinus, Plus\}}}. - -This concept is inductive. If we have a list \isa{args} of ground terms -over~\isa{F} and a function symbol \isa{f} in \isa{F}, then we -can apply \isa{f} to \isa{args} to obtain another ground term. -The only difficulty is that the argument list may be of any length. Hitherto, -each rule in an inductive definition referred to the inductively -defined set a fixed number of times, typically once or twice. -A universal quantifier in the premise of the introduction rule -expresses that every element of \isa{args} belongs -to our inductively defined set: is a ground term -over~\isa{F}. The function {\isa{set}} denotes the set of elements in a given -list. -\begin{isabelle} -\isacommand{consts}\ gterms\ ::\ "'f\ set\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline -\isacommand{inductive}\ "gterms\ F"\isanewline -\isakeyword{intros}\isanewline -step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ gterms\ F;\ \ f\ \isasymin \ F\isasymrbrakk \isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ gterms\ -F" -\end{isabelle} - -To demonstrate a proof from this definition, let us -show that the function \isa{gterms} -is \textbf{monotonic}. We shall need this concept shortly. -\begin{isabelle} -\isacommand{lemma}\ "F\isasymsubseteq G\ \isasymLongrightarrow \ gterms\ F\ \isasymsubseteq \ gterms\ G"\isanewline -\isacommand{apply}\ clarify\isanewline -\isacommand{apply}\ (erule\ gterms.induct)\isanewline -\isacommand{apply}\ blast\isanewline -\isacommand{done} -\end{isabelle} -Intuitively, this theorem says that -enlarging the set of function symbols enlarges the set of ground -terms. The proof is a trivial rule induction. -First we use the \isa{clarify} method to assume the existence of an element of -\isa{terms~F}. (We could have used \isa{intro subsetI}.) We then -apply rule induction. Here is the resulting subgoal: -\begin{isabelle} -1.\ \isasymAnd x\ f\ args.\isanewline -\ \ \ \ \ \ \isasymlbrakk F\ \isasymsubseteq \ G;\ \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand \ t\ \isasymin \ gterms\ G;\ f\ \isasymin \ F\isasymrbrakk \isanewline -\ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G% -\end{isabelle} -% -The assumptions state that \isa{f} belongs -to~\isa{F}, which is included in~\isa{G}, and that every element of the list \isa{args} is -a ground term over~\isa{G}. The \isa{blast} method finds this chain of reasoning easily. - -\textit{Remark}: why do we call this function \isa{gterms} instead -of {\isa{gterm}}? Isabelle maintains separate name spaces for types -and constants, so there is no danger of confusion. However, name -clashes could arise in the theorems that Isabelle generates. -Our choice of names keeps {\isa{gterms.induct}} separate from {\isa{gterm.induct}}. - -\subsection{Rule inversion}\label{sec:rule-inversion} - -Case analysis on an inductive definition is called \textbf{rule inversion}. -It is frequently used in proofs about operational semantics. It can be -highly effective when it is applied automatically. Let us look at how rule -inversion is done in Isabelle. - -Recall that \isa{even} is the minimal set closed under these two rules: -\begin{isabelle} -0\ \isasymin \ even\isanewline -n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\ n))\ \isasymin -\ even -\end{isabelle} -Minimality means that \isa{even} contains only the elements that these -rules force it to contain. If we are told that \isa{a} -belongs to -\isa{even} then there are only two possibilities. Either \isa{a} is \isa{0} -or else \isa{a} has the form \isa{Suc(Suc~n)}, for an arbitrary \isa{n} -that belongs to -\isa{even}. That is the gist of the \isa{cases} rule, which Isabelle proves -for us when it accepts an inductive definition: -\begin{isabelle} -\isasymlbrakk a\ \isasymin \ even;\isanewline -\ a\ =\ 0\ \isasymLongrightarrow \ P;\isanewline -\ \isasymAnd n.\ \isasymlbrakk a\ =\ Suc(Suc\ n);\ n\ \isasymin \ -even\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk \ -\isasymLongrightarrow \ P -\rulename{even.cases} -\end{isabelle} - -This general rule is less useful than instances of it for -specific patterns. For example, if \isa{a} has the form -\isa{Suc(Suc~n)} then the first case becomes irrelevant, while the second -case tells us that \isa{n} belongs to \isa{even}. Isabelle will generate -this instance for us: -\begin{isabelle} -\isacommand{inductive\_cases}\ Suc_Suc_cases\ [elim!]: -\ "Suc(Suc\ n)\ \isasymin \ even" -\end{isabelle} -The \isacommand{inductive\_cases} command generates an instance of the -\isa{cases} rule for the supplied pattern and gives it the supplied name: -% -\begin{isabelle} -\isasymlbrakk Suc\ (Suc\ n)\ \isasymin \ even;\ n\ \isasymin \ even\ -\isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P% -\rulename{Suc_Suc_cases} -\end{isabelle} -% -Applying this as an elimination rule yields one case where \isa{even.cases} -would yield two. Rule inversion works well when the conclusions of the -introduction rules involve datatype constructors like \isa{Suc} and \isa{\#} -(list `cons'); freeness reasoning discards all but one or two cases. - -In the \isacommand{inductive\_cases} command we supplied an -attribute, \isa{elim!}, indicating that this elimination rule can be applied -aggressively. The original -\isa{cases} rule would loop if used in that manner because the -pattern~\isa{a} matches everything. - -The rule \isa{Suc_Suc_cases} is equivalent to the following implication: -\begin{isabelle} -Suc (Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ n\ \isasymin \ -even -\end{isabelle} -% -In \S\ref{sec:gen-rule-induction} we devoted some effort to proving precisely -this result. Yet we could have obtained it by a one-line declaration. -This example also justifies the terminology \textbf{rule inversion}: the new -rule inverts the introduction rule \isa{even.step}. - -For one-off applications of rule inversion, use the \isa{ind_cases} method. -Here is an example: -\begin{isabelle} -\isacommand{apply}\ (ind_cases\ "Suc(Suc\ n)\ \isasymin \ even") -\end{isabelle} -The specified instance of the \isa{cases} rule is generated, applied, and -discarded. - -\medskip -Let us try rule inversion on our ground terms example: -\begin{isabelle} -\isacommand{inductive\_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\ -\isasymin\ gterms\ F" -\end{isabelle} -% -Here is the result. No cases are discarded (there was only one to begin -with) but the rule applies specifically to the pattern \isa{Apply\ f\ args}. -It can be applied repeatedly as an elimination rule without looping, so we -have given the -\isa{elim!}\ attribute. -\begin{isabelle} -\isasymlbrakk Apply\ f\ args\ \isasymin \ gterms\ F;\isanewline -\ \isasymlbrakk -\isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F;\ f\ \isasymin -\ F\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk\isanewline -\isasymLongrightarrow \ P% -\rulename{gterm_Apply_elim} -\end{isabelle} - -This rule replaces an assumption about \isa{Apply\ f\ args} by -assumptions about \isa{f} and~\isa{args}. Here is a proof in which this -inference is essential. We show that if \isa{t} is a ground term over both -of the sets -\isa{F} and~\isa{G} then it is also a ground term over their intersection, -\isa{F\isasyminter G}. -\begin{isabelle} -\isacommand{lemma}\ gterms_IntI\ [rule_format]:\isanewline -\ \ \ \ \ "t\ \isasymin \ gterms\ F\ \isasymLongrightarrow \ t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\isasyminter G)"\isanewline -\isacommand{apply}\ (erule\ gterms.induct)\isanewline -\isacommand{apply}\ blast\isanewline -\isacommand{done} -\end{isabelle} -% -The proof begins with rule induction over the definition of -\isa{gterms}, which leaves a single subgoal: -\begin{isabelle} -1.\ \isasymAnd args\ f.\isanewline -\ \ \ \ \ \ \isasymlbrakk \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\ \isasyminter \ G));\isanewline -\ \ \ \ \ \ \ f\ \isasymin \ F\isasymrbrakk \isanewline -\ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ (F\ \isasyminter \ G) -\end{isabelle} -% -The induction hypothesis states that every element of \isa{args} belongs to -\isa{gterms\ (F\ \isasyminter \ G)} --- provided it already belongs to -\isa{gterms\ G}. How do we meet that condition? - -By assuming (as we may) the formula \isa{Apply\ f\ args\ \isasymin \ gterms\ -G}. Rule inversion, in the form of \isa{gterm_Apply_elim}, infers that every -element of \isa{args} belongs to -\isa{gterms~G}. It also yields \isa{f\ \isasymin \ G}, which will allow us -to conclude \isa{f\ \isasymin \ F\ \isasyminter \ G}. All of this reasoning -is done by \isa{blast}. - -\medskip - -To summarize, every inductive definition produces a \isa{cases} rule. The -\isacommand{inductive\_cases} command stores an instance of the \isa{cases} -rule for a given pattern. Within a proof, the \isa{ind_cases} method -applies an instance of the \isa{cases} -rule. - - -\subsection{Continuing the `ground terms' example} - -Call a term \textbf{well-formed} if each symbol occurring in it has -the correct number of arguments. To formalize this concept, we -introduce a function mapping each symbol to its arity, a natural -number. - -Let us define the set of well-formed ground terms. -Suppose we are given a function called \isa{arity}, specifying the arities to be used. -In the inductive step, we have a list \isa{args} of such terms and a function -symbol~\isa{f}. If the length of the list matches the function's arity -then applying \isa{f} to \isa{args} yields a well-formed term. -\begin{isabelle} -\isacommand{consts}\ well_formed_gterm\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline -\isacommand{inductive}\ "well_formed_gterm\ arity"\isanewline -\isakeyword{intros}\isanewline -step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ well_formed_gterm\ arity;\ \ \isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm\ -arity" -\end{isabelle} -% -The inductive definition neatly captures the reasoning above. -It is just an elaboration of the previous one, consisting of a single -introduction rule. The universal quantification over the -\isa{set} of arguments expresses that all of them are well-formed. - -\subsection{Alternative definition using a monotonic function} - -An inductive definition may refer to the inductively defined -set through an arbitrary monotonic function. To demonstrate this -powerful feature, let us -change the inductive definition above, replacing the -quantifier by a use of the function \isa{lists}. This -function, from the Isabelle library, is analogous to the -function \isa{gterms} declared above. If \isa{A} is a set then -{\isa{lists A}} is the set of lists whose elements belong to -\isa{A}. - -In the inductive definition of well-formed terms, examine the one -introduction rule. The first premise states that \isa{args} belongs to -the \isa{lists} of well-formed terms. This formulation is more -direct, if more obscure, than using a universal quantifier. -\begin{isabelle} -\isacommand{consts}\ well_formed_gterm'\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline -\isacommand{inductive}\ "well_formed_gterm'\ arity"\isanewline -\isakeyword{intros}\isanewline -step[intro!]:\ "\isasymlbrakk args\ \isasymin \ lists\ (well_formed_gterm'\ arity);\ \ \isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm'\ arity"\isanewline -\isakeyword{monos}\ lists_mono -\end{isabelle} - -We must cite the theorem \isa{lists_mono} in order to justify -using the function \isa{lists}. -\begin{isabelle} -A\ \isasymsubseteq\ B\ \isasymLongrightarrow \ lists\ A\ \isasymsubseteq -\ lists\ B\rulename{lists_mono} -\end{isabelle} -% -Why must the function be monotonic? An inductive definition describes -an iterative construction: each element of the set is constructed by a -finite number of introduction rule applications. For example, the -elements of \isa{even} are constructed by finitely many applications of -the rules -\begin{isabelle} -0\ \isasymin \ even\isanewline -n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\ n))\ \isasymin -\ even -\end{isabelle} -All references to a set in its -inductive definition must be positive. Applications of an -introduction rule cannot invalidate previous applications, allowing the -construction process to converge. -The following pair of rules do not constitute an inductive definition: -\begin{isabelle} -0\ \isasymin \ even\isanewline -n\ \isasymnotin \ even\ \isasymLongrightarrow \ (Suc\ n)\ \isasymin -\ even -\end{isabelle} -% -Showing that 4 is even using these rules requires showing that 3 is not -even. It is far from trivial to show that this set of rules -characterizes the even numbers. - -Even with its use of the function \isa{lists}, the premise of our -introduction rule is positive: -\begin{isabelle} -args\ \isasymin \ lists\ (well_formed_gterm'\ arity) -\end{isabelle} -To apply the rule we construct a list \isa{args} of previously -constructed well-formed terms. We obtain a -new term, \isa{Apply\ f\ args}. Because \isa{lists} is monotonic, -applications of the rule remain valid as new terms are constructed. -Further lists of well-formed -terms become available and none are taken away. - - -\subsection{A proof of equivalence} - -We naturally hope that these two inductive definitions of `well-formed' -coincide. The equality can be proved by separate inclusions in -each direction. Each is a trivial rule induction. -\begin{isabelle} -\isacommand{lemma}\ "well_formed_gterm\ arity\ \isasymsubseteq \ well_formed_gterm'\ arity"\isanewline -\isacommand{apply}\ clarify\isanewline -\isacommand{apply}\ (erule\ well_formed_gterm.induct)\isanewline -\isacommand{apply}\ auto\isanewline -\isacommand{done} -\end{isabelle} - -The \isa{clarify} method gives -us an element of \isa{well_formed_gterm\ arity} on which to perform -induction. The resulting subgoal can be proved automatically: -\begin{isabelle} -{\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline -\ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline -\ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline -\ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline -\ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity% -\end{isabelle} -% -This proof resembles the one given in -\S\ref{sec:gterm-datatype} above, especially in the form of the -induction hypothesis. Next, we consider the opposite inclusion: -\begin{isabelle} -\isacommand{lemma}\ "well_formed_gterm'\ arity\ \isasymsubseteq \ well_formed_gterm\ arity"\isanewline -\isacommand{apply}\ clarify\isanewline -\isacommand{apply}\ (erule\ well_formed_gterm'.induct)\isanewline -\isacommand{apply}\ auto\isanewline -\isacommand{done} -\end{isabelle} -% -The proof script is identical, but the subgoal after applying induction may -be surprising: -\begin{isabelle} -1.\ \isasymAnd x\ args\ f.\isanewline -\ \ \ \ \ \ \isasymlbrakk args\ \isasymin \ lists\ (well_formed_gterm'\ arity\ \isasyminter\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacharbraceleft u.\ u\ \isasymin \ well_formed_gterm\ arity\isacharbraceright );\isanewline -\ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline -\ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ well_formed_gterm\ arity% -\end{isabelle} -The induction hypothesis contains an application of \isa{lists}. Using a -monotonic function in the inductive definition always has this effect. The -subgoal may look uninviting, but fortunately a useful rewrite rule concerning -\isa{lists} is available: -\begin{isabelle} -lists\ (A\ \isasyminter \ B)\ =\ lists\ A\ \isasyminter \ lists\ B -\rulename{lists_Int_eq} -\end{isabelle} -% -Thanks to this default simplification rule, the induction hypothesis -is quickly replaced by its two parts: -\begin{isabelle} -\ \ \ \ \ \ \ args\ \isasymin \ lists\ (well_formed_gterm'\ arity)\isanewline -\ \ \ \ \ \ \ args\ \isasymin \ lists\ (well_formed_gterm\ arity) -\end{isabelle} -Invoking the rule \isa{well_formed_gterm.step} completes the proof. The -call to -\isa{auto} does all this work. - -This example is typical of how monotonic functions can be used. In -particular, a rewrite rule analogous to \isa{lists_Int_eq} holds in most -cases. Monotonicity implies one direction of this set equality; we have -this theorem: -\begin{isabelle} -mono\ f\ \isasymLongrightarrow \ f\ (A\ \isasyminter \ B)\ \isasymsubseteq \ -f\ A\ \isasyminter \ f\ B% -\rulename{mono_Int} -\end{isabelle} - - -To summarize: a universal quantifier in an introduction rule -lets it refer to any number of instances of -the inductively defined set. A monotonic function in an introduction -rule lets it refer to constructions over the inductively defined -set. Each element of an inductively defined set is created -through finitely many applications of the introduction rules. So each rule -must be positive, and never can it refer to \textit{infinitely} many -previous instances of the inductively defined set. - - - -\begin{exercise} -Prove this theorem, one direction of which was proved in -\S\ref{sec:rule-inversion} above. -\begin{isabelle} -\isacommand{lemma}\ gterms_Int_eq\ [simp]:\ "gterms\ (F\isasyminter G)\ =\ -gterms\ F\ \isasyminter \ gterms\ G"\isanewline -\end{isabelle} -\end{exercise} - - -\begin{exercise} -A function mapping function symbols to their -types is called a \textbf{signature}. Given a type -ranging over type symbols, we can represent a function's type by a -list of argument types paired with the result type. -Complete this inductive definition: -\begin{isabelle} -\isacommand{consts}\ well_typed_gterm::\ "('f\ \isasymRightarrow \ 't\ list\ *\ 't)\ \isasymRightarrow \ ('f\ gterm\ *\ 't)set"\isanewline -\isacommand{inductive}\ "well_typed_gterm\ sig"\isanewline -\end{isabelle} -\end{exercise} diff -r b254d5ad6dd4 -r ca2b00c4bba7 doc-src/TutorialI/Inductive/Even.tex --- a/doc-src/TutorialI/Inductive/Even.tex Fri Jan 12 16:07:20 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,223 +0,0 @@ -\section{The set of even numbers} - -The set of even numbers can be inductively defined as the least set -containing 0 and closed under the operation ${\cdots}+2$. Obviously, -\emph{even} can also be expressed using the divides relation (\isa{dvd}). -We shall prove below that the two formulations coincide. On the way we -shall examine the primary means of reasoning about inductively defined -sets: rule induction. - -\subsection{Making an inductive definition} - -Using \isacommand{consts}, we declare the constant \isa{even} to be a set -of natural numbers. The \isacommand{inductive} declaration gives it the -desired properties. -\begin{isabelle} -\isacommand{consts}\ even\ ::\ "nat\ set"\isanewline -\isacommand{inductive}\ even\isanewline -\isakeyword{intros}\isanewline -zero[intro!]:\ "0\ \isasymin \ even"\isanewline -step[intro!]:\ "n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\ -n))\ \isasymin \ even" -\end{isabelle} - -An inductive definition consists of introduction rules. The first one -above states that 0 is even; the second states that if $n$ is even, then so -is -$n+2$. Given this declaration, Isabelle generates a fixed point definition -for \isa{even} and proves theorems about it. These theorems include the -introduction rules specified in the declaration, an elimination rule for case -analysis and an induction rule. We can refer to these theorems by -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} -\end{isabelle} - -The introduction rules can be given attributes. Here both rules are -specified as \isa{intro!}, directing the classical reasoner to -apply them aggressively. Obviously, regarding 0 as even is safe. The -\isa{step} rule is also safe because $n+2$ is even if and only if $n$ is -even. We prove this equivalence later. - -\subsection{Using introduction rules} - -Our first lemma states that numbers of the form $2\times k$ are even. -Introduction rules are used to show that specific values belong to the -inductive set. Such proofs typically involve -induction, perhaps over some other inductive set. -\begin{isabelle} -\isacommand{lemma}\ two_times_even[intro!]:\ "\#2*k\ \isasymin \ even" -\isanewline -\isacommand{apply}\ (induct\ "k")\isanewline -\ \isacommand{apply}\ auto\isanewline -\isacommand{done} -\end{isabelle} -% -The first step is induction on the natural number \isa{k}, which leaves -two subgoals: -\begin{isabelle} -\ 1.\ \#2\ *\ 0\ \isasymin \ even\isanewline -\ 2.\ \isasymAnd n.\ \#2\ *\ n\ \isasymin \ even\ \isasymLongrightarrow \ \#2\ *\ Suc\ n\ \isasymin \ even -\end{isabelle} -% -Here \isa{auto} simplifies both subgoals so that they match the introduction -rules, which are then applied automatically. - -Our ultimate goal is to prove the equivalence between the traditional -definition of \isa{even} (using the divides relation) and our inductive -definition. One direction of this equivalence is immediate by the lemma -just proved, whose \isa{intro!} attribute ensures it will be used. -\begin{isabelle} -\isacommand{lemma}\ dvd_imp_even:\ "\#2\ dvd\ n\ \isasymLongrightarrow \ n\ \isasymin \ even"\isanewline -\isacommand{apply}\ (auto\ simp\ add:\ dvd_def)\isanewline -\isacommand{done} -\end{isabelle} - -\subsection{Rule induction} -\label{sec:rule-induction} - -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 -\ \isacommand{apply}\ simp\isanewline -\isacommand{apply}\ (simp\ add:\ dvd_def)\isanewline -\isacommand{apply}\ clarify\isanewline -\isacommand{apply}\ (rule_tac\ x\ =\ "Suc\ k"\ \isakeyword{in}\ exI)\isanewline -\isacommand{apply}\ simp\isanewline -\isacommand{done} -\end{isabelle} -% -We begin by applying induction. Note that \isa{even.induct} has the form -of an elimination rule, so we use the method \isa{erule}. We get two -subgoals: -\begin{isabelle} -\ 1.\ \#2\ dvd\ 0\isanewline -\ 2.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ \#2\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ \#2\ dvd\ Suc\ (Suc\ n) -\end{isabelle} -% -The first subgoal is trivial (by \isa{simp}). For the second -subgoal, we unfold the definition of \isa{dvd}: -\begin{isabelle} -\ 1.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ \isasymexists k.\ -n\ =\ \#2\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ -Suc\ (Suc\ n)\ =\ \#2\ *\ k -\end{isabelle} -% -Then we use -\isa{clarify} to eliminate the existential quantifier from the assumption -and replace \isa{n} by \isa{\#2\ *\ k}. -\begin{isabelle} -\ 1.\ \isasymAnd n\ k.\ \#2\ *\ k\ \isasymin \ even\ \isasymLongrightarrow \ \isasymexists ka.\ Suc\ (Suc\ (\#2\ *\ k))\ =\ \#2\ *\ ka% -\end{isabelle} -% -The \isa{rule_tac\ldots exI} tells Isabelle that the desired -\isa{ka} is -\isa{Suc\ k}. With this hint, the subgoal becomes trivial, and \isa{simp} -concludes the proof. - -\medskip -Combining the previous two results yields our objective, the -equivalence relating \isa{even} and \isa{dvd}. -% -%we don't want [iff]: discuss? -\begin{isabelle} -\isacommand{theorem}\ even_iff_dvd:\ "(n\ \isasymin \ even)\ =\ (\#2\ dvd\ n)"\isanewline -\isacommand{apply}\ (blast\ intro:\ dvd_imp_even\ even_imp_dvd)\isanewline -\isacommand{done} -\end{isabelle} - -\subsection{Generalization and rule induction} -\label{sec:gen-rule-induction} - -Everybody knows that when before applying induction we often must generalize -the induction formula. This step is just as important with rule induction, -and the required generalizations can be complicated. In this -example, the obvious statement of the result is not inductive: -% -\begin{isabelle} -\isacommand{lemma}\ "Suc\ (Suc\ n)\ \isasymin \ even\ -\isasymLongrightarrow \ n\ \isasymin \ even"\isanewline -\isacommand{apply}\ (erule\ even.induct)\isanewline -\isacommand{oops} -\end{isabelle} -% -Rule induction finds no occurrences of \isa{Suc\ (Suc\ n)} in the -conclusion, which it therefore leaves unchanged. (Look at -\isa{even.induct} to see why this happens.) We get these subgoals: -\begin{isabelle} -\ 1.\ n\ \isasymin \ even\isanewline -\ 2.\ \isasymAnd na.\ \isasymlbrakk na\ \isasymin \ even;\ n\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ n\ \isasymin \ even% -\end{isabelle} -The first one is hopeless. In general, rule inductions involving -non-trivial terms will probably go wrong. How to deal with such situations -in general is described in {\S}\ref{sec:ind-var-in-prems} below. -In the current case the solution is easy because -we have the necessary inverse, subtraction: -\begin{isabelle} -\isacommand{lemma}\ even_imp_even_minus_2:\ "n\ \isasymin \ even\ \isasymLongrightarrow \ n-\#2\ \isasymin \ even"\isanewline -\isacommand{apply}\ (erule\ even.induct)\isanewline -\ \isacommand{apply}\ auto\isanewline -\isacommand{done} -\end{isabelle} -% -This lemma is trivially inductive. Here are the subgoals: -\begin{isabelle} -\ 1.\ 0\ -\ \#2\ \isasymin \ even\isanewline -\ 2.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ n\ -\ \#2\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ Suc\ (Suc\ n)\ -\ \#2\ \isasymin \ even% -\end{isabelle} -The first is trivial because \isa{0\ -\ \#2} simplifies to \isa{0}, which is -even. The second is trivial too: \isa{Suc\ (Suc\ n)\ -\ \#2} simplifies to -\isa{n}, matching the assumption. - -\medskip -Using our lemma, we can easily prove the result we originally wanted: -\begin{isabelle} -\isacommand{lemma}\ Suc_Suc_even_imp_even:\ "Suc\ (Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ n\ \isasymin \ even"\isanewline -\isacommand{apply}\ (drule\ even_imp_even_minus_2)\isanewline -\isacommand{apply}\ simp\isanewline -\isacommand{done} -\end{isabelle} - -We have just proved the converse of the introduction rule \isa{even.step}. -This suggests proving the following equivalence. We give it the \isa{iff} -attribute because of its obvious value for simplification. -\begin{isabelle} -\isacommand{lemma}\ [iff]:\ "((Suc\ (Suc\ n))\ \isasymin \ even)\ =\ (n\ -\isasymin \ even)"\isanewline -\isacommand{apply}\ (blast\ dest:\ Suc_Suc_even_imp_even)\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. diff -r b254d5ad6dd4 -r ca2b00c4bba7 doc-src/TutorialI/Inductive/advanced-examples.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Inductive/advanced-examples.tex Fri Jan 12 16:09:33 2001 +0100 @@ -0,0 +1,434 @@ +% $Id$ +This section describes advanced features of inductive definitions. +The premises of introduction rules may contain universal quantifiers and +monotonic functions. Theorems may be proved by rule inversion. + +\subsection{Universal Quantifiers in Introduction Rules} +\label{sec:gterm-datatype} + +As a running example, this section develops the theory of \textbf{ground +terms}: terms constructed from constant and function +symbols but not variables. To simplify matters further, we regard a +constant as a function applied to the null argument list. Let us declare a +datatype \isa{gterm} for the type of ground terms. It is a type constructor +whose argument is a type of function symbols. +\begin{isabelle} +\isacommand{datatype}\ 'f\ gterm\ =\ Apply\ 'f\ "'f\ gterm\ list" +\end{isabelle} +To try it out, we declare a datatype of some integer operations: +integer constants, the unary minus operator and the addition +operator. +\begin{isabelle} +\isacommand{datatype}\ integer_op\ =\ Number\ int\ |\ UnaryMinus\ |\ Plus +\end{isabelle} +Now the type \isa{integer\_op gterm} denotes the ground +terms built over those symbols. + +The type constructor \texttt{gterm} can be generalized to a function +over sets. It returns +the set of ground terms that can be formed over a set \isa{F} of function symbols. For +example, we could consider the set of ground terms formed from the finite +set {\isa{\{Number 2, UnaryMinus, Plus\}}}. + +This concept is inductive. If we have a list \isa{args} of ground terms +over~\isa{F} and a function symbol \isa{f} in \isa{F}, then we +can apply \isa{f} to \isa{args} to obtain another ground term. +The only difficulty is that the argument list may be of any length. Hitherto, +each rule in an inductive definition referred to the inductively +defined set a fixed number of times, typically once or twice. +A universal quantifier in the premise of the introduction rule +expresses that every element of \isa{args} belongs +to our inductively defined set: is a ground term +over~\isa{F}. The function {\isa{set}} denotes the set of elements in a given +list. +\begin{isabelle} +\isacommand{consts}\ gterms\ ::\ "'f\ set\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline +\isacommand{inductive}\ "gterms\ F"\isanewline +\isakeyword{intros}\isanewline +step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ gterms\ F;\ \ f\ \isasymin \ F\isasymrbrakk \isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ gterms\ +F" +\end{isabelle} + +To demonstrate a proof from this definition, let us +show that the function \isa{gterms} +is \textbf{monotonic}. We shall need this concept shortly. +\begin{isabelle} +\isacommand{lemma}\ gterms_mono:\ "F\isasymsubseteq G\ \isasymLongrightarrow \ gterms\ F\ \isasymsubseteq \ gterms\ G"\isanewline +\isacommand{apply}\ clarify\isanewline +\isacommand{apply}\ (erule\ gterms.induct)\isanewline +\isacommand{apply}\ blast\isanewline +\isacommand{done} +\end{isabelle} +Intuitively, this theorem says that +enlarging the set of function symbols enlarges the set of ground +terms. The proof is a trivial rule induction. +First we use the \isa{clarify} method to assume the existence of an element of +\isa{terms~F}. (We could have used \isa{intro subsetI}.) We then +apply rule induction. Here is the resulting subgoal: +\begin{isabelle} +\ 1.\ \isasymAnd x\ args\ f.\isanewline +\ \ \ \ \ \ \ \isasymlbrakk F\ \isasymsubseteq \ G;\ \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand \ t\ \isasymin \ gterms\ G;\ f\ \isasymin \ F\isasymrbrakk \isanewline +\ \ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G% +\end{isabelle} +% +The assumptions state that \isa{f} belongs +to~\isa{F}, which is included in~\isa{G}, and that every element of the list \isa{args} is +a ground term over~\isa{G}. The \isa{blast} method finds this chain of reasoning easily. + +\begin{warn} +Why do we call this function \isa{gterms} instead +of {\isa{gterm}}? A constant may have the same name as a type. However, +name clashes could arise in the theorems that Isabelle generates. +Our choice of names keeps {\isa{gterms.induct}} separate from +{\isa{gterm.induct}}. +\end{warn} + + +\subsection{Rule Inversion}\label{sec:rule-inversion} + +Case analysis on an inductive definition is called \textbf{rule inversion}. +It is frequently used in proofs about operational semantics. It can be +highly effective when it is applied automatically. Let us look at how rule +inversion is done in Isabelle. + +Recall that \isa{even} is the minimal set closed under these two rules: +\begin{isabelle} +0\ \isasymin \ even\isanewline +n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\ n))\ \isasymin +\ even +\end{isabelle} +Minimality means that \isa{even} contains only the elements that these +rules force it to contain. If we are told that \isa{a} +belongs to +\isa{even} then there are only two possibilities. Either \isa{a} is \isa{0} +or else \isa{a} has the form \isa{Suc(Suc~n)}, for an arbitrary \isa{n} +that belongs to +\isa{even}. That is the gist of the \isa{cases} rule, which Isabelle proves +for us when it accepts an inductive definition: +\begin{isabelle} +\isasymlbrakk a\ \isasymin \ even;\isanewline +\ a\ =\ 0\ \isasymLongrightarrow \ P;\isanewline +\ \isasymAnd n.\ \isasymlbrakk a\ =\ Suc(Suc\ n);\ n\ \isasymin \ +even\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk \ +\isasymLongrightarrow \ P +\rulename{even.cases} +\end{isabelle} + +This general rule is less useful than instances of it for +specific patterns. For example, if \isa{a} has the form +\isa{Suc(Suc~n)} then the first case becomes irrelevant, while the second +case tells us that \isa{n} belongs to \isa{even}. Isabelle will generate +this instance for us: +\begin{isabelle} +\isacommand{inductive\_cases}\ Suc_Suc_cases\ [elim!]: +\ "Suc(Suc\ n)\ \isasymin \ even" +\end{isabelle} +The \isacommand{inductive\_cases} command generates an instance of the +\isa{cases} rule for the supplied pattern and gives it the supplied name: +% +\begin{isabelle} +\isasymlbrakk Suc\ (Suc\ n)\ \isasymin \ even;\ n\ \isasymin \ even\ +\isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P% +\rulename{Suc_Suc_cases} +\end{isabelle} +% +Applying this as an elimination rule yields one case where \isa{even.cases} +would yield two. Rule inversion works well when the conclusions of the +introduction rules involve datatype constructors like \isa{Suc} and \isa{\#} +(list `cons'); freeness reasoning discards all but one or two cases. + +In the \isacommand{inductive\_cases} command we supplied an +attribute, \isa{elim!}, indicating that this elimination rule can be applied +aggressively. The original +\isa{cases} rule would loop if used in that manner because the +pattern~\isa{a} matches everything. + +The rule \isa{Suc_Suc_cases} is equivalent to the following implication: +\begin{isabelle} +Suc (Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ n\ \isasymin \ +even +\end{isabelle} +% +In {\S}\ref{sec:gen-rule-induction} we devoted some effort to proving precisely +this result. Yet we could have obtained it by a one-line declaration. +This example also justifies the terminology \textbf{rule inversion}: the new +rule inverts the introduction rule \isa{even.step}. + +For one-off applications of rule inversion, use the \isa{ind_cases} method. +Here is an example: +\begin{isabelle} +\isacommand{apply}\ (ind_cases\ "Suc(Suc\ n)\ \isasymin \ even") +\end{isabelle} +The specified instance of the \isa{cases} rule is generated, applied, and +discarded. + +\medskip +Let us try rule inversion on our ground terms example: +\begin{isabelle} +\isacommand{inductive\_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\ +\isasymin\ gterms\ F" +\end{isabelle} +% +Here is the result. No cases are discarded (there was only one to begin +with) but the rule applies specifically to the pattern \isa{Apply\ f\ args}. +It can be applied repeatedly as an elimination rule without looping, so we +have given the +\isa{elim!}\ attribute. +\begin{isabelle} +\isasymlbrakk Apply\ f\ args\ \isasymin \ gterms\ F;\isanewline +\ \isasymlbrakk +\isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F;\ f\ \isasymin +\ F\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk\isanewline +\isasymLongrightarrow \ P% +\rulename{gterm_Apply_elim} +\end{isabelle} + +This rule replaces an assumption about \isa{Apply\ f\ args} by +assumptions about \isa{f} and~\isa{args}. Here is a proof in which this +inference is essential. We show that if \isa{t} is a ground term over both +of the sets +\isa{F} and~\isa{G} then it is also a ground term over their intersection, +\isa{F\isasyminter G}. +\begin{isabelle} +\isacommand{lemma}\ gterms_IntI\ [rule_format]:\isanewline +\ \ \ \ \ "t\ \isasymin \ gterms\ F\ \isasymLongrightarrow \ t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\isasyminter G)"\isanewline +\isacommand{apply}\ (erule\ gterms.induct)\isanewline +\isacommand{apply}\ blast\isanewline +\isacommand{done} +\end{isabelle} +% +The proof begins with rule induction over the definition of +\isa{gterms}, which leaves a single subgoal: +\begin{isabelle} +1.\ \isasymAnd args\ f.\isanewline +\ \ \ \ \ \ \isasymlbrakk \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\ \isasyminter \ G));\isanewline +\ \ \ \ \ \ \ f\ \isasymin \ F\isasymrbrakk \isanewline +\ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ (F\ \isasyminter \ G) +\end{isabelle} +% +The induction hypothesis states that every element of \isa{args} belongs to +\isa{gterms\ (F\ \isasyminter \ G)} --- provided it already belongs to +\isa{gterms\ G}. How do we meet that condition? + +By assuming (as we may) the formula \isa{Apply\ f\ args\ \isasymin \ gterms\ +G}. Rule inversion, in the form of \isa{gterm_Apply_elim}, infers that every +element of \isa{args} belongs to +\isa{gterms~G}. It also yields \isa{f\ \isasymin \ G}, which will allow us +to conclude \isa{f\ \isasymin \ F\ \isasyminter \ G}. All of this reasoning +is done by \isa{blast}. + +\medskip + +To summarize, every inductive definition produces a \isa{cases} rule. The +\isacommand{inductive\_cases} command stores an instance of the \isa{cases} +rule for a given pattern. Within a proof, the \isa{ind_cases} method +applies an instance of the \isa{cases} +rule. + + +\subsection{Continuing the Ground Terms Example} + +Call a term \textbf{well-formed} if each symbol occurring in it has +the correct number of arguments. To formalize this concept, we +introduce a function mapping each symbol to its \textbf{arity}, a natural +number. + +Let us define the set of well-formed ground terms. +Suppose we are given a function called \isa{arity}, specifying the arities to be used. +In the inductive step, we have a list \isa{args} of such terms and a function +symbol~\isa{f}. If the length of the list matches the function's arity +then applying \isa{f} to \isa{args} yields a well-formed term. +\begin{isabelle} +\isacommand{consts}\ well_formed_gterm\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline +\isacommand{inductive}\ "well_formed_gterm\ arity"\isanewline +\isakeyword{intros}\isanewline +step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ well_formed_gterm\ arity;\ \ \isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm\ +arity" +\end{isabelle} +% +The inductive definition neatly captures the reasoning above. +It is just an elaboration of the previous one, consisting of a single +introduction rule. The universal quantification over the +\isa{set} of arguments expresses that all of them are well-formed. + +\subsection{Alternative Definition Using a Monotonic Function} + +An inductive definition may refer to the inductively defined +set through an arbitrary monotonic function. To demonstrate this +powerful feature, let us +change the inductive definition above, replacing the +quantifier by a use of the function \isa{lists}. This +function, from the Isabelle theory of lists, is analogous to the +function \isa{gterms} declared above: if \isa{A} is a set then +{\isa{lists A}} is the set of lists whose elements belong to +\isa{A}. + +In the inductive definition of well-formed terms, examine the one +introduction rule. The first premise states that \isa{args} belongs to +the \isa{lists} of well-formed terms. This formulation is more +direct, if more obscure, than using a universal quantifier. +\begin{isabelle} +\isacommand{consts}\ well_formed_gterm'\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline +\isacommand{inductive}\ "well_formed_gterm'\ arity"\isanewline +\isakeyword{intros}\isanewline +step[intro!]:\ "\isasymlbrakk args\ \isasymin \ lists\ (well_formed_gterm'\ arity);\ \ \isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm'\ arity"\isanewline +\isakeyword{monos}\ lists_mono +\end{isabelle} + +We must cite the theorem \isa{lists_mono} in order to justify +using the function \isa{lists}. +\begin{isabelle} +A\ \isasymsubseteq\ B\ \isasymLongrightarrow \ lists\ A\ \isasymsubseteq +\ lists\ B\rulename{lists_mono} +\end{isabelle} +% +Why must the function be monotonic? An inductive definition describes +an iterative construction: each element of the set is constructed by a +finite number of introduction rule applications. For example, the +elements of \isa{even} are constructed by finitely many applications of +the rules +\begin{isabelle} +0\ \isasymin \ even\isanewline +n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\ n))\ \isasymin +\ even +\end{isabelle} +All references to a set in its +inductive definition must be positive. Applications of an +introduction rule cannot invalidate previous applications, allowing the +construction process to converge. +The following pair of rules do not constitute an inductive definition: +\begin{isabelle} +0\ \isasymin \ even\isanewline +n\ \isasymnotin \ even\ \isasymLongrightarrow \ (Suc\ n)\ \isasymin +\ even +\end{isabelle} +% +Showing that 4 is even using these rules requires showing that 3 is not +even. It is far from trivial to show that this set of rules +characterizes the even numbers. + +Even with its use of the function \isa{lists}, the premise of our +introduction rule is positive: +\begin{isabelle} +args\ \isasymin \ lists\ (well_formed_gterm'\ arity) +\end{isabelle} +To apply the rule we construct a list \isa{args} of previously +constructed well-formed terms. We obtain a +new term, \isa{Apply\ f\ args}. Because \isa{lists} is monotonic, +applications of the rule remain valid as new terms are constructed. +Further lists of well-formed +terms become available and none are taken away. + + +\subsection{A Proof of Equivalence} + +We naturally hope that these two inductive definitions of ``well-formed'' +coincide. The equality can be proved by separate inclusions in +each direction. Each is a trivial rule induction. +\begin{isabelle} +\isacommand{lemma}\ "well_formed_gterm\ arity\ \isasymsubseteq \ well_formed_gterm'\ arity"\isanewline +\isacommand{apply}\ clarify\isanewline +\isacommand{apply}\ (erule\ well_formed_gterm.induct)\isanewline +\isacommand{apply}\ auto\isanewline +\isacommand{done} +\end{isabelle} + +The \isa{clarify} method gives +us an element of \isa{well_formed_gterm\ arity} on which to perform +induction. The resulting subgoal can be proved automatically: +\begin{isabelle} +{\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline +\ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline +\ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline +\ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity% +\end{isabelle} +% +This proof resembles the one given in +{\S}\ref{sec:gterm-datatype} above, especially in the form of the +induction hypothesis. Next, we consider the opposite inclusion: +\begin{isabelle} +\isacommand{lemma}\ "well_formed_gterm'\ arity\ \isasymsubseteq \ well_formed_gterm\ arity"\isanewline +\isacommand{apply}\ clarify\isanewline +\isacommand{apply}\ (erule\ well_formed_gterm'.induct)\isanewline +\isacommand{apply}\ auto\isanewline +\isacommand{done} +\end{isabelle} +% +The proof script is identical, but the subgoal after applying induction may +be surprising: +\begin{isabelle} +1.\ \isasymAnd x\ args\ f.\isanewline +\ \ \ \ \ \ \isasymlbrakk args\ \isasymin \ lists\ (well_formed_gterm'\ arity\ \isasyminter\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacharbraceleft u.\ u\ \isasymin \ well_formed_gterm\ arity\isacharbraceright );\isanewline +\ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline +\ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ well_formed_gterm\ arity% +\end{isabelle} +The induction hypothesis contains an application of \isa{lists}. Using a +monotonic function in the inductive definition always has this effect. The +subgoal may look uninviting, but fortunately a useful rewrite rule concerning +\isa{lists} is available: +\begin{isabelle} +lists\ (A\ \isasyminter \ B)\ =\ lists\ A\ \isasyminter \ lists\ B +\rulename{lists_Int_eq} +\end{isabelle} +% +Thanks to this default simplification rule, the induction hypothesis +is quickly replaced by its two parts: +\begin{isabelle} +\ \ \ \ \ \ \ args\ \isasymin \ lists\ (well_formed_gterm'\ arity)\isanewline +\ \ \ \ \ \ \ args\ \isasymin \ lists\ (well_formed_gterm\ arity) +\end{isabelle} +Invoking the rule \isa{well_formed_gterm.step} completes the proof. The +call to +\isa{auto} does all this work. + +This example is typical of how monotonic functions can be used. In +particular, a rewrite rule analogous to \isa{lists_Int_eq} holds in most +cases. Monotonicity implies one direction of this set equality; we have +this theorem: +\begin{isabelle} +mono\ f\ \isasymLongrightarrow \ f\ (A\ \isasyminter \ B)\ \isasymsubseteq \ +f\ A\ \isasyminter \ f\ B% +\rulename{mono_Int} +\end{isabelle} + + +To summarize: a universal quantifier in an introduction rule +lets it refer to any number of instances of +the inductively defined set. A monotonic function in an introduction +rule lets it refer to constructions over the inductively defined +set. Each element of an inductively defined set is created +through finitely many applications of the introduction rules. So each rule +must be positive, and never can it refer to \textit{infinitely} many +previous instances of the inductively defined set. + + + +\begin{exercise} +Prove this theorem, one direction of which was proved in +{\S}\ref{sec:rule-inversion} above. +\begin{isabelle} +\isacommand{lemma}\ gterms_Int_eq\ [simp]:\ "gterms\ (F\isasyminter G)\ =\ +gterms\ F\ \isasyminter \ gterms\ G"\isanewline +\end{isabelle} +\end{exercise} + + +\begin{exercise} +A function mapping function symbols to their +types is called a \textbf{signature}. Given a type +ranging over type symbols, we can represent a function's type by a +list of argument types paired with the result type. +Complete this inductive definition: +\begin{isabelle} +\isacommand{consts}\ well_typed_gterm::\ "('f\ \isasymRightarrow \ 't\ list\ *\ 't)\ \isasymRightarrow \ ('f\ gterm\ *\ 't)set"\isanewline +\isacommand{inductive}\ "well_typed_gterm\ sig"\isanewline +\end{isabelle} +\end{exercise} diff -r b254d5ad6dd4 -r ca2b00c4bba7 doc-src/TutorialI/Inductive/even-example.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Inductive/even-example.tex Fri Jan 12 16:09:33 2001 +0100 @@ -0,0 +1,222 @@ +% $Id$ +\section{The Set of Even Numbers} + +The set of even numbers can be inductively defined as the least set +containing 0 and closed under the operation ${\cdots}+2$. Obviously, +\emph{even} can also be expressed using the divides relation (\isa{dvd}). +We shall prove below that the two formulations coincide. On the way we +shall examine the primary means of reasoning about inductively defined +sets: rule induction. + +\subsection{Making an Inductive Definition} + +Using \isacommand{consts}, we declare the constant \isa{even} to be a set +of natural numbers. The \isacommand{inductive} declaration gives it the +desired properties. +\begin{isabelle} +\isacommand{consts}\ even\ ::\ "nat\ set"\isanewline +\isacommand{inductive}\ even\isanewline +\isakeyword{intros}\isanewline +zero[intro!]:\ "0\ \isasymin \ even"\isanewline +step[intro!]:\ "n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\ +n))\ \isasymin \ even" +\end{isabelle} + +An inductive definition consists of introduction rules. The first one +above states that 0 is even; the second states that if $n$ is even, then so +is +$n+2$. Given this declaration, Isabelle generates a fixed point definition +for \isa{even} and proves theorems about it. These theorems include the +introduction rules specified in the declaration, an elimination rule for case +analysis and an induction rule. We can refer to these theorems by +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} +\end{isabelle} + +The introduction rules can be given attributes. Here both rules are +specified as \isa{intro!}, directing the classical reasoner to +apply them aggressively. Obviously, regarding 0 as even is safe. The +\isa{step} rule is also safe because $n+2$ is even if and only if $n$ is +even. We prove this equivalence later. + +\subsection{Using Introduction Rules} + +Our first lemma states that numbers of the form $2\times k$ are even. +Introduction rules are used to show that specific values belong to the +inductive set. Such proofs typically involve +induction, perhaps over some other inductive set. +\begin{isabelle} +\isacommand{lemma}\ two_times_even[intro!]:\ "\#2*k\ \isasymin \ even" +\isanewline +\isacommand{apply}\ (induct\ "k")\isanewline +\ \isacommand{apply}\ auto\isanewline +\isacommand{done} +\end{isabelle} +% +The first step is induction on the natural number \isa{k}, which leaves +two subgoals: +\begin{isabelle} +\ 1.\ \#2\ *\ 0\ \isasymin \ even\isanewline +\ 2.\ \isasymAnd n.\ \#2\ *\ n\ \isasymin \ even\ \isasymLongrightarrow \ \#2\ *\ Suc\ n\ \isasymin \ even +\end{isabelle} +% +Here \isa{auto} simplifies both subgoals so that they match the introduction +rules, which are then applied automatically. + +Our ultimate goal is to prove the equivalence between the traditional +definition of \isa{even} (using the divides relation) and our inductive +definition. One direction of this equivalence is immediate by the lemma +just proved, whose \isa{intro!} attribute ensures it will be used. +\begin{isabelle} +\isacommand{lemma}\ dvd_imp_even:\ "\#2\ dvd\ n\ \isasymLongrightarrow \ n\ \isasymin \ even"\isanewline +\isacommand{by}\ (auto\ simp\ add:\ dvd_def) +\end{isabelle} + +\subsection{Rule Induction} +\label{sec:rule-induction} + +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" +\end{isabelle} +% +We begin by applying induction. Note that \isa{even.induct} has the form +of an elimination rule, so we use the method \isa{erule}. We get two +subgoals: +\begin{isabelle} +\isacommand{apply}\ (erule\ even.induct) +\isanewline\isanewline +\ 1.\ \#2\ dvd\ 0\isanewline +\ 2.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ \#2\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ \#2\ dvd\ Suc\ (Suc\ n) +\end{isabelle} +% +We unfold the definition of \isa{dvd} in both subgoals, proving the first +one and simplifying the second: +\begin{isabelle} +\isacommand{apply}\ (simp_all\ add:\ dvd_def) +\isanewline\isanewline +\ 1.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ \isasymexists k.\ +n\ =\ \#2\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ +Suc\ (Suc\ n)\ =\ \#2\ *\ k +\end{isabelle} +% +The next command eliminates the existential quantifier from the assumption +and replaces \isa{n} by \isa{\#2\ *\ k}. +\begin{isabelle} +\isacommand{apply}\ clarify +\isanewline\isanewline +\ 1.\ \isasymAnd n\ k.\ \#2\ *\ k\ \isasymin \ even\ \isasymLongrightarrow \ \isasymexists ka.\ Suc\ (Suc\ (\#2\ *\ k))\ =\ \#2\ *\ ka% +\end{isabelle} +% +To conclude, we tell Isabelle that the desired value is +\isa{Suc\ k}. With this hint, the subgoal falls to \isa{simp}. +\begin{isabelle} +\isacommand{apply}\ (rule_tac\ x\ =\ "Suc\ k"\ \isakeyword{in}\ exI, +\isacommand{apply}\ simp) +\end{isabelle} + + +\medskip +Combining the previous two results yields our objective, the +equivalence relating \isa{even} and \isa{dvd}. +% +%we don't want [iff]: discuss? +\begin{isabelle} +\isacommand{theorem}\ even_iff_dvd:\ "(n\ \isasymin \ even)\ =\ (\#2\ dvd\ n)"\isanewline +\isacommand{by}\ (blast\ intro:\ dvd_imp_even\ even_imp_dvd) +\end{isabelle} + + +\subsection{Generalization and Rule Induction} +\label{sec:gen-rule-induction} + +Before applying induction, we typically must generalize +the induction formula. With rule induction, the required generalization +can be hard to find and sometimes requires a complete reformulation of the +problem. In this example, the obvious statement of the result is not +inductive: +% +\begin{isabelle} +\isacommand{lemma}\ "Suc\ (Suc\ n)\ \isasymin \ even\ +\isasymLongrightarrow \ n\ \isasymin \ even"\isanewline +\isacommand{apply}\ (erule\ even.induct)\isanewline +\isacommand{oops} +\end{isabelle} +% +Rule induction finds no occurrences of \isa{Suc(Suc\ n)} in the +conclusion, which it therefore leaves unchanged. (Look at +\isa{even.induct} to see why this happens.) We have these subgoals: +\begin{isabelle} +\ 1.\ n\ \isasymin \ even\isanewline +\ 2.\ \isasymAnd na.\ \isasymlbrakk na\ \isasymin \ even;\ n\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ n\ \isasymin \ even% +\end{isabelle} +The first one is hopeless. Rule inductions involving +non-trivial terms usually fail. How to deal with such situations +in general is described in {\S}\ref{sec:ind-var-in-prems} below. +In the current case the solution is easy because +we have the necessary inverse, subtraction: +\begin{isabelle} +\isacommand{lemma}\ even_imp_even_minus_2:\ "n\ \isasymin \ even\ \isasymLongrightarrow \ n-\#2\ \isasymin \ even"\isanewline +\isacommand{apply}\ (erule\ even.induct)\isanewline +\ \isacommand{apply}\ auto\isanewline +\isacommand{done} +\end{isabelle} +% +This lemma is trivially inductive. Here are the subgoals: +\begin{isabelle} +\ 1.\ 0\ -\ \#2\ \isasymin \ even\isanewline +\ 2.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ n\ -\ \#2\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ Suc\ (Suc\ n)\ -\ \#2\ \isasymin \ even% +\end{isabelle} +The first is trivial because \isa{0\ -\ \#2} simplifies to \isa{0}, which is +even. The second is trivial too: \isa{Suc\ (Suc\ n)\ -\ \#2} simplifies to +\isa{n}, matching the assumption. + +\medskip +Using our lemma, we can easily prove the result we originally wanted: +\begin{isabelle} +\isacommand{lemma}\ Suc_Suc_even_imp_even:\ "Suc\ (Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ n\ \isasymin \ even"\isanewline +\isacommand{by}\ (drule\ even_imp_even_minus_2, \isacommand{apply}\ simp) +\end{isabelle} + +We have just proved the converse of the introduction rule \isa{even.step}. +This suggests proving the following equivalence. We give it the \isa{iff} +attribute because of its obvious value for simplification. +\begin{isabelle} +\isacommand{lemma}\ [iff]:\ "((Suc\ (Suc\ n))\ \isasymin \ even)\ =\ (n\ +\isasymin \ even)"\isanewline +\isacommand{by}\ (blast\ dest:\ Suc_Suc_even_imp_even) +\end{isabelle} + +The even numbers example has shown how inductive definitions can be used. +Later examples will show that they are actually worth using.