1open HolKernel boolLib bossLib Parse; val _ = new_theory "stop_and_copy"; 2 3open pred_setTheory arithmeticTheory pairTheory listTheory combinTheory; 4open finite_mapTheory sumTheory relationTheory; 5 6infix \\ 7val op \\ = op THEN; 8val RW = REWRITE_RULE; 9val RW1 = ONCE_REWRITE_RULE; 10fun SUBGOAL q = REVERSE (sg q) 11fun ALPHA_TAC s = let 12 fun my_alpha_conv tm = 13 ALPHA_CONV (mk_var(s,type_of (fst(dest_abs tm)))) tm 14 in CONV_TAC (RAND_CONV my_alpha_conv) end; 15 16 17 18val _ = Hol_datatype `heap_address = H_ADDR of num | H_DATA of 'a`; 19val heap_address_11 = fetch "-" "heap_address_11"; 20val heap_address_distinct = fetch "-" "heap_address_distinct"; 21 22val _ = type_abbrev("abs_heap",``:(num |-> ('b heap_address) list # 'a) # 23 (num set) # (num set) # (num set) # (num -> num)``); 24 25val ADDR_MAP_def = Define ` 26 (ADDR_MAP f [] = []) /\ 27 (ADDR_MAP f (H_ADDR x::xs) = H_ADDR (f x) :: ADDR_MAP f xs) /\ 28 (ADDR_MAP f (H_DATA y::xs) = H_DATA y :: ADDR_MAP f xs)`; 29 30val IN_THM = SIMP_RULE std_ss [EXTENSION,GSPECIFICATION] 31val ADDR_SET_def = (IN_THM o Define) `ADDR_SET s = { x | MEM (H_ADDR x) s }`; 32 33val (gc_reachable_rules,gc_reachable_ind,gc_reachable_cases) = Hol_reln ` 34 (!h roots x. 35 x IN ADDR_SET roots ==> gc_reachable (h,roots) x) /\ 36 (!h roots x a xs d. 37 a IN FDOM h /\ (h ' a = (xs,d)) /\ x IN ADDR_SET xs /\ gc_reachable (h,roots) a ==> 38 gc_reachable (h,roots) x)`; 39 40val PAIR_TRANSLATE_def = Define `PAIR_TRANSLATE f (xs,a) = (ADDR_MAP f xs,a)`; 41val SET_TRANSLATE_def = (IN_THM o Define) `SET_TRANSLATE f s = { x | (f x) IN s }`; 42val HAS_CHANGED_def = (IN_THM o Define) `HAS_CHANGED f = { x | ~(f x = x) }`; 43val POINTERS_def = (IN_THM o Define) `POINTERS h y = 44 { a | ?b zs d. b IN y /\ b IN FDOM h /\ (h ' b = (zs,d)) /\ a IN ADDR_SET zs }`; 45 46val gc_filter_def = Define ` 47 gc_filter (h,roots) = (DRESTRICT h (gc_reachable (h,roots)),roots)`; 48 49val gc_copy_def = Define ` 50 gc_copy (h1,roots1) (h2,roots2) = 51 ?f. (f o f = I) /\ (FDOM h1 = SET_TRANSLATE f (FDOM h2)) /\ 52 (roots2 = ADDR_MAP f roots1) /\ 53 !x. x IN FDOM h1 ==> (h1 ' x = PAIR_TRANSLATE f (h2 ' (f x)))`; 54 55val gc_exec_def = Define `gc_exec x y = gc_copy (gc_filter x) y`; 56 57val (abs_step_rules,abs_step_ind,abs_step_cases) = Hol_reln ` 58 (!h x y z f a. 59 a IN z /\ ~(f a = a) ==> 60 abs_step (h,x,y,z,f) (h,x,y,z DELETE a,f)) /\ 61 (!h x y z f a xs d. 62 a IN y /\ (h ' a = (xs,d)) /\ (!b. b IN ADDR_SET xs ==> ~(f b = b)) ==> 63 abs_step (h,x,y,z,f) (h |+ (a,ADDR_MAP f xs,d),a INSERT x,y DELETE a,z,f)) /\ 64 (!h x y z f a b xs d. 65 a IN z /\ (f a = a) /\ (f b = b) /\ ~(b IN FDOM h) /\ a IN FDOM h /\ (h ' a = (xs,d)) ==> 66 abs_step (h,x,y,z,f) (h |+ (b,xs,d) \\ a,x,b INSERT y,z UNION (ADDR_SET xs),(a =+ b) ((b =+ a) f)))`; 67 68val abs_steps_def = Define `abs_steps = RTC abs_step`; 69 70val abs_steps_TRANS = store_thm("abs_steps_TRANS", 71 ``!x y z. abs_steps x y /\ abs_steps y z ==> abs_steps x z``, 72 METIS_TAC [abs_steps_def,RTC_RTC]); 73 74val (abs_gc_rules,abs_gc_ind,abs_gc_cases) = Hol_reln ` 75 (!h roots h2 f x. 76 abs_steps (h,{},{},ADDR_SET roots,I) (h2,x,{},{},f) ==> 77 abs_gc (h,roots) (DRESTRICT h2 x,ADDR_MAP f roots))`; 78 79val abs_gc_inv_def = Define ` 80 abs_gc_inv (h1,roots1) (h,x,y,z,f) = 81 let old = FDOM h UNION HAS_CHANGED f DIFF (x UNION y) in 82 DISJOINT x y /\ 83 POINTERS h x SUBSET (x UNION y) /\ 84 POINTERS h (UNIV DIFF x) SUBSET old /\ 85 POINTERS h y UNION ADDR_SET roots1 SUBSET SET_TRANSLATE f (x UNION y) UNION z /\ 86 SET_TRANSLATE f (x UNION y) UNION z SUBSET gc_reachable (h1,roots1) /\ 87 (!a. a IN z ==> if f a = a then a IN old else f a IN x UNION y) /\ 88 (!a. ~(f a = a) ==> ~(a IN x UNION y = f a IN x UNION y)) /\ 89 (!a. a IN y \/ a IN x = ~(f a = a) /\ a IN FDOM h) /\ (f o f = I) /\ 90 (SET_TRANSLATE f (FDOM h) = FDOM h1) /\ 91 (!d. d IN FDOM h1 ==> 92 (h1 ' d = if (f d) IN x then PAIR_TRANSLATE f (h ' (f d)) else h ' (f d)))`; 93 94val SET_TAC = 95 FULL_SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_UNION,IN_DELETE,SUBSET_DEF, 96 DISJOINT_DEF,NOT_IN_EMPTY,EXTENSION,IN_INSERT,IN_INTER,IN_DIFF,IN_UNIV] 97 \\ METIS_TAC [PAIR_EQ]; 98 99val SET2_TAC = 100 FULL_SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_UNION,IN_DELETE,SUBSET_DEF, 101 DISJOINT_DEF,NOT_IN_EMPTY,EXTENSION,IN_INSERT,IN_INTER,IN_DIFF,IN_UNIV, 102 POINTERS_def,HAS_CHANGED_def,SET_TRANSLATE_def,FDOM_FUPDATE, 103 FDOM_DOMSUB,FAPPLY_FUPDATE_THM,DOMSUB_FAPPLY_THM] \\ SET_TAC; 104 105val POINTERS_IGNORE = prove( 106 ``~(a IN x) ==> (POINTERS (h |+ (a,xs,d)) x = POINTERS h x) /\ 107 (POINTERS (h \\ a) x = POINTERS h x)``, 108 SET2_TAC); 109 110val set_SUBSET_POINTERS = prove( 111 ``(h ' a = (xs,d)) /\ a IN FDOM h /\ a IN x ==> ADDR_SET xs SUBSET POINTERS h x``, 112 SET2_TAC); 113 114val POINTER_FUPDATE_EQ = store_thm("POINTER_FUPDATE_EQ", 115 ``~(b IN FDOM h) /\ b IN x ==> 116 (POINTERS (h |+ (b,xs,d)) x = POINTERS h x UNION ADDR_SET xs)``, 117 SET2_TAC); 118 119val POINTERS_FUPDATE = prove( 120 ``POINTERS (h |+ (b,xs,d)) (b INSERT y) SUBSET POINTERS h y UNION ADDR_SET xs``, 121 SET2_TAC); 122 123val POINTERS_SUBSET = prove( 124 ``!h x y. x SUBSET y ==> POINTERS h x SUBSET POINTERS h y``, 125 SET2_TAC); 126 127val POINTERS_DOMSUB = prove( 128 ``!h y. POINTERS (h \\ a) y SUBSET POINTERS h y``, 129 SET2_TAC); 130 131val SET_TRANSLATE_SUBSET = prove( 132 ``!f x y. (f o f = I) ==> 133 (SET_TRANSLATE f x SUBSET y = x SUBSET SET_TRANSLATE f y)``, 134 SIMP_TAC std_ss [FUN_EQ_THM] \\ SET2_TAC); 135 136val SET_TRANSLATE_MAP = prove( 137 ``!xs f. (f o f = I) ==> (ADDR_SET (ADDR_MAP f xs) = SET_TRANSLATE f (ADDR_SET xs))``, 138 SIMP_TAC std_ss [EXTENSION,ADDR_SET_def,SET_TRANSLATE_def] 139 \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ Induct 140 \\ ASM_SIMP_TAC std_ss [ADDR_MAP_def,MEM] \\ Cases 141 \\ ASM_SIMP_TAC std_ss [ADDR_MAP_def,MEM,heap_address_11,heap_address_distinct] 142 \\ SET2_TAC); 143 144val SET_TRANSLATE_THM = prove( 145 ``(f o f = I) ==> 146 (SET_TRANSLATE f (x UNION y) = (SET_TRANSLATE f x) UNION (SET_TRANSLATE f y)) /\ 147 (SET_TRANSLATE f (x INTER y) = (SET_TRANSLATE f x) INTER (SET_TRANSLATE f y)) /\ 148 (SET_TRANSLATE f (a INSERT x) = (f a) INSERT (SET_TRANSLATE f x)) /\ 149 (SET_TRANSLATE f (SET_TRANSLATE f x) = x)``, 150 SIMP_TAC std_ss [EXTENSION] \\ SIMP_TAC std_ss [FUN_EQ_THM] \\ SET2_TAC); 151 152val SET_TRANSLATE_IGNORE = prove( 153 ``(f o f = I) /\ (f a = a) /\ (f b = b) /\ ~(a IN x) /\ ~(b IN x) ==> 154 (SET_TRANSLATE ((a =+ b) ((b =+ a) f)) x = SET_TRANSLATE f x)``, 155 SIMP_TAC std_ss [EXTENSION] \\ SIMP_TAC std_ss [FUN_EQ_THM,APPLY_UPDATE_THM, 156 SET_TRANSLATE_def] \\ SET2_TAC); 157 158val ADDR_MAP_ADDR_MAP = store_thm("ADDR_MAP_ADDR_MAP", 159 ``!xs f. (f o f = I) ==> (ADDR_MAP f (ADDR_MAP f xs) = xs)``, 160 Induct \\ SIMP_TAC std_ss [ADDR_MAP_def] \\ Cases 161 \\ ASM_SIMP_TAC std_ss [ADDR_MAP_def,FUN_EQ_THM]); 162 163val ADDR_MAP_EQ_ADDR_MAP = prove( 164 ``!xs f g. (ADDR_MAP f xs = ADDR_MAP g xs) = !x. x IN ADDR_SET xs ==> (f x = g x)``, 165 Induct \\ SIMP_TAC std_ss [ADDR_MAP_def,ADDR_SET_def,MEM] 166 \\ Cases \\ FULL_SIMP_TAC std_ss [ADDR_MAP_def,ADDR_SET_def,MEM,CONS_11, 167 heap_address_11,heap_address_distinct] \\ SET_TAC); 168 169val abs_step_thm = prove( 170 ``!s1 s2. abs_step s1 s2 /\ abs_gc_inv (h0,r0) s1 ==> abs_gc_inv (h0,r0) s2``, 171 REPEAT STRIP_TAC \\ Q.PAT_X_ASSUM `abs_step s1 s1i` ASSUME_TAC 172 \\ FULL_SIMP_TAC std_ss [abs_step_cases] 173 THEN1 (FULL_SIMP_TAC std_ss [abs_gc_inv_def,IN_UNION,IN_DELETE,LET_DEF] 174 \\ `f a IN x UNION y` by SET_TAC 175 \\ SUBGOAL `a IN SET_TRANSLATE f (x UNION y)` THEN1 SET_TAC \\ SET2_TAC) 176 THEN1 177 (FULL_SIMP_TAC std_ss [abs_gc_inv_def,IN_UNION,IN_DELETE,FDOM_FUPDATE,LET_DEF] 178 \\ `a INSERT FDOM h = FDOM h` by SET_TAC \\ ASM_SIMP_TAC std_ss [IN_INSERT] 179 \\ `~(a IN x) /\ ~(a IN (FDOM h UNION HAS_CHANGED f DIFF (a INSERT x)))` by SET_TAC 180 \\ ASM_SIMP_TAC std_ss [POINTERS_IGNORE] \\ STRIP_TAC THEN1 SET_TAC 181 \\ `(a INSERT x) UNION (y DELETE a) UNION z = x UNION y UNION z` by SET_TAC 182 \\ `(a INSERT x) UNION (y DELETE a) = x UNION y` by SET_TAC 183 \\ ASM_SIMP_TAC std_ss [] 184 \\ REVERSE (REPEAT STRIP_TAC) THEN1 185 (Cases_on `f d' = a` \\ ASM_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM,IN_INSERT] 186 \\ `~(a IN x)` by SET_TAC 187 \\ ASM_SIMP_TAC std_ss [PAIR_TRANSLATE_def,ADDR_MAP_ADDR_MAP]) 188 THEN1 SET_TAC THEN1 SET_TAC THEN1 SET_TAC THEN1 SET2_TAC THEN1 SET2_TAC 189 \\ MATCH_MP_TAC (MATCH_MP (RW [GSYM AND_IMP_INTRO] SUBSET_TRANS) (SPEC_ALL POINTERS_FUPDATE)) 190 \\ ASM_SIMP_TAC std_ss [UNION_SUBSET] \\ `a IN FDOM h` by SET_TAC 191 \\ IMP_RES_TAC set_SUBSET_POINTERS \\ POP_ASSUM (K ALL_TAC) 192 \\ ASM_SIMP_TAC std_ss [SET_TRANSLATE_MAP,SET_TRANSLATE_SUBSET] \\ SET2_TAC) 193 THEN1 194 (FULL_SIMP_TAC std_ss [abs_gc_inv_def,IN_UNION,IN_DELETE,FDOM_FUPDATE,IN_INSERT,LET_DEF] 195 \\ `~(a IN x) /\ ~(b IN x) /\ ~(a = b) /\ a IN (UNIV DIFF x) /\ a IN (UNIV DIFF (x UNION y))` by SET_TAC 196 \\ `ADDR_SET xs SUBSET POINTERS h (UNIV DIFF (x UNION y))` by METIS_TAC [set_SUBSET_POINTERS] 197 \\ `((a =+ b) ((b =+ a) f) o (a =+ b) ((b =+ a) f) = I)` by 198 (FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,FUN_EQ_THM] \\ SET_TAC) 199 \\ STRIP_TAC THEN1 SET_TAC 200 \\ ASM_SIMP_TAC std_ss [POINTERS_IGNORE] \\ STRIP_TAC THEN1 SET_TAC 201 \\ `(HAS_CHANGED ((a =+ b) ((b =+ a) f)) = a INSERT b INSERT HAS_CHANGED f) /\ 202 ~(b IN HAS_CHANGED f)` by 203 (FULL_SIMP_TAC std_ss [EXTENSION,HAS_CHANGED_def,APPLY_UPDATE_THM] \\ SET2_TAC) 204 \\ STRIP_TAC THEN1 (FULL_SIMP_TAC std_ss [] \\ SET2_TAC) 205 \\ `~(a IN y) /\ ~(b IN y)` by SET_TAC 206 \\ FULL_SIMP_TAC std_ss [SET_TRANSLATE_THM,APPLY_UPDATE_THM,SET_TRANSLATE_IGNORE] 207 \\ STRIP_TAC THEN1 SET2_TAC 208 \\ STRIP_TAC THEN1 209 (`a IN gc_reachable (h0,r0)` by SET_TAC 210 \\ SUBGOAL `ADDR_SET xs SUBSET gc_reachable (h0,r0)` THEN1 SET_TAC 211 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF] \\ REPEAT STRIP_TAC 212 \\ SIMP_TAC std_ss [IN_DEF] \\ ONCE_REWRITE_TAC [gc_reachable_cases] 213 \\ DISJ2_TAC \\ Q.PAT_X_ASSUM `a IN gc_reachable hhh` 214 (ASSUME_TAC o SIMP_RULE std_ss [IN_DEF]) \\ ASM_SIMP_TAC std_ss [] 215 \\ Q.LIST_EXISTS_TAC [`a`,`xs`,`d`] \\ ASM_SIMP_TAC std_ss [] \\ SET2_TAC) 216 \\ STRIP_TAC THEN1 217 (FULL_SIMP_TAC std_ss [FDOM_FUPDATE,FDOM_DOMSUB] 218 \\ ALPHA_TAC "n" \\ REPEAT STRIP_TAC THEN1 219 (Cases_on `a = n` \\ FULL_SIMP_TAC std_ss [] 220 \\ SUBGOAL `~(n = b)` THEN1 (FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ SET_TAC) 221 \\ CCONTR_TAC \\ FULL_SIMP_TAC std_ss [] 222 \\ `~(b IN HAS_CHANGED f)` by (SIMP_TAC std_ss [HAS_CHANGED_def] \\ SET_TAC) 223 \\ SET_TAC) 224 \\ Cases_on `a = n` \\ FULL_SIMP_TAC std_ss [] 225 \\ `POINTERS h (UNIV DIFF (x UNION y)) SUBSET POINTERS h (UNIV DIFF x)` by 226 (MATCH_MP_TAC POINTERS_SUBSET \\ SET_TAC) 227 \\ `n IN FDOM h UNION HAS_CHANGED f DIFF (x UNION y)` by SET_TAC 228 \\ FULL_SIMP_TAC std_ss [IN_INSERT,IN_UNION,IN_DELETE,IN_DIFF] \\ SET_TAC) 229 \\ FULL_SIMP_TAC std_ss [FDOM_DOMSUB,FDOM_FUPDATE,IN_INSERT] 230 \\ STRIP_TAC THEN1 (FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ SET_TAC) 231 \\ STRIP_TAC THEN1 (FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ SET_TAC) 232 \\ Q.PAT_X_ASSUM `gg = FDOM h0` (ASSUME_TAC o GSYM) \\ ASM_SIMP_TAC std_ss [] 233 \\ STRIP_TAC THEN1 234 (FULL_SIMP_TAC std_ss [EXTENSION,SET_TRANSLATE_def,APPLY_UPDATE_THM] 235 \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ SET_TAC) 236 \\ ALPHA_TAC "i" \\ STRIP_TAC 237 \\ Cases_on `(i = a) \/ (i = b)` \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM, 238 FUN_EQ_THM,DOMSUB_FAPPLY_THM,FAPPLY_FUPDATE_THM] 239 THEN1 (FULL_SIMP_TAC std_ss [SET_TRANSLATE_def]) 240 \\ `~(f i = a) /\ ~(f i = b)` by METIS_TAC [] 241 \\ Cases_on `f i IN x` \\ FULL_SIMP_TAC std_ss [] 242 \\ `?xs d. h ' (f i) = (xs,d)` by METIS_TAC [PAIR] 243 \\ ASM_SIMP_TAC std_ss [PAIR_TRANSLATE_def,IN_DEF,SET_TRANSLATE_def] 244 \\ ASM_SIMP_TAC std_ss [ADDR_MAP_EQ_ADDR_MAP,APPLY_UPDATE_THM] 245 \\ REPEAT STRIP_TAC 246 \\ `ADDR_SET xs' SUBSET x UNION y` by METIS_TAC [set_SUBSET_POINTERS,SUBSET_TRANS] 247 \\ SET_TAC)); 248 249val abs_steps_thm = prove( 250 ``!s1 s2. abs_steps s1 s2 /\ abs_gc_inv (h0,r0) s1 ==> abs_gc_inv (h0,r0) s2``, 251 SIMP_TAC std_ss [GSYM AND_IMP_INTRO,abs_steps_def] 252 \\ HO_MATCH_MP_TAC RTC_INDUCT \\ SIMP_TAC std_ss [] \\ METIS_TAC [abs_step_thm]); 253 254val ok_heap_def = Define ` 255 ok_heap (h,roots) = (POINTERS h UNIV UNION ADDR_SET roots SUBSET FDOM h)`; 256 257val ok_heap_IMP = store_thm("ok_heap_IMP", 258 ``ok_heap (h1,roots1) ==> abs_gc_inv (h1,roots1) (h1,{},{},ADDR_SET roots1,I)``, 259 FULL_SIMP_TAC std_ss [abs_gc_inv_def,LET_DEF,ok_heap_def] 260 \\ SUBGOAL `ADDR_SET roots1 SUBSET gc_reachable (h1,roots1)` THEN1 SET2_TAC 261 \\ SIMP_TAC std_ss [SUBSET_DEF] \\ REPEAT STRIP_TAC \\ SIMP_TAC std_ss [IN_DEF] 262 \\ ONCE_REWRITE_TAC [gc_reachable_cases] \\ ASM_SIMP_TAC std_ss []); 263 264val abs_gc_thm = store_thm("abs_gc_thm", 265 ``!h1 roots1 h2 roots2. 266 ok_heap (h1,roots1) /\ abs_gc (h1,roots1) (h2,roots2) ==> 267 gc_exec (h1,roots1) (h2,roots2)``, 268 SIMP_TAC std_ss [abs_gc_cases,gc_exec_def,gc_filter_def,gc_copy_def] 269 \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `f` \\ ASM_SIMP_TAC std_ss [] 270 \\ IMP_RES_TAC ok_heap_IMP \\ IMP_RES_TAC abs_steps_thm \\ POP_ASSUM MP_TAC 271 \\ SIMP_TAC std_ss [abs_gc_inv_def,LET_DEF,NOT_IN_EMPTY,UNION_EMPTY] 272 \\ STRIP_TAC \\ SIMP_TAC std_ss [FDOM_DRESTRICT,DRESTRICT_DEF] 273 \\ SUBGOAL `gc_reachable (h1,roots1) = SET_TRANSLATE f x` THEN1 SET2_TAC 274 \\ ASM_SIMP_TAC std_ss [SET_EQ_SUBSET] \\ SIMP_TAC std_ss [SUBSET_DEF] 275 \\ `?tt. (h1,roots1) = tt` by METIS_TAC [PAIR] \\ ASM_SIMP_TAC std_ss [] 276 \\ REPEAT STRIP_TAC \\ REPEAT (POP_ASSUM MP_TAC) 277 \\ SIMP_TAC std_ss [AND_IMP_INTRO] \\ ONCE_REWRITE_TAC [CONJ_COMM] 278 \\ SIMP_TAC std_ss [GSYM CONJ_ASSOC] \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO] 279 \\ STRIP_TAC \\ POP_ASSUM (MP_TAC o SIMP_RULE std_ss [IN_DEF]) 280 \\ Q.SPEC_TAC (`x'`,`q`) \\ Q.SPEC_TAC (`tt`,`t`) 281 \\ HO_MATCH_MP_TAC gc_reachable_ind \\ REPEAT STRIP_TAC THEN1 SET_TAC 282 \\ FULL_SIMP_TAC std_ss [SET_TRANSLATE_def] 283 \\ `h2' ' (f q') = (ADDR_MAP f xs,d)` by 284 (Q.PAT_X_ASSUM `!d. d IN FDOM h ==> bb` (MP_TAC o GSYM o Q.SPEC `q'`) 285 \\ `?xs2 d2. h2' ' (f q') = (xs2,d2)` by METIS_TAC [PAIR] 286 \\ ASM_SIMP_TAC std_ss [PAIR_TRANSLATE_def] 287 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 288 \\ ASM_SIMP_TAC std_ss [ADDR_MAP_ADDR_MAP]) 289 \\ `ADDR_SET (ADDR_MAP f xs) SUBSET POINTERS h2' x` by METIS_TAC [set_SUBSET_POINTERS] 290 \\ `f q IN ADDR_SET (ADDR_MAP f xs)` by 291 (FULL_SIMP_TAC std_ss [SET_TRANSLATE_MAP,SET_TRANSLATE_def] 292 \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM]) \\ SET_TAC); 293 294val gc_copy_thm = prove( 295 ``ok_heap (h1,roots1) /\ gc_copy (h1,roots1) (h2,roots2) ==> ok_heap (h2,roots2)``, 296 SIMP_TAC std_ss [gc_exec_def,gc_copy_def,gc_filter_def,ok_heap_def] 297 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,IN_UNION,POINTERS_def] 298 \\ `!k. f (f k) = k` by FULL_SIMP_TAC std_ss [FUN_EQ_THM] 299 \\ REVERSE (REPEAT STRIP_TAC) THEN1 300 (POP_ASSUM MP_TAC \\ FULL_SIMP_TAC std_ss [SET_TRANSLATE_MAP,SET_TRANSLATE_def] 301 \\ SET_TAC) 302 \\ FULL_SIMP_TAC std_ss [IN_UNIV,SET_TRANSLATE_def,EXTENSION] 303 \\ Q.PAT_X_ASSUM `!d. ff IN FDOM h1 <=> bb IN FDOM h2` ASSUME_TAC 304 \\ FULL_SIMP_TAC std_ss [] 305 \\ `h1 ' (f b) = PAIR_TRANSLATE f (zs,d)` by METIS_TAC [] 306 \\ FULL_SIMP_TAC std_ss [PAIR_TRANSLATE_def] 307 \\ SUBGOAL `f x IN ADDR_SET (ADDR_MAP f zs)` THEN1 METIS_TAC [] 308 \\ FULL_SIMP_TAC std_ss [SET_TRANSLATE_MAP,SET_TRANSLATE_def]); 309 310val gc_filter_thm = prove( 311 ``ok_heap (h1,roots1) ==> ok_heap (gc_filter(h1,roots1))``, 312 SIMP_TAC std_ss [gc_exec_def,gc_copy_def,gc_filter_def,ok_heap_def] 313 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,IN_UNION,POINTERS_def] 314 \\ REVERSE (REPEAT STRIP_TAC) THEN1 315 (RES_TAC \\ FULL_SIMP_TAC std_ss [FDOM_DRESTRICT,IN_INTER] 316 \\ FULL_SIMP_TAC std_ss [IN_DEF] \\ ONCE_REWRITE_TAC [gc_reachable_cases] 317 \\ ASM_SIMP_TAC std_ss [IN_DEF]) 318 \\ FULL_SIMP_TAC std_ss [FDOM_DRESTRICT,IN_INTER] 319 \\ Q.PAT_X_ASSUM `DRESTRICT h1 (gc_reachable (h1,roots1)) ' b = (zs,d)` MP_TAC 320 \\ ASM_SIMP_TAC std_ss [DRESTRICT_DEF,IN_INTER] \\ REPEAT STRIP_TAC THEN1 SET_TAC 321 \\ FULL_SIMP_TAC std_ss [IN_DEF] 322 \\ ONCE_REWRITE_TAC [gc_reachable_cases] \\ DISJ2_TAC 323 \\ SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `b` \\ ASM_SIMP_TAC std_ss [IN_DEF]); 324 325val gc_exec_thm = store_thm("gc_exec_thm", 326 ``ok_heap (h1,roots1) /\ gc_exec (h1,roots1) (h2,roots2) ==> ok_heap (h2,roots2)``, 327 METIS_TAC [gc_exec_def,gc_filter_thm,gc_copy_thm,PAIR]); 328 329(* next level *) 330 331val _ = Hol_datatype `heap_element = 332 H_EMP | H_REF of num | H_BLOCK of ('a heap_address) list # (num # 'b)`; 333val heap_element_distinct = fetch "-" "heap_element_distinct"; 334val heap_element_11 = fetch "-" "heap_element_11"; 335 336val isDATA_def = Define `isDATA x = ?i. x = H_DATA i`; 337val isADDR_def = Define `isADDR x = ?i. x = H_ADDR i`; 338val isREF_def = Define `isREF x = ?i. x = H_REF i`; 339val isBLOCK_def = Define `isBLOCK x = ?i. x = H_BLOCK i`; 340val getADDR_def = Define `getADDR (H_ADDR x) = x`; 341val getREF_def = Define `getREF (H_REF x) = x`; 342val getBLOCK_def = Define `getBLOCK (H_BLOCK y) = y`; 343val getLENGTH_def = Define ` 344 (getLENGTH (H_BLOCK (m,l,n)) = l + 1) /\ 345 (getLENGTH (H_REF i) = 0) /\ 346 (getLENGTH (H_EMP) = 0)`; 347 348val RANGE_def = Define `RANGE(i:num,j) k = i <= k /\ k < j`; 349val CUT_def = Define `CUT (i,j) m = \k. if RANGE (i,j) k then m k else H_EMP`; 350 351val D0 = Define `D0 m k = ?x y z. m (k:num) = H_BLOCK (x,y,z)`; 352val D1 = Define `D1 m i = ?k x y z. (m (k:num) = H_BLOCK(x,y,z)) /\ i IN ADDR_SET x`; 353val R0 = Define `R0 m k = ?a. m (k:num) = H_REF a`; 354val R1 = Define `R1 m a = ?k. m (k:num) = H_REF a`; 355val DR0 = Define `DR0 m k = D0 m k \/ R0 m k` 356val DR1 = Define `DR1 m k = D1 m k \/ R1 m k` 357 358val EMP_RANGE_def = Define ` 359 EMP_RANGE (b,e) m = !k. k IN RANGE(b,e) ==> (m k = H_EMP)`; 360 361val rel_move_def = Define ` 362 (rel_move (H_DATA x,j,m,b,e,b2,e2) = (T,H_DATA x,j,m)) /\ 363 (rel_move (H_ADDR a,j,m,b,e,b2,e2) = 364 case m a of 365 H_EMP => (F,ARB) 366 | H_REF i => (RANGE (b2,e2) a,H_ADDR i,j,m) 367 | H_BLOCK (xs,n,d) => let cond = RANGE (b2,e2) a in 368 let m = (a =+ H_REF j) m in 369 let cond = RANGE (b,e) j /\ (m j = H_EMP) /\ cond in 370 let m = (j =+ H_BLOCK (xs,n,d)) m in 371 (cond,H_ADDR j,j + n + 1,m))`; 372 373val rel_move_list_def = Define ` 374 (rel_move_list ([],j,m,b,e,b2,e2) = (T,[],j,m)) /\ 375 (rel_move_list (x::xs,j,m,b,e,b2,e2) = 376 let (c1,x,j,m) = rel_move (x,j,m,b,e,b2,e2) in 377 let (c2,xs,j,m) = rel_move_list (xs,j,m,b,e,b2,e2) in 378 (c1 /\ c2,x::xs,j,m))`; 379 380val rel_gc_step_def = Define ` 381 rel_gc_step (i,j,m,b,e,b2,e2) = 382 let cond = isBLOCK (m i) in 383 let (xs,n,d) = getBLOCK (m i) in 384 let (c2,ys,j,m) = rel_move_list (xs,j,m,b,e,b2,e2) in 385 let cond = cond /\ (m i = H_BLOCK (xs,n,d)) /\ RANGE(b,e)i /\ c2 /\ 386 EMP_RANGE (i+1,i+n+1) m in 387 let m = (i =+ H_BLOCK (ys,n,d)) m in 388 let i = i + n + 1 in 389 let cond = cond /\ i <= j in 390 (cond,i,j,m)`; 391 392val rel_gc_loop_def = tDefine "rel_gc_loop" ` 393 rel_gc_loop (i,j,m,b,e,b2,e2) = 394 if i = j then (T,i,m) else 395 if ~(i < j /\ j <= e) then (F,ARB) else 396 let (c1,i,j,m) = rel_gc_step (i,j,m,b,e,b2,e2) in 397 let (c2,i,m) = rel_gc_loop (i,j,m,b,e,b2,e2) in 398 (c1/\c2,i,m)` 399 (WF_REL_TAC `measure (\(i,j,m,b,e,b2,e2). e - i)` 400 \\ SIMP_TAC std_ss [rel_gc_step_def,LET_DEF] 401 \\ CONV_TAC (DEPTH_CONV (helperLib.FORCE_PBETA_CONV)) 402 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 403 \\ SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ DECIDE_TAC); 404 405val rel_gc_def = Define ` 406 rel_gc (b:num,e:num,b2:num,e2:num,roots,m) = 407 let (b2,e2,b,e) = (b,e,b2,e2) in 408 let (cond,roots,j,m) = rel_move_list (roots,b,m,b,e,b2,e2) in 409 let (c,i,m) = rel_gc_loop (b,j,m,b,e,b2,e2) in 410 let cond = cond /\ b <= i /\ i <= e in 411 let m = CUT (b,i) m in 412 (c /\ cond,b,i,e,b2,e2,roots,m)`; 413 414 415 416(* invariant *) 417 418val (full_heap_rules,full_heap_ind,full_heap_cases) = 419 Hol_reln 420 `(!b m. full_heap b b m) /\ 421 (!b e m n xs d. 422 (m b = H_BLOCK (xs,n,d)) /\ EMP_RANGE (b+1,b+n+1) m /\ 423 full_heap (b+n+1) e m ==> full_heap b e m)`; 424 425val full_heap_ind = IndDefLib.derive_strong_induction(full_heap_rules,full_heap_ind); 426val _ = save_thm("full_heap_ind",full_heap_ind); 427 428val (part_heap_rules,part_heap_ind,part_heap_cases) = 429 Hol_reln 430 `(!b m. part_heap b b m 0) /\ 431 (!b e m k. 432 ~(isBLOCK (m b)) /\ part_heap (b+1) e m k ==> part_heap b e m k) /\ 433 (!b e m n xs d k. 434 (m b = H_BLOCK (xs,n,d)) /\ EMP_RANGE (b+1,b+n+1) m /\ 435 part_heap (b+n+1) e m k ==> part_heap b e m (k+n+1))`; 436 437val part_heap_ind = IndDefLib.derive_strong_induction(part_heap_rules,part_heap_ind); 438val _ = save_thm("part_heap_ind",part_heap_ind); 439 440val ref_heap_mem_def = Define ` 441 ref_heap_mem (h,f) m = 442 !a. m a = if a IN FDOM h then H_BLOCK (h ' a) else 443 if f a = a then H_EMP else H_REF (f a)`; 444 445val gc_inv_def = Define ` 446 gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,z) = 447 (b <= i /\ i <= j /\ j <= e) /\ 448 (* semispaces are disjoint, simplified *) 449 (~(e2 <= b) ==> e <= b2) /\ 450 (* EMP outside of b2-e2 and b-j *) 451 (!k. ~(RANGE(b2,e2)k) /\ ~(RANGE(b,j)k) ==> (m k = H_EMP)) /\ 452 (* heap full of BLOCK elements between b-i, i-j *) 453 full_heap b i m /\ full_heap i j m /\ 454 (* data elements from b2-e2 fit into j-e *) 455 (?len. part_heap b2 e2 m len /\ len <= e-j) /\ 456 (* refinement *) 457 ref_heap_mem (h,f) m /\ 458 (* simulation *) 459 ok_heap (h1,roots1) /\ 460 abs_steps (h1,{},{},ADDR_SET roots1,I) (h,D0(CUT(b,i)m),D0(CUT(i,j)m),z,f)`; 461 462(* some lemmas *) 463 464val RANGE_TAC = FULL_SIMP_TAC std_ss [RANGE_def,IN_DEF,gc_inv_def] \\ DECIDE_TAC 465 466val gc_inv_IMP = store_thm("gc_inv_IMP", 467 ``gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,z) ==> 468 abs_gc_inv (h1,roots1) (h,D0(CUT(b,i)m),D0(CUT(i,j)m),z,f)``, 469 SIMP_TAC std_ss [gc_inv_def] \\ METIS_TAC [ok_heap_IMP,abs_steps_thm]); 470 471val gc_inv_THM = store_thm("gc_inv_THM", 472 ``gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,z) = 473 gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,z) /\ 474 abs_gc_inv (h1,roots1) (h,D0(CUT(b,i)m),D0(CUT(i,j)m),z,f)``, 475 METIS_TAC [gc_inv_IMP]); 476 477val full_heap_REFL = store_thm("full_heap_REFL", 478 ``!b m. full_heap b b m``, 479 METIS_TAC [full_heap_cases]); 480 481val full_heap_TRANS = store_thm("full_heap_TRANS", 482 ``!j b i m. full_heap b i m /\ full_heap i j m ==> full_heap b j m``, 483 STRIP_TAC \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO] \\ HO_MATCH_MP_TAC full_heap_ind 484 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ METIS_TAC [full_heap_cases]); 485 486val full_heap_step = prove( 487 ``!n xs d b e m. full_heap b e m ==> 488 (m e = H_BLOCK (xs,n,d)) /\ EMP_RANGE (e+1,e+n+1) m ==> 489 full_heap b (e+n+1) m``, 490 NTAC 3 STRIP_TAC 491 \\ HO_MATCH_MP_TAC full_heap_ind \\ STRIP_TAC THEN1 METIS_TAC [full_heap_cases] 492 \\ REPEAT STRIP_TAC \\ RES_TAC \\ METIS_TAC [full_heap_cases]); 493 494val CUT_EQ = store_thm("CUT_EQ", 495 ``((CUT (b,e) m a = H_BLOCK x) = (a IN RANGE (b,e) /\ (m a = H_BLOCK x))) /\ 496 ((CUT (b,e) m a = H_REF i) = (a IN RANGE (b,e) /\ (m a = H_REF i)))``, 497 SIMP_TAC std_ss [CUT_def,IN_DEF] \\ SRW_TAC [] []); 498 499val CUT_update = prove( 500 ``~RANGE (i,j) k ==> (CUT (i,j) ((k =+ x) m) = CUT (i,j) m)``, 501 SIMP_TAC std_ss [CUT_def,UPDATE_def,FUN_EQ_THM] \\ METIS_TAC []); 502 503val part_heap_LESS_EQ = store_thm("part_heap_LESS_EQ", 504 ``!b e m k. part_heap b e m k ==> b <= e``, 505 HO_MATCH_MP_TAC part_heap_ind \\ REPEAT STRIP_TAC \\ DECIDE_TAC); 506 507val EMP_RANGE_RANGE = store_thm("EMP_RANGE_RANGE", 508 ``!b e i m. 509 ~(RANGE(b,e)i) ==> (EMP_RANGE (b,e) ((i=+x)m) = EMP_RANGE (b,e) m)``, 510 FULL_SIMP_TAC std_ss [EMP_RANGE_def,APPLY_UPDATE_THM,IN_DEF] \\ METIS_TAC []); 511 512val part_heap_TRANS = store_thm("part_heap_TRANS", 513 ``!j k2 b i m k1. part_heap b i m k1 /\ part_heap i j m k2 ==> part_heap b j m (k1+k2)``, 514 NTAC 2 STRIP_TAC \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO] 515 \\ HO_MATCH_MP_TAC part_heap_ind \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC 516 THEN1 (REPEAT STRIP_TAC \\ RES_TAC \\ METIS_TAC [part_heap_cases]) 517 \\ REPEAT STRIP_TAC \\ RES_TAC \\ ONCE_REWRITE_TAC [part_heap_cases] 518 \\ ASM_SIMP_TAC std_ss [heap_element_11] \\ DISJ2_TAC 519 \\ Q.EXISTS_TAC `k1+k2` \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC); 520 521val part_heap_IGNORE = store_thm("part_heap_IGNORE", 522 ``!b e m k. part_heap b e m k /\ ~(RANGE(b,e)i) ==> 523 part_heap b e ((i =+ x) m) k``, 524 SIMP_TAC std_ss [GSYM AND_IMP_INTRO] \\ HO_MATCH_MP_TAC part_heap_ind 525 \\ STRIP_TAC THEN1 METIS_TAC [part_heap_cases] 526 \\ STRIP_TAC THEN1 527 (REPEAT STRIP_TAC \\ IMP_RES_TAC part_heap_LESS_EQ 528 \\ `~(RANGE(b+1,e)i) /\ ~(i = b)` by RANGE_TAC \\ RES_TAC 529 \\ METIS_TAC [APPLY_UPDATE_THM,part_heap_cases]) 530 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC part_heap_LESS_EQ 531 \\ `~RANGE (b + n + 1,e) i /\ ~(b = i) /\ ~(RANGE(b+1,b+n+1)i)` by RANGE_TAC 532 \\ ONCE_REWRITE_TAC [part_heap_cases] \\ DISJ2_TAC \\ DISJ2_TAC 533 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,heap_element_11,EMP_RANGE_RANGE]); 534 535val part_heap_EMP_RANGE = store_thm("part_heap_EMP_RANGE", 536 ``!i m. b <= i /\ EMP_RANGE (b,i) m ==> part_heap b i m 0``, 537 STRIP_TAC \\ completeInduct_on `i-b` \\ REPEAT STRIP_TAC \\ Cases_on `i = b` 538 \\ FULL_SIMP_TAC std_ss [] THEN1 METIS_TAC [part_heap_cases] 539 \\ `b+1 <= i /\ i - (b + 1) < i - b /\ (i - (b + 1) = i - (b + 1))` by DECIDE_TAC 540 \\ ONCE_REWRITE_TAC [part_heap_cases] \\ DISJ2_TAC \\ DISJ1_TAC 541 \\ SUBGOAL `(m b = H_EMP) /\ EMP_RANGE (b+1,i) m` 542 THEN1 (RES_TAC \\ FULL_SIMP_TAC std_ss [isBLOCK_def,heap_element_distinct]) 543 \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF] 544 \\ `RANGE(b,i)b` by RANGE_TAC \\ ASM_SIMP_TAC std_ss [] 545 \\ REPEAT STRIP_TAC \\ `RANGE(b,i)k` by RANGE_TAC \\ ASM_SIMP_TAC std_ss []); 546 547val part_heap_REF = store_thm("part_heap_REF", 548 ``!b e m k. part_heap b e m k /\ (m i = H_BLOCK (x,y,d)) /\ RANGE(b,e)i ==> 549 y+1 <= k /\ part_heap b e ((i =+ H_REF t) m) (k - (y + 1))``, 550 SIMP_TAC std_ss [GSYM AND_IMP_INTRO] \\ HO_MATCH_MP_TAC part_heap_ind 551 \\ STRIP_TAC THEN1 (REPEAT STRIP_TAC \\ `F` by RANGE_TAC) 552 \\ STRIP_TAC THEN1 553 (NTAC 7 STRIP_TAC \\ FULL_SIMP_TAC std_ss [] \\ Cases_on `i = b` 554 THEN1 FULL_SIMP_TAC std_ss [isBLOCK_def,heap_element_11] 555 \\ `RANGE (b + 1,e) i` by RANGE_TAC 556 \\ METIS_TAC [APPLY_UPDATE_THM,part_heap_cases]) 557 \\ NTAC 10 STRIP_TAC \\ RES_TAC 558 \\ Cases_on `RANGE (b + n + 1,e) i` THEN1 559 (`~(i = b)` by RANGE_TAC \\ RES_TAC \\ STRIP_TAC THEN1 DECIDE_TAC 560 \\ ONCE_REWRITE_TAC [part_heap_cases] \\ DISJ2_TAC \\ DISJ2_TAC 561 \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM,heap_element_11] 562 \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF,APPLY_UPDATE_THM] 563 \\ Q.EXISTS_TAC `k-(y+1)` \\ STRIP_TAC THEN1 RANGE_TAC 564 \\ ASM_SIMP_TAC std_ss [] \\ ALPHA_TAC "j" \\ REPEAT STRIP_TAC 565 \\ Cases_on `i = j` \\ FULL_SIMP_TAC std_ss [heap_element_distinct] \\ RANGE_TAC) 566 \\ Cases_on `RANGE (b + 1,b + n + 1) i` THEN1 567 (FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF] \\ RES_TAC 568 \\ FULL_SIMP_TAC std_ss [heap_element_distinct]) 569 \\ `i = b` by RANGE_TAC \\ FULL_SIMP_TAC std_ss [heap_element_11] 570 \\ ONCE_REWRITE_TAC [part_heap_cases] \\ DISJ2_TAC \\ DISJ1_TAC 571 \\ SIMP_TAC std_ss [isBLOCK_def,APPLY_UPDATE_THM,heap_element_distinct] 572 \\ FULL_SIMP_TAC std_ss [DECIDE ``k+n+1-(n+1)=k``] 573 \\ MATCH_MP_TAC part_heap_IGNORE \\ REVERSE STRIP_TAC THEN1 RANGE_TAC 574 \\ ONCE_REWRITE_TAC [GSYM (RW1[ADD_COMM]ADD_0)] 575 \\ MATCH_MP_TAC part_heap_TRANS \\ Q.EXISTS_TAC `b+n+1` \\ ASM_SIMP_TAC std_ss [] 576 \\ ASM_SIMP_TAC std_ss [part_heap_EMP_RANGE]); 577 578val part_heap_LENGTH_LESS_EQ = store_thm("part_heap_LENGTH_LESS_EQ", 579 ``!b e m k. part_heap b e m k ==> k <= e - b``, 580 HO_MATCH_MP_TAC part_heap_ind \\ ASM_SIMP_TAC std_ss [] 581 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC part_heap_LESS_EQ \\ DECIDE_TAC); 582 583val CUT_UPDATE = store_thm("CUT_UPDATE", 584 ``!b e a m x. 585 (~(RANGE(b,e)a) ==> (CUT(b,e)((a=+x)m) = CUT(b,e)m)) /\ 586 (RANGE(b,e)a ==> (CUT(b,e)((a=+x)m) = (a=+x)(CUT(b,e)m)))``, 587 FULL_SIMP_TAC std_ss [FUN_EQ_THM,CUT_def,APPLY_UPDATE_THM] \\ METIS_TAC []); 588 589val ref_heap_mem_IMP = prove( 590 ``(ref_heap_mem (h,f) m /\ (m n = H_BLOCK x) ==> n IN FDOM h /\ (h ' n = x)) /\ 591 (ref_heap_mem (h,f) m /\ (m n = H_REF i) ==> ~(n IN FDOM h) /\ ~(f n = n) /\ (f n = i)) /\ 592 (ref_heap_mem (h,f) m /\ (m n = H_EMP) ==> ~(n IN FDOM h) /\ (f n = n))``, 593 SIMP_TAC std_ss [ref_heap_mem_def,GSYM AND_IMP_INTRO] 594 \\ METIS_TAC [heap_element_11,heap_element_distinct]); 595 596val full_heap_LESS_EQ = store_thm("full_heap_LESS_EQ", 597 ``!b e m. full_heap b e m ==> b <= e``, 598 HO_MATCH_MP_TAC full_heap_ind \\ REPEAT STRIP_TAC \\ DECIDE_TAC); 599 600val full_heap_IGNORE = prove( 601 ``!m2 b e m. full_heap b e m /\ (!a. RANGE(b,e)a ==> (m2 a = m a)) ==> 602 full_heap b e m2``, 603 STRIP_TAC \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO] 604 \\ HO_MATCH_MP_TAC full_heap_ind \\ REPEAT STRIP_TAC 605 \\ ONCE_REWRITE_TAC [full_heap_cases] \\ SIMP_TAC std_ss [APPLY_UPDATE_THM] 606 \\ IMP_RES_TAC full_heap_LESS_EQ 607 \\ `RANGE (b,e) b` by (FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC) 608 \\ RES_TAC \\ DISJ2_TAC \\ ASM_SIMP_TAC std_ss [heap_element_11] 609 \\ REPEAT STRIP_TAC THEN1 610 (FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF] 611 \\ REPEAT STRIP_TAC \\ RES_TAC 612 \\ `RANGE (b,e) k` by RANGE_TAC \\ ASM_SIMP_TAC std_ss []) 613 \\ Q.PAT_X_ASSUM `bbb ==> full_heap (b + n + 1) e m2` MATCH_MP_TAC 614 \\ REPEAT STRIP_TAC \\ RES_TAC 615 \\ `RANGE (b,e) a` by RANGE_TAC \\ ASM_SIMP_TAC std_ss []); 616 617val full_heap_RANGE = store_thm("full_heap_RANGE", 618 ``!i x b e m. full_heap b e m /\ ~(RANGE(b,e)i) ==> full_heap b e ((i =+ x) m)``, 619 REPEAT STRIP_TAC \\ MATCH_MP_TAC full_heap_IGNORE \\ Q.EXISTS_TAC `m` 620 \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM] \\ REPEAT STRIP_TAC 621 \\ Cases_on `a = i` \\ FULL_SIMP_TAC std_ss [RANGE_def]); 622 623val full_heap_R0 = prove( 624 ``!b e m. full_heap b e m ==> !k. RANGE(b,e)k ==> ~(R0 m k)``, 625 HO_MATCH_MP_TAC full_heap_ind \\ REPEAT STRIP_TAC 626 THEN1 (FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC) 627 \\ Cases_on `b = k` \\ FULL_SIMP_TAC std_ss [R0,heap_element_distinct] 628 \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF,heap_element_distinct] 629 \\ Cases_on `RANGE (b + n + 1,e) k` THEN1 METIS_TAC [] 630 \\ `RANGE (b + 1,b + n + 1) k` by (FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC) 631 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [R0,heap_element_distinct]); 632 633(* proof *) 634 635val move_lemma = store_thm("move_lemma", 636 ``gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,z UNION {n}) /\ 637 n IN (DR0(CUT(b2,e2)m)) ==> 638 (m n = H_REF (f n)) /\ ~(f n = n) \/ 639 getLENGTH (m n) <= e - j /\ (m n = H_BLOCK (h ' n)) /\ n IN FDOM h /\ ~(n = j) /\ 640 n IN RANGE(b2,e2) /\ (f n = n) /\ EMP_RANGE (j,j+getLENGTH(H_BLOCK (h ' n))) m``, 641 PURE_ONCE_REWRITE_TAC [gc_inv_THM] \\ ONCE_REWRITE_TAC [IN_DEF] \\ STRIP_TAC 642 \\ FULL_SIMP_TAC std_ss [gc_inv_def] \\ FULL_SIMP_TAC std_ss [DR0,R0,D0,CUT_EQ] 643 \\ IMP_RES_TAC ref_heap_mem_IMP \\ ASM_SIMP_TAC std_ss [heap_element_11,heap_element_distinct] 644 \\ SIMP_TAC std_ss [getLENGTH_def] \\ `n < e2` by RANGE_TAC 645 \\ `(CUT(b2,e2)m) n = H_BLOCK (x,y,z')` by FULL_SIMP_TAC std_ss [CUT_EQ] 646 \\ FULL_SIMP_TAC std_ss [IN_DEF] 647 \\ IMP_RES_TAC part_heap_REF \\ STRIP_TAC THEN1 RANGE_TAC 648 \\ FULL_SIMP_TAC std_ss [abs_gc_inv_def,LET_DEF] 649 \\ STRIP_TAC THEN1 RANGE_TAC 650 \\ STRIP_TAC THEN1 651 (`n IN FDOM h` by FULL_SIMP_TAC std_ss [IN_DEF] \\ CCONTR_TAC 652 \\ `n IN D0 (CUT (i,j) m) \/ n IN D0 (CUT (b,i) m)` by METIS_TAC [] 653 \\ FULL_SIMP_TAC std_ss [D0,CUT_EQ,IN_DEF] \\ RANGE_TAC) 654 \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF] 655 \\ REPEAT STRIP_TAC \\ Q.PAT_X_ASSUM `!k. bbb ==> (m k = H_EMP)` MATCH_MP_TAC 656 \\ RANGE_TAC); 657 658val ADDR_SET_THM = store_thm("ADDR_SET_THM", 659 ``(ADDR_SET [] = {}) /\ 660 (ADDR_SET (H_DATA x :: xs) = ADDR_SET xs) /\ 661 (ADDR_SET (H_ADDR y :: xs) = y INSERT ADDR_SET xs)``, 662 SRW_TAC [] [ADDR_SET_def,EXTENSION,MEM,NOT_IN_EMPTY,IN_INSERT]); 663 664val CUT_EMPTY = store_thm("CUT_EMPTY", 665 ``(D0(CUT(j,j)m) = {}) /\ (D1(CUT(j,j)m) = {}) /\ 666 (R0(CUT(j,j)m) = {}) /\ (R1(CUT(j,j)m) = {})``, 667 SIMP_TAC std_ss [EXTENSION,NOT_IN_EMPTY] 668 \\ `!j n. ~RANGE(j,j)n` by RANGE_TAC 669 \\ ASM_SIMP_TAC std_ss [IN_DEF,D0,R0,D1,R1,CUT_EQ]); 670 671val remove_from_z = prove( 672 ``~(f n = n) ==> abs_steps (h,x,y,z UNION {n},f) (h,x,y,z,f)``, 673 REPEAT STRIP_TAC \\ SIMP_TAC std_ss [abs_steps_def] \\ Cases_on `n IN z` 674 THEN1 (`z UNION {n} = z` by SET_TAC \\ FULL_SIMP_TAC std_ss [RTC_REFL]) 675 \\ `(z,f) = ((z UNION {n}) DELETE n,f)` by SET_TAC 676 \\ POP_ASSUM (fn th => ONCE_REWRITE_TAC [th]) \\ MATCH_MP_TAC RTC_SINGLE 677 \\ SIMP_TAC std_ss [abs_step_cases] \\ SET_TAC); 678 679val full_heap_BLOCK = prove( 680 ``!b e m. full_heap b e m /\ (m i = H_BLOCK (x2,y,z2)) ==> 681 full_heap b e ((i =+ H_BLOCK (x,y,z)) m)``, 682 SIMP_TAC std_ss [GSYM AND_IMP_INTRO] \\ HO_MATCH_MP_TAC full_heap_ind 683 \\ SIMP_TAC std_ss [full_heap_REFL] \\ REPEAT STRIP_TAC \\ RES_TAC 684 \\ ONCE_REWRITE_TAC [full_heap_cases] 685 \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF,APPLY_UPDATE_THM] 686 \\ METIS_TAC [heap_element_11,heap_element_distinct,PAIR_EQ]); 687 688val move_thm = store_thm("move_thm", 689 ``gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,z UNION ADDR_SET [x]) /\ 690 ADDR_SET [x] SUBSET (DR0(CUT(b2,e2)m)) /\ 691 (rel_move (x,j,m,b,e,b2,e2) = (c,x2,j2,m2)) ==> 692 ?h2 f2. gc_inv (h1,roots1,h2,f2) (b,i,j2,e,b2,e2,m2,z UNION (D1(CUT(j,j2)m2))) /\ j <= j2 /\ 693 DR0 (CUT (b2,e2) m) SUBSET DR0 (CUT (b2,e2) m2) /\ 694 (CUT(b,j)m = CUT(b,j)m2) /\ 695 (!a. ~(f a = a) ==> (f2 a = f a)) /\ 696 (!a. a IN ADDR_SET [x2] ==> ~(f2 a = a)) /\ 697 ([x2] = ADDR_MAP f2 [x]) /\ full_heap j j2 m2 /\ c``, 698 CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [gc_inv_THM])) 699 \\ REVERSE (Cases_on `x`) THEN1 700 (SIMP_TAC std_ss [rel_move_def] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 701 \\ sg `ADDR_SET [H_DATA a] = {}` \\ ASM_SIMP_TAC std_ss [full_heap_REFL] 702 \\ ASM_SIMP_TAC std_ss [ADDR_SET_def,SUBSET_DEF,MEM,NOT_IN_EMPTY,ADDR_MAP_def, 703 heap_address_distinct,EXTENSION,UNION_EMPTY,CUT_EMPTY] \\ SET_TAC) 704 \\ SIMP_TAC std_ss [ADDR_SET_THM,INSERT_SUBSET,EMPTY_SUBSET] 705 \\ STRIP_TAC 706 \\ IMP_RES_TAC move_lemma \\ FULL_SIMP_TAC std_ss [heap_element_distinct] 707 THEN1 708 (Q.LIST_EXISTS_TAC [`h`,`f`] \\ ASM_SIMP_TAC std_ss [] 709 \\ Q.PAT_X_ASSUM `rel_move xx = fg` MP_TAC \\ ASM_SIMP_TAC (srw_ss()) [rel_move_def] 710 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [ADDR_SET_THM, 711 IN_INSERT,NOT_IN_EMPTY,CUT_EMPTY,UNION_EMPTY,full_heap_REFL] 712 \\ FULL_SIMP_TAC std_ss [gc_inv_def,ADDR_MAP_def] \\ IMP_RES_TAC remove_from_z 713 \\ `f o f = I` by METIS_TAC [abs_gc_inv_def] \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM] 714 \\ FULL_SIMP_TAC std_ss [IN_DEF,DR0,D0,R0,CUT_EQ] 715 \\ METIS_TAC [abs_steps_thm,remove_from_z,abs_steps_TRANS]) 716 \\ `?x y d. h ' n = (x,y,d)` by METIS_TAC [PAIR] 717 \\ Q.PAT_X_ASSUM `rel_move xx = fg` MP_TAC \\ ASM_SIMP_TAC (srw_ss()) [rel_move_def] 718 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [LET_DEF,DECIDE ``j <= j + y + 1``] 719 \\ STRIP_TAC 720 \\ Q.LIST_EXISTS_TAC [`h |+ (j,h ' n) \\ n`,`(n =+ j) ((j =+ n) f)`] \\ ASM_SIMP_TAC std_ss [] 721 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,ADDR_SET_THM,IN_INSERT,NOT_IN_EMPTY] 722 \\ `full_heap j (j + y + 1) ((j =+ H_BLOCK (x,y,d)) ((n =+ H_REF j) m))` by 723 (Q.PAT_X_ASSUM `~(n = j)` (fn th => REWRITE_TAC [MATCH_MP UPDATE_COMMUTES (GSYM th)]) 724 \\ `~(RANGE(j,j+y+1)n)` by 725 (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [IN_DEF,R0,D0,DR0,EMP_RANGE_def, 726 getLENGTH_def,ADD_ASSOC,heap_element_distinct]) 727 \\ MATCH_MP_TAC full_heap_RANGE \\ ASM_SIMP_TAC std_ss [] 728 \\ ONCE_REWRITE_TAC [full_heap_cases] \\ DISJ2_TAC 729 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,heap_element_11,full_heap_REFL, 730 EMP_RANGE_def,getLENGTH_def,IN_DEF,ADD_ASSOC] \\ REPEAT STRIP_TAC 731 \\ `~(j = k) /\ RANGE (j,j + y + 1) k` by RANGE_TAC \\ SET_TAC) 732 \\ MATCH_MP_TAC (METIS_PROVE [] ``(b1 ==> b2) /\ b1 ==> b1 /\ b2``) 733 \\ STRIP_TAC THEN1 734 (STRIP_TAC 735 \\ `~(RANGE(b,j)j) /\ ~(RANGE(b,j)n) /\ ~(RANGE(b2,e2)j)` by RANGE_TAC 736 \\ ASM_SIMP_TAC std_ss [CUT_UPDATE,ADDR_MAP_def] 737 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,DR0,IN_DEF,D0,R0,CUT_EQ,APPLY_UPDATE_THM] 738 \\ FULL_SIMP_TAC std_ss [getLENGTH_def,EMP_RANGE_def,ADD_ASSOC,IN_DEF] 739 \\ `RANGE (j,j + y + 1) j` by RANGE_TAC 740 \\ `RANGE (b,e) j` by RANGE_TAC 741 \\ FULL_SIMP_TAC std_ss [gc_inv_def,FUN_EQ_THM,abs_gc_inv_def,LET_DEF] 742 \\ `f j = j` by METIS_TAC [ref_heap_mem_def,heap_element_distinct] 743 \\ REPEAT STRIP_TAC \\ METIS_TAC [heap_element_11,heap_element_distinct,PAIR_EQ]) 744 \\ FULL_SIMP_TAC std_ss [gc_inv_def] 745 \\ FULL_SIMP_TAC std_ss [getLENGTH_def] 746 \\ `~(RANGE(b,i)j) /\ ~(RANGE(b,i)n) /\ ~(RANGE(i,j)j) /\ 747 ~(RANGE(i,j)n) /\ ~(RANGE(b2,e2)j)` by RANGE_TAC 748 \\ REPEAT STRIP_TAC THEN1 RANGE_TAC THEN1 RANGE_TAC 749 THEN1 (`~(j = k) /\ ~(n = k) /\ ~RANGE (b,j) k` by RANGE_TAC \\ METIS_TAC [APPLY_UPDATE_THM]) 750 THEN1 METIS_TAC [full_heap_RANGE] 751 THEN1 752 (MATCH_MP_TAC full_heap_TRANS \\ Q.EXISTS_TAC `j` \\ ASM_SIMP_TAC std_ss [full_heap_RANGE]) 753 THEN1 754 (Q.EXISTS_TAC `len - (y+1)` \\ FULL_SIMP_TAC std_ss [IN_DEF] 755 \\ IMP_RES_TAC (Q.INST [`t`|->`j`] part_heap_REF) 756 \\ REVERSE STRIP_TAC THEN1 DECIDE_TAC 757 \\ MATCH_MP_TAC part_heap_IGNORE \\ ASM_SIMP_TAC std_ss []) 758 THEN1 759 (SIMP_TAC std_ss [ref_heap_mem_def,APPLY_UPDATE_THM,FDOM_FUPDATE,FDOM_DOMSUB, 760 IN_INSERT,IN_DELETE,FAPPLY_FUPDATE_THM,DOMSUB_FAPPLY_THM] 761 \\ ALPHA_TAC "k" \\ REPEAT STRIP_TAC 762 \\ Cases_on `j = k` \\ FULL_SIMP_TAC std_ss [] 763 \\ Cases_on `k = n` \\ FULL_SIMP_TAC std_ss [ref_heap_mem_def]) 764 \\ FULL_SIMP_TAC std_ss [CUT_UPDATE] 765 \\ Q.PAT_X_ASSUM `~(n = j)` (fn th => REWRITE_TAC [MATCH_MP UPDATE_COMMUTES (GSYM th)] THEN ASSUME_TAC th) 766 \\ `~(RANGE(j,j + y + 1)n) /\ ~(RANGE(i,j + y + 1)n)` by RANGE_TAC 767 \\ FULL_SIMP_TAC std_ss [CUT_UPDATE] 768 \\ REPEAT (Q.PAT_X_ASSUM `~(RANGE(xx,yy)df)` (K ALL_TAC)) 769 \\ `!k. RANGE (i,j + y + 1) k /\ ~RANGE (i,j) k ==> RANGE (j,j + y + 1) k` by RANGE_TAC 770 \\ `D0 (CUT (i,j + y + 1) ((j =+ H_BLOCK (x,y,d)) m)) = 771 j INSERT D0 (CUT (i,j) m)` by 772 (FULL_SIMP_TAC std_ss [EXTENSION,IN_INSERT] 773 \\ FULL_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,APPLY_UPDATE_THM,EMP_RANGE_def,IN_DEF] 774 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC THEN1 775 (Cases_on `j = x'` \\ FULL_SIMP_TAC std_ss [heap_element_11] 776 \\ CCONTR_TAC \\ `RANGE(j,j+y+1)x'` by RANGE_TAC 777 \\ METIS_TAC [heap_element_distinct,ADD_ASSOC]) 778 \\ Cases_on `j = x'` \\ FULL_SIMP_TAC std_ss [heap_element_11] \\ RANGE_TAC) 779 \\ `D1 (CUT (j,j + y + 1) ((j =+ H_BLOCK (x,y,d)) m)) = ADDR_SET x` by 780 (FULL_SIMP_TAC std_ss [FUN_EQ_THM,D1,CUT_EQ,IN_DEF,APPLY_UPDATE_THM,EMP_RANGE_def] 781 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 782 THEN1 (Cases_on `j = k` \\ METIS_TAC 783 [heap_element_11,heap_element_distinct,PAIR_EQ,ADD_ASSOC]) 784 \\ Q.EXISTS_TAC `j` \\ ASM_SIMP_TAC std_ss [heap_element_11] \\ RANGE_TAC) 785 \\ ASM_SIMP_TAC std_ss [] 786 \\ MATCH_MP_TAC abs_steps_TRANS 787 \\ Q.EXISTS_TAC `(h,D0 (CUT (b,i) m),D0 (CUT (i,j) m),z UNION {n},f)` 788 \\ ASM_SIMP_TAC std_ss [] 789 \\ MATCH_MP_TAC abs_steps_TRANS 790 \\ Q.EXISTS_TAC `(h |+ (j,x,y,d) \\ n,D0 (CUT (b,i) m),j INSERT D0 (CUT (i,j) m), 791 (z UNION ADDR_SET x) UNION {n},(n =+ j) ((j =+ n) f))` 792 \\ REVERSE STRIP_TAC 793 THEN1 (MATCH_MP_TAC remove_from_z \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM]) 794 \\ `!xx. z UNION xx UNION {n} = z UNION {n} UNION xx` by SET_TAC 795 \\ ASM_SIMP_TAC std_ss [] 796 \\ SIMP_TAC std_ss [abs_steps_def] \\ MATCH_MP_TAC RTC_SINGLE 797 \\ SIMP_TAC std_ss [abs_step_cases] \\ DISJ2_TAC \\ DISJ2_TAC 798 \\ Q.LIST_EXISTS_TAC [`n`,`j`,`x`,`(y,d)`] \\ ASM_SIMP_TAC std_ss [] 799 \\ STRIP_TAC THEN1 SET_TAC 800 \\ `~RANGE (b2,e2) j /\ ~RANGE (b,j) j` by RANGE_TAC 801 \\ `m j = H_EMP` by SET_TAC 802 \\ Q.PAT_X_ASSUM `ref_heap_mem (h,f) m` (fn th => FULL_SIMP_TAC std_ss [RW[ref_heap_mem_def]th]) 803 \\ METIS_TAC [heap_element_distinct,IN_UNION,IN_INSERT]); 804 805val ADDR_SET_CONS = store_thm("ADDR_SET_CONS", 806 ``!h xs. ADDR_SET (h::xs) = ADDR_SET xs UNION ADDR_SET [h]``, 807 Cases \\ FULL_SIMP_TAC std_ss [ADDR_SET_THM,EXTENSION,IN_UNION] \\ SET_TAC); 808 809val D1_UNION = store_thm("D1_UNION", 810 ``b <= i /\ i <= j ==> (D1(CUT(b,j)m) = D1(CUT(b,i)m) UNION D1(CUT(i,j)m)) /\ 811 (D0(CUT(b,j)m) = D0(CUT(b,i)m) UNION D0(CUT(i,j)m))``, 812 SIMP_TAC std_ss [EXTENSION,IN_UNION] \\ SIMP_TAC std_ss [IN_DEF,D1,CUT_EQ,D0] 813 \\ REPEAT STRIP_TAC \\ `!k. RANGE(b,j)k = RANGE(b,i)k \/ RANGE(i,j)k` by RANGE_TAC 814 \\ SET_TAC); 815 816val D1_CUT_EQ_ADDR_SET_THM = prove( 817 ``(m j = H_BLOCK (x,y,d)) /\ EMP_RANGE (j+1,j+y+1) m ==> 818 (D1 (CUT (j,j + y + 1) m) = ADDR_SET x)``, 819 FULL_SIMP_TAC std_ss [FUN_EQ_THM,D1,CUT_EQ,IN_DEF,APPLY_UPDATE_THM,EMP_RANGE_def] 820 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 821 THEN1 (Cases_on `j = k` \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF] 822 THEN1 METIS_TAC [heap_element_11,heap_element_distinct,PAIR_EQ,ADD_ASSOC] 823 \\ `RANGE (j + 1,j + y + 1) k` by RANGE_TAC 824 \\ METIS_TAC [heap_element_distinct]) 825 \\ Q.EXISTS_TAC `j` \\ ASM_SIMP_TAC std_ss [heap_element_11] \\ RANGE_TAC); 826 827val EQ_RANGE_def = Define ` 828 EQ_RANGE (b,e) m m2 = !k. k IN RANGE (b,e) ==> (m k = m2 k)`; 829 830val EQ_RANGE_IMP_EQ_RANGE = store_thm("EQ_RANGE_IMP_EQ_RANGE", 831 ``!b e i j m m2. EQ_RANGE (b,e) m m2 /\ b <= i /\ j <= e ==> EQ_RANGE (i,j) m m2``, 832 SIMP_TAC std_ss [EQ_RANGE_def,IN_DEF,RANGE_def] \\ REPEAT STRIP_TAC 833 \\ Q.PAT_X_ASSUM `!k.bbb` MATCH_MP_TAC \\ DECIDE_TAC); 834 835val EQ_RANGE_full_heap = store_thm("EQ_RANGE_full_heap", 836 ``!m2 b e m. full_heap b e m /\ EQ_RANGE (b,e) m m2 ==> full_heap b e m2``, 837 STRIP_TAC \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO] \\ HO_MATCH_MP_TAC full_heap_ind 838 \\ REPEAT STRIP_TAC THEN1 METIS_TAC [full_heap_cases] 839 \\ ONCE_REWRITE_TAC [full_heap_cases] \\ IMP_RES_TAC full_heap_LESS_EQ 840 \\ `~(e = b)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 841 \\ `b IN RANGE (b,e)` by (SIMP_TAC std_ss [RANGE_def,IN_DEF] \\ DECIDE_TAC) 842 \\ `m2 b = m b` by METIS_TAC [EQ_RANGE_def] 843 \\ ASM_SIMP_TAC std_ss [heap_element_11] 844 \\ `b <= b + n + 1 /\ e <= e` by DECIDE_TAC \\ REVERSE STRIP_TAC 845 THEN1 (IMP_RES_TAC EQ_RANGE_IMP_EQ_RANGE \\ RES_TAC \\ ASM_SIMP_TAC std_ss []) 846 \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF] 847 \\ REPEAT STRIP_TAC \\ RES_TAC 848 \\ `k IN RANGE (b,e)` suffices_by METIS_TAC [EQ_RANGE_def] 849 \\ FULL_SIMP_TAC std_ss [RANGE_def,IN_DEF] \\ DECIDE_TAC); 850 851val EQ_RANGE_CUT = store_thm("EQ_RANGE_CUT", 852 ``EQ_RANGE (b,i) m (CUT (b,i) m)``, 853 SIMP_TAC std_ss [EQ_RANGE_def,CUT_def,IN_DEF]); 854 855val EQ_RANGE_THM = store_thm("EQ_RANGE_THM", 856 ``(CUT (b,e) m1 = CUT (b,e) m2) ==> EQ_RANGE (b,e) m1 m2``, 857 FULL_SIMP_TAC std_ss [CUT_def,FUN_EQ_THM,EQ_RANGE_def,IN_DEF] \\ SET_TAC); 858 859val move_list_thm = store_thm("move_list_thm", 860 ``!xs z h f m j xs2 j2 (m2:num -> ('a,'b) heap_element). 861 gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,z UNION ADDR_SET xs) /\ 862 ADDR_SET xs SUBSET (DR0(CUT(b2,e2)m)) /\ 863 (rel_move_list (xs,j,m,b,e,b2,e2) = (c,xs2,j2,m2)) ==> 864 ?h3 f3. gc_inv (h1,roots1,h3,f3) (b,i,j2,e,b2,e2,m2,z UNION (D1(CUT(j,j2)m2))) /\ j <= j2 /\ 865 DR0 (CUT (b2,e2) m) SUBSET DR0 (CUT (b2,e2) m2) /\ 866 (CUT(b,j)m = CUT(b,j)m2) /\ 867 (!a. ~(f a = a) ==> (f3 a = f a)) /\ 868 (!a. a IN ADDR_SET xs2 ==> ~(f3 a = a)) /\ 869 (xs2 = ADDR_MAP f3 xs) /\ full_heap j j2 m2 /\ c``, 870 Induct \\ SIMP_TAC std_ss [ADDR_SET_THM,UNION_EMPTY,rel_move_list_def,ADDR_MAP_def, 871 NOT_IN_EMPTY,CUT_EMPTY,LET_DEF,full_heap_REFL] THEN1 SET_TAC 872 \\ ONCE_REWRITE_TAC [ADDR_SET_CONS] 873 \\ NTAC 6 STRIP_TAC \\ FULL_SIMP_TAC std_ss [UNION_SUBSET] 874 \\ `?x3 j3 m3 c3. rel_move (h,j,m,b,e,b2,e2) = (c3,x3,j3,m3)` by METIS_TAC [PAIR] 875 \\ `?xs4 j4 m4 c4. rel_move_list (xs,j3,m3,b,e,b2,e2) = (c4,xs4,j4,m4)` by METIS_TAC [PAIR] 876 \\ FULL_SIMP_TAC std_ss [UNION_ASSOC] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 877 \\ REPEAT STRIP_TAC 878 \\ IMP_RES_TAC move_thm \\ Q.PAT_X_ASSUM `!z roots1 i. bb` (K ALL_TAC) 879 \\ Q.PAT_X_ASSUM `!z h f.bbb` (MP_TAC o Q.SPECL [ 880 `z UNION D1(CUT(j,j3)(m3:num -> ('a,'b) heap_element))`, 881 `h2`,`f2`,`m3`,`j3`,`xs4`,`j4`,`m4`]) 882 \\ `ADDR_SET xs SUBSET DR0 (CUT (b2,e2) m3)` by SET_TAC 883 \\ FULL_SIMP_TAC std_ss [AC UNION_ASSOC UNION_COMM] 884 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [IN_UNION] 885 \\ Q.LIST_EXISTS_TAC [`h3`,`f3`] \\ `j <= j4` by DECIDE_TAC 886 \\ ONCE_REWRITE_TAC [ADDR_SET_CONS] \\ ASM_SIMP_TAC std_ss [] 887 \\ `(CUT (b,j) m3 = CUT (b,j) m4) /\ (CUT (j,j3) m3 = CUT (j,j3) m4)` by 888 (`!k. k < j ==> k < j3` by DECIDE_TAC 889 \\ `!k. j <= k ==> b <= k` by RANGE_TAC 890 \\ FULL_SIMP_TAC std_ss [CUT_def,RANGE_def,FUN_EQ_THM] \\ SET_TAC) 891 \\ IMP_RES_TAC EQ_RANGE_THM \\ IMP_RES_TAC EQ_RANGE_full_heap 892 \\ IMP_RES_TAC full_heap_TRANS \\ ASM_SIMP_TAC std_ss [] 893 \\ REVERSE STRIP_TAC THEN1 894 (ASM_SIMP_TAC std_ss [] \\ STRIP_TAC THEN1 SET_TAC \\ STRIP_TAC THEN1 SET_TAC 895 \\ Cases_on `h` \\ FULL_SIMP_TAC std_ss [ADDR_MAP_def,CONS_11, 896 ADDR_SET_def,MEM,heap_address_11] \\ IMP_RES_TAC gc_inv_IMP 897 \\ `f2 (f2 n) = n` by FULL_SIMP_TAC std_ss [gc_inv_def,FUN_EQ_THM,abs_gc_inv_def,LET_DEF] 898 \\ FULL_SIMP_TAC std_ss []) 899 \\ `D1 (CUT (j,j4) m4) = D1 (CUT (j,j3) m4) UNION D1 (CUT (j3,j4) m4)` 900 by METIS_TAC [D1_UNION] \\ FULL_SIMP_TAC std_ss [AC UNION_ASSOC UNION_COMM]); 901 902val D0_UPDATE = store_thm("D0_UPDATE", 903 ``!i x m. i IN D0 m ==> (D0 ((i =+ H_BLOCK x) m) = D0 m)``, 904 SIMP_TAC std_ss [FORALL_PROD,FUN_EQ_THM,IN_DEF,D0,CUT_EQ,APPLY_UPDATE_THM] 905 \\ METIS_TAC []); 906 907val gc_step_lemma = store_thm("gc_step_lemma", 908 ``gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,D1(CUT(i,j)m)) ==> ~(i = j) ==> 909 ?xs n d. (m i = H_BLOCK (xs,n,d)) /\ 910 EMP_RANGE (i + 1,i + n + 1) m /\ 911 full_heap (i + n + 1) j m /\ 912 ADDR_SET xs SUBSET DR0 (CUT (b2,e2) m) /\ 913 (D1 (CUT (i,j) m) = D1 (CUT (i+n+1,j) m) UNION ADDR_SET xs)``, 914 SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC \\ IMP_RES_TAC gc_inv_IMP 915 \\ `full_heap i j m` by METIS_TAC [gc_inv_def] \\ POP_ASSUM MP_TAC 916 \\ ONCE_REWRITE_TAC [full_heap_cases] \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC 917 \\ ASM_SIMP_TAC std_ss [heap_element_11] \\ STRIP_TAC THEN1 METIS_TAC [full_heap_cases] 918 \\ IMP_RES_TAC full_heap_LESS_EQ 919 \\ `i < i + n + 1 /\ i <= i + n + 1` by DECIDE_TAC 920 \\ `D1 (CUT (i,j) m) = D1 (CUT (i+n+1,j) m) UNION ADDR_SET xs` 921 by METIS_TAC [D1_UNION,D1_CUT_EQ_ADDR_SET_THM,UNION_COMM] 922 \\ ASM_SIMP_TAC std_ss [] 923 \\ `i IN FDOM h /\ (h ' i = (xs,n,d))` by METIS_TAC [gc_inv_def, 924 ref_heap_mem_def, heap_element_distinct,heap_element_11,PAIR_EQ] 925 \\ `i IN (UNIV DIFF D0 (CUT (b,i) m))` by 926 (FULL_SIMP_TAC std_ss [IN_DIFF,IN_UNIV] 927 \\ FULL_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,heap_element_11] \\ RANGE_TAC) 928 \\ `ADDR_SET xs SUBSET POINTERS h (UNIV DIFF D0 (CUT (b,i) m))` 929 by METIS_TAC [set_SUBSET_POINTERS] 930 \\ `D0 (CUT (b,i) m) UNION D0 (CUT (i,j) m) = D0 (CUT(b,j)m)` 931 by METIS_TAC [D1_UNION,gc_inv_def,abs_gc_inv_def] 932 \\ `ADDR_SET xs SUBSET (FDOM h UNION HAS_CHANGED f DIFF (D0 (CUT (b,j) m)))` by 933 (FULL_SIMP_TAC std_ss [gc_inv_def,abs_gc_inv_def,LET_DEF] \\ SET_TAC) 934 \\ SIMP_TAC std_ss [SUBSET_DEF] \\ REPEAT STRIP_TAC 935 \\ `x IN (FDOM h UNION HAS_CHANGED f DIFF D0 (CUT (b,j) m))` by SET_TAC 936 \\ Cases_on `x IN FDOM h` THEN1 937 (`~(x IN D0 (CUT (b,j) m))` by SET_TAC 938 \\ POP_ASSUM MP_TAC \\ SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ] 939 \\ `?x1 y1 d1. h ' x = (x1,y1,d1)` by METIS_TAC [PAIR] 940 \\ `m x = H_BLOCK (x1,y1,d1)` by METIS_TAC [ref_heap_mem_def,gc_inv_def] 941 \\ FULL_SIMP_TAC std_ss [heap_element_11,DR0,D0,R0,CUT_EQ, 942 heap_element_distinct,IN_DEF] \\ CCONTR_TAC 943 \\ FULL_SIMP_TAC std_ss [gc_inv_def,abs_gc_inv_def,LET_DEF] 944 \\ METIS_TAC [heap_element_distinct]) 945 \\ FULL_SIMP_TAC std_ss [IN_DIFF,IN_UNION] 946 \\ Q.PAT_X_ASSUM `~(x IN D0 (CUT (b,j) m))` MP_TAC 947 \\ SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ] 948 \\ FULL_SIMP_TAC std_ss [HAS_CHANGED_def] 949 \\ FULL_SIMP_TAC std_ss [gc_inv_def,abs_gc_inv_def,LET_DEF] 950 \\ `m x = H_REF (f x)` by METIS_TAC [ref_heap_mem_def] 951 \\ FULL_SIMP_TAC std_ss [heap_element_distinct,DR0,D0,R0,CUT_EQ,heap_element_11] 952 \\ SIMP_TAC std_ss [IN_DEF] 953 \\ `full_heap b j m` by METIS_TAC [full_heap_TRANS] 954 \\ `R0 m x` by FULL_SIMP_TAC std_ss [R0,heap_element_11] 955 \\ CCONTR_TAC \\ METIS_TAC [full_heap_R0,heap_element_distinct]); 956 957val gc_step_thm = store_thm("gc_step_thm", 958 ``gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,D1(CUT(i,j)m)) /\ ~(i = j) ==> 959 (rel_gc_step (i,j,m,b,e,b2,e2) = (c,i2,j2,m2)) ==> 960 ?h3 f3. gc_inv (h1,roots1,h3,f3) (b,i2,j2,e,b2,e2,m2,D1(CUT(i2,j2)m2)) /\ 961 i < i2 /\ j <= j2 /\ c /\ !a. ~(f a = a) ==> (f3 a = f a)``, 962 STRIP_TAC \\ IMP_RES_TAC gc_inv_IMP \\ STRIP_ASSUME_TAC (UNDISCH_ALL gc_step_lemma) 963 \\ ASM_SIMP_TAC std_ss [rel_gc_step_def,LET_DEF,getBLOCK_def] 964 \\ `?xs3 j3 m3 c3. rel_move_list (xs,j,m,b,e,b2,e2) = (c3,xs3,j3,m3)` by METIS_TAC [PAIR] 965 \\ FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ helperLib.EXPAND_TAC 966 \\ `~RANGE(i + n + 1,j3)i` by RANGE_TAC \\ FULL_SIMP_TAC std_ss [CUT_UPDATE] 967 \\ IMP_RES_TAC full_heap_LESS_EQ 968 \\ `i < i + n + 1 /\ i <= i + n + 1` by DECIDE_TAC 969 \\ FULL_SIMP_TAC std_ss [] 970 \\ Q.PAT_X_ASSUM `gc_inv (h1,roots1,h,f) xxx` (fn th => ASSUME_TAC th THEN 971 MP_TAC (Q.INST [`xs2`|->`xs3`,`j2`|->`j3`,`m2`|->`m3`,`c`|->`c3`] 972 (helperLib.MATCH_INST (SPEC_ALL move_list_thm) (concl th)))) 973 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 974 \\ `CUT (i + n + 1,j) m = CUT (i + n + 1,j) m3` by 975 (FULL_SIMP_TAC std_ss [gc_inv_def,abs_gc_inv_def,LET_DEF] 976 \\ `!k. i + n + 1 <= k ==> b <= k` by DECIDE_TAC 977 \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM,CUT_def,RANGE_def] \\ SET_TAC) 978 \\ `i + n + 1 <= j` by RANGE_TAC 979 \\ `D1 (CUT (i + n + 1,j) m3) UNION D1 (CUT (j,j3) m3) = D1 (CUT (i + n + 1,j3) m3)` 980 by METIS_TAC [D1_UNION,gc_inv_def,abs_gc_inv_def] 981 \\ FULL_SIMP_TAC std_ss [] \\ Q.LIST_EXISTS_TAC [`h3 |+ (i,ADDR_MAP f3 xs,n,d)`,`f3`] 982 \\ `~RANGE(b2,e2)i /\ RANGE(b,j3)i /\ RANGE(b,i+n+1)i` by RANGE_TAC 983 \\ FULL_SIMP_TAC std_ss [gc_inv_def,CUT_UPDATE] 984 \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM] 985 \\ `i IN D0 (CUT (b,i + n + 1) m3) /\ 986 (m3 i = H_BLOCK (xs,n,d))` by 987 (`!k. k < i + n + 1 ==> k < j` by DECIDE_TAC 988 \\ FULL_SIMP_TAC std_ss [] 989 \\ `CUT (b,i+n+1) m3 = CUT (b,i+n+1) m` by 990 (FULL_SIMP_TAC std_ss [CUT_def,RANGE_def] \\ SET_TAC) 991 \\ `(CUT(b,i+n+1)m3) i = H_BLOCK (xs,n,d)` by 992 (FULL_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [CUT_EQ,IN_DEF]) 993 \\ FULL_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,heap_element_11]) 994 \\ REVERSE STRIP_TAC 995 THEN1 (ASM_SIMP_TAC std_ss [isBLOCK_def] \\ `RANGE (b,e) i` by RANGE_TAC 996 \\ ASM_SIMP_TAC (srw_ss()) [] 997 \\ `~(i = j3)` by RANGE_TAC 998 \\ Q.PAT_X_ASSUM `full_heap i j3 m3` MP_TAC 999 \\ ASM_SIMP_TAC (srw_ss()) [Once full_heap_cases] 1000 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC full_heap_LESS_EQ) 1001 \\ STRIP_TAC THEN1 RANGE_TAC \\ STRIP_TAC THEN1 METIS_TAC [] 1002 \\ FULL_SIMP_TAC std_ss [D0_UPDATE] 1003 \\ STRIP_TAC THEN1 1004 (MATCH_MP_TAC (RW[AND_IMP_INTRO]full_heap_step) 1005 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,heap_element_11,EMP_RANGE_def,IN_DEF] 1006 \\ STRIP_TAC THEN1 METIS_TAC [full_heap_BLOCK] 1007 \\ FULL_SIMP_TAC std_ss [CUT_def,FUN_EQ_THM] \\ REPEAT STRIP_TAC 1008 \\ `RANGE (b,j) k /\ ~(RANGE (i + 1,i + n + 1) i)` by RANGE_TAC \\ SET_TAC) 1009 \\ STRIP_TAC THEN1 1010 (FULL_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,heap_element_11] 1011 \\ `~(i = j3)` by RANGE_TAC 1012 \\ METIS_TAC [full_heap_BLOCK,full_heap_cases,heap_element_11,PAIR_EQ]) 1013 \\ STRIP_TAC THEN1 1014 (Q.EXISTS_TAC `len'` \\ ASM_SIMP_TAC std_ss [] 1015 \\ MATCH_MP_TAC part_heap_IGNORE \\ ASM_SIMP_TAC std_ss []) 1016 \\ REPEAT STRIP_TAC THEN1 1017 (FULL_SIMP_TAC std_ss [ref_heap_mem_def,APPLY_UPDATE_THM,FDOM_FUPDATE,IN_INSERT] 1018 \\ REPEAT STRIP_TAC \\ Cases_on `i = a` 1019 \\ FULL_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM]) 1020 \\ MATCH_MP_TAC abs_steps_TRANS 1021 \\ Q.EXISTS_TAC `(h3,D0 (CUT (b,i) m3),D0 (CUT (i,j3) m3), 1022 D1 (CUT (i + n + 1,j3) m3),f3)` \\ ASM_SIMP_TAC std_ss [] 1023 \\ SIMP_TAC std_ss [abs_steps_def] 1024 \\ MATCH_MP_TAC RTC_SINGLE 1025 \\ SIMP_TAC std_ss [abs_step_cases] \\ DISJ2_TAC \\ DISJ1_TAC 1026 \\ Q.LIST_EXISTS_TAC [`i`,`xs`,`(n,d)`] \\ ASM_SIMP_TAC std_ss [] 1027 \\ IMP_RES_TAC ok_heap_IMP \\ IMP_RES_TAC abs_steps_thm \\ POP_ASSUM (K ALL_TAC) 1028 \\ `f3 o f3 = I` by FULL_SIMP_TAC std_ss [gc_inv_def,abs_gc_inv_def,LET_DEF] 1029 \\ FULL_SIMP_TAC std_ss [SET_TRANSLATE_MAP,SET_TRANSLATE_def] 1030 \\ Q.PAT_X_ASSUM `!a. bbb` (MP_TAC o Q.GEN `a` o Q.SPEC `(f3:num->num) a`) 1031 \\ `!k. f3 (f3 k) = (k:num)` by FULL_SIMP_TAC std_ss [FUN_EQ_THM] 1032 \\ FULL_SIMP_TAC std_ss [] \\ STRIP_TAC 1033 \\ FULL_SIMP_TAC std_ss [SET_EQ_SUBSET,GSYM SUBSET_INSERT_DELETE,INSERT_SUBSET] 1034 \\ SIMP_TAC std_ss [SUBSET_DEF,IN_INSERT,IN_DELETE] 1035 \\ `RANGE (i,j3) i` by RANGE_TAC 1036 \\ ASM_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,heap_element_11] 1037 \\ REVERSE (REPEAT STRIP_TAC) 1038 THEN1 METIS_TAC [heap_element_distinct,ref_heap_mem_def,heap_element_11,PAIR_EQ] 1039 THEN1 1040 (FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF,heap_element_11] 1041 \\ CCONTR_TAC \\ FULL_SIMP_TAC std_ss [] 1042 \\ `RANGE(i+1,i+n+1)x /\ RANGE(b,j)x` by RANGE_TAC \\ RES_TAC 1043 \\ FULL_SIMP_TAC std_ss [CUT_def,FUN_EQ_THM] \\ METIS_TAC [heap_element_distinct]) 1044 THEN1 (FULL_SIMP_TAC std_ss [heap_element_11] \\ RANGE_TAC) 1045 THEN1 (FULL_SIMP_TAC std_ss [heap_element_11] \\ RANGE_TAC) 1046 THEN1 (FULL_SIMP_TAC std_ss [heap_element_11] \\ RANGE_TAC) 1047 THEN1 1048 (FULL_SIMP_TAC std_ss [heap_element_11] 1049 \\ REVERSE (Cases_on `RANGE(i+1,i+n+1)x`) THEN1 RANGE_TAC 1050 \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF,heap_element_11] 1051 \\ FULL_SIMP_TAC std_ss [CUT_def,FUN_EQ_THM] 1052 \\ `m x = H_EMP` by SET_TAC 1053 \\ `RANGE(b,j)x` by RANGE_TAC \\ RES_TAC 1054 \\ FULL_SIMP_TAC std_ss [CUT_def,FUN_EQ_THM] \\ METIS_TAC [heap_element_distinct])); 1055 1056val gc_loop_thm = store_thm("gc_loop_thm", 1057 ``!j h f m i2 m2 c2. 1058 gc_inv (h1,roots1,h,f) (b,i,j,e,b2,e2,m,D1(CUT(i,j)m)) ==> 1059 (rel_gc_loop (i,j,m,b,e,b2,e2) = (c2,i2,m2)) ==> 1060 ?h4 f4. gc_inv (h1,roots1,h4,f4) (b,i2,i2,e,b2,e2,m2,{}) /\ j <= i2 /\ c2 /\ 1061 !a. f a <> a ==> (f4 a = f a)``, 1062 completeInduct_on `e - i` \\ NTAC 4 STRIP_TAC \\ Cases_on `i = j` 1063 \\ ONCE_REWRITE_TAC [rel_gc_loop_def] \\ ASM_SIMP_TAC std_ss [CUT_EMPTY] THEN1 SET_TAC 1064 \\ NTAC 7 STRIP_TAC \\ `?i3 j3 m3 c3. rel_gc_step (i,j,m,b,e,b2,e2) = (c3,i3,j3,m3)` by METIS_TAC [PAIR] 1065 \\ FULL_SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC \\ IMP_RES_TAC gc_step_thm 1066 \\ `i < j /\ j <= e` by RANGE_TAC \\ FULL_SIMP_TAC std_ss [] 1067 \\ Q.PAT_X_ASSUM `xxxx = (c2,i2,m2)` MP_TAC 1068 \\ CONV_TAC (DEPTH_CONV (helperLib.FORCE_PBETA_CONV)) 1069 \\ SIMP_TAC bool_ss [PAIR] \\ REPEAT STRIP_TAC 1070 \\ `(e - i3 < e - i) /\ (e - i3 = e - i3)` by RANGE_TAC 1071 \\ RES_TAC \\ IMP_RES_TAC LESS_EQ_TRANS \\ ASM_SIMP_TAC std_ss [] \\ SET_TAC); 1072 1073val ok_full_heap_def = Define ` 1074 ok_full_heap (h,roots) (b,i,e,b2,e2,m) = 1075 b <= i /\ i <= e /\ b2 <= e2 /\ (e2 - b2 = e - b) /\ (~(e2 <= b) ==> e <= b2) /\ 1076 (!k. ~RANGE (b,i) k ==> (m k = H_EMP)) /\ 1077 (?t. part_heap b i m t) /\ ref_heap_mem (h,I) m /\ ok_heap (h,roots)`; 1078 1079val ok_full_heap_IMP = store_thm("ok_full_heap_IMP", 1080 ``ok_full_heap (h,roots) (b2,i,e2,b,e,m) ==> 1081 gc_inv (h,roots,h,I) (b,b,b,e,b2,e2,m,ADDR_SET roots) /\ 1082 ADDR_SET roots SUBSET DR0 (CUT (b2,e2) m)``, 1083 STRIP_TAC \\ FULL_SIMP_TAC std_ss [gc_inv_def,ok_full_heap_def,full_heap_REFL] 1084 \\ IMP_RES_TAC ok_heap_IMP \\ REPEAT STRIP_TAC 1085 \\ FULL_SIMP_TAC std_ss [CUT_EMPTY] 1086 THEN1 (Q.PAT_X_ASSUM `!k.bb` MATCH_MP_TAC \\ RANGE_TAC) 1087 THEN1 (`part_heap i e2 m 0` by 1088 (MATCH_MP_TAC part_heap_EMP_RANGE \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF] 1089 \\ REPEAT STRIP_TAC \\ `~RANGE (b2,i) k` by RANGE_TAC \\ RES_TAC) 1090 \\ IMP_RES_TAC part_heap_TRANS \\ Q.EXISTS_TAC `t` \\ FULL_SIMP_TAC std_ss [] 1091 \\ IMP_RES_TAC part_heap_LENGTH_LESS_EQ) 1092 \\ SIMP_TAC std_ss [abs_steps_def,RTC_REFL] 1093 \\ FULL_SIMP_TAC std_ss [ok_heap_def,UNION_SUBSET] 1094 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF] \\ REPEAT STRIP_TAC \\ RES_TAC 1095 \\ SIMP_TAC std_ss [DR0,D0,R0,CUT_EQ,IN_DEF] \\ DISJ1_TAC 1096 \\ `?x1 x2 x3. h ' x = (x1,x2,x3)` by METIS_TAC [PAIR] 1097 \\ Cases_on `m x` \\ POP_ASSUM MP_TAC 1098 \\ FULL_SIMP_TAC std_ss [ref_heap_mem_def,heap_element_distinct] 1099 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [heap_element_11] 1100 \\ `RANGE (b2,i) x` by METIS_TAC [heap_element_distinct] 1101 \\ REPEAT STRIP_TAC \\ RANGE_TAC); 1102 1103val full_heap_IMP_part_heap = store_thm("full_heap_IMP_part_heap", 1104 ``!b e m. full_heap b e m ==> part_heap b e m (e-b)``, 1105 HO_MATCH_MP_TAC full_heap_ind \\ REPEAT STRIP_TAC 1106 THEN1 (SIMP_TAC std_ss [] \\ METIS_TAC [part_heap_cases]) 1107 \\ ONCE_REWRITE_TAC [part_heap_cases] \\ DISJ2_TAC \\ DISJ2_TAC 1108 \\ ASM_SIMP_TAC std_ss [CUT_EQ,heap_element_11] 1109 \\ Q.EXISTS_TAC `e - (b + n + 1)` \\ ASM_SIMP_TAC std_ss [] 1110 \\ IMP_RES_TAC full_heap_LESS_EQ \\ DECIDE_TAC); 1111 1112val gc_thm = store_thm("gc_thm", 1113 ``ok_full_heap (h,roots) (b2,i,e2,b,e,m) ==> 1114 (rel_gc (b2,e2,b,e,roots,m) = (c,b,i2,e,b2,e2,roots2,m2)) ==> 1115 ?h2. ok_full_heap (h2,roots2) (b,i2,e,b2,e2,m2) /\ 1116 gc_exec (h,roots) (h2,roots2) /\ full_heap b i2 m2 /\ c``, 1117 STRIP_TAC \\ IMP_RES_TAC ok_full_heap_IMP 1118 \\ SIMP_TAC std_ss [rel_gc_def,LET_DEF] 1119 \\ `?r3 b3 m3 c3. rel_move_list (roots,b,m,b,e,b2,e2) = (c3,r3,b3,m3)` by METIS_TAC [PAIR] 1120 \\ `?i4 m4 c4. rel_gc_loop (b,b3,m3,b,e,b2,e2) = (c4,i4,m4)` by METIS_TAC [PAIR] 1121 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 1122 \\ IMP_RES_TAC (RW [UNION_EMPTY] (helperLib.SUBST_INST [``z:num set``|->``{}:num set``] move_list_thm)) 1123 \\ Q.PAT_X_ASSUM `gc_inv (h,roots,h3,f3) ttt` MP_TAC 1124 \\ REPEAT (Q.PAT_X_ASSUM `gc_inv xxx yyy` (K ALL_TAC)) \\ STRIP_TAC 1125 \\ IMP_RES_TAC (GEN_ALL (RW [] (Q.INST [`c`|->`T`] (SPEC_ALL gc_loop_thm)))) 1126 \\ Q.PAT_X_ASSUM `r3 = ADDR_MAP f3 roots` MP_TAC 1127 \\ REPEAT (Q.PAT_X_ASSUM `r3 = ADDR_MAP xx roots` (K ALL_TAC)) \\ STRIP_TAC 1128 \\ FULL_SIMP_TAC std_ss [] 1129 \\ `f3 o f3 = I` by 1130 (FULL_SIMP_TAC std_ss [gc_inv_def] 1131 \\ IMP_RES_TAC ok_heap_IMP \\ IMP_RES_TAC abs_steps_thm 1132 \\ FULL_SIMP_TAC std_ss [abs_gc_inv_def,LET_DEF,gc_inv_def]) 1133 \\ Q.PAT_X_ASSUM `gc_inv (h,roots,h4,f4) ttt` MP_TAC 1134 \\ REPEAT (Q.PAT_X_ASSUM `gc_inv xxx yyy` (K ALL_TAC)) 1135 \\ SIMP_TAC std_ss [gc_inv_def] \\ REPEAT STRIP_TAC 1136 \\ Q.EXISTS_TAC `DRESTRICT h4 (D0 (CUT (b,i4) m4))` 1137 \\ FULL_SIMP_TAC std_ss [CUT_EMPTY] \\ helperLib.CLEAN_TAC 1138 \\ `gc_exec (h,roots) (DRESTRICT h4 (D0 (CUT (b,i4) m4)),ADDR_MAP f3 roots)` by 1139 (MATCH_MP_TAC abs_gc_thm \\ ASM_SIMP_TAC std_ss [] 1140 \\ SIMP_TAC std_ss [abs_gc_cases] 1141 \\ Q.LIST_EXISTS_TAC [`h4`,`f4`,`(D0 (CUT (b,i4) m4))`] 1142 \\ ASM_SIMP_TAC std_ss [ADDR_MAP_EQ_ADDR_MAP] 1143 \\ FULL_SIMP_TAC std_ss [SET_TRANSLATE_MAP,SET_TRANSLATE_def] 1144 \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ SET_TAC) 1145 \\ IMP_RES_TAC gc_exec_thm \\ ASM_SIMP_TAC std_ss [] 1146 \\ `full_heap b i4 (CUT (b,i4) m4)` by 1147 (MATCH_MP_TAC full_heap_IGNORE \\ Q.EXISTS_TAC `m4` 1148 \\ ASM_SIMP_TAC std_ss [CUT_def]) 1149 \\ FULL_SIMP_TAC std_ss [ok_full_heap_def] \\ REPEAT STRIP_TAC 1150 THEN1 RANGE_TAC THEN1 FULL_SIMP_TAC std_ss [CUT_def,IN_DEF] 1151 THEN1 METIS_TAC [full_heap_IMP_part_heap,EQ_RANGE_full_heap,EQ_RANGE_CUT] 1152 \\ FULL_SIMP_TAC std_ss [ref_heap_mem_def,FUN_EQ_THM,FDOM_DRESTRICT,IN_INTER] 1153 \\ ASM_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ] 1154 \\ REPEAT STRIP_TAC \\ CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [CUT_def])) 1155 \\ Cases_on `RANGE (b,i4) a` \\ ASM_SIMP_TAC std_ss [IN_DEF] 1156 \\ Cases_on `FDOM h4 a` \\ ASM_SIMP_TAC std_ss [IN_DEF] THEN1 1157 (`?x1 x2 x3. h4 ' a = (x1,x2,x3)` by METIS_TAC [PAIR] 1158 \\ ASM_SIMP_TAC std_ss [heap_element_11,DRESTRICT_DEF,IN_INTER] 1159 \\ FULL_SIMP_TAC std_ss [IN_DEF,D0,CUT_EQ,heap_element_11]) 1160 \\ Cases_on `f4 a = a` \\ ASM_SIMP_TAC std_ss [heap_element_distinct] 1161 \\ FULL_SIMP_TAC std_ss [abs_gc_inv_def,LET_DEF,NOT_IN_EMPTY,IN_UNION] 1162 \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM] 1163 \\ `R0 m4 a` by FULL_SIMP_TAC std_ss [R0,IN_DEF,heap_element_11] 1164 \\ METIS_TAC [full_heap_R0]); 1165 1166(* split the memory *) 1167 1168val split_move_def = Define ` 1169 (split_move (H_DATA x,j,mF,mT,e) = (T,H_DATA x,j,mF,mT)) /\ 1170 (split_move (H_ADDR a,j,mF,mT,e) = 1171 case mF a of 1172 H_EMP => (F,ARB) 1173 | H_REF i => (a < e,H_ADDR i,j,mF,mT) 1174 | H_BLOCK (xs,n,d) => let cond = a < e in 1175 let mF = (a =+ H_REF j) mF in 1176 let cond = j < e /\ (mT j = H_EMP) /\ cond in 1177 let mT = (j =+ H_BLOCK (xs,n,d)) mT in 1178 (cond,H_ADDR j,j + n + 1,mF,mT))`; 1179 1180val split_move_list_def = Define ` 1181 (split_move_list ([],j,mF,mT,e) = (T,[],j,mF,mT)) /\ 1182 (split_move_list (x::xs,j,mF,mT,e) = 1183 let (c1,x,j,mF,mT) = split_move (x,j,mF,mT,e) in 1184 let (c2,xs,j,mF,mT) = split_move_list (xs,j,mF,mT,e) in 1185 (c1 /\ c2,x::xs,j,mF,mT))`; 1186 1187val split_gc_step_def = Define ` 1188 split_gc_step (i,j,mF,mT,e) = 1189 let cond = isBLOCK (mT i) /\ i < e in 1190 let (xs,n,d) = getBLOCK (mT i) in 1191 let (c2,ys,j,mF,mT) = split_move_list (xs,j,mF,mT,e) in 1192 let cond = cond /\ (mT i = H_BLOCK (xs,n,d)) /\ c2 in 1193 let mT = (i =+ H_BLOCK (ys,n,d)) mT in 1194 let i = i + n + 1 in 1195 let cond = cond /\ i <= j in 1196 (cond,i,j,mF,mT)`; 1197 1198val split_gc_loop_def = tDefine "split_gc_loop" ` 1199 split_gc_loop (i,j,mF,mT,e) = 1200 if i = j then (T,i,mF,mT) else 1201 if ~(i < j /\ j <= e) then (F,ARB) else 1202 let (c1,i,j,mF,mT) = split_gc_step (i,j,mF,mT,e) in 1203 let (c2,i,mF,mT) = split_gc_loop (i,j,mF,mT,e) in 1204 (c1 /\ c2,i,mF,mT)` 1205 (WF_REL_TAC `measure (\(i,j,mF,mT,e). e - i)` 1206 \\ SIMP_TAC std_ss [split_gc_step_def,LET_DEF] 1207 \\ CONV_TAC (DEPTH_CONV (helperLib.FORCE_PBETA_CONV)) 1208 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 1209 \\ SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ DECIDE_TAC); 1210 1211val split_gc_def = Define ` 1212 split_gc (roots,mF,mT,e) = 1213 let (cond,roots,j,mF,mT) = split_move_list (roots,0,mF,mT,e) in 1214 let (c,i,mF,mT) = split_gc_loop (0,j,mF,mT,e) in 1215 let mT = CUT (0,i) mT in 1216 (c /\ cond,i,roots,mT,e)`; 1217 1218(* connection *) 1219 1220val ADDR_APPLY_def = Define ` 1221 (ADDR_APPLY f (H_ADDR a) = H_ADDR (f a)) /\ 1222 (ADDR_APPLY f (H_DATA x) = H_DATA x)`; 1223 1224val BLOCK_APPLY_def = Define ` 1225 (BLOCK_APPLY f (H_BLOCK (xs,d)) = H_BLOCK (ADDR_MAP f xs,d)) /\ 1226 (BLOCK_APPLY f (H_REF i) = H_REF i) /\ 1227 (BLOCK_APPLY f (H_EMP) = H_EMP)`; 1228 1229val memF_def = Define ` 1230 memF m e = \a. if a < e then BLOCK_APPLY (\a. a - e) (m (a+e:num)) else H_EMP`; 1231 1232val memT_def = Define ` 1233 memT m e i = \a. if e <= a:num then H_EMP else 1234 if a < i then m a else BLOCK_APPLY (\a. a - e) (m a)`; 1235 1236val memF_UPDATE = prove( 1237 ``(j < e ==> (memF ((j =+ x) m) e = memF m e)) /\ 1238 (RANGE (e,e + e) n ==> (memF ((n =+ x) m) e = (n - e =+ BLOCK_APPLY (\a. a - e) x) (memF m e)))``, 1239 REPEAT STRIP_TAC THEN1 1240 (`!a. ~(j = a + e)` by (STRIP_TAC \\ DECIDE_TAC) 1241 \\ ASM_SIMP_TAC std_ss [memF_def,APPLY_UPDATE_THM]) 1242 \\ ASM_SIMP_TAC std_ss [memF_def,APPLY_UPDATE_THM,FUN_EQ_THM] 1243 \\ REPEAT STRIP_TAC \\ Cases_on `x' = n - e` 1244 THEN1 (`n - e < e /\ (n - e + e = n)` by RANGE_TAC \\ FULL_SIMP_TAC std_ss []) 1245 \\ `~(n = x' + e)` by RANGE_TAC \\ ASM_SIMP_TAC std_ss []); 1246 1247val memT_UPDATE = prove( 1248 ``((RANGE (e,e + e) n ==> (memT ((n =+ x) m) e i = memT m e i))) /\ 1249 (i <= j /\ j < e ==> 1250 (memT ((j =+ x) m) e i = (j =+ BLOCK_APPLY (\a. a - e) x) (memT m e i)))``, 1251 REPEAT STRIP_TAC THEN1 1252 (ASM_SIMP_TAC std_ss [memT_def,APPLY_UPDATE_THM,FUN_EQ_THM] 1253 \\ STRIP_TAC \\ Q.SPEC_TAC (`x'`,`a`) 1254 \\ STRIP_TAC \\ Cases_on `e <= a` \\ ASM_SIMP_TAC std_ss [] 1255 \\ Cases_on `a < i` \\ ASM_SIMP_TAC std_ss [] 1256 \\ `~(n = a)` by RANGE_TAC \\ ASM_SIMP_TAC std_ss []) 1257 \\ ASM_SIMP_TAC std_ss [memT_def,APPLY_UPDATE_THM,FUN_EQ_THM] 1258 \\ STRIP_TAC \\ Q.SPEC_TAC (`x'`,`a`) \\ STRIP_TAC 1259 \\ Cases_on `j = a` \\ ASM_SIMP_TAC std_ss [] 1260 \\ `~(e <= a) /\ ~(a < i)` by RANGE_TAC \\ ASM_SIMP_TAC std_ss []); 1261 1262val spilt_move_thm = prove( 1263 ``(rel_move (x,j,m,0,e,e,e+e) = (T,x2,j2,m2)) /\ i <= j ==> 1264 (split_move (ADDR_APPLY (\a. a - e) x,j,memF m e,memT m e i,e) = 1265 (T,x2,j2,memF m2 e,memT m2 e i)) /\ j <= j2``, 1266 ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ REVERSE (Cases_on `x`) 1267 \\ SIMP_TAC std_ss [rel_move_def,split_move_def,ADDR_APPLY_def] 1268 \\ Cases_on `m n` \\ ASM_SIMP_TAC (srw_ss()) [] \\ STRIP_TAC THEN1 1269 (`memF m e (n - e) = H_REF n'` by 1270 (FULL_SIMP_TAC std_ss [memF_def] 1271 \\ `n < e + e /\ 0 < e /\ (n - e + e = n)` by RANGE_TAC 1272 \\ ASM_SIMP_TAC std_ss [BLOCK_APPLY_def]) 1273 \\ ASM_SIMP_TAC (srw_ss()) [] \\ RANGE_TAC) 1274 \\ `?xs n d. p = (xs,n,d)` by METIS_TAC [PAIR] 1275 \\ FULL_SIMP_TAC (srw_ss()) [LET_DEF] 1276 \\ `n < e + e /\ 0 < e /\ (n - e + e = n) /\ j < e /\ ~(n = j)` by RANGE_TAC 1277 \\ `memF m e (n - e) = H_BLOCK (ADDR_MAP (\a. a - e) xs,n',d)` by 1278 (ASM_SIMP_TAC std_ss [memF_def] 1279 \\ ASM_SIMP_TAC std_ss [BLOCK_APPLY_def]) 1280 \\ ASM_SIMP_TAC (srw_ss()) [DECIDE ``j <= j + n + 1``] 1281 \\ REPEAT STRIP_TAC 1282 THEN1 (FULL_SIMP_TAC std_ss [memT_def,BLOCK_APPLY_def,APPLY_UPDATE_THM]) 1283 \\ ASM_SIMP_TAC std_ss [memF_UPDATE,BLOCK_APPLY_def,memT_UPDATE]); 1284 1285val ADDR_MAP_CONS = prove( 1286 ``!x xs f. ADDR_MAP f (x::xs) = ADDR_APPLY f x :: ADDR_MAP f xs``, 1287 Cases \\ ASM_SIMP_TAC std_ss [ADDR_APPLY_def,ADDR_MAP_def]); 1288 1289val spilt_move_list_thm = prove( 1290 ``!xs j m xs2 j2 m2. 1291 (rel_move_list (xs,j,m,0,e,e,e+e) = (T,xs2,j2,m2)) /\ i <= j ==> 1292 (split_move_list (ADDR_MAP (\a. a - e) xs,j,memF m e,memT m e i,e) = 1293 (T,xs2,j2,memF m2 e,memT m2 e i))``, 1294 Induct \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 1295 \\ SIMP_TAC std_ss [rel_move_list_def,ADDR_MAP_def,split_move_list_def] 1296 \\ NTAC 3 STRIP_TAC 1297 \\ `?c1 x1 j1 m1. rel_move (h,j,m,0,e,e,e + e) = (c1,x1,j1,m1)` by METIS_TAC [PAIR] 1298 \\ `?c3 xs3 j3 m3. rel_move_list (xs,j1,m1,0,e,e,e + e) = (c3,xs3,j3,m3)` by METIS_TAC [PAIR] 1299 \\ ASM_SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC 1300 \\ FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC spilt_move_thm 1301 \\ ASM_SIMP_TAC std_ss [ADDR_MAP_CONS,split_move_list_def,LET_DEF] 1302 \\ `i <= j1` by DECIDE_TAC \\ RES_TAC \\ ASM_SIMP_TAC std_ss []); 1303 1304val spilt_gc_step_thm = prove( 1305 ``(rel_gc_step (i,j,m,0,e,e,e+e) = (T,i2,j2,m2)) /\ i <= j /\ i <= e ==> 1306 (split_gc_step (i,j,memF m e,memT m e i,e) = (T,i2,j2,memF m2 e,memT m2 e i2)) /\ i2 <= j2 /\ i < i2``, 1307 ONCE_REWRITE_TAC [EQ_SYM_EQ] 1308 \\ SIMP_TAC std_ss [rel_gc_step_def,split_gc_step_def] 1309 \\ `?xs n d. getBLOCK (m i) = (xs,n,d)` by METIS_TAC [PAIR] 1310 \\ `?c3 xs3 j3 m3. rel_move_list (xs,j,m,0,e,e,e + e) = (c3,xs3,j3,m3)` by METIS_TAC [PAIR] 1311 \\ ASM_SIMP_TAC std_ss [LET_DEF] \\ STRIP_TAC 1312 \\ FULL_SIMP_TAC std_ss [DECIDE ``i < i + n + 1:num``] 1313 \\ IMP_RES_TAC spilt_move_list_thm 1314 \\ Q.PAT_X_ASSUM `!x.bb` (K ALL_TAC) 1315 \\ `i < e` by RANGE_TAC 1316 \\ `~(e <= i)` by RANGE_TAC 1317 \\ `memT m e i i = H_BLOCK (ADDR_MAP (\a. a - e) xs,n,d)` by 1318 (ASM_SIMP_TAC std_ss [memT_def] \\ Cases_on `m i` 1319 \\ FULL_SIMP_TAC (srw_ss()) [isBLOCK_def,getBLOCK_def,BLOCK_APPLY_def]) 1320 \\ ASM_SIMP_TAC std_ss [getBLOCK_def,GSYM CONJ_ASSOC] 1321 \\ STRIP_TAC THEN1 METIS_TAC [isBLOCK_def] 1322 \\ ASM_SIMP_TAC std_ss [memF_UPDATE] 1323 \\ ASM_SIMP_TAC std_ss [memT_def,BLOCK_APPLY_def] 1324 \\ SIMP_TAC std_ss [FUN_EQ_THM,APPLY_UPDATE_THM] \\ STRIP_TAC 1325 \\ Cases_on `i = a` \\ ASM_SIMP_TAC std_ss [] 1326 THEN1 (`~(e <= a) /\ a < a + n + 1` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss []) 1327 \\ Cases_on `e <= a` \\ ASM_SIMP_TAC std_ss [] 1328 \\ Cases_on `a < i` \\ ASM_SIMP_TAC std_ss [] 1329 THEN1 (`a < i + n + 1` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss []) 1330 \\ Cases_on `a < i + n + 1` \\ ASM_SIMP_TAC std_ss [] 1331 \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF] 1332 \\ `RANGE (i + 1,i + n + 1) a` by RANGE_TAC 1333 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [BLOCK_APPLY_def]); 1334 1335val spilt_gc_loop_thm = prove( 1336 ``!i e j m i2 m2. 1337 (rel_gc_loop (i,j,m,0,e,e,e+e) = (T,i2,m2)) /\ i <= j ==> 1338 (split_gc_loop (i,j,memF m e,memT m e i,e) = (T,i2,memF m2 e,memT m2 e i2))``, 1339 completeInduct_on `e-i:num` \\ NTAC 7 STRIP_TAC 1340 \\ ONCE_REWRITE_TAC [split_gc_loop_def,rel_gc_loop_def] 1341 \\ Cases_on `i = j` \\ ASM_SIMP_TAC std_ss [] 1342 \\ Cases_on `i < j` \\ ASM_SIMP_TAC std_ss [] 1343 \\ Cases_on `j <= e` \\ ASM_SIMP_TAC std_ss [] 1344 \\ `?c3 i3 j3 m3. rel_gc_step (i,j,m,0,e,e,e + e) = (c3,i3,j3,m3)` by METIS_TAC [PAIR] 1345 \\ `?c4 i4 m4. rel_gc_loop (i3,j3,m3,0,e,e,e + e) = (c4,i4,m4)` by METIS_TAC [PAIR] 1346 \\ ASM_SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC 1347 \\ `i <= e /\ i < j` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [] 1348 \\ IMP_RES_TAC spilt_gc_step_thm \\ REPEAT (Q.PAT_X_ASSUM `!x y.bb` (K ALL_TAC)) 1349 \\ ASM_SIMP_TAC std_ss [] 1350 \\ `e - i3 < e - i /\ (e - i3 = e - i3)` by DECIDE_TAC 1351 \\ RES_TAC \\ ASM_SIMP_TAC std_ss []); 1352 1353val spilt_gc_thm = prove( 1354 ``(rel_gc (e,e+e,0,e,roots,m) = (T,b2,i2,e2,x1,x2,roots2,m2)) ==> 1355 (split_gc (ADDR_MAP (\a. a - e) roots,memF m e,memT m e 0,e) = (T,i2,roots2,m2,e))``, 1356 SIMP_TAC std_ss [rel_gc_def,LET_DEF] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 1357 \\ `?c1 xs1 j1 m1. rel_move_list (roots,0,m,0,e,e,e + e) = (c1,xs1,j1,m1)` by METIS_TAC [PAIR] 1358 \\ `?c2 i2 m2. rel_gc_loop (0,j1,m1,0,e,e,e + e) = (c2,i2,m2)` by METIS_TAC [PAIR] 1359 \\ ASM_SIMP_TAC std_ss [split_gc_def] \\ REPEAT STRIP_TAC 1360 \\ FULL_SIMP_TAC std_ss [] 1361 \\ IMP_RES_TAC (RW [LESS_EQ_REFL] (Q.INST [`i`|->`0`] (Q.SPECL [`xs`,`0`] spilt_move_list_thm))) 1362 \\ ASM_SIMP_TAC std_ss [LET_DEF] 1363 \\ IMP_RES_TAC (RW [DECIDE ``0 <= n:num``] (Q.SPEC `0` spilt_gc_loop_thm)) 1364 \\ ASM_SIMP_TAC std_ss [] 1365 \\ SIMP_TAC std_ss [memT_def,CUT_def] 1366 \\ SIMP_TAC std_ss [FUN_EQ_THM] \\ REPEAT STRIP_TAC 1367 \\ Cases_on `e <= k` \\ ASM_SIMP_TAC std_ss [RANGE_def,BLOCK_APPLY_def] 1368 \\ SRW_TAC [] [] \\ `F` by DECIDE_TAC); 1369 1370val split_lemma = prove( 1371 ``ok_full_heap (h,roots) (e,i,e+e,0,e,m) ==> 1372 ?h2 m2 i2 roots2. 1373 (split_gc (ADDR_MAP (\a. a - e) roots,memF m e,memT m e 0,e) = (T,i2,roots2,m2,e)) /\ 1374 ok_full_heap (h2,roots2) (0,i2,e,e,e + e,m2) /\ gc_exec (h,roots) (h2,roots2) /\ 1375 full_heap 0 i2 m2``, 1376 REPEAT STRIP_TAC 1377 \\ `?i2 m2 roots2 c. (rel_gc (e,e + e,0,e,roots,m) = (c,0,i2,e,e,e + e,roots2,m2))` by 1378 (SIMP_TAC std_ss [rel_gc_def,LET_DEF] 1379 \\ CONV_TAC (DEPTH_CONV (helperLib.FORCE_PBETA_CONV)) 1380 \\ SIMP_TAC std_ss []) 1381 \\ IMP_RES_TAC gc_thm \\ FULL_SIMP_TAC std_ss [] 1382 \\ IMP_RES_TAC spilt_gc_thm \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC []); 1383 1384val memI_def = Define ` 1385 memI m e = (\a. if a < e then H_EMP else BLOCK_APPLY (\a. a + e) (m (a - e)))`; 1386 1387val heapI_def = Define ` 1388 heapI h e = FUN_FMAP (\a. getBLOCK (BLOCK_APPLY (\a. a + e) (H_BLOCK (h ' (a - e))))) 1389 (\a. if a < e then F else (a - e:num) IN FDOM h)`; 1390 1391val ADDR_MAP_ID = prove( 1392 ``!xs g f. (g o f = I) ==> (ADDR_MAP g (ADDR_MAP f xs) = xs)``, 1393 Induct \\ SIMP_TAC std_ss [ADDR_MAP_def] \\ Cases 1394 \\ ASM_SIMP_TAC std_ss [ADDR_MAP_def,FUN_EQ_THM]); 1395 1396val BLOCK_APPLY_ID = prove( 1397 ``!h g. (h o g = I) ==> !x. BLOCK_APPLY h (BLOCK_APPLY g x) = x``, 1398 REPEAT STRIP_TAC \\ Cases_on `x` 1399 \\ FULL_SIMP_TAC std_ss [BLOCK_APPLY_def,FUN_EQ_THM] 1400 \\ Q.SPEC_TAC (`p`,`p`) \\ ASM_SIMP_TAC std_ss [FORALL_PROD,BLOCK_APPLY_def] 1401 \\ IMP_RES_TAC (SIMP_RULE std_ss [FUN_EQ_THM] ADDR_MAP_ID) 1402 \\ ASM_SIMP_TAC std_ss []); 1403 1404val part_heap_memI = prove( 1405 ``!k b e m t. 1406 part_heap b e m t ==> 1407 part_heap (b + k) (e + k) (memI m k) t``, 1408 STRIP_TAC \\ HO_MATCH_MP_TAC part_heap_ind \\ REPEAT STRIP_TAC 1409 \\ ONCE_REWRITE_TAC [part_heap_cases] \\ ASM_SIMP_TAC std_ss [] THEN1 1410 (DISJ2_TAC \\ DISJ1_TAC \\ FULL_SIMP_TAC std_ss [memI_def] 1411 \\ ASM_SIMP_TAC std_ss [DECIDE ``~(b+k<k:num)``] 1412 \\ STRIP_TAC THEN1 1413 (Cases_on `m b` \\ ASM_SIMP_TAC (srw_ss()) [isBLOCK_def,BLOCK_APPLY_def] 1414 \\ Cases_on `p` \\ Cases_on `r` 1415 \\ FULL_SIMP_TAC (srw_ss()) [isBLOCK_def,BLOCK_APPLY_def]) 1416 \\ FULL_SIMP_TAC std_ss [AC ADD_COMM ADD_ASSOC]) 1417 \\ FULL_SIMP_TAC (srw_ss()) [memI_def,BLOCK_APPLY_def,DECIDE ``~(b+k<k:num)``, 1418 isBLOCK_def,AC ADD_COMM ADD_ASSOC] \\ REPEAT (Q.EXISTS_TAC `t`) 1419 \\ FULL_SIMP_TAC (srw_ss()) [AC ADD_COMM ADD_ASSOC,BLOCK_APPLY_def] 1420 \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def] \\ REPEAT STRIP_TAC 1421 \\ Cases_on `a < k` \\ FULL_SIMP_TAC std_ss [IN_DEF] 1422 \\ `RANGE (b + 1,b + (n + 1)) (a - k)` by RANGE_TAC 1423 \\ FULL_SIMP_TAC (srw_ss()) [AC ADD_COMM ADD_ASSOC,BLOCK_APPLY_def]); 1424 1425val FINITE_heapI = prove( 1426 ``FINITE (\a. ~(a < e) /\ a - (e:num) IN FDOM h)``, 1427 SUBGOAL `(\a. ~(a < e) /\ a - (e:num) IN FDOM h) = 1428 (IMAGE (\a. a + e) (FDOM h)) DIFF {a | (a < e)}` 1429 \\ ASM_SIMP_TAC std_ss [] 1430 THEN1 METIS_TAC [FINITE_DIFF,IMAGE_FINITE,FDOM_FINITE] 1431 \\ ASM_SIMP_TAC std_ss [EXTENSION,IN_DIFF,GSPECIFICATION,IN_IMAGE] 1432 \\ ASM_SIMP_TAC std_ss [IN_DEF] \\ REPEAT STRIP_TAC 1433 \\ Cases_on `x < e` \\ ASM_SIMP_TAC std_ss [] 1434 \\ `!a. (x = a + e) = (a = x - e)` by DECIDE_TAC 1435 \\ ASM_SIMP_TAC std_ss []); 1436 1437val FDOM_heapI = prove( 1438 ``!h a e. a IN FDOM (heapI h e) = ~(a < e) /\ a - e IN FDOM h``, 1439 SIMP_TAC std_ss [heapI_def,FUN_FMAP_DEF,FINITE_heapI] 1440 \\ SIMP_TAC std_ss [IN_DEF]); 1441 1442val APPLY_heapI = prove( 1443 ``!a h e. 1444 a IN FDOM (heapI h e) ==> 1445 (heapI h e ' a = getBLOCK (BLOCK_APPLY (\a. a + e) (H_BLOCK (h ' (a - e)))))``, 1446 SIMP_TAC std_ss [heapI_def,FUN_FMAP_DEF,FINITE_heapI]); 1447 1448val IN_ADDR_SET_ADDR_MAP_LEMMA = prove( 1449 ``!xs x e. 1450 x IN ADDR_SET (ADDR_MAP (\a. a + e) xs) ==> 1451 ~(x < e) /\ x - e IN ADDR_SET xs``, 1452 Induct \\ SIMP_TAC std_ss [ADDR_SET_def,ADDR_MAP_def,MEM] \\ Cases 1453 \\ FULL_SIMP_TAC (srw_ss()) [ADDR_SET_def,ADDR_MAP_def,MEM] 1454 \\ REVERSE (NTAC 3 STRIP_TAC) THEN1 METIS_TAC [] 1455 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC); 1456 1457val ok_full_heap_IMP_heapI = store_thm("ok_full_heap_IMP_heapI", 1458 ``ok_full_heap (h,roots) (0,i,e,e,e+e,m) ==> 1459 ok_full_heap (heapI h e, 1460 ADDR_MAP (\a. a + e) roots) 1461 (e,e+i,e+e,0,e,memI m e) /\ 1462 (memF (memI m e) e = m) /\ 1463 (memT (memI m e) e 0 = \x.H_EMP)``, 1464 FULL_SIMP_TAC std_ss [ok_full_heap_def] \\ REPEAT STRIP_TAC 1465 THEN1 1466 (Cases_on `k < e` \\ ASM_SIMP_TAC std_ss [memI_def] 1467 \\ `~RANGE (0,i) (k - e)` by RANGE_TAC 1468 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [BLOCK_APPLY_def]) 1469 THEN1 1470 (Q.EXISTS_TAC `t` \\ ONCE_REWRITE_TAC [ADD_COMM] 1471 \\ MATCH_MP_TAC (RW [ADD_CLAUSES] (Q.SPECL [`e`,`0`,`i`] part_heap_memI)) 1472 \\ ASM_SIMP_TAC std_ss []) 1473 THEN1 1474 (FULL_SIMP_TAC std_ss [ref_heap_mem_def,memI_def,APPLY_heapI] 1475 \\ FULL_SIMP_TAC std_ss [FDOM_heapI] \\ REPEAT STRIP_TAC 1476 \\ Cases_on `a < e` \\ ASM_SIMP_TAC std_ss [] 1477 \\ Cases_on `a - e IN FDOM h` \\ ASM_SIMP_TAC std_ss [BLOCK_APPLY_def] 1478 \\ Cases_on `h ' (a - e)` \\ Cases_on `r` 1479 \\ FULL_SIMP_TAC std_ss [BLOCK_APPLY_def,getBLOCK_def]) 1480 THEN1 1481 (FULL_SIMP_TAC std_ss [ok_heap_def,memI_def,APPLY_heapI] 1482 \\ FULL_SIMP_TAC std_ss [POINTERS_def,SUBSET_DEF,IN_UNION,IN_UNIV] 1483 \\ REVERSE (REPEAT STRIP_TAC) 1484 THEN1 METIS_TAC [IN_ADDR_SET_ADDR_MAP_LEMMA,FDOM_heapI] 1485 \\ Q.PAT_X_ASSUM `b IN FDOM (heapI h e)` ASSUME_TAC 1486 \\ FULL_SIMP_TAC std_ss [APPLY_heapI] 1487 \\ Q.PAT_X_ASSUM `xxx = (zs,d)` MP_TAC 1488 \\ `?xs n2 d2. h ' (b - e) = (xs,n2,d2)` by METIS_TAC [PAIR] 1489 \\ FULL_SIMP_TAC std_ss [BLOCK_APPLY_def,getBLOCK_def] 1490 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ ASM_SIMP_TAC std_ss [] 1491 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 1492 \\ IMP_RES_TAC IN_ADDR_SET_ADDR_MAP_LEMMA 1493 \\ METIS_TAC [IN_ADDR_SET_ADDR_MAP_LEMMA,FDOM_heapI]) 1494 THEN1 1495 (SIMP_TAC std_ss [memF_def,FUN_EQ_THM] \\ REPEAT STRIP_TAC 1496 \\ Cases_on `x < e` \\ ASM_SIMP_TAC std_ss [] THEN1 1497 (`~(x + e < e)` by RANGE_TAC \\ ASM_SIMP_TAC std_ss [memI_def] 1498 \\ SUBGOAL `(\a. a - e) o (\a. a + e:num) = I` 1499 THEN1 METIS_TAC [BLOCK_APPLY_ID] 1500 \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM]) 1501 \\ `~RANGE (0,i) x` by RANGE_TAC \\ METIS_TAC []) 1502 THEN 1503 (SIMP_TAC std_ss [memT_def,FUN_EQ_THM] \\ REPEAT STRIP_TAC 1504 \\ Cases_on `e <= x` \\ ASM_SIMP_TAC std_ss [memI_def] 1505 \\ Cases_on `x < e` \\ ASM_SIMP_TAC std_ss [BLOCK_APPLY_def] 1506 \\ `(\a. a - e) o (\a. a + e:num) = I` by FULL_SIMP_TAC std_ss [FUN_EQ_THM] 1507 \\ ASM_SIMP_TAC std_ss [BLOCK_APPLY_ID] 1508 \\ `~RANGE (0,i) (x-e)` by RANGE_TAC \\ METIS_TAC [])); 1509 1510val split_gc_thm = store_thm("split_gc_thm", 1511 ``ok_full_heap (h,roots) (0,i,e,e,e+e,m) ==> 1512 ?h2 m2 i2 roots2. 1513 (split_gc (roots,m,(\x.H_EMP),e) = (T,i2,roots2,m2,e)) /\ 1514 ok_full_heap (h2,roots2) (0,i2,e,e,e + e,m2) /\ 1515 full_heap 0 i2 m2 /\ 1516 gc_exec (heapI h e,ADDR_MAP (\a. a + e) roots) (h2,roots2)``, 1517 REPEAT STRIP_TAC \\ IMP_RES_TAC ok_full_heap_IMP_heapI 1518 \\ IMP_RES_TAC split_lemma \\ REPEAT (POP_ASSUM MP_TAC) 1519 \\ ASM_SIMP_TAC std_ss [] 1520 \\ `(\a. a - e) o (\a. a + e:num) = I` by FULL_SIMP_TAC std_ss [FUN_EQ_THM] 1521 \\ ASM_SIMP_TAC std_ss [ADDR_MAP_ID] \\ METIS_TAC []); 1522 1523 1524(* representation of s-expressions in abstract heap, given symbol-table sym *) 1525 1526open lisp_sexpTheory; 1527 1528val LIST_FIND_def = Define ` 1529 (LIST_FIND n x [] = NONE) /\ 1530 (LIST_FIND n x (y::ys) = if x = y then SOME n else LIST_FIND (n+1) x ys)`; 1531 1532val LIST_FIND_LESS_EQ = store_thm("LIST_FIND_LESS_EQ", 1533 ``!xs x k d. (LIST_FIND k x xs = SOME d) ==> k <= d``, 1534 Induct \\ SIMP_TAC std_ss [LIST_FIND_def,APPEND] \\ REPEAT STRIP_TAC 1535 \\ Cases_on `x = h` \\ FULL_SIMP_TAC std_ss [] \\ RES_TAC \\ DECIDE_TAC); 1536 1537val lisp_x_def = Define ` 1538 (lisp_x (m,sym) (a,Val k) = 1539 (a = H_DATA (INL ((n2w k):word30))) /\ k < 2**30) /\ 1540 (lisp_x (m,sym) (a,Sym s) = 1541 ?k. (LIST_FIND 0 s sym = SOME k) /\ 1542 (a = H_DATA (INR ((n2w k):29 word))) /\ k < 2**29) /\ 1543 (lisp_x (m,sym) (a,Dot x y) = 1544 ?ax ay k. 1545 (a = H_ADDR k) /\ (m k = H_BLOCK ([ax;ay],0,())) /\ 1546 lisp_x (m,sym) (ax,x) /\ lisp_x (m,sym) (ay,y))` 1547 1548val ADDR_MAP_TWICE = prove( 1549 ``!xs. ADDR_MAP f (ADDR_MAP g xs) = ADDR_MAP (f o g) xs``, 1550 Induct \\ SIMP_TAC std_ss [ADDR_MAP_def] \\ Cases 1551 \\ ASM_SIMP_TAC std_ss [ADDR_MAP_def]); 1552 1553val EL_ADDR_MAP = prove( 1554 ``!xs k. k < LENGTH xs ==> (EL k (ADDR_MAP f xs) = ADDR_APPLY f (EL k xs))``, 1555 Induct \\ SIMP_TAC std_ss [LENGTH] \\ Cases \\ Cases 1556 \\ ASM_SIMP_TAC std_ss [LENGTH,ADDR_APPLY_def,ADDR_MAP_def,EL,HD,TL]); 1557 1558val ADDR_APPLY_EQ_DATA = prove( 1559 ``!x y f. (ADDR_APPLY f x = H_DATA y) = (x = H_DATA y)``, 1560 Cases \\ SRW_TAC [] [ADDR_APPLY_def]); 1561 1562val PAIR_TRANSLATE_FLIP = prove( 1563 ``!x y f. (f o f = I) ==> ((PAIR_TRANSLATE f x = y) = (x = PAIR_TRANSLATE f y))``, 1564 SIMP_TAC std_ss [FORALL_PROD,PAIR_TRANSLATE_def] \\ METIS_TAC [ADDR_MAP_ID]); 1565 1566val ADDR_MAP_THM = prove( 1567 ``!xs f. ADDR_MAP f xs = MAP (ADDR_APPLY f) xs``, 1568 Induct \\ SIMP_TAC std_ss [ADDR_MAP_def,ADDR_APPLY_def,MAP] \\ Cases 1569 \\ ASM_SIMP_TAC std_ss [ADDR_MAP_def,ADDR_APPLY_def,MAP]); 1570 1571val lisp_x_gc_thm = store_thm("lisp_x_gc_thm", 1572 ``ok_full_heap (h,roots) (0,i,e,e,e+e,m) /\ k < LENGTH roots /\ 1573 (split_gc (roots,m,(\x.H_EMP),e) = (c2,i2,roots2,m2,e)) ==> 1574 lisp_x (m,sym) (EL k roots,x) ==> 1575 lisp_x (m2,sym) (EL k roots2,x)``, 1576 STRIP_TAC 1577 \\ IMP_RES_TAC split_gc_thm 1578 \\ FULL_SIMP_TAC std_ss [] 1579 \\ REPEAT (POP_ASSUM MP_TAC) 1580 \\ SIMP_TAC std_ss [] 1581 \\ REPEAT STRIP_TAC 1582 \\ POP_ASSUM MP_TAC 1583 \\ POP_ASSUM MP_TAC 1584 \\ Q.PAT_X_ASSUM `k < LENGTH roots` MP_TAC 1585 \\ Q.PAT_X_ASSUM `ok_full_heap (h2,roots2) (0,i2,e,e,e + e,m2)` MP_TAC 1586 \\ IMP_RES_TAC ok_full_heap_IMP_heapI 1587 \\ Q.PAT_X_ASSUM `ok_full_heap (heapI h e,yy) xxx` MP_TAC 1588 \\ Q.SPEC_TAC (`heapI h e`,`h1`) \\ STRIP_TAC 1589 \\ REPEAT (POP_ASSUM (K ALL_TAC)) \\ REPEAT STRIP_TAC 1590 \\ POP_ASSUM MP_TAC 1591 \\ FULL_SIMP_TAC std_ss [gc_exec_def,gc_copy_def,gc_filter_def] 1592 \\ FULL_SIMP_TAC std_ss [ADDR_MAP_TWICE,EL_ADDR_MAP] 1593 \\ `?r. EL k roots = r` by METIS_TAC [] 1594 \\ ASM_SIMP_TAC std_ss [] 1595 \\ `ADDR_SET (ADDR_MAP (\a. a + e) [r]) SUBSET gc_reachable (h1,ADDR_MAP (\a. a + e) roots)` by 1596 (REVERSE (Cases_on `r`) 1597 \\ SIMP_TAC std_ss [ADDR_MAP_def,ADDR_SET_THM,EMPTY_SUBSET,INSERT_SUBSET] 1598 \\ SIMP_TAC std_ss [IN_DEF] \\ ONCE_REWRITE_TAC [gc_reachable_cases] \\ DISJ1_TAC 1599 \\ SIMP_TAC std_ss [ADDR_SET_def] 1600 \\ `MEM (H_ADDR n) roots` by METIS_TAC [rich_listTheory.EL_IS_EL] 1601 \\ POP_ASSUM MP_TAC \\ REPEAT (POP_ASSUM (K ALL_TAC)) 1602 \\ Induct_on `roots` \\ SIMP_TAC std_ss [MEM] \\ Cases 1603 \\ SIMP_TAC (srw_ss()) [ADDR_MAP_def] \\ METIS_TAC []) 1604 \\ POP_ASSUM MP_TAC \\ POP_ASSUM (K ALL_TAC) 1605 \\ Q.SPEC_TAC (`r`,`r`) \\ Q.SPEC_TAC (`x`,`x`) 1606 \\ REVERSE Induct 1607 THEN1 (SIMP_TAC std_ss [lisp_x_def,ADDR_APPLY_EQ_DATA]) 1608 THEN1 (SIMP_TAC std_ss [lisp_x_def,ADDR_APPLY_EQ_DATA]) 1609 \\ SIMP_TAC std_ss [lisp_x_def] \\ REPEAT STRIP_TAC 1610 \\ ASM_SIMP_TAC (srw_ss()) [ADDR_APPLY_def] 1611 \\ `(k' + e) IN FDOM h1 /\ (h1 ' (k' + e) = (ADDR_MAP (\a. a + e) [ax; ay],0,()))` by 1612 (Q.PAT_X_ASSUM `ok_full_heap (h1,ADDR_MAP (\a. a + e) roots) xxx` MP_TAC 1613 \\ SIMP_TAC std_ss [ok_full_heap_def] \\ REPEAT STRIP_TAC 1614 \\ FULL_SIMP_TAC std_ss [ref_heap_mem_def] 1615 \\ Q.PAT_X_ASSUM `!a.bbb` (MP_TAC o Q.SPEC `k' + e`) 1616 \\ ASM_SIMP_TAC std_ss [memI_def,BLOCK_APPLY_def,DECIDE ``~(k+e<e:num)``] 1617 \\ Cases_on `k' + e IN FDOM h1` \\ ASM_SIMP_TAC (srw_ss()) []) 1618 \\ FULL_SIMP_TAC std_ss [ADDR_MAP_def,INSERT_SUBSET,EMPTY_SUBSET,ADDR_SET_THM] 1619 \\ FULL_SIMP_TAC std_ss [FDOM_DRESTRICT,IN_INTER] 1620 \\ `h1 ' (k' + e) = PAIR_TRANSLATE f (h2 ' (f (k' + e)))` by 1621 (RES_TAC \\ POP_ASSUM MP_TAC 1622 \\ SIMP_TAC std_ss [DRESTRICT_DEF,FDOM_DRESTRICT,IN_INTER] \\ METIS_TAC []) 1623 \\ FULL_SIMP_TAC std_ss [] 1624 \\ Q.PAT_X_ASSUM `f o f = I` ASSUME_TAC 1625 \\ FULL_SIMP_TAC std_ss [PAIR_TRANSLATE_FLIP] 1626 \\ FULL_SIMP_TAC std_ss [PAIR_TRANSLATE_def,ADDR_MAP_TWICE] 1627 \\ `(f (k' + e)) IN FDOM h2` by 1628 (FULL_SIMP_TAC std_ss [EXTENSION,SET_TRANSLATE_def,IN_INTER] \\ RES_TAC) 1629 \\ `m2 (f (k' + e)) = H_BLOCK (h2 ' (f (k' + e)))` by 1630 (FULL_SIMP_TAC std_ss [ok_full_heap_def,ref_heap_mem_def]) 1631 \\ POP_ASSUM MP_TAC 1632 \\ ASM_SIMP_TAC std_ss [ADDR_MAP_THM,MAP] \\ STRIP_TAC 1633 \\ SIMP_TAC (srw_ss()) [] \\ REPEAT STRIP_TAC THEN1 1634 (Q.PAT_X_ASSUM `!x.bbb` (K ALL_TAC) 1635 \\ Q.PAT_X_ASSUM `!x.bbb` (MATCH_MP_TAC o RW [AND_IMP_INTRO]) 1636 \\ ASM_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def] 1637 \\ Cases_on `ax` \\ FULL_SIMP_TAC (srw_ss()) [MEM,ADDR_MAP_def] 1638 \\ SIMP_TAC std_ss [IN_DEF] 1639 \\ ONCE_REWRITE_TAC [gc_reachable_cases] \\ DISJ2_TAC 1640 \\ SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `k' + e` 1641 \\ ASM_SIMP_TAC std_ss [PAIR_TRANSLATE_def,ADDR_SET_def,MEM,ADDR_MAP_def] 1642 \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM,IN_DEF]) 1643 THEN1 1644 (Q.PAT_X_ASSUM `!x.bbb` (MATCH_MP_TAC o RW [AND_IMP_INTRO]) 1645 \\ ASM_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def] 1646 \\ Cases_on `ay` \\ FULL_SIMP_TAC (srw_ss()) [MEM,ADDR_MAP_def] 1647 \\ SIMP_TAC std_ss [IN_DEF] 1648 \\ ONCE_REWRITE_TAC [gc_reachable_cases] \\ DISJ2_TAC 1649 \\ SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `k' + e` 1650 \\ ASM_SIMP_TAC std_ss [PAIR_TRANSLATE_def,ADDR_SET_def,MEM,ADDR_MAP_def] 1651 \\ SIMP_TAC std_ss [ADDR_MAP_THM,MAP,MEM,ADDR_APPLY_def] 1652 \\ FULL_SIMP_TAC std_ss [ADDR_MAP_THM,FUN_EQ_THM,IN_DEF])); 1653 1654 1655val _ = export_theory(); 1656