README
1===============================================================================
2== This directory contains HOL88 proofs due to Tom Melhan in 1987. They ==
3== were updated for HOL98 by Mike Gordon in 2000 for use in teaching at ==
4== OGI, and they still run in HOL4 (though the compiling preludes could ==
5== perhaps do with some updating). ==
6===============================================================================
7
8The definitions are:
9
10 tempabsTheory.Inf
11 |- !sig. Inf sig = !t. ?t'. t < t' /\ sig t'
12
13 tempabsTheory.when
14 |- !sig cntl. sig when cntl = sig o Timeof cntl
15
16 dffTheory.Rise
17 |- !s t. Rise s t = ~s t /\ s (t + 1)
18
19 dffTheory.Dtype
20 |- !ck d q.
21 Dtype (ck,d,q) = !t. q (t + 1) = (if Rise ck t then d t else q t)
22
23 dffTheory.Del
24 |- !inp out. Del (inp,out) = !t. out (t + 1) = inp t
25
26The theorem we need is:
27
28 dffTheory.Dtype_correct
29 |- !ck.
30 Inf (Rise ck) ==>
31 !d q. Dtype (ck,d,q) ==> Del (d when Rise ck,q when Rise ck)
32
33
34