1open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_inv"; 2 3open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory; 4open combinTheory finite_mapTheory stringTheory addressTheory; 5 6open lisp_gcTheory cheney_gcTheory cheney_allocTheory; 7open lisp_typeTheory divideTheory; 8 9infix \\ 10val op \\ = op THEN; 11val RW = REWRITE_RULE; 12val RW1 = ONCE_REWRITE_RULE; 13 14(* --- definitions --- *) 15 16 17(* s-expression assertion *) 18 19val lisp_x_def = Define ` 20 (lisp_x (Val k) (a,dm,m) sym <=> (a = n2w (k * 4 + 2)) /\ k < 2 ** 30) /\ 21 (lisp_x (Sym s) (a,dm,m) sym <=> 22 ((a - 3w) && 3w = 0w) /\ (a - 3w,s) IN sym) /\ 23 (lisp_x (Dot x y) (a,dm,m) sym <=> a IN dm /\ ALIGNED a /\ 24 lisp_x x (m a,dm,m) sym /\ lisp_x y (m (a+4w),dm,m) sym)`; 25 26(* symbol table inv *) 27 28val string_mem_def = Define ` 29 (string_mem "" (a,m:word32->word8,df) = T) /\ 30 (string_mem (STRING c s) (a,m,df) <=> a IN df /\ 31 (m a = n2w (ORD c)) /\ string_mem s (a+1w,m,df))`; 32 33val string_mem_dom_def = Define ` 34 (string_mem_dom "" (a:word32) = {}) /\ 35 (string_mem_dom (STRING c s) a = a INSERT string_mem_dom s (a+1w))`; 36 37val symbol_table_def = Define ` 38 (symbol_table [] x (a,dm,m,dg,g) <=> (m a = 0w) /\ a IN dm /\ (x = {})) /\ 39 (symbol_table (s::xs) x (a,dm,m,dg,g) <=> 40 s <> "" /\ string_mem s (a+8w,g,dg) /\ 41 (m a = n2w (LENGTH s)) /\ {a; a+4w} SUBSET dm /\ ((a,s) IN x) /\ 42 let a' = a + n2w (8 + (LENGTH s + 3) DIV 4 * 4) in 43 a <+ a' /\ (m (a+4w) = a') /\ 44 symbol_table xs (x DELETE (a,s)) (a',dm,m,dg,g))`; 45 46val symbol_table_dom_def = Define ` 47 (symbol_table_dom [] (a,dm,dg) <=> ALIGNED a /\ a IN dm) /\ 48 (symbol_table_dom (s::xs) (a,dm,dg) <=> ~(s = "") /\ 49 string_mem_dom s (a+8w) SUBSET dg /\ {a; a+4w} SUBSET dm /\ 50 w2n a + 8 + LENGTH s + 3 < 2**32 /\ 51 a <+ a + n2w (8 + (LENGTH s + 3) DIV 4 * 4) /\ 52 symbol_table_dom xs (a + n2w (8 + (LENGTH s + 3) DIV 4 * 4),dm,dg))`; 53 54val builtin_symbols_def = Define ` 55 builtin_symbols = 56 ["nil"; "t"; "quote"; "+"; "-"; "*"; "div"; "mod"; "<"; "car"; "cdr"; 57 "cons"; "equal"; "cond"; "atomp"; "consp"; "numberp"; "symbolp"; "lambda"]`; 58 59val builtin_symbols_set_def = Define ` 60 builtin_symbols_set (w:word32) = 61 {(w,"nil"); (w + 12w,"t"); (w + 24w,"quote"); (w + 40w,"+"); 62 (w + 52w,"-"); (w + 64w,"*"); (w + 76w,"div"); (w + 88w,"mod"); 63 (w + 100w,"<"); (w + 112w,"car"); (w + 124w,"cdr"); 64 (w + 136w,"cons"); (w + 148w,"equal"); (w + 164w,"cond"); 65 (w + 176w,"atomp"); (w + 192w,"consp"); (w + 208w,"numberp"); 66 (w + 224w,"symbolp"); (w + 240w,"lambda")}`; 67 68Definition set_add_def: 69 set_add a x (b,s) <=> (b - (a:'a word), s) IN x 70End 71 72val lisp_symbol_table_def = Define ` 73 lisp_symbol_table x (a,dm,m,dg,g) = 74 ?symbols. 75 symbol_table (builtin_symbols ++ symbols) (set_add a x) (a,dm,m,dg,g) /\ 76 ALL_DISTINCT (builtin_symbols ++ symbols)`; 77 78(* main heap inv *) 79 80val lisp_inv_def = Define ` 81 lisp_inv (t1,t2,t3,t4,t5,t6,l) (w1,w2,w3,w4,w5,w6,a,dm,m,sym,rest) = 82 ?i u. 83 let v = if u then 1 + l else 1 in 84 let d = ch_active_set (a,v,i) in 85 32 <= w2n a /\ w2n a + 2 * 8 * l + 20 < 2 ** 32 /\ l <> 0 /\ 86 (m a = a + n2w (8 * i)) /\ ALIGNED a /\ v <= i /\ 87 i <= v + l /\ (m (a + 4w) = a + n2w (8 * (v + l))) /\ 88 (m (a - 28w) = if u then 0w else 1w) /\ 89 (m (a - 32w) = n2w (8 * l)) /\ (dm = ref_set a (l + l + 1)) /\ 90 lisp_symbol_table sym (a + 16w * n2w l + 24w,rest) /\ 91 lisp_x t1 (w1,d,m) sym /\ lisp_x t2 (w2,d,m) sym /\ 92 lisp_x t3 (w3,d,m) sym /\ lisp_x t4 (w4,d,m) sym /\ 93 lisp_x t5 (w5,d,m) sym /\ lisp_x t6 (w6,d,m) sym /\ 94 !w. w IN d ==> ok_data (m w) d /\ ok_data (m (w + 4w)) d`; 95 96 97(* --- theorems --- *) 98 99val lisp_x_word_tree = prove( 100 ``!x a dm m sym. 101 lisp_x x (a,dm,m) sym ==> 102 ?t. word_tree t (a,m) dm /\ (LSIZE x = XSIZE t) /\ (LDEPTH x = XDEPTH t) /\ 103 !a2 m2 dm2. word_tree t (a2,m2) dm2 ==> lisp_x x (a2,dm2,m2) sym``, 104 REVERSE Induct \\ REWRITE_TAC [lisp_x_def,ALIGNED_INTRO] 105 \\ REPEAT STRIP_TAC THEN1 106 (Q.EXISTS_TAC `XSym (ADDR30 a)` 107 \\ REWRITE_TAC [word_tree_def,XSIZE_def,LSIZE_def,XDEPTH_def,LDEPTH_def] 108 \\ STRIP_ASSUME_TAC (Q.SPEC `a` EXISTS_ADDR32) 109 \\ FULL_SIMP_TAC std_ss [word_arith_lemma4,ALIGNED_ADDR32, 110 ALIGNED_ADD_EQ,ALIGNED_n2w,ADDR30_ADDR32]) 111 THEN1 112 (Q.EXISTS_TAC `XVal (n2w n)` 113 \\ REWRITE_TAC [word_tree_def,XSIZE_def,LSIZE_def,XDEPTH_def,LDEPTH_def] 114 \\ ASM_SIMP_TAC std_ss [ADDR32_n2w,word_add_n2w,AC MULT_ASSOC MULT_COMM]) 115 \\ Q.PAT_X_ASSUM `!a. bbb` IMP_RES_TAC 116 \\ Q.PAT_X_ASSUM `!a dm m sym. bbb` IMP_RES_TAC 117 \\ Q.EXISTS_TAC `XDot t' t` 118 \\ ASM_SIMP_TAC std_ss [word_tree_def,XSIZE_def,LSIZE_def,XDEPTH_def,LDEPTH_def]); 119 120 121(* cons *) 122 123val lisp_inv_cons = store_thm("lisp_inv_cons", 124 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (ww1,ww2,ww3,ww4,ww5,ww6,a,x,xs,sym,rest) ==> 125 SUM_LSIZE [x1;x2;x3;x4;x5;x6] < limit ==> 126 ?w1 w2 w3 w4 w5 w6 a' x' xs'. 127 (arm_alloc (ww1,ww2,ww3,ww4,ww5,ww6,a,x,xs) = (w1,w2,w3,w4,w5,w6,a',x',xs')) /\ 128 lisp_inv (Dot x1 x2,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a',x',xs',sym,rest) /\ 129 arm_alloc_pre (ww1,ww2,ww3,ww4,ww5,ww6,a,x,xs) /\ (a' = a) /\ (x' = x)``, 130 SIMP_TAC std_ss [lisp_inv_def,SUM_LSIZE_def,ADD_ASSOC,LET_DEF] 131 \\ REPEAT STRIP_TAC 132 \\ Q.ABBREV_TAC `s = ch_active_set (a,if u then 1 + limit else 1,i)` 133 \\ (STRIP_ASSUME_TAC o UNDISCH o Q.SPECL [`x1`,`ww1`,`s`,`xs`,`sym`]) lisp_x_word_tree 134 \\ (STRIP_ASSUME_TAC o UNDISCH o Q.SPECL [`x2`,`ww2`,`s`,`xs`,`sym`]) lisp_x_word_tree 135 \\ (STRIP_ASSUME_TAC o UNDISCH o Q.SPECL [`x3`,`ww3`,`s`,`xs`,`sym`]) lisp_x_word_tree 136 \\ (STRIP_ASSUME_TAC o UNDISCH o Q.SPECL [`x4`,`ww4`,`s`,`xs`,`sym`]) lisp_x_word_tree 137 \\ (STRIP_ASSUME_TAC o UNDISCH o Q.SPECL [`x5`,`ww5`,`s`,`xs`,`sym`]) lisp_x_word_tree 138 \\ (STRIP_ASSUME_TAC o UNDISCH o Q.SPECL [`x6`,`ww6`,`s`,`xs`,`sym`]) lisp_x_word_tree 139 \\ Q.ABBREV_TAC `t1 = t` 140 \\ Q.ABBREV_TAC `t2 = t'` 141 \\ Q.ABBREV_TAC `t3 = t''` 142 \\ Q.ABBREV_TAC `t4 = t'''` 143 \\ Q.ABBREV_TAC `t5 = t''''` 144 \\ Q.ABBREV_TAC `t6 = t'''''` 145 \\ NTAC 6 (POP_ASSUM (K ALL_TAC)) 146 \\ `?w1 w2 w3 w4 w5 w6 a' x' xs'. 147 (arm_alloc (ww1,ww2,ww3,ww4,ww5,ww6,a,x,xs) = 148 (w1,w2,w3,w4,w5,w6,a',x',xs'))` by METIS_TAC [PAIR] 149 \\ Q.ABBREV_TAC `v = if u then 1 + limit else 1` 150 \\ `ch_tree (t1,t2,t3,t4,t5,t6,limit) (ww1,ww2,ww3,ww4,ww5,ww6,a,x,xs,a + n2w (8 * v),i-v)` by 151 (FULL_SIMP_TAC std_ss [ch_tree_def,LET_DEF] 152 \\ Q.EXISTS_TAC `i` \\ Q.EXISTS_TAC `u` \\ Q.UNABBREV_TAC `v` 153 \\ FULL_SIMP_TAC std_ss [ch_tree_def,LET_DEF]) 154 \\ FULL_SIMP_TAC std_ss [] 155 \\ IMP_RES_TAC ch_tree_alloc 156 \\ POP_ASSUM MP_TAC 157 \\ SIMP_TAC std_ss [ch_tree_def,LET_DEF] 158 \\ STRIP_TAC 159 \\ Q.PAT_X_ASSUM `a' = a` (fn th => FULL_SIMP_TAC std_ss [th]) 160 \\ Q.EXISTS_TAC `i'` \\ Q.EXISTS_TAC `u'` 161 \\ FULL_SIMP_TAC std_ss [word_tree_def,lisp_x_def] \\ METIS_TAC []); 162 163 164(* swap *) 165 166val lisp_inv_swap1 = store_thm("lisp_inv_swap1", 167 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 168 lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)``, 169 SIMP_TAC std_ss [lisp_inv_def,LET_DEF] \\ REPEAT STRIP_TAC 170 \\ Q.EXISTS_TAC `i` \\ Q.EXISTS_TAC `u` \\ ASM_SIMP_TAC std_ss []); 171 172val lisp_inv_swap2 = store_thm("lisp_inv_swap2", 173 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 174 lisp_inv (x2,x1,x3,x4,x5,x6,limit) (w2,w1,w3,w4,w5,w6,a,x,xs,s,rest)``, 175 SIMP_TAC std_ss [lisp_inv_def,LET_DEF] \\ REPEAT STRIP_TAC 176 \\ Q.EXISTS_TAC `i` \\ Q.EXISTS_TAC `u` \\ ASM_SIMP_TAC std_ss []); 177 178val lisp_inv_swap3 = store_thm("lisp_inv_swap3", 179 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 180 lisp_inv (x3,x2,x1,x4,x5,x6,limit) (w3,w2,w1,w4,w5,w6,a,x,xs,s,rest)``, 181 SIMP_TAC std_ss [lisp_inv_def,LET_DEF] \\ REPEAT STRIP_TAC 182 \\ Q.EXISTS_TAC `i` \\ Q.EXISTS_TAC `u` \\ ASM_SIMP_TAC std_ss []); 183 184val lisp_inv_swap4 = store_thm("lisp_inv_swap4", 185 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 186 lisp_inv (x4,x2,x3,x1,x5,x6,limit) (w4,w2,w3,w1,w5,w6,a,x,xs,s,rest)``, 187 SIMP_TAC std_ss [lisp_inv_def,LET_DEF] \\ REPEAT STRIP_TAC 188 \\ Q.EXISTS_TAC `i` \\ Q.EXISTS_TAC `u` \\ ASM_SIMP_TAC std_ss []); 189 190val lisp_inv_swap5 = store_thm("lisp_inv_swap5", 191 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 192 lisp_inv (x5,x2,x3,x4,x1,x6,limit) (w5,w2,w3,w4,w1,w6,a,x,xs,s,rest)``, 193 SIMP_TAC std_ss [lisp_inv_def,LET_DEF] \\ REPEAT STRIP_TAC 194 \\ Q.EXISTS_TAC `i` \\ Q.EXISTS_TAC `u` \\ ASM_SIMP_TAC std_ss []); 195 196val lisp_inv_swap6 = store_thm("lisp_inv_swap6", 197 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 198 lisp_inv (x6,x2,x3,x4,x5,x1,limit) (w6,w2,w3,w4,w5,w1,a,x,xs,s,rest)``, 199 SIMP_TAC std_ss [lisp_inv_def,LET_DEF] \\ REPEAT STRIP_TAC 200 \\ Q.EXISTS_TAC `i` \\ Q.EXISTS_TAC `u` \\ ASM_SIMP_TAC std_ss []); 201 202fun find_swap_thm n = 203 el n [lisp_inv_swap1,lisp_inv_swap2,lisp_inv_swap3,lisp_inv_swap4,lisp_inv_swap5,lisp_inv_swap6] 204 205fun generate_swap i j = 206 if i = 1 then find_swap_thm j else 207 if j = 1 then find_swap_thm i else 208 if i = j then find_swap_thm 1 else 209 DISCH_ALL (MATCH_MP (find_swap_thm i) (MATCH_MP (find_swap_thm j) (UNDISCH (find_swap_thm i)))); 210 (* e.g. to swap 4 and 5 do generate_swap 4 5 *) 211 212 213(* copy *) 214 215val lisp_inv_copy = store_thm("lisp_inv_copy", 216 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 217 lisp_inv (x1,x1,x3,x4,x5,x6,limit) (w1,w1,w3,w4,w5,w6,a,x,xs,s,rest)``, 218 SIMP_TAC std_ss [lisp_inv_def,LET_DEF] \\ REPEAT STRIP_TAC 219 \\ Q.EXISTS_TAC `i` \\ Q.EXISTS_TAC `u` \\ ASM_SIMP_TAC std_ss []); 220 221fun generate_copy i j = 222 if i = j then generate_swap 1 1 else 223 if j = 2 then let 224 val sw1 = generate_swap 1 i 225 val sw2 = generate_swap 1 2 226 val th = MATCH_MP lisp_inv_copy (MATCH_MP sw2 (UNDISCH sw1)) 227 in DISCH_ALL (MATCH_MP sw1 th) end 228 else let 229 val sw1 = generate_swap 2 i 230 val sw2 = generate_swap 1 j 231 val th = MATCH_MP lisp_inv_copy (MATCH_MP sw2 (UNDISCH sw1)) 232 in DISCH_ALL (MATCH_MP sw1 (MATCH_MP sw2 th)) end; 233 (* e.g. to copy 5 into 3 do generate_copy 3 5 *) 234 235val lisp_inv_move = save_thm("lisp_inv_move",let 236 fun pairs x [] = [] | pairs x (y::ys) = (x,y) :: pairs x ys 237 fun cross [] ys = [] | cross (x::xs) ys = pairs x ys @ cross xs ys 238 val list = filter (fn (x,y) => not (x = y)) (cross [1,2,3,4,5,6] [1,2,3,4,5,6]) 239 val thms = map (fn (x,y) => UNDISCH (generate_copy y x)) list 240 in RW [] (DISCH_ALL (foldr (uncurry CONJ) TRUTH thms)) end); 241 242 243(* assignments *) 244 245val lisp_inv_Val = store_thm("lisp_inv_Val", 246 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 247 !n. n < 2 ** 30 ==> 248 lisp_inv (Val n,x2,x3,x4,x5,x6,limit) 249 (n2w (n * 4 + 2),w2,w3,w4,w5,w6,a,x,xs,s,rest)``, 250 SIMP_TAC std_ss [lisp_inv_def,LET_DEF] \\ REPEAT STRIP_TAC 251 \\ Q.EXISTS_TAC `i` \\ Q.EXISTS_TAC `u` \\ ASM_SIMP_TAC std_ss [lisp_x_def]); 252 253 254(* car and cdr *) 255 256val lisp_inv_car_cdr = store_thm("lisp_inv_car_cdr", 257 ``lisp_inv (Dot y1 y2,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 258 (w1 && 3w = 0w) /\ w1 IN x /\ w1 + 4w IN x /\ 259 lisp_inv (y1,x2,x3,x4,x5,x6,limit) (xs w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) /\ 260 lisp_inv (y2,x2,x3,x4,x5,x6,limit) (xs (w1 + 4w),w2,w3,w4,w5,w6,a,x,xs,s,rest)``, 261 SIMP_TAC std_ss [lisp_inv_def,LET_DEF] \\ REVERSE (REPEAT STRIP_TAC) 262 \\ FULL_SIMP_TAC std_ss [lisp_x_def,ALIGNED_INTRO] 263 \\ REPEAT (Q.EXISTS_TAC `i` \\ Q.EXISTS_TAC `u`) 264 \\ ASM_SIMP_TAC std_ss [lisp_x_def] 265 \\ FULL_SIMP_TAC std_ss [ref_set_def,ch_active_set_def,IN_UNION,GSPECIFICATION] 266 \\ DISJ1_TAC \\ REWRITE_TAC [word_mul_n2w,word_add_n2w,GSYM WORD_ADD_ASSOC] THENL [ 267 Q.EXISTS_TAC `2 * j + 1` 268 \\ SIMP_TAC std_ss [LEFT_ADD_DISTRIB,MULT_ASSOC] 269 \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC, 270 Q.EXISTS_TAC `2 * j` 271 \\ SIMP_TAC std_ss [LEFT_ADD_DISTRIB,MULT_ASSOC] 272 \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC]); 273 274val lisp_inv_car_lemma = prove( 275 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> isDot x1 ==> 276 lisp_inv (CAR x1,x2,x3,x4,x5,x6,limit) (xs w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)``, 277 METIS_TAC [lisp_inv_car_cdr,isDot_thm,CAR_def]); 278 279val lisp_inv_cdr_lemma = prove( 280 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> isDot x1 ==> 281 lisp_inv (CDR x1,x2,x3,x4,x5,x6,limit) (xs (w1 + 4w),w2,w3,w4,w5,w6,a,x,xs,s,rest)``, 282 METIS_TAC [lisp_inv_car_cdr,isDot_thm,CDR_def]); 283 284val lisp_inv_address_lemma = prove( 285 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 286 isDot x1 ==> (w1 && 3w = 0w) /\ w1 IN x /\ w1 + 4w IN x``, 287 METIS_TAC [lisp_inv_car_cdr,isDot_thm]); 288 289val eq_lemma = METIS_PROVE [] ``(x ==> y) ==> (y ==> x) ==> (x = y:bool)`` 290fun mk_eq_lemma th = MATCH_MP (MATCH_MP eq_lemma th) th; 291 292fun generate_CAR i j is_car = let 293 val th = if is_car then lisp_inv_car_lemma else lisp_inv_cdr_lemma 294 val th = MATCH_MP th (UNDISCH (generate_swap 1 i)) 295 val th = UNDISCH (RW [AND_IMP_INTRO] (DISCH_ALL th)) 296 val th = DISCH_ALL (RW1 [mk_eq_lemma (generate_swap 1 i)] th) 297 val th = RW [GSYM AND_IMP_INTRO] th 298 val th = MATCH_MP th (UNDISCH (generate_copy i j)) 299 in DISCH_ALL th end; 300 (* to put car of 5 in 2 do generate_CAR 2 5 false *) 301 302val lisp_inv_address = save_thm("lisp_inv_address",let 303 val thms = [MATCH_MP lisp_inv_address_lemma (UNDISCH lisp_inv_swap1), 304 MATCH_MP lisp_inv_address_lemma (UNDISCH lisp_inv_swap2), 305 MATCH_MP lisp_inv_address_lemma (UNDISCH lisp_inv_swap3), 306 MATCH_MP lisp_inv_address_lemma (UNDISCH lisp_inv_swap4), 307 MATCH_MP lisp_inv_address_lemma (UNDISCH lisp_inv_swap5), 308 MATCH_MP lisp_inv_address_lemma (UNDISCH lisp_inv_swap6)] 309 in RW [] (DISCH_ALL (foldr (uncurry CONJ) TRUTH thms)) end); 310 311val lisp_inv_car = save_thm("lisp_inv_car",let 312 fun pairs x [] = [] | pairs x (y::ys) = (x,y) :: pairs x ys 313 fun cross [] ys = [] | cross (x::xs) ys = pairs x ys @ cross xs ys 314 val thms = map (fn (x,y) => UNDISCH (generate_CAR y x true)) (cross [1,2,3,4,5,6] [1,2,3,4,5,6]) 315 in RW [] (DISCH_ALL (foldr (uncurry CONJ) TRUTH thms)) end); 316 317val lisp_inv_cdr = save_thm("lisp_inv_cdr",let 318 fun pairs x [] = [] | pairs x (y::ys) = (x,y) :: pairs x ys 319 fun cross [] ys = [] | cross (x::xs) ys = pairs x ys @ cross xs ys 320 val thms = map (fn (x,y) => UNDISCH (generate_CAR y x false)) (cross [1,2,3,4,5,6] [1,2,3,4,5,6]) 321 in RW [] (DISCH_ALL (foldr (uncurry CONJ) TRUTH thms)) end); 322 323 324(* test *) 325 326val n2w_and_1_lemma = prove( 327 ``!w:word32. ((2w * w) && 1w = 0w) /\ ~((2w * w + 1w) && 1w = 0w)``, 328 Cases_word 329 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_mul_n2w,word_add_n2w, 330 n2w_and_1,n2w_11,RW1[MULT_COMM]MOD_EQ_0,RW1[MULT_COMM]MOD_MULT]); 331 332val lisp_inv_test_lemma = prove( 333 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 334 ((w1 && 3w = 0w) = isDot x1) /\ ((w1 && 1w = 0w) = ~isSym x1)``, 335 SIMP_TAC std_ss [lisp_inv_def,LET_DEF] \\ REPEAT STRIP_TAC 336 \\ Cases_on `x1` \\ FULL_SIMP_TAC std_ss [isDot_def,isSym_def, 337 lisp_x_def,ALIGNED_INTRO, GSYM word_add_n2w] 338 \\ REWRITE_TAC [GSYM (RW1 [MULT_COMM] ADDR32_n2w)] 339 \\ SIMP_TAC std_ss [ALIGNED_ADD_EQ,ALIGNED_ADDR32,ALIGNED_n2w] 340 THEN1 (IMP_RES_TAC NOT_ALIGNED \\ FULL_SIMP_TAC std_ss [WORD_SUB_ADD]) 341 \\ FULL_SIMP_TAC std_ss [ALIGNED_and_1] 342 \\ FULL_SIMP_TAC std_ss [ADDR32_n2w,word_add_n2w] 343 \\ REWRITE_TAC [DECIDE ``4 * n + 2 = 2 * (2 * n + 1):num``] 344 \\ REWRITE_TAC [GSYM word_mul_n2w,n2w_and_1_lemma] 345 \\ STRIP_ASSUME_TAC (Q.SPEC `w1` EXISTS_ADDR32) 346 \\ FULL_SIMP_TAC std_ss [ALIGNED_ADDR32,ALIGNED_ADD_EQ, 347 word_arith_lemma4,ALIGNED_n2w] 348 \\ Q.SPEC_TAC (`a'`,`q`) \\ Cases_word 349 \\ REWRITE_TAC [ADDR32_n2w,word_add_n2w,DECIDE ``4*n+3 = 2*(2*n+1)+1:num``] 350 \\ REWRITE_TAC [GSYM word_mul_n2w,GSYM word_add_n2w,n2w_and_1_lemma]); 351 352val lisp_inv_test = save_thm("lisp_inv_test",let 353 val thms = [MATCH_MP lisp_inv_test_lemma (UNDISCH lisp_inv_swap1), 354 MATCH_MP lisp_inv_test_lemma (UNDISCH lisp_inv_swap2), 355 MATCH_MP lisp_inv_test_lemma (UNDISCH lisp_inv_swap3), 356 MATCH_MP lisp_inv_test_lemma (UNDISCH lisp_inv_swap4), 357 MATCH_MP lisp_inv_test_lemma (UNDISCH lisp_inv_swap5), 358 MATCH_MP lisp_inv_test_lemma (UNDISCH lisp_inv_swap6)] 359 in RW [] (DISCH_ALL (foldr (uncurry CONJ) TRUTH thms)) end); 360 361 362(* basic equality *) 363 364val symbol_table_LOWER_EQ = prove( 365 ``!xs a sym. symbol_table xs sym (a,dm,m,dg,g) /\ (b,x) IN sym ==> a <=+ b``, 366 Induct \\ SIMP_TAC std_ss [symbol_table_def,NOT_IN_EMPTY,LET_DEF] 367 \\ REPEAT STRIP_TAC \\ Cases_on `a = b` THEN1 METIS_TAC [WORD_LOWER_EQ_REFL] 368 \\ `(b,x) IN (sym DELETE (a,h))` by METIS_TAC [IN_DELETE,PAIR_EQ] 369 \\ RES_TAC \\ IMP_RES_TAC WORD_LOWER_LOWER_EQ_TRANS 370 \\ ASM_SIMP_TAC std_ss [WORD_LOWER_OR_EQ]); 371 372val symbol_tabel_11 = prove( 373 ``!xs a sym. symbol_table xs sym (a,dm,m,dg,g) /\ (b,x) IN sym /\ (b,y) IN sym ==> 374 (x = y)``, 375 Induct \\ SIMP_TAC std_ss [symbol_table_def,NOT_IN_EMPTY,LET_DEF] 376 \\ REPEAT STRIP_TAC 377 \\ REVERSE (Cases_on `a = b`) THEN1 378 (`(b,x) IN (sym DELETE (a,h)) /\ (b,y) IN (sym DELETE (a,h))` by 379 METIS_TAC [IN_DELETE,PAIR_EQ] 380 \\ METIS_TAC []) 381 \\ FULL_SIMP_TAC std_ss [] 382 \\ Q.ABBREV_TAC `a2 = b + n2w (8 + (LENGTH h + 3) DIV 4 * 4)` 383 \\ Cases_on `(b,x) IN (sym DELETE (a,h))` THEN1 384 (`a2 <=+ b` by METIS_TAC [symbol_table_LOWER_EQ] 385 \\ METIS_TAC [WORD_LOWER_EQ_ANTISYM]) 386 \\ Cases_on `(b,y) IN (sym DELETE (a,h))` THEN1 387 (`a2 <=+ b` by METIS_TAC [symbol_table_LOWER_EQ] 388 \\ METIS_TAC [WORD_LOWER_EQ_ANTISYM]) 389 \\ METIS_TAC [IN_DELETE,PAIR_EQ]); 390 391val symbol_table_MEM = store_thm("symbol_table_MEM", 392 ``!xs a sym. symbol_table xs sym (a,dm,m,dg,g) /\ (b,x) IN sym ==> 393 MEM x xs``, 394 Induct THEN1 SIMP_TAC std_ss [symbol_table_def,NOT_IN_EMPTY,LET_DEF] 395 \\ REPEAT STRIP_TAC 396 \\ `!y. (b,y) IN sym ==> (x = y)` by METIS_TAC [symbol_tabel_11] 397 \\ Cases_on `b = a` 398 \\ FULL_SIMP_TAC std_ss [symbol_table_def,MEM,LET_DEF] 399 \\ METIS_TAC [IN_DELETE,PAIR_EQ]); 400 401val symbol_table_eq = store_thm("symbol_table_eq", 402 ``!xs sym a. 403 symbol_table xs sym (a,dm,m,dg,g) /\ ALL_DISTINCT xs ==> 404 (w1,s1) IN sym /\ (w2,s2) IN sym ==> ((w1 = w2) = (s1 = s2))``, 405 Induct THEN1 SIMP_TAC std_ss [symbol_table_def,NOT_IN_EMPTY] 406 \\ REWRITE_TAC [symbol_table_def] 407 \\ STRIP_TAC \\ STRIP_TAC \\ STRIP_TAC 408 \\ Q.ABBREV_TAC `a2 = a + n2w (8 + (LENGTH h + 3) DIV 4 * 4)` 409 \\ SIMP_TAC std_ss [LET_DEF,ALL_DISTINCT] 410 \\ REPEAT STRIP_TAC 411 \\ Cases_on `(w1,s1) IN (sym DELETE (a,h))` 412 \\ Cases_on `(w2,s2) IN (sym DELETE (a,h))` 413 THEN1 METIS_TAC [] THENL [ 414 `(w2 = a) /\ (s2 = h)` by (FULL_SIMP_TAC std_ss [IN_DELETE] \\ METIS_TAC []) 415 \\ `a2 <=+ w1 /\ MEM s1 xs` by METIS_TAC [symbol_table_LOWER_EQ,symbol_table_MEM] 416 \\ IMP_RES_TAC WORD_LOWER_LOWER_EQ_TRANS 417 \\ METIS_TAC [WORD_LOWER_NOT_EQ], 418 `(w1 = a) /\ (s1 = h)` by (FULL_SIMP_TAC std_ss [IN_DELETE] \\ METIS_TAC []) 419 \\ `a2 <=+ w2 /\ MEM s2 xs` by METIS_TAC [symbol_table_LOWER_EQ,symbol_table_MEM] 420 \\ IMP_RES_TAC WORD_LOWER_LOWER_EQ_TRANS 421 \\ METIS_TAC [WORD_LOWER_NOT_EQ], 422 `(w1 = a) /\ (s1 = h)` by (FULL_SIMP_TAC std_ss [IN_DELETE] \\ METIS_TAC []) 423 \\ `(w2 = a) /\ (s2 = h)` by (FULL_SIMP_TAC std_ss [IN_DELETE] \\ METIS_TAC []) 424 \\ ASM_SIMP_TAC std_ss []]); 425 426val lisp_inv_eq_lemma = prove( 427 ``(isVal x1 /\ isVal x2) \/ (isSym x1 /\ isSym x2) ==> 428 lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 429 ((x1 = x2) = (w1 = w2))``, 430 STRIP_TAC THEN1 431 (`?a1 a2. (x1 = Val a1) /\ (x2 = Val a2)` by 432 (Cases_on `x1` \\ Cases_on `x2` \\ FULL_SIMP_TAC std_ss [isVal_def,SExp_11]) 433 \\ ASM_SIMP_TAC std_ss [LISP_LESS_def,lisp_inv_def,LET_DEF] 434 \\ REPEAT STRIP_TAC 435 \\ FULL_SIMP_TAC std_ss [lisp_x_def,GSYM word_add_n2w,ADDR32_11, 436 WORD_EQ_ADD_RCANCEL, GSYM (RW1 [MULT_COMM] ADDR32_n2w)] 437 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,SExp_11]) 438 \\ `?a1 a2. (x1 = Sym a1) /\ (x2 = Sym a2)` by 439 (Cases_on `x1` \\ Cases_on `x2` \\ FULL_SIMP_TAC std_ss [isSym_def,SExp_11]) 440 \\ ASM_SIMP_TAC std_ss [SExp_11] 441 \\ `?dg dm g m. rest = (dm,m,dg,g)` by METIS_TAC [PAIR] 442 \\ FULL_SIMP_TAC std_ss [lisp_inv_def,lisp_symbol_table_def, 443 LET_DEF,lisp_x_def] \\ STRIP_TAC 444 \\ Q.ABBREV_TAC `ww = a + 16w * n2w limit + 24w` 445 \\ `((w1 - 3w) + ww,a1) IN (set_add ww s)` by 446 FULL_SIMP_TAC std_ss [set_add_def,set_add_def,IN_DEF,WORD_ADD_SUB] 447 \\ `((w2 - 3w) + ww,a2) IN (set_add ww s)` by 448 FULL_SIMP_TAC std_ss [set_add_def,set_add_def,IN_DEF,WORD_ADD_SUB] 449 \\ IMP_RES_TAC (GSYM symbol_table_eq) 450 \\ ASM_SIMP_TAC std_ss [WORD_EQ_ADD_RCANCEL] 451 \\ ONCE_REWRITE_TAC [Q.SPECL [`x`,`3w`,`y`] (GSYM WORD_EQ_ADD_RCANCEL)] 452 \\ REWRITE_TAC [WORD_SUB_ADD] 453 \\ ASM_SIMP_TAC std_ss [WORD_EQ_ADD_RCANCEL]); 454 455val lisp_inv_eq = store_thm("lisp_inv_eq", 456 ``~isDot x1 \/ ~isDot x2 ==> 457 lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 458 ((x1 = x2) = (w1 = w2))``, 459 STRIP_TAC THENL [ 460 Cases_on `x1` \\ FULL_SIMP_TAC std_ss [isDot_def] 461 \\ Cases_on `x2` \\ STRIP_TAC \\ SIMP_TAC std_ss [SExp_distinct] 462 \\ IMP_RES_TAC lisp_inv_test 463 \\ FULL_SIMP_TAC std_ss [isVal_def,isSym_def,isDot_def] 464 \\ METIS_TAC [lisp_inv_eq_lemma,isVal_def,isSym_def], 465 Cases_on `x2` \\ FULL_SIMP_TAC std_ss [isDot_def] 466 \\ Cases_on `x1` \\ STRIP_TAC \\ SIMP_TAC std_ss [SExp_distinct] 467 \\ IMP_RES_TAC lisp_inv_test 468 \\ FULL_SIMP_TAC std_ss [isVal_def,isSym_def,isDot_def] 469 \\ METIS_TAC [lisp_inv_eq_lemma,isVal_def,isSym_def]]); 470 471val lisp_inv_eq_0 = store_thm("lisp_inv_eq_0", 472 ``!n. n < 2 ** 30 ==> 473 lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 474 ((x1 = Val n) = (w1 = n2w (n * 4 + 2)))``, 475 REPEAT STRIP_TAC 476 \\ `lisp_inv (x1,x1,x3,x4,x5,x6,limit) (w1,w1,w3,w4,w5,w6,a,x,xs,s,rest)` by 477 METIS_TAC [lisp_inv_move] 478 \\ (IMP_RES_TAC o DISCH ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)`` o 479 UNDISCH o Q.SPEC `n` o UNDISCH) lisp_inv_Val 480 \\ MATCH_MP_TAC (RW [AND_IMP_INTRO] lisp_inv_eq) 481 \\ REWRITE_TAC [isDot_def] 482 \\ (IMP_RES_TAC o DISCH ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)`` o 483 MATCH_MP lisp_inv_swap2 o UNDISCH o Q.SPEC `n` o UNDISCH) lisp_inv_Val); 484 485 486(* symbol test *) 487 488val builti_symbols_thm = store_thm("builti_symbols_thm", 489 ``lisp_symbol_table s (sa,rest) ==> 490 (ADDR32 0w,"nil") IN s /\ 491 (ADDR32 3w,"t") IN s /\ 492 (ADDR32 6w,"quote") IN s /\ 493 (ADDR32 10w,"+") IN s /\ 494 (ADDR32 13w,"-") IN s /\ 495 (ADDR32 16w,"*") IN s /\ 496 (ADDR32 19w,"div") IN s /\ 497 (ADDR32 22w,"mod") IN s /\ 498 (ADDR32 25w,"<") IN s /\ 499 (ADDR32 28w,"car") IN s /\ 500 (ADDR32 31w,"cdr") IN s /\ 501 (ADDR32 34w,"cons") IN s /\ 502 (ADDR32 37w,"equal") IN s /\ 503 (ADDR32 41w,"cond") IN s /\ 504 (ADDR32 44w,"atomp") IN s /\ 505 (ADDR32 48w,"consp") IN s /\ 506 (ADDR32 52w,"numberp") IN s /\ 507 (ADDR32 56w,"symbolp") IN s /\ 508 (ADDR32 60w,"lambda") IN s``, 509 `?dg g dm m. rest = (dm,m,dg,g)` by METIS_TAC [PAIR] 510 \\ ASM_REWRITE_TAC [lisp_symbol_table_def] 511 \\ POP_ASSUM (K ALL_TAC) 512 \\ STRIP_TAC \\ POP_ASSUM MP_TAC \\ POP_ASSUM MP_TAC 513 \\ REWRITE_TAC [builtin_symbols_def,APPEND] 514 \\ ONCE_REWRITE_TAC [symbol_table_def] 515 \\ SIMP_TAC std_ss [LENGTH,LET_DEF] 516 \\ SIMP_TAC std_ss [IN_DEF,set_add_def,WORD_SUB_REFL] 517 \\ ONCE_REWRITE_TAC [symbol_table_def] 518 \\ SIMP_TAC std_ss [LENGTH,LET_DEF,IN_DELETE] 519 \\ SIMP_TAC std_ss [IN_DEF,set_add_def,WORD_ADD_SUB2,ADDR32_n2w] 520 \\ NTAC 30 (SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_add_n2w] 521 \\ ONCE_REWRITE_TAC [symbol_table_def] 522 \\ SIMP_TAC std_ss [LENGTH,LET_DEF,IN_DELETE] 523 \\ SIMP_TAC std_ss [IN_DEF,set_add_def,WORD_ADD_SUB2,ADDR32_n2w])) 524 525val lisp_symbol_table_11 = store_thm("lisp_symbol_table_11", 526 ``lisp_symbol_table s (sa,rest) /\ 527 (x1,s1) IN s /\ (x2,s2) IN s ==> 528 ((x1 = x2) = (s1 = s2))``, 529 `?dg g dm m. rest = (dm,m,dg,g)` by METIS_TAC [PAIR] 530 \\ ASM_REWRITE_TAC [lisp_symbol_table_def] 531 \\ REPEAT STRIP_TAC 532 \\ `(x1 + sa,s1) IN (set_add sa s)` by 533 FULL_SIMP_TAC std_ss [IN_DEF,set_add_def,WORD_ADD_SUB] 534 \\ `(x2 + sa,s2) IN (set_add sa s)` by 535 FULL_SIMP_TAC std_ss [IN_DEF,set_add_def,WORD_ADD_SUB] 536 \\ IMP_RES_TAC symbol_table_eq 537 \\ METIS_TAC [WORD_EQ_ADD_RCANCEL,ADDR32_11]); 538 539val lisp_symbol_table_11_ADDR32 = prove( 540 ``lisp_symbol_table s (sa,rest) /\ 541 (ADDR32 x1,s1) IN s /\ (ADDR32 x2,s2) IN s ==> 542 ((x1 = x2) = (s1 = s2))``, 543 `?dg g dm m. rest = (dm,m,dg,g)` by METIS_TAC [PAIR] 544 \\ ASM_REWRITE_TAC [lisp_symbol_table_def] 545 \\ REPEAT STRIP_TAC 546 \\ `(ADDR32 x1 + sa,s1) IN (set_add sa s)` by 547 FULL_SIMP_TAC std_ss [IN_DEF,set_add_def,WORD_ADD_SUB] 548 \\ `(ADDR32 x2 + sa,s2) IN (set_add sa s)` by 549 FULL_SIMP_TAC std_ss [IN_DEF,set_add_def,WORD_ADD_SUB] 550 \\ IMP_RES_TAC symbol_table_eq 551 \\ METIS_TAC [WORD_EQ_ADD_RCANCEL,ADDR32_11]); 552 553val lisp_inv_test_builtin_lemma = prove( 554 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 555 ((w1 = ADDR32 0w + 3w) = (x1 = Sym "nil")) /\ 556 ((w1 = ADDR32 3w + 3w) = (x1 = Sym "t")) /\ 557 ((w1 = ADDR32 6w + 3w) = (x1 = Sym "quote")) /\ 558 ((w1 = ADDR32 10w + 3w) = (x1 = Sym "+")) /\ 559 ((w1 = ADDR32 13w + 3w) = (x1 = Sym "-")) /\ 560 ((w1 = ADDR32 16w + 3w) = (x1 = Sym "*")) /\ 561 ((w1 = ADDR32 19w + 3w) = (x1 = Sym "div")) /\ 562 ((w1 = ADDR32 22w + 3w) = (x1 = Sym "mod")) /\ 563 ((w1 = ADDR32 25w + 3w) = (x1 = Sym "<")) /\ 564 ((w1 = ADDR32 28w + 3w) = (x1 = Sym "car")) /\ 565 ((w1 = ADDR32 31w + 3w) = (x1 = Sym "cdr")) /\ 566 ((w1 = ADDR32 34w + 3w) = (x1 = Sym "cons")) /\ 567 ((w1 = ADDR32 37w + 3w) = (x1 = Sym "equal")) /\ 568 ((w1 = ADDR32 41w + 3w) = (x1 = Sym "cond")) /\ 569 ((w1 = ADDR32 44w + 3w) = (x1 = Sym "atomp")) /\ 570 ((w1 = ADDR32 48w + 3w) = (x1 = Sym "consp")) /\ 571 ((w1 = ADDR32 52w + 3w) = (x1 = Sym "numberp")) /\ 572 ((w1 = ADDR32 56w + 3w) = (x1 = Sym "symbolp")) /\ 573 ((w1 = ADDR32 60w + 3w) = (x1 = Sym "lambda"))``, 574 STRIP_TAC \\ REVERSE (Cases_on `isSym x1 `) THEN1 575 (`w1 && 1w = 0w` by METIS_TAC [lisp_inv_test] 576 \\ Cases_on `x1` \\ FULL_SIMP_TAC std_ss 577 [isDot_def,isVal_def,isSym_def,SExp_distinct] 578 \\ REPEAT STRIP_TAC 579 \\ FULL_SIMP_TAC std_ss [ADDR32_n2w,word_add_n2w,n2w_and_1] 580 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [n2w_11]) 581 \\ FULL_SIMP_TAC std_ss [lisp_inv_def,LET_DEF] 582 \\ Q.ABBREV_TAC `sa = a + 16w * n2w limit + 24w` 583 \\ POP_ASSUM (K ALL_TAC) 584 \\ FULL_SIMP_TAC std_ss [isSym_thm,lisp_x_def,SExp_11] 585 \\ FULL_SIMP_TAC std_ss [isSym_thm,lisp_x_def,SExp_11] 586 \\ STRIP_ASSUME_TAC (Q.SPEC `w1`EXISTS_ADDR32) 587 \\ FULL_SIMP_TAC std_ss [ALIGNED_INTRO,word_arith_lemma4, 588 ALIGNED_ADD_EQ,ALIGNED_ADDR32,ALIGNED_n2w] 589 \\ FULL_SIMP_TAC std_ss [WORD_EQ_ADD_RCANCEL,ADDR32_11] 590 \\ Q.PAT_X_ASSUM `xx IN s` MP_TAC 591 \\ Q.PAT_X_ASSUM `lisp_symbol_table sss ssss` MP_TAC 592 \\ REPEAT (POP_ASSUM (K ALL_TAC)) \\ STRIP_TAC 593 \\ IMP_RES_TAC builti_symbols_thm 594 \\ REPEAT STRIP_TAC 595 \\ (MATCH_MP_TAC lisp_symbol_table_11_ADDR32 596 \\ FULL_SIMP_TAC std_ss [WORD_ADD_0])); 597 598val lisp_inv_builtin = save_thm("lisp_inv_builtin", 599 SIMP_RULE std_ss [ADDR32_n2w,word_add_n2w] 600 lisp_inv_test_builtin_lemma); 601 602val lisp_inv_nil = store_thm("lisp_inv_nil", 603 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 604 lisp_inv (Sym "nil",x2,x3,x4,x5,x6,limit) (3w,w2,w3,w4,w5,w6,a,x,xs,s,rest)``, 605 SIMP_TAC std_ss [lisp_inv_def,LET_DEF] \\ REPEAT STRIP_TAC 606 \\ Q.EXISTS_TAC `i` \\ Q.EXISTS_TAC `u` 607 \\ ASM_SIMP_TAC std_ss [lisp_x_def,ALIGNED_INTRO,word_arith_lemma2, 608 ALIGNED_n2w] \\ IMP_RES_TAC builti_symbols_thm 609 \\ FULL_SIMP_TAC std_ss [ADDR32_n2w]); 610 611val lisp_inv_t = store_thm("lisp_inv_t", 612 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 613 lisp_inv (Sym "t",x2,x3,x4,x5,x6,limit) (15w,w2,w3,w4,w5,w6,a,x,xs,s,rest)``, 614 SIMP_TAC std_ss [lisp_inv_def,LET_DEF] \\ REPEAT STRIP_TAC 615 \\ Q.EXISTS_TAC `i` \\ Q.EXISTS_TAC `u` 616 \\ ASM_SIMP_TAC std_ss [lisp_x_def,ALIGNED_INTRO,word_arith_lemma2, 617 ALIGNED_n2w] \\ IMP_RES_TAC builti_symbols_thm 618 \\ FULL_SIMP_TAC std_ss [ADDR32_n2w]); 619 620val lisp_inv_quote = store_thm("lisp_inv_quote", 621 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 622 lisp_inv (Sym "quote",x2,x3,x4,x5,x6,limit) (27w,w2,w3,w4,w5,w6,a,x,xs,s,rest)``, 623 SIMP_TAC std_ss [lisp_inv_def,LET_DEF] \\ REPEAT STRIP_TAC 624 \\ Q.EXISTS_TAC `i` \\ Q.EXISTS_TAC `u` 625 \\ ASM_SIMP_TAC std_ss [lisp_x_def,ALIGNED_INTRO,word_arith_lemma2, 626 ALIGNED_n2w] \\ IMP_RES_TAC builti_symbols_thm 627 \\ FULL_SIMP_TAC std_ss [ADDR32_n2w]); 628 629 630(* basic arithmetic *) 631 632val lisp_inv_read_Val = prove( 633 ``lisp_inv (Val n,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 634 n < 2 ** 30 /\ (w1 = n2w (4 * n + 2))``, 635 SIMP_TAC std_ss [lisp_inv_def,LET_DEF] \\ REPEAT STRIP_TAC 636 \\ FULL_SIMP_TAC std_ss [lisp_x_def,AC MULT_COMM MULT_ASSOC]); 637 638val isVal_TAC = 639 REWRITE_TAC [GSYM AND_IMP_INTRO,isVal_thm] 640 \\ REPEAT (STRIP_TAC \\ ASM_SIMP_TAC std_ss [getVal_def]) 641 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC lisp_inv_read_Val 642 \\ IMP_RES_TAC (DISCH_ALL (MATCH_MP lisp_inv_read_Val 643 (UNDISCH (Q.INST [`x2`|->`Val n`] lisp_inv_swap2)))) 644 645val lisp_inv_ADD = store_thm("lisp_inv_ADD", 646 ``isVal x1 /\ isVal x2 /\ getVal x1 + getVal x2 < 2**30 ==> 647 lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 648 lisp_inv (LISP_ADD x1 x2,x2,x3,x4,x5,x6,limit) (w1+w2-2w,w2,w3,w4,w5,w6,a,x,xs,s,rest)``, 649 isVal_TAC 650 \\ ASM_REWRITE_TAC [LISP_ADD_def,GSYM word_add_n2w,WORD_ADD_ASSOC,WORD_ADD_SUB] 651 \\ ASM_REWRITE_TAC [word_add_n2w,DECIDE ``4*m+2+4*n = (m+n) * 4 + 2:num``] 652 \\ (MATCH_MP_TAC o RW [AND_IMP_INTRO] o DISCH_ALL o SPEC_ALL o UNDISCH) lisp_inv_Val 653 \\ SIMP_TAC std_ss [] \\ METIS_TAC []); 654 655val lisp_inv_ADD1 = store_thm("lisp_inv_ADD1", 656 ``isVal x1 /\ getVal x1 + 1 < 2**30 ==> 657 lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 658 lisp_inv (LISP_ADD x1 (Val 1),x2,x3,x4,x5,x6,limit) (w1 + 4w,w2,w3,w4,w5,w6,a,x,xs,s,rest)``, 659 isVal_TAC 660 \\ ASM_REWRITE_TAC [LISP_ADD_def,GSYM word_add_n2w,WORD_ADD_ASSOC,WORD_ADD_SUB] 661 \\ ASM_REWRITE_TAC [word_add_n2w,DECIDE ``4*m+2+4 = (m+1) * 4 + 2:num``] 662 \\ (MATCH_MP_TAC o GEN_ALL o RW [AND_IMP_INTRO] o DISCH_ALL o SPEC_ALL o UNDISCH) lisp_inv_Val 663 \\ SIMP_TAC std_ss [] \\ METIS_TAC []); 664 665val lisp_inv_SUB = store_thm("lisp_inv_SUB", 666 ``isVal x1 /\ isVal x2 /\ getVal x2 <= getVal x1 ==> 667 lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 668 lisp_inv (LISP_SUB x1 x2,x2,x3,x4,x5,x6,limit) (w1 - w2 + 2w,w2,w3,w4,w5,w6,a,x,xs,s,rest)``, 669 isVal_TAC 670 \\ ASM_REWRITE_TAC [LISP_SUB_def,GSYM word_add_n2w,WORD_ADD_ASSOC,WORD_ADD_SUB] 671 \\ `(n2w (4 * a') + 2w - (n2w (4 * a'') + 2w) + 2w:word32 = 672 n2w ((a' - a'') * 4 + 2)) /\ a' < a'' + 1073741824` suffices_by (STRIP_TAC THEN ASM_SIMP_TAC std_ss [] 673 \\ (MATCH_MP_TAC o GEN_ALL o RW [AND_IMP_INTRO] o DISCH_ALL o SPEC_ALL o UNDISCH) lisp_inv_Val 674 \\ ASM_SIMP_TAC std_ss [word_add_n2w] \\ METIS_TAC []) 675 \\ REVERSE STRIP_TAC 676 THEN1 (FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC) 677 \\ REWRITE_TAC [word_add_n2w,word_arith_lemma2] 678 \\ `~(4 * a' + 2 < 4 * a'' + 2)` by DECIDE_TAC 679 \\ ASM_SIMP_TAC bool_ss [word_add_n2w] 680 \\ MATCH_MP_TAC (METIS_PROVE [] ``(x = y) ==> (f x = f y)``) 681 \\ DECIDE_TAC); 682 683val lisp_inv_SUB1 = store_thm("lisp_inv_SUB1", 684 ``isVal x1 /\ 0 < getVal x1 ==> 685 lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 686 lisp_inv (LISP_SUB x1 (Val 1),x2,x3,x4,x5,x6,limit) (w1 - 4w,w2,w3,w4,w5,w6,a,x,xs,s,rest)``, 687 isVal_TAC 688 \\ ASM_REWRITE_TAC [LISP_SUB_def,GSYM word_add_n2w,WORD_ADD_ASSOC,WORD_ADD_SUB] 689 \\ `(n2w (4 * a') + 2w - 4w:word32 = 690 n2w ((a' - 1) * 4 + 2)) /\ a' < 1073741825` suffices_by (STRIP_TAC THEN ASM_SIMP_TAC std_ss [] 691 \\ (MATCH_MP_TAC o GEN_ALL o RW [AND_IMP_INTRO] o DISCH_ALL o SPEC_ALL o UNDISCH) lisp_inv_Val 692 \\ ASM_SIMP_TAC std_ss [word_add_n2w] \\ METIS_TAC []) 693 \\ REVERSE STRIP_TAC 694 THEN1 (FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC) 695 \\ REWRITE_TAC [word_add_n2w,word_arith_lemma2] 696 \\ `~(4 * a' + 2 < 4)` by DECIDE_TAC 697 \\ ASM_SIMP_TAC bool_ss [word_add_n2w] 698 \\ MATCH_MP_TAC (METIS_PROVE [] ``(x = y) ==> (f x = f y)``) 699 \\ DECIDE_TAC); 700 701val word_lsr_n2w = store_thm("word_lsr_n2w", 702 ``!m n. m < dimword (:'a) ==> 703 (((n2w m):'a word) >>> n = n2w (m DIV (2 ** n)))``, 704 ONCE_REWRITE_TAC [GSYM n2w_w2n] THEN REWRITE_TAC [w2n_lsr] 705 THEN REWRITE_TAC [n2w_w2n] THEN SIMP_TAC std_ss [w2n_n2w]); 706 707val LEMMA_MULT_4 = DECIDE ``!n. n < 1073741824 ==> 4 * n + 2 < 4294967296:num`` 708 709val lisp_inv_Val_nil_nil = let 710 val imp = ((UNDISCH o SPEC_ALL o UNDISCH) lisp_inv_Val) 711 val imp1 = DISCH_ALL (MATCH_MP lisp_inv_swap2 (UNDISCH lisp_inv_nil)) 712 val imp2 = DISCH_ALL (MATCH_MP lisp_inv_swap3 (UNDISCH lisp_inv_nil)) 713 val imp1 = DISCH_ALL (MATCH_MP imp1 (UNDISCH lisp_inv_swap2)) 714 val imp2 = DISCH_ALL (MATCH_MP imp2 (UNDISCH lisp_inv_swap3)) 715 val imp = (GEN_ALL o RW [AND_IMP_INTRO] o DISCH_ALL) (MATCH_MP imp2 (MATCH_MP imp1 imp)) 716 in imp end; 717 718val lisp_inv_MULT = store_thm("lisp_inv_MULT", 719 ``isVal x1 /\ isVal x2 /\ getVal x1 * getVal x2 < 2 ** 30 ==> 720 lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 721 lisp_inv (LISP_MULT x1 x2, Sym "nil", Sym "nil",x4,x5,x6,limit) 722 (((w1 >>> 2) * (w2 >>> 2)) << 2 + 2w, 3w, 3w,w4,w5,w6,a,x,xs,s,rest)``, 723 SIMP_TAC std_ss [GSYM AND_IMP_INTRO,isVal_thm] 724 \\ STRIP_TAC THEN STRIP_TAC 725 \\ ASM_SIMP_TAC std_ss [getVal_def,LISP_MULT_def] 726 \\ REPEAT STRIP_TAC 727 \\ IMP_RES_TAC lisp_inv_swap2 728 \\ IMP_RES_TAC lisp_inv_read_Val 729 \\ FULL_SIMP_TAC std_ss [] 730 \\ `(n2w (4 * a' + 2) >>> 2 * n2w (4 * a'' + 2) >>> 2) << 2 + 2w:word32 = 731 n2w ((a' * a'') * 4 + 2)` suffices_by (STRIP_TAC THEN ASM_SIMP_TAC std_ss [] 732 \\ MATCH_MP_TAC lisp_inv_Val_nil_nil 733 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC []) 734 \\ IMP_RES_TAC LEMMA_MULT_4 735 \\ IMP_RES_TAC (SIMP_RULE (std_ss++SIZES_ss) [] (INST_TYPE [``:'a``|->``:32``] word_lsr_n2w)) 736 \\ ASM_SIMP_TAC std_ss [DIV_MULT] 737 \\ ONCE_REWRITE_TAC [MULT_COMM] 738 \\ ASM_SIMP_TAC std_ss [DIV_MULT,WORD_MUL_LSL,word_mul_n2w,word_add_n2w]); 739 740val LISP_DIV_MOD_LEMMA = prove( 741 ``!n. n < 1073741824 ==> (n2w (4 * n + 2) >>> 2 = (n2w n):word32)``, 742 REPEAT STRIP_TAC 743 \\ `4 * n + 2 < 4 * (n + 1)` by DECIDE_TAC 744 \\ `4 * (n + 1) <= 4 * 1073741824` by 745 (SIMP_TAC bool_ss [LE_MULT_LCANCEL] \\ DECIDE_TAC) 746 \\ IMP_RES_TAC LESS_LESS_EQ_TRANS 747 \\ FULL_SIMP_TAC std_ss [] 748 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_LSR_n2w] 749 \\ ONCE_REWRITE_TAC [MULT_COMM] 750 \\ SIMP_TAC std_ss [DIV_MULT]); 751 752val lisp_inv_DIV = store_thm("lisp_inv_DIV", 753 ``isVal x1 /\ isVal x2 /\ getVal x2 <> 0 ==> 754 lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 755 lisp_inv (LISP_DIV x1 x2, Sym "nil", Sym "nil",x4,x5,x6,limit) 756 (((w1 >>> 2) // (w2 >>> 2)) << 2 + 2w,3w,3w,w4,w5,w6,a,x,xs,s,rest) /\ 757 lisp_word_div_pre (w1,w2)``, 758 SIMP_TAC std_ss [GSYM AND_IMP_INTRO,isVal_thm] 759 \\ STRIP_TAC THEN STRIP_TAC 760 \\ ASM_SIMP_TAC std_ss [getVal_def,LISP_DIV_def] 761 \\ STRIP_TAC \\ STRIP_TAC 762 \\ IMP_RES_TAC lisp_inv_swap2 763 \\ IMP_RES_TAC lisp_inv_read_Val 764 \\ FULL_SIMP_TAC std_ss [] 765 \\ `(n2w (4 * a' + 2) >>> 2 // n2w (4 * a'' + 2) >>> 2) << 2 + 2w:word32 = 766 n2w ((a' DIV a'') * 4 + 2)` by 767 (IMP_RES_TAC LEMMA_MULT_4 768 \\ IMP_RES_TAC (SIMP_RULE (std_ss++SIZES_ss) [] (INST_TYPE [``:'a``|->``:32``] word_lsr_n2w)) 769 \\ ASM_SIMP_TAC std_ss [DIV_MULT] 770 \\ ONCE_REWRITE_TAC [MULT_COMM] 771 \\ ASM_SIMP_TAC std_ss [DIV_MULT,WORD_MUL_LSL,word_mul_n2w,word_add_n2w] 772 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_div_def,w2n_n2w,word_mul_n2w,word_add_n2w] 773 \\ `a'' < 4294967296 /\ a' < 4294967296` by DECIDE_TAC 774 \\ ASM_SIMP_TAC std_ss []) 775 \\ STRIP_TAC THEN1 776 (ASM_SIMP_TAC std_ss [] 777 \\ MATCH_MP_TAC lisp_inv_Val_nil_nil 778 \\ `0 < a''` by DECIDE_TAC 779 \\ IMP_RES_TAC DIV_LESS_EQ 780 \\ `a' <= 1073741823` by DECIDE_TAC 781 \\ `a' DIV a'' <= 1073741823` by METIS_TAC [LESS_EQ_TRANS] 782 \\ `a' DIV a'' < 1073741824` by DECIDE_TAC 783 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC []) 784 \\ SIMP_TAC std_ss [lisp_word_div_pre_def,LET_DEF] 785 \\ IMP_RES_TAC LISP_DIV_MOD_LEMMA 786 \\ `a' < 4294967296 /\ a'' < 4294967296` by DECIDE_TAC 787 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,n2w_11] 788 \\ DECIDE_TAC); 789 790val lisp_inv_MOD = store_thm("lisp_inv_MOD", 791 ``isVal x1 /\ isVal x2 /\ getVal x2 <> 0 ==> 792 lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 793 lisp_inv (LISP_MOD x1 x2, Sym "nil", Sym "nil",x4,x5,x6,limit) 794 ((word_mod (w1 >>> 2) (w2 >>> 2)) << 2 + 2w,3w,3w,w4,w5,w6,a,x,xs,s,rest) /\ 795 lisp_word_mod_pre (w1,w2)``, 796 SIMP_TAC std_ss [GSYM AND_IMP_INTRO,isVal_thm] 797 \\ STRIP_TAC THEN STRIP_TAC 798 \\ ASM_SIMP_TAC std_ss [getVal_def,LISP_MOD_def] 799 \\ STRIP_TAC \\ STRIP_TAC 800 \\ IMP_RES_TAC lisp_inv_swap2 801 \\ IMP_RES_TAC lisp_inv_read_Val 802 \\ FULL_SIMP_TAC std_ss [] 803 \\ `(word_mod (n2w (4 * a' + 2) >>> 2) (n2w (4 * a'' + 2) >>> 2)) << 2 + 2w:word32 = 804 n2w ((a' MOD a'') * 4 + 2)` by 805 (IMP_RES_TAC LEMMA_MULT_4 806 \\ IMP_RES_TAC (SIMP_RULE (std_ss++SIZES_ss) [] (INST_TYPE [``:'a``|->``:32``] word_lsr_n2w)) 807 \\ ASM_SIMP_TAC std_ss [DIV_MULT] 808 \\ ONCE_REWRITE_TAC [MULT_COMM] 809 \\ ASM_SIMP_TAC std_ss [DIV_MULT,WORD_MUL_LSL,word_mul_n2w,word_add_n2w] 810 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_mod_def,w2n_n2w,word_mul_n2w,word_add_n2w] 811 \\ `a'' < 4294967296 /\ a' < 4294967296` by DECIDE_TAC 812 \\ ASM_SIMP_TAC std_ss []) 813 \\ STRIP_TAC THEN1 814 (ASM_SIMP_TAC std_ss [] 815 \\ MATCH_MP_TAC lisp_inv_Val_nil_nil 816 \\ `0 < a''` by DECIDE_TAC 817 \\ IMP_RES_TAC MOD_LESS 818 \\ `a' MOD a'' < a''` by METIS_TAC [] 819 \\ `a' MOD a'' < 1073741824` by DECIDE_TAC 820 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC []) 821 \\ SIMP_TAC std_ss [lisp_word_mod_pre_def,LET_DEF] 822 \\ IMP_RES_TAC LISP_DIV_MOD_LEMMA 823 \\ `a' < 4294967296 /\ a'' < 4294967296` by DECIDE_TAC 824 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,n2w_11] 825 \\ DECIDE_TAC); 826 827val lisp_inv_LESS = store_thm("lisp_inv_LESS", 828 ``isVal x1 /\ isVal x2 ==> 829 lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest) ==> 830 (getVal x1 < getVal x2 <=> w1 <+ w2)``, 831 isVal_TAC \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [WORD_LO,w2n_n2w] 832 \\ `(4 * a'' + 2) < 4294967296 /\ (4 * a' + 2) < 4294967296` by DECIDE_TAC 833 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC); 834 835 836(* LDEPTH *) 837 838val word_tree_11 = prove( 839 ``!t a u d m. word_tree t (a,m) d ==> word_tree u (a,m) d ==> (t = u)``, 840 REVERSE (Induct_on `t`) 841 \\ Cases_on `u` \\ SIMP_TAC std_ss [word_tree_def,ALIGNED_INTRO] 842 \\ SIMP_TAC std_ss [ADDR32_NEQ_ADDR32,ALIGNED_ADDR32,ALIGNED_ADD_EQ] 843 \\ SIMP_TAC std_ss [ALIGNED_n2w,WORD_EQ_ADD_RCANCEL,ADDR32_11] 844 \\ SIMP_TAC std_ss [XExp_11] \\ METIS_TAC []); 845 846val word_tree_IMP_DELETE = prove( 847 ``!t a m d. word_tree t (a,m) d ==> ~(word_tree t (a,m) (d DELETE w)) ==> 848 ?u. word_tree u (w,m) d /\ XSIZE u <= XSIZE t``, 849 Induct \\ SIMP_TAC std_ss [word_tree_def] \\ REPEAT STRIP_TAC 850 \\ (Cases_on `a = w` THEN1 METIS_TAC [word_tree_def,LESS_EQ_TRANS,LESS_EQ_REFL]) 851 \\ FULL_SIMP_TAC std_ss [IN_DELETE,XSIZE_def] 852 \\ `XSIZE t <= SUC (XSIZE t + XSIZE t')` by DECIDE_TAC 853 \\ `XSIZE t' <= SUC (XSIZE t + XSIZE t')` by DECIDE_TAC 854 \\ METIS_TAC [word_tree_def,LESS_EQ_TRANS,LESS_EQ_REFL]); 855 856val word_tree_XDot_IMP = prove( 857 ``word_tree (XDot x y) (a,m) dm ==> 858 a IN dm /\ ALIGNED a /\ 859 word_tree x (m a,m) (dm DELETE a) /\ 860 word_tree y (m (a + 4w),m) (dm DELETE a)``, 861 STRIP_TAC 862 \\ `!u. word_tree u (a,m) dm ==> (XDot x y = u)` by METIS_TAC [word_tree_11] 863 \\ FULL_SIMP_TAC std_ss [word_tree_def] 864 \\ CCONTR_TAC \\ FULL_SIMP_TAC std_ss [] 865 \\ IMP_RES_TAC word_tree_IMP_DELETE 866 \\ `u = XDot x y` by METIS_TAC [] 867 \\ FULL_SIMP_TAC std_ss [XSIZE_def] \\ DECIDE_TAC); 868 869val word_tree_XDEPTH_LEMMA = prove( 870 ``!s t m a. 871 word_tree t (a,m) s /\ FINITE s ==> XDEPTH t <= CARD s``, 872 STRIP_TAC \\ Induct_on `CARD s` \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 873 \\ SIMP_TAC std_ss [] THEN1 874 (REPEAT STRIP_TAC \\ Cases_on `t` 875 \\ SIMP_TAC std_ss [XDEPTH_def] 876 \\ IMP_RES_TAC CARD_EQ_0 877 \\ FULL_SIMP_TAC std_ss [word_tree_def,NOT_IN_EMPTY]) 878 \\ REPEAT STRIP_TAC \\ REVERSE (Cases_on `t`) 879 \\ FULL_SIMP_TAC std_ss [XDEPTH_def,lisp_x_def] 880 \\ IMP_RES_TAC word_tree_XDot_IMP 881 \\ `(v = CARD (s DELETE (a:word32))) /\ FINITE (s DELETE a)` suffices_by 882 (STRIP_TAC THEN METIS_TAC []) 883 \\ IMP_RES_TAC CARD_DELETE 884 \\ ASM_SIMP_TAC std_ss [FINITE_DELETE]); 885 886val CARD_ch_active_set = prove( 887 ``!k i a. 888 (CARD (ch_active_set (a,i,i + k)) <= k) /\ 889 FINITE (ch_active_set (a,i,i + k))``, 890 Induct THENL [ 891 REPEAT STRIP_TAC 892 \\ `ch_active_set (a,i,i + 0) = {}` by 893 (FULL_SIMP_TAC std_ss [EXTENSION,ch_active_set_def,NOT_IN_EMPTY, 894 GSPECIFICATION] \\ DECIDE_TAC) 895 \\ ASM_SIMP_TAC std_ss [CARD_EMPTY,FINITE_EMPTY], 896 REPEAT STRIP_TAC 897 \\ `(ch_active_set (a,i,i + SUC k) = 898 (a + 8w * n2w i) INSERT ch_active_set (a,SUC i,SUC i + k))` by 899 (FULL_SIMP_TAC std_ss [EXTENSION,ch_active_set_def,NOT_IN_EMPTY, 900 GSPECIFICATION,IN_INSERT] 901 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 902 \\ ASM_SIMP_TAC std_ss [] THENL [ 903 Cases_on `i = j` \\ ASM_SIMP_TAC std_ss [] \\ DISJ2_TAC 904 \\ Q.EXISTS_TAC `j` \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC, 905 Q.EXISTS_TAC `i` \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC, 906 Q.EXISTS_TAC `j` \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC]) 907 \\ ASM_SIMP_TAC std_ss [CARD_INSERT,FINITE_INSERT] 908 \\ Cases_on `a + 8w * n2w i IN ch_active_set (a,SUC i,SUC i + k)` 909 \\ ASM_SIMP_TAC std_ss [CARD_INSERT,FINITE_INSERT] 910 \\ MATCH_MP_TAC LESS_EQ_TRANS 911 \\ Q.EXISTS_TAC `SUC (CARD (ch_active_set (a,SUC i,SUC i + k)))` 912 \\ ASM_SIMP_TAC std_ss []]); 913 914val word_tree_XDEPTH = prove( 915 ``!t a m w v i. 916 word_tree t (a,m) (ch_active_set (w,v,i)) /\ v <= i ==> XDEPTH t <= i - v``, 917 REPEAT STRIP_TAC 918 \\ STRIP_ASSUME_TAC (Q.SPECL [`(i - v)`,`v`,`w`] CARD_ch_active_set) 919 \\ `v + (i - v) = i` by DECIDE_TAC 920 \\ FULL_SIMP_TAC std_ss [] 921 \\ MATCH_MP_TAC LESS_EQ_TRANS 922 \\ Q.EXISTS_TAC `CARD (ch_active_set (w,v,i))` 923 \\ ASM_SIMP_TAC std_ss [] 924 \\ MATCH_MP_TAC word_tree_XDEPTH_LEMMA 925 \\ Q.EXISTS_TAC `m` \\ Q.EXISTS_TAC `a` 926 \\ ASM_SIMP_TAC std_ss []); 927 928val lisp_inv_LDEPTH_LEMMA = prove( 929 ``lisp_inv (x1,x2,x3,x4,x5,x6,l) (w1,w2,w3,w4,w5,w6,a,df,f,s,rest) ==> 930 LDEPTH x1 <= l``, 931 SIMP_TAC std_ss [lisp_inv_def,LET_DEF] \\ REPEAT STRIP_TAC 932 \\ Q.ABBREV_TAC `v = if u then 1 + l else 1` 933 \\ MATCH_MP_TAC LESS_EQ_TRANS 934 \\ Q.EXISTS_TAC `i - v` 935 \\ REVERSE STRIP_TAC THEN1 936 (Cases_on `u` \\ Q.UNABBREV_TAC `v` 937 \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC) 938 \\ (STRIP_ASSUME_TAC o UNDISCH o 939 Q.SPECL [`x1`,`w1`,`ch_active_set (a,v,i)`,`f`,`s`]) lisp_x_word_tree 940 \\ ASM_SIMP_TAC std_ss [] 941 \\ MATCH_MP_TAC word_tree_XDEPTH 942 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC []); 943 944val lisp_inv_LDEPTH = store_thm("lisp_inv_LDEPTH", 945 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,df,f,s,rest) ==> 946 LDEPTH x1 <= limit /\ LDEPTH x2 <= limit /\ LDEPTH x3 <= limit /\ 947 LDEPTH x4 <= limit /\ LDEPTH x5 <= limit /\ LDEPTH x6 <= limit``, 948 STRIP_TAC 949 \\ IMP_RES_TAC lisp_inv_swap2 950 \\ IMP_RES_TAC lisp_inv_swap3 951 \\ IMP_RES_TAC lisp_inv_swap4 952 \\ IMP_RES_TAC lisp_inv_swap5 953 \\ IMP_RES_TAC lisp_inv_swap6 954 \\ IMP_RES_TAC lisp_inv_LDEPTH_LEMMA \\ ASM_SIMP_TAC std_ss []); 955 956 957val _ = export_theory(); 958