summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Doc/Prog_Prove/Types_and_funs.thy

author | wenzelm |

Tue Oct 07 22:35:11 2014 +0200 (2014-10-07) | |

changeset 58620 | 7435b6a3f72e |

parent 58605 | 9d5013661ac6 |

child 58860 | fee7cfa69c50 |

permissions | -rw-r--r-- |

more antiquotations;

1 (*<*)

2 theory Types_and_funs

3 imports Main

4 begin

5 (*>*)

6 text{*

7 \vspace{-5ex}

8 \section{Type and Function Definitions}

10 Type synonyms are abbreviations for existing types, for example

11 \index{string@@{text string}}*}

13 type_synonym string = "char list"

15 text{*

16 Type synonyms are expanded after parsing and are not present in internal representation and output. They are mere conveniences for the reader.

18 \subsection{Datatypes}

19 \label{sec:datatypes}

21 The general form of a datatype definition looks like this:

22 \begin{quote}

23 \begin{tabular}{@ {}rclcll}

24 \indexed{\isacom{datatype}}{datatype} @{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"}

25 & = & $C_1 \ @{text"\""}\tau_{1,1}@{text"\""} \dots @{text"\""}\tau_{1,n_1}@{text"\""}$ \\

26 & $|$ & \dots \\

27 & $|$ & $C_k \ @{text"\""}\tau_{k,1}@{text"\""} \dots @{text"\""}\tau_{k,n_k}@{text"\""}$

28 \end{tabular}

29 \end{quote}

30 It introduces the constructors \

31 $C_i :: \tau_{i,1}\Rightarrow \cdots \Rightarrow \tau_{i,n_i} \Rightarrow$~@{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"} \ and expresses that any value of this type is built from these constructors in a unique manner. Uniqueness is implied by the following

32 properties of the constructors:

33 \begin{itemize}

34 \item \emph{Distinctness:} $C_i\ \ldots \neq C_j\ \dots$ \quad if $i \neq j$

35 \item \emph{Injectivity:}

36 \begin{tabular}[t]{l}

37 $(C_i \ x_1 \dots x_{n_i} = C_i \ y_1 \dots y_{n_i}) =$\\

38 $(x_1 = y_1 \land \dots \land x_{n_i} = y_{n_i})$

39 \end{tabular}

40 \end{itemize}

41 The fact that any value of the datatype is built from the constructors implies

42 the \concept{structural induction}\index{induction} rule: to show

43 $P~x$ for all $x$ of type @{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"},

44 one needs to show $P(C_i\ x_1 \dots x_{n_i})$ (for each $i$) assuming

45 $P(x_j)$ for all $j$ where $\tau_{i,j} =$~@{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"}.

46 Distinctness and injectivity are applied automatically by @{text auto}

47 and other proof methods. Induction must be applied explicitly.

49 Like in functional programming languages, datatype values can be taken apart

50 with case expressions\index{case expression}\index{case expression@@{text "case ... of"}}, for example

51 \begin{quote}

52 \noquotes{@{term[source] "(case xs of [] \<Rightarrow> 0 | x # _ \<Rightarrow> Suc x)"}}

53 \end{quote}

54 Case expressions must be enclosed in parentheses.

56 As an example of a datatype beyond @{typ nat} and @{text list}, consider binary trees:

57 *}

59 datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"

61 text{* with a mirror function: *}

63 fun mirror :: "'a tree \<Rightarrow> 'a tree" where

64 "mirror Tip = Tip" |

65 "mirror (Node l a r) = Node (mirror r) a (mirror l)"

67 text{* The following lemma illustrates induction: *}

69 lemma "mirror(mirror t) = t"

70 apply(induction t)

72 txt{* yields

73 @{subgoals[display]}

74 The induction step contains two induction hypotheses, one for each subtree.

75 An application of @{text auto} finishes the proof.

77 A very simple but also very useful datatype is the predefined

78 @{datatype[display] option}\index{option@@{text option}}\index{None@@{const None}}\index{Some@@{const Some}}

79 Its sole purpose is to add a new element @{const None} to an existing

80 type @{typ 'a}. To make sure that @{const None} is distinct from all the

81 elements of @{typ 'a}, you wrap them up in @{const Some} and call

82 the new type @{typ"'a option"}. A typical application is a lookup function

83 on a list of key-value pairs, often called an association list:

84 *}

85 (*<*)

86 apply auto

87 done

88 (*>*)

89 fun lookup :: "('a * 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" where

90 "lookup [] x = None" |

91 "lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"

93 text{*

94 Note that @{text"\<tau>\<^sub>1 * \<tau>\<^sub>2"} is the type of pairs, also written @{text"\<tau>\<^sub>1 \<times> \<tau>\<^sub>2"}.

95 Pairs can be taken apart either by pattern matching (as above) or with the

96 projection functions @{const fst} and @{const snd}: @{thm fst_conv[of x y]} and @{thm snd_conv[of x y]}.

97 Tuples are simulated by pairs nested to the right: @{term"(a,b,c)"}

98 is short for @{text"(a, (b, c))"} and @{text "\<tau>\<^sub>1 \<times> \<tau>\<^sub>2 \<times> \<tau>\<^sub>3"} is short for

99 @{text "\<tau>\<^sub>1 \<times> (\<tau>\<^sub>2 \<times> \<tau>\<^sub>3)"}.

101 \subsection{Definitions}

103 Non-recursive functions can be defined as in the following example:

104 \index{definition@\isacom{definition}}*}

106 definition sq :: "nat \<Rightarrow> nat" where

107 "sq n = n * n"

109 text{* Such definitions do not allow pattern matching but only

110 @{text"f x\<^sub>1 \<dots> x\<^sub>n = t"}, where @{text f} does not occur in @{text t}.

112 \subsection{Abbreviations}

114 Abbreviations are similar to definitions:

115 \index{abbreviation@\isacom{abbreviation}}*}

117 abbreviation sq' :: "nat \<Rightarrow> nat" where

118 "sq' n \<equiv> n * n"

120 text{* The key difference is that @{const sq'} is only syntactic sugar:

121 after parsing, @{term"sq' t"} is replaced by \mbox{@{term"t*t"}};

122 before printing, every occurrence of @{term"u*u"} is replaced by

123 \mbox{@{term"sq' u"}}. Internally, @{const sq'} does not exist.

124 This is the

125 advantage of abbreviations over definitions: definitions need to be expanded

126 explicitly (\autoref{sec:rewr-defs}) whereas abbreviations are already

127 expanded upon parsing. However, abbreviations should be introduced sparingly:

128 if abused, they can lead to a confusing discrepancy between the internal and

129 external view of a term.

131 The ASCII representation of @{text"\<equiv>"} is \texttt{==} or \xsymbol{equiv}.

133 \subsection{Recursive Functions}

134 \label{sec:recursive-funs}

136 Recursive functions are defined with \indexed{\isacom{fun}}{fun} by pattern matching

137 over datatype constructors. The order of equations matters, as in

138 functional programming languages. However, all HOL functions must be

139 total. This simplifies the logic --- terms are always defined --- but means

140 that recursive functions must terminate. Otherwise one could define a

141 function @{prop"f n = f n + (1::nat)"} and conclude \mbox{@{prop"(0::nat) = 1"}} by

142 subtracting @{term"f n"} on both sides.

144 Isabelle's automatic termination checker requires that the arguments of

145 recursive calls on the right-hand side must be strictly smaller than the

146 arguments on the left-hand side. In the simplest case, this means that one

147 fixed argument position decreases in size with each recursive call. The size

148 is measured as the number of constructors (excluding 0-ary ones, e.g., @{text

149 Nil}). Lexicographic combinations are also recognized. In more complicated

150 situations, the user may have to prove termination by hand. For details

151 see~@{cite Krauss}.

153 Functions defined with \isacom{fun} come with their own induction schema

154 that mirrors the recursion schema and is derived from the termination

155 order. For example,

156 *}

158 fun div2 :: "nat \<Rightarrow> nat" where

159 "div2 0 = 0" |

160 "div2 (Suc 0) = 0" |

161 "div2 (Suc(Suc n)) = Suc(div2 n)"

163 text{* does not just define @{const div2} but also proves a

164 customized induction rule:

165 \[

166 \inferrule{

167 \mbox{@{thm (prem 1) div2.induct}}\\

168 \mbox{@{thm (prem 2) div2.induct}}\\

169 \mbox{@{thm (prem 3) div2.induct}}}

170 {\mbox{@{thm (concl) div2.induct[of _ "m"]}}}

171 \]

172 This customized induction rule can simplify inductive proofs. For example,

173 *}

175 lemma "div2(n) = n div 2"

176 apply(induction n rule: div2.induct)

178 txt{* (where the infix @{text div} is the predefined division operation)

179 yields the subgoals

180 @{subgoals[display,margin=65]}

181 An application of @{text auto} finishes the proof.

182 Had we used ordinary structural induction on @{text n},

183 the proof would have needed an additional

184 case analysis in the induction step.

186 This example leads to the following induction heuristic:

187 \begin{quote}

188 \emph{Let @{text f} be a recursive function.

189 If the definition of @{text f} is more complicated

190 than having one equation for each constructor of some datatype,

191 then properties of @{text f} are best proved via @{text "f.induct"}.\index{inductionrule@@{text".induct"}}}

192 \end{quote}

194 The general case is often called \concept{computation induction},

195 because the induction follows the (terminating!) computation.

196 For every defining equation

197 \begin{quote}

198 @{text "f(e) = \<dots> f(r\<^sub>1) \<dots> f(r\<^sub>k) \<dots>"}

199 \end{quote}

200 where @{text"f(r\<^sub>i)"}, @{text"i=1\<dots>k"}, are all the recursive calls,

201 the induction rule @{text"f.induct"} contains one premise of the form

202 \begin{quote}

203 @{text"P(r\<^sub>1) \<Longrightarrow> \<dots> \<Longrightarrow> P(r\<^sub>k) \<Longrightarrow> P(e)"}

204 \end{quote}

205 If @{text "f :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<tau>\<^sub>n \<Rightarrow> \<tau>"} then @{text"f.induct"} is applied like this:

206 \begin{quote}

207 \isacom{apply}@{text"(induction x\<^sub>1 \<dots> x\<^sub>n rule: f.induct)"}\index{inductionrule@@{text"induction ... rule:"}}

208 \end{quote}

209 where typically there is a call @{text"f x\<^sub>1 \<dots> x\<^sub>n"} in the goal.

210 But note that the induction rule does not mention @{text f} at all,

211 except in its name, and is applicable independently of @{text f}.

214 \subsection*{Exercises}

216 \begin{exercise}

217 Starting from the type @{text "'a tree"} defined in the text, define

218 a function @{text "contents ::"} @{typ "'a tree \<Rightarrow> 'a list"}

219 that collects all values in a tree in a list, in any order,

220 without removing duplicates.

221 Then define a function @{text "treesum ::"} @{typ "nat tree \<Rightarrow> nat"}

222 that sums up all values in a tree of natural numbers

223 and prove @{prop "treesum t = listsum(contents t)"}.

224 \end{exercise}

226 \begin{exercise}

227 Define a new type @{text "'a tree2"} of binary trees where values are also

228 stored in the leaves of the tree. Also reformulate the

229 @{const mirror} function accordingly. Define two functions

230 @{text "pre_order"} and @{text "post_order"} of type @{text "'a tree2 \<Rightarrow> 'a list"}

231 that traverse a tree and collect all stored values in the respective order in

232 a list. Prove @{prop "pre_order (mirror t) = rev (post_order t)"}.

233 \end{exercise}

235 \begin{exercise}

236 Define a function @{text "intersperse ::"} @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"}

237 such that @{text "intersperse a [x\<^sub>1, ..., x\<^sub>n] = [x\<^sub>1, a, x\<^sub>2, a, ..., a, x\<^sub>n]"}.

238 Now prove that @{prop "map f (intersperse a xs) = intersperse (f a) (map f xs)"}.

239 \end{exercise}

242 \section{Induction Heuristics}\index{induction heuristics}

244 We have already noted that theorems about recursive functions are proved by

245 induction. In case the function has more than one argument, we have followed

246 the following heuristic in the proofs about the append function:

247 \begin{quote}

248 \emph{Perform induction on argument number $i$\\

249 if the function is defined by recursion on argument number $i$.}

250 \end{quote}

251 The key heuristic, and the main point of this section, is to

252 \emph{generalize the goal before induction}.

253 The reason is simple: if the goal is

254 too specific, the induction hypothesis is too weak to allow the induction

255 step to go through. Let us illustrate the idea with an example.

257 Function @{const rev} has quadratic worst-case running time

258 because it calls append for each element of the list and

259 append is linear in its first argument. A linear time version of

260 @{const rev} requires an extra argument where the result is accumulated

261 gradually, using only~@{text"#"}:

262 *}

263 (*<*)

264 apply auto

265 done

266 (*>*)

267 fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where

268 "itrev [] ys = ys" |

269 "itrev (x#xs) ys = itrev xs (x#ys)"

271 text{* The behaviour of @{const itrev} is simple: it reverses

272 its first argument by stacking its elements onto the second argument,

273 and it returns that second argument when the first one becomes

274 empty. Note that @{const itrev} is tail-recursive: it can be

275 compiled into a loop; no stack is necessary for executing it.

277 Naturally, we would like to show that @{const itrev} does indeed reverse

278 its first argument provided the second one is empty:

279 *}

281 lemma "itrev xs [] = rev xs"

283 txt{* There is no choice as to the induction variable:

284 *}

286 apply(induction xs)

287 apply(auto)

289 txt{*

290 Unfortunately, this attempt does not prove

291 the induction step:

292 @{subgoals[display,margin=70]}

293 The induction hypothesis is too weak. The fixed

294 argument,~@{term"[]"}, prevents it from rewriting the conclusion.

295 This example suggests a heuristic:

296 \begin{quote}

297 \emph{Generalize goals for induction by replacing constants by variables.}

298 \end{quote}

299 Of course one cannot do this naively: @{prop"itrev xs ys = rev xs"} is

300 just not true. The correct generalization is

301 *};

302 (*<*)oops;(*>*)

303 lemma "itrev xs ys = rev xs @ ys"

304 (*<*)apply(induction xs, auto)(*>*)

305 txt{*

306 If @{text ys} is replaced by @{term"[]"}, the right-hand side simplifies to

307 @{term"rev xs"}, as required.

308 In this instance it was easy to guess the right generalization.

309 Other situations can require a good deal of creativity.

311 Although we now have two variables, only @{text xs} is suitable for

312 induction, and we repeat our proof attempt. Unfortunately, we are still

313 not there:

314 @{subgoals[display,margin=65]}

315 The induction hypothesis is still too weak, but this time it takes no

316 intuition to generalize: the problem is that the @{text ys}

317 in the induction hypothesis is fixed,

318 but the induction hypothesis needs to be applied with

319 @{term"a # ys"} instead of @{text ys}. Hence we prove the theorem

320 for all @{text ys} instead of a fixed one. We can instruct induction

321 to perform this generalization for us by adding @{text "arbitrary: ys"}\index{arbitrary@@{text"arbitrary:"}}.

322 *}

323 (*<*)oops

324 lemma "itrev xs ys = rev xs @ ys"

325 (*>*)

326 apply(induction xs arbitrary: ys)

328 txt{* The induction hypothesis in the induction step is now universally quantified over @{text ys}:

329 @{subgoals[display,margin=65]}

330 Thus the proof succeeds:

331 *}

333 apply auto

334 done

336 text{*

337 This leads to another heuristic for generalization:

338 \begin{quote}

339 \emph{Generalize induction by generalizing all free

340 variables\\ {\em(except the induction variable itself)}.}

341 \end{quote}

342 Generalization is best performed with @{text"arbitrary: y\<^sub>1 \<dots> y\<^sub>k"}.

343 This heuristic prevents trivial failures like the one above.

344 However, it should not be applied blindly.

345 It is not always required, and the additional quantifiers can complicate

346 matters in some cases. The variables that need to be quantified are typically

347 those that change in recursive calls.

350 \subsection*{Exercises}

352 \begin{exercise}

353 Write a tail-recursive variant of the @{text add} function on @{typ nat}:

354 @{term "itadd :: nat \<Rightarrow> nat \<Rightarrow> nat"}.

355 Tail-recursive means that in the recursive case, @{text itadd} needs to call

356 itself directly: \mbox{@{term"itadd (Suc m) n"}} @{text"= itadd \<dots>"}.

357 Prove @{prop "itadd m n = add m n"}.

358 \end{exercise}

361 \section{Simplification}

363 So far we have talked a lot about simplifying terms without explaining the concept.

364 \conceptidx{Simplification}{simplification} means

365 \begin{itemize}

366 \item using equations $l = r$ from left to right (only),

367 \item as long as possible.

368 \end{itemize}

369 To emphasize the directionality, equations that have been given the

370 @{text"simp"} attribute are called \conceptidx{simplification rules}{simplification rule}.

371 Logically, they are still symmetric, but proofs by

372 simplification use them only in the left-to-right direction. The proof tool

373 that performs simplifications is called the \concept{simplifier}. It is the

374 basis of @{text auto} and other related proof methods.

376 The idea of simplification is best explained by an example. Given the

377 simplification rules

378 \[

379 \begin{array}{rcl@ {\quad}l}

380 @{term"0 + n::nat"} &@{text"="}& @{text n} & (1) \\

381 @{term"(Suc m) + n"} &@{text"="}& @{term"Suc (m + n)"} & (2) \\

382 @{text"(Suc m \<le> Suc n)"} &@{text"="}& @{text"(m \<le> n)"} & (3)\\

383 @{text"(0 \<le> m)"} &@{text"="}& @{const True} & (4)

384 \end{array}

385 \]

386 the formula @{prop"0 + Suc 0 \<le> Suc 0 + x"} is simplified to @{const True}

387 as follows:

388 \[

389 \begin{array}{r@ {}c@ {}l@ {\quad}l}

390 @{text"(0 + Suc 0"} & \leq & @{text"Suc 0 + x)"} & \stackrel{(1)}{=} \\

391 @{text"(Suc 0"} & \leq & @{text"Suc 0 + x)"} & \stackrel{(2)}{=} \\

392 @{text"(Suc 0"} & \leq & @{text"Suc (0 + x))"} & \stackrel{(3)}{=} \\

393 @{text"(0"} & \leq & @{text"0 + x)"} & \stackrel{(4)}{=} \\[1ex]

394 & @{const True}

395 \end{array}

396 \]

397 Simplification is often also called \concept{rewriting}

398 and simplification rules \conceptidx{rewrite rules}{rewrite rule}.

400 \subsection{Simplification Rules}

402 The attribute @{text"simp"} declares theorems to be simplification rules,

403 which the simplifier will use automatically. In addition,

404 \isacom{datatype} and \isacom{fun} commands implicitly declare some

405 simplification rules: \isacom{datatype} the distinctness and injectivity

406 rules, \isacom{fun} the defining equations. Definitions are not declared

407 as simplification rules automatically! Nearly any theorem can become a

408 simplification rule. The simplifier will try to transform it into an

409 equation. For example, the theorem @{prop"\<not> P"} is turned into @{prop"P = False"}.

411 Only equations that really simplify, like @{prop"rev (rev xs) = xs"} and

412 @{prop"xs @ [] = xs"}, should be declared as simplification

413 rules. Equations that may be counterproductive as simplification rules

414 should only be used in specific proof steps (see \autoref{sec:simp} below).

415 Distributivity laws, for example, alter the structure of terms

416 and can produce an exponential blow-up.

418 \subsection{Conditional Simplification Rules}

420 Simplification rules can be conditional. Before applying such a rule, the

421 simplifier will first try to prove the preconditions, again by

422 simplification. For example, given the simplification rules

423 \begin{quote}

424 @{prop"p(0::nat) = True"}\\

425 @{prop"p(x) \<Longrightarrow> f(x) = g(x)"},

426 \end{quote}

427 the term @{term"f(0::nat)"} simplifies to @{term"g(0::nat)"}

428 but @{term"f(1::nat)"} does not simplify because @{prop"p(1::nat)"}

429 is not provable.

431 \subsection{Termination}

433 Simplification can run forever, for example if both @{prop"f x = g x"} and

434 @{prop"g(x) = f(x)"} are simplification rules. It is the user's

435 responsibility not to include simplification rules that can lead to

436 nontermination, either on their own or in combination with other

437 simplification rules. The right-hand side of a simplification rule should

438 always be ``simpler'' than the left-hand side --- in some sense. But since

439 termination is undecidable, such a check cannot be automated completely

440 and Isabelle makes little attempt to detect nontermination.

442 When conditional simplification rules are applied, their preconditions are

443 proved first. Hence all preconditions need to be

444 simpler than the left-hand side of the conclusion. For example

445 \begin{quote}

446 @{prop "n < m \<Longrightarrow> (n < Suc m) = True"}

447 \end{quote}

448 is suitable as a simplification rule: both @{prop"n<m"} and @{const True}

449 are simpler than \mbox{@{prop"n < Suc m"}}. But

450 \begin{quote}

451 @{prop "Suc n < m \<Longrightarrow> (n < m) = True"}

452 \end{quote}

453 leads to nontermination: when trying to rewrite @{prop"n<m"} to @{const True}

454 one first has to prove \mbox{@{prop"Suc n < m"}}, which can be rewritten to @{const True} provided @{prop"Suc(Suc n) < m"}, \emph{ad infinitum}.

456 \subsection{The \indexed{@{text simp}}{simp} Proof Method}

457 \label{sec:simp}

459 So far we have only used the proof method @{text auto}. Method @{text simp}

460 is the key component of @{text auto}, but @{text auto} can do much more. In

461 some cases, @{text auto} is overeager and modifies the proof state too much.

462 In such cases the more predictable @{text simp} method should be used.

463 Given a goal

464 \begin{quote}

465 @{text"1. \<lbrakk> P\<^sub>1; \<dots>; P\<^sub>m \<rbrakk> \<Longrightarrow> C"}

466 \end{quote}

467 the command

468 \begin{quote}

469 \isacom{apply}@{text"(simp add: th\<^sub>1 \<dots> th\<^sub>n)"}

470 \end{quote}

471 simplifies the assumptions @{text "P\<^sub>i"} and the conclusion @{text C} using

472 \begin{itemize}

473 \item all simplification rules, including the ones coming from \isacom{datatype} and \isacom{fun},

474 \item the additional lemmas @{text"th\<^sub>1 \<dots> th\<^sub>n"}, and

475 \item the assumptions.

476 \end{itemize}

477 In addition to or instead of @{text add} there is also @{text del} for removing

478 simplification rules temporarily. Both are optional. Method @{text auto}

479 can be modified similarly:

480 \begin{quote}

481 \isacom{apply}@{text"(auto simp add: \<dots> simp del: \<dots>)"}

482 \end{quote}

483 Here the modifiers are @{text"simp add"} and @{text"simp del"}

484 instead of just @{text add} and @{text del} because @{text auto}

485 does not just perform simplification.

487 Note that @{text simp} acts only on subgoal 1, @{text auto} acts on all

488 subgoals. There is also @{text simp_all}, which applies @{text simp} to

489 all subgoals.

491 \subsection{Rewriting with Definitions}

492 \label{sec:rewr-defs}

494 Definitions introduced by the command \isacom{definition}

495 can also be used as simplification rules,

496 but by default they are not: the simplifier does not expand them

497 automatically. Definitions are intended for introducing abstract concepts and

498 not merely as abbreviations. Of course, we need to expand the definition

499 initially, but once we have proved enough abstract properties of the new

500 constant, we can forget its original definition. This style makes proofs more

501 robust: if the definition has to be changed, only the proofs of the abstract

502 properties will be affected.

504 The definition of a function @{text f} is a theorem named @{text f_def}

505 and can be added to a call of @{text simp} like any other theorem:

506 \begin{quote}

507 \isacom{apply}@{text"(simp add: f_def)"}

508 \end{quote}

509 In particular, let-expressions can be unfolded by

510 making @{thm[source] Let_def} a simplification rule.

512 \subsection{Case Splitting With @{text simp}}

514 Goals containing if-expressions are automatically split into two cases by

515 @{text simp} using the rule

516 \begin{quote}

517 @{prop"P(if A then s else t) = ((A \<longrightarrow> P(s)) \<and> (~A \<longrightarrow> P(t)))"}

518 \end{quote}

519 For example, @{text simp} can prove

520 \begin{quote}

521 @{prop"(A \<and> B) = (if A then B else False)"}

522 \end{quote}

523 because both @{prop"A \<longrightarrow> (A & B) = B"} and @{prop"~A \<longrightarrow> (A & B) = False"}

524 simplify to @{const True}.

526 We can split case-expressions similarly. For @{text nat} the rule looks like this:

527 @{prop[display,margin=65,indent=4]"P(case e of 0 \<Rightarrow> a | Suc n \<Rightarrow> b n) = ((e = 0 \<longrightarrow> P a) & (ALL n. e = Suc n \<longrightarrow> P(b n)))"}

528 Case expressions are not split automatically by @{text simp}, but @{text simp}

529 can be instructed to do so:

530 \begin{quote}

531 \isacom{apply}@{text"(simp split: nat.split)"}

532 \end{quote}

533 splits all case-expressions over natural numbers. For an arbitrary

534 datatype @{text t} it is @{text "t.split"}\index{split@@{text".split"}} instead of @{thm[source] nat.split}.

535 Method @{text auto} can be modified in exactly the same way.

536 The modifier \indexed{@{text "split:"}}{split} can be followed by multiple names.

537 Splitting if or case-expressions in the assumptions requires

538 @{text "split: if_splits"} or @{text "split: t.splits"}.

541 \subsection*{Exercises}

543 \exercise\label{exe:tree0}

544 Define a datatype @{text tree0} of binary tree skeletons which do not store

545 any information, neither in the inner nodes nor in the leaves.

546 Define a function @{text "nodes :: tree0 \<Rightarrow> nat"} that counts the number of

547 all nodes (inner nodes and leaves) in such a tree.

548 Consider the following recursive function:

549 *}

550 (*<*)

551 datatype tree0 = Tip | Node tree0 tree0

552 (*>*)

553 fun explode :: "nat \<Rightarrow> tree0 \<Rightarrow> tree0" where

554 "explode 0 t = t" |

555 "explode (Suc n) t = explode n (Node t t)"

557 text {*

558 Find an equation expressing the size of a tree after exploding it

559 (\noquotes{@{term [source] "nodes (explode n t)"}}) as a function

560 of @{term "nodes t"} and @{text n}. Prove your equation.

561 You may use the usual arithmetic operators, including the exponentiation

562 operator ``@{text"^"}''. For example, \noquotes{@{prop [source] "2 ^ 2 = 4"}}.

564 Hint: simplifying with the list of theorems @{thm[source] algebra_simps}

565 takes care of common algebraic properties of the arithmetic operators.

566 \endexercise

568 \exercise

569 Define arithmetic expressions in one variable over integers (type @{typ int})

570 as a data type:

571 *}

573 datatype exp = Var | Const int | Add exp exp | Mult exp exp

575 text{*

576 Define a function \noquotes{@{term [source]"eval :: exp \<Rightarrow> int \<Rightarrow> int"}}

577 such that @{term"eval e x"} evaluates @{text e} at the value

578 @{text x}.

580 A polynomial can be represented as a list of coefficients, starting with

581 the constant. For example, @{term "[4, 2, -1, 3::int]"} represents the

582 polynomial $4 + 2x - x^2 + 3x^3$.

583 Define a function \noquotes{@{term [source] "evalp :: int list \<Rightarrow> int \<Rightarrow> int"}}

584 that evaluates a polynomial at the given value.

585 Define a function \noquotes{@{term[source] "coeffs :: exp \<Rightarrow> int list"}}

586 that transforms an expression into a polynomial. This may require auxiliary

587 functions. Prove that @{text coeffs} preserves the value of the expression:

588 \mbox{@{prop"evalp (coeffs e) x = eval e x"}.}

589 Hint: consider the hint in Exercise~\ref{exe:tree0}.

590 \endexercise

591 *}

592 (*<*)

593 end

594 (*>*)