Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Calling size_change automatically when lexicog...

view this post on Zulip Email Gateway (Aug 22 2022 at 15:34):

From: Tobias Nipkow <nipkow@in.tum.de>
The reason for not trying size change termination automatically: size change
termination is much more heavweight: you pull in more libraries and the
algorithm is more complex (probably PSPACE complete).

Tobias
smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 15:35):

From: Sebastiaan Joosten <sjcjoosten@gmail.com>
Hi Dominic,

It seems that one reason not to call any method automatically after lexicographic_order fails, is that this would hide the rather nice error message that lexicographic_order offers. In fact, I have not been able to automatically call any method after lexicographic_order fails, as it seem to fail hard when producing the error message. I'm not 100% sure though, me not being able to do something might not (probably doesn't) mean that it's impossible.

To solve your problem, you might simply install size_change as the default termination prover (keeping in mind Tobias' explanation on why this might be a bad idea):

(* use size_change as default termination prover *)
ML ‹

val _ =
Theory.setup
(Context.theory_map (Function_Common.set_termination_prover
(K (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))))

›

fun foo where (* only works with size_change *)
"foo Nil (Cons x xs) = foo xs Nil" |
"foo (Cons x xs) y = foo y xs" |
"foo _ _ = Nil"

Best,

Sebastiaan

view this post on Zulip Email Gateway (Aug 22 2022 at 15:35):

From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Sebastian, Tobias,

Thanks for the explanation of why lexicographic_order is preferred
over size_change, and for the tip on changing the default termination
prover. That's very useful.

Thanks,
Dominic

Last updated: Nov 21 2024 at 12:39 UTC