Stream: Archive Mirror: Isabelle Users Mailing List

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

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: Nov 21 2024 at 12:39 UTC