author  wenzelm 
Tue, 31 Mar 2015 22:31:05 +0200  
changeset 59886  e0dc738eb08c 
parent 58860  fee7cfa69c50 
child 64862  2baa926a958d 
permissions  rwrr 
47269  1 
(*<*) 
2 
theory Types_and_funs 

3 
imports Main 

4 
begin 

5 
(*>*) 

6 
text{* 

7 
\vspace{5ex} 

52361  8 
\section{Type and Function Definitions} 
47269  9 

10 
Type synonyms are abbreviations for existing types, for example 

58521  11 
\index{string@@{text string}}*} 
47269  12 

13 
type_synonym string = "char list" 

14 

58521  15 
text{* 
47269  16 
Type synonyms are expanded after parsing and are not present in internal representation and output. They are mere conveniences for the reader. 
17 

18 
\subsection{Datatypes} 

51465  19 
\label{sec:datatypes} 
47269  20 

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

22 
\begin{quote} 

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

55348  24 
\indexed{\isacom{datatype}}{datatype} @{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"} 
47269  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 \ 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

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 
47269  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 

55348  42 
the \concept{structural induction}\index{induction} rule: to show 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

43 
$P~x$ for all $x$ of type @{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"}, 
47269  44 
one needs to show $P(C_i\ x_1 \dots x_{n_i})$ (for each $i$) assuming 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

45 
$P(x_j)$ for all $j$ where $\tau_{i,j} =$~@{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"}. 
47269  46 
Distinctness and injectivity are applied automatically by @{text auto} 
47 
and other proof methods. Induction must be applied explicitly. 

48 

58605  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 

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

53 
\end{quote} 

58605  54 
Case expressions must be enclosed in parentheses. 
47269  55 

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

47306  59 
datatype 'a tree = Tip  Node "'a tree" 'a "'a tree" 
47269  60 

61 
text{* with a mirror function: *} 

62 

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)" 

66 

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

68 

69 
lemma "mirror(mirror t) = t" 

70 
apply(induction t) 

71 

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. 

76 

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

55348  78 
@{datatype[display] option}\index{option@@{text option}}\index{None@@{const None}}\index{Some@@{const Some}} 
47269  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 keyvalue 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 

47306  90 
"lookup [] x = None"  
91 
"lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)" 

47269  92 

93 
text{* 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

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"}. 
51393  95 
Pairs can be taken apart either by pattern matching (as above) or with the 
57804  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 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

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

101 
\subsection{Definitions} 

102 

56989  103 
Nonrecursive functions can be defined as in the following example: 
55348  104 
\index{definition@\isacom{definition}}*} 
47269  105 

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

107 
"sq n = n * n" 

108 

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

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

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

112 
\subsection{Abbreviations} 

113 

114 
Abbreviations are similar to definitions: 

55348  115 
\index{abbreviation@\isacom{abbreviation}}*} 
47269  116 

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

52045  118 
"sq' n \<equiv> n * n" 
47269  119 

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

58521  121 
after parsing, @{term"sq' t"} is replaced by \mbox{@{term"t*t"}}; 
52045  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 

47269  125 
advantage of abbreviations over definitions: definitions need to be expanded 
52045  126 
explicitly (\autoref{sec:rewrdefs}) whereas abbreviations are already 
47269  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. 

130 

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

52361  133 
\subsection{Recursive Functions} 
47269  134 
\label{sec:recursivefuns} 
135 

55348  136 
Recursive functions are defined with \indexed{\isacom{fun}}{fun} by pattern matching 
56989  137 
over datatype constructors. The order of equations matters, as in 
47269  138 
functional programming languages. However, all HOL functions must be 
58602  139 
total. This simplifies the logic  terms are always defined  but means 
47269  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. 

143 

47711  144 
Isabelle's automatic termination checker requires that the arguments of 
47269  145 
recursive calls on the righthand side must be strictly smaller than the 
146 
arguments on the lefthand side. In the simplest case, this means that one 

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

58504  148 
is measured as the number of constructors (excluding 0ary ones, e.g., @{text 
47711  149 
Nil}). Lexicographic combinations are also recognized. In more complicated 
47269  150 
situations, the user may have to prove termination by hand. For details 
58620  151 
see~@{cite Krauss}. 
47269  152 

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 
*} 

157 

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

159 
"div2 0 = 0"  

54136  160 
"div2 (Suc 0) = 0"  
47269  161 
"div2 (Suc(Suc n)) = Suc(div2 n)" 
162 

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

47711  164 
customized induction rule: 
47269  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 
\] 

47711  172 
This customized induction rule can simplify inductive proofs. For example, 
47269  173 
*} 
174 

