An Isabelle/HOL Formalization of Rewriting
for Certified Tool Assertions

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