Theory Common_Patterns

(*  Title:      HOL/Induct/Common_Patterns.thy
    Author:     Makarius
*)

section ‹Common patterns of induction›

theory Common_Patterns
imports Main
begin

text ‹
  The subsequent Isar proof schemes illustrate common proof patterns
  supported by the generic ‹induct› method.

  To demonstrate variations on statement (goal) structure we refer to
  the induction rule of Peano natural numbers: @{thm nat.induct
  [no_vars]}, which is the simplest case of datatype induction.  We
  shall also see more complex (mutual) datatype inductions involving
  several rules.  Working with inductive predicates is similar, but
  involves explicit facts about membership, instead of implicit
  syntactic typing.
›


subsection ‹Variations on statement structure›

subsubsection ‹Local facts and parameters›

text ‹
  Augmenting a problem by additional facts and locally fixed variables
  is a bread-and-butter method in many applications.  This is where
  unwieldy object-level ‹∀› and ‹⟶› used to occur in
  the past.  The ‹induct› method works with primary means of
  the proof language instead.
›

lemma
  fixes n :: nat
    and x :: 'a
  assumes "A n x"
  shows "P n x" using ‹A n x›
proof (induct n arbitrary: x)
  case 0
  note prem = ‹A 0 x›
  show "P 0 x" \<proof>
next
  case (Suc n)
  note hyp = ‹⋀x. A n x ⟹ P n x›
    and prem = ‹A (Suc n) x›
  show "P (Suc n) x" \<proof>
qed


subsubsection ‹Local definitions›

text ‹
  Here the idea is to turn sub-expressions of the problem into a
  defined induction variable.  This is often accompanied with fixing
  of auxiliary parameters in the original expression, otherwise the
  induction step would refer invariably to particular entities.  This
  combination essentially expresses a partially abstracted
  representation of inductive expressions.
›

lemma
  fixes a :: "'a ⇒ nat"
  assumes "A (a x)"
  shows "P (a x)" using ‹A (a x)›
proof (induct n ≡ "a x" arbitrary: x)
  case 0
  note prem = ‹A (a x)›
    and defn = ‹0 = a x›
  show "P (a x)" \<proof>
next
  case (Suc n)
  note hyp = ‹⋀x. n = a x ⟹ A (a x) ⟹ P (a x)›
    and prem = ‹A (a x)›
    and defn = ‹Suc n = a x›
  show "P (a x)" \<proof>
qed

text ‹
  Observe how the local definition ‹n = a x› recurs in the
  inductive cases as ‹0 = a x› and ‹Suc n = a x›,
  according to underlying induction rule.
›


subsubsection ‹Simple simultaneous goals›

text ‹
  The most basic simultaneous induction operates on several goals
  one-by-one, where each case refers to induction hypotheses that are
  duplicated according to the number of conclusions.
›

lemma
  fixes n :: nat
  shows "P n" and "Q n"
proof (induct n)
  case 0 case 1
  show "P 0" \<proof>
next
  case 0 case 2
  show "Q 0" \<proof>
next
  case (Suc n) case 1
  note hyps = ‹P n› ‹Q n›
  show "P (Suc n)" \<proof>
next
  case (Suc n) case 2
  note hyps = ‹P n› ‹Q n›
  show "Q (Suc n)" \<proof>
qed

text ‹
  The split into subcases may be deferred as follows -- this is
  particularly relevant for goal statements with local premises.
›

lemma
  fixes n :: nat
  shows "A n ⟹ P n"
    and "B n ⟹ Q n"
proof (induct n)
  case 0
  {
    case 1
    note ‹A 0›
    show "P 0" \<proof>
  next
    case 2
    note ‹B 0›
    show "Q 0" \<proof>
  }
next
  case (Suc n)
  note ‹A n ⟹ P n›
    and ‹B n ⟹ Q n›
  {
    case 1
    note ‹A (Suc n)›
    show "P (Suc n)" \<proof>
  next
    case 2
    note ‹B (Suc n)›
    show "Q (Suc n)" \<proof>
  }
qed


subsubsection ‹Compound simultaneous goals›

text ‹
  The following pattern illustrates the slightly more complex
  situation of simultaneous goals with individual local assumptions.
  In compound simultaneous statements like this, local assumptions
  need to be included into each goal, using ‹⟹› of the Pure
  framework.  In contrast, local parameters do not require separate
  ‹⋀› prefixes here, but may be moved into the common context
  of the whole statement.
›

lemma
  fixes n :: nat
    and x :: 'a
    and y :: 'b
  shows "A n x ⟹ P n x"
    and "B n y ⟹ Q n y"
proof (induct n arbitrary: x y)
  case 0
  {
    case 1
    note prem = ‹A 0 x›
    show "P 0 x" \<proof>
  }
  {
    case 2
    note prem = ‹B 0 y›
    show "Q 0 y" \<proof>
  }
next
  case (Suc n)
  note hyps = ‹⋀x. A n x ⟹ P n x› ‹⋀y. B n y ⟹ Q n y›
  then have some_intermediate_result \<proof>
  {
    case 1
    note prem = ‹A (Suc n) x›
    show "P (Suc n) x" \<proof>
  }
  {
    case 2
    note prem = ‹B (Suc n) y›
    show "Q (Suc n) y" \<proof>
  }
qed

text ‹
  Here ‹induct› provides again nested cases with numbered
  sub-cases, which allows to share common parts of the body context.
  In typical applications, there could be a long intermediate proof of
  general consequences of the induction hypotheses, before finishing
  each conclusion separately.
