21212

1 
(* Title: Doc/IsarAdvanced/Functions/Thy/Fundefs.thy


2 
ID: $Id$


3 
Author: Alexander Krauss, TU Muenchen


4 


5 
Tutorial for function definitions with the new "function" package.


6 
*)


7 


8 
theory Functions


9 
imports Main


10 
begin


11 

23188

12 
section {* Function Definitions for Dummies *}

21212

13 


14 
text {*


15 
In most cases, defining a recursive function is just as simple as other definitions:

23003

16 
*}

21212

17 


18 
fun fib :: "nat \<Rightarrow> nat"


19 
where


20 
"fib 0 = 1"


21 
 "fib (Suc 0) = 1"


22 
 "fib (Suc (Suc n)) = fib n + fib (Suc n)"


23 


24 
text {*

23003

25 
The syntax is rather selfexplanatory: We introduce a function by


26 
giving its name, its type and a set of defining recursive

23805

27 
equations.

23003

28 
*}


29 


30 
text {*


31 
The function always terminates, since its argument gets smaller in

23188

32 
every recursive call.


33 
Since HOL is a logic of total functions, termination is a


34 
fundamental requirement to prevent inconsistencies\footnote{From the


35 
\qt{definition} @{text "f(n) = f(n) + 1"} we could prove


36 
@{text "0 = 1"} by subtracting @{text "f(n)"} on both sides.}.


37 
Isabelle tries to prove termination automatically when a definition


38 
is made. In \S\ref{termination}, we will look at cases where this


39 
fails and see what to do then.

21212

40 
*}


41 


42 
subsection {* Pattern matching *}


43 

22065

44 
text {* \label{patmatch}

23003

45 
Like in functional programming, we can use pattern matching to


46 
define functions. At the moment we will only consider \emph{constructor

21212

47 
patterns}, which only consist of datatype constructors and

23805

48 
variables. Furthermore, patterns must be linear, i.e.\ all variables


49 
on the left hand side of an equation must be distinct. In


50 
\S\ref{genpats} we discuss more general pattern matching.

21212

51 


52 
If patterns overlap, the order of the equations is taken into


53 
account. The following function inserts a fixed element between any


54 
two elements of a list:


55 
*}


56 


57 
fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"


58 
where


59 
"sep a (x#y#xs) = x # a # sep a (y # xs)"


60 
 "sep a xs = xs"


61 


62 
text {*

23188

63 
Overlapping patterns are interpreted as \qt{increments} to what is

21212

64 
already there: The second equation is only meant for the cases where


65 
the first one does not match. Consequently, Isabelle replaces it

22065

66 
internally by the remaining cases, making the patterns disjoint:

21212

67 
*}


68 

22065

69 
thm sep.simps

21212

70 

22065

71 
text {* @{thm [display] sep.simps[no_vars]} *}

21212

72 


73 
text {*

23805

74 
\noindent The equations from function definitions are automatically used in

21212

75 
simplification:


76 
*}


77 

23188

78 
lemma "sep 0 [1, 2, 3] = [1, 0, 2, 0, 3]"

21212

79 
by simp


80 


81 
subsection {* Induction *}


82 

22065

83 
text {*


84 

23805

85 
Isabelle provides customized induction rules for recursive


86 
functions. These rules follow the recursive structure of the


87 
definition. Here is the rule @{text sep.induct} arising from the


88 
above definition of @{const sep}:


89 


90 
@{thm [display] sep.induct}


91 


92 
We have a step case for list with at least two elements, and two


93 
base cases for the zero and the oneelement list. Here is a simple


94 
proof about @{const sep} and @{const map}


95 
*}

23188

96 

23805

97 
lemma "map f (sep x ys) = sep (f x) (map f ys)"


98 
apply (induct x ys rule: sep.induct)


99 


100 
txt {*


101 
We get three cases, like in the definition.


102 


103 
@{subgoals [display]}


104 
*}


105 


106 
apply auto


107 
done


108 
text {*

23188

109 


110 
With the \cmd{fun} command, you can define about 80\% of the


111 
functions that occur in practice. The rest of this tutorial explains


112 
the remaining 20\%.

22065

113 
*}

21212

114 


115 

23188

116 
section {* fun vs.\ function *}

21212

117 


118 
text {*

23188

119 
The \cmd{fun} command provides a

21212

120 
convenient shorthand notation for simple function definitions. In


121 
this mode, Isabelle tries to solve all the necessary proof obligations

23188

122 
automatically. If a proof fails, the definition is

22065

123 
rejected. This can either mean that the definition is indeed faulty,


124 
or that the default proof procedures are just not smart enough (or


125 
rather: not designed) to handle the definition.


126 

23188

127 
By expanding the abbreviation to the more verbose \cmd{function} command, these proof obligations become visible and can be analyzed or


128 
solved manually. The expansion from \cmd{fun} to \cmd{function} is as follows:

22065

129 


130 
\end{isamarkuptext}


131 


132 

23188

133 
\[\left[\;\begin{minipage}{0.25\textwidth}\vspace{6pt}


134 
\cmd{fun} @{text "f :: \<tau>"}\\%


135 
\cmd{where}\\%


136 
\hspace*{2ex}{\it equations}\\%


137 
\hspace*{2ex}\vdots\vspace*{6pt}


138 
\end{minipage}\right]


139 
\quad\equiv\quad


140 
\left[\;\begin{minipage}{0.45\textwidth}\vspace{6pt}


141 
\cmd{function} @{text "("}\cmd{sequential}@{text ") f :: \<tau>"}\\%


142 
\cmd{where}\\%


143 
\hspace*{2ex}{\it equations}\\%


144 
\hspace*{2ex}\vdots\\%

22065

145 
\cmd{by} @{text "pat_completeness auto"}\\%

23188

146 
\cmd{termination by} @{text "lexicographic_order"}\vspace{6pt}


147 
\end{minipage}


148 
\right]\]

21212

149 

22065

150 
\begin{isamarkuptext}


151 
\vspace*{1em}

23188

152 
\noindent Some details have now become explicit:

21212

153 


154 
\begin{enumerate}

22065

155 
\item The \cmd{sequential} option enables the preprocessing of

23805

156 
pattern overlaps which we already saw. Without this option, the equations

21212

157 
must already be disjoint and complete. The automatic completion only

23188

158 
works with constructor patterns.

21212

159 

23188

160 
\item A function definition produces a proof obligation which


161 
expresses completeness and compatibility of patterns (we talk about

22065

162 
this later). The combination of the methods @{text "pat_completeness"} and


163 
@{text "auto"} is used to solve this proof obligation.

21212

164 


165 
\item A termination proof follows the definition, started by the

23188

166 
\cmd{termination} command. This will be explained in \S\ref{termination}.

22065

167 
\end{enumerate}


168 
Whenever a \cmd{fun} command fails, it is usually a good idea to


169 
expand the syntax to the more verbose \cmd{function} form, to see


170 
what is actually going on.

21212

171 
*}


