# HG changeset patch # User berghofe # Date 1184852136 -7200 # Node ID ca73e86c22bba845669cf69632a9bae7b4b2ada6 # Parent 32d76edc5e5cb523fdfb7a934f01b2e6f285eb51 updated diff -r 32d76edc5e5c -r ca73e86c22bb doc-src/TutorialI/Inductive/document/Advanced.tex --- a/doc-src/TutorialI/Inductive/document/Advanced.tex Thu Jul 19 15:35:00 2007 +0200 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Thu Jul 19 15:35:36 2007 +0200 @@ -3,36 +3,90 @@ \def\isabellecontext{Advanced}% % \isadelimtheory -\isanewline % \endisadelimtheory % \isatagtheory -\isacommand{theory}\isamarkupfalse% -\ Advanced\ \isakeyword{imports}\ Even\ \isakeyword{begin}% +% \endisatagtheory {\isafoldtheory}% % \isadelimtheory -\isanewline % \endisadelimtheory -\isanewline -\isanewline +% +\begin{isamarkuptext}% +The premises of introduction rules may contain universal quantifiers and +monotone functions. A universal quantifier lets the rule +refer to any number of instances of +the inductively defined set. A monotone function lets the rule refer +to existing constructions (such as ``list of'') over the inductively defined +set. The examples below show how to use the additional expressiveness +and how to reason from the resulting definitions.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Universal Quantifiers in Introduction Rules \label{sec:gterm-datatype}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\index{ground terms example|(}% +\index{quantifiers!and inductive definitions|(}% +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.% +\end{isamarkuptext}% +\isamarkuptrue% \isacommand{datatype}\isamarkupfalse% -\ {\isacharprime}f\ gterm\ {\isacharequal}\ Apply\ {\isacharprime}f\ {\isachardoublequoteopen}{\isacharprime}f\ gterm\ list{\isachardoublequoteclose}\isanewline -\isanewline +\ {\isacharprime}f\ gterm\ {\isacharequal}\ Apply\ {\isacharprime}f\ {\isachardoublequoteopen}{\isacharprime}f\ gterm\ list{\isachardoublequoteclose}% +\begin{isamarkuptext}% +To try it out, we declare a datatype of some integer operations: +integer constants, the unary minus operator and the addition +operator.% +\end{isamarkuptext}% +\isamarkuptrue% \isacommand{datatype}\isamarkupfalse% -\ integer{\isacharunderscore}op\ {\isacharequal}\ Number\ int\ {\isacharbar}\ UnaryMinus\ {\isacharbar}\ Plus\isanewline -\isanewline +\ integer{\isacharunderscore}op\ {\isacharequal}\ Number\ int\ {\isacharbar}\ UnaryMinus\ {\isacharbar}\ Plus% +\begin{isamarkuptext}% +Now the type \isa{integer{\isacharunderscore}op\ gterm} denotes the ground +terms built over those symbols. + +The type constructor \isa{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{{\isacharbraceleft}Number\ {\isadigit{2}}{\isacharcomma}\ UnaryMinus{\isacharcomma}\ Plus{\isacharbraceright}}. + +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.% +\end{isamarkuptext}% +\isamarkuptrue% \isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% \isanewline \ \ gterms\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ set\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequoteclose}\isanewline \ \ \isakeyword{for}\ F\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ set{\isachardoublequoteclose}\isanewline \isakeyword{where}\isanewline step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ \ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ gterms\ F{\isachardoublequoteclose}\isanewline -\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ gterms\ F{\isachardoublequoteclose}% +\begin{isamarkuptext}% +To demonstrate a proof from this definition, let us +show that the function \isa{gterms} +is \textbf{monotone}. We shall need this concept shortly.% +\end{isamarkuptext}% +\isamarkuptrue% \isacommand{lemma}\isamarkupfalse% \ gterms{\isacharunderscore}mono{\isacharcolon}\ {\isachardoublequoteopen}F{\isasymsubseteq}G\ {\isasymLongrightarrow}\ gterms\ F\ {\isasymsubseteq}\ gterms\ G{\isachardoublequoteclose}\isanewline % @@ -44,16 +98,7 @@ \isacommand{apply}\isamarkupfalse% \ clarify\isanewline \isacommand{apply}\isamarkupfalse% -\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}% -\begin{isamarkuptxt}% -\begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}F\ {\isasymsubseteq}\ G{\isacharsemicolon}\ {\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ gterms\ G{\isacharbraceright}{\isacharsemicolon}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }f\ {\isasymin}\ F{\isasymrbrakk}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G% -\end{isabelle}% -\end{isamarkuptxt}% -\isamarkuptrue% +\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}\isanewline \isacommand{apply}\isamarkupfalse% \ blast\isanewline \isacommand{done}\isamarkupfalse% @@ -65,34 +110,162 @@ % \endisadelimproof % -\begin{isamarkuptext}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\begin{isamarkuptxt}% +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{gterms\ F}. (We could have used \isa{intro\ subsetI}.) We then +apply rule induction. Here is the resulting subgoal: \begin{isabelle}% -\ \ \ \ \ {\isasymlbrakk}a\ {\isasymin}\ even{\isacharsemicolon}\ a\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}a\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}F\ {\isasymsubseteq}\ G{\isacharsemicolon}\ {\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasymand}\ t\ {\isasymin}\ gterms\ G{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G% \end{isabelle} -\rulename{even.cases} +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.% +\end{isamarkuptxt}% +\isamarkuptrue% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +\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{\isachardot}induct} separate from +\isa{gterm{\isachardot}induct}. +\end{warn} -Just as a demo I include -the two forms that Markus has made available. First the one for binding the -result to a name% +Call a term \textbf{well-formed} if each symbol occurring in it is applied +to the correct number of arguments. (This number is called the symbol's +\textbf{arity}.) We can express well-formedness by +generalizing the inductive definition of +\isa{gterms}. +Suppose we are given a function called \isa{arity}, specifying the arities +of all symbols. 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.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% +\isanewline +\ \ well{\isacharunderscore}formed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{for}\ arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharsemicolon}\ \ \isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequoteclose}% +\begin{isamarkuptext}% +The inductive definition neatly captures the reasoning above. +The universal quantification over the +\isa{set} of arguments expresses that all of them are well-formed.% +\index{quantifiers!and inductive definitions|)}% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{inductive{\isacharunderscore}cases}\isamarkupfalse% -\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline +% +\isamarkupsubsection{Alternative Definition Using a Monotone Function% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\index{monotone functions!and inductive definitions|(}% +An inductive definition may refer to the +inductively defined set through an arbitrary monotone 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.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% \isanewline -\isacommand{thm}\isamarkupfalse% -\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases% +\ \ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{for}\ arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}args\ {\isasymin}\ lists\ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharparenright}{\isacharsemicolon}\ \ \isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequoteclose}\isanewline +\isakeyword{monos}\ lists{\isacharunderscore}mono% \begin{isamarkuptext}% +We cite the theorem \isa{lists{\isacharunderscore}mono} to justify +using the function \isa{lists}.% +\footnote{This particular theorem is installed by default already, but we +include the \isakeyword{monos} declaration in order to illustrate its syntax.} \begin{isabelle}% -\ \ \ \ \ {\isasymlbrakk}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P% +A\ {\isasymsubseteq}\ B\ {\isasymLongrightarrow}\ lists\ A\ {\isasymsubseteq}\ lists\ B\rulename{lists{\isacharunderscore}mono}% +\end{isabelle} +Why must the function be monotone? 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}% +{\isadigit{0}}\ {\isasymin}\ even\isasep\isanewline% +n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even% \end{isabelle} -\rulename{Suc_Suc_cases} +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{trivlist} +\item \isa{{\isadigit{0}}\ {\isasymin}\ even} +\item \isa{n\ {\isasymnotin}\ even\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ even} +\end{trivlist} +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. -and now the one for local usage:% +Even with its use of the function \isa{lists}, the premise of our +introduction rule is positive: +\begin{isabelle}% +args\ {\isasymin}\ lists\ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharparenright}% +\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 monotone, +applications of the rule remain valid as new terms are constructed. +Further lists of well-formed +terms become available and none are taken away.% +\index{monotone functions!and inductive definitions|)}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{A Proof of Equivalence% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +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.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\isamarkupfalse% -\ {\isachardoublequoteopen}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P\ n{\isachardoublequoteclose}\isanewline +\ {\isachardoublequoteopen}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequoteclose}\isanewline % \isadelimproof % @@ -100,26 +273,176 @@ % \isatagproof \isacommand{apply}\isamarkupfalse% -\ {\isacharparenleft}ind{\isacharunderscore}cases\ {\isachardoublequoteopen}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequoteclose}{\isacharparenright}\isanewline -\isacommand{oops}\isamarkupfalse% +\ clarify\isanewline +\isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}\isanewline +\isacommand{apply}\isamarkupfalse% +\ auto\isanewline +\isacommand{done}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\begin{isamarkuptxt}% +The \isa{clarify} method gives +us an element of \isa{well{\isacharunderscore}formed{\isacharunderscore}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 +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\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:% +\end{isamarkuptxt}% +\isamarkuptrue% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isacommand{lemma}\isamarkupfalse% +\ {\isachardoublequoteopen}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{apply}\isamarkupfalse% +\ clarify\isanewline +\isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}\isanewline +\isacommand{apply}\isamarkupfalse% +\ auto\isanewline +\isacommand{done}\isamarkupfalse% % \endisatagproof {\isafoldproof}% % \isadelimproof -\isanewline +% +\endisadelimproof +% +\isadelimproof % \endisadelimproof -\isanewline +% +\isatagproof +% +\begin{isamarkuptxt}% +The proof script is identical, but the subgoal after applying induction may +be surprising: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}args\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}}{\isasymin}\ lists\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ }{\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasyminter}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ {\isacharparenleft}}{\isacharbraceleft}a{\isachardot}\ a\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharbraceright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity% +\end{isabelle} +The induction hypothesis contains an application of \isa{lists}. Using a +monotone function in the inductive definition always has this effect. The +subgoal may look uninviting, but fortunately +\isa{lists} distributes over intersection: +\begin{isabelle}% +lists\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isacharequal}\ lists\ A\ {\isasyminter}\ lists\ B\rulename{lists{\isacharunderscore}Int{\isacharunderscore}eq}% +\end{isabelle} +Thanks to this default simplification rule, the induction hypothesis +is quickly replaced by its two parts: +\begin{trivlist} +\item \isa{args\ {\isasymin}\ lists\ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharparenright}} +\item \isa{args\ {\isasymin}\ lists\ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharparenright}} +\end{trivlist} +Invoking the rule \isa{well{\isacharunderscore}formed{\isacharunderscore}gterm{\isachardot}step} completes the proof. The +call to \isa{auto} does all this work. + +This example is typical of how monotone functions +\index{monotone functions} can be used. In particular, many of them +distribute over intersection. Monotonicity implies one direction of +this set equality; we have this theorem: +\begin{isabelle}% +mono\ f\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isasymsubseteq}\ f\ A\ {\isasyminter}\ f\ B\rulename{mono{\isacharunderscore}Int}% +\end{isabelle}% +\end{isamarkuptxt}% +\isamarkuptrue% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupsubsection{Another Example of Rule Inversion% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\index{rule inversion|(}% +Does \isa{gterms} distribute over intersection? We have proved that this +function is monotone, so \isa{mono{\isacharunderscore}Int} gives one of the inclusions. The +opposite inclusion asserts 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}.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ gterms{\isacharunderscore}IntI{\isacharcolon}\isanewline +\ \ \ \ \ {\isachardoublequoteopen}t\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}{\isachardoublequoteclose}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +Attempting this proof, we get the assumption +\isa{Apply\ f\ args\ {\isasymin}\ gterms\ G}, which cannot be broken down. +It looks like a job for rule inversion:\cmmdx{inductive\protect\_cases}% +\end{isamarkuptext}% +\isamarkuptrue% \isacommand{inductive{\isacharunderscore}cases}\isamarkupfalse% \ gterm{\isacharunderscore}Apply{\isacharunderscore}elim\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isachardoublequoteclose}% \begin{isamarkuptext}% -this is what we get: - +Here is the result. \begin{isabelle}% -\ \ \ \ \ {\isasymlbrakk}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P% +{\isasymlbrakk}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isacharsemicolon}\isanewline +\isaindent{\ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\isanewline +{\isasymLongrightarrow}\ P\rulename{gterm{\isacharunderscore}Apply{\isacharunderscore}elim}% \end{isabelle} -\rulename{gterm_Apply_elim}% +This rule replaces an assumption about \isa{Apply\ f\ args} by +assumptions about \isa{f} and~\isa{args}. +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{\isacharbang}} attribute. + +Now we can prove the other half of that distributive law.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\isamarkupfalse% @@ -132,19 +455,7 @@ % \isatagproof \isacommand{apply}\isamarkupfalse% -\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}% -\begin{isamarkuptxt}% -\begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}args\ f{\isachardot}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ gterms\ F\ {\isasyminter}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ t\ {\isasymin}\ }{\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ x\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}{\isacharbraceright}{\isacharsemicolon}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }f\ {\isasymin}\ F{\isasymrbrakk}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }Apply\ f\ args\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}% -\end{isabelle}% -\end{isamarkuptxt}% -\isamarkuptrue% +\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}\isanewline \isacommand{apply}\isamarkupfalse% \ blast\isanewline \isacommand{done}\isamarkupfalse% @@ -156,16 +467,45 @@ % \endisadelimproof % -\begin{isamarkuptext}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\begin{isamarkuptxt}% +The proof begins with rule induction over the definition of +\isa{gterms}, which leaves a single subgoal: \begin{isabelle}% -\ \ \ \ \ mono\ f\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isasymsubseteq}\ f\ A\ {\isasyminter}\ f\ B% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}args\ f{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ gterms\ F\ {\isasymand}\ {\isacharparenleft}t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }f\ {\isasymin}\ F{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }Apply\ f\ args\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}% \end{isabelle} -\rulename{mono_Int}% -\end{isamarkuptext}% +To prove this, we assume \isa{Apply\ f\ args\ {\isasymin}\ gterms\ G}. Rule inversion, +in the form of \isa{gterm{\isacharunderscore}Apply{\isacharunderscore}elim}, infers +that every element of \isa{args} belongs to +\isa{gterms\ G}; hence (by the induction hypothesis) it belongs +to \isa{gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}}. Rule inversion also yields +\isa{f\ {\isasymin}\ G} and hence \isa{f\ {\isasymin}\ F\ {\isasyminter}\ G}. +All of this reasoning is done by \isa{blast}. + +\smallskip +Our distributive law is a trivial consequence of previously-proved results:% +\end{isamarkuptxt}% \isamarkuptrue% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof \isacommand{lemma}\isamarkupfalse% \ gterms{\isacharunderscore}Int{\isacharunderscore}eq\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline -\ \ \ \ \ {\isachardoublequoteopen}gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}\ {\isacharequal}\ gterms\ F\ {\isasyminter}\ gterms\ G{\isachardoublequoteclose}\isanewline +\ \ \ \ \ {\isachardoublequoteopen}gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}\ {\isacharequal}\ gterms\ F\ {\isasyminter}\ gterms\ G{\isachardoublequoteclose}\isanewline % \isadelimproof % @@ -181,120 +521,31 @@ % \endisadelimproof % -\begin{isamarkuptext}% -the following declaration isn't actually used% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{consts}\isamarkupfalse% -\ integer{\isacharunderscore}arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}integer{\isacharunderscore}op\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline -\isacommand{primrec}\isamarkupfalse% -\isanewline -{\isachardoublequoteopen}integer{\isacharunderscore}arity\ {\isacharparenleft}Number\ n{\isacharparenright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline -{\isachardoublequoteopen}integer{\isacharunderscore}arity\ UnaryMinus\ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline -{\isachardoublequoteopen}integer{\isacharunderscore}arity\ Plus\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline -\isanewline +\index{rule inversion|)}% +\index{ground terms example|)} + + +\begin{isamarkuptext} +\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{inductive{\isacharunderscore}set}\isamarkupfalse% \isanewline -\ \ well{\isacharunderscore}formed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequoteclose}\isanewline -\ \ \isakeyword{for}\ arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline -\isakeyword{where}\isanewline -step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharsemicolon}\ \ \isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequoteclose}\isanewline -\isanewline -\isanewline -\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% -\isanewline -\ \ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequoteclose}\isanewline -\ \ \isakeyword{for}\ arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline -\isakeyword{where}\isanewline -step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}args\ {\isasymin}\ lists\ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharparenright}{\isacharsemicolon}\ \ \isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequoteclose}\isanewline -\isakeyword{monos}\ lists{\isacharunderscore}mono\isanewline -\isanewline -\isacommand{lemma}\isamarkupfalse% -\ {\isachardoublequoteopen}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequoteclose}\isanewline +\ \ well{\isacharunderscore}typed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}f\ gterm\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{for}\ sig\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isachardoublequoteclose}% +\end{isabelle} +\end{exercise} +\end{isamarkuptext} % \isadelimproof % \endisadelimproof % \isatagproof -\isacommand{apply}\isamarkupfalse% -\ clarify% -\begin{isamarkuptxt}% -The situation after clarify -\begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymLongrightarrow}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity% -\end{isabelle}% -\end{isamarkuptxt}% -\isamarkuptrue% -\isacommand{apply}\isamarkupfalse% -\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}% -\begin{isamarkuptxt}% -note the induction hypothesis! -\begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasyminter}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ t\ {\isasymin}\ }{\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharbraceright}{\isacharsemicolon}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity% -\end{isabelle}% -\end{isamarkuptxt}% -\isamarkuptrue% -\isacommand{apply}\isamarkupfalse% -\ auto\isanewline -\isacommand{done}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -\isanewline -% -\endisadelimproof -\isanewline -\isanewline -\isanewline -\isacommand{lemma}\isamarkupfalse% -\ {\isachardoublequoteopen}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequoteclose}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{apply}\isamarkupfalse% -\ clarify% -\begin{isamarkuptxt}% -The situation after clarify -\begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymLongrightarrow}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity% -\end{isabelle}% -\end{isamarkuptxt}% -\isamarkuptrue% -\isacommand{apply}\isamarkupfalse% -\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}% -\begin{isamarkuptxt}% -note the induction hypothesis! -\begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}args\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}}{\isasymin}\ lists\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ }{\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasyminter}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ {\isacharparenleft}}{\isacharbraceleft}a{\isachardot}\ a\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharbraceright}{\isacharparenright}{\isacharsemicolon}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity% -\end{isabelle}% -\end{isamarkuptxt}% -\isamarkuptrue% -\isacommand{apply}\isamarkupfalse% -\ auto\isanewline -\isacommand{done}\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -303,115 +554,31 @@ % \endisadelimproof % -\begin{isamarkuptext}% -\begin{isabelle}% -\ \ \ \ \ lists\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isacharequal}\ lists\ A\ {\isasyminter}\ lists\ B% -\end{isabelle}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\begin{isamarkuptext}% -the rest isn't used: too complicated. OK for an exercise though.% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% -\isanewline -\ \ integer{\isacharunderscore}signature\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}integer{\isacharunderscore}op\ {\isacharasterisk}\ {\isacharparenleft}unit\ list\ {\isacharasterisk}\ unit{\isacharparenright}{\isacharparenright}\ set{\isachardoublequoteclose}\isanewline -\isakeyword{where}\isanewline -\ \ Number{\isacharcolon}\ \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}Number\ n{\isacharcomma}\ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequoteclose}\isanewline -{\isacharbar}\ UnaryMinus{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}UnaryMinus{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequoteclose}\isanewline -{\isacharbar}\ Plus{\isacharcolon}\ \ \ \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}Plus{\isacharcomma}\ \ \ \ \ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharparenright}{\isacharcomma}{\isacharparenleft}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequoteclose}\isanewline -\isanewline -\isanewline -\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% -\isanewline -\ \ well{\isacharunderscore}typed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}f\ gterm\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}set{\isachardoublequoteclose}\isanewline -\ \ \isakeyword{for}\ sig\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isachardoublequoteclose}\isanewline -\isakeyword{where}\isanewline -step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline -\ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}{\isasymforall}pair\ {\isasymin}\ set\ args{\isachardot}\ pair\ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isacharsemicolon}\ \isanewline -\ \ \ \ \ \ sig\ f\ {\isacharequal}\ {\isacharparenleft}map\ snd\ args{\isacharcomma}\ rtype{\isacharparenright}{\isasymrbrakk}\isanewline -\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ {\isacharparenleft}map\ fst\ args{\isacharparenright}{\isacharcomma}\ rtype{\isacharparenright}\ \isanewline -\ \ \ \ \ \ \ \ \ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% -\isanewline -\ \ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}f\ gterm\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}set{\isachardoublequoteclose}\isanewline -\ \ \isakeyword{for}\ sig\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isachardoublequoteclose}\isanewline -\isakeyword{where}\isanewline -step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline -\ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}args\ {\isasymin}\ lists{\isacharparenleft}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isacharparenright}{\isacharsemicolon}\ \isanewline -\ \ \ \ \ \ sig\ f\ {\isacharequal}\ {\isacharparenleft}map\ snd\ args{\isacharcomma}\ rtype{\isacharparenright}{\isasymrbrakk}\isanewline -\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ {\isacharparenleft}map\ fst\ args{\isacharparenright}{\isacharcomma}\ rtype{\isacharparenright}\ \isanewline -\ \ \ \ \ \ \ \ \ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequoteclose}\isanewline -\isakeyword{monos}\ lists{\isacharunderscore}mono\isanewline -\isanewline -\isanewline -\isacommand{lemma}\isamarkupfalse% -\ {\isachardoublequoteopen}well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequoteclose}\isanewline -% \isadelimproof % \endisadelimproof % \isatagproof -\isacommand{apply}\isamarkupfalse% -\ clarify\isanewline -\isacommand{apply}\isamarkupfalse% -\ {\isacharparenleft}erule\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}\isanewline -\isacommand{apply}\isamarkupfalse% -\ auto\isanewline -\isacommand{done}\isamarkupfalse% % \endisatagproof {\isafoldproof}% % \isadelimproof -\isanewline -% -\endisadelimproof -\isanewline -\isacommand{lemma}\isamarkupfalse% -\ {\isachardoublequoteopen}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequoteclose}\isanewline -% -\isadelimproof % \endisadelimproof % -\isatagproof -\isacommand{apply}\isamarkupfalse% -\ clarify\isanewline -\isacommand{apply}\isamarkupfalse% -\ {\isacharparenleft}erule\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}\isanewline -\isacommand{apply}\isamarkupfalse% -\ auto\isanewline -\isacommand{done}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -\isanewline -% -\endisadelimproof -\isanewline -% \isadelimtheory -\isanewline % \endisadelimtheory % \isatagtheory -\isacommand{end}\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% % \isadelimtheory -\isanewline % \endisadelimtheory -\isanewline \end{isabellebody}% %%% Local Variables: %%% mode: latex diff -r 32d76edc5e5c -r ca73e86c22bb doc-src/TutorialI/Inductive/document/Even.tex --- a/doc-src/TutorialI/Inductive/document/Even.tex Thu Jul 19 15:35:00 2007 +0200 +++ b/doc-src/TutorialI/Inductive/document/Even.tex Thu Jul 19 15:35:36 2007 +0200 @@ -3,44 +3,81 @@ \def\isabellecontext{Even}% % \isadelimtheory -\isanewline % \endisadelimtheory % \isatagtheory -\isacommand{theory}\isamarkupfalse% -\ Even\ \isakeyword{imports}\ Main\ \isakeyword{begin}% +% \endisatagtheory {\isafoldtheory}% % \isadelimtheory -\isanewline % \endisadelimtheory -\isanewline -\isanewline +% +\isamarkupsection{The Set of Even Numbers% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\index{even numbers!defining inductively|(}% +The set of even numbers can be inductively defined as the least set +containing 0 and closed under the operation $+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.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Making an Inductive Definition% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Using \commdx{inductive\_set}, we declare the constant \isa{even} to be +a set of natural numbers with the desired properties.% +\end{isamarkuptext}% +\isamarkuptrue% \isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% \ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline \isakeyword{where}\isanewline \ \ zero{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline {\isacharbar}\ step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymin}\ even{\isachardoublequoteclose}% \begin{isamarkuptext}% -An inductive definition consists of introduction rules. - -\begin{isabelle}% -\ \ \ \ \ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even% -\end{isabelle} -\rulename{even.step} - +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, +thus following the definitional approach (see {\S}\ref{sec:definitional}). +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}% -\ \ \ \ \ {\isasymlbrakk}x\ {\isasymin}\ even{\isacharsemicolon}\ P\ {\isadigit{0}}{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ P\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x% +{\isadigit{0}}\ {\isasymin}\ even\rulename{even{\isachardot}zero}\par\smallskip% +n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\rulename{even{\isachardot}step}% \end{isabelle} -\rulename{even.induct} -Attributes can be given to the introduction rules. Here both rules are -specified as \isa{intro!} - -Our first lemma states that numbers of the form $2\times k$ are even.% +The introduction rules can be given attributes. Here +both rules are specified as \isa{intro!},% +\index{intro"!@\isa {intro"!} (attribute)} +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.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Using Introduction Rules% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +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.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\isamarkupfalse% @@ -52,18 +89,7 @@ % \isatagproof \isacommand{apply}\isamarkupfalse% -\ {\isacharparenleft}induct{\isacharunderscore}tac\ k{\isacharparenright}% -\begin{isamarkuptxt}% -The first step is induction on the natural number \isa{k}, which leaves -two subgoals: -\begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{0}}\ {\isasymin}\ even\isanewline -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isadigit{2}}\ {\isacharasterisk}\ Suc\ n\ {\isasymin}\ even% -\end{isabelle} -Here \isa{auto} simplifies both subgoals so that they match the introduction -rules, which then are applied automatically.% -\end{isamarkuptxt}% -\isamarkuptrue% +\ {\isacharparenleft}induct{\isacharunderscore}tac\ k{\isacharparenright}\isanewline \ \isacommand{apply}\isamarkupfalse% \ auto\isanewline \isacommand{done}\isamarkupfalse% @@ -75,13 +101,36 @@ % \endisadelimproof % -\begin{isamarkuptext}% -Our goal is to prove the equivalence between the traditional definition -of even (using the divides relation) and our inductive definition. Half of -this equivalence is trivial using the lemma just proved, whose \isa{intro!} -attribute ensures it will be applied automatically.% -\end{isamarkuptext}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\begin{isamarkuptxt}% +\noindent +The first step is induction on the natural number \isa{k}, which leaves +two subgoals: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{0}}\ {\isasymin}\ even\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isadigit{2}}\ {\isacharasterisk}\ 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{\isacharbang}} attribute ensures it is applied automatically.% +\end{isamarkuptxt}% \isamarkuptrue% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof \isacommand{lemma}\isamarkupfalse% \ dvd{\isacharunderscore}imp{\isacharunderscore}even{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{2}}\ dvd\ n\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline % @@ -99,25 +148,59 @@ % \endisadelimproof % +\isamarkupsubsection{Rule Induction \label{sec:rule-induction}% +} +\isamarkuptrue% +% \begin{isamarkuptext}% -our first rule induction!% +\index{rule induction|(}% +From the definition of the set +\isa{even}, Isabelle has +generated an induction rule: +\begin{isabelle}% +{\isasymlbrakk}x\ {\isasymin}\ even{\isacharsemicolon}\ P\ {\isadigit{0}}{\isacharsemicolon}\isanewline +\isaindent{\ }{\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ P\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isasymrbrakk}\isanewline +{\isasymLongrightarrow}\ P\ x\rulename{even{\isachardot}induct}% +\end{isabelle} +A property \isa{P} holds for every even number provided it +holds for~\isa{{\isadigit{0}}} and is closed under the operation +\isa{Suc(Suc \(\cdot\))}. 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{{\isadigit{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.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\isamarkupfalse% -\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ n{\isachardoublequoteclose}\isanewline -% +\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ n{\isachardoublequoteclose}% \isadelimproof % \endisadelimproof % \isatagproof +% +\begin{isamarkuptxt}% +We begin by applying induction. Note that \isa{even{\isachardot}induct} has the form +of an elimination rule, so we use the method \isa{erule}. We get two +subgoals:% +\end{isamarkuptxt}% +\isamarkuptrue% \isacommand{apply}\isamarkupfalse% \ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}% \begin{isamarkuptxt}% \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}% -\end{isabelle}% +\end{isabelle} +We unfold the definition of \isa{dvd} in both subgoals, proving the first +one and simplifying the second:% \end{isamarkuptxt}% \isamarkuptrue% \isacommand{apply}\isamarkupfalse% @@ -125,7 +208,9 @@ \begin{isamarkuptxt}% \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isasymexists}k{\isachardot}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}k{\isachardot}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k% -\end{isabelle}% +\end{isabelle} +The next command eliminates the existential quantifier from the assumption +and replaces \isa{n} by \isa{{\isadigit{2}}\ {\isacharasterisk}\ k}.% \end{isamarkuptxt}% \isamarkuptrue% \isacommand{apply}\isamarkupfalse% @@ -133,13 +218,13 @@ \begin{isamarkuptxt}% \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ k{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ k\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isasymexists}ka{\isachardot}\ Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ ka% -\end{isabelle}% +\end{isabelle} +To conclude, we tell Isabelle that the desired value is +\isa{Suc\ k}. With this hint, the subgoal falls to \isa{simp}.% \end{isamarkuptxt}% \isamarkuptrue% \isacommand{apply}\isamarkupfalse% -\ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}Suc\ k{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharcomma}\ simp{\isacharparenright}\isanewline -\isacommand{done}\isamarkupfalse% -% +\ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}Suc\ k{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharcomma}\ simp{\isacharparenright}% \endisatagproof {\isafoldproof}% % @@ -148,7 +233,10 @@ \endisadelimproof % \begin{isamarkuptext}% -no iff-attribute because we don't always want to use it% +Combining the previous two results yields our objective, the +equivalence relating \isa{even} and \isa{dvd}. +% +%we don't want [iff]: discuss?% \end{isamarkuptext}% \isamarkuptrue% \isacommand{theorem}\isamarkupfalse% @@ -168,12 +256,21 @@ % \endisadelimproof % +\isamarkupsubsection{Generalization and Rule Induction \label{sec:gen-rule-induction}% +} +\isamarkuptrue% +% \begin{isamarkuptext}% -this result ISN'T inductive...% +\index{generalizing for 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, our first attempt uses the obvious statement of +the result. It fails:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\isamarkupfalse% -\ Suc{\isacharunderscore}Suc{\isacharunderscore}even{\isacharunderscore}imp{\isacharunderscore}even{\isacharcolon}\ {\isachardoublequoteopen}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline +\ {\isachardoublequoteopen}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline % \isadelimproof % @@ -181,14 +278,7 @@ % \isatagproof \isacommand{apply}\isamarkupfalse% -\ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}% -\begin{isamarkuptxt}% -\begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ n\ {\isasymin}\ even\isanewline -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}na{\isachardot}\ {\isasymlbrakk}na\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even% -\end{isabelle}% -\end{isamarkuptxt}% -\isamarkuptrue% +\ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}\isanewline \isacommand{oops}\isamarkupfalse% % \endisatagproof @@ -198,10 +288,35 @@ % \endisadelimproof % -\begin{isamarkuptext}% -...so we need an inductive lemma...% -\end{isamarkuptext}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\begin{isamarkuptxt}% +Rule induction finds no occurrences of \isa{Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}} in the +conclusion, which it therefore leaves unchanged. (Look at +\isa{even{\isachardot}induct} to see why this happens.) We have these subgoals: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ n\ {\isasymin}\ even\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}na{\isachardot}\ {\isasymlbrakk}na\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even% +\end{isabelle} +The first one is hopeless. Rule induction on +a non-variable term discards information, and usually fails. +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:% +\end{isamarkuptxt}% \isamarkuptrue% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof \isacommand{lemma}\isamarkupfalse% \ even{\isacharunderscore}imp{\isacharunderscore}even{\isacharunderscore}minus{\isacharunderscore}{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline % @@ -211,15 +326,8 @@ % \isatagproof \isacommand{apply}\isamarkupfalse% -\ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}% -\begin{isamarkuptxt}% -\begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isadigit{0}}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even\isanewline -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even% -\end{isabelle}% -\end{isamarkuptxt}% -\isamarkuptrue% -\isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}\isanewline +\ \isacommand{apply}\isamarkupfalse% \ auto\isanewline \isacommand{done}\isamarkupfalse% % @@ -230,10 +338,34 @@ % \endisadelimproof % -\begin{isamarkuptext}% -...and prove it in a separate step% -\end{isamarkuptext}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\begin{isamarkuptxt}% +This lemma is trivially inductive. Here are the subgoals: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isadigit{0}}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even% +\end{isabelle} +The first is trivial because \isa{{\isadigit{0}}\ {\isacharminus}\ {\isadigit{2}}} simplifies to \isa{{\isadigit{0}}}, which is +even. The second is trivial too: \isa{Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharminus}\ {\isadigit{2}}} simplifies to +\isa{n}, matching the assumption.% +\index{rule induction|)} %the sequel isn't really about induction + +\medskip +Using our lemma, we can easily prove the result we originally wanted:% +\end{isamarkuptxt}% \isamarkuptrue% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof \isacommand{lemma}\isamarkupfalse% \ Suc{\isacharunderscore}Suc{\isacharunderscore}even{\isacharunderscore}imp{\isacharunderscore}even{\isacharcolon}\ {\isachardoublequoteopen}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline % @@ -248,11 +380,15 @@ {\isafoldproof}% % \isadelimproof -\isanewline % \endisadelimproof -\isanewline -\isanewline +% +\begin{isamarkuptext}% +We have just proved the converse of the introduction rule \isa{even{\isachardot}step}. +This suggests proving the following equivalence. We give it the +\attrdx{iff} attribute because of its obvious value for simplification.% +\end{isamarkuptext}% +\isamarkuptrue% \isacommand{lemma}\isamarkupfalse% \ {\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymin}\ even{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymin}\ even{\isacharparenright}{\isachardoublequoteclose}\isanewline % @@ -267,26 +403,127 @@ {\isafoldproof}% % \isadelimproof -\isanewline % \endisadelimproof % +\isamarkupsubsection{Rule Inversion \label{sec:rule-inversion}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\index{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/HOL\@. + +Recall that \isa{even} is the minimal set closed under these two rules: +\begin{isabelle}% +{\isadigit{0}}\ {\isasymin}\ even\isasep\isanewline% +n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\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{{\isadigit{0}}} +or else \isa{a} has the form \isa{Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}}, for some suitable \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{\isacharsemicolon}\ a\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\isanewline +\isaindent{\ }{\isasymAnd}n{\isachardot}\ {\isasymlbrakk}a\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\isanewline +{\isasymLongrightarrow}\ P\rulename{even{\isachardot}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\ {\isacharparenleft}Suc\ n{\isacharparenright}} 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:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{inductive{\isacharunderscore}cases}\isamarkupfalse% +\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequoteclose}% +\begin{isamarkuptext}% +The \commdx{inductive\protect\_cases} command generates an instance of +the \isa{cases} rule for the supplied pattern and gives it the supplied name: +\begin{isabelle}% +{\isasymlbrakk}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\rulename{Suc{\isacharunderscore}Suc{\isacharunderscore}cases}% +\end{isabelle} +Applying this as an elimination rule yields one case where \isa{even{\isachardot}cases} +would yield two. Rule inversion works well when the conclusions of the +introduction rules involve datatype constructors like \isa{Suc} and \isa{{\isacharhash}} +(list ``cons''); freeness reasoning discards all but one or two cases. + +In the \isacommand{inductive\_cases} command we supplied an +attribute, \isa{elim{\isacharbang}}, +\index{elim"!@\isa {elim"!} (attribute)}% +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{\isacharunderscore}Suc{\isacharunderscore}cases} is equivalent to the following implication: +\begin{isabelle}% +Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even% +\end{isabelle} +Just above we devoted some effort to reaching precisely +this result. Yet we could have obtained it by a one-line declaration, +dispensing with the lemma \isa{even{\isacharunderscore}imp{\isacharunderscore}even{\isacharunderscore}minus{\isacharunderscore}{\isadigit{2}}}. +This example also justifies the terminology +\textbf{rule inversion}: the new rule inverts the introduction rule +\isa{even{\isachardot}step}. In general, a rule can be inverted when the set of elements +it introduces is disjoint from those of the other introduction rules. + +For one-off applications of rule inversion, use the \methdx{ind_cases} method. +Here is an example:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}ind{\isacharunderscore}cases\ {\isachardoublequoteopen}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequoteclose}{\isacharparenright}% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +The specified instance of the \isa{cases} rule is generated, then applied +as an elimination rule. + +To summarize, every inductive definition produces a \isa{cases} rule. The +\commdx{inductive\protect\_cases} command stores an instance of the +\isa{cases} rule for a given pattern. Within a proof, the +\isa{ind{\isacharunderscore}cases} method applies an instance of the \isa{cases} +rule. + +The even numbers example has shown how inductive definitions can be +used. Later examples will show that they are actually worth using.% +\index{rule inversion|)}% +\index{even numbers!defining inductively|)}% +\end{isamarkuptext}% +\isamarkuptrue% +% \isadelimtheory -\isanewline % \endisadelimtheory % \isatagtheory -\isacommand{end}\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% % \isadelimtheory -\isanewline % \endisadelimtheory -\isanewline \end{isabellebody}% %%% Local Variables: %%% mode: latex diff -r 32d76edc5e5c -r ca73e86c22bb doc-src/TutorialI/Inductive/document/Star.tex --- a/doc-src/TutorialI/Inductive/document/Star.tex Thu Jul 19 15:35:00 2007 +0200 +++ b/doc-src/TutorialI/Inductive/document/Star.tex Thu Jul 19 15:35:36 2007 +0200 @@ -91,7 +91,8 @@ \isaindent{\ \ \ \ \ \ }{\isasymAnd}x\ y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isacharquery}P\ y\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ z{\isasymrbrakk}\isanewline \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}x{\isadigit{2}}{\isachardot}{\isadigit{0}}% \end{isabelle} -It says that \isa{{\isacharquery}P} holds for an arbitrary pair \isa{{\isacharparenleft}{\isacharquery}xb{\isacharcomma}{\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}} if \isa{{\isacharquery}P} is preserved by all rules of the inductive definition, +It says that \isa{{\isacharquery}P} holds for an arbitrary pair \isa{{\isacharparenleft}{\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{0}}{\isacharcomma}\ {\isacharquery}x{\isadigit{2}}{\isachardot}{\isadigit{0}}{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}} +if \isa{{\isacharquery}P} is preserved by all rules of the inductive definition, i.e.\ if \isa{{\isacharquery}P} holds for the conclusion provided it holds for the premises. In general, rule induction for an $n$-ary inductive relation $R$ expects a premise of the form $(x@1,\dots,x@n) \in R$.