47269

1 
(*<*)


2 
theory Types_and_funs


3 
imports Main


4 
begin


5 
(*>*)


6 
text{*


7 
\vspace{5ex}


8 
\section{Type and function definitions}


9 


10 
Type synonyms are abbreviations for existing types, for example


11 
*}


12 


13 
type_synonym string = "char list"


14 


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.


17 


18 
\subsection{Datatypes}


19 


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


21 
\begin{quote}


22 
\begin{tabular}{@ {}rclcll}


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


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


25 
& $$ & \dots \\


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


27 
\end{tabular}


28 
\end{quote}


29 
It introduces the constructors \


30 
$C_i :: \tau_{i,1}\Rightarrow \cdots \Rightarrow \tau_{i,n_i} \Rightarrow$~@{text "('a\<^isub>1,\<dots>,'a\<^isub>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


31 
properties of the constructors:


32 
\begin{itemize}


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


34 
\item \emph{Injectivity:}


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


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


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


38 
\end{tabular}


39 
\end{itemize}


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


41 
the structural induction rule: to show


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


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


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


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


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


47 


48 
Datatype values can be taken apart with caseexpressions, for example


49 
\begin{quote}


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


51 
\end{quote}


52 
just like in functional programming languages. Case expressions


53 
must be enclosed in parentheses.


54 


55 
As an example, consider binary trees:


56 
*}


57 

47306

58 
datatype 'a tree = Tip  Node "'a tree" 'a "'a tree"

47269

59 


60 
text{* with a mirror function: *}


61 


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


63 
"mirror Tip = Tip" 


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


65 


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


67 


68 
lemma "mirror(mirror t) = t"


69 
apply(induction t)


70 


71 
txt{* yields


72 
@{subgoals[display]}


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


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


75 


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


77 
@{datatype[display] option}


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


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


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


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


82 
on a list of keyvalue pairs, often called an association list:


83 
*}


84 
(*<*)


85 
apply auto


86 
done


87 
(*>*)


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

47306

89 
"lookup [] x = None" 


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

47269

91 


92 
text{*


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

51393

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


95 
projection functions @{const fst} and @{const snd}: @{thm fst_conv} and @{thm snd_conv}. Tuples are simulated by pairs nested to the right: @{term"(a,b,c)"}


96 
abbreviates @{text"(a, (b, c))"} and @{text "\<tau>\<^isub>1 \<times> \<tau>\<^isub>2 \<times> \<tau>\<^isub>3"} abbreviates


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

47269

98 


99 
\subsection{Definitions}


100 


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


102 
*}


103 


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


105 
"sq n = n * n"


106 


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


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


109 


110 
\subsection{Abbreviations}


111 


112 
Abbreviations are similar to definitions:


113 
*}


114 


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


116 
"sq' n == n * n"


117 


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


119 
@{term"sq' t"} is replaced by \mbox{@{term"t*t"}} after parsing, and every


120 
occurrence of a term @{term"u*u"} is replaced by \mbox{@{term"sq' u"}} before


121 
printing. Internally, @{const sq'} does not exist. This is also the


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


123 
explicitly (see \autoref{sec:rewrdefs}) whereas abbreviations are already


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


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


126 
external view of a term.


127 


128 
\subsection{Recursive functions}


129 
\label{sec:recursivefuns}


130 


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


132 
over datatype constructors. The order of equations matters. Just as in


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


134 
total. This simplifies the logicterms are always definedbut means


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


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


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


138 

47711

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

47269

140 
recursive calls on the righthand side must be strictly smaller than the


141 
arguments on the lefthand side. In the simplest case, this means that one


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


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

47711

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

47269

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


146 
see~\cite{Krauss}.


147 


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


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


150 
order. For example,


151 
*}


152 


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


154 
"div2 0 = 0" 


155 
"div2 (Suc 0) = Suc 0" 


156 
"div2 (Suc(Suc n)) = Suc(div2 n)"


157 


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

47711

159 
customized induction rule:

47269

160 
\[


161 
\inferrule{


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


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


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


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


166 
\]

47711

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

47269

168 
*}


169 


170 
lemma "div2(n+n) = n"


171 
apply(induction n rule: div2.induct)


172 


173 
txt{* yields the 3 subgoals


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


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


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


177 
the proof would have needed an additional

47711

178 
case analysis in the induction step.

47269

179 


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


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


182 
For every defining equation


183 
\begin{quote}


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


185 
\end{quote}


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


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


188 
\begin{quote}


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


190 
\end{quote}


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


192 
\begin{quote}


193 
\isacom{apply}@{text"(induction x\<^isub>1 \<dots> x\<^isub>n rule: f.induct)"}


194 
\end{quote}


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


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


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


198 


199 
\section{Induction heuristics}


200 


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


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


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


204 
\begin{quote}


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


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


207 
\end{quote}


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

47711

209 
\emph{generalize the goal before induction}.

47269

210 
The reason is simple: if the goal is


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


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


213 


214 
Function @{const rev} has quadratic worstcase running time


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


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


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


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


219 
*}


220 
(*<*)


221 
apply auto


222 
done


223 
(*>*)


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

47711

225 
"itrev [] ys = ys" 

47269

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


227 


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


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

47711

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

47269

231 
empty. Note that @{const itrev} is tailrecursive: it can be


