(* ID:         $Id$ *)

(*<*)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\protect\_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.  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)

 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 @{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

(*<*)

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)

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(*>*)