doc-src/TutorialI/Inductive/Even.thy

 (* 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 \<in> even"
 | step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even"
 
-text{*An inductive definition consists of introduction rules. 
-
-@{thm[display] even.step[no_vars]}
-\rulename{even.step}
-
-@{thm[display] even.induct[no_vars]}
-\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. *}
+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)}
+
+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.
+*}
+
+subsection{*Using Introduction Rules*}
+
+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 \<in> 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 \<in> 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.*};
+Here @{text 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 @{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 \<Longrightarrow> n \<in> even"
+by (auto simp add: dvd_def)
+
+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 \<in> even \<Longrightarrow> 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]}
+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]}
+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]}
+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(*>*)
+
+text {*
+Combining the previous two results yields our objective, the
+equivalence relating @{term even} and @{text dvd}. 
+%
+%we don't want [iff]: discuss?
+*}
+
+theorem even_iff_dvd: "(n \<in> even) = (2 dvd n)"
+by (blast intro: dvd_imp_even even_imp_dvd)
+
+
+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) \<in> even \<Longrightarrow> n \<in> even"
+apply (erule even.induct)
+oops
+(*<*)
+lemma "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> 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 \<in> even \<Longrightarrow> n - 2 \<in> even"
+apply (erule even.induct)
  apply auto
 done
-
-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.  *}
-
-lemma dvd_imp_even: "2 dvd n \<Longrightarrow> n \<in> even"
-by (auto simp add: dvd_def)
-
-text{*our first rule induction!*}
-lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n"
-apply (erule even.induct)
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-*};
-apply (simp_all add: dvd_def)
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-*};
-apply clarify
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-*};
-apply (rule_tac x = "Suc k" in exI, simp)
-done
-
-
-text{*no iff-attribute because we don't always want to use it*}
-theorem even_iff_dvd: "(n \<in> 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) \<in> even \<Longrightarrow> n \<in> even"
-apply (erule even.induct)
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-*};
-oops
-
-text{*...so we need an inductive lemma...*}
-lemma even_imp_even_minus_2: "n \<in> even \<Longrightarrow> n - 2 \<in> even"
-apply (erule even.induct)
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-*};
-apply auto
-done
-
-text{*...and prove it in a separate step*}
+(*<*)
+lemma "n \<in>  even \<Longrightarrow> n - 2 \<in> 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
+
+\medskip
+Using our lemma, we can easily prove the result we originally wanted:
+*}
+(*<*)oops(*>*)
 lemma Suc_Suc_even_imp_even: "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> 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)) \<in> even) = (n \<in> 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) \<in> 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) \<in> even \<Longrightarrow> n \<in> 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) \<in> even \<Longrightarrow> P"(*>*)
+apply (ind_cases "Suc(Suc n) \<in> 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(*>*)