1signature ILTheory = 2sig 3 type thm = Thm.thm 4 5 (* Definitions *) 6 val BLK : thm 7 val CJ : thm 8 val CTL_STRUCTURE_TY_DEF : thm 9 val CTL_STRUCTURE_case_def : thm 10 val CTL_STRUCTURE_repfns : thm 11 val CTL_STRUCTURE_size_def : thm 12 val DOPER_TY_DEF : thm 13 val DOPER_case_def : thm 14 val DOPER_repfns : thm 15 val DOPER_size_def : thm 16 val IL0_def : thm 17 val IL10_def : thm 18 val IL11_def : thm 19 val IL12_def : thm 20 val IL13_def : thm 21 val IL14_def : thm 22 val IL15_def : thm 23 val IL16_def : thm 24 val IL17_def : thm 25 val IL18_def : thm 26 val IL19_def : thm 27 val IL1_def : thm 28 val IL20_def : thm 29 val IL21_def : thm 30 val IL2_def : thm 31 val IL3_def : thm 32 val IL4_def : thm 33 val IL5_def : thm 34 val IL6_def : thm 35 val IL7_def : thm 36 val IL8_def : thm 37 val IL9_def : thm 38 val MADD : thm 39 val MAND : thm 40 val MASR : thm 41 val MC : thm 42 val MEOR : thm 43 val MEXP_TY_DEF : thm 44 val MEXP_case_def : thm 45 val MEXP_repfns : thm 46 val MEXP_size_def : thm 47 val MLDR : thm 48 val MLSL : thm 49 val MLSR : thm 50 val MMOV : thm 51 val MMUL : thm 52 val MORR : thm 53 val MPOP : thm 54 val MPUSH : thm 55 val MR : thm 56 val MREG_BIJ : thm 57 val MREG_TY_DEF : thm 58 val MREG_case : thm 59 val MREG_size_def : thm 60 val MROR : thm 61 val MRSB : thm 62 val MSTR : thm 63 val MSUB : thm 64 val R0 : thm 65 val R1 : thm 66 val R10 : thm 67 val R11 : thm 68 val R12 : thm 69 val R13 : thm 70 val R14 : thm 71 val R2 : thm 72 val R3 : thm 73 val R4 : thm 74 val R5 : thm 75 val R6 : thm 76 val R7 : thm 77 val R8 : thm 78 val R9 : thm 79 val SC : thm 80 val TR : thm 81 val WELL_FORMED_SUB_def : thm 82 val WELL_FORMED_def : thm 83 val eval_il_cond_def : thm 84 val from_reg_index_def : thm 85 val index_of_reg_def : thm 86 val mdecode_def : thm 87 val popL_def : thm 88 val pushL_def : thm 89 val run_arm_def : thm 90 val run_ir_def : thm 91 val toEXP_def : thm 92 val toMEM_def : thm 93 val toREG_def : thm 94 val translate_assignment_def : thm 95 val translate_condition_def : thm 96 val translate_primitive_def : thm 97 98 (* Theorems *) 99 val BLOCK_IS_WELL_FORMED : thm 100 val CTL_STRUCTURE_11 : thm 101 val CTL_STRUCTURE_Axiom : thm 102 val CTL_STRUCTURE_case_cong : thm 103 val CTL_STRUCTURE_distinct : thm 104 val CTL_STRUCTURE_induction : thm 105 val CTL_STRUCTURE_nchotomy : thm 106 val DOPER_11 : thm 107 val DOPER_Axiom : thm 108 val DOPER_case_cong : thm 109 val DOPER_distinct : thm 110 val DOPER_induction : thm 111 val DOPER_nchotomy : thm 112 val HOARE_CJ_IR : thm 113 val HOARE_SC_IR : thm 114 val HOARE_TR_IR : thm 115 val IR_CJ_IS_WELL_FORMED : thm 116 val IR_SC_IS_WELL_FORMED : thm 117 val IR_SEMANTICS_BLK : thm 118 val IR_SEMANTICS_CJ : thm 119 val IR_SEMANTICS_SC : thm 120 val IR_SEMANTICS_TR : thm 121 val IR_TR_IS_WELL_FORMED : thm 122 val MEXP_11 : thm 123 val MEXP_Axiom : thm 124 val MEXP_case_cong : thm 125 val MEXP_distinct : thm 126 val MEXP_induction : thm 127 val MEXP_nchotomy : thm 128 val MREG2num_11 : thm 129 val MREG2num_ONTO : thm 130 val MREG2num_num2MREG : thm 131 val MREG2num_thm : thm 132 val MREG_Axiom : thm 133 val MREG_EQ_MREG : thm 134 val MREG_case_cong : thm 135 val MREG_case_def : thm 136 val MREG_distinct : thm 137 val MREG_induction : thm 138 val MREG_nchotomy : thm 139 val SEMANTICS_OF_IR : thm 140 val STATEMENT_IS_WELL_FORMED : thm 141 val TRANSLATE_ASSIGMENT_CORRECT : thm 142 val TRANSLATE_ASSIGMENT_CORRECT_2 : thm 143 val UPLOAD_LEM_2 : thm 144 val WELL_FORMED_SUB_thm : thm 145 val WELL_FORMED_thm : thm 146 val datatype_CTL_STRUCTURE : thm 147 val datatype_DOPER : thm 148 val datatype_MEXP : thm 149 val datatype_MREG : thm 150 val from_reg_index_thm : thm 151 val num2MREG_11 : thm 152 val num2MREG_MREG2num : thm 153 val num2MREG_ONTO : thm 154 val num2MREG_thm : thm 155 val translate_def : thm 156 val translate_ind : thm 157 158 val IL_grammars : type_grammar.grammar * term_grammar.grammar 159 160 161(* 162 [ARMComposition] Parent theory of "IL" 163 164 [BLK] Definition 165 166 |- BLK = IL18 167 168 [CJ] Definition 169 170 |- CJ = IL20 171 172 [CTL_STRUCTURE_TY_DEF] Definition 173 174 |- ?rep. 175 TYPE_DEFINITION 176 (\a0'. 177 !'CTL_STRUCTURE'. 178 (!a0'. 179 (?a. a0' = (\a. CONSTR 0 (a,@v. T) (\n. BOTTOM)) a) \/ 180 (?a0 a1. 181 (a0' = 182 (\a0 a1. 183 CONSTR (SUC 0) ((@v. T),@v. T) 184 (FCONS a0 (FCONS a1 (\n. BOTTOM)))) a0 a1) /\ 185 'CTL_STRUCTURE' a0 /\ 'CTL_STRUCTURE' a1) \/ 186 (?a0 a1 a2. 187 (a0' = 188 (\a0 a1 a2. 189 CONSTR (SUC (SUC 0)) ((@v. T),a0) 190 (FCONS a1 (FCONS a2 (\n. BOTTOM)))) a0 a1 a2) /\ 191 'CTL_STRUCTURE' a1 /\ 'CTL_STRUCTURE' a2) \/ 192 (?a0 a1. 193 (a0' = 194 (\a0 a1. 195 CONSTR (SUC (SUC (SUC 0))) ((@v. T),a0) 196 (FCONS a1 (\n. BOTTOM))) a0 a1) /\ 197 'CTL_STRUCTURE' a1) ==> 198 'CTL_STRUCTURE' a0') ==> 199 'CTL_STRUCTURE' a0') rep 200 201 [CTL_STRUCTURE_case_def] Definition 202 203 |- (!f f1 f2 f3 a. CTL_STRUCTURE_case f f1 f2 f3 (BLK a) = f a) /\ 204 (!f f1 f2 f3 a0 a1. CTL_STRUCTURE_case f f1 f2 f3 (SC a0 a1) = f1 a0 a1) /\ 205 (!f f1 f2 f3 a0 a1 a2. 206 CTL_STRUCTURE_case f f1 f2 f3 (CJ a0 a1 a2) = f2 a0 a1 a2) /\ 207 !f f1 f2 f3 a0 a1. CTL_STRUCTURE_case f f1 f2 f3 (TR a0 a1) = f3 a0 a1 208 209 [CTL_STRUCTURE_repfns] Definition 210 211 |- (!a. mk_CTL_STRUCTURE (dest_CTL_STRUCTURE a) = a) /\ 212 !r. 213 (\a0'. 214 !'CTL_STRUCTURE'. 215 (!a0'. 216 (?a. a0' = (\a. CONSTR 0 (a,@v. T) (\n. BOTTOM)) a) \/ 217 (?a0 a1. 218 (a0' = 219 (\a0 a1. 220 CONSTR (SUC 0) ((@v. T),@v. T) 221 (FCONS a0 (FCONS a1 (\n. BOTTOM)))) a0 a1) /\ 222 'CTL_STRUCTURE' a0 /\ 'CTL_STRUCTURE' a1) \/ 223 (?a0 a1 a2. 224 (a0' = 225 (\a0 a1 a2. 226 CONSTR (SUC (SUC 0)) ((@v. T),a0) 227 (FCONS a1 (FCONS a2 (\n. BOTTOM)))) a0 a1 a2) /\ 228 'CTL_STRUCTURE' a1 /\ 'CTL_STRUCTURE' a2) \/ 229 (?a0 a1. 230 (a0' = 231 (\a0 a1. 232 CONSTR (SUC (SUC (SUC 0))) ((@v. T),a0) 233 (FCONS a1 (\n. BOTTOM))) a0 a1) /\ 234 'CTL_STRUCTURE' a1) ==> 235 'CTL_STRUCTURE' a0') ==> 236 'CTL_STRUCTURE' a0') r = 237 (dest_CTL_STRUCTURE (mk_CTL_STRUCTURE r) = r) 238 239 [CTL_STRUCTURE_size_def] Definition 240 241 |- (!a. CTL_STRUCTURE_size (BLK a) = 1 + list_size DOPER_size a) /\ 242 (!a0 a1. 243 CTL_STRUCTURE_size (SC a0 a1) = 244 1 + (CTL_STRUCTURE_size a0 + CTL_STRUCTURE_size a1)) /\ 245 (!a0 a1 a2. 246 CTL_STRUCTURE_size (CJ a0 a1 a2) = 247 1 + 248 ((\(x,y). MREG_size x + (\(x,y). COND_size x + MEXP_size y) y) a0 + 249 (CTL_STRUCTURE_size a1 + CTL_STRUCTURE_size a2))) /\ 250 !a0 a1. 251 CTL_STRUCTURE_size (TR a0 a1) = 252 1 + 253 ((\(x,y). MREG_size x + (\(x,y). COND_size x + MEXP_size y) y) a0 + 254 CTL_STRUCTURE_size a1) 255 256 [DOPER_TY_DEF] Definition 257 258 |- ?rep. 259 TYPE_DEFINITION 260 (\a0'. 261 !'DOPER'. 262 (!a0'. 263 (?a0 a1. 264 a0' = 265 (\a0 a1. 266 CONSTR 0 267 (a0,a1,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),@v. T) 268 (\n. BOTTOM)) a0 a1) \/ 269 (?a0 a1. 270 a0' = 271 (\a0 a1. 272 CONSTR (SUC 0) 273 (a1,a0,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),@v. T) 274 (\n. BOTTOM)) a0 a1) \/ 275 (?a0 a1. 276 a0' = 277 (\a0 a1. 278 CONSTR (SUC (SUC 0)) 279 (a0,(@v. T),a1,(@v. T),(@v. T),(@v. T),(@v. T),@v. T) 280 (\n. BOTTOM)) a0 a1) \/ 281 (?a0 a1 a2. 282 a0' = 283 (\a0 a1 a2. 284 CONSTR (SUC (SUC (SUC 0))) 285 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) 286 (\n. BOTTOM)) a0 a1 a2) \/ 287 (?a0 a1 a2. 288 a0' = 289 (\a0 a1 a2. 290 CONSTR (SUC (SUC (SUC (SUC 0)))) 291 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) 292 (\n. BOTTOM)) a0 a1 a2) \/ 293 (?a0 a1 a2. 294 a0' = 295 (\a0 a1 a2. 296 CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) 297 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) 298 (\n. BOTTOM)) a0 a1 a2) \/ 299 (?a0 a1 a2. 300 a0' = 301 (\a0 a1 a2. 302 CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0)))))) 303 (a0,(@v. T),(@v. T),a1,a2,(@v. T),(@v. T),@v. T) 304 (\n. BOTTOM)) a0 a1 a2) \/ 305 (?a0 a1 a2. 306 a0' = 307 (\a0 a1 a2. 308 CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))) 309 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) 310 (\n. BOTTOM)) a0 a1 a2) \/ 311 (?a0 a1 a2. 312 a0' = 313 (\a0 a1 a2. 314 CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))) 315 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) 316 (\n. BOTTOM)) a0 a1 a2) \/ 317 (?a0 a1 a2. 318 a0' = 319 (\a0 a1 a2. 320 CONSTR 321 (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))) 322 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) 323 (\n. BOTTOM)) a0 a1 a2) \/ 324 (?a0 a1 a2. 325 a0' = 326 (\a0 a1 a2. 327 CONSTR 328 (SUC 329 (SUC 330 (SUC 331 (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))) 332 (a0,(@v. T),(@v. T),a1,(@v. T),a2,(@v. T),@v. T) 333 (\n. BOTTOM)) a0 a1 a2) \/ 334 (?a0 a1 a2. 335 a0' = 336 (\a0 a1 a2. 337 CONSTR 338 (SUC 339 (SUC 340 (SUC 341 (SUC 342 (SUC 343 (SUC 344 (SUC (SUC (SUC (SUC (SUC 0))))))))))) 345 (a0,(@v. T),(@v. T),a1,(@v. T),a2,(@v. T),@v. T) 346 (\n. BOTTOM)) a0 a1 a2) \/ 347 (?a0 a1 a2. 348 a0' = 349 (\a0 a1 a2. 350 CONSTR 351 (SUC 352 (SUC 353 (SUC 354 (SUC 355 (SUC 356 (SUC 357 (SUC 358 (SUC 359 (SUC 360 (SUC (SUC (SUC 0)))))))))))) 361 (a0,(@v. T),(@v. T),a1,(@v. T),a2,(@v. T),@v. T) 362 (\n. BOTTOM)) a0 a1 a2) \/ 363 (?a0 a1 a2. 364 a0' = 365 (\a0 a1 a2. 366 CONSTR 367 (SUC 368 (SUC 369 (SUC 370 (SUC 371 (SUC 372 (SUC 373 (SUC 374 (SUC 375 (SUC 376 (SUC 377 (SUC 378 (SUC 379 (SUC 0))))))))))))) 380 (a0,(@v. T),(@v. T),a1,(@v. T),a2,(@v. T),@v. T) 381 (\n. BOTTOM)) a0 a1 a2) \/ 382 (?a0 a1. 383 a0' = 384 (\a0 a1. 385 CONSTR 386 (SUC 387 (SUC 388 (SUC 389 (SUC 390 (SUC 391 (SUC 392 (SUC 393 (SUC 394 (SUC 395 (SUC 396 (SUC 397 (SUC 398 (SUC 399 (SUC 400 0)))))))))))))) 401 ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),a0,a1) 402 (\n. BOTTOM)) a0 a1) \/ 403 (?a0 a1. 404 a0' = 405 (\a0 a1. 406 CONSTR 407 (SUC 408 (SUC 409 (SUC 410 (SUC 411 (SUC 412 (SUC 413 (SUC 414 (SUC 415 (SUC 416 (SUC 417 (SUC 418 (SUC 419 (SUC 420 (SUC 421 (SUC 422 0))))))))))))))) 423 ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),a0,a1) 424 (\n. BOTTOM)) a0 a1) ==> 425 'DOPER' a0') ==> 426 'DOPER' a0') rep 427 428 [DOPER_case_def] Definition 429 430 |- (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 a0 a1. 431 DOPER_case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 432 (MLDR a0 a1) = 433 f a0 a1) /\ 434 (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 a0 a1. 435 DOPER_case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 436 (MSTR a0 a1) = 437 f1 a0 a1) /\ 438 (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 a0 a1. 439 DOPER_case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 440 (MMOV a0 a1) = 441 f2 a0 a1) /\ 442 (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 a0 a1 a2. 443 DOPER_case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 444 (MADD a0 a1 a2) = 445 f3 a0 a1 a2) /\ 446 (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 a0 a1 a2. 447 DOPER_case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 448 (MSUB a0 a1 a2) = 449 f4 a0 a1 a2) /\ 450 (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 a0 a1 a2. 451 DOPER_case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 452 (MRSB a0 a1 a2) = 453 f5 a0 a1 a2) /\ 454 (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 a0 a1 a2. 455 DOPER_case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 456 (MMUL a0 a1 a2) = 457 f6 a0 a1 a2) /\ 458 (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 a0 a1 a2. 459 DOPER_case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 460 (MAND a0 a1 a2) = 461 f7 a0 a1 a2) /\ 462 (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 a0 a1 a2. 463 DOPER_case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 464 (MORR a0 a1 a2) = 465 f8 a0 a1 a2) /\ 466 (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 a0 a1 a2. 467 DOPER_case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 468 (MEOR a0 a1 a2) = 469 f9 a0 a1 a2) /\ 470 (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 a0 a1 a2. 471 DOPER_case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 472 (MLSL a0 a1 a2) = 473 f10 a0 a1 a2) /\ 474 (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 a0 a1 a2. 475 DOPER_case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 476 (MLSR a0 a1 a2) = 477 f11 a0 a1 a2) /\ 478 (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 a0 a1 a2. 479 DOPER_case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 480 (MASR a0 a1 a2) = 481 f12 a0 a1 a2) /\ 482 (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 a0 a1 a2. 483 DOPER_case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 484 (MROR a0 a1 a2) = 485 f13 a0 a1 a2) /\ 486 (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 a0 a1. 487 DOPER_case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 488 (MPUSH a0 a1) = 489 f14 a0 a1) /\ 490 !f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 a0 a1. 491 DOPER_case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 492 (MPOP a0 a1) = 493 f15 a0 a1 494 495 [DOPER_repfns] Definition 496 497 |- (!a. mk_DOPER (dest_DOPER a) = a) /\ 498 !r. 499 (\a0'. 500 !'DOPER'. 501 (!a0'. 502 (?a0 a1. 503 a0' = 504 (\a0 a1. 505 CONSTR 0 506 (a0,a1,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),@v. T) 507 (\n. BOTTOM)) a0 a1) \/ 508 (?a0 a1. 509 a0' = 510 (\a0 a1. 511 CONSTR (SUC 0) 512 (a1,a0,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),@v. T) 513 (\n. BOTTOM)) a0 a1) \/ 514 (?a0 a1. 515 a0' = 516 (\a0 a1. 517 CONSTR (SUC (SUC 0)) 518 (a0,(@v. T),a1,(@v. T),(@v. T),(@v. T),(@v. T),@v. T) 519 (\n. BOTTOM)) a0 a1) \/ 520 (?a0 a1 a2. 521 a0' = 522 (\a0 a1 a2. 523 CONSTR (SUC (SUC (SUC 0))) 524 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) 525 (\n. BOTTOM)) a0 a1 a2) \/ 526 (?a0 a1 a2. 527 a0' = 528 (\a0 a1 a2. 529 CONSTR (SUC (SUC (SUC (SUC 0)))) 530 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) 531 (\n. BOTTOM)) a0 a1 a2) \/ 532 (?a0 a1 a2. 533 a0' = 534 (\a0 a1 a2. 535 CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) 536 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) 537 (\n. BOTTOM)) a0 a1 a2) \/ 538 (?a0 a1 a2. 539 a0' = 540 (\a0 a1 a2. 541 CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0)))))) 542 (a0,(@v. T),(@v. T),a1,a2,(@v. T),(@v. T),@v. T) 543 (\n. BOTTOM)) a0 a1 a2) \/ 544 (?a0 a1 a2. 545 a0' = 546 (\a0 a1 a2. 547 CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))) 548 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) 549 (\n. BOTTOM)) a0 a1 a2) \/ 550 (?a0 a1 a2. 551 a0' = 552 (\a0 a1 a2. 553 CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))) 554 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) 555 (\n. BOTTOM)) a0 a1 a2) \/ 556 (?a0 a1 a2. 557 a0' = 558 (\a0 a1 a2. 559 CONSTR 560 (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))) 561 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) 562 (\n. BOTTOM)) a0 a1 a2) \/ 563 (?a0 a1 a2. 564 a0' = 565 (\a0 a1 a2. 566 CONSTR 567 (SUC 568 (SUC 569 (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))) 570 (a0,(@v. T),(@v. T),a1,(@v. T),a2,(@v. T),@v. T) 571 (\n. BOTTOM)) a0 a1 a2) \/ 572 (?a0 a1 a2. 573 a0' = 574 (\a0 a1 a2. 575 CONSTR 576 (SUC 577 (SUC 578 (SUC 579 (SUC 580 (SUC 581 (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))) 582 (a0,(@v. T),(@v. T),a1,(@v. T),a2,(@v. T),@v. T) 583 (\n. BOTTOM)) a0 a1 a2) \/ 584 (?a0 a1 a2. 585 a0' = 586 (\a0 a1 a2. 587 CONSTR 588 (SUC 589 (SUC 590 (SUC 591 (SUC 592 (SUC 593 (SUC 594 (SUC 595 (SUC 596 (SUC (SUC (SUC (SUC 0)))))))))))) 597 (a0,(@v. T),(@v. T),a1,(@v. T),a2,(@v. T),@v. T) 598 (\n. BOTTOM)) a0 a1 a2) \/ 599 (?a0 a1 a2. 600 a0' = 601 (\a0 a1 a2. 602 CONSTR 603 (SUC 604 (SUC 605 (SUC 606 (SUC 607 (SUC 608 (SUC 609 (SUC 610 (SUC 611 (SUC 612 (SUC 613 (SUC 614 (SUC (SUC 0))))))))))))) 615 (a0,(@v. T),(@v. T),a1,(@v. T),a2,(@v. T),@v. T) 616 (\n. BOTTOM)) a0 a1 a2) \/ 617 (?a0 a1. 618 a0' = 619 (\a0 a1. 620 CONSTR 621 (SUC 622 (SUC 623 (SUC 624 (SUC 625 (SUC 626 (SUC 627 (SUC 628 (SUC 629 (SUC 630 (SUC 631 (SUC 632 (SUC 633 (SUC 634 (SUC 635 0)))))))))))))) 636 ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),a0,a1) 637 (\n. BOTTOM)) a0 a1) \/ 638 (?a0 a1. 639 a0' = 640 (\a0 a1. 641 CONSTR 642 (SUC 643 (SUC 644 (SUC 645 (SUC 646 (SUC 647 (SUC 648 (SUC 649 (SUC 650 (SUC 651 (SUC 652 (SUC 653 (SUC 654 (SUC 655 (SUC 656 (SUC 657 0))))))))))))))) 658 ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),a0,a1) 659 (\n. BOTTOM)) a0 a1) ==> 660 'DOPER' a0') ==> 661 'DOPER' a0') r = 662 (dest_DOPER (mk_DOPER r) = r) 663 664 [DOPER_size_def] Definition 665 666 |- (!a0 a1. 667 DOPER_size (MLDR a0 a1) = 668 1 + (MREG_size a0 + (\(x,y). (\x. x) x + OFFSET_size y) a1)) /\ 669 (!a0 a1. 670 DOPER_size (MSTR a0 a1) = 671 1 + ((\(x,y). (\x. x) x + OFFSET_size y) a0 + MREG_size a1)) /\ 672 (!a0 a1. DOPER_size (MMOV a0 a1) = 1 + (MREG_size a0 + MEXP_size a1)) /\ 673 (!a0 a1 a2. 674 DOPER_size (MADD a0 a1 a2) = 675 1 + (MREG_size a0 + (MREG_size a1 + MEXP_size a2))) /\ 676 (!a0 a1 a2. 677 DOPER_size (MSUB a0 a1 a2) = 678 1 + (MREG_size a0 + (MREG_size a1 + MEXP_size a2))) /\ 679 (!a0 a1 a2. 680 DOPER_size (MRSB a0 a1 a2) = 681 1 + (MREG_size a0 + (MREG_size a1 + MEXP_size a2))) /\ 682 (!a0 a1 a2. 683 DOPER_size (MMUL a0 a1 a2) = 684 1 + (MREG_size a0 + (MREG_size a1 + MREG_size a2))) /\ 685 (!a0 a1 a2. 686 DOPER_size (MAND a0 a1 a2) = 687 1 + (MREG_size a0 + (MREG_size a1 + MEXP_size a2))) /\ 688 (!a0 a1 a2. 689 DOPER_size (MORR a0 a1 a2) = 690 1 + (MREG_size a0 + (MREG_size a1 + MEXP_size a2))) /\ 691 (!a0 a1 a2. 692 DOPER_size (MEOR a0 a1 a2) = 693 1 + (MREG_size a0 + (MREG_size a1 + MEXP_size a2))) /\ 694 (!a0 a1 a2. 695 DOPER_size (MLSL a0 a1 a2) = 1 + (MREG_size a0 + MREG_size a1)) /\ 696 (!a0 a1 a2. 697 DOPER_size (MLSR a0 a1 a2) = 1 + (MREG_size a0 + MREG_size a1)) /\ 698 (!a0 a1 a2. 699 DOPER_size (MASR a0 a1 a2) = 1 + (MREG_size a0 + MREG_size a1)) /\ 700 (!a0 a1 a2. 701 DOPER_size (MROR a0 a1 a2) = 1 + (MREG_size a0 + MREG_size a1)) /\ 702 (!a0 a1. DOPER_size (MPUSH a0 a1) = 1 + (a0 + list_size (\x. x) a1)) /\ 703 !a0 a1. DOPER_size (MPOP a0 a1) = 1 + (a0 + list_size (\x. x) a1) 704 705 [IL0_def] Definition 706 707 |- IL0 = (\a. mk_MEXP ((\a. CONSTR 0 (a,(@v. T),@v. T) (\n. BOTTOM)) a)) 708 709 [IL10_def] Definition 710 711 |- IL10 = 712 (\a0 a1 a2. 713 mk_DOPER 714 ((\a0 a1 a2. 715 CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))) 716 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a0 717 a1 a2)) 718 719 [IL11_def] Definition 720 721 |- IL11 = 722 (\a0 a1 a2. 723 mk_DOPER 724 ((\a0 a1 a2. 725 CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))) 726 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a0 727 a1 a2)) 728 729 [IL12_def] Definition 730 731 |- IL12 = 732 (\a0 a1 a2. 733 mk_DOPER 734 ((\a0 a1 a2. 735 CONSTR 736 (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))) 737 (a0,(@v. T),(@v. T),a1,(@v. T),a2,(@v. T),@v. T) (\n. BOTTOM)) a0 738 a1 a2)) 739 740 [IL13_def] Definition 741 742 |- IL13 = 743 (\a0 a1 a2. 744 mk_DOPER 745 ((\a0 a1 a2. 746 CONSTR 747 (SUC 748 (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))) 749 (a0,(@v. T),(@v. T),a1,(@v. T),a2,(@v. T),@v. T) (\n. BOTTOM)) a0 750 a1 a2)) 751 752 [IL14_def] Definition 753 754 |- IL14 = 755 (\a0 a1 a2. 756 mk_DOPER 757 ((\a0 a1 a2. 758 CONSTR 759 (SUC 760 (SUC 761 (SUC 762 (SUC 763 (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))))) 764 (a0,(@v. T),(@v. T),a1,(@v. T),a2,(@v. T),@v. T) (\n. BOTTOM)) a0 765 a1 a2)) 766 767 [IL15_def] Definition 768 769 |- IL15 = 770 (\a0 a1 a2. 771 mk_DOPER 772 ((\a0 a1 a2. 773 CONSTR 774 (SUC 775 (SUC 776 (SUC 777 (SUC 778 (SUC 779 (SUC 780 (SUC 781 (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))))) 782 (a0,(@v. T),(@v. T),a1,(@v. T),a2,(@v. T),@v. T) (\n. BOTTOM)) a0 783 a1 a2)) 784 785 [IL16_def] Definition 786 787 |- IL16 = 788 (\a0 a1. 789 mk_DOPER 790 ((\a0 a1. 791 CONSTR 792 (SUC 793 (SUC 794 (SUC 795 (SUC 796 (SUC 797 (SUC 798 (SUC 799 (SUC 800 (SUC 801 (SUC 802 (SUC (SUC (SUC (SUC 0)))))))))))))) 803 ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),a0,a1) 804 (\n. BOTTOM)) a0 a1)) 805 806 [IL17_def] Definition 807 808 |- IL17 = 809 (\a0 a1. 810 mk_DOPER 811 ((\a0 a1. 812 CONSTR 813 (SUC 814 (SUC 815 (SUC 816 (SUC 817 (SUC 818 (SUC 819 (SUC 820 (SUC 821 (SUC 822 (SUC 823 (SUC 824 (SUC 825 (SUC 826 (SUC (SUC 0))))))))))))))) 827 ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),a0,a1) 828 (\n. BOTTOM)) a0 a1)) 829 830 [IL18_def] Definition 831 832 |- IL18 = (\a. mk_CTL_STRUCTURE ((\a. CONSTR 0 (a,@v. T) (\n. BOTTOM)) a)) 833 834 [IL19_def] Definition 835 836 |- IL19 = 837 (\a0 a1. 838 mk_CTL_STRUCTURE 839 ((\a0 a1. 840 CONSTR (SUC 0) ((@v. T),@v. T) (FCONS a0 (FCONS a1 (\n. BOTTOM)))) 841 (dest_CTL_STRUCTURE a0) (dest_CTL_STRUCTURE a1))) 842 843 [IL1_def] Definition 844 845 |- IL1 = 846 (\a0 a1. 847 mk_MEXP ((\a0 a1. CONSTR (SUC 0) ((@v. T),a0,a1) (\n. BOTTOM)) a0 a1)) 848 849 [IL20_def] Definition 850 851 |- IL20 = 852 (\a0 a1 a2. 853 mk_CTL_STRUCTURE 854 ((\a0 a1 a2. 855 CONSTR (SUC (SUC 0)) ((@v. T),a0) 856 (FCONS a1 (FCONS a2 (\n. BOTTOM)))) a0 (dest_CTL_STRUCTURE a1) 857 (dest_CTL_STRUCTURE a2))) 858 859 [IL21_def] Definition 860 861 |- IL21 = 862 (\a0 a1. 863 mk_CTL_STRUCTURE 864 ((\a0 a1. 865 CONSTR (SUC (SUC (SUC 0))) ((@v. T),a0) (FCONS a1 (\n. BOTTOM))) a0 866 (dest_CTL_STRUCTURE a1))) 867 868 [IL2_def] Definition 869 870 |- IL2 = 871 (\a0 a1. 872 mk_DOPER 873 ((\a0 a1. 874 CONSTR 0 (a0,a1,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),@v. T) 875 (\n. BOTTOM)) a0 a1)) 876 877 [IL3_def] Definition 878 879 |- IL3 = 880 (\a0 a1. 881 mk_DOPER 882 ((\a0 a1. 883 CONSTR (SUC 0) 884 (a1,a0,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),@v. T) 885 (\n. BOTTOM)) a0 a1)) 886 887 [IL4_def] Definition 888 889 |- IL4 = 890 (\a0 a1. 891 mk_DOPER 892 ((\a0 a1. 893 CONSTR (SUC (SUC 0)) 894 (a0,(@v. T),a1,(@v. T),(@v. T),(@v. T),(@v. T),@v. T) 895 (\n. BOTTOM)) a0 a1)) 896 897 [IL5_def] Definition 898 899 |- IL5 = 900 (\a0 a1 a2. 901 mk_DOPER 902 ((\a0 a1 a2. 903 CONSTR (SUC (SUC (SUC 0))) 904 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a0 905 a1 a2)) 906 907 [IL6_def] Definition 908 909 |- IL6 = 910 (\a0 a1 a2. 911 mk_DOPER 912 ((\a0 a1 a2. 913 CONSTR (SUC (SUC (SUC (SUC 0)))) 914 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a0 915 a1 a2)) 916 917 [IL7_def] Definition 918 919 |- IL7 = 920 (\a0 a1 a2. 921 mk_DOPER 922 ((\a0 a1 a2. 923 CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) 924 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a0 925 a1 a2)) 926 927 [IL8_def] Definition 928 929 |- IL8 = 930 (\a0 a1 a2. 931 mk_DOPER 932 ((\a0 a1 a2. 933 CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0)))))) 934 (a0,(@v. T),(@v. T),a1,a2,(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a0 935 a1 a2)) 936 937 [IL9_def] Definition 938 939 |- IL9 = 940 (\a0 a1 a2. 941 mk_DOPER 942 ((\a0 a1 a2. 943 CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))) 944 (a0,(@v. T),a2,a1,(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a0 945 a1 a2)) 946 947 [MADD] Definition 948 949 |- MADD = IL5 950 951 [MAND] Definition 952 953 |- MAND = IL9 954 955 [MASR] Definition 956 957 |- MASR = IL14 958 959 [MC] Definition 960 961 |- MC = IL1 962 963 [MEOR] Definition 964 965 |- MEOR = IL11 966 967 [MEXP_TY_DEF] Definition 968 969 |- ?rep. 970 TYPE_DEFINITION 971 (\a0'. 972 !'MEXP'. 973 (!a0'. 974 (?a. a0' = (\a. CONSTR 0 (a,(@v. T),@v. T) (\n. BOTTOM)) a) \/ 975 (?a0 a1. 976 a0' = 977 (\a0 a1. CONSTR (SUC 0) ((@v. T),a0,a1) (\n. BOTTOM)) a0 978 a1) ==> 979 'MEXP' a0') ==> 980 'MEXP' a0') rep 981 982 [MEXP_case_def] Definition 983 984 |- (!f f1 a. MEXP_case f f1 (MR a) = f a) /\ 985 !f f1 a0 a1. MEXP_case f f1 (MC a0 a1) = f1 a0 a1 986 987 [MEXP_repfns] Definition 988 989 |- (!a. mk_MEXP (dest_MEXP a) = a) /\ 990 !r. 991 (\a0'. 992 !'MEXP'. 993 (!a0'. 994 (?a. a0' = (\a. CONSTR 0 (a,(@v. T),@v. T) (\n. BOTTOM)) a) \/ 995 (?a0 a1. 996 a0' = 997 (\a0 a1. CONSTR (SUC 0) ((@v. T),a0,a1) (\n. BOTTOM)) a0 998 a1) ==> 999 'MEXP' a0') ==> 1000 'MEXP' a0') r = 1001 (dest_MEXP (mk_MEXP r) = r) 1002 1003 [MEXP_size_def] Definition 1004 1005 |- (!a. MEXP_size (MR a) = 1 + MREG_size a) /\ !a0 a1. MEXP_size (MC a0 a1) = 1 1006 1007 [MLDR] Definition 1008 1009 |- MLDR = IL2 1010 1011 [MLSL] Definition 1012 1013 |- MLSL = IL12 1014 1015 [MLSR] Definition 1016 1017 |- MLSR = IL13 1018 1019 [MMOV] Definition 1020 1021 |- MMOV = IL4 1022 1023 [MMUL] Definition 1024 1025 |- MMUL = IL8 1026 1027 [MORR] Definition 1028 1029 |- MORR = IL10 1030 1031 [MPOP] Definition 1032 1033 |- MPOP = IL17 1034 1035 [MPUSH] Definition 1036 1037 |- MPUSH = IL16 1038 1039 [MR] Definition 1040 1041 |- MR = IL0 1042 1043 [MREG_BIJ] Definition 1044 1045 |- (!a. num2MREG (MREG2num a) = a) /\ 1046 !r. (\n. n < 15) r = (MREG2num (num2MREG r) = r) 1047 1048 [MREG_TY_DEF] Definition 1049 1050 |- ?rep. TYPE_DEFINITION (\n. n < 15) rep 1051 1052 [MREG_case] Definition 1053 1054 |- !v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 x. 1055 (case x of 1056 R0 -> v0 1057 || R1 -> v1 1058 || R2 -> v2 1059 || R3 -> v3 1060 || R4 -> v4 1061 || R5 -> v5 1062 || R6 -> v6 1063 || R7 -> v7 1064 || R8 -> v8 1065 || R9 -> v9 1066 || R10 -> v10 1067 || R11 -> v11 1068 || R12 -> v12 1069 || R13 -> v13 1070 || R14 -> v14) = 1071 (\m. 1072 (if m < 7 then 1073 (if m < 3 then 1074 (if m < 1 then v0 else (if m = 1 then v1 else v2)) 1075 else 1076 (if m < 4 then 1077 v3 1078 else 1079 (if m < 5 then v4 else (if m = 5 then v5 else v6)))) 1080 else 1081 (if m < 10 then 1082 (if m < 8 then v7 else (if m = 8 then v8 else v9)) 1083 else 1084 (if m < 12 then 1085 (if m = 10 then v10 else v11) 1086 else 1087 (if m < 13 then v12 else (if m = 13 then v13 else v14)))))) 1088 (MREG2num x) 1089 1090 [MREG_size_def] Definition 1091 1092 |- !x. MREG_size x = 0 1093 1094 [MROR] Definition 1095 1096 |- MROR = IL15 1097 1098 [MRSB] Definition 1099 1100 |- MRSB = IL7 1101 1102 [MSTR] Definition 1103 1104 |- MSTR = IL3 1105 1106 [MSUB] Definition 1107 1108 |- MSUB = IL6 1109 1110 [R0] Definition 1111 1112 |- R0 = num2MREG 0 1113 1114 [R1] Definition 1115 1116 |- R1 = num2MREG 1 1117 1118 [R10] Definition 1119 1120 |- R10 = num2MREG 10 1121 1122 [R11] Definition 1123 1124 |- R11 = num2MREG 11 1125 1126 [R12] Definition 1127 1128 |- R12 = num2MREG 12 1129 1130 [R13] Definition 1131 1132 |- R13 = num2MREG 13 1133 1134 [R14] Definition 1135 1136 |- R14 = num2MREG 14 1137 1138 [R2] Definition 1139 1140 |- R2 = num2MREG 2 1141 1142 [R3] Definition 1143 1144 |- R3 = num2MREG 3 1145 1146 [R4] Definition 1147 1148 |- R4 = num2MREG 4 1149 1150 [R5] Definition 1151 1152 |- R5 = num2MREG 5 1153 1154 [R6] Definition 1155 1156 |- R6 = num2MREG 6 1157 1158 [R7] Definition 1159 1160 |- R7 = num2MREG 7 1161 1162 [R8] Definition 1163 1164 |- R8 = num2MREG 8 1165 1166 [R9] Definition 1167 1168 |- R9 = num2MREG 9 1169 1170 [SC] Definition 1171 1172 |- SC = IL19 1173 1174 [TR] Definition 1175 1176 |- TR = IL21 1177 1178 [WELL_FORMED_SUB_def] Definition 1179 1180 |- (!stmL. WELL_FORMED_SUB (BLK stmL) = T) /\ 1181 (!S1 S2. WELL_FORMED_SUB (SC S1 S2) = WELL_FORMED S1 /\ WELL_FORMED S2) /\ 1182 (!cond S1 S2. 1183 WELL_FORMED_SUB (CJ cond S1 S2) = WELL_FORMED S1 /\ WELL_FORMED S2) /\ 1184 !cond S1. 1185 WELL_FORMED_SUB (TR cond S1) = 1186 WELL_FORMED S1 /\ WF_TR (translate_condition cond,translate S1) 1187 1188 [WELL_FORMED_def] Definition 1189 1190 |- (!stmL. WELL_FORMED (BLK stmL) = well_formed (translate (BLK stmL))) /\ 1191 (!S1 S2. 1192 WELL_FORMED (SC S1 S2) = 1193 well_formed (translate (SC S1 S2)) /\ WELL_FORMED S1 /\ 1194 WELL_FORMED S2) /\ 1195 (!cond S1 S2. 1196 WELL_FORMED (CJ cond S1 S2) = 1197 well_formed (translate (CJ cond S1 S2)) /\ WELL_FORMED S1 /\ 1198 WELL_FORMED S2) /\ 1199 !cond S1. 1200 WELL_FORMED (TR cond S1) = 1201 well_formed (translate (TR cond S1)) /\ WELL_FORMED S1 /\ 1202 WF_TR (translate_condition cond,translate S1) 1203 1204 [eval_il_cond_def] Definition 1205 1206 |- !cond. eval_il_cond cond = eval_cond (translate_condition cond) 1207 1208 [from_reg_index_def] Definition 1209 1210 |- !i. 1211 from_reg_index i = 1212 (if i = 0 then 1213 R0 1214 else 1215 (if i = 1 then 1216 R1 1217 else 1218 (if i = 2 then 1219 R2 1220 else 1221 (if i = 3 then 1222 R3 1223 else 1224 (if i = 4 then 1225 R4 1226 else 1227 (if i = 5 then 1228 R5 1229 else 1230 (if i = 6 then 1231 R6 1232 else 1233 (if i = 7 then 1234 R7 1235 else 1236 (if i = 8 then 1237 R8 1238 else 1239 (if i = 9 then 1240 R9 1241 else 1242 (if i = 10 then 1243 R10 1244 else 1245 (if i = 11 then 1246 R11 1247 else 1248 (if i = 12 then 1249 R12 1250 else 1251 (if i = 13 then 1252 R13 1253 else 1254 R14)))))))))))))) 1255 1256 [index_of_reg_def] Definition 1257 1258 |- (index_of_reg R0 = 0) /\ (index_of_reg R1 = 1) /\ (index_of_reg R2 = 2) /\ 1259 (index_of_reg R3 = 3) /\ (index_of_reg R4 = 4) /\ (index_of_reg R5 = 5) /\ 1260 (index_of_reg R6 = 6) /\ (index_of_reg R7 = 7) /\ (index_of_reg R8 = 8) /\ 1261 (index_of_reg R9 = 9) /\ (index_of_reg R10 = 10) /\ 1262 (index_of_reg R11 = 11) /\ (index_of_reg R12 = 12) /\ 1263 (index_of_reg R13 = 13) /\ (index_of_reg R14 = 14) 1264 1265 [mdecode_def] Definition 1266 1267 |- (!st dst src. 1268 mdecode st (MLDR dst src) = 1269 write st (toREG dst) (read st (toMEM src))) /\ 1270 (!st dst src. 1271 mdecode st (MSTR dst src) = 1272 write st (toMEM dst) (read st (toREG src))) /\ 1273 (!st dst src. 1274 mdecode st (MMOV dst src) = 1275 write st (toREG dst) (read st (toEXP src))) /\ 1276 (!st dst src1 src2. 1277 mdecode st (MADD dst src1 src2) = 1278 write st (toREG dst) (read st (toREG src1) + read st (toEXP src2))) /\ 1279 (!st dst src1 src2. 1280 mdecode st (MSUB dst src1 src2) = 1281 write st (toREG dst) (read st (toREG src1) - read st (toEXP src2))) /\ 1282 (!st dst src1 src2. 1283 mdecode st (MRSB dst src1 src2) = 1284 write st (toREG dst) (read st (toEXP src2) - read st (toREG src1))) /\ 1285 (!st dst src1 src2_reg. 1286 mdecode st (MMUL dst src1 src2_reg) = 1287 write st (toREG dst) 1288 (read st (toREG src1) * read st (toREG src2_reg))) /\ 1289 (!st dst src1 src2. 1290 mdecode st (MAND dst src1 src2) = 1291 write st (toREG dst) (read st (toREG src1) && read st (toEXP src2))) /\ 1292 (!st dst src1 src2. 1293 mdecode st (MORR dst src1 src2) = 1294 write st (toREG dst) (read st (toREG src1) !! read st (toEXP src2))) /\ 1295 (!st dst src1 src2. 1296 mdecode st (MEOR dst src1 src2) = 1297 write st (toREG dst) (read st (toREG src1) ?? read st (toEXP src2))) /\ 1298 (!st dst src2_reg src2_num. 1299 mdecode st (MLSL dst src2_reg src2_num) = 1300 write st (toREG dst) (read st (toREG src2_reg) << w2n src2_num)) /\ 1301 (!st dst src2_reg src2_num. 1302 mdecode st (MLSR dst src2_reg src2_num) = 1303 write st (toREG dst) (read st (toREG src2_reg) >>> w2n src2_num)) /\ 1304 (!st dst src2_reg src2_num. 1305 mdecode st (MASR dst src2_reg src2_num) = 1306 write st (toREG dst) (read st (toREG src2_reg) >> w2n src2_num)) /\ 1307 (!st dst src2_reg src2_num. 1308 mdecode st (MROR dst src2_reg src2_num) = 1309 write st (toREG dst) (read st (toREG src2_reg) #>> w2n src2_num)) /\ 1310 (!st dst' srcL. mdecode st (MPUSH dst' srcL) = pushL st dst' srcL) /\ 1311 !st dst' srcL. mdecode st (MPOP dst' srcL) = popL st dst' srcL 1312 1313 [popL_def] Definition 1314 1315 |- !st baseR regL. 1316 popL st baseR regL = 1317 write 1318 (FST 1319 (FOLDL 1320 (\(st1,i) reg. 1321 (write st1 reg (read st (MEM (baseR,POS (i + 1)))),i + 1)) 1322 (st,0) (MAP REG regL))) (REG baseR) 1323 (read st (REG baseR) + n2w (LENGTH regL)) 1324 1325 [pushL_def] Definition 1326 1327 |- !st baseR regL. 1328 pushL st baseR regL = 1329 write 1330 (FST 1331 (FOLDL 1332 (\(st1,i) reg. 1333 (write st1 (MEM (baseR,NEG i)) (read st reg),i + 1)) (st,0) 1334 (REVERSE (MAP REG regL)))) (REG baseR) 1335 (read st (REG baseR) - n2w (LENGTH regL)) 1336 1337 [run_arm_def] Definition 1338 1339 |- !arm pc cpsr st pcS. 1340 run_arm arm ((pc,cpsr,st),pcS) = 1341 runTo (upload arm (\i. ARB) pc) (pc + LENGTH arm) ((pc,cpsr,st),pcS) 1342 1343 [run_ir_def] Definition 1344 1345 |- !ir st. run_ir ir st = get_st (run_arm (translate ir) ((0,0w,st),{})) 1346 1347 [toEXP_def] Definition 1348 1349 |- (!r. toEXP (MR r) = toREG r) /\ 1350 !shift c. toEXP (MC shift c) = WCONST (w2w c #>> (2 * w2n shift)) 1351 1352 [toMEM_def] Definition 1353 1354 |- !base offset. toMEM (base,offset) = MEM (base,offset) 1355 1356 [toREG_def] Definition 1357 1358 |- !r. toREG r = REG (index_of_reg r) 1359 1360 [translate_assignment_def] Definition 1361 1362 |- (!dst src. 1363 translate_assignment (MMOV dst src) = 1364 ((MOV,NONE,F),SOME (toREG dst),[toEXP src],NONE)) /\ 1365 (!dst src1 src2. 1366 translate_assignment (MADD dst src1 src2) = 1367 ((ADD,NONE,F),SOME (toREG dst),[toREG src1; toEXP src2],NONE)) /\ 1368 (!dst src1 src2. 1369 translate_assignment (MSUB dst src1 src2) = 1370 ((SUB,NONE,F),SOME (toREG dst),[toREG src1; toEXP src2],NONE)) /\ 1371 (!dst src1 src2. 1372 translate_assignment (MRSB dst src1 src2) = 1373 ((RSB,NONE,F),SOME (toREG dst),[toREG src1; toEXP src2],NONE)) /\ 1374 (!dst src1 src2_reg. 1375 translate_assignment (MMUL dst src1 src2_reg) = 1376 ((MUL,NONE,F),SOME (toREG dst),[toREG src1; toREG src2_reg],NONE)) /\ 1377 (!dst src1 src2. 1378 translate_assignment (MAND dst src1 src2) = 1379 ((AND,NONE,F),SOME (toREG dst),[toREG src1; toEXP src2],NONE)) /\ 1380 (!dst src1 src2. 1381 translate_assignment (MORR dst src1 src2) = 1382 ((ORR,NONE,F),SOME (toREG dst),[toREG src1; toEXP src2],NONE)) /\ 1383 (!dst src1 src2. 1384 translate_assignment (MEOR dst src1 src2) = 1385 ((EOR,NONE,F),SOME (toREG dst),[toREG src1; toEXP src2],NONE)) /\ 1386 (!dst src2_reg src2_num. 1387 translate_assignment (MLSL dst src2_reg src2_num) = 1388 ((LSL,NONE,F),SOME (toREG dst),[toREG src2_reg; WCONST (w2w src2_num)], 1389 NONE)) /\ 1390 (!dst src2_reg src2_num. 1391 translate_assignment (MLSR dst src2_reg src2_num) = 1392 ((LSR,NONE,F),SOME (toREG dst),[toREG src2_reg; WCONST (w2w src2_num)], 1393 NONE)) /\ 1394 (!dst src2_reg src2_num. 1395 translate_assignment (MASR dst src2_reg src2_num) = 1396 ((ASR,NONE,F),SOME (toREG dst),[toREG src2_reg; WCONST (w2w src2_num)], 1397 NONE)) /\ 1398 (!dst src2_reg src2_num. 1399 translate_assignment (MROR dst src2_reg src2_num) = 1400 ((ROR,NONE,F),SOME (toREG dst),[toREG src2_reg; WCONST (w2w src2_num)], 1401 NONE)) /\ 1402 (!dst src. 1403 translate_assignment (MLDR dst src) = 1404 ((LDR,NONE,F),SOME (toREG dst),[toMEM src],NONE)) /\ 1405 (!dst src. 1406 translate_assignment (MSTR dst src) = 1407 ((STR,NONE,F),SOME (toREG src),[toMEM dst],NONE)) /\ 1408 (!dst srcL. 1409 translate_assignment (MPUSH dst srcL) = 1410 ((STMFD,NONE,F),SOME (WREG dst),MAP REG srcL,NONE)) /\ 1411 !dst srcL. 1412 translate_assignment (MPOP dst srcL) = 1413 ((LDMFD,NONE,F),SOME (WREG dst),MAP REG srcL,NONE) 1414 1415 [translate_condition_def] Definition 1416 1417 |- !r c e. translate_condition (r,c,e) = (toREG r,c,toEXP e) 1418 1419 [translate_primitive_def] Definition 1420 1421 |- translate = 1422 WFREC 1423 (@R. 1424 WF R /\ (!stm stmL. R (BLK stmL) (BLK (stm::stmL))) /\ 1425 (!S1 S2. R S2 (SC S1 S2)) /\ (!S2 S1. R S1 (SC S1 S2)) /\ 1426 (!Sfalse cond Strue. R Strue (CJ cond Strue Sfalse)) /\ 1427 (!Strue cond Sfalse. R Sfalse (CJ cond Strue Sfalse)) /\ 1428 !cond Sbody. R Sbody (TR cond Sbody)) 1429 (\translate a. 1430 case a of 1431 BLK [] -> I [] 1432 || BLK (stm::stmL) -> 1433 I (translate_assignment stm::translate (BLK stmL)) 1434 || SC S1 S2 -> I (mk_SC (translate S1) (translate S2)) 1435 || CJ cond Strue Sfalse -> 1436 I 1437 (mk_CJ (translate_condition cond) (translate Strue) 1438 (translate Sfalse)) 1439 || TR cond' Sbody -> 1440 I (mk_TR (translate_condition cond') (translate Sbody))) 1441 1442 [BLOCK_IS_WELL_FORMED] Theorem 1443 1444 |- !stmL. WELL_FORMED (BLK stmL) 1445 1446 [CTL_STRUCTURE_11] Theorem 1447 1448 |- (!a a'. (BLK a = BLK a') = (a = a')) /\ 1449 (!a0 a1 a0' a1'. (SC a0 a1 = SC a0' a1') = (a0 = a0') /\ (a1 = a1')) /\ 1450 (!a0 a1 a2 a0' a1' a2'. 1451 (CJ a0 a1 a2 = CJ a0' a1' a2') = 1452 (a0 = a0') /\ (a1 = a1') /\ (a2 = a2')) /\ 1453 !a0 a1 a0' a1'. (TR a0 a1 = TR a0' a1') = (a0 = a0') /\ (a1 = a1') 1454 1455 [CTL_STRUCTURE_Axiom] Theorem 1456 1457 |- !f0 f1 f2 f3. 1458 ?fn. 1459 (!a. fn (BLK a) = f0 a) /\ 1460 (!a0 a1. fn (SC a0 a1) = f1 a0 a1 (fn a0) (fn a1)) /\ 1461 (!a0 a1 a2. fn (CJ a0 a1 a2) = f2 a0 a1 a2 (fn a1) (fn a2)) /\ 1462 !a0 a1. fn (TR a0 a1) = f3 a0 a1 (fn a1) 1463 1464 [CTL_STRUCTURE_case_cong] Theorem 1465 1466 |- !M M' f f1 f2 f3. 1467 (M = M') /\ (!a. (M' = BLK a) ==> (f a = f' a)) /\ 1468 (!a0 a1. (M' = SC a0 a1) ==> (f1 a0 a1 = f1' a0 a1)) /\ 1469 (!a0 a1 a2. (M' = CJ a0 a1 a2) ==> (f2 a0 a1 a2 = f2' a0 a1 a2)) /\ 1470 (!a0 a1. (M' = TR a0 a1) ==> (f3 a0 a1 = f3' a0 a1)) ==> 1471 (CTL_STRUCTURE_case f f1 f2 f3 M = CTL_STRUCTURE_case f' f1' f2' f3' M') 1472 1473 [CTL_STRUCTURE_distinct] Theorem 1474 1475 |- (!a1 a0 a. ~(BLK a = SC a0 a1)) /\ (!a2 a1 a0 a. ~(BLK a = CJ a0 a1 a2)) /\ 1476 (!a1 a0 a. ~(BLK a = TR a0 a1)) /\ 1477 (!a2 a1' a1 a0' a0. ~(SC a0 a1 = CJ a0' a1' a2)) /\ 1478 (!a1' a1 a0' a0. ~(SC a0 a1 = TR a0' a1')) /\ 1479 !a2 a1' a1 a0' a0. ~(CJ a0 a1 a2 = TR a0' a1') 1480 1481 [CTL_STRUCTURE_induction] Theorem 1482 1483 |- !P. 1484 (!l. P (BLK l)) /\ (!C C0. P C /\ P C0 ==> P (SC C C0)) /\ 1485 (!C C0. P C /\ P C0 ==> !p. P (CJ p C C0)) /\ 1486 (!C. P C ==> !p. P (TR p C)) ==> 1487 !C. P C 1488 1489 [CTL_STRUCTURE_nchotomy] Theorem 1490 1491 |- !C. 1492 (?l. C = BLK l) \/ (?C' C0. C = SC C' C0) \/ (?p C' C0. C = CJ p C' C0) \/ 1493 ?p C'. C = TR p C' 1494 1495 [DOPER_11] Theorem 1496 1497 |- (!a0 a1 a0' a1'. (MLDR a0 a1 = MLDR a0' a1') = (a0 = a0') /\ (a1 = a1')) /\ 1498 (!a0 a1 a0' a1'. (MSTR a0 a1 = MSTR a0' a1') = (a0 = a0') /\ (a1 = a1')) /\ 1499 (!a0 a1 a0' a1'. (MMOV a0 a1 = MMOV a0' a1') = (a0 = a0') /\ (a1 = a1')) /\ 1500 (!a0 a1 a2 a0' a1' a2'. 1501 (MADD a0 a1 a2 = MADD a0' a1' a2') = 1502 (a0 = a0') /\ (a1 = a1') /\ (a2 = a2')) /\ 1503 (!a0 a1 a2 a0' a1' a2'. 1504 (MSUB a0 a1 a2 = MSUB a0' a1' a2') = 1505 (a0 = a0') /\ (a1 = a1') /\ (a2 = a2')) /\ 1506 (!a0 a1 a2 a0' a1' a2'. 1507 (MRSB a0 a1 a2 = MRSB a0' a1' a2') = 1508 (a0 = a0') /\ (a1 = a1') /\ (a2 = a2')) /\ 1509 (!a0 a1 a2 a0' a1' a2'. 1510 (MMUL a0 a1 a2 = MMUL a0' a1' a2') = 1511 (a0 = a0') /\ (a1 = a1') /\ (a2 = a2')) /\ 1512 (!a0 a1 a2 a0' a1' a2'. 1513 (MAND a0 a1 a2 = MAND a0' a1' a2') = 1514 (a0 = a0') /\ (a1 = a1') /\ (a2 = a2')) /\ 1515 (!a0 a1 a2 a0' a1' a2'. 1516 (MORR a0 a1 a2 = MORR a0' a1' a2') = 1517 (a0 = a0') /\ (a1 = a1') /\ (a2 = a2')) /\ 1518 (!a0 a1 a2 a0' a1' a2'. 1519 (MEOR a0 a1 a2 = MEOR a0' a1' a2') = 1520 (a0 = a0') /\ (a1 = a1') /\ (a2 = a2')) /\ 1521 (!a0 a1 a2 a0' a1' a2'. 1522 (MLSL a0 a1 a2 = MLSL a0' a1' a2') = 1523 (a0 = a0') /\ (a1 = a1') /\ (a2 = a2')) /\ 1524 (!a0 a1 a2 a0' a1' a2'. 1525 (MLSR a0 a1 a2 = MLSR a0' a1' a2') = 1526 (a0 = a0') /\ (a1 = a1') /\ (a2 = a2')) /\ 1527 (!a0 a1 a2 a0' a1' a2'. 1528 (MASR a0 a1 a2 = MASR a0' a1' a2') = 1529 (a0 = a0') /\ (a1 = a1') /\ (a2 = a2')) /\ 1530 (!a0 a1 a2 a0' a1' a2'. 1531 (MROR a0 a1 a2 = MROR a0' a1' a2') = 1532 (a0 = a0') /\ (a1 = a1') /\ (a2 = a2')) /\ 1533 (!a0 a1 a0' a1'. 1534 (MPUSH a0 a1 = MPUSH a0' a1') = (a0 = a0') /\ (a1 = a1')) /\ 1535 !a0 a1 a0' a1'. (MPOP a0 a1 = MPOP a0' a1') = (a0 = a0') /\ (a1 = a1') 1536 1537 [DOPER_Axiom] Theorem 1538 1539 |- !f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15. 1540 ?fn. 1541 (!a0 a1. fn (MLDR a0 a1) = f0 a0 a1) /\ 1542 (!a0 a1. fn (MSTR a0 a1) = f1 a0 a1) /\ 1543 (!a0 a1. fn (MMOV a0 a1) = f2 a0 a1) /\ 1544 (!a0 a1 a2. fn (MADD a0 a1 a2) = f3 a0 a1 a2) /\ 1545 (!a0 a1 a2. fn (MSUB a0 a1 a2) = f4 a0 a1 a2) /\ 1546 (!a0 a1 a2. fn (MRSB a0 a1 a2) = f5 a0 a1 a2) /\ 1547 (!a0 a1 a2. fn (MMUL a0 a1 a2) = f6 a0 a1 a2) /\ 1548 (!a0 a1 a2. fn (MAND a0 a1 a2) = f7 a0 a1 a2) /\ 1549 (!a0 a1 a2. fn (MORR a0 a1 a2) = f8 a0 a1 a2) /\ 1550 (!a0 a1 a2. fn (MEOR a0 a1 a2) = f9 a0 a1 a2) /\ 1551 (!a0 a1 a2. fn (MLSL a0 a1 a2) = f10 a0 a1 a2) /\ 1552 (!a0 a1 a2. fn (MLSR a0 a1 a2) = f11 a0 a1 a2) /\ 1553 (!a0 a1 a2. fn (MASR a0 a1 a2) = f12 a0 a1 a2) /\ 1554 (!a0 a1 a2. fn (MROR a0 a1 a2) = f13 a0 a1 a2) /\ 1555 (!a0 a1. fn (MPUSH a0 a1) = f14 a0 a1) /\ 1556 !a0 a1. fn (MPOP a0 a1) = f15 a0 a1 1557 1558 [DOPER_case_cong] Theorem 1559 1560 |- !M M' f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15. 1561 (M = M') /\ (!a0 a1. (M' = MLDR a0 a1) ==> (f a0 a1 = f' a0 a1)) /\ 1562 (!a0 a1. (M' = MSTR a0 a1) ==> (f1 a0 a1 = f1' a0 a1)) /\ 1563 (!a0 a1. (M' = MMOV a0 a1) ==> (f2 a0 a1 = f2' a0 a1)) /\ 1564 (!a0 a1 a2. (M' = MADD a0 a1 a2) ==> (f3 a0 a1 a2 = f3' a0 a1 a2)) /\ 1565 (!a0 a1 a2. (M' = MSUB a0 a1 a2) ==> (f4 a0 a1 a2 = f4' a0 a1 a2)) /\ 1566 (!a0 a1 a2. (M' = MRSB a0 a1 a2) ==> (f5 a0 a1 a2 = f5' a0 a1 a2)) /\ 1567 (!a0 a1 a2. (M' = MMUL a0 a1 a2) ==> (f6 a0 a1 a2 = f6' a0 a1 a2)) /\ 1568 (!a0 a1 a2. (M' = MAND a0 a1 a2) ==> (f7 a0 a1 a2 = f7' a0 a1 a2)) /\ 1569 (!a0 a1 a2. (M' = MORR a0 a1 a2) ==> (f8 a0 a1 a2 = f8' a0 a1 a2)) /\ 1570 (!a0 a1 a2. (M' = MEOR a0 a1 a2) ==> (f9 a0 a1 a2 = f9' a0 a1 a2)) /\ 1571 (!a0 a1 a2. (M' = MLSL a0 a1 a2) ==> (f10 a0 a1 a2 = f10' a0 a1 a2)) /\ 1572 (!a0 a1 a2. (M' = MLSR a0 a1 a2) ==> (f11 a0 a1 a2 = f11' a0 a1 a2)) /\ 1573 (!a0 a1 a2. (M' = MASR a0 a1 a2) ==> (f12 a0 a1 a2 = f12' a0 a1 a2)) /\ 1574 (!a0 a1 a2. (M' = MROR a0 a1 a2) ==> (f13 a0 a1 a2 = f13' a0 a1 a2)) /\ 1575 (!a0 a1. (M' = MPUSH a0 a1) ==> (f14 a0 a1 = f14' a0 a1)) /\ 1576 (!a0 a1. (M' = MPOP a0 a1) ==> (f15 a0 a1 = f15' a0 a1)) ==> 1577 (DOPER_case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 M = 1578 DOPER_case f' f1' f2' f3' f4' f5' f6' f7' f8' f9' f10' f11' f12' f13' 1579 f14' f15' M') 1580 1581 [DOPER_distinct] Theorem 1582 1583 |- (!a1' a1 a0' a0. ~(MLDR a0 a1 = MSTR a0' a1')) /\ 1584 (!a1' a1 a0' a0. ~(MLDR a0 a1 = MMOV a0' a1')) /\ 1585 (!a2 a1' a1 a0' a0. ~(MLDR a0 a1 = MADD a0' a1' a2)) /\ 1586 (!a2 a1' a1 a0' a0. ~(MLDR a0 a1 = MSUB a0' a1' a2)) /\ 1587 (!a2 a1' a1 a0' a0. ~(MLDR a0 a1 = MRSB a0' a1' a2)) /\ 1588 (!a2 a1' a1 a0' a0. ~(MLDR a0 a1 = MMUL a0' a1' a2)) /\ 1589 (!a2 a1' a1 a0' a0. ~(MLDR a0 a1 = MAND a0' a1' a2)) /\ 1590 (!a2 a1' a1 a0' a0. ~(MLDR a0 a1 = MORR a0' a1' a2)) /\ 1591 (!a2 a1' a1 a0' a0. ~(MLDR a0 a1 = MEOR a0' a1' a2)) /\ 1592 (!a2 a1' a1 a0' a0. ~(MLDR a0 a1 = MLSL a0' a1' a2)) /\ 1593 (!a2 a1' a1 a0' a0. ~(MLDR a0 a1 = MLSR a0' a1' a2)) /\ 1594 (!a2 a1' a1 a0' a0. ~(MLDR a0 a1 = MASR a0' a1' a2)) /\ 1595 (!a2 a1' a1 a0' a0. ~(MLDR a0 a1 = MROR a0' a1' a2)) /\ 1596 (!a1' a1 a0' a0. ~(MLDR a0 a1 = MPUSH a0' a1')) /\ 1597 (!a1' a1 a0' a0. ~(MLDR a0 a1 = MPOP a0' a1')) /\ 1598 (!a1' a1 a0' a0. ~(MSTR a0 a1 = MMOV a0' a1')) /\ 1599 (!a2 a1' a1 a0' a0. ~(MSTR a0 a1 = MADD a0' a1' a2)) /\ 1600 (!a2 a1' a1 a0' a0. ~(MSTR a0 a1 = MSUB a0' a1' a2)) /\ 1601 (!a2 a1' a1 a0' a0. ~(MSTR a0 a1 = MRSB a0' a1' a2)) /\ 1602 (!a2 a1' a1 a0' a0. ~(MSTR a0 a1 = MMUL a0' a1' a2)) /\ 1603 (!a2 a1' a1 a0' a0. ~(MSTR a0 a1 = MAND a0' a1' a2)) /\ 1604 (!a2 a1' a1 a0' a0. ~(MSTR a0 a1 = MORR a0' a1' a2)) /\ 1605 (!a2 a1' a1 a0' a0. ~(MSTR a0 a1 = MEOR a0' a1' a2)) /\ 1606 (!a2 a1' a1 a0' a0. ~(MSTR a0 a1 = MLSL a0' a1' a2)) /\ 1607 (!a2 a1' a1 a0' a0. ~(MSTR a0 a1 = MLSR a0' a1' a2)) /\ 1608 (!a2 a1' a1 a0' a0. ~(MSTR a0 a1 = MASR a0' a1' a2)) /\ 1609 (!a2 a1' a1 a0' a0. ~(MSTR a0 a1 = MROR a0' a1' a2)) /\ 1610 (!a1' a1 a0' a0. ~(MSTR a0 a1 = MPUSH a0' a1')) /\ 1611 (!a1' a1 a0' a0. ~(MSTR a0 a1 = MPOP a0' a1')) /\ 1612 (!a2 a1' a1 a0' a0. ~(MMOV a0 a1 = MADD a0' a1' a2)) /\ 1613 (!a2 a1' a1 a0' a0. ~(MMOV a0 a1 = MSUB a0' a1' a2)) /\ 1614 (!a2 a1' a1 a0' a0. ~(MMOV a0 a1 = MRSB a0' a1' a2)) /\ 1615 (!a2 a1' a1 a0' a0. ~(MMOV a0 a1 = MMUL a0' a1' a2)) /\ 1616 (!a2 a1' a1 a0' a0. ~(MMOV a0 a1 = MAND a0' a1' a2)) /\ 1617 (!a2 a1' a1 a0' a0. ~(MMOV a0 a1 = MORR a0' a1' a2)) /\ 1618 (!a2 a1' a1 a0' a0. ~(MMOV a0 a1 = MEOR a0' a1' a2)) /\ 1619 (!a2 a1' a1 a0' a0. ~(MMOV a0 a1 = MLSL a0' a1' a2)) /\ 1620 (!a2 a1' a1 a0' a0. ~(MMOV a0 a1 = MLSR a0' a1' a2)) /\ 1621 (!a2 a1' a1 a0' a0. ~(MMOV a0 a1 = MASR a0' a1' a2)) /\ 1622 (!a2 a1' a1 a0' a0. ~(MMOV a0 a1 = MROR a0' a1' a2)) /\ 1623 (!a1' a1 a0' a0. ~(MMOV a0 a1 = MPUSH a0' a1')) /\ 1624 (!a1' a1 a0' a0. ~(MMOV a0 a1 = MPOP a0' a1')) /\ 1625 (!a2' a2 a1' a1 a0' a0. ~(MADD a0 a1 a2 = MSUB a0' a1' a2')) /\ 1626 (!a2' a2 a1' a1 a0' a0. ~(MADD a0 a1 a2 = MRSB a0' a1' a2')) /\ 1627 (!a2' a2 a1' a1 a0' a0. ~(MADD a0 a1 a2 = MMUL a0' a1' a2')) /\ 1628 (!a2' a2 a1' a1 a0' a0. ~(MADD a0 a1 a2 = MAND a0' a1' a2')) /\ 1629 (!a2' a2 a1' a1 a0' a0. ~(MADD a0 a1 a2 = MORR a0' a1' a2')) /\ 1630 (!a2' a2 a1' a1 a0' a0. ~(MADD a0 a1 a2 = MEOR a0' a1' a2')) /\ 1631 (!a2' a2 a1' a1 a0' a0. ~(MADD a0 a1 a2 = MLSL a0' a1' a2')) /\ 1632 (!a2' a2 a1' a1 a0' a0. ~(MADD a0 a1 a2 = MLSR a0' a1' a2')) /\ 1633 (!a2' a2 a1' a1 a0' a0. ~(MADD a0 a1 a2 = MASR a0' a1' a2')) /\ 1634 (!a2' a2 a1' a1 a0' a0. ~(MADD a0 a1 a2 = MROR a0' a1' a2')) /\ 1635 (!a2 a1' a1 a0' a0. ~(MADD a0 a1 a2 = MPUSH a0' a1')) /\ 1636 (!a2 a1' a1 a0' a0. ~(MADD a0 a1 a2 = MPOP a0' a1')) /\ 1637 (!a2' a2 a1' a1 a0' a0. ~(MSUB a0 a1 a2 = MRSB a0' a1' a2')) /\ 1638 (!a2' a2 a1' a1 a0' a0. ~(MSUB a0 a1 a2 = MMUL a0' a1' a2')) /\ 1639 (!a2' a2 a1' a1 a0' a0. ~(MSUB a0 a1 a2 = MAND a0' a1' a2')) /\ 1640 (!a2' a2 a1' a1 a0' a0. ~(MSUB a0 a1 a2 = MORR a0' a1' a2')) /\ 1641 (!a2' a2 a1' a1 a0' a0. ~(MSUB a0 a1 a2 = MEOR a0' a1' a2')) /\ 1642 (!a2' a2 a1' a1 a0' a0. ~(MSUB a0 a1 a2 = MLSL a0' a1' a2')) /\ 1643 (!a2' a2 a1' a1 a0' a0. ~(MSUB a0 a1 a2 = MLSR a0' a1' a2')) /\ 1644 (!a2' a2 a1' a1 a0' a0. ~(MSUB a0 a1 a2 = MASR a0' a1' a2')) /\ 1645 (!a2' a2 a1' a1 a0' a0. ~(MSUB a0 a1 a2 = MROR a0' a1' a2')) /\ 1646 (!a2 a1' a1 a0' a0. ~(MSUB a0 a1 a2 = MPUSH a0' a1')) /\ 1647 (!a2 a1' a1 a0' a0. ~(MSUB a0 a1 a2 = MPOP a0' a1')) /\ 1648 (!a2' a2 a1' a1 a0' a0. ~(MRSB a0 a1 a2 = MMUL a0' a1' a2')) /\ 1649 (!a2' a2 a1' a1 a0' a0. ~(MRSB a0 a1 a2 = MAND a0' a1' a2')) /\ 1650 (!a2' a2 a1' a1 a0' a0. ~(MRSB a0 a1 a2 = MORR a0' a1' a2')) /\ 1651 (!a2' a2 a1' a1 a0' a0. ~(MRSB a0 a1 a2 = MEOR a0' a1' a2')) /\ 1652 (!a2' a2 a1' a1 a0' a0. ~(MRSB a0 a1 a2 = MLSL a0' a1' a2')) /\ 1653 (!a2' a2 a1' a1 a0' a0. ~(MRSB a0 a1 a2 = MLSR a0' a1' a2')) /\ 1654 (!a2' a2 a1' a1 a0' a0. ~(MRSB a0 a1 a2 = MASR a0' a1' a2')) /\ 1655 (!a2' a2 a1' a1 a0' a0. ~(MRSB a0 a1 a2 = MROR a0' a1' a2')) /\ 1656 (!a2 a1' a1 a0' a0. ~(MRSB a0 a1 a2 = MPUSH a0' a1')) /\ 1657 (!a2 a1' a1 a0' a0. ~(MRSB a0 a1 a2 = MPOP a0' a1')) /\ 1658 (!a2' a2 a1' a1 a0' a0. ~(MMUL a0 a1 a2 = MAND a0' a1' a2')) /\ 1659 (!a2' a2 a1' a1 a0' a0. ~(MMUL a0 a1 a2 = MORR a0' a1' a2')) /\ 1660 (!a2' a2 a1' a1 a0' a0. ~(MMUL a0 a1 a2 = MEOR a0' a1' a2')) /\ 1661 (!a2' a2 a1' a1 a0' a0. ~(MMUL a0 a1 a2 = MLSL a0' a1' a2')) /\ 1662 (!a2' a2 a1' a1 a0' a0. ~(MMUL a0 a1 a2 = MLSR a0' a1' a2')) /\ 1663 (!a2' a2 a1' a1 a0' a0. ~(MMUL a0 a1 a2 = MASR a0' a1' a2')) /\ 1664 (!a2' a2 a1' a1 a0' a0. ~(MMUL a0 a1 a2 = MROR a0' a1' a2')) /\ 1665 (!a2 a1' a1 a0' a0. ~(MMUL a0 a1 a2 = MPUSH a0' a1')) /\ 1666 (!a2 a1' a1 a0' a0. ~(MMUL a0 a1 a2 = MPOP a0' a1')) /\ 1667 (!a2' a2 a1' a1 a0' a0. ~(MAND a0 a1 a2 = MORR a0' a1' a2')) /\ 1668 (!a2' a2 a1' a1 a0' a0. ~(MAND a0 a1 a2 = MEOR a0' a1' a2')) /\ 1669 (!a2' a2 a1' a1 a0' a0. ~(MAND a0 a1 a2 = MLSL a0' a1' a2')) /\ 1670 (!a2' a2 a1' a1 a0' a0. ~(MAND a0 a1 a2 = MLSR a0' a1' a2')) /\ 1671 (!a2' a2 a1' a1 a0' a0. ~(MAND a0 a1 a2 = MASR a0' a1' a2')) /\ 1672 (!a2' a2 a1' a1 a0' a0. ~(MAND a0 a1 a2 = MROR a0' a1' a2')) /\ 1673 (!a2 a1' a1 a0' a0. ~(MAND a0 a1 a2 = MPUSH a0' a1')) /\ 1674 (!a2 a1' a1 a0' a0. ~(MAND a0 a1 a2 = MPOP a0' a1')) /\ 1675 (!a2' a2 a1' a1 a0' a0. ~(MORR a0 a1 a2 = MEOR a0' a1' a2')) /\ 1676 (!a2' a2 a1' a1 a0' a0. ~(MORR a0 a1 a2 = MLSL a0' a1' a2')) /\ 1677 (!a2' a2 a1' a1 a0' a0. ~(MORR a0 a1 a2 = MLSR a0' a1' a2')) /\ 1678 (!a2' a2 a1' a1 a0' a0. ~(MORR a0 a1 a2 = MASR a0' a1' a2')) /\ 1679 (!a2' a2 a1' a1 a0' a0. ~(MORR a0 a1 a2 = MROR a0' a1' a2')) /\ 1680 (!a2 a1' a1 a0' a0. ~(MORR a0 a1 a2 = MPUSH a0' a1')) /\ 1681 (!a2 a1' a1 a0' a0. ~(MORR a0 a1 a2 = MPOP a0' a1')) /\ 1682 (!a2' a2 a1' a1 a0' a0. ~(MEOR a0 a1 a2 = MLSL a0' a1' a2')) /\ 1683 (!a2' a2 a1' a1 a0' a0. ~(MEOR a0 a1 a2 = MLSR a0' a1' a2')) /\ 1684 (!a2' a2 a1' a1 a0' a0. ~(MEOR a0 a1 a2 = MASR a0' a1' a2')) /\ 1685 (!a2' a2 a1' a1 a0' a0. ~(MEOR a0 a1 a2 = MROR a0' a1' a2')) /\ 1686 (!a2 a1' a1 a0' a0. ~(MEOR a0 a1 a2 = MPUSH a0' a1')) /\ 1687 (!a2 a1' a1 a0' a0. ~(MEOR a0 a1 a2 = MPOP a0' a1')) /\ 1688 (!a2' a2 a1' a1 a0' a0. ~(MLSL a0 a1 a2 = MLSR a0' a1' a2')) /\ 1689 (!a2' a2 a1' a1 a0' a0. ~(MLSL a0 a1 a2 = MASR a0' a1' a2')) /\ 1690 (!a2' a2 a1' a1 a0' a0. ~(MLSL a0 a1 a2 = MROR a0' a1' a2')) /\ 1691 (!a2 a1' a1 a0' a0. ~(MLSL a0 a1 a2 = MPUSH a0' a1')) /\ 1692 (!a2 a1' a1 a0' a0. ~(MLSL a0 a1 a2 = MPOP a0' a1')) /\ 1693 (!a2' a2 a1' a1 a0' a0. ~(MLSR a0 a1 a2 = MASR a0' a1' a2')) /\ 1694 (!a2' a2 a1' a1 a0' a0. ~(MLSR a0 a1 a2 = MROR a0' a1' a2')) /\ 1695 (!a2 a1' a1 a0' a0. ~(MLSR a0 a1 a2 = MPUSH a0' a1')) /\ 1696 (!a2 a1' a1 a0' a0. ~(MLSR a0 a1 a2 = MPOP a0' a1')) /\ 1697 (!a2' a2 a1' a1 a0' a0. ~(MASR a0 a1 a2 = MROR a0' a1' a2')) /\ 1698 (!a2 a1' a1 a0' a0. ~(MASR a0 a1 a2 = MPUSH a0' a1')) /\ 1699 (!a2 a1' a1 a0' a0. ~(MASR a0 a1 a2 = MPOP a0' a1')) /\ 1700 (!a2 a1' a1 a0' a0. ~(MROR a0 a1 a2 = MPUSH a0' a1')) /\ 1701 (!a2 a1' a1 a0' a0. ~(MROR a0 a1 a2 = MPOP a0' a1')) /\ 1702 !a1' a1 a0' a0. ~(MPUSH a0 a1 = MPOP a0' a1') 1703 1704 [DOPER_induction] Theorem 1705 1706 |- !P. 1707 (!M p. P (MLDR M p)) /\ (!p M. P (MSTR p M)) /\ (!M M0. P (MMOV M M0)) /\ 1708 (!M M0 M1. P (MADD M M0 M1)) /\ (!M M0 M1. P (MSUB M M0 M1)) /\ 1709 (!M M0 M1. P (MRSB M M0 M1)) /\ (!M M0 M1. P (MMUL M M0 M1)) /\ 1710 (!M M0 M1. P (MAND M M0 M1)) /\ (!M M0 M1. P (MORR M M0 M1)) /\ 1711 (!M M0 M1. P (MEOR M M0 M1)) /\ (!M M0 c. P (MLSL M M0 c)) /\ 1712 (!M M0 c. P (MLSR M M0 c)) /\ (!M M0 c. P (MASR M M0 c)) /\ 1713 (!M M0 c. P (MROR M M0 c)) /\ (!n l. P (MPUSH n l)) /\ 1714 (!n l. P (MPOP n l)) ==> 1715 !D. P D 1716 1717 [DOPER_nchotomy] Theorem 1718 1719 |- !D. 1720 (?M p. D = MLDR M p) \/ (?p M. D = MSTR p M) \/ (?M M0. D = MMOV M M0) \/ 1721 (?M M0 M1. D = MADD M M0 M1) \/ (?M M0 M1. D = MSUB M M0 M1) \/ 1722 (?M M0 M1. D = MRSB M M0 M1) \/ (?M M0 M1. D = MMUL M M0 M1) \/ 1723 (?M M0 M1. D = MAND M M0 M1) \/ (?M M0 M1. D = MORR M M0 M1) \/ 1724 (?M M0 M1. D = MEOR M M0 M1) \/ (?M M0 c. D = MLSL M M0 c) \/ 1725 (?M M0 c. D = MLSR M M0 c) \/ (?M M0 c. D = MASR M M0 c) \/ 1726 (?M M0 c. D = MROR M M0 c) \/ (?n l. D = MPUSH n l) \/ ?n l. D = MPOP n l 1727 1728 [HOARE_CJ_IR] Theorem 1729 1730 |- !cond ir_t ir_f P Q R. 1731 WELL_FORMED ir_t /\ WELL_FORMED ir_f /\ 1732 (!st. P st ==> Q (run_ir ir_t st)) /\ 1733 (!st. P st ==> R (run_ir ir_f st)) ==> 1734 !st. 1735 P st ==> 1736 (if eval_il_cond cond st then 1737 Q (run_ir (CJ cond ir_t ir_f) st) 1738 else 1739 R (run_ir (CJ cond ir_t ir_f) st)) 1740 1741 [HOARE_SC_IR] Theorem 1742 1743 |- !ir1 ir2 P Q R T. 1744 WELL_FORMED ir1 /\ WELL_FORMED ir2 /\ (!st. P st ==> Q (run_ir ir1 st)) /\ 1745 (!st. R st ==> T (run_ir ir2 st)) /\ (!st. Q st ==> R st) ==> 1746 !st. P st ==> T (run_ir (SC ir1 ir2) st) 1747 1748 [HOARE_TR_IR] Theorem 1749 1750 |- !cond ir P. 1751 WELL_FORMED ir /\ WF_TR (translate_condition cond,translate ir) /\ 1752 (!st. P st ==> P (run_ir ir st)) ==> 1753 !st. 1754 P st ==> 1755 P (run_ir (TR cond ir) st) /\ eval_il_cond cond (run_ir (TR cond ir) st) 1756 1757 [IR_CJ_IS_WELL_FORMED] Theorem 1758 1759 |- !cond ir_t ir_f. 1760 WELL_FORMED ir_t /\ WELL_FORMED ir_f = WELL_FORMED (CJ cond ir_t ir_f) 1761 1762 [IR_SC_IS_WELL_FORMED] Theorem 1763 1764 |- !ir1 ir2. WELL_FORMED ir1 /\ WELL_FORMED ir2 = WELL_FORMED (SC ir1 ir2) 1765 1766 [IR_SEMANTICS_BLK] Theorem 1767 1768 |- (run_ir (BLK (stm::stmL)) st = run_ir (BLK stmL) (mdecode st stm)) /\ 1769 (run_ir (BLK []) st = st) 1770 1771 [IR_SEMANTICS_CJ] Theorem 1772 1773 |- WELL_FORMED ir_t /\ WELL_FORMED ir_f ==> 1774 (run_ir (CJ cond ir_t ir_f) st = 1775 (if eval_il_cond cond st then run_ir ir_t st else run_ir ir_f st)) 1776 1777 [IR_SEMANTICS_SC] Theorem 1778 1779 |- WELL_FORMED ir1 /\ WELL_FORMED ir2 ==> 1780 (run_ir (SC ir1 ir2) st = run_ir ir2 (run_ir ir1 st)) 1781 1782 [IR_SEMANTICS_TR] Theorem 1783 1784 |- WELL_FORMED ir /\ WF_TR (translate_condition cond,translate ir) ==> 1785 (run_ir (TR cond ir) st = 1786 WHILE (\st'. ~eval_il_cond cond st') (run_ir ir) st) 1787 1788 [IR_TR_IS_WELL_FORMED] Theorem 1789 1790 |- !ir cond. 1791 WELL_FORMED ir /\ WF_TR (translate_condition cond,translate ir) = 1792 WELL_FORMED (TR cond ir) 1793 1794 [MEXP_11] Theorem 1795 1796 |- (!a a'. (MR a = MR a') = (a = a')) /\ 1797 !a0 a1 a0' a1'. (MC a0 a1 = MC a0' a1') = (a0 = a0') /\ (a1 = a1') 1798 1799 [MEXP_Axiom] Theorem 1800 1801 |- !f0 f1. ?fn. (!a. fn (MR a) = f0 a) /\ !a0 a1. fn (MC a0 a1) = f1 a0 a1 1802 1803 [MEXP_case_cong] Theorem 1804 1805 |- !M M' f f1. 1806 (M = M') /\ (!a. (M' = MR a) ==> (f a = f' a)) /\ 1807 (!a0 a1. (M' = MC a0 a1) ==> (f1 a0 a1 = f1' a0 a1)) ==> 1808 (MEXP_case f f1 M = MEXP_case f' f1' M') 1809 1810 [MEXP_distinct] Theorem 1811 1812 |- !a1 a0 a. ~(MR a = MC a0 a1) 1813 1814 [MEXP_induction] Theorem 1815 1816 |- !P. (!M. P (MR M)) /\ (!c c0. P (MC c c0)) ==> !M. P M 1817 1818 [MEXP_nchotomy] Theorem 1819 1820 |- !M. (?M'. M = MR M') \/ ?c c0. M = MC c c0 1821 1822 [MREG2num_11] Theorem 1823 1824 |- !a a'. (MREG2num a = MREG2num a') = (a = a') 1825 1826 [MREG2num_ONTO] Theorem 1827 1828 |- !r. r < 15 = ?a. r = MREG2num a 1829 1830 [MREG2num_num2MREG] Theorem 1831 1832 |- !r. r < 15 = (MREG2num (num2MREG r) = r) 1833 1834 [MREG2num_thm] Theorem 1835 1836 |- (MREG2num R0 = 0) /\ (MREG2num R1 = 1) /\ (MREG2num R2 = 2) /\ 1837 (MREG2num R3 = 3) /\ (MREG2num R4 = 4) /\ (MREG2num R5 = 5) /\ 1838 (MREG2num R6 = 6) /\ (MREG2num R7 = 7) /\ (MREG2num R8 = 8) /\ 1839 (MREG2num R9 = 9) /\ (MREG2num R10 = 10) /\ (MREG2num R11 = 11) /\ 1840 (MREG2num R12 = 12) /\ (MREG2num R13 = 13) /\ (MREG2num R14 = 14) 1841 1842 [MREG_Axiom] Theorem 1843 1844 |- !x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14. 1845 ?f. 1846 (f R0 = x0) /\ (f R1 = x1) /\ (f R2 = x2) /\ (f R3 = x3) /\ 1847 (f R4 = x4) /\ (f R5 = x5) /\ (f R6 = x6) /\ (f R7 = x7) /\ 1848 (f R8 = x8) /\ (f R9 = x9) /\ (f R10 = x10) /\ (f R11 = x11) /\ 1849 (f R12 = x12) /\ (f R13 = x13) /\ (f R14 = x14) 1850 1851 [MREG_EQ_MREG] Theorem 1852 1853 |- !a a'. (a = a') = (MREG2num a = MREG2num a') 1854 1855 [MREG_case_cong] Theorem 1856 1857 |- !M M' v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14. 1858 (M = M') /\ ((M' = R0) ==> (v0 = v0')) /\ ((M' = R1) ==> (v1 = v1')) /\ 1859 ((M' = R2) ==> (v2 = v2')) /\ ((M' = R3) ==> (v3 = v3')) /\ 1860 ((M' = R4) ==> (v4 = v4')) /\ ((M' = R5) ==> (v5 = v5')) /\ 1861 ((M' = R6) ==> (v6 = v6')) /\ ((M' = R7) ==> (v7 = v7')) /\ 1862 ((M' = R8) ==> (v8 = v8')) /\ ((M' = R9) ==> (v9 = v9')) /\ 1863 ((M' = R10) ==> (v10 = v10')) /\ ((M' = R11) ==> (v11 = v11')) /\ 1864 ((M' = R12) ==> (v12 = v12')) /\ ((M' = R13) ==> (v13 = v13')) /\ 1865 ((M' = R14) ==> (v14 = v14')) ==> 1866 ((case M of 1867 R0 -> v0 1868 || R1 -> v1 1869 || R2 -> v2 1870 || R3 -> v3 1871 || R4 -> v4 1872 || R5 -> v5 1873 || R6 -> v6 1874 || R7 -> v7 1875 || R8 -> v8 1876 || R9 -> v9 1877 || R10 -> v10 1878 || R11 -> v11 1879 || R12 -> v12 1880 || R13 -> v13 1881 || R14 -> v14) = 1882 case M' of 1883 R0 -> v0' 1884 || R1 -> v1' 1885 || R2 -> v2' 1886 || R3 -> v3' 1887 || R4 -> v4' 1888 || R5 -> v5' 1889 || R6 -> v6' 1890 || R7 -> v7' 1891 || R8 -> v8' 1892 || R9 -> v9' 1893 || R10 -> v10' 1894 || R11 -> v11' 1895 || R12 -> v12' 1896 || R13 -> v13' 1897 || R14 -> v14') 1898 1899 [MREG_case_def] Theorem 1900 1901 |- (!v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14. 1902 (case R0 of 1903 R0 -> v0 1904 || R1 -> v1 1905 || R2 -> v2 1906 || R3 -> v3 1907 || R4 -> v4 1908 || R5 -> v5 1909 || R6 -> v6 1910 || R7 -> v7 1911 || R8 -> v8 1912 || R9 -> v9 1913 || R10 -> v10 1914 || R11 -> v11 1915 || R12 -> v12 1916 || R13 -> v13 1917 || R14 -> v14) = 1918 v0) /\ 1919 (!v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14. 1920 (case R1 of 1921 R0 -> v0 1922 || R1 -> v1 1923 || R2 -> v2 1924 || R3 -> v3 1925 || R4 -> v4 1926 || R5 -> v5 1927 || R6 -> v6 1928 || R7 -> v7 1929 || R8 -> v8 1930 || R9 -> v9 1931 || R10 -> v10 1932 || R11 -> v11 1933 || R12 -> v12 1934 || R13 -> v13 1935 || R14 -> v14) = 1936 v1) /\ 1937 (!v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14. 1938 (case R2 of 1939 R0 -> v0 1940 || R1 -> v1 1941 || R2 -> v2 1942 || R3 -> v3 1943 || R4 -> v4 1944 || R5 -> v5 1945 || R6 -> v6 1946 || R7 -> v7 1947 || R8 -> v8 1948 || R9 -> v9 1949 || R10 -> v10 1950 || R11 -> v11 1951 || R12 -> v12 1952 || R13 -> v13 1953 || R14 -> v14) = 1954 v2) /\ 1955 (!v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14. 1956 (case R3 of 1957 R0 -> v0 1958 || R1 -> v1 1959 || R2 -> v2 1960 || R3 -> v3 1961 || R4 -> v4 1962 || R5 -> v5 1963 || R6 -> v6 1964 || R7 -> v7 1965 || R8 -> v8 1966 || R9 -> v9 1967 || R10 -> v10 1968 || R11 -> v11 1969 || R12 -> v12 1970 || R13 -> v13 1971 || R14 -> v14) = 1972 v3) /\ 1973 (!v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14. 1974 (case R4 of 1975 R0 -> v0 1976 || R1 -> v1 1977 || R2 -> v2 1978 || R3 -> v3 1979 || R4 -> v4 1980 || R5 -> v5 1981 || R6 -> v6 1982 || R7 -> v7 1983 || R8 -> v8 1984 || R9 -> v9 1985 || R10 -> v10 1986 || R11 -> v11 1987 || R12 -> v12 1988 || R13 -> v13 1989 || R14 -> v14) = 1990 v4) /\ 1991 (!v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14. 1992 (case R5 of 1993 R0 -> v0 1994 || R1 -> v1 1995 || R2 -> v2 1996 || R3 -> v3 1997 || R4 -> v4 1998 || R5 -> v5 1999 || R6 -> v6 2000 || R7 -> v7 2001 || R8 -> v8 2002 || R9 -> v9 2003 || R10 -> v10 2004 || R11 -> v11 2005 || R12 -> v12 2006 || R13 -> v13 2007 || R14 -> v14) = 2008 v5) /\ 2009 (!v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14. 2010 (case R6 of 2011 R0 -> v0 2012 || R1 -> v1 2013 || R2 -> v2 2014 || R3 -> v3 2015 || R4 -> v4 2016 || R5 -> v5 2017 || R6 -> v6 2018 || R7 -> v7 2019 || R8 -> v8 2020 || R9 -> v9 2021 || R10 -> v10 2022 || R11 -> v11 2023 || R12 -> v12 2024 || R13 -> v13 2025 || R14 -> v14) = 2026 v6) /\ 2027 (!v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14. 2028 (case R7 of 2029 R0 -> v0 2030 || R1 -> v1 2031 || R2 -> v2 2032 || R3 -> v3 2033 || R4 -> v4 2034 || R5 -> v5 2035 || R6 -> v6 2036 || R7 -> v7 2037 || R8 -> v8 2038 || R9 -> v9 2039 || R10 -> v10 2040 || R11 -> v11 2041 || R12 -> v12 2042 || R13 -> v13 2043 || R14 -> v14) = 2044 v7) /\ 2045 (!v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14. 2046 (case R8 of 2047 R0 -> v0 2048 || R1 -> v1 2049 || R2 -> v2 2050 || R3 -> v3 2051 || R4 -> v4 2052 || R5 -> v5 2053 || R6 -> v6 2054 || R7 -> v7 2055 || R8 -> v8 2056 || R9 -> v9 2057 || R10 -> v10 2058 || R11 -> v11 2059 || R12 -> v12 2060 || R13 -> v13 2061 || R14 -> v14) = 2062 v8) /\ 2063 (!v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14. 2064 (case R9 of 2065 R0 -> v0 2066 || R1 -> v1 2067 || R2 -> v2 2068 || R3 -> v3 2069 || R4 -> v4 2070 || R5 -> v5 2071 || R6 -> v6 2072 || R7 -> v7 2073 || R8 -> v8 2074 || R9 -> v9 2075 || R10 -> v10 2076 || R11 -> v11 2077 || R12 -> v12 2078 || R13 -> v13 2079 || R14 -> v14) = 2080 v9) /\ 2081 (!v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14. 2082 (case R10 of 2083 R0 -> v0 2084 || R1 -> v1 2085 || R2 -> v2 2086 || R3 -> v3 2087 || R4 -> v4 2088 || R5 -> v5 2089 || R6 -> v6 2090 || R7 -> v7 2091 || R8 -> v8 2092 || R9 -> v9 2093 || R10 -> v10 2094 || R11 -> v11 2095 || R12 -> v12 2096 || R13 -> v13 2097 || R14 -> v14) = 2098 v10) /\ 2099 (!v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14. 2100 (case R11 of 2101 R0 -> v0 2102 || R1 -> v1 2103 || R2 -> v2 2104 || R3 -> v3 2105 || R4 -> v4 2106 || R5 -> v5 2107 || R6 -> v6 2108 || R7 -> v7 2109 || R8 -> v8 2110 || R9 -> v9 2111 || R10 -> v10 2112 || R11 -> v11 2113 || R12 -> v12 2114 || R13 -> v13 2115 || R14 -> v14) = 2116 v11) /\ 2117 (!v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14. 2118 (case R12 of 2119 R0 -> v0 2120 || R1 -> v1 2121 || R2 -> v2 2122 || R3 -> v3 2123 || R4 -> v4 2124 || R5 -> v5 2125 || R6 -> v6 2126 || R7 -> v7 2127 || R8 -> v8 2128 || R9 -> v9 2129 || R10 -> v10 2130 || R11 -> v11 2131 || R12 -> v12 2132 || R13 -> v13 2133 || R14 -> v14) = 2134 v12) /\ 2135 (!v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14. 2136 (case R13 of 2137 R0 -> v0 2138 || R1 -> v1 2139 || R2 -> v2 2140 || R3 -> v3 2141 || R4 -> v4 2142 || R5 -> v5 2143 || R6 -> v6 2144 || R7 -> v7 2145 || R8 -> v8 2146 || R9 -> v9 2147 || R10 -> v10 2148 || R11 -> v11 2149 || R12 -> v12 2150 || R13 -> v13 2151 || R14 -> v14) = 2152 v13) /\ 2153 !v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14. 2154 (case R14 of 2155 R0 -> v0 2156 || R1 -> v1 2157 || R2 -> v2 2158 || R3 -> v3 2159 || R4 -> v4 2160 || R5 -> v5 2161 || R6 -> v6 2162 || R7 -> v7 2163 || R8 -> v8 2164 || R9 -> v9 2165 || R10 -> v10 2166 || R11 -> v11 2167 || R12 -> v12 2168 || R13 -> v13 2169 || R14 -> v14) = 2170 v14 2171 2172 [MREG_distinct] Theorem 2173 2174 |- ~(R0 = R1) /\ ~(R0 = R2) /\ ~(R0 = R3) /\ ~(R0 = R4) /\ ~(R0 = R5) /\ 2175 ~(R0 = R6) /\ ~(R0 = R7) /\ ~(R0 = R8) /\ ~(R0 = R9) /\ ~(R0 = R10) /\ 2176 ~(R0 = R11) /\ ~(R0 = R12) /\ ~(R0 = R13) /\ ~(R0 = R14) /\ ~(R1 = R2) /\ 2177 ~(R1 = R3) /\ ~(R1 = R4) /\ ~(R1 = R5) /\ ~(R1 = R6) /\ ~(R1 = R7) /\ 2178 ~(R1 = R8) /\ ~(R1 = R9) /\ ~(R1 = R10) /\ ~(R1 = R11) /\ ~(R1 = R12) /\ 2179 ~(R1 = R13) /\ ~(R1 = R14) /\ ~(R2 = R3) /\ ~(R2 = R4) /\ ~(R2 = R5) /\ 2180 ~(R2 = R6) /\ ~(R2 = R7) /\ ~(R2 = R8) /\ ~(R2 = R9) /\ ~(R2 = R10) /\ 2181 ~(R2 = R11) /\ ~(R2 = R12) /\ ~(R2 = R13) /\ ~(R2 = R14) /\ ~(R3 = R4) /\ 2182 ~(R3 = R5) /\ ~(R3 = R6) /\ ~(R3 = R7) /\ ~(R3 = R8) /\ ~(R3 = R9) /\ 2183 ~(R3 = R10) /\ ~(R3 = R11) /\ ~(R3 = R12) /\ ~(R3 = R13) /\ ~(R3 = R14) /\ 2184 ~(R4 = R5) /\ ~(R4 = R6) /\ ~(R4 = R7) /\ ~(R4 = R8) /\ ~(R4 = R9) /\ 2185 ~(R4 = R10) /\ ~(R4 = R11) /\ ~(R4 = R12) /\ ~(R4 = R13) /\ ~(R4 = R14) /\ 2186 ~(R5 = R6) /\ ~(R5 = R7) /\ ~(R5 = R8) /\ ~(R5 = R9) /\ ~(R5 = R10) /\ 2187 ~(R5 = R11) /\ ~(R5 = R12) /\ ~(R5 = R13) /\ ~(R5 = R14) /\ ~(R6 = R7) /\ 2188 ~(R6 = R8) /\ ~(R6 = R9) /\ ~(R6 = R10) /\ ~(R6 = R11) /\ ~(R6 = R12) /\ 2189 ~(R6 = R13) /\ ~(R6 = R14) /\ ~(R7 = R8) /\ ~(R7 = R9) /\ ~(R7 = R10) /\ 2190 ~(R7 = R11) /\ ~(R7 = R12) /\ ~(R7 = R13) /\ ~(R7 = R14) /\ ~(R8 = R9) /\ 2191 ~(R8 = R10) /\ ~(R8 = R11) /\ ~(R8 = R12) /\ ~(R8 = R13) /\ ~(R8 = R14) /\ 2192 ~(R9 = R10) /\ ~(R9 = R11) /\ ~(R9 = R12) /\ ~(R9 = R13) /\ ~(R9 = R14) /\ 2193 ~(R10 = R11) /\ ~(R10 = R12) /\ ~(R10 = R13) /\ ~(R10 = R14) /\ 2194 ~(R11 = R12) /\ ~(R11 = R13) /\ ~(R11 = R14) /\ ~(R12 = R13) /\ 2195 ~(R12 = R14) /\ ~(R13 = R14) 2196 2197 [MREG_induction] Theorem 2198 2199 |- !P. 2200 P R0 /\ P R1 /\ P R10 /\ P R11 /\ P R12 /\ P R13 /\ P R14 /\ P R2 /\ 2201 P R3 /\ P R4 /\ P R5 /\ P R6 /\ P R7 /\ P R8 /\ P R9 ==> 2202 !a. P a 2203 2204 [MREG_nchotomy] Theorem 2205 2206 |- !a. 2207 (a = R0) \/ (a = R1) \/ (a = R2) \/ (a = R3) \/ (a = R4) \/ (a = R5) \/ 2208 (a = R6) \/ (a = R7) \/ (a = R8) \/ (a = R9) \/ (a = R10) \/ (a = R11) \/ 2209 (a = R12) \/ (a = R13) \/ (a = R14) 2210 2211 [SEMANTICS_OF_IR] Theorem 2212 2213 |- WELL_FORMED ir1 /\ WELL_FORMED ir2 ==> 2214 (run_ir (BLK (stm::stmL)) st = run_ir (BLK stmL) (mdecode st stm)) /\ 2215 (run_ir (BLK []) st = st) /\ 2216 (run_ir (SC ir1 ir2) st = run_ir ir2 (run_ir ir1 st)) /\ 2217 (run_ir (CJ cond ir1 ir2) st = 2218 (if eval_il_cond cond st then run_ir ir1 st else run_ir ir2 st)) /\ 2219 (WF_TR (translate_condition cond,translate ir1) ==> 2220 (run_ir (TR cond ir1) st = 2221 WHILE (\st'. ~eval_il_cond cond st') (run_ir ir1) st)) 2222 2223 [STATEMENT_IS_WELL_FORMED] Theorem 2224 2225 |- !stm. well_formed [translate_assignment stm] 2226 2227 [TRANSLATE_ASSIGMENT_CORRECT] Theorem 2228 2229 |- !stm pc cpsr st. 2230 (SUC pc,cpsr,mdecode st stm) = 2231 decode_cond (pc,cpsr,st) (translate_assignment stm) 2232 2233 [TRANSLATE_ASSIGMENT_CORRECT_2] Theorem 2234 2235 |- !stm s. 2236 decode_cond s (translate_assignment stm) = 2237 (SUC (FST s),FST (SND s),mdecode (SND (SND s)) stm) 2238 2239 [UPLOAD_LEM_2] Theorem 2240 2241 |- !s stm iB. upload [stm] iB (FST s) (FST s) = stm 2242 2243 [WELL_FORMED_SUB_thm] Theorem 2244 2245 |- !ir. WELL_FORMED ir = WELL_FORMED_SUB ir /\ well_formed (translate ir) 2246 2247 [WELL_FORMED_thm] Theorem 2248 2249 |- (WELL_FORMED (BLK stmL) = T) /\ 2250 (WELL_FORMED (SC S1 S2) = WELL_FORMED S1 /\ WELL_FORMED S2) /\ 2251 (WELL_FORMED (CJ cond S1 S2) = WELL_FORMED S1 /\ WELL_FORMED S2) /\ 2252 (WELL_FORMED (TR cond S1) = 2253 WELL_FORMED S1 /\ WF_TR (translate_condition cond,translate S1)) 2254 2255 [datatype_CTL_STRUCTURE] Theorem 2256 2257 |- DATATYPE (CTL_STRUCTURE BLK SC CJ TR) 2258 2259 [datatype_DOPER] Theorem 2260 2261 |- DATATYPE 2262 (DOPER MLDR MSTR MMOV MADD MSUB MRSB MMUL MAND MORR MEOR MLSL MLSR MASR 2263 MROR MPUSH MPOP) 2264 2265 [datatype_MEXP] Theorem 2266 2267 |- DATATYPE (MEXP MR MC) 2268 2269 [datatype_MREG] Theorem 2270 2271 |- DATATYPE (MREG R0 R1 R2 R3 R4 R5 R6 R7 R8 R9 R10 R11 R12 R13 R14) 2272 2273 [from_reg_index_thm] Theorem 2274 2275 |- (from_reg_index 0 = R0) /\ (from_reg_index 1 = R1) /\ 2276 (from_reg_index 2 = R2) /\ (from_reg_index 3 = R3) /\ 2277 (from_reg_index 4 = R4) /\ (from_reg_index 5 = R5) /\ 2278 (from_reg_index 6 = R6) /\ (from_reg_index 7 = R7) /\ 2279 (from_reg_index 8 = R8) /\ (from_reg_index 9 = R9) /\ 2280 (from_reg_index 10 = R10) /\ (from_reg_index 11 = R11) /\ 2281 (from_reg_index 12 = R12) /\ (from_reg_index 13 = R13) /\ 2282 (from_reg_index 14 = R14) 2283 2284 [num2MREG_11] Theorem 2285 2286 |- !r r'. r < 15 ==> r' < 15 ==> ((num2MREG r = num2MREG r') = (r = r')) 2287 2288 [num2MREG_MREG2num] Theorem 2289 2290 |- !a. num2MREG (MREG2num a) = a 2291 2292 [num2MREG_ONTO] Theorem 2293 2294 |- !a. ?r. (a = num2MREG r) /\ r < 15 2295 2296 [num2MREG_thm] Theorem 2297 2298 |- (num2MREG 0 = R0) /\ (num2MREG 1 = R1) /\ (num2MREG 2 = R2) /\ 2299 (num2MREG 3 = R3) /\ (num2MREG 4 = R4) /\ (num2MREG 5 = R5) /\ 2300 (num2MREG 6 = R6) /\ (num2MREG 7 = R7) /\ (num2MREG 8 = R8) /\ 2301 (num2MREG 9 = R9) /\ (num2MREG 10 = R10) /\ (num2MREG 11 = R11) /\ 2302 (num2MREG 12 = R12) /\ (num2MREG 13 = R13) /\ (num2MREG 14 = R14) 2303 2304 [translate_def] Theorem 2305 2306 |- (translate (BLK (stm::stmL)) = 2307 translate_assignment stm::translate (BLK stmL)) /\ 2308 (translate (BLK []) = []) /\ 2309 (translate (SC S1 S2) = mk_SC (translate S1) (translate S2)) /\ 2310 (translate (CJ cond Strue Sfalse) = 2311 mk_CJ (translate_condition cond) (translate Strue) (translate Sfalse)) /\ 2312 (translate (TR cond Sbody) = 2313 mk_TR (translate_condition cond) (translate Sbody)) 2314 2315 [translate_ind] Theorem 2316 2317 |- !P. 2318 (!stm stmL. P (BLK stmL) ==> P (BLK (stm::stmL))) /\ P (BLK []) /\ 2319 (!S1 S2. P S1 /\ P S2 ==> P (SC S1 S2)) /\ 2320 (!cond Strue Sfalse. P Sfalse /\ P Strue ==> P (CJ cond Strue Sfalse)) /\ 2321 (!cond Sbody. P Sbody ==> P (TR cond Sbody)) ==> 2322 !v. P v 2323 2324 2325*) 2326end 2327