1open HolKernel boolLib bossLib 2open set_sepTheory progTheory 3 4val _ = new_theory "state" 5 6val _ = ParseExtras.temp_loose_equality() 7 8(* ------------------------------------------------------------------------ 9 We use Hoare triples defined in examples/machine-code/hoare-triple/progTheory 10 These are of the form: 11 12 SPEC (to_set,next,instr,less,allow) p c q 13 14 'a the state type 15 'b set the "set view" of states 16 'c the code-pool type 17 18 to_set : 'a -> 'b set maps states to a set view. 19 (This will be specialized to ``STATE m`` for 20 a map ``m: 'a -> ('name # 'value) set``. 21 The tool stateLib.sep_definitions helps 22 automatically define m, 'name and 'value for 23 L3 specifications.) 24 25 next : 'a -> 'a -> bool next-state relation. 26 (This will be specialized to 27 ``NEXT_REL (=) next`` for some next-state 28 function "next".) 29 30 instr : 'c -> 'b set maps the code pool to a set view. 31 32 less : 'a -> 'a -> bool ordering on states. 33 (This will be specialized to ``(=)``.) 34 35 allow : 'a -> bool "always valid" states. 36 (This will be specialized to ``K F``, i.e. 37 "Just use the supplied pre-condition and 38 post-condition predicates".) 39 40 p : 'b set -> bool pre-condition. 41 42 c : 'c -> bool code-pool. 43 44 q : 'b set -> bool post-condition. 45 ------------------------------------------------------------------------ *) 46 47(* ------------------------------------------------------------------------ 48 NEXT_REL is used to capture valid sequences of states, as determined by a 49 next-state function "next" (and state relation "r"). The next-state relation 50 supplied to SPEC is ``NEXT_REL r next : 'a -> 'a -> bool``. 51 52 We are only really interested in cases where "r" is pre-order on states. 53 The tools (in stateLib) go further and assume "r" is "=". Thus, the 54 specified sequence of states for 55 56 seq_relation (NEXT_REL (=) next) seq s 57 58 is 59 60 seq 0 = s, 61 seq 1 = THE (next s), 62 seq 2 = THE (next (THE (next s))), ... 63 64 If ``next (seq n) = NONE`` for some "n" then this final state is repeated 65 ad infinitum. 66 ------------------------------------------------------------------------ *) 67 68val NEXT_REL_def = Define` 69 NEXT_REL (r: 's -> 's -> bool) (next: 's -> 's option) s t = 70 ?u. r s u /\ (next u = SOME t)` 71 72val NEXT_REL_EQ = Q.store_thm ("NEXT_REL_EQ", 73 `!next. NEXT_REL (=) next = \s t. next s = SOME t`, 74 rw [NEXT_REL_def, FUN_EQ_THM]) 75 76(* ------------------------------------------------------------------------ 77 SELECT_STATE is used to construct a "set view" of states. 78 79 'a the state type 80 'b state component name type 81 'c state component value type 82 ('b # 'c) set the type for the set view of states 83 84 m : 'a -> 'b -> 'c converts a state into a map from names to values 85 d : 'b set the domain (component names) of interest 86 87 The set view is the graph of the map "m", i.e. 88 89 { (name, m s name) | name IN d } 90 91 Thus, ``SELECT_STATE m UNIV : 'a -> ('b # 'c) set`` is a suitable "to_set" 92 map in instances of SPEC. 93 94 For example, for ARM we have 95 96 'a is arm_state 97 'b is arm_component 98 'c is arm_data 99 m is arm_proj 100 101 The term ``SELECT_STATE arm_proj {arm_c_CPSR_Z} s`` then represents the set 102 103 {(arm_c_CPSR_Z, arm_proj s arm_c_CPSR_Z)} 104 105 which is defined to be 106 107 {(arm_c_CPSR_Z, arm_d_bool s.CPSR.Z)} 108 109 Thus, component ``arm_c_CPSR_Z`` is associated with the value ``s.CPSR.Z``. 110 111 A predicate arm_CPSR_Z is defined as follows 112 113 !d. arm_CPSR_Z d = {{(arm_c_CPSR_Z,arm_d_bool d)}} 114 115 ------------------------------------------------------------------------ *) 116 117val SELECT_STATE_def = Define `SELECT_STATE m d s = fun2set (m s, d)` 118 119(* The "universal" to-set map *) 120 121val STATE_def = Define `STATE m = SELECT_STATE m UNIV` 122 123(* The "complement" to-set map *) 124 125val FRAME_STATE_def = Define `FRAME_STATE m d = SELECT_STATE m (COMPL d)` 126 127(* ------------------------------------------------------------------------ 128 We now show that 129 130 PreOrder r ==> 131 (!y s t1. 132 p (SELECT_STATE m y t1) /\ r t1 s ==> 133 ?v t2. 134 p (SELECT_STATE m y s) /\ 135 (next s = SOME v) /\ 136 q (SELECT_STATE m y t2) /\ r t2 v /\ 137 (FRAME_STATE m y t1 = FRAME_STATE m y t2)) ==> 138 SPEC (STATE m, NEXT_REL r next, instr, r, K F) p {} q`, 139 140 and this is then used to show that 141 142 (!y s. 143 (p * CODE_POOL instr c) (SELECT_STATE m y s) ==> 144 ?v. 145 (next s = SOME v) /\ 146 (q * CODE_POOL instr c) (SELECT_STATE m y v) /\ 147 (FRAME_STATE m y s = FRAME_STATE m y v)) ==> 148 SPEC (STATE m,NEXT_REL $= next,instr,$=,K F) p c q 149 150 This theorem is used to derive SPEC theorems for machine-code instructions. 151 Given a next-state theorem of the form 152 153 p1 /\ ... /\ pn ==> (next s = SOME v), 154 155 the procedure is as follows: 156 157 - Use MATCH_MP and proceed to show the antecedent is true. 158 159 - Use GEN_TAC and STIP_TAC, so that we assume assertions for "s" from 160 pre-condition "p" and "CODE_POOL instr c". 161 162 Assertion "p" will normally consist of a starred collection of 163 state component assertions. These are expanded using the theorem 164 STAR_SELECT_STATE below. The definition of "m" is also used. 165 For example, if we have 166 167 (arm_CPSR_Z v * p) (SELECT_STATE arm_proj y s) 168 169 then this can be used to deduce ``arm_c_CPSR_Z IN y`` and 170 ``s.CPSR.Z = v``. We then iterate on the remaining "p". 171 172 - We now have three sub-goals. 173 174 1. Prove the existance of a next-state for "s". The witness comes 175 from the RHS of the supplied next-state theorem. The main task 176 is to verify that each condition "p1, ..., pn" is satisfied by 177 the assumptions (pre-condition assertions). 178 179 2. Show that state "v" satisfies the post-condition assertions in "q". 180 Again, this uses the STAR_SELECT_STATE. This time extra rewrites 181 are needed to reason about state (record and map) updates. 182 183 3. Show that the "s" and "v" do not differ for components that are not 184 mentioned in "y". This is based on using theorem UPDATE_FRAME_STATE 185 below. The tool stateLib.update_frame_state_thm can be used to 186 generate appropriate theorem instances for an L3 specification 187 188 ------------------------------------------------------------------------ *) 189 190val SPLIT_STATE = Q.store_thm ("SPLIT_STATE", 191 `!m s u v. 192 SPLIT (STATE m s) (u, v) = 193 ?y. (u = SELECT_STATE m y s) /\ (v = FRAME_STATE m y s)`, 194 rw [SPLIT_def, STATE_def, SELECT_STATE_def, FRAME_STATE_def, 195 pred_setTheory.DISJOINT_DEF, fun2set_def] 196 \\ eq_tac 197 \\ rw [pred_setTheory.EXTENSION] 198 >| [ 199 qexists_tac `IMAGE FST u` 200 \\ rw [] 201 \\ metis_tac [pairTheory.FST], 202 eq_tac \\ rw [], 203 metis_tac [pairTheory.FST] 204 ]) 205 206val SPLIT_STATE_cor = METIS_PROVE [SPLIT_STATE] 207 ``p (SELECT_STATE m y s) ==> 208 ?u v. SPLIT (STATE m s) (u, v) /\ p u /\ (\v. v = FRAME_STATE m y s) v`` 209 210val FRAME_SET_EQ = Q.store_thm ("FRAME_SET_EQ", 211 `!m x y s t. (FRAME_STATE m x s = FRAME_STATE m y t) ==> (x = y)`, 212 simp [pred_setTheory.EXTENSION, FRAME_STATE_def, SELECT_STATE_def, 213 fun2set_def] 214 \\ metis_tac [pairTheory.FST]) 215 216val R_STATE_SEMANTICS = Q.store_thm ("R_STATE_SEMANTICS", 217 `!m next instr r p q. 218 SPEC (STATE m, next, instr, r, K F) p {} q = 219 !y s t1 seq. 220 p (SELECT_STATE m y t1) /\ r t1 s /\ rel_sequence next seq s ==> 221 ?k t2. q (SELECT_STATE m y t2) /\ r t2 (seq k) /\ 222 (FRAME_STATE m y t1 = FRAME_STATE m y t2)`, 223 simp [GSYM RUN_EQ_SPEC, RUN_def, STAR_def, SEP_REFINE_def] 224 \\ REPEAT strip_tac 225 \\ Tactical.REVERSE eq_tac 226 \\ REPEAT strip_tac 227 >- (full_simp_tac std_ss [SPLIT_STATE] 228 \\ metis_tac []) 229 \\ full_simp_tac std_ss 230 [METIS_PROVE [] ``((?x. P x) ==> b) = !x. P x ==> b``, 231 METIS_PROVE [] ``(b /\ (?x. P x)) = ?x. b /\ P x``] 232 \\ full_simp_tac std_ss [GSYM AND_IMP_INTRO] 233 \\ imp_res_tac SPLIT_STATE_cor 234 \\ res_tac 235 \\ full_simp_tac bool_ss [SPLIT_STATE] 236 \\ metis_tac [FRAME_SET_EQ] 237 ) 238 239val STATE_SEMANTICS = Q.store_thm ("STATE_SEMANTICS", 240 `!m next instr p q. 241 SPEC (STATE m, next, instr, $=, K F) p {} q = 242 !y s seq. 243 p (SELECT_STATE m y s) /\ rel_sequence next seq s ==> 244 ?k. q (SELECT_STATE m y (seq k)) /\ 245 (FRAME_STATE m y s = FRAME_STATE m y (seq k))`, 246 rw [R_STATE_SEMANTICS]) 247 248val IMP_R_SPEC = Q.prove( 249 `!r m next instr p q. 250 PreOrder r ==> 251 (!y s t1. 252 p (SELECT_STATE m y t1) /\ r t1 s ==> 253 ?v t2. 254 p (SELECT_STATE m y s) /\ 255 (next s = SOME v) /\ q (SELECT_STATE m y t2) /\ r t2 v /\ 256 (FRAME_STATE m y t1 = FRAME_STATE m y t2)) ==> 257 SPEC (STATE m, NEXT_REL r next, instr, r, K F) p {} q`, 258 rewrite_tac [R_STATE_SEMANTICS, relationTheory.PreOrder, 259 relationTheory.reflexive_def, relationTheory.transitive_def] 260 \\ REPEAT strip_tac 261 \\ `p (SELECT_STATE m y s)` by metis_tac [] 262 \\ `NEXT_REL r next (seq 0) (seq (SUC 0))` 263 by ( 264 `?x. NEXT_REL r next (seq 0) x` 265 by (res_tac 266 \\ qexists_tac `v` 267 \\ asm_simp_tac std_ss [NEXT_REL_def] 268 \\ qexists_tac `seq 0` 269 \\ asm_simp_tac std_ss [] 270 \\ full_simp_tac bool_ss [rel_sequence_def] 271 ) 272 \\ metis_tac [rel_sequence_def] 273 ) 274 \\ full_simp_tac std_ss [NEXT_REL_def] 275 \\ `seq 0 = s` by full_simp_tac std_ss [rel_sequence_def] 276 \\ full_simp_tac std_ss [] 277 \\ qexists_tac `1` 278 \\ `r t1 u` by metis_tac [] 279 \\ qpat_assum `!y:'b set. P` 280 (qspecl_then [`y`,`u`,`t1`] 281 (strip_assume_tac o UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO])) 282 \\ qexists_tac `t2` 283 \\ metis_tac [optionTheory.SOME_11] 284 ) 285 286val PreOrder_EQ = Q.store_thm ("PreOrder_EQ", 287 `PreOrder (=)`, 288 rw [relationTheory.PreOrder, relationTheory.reflexive_def, 289 relationTheory.transitive_def]) 290 291val IMP_SPEC = Q.prove( 292 `!m next instr p q. 293 (!y s. 294 p (SELECT_STATE m y s) ==> 295 ?v. (next s = SOME v) /\ q (SELECT_STATE m y v) /\ 296 (FRAME_STATE m y s = FRAME_STATE m y v)) ==> 297 SPEC (STATE m, NEXT_REL (=) next, instr, (=), K F) p {} q`, 298 REPEAT strip_tac 299 \\ qspec_then `(=)` (match_mp_tac o REWRITE_RULE [PreOrder_EQ]) IMP_R_SPEC 300 \\ metis_tac []) 301 302val STATE_SPEC_CODE = 303 Drule.ISPEC 304 (IMP_R_SPEC 305 |> Drule.SPEC_ALL 306 |> Thm.concl 307 |> boolSyntax.dest_imp |> snd 308 |> boolSyntax.dest_imp |> snd 309 |> boolSyntax.rator 310 |> boolSyntax.rator 311 |> boolSyntax.rator 312 |> boolSyntax.rand) SPEC_CODE 313 |> SIMP_RULE std_ss [] 314 |> Drule.GEN_ALL 315 316val IMP_R_SPEC = Theory.save_thm ("IMP_R_SPEC", 317 IMP_R_SPEC 318 |> Q.SPECL [`r`, `m`, `next`, `instr: 'd -> 'b # 'c -> bool`, 319 `CODE_POOL instr (c: 'd -> bool) * p`, 320 `CODE_POOL instr (c: 'd -> bool) * q`] 321 |> REWRITE_RULE [STATE_SPEC_CODE] 322 |> ONCE_REWRITE_RULE [STAR_COMM] 323 |> Q.GENL [`r`, `m`, `next`, `instr`, `c`, `p`, `q`] 324 ) 325 326val IMP_SPEC = Theory.save_thm ("IMP_SPEC", 327 IMP_SPEC 328 |> Q.SPECL [`m`, `next`, `instr: 'd -> 'b # 'c -> bool`, 329 `CODE_POOL instr (c: 'd -> bool) * p`, 330 `CODE_POOL instr (c: 'd -> bool) * q`] 331 |> REWRITE_RULE [STATE_SPEC_CODE] 332 |> ONCE_REWRITE_RULE [STAR_COMM] 333 |> Q.GENL [`m`, `next`, `instr`, `c`, `p`, `q`] 334 ) 335 336val SEP_EQ_SINGLETON = Q.store_thm ("SEP_EQ_SINGLETON", 337 `!x. SEP_EQ x = { x }`, 338 rw [SEP_EQ_def, pred_setTheory.EXTENSION, boolTheory.IN_DEF]) 339 340val CODE_POOL = Theory.save_thm ("CODE_POOL", 341 REWRITE_RULE [GSYM SEP_EQ_def, SEP_EQ_SINGLETON] CODE_POOL_def) 342 343(* ........................................................................ *) 344 345(* 346val DIFF_EMPTY = Q.store_thm("DIFF_EMPTY", 347 `!t v s. (t = v) /\ (s DIFF t = {}) ==> (s DIFF v = {})`, 348 ntac 2 (srw_tac [] []) 349 ) 350*) 351 352val IN_SUBSET = Q.prove( 353 `!a A B. a IN A /\ A SUBSET B ==> a IN B`, 354 srw_tac [] [pred_setTheory.SUBSET_DEF]) 355 356val PAIR_GRAPH = Q.prove( 357 `!m s. 358 (!e. e IN s ==> (SND e = m (FST e))) = 359 (!a b. (a, b) IN s ==> (b = m a))`, 360 REPEAT strip_tac 361 \\ eq_tac 362 \\ rw [] 363 \\ metis_tac [pairTheory.FST, pairTheory.SND]) 364 365val IN_fun2set_cor = 366 IN_fun2set 367 |> Q.SPECL [`FST c`, `SND c`] 368 |> REWRITE_RULE [pairTheory.PAIR] 369 |> Drule.GEN_ALL 370 371val SUBSET_fun2set = Q.prove( 372 `!m s cd x. 373 cd SUBSET fun2set (m s, x) = 374 IMAGE FST cd SUBSET x /\ (!e. e IN cd ==> (SND e = m s (FST e)))`, 375 rw [fun2set_def, pred_setTheory.SUBSET_DEF] 376 \\ eq_tac 377 \\ rw [] 378 \\ metis_tac [pairTheory.FST, pairTheory.SND, pairTheory.PAIR] 379 ) 380 381val fun2set_DIFF = Q.prove( 382 `!x f q. (!e. e IN q ==> (SND e = f (FST e))) ==> 383 (fun2set (f, x) DIFF q = fun2set (f, x DIFF IMAGE FST q))`, 384 rw [pred_setTheory.EXTENSION, IN_fun2set_cor] 385 \\ eq_tac 386 \\ rw [] 387 \\ metis_tac [pairTheory.FST, pairTheory.SND, pairTheory.PAIR] 388 ) 389 390val fun2set_DIFF2 = Q.prove( 391 `!x m s q. 392 q SUBSET (fun2set (m s, x)) ==> 393 (fun2set (m s, x) DIFF q = fun2set (m s, x DIFF IMAGE FST q))`, 394 metis_tac [fun2set_DIFF, SUBSET_fun2set, PAIR_GRAPH] 395 ) 396 397val STAR_SELECT_STATE = Q.store_thm ("STAR_SELECT_STATE", 398 `!cd m p s x. 399 ({cd} * p) (SELECT_STATE m x s) = 400 (!c d. (c, d) IN cd ==> (m s c = d)) /\ IMAGE FST cd SUBSET x /\ 401 p (SELECT_STATE m (x DIFF IMAGE FST cd) s)`, 402 REPEAT strip_tac 403 \\ once_rewrite_tac [GSYM SEP_EQ_SINGLETON] 404 \\ simp [SELECT_STATE_def, EQ_STAR] 405 \\ eq_tac 406 \\ rw [] 407 >- metis_tac [IN_SUBSET, IN_fun2set, PAIR_GRAPH] 408 >- metis_tac [SUBSET_fun2set] 409 >- metis_tac [fun2set_DIFF2, PAIR_GRAPH] 410 >- metis_tac [fun2set_DIFF, PAIR_GRAPH] 411 \\ metis_tac [SUBSET_fun2set, PAIR_GRAPH] 412 ) 413 414(* 415val STAR_SELECT_STATE1 = Theory.save_thm ("STAR_SELECT_STATE1", 416 STAR_SELECT_STATE 417 |> Q.SPEC `{(v, w)}` 418 |> SIMP_RULE (srw_ss()) [GSYM pred_setTheory.DELETE_DEF] 419 |> Drule.GEN_ALL 420 ) 421*) 422 423val emp_SELECT_STATE = Q.store_thm ("emp_SELECT_STATE", 424 `!m x s. emp (SELECT_STATE m x s) = (x = {})`, 425 rw [emp_def, SELECT_STATE_def, fun2set_def, pred_setTheory.EXTENSION] 426 ) 427 428(* ........................................................................ *) 429 430val UPDATE_FRAME_STATE = Q.store_thm ("UPDATE_FRAME_STATE", 431 `!m f u r. 432 (!b s a w. b <> f a ==> (m (u s a w) b = m (r s) b)) ==> 433 !a w s x. 434 f a IN x ==> (FRAME_STATE m x (u s a w) = FRAME_STATE m x (r s))`, 435 rw [FRAME_STATE_def, SELECT_STATE_def, fun2set_def, pred_setTheory.EXTENSION] 436 \\ metis_tac [] 437 ) 438 439(* ------------------------------------------------------------------------ *) 440 441val cond_true_elim = Theory.save_thm("cond_true_elim", 442 simpLib.SIMP_PROVE bool_ss [set_sepTheory.SEP_CLAUSES] 443 ``(!p:'a set set. p * cond T = p) /\ 444 (!p:'a set set. cond T * p = p)``) 445 446val UNION_STAR = Q.store_thm("UNION_STAR", 447 `!a b c. DISJOINT a b ==> ({a UNION b} * c = {a} * {b} * c)`, 448 simp [set_sepTheory.STAR_def, set_sepTheory.SPLIT_def] 449 ) 450 451val BIGUNION_IMAGE_1 = Q.store_thm("BIGUNION_IMAGE_1", 452 `!f x. BIGUNION (IMAGE f {x}) = f x`, 453 simp [] 454 ) 455 456val BIGUNION_IMAGE_2 = Q.store_thm("BIGUNION_IMAGE_2", 457 `!f x y. BIGUNION (IMAGE f {x; y}) = f x UNION f y`, 458 simp [] 459 ) 460 461(* ........................................................................ *) 462 463val SEP_EQ_STAR = Q.store_thm("SEP_EQ_STAR", 464 `((q = p1 UNION p2) /\ DISJOINT p1 p2) ==> 465 ((SEP_EQ p1 * SEP_EQ p2) = (SEP_EQ q))`, 466 REPEAT strip_tac 467 \\ simp_tac std_ss [SEP_EQ_def, Once FUN_EQ_THM, STAR_def, SPLIT_def] 468 \\ METIS_TAC [] 469 ) 470 471val MAPPED_COMPONENT_INSERT = Q.store_thm("MAPPED_COMPONENT_INSERT", 472 `!P n x y single_c map_c. 473 (!c d. single_c c d = {set (GENLIST (\i. (x c i, y d i)) n)}) ==> 474 (!a b i j. P a /\ P b /\ i < n /\ j < n ==> 475 ((x a i = x b j) = (a = b) /\ (i = j))) /\ 476 (!df f. map_c df f = 477 {BIGUNION {BIGUNION (single_c c (f c)) | c | c IN df /\ P c}}) ==> 478 !f df c d. 479 c IN df /\ P c ==> 480 (single_c c d * map_c (df DELETE c) f = map_c df ((c =+ d) f))`, 481 REPEAT strip_tac 482 \\ asm_rewrite_tac [GSYM SEP_EQ_SINGLETON] 483 \\ match_mp_tac SEP_EQ_STAR 484 \\ rewrite_tac [SEP_EQ_SINGLETON, pred_setTheory.BIGUNION_SING, 485 pred_setTheory.DISJOINT_DEF, pred_setTheory.EXTENSION] 486 \\ rw [boolTheory.PULL_EXISTS, combinTheory.APPLY_UPDATE_THM, 487 listTheory.MEM_GENLIST] 488 >- metis_tac [] 489 \\ Cases_on `x'` \\ simp [] (* shouldn't rely on name here *) 490 \\ Cases_on `i < n` \\ simp [] 491 \\ Cases_on `i' < n` \\ simp [] 492 \\ metis_tac [] 493 ) 494 495val cnv = SIMP_CONV (srw_ss()) [DECIDE ``i < 1n = (i = 0)``] 496 497val MAPPED_COMPONENT_INSERT1 = Theory.save_thm("MAPPED_COMPONENT_INSERT1", 498 MAPPED_COMPONENT_INSERT 499 |> Q.SPECL [`K T`, `1n`, `\c i. x c`, `\d i. y d`] 500 |> Conv.CONV_RULE 501 (Conv.STRIP_QUANT_CONV 502 (Conv.RATOR_CONV cnv 503 THENC Conv.RAND_CONV (Conv.RATOR_CONV cnv) 504 THENC REWRITE_CONV [combinTheory.K_THM])) 505 |> Drule.GEN_ALL) 506 507val MAPPED_COMPONENT_INSERT_OPT = Q.store_thm("MAPPED_COMPONENT_INSERT_OPT", 508 `!y x single_c map_c. 509 (!c d. single_c c d = {{(x c,y d)}}) ==> 510 (!a b. (x a = x b) <=> (a = b)) /\ 511 (!df f. 512 map_c df f = 513 {BIGUNION {BIGUNION (single_c c (SOME (f c))) | c IN df}}) ==> 514 !f df c d. 515 c IN df ==> 516 (single_c c (SOME d) * map_c (df DELETE c) f = map_c df ((c =+ d) f))`, 517 REPEAT strip_tac 518 \\ asm_rewrite_tac [GSYM SEP_EQ_SINGLETON] 519 \\ match_mp_tac SEP_EQ_STAR 520 \\ rewrite_tac [SEP_EQ_SINGLETON, pred_setTheory.BIGUNION_SING, 521 pred_setTheory.DISJOINT_DEF, pred_setTheory.EXTENSION] 522 \\ rw [boolTheory.PULL_EXISTS, combinTheory.APPLY_UPDATE_THM] 523 >- metis_tac [] 524 \\ Cases_on `x'` \\ simp [] (* shouldn't rely on name here *) 525 \\ metis_tac [] 526 ) 527 528(* ........................................................................ *) 529 530val SEP_ARRAY_FRAME = Q.store_thm("SEP_ARRAY_FRAME", 531 `!x (prefix: 'a word list) (postfix: 'a word list) p c q m i a l1 l2. 532 (LENGTH l2 = LENGTH l1) /\ 533 SPEC x (p * SEP_ARRAY m i a l1) c (q * SEP_ARRAY m i a l2) ==> 534 SPEC x (p * SEP_ARRAY m i (a - n2w (LENGTH prefix) * i) 535 (prefix ++ l1 ++ postfix)) c 536 (q * SEP_ARRAY m i (a - n2w (LENGTH prefix) * i) 537 (prefix ++ l2 ++ postfix))`, 538 REPEAT strip_tac 539 \\ rewrite_tac [set_sepTheory.SEP_ARRAY_APPEND] 540 \\ pop_assum 541 (assume_tac o 542 helperLib.SPECC_FRAME_RULE 543 ``SEP_ARRAY (m: 'e word -> 'a word -> ('c -> bool) -> bool) i 544 (a - n2w (LENGTH prefix) * i) (prefix: 'a word list)``) 545 \\ pop_assum 546 (assume_tac o 547 helperLib.SPECC_FRAME_RULE 548 ``SEP_ARRAY (m: 'e word -> 'a word -> ('c -> bool) -> bool) i 549 (a - n2w (LENGTH (prefix: 'a word list)) * i + 550 n2w (LENGTH (prefix ++ l1)) * i) 551 (postfix: 'a word list)``) 552 \\ full_simp_tac (srw_ss()++helperLib.star_ss) [] 553 ) 554 555(* ------------------------------------------------------------------------ *) 556 557val () = export_theory () 558