Email Gateway (Aug 17 2022 at 13:26): Email Gateway (Aug 17 2022 at 13:26):From: Tom Melham <Tom.Melham@comlab.ox.ac.uk>
Dear Martin,
I don't read the Isabelle mailing list, but someone forwarded your
query about developing my theory of temporal abstraction operators in
Isabelle. I can't help with Isabelle, but did dig up the original HOL
proofs - which are in the attached compressed tarfile. I hope the
sequence of lemmas, at least, is of some help.
I recall that a use of the Well Ordering Property for the naturals was
crucial in the proofs. This property ('WOP') is equivalent to
induction and is proved in the standard HOL prelude. I'm not sure if
it's available in Isabelle, but it isn't hard to prove.
Best wishes,
Tom
temporal.tar.gz
Last updated: May 03 2024 at 12:27 UTC