HOL/Induct/Common_Patterns.thy
authorwenzelm
Sun Sep 16 21:04:45 2007 +0200 (2007-09-16)
changeset 24608aae1095dbe3b
parent 24607 fc06b84acd81
child 24609 3f238d4987c0
HOL/Induct/Common_Patterns.thy
src/HOL/Induct/Common_Patterns.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Induct/Common_Patterns.thy	Sun Sep 16 21:04:45 2007 +0200
     1.3 @@ -0,0 +1,372 @@
     1.4 +(*  Title:      HOL/Induct/Common_Patterns.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +*)
     1.8 +
     1.9 +header {* Common patterns of induction *}
    1.10 +
    1.11 +theory Common_Patterns
    1.12 +imports Main
    1.13 +begin
    1.14 +
    1.15 +text {*
    1.16 +  The subsequent Isar proof schemes illustrate common proof patterns
    1.17 +  supported by the generic @{text "induct"} method.
    1.18 +
    1.19 +  To demonstrate variations on statement (goal) structure we refer to
    1.20 +  the induction rule of Peano natural numbers: @{thm nat.induct
    1.21 +  [no_vars]}, which is the simplest case of datatype induction.  We
    1.22 +  shall also see more complex (mutual) datatype inductions involving
    1.23 +  several rules.  Working with inductive predicates is similar, but
    1.24 +  involves explicit facts about membership, instead of implicit
    1.25 +  syntactic typing.
    1.26 +*}
    1.27 +
    1.28 +
    1.29 +subsection {* Variations on statement structure *}
    1.30 +
    1.31 +subsubsection {* Local facts and parameters *}
    1.32 +
    1.33 +text {*
    1.34 +  Augmenting a problem by additional facts and locally fixed variables
    1.35 +  is a bread-and-butter method in many applications.  This is where
    1.36 +  unwieldy object-level @{text "\<forall>"} and @{text "\<longrightarrow>"} used to occur in
    1.37 +  the past.  The @{text "induct"} method works with primary means of
    1.38 +  the proof language instead.
    1.39 +*}
    1.40 +
    1.41 +lemma
    1.42 +  fixes n :: nat
    1.43 +    and x :: 'a
    1.44 +  assumes "A n x"
    1.45 +  shows "P n x" using `A n x`
    1.46 +proof (induct n arbitrary: x)
    1.47 +  case 0
    1.48 +  note prem = `A 0 x`
    1.49 +  show "P 0 x" sorry
    1.50 +next
    1.51 +  case (Suc n)
    1.52 +  note hyp = `\<And>x. A n x \<Longrightarrow> P n x`
    1.53 +    and prem = `A (Suc n) x`
    1.54 +  show "P (Suc n) x" sorry
    1.55 +qed
    1.56 +
    1.57 +
    1.58 +subsubsection {* Local definitions *}
    1.59 +
    1.60 +text {*
    1.61 +  Here the idea is to turn sub-expressions of the problem into a
    1.62 +  defined induction variable.  This is often accompanied with fixing
    1.63 +  of auxiliary parameters in the original expression, otherwise the
    1.64 +  induction step would refer invariably to particular entities.  This
    1.65 +  combination essentially expresses a partially abstracted
    1.66 +  representation of inductive expressions.
    1.67 +*}
    1.68 +
    1.69 +lemma
    1.70 +  fixes a :: "'a \<Rightarrow> nat"
    1.71 +  assumes "A (a x)"
    1.72 +  shows "P (a x)" using `A (a x)`
    1.73 +proof (induct n \<equiv> "a x" arbitrary: x)
    1.74 +  case 0
    1.75 +  note prem = `A (a x)`
    1.76 +    and defn = `0 = a x`
    1.77 +  show "P (a x)" sorry
    1.78 +next
    1.79 +  case (Suc n)
    1.80 +  note hyp = `\<And>x. A (a x) \<Longrightarrow> n = a x \<Longrightarrow> P (a x)`
    1.81 +    and prem = `A (a x)`
    1.82 +    and defn = `Suc n = a x`
    1.83 +  show "P (a x)" sorry
    1.84 +qed
    1.85 +
    1.86 +text {*
    1.87 +  Observe how the local definition @{text "n = a x"} recurs in the
    1.88 +  inductive cases as @{text "0 = a x"} and @{text "Suc n = a x"},
    1.89 +  according to underlying induction rule.
    1.90 +*}
    1.91 +
    1.92 +
    1.93 +subsubsection {* Simple simultaneous goals *}
    1.94 +
    1.95 +text {*
    1.96 +  The most basic simultaneous induction operates on several goals
    1.97 +  one-by-one, where each case refers to induction hypotheses that are
    1.98 +  duplicated according to the number of conclusions.
    1.99 +*}
   1.100 +
   1.101 +lemma
   1.102 +  fixes n :: nat
   1.103 +  shows "P n" and "Q n"
   1.104 +proof (induct n)
   1.105 +  case 0 case 1
   1.106 +  show "P 0" sorry
   1.107 +next
   1.108 +  case 0 case 2
   1.109 +  show "Q 0" sorry
   1.110 +next
   1.111 +  case (Suc n) case 1
   1.112 +  note hyps = `P n` `Q n`
   1.113 +  show "P (Suc n)" sorry
   1.114 +next
   1.115 +  case (Suc n) case 2
   1.116 +  note hyps = `P n` `Q n`
   1.117 +  show "Q (Suc n)" sorry
   1.118 +qed
   1.119 +
   1.120 +text {*
   1.121 +  The split into subcases may be deferred as follows -- this is
   1.122 +  particularly relevant for goal statements with local premises.
   1.123 +*}
   1.124 +
   1.125 +lemma
   1.126 +  fixes n :: nat
   1.127 +  shows "A n \<Longrightarrow> P n"
   1.128 +    and "B n \<Longrightarrow> Q n"
   1.129 +proof (induct n)
   1.130 +  case 0
   1.131 +  {
   1.132 +    case 1
   1.133 +    note `A 0`
   1.134 +    show "P 0" sorry
   1.135 +  next
   1.136 +    case 2
   1.137 +    note `B 0`
   1.138 +    show "Q 0" sorry
   1.139 +  }
   1.140 +next
   1.141 +  case (Suc n)
   1.142 +  note `A n \<Longrightarrow> P n`
   1.143 +    and `B n \<Longrightarrow> Q n`
   1.144 +  {
   1.145 +    case 1
   1.146 +    note `A (Suc n)`
   1.147 +    show "P (Suc n)" sorry
   1.148 +  next
   1.149 +    case 2
   1.150 +    note `B (Suc n)`
   1.151 +    show "Q (Suc n)" sorry
   1.152 +  }
   1.153 +qed
   1.154 +
   1.155 +
   1.156 +subsubsection {* Compound simultaneous goals *}
   1.157 +
   1.158 +text {*
   1.159 +  The following pattern illustrates the slightly more complex
   1.160 +  situation of simultaneous goals with individual local assumptions.
   1.161 +  In compound simultaneous statements like this, local assumptions
   1.162 +  need to be included into each goal, using @{text "\<Longrightarrow>"} of the Pure
   1.163 +  framework.  In contrast, local parameters do not require separate
   1.164 +  @{text "\<And>"} prefixes here, but may be moved into the common context
   1.165 +  of the whole statement.
   1.166 +*}
   1.167 +
   1.168 +lemma
   1.169 +  fixes n :: nat
   1.170 +    and x :: 'a
   1.171 +    and y :: 'b
   1.172 +  shows "A n x \<Longrightarrow> P n x"
   1.173 +    and "B n y \<Longrightarrow> Q n y"
   1.174 +proof (induct n arbitrary: x y)
   1.175 +  case 0
   1.176 +  {
   1.177 +    case 1
   1.178 +    note prem = `A 0 x`
   1.179 +    show "P 0 x" sorry
   1.180 +  }
   1.181 +  {
   1.182 +    case 2
   1.183 +    note prem = `B 0 y`
   1.184 +    show "Q 0 y" sorry
   1.185 +  }
   1.186 +next
   1.187 +  case (Suc n)
   1.188 +  note hyps = `\<And>x. A n x \<Longrightarrow> P n x` `\<And>y. B n y \<Longrightarrow> Q n y`
   1.189 +  then have some_intermediate_result sorry
   1.190 +  {
   1.191 +    case 1
   1.192 +    note prem = `A (Suc n) x`
   1.193 +    show "P (Suc n) x" sorry
   1.194 +  }
   1.195 +  {
   1.196 +    case 2
   1.197 +    note prem = `B (Suc n) y`
   1.198 +    show "Q (Suc n) y" sorry
   1.199 +  }
   1.200 +qed
   1.201 +
   1.202 +text {*
   1.203 +  Here @{text "induct"} provides again nested cases with numbered
   1.204 +  sub-cases, which allows to share common parts of the body context.
   1.205 +  In typical applications, there could be a long intermediate proof of
   1.206 +  general consequences of the induction hypotheses, before finishing
   1.207 +  each conclusion separately.
   1.208 +*}
   1.209 +
   1.210 +
   1.211 +subsection {* Multiple rules *}
   1.212 +
   1.213 +text {*
   1.214 +  Multiple induction rules emerge from mutual definitions of
   1.215 +  datatypes, inductive predicates, functions etc.  The @{text
   1.216 +  "induct"} method accepts replicated arguments (with @{text "and"}
   1.217 +  separator), corresponding to each projection of the induction
   1.218 +  principle.
   1.219 +
   1.220 +  The goal statement essentially follows the same arrangement,
   1.221 +  although it might be subdivided into simultaneous sub-problems as
   1.222 +  before!
   1.223 +*}
   1.224 +
   1.225 +datatype foo = Foo1 nat | Foo2 bar
   1.226 +  and bar = Bar1 bool | Bar2 bazar
   1.227 +  and bazar = Bazar foo
   1.228 +
   1.229 +text {*
   1.230 +  The pack of induction rules for this datatype is: @{thm [display]
   1.231 +  foo_bar_bazar.inducts [no_vars]}
   1.232 +
   1.233 +  This corresponds to the following basic proof pattern:
   1.234 +*}
   1.235 +
   1.236 +lemma
   1.237 +  fixes foo :: foo
   1.238 +    and bar :: bar
   1.239 +    and bazar :: bazar
   1.240 +  shows "P foo"
   1.241 +    and "Q bar"
   1.242 +    and "R bazar"
   1.243 +proof (induct foo and bar and bazar)
   1.244 +  case (Foo1 n)
   1.245 +  show "P (Foo1 n)" sorry
   1.246 +next
   1.247 +  case (Foo2 bar)
   1.248 +  note `Q bar`
   1.249 +  show "P (Foo2 bar)" sorry
   1.250 +next
   1.251 +  case (Bar1 b)
   1.252 +  show "Q (Bar1 b)" sorry
   1.253 +next
   1.254 +  case (Bar2 bazar)
   1.255 +  note `R bazar`
   1.256 +  show "Q (Bar2 bazar)" sorry
   1.257 +next
   1.258 +  case (Bazar foo)
   1.259 +  note `P foo`
   1.260 +  show "R (Bazar foo)" sorry
   1.261 +qed
   1.262 +
   1.263 +text {*
   1.264 +  This can be combined with the previous techniques for compound
   1.265 +  statements, e.g.\ like this.
   1.266 +*}
   1.267 +
   1.268 +lemma
   1.269 +  fixes x :: 'a and y :: 'b and z :: 'c
   1.270 +    and foo :: foo
   1.271 +    and bar :: bar
   1.272 +    and bazar :: bazar
   1.273 +  shows
   1.274 +    "A x foo \<Longrightarrow> P x foo"
   1.275 +  and
   1.276 +    "B1 y bar \<Longrightarrow> Q1 y bar"
   1.277 +    "B2 y bar \<Longrightarrow> Q2 y bar"
   1.278 +  and
   1.279 +    "C1 z bazar \<Longrightarrow> R1 z bazar"
   1.280 +    "C2 z bazar \<Longrightarrow> R2 z bazar"
   1.281 +    "C3 z bazar \<Longrightarrow> R3 z bazar"
   1.282 +proof (induct foo and bar and bazar arbitrary: x and y and z)
   1.283 +  oops
   1.284 +
   1.285 +
   1.286 +subsection {* Inductive predicates *}
   1.287 +
   1.288 +text {*
   1.289 +  The most basic form of induction involving predicates (or sets)
   1.290 +  essentially eliminates a given membership fact.
   1.291 +*}
   1.292 +
   1.293 +inductive Even :: "nat \<Rightarrow> bool" where
   1.294 +  zero: "Even 0"
   1.295 +| double: "Even n \<Longrightarrow> Even (2 * n)"
   1.296 +
   1.297 +lemma
   1.298 +  assumes "Even n"
   1.299 +  shows "P n"
   1.300 +  using assms
   1.301 +proof induct
   1.302 +  case zero
   1.303 +  show "P 0" sorry
   1.304 +next
   1.305 +  case (double n)
   1.306 +  note `Even n` and `P n`
   1.307 +  show "P (2 * n)" sorry
   1.308 +qed
   1.309 +
   1.310 +text {*
   1.311 +  Alternatively, an initial rule statement may be proven as follows,
   1.312 +  performing ``in-situ'' elimination with explicit rule specification.
   1.313 +*}
   1.314 +
   1.315 +lemma "Even n \<Longrightarrow> P n"
   1.316 +proof (induct rule: Even.induct)
   1.317 +  oops
   1.318 +
   1.319 +text {*
   1.320 +  Simultaneous goals do not introduce anything new.
   1.321 +*}
   1.322 +
   1.323 +lemma
   1.324 +  assumes "Even n"
   1.325 +  shows "P1 n" and "P2 n"
   1.326 +  using assms
   1.327 +proof induct
   1.328 +  case zero
   1.329 +  {
   1.330 +    case 1
   1.331 +    show "P1 0" sorry
   1.332 +  next
   1.333 +    case 2
   1.334 +    show "P2 0" sorry
   1.335 +  }
   1.336 +next
   1.337 +  case (double n)
   1.338 +  note `Even n` and `P1 n` and `P2 n`
   1.339 +  {
   1.340 +    case 1
   1.341 +    show "P1 (2 * n)" sorry
   1.342 +  next
   1.343 +    case 2
   1.344 +    show "P2 (2 * n)" sorry
   1.345 +  }
   1.346 +qed
   1.347 +
   1.348 +text {*
   1.349 +  Working with mutual rules requires special care in composing the
   1.350 +  statement as a two-level conjunction, using lists of propositions
   1.351 +  separated by @{text "and"}.  For example:
   1.352 +*}
   1.353 +
   1.354 +inductive Evn :: "nat \<Rightarrow> bool" and Odd :: "nat \<Rightarrow> bool"
   1.355 +where
   1.356 +  zero: "Evn 0"
   1.357 +| succ_Evn: "Evn n \<Longrightarrow> Odd (Suc n)"
   1.358 +| succ_Odd: "Odd n \<Longrightarrow> Evn (Suc n)"
   1.359 +
   1.360 +lemma "Evn n \<Longrightarrow> P n"
   1.361 +  and "Odd n \<Longrightarrow> Q n"
   1.362 +proof (induct rule: Evn_Odd.inducts)
   1.363 +  case zero
   1.364 +  show "P 0" sorry
   1.365 +next
   1.366 +  case (succ_Evn n)
   1.367 +  note `Evn n` and `P n`
   1.368 +  show "Q (Suc n)" sorry
   1.369 +next
   1.370 +  case (succ_Odd n)
   1.371 +  note `Odd n` and `Q n`
   1.372 +  show "P (Suc n)" sorry
   1.373 +qed
   1.374 +
   1.375 +end
   1.376 \ No newline at end of file