1open HolKernel Parse boolLib bossLib; 2 3(* 4quietdec := true; 5loadPath := 6 (concat [Globals.HOLDIR, "/examples/decidable_separationLogic/src"]) :: 7 !loadPath; 8 9map load ["finite_mapTheory", "relationTheory", "congLib", "sortingTheory", 10 "rich_listTheory", "decidable_separationLogicTheory", "listLib", "stringTheory", "pred_setLib"]; 11show_assums := true; 12*) 13 14open finite_mapTheory relationTheory pred_setTheory congLib sortingTheory 15 listTheory rich_listTheory decidable_separationLogicTheory listLib stringTheory; 16 17 18(* 19quietdec := false; 20*) 21 22val _ = new_theory "decidable_separationLogicLib"; 23 24 25val nchotomy_thm = prove (``!x. 26 (x = sf_emp) \/ (?d l. x = sf_points_to d l) \/ 27 (?l d d0. x = sf_tree l d d0) \/ ?d d0. x = sf_star d d0``, 28 REWRITE_TAC [TypeBase.nchotomy_of ``:('a,'b,'c) ds_spatial_formula``]); 29 30val _ = TypeBase.write [TypeBasePure.put_nchotomy nchotomy_thm (valOf (TypeBase.fetch ``:('a,'b,'c) ds_spatial_formula``))]; 31 32 33 34val INFINITE_UNIV___NUM = store_thm ("INFINITE_UNIV___NUM", 35 ``INFINITE (UNIV:num set)``, 36 37SIMP_TAC std_ss [INFINITE_UNIV] THEN 38Q.EXISTS_TAC `SUC` THEN 39SIMP_TAC std_ss [] THEN 40Q.EXISTS_TAC `0` THEN 41DECIDE_TAC); 42 43 44 45 46val INFINITE_UNIV___STRING = store_thm ("INFINITE_UNIV___STRING", 47 ``INFINITE (UNIV:string set)``, 48 49SIMP_TAC std_ss [INFINITE_UNIV] THEN 50Q.EXISTS_TAC `STRING c` THEN 51SIMP_TAC list_ss [] THEN 52Q.EXISTS_TAC `""` THEN 53SIMP_TAC list_ss []); 54 55 56 57 58val SAFE_EL_def = Define ` 59 (SAFE_EL e n [] = e) /\ 60 (SAFE_EL e 0 (x::l) = x) /\ 61 (SAFE_EL e (SUC n) (x::l) = SAFE_EL e n l)` 62 63 64val SAFE_EL_SEM = store_thm ("SAFE_EL_SEM", 65 ``!e n l. SAFE_EL e n l = 66 if (n < LENGTH l) then EL n l else e``, 67 68 Induct_on `n` THENL [ 69 Cases_on `l` THEN SIMP_TAC list_ss [SAFE_EL_def], 70 Cases_on `l` THEN ASM_SIMP_TAC list_ss [SAFE_EL_def] 71 ]) 72 73 74val SAFE_DEL_EL_def = Define ` 75 (SAFE_DEL_EL n [] = []) /\ 76 (SAFE_DEL_EL 0 (x::l) = [x]) /\ 77 (SAFE_DEL_EL (SUC n) (x::l) = SAFE_DEL_EL n l)` 78 79val SAFE_DEL_EL_THM = store_thm ("SAFE_DEL_EL_THM", 80 ``(!n. (SAFE_DEL_EL n [] = [])) /\ 81 (!x l. (SAFE_DEL_EL 0 (x::l) = [x])) /\ 82 (!n x l. (SAFE_DEL_EL (SUC n) (x::l) = SAFE_DEL_EL n l))``, 83 84REWRITE_TAC [SAFE_DEL_EL_def]); 85 86 87 88val SAFE_DEL_EL_SEM = store_thm ("SAFE_DEL_EL_SEM", 89 ``(!n (l:'a list). (n < LENGTH l) ==> (SAFE_DEL_EL n l = [EL n l])) /\ 90 (!n (l:'a list). ~(n < LENGTH l) ==> (SAFE_DEL_EL n l = []))``, 91 92 SIMP_TAC std_ss [GSYM FORALL_AND_THM] THEN 93 Induct_on `n` THENL [ 94 Cases_on `l` THEN SIMP_TAC list_ss [SAFE_DEL_EL_THM], 95 Cases_on `l` THEN ASM_SIMP_TAC list_ss [SAFE_DEL_EL_THM] 96 ]) 97 98 99val DELETE_ELEMENT_def = Define ` 100 (DELETE_ELEMENT n [] = []) /\ 101 (DELETE_ELEMENT 0 (x::l) = l) /\ 102 (DELETE_ELEMENT (SUC n) (x::l) = x::DELETE_ELEMENT n l)` 103 104val DELETE_ELEMENT_THM = store_thm ("DELETE_ELEMENT_THM", 105 ``(!n. DELETE_ELEMENT n [] = []) /\ 106 (!x l. DELETE_ELEMENT 0 (x::l) = l) /\ 107 (!n x l. (DELETE_ELEMENT (SUC n) (x::l) = x::DELETE_ELEMENT n l))``, 108 109 REWRITE_TAC [DELETE_ELEMENT_def]) 110 111 112val MEM_DELETE_ELEMENT = store_thm ("MEM_DELETE_ELEMENT", 113 ``!x n l. ((~(x = EL n l)) /\ MEM x l) ==> 114 MEM x (DELETE_ELEMENT n l)``, 115 116 117 Induct_on `l` THENL [ 118 SIMP_TAC list_ss [DELETE_ELEMENT_THM], 119 120 Cases_on `n` THEN ( 121 SIMP_TAC list_ss [DELETE_ELEMENT_THM] THEN 122 METIS_TAC[] 123 ) 124 ]); 125 126 127val LENGTH_DELETE_ELEMENT = store_thm ("LENGTH_DELETE_ELEMENT", 128 ``!n l. LENGTH (DELETE_ELEMENT n l) = 129 if (n < LENGTH l) then PRE (LENGTH l) else LENGTH l``, 130 131 Induct_on `l` THENL [ 132 SIMP_TAC list_ss [DELETE_ELEMENT_THM], 133 134 Cases_on `n` THEN ( 135 ASM_SIMP_TAC list_ss [DELETE_ELEMENT_THM] 136 ) 137 ]); 138 139 140val EL_DELETE_ELEMENT = store_thm ("EL_DELETE_ELEMENT", 141 ``(!n1 n2 l. ((n1 < n2) ==> (EL n1 (DELETE_ELEMENT n2 l) = EL n1 l))) /\ 142 (!n1 n2 l. (~(n1 < n2) /\ (n1 < LENGTH l)) ==> (EL n1 (DELETE_ELEMENT n2 l) = EL (SUC n1) l))``, 143 144 CONJ_TAC THENL [ 145 Induct_on `l` THENL [ 146 SIMP_TAC list_ss [DELETE_ELEMENT_THM], 147 148 Cases_on `n2` THENL [ 149 SIMP_TAC list_ss [], 150 151 SIMP_TAC list_ss [DELETE_ELEMENT_THM] THEN 152 Cases_on `n1` THEN SIMP_TAC list_ss [] THEN 153 ASM_SIMP_TAC std_ss [] 154 ] 155 ], 156 157 158 Induct_on `l` THENL [ 159 SIMP_TAC list_ss [DELETE_ELEMENT_THM], 160 161 Cases_on `n1` THENL [ 162 SIMP_TAC list_ss [] THEN 163 REPEAT STRIP_TAC THEN 164 `n2 = 0` by DECIDE_TAC THEN 165 ASM_SIMP_TAC std_ss [DELETE_ELEMENT_THM], 166 167 168 SIMP_TAC list_ss [] THEN 169 Cases_on `n2` THENL [ 170 SIMP_TAC list_ss [DELETE_ELEMENT_THM], 171 ASM_SIMP_TAC list_ss [DELETE_ELEMENT_THM] 172 ] 173 ] 174 ] 175 ] 176); 177 178 179 180 181val DELETE_ELEMENT_DELETE_ELEMENT = store_thm ("EL_DELETE_ELEMENT", 182 ``!n1 n2 l. ((n1 <= n2) ==> (DELETE_ELEMENT n2 (DELETE_ELEMENT n1 l) = 183 DELETE_ELEMENT n1 (DELETE_ELEMENT (SUC n2) l)))``, 184 185 Induct_on `l` THENL [ 186 SIMP_TAC list_ss [DELETE_ELEMENT_THM], 187 188 Cases_on `n1` THEN Cases_on `n2` THEN ( 189 ASM_SIMP_TAC list_ss [DELETE_ELEMENT_THM] 190 ) 191 ]); 192 193 194val SWAP_ELEMENTS_def = Define ` 195 (SWAP_ELEMENTS 0 0 l = l) /\ 196 (SWAP_ELEMENTS (SUC n) 0 l = l) /\ 197 (SWAP_ELEMENTS x y [] = []) /\ 198 (SWAP_ELEMENTS x y [e] = [e]) /\ 199 (SWAP_ELEMENTS 0 (SUC n) (e1::e2::l) = (SAFE_EL e1 n (e2::l)) :: REPLACE_ELEMENT e1 n (e2::l)) /\ 200 (SWAP_ELEMENTS (SUC m) (SUC n) (e::l) = e:: (SWAP_ELEMENTS m n l))` 201 202val SWAP_ELEMENTS_THM = store_thm ("SWAP_ELEMENTS_THM", 203 ``(!x y (l:'a list). y <= x ==> (SWAP_ELEMENTS x y l = l)) /\ 204 (!x y. SWAP_ELEMENTS x y [] = ([]:'a list)) /\ 205 (!x y e:'a. SWAP_ELEMENTS x y [e] = [e]) /\ 206 (!y e (l:'a list). SWAP_ELEMENTS y y l = l) /\ 207 (!y e (l:'a list). SWAP_ELEMENTS (SUC y) 0 l = l) /\ 208 (!y e (l:'a list). 209 (SWAP_ELEMENTS 0 (SUC y) (e::l) = (SAFE_EL e y l) :: REPLACE_ELEMENT e y l)) /\ 210 (!x y e (l:'a list). (SWAP_ELEMENTS (SUC x) (SUC y) (e::l) = e:: (SWAP_ELEMENTS x y l))) 211``, 212 MATCH_MP_TAC (prove (``(a /\ (a ==> b)) ==> (a /\ b)``, PROVE_TAC[])) THEN 213 CONJ_TAC THEN1 ( 214 Induct_on `x` THENL [ 215 Cases_on `l` THENL [ 216 SIMP_TAC std_ss [SWAP_ELEMENTS_def], 217 Cases_on `t` THEN SIMP_TAC std_ss [SWAP_ELEMENTS_def] 218 ], 219 220 Cases_on `y` THENL [ 221 Cases_on `l` THENL [ 222 SIMP_TAC std_ss [SWAP_ELEMENTS_def], 223 Cases_on `t` THEN SIMP_TAC std_ss [SWAP_ELEMENTS_def] 224 ], 225 226 Cases_on `l` THENL [ 227 SIMP_TAC std_ss [SWAP_ELEMENTS_def], 228 229 Cases_on `t` THEN 230 ASM_SIMP_TAC std_ss [SWAP_ELEMENTS_def] 231 ] 232 ] 233 ] 234 ) THEN 235 STRIP_TAC THEN 236 REPEAT CONJ_TAC THENL [ 237 Cases_on `x` THEN Cases_on `y` THEN 238 SIMP_TAC std_ss [SWAP_ELEMENTS_def], 239 240 Cases_on `x` THEN Cases_on `y` THEN 241 SIMP_TAC std_ss [SWAP_ELEMENTS_def], 242 243 ASM_SIMP_TAC arith_ss [], 244 245 ASM_SIMP_TAC arith_ss [], 246 247 Cases_on `l` THENL [ 248 SIMP_TAC std_ss [SWAP_ELEMENTS_def] THEN 249 Cases_on `y` THEN 250 SIMP_TAC std_ss [SAFE_EL_def, REPLACE_ELEMENT_def], 251 252 SIMP_TAC std_ss [SWAP_ELEMENTS_def] 253 ], 254 255 Cases_on `l` THEN 256 Cases_on `x` THEN Cases_on `y` THEN 257 SIMP_TAC std_ss [SWAP_ELEMENTS_def] 258 ]) 259 260 261 262val SWAP_ELEMENTS_SEM = store_thm ("SWAP_ELEMENTS_SEM", 263 ``!x y l. ((x <= y) /\ y < LENGTH l) ==> 264 ((EL x (SWAP_ELEMENTS x y l) = EL y l) /\ 265 (EL y (SWAP_ELEMENTS x y l) = EL x l) /\ 266 (!p. (~(p = x) /\ ~(p = y) /\ (p < LENGTH l)) ==> 267 (EL p (SWAP_ELEMENTS x y l) = EL p l)))``, 268 269 Induct_on `x` THENL [ 270 Induct_on `y` THENL [ 271 SIMP_TAC list_ss [SWAP_ELEMENTS_THM], 272 273 Cases_on `l` THEN1 SIMP_TAC list_ss [] THEN 274 SIMP_TAC list_ss [SWAP_ELEMENTS_THM, SAFE_EL_SEM, REPLACE_ELEMENT_SEM] THEN 275 REPEAT STRIP_TAC THEN 276 Cases_on `p` THENL [ 277 FULL_SIMP_TAC std_ss [], 278 279 FULL_SIMP_TAC list_ss [REPLACE_ELEMENT_SEM] 280 ] 281 ], 282 283 Cases_on `y` THEN1 SIMP_TAC list_ss [] THEN 284 Cases_on `l` THEN1 SIMP_TAC list_ss [] THEN 285 286 ASM_SIMP_TAC list_ss [SWAP_ELEMENTS_THM] THEN 287 REPEAT STRIP_TAC THEN 288 Cases_on `p` THENL [ 289 SIMP_TAC list_ss [], 290 FULL_SIMP_TAC list_ss [] 291 ] 292 ]) 293 294val SWAP_ELEMENTS_SEM___MP = save_thm ("SWAP_ELEMENTS_SEM___MP", 295(SIMP_RULE std_ss [IMP_CONJ_THM, FORALL_AND_THM, 296 GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO] SWAP_ELEMENTS_SEM)); 297 298 299val SWAP_TO_POS_def = Define ` 300 (SWAP_TO_POS x y [] = []) /\ 301 (SWAP_TO_POS 0 0 (e::l) = (e::l)) /\ 302 (SWAP_TO_POS (SUC m) 0 (e::l) = e::l) /\ 303 (SWAP_TO_POS 0 (SUC n) (e::l) = (SAFE_DEL_EL n l) ++ e::(DELETE_ELEMENT n l))/\ 304 (SWAP_TO_POS (SUC m) (SUC n) (e::l) = e::SWAP_TO_POS m n l)` 305 306val SWAP_TO_POS_THM = store_thm ("SWAP_TO_POS_THM", 307 ``(!x y (l:'a list). y <= x ==> (SWAP_TO_POS x y l = l)) /\ 308 (!x y. SWAP_TO_POS x y [] = ([]:'a list)) /\ 309 (!x y e:'a. SWAP_TO_POS x y [e] = [e]) /\ 310 (!y e (l:'a list). SWAP_TO_POS y y l = l) /\ 311 (!y e (l:'a list). SWAP_TO_POS (SUC y) 0 l = l) /\ 312 (!y e (l:'a list). 313 (SWAP_TO_POS 0 (SUC y) (e::l) = (SAFE_DEL_EL y l) ++ e::DELETE_ELEMENT y l)) /\ 314 (!x y e (l:'a list). (SWAP_TO_POS (SUC x) (SUC y) (e::l) = e:: (SWAP_TO_POS x y l)))``, 315 316 MATCH_MP_TAC (prove (``(a /\ (a ==> b)) ==> (a /\ b)``, PROVE_TAC[])) THEN 317 CONJ_TAC THEN1 ( 318 Induct_on `x` THENL [ 319 Cases_on `l` THEN SIMP_TAC std_ss [SWAP_TO_POS_def], 320 321 Cases_on `y` THENL [ 322 Cases_on `l` THEN SIMP_TAC std_ss [SWAP_TO_POS_def], 323 Cases_on `l` THEN ASM_SIMP_TAC std_ss [SWAP_TO_POS_def] 324 ] 325 ] 326 ) THEN 327 STRIP_TAC THEN 328 REPEAT CONJ_TAC THENL [ 329 Cases_on `x` THEN Cases_on `y` THEN 330 SIMP_TAC std_ss [SWAP_TO_POS_def], 331 332 Cases_on `x` THEN Cases_on `y` THEN ( 333 SIMP_TAC list_ss [SWAP_TO_POS_def, DELETE_ELEMENT_THM, SAFE_DEL_EL_THM] 334 ) THEN 335 Cases_on `n` THEN Cases_on `n'` THEN 336 SIMP_TAC std_ss [SWAP_TO_POS_def], 337 338 ASM_SIMP_TAC arith_ss [], 339 340 ASM_SIMP_TAC arith_ss [], 341 342 SIMP_TAC std_ss [SWAP_TO_POS_def], 343 SIMP_TAC std_ss [SWAP_TO_POS_def] 344 ]) 345 346 347 348 349 350 351 352 353val SUC_RULE = CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV; 354 355 356val SWAP_ELEMENTS___REWRITE = SUC_RULE (CONJUNCT2 SWAP_ELEMENTS_THM); 357val REPLACE_ELEMENT___REWRITE = SUC_RULE (SIMP_RULE std_ss [FORALL_AND_THM] (GEN_ALL REPLACE_ELEMENT_def)) 358val SAFE_EL___REWRITE = SUC_RULE (SIMP_RULE std_ss [FORALL_AND_THM] (GEN_ALL SAFE_EL_def)) 359val SWAP_TO_POS___REWRITE = SUC_RULE (CONJUNCT2 SWAP_TO_POS_THM); 360val DELETE_ELEMENT___REWRITE = SUC_RULE (DELETE_ELEMENT_THM); 361val SAFE_DEL_EL___REWRITE = SUC_RULE (SAFE_DEL_EL_THM); 362 363val SWAP_REWRITES = save_thm ("SWAP_REWRITES", 364 LIST_CONJ [SWAP_ELEMENTS___REWRITE, REPLACE_ELEMENT___REWRITE, SAFE_EL___REWRITE, 365 SWAP_TO_POS___REWRITE, DELETE_ELEMENT___REWRITE, SAFE_DEL_EL___REWRITE]) 366 367 368 369val PERM___SAFE_REPLACE_EL = store_thm ("PERM___SAFE_REPLACE_EL", 370``!e n l. PERM ((SAFE_EL e n l) :: REPLACE_ELEMENT e n l) (e::l)``, 371 372Induct_on `n` THENL [ 373 Cases_on `l` THENL [ 374 SIMP_TAC std_ss [SAFE_EL_def, REPLACE_ELEMENT_def, PERM_REFL], 375 376 SIMP_TAC std_ss [SAFE_EL_def, REPLACE_ELEMENT_def, PERM_REFL, 377 PERM_SWAP_AT_FRONT] 378 ], 379 380 Cases_on `l` THENL [ 381 SIMP_TAC std_ss [SAFE_EL_def, REPLACE_ELEMENT_def, PERM_REFL], 382 383 SIMP_TAC std_ss [SAFE_EL_def, REPLACE_ELEMENT_def] THEN 384 GEN_TAC THEN 385 `!e1:'a e2 e3 e4 l l'. 386 PERM (e1::e2::l) (e3::e4::l') = 387 PERM (e2::e1::l) (e4::e3::l')` suffices_by (STRIP_TAC THEN 388 METIS_TAC[PERM_MONO] 389 ) THEN 390 POP_ASSUM (fn thm => ALL_TAC) THEN 391 METIS_TAC[PERM_MONO, PERM_TRANS, PERM_SWAP_AT_FRONT, PERM_SYM, PERM_REFL] 392 ] 393]) 394 395val PERM___SWAP_ELEMENTS = store_thm ("PERM___SWAP_ELEMENTS", 396``!m n l. PERM (SWAP_ELEMENTS m n l) l``, 397 398Induct_on `m` THENL [ 399 Cases_on `n` THENL [ 400 SIMP_TAC std_ss [SWAP_ELEMENTS_THM, PERM_REFL], 401 402 Cases_on `l` THENL [ 403 SIMP_TAC std_ss [SWAP_ELEMENTS_THM, PERM_REFL], 404 405 Cases_on `t` THENL [ 406 Cases_on `n'` THEN 407 SIMP_TAC std_ss [SWAP_ELEMENTS_THM, PERM_REFL, SAFE_EL_def, REPLACE_ELEMENT_def], 408 409 SIMP_TAC std_ss [SWAP_ELEMENTS_def, PERM___SAFE_REPLACE_EL] 410 ] 411 ] 412 ], 413 414 Cases_on `n` THENL [ 415 SIMP_TAC std_ss [SWAP_ELEMENTS_THM, PERM_REFL], 416 417 Cases_on `l` THENL [ 418 SIMP_TAC std_ss [SWAP_ELEMENTS_THM, PERM_REFL], 419 420 SIMP_TAC std_ss [SWAP_ELEMENTS_THM] THEN 421 METIS_TAC[PERM_MONO] 422 ] 423 ] 424]); 425 426 427val SWAP_ELEMENTS___LENGTH = store_thm ("SWAP_ELEMENTS___LENGTH", 428``!n m l. (LENGTH (SWAP_ELEMENTS n m l) = LENGTH l)``, 429METIS_TAC[PERM_LENGTH, PERM___SWAP_ELEMENTS]); 430 431val SWAP_ELEMENTS___EQ_NIL = store_thm ("SWAP_ELEMENTS___EQ_NIL", 432 ``!n m l. (SWAP_ELEMENTS n m l = []) = (l = [])``, 433 SIMP_TAC std_ss [GSYM LENGTH_NIL, SWAP_ELEMENTS___LENGTH]) 434 435 436val PERM___SWAP_TO_POS = store_thm ("PERM___SWAP_TO_POS", 437``!m n l. PERM (SWAP_TO_POS m n l) l``, 438 439Induct_on `m` THENL [ 440 Cases_on `n` THENL [ 441 SIMP_TAC std_ss [SWAP_TO_POS_THM, PERM_REFL], 442 443 Cases_on `l` THENL [ 444 SIMP_TAC std_ss [SWAP_TO_POS_THM, PERM_REFL], 445 446 SIMP_TAC std_ss [SWAP_TO_POS_THM, PERM_REFL] THEN 447 Q.SPEC_TAC (`t`, `l`) THEN 448 Q.SPEC_TAC (`h`, `h`) THEN 449 Q.SPEC_TAC (`n'`, `n`) THEN 450 Induct_on `n` THENL [ 451 Cases_on `l` THENL [ 452 SIMP_TAC list_ss [SAFE_DEL_EL_THM, DELETE_ELEMENT_THM, PERM_REFL], 453 454 SIMP_TAC list_ss [SAFE_DEL_EL_THM, DELETE_ELEMENT_THM, PERM_REFL, 455 PERM_SWAP_AT_FRONT] 456 ], 457 458 Cases_on `l` THENL [ 459 SIMP_TAC list_ss [SAFE_DEL_EL_THM, DELETE_ELEMENT_THM, PERM_REFL], 460 461 SIMP_TAC std_ss [SAFE_DEL_EL_THM, DELETE_ELEMENT_THM] THEN 462 GEN_TAC THEN 463 `PERM (SAFE_DEL_EL n t ++ h'::h::DELETE_ELEMENT n t) 464 (h'::(SAFE_DEL_EL n t ++ h::DELETE_ELEMENT n t))` by ( 465 `h'::h::DELETE_ELEMENT n t = 466 [h'] ++ (h::DELETE_ELEMENT n t)` by METIS_TAC [CONS_APPEND] THEN 467 `h'::SAFE_DEL_EL n t = [h']++SAFE_DEL_EL n t` by METIS_TAC [CONS_APPEND] THEN 468 ASM_SIMP_TAC std_ss [APPEND_ASSOC, GSYM APPEND] THEN 469 REPEAT (POP_ASSUM (fn thm => ALL_TAC)) THEN 470 METIS_TAC [PERM_APPEND, APPEND_ASSOC, PERM_CONG, PERM_REFL] 471 ) THEN 472 METIS_TAC[PERM_MONO, PERM_REFL, PERM_TRANS] 473 ] 474 ] 475 ] 476 ], 477 478 Cases_on `n` THENL [ 479 SIMP_TAC std_ss [SWAP_TO_POS_THM, PERM_REFL], 480 481 Cases_on `l` THENL [ 482 SIMP_TAC std_ss [SWAP_TO_POS_THM, PERM_REFL], 483 484 SIMP_TAC std_ss [SWAP_TO_POS_THM] THEN 485 METIS_TAC[PERM_MONO] 486 ] 487 ] 488]); 489 490 491 492val LIST_DS_ENTAILS___PERM_SWAP_ELEMENTS = store_thm ( 493"LIST_DS_ENTAILS___PERM_SWAP_ELEMENTS", 494``!n1 m1 n2 m2 n3 m3 n4 m4 n5 m5 n6 m6 c1 c2 pf sf pf' sf'. 495 496LIST_DS_ENTAILS (c1, c2) (pf, sf) (pf', sf') = 497LIST_DS_ENTAILS (SWAP_ELEMENTS n5 m5 c1, SWAP_ELEMENTS n6 m6 c2) ((SWAP_ELEMENTS n1 m1 pf), (SWAP_ELEMENTS n2 m2 sf)) 498 ((SWAP_ELEMENTS n3 m3 pf'), (SWAP_ELEMENTS n4 m4 sf'))``, 499 500REPEAT STRIP_TAC THEN 501MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 502METIS_TAC [PERM___SWAP_ELEMENTS, PERM_SYM]); 503 504 505 506val LIST_DS_ENTAILS___PERM_SWAP_TO_POS = store_thm ( 507"LIST_DS_ENTAILS___PERM_SWAP_TO_POS", 508``!n1 m1 n2 m2 n3 m3 n4 m4 n5 m5 n6 m6 c1 c2 pf sf pf' sf'. 509 510LIST_DS_ENTAILS (c1,c2) (pf, sf) (pf', sf') = 511LIST_DS_ENTAILS (SWAP_TO_POS n5 m5 c1, SWAP_TO_POS n6 m6 c2) ((SWAP_TO_POS n1 m1 pf), (SWAP_TO_POS n2 m2 sf)) 512 ((SWAP_TO_POS n3 m3 pf'), (SWAP_TO_POS n4 m4 sf'))``, 513 514REPEAT STRIP_TAC THEN 515MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 516METIS_TAC [PERM___SWAP_TO_POS, PERM_SYM]); 517 518 519 520val PF_TURN_EQ_def = Define ` 521 (PF_TURN_EQ (pf_equal e1 e2) = (pf_equal e2 e1)) /\ 522 (PF_TURN_EQ (pf_unequal e1 e2) = (pf_unequal e2 e1)) /\ 523 (PF_TURN_EQ x = x)` 524 525 526val PF_TURN_EQ___SEM = store_thm ("PF_TURN_EQ___SEM", 527 ``!s pf. PF_SEM s (PF_TURN_EQ pf) = PF_SEM s pf``, 528 529 Induct_on `pf` THEN ( 530 SIMP_TAC std_ss [PF_TURN_EQ_def, PF_SEM_def, DS_EXPRESSION_EQUAL_def] THEN 531 METIS_TAC[] 532 ) 533); 534 535 536 537val SAFE_MAP_def = Define ` 538 (SAFE_MAP x f g [] = []) /\ 539 (SAFE_MAP T [] g l = MAP g l) /\ 540 (SAFE_MAP F [] g l = l) /\ 541 (SAFE_MAP x (T::f) g (e::l) = (g e)::(SAFE_MAP x f g l)) /\ 542 (SAFE_MAP x (F::f) g (e::l) = e::(SAFE_MAP x f g l))` 543 544val SAFE_MAP_THM = store_thm ("SAFE_MAP_THM", 545``(SAFE_MAP x f g [] = []) /\ 546(SAFE_MAP T [] g l = MAP g l) /\ 547(SAFE_MAP F [] g l = l) /\ 548(SAFE_MAP x (T::f) g (e::l) = (g e)::(SAFE_MAP x f g l)) /\ 549(SAFE_MAP x (F::f) g (e::l) = e::(SAFE_MAP x f g l))``, 550 551Cases_on `l` THEN SIMP_TAC list_ss [SAFE_MAP_def]) 552 553 554val LIST_PF_SEM___PF_TURN_EQ = store_thm ("LIST_PF_SEM___PF_TURN_EQ", 555 ``!f s pfL. LIST_PF_SEM s (SAFE_MAP F f PF_TURN_EQ pfL) = 556 LIST_PF_SEM s pfL``, 557 558 Induct_on `pfL` THENL [ 559 SIMP_TAC list_ss [SAFE_MAP_THM], 560 561 Cases_on `f` THENL [ 562 SIMP_TAC std_ss [SAFE_MAP_THM], 563 564 Cases_on `h` THEN ( 565 ASM_SIMP_TAC list_ss [LIST_PF_SEM_THM, PF_TURN_EQ___SEM, SAFE_MAP_THM] 566 ) 567 ] 568 ]) 569 570 571val LIST_DS_ENTAILS___PF_TURN_EQ = store_thm ("LIST_DS_ENTAILS___PF_TURN_EQ", 572``!f1 f2 C pf sf pf' sf'. 573 LIST_DS_ENTAILS C (pf, sf) (pf', sf') = 574 LIST_DS_ENTAILS C (SAFE_MAP F f1 PF_TURN_EQ pf, sf) (SAFE_MAP F f2 PF_TURN_EQ pf', sf')``, 575 576 SIMP_TAC std_ss [LIST_DS_ENTAILS_def, LIST_DS_SEM_def, LIST_PF_SEM___PF_TURN_EQ]) 577 578 579 580 581 582 583 584val SAFE_BUTFIRSTN_def = Define ` 585 (SAFE_BUTFIRSTN 0 l = l) /\ 586 (SAFE_BUTFIRSTN n [] = []) /\ 587 (SAFE_BUTFIRSTN (SUC n) (e::l) = SAFE_BUTFIRSTN n l)`; 588 589 590 591val SAFE_BUTFIRSTN_THM = store_thm ("SAFE_BUTFIRSTN_THM", 592 ``(SAFE_BUTFIRSTN 0 l = l) /\ 593 (SAFE_BUTFIRSTN n [] = []) /\ 594 (SAFE_BUTFIRSTN (SUC n) (e::l) = SAFE_BUTFIRSTN n l)``, 595 596 Cases_on `n` THEN SIMP_TAC std_ss [SAFE_BUTFIRSTN_def]) 597 598 599val SAFE_BUTFIRSTN___REWRITE = save_thm ("SAFE_BUTFIRSTN___REWRITE", 600SUC_RULE (SIMP_RULE std_ss [FORALL_AND_THM] (GEN_ALL SAFE_BUTFIRSTN_THM))); 601 602 603val POS_FILTER_def = Define ` 604 (POS_FILTER [] p l = l) /\ 605 (POS_FILTER f p [] = []) /\ 606 (POS_FILTER (T::f) p (e::l) = let (l' = POS_FILTER f p l) in if p e then l' else (e::l')) /\ 607 (POS_FILTER (F::f) p (e::l) = e::(POS_FILTER f p l))` 608 609 610val POS_FILTER_THM = store_thm ("POS_FILTER_THM", 611`` (POS_FILTER [] p l = l) /\ 612 (POS_FILTER f p [] = []) /\ 613 (POS_FILTER (T::f) p (e::l) = let (l' = POS_FILTER f p l) in if p e then l' else (e::l')) /\ 614 (POS_FILTER (F::f) p (e::l) = e::(POS_FILTER f p l))``, 615 616Cases_on `f` THEN REWRITE_TAC [POS_FILTER_def]) 617 618 619val MEM_POS_FILTER = store_thm ("MEM_POS_FILTER", 620 ``!x f p l. ((MEM x l) /\ ~(p x)) ==> MEM x (POS_FILTER f p l)``, 621 622 Induct_on `l` THENL [ 623 SIMP_TAC std_ss [POS_FILTER_THM], 624 625 Cases_on `f` THEN SIMP_TAC list_ss [POS_FILTER_THM] THEN 626 Cases_on `h` THEN ( 627 ASM_SIMP_TAC list_ss [POS_FILTER_THM, LET_THM, RIGHT_AND_OVER_OR, DISJ_IMP_THM, FORALL_AND_THM, 628 COND_RATOR, COND_RAND] 629 ) 630 ]) 631 632 633val MEM_POS_FILTER_2 = store_thm ("MEM_POS_FILTER_2", 634 ``!x f p l. MEM x (POS_FILTER f p l) ==> (MEM x l)``, 635 636 Induct_on `l` THENL [ 637 SIMP_TAC std_ss [POS_FILTER_THM], 638 639 Cases_on `f` THEN SIMP_TAC list_ss [POS_FILTER_THM] THEN 640 Cases_on `h` THEN ( 641 ASM_SIMP_TAC list_ss [POS_FILTER_THM, LET_THM, 642 COND_RATOR, COND_RAND] THEN 643 METIS_TAC[] 644 ) 645 ]) 646 647 648val SAFE_FILTER_def = Define ` 649 (SAFE_FILTER T [] l = l) /\ 650 (SAFE_FILTER F [] l = []) /\ 651 (SAFE_FILTER x f [] = []) /\ 652 (SAFE_FILTER x (T::f) (e::l) = e::SAFE_FILTER x f l) /\ 653 (SAFE_FILTER x (F::f) (e::l) = SAFE_FILTER x f l)`; 654 655 656val SAFE_FILTER_THM = store_thm ("SAFE_FILTER_THM", 657`` (SAFE_FILTER T [] l = l) /\ 658 (SAFE_FILTER F [] l = []) /\ 659 (SAFE_FILTER x f [] = []) /\ 660 (SAFE_FILTER x (T::f) (e::l) = e::SAFE_FILTER x f l) /\ 661 (SAFE_FILTER x (F::f) (e::l) = SAFE_FILTER x f l)``, 662 663 Cases_on `x` THEN 664 SIMP_TAC std_ss [SAFE_FILTER_def] THEN 665 Cases_on `f` THEN 666 SIMP_TAC std_ss [SAFE_FILTER_def]) 667 668val SAFE_FILTER_APPEND = store_thm ("SAFE_FILTER_APPEND", 669 ``!x f l1 l2. SAFE_FILTER x f (l1 ++ l2) = 670 SAFE_FILTER x f l1 ++ (SAFE_FILTER x (SAFE_BUTFIRSTN (LENGTH l1) f) l2)``, 671 672 Induct_on `l1` THENL [ 673 SIMP_TAC list_ss [SAFE_BUTFIRSTN_THM, SAFE_FILTER_THM], 674 675 Cases_on `f` THENL [ 676 Cases_on `x` THENL [ 677 SIMP_TAC list_ss [SAFE_FILTER_THM, SAFE_BUTFIRSTN_THM], 678 SIMP_TAC list_ss [SAFE_FILTER_THM, SAFE_BUTFIRSTN_THM] 679 ], 680 681 Cases_on `h` THEN ( 682 ASM_SIMP_TAC list_ss [SAFE_FILTER_THM, SAFE_BUTFIRSTN_THM] 683 ) 684 ] 685 ]) 686 687val MEM_SAFE_FILTER = store_thm ("MEM_SAFE_FILTER", 688 ``!x f l e. MEM e (SAFE_FILTER x f l) ==> MEM e l``, 689 690 Induct_on `f` THENL [ 691 Cases_on `x` THEN 692 SIMP_TAC list_ss [SAFE_FILTER_THM], 693 694 Cases_on `l` THEN ( 695 SIMP_TAC list_ss [SAFE_FILTER_THM] 696 ) THEN 697 Cases_on `h'` THEN ( 698 SIMP_TAC list_ss [SAFE_FILTER_THM] THEN 699 METIS_TAC[] 700 ) 701 ]); 702 703 704 705val LIST_PF_SEM___SAFE_FILTER = store_thm ("LIST_PF_SEM___SAFE_FILTER", 706``!s x f pfL. LIST_PF_SEM s pfL ==> LIST_PF_SEM s (SAFE_FILTER x f pfL)``, 707 708Induct_on `pfL` THENL [ 709 SIMP_TAC std_ss [SAFE_FILTER_THM], 710 711 Cases_on `f` THENL [ 712 Cases_on `x` THEN 713 SIMP_TAC std_ss [SAFE_FILTER_THM, LIST_PF_SEM_THM], 714 715 Cases_on `h` THENL [ 716 ASM_SIMP_TAC std_ss [SAFE_FILTER_THM, LIST_PF_SEM_THM], 717 ASM_SIMP_TAC std_ss [SAFE_FILTER_THM, LIST_PF_SEM_THM] 718 ] 719 ] 720]); 721 722 723 724val LIST_DS_ENTAILS___CLEAN_PF = store_thm ("LIST_DS_ENTAILS___CLEAN_PF", 725``!x f C pf sf pf' sf'. 726LIST_DS_ENTAILS C (SAFE_FILTER x f pf, sf) (pf', sf') ==> 727LIST_DS_ENTAILS C (pf, sf) (pf', sf')``, 728 729SIMP_TAC std_ss [LIST_DS_ENTAILS_def, LIST_DS_SEM_def] THEN 730METIS_TAC[LIST_PF_SEM___SAFE_FILTER]) 731 732 733 734 735val SWAP_TO_POS___DELETE_ELEMENT = store_thm ("SWAP_TO_POS___DELETE_ELEMENT", 736 737 ``!n l. n < LENGTH l ==> 738 ((SWAP_TO_POS 0 n l) = (EL n l)::(DELETE_ELEMENT n l))``, 739 740 Cases_on `l` THEN Cases_on `n` THEN 741 SIMP_TAC list_ss [SWAP_TO_POS_THM, DELETE_ELEMENT_THM, SAFE_DEL_EL_SEM]) 742 743val SAFE_DEL_EL___EQ = store_thm ("SAFE_DEL_EL___EQ", 744 ``(!n (l:'a list). (SAFE_DEL_EL n l = []) = (~(n < LENGTH l))) /\ 745 (!n (l:'a list) e. (SAFE_DEL_EL n l = [e]) = ((n < LENGTH l) /\ (EL n l = e))) /\ 746 (!n (l:'a list) e1 e2 eL. ~(SAFE_DEL_EL n l = e1::e2::eL))``, 747 748SIMP_TAC std_ss [GSYM FORALL_AND_THM] THEN 749REPEAT GEN_TAC THEN 750Cases_on `n < LENGTH l` THEN ( 751 ASM_SIMP_TAC list_ss [SAFE_DEL_EL_SEM] 752)) 753 754 755 756val INFERENCE_SUBSTITUTION___EVAL1 = store_thm ("INFERENCE_SUBSTITUTION___EVAL1", 757``!n e v c1 c2 pfL sfL pfL' sfL'. 758 (SAFE_DEL_EL n pfL = [pf_equal (dse_var v) e]) ==> 759 760 ( 761 LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') = 762 LIST_DS_ENTAILS (MAP (DS_VAR_SUBST v e) c1, MAP (\x. (DS_VAR_SUBST v e (FST x), DS_VAR_SUBST v e (SND x))) c2) 763 (MAP (PF_SUBST v e) (DELETE_ELEMENT n pfL),MAP (SF_SUBST v e) sfL) 764 (MAP (PF_SUBST v e) pfL',MAP (SF_SUBST v e) sfL'))``, 765 766SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 767REPEAT STRIP_TAC THEN 768`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 769 LIST_DS_ENTAILS (c1, c2) (SWAP_TO_POS 0 n pfL,sfL) (pfL',sfL')` by ( 770 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 771 SIMP_TAC std_ss [PERM_REFL] THEN 772 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 773) THEN 774FULL_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT, 775 GSYM INFERENCE_SUBSTITUTION]) 776 777 778 779val INFERENCE_SUBSTITUTION___EVAL2 = store_thm ("INFERENCE_SUBSTITUTION___EVAL2", 780``!n e v c1 c2 pfL sfL pfL' sfL'. 781 (SAFE_DEL_EL n pfL = [pf_equal e (dse_var v)]) ==> 782 783 ( 784 LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') = 785 LIST_DS_ENTAILS (MAP (DS_VAR_SUBST v e) c1, MAP (\x. (DS_VAR_SUBST v e (FST x), DS_VAR_SUBST v e (SND x))) c2) 786 (MAP (PF_SUBST v e) (DELETE_ELEMENT n pfL),MAP (SF_SUBST v e) sfL) 787 (MAP (PF_SUBST v e) pfL',MAP (SF_SUBST v e) sfL'))``, 788 789 790SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 791REPEAT STRIP_TAC THEN 792`LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') = 793 LIST_DS_ENTAILS (c1,c2) (SWAP_TO_POS 0 n pfL,sfL) (pfL',sfL')` by ( 794 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 795 SIMP_TAC std_ss [PERM_REFL] THEN 796 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 797) THEN 798`LIST_DS_ENTAILS (c1,c2) (pf_equal e (dse_var v)::DELETE_ELEMENT n pfL,sfL) (pfL',sfL') = 799 LIST_DS_ENTAILS (c1,c2) (pf_equal (dse_var v) e::DELETE_ELEMENT n pfL,sfL) (pfL',sfL')` by ( 800 SIMP_TAC std_ss [LIST_DS_ENTAILS_def, LIST_DS_SEM_EVAL, DS_EXPRESSION_EQUAL_def] THEN 801 METIS_TAC[] 802) THEN 803FULL_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT, 804 GSYM INFERENCE_SUBSTITUTION]); 805 806 807 808 809 810val PF_TRIVIAL_FILTER_PRED_def = Define 811 `(PF_TRIVIAL_FILTER_PRED pf_true = T) /\ 812 (PF_TRIVIAL_FILTER_PRED (pf_unequal e1 e2) = F) /\ 813 (PF_TRIVIAL_FILTER_PRED (pf_equal e1 e2) = (e1 = e2)) /\ 814 (PF_TRIVIAL_FILTER_PRED (pf_and pf1 pf2) = 815 PF_TRIVIAL_FILTER_PRED pf1 /\ PF_TRIVIAL_FILTER_PRED pf2)` 816 817 818val PF_TRIVIAL_FILTER_PRED_SEM = store_thm ("PF_TRIVIAL_FILTER_PRED_SEM", 819 820 ``!pf. PF_TRIVIAL_FILTER_PRED pf ==> !s. PF_SEM s pf``, 821 822Induct_on `pf` THENL [ 823 REWRITE_TAC [PF_SEM_def], 824 SIMP_TAC std_ss [PF_SEM_def, PF_TRIVIAL_FILTER_PRED_def, DS_EXPRESSION_EQUAL_def], 825 SIMP_TAC std_ss [PF_TRIVIAL_FILTER_PRED_def], 826 ASM_SIMP_TAC std_ss [PF_SEM_def, PF_TRIVIAL_FILTER_PRED_def] 827]); 828 829 830 831val LIST_PF_SEM___TRIVIAL_FILTER_THM = store_thm ("LIST_PF_SEM___TRIVIAL_FILTER_THM", 832 ``!s f pfL. 833 LIST_PF_SEM s (POS_FILTER f PF_TRIVIAL_FILTER_PRED pfL) = 834 LIST_PF_SEM s pfL``, 835 836Induct_on `pfL` THENL [ 837 REWRITE_TAC [POS_FILTER_THM], 838 839 Cases_on `f` THEN1 REWRITE_TAC [POS_FILTER_THM] THEN 840 Cases_on `h` THENL [ 841 ASM_SIMP_TAC std_ss [POS_FILTER_THM, LET_THM, COND_RATOR, COND_RAND, 842 LIST_PF_SEM_THM, PF_TRIVIAL_FILTER_PRED_SEM], 843 844 ASM_SIMP_TAC std_ss [POS_FILTER_THM, LIST_PF_SEM_THM] 845 ] 846]); 847 848 849 850 851 852 853val SF_TRIVIAL_FILTER_PRED_def = Define 854 `(SF_TRIVIAL_FILTER_PRED sf_emp = T) /\ 855 (SF_TRIVIAL_FILTER_PRED (sf_points_to e a) = F) /\ 856 (SF_TRIVIAL_FILTER_PRED (sf_tree fL es e) = (es = e)) /\ 857 (SF_TRIVIAL_FILTER_PRED (sf_star sf1 sf2) = 858 SF_TRIVIAL_FILTER_PRED sf1 /\ SF_TRIVIAL_FILTER_PRED sf2)` 859 860 861val SF_TRIVIAL_FILTER_PRED_THM = store_thm ("SF_TRIVIAL_FILTER_PRED_THM", 862 ``(SF_TRIVIAL_FILTER_PRED sf_emp = T) /\ 863 (SF_TRIVIAL_FILTER_PRED (sf_points_to e a) = F) /\ 864 (SF_TRIVIAL_FILTER_PRED (sf_tree fL es e) = (es = e)) /\ 865 (SF_TRIVIAL_FILTER_PRED (sf_ls f e1 e2) = (e1 = e2)) /\ 866 (SF_TRIVIAL_FILTER_PRED (sf_bin_tree (f1,f2) e) = (e = dse_nil)) /\ 867 (SF_TRIVIAL_FILTER_PRED (sf_star sf1 sf2) = 868 SF_TRIVIAL_FILTER_PRED sf1 /\ SF_TRIVIAL_FILTER_PRED sf2)``, 869 870SIMP_TAC std_ss [SF_TRIVIAL_FILTER_PRED_def, sf_ls_def, sf_bin_tree_def] THEN 871METIS_TAC[]); 872 873 874 875 876val SF_TRIVIAL_FILTER_PRED_SEM = store_thm ("SF_TRIVIAL_FILTER_PRED_SEM", 877 878 ``!sf. SF_TRIVIAL_FILTER_PRED sf ==> (!s h. SF_SEM s h sf = (h = FEMPTY))``, 879 880Induct_on `sf` THENL [ 881 REWRITE_TAC [SF_SEM_def], 882 SIMP_TAC std_ss [SF_TRIVIAL_FILTER_PRED_def], 883 SIMP_TAC std_ss [SF_TRIVIAL_FILTER_PRED_def, SF_SEM___sf_tree_THM, DS_EXPRESSION_EQUAL_def], 884 885 ASM_SIMP_TAC std_ss [SF_SEM_def, SF_TRIVIAL_FILTER_PRED_def, FUNION_FEMPTY_1, FDOM_FEMPTY, 886 DISJOINT_EMPTY] 887]); 888 889 890 891 892 893val LIST_SF_SEM___TRIVIAL_FILTER_THM = store_thm ("LIST_SF_SEM___TRIVIAL_FILTER_THM", 894 ``!s h f sfL. 895 LIST_SF_SEM s h (POS_FILTER f SF_TRIVIAL_FILTER_PRED sfL) = 896 LIST_SF_SEM s h sfL``, 897 898Induct_on `sfL` THENL [ 899 REWRITE_TAC [POS_FILTER_THM], 900 901 Cases_on `f` THEN1 REWRITE_TAC [POS_FILTER_THM] THEN 902 Cases_on `h` THENL [ 903 ASM_SIMP_TAC std_ss [POS_FILTER_THM, LET_THM, COND_RATOR, COND_RAND, 904 LIST_SF_SEM_THM, SF_TRIVIAL_FILTER_PRED_SEM, FUNION_FEMPTY_1, 905 DISJOINT_EMPTY, FDOM_FEMPTY], 906 907 ASM_SIMP_TAC std_ss [POS_FILTER_THM, LIST_SF_SEM_THM] 908 ] 909]); 910 911 912val HEAP_DISTINCT___TRIVIAL_FILTER_THM = store_thm ("HEAP_DISTINCT___TRIVIAL_FILTER_THM", 913 ``!s h f c1 c2. 914 (HEAP_DISTINCT s h c1 (POS_FILTER f (\x. (FST x = SND x)) c2) = 915 HEAP_DISTINCT s h c1 c2)``, 916 917 918Induct_on `c2` THENL [ 919 SIMP_TAC list_ss [POS_FILTER_THM], 920 921 REPEAT GEN_TAC THEN 922 Cases_on `h` THEN 923 Cases_on `f` THEN1 REWRITE_TAC [POS_FILTER_THM] THEN 924 Cases_on `(POS_FILTER (h::t) (\x. FST x = SND x) ((q,r)::c2)) = 925 ((q,r)::(POS_FILTER t (\x. FST x = SND x) c2))` THEN1 ( 926 ASM_SIMP_TAC std_ss [HEAP_DISTINCT___IND_DEF] THEN 927 EQ_TAC THEN STRIP_TAC THEN 928 ASM_SIMP_TAC std_ss [] THENL [ 929 DISJ2_TAC THEN 930 REPEAT STRIP_TAC THEN 931 Cases_on `DS_EXPRESSION_EQUAL s e1' e2'` THEN ASM_REWRITE_TAC[] THEN 932 `MEM (e1',e2') (POS_FILTER t (\x. FST x = SND x) c2)` by ( 933 MATCH_MP_TAC MEM_POS_FILTER THEN 934 FULL_SIMP_TAC std_ss [DS_EXPRESSION_EQUAL_def] THEN 935 METIS_TAC[] 936 ) THEN 937 METIS_TAC[], 938 939 940 DISJ2_TAC THEN 941 REPEAT STRIP_TAC THEN 942 `MEM (e1',e2') c2` by METIS_TAC[MEM_POS_FILTER_2] THEN 943 METIS_TAC[] 944 ] 945 ) THEN 946 Cases_on `h` THENL [ 947 ASM_SIMP_TAC std_ss [POS_FILTER_THM, LET_THM] THEN 948 Cases_on `q = r` THENL [ 949 ASM_SIMP_TAC std_ss [HEAP_DISTINCT___EQUAL], 950 FULL_SIMP_TAC std_ss [POS_FILTER_THM, LET_THM] 951 ], 952 953 FULL_SIMP_TAC std_ss [POS_FILTER_THM] 954 ] 955]); 956 957 958 959 960val INFERENCE_TRIVIAL_FILTER = store_thm ("INFERENCE_TRIVIAL_FILTER", 961``!f1 f2 f3 f4 f5 c1 c2 pfL sfL pfL' sfL'. 962 LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 963 LIST_DS_ENTAILS (c1, (POS_FILTER f1 (\x. (FST x = SND x)) c2)) (POS_FILTER f2 PF_TRIVIAL_FILTER_PRED pfL, POS_FILTER f3 SF_TRIVIAL_FILTER_PRED sfL) (POS_FILTER f4 PF_TRIVIAL_FILTER_PRED pfL',POS_FILTER f5 SF_TRIVIAL_FILTER_PRED sfL')``, 964 965SIMP_TAC std_ss [LIST_DS_ENTAILS_def, LIST_DS_SEM_def, LIST_PF_SEM___TRIVIAL_FILTER_THM, 966 LIST_SF_SEM___TRIVIAL_FILTER_THM, HEAP_DISTINCT___TRIVIAL_FILTER_THM]); 967 968 969 970val INFERENCE_INCONSISTENT_UNEQUAL___EVAL = store_thm ("INFERENCE_INCONSISTENT_UNEQUAL___EVAL", 971 ``!n e c1 c2 pfL sfL pfL' sfL'. 972 (SAFE_DEL_EL n pfL = [pf_unequal e e]) ==> 973 LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL')``, 974 975 976SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 977REPEAT STRIP_TAC THEN 978`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 979 LIST_DS_ENTAILS (c1, c2) (SWAP_TO_POS 0 n pfL,sfL) (pfL',sfL')` by ( 980 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 981 SIMP_TAC std_ss [PERM_REFL] THEN 982 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 983) THEN 984ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT, INFERENCE_INCONSISTENT]); 985 986 987 988 989val INFERENCE_INCONSISTENT___NIL_POINTS_TO___EVAL = store_thm ("INFERENCE_INCONSISTENT___NIL_POINTS_TO___EVAL", 990 ``!n a c1 c2 pfL sfL pfL' sfL'. 991 (SAFE_DEL_EL n sfL = [sf_points_to dse_nil a]) ==> 992 LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL')``, 993 994 995SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 996REPEAT STRIP_TAC THEN 997`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 998 LIST_DS_ENTAILS (c1, c2) (pfL,SWAP_TO_POS 0 n sfL) (pfL',sfL')` by ( 999 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 1000 SIMP_TAC std_ss [PERM_REFL] THEN 1001 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 1002) THEN 1003ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT, INFERENCE_INCONSISTENT___NIL_POINTS_TO]) 1004 1005 1006 1007val INFERENCE_INCONSISTENT___precondition_POINTS_TO___EVAL = store_thm ("INFERENCE_INCONSISTENT___precondition_POINTS_TO___EVAL", 1008 ``!m n e a c1 c2 pfL sfL pfL' sfL'. 1009 ((SAFE_DEL_EL n sfL = [sf_points_to e a]) /\ 1010 (SAFE_DEL_EL m c1 = [e])) ==> 1011 LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL')``, 1012 1013 1014SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 1015REPEAT STRIP_TAC THEN 1016`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 1017 LIST_DS_ENTAILS (c1, c2) (pfL,SWAP_TO_POS 0 n sfL) (pfL',sfL')` by ( 1018 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 1019 SIMP_TAC std_ss [PERM_REFL] THEN 1020 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 1021) THEN 1022ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 1023MATCH_MP_TAC INFERENCE_INCONSISTENT___precondition_POINTS_TO THEN 1024ASM_SIMP_TAC std_ss [EL_IS_EL] 1025); 1026 1027 1028val INFERENCE_INCONSISTENT___precondition_BIN_TREE___EVAL = store_thm ("INFERENCE_INCONSISTENT___precondition_BIN_TREE___EVAL", 1029 ``!m n e fL c1 c2 pfL sfL pfL' sfL'. 1030 ((SAFE_DEL_EL n sfL = [sf_bin_tree fL e]) /\ 1031 (SAFE_DEL_EL m c1 = [e])) ==> 1032 LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL')``, 1033 1034 1035Cases_on `fL` THEN 1036SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 1037REPEAT STRIP_TAC THEN 1038`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 1039 LIST_DS_ENTAILS (c1, c2) (pfL,SWAP_TO_POS 0 n sfL) (pfL',sfL')` by ( 1040 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 1041 SIMP_TAC std_ss [PERM_REFL] THEN 1042 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 1043) THEN 1044ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 1045MATCH_MP_TAC INFERENCE_INCONSISTENT___precondition_BIN_TREE THEN 1046ASM_SIMP_TAC std_ss [EL_IS_EL]); 1047 1048 1049val INFERENCE_INCONSISTENT___precondition_dse_nil = store_thm ("INFERENCE_INCONSISTENT___precondition_dse_nil", 1050 ``!n c1 c2 pfL sfL pfL' sfL'. 1051 (SAFE_DEL_EL n c1 = [dse_nil]) ==> 1052 LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL')``, 1053 1054SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 1055REPEAT STRIP_TAC THEN 1056`MEM dse_nil c1` by METIS_TAC [EL_IS_EL] THEN 1057ASM_SIMP_TAC std_ss [LIST_DS_ENTAILS_def] THEN 1058METIS_TAC[HEAP_DISTINCT___dse_nil, DS_EXPRESSION_EQUAL_def]); 1059 1060 1061 1062val INFERENCE_INCONSISTENT___precondition_distinct = store_thm ("INFERENCE_INCONSISTENT___precondition_distinct", 1063 ``!n m e c1 c2 pfL sfL pfL' sfL'. 1064 ((SAFE_DEL_EL n c1 = [e]) /\ (SAFE_DEL_EL m c1 = [e]) /\ ~(n = m)) ==> 1065 LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL')``, 1066 1067SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 1068REPEAT STRIP_TAC THEN 1069ASM_SIMP_TAC std_ss [LIST_DS_ENTAILS_def] THEN 1070METIS_TAC[HEAP_DISTINCT___NOT_ALL_DISTINCT]); 1071 1072 1073 1074val _ = Hol_datatype `hypothesis_rule_cases = 1075 hyp_keep 1076 | hyp_c_dse_nil of bool => num 1077 | hyp_c_unequal of num => num 1078 | hyp_in_precond of bool => num 1079 | hyp_in_self of bool => num` 1080 1081 1082val HYPOTHESIS_RULE_COND_def = Define ` 1083 (HYPOTHESIS_RULE_COND cL pfL1 pfL2 n h hyp_keep = F) /\ 1084 1085 (HYPOTHESIS_RULE_COND cL pfL1 pfL2 n (pf_unequal e1 e2) (hyp_c_dse_nil F m) = 1086 ((e1 = dse_nil) /\ (SAFE_DEL_EL m cL = [e2]))) /\ 1087 (HYPOTHESIS_RULE_COND cL pfL1 pfL2 n (pf_unequal e1 e2) (hyp_c_dse_nil T m) = 1088 ((e2 = dse_nil) /\ (SAFE_DEL_EL m cL = [e1]))) /\ 1089 (HYPOTHESIS_RULE_COND cL pfL1 pfL2 n pf (hyp_c_dse_nil b m) = F) /\ 1090 1091 (HYPOTHESIS_RULE_COND cL pfL1 pfL2 n (pf_unequal e1 e2) (hyp_c_unequal m1 m2) = 1092 (~(m1 = m2) /\ (SAFE_DEL_EL m1 cL = [e1]) /\ (SAFE_DEL_EL m2 cL = [e2]))) /\ 1093 (HYPOTHESIS_RULE_COND cL pfL1 pfL2 n pf (hyp_c_unequal m1 m2) = F) /\ 1094 1095 1096 (HYPOTHESIS_RULE_COND cL pfL1 pfL2 n h (hyp_in_precond F m) = 1097 (SAFE_DEL_EL m pfL1 = [h])) /\ 1098 (HYPOTHESIS_RULE_COND cL pfL1 pfL2 n h (hyp_in_precond T m) = 1099 (SAFE_DEL_EL m pfL1 = [PF_TURN_EQ h])) /\ 1100 1101 (HYPOTHESIS_RULE_COND cL pfL1 pfL2 n h (hyp_in_self F m) = 1102 ((m < n) /\ (SAFE_DEL_EL m pfL2 = [h]))) /\ 1103 (HYPOTHESIS_RULE_COND cL pfL1 pfL2 n h (hyp_in_self T m) = 1104 ((m < n) /\ (SAFE_DEL_EL m pfL2 = [PF_TURN_EQ h])))` 1105 1106 1107 1108val HYPOTHESIS_RULE_COND_THM = store_thm ("HYPOTHESIS_RULE_COND_THM", 1109`` (HYPOTHESIS_RULE_COND cL pfL1 pfL2 n pf hyp_keep = F) /\ 1110 1111 (HYPOTHESIS_RULE_COND cL pfL1 pfL2 n (pf_unequal e1 e2) (hyp_c_dse_nil F m) = 1112 ((e1 = dse_nil) /\ (SAFE_DEL_EL m cL = [e2]))) /\ 1113 (HYPOTHESIS_RULE_COND cL pfL1 pfL2 n (pf_unequal e1 e2) (hyp_c_dse_nil T m) = 1114 ((e2 = dse_nil) /\ (SAFE_DEL_EL m cL = [e1]))) /\ 1115 1116 (HYPOTHESIS_RULE_COND cL pfL1 pfL2 n (pf_unequal e1 e2) (hyp_c_unequal m1 m2) = 1117 (~(m1 = m2) /\(SAFE_DEL_EL m1 cL = [e1]) /\ (SAFE_DEL_EL m2 cL = [e2]))) /\ 1118 1119 (HYPOTHESIS_RULE_COND cL pfL1 pfL2 n pf (hyp_in_precond b m) = 1120 (SAFE_DEL_EL m pfL1 = [if b then PF_TURN_EQ pf else pf])) /\ 1121 1122 (HYPOTHESIS_RULE_COND cL pfL1 pfL2 n pf (hyp_in_self b m) = 1123 ((m < n) /\ (SAFE_DEL_EL m pfL2 = [if b then PF_TURN_EQ pf else pf])))``, 1124 1125Cases_on `pf` THEN Cases_on `b` THEN SIMP_TAC std_ss [HYPOTHESIS_RULE_COND_def]); 1126 1127 1128val HYPOTHESIS_RULE_COND___SEM = store_thm ("HYPOTHESIS_RULE_COND___SEM", 1129``!s h n cL pfL1 pfL2 c2 hyp_cond pf. 1130 (HEAP_DISTINCT s h cL c2 /\ 1131 LIST_PF_SEM s pfL1 /\ LIST_PF_SEM s pfL2 /\ n <= LENGTH pfL2 /\ 1132 HYPOTHESIS_RULE_COND cL pfL1 (pfL2++l) n pf hyp_cond) ==> 1133 (PF_SEM s pf)``, 1134 1135Cases_on `hyp_cond` THENL [ 1136 SIMP_TAC std_ss [HYPOTHESIS_RULE_COND_THM], 1137 1138 Cases_on `pf` THEN ( 1139 SIMP_TAC std_ss [HYPOTHESIS_RULE_COND_def] 1140 ) THEN 1141 Cases_on `b` THEN ( 1142 SIMP_TAC std_ss [HYPOTHESIS_RULE_COND_def, SAFE_DEL_EL___EQ, PF_SEM_def] THEN 1143 METIS_TAC[HEAP_DISTINCT___dse_nil, DS_EXPRESSION_EQUAL_def, MEM_EL] 1144 ), 1145 1146 Cases_on `pf` THEN 1147 SIMP_TAC list_ss [HYPOTHESIS_RULE_COND_def, SAFE_DEL_EL___EQ] THEN 1148 REPEAT STRIP_TAC THEN 1149 FULL_SIMP_TAC list_ss [HEAP_DISTINCT_def, EL_ALL_DISTINCT_EQ, EL_MAP] THEN 1150 `~(DS_EXPRESSION_EVAL_VALUE s (EL n cL) = DS_EXPRESSION_EVAL_VALUE s (EL n0 cL))` by METIS_TAC[] THEN 1151 `~IS_DSV_NIL (DS_EXPRESSION_EVAL s (EL n cL)) /\ ~IS_DSV_NIL (DS_EXPRESSION_EVAL s (EL n0 cL))` by METIS_TAC[MEM_EL] THEN 1152 FULL_SIMP_TAC std_ss [DS_EXPRESSION_EVAL_VALUE_def, NOT_IS_DSV_NIL_THM] THEN 1153 FULL_SIMP_TAC std_ss [GET_DSV_VALUE_def, PF_SEM_def, DS_EXPRESSION_EQUAL_def] THEN 1154 METIS_TAC[], 1155 1156 1157 SIMP_TAC list_ss [HYPOTHESIS_RULE_COND_THM, SAFE_DEL_EL___EQ] THEN 1158 REPEAT STRIP_TAC THEN 1159 METIS_TAC[MEM_LIST_PF_SEM, MEM_EL, PF_TURN_EQ___SEM], 1160 1161 1162 SIMP_TAC list_ss [HYPOTHESIS_RULE_COND_THM, SAFE_DEL_EL___EQ] THEN 1163 REPEAT STRIP_TAC THEN 1164 `n < LENGTH pfL2` by DECIDE_TAC THEN 1165 FULL_SIMP_TAC std_ss [EL_APPEND1] THEN 1166 METIS_TAC[MEM_LIST_PF_SEM, MEM_EL, PF_TURN_EQ___SEM] 1167]) 1168 1169 1170 1171 1172 1173val HYPOTHESIS_RULE_MAP_def = Define ` 1174 (HYPOTHESIS_RULE_MAP cL pfL1 pfL2 n f [] = []) /\ 1175 (HYPOTHESIS_RULE_MAP cL pfL1 pfL2 n [] l = l) /\ 1176 (HYPOTHESIS_RULE_MAP cL pfL1 pfL2 n (hyp_case::f) (h::l) = 1177 if HYPOTHESIS_RULE_COND cL pfL1 pfL2 n h hyp_case then 1178 HYPOTHESIS_RULE_MAP cL pfL1 pfL2 (SUC n) f l 1179 else 1180 h::(HYPOTHESIS_RULE_MAP cL pfL1 pfL2 (SUC n) f l) 1181 )` 1182 1183 1184val HYPOTHESIS_RULE_MAP_THM = store_thm ("HYPOTHESIS_RULE_MAP_THM", 1185`` (HYPOTHESIS_RULE_MAP cL pfL1 pfL2 n f [] = []) /\ 1186 (HYPOTHESIS_RULE_MAP cL pfL1 pfL2 n [] l = l) /\ 1187 (HYPOTHESIS_RULE_MAP cL pfL1 pfL2 n (hyp_case::f) (h::l) = 1188 if HYPOTHESIS_RULE_COND cL pfL1 pfL2 n h hyp_case then 1189 HYPOTHESIS_RULE_MAP cL pfL1 pfL2 (SUC n) f l 1190 else 1191 h::(HYPOTHESIS_RULE_MAP cL pfL1 pfL2 (SUC n) f l) 1192 )``, 1193 1194Cases_on `l` THEN SIMP_TAC list_ss [HYPOTHESIS_RULE_MAP_def]); 1195 1196 1197val HYPOTHESIS_RULE_MAP___SEM1 = prove ( 1198``!s h n cL c2 pfL1 pfL2 f l. 1199 (HEAP_DISTINCT s h cL c2 /\ LIST_PF_SEM s pfL1 /\ LIST_PF_SEM s pfL2 /\ n <= LENGTH pfL2) ==> 1200 1201 (LIST_PF_SEM s (HYPOTHESIS_RULE_MAP cL pfL1 (pfL2++l) n f l) = 1202 LIST_PF_SEM s l)``, 1203 1204 1205 1206Induct_on `l` THENL [ 1207 SIMP_TAC list_ss [HYPOTHESIS_RULE_MAP_THM], 1208 1209 Cases_on `f` THEN SIMP_TAC list_ss [HYPOTHESIS_RULE_MAP_def] THEN 1210 REPEAT STRIP_TAC THEN 1211 `PF_SEM s h' ==> (LIST_PF_SEM s (HYPOTHESIS_RULE_MAP cL pfL1 (pfL2 ++ h'::l) (SUC n) t l) = 1212 LIST_PF_SEM s l)` by ( 1213 `(pfL2 ++ (h'::l)) = ((pfL2 ++ [h']) ++ l)` by ( 1214 SIMP_TAC std_ss [APPEND_11, GSYM APPEND_ASSOC, APPEND] 1215 ) THEN 1216 ASM_REWRITE_TAC[] THEN 1217 STRIP_TAC THEN 1218 Q.PAT_X_ASSUM `!s n. P s n` MATCH_MP_TAC THEN 1219 ASM_SIMP_TAC list_ss [LIST_PF_SEM_THM] THEN 1220 METIS_TAC[] 1221 ) THEN 1222 1223 1224 1225 Cases_on `HYPOTHESIS_RULE_COND cL pfL1 (pfL2 ++ h'::l) n h' h ` THENL [ 1226 ASM_SIMP_TAC std_ss [LIST_PF_SEM_THM] THEN 1227 `PF_SEM s h'` by METIS_TAC[HYPOTHESIS_RULE_COND___SEM] THEN 1228 ASM_SIMP_TAC std_ss [], 1229 1230 ASM_SIMP_TAC std_ss [LIST_PF_SEM_THM] THEN 1231 Cases_on `PF_SEM s h'` THEN ASM_REWRITE_TAC[] THEN 1232 METIS_TAC[] 1233 ] 1234]) 1235 1236 1237val HYPOTHESIS_RULE_MAP___SEM = store_thm ("HYPOTHESIS_RULE_MAP___SEM", 1238``!s h c1 c2 pfL1 f l. 1239 HEAP_DISTINCT s h c1 c2 /\ LIST_PF_SEM s pfL1 ==> 1240 1241 (LIST_PF_SEM s (HYPOTHESIS_RULE_MAP c1 pfL1 l 0 f l) = 1242 LIST_PF_SEM s l)``, 1243 1244REPEAT STRIP_TAC THEN 1245MP_TAC (Q.SPECL [`s`, `h`, `0`, `c1`, `c2`, `pfL1`, `[]`, `f`, `l`] HYPOTHESIS_RULE_MAP___SEM1) THEN 1246ASM_SIMP_TAC list_ss [LIST_PF_SEM_THM]) 1247 1248 1249 1250 1251 1252 1253 1254val INFERENCE_HYPOTHESIS___EVAL = store_thm ("INFERENCE_HYPOTHESIS___EVAL", 1255 ``!f1 f2 c1 c2 pfL sfL pfL' sfL'. 1256 LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') = 1257 LIST_DS_ENTAILS (c1,c2) (HYPOTHESIS_RULE_MAP c1 [] pfL 0 f1 pfL,sfL) (HYPOTHESIS_RULE_MAP c1 pfL pfL' 0 f2 pfL',sfL')``, 1258 1259SIMP_TAC std_ss [LIST_DS_ENTAILS_def, HYPOTHESIS_RULE_MAP___SEM, 1260 LIST_DS_SEM_def, LIST_PF_SEM_THM] THEN 1261METIS_TAC[HYPOTHESIS_RULE_MAP___SEM, LIST_PF_SEM_THM]) 1262 1263 1264 1265 1266 1267 1268val INFERENCE_STAR_INTRODUCTION___points_to___EVAL = store_thm ("INFERENCE_STAR_INTRODUCTION___points_to___EVAL", 1269 ``!e n a1 m a2 c1 c2 pfL sfL pfL' sfL'. 1270 ( 1271 (SAFE_DEL_EL n sfL = [sf_points_to e a1]) /\ 1272 (SAFE_DEL_EL m sfL' = [sf_points_to e a2]) /\ 1273 (EVERY (\x. MEM x a1) a2) /\ ALL_DISTINCT (MAP FST a1)) ==> 1274 1275 (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') = 1276 LIST_DS_ENTAILS (e::c1,c2) (pfL,DELETE_ELEMENT n sfL) (pfL',DELETE_ELEMENT m sfL'))``, 1277 1278 1279SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 1280REPEAT STRIP_TAC THEN 1281`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 1282 LIST_DS_ENTAILS (c1, c2) (pfL,SWAP_TO_POS 0 n sfL) (pfL',SWAP_TO_POS 0 m sfL')` by ( 1283 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 1284 SIMP_TAC std_ss [PERM_REFL] THEN 1285 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 1286) THEN 1287ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 1288MATCH_MP_TAC (GSYM INFERENCE_STAR_INTRODUCTION___points_to) THEN 1289FULL_SIMP_TAC std_ss [EVERY_MEM]) 1290 1291 1292 1293val INFERENCE_STAR_INTRODUCTION___list___EVAL = store_thm ("INFERENCE_STAR_INTRODUCTION___list___EVAL", 1294 ``!f e1 e2 n m c1 c2 pfL sfL pfL' sfL'. 1295 ( 1296 (SAFE_DEL_EL n sfL = [sf_ls f e1 e2]) /\ 1297 (SAFE_DEL_EL m sfL' = [sf_ls f e1 e2])) ==> 1298 1299 (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') = 1300 LIST_DS_ENTAILS (c1,(e1,e2)::c2) (pfL,DELETE_ELEMENT n sfL) (pfL',DELETE_ELEMENT m sfL'))``, 1301 1302 1303SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 1304REPEAT STRIP_TAC THEN 1305`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 1306 LIST_DS_ENTAILS (c1, c2) (pfL,SWAP_TO_POS 0 n sfL) (pfL',SWAP_TO_POS 0 m sfL')` by ( 1307 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 1308 SIMP_TAC std_ss [PERM_REFL] THEN 1309 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 1310) THEN 1311ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 1312ASM_REWRITE_TAC [INFERENCE_STAR_INTRODUCTION___list]) 1313 1314 1315 1316 1317 1318val INFERENCE_STAR_INTRODUCTION___bin_tree___EVAL = store_thm ("INFERENCE_STAR_INTRODUCTION___bin_tree___EVAL", 1319 ``!e f1 f2 f1' f2' n m c1 c2 pfL sfL pfL' sfL'. 1320 (((f1' = f1) /\ (f2' = f2) \/ (f2' = f1) /\ (f1' = f2)) /\ 1321 (SAFE_DEL_EL n sfL = [sf_bin_tree (f1,f2) e]) /\ 1322 (SAFE_DEL_EL m sfL' = [sf_bin_tree (f1',f2') e])) ==> 1323 1324 (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') = 1325 LIST_DS_ENTAILS (c1,(e,dse_nil)::c2) (pfL,DELETE_ELEMENT n sfL) (pfL',DELETE_ELEMENT m sfL'))``, 1326 1327 1328SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 1329REPEAT STRIP_TAC THEN ( 1330 `LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 1331 LIST_DS_ENTAILS (c1, c2) (pfL,SWAP_TO_POS 0 n sfL) (pfL',SWAP_TO_POS 0 m sfL')` by ( 1332 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 1333 SIMP_TAC std_ss [PERM_REFL] THEN 1334 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 1335 ) THEN 1336 ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 1337 MATCH_MP_TAC (GSYM INFERENCE_STAR_INTRODUCTION___bin_tree) THEN 1338 ASM_REWRITE_TAC[] 1339)) 1340 1341 1342 1343 1344 1345val INFERENCE_STAR_INTRODUCTION___EVAL1 = store_thm ("INFERENCE_STAR_INTRODUCTION___EVAL1", 1346 ``!sfL'' c1 c2 pfL sfL pfL' sfL'. 1347 (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') ==> 1348 LIST_DS_ENTAILS (c1,c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL''))``, 1349 1350 1351REPEAT STRIP_TAC THEN 1352`LIST_DS_ENTAILS (c1, c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL'') = 1353 LIST_DS_ENTAILS (c1, c2) (pfL,sfL''++sfL) (pfL',sfL''++sfL')` by ( 1354 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 1355 SIMP_TAC std_ss [PERM_REFL, PERM_APPEND] 1356) THEN 1357ASM_REWRITE_TAC[] THEN POP_ASSUM (K ALL_TAC) THEN 1358 1359Induct_on `sfL''` THENL [ 1360 ASM_SIMP_TAC list_ss [], 1361 ASM_SIMP_TAC list_ss [INFERENCE_STAR_INTRODUCTION___IMPL] 1362]) 1363 1364 1365 1366 1367val INFERENCE_STAR_INTRODUCTION___EVAL1 = store_thm ("INFERENCE_STAR_INTRODUCTION___EVAL1", 1368 ``!sfL'' c1 c2 pfL sfL pfL' sfL'. 1369 (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') ==> 1370 LIST_DS_ENTAILS (c1,c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL''))``, 1371 1372 1373REPEAT STRIP_TAC THEN 1374`LIST_DS_ENTAILS (c1, c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL'') = 1375 LIST_DS_ENTAILS (c1, c2) (pfL,sfL''++sfL) (pfL',sfL''++sfL')` by ( 1376 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 1377 SIMP_TAC std_ss [PERM_REFL, PERM_APPEND] 1378) THEN 1379ASM_REWRITE_TAC[] THEN POP_ASSUM (K ALL_TAC) THEN 1380 1381Induct_on `sfL''` THENL [ 1382 ASM_SIMP_TAC list_ss [], 1383 ASM_SIMP_TAC list_ss [INFERENCE_STAR_INTRODUCTION___IMPL] 1384]) 1385 1386 1387val INFERENCE_STAR_INTRODUCTION___EVAL2 = store_thm ("INFERENCE_STAR_INTRODUCTION___EVAL2", 1388 ``!x n1 n2 c1 c2 pfL sfL pfL' sfL'. 1389 ((SAFE_DEL_EL n1 sfL = [x]) /\ 1390 (SAFE_DEL_EL n2 sfL' = [x]) /\ 1391 LIST_DS_ENTAILS (c1,c2) (pfL,DELETE_ELEMENT n1 sfL) (pfL',DELETE_ELEMENT n2 sfL')) ==> 1392 LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL')``, 1393 1394REPEAT GEN_TAC THEN 1395`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 1396 LIST_DS_ENTAILS (c1, c2) (pfL,SWAP_TO_POS 0 n1 sfL) (pfL',SWAP_TO_POS 0 n2 sfL')` by ( 1397 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 1398 SIMP_TAC std_ss [PERM_REFL] THEN 1399 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 1400) THEN 1401ASM_SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 1402POP_ASSUM (K ALL_TAC) THEN 1403STRIP_TAC THEN 1404POP_ASSUM MP_TAC THEN 1405ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 1406METIS_TAC[INFERENCE_STAR_INTRODUCTION___IMPL]); 1407 1408 1409 1410 1411 1412 1413 1414 1415 1416 1417val SF_POINTS_TO_LIST_def = Define ` 1418 (SF_POINTS_TO_LIST [] = []) /\ 1419 (SF_POINTS_TO_LIST ((sf_points_to e1 e2)::l) = e1::SF_POINTS_TO_LIST l) /\ 1420 (SF_POINTS_TO_LIST (sf::l) = SF_POINTS_TO_LIST l)` 1421 1422 1423 1424 1425val EL___SF_POINTS_TO_LIST = store_thm ("EL___SF_POINTS_TO_LIST", 1426``!l n. (n < LENGTH (SF_POINTS_TO_LIST l)) ==> 1427 ?n' a. (n' < LENGTH l) /\ (n <= n') /\ 1428 (EL n' l = sf_points_to (EL n (SF_POINTS_TO_LIST l)) a)``, 1429 1430Induct_on `l` THENL [ 1431 SIMP_TAC list_ss [SF_POINTS_TO_LIST_def], 1432 1433 GEN_TAC THEN 1434 Cases_on `SF_POINTS_TO_LIST (h::l) = SF_POINTS_TO_LIST l` THEN1 ( 1435 ASM_SIMP_TAC list_ss [] THEN 1436 REPEAT STRIP_TAC THEN 1437 RES_TAC THEN 1438 Q.EXISTS_TAC `SUC n'` THEN 1439 Q.EXISTS_TAC `a` THEN 1440 ASM_SIMP_TAC list_ss [] 1441 ) THEN 1442 Cases_on `h` THEN FULL_SIMP_TAC list_ss [SF_POINTS_TO_LIST_def] THEN 1443 REPEAT STRIP_TAC THEN 1444 Cases_on `n` THENL [ 1445 FULL_SIMP_TAC std_ss [] THEN 1446 Q.EXISTS_TAC `0` THEN 1447 SIMP_TAC list_ss [] THEN 1448 METIS_TAC[], 1449 1450 FULL_SIMP_TAC list_ss [] THEN 1451 RES_TAC THEN 1452 Q.EXISTS_TAC `SUC n''` THEN 1453 Q.EXISTS_TAC `a` THEN 1454 ASM_SIMP_TAC list_ss [] 1455 ] 1456]) 1457 1458 1459 1460val EL2___SF_POINTS_TO_LIST = store_thm ("EL___SF_POINTS_TO_LIST", 1461 1462``!l n m. ((m < LENGTH (SF_POINTS_TO_LIST l)) /\ (n < m)) ==> 1463 ?n' m' e e'. (m' < LENGTH l) /\ (n <= n') /\ (m <= m') /\ 1464 (n' < m') /\ (EL n' l = sf_points_to (EL n (SF_POINTS_TO_LIST l)) e) /\ 1465 (EL m' l = sf_points_to (EL m (SF_POINTS_TO_LIST l)) e')``, 1466 1467Induct_on `l` THENL [ 1468 SIMP_TAC list_ss [SF_POINTS_TO_LIST_def], 1469 1470 GEN_TAC THEN 1471 Cases_on `SF_POINTS_TO_LIST (h::l) = SF_POINTS_TO_LIST l` THEN1 ( 1472 ASM_SIMP_TAC list_ss [] THEN 1473 REPEAT STRIP_TAC THEN 1474 Q.PAT_X_ASSUM `!n m. P n m` (fn thm => MP_TAC (Q.ISPECL [`n:num`, `m:num`] thm)) THEN 1475 ASM_SIMP_TAC std_ss [] THEN 1476 STRIP_TAC THEN 1477 Q.EXISTS_TAC `SUC n'` THEN 1478 Q.EXISTS_TAC `SUC m'` THEN 1479 Q.EXISTS_TAC `e` THEN 1480 Q.EXISTS_TAC `e'` THEN 1481 ASM_SIMP_TAC list_ss [] 1482 ) THEN 1483 Cases_on `h` THEN FULL_SIMP_TAC std_ss [SF_POINTS_TO_LIST_def] THEN 1484 POP_ASSUM (fn thm => ALL_TAC) THEN 1485 ASM_SIMP_TAC list_ss [] THEN 1486 REPEAT STRIP_TAC THEN 1487 Cases_on `m` THEN1 FULL_SIMP_TAC std_ss [] THEN 1488 Cases_on `n` THENL [ 1489 FULL_SIMP_TAC std_ss [] THEN 1490 `?n'' e. 1491 n'' < LENGTH l /\ n' <= n'' /\ 1492 (EL n'' l = sf_points_to (EL n' (SF_POINTS_TO_LIST l)) e)` by 1493 METIS_TAC [EL___SF_POINTS_TO_LIST] THEN 1494 Q.EXISTS_TAC `0` THEN 1495 Q.EXISTS_TAC `SUC n''` THEN 1496 ASM_SIMP_TAC list_ss [] THEN 1497 METIS_TAC[], 1498 1499 1500 FULL_SIMP_TAC list_ss [] THEN 1501 Q.PAT_X_ASSUM `!n m. P n m` (fn thm => MP_TAC (Q.ISPECL [`n'':num`, `n':num`] thm)) THEN 1502 ASM_SIMP_TAC list_ss [] THEN 1503 STRIP_TAC THEN 1504 Q.EXISTS_TAC `SUC n'''` THEN 1505 Q.EXISTS_TAC `SUC m'` THEN 1506 Q.EXISTS_TAC `e` THEN 1507 Q.EXISTS_TAC `e'` THEN 1508 ASM_SIMP_TAC list_ss [] 1509 ] 1510]); 1511 1512 1513 1514 1515 1516 1517 1518 1519 1520 1521 1522val _ = Hol_datatype `pointsto_cases = 1523 pointsto_skip 1524 | pointsto_pointsto 1525 | pointsto_tree of bool => num` 1526 1527val SF_POINTS_TO_LIST_COND_def = Define ` 1528 (SF_POINTS_TO_LIST_COND pfL pointsto_skip h = []) /\ 1529 (SF_POINTS_TO_LIST_COND pfL pointsto_pointsto (sf_points_to e a) = [e]) /\ 1530 (SF_POINTS_TO_LIST_COND pfL pointsto_pointsto (_) = []) /\ 1531 (SF_POINTS_TO_LIST_COND pfL (pointsto_tree turn n) (sf_tree fL es e) = 1532 if (SAFE_DEL_EL n pfL = [if turn then pf_unequal es e else pf_unequal e es]) then [e] else []) /\ 1533 (SF_POINTS_TO_LIST_COND pfL (pointsto_tree turn n) _ = [])` 1534 1535val SF_POINTS_TO_LIST_COND_THM = store_thm ("SF_POINTS_TO_LIST_COND_THM", 1536``(SF_POINTS_TO_LIST_COND pfL pointsto_skip h = []) /\ 1537 (SF_POINTS_TO_LIST_COND pfL pointsto_pointsto (sf_points_to e a) = [e]) /\ 1538 (SF_POINTS_TO_LIST_COND pfL (pointsto_tree T n) (sf_tree fL es e) = 1539 if (SAFE_DEL_EL n pfL = [pf_unequal es e]) then [e] else []) /\ 1540 (SF_POINTS_TO_LIST_COND pfL (pointsto_tree F n) (sf_tree fL es e) = 1541 if (SAFE_DEL_EL n pfL = [pf_unequal e es]) then [e] else []) /\ 1542 (SF_POINTS_TO_LIST_COND pfL (pointsto_tree T n) (sf_ls f e1 e2) = 1543 if (SAFE_DEL_EL n pfL = [pf_unequal e2 e1]) then [e1] else []) /\ 1544 (SF_POINTS_TO_LIST_COND pfL (pointsto_tree F n) (sf_ls f e1 e2) = 1545 if (SAFE_DEL_EL n pfL = [pf_unequal e1 e2]) then [e1] else []) /\ 1546 1547 (SF_POINTS_TO_LIST_COND pfL (pointsto_tree T n) (sf_bin_tree (f1,f2) e) = 1548 if (SAFE_DEL_EL n pfL = [pf_unequal dse_nil e]) then [e] else []) /\ 1549 (SF_POINTS_TO_LIST_COND pfL (pointsto_tree F n) (sf_bin_tree (f1,f2) e) = 1550 if (SAFE_DEL_EL n pfL = [pf_unequal e dse_nil]) then [e] else [])``, 1551 1552SIMP_TAC std_ss [SF_POINTS_TO_LIST_COND_def, sf_ls_def, sf_bin_tree_def]) 1553 1554 1555 1556 1557val SF_POINTS_TO_LIST_COND_FILTER_def = Define ` 1558 (SF_POINTS_TO_LIST_COND_FILTER pfL f [] = []) /\ 1559 (SF_POINTS_TO_LIST_COND_FILTER pfL [] l = []) /\ 1560 (SF_POINTS_TO_LIST_COND_FILTER pfL (pointsto_case::f) (h::l) = 1561 (SF_POINTS_TO_LIST_COND pfL pointsto_case h)++ 1562 (SF_POINTS_TO_LIST_COND_FILTER pfL f l))` 1563 1564 1565 1566 1567 1568val SF_POINTS_TO_LIST_COND___PRED_def = Define ` 1569 SF_POINTS_TO_LIST_COND___PRED pfL e1 e2 = 1570((?a. (e2 = sf_points_to e1 a)) \/ 1571 ((?es b fL m. 1572 (m < LENGTH pfL) /\ 1573 (EL m pfL = (if b then (pf_unequal es e1) else (pf_unequal e1 es))) /\ 1574 (e2 = sf_tree fL es e1))))`; 1575 1576 1577 1578val SF_POINTS_TO_LIST_COND___PRED___WEAKEN = store_thm ("SF_POINTS_TO_LIST_COND___PRED___WEAKEN", 1579 ``!pfL1 pfL2 e1 e2. ((!x. MEM x pfL1 ==> MEM x pfL2) /\ 1580 SF_POINTS_TO_LIST_COND___PRED pfL1 e1 e2) ==> 1581 SF_POINTS_TO_LIST_COND___PRED (pfL2) e1 e2``, 1582 1583SIMP_TAC std_ss [SF_POINTS_TO_LIST_COND___PRED_def] THEN 1584REPEAT STRIP_TAC THEN 1585ASM_SIMP_TAC std_ss [ds_spatial_formula_11, ds_spatial_formula_distinct] THEN 1586METIS_TAC[MEM_EL]); 1587 1588 1589 1590val EL___SF_POINTS_TO_LIST_COND_FILTER = store_thm ("EL___SF_POINTS_TO_LIST_COND_FILTER", 1591``!l pfL f n. (n < LENGTH (SF_POINTS_TO_LIST_COND_FILTER pfL f l)) ==> 1592 (?n'. (n' < LENGTH l) /\ (n <= n') /\ 1593 SF_POINTS_TO_LIST_COND___PRED pfL (EL n (SF_POINTS_TO_LIST_COND_FILTER pfL f l)) (EL n' l))``, 1594 1595Induct_on `l` THENL [ 1596 Cases_on `f` THEN 1597 SIMP_TAC list_ss [SF_POINTS_TO_LIST_COND_FILTER_def], 1598 1599 REPEAT GEN_TAC THEN 1600 Cases_on `f` THEN1 SIMP_TAC list_ss [SF_POINTS_TO_LIST_COND_FILTER_def] THEN 1601 1602 Cases_on `(SF_POINTS_TO_LIST_COND_FILTER pfL (h'::t) (h::l)) = 1603 (SF_POINTS_TO_LIST_COND_FILTER pfL t l)` THEN1 ( 1604 ASM_SIMP_TAC list_ss [] THEN 1605 REPEAT STRIP_TAC THEN 1606 RES_TAC THEN 1607 Q.EXISTS_TAC `SUC n'` THEN 1608 ASM_SIMP_TAC list_ss [] 1609 ) THEN 1610 `?x. (SF_POINTS_TO_LIST_COND_FILTER pfL (h'::t) (h::l)) = 1611 x::(SF_POINTS_TO_LIST_COND_FILTER pfL t l)` by ( 1612 Cases_on `h` THEN 1613 Cases_on `h'` THEN 1614 FULL_SIMP_TAC list_ss [SF_POINTS_TO_LIST_COND_FILTER_def, SF_POINTS_TO_LIST_COND_def, 1615 COND_RATOR, COND_RAND] 1616 ) THEN 1617 FULL_SIMP_TAC list_ss [] THEN 1618 STRIP_TAC THEN 1619 Tactical.REVERSE (Cases_on `n`) THEN1 ( 1620 FULL_SIMP_TAC std_ss [] THEN 1621 RES_TAC THEN 1622 Q.EXISTS_TAC `SUC n''` THEN 1623 ASM_SIMP_TAC list_ss [] 1624 ) THEN 1625 FULL_SIMP_TAC list_ss [] THEN 1626 1627 Q.EXISTS_TAC `0` THEN 1628 SIMP_TAC list_ss [SF_POINTS_TO_LIST_COND___PRED_def] THEN 1629 Cases_on `h'` THEN Cases_on `h` THEN ( 1630 FULL_SIMP_TAC list_ss [SF_POINTS_TO_LIST_COND_FILTER_def, SF_POINTS_TO_LIST_COND_def, 1631 ds_spatial_formula_11, ds_spatial_formula_distinct] 1632 ) THEN 1633 Cases_on `SAFE_DEL_EL n pfL = [(if b then pf_unequal d d0 else pf_unequal d0 d)]` THEN FULL_SIMP_TAC list_ss [] THEN 1634 FULL_SIMP_TAC list_ss [SAFE_DEL_EL___EQ] THEN 1635 METIS_TAC[] 1636]) 1637 1638 1639 1640val EL2___SF_POINTS_TO_LIST_COND_FILTER = store_thm ("EL2___SF_POINTS_TO_LIST_COND_FILTER", 1641 1642``!l pfL f n m. ((m < LENGTH (SF_POINTS_TO_LIST_COND_FILTER pfL f l)) /\ (n < m)) ==> 1643 ?n' m'. (m' < LENGTH l) /\ (n <= n') /\ (m <= m') /\ 1644 (n' < m') /\ 1645 SF_POINTS_TO_LIST_COND___PRED pfL (EL n (SF_POINTS_TO_LIST_COND_FILTER pfL f l)) (EL n' l) /\ 1646 SF_POINTS_TO_LIST_COND___PRED pfL (EL m (SF_POINTS_TO_LIST_COND_FILTER pfL f l)) (EL m' l)``, 1647 1648 1649Induct_on `l` THENL [ 1650 Cases_on `f` THEN 1651 SIMP_TAC list_ss [SF_POINTS_TO_LIST_COND_FILTER_def], 1652 1653 REPEAT GEN_TAC THEN 1654 Cases_on `f` THEN1 SIMP_TAC list_ss [SF_POINTS_TO_LIST_COND_FILTER_def] THEN 1655 Cases_on `(SF_POINTS_TO_LIST_COND_FILTER pfL (h'::t) (h::l)) = 1656 (SF_POINTS_TO_LIST_COND_FILTER pfL t l)` THEN1 ( 1657 ASM_SIMP_TAC list_ss [] THEN 1658 REPEAT STRIP_TAC THEN 1659 Q.PAT_X_ASSUM `!pfL f n m. P n m` (fn thm => MP_TAC (Q.SPECL [`pfL`, `t`, `n:num`, `m:num`] thm)) THEN 1660 ASM_REWRITE_TAC [] THEN 1661 STRIP_TAC THEN 1662 Q.EXISTS_TAC `SUC n'` THEN 1663 Q.EXISTS_TAC `SUC m'` THEN 1664 ASM_SIMP_TAC list_ss [] 1665 ) THEN 1666 `?x. (SF_POINTS_TO_LIST_COND_FILTER pfL (h'::t) (h::l)) = 1667 x::(SF_POINTS_TO_LIST_COND_FILTER pfL t l)` by ( 1668 Cases_on `h` THEN 1669 Cases_on `h'` THEN 1670 FULL_SIMP_TAC list_ss [SF_POINTS_TO_LIST_COND_FILTER_def, SF_POINTS_TO_LIST_COND_def, 1671 COND_RATOR, COND_RAND] 1672 ) THEN 1673 FULL_SIMP_TAC list_ss [] THEN 1674 Cases_on `m` THEN1 FULL_SIMP_TAC std_ss [] THEN 1675 Cases_on `n` THENL [ 1676 FULL_SIMP_TAC list_ss [] THEN 1677 STRIP_TAC THEN 1678 MP_TAC (Q.SPECL [`h::l`, `pfL`, `h'::t`, `SUC n'`] EL___SF_POINTS_TO_LIST_COND_FILTER) THEN 1679 ASM_SIMP_TAC list_ss [] THEN 1680 STRIP_TAC THEN 1681 Q.EXISTS_TAC `0` THEN 1682 Q.EXISTS_TAC `n''` THEN 1683 ASM_SIMP_TAC list_ss [] THEN 1684 1685 Q.PAT_X_ASSUM `Y = x::Z` MP_TAC THEN 1686 Cases_on `h'` THEN Cases_on `h` THEN ( 1687 SIMP_TAC list_ss [SF_POINTS_TO_LIST_COND___PRED_def, SF_POINTS_TO_LIST_COND_FILTER_def, 1688 SF_POINTS_TO_LIST_COND_def, ds_spatial_formula_11, ds_spatial_formula_distinct] 1689 ) THEN 1690 SIMP_TAC list_ss [COND_RATOR, COND_RAND, SAFE_DEL_EL___EQ] THEN 1691 METIS_TAC[], 1692 1693 1694 SIMP_TAC std_ss [] THEN 1695 STRIP_TAC THEN 1696 Q.PAT_X_ASSUM `!pfL f n m. P n m` (fn thm => MP_TAC (Q.SPECL [`pfL`, `t`, `n'':num`, `n':num`] thm)) THEN 1697 ASM_SIMP_TAC list_ss [] THEN 1698 STRIP_TAC THEN 1699 Q.EXISTS_TAC `SUC n'''` THEN 1700 Q.EXISTS_TAC `SUC m'` THEN 1701 ASM_SIMP_TAC list_ss [] 1702 ] 1703]); 1704 1705 1706 1707 1708 1709 1710 1711 1712 1713 1714 1715 1716 1717val INFERENCE_NIL_NOT_LVAL___EVAL_NIL1 = prove ( 1718 1719``!l c1 c2 pfL sfL pfL' sfL'. 1720 (!x. MEM x l ==> ?y. SF_POINTS_TO_LIST_COND___PRED pfL x y /\ MEM y sfL) ==> 1721 1722 (LIST_DS_ENTAILS (c1, c2) 1723 (MAP (\e. pf_unequal e dse_nil) l ++ pfL,sfL) 1724 (pfL',sfL') = 1725 LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL'))``, 1726 1727 1728NTAC 7 GEN_TAC THEN 1729Induct_on `l` THENL [ 1730 SIMP_TAC list_ss [SAFE_FILTER_THM], 1731 1732 SIMP_TAC list_ss [DISJ_IMP_THM, FORALL_AND_THM] THEN 1733 REPEAT STRIP_TAC THEN 1734 FULL_SIMP_TAC list_ss [] THEN 1735 Q.PAT_X_ASSUM `Y = LIST_DS_ENTAILS (c1,c2) (pfL, sfL) (pfL', sfL')` 1736 (fn thm => (ASSUME_TAC (GSYM thm))) THEN 1737 FULL_SIMP_TAC std_ss [MEM_EL] THEN 1738 Q.PAT_X_ASSUM `Y = EL n sfL` (ASSUME_TAC o GSYM) THEN 1739 1740 `!pfL. LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 1741 LIST_DS_ENTAILS (c1, c2) (pfL,SWAP_TO_POS 0 n sfL) (pfL',sfL')` by ( 1742 GEN_TAC THEN 1743 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 1744 SIMP_TAC std_ss [PERM_REFL] THEN 1745 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 1746 ) THEN 1747 FULL_SIMP_TAC std_ss [SF_POINTS_TO_LIST_COND___PRED_def, SWAP_TO_POS___DELETE_ELEMENT] THENL [ 1748 ASM_SIMP_TAC list_ss [INFERENCE_NIL_NOT_LVAL___points_to], 1749 1750 1751 MATCH_MP_TAC INFERENCE_NIL_NOT_LVAL___tree THEN 1752 SIMP_TAC list_ss [MEM_UNEQ_PF_LIST_def] THEN 1753 METIS_TAC[MEM_EL] 1754 ] 1755]) 1756 1757 1758 1759val INFERENCE_NIL_NOT_LVAL___EVAL = store_thm ("INFERENCE_NIL_NOT_LVAL___EVAL", 1760``!f c1 c2 pfL sfL pfL' sfL'. 1761 LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 1762 (LIST_DS_ENTAILS (c1, c2) 1763 ((MAP (\e. pf_unequal e dse_nil) (SF_POINTS_TO_LIST_COND_FILTER pfL f sfL)) ++ pfL,sfL) 1764 (pfL',sfL'))``, 1765 1766REPEAT GEN_TAC THEN 1767MATCH_MP_TAC (GSYM INFERENCE_NIL_NOT_LVAL___EVAL_NIL1) THEN 1768REPEAT STRIP_TAC THEN 1769FULL_SIMP_TAC std_ss [MEM_EL] THEN 1770METIS_TAC[EL___SF_POINTS_TO_LIST_COND_FILTER]); 1771 1772 1773 1774 1775 1776 1777val DISJOINT_LIST_PRODUCT_def = Define ` 1778 (DISJOINT_LIST_PRODUCT [] = []) /\ 1779 (DISJOINT_LIST_PRODUCT (e::l) = 1780 (MAP (\x. (e, x)) l)++(DISJOINT_LIST_PRODUCT l))`; 1781 1782val MEM___DISJOINT_LIST_PRODUCT = store_thm ("MEM___DISJOINT_LIST_PRODUCT", 1783 ``!e1 e2. (MEM (e1, e2) (DISJOINT_LIST_PRODUCT l) = 1784 ?n m. (n < m) /\ (m < LENGTH l) /\ 1785 (e1 = EL n l) /\ (e2 = EL m l))``, 1786 1787Induct_on `l` THENL [ 1788 SIMP_TAC list_ss [DISJOINT_LIST_PRODUCT_def], 1789 1790 ASM_SIMP_TAC list_ss [DISJOINT_LIST_PRODUCT_def, MEM_MAP] THEN 1791 REPEAT STRIP_TAC THEN EQ_TAC THENL [ 1792 REPEAT STRIP_TAC THENL [ 1793 FULL_SIMP_TAC std_ss [MEM_EL] THEN 1794 Q.EXISTS_TAC `0` THEN 1795 Q.EXISTS_TAC `SUC n` THEN 1796 ASM_SIMP_TAC list_ss [], 1797 1798 Q.EXISTS_TAC `SUC n` THEN 1799 Q.EXISTS_TAC `SUC m` THEN 1800 ASM_SIMP_TAC list_ss [] 1801 ], 1802 1803 STRIP_TAC THEN 1804 Cases_on `m` THEN1 FULL_SIMP_TAC std_ss [] THEN 1805 Cases_on `n` THENL [ 1806 DISJ1_TAC THEN 1807 FULL_SIMP_TAC list_ss [MEM_EL] THEN 1808 METIS_TAC[], 1809 1810 DISJ2_TAC THEN 1811 FULL_SIMP_TAC list_ss [] THEN 1812 METIS_TAC[] 1813 ] 1814 ] 1815]) 1816 1817 1818 1819val LIST_PRODUCT_def = Define ` 1820 (LIST_PRODUCT [] l2 = []) /\ 1821 (LIST_PRODUCT (e::l1) l2 = 1822 (MAP (\x. (e, x)) l2)++(LIST_PRODUCT l1 l2))`; 1823 1824val MEM___LIST_PRODUCT = store_thm ("MEM___DISJOINT_LIST_PRODUCT", 1825 ``!l1 l2 e1 e2. (MEM (e1, e2) (LIST_PRODUCT l1 l2) = 1826 (MEM e1 l1 /\ MEM e2 l2))``, 1827 1828Induct_on `l1` THENL [ 1829 SIMP_TAC list_ss [LIST_PRODUCT_def], 1830 1831 ASM_SIMP_TAC list_ss [LIST_PRODUCT_def, MEM_MAP] THEN 1832 METIS_TAC[] 1833]); 1834 1835 1836 1837 1838val PERM___TWO_ELEMENTS_TO_FRONT_1 = store_thm ("PERM___TWO_ELEMENTS_TO_FRONT_1", 1839``!n1 n2. ((n1 < n2) /\ n2 < LENGTH l) ==> 1840PERM (EL n1 l::EL n2 l::(DELETE_ELEMENT n1 (DELETE_ELEMENT n2 l))) l``, 1841 1842 1843REPEAT STRIP_TAC THEN 1844Cases_on `n2` THEN1 FULL_SIMP_TAC arith_ss [] THEN 1845`!l'. PERM l' l = PERM l' (SWAP_TO_POS (SUC 0) (SUC n) (SWAP_TO_POS 0 n1 l))` by 1846 METIS_TAC[PERM_TRANS, PERM_SYM, PERM___SWAP_TO_POS] THEN 1847ASM_REWRITE_TAC[] THEN 1848MATCH_MP_TAC (prove (``(l = l') ==> PERM l l'``, SIMP_TAC std_ss [PERM_REFL])) THEN 1849 1850`LENGTH (SWAP_TO_POS (SUC 0) (SUC n) l) = LENGTH l` by METIS_TAC[PERM___SWAP_TO_POS, PERM_LENGTH] THEN 1851`n1 < LENGTH l` by DECIDE_TAC THEN 1852ASM_SIMP_TAC bool_ss [SWAP_TO_POS___DELETE_ELEMENT, SWAP_TO_POS_THM] THEN 1853 1854`n < LENGTH (DELETE_ELEMENT n1 l)` by ASM_SIMP_TAC list_ss [LENGTH_DELETE_ELEMENT] THEN 1855ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 1856`~(n < n1)` by DECIDE_TAC THEN 1857`n < LENGTH l` by DECIDE_TAC THEN 1858ASM_SIMP_TAC list_ss [EL_DELETE_ELEMENT] THEN 1859`n1 <= n` by DECIDE_TAC THEN 1860ASM_SIMP_TAC std_ss [GSYM DELETE_ELEMENT_DELETE_ELEMENT]) 1861 1862 1863 1864val PERM___TWO_ELEMENTS_TO_FRONT_2 = store_thm ("PERM___TWO_ELEMENTS_TO_FRONT_2", 1865``!n1 n2. ((n2 < n1) /\ n1 < LENGTH l) ==> 1866PERM (EL n1 l::EL n2 l::(DELETE_ELEMENT n2 (DELETE_ELEMENT n1 l))) l``, 1867 1868REPEAT STRIP_TAC THEN 1869`!l'. PERM l' l = 1870 PERM l' (EL n2 l::EL n1 l::DELETE_ELEMENT n2 (DELETE_ELEMENT n1 l))` by 1871 METIS_TAC[PERM_SYM, PERM___TWO_ELEMENTS_TO_FRONT_1, PERM_TRANS, PERM_REFL] THEN 1872ASM_SIMP_TAC std_ss [PERM_SWAP_AT_FRONT, PERM_REFL]); 1873 1874 1875 1876val PERM___TWO_ELEMENTS_TO_FRONT_3 = store_thm ("PERM___TWO_ELEMENTS_TO_FRONT_3", 1877``!n1 n2. (~(n1 = n2) /\ n1 < LENGTH l /\ n2 < LENGTH l) ==> 1878?l'. (PERM (EL n1 l::EL n2 l::l') l) /\ 1879 (PERM (EL n2 l::l') (DELETE_ELEMENT n1 l))``, 1880 1881REPEAT STRIP_TAC THEN 1882HO_MATCH_MP_TAC (prove (``((?l. P l) /\ (!l. P l ==> Q l)) ==> (?l. P l /\ Q l)``, METIS_TAC[])) THEN 1883CONJ_TAC THEN1 ( 1884 `(n1 < n2) \/ (n2 < n1)` by DECIDE_TAC THENL [ 1885 METIS_TAC[PERM___TWO_ELEMENTS_TO_FRONT_1], 1886 METIS_TAC[PERM___TWO_ELEMENTS_TO_FRONT_2] 1887 ] 1888) THEN 1889REPEAT STRIP_TAC THEN 1890`PERM (EL n1 l::EL n2 l::l') (SWAP_TO_POS 0 n1 l)` by METIS_TAC[PERM_TRANS, PERM___SWAP_TO_POS, PERM_SYM] THEN 1891POP_ASSUM MP_TAC THEN 1892ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT, PERM_CONS_IFF] 1893); 1894 1895 1896val INFERENCE_PARTIAL___EVAL1 = prove ( 1897 1898``!l c1 c2 pfL sfL pfL' sfL'. 1899 (!e1 e2. MEM (e1,e2) l ==> 1900 (?n1 n2 y1 y2. (n1 < n2) /\ 1901 SF_POINTS_TO_LIST_COND___PRED pfL e1 y1 /\ 1902 SF_POINTS_TO_LIST_COND___PRED pfL e2 y2 /\ 1903 (SAFE_DEL_EL n1 sfL = [y1]) /\ 1904 (SAFE_DEL_EL n2 sfL = [y2]))) ==> 1905 1906 (LIST_DS_ENTAILS (c1, c2) 1907 ((MAP (\(e1,e2). pf_unequal e1 e2) l) ++ pfL,sfL) 1908 (pfL',sfL') = 1909 LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL'))``, 1910 1911REPEAT GEN_TAC THEN 1912Induct_on `l` THENL [ 1913 SIMP_TAC list_ss [], 1914 1915 SIMP_TAC list_ss [DISJ_IMP_THM, FORALL_AND_THM] THEN 1916 Cases_on `h` THEN 1917 SIMP_TAC list_ss [] THEN 1918 REPEAT STRIP_TAC THEN 1919 Q.PAT_X_ASSUM `Y ==> (X = Z)` MP_TAC THEN 1920 ASM_REWRITE_TAC[] THEN 1921 SIMP_TAC std_ss [Once EQ_SYM_EQ] THEN 1922 STRIP_TAC THEN 1923 `?sfL''. PERM (y1::y2::sfL'') sfL` by ( 1924 FULL_SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 1925 METIS_TAC[PERM___TWO_ELEMENTS_TO_FRONT_1] 1926 ) THEN 1927 `!pfL. 1928 LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 1929 LIST_DS_ENTAILS (c1, c2) (pfL,y1::y2::sfL'') (pfL',sfL')` by ( 1930 GEN_TAC THEN 1931 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 1932 ASM_SIMP_TAC std_ss [PERM_REFL] THEN 1933 METIS_TAC[PERM_SYM] 1934 ) THEN 1935 ASM_SIMP_TAC std_ss [] THEN 1936 1937 FULL_SIMP_TAC std_ss [SF_POINTS_TO_LIST_COND___PRED_def] THENL [ 1938 REWRITE_TAC [INFERENCE_PARTIAL___points_to___points_to], 1939 1940 MATCH_MP_TAC INFERENCE_PARTIAL___points_to___tree THEN 1941 SIMP_TAC list_ss [MEM_UNEQ_PF_LIST_def] THEN 1942 METIS_TAC[MEM_EL], 1943 1944 1945 `!pfL. 1946 LIST_DS_ENTAILS (c1, c2) (pfL,sf_tree fL es q::sf_points_to r a::sfL'') (pfL',sfL') = 1947 LIST_DS_ENTAILS (c1, c2) (pfL,sf_points_to r a::sf_tree fL es q::sfL'') (pfL',sfL')` by ( 1948 GEN_TAC THEN 1949 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 1950 SIMP_TAC std_ss [PERM_REFL, PERM_SWAP_AT_FRONT] 1951 ) THEN 1952 `!pfL sfL. LIST_DS_ENTAILS (c1,c2) (pf_unequal q r::pfL, sfL) (pfL', sfL') = 1953 LIST_DS_ENTAILS (c1,c2) (pf_unequal r q::pfL, sfL) (pfL', sfL')` by ( 1954 SIMP_TAC std_ss [LIST_DS_ENTAILS_def, LIST_DS_SEM_EVAL, DS_EXPRESSION_EQUAL_def] THEN 1955 METIS_TAC[] 1956 ) THEN 1957 ASM_REWRITE_TAC[] THEN 1958 MATCH_MP_TAC INFERENCE_PARTIAL___points_to___tree THEN 1959 SIMP_TAC list_ss [MEM_UNEQ_PF_LIST_def] THEN 1960 METIS_TAC[MEM_EL], 1961 1962 1963 MATCH_MP_TAC INFERENCE_PARTIAL___tree___tree THEN 1964 SIMP_TAC list_ss [MEM_UNEQ_PF_LIST_def] THEN 1965 METIS_TAC[MEM_EL] 1966 ] 1967]) 1968 1969 1970 1971 1972 1973val INFERENCE_PARTIAL___EVAL2 = prove ( 1974 1975``!f f2 c1 c2 pfL sfL pfL' sfL'. 1976 (LIST_DS_ENTAILS (c1, c2) 1977 ((MAP (\(e1,e2). pf_unequal e1 e2) (SAFE_FILTER F f (DISJOINT_LIST_PRODUCT (SF_POINTS_TO_LIST_COND_FILTER pfL f2 sfL)))) ++ (pfL),sfL) 1978 (pfL',sfL') = 1979 LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL'))``, 1980 1981 1982 1983REPEAT GEN_TAC THEN 1984MATCH_MP_TAC INFERENCE_PARTIAL___EVAL1 THEN 1985REPEAT STRIP_TAC THEN 1986`MEM (e1,e2) (DISJOINT_LIST_PRODUCT (SF_POINTS_TO_LIST_COND_FILTER pfL f2 sfL))` by METIS_TAC[MEM_SAFE_FILTER] THEN 1987FULL_SIMP_TAC std_ss [MEM___DISJOINT_LIST_PRODUCT, SAFE_DEL_EL___EQ] THEN 1988MP_TAC (ISPECL [``sfL:('c, 'b, 'a) ds_spatial_formula list``,``pfL:('b, 'a) ds_pure_formula list``, ``f2:pointsto_cases list``, ``n:num``, ``m:num``] EL2___SF_POINTS_TO_LIST_COND_FILTER) THEN 1989ASM_REWRITE_TAC[] THEN 1990REPEAT STRIP_TAC THEN 1991Q.EXISTS_TAC `n'` THEN 1992Q.EXISTS_TAC `m'` THEN 1993ASM_SIMP_TAC arith_ss []) 1994 1995 1996 1997 1998 1999val INFERENCE_PARTIAL___EVAL3 = prove ( 2000 2001``!l c1 c2 pfL sfL pfL' sfL'. 2002 (!e1 e2. MEM (e1,e2) l ==> 2003 (?n1 n2 y1. 2004 SF_POINTS_TO_LIST_COND___PRED pfL e1 y1 /\ 2005 (SAFE_DEL_EL n1 sfL = [y1]) /\ 2006 (SAFE_DEL_EL n2 c1 = [e2]))) ==> 2007 2008 (LIST_DS_ENTAILS (c1, c2) 2009 ((MAP (\(e1,e2). pf_unequal e1 e2) l) ++ pfL,sfL) 2010 (pfL',sfL') = 2011 LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL'))``, 2012 2013REPEAT GEN_TAC THEN 2014Induct_on `l` THENL [ 2015 SIMP_TAC list_ss [], 2016 2017 SIMP_TAC list_ss [DISJ_IMP_THM, FORALL_AND_THM] THEN 2018 Cases_on `h` THEN 2019 SIMP_TAC list_ss [] THEN 2020 REPEAT STRIP_TAC THEN 2021 Q.PAT_X_ASSUM `Y ==> (X = Z)` MP_TAC THEN 2022 ASM_REWRITE_TAC[] THEN 2023 SIMP_TAC std_ss [Once EQ_SYM_EQ] THEN 2024 STRIP_TAC THEN 2025 `!pfL. 2026 LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 2027 LIST_DS_ENTAILS (c1, c2) (pfL,SWAP_TO_POS 0 n1 sfL) (pfL',sfL')` by ( 2028 GEN_TAC THEN 2029 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 2030 SIMP_TAC std_ss [PERM_REFL] THEN 2031 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2032 ) THEN 2033 FULL_SIMP_TAC std_ss [SAFE_DEL_EL___EQ, SWAP_TO_POS___DELETE_ELEMENT] THEN 2034 `MEM r c1` by METIS_TAC[MEM_EL] THEN 2035 2036 FULL_SIMP_TAC std_ss [SF_POINTS_TO_LIST_COND___PRED_def] THENL [ 2037 ASM_SIMP_TAC std_ss [INFERENCE_PARTIAL___precondition___points_to], 2038 2039 MATCH_MP_TAC INFERENCE_PARTIAL___precondition___tree THEN 2040 ASM_SIMP_TAC list_ss [MEM_UNEQ_PF_LIST_def] THEN 2041 METIS_TAC[MEM_EL] 2042 ] 2043]) 2044 2045 2046 2047val INFERENCE_PARTIAL___EVAL4 = prove ( 2048 2049``!f f2 c1 c2 pfL1 pfL sfL pfL' sfL'. 2050 (LIST_DS_ENTAILS (c1, c2) 2051 ((MAP (\(e1,e2). pf_unequal e1 e2) (SAFE_FILTER F f (LIST_PRODUCT (SF_POINTS_TO_LIST_COND_FILTER pfL f2 sfL) c1))) ++ (pfL1++pfL),sfL) 2052 (pfL',sfL') = 2053 LIST_DS_ENTAILS (c1, c2) (pfL1++pfL,sfL) (pfL',sfL'))``, 2054 2055 2056 2057REPEAT GEN_TAC THEN 2058MATCH_MP_TAC INFERENCE_PARTIAL___EVAL3 THEN 2059REPEAT STRIP_TAC THEN 2060`MEM (e1,e2) (LIST_PRODUCT (SF_POINTS_TO_LIST_COND_FILTER pfL f2 sfL) c1)` by METIS_TAC[MEM_SAFE_FILTER] THEN 2061FULL_SIMP_TAC std_ss [MEM___LIST_PRODUCT, SAFE_DEL_EL___EQ] THEN 2062FULL_SIMP_TAC std_ss [MEM_EL] THEN 2063`!x. MEM x pfL ==> MEM x (pfL1 ++ pfL)` by SIMP_TAC list_ss [] THEN 2064METIS_TAC[EL___SF_POINTS_TO_LIST_COND_FILTER, SF_POINTS_TO_LIST_COND___PRED___WEAKEN]) 2065 2066 2067 2068val INFERENCE_PARTIAL___EVAL = store_thm ("INFERENCE_PARTIAL___EVAL", 2069 2070``!f f2 c1 c2 pfL sfL pfL' sfL'. 2071 LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 2072 (LIST_DS_ENTAILS (c1, c2) 2073 ((MAP (\(e1,e2). pf_unequal e1 e2) (SAFE_FILTER F f 2074 ((LIST_PRODUCT (SF_POINTS_TO_LIST_COND_FILTER pfL f2 sfL) c1) ++ (DISJOINT_LIST_PRODUCT (SF_POINTS_TO_LIST_COND_FILTER pfL f2 sfL))))) ++ pfL,sfL) 2075 (pfL',sfL'))``, 2076 2077SIMP_TAC list_ss [SAFE_FILTER_APPEND] THEN 2078REPEAT STRIP_TAC THEN 2079REWRITE_TAC [GSYM APPEND_ASSOC] THEN 2080REWRITE_TAC [INFERENCE_PARTIAL___EVAL4] THEN 2081REWRITE_TAC [INFERENCE_PARTIAL___EVAL2]); 2082 2083 2084 2085 2086 2087 2088 2089val INFERENCE___precondition_STRENGTHEN_1 = store_thm ("INFERENCE___precondition_STRENGTHEN_1", 2090``!n1 n2 e1 e2 c1 c2 pfL sfL pfL' sfL'. 2091 ((SAFE_DEL_EL n1 pfL = [pf_unequal e1 e2]) /\ 2092 (SAFE_DEL_EL n2 c2 = [(e1,e2)])) ==> 2093 2094 (LIST_DS_ENTAILS (c1, c2) (pfL, sfL) (pfL', sfL') = 2095 LIST_DS_ENTAILS (e1::c1, DELETE_ELEMENT n2 c2) (pfL, sfL) (pfL', sfL'))``, 2096 2097 2098SIMP_TAC std_ss [SAFE_DEL_EL___EQ, LIST_DS_ENTAILS_def] THEN 2099REPEAT STRIP_TAC THEN 2100HO_MATCH_MP_TAC (prove (``(!s h. P s h = Q s h) ==> ((!s h. P s h) = (!s h. Q s h))``, METIS_TAC[])) THEN 2101REPEAT STRIP_TAC THEN 2102Cases_on `LIST_DS_SEM s h (pfL,sfL)` THEN ASM_REWRITE_TAC[] THEN 2103Cases_on `LIST_DS_SEM s h (pfL',sfL')` THEN ASM_REWRITE_TAC[] THEN 2104 2105REPEAT STRIP_TAC THEN 2106`(HEAP_DISTINCT s h c1 c2) = 2107 (HEAP_DISTINCT s h c1 (SWAP_TO_POS 0 n2 c2))` by ( 2108 MATCH_MP_TAC HEAP_DISTINCT___PERM THEN 2109 SIMP_TAC std_ss [PERM_REFL] THEN 2110 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2111) THEN 2112ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 2113MATCH_MP_TAC HEAP_DISTINCT___UNEQUAL THEN 2114`PF_SEM s (pf_unequal e1 e2)` by METIS_TAC[MEM_LIST_PF_SEM, MEM_EL, LIST_DS_SEM_def] THEN 2115FULL_SIMP_TAC std_ss [PF_SEM_def]) 2116 2117 2118 2119 2120val INFERENCE___precondition_STRENGTHEN_2 = store_thm ("INFERENCE___precondition_STRENGTHEN_2", 2121``!n1 n2 e1 e2 c1 c2 pfL sfL pfL' sfL'. 2122 ((SAFE_DEL_EL n1 pfL = [pf_unequal e2 e1]) /\ 2123 (SAFE_DEL_EL n2 c2 = [(e1,e2)])) ==> 2124 2125 (LIST_DS_ENTAILS (c1, c2) (pfL, sfL) (pfL', sfL') = 2126 LIST_DS_ENTAILS (e1::c1, DELETE_ELEMENT n2 c2) (pfL, sfL) (pfL', sfL'))``, 2127 2128 2129SIMP_TAC std_ss [SAFE_DEL_EL___EQ, LIST_DS_ENTAILS_def] THEN 2130REPEAT STRIP_TAC THEN 2131HO_MATCH_MP_TAC (prove (``(!s h. P s h = Q s h) ==> ((!s h. P s h) = (!s h. Q s h))``, METIS_TAC[])) THEN 2132REPEAT STRIP_TAC THEN 2133Cases_on `LIST_DS_SEM s h (pfL,sfL)` THEN ASM_REWRITE_TAC[] THEN 2134Cases_on `LIST_DS_SEM s h (pfL',sfL')` THEN ASM_REWRITE_TAC[] THEN 2135 2136REPEAT STRIP_TAC THEN 2137`(HEAP_DISTINCT s h c1 c2) = 2138 (HEAP_DISTINCT s h c1 (SWAP_TO_POS 0 n2 c2))` by ( 2139 MATCH_MP_TAC HEAP_DISTINCT___PERM THEN 2140 SIMP_TAC std_ss [PERM_REFL] THEN 2141 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2142) THEN 2143ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 2144MATCH_MP_TAC HEAP_DISTINCT___UNEQUAL THEN 2145`PF_SEM s (pf_unequal e2 e1)` by METIS_TAC[MEM_LIST_PF_SEM, MEM_EL, LIST_DS_SEM_def] THEN 2146FULL_SIMP_TAC std_ss [PF_SEM_def, DS_EXPRESSION_EQUAL_def]) 2147 2148 2149 2150 2151val INFERENCE___precondition_NOT_DISTINCT_EQ___EVAL = store_thm ("INFERENCE___precondition_NOT_DISTINCT_EQ___EVAL", 2152``!n1 n2 e1 e2 c1 c2 pfL sfL pfL' sfL'. 2153 ((n1 < n2) /\ (SAFE_DEL_EL n1 c2 = [(e1,e2)]) /\ 2154 (SAFE_DEL_EL n2 c2 = [(e1,e2)])) ==> 2155 2156 (LIST_DS_ENTAILS (c1, c2) (pfL, sfL) (pfL', sfL') = 2157 LIST_DS_ENTAILS (c1, DELETE_ELEMENT n1 (DELETE_ELEMENT n2 c2)) (pf_equal e1 e2::pfL, sfL) (pfL', sfL'))``, 2158 2159 2160SIMP_TAC std_ss [SAFE_DEL_EL___EQ, LIST_DS_ENTAILS_def, LIST_DS_SEM_THM, PF_SEM_def] THEN 2161REPEAT STRIP_TAC THEN 2162HO_MATCH_MP_TAC (prove (``(!s h. P s h = Q s h) ==> ((!s h. P s h) = (!s h. Q s h))``, 2163METIS_TAC[])) THEN 2164REPEAT STRIP_TAC THEN 2165Cases_on `LIST_DS_SEM s h (pfL', sfL')` THEN ASM_SIMP_TAC std_ss [] THEN 2166Cases_on `LIST_DS_SEM s h (pfL, sfL)` THEN ASM_REWRITE_TAC[] THEN 2167Cases_on `~DS_EXPRESSION_EQUAL s e1 e2` THEN1 ( 2168 `~(n1 = n2)` by DECIDE_TAC THEN 2169 METIS_TAC[pairTheory.FST, pairTheory.SND, HEAP_DISTINCT___NOT_ALL_DISTINCT2] 2170) THEN 2171FULL_SIMP_TAC std_ss [] THEN 2172SIMP_TAC std_ss [HEAP_DISTINCT_def] THEN 2173`(FILTER (\(e1,e2). ~DS_EXPRESSION_EQUAL s e1 e2) 2174 (DELETE_ELEMENT n1 (DELETE_ELEMENT n2 c2))) = 2175 (FILTER (\(e1,e2). ~DS_EXPRESSION_EQUAL s e1 e2) c2)` by ( 2176 Q.PAT_X_ASSUM `n1 < n2` MP_TAC THEN 2177 REPEAT (Q.PAT_X_ASSUM `N < LENGTH c2` MP_TAC) THEN 2178 REPEAT (Q.PAT_X_ASSUM `X = (e1,e2)` MP_TAC) THEN 2179 Q.PAT_X_ASSUM `DS_EXPRESSION_EQUAL s e1 e2` MP_TAC THEN 2180 REPEAT (POP_ASSUM (K ALL_TAC)) THEN 2181 Q.SPEC_TAC (`n2`, `n2`) THEN 2182 Q.SPEC_TAC (`n1`, `n1`) THEN 2183 REWRITE_TAC [AND_IMP_INTRO, GSYM CONJ_ASSOC] THEN 2184 2185 Induct_on `c2` THENL [ 2186 SIMP_TAC list_ss [], 2187 2188 SIMP_TAC list_ss [] THEN 2189 REPEAT STRIP_TAC THEN 2190 Cases_on `n2` THEN1 FULL_SIMP_TAC list_ss [] THEN 2191 Cases_on `n1` THENL [ 2192 FULL_SIMP_TAC list_ss [DELETE_ELEMENT_THM] THEN 2193 Q.PAT_X_ASSUM `n < LENGTH c2` MP_TAC THEN 2194 Q.PAT_X_ASSUM `X = (e1,e2)` MP_TAC THEN 2195 Q.PAT_X_ASSUM `DS_EXPRESSION_EQUAL s e1 e2` MP_TAC THEN 2196 REPEAT (POP_ASSUM (K ALL_TAC)) THEN 2197 Q.SPEC_TAC (`n`, `n`) THEN 2198 REWRITE_TAC [AND_IMP_INTRO, GSYM CONJ_ASSOC] THEN 2199 Induct_on `c2` THENL [ 2200 SIMP_TAC list_ss [], 2201 2202 SIMP_TAC list_ss [] THEN 2203 Cases_on `n` THENL [ 2204 SIMP_TAC list_ss [DELETE_ELEMENT_THM], 2205 2206 SIMP_TAC list_ss [DELETE_ELEMENT_THM] THEN 2207 METIS_TAC[] 2208 ] 2209 ], 2210 2211 FULL_SIMP_TAC list_ss [DELETE_ELEMENT_THM] 2212 ] 2213 ] 2214) THEN 2215`!e1 e2. ~(DS_EXPRESSION_EQUAL s e1 e2) ==> 2216 (MEM (e1,e2) c2 = MEM (e1,e2) (DELETE_ELEMENT n1 (DELETE_ELEMENT n2 c2)))` by ( 2217 REPEAT STRIP_TAC THEN 2218 `!l. MEM (e1', e2') l = 2219 MEM (e1', e2') (FILTER (\(e1,e2). ~DS_EXPRESSION_EQUAL s e1 e2) l)` by ( 2220 ASM_SIMP_TAC std_ss [MEM_FILTER] 2221 ) THEN 2222 METIS_TAC[] 2223) THEN 2224METIS_TAC[]); 2225 2226 2227 2228 2229val INFERENCE___precondition_precondition_EQ___EVAL = store_thm ("INFERENCE___precondition_precondition_EQ___EVAL", 2230``!n1 n2 e1 e2 c1 c2 pfL sfL pfL' sfL'. 2231 ((SAFE_DEL_EL n1 c1 = [e1]) /\ 2232 (SAFE_DEL_EL n2 c2 = [(e1,e2)])) ==> 2233 2234 (LIST_DS_ENTAILS (c1, c2) (pfL, sfL) (pfL', sfL') = 2235 LIST_DS_ENTAILS (c1, (DELETE_ELEMENT n2 c2)) (pf_equal e1 e2::pfL, sfL) (pfL', sfL'))``, 2236 2237 2238SIMP_TAC std_ss [SAFE_DEL_EL___EQ, LIST_DS_ENTAILS_def, LIST_DS_SEM_THM, PF_SEM_def] THEN 2239REPEAT STRIP_TAC THEN 2240HO_MATCH_MP_TAC (prove (``(!s h. P s h = Q s h) ==> ((!s h. P s h) = (!s h. Q s h))``, 2241METIS_TAC[])) THEN 2242REPEAT STRIP_TAC THEN 2243Cases_on `LIST_DS_SEM s h (pfL', sfL')` THEN ASM_SIMP_TAC std_ss [] THEN 2244Cases_on `LIST_DS_SEM s h (pfL, sfL)` THEN ASM_REWRITE_TAC[] THEN 2245MATCH_MP_TAC (prove (``(~a = ~b) ==> (a = b)``, SIMP_TAC list_ss [])) THEN 2246REWRITE_TAC [] THEN 2247SIMP_TAC std_ss [] THEN 2248 2249`(HEAP_DISTINCT s h c1 c2) = 2250 (HEAP_DISTINCT s h c1 (SWAP_TO_POS 0 n2 c2))` by ( 2251 MATCH_MP_TAC HEAP_DISTINCT___PERM THEN 2252 SIMP_TAC std_ss [PERM_REFL] THEN 2253 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2254) THEN 2255`!c2. 2256 (HEAP_DISTINCT s h c1 c2) = 2257 (HEAP_DISTINCT s h (SWAP_TO_POS 0 n1 c1) c2)` by ( 2258 GEN_TAC THEN 2259 MATCH_MP_TAC HEAP_DISTINCT___PERM THEN 2260 SIMP_TAC std_ss [PERM_REFL] THEN 2261 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2262) THEN 2263ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 2264 2265SIMP_TAC list_ss [HEAP_DISTINCT___IND_DEF, DISJ_IMP_THM, FORALL_AND_THM] THEN 2266EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN 2267FULL_SIMP_TAC std_ss [DS_EXPRESSION_EQUAL_def]) 2268 2269 2270 2271 2272 2273 2274 2275 2276 2277val INFERENCE___NIL_LIST_EVAL = store_thm ("INFERENCE___NIL_LIST_EVAL", 2278``!n f e c1 c2 pfL sfL pfL' sfL'. 2279 (SAFE_DEL_EL n sfL = [sf_ls f dse_nil e]) ==> 2280 2281 (LIST_DS_ENTAILS (c1, c2) (pfL, sfL) (pfL', sfL') = 2282 LIST_DS_ENTAILS (c1, c2) ((pf_equal e dse_nil)::pfL, DELETE_ELEMENT n sfL) (pfL', sfL'))``, 2283 2284 2285SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 2286REPEAT STRIP_TAC THEN 2287`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 2288LIST_DS_ENTAILS (c1, c2) (pfL,SWAP_TO_POS 0 n sfL) (pfL',sfL')` by ( 2289 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 2290 SIMP_TAC std_ss [PERM_REFL] THEN 2291 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2292) THEN 2293ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 2294ASM_REWRITE_TAC[INFERENCE___NIL_LIST]) 2295 2296 2297 2298 2299val INFERENCE___precondition_LIST_EVAL = store_thm ("INFERENCE___precondition_LIST_EVAL", 2300``!n1 n2 f e1 e2 c1 c2 pfL sfL pfL' sfL'. 2301 ((SAFE_DEL_EL n2 sfL = [sf_ls f e1 e2]) /\ 2302 (SAFE_DEL_EL n1 c1 = [e1])) ==> 2303 2304 (LIST_DS_ENTAILS (c1, c2) (pfL, sfL) (pfL', sfL') = 2305 LIST_DS_ENTAILS (c1, c2) ((pf_equal e2 e1)::pfL, DELETE_ELEMENT n2 sfL) (pfL', sfL'))``, 2306 2307 2308SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 2309REPEAT STRIP_TAC THEN 2310`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 2311LIST_DS_ENTAILS (c1, c2) (pfL,SWAP_TO_POS 0 n2 sfL) (pfL',sfL')` by ( 2312 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 2313 SIMP_TAC std_ss [PERM_REFL] THEN 2314 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2315) THEN 2316ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 2317SIMP_TAC list_ss [LIST_DS_ENTAILS_def] THEN 2318HO_MATCH_MP_TAC (prove (``(!s h. P s h = Q s h) ==> ((!s h. P s h) = (!s h. Q s h))``, METIS_TAC[])) THEN 2319REPEAT STRIP_TAC THEN 2320Cases_on `HEAP_DISTINCT s h c1 c2` THEN ASM_REWRITE_TAC[] THEN 2321Cases_on `LIST_DS_SEM s h (pfL', sfL')` THEN ASM_REWRITE_TAC[] THEN 2322SIMP_TAC std_ss [LIST_DS_SEM_THM, PF_SEM_def] THEN 2323Cases_on `DS_EXPRESSION_EQUAL s e2 (EL n1 c1)` THENL [ 2324 FULL_SIMP_TAC std_ss [SF_SEM___sf_ls_THM, LET_THM, DS_EXPRESSION_EQUAL_def, 2325 FUNION_FEMPTY_1, FDOM_FEMPTY, DISJOINT_EMPTY], 2326 2327 2328 FULL_SIMP_TAC std_ss [SF_SEM___sf_ls_THM, LET_THM, DS_EXPRESSION_EQUAL_def] THEN 2329 SIMP_TAC std_ss [SF_SEM___sf_points_to_THM, DS_POINTS_TO_def] THEN 2330 REPEAT STRIP_TAC THEN 2331 `~(GET_DSV_VALUE (DS_EXPRESSION_EVAL s (EL n1 c1)) IN FDOM h)` by ( 2332 FULL_SIMP_TAC std_ss [HEAP_DISTINCT_def] THEN 2333 METIS_TAC[MEM_EL] 2334 ) THEN 2335 Cases_on `h = FUNION h1 h2` THEN ASM_REWRITE_TAC[] THEN 2336 FULL_SIMP_TAC std_ss [FDOM_FUNION, IN_UNION] 2337]); 2338 2339 2340 2341 2342 2343val INFERENCE___NON_EMPTY_LS___EVAL = store_thm ("INFERENCE___NON_EMPTY_LS___EVAL", 2344``!n1 n2 n3 b e1 e2 e3 f a c1 c2 pfL sfL pfL' sfL'. 2345 ((SAFE_DEL_EL n1 sfL' = [sf_ls f e1 e3]) /\ 2346 (SAFE_DEL_EL n2 pfL = [if b then pf_unequal e1 e3 else pf_unequal e3 e1]) /\ 2347 (SAFE_DEL_EL n3 sfL = [sf_points_to e1 a]) /\ 2348 (MEM (f,e2) a) /\ ALL_DISTINCT (MAP FST a)) ==> 2349 2350 (LIST_DS_ENTAILS (c1, c2) (pfL, sfL) (pfL', sfL') = 2351 LIST_DS_ENTAILS (e1::c1, c2) (pfL, DELETE_ELEMENT n3 sfL) (pfL', (sf_ls f e2 e3)::DELETE_ELEMENT n1 sfL'))``, 2352 2353 2354SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 2355REPEAT STRIP_TAC THEN 2356`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 2357 LIST_DS_ENTAILS (c1, c2) (pfL,SWAP_TO_POS 0 n3 sfL) (pfL',SWAP_TO_POS 0 n1 sfL')` by ( 2358 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 2359 SIMP_TAC std_ss [PERM_REFL] THEN 2360 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2361) THEN 2362`!c1 c2 sfL pfL' sfL'. 2363 LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 2364 LIST_DS_ENTAILS (c1, c2) (SWAP_TO_POS 0 n2 pfL,sfL) (pfL',sfL')` by ( 2365 REPEAT GEN_TAC THEN 2366 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 2367 SIMP_TAC std_ss [PERM_REFL] THEN 2368 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2369) THEN 2370`!c1 c2 pfL sfL pfL' sfL'. 2371 LIST_DS_ENTAILS (c1, c2) ((if b then pf_unequal e1 e3 else pf_unequal e3 e1)::pfL,sfL) (pfL',sfL') = 2372 LIST_DS_ENTAILS (c1, c2) (pf_unequal e1 e3::pfL,sfL) (pfL',sfL')` by ( 2373 REPEAT GEN_TAC THEN 2374 SIMP_TAC std_ss [LIST_DS_ENTAILS_def, LIST_DS_SEM_THM, COND_RAND, COND_RATOR, 2375 PF_SEM_def, DS_EXPRESSION_EQUAL_def] THEN 2376 METIS_TAC[] 2377) THEN 2378ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 2379 2380MP_TAC (Q.SPECL [`e1`, `e2`, `e3`, `f`, `a`] (GSYM INFERENCE_NON_EMPTY_LS)) THEN 2381ASM_SIMP_TAC list_ss [] THEN STRIP_TAC THEN POP_ASSUM (K ALL_TAC) THEN 2382METIS_TAC[INFERENCE_STAR_INTRODUCTION___points_to]) 2383 2384 2385 2386 2387 2388 2389val INFERENCE___NON_EMPTY_BIN_TREE___EVAL = store_thm ("INFERENCE___NON_EMPTY_BIN_TREE___EVAL", 2390``!n1 n2 e e1 e2 f1 f2 a c1 c2 pfL sfL pfL' sfL'. 2391 ((SAFE_DEL_EL n1 sfL' = [sf_bin_tree (f1,f2) e]) /\ 2392 (SAFE_DEL_EL n2 sfL = [sf_points_to e a]) /\ 2393 (MEM (f1,e1) a) /\ MEM (f2,e2) a /\ ~(f1 = f2) /\ ALL_DISTINCT (MAP FST a)) ==> 2394 2395 (LIST_DS_ENTAILS (c1, c2) (pfL, sfL) (pfL', sfL') = 2396 LIST_DS_ENTAILS (e::c1, c2) (pfL, DELETE_ELEMENT n2 sfL) (pfL', (sf_bin_tree (f1,f2) e1)::(sf_bin_tree (f1,f2) e2)::DELETE_ELEMENT n1 sfL'))``, 2397 2398 2399SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 2400REPEAT STRIP_TAC THEN 2401`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 2402 LIST_DS_ENTAILS (c1, c2) (pfL,SWAP_TO_POS 0 n2 sfL) (pfL',SWAP_TO_POS 0 n1 sfL')` by ( 2403 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 2404 SIMP_TAC std_ss [PERM_REFL] THEN 2405 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2406) THEN 2407ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 2408 2409MP_TAC (Q.SPECL [`e`, `e1`, `e2`, `f1`, `f2`, `a`] (GSYM INFERENCE_NON_EMPTY_BIN_TREE)) THEN 2410ASM_SIMP_TAC list_ss [] THEN STRIP_TAC THEN POP_ASSUM (K ALL_TAC) THEN 2411METIS_TAC[INFERENCE_STAR_INTRODUCTION___points_to]) 2412 2413 2414 2415 2416val INFERENCE_UNROLL_COLLAPSE_LS___EVAL = store_thm ("INFERENCE_UNROLL_COLLAPSE_LS___EVAL", 2417``!n (e1:('b, 'a) ds_expression) e2 (f:'c) c1 c2 pfL sfL pfL' sfL'. 2418 ((SAFE_DEL_EL n sfL = [sf_ls f e1 e2]) /\ 2419 INFINITE (UNIV:'b set)) ==> 2420 2421 (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') = 2422 (LIST_DS_ENTAILS (c1,c2) (pf_equal e1 e2::pfL,DELETE_ELEMENT n sfL) (pfL',sfL') /\ 2423 (!x. 2424 LIST_DS_ENTAILS (c1,c2) 2425 (pf_unequal e1 e2::pf_unequal (dse_const x) e2::pfL, 2426 sf_points_to e1 [(f,dse_const x)]:: 2427 sf_points_to (dse_const x) [(f,e2)]::DELETE_ELEMENT n sfL) (pfL',sfL'))))``, 2428 2429 2430SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 2431REPEAT STRIP_TAC THEN 2432`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 2433 LIST_DS_ENTAILS (c1, c2) (pfL,SWAP_TO_POS 0 n sfL) (pfL',sfL')` by ( 2434 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 2435 SIMP_TAC std_ss [PERM_REFL] THEN 2436 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2437) THEN 2438ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 2439METIS_TAC [INFERENCE_UNROLL_COLLAPSE_LS]); 2440 2441 2442 2443 2444 2445val INFERENCE_UNROLL_COLLAPSE_PRECONDITION___EVAL = store_thm ("INFERENCE_UNROLL_COLLAPSE_PRECONDITION___EVAL", 2446``!e1 e2 c1 c2 pfL sfL pfL' sfL'. 2447 (LIST_DS_ENTAILS (c1,(e1,e2)::c2) (pfL,sfL) (pfL',sfL')) = 2448 (LIST_DS_ENTAILS (e1::c1,c2) (pf_unequal e1 e2::pfL,sfL) (pfL',sfL') /\ 2449 LIST_DS_ENTAILS (c1,c2) (pf_equal e1 e2::pfL,sfL) (pfL',sfL'))``, 2450 2451SIMP_TAC std_ss [LIST_DS_ENTAILS_def, GSYM FORALL_AND_THM, HEAP_DISTINCT___IND_DEF, 2452 LIST_DS_SEM_THM, PF_SEM_def] THEN 2453METIS_TAC[]); 2454 2455 2456val INFERENCE_UNROLL_COLLAPSE_LS___NON_EMPTY___EVAL = store_thm ("INFERENCE_UNROLL_COLLAPSE_LS___NON_EMPTY___EVAL", 2457``!n n2 b (e1:('b, 'a) ds_expression) e2 (f:'c) c1 c2 pfL sfL pfL' sfL'. 2458 ((SAFE_DEL_EL n sfL = [sf_ls f e1 e2]) /\ 2459 (SAFE_DEL_EL n2 pfL = [if b then pf_unequal e2 e1 else pf_unequal e1 e2]) /\ 2460 INFINITE (UNIV:'b set)) ==> 2461 2462 (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') = 2463 (!x. 2464 LIST_DS_ENTAILS (c1,c2) 2465 (pf_unequal (dse_const x) e2::pfL, 2466 sf_points_to e1 [(f,dse_const x)]:: 2467 sf_points_to (dse_const x) [(f,e2)]::DELETE_ELEMENT n sfL) (pfL',sfL')))``, 2468 2469 2470SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 2471REPEAT STRIP_TAC THEN 2472`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 2473 LIST_DS_ENTAILS (c1, c2) (SWAP_TO_POS 0 n2 pfL,SWAP_TO_POS 0 n sfL) (pfL',sfL')` by ( 2474 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 2475 SIMP_TAC std_ss [PERM_REFL] THEN 2476 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2477) THEN 2478`!sfL pfL' sfL' h. 2479 LIST_DS_ENTAILS (c1, c2) (h::pfL,sfL) (pfL',sfL') = 2480 LIST_DS_ENTAILS (c1, c2) (SWAP_TO_POS 0 (SUC n2) (h::pfL),sfL) (pfL',sfL')` by ( 2481 REPEAT GEN_TAC THEN 2482 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 2483 SIMP_TAC std_ss [PERM_REFL, PERM_CONS_IFF] THEN 2484 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2485) THEN 2486`!pfL sfL sfL' pfL'. 2487 LIST_DS_ENTAILS (c1,c2) ((if b then pf_unequal e2 e1 else pf_unequal e1 e2)::pfL,sfL) (pfL',sfL') = 2488 LIST_DS_ENTAILS (c1,c2) (pf_unequal e1 e2::pfL,sfL) (pfL',sfL')` by ( 2489 REPEAT GEN_TAC THEN 2490 SIMP_TAC std_ss [LIST_DS_ENTAILS_def, LIST_DS_SEM_THM, COND_RAND, COND_RATOR, 2491 PF_SEM_def, DS_EXPRESSION_EQUAL_def] THEN 2492 METIS_TAC[] 2493) THEN 2494ASM_SIMP_TAC list_ss [SWAP_TO_POS___DELETE_ELEMENT, DELETE_ELEMENT_THM] THEN 2495ASM_SIMP_TAC std_ss [GSYM INFERENCE_UNROLL_COLLAPSE_LS___NON_EMPTY]); 2496 2497 2498 2499 2500 2501 2502 2503 2504 2505 2506val INFERENCE_UNROLL_COLLAPSE_BIN_TREE___EVAL = store_thm ("INFERENCE_UNROLL_COLLAPSE_BIN_TREE___EVAL", 2507``!n (e:('b, 'a) ds_expression) (f1:'c) f2 c1 c2 pfL sfL pfL' sfL'. 2508 ((SAFE_DEL_EL n sfL = [sf_bin_tree (f1,f2) e]) /\ ~(f1 = f2) /\ 2509 INFINITE (UNIV:'b set)) ==> 2510 2511 (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') = 2512 (LIST_DS_ENTAILS (c1,c2) (pf_equal e dse_nil::pfL,DELETE_ELEMENT n sfL) (pfL',sfL') /\ 2513 (!x1 x2. 2514 LIST_DS_ENTAILS (c1,c2) 2515 (pf_unequal e dse_nil::pf_unequal (dse_const x1) dse_nil::pf_unequal (dse_const x2) dse_nil::pfL, 2516 sf_points_to e [(f1,dse_const x1);(f2,dse_const x2)]:: 2517 sf_points_to (dse_const x1) [(f1,dse_nil);(f2,dse_nil)]::sf_points_to (dse_const x2) [(f1,dse_nil);(f2,dse_nil)]::DELETE_ELEMENT n sfL) (pfL',sfL'))))``, 2518 2519 2520SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 2521REPEAT STRIP_TAC THEN 2522`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 2523 LIST_DS_ENTAILS (c1, c2) (pfL,SWAP_TO_POS 0 n sfL) (pfL',sfL')` by ( 2524 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 2525 SIMP_TAC std_ss [PERM_REFL] THEN 2526 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2527) THEN 2528ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 2529METIS_TAC [INFERENCE_UNROLL_COLLAPSE_BIN_TREE]); 2530 2531 2532 2533 2534 2535val INFERENCE_APPEND_LIST___nil___EVAL = store_thm ("INFERENCE_APPEND_LIST___nil___EVAL", 2536``!n1 n2 (e1:('b, 'a) ds_expression) e2 f c1 c2 pfL sfL pfL' sfL'. 2537 ((SAFE_DEL_EL n1 sfL = [sf_ls f e1 e2]) /\ 2538 (SAFE_DEL_EL n2 sfL' = [sf_ls f e1 dse_nil]) /\ 2539 INFINITE (UNIV:'b set)) ==> 2540 2541 (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') = 2542 (LIST_DS_ENTAILS (c1,(e1,e2)::c2) (pfL,DELETE_ELEMENT n1 sfL) (pfL',sf_ls f e2 dse_nil::DELETE_ELEMENT n2 sfL')))``, 2543 2544 2545SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 2546REPEAT STRIP_TAC THEN 2547`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 2548 LIST_DS_ENTAILS (c1, c2) (pfL,SWAP_TO_POS 0 n1 sfL) (pfL',SWAP_TO_POS 0 n2 sfL')` by ( 2549 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 2550 SIMP_TAC std_ss [PERM_REFL] THEN 2551 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2552) THEN 2553ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT, 2554 GSYM INFERENCE_APPEND_LIST___nil, 2555 GSYM INFERENCE_STAR_INTRODUCTION___list]); 2556 2557 2558 2559 2560 2561val INFERENCE_APPEND_LIST___precond___EVAL = store_thm ("INFERENCE_APPEND_LIST___precond___EVAL", 2562``!n1 n2 (e1:('b, 'a) ds_expression) e2 f e3 n3 n4 b c1 c2 pfL sfL pfL' sfL'. 2563 ((SAFE_DEL_EL n1 sfL = [sf_ls f e1 e2]) /\ 2564 (SAFE_DEL_EL n2 sfL' = [sf_ls f e1 e3]) /\ 2565 (SAFE_DEL_EL n4 pfL = [if b then pf_unequal e3 e1 else pf_unequal e1 e3]) /\ 2566 (SAFE_DEL_EL n3 c1 = [e3]) /\ 2567 INFINITE (UNIV:'b set)) ==> 2568 2569 (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') = 2570 (LIST_DS_ENTAILS (c1,(e1,e2)::c2) (pfL,DELETE_ELEMENT n1 sfL) (pfL',sf_ls f e2 e3::DELETE_ELEMENT n2 sfL')))``, 2571 2572 2573REPEAT STRIP_TAC THEN 2574FULL_SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 2575`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 2576 LIST_DS_ENTAILS (c1, c2) (pfL,SWAP_TO_POS 0 n1 sfL) (pfL',SWAP_TO_POS 0 n2 sfL')` by ( 2577 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 2578 SIMP_TAC std_ss [PERM_REFL] THEN 2579 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2580) THEN 2581`!c2 pfL sfL pfL' sfL'. 2582 LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 2583 LIST_DS_ENTAILS (SWAP_TO_POS 0 n3 c1, c2) (pfL,sfL) (pfL',sfL')` by ( 2584 REPEAT GEN_TAC THEN 2585 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 2586 SIMP_TAC std_ss [PERM_REFL] THEN 2587 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2588) THEN 2589`MEM_UNEQ_PF_LIST e1 e3 pfL` by ( 2590 SIMP_TAC std_ss [MEM_UNEQ_PF_LIST_def] THEN 2591 METIS_TAC[MEM_EL] 2592) THEN 2593ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT, 2594 GSYM INFERENCE_APPEND_LIST___precond, 2595 GSYM INFERENCE_STAR_INTRODUCTION___list]); 2596 2597 2598 2599 2600val INFERENCE_APPEND_LIST___points_to___EVAL = store_thm ("INFERENCE_APPEND_LIST___points_to___EVAL", 2601``!n1 n2 (e1:('b, 'a) ds_expression) e2 f e3 n3 a n4 b c1 c2 pfL sfL pfL' sfL'. 2602 ((SAFE_DEL_EL n1 sfL = [sf_ls f e1 e2]) /\ 2603 (SAFE_DEL_EL n2 sfL' = [sf_ls f e1 e3]) /\ 2604 (SAFE_DEL_EL n3 sfL = [sf_points_to e3 a]) /\ 2605 (SAFE_DEL_EL n4 pfL = [if b then pf_unequal e3 e1 else pf_unequal e1 e3]) /\ 2606 INFINITE (UNIV:'b set)) ==> 2607 2608 (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') = 2609 (LIST_DS_ENTAILS (c1,(e1,e2)::c2) (pfL,DELETE_ELEMENT n1 sfL) (pfL',sf_ls f e2 e3::DELETE_ELEMENT n2 sfL')))``, 2610 2611 2612SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 2613REPEAT STRIP_TAC THEN 2614`?sfL''. PERM (EL n1 sfL::EL n3 sfL::sfL'') sfL /\ 2615 PERM (EL n3 sfL::sfL'') (DELETE_ELEMENT n1 sfL)` by ( 2616 MATCH_MP_TAC PERM___TWO_ELEMENTS_TO_FRONT_3 THEN 2617 ASM_SIMP_TAC std_ss [] THEN 2618 CCONTR_TAC THEN 2619 FULL_SIMP_TAC std_ss [ds_spatial_formula_distinct, sf_ls_def] 2620) THEN 2621 2622`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 2623 LIST_DS_ENTAILS (c1, c2) (pfL,EL n1 sfL::EL n3 sfL::sfL'') (pfL',SWAP_TO_POS 0 n2 sfL')` by ( 2624 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 2625 SIMP_TAC std_ss [PERM_REFL] THEN 2626 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2627) THEN 2628ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 2629 2630`MEM_UNEQ_PF_LIST e1 e3 pfL` by ( 2631 SIMP_TAC std_ss [MEM_UNEQ_PF_LIST_def] THEN 2632 METIS_TAC[MEM_EL] 2633) THEN 2634ASM_SIMP_TAC std_ss [GSYM INFERENCE_APPEND_LIST___points_to, 2635 GSYM INFERENCE_STAR_INTRODUCTION___list] THEN 2636 2637MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 2638SIMP_TAC std_ss [PERM_REFL] THEN 2639METIS_TAC[]); 2640 2641 2642 2643 2644 2645val INFERENCE_APPEND_LIST___tree___EVAL = store_thm ("INFERENCE_APPEND_LIST___tree___EVAL", 2646``!n1 n2 (e1:('b, 'a) ds_expression) e2 n3 e3 fL es n4 b1 n5 b2 f c1 c2 pfL sfL pfL' sfL'. 2647 ((SAFE_DEL_EL n1 sfL = [sf_ls f e1 e2]) /\ 2648 (SAFE_DEL_EL n2 sfL' = [sf_ls f e1 e3]) /\ 2649 (SAFE_DEL_EL n3 sfL = [sf_tree fL es e3]) /\ 2650 (~(n3 = n1)) /\ 2651 (SAFE_DEL_EL n4 pfL = [if b1 then pf_unequal e3 e1 else pf_unequal e1 e3]) /\ 2652 (SAFE_DEL_EL n5 pfL = [if b2 then pf_unequal es e3 else pf_unequal e3 es]) /\ 2653 INFINITE (UNIV:'b set)) ==> 2654 2655 (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') = 2656 (LIST_DS_ENTAILS (c1,(e1,e2)::c2) (pfL,DELETE_ELEMENT n1 sfL) (pfL',sf_ls f e2 e3::DELETE_ELEMENT n2 sfL')))``, 2657 2658 2659SIMP_TAC std_ss [SAFE_DEL_EL___EQ] THEN 2660REPEAT STRIP_TAC THEN 2661`?sfL''. PERM (EL n1 sfL::EL n3 sfL::sfL'') sfL /\ 2662 PERM (EL n3 sfL::sfL'') (DELETE_ELEMENT n1 sfL)` by ( 2663 MATCH_MP_TAC PERM___TWO_ELEMENTS_TO_FRONT_3 THEN 2664 ASM_SIMP_TAC std_ss [] 2665) THEN 2666 2667`LIST_DS_ENTAILS (c1, c2) (pfL,sfL) (pfL',sfL') = 2668 LIST_DS_ENTAILS (c1, c2) (pfL,EL n1 sfL::EL n3 sfL::sfL'') (pfL',SWAP_TO_POS 0 n2 sfL')` by ( 2669 MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 2670 SIMP_TAC std_ss [PERM_REFL] THEN 2671 METIS_TAC[PERM___SWAP_TO_POS, PERM_SYM] 2672) THEN 2673ASM_SIMP_TAC std_ss [SWAP_TO_POS___DELETE_ELEMENT] THEN 2674 2675`MEM_UNEQ_PF_LIST e1 e3 pfL /\ MEM_UNEQ_PF_LIST e3 es pfL` by ( 2676 SIMP_TAC std_ss [MEM_UNEQ_PF_LIST_def] THEN 2677 METIS_TAC[MEM_EL] 2678) THEN 2679ASM_SIMP_TAC std_ss [GSYM INFERENCE_APPEND_LIST___tree, 2680 GSYM INFERENCE_STAR_INTRODUCTION___list] THEN 2681 2682MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN 2683SIMP_TAC std_ss [PERM_REFL] THEN 2684METIS_TAC[]); 2685 2686 2687 2688 2689 2690(* 2691 2692 2693 2694val FINITE_DISTINCT_STACK_EXISTS_THM = store_thm ("FINITE_DISTINCT_STACK_EXISTS_THM", 2695 ``(INFINITE (UNIV:'b set)) ==> 2696 !eL. (FINITE (eL:('b, 'a) ds_expression set)) ==> ( 2697 !X. FINITE X ==> 2698 ?s. (!e. (e IN eL) ==> (IS_DSV_NIL (DS_EXPRESSION_EVAL s e) = (e = dse_nil))) /\ 2699 (!v. (dse_var v IN eL) ==> ~(GET_DSV_VALUE (s v) IN X)) /\ 2700 (!e1 e2. (e1 IN eL /\ e2 IN eL) ==> ( 2701 DS_EXPRESSION_EQUAL s e1 e2 = (e1 = e2))))``, 2702 2703 2704STRIP_TAC THEN 2705pred_setLib.SET_INDUCT_TAC THENL [ 2706 SIMP_TAC list_ss [NOT_IN_EMPTY], 2707 2708 Cases_on `e` THENL [ 2709 GEN_TAC THEN 2710 Q.PAT_X_ASSUM `!X. P X` (fn thm => ASSUME_TAC(Q.SPEC `GET_DSV_VALUE d INSERT X` thm)) THEN 2711 STRIP_TAC THEN 2712 FULL_SIMP_TAC std_ss [FINITE_INSERT] THEN 2713 Q.EXISTS_TAC `s'` THEN 2714 FULL_SIMP_TAC std_ss [IN_INSERT, FORALL_AND_THM, DISJ_IMP_THM, FORALL_AND_THM, 2715 LEFT_AND_OVER_OR, RIGHT_AND_OVER_OR, dse_nil_def, DS_EXPRESSION_EQUAL_def, 2716 ds_value_11, DS_EXPRESSION_EVAL_def, ds_expression_11, ds_value_distinct, 2717 ds_expression_distinct, IN_INSERT, IS_DSV_NIL_THM] THEN 2718 SIMP_TAC std_ss [GSYM FORALL_AND_THM] THEN 2719 Cases_on `e1` THENL [ 2720 SIMP_TAC std_ss [DS_EXPRESSION_EVAL_def, ds_expression_11], 2721 2722 SIMP_TAC std_ss [DS_EXPRESSION_EVAL_def, ds_expression_distinct] THEN 2723 METIS_TAC[] 2724 ], 2725 2726 2727 GEN_TAC THEN 2728 Q.PAT_X_ASSUM `!X. P X` (fn thm => ASSUME_TAC(Q.SPEC `X` thm)) THEN 2729 STRIP_TAC THEN 2730 FULL_SIMP_TAC std_ss [] THEN 2731 2732 `?c. ~(c IN (X UNION (IMAGE (DS_EXPRESSION_EVAL_VALUE s') s)))` by 2733 METIS_TAC[NOT_IN_FINITE, IMAGE_FINITE, 2734 FINITE_UNION] THEN 2735 2736 Q.EXISTS_TAC `\x. if (x = v) then dsv_const c else s' x` THEN 2737 ASM_SIMP_TAC std_ss [IN_INSERT, FORALL_AND_THM, DISJ_IMP_THM, FORALL_AND_THM, 2738 LEFT_AND_OVER_OR, RIGHT_AND_OVER_OR] THEN 2739 FULL_SIMP_TAC std_ss [IS_DSV_NIL_THM, DS_EXPRESSION_EQUAL_def, DS_EXPRESSION_EVAL_def, 2740 dse_nil_def, ds_value_distinct, ds_expression_distinct, ds_expression_11, 2741 GET_DSV_VALUE_def] THEN 2742 REPEAT STRIP_TAC THENL [ 2743 `((DS_EXPRESSION_EVAL s' e = dsv_nil) = (e = dse_const dsv_nil))` by METIS_TAC[] THEN 2744 Cases_on `e` THENL [ 2745 SIMP_TAC std_ss [DS_EXPRESSION_EVAL_def, ds_expression_11], 2746 2747 `~(v' = v)` by METIS_TAC[] THEN 2748 FULL_SIMP_TAC std_ss [DS_EXPRESSION_EVAL_def] 2749 ], 2750 2751 2752 FULL_SIMP_TAC std_ss [IN_UNION], 2753 METIS_TAC[], 2754 2755 2756 Cases_on `e2` THENL [ 2757 SIMP_TAC list_ss [DS_EXPRESSION_EVAL_def, ds_expression_distinct] THEN 2758 FULL_SIMP_TAC std_ss [IN_UNION, IN_IMAGE, DS_EXPRESSION_EVAL_VALUE_def] THEN 2759 `~(c = GET_DSV_VALUE (DS_EXPRESSION_EVAL s' (dse_const d)))` by METIS_TAC[] THEN 2760 FULL_SIMP_TAC std_ss [DS_EXPRESSION_EVAL_def] THEN 2761 Cases_on `d` THENL [ 2762 SIMP_TAC list_ss [ds_value_distinct], 2763 FULL_SIMP_TAC std_ss [GET_DSV_VALUE_def, ds_value_11] 2764 ], 2765 2766 `~(v'=v)` by METIS_TAC[] THEN 2767 ASM_SIMP_TAC std_ss [DS_EXPRESSION_EVAL_def, ds_expression_11] THEN 2768 FULL_SIMP_TAC std_ss [IN_UNION, IN_IMAGE, DS_EXPRESSION_EVAL_VALUE_def] THEN 2769 `~(c = GET_DSV_VALUE (DS_EXPRESSION_EVAL s' (dse_var v')))` by METIS_TAC[] THEN 2770 FULL_SIMP_TAC std_ss [DS_EXPRESSION_EVAL_def] THEN 2771 Cases_on `s' v'` THENL [ 2772 SIMP_TAC list_ss [ds_value_distinct], 2773 FULL_SIMP_TAC std_ss [GET_DSV_VALUE_def, ds_value_11] 2774 ] 2775 ], 2776 2777 2778 Cases_on `e1` THENL [ 2779 SIMP_TAC list_ss [DS_EXPRESSION_EVAL_def, ds_expression_distinct] THEN 2780 FULL_SIMP_TAC std_ss [IN_UNION, IN_IMAGE, DS_EXPRESSION_EVAL_VALUE_def] THEN 2781 `~(c = GET_DSV_VALUE (DS_EXPRESSION_EVAL s' (dse_const d)))` by METIS_TAC[] THEN 2782 FULL_SIMP_TAC std_ss [DS_EXPRESSION_EVAL_def] THEN 2783 Cases_on `d` THENL [ 2784 SIMP_TAC list_ss [ds_value_distinct], 2785 FULL_SIMP_TAC std_ss [GET_DSV_VALUE_def, ds_value_11] 2786 ], 2787 2788 `~(v'=v)` by METIS_TAC[] THEN 2789 ASM_SIMP_TAC std_ss [DS_EXPRESSION_EVAL_def, ds_expression_11] THEN 2790 FULL_SIMP_TAC std_ss [IN_UNION, IN_IMAGE, DS_EXPRESSION_EVAL_VALUE_def] THEN 2791 `~(c = GET_DSV_VALUE (DS_EXPRESSION_EVAL s' (dse_var v')))` by METIS_TAC[] THEN 2792 FULL_SIMP_TAC std_ss [DS_EXPRESSION_EVAL_def] THEN 2793 Cases_on `s' v'` THENL [ 2794 SIMP_TAC list_ss [ds_value_distinct], 2795 FULL_SIMP_TAC std_ss [GET_DSV_VALUE_def, ds_value_11] 2796 ] 2797 ], 2798 2799 `!e. e IN s ==> 2800 (DS_EXPRESSION_EVAL (\x. (if x = v then dsv_const c else s' x)) e = 2801 DS_EXPRESSION_EVAL s' e)` by ( 2802 REPEAT STRIP_TAC THEN 2803 Cases_on `e` THENL [ 2804 SIMP_TAC std_ss [DS_EXPRESSION_EVAL_def], 2805 2806 `~(v' = v)` by METIS_TAC[] THEN 2807 ASM_SIMP_TAC std_ss [DS_EXPRESSION_EVAL_def] 2808 ] 2809 ) THEN 2810 FULL_SIMP_TAC std_ss [] 2811 ] 2812 ] 2813]); 2814 2815 2816 2817 2818 2819val FINITE_DISTINCT_STACK_EXISTS_THM2 = store_thm ("FINITE_DISTINCT_STACK_EXISTS_THM2", 2820 ``!eL. (FINITE (eL:('b, 'a) ds_expression set) /\ (INFINITE (UNIV:'b set))) ==> 2821 ?s. (!e. (e IN eL) ==> (IS_DSV_NIL (DS_EXPRESSION_EVAL s e) = (e = dse_nil))) /\ 2822 (!e1 e2. (e1 IN eL /\ e2 IN eL) ==> ( 2823 DS_EXPRESSION_EQUAL s e1 e2 = (e1 = e2)))``, 2824 2825REPEAT STRIP_TAC THEN 2826METIS_TAC[FINITE_EMPTY, FINITE_DISTINCT_STACK_EXISTS_THM]); 2827 2828 2829 2830 2831 2832val PF_IS_WELL_FORMED_UNEQUAL_def = Define ` 2833 (SF_IS_WELL_FORMED_UNEQUAL (pf_unequal e1 e2) = ~(e1 = e2)) /\ 2834 (SF_IS_WELL_FORMED_UNEQUAL _ = F)`; 2835 2836val SF_IS_WELL_FORMED_POINTSTO_def = Define ` 2837 (SF_IS_WELL_FORMED_POINTSTO (sf_points_to e a) = 2838 ALL_DISTINCT (MAP FST a)) /\ 2839 (SF_IS_WELL_FORMED_POINTSTO _ = F)`; 2840 2841val LIST_DS_ENTAILS___IS_SIMPLE_LHS_def = Define 2842 `LIST_DS_ENTAILS___IS_SIMPLE_LHS c1 pfL sfL = 2843 (ALL_DISTINCT c1 /\ 2844 EVERY PF_IS_WELL_FORMED_UNEQUAL pfL /\ 2845 EVERY SF_IS_WELL_FORMED_POINTSTO sfL /\ 2846 ALL_DISTINCT (SF_POINTS_TO_LIST sfL) /\ 2847 EVERY (\x. ~(MEM x (SF_POINTS_TO_LIST sfL))) c1)` 2848 2849 2850 2851DB.find "SF_POINTS_TO_LIST_def" 2852 2853 2854 2855 2856*) 2857 2858val _ = export_theory(); 2859