1 2open HolKernel Parse boolLib bossLib; 3 4val _ = new_theory "straightline"; 5 6open wordsTheory wordsLib pairTheory listTheory relationTheory; 7open pred_setTheory arithmeticTheory combinTheory; 8open arm_decompTheory set_sepTheory progTheory addressTheory; 9open tripleTheory lcsymtacs GraphLangTheory; 10 11val arm_assert_def = Define ` 12 arm_assert (p,r0,r1,r2,r3,r4,r5,r6,r7,r8,r9,r10,r11,r12,r13,r14,n,z,c,v, 13 mode,dmem,memory,dom_stack,stack) = 14 arm_PC p * 15 arm_REG (R_mode mode 0w) r0 * 16 arm_REG (R_mode mode 1w) r1 * 17 arm_REG (R_mode mode 2w) r2 * 18 arm_REG (R_mode mode 3w) r3 * 19 arm_REG (R_mode mode 4w) r4 * 20 arm_REG (R_mode mode 5w) r5 * 21 arm_REG (R_mode mode 6w) r6 * 22 arm_REG (R_mode mode 7w) r7 * 23 arm_REG (R_mode mode 8w) r8 * 24 arm_REG (R_mode mode 9w) r9 * 25 arm_REG (R_mode mode 10w) r10 * 26 arm_REG (R_mode mode 11w) r11 * 27 arm_REG (R_mode mode 12w) r12 * 28 arm_REG (R_mode mode 13w) r13 * 29 arm_REG (R_mode mode 14w) r14 * 30 arm_CPSR_N n * 31 arm_CPSR_Z z * 32 arm_CPSR_C c * 33 arm_CPSR_V v * 34 arm_OK mode * 35 arm_MEMORY dmem memory * 36 arm_STACK_MEMORY dom_stack stack` 37 38val TRIPLE_INTRO = store_thm("TRIPLE_INTRO", 39 ``(c_post ==> SPEC model (assert p) code (assert post)) ==> 40 TRIPLE (assert,model) (pre,p) code (pre /\ c_post,post)``, 41 full_simp_tac std_ss [tripleTheory.TRIPLE_def]); 42 43val SPEC_VAR_PC = store_thm("SPEC_VAR_PC", 44 ``SPEC m (pre * res w) code q ==> 45 !p. (p = w) ==> SPEC m (pre * res p) code q``, 46 fs []); 47 48val TRIPLE_NOP = store_thm("TRIPLE_NOP", 49 ``TRIPLE (arm_assert,ARM_MODEL) 50 (pre,p,r0,r1,r2,r3,r4,r5,r6,r7,r8,r9,r10,r11,r12,r13,r14,n,z,c,v, 51 mode,dmem,memory,dom_stack,stack) code 52 (pre,p,r0,r1,r2,r3,r4,r5,r6,r7,r8,r9,r10,r11,r12,r13,r14,n,z,c,v, 53 mode,dmem,memory,dom_stack,stack)``, 54 fs [TRIPLE_def,SPEC_REFL]); 55 56val COMBINE1 = store_thm("COMBINE1", 57 ``((x1 = x2) ==> (t1 = t2)) /\ ((y1 = y2) ==> (u1 = u2)) ==> 58 (((x1,y1) = (x2,y2)) ==> ((t1,u1) = (t2,u2)))``,fs []) 59 60val COMBINE2 = store_thm("COMBINE2", 61 ``((x1 = x2) ==> (t1 = t2)) /\ ((u1 = u2)) ==> 62 (((x1) = (x2)) ==> ((t1,u1) = (t2,u2)))``,fs []) 63 64val COMBINE3 = store_thm("COMBINE3", 65 ``((t1 = t2)) /\ ((y1 = y2) ==> (u1 = u2)) ==> 66 (((y1) = (y2)) ==> ((t1,u1) = (t2,u2)))``,fs []) 67 68val COMBINE4 = store_thm("COMBINE4", 69 ``(t1 = t2) /\ (u1 = u2) ==> ((t1,u1) = (t2,u2))``,fs []) 70 71val DO_NOTHING_def = Define `DO_NOTHING x = x`; 72 73val _ = export_theory(); 74