diff -r 619531d87ce4 -r 4e2ee88276d2 doc-src/TutorialI/document/Even.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/document/Even.tex	Thu Jul 26 19:59:06 2012 +0200
@@ -0,0 +1,543 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Even}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\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\protect\_set}, we declare the constant \isa{even} to be
+a set of natural numbers with the desired properties.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse%
+\ even\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ set{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
+zero{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{0}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+step{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+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}%
+{\isadigit{0}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\rulename{even{\isaliteral{2E}{\isachardot}}zero}\par\smallskip%
+n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\rulename{even{\isaliteral{2E}{\isachardot}}step}%
+\end{isabelle}
+
+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%
+\ two{\isaliteral{5F}{\isacharunderscore}}times{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{2}}{\isaliteral{2A}{\isacharasterisk}}k\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ k{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \isacommand{apply}\isamarkupfalse%
+\ auto\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\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}}{\isaliteral{2E}{\isachardot}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isadigit{0}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\isanewline
+\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ Suc\ n\ {\isaliteral{5C3C696E3E}{\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{\isaliteral{21}{\isacharbang}}} attribute ensures it is applied automatically.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isacommand{lemma}\isamarkupfalse%
+\ dvd{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{2}}\ dvd\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}auto\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ dvd{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsection{Rule Induction \label{sec:rule-induction}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\index{rule induction|(}%
+From the definition of the set
+\isa{even}, Isabelle has
+generated an induction rule:
+\begin{isabelle}%
+{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{3B}{\isacharsemicolon}}\ P\ {\isadigit{0}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isaindent{\ }{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{3B}{\isacharsemicolon}}\ P\ n{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
+{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x\rulename{even{\isaliteral{2E}{\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{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}dvd{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isadigit{2}}\ dvd\ n{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+We begin by applying induction.  Note that \isa{even{\isaliteral{2E}{\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%
+\ {\isaliteral{28}{\isacharparenleft}}erule\ even{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline
+\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{3B}{\isacharsemicolon}}\ {\isadigit{2}}\ dvd\ n{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isadigit{2}}\ dvd\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}%
+\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%
+\ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ dvd{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}k{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ k{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}k{\isaliteral{2E}{\isachardot}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ k%
+\end{isabelle}
+The next command eliminates the existential quantifier from the assumption
+and replaces \isa{n} by \isa{{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ k}.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+\ clarify%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}n\ k{\isaliteral{2E}{\isachardot}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ k\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}ka{\isaliteral{2E}{\isachardot}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ 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}.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}Suc\ k{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{in}\ exI{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+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%
+\ even{\isaliteral{5F}{\isacharunderscore}}iff{\isaliteral{5F}{\isacharunderscore}}dvd{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}\ dvd\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}blast\ intro{\isaliteral{3A}{\isacharcolon}}\ dvd{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}even\ even{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}dvd{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsection{Generalization and Rule Induction \label{sec:gen-rule-induction}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\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%
+\ {\isaliteral{22}{\isachardoublequoteopen}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}erule\ even{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{oops}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+Rule induction finds no occurrences of \isa{Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}} in the
+conclusion, which it therefore leaves unchanged.  (Look at
+\isa{even{\isaliteral{2E}{\isachardot}}induct} to see why this happens.)  We have these subgoals:
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\isanewline
+\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}na{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}na\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{3B}{\isacharsemicolon}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{5C3C696E3E}{\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{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{5F}{\isacharunderscore}}minus{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}erule\ even{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \isacommand{apply}\isamarkupfalse%
+\ auto\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+This lemma is trivially inductive.  Here are the subgoals:
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isadigit{0}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\isanewline
+\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{3B}{\isacharsemicolon}}\ n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even%
+\end{isabelle}
+The first is trivial because \isa{{\isadigit{0}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}} simplifies to \isa{{\isadigit{0}}}, which is
+even.  The second is trivial too: \isa{Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\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{\isaliteral{5F}{\isacharunderscore}}Suc{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}drule\ even{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{5F}{\isacharunderscore}}minus{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+We have just proved the converse of the introduction rule \isa{even{\isaliteral{2E}{\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%
+\ {\isaliteral{5B}{\isacharbrackleft}}iff{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}blast\ dest{\isaliteral{3A}{\isacharcolon}}\ Suc{\isaliteral{5F}{\isacharunderscore}}Suc{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\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}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\isasep\isanewline%
+n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\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\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\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}%
+{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{3B}{\isacharsemicolon}}\ a\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isaindent{\ }{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}a\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
+{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\rulename{even{\isaliteral{2E}{\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\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\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{\isaliteral{5F}{\isacharunderscore}}cases}\isamarkupfalse%
+\ Suc{\isaliteral{5F}{\isacharunderscore}}Suc{\isaliteral{5F}{\isacharunderscore}}cases\ {\isaliteral{5B}{\isacharbrackleft}}elim{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\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}%
+{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{3B}{\isacharsemicolon}}\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\rulename{Suc{\isaliteral{5F}{\isacharunderscore}}Suc{\isaliteral{5F}{\isacharunderscore}}cases}%
+\end{isabelle}
+Applying this as an elimination rule yields one case where \isa{even{\isaliteral{2E}{\isachardot}}cases}
+would yield two.  Rule inversion works well when the conclusions of the
+introduction rules involve datatype constructors like \isa{Suc} and \isa{{\isaliteral{23}{\isacharhash}}}
+(list ``cons''); freeness reasoning discards all but one or two cases.
+
+In the \isacommand{inductive\_cases} command we supplied an
+attribute, \isa{elim{\isaliteral{21}{\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{\isaliteral{5F}{\isacharunderscore}}Suc{\isaliteral{5F}{\isacharunderscore}}cases} is equivalent to the following implication:
+\begin{isabelle}%
+Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{5C3C696E3E}{\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{\isaliteral{5F}{\isacharunderscore}}imp{\isaliteral{5F}{\isacharunderscore}}even{\isaliteral{5F}{\isacharunderscore}}minus{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}}. 
+This example also justifies the terminology
+\textbf{rule inversion}: the new rule inverts the introduction rule
+\isa{even{\isaliteral{2E}{\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%
+\ {\isaliteral{28}{\isacharparenleft}}ind{\isaliteral{5F}{\isacharunderscore}}cases\ {\isaliteral{22}{\isachardoublequoteopen}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\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{\isaliteral{5F}{\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
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: