1open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_print"; 2 3open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory; 4open compilerLib; 5 6open combinTheory finite_mapTheory addressTheory stringTheory helperLib;; 7open lisp_gcTheory; 8open lisp_typeTheory lisp_invTheory; 9open set_sepTheory; 10open divideTheory; 11open lisp_parseTheory; 12 13open decompilerLib prog_armLib prog_ppcLib prog_x86Lib; 14 15val decompile_arm = decompile prog_armLib.arm_tools; 16val decompile_ppc = decompile prog_ppcLib.ppc_tools; 17val decompile_x86 = decompile prog_x86Lib.x86_tools; 18 19 20infix \\ 21val op \\ = op THEN; 22val RW = REWRITE_RULE; 23val RW1 = ONCE_REWRITE_RULE; 24 25 26 27(* setting up the compiler *) 28val _ = codegen_x86Lib.set_x86_regs 29 [(3,"eax"),(4,"ecx"),(5,"edx"),(6,"ebx"),(7,"edi"),(8,"esi"),(9,"ebp")] 30 31 32(* teach the compiler to compile ``let r4 = r4 * 10w in`` *) 33 34val (x86_10_th,x86_10_def) = decompile_x86 "x86_10" ` 35 01C9 36 8D0C89`; 37 38val x86_10_lemma = prove( 39 ``!w. x86_10 w = w * 10w``, 40 SIMP_TAC (std_ss++SIZES_ss) [x86_10_def,LET_DEF,w2n_n2w] 41 THEN SIMP_TAC (std_ss++wordsLib.WORD_ss) []); 42 43val (arm_10_th,arm_10_def,_) = compile "arm" `` 44 arm_10 r4 = let r2 = 10w in 45 let r4 = r4 * r2 in r4:word32`` 46 47val (ppc_10_th,ppc_10_def,_) = compile "ppc" `` 48 ppc_10 r4 = let r4 = r4 * 10w in r4:word32`` 49 50val x86_10_thm = SIMP_RULE std_ss [LET_DEF,x86_10_lemma] x86_10_th 51val ppc_10_thm = SIMP_RULE std_ss [LET_DEF,ppc_10_def] ppc_10_th 52val arm_10_thm = SIMP_RULE std_ss [LET_DEF,arm_10_def] arm_10_th 53 54val _ = codegenLib.add_compiled [x86_10_thm,ppc_10_thm,arm_10_thm] 55 56 57(* reverse a string *) 58 59val (thms,arm_str_rev_def,arm_str_rev_pre_def) = compile_all `` 60 arm_string_rev(r3:word32,r6,r7,df:word32 set,f:word32->word8) = 61 if r3 = 0w then (r7,df,f) else 62 let r4 = (w2w (f r6)):word32 in 63 let r5 = (w2w (f r7)):word32 in 64 let f = (r6 =+ w2w r5) f in 65 let f = (r7 =+ w2w r4) f in 66 let r6 = r6 - 1w in 67 let r7 = r7 + 1w in 68 let r3 = r3 - 1w in 69 arm_string_rev(r3,r6,r7,df,f)`` 70 71val (thms,arm_str_reverse_def,arm_str_reverse_pre_def) = compile_all `` 72 arm_string_reverse1(r6,r7,df:word32 set,f:word32->word8) = 73 let r3 = r7 - r6 in 74 let r3 = r3 >>> 1 in 75 let r6 = r6 + r3 in 76 let r6 = r6 - 1w in 77 let r7 = r7 - r3 in 78 let (r7,df,f) = arm_string_rev(r3,r6,r7,df,f) in 79 (r7,df,f)`` 80 81val one_list_def = Define ` 82 (one_list a [] b = cond (b = a)) /\ 83 (one_list a (x::xs) b = one (a,x) * one_list (a + 1w) xs b)`; 84 85val one_space_def = Define ` 86 (one_space a 0 b = cond (b = a)) /\ 87 (one_space a (SUC n) b = SEP_EXISTS y. one (a,y) * one_space (a + 1w) n b)`; 88 89val one_string_def = Define ` 90 one_string a (s:string) b = one_list a (MAP (n2w o ORD) s) b`; 91 92val one_list_SNOC = prove( 93 ``!a xs x b. one_list a (xs ++ [x]) b = 94 one_list a xs (b - 1w) * one (b - 1w, x)``, 95 Induct_on `xs` 96 \\ ASM_REWRITE_TAC [one_list_def,APPEND,cond_STAR,FUN_EQ_THM,STAR_ASSOC] 97 \\ REWRITE_TAC [WORD_EQ_SUB_RADD] \\ METIS_TAC [WORD_ADD_SUB]); 98 99val w2w_w2w_lemma = prove( 100 ``!x. w2w ((w2w x):word32) = x:word8``, 101 Cases_word 102 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 103 \\ `n < 4294967296` by DECIDE_TAC 104 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w]); 105 106val arm_string_rev_lemma = prove( 107 ``!ys xs r6 r7 r6i r7i f p. 108 (p * one_list r6i xs (r6 + 1w) * one_list r7 ys r7i) (fun2set (f,df)) /\ 109 (LENGTH xs = LENGTH ys) /\ LENGTH ys < 2 ** 32 ==> 110 ?fi. arm_string_rev_pre (n2w (LENGTH ys),r6,r7,df,f) /\ 111 (arm_string_rev (n2w (LENGTH ys),r6,r7,df,f) = (r7i,df,fi)) /\ 112 (p * one_list r6i (REVERSE ys) (r6 + 1w) * 113 one_list r7 (REVERSE xs) r7i) (fun2set (fi,df))``, 114 Induct THEN1 115 (Cases \\ SIMP_TAC std_ss [LENGTH, DECIDE ``~(SUC n = 0:num)``] 116 \\ SIMP_TAC std_ss [REVERSE_DEF,one_list_def,cond_STAR,LENGTH] 117 \\ ONCE_REWRITE_TAC [arm_str_rev_def,arm_str_rev_pre_def] 118 \\ SIMP_TAC std_ss []) 119 \\ NTAC 8 STRIP_TAC 120 \\ STRIP_ASSUME_TAC (Q.ISPEC `xs:word8 list` rich_listTheory.SNOC_CASES) 121 \\ FULL_SIMP_TAC std_ss [LENGTH, DECIDE ``~(SUC n = 0:num)``] 122 \\ REWRITE_TAC [rich_listTheory.SNOC_APPEND,REVERSE_APPEND,REVERSE_DEF] 123 \\ REWRITE_TAC [APPEND,one_list_def,STAR_ASSOC,LENGTH_APPEND,LENGTH] 124 \\ REWRITE_TAC [DECIDE ``(m + SUC 0 = SUC n) = (m = n:num)``] 125 \\ SIMP_TAC std_ss [one_list_SNOC,WORD_ADD_SUB,STAR_ASSOC] 126 \\ POP_ASSUM (K ALL_TAC) \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `l`) 127 \\ REPEAT STRIP_TAC \\ `LENGTH ys < 4294967296` by DECIDE_TAC 128 \\ FULL_SIMP_TAC std_ss [] 129 \\ ONCE_REWRITE_TAC [arm_str_rev_def,arm_str_rev_pre_def] 130 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,n2w_11,DECIDE ``~(SUC n = 0:num)``] 131 \\ REWRITE_TAC [w2w_w2w_lemma,ADD1,GSYM word_add_n2w,WORD_ADD_SUB] 132 \\ `(f r6 = x) /\ r6 IN df` by SEP_READ_TAC 133 \\ `(f r7 = h) /\ r7 IN df` by SEP_READ_TAC 134 \\ ASM_SIMP_TAC std_ss [] 135 \\ Q.ABBREV_TAC `f2 = (r7 =+ x) ((r6 =+ h) f)` 136 \\ `(p * one (r6,h) * one (r7,x) * one_list r6i l (r6 - 1w + 1w) * 137 one_list (r7 + 0x1w) ys r7i) (fun2set (f2,df))` by 138 (REWRITE_TAC [WORD_SUB_ADD] \\ Q.UNABBREV_TAC `f2` \\ SEP_WRITE_TAC) 139 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [] 140 \\ FULL_SIMP_TAC (std_ss++star_ss) [WORD_SUB_ADD]) 141 142val one_list_LENGTH = prove( 143 ``!xs p r6 r7. (p * one_list r6 xs r7) (fun2set (f,df)) ==> 144 (r7 - r6 = n2w (LENGTH xs))``, 145 Induct 146 \\ SIMP_TAC std_ss [LENGTH,one_list_def,cond_STAR,WORD_SUB_REFL] 147 \\ REPEAT STRIP_TAC 148 \\ `!n. (r7 - r6 = n2w (SUC n)) = (r7 - (r6 + 1w) = n2w n)` by 149 (ONCE_REWRITE_TAC [GSYM WORD_EQ_SUB_ZERO] 150 \\ SIMP_TAC std_ss [ADD1,GSYM word_add_n2w,WORD_SUB_PLUS] 151 \\ SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC, word_sub_def]) 152 \\ ASM_SIMP_TAC std_ss [] 153 \\ POP_ASSUM (K ALL_TAC) 154 \\ Q.PAT_X_ASSUM `!p. bbb` MATCH_MP_TAC 155 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC] \\ METIS_TAC []); 156 157val SPLIT_LIST_MIDDLE = prove( 158 ``!xs:'a list. 159 ?ys qs zs. (xs = ys ++ qs ++ zs) /\ ((LENGTH xs) DIV 2 = LENGTH ys) /\ 160 (LENGTH zs = LENGTH ys) /\ LENGTH qs < 2``, 161 STRIP_TAC 162 \\ Q.EXISTS_TAC `TAKE ((LENGTH xs) DIV 2) xs` 163 \\ Q.EXISTS_TAC `TAKE ((LENGTH xs) - (LENGTH xs) DIV 2 * 2) (DROP ((LENGTH xs) DIV 2) xs)` 164 \\ Q.EXISTS_TAC `DROP ((LENGTH xs) - (LENGTH xs) DIV 2 * 2) (DROP ((LENGTH xs) DIV 2) xs)` 165 \\ REWRITE_TAC [TAKE_DROP] 166 \\ (ASSUME_TAC o Q.SPEC `LENGTH (xs:'a list)` o MATCH_MP (GSYM DIVISION)) (DECIDE ``0 < 2:num``) 167 \\ `LENGTH xs DIV 2 <= LENGTH xs` by DECIDE_TAC 168 \\ `LENGTH xs - LENGTH xs DIV 2 * 2 = LENGTH xs MOD 2` by DECIDE_TAC 169 \\ ASM_SIMP_TAC std_ss [TAKE_DROP, GSYM APPEND_ASSOC] 170 \\ IMP_RES_TAC LENGTH_TAKE \\ ASM_SIMP_TAC std_ss [LENGTH_DROP] 171 \\ STRIP_TAC THEN1 DECIDE_TAC 172 \\ Cases_on `LENGTH xs MOD 2` THEN1 ASM_SIMP_TAC std_ss [rich_listTheory.FIRSTN,LENGTH] 173 \\ Tactical.REVERSE (Cases_on `n`) THEN1 (`F` by DECIDE_TAC) 174 \\ Cases_on `DROP (LENGTH xs DIV 2) xs` \\ EVAL_TAC); 175 176val one_list_APPEND = prove( 177 ``!xs ys a b. one_list a (xs ++ ys) b = 178 one_list a xs (a + n2w (LENGTH xs)) * 179 one_list (a + n2w (LENGTH xs)) ys b``, 180 Induct 181 \\ ASM_REWRITE_TAC [one_list_def,APPEND,LENGTH,WORD_ADD_0,SEP_CLAUSES] 182 \\ REWRITE_TAC [GSYM WORD_ADD_ASSOC, word_add_n2w, ADD1] 183 \\ SIMP_TAC (std_ss++star_ss) [AC ADD_ASSOC ADD_COMM]); 184 185val arm_string_rev_lemma = prove( 186 ``!xs r6 r7 f p. 187 (p * one_list r6 xs r7) (fun2set (f,df)) /\ LENGTH xs < 2 ** 32 ==> 188 ?fi. arm_string_reverse1_pre (r6,r7,df,f) /\ 189 (arm_string_reverse1 (r6,r7,df,f) = (r7,df,fi)) /\ 190 (p * one_list r6 (REVERSE xs) r7) (fun2set (fi,df))``, 191 REWRITE_TAC [arm_str_reverse_def,arm_str_reverse_pre_def] 192 \\ SIMP_TAC std_ss [LET_DEF,EVAL ``w2n (1w:word32)``] 193 \\ REPEAT STRIP_TAC 194 \\ IMP_RES_TAC one_list_LENGTH 195 \\ `LENGTH xs < dimword (:32)` by (ASM_SIMP_TAC (std_ss++SIZES_ss) []) 196 \\ IMP_RES_TAC word_LSR_n2w 197 \\ ASM_SIMP_TAC std_ss [] 198 \\ STRIP_ASSUME_TAC (ISPEC ``xs:word8 list`` SPLIT_LIST_MIDDLE) 199 \\ Q.PAT_X_ASSUM `LENGTH xs DIV 2 = LENGTH ys` (fn th => REWRITE_TAC [th]) 200 \\ FULL_SIMP_TAC std_ss [REVERSE_APPEND] 201 \\ `REVERSE qs = qs` by 202 (Cases_on `qs` \\ FULL_SIMP_TAC std_ss [LENGTH,REVERSE_DEF] 203 \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [LENGTH,REVERSE_DEF,APPEND] 204 \\ `F` by DECIDE_TAC) 205 \\ `LENGTH zs < 2**32 /\ (LENGTH ys = LENGTH zs)` by 206 (FULL_SIMP_TAC std_ss [LENGTH_APPEND] \\ DECIDE_TAC) 207 \\ FULL_SIMP_TAC bool_ss [one_list_APPEND,STAR_ASSOC,LENGTH_APPEND, 208 rich_listTheory.LENGTH_REVERSE,WORD_ADD_ASSOC] 209 \\ `r7 - n2w (LENGTH ys) = r6 + n2w (LENGTH ys + LENGTH qs)` by 210 FULL_SIMP_TAC bool_ss [WORD_EQ_SUB_RADD,GSYM word_add_n2w, 211 AC WORD_ADD_COMM WORD_ADD_ASSOC] 212 \\ ASM_SIMP_TAC bool_ss [] 213 \\ `((p * one_list (r6 + n2w (LENGTH ys)) qs (r6 + n2w (LENGTH ys) + n2w (LENGTH qs))) * 214 one_list r6 ys (r6 + n2w (LENGTH ys) - 1w + 1w) * 215 one_list (r7 - n2w (LENGTH ys)) zs r7) 216 (fun2set (f,df))` by 217 FULL_SIMP_TAC (std_ss++star_ss) [WORD_SUB_ADD,GSYM word_add_n2w, WORD_ADD_ASSOC] 218 \\ IMP_RES_TAC arm_string_rev_lemma 219 \\ Q.PAT_X_ASSUM `r7 - n2w (LENGTH ys) = r6 + n2w (LENGTH ys + LENGTH qs)` ASSUME_TAC 220 \\ Q.PAT_X_ASSUM `LENGTH ys = LENGTH zs` (ASSUME_TAC o GSYM) 221 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w] 222 \\ FULL_SIMP_TAC std_ss [WORD_ADD_SUB,WORD_SUB_ADD] 223 \\ FULL_SIMP_TAC (std_ss++star_ss) [AC WORD_ADD_COMM WORD_ADD_ASSOC]); 224 225 226(* print a number reversed *) 227 228val _ = codegenLib.add_compiled [arm_div_mod_thm,x86_div_mod_thm,ppc_div_mod_thm]; 229 230val (thms,arm_str2num_def,arm_str2num_pre_def) = compile_all `` 231 arm_str2num1(r3:word32,r4,r7,df:word32 set,f:word32->word8) = 232 let (r3,r5) = (r3 // r4, word_mod r3 r4) in 233 let r5 = r5 + 48w in 234 let f = (r7 =+ w2w r5) f in 235 let r7 = r7 + 1w in 236 if r3 = 0w then (r7,f,df) else 237 arm_str2num1(r3,r4,r7,df,f)`` 238 239val arm_str2num_lemma = prove( 240 ``!n r7 a f p. 241 (p * one_space r7 (LENGTH (num2str n)) a) (fun2set (f,df)) /\ n < 2 ** 31 ==> 242 ?fi. arm_str2num1_pre (n2w n,10w,r7,df,f) /\ 243 (arm_str2num1 (n2w n,10w,r7,df,f) = (a,fi,df)) /\ 244 (p * one_string r7 (REVERSE (num2str n)) a) (fun2set (fi,df))``, 245 completeInduct_on `n` 246 \\ ONCE_REWRITE_TAC [arm_str2num_def,arm_str2num_pre_def] 247 \\ SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,n2w_11,w2n_n2w] 248 \\ REPEAT STRIP_TAC 249 \\ `n < 4294967296` by DECIDE_TAC 250 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,n2w_11,w2n_n2w,word_mod_def,word_div_def,word_add_n2w] 251 \\ `(n DIV 10) < 4294967296` by (ASM_SIMP_TAC std_ss [DIV_LT_X] \\ DECIDE_TAC) 252 \\ ASM_SIMP_TAC std_ss [] 253 \\ `w2w ((n2w (n MOD 10 + 48)):word32) = n2w (ORD (CHR (n MOD 10 + 48))):word8` by 254 (`n MOD 10 < 10` by (MATCH_MP_TAC MOD_LESS THEN SIMP_TAC std_ss []) 255 \\ `n MOD 10 + 48 < 256 /\ n MOD 10 + 48 < 4294967296` by DECIDE_TAC 256 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [ORD_CHR,w2w_def,n2w_w2n,w2n_n2w]) 257 \\ ASM_SIMP_TAC std_ss [] 258 \\ Cases_on `n < 10` THEN1 259 (IMP_RES_TAC LESS_DIV_EQ_ZERO \\ ASM_SIMP_TAC std_ss [] 260 \\ `num2str n = [CHR (n + 48)]` by 261 (ONCE_REWRITE_TAC [num2str_def] \\ ASM_SIMP_TAC std_ss [dec2str_def]) 262 \\ FULL_SIMP_TAC bool_ss [LENGTH,one_space_def,SEP_CLAUSES,one_string_def] 263 \\ FULL_SIMP_TAC bool_ss [SEP_EXISTS,cond_STAR,STAR_ASSOC,MAP,REVERSE_DEF,APPEND] 264 \\ FULL_SIMP_TAC std_ss [one_list_def,SEP_CLAUSES] 265 \\ `(f r7 = y) /\ r7 IN df` by SEP_READ_TAC 266 \\ ASM_SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 267 \\ `~(n DIV 10 < 1)` by ASM_SIMP_TAC std_ss [DIV_LT_X] 268 \\ FULL_SIMP_TAC std_ss [DECIDE ``n < 1 = (n = 0:num)``] 269 \\ `(n DIV 10 < n)` by (ASM_SIMP_TAC std_ss [DIV_LT_X] THEN DECIDE_TAC) 270 \\ Q.PAT_X_ASSUM `!m. bbb` (ASSUME_TAC o UNDISCH o Q.SPEC `n DIV 10`) 271 \\ `n DIV 10 < 2147483648` by DECIDE_TAC 272 \\ FULL_SIMP_TAC std_ss [] 273 \\ `num2str n = STRCAT (num2str (n DIV 10)) (dec2str (n MOD 10))` by METIS_TAC [num2str_def] 274 \\ FULL_SIMP_TAC std_ss [dec2str_def,REVERSE_APPEND,APPEND,REVERSE_DEF, 275 LENGTH_APPEND,LENGTH,GSYM ADD1,one_space_def] 276 \\ FULL_SIMP_TAC bool_ss [LENGTH,one_space_def,SEP_CLAUSES,one_string_def] 277 \\ FULL_SIMP_TAC bool_ss [SEP_EXISTS,cond_STAR,STAR_ASSOC,MAP,REVERSE_DEF,APPEND] 278 \\ FULL_SIMP_TAC std_ss [one_list_def,SEP_CLAUSES] 279 \\ ` ((p * one (r7,n2w (ORD (CHR (n MOD 10 + 48))))) * 280 one_space (r7 + 0x1w) (STRLEN (num2str (n DIV 10))) a) 281 (fun2set ((r7 =+ n2w (ORD (CHR (n MOD 10 + 48)))) f,df))` by SEP_WRITE_TAC 282 \\ `(f r7 = y) /\ r7 IN df` by SEP_READ_TAC 283 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [STAR_ASSOC]); 284 285 286(* printing a number properly *) 287 288val (thms,arm_print_num_def,arm_print_num_pre_def) = compile_all `` 289 arm_print_num(r3:word32,r7,df:word32 set,f:word32->word8) = 290 let r3 = r3 >>> 2 in 291 let r4 = 10w:word32 in 292 let r6 = r7:word32 in 293 let (r7,f,df) = arm_str2num1(r3,r4,r7,df,f) in 294 let (r7,df,f) = arm_string_reverse1(r6,r7,df,f) in 295 (r7,f,df)``; 296 297val LENGTH_num2str = prove( 298 ``!n. 0 < n ==> LENGTH (num2str n) <= n``, 299 completeInduct_on `n` \\ Cases_on `n < 10` THEN1 300 (ONCE_REWRITE_TAC [num2str_def] 301 \\ IMP_RES_TAC LESS_DIV_EQ_ZERO 302 \\ ASM_SIMP_TAC std_ss [dec2str_def,LENGTH] 303 \\ DECIDE_TAC) 304 \\ `~(n DIV 10 < 1)` by ASM_SIMP_TAC std_ss [DIV_LT_X] 305 \\ FULL_SIMP_TAC std_ss [DECIDE ``n < 1 = (n = 0:num)``] 306 \\ ONCE_REWRITE_TAC [num2str_def] 307 \\ ASM_SIMP_TAC std_ss [LENGTH_APPEND,APPEND,dec2str_def,LENGTH] 308 \\ FULL_SIMP_TAC std_ss [DECIDE ``(n <> 0) = 0 < n:num``] 309 \\ REPEAT STRIP_TAC 310 \\ `(n DIV 10 < n)` by (ASM_SIMP_TAC std_ss [DIV_LT_X] THEN DECIDE_TAC) 311 \\ `STRLEN (num2str (n DIV 10)) <= n DIV 10` by METIS_TAC [] 312 \\ ASSUME_TAC (Q.SPEC `n` (MATCH_MP DIVISION (DECIDE ``0 < 10:num``))) 313 \\ DECIDE_TAC); 314 315val arm_print_num_lemma = prove( 316 ``!n r7 a f p. 317 (p * one_space r7 (LENGTH (num2str n)) a) (fun2set (f,df)) /\ n < 2 ** 30 ==> 318 ?fi. arm_print_num_pre (n2w (4 * n + 2),r7,df,f) /\ 319 (arm_print_num (n2w (4 * n + 2),r7,df,f) = (a,fi,df)) /\ 320 (p * one_string r7 (num2str n) a) (fun2set (fi,df))``, 321 REWRITE_TAC [arm_print_num_def,arm_print_num_pre_def] 322 \\ SIMP_TAC std_ss [LET_DEF] 323 \\ REPEAT STRIP_TAC 324 \\ `4 * n + 2 < dimword (:32)` by (SIMP_TAC (std_ss++SIZES_ss) [] \\ DECIDE_TAC) 325 \\ IMP_RES_TAC word_LSR_n2w 326 \\ ASM_SIMP_TAC std_ss [] 327 \\ ONCE_REWRITE_TAC [MULT_COMM] 328 \\ SIMP_TAC std_ss [DIV_MULT] 329 \\ `n < 2**31` by (SIMP_TAC std_ss [] \\ DECIDE_TAC) 330 \\ IMP_RES_TAC arm_str2num_lemma 331 \\ ASM_SIMP_TAC std_ss [] 332 \\ FULL_SIMP_TAC std_ss [one_string_def] 333 \\ `LENGTH (MAP (n2w o ORD) (REVERSE (num2str n))) < 2**32 /\ 334 LENGTH (MAP ((n2w:num->word8) o ORD) (REVERSE (num2str n))) < 2**32` suffices_by 335 (STRIP_TAC THEN IMP_RES_TAC arm_string_rev_lemma 336 \\ FULL_SIMP_TAC std_ss [rich_listTheory.MAP_REVERSE,REVERSE_REVERSE]) 337 \\ REWRITE_TAC [LENGTH_MAP,rich_listTheory.LENGTH_REVERSE] 338 \\ Cases_on `n = 0` THEN1 (ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 339 \\ MATCH_MP_TAC LESS_EQ_LESS_TRANS 340 \\ Q.EXISTS_TAC `n` 341 \\ FULL_SIMP_TAC std_ss [LENGTH_num2str,DECIDE ``n <> 0 = 0 < n:num``] 342 \\ DECIDE_TAC) 343 344 345(* copy a string *) 346 347val (thms,arm_string_copy_def,arm_string_copy_pre_def) = compile_all `` 348 arm_string_copy (r5,r6,r7,dg:word32 set,g:word32->word8,df:word32 set,f:word32->word8) = 349 if r5 = 0w:word32 then (r7,dg,g,f,df) else 350 let r3 = (w2w (g r6)):word32 in 351 let r6 = r6 + 1w in 352 let f = (r7 =+ w2w r3) f in 353 let r7 = r7 + 1w in 354 let r5 = r5 - 1w in 355 arm_string_copy (r5,r6,r7,dg,g,df,f)`` 356 357val arm_string_copy_lemma = prove( 358 ``!s r6 r7 f p. 359 string_mem s (r6,g,dg) /\ 360 (p * one_space r7 (LENGTH s) a) (fun2set (f,df)) /\ LENGTH s < 2 ** 32 ==> 361 ?fi. arm_string_copy_pre (n2w (LENGTH s),r6,r7,dg,g,df,f) /\ 362 (arm_string_copy (n2w (LENGTH s),r6,r7,dg,g,df,f) = (a,dg,g,fi,df)) /\ 363 (p * one_string r7 s a) (fun2set (fi,df))``, 364 Induct \\ ONCE_REWRITE_TAC [arm_string_copy_def,arm_string_copy_pre_def] 365 \\ SIMP_TAC std_ss [one_string_def,one_list_def,LENGTH,one_space_def,MAP,cond_STAR] 366 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11,DECIDE ``~(SUC n = 0:num)``,LET_DEF] 367 \\ SIMP_TAC std_ss [ADD1,GSYM word_add_n2w,WORD_ADD_SUB,string_mem_def,w2w_w2w_lemma] 368 \\ SIMP_TAC std_ss [STAR_ASSOC,SEP_CLAUSES] 369 \\ SIMP_TAC std_ss [SEP_EXISTS] 370 \\ REPEAT STRIP_TAC 371 \\ `STRLEN s < 4294967296` by DECIDE_TAC 372 \\ FULL_SIMP_TAC std_ss [] 373 \\ `(p * one (r7, n2w (ORD h)) * one_space (r7 + 0x1w) (STRLEN s) a) 374 (fun2set ((r7 =+ n2w (ORD h)) f,df))` by SEP_WRITE_TAC 375 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [] 376 \\ `(f r7 = y) /\ r7 IN df` by SEP_READ_TAC 377 \\ FULL_SIMP_TAC (std_ss++star_ss) [one_string_def]); 378 379 380(* printing a symbol *) 381 382val (thms,arm_copy_symbol_def,arm_copy_symbol_pre_def) = compile_all `` 383 arm_copy_symbol (r3,r7,dm:word32 set,m:word32->word32,dg:word32 set,g:word32->word8,df:word32 set,f:word32->word8) = 384 let r5 = m (r3 - 3w) in (* length *) 385 let r6 = r3 + 5w in (* init pointer *) 386 let (r7,dg,g,f,df) = arm_string_copy (r5,r6,r7,dg,g,df,f) in 387 (r7,dm,m,dg,g,df,f)`` 388 389val symbol_table_IMP = prove( 390 ``!xs a w sym. 391 (a + w - 0x3w,s) IN sym /\ 392 symbol_table xs sym (a,dm,m,dg,g) /\ ALL_DISTINCT xs ==> 393 (m (a + w - 0x3w) = n2w (STRLEN s)) /\ (a + w - 0x3w) IN dm /\ 394 string_mem s (a + w + 0x5w,g,dg)``, 395 Induct THEN1 396 (SIMP_TAC std_ss [symbol_table_def,set_add_def,EXTENSION,FORALL_PROD, 397 NOT_IN_EMPTY] \\ SIMP_TAC std_ss [IN_DEF,set_add_def] 398 \\ METIS_TAC []) 399 \\ NTAC 5 STRIP_TAC 400 \\ FULL_SIMP_TAC std_ss [ALL_DISTINCT] 401 \\ FULL_SIMP_TAC std_ss [symbol_table_def,LET_DEF] 402 \\ REVERSE (Cases_on `h = s`) THENL [ 403 Q.ABBREV_TAC `a2 = a + n2w (8 + (STRLEN h + 3) DIV 4 * 4)` 404 \\ Q.PAT_X_ASSUM `!a. bbb` (MP_TAC o Q.SPECL [`a2`,`(w + a) - a2`,`sym DELETE (a,h)`]) 405 \\ ASM_SIMP_TAC std_ss [WORD_SUB_ADD2] 406 \\ FULL_SIMP_TAC std_ss [IN_DELETE,AC WORD_ADD_COMM WORD_ADD_ASSOC], 407 Cases_on `(a + w - 0x3w,s) IN sym DELETE (a,h)` 408 THEN1 (IMP_RES_TAC symbol_table_MEM \\ METIS_TAC []) 409 \\ POP_ASSUM MP_TAC 410 \\ ASM_SIMP_TAC std_ss [IN_DELETE] 411 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 412 \\ SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,WORD_ADD_SUB_ASSOC] 413 \\ FULL_SIMP_TAC std_ss [WORD_EQ_SUB_ZERO,word_arith_lemma1,INSERT_SUBSET]]); 414 415val arm_copy_symbol_lemma = prove( 416 ``!r3 r7 r9 f p. 417 ALIGNED r9 /\ ALIGNED (r3 - 0x3w) /\ (r3 - 0x3w,s) IN sym /\ 418 lisp_symbol_table sym (r9,dm,m,dg,g) /\ STRLEN s < 2**32 /\ 419 (p * one_space r7 (LENGTH s) a) (fun2set (f,df)) ==> 420 ?fi. arm_copy_symbol_pre (r3 + r9,r7,dm,m,dg,g,df,f) /\ 421 (arm_copy_symbol (r3 + r9,r7,dm,m,dg,g,df,f) = (a,dm,m,dg,g,df,fi)) /\ 422 (p * one_string r7 s a) (fun2set (fi,df))``, 423 SIMP_TAC std_ss [lisp_symbol_table_def] \\ REPEAT STRIP_TAC 424 \\ REPEAT (POP_ASSUM MP_TAC) 425 \\ Q.SPEC_TAC (`builtin_symbols ++ symbols`,`xs`) 426 \\ REPEAT STRIP_TAC 427 \\ `(r9 + r3 - 0x3w,s) IN (set_add r9 sym)` by 428 (SIMP_TAC std_ss [IN_DEF,set_add_def,WORD_ADD_SUB_ASSOC] 429 \\ ONCE_REWRITE_TAC [WORD_ADD_COMM] 430 \\ FULL_SIMP_TAC std_ss [WORD_SUB_ADD,IN_DEF]) 431 \\ IMP_RES_TAC symbol_table_IMP 432 \\ ASM_SIMP_TAC std_ss [arm_copy_symbol_def,arm_copy_symbol_pre_def,LET_DEF] 433 \\ ONCE_REWRITE_TAC [WORD_ADD_COMM] 434 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED_ADD_EQ,WORD_ADD_SUB_ASSOC] 435 \\ `?fi. arm_string_copy_pre (n2w (STRLEN s),r9 + r3 + 0x5w,r7,dg,g,df,f) /\ 436 (arm_string_copy (n2w (STRLEN s),r9 + r3 + 0x5w,r7,dg,g,df,f) = 437 (a,dg,g,fi,df)) /\ (p * one_string r7 s a) (fun2set (fi,df))` 438 by METIS_TAC [SIMP_RULE std_ss [] arm_string_copy_lemma] 439 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM]); 440 441 442 443(* lisp_inv ==> lisp_tree *) 444 445val lisp_tree_def = Define ` 446 (lisp_tree (Val k) (a,dm,m) sym = (a = n2w (k * 4 + 2)) /\ k < 2 ** 30) /\ 447 (lisp_tree (Sym s) (a,dm,m) sym = ALIGNED (a - 3w) /\ (a - 3w,s) IN sym) /\ 448 (lisp_tree (Dot x y) (a,dm,m) sym = a IN dm /\ (a + 4w) IN dm /\ ALIGNED a /\ 449 lisp_tree x (m a,dm,m) sym /\ lisp_tree y (m (a+4w),dm,m) sym)`; 450 451val lisp_x_IMP_lisp_tree = prove( 452 ``!t w a i n sym. 453 lisp_x t (w,ch_active_set (a,i,n),m) sym ==> 454 lisp_tree t (w,ch_active_set2 (a,i,n),m) sym``, 455 Induct \\ SIMP_TAC std_ss [lisp_tree_def,lisp_x_def,ALIGNED_INTRO] 456 \\ REVERSE (REPEAT STRIP_TAC) 457 THEN1 METIS_TAC [] THEN1 METIS_TAC [] 458 \\ ASM_SIMP_TAC std_ss [ch_active_set2_def,IN_UNION] 459 \\ DISJ2_TAC 460 \\ FULL_SIMP_TAC std_ss [ch_active_set_def,GSPECIFICATION] 461 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,WORD_EQ_ADD_CANCEL] 462 \\ SIMP_TAC std_ss [word_mul_n2w,word_add_n2w] 463 \\ Q.EXISTS_TAC `j` \\ ASM_SIMP_TAC std_ss []); 464 465val lisp_inv_IMP_lisp_tree = prove( 466 ``lisp_inv (t1,t2,t3,t4,t5,t6,l) (w1,w2,w3,w4,w5,w6,a,dm,m,sym,rest) ==> 467 ?i n. lisp_tree t1 (w1,ch_active_set2 (a,i,n),m) sym /\ 468 0 < i /\ i <= n /\ n <= i + l``, 469 SIMP_TAC std_ss [lisp_inv_def,LET_DEF] \\ REPEAT STRIP_TAC 470 \\ Q.EXISTS_TAC `if u then 1 + l else 1` 471 \\ Q.EXISTS_TAC `i` \\ STRIP_TAC 472 THEN1 (MATCH_MP_TAC lisp_x_IMP_lisp_tree \\ ASM_SIMP_TAC std_ss []) 473 \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC); 474 475 476(* testing isQuote *) 477 478val lisp_symbol_table_consts = prove( 479 ``!sym a dm m dg g. 480 lisp_symbol_table sym (a,rest) ==> 481 ((w - 3w, "nil") IN sym ==> (w = 3w)) /\ 482 ((w - 3w, "quote") IN sym ==> (w = 27w))``, 483 REPEAT STRIP_TAC 484 \\ IMP_RES_TAC builti_symbols_thm THENL [ 485 `w - 3w = ADDR32 0w` by METIS_TAC [lisp_symbol_table_11] 486 \\ FULL_SIMP_TAC std_ss [WORD_EQ_SUB_RADD] \\ EVAL_TAC, 487 `w - 3w = ADDR32 6w` by METIS_TAC [lisp_symbol_table_11] 488 \\ FULL_SIMP_TAC std_ss [WORD_EQ_SUB_RADD] \\ EVAL_TAC]); 489 490val (thms,arm_is_quote_def,arm_is_quote_pre_def) = compile_all `` 491 arm_is_quote (r3:word32,r4:word32,dh:word32 set,h:word32->word32) = 492 if r4 && 2w = 0w then (let r5 = 0w in (r3,r4,r5,dh,h)) else 493 let r5 = h r3 in 494 let r6 = h (r3 + 4w) in 495 if ~(r5 = 27w) then (let r5 = 0w in (r3,r4,r5,dh,h)) else 496 if ~(r6 && 3w = 0w) then (let r5 = 0w in (r3,r4,r5,dh,h)) else 497 let r5 = h (r6 + 4w) in 498 let r6 = h r6 in 499 if ~(r5 = 3w) then (let r5 = 0w in (r3,r4,r5,dh,h)) else 500 let r3 = r6 in (r3,r4,r5,dh,h)``; 501 502val arm_is_quote_lemma = prove( 503 ``!x w v dh h. 504 lisp_symbol_table sym (a,rest) /\ 505 lisp_tree x (w,dh,h) sym /\ isDot x ==> 506 arm_is_quote_pre(w,v,dh,h) /\ 507 if isQuote x /\ ~(v && 2w = 0w) then 508 (arm_is_quote(w,v,dh,h) = (h (h (w + 4w)), v, 3w, dh,h)) /\ 509 lisp_tree (CAR (CDR x)) (h (h (w + 4w)),dh,h) sym 510 else 511 (arm_is_quote(w,v,dh,h) = (w, v, 0w, dh,h))``, 512 NTAC 6 STRIP_TAC \\ Cases_on `~(v && 2w = 0w) /\ isQuote x` THEN1 513 (FULL_SIMP_TAC std_ss [isQuote_thm,SExp_11,CAR_def,CDR_def] 514 \\ FULL_SIMP_TAC std_ss [lisp_tree_def] 515 \\ ONCE_REWRITE_TAC [arm_is_quote_def,arm_is_quote_pre_def] 516 \\ ASM_SIMP_TAC std_ss [LET_DEF,ALIGNED_INTRO] 517 \\ ONCE_REWRITE_TAC [ALIGNED_MOD_4] 518 \\ ASM_SIMP_TAC std_ss [WORD_ADD_0] 519 \\ IMP_RES_TAC lisp_symbol_table_consts 520 \\ ASM_SIMP_TAC std_ss []) 521 \\ ASM_SIMP_TAC std_ss [] 522 \\ Cases_on `v && 2w = 0w` THEN1 523 (ASM_SIMP_TAC std_ss [arm_is_quote_pre_def,arm_is_quote_def,LET_DEF] 524 \\ ONCE_REWRITE_TAC [WORD_AND_COMM] \\ ASM_SIMP_TAC std_ss []) 525 \\ Q.PAT_X_ASSUM `~(bbb /\ cc)` MP_TAC 526 \\ ASM_SIMP_TAC std_ss [] 527 \\ STRIP_TAC 528 \\ FULL_SIMP_TAC std_ss [isQuote_thm,SExp_11,CAR_def,CDR_def] 529 \\ Q.PAT_X_ASSUM `isDot x` ASSUME_TAC 530 \\ FULL_SIMP_TAC std_ss [isDot_thm,SExp_11,lisp_tree_def] 531 \\ ONCE_REWRITE_TAC [arm_is_quote_def,arm_is_quote_pre_def] 532 \\ ASM_SIMP_TAC std_ss [LET_DEF,ALIGNED_INTRO] 533 \\ ONCE_REWRITE_TAC [ALIGNED_MOD_4] 534 \\ ASM_SIMP_TAC std_ss [WORD_ADD_0] 535 \\ REVERSE (Cases_on `h w = 0x1Bw` \\ ASM_SIMP_TAC std_ss []) 536 THEN1 FULL_SIMP_TAC std_ss [lisp_tree_def] 537 \\ Cases_on `ALIGNED (h (w + 0x4w))` \\ ASM_SIMP_TAC std_ss [] 538 \\ FULL_SIMP_TAC std_ss [SExp_11,lisp_tree_def] 539 \\ `isDot b` by 540 (Cases_on `b` \\ FULL_SIMP_TAC std_ss [lisp_tree_def,isDot_def] 541 \\ IMP_RES_TAC NOT_ALIGNED 542 \\ FULL_SIMP_TAC std_ss [WORD_SUB_ADD] 543 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w,RW1 [MULT_COMM] (GSYM ADDR32_n2w)] 544 \\ Q.PAT_X_ASSUM `h (w + 0x4w) = ADDR32 (n2w n) + 0x2w` ASSUME_TAC 545 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1] 546 \\ Q.PAT_X_ASSUM `~ALIGNED (ADDR32 (n2w n) + 0x4w)` MP_TAC 547 \\ ONCE_REWRITE_TAC [ALIGNED_MOD_4] 548 \\ ASM_SIMP_TAC std_ss [WORD_ADD_0,ALIGNED_ADDR32] 549 \\ ONCE_REWRITE_TAC [ALIGNED_MOD_4] 550 \\ ASM_SIMP_TAC std_ss [WORD_ADD_0,ALIGNED_ADDR32]) 551 \\ FULL_SIMP_TAC std_ss [isDot_thm,lisp_tree_def] 552 \\ FULL_SIMP_TAC std_ss [isDot_thm,lisp_tree_def] 553 \\ Cases_on `h (h (w + 0x4w) + 0x4w) <> 0x3w` 554 \\ FULL_SIMP_TAC std_ss [isDot_thm,lisp_tree_def,SExp_11] 555 THEN1 556 (REVERSE (Cases_on `a'`) 557 \\ FULL_SIMP_TAC std_ss [lisp_tree_def,ALIGNED_n2w] 558 \\ IMP_RES_TAC builti_symbols_thm THEN1 559 (FULL_SIMP_TAC std_ss [SExp_11] 560 \\ `0x1Bw - 0x3w <> ADDR32 0x6w` by METIS_TAC [lisp_symbol_table_11] 561 \\ FULL_SIMP_TAC std_ss [WORD_EQ_SUB_RADD,ADDR32_n2w,word_add_n2w]) 562 \\ FULL_SIMP_TAC std_ss [GSYM ADDR32_n2w,GSYM word_add_n2w,GSYM WORD_EQ_SUB_RADD] 563 \\ FULL_SIMP_TAC std_ss [word_arith_lemma2,RW1 [MULT_COMM] (GSYM ADDR32_n2w)] 564 \\ `ALIGNED (ADDR32 (n2w n)) /\ ~(ALIGNED (0x19w))` by 565 SIMP_TAC std_ss [ALIGNED_ADDR32,ALIGNED_n2w] 566 \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC []) 567 \\ REVERSE (Cases_on `b'`) 568 \\ FULL_SIMP_TAC std_ss [lisp_tree_def,ALIGNED_n2w] 569 \\ IMP_RES_TAC builti_symbols_thm THEN1 570 (FULL_SIMP_TAC std_ss [SExp_11] 571 \\ `0x3w - 0x3w <> ADDR32 0w` by METIS_TAC [lisp_symbol_table_11] 572 \\ FULL_SIMP_TAC std_ss [WORD_EQ_SUB_RADD,ADDR32_n2w,word_add_n2w]) 573 \\ FULL_SIMP_TAC std_ss [GSYM ADDR32_n2w,GSYM word_add_n2w,GSYM WORD_EQ_SUB_RADD] 574 \\ FULL_SIMP_TAC std_ss [word_arith_lemma2,RW1 [MULT_COMM] (GSYM ADDR32_n2w)] 575 \\ `ALIGNED (ADDR32 (n2w n)) /\ ~(ALIGNED (0x1w))` by 576 SIMP_TAC std_ss [ALIGNED_ADDR32,ALIGNED_n2w] 577 \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC []); 578 579 580(* main print loop 581 582 r4 = 000 --> stop 583 r4 = 001 --> print second part of dot, no parenthesis 584 r4 = 010 --> print second part of dot, with parenthesis 585 r4 = 101 --> print normal expression, no parenthesis 586 r4 = 110 --> print normal expression, with parenthesis 587 r4 = 011 --> print parenthesis only 588 589*) 590 591val (thms,arm_print_exit_def,arm_print_exit_pre_def) = compile_all `` 592 arm_print_exit(r3:word32,r4:word32) = 593 (* return r5: 0w = do nothing; 1w = print ")"; 2w = print " " or " . " *) 594 if r4 = 3w then let r5 = 1w in (r3,r4,r5) else 595 if r3 = 3w then let r5 = r4 - 1w in (r3,r4,r5) else 596 let r5 = 2w in (r3,r4,r5)``; 597 598val (thms,arm_set_return_def,arm_set_return_pre_def) = compile_all `` 599 arm_set_return (r4:word32,r5:word32,r8:word32,dh:word32 set,h:word32->word32) = 600 if r4 = 2w then 601 let r5 = 3w in 602 let h = (r8 =+ r5) h in 603 let r4 = 5w in 604 (r4,r5,r8,dh,h) 605 else 606 let r8 = r8 - 8w in 607 let r4 = 5w:word32 in 608 (r4,r5,r8,dh,h)``; 609 610(* val (arm_print_loop_aux_def,arm_print_loop_aux_pre_def) = tailrecLib.tailrec_define `` *) 611val (thms,arm_print_loop_aux_def,arm_print_loop_aux_pre_def) = compile_all `` 612 arm_print_loop_aux (r3:word32,r4:word32,r7:word32,r8:word32,dh:word32 set,h:word32->word32,df:word32 set,f:word32->word8) = 613 let (r3,r4,r5) = arm_print_exit(r3,r4) in 614 if r5 = 2w then (* print second part of dot *) 615 let r6 = 32w:word32 in 616 let (r4,r5,r8,dh,h) = arm_set_return (r4,r5,r8,dh,h) in 617 let f = (r7 =+ w2w r6) f in 618 if r3 && 3w = 0w then (* print " " *) 619 let r7 = r7 + 1w in 620 (r3,r4,r7,r8,dh,h,df,f) 621 else (* print " . " *) 622 let r5 = 46w:word32 in 623 let f = (r7 + 2w =+ w2w r6) f in 624 let f = (r7 + 1w =+ w2w r5) f in 625 let r7 = r7 + 3w in 626 (r3,r4,r7,r8,dh,h,df,f) 627 else 628 let r8 = r8 - 8w in 629 let r4 = h r8 in 630 let r3 = h (r8 + 4w) in 631 if r5 = 0w then 632 (r3,r4,r7,r8,dh,h,df,f) 633 else 634 let r5 = 41w:word32 in 635 let f = (r7 =+ w2w r5) f in 636 let r7 = r7 + 1w in 637 (r3,r4,r7,r8,dh,h,df,f)``; 638 639val (thms,arm_print_loop_def,arm_print_loop_pre_def) = compile_all `` 640 arm_print_loop (r3:word32,r4:word32,r7:word32,r8:word32,r9:word32,dh:word32 set,h:word32->word32,dm:word32 set,m:word32->word32,dg:word32 set,g:word32->word8,df:word32 set,f:word32->word8) = 641 if r4 = 0w then 642 let r5 = 0w:word32 in 643 let f = (r7 =+ w2w r5) f in 644 let r7 = r7 + 1w in 645 (r3,r4,r7,r8,r9,dh,h,dm,m,dg,g,df,f) 646 else 647 if r4 && 4w = 0w then (* if true, first part of dot pair evaluated *) 648 let (r3,r4,r7,r8,dh,h,df,f) = arm_print_loop_aux (r3,r4,r7,r8,dh,h,df,f) in 649 arm_print_loop (r3,r4,r7,r8,r9,dh,h,dm,m,dg,g,df,f) 650 else if ~(r3 && 1w = 0w) then (* must be symbol *) 651 let r3 = r3 + r9 in 652 let (r7,dm,m,dg,g,df,f) = arm_copy_symbol (r3,r7,dm,m,dg,g,df,f) in 653 let r4 = h r8 in 654 let r3 = h (r8 + 4w) in 655 arm_print_loop (r3,r4,r7,r8,r9,dh,h,dm,m,dg,g,df,f) 656 else if ~(r3 && 3w = 0w) then (* must be val *) 657 let (r7,f,df) = arm_print_num (r3,r7,df,f) in 658 let r4 = h r8 in 659 let r3 = h (r8 + 4w) in 660 arm_print_loop (r3,r4,r7,r8,r9,dh,h,dm,m,dg,g,df,f) 661 else (* must be a pair *) 662 let (r3,r4,r5,dh,h) = arm_is_quote (r3,r4,dh,h) in 663 if ~(r5 = 0w) then (* print quote *) 664 let r5 = 39w:word32 in 665 let f = (r7 =+ w2w r5) f in 666 let r7 = r7 + 1w in 667 let r4 = 6w in 668 arm_print_loop (r3,r4,r7,r8,r9,dh,h,dm,m,dg,g,df,f) 669 else 670 let r8 = r8 + 8w in 671 let r5 = h (r3 + 4w) in 672 let r6 = r4 - 4w in 673 let r3 = h r3 in 674 let h = (r8 =+ r6) h in 675 let r6 = 40w:word32 in 676 let h = (r8 + 4w =+ r5) h in 677 if r4 && 2w = 0w then (* parenthesis *) 678 let r4 = 6w in 679 arm_print_loop (r3,r4,r7,r8,r9,dh,h,dm,m,dg,g,df,f) 680 else 681 let r4 = 6w:word32 in 682 let f = (r7 =+ w2w r6) f in 683 let r7 = r7 + 1w in 684 arm_print_loop (r3,r4,r7,r8,r9,dh,h,dm,m,dg,g,df,f)`` 685 686 687 688val arm_print_loop1_def = Define `arm_print_loop1 = arm_print_loop`; 689val arm_print_loop1_pre_def = Define `arm_print_loop1_pre = arm_print_loop_pre`; 690 691val lisp_tree_SUBSET = prove( 692 ``!t w. lisp_tree t (w,d,h) sym /\ d SUBSET dh ==> 693 lisp_tree t (w,dh,h) sym``, 694 Induct \\ SIMP_TAC std_ss [lisp_tree_def] \\ METIS_TAC [SUBSET_DEF]); 695 696val stack_slots_def = Define ` 697 (stack_slots (a:word32) 0 = emp) /\ 698 (stack_slots a (SUC n) = SEP_EXISTS u1 u2. one (a,u1:word32) * one (a+4w,u2) * stack_slots (a+8w) n)`; 699 700val stack_slots_ADD = prove( 701 ``!n a m. ?fr. stack_slots a (n + m) = stack_slots a n * fr``, 702 Induct \\ SIMP_TAC std_ss [stack_slots_def,SEP_CLAUSES,ADD] 703 \\ REPEAT STRIP_TAC 704 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL[`a+8w`,`m`]) 705 \\ ASM_SIMP_TAC std_ss [STAR_ASSOC] \\ METIS_TAC []); 706 707val IF_SIMPS = prove( 708 ``!b f x g y. 709 ((if b then f x else g y) = (if b then f else g) (if b then x else y)) /\ 710 ((if b then x else x) = x)``, 711 Cases \\ SIMP_TAC std_ss []); 712 713val NOT_IN_lisp_tree = prove( 714 ``!t w d a h r3. 715 ~(a IN d) ==> 716 (lisp_tree t (r3,d,(a =+ w) h) sym = lisp_tree t (r3,d,h) sym)``, 717 Induct \\ ASM_SIMP_TAC std_ss [lisp_tree_def,APPLY_UPDATE_THM] \\ METIS_TAC []) 718 719val one_space_ADD = prove( 720 ``!m n a c. 721 one_space a (m + n) c = 722 one_space a m (a + n2w m) * 723 one_space (a + n2w m) n c``, 724 Induct 725 \\ ASM_SIMP_TAC std_ss [one_space_def,WORD_ADD_0,SEP_CLAUSES,ADD] 726 \\ SIMP_TAC std_ss [ADD1,GSYM word_add_n2w] 727 \\ SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM,STAR_ASSOC]); 728 729val one_string_STRCAT = prove( 730 ``!s t a c. 731 one_string a (s ++ t) c = 732 one_string a s (a + n2w (LENGTH s)) * 733 one_string (a + n2w (LENGTH s)) t c``, 734 Induct 735 \\ FULL_SIMP_TAC std_ss [one_string_def,WORD_ADD_0,SEP_CLAUSES, 736 ADD,MAP,LENGTH,one_list_def,APPEND] 737 \\ SIMP_TAC std_ss [ADD1,GSYM word_add_n2w] 738 \\ SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM,STAR_ASSOC]); 739 740val stack_slots_MAX = prove( 741 ``!m n a. ?fr. stack_slots a (MAX m n) = 742 stack_slots a m * fr``, 743 REPEAT STRIP_TAC 744 \\ SIMP_TAC std_ss [MAX_DEF] 745 \\ REVERSE (Cases_on `m < n`) 746 \\ ASM_SIMP_TAC std_ss [] 747 THEN1 (Q.EXISTS_TAC `emp` \\ SIMP_TAC std_ss [SEP_CLAUSES]) 748 \\ `m <= n` by DECIDE_TAC 749 \\ FULL_SIMP_TAC std_ss [LESS_EQ_EXISTS] 750 \\ SIMP_TAC std_ss [stack_slots_ADD] 751 \\ METIS_TAC [stack_slots_ADD]); 752 753val fun_eq_def = Define `fun_eq d h1 h2 = !w. w IN d ==> (h1 w = h2 w)`; 754 755val fun_eq_lisp_tree = prove( 756 ``!d h hi. 757 fun_eq d h hi ==> 758 !t a sym. lisp_tree t (a,d,h) sym = lisp_tree t (a,d,hi) sym``, 759 SIMP_TAC std_ss [fun_eq_def] \\ NTAC 4 STRIP_TAC 760 \\ Induct \\ SIMP_TAC std_ss [lisp_tree_def] 761 \\ REPEAT STRIP_TAC 762 \\ Cases_on `a IN d /\ a + 4w IN d` \\ ASM_SIMP_TAC std_ss [] 763 \\ FULL_SIMP_TAC std_ss []); 764 765val arm_print_loop_lemma = prove( 766 ``!t b p w1 w2 r3 r7 r8 a h f q c. 767 let s = sexp2string_aux (t, b) in 768 let r4 = if b then 6w else 5w in 769 (p * one_space r7 (STRLEN s) c) (fun2set (f,df)) /\ 770 lisp_symbol_table sym (r9,dm,m,dg,g) /\ 771 ALIGNED r8 /\ ALIGNED r9 /\ STRLEN s < 2**32 /\ 772 lisp_tree t (r3,d,h) sym /\ d SUBSET dh /\ 773 (q * one (r8,w2) * one (r8 + 4w,w1) * stack_slots (r8 + 8w) (LDEPTH t)) 774 (fun2set (h,dh DIFF d)) ==> 775 ?hi fi. 776 (arm_print_loop_pre (r3,r4,r7,r8,r9,dh,h,dm,m,dg,g,df,f) = 777 arm_print_loop1_pre (w1,w2,c,r8,r9,dh,hi,dm,m,dg,g,df,fi)) /\ 778 (arm_print_loop (r3,r4,r7,r8,r9,dh,h,dm,m,dg,g,df,f) = 779 arm_print_loop1 (w1,w2,c,r8,r9,dh,hi,dm,m,dg,g,df,fi)) /\ 780 (p * one_string r7 s c) (fun2set (fi,df)) /\ 781 (q * one (r8,w2) * one (r8 + 4w,w1) * stack_slots (r8 + 8w) (LDEPTH t)) 782 (fun2set (hi,dh DIFF d)) /\ fun_eq d h hi``, 783 completeInduct_on `LSIZE t` 784 \\ POP_ASSUM (ASSUME_TAC o RW1 [GSYM CONTAINER_def]) 785 \\ SIMP_TAC std_ss [LET_DEF] 786 \\ REPEAT STRIP_TAC 787 \\ `~((if b then 6w else 5w) = 0w:word32)` by (Cases_on `b` \\ EVAL_TAC) 788 \\ `~((if b then 6w else 5w) && 4w = 0w:word32)` by (Cases_on `b` \\ EVAL_TAC) 789 \\ `~((if b then 0x6w else 0x5w) = 0x3w:word32)` by (Cases_on `b` \\ EVAL_TAC) 790 \\ ONCE_REWRITE_TAC [arm_print_loop_def] 791 \\ ASM_SIMP_TAC std_ss [LET_DEF] 792 \\ Cases_on `isVal t` THEN1 793 (Q.PAT_X_ASSUM `CONTAINER (!m. bbb)` (K ALL_TAC) 794 \\ FULL_SIMP_TAC std_ss [isVal_thm] 795 \\ FULL_SIMP_TAC std_ss [lisp_tree_def] 796 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,ALIGNED_INTRO] 797 \\ `~ALIGNED (n2w (a * 4 + 2))` by 798 (ONCE_REWRITE_TAC [MULT_COMM] 799 \\ SIMP_TAC std_ss [GSYM word_add_n2w] 800 \\ SIMP_TAC std_ss [GSYM ADDR32_n2w] 801 \\ SIMP_TAC std_ss [ALIGNED_ADD_EQ,ALIGNED_ADDR32,ALIGNED_n2w]) 802 \\ ASM_SIMP_TAC std_ss [] 803 \\ `n2w (a * 4 + 2) && 0x1w = 0w:word32` by 804 (SIMP_TAC std_ss [n2w_and_1] 805 \\ REWRITE_TAC [DECIDE ``n * 4 + 2 = (n * 2 + 1) * 2:num``] 806 \\ REWRITE_TAC [MATCH_MP MOD_EQ_0 (DECIDE ``0<2:num``)]) 807 \\ ASM_SIMP_TAC std_ss [] 808 \\ FULL_SIMP_TAC std_ss [sexp2string_aux_def] 809 \\ (STRIP_ASSUME_TAC o UNDISCH_ALL o Q.SPECL [`a`,`r7`,`c`,`f`,`p`] o 810 RW1 [MULT_COMM] o 811 SIMP_RULE std_ss [GSYM AND_IMP_INTRO]) arm_print_num_lemma 812 \\ ASM_SIMP_TAC std_ss [] 813 \\ `(h r8 = w2) /\ r8 IN dh DIFF d` by SEP_READ_TAC 814 \\ `(h (r8 + 4w) = w1) /\ (r8 + 4w) IN dh DIFF d` by SEP_READ_TAC 815 \\ FULL_SIMP_TAC std_ss [IN_DIFF] 816 \\ Q.EXISTS_TAC `h` 817 \\ Q.EXISTS_TAC `fi` 818 \\ ASM_SIMP_TAC std_ss [arm_print_loop1_def] 819 \\ ONCE_REWRITE_TAC [arm_print_loop_pre_def] 820 \\ ASM_SIMP_TAC std_ss [arm_print_loop1_pre_def,LET_DEF] 821 \\ ASM_SIMP_TAC std_ss [LET_DEF,ALIGNED_INTRO] 822 \\ ONCE_REWRITE_TAC [WORD_AND_COMM] 823 \\ ASM_SIMP_TAC std_ss [fun_eq_def] 824 \\ ALIGNED_TAC) 825 \\ Cases_on `isSym t` THEN1 826 (Q.PAT_X_ASSUM `CONTAINER (!m. bbb)` (K ALL_TAC) 827 \\ FULL_SIMP_TAC std_ss [isSym_thm] 828 \\ FULL_SIMP_TAC std_ss [isSym_thm,lisp_tree_def,GSYM STAR_ASSOC] 829 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,ALIGNED_INTRO] 830 \\ `~((r3 && 0x1w) = 0x0w)` by 831 (`ALIGNED (r3 - 3w + 4w)` by ALIGNED_TAC 832 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3] 833 \\ POP_ASSUM MP_TAC 834 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 835 \\ Q.SPEC_TAC (`r3`,`w`) \\ Cases_word 836 \\ SIMP_TAC std_ss [ALIGNED_n2w,word_add_n2w,n2w_and_1] 837 \\ SIMP_TAC std_ss [bitTheory.MOD_PLUS_1] 838 \\ STRIP_TAC 839 \\ STRIP_ASSUME_TAC (Q.SPEC `n` (MATCH_MP DIVISION (DECIDE ``0<4:num``))) 840 \\ `n MOD 4 = 3` by DECIDE_TAC 841 \\ ONCE_ASM_REWRITE_TAC [] 842 \\ Q.PAT_X_ASSUM `n = mmm` (K ALL_TAC) 843 \\ ASM_SIMP_TAC std_ss [] 844 \\ REWRITE_TAC [DECIDE ``m * 4 + 3 = (m * 2 + 1) * 2 + 1:num``] 845 \\ REWRITE_TAC [MATCH_MP MOD_MULT (DECIDE ``1 < 2:num``)] \\ EVAL_TAC) 846 \\ FULL_SIMP_TAC std_ss [sexp2string_aux_def] 847 \\ `(h r8 = w2) /\ r8 IN dh DIFF d` by SEP_READ_TAC 848 \\ `(h (r8 + 4w) = w1) /\ (r8 + 4w) IN dh DIFF d` by SEP_READ_TAC 849 \\ FULL_SIMP_TAC std_ss [IN_DIFF] 850 \\ `?fi. arm_copy_symbol_pre (r3 + r9,r7,dm,m,dg,g,df,f) /\ 851 (arm_copy_symbol (r3 + r9,r7,dm,m,dg,g,df,f) = 852 (c,dm,m,dg,g,df,fi)) /\ 853 (p * one_string r7 a c) (fun2set (fi,df))` by 854 METIS_TAC [EVAL ``(2:num)**32``,arm_copy_symbol_lemma] 855 \\ Q.EXISTS_TAC `h` 856 \\ Q.EXISTS_TAC `fi` 857 \\ ASM_SIMP_TAC std_ss [arm_print_loop1_def] 858 \\ ONCE_REWRITE_TAC [arm_print_loop_pre_def] 859 \\ ASM_SIMP_TAC std_ss [arm_print_loop1_pre_def,LET_DEF] 860 \\ ASM_SIMP_TAC std_ss [LET_DEF,ALIGNED_INTRO] 861 \\ ONCE_REWRITE_TAC [WORD_AND_COMM] 862 \\ ASM_SIMP_TAC std_ss [fun_eq_def] 863 \\ ALIGNED_TAC) 864 \\ `isDot t` by (Cases_on `t` \\ FULL_SIMP_TAC std_ss [isVal_def,isSym_def,isDot_def]) 865 \\ `ALIGNED r3` by 866 (FULL_SIMP_TAC std_ss [isDot_thm,lisp_tree_def,GSYM STAR_ASSOC] 867 \\ FULL_SIMP_TAC std_ss [isDot_thm,lisp_tree_def,GSYM STAR_ASSOC] 868 \\ FULL_SIMP_TAC std_ss [isSym_thm,lisp_tree_def,GSYM STAR_ASSOC]) 869 \\ `r3 && 0x1w = 0x0w` by 870 (POP_ASSUM MP_TAC \\ Q.SPEC_TAC (`r3`,`a`) \\ Cases 871 \\ SIMP_TAC std_ss [ALIGNED_n2w,n2w_and_1] \\ STRIP_TAC 872 \\ `n = n DIV 4 * 4` by METIS_TAC [DIVISION,ADD_0,DECIDE ``0<4:num``] 873 \\ ONCE_ASM_REWRITE_TAC [] 874 \\ REWRITE_TAC [MATCH_MP MOD_EQ_0 (DECIDE ``0<2:num``),DECIDE ``n * 4:num = (n * 2) * 2``]) 875 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO] 876 \\ Q.ABBREV_TAC `r = if b then 0x6w else 0x5w:word32` 877 \\ `arm_is_quote_pre (r3,r,dh,h) /\ 878 (if isQuote t /\ ~((r && 0x2w) = 0x0w) then 879 (arm_is_quote (r3,r,dh,h) = (h (h (r3 + 0x4w)),r,0x3w,dh,h)) /\ 880 lisp_tree (CAR (CDR t)) (h (h (r3 + 0x4w)),dh,h) sym 881 else arm_is_quote (r3,r,dh,h) = (r3,r,0x0w,dh,h))` by 882 (IMP_RES_TAC lisp_tree_SUBSET 883 \\ IMP_RES_TAC arm_is_quote_lemma \\ METIS_TAC []) 884 \\ `~((r && 0x2w) = 0x0w) = b` by 885 (Q.UNABBREV_TAC `r` \\ Cases_on `b` \\ EVAL_TAC) 886 \\ FULL_SIMP_TAC std_ss [] 887 \\ Cases_on `isQuote t /\ b` THEN1 888 (FULL_SIMP_TAC std_ss [CONTAINER_def] 889 \\ REWRITE_TAC [EVAL ``3w = 0w:word32``] 890 \\ `sexp2string_aux (t,T) = (#"'")::sexp2string_aux (CAR (CDR t),T)` by 891 (FULL_SIMP_TAC std_ss [isQuote_thm,CAR_def,CDR_def,LET_DEF] 892 \\ ASM_SIMP_TAC std_ss [sexp2string_aux_def,SExp_11,isQuote_thm] 893 \\ SIMP_TAC std_ss [LIST_STRCAT_def,CAR_def,CDR_def,APPEND_NIL,APPEND]) 894 \\ FULL_SIMP_TAC std_ss [LENGTH,one_space_def,SEP_CLAUSES,one_string_def] 895 \\ Q.ABBREV_TAC `f2 = (r7 =+ w2w (0x27w:word32)) f` 896 \\ SIMP_TAC std_ss [MAP,one_list_def,GSYM one_string_def] 897 \\ FULL_SIMP_TAC std_ss [EVAL ``ORD #"'"``,STAR_ASSOC,SEP_EXISTS] 898 \\ Q.ABBREV_TAC `r3n = h (h (r3 + 0x4w))` 899 \\ `(p * one (r7,0x27w) * 900 one_space (r7 + 0x1w) (STRLEN (sexp2string_aux (CAR (CDR t),T)))c) 901 (fun2set (f2,df))` by 902 (Q.UNABBREV_TAC `f2` 903 \\ REWRITE_TAC [EVAL ``(w2w:word32->word8) 0x27w``] 904 \\ SEP_WRITE_TAC) 905 \\ `LSIZE (CAR (CDR t)) < LSIZE t` by 906 (FULL_SIMP_TAC std_ss [isQuote_thm,CAR_def,CDR_def,LSIZE_def] \\ DECIDE_TAC) 907 \\ `(STRLEN (sexp2string_aux (CAR (CDR t),T))) < 4294967296` by DECIDE_TAC 908 \\ `LDEPTH (CAR (CDR t)) <= LDEPTH t` by 909 (FULL_SIMP_TAC std_ss [isQuote_thm,CAR_def,CDR_def,LDEPTH_def] \\ DECIDE_TAC) 910 \\ FULL_SIMP_TAC std_ss [LESS_EQ_EXISTS] 911 \\ STRIP_ASSUME_TAC (Q.SPECL [`LDEPTH (CAR (CDR t))`,`r8+8w`,`p'`] stack_slots_ADD) 912 \\ FULL_SIMP_TAC std_ss [] 913 \\ `(q * fr * one (r8,w2) * one (r8 + 0x4w,w1) * 914 stack_slots (r8 + 0x8w) (LDEPTH (CAR (CDR t)))) 915 (fun2set (h,dh DIFF d))` by FULL_SIMP_TAC (std_ss++star_ss) [] 916 \\ `lisp_tree (CAR (CDR t)) (r3n,d,h) sym` by 917 (Q.UNABBREV_TAC `r3n` 918 \\ FULL_SIMP_TAC std_ss [isQuote_thm,CAR_def,CDR_def] 919 \\ FULL_SIMP_TAC std_ss [isQuote_thm,CAR_def,CDR_def,lisp_tree_def]) 920 \\ Q.PAT_X_ASSUM `!m. bbb` (ASSUME_TAC o UNDISCH o Q.SPEC `LSIZE (CAR (CDR t))`) 921 \\ POP_ASSUM (ASSUME_TAC o RW [] o Q.SPEC `(CAR (CDR t))`) 922 \\ POP_ASSUM (ASSUME_TAC o 923 SIMP_RULE std_ss [LET_DEF,GSYM AND_IMP_INTRO,GSYM one_string_def] o 924 Q.SPECL [`T`,`p * one (r7,0x27w)`,`w1`,`w2`,`r3n`,`r7+1w`,`r8`,`h`,`f2`,`q * fr`,`c`]) 925 \\ REPEAT (POP_ASSUM (STRIP_ASSUME_TAC o UNDISCH)) 926 \\ Q.EXISTS_TAC `hi` 927 \\ Q.EXISTS_TAC `fi` 928 \\ ASM_SIMP_TAC std_ss [one_string_def,MAP,one_list_def] 929 \\ ASM_SIMP_TAC std_ss [GSYM one_string_def,EVAL ``ORD #"'"``,STAR_ASSOC] 930 \\ FULL_SIMP_TAC (std_ss++star_ss) [] 931 \\ ONCE_REWRITE_TAC [arm_print_loop_pre_def] 932 \\ ASM_SIMP_TAC std_ss [LET_DEF,ALIGNED_INTRO] 933 \\ ONCE_REWRITE_TAC [WORD_AND_COMM] 934 \\ ASM_SIMP_TAC std_ss [LET_DEF,EVAL ``3w = 0w:word32``] 935 \\ ASM_SIMP_TAC std_ss [LET_DEF,ALIGNED_INTRO] 936 \\ ONCE_REWRITE_TAC [WORD_AND_COMM] 937 \\ ASM_SIMP_TAC std_ss [LET_DEF,ALIGNED_INTRO] 938 \\ `r7 IN df` by SEP_READ_TAC 939 \\ ASM_SIMP_TAC std_ss [arm_print_loop1_pre_def]) 940 \\ POP_ASSUM MP_TAC 941 \\ REWRITE_TAC [METIS_PROVE [] ``~(b /\ c) = b ==> ~c``] 942 \\ STRIP_TAC 943 \\ ONCE_REWRITE_TAC [arm_print_loop_pre_def] 944 \\ ASM_SIMP_TAC std_ss [LET_DEF,ALIGNED_INTRO] 945 \\ ONCE_REWRITE_TAC [WORD_AND_COMM] 946 \\ ASM_SIMP_TAC std_ss [LET_DEF,ALIGNED_INTRO] 947 \\ `arm_is_quote (r3,r,dh,h) = (r3,r,0x0w,dh,h)` by METIS_TAC [] 948 \\ `((r && 0x2w) = 0x0w) <=> ~b` by METIS_TAC [] 949 \\ ASM_SIMP_TAC std_ss [NOT_IF,word_arith_lemma1] 950 \\ ONCE_REWRITE_TAC [WORD_AND_COMM] 951 \\ ASM_SIMP_TAC std_ss [LET_DEF,ALIGNED_INTRO] 952 \\ Q.ABBREV_TAC `h2 = (r8 + 0xCw =+ h (r3 + 0x4w)) ((r8 + 0x8w =+ r - 0x4w) h)` 953 \\ `?a1 a2. t = Dot a1 a2` by FULL_SIMP_TAC std_ss [isDot_thm,SExp_11] 954 \\ `lisp_tree t (r3,d,h2) sym /\ (h2 r3 = h r3) /\ (h2 (r3 + 4w) = h (r3 + 4w))` by 955 (FULL_SIMP_TAC std_ss [LDEPTH_def,stack_slots_def,word_arith_lemma1] 956 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES] 957 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,STAR_ASSOC] 958 \\ `r8 + 0x8w IN dh DIFF d /\ r8 + 0xCw IN dh DIFF d` by SEP_READ_TAC 959 \\ FULL_SIMP_TAC std_ss [IN_DIFF] 960 \\ Q.UNABBREV_TAC `h2` 961 \\ ASM_SIMP_TAC std_ss [NOT_IN_lisp_tree] 962 \\ FULL_SIMP_TAC std_ss [lisp_tree_def,APPLY_UPDATE_THM] 963 \\ METIS_TAC []) 964 \\ `ALIGNED (r8 + 8w)` by ALIGNED_TAC 965 \\ Q.ABBREV_TAC `s1 = sexp2string_aux (a1,T)` 966 \\ Q.ABBREV_TAC `s2 = if a2 = Sym "nil" then "" else sexp2string_aux (a2,F)` 967 \\ Q.ABBREV_TAC `s3 = if a2 = Sym "nil" then "" else if isDot a2 then " " else " . "` 968 \\ Q.ABBREV_TAC `p1 = if b then "(" else ""` 969 \\ Q.ABBREV_TAC `p2 = if b then ")" else ""` 970 \\ `sexp2string_aux (t,b) = p1 ++ s1 ++ s3 ++ s2 ++ p2` by 971 (Q.UNABBREV_TAC `s1` \\ Q.UNABBREV_TAC `s2` 972 \\ Q.UNABBREV_TAC `p1` \\ Q.UNABBREV_TAC `p2` 973 \\ Q.UNABBREV_TAC `s3` \\ Cases_on `b` 974 \\ Cases_on `a2 = Sym "nil"` 975 \\ Cases_on `isDot a2` 976 \\ FULL_SIMP_TAC std_ss [sexp2string_aux_def,LET_DEF,IF_SIMPS, 977 APPEND,APPEND_NIL,LIST_STRCAT_def,APPEND_ASSOC] 978 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND]) 979 \\ ONCE_REWRITE_TAC [WORD_AND_COMM] \\ ASM_SIMP_TAC std_ss [] 980 \\ `ALIGNED (r3 + 4w) /\ ALIGNED (r8 + 12w)` by ALIGNED_TAC 981 \\ `r3 + 0x4w IN dh /\ r3 IN dh /\ r8 + 0x8w IN dh /\ r8 + 0xCw IN dh` by 982 (Q.PAT_X_ASSUM `isDot t` (ASSUME_TAC) 983 \\ FULL_SIMP_TAC std_ss [isDot_thm,LDEPTH_def] 984 \\ FULL_SIMP_TAC std_ss [stack_slots_def,SEP_CLAUSES] 985 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,lisp_tree_def] 986 \\ STRIP_TAC THEN1 METIS_TAC [SUBSET_DEF] 987 \\ STRIP_TAC THEN1 METIS_TAC [SUBSET_DEF] 988 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1] 989 \\ `r8 + 0x8w IN dh DIFF d /\ r8 + 0xCw IN dh DIFF d` by SEP_READ_TAC 990 \\ FULL_SIMP_TAC std_ss [IN_DIFF]) 991 \\ `b ==> r7 IN df` by 992 (REPEAT STRIP_TAC 993 \\ Q.PAT_X_ASSUM `t = Dot a1 a2` (K ALL_TAC) 994 \\ Q.UNABBREV_TAC `p1` 995 \\ FULL_SIMP_TAC bool_ss [one_space_def,LENGTH_APPEND,one_space_ADD,one_space_def,LENGTH] 996 \\ FULL_SIMP_TAC std_ss [stack_slots_def,SEP_CLAUSES] 997 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,lisp_tree_def] 998 \\ SEP_READ_TAC) 999 \\ ASM_SIMP_TAC std_ss [NOT_IF] 1000 \\ FULL_SIMP_TAC std_ss [IF_SIMPS,EVAL ``(w2w:word32->word8) 0x29w``] 1001 \\ Q.ABBREV_TAC `f2 = if b then (r7 =+ 0x28w) f else f` 1002 \\ Q.ABBREV_TAC `r72 = if b then r7 + 0x1w else r7` 1003 \\ FULL_SIMP_TAC std_ss [isVal_def,isDot_def,isSym_def] 1004 \\ REPEAT (Q.PAT_X_ASSUM `T` (K ALL_TAC)) 1005 \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND] 1006 \\ `STRLEN s1 < 4294967296 /\ STRLEN s2 < 4294967296` by DECIDE_TAC 1007 \\ `(p * one_string r7 p1 r72 * 1008 one_space r72 (LENGTH (s1++s3++s2++p2)) c) (fun2set (f2,df))` by 1009 (Q.UNABBREV_TAC `r72` \\ Q.UNABBREV_TAC `p1` 1010 \\ Q.UNABBREV_TAC `p2` \\ Q.UNABBREV_TAC `f2` 1011 \\ REVERSE (Cases_on `b`) 1012 \\ FULL_SIMP_TAC std_ss [one_string_def,MAP,one_list_def, 1013 SEP_CLAUSES,LENGTH_APPEND,LENGTH,EVAL ``ORD #"("``,GSYM ADD_ASSOC] 1014 \\ Q.PAT_X_ASSUM `pp (fun2set (f,df))` (ASSUME_TAC o RW [GSYM (RW1[ADD_COMM]ADD1)]) 1015 \\ FULL_SIMP_TAC std_ss [one_space_def,SEP_CLAUSES] 1016 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,STAR_ASSOC] 1017 \\ SEP_WRITE_TAC) 1018 \\ Q.PAT_X_ASSUM `bb (fun2set (h,dh DIFF d))` (ASSUME_TAC o RW [LDEPTH_def]) 1019 \\ FULL_SIMP_TAC std_ss [stack_slots_def,SEP_CLAUSES] 1020 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,STAR_ASSOC,word_arith_lemma1] 1021 \\ STRIP_ASSUME_TAC (Q.SPECL [`LDEPTH a1`,`LDEPTH a2`,`r8+16w`] stack_slots_MAX) 1022 \\ FULL_SIMP_TAC std_ss [] 1023 \\ `(q * fr * one (r8,w2) * one (r8 + 0x4w,w1) * one (r8 + 0x8w,r-4w) * 1024 one (r8 + 0xCw,h (r3+4w)) * stack_slots (r8 + 0x10w) (LDEPTH a1)) 1025 (fun2set (h2,dh DIFF d))` by 1026 (Q.UNABBREV_TAC `h2` \\ SEP_WRITE_TAC) 1027 \\ `lisp_tree a1 (h r3,d,h2) sym` by 1028 (FULL_SIMP_TAC std_ss [lisp_tree_def] 1029 \\ Q.UNABBREV_TAC `h2` 1030 \\ `r8 + 8w IN dh DIFF d /\ r8 + 12w IN dh DIFF d` by SEP_READ_TAC 1031 \\ FULL_SIMP_TAC std_ss [IN_DIFF] 1032 \\ METIS_TAC [NOT_IN_lisp_tree]) 1033 \\ Q.ABBREV_TAC `r73 = r72 + n2w (STRLEN s1)` 1034 \\ `(p * one_string r7 p1 r72 * 1035 one_space r73 (STRLEN ((STRCAT s3 (STRCAT s2 p2)))) c * 1036 one_space r72 (STRLEN s1) r73) (fun2set (f2,df))` by 1037 (Q.UNABBREV_TAC `r73` 1038 \\ FULL_SIMP_TAC (std_ss++star_ss) [one_space_ADD,LENGTH_APPEND] 1039 \\ FULL_SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_add_n2w] 1040 \\ FULL_SIMP_TAC std_ss [AC ADD_COMM ADD_ASSOC] 1041 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 1042 \\ FULL_SIMP_TAC std_ss [LSIZE_def] 1043 \\ Q.PAT_X_ASSUM `CONTAINER (!m. bbb)` (fn th => let val th = RW [CONTAINER_def] th in 1044 (ASSUME_TAC o RW [] o Q.SPEC `F` o RW [] o Q.SPEC `a2` o 1045 RW [DECIDE ``n < SUC (m + n):num``] o Q.SPEC `LSIZE a2`) th 1046 THEN 1047 (ASSUME_TAC o RW [] o Q.SPEC `T` o RW [] o Q.SPEC `a1` o 1048 RW [DECIDE ``m < SUC (m + n):num``] o Q.SPEC `LSIZE a1`) th end) 1049 \\ POP_ASSUM (ASSUME_TAC o SIMP_RULE std_ss [LET_DEF]) 1050 \\ Q.UNABBREV_TAC `s1` 1051 \\ POP_ASSUM (ASSUME_TAC o RW [GSYM AND_IMP_INTRO] o 1052 RW [arm_print_loop1_def,arm_print_loop1_pre_def] o 1053 Q.SPECL [`p * one_string r7 p1 r72 * 1054 one_space r73 (STRLEN ((STRCAT s3 (STRCAT s2 p2)))) c`, 1055 `h (r3+4w:word32)`,`r-4w`,`h (r3:word32)`, 1056 `r72`,`r8+8w`,`h2`,`f2`,`q * fr * one (r8,w2) * one (r8 + 0x4w,w1)`,`r73`]) 1057 \\ POP_ASSUM (ASSUME_TAC o SIMP_RULE std_ss [word_arith_lemma1]) 1058 \\ REPEAT (POP_ASSUM (STRIP_ASSUME_TAC o UNDISCH)) 1059 \\ Q.UNABBREV_TAC `f2` 1060 \\ ASM_SIMP_TAC std_ss [EVAL ``(w2w:word32->word8) 0x28w``] 1061 \\ Q.ABBREV_TAC `s1 = sexp2string_aux (a1,T)` 1062 \\ `(r - 4w && 4w = 0w) /\ ~(r - 4w = 0w) /\ ~(r - 4w = 3w)` by 1063 (Q.UNABBREV_TAC `r` \\ Cases_on `b` \\ EVAL_TAC) 1064 \\ ONCE_REWRITE_TAC [arm_print_loop_def,arm_print_loop_pre_def] 1065 \\ ASM_SIMP_TAC std_ss [] 1066 \\ ONCE_REWRITE_TAC [WORD_AND_COMM] 1067 \\ ASM_SIMP_TAC std_ss [] 1068 \\ ONCE_REWRITE_TAC [WORD_AND_COMM] 1069 \\ ASM_SIMP_TAC std_ss [] 1070 \\ `fun_eq d h hi` by 1071 (`fun_eq d h h2` suffices_by METIS_TAC [fun_eq_def] 1072 \\ SIMP_TAC std_ss [fun_eq_def] 1073 \\ REPEAT STRIP_TAC 1074 \\ Q.PAT_X_ASSUM `t = Dot a1 a2` ASSUME_TAC 1075 \\ Q.UNABBREV_TAC `h2` 1076 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,IN_DIFF] 1077 \\ `r8 + 8w IN dh DIFF d` by SEP_READ_TAC 1078 \\ `r8 + 12w IN dh DIFF d` by SEP_READ_TAC 1079 \\ FULL_SIMP_TAC std_ss [IN_DIFF] 1080 \\ METIS_TAC []) 1081 \\ Cases_on `a2 = Sym "nil"` THEN1 1082 (FULL_SIMP_TAC std_ss [] 1083 \\ Q.UNABBREV_TAC `s3` \\ Q.UNABBREV_TAC `s2` 1084 \\ FULL_SIMP_TAC std_ss [APPEND_NIL,APPEND,lisp_tree_def] 1085 \\ `h (r3 + 0x4w) = 3w` by METIS_TAC [lisp_symbol_table_consts] 1086 \\ ASM_SIMP_TAC std_ss [arm_print_loop_aux_pre_def,arm_print_loop_aux_def,arm_print_exit_def] 1087 \\ SIMP_TAC std_ss [LET_DEF,word_arith_lemma1] 1088 \\ `~(r - 5w = 2w) /\ ((r - 5w = 0w) = ~b)` by 1089 (Q.UNABBREV_TAC `r` \\ Cases_on `b` \\ EVAL_TAC) 1090 \\ ASM_SIMP_TAC std_ss [WORD_ADD_SUB,NOT_IF] 1091 \\ SIMP_TAC std_ss [EVAL ``(w2w:word32->word8) 0x29w``] 1092 \\ SIMP_TAC std_ss [IF_SIMPS] 1093 \\ Q.ABBREV_TAC `fi2 = if b then (r73 =+ 0x29w) fi else fi` 1094 \\ Q.ABBREV_TAC `r74 = if b then r73 + 0x1w else r73` 1095 \\ `(hi (r8 + 0x4w) = w1)` by SEP_READ_TAC 1096 \\ `(hi (r8) = w2)` by SEP_READ_TAC 1097 \\ ASM_SIMP_TAC std_ss [] 1098 \\ `c = r74` by 1099 (Q.UNABBREV_TAC `p2` \\ Q.UNABBREV_TAC `r74` 1100 \\ REVERSE (Cases_on `b`) 1101 \\ FULL_SIMP_TAC (bool_ss++sep_cond_ss) [one_space_def,LENGTH,cond_STAR] 1102 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [SEP_CLAUSES] 1103 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,cond_STAR]) 1104 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO] 1105 \\ `r8 IN dh DIFF d /\ r8 + 4w IN dh DIFF d` by SEP_READ_TAC 1106 \\ `ALIGNED (r8 + 4w)` by ALIGNED_TAC 1107 \\ `b ==> r73 IN df` by 1108 (REPEAT STRIP_TAC 1109 \\ Q.UNABBREV_TAC `p2` 1110 \\ FULL_SIMP_TAC bool_ss [one_space_def,LENGTH,SEP_CLAUSES] 1111 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] \\ SEP_READ_TAC) 1112 \\ FULL_SIMP_TAC std_ss [IN_DIFF] 1113 \\ Q.EXISTS_TAC `hi` 1114 \\ Q.EXISTS_TAC `fi2` 1115 \\ ASM_SIMP_TAC std_ss [arm_print_loop1_pre_def,arm_print_loop1_def] 1116 \\ ONCE_REWRITE_TAC [LDEPTH_def] 1117 \\ ASM_SIMP_TAC std_ss [stack_slots_def,SEP_CLAUSES,word_arith_lemma1] 1118 \\ SIMP_TAC std_ss [SEP_EXISTS,word_arith_lemma1] 1119 \\ REVERSE STRIP_TAC THEN1 1120 (Q.EXISTS_TAC `r - 4w` \\ Q.EXISTS_TAC `h (r3 + 4w)` 1121 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 1122 \\ FULL_SIMP_TAC std_ss [one_string_STRCAT] 1123 \\ Q.UNABBREV_TAC `p1` 1124 \\ Q.UNABBREV_TAC `p2` 1125 \\ Q.UNABBREV_TAC `r72` 1126 \\ Q.UNABBREV_TAC `r73` 1127 \\ Q.UNABBREV_TAC `fi2` 1128 \\ Q.UNABBREV_TAC `r74` 1129 \\ REVERSE (Cases_on `b`) THEN1 1130 (FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM] 1131 \\ FULL_SIMP_TAC std_ss [one_string_def,one_list_def,MAP,LENGTH] 1132 \\ FULL_SIMP_TAC std_ss [WORD_ADD_0,SEP_CLAUSES,one_space_def,APPEND]) 1133 \\ FULL_SIMP_TAC std_ss [LENGTH,SIMP_RULE std_ss [] 1134 (REWRITE_CONV [one_space_def] ``one_space a (SUC 0) b``)] 1135 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES] 1136 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,LENGTH_APPEND,LENGTH,GSYM word_add_n2w] 1137 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] 1138 \\ FULL_SIMP_TAC std_ss [one_string_def,one_list_def,MAP] 1139 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,EVAL ``ORD #")"``] 1140 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC,SEP_CLAUSES] 1141 \\ SEP_WRITE_TAC) 1142 \\ ASM_SIMP_TAC std_ss [arm_print_loop_aux_def,arm_print_loop_aux_pre_def,arm_print_exit_def] 1143 \\ `~(h (r3 + 4w) = 3w)` by 1144 (IMP_RES_TAC builti_symbols_thm 1145 \\ CCONTR_TAC 1146 \\ FULL_SIMP_TAC std_ss [ADDR32_n2w,word_add_n2w] 1147 \\ Q.PAT_X_ASSUM `t = Dot a1 a2` (ASSUME_TAC) 1148 \\ FULL_SIMP_TAC std_ss [lisp_tree_def] 1149 \\ Q.PAT_X_ASSUM `!x.bbb` (K ALL_TAC) 1150 \\ Cases_on `a2` 1151 \\ FULL_SIMP_TAC std_ss [lisp_tree_def,ALIGNED_n2w] 1152 \\ FULL_SIMP_TAC std_ss [GSYM ADDR32_n2w,GSYM word_add_n2w,GSYM WORD_EQ_SUB_RADD] 1153 \\ FULL_SIMP_TAC std_ss [word_arith_lemma2,RW1 [MULT_COMM] (GSYM ADDR32_n2w)] 1154 \\ `ALIGNED (ADDR32 (n2w n)) /\ ~(ALIGNED (0x1w))` by 1155 SIMP_TAC std_ss [ALIGNED_ADDR32,ALIGNED_n2w] 1156 \\ FULL_SIMP_TAC std_ss [] THEN1 METIS_TAC [] 1157 \\ METIS_TAC [lisp_symbol_table_11]) 1158 \\ FULL_SIMP_TAC std_ss [LET_DEF,arm_set_return_def] 1159 \\ SIMP_TAC std_ss [ALIGNED_INTRO] 1160 \\ `ALIGNED (h (r3 + 0x4w)) = isDot a2` by 1161 (Q.PAT_X_ASSUM `t = Dot a1 a2` (ASSUME_TAC) 1162 \\ FULL_SIMP_TAC std_ss [lisp_tree_def] 1163 \\ Cases_on `a2` 1164 \\ FULL_SIMP_TAC std_ss [lisp_tree_def,isDot_def] 1165 \\ SIMP_TAC std_ss [GSYM word_add_n2w,GSYM (RW1 [MULT_COMM] ADDR32_n2w)] 1166 \\ SIMP_TAC std_ss [ALIGNED_ADD_EQ,ALIGNED_ADDR32,ALIGNED_n2w] 1167 \\ IMP_RES_TAC NOT_ALIGNED 1168 \\ FULL_SIMP_TAC std_ss [WORD_SUB_ADD]) 1169 \\ ASM_SIMP_TAC std_ss [WORD_ADD_SUB] 1170 \\ `(r - 0x4w = 0x2w) = b` by 1171 (Q.UNABBREV_TAC `r` \\ Cases_on `b` \\ EVAL_TAC) 1172 \\ ASM_SIMP_TAC std_ss [EVAL ``(w2w:word32->word8) 0x20w``] 1173 \\ ASM_SIMP_TAC std_ss [EVAL ``(w2w:word32->word8) 0x2Ew``] 1174 \\ ASM_SIMP_TAC std_ss [arm_set_return_pre_def,LET_DEF,ALIGNED_INTRO] 1175 \\ `(isDot a2 ==> r73 IN df) /\ 1176 (~(isDot a2) ==> r73 IN df /\ r73 + 1w IN df /\ r73 + 2w IN df)` by 1177 (REPEAT STRIP_TAC \\ Q.UNABBREV_TAC `s3` 1178 \\ FULL_SIMP_TAC std_ss [APPEND,LENGTH,one_space_def,SEP_CLAUSES] 1179 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,word_arith_lemma1] \\ SEP_READ_TAC) 1180 \\ ASM_SIMP_TAC std_ss [] 1181 \\ Q.ABBREV_TAC `r8i = if b then r8 + 8w else r8` 1182 \\ Q.ABBREV_TAC `hi2 = if b then (r8 + 8w =+ 3w ) hi else hi` 1183 \\ `(if b then (5w,0x3w:word32,r8 + 0x8w,dh,(r8 + 0x8w =+ 0x3w) hi) 1184 else (5w,0x2w,r8,dh,hi)) = 1185 (5w:word32,if b then 3w else 2w, r8i, dh, hi2)` by 1186 (Q.UNABBREV_TAC `r8i` 1187 \\ Q.UNABBREV_TAC `hi2` 1188 \\ Q.UNABBREV_TAC `r` 1189 \\ Cases_on `b` 1190 \\ SIMP_TAC std_ss [word_add_n2w,WORD_SUB_ADD]) 1191 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 1192 \\ Q.ABBREV_TAC `r74 = r73 + if isDot a2 then 1w else 3w` 1193 \\ Q.ABBREV_TAC `fi2 = if isDot a2 then (r73 =+ 0x20w) fi else 1194 (r73 + 0x1w =+ 0x2Ew) ((r73 + 0x2w =+ 0x20w) ((r73 =+ 0x20w) fi))` 1195 \\ `(if isDot a2 then 1196 (h (r3 + 0x4w),5w:word32,r73 + 0x1w,r8i,dh,hi2,df,(r73 =+ 0x20w) fi) 1197 else 1198 (h (r3 + 0x4w),5w,r73 + 0x3w,r8i,dh,hi2,df, 1199 (r73 + 0x1w =+ 0x2Ew) 1200 ((r73 + 0x2w =+ 0x20w) ((r73 =+ 0x20w) fi)))) = 1201 (h (r3 + 0x4w),5w,r74,r8i,dh,hi2,df,fi2)` by 1202 (Q.UNABBREV_TAC `r74` \\ Q.UNABBREV_TAC `fi2` 1203 \\ Cases_on `isDot a2` \\ ASM_SIMP_TAC std_ss []) 1204 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 1205 \\ Q.UNABBREV_TAC `s2` 1206 \\ Q.ABBREV_TAC `s2 = sexp2string_aux (a2,F)` 1207 \\ Q.ABBREV_TAC `r75 = r74 + n2w (LENGTH s2)` 1208 \\ `(p * one_string r7 p1 r72 * one_string r72 s1 r73 * 1209 one_string r73 s3 r74 * one_space r75 (LENGTH p2) c * 1210 one_space r74 (LENGTH s2) r75) (fun2set (fi2,df))` by 1211 (Q.UNABBREV_TAC `r73` \\ Q.UNABBREV_TAC `r74` 1212 \\ Q.UNABBREV_TAC `r75` 1213 \\ Q.UNABBREV_TAC `fi2` \\ Q.UNABBREV_TAC `s3` 1214 \\ Cases_on `isDot a2` THENL [ 1215 ASM_SIMP_TAC std_ss [one_string_def,MAP,one_list_def] 1216 \\ FULL_SIMP_TAC std_ss [GSYM one_string_def,SEP_CLAUSES] 1217 \\ FULL_SIMP_TAC std_ss [EVAL ``ORD #" "``,LENGTH_APPEND] 1218 \\ FULL_SIMP_TAC std_ss [one_space_ADD,LENGTH] 1219 \\ FULL_SIMP_TAC std_ss [LENGTH,SIMP_RULE std_ss [] 1220 (REWRITE_CONV [one_space_def] ``one_space a (SUC 0) b``)] 1221 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES] 1222 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,STAR_ASSOC] 1223 \\ SEP_WRITE_TAC, 1224 ASM_SIMP_TAC std_ss [one_string_def,MAP,one_list_def] 1225 \\ FULL_SIMP_TAC std_ss [GSYM one_string_def,SEP_CLAUSES] 1226 \\ FULL_SIMP_TAC std_ss [EVAL ``ORD #" "``,LENGTH_APPEND] 1227 \\ FULL_SIMP_TAC std_ss [EVAL ``ORD #"."``,LENGTH_APPEND] 1228 \\ FULL_SIMP_TAC std_ss [one_space_ADD,LENGTH] 1229 \\ FULL_SIMP_TAC std_ss [LENGTH,SIMP_RULE std_ss [] 1230 (REWRITE_CONV [one_space_def] ``one_space a (SUC (SUC (SUC 0))) b``)] 1231 \\ FULL_SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_add_n2w] 1232 \\ FULL_SIMP_TAC std_ss [ADD_ASSOC,SEP_CLAUSES] 1233 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,STAR_ASSOC] 1234 \\ SEP_WRITE_TAC]) 1235 \\ `fun_eq d h hi2` by 1236 (`fun_eq d hi hi2` suffices_by METIS_TAC [fun_eq_def] 1237 \\ SIMP_TAC std_ss [fun_eq_def] 1238 \\ REPEAT STRIP_TAC 1239 \\ Q.UNABBREV_TAC `hi2` 1240 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,IN_DIFF] 1241 \\ Cases_on `b` \\ ASM_SIMP_TAC std_ss [] 1242 \\ `r8 + 8w IN dh DIFF d` by SEP_READ_TAC 1243 \\ Q.UNABBREV_TAC `r8i` 1244 \\ FULL_SIMP_TAC std_ss [IN_DIFF] 1245 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,IN_DIFF] 1246 \\ METIS_TAC []) 1247 \\ `lisp_tree a2 (h (r3 + 4w),d,h) sym` by 1248 (Q.PAT_X_ASSUM `t = Dot a1 a2` ASSUME_TAC 1249 \\ FULL_SIMP_TAC std_ss [lisp_tree_def]) 1250 \\ `lisp_tree a2 (h (r3 + 4w),d,hi2) sym` by METIS_TAC [fun_eq_lisp_tree] 1251 \\ `(q * one (r8,w2) * one (r8 + 0x4w,w1) * 1252 one (r8 + 0x8w,r - 0x4w) * one (r8 + 0xCw,h (r3 + 0x4w)) * 1253 stack_slots (r8 + 0x10w) (MAX (LDEPTH a1) (LDEPTH a2))) 1254 (fun2set (hi,dh DIFF d))` by 1255 FULL_SIMP_TAC (std_ss++star_ss) [] 1256 \\ Q.PAT_X_ASSUM `bb = bbb * fr` (fn th => REWRITE_TAC [GSYM th]) 1257 \\ REVERSE (Cases_on `b`) THEN1 1258 (FULL_SIMP_TAC std_ss [] \\ Q.UNABBREV_TAC `r` 1259 \\ Q.UNABBREV_TAC `r8i` \\ Q.UNABBREV_TAC `hi2` 1260 \\ `(q * one (r8,w2) * one (r8 + 0x4w,w1) * 1261 stack_slots (r8+8w) (SUC (MAX (LDEPTH a1) (LDEPTH a2)))) 1262 (fun2set (hi,dh DIFF d))` by 1263 (FULL_SIMP_TAC std_ss [stack_slots_def,SEP_CLAUSES] 1264 \\ SIMP_TAC std_ss [SEP_EXISTS,word_arith_lemma1] 1265 \\ Q.EXISTS_TAC `5w-4w` 1266 \\ Q.EXISTS_TAC `h (r3 + 4w:word32)` 1267 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 1268 \\ `LDEPTH a2 <= SUC (MAX (LDEPTH a1) (LDEPTH a2))` by 1269 (SIMP_TAC std_ss [MAX_DEF] \\ DECIDE_TAC) 1270 \\ FULL_SIMP_TAC std_ss [LESS_EQ_EXISTS] 1271 \\ FULL_SIMP_TAC std_ss [] 1272 \\ `?fr2. stack_slots (r8 + 8w) (LDEPTH a2 + p') = 1273 stack_slots (r8 + 8w) (LDEPTH a2) * fr2` by 1274 METIS_TAC [stack_slots_ADD] 1275 \\ FULL_SIMP_TAC std_ss [] 1276 \\ `((q * fr2) * one (r8,w2) * one (r8 + 0x4w,w1) * 1277 stack_slots (r8 + 0x8w) (LDEPTH a2)) 1278 (fun2set (hi,dh DIFF d))` by 1279 FULL_SIMP_TAC (std_ss++star_ss) [] 1280 \\ Q.PAT_X_ASSUM `!p w1. bbb` (ASSUME_TAC o 1281 Q.SPECL [`p * one_string r7 p1 r72 * one_string r72 s1 r73 * 1282 one_string r73 s3 r74 * one_space r75 (STRLEN p2) c`, 1283 `w1`,`w2`,`h ((r3:word32)+4w)`,`r74`,`r8`,`hi`,`fi2`]) 1284 \\ POP_ASSUM (ASSUME_TAC o Q.SPECL [`q * fr2`,`r75`]) 1285 \\ POP_ASSUM (ASSUME_TAC o SIMP_RULE std_ss [GSYM AND_IMP_INTRO]) 1286 \\ REPEAT (POP_ASSUM (STRIP_ASSUME_TAC o UNDISCH)) 1287 \\ ASM_SIMP_TAC std_ss [] 1288 \\ `c = r75` by 1289 (Q.UNABBREV_TAC `p2` 1290 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [LENGTH,one_space_def,cond_STAR]) 1291 \\ Q.EXISTS_TAC `hi'` \\ Q.EXISTS_TAC `fi'` 1292 \\ ASM_SIMP_TAC std_ss [] 1293 \\ REVERSE STRIP_TAC THEN1 1294 (ASM_SIMP_TAC std_ss [LDEPTH_def] 1295 \\ FULL_SIMP_TAC (std_ss++star_ss) [] 1296 \\ FULL_SIMP_TAC std_ss [fun_eq_def] \\ METIS_TAC []) 1297 \\ Q.UNABBREV_TAC `p1` \\ Q.UNABBREV_TAC `p2` 1298 \\ FULL_SIMP_TAC std_ss [APPEND,APPEND_NIL] 1299 \\ FULL_SIMP_TAC std_ss [one_string_STRCAT] 1300 \\ Q.UNABBREV_TAC `r75` 1301 \\ Q.UNABBREV_TAC `r74` 1302 \\ REVERSE (Cases_on `r7 = r72`) 1303 \\ FULL_SIMP_TAC std_ss [one_string_def,MAP,one_list_def,SEP_CLAUSES,cond_STAR] 1304 \\ FULL_SIMP_TAC (std_ss++star_ss) [SEP_F_def] 1305 \\ `(if isDot a2 then 0x1w else 0x3w) = n2w (LENGTH s3):word32` by 1306 (Q.UNABBREV_TAC `s3` \\ Cases_on `isDot a2` \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 1307 \\ FULL_SIMP_TAC std_ss [] 1308 \\ Q.UNABBREV_TAC `r73` 1309 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,LENGTH_APPEND] 1310 \\ FULL_SIMP_TAC (std_ss++star_ss) [AC WORD_ADD_ASSOC WORD_ADD_COMM, 1311 LENGTH,one_space_def,SEP_CLAUSES]) 1312 \\ FULL_SIMP_TAC std_ss [] 1313 \\ STRIP_ASSUME_TAC (Q.SPECL [`LDEPTH a2`,`LDEPTH a1`,`r8+16w`] (RW1 [MAX_COMM] stack_slots_MAX)) 1314 \\ Q.UNABBREV_TAC `r8i` 1315 \\ ASM_SIMP_TAC std_ss [LDEPTH_def,stack_slots_def,word_arith_lemma1] 1316 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES] 1317 \\ `(q * fr' * one (r8,w2) * one (r8 + 0x4w,w1) * 1318 one (r8 + 0x8w,3w) * one (r8 + 0xCw,h (r3 + 0x4w)) * 1319 stack_slots (r8 + 0x10w) (LDEPTH a2)) 1320 (fun2set (hi2,dh DIFF d))` by 1321 (Q.UNABBREV_TAC `hi2` \\ Q.UNABBREV_TAC `r` 1322 \\ FULL_SIMP_TAC std_ss [EVAL ``6w-4w:word32``] 1323 \\ SEP_WRITE_TAC) 1324 \\ Q.PAT_X_ASSUM `!p w1. bbb` (ASSUME_TAC o 1325 RW [arm_print_loop1_pre_def,arm_print_loop1_def] o 1326 Q.SPECL [`p * one_string r7 p1 r72 * one_string r72 s1 r73 * 1327 one_string r73 s3 r74 * one_space r75 (STRLEN p2) c`, 1328 `h ((r3:word32)+4w)`,`3w`,`h ((r3:word32)+4w)`,`r74`,`r8+8w`,`hi2`,`fi2`]) 1329 \\ POP_ASSUM (ASSUME_TAC o Q.SPECL [`q * fr' * one (r8,w2) * one (r8 + 0x4w,w1)`,`r75`]) 1330 \\ POP_ASSUM (ASSUME_TAC o SIMP_RULE std_ss [GSYM AND_IMP_INTRO]) 1331 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1] 1332 \\ REPEAT (POP_ASSUM (STRIP_ASSUME_TAC o UNDISCH)) 1333 \\ ASM_SIMP_TAC std_ss [] 1334 \\ ONCE_REWRITE_TAC [arm_print_loop_pre_def,arm_print_loop_def] 1335 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11,EVAL ``3w && 4w:word32``] 1336 \\ SIMP_TAC std_ss [arm_print_loop_aux_def,arm_print_loop_aux_pre_def,arm_print_exit_def,LET_DEF] 1337 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11,WORD_ADD_SUB] 1338 \\ SIMP_TAC std_ss [EVAL ``(w2w:word32->word8) 0x29w``] 1339 \\ ONCE_REWRITE_TAC [WORD_AND_COMM] 1340 \\ ASM_SIMP_TAC std_ss [EVAL ``3w && 4w:word32``] 1341 \\ `c = r75 + 1w` by 1342 (Q.UNABBREV_TAC `p2` 1343 \\ FULL_SIMP_TAC (bool_ss++sep_cond_ss) [one_space_def,LENGTH,SEP_CLAUSES] 1344 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,cond_STAR]) 1345 \\ ASM_SIMP_TAC std_ss [] 1346 \\ `hi' (r8 + 0x4w) = w1` by SEP_READ_TAC 1347 \\ `hi' (r8) = w2` by SEP_READ_TAC 1348 \\ ASM_SIMP_TAC std_ss [] 1349 \\ Q.EXISTS_TAC `hi'` 1350 \\ Q.EXISTS_TAC `(r75 =+ 0x29w) fi'` 1351 \\ ASM_SIMP_TAC std_ss [arm_print_loop1_def,arm_print_loop1_pre_def] 1352 \\ SIMP_TAC std_ss [ALIGNED_INTRO] 1353 \\ `ALIGNED r8 /\ r8 IN dh DIFF d /\ ALIGNED (r8 + 0x4w) /\ r8 + 0x4w IN dh DIFF d` by 1354 (ALIGNED_TAC \\ SEP_READ_TAC) 1355 \\ `r75 IN df` by 1356 (Q.UNABBREV_TAC `p2` 1357 \\ FULL_SIMP_TAC bool_ss [one_space_def,LENGTH_APPEND,one_space_ADD,one_space_def,LENGTH] 1358 \\ FULL_SIMP_TAC std_ss [stack_slots_def,SEP_CLAUSES] 1359 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,lisp_tree_def] 1360 \\ SEP_READ_TAC) 1361 \\ FULL_SIMP_TAC std_ss [IN_DIFF] 1362 \\ REVERSE (REPEAT STRIP_TAC) 1363 THEN1 FULL_SIMP_TAC std_ss [fun_eq_def] 1364 THEN1 1365 (SIMP_TAC std_ss [SEP_EXISTS] 1366 \\ Q.EXISTS_TAC `3w` 1367 \\ Q.EXISTS_TAC `h(r3+4w:word32)` 1368 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 1369 \\ Q.UNABBREV_TAC `p2` 1370 \\ SIMP_TAC std_ss [one_string_STRCAT] 1371 \\ FULL_SIMP_TAC std_ss [one_string_def,one_list_def,MAP,EVAL ``ORD #")"``] 1372 \\ FULL_SIMP_TAC bool_ss [LENGTH,one_space_def,SEP_CLAUSES] 1373 \\ FULL_SIMP_TAC std_ss [GSYM one_string_def,STAR_ASSOC,SEP_EXISTS] 1374 \\ Q.UNABBREV_TAC `r75` 1375 \\ Q.UNABBREV_TAC `r74` 1376 \\ Q.UNABBREV_TAC `r73` 1377 \\ Q.UNABBREV_TAC `r72` 1378 \\ `(if isDot a2 then 0x1w else 0x3w) = n2w (LENGTH s3):word32` by 1379 (Q.UNABBREV_TAC `s3` \\ Cases_on `isDot a2` \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 1380 \\ FULL_SIMP_TAC std_ss [] 1381 \\ FULL_SIMP_TAC (std_ss++star_ss) [SEP_F_def,one_space_def,LENGTH,SEP_CLAUSES] 1382 \\ Q.UNABBREV_TAC `p1` 1383 \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND,word_arith_lemma1] 1384 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM,LENGTH,SEP_CLAUSES] 1385 \\ SEP_WRITE_TAC); 1386 1387val arm_print_loop_sexp = 1388 (Q.GEN `t` o SIMP_RULE bool_ss [GSYM sexp2string_def,LET_DEF] o 1389 Q.SPECL [`t`,`T`]) arm_print_loop_lemma; 1390 1391 1392val (thms,arm_init_stack_def,arm_init_stack_pre_def) = compile_all `` 1393 arm_init_stack (r4:word32,r8:word32,r9:word32) = 1394 if r8 = 0w then 1395 let r8 = r9 in 1396 (r4,r8,r9) 1397 else 1398 let r8 = r9 + r4 in 1399 let r8 = r8 + 8w in 1400 (r4,r8,r9)``; 1401 1402val (arm_print_sexp_thms,arm_print_sexp_def,arm_print_sexp_pre_def) = compile_all `` 1403 arm_print_sexp (r3,r7,r9,dh,h,df,f,dm,m,dg,g) = 1404 let r4 = h (r9 - 0x20w) in 1405 let r8 = h (r9 - 0x1Cw) in 1406 let (r4,r8,r9) = arm_init_stack (r4,r8,r9) in 1407 let r4 = r4 + r4 in 1408 let r4 = r4 + r9 in 1409 let r4 = r4 + 0x18w in 1410 let h = (r4 - 8w =+ r9) h in 1411 let h = (r4 - 4w =+ r7) h in 1412 let r9 = r4 in 1413 let r4 = 0w in 1414 let h = (r8 =+ r4) h in 1415 let r4 = 6w in 1416 let (r3,r4,r7,r8,r9,dh,h,dm,m,dg,g,df,f) = 1417 arm_print_loop (r3,r4,r7,r8,r9,dh,h,dm,m,dg,g,df,f) in 1418 let r3 = h (r9 - 4w) in 1419 let r9 = h (r9 - 8w) in 1420 (r3,r4,r7,r8,r9,dh,h,df,f,dm,m,dg,g)``; 1421 1422val one_space_LESS_EQ = prove( 1423 ``!n a b df f. one_space a n b ((fun2set (f,df)):(word32 # 'a) set) ==> n <= 2**32``, 1424 ONCE_REWRITE_TAC [DECIDE ``n<=m = ~(m+1<=n:num)``] 1425 \\ REPEAT STRIP_TAC 1426 \\ FULL_SIMP_TAC bool_ss [LESS_EQ_EXISTS,GSYM ADD_ASSOC] 1427 \\ FULL_SIMP_TAC std_ss [one_space_ADD] 1428 \\ POP_ASSUM (K ALL_TAC) 1429 \\ POP_ASSUM MP_TAC 1430 \\ REWRITE_TAC [GSYM (EVAL ``SUC 4294967295``),GSYM (EVAL ``SUC 0``)] 1431 \\ SIMP_TAC bool_ss [one_space_def,SEP_CLAUSES] 1432 \\ SIMP_TAC std_ss [SEP_EXISTS] 1433 \\ ONCE_REWRITE_TAC [GSYM n2w_mod] 1434 \\ SIMP_TAC (std_ss++SIZES_ss) [] 1435 \\ REPEAT STRIP_TAC 1436 \\ `~(a = a + 0w)` by SEP_NEQ_TAC 1437 \\ FULL_SIMP_TAC std_ss [WORD_ADD_0]); 1438 1439val ch_active_set2_thm = prove( 1440 ``ch_active_set2 (a,i,n) = { a + n2w (4 * j) | 2 * i <= j /\ j < 2 * n }``, 1441 SIMP_TAC (std_ss++SIZES_ss) [ch_active_set2_def,ch_active_set_def,IN_UNION, 1442 IN_DELETE,WORD_EQ_ADD_CANCEL,n2w_11,GSPECIFICATION,EXTENSION] 1443 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 1444 \\ ASM_SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,WORD_EQ_ADD_CANCEL] 1445 \\ ASM_SIMP_TAC std_ss [word_mul_n2w,word_add_n2w] 1446 THEN1 (Q.EXISTS_TAC `2*j` 1447 \\ SIMP_TAC std_ss [MULT_ASSOC,LEFT_ADD_DISTRIB] \\ DECIDE_TAC) 1448 THEN1 (Q.EXISTS_TAC `1+2*j` 1449 \\ SIMP_TAC std_ss [MULT_ASSOC,LEFT_ADD_DISTRIB] \\ DECIDE_TAC) 1450 \\ `?r q. (j = q * 2 + r) /\ r < 2` by METIS_TAC [DA,DECIDE ``0<2:num``] 1451 \\ Cases_on `r = 1` THENL [ 1452 FULL_SIMP_TAC std_ss [] \\ DISJ2_TAC \\ Q.EXISTS_TAC `q` 1453 \\ SIMP_TAC std_ss [DECIDE ``4 * (q * 2 + 1) = 4 + 8 * q:num``] \\ DECIDE_TAC, 1454 `r = 0` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [DECIDE ``4 * (q * 2) = 8 * q:num``] 1455 \\ DISJ1_TAC \\ Q.EXISTS_TAC `q` \\ SIMP_TAC std_ss [] \\ DECIDE_TAC]); 1456 1457val stack_slots_INTRO = prove( 1458 ``!n a. 8 * n < 2 ** 32 ==> stack_slots a n (fun2set (f,ch_active_set2 (a,0,n)))``, 1459 Induct 1460 \\ SIMP_TAC std_ss [stack_slots_def,emp_def,fun2set_EMPTY] 1461 THEN1 (SIMP_TAC std_ss [EXTENSION,ch_active_set_def,ch_active_set2_def] 1462 \\ SIMP_TAC std_ss [IN_UNION,GSPECIFICATION,NOT_IN_EMPTY]) 1463 \\ SIMP_TAC std_ss [SEP_EXISTS] 1464 \\ SIMP_TAC std_ss [GSYM STAR_ASSOC,one_STAR,IN_fun2set,fun2set_DELETE] 1465 \\ REPEAT STRIP_TAC THENL [ 1466 SIMP_TAC std_ss [ch_active_set2_def,ch_active_set_def,IN_UNION,GSPECIFICATION] 1467 \\ DISJ1_TAC \\ Q.EXISTS_TAC `0` \\ SIMP_TAC std_ss [WORD_ADD_0,word_mul_n2w], 1468 SIMP_TAC (std_ss++SIZES_ss) [ch_active_set2_def,ch_active_set_def,IN_UNION, 1469 IN_DELETE,WORD_EQ_ADD_CANCEL,n2w_11,GSPECIFICATION] 1470 \\ DISJ2_TAC \\ Q.EXISTS_TAC `0` \\ SIMP_TAC std_ss [WORD_ADD_0,word_mul_n2w], 1471 `ch_active_set2 (a,0,SUC n) DELETE a DELETE (a + 0x4w) = 1472 ch_active_set2 (a + 8w,0,n)` by 1473 (SIMP_TAC (std_ss++SIZES_ss) [ch_active_set2_thm,ch_active_set_def,IN_UNION, 1474 IN_DELETE,WORD_EQ_ADD_CANCEL,n2w_11,GSPECIFICATION,EXTENSION] 1475 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 1476 \\ ASM_SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,WORD_EQ_ADD_CANCEL] 1477 \\ ASM_SIMP_TAC std_ss [word_mul_n2w,word_add_n2w] THENL [ 1478 Q.EXISTS_TAC `j - 2` 1479 \\ Cases_on `j = 0` THEN1 FULL_SIMP_TAC std_ss [WORD_ADD_0] 1480 \\ Cases_on `j = 1` THEN1 FULL_SIMP_TAC std_ss [WORD_ADD_0] 1481 \\ `8 + 4 * (j - 2) = 4 * j` by DECIDE_TAC 1482 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC, 1483 Q.EXISTS_TAC `2 + j` 1484 \\ SIMP_TAC std_ss [MULT_ASSOC,LEFT_ADD_DISTRIB] \\ DECIDE_TAC, 1485 FULL_SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,WORD_EQ_ADD_CANCEL,word_add_n2w] 1486 \\ `8 + 4 * j < 4294967296` by DECIDE_TAC 1487 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [n2w_11], 1488 FULL_SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,WORD_EQ_ADD_CANCEL,word_add_n2w] 1489 \\ `8 + 4 * j < 4294967296` by DECIDE_TAC 1490 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] \\ DECIDE_TAC]) 1491 \\ FULL_SIMP_TAC std_ss [] 1492 \\ `8 * n < 4294967296` by DECIDE_TAC 1493 \\ RES_TAC \\ FULL_SIMP_TAC std_ss []]); 1494 1495val fun2set_UPDATE = prove( 1496 ``!a w df f. ~(a IN df) ==> (fun2set ((a =+ w) f,df) = fun2set (f,df))``, 1497 SIMP_TAC std_ss [fun2set_def,EXTENSION,GSPECIFICATION,APPLY_UPDATE_THM] 1498 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 1499 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC []); 1500 1501val DIFF_DIFF_EQ = prove( 1502 ``!d dh. d SUBSET dh ==> (dh DIFF (dh DIFF d) = d)``, 1503 FULL_SIMP_TAC std_ss [EXTENSION,DISJOINT_DEF,IN_INTER,NOT_IN_EMPTY, 1504 SUBSET_DEF,IN_DIFF] \\ METIS_TAC []); 1505 1506val arm_print_sexp_lemma = store_thm("arm_print_sexp_lemma", 1507 ``(one_space r7 (STRLEN (sexp2string t1) + 1) c) (fun2set (f,df)) /\ 1508 lisp_inv (t1,t2,t3,t4,t5,t6,l) (w1,w2,w3,w4,w5,w6,r9,dh,h,sym,rest) ==> 1509 ?r4i r7i r8i hi fi. 1510 arm_print_sexp_pre (w1,r7,r9,dh,h,df,f,rest) /\ 1511 (arm_print_sexp (w1,r7,r9,dh,h,df,f,rest) = 1512 (r7,r4i,r7i,r8i,r9,dh,hi,df,fi,rest)) /\ 1513 (one_string r7 (STRCAT (sexp2string t1) null_string) c) (fun2set (fi,df))``, 1514 STRIP_TAC 1515 \\ IMP_RES_TAC one_space_LESS_EQ 1516 \\ REPEAT (POP_ASSUM MP_TAC) 1517 \\ SIMP_TAC std_ss [one_space_ADD,SEP_EXISTS] 1518 \\ SIMP_TAC bool_ss [GSYM (EVAL ``SUC 0``),one_space_def,SEP_CLAUSES] 1519 \\ SIMP_TAC bool_ss [SEP_EXISTS] 1520 \\ REPEAT STRIP_TAC 1521 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 1522 \\ `LDEPTH t1 <= l` by IMP_RES_TAC lisp_inv_LDEPTH 1523 \\ `?dm m dg g. rest = (dm,m,dg,g)` by METIS_TAC [PAIR] 1524 \\ FULL_SIMP_TAC std_ss [lisp_inv_def,LET_DEF] 1525 \\ SIMP_TAC std_ss [arm_print_sexp_def,arm_print_sexp_pre_def,LET_DEF] 1526 \\ `ALIGNED (r9 - 0x20w) /\ ALIGNED (r9 - 0x1Cw)` by ALIGNED_TAC 1527 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO] 1528 \\ `arm_init_stack (n2w (8 * l),if u then 0x0w else 0x1w,r9) = 1529 (n2w (8 * l),if u then r9 else r9 + 8w * n2w l + 8w,r9)` by 1530 (REVERSE (Cases_on `u`) \\ ASM_SIMP_TAC std_ss [arm_init_stack_def,LET_DEF] 1531 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11,AC WORD_ADD_ASSOC WORD_ADD_COMM,GSYM word_mul_n2w]) 1532 \\ ASM_SIMP_TAC std_ss [] 1533 \\ Q.ABBREV_TAC `a = n2w (8 * l) + n2w (8 * l) + r9 + 0x18w` 1534 \\ Q.ABBREV_TAC `a1 = if u then r9 else r9 + 0x8w * n2w l + 0x8w` 1535 \\ `r9 + (n2w (8 * l) + n2w (8 * l)) + 0x18w = a` by 1536 (Q.UNABBREV_TAC `a` \\ SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC]) 1537 \\ ASM_SIMP_TAC std_ss [] 1538 \\ `ALIGNED a` by 1539 (Q.UNABBREV_TAC `a` 1540 \\ SIMP_TAC bool_ss [DECIDE ``8 * i = 4 * (2 * i):num``] 1541 \\ SIMP_TAC bool_ss [GSYM ADDR32_n2w,GSYM WORD_ADD_ASSOC] 1542 \\ ASM_SIMP_TAC std_ss [ALIGNED_ADD_EQ,ALIGNED_ADDR32,ALIGNED_n2w]) 1543 \\ ASM_SIMP_TAC std_ss [ALIGNED_ADD_EQ,ALIGNED_n2w] 1544 \\ `r9 - 0x20w IN ref_set r9 (l + l + 1) /\ 1545 r9 - 0x1Cw IN ref_set r9 (l + l + 1) /\ 1546 a - 0x8w IN ref_set r9 (l + l + 1) /\ 1547 a - 0x4w IN ref_set r9 (l + l + 1)` by 1548 (SIMP_TAC std_ss [ref_set_def,IN_UNION,GSPECIFICATION] 1549 \\ REPEAT STRIP_TAC 1550 THEN1 (DISJ2_TAC \\ Q.EXISTS_TAC `8` \\ SIMP_TAC std_ss []) 1551 THEN1 (DISJ2_TAC \\ Q.EXISTS_TAC `7` \\ SIMP_TAC std_ss []) 1552 \\ Q.UNABBREV_TAC `a` \\ DISJ1_TAC THENL [ 1553 Q.EXISTS_TAC `2 * (l + l + 1) + 2` 1554 \\ SIMP_TAC std_ss [LEFT_ADD_DISTRIB,MULT_ASSOC] 1555 \\ SIMP_TAC std_ss [word_arith_lemma4] 1556 \\ SIMP_TAC std_ss [GSYM ADD_ASSOC] 1557 \\ SIMP_TAC std_ss [GSYM word_mul_n2w,GSYM word_add_n2w] 1558 \\ SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM], 1559 Q.EXISTS_TAC `2 * (l + l + 1) + 3` 1560 \\ SIMP_TAC std_ss [LEFT_ADD_DISTRIB,MULT_ASSOC] 1561 \\ SIMP_TAC std_ss [word_arith_lemma4] 1562 \\ SIMP_TAC std_ss [GSYM ADD_ASSOC] 1563 \\ SIMP_TAC std_ss [GSYM word_mul_n2w,GSYM word_add_n2w] 1564 \\ SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM]]) 1565 \\ ASM_SIMP_TAC std_ss [] 1566 \\ FULL_SIMP_TAC std_ss [DECIDE ``n + 1 <= 4294967296 = n < 4294967296:num``] 1567 \\ `ALIGNED a1` by 1568 (Q.UNABBREV_TAC `a1` 1569 \\ Cases_on `u` \\ ASM_SIMP_TAC std_ss [] 1570 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_mul_n2w,word_add_n2w] 1571 \\ REWRITE_TAC [DECIDE ``8 * l + 8 = 4 * (2 * l + 2):num``,GSYM ADDR32_n2w] 1572 \\ ASM_SIMP_TAC std_ss [ALIGNED_ADD_EQ,ALIGNED_ADDR32]) 1573 \\ `lisp_tree t1 (w1,ch_active_set2 (r9,if u then 1 + l else 1,i),h) sym` 1574 by IMP_RES_TAC lisp_x_IMP_lisp_tree 1575 \\ Q.ABBREV_TAC `h2 = (a1 =+ 0x0w) ((a - 0x4w =+ r7) ((a - 0x8w =+ r9) h))` 1576 \\ `r9 + 0x10w * n2w l + 0x18w = a` by 1577 (Q.UNABBREV_TAC `a` 1578 \\ SIMP_TAC std_ss [word_add_n2w,DECIDE ``8*l+8*l = 16 * l:num``] 1579 \\ SIMP_TAC std_ss [word_mul_n2w,AC WORD_ADD_COMM WORD_ADD_ASSOC]) 1580 \\ `~(a1 = a - 0x4w) /\ ~(a1 = a - 0x8w)` by 1581 (POP_ASSUM (ASSUME_TAC o GSYM) \\ FULL_SIMP_TAC std_ss [] 1582 \\ Q.UNABBREV_TAC `a1` 1583 \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL] 1584 \\ FULL_SIMP_TAC std_ss [word_sub_def,GSYM WORD_ADD_ASSOC] 1585 \\ FULL_SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,GSYM word_sub_def] 1586 \\ SIMP_TAC std_ss [word_arith_lemma2] 1587 \\ SIMP_TAC std_ss [word_add_n2w,word_mul_n2w] 1588 \\ `16 * l + 20 < 4294967296 /\ 16 * l + 16 < 4294967296` by DECIDE_TAC 1589 \\ `8 * l + 8 < 4294967296` by DECIDE_TAC 1590 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 1591 \\ DECIDE_TAC) 1592 \\ FULL_SIMP_TAC std_ss [GSYM CONJ_ASSOC] 1593 \\ Q.ABBREV_TAC `d = ch_active_set2 (a1,0,SUC l)` 1594 \\ Q.ABBREV_TAC `d2 = ch_active_set2 (r9,if u then 1 + l else 1,i)` 1595 \\ `DISJOINT d d2` by 1596 (SIMP_TAC std_ss [DISJOINT_DEF,EXTENSION,IN_INTER,NOT_IN_EMPTY] 1597 \\ STRIP_TAC \\ Cases_on `x IN d` \\ ASM_SIMP_TAC std_ss [] 1598 \\ Q.UNABBREV_TAC `d` \\ Q.UNABBREV_TAC `d2` 1599 \\ FULL_SIMP_TAC std_ss [ch_active_set_def,ch_active_set2_def] 1600 \\ FULL_SIMP_TAC std_ss [IN_UNION,GSPECIFICATION] 1601 \\ Q.UNABBREV_TAC `a1` \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [] 1602 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,WORD_EQ_ADD_CANCEL] 1603 \\ SIMP_TAC std_ss [word_mul_n2w,word_add_n2w] 1604 THEN1 1605 (REPEAT STRIP_TAC 1606 \\ `8 * j < 4294967296` by DECIDE_TAC 1607 \\ SIMP_TAC std_ss [DISJ_ASSOC] 1608 \\ REWRITE_TAC [METIS_PROVE [] ``c \/ ~b = (b ==> c)``] 1609 \\ NTAC 2 STRIP_TAC 1610 \\ `8 * j' < 4294967296 /\ 4 + 8 * j' < 4294967296` by DECIDE_TAC 1611 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] \\ DECIDE_TAC) 1612 THEN1 1613 (REPEAT STRIP_TAC 1614 \\ `8 * l + (8 + 8 * j) < 4294967296` by DECIDE_TAC 1615 \\ SIMP_TAC std_ss [DISJ_ASSOC] 1616 \\ REWRITE_TAC [METIS_PROVE [] ``c \/ ~b = (b ==> c)``] 1617 \\ NTAC 2 STRIP_TAC 1618 \\ `8 * j' < 4294967296 /\ 4 + 8 * j' < 4294967296` by DECIDE_TAC 1619 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] \\ DECIDE_TAC) 1620 THEN1 1621 (REPEAT STRIP_TAC 1622 \\ `4 + 8 * j < 4294967296 /\ 8 * j < 4294967296` by DECIDE_TAC 1623 \\ SIMP_TAC std_ss [DISJ_ASSOC] 1624 \\ REWRITE_TAC [METIS_PROVE [] ``c \/ ~b = (b ==> c)``] 1625 \\ NTAC 2 STRIP_TAC 1626 \\ `8 * j' < 4294967296 /\ 4 + 8 * j' < 4294967296` by DECIDE_TAC 1627 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] \\ DECIDE_TAC) 1628 THEN1 1629 (REPEAT STRIP_TAC 1630 \\ `8 * l + (8 + (4 + 8 * j)) < 4294967296` by DECIDE_TAC 1631 \\ SIMP_TAC std_ss [DISJ_ASSOC] 1632 \\ REWRITE_TAC [METIS_PROVE [] ``c \/ ~b = (b ==> c)``] 1633 \\ NTAC 2 STRIP_TAC 1634 \\ `8 * j' < 4294967296 /\ 4 + 8 * j' < 4294967296` by DECIDE_TAC 1635 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] \\ DECIDE_TAC)) 1636 \\ REPEAT (Q.PAT_X_ASSUM `lisp_x tt ww sym` (K ALL_TAC)) 1637 \\ Q.PAT_X_ASSUM `!x. bb` (K ALL_TAC) 1638 \\ Q.ABBREV_TAC `c2 = r7 + n2w (STRLEN (sexp2string t1))` 1639 \\ `d2 SUBSET ref_set r9 (l+l+1)` by 1640 (Q.UNABBREV_TAC `d2` 1641 \\ SIMP_TAC std_ss [ch_active_set2_def,SUBSET_DEF,IN_UNION] 1642 \\ SIMP_TAC std_ss [ref_set_def,ch_active_set_def,GSPECIFICATION,IN_UNION] 1643 \\ REPEAT STRIP_TAC \\ DISJ1_TAC \\ ASM_SIMP_TAC std_ss [] 1644 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,WORD_EQ_ADD_CANCEL] 1645 \\ SIMP_TAC std_ss [word_mul_n2w,word_add_n2w] THENL [ 1646 Q.EXISTS_TAC `2 * j` \\ SIMP_TAC std_ss [MULT_ASSOC] 1647 \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC, 1648 Q.EXISTS_TAC `1 + 2 * j` \\ SIMP_TAC std_ss [MULT_ASSOC,LEFT_ADD_DISTRIB] 1649 \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC]) 1650 \\ `d SUBSET ref_set r9 (l+l+1)` by 1651 (Q.UNABBREV_TAC `d` 1652 \\ SIMP_TAC std_ss [ch_active_set2_def,SUBSET_DEF,IN_UNION] 1653 \\ SIMP_TAC std_ss [ref_set_def,ch_active_set_def,GSPECIFICATION,IN_UNION] 1654 \\ Q.UNABBREV_TAC `a1` 1655 \\ REPEAT STRIP_TAC \\ DISJ1_TAC \\ ASM_SIMP_TAC std_ss [] 1656 \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [] 1657 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,WORD_EQ_ADD_CANCEL] 1658 \\ SIMP_TAC std_ss [word_mul_n2w,word_add_n2w] 1659 THEN1 (Q.EXISTS_TAC `2 * j` \\ SIMP_TAC std_ss [MULT_ASSOC] \\ DECIDE_TAC) 1660 THEN1 (Q.EXISTS_TAC `2 * (l + (1 + j))` 1661 \\ SIMP_TAC std_ss [MULT_ASSOC,LEFT_ADD_DISTRIB] \\ DECIDE_TAC) 1662 THEN1 (Q.EXISTS_TAC `1 + 2 * j` 1663 \\ SIMP_TAC std_ss [MULT_ASSOC,LEFT_ADD_DISTRIB] \\ DECIDE_TAC) 1664 THEN1 (Q.EXISTS_TAC `2 * l + (2 + (1 + 2 * j))` 1665 \\ SIMP_TAC std_ss [MULT_ASSOC,LEFT_ADD_DISTRIB] \\ DECIDE_TAC)) 1666 \\ Q.PAT_X_ASSUM `dh = ref_set r9 (l + l + 1)` (ASSUME_TAC o GSYM) 1667 \\ FULL_SIMP_TAC std_ss [] 1668 \\ `8 * (SUC l) < 2 ** 32` by (FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC) 1669 \\ IMP_RES_TAC stack_slots_INTRO 1670 \\ POP_ASSUM (ASSUME_TAC o Q.SPECL [`h`,`a1`]) 1671 \\ Q.UNABBREV_TAC `d` 1672 \\ Q.ABBREV_TAC `d = ch_active_set2 (a1,0,SUC l)` 1673 \\ FULL_SIMP_TAC std_ss [stack_slots_def,SEP_EXISTS] 1674 \\ `a1 IN d` by SEP_READ_TAC 1675 \\ `a1 IN dh` by METIS_TAC [SUBSET_DEF] 1676 \\ ASM_SIMP_TAC std_ss [] 1677 \\ `~(a - 0x4w IN d) /\ ~(a - 0x8w IN d)` by 1678 (Q.PAT_X_ASSUM `r9 + 0x10w * n2w l + 0x18w = a` (ASSUME_TAC o GSYM) 1679 \\ FULL_SIMP_TAC std_ss [] 1680 \\ Q.UNABBREV_TAC `d` \\ Q.UNABBREV_TAC `a1` 1681 \\ SIMP_TAC std_ss [ch_active_set2_thm,GSPECIFICATION] 1682 \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [] 1683 \\ SIMP_TAC std_ss [word_sub_def] 1684 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,WORD_EQ_ADD_CANCEL] 1685 \\ SIMP_TAC std_ss [word_mul_n2w,word_add_n2w] 1686 \\ REPEAT STRIP_TAC 1687 \\ SIMP_TAC std_ss [GSYM word_sub_def,word_arith_lemma2,word_add_n2w] 1688 \\ `16 * l + 20 < 4294967296 /\ 16 * l + 16 < 4294967296` by DECIDE_TAC 1689 \\ SIMP_TAC std_ss [DISJ_ASSOC] 1690 \\ REWRITE_TAC [METIS_PROVE [] ``c \/ ~b = (b ==> c)``] 1691 \\ STRIP_TAC THENL [ 1692 `4 * j < 4294967296` by DECIDE_TAC 1693 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [MULT_ASSOC,LEFT_ADD_DISTRIB,n2w_11] 1694 \\ DECIDE_TAC, 1695 `4 * j < 4294967296` by DECIDE_TAC 1696 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [MULT_ASSOC,LEFT_ADD_DISTRIB,n2w_11] 1697 \\ DECIDE_TAC, 1698 `8 * l + (8 + 4 * j) < 4294967296` by DECIDE_TAC 1699 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [MULT_ASSOC,LEFT_ADD_DISTRIB,n2w_11] 1700 \\ DECIDE_TAC, 1701 `8 * l + (8 + 4 * j) < 4294967296` by DECIDE_TAC 1702 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [MULT_ASSOC,LEFT_ADD_DISTRIB,n2w_11] 1703 \\ DECIDE_TAC]) 1704 \\ `(one (a1,y') * one (a1 + 0x4w,y'') * stack_slots (a1 + 0x8w) l) 1705 (fun2set (((a - 0x4w =+ r7) ((a - 0x8w =+ r9) h)),d))` by 1706 ASM_SIMP_TAC std_ss [fun2set_UPDATE] 1707 \\ `(one (a1,0w) * one (a1 + 0x4w,y'') * stack_slots (a1 + 0x8w) l) 1708 (fun2set (h2,d))` by 1709 (Q.UNABBREV_TAC `h2` 1710 \\ Q.ABBREV_TAC `h3 = (a - 0x4w =+ r7) ((a - 0x8w =+ r9) h)` 1711 \\ SEP_WRITE_TAC) 1712 \\ STRIP_ASSUME_TAC (Q.SPECL [`LDEPTH t1`,`l`,`a1+8w`] stack_slots_MAX) 1713 \\ `MAX (LDEPTH t1) l = l` by (ASM_SIMP_TAC std_ss [MAX_DEF] \\ DECIDE_TAC) 1714 \\ FULL_SIMP_TAC std_ss [] 1715 \\ `(fr * one (a1,0w) * one (a1 + 0x4w,y'') * stack_slots (a1 + 0x8w) (LDEPTH t1)) 1716 (fun2set (h2,d)) /\ 1717 (one (c2,y) * one_space r7 (STRLEN (sexp2string t1)) c2) 1718 (fun2set (f,df))` by (FULL_SIMP_TAC (std_ss++star_ss) [] \\ DECIDE_TAC) 1719 \\ Q.ABBREV_TAC `d3 = dh DIFF d` 1720 \\ `dh DIFF d3 = d` by (Q.UNABBREV_TAC `d3` \\ ASM_SIMP_TAC std_ss [DIFF_DIFF_EQ]) 1721 \\ `(fr * one (a1,0w) * one (a1 + 0x4w,y'') * stack_slots (a1 + 0x8w) (LDEPTH t1)) 1722 (fun2set (h2,dh DIFF d3))` by (FULL_SIMP_TAC (std_ss++star_ss) [] \\ DECIDE_TAC) 1723 \\ `d3 SUBSET dh` by (Q.UNABBREV_TAC `d3` \\ SIMP_TAC std_ss [SUBSET_DEF,IN_DIFF]) 1724 \\ `d2 SUBSET d3` by 1725 (Q.UNABBREV_TAC `d3` 1726 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,IN_DIFF,DISJOINT_DEF,IN_INTER,EXTENSION,NOT_IN_EMPTY] 1727 \\ METIS_TAC []) 1728 \\ MP_TAC ((Q.INST [`r9`|->`a`,`d`|->`d3`] o 1729 Q.SPECL [`t1`,`one (c2,y)`,`y''`,`0w`,`w1`,`r7`,`a1`,`h2`,`f`,`fr`,`c2`]) 1730 arm_print_loop_sexp) 1731 \\ `~(a - 0x4w IN d2) /\ ~(a - 0x8w IN d2)` by 1732 (Q.PAT_X_ASSUM `r9 + 0x10w * n2w l + 0x18w = a` (ASSUME_TAC o GSYM) 1733 \\ FULL_SIMP_TAC std_ss [] 1734 \\ Q.UNABBREV_TAC `d2` \\ Q.UNABBREV_TAC `a1` 1735 \\ SIMP_TAC std_ss [ch_active_set2_thm,GSPECIFICATION] 1736 \\ REPEAT (Q.PAT_X_ASSUM `bbb (fun2set(ff,fff))` (K ALL_TAC)) 1737 \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [] 1738 \\ SIMP_TAC std_ss [word_sub_def] 1739 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,WORD_EQ_ADD_CANCEL] 1740 \\ SIMP_TAC std_ss [word_mul_n2w,word_add_n2w] 1741 \\ REPEAT STRIP_TAC 1742 \\ SIMP_TAC std_ss [GSYM word_sub_def,word_arith_lemma2,word_add_n2w] 1743 \\ `16 * l + 20 < 4294967296 /\ 16 * l + 16 < 4294967296` by DECIDE_TAC 1744 \\ SIMP_TAC std_ss [DISJ_ASSOC] 1745 \\ REWRITE_TAC [METIS_PROVE [] ``c \/ ~b = (b ==> c)``] 1746 \\ STRIP_TAC \\ STRIP_TAC 1747 \\ `4 * j < 4294967296` by DECIDE_TAC 1748 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [MULT_ASSOC,LEFT_ADD_DISTRIB,n2w_11] 1749 \\ DECIDE_TAC) 1750 \\ `lisp_tree t1 (w1,d2,h2) sym` by 1751 (Q.UNABBREV_TAC `h2` 1752 \\ `~(a1 IN d2)` by METIS_TAC [DISJOINT_DEF,IN_INTER,NOT_IN_EMPTY,EXTENSION] 1753 \\ ASM_SIMP_TAC std_ss [NOT_IN_lisp_tree]) 1754 \\ IMP_RES_TAC lisp_tree_SUBSET 1755 \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC 1756 \\ ASM_SIMP_TAC std_ss [] 1757 \\ SIMP_TAC std_ss [arm_print_loop1_pre_def,arm_print_loop1_def] 1758 \\ ONCE_REWRITE_TAC [arm_print_loop_pre_def,arm_print_loop_def] 1759 \\ ASM_SIMP_TAC std_ss [LET_DEF,w2w_0] 1760 \\ SIMP_TAC std_ss [one_string_STRCAT,null_string_def] 1761 \\ `c2 IN df` by SEP_READ_TAC 1762 \\ FULL_SIMP_TAC std_ss [one_string_def,one_list_def,MAP,EVAL ``ORD #"\^@"``] 1763 \\ SIMP_TAC std_ss [SEP_CLAUSES,CONJ_ASSOC] 1764 \\ REVERSE STRIP_TAC THEN1 SEP_WRITE_TAC 1765 \\ `a - 0x4w IN d3 /\ a - 0x8w IN d3` by 1766 (Q.UNABBREV_TAC `d3` \\ ASM_SIMP_TAC std_ss [IN_DIFF]) 1767 \\ `(hi (a - 0x4w) = h2 (a - 0x4w)) /\ (hi (a - 0x8w) = h2 (a - 0x8w))` by FULL_SIMP_TAC std_ss [fun_eq_def] 1768 \\ ASM_SIMP_TAC std_ss [] 1769 \\ Q.UNABBREV_TAC `h2` 1770 \\ REPEAT (Q.PAT_X_ASSUM `bbb (fun2set(ff,fff))` (K ALL_TAC)) 1771 \\ SIMP_TAC std_ss [APPLY_UPDATE_THM] 1772 \\ ASM_SIMP_TAC std_ss [word_sub_def,word_2comp_n2w] 1773 \\ SIMP_TAC (std_ss++SIZES_ss) [WORD_EQ_ADD_CANCEL,n2w_11]); 1774 1775(* 1776 1777set_trace "Goalstack.print_goal_at_top" 1 1778set_trace "Goalstack.print_goal_at_top" 0 1779 1780*) 1781 1782val (arm_sexp2string_th,arm_sexp2string_def,arm_sexp2string_pre_def) = compile "arm" `` 1783 arm_sexp2string (r1,r3,r9,dh,h,df,f,dm,m,dg,g) = 1784 let r7 = r1 in 1785 let (r3,r4,r7,r8,r9,dh,h,df,f,dm,m,dg,g) = 1786 arm_print_sexp (r3,r7,r9,dh,h,df,f,dm,m,dg,g) in 1787 let r3 = r1 in 1788 (r3,dh,h,df,f,dm,m,dg,g)``; 1789 1790val (ppc_sexp2string_th,ppc_sexp2string_def,ppc_sexp2string_pre_def) = compile "ppc" `` 1791 ppc_sexp2string (r1,r3,r9,dh,h,df,f,dm,m,dg,g) = 1792 let r7 = r1 in 1793 let (r3,r4,r7,r8,r9,dh,h,df,f,dm,m,dg,g) = 1794 arm_print_sexp (r3,r7,r9,dh,h,df,f,dm,m,dg,g) in 1795 let r3 = r1 in 1796 (r3,dh,h,df,f,dm,m,dg,g)``; 1797 1798fun save_all prefix postfix = 1799 map (fn (n,th) => save_thm(prefix ^ n ^ postfix,th)); 1800 1801val _ = save_all "" "_sexp2string_thm" 1802 ([("arm",arm_sexp2string_th),("ppc",ppc_sexp2string_th)] @ 1803 filter (fn (n,th) => n = "x86") arm_print_sexp_thms); 1804 1805 1806val _ = export_theory(); 1807