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