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