[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,

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

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