24608

1 
(* Title: HOL/Induct/Common_Patterns.thy


2 
ID: $Id$


3 
Author: Makarius


4 
*)


5 


6 
header {* Common patterns of induction *}


7 


8 
theory Common_Patterns


9 
imports Main


10 
begin


11 


12 
text {*


13 
The subsequent Isar proof schemes illustrate common proof patterns


14 
supported by the generic @{text "induct"} method.


15 


16 
To demonstrate variations on statement (goal) structure we refer to


17 
the induction rule of Peano natural numbers: @{thm nat.induct


18 
[no_vars]}, which is the simplest case of datatype induction. We


19 
shall also see more complex (mutual) datatype inductions involving


20 
several rules. Working with inductive predicates is similar, but


21 
involves explicit facts about membership, instead of implicit


22 
syntactic typing.


23 
*}


24 


25 


26 
subsection {* Variations on statement structure *}


27 


28 
subsubsection {* Local facts and parameters *}


29 


30 
text {*


31 
Augmenting a problem by additional facts and locally fixed variables


32 
is a breadandbutter method in many applications. This is where


33 
unwieldy objectlevel @{text "\<forall>"} and @{text "\<longrightarrow>"} used to occur in


34 
the past. The @{text "induct"} method works with primary means of


35 
the proof language instead.


36 
*}


37 


38 
lemma


39 
fixes n :: nat


40 
and x :: 'a


41 
assumes "A n x"


42 
shows "P n x" using `A n x`


43 
proof (induct n arbitrary: x)


44 
case 0


45 
note prem = `A 0 x`


46 
show "P 0 x" sorry


47 
next


48 
case (Suc n)


49 
note hyp = `\<And>x. A n x \<Longrightarrow> P n x`


50 
and prem = `A (Suc n) x`


51 
show "P (Suc n) x" sorry


52 
qed


53 


54 


55 
subsubsection {* Local definitions *}


56 


57 
text {*


58 
Here the idea is to turn subexpressions of the problem into a


59 
defined induction variable. This is often accompanied with fixing


60 
of auxiliary parameters in the original expression, otherwise the


61 
induction step would refer invariably to particular entities. This


62 
combination essentially expresses a partially abstracted


63 
representation of inductive expressions.


64 
*}


65 


66 
lemma


67 
fixes a :: "'a \<Rightarrow> nat"


68 
assumes "A (a x)"


69 
shows "P (a x)" using `A (a x)`


70 
proof (induct n \<equiv> "a x" arbitrary: x)


71 
case 0


72 
note prem = `A (a x)`


73 
and defn = `0 = a x`


74 
show "P (a x)" sorry


75 
next


76 
case (Suc n)


77 
note hyp = `\<And>x. A (a x) \<Longrightarrow> n = a x \<Longrightarrow> P (a x)`


78 
and prem = `A (a x)`


79 
and defn = `Suc n = a x`


80 
show "P (a x)" sorry


81 
qed


82 


83 
text {*


84 
Observe how the local definition @{text "n = a x"} recurs in the


85 
inductive cases as @{text "0 = a x"} and @{text "Suc n = a x"},


86 
according to underlying induction rule.


87 
*}


88 


89 


90 
subsubsection {* Simple simultaneous goals *}


91 


92 
text {*


93 
The most basic simultaneous induction operates on several goals


94 
onebyone, where each case refers to induction hypotheses that are


95 
duplicated according to the number of conclusions.


96 
*}


97 


98 
lemma


99 
fixes n :: nat


100 
shows "P n" and "Q n"


101 
proof (induct n)


102 
case 0 case 1


103 
show "P 0" sorry


104 
next


105 
case 0 case 2


106 
show "Q 0" sorry


107 
next


108 
case (Suc n) case 1


109 
note hyps = `P n` `Q n`


110 
show "P (Suc n)" sorry


111 
next


112 
case (Suc n) case 2


113 
note hyps = `P n` `Q n`


114 
show "Q (Suc n)" sorry


115 
qed


116 


