(*<*)theory Even imports "../Setup" begin(*>*)

section‹The Set of Even Numbers›

text ‹
 index{even numbers!defining inductively|(}%
  set of even numbers can be inductively defined as the least set
  0 and closed under the operation $+2$. Obviously,
 emph{even} can also be expressed using the divides relation (‹dvd›).
  shall prove below that the two formulations coincide. On the way we
  examine the primary means of reasoning about inductively defined
 : rule induction.
 ›

subsection‹Making an Inductive Definition›

text ‹
  \commdx{inductive\protect\_set}, we declare the constant ‹even› to be
  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 ‹
  inductive definition consists of introduction rules. The first one
  states that 0 is even; the second states that if $n$ is even, then so
 ~$n+2$. Given this declaration, Isabelle generates a fixed point
  for term‹even› and proves theorems about it,
  following the definitional approach (see {\S}\ref{sec:definitional}).
  theorems
  the introduction rules specified in the declaration, an elimination
  for case analysis and an induction rule. We can refer to these
  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)}

  introduction rules can be given attributes. Here
  rules are specified as \isa{intro!},%
 index{intro"!@\isa {intro"!} (attribute)}
  the classical reasoner to
  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
 . We prove this equivalence later.
 ›

subsection‹Using Introduction Rules›

text ‹
  first lemma states that numbers of the form $2\times k$ are even.
  rules are used to show that specific values belong to the
  set. Such proofs typically involve
 , 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
  first step is induction on the natural number ‹k›, which leaves
  subgoals:
 {subgoals[display,indent=0,margin=65]}
  ‹auto› simplifies both subgoals so that they match the introduction
 , which are then applied automatically.

  ultimate goal is to prove the equivalence between the traditional
  of ‹even› (using the divides relation) and our inductive
 . One direction of this equivalence is immediate by the lemma
  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|(}%
  the definition of the set
 term‹even›, Isabelle has
  an induction rule:
 {named_thms [display,indent=0,margin=40] even.induct [no_vars] (even.induct)}
  property term‹P› holds for every even number provided it
  for~‹0› and is closed under the operation
 isa{Suc(Suc \(\cdot\))}. Then term‹P› is closed under the introduction
  for term‹even›, which is the least set closed under those rules.
  type of inductive argument is called \textbf{rule induction}.

  from the double application of term‹Suc›, the induction rule above
  the familiar mathematical induction, which indeed is an instance
  rule induction; the natural numbers can be defined inductively to be
  least set containing ‹0› and closed under~term‹Suc›.

  is the usual way of proving a property of the elements of an
  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 ‹
  begin by applying induction. Note that ‹even.induct› has the form
  an elimination rule, so we use the method ‹erule›. We get two
 :
 ›
apply (erule even.induct)
txt ‹
 {subgoals[display,indent=0]}
  unfold the definition of ‹dvd› in both subgoals, proving the first
  and simplifying the second:
 ›
apply (simp_all add: dvd_def)
txt ‹
 {subgoals[display,indent=0]}
  next command eliminates the existential quantifier from the assumption
  replaces ‹n› by ‹2 * k›.
 ›
apply clarify
txt ‹
 {subgoals[display,indent=0]}
  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 ‹
  the previous two results yields our objective, the
  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}%
  applying induction, we typically must generalize
  induction formula. With rule induction, the required generalization
  be hard to find and sometimes requires a complete reformulation of the
 . In this example, our first attempt uses the obvious statement of
  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 ‹
  induction finds no occurrences of term‹Suc(Suc n)› in the
 , which it therefore leaves unchanged. (Look at
 ‹even.induct› to see why this happens.) We have these subgoals:
 {subgoals[display,indent=0]}
  first one is hopeless. Rule induction on
  non-variable term discards information, and usually fails.
  to deal with such situations
  general is described in {\S}\ref{sec:ind-var-in-prems} below.
  the current case the solution is easy because
  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 ‹
  lemma is trivially inductive. Here are the subgoals:
 {subgoals[display,indent=0]}
  first is trivial because ‹0 - 2› simplifies to ‹0›, which is
 . 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
  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 ‹
  have just proved the converse of the introduction rule ‹even.step›.
  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|(}%
  analysis on an inductive definition is called \textbf{rule
 }. It is frequently used in proofs about operational
 . It can be highly effective when it is applied
 . Let us look at how rule inversion is done in
 /HOL\@.

  that term‹even› is the minimal set closed under these two rules:
 {thm [display,indent=0] even.intros [no_vars]}
  means that term‹even› contains only the elements that these
  force it to contain. If we are told that term‹a›
  to
 term‹even› then there are only two possibilities. Either term‹a› is ‹0›
  else term‹a› has the form term‹Suc(Suc n)›, for some suitable term‹n›
  belongs to
 term‹even›. That is the gist of the term‹cases› rule, which Isabelle proves
  us when it accepts an inductive definition:
 {named_thms [display,indent=0,margin=40] even.cases [no_vars] (even.cases)}
  general rule is less useful than instances of it for
  patterns. For example, if term‹a› has the form
 term‹Suc(Suc n)› then the first case becomes irrelevant, while the second
  tells us that term‹n› belongs to term‹even›. Isabelle will generate
  instance for us:
 ›

inductive_cases Suc_Suc_cases [elim!]: "Suc(Suc n) ∈ even"

text ‹
  \commdx{inductive\protect\_cases} command generates an instance of
  ‹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)}
  this as an elimination rule yields one case where ‹even.cases›
  yield two. Rule inversion works well when the conclusions of the
  rules involve datatype constructors like term‹Suc› and ‹#›
 list ``cons''); freeness reasoning discards all but one or two cases.

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

  rule ‹Suc_Suc_cases› is equivalent to the following implication:
 {term [display,indent=0] "Suc (Suc n) ∈ even ==> n ∈ even"}
  above we devoted some effort to reaching precisely
  result. Yet we could have obtained it by a one-line declaration,
  with the lemma ‹even_imp_even_minus_2›.
  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
  introduces is disjoint from those of the other introduction rules.

  one-off applications of rule inversion, use the \methdx{ind_cases} method.
  is an example:
 ›

(*<*)lemma "Suc(Suc n) \<in> even \<Longrightarrow> P"(*>*)
apply (ind_cases "Suc(Suc n) ∈ even")
(*<*)oops(*>*)

text ‹
  specified instance of the ‹cases› rule is generated, then applied
  an elimination rule.

  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›
 .

  even numbers example has shown how inductive definitions can be
 . Later examples will show that they are actually worth using.%
 index{rule inversion|)}%
 index{even numbers!defining inductively|)}
 ›

(*<*)end(*>*)