54571  175 
lemma "div2(n) = n div 2" 
47269  176 
apply(induction n rule: div2.induct) 
177 

54571  178 
txt{* (where the infix @{text div} is the predefined division operation) 
56989  179 
yields the subgoals 
47269  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 

47711  184 
case analysis in the induction step. 
47269  185 

54571  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, 

55348  191 
then properties of @{text f} are best proved via @{text "f.induct"}.\index{inductionrule@@{text".induct"}}} 
54571  192 
\end{quote} 
193 

47269  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} 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

198 
@{text "f(e) = \<dots> f(r\<^sub>1) \<dots> f(r\<^sub>k) \<dots>"} 
47269  199 
\end{quote} 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

200 
where @{text"f(r\<^sub>i)"}, @{text"i=1\<dots>k"}, are all the recursive calls, 
47269  201 
the induction rule @{text"f.induct"} contains one premise of the form 
202 
\begin{quote} 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

203 
@{text"P(r\<^sub>1) \<Longrightarrow> \<dots> \<Longrightarrow> P(r\<^sub>k) \<Longrightarrow> P(e)"} 
47269  204 
\end{quote} 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

205 
If @{text "f :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<tau>\<^sub>n \<Rightarrow> \<tau>"} then @{text"f.induct"} is applied like this: 
47269  206 
\begin{quote} 
55348  207 
\isacom{apply}@{text"(induction x\<^sub>1 \<dots> x\<^sub>n rule: f.induct)"}\index{inductionrule@@{text"induction ... rule:"}} 
47269  208 
\end{quote} 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

209 
where typically there is a call @{text"f x\<^sub>1 \<dots> x\<^sub>n"} in the goal. 
47269  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}. 

212 

54136  213 

54436  214 
\subsection*{Exercises} 
54136  215 

216 
\begin{exercise} 

54194  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} 

225 

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} 

234 

235 
\begin{exercise} 

54571  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)"}. 

54136  239 
\end{exercise} 
240 

241 

55348  242 
\section{Induction Heuristics}\index{induction heuristics} 
47269  243 

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 

58502  252 
\emph{generalize the goal before induction}. 
47269  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. 

256 

257 
Function @{const rev} has quadratic worstcase 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 

47711  268 
"itrev [] ys = ys"  
47269  269 
"itrev (x#xs) ys = itrev xs (x#ys)" 
270 

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

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

47711  273 
and it returns that second argument when the first one becomes 
47269  274 
empty. Note that @{const itrev} is tailrecursive: it can be 
56989  275 
compiled into a loop; no stack is necessary for executing it. 
47269  276 

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

278 
its first argument provided the second one is empty: 

279 
*} 

280 

281 
lemma "itrev xs [] = rev xs" 

282 

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

284 
*} 

285 

286 
apply(induction xs) 

287 
apply(auto) 

288 

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} 

58502  297 
\emph{Generalize goals for induction by replacing constants by variables.} 
47269  298 
\end{quote} 
58519  299 
Of course one cannot do this naively: @{prop"itrev xs ys = rev xs"} is 
58502  300 
just not true. The correct generalization is 
58860  301 
*} 
302 
(*<*)oops(*>*) 

47269  303 
lemma "itrev xs ys = rev xs @ ys" 
304 
(*<*)apply(induction xs, auto)(*>*) 

305 
txt{* 

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

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

58502  308 
In this instance it was easy to guess the right generalization. 
47269  309 
Other situations can require a good deal of creativity. 
310 

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 

58502  316 
intuition to generalize: the problem is that the @{text ys} 
47269  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 

58502  321 
to perform this generalization for us by adding @{text "arbitrary: ys"}\index{arbitrary@@{text"arbitrary:"}}. 
47269  322 
*} 
323 
(*<*)oops 

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

325 
(*>*) 

326 
apply(induction xs arbitrary: ys) 

327 

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 
*} 

332 

333 
apply auto 

334 
done 

335 

336 
text{* 

58502  337 
This leads to another heuristic for generalization: 
47269  338 
\begin{quote} 
58502  339 
\emph{Generalize induction by generalizing all free 
47269  340 
variables\\ {\em(except the induction variable itself)}.} 
341 
\end{quote} 

58502  342 
Generalization is best performed with @{text"arbitrary: y\<^sub>1 \<dots> y\<^sub>k"}. 
47269  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. 

348 

54136  349 

54436  350 
\subsection*{Exercises} 
54136  351 

352 
\begin{exercise} 

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

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

355 
Tailrecursive 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} 

359 

360 

