### Termination of Isabelle Functions via Termination of Rewriting

#### Introduction

The most popular instance of the generic proof assistant Isabelle is its instantiation to higher-order logic (Isabelle/HOL). The system provides a convenient functional programming layer having datatypes and recursive functions with pattern-matching. A necessary restriction for newly defined functions is that they are terminating. Otherwise a defining equation like

```
f x = f x + 1
```

would easily lead to inconsistency. There are already some built-in means to prove termination of functions automatically in some cases. However, by exploiting IsaFoR and devising suitable tactics to reduce termination of an Isabelle/HOL function to termination of a constructed term rewrite system, we are able to use external termination tools in order to prove termination of user-defined functions. In the following we demonstrate the usage of our approach by example. (A description of the internal construction is contained in a recently submitted paper.)

Note: We describe a prototype implementation and assume basic Isabelle knowledge.

#### Usage

If you want to use our approach in your own Isabelle/HOL theory, you have
to base it on `TermFun.thy`

(which is part of IsaFoR) as
follows:

```
theory MyTheory imports TermFun begin
```

Note: Since the new commands `define_trs`

and
`export_termination_problem`

are provided, you
also have to update your keyword file when using Proof-General (an
appropriate `isar-keywords.el`

file is included in IsaFoR).

Now, the typical situation is that you define some new function that is not proved to be terminating automatically. We give two examples illustrating the usage of our approach in the following.

##### A First Example

The first example is a function `remdups`

removing duplicates
from a binary search tree.
For quick reference, we first present `remdups`

and its
termination proof, then we explain the single steps of the proof in more
detail, and finally, we give auxiliary definitions of datatypes and
functions.

###### Proving Termination of `remdups`

```
1 function remdups where
2 "remdups E = E"
3 | "remdups (N l x r) = N (remdups (del x l)) x (remdups (del x r))"
4 by pat_completeness auto
5
6 setup {* Term_Fun.register_datatypes ["Bin_Tree.tree"] *}
7 define_trs getmax.simps
8 define_trs delmax.simps
9 define_trs del.simps
10 define_trs (no_sim) remdups.psimps
11
12 termination remdups
13 apply (trs_reduce remdups)
14 apply (simp only: all_trs_defs set_list_conv)
15 export_termination_problem "remdups.xml"
16 apply (ceta_import_proof "remdups.proof.xml")
17 apply ceta_eval
18 done
```

###### Detailed Description

Since the datatype `tree`

is user-defined, we have to tell the
system that it should provide a first-order term representation for it,
which is done in line 6.

The four `define_trs`

commands in lines 7 to 10, generate term
rewrite systems (TRSs) for all involved functions. Note the attribute
`(no_sim)`

in the last command, which prevents the system from
proving the simulation lemma of `remdups`

, since this would
require termination (consult the paper for more details). The result are
the four TRSs (as HOL values)
`getmax.trs`

,
`delmax.trs`

,
`del.trs`

, and
`remdups.trs`

. Every TRS for a function `f`

has the
name `f.trs`

and the definition (i.e., defining equation of
`f.trs`

) `f.trs_def`

.

Line 13 takes care of reducing the termination proof obligation for
`remdups`

to termination of `f.trs`

. A major part of
our paper describes this process in more detail.

In line 14 the TRS is brought in a form that facilitates the XML export in
the next line, that is, the set of rules is explicitly transformed into a
finite list of rules. The command of line 15, creates the file
`remdups.xml`

in the current directory which contains an XML
encoding (using the XML format of the termination competition) of the
`remdups`

TRS.

At this point, we can use an arbitray termination tool which supports
the
CPF format
to proof termination of the generated TRS.
(Special versions of
AProVE
and
TTT2 that can be used to produce the
necessary certificates are available for download.)
We assume that the result is
saved to the file `remdups.proof.xml`

.

