I'm trying to prove termination of a partial function. I've read `functions.pdf`

, but I can't figure out a nice way to do exactly what I'm looking for. Ideally, I'd like to be able to provide an “expected” domain to some tactic, and then be required to prove that

- recursive calls stay within that expected domain
**and** - show that some provided measure decreases on each recursive call, as with the
`relation`

method.

Background info: The function in my use case is a tail-recursive variant of

`Tree.subtrees`

that returns a`'a tree list`

, and which has been compiled (for lack of a better word) to use`nat`

as an argument & return type. The termination of the non-encoded version can't be shown by`fun`

, but there's a somewhat simple measure that works with`relation`

. Because of this, my gut feeling is that I should use`relation`

to prove termination of the encoded variant. However, when arguments that don't represent valid`'a tree`

or`'a tree list`

values under the encoding are passed in, the function might not actually terminate.

Isabelle examples of what I'm looking for

Does anyone here have pointers for next steps? Am I missing something obvious? I've tried staring at the definition of `relation`

itself, but that just made my eyes glaze over :)

One way to deal with "partial" functions I've seen and used myself is to use conditional equations. I'm not going to refer to your given example, since you could just split your patterins into `Suc 0`

and `Suc (Suc n)`

to achieve the same effect. Instead I'll try to give you hints for your actual use-case:

I imagine you have some kind of (inductive) definition of which naturals encode a tree.

```
definition is_tree :: "nat ⇒ bool" where
"is_tree n ≡ True"
```

You can then use that predicate to "restrict" your function to your desired domain.

```
function subtrees' :: "nat ⇒ nat" where
"subtrees' n = undefined" if "is_tree n" ― ‹definition for wellformed input›
| "subtrees' n = undefined" if "¬is_tree n" ― ‹some dummy value for inputs outside your domain›
by auto
```

You can then (hopefully) proceed with your termination proof using relation again (depending on how your actual definition of `subtrees'`

looks). The conditional equations should then give you your required assumptions in the specific cases.

```
termination subtrees'
apply (relation "(λx. x) <*mlex*> {}")
...
```

Since the function is tail recursive, I propose you use the partial_function command. It is much nicer to deal with than the domain predicate generated by the function package.

Take a look at the induction pcpl and other thms it produces, and see if they are usable.

Thanks for the replies!

~~Both the ~~ Found `… if "n ∈ …"`

and `partial_function`

approaches seem to have the drawback that code equations aren't generated by Isabelle. This is really unfortunate — am I missing something obvious here?`[code]:`

, that seems to work fine.

The restricted `function`

version certainly expects me to prove things that look much better than before when using `relation`

. I'm not super excited about having to deal with weirder (or more!) simp rules, but it might be manageable. Regardless, I tried out Mohammad's suggestion first since I'm trying to avoid changing the generated code :)

`partial_function`

's induction scheme certainly doesn't look fun. However, I managed to avoid it completely for a correctness lemma for the generated function, using the original (non-partial and non-encoded) function's induction scheme instead. I had to add an additional conclusion, namely that the generated function's result is a valid encoding—this is needed as an IH.

If I understand this correctly, then, is proving an equation like `subtreest' abc = encode (subtreest (decode (abc)))`

(simplified for sake the of this question) sufficient to convince isabelle that `subtreest'`

terminates on input `abc`

? I'm not sure how much that HOL equality actually means—`undefined`

still makes me nervous :) I did find Manuel's post on stackoverflow here as an explanation of `undefined`

in general, but this still feels wrong as an approach to proving function termination.

No, partial_function, by definition, gives you a function that does not necessarily terminate on all inputs. This means that the correctness theorem you prove is only for the inputs on which it terminates. Hence it is called partial correctness. That thm should have the assumption characterising the domain on which it termiantes, however.

Also, your approach of using the original function's IH is the right one, at least in my experience of using partial_function.

This means that the correctness theorem you prove is only for the inputs on which it terminates.

I understand this, and in my case, the argument domain is implicitly restricted by the encode functions wrapped around `subtrees'`

arguments in the lemma statement. I guess what I'm wondering is whether the partial correctness proof is “all I need” to prove partial termination. Maybe this stems from a misunderstanding on my side of the definition of termination in Isabelle.

Yes, that is all you need. The proof of termination is inherent in the induction principle coming from the original function.

Note that you can also call `function`

with the option `(domintros)`

. That gives you a bunch of rules that allow you to reason explicitly about the domain of the function.

I think that is what he wants to avoid since he already has a termination proof for a function that does the same recursion as the partial function.

Johannes Neubrand has marked this topic as resolved.

Last updated: Dec 07 2023 at 08:19 UTC