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