## Stream: Beginner Questions

### Topic: Unfinished termination proof allows to finish proof

#### Robert Soeldner (Jun 23 2021 at 13:21):

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?

#### Mathias Fleury (Jun 23 2021 at 13:23):

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

#### Mathias Fleury (Jun 23 2021 at 13:23):

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

#### Mathias Fleury (Jun 23 2021 at 13:23):

So: yes this is expected.

#### Mathias Fleury (Jun 23 2021 at 13:25):

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`

#### Manuel Eberl (Jun 23 2021 at 13:26):

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.

#### Robert Soeldner (Jun 23 2021 at 13:34):

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?

#### Mathias Fleury (Jun 23 2021 at 13:36):

termination has to prove all goals.

#### Robert Soeldner (Jun 23 2021 at 13:42):

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?

#### Jakub Kądziołka (Jun 23 2021 at 13:43):

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

Last updated: Aug 13 2022 at 05:18 UTC