1 2open HolKernel boolLib bossLib Parse; 3open pred_setTheory arithmeticTheory pairTheory listTheory combinTheory finite_mapTheory; 4 5 6val _ = new_theory "cheney_gc"; 7 8infix \\ 9val op \\ = op THEN; 10val RW = REWRITE_RULE; 11val RW1 = ONCE_REWRITE_RULE; 12 13 14(* -- helper -- *) 15 16fun FORCE_PBETA_CONV tm = let 17 val (tm1,tm2) = dest_comb tm 18 val vs = fst (pairSyntax.dest_pabs tm1) 19 fun expand_pair_conv tm = ISPEC tm (GSYM pairTheory.PAIR) 20 fun get_conv vs = let 21 val (x,y) = pairSyntax.dest_pair vs 22 in expand_pair_conv THENC (RAND_CONV (get_conv y)) end 23 handle HOL_ERR e => ALL_CONV 24 in (RAND_CONV (get_conv vs) THENC PairRules.PBETA_CONV) tm end; 25 26(* -- abstraction -- *) 27 28val SUBSET0_DEF = new_infixr_definition 29 ("SUBSET0_DEF", ���SUBSET0 s t = s SUBSET (0 INSERT t)���,451); 30 31val SUBSET0_TRANS = store_thm("SUBSET0_TRANS", 32 ``!x y z. x SUBSET0 y /\ y SUBSET0 z ==> x SUBSET0 z``, 33 REWRITE_TAC [SUBSET0_DEF,SUBSET_DEF,IN_INSERT] \\ METIS_TAC []); 34 35val _ = Hol_datatype ` 36 heap_type = EMP | REF of num | DATA of num # num # 'a`; 37 38val isREF_def = Define `isREF x = ?i. x = REF i`; 39val getREF_def = Define `getREF (REF x) = x`; 40val getDATA_def = Define `getDATA (DATA y) = y`; 41 42val heap_type_distinct = fetch "-" "heap_type_distinct" 43val heap_type_11 = fetch "-" "heap_type_11" 44 45val RANGE_def = Define `RANGE(i:num,j) k = i <= k /\ k < j`; 46val IRANGE_def = Define `IRANGE(i:num,j) k = ~(i <= k /\ k < j)`; 47 48val CUT_def = Define `CUT (i,j) m = \k. if RANGE (i,j) k then m k else EMP`; 49val ICUT_def = Define `ICUT (i,j) m = \k. if IRANGE (i,j) k then m k else EMP`; 50 51val D0 = Define `D0 m k = ?x y z. m (k:num) = DATA(x,y,z)`; 52val D1 = Define `D1 m x = ?k y z. (m (k:num) = DATA(x,y,z)) \/ (m k = DATA(y,x,z))`; 53val R0 = Define `R0 m k = ?a. m (k:num) = REF a`; 54val R1 = Define `R1 m a = ?k. m (k:num) = REF a`; 55val DR0 = Define `DR0 m k = D0 m k \/ R0 m k` 56val DR1 = Define `DR1 m k = D1 m k \/ R1 m k` 57 58val ADDR_def = Define ` 59 (ADDR k n EMP = (n = k)) /\ 60 (ADDR k n (REF i) = (n = i)) /\ 61 (ADDR k n (DATA x) = (n = k))`; 62 63val abs_def = Define ` 64 abs m (a,n,n',d) = 65 ?k k'. (m a = DATA(k,k',d)) /\ ADDR k n (m k) /\ ADDR k' n' (m k')`; 66 67val basic_abs = Define ` 68 basic_abs m (a,n,n',d) = (m a = DATA(n,n',d))`; 69 70val apply_def = Define `apply h s (a,n,n',d) = (h a,h n,h n',d) IN s`; 71 72val PATH_def = Define ` 73 (PATH (x,[]) s = T) /\ 74 (PATH (x,y::ys) s = PATH (y,ys) s /\ ?z d. (x,y,z,d) IN s \/ (x,z,y,d) IN s)`; 75 76val reachable_def = Define ` 77 reachable r s i = (r = i) \/ ?p. PATH (r,p++[i]) s`; 78 79val UPDATE_thm = prove( 80 ``!a b. a =+ b = (\f k. (if k = a then b else f k))``, 81 SIMP_TAC std_ss [UPDATE_def,FUN_EQ_THM] \\ METIS_TAC []); 82 83val roots_inv_def = Define ` 84 roots_inv (b,j,m,xx) = 85 ?v. (v o v = I) /\ (xx = apply v (abs m)) /\ 86 (!k. ~isREF(m k) /\ ~RANGE(b,j)k ==> (v k = k)) /\ 87 (!k i. (m k = REF i) ==> (v k = i))`; 88 89val cheney_inv_def = Define ` 90 cheney_inv(b,b',i,j,j',e,f,m,x,xx,r) = 91 (0 < b /\ b <= b' /\ b' <= j /\ b <= i /\ i <= j /\ j <= e /\ e <= f) /\ 92 (!k. j <= k /\ k < e \/ f < k ==> (m k = EMP)) /\ (* all EMP between j and e *) 93 (D0(CUT(b,j)m) = RANGE(b,j)) /\ (* all DATA between b and j *) 94 (D1(CUT(b,i)m) SUBSET0 RANGE(b,j)) /\ (* b-i links only to b-j and nil *) 95 (RANGE(i,j') SUBSET (r UNION D1(CUT(b,i)m))) /\ (* every i-j is linked to by some b-i *) 96 (D1(CUT(i,j)m) SUBSET0 DR0(ICUT(b,e)m)) /\ (* i-j links only outside of b-e *) 97 (D1(ICUT(b,e)m) SUBSET0 DR0(ICUT(b,e)m)) /\ (* outside of b-e links only to outside b-e *) 98 (R1(m) = RANGE(b,j)) /\ (* all REFs refer to b-j elements *) 99 (!i j k. (m i = REF k) /\ (m j = REF k) ==> (i = j)) /\ (* REFs are injective *) 100 (CARD(D0(ICUT(b,e)m)) <= e-j) /\ (* num of elements outside b-e fit into e-j *) 101 FINITE (D0(ICUT(b,e)m)) /\ (* the set is finite *) 102 (m 0 = EMP) /\ (* 0 points at no data *) 103 RANGE(b,i) SUBSET (* all of b-i is reachable from r *) 104 (\x. ?t. t IN r /\ x IN reachable t (basic_abs(CUT(b,i)m))) /\ 105 (!k i. (x k = REF i) ==> (m k = REF i)) /\ (* refernces are reserved *) 106 roots_inv (b,j,m,abs xx) (* memory is permuted *)`; 107 108val ok_state_def = Define ` 109 ok_state (i,e,r,l,u,m) = 110 let a = (if u then 1 + l else 1) in 111 let s = RANGE(a,i) in 112 a <= i /\ i <= e /\ (e = a + l) /\ 113 (!k. MEM k r /\ ~(k = 0) ==> k IN s) /\ 114 (!k. ~(k IN s) ==> (m k = EMP)) /\ 115 (!k. k IN s ==> ?x y d. (m k = DATA(x,y,d)) /\ {x;y} SUBSET0 s)`; 116 117val move_def = Define ` 118 move(x,j,m) = 119 if x = 0 then (x,j,m) else 120 if isREF (m x) then (getREF (m x),j,m) else 121 let m = (j =+ m x) m in 122 let m = (x =+ REF j) m in 123 (j,j+1,m)`; 124 125val cheney_step_def = Define ` 126 cheney_step (i,j,e,m) = 127 let (x,y,d) = getDATA (m i) in 128 let (x,j,m) = move (x,j,m) in 129 let (y,j,m) = move (y,j,m) in 130 let m = (i =+ DATA (x,y,d)) m in 131 (i+1,j,e,m)`; 132 133val cheney_def = tDefine "cheney" ` 134 cheney(i,j,e,m) = 135 if (i = j) \/ e < i then (i,m) else 136 cheney(cheney_step(i,j,e,m))` 137 (WF_REL_TAC `measure (\(i,j,e,m). (e + 1) - i)` 138 \\ REWRITE_TAC [cheney_step_def,LET_DEF] 139 \\ CONV_TAC (DEPTH_CONV FORCE_PBETA_CONV) 140 \\ REWRITE_TAC [FST,SND] \\ DECIDE_TAC); 141 142val cheney_ind = fetch "-" "cheney_ind"; 143 144val m_DATA = store_thm("m_DATA", 145 ``cheney_inv(b,b',i,j,j',e,f,m,x,xx,r) /\ ~(i = j) ==> ?ax ay ad. m i = DATA (ax,ay,ad)``, 146 SIMP_TAC std_ss [cheney_inv_def,FUN_EQ_THM,D0,IN_DEF,RANGE_def,CUT_def] 147 \\ REPEAT STRIP_TAC \\ `b <= i /\ i < j` by DECIDE_TAC \\ METIS_TAC []); 148 149val IN_EQ_SUBSET = 150 GEN_ALL (GSYM (REWRITE_CONV [INSERT_SUBSET,EMPTY_SUBSET] ``{i:'a} SUBSET x``)); 151 152val RANGE_IRANGE = prove( 153 ``!b e x y. RANGE (b,e) x /\ IRANGE (b,e) y ==> ~(x = y)``, 154 REWRITE_TAC [RANGE_def,IRANGE_def] \\ DECIDE_TAC); 155 156val RANGE_expand = prove( 157 ``!i j k x. RANGE (i,j) x /\ j <= k ==> RANGE (i,k) x``, 158 REWRITE_TAC [RANGE_def,IRANGE_def] \\ DECIDE_TAC); 159 160val RANGE_expand_left = prove( 161 ``!i j k x. RANGE (i,j) x /\ k <= i ==> RANGE (k,j) x``, 162 REWRITE_TAC [RANGE_def,IRANGE_def] \\ DECIDE_TAC); 163 164val CUT_update = prove( 165 ``~RANGE (i,j) k ==> (CUT (i,j) ((k =+ x) m) = CUT (i,j) m)``, 166 SIMP_TAC std_ss [CUT_def,UPDATE_def,FUN_EQ_THM] \\ METIS_TAC []); 167 168val ICUT_update = prove( 169 ``~IRANGE (i,j) k ==> (ICUT (i,j) ((k =+ x) m) = ICUT (i,j) m)``, 170 SIMP_TAC std_ss [ICUT_def,UPDATE_def,FUN_EQ_THM] \\ METIS_TAC []); 171 172val update_update = prove( 173 ``!m i x y. (i =+ y) ((i =+ x) m) = (i=+ y) m``, 174 SIMP_TAC std_ss [FUN_EQ_THM,UPDATE_def]); 175 176val expand_CUT = prove( 177 ``RANGE (a,b) SUBSET RANGE (c,d) /\ (CUT(c,d)m=CUT(c,d)n) ==> (CUT(a,b)m=CUT(a,b)n)``, 178 SIMP_TAC std_ss [SUBSET_DEF,IN_DEF,FUN_EQ_THM,RANGE_def,CUT_def] \\ METIS_TAC []); 179 180val D1_SUBSET0 = prove( 181 ``D1 (CUT(j,j+1)m) SUBSET0 s /\ D1 (CUT(i,j)m) SUBSET0 s ==> 182 D1 (CUT(i,j+1)m) SUBSET0 s``, 183 REWRITE_TAC [SUBSET0_DEF,SUBSET_DEF,IN_INSERT] 184 \\ SIMP_TAC std_ss [IN_DEF,D1,CUT_def,RANGE_def,DECIDE ``k<n+1=k<=n``] 185 \\ METIS_TAC [DECIDE ``n <= k \/ k < n:num``,fetch "-" "heap_type_distinct"]); 186 187val swap_def = Define ` 188 swap i j = \k. if k = i then j else if k = j then i else k`; 189 190val swap_swap = store_thm("swap_swap", 191 ``!i:'a j. swap i j o swap i j = I``, 192 SIMP_TAC std_ss [swap_def,FUN_EQ_THM] 193 \\ REPEAT STRIP_TAC \\ Cases_on `x = i` \\ Cases_on `x = j` \\ Cases_on `i = j` 194 \\ ASM_SIMP_TAC std_ss []); 195 196val swap_swap2 = prove( 197 ``!i:'a j x. swap i j (swap i j x) = x``, 198 SIMP_TAC std_ss [swap_def] 199 \\ REPEAT STRIP_TAC \\ Cases_on `x = i` \\ Cases_on `x = j` \\ Cases_on `i = j` 200 \\ ASM_SIMP_TAC std_ss []); 201 202val swap_id = prove( 203 ``!i j k. ~(i = k) /\ ~(j = k) ==> (swap i j k = k)``, 204 SIMP_TAC std_ss [swap_def]); 205 206val apply_apply = store_thm("apply_apply", 207 ``!s f g. apply f (apply g s) = apply (g o f) s``, 208 SIMP_TAC std_ss [FUN_EQ_THM] \\ REPEAT STRIP_TAC 209 \\ Cases_on `x` \\ Cases_on `r` \\ Cases_on `r'` 210 \\ SIMP_TAC std_ss [apply_def,IN_DEF]); 211 212val apply_I = store_thm("apply_I", 213 ``!s. apply I s = s``, 214 REWRITE_TAC [FUN_EQ_THM] \\ REPEAT STRIP_TAC 215 \\ Cases_on `x` \\ Cases_on `r` \\ Cases_on `r'` \\ SIMP_TAC std_ss [apply_def,IN_DEF]); 216 217val RANGE_IMP_NOT_DR0 = prove( 218 ``!i j x m. RANGE (i,j) x ==> ~DR0 (ICUT(i,j)m) x``, 219 SIMP_TAC std_ss [DR0,D0,R0,ICUT_def,IRANGE_def,RANGE_def,heap_type_distinct]); 220 221val D0_IMP = prove( 222 ``D0 (CUT (b,j) m) i ==> ?h g dd. RANGE(b,j)i /\ (m i = DATA(h,g,dd))``, 223 SIMP_TAC std_ss [D0,CUT_def] \\ METIS_TAC [heap_type_distinct]); 224 225val D1_IMP = prove( 226 ``D1 (CUT (b,i) m) j ==> 227 ?h g dd. RANGE(b,i)h /\ (~(m h = DATA(j,g,dd)) ==> (m h = DATA(g,j,dd)))``, 228 SIMP_TAC std_ss [D1,CUT_def] \\ REPEAT STRIP_TAC 229 \\ Q.EXISTS_TAC `k` \\ Cases_on `RANGE (b,i) k` 230 \\ FULL_SIMP_TAC std_ss [heap_type_distinct,heap_type_11] \\ METIS_TAC []); 231 232val lemma2 = prove( 233 ``k IN D1 m /\ ~(j = x) /\ IRANGE(b,e)x /\ ~(j = e) /\ 234 cheney_inv (b,b',i,j,j',e,f,m,w,xx,r) /\ (m x = DATA (n',n'',d')) /\ (m j = EMP) ==> 235 (ADDR k (swap j x t) (((x =+ REF j) ((j =+ (DATA (n',n'',d'))) m)) k) = 236 ADDR k t (m k))``, 237 SIMP_TAC std_ss [UPDATE_def,swap_def] \\ Cases_on `k = j` \\ ASM_REWRITE_TAC [] THENL [ 238 REPEAT STRIP_TAC 239 \\ `{j} SUBSET D1 m` by METIS_TAC [IN_EQ_SUBSET] \\ FULL_SIMP_TAC std_ss [cheney_inv_def] 240 \\ `{j} SUBSET (D1 (ICUT (b,e) m)) \/ {j} SUBSET (D1 (CUT (b,i) m)) \/ 241 {j} SUBSET (D1 (CUT (i,j) m)) \/ {j} SUBSET (D1 (CUT (j,e) m))` by 242 (FULL_SIMP_TAC std_ss [GSYM IN_EQ_SUBSET,IN_DEF,D1,GSYM RANGE_def] 243 \\ SIMP_TAC std_ss [CUT_def,ICUT_def] 244 \\ `IRANGE(b,e)k' \/ RANGE(b,i)k' \/ RANGE(i,j)k' \/ RANGE(j,e)k'` by 245 (REWRITE_TAC [RANGE_def,IRANGE_def] \\ DECIDE_TAC) 246 \\ METIS_TAC [heap_type_distinct]) 247 THENL [ 248 FULL_SIMP_TAC bool_ss [SUBSET0_DEF] 249 \\ `{j} SUBSET 0 INSERT DR0 (ICUT (b,e) m)` by METIS_TAC [SUBSET_TRANS] 250 \\ FULL_SIMP_TAC bool_ss [GSYM IN_EQ_SUBSET,IN_INSERT,IN_DEF] THEN1 `F` by DECIDE_TAC 251 \\ `RANGE (b,e) j` by (REWRITE_TAC [RANGE_def] \\ DECIDE_TAC) 252 \\ IMP_RES_TAC RANGE_IMP_NOT_DR0, 253 FULL_SIMP_TAC bool_ss [SUBSET0_DEF] 254 \\ `{j} SUBSET 0 INSERT RANGE (b,j)` by METIS_TAC [SUBSET_TRANS] 255 \\ FULL_SIMP_TAC bool_ss [GSYM IN_EQ_SUBSET,IN_INSERT,IN_DEF,RANGE_def] 256 \\ `F` by DECIDE_TAC, 257 FULL_SIMP_TAC bool_ss [SUBSET0_DEF] 258 \\ `{j} SUBSET 0 INSERT DR0 (ICUT (b,e) m)` by METIS_TAC [SUBSET_TRANS] 259 \\ FULL_SIMP_TAC bool_ss [GSYM IN_EQ_SUBSET,IN_INSERT,IN_DEF] THEN1 `F` by DECIDE_TAC 260 \\ `RANGE (b,e) j` by (REWRITE_TAC [RANGE_def] \\ DECIDE_TAC) 261 \\ IMP_RES_TAC RANGE_IMP_NOT_DR0, 262 FULL_SIMP_TAC bool_ss [GSYM IN_EQ_SUBSET,IN_INSERT,IN_DEF,D1,CUT_def,RANGE_def] 263 \\ `F` by METIS_TAC [heap_type_distinct]], 264 Cases_on `k = x` \\ ASM_SIMP_TAC std_ss [ADDR_def] THEN1 METIS_TAC [] 265 \\ Cases_on `m k` \\ ASM_REWRITE_TAC [ADDR_def] THENL [ 266 Cases_on `t = j` \\ Cases_on `t = x` \\ FULL_SIMP_TAC bool_ss [], 267 REPEAT STRIP_TAC 268 \\ `~(n = x)` by 269 (CCONTR_TAC \\ FULL_SIMP_TAC bool_ss [] 270 \\ `{x} SUBSET R1 m` by (SIMP_TAC std_ss [GSYM IN_EQ_SUBSET,IN_DEF] \\ METIS_TAC [R1]) 271 \\ `{x} SUBSET RANGE (b,j)` by METIS_TAC [cheney_inv_def,SUBSET_TRANS] 272 \\ FULL_SIMP_TAC bool_ss [GSYM IN_EQ_SUBSET,IN_DEF,RANGE_def,IRANGE_def,cheney_inv_def] 273 \\ DECIDE_TAC) 274 \\ `~(n = j)` by 275 (CCONTR_TAC \\ FULL_SIMP_TAC bool_ss [] 276 \\ `{j} SUBSET R1 m` by (SIMP_TAC std_ss [GSYM IN_EQ_SUBSET,IN_DEF] \\ METIS_TAC [R1]) 277 \\ `{j} SUBSET RANGE (b,j)` by METIS_TAC [cheney_inv_def,SUBSET_TRANS] 278 \\ FULL_SIMP_TAC bool_ss [GSYM IN_EQ_SUBSET,IN_DEF,RANGE_def,IRANGE_def,cheney_inv_def] 279 \\ DECIDE_TAC) 280 \\ METIS_TAC [], 281 Cases_on `t = j` \\ Cases_on `t = x` \\ FULL_SIMP_TAC bool_ss []]]); 282 283val lemma = prove( 284 ``(m x = DATA (n',n'',d')) /\ (m j = EMP) ==> 285 (((x =+ REF j) ((j =+ DATA (n',n'',d')) m) (swap j x a) = DATA (k,k',v)) = 286 (m a = DATA (k,k',v)))``, 287 SIMP_TAC std_ss [UPDATE_def,swap_def] 288 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 289 \\ Cases_on `a = j` \\ FULL_SIMP_TAC bool_ss [swap_def,heap_type_distinct] 290 \\ Cases_on `a = x` \\ FULL_SIMP_TAC bool_ss [swap_def,heap_type_11,PAIR_EQ]); 291 292val move_lemma_lemma = prove( 293 ``!d' b b' i j j' e m w r x n' n''. 294 (m x = DATA (n',n'',d')) /\ (m j = EMP) /\ ~(j = e) /\ 295 cheney_inv (b,b',i,j,j',e,f,m,w,xx,r) /\ IRANGE (b,e) x /\ ~(x = 0) ==> 296 (apply (swap j x) (abs((x =+ REF j) ((j =+ m x) m))) = abs m)``, 297 REWRITE_TAC [FUN_EQ_THM] \\ REPEAT STRIP_TAC 298 \\ `?a t u v. x' = (a,t,u,v)` by METIS_TAC [PAIR_EQ,PAIR] 299 \\ ASM_SIMP_TAC std_ss [apply_def,IN_DEF,abs_def,lemma] 300 \\ `~(j = x)` by (FULL_SIMP_TAC bool_ss [IRANGE_def,cheney_inv_def] \\ DECIDE_TAC) 301 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 302 \\ Q.EXISTS_TAC `k` \\ Q.EXISTS_TAC `k'` 303 \\ `k IN D1 m /\ k' IN D1 m` by (SIMP_TAC std_ss [IN_DEF,D1] \\ METIS_TAC []) 304 \\ ASSUME_TAC (GSYM (UNDISCH_ALL (RW [GSYM AND_IMP_INTRO] (Q.INST [`d`|->`v`] lemma2)))) 305 \\ ASSUME_TAC (GSYM (UNDISCH_ALL (RW [GSYM AND_IMP_INTRO] 306 (Q.INST [`d`|->`v`,`k`|->`k'`,`t`|->`u`] lemma2)))) 307 \\ ASM_REWRITE_TAC [] \\ METIS_TAC []); 308 309val move_lemma2 = prove( 310 ``!i j s t. (apply (swap i j) s = t) = (s = apply (swap i j) t)``, 311 REWRITE_TAC [apply_def,swap_def,FUN_EQ_THM] 312 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 313 \\ Cases_on `x` \\ Cases_on `r` \\ Cases_on `r'` 314 \\ POP_ASSUM (ASSUME_TAC o 315 Q.SPECL [`(swap i j q,swap i j q',swap i j q'',r)`]) 316 \\ FULL_SIMP_TAC std_ss [apply_def,swap_def,IN_DEF] 317 \\ Cases_on `q= i` \\ FULL_SIMP_TAC bool_ss [] 318 \\ Cases_on `q'= i` \\ FULL_SIMP_TAC bool_ss [] 319 \\ Cases_on `q''= i` \\ FULL_SIMP_TAC bool_ss [] 320 \\ Cases_on `q= j` \\ FULL_SIMP_TAC bool_ss [] 321 \\ Cases_on `q'= j` \\ FULL_SIMP_TAC bool_ss [] 322 \\ Cases_on `q''= j` \\ FULL_SIMP_TAC bool_ss []); 323 324val cheney_inv_CUT_lemma = prove( 325 ``cheney_inv (b,b',i,j,j3,e,f,m,w,xx,r) /\ ~(j = e) /\ IRANGE(b,e)x ==> 326 (RANGE (b,i) SUBSET RANGE (b,j)) /\ ~RANGE(b,j+1)x /\ ~RANGE(b,i)j /\ ~RANGE(b,i)x /\ 327 (RANGE (b,j+1) SUBSET RANGE (b,e)) /\ RANGE (b,j) SUBSET0 RANGE (b,j + 1) /\ 328 (RANGE (i,j+1) SUBSET RANGE (b,j+1)) /\ ~RANGE(i,j+1)x /\ ~RANGE(b,b')j /\ ~RANGE(b,b')x /\ 329 ~RANGE(i,j)j /\ ~RANGE(b,e)x /\ ~RANGE(b,j)j /\ ~RANGE(b,j)x``, 330 FULL_SIMP_TAC bool_ss [SUBSET_DEF,SUBSET0_DEF,IN_INSERT] 331 \\ FULL_SIMP_TAC std_ss [IN_DEF,cheney_inv_def,RANGE_def,IRANGE_def] 332 \\ REPEAT STRIP_TAC \\ DECIDE_TAC); 333 334val RANGE_simp = prove( 335 ``!i j k. ~(i = j) ==> (RANGE(k,i+1)j = RANGE(k,i)j)``, 336 SIMP_TAC bool_ss [RANGE_def,IN_DEF] \\ DECIDE_TAC); 337 338val move_lemma = store_thm("move_lemma", 339 ``cheney_inv (b,b',i,j,j3,e,f,m,w,xx,r) /\ {x} SUBSET0 DR0(ICUT(b,e)m) ==> 340 (move(x,j,m) = (x2,j2,m2)) ==> 341 cheney_inv(b,b',i,j2,j3,e,f,m2,w,xx,r) /\ {x2} SUBSET0 RANGE(b,j2) /\ j <= j2 /\ 342 (CUT(b,j)m = CUT(b,j)m2) /\ (DR0 (ICUT(b,e)m) = DR0 (ICUT(b,e)m2)) /\ 343 (if x = 0 then x2 = 0 else (m2 x = REF x2) /\ D0 (CUT(b,j2)m2) x2) /\ 344 (!a i. (m a = REF i) ==> (m2 a = REF i)) /\ 345 (if ~(x = 0) /\ (m2 x = REF j) then j2 = j + 1 else j2 = j) /\ 346 (~(x = 0) /\ ~isREF (m x) ==> (abs m = apply (swap j x) (abs m2))) /\ x <= f``, 347 Cases_on `x = 0` \\ ASM_SIMP_TAC bool_ss [move_def,PAIR_EQ,LESS_EQ_REFL] 348 \\ ASM_SIMP_TAC bool_ss [SUBSET0_DEF,INSERT_SUBSET,EMPTY_SUBSET,IN_INSERT] 349 THEN1 (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC bool_ss [ZERO_LESS_EQ]) \\ STRIP_TAC 350 \\ `x <= f` by 351 (Cases_on `IRANGE (b,e) x` \\ FULL_SIMP_TAC bool_ss [IN_DEF,DR0,D0,R0, 352 ICUT_def,heap_type_distinct,cheney_inv_def,DECIDE ``x < j = ~(j <= x:num)``] 353 \\ METIS_TAC [heap_type_distinct]) \\ ASM_SIMP_TAC bool_ss [] 354 \\ Cases_on `isREF (m x)` \\ ASM_REWRITE_TAC [] 355 THEN1 356 (FULL_SIMP_TAC bool_ss [isREF_def,getREF_def,PAIR_EQ] 357 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ,SUBSET_REFL,LESS_EQ_REFL] 358 \\ ASM_SIMP_TAC bool_ss [] \\ REPEAT STRIP_TAC 359 \\ FULL_SIMP_TAC bool_ss [cheney_inv_def,heap_type_11] THENL [ 360 Q.PAT_X_ASSUM `R1 m = RANGE (b,j)` (fn th => REWRITE_TAC [GSYM th]) \\ DISJ2_TAC 361 \\ SIMP_TAC bool_ss [GSYM IN_EQ_SUBSET,IN_DEF,R1] \\ METIS_TAC [], 362 FULL_SIMP_TAC bool_ss [cheney_inv_def,SUBSET_DEF,IN_DEF] 363 \\ `R1 m i'` by (REWRITE_TAC [R1] \\ METIS_TAC []) \\ METIS_TAC [], 364 FULL_SIMP_TAC bool_ss [cheney_inv_def,SUBSET_DEF,IN_DEF] 365 \\ `~RANGE (b,i') i'` by (REWRITE_TAC [RANGE_def] \\ DECIDE_TAC) 366 \\ `R1 m i'` by (REWRITE_TAC [R1] \\ METIS_TAC []) \\ METIS_TAC []]) 367 \\ SIMP_TAC std_ss [LET_DEF] 368 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ ASM_SIMP_TAC bool_ss [] \\ STRIP_TAC 369 \\ `IRANGE (b,e) x /\ ?t u v. m x = DATA (t,u,v)` by 370 (FULL_SIMP_TAC bool_ss [IN_DEF,DR0,isREF_def,D0,R0,ICUT_def] 371 \\ Cases_on `IRANGE (b,e) x` 372 \\ FULL_SIMP_TAC bool_ss [heap_type_distinct] \\ METIS_TAC []) 373 \\ `~(j = e)` by 374 (CCONTR_TAC \\ FULL_SIMP_TAC bool_ss [DECIDE ``m <= n - n = (m = 0)``,cheney_inv_def] 375 \\ `x IN D0 (ICUT(b,e)m)` 376 by (FULL_SIMP_TAC bool_ss [IN_DEF,D0,ICUT_def] \\ METIS_TAC[]) 377 \\ METIS_TAC [CARD_EQ_0,NOT_IN_EMPTY]) 378 \\ `ICUT(b,e) ((x =+ (REF j)) ((j =+ m x) m)) = 379 ICUT(b,e) ((x =+ (REF j)) m)` by 380 (Cases_on `x = j` \\ ASM_REWRITE_TAC [update_update] 381 \\ SIMP_TAC std_ss [ICUT_def,FUN_EQ_THM,UPDATE_def] \\ STRIP_TAC 382 \\ Cases_on `IRANGE (b,e) x'` \\ ASM_REWRITE_TAC [] 383 \\ Cases_on `x = x'` \\ ASM_REWRITE_TAC [] 384 \\ `~(j = x')` by (FULL_SIMP_TAC bool_ss [cheney_inv_def,IRANGE_def] \\ DECIDE_TAC) 385 \\ ASM_REWRITE_TAC []) 386 \\ `abs ((x =+ REF j) ((j =+ DATA (t,u,v)) m)) = apply (swap j x) (abs m)` by 387 (Q.PAT_X_ASSUM `m x = DATA (t,u,v)` (fn th => REWRITE_TAC [GSYM th] \\ ASSUME_TAC th) 388 \\ REWRITE_TAC [GSYM move_lemma2] 389 \\ MATCH_MP_TAC (GEN_ALL move_lemma_lemma) 390 \\ Q.EXISTS_TAC `xx` \\ Q.EXISTS_TAC `f` \\ Q.EXISTS_TAC `v` 391 \\ Q.EXISTS_TAC `b` \\ Q.EXISTS_TAC `b'` \\ Q.EXISTS_TAC `i` 392 \\ Q.EXISTS_TAC `j3` \\ Q.EXISTS_TAC `e` \\ Q.EXISTS_TAC `w` 393 \\ Q.EXISTS_TAC `r` \\ Q.EXISTS_TAC `t` \\ Q.EXISTS_TAC `u` 394 \\ FULL_SIMP_TAC std_ss [cheney_inv_def] 395 \\ `j <= j /\ j < e` by DECIDE_TAC 396 \\ METIS_TAC []) 397 \\ IMP_RES_TAC cheney_inv_CUT_lemma 398 \\ REPEAT (Q.PAT_X_ASSUM `!tyu.fgh` (fn th => ALL_TAC)) 399 \\ FULL_SIMP_TAC std_ss [cheney_inv_def] 400 \\ ASM_SIMP_TAC bool_ss [CUT_update,apply_apply,swap_swap,apply_I] 401 \\ REPEAT STRIP_TAC THEN1 DECIDE_TAC THEN1 DECIDE_TAC THEN1 DECIDE_TAC 402 THEN1 403 (`~(k = j) /\ ~(k = x)` by (FULL_SIMP_TAC bool_ss [IRANGE_def] \\ DECIDE_TAC) 404 \\ ASM_SIMP_TAC bool_ss [UPDATE_def] \\ METIS_TAC [DECIDE ``j + 1 <= k ==> j <= k``]) 405 THEN1 406 (`~(k = j) /\ ~(x = k)` by DECIDE_TAC \\ ASM_SIMP_TAC bool_ss [UPDATE_def]) 407 THEN1 408 (ASM_SIMP_TAC std_ss [FUN_EQ_THM,D0,CUT_def,RANGE_def,IN_DEF] 409 \\ STRIP_TAC \\ Cases_on `x' = j` \\ ASM_REWRITE_TAC [] 410 \\ ASM_SIMP_TAC std_ss [UPDATE_def] THEN1 METIS_TAC [heap_type_distinct] 411 \\ ASM_SIMP_TAC bool_ss [DECIDE ``~(x = n) ==> (x < n + 1 = x < n)``] 412 \\ REWRITE_TAC [GSYM RANGE_def] 413 \\ Cases_on ` RANGE (b,j) x'` \\ ASM_REWRITE_TAC [heap_type_distinct] 414 \\ FULL_SIMP_TAC bool_ss [D0,FUN_EQ_THM,CUT_def] \\ METIS_TAC []) 415 THEN1 416 (MATCH_MP_TAC SUBSET0_TRANS \\ Q.EXISTS_TAC `RANGE (b,j)` \\ ASM_REWRITE_TAC []) 417 THEN1 418 (Q.PAT_X_ASSUM `m x = DATA (t,u,v)` (ASSUME_TAC o GSYM) \\ ASM_REWRITE_TAC [] 419 \\ MATCH_MP_TAC SUBSET0_TRANS \\ Q.EXISTS_TAC `DR0 (ICUT (b,e) m)` 420 \\ ONCE_REWRITE_TAC [CONJ_COMM] \\ STRIP_TAC THEN1 421 (REWRITE_TAC [DR0,SUBSET0_DEF,SUBSET_DEF,IN_INSERT] 422 \\ SIMP_TAC std_ss [IN_DEF,DR0,UPDATE_def,ICUT_def,FUN_EQ_THM,D0,R0] 423 \\ STRIP_TAC \\ Cases_on `IRANGE (b,e) x'` 424 \\ ASM_REWRITE_TAC [heap_type_distinct] \\ METIS_TAC []) 425 \\ MATCH_MP_TAC D1_SUBSET0 \\ ASM_SIMP_TAC bool_ss [CUT_update] 426 \\ Q.PAT_X_ASSUM `DATA (t,u,v) = m x` (ASSUME_TAC o GSYM) \\ ASM_REWRITE_TAC [] 427 \\ MATCH_MP_TAC SUBSET0_TRANS \\ Q.EXISTS_TAC `{t;u}` \\ STRIP_TAC THEN1 428 (REWRITE_TAC [DR0,SUBSET0_DEF,SUBSET_DEF,IN_INSERT,CUT_def] 429 \\ SIMP_TAC std_ss [IN_DEF,DR0,UPDATE_def,ICUT_def,FUN_EQ_THM,D0,R0] 430 \\ SIMP_TAC std_ss [RANGE_def,DECIDE ``j <= k /\ k < j+1 = (j = k)``,D1] 431 \\ REPEAT (POP_ASSUM (fn th => ALL_TAC)) 432 \\ REPEAT STRIP_TAC \\ Cases_on `j = k` 433 \\ FULL_SIMP_TAC bool_ss [heap_type_11,PAIR_EQ,heap_type_distinct]) 434 \\ MATCH_MP_TAC SUBSET0_TRANS \\ Q.EXISTS_TAC `D1 (ICUT (b,e) m)` \\ STRIP_TAC THEN1 435 (REWRITE_TAC [SUBSET0_DEF,INSERT_SUBSET,EMPTY_SUBSET,IN_INSERT] 436 \\ MATCH_MP_TAC (METIS_PROVE [] ``x /\ y ==> (t \/ x) /\ (d:bool \/ y)``) 437 \\ SIMP_TAC std_ss [IN_DEF,D1,ICUT_def] \\ METIS_TAC []) 438 \\ ASM_REWRITE_TAC []) 439 THEN1 440 (MATCH_MP_TAC SUBSET0_TRANS \\ Q.EXISTS_TAC `D1 (ICUT (b,e) m)` \\ STRIP_TAC THEN1 441 (REWRITE_TAC [DR0,SUBSET0_DEF,SUBSET_DEF,IN_INSERT,CUT_def,D1] 442 \\ SIMP_TAC std_ss [IN_DEF,DR0,UPDATE_def,ICUT_def,FUN_EQ_THM,D0,R0,D1] 443 \\ METIS_TAC [heap_type_11,PAIR_EQ,heap_type_distinct]) 444 \\ MATCH_MP_TAC SUBSET0_TRANS 445 \\ Q.EXISTS_TAC `DR0 (ICUT (b,e) m)` \\ ASM_REWRITE_TAC [] 446 \\ REWRITE_TAC [DR0,SUBSET0_DEF,SUBSET_DEF,IN_INSERT,CUT_def,D1] 447 \\ SIMP_TAC std_ss [IN_DEF,DR0,UPDATE_def,ICUT_def,FUN_EQ_THM,D0,R0] 448 \\ METIS_TAC [heap_type_11,PAIR_EQ,heap_type_distinct]) 449 THEN1 450 (`j < e` by DECIDE_TAC 451 \\ `m j = EMP` by METIS_TAC [LESS_EQ_REFL] 452 \\ sg `!xx. R1 ((x =+ REF j) ((j =+ DATA (t,u,v)) m)) xx = (j = xx) \/ R1 m xx` 453 THENL [ALL_TAC,ASM_SIMP_TAC bool_ss [FUN_EQ_THM,RANGE_def] \\ DECIDE_TAC] 454 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 455 \\ FULL_SIMP_TAC bool_ss [R1,UPDATE_def] THENL [ 456 Cases_on `x = k` \\ FULL_SIMP_TAC bool_ss [heap_type_11] 457 \\ Cases_on `j = k` \\ FULL_SIMP_TAC bool_ss [heap_type_distinct] \\ METIS_TAC [], 458 Q.EXISTS_TAC `x` \\ METIS_TAC [], 459 Q.EXISTS_TAC `k` \\ Cases_on `k = x` \\ FULL_SIMP_TAC std_ss [heap_type_distinct] 460 \\ Cases_on `j = k` \\ FULL_SIMP_TAC std_ss [heap_type_distinct]]) 461 THEN1 462 (Cases_on `k = j` THENL [ 463 Cases_on `i' = x` THENL [ALL_TAC, 464 Cases_on `j = i'` \\ FULL_SIMP_TAC bool_ss [UPDATE_def,heap_type_distinct] 465 \\ FULL_SIMP_TAC bool_ss [FUN_EQ_THM,R1] \\ METIS_TAC []] 466 \\ Cases_on `j' = x` THENL [ALL_TAC, 467 Cases_on `j = j'` \\ FULL_SIMP_TAC bool_ss [UPDATE_def,heap_type_distinct] 468 \\ FULL_SIMP_TAC bool_ss [FUN_EQ_THM,R1] \\ METIS_TAC []] 469 \\ ASM_SIMP_TAC bool_ss [], 470 `m i' = REF k` by 471 (Cases_on `x = i'` \\ Cases_on `j = i'` 472 \\ FULL_SIMP_TAC bool_ss [UPDATE_def,heap_type_distinct,heap_type_11] \\ METIS_TAC []) 473 \\ `m j' = REF k` by 474 (Cases_on `x = j'` \\ Cases_on `j = j'` 475 \\ FULL_SIMP_TAC bool_ss [UPDATE_def,heap_type_distinct,heap_type_11] \\ METIS_TAC []) 476 \\ METIS_TAC []]) 477 THEN1 478 (REWRITE_TAC [SUB_PLUS] 479 \\ `D0 (ICUT (b,e) ((x =+ REF j) m)) = D0 (ICUT (b,e) m) DELETE x` by 480 (REWRITE_TAC [EXTENSION,IN_DELETE] 481 \\ SIMP_TAC std_ss [IN_DEF,ICUT_def,D0,UPDATE_def] \\ STRIP_TAC 482 \\ Cases_on `IRANGE (b,e) x'` \\ ASM_REWRITE_TAC [heap_type_distinct] 483 \\ Cases_on `x' = x` \\ ASM_REWRITE_TAC [heap_type_distinct] 484 \\ simp[]) 485 \\ ASM_SIMP_TAC bool_ss [CARD_DELETE] 486 \\ `x IN D0 (ICUT (b,e) m)` by 487 (ASM_SIMP_TAC std_ss [IN_DEF,D0,ICUT_def] \\ METIS_TAC []) 488 \\ ASM_SIMP_TAC bool_ss [] \\ DECIDE_TAC) 489 THEN1 490 (`D0 (ICUT (b,e) ((x =+ REF j) m)) = D0 (ICUT (b,e) m) DELETE x` by 491 (REWRITE_TAC [EXTENSION,IN_DELETE] 492 \\ SIMP_TAC std_ss [IN_DEF,ICUT_def,D0,UPDATE_def] \\ STRIP_TAC 493 \\ Cases_on `IRANGE (b,e) x'` \\ ASM_REWRITE_TAC [heap_type_distinct] 494 \\ Cases_on `x = x'` \\ ASM_REWRITE_TAC [heap_type_distinct] \\ METIS_TAC []) 495 \\ ASM_SIMP_TAC std_ss [FINITE_DELETE]) 496 THEN1 497 (`~(0 = j)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [UPDATE_def]) 498 THEN1 499 (`j < e` by DECIDE_TAC 500 \\ `(m j = EMP) /\ (m k = REF i')` by METIS_TAC [LESS_EQ_REFL] 501 \\ Cases_on `k = j` THEN1 METIS_TAC [heap_type_distinct] 502 \\ Cases_on `k = x` THEN1 METIS_TAC [heap_type_distinct] 503 \\ ASM_SIMP_TAC std_ss [UPDATE_def]) 504 THEN1 505 (FULL_SIMP_TAC bool_ss [roots_inv_def] 506 \\ ASM_REWRITE_TAC [apply_apply] 507 \\ Q.EXISTS_TAC `swap j x o v'` \\ REWRITE_TAC [] 508 \\ REWRITE_TAC [GSYM (SIMP_CONV std_ss [] ``(f o g) o h``),swap_swap] 509 \\ SIMP_TAC std_ss [] 510 \\ SIMP_TAC std_ss [UPDATE_def] 511 \\ `m j = EMP` by METIS_TAC [LESS_OR_EQ,LESS_EQ_REFL,cheney_inv_def] 512 \\ `~isREF(m j) /\ ~isREF(m x)` by METIS_TAC [heap_type_distinct,isREF_def] 513 \\ `(v' j = j) /\ (v' x = x)` by METIS_TAC [] 514 \\ STRIP_TAC THEN1 515 (SIMP_TAC std_ss [FUN_EQ_THM,swap_def] \\ STRIP_TAC 516 \\ `!k. v' (v' k) = k` by FULL_SIMP_TAC std_ss [FUN_EQ_THM] 517 \\ Cases_on `x' = r''` \\ Cases_on `x' = h` \\ METIS_TAC []) 518 \\ STRIP_TAC THENL [ 519 STRIP_TAC \\ Cases_on `x = k` \\ ASM_SIMP_TAC bool_ss [isREF_def,heap_type_11] 520 \\ Cases_on `k = j` \\ ASM_SIMP_TAC bool_ss [heap_type_distinct] 521 \\ REPEAT STRIP_TAC THENL [ 522 `b <=i /\ i <= j ==> RANGE(b,j+1)j` by (REPEAT (POP_ASSUM (K ALL_TAC)) 523 \\ SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC) 524 \\ METIS_TAC [], 525 `~RANGE(b,j)k` by METIS_TAC [RANGE_simp] 526 \\ `v' k = k` by METIS_TAC [isREF_def] 527 \\ ASM_SIMP_TAC bool_ss [swap_def]], 528 STRIP_TAC \\ Cases_on `k = x` \\ ASM_SIMP_TAC bool_ss [heap_type_11] 529 THEN1 (SIMP_TAC std_ss [swap_def] \\ METIS_TAC []) 530 \\ Cases_on `k = j` \\ ASM_SIMP_TAC bool_ss [heap_type_distinct] 531 \\ REPEAT STRIP_TAC \\ `v' k = i'` by METIS_TAC [] 532 \\ ASM_SIMP_TAC std_ss [] 533 \\ `R1 m i'` by METIS_TAC [R1] 534 \\ `RANGE(b,j)i'` by METIS_TAC [cheney_inv_def] 535 \\ `~(j = i') /\ ~(x = i')` by METIS_TAC [] 536 \\ ASM_SIMP_TAC std_ss [swap_def]]) 537 THEN1 (SIMP_TAC std_ss [RANGE_def,IN_DEF] \\ DECIDE_TAC) 538 THEN1 539 (ASM_SIMP_TAC std_ss [DR0,D0,R0,ICUT_def,FUN_EQ_THM,UPDATE_def] \\ STRIP_TAC 540 \\ Cases_on `IRANGE (b,e) x'` \\ ASM_REWRITE_TAC [] 541 \\ Cases_on `x = x'` \\ ASM_SIMP_TAC std_ss [heap_type_11] THEN1 METIS_TAC []) 542 THEN1 (SIMP_TAC bool_ss [UPDATE_def]) 543 THEN1 (IMP_RES_TAC LESS_EQ_TRANS 544 \\ ASM_SIMP_TAC std_ss [D0,CUT_def,RANGE_def,UPDATE_def] \\ METIS_TAC []) 545 THEN1 546 (Cases_on `a = x` \\ FULL_SIMP_TAC bool_ss [] THEN1 METIS_TAC [heap_type_distinct] 547 \\ `j < e` by DECIDE_TAC 548 \\ `m j = EMP` by METIS_TAC [LESS_EQ_REFL] 549 \\ Cases_on `a = j` \\ FULL_SIMP_TAC bool_ss [] THEN1 METIS_TAC [heap_type_distinct] 550 \\ ASM_SIMP_TAC std_ss [UPDATE_def]) 551 THEN1 SIMP_TAC std_ss [UPDATE_def]); 552 553val abs_update_lemma = prove( 554 ``!m i x y d x' y'. 555 (m i = DATA (x,y,d)) /\ (m 0 = EMP) /\ 556 (if x = 0 then x' = 0 else (m x = REF x') /\ D0 m x') /\ 557 (if y = 0 then y' = 0 else (m y = REF y') /\ D0 m y') ==> 558 (abs ((i =+ DATA (x',y',d))m) = abs m)``, 559 REWRITE_TAC [FUN_EQ_THM,D0] \\ REPEAT STRIP_TAC 560 \\ `?a0 x0 y0 D0. x'' = (a0,x0,y0,D0)` by METIS_TAC [PAIR] 561 \\ ASM_SIMP_TAC bool_ss [abs_def,UPDATE_thm] 562 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC THENL [ 563 Cases_on `a0 = i` THENL [ 564 FULL_SIMP_TAC std_ss [heap_type_11] \\ STRIP_TAC 565 THENL [Cases_on `x = 0`,Cases_on `y = 0`] 566 \\ FULL_SIMP_TAC bool_ss [ADDR_def] \\ METIS_TAC [ADDR_def], 567 FULL_SIMP_TAC std_ss [heap_type_11] 568 \\ Cases_on `k = i` \\ Cases_on `k' = i` 569 \\ FULL_SIMP_TAC bool_ss [ADDR_def]], 570 Cases_on `a0 = i` THENL [ 571 FULL_SIMP_TAC std_ss [heap_type_11] \\ STRIP_TAC 572 THENL [Cases_on `x = 0`,Cases_on `y = 0`] 573 \\ FULL_SIMP_TAC bool_ss [ADDR_def] \\ METIS_TAC [ADDR_def], 574 FULL_SIMP_TAC std_ss [heap_type_11] \\ STRIP_TAC 575 \\ Cases_on `k = i` \\ Cases_on `k' = i` 576 \\ FULL_SIMP_TAC bool_ss [ADDR_def] \\ METIS_TAC [ADDR_def]]]); 577 578val maintain_lemma = prove( 579 ``!b i j j2 m x y. 580 b <= i /\ i <= j /\ 581 RANGE (i,j) SUBSET (r UNION D1 (CUT (b,i) m)) /\ 582 RANGE (j,j2) SUBSET {x;y} ==> 583 RANGE (i + 1,j2) SUBSET (r UNION D1 (CUT (b,i + 1) ((i =+ DATA (x,y,d)) m)))``, 584 SIMP_TAC bool_ss [SUBSET_DEF,IN_UNION,NOT_IN_EMPTY,IN_INSERT] 585 \\ SIMP_TAC bool_ss [IN_DEF,D1,CUT_def] \\ REPEAT STRIP_TAC 586 \\ Cases_on `r x'` \\ ASM_REWRITE_TAC [] 587 \\ sg `RANGE (j,j2) x' \/ RANGE (i,j) x'` THENL [ 588 FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC, 589 `RANGE (b,i + 1) i` by (FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC) 590 \\ Q.EXISTS_TAC `i` \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM,heap_type_11] \\ METIS_TAC [], 591 RES_TAC \\ Cases_on `RANGE(b,i)k` \\ FULL_SIMP_TAC std_ss [heap_type_distinct] 592 \\ `RANGE (b,i + 1) k /\ ~(i = k)` by (FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC) 593 \\ Q.EXISTS_TAC `k` \\ ASM_SIMP_TAC std_ss [UPDATE_def,heap_type_11] \\ METIS_TAC []]); 594 595val RANGE_split = prove( 596 ``j <= j' ==> j' <= j'' ==> (RANGE(j,j'') = RANGE (j,j') UNION RANGE(j',j''))``, 597 REWRITE_TAC [EXTENSION,IN_UNION] \\ SIMP_TAC std_ss [IN_DEF,RANGE_def] \\ DECIDE_TAC); 598 599val RANGE_lemmas = store_thm("RANGE_lemmas", 600 ``!n. (RANGE(n,n+1) = {n}) /\ (RANGE(n,n) = {})``, 601 REWRITE_TAC [EXTENSION,IN_INSERT,NOT_IN_EMPTY] 602 \\ SIMP_TAC bool_ss [RANGE_def,IN_DEF] \\ DECIDE_TAC); 603 604val PATH_CUT_expand = prove( 605 ``!p r b i j m. PATH (r,p) (basic_abs(CUT (b,i) m)) /\ i <= j ==> 606 PATH (r,p) (basic_abs(CUT (b,j) m))``, 607 Induct \\ REWRITE_TAC [PATH_def] \\ REPEAT STRIP_TAC 608 \\ `RANGE (b,i) r ==> RANGE (b,j) r` by (REWRITE_TAC [RANGE_def] \\ DECIDE_TAC) 609 \\ FULL_SIMP_TAC bool_ss [CUT_def,basic_abs,IN_DEF] 610 \\ METIS_TAC [heap_type_distinct]); 611 612val reachable_CUT_expand = prove( 613 ``!r b i j m. reachable r (basic_abs (CUT (b,i) m)) x /\ i <= j ==> 614 reachable r (basic_abs (CUT (b,j) m)) x``, 615 SIMP_TAC bool_ss [reachable_def] \\ REPEAT STRIP_TAC \\ METIS_TAC [PATH_CUT_expand]); 616 617val CUT_EQ_EMP_IMP = prove( 618 ``(CUT (b,i) m x = EMP) /\ RANGE(b,i)x ==> (m x = EMP)``, 619 SIMP_TAC std_ss [D0,CUT_def] \\ METIS_TAC []); 620 621val PATH_snoc = prove( 622 ``!ys x y z m. PATH(x,ys++[y])m /\ PATH(y,[z])m ==> PATH(x,ys++[y]++[z])m``, 623 Induct THEN1 (REWRITE_TAC [APPEND,PATH_def] \\ METIS_TAC []) 624 \\ ASM_SIMP_TAC std_ss [PATH_def,APPEND]); 625 626val move_IMP = prove( 627 ``!x j m x' j' m'. (move (x,j,m) = (x',j',m')) ==> j <= j'``, 628 SIMP_TAC std_ss [move_def,LET_DEF] \\ NTAC 6 STRIP_TAC 629 \\ Cases_on `x = 0` \\ ASM_SIMP_TAC std_ss [PAIR_EQ] 630 \\ Cases_on `isREF (m x)` \\ ASM_SIMP_TAC std_ss [PAIR_EQ] 631 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [] \\ DECIDE_TAC); 632 633val cheney_inv_step = store_thm("cheney_inv_step", 634 ``cheney_inv(b,b',i,j,j,e,f,m,w,xx,r) /\ ~(i = j) /\ 635 (cheney_step(i,j,e,m) = (i2,j2,e2,m2)) ==> (e2 = e) /\ j <= j2 /\ 636 cheney_inv(b,b',i2,j2,j2,e2,f,m2,w,xx,r)``, 637 REWRITE_TAC [cheney_step_def] 638 \\ `?x y d. getDATA (m i) = (x,y,d)` by METIS_TAC [PAIR] 639 \\ `?x' j' m'. move (x,j,m) = (x',j',m')` by METIS_TAC [PAIR] 640 \\ `?y' j'' m''. move (y,j',m') = (y',j'',m'')` by METIS_TAC [PAIR] 641 \\ ASM_SIMP_TAC std_ss [LET_DEF] 642 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 643 \\ SIMP_TAC bool_ss [] 644 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 645 \\ REPEAT STRIP_TAC 646 \\ Q.PAT_X_ASSUM `i + 1 = i2` (K ALL_TAC) 647 \\ Q.PAT_X_ASSUM `j'' = j2` (K ALL_TAC) 648 \\ Q.PAT_X_ASSUM `e = e2` (K ALL_TAC) 649 \\ Q.PAT_X_ASSUM `(i =+ DATA (x',y',d)) m'' = m2` (K ALL_TAC) 650 \\ `i <= e` by (FULL_SIMP_TAC bool_ss [cheney_inv_def] \\ DECIDE_TAC) 651 \\ Q.PAT_X_ASSUM `_ <> _` (ASSUME_TAC o GSYM) 652 \\ `?ax ay ad. m i = DATA (ax,ay,ad)` by METIS_TAC [m_DATA] 653 \\ `~IRANGE (b,e) i /\ i + 1 <= j /\ b <= i /\ i <= j /\ ~RANGE(b,i)i /\ RANGE(i,j) i` by 654 (FULL_SIMP_TAC bool_ss [cheney_inv_def,IRANGE_def,RANGE_def] \\ DECIDE_TAC) 655 \\ FULL_SIMP_TAC bool_ss [getDATA_def,PAIR_EQ] 656 \\ `{x;y} SUBSET0 D1 (CUT(i,j)m)` by 657 (SIMP_TAC bool_ss [SUBSET0_DEF,INSERT_SUBSET,EMPTY_SUBSET,IN_INSERT] 658 \\ FULL_SIMP_TAC bool_ss [IN_DEF,D1,RANGE_def,cheney_inv_def,CUT_def] 659 \\ `i <= i /\ i < j` by DECIDE_TAC 660 \\ STRIP_TAC \\ DISJ2_TAC \\ Q.EXISTS_TAC `i` \\ ASM_REWRITE_TAC [] \\ METIS_TAC []) 661 \\ `{x;y} SUBSET0 DR0 (ICUT(b,e)m)` by 662 (MATCH_MP_TAC SUBSET0_TRANS \\ METIS_TAC [cheney_inv_def]) 663 \\ `{x} SUBSET0 DR0 (ICUT(b,e)m)` by 664 FULL_SIMP_TAC bool_ss [SUBSET0_DEF,INSERT_SUBSET,EMPTY_SUBSET,IN_INSERT] 665 \\ IMP_RES_TAC move_lemma 666 \\ `{y} SUBSET0 DR0 (ICUT(b,e)m')` by 667 FULL_SIMP_TAC bool_ss [SUBSET0_DEF,INSERT_SUBSET,EMPTY_SUBSET,IN_INSERT] 668 \\ IMP_RES_TAC move_lemma 669 \\ Q.PAT_X_ASSUM `cheney_inv (b,b',i,j,j,e,f,m,w,xx,r)` (fn th => ALL_TAC) 670 \\ Q.PAT_X_ASSUM `cheney_inv (b,b',i,j',j,e,f,m',w,xx,r)` (fn th => ALL_TAC) 671 \\ FULL_SIMP_TAC bool_ss [cheney_inv_def] 672 \\ ASM_SIMP_TAC bool_ss [ICUT_update] THEN1 DECIDE_TAC 673 \\ REPEAT STRIP_TAC 674 THEN1 DECIDE_TAC 675 THEN1 DECIDE_TAC 676 THEN1 677 (`~(k = i)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [UPDATE_def]) 678 THEN1 679 (`~(k = i)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [UPDATE_def]) 680 THEN1 681 (sg `D0 (CUT (b,j'') ((i =+ DATA (x',y',d)) m'')) = 682 i INSERT D0 (CUT (b,j'') m'')` THENL [ 683 SIMP_TAC std_ss [EXTENSION,D0,CUT_def,IN_INSERT] 684 \\ SIMP_TAC std_ss [IN_DEF,D0,UPDATE_def] \\ STRIP_TAC 685 \\ Cases_on `RANGE (b,j'') x''` \\ ASM_SIMP_TAC std_ss [heap_type_distinct] 686 THEN1 (Cases_on `x'' = i` \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC []) 687 \\ FULL_SIMP_TAC bool_ss [RANGE_def,IRANGE_def] \\ DECIDE_TAC, 688 ASM_SIMP_TAC std_ss [EXTENSION,IN_INSERT] 689 \\ SIMP_TAC std_ss [RANGE_def,IN_DEF] 690 \\ STRIP_TAC \\ Cases_on `x'' = i` \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC]) 691 THEN1 692 (MATCH_MP_TAC D1_SUBSET0 693 \\ `~RANGE(b,i)i` by (REWRITE_TAC [RANGE_def] \\ DECIDE_TAC) 694 \\ ASM_SIMP_TAC bool_ss [CUT_update] 695 \\ sg `D1 (CUT (i,i + 1) ((i =+ DATA (x',y',d))m'')) = {x';y'}` THENL [ 696 ASM_SIMP_TAC std_ss [D1,EXTENSION,IN_INSERT,NOT_IN_EMPTY] 697 \\ ASM_SIMP_TAC std_ss [D1,IN_DEF,CUT_def,RANGE_def,DECIDE ``i<=k/\k<i+1 = (k = i)``] 698 \\ SIMP_TAC bool_ss [UPDATE_def] 699 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 700 \\ Cases_on `k = i` \\ FULL_SIMP_TAC bool_ss [heap_type_11,heap_type_distinct,PAIR_EQ] 701 \\ METIS_TAC [], 702 ASM_REWRITE_TAC [] 703 \\ `RANGE(b,j') SUBSET RANGE(b,j'')` by 704 (SIMP_TAC std_ss [SUBSET_DEF,IN_DEF,RANGE_def] \\ DECIDE_TAC) 705 \\ FULL_SIMP_TAC std_ss [SUBSET0_DEF,INSERT_SUBSET,EMPTY_SUBSET] 706 \\ METIS_TAC [IN_INSERT,SUBSET_DEF]]) 707 THEN1 708 (MATCH_MP_TAC maintain_lemma \\ Q.EXISTS_TAC `j` 709 \\ ASSUME_TAC (UNDISCH_ALL RANGE_split) 710 \\ ASM_SIMP_TAC bool_ss [UNION_SUBSET] \\ STRIP_TAC 711 THENL [Cases_on `~(x = 0) /\ (m' x = REF j)`,Cases_on `~(y = 0) /\ (m'' y = REF j')`] 712 \\ NTAC 2 (FULL_SIMP_TAC bool_ss 713 [heap_type_11,RANGE_lemmas,INSERT_SUBSET,IN_INSERT,EMPTY_SUBSET])) 714 THEN1 715 (`~(RANGE(i+1,j'')i)` by (REWRITE_TAC [RANGE_def] \\ DECIDE_TAC) 716 \\ ASM_SIMP_TAC bool_ss [CUT_update] 717 \\ MATCH_MP_TAC SUBSET0_TRANS 718 \\ Q.EXISTS_TAC `D1 (CUT (i,j'') m'')` \\ ASM_SIMP_TAC bool_ss [] 719 \\ SIMP_TAC std_ss [D1,SUBSET_DEF,SUBSET0_DEF,IN_INSERT] 720 \\ SIMP_TAC std_ss [D1,IN_DEF,CUT_def,RANGE_def] 721 \\ METIS_TAC [DECIDE ``i + 1 <= k /\ k < j'' ==> i <= k /\ k < j''``,heap_type_distinct]) 722 THEN1 723 (Q.PAT_X_ASSUM `R1 m'' = RANGE (b,j'')` (fn th => REWRITE_TAC [GSYM th]) 724 \\ `m'' i = DATA (ax,ay,ad)` by 725 (sg `RANGE (b,j) i /\ RANGE (b,j') i` 726 \\ FULL_SIMP_TAC bool_ss [CUT_def,FUN_EQ_THM] 727 THEN1 (REWRITE_TAC [RANGE_def] \\ DECIDE_TAC)\\ METIS_TAC []) 728 \\ SIMP_TAC std_ss [R1,IN_DEF,CUT_def,RANGE_def,SUBSET_DEF,UPDATE_def,FUN_EQ_THM] 729 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC \\ METIS_TAC [heap_type_distinct]) 730 THEN1 731 (Cases_on `i = j'''` \\ FULL_SIMP_TAC bool_ss [heap_type_distinct,UPDATE_def] 732 \\ Cases_on `i = i'` \\ FULL_SIMP_TAC bool_ss [heap_type_distinct,UPDATE_def] \\ METIS_TAC []) 733 THEN1 734 (`~(i = 0)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [UPDATE_def]) 735 THEN1 736 (MATCH_MP_TAC SUBSET_TRANS \\ Q.EXISTS_TAC `i INSERT RANGE(b,i)` \\ STRIP_TAC 737 THEN1 (REWRITE_TAC [SUBSET_DEF,IN_INSERT] \\ SIMP_TAC std_ss [IN_DEF,RANGE_def] \\ DECIDE_TAC) 738 \\ REWRITE_TAC [INSERT_SUBSET] \\ SIMP_TAC std_ss [IN_DEF] \\ STRIP_TAC THENL [ 739 SIMP_TAC std_ss [reachable_def,basic_abs] 740 \\ FULL_SIMP_TAC bool_ss [SUBSET_DEF,IN_INSERT,IN_UNION] 741 \\ FULL_SIMP_TAC bool_ss [IN_DEF] 742 \\ `(r i) \/ D1 (CUT (b,i) m'') i` by METIS_TAC [] 743 THEN1 METIS_TAC [] \\ IMP_RES_TAC D1_IMP 744 \\ `?t. r t /\ reachable t (basic_abs (CUT (b,i) m'')) h` by METIS_TAC [] 745 \\ `PATH (h,[i]) (basic_abs (CUT (b,i + 1) ((i =+ DATA (x',y',d))m'')))` by 746 (`RANGE (b,i+1) h /\ ~(h = i)` by (FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC) 747 \\ ASM_SIMP_TAC std_ss [PATH_def,APPEND,IN_DEF,basic_abs,CUT_def,UPDATE_def] 748 \\ METIS_TAC []) 749 \\ Q.EXISTS_TAC `t` \\ FULL_SIMP_TAC bool_ss [reachable_def] \\ DISJ2_TAC 750 THEN1 (Q.EXISTS_TAC `[]` \\ ASM_SIMP_TAC bool_ss [APPEND]) 751 \\ Q.EXISTS_TAC `p ++ [h]` \\ MATCH_MP_TAC PATH_snoc \\ ASM_SIMP_TAC bool_ss [] 752 \\ MATCH_MP_TAC PATH_CUT_expand \\ Q.EXISTS_TAC `i` 753 \\ ASM_SIMP_TAC bool_ss [CUT_update] \\ DECIDE_TAC, 754 FULL_SIMP_TAC std_ss [SUBSET_DEF,IN_DEF] \\ REPEAT STRIP_TAC 755 \\ `?t. r t /\ reachable t (basic_abs (CUT (b,i) m'')) x''` by METIS_TAC [] 756 \\ Q.EXISTS_TAC `t` \\ ASM_SIMP_TAC std_ss [] 757 \\ MATCH_MP_TAC reachable_CUT_expand \\ Q.EXISTS_TAC `i` 758 \\ ASM_SIMP_TAC bool_ss [CUT_update] \\ DECIDE_TAC]) 759 THEN1 760 (`m'' k = REF i'` by METIS_TAC [] 761 \\ Cases_on `k = i` \\ ASM_SIMP_TAC bool_ss [UPDATE_def] 762 \\ `RANGE(b,j'')i` by (REWRITE_TAC [RANGE_def] \\ DECIDE_TAC) 763 \\ `D0 (CUT (b,j'') m'') i` by METIS_TAC [] \\ IMP_RES_TAC D0_IMP 764 \\ `F` by METIS_TAC [heap_type_distinct]) 765 THEN1 766 (`!x i j m. D0 (CUT (i,j) m) x ==> D0 m x` by 767 (SIMP_TAC bool_ss [D0,CUT_def] \\ METIS_TAC [heap_type_distinct]) 768 \\ sg `abs ((i =+ DATA (x',y',d))m'') = abs m''` THENL [ 769 MATCH_MP_TAC (GEN_ALL abs_update_lemma) 770 \\ Q.EXISTS_TAC `x` \\ Q.EXISTS_TAC `y` \\ ASM_SIMP_TAC bool_ss [heap_type_11] 771 \\ REPEAT (Q.PAT_X_ASSUM `fgh SUBSET0 jkl` (fn th => ALL_TAC)) 772 \\ `RANGE(b,j) i /\ RANGE(b,j') i` by (REWRITE_TAC [RANGE_def] \\ DECIDE_TAC) 773 \\ `(m'' i = m i)` by (FULL_SIMP_TAC bool_ss [CUT_def,FUN_EQ_THM] \\ METIS_TAC []) 774 \\ ASM_SIMP_TAC bool_ss [] \\ STRIP_TAC 775 THEN1 (Cases_on `x = 0` \\ FULL_SIMP_TAC bool_ss [] \\ METIS_TAC []) 776 THEN1 (Cases_on `y = 0` \\ FULL_SIMP_TAC bool_ss [] \\ METIS_TAC []), 777 FULL_SIMP_TAC bool_ss [roots_inv_def] \\ Q.EXISTS_TAC `v` 778 \\ ASM_SIMP_TAC bool_ss [] \\ STRIP_TAC \\ STRIP_TAC 779 \\ `RANGE(b,j'') i` by (REWRITE_TAC [RANGE_def] \\ DECIDE_TAC) 780 \\ Cases_on `k = i` \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM,heap_type_distinct] 781 \\ METIS_TAC []])); 782 783val cheney_inv_maintained = (SIMP_RULE std_ss [] o prove)( 784 ``!i j e m. 785 (\(i,j,e,m). 786 !r. cheney_inv(b,b',i,j,j,e,f,m,w,xx,r) ==> 787 !i2 m2. (cheney(i,j,e,m) = (i2,m2)) ==> 788 cheney_inv(b,b',i2,i2,i2,e,f,m2,w,xx,r) /\ j <= i2) (i,j,e,m)``, 789 MATCH_MP_TAC cheney_ind \\ SIMP_TAC std_ss [] \\ NTAC 5 STRIP_TAC 790 \\ `?i2 j2 e2 m2. cheney_step (i,j,e,m) = (i2,j2,e2,m2)` by METIS_TAC [PAIR] 791 \\ ASM_SIMP_TAC std_ss [] \\ Cases_on `(i = j) \/ (e < i)` 792 \\ FULL_SIMP_TAC bool_ss [] \\ NTAC 3 STRIP_TAC \\ ONCE_REWRITE_TAC [cheney_def] 793 THEN1 (REWRITE_TAC [PAIR_EQ] \\ METIS_TAC [LESS_EQ_REFL]) 794 THEN1 (FULL_SIMP_TAC bool_ss [cheney_inv_def] \\ `F` by DECIDE_TAC) 795 \\ FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC cheney_inv_step \\ METIS_TAC [LESS_EQ_TRANS]); 796 797val move_roots_def = Define ` 798 (move_roots ([],j,m) = ([],j,m)) /\ 799 (move_roots (r::rs,j,m) = 800 let (r,j,m) = move(r,j,m) in 801 let (rs,j,m) = move_roots(rs,j,m) in 802 (r::rs,j,m))`; 803 804val cheney_collect_def = Define ` 805 cheney_collector(i:num,e:num,root,l,u,m) = 806 let u = ~u:bool in 807 let i = (if u then 1+l else 1) in 808 let (root,j,m) = move_roots(root,i,m) in 809 let (j,m) = cheney(i,j,i+l,m) in 810 let m = CUT (i,i+l) m in 811 (j,i+l,root,l,u,m)`; 812 813val CUT_EMPTY = prove( 814 ``!b m. (CUT (b,b) m = \x.EMP) /\ (ICUT (b,b) m = m) /\ 815 (RANGE(b,b) = \x.F) /\ (IRANGE(b,b) = \x.T)``, 816 SIMP_TAC std_ss [FUN_EQ_THM,RANGE_def,CUT_def,ICUT_def,RANGE_def,IRANGE_def] 817 \\ METIS_TAC [DECIDE ``~(b <= n /\ n < b:num)``]); 818 819val FINITE_RANGE = prove( 820 ``!j i. FINITE (RANGE(i,i+j)) /\ (CARD (RANGE(i,i+j)) = j)``, 821 Induct \\ REWRITE_TAC [CUT_EMPTY,ADD_0,FINITE_EMPTY,CARD_EMPTY,GSYM EMPTY_DEF] \\ STRIP_TAC 822 \\ sg `(RANGE (i,i + SUC j) = (i + j) INSERT RANGE (i,i + j)) /\ 823 ~((i + j) IN RANGE (i,i + j))` 824 \\ ASM_SIMP_TAC bool_ss [FINITE_INSERT,CARD_INSERT,EXTENSION,IN_INSERT] 825 \\ SIMP_TAC std_ss [IN_DEF,RANGE_def] \\ DECIDE_TAC); 826 827val FINITE_RANGE2 = store_thm("FINITE_RANGE", 828 ``!i j. FINITE (RANGE(i,j)) /\ (CARD (RANGE(i,j)) = j - i)``, 829 NTAC 2 STRIP_TAC \\ Cases_on `i <= j` 830 THEN1 (FULL_SIMP_TAC bool_ss [LESS_EQ_EXISTS,FINITE_RANGE] \\ DECIDE_TAC) 831 \\ sg `RANGE (i,j) = EMPTY` \\ ASM_REWRITE_TAC [FINITE_EMPTY,CARD_EMPTY] 832 \\ FULL_SIMP_TAC bool_ss [EXTENSION,NOT_IN_EMPTY] 833 \\ SIMP_TAC std_ss [IN_DEF,RANGE_def] \\ DECIDE_TAC); 834 835val WFS_inv_IMP_cheney_inv = store_thm("ok_state_IMP_cheney_inv", 836 ``ok_state (i,e6,r,l,u,m) ==> 837 let b = if ~u then 1 + l else 1 in 838 cheney_inv (b,b,b,b,b,b + l,l+l+1,m,m,m,{}) /\ 839 !k. MEM k r ==> {k} SUBSET0 DR0 (ICUT (b,b+l) m)``, 840 REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [LET_DEF,cheney_inv_def,ok_state_def,CUT_EMPTY] 841 \\ Q.ABBREV_TAC `b = if u then 1 + l else 1` 842 \\ Q.ABBREV_TAC `b2 = if ~u then 1 + l else 1` 843 \\ `(ICUT (b2,b2 + l) m) = m` by 844 (FULL_SIMP_TAC bool_ss [ICUT_def,FUN_EQ_THM,IN_DEF] 845 \\ sg `!k. RANGE(b,i)k ==> IRANGE (b2,b2 + l) k` 846 THENL [ALL_TAC,METIS_TAC []] \\ Q.UNABBREV_TAC `b` \\ Q.UNABBREV_TAC `b2` 847 \\ Cases_on `u` \\ FULL_SIMP_TAC bool_ss [IRANGE_def,RANGE_def] \\ DECIDE_TAC) 848 \\ ASM_REWRITE_TAC [] \\ REPEAT STRIP_TAC 849 THEN1 (Q.UNABBREV_TAC `b2` \\ Cases_on `u` \\ DECIDE_TAC) 850 THEN1 (Q.UNABBREV_TAC `b2` \\ Cases_on `u` \\ DECIDE_TAC) 851 THEN1 852 (Q.PAT_X_ASSUM `!k. ~bb:bool ==> c` MATCH_MP_TAC 853 \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def] 854 \\ Q.UNABBREV_TAC `b` \\ Q.UNABBREV_TAC `b2` \\ DECIDE_TAC) 855 THEN1 856 (Q.PAT_X_ASSUM `!k. ~bbb:bool ==> c` MATCH_MP_TAC 857 \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def] 858 \\ Q.UNABBREV_TAC `b` \\ Q.UNABBREV_TAC `b2` \\ DECIDE_TAC) 859 THEN1 (SIMP_TAC std_ss [FUN_EQ_THM,D0,heap_type_distinct]) 860 THEN1 (SIMP_TAC std_ss [SUBSET0_DEF,IN_INSERT,SUBSET_DEF] 861 \\ SIMP_TAC std_ss [IN_DEF,D1,heap_type_distinct]) 862 THEN1 (SIMP_TAC std_ss [SUBSET0_DEF,IN_INSERT,SUBSET_DEF] 863 \\ SIMP_TAC std_ss [IN_DEF,D1,heap_type_distinct]) 864 THEN1 (SIMP_TAC std_ss [SUBSET0_DEF,IN_INSERT,SUBSET_DEF] 865 \\ SIMP_TAC std_ss [IN_DEF,D1,heap_type_distinct]) 866 THEN1 867 (FULL_SIMP_TAC std_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY] 868 \\ FULL_SIMP_TAC std_ss [IN_DEF,DR0,D1,D0,ICUT_def] \\ REPEAT STRIP_TAC 869 \\ `RANGE(b,i)k` by METIS_TAC [heap_type_distinct] 870 \\ Cases_on `x = 0` \\ ASM_SIMP_TAC bool_ss [] 871 \\ `RANGE(b,i)x` by METIS_TAC [heap_type_11,PAIR_EQ] 872 \\ ASM_REWRITE_TAC [] \\ METIS_TAC []) 873 THEN1 (ASM_SIMP_TAC std_ss [FUN_EQ_THM,R1] \\ METIS_TAC [heap_type_distinct]) 874 THEN1 METIS_TAC [heap_type_distinct] 875 THEN1 876 (MATCH_MP_TAC LESS_EQ_TRANS \\ Q.EXISTS_TAC `CARD (RANGE(b,i))` \\ STRIP_TAC 877 THENL [ALL_TAC, REWRITE_TAC [FINITE_RANGE2] \\ DECIDE_TAC] 878 \\ MATCH_MP_TAC ((GEN_ALL o RW [AND_IMP_INTRO] o DISCH_ALL o 879 SPEC_ALL o UNDISCH o SPEC_ALL) CARD_SUBSET) 880 \\ FULL_SIMP_TAC std_ss [FINITE_RANGE2,SUBSET_DEF,IN_DEF,D0] 881 \\ METIS_TAC [heap_type_distinct]) 882 THEN1 883 (MATCH_MP_TAC ((GEN_ALL o RW [AND_IMP_INTRO] o DISCH_ALL o 884 SPEC_ALL o UNDISCH o SPEC_ALL) SUBSET_FINITE) 885 \\ Q.EXISTS_TAC `RANGE(b,i)` \\ FULL_SIMP_TAC std_ss [D0,SUBSET_DEF,IN_DEF,ICUT_def,FINITE_RANGE2] 886 \\ METIS_TAC [heap_type_distinct]) 887 THEN1 888 (Q.PAT_X_ASSUM `!k. ~bbb:bool ==> c` MATCH_MP_TAC 889 \\ Q.UNABBREV_TAC `b` \\ Cases_on `u` \\ FULL_SIMP_TAC bool_ss [RANGE_def,IN_DEF] \\ DECIDE_TAC) 890 THEN1 REWRITE_TAC [GSYM EMPTY_DEF,EMPTY_SUBSET] 891 THEN1 892 (REWRITE_TAC [roots_inv_def] \\ Q.EXISTS_TAC `I` \\ ASM_SIMP_TAC std_ss [apply_I] 893 \\ METIS_TAC [heap_type_distinct]) 894 THEN1 895 (Cases_on `k = 0` THEN1 ASM_SIMP_TAC std_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY] 896 \\ REWRITE_TAC [SUBSET0_DEF,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY] 897 \\ RES_TAC \\ RES_TAC \\ FULL_SIMP_TAC std_ss [IN_DEF,DR0,D0,heap_type_11] \\ METIS_TAC [])); 898 899val reachables_def = Define ` 900 reachables rs h (a,x,y,d) = (a,x,y,d) IN h /\ ?r. MEM r rs /\ a IN reachable r h`; 901 902val basic_abs_EQ_abs = prove( 903 ``!m. (!k i. ~(m k = REF i)) ==> (basic_abs m = abs m)``, 904 REWRITE_TAC [FUN_EQ_THM] \\ REPEAT STRIP_TAC 905 \\ `?a y z d. x = (a,y,z,d)` by METIS_TAC [PAIR] 906 \\ ASM_SIMP_TAC std_ss [abs_def,basic_abs] 907 \\ EQ_TAC \\ REPEAT STRIP_TAC THENL [ 908 Q.EXISTS_TAC `y` \\ Q.EXISTS_TAC `z` \\ ASM_REWRITE_TAC [] 909 \\ STRIP_TAC THENL [Cases_on `m y`,Cases_on `m z`] 910 \\ FULL_SIMP_TAC bool_ss [ADDR_def] \\ METIS_TAC [], 911 FULL_SIMP_TAC bool_ss [heap_type_11,PAIR_EQ] 912 \\ STRIP_TAC THENL [Cases_on `m k`,Cases_on `m k'`] 913 \\ FULL_SIMP_TAC bool_ss [ADDR_def] \\ METIS_TAC []]); 914 915val apply_reachables_lemma = prove( 916 ``(!x. f (g x) = x) /\ (!x. g (f x) = x) ==> 917 PATH (r,p ++ [g a]) s ==> PATH (f r,MAP f p ++ [a]) (apply g s)``, 918 STRIP_TAC \\ Q.SPEC_TAC (`r`,`r`) \\ Q.SPEC_TAC (`p`,`p`) \\ Induct 919 \\ ASM_SIMP_TAC std_ss [APPEND,MAP,PATH_def,IN_DEF,apply_def] \\ METIS_TAC []); 920 921val apply_reachables = store_thm("apply_reachables", 922 ``!r f g s. (f o g = I) /\ (g o f = I) ==> 923 (apply g (reachables r s) = reachables (MAP f r) (apply g s))``, 924 REWRITE_TAC [FUN_EQ_THM] \\ REPEAT STRIP_TAC 925 \\ `?a y z d. x = (a,y,z,d)` by METIS_TAC [PAIR] 926 \\ ASM_SIMP_TAC std_ss [reachables_def,IN_DEF,apply_def,reachable_def,MEM_MAP] 927 \\ Cases_on `s (g a,g y,g z,d)` \\ ASM_REWRITE_TAC [] 928 \\ EQ_TAC \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 929 THEN1 METIS_TAC [apply_reachables_lemma] 930 THEN1 METIS_TAC [apply_reachables_lemma] 931 THEN1 METIS_TAC [apply_reachables_lemma] 932 \\ Q.EXISTS_TAC `y'` \\ ASM_REWRITE_TAC [] 933 \\ DISJ2_TAC \\ Q.EXISTS_TAC `MAP g p` 934 \\ Q.UNDISCH_TAC `PATH (r',p ++ [a]) (apply g s)` 935 \\ ASM_REWRITE_TAC [] 936 \\ Q.SPEC_TAC (`y'`,`yy`) \\ Induct_on `p` 937 \\ ASM_SIMP_TAC std_ss [APPEND,MAP,PATH_def,IN_DEF,apply_def] \\ METIS_TAC []); 938 939val PATH_CUT = prove( 940 ``!p r x i j m. 941 RANGE(i,j)r /\ ~RANGE(i,j)x /\ PATH (r,p ++ [x]) (abs m) /\ ~(x = 0) /\ (m 0 = EMP) ==> 942 ?s d. PATH(s,[d]) (abs m) /\ RANGE(i,j)s /\ ~RANGE(i,j)d /\ ~(d = 0)``, 943 Induct THEN1 (REWRITE_TAC [APPEND] \\ METIS_TAC []) 944 \\ NTAC 6 STRIP_TAC 945 \\ CONV_TAC (RATOR_CONV (REWRITE_CONV [PATH_def,APPEND])) 946 \\ Cases_on `RANGE(i,j)h` THEN1 METIS_TAC [] 947 \\ REWRITE_TAC [PATH_def] \\ REPEAT STRIP_TAC 948 \\ `~(h = 0)` by (CCONTR_TAC \\ Cases_on `p` 949 \\ FULL_SIMP_TAC bool_ss [APPEND,PATH_def,IN_DEF,abs_def,heap_type_distinct]) 950 \\ METIS_TAC []); 951 952val fix_ADDR = prove( 953 ``!m ax ay az k k' ad b j e. 954 (m ax = DATA (k,k',ad)) /\ (!k. j <= k /\ k < e ==> (m k = EMP)) /\ 955 RANGE (b,e) ax /\ (D1 (CUT (b,j) m) SUBSET0 RANGE (b,j)) /\ (m 0 = EMP) /\ 956 (D0 (CUT (b,j) m) = RANGE (b,j)) ==> 957 (ADDR k ay (m k) = (ay = k)) /\ (ADDR k' az (m k') = (az = k'))``, 958 REPEAT STRIP_TAC THENL [ 959 Cases_on `m k` \\ ASM_SIMP_TAC bool_ss [ADDR_def] 960 \\ Cases_on `j <= ax` THEN1 METIS_TAC [heap_type_distinct,RANGE_def] 961 \\ `RANGE(b,j) ax` by FULL_SIMP_TAC bool_ss [RANGE_def,DECIDE ``~(m<=n) = n < m:num``] 962 \\ `D1 (CUT (b,j) m) k` by (ASM_SIMP_TAC std_ss [D1,CUT_def] \\ METIS_TAC []) 963 \\ FULL_SIMP_TAC bool_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT] 964 \\ FULL_SIMP_TAC bool_ss [IN_DEF] 965 \\ `RANGE (b,j) k` by METIS_TAC [heap_type_distinct] 966 \\ `D0 (CUT (b,j) m) k` by METIS_TAC [] 967 \\ IMP_RES_TAC D0_IMP \\ METIS_TAC [heap_type_distinct], 968 Cases_on `m k'` \\ ASM_SIMP_TAC bool_ss [ADDR_def] 969 \\ Cases_on `j <= ax` THEN1 METIS_TAC [heap_type_distinct,RANGE_def] 970 \\ `RANGE(b,j) ax` by FULL_SIMP_TAC bool_ss [RANGE_def,DECIDE ``~(m<=n) = n < m:num``] 971 \\ `D1 (CUT (b,j) m) k'` by (ASM_SIMP_TAC std_ss [D1,CUT_def] \\ METIS_TAC []) 972 \\ FULL_SIMP_TAC bool_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT] 973 \\ FULL_SIMP_TAC bool_ss [IN_DEF] 974 \\ `RANGE (b,j) k'` by METIS_TAC [heap_type_distinct] 975 \\ `D0 (CUT (b,j) m) k'` by METIS_TAC [] 976 \\ IMP_RES_TAC D0_IMP \\ METIS_TAC [heap_type_distinct]]); 977 978val CUT_EQ_DATA_IMP = prove( 979 ``(CUT (i,j) m y = DATA x) ==> (m y = DATA x) /\ RANGE(i,j)y``, 980 SIMP_TAC std_ss [CUT_def] \\ METIS_TAC [heap_type_distinct]); 981 982val PATH_CUT_IMP = prove( 983 ``!p b i j m. 984 (D1 (CUT (i,j) m) SUBSET0 RANGE (i,j)) /\ (D0 (CUT (i,j) m) = RANGE (i,j)) /\ (m 0 = EMP) /\ 985 PATH (b,p) (abs (CUT (i,j) m)) ==> PATH (b,p) (abs m)``, 986 Induct \\ FULL_SIMP_TAC std_ss [PATH_def,IN_DEF,abs_def,CUT_def,APPEND] 987 \\ FULL_SIMP_TAC bool_ss [GSYM CUT_def] \\ REPEAT STRIP_TAC 988 THENL [METIS_TAC [heap_type_distinct],ALL_TAC,METIS_TAC [heap_type_distinct],ALL_TAC] 989 \\ Cases_on `RANGE(i,j)b` \\ FULL_SIMP_TAC std_ss [heap_type_distinct,heap_type_11] 990 \\ FULL_SIMP_TAC std_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT] 991 \\ FULL_SIMP_TAC std_ss [IN_DEF] 992 \\ `D1 (CUT (i,j) m) k /\ D1 (CUT (i,j) m) k'` by 993 (SIMP_TAC std_ss [D1,CUT_def] \\ METIS_TAC [heap_type_distinct]) 994 \\ `~(k = 0) ==> D0 (CUT (i,j) m) k` by METIS_TAC [] 995 \\ `~(k' = 0) ==> D0 (CUT (i,j) m) k'` by METIS_TAC [] 996 THENL [Q.EXISTS_TAC `k'`,Q.EXISTS_TAC `k`] \\ Q.EXISTS_TAC `d` 997 THENL [DISJ1_TAC,DISJ2_TAC] \\ REWRITE_TAC [] 998 \\ Cases_on `k = 0` \\ Cases_on `k' = 0` \\ FULL_SIMP_TAC std_ss [ADDR_def] 999 \\ IMP_RES_TAC D0_IMP \\ FULL_SIMP_TAC bool_ss [ADDR_def] 1000 \\ METIS_TAC [ADDR_def]); 1001 1002val reachable_IMP = prove( 1003 ``!b m i j x. 1004 (D1 (CUT (i,j) m) SUBSET0 RANGE (i,j)) /\ (D0 (CUT (i,j) m) = RANGE (i,j)) /\ (m 0 = EMP) /\ 1005 reachable b (abs (CUT (i,j) m)) x ==> reachable b (abs m) x``, 1006 REWRITE_TAC [reachable_def] \\ METIS_TAC [PATH_CUT_IMP]); 1007 1008val MAP_INV = prove( 1009 ``!g f. (g o f = I) /\ (f o g = I) ==> !xs ys. (xs = MAP f ys) = (MAP g xs = ys)``, 1010 NTAC 3 STRIP_TAC \\ Induct 1011 \\ Cases_on `ys` \\ ASM_SIMP_TAC std_ss [MAP,NOT_CONS_NIL,CONS_11] 1012 \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ METIS_TAC []); 1013 1014val move_roots_spec = prove( 1015 ``!a. ((if ~u then a + l else a) = b) ==> 1016 !r j m r' j' m' w ww xx. 1017 cheney_inv (b,b,b,j,b,b+l,f,m,w:num->'a heap_type,xx:num->'a heap_type,ww) /\ 1018 (!k. MEM k r ==> {k} SUBSET0 DR0 (ICUT (b,b + l) m)) /\ 1019 (move_roots (r,j,m) = (r',j',m')) ==> 1020 cheney_inv (b,b,b,j',b,b+l,f,m',w,xx,ww) /\ j <= j' /\ 1021 (!k. MEM k r' /\ ~(k = 0) ==> RANGE (b,j') k) /\ 1022 (!k. RANGE(j,j') k ==> MEM k r') /\ 1023 (!k i. (m k = REF i) ==> (m' k = REF i)) /\ 1024 (LENGTH r = LENGTH r') /\ 1025 (!k. MEM k r /\ ~(k = 0) \/ isREF (m k) ==> isREF(m' k)) /\ 1026 (!k k'. MEM (k,k') (ZIP(r,r')) ==> if k = 0 then k' = 0 else (m' k = REF k'))``, 1027 STRIP_TAC \\ STRIP_TAC \\ Induct THEN1 1028 (ONCE_REWRITE_TAC [EQ_SYM_EQ] 1029 \\ SIMP_TAC std_ss [PAIR_EQ,move_roots_def,MEM,RANGE_lemmas,EMPTY_DEF, 1030 LESS_EQ_REFL,MAP,apply_I,ZIP]) 1031 \\ NTAC 9 STRIP_TAC 1032 \\ `?r' j' m'. move (h,j,m) = (r',j',m')` by METIS_TAC [PAIR] 1033 \\ `?rs3 j3 m3. move_roots (r,j'',m'') = (rs3,j3,m3)` by METIS_TAC [PAIR] 1034 \\ ASM_SIMP_TAC std_ss [move_roots_def,LET_DEF] 1035 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC bool_ss [MEM] \\ STRIP_TAC 1036 \\ `{h} SUBSET0 DR0 (ICUT (b,b + l) m)` by METIS_TAC [] 1037 \\ IMP_RES_TAC move_lemma 1038 \\ `!k. MEM k r ==> {k} SUBSET0 DR0 (ICUT (b,b + l) m'')` by METIS_TAC [] 1039 \\ Q.PAT_X_ASSUM `!j m r'. bb` (STRIP_ASSUME_TAC o UNDISCH_ALL o 1040 RW [GSYM AND_IMP_INTRO] o Q.SPECL [`j''`,`m''`,`rs3`,`j3`,`m3`,`w`,`ww`,`xx`]) 1041 \\ STRIP_TAC THEN1 METIS_TAC [] 1042 \\ STRIP_TAC THEN1 DECIDE_TAC 1043 \\ STRIP_TAC THEN1 1044 (REPEAT STRIP_TAC \\ Cases_on `h = 0` THEN1 METIS_TAC [] \\ FULL_SIMP_TAC bool_ss [] 1045 \\ IMP_RES_TAC D0_IMP \\ FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC) 1046 \\ STRIP_TAC THEN1 1047 (REPEAT STRIP_TAC \\ Cases_on `k = r''` THEN1 METIS_TAC [] \\ DISJ2_TAC 1048 \\ Cases_on `h = 0` THEN1 METIS_TAC [] \\ FULL_SIMP_TAC bool_ss [] \\ IMP_RES_TAC D0_IMP 1049 \\ Q.PAT_X_ASSUM `!k. RANGE (_,_) k ==> MEM k rs3` MATCH_MP_TAC 1050 \\ Cases_on ` m'' h = REF j` \\ FULL_SIMP_TAC bool_ss [heap_type_11] 1051 \\ FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC) 1052 \\ STRIP_TAC THEN1 METIS_TAC [] 1053 \\ ASM_SIMP_TAC std_ss [LENGTH,ZIP,MEM] 1054 \\ STRIP_TAC THEN1 1055 (STRIP_TAC \\ Cases_on `isREF(m k)` \\ ASM_SIMP_TAC bool_ss [] THEN1 METIS_TAC [isREF_def] 1056 \\ REPEAT STRIP_TAC THENL [ALL_TAC,METIS_TAC []] 1057 \\ `~(h = 0)` by DECIDE_TAC 1058 \\ FULL_SIMP_TAC bool_ss [move_def,LET_DEF,PAIR_EQ] 1059 \\ Q.PAT_X_ASSUM `!k. bbb ==> isREF (m3 k)` MATCH_MP_TAC \\ DISJ2_TAC 1060 \\ Q.PAT_X_ASSUM `(h =+ REF j) ((j =+ m h) m) = m''` (fn th => REWRITE_TAC [GSYM th]) 1061 \\ SIMP_TAC std_ss [isREF_def,UPDATE_def,heap_type_11]) 1062 \\ REPEAT STRIP_TAC THEN1 METIS_TAC [] 1063 \\ Cases_on `k = 0` \\ ASM_SIMP_TAC bool_ss [] \\ METIS_TAC []); 1064 1065val cheney_inv_intro = store_thm("cheney_inv_setup", 1066 ``cheney_inv (b,b,b,j,b,e,f,m',m,m,{}) ==> cheney_inv (b,j,b,j,j,e,f,m',m',m,RANGE(b,j))``, 1067 SIMP_TAC bool_ss [cheney_inv_def,LESS_EQ_REFL] \\ REPEAT STRIP_TAC 1068 THEN1 METIS_TAC [] THEN1 METIS_TAC [] 1069 THEN1 (REWRITE_TAC [SUBSET_DEF,IN_UNION] \\ SIMP_TAC bool_ss [IN_DEF]) 1070 THEN1 METIS_TAC [] \\ REWRITE_TAC [RANGE_lemmas,EMPTY_SUBSET]); 1071 1072val list_RANGE_aux_def = Define ` 1073 (list_RANGE_aux 0 n = []) /\ 1074 (list_RANGE_aux (SUC m) n = n::list_RANGE_aux m (n+1))`; 1075 1076val list_RANGE_def = Define ` 1077 list_RANGE(i,j) = list_RANGE_aux (j-i) i`; 1078 1079val list_RANGE_aux_thm = prove( 1080 ``!j i k. MEM k (list_RANGE_aux j i) = RANGE(i,i+j) k``, 1081 Induct \\ ASM_REWRITE_TAC [list_RANGE_aux_def,MEM,RANGE_lemmas,ADD_0,EMPTY_DEF] 1082 \\ REWRITE_TAC [RANGE_def] \\ DECIDE_TAC); 1083 1084val list_RANGE_thm = prove( 1085 ``!i j k. MEM k (list_RANGE(i,j)) = RANGE(i,j) k``, 1086 REWRITE_TAC [list_RANGE_def] \\ REPEAT STRIP_TAC \\ Cases_on `i <= j` THENL [ 1087 FULL_SIMP_TAC bool_ss [LESS_EQ_EXISTS] \\ `i + p - i = p` by DECIDE_TAC 1088 \\ FULL_SIMP_TAC bool_ss [LESS_EQ_EXISTS,list_RANGE_aux_thm], 1089 `j - i = 0` by DECIDE_TAC \\ ASM_SIMP_TAC bool_ss [list_RANGE_aux_def,RANGE_def,MEM] 1090 \\ DECIDE_TAC]); 1091 1092val cheney_collector_spec = store_thm("cheney_collector_spec", 1093 ``ok_state(j6,e6,r,l,u,m) /\ (cheney_collector (j6,e6,r,l,u,m) = (j2,e2,r2',l2,u2,m2)) ==> 1094 ok_state(j2,e2,r2',l2,u2,m2) /\ (l = l2) /\ 1095 ?f. (f o f = I) /\ (MAP f r = r2') /\ (f 0 = 0) /\ 1096 (apply f (reachables r (basic_abs m)) = basic_abs m2)``, 1097 ASM_SIMP_TAC std_ss [cheney_collect_def,LET_DEF] 1098 \\ Q.ABBREV_TAC `b = if ~u then 1 + l else 1` 1099 \\ Q.ABBREV_TAC `e = b + l` 1100 \\ `?r' j' m'. move_roots (r,b,m) = (r',j',m')` by METIS_TAC [PAIR] 1101 \\ `?j'' m''. cheney (b,j',e,m') = (j'',m'')` by METIS_TAC [PAIR] 1102 \\ ASM_SIMP_TAC std_ss [] 1103 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 1104 \\ SIMP_TAC std_ss [] \\ STRIP_TAC 1105 \\ Q.UNABBREV_TAC `b` 1106 \\ IMP_RES_TAC (SIMP_RULE std_ss [LET_DEF] WFS_inv_IMP_cheney_inv) 1107 \\ Q.ABBREV_TAC `b = if ~u then 1 + l else 1` 1108 \\ `(if ~u then 1 + l else 1) = b` by METIS_TAC [] 1109 \\ (STRIP_ASSUME_TAC o RW [AND_IMP_INTRO] o 1110 UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o Q.INST [`f`|->`l+l+1`] o 1111 Q.SPECL [`r`,`b`,`m`,`r'`,`j'`,`m'`,`m`,`{}`,`m`] o UNDISCH o Q.SPEC `1`) move_roots_spec 1112 \\ `cheney_inv (b,j',b,j',j',b + l,l+l+1,m',m',m,RANGE(b,j'))` by METIS_TAC [cheney_inv_intro] 1113 \\ Q.UNABBREV_TAC `e` \\ Q.ABBREV_TAC `e = b + l` 1114 \\ `cheney_inv (b,j',j'',j'',j'',e,l+l+1,m'',m',m,RANGE (b,j')) /\ j' <= j''` by METIS_TAC [cheney_inv_maintained] 1115 \\ STRIP_TAC THEN1 1116 (FULL_SIMP_TAC std_ss [cheney_inv_def,ok_state_def,LET_DEF,IN_DEF] 1117 \\ `!k. RANGE(b,j') k ==> RANGE(b,j'')k` by (REWRITE_TAC [RANGE_def] \\ DECIDE_TAC) 1118 \\ REPEAT STRIP_TAC THEN1 METIS_TAC [] THENL [ 1119 Cases_on `RANGE(b,e)k` \\ ASM_SIMP_TAC std_ss [CUT_def] 1120 \\ Q.PAT_X_ASSUM `!k. bb ==> (m'' k = EMP)` MATCH_MP_TAC 1121 \\ FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC, 1122 `D0 (CUT (b,j'') m'') k` by METIS_TAC [] \\ IMP_RES_TAC D0_IMP 1123 \\ Q.EXISTS_TAC `h` \\ Q.EXISTS_TAC `g` \\ Q.EXISTS_TAC `dd` 1124 \\ `RANGE(b,e)k` by (FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC) 1125 \\ ASM_SIMP_TAC std_ss [CUT_def] 1126 \\ MATCH_MP_TAC SUBSET0_TRANS \\ Q.EXISTS_TAC `D1 (CUT (b,j'') m'')` 1127 \\ ASM_SIMP_TAC std_ss [] 1128 \\ ASM_SIMP_TAC std_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY] 1129 \\ ASM_SIMP_TAC std_ss [IN_DEF,D1,CUT_def] \\ METIS_TAC []]) 1130 \\ `basic_abs m = abs m` by 1131 (MATCH_MP_TAC basic_abs_EQ_abs \\ FULL_SIMP_TAC bool_ss [ok_state_def,LET_DEF] 1132 \\ METIS_TAC [heap_type_distinct]) 1133 \\ ASM_SIMP_TAC bool_ss [] 1134 \\ Q.PAT_X_ASSUM `cheney_inv (b,b,b,b,b,e,l+l+1,m,m,m,{})` (K ALL_TAC) 1135 \\ Q.PAT_X_ASSUM `cheney_inv (b,j',b,j',j',e,l+l+1,m',m',m,RANGE (b,j'))` (K ALL_TAC) 1136 \\ `m' 0 = EMP` by METIS_TAC [cheney_inv_def] 1137 \\ Q.PAT_X_ASSUM `cheney_inv (b,b,b,j',b,e,l+l+1,m',m,m,{})` (K ALL_TAC) 1138 \\ FULL_SIMP_TAC bool_ss [cheney_inv_def] 1139 \\ `(\x. ?t. t IN RANGE(b,j') /\ x IN reachable t (abs m'')) 1140 SUBSET (0 INSERT RANGE (b,b+l))` by 1141 (Q.UNABBREV_TAC `e` \\ Cases_on `l = 0` THEN1 1142 (`b = j'` by DECIDE_TAC \\ ASM_SIMP_TAC bool_ss [RANGE_lemmas,NOT_IN_EMPTY] 1143 \\ REWRITE_TAC [GSYM EMPTY_DEF,EMPTY_SUBSET]) 1144 \\ REWRITE_TAC [SUBSET_DEF,IN_INSERT] \\ SIMP_TAC std_ss [IN_DEF,reachable_def] 1145 \\ REPEAT STRIP_TAC THEN1 (FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC) 1146 \\ CCONTR_TAC \\ FULL_SIMP_TAC bool_ss [] 1147 \\ `RANGE (b,b + l) t` by (FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC) 1148 \\ (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o 1149 Q.SPECL [`p`,`t`,`x`,`b`,`b+l`,`m''`]) PATH_CUT 1150 \\ FULL_SIMP_TAC bool_ss [PATH_def,IN_DEF,abs_def] 1151 \\ (Cases_on `j'' <= s` 1152 THEN1 (`s < b + l` by FULL_SIMP_TAC bool_ss [RANGE_def] \\ METIS_TAC [heap_type_distinct]) 1153 \\ `s < j''` by DECIDE_TAC 1154 \\ `RANGE(b,j'')s` by FULL_SIMP_TAC std_ss [RANGE_def] 1155 \\ `D1 (CUT (b,j'') m'') k /\ D1 (CUT (b,j'') m'') k'` by 1156 (FULL_SIMP_TAC std_ss [D1,CUT_def] \\ METIS_TAC []) 1157 \\ `~(k = 0) ==> RANGE(b,j'')k` by 1158 (FULL_SIMP_TAC bool_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT] 1159 \\ FULL_SIMP_TAC bool_ss [IN_DEF] \\ METIS_TAC []) 1160 \\ `~(k' = 0) ==> RANGE(b,j'')k'` by 1161 (FULL_SIMP_TAC bool_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT] 1162 \\ FULL_SIMP_TAC bool_ss [IN_DEF] \\ METIS_TAC [])) 1163 THENL [ 1164 `d = k` by 1165 (Cases_on `k = 0` THEN1 METIS_TAC [ADDR_def] 1166 \\ `D0 (CUT (b,j'') m'') k` by METIS_TAC [] 1167 \\ IMP_RES_TAC D0_IMP \\ METIS_TAC [ADDR_def]), 1168 `d = k'` by 1169 (Cases_on `k' = 0` THEN1 METIS_TAC [ADDR_def] 1170 \\ `D0 (CUT (b,j'') m'') k'` by METIS_TAC [] 1171 \\ IMP_RES_TAC D0_IMP \\ METIS_TAC [ADDR_def])] 1172 \\ `~RANGE(b,j'')d` by (FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC) 1173 \\ METIS_TAC []) 1174 \\ `basic_abs (CUT(b,e)m'') = reachables r' (abs m'')` by 1175 (REWRITE_TAC [METIS_PROVE [PAIR] ``!f g. (f = g) = !x y z d. f (x,y,z,d) = g (x,y,z,d)``] 1176 \\ ASM_SIMP_TAC bool_ss [reachables_def] 1177 \\ FULL_SIMP_TAC bool_ss [SUBSET_DEF,IN_INSERT] 1178 \\ FULL_SIMP_TAC bool_ss [IN_DEF,basic_abs,abs_def] 1179 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ STRIP_TAC THENL [ 1180 IMP_RES_TAC CUT_EQ_DATA_IMP 1181 \\ ASM_SIMP_TAC std_ss [heap_type_11] 1182 \\ Cases_on `x = 0` THEN1 (`F` by METIS_TAC [heap_type_distinct]) 1183 \\ Cases_on `j'' <= x` THEN1 (`F` by METIS_TAC [RANGE_def,heap_type_distinct]) 1184 \\ `RANGE(b,j'')x` by FULL_SIMP_TAC bool_ss [DECIDE ``~(m<=n)=n<m:num``,RANGE_def] 1185 \\ REPEAT STRIP_TAC THENL [ 1186 `D1 (CUT (b,j'') m'') y` by (SIMP_TAC bool_ss [CUT_def,D1] \\ METIS_TAC []) 1187 \\ Cases_on `y = 0` THEN1 METIS_TAC [ADDR_def] 1188 \\ `RANGE(b,j'')y` by 1189 (FULL_SIMP_TAC bool_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT] 1190 \\ FULL_SIMP_TAC bool_ss [IN_DEF] \\ METIS_TAC []) 1191 \\ `D0 (CUT (b,j'') m'') y` by METIS_TAC [] 1192 \\ IMP_RES_TAC D0_IMP \\ ASM_SIMP_TAC bool_ss [ADDR_def], 1193 `D1 (CUT (b,j'') m'') z` by (SIMP_TAC bool_ss [CUT_def,D1] \\ METIS_TAC []) 1194 \\ Cases_on `z = 0` THEN1 METIS_TAC [ADDR_def] 1195 \\ `RANGE(b,j'')z` by 1196 (FULL_SIMP_TAC bool_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT] 1197 \\ FULL_SIMP_TAC bool_ss [IN_DEF] \\ METIS_TAC []) 1198 \\ `D0 (CUT (b,j'') m'') z` by METIS_TAC [] 1199 \\ IMP_RES_TAC D0_IMP \\ ASM_SIMP_TAC bool_ss [ADDR_def], 1200 RES_TAC \\ Q.EXISTS_TAC `t` \\ STRIP_TAC THEN1 METIS_TAC [] 1201 \\ MATCH_MP_TAC reachable_IMP 1202 \\ Q.EXISTS_TAC `b` \\ Q.EXISTS_TAC `j''` \\ ASM_SIMP_TAC bool_ss [] 1203 \\ sg `abs (CUT (b,j'')m'') = basic_abs (CUT (b,j'') m'')` 1204 THENL [ALL_TAC,METIS_TAC []] 1205 \\ MATCH_MP_TAC (GSYM basic_abs_EQ_abs) 1206 \\ SIMP_TAC bool_ss [CUT_def] \\ NTAC 2 STRIP_TAC 1207 \\ Cases_on `RANGE(b,j'')k` \\ ASM_SIMP_TAC bool_ss [heap_type_distinct] 1208 \\ `D0 (CUT (b,j'') m'') k` by METIS_TAC [] 1209 \\ IMP_RES_TAC D0_IMP \\ ASM_SIMP_TAC bool_ss [heap_type_distinct]], 1210 Q.UNABBREV_TAC `e` \\ Cases_on `r'' = 0` THENL [ 1211 FULL_SIMP_TAC bool_ss [reachable_def] THEN1 METIS_TAC [heap_type_distinct] 1212 \\ FULL_SIMP_TAC bool_ss [PATH_def,APPEND,IN_DEF,abs_def] 1213 \\ Cases_on `p` \\ FULL_SIMP_TAC bool_ss [PATH_def,APPEND,IN_DEF,abs_def] 1214 \\ METIS_TAC [heap_type_distinct], 1215 `(x = 0) \/ RANGE (b,b + l) x` by METIS_TAC [] 1216 THEN1 METIS_TAC [heap_type_distinct] 1217 \\ ASM_SIMP_TAC bool_ss [CUT_def,heap_type_11,PAIR_EQ] 1218 \\ FULL_SIMP_TAC bool_ss [GSYM AND_IMP_INTRO] 1219 \\ `!k. j'' <= k /\ k < b + l ==> (m'' k = EMP)` by METIS_TAC [] 1220 \\ `(ADDR k y (m'' k) = (y = k)) /\ (ADDR k' z (m'' k') = (z = k'))` by 1221 (MATCH_MP_TAC fix_ADDR \\ Q.EXISTS_TAC `x` \\ Q.EXISTS_TAC `d` \\ Q.EXISTS_TAC `b` 1222 \\ Q.EXISTS_TAC `j''` \\ Q.EXISTS_TAC `b+l` \\ ASM_SIMP_TAC bool_ss []) 1223 \\ FULL_SIMP_TAC bool_ss []]]) 1224 \\ Q.PAT_X_ASSUM `roots_inv (b,j'',m'',abs m)` (STRIP_ASSUME_TAC o RW [roots_inv_def]) 1225 \\ Q.EXISTS_TAC `v` \\ ASM_SIMP_TAC bool_ss [apply_apply] 1226 \\ `apply v (reachables r (apply v (abs m''))) = 1227 reachables (MAP v r) (apply v (apply v (abs m'')))` by METIS_TAC [apply_reachables] 1228 \\ ASM_SIMP_TAC bool_ss [apply_apply,apply_I] 1229 \\ `v 0 = 0` by 1230 (`~isREF(m'' 0)` by METIS_TAC [isREF_def,heap_type_distinct] 1231 \\ `~RANGE(b,j'')0` by (REWRITE_TAC [RANGE_def] \\ DECIDE_TAC) 1232 \\ METIS_TAC []) 1233 \\ ASM_SIMP_TAC bool_ss [] 1234 \\ ONCE_REWRITE_TAC [METIS_PROVE [] ``b /\ c = b /\ (b ==> c:bool)``] 1235 \\ SIMP_TAC bool_ss [] 1236 \\ `!k k'. MEM (k,k') (ZIP (r,r')) ==> (v k = k')` by METIS_TAC [] 1237 \\ Q.UNDISCH_TAC `!k k'. MEM (k,k') (ZIP (r,r')) ==> (v k = k')` 1238 \\ Q.UNDISCH_TAC `LENGTH r = LENGTH r'` 1239 \\ REPEAT (POP_ASSUM (K ALL_TAC)) \\ Q.SPEC_TAC (`r'`,`ys`) \\ Q.SPEC_TAC (`r`,`xs`) 1240 \\ Induct THENL [ALL_TAC,STRIP_TAC] \\ Cases 1241 \\ SIMP_TAC std_ss [LENGTH,DECIDE ``~(0 = SUC n)``,MAP,ADD,EQ_ADD_RCANCEL,ZIP,MEM,CONS_11] 1242 \\ METIS_TAC [PAIR_EQ]); 1243 1244val _ = export_theory(); 1245