1 2open HolKernel boolLib bossLib Parse; 3open pred_setTheory arithmeticTheory pairTheory listTheory combinTheory finite_mapTheory; 4open cheney_gcTheory; 5 6val _ = new_theory "cheney_alloc"; 7 8infix \\ 9val op \\ = op THEN; 10val RW = REWRITE_RULE; 11val RW1 = ONCE_REWRITE_RULE; 12 13 14(* -- definitions -- *) 15 16val cheney_alloc_gc_def = Define ` 17 cheney_alloc_gc (i,e,root,l,u,m) = 18 if i < e then (i,e,root,l,u,m) else cheney_collector(i,e,root,l,u,m)`; 19 20val cheney_alloc_aux_def = Define ` 21 cheney_alloc_aux (i,e,root,l,u,m) d = 22 if i = e then (i,e,0::TL root,l,u,m) else 23 let m = (i =+ DATA(HD root,HD (TL root),d)) m in 24 (i+1,e,i::TL root,l,u,m)`; 25 26val cheney_alloc_def = Define ` 27 cheney_alloc(i,e,root,l,u,m) d = cheney_alloc_aux (cheney_alloc_gc (i,e,root,l,u,m)) d`; 28 29(* -- helper -- *) 30 31fun FORCE_PBETA_CONV tm = let 32 val (tm1,tm2) = dest_comb tm 33 val vs = fst (pairSyntax.dest_pabs tm1) 34 fun expand_pair_conv tm = ISPEC tm (GSYM pairTheory.PAIR) 35 fun get_conv vs = let 36 val (x,y) = pairSyntax.dest_pair vs 37 in expand_pair_conv THENC (RAND_CONV (get_conv y)) end 38 handle HOL_ERR e => ALL_CONV 39 in (RAND_CONV (get_conv vs) THENC PairRules.PBETA_CONV) tm end; 40 41(* -- theorems -- *) 42 43val bijection_def = Define `bijection g = ONTO g /\ ONE_ONE g`; 44 45val bijection_swap = prove( 46 ``!i j. bijection (swap i j)``, 47 SIMP_TAC std_ss [bijection_def,ONTO_DEF,ONE_ONE_THM,swap_def] 48 \\ REPEAT STRIP_TAC THENL [ 49 Cases_on `y = i` THEN1 (Q.EXISTS_TAC `j` \\ Cases_on `j = i` \\ ASM_REWRITE_TAC []) 50 \\ Cases_on `y = j` THEN1 (Q.EXISTS_TAC `i` \\ Cases_on `j = i` \\ ASM_REWRITE_TAC []) 51 \\ Q.EXISTS_TAC `y` \\ ASM_REWRITE_TAC [], 52 Cases_on `x1 = i` \\ Cases_on `x2 = i` 53 \\ Cases_on `x1 = j` \\ Cases_on `x2 = j` \\ FULL_SIMP_TAC bool_ss []]); 54 55val bijection_inv = prove( 56 ``!f. bijection f ==> ?g. (f o g = I) /\ (g o f = I) /\ bijection g``, 57 SIMP_TAC std_ss [bijection_def,ONE_ONE_DEF,ONTO_DEF,FUN_EQ_THM] 58 \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `\x. @y. f y = x` \\ METIS_TAC []); 59 60val bijection_bijection = prove( 61 ``!f g. bijection f /\ bijection g ==> bijection (f o g)``, 62 SIMP_TAC std_ss [bijection_def,ONTO_DEF,ONE_ONE_THM] \\ METIS_TAC []); 63 64val basic_abs = basic_abs_def 65 66val ok_abs_def = Define ` 67 ok_abs (r,h:(num|->(num#num#'a)),l:num) = 68 ~(0 IN FDOM h) /\ FEVERY (\(x,y,z,d). {y;z} SUBSET0 FDOM h) h /\ 69 (!k. MEM k r /\ ~(k = 0) ==> k IN FDOM h)`; 70 71val ch_set_def = Define `ch_set h (x,y,z,d) = (h ' x = (y,z,d)) /\ x IN FDOM h`; 72 73val abstract_def = Define ` 74 abstract(b,m) = { (b(x), b(y), b(z), d) |(x,y,z,d)| m(x) = DATA(y,z,d) }`; 75 76val ch_inv_def = Define ` 77 ch_inv (r,h,l) (i,e,c,l',u,m) = 78 ok_state (i,e,c,l,u,m) /\ ok_abs (r,h,l) /\ (l = l') /\ 79 ?b. bijection b /\ (b 0 = 0) /\ (MAP b c = r) /\ 80 reachables r (ch_set(h)) SUBSET abstract(b,m) /\ abstract(b,m) SUBSET ch_set(h)`; 81 82val apply_abstract = prove( 83 ``!b m. bijection b ==> (apply b (abstract(b,m)) = basic_abs m)``, 84 REWRITE_TAC [METIS_PROVE [PAIR] ``!f g. (f = g) = !x y z d. f (x,y,z,d) = g (x,y,z,d)``] 85 \\ SIMP_TAC bool_ss [apply_def,abstract_def,GSPECIFICATION,basic_abs] 86 \\ REPEAT STRIP_TAC \\ REVERSE EQ_TAC \\ REPEAT STRIP_TAC 87 THEN1 (Q.EXISTS_TAC `(x,y,z,d)` \\ ASM_SIMP_TAC std_ss []) 88 \\ Cases_on `x'` \\ Cases_on `r` \\ Cases_on `r'` 89 \\ FULL_SIMP_TAC std_ss [bijection_def,ONE_ONE_DEF] \\ METIS_TAC []); 90 91val SUBSET_IMP_apply_SUBSET = prove( 92 ``!b s t. s SUBSET t ==> apply b s SUBSET apply b t``, 93 SIMP_TAC bool_ss [SUBSET_DEF,IN_DEF,apply_def, 94 METIS_PROVE [PAIR] ``(!x. f x ==> g x) = !x y z d. f (x,y,z,d) ==> g (x,y,z,d)``]); 95 96val SUBSET_EQ_apply_SUBSET = prove( 97 ``!b s t. bijection b ==> (s SUBSET t = apply b s SUBSET apply b t)``, 98 REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC THEN1 METIS_TAC [SUBSET_IMP_apply_SUBSET] 99 \\ IMP_RES_TAC bijection_inv \\ METIS_TAC [apply_apply,apply_I,SUBSET_IMP_apply_SUBSET]); 100 101val ch_inv_thm = prove( 102 ``ch_inv (r,h,l) (i,e,c,l',u,m) = 103 ok_state (i,e,c,l,u,m) /\ ok_abs (r,h,l) /\ (l = l') /\ 104 ?b. bijection b /\ (b 0 = 0) /\ (MAP b c = r) /\ 105 (basic_abs m SUBSET apply b (ch_set h)) /\ 106 (apply b (reachables r (ch_set h)) SUBSET basic_abs m)``, 107 METIS_TAC [SUBSET_EQ_apply_SUBSET,apply_abstract,ch_inv_def]); 108 109val INFINITE_num = prove( 110 ``INFINITE (UNIV:num->bool)``, 111 REWRITE_TAC [INFINITE_UNIV] \\ Q.EXISTS_TAC `SUC` 112 \\ SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `0` \\ DECIDE_TAC); 113 114val fresh_def = Define `fresh (h:num|->(num#num#'a)) = @x:num. ~(x IN 0 INSERT FDOM h)`; 115 116val fresh_NOT_IN_FDOM = (SIMP_RULE std_ss [IN_INSERT] o prove)( 117 ``!h. ~(fresh h IN 0 INSERT FDOM h)``, 118 REWRITE_TAC [fresh_def] \\ METIS_TAC [NOT_IN_FINITE,INFINITE_num,FINITE_INSERT,FDOM_FINITE]); 119 120val _ = save_thm("fresh_NOT_IN_FDOM",fresh_NOT_IN_FDOM); 121 122val fresh_THM = prove( 123 ``FEVERY (\(x,y,z,d). {y; z} SUBSET0 FDOM h) h ==> 124 !y z d. ~((fresh h,y,z,d) IN ch_set h) /\ ~((z,fresh h,y,d) IN ch_set h) /\ 125 ~((y,z,fresh h,d) IN ch_set h) /\ ~(fresh h = 0)``, 126 SIMP_TAC std_ss [fresh_NOT_IN_FDOM,IN_DEF,ch_set_def,FEVERY_DEF] 127 \\ REWRITE_TAC [METIS_PROVE [] ``x \/ ~y = y ==> x:bool``] 128 \\ REPEAT STRIP_TAC \\ RES_TAC \\ Q.PAT_X_ASSUM `h ' qq = gh` ASSUME_TAC 129 \\ FULL_SIMP_TAC std_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY,IN_DEF] 130 \\ METIS_TAC [SIMP_RULE std_ss [IN_DEF] fresh_NOT_IN_FDOM]); 131 132val INSERT_THM = prove( 133 ``!x s. x INSERT s = \y. (x = y) \/ s y``, 134 SIMP_TAC std_ss [EXTENSION,IN_INSERT] \\ SIMP_TAC std_ss [IN_DEF] \\ METIS_TAC []); 135 136val apply_INSERT = prove( 137 ``!k f. (f o k = I) ==> (k o f = I) ==> !x y z d s. 138 (apply f ((x:num,y,z,d:'a) INSERT s) = ((k x):num,k y,k z,d) INSERT apply f s)``, 139 REWRITE_TAC [METIS_PROVE [PAIR] ``!f g. (f = g) = !x y z d. f (x,y,z,d) = g (x,y,z,d)``] 140 \\ SIMP_TAC std_ss [apply_def,IN_DEF,INSERT_THM,FUN_EQ_THM] \\ METIS_TAC []); 141 142val PATH_SUBSET = prove( 143 ``!xs x s t. PATH (x,xs) s /\ s SUBSET t ==> PATH (x,xs) t``, 144 Induct \\ FULL_SIMP_TAC std_ss[PATH_def,SUBSET_DEF] \\ METIS_TAC []); 145 146val fix_MEM = prove(``set l x = MEM x l``, SIMP_TAC bool_ss [IN_DEF]) 147 148val reachables_reachables = prove( 149 ``!c s. reachables c (reachables c s) = reachables c s``, 150 REWRITE_TAC [METIS_PROVE [PAIR] ``!f g. (f = g) = !x y z d. f (x,y,z,d) = g (x,y,z,d)``] 151 \\ REPEAT STRIP_TAC \\ SIMP_TAC std_ss [reachables_def,IN_DEF] 152 \\ REWRITE_TAC [fix_MEM] 153 \\ EQ_TAC \\ SIMP_TAC std_ss [] \\ REWRITE_TAC [reachable_def] 154 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC bool_ss [] 155 \\ Q.EXISTS_TAC `r` \\ ASM_SIMP_TAC bool_ss [] \\ DISJ2_TAC \\ Q.EXISTS_TAC `p` 156 \\ REPEAT (POP_ASSUM (fn th => ASSUME_TAC th \\ UNDISCH_TAC (concl th))) 157 \\ Q.SPEC_TAC(`d`,`d`) \\ Q.SPEC_TAC(`z`,`z`) \\ Q.SPEC_TAC(`y`,`y`) 158 \\ Q.SPEC_TAC(`x`,`x`) \\ Q.SPEC_TAC(`c`,`c`) \\ Q.SPEC_TAC(`r`,`r`) 159 \\ Induct_on `p` \\ REWRITE_TAC [APPEND,PATH_def] 160 THEN1 (SIMP_TAC std_ss [PATH_def,IN_DEF,reachables_def,reachable_def] \\ METIS_TAC []) 161 \\ NTAC 8 STRIP_TAC \\ RES_TAC 162 \\ FULL_SIMP_TAC std_ss [reachables_def,IN_DEF,reachable_def] 163 \\ FULL_SIMP_TAC bool_ss [fix_MEM] \\ REPEAT STRIP_TAC 164 THENL [ALL_TAC,METIS_TAC [],ALL_TAC,METIS_TAC []] 165 \\ MATCH_MP_TAC PATH_SUBSET \\ Q.EXISTS_TAC `reachables [h] s` 166 \\ (STRIP_TAC THEN1 METIS_TAC [MEM]) 167 \\ ASM_SIMP_TAC bool_ss [SUBSET_DEF,IN_DEF] 168 \\ Cases \\ Cases_on `r'` \\ Cases_on `r''` 169 \\ SIMP_TAC std_ss [reachables_def,IN_DEF,reachable_def,MEM] 170 \\ REWRITE_TAC [fix_MEM] 171 \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `r` \\ ASM_SIMP_TAC bool_ss [] \\ DISJ2_TAC THENL [ 172 Q.EXISTS_TAC `[]` \\ ASM_REWRITE_TAC [APPEND,PATH_def,IN_DEF] \\ METIS_TAC [], 173 Q.EXISTS_TAC `h::p'` \\ ASM_REWRITE_TAC [APPEND,PATH_def,IN_DEF] \\ METIS_TAC [], 174 Q.EXISTS_TAC `[]` \\ ASM_REWRITE_TAC [APPEND,PATH_def,IN_DEF] \\ METIS_TAC [], 175 Q.EXISTS_TAC `h::p'` \\ ASM_REWRITE_TAC [APPEND,PATH_def,IN_DEF] \\ METIS_TAC []]); 176 177val bijection_apply = prove( 178 ``!b. bijection b ==> bijection (apply b)``, 179 REPEAT STRIP_TAC \\ IMP_RES_TAC bijection_inv 180 \\ SIMP_TAC std_ss [bijection_def,ONE_ONE_DEF,ONTO_DEF] \\ REPEAT STRIP_TAC 181 THEN1 (Q.EXISTS_TAC `apply g y` \\ ASM_REWRITE_TAC [apply_apply,apply_I]) 182 \\ SIMP_TAC std_ss [EXTENSION,IN_DEF] 183 \\ Cases \\ Cases_on `r` \\ Cases_on `r'` 184 \\ Q.SPEC_TAC (`q`,`x`) \\ Q.SPEC_TAC (`q'`,`y`) \\ Q.SPEC_TAC (`q''`,`z`) \\ Q.SPEC_TAC (`r`,`d`) 185 \\ CCONTR_TAC \\ FULL_SIMP_TAC bool_ss [] 186 \\ `apply b x1 (g x,g y,g z,d) = apply b x2 (g x,g y,g z,d)` by METIS_TAC [] 187 \\ FULL_SIMP_TAC bool_ss [apply_def] 188 \\ sg `!x. b (g x) = x` \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM,IN_DEF]); 189 190val CARD_EQ_CARD_apply = prove( 191 ``!s:('a#'a#'a#'b)set b:'a->'a. FINITE s /\ bijection b ==> (CARD s = CARD (apply b s))``, 192 REPEAT STRIP_TAC \\ (MATCH_MP_TAC o RW [AND_IMP_INTRO] o 193 Q.GEN `f` o DISCH_ALL o SPEC_ALL o UNDISCH o SPEC_ALL) FINITE_BIJ_CARD_EQ 194 \\ ASM_REWRITE_TAC [] 195 \\ `?k. (b o k = I) /\ (k o b = I) /\ bijection k` by METIS_TAC [bijection_inv] 196 \\ Q.EXISTS_TAC `\x. (k (FST x),k (FST (SND x)),k (FST (SND (SND x))),SND (SND (SND x)))` 197 \\ SIMP_TAC std_ss [BIJ_DEF,INJ_DEF,SURJ_DEF] \\ REPEAT STRIP_TAC THENL [ 198 Cases_on `x` \\ Cases_on `r` \\ Cases_on `r'` 199 \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM,IN_DEF,apply_def], 200 Cases_on `x` \\ Cases_on `r` \\ Cases_on `r'` 201 \\ Cases_on `x'` \\ Cases_on `r'` \\ Cases_on `r''` 202 \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC [bijection_def,ONE_ONE_DEF], 203 Cases_on `x` \\ Cases_on `r` \\ Cases_on `r'` 204 \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM,IN_DEF,apply_def], 205 Cases_on `x` \\ Cases_on `r` \\ Cases_on `r'` 206 \\ Q.EXISTS_TAC `(b q,b q',b q'',r)` 207 \\ FULL_SIMP_TAC std_ss [IN_DEF,apply_def,FUN_EQ_THM], 208 MATCH_MP_TAC 209 (Q.ISPEC `\x. (b (FST x):'a,b (FST (SND x)):'a,b (FST (SND (SND x))):'a,SND (SND (SND x)):'b)` FINITE_INJ) 210 \\ Q.EXISTS_TAC `s` \\ ASM_SIMP_TAC std_ss [BIJ_DEF,INJ_DEF,SURJ_DEF] 211 \\ REPEAT STRIP_TAC \\ Cases_on `x` \\ Cases_on `r` \\ Cases_on `r'` 212 \\ FULL_SIMP_TAC std_ss [BIJ_DEF,INJ_DEF,SURJ_DEF,IN_DEF,apply_def] 213 \\ Cases_on `x'` \\ Cases_on `r'` \\ Cases_on `r''` 214 \\ FULL_SIMP_TAC std_ss [BIJ_DEF,INJ_DEF,SURJ_DEF,IN_DEF,apply_def] 215 \\ METIS_TAC [bijection_def,ONE_ONE_DEF]]); 216 217val apply_switch = prove( 218 ``!f f' x x'. (f o f' = I) /\ (x' = apply f x) ==> (x = apply f' x')``, 219 SIMP_TAC bool_ss [apply_apply,apply_I]); 220 221val ok_state_part_def = Define ` 222 ok_state_part (i,j,m) = 223 !k. if ~RANGE(i,j) k then m k = EMP else ?y z d. m k = DATA (y,z,d)`; 224 225val WFS_part_IMP_CUT = prove( 226 ``ok_state_part(i,j,m) ==> (m = CUT (i,j)m)``, 227 SIMP_TAC std_ss [ok_state_part_def,LET_DEF,IN_DEF,CUT_def,FUN_EQ_THM] 228 \\ REPEAT STRIP_TAC \\ METIS_TAC []); 229 230val WFS_IMP_CUT = prove( 231 ``ok_state(i,e,r,l,u,m) ==> (m = CUT (if u then 1 + l else 1,i)m)``, 232 SIMP_TAC std_ss [ok_state_def,LET_DEF,IN_DEF,CUT_def,FUN_EQ_THM] 233 \\ REPEAT STRIP_TAC \\ METIS_TAC []); 234 235val FINITE_basic_abs_CUT = prove( 236 ``!j i m. FINITE (basic_abs (CUT(i,j)m))``, 237 REPEAT STRIP_TAC 238 \\ MATCH_MP_TAC (INST_TYPE [``:'a``|->``:(num#num#num#'a)``,``:'b``|->``:num``] FINITE_INJ) 239 \\ Q.EXISTS_TAC `FST` \\ Q.EXISTS_TAC `RANGE(i,j)` 240 \\ SIMP_TAC std_ss [INJ_DEF,FINITE_RANGE] \\ REPEAT STRIP_TAC 241 \\ Cases_on `x` \\ Cases_on `r` \\ Cases_on `r'` 242 THEN1 (FULL_SIMP_TAC std_ss [IN_DEF,basic_abs,CUT_def] \\ METIS_TAC [heap_type_distinct]) 243 \\ Cases_on `y` \\ Cases_on `r'` \\ Cases_on `r''` 244 \\ FULL_SIMP_TAC std_ss [IN_DEF,basic_abs,CUT_def,heap_type_11] \\ METIS_TAC []); 245 246val ok_state_CARD_EQ_lemma = prove( 247 ``!j i m. ok_state_part (i,i+j,m) ==> (CARD (basic_abs m) = j)``, 248 Induct THENL [ 249 SIMP_TAC std_ss [ok_state_part_def,LET_DEF,RANGE_lemmas,EMPTY_DEF] 250 \\ REPEAT STRIP_TAC \\ sg `basic_abs m = {}` \\ ASM_REWRITE_TAC [CARD_EMPTY] 251 \\ SIMP_TAC std_ss[FUN_EQ_THM,EMPTY_DEF] 252 \\ Cases \\ Cases_on `r` \\ Cases_on `r'` 253 \\ ASM_SIMP_TAC std_ss[basic_abs,heap_type_distinct], 254 REPEAT STRIP_TAC \\ sg `ok_state_part (i,i+j,(i+j =+ EMP) m)` THENL [ 255 FULL_SIMP_TAC std_ss [ok_state_part_def,LET_DEF] \\ REPEAT STRIP_TAC 256 \\ Cases_on `RANGE(i,i+j)k` \\ ASM_SIMP_TAC std_ss [UPDATE_def] THENL [ 257 `~(i + j = k) /\ RANGE(i,i+SUC j)k` by (FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC) 258 \\ METIS_TAC [], 259 Cases_on `i + j = k` \\ ASM_SIMP_TAC bool_ss [] 260 \\ `~RANGE(i,i+SUC j)k` by (FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC) 261 \\ METIS_TAC []], 262 RES_TAC 263 \\ `RANGE(i,i+SUC j)(i+j)` by (FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC) 264 \\ `?x y d. m (i + j) = DATA(x,y,d)` by METIS_TAC [ok_state_part_def] 265 \\ Q.ABBREV_TAC `xxx = basic_abs ((i+j =+ EMP) m)` 266 \\ sg `(basic_abs m = (i+j,x,y,d) INSERT xxx) /\ ~((i+j,x,y,d) IN xxx)` 267 \\ REWRITE_TAC [METIS_PROVE [PAIR] ``!f g. (f = g) = !x y z d. f (x,y,z,d) = g (x,y,z,d)``] 268 \\ Q.UNABBREV_TAC `xxx` THENL [ 269 SIMP_TAC std_ss [INSERT_THM,IN_DEF,basic_abs,UPDATE_def,heap_type_distinct] 270 \\ REPEAT STRIP_TAC 271 \\ Cases_on `x' = i + j` \\ ASM_SIMP_TAC std_ss [heap_type_11,heap_type_distinct], 272 `FINITE (basic_abs m)` by METIS_TAC [WFS_part_IMP_CUT,FINITE_basic_abs_CUT] 273 \\ METIS_TAC [CARD_INSERT,FINITE_INSERT]]]]); 274 275val ok_state_CARD_EQ = prove( 276 ``!j i m. ok_state_part (i,j,m) ==> (CARD (basic_abs m) = j - i)``, 277 NTAC 3 STRIP_TAC \\ Cases_on `i <= j` THENL [ 278 FULL_SIMP_TAC bool_ss [LESS_EQ_EXISTS] 279 \\ `i + p - i = p` by DECIDE_TAC \\ METIS_TAC [ok_state_CARD_EQ_lemma], 280 ` (j - i = 0) /\ !k.~RANGE(i,j)k` by (REWRITE_TAC [RANGE_def] \\ DECIDE_TAC) 281 \\ ASM_SIMP_TAC bool_ss [ok_state_part_def] \\ STRIP_TAC 282 \\ sg `basic_abs m = {}` \\ ASM_SIMP_TAC bool_ss [CARD_EMPTY] 283 \\ REWRITE_TAC [METIS_PROVE [PAIR] ``!f g. (f = g) = !x y z d. f (x,y,z,d) = g (x,y,z,d)``] 284 \\ ASM_REWRITE_TAC [basic_abs,EMPTY_DEF,heap_type_distinct]]); 285 286val WFS_IMP_WFS_part = prove( 287 ``ok_state (i,e,c,l,u,m) ==> ok_state_part (if u then 1 + l else 1,i,m)``, 288 SIMP_TAC std_ss [LET_DEF,ok_state_def,ok_state_part_def,IN_DEF] \\ METIS_TAC []); 289 290val MAP_INV = prove( 291 ``!f g xs ys. (MAP f xs = ys) /\ (g o f = I) /\ (f o g = I) ==> (MAP g ys = xs)``, 292 Induct_on `xs` \\ Cases_on `ys` \\ FULL_SIMP_TAC std_ss [MAP,NOT_CONS_NIL,FUN_EQ_THM,CONS_11] 293 \\ METIS_TAC []); 294 295val reachables_SUBSET = prove( 296 ``!x s. t SUBSET s ==> reachables x t SUBSET s``, 297 SIMP_TAC bool_ss [SUBSET_DEF,IN_DEF] \\ REPEAT STRIP_TAC 298 \\ Cases_on `x'` \\ Cases_on `r` \\ Cases_on `r'` 299 \\ FULL_SIMP_TAC std_ss [reachables_def,IN_DEF] \\ METIS_TAC []); 300 301val apply_SUBSET = prove( 302 ``!f s t. t SUBSET s ==> apply f t SUBSET apply f s``, 303 SIMP_TAC bool_ss [SUBSET_DEF,IN_DEF] \\ REPEAT STRIP_TAC 304 \\ Cases_on `x` \\ Cases_on `r` \\ Cases_on `r'` 305 \\ FULL_SIMP_TAC std_ss [apply_def,IN_DEF] \\ METIS_TAC []); 306 307val EXPAND_SUBSET = prove( 308 ``!t s. t SUBSET s = !x y z d. t (x,y,z,d) ==> s (x,y,z,d)``, 309 SIMP_TAC std_ss [SUBSET_DEF,IN_DEF] \\ METIS_TAC [PAIR,PAIR_EQ]); 310 311val FINITE_set = prove( 312 ``!h:num|->num#num#'a. FINITE (ch_set h)``, 313 CONV_TAC (QUANT_CONV (UNBETA_CONV ``h:num|->num#num#'a``)) 314 \\ MATCH_MP_TAC fmap_INDUCT \\ SIMP_TAC bool_ss [] \\ REPEAT STRIP_TAC THENL [ 315 sg `ch_set (FEMPTY:num|->num#num#'a) = {}` 316 \\ ASM_SIMP_TAC bool_ss [FINITE_EMPTY] 317 \\ ASM_SIMP_TAC bool_ss [FINITE_EMPTY,ch_set_def,EMPTY_DEF,FDOM_FEMPTY,IN_DEF, 318 METIS_PROVE [PAIR] ``!f g. (f = g) = !x y z d. f (x,y,z,d) = g (x,y,z,d)``], 319 sg `ch_set ((f |+ (x,y)):num|->num#num#'a) = (x,y) INSERT ch_set f` 320 \\ ASM_SIMP_TAC std_ss [FINITE_INSERT] 321 \\ FULL_SIMP_TAC bool_ss [ch_set_def,INSERT_THM,FAPPLY_FUPDATE_THM,FDOM_FUPDATE,IN_DEF, 322 METIS_PROVE [PAIR] ``!f g. (f = g) = !x y z d. f (x,y,z,d) = g (x,y,z,d)``] 323 \\ Cases_on `y` \\ Cases_on `r` \\ METIS_TAC [PAIR_EQ]]); 324 325val cheney_alloc_gc_spec = store_thm("cheney_alloc_gc_spec", 326 ``(cheney_alloc_gc (i,e,c,l,u,m) = (i',e',c',l',u',m')) ==> 327 ch_inv (r,h,l) (i,e,c,l,u,m) /\ CARD (reachables r (ch_set h)) < l ==> 328 i' < e' /\ ch_inv (r,h,l) (i',e',c',l',u',m')``, 329 Cases_on `i < e` \\ ASM_SIMP_TAC bool_ss [PAIR_EQ,cheney_alloc_gc_def] THEN1 METIS_TAC [] 330 \\ POP_ASSUM (K ALL_TAC) 331 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC bool_ss [ch_inv_thm] 332 \\ IMP_RES_TAC cheney_collector_spec \\ ASM_SIMP_TAC bool_ss [] 333 \\ `bijection f` by (FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ METIS_TAC [ONE_ONE_DEF,ONTO_DEF,bijection_def]) 334 \\ `apply b (reachables r (ch_set h)) = apply f (basic_abs m')` by 335 (REWRITE_TAC [METIS_PROVE [PAIR] ``!f g. (f = g) = !x y z d. f (x,y,z,d) = g (x,y,z,d)``] 336 \\ Q.PAT_X_ASSUM `apply f (reachables c (basic_abs m)) = basic_abs m'` 337 (fn th => ASM_REWRITE_TAC [GSYM th,apply_apply,apply_I]) 338 \\ `?k. (b o k = I) /\ (k o b = I) /\ bijection k` by METIS_TAC [bijection_inv] 339 \\ IMP_RES_TAC (Q.ISPECL [`r:num list`,`f:num->num`,`g:num->num`,`s:(num#num#num#'a)set`] apply_reachables) 340 \\ IMP_RES_TAC MAP_INV \\ FULL_SIMP_TAC bool_ss [] 341 \\ REPEAT (Q.PAT_X_ASSUM `!hj.jk` (K ALL_TAC)) 342 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC THENL [ 343 REWRITE_TAC [reachables_def] 344 \\ STRIP_TAC THEN1 (FULL_SIMP_TAC bool_ss [SUBSET_DEF,IN_DEF] \\ METIS_TAC []) 345 \\ FULL_SIMP_TAC bool_ss [reachables_def,IN_DEF,reachable_def] THEN1 METIS_TAC [] 346 \\ FULL_SIMP_TAC bool_ss [fix_MEM] 347 \\ Q.EXISTS_TAC `r'` \\ ASM_REWRITE_TAC [] \\ DISJ2_TAC \\ Q.EXISTS_TAC `p` 348 \\ Q.UNDISCH_TAC `PATH (r',p ++ [x]) (apply b (ch_set h))` 349 \\ `reachables [r'] (apply b (ch_set h)) SUBSET basic_abs m` by 350 (MATCH_MP_TAC SUBSET_TRANS \\ Q.EXISTS_TAC `reachables c (apply b (ch_set h))` 351 \\ ASM_SIMP_TAC bool_ss [] 352 \\ ASM_SIMP_TAC std_ss [SUBSET_DEF,IN_DEF] 353 \\ Cases \\ Cases_on `r''` \\ Cases_on `r'''` 354 \\ ASM_SIMP_TAC std_ss [reachables_def,MEM] \\ METIS_TAC []) 355 \\ Q.UNDISCH_TAC `reachables [r'] (apply b (ch_set h)) SUBSET basic_abs m` 356 \\ Q.SPEC_TAC (`r'`,`rr`) \\ Induct_on `p` THEN1 357 (SIMP_TAC bool_ss [APPEND,PATH_def,EXPAND_SUBSET,reachables_def,MEM,IN_DEF] 358 \\ METIS_TAC [reachable_def]) 359 \\ SIMP_TAC std_ss [APPEND,PATH_def] \\ REPEAT STRIP_TAC THENL [ 360 `reachables [h'] (apply b (ch_set h)) SUBSET reachables [rr] (apply b (ch_set h))` by 361 (ASM_SIMP_TAC bool_ss [EXPAND_SUBSET,reachables_def,MEM,reachable_def,IN_DEF] 362 \\ REPEAT STRIP_TAC \\ DISJ2_TAC THENL [ 363 Q.EXISTS_TAC `[]` \\ ASM_SIMP_TAC bool_ss [PATH_def,APPEND] \\ METIS_TAC [], 364 Q.EXISTS_TAC `h'::p'` \\ ASM_SIMP_TAC bool_ss [PATH_def,APPEND] \\ METIS_TAC []]) 365 \\ METIS_TAC [SUBSET_TRANS], 366 `reachables [rr] (apply b (ch_set h)) (rr,h',z',d')` by 367 (FULL_SIMP_TAC std_ss [reachables_def,MEM,IN_DEF,reachable_def] \\ METIS_TAC []) 368 \\ FULL_SIMP_TAC bool_ss [IN_DEF,SUBSET_DEF] \\ METIS_TAC [], 369 `reachables [h'] (apply b (ch_set h)) SUBSET reachables [rr] (apply b (ch_set h))` by 370 (ASM_SIMP_TAC bool_ss [EXPAND_SUBSET,reachables_def,MEM,reachable_def,IN_DEF] 371 \\ REPEAT STRIP_TAC \\ DISJ2_TAC THENL [ 372 Q.EXISTS_TAC `[]` \\ ASM_SIMP_TAC bool_ss [PATH_def,APPEND] \\ METIS_TAC [], 373 Q.EXISTS_TAC `h'::p'` \\ ASM_SIMP_TAC bool_ss [PATH_def,APPEND] \\ METIS_TAC []]) 374 \\ METIS_TAC [SUBSET_TRANS], 375 `reachables [rr] (apply b (ch_set h)) (rr,z',h',d')` by 376 (FULL_SIMP_TAC std_ss [reachables_def,MEM,IN_DEF,reachable_def] \\ METIS_TAC []) 377 \\ FULL_SIMP_TAC bool_ss [IN_DEF,SUBSET_DEF] \\ METIS_TAC []], 378 FULL_SIMP_TAC std_ss [reachables_def,SUBSET_DEF,IN_DEF] 379 \\ FULL_SIMP_TAC bool_ss [fix_MEM] 380 \\ Q.EXISTS_TAC `r'` \\ ASM_REWRITE_TAC [] 381 \\ FULL_SIMP_TAC std_ss [reachable_def] \\ DISJ2_TAC \\ Q.EXISTS_TAC `p` 382 \\ Q.UNDISCH_TAC `PATH (r',p ++ [x]) (basic_abs m)` 383 \\ Q.UNDISCH_TAC `!x. basic_abs m x ==> apply b (ch_set h) x` 384 \\ Q.SPEC_TAC (`r'`,`rr`) \\ Induct_on `p` 385 \\ SIMP_TAC bool_ss [PATH_def,APPEND,IN_DEF] \\ METIS_TAC []]) 386 \\ ALL_TAC THENL [ 387 `FINITE (reachables r (ch_set h))` by 388 ((MATCH_MP_TAC o RW [AND_IMP_INTRO] o Q.GEN `s` o DISCH_ALL o 389 SPEC_ALL o UNDISCH o SPEC_ALL) SUBSET_FINITE 390 \\ Q.EXISTS_TAC `ch_set h` \\ FULL_SIMP_TAC bool_ss [ok_abs_def,FINITE_set] 391 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,IN_DEF] 392 \\ Cases \\ Cases_on `r'` \\ Cases_on `r''` 393 \\ FULL_SIMP_TAC std_ss [reachables_def,IN_DEF]) 394 \\ `FINITE (basic_abs m')` by METIS_TAC [FINITE_basic_abs_CUT,WFS_IMP_CUT] 395 \\ `CARD (basic_abs m') < l` by METIS_TAC [CARD_EQ_CARD_apply] 396 \\ IMP_RES_TAC WFS_IMP_WFS_part \\ IMP_RES_TAC ok_state_CARD_EQ 397 \\ `e' = (if u' then 1 + l else 1) + l` by METIS_TAC [ok_state_def] 398 \\ Cases_on `u'` \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC, 399 `?k. (f o k = I) /\ (k o f = I) /\ bijection k` by METIS_TAC [bijection_inv] 400 \\ `(k o f) 0 = 0` by (ASM_REWRITE_TAC [] \\ SIMP_TAC std_ss []) 401 \\ Q.EXISTS_TAC `b o f` \\ ASM_SIMP_TAC std_ss [bijection_bijection,GSYM apply_apply] 402 \\ REWRITE_TAC [GSYM rich_listTheory.MAP_MAP_o] 403 \\ IMP_RES_TAC MAP_INV 404 \\ IMP_RES_TAC (Q.ISPECL [`r:num list`,`f:num->num`,`g:num->num`,`s:(num#num#num#'a)set`] apply_reachables) 405 \\ ASM_SIMP_TAC std_ss [reachables_reachables,apply_apply,apply_I,SUBSET_REFL] 406 \\ `basic_abs m' = apply f (apply b (reachables r (ch_set h)))` by METIS_TAC [apply_switch] 407 \\ Q.PAT_X_ASSUM `apply b (reachables r (ch_set h)) = apply f (basic_abs m')` (K ALL_TAC) 408 \\ Q.PAT_X_ASSUM `apply f (reachables c (basic_abs m)) = basic_abs m'` (K ALL_TAC) 409 \\ ASM_SIMP_TAC std_ss [GSYM apply_apply] 410 \\ METIS_TAC [apply_SUBSET,reachables_SUBSET,SUBSET_REFL]]); 411 412val PATH_INSERT = prove( 413 ``(!y z d. ~((x:num,y:num,z:num,d:'a) IN s) /\ ~((z,x,y,d) IN s) /\ ~((y,z,x,d) IN s)) /\ ~(x = y) ==> 414 (PATH (y,p) ((x,y',z,d) INSERT s) = PATH (y,p) s)``, 415 REPEAT STRIP_TAC \\ REVERSE EQ_TAC \\ REPEAT STRIP_TAC 416 THEN1 (MATCH_MP_TAC PATH_SUBSET \\ Q.EXISTS_TAC `s` \\ ASM_SIMP_TAC bool_ss [SUBSET_DEF,IN_INSERT]) 417 \\ Q.UNDISCH_TAC `PATH (y,p) ((x,y',z,d) INSERT s)` 418 \\ Q.UNDISCH_TAC `~(x = y)` \\ Q.SPEC_TAC (`(y',z,d)`,`t`) 419 \\ Cases \\ Cases_on `r` \\ Q.SPEC_TAC (`y`,`y`) 420 \\ Induct_on `p` \\ SIMP_TAC std_ss [PATH_def,IN_INSERT,PAIR_EQ] 421 \\ REPEAT STRIP_TAC \\ `~(x = h)` by METIS_TAC [] \\ RES_TAC \\ METIS_TAC []); 422 423val reachable_INSERT = prove( 424 ``(!y z d. ~((x,y,z,d) IN s) /\ ~((z,x,y,d) IN s) /\ ~((y,z,x,d) IN s)) /\ ~(a = x) /\ ~(x = y) /\ ~(x = z) ==> 425 (reachable x ((x:num,y:num,z:num,d:'a) INSERT s) a = reachable y s a \/ reachable z s a)``, 426 ASM_SIMP_TAC bool_ss [reachable_def] 427 \\ REPEAT STRIP_TAC \\ REVERSE EQ_TAC \\ REPEAT STRIP_TAC THENL [ 428 Q.EXISTS_TAC `[]` \\ SIMP_TAC std_ss [PATH_def,APPEND,IN_INSERT] \\ METIS_TAC [], 429 Q.EXISTS_TAC `y::p` \\ SIMP_TAC std_ss [PATH_def,APPEND,IN_INSERT] 430 \\ REVERSE STRIP_TAC \\ METIS_TAC [PATH_INSERT], 431 Q.EXISTS_TAC `[]` \\ SIMP_TAC std_ss [PATH_def,APPEND,IN_INSERT] \\ METIS_TAC [], 432 Q.EXISTS_TAC `z::p` \\ SIMP_TAC std_ss [PATH_def,APPEND,IN_INSERT] 433 \\ REVERSE STRIP_TAC \\ METIS_TAC [PATH_INSERT], 434 Cases_on `p` \\ FULL_SIMP_TAC std_ss [APPEND,PATH_def,IN_INSERT] THEN1 METIS_TAC [] 435 \\ METIS_TAC [PATH_INSERT]]); 436 437val reachables_INSERT = prove( 438 ``!ts x y z d s. 439 (!y z d. ~((x,y,z,d) IN s) /\ ~((z,x,y,d) IN s) /\ ~((y,z,x,d) IN s)) /\ ~(x = y) /\ ~(x = z) ==> 440 (reachables (x::ts) ((x:num,y:num,z:num,d:'a) INSERT s) = (x,y,z,d) INSERT reachables (y::z::ts) s)``, 441 REWRITE_TAC [METIS_PROVE [PAIR] ``!f g. (f = g) = !a b c e. f (a,b,c,e) = g (a,b,c,e)``] 442 \\ SIMP_TAC std_ss [reachables_def,IN_DEF,INSERT_THM] 443 \\ REWRITE_TAC [fix_MEM] 444 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC bool_ss [] THENL [ 445 REVERSE (Cases_on `r = x`) \\ FULL_SIMP_TAC bool_ss [GSYM INSERT_THM] THENL [ 446 FULL_SIMP_TAC bool_ss [MEM] \\ DISJ2_TAC \\ Q.EXISTS_TAC `r` 447 \\ FULL_SIMP_TAC bool_ss [reachable_def] \\ DISJ2_TAC \\ Q.EXISTS_TAC `p` 448 \\ METIS_TAC [SIMP_RULE std_ss [IN_DEF] PATH_INSERT], 449 `reachable y s a \/ reachable z s a` by METIS_TAC [SIMP_RULE std_ss [IN_DEF] reachable_INSERT] 450 \\ METIS_TAC [MEM]], 451 Q.EXISTS_TAC `a` \\ SIMP_TAC bool_ss [reachable_def,MEM], 452 FULL_SIMP_TAC bool_ss [MEM,GSYM INSERT_THM] 453 THEN1 METIS_TAC [SIMP_RULE std_ss [IN_DEF] reachable_INSERT,MEM] 454 THEN1 METIS_TAC [SIMP_RULE std_ss [IN_DEF] reachable_INSERT,MEM] 455 \\ Q.EXISTS_TAC `r` \\ ASM_SIMP_TAC std_ss [] 456 \\ FULL_SIMP_TAC bool_ss [reachable_def] \\ DISJ2_TAC \\ Q.EXISTS_TAC `p` 457 \\ MATCH_MP_TAC PATH_SUBSET \\ Q.EXISTS_TAC `s` 458 \\ ASM_SIMP_TAC bool_ss [SUBSET_DEF,IN_INSERT]]); 459 460val reachables_DUP = prove( 461 ``!x y ys s. reachables (x::y::y::ys) s = reachables (x::y::ys) s``, 462 REWRITE_TAC [METIS_PROVE [PAIR] ``!f g. (f = g) = !a b c e. f (a,b,c,e) = g (a,b,c,e)``] 463 \\ SIMP_TAC std_ss [reachables_def,IN_DEF,INSERT_THM,MEM] \\ METIS_TAC []); 464 465val apply_swap_ID = prove( 466 ``(!y z d. ~(s(i,y,z,d)) /\ ~(s(z,i,y,d)) /\ ~(s(y,z,i,d)) /\ 467 ~(s(j,y,z,d)) /\ ~(s(z,j,y,d)) /\ ~(s(y,z,j,d))) ==> 468 (apply (swap i j) s = s)``, 469 REWRITE_TAC [METIS_PROVE [PAIR] ``!f g. (f = g) = !x y z d. f (x,y,z,d) = g (x,y,z,d)``] 470 \\ SIMP_TAC std_ss [apply_def,IN_DEF,swap_def] \\ REPEAT STRIP_TAC 471 \\ Cases_on `x = i` \\ Cases_on `y = i` \\ Cases_on `z = i` \\ ASM_SIMP_TAC bool_ss [] 472 \\ Cases_on `x = j` \\ Cases_on `y = j` \\ Cases_on `z = j` \\ ASM_SIMP_TAC bool_ss []); 473 474val ok_state_IMP_bounds = prove( 475 ``ok_state (i,e,c,l,u,m) /\ (m k = DATA(x,y,d)) ==> (x < i \/ (x = 0)) /\ (y < i \/ (y = 0))``, 476 FULL_SIMP_TAC std_ss [ok_state_def,LET_DEF,SUBSET0_DEF,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY] 477 \\ FULL_SIMP_TAC std_ss [IN_DEF] \\ REPEAT STRIP_TAC 478 \\ Cases_on ` RANGE (if u then 1 + l else 1,i) k` \\ RES_TAC 479 \\ FULL_SIMP_TAC bool_ss [heap_type_11,heap_type_distinct,PAIR_EQ,RANGE_def] \\ METIS_TAC []); 480 481val MAP_ID =prove( 482 ``!xs. (!k. MEM k xs ==> (f k = k)) ==> (MAP f xs = xs)``, 483 Induct \\ ASM_SIMP_TAC std_ss [MAP,MEM,CONS_11] \\ METIS_TAC []); 484 485val RANGE_BORDER = prove(``~RANGE(i,j)j``,REWRITE_TAC [RANGE_def] \\ DECIDE_TAC); 486 487val cheney_alloc_lemma = prove( 488 ``!i e t l u m x y z d k. 489 ok_state (i,e,t,l,u,m) /\ basic_abs m (x,y,z,d) /\ (!a b c. ~basic_abs m (k,a,b,c)) /\ ~(k = 0) ==> 490 ~(i = x) /\ ~(i = y) /\ ~(i = z) /\ ~(k = x) /\ ~(k = y) /\ ~(k = z)``, 491 SIMP_TAC bool_ss [ok_state_def,LET_DEF,basic_abs,SUBSET0_DEF,SUBSET_DEF,IN_INSERT] 492 \\ SIMP_TAC bool_ss [IN_DEF] \\ NTAC 12 STRIP_TAC 493 \\ `~(i = 0)` by (Cases_on `u` \\ FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC) 494 \\ `RANGE (if u then 1+l else 1,i) x` by METIS_TAC [heap_type_distinct] 495 \\ RES_TAC \\ FULL_SIMP_TAC bool_ss [heap_type_11,PAIR_EQ] 496 \\ METIS_TAC [RANGE_BORDER,heap_type_distinct]); 497 498val set_FUPDATE = prove( 499 ``!h x y d. ch_set (h |+ (fresh h,x,y,d)) = (fresh h,x,y,d) INSERT ch_set h``, 500 REWRITE_TAC [METIS_PROVE [PAIR] ``!f g. (f = g) = !a b c e. f (a,b,c,e) = g (a,b,c,e)``] 501 \\ SIMP_TAC std_ss [ch_set_def,INSERT_THM,FDOM_FUPDATE,IN_DEF,FAPPLY_FUPDATE_THM] 502 \\ METIS_TAC [PAIR_EQ,SIMP_RULE std_ss [IN_DEF,INSERT_THM] fresh_NOT_IN_FDOM]); 503 504val ok_state_LESS = prove( 505 ``!t v i e r l u m d. 506 ok_state (i,e,t::v::r,l,u,m) /\ i < e ==> 507 ok_state (i + 1,e,i::v::r,l,u,(i =+ DATA (t,v,d)) m)``, 508 SIMP_TAC std_ss [ok_state_def,LET_DEF,IN_DEF] \\ REPEAT STRIP_TAC 509 \\ FULL_SIMP_TAC bool_ss [fix_MEM] 510 THEN1 (Cases_on `u` \\ FULL_SIMP_TAC bool_ss [] \\ DECIDE_TAC) 511 THEN1 (Cases_on `u` \\ FULL_SIMP_TAC bool_ss [] \\ DECIDE_TAC) THENL [ 512 Cases_on `k = i` THEN1 (FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC) 513 \\ `RANGE ((if u then 1 + l else 1),i) k ==> RANGE ((if u then 1 + l else 1),i + 1) k` by 514 (Cases_on `u` \\ FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC) 515 \\ FULL_SIMP_TAC bool_ss [MEM] \\ METIS_TAC [], 516 `~RANGE ((if u then 1 + l else 1),i) k` by 517 (Cases_on `u` \\ FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC) 518 \\ Cases_on `i = k` \\ FULL_SIMP_TAC bool_ss [UPDATE_def,heap_type_distinct] 519 \\ Q.ABBREV_TAC `nn = if u then 1 + l else 1` 520 \\ `RANGE (nn,k + 1) k` by (REWRITE_TAC [RANGE_def] \\ DECIDE_TAC) \\ METIS_TAC [], 521 Cases_on `i = k` \\ FULL_SIMP_TAC bool_ss 522 [UPDATE_def,heap_type_11,PAIR_EQ,SUBSET0_DEF,SUBSET_DEF,INSERT_THM,IN_DEF,EMPTY_DEF,MEM] 523 \\ `!k. RANGE ((if u then 1 + l else 1),i) k ==> RANGE ((if u then 1 + l else 1),i + 1) k` by 524 (Cases_on `u` \\ FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC) THEN1 METIS_TAC [] 525 \\ `RANGE ((if u then 1 + l else 1),i) k` by 526 (Cases_on `u` \\ FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC) 527 \\ RES_TAC \\ METIS_TAC []]); 528 529val cheney_alloc_ok = store_thm("cheney_alloc_ok", 530 ``!i e t v r l u m d. 531 ok_state (i,e,t::v::r,l,u,m) ==> ok_state (cheney_alloc (i,e,t::v::r,l,u,m) (d:'a))``, 532 REWRITE_TAC [cheney_alloc_def,cheney_alloc_gc_def] \\ REPEAT STRIP_TAC 533 \\ Cases_on `i < e` \\ ASM_SIMP_TAC bool_ss [cheney_alloc_aux_def] THEN1 534 (ASM_SIMP_TAC std_ss [LET_DEF,DECIDE ``n<m ==> ~(n=m:num)``,HD,TL] \\ METIS_TAC [ok_state_LESS]) 535 \\ `?i2 e2 root2 l2 u2 m2. cheney_collector (i,e,t::v::r,l,u,m) = (i2,e2,root2,l2,u2,m2)` by METIS_TAC [PAIR] 536 \\ ASM_SIMP_TAC bool_ss [cheney_alloc_aux_def] 537 \\ IMP_RES_TAC cheney_collector_spec 538 \\ Cases_on `i2 = e2` \\ ASM_SIMP_TAC std_ss [LET_DEF] THEN1 539 (Q.PAT_X_ASSUM `ok_state (i2,e2,root2,l2,u2,m2)` MP_TAC 540 \\ Cases_on `root2` 541 \\ FULL_SIMP_TAC std_ss [MAP,NOT_CONS_NIL,TL] 542 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 543 \\ SIMP_TAC std_ss [ok_state_def,LET_DEF] 544 \\ REPEAT STRIP_TAC 545 \\ FULL_SIMP_TAC std_ss [MEM] 546 \\ METIS_TAC []) 547 \\ `FST (SND (SND (cheney_collector (i,e,t::v::r,l,u,m)))) = root2` by METIS_TAC [PAIR_EQ,PAIR] 548 \\ Q.PAT_X_ASSUM `FST (SND xx) = yy` (ASSUME_TAC o RW [FST,SND] o 549 CONV_RULE (DEPTH_CONV FORCE_PBETA_CONV) o 550 SIMP_RULE std_ss [LET_DEF,move_roots_def,cheney_collector_def]) 551 \\ Cases_on `root2` \\ FULL_SIMP_TAC std_ss [NOT_CONS_NIL] 552 \\ Cases_on `t'` \\ FULL_SIMP_TAC std_ss [NOT_CONS_NIL,CONS_11] 553 \\ FULL_SIMP_TAC std_ss [HD,TL] \\ MATCH_MP_TAC ok_state_LESS \\ ASM_SIMP_TAC bool_ss [] 554 \\ Cases_on `u2` \\ FULL_SIMP_TAC bool_ss [ok_state_def,LET_DEF] \\ DECIDE_TAC); 555 556val cheney_alloc_spec = store_thm("cheney_alloc_spec", 557 ``(cheney_alloc s (d:'a) = s') ==> 558 ch_inv (t1::t2::ts,h,l) s /\ CARD (reachables (t1::t2::ts) (ch_set h)) < l ==> 559 ch_inv (fresh h::t2::ts, h |+ (fresh h,t1,t2,d),l) s'``, 560 `?i e root a l u m. s = (i,e,root,l,u,m)` by METIS_TAC [PAIR] 561 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ ASM_SIMP_TAC bool_ss [] 562 \\ STRIP_TAC \\ REPEAT (POP_ASSUM (K ALL_TAC)) 563 \\ ASM_SIMP_TAC bool_ss [cheney_alloc_def] 564 \\ Cases_on `~(l' = l)` THEN1 METIS_TAC [ch_inv_def] 565 \\ FULL_SIMP_TAC bool_ss [] \\ POP_ASSUM (K ALL_TAC) 566 \\ `?i' e' c' l' u' m'. (cheney_alloc_gc (i,e,root,l,u,m) = (i',e',c',l',u',m'))` by METIS_TAC [PAIR] 567 \\ ASM_SIMP_TAC std_ss [LET_DEF,cheney_alloc_aux_def] \\ REPEAT STRIP_TAC 568 \\ IMP_RES_TAC cheney_alloc_gc_spec 569 \\ FULL_SIMP_TAC std_ss [ch_inv_thm,ok_abs_def,FINITE_INSERT,DECIDE ``i<e==>~(i=e:num)``] 570 \\ STRIP_TAC THEN1 571 (Cases_on `c'` \\ FULL_SIMP_TAC bool_ss [MAP,NOT_CONS_NIL,TL,MEM] 572 \\ Cases_on `t` \\ FULL_SIMP_TAC bool_ss [MAP,NOT_CONS_NIL,TL,MEM,CONS_11,HD,TL] 573 \\ METIS_TAC [ok_state_LESS]) 574 \\ STRIP_TAC THEN1 575 (FULL_SIMP_TAC bool_ss [IN_INSERT,FDOM_FUPDATE,fresh_NOT_IN_FDOM,MEM,FEVERY_FUPDATE,PAIR_EQ] 576 \\ REVERSE STRIP_TAC THEN1 METIS_TAC [] 577 \\ SIMP_TAC std_ss [fresh_NOT_IN_FDOM,NOT_FDOM_DRESTRICT] \\ STRIP_TAC 578 THEN1 (FULL_SIMP_TAC std_ss [SUBSET0_DEF,SUBSET_DEF,IN_DEF,INSERT_THM,EMPTY_DEF] \\ METIS_TAC []) 579 \\ MATCH_MP_TAC (METIS_PROVE [FEVERY_DEF] ``!P Q h. (!x. P x ==> Q x) /\ FEVERY P h ==> FEVERY Q h``) 580 \\ Q.EXISTS_TAC `(\(x,y,z,d). {y; z} SUBSET0 FDOM h)` \\ ASM_SIMP_TAC bool_ss [] 581 \\ Cases \\ Cases_on `r` \\ Cases_on `r'` 582 \\ FULL_SIMP_TAC std_ss [SUBSET0_DEF,SUBSET_DEF,IN_DEF,INSERT_THM,EMPTY_DEF] \\ METIS_TAC []) 583 \\ `?k. (b' o k = I) /\ (k o b' = I) /\ bijection k` by METIS_TAC [bijection_inv] 584 \\ Q.EXISTS_TAC `b' o swap i' (k (fresh h))` 585 \\ ASM_SIMP_TAC std_ss [GSYM apply_apply,bijection_bijection,bijection_swap] 586 \\ `!x. b' (k x) = x` by FULL_SIMP_TAC std_ss [FUN_EQ_THM] 587 \\ ASM_SIMP_TAC bool_ss [METIS_PROVE [swap_def] ``!i k. swap i k i = k``] 588 \\ Cases_on `c'` \\ FULL_SIMP_TAC bool_ss [MAP,NOT_CONS_NIL,TL,MEM,HD,CONS_11] 589 \\ IMP_RES_TAC fresh_THM 590 \\ Cases_on `k (fresh h) = 0` THEN1 METIS_TAC [] 591 \\ `~(i' = 0)` by (Cases_on `u'` \\ 592 FULL_SIMP_TAC bool_ss [RANGE_def,ok_state_def,IN_DEF,LET_DEF] \\ DECIDE_TAC) 593 \\ STRIP_TAC THEN1 ASM_SIMP_TAC std_ss [swap_def] 594 \\ SIMP_TAC std_ss [GSYM CONJ_ASSOC,GSYM rich_listTheory.MAP_MAP_o] 595 \\ STRIP_TAC THEN1 ASM_SIMP_TAC std_ss [swap_def] 596 \\ `(MAP b' (MAP (swap i' (k (fresh h))) t) = t2::ts)` by 597 (Q.PAT_X_ASSUM `MAP b' t = t2::ts` (ASSUME_TAC o GSYM) 598 \\ ASM_SIMP_TAC bool_ss [] 599 \\ MATCH_MP_TAC (METIS_PROVE [] ``(x = y) ==> (f x = f y)``) 600 \\ MATCH_MP_TAC MAP_ID 601 \\ REPEAT STRIP_TAC 602 \\ FULL_SIMP_TAC std_ss [ok_state_def,LET_DEF,IN_DEF,RANGE_def,MEM] 603 \\ Cases_on `k' = 0` \\ ASM_SIMP_TAC std_ss [swap_def] 604 \\ `~(k' = i')` by METIS_TAC [DECIDE ``m<n:num ==> ~(m=n)``] 605 \\ Cases_on `k' = k (fresh h)` \\ ASM_SIMP_TAC bool_ss [] 606 \\ `?x y d. (m' k' = DATA (x,y,d))` by METIS_TAC [] 607 \\ `basic_abs m' (k (fresh h),x,y,d)` by (SIMP_TAC bool_ss [basic_abs] \\ METIS_TAC []) 608 \\ `apply b' (ch_set h) (k (fresh h),x,y,d)` by (FULL_SIMP_TAC std_ss [SUBSET_DEF,IN_DEF] \\ METIS_TAC []) 609 \\ FULL_SIMP_TAC std_ss [apply_def,IN_DEF,FUN_EQ_THM,ch_set_def] 610 \\ METIS_TAC [SIMP_RULE std_ss [IN_DEF] fresh_NOT_IN_FDOM]) 611 \\ ASM_SIMP_TAC bool_ss [] 612 \\ `m' i' = EMP` by 613 (FULL_SIMP_TAC bool_ss [ok_state_def,LET_DEF,RANGE_def,IN_DEF] 614 \\ METIS_TAC [DECIDE ``~(n<n:num)``]) 615 \\`(basic_abs ((i' =+ DATA (h',HD t,d)) m') = (i',h',HD t,d) INSERT basic_abs m') /\ 616 !x y z. ~((i',x,y,z) IN basic_abs m')` by 617 (REWRITE_TAC [METIS_PROVE [PAIR] ``!f g. (f = g) = !x y z d. f (x,y,z,d) = g (x,y,z,d)``] 618 \\ ASM_SIMP_TAC std_ss [INSERT_THM,basic_abs,IN_DEF,UPDATE_def,heap_type_distinct] 619 \\ REPEAT STRIP_TAC \\ Cases_on `x = i'` 620 \\ FULL_SIMP_TAC std_ss [heap_type_distinct,heap_type_11]) 621 \\ REWRITE_TAC [set_FUPDATE] 622 \\ ASM_SIMP_TAC bool_ss [] 623 \\ Q.ABBREV_TAC `mm = basic_abs m'` 624 \\ Q.ABBREV_TAC `f = fresh h` 625 \\ `reachables (f::t2::ts) ((f,t1,t2,d) INSERT ch_set h) = 626 (f,t1,t2,d) INSERT reachables (t1::t2::ts) (ch_set h)` by 627 (MATCH_MP_TAC (RW [reachables_DUP] (Q.SPECL [`z::ys`,`x`,`y`,`z`] reachables_INSERT)) 628 \\ METIS_TAC [fresh_NOT_IN_FDOM]) 629 \\ ASM_SIMP_TAC bool_ss [] 630 \\ Cases_on `t` \\ FULL_SIMP_TAC bool_ss [MAP,NOT_CONS_NIL,TL,MEM,HD,CONS_11] 631 \\ `reachables (i'::h''::t') ((i',h',h'',d) INSERT mm) = 632 (i',h',h'',d) INSERT reachables (h'::h''::t') mm` by 633 (MATCH_MP_TAC (RW [reachables_DUP] (Q.SPECL [`z::ys`,`x`,`y`,`z`] reachables_INSERT)) 634 \\ Q.UNABBREV_TAC `mm` 635 \\ FULL_SIMP_TAC bool_ss [IN_DEF,basic_abs,ok_state_def,LET_DEF] 636 \\ `~((if u' then 1 + l' else 1) <= 0)` by (Cases_on `u'` \\ REWRITE_TAC [] \\ DECIDE_TAC) 637 \\ REPEAT STRIP_TAC THENL [ 638 Cases_on `RANGE (if u' then 1+l' else 1,i') z` \\ RES_TAC 639 \\ FULL_SIMP_TAC std_ss [heap_type_11,SUBSET0_DEF,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY] 640 \\ FULL_SIMP_TAC bool_ss [RANGE_def,IN_DEF] \\ METIS_TAC [DECIDE ``~(i<i:num)``], 641 Cases_on `RANGE (if u' then 1+l' else 1,i') y` \\ RES_TAC 642 \\ FULL_SIMP_TAC std_ss [heap_type_11,SUBSET0_DEF,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY] 643 \\ FULL_SIMP_TAC bool_ss [RANGE_def,IN_DEF] \\ METIS_TAC [DECIDE ``~(i<i:num)``], 644 `~(b' h' = 0)` by METIS_TAC [bijection_def,ONE_ONE_DEF] 645 \\ FULL_SIMP_TAC bool_ss [fix_MEM, MEM] 646 \\ METIS_TAC [RANGE_BORDER], 647 `~(b' h'' = 0)` by METIS_TAC [bijection_def,ONE_ONE_DEF] 648 \\ FULL_SIMP_TAC bool_ss [MEM, fix_MEM] \\ METIS_TAC [RANGE_BORDER]]) 649 \\ ASM_SIMP_TAC bool_ss [] 650 \\ `(k 0 = 0)` by (FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ METIS_TAC []) 651 \\ Q.UNABBREV_TAC `f` 652 \\ `swap i' (k (fresh h)) o swap i' (k (fresh h)) = I` by METIS_TAC [swap_swap] 653 \\ (ASSUME_TAC o UNDISCH_ALL o Q.SPECL [`k`,`b'`]) apply_INSERT 654 \\ (ASSUME_TAC o UNDISCH_ALL o Q.SPECL [`swap i' (k (fresh h))`,`swap i' (k (fresh h))`]) apply_INSERT 655 \\ ASM_SIMP_TAC std_ss [] 656 \\ `swap i' (k (fresh h)) (k (fresh h)) = i'` by SIMP_TAC bool_ss [swap_def] 657 \\ ASM_SIMP_TAC std_ss [] 658 \\ `(k t1 = h') /\ (k t2 = h'')` by METIS_TAC [bijection_def,ONE_ONE_DEF] 659 \\ `~(i' = h') /\ ~(i' = h'')` by 660 (REPEAT STRIP_TAC \\ FULL_SIMP_TAC bool_ss [IN_DEF,basic_abs,ok_state_def,LET_DEF,MEM] 661 \\ METIS_TAC [RANGE_BORDER]) 662 \\ `~(k (fresh h) = h')` by 663 (STRIP_TAC \\ `fresh h = t1` by METIS_TAC [bijection_def,ONE_ONE_DEF] \\ METIS_TAC [fresh_NOT_IN_FDOM]) 664 \\ `~(k (fresh h) = h'')` by 665 (STRIP_TAC \\ `fresh h = t2` by METIS_TAC [bijection_def,ONE_ONE_DEF] \\ METIS_TAC [fresh_NOT_IN_FDOM]) 666 \\ `swap i' (k (fresh h)) h' = h'` by FULL_SIMP_TAC bool_ss [swap_def] 667 \\ `swap i' (k (fresh h)) h'' = h''` by FULL_SIMP_TAC bool_ss [swap_def] 668 \\ ASM_SIMP_TAC bool_ss [] 669 \\ SIMP_TAC std_ss [EXPAND_SUBSET,INSERT_THM] \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC bool_ss [] 670 \\ Q.UNABBREV_TAC `mm` \\ DISJ2_TAC THEN1 671 (ONCE_REWRITE_TAC [apply_def] 672 \\ FULL_SIMP_TAC bool_ss [basic_abs,ok_state_def,LET_DEF] 673 \\ `~(i' = x)` by (REPEAT STRIP_TAC \\ FULL_SIMP_TAC bool_ss [IN_DEF,basic_abs,LET_DEF,MEM] 674 \\ METIS_TAC [RANGE_BORDER]) 675 \\ `x IN RANGE (if u' then 1+l' else 1,i')` by METIS_TAC [heap_type_distinct] 676 \\ `?x' y d. (m' x = DATA (x',y,d)) /\ {x'; y} SUBSET0 RANGE (if u' then 1+l' else 1,i')` by METIS_TAC [] 677 \\ FULL_SIMP_TAC std_ss [heap_type_11,SUBSET0_DEF,SUBSET_DEF,IN_INSERT] 678 \\ FULL_SIMP_TAC std_ss [IN_DEF] \\ `~(y = i') /\ ~(z = i')` by METIS_TAC [RANGE_BORDER] 679 \\ `~(x = k (fresh h)) /\ ~(y = k (fresh h)) /\ ~(z = k (fresh h))` suffices_by 680 (STRIP_TAC THEN ASM_SIMP_TAC std_ss [swap_def] \\ METIS_TAC [basic_abs]) 681 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC bool_ss [] 682 \\ `RANGE (if u' then 1+l' else 1,i') (k (fresh h))` by METIS_TAC [] 683 \\ `?j1 j2 j3. basic_abs m' (k (fresh h),j1,j2,j3)` by METIS_TAC [basic_abs] 684 \\ `apply b' (ch_set h) (k (fresh h),j1,j2,j3)` by METIS_TAC [] 685 \\ FULL_SIMP_TAC bool_ss [apply_def,IN_DEF] \\ METIS_TAC []) 686 \\ Q.PAT_X_ASSUM `xxx SUBSET basic_abs m'` 687 (fn th => MATCH_MP_TAC (RW [EXPAND_SUBSET] th) \\ ASSUME_TAC th) 688 \\ Q.ABBREV_TAC `xxx = apply b' (reachables (t1::t2::ts) (ch_set h))` 689 \\ Q.PAT_X_ASSUM `apply (swap i' (k (fresh h))) xxx (x,y,z,d')` 690 (ASSUME_TAC o SIMP_RULE std_ss [apply_def,IN_DEF]) 691 \\ FULL_SIMP_TAC bool_ss [EXPAND_SUBSET] 692 \\ `basic_abs m' (swap i' (k (fresh h)) x,swap i' (k (fresh h)) y, 693 swap i' (k (fresh h)) z,d')` by METIS_TAC [] 694 \\ Q.ABBREV_TAC `ff = (fresh h)` 695 \\ `(!a5 b5 c5. ~basic_abs m' (k ff,a5,b5,c5))` by 696 (REPEAT STRIP_TAC \\ `apply b' (ch_set h) (k ff,a5,b5,c5)` by METIS_TAC [] 697 \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM,apply_def] \\ METIS_TAC [apply_def]) 698 \\ Q.ABBREV_TAC `sx = swap i' (k ff) x` 699 \\ Q.ABBREV_TAC `sy = swap i' (k ff) y` 700 \\ Q.ABBREV_TAC `sz = swap i' (k ff) z` 701 \\ `~(i' = sx) /\ ~(i' = sy) /\ ~(i' = sz) /\ ~(k ff = sx) /\ ~(k ff = sy) /\ ~(k ff = sz)` by 702 (MATCH_MP_TAC cheney_alloc_lemma \\ Q.EXISTS_TAC `e'` 703 \\ Q.EXISTS_TAC `h'::h''::t'` \\ Q.EXISTS_TAC `l'` \\ Q.EXISTS_TAC `u'` 704 \\ Q.EXISTS_TAC `m'` \\ Q.EXISTS_TAC `d'` \\ ASM_SIMP_TAC bool_ss []) 705 \\ Q.UNABBREV_TAC `sx` \\ Q.UNABBREV_TAC `sy` \\ Q.UNABBREV_TAC `sz` 706 \\ FULL_SIMP_TAC bool_ss [swap_def] 707 \\ Cases_on `x = i'` \\ FULL_SIMP_TAC bool_ss [] 708 \\ Cases_on `y = i'` \\ FULL_SIMP_TAC bool_ss [] 709 \\ Cases_on `z = i'` \\ FULL_SIMP_TAC bool_ss [] 710 \\ Cases_on `x = k ff` \\ FULL_SIMP_TAC bool_ss [] 711 \\ Cases_on `y = k ff` \\ FULL_SIMP_TAC bool_ss [] 712 \\ Cases_on `z = k ff` \\ FULL_SIMP_TAC bool_ss [] 713 \\ METIS_TAC []); 714 715val cheney_init = store_thm("cheney_init", 716 ``!xs l. ch_inv (MAP (\x.0) xs,FEMPTY,l) (1,1+l,MAP (\x.0) (xs:num list),l,F,\x.EMP)``, 717 SIMP_TAC bool_ss [ch_inv_thm,ok_state_def,ok_abs_def,FEVERY_FEMPTY,FDOM_FEMPTY, 718 LESS_EQ_REFL,LET_DEF,FINITE_EMPTY,MEM_MAP,heap_type_distinct,NOT_IN_EMPTY, 719 RANGE_lemmas,DECIDE ``1<=1+l:num``] 720 \\ REVERSE (REPEAT STRIP_TAC) THEN1 721 (Q.EXISTS_TAC `I` \\ SIMP_TAC std_ss [rich_listTheory.MAP_MAP_o,apply_I, 722 bijection_def,ONTO_DEF,EXPAND_SUBSET,reachables_def,EMPTY_DEF,IN_DEF, 723 basic_abs,heap_type_distinct,ONE_ONE_DEF,ch_set_def,FDOM_FEMPTY]) 724 \\ METIS_TAC []); 725 726(* add to library? *) 727 728val MEM_TAKE = prove( 729 ``!xs n x. MEM x (TAKE n xs) ==> MEM x xs``, 730 Induct THEN REWRITE_TAC [TAKE_def] THEN METIS_TAC [MEM]); 731 732val MEM_DROP = prove( 733 ``!xs n x. MEM x (DROP n xs) ==> MEM x xs``, 734 Induct THEN REWRITE_TAC [DROP_def] THEN METIS_TAC [MEM]); 735 736val MAP_DROP = prove( 737 ``!xs f n. MAP f (DROP n xs) = DROP n (MAP f xs)``, 738 Induct THEN REWRITE_TAC [DROP_def,MAP,CONS_11] THEN METIS_TAC [MAP]); 739 740val MAP_TAKE = prove( 741 ``!xs f n. MAP f (TAKE n xs) = TAKE n (MAP f xs)``, 742 Induct THEN REWRITE_TAC [TAKE_def,MAP,CONS_11] THEN METIS_TAC [MAP]); 743 744(* /add *) 745 746val LIST_DELETE_def = Define ` 747 LIST_DELETE n xs = TAKE n xs ++ DROP (SUC n) xs`; 748 749val LIST_INSERT_def = Define ` 750 LIST_INSERT y n xs = TAKE n xs ++ [y] ++ DROP n xs`; 751 752val LIST_UPDATE_def = Define ` 753 LIST_UPDATE n y xs = LIST_DELETE n (LIST_INSERT y (SUC n) xs)`; 754 755val MEM_LIST_DELETE = prove( 756 ``!xs n x. MEM x (LIST_DELETE n xs) ==> MEM x xs``, 757 METIS_TAC [LIST_DELETE_def,MEM_APPEND,MEM_DROP,MEM_TAKE]); 758 759val MEM_LIST_INSERT = prove( 760 ``!xs n x. MEM x (LIST_INSERT y n xs) ==> MEM x (y::xs)``, 761 METIS_TAC [LIST_INSERT_def,MEM_APPEND,MEM,MEM_DROP,MEM_TAKE]); 762 763val MAP_LIST_DELETE = prove( 764 ``!xs n f. MAP f (LIST_DELETE n xs) = LIST_DELETE n (MAP f xs)``, 765 REWRITE_TAC [LIST_DELETE_def,MAP_DROP,MAP_TAKE,MAP_APPEND]); 766 767val MAP_LIST_INSERT = prove( 768 ``!xs n f. MAP f (LIST_INSERT y n xs) = LIST_INSERT (f y) n (MAP f xs)``, 769 REWRITE_TAC [LIST_INSERT_def,MAP_DROP,MAP_TAKE,MAP_APPEND,MAP]); 770 771val cheney_DELETE = prove( 772 ``!n xs ys. ch_inv (xs,h,l) (i,e,ys,l,u,m) ==> 773 ch_inv (LIST_DELETE n xs,h,l) (i,e,LIST_DELETE n ys,l,u,m)``, 774 SIMP_TAC bool_ss [ch_inv_thm,ok_abs_def,ok_state_def,LET_DEF,MEM,MAP,CONS_11] 775 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC bool_ss [] \\ IMP_RES_TAC MEM_LIST_DELETE 776 THEN1 METIS_TAC [] THEN1 METIS_TAC [] 777 \\ Q.EXISTS_TAC `b` \\ ASM_SIMP_TAC bool_ss [MAP_LIST_DELETE] 778 \\ MATCH_MP_TAC SUBSET_TRANS \\ Q.EXISTS_TAC `apply b (reachables xs (ch_set h))` 779 \\ ASM_SIMP_TAC bool_ss [] \\ FULL_SIMP_TAC bool_ss [EXPAND_SUBSET] 780 \\ FULL_SIMP_TAC bool_ss [apply_def,reachables_def,IN_DEF,MEM,MAP] 781 \\ FULL_SIMP_TAC bool_ss [fix_MEM] 782 \\ METIS_TAC [MEM_LIST_DELETE]); 783 784val cheney_INSERT = prove( 785 ``!n x xs y ys. ch_inv (x::xs,h,l) (i,e,y::ys,l,u,m) ==> 786 ch_inv (LIST_INSERT x n xs,h,l) (i,e,LIST_INSERT y n ys,l,u,m)``, 787 SIMP_TAC bool_ss [ch_inv_thm,ok_abs_def,ok_state_def,LET_DEF,MEM] 788 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC bool_ss [] \\ IMP_RES_TAC MEM_LIST_INSERT 789 THEN1 METIS_TAC [MEM] THEN1 METIS_TAC [MEM] 790 \\ Q.EXISTS_TAC `b` \\ FULL_SIMP_TAC bool_ss [MAP_LIST_INSERT,MAP,CONS_11] 791 \\ MATCH_MP_TAC SUBSET_TRANS \\ Q.EXISTS_TAC `apply b (reachables (x::xs) (ch_set h))` 792 \\ ASM_SIMP_TAC bool_ss [] \\ FULL_SIMP_TAC bool_ss [EXPAND_SUBSET] 793 \\ FULL_SIMP_TAC bool_ss [apply_def,reachables_def,IN_DEF,MEM,MAP] 794 \\ FULL_SIMP_TAC bool_ss [fix_MEM] 795 \\ METIS_TAC [MEM_LIST_INSERT,MEM]); 796 797val cheney_UPDATE = prove( 798 ``!n x xs y ys. ch_inv (x::xs,h,l) (i,e,y::ys,l,u,m) ==> 799 ch_inv (LIST_UPDATE n x xs,h,l) (i,e,LIST_UPDATE n y ys,l,u,m)``, 800 REPEAT STRIP_TAC \\ REWRITE_TAC [LIST_UPDATE_def] 801 \\ MATCH_MP_TAC cheney_DELETE \\ MATCH_MP_TAC cheney_INSERT \\ ASM_REWRITE_TAC []); 802 803val cheney_0 = store_thm("cheney_0", 804 ``!xs ys n h l i e u m. 805 ch_inv (xs,h,l) (i,e,ys,l,u,m) ==> 806 ch_inv (LIST_UPDATE n 0 xs,h,l) (i,e,LIST_UPDATE n 0 ys,l,u,m)``, 807 REPEAT STRIP_TAC \\ MATCH_MP_TAC cheney_UPDATE 808 \\ FULL_SIMP_TAC bool_ss [ch_inv_thm,ok_abs_def,ok_state_def,LET_DEF,MEM] 809 \\ REPEAT STRIP_TAC THEN1 METIS_TAC [] THEN1 METIS_TAC [] 810 \\ Q.EXISTS_TAC `b` \\ ASM_SIMP_TAC bool_ss [MAP] 811 \\ MATCH_MP_TAC SUBSET_TRANS \\ Q.EXISTS_TAC `apply b (reachables xs (ch_set h))` 812 \\ ASM_SIMP_TAC bool_ss [] \\ MATCH_MP_TAC apply_SUBSET 813 \\ SIMP_TAC std_ss [reachables_def,EXPAND_SUBSET,MEM] \\ REVERSE (REPEAT STRIP_TAC) 814 THEN1 METIS_TAC [] 815 \\ Q.UNDISCH_TAC `x IN reachable r (ch_set h)` \\ ASM_SIMP_TAC std_ss [reachable_def,IN_DEF] 816 \\ REPEAT STRIP_TAC THEN1 FULL_SIMP_TAC std_ss [IN_DEF,ch_set_def] 817 \\ Cases_on `p` \\ FULL_SIMP_TAC bool_ss [APPEND,PATH_def,IN_DEF,ch_set_def] \\ METIS_TAC []); 818 819val MAP_MEM_ZIP = prove( 820 ``!xs ys b x y. (MAP b ys = xs) /\ MEM (x,y) (ZIP (xs,ys)) ==> MEM x xs /\ MEM y ys /\ (b y = x)``, 821 Induct THENL [ALL_TAC,STRIP_TAC] 822 \\ Cases \\ REWRITE_TAC [MAP,MEM,ZIP,NOT_CONS_NIL,NOT_NIL_CONS,CONS_11] 823 \\ METIS_TAC [PAIR_EQ]); 824 825val reachable_expand = prove( 826 ``!x y s t. reachable y s t /\ (?z d. s (x,y,z,d) \/ s (x,z,y,d)) ==> reachable x s t``, 827 SIMP_TAC bool_ss [reachable_def] \\ REPEAT STRIP_TAC \\ DISJ2_TAC 828 THENL [Q.EXISTS_TAC `[]`,Q.EXISTS_TAC `[]`,Q.EXISTS_TAC `y::p`,Q.EXISTS_TAC `y::p`] 829 \\ ASM_SIMP_TAC std_ss [PATH_def,APPEND,IN_DEF] \\ METIS_TAC []); 830 831val cheney_move = store_thm("cheney_move", 832 ``!xs ys x y h l i e u m. 833 ch_inv (xs,h,l) (i,e,ys,l,u,m) /\ MEM (x,y) (ZIP (xs,ys)) ==> 834 ch_inv (LIST_UPDATE n x xs,h,l) (i,e,LIST_UPDATE n y ys,l,u,m)``, 835 REPEAT STRIP_TAC \\ MATCH_MP_TAC cheney_UPDATE 836 \\ FULL_SIMP_TAC bool_ss [ch_inv_thm,ok_abs_def,ok_state_def,LET_DEF,MEM,MAP,CONS_11] 837 \\ IMP_RES_TAC MAP_MEM_ZIP \\ REPEAT STRIP_TAC 838 THEN1 METIS_TAC [] THEN1 METIS_TAC [] THEN1 METIS_TAC [] THEN1 METIS_TAC [] 839 \\ Q.EXISTS_TAC `b` \\ ASM_SIMP_TAC std_ss [] 840 \\ sg `reachables (x::xs) (ch_set h) = reachables xs (ch_set h)` 841 \\ ASM_SIMP_TAC std_ss [] 842 \\ MATCH_MP_TAC (METIS_PROVE [PAIR] ``(!x y z q. f (x,y,z,q) = g (x,y,z,q)) ==> (f = g)``) 843 \\ SIMP_TAC bool_ss [reachables_def,MEM] \\ METIS_TAC []); 844 845val CONS_LIST_UPDATE = prove( 846 ``!n x y xs. x::LIST_UPDATE n y xs = LIST_UPDATE (SUC n) y (x::xs)``, 847 REWRITE_TAC [LIST_UPDATE_def,LIST_DELETE_def,LIST_INSERT_def,rich_listTheory.BUTFIRSTN, 848 rich_listTheory.FIRSTN,APPEND]); 849 850val cheney_move2 = store_thm("cheney_move2", 851 ``!xs ys x1 y1 n1 x2 y2 n2 h l i e u m. 852 ch_inv (xs,h,l) (i,e,ys,l,u,m) /\ MEM (x1,y1) (ZIP (xs,ys)) /\ MEM (x2,y2) (ZIP (xs,ys)) ==> 853 ch_inv (LIST_UPDATE n1 x1 (LIST_UPDATE n2 x2 xs),h,l) 854 (i,e,LIST_UPDATE n1 y1 (LIST_UPDATE n2 y2 ys),l,u,m)``, 855 REPEAT STRIP_TAC \\ MATCH_MP_TAC cheney_UPDATE 856 \\ REWRITE_TAC [CONS_LIST_UPDATE] \\ MATCH_MP_TAC cheney_UPDATE 857 \\ FULL_SIMP_TAC bool_ss [ch_inv_thm,ok_abs_def,ok_state_def,LET_DEF,MEM,MAP,CONS_11] 858 \\ IMP_RES_TAC MAP_MEM_ZIP \\ REPEAT STRIP_TAC 859 THEN1 METIS_TAC [] THEN1 METIS_TAC [] THEN1 METIS_TAC [] THEN1 METIS_TAC [] 860 THEN1 METIS_TAC [] THEN1 METIS_TAC [] 861 \\ Q.EXISTS_TAC `b` \\ ASM_SIMP_TAC std_ss [] 862 \\ sg `reachables (x2::x1::xs) (ch_set h) = reachables xs (ch_set h)` 863 \\ ASM_SIMP_TAC std_ss [] 864 \\ MATCH_MP_TAC (METIS_PROVE [PAIR] ``(!x y z q. f (x,y,z,q) = g (x,y,z,q)) ==> (f = g)``) 865 \\ SIMP_TAC bool_ss [reachables_def,MEM] \\ METIS_TAC []); 866 867val cheney_car_cdr = store_thm("cheney_car_cdr", 868 ``!xs ys x y h l i e u m. 869 ch_inv (xs,h,l) (i,e,ys,l,u,m) /\ MEM (x,y) (ZIP (xs,ys)) /\ ~(y = 0) ==> 870 ch_inv (LIST_UPDATE n (FST (h ' x)) xs,h,l) (i,e,LIST_UPDATE n (FST (getDATA (m y))) ys,l,u,m) /\ 871 ch_inv (LIST_UPDATE n (FST (SND (h ' x))) xs,h,l) (i,e,LIST_UPDATE n (FST (SND (getDATA (m y)))) ys,l,u,m)``, 872 REPEAT STRIP_TAC \\ MATCH_MP_TAC cheney_UPDATE 873 \\ FULL_SIMP_TAC bool_ss [ch_inv_thm,ok_abs_def,ok_state_def,LET_DEF,MEM,MAP,CONS_11] 874 \\ IMP_RES_TAC MAP_MEM_ZIP 875 \\ `y IN RANGE ((if u then 1 + l else 1),i)` by METIS_TAC [] 876 \\ `?x3 y3 d. (m y = DATA (x3,y3,d)) /\ {x3; y3} SUBSET0 RANGE ((if u then 1 + l else 1),i)` 877 by METIS_TAC [] 878 \\ Q.PAT_X_ASSUM `!k. ppp ==> ?x. bbb` (K ALL_TAC) 879 \\ FULL_SIMP_TAC bool_ss [getDATA_def,FST,SND,FEVERY_DEF] 880 \\ (STRIP_TAC THEN1 (FULL_SIMP_TAC std_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY] \\ METIS_TAC [])) 881 \\ `~(x = 0)` by METIS_TAC [bijection_def,ONE_ONE_DEF] 882 \\ `(\(x,y,z,d). {y; z} SUBSET0 FDOM h) (x,h ' x)` by METIS_TAC [] 883 \\ `?a1 b1 c1. h ' x = (a1,b1,c1)` by METIS_TAC [PAIR] 884 \\ FULL_SIMP_TAC std_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT] 885 \\ (STRIP_TAC THEN1 METIS_TAC []) 886 \\ Q.EXISTS_TAC `b` \\ ASM_SIMP_TAC bool_ss [] 887 \\ FULL_SIMP_TAC std_ss [IN_DEF] 888 \\ `basic_abs m (y,x3,y3,d)` by FULL_SIMP_TAC bool_ss [basic_abs] 889 \\ `apply b (ch_set h) (y,x3,y3,d)` by METIS_TAC [] 890 \\ Q.PAT_X_ASSUM `b y = x` ASSUME_TAC 891 \\ FULL_SIMP_TAC std_ss [apply_def,ch_set_def,IN_DEF] 892 \\ REPEAT STRIP_TAC 893 \\ Q.PAT_X_ASSUM ` !x. apply b (reachables xs (ch_set h)) x ==> basic_abs m x` MATCH_MP_TAC 894 \\ Cases_on `x'` \\ Cases_on `r` \\ Cases_on `r'` 895 \\ (REVERSE (FULL_SIMP_TAC std_ss [apply_def,IN_DEF,reachables_def,MEM]) THEN1 METIS_TAC []) 896 \\ Q.EXISTS_TAC `x` \\ ASM_SIMP_TAC bool_ss [] 897 \\ MATCH_MP_TAC reachable_expand 898 \\ Q.EXISTS_TAC `r'` \\ ASM_SIMP_TAC bool_ss [ch_set_def,IN_DEF,PAIR_EQ] \\ METIS_TAC []); 899 900val cheney_data = store_thm("cheney_data", 901 ``ch_inv (xs,h,l) (i,e,ys,l,u,m) /\ MEM (x,y) (ZIP (xs,ys)) /\ ~(y = 0) ==> 902 (SND (SND (h ' x)) = SND (SND (getDATA (m y))))``, 903 REPEAT STRIP_TAC 904 \\ FULL_SIMP_TAC bool_ss [ch_inv_thm,ok_abs_def,ok_state_def,LET_DEF,MEM,MAP,CONS_11] 905 \\ IMP_RES_TAC MAP_MEM_ZIP 906 \\ `y IN RANGE ((if u then 1 + l else 1),i)` by METIS_TAC [] 907 \\ `?x3 y3 d. (m y = DATA (x3,y3,d)) /\ {x3; y3} SUBSET0 RANGE ((if u then 1 + l else 1),i)` 908 by METIS_TAC [] 909 \\ Q.PAT_X_ASSUM `!k. ppp ==> ?x. bbb` (K ALL_TAC) 910 \\ FULL_SIMP_TAC bool_ss [getDATA_def,FST,SND,FEVERY_DEF] 911 \\ `~(x = 0)` by METIS_TAC [bijection_def,ONE_ONE_DEF] 912 \\ `(\(x,y,z,d). {y; z} SUBSET0 FDOM h) (x,h ' x)` by METIS_TAC [] 913 \\ `?a1 b1 c1. h ' x = (a1,b1,c1)` by METIS_TAC [PAIR] 914 \\ FULL_SIMP_TAC std_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT] 915 \\ FULL_SIMP_TAC std_ss [IN_DEF] 916 \\ `basic_abs m (y,x3,y3,d)` by FULL_SIMP_TAC bool_ss [basic_abs] 917 \\ `apply b (ch_set h) (y,x3,y3,d)` by METIS_TAC [] 918 \\ Q.PAT_X_ASSUM `b y = x` ASSUME_TAC 919 \\ FULL_SIMP_TAC std_ss [apply_def,ch_set_def,IN_DEF]); 920 921val ch_set_FUPDATE = prove( 922 ``ch_set (h |+ (fresh h,v1,v2,x)) = (fresh h,v1,v2,x) INSERT ch_set h``, 923 REWRITE_TAC [METIS_PROVE [PAIR] ``(f = g) = !a x y d. f (a,x,y,d) = g (a,x,y,d)``] 924 \\ SIMP_TAC std_ss [ch_set_def,FAPPLY_FUPDATE_THM,FDOM_FUPDATE,IN_INSERT] 925 \\ SIMP_TAC bool_ss [SIMP_RULE std_ss [IN_DEF] IN_INSERT,PAIR_EQ,ch_set_def] 926 \\ METIS_TAC [PAIR_EQ,fresh_NOT_IN_FDOM]); 927 928val FINITE_ch_set = store_thm("FINITE_ch_set", 929 ``!h:num|->num#num#'a. FINITE (ch_set h)``, 930 CONV_TAC (QUANT_CONV (UNBETA_CONV ``h:num|->num#num#'a``)) 931 \\ MATCH_MP_TAC fmap_INDUCT \\ SIMP_TAC bool_ss [] \\ REPEAT STRIP_TAC THENL [ 932 sg `ch_set (FEMPTY:num|->num#num#'a) = {}` 933 \\ ASM_SIMP_TAC bool_ss [FINITE_EMPTY] 934 \\ ASM_SIMP_TAC bool_ss [FINITE_EMPTY,ch_set_def,EMPTY_DEF,FDOM_FEMPTY,IN_DEF, 935 METIS_PROVE [PAIR] ``!f g. (f = g) = !x y z d. f (x,y,z,d) = g (x,y,z,d)``], 936 sg `ch_set ((f |+ (x,y)):num|->num#num#'a) = (x,y) INSERT ch_set f` 937 \\ ASM_SIMP_TAC std_ss [FINITE_INSERT] 938 \\ FULL_SIMP_TAC bool_ss [ch_set_def,INSERT_THM,FAPPLY_FUPDATE_THM,FDOM_FUPDATE,IN_DEF, 939 METIS_PROVE [PAIR] ``!f g. (f = g) = !x y z d. f (x,y,z,d) = g (x,y,z,d)``] 940 \\ Cases_on `y` \\ Cases_on `r` \\ METIS_TAC [PAIR_EQ]]); 941 942val FINITE_reachables = store_thm("FINITE_reachables", 943 ``!r h:num|->num#num#'a. FINITE (reachables r (ch_set h))``, 944 REPEAT STRIP_TAC 945 \\ (MATCH_MP_TAC o RW [AND_IMP_INTRO] o Q.GEN `s` o DISCH_ALL o 946 SPEC_ALL o UNDISCH o SPEC_ALL) SUBSET_FINITE 947 \\ Q.EXISTS_TAC `ch_set h` \\ FULL_SIMP_TAC bool_ss [ok_abs_def,FINITE_ch_set] 948 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,IN_DEF,FINITE_ch_set] 949 \\ Cases \\ Cases_on `r'` \\ Cases_on `r''` 950 \\ FULL_SIMP_TAC std_ss [reachables_def,IN_DEF]); 951 952val reachables_EQ_EMPTY = store_thm("reachables_EQ_EMPTY", 953 ``!x h. ~(x IN FDOM h) ==> (reachables [x] (ch_set h) = {})``, 954 REWRITE_TAC [METIS_PROVE [PAIR] ``(f = g) = (!a x y d. f (a,x,y,d) = g (a,x,y,d))``] 955 \\ SIMP_TAC bool_ss [reachables_def,MEM,IN_DEF,EMPTY_DEF,ch_set_def,reachable_def] 956 \\ REPEAT STRIP_TAC \\ Cases_on `a = x` \\ ASM_SIMP_TAC bool_ss [] 957 \\ DISJ2_TAC \\ CCONTR_TAC \\ FULL_SIMP_TAC bool_ss [] 958 \\ Cases_on `p` \\ REPEAT (FULL_SIMP_TAC std_ss [ch_set_def,APPEND,PATH_def,IN_DEF])); 959 960val reachables_NEXT = store_thm("reachables_NEXT", 961 ``!i x1 x2 d h. 962 i IN FDOM h /\ (h ' i = (x1,x2,d)) ==> 963 (reachables [i] (ch_set h) = 964 {(i,x1,x2,d)} UNION reachables [x1] (ch_set h) UNION reachables [x2] (ch_set h))``, 965 REWRITE_TAC [METIS_PROVE [PAIR] ``(f = g) = (!a x y d. f (a,x,y,d) = g (a,x,y,d))``] 966 \\ SIMP_TAC bool_ss [SIMP_RULE std_ss [IN_DEF] (CONJ IN_UNION IN_INSERT),EMPTY_DEF] 967 \\ SIMP_TAC bool_ss [reachables_def,IN_DEF,MEM,reachable_def] 968 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ STRIP_TAC 969 THEN1 FULL_SIMP_TAC bool_ss [ch_set_def] 970 THEN1 (Cases_on `p` \\ NTAC 2 (FULL_SIMP_TAC bool_ss [APPEND,PATH_def,ch_set_def,IN_DEF,PAIR_EQ]) 971 \\ METIS_TAC []) 972 \\ FULL_SIMP_TAC bool_ss [PAIR_EQ,ch_set_def,IN_DEF] 973 THEN1 (DISJ2_TAC \\ Q.EXISTS_TAC `[]` \\ 974 FULL_SIMP_TAC bool_ss [APPEND,PATH_def,IN_DEF,ch_set_def,PAIR_EQ] \\ METIS_TAC []) 975 THEN1 (DISJ2_TAC \\ Q.EXISTS_TAC `x1::p` \\ 976 FULL_SIMP_TAC bool_ss [APPEND,PATH_def,IN_DEF,ch_set_def,PAIR_EQ] \\ METIS_TAC []) 977 THEN1 (DISJ2_TAC \\ Q.EXISTS_TAC `[]` \\ 978 FULL_SIMP_TAC bool_ss [APPEND,PATH_def,IN_DEF,ch_set_def,PAIR_EQ] \\ METIS_TAC []) 979 THEN1 (DISJ2_TAC \\ Q.EXISTS_TAC `x2::p` \\ 980 FULL_SIMP_TAC bool_ss [APPEND,PATH_def,IN_DEF,ch_set_def,PAIR_EQ] \\ METIS_TAC [])); 981 982 983 984 985val reachables_THM = store_thm("reachables_THM", 986 ``!x y xs h. (reachables [] h = {}) /\ 987 (reachables (x::xs) h = reachables [x] h UNION reachables xs h)``, 988 REPEAT STRIP_TAC \\ REWRITE_TAC [EXTENSION,IN_UNION] 989 \\ Cases \\ Cases_on `r` \\ Cases_on `r'` 990 \\ SIMP_TAC bool_ss [reachables_def,MEM,IN_DEF,EMPTY_DEF] \\ METIS_TAC []); 991 992val reachables_fresh_LEMMA = prove( 993 ``reachables [fresh h] (ch_set (h |+ (fresh h,v1,v2,x))) = 994 {(fresh h,v1,v2,x)} UNION reachables [v1] (ch_set (h |+ (fresh h,v1,v2,x))) UNION 995 reachables [v2] (ch_set (h |+ (fresh h,v1,v2,x)))``, 996 MATCH_MP_TAC reachables_NEXT \\ SIMP_TAC bool_ss [FDOM_FUPDATE,IN_INSERT,FAPPLY_FUPDATE_THM]); 997 998val PATH_APPEND = prove( 999 ``!xs x y ys. PATH (x,xs ++ y::ys) s = PATH(x,xs++[y]) s /\ PATH(y,ys) s``, 1000 Induct \\ SIMP_TAC std_ss [PATH_def,APPEND] \\ METIS_TAC []); 1001 1002val LEMMA = prove( 1003 ``!p r. MEM r (v1::v2::vs) /\ PATH (r,p++[a]) ((fresh h,v1,v2,d) INSERT (ch_set h)) ==> 1004 ?p r'. MEM r' (v1::v2::vs) /\ 1005 (PATH (r',p++[a]) ((fresh h,v1,v2,d) INSERT (ch_set h)) \/ (a = v1) \/ (a = v2)) /\ 1006 ~MEM (fresh h) p``, 1007 completeInduct_on `LENGTH (p:num list)` \\ STRIP_TAC 1008 \\ REVERSE (Cases_on `?xs ys. p = xs ++ [fresh h] ++ ys`) \\ FULL_SIMP_TAC std_ss [] THENL [ 1009 REPEAT STRIP_TAC 1010 \\ Q.EXISTS_TAC `p` 1011 \\ Q.EXISTS_TAC `r` \\ ASM_SIMP_TAC bool_ss [] 1012 \\ Q.PAT_X_ASSUM `!xs ys. bbb` MP_TAC 1013 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 1014 \\ Induct_on `p` \\ SIMP_TAC bool_ss [MEM] \\ METIS_TAC [APPEND,CONS_11], 1015 REWRITE_TAC [GSYM APPEND_ASSOC,APPEND] 1016 \\ ONCE_REWRITE_TAC [PATH_APPEND] 1017 \\ Cases_on `ys` 1018 \\ SIMP_TAC bool_ss [APPEND,PATH_def,IN_INSERT] 1019 \\ SIMP_TAC bool_ss [IN_DEF] 1020 \\ SIMP_TAC bool_ss [fix_MEM,ch_set_def,fresh_NOT_IN_FDOM,PAIR_EQ,LENGTH_APPEND,LENGTH] 1021 THEN1 (REPEAT STRIP_TAC \\ METIS_TAC [MEM]) 1022 \\ STRIP_TAC 1023 \\ `LENGTH t < v` by DECIDE_TAC 1024 \\ REPEAT STRIP_TAC 1025 \\ `(LENGTH t = LENGTH t) /\ (MEM h' (v1::v2::vs))` by METIS_TAC [MEM] 1026 \\ METIS_TAC []]); 1027 1028val LEMMA2 = prove( 1029 ``!p k r. ~MEM k (r::p) ==> (PATH (r,p ++ [a]) ((k,x,y,z) INSERT s) = PATH (r,p ++ [a]) s)``, 1030 Induct \\ FULL_SIMP_TAC bool_ss [PATH_def,APPEND,MEM,IN_INSERT,PAIR_EQ]); 1031 1032val LEMMA3 = prove( 1033 ``!p k r x y z. ~MEM k (r::p) /\ PATH (r,p ++ [a]) ((k,x,y,z) INSERT s) ==> PATH (r,p ++ [a]) s``, 1034 METIS_TAC [LEMMA2]); 1035 1036val reachable_SUBSET = prove( 1037 ``!xs x s t. reachable x s y /\ s SUBSET t ==> reachable x t y``, 1038 METIS_TAC [reachable_def,PATH_SUBSET]); 1039 1040val reachables_fresh = store_thm("reachables_fresh", 1041 ``reachables (fresh h::vs) (ch_set (h |+ (fresh h,v1,v2,x))) = 1042 (fresh h,v1,v2,x) INSERT reachables (v1::v2::vs) (ch_set h)``, 1043 NTAC 2 (ONCE_REWRITE_TAC [reachables_THM]) 1044 \\ REWRITE_TAC [CONJUNCT1 (SPEC_ALL reachables_THM),UNION_EMPTY] 1045 \\ REWRITE_TAC [reachables_fresh_LEMMA,INSERT_UNION_EQ,UNION_EMPTY,GSYM UNION_ASSOC] 1046 \\ REWRITE_TAC [GSYM reachables_THM,ch_set_FUPDATE] 1047 \\ REWRITE_TAC [METIS_PROVE [PAIR] ``(f = g) = !a x y d. f (a,x,y,d) = g (a,x,y,d)``] 1048 \\ SIMP_TAC bool_ss [SIMP_RULE std_ss [IN_DEF] IN_INSERT,PAIR_EQ,ch_set_def] 1049 \\ REPEAT STRIP_TAC \\ REVERSE EQ_TAC THENL [ 1050 FULL_SIMP_TAC bool_ss [reachables_def,IN_INSERT,PAIR_EQ] 1051 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC bool_ss [IN_DEF] 1052 \\ DISJ2_TAC \\ Q.EXISTS_TAC `r` \\ ASM_SIMP_TAC bool_ss [] 1053 \\ METIS_TAC [reachable_SUBSET,IN_INSERT,SUBSET_DEF], 1054 FULL_SIMP_TAC bool_ss [reachables_def,IN_INSERT,PAIR_EQ] 1055 \\ FULL_SIMP_TAC bool_ss [IN_DEF,reachable_def] 1056 \\ FULL_SIMP_TAC bool_ss [fix_MEM] 1057 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC bool_ss [] THEN1 METIS_TAC [] 1058 \\ CONV_TAC RIGHT_OR_EXISTS_CONV 1059 \\ Cases_on `(a = v1)` THEN1 METIS_TAC [MEM] 1060 \\ Cases_on `(a = v2)` THEN1 METIS_TAC [MEM] 1061 \\ ASM_SIMP_TAC bool_ss [] 1062 \\ Cases_on `a = fresh h` 1063 \\ FULL_SIMP_TAC bool_ss [ch_set_def,fresh_NOT_IN_FDOM] 1064 \\ IMP_RES_TAC LEMMA 1065 \\ REVERSE (Cases_on `r' = fresh h`) THENL [ 1066 `~MEM (fresh h) (r'::p')` by METIS_TAC [MEM] 1067 \\ IMP_RES_TAC LEMMA3 1068 \\ Q.EXISTS_TAC `r'` 1069 \\ ASM_SIMP_TAC bool_ss [] 1070 \\ DISJ2_TAC 1071 \\ Q.EXISTS_TAC `p'` 1072 \\ ASM_SIMP_TAC bool_ss [], 1073 Cases_on `p'` 1074 \\ FULL_SIMP_TAC bool_ss [APPEND,PATH_def,IN_INSERT,PAIR_EQ] 1075 \\ FULL_SIMP_TAC bool_ss [IN_DEF] 1076 \\ FULL_SIMP_TAC bool_ss [ch_set_def,fresh_NOT_IN_FDOM,fix_MEM] 1077 \\ METIS_TAC [MEM,LEMMA3]]]); 1078 1079val _ = export_theory(); 1080