Robert Soeldner (Jun 23 2021 at 13:21): 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: Apr 26 2024 at 20:16 UTC