Hi,

I have a mutual recursive function defined using

```
function (sequential) ...
by pat_completeness auto
termination by lexicographic_order
```

where by the termination proof fails with unfinished subgoals. With this definition (incl. the unfinished proof goals), I'm able to proof a lemma using the simplifier, without the termination proof it fails. Is this an expected behavior?

without termination, all simp rules are of the form "x in the terminating domain ==> f x = ..."

With termination, the "termination domain" covers all values.

So: yes this is expected.

For the sake of an example:

`f x = (if x >= 0 then x * (f (x-1)) else f x + 1`

This is terminating for `x >= 0`

, but you cannot use the simplification rule because the definition is not looping for `x < 0`

Also, in the interactive mode in Isabelle/jEdit, proofs are checked in parallel and you can use a result before its proof has been checked. In particular, you can use a result even if the proof failed.

Mathias Fleury said:

without termination, all simp rules are of the form "x in the terminating domain ==> f x = ..."

Does this mean, the unfinished subgoals will be excluded from the simp rules but I'm able to use the proven ones?

termination has to prove all goals.

Thank you, I will re-read few sections in https://isabelle.in.tum.de/doc/functions.pdf . Is there a way of showing, which steps the simplifier has used?

you can do `using [[simp_trace_new]] by simp`

Last updated: Sep 25 2022 at 23:25 UTC