NameDateSize

..25-Jul-201921

dffScript.smlH A D25-Jul-20193.8 KiB

nextScript.smlH A D25-Jul-20193.3 KiB

READMEH A D25-Jul-20191 KiB

stableScript.smlH A D25-Jul-20192 KiB

tempabsScript.smlH A D25-Jul-201925.6 KiB

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