232 
compiled into a loop, no stack is necessary for executing it.


233 


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


235 
its first argument provided the second one is empty:


236 
*}


237 


238 
lemma "itrev xs [] = rev xs"


239 


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


241 
*}


242 


243 
apply(induction xs)


244 
apply(auto)


245 


246 
txt{*


247 
Unfortunately, this attempt does not prove


248 
the induction step:


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


250 
The induction hypothesis is too weak. The fixed


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


252 
This example suggests a heuristic:


253 
\begin{quote}

47711

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

47269

255 
\end{quote}


256 
Of course one cannot do this na\"{\i}vely: @{prop"itrev xs ys = rev xs"} is

47711

257 
just not true. The correct generalization is

47269

258 
*};


259 
(*<*)oops;(*>*)


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


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


262 
txt{*


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


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

47711

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

47269

266 
Other situations can require a good deal of creativity.


267 


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


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


270 
not there:


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


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

47711

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

47269

274 
in the induction hypothesis is fixed,


275 
but the induction hypothesis needs to be applied with


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


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

47711

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

47269

279 
*}


280 
(*<*)oops


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


282 
(*>*)


283 
apply(induction xs arbitrary: ys)


284 


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


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


287 
Thus the proof succeeds:


288 
*}


289 


290 
apply auto


291 
done


292 


293 
text{*

47711

294 
This leads to another heuristic for generalization:

47269

295 
\begin{quote}

47711

296 
\emph{Generalize induction by generalizing all free

47269

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


298 
\end{quote}

47711

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

47269

300 
This heuristic prevents trivial failures like the one above.


301 
However, it should not be applied blindly.


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


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


304 
those that change in recursive calls.


305 


306 
\section{Simplification}


307 


308 
So far we have talked a lot about simplifying terms without explaining the concept. \concept{Simplification} means


309 
\begin{itemize}


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


311 
\item as long as possible.


312 
\end{itemize}

47711

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

47269

314 
@{text"simp"} attribute are called \concept{simplification}


315 
rules. Logically, they are still symmetric, but proofs by


316 
simplification use them only in the lefttoright direction. The proof tool


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


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


319 


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


321 
simplification rules


322 
\[


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


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


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


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


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


328 
\end{array}


329 
\]


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


331 
as follows:


332 
\[


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


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


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


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


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


338 
& @{const True}


339 
\end{array}


340 
\]


341 
Simplification is often also called \concept{rewriting}


342 
and simplification rules \concept{rewrite rules}.


343 


344 
\subsection{Simplification rules}


345 


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


347 
which the simplifier will use automatically. In addition,


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


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


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


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


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


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


354 


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


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


357 
rules. Equations that may be counterproductive as simplification rules


358 
should only be used in specific proof steps (see \S\ref{sec:simp} below).


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


360 
and can produce an exponential blowup.


361 


362 
\subsection{Conditional simplification rules}


363 


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


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


366 
simplification. For example, given the simplification rules


367 
\begin{quote}


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


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


370 
\end{quote}


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


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


373 
is not provable.


374 


375 
\subsection{Termination}


376 


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


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


379 
responsibility not to include simplification rules that can lead to


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


381 
simplification rules. The righthand side of a simplification rule should


382 
always be ``simpler'' than the lefthand sidein some sense. But since


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


384 
and Isabelle makes little attempt to detect nontermination.


385 


386 
When conditional simplification rules are applied, their preconditions are


387 
proved first. Hence all preconditions need to be


388 
simpler than the lefthand side of the conclusion. For example


389 
\begin{quote}


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


391 
\end{quote}


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


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


394 
\begin{quote}


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


396 
\end{quote}


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


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


399 


400 
\subsection{The @{text simp} proof method}


401 
\label{sec:simp}


402 


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


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


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


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


407 
Given a goal


408 
\begin{quote}


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


410 
\end{quote}


411 
the command


412 
\begin{quote}


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


414 
\end{quote}


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


416 
\begin{itemize}


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


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


419 
\item the assumptions.


420 
\end{itemize}


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


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


423 
can be modified similarly:


424 
\begin{quote}


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


426 
\end{quote}


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


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


429 
does not just perform simplification.


430 


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


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


433 
all subgoals.


434 


435 
\subsection{Rewriting with definitions}


436 
\label{sec:rewrdefs}


437 


438 
Definitions introduced by the command \isacom{definition}


439 
can also be used as simplification rules,


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


441 
automatically. Definitions are intended for introducing abstract concepts and


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


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


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


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


446 
properties will be affected.


447 


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


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


450 
\begin{quote}


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


452 
\end{quote}


453 
In particular, letexpressions can be unfolded by


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


455 


456 
\subsection{Case splitting with @{text simp}}


457 


458 
Goals containing ifexpressions are automatically split into two cases by


459 
@{text simp} using the rule


460 
\begin{quote}


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


462 
\end{quote}


463 
For example, @{text simp} can prove


464 
\begin{quote}


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


466 
\end{quote}


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


468 
simplify to @{const True}.


469 


470 
We can split caseexpressions similarly. For @{text nat} the rule looks like this:


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


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


473 
can be instructed to do so:


474 
\begin{quote}


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


476 
\end{quote}


477 
splits all caseexpressions over natural numbers. For an arbitrary


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


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


480 
*}


481 
(*<*)


482 
end


483 
(*>*)
