1% This example isn't finished %
2
3%============================================================================%
4% The example proof in this file comes from the paper "Traces for Hardware   %
5% Verification" by Roger Stokes of ICL.                                      %
6%============================================================================%
7
8new_theory `trace_counter`;;
9
10new_prim_rec_definition
11 (`COUNTER`,
12  "(COUNTER 0 reset out = T) /\
13   (COUNTER (SUC m) reset out =
14    ((m=0) \/
15     ((out(SUC m) = ((reset m=0) => 0 | (out m)+1)) /\
16      COUNTER m reset out)))");;
17
18new_prim_rec_definition
19 (`INIT`,
20  "(INIT 0 reset p1 p2 = T) /\
21   (INIT(SUC m) reset p1 p2 =
22    (p2(SUC m) = ((reset(SUC m)=1) => 0 | p1(SUC m))) /\
23    INIT m reset p1 p2)");;
24
25new_prim_rec_definition
26 (`INC`,
27  "(INC 0 out p1 = T) /\
28   (INC (SUC m) out p1 =
29    (p1(SUC m) = out(SUC m)+1) /\
30    INC m out p1)");;
31
32new_prim_rec_definition
33 (`DEL`,
34  "(DEL 0 p2 (out:num->*) = T) /\
35   (DEL (SUC m) p2 out =
36    (m = 1) \/
37    ((out(SUC m) = p2 m) /\
38     DEL m p2 out))");;
39
40
41let COUNTER = theorem `trace_counter` `COUNTER`
42and INIT    = theorem `trace_counter` `INIT`
43and INC     = theorem `trace_counter` `INC`
44and DEL     = theorem `trace_counter` `DEL`;;
45
46prove_thm
47 (`Correctness`,
48  "!m reset out p1 p2.
49    INIT m reset p1 p2 /\
50    DEL m p2 out       /\
51    INC m out p1
52    ==>
53    COUNTER m reset out",
54   INDUCT_TAC
55    THEN REPEAT GEN_TAC
56    THEN ASM_REWRITE_TAC[COUNTER;INIT;INC;DEL]);;
57
58
59prove_thm
60 (`Termination`,
61  "!m. ?reset out p1 p2.
62    INIT m reset p1 p2 /\
63    DEL m p2 out       /\
64    INC m out p1",
65   INDUCT_TAC
66    THEN REPEAT GEN_TAC
67    THEN ASM_REWRITE_TAC[COUNTER;INIT;INC;DEL]);;
68