1% The Counter Example using "temporal" operators %
2
3new_theory `COUNT`;;
4
5let time = ":num"
6and val  = ":num";;
7
8let sig = ":^time -> ^val";;
9
10new_definition
11 (`DEL`, "DEL(x:^sig,x':^sig) = !t. x t = x'(t-1)");;
12
13new_definition(`INC`, "(INC:^sig->^sig) x = \t. (x t)+1");;
14
15new_definition
16 (`COUNT_SPEC`,
17  "COUNT_SPEC (sw,i,o) = DEL(o,(sw -> i | INC o))");;
18
19% The primitives: MUX, REG and INCR %
20
21new_definition
22 (`MUX`,
23  "MUX(switch,i1:^sig,i2:^sig,o:^sig) = (o = (switch -> i1 | i2))");;
24
25new_definition
26 (`REG`,
27  "REG (i:^sig,o:^sig) = DEL(o,i)");;
28
29new_definition
30 (`INCR`,
31  "INCR(i:^sig,o:^sig) = (o = INC i)");;
32
33new_definition
34 (`COUNT_IMP`,
35  "COUNT_IMP (sw,i,o) = ?l1 l2. 
36                         MUX (sw,i,l2,l1) /\
37                         REG (l1,o)       /\
38                         INCR (o,l2)");;
39
40let COUNT_SPEC = definition `COUNT` `COUNT_SPEC`
41and COUNT_IMP  = definition `COUNT` `COUNT_IMP`;;
42
43let MUX  = definition `COUNT` `MUX`
44and REG  = definition `COUNT` `REG`
45and INCR = definition `COUNT` `INCR`;;
46
47
48let prims = [MUX;REG;INCR];;
49
50let th1 = UNFOLD_RULE prims COUNT_IMP;;
51
52let th2 = OLD_UNWIND_RULE th1;;
53
54let th3 = PRUNE_RULE th2;;
55
56let EXPAND thl th =
57 let th1 = UNFOLD_RULE thl th
58 in
59 let th2 = OLD_UNWIND_RULE th1
60 in
61 PRUNE_RULE th2;;
62
63let COUNT_CORRECTNESS =
64 prove_thm
65  (`COUNT_CORRECTNESS`,
66   "COUNT_SPEC(sw,i,o) = COUNT_IMP(sw,i,o)",
67   REWRITE_TAC[COUNT_SPEC;EXPAND prims COUNT_IMP]);;
68