1% PROOF : Transistor Implementation of a Counter % 2% FILE : incn.ml % 3% % 4% DESCRIPTION : Connect carry-in line of n-bit halfadder to Vdd to % 5% make a n-bit increment circuit and derives its % 6% behaviour in terms of addition modulo (2 EXP n). % 7% % 8% AUTHOR : J.Joyce % 9% DATE : 1 April 1987 % 10 11new_theory `incn`;; 12 13loadt `misc`;; 14loadt `types`;; 15 16new_parent `mod`;; 17new_parent `halfaddn`;; 18 19let INCn_IMP = new_definition ( 20 `INCn_IMP`, 21 "INCn_IMP n (i:^bus,o:^bus) = 22 ?cin cout. HALFADDn_IMP n i cin o cout /\ Vdd cin");; 23 24let Vdd = definition `mos` `Vdd`;; 25let Def = definition `dataabs` `Def`;; 26let BoolVal = definition `dataabs` `BoolVal`;; 27let WordVal = theorem `dataabs` `WordVal`;; 28 29let MOD_THM = theorem `mod` `MOD_THM`;; 30let BoolAbs_THM = theorem `dataabs` `BoolAbs_THM`;; 31let HALFADDn_CORRECT = theorem `halfaddn` `HALFADDn_CORRECT`;; 32 33let lemma1 = TAC_PROOF ( 34 ([],"!w. Vdd w ==> !t. Def (w t) /\ (BoolVal (BoolAbs (w t)) = 1)"), 35 PURE_REWRITE_TAC [Vdd] THEN 36 REPEAT STRIP_TAC THEN 37 ASM_REWRITE_TAC [Def;BoolVal;BoolAbs_THM]);; 38 39let lemma2 = 40 GEN_ALL 41 (PURE_REWRITE_RULE [MULT_CLAUSES;ADD_CLAUSES] 42 (SPECL ["m";"n";"0"] MOD_THM));; 43let lemma3 = 44 GEN_ALL 45 (PURE_REWRITE_RULE [MULT_CLAUSES] (SPECL ["m";"n";"1"] MOD_THM));; 46 47let th1 = TAC_PROOF ( 48 ([],"1 < 2"), 49 SUC_FORM_TAC THEN REWRITE_TAC [LESS_SUC_REFL]);; 50 51let th2 = TAC_PROOF ( 52 ([],"0 < 2"), 53 SUC_FORM_TAC THEN REWRITE_TAC [LESS_0]);; 54 55let th3 = (DEPTH_CONV (REWRITE_CONV (num_CONV "2"))) "2 * a";; 56 57let th4 = 58 GEN_ALL 59 (SUBS [SPECL ["m";"p"] ADD_SYM;SPECL ["n";"p"] ADD_SYM] 60 (SPEC_ALL LESS_MONO_ADD_EQ));; 61 62let th5 = TAC_PROOF ( 63 ([],"!m n p. m < n ==> m < n + p"), 64 GEN_TAC THEN GEN_TAC THEN 65 INDUCT_TAC THEN 66 REWRITE_TAC [ADD_CLAUSES] THEN 67 DISCH_TAC THEN 68 RES_TAC THEN 69 IMP_RES_TAC LESS_SUC);; 70 71let th6 = TAC_PROOF ( 72 ([],"!n w. WordVal n (w:^word) < 2 EXP (SUC n)"), 73 REPEAT GEN_TAC THEN 74 SPEC_TAC ("n","n") THEN 75 PURE_REWRITE_TAC [EXP] THEN 76 INDUCT_TAC THENL 77 [PURE_REWRITE_TAC [WordVal;EXP;MULT_CLAUSES] THEN 78 BOOL_CASES_TAC "(w:^word) 0" THEN 79 REWRITE_TAC [BoolVal;th1;th2]; 80 PURE_REWRITE_TAC [WordVal;MULT_CLAUSES;th3] THEN 81 BOOL_CASES_TAC "(w:^word) (SUC n)" THENL 82 [ASM_REWRITE_TAC [EXP;BoolVal;MULT_CLAUSES;th4]; 83 REWRITE_TAC [EXP;BoolVal;MULT_CLAUSES;ADD_CLAUSES] THEN 84 IMP_RES_TAC 85 (SPECL ["WordVal n w";"2 * (2 EXP n)";"2 * (2 EXP n)"] th5)]]);; 86 87let th7 = ASSUME 88 "((2 EXP (SUC n)) * (BoolVal(BoolAbs(cout t)))) + 89 (WordVal n(WordAbs(o t))) = 90 (WordVal n(WordAbs(i t))) + (BoolVal(BoolAbs(cin t)))";; 91 92let th8 = SUBS [ASSUME "BoolVal(BoolAbs (cin t)) = 1"] th7;; 93 94let th9 = MATCH_MP lemma2 (SPECL ["n";"(WordAbs (o t)):^word"] th6);; 95let th10 = MATCH_MP lemma3 (SPECL ["n";"(WordAbs (o t)):^word"] th6);; 96 97let INCn_CORRECT = prove_thm ( 98 `INCn_CORRECT`, 99 "!n i o. 100 INCn_IMP n (i:^bus,o:^bus) 101 ==> 102 !t. 103 Defn n (i t) ==> 104 Defn n (o t) /\ 105 (WordVal n (WordAbs (o t)) = 106 (((WordVal n (WordAbs (i t))) + 1) MOD (2 EXP (SUC n))))", 107 PURE_REWRITE_TAC [INCn_IMP] THEN 108 REPEAT STRIP_TAC THEN 109 HOL_IMP_RES_THEN (STRIP_ASSUME_TAC o (SPEC "t")) lemma1 THEN 110 IMP_RES_TAC HALFADDn_CORRECT THEN 111 RES_TAC THEN 112 SUBST1_TAC (SYM th8) THEN 113 BOOL_CASES_TAC "BoolAbs (cout t)" THEN 114 REWRITE_TAC [BoolVal;MULT_CLAUSES;ADD_CLAUSES] THENL 115 [ACCEPT_TAC th10; ACCEPT_TAC th9]);; 116 117close_theory ();; 118