Email Gateway (Aug 17 2022 at 13:26): Email Gateway (Aug 17 2022 at 13:26):From: Martin Ellis <m.a.ellis@ncl.ac.uk>
Hi,
I've been trying to model sequential hardware based on
Tom Melham's "Higher Order Logic and Hardware Verification":
http://www.dcs.gla.ac.uk/~tfm/Papers/HVbook.html
The idea is that there is:
concrete time, could represent a gate delay, or a femto-second,
or whatever, it doesn't really matter as long as its units are longer
than abstract time units.
a predicate P t, which is true for every concrete time t for
which there is a corresponding abstract time
a relation Istimeof P n t, which is true iff P is true for the n'th time
at t.
a function Time of P n, which I think is either defined
Timeof P n == (SOME t. Istimeof P n t); or
Timeof P n == (THE t. Istimeof P n t)
Inf P is true iff P is True infinitely often: ALL t.EX t'. t' > t /\ P t'
0 1 < --- Abstract time
| \
0 1 2 3 4 <--- Concrete time
T F F T F <--- P
I've been trying to show Theorem 6.1 in the book
Inf P --> (EX! t. Istimeof P n t)
which Melham suggests is proved by showing existence ("by induction on n") and
uniqueness (also by induction on n) separately, but have two big problems.
Firstly, I don't seem to be able to do the induction step of the existence
part. I've attached my attempt...
Looking at the definitions, I thought complete induction (using
nat_less_induct) might be more appropriate - however I didn't get anywhere
at all using that...
Secondly, I can't figure out how to do the uniqueness part.
The file I've attached contains a simpler uniqueness proof, and I can't find
any examples that suggest how I might approach it.
(Actually, I read the "Advanced Induction Techniques" section in the tutorial,
but still can't quite get there)
You'll understand that this rather scuppers all proof attempts I've made.
(The other thing I don't understand is that, although I can't prove lemmas of
the form (Inf P) --> Q, and hence (ALL t. EX t'. t < t' /\ P t) --> Q,
I do seem to be able to prove those of the form
ALL t. EX t'. t < t' /\ P t --> Q, i.e. where the quantifiers scope over the
entire expression, including Q, rather than just the anticedent. The reason
I find this strange is because none of the quantified variables occur in Q.)
Can anyone suggest how to proceed? I've spent the best part of a fortnight
going around in circles. :o( Surely somebody has done this before, no?
Perhaps there are more appropriate constructs in Isabelle/HOL to model this?
Thanks
Martin
MelhamQ.thy
Last updated: Nov 21 2024 at 12:39 UTC