Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Reusing termination order found by lexicograph...


view this post on Zulip Email Gateway (Aug 22 2022 at 18:54):

From: Mark Wassell <mpwassell@gmail.com>
Hello,

I have a set of mutually recursive functions for which the
lexicographic_order method takes a long time to process. When it does
finish, it prints out a termination order.

Is there a way to make use of the found termination order to shorten the
re-processing of the theory file when I make changes that wouldn't affect
the termination proof?

I have tried to do proof(relation <termination order>) and some of the
goals are easy to prove uniformly (with wf_mlex, mlex_less and auto) but
some of the goals need individual attention (and there are a lot of them).

Cheers

Mark


Last updated: Mar 28 2024 at 08:18 UTC