1% PROOF		: Transistor Implementation of a Counter		%
2% FILE		: count.ml						%
3%									%
4% DESCRIPTION	: Top-level implementation of the counter with three	%
5%		  different correctness statements.			%
6%									%
7% AUTHOR	: J.Joyce						%
8% DATE		: 1 April 1987						%
9
10new_theory `count`;;
11
12loadt `misc`;;
13loadt `types`;;
14
15new_parent `regn`;;
16new_parent `muxn`;;
17new_parent `incn`;;
18
19let COUNT_IMP = new_definition (
20	`COUNT_IMP`,
21	"COUNT_IMP n (phiA:^wire,reset:^wire,in:^bus,out:^bus) =
22	  ?phiAbar phiB phiBbar b1 b2.
23	    Clock (phiA,phiAbar,phiB,phiBbar) /\
24	    REGn_IMP n (phiA,phiB,b1,out) /\
25	    MUXn_IMP n (reset,in,b2,b1) /\
26	    INCn_IMP n (out,b2) /\
27	    isBus n b1 /\
28	    isBus n b2");;
29
30let when = definition `tempabs` `when`;;
31let mux = definition `muxn` `mux`;;
32
33let BoolAbs_THM = theorem `dataabs` `BoolAbs_THM`;;
34let REGn_CORRECT = theorem `regn` `REGn_CORRECT`;;
35let MUXn_CORRECT = theorem `muxn` `MUXn_CORRECT`;;
36let INCn_CORRECT = theorem `incn` `INCn_CORRECT`;;
37
38let LESS_OR_EQ_ADD = TAC_PROOF(
39	([],"!m n. m <= n = (?p. p + m = n)"),
40	REPEAT GEN_TAC THEN
41	EQ_TAC THENL
42	[PURE_REWRITE_TAC [LESS_OR_EQ] THEN
43	 REPEAT STRIP_TAC THENL
44	 [IMP_RES_TAC LESS_ADD;
45	  EXISTS_TAC "0" THEN ASM_REWRITE_TAC [ADD_CLAUSES]];
46	 REPEAT STRIP_TAC THEN
47	 FIRST_ASSUM (SUBST1_TAC o SYM) THEN
48	 SUBST1_TAC (SPECL ["p";"m"] ADD_SYM) THEN
49	 REWRITE_TAC [LESS_EQ_ADD]]);;
50
51
52% =========================================== %
53% Basic Behaviour disregarding initialization %
54
55let COUNT_CORRECT1 = prove_thm (
56	`COUNT_CORRECT1`,
57	"!n clk reset inp out.
58	  COUNT_IMP n (clk,reset,inp,out) /\
59	  isBus n inp /\
60	  isBus n out
61	  ==>
62	  !t.
63	    Def ((reset when (isHi clk)) t) /\
64	      Defn n ((inp when (isHi clk)) t) /\
65	        (((reset when (isHi clk)) t = Hi) \/
66	          (Defn n ((out when (isHi clk)) t)))
67	    ==>
68	    Defn n ((out when (isHi clk)) (t+1)) /\
69	      (WordVal n (WordAbs ((out when (isHi clk)) (t+1))) =
70	        (BoolAbs ((reset when (isHi clk)) t) =>
71	          (WordVal n (WordAbs ((inp when (isHi clk)) t))) |
72	          (((WordVal n (WordAbs ((out when (isHi clk)) t))) + 1)
73	            MOD (2 EXP (SUC n)))))",
74	let REGn_thm = (BETA_RULE (PURE_REWRITE_RULE [when] REGn_CORRECT))
75	in
76	PURE_REWRITE_TAC [COUNT_IMP;when] THEN
77	BETA_TAC THEN
78	REPEAT STRIP_TAC THEN
79	IMP_RES_TAC REGn_thm THEN
80	IMP_RES_TAC MUXn_CORRECT THEN
81	IMP_RES_TAC INCn_CORRECT THEN
82	ASM_REWRITE_TAC [mux] THENL
83	[ASM_REWRITE_TAC [BoolAbs_THM];
84	 ASM_REWRITE_TAC [BoolAbs_THM];
85	 COND_CASES_TAC THEN ASM_REWRITE_TAC [BoolAbs_THM];
86	 COND_CASES_TAC THEN ASM_REWRITE_TAC [BoolAbs_THM]]);;
87
88% ================================================== %
89% Behaviour plus proper initialization at some point %
90
91let th1 = CONJUNCT1 (CONJUNCT2 (CONJUNCT2 ADD_CLAUSES));;
92let th2 = (DEPTH_CONV (REWRITE_CONV th1)) "((SUC p) + sysinit)";;
93let th3 = SYM (TRANS th2 ((REWRITE_CONV ADD1) (rhs (concl th2))));;
94
95let COUNT_CORRECT2 = prove_thm (
96	`COUNT_CORRECT2`,
97	"!n clk reset inp out.
98	  COUNT_IMP n (clk,reset,inp,out) /\
99	  isBus n inp /\
100	  isBus n out /\
101	  (!t. Def ((reset when (isHi clk)) t)) /\
102	  (!t. Defn n ((inp when (isHi clk)) t))
103	  ==>
104	  !sysinit.
105	    ((reset when (isHi clk)) sysinit = Hi)
106	    ==>
107	    !t. sysinit <= t ==>
108	      Defn n ((out when (isHi clk)) (t+1)) /\
109	        (WordVal n (WordAbs ((out when (isHi clk)) (t+1))) =
110	          (BoolAbs ((reset when (isHi clk)) t) =>
111	            (WordVal n (WordAbs ((inp when (isHi clk)) t))) |
112	            (((WordVal n (WordAbs ((out when (isHi clk)) t))) + 1)
113	              MOD (2 EXP (SUC n)))))",
114	PURE_REWRITE_TAC [LESS_OR_EQ_ADD] THEN
115	REPEAT GEN_TAC THEN STRIP_TAC THEN
116	GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN
117	DISCH_THEN (STRIP_THM_THEN (SUBST1_TAC o SYM)) THEN
118	SPEC_TAC ("p","p") THEN
119	INDUCT_TAC THENL
120	[PURE_REWRITE_TAC [ADD_CLAUSES] THEN
121	 ASSUM_LIST (MAP_EVERY
122	   (\thm. if (is_forall (concl thm))
123	     then (ASSUME_TAC (SPEC "sysinit" thm)) else ALL_TAC)) THEN
124	 IMP_RES_TAC COUNT_CORRECT1 THEN
125	 RES_TAC THEN
126	 ASM_REWRITE_TAC [];
127	 ASSUM_LIST (MAP_EVERY
128	   (\thm. if (is_forall (concl thm))
129	     then (ASSUME_TAC (SPEC "(SUC p) + sysinit" thm))
130	     else ALL_TAC)) THEN
131	 ASSUM_LIST (MAP_EVERY
132	   (\thm. if (is_conj (concl thm))
133	     then (ASSUME_TAC (SUBS [th3] (CONJUNCT1 thm)))
134	     else ALL_TAC)) THEN
135	 IMP_RES_TAC COUNT_CORRECT1 THEN
136	 RES_TAC THEN
137	 ASM_REWRITE_TAC []]);;
138
139% ========================================================== %
140% Similar to COUNT_CORRECT2 but weaker assumptions on inputs %
141
142let COUNT_CORRECT3 = prove_thm (
143	`COUNT_CORRECT3`,
144	"!n clk reset inp out.
145	  COUNT_IMP n (clk,reset,inp,out) /\
146	  isBus n inp /\
147	  isBus n out
148	  ==>
149	  !sysinit.
150	    (!t. sysinit <= t ==> Def ((reset when (isHi clk)) t)) /\
151	    (!t. sysinit <= t ==> Defn n ((inp when (isHi clk)) t)) /\
152	    ((reset when (isHi clk)) sysinit = Hi)
153	    ==>
154	    !t. sysinit <= t ==>
155	      Defn n ((out when (isHi clk)) (t+1)) /\
156	        (WordVal n (WordAbs ((out when (isHi clk)) (t+1))) =
157	          (BoolAbs ((reset when (isHi clk)) t) =>
158	            (WordVal n (WordAbs ((inp when (isHi clk)) t))) |
159	            (((WordVal n (WordAbs ((out when (isHi clk)) t))) + 1)
160	              MOD (2 EXP (SUC n)))))",
161	REPEAT GEN_TAC THEN STRIP_TAC THEN
162	GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN
163	PURE_REWRITE_TAC [LESS_OR_EQ_ADD] THEN
164	DISCH_THEN (STRIP_THM_THEN (SUBST1_TAC o SYM)) THEN
165	SPEC_TAC ("p","p") THEN
166	INDUCT_TAC THENL
167	[PURE_REWRITE_TAC [ADD_CLAUSES] THEN
168	 ASSUME_TAC (SPEC "sysinit" LESS_EQ_REFL) THEN
169	 RES_TAC THEN
170	 IMP_RES_TAC COUNT_CORRECT1 THEN
171	 RES_TAC THEN
172	 ASM_REWRITE_TAC [];
173	 ASSUME_TAC
174	   (SUBS [SPECL ["sysinit";"SUC p"] ADD_SYM]
175	    (SPECL ["sysinit";"SUC p"] LESS_EQ_ADD)) THEN
176	 RES_TAC THEN
177	 ASSUM_LIST (MAP_EVERY
178	   (\thm. if (is_conj (concl thm))
179	     then (ASSUME_TAC (SUBS [th3] (CONJUNCT1 thm)))
180	     else ALL_TAC)) THEN
181	 IMP_RES_TAC COUNT_CORRECT1 THEN
182	 RES_TAC THEN
183	 ASM_REWRITE_TAC []]);;
184
185close_theory ();;
186