Theory Even
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› 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. 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
‹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›, which leaves
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
\<^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~‹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 ‹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 ‹even.induct› has the form
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› 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 ‹n› by ‹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 ‹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 ‹dvd›.
%
%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 \<^term>‹Suc(Suc n)› in the
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› simplifies to ‹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) ∈ 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 \<^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 ‹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 ‹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 ‹even.cases›
would yield two. Rule inversion works well when the conclusions of the
introduction rules involve datatype constructors like \<^term>‹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
\<^term>‹cases› rule would loop if used in that manner because the
pattern~\<^term>‹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) ∈ even ⟹ P"
apply (ind_cases "Suc(Suc n) ∈ even")
oops
text ‹
The specified instance of the ‹cases› rule is generated, then applied
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