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

src/Doc/Prog_Prove/Types_and_funs.thy

author | wenzelm |

Fri Jan 12 14:08:53 2018 +0100 (2018-01-12) | |

changeset 67406 | 23307fd33906 |

parent 64862 | 2baa926a958d |

child 67613 | ce654b0e6d69 |

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

isabelle update_cartouches -c;

1 (*<*)

2 theory Types_and_funs

3 imports Main

4 begin

5 (*>*)

6 text\<open>

7 \vspace{-5ex}

8 \section{Type and Function Definitions}

10 Type synonyms are abbreviations for existing types, for example

11 \index{string@@{text string}}\<close>

13 type_synonym string = "char list"

15 text\<open>

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 \<close>

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

61 text\<open>with a mirror function:\<close>

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\<open>The following lemma illustrates induction:\<close>

69 lemma "mirror(mirror t) = t"

70 apply(induction t)

72 txt\<open>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 \<close>

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\<open>

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}}\<close>

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

107 "sq n = n * n"

109 text\<open>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}}\<close>

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

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

120 text\<open>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 \<close>

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\<open>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 \<close>

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

176 apply(induction n rule: div2.induct)

178 txt\<open>(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 "sum_tree ::"} @{typ "nat tree \<Rightarrow> nat"}

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

223 and prove @{prop "sum_tree t = sum_list(contents t)"}

224 (where @{const sum_list} is predefined).

225 \end{exercise}

227 \begin{exercise}

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

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

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

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

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

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

234 \end{exercise}

236 \begin{exercise}

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

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

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

240 \end{exercise}

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

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

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

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

248 \begin{quote}

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

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

251 \end{quote}

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

253 \emph{generalize the goal before induction}.

254 The reason is simple: if the goal is

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

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

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

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

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

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

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

263 \<close>

264 (*<*)

265 apply auto

266 done

267 (*>*)

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

269 "itrev [] ys = ys" |

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

272 text\<open>The behaviour of @{const itrev} is simple: it reverses

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

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

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

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

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

279 its first argument provided the second one is empty:

280 \<close>

282 lemma "itrev xs [] = rev xs"

284 txt\<open>There is no choice as to the induction variable:

285 \<close>

287 apply(induction xs)

288 apply(auto)

290 txt\<open>

291 Unfortunately, this attempt does not prove

292 the induction step:

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

294 The induction hypothesis is too weak. The fixed

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

296 This example suggests a heuristic:

297 \begin{quote}

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

299 \end{quote}

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

301 just not true. The correct generalization is

302 \<close>

303 (*<*)oops(*>*)

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

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

306 txt\<open>

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

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

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

310 Other situations can require a good deal of creativity.

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

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

314 not there:

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

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

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

318 in the induction hypothesis is fixed,

319 but the induction hypothesis needs to be applied with

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

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

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

323 \<close>

324 (*<*)oops

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

326 (*>*)

327 apply(induction xs arbitrary: ys)

329 txt\<open>The induction hypothesis in the induction step is now universally quantified over @{text ys}:

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

331 Thus the proof succeeds:

332 \<close>

334 apply auto

335 done

337 text\<open>

338 This leads to another heuristic for generalization:

339 \begin{quote}

340 \emph{Generalize induction by generalizing all free

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

342 \end{quote}

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

344 This heuristic prevents trivial failures like the one above.

345 However, it should not be applied blindly.

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

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

348 those that change in recursive calls.

351 \subsection*{Exercises}

353 \begin{exercise}

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

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

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

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

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

359 \end{exercise}

362 \section{Simplification}

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

365 \conceptidx{Simplification}{simplification} means

366 \begin{itemize}

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

368 \item as long as possible.

369 \end{itemize}

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

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

372 Logically, they are still symmetric, but proofs by

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

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

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

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

378 simplification rules

379 \[

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

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

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

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

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

385 \end{array}

386 \]

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

388 as follows:

389 \[

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

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

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

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

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

395 & @{const True}

396 \end{array}

397 \]

398 Simplification is often also called \concept{rewriting}

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

401 \subsection{Simplification Rules}

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

404 which the simplifier will use automatically. In addition,

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

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

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

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

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

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

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

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

414 rules. Equations that may be counterproductive as simplification rules

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

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

417 and can produce an exponential blow-up.

419 \subsection{Conditional Simplification Rules}

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

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

423 simplification. For example, given the simplification rules

424 \begin{quote}

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

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

427 \end{quote}

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

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

430 is not provable.

432 \subsection{Termination}

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

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

436 responsibility not to include simplification rules that can lead to

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

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

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

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

441 and Isabelle makes little attempt to detect nontermination.

443 When conditional simplification rules are applied, their preconditions are

444 proved first. Hence all preconditions need to be

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

446 \begin{quote}

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

448 \end{quote}

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

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

451 \begin{quote}

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

453 \end{quote}

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

455 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}.

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

458 \label{sec:simp}

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

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

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

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

464 Given a goal

465 \begin{quote}

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

467 \end{quote}

468 the command

469 \begin{quote}

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

471 \end{quote}

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

473 \begin{itemize}

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

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

476 \item the assumptions.

477 \end{itemize}

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

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

480 can be modified similarly:

481 \begin{quote}

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

483 \end{quote}

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

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

486 does not just perform simplification.

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

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

490 all subgoals.

492 \subsection{Rewriting with Definitions}

493 \label{sec:rewr-defs}

495 Definitions introduced by the command \isacom{definition}

496 can also be used as simplification rules,

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

498 automatically. Definitions are intended for introducing abstract concepts and

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

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

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

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

503 properties will be affected.

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

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

507 \begin{quote}

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

509 \end{quote}

510 In particular, let-expressions can be unfolded by

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

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

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

516 @{text simp} using the rule

517 \begin{quote}

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

519 \end{quote}

520 For example, @{text simp} can prove

521 \begin{quote}

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

523 \end{quote}

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

525 simplify to @{const True}.

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

528 @{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)))"}

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

530 can be instructed to do so:

531 \begin{quote}

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

533 \end{quote}

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

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

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

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

538 Splitting if or case-expressions in the assumptions requires

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

542 \subsection*{Exercises}

544 \exercise\label{exe:tree0}

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

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

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

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

549 Consider the following recursive function:

550 \<close>

551 (*<*)

552 datatype tree0 = Tip | Node tree0 tree0

553 (*>*)

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

555 "explode 0 t = t" |

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

558 text \<open>

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

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

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

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

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

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

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

567 \endexercise

569 \exercise

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

571 as a data type:

572 \<close>

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

576 text\<open>

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

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

579 @{text x}.

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

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

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

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

585 that evaluates a polynomial at the given value.

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

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

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

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

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

591 \endexercise

592 \<close>

593 (*<*)

594 end

595 (*>*)