[isabelle] Re: Hardware Modelling - Temporal Abstraction



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




Attachment: temporal.tar.gz
Description: application/tgz



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.