1% PROOF		: Transistor Implementation of a Counter		%
2% FILE		: gates.ml						%
3%									%
4% DESCRIPTION	: Defines CMOS implementations of basic gates used	%
5%		  in the increment unit circuit and derives boolean	%
6%		  behaviours.						%
7%									%
8% AUTHOR	: J.Joyce						%
9% DATE		: 31 March 1987						%
10
11new_theory `gates`;;
12
13loadt `misc`;;
14loadt `types`;;
15
16new_parent `dataabs`;;
17
18let inv = new_definition (`inv`,"inv i = ~i");;
19let nand = new_definition (`nand`,"nand (i1,i2) = ~(i1 /\ i2)");;
20let and = new_definition (`and`,"and (i1,i2) = (i1 /\ i2)");;
21let xor = new_definition (`xor`,"xor (i1,i2) = (i1 /\ ~i2) \/ (~i1 /\ i2)");;
22
23let INV_IMP = new_definition (
24	`INV_IMP`,
25	"INV_IMP (i:^wire,o:^wire) =
26	  ?w1 w2 w3 w4.
27	    Vdd (w1) /\
28	    Ptran (i,w1,w2) /\
29	    Join (w2,w3,o) /\
30	    Ntran (i,w4,w3) /\
31	    Gnd (w4)");;
32
33let NAND_IMP = new_definition (
34	`NAND_IMP`,
35	"NAND_IMP (i1:^wire,i2:^wire,o:^wire) =
36	  ?w1 w2 w3 w4 w5 w6 w7.
37	    Vdd (w1) /\
38	    Ptran (i1,w1,w2) /\
39	    Ptran (i2,w1,w3) /\
40	    Join (w2,w3,w4) /\
41	    Join (w4,w5,o) /\
42	    Ntran (i1,w6,w5) /\
43	    Ntran (i2,w7,w6) /\
44	    Gnd (w7)");;
45
46let AND_IMP = new_definition (
47	`AND_IMP`,
48	"AND_IMP (i1:^wire,i2:^wire,o:^wire) =
49	  ?w. NAND_IMP (i1,i2,w) /\ INV_IMP (w,o)");;
50
51let XOR_IMP = new_definition (
52	`XOR_IMP`,
53	"XOR_IMP (i1:^wire,i2:^wire,o:^wire) =
54	  ?w1 w2 w3.
55	    NAND_IMP (i1,i2,w1) /\
56	    NAND_IMP (i1,w1,w2) /\
57	    NAND_IMP (i2,w1,w3) /\
58	    NAND_IMP (w2,w3,o)");;
59
60let val_not_eq_ax = axiom `mos` `val_not_eq_ax`;;
61
62let U = definition `mos` `U`;;
63let Not = definition `mos` `Not`;;
64let Vdd = definition `mos` `Vdd`;;
65let Gnd = definition `mos` `Gnd`;;
66let Ptran = definition `mos` `Ptran`;;
67let Ntran = definition `mos` `Ntran`;;
68let Join = definition `mos` `Join`;;
69let Def = definition `dataabs` `Def`;;
70let BoolAbs_THM = theorem `dataabs` `BoolAbs_THM`;;
71let Def_DISJ_CASES = theorem `dataabs` `Def_DISJ_CASES`;;
72
73let INV_CORRECT = prove_thm (
74	`INV_CORRECT`,
75	"!i o.
76	  INV_IMP (i,o)
77	  ==>
78	  !t.
79	    Def (i t) ==>
80	      Def (o t) /\ (BoolAbs (o t) = inv (BoolAbs (i t)))",
81	let th1 = EXPANDF [Vdd;Gnd;Ptran;Ntran;Join] INV_IMP
82	in
83	PURE_REWRITE_TAC [th1] THEN
84	REPEAT STRIP_TAC THEN
85	PURE_REWRITE_TAC [Def] THEN
86	IMP_RES_TAC Def_DISJ_CASES THEN
87	ASM_REWRITE_TAC [val_not_eq_ax;U;BoolAbs_THM;inv]);;
88
89let NAND_CORRECT = prove_thm (
90	`NAND_CORRECT`,
91	"!i1 i2 o.
92	  NAND_IMP (i1,i2,o)
93	  ==>
94	  !t.
95	    Def (i1 t) /\ Def (i2 t) ==>
96	      Def (o t) /\
97	        (BoolAbs (o t) = nand (BoolAbs (i1 t),BoolAbs (i2 t)))",
98	let th1 = EXPANDF [Vdd;Gnd;Ptran;Ntran;Join] NAND_IMP
99	in
100	PURE_REWRITE_TAC [th1] THEN
101	REPEAT STRIP_TAC THEN
102	PURE_REWRITE_TAC [Def] THEN
103	IMP_RES_TAC Def_DISJ_CASES THEN
104	ASM_REWRITE_TAC [val_not_eq_ax;U;BoolAbs_THM;nand]);;
105
106let AND_CORRECT = prove_thm (
107	`AND_CORRECT`,
108	"!i1 i2 o.
109	  AND_IMP (i1,i2,o)
110	  ==>
111	  !t.
112	    Def (i1 t) /\ Def (i2 t) ==>
113	      Def (o t) /\
114	        (BoolAbs (o t) = and (BoolAbs (i1 t),BoolAbs (i2 t)))",
115	PURE_REWRITE_TAC [AND_IMP] THEN
116	REPEAT STRIP_TAC THEN
117	IMP_RES_TAC NAND_CORRECT THEN
118	RES_TAC THEN
119	IMP_RES_TAC INV_CORRECT THEN
120	RES_TAC THEN
121	ASM_REWRITE_TAC [nand;inv;and]);;
122
123let XOR_CORRECT = prove_thm (
124	`XOR_CORRECT`,
125	"!i1 i2 o.
126	  XOR_IMP (i1,i2,o)
127	  ==>
128	  !t.
129	    Def (i1 t) /\ Def (i2 t) ==>
130	      Def (o t) /\
131	        (BoolAbs (o t) = xor (BoolAbs (i1 t),BoolAbs (i2 t)))",
132	PURE_REWRITE_TAC [XOR_IMP] THEN
133	REPEAT STRIP_TAC THEN
134	IMP_RES_TAC NAND_CORRECT THEN
135	RES_TAC THEN
136	ASM_REWRITE_TAC [] THEN
137	BOOL_CASES_TAC "BoolAbs (i1 t)" THEN
138	BOOL_CASES_TAC "BoolAbs (i2 t)" THEN
139	REWRITE_TAC [nand;xor]);;
140
141close_theory ();;
142