172 


173 

23188

174 
section {* Termination *}

21212

175 

23188

176 
text {*\label{termination}

23805

177 
The method @{text "lexicographic_order"} is the default method for


178 
termination proofs. It can prove termination of a

23188

179 
certain class of functions by searching for a suitable lexicographic


180 
combination of size measures. Of course, not all functions have such

23805

181 
a simple termination argument. For them, we can specify the termination


182 
relation manually.

23188

183 
*}


184 


185 
subsection {* The {\tt relation} method *}


186 
text{*

21212

187 
Consider the following function, which sums up natural numbers up to

22065

188 
@{text "N"}, using a counter @{text "i"}:

21212

189 
*}


190 


191 
function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"


192 
where


193 
"sum i N = (if i > N then 0 else i + sum (Suc i) N)"

22065

194 
by pat_completeness auto

21212

195 


196 
text {*

22065

197 
\noindent The @{text "lexicographic_order"} method fails on this example, because none of the

23805

198 
arguments decreases in the recursive call, with respect to the standard size ordering.


199 
To prove termination manually, we must provide a custom wellfounded relation.

21212

200 


201 
The termination argument for @{text "sum"} is based on the fact that


202 
the \emph{difference} between @{text "i"} and @{text "N"} gets


203 
smaller in every step, and that the recursion stops when @{text "i"}

23805

204 
is greater than @{text "N"}. Phrased differently, the expression


205 
@{text "N + 1  i"} always decreases.

21212

206 

22065

207 
We can use this expression as a measure function suitable to prove termination.

21212

208 
*}


209 

23805

210 
termination

23188

211 
apply (relation "measure (\<lambda>(i,N). N + 1  i)")

21212

212 

23188

213 
txt {*

23003

214 
The \cmd{termination} command sets up the termination goal for the

23188

215 
specified function @{text "sum"}. If the function name is omitted, it

23003

216 
implicitly refers to the last function definition.


217 

22065

218 
The @{text relation} method takes a relation of


219 
type @{typ "('a \<times> 'a) set"}, where @{typ "'a"} is the argument type of


220 
the function. If the function has multiple curried arguments, then


221 
these are packed together into a tuple, as it happened in the above


222 
example.

21212

223 

23188

224 
The predefined function @{term_type "measure"} constructs a


225 
wellfounded relation from a mapping into the natural numbers (a


226 
\emph{measure function}).

22065

227 


228 
After the invocation of @{text "relation"}, we must prove that (a)


229 
the relation we supplied is wellfounded, and (b) that the arguments


230 
of recursive calls indeed decrease with respect to the

23188

231 
relation:


232 


233 
@{subgoals[display,indent=0]}

22065

234 

23188

235 
These goals are all solved by @{text "auto"}:


236 
*}


237 


238 
apply auto


239 
done


240 


241 
text {*

22065

242 
Let us complicate the function a little, by adding some more


243 
recursive calls:

21212

244 
*}


245 


246 
function foo :: "nat \<Rightarrow> nat \<Rightarrow> nat"


247 
where


248 
"foo i N = (if i > N


249 
then (if N = 0 then 0 else foo 0 (N  1))


250 
else i + foo (Suc i) N)"


251 
by pat_completeness auto


252 


253 
text {*


254 
When @{text "i"} has reached @{text "N"}, it starts at zero again


255 
and @{text "N"} is decremented.


256 
This corresponds to a nested


257 
loop where one index counts up and the other down. Termination can


258 
be proved using a lexicographic combination of two measures, namely

22065

259 
the value of @{text "N"} and the above difference. The @{const


260 
"measures"} combinator generalizes @{text "measure"} by taking a


261 
list of measure functions.

21212

262 
*}


263 


264 
termination

22065

265 
by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1  i]") auto

21212

266 

23188

267 
subsection {* How @{text "lexicographic_order"} works *}


268 


269 
(*fun fails :: "nat \<Rightarrow> nat list \<Rightarrow> nat"


270 
where


271 
"fails a [] = a"


272 
 "fails a (x#xs) = fails (x + a) (x # xs)"


273 
*)

23003

274 


275 
text {*

23188

276 
To see how the automatic termination proofs work, let's look at an


277 
example where it fails\footnote{For a detailed discussion of the


278 
termination prover, see \cite{bulwahnKN07}}:


279 


280 
\end{isamarkuptext}


281 
\cmd{fun} @{text "fails :: \"nat \<Rightarrow> nat list \<Rightarrow> nat\""}\\%


282 
\cmd{where}\\%


283 
\hspace*{2ex}@{text "\"fails a [] = a\""}\\%


284 
\hspace*{1.5ex}@{text "\"fails a (x#xs) = fails (x + a) (x#xs)\""}\\


285 
\begin{isamarkuptext}


286 


287 
\noindent Isabelle responds with the following error:


288 


289 
\begin{isabelle}

23805

290 
*** Unfinished subgoals:\newline


291 
*** (a, 1, <):\newline


292 
*** \ 1.~@{text "\<And>x. x = 0"}\newline


293 
*** (a, 1, <=):\newline


294 
*** \ 1.~False\newline


295 
*** (a, 2, <):\newline


296 
*** \ 1.~False\newline

23188

297 
*** Calls:\newline


298 
*** a) @{text "(a, x # xs) >> (x + a, x # xs)"}\newline


299 
*** Measures:\newline


300 
*** 1) @{text "\<lambda>x. size (fst x)"}\newline


301 
*** 2) @{text "\<lambda>x. size (snd x)"}\newline

23805

302 
*** Result matrix:\newline


303 
*** \ \ \ \ 1\ \ 2 \newline


