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