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