›


subsection ‹Multiple rules›

text ‹
  Multiple induction rules emerge from mutual definitions of
  datatypes, inductive predicates, functions etc.  The ‹induct› method accepts replicated arguments (with ‹and›
  separator), corresponding to each projection of the induction
  principle.

  The goal statement essentially follows the same arrangement,
  although it might be subdivided into simultaneous sub-problems as
  before!
›

datatype foo = Foo1 nat | Foo2 bar
  and bar = Bar1 bool | Bar2 bazar
  and bazar = Bazar foo

text ‹
  The pack of induction rules for this datatype is: @{thm [display]
  foo.induct [no_vars] bar.induct [no_vars] bazar.induct [no_vars]}

  This corresponds to the following basic proof pattern:
›

lemma
  fixes foo :: foo
    and bar :: bar
    and bazar :: bazar
  shows "P foo"
    and "Q bar"
    and "R bazar"
proof (induct foo and bar and bazar)
  case (Foo1 n)
  show "P (Foo1 n)" \<proof>
next
  case (Foo2 bar)
  note ‹Q bar›
  show "P (Foo2 bar)" \<proof>
next
  case (Bar1 b)
  show "Q (Bar1 b)" \<proof>
next
  case (Bar2 bazar)
  note ‹R bazar›
  show "Q (Bar2 bazar)" \<proof>
next
  case (Bazar foo)
  note ‹P foo›
  show "R (Bazar foo)" \<proof>
qed

text ‹
  This can be combined with the previous techniques for compound
  statements, e.g.\ like this.
›

lemma
  fixes x :: 'a and y :: 'b and z :: 'c
    and foo :: foo
    and bar :: bar
    and bazar :: bazar
  shows
    "A x foo ⟹ P x foo"
  and
    "B1 y bar ⟹ Q1 y bar"
    "B2 y bar ⟹ Q2 y bar"
  and
    "C1 z bazar ⟹ R1 z bazar"
    "C2 z bazar ⟹ R2 z bazar"
    "C3 z bazar ⟹ R3 z bazar"
proof (induct foo and bar and bazar arbitrary: x and y and z)
  oops


subsection ‹Inductive predicates›

text ‹
  The most basic form of induction involving predicates (or sets)
  essentially eliminates a given membership fact.
›

inductive Even :: "nat ⇒ bool" where
  zero: "Even 0"
| double: "Even (2 * n)" if "Even n" for n

lemma
  assumes "Even n"
  shows "P n"
  using assms
proof induct
  case zero
  show "P 0" \<proof>
next
  case (double n)
  note ‹Even n› and ‹P n›
  show "P (2 * n)" \<proof>
qed

text ‹
  Alternatively, an initial rule statement may be proven as follows,
  performing ``in-situ'' elimination with explicit rule specification.
›

lemma "Even n ⟹ P n"
proof (induct rule: Even.induct)
  oops

text ‹
  Simultaneous goals do not introduce anything new.
›

lemma
  assumes "Even n"
  shows "P1 n" and "P2 n"
  using assms
proof induct
  case zero
  {
    case 1
    show "P1 0" \<proof>
  next
    case 2
    show "P2 0" \<proof>
  }
next
  case (double n)
  note ‹Even n› and ‹P1 n› and ‹P2 n›
  {
    case 1
    show "P1 (2 * n)" \<proof>
  next
    case 2
    show "P2 (2 * n)" \<proof>
  }
qed

text ‹
  Working with mutual rules requires special care in composing the
  statement as a two-level conjunction, using lists of propositions
  separated by ‹and›.  For example:
›

inductive Evn :: "nat ⇒ bool" and Odd :: "nat ⇒ bool"
where
  zero: "Evn 0"
| succ_Evn: "Odd (Suc n)" if "Evn n" for n
| succ_Odd: "Evn (Suc n)" if "Odd n" for n

lemma
    "Evn n ⟹ P1 n"
    "Evn n ⟹ P2 n"
    "Evn n ⟹ P3 n"
  and
    "Odd n ⟹ Q1 n"
    "Odd n ⟹ Q2 n"
proof (induct rule: Evn_Odd.inducts)
  case zero
  { case 1 show "P1 0" \<proof> }
  { case 2 show "P2 0" \<proof> }
  { case 3 show "P3 0" \<proof> }
next
  case (succ_Evn n)
  note ‹Evn n› and ‹P1 n› ‹P2 n› ‹P3 n›
  { case 1 show "Q1 (Suc n)" \<proof> }
  { case 2 show "Q2 (Suc n)" \<proof> }
next
  case (succ_Odd n)
  note ‹Odd n› and ‹Q1 n› ‹Q2 n›
  { case 1 show "P1 (Suc n)" \<proof> }
  { case 2 show "P2 (Suc n)" \<proof> }
  { case 3 show "P3 (Suc n)" \<proof> }
qed


text ‹
  Cases and hypotheses in each case can be named explicitly.
›

inductive star :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for r
where
  refl: "star r x x" for x
| step: "star r x z" if "r x y" and "star r y z" for x y z

text ‹Underscores are replaced by the default name hyps:›

lemmas star_induct = star.induct [case_names base step[r _ IH]]

lemma "star r x y ⟹ star r y z ⟹ star r x z"
proof (induct rule: star_induct) print_cases
  case base
  then show ?case .
next
  case (step a b c) print_facts
  from step.prems have "star r b z" by (rule step.IH)
  with step.r show ?case by (rule star.step)
qed

end