47269  361 
\section{Simplification} 
362 

55317  363 
So far we have talked a lot about simplifying terms without explaining the concept. 
364 
\conceptidx{Simplification}{simplification} means 

47269  365 
\begin{itemize} 
366 
\item using equations $l = r$ from left to right (only), 

367 
\item as long as possible. 

368 
\end{itemize} 

47711  369 
To emphasize the directionality, equations that have been given the 
55317  370 
@{text"simp"} attribute are called \conceptidx{simplification rules}{simplification rule}. 
371 
Logically, they are still symmetric, but proofs by 

47269  372 
simplification use them only in the lefttoright 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. 

375 

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)}{=} \\ 

57817  392 
@{text"(Suc 0"} & \leq & @{text"Suc (0 + x))"} & \stackrel{(3)}{=} \\ 
47269  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} 

55317  398 
and simplification rules \conceptidx{rewrite rules}{rewrite rule}. 
47269  399 

52361  400 
\subsection{Simplification Rules} 
47269  401 

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

410 

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 

58521  414 
should only be used in specific proof steps (see \autoref{sec:simp} below). 
47269  415 
Distributivity laws, for example, alter the structure of terms 
416 
and can produce an exponential blowup. 

417 

52361  418 
\subsection{Conditional Simplification Rules} 
47269  419 

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. 

430 

431 
\subsection{Termination} 

432 

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 righthand side of a simplification rule should 

58602  438 
always be ``simpler'' than the lefthand side  in some sense. But since 
47269  439 
termination is undecidable, such a check cannot be automated completely 
440 
and Isabelle makes little attempt to detect nontermination. 

441 

442 
When conditional simplification rules are applied, their preconditions are 

443 
proved first. Hence all preconditions need to be 

444 
simpler than the lefthand 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}. 

455 

55348  456 
\subsection{The \indexed{@{text simp}}{simp} Proof Method} 
47269  457 
\label{sec:simp} 
458 

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} 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

465 
@{text"1. \<lbrakk> P\<^sub>1; \<dots>; P\<^sub>m \<rbrakk> \<Longrightarrow> C"} 
47269  466 
\end{quote} 
467 
the command 

468 
\begin{quote} 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

469 
\isacom{apply}@{text"(simp add: th\<^sub>1 \<dots> th\<^sub>n)"} 
47269  470 
\end{quote} 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

471 
simplifies the assumptions @{text "P\<^sub>i"} and the conclusion @{text C} using 
47269  472 
\begin{itemize} 
473 
\item all simplification rules, including the ones coming from \isacom{datatype} and \isacom{fun}, 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

474 
\item the additional lemmas @{text"th\<^sub>1 \<dots> th\<^sub>n"}, and 
47269  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. 

486 

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. 

490 

56989  491 
\subsection{Rewriting with Definitions} 
47269  492 
\label{sec:rewrdefs} 
493 

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. 

503 

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

58605  505 
and can be added to a call of @{text simp} like any other theorem: 
47269  506 
\begin{quote} 
507 
\isacom{apply}@{text"(simp add: f_def)"} 

508 
\end{quote} 

509 
In particular, letexpressions can be unfolded by 

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

511 

52361  512 
\subsection{Case Splitting With @{text simp}} 
47269  513 

514 
Goals containing ifexpressions 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}. 

525 

526 
We can split caseexpressions 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 caseexpressions over natural numbers. For an arbitrary 

55348  534 
datatype @{text t} it is @{text "t.split"}\index{split@@{text".split"}} instead of @{thm[source] nat.split}. 
47269  535 
Method @{text auto} can be modified in exactly the same way. 
55348  536 
The modifier \indexed{@{text "split:"}}{split} can be followed by multiple names. 
54605  537 
Splitting if or caseexpressions in the assumptions requires 
538 
@{text "split: if_splits"} or @{text "split: t.splits"}. 

52593  539 

540 

54436  541 
\subsection*{Exercises} 
52593  542 

54195  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. 

54467  546 
Define a function @{text "nodes :: tree0 \<Rightarrow> nat"} that counts the number of 
54195  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)" 

556 

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. 

56989  561 
You may use the usual arithmetic operators, including the exponentiation 
54195  562 
operator ``@{text"^"}''. For example, \noquotes{@{prop [source] "2 ^ 2 = 4"}}. 
563 

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 

567 

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

570 
as a data type: 

571 
*} 

572 

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

574 

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

579 

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

54467  589 
Hint: consider the hint in Exercise~\ref{exe:tree0}. 
52593  590 
\endexercise 
47269  591 
*} 
592 
(*<*) 

593 
end 

594 
(*>*) 