117 
text {*


118 
The split into subcases may be deferred as follows  this is


119 
particularly relevant for goal statements with local premises.


120 
*}


121 


122 
lemma


123 
fixes n :: nat


124 
shows "A n \<Longrightarrow> P n"


125 
and "B n \<Longrightarrow> Q n"


126 
proof (induct n)


127 
case 0


128 
{


129 
case 1


130 
note `A 0`


131 
show "P 0" sorry


132 
next


133 
case 2


134 
note `B 0`


135 
show "Q 0" sorry


136 
}


137 
next


138 
case (Suc n)


139 
note `A n \<Longrightarrow> P n`


140 
and `B n \<Longrightarrow> Q n`


141 
{


142 
case 1


143 
note `A (Suc n)`


144 
show "P (Suc n)" sorry


145 
next


146 
case 2


147 
note `B (Suc n)`


148 
show "Q (Suc n)" sorry


149 
}


150 
qed


151 


152 


153 
subsubsection {* Compound simultaneous goals *}


154 


155 
text {*


156 
The following pattern illustrates the slightly more complex


157 
situation of simultaneous goals with individual local assumptions.


158 
In compound simultaneous statements like this, local assumptions


159 
need to be included into each goal, using @{text "\<Longrightarrow>"} of the Pure


160 
framework. In contrast, local parameters do not require separate


161 
@{text "\<And>"} prefixes here, but may be moved into the common context


162 
of the whole statement.


163 
*}


164 


165 
lemma


166 
fixes n :: nat


167 
and x :: 'a


168 
and y :: 'b


169 
shows "A n x \<Longrightarrow> P n x"


170 
and "B n y \<Longrightarrow> Q n y"


171 
proof (induct n arbitrary: x y)


172 
case 0


173 
{


174 
case 1


175 
note prem = `A 0 x`


176 
show "P 0 x" sorry


177 
}


178 
{


179 
case 2


180 
note prem = `B 0 y`


181 
show "Q 0 y" sorry


182 
}


183 
next


184 
case (Suc n)


185 
note hyps = `\<And>x. A n x \<Longrightarrow> P n x` `\<And>y. B n y \<Longrightarrow> Q n y`


186 
then have some_intermediate_result sorry


187 
{


188 
case 1


189 
note prem = `A (Suc n) x`


190 
show "P (Suc n) x" sorry


191 
}


192 
{


193 
case 2


194 
note prem = `B (Suc n) y`


195 
show "Q (Suc n) y" sorry


196 
}


197 
qed


198 


199 
text {*


200 
Here @{text "induct"} provides again nested cases with numbered


201 
subcases, which allows to share common parts of the body context.


202 
In typical applications, there could be a long intermediate proof of


203 
general consequences of the induction hypotheses, before finishing


204 
each conclusion separately.


205 
*}


206 


207 


208 
subsection {* Multiple rules *}


209 


210 
text {*


211 
Multiple induction rules emerge from mutual definitions of


212 
datatypes, inductive predicates, functions etc. The @{text


213 
"induct"} method accepts replicated arguments (with @{text "and"}


214 
separator), corresponding to each projection of the induction


215 
principle.


216 


217 
The goal statement essentially follows the same arrangement,


218 
although it might be subdivided into simultaneous subproblems as


219 
before!


220 
*}


221 


222 
datatype foo = Foo1 nat  Foo2 bar


223 
and bar = Bar1 bool  Bar2 bazar


224 
and bazar = Bazar foo


225 


226 
text {*


227 
The pack of induction rules for this datatype is: @{thm [display]


228 
foo_bar_bazar.inducts [no_vars]}


229 


230 
This corresponds to the following basic proof pattern:


231 
*}


232 


233 
lemma


234 
fixes foo :: foo


235 
and bar :: bar


236 
and bazar :: bazar


237 
shows "P foo"


238 
and "Q bar"


239 
and "R bazar"


240 
proof (induct foo and bar and bazar)


241 
case (Foo1 n)


242 
show "P (Foo1 n)" sorry


243 
next


244 
case (Foo2 bar)


245 
note `Q bar`


