# HG changeset patch # User berghofe # Date 1184851791 -7200 # Node ID 9d87177f1f897c9b925d51516714983a4f8700ae # Parent 598839baafeda437e067889322a49a1563bece1f LaTeX code is now generated directly from theory file. diff -r 598839baafed -r 9d87177f1f89 doc-src/TutorialI/Inductive/Advanced.thy --- a/doc-src/TutorialI/Inductive/Advanced.thy Wed Jul 18 14:46:59 2007 +0200 +++ b/doc-src/TutorialI/Inductive/Advanced.thy Thu Jul 19 15:29:51 2007 +0200 @@ -1,10 +1,61 @@ (* ID: $Id$ *) -theory Advanced imports Even begin +(*<*)theory Advanced imports Even uses "../../antiquote_setup.ML" begin(*>*) + +text {* +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. +*} +subsection{* Universal Quantifiers in Introduction Rules \label{sec:gterm-datatype} *} + +text {* +\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 @{text gterm} for the type of ground terms. It is a type constructor +whose argument is a type of function symbols. +*} datatype 'f gterm = Apply 'f "'f gterm list" -datatype integer_op = Number int | UnaryMinus | Plus; +text {* +To try it out, we declare a datatype of some integer operations: +integer constants, the unary minus operator and the addition +operator. +*} + +datatype integer_op = Number int | UnaryMinus | Plus + +text {* +Now the type @{typ "integer_op gterm"} denotes the ground +terms built over those symbols. + +The type constructor @{text gterm} can be generalized to a function +over sets. It returns +the set of ground terms that can be formed over a set @{text F} of function symbols. For +example, we could consider the set of ground terms formed from the finite +set @{text "{Number 2, UnaryMinus, Plus}"}. + +This concept is inductive. If we have a list @{text args} of ground terms +over~@{text F} and a function symbol @{text f} in @{text F}, then we +can apply @{text f} to @{text 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 @{text args} belongs +to our inductively defined set: is a ground term +over~@{text F}. The function @{term set} denotes the set of elements in a given +list. +*} inductive_set gterms :: "'f set \ 'f gterm set" @@ -13,77 +64,56 @@ step[intro!]: "\\t \ set args. t \ gterms F; f \ F\ \ (Apply f args) \ gterms F" +text {* +To demonstrate a proof from this definition, let us +show that the function @{term gterms} +is \textbf{monotone}. We shall need this concept shortly. +*} + +lemma gterms_mono: "F\G \ gterms F \ gterms G" +apply clarify +apply (erule gterms.induct) +apply blast +done +(*<*) lemma gterms_mono: "F\G \ gterms F \ gterms G" apply clarify apply (erule gterms.induct) +(*>*) txt{* -@{subgoals[display,indent=0,margin=65]} -*}; -apply blast -done - - -text{* -@{thm[display] even.cases[no_vars]} -\rulename{even.cases} - -Just as a demo I include -the two forms that Markus has made available. First the one for binding the -result to a name - +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 @{text clarify} method to assume the existence of an element of +@{term "gterms F"}. (We could have used @{text "intro subsetI"}.) We then +apply rule induction. Here is the resulting subgoal: +@{subgoals[display,indent=0]} +The assumptions state that @{text f} belongs +to~@{text F}, which is included in~@{text G}, and that every element of the list @{text args} is +a ground term over~@{text G}. The @{text blast} method finds this chain of reasoning easily. *} - -inductive_cases Suc_Suc_cases [elim!]: - "Suc(Suc n) \ even" - -thm Suc_Suc_cases; - -text{* -@{thm[display] Suc_Suc_cases[no_vars]} -\rulename{Suc_Suc_cases} - -and now the one for local usage: -*} - -lemma "Suc(Suc n) \ even \ P n"; -apply (ind_cases "Suc(Suc n) \ even"); -oops +(*<*)oops(*>*) +text {* +\begin{warn} +Why do we call this function @{text gterms} instead +of @{text 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 @{text gterms.induct} separate from +@{text gterm.induct}. +\end{warn} -inductive_cases gterm_Apply_elim [elim!]: "Apply f args \ gterms F" - -text{*this is what we get: - -@{thm[display] gterm_Apply_elim[no_vars]} -\rulename{gterm_Apply_elim} +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 @{text arity}, specifying the arities +of all symbols. In the inductive step, we have a list @{text args} of such +terms and a function symbol~@{text f}. If the length of the list matches the +function's arity then applying @{text f} to @{text args} yields a well-formed +term. *} -lemma gterms_IntI [rule_format, intro!]: - "t \ gterms F \ t \ gterms G \ t \ gterms (F\G)" -apply (erule gterms.induct) -txt{* -@{subgoals[display,indent=0,margin=65]} -*}; -apply blast -done - - -text{* -@{thm[display] mono_Int[no_vars]} -\rulename{mono_Int} -*} - -lemma gterms_Int_eq [simp]: - "gterms (F\G) = gterms F \ gterms G" -by (blast intro!: mono_Int monoI gterms_mono) - - -text{*the following declaration isn't actually used*} -consts integer_arity :: "integer_op \ nat" -primrec -"integer_arity (Number n) = 0" -"integer_arity UnaryMinus = 1" -"integer_arity Plus = 2" - inductive_set well_formed_gterm :: "('f \ nat) \ 'f gterm set" for arity :: "'f \ nat" @@ -92,6 +122,32 @@ length args = arity f\ \ (Apply f args) \ well_formed_gterm arity" +text {* +The inductive definition neatly captures the reasoning above. +The universal quantification over the +@{text set} of arguments expresses that all of them are well-formed.% +\index{quantifiers!and inductive definitions|)} +*} + +subsection{* Alternative Definition Using a Monotone Function *} + +text {* +\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 @{term lists}. This +function, from the Isabelle theory of lists, is analogous to the +function @{term gterms} declared above: if @{text A} is a set then +@{term "lists A"} is the set of lists whose elements belong to +@{term A}. + +In the inductive definition of well-formed terms, examine the one +introduction rule. The first premise states that @{text args} belongs to +the @{text lists} of well-formed terms. This formulation is more +direct, if more obscure, than using a universal quantifier. +*} inductive_set well_formed_gterm' :: "('f \ nat) \ 'f gterm set" @@ -102,41 +158,214 @@ \ (Apply f args) \ well_formed_gterm' arity" monos lists_mono +text {* +We cite the theorem @{text lists_mono} to justify +using the function @{term lists}.% +\footnote{This particular theorem is installed by default already, but we +include the \isakeyword{monos} declaration in order to illustrate its syntax.} +@{named_thms [display,indent=0] lists_mono [no_vars] (lists_mono)} +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 +@{thm [display,indent=0] even.intros [no_vars]} +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 @{term "0 \ even"} +\item @{term "n \ even \ (Suc n) \ 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. + +Even with its use of the function \isa{lists}, the premise of our +introduction rule is positive: +@{thm_style [display,indent=0] prem1 step [no_vars]} +To apply the rule we construct a list @{term args} of previously +constructed well-formed terms. We obtain a +new term, @{term "Apply f args"}. Because @{term 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|)} +*} + +subsection{* A Proof of Equivalence *} + +text {* +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. +*} + lemma "well_formed_gterm arity \ well_formed_gterm' arity" apply clarify -txt{* -The situation after clarify -@{subgoals[display,indent=0,margin=65]} -*}; +apply (erule well_formed_gterm.induct) +apply auto +done +(*<*) +lemma "well_formed_gterm arity \ well_formed_gterm' arity" +apply clarify apply (erule well_formed_gterm.induct) -txt{* -note the induction hypothesis! -@{subgoals[display,indent=0,margin=65]} -*}; +(*>*) +txt {* +The @{text clarify} method gives +us an element of @{term "well_formed_gterm arity"} on which to perform +induction. The resulting subgoal can be proved automatically: +@{subgoals[display,indent=0]} +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: +*} +(*<*)oops(*>*) +lemma "well_formed_gterm' arity \ well_formed_gterm arity" +apply clarify +apply (erule well_formed_gterm'.induct) apply auto done +(*<*) +lemma "well_formed_gterm' arity \ well_formed_gterm arity" +apply clarify +apply (erule well_formed_gterm'.induct) +(*>*) +txt {* +The proof script is identical, but the subgoal after applying induction may +be surprising: +@{subgoals[display,indent=0,margin=65]} +The induction hypothesis contains an application of @{term lists}. Using a +monotone function in the inductive definition always has this effect. The +subgoal may look uninviting, but fortunately +@{term lists} distributes over intersection: +@{named_thms [display,indent=0] lists_Int_eq [no_vars] (lists_Int_eq)} +Thanks to this default simplification rule, the induction hypothesis +is quickly replaced by its two parts: +\begin{trivlist} +\item @{term "args \ lists (well_formed_gterm' arity)"} +\item @{term "args \ lists (well_formed_gterm arity)"} +\end{trivlist} +Invoking the rule @{text well_formed_gterm.step} completes the proof. The +call to @{text 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: +@{named_thms [display,indent=0] mono_Int [no_vars] (mono_Int)} +*} +(*<*)oops(*>*) -lemma "well_formed_gterm' arity \ well_formed_gterm arity" -apply clarify -txt{* -The situation after clarify +subsection{* Another Example of Rule Inversion *} + +text {* +\index{rule inversion|(}% +Does @{term gterms} distribute over intersection? We have proved that this +function is monotone, so @{text mono_Int} gives one of the inclusions. The +opposite inclusion asserts that if @{term t} is a ground term over both of the +sets +@{term F} and~@{term G} then it is also a ground term over their intersection, +@{term "F \ G"}. +*} + +lemma gterms_IntI: + "t \ gterms F \ t \ gterms G \ t \ gterms (F\G)" +(*<*)oops(*>*) +text {* +Attempting this proof, we get the assumption +@{term "Apply f args \ gterms G"}, which cannot be broken down. +It looks like a job for rule inversion:\cmmdx{inductive\protect\_cases} +*} + +inductive_cases gterm_Apply_elim [elim!]: "Apply f args \ gterms F" + +text {* +Here is the result. +@{named_thms [display,indent=0,margin=50] gterm_Apply_elim [no_vars] (gterm_Apply_elim)} +This rule replaces an assumption about @{term "Apply f args"} by +assumptions about @{term f} and~@{term args}. +No cases are discarded (there was only one to begin +with) but the rule applies specifically to the pattern @{term "Apply f args"}. +It can be applied repeatedly as an elimination rule without looping, so we +have given the @{text "elim!"} attribute. + +Now we can prove the other half of that distributive law. +*} + +lemma gterms_IntI [rule_format, intro!]: + "t \ gterms F \ t \ gterms G \ t \ gterms (F\G)" +apply (erule gterms.induct) +apply blast +done +(*<*) +lemma "t \ gterms F \ t \ gterms G \ t \ gterms (F\G)" +apply (erule gterms.induct) +(*>*) +txt {* +The proof begins with rule induction over the definition of +@{term gterms}, which leaves a single subgoal: @{subgoals[display,indent=0,margin=65]} -*}; -apply (erule well_formed_gterm'.induct) -txt{* -note the induction hypothesis! -@{subgoals[display,indent=0,margin=65]} -*}; -apply auto -done +To prove this, we assume @{term "Apply f args \ gterms G"}. Rule inversion, +in the form of @{text gterm_Apply_elim}, infers +that every element of @{term args} belongs to +@{term "gterms G"}; hence (by the induction hypothesis) it belongs +to @{term "gterms (F \ G)"}. Rule inversion also yields +@{term "f \ G"} and hence @{term "f \ F \ G"}. +All of this reasoning is done by @{text blast}. + +\smallskip +Our distributive law is a trivial consequence of previously-proved results: +*} +(*<*)oops(*>*) +lemma gterms_Int_eq [simp]: + "gterms (F \ G) = gterms F \ gterms G" +by (blast intro!: mono_Int monoI gterms_mono) + +text_raw {* +\index{rule inversion|)}% +\index{ground terms example|)} -text{* -@{thm[display] lists_Int_eq[no_vars]} +\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} *} +inductive_set + well_typed_gterm :: "('f \ 't list * 't) \ ('f gterm * 't)set" + for sig :: "'f \ 't list * 't" +(*<*) +where +step[intro!]: + "\\pair \ set args. pair \ well_typed_gterm sig; + sig f = (map snd args, rtype)\ + \ (Apply f (map fst args), rtype) + \ well_typed_gterm sig" +(*>*) +text_raw {* +\end{isabelle} +\end{exercise} +\end{isamarkuptext} +*} + +(*<*) + +text{*the following declaration isn't actually used*} +consts integer_arity :: "integer_op \ nat" +primrec +"integer_arity (Number n) = 0" +"integer_arity UnaryMinus = 1" +"integer_arity Plus = 2" + text{* the rest isn't used: too complicated. OK for an exercise though.*} inductive_set @@ -146,17 +375,6 @@ | UnaryMinus: "(UnaryMinus, ([()], ())) \ integer_signature" | Plus: "(Plus, ([(),()], ())) \ integer_signature" - -inductive_set - well_typed_gterm :: "('f \ 't list * 't) \ ('f gterm * 't)set" - for sig :: "'f \ 't list * 't" -where -step[intro!]: - "\\pair \ set args. pair \ well_typed_gterm sig; - sig f = (map snd args, rtype)\ - \ (Apply f (map fst args), rtype) - \ well_typed_gterm sig" - inductive_set well_typed_gterm' :: "('f \ 't list * 't) \ ('f gterm * 't)set" for sig :: "'f \ 't list * 't" @@ -183,4 +401,4 @@ end - +(*>*) diff -r 598839baafed -r 9d87177f1f89 doc-src/TutorialI/Inductive/Even.thy --- a/doc-src/TutorialI/Inductive/Even.thy Wed Jul 18 14:46:59 2007 +0200 +++ b/doc-src/TutorialI/Inductive/Even.thy Thu Jul 19 15:29:51 2007 +0200 @@ -1,89 +1,290 @@ (* ID: $Id$ *) -theory Even imports Main begin +(*<*)theory Even imports Main uses "../../antiquote_setup.ML" begin(*>*) + +section{* The Set of Even Numbers *} +text {* +\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 (@{text dvd}). +We shall prove below that the two formulations coincide. On the way we +shall examine the primary means of reasoning about inductively defined +sets: rule induction. +*} + +subsection{* Making an Inductive Definition *} + +text {* +Using \commdx{inductive\_set}, we declare the constant @{text even} to be +a set of natural numbers with the desired properties. +*} inductive_set even :: "nat set" where zero[intro!]: "0 \ even" | step[intro!]: "n \ even \ (Suc (Suc n)) \ even" -text{*An inductive definition consists of introduction rules. - -@{thm[display] even.step[no_vars]} -\rulename{even.step} +text {* +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 @{term 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: +@{named_thms[display,indent=0] even.zero[no_vars] (even.zero) even.step[no_vars] (even.step)} -@{thm[display] even.induct[no_vars]} -\rulename{even.induct} +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 +@{text step} rule is also safe because $n+2$ is even if and only if $n$ is +even. We prove this equivalence later. +*} -Attributes can be given to the introduction rules. Here both rules are -specified as \isa{intro!} +subsection{*Using Introduction Rules*} -Our first lemma states that numbers of the form $2\times k$ are even. *} +text {* +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. +*} + lemma two_times_even[intro!]: "2*k \ even" apply (induct_tac k) -txt{* -The first step is induction on the natural number \isa{k}, which leaves + apply auto +done +(*<*) +lemma "2*k \ even" +apply (induct_tac k) +(*>*) +txt {* +\noindent +The first step is induction on the natural number @{text k}, which leaves two subgoals: @{subgoals[display,indent=0,margin=65]} -Here \isa{auto} simplifies both subgoals so that they match the introduction -rules, which then are applied automatically.*}; - apply auto -done +Here @{text auto} simplifies both subgoals so that they match the introduction +rules, which are then applied automatically. -text{*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. *} - +Our ultimate goal is to prove the equivalence between the traditional +definition of @{text even} (using the divides relation) and our inductive +definition. One direction of this equivalence is immediate by the lemma +just proved, whose @{text "intro!"} attribute ensures it is applied automatically. +*} +(*<*)oops(*>*) lemma dvd_imp_even: "2 dvd n \ n \ even" by (auto simp add: dvd_def) -text{*our first rule induction!*} +subsection{* Rule Induction \label{sec:rule-induction} *} + +text {* +\index{rule induction|(}% +From the definition of the set +@{term even}, Isabelle has +generated an induction rule: +@{named_thms [display,indent=0,margin=40] even.induct [no_vars] (even.induct)} +A property @{term P} holds for every even number provided it +holds for~@{text 0} and is closed under the operation +\isa{Suc(Suc \(\cdot\))}. Then @{term P} is closed under the introduction +rules for @{term 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 @{term 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 @{text 0} and closed under~@{term 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 +@{term even} are multiples of two. +*} + lemma even_imp_dvd: "n \ even \ 2 dvd n" +txt {* +We begin by applying induction. Note that @{text even.induct} has the form +of an elimination rule, so we use the method @{text erule}. We get two +subgoals: +*} apply (erule even.induct) -txt{* -@{subgoals[display,indent=0,margin=65]} -*}; +txt {* +@{subgoals[display,indent=0]} +We unfold the definition of @{text dvd} in both subgoals, proving the first +one and simplifying the second: +*} apply (simp_all add: dvd_def) -txt{* -@{subgoals[display,indent=0,margin=65]} -*}; +txt {* +@{subgoals[display,indent=0]} +The next command eliminates the existential quantifier from the assumption +and replaces @{text n} by @{text "2 * k"}. +*} apply clarify -txt{* -@{subgoals[display,indent=0,margin=65]} -*}; +txt {* +@{subgoals[display,indent=0]} +To conclude, we tell Isabelle that the desired value is +@{term "Suc k"}. With this hint, the subgoal falls to @{text simp}. +*} apply (rule_tac x = "Suc k" in exI, simp) -done +(*<*)done(*>*) +text {* +Combining the previous two results yields our objective, the +equivalence relating @{term even} and @{text dvd}. +% +%we don't want [iff]: discuss? +*} -text{*no iff-attribute because we don't always want to use it*} theorem even_iff_dvd: "(n \ even) = (2 dvd n)" by (blast intro: dvd_imp_even even_imp_dvd) -text{*this result ISN'T inductive...*} -lemma Suc_Suc_even_imp_even: "Suc (Suc n) \ even \ n \ even" + +subsection{* Generalization and Rule Induction \label{sec:gen-rule-induction} *} + +text {* +\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: +*} + +lemma "Suc (Suc n) \ even \ n \ even" apply (erule even.induct) -txt{* -@{subgoals[display,indent=0,margin=65]} -*}; oops - -text{*...so we need an inductive lemma...*} +(*<*) +lemma "Suc (Suc n) \ even \ n \ even" +apply (erule even.induct) +(*>*) +txt {* +Rule induction finds no occurrences of @{term "Suc(Suc n)"} in the +conclusion, which it therefore leaves unchanged. (Look at +@{text even.induct} to see why this happens.) We have these subgoals: +@{subgoals[display,indent=0]} +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: +*} +(*<*)oops(*>*) lemma even_imp_even_minus_2: "n \ even \ n - 2 \ even" apply (erule even.induct) -txt{* -@{subgoals[display,indent=0,margin=65]} -*}; -apply auto + apply auto done +(*<*) +lemma "n \ even \ n - 2 \ even" +apply (erule even.induct) +(*>*) +txt {* +This lemma is trivially inductive. Here are the subgoals: +@{subgoals[display,indent=0]} +The first is trivial because @{text "0 - 2"} simplifies to @{text 0}, which is +even. The second is trivial too: @{term "Suc (Suc n) - 2"} simplifies to +@{term n}, matching the assumption.% +\index{rule induction|)} %the sequel isn't really about induction -text{*...and prove it in a separate step*} +\medskip +Using our lemma, we can easily prove the result we originally wanted: +*} +(*<*)oops(*>*) lemma Suc_Suc_even_imp_even: "Suc (Suc n) \ even \ n \ even" by (drule even_imp_even_minus_2, simp) +text {* +We have just proved the converse of the introduction rule @{text even.step}. +This suggests proving the following equivalence. We give it the +\attrdx{iff} attribute because of its obvious value for simplification. +*} lemma [iff]: "((Suc (Suc n)) \ even) = (n \ even)" by (blast dest: Suc_Suc_even_imp_even) -end + +subsection{* Rule Inversion \label{sec:rule-inversion} *} + +text {* +\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 @{term even} is the minimal set closed under these two rules: +@{thm [display,indent=0] even.intros [no_vars]} +Minimality means that @{term even} contains only the elements that these +rules force it to contain. If we are told that @{term a} +belongs to +@{term even} then there are only two possibilities. Either @{term a} is @{text 0} +or else @{term a} has the form @{term "Suc(Suc n)"}, for some suitable @{term n} +that belongs to +@{term even}. That is the gist of the @{term cases} rule, which Isabelle proves +for us when it accepts an inductive definition: +@{named_thms [display,indent=0,margin=40] even.cases [no_vars] (even.cases)} +This general rule is less useful than instances of it for +specific patterns. For example, if @{term a} has the form +@{term "Suc(Suc n)"} then the first case becomes irrelevant, while the second +case tells us that @{term n} belongs to @{term even}. Isabelle will generate +this instance for us: +*} + +inductive_cases Suc_Suc_cases [elim!]: "Suc(Suc n) \ even" + +text {* +The \commdx{inductive\protect\_cases} command generates an instance of +the @{text cases} rule for the supplied pattern and gives it the supplied name: +@{named_thms [display,indent=0] Suc_Suc_cases [no_vars] (Suc_Suc_cases)} +Applying this as an elimination rule yields one case where @{text even.cases} +would yield two. Rule inversion works well when the conclusions of the +introduction rules involve datatype constructors like @{term Suc} and @{text "#"} +(list ``cons''); freeness reasoning discards all but one or two cases. +In the \isacommand{inductive\_cases} command we supplied an +attribute, @{text "elim!"}, +\index{elim"!@\isa {elim"!} (attribute)}% +indicating that this elimination rule can be +applied aggressively. The original +@{term cases} rule would loop if used in that manner because the +pattern~@{term a} matches everything. + +The rule @{text Suc_Suc_cases} is equivalent to the following implication: +@{term [display,indent=0] "Suc (Suc n) \ even \ n \ even"} +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 @{text even_imp_even_minus_2}. +This example also justifies the terminology +\textbf{rule inversion}: the new rule inverts the introduction rule +@{text even.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: +*} + +(*<*)lemma "Suc(Suc n) \ even \ P"(*>*) +apply (ind_cases "Suc(Suc n) \ even") +(*<*)oops(*>*) + +text {* +The specified instance of the @{text cases} rule is generated, then applied +as an elimination rule. + +To summarize, every inductive definition produces a @{text cases} rule. The +\commdx{inductive\protect\_cases} command stores an instance of the +@{text cases} rule for a given pattern. Within a proof, the +@{text ind_cases} method applies an instance of the @{text 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(*>*)