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