Auf PC laden  Even.thy

(*<*)theory Even imports "../Setup" 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 (‹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 ‹even› t
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. 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 🍋‹even› a
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
‹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 ∈ even"
apply (induct_tac k)
 apply auto
done
(*<*)
lemma "2*k ∈ even"
apply (induct_tac k)
(*>*)
txt ‹
 \noindent
 The first step is induction on the natural number ‹k›,
two subgoals:
@{subgoals[display,indent=0,margin=65]}
Here ‹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 ‹even› (using the divides relation) and our inductive
definition.  One direction of this equivalence is immediate by the lemma
just proved, whose ‹intro!› attribute ensures it is applied automatically.
›
(*<*)oops(*>*)
lemma dvd_imp_even: "2 dvd n ==> n ∈ even"
by (auto simp add: dvd_def)

subsection‹Rule Induction \label{sec:rule-induction}›

text ‹
 \index{rule induction|(}%
 From the definition of the set
 🍋‹even›,
generated an induction rule:
@{named_thms [display,indent=0,margin=40] even.induct [no_vars] (even.induct)}
A property 🍋‹P› holds for every even number provided it
holds for~‹0› and is closed under the operation
\isa{Suc(Suc \(\cdot\))}.  Then 🍋‹P› is closed under the introduction
rules for 🍋‹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 🍋‹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 ‹0› and closed under~🍋‹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
🍋‹even› are multiples of two.
›

lemma even_imp_dvd: "n ∈ even ==> 2 dvd n"
txt ‹
 We begin by applying induction. Note that ‹even.induct› h
of an elimination rule, so we use the method ‹erule›.  We get two
subgoals:
›
apply (erule even.induct)
txt ‹
 @{subgoals[display,indent=0]}
 We unfold the definition of ‹dvd› i
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 ‹n› b
›
apply clarify
txt ‹
 @{subgoals[display,indent=0]}
 To conclude, we tell Isabelle that the desired value is
 🍋‹Suc k›.
›
apply (rule_tac x = "Suc k" in exI, simp)
(*<*)done(*>*)

text ‹
 Combining the previous two results yields our objective, the
 equivalence relating 🍋‹even› a
%
%we don't want [iff]: discuss?
›

theorem even_iff_dvd: "(n ∈ 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) ∈ even ==> n ∈ even"
apply (erule even.induct)
oops
(*<*)
lemma "Suc (Suc n) ∈ even ==> n ∈ even"
apply (erule even.induct)
(*>*)
txt ‹
 Rule induction finds no occurrences of 🍋‹Suc(Suc n)› i
conclusion, which it therefore leaves unchanged.  (Look at
‹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)
 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 ‹0 - 2› s
even.  The second is trivial too: 🍋‹Suc (Suc n) - 2› simplifies to
🍋‹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) ∈ even ==> n ∈ even"
by (drule even_imp_even_minus_2, simp)

text ‹
 We have just proved the converse of the introduction rule ‹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)


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 🍋‹even› i
@{thm [display,indent=0] even.intros [no_vars]}
Minimality means that 🍋‹even› contains only the elements that these
rules force it to contain.  If we are told that 🍋‹a›
belongs to
🍋‹even› then there are only two possibilities.  Either 🍋‹a› is ‹0›
or else 🍋‹a› has the form 🍋‹Suc(Suc n)›, for some suitable 🍋‹n›
that belongs to
🍋‹even›.  That is the gist of the 🍋‹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 🍋‹a› has the form
🍋‹Suc(Suc n)› then the first case becomes irrelevant, while the second
case tells us that 🍋‹n› belongs to 🍋‹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 ‹cases› r
@{named_thms [display,indent=0] Suc_Suc_cases [no_vars] (Suc_Suc_cases)}
Applying this as an elimination rule yields one case where ‹even.cases›
would yield two.  Rule inversion works well when the conclusions of the
introduction rules involve datatype constructors like 🍋‹Suc› and ‹#›
(list ``cons''); freeness reasoning discards all but one or two cases.

In the \isacommand{inductive\_cases} command we supplied an
attribute, ‹elim!›,
\index{elim"!@\isa {elim"!} (attribute)}%
indicating that this elimination rule can be
applied aggressively.  The original
🍋‹cases› rule would loop if used in that manner because the
pattern~🍋‹a› matches everything.

The rule ‹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 ‹even_imp_even_minus_2›. 
This example also justifies the terminology
\textbf{rule inversion}: the new rule inverts the introduction rule
‹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) ∈ even")
(*<*)oops(*>*)

text ‹
 The specified instance of the ‹cases› r
as an elimination rule.

To summarize, every inductive definition produces a ‹cases› rule.  The
\commdx{inductive\protect\_cases} command stores an instance of the
‹cases› rule for a given pattern.  Within a proof, the
‹ind_cases› method applies an instance of the ‹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(*>*)