In line 16 the XML certificate is parsed into Isabelle/HOL and certified by CeTA's check-function in line 17. This concludes the proof.

###### Auxiliary Datatypes and Functions

The function `remdups`

is based on the following user-defined
datatype and auxiliary functions:

```
datatype tree = E | N tree nat tree
fun getmax where
"getmax E = 0"
| "getmax (N l x E) = x"
| "getmax (N l x r) = getmax r"
fun delmax where
"delmax E = E"
| "delmax (N l x E) = l"
| "delmax (N l x r) = N l x (delmax r)"
fun del where
"del x E = E"
| "del x (N E y r) =
(if x < y then (N E y r)
else if eq x y then del x r
else N E y (del x r))"
| "del x (N l y r) =
(if x < y then N (del x l) y r
else if x > y then N l y (del x r)
else N (delmax (del x l)) (getmax (del x l)) (del x r))"
```

##### A Second Example

Assume you wanted to define the function```
fun evenodd :: "bool => nat => bool"
where
"evenodd True 0 = False " |
"evenodd False x = (~ evenodd True x)" |
"evenodd True (Suc x) = evenodd False x"
```

resulting in an error-message ending with something like
```
*** Could not find lexicographic termination order.
*** At command "fun" (line 3 of "MyTheory.thy")
```

Thus we tell the system that we want to switch to "expert-mode" and prove
termination manually by using `function`

instead of
`fun`

and proving the completeness of the involved patterns as
follows
```
function evenodd :: "bool => nat => bool"
where
"evenodd True 0 = False " |
"evenodd False x = (~ evenodd True x)" |
"evenodd True (Suc x) = evenodd False x"
by (pat_completeness) auto
```

We now have the partial simplification rules `evenodd.psimps`

```
evenodd_dom (True, 0) ==> evenodd True 0 = False
evenodd_dom (False, ?x) ==> evenodd False ?x = (~ evenodd True ?x)
evenodd_dom (True, Suc ?x) ==> evenodd True (Suc ?x) = evenodd False ?x
```

whose shape indicates that termination is still missing (every equation has
the precondition that `evenodd`

is defined on the corresponding
input).

The next step is to obtain a term rewrite system, representing the function
`evenodd`

. Since this function uses `~`

(Isabelle/HOL's logical negation) we further need a TRS representation of
negation. Both can be obtained as follows

```
define_trs not_True_eq_False not_False_eq_True
define_trs (no_sim) evenodd.psimps
```

where the `no_sim`

suppresses the generation of so called
simulation lemmas (consult the paper for further information). Internally,
the following TRS was constructed (using the ASCII format of the
termination competition):

```
(VAR x)(RULES
Not(True) -> False
Not(False) -> True
evenodd(True, 0) -> False
evenodd(False, x) -> Not(evenodd(True, x))
evenodd(True, Suc(x)) -> evenodd(False, x)
)
```

which is available under the name `evenodd.trs_def`

.
Now, to prove termination of `evenodd`

, we first reduce the
termination obligation produced by Isabelle/HOL, to termination of the
above TRS, using our `trs_reduce`

method.

```
termination evenodd
apply (trs_reduce evenodd)
apply (simp only: all_trs_defs set_list_conv)
```

where `all_trs_defs`

is a theorem containing all defined TRSs
and `set_list_conv`

is used to transform finite sets into lists.
Afterward we export the resulting termination problem of
`evenodd.trs`

to an external XML file (using the XML format of
the termination competition).

```
export_termination_problem "evenodd.xml"
```

An arbitrary termination tool (which has to support the
CPF format) can
now be used to produce a termination proof in the file
`evenodd.proof.xml`

, which is parsed into Isabelle/HOL in turn.
```
apply (ceta_import_proof "evenodd.proof.xml")
```

Finally, the proof is certified inside Isabelle/HOL and we are done.
```
apply (ceta_eval)
done
```

All of these steps remain to be integrated in a more user-friendly interface in the future.