1% PROOF : Transistor Implementation of a Counter % 2% FILE : toplevel.ml % 3% % 4% DESCRIPTION : Top-level implementation using the counter and % 5% some I/0 devices. % 6% % 7% AUTHOR : J.Joyce % 8% DATE : 1 April 1987 % 9 10new_theory `toplevel`;; 11 12loadt `misc`;; 13loadt `types`;; 14 15new_parent `count`;; 16 17let BUTTON = new_definition ( 18 `BUTTON`, 19 "BUTTON (g:^wire,i:^boolsig,o:^wire) = 20 (!t. Def ((o when (isHi g)) t)) /\ 21 (!t. (i t = BoolAbs ((o when (isHi g)) t)))");; 22 23let SWITCHES = new_definition ( 24 `SWITCHES`, 25 "SWITCHES n (g:^wire,i:^numsig,o:^bus) = 26 (!t. Defn n ((o when (isHi g)) t)) /\ 27 (!t. (i t = WordVal n (WordAbs ((o when (isHi g)) t))))");; 28 29let DISPLAY = new_definition ( 30 `DISPLAY`, 31 "DISPLAY n (g:^wire,i:^bus,o:^numsig) = 32 !t. 33 Defn n ((i when (isHi g)) t) ==> 34 (o t = WordVal n (WordAbs ((i when (isHi g)) t)))");; 35 36let DEVICE_IMP = new_definition ( 37 `DEVICE_IMP`, 38 "DEVICE_IMP n (button:^boolsig,switches:^numsig,display:^numsig) = 39 ?phiA w1 b1 b2. 40 BUTTON (phiA,button,w1) /\ 41 SWITCHES n (phiA,switches,b1) /\ 42 DISPLAY n (phiA,b2,display) /\ 43 COUNT_IMP n (phiA,w1,b1,b2) /\ 44 isBus n b1 /\ 45 isBus n b2");; 46 47let Def_DISJ_CASES = theorem `dataabs` `Def_DISJ_CASES`;; 48let BoolAbs_THM = theorem `dataabs` `BoolAbs_THM`;; 49let COUNT_CORRECT = theorem `count` `COUNT_CORRECT2`;; 50 51let LESS_OR_EQ_ADD = TAC_PROOF( 52 ([],"!m n. m <= n = (?p. p + m = n)"), 53 REPEAT GEN_TAC THEN 54 EQ_TAC THENL 55 [PURE_REWRITE_TAC [LESS_OR_EQ] THEN 56 REPEAT STRIP_TAC THENL 57 [IMP_RES_TAC LESS_ADD; 58 EXISTS_TAC "0" THEN ASM_REWRITE_TAC [ADD_CLAUSES]]; 59 REPEAT STRIP_TAC THEN 60 FIRST_ASSUM (SUBST1_TAC o SYM) THEN 61 SUBST1_TAC (SPECL ["p";"m"] ADD_SYM) THEN 62 REWRITE_TAC [LESS_EQ_ADD]]);; 63 64let ASSUM_LIST_SPEC_TAC tm = 65 ASSUM_LIST (MAP_EVERY 66 (\thm. 67 if not (is_forall (concl thm)) then ALL_TAC 68 else let var = fst (dest_forall (concl thm)) in 69 if not (type_of tm = type_of var) then ALL_TAC 70 else ASSUME_TAC (SPEC tm thm) ? 71 failwith `ASSUM_LIST_SPEC_TAC`));; 72 73let lemma1 = TAC_PROOF (( 74 [], 75 "!w t. 76 Def (w t) ==> (b t = BoolAbs (w t)) ==> (b t = T) ==> (w t = Hi)"), 77 REPEAT GEN_TAC THEN 78 DISCH_THEN (STRIP_THM_THEN SUBST1_TAC o(MATCH_MP Def_DISJ_CASES)) THEN 79 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC [BoolAbs_THM]);; 80 81let lemma2 = 82 GEN_ALL 83 (SUBS [SPECL ["m";"n"] ADD_SYM] (SPECL ["m";"n"] LESS_EQ_ADD));; 84 85let th1 = CONJUNCT1 (CONJUNCT2 (CONJUNCT2 ADD_CLAUSES));; 86let th2 = (DEPTH_CONV (REWRITE_CONV th1)) "((SUC n') + sysinit)";; 87let th3 = SYM (TRANS th2 ((REWRITE_CONV ADD1) (rhs (concl th2))));; 88let th4 = ASSUME 89 "display((n' + sysinit) + 1) = 90 WordVal n(WordAbs((b2 when (isHi phiA))((n' + sysinit) + 1)))";; 91let th5 = SUBS [th3] th4;; 92 93let TOPLEVEL_CORRECT = prove_thm ( 94 `TOPLEVEL_CORRECT`, 95 "!n. 96 let max = 2 EXP (n + 1) in 97 !button switches display sysinit. 98 DEVICE_IMP n (button,switches,display) /\ 99 (button sysinit = T) 100 ==> 101 !t. sysinit <= t ==> 102 (display (t + 1) = 103 button t => switches t | (((display t) + 1) MOD max))", 104 GEN_TAC THEN 105 SUBST1_TAC (SYM (SPEC "n" ADD1)) THEN 106 PURE_REWRITE_TAC [LET_DEF;DEVICE_IMP;BUTTON;SWITCHES;DISPLAY] THEN 107 BETA_TAC THEN 108 REPEAT GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN 109 PURE_REWRITE_TAC [LESS_OR_EQ_ADD] THEN 110 DISCH_THEN (STRIP_THM_THEN (SUBST1_TAC o SYM)) THEN 111 ASSUM_LIST_SPEC_TAC "sysinit" THEN 112 IMP_RES_TAC lemma1 THEN 113 DISJ_CASES_THENL 114 [SUBST1_TAC;STRIP_THM_THEN SUBST1_TAC] (SPEC "p" num_CASES) THENL 115 [PURE_REWRITE_TAC [ADD_CLAUSES] THEN 116 ASSUME_TAC (SPEC "sysinit" LESS_EQ_REFL) THEN 117 IMP_RES_TAC COUNT_CORRECT THEN 118 RES_TAC THEN 119 ASM_REWRITE_TAC [BoolAbs_THM]; 120 ASSUME_TAC (SPECL ["sysinit";"n'"] lemma2) THEN 121 ASSUME_TAC (SPECL ["sysinit";"SUC n'"] lemma2) THEN 122 IMP_RES_TAC COUNT_CORRECT THEN 123 RES_TAC THEN 124 ASM_REWRITE_TAC [] THEN 125 SUBST1_TAC th5 THEN 126 ASM_REWRITE_TAC []]);; 127 128close_theory ();; 129