1% PROOF		: Transistor Implementation of a Counter		%
2% FILE		: muxn.ml						%
3%									%
4% DESCRIPTION	: Defines a CMOS Mux and uses this to construct a	%
5%		  n-bit Mux.  Only the control line is abstracted	%
6%		  to a boolean signal.					%
7%									%
8% AUTHOR	: J.Joyce						%
9% DATE		: 31 March 1987						%
10
11new_theory `muxn`;;
12
13loadt `misc`;;
14loadt `types`;;
15
16new_parent `gates`;;
17
18let mux = new_definition (`mux`,"mux (cntl,i1:*,i2:*) = cntl => i1 | i2");;
19
20let CMUX_IMP = new_definition (
21	`CMUX_IMP`,
22	"CMUX_IMP (cntl:^wire,cntlbar:^wire,i1:^wire,i2:^wire,o:^wire) =
23	  ?w1 w2 w3 w4 w5 w6.
24	    Ptran (cntlbar,i1,w1) /\
25	    Ntran (cntl,i1,w2) /\
26	    Join (w1,w2,w3) /\
27	    Join (w3,w4,o) /\
28	    Join (w5,w6,w4) /\
29	    Ptran (cntl,i2,w5) /\
30	    Ntran (cntlbar,i2,w6)");;
31
32let CMUXn_IMP = new_definition (
33	`CMUXn_IMP`,
34	"CMUXn_IMP n (cntl:^wire,cntlbar:^wire,i1:^bus,i2:^bus,o:^bus) =
35	  !m. m <= n ==>
36	    CMUX_IMP
37	      (cntl,cntlbar,DEST_BUS i1 m,DEST_BUS i2 m,DEST_BUS o m)");;
38
39let MUXn_IMP = new_definition (
40	`MUXn_IMP`,
41	"MUXn_IMP n (cntl:^wire,i1:^bus,i2:^bus,o:^bus) =
42	  ?cntlbar.
43	    INV_IMP (cntl,cntlbar) /\ CMUXn_IMP n (cntl,cntlbar,i1,i2,o)");;
44
45let U = definition `mos` `U`;;
46let Vdd = definition `mos` `Vdd`;;
47let Gnd = definition `mos` `Gnd`;;
48let Ptran = definition `mos` `Ptran`;;
49let Ntran = definition `mos` `Ntran`;;
50let Join = definition `mos` `Join`;;
51let Not = definition `mos` `Not`;;
52let Def = definition `dataabs` `Def`;;
53let DEST_BUS = definition `dataabs` `DEST_BUS`;;
54let INV_IMP = definition `gates` `INV_IMP`;;
55
56let val_not_eq_ax = axiom `mos` `val_not_eq_ax`;;
57
58let Def_DISJ_CASES = theorem `dataabs` `Def_DISJ_CASES`;;
59let BoolAbs_THM = theorem `dataabs` `BoolAbs_THM`;;
60let isBus_THM = theorem `dataabs` `isBus_THM`;;
61
62let lemma1 = TAC_PROOF ((
63	  [],
64	  "(!t1:*. !t2:*. (((t1 = t2) => t1 | t1) = t1)) /\
65	   (!t1:*. !t2:*. (((t1 = t2) => t2 | t2) = t2)) /\
66	   (!t1:*. !t2:*. (((t1 = t2) => t1 | t2) = t2)) /\
67	   (!t1:*. !t2:*. (((t1 = t2) => t2 | t1) = t1))"),
68	let thm = SYM (CONJUNCT2(CONJUNCT2(CONJUNCT2 (SPEC_ALL EQ_CLAUSES))))
69	in
70	REPEAT STRIP_TAC THEN
71	DISJ_CASES_TAC (SPEC "t1 = t2" EXCLUDED_MIDDLE) THEN
72	IMP_RES_TAC thm THEN
73	ASM_REWRITE_TAC []);;
74
75let CMUX_CORRECT = prove_thm (
76	`CMUX_CORRECT`,
77	"!cntl cntlbar i1 i2 o.
78	  CMUX_IMP (cntl,cntlbar,i1,i2,o)
79	  ==>
80	  !t.
81	    Def (cntl t) /\ (cntlbar t = Not (cntl t))
82	    ==>
83	    (o t = mux (BoolAbs (cntl t),i1 t,i2 t))",
84	PURE_REWRITE_TAC [EXPANDF [Ptran;Ntran;Join] CMUX_IMP] THEN
85	REPEAT STRIP_TAC THEN
86	IMP_RES_TAC Def_DISJ_CASES THEN
87	ASM_REWRITE_TAC [Not;mux;U;val_not_eq_ax;BoolAbs_THM;lemma1]);;
88
89let CMUXn_CORRECT = prove_thm (
90	`CMUXn_CORRECT`,
91	"!n cntl cntlbar i1 i2 o.
92	  CMUXn_IMP n (cntl,cntlbar,i1,i2,o) /\
93	  isBus n i1 /\
94	  isBus n i2 /\
95	  isBus n o
96	  ==>
97	  !t.
98	    Def (cntl t) /\ (cntlbar t = Not (cntl t))
99	    ==>
100	    (o t = mux (BoolAbs (cntl t),i1 t,i2 t))",
101	PURE_REWRITE_TAC [CMUXn_IMP;mux] THEN
102	REPEAT STRIP_TAC THEN
103	COND_CASES_TAC THEN
104	IMP_RES_TAC isBus_THM THEN
105	ASM_REWRITE_TAC [] THEN
106	REPEAT STRIP_TAC THEN
107	RES_TAC THEN
108	HOL_IMP_RES_THEN
109	  (ASSUME_TAC o BETA_RULE o PURE_REWRITE_RULE [DEST_BUS])
110	  CMUX_CORRECT THEN
111	RES_TAC THEN
112	ASM_REWRITE_TAC [mux]);;
113
114let th1 = TAC_PROOF (
115	([],"!i o. INV_IMP (i,o) ==> !t. Def (i t) ==> (o t = Not (i t))"),
116	PURE_REWRITE_TAC [EXPANDF [Vdd;Gnd;Ptran;Ntran;Join] INV_IMP] THEN
117	REPEAT STRIP_TAC THEN
118	IMP_RES_TAC Def_DISJ_CASES THEN
119	ASM_REWRITE_TAC [Not;U;val_not_eq_ax]);;
120
121let MUXn_CORRECT = prove_thm (
122	`MUXn_CORRECT`,
123	"!n cntl i1 i2 o.
124	  MUXn_IMP n (cntl,i1,i2,o) /\
125	  isBus n i1 /\
126	  isBus n i2 /\
127	  isBus n o
128	  ==>
129	  !t. Def (cntl t) ==> (o t = mux (BoolAbs (cntl t),i1 t,i2 t))",
130	PURE_REWRITE_TAC [MUXn_IMP] THEN
131	REPEAT STRIP_TAC THEN
132	IMP_RES_TAC th1 THEN
133	IMP_RES_TAC CMUXn_CORRECT THEN
134	RES_TAC);;
135
136close_theory ();;
137