# HG changeset patch
# User wenzelm
# Date 1189969485 -7200
# Node ID aae1095dbe3b0d98217f7f8c6053b0c6e55f18c3
# Parent  fc06b84acd81f92b791e6e5ed9cbcf55e8ce2a48
HOL/Induct/Common_Patterns.thy

diff -r fc06b84acd81 -r aae1095dbe3b src/HOL/Induct/Common_Patterns.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Common_Patterns.thy	Sun Sep 16 21:04:45 2007 +0200
@@ -0,0 +1,372 @@
+(*  Title:      HOL/Induct/Common_Patterns.thy
+    ID:         $Id$
+    Author:     Makarius
+*)
+
+header {* Common patterns of induction *}
+
+theory Common_Patterns
+imports Main
+begin
+
+text {*
+  The subsequent Isar proof schemes illustrate common proof patterns
+  supported by the generic @{text "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 @{text "\<forall>"} and @{text "\<longrightarrow>"} used to occur in
+  the past.  The @{text "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" sorry
+next
+  case (Suc n)
+  note hyp = `\<And>x. A n x \<Longrightarrow> P n x`
+    and prem = `A (Suc n) x`
+  show "P (Suc n) x" sorry
+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 \<Rightarrow> nat"
+  assumes "A (a x)"
+  shows "P (a x)" using `A (a x)`
+proof (induct n \<equiv> "a x" arbitrary: x)
+  case 0
+  note prem = `A (a x)`
+    and defn = `0 = a x`
+  show "P (a x)" sorry
+next
+  case (Suc n)
+  note hyp = `\<And>x. A (a x) \<Longrightarrow> n = a x \<Longrightarrow> P (a x)`
+    and prem = `A (a x)`
+    and defn = `Suc n = a x`
+  show "P (a x)" sorry
+qed
+
+text {*
+  Observe how the local definition @{text "n = a x"} recurs in the
+  inductive cases as @{text "0 = a x"} and @{text "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" sorry
+next
+  case 0 case 2
+  show "Q 0" sorry
+next
+  case (Suc n) case 1
+  note hyps = `P n` `Q n`
+  show "P (Suc n)" sorry
+next
+  case (Suc n) case 2
+  note hyps = `P n` `Q n`
+  show "Q (Suc n)" sorry
+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 \<Longrightarrow> P n"
+    and "B n \<Longrightarrow> Q n"
+proof (induct n)
+  case 0
+  {
+    case 1
+    note `A 0`
+    show "P 0" sorry
+  next
+    case 2
+    note `B 0`
+    show "Q 0" sorry
+  }
+next
+  case (Suc n)
+  note `A n \<Longrightarrow> P n`
+    and `B n \<Longrightarrow> Q n`
+  {
+    case 1
+    note `A (Suc n)`
+    show "P (Suc n)" sorry
+  next
+    case 2
+    note `B (Suc n)`
+    show "Q (Suc n)" sorry
+  }
+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 @{text "\<Longrightarrow>"} of the Pure
+  framework.  In contrast, local parameters do not require separate
+  @{text "\<And>"} 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 \<Longrightarrow> P n x"
+    and "B n y \<Longrightarrow> Q n y"
+proof (induct n arbitrary: x y)
+  case 0
+  {
+    case 1
+    note prem = `A 0 x`
+    show "P 0 x" sorry
+  }
+  {
+    case 2
+    note prem = `B 0 y`
+    show "Q 0 y" sorry
+  }
+next
+  case (Suc n)
+  note hyps = `\<And>x. A n x \<Longrightarrow> P n x` `\<And>y. B n y \<Longrightarrow> Q n y`
+  then have some_intermediate_result sorry
+  {
+    case 1
+    note prem = `A (Suc n) x`
+    show "P (Suc n) x" sorry
+  }
+  {
+    case 2
+    note prem = `B (Suc n) y`
+    show "Q (Suc n) y" sorry
+  }
+qed
+
+text {*
+  Here @{text "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 @{text
+  "induct"} method accepts replicated arguments (with @{text "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_bar_bazar.inducts [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)" sorry
+next
+  case (Foo2 bar)
+  note `Q bar`
+  show "P (Foo2 bar)" sorry
+next
+  case (Bar1 b)
+  show "Q (Bar1 b)" sorry
+next
+  case (Bar2 bazar)
+  note `R bazar`
+  show "Q (Bar2 bazar)" sorry
+next
+  case (Bazar foo)
+  note `P foo`
+  show "R (Bazar foo)" sorry
+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 \<Longrightarrow> P x foo"
+  and
+    "B1 y bar \<Longrightarrow> Q1 y bar"
+    "B2 y bar \<Longrightarrow> Q2 y bar"
+  and
+    "C1 z bazar \<Longrightarrow> R1 z bazar"
+    "C2 z bazar \<Longrightarrow> R2 z bazar"
+    "C3 z bazar \<Longrightarrow> 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 \<Rightarrow> bool" where
+  zero: "Even 0"
+| double: "Even n \<Longrightarrow> Even (2 * n)"
+
+lemma
+  assumes "Even n"
+  shows "P n"
+  using assms
+proof induct
+  case zero
+  show "P 0" sorry
+next
+  case (double n)
+  note `Even n` and `P n`
+  show "P (2 * n)" sorry
+qed
+
+text {*
+  Alternatively, an initial rule statement may be proven as follows,
+  performing ``in-situ'' elimination with explicit rule specification.
+*}
+
+lemma "Even n \<Longrightarrow> 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" sorry
+  next
+    case 2
+    show "P2 0" sorry
+  }
+next
+  case (double n)
+  note `Even n` and `P1 n` and `P2 n`
+  {
+    case 1
+    show "P1 (2 * n)" sorry
+  next
+    case 2
+    show "P2 (2 * n)" sorry
+  }
+qed
+
+text {*
+  Working with mutual rules requires special care in composing the
+  statement as a two-level conjunction, using lists of propositions
+  separated by @{text "and"}.  For example:
+*}
+
+inductive Evn :: "nat \<Rightarrow> bool" and Odd :: "nat \<Rightarrow> bool"
+where
+  zero: "Evn 0"
+| succ_Evn: "Evn n \<Longrightarrow> Odd (Suc n)"
+| succ_Odd: "Odd n \<Longrightarrow> Evn (Suc n)"
+
+lemma "Evn n \<Longrightarrow> P n"
+  and "Odd n \<Longrightarrow> Q n"
+proof (induct rule: Evn_Odd.inducts)
+  case zero
+  show "P 0" sorry
+next
+  case (succ_Evn n)
+  note `Evn n` and `P n`
+  show "Q (Suc n)" sorry
+next
+  case (succ_Odd n)
+  note `Odd n` and `Q n`
+  show "P (Suc n)" sorry
+qed
+
+end
\ No newline at end of file