1open HolKernel boolLib bossLib
2open set_sepTheory progTheory temporalTheory stateTheory
3
4val _ = new_theory "temporal_state"
5
6infix \\
7val op \\ = op THEN;
8
9(* ------------------------------------------------------------------------ *)
10
11val TEMPORAL_NEXT_def = Define`
12   TEMPORAL_NEXT
13      ((to_set,next,instr,less,avoid): ('a, 'b, 'c) processor) p c q =
14   TEMPORAL (to_set,next,instr,$=,K F) c (T_IMPLIES (NOW p) (NEXT (NOW q)))`
15
16(* ------------------------------------------------------------------------ *)
17
18val INIT =
19   strip_tac
20   \\ `?to_set next instr less avoid. x = (to_set,next,instr,less,avoid)`
21   by metis_tac [pairTheory.PAIR]
22
23val TEMPORAL_NEXT_MOVE_COND = Q.store_thm("TEMPORAL_NEXT_MOVE_COND",
24   `!x p c q g.
25       TEMPORAL_NEXT x (p * cond g) c q <=> g ==> TEMPORAL_NEXT x p c q`,
26   INIT
27   \\ Cases_on `g`
28   \\ simp [SEP_F_def, TEMPORAL_NEXT_def, TEMPORAL_def, SEP_CLAUSES,
29            SEP_REFINE_def, T_IMPLIES_def, NOW_def]
30   )
31
32val TEMPORAL_NEXT_FRAME = Q.store_thm("TEMPORAL_NEXT_FRAME",
33   `!x p c q. TEMPORAL_NEXT x p c q ==> !r. TEMPORAL_NEXT x (p * r) c (q * r)`,
34   INIT
35   \\ simp [GSYM STAR_ASSOC, TEMPORAL_NEXT_def, TEMPORAL_def,
36            T_IMPLIES_def, NOW_def, NEXT_def]
37   \\ REPEAT strip_tac
38   \\ qpat_assum `!a. b`
39         (qspecl_then [`state`, `seq`, `r * r'`] imp_res_tac)
40   \\ fs [AC STAR_COMM STAR_ASSOC]
41   )
42
43val TEMPORAL_NEXT_DUPLICATE_COND = Q.store_thm("TEMPORAL_NEXT_DUPLICATE_COND",
44   `!x p c q g.
45        TEMPORAL_NEXT x (p * cond g) c q ==>
46        TEMPORAL_NEXT x (p * cond g) c (q * cond g)`,
47   simp [TEMPORAL_NEXT_MOVE_COND, SEP_CLAUSES]
48   )
49
50val TEMPORAL_NEXT_FALSE_PRE = Q.store_thm("TEMPORAL_NEXT_FALSE_PRE",
51   `!x c q. TEMPORAL_NEXT x SEP_F c q`,
52   INIT
53   \\ simp [SEP_F_def, TEMPORAL_NEXT_def, TEMPORAL_def, SEP_CLAUSES,
54            SEP_REFINE_def, T_IMPLIES_def, NOW_def]
55   )
56
57(* ------------------------------------------------------------------------ *)
58
59val CODE_POOL_EMP = Q.prove(
60   `!instr. CODE_POOL instr {} = emp`,
61   simp [CODE_POOL_def, emp_def]
62   )
63
64val SPLIT_STATE_cor = METIS_PROVE [SPLIT_STATE]
65   ``p (SELECT_STATE m y s) ==>
66     ?u v. SPLIT (STATE m s) (u, v) /\ p u /\ (\v. v = FRAME_STATE m y s) v``
67
68val TEMPORAL_STATE_SEMANTICS = Q.store_thm("TEMPORAL_STATE_SEMANTICS",
69   `!m next instr less avoid p q.
70       TEMPORAL_NEXT (STATE m, next, instr, less, avoid) p {} q =
71       !state y seq.
72          p (SELECT_STATE m y (seq 0)) /\ rel_sequence next seq state ==>
73          q (SELECT_STATE m y (seq 1)) /\
74          (FRAME_STATE m y (seq 0) = FRAME_STATE m y (seq 1))`,
75   simp [TEMPORAL_NEXT_def, TEMPORAL_def, T_IMPLIES_def, NOW_def, NEXT_def,
76         CODE_POOL_EMP, SEP_CLAUSES]
77   \\ simp [STAR_def, SEP_REFINE_def]
78   \\ REPEAT strip_tac
79   \\ Tactical.REVERSE eq_tac
80   \\ REPEAT strip_tac
81   >- (full_simp_tac std_ss [SPLIT_STATE]
82       \\ metis_tac [])
83   \\ imp_res_tac SPLIT_STATE_cor
84   \\ res_tac
85   \\ full_simp_tac bool_ss [SPLIT_STATE]
86   \\ metis_tac [FRAME_SET_EQ]
87   )
88
89val IMP_TEMPORAL = Q.prove(
90   `!m next instr less avoid p q.
91       (!y s.
92          p (SELECT_STATE m y s) ==>
93          ?v. (next s = SOME v) /\ q (SELECT_STATE m y v) /\
94              (FRAME_STATE m y s = FRAME_STATE m y v)) ==>
95       TEMPORAL_NEXT (STATE m, NEXT_REL (=) next, instr, less, avoid) p {} q`,
96   rewrite_tac [TEMPORAL_STATE_SEMANTICS]
97   \\ REPEAT strip_tac
98   \\ `NEXT_REL (=) next (seq 0) (seq (SUC 0))`
99   by (
100       `?x. NEXT_REL (=) next (seq 0) x`
101       by (res_tac
102           \\ qexists_tac `v`
103           \\ asm_simp_tac std_ss [NEXT_REL_def]
104           \\ qexists_tac `seq 0`
105           \\ asm_simp_tac std_ss []
106           \\ full_simp_tac bool_ss [rel_sequence_def]
107          )
108       \\ metis_tac [rel_sequence_def]
109      )
110   \\ full_simp_tac std_ss [NEXT_REL_def]
111   \\ qpat_assum `!y:'b set. P` (qspecl_then [`y`,`seq 0`] imp_res_tac)
112   \\ metis_tac [optionTheory.SOME_11]
113   )
114
115val TEMPORAL_NEXT_CODE = Q.store_thm("TEMPORAL_NEXT_CODE",
116   `!x p c q.
117       TEMPORAL_NEXT x (CODE_POOL (FST (SND (SND x))) c * p) {}
118                       (CODE_POOL (FST (SND (SND x))) c * q) =
119    TEMPORAL_NEXT x p c q`,
120   INIT
121   \\ simp [TEMPORAL_NEXT_def, TEMPORAL_def, T_IMPLIES_def, NOW_def, NEXT_def,
122            CODE_POOL_EMP, SEP_CLAUSES,
123            AC set_sepTheory.STAR_ASSOC set_sepTheory.STAR_COMM]
124   )
125
126val TEMPORAL_MOVE_CODE = Q.store_thm("TEMPORAL_MOVE_CODE",
127   `!to_set next instr less avoid p c q.
128       TEMPORAL_NEXT (to_set,next,instr,less,avoid)
129          (p * CODE_POOL instr c) {} (q * CODE_POOL instr c) =
130    TEMPORAL_NEXT (to_set,next,instr,less,avoid) p c q`,
131   simp [TEMPORAL_NEXT_def, TEMPORAL_def, T_IMPLIES_def, NOW_def, NEXT_def,
132         CODE_POOL_EMP, SEP_CLAUSES]
133   )
134
135val IMP_TEMPORAL = Theory.save_thm ("IMP_TEMPORAL",
136   IMP_TEMPORAL
137   |> Q.SPECL [`m`, `next`, `instr: 'd -> 'b # 'c -> bool`, `less`, `avoid`,
138               `p * CODE_POOL instr (c: 'd -> bool)`,
139               `q * CODE_POOL instr (c: 'd -> bool)`]
140   |> REWRITE_RULE [TEMPORAL_MOVE_CODE]
141   |> Q.GENL [`m`, `next`, `instr`, `less`, `avoid`, `c`, `p`, `q`]
142   )
143
144(* ------------------------------------------------------------------------ *)
145
146fun SPECC_FRAME_RULE frame th =
147   Thm.SPEC frame (Drule.MATCH_MP TEMPORAL_NEXT_FRAME th)
148
149val SEP_ARRAY_TEMPORAL_FRAME = Q.store_thm("SEP_ARRAY_TEMPORAL_FRAME",
150   `!x (prefix: 'a word list) (postfix: 'a word list) p c q m i a l1 l2.
151       (LENGTH l2 = LENGTH l1) /\
152       TEMPORAL_NEXT x (p * SEP_ARRAY m i a l1) c (q * SEP_ARRAY m i a l2) ==>
153       TEMPORAL_NEXT x (p * SEP_ARRAY m i (a - n2w (LENGTH prefix) * i)
154                                      (prefix ++ l1 ++ postfix)) c
155              (q * SEP_ARRAY m i (a - n2w (LENGTH prefix) * i)
156                             (prefix ++ l2 ++ postfix))`,
157   REPEAT strip_tac
158   \\ rewrite_tac [set_sepTheory.SEP_ARRAY_APPEND]
159   \\ pop_assum
160        (assume_tac o
161         SPECC_FRAME_RULE
162            ``SEP_ARRAY (m: 'e word -> 'a word -> ('c -> bool) -> bool) i
163                        (a - n2w (LENGTH prefix) * i) (prefix: 'a word list)``)
164   \\ pop_assum
165        (assume_tac o
166         SPECC_FRAME_RULE
167            ``SEP_ARRAY (m: 'e word -> 'a word -> ('c -> bool) -> bool) i
168                        (a - n2w (LENGTH (prefix: 'a word list)) * i +
169                         n2w (LENGTH (prefix ++ l1)) * i)
170                        (postfix: 'a word list)``)
171   \\ full_simp_tac (srw_ss()++helperLib.star_ss) []
172   )
173
174(* ------------------------------------------------------------------------ *)
175
176val () = export_theory ()
177