304 
*** a: ? <= \newline


305 
*** Could not find lexicographic termination order.\newline

23188

306 
*** At command "fun".\newline


307 
\end{isabelle}

23003

308 
*}


309 

23188

310 


311 
text {*


312 


313 

23805

314 
The the key to this error message is the matrix at the bottom. The rows

23188

315 
of that matrix correspond to the different recursive calls (In our


316 
case, there is just one). The columns are the function's arguments


317 
(expressed through different measure functions, which map the


318 
argument tuple to a natural number).


319 


320 
The contents of the matrix summarize what is known about argument


321 
descents: The second argument has a weak descent (@{text "<="}) at the


322 
recursive call, and for the first argument nothing could be proved,

23805

323 
which is expressed by @{text "?"}. In general, there are the values


324 
@{text "<"}, @{text "<="} and @{text "?"}.

23188

325 


326 
For the failed proof attempts, the unfinished subgoals are also

23805

327 
printed. Looking at these will often point to a missing lemma.

23188

328 


329 
% As a more real example, here is quicksort:


330 
*}


331 
(*


332 
function qs :: "nat list \<Rightarrow> nat list"

23003

333 
where

23188

334 
"qs [] = []"


335 
 "qs (x#xs) = qs [y\<in>xs. y < x] @ x # qs [y\<in>xs. y \<ge> x]"

23003

336 
by pat_completeness auto


337 

23188

338 
termination apply lexicographic_order


339 


340 
text {* If we try @{text "lexicographic_order"} method, we get the


341 
following error *}


342 
termination by (lexicographic_order simp:l2)

23003

343 

23188

344 
lemma l: "x \<le> y \<Longrightarrow> x < Suc y" by arith

23003

345 

23188

346 
function


347 


348 
*)

21212

349 


350 
section {* Mutual Recursion *}


351 


352 
text {*


353 
If two or more functions call one another mutually, they have to be defined

23188

354 
in one step. Here are @{text "even"} and @{text "odd"}:

21212

355 
*}


356 

22065

357 
function even :: "nat \<Rightarrow> bool"


358 
and odd :: "nat \<Rightarrow> bool"

21212

359 
where


360 
"even 0 = True"


361 
 "odd 0 = False"


362 
 "even (Suc n) = odd n"


363 
 "odd (Suc n) = even n"

22065

364 
by pat_completeness auto

21212

365 


366 
text {*

23188

367 
To eliminate the mutual dependencies, Isabelle internally

21212

368 
creates a single function operating on the sum

23188

369 
type @{typ "nat + nat"}. Then, @{const even} and @{const odd} are


370 
defined as projections. Consequently, termination has to be proved

21212

371 
simultaneously for both functions, by specifying a measure on the


372 
sum type:


373 
*}


374 


375 
termination

23188

376 
by (relation "measure (\<lambda>x. case x of Inl n \<Rightarrow> n  Inr n \<Rightarrow> n)") auto


377 


378 
text {*


379 
We could also have used @{text lexicographic_order}, which


380 
supports mutual recursive termination proofs to a certain extent.


381 
*}

22065

382 


383 
subsection {* Induction for mutual recursion *}


384 


385 
text {*


386 


387 
When functions are mutually recursive, proving properties about them

23188

388 
generally requires simultaneous induction. The induction rule @{text "even_odd.induct"}


389 
generated from the above definition reflects this.

22065

390 


391 
Let us prove something about @{const even} and @{const odd}:


392 
*}


393 

23188

394 
lemma even_odd_mod2:

22065

395 
"even n = (n mod 2 = 0)"


396 
"odd n = (n mod 2 = 1)"


397 


398 
txt {*


399 
We apply simultaneous induction, specifying the induction variable


400 
for both goals, separated by \cmd{and}: *}


401 


402 
apply (induct n and n rule: even_odd.induct)


403 


404 
txt {*


405 
We get four subgoals, which correspond to the clauses in the


406 
definition of @{const even} and @{const odd}:


407 
@{subgoals[display,indent=0]}


408 
Simplification solves the first two goals, leaving us with two


409 
statements about the @{text "mod"} operation to prove:


410 
*}


411 


412 
apply simp_all


413 


414 
txt {*


415 
@{subgoals[display,indent=0]}


416 

23805

417 
\noindent These can be handled by Isabelle's arithmetic decision procedures.

22065

418 


419 
*}


420 

23805

421 
apply arith


422 
apply arith

22065

423 
done

21212

424 

22065

425 
text {*

23188

426 
In proofs like this, the simultaneous induction is really essential:


427 
Even if we are just interested in one of the results, the other


428 
one is necessary to strengthen the induction hypothesis. If we leave


429 
out the statement about @{const odd} (by substituting it with @{term


430 
"True"}), the same proof fails:

22065

431 
*}


432 

23188

433 
lemma failed_attempt:

22065

434 
"even n = (n mod 2 = 0)"


435 
"True"


436 
apply (induct n rule: even_odd.induct)


437 


438 
txt {*


439 
\noindent Now the third subgoal is a dead end, since we have no

23188

440 
useful induction hypothesis available:

22065

441 


442 
@{subgoals[display,indent=0]}


443 
*}


444 


445 
oops


446 

23188

447 
section {* General pattern matching *}

23805

448 
text{*\label{genpats} *}

22065

449 

23188

450 
subsection {* Avoiding automatic pattern splitting *}

22065

451 


452 
text {*


453 


454 
Up to now, we used pattern matching only on datatypes, and the


455 
patterns were always disjoint and complete, and if they weren't,


456 
they were made disjoint automatically like in the definition of


457 
@{const "sep"} in \S\ref{patmatch}.


458 

23188

459 
This automatic splitting can significantly increase the number of


460 
equations involved, and this is not always desirable. The following


461 
example shows the problem:

22065

462 

23805

463 
Suppose we are modeling incomplete knowledge about the world by a

23003

464 
threevalued datatype, which has values @{term "T"}, @{term "F"}


465 
and @{term "X"} for true, false and uncertain propositions, respectively.

22065

466 
*}


467 


468 
datatype P3 = T  F  X


469 

23188

470 
text {* \noindent Then the conjunction of such values can be defined as follows: *}

22065

471 


472 
fun And :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"


473 
where


474 
"And T p = p"

23003

475 
 "And p T = p"


476 
 "And p F = F"


