1%  MICROCODED COMPUTER PROOF : HOL                                      %
2%                                                                       %
3%  'proof4.ml'                                                          %
4%                                                                       %
5%  Description                                                          % 
6%                                                                       %
7%     This theory puts the results from 'proof3' into the final form    %
8%  for the case analysis.  The theorems from 'proof3' are conjunctions  %
9%  consisting of four conjuncts which state equivalences.  These are    %
10%  are changed into theorems about the equivalence of four-tuples in    %
11%  accordance with the target level specification.  Furthermore, the    %
12%  assumption that "mpc t1 = #00000" is traded in for the assumptions   %
13%  "ready t1" and "idle t1" using a lemma from 'proof1'.  Similarly,    %
14%  "mpc t1 = #00101" is replaced by the assumptions "ready t1" and      %
15%  "~idle t1".                                                          %
16%                                                                       %
17%  Author:  Jeff Joyce                                                  %
18%  Date:    August 4, 1985                                              %
19
20new_theory `proof4`;;
21
22new_parent `proof3`;;
23
24let ready_idle_mpc = theorem `proof1` `ready_idle_mpc`;;
25let ready_not_idle_mpc = theorem `proof1` `ready_not_idle_mpc`;;
26
27let SIMP_mpc_0_button_T_knob_0 =
28 theorem `proof3` `SIMP_mpc_0_button_T_knob_0`;;
29let SIMP_mpc_0_button_T_knob_1 =
30 theorem `proof3` `SIMP_mpc_0_button_T_knob_1`;;
31let SIMP_mpc_0_button_T_knob_2 =
32 theorem `proof3` `SIMP_mpc_0_button_T_knob_2`;;
33let SIMP_mpc_0_button_T_knob_3 =
34 theorem `proof3` `SIMP_mpc_0_button_T_knob_3`;;
35let SIMP_mpc_0_button_F =
36 theorem `proof3` `SIMP_mpc_0_button_F`;;
37let SIMP_mpc_5_button_T =
38 theorem `proof3` `SIMP_mpc_5_button_T`;;
39let SIMP_mpc_5_button_F_opcode_0 =
40 theorem `proof3` `SIMP_mpc_5_button_F_opcode_0`;;
41let SIMP_mpc_5_button_F_opcode_1 =
42 theorem `proof3` `SIMP_mpc_5_button_F_opcode_1`;;
43let SIMP_mpc_5_button_F_zero_opcode_2 =
44 theorem `proof3` `SIMP_mpc_5_button_F_zero_opcode_2`;;
45let SIMP_mpc_5_button_F_nonzero_opcode_2 =
46 theorem `proof3` `SIMP_mpc_5_button_F_nonzero_opcode_2`;;
47let SIMP_mpc_5_button_F_opcode_3 =
48 theorem `proof3` `SIMP_mpc_5_button_F_opcode_3`;;
49let SIMP_mpc_5_button_F_opcode_4 =
50 theorem `proof3` `SIMP_mpc_5_button_F_opcode_4`;;
51let SIMP_mpc_5_button_F_opcode_5 =
52 theorem `proof3` `SIMP_mpc_5_button_F_opcode_5`;;
53let SIMP_mpc_5_button_F_opcode_6 =
54 theorem `proof3` `SIMP_mpc_5_button_F_opcode_6`;;d
55let SIMP_mpc_5_button_F_opcode_7 =
56 theorem `proof3` `SIMP_mpc_5_button_F_opcode_7`;;
57
58let idle_T_lemma =
59 SYM
60  (CONJUNCT1 (CONJUNCT2 (SPEC "(idle (t2:num)):bool" EQ_CLAUSES)));;
61
62let idle_F_lemma =
63 SYM
64  (CONJUNCT2
65   (CONJUNCT2 (CONJUNCT2 (SPEC "(idle (t2:num)):bool" EQ_CLAUSES))));;
66
67%     tuples_lemma =                                                    %
68%     |- !a1 a2 b1 b2 c1 c2 d1 d2.                                      %
69%     (a1 = a2) /\ (b1 = b2) /\ (c1 = c2) /\ (d1 = d2) ==>              %
70%     (a1,b1,c1,d1 = a2,b2,c2,d2)                                       %
71
72let tuples_lemma =
73  (GEN_ALL
74   (DISCH_ALL
75    (SUBS_OCCS
76     (map
77      (\th.([2],th))
78      (CONJUNCTS
79       (ASSUME
80        "(((a1:mem13_16) = (a2:mem13_16)) /\
81          ((b1:word13) = (b2:word13)) /\
82          ((c1:word16) = (c2:word16)) /\
83          ((d1:bool) = (d2:bool)))")))
84     (REFL "a1:mem13_16,b1:word13,c1:word16,d1:bool"))));;
85
86let four_tuple thm =
87 let th1 = (SUBS [idle_T_lemma;idle_F_lemma] thm) in
88 let (m_lhs,m_rhs) =
89  (dest_eq (fst (dest_conj (snd (dest_thm th1))))) in
90 let (pc_lhs,pc_rhs) =
91  (dest_eq (fst (dest_conj (snd (dest_conj (snd (dest_thm th1))))))) in
92 let (acc_lhs,acc_rhs) =
93  (dest_eq (fst (dest_conj
94   (snd (dest_conj (snd (dest_conj (snd (dest_thm th1))))))))) in
95 let (idle_lhs,idle_rhs) =
96  (dest_eq (snd (dest_conj
97   (snd (dest_conj (snd (dest_conj (snd (dest_thm th1))))))))) in
98 let th2 =
99  SPECL [m_lhs;m_rhs;pc_lhs;pc_rhs;acc_lhs;acc_rhs;idle_lhs;idle_rhs]
100   tuples_lemma in
101 (MP th2 th1);;
102
103let introduce_idle_asm b thm =
104 if b
105  then (MP (DISCH "(mpc (t1:num)) = #00000" thm) ready_idle_mpc)
106  else (MP (DISCH "(mpc (t1:num)) = #00101" thm) ready_not_idle_mpc);;
107
108% ===================================================================== %
109% Case: idle, button = T, knob is 0 =================================== %
110
111let CASE_idle_button_T_knob_0 =
112 save_thm
113 (
114  `CASE_idle_button_T_knob_0`,
115  (introduce_idle_asm true (four_tuple SIMP_mpc_0_button_T_knob_0))
116 );;
117
118% ===================================================================== %
119% Case: idle, button = T, knob is 1 =================================== %
120
121let CASE_idle_button_T_knob_1 =
122 save_thm
123 (
124  `CASE_idle_button_T_knob_1`,
125  (introduce_idle_asm true (four_tuple SIMP_mpc_0_button_T_knob_1))
126 );;
127
128% ===================================================================== %
129% Case: idle, button = T, knob is 2 =================================== %
130
131let CASE_idle_button_T_knob_2 =
132 save_thm
133 (
134  `CASE_idle_button_T_knob_2`,
135  (introduce_idle_asm true (four_tuple SIMP_mpc_0_button_T_knob_2))
136 );;
137
138% ===================================================================== %
139% Case: idle, button = T, knob is 3 =================================== %
140
141let CASE_idle_button_T_knob_3 =
142 save_thm
143 (
144  `CASE_idle_button_T_knob_3`,
145  (introduce_idle_asm true (four_tuple SIMP_mpc_0_button_T_knob_3))
146 );;
147
148% ===================================================================== %
149% Case: idle, button = F ============================================== %
150
151let CASE_idle_button_F =
152 save_thm
153 (
154  `CASE_idle_button_F`,
155  (introduce_idle_asm true (four_tuple SIMP_mpc_0_button_F))
156 );;
157
158% ===================================================================== %
159% Case: run, button = T =============================================== %
160
161let CASE_run_button_T =
162 save_thm
163 (
164  `CASE_run_button_T`,
165  (introduce_idle_asm false (four_tuple SIMP_mpc_5_button_T))
166 );;
167
168% ===================================================================== %
169% Case: run, button = F, opcode is 0 (HALT) =========================== %
170
171let CASE_run_button_F_opcode_0 =
172 save_thm
173 (
174  `CASE_run_button_F_opcode_0`,
175  (introduce_idle_asm false (four_tuple SIMP_mpc_5_button_F_opcode_0))
176 );;
177
178% ===================================================================== %
179% Case: run, button = F, opcode is 1 (JMP) ============================ %
180
181let CASE_run_button_F_opcode_1 =
182 save_thm
183 (
184  `CASE_run_button_F_opcode_1`,
185  (introduce_idle_asm false (four_tuple SIMP_mpc_5_button_F_opcode_1))
186 );;
187
188% ===================================================================== %
189% Case: run, button = F, zero, opcode is 2 (JZR) ====================== %
190
191let CASE_run_button_F_zero_opcode_2 =
192 save_thm
193 (
194  `CASE_run_button_F_zero_opcode_2`,
195  (introduce_idle_asm false (four_tuple SIMP_mpc_5_button_F_zero_opcode_2))
196 );;
197
198% ===================================================================== %
199% Case: run, button = F, nonzero, opcode is 2 (JZR) =================== %
200
201let CASE_run_button_F_nonzero_opcode_2 =
202 save_thm
203 (
204  `CASE_run_button_F_nonzero_opcode_2`,
205  (introduce_idle_asm false (four_tuple SIMP_mpc_5_button_F_nonzero_opcode_2))
206 );;
207
208% ===================================================================== %
209% Case: run, button = F, opcode is 3 (ADD) ============================ %
210
211let CASE_run_button_F_opcode_3 =
212 save_thm
213 (
214  `CASE_run_button_F_opcode_3`,
215  (introduce_idle_asm false (four_tuple SIMP_mpc_5_button_F_opcode_3))
216 );;
217
218% ===================================================================== %
219% Case: run, button = F, opcode is 4 (SUB) ============================ %
220
221let CASE_run_button_F_opcode_4 =
222 save_thm
223 (
224  `CASE_run_button_F_opcode_4`,
225  (introduce_idle_asm false (four_tuple SIMP_mpc_5_button_F_opcode_4))
226 );;
227
228% ===================================================================== %
229% Case: run, button = F, opcode is 5 (LD) ============================= %
230
231let CASE_run_button_F_opcode_5 =
232 save_thm
233 (
234  `CASE_run_button_F_opcode_5`,
235  (introduce_idle_asm false (four_tuple SIMP_mpc_5_button_F_opcode_5))
236 );;
237
238% ===================================================================== %
239% Case: run, button = F, opcode is 6 (ST) ============================= %
240
241let CASE_run_button_F_opcode_6 =
242 save_thm
243 (
244  `CASE_run_button_F_opcode_6`,
245  (introduce_idle_asm false (four_tuple SIMP_mpc_5_button_F_opcode_6))
246 );;
247
248% ===================================================================== %
249% Case: run, button = F, opcode is 7 (SKIP) =========================== %
250
251let CASE_run_button_F_opcode_7 =
252 save_thm
253 (
254  `CASE_run_button_F_opcode_7`,
255  (introduce_idle_asm false (four_tuple SIMP_mpc_5_button_F_opcode_7))
256 );;
257
258close_theory ();;
259