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