246 
show "P (Foo2 bar)" sorry


247 
next


248 
case (Bar1 b)


249 
show "Q (Bar1 b)" sorry


250 
next


251 
case (Bar2 bazar)


252 
note `R bazar`


253 
show "Q (Bar2 bazar)" sorry


254 
next


255 
case (Bazar foo)


256 
note `P foo`


257 
show "R (Bazar foo)" sorry


258 
qed


259 


260 
text {*


261 
This can be combined with the previous techniques for compound


262 
statements, e.g.\ like this.


263 
*}


264 


265 
lemma


266 
fixes x :: 'a and y :: 'b and z :: 'c


267 
and foo :: foo


268 
and bar :: bar


269 
and bazar :: bazar


270 
shows


271 
"A x foo \<Longrightarrow> P x foo"


272 
and


273 
"B1 y bar \<Longrightarrow> Q1 y bar"


274 
"B2 y bar \<Longrightarrow> Q2 y bar"


275 
and


276 
"C1 z bazar \<Longrightarrow> R1 z bazar"


277 
"C2 z bazar \<Longrightarrow> R2 z bazar"


278 
"C3 z bazar \<Longrightarrow> R3 z bazar"


279 
proof (induct foo and bar and bazar arbitrary: x and y and z)


280 
oops


281 


282 


283 
subsection {* Inductive predicates *}


284 


285 
text {*


286 
The most basic form of induction involving predicates (or sets)


287 
essentially eliminates a given membership fact.


288 
*}


289 


290 
inductive Even :: "nat \<Rightarrow> bool" where


291 
zero: "Even 0"


292 
 double: "Even n \<Longrightarrow> Even (2 * n)"


293 


294 
lemma


295 
assumes "Even n"


296 
shows "P n"


297 
using assms


298 
proof induct


299 
case zero


300 
show "P 0" sorry


301 
next


302 
case (double n)


303 
note `Even n` and `P n`


304 
show "P (2 * n)" sorry


305 
qed


306 


307 
text {*


308 
Alternatively, an initial rule statement may be proven as follows,


309 
performing ``insitu'' elimination with explicit rule specification.


310 
*}


311 


312 
lemma "Even n \<Longrightarrow> P n"


313 
proof (induct rule: Even.induct)


314 
oops


315 


316 
text {*


317 
Simultaneous goals do not introduce anything new.


318 
*}


319 


320 
lemma


321 
assumes "Even n"


322 
shows "P1 n" and "P2 n"


323 
using assms


324 
proof induct


325 
case zero


326 
{


327 
case 1


328 
show "P1 0" sorry


329 
next


330 
case 2


331 
show "P2 0" sorry


332 
}


333 
next


334 
case (double n)


335 
note `Even n` and `P1 n` and `P2 n`


336 
{


337 
case 1


338 
show "P1 (2 * n)" sorry


339 
next


340 
case 2


341 
show "P2 (2 * n)" sorry


342 
}


343 
qed


344 


345 
text {*


346 
Working with mutual rules requires special care in composing the


347 
statement as a twolevel conjunction, using lists of propositions


348 
separated by @{text "and"}. For example:


349 
*}


350 


351 
inductive Evn :: "nat \<Rightarrow> bool" and Odd :: "nat \<Rightarrow> bool"


352 
where


353 
zero: "Evn 0"


354 
 succ_Evn: "Evn n \<Longrightarrow> Odd (Suc n)"


355 
 succ_Odd: "Odd n \<Longrightarrow> Evn (Suc n)"


356 


357 
lemma "Evn n \<Longrightarrow> P n"


358 
and "Odd n \<Longrightarrow> Q n"


359 
proof (induct rule: Evn_Odd.inducts)


360 
case zero


361 
show "P 0" sorry


362 
next


363 
case (succ_Evn n)


364 
note `Evn n` and `P n`


365 
show "Q (Suc n)" sorry


366 
next


367 
case (succ_Odd n)


368 
note `Odd n` and `Q n`


369 
show "P (Suc n)" sorry


370 
qed


371 


372 
end 