1% PROOF : Transistor Implementation of a Counter % 2% FILE : halfaddn.ml % 3% % 4% DESCRIPTION : Defines a CMOS half-adder circuit and uses this % 5% to construct a n-bit half-adder. % 6% % 7% The specification of the half-adder is based on the % 8% specification and proof of a full-adder reported in % 9% Cambridge University Computer Laboratory Technical % 10% Reports #77 (M.Gordon) and #91 (A.Camilleri,M.Gordon, % 11% and T.Melham). % 12% % 13% AUTHOR : J.Joyce % 14% DATE : 31 March 1987 % 15 16new_theory `halfaddn`;; 17 18loadt `misc`;; 19loadt `types`;; 20 21new_parent `gates`;; 22 23let HALFADD_IMP = new_definition ( 24 `HALFADD_IMP`, 25 "HALFADD_IMP (a:^wire,cin:^wire,sum:^wire,cout:^wire) = 26 AND_IMP (a,cin,cout) /\ XOR_IMP (a,cin,sum)");; 27 28let HALFADDn_IMP = new_prim_rec_definition ( 29 `HALFADDn_IMP`, 30 "(HALFADDn_IMP 0 (a:^bus) (cin:^wire) (sum:^bus) (cout:^wire) = 31 HALFADD_IMP (DEST_BUS a 0,cin,DEST_BUS sum 0,cout)) /\ 32 (HALFADDn_IMP (SUC n) a cin sum cout = 33 ?c. 34 HALFADDn_IMP n a cin sum c /\ 35 HALFADD_IMP (DEST_BUS a (SUC n),c,DEST_BUS sum (SUC n),cout))");; 36 37let Defn = theorem `dataabs` `Defn`;; 38let WordAbs = definition `dataabs` `WordAbs`;; 39let BoolVal = definition `dataabs` `BoolVal`;; 40let WordVal = theorem `dataabs` `WordVal`;; 41let DEST_BUS = definition `dataabs` `DEST_BUS`;; 42let and = definition `gates` `and`;; 43let xor = definition `gates` `xor`;; 44 45let val_not_eq_ax = axiom `mos` `val_not_eq_ax`;; 46 47let AND_CORRECT = theorem `gates` `AND_CORRECT`;; 48let XOR_CORRECT = theorem `gates` `XOR_CORRECT`;; 49 50let HALFADD_CORRECT = prove_thm ( 51 `HALFADD_CORRECT`, 52 "!i cin sum cout. 53 HALFADD_IMP (i,cin,sum,cout) 54 ==> 55 !t. 56 Def (i t) /\ Def (cin t) ==> 57 Def (sum t) /\ Def (cout t) /\ 58 ((2 * (BoolVal (BoolAbs (cout t)))) + 59 (BoolVal (BoolAbs (sum t))) = 60 (BoolVal (BoolAbs (i t))) + (BoolVal (BoolAbs (cin t))))", 61 PURE_REWRITE_TAC [HALFADD_IMP] THEN 62 REPEAT STRIP_TAC THEN 63 IMP_RES_TAC AND_CORRECT THEN 64 IMP_RES_TAC XOR_CORRECT THEN 65 RES_TAC THEN 66 ASM_REWRITE_TAC [and;xor;BoolVal] THEN 67 BOOL_CASES_TAC "BoolAbs (i t)" THEN 68 BOOL_CASES_TAC "BoolAbs (cin t)" THEN 69 REWRITE_TAC [MULT_CLAUSES;ADD_CLAUSES;num_CONV "2";num_CONV "1"]);; 70 71let th1 = ASSUME 72 "(2 * (BoolVal(BoolAbs(cout t)))) + 73 (BoolVal(BoolAbs(sum t(SUC n)))) = 74 (BoolVal(BoolAbs(i t(SUC n)))) + (BoolVal(BoolAbs(c t)))";; 75 76let th2 = AP_TERM "$* (2 EXP (SUC n))" th1;; 77let th3 = PURE_REWRITE_RULE [MULT_ASSOC;LEFT_ADD_DISTRIB] th2;; 78let th4 = SUBS [SPECL ["2 EXP (SUC n)";"2"] MULT_SYM] th3;; 79let th5 = PURE_REWRITE_RULE [SYM (CONJUNCT2 EXP)] th4;; 80let th6 = BETA_RULE (AP_TERM "\tm. tm + (WordVal n (WordAbs (sum t)))" th5);; 81let th7 = PURE_REWRITE_RULE [GEN_ALL (SYM (SPEC_ALL ADD_ASSOC))] th6;; 82 83let th8 = 84 BETA_RULE 85 ((DEPTH_CONV (REWRITE_CONV WordAbs)) "WordAbs v n");; 86 87let HALFADDn_CORRECT = prove_thm ( 88 `HALFADDn_CORRECT`, 89 "!n i cin sum cout. 90 HALFADDn_IMP n i cin sum cout 91 ==> 92 !t. 93 Defn n (i t) /\ Def (cin t) ==> 94 Defn n (sum t) /\ Def (cout t) /\ 95 (((2 EXP (SUC n)) * (BoolVal (BoolAbs (cout t)))) + 96 (WordVal n (WordAbs (sum t))) = 97 (WordVal n (WordAbs (i t))) + (BoolVal (BoolAbs (cin t))))", 98 INDUCT_TAC THENL 99 [PURE_REWRITE_TAC [HALFADDn_IMP;Defn;WordAbs;WordVal] THEN 100 BETA_TAC THEN 101 PURE_REWRITE_TAC [EXP;MULT_CLAUSES] THEN 102 REPEAT STRIP_TAC THEN 103 HOL_IMP_RES_THEN 104 (IMP_RES_TAC o BETA_RULE o (PURE_REWRITE_RULE [DEST_BUS])) 105 HALFADD_CORRECT THEN 106 RES_TAC; 107 PURE_REWRITE_TAC [HALFADDn_IMP;Defn] THEN 108 REPEAT GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN 109 GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN 110 RES_TAC THEN 111 RES_TAC THEN 112 HOL_IMP_RES_THEN 113 (IMP_RES_TAC o BETA_RULE o (PURE_REWRITE_RULE [DEST_BUS])) 114 HALFADD_CORRECT THEN 115 REPEAT STRIP_TAC THENL 116 [FIRST_ASSUM ACCEPT_TAC; 117 FIRST_ASSUM ACCEPT_TAC; 118 FIRST_ASSUM ACCEPT_TAC; 119 PURE_REWRITE_TAC 120 [WordVal;th8;GEN_ALL (SYM (SPEC_ALL ADD_ASSOC))] THEN 121 SUBST1_TAC th7 THEN 122 ASM_REWRITE_TAC []]]);; 123 124close_theory ();; 125