477 
 "And F p = F"


478 
 "And X X = X"

21212

479 


480 

22065

481 
text {*


482 
This definition is useful, because the equations can directly be used

23805

483 
as simplification rules rules. But the patterns overlap: For example,

23188

484 
the expression @{term "And T T"} is matched by both the first and


485 
the second equation. By default, Isabelle makes the patterns disjoint by

22065

486 
splitting them up, producing instances:


487 
*}


488 


489 
thm And.simps


490 


491 
text {*


492 
@{thm[indent=4] And.simps}


493 


494 
\vspace*{1em}

23003

495 
\noindent There are several problems with this:

22065

496 


497 
\begin{enumerate}

23188

498 
\item If the datatype has many constructors, there can be an

22065

499 
explosion of equations. For @{const "And"}, we get seven instead of

23003

500 
five equations, which can be tolerated, but this is just a small

22065

501 
example.


502 

23188

503 
\item Since splitting makes the equations \qt{less general}, they

22065

504 
do not always match in rewriting. While the term @{term "And x F"}

23188

505 
can be simplified to @{term "F"} with the original equations, a

22065

506 
(manual) case split on @{term "x"} is now necessary.


507 


508 
\item The splitting also concerns the induction rule @{text


509 
"And.induct"}. Instead of five premises it now has seven, which


510 
means that our induction proofs will have more cases.


511 


512 
\item In general, it increases clarity if we get the same definition


513 
back which we put in.


514 
\end{enumerate}


515 

23188

516 
If we do not want the automatic splitting, we can switch it off by


517 
leaving out the \cmd{sequential} option. However, we will have to


518 
prove that our pattern matching is consistent\footnote{This prevents


519 
us from defining something like @{term "f x = True"} and @{term "f x


520 
= False"} simultaneously.}:

22065

521 
*}


522 


523 
function And2 :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"


524 
where


525 
"And2 T p = p"

23003

526 
 "And2 p T = p"


527 
 "And2 p F = F"


528 
 "And2 F p = F"


529 
 "And2 X X = X"

22065

530 


531 
txt {*

23188

532 
\noindent Now let's look at the proof obligations generated by a

22065

533 
function definition. In this case, they are:


534 

23188

535 
@{subgoals[display,indent=0]}\vspace{1.2em}\hspace{3cm}\vdots\vspace{1.2em}

22065

536 


537 
The first subgoal expresses the completeness of the patterns. It has


538 
the form of an elimination rule and states that every @{term x} of

23188

539 
the function's input type must match at least one of the patterns\footnote{Completeness could

22065

540 
be equivalently stated as a disjunction of existential statements:


541 
@{term "(\<exists>p. x = (T, p)) \<or> (\<exists>p. x = (p, T)) \<or> (\<exists>p. x = (p, F)) \<or>

23188

542 
(\<exists>p. x = (F, p)) \<or> (x = (X, X))"}.}. If the patterns just involve


543 
datatypes, we can solve it with the @{text "pat_completeness"}


544 
method:

22065

545 
*}


546 


547 
apply pat_completeness


548 


549 
txt {*


550 
The remaining subgoals express \emph{pattern compatibility}. We do

23188

551 
allow that an input value matches multiple patterns, but in this

22065

552 
case, the result (i.e.~the right hand sides of the equations) must


553 
also be equal. For each pair of two patterns, there is one such


554 
subgoal. Usually this needs injectivity of the constructors, which


555 
is used automatically by @{text "auto"}.


556 
*}


557 


558 
by auto

21212

559 


560 

22065

561 
subsection {* Nonconstructor patterns *}

21212

562 

23188

563 
text {*

23805

564 
Most of Isabelle's basic types take the form of inductive datatypes,


565 
and usually pattern matching works on the constructors of such types.


566 
However, this need not be always the case, and the \cmd{function}


567 
command handles other kind of patterns, too.

23188

568 

23805

569 
One wellknown instance of nonconstructor patterns are

23188

570 
socalled \emph{$n+k$patterns}, which are a little controversial in


571 
the functional programming world. Here is the initial fibonacci


572 
example with $n+k$patterns:


573 
*}


574 


575 
function fib2 :: "nat \<Rightarrow> nat"


576 
where


577 
"fib2 0 = 1"


578 
 "fib2 1 = 1"


579 
 "fib2 (n + 2) = fib2 n + fib2 (Suc n)"


580 


581 
(*<*)ML "goals_limit := 1"(*>*)


582 
txt {*

23805

583 
This kind of matching is again justified by the proof of pattern


584 
completeness and compatibility.

23188

585 
The proof obligation for pattern completeness states that every natural number is


586 
either @{term "0::nat"}, @{term "1::nat"} or @{term "n +


587 
(2::nat)"}:


588 


589 
@{subgoals[display,indent=0]}


590 


591 
This is an arithmetic triviality, but unfortunately the


592 
@{text arith} method cannot handle this specific form of an

23805

593 
elimination rule. However, we can use the method @{text


594 
"elim_to_cases"} to do an adhoc conversion to a disjunction of


595 
existentials, which can then be soved by the arithmetic decision procedure.


596 
Pattern compatibility and termination are automatic as usual.

23188

597 
*}


598 
(*<*)ML "goals_limit := 10"(*>*)

23805

599 
apply elim_to_cases


600 
apply arith

23188

601 
apply auto


602 
done


603 
termination by lexicographic_order


604 


605 
text {*


606 
We can stretch the notion of pattern matching even more. The


607 
following function is not a sensible functional program, but a


608 
perfectly valid mathematical definition:


609 
*}


610 


611 
function ev :: "nat \<Rightarrow> bool"


612 
where


613 
"ev (2 * n) = True"


614 
 "ev (2 * n + 1) = False"

23805

615 
apply elim_to_cases


616 
by arith+

23188

617 
termination by (relation "{}") simp


618 


619 
text {*


620 
This general notion of pattern matching gives you the full freedom


621 
of mathematical specifications. However, as always, freedom should


622 
be used with care:


623 


624 
If we leave the area of constructor


625 
patterns, we have effectively departed from the world of functional


626 
programming. This means that it is no longer possible to use the


627 
code generator, and expect it to generate ML code for our


628 
definitions. Also, such a specification might not work very well together with


629 
simplification. Your mileage may vary.


630 
*}


631 


632 


633 
subsection {* Conditional equations *}


634 


635 
text {*


636 
The function package also supports conditional equations, which are


637 
similar to guards in a language like Haskell. Here is Euclid's


638 
algorithm written with conditional patterns\footnote{Note that the


639 
patterns are also overlapping in the base case}:


640 
*}


641 


642 
function gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat"


643 
where


644 
"gcd x 0 = x"


645 
 "gcd 0 y = y"


646 
 "x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (Suc x) (y  x)"


647 
 "\<not> x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (x  y) (Suc y)"

23805

648 
by (elim_to_cases, auto, arith)

23188

649 
termination by lexicographic_order


650 


651 
text {*


652 
By now, you can probably guess what the proof obligations for the


653 
pattern completeness and compatibility look like.


654 


655 
Again, functions with conditional patterns are not supported by the


656 
code generator.


657 
*}


658 


659 


660 
subsection {* Pattern matching on strings *}


661 


662 
text {*

23805

663 
As strings (as lists of characters) are normal datatypes, pattern

23188

664 
matching on them is possible, but somewhat problematic. Consider the


665 
following definition:


666 


667 
\end{isamarkuptext}


668 
\noindent\cmd{fun} @{text "check :: \"string \<Rightarrow> bool\""}\\%


669 
\cmd{where}\\%


670 
\hspace*{2ex}@{text "\"check (''good'') = True\""}\\%


671 
@{text " \"check s = False\""}


672 
\begin{isamarkuptext}


673 

23805

674 
\noindent An invocation of the above \cmd{fun} command does not

23188

675 
terminate. What is the problem? Strings are lists of characters, and

23805

676 
characters are a datatype with a lot of constructors. Splitting the

23188

677 
catchall pattern thus leads to an explosion of cases, which cannot


678 
be handled by Isabelle.


679 


680 
There are two things we can do here. Either we write an explicit


681 
@{text "if"} on the right hand side, or we can use conditional patterns:


682 
*}


683 


684 
function check :: "string \<Rightarrow> bool"


685 
where


686 
"check (''good'') = True"


687 
 "s \<noteq> ''good'' \<Longrightarrow> check s = False"


688 
by auto

22065

689 


690 


691 
section {* Partiality *}


692 


693 
text {*


694 
In HOL, all functions are total. A function @{term "f"} applied to

23188

695 
@{term "x"} always has the value @{term "f x"}, and there is no notion

22065

696 
of undefinedness.

23188

697 
This is why we have to do termination


698 
proofs when defining functions: The proof justifies that the


699 
function can be defined by wellfounded recursion.

22065

700 

23188

701 
However, the \cmd{function} package does support partiality to a


702 
certain extent. Let's look at the following function which looks


703 
for a zero of a given function f.

23003

704 
*}


705 


706 
function (*<*)(domintros, tailrec)(*>*)findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"


707 
where


708 
"findzero f n = (if f n = 0 then n else findzero f (Suc n))"


709 
by pat_completeness auto


710 
(*<*)declare findzero.simps[simp del](*>*)


711 


712 
text {*

23805

713 
\noindent Clearly, any attempt of a termination proof must fail. And without

23003

714 
that, we do not get the usual rules @{text "findzero.simp"} and


715 
@{text "findzero.induct"}. So what was the definition good for at all?


716 
*}


717 


718 
subsection {* Domain predicates *}


719 


720 
text {*


721 
The trick is that Isabelle has not only defined the function @{const findzero}, but also


722 
a predicate @{term "findzero_dom"} that characterizes the values where the function

23188

723 
terminates: the \emph{domain} of the function. If we treat a


724 
partial function just as a total function with an additional domain


725 
predicate, we can derive simplification and


726 
induction rules as we do for total functions. They are guarded


727 
by domain conditions and are called @{text psimps} and @{text


728 
pinduct}:

23003

729 
*}


730 

23805

731 
text {*


732 
\noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.psimps}\end{minipage}


733 
\hfill(@{text "findzero.psimps"})


734 
\vspace{1em}

23003

735 

23805

736 
\noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.pinduct}\end{minipage}


737 
\hfill(@{text "findzero.pinduct"})

23003

738 
*}


739 


740 
text {*

23188

741 
Remember that all we


742 
are doing here is use some tricks to make a total function appear

23003

743 
as if it was partial. We can still write the term @{term "findzero


744 
(\<lambda>x. 1) 0"} and like any other term of type @{typ nat} it is equal


745 
to some natural number, although we might not be able to find out

23188

746 
which one. The function is \emph{underdefined}.

23003

747 

23805

748 
But it is defined enough to prove something interesting about it. We

23188

749 
can prove that if @{term "findzero f n"}

23805

750 
terminates, it indeed returns a zero of @{term f}:

23003

751 
*}


752 


753 
lemma findzero_zero: "findzero_dom (f, n) \<Longrightarrow> f (findzero f n) = 0"


754 

23805

755 
txt {* \noindent We apply induction as usual, but using the partial induction

23003

756 
rule: *}


757 


758 
apply (induct f n rule: findzero.pinduct)


759 

23805

760 
txt {* \noindent This gives the following subgoals:

23003

761 


762 
@{subgoals[display,indent=0]}


763 

23805

764 
\noindent The hypothesis in our lemma was used to satisfy the first premise in

23188

765 
the induction rule. However, we also get @{term


766 
"findzero_dom (f, n)"} as a local assumption in the induction step. This

23003

767 
allows to unfold @{term "findzero f n"} using the @{text psimps}

23188

768 
rule, and the rest is trivial. Since the @{text psimps} rules carry the

23003

769 
@{text "[simp]"} attribute by default, we just need a single step:


770 
*}


771 
apply simp


772 
done


773 


774 
text {*


775 
Proofs about partial functions are often not harder than for total


776 
functions. Fig.~\ref{findzero_isar} shows a slightly more


777 
complicated proof written in Isar. It is verbose enough to show how


778 
partiality comes into play: From the partial induction, we get an


779 
additional domain condition hypothesis. Observe how this condition


780 
is applied when calls to @{term findzero} are unfolded.


781 
*}


782 


783 
text_raw {*


784 
\begin{figure}

23188

785 
\hrule\vspace{6pt}

23003

786 
\begin{minipage}{0.8\textwidth}


787 
\isabellestyle{it}


788 
\isastyle\isamarkuptrue


789 
*}


790 
lemma "\<lbrakk>findzero_dom (f, n); x \<in> {n ..< findzero f n}\<rbrakk> \<Longrightarrow> f x \<noteq> 0"


791 
proof (induct rule: findzero.pinduct)


792 
fix f n assume dom: "findzero_dom (f, n)"

23188

793 
and IH: "\<lbrakk>f n \<noteq> 0; x \<in> {Suc n ..< findzero f (Suc n)}\<rbrakk> \<Longrightarrow> f x \<noteq> 0"


794 
and x_range: "x \<in> {n ..< findzero f n}"

23003

795 
have "f n \<noteq> 0"


796 
proof


797 
assume "f n = 0"


798 
with dom have "findzero f n = n" by simp


799 
with x_range show False by auto


800 
qed


801 


802 
from x_range have "x = n \<or> x \<in> {Suc n ..< findzero f n}" by auto


803 
thus "f x \<noteq> 0"


804 
proof


805 
assume "x = n"


806 
with `f n \<noteq> 0` show ?thesis by simp


807 
next

23188

808 
assume "x \<in> {Suc n ..< findzero f n}"

23805

809 
with dom and `f n \<noteq> 0` have "x \<in> {Suc n ..< findzero f (Suc n)}" by simp

23003

810 
with IH and `f n \<noteq> 0`


811 
show ?thesis by simp


812 
qed


813 
qed


814 
text_raw {*


815 
\isamarkupfalse\isabellestyle{tt}

23188

816 
\end{minipage}\vspace{6pt}\hrule

23003

817 
\caption{A proof about a partial function}\label{findzero_isar}


818 
\end{figure}


819 
*}


820 


821 
subsection {* Partial termination proofs *}


822 


823 
text {*


824 
Now that we have proved some interesting properties about our


825 
function, we should turn to the domain predicate and see if it is


826 
actually true for some values. Otherwise we would have just proved


827 
lemmas with @{term False} as a premise.


828 


829 
Essentially, we need some introduction rules for @{text


830 
findzero_dom}. The function package can prove such domain


831 
introduction rules automatically. But since they are not used very

23188

832 
often (they are almost never needed if the function is total), this


833 
functionality is disabled by default for efficiency reasons. So we have to go

23003

834 
back and ask for them explicitly by passing the @{text


835 
"(domintros)"} option to the function package:


836 

23188

837 
\vspace{1ex}

23003

838 
\noindent\cmd{function} @{text "(domintros) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%


839 
\cmd{where}\isanewline%


840 
\ \ \ldots\\


841 

23188

842 
\noindent Now the package has proved an introduction rule for @{text findzero_dom}:

23003

843 
*}


844 


845 
thm findzero.domintros


846 


847 
text {*


848 
@{thm[display] findzero.domintros}


849 


850 
Domain introduction rules allow to show that a given value lies in the


851 
domain of a function, if the arguments of all recursive calls


852 
are in the domain as well. They allow to do a \qt{single step} in a


853 
termination proof. Usually, you want to combine them with a suitable


854 
induction principle.


855 


856 
Since our function increases its argument at recursive calls, we


857 
need an induction principle which works \qt{backwards}. We will use


858 
@{text inc_induct}, which allows to do induction from a fixed number


859 
\qt{downwards}:


860 

23188

861 
\begin{center}@{thm inc_induct}\hfill(@{text "inc_induct"})\end{center}

23003

862 

23188

863 
Figure \ref{findzero_term} gives a detailed Isar proof of the fact

23003

864 
that @{text findzero} terminates if there is a zero which is greater


865 
or equal to @{term n}. First we derive two useful rules which will


866 
solve the base case and the step case of the induction. The

23805

867 
induction is then straightforward, except for the unusual induction

23003

868 
principle.


869 


870 
*}


871 


872 
text_raw {*


873 
\begin{figure}

23188

874 
\hrule\vspace{6pt}

23003

875 
\begin{minipage}{0.8\textwidth}


876 
\isabellestyle{it}


877 
\isastyle\isamarkuptrue


878 
*}


879 
lemma findzero_termination:

23188

880 
assumes "x \<ge> n" and "f x = 0"

23003

881 
shows "findzero_dom (f, n)"


882 
proof 


883 
have base: "findzero_dom (f, x)"


884 
by (rule findzero.domintros) (simp add:`f x = 0`)


885 


886 
have step: "\<And>i. findzero_dom (f, Suc i)


887 
\<Longrightarrow> findzero_dom (f, i)"


888 
by (rule findzero.domintros) simp


889 

23188

890 
from `x \<ge> n` show ?thesis

23003

891 
proof (induct rule:inc_induct)

23188

892 
show "findzero_dom (f, x)" by (rule base)

23003

893 
next


894 
fix i assume "findzero_dom (f, Suc i)"

23188

895 
thus "findzero_dom (f, i)" by (rule step)

23003

896 
qed


897 
qed


898 
text_raw {*


899 
\isamarkupfalse\isabellestyle{tt}

23188

900 
\end{minipage}\vspace{6pt}\hrule

23003

901 
\caption{Termination proof for @{text findzero}}\label{findzero_term}


902 
\end{figure}


903 
*}


904 


905 
text {*


906 
Again, the proof given in Fig.~\ref{findzero_term} has a lot of


907 
detail in order to explain the principles. Using more automation, we


908 
can also have a short proof:


909 
*}


910 


911 
lemma findzero_termination_short:


912 
assumes zero: "x >= n"


913 
assumes [simp]: "f x = 0"


914 
shows "findzero_dom (f, n)"

23805

915 
using zero


916 
by (induct rule:inc_induct) (auto intro: findzero.domintros)

23003

917 


918 
text {*

23188

919 
\noindent It is simple to combine the partial correctness result with the

23003

920 
termination lemma:


921 
*}


922 


923 
lemma findzero_total_correctness:


924 
"f x = 0 \<Longrightarrow> f (findzero f 0) = 0"


925 
by (blast intro: findzero_zero findzero_termination)


926 


927 
subsection {* Definition of the domain predicate *}


928 


929 
text {*


930 
Sometimes it is useful to know what the definition of the domain

23805

931 
predicate looks like. Actually, @{text findzero_dom} is just an

23003

932 
abbreviation:


933 


934 
@{abbrev[display] findzero_dom}


935 

23188

936 
The domain predicate is the \emph{accessible part} of a relation @{const

23003

937 
findzero_rel}, which was also created internally by the function


938 
package. @{const findzero_rel} is just a normal

23188

939 
inductive predicate, so we can inspect its definition by

23003

940 
looking at the introduction rules @{text findzero_rel.intros}.


941 
In our case there is just a single rule:


942 


943 
@{thm[display] findzero_rel.intros}


944 

23188

945 
The predicate @{const findzero_rel}

23003

946 
describes the \emph{recursion relation} of the function


947 
definition. The recursion relation is a binary relation on


948 
the arguments of the function that relates each argument to its


949 
recursive calls. In general, there is one introduction rule for each


950 
recursive call.


951 

23805

952 
The predicate @{term "accp findzero_rel"} is the accessible part of

23003

953 
that relation. An argument belongs to the accessible part, if it can

23188

954 
be reached in a finite number of steps (cf.~its definition in @{text


955 
"Accessible_Part.thy"}).

23003

956 


957 
Since the domain predicate is just an abbreviation, you can use

23805

958 
lemmas for @{const accp} and @{const findzero_rel} directly. Some


959 
lemmas which are occasionally useful are @{text accpI}, @{text


960 
accp_downward}, and of course the introduction and elimination rules

23003

961 
for the recursion relation @{text "findzero.intros"} and @{text "findzero.cases"}.


962 
*}


963 


964 
(*lemma findzero_nicer_domintros:


965 
"f x = 0 \<Longrightarrow> findzero_dom (f, x)"


966 
"findzero_dom (f, Suc x) \<Longrightarrow> findzero_dom (f, x)"

23805

967 
by (rule accpI, erule findzero_rel.cases, auto)+

23003

968 
*)


969 


970 
subsection {* A Useful Special Case: Tail recursion *}


971 


972 
text {*


973 
The domain predicate is our trick that allows us to model partiality


974 
in a world of total functions. The downside of this is that we have


975 
to carry it around all the time. The termination proof above allowed


976 
us to replace the abstract @{term "findzero_dom (f, n)"} by the more

23188

977 
concrete @{term "(x \<ge> n \<and> f x = (0::nat))"}, but the condition is still


978 
there and can only be discharged for special cases.


979 
In particular, the domain predicate guards the unfolding of our

23003

980 
function, since it is there as a condition in the @{text psimp}


981 
rules.


982 


983 
Now there is an important special case: We can actually get rid


984 
of the condition in the simplification rules, \emph{if the function


985 
is tailrecursive}. The reason is that for all tailrecursive


986 
equations there is a total function satisfying them, even if they


987 
are nonterminating.


988 

23188

989 
% A function is tail recursive, if each call to the function is either


990 
% equal


991 
%


992 
% So the outer form of the


993 
%


994 
%if it can be written in the following


995 
% form:


996 
% {term[display] "f x = (if COND x then BASE x else f (LOOP x))"}


997 


998 

23003

999 
The function package internally does the right construction and can


1000 
derive the unconditional simp rules, if we ask it to do so. Luckily,


1001 
our @{const "findzero"} function is tailrecursive, so we can just go


1002 
back and add another option to the \cmd{function} command:


1003 

23188

1004 
\vspace{1ex}

23003

1005 
\noindent\cmd{function} @{text "(domintros, tailrec) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%


1006 
\cmd{where}\isanewline%


1007 
\ \ \ldots\\%


1008 


1009 

23188

1010 
\noindent Now, we actually get unconditional simplification rules, even

23003

1011 
though the function is partial:


1012 
*}


1013 


1014 
thm findzero.simps


1015 


1016 
text {*


1017 
@{thm[display] findzero.simps}


1018 

23188

1019 
\noindent Of course these would make the simplifier loop, so we better remove

23003

1020 
them from the simpset:


1021 
*}


1022 


1023 
declare findzero.simps[simp del]


1024 

23188

1025 
text {*


1026 
Getting rid of the domain conditions in the simplification rules is


1027 
not only useful because it simplifies proofs. It is also required in


1028 
order to use Isabelle's code generator to generate ML code


1029 
from a function definition.


1030 
Since the code generator only works with equations, it cannot be


1031 
used with @{text "psimp"} rules. Thus, in order to generate code for


1032 
partial functions, they must be defined as a tail recursion.


1033 
Luckily, many functions have a relatively natural tail recursive


1034 
definition.


1035 
*}

23003

1036 


1037 
section {* Nested recursion *}


1038 


1039 
text {*


1040 
Recursive calls which are nested in one another frequently cause


1041 
complications, since their termination proof can depend on a partial


1042 
correctness property of the function itself.


1043 


1044 
As a small example, we define the \qt{nested zero} function:


1045 
*}


1046 


1047 
function nz :: "nat \<Rightarrow> nat"


1048 
where


1049 
"nz 0 = 0"


1050 
 "nz (Suc n) = nz (nz n)"


1051 
by pat_completeness auto


1052 


1053 
text {*


1054 
If we attempt to prove termination using the identity measure on


1055 
naturals, this fails:


1056 
*}


1057 


1058 
termination


1059 
apply (relation "measure (\<lambda>n. n)")


1060 
apply auto


1061 


1062 
txt {*


1063 
We get stuck with the subgoal


1064 


1065 
@{subgoals[display]}


1066 


1067 
Of course this statement is true, since we know that @{const nz} is


1068 
the zero function. And in fact we have no problem proving this


1069 
property by induction.


1070 
*}

23805

1071 
(*<*)oops(*>*)

23003

1072 
lemma nz_is_zero: "nz_dom n \<Longrightarrow> nz n = 0"


1073 
by (induct rule:nz.pinduct) auto


1074 


1075 
text {*


1076 
We formulate this as a partial correctness lemma with the condition


1077 
@{term "nz_dom n"}. This allows us to prove it with the @{text


1078 
pinduct} rule before we have proved termination. With this lemma,


1079 
the termination proof works as expected:


1080 
*}


1081 


1082 
termination


1083 
by (relation "measure (\<lambda>n. n)") (auto simp: nz_is_zero)


1084 


1085 
text {*


1086 
As a general strategy, one should prove the statements needed for


1087 
termination as a partial property first. Then they can be used to do


1088 
the termination proof. This also works for less trivial

23188

1089 
examples. Figure \ref{f91} defines the 91function, a wellknown


1090 
challenge problem due to John McCarthy, and proves its termination.

23003

1091 
*}


1092 


1093 
text_raw {*


1094 
\begin{figure}

23188

1095 
\hrule\vspace{6pt}

23003

1096 
\begin{minipage}{0.8\textwidth}


1097 
\isabellestyle{it}


1098 
\isastyle\isamarkuptrue


1099 
*}


1100 

23188

1101 
function f91 :: "nat \<Rightarrow> nat"

23003

1102 
where


1103 
"f91 n = (if 100 < n then n  10 else f91 (f91 (n + 11)))"


1104 
by pat_completeness auto


1105 


1106 
lemma f91_estimate:


1107 
assumes trm: "f91_dom n"


1108 
shows "n < f91 n + 11"


1109 
using trm by induct auto


1110 


1111 
termination


1112 
proof


1113 
let ?R = "measure (\<lambda>x. 101  x)"


1114 
show "wf ?R" ..


1115 


1116 
fix n :: nat assume "\<not> 100 < n"  "Assumptions for both calls"


1117 


1118 
thus "(n + 11, n) \<in> ?R" by simp  "Inner call"


1119 


1120 
assume inner_trm: "f91_dom (n + 11)"  "Outer call"


1121 
with f91_estimate have "n + 11 < f91 (n + 11) + 11" .

23805

1122 
with `\<not> 100 < n` show "(f91 (n + 11), n) \<in> ?R" by simp

23003

1123 
qed


1124 


1125 
text_raw {*


1126 
\isamarkupfalse\isabellestyle{tt}

23188

1127 
\end{minipage}


1128 
\vspace{6pt}\hrule

23003

1129 
\caption{McCarthy's 91function}\label{f91}


1130 
\end{figure}

22065

1131 
*}


1132 


1133 

23003

1134 
section {* HigherOrder Recursion *}

22065

1135 

23003

1136 
text {*


1137 
Higherorder recursion occurs when recursive calls


1138 
are passed as arguments to higherorder combinators such as @{term


1139 
map}, @{term filter} etc.

23805

1140 
As an example, imagine a datatype of nary trees:

23003

1141 
*}


1142 


1143 
datatype 'a tree =


1144 
Leaf 'a


1145 
 Branch "'a tree list"


1146 


1147 


1148 
text {* \noindent We can define a map function for trees, using the predefined


1149 
map function for lists. *}

22065

1150 

23003

1151 
function treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"


1152 
where


1153 
"treemap f (Leaf n) = Leaf (f n)"


1154 
 "treemap f (Branch l) = Branch (map (treemap f) l)"


1155 
by pat_completeness auto

22065

1156 


1157 
text {*

23003

1158 
We do the termination proof manually, to point out what happens


1159 
here:


1160 
*}


1161 


1162 
termination proof


1163 
txt {*


1164 


1165 
As usual, we have to give a wellfounded relation, such that the


1166 
arguments of the recursive calls get smaller. But what exactly are


1167 
the arguments of the recursive calls? Isabelle gives us the


1168 
subgoals


1169 


1170 
@{subgoals[display,indent=0]}


1171 


1172 
So Isabelle seems to know that @{const map} behaves nicely and only


1173 
applies the recursive call @{term "treemap f"} to elements


1174 
of @{term "l"}. Before we discuss where this knowledge comes from,


1175 
let us finish the termination proof:


1176 
*}


1177 


1178 
show "wf (measure (size o snd))" by simp


1179 
next


1180 
fix f l and x :: "'a tree"


1181 
assume "x \<in> set l"


1182 
thus "((f, x), (f, Branch l)) \<in> measure (size o snd)"


1183 
apply simp


1184 
txt {*


1185 
Simplification returns the following subgoal:


1186 

23805

1187 
@{text[display] "1. x \<in> set l \<Longrightarrow> size x < Suc (tree_list_size l)"}

23003

1188 


1189 
We are lacking a property about the function @{const


1190 
tree_list_size}, which was generated automatically at the


1191 
definition of the @{text tree} type. We should go back and prove


1192 
it, by induction.


1193 
*}

23805

1194 
(*<*)oops(*>*)

23003

1195 


1196 
lemma tree_list_size[simp]: "x \<in> set l \<Longrightarrow> size x < Suc (tree_list_size l)"


1197 
by (induct l) auto


1198 


1199 
text {*


1200 
Now the whole termination proof is automatic:


1201 
*}


1202 


1203 
termination


1204 
by lexicographic_order

22065

1205 


1206 

23003

1207 
subsection {* Congruence Rules *}


1208 


1209 
text {*


1210 
Let's come back to the question how Isabelle knows about @{const


1211 
map}.


1212 


1213 
The knowledge about map is encoded in socalled congruence rules,


1214 
which are special theorems known to the \cmd{function} command. The


1215 
rule for map is


1216 


1217 
@{thm[display] map_cong}


1218 


1219 
You can read this in the following way: Two applications of @{const


1220 
map} are equal, if the list arguments are equal and the functions


1221 
coincide on the elements of the list. This means that for the value


1222 
@{term "map f l"} we only have to know how @{term f} behaves on


1223 
@{term l}.


1224 


1225 
Usually, one such congruence rule is


1226 
needed for each higherorder construct that is used when defining


1227 
new functions. In fact, even basic functions like @{const

23805

1228 
If} and @{const Let} are handled by this mechanism. The congruence

23003

1229 
rule for @{const If} states that the @{text then} branch is only


1230 
relevant if the condition is true, and the @{text else} branch only if it


1231 
is false:


1232 


1233 
@{thm[display] if_cong}


1234 


1235 
Congruence rules can be added to the


1236 
function package by giving them the @{term fundef_cong} attribute.


1237 

23805

1238 
The constructs that are predefined in Isabelle, usually


1239 
come with the respective congruence rules.


1240 
But if you define your own higherorder functions, you will have to

23003

1241 
come up with the congruence rules yourself, if you want to use your

23805

1242 
functions in recursive definitions.


1243 
*}


1244 


1245 
subsection {* Congruence Rules and Evaluation Order *}


1246 


1247 
text {*


1248 
Higher order logic differs from functional programming languages in

