1open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_parse"; 2 3open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory; 4open combinTheory finite_mapTheory stringTheory relationTheory; 5 6open lisp_sexpTheory; 7 8(* file structure: 9 1. we first define how to print s-expressions, then 10 2. we define a function which parses printed s-expressions. 11*) 12 13infix \\ 14val op \\ = op THEN; 15val RW = REWRITE_RULE; 16val RW1 = ONCE_REWRITE_RULE; 17 18val TOKEN_OPEN = ``(Val 0, Val 1)`` 19val TOKEN_DOT = ``(Val 1, Val 1)`` 20val TOKEN_CLOSE = ``(Val 2, Val 1)`` 21val TOKEN_QUOTE = ``(Val 3, Val 1)`` 22val TOKEN_SAVE = ``(Val index, Val 2)`` 23val TOKEN_LOAD = ``(Val index, Val 3)`` 24val NO_TOKEN = ``(Sym "NIL", Sym "NIL")`` 25 26val SExp_print_induct = store_thm("SExp_print_induct", 27 ``!P. (!x. (if isQuote x then P (CAR (CDR x)) else 28 if isDot x then P (CAR x) /\ P (CDR x) else T) ==> P x) ==> 29 !x. P x``, 30 REPEAT STRIP_TAC \\ completeInduct_on `LSIZE x` 31 \\ REPEAT STRIP_TAC 32 \\ Cases_on `isQuote x` 33 \\ Q.PAT_X_ASSUM `!x. bbb ==> P x` MATCH_MP_TAC THEN1 34 (ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [isQuote_thm,CAR_def,CDR_def] 35 \\ FULL_SIMP_TAC std_ss [LSIZE_def,ADD1,GSYM ADD_ASSOC]) 36 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 37 \\ FULL_SIMP_TAC std_ss [isDot_thm,CAR_def,CDR_def,LSIZE_def] 38 \\ FULL_SIMP_TAC std_ss [isDot_thm,CAR_def,CDR_def,LSIZE_def] 39 \\ METIS_TAC [DECIDE ``n < SUC (m + n)``,ADD_COMM]); 40 41 42(* Part 1 - section 1: print s-expressions *) 43 44val LIST_STRCAT_def = Define ` 45 (LIST_STRCAT [] = "") /\ 46 (LIST_STRCAT (x::xs) = STRCAT x (LIST_STRCAT xs))`; 47 48val dec2str_def = Define `dec2str n = STRING (CHR (n + 48)) ""`; 49 50val num2str_def = tDefine "num2str" ` 51 num2str n = 52 if n DIV 10 = 0 then dec2str (n MOD 10) else 53 STRCAT (num2str (n DIV 10)) (dec2str (n MOD 10))` 54 (Q.EXISTS_TAC `measure I` 55 \\ SIMP_TAC std_ss [prim_recTheory.WF_measure] 56 \\ SIMP_TAC std_ss [prim_recTheory.measure_thm] 57 \\ STRIP_TAC 58 \\ STRIP_ASSUME_TAC (Q.SPEC `n` (MATCH_MP DA (DECIDE ``0 < 10:num``))) 59 \\ ASM_SIMP_TAC std_ss [DIV_MULT] 60 \\ DECIDE_TAC); 61 62val number_char_def = Define ` 63 number_char c = 48 <= ORD c /\ ORD c < 58`; 64 65val space_char_def = Define ` 66 space_char c = ORD c <= 32`; 67 68val identifier_char_def = Define ` 69 identifier_char c = 42 <= ORD c /\ ~(ORD c = 46) /\ ~(ORD c = 59) /\ ~(ORD c = 124)`; 70 71val identifier_string_def = Define ` 72 identifier_string s = 73 ~(s = "") /\ EVERY identifier_char s /\ ~number_char (HD s)`; 74 75val sym2str_aux_def = Define ` 76 (sym2str_aux [] = []) /\ 77 (sym2str_aux (x::xs) = 78 if (ORD x = 0) then (#"\\")::(#"0")::sym2str_aux xs else 79 if MEM x [#"|";#"\\"] 80 then #"\\"::x::sym2str_aux xs else x::sym2str_aux xs)`; 81 82val is_lower_case_def = Define ` 83 is_lower_case c = #"a" <= c /\ c <= #"z"`; 84 85val upper_case_def = Define ` 86 upper_case c = if is_lower_case c then CHR (ORD c - 32) else c`; 87 88val sym2str_def = Define ` 89 sym2str s = 90 if identifier_string s /\ EVERY (\c. ~(is_lower_case c)) s 91 then s else "|" ++ sym2str_aux s ++ "|"`; 92 93val sexp2string_aux_def = tDefine "sexp2string_aux" ` 94 (sexp2string_aux (Val n, b) = num2str n) /\ 95 (sexp2string_aux (Sym s, b) = sym2str s) /\ 96 (sexp2string_aux (Dot x y, b) = 97 if isQuote (Dot x y) then LIST_STRCAT ["'"; sexp2string_aux (CAR y,T)] else 98 let (a,e) = if b then ("(",")") else ("","") in 99 if y = Sym "NIL" then LIST_STRCAT [a; sexp2string_aux (x,T); e] else 100 if isDot y /\ ~(isQuote y) 101 then LIST_STRCAT [a; sexp2string_aux (x,T); " "; sexp2string_aux (y,F); e] 102 else LIST_STRCAT [a; sexp2string_aux (x,T); " . "; sexp2string_aux (y,F); e])` 103 (WF_REL_TAC `measure (LSIZE o FST)` \\ REWRITE_TAC [LSIZE_def,ADD1] 104 \\ REPEAT STRIP_TAC 105 \\ FULL_SIMP_TAC std_ss [isQuote_thm,SExp_11,CAR_def,LSIZE_def] 106 \\ DECIDE_TAC); 107 108val sexp2string_def = Define `sexp2string x = sexp2string_aux (x, T)`; 109 110 111(* Part 1 - section 2: printing s-expressions with abbreviations *) 112 113val isAtom_def = Define ` 114 isAtom abbrevs s = ~isDot s \/ isQuote s \/ s IN FDOM abbrevs`; 115 116val sexp2abbrev_aux_def = tDefine "sexp2abbrev_aux" ` 117 sexp2abbrev_aux s b abbrevs ps = 118 let index = abbrevs ' s in 119 let prefix = (if s IN FDOM abbrevs then "#" ++ (num2str index) ++ "=" else "") in 120 if s IN FDOM abbrevs /\ s IN ps then 121 ("#" ++ (num2str index) ++ "#", ps) 122 else 123 if isVal s then (prefix ++ num2str (getVal s), if s IN FDOM abbrevs then s INSERT ps else ps) else 124 if isSym s then (prefix ++ sym2str (getSym s), if s IN FDOM abbrevs then s INSERT ps else ps) else 125 if isQuote s then 126 let (str2,ps2) = sexp2abbrev_aux (CAR (CDR s)) T abbrevs ps in 127 (prefix ++ "'" ++ str2, 128 if s IN FDOM abbrevs then s INSERT ps2 else ps2) 129 else 130 let b = b \/ ~(prefix = "") in 131 let (s1,s2) = (if b then ("(",")") else ("","")) in 132 let (str1,ps1) = sexp2abbrev_aux (CAR s) T abbrevs ps in 133 let (str2,ps2) = sexp2abbrev_aux (CDR s) F abbrevs ps1 in 134 ((prefix ++ s1 ++ str1 ++ 135 (if CDR s = Sym "NIL" then "" else 136 (if isAtom abbrevs (CDR s) then " . " else " ") ++ 137 str2) ++ s2), 138 if CDR s = Sym "NIL" 139 then if s IN FDOM abbrevs then s INSERT ps1 else ps1 140 else if s IN FDOM abbrevs then s INSERT ps2 else ps2)` 141 (WF_REL_TAC `measure (\(s,b,abbrevs,ps). LSIZE s)` \\ SRW_TAC [] [] 142 \\ `isDot s` by (Cases_on `s` \\ FULL_SIMP_TAC std_ss [isVal_def,isDot_def,isSym_def]) 143 \\ FULL_SIMP_TAC std_ss [isQuote_thm,isDot_thm,CDR_def,CAR_def,LSIZE_def] 144 \\ FULL_SIMP_TAC std_ss [SExp_11,LSIZE_def,CAR_def,CDR_def] 145 \\ DECIDE_TAC); 146 147val sexp_abbrev_fmap_def = Define ` 148 (sexp_abbrev_fmap [] n = FEMPTY) /\ 149 (sexp_abbrev_fmap (x::xs) n = sexp_abbrev_fmap xs (n+1) |+ (x:SExp,n))`; 150 151val sexp2abbrev_def = Define ` 152 sexp2abbrev s abbrevs = FST (sexp2abbrev_aux s T (sexp_abbrev_fmap abbrevs 0) {})`; 153 154val sexp2abbrev_aux_EQ_sexp2string_aux = prove( 155 ``!s b. sexp2abbrev_aux s b FEMPTY {} = (sexp2string_aux (s,b),{})``, 156 HO_MATCH_MP_TAC SExp_print_induct \\ REPEAT STRIP_TAC 157 \\ ONCE_REWRITE_TAC [sexp2abbrev_aux_def] 158 \\ SIMP_TAC std_ss [NOT_IN_EMPTY,FDOM_FEMPTY,LET_DEF] 159 \\ Cases_on `isVal s` \\ ASM_SIMP_TAC std_ss [APPEND] 160 THEN1 (FULL_SIMP_TAC std_ss [isVal_thm,getVal_def,sexp2string_aux_def]) 161 \\ Cases_on `isSym s` \\ ASM_SIMP_TAC std_ss [APPEND] 162 THEN1 (FULL_SIMP_TAC std_ss [isSym_thm,getSym_def,sexp2string_aux_def]) 163 \\ Cases_on `isQuote s` \\ ASM_SIMP_TAC std_ss [APPEND] THEN1 164 (FULL_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [isQuote_thm] 165 \\ SIMP_TAC std_ss [sexp2string_aux_def,isQuote_def,CAR_def,CDR_def, 166 isDot_def,LIST_STRCAT_def,APPEND_NIL,APPEND]) 167 \\ `isDot s` by (Cases_on `s` \\ FULL_SIMP_TAC std_ss [isDot_def,isVal_def,isSym_def]) 168 \\ FULL_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [isDot_thm] 169 \\ FULL_SIMP_TAC std_ss [sexp2string_aux_def,CAR_def,CDR_def,LIST_STRCAT_def] 170 \\ Cases_on `b` \\ FULL_SIMP_TAC std_ss [LET_DEF,isAtom_def,FDOM_FEMPTY,NOT_IN_EMPTY] 171 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss []); 172 173val sexp2abbrev_NIL = prove( 174 ``!s. sexp2abbrev s [] = sexp2string s``, 175 SIMP_TAC std_ss [sexp2abbrev_def,sexp2string_def,sexp_abbrev_fmap_def, 176 sexp2abbrev_aux_EQ_sexp2string_aux]); 177 178(* 179 180val list2sexp_def = Define ` 181 (list2sexp [] = Sym "NIL") /\ 182 (list2sexp (x::xs) = Dot x (list2sexp xs))`; 183 184val A1 = Define `A1 = list2sexp [Sym "a"; Val 4]`; 185val A2 = Define `A2 = list2sexp [Sym "b"; Sym "c"]`; 186 187EVAL ``sexp2abbrev (list2sexp [A1;Dot A1 A2;list2sexp [Sym "QUOTE"; A2]]) [A1;A2]`` 188 189*) 190 191val sexp2abbrevt_aux_def = tDefine "sexp2abbrevt_aux" ` 192 sexp2abbrevt_aux s b abbrevs ps = 193 let index = abbrevs ' s in 194 let prefix = (if s IN FDOM abbrevs then [^TOKEN_SAVE] else []) in 195 if s IN FDOM abbrevs /\ s IN ps then 196 ([(^TOKEN_LOAD)], ps) 197 else 198 if ~(isDot s) then (prefix ++ [(s,Val 0)], if s IN FDOM abbrevs then s INSERT ps else ps) else 199 if isQuote s then 200 let (str2,ps2) = sexp2abbrevt_aux (CAR (CDR s)) T abbrevs ps in 201 (prefix ++ [^TOKEN_QUOTE] ++ str2, 202 if s IN FDOM abbrevs then s INSERT ps2 else ps2) 203 else 204 let b = b \/ ~(prefix = []) in 205 let (s1,s2) = (if b then ([^TOKEN_OPEN],[^TOKEN_CLOSE]) else ([],[])) in 206 let (str1,ps1) = sexp2abbrevt_aux (CAR s) T abbrevs ps in 207 let (str2,ps2) = sexp2abbrevt_aux (CDR s) F abbrevs ps1 in 208 ((prefix ++ s1 ++ str1 ++ 209 (if CDR s = Sym "NIL" then [] else 210 (if isAtom abbrevs (CDR s) then [^TOKEN_DOT] else []) ++ 211 str2) ++ s2), 212 if CDR s = Sym "NIL" 213 then if s IN FDOM abbrevs then s INSERT ps1 else ps1 214 else if s IN FDOM abbrevs then s INSERT ps2 else ps2)` 215 (WF_REL_TAC `measure (\(s,b,abbrevs,ps). LSIZE s)` \\ SRW_TAC [] [] 216 \\ `isDot s` by (Cases_on `s` \\ FULL_SIMP_TAC std_ss [isVal_def,isDot_def,isSym_def]) 217 \\ FULL_SIMP_TAC std_ss [isQuote_thm,isDot_thm,CDR_def,CAR_def,LSIZE_def] 218 \\ FULL_SIMP_TAC std_ss [SExp_11,LSIZE_def,CAR_def,CDR_def] 219 \\ DECIDE_TAC) 220 221 222 223(* Part 2 - section 1: reading tokens from a string, i.e. lexing or scanning *) 224 225val read_while_def = Define ` 226 (read_while P "" s = (s,"")) /\ 227 (read_while P (STRING c cs) s = 228 if P c then read_while P cs (STRCAT s (STRING c "")) 229 else (s,STRING c cs))`; 230 231val read_while_thm = prove( 232 ``!cs s cs' s'. 233 (read_while P cs s = (s',cs')) ==> LENGTH cs' <= LENGTH cs + LENGTH s``, 234 Induct \\ SIMP_TAC std_ss [read_while_def] 235 \\ REPEAT STRIP_TAC 236 \\ Cases_on `P h` \\ FULL_SIMP_TAC std_ss [LENGTH] 237 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_APPEND] 238 \\ REPEAT (Q.PAT_X_ASSUM `STRING c cs = cs'` (ASSUME_TAC o GSYM)) 239 \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_APPEND] \\ DECIDE_TAC); 240 241val str2num_def = Define ` 242 (str2num "" = 0) /\ 243 (str2num (STRING c s) = (ORD c - 48) * 10 ** (LENGTH s) + str2num s)`; 244 245val str2num_dec2str = prove( 246 ``!n. n < 10 ==> (str2num (dec2str n) = n) /\ ~(dec2str n = "") /\ 247 EVERY number_char (dec2str n)``, 248 SRW_TAC [] [dec2str_def,str2num_def,LENGTH,ORD_CHR,number_char_def] 249 \\ `n + 48 < 256` by DECIDE_TAC 250 \\ IMP_RES_TAC ORD_CHR 251 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC); 252 253val str2num_STRCAT = prove( 254 ``!s c. str2num (STRCAT s (STRING c "")) = str2num s * 10 + str2num (STRING c "")``, 255 Induct \\ ASM_SIMP_TAC std_ss [str2num_def,STRCAT_def,LENGTH_APPEND, 256 LENGTH,EXP_ADD,RIGHT_ADD_DISTRIB,AC MULT_ASSOC MULT_COMM, AC ADD_ASSOC ADD_COMM]); 257 258val dec2str_lemma = prove( 259 ``?c. dec2str r = STRING c ""``, 260 SRW_TAC [] [dec2str_def,str2num_def,LENGTH]); 261 262val str2num_num2str = store_thm("str2num_num2str", 263 ``!n. (str2num (num2str n) = n) /\ ~((num2str n) = "") /\ 264 EVERY number_char (num2str n)``, 265 completeInduct_on `n` \\ Cases_on `n < 10` THEN1 266 (IMP_RES_TAC LESS_DIV_EQ_ZERO \\ ONCE_REWRITE_TAC [num2str_def] 267 \\ ASM_SIMP_TAC std_ss [str2num_dec2str]) 268 \\ STRIP_ASSUME_TAC (Q.SPEC `n` (MATCH_MP DA (DECIDE ``0 < 10:num``))) 269 \\ ONCE_REWRITE_TAC [num2str_def] 270 \\ ASM_SIMP_TAC std_ss [DIV_MULT] 271 \\ Cases_on `q = 0` THEN1 (FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC) 272 \\ ASM_SIMP_TAC std_ss [MOD_TIMES,STRCAT_EQ_EMPTY,EVERY_APPEND] 273 \\ ASM_SIMP_TAC std_ss [str2num_dec2str,str2num_STRCAT] 274 \\ `q < n` by DECIDE_TAC \\ RES_TAC 275 \\ STRIP_ASSUME_TAC dec2str_lemma 276 \\ ASM_SIMP_TAC std_ss [str2num_STRCAT] 277 \\ METIS_TAC [str2num_dec2str]); 278 279val str2sym_aux_def = Define ` 280 (str2sym_aux [] b = ("",[])) /\ 281 (str2sym_aux (c::cs) T = 282 let (x1,x2) = str2sym_aux cs F in ((if c = #"0" then CHR 0 else c)::x1,x2)) /\ 283 (str2sym_aux (c::cs) F = 284 if c = #"\\" then str2sym_aux cs T else 285 if c = #"|" then ("",cs) else 286 let (x1,x2) = str2sym_aux cs F in (c::x1,x2))`; 287 288val str2sym_def = Define ` 289 (str2sym "" = ("","")) /\ 290 (str2sym (c::cs) = 291 if c = #"|" then 292 (let (ident,cs) = str2sym_aux cs F 293 in 294 ((ident,cs))) 295 else 296 (let (ident,cs1) = read_while identifier_char cs "" in 297 let ident = MAP upper_case (c :: ident) 298 in 299 ((ident,cs1))))`; 300 301val str2sym_aux_sym2str_aux = prove( 302 ``!s. str2sym_aux (sym2str_aux s ++ "|" ++ ts) F = (s,ts)``, 303 Induct \\ SRW_TAC [] [str2sym_aux_def,sym2str_aux_def,MEM] 304 \\ FULL_SIMP_TAC std_ss [] 305 \\ Cases_on `h` \\ FULL_SIMP_TAC std_ss [ORD_CHR]); 306 307val next_token_def = tDefine "next_token" ` 308 (next_token "" = (^NO_TOKEN,"")) /\ 309 (next_token (c::cs) = 310 if space_char c then next_token cs else 311 if c = #"(" then (^TOKEN_OPEN,cs) else 312 if c = #"." then (^TOKEN_DOT,cs) else 313 if c = #")" then (^TOKEN_CLOSE,cs) else 314 if c = #"'" then (^TOKEN_QUOTE,cs) else 315 if c = #"#" then 316 (let (index_str,cs) = read_while number_char cs "" in 317 let index = str2num index_str in 318 if cs = "" then (^NO_TOKEN,"") else 319 if HD cs = #"#" then (^TOKEN_LOAD,TL cs) else 320 if HD cs = #"=" then (^TOKEN_SAVE,TL cs) else (^NO_TOKEN,TL cs)) else 321 if number_char c then 322 (let (index_str,cs) = read_while number_char cs "" in 323 let index = str2num (c::index_str) in 324 ((Val index, Val 0),cs)) else 325 if c = #";" then 326 (let cs = SND (read_while (\x. ~(x = #"\n")) cs "") in 327 next_token cs) 328 else let (ident,cs) = str2sym (c::cs) in 329 ((Sym ident, Val 0),cs))` 330 (WF_REL_TAC `measure LENGTH` \\ SIMP_TAC std_ss [LENGTH] \\ REPEAT STRIP_TAC 331 \\ Cases_on `read_while (\x. x <> #"\n") cs ""` \\ IMP_RES_TAC read_while_thm 332 \\ FULL_SIMP_TAC std_ss [LENGTH] \\ DECIDE_TAC); 333 334val is_eof_def = tDefine "is_eof" ` 335 (is_eof "" = (T,"")) /\ 336 (is_eof (c::cs) = 337 if space_char c then is_eof cs else 338 if c = #";" then 339 (let cs = SND (read_while (\x. ~(x = #"\n")) cs "") in 340 is_eof cs) 341 else (F,c::cs))` 342 (WF_REL_TAC `measure LENGTH` \\ SIMP_TAC std_ss [LENGTH] \\ REPEAT STRIP_TAC 343 \\ Cases_on `read_while (\x. x <> #"\n") cs ""` \\ IMP_RES_TAC read_while_thm 344 \\ FULL_SIMP_TAC std_ss [LENGTH] \\ DECIDE_TAC); 345 346val str2sym_aux_LENGTH = prove( 347 ``!s b t x. (str2sym_aux s b = (x,t)) ==> LENGTH t <= LENGTH s``, 348 Induct \\ SRW_TAC [] [str2sym_aux_def] \\ SRW_TAC [] [] 349 \\ Cases_on `b`\\ FULL_SIMP_TAC std_ss [str2sym_aux_def] 350 \\ POP_ASSUM MP_TAC 351 \\ `?a1 a2. str2sym_aux s F = (a1,a2)` by METIS_TAC [PAIR] 352 \\ `?b1 b2. str2sym_aux s T = (b1,b2)` by METIS_TAC [PAIR] 353 \\ FULL_SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC 354 \\ REPEAT (Q.PAT_X_ASSUM `bbb = t` (ASSUME_TAC o GSYM)) 355 THEN1 (RES_TAC \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC) 356 \\ POP_ASSUM MP_TAC \\ SRW_TAC [] [] 357 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC); 358 359val str2sym_LENGTH = prove( 360 ``!s t x. ~(s = []) /\ (str2sym s = (x,t)) ==> LENGTH t < LENGTH s``, 361 SIMP_TAC std_ss [str2sym_def,LET_DEF] \\ NTAC 3 STRIP_TAC \\ Cases_on `s` 362 \\ SIMP_TAC std_ss [str2sym_def,LET_DEF] 363 \\ `?a1 a2. str2sym_aux t' F = (a1,a2)` by METIS_TAC [PAIR] 364 \\ `?y1 y2. read_while identifier_char t' "" = (y1,y2)` by METIS_TAC [PAIR] 365 \\ IMP_RES_TAC read_while_thm 366 \\ ASM_SIMP_TAC std_ss [] \\ IMP_RES_TAC str2sym_aux_LENGTH 367 \\ FULL_SIMP_TAC std_ss [LENGTH,HD,LENGTH_NIL,NOT_CONS_NIL,TL] 368 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss [TL] \\ DECIDE_TAC); 369 370val next_token_LENGTH = prove( 371 ``!s x t. (next_token s = (x,t)) ==> LENGTH t < LENGTH s \/ (s = "")``, 372 HO_MATCH_MP_TAC (fetch "-" "next_token_ind") \\ REPEAT STRIP_TAC 373 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM MP_TAC 374 \\ ONCE_REWRITE_TAC [next_token_def] 375 \\ ASM_SIMP_TAC std_ss [] 376 \\ Cases_on `space_char c` \\ ASM_SIMP_TAC std_ss [] THEN1 377 (REPEAT STRIP_TAC \\ RES_TAC \\ ASM_SIMP_TAC std_ss [LENGTH] 378 THEN1 (DISJ1_TAC \\ DECIDE_TAC) 379 \\ FULL_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [next_token_def] 380 \\ Q.PAT_X_ASSUM `"" = t` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 381 \\ EVAL_TAC) 382 \\ `?x1 x2. read_while number_char s "" = (x1,x2)` by METIS_TAC [PAIR] 383 \\ `?y1 y2. read_while (\x. x <> #"\n") s "" = (y1,y2)` by METIS_TAC [PAIR] 384 \\ `?z1 z2. str2sym (c::s) = (z1,z2)` by METIS_TAC [PAIR] 385 \\ IMP_RES_TAC str2sym_LENGTH 386 \\ FULL_SIMP_TAC std_ss [LET_DEF] \\ IMP_RES_TAC read_while_thm 387 \\ SRW_TAC [] [LENGTH] \\ ASM_SIMP_TAC std_ss [LENGTH] 388 \\ REPEAT (Cases_on `x2`) 389 \\ FULL_SIMP_TAC std_ss [LENGTH,TL,NOT_CONS_NIL,HD,ADD1] 390 \\ REPEAT DECIDE_TAC 391 \\ RES_TAC \\ REPEAT DECIDE_TAC 392 \\ FULL_SIMP_TAC std_ss [EVAL ``next_token ""``] 393 \\ REPEAT (Q.PAT_X_ASSUM `"" = t` (fn th => FULL_SIMP_TAC std_ss [GSYM th])) 394 \\ FULL_SIMP_TAC std_ss [LENGTH] \\ REPEAT DECIDE_TAC); 395 396val sexp_lex_def = tDefine "sexp_lex" ` 397 sexp_lex s = 398 if SND (FST (next_token s)) = Sym "NIL" then ([],"") else 399 let (ts,s2) = sexp_lex (SND (next_token s)) in 400 (FST (next_token s)::ts,s2)` 401 (WF_REL_TAC `measure (LENGTH)` \\ REPEAT STRIP_TAC 402 \\ Cases_on `next_token s` \\ FULL_SIMP_TAC std_ss [] 403 \\ Cases_on `q` \\ FULL_SIMP_TAC std_ss [] 404 \\ IMP_RES_TAC next_token_LENGTH \\ FULL_SIMP_TAC std_ss [] 405 \\ FULL_SIMP_TAC std_ss [next_token_def] \\ METIS_TAC []); 406 407val sexp_lex_thm = prove( 408 ``sexp_lex s = 409 let (t,s) = next_token s in 410 if SND t = Sym "NIL" then ([],[]) else 411 let (ts,s) = sexp_lex s in 412 (t::ts,s)``, 413 SIMP_TAC std_ss [Once sexp_lex_def] 414 \\ SIMP_TAC std_ss [LET_DEF] 415 \\ Cases_on `next_token s` \\ ASM_SIMP_TAC std_ss []); 416 417val sexp2abbrev_aux_SND = prove( 418 ``!exp b abbrevs ps xs1 xs2 ps1 ps2. 419 ((xs1,ps1) = sexp2abbrev_aux exp b abbrevs ps) ==> 420 ((xs2,ps2) = sexp2abbrevt_aux exp b abbrevs ps) ==> 421 (ps1 = ps2)``, 422 HO_MATCH_MP_TAC SExp_print_induct \\ NTAC 9 STRIP_TAC 423 \\ ONCE_REWRITE_TAC [sexp2abbrevt_aux_def,sexp2abbrev_aux_def] 424 \\ Q.ABBREV_TAC `index = abbrevs ' exp` 425 \\ SIMP_TAC std_ss [LET_DEF] 426 \\ Q.ABBREV_TAC `t_prefix = if exp IN FDOM abbrevs then [(Val index,Val 2)] else []` 427 \\ Q.ABBREV_TAC `s_prefix = if exp IN FDOM abbrevs then STRCAT (STRCAT "#" (num2str index)) "=" else ""` 428 \\ `?t_str1 t_ps1. sexp2abbrevt_aux (CAR exp) T abbrevs ps = (t_str1,t_ps1)` by METIS_TAC [PAIR] 429 \\ `?t_str2 t_ps2. sexp2abbrevt_aux (CDR exp) F abbrevs t_ps1 = (t_str2,t_ps2)` by METIS_TAC [PAIR] 430 \\ `?t_str3 t_ps3. sexp2abbrevt_aux (CAR (CDR exp)) T abbrevs ps = (t_str3,t_ps3)` by METIS_TAC [PAIR] 431 \\ `?s_str1 s_ps1. sexp2abbrev_aux (CAR exp) T abbrevs ps = (s_str1,s_ps1)` by METIS_TAC [PAIR] 432 \\ `?s_str2 s_ps2. sexp2abbrev_aux (CDR exp) F abbrevs s_ps1 = (s_str2,s_ps2)` by METIS_TAC [PAIR] 433 \\ `?s_str3 s_ps3. sexp2abbrev_aux (CAR (CDR exp)) T abbrevs ps = (s_str3,s_ps3)` by METIS_TAC [PAIR] 434 \\ ASM_SIMP_TAC std_ss [] 435 \\ Cases_on `Abbrev (exp IN FDOM abbrevs /\ exp IN ps)` 436 THEN1 (POP_ASSUM MP_TAC \\ SIMP_TAC std_ss [markerTheory.Abbrev_def]) 437 \\ IMP_RES_TAC (METIS_PROVE [] ``~Abbrev b ==> ~b``) 438 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 439 \\ Cases_on `isVal exp` 440 THEN1 (FULL_SIMP_TAC std_ss [isVal_thm,isDot_def,isVal_def,SExp_11]) 441 \\ Cases_on `isSym exp` 442 THEN1 (FULL_SIMP_TAC std_ss [isSym_thm,isDot_def,isSym_def,SExp_11]) 443 \\ `isDot exp` by (Cases_on `exp` \\ FULL_SIMP_TAC std_ss [isVal_def,isSym_def,isDot_def]) 444 \\ ASM_SIMP_TAC std_ss [] 445 \\ Cases_on `isQuote exp` THEN1 (FULL_SIMP_TAC std_ss [] \\ METIS_TAC []) 446 \\ ASM_SIMP_TAC std_ss [] 447 \\ `(t_prefix = []) = (s_prefix = [])` by 448 (FULL_SIMP_TAC std_ss [APPEND] \\ METIS_TAC [NOT_CONS_NIL]) 449 \\ ASM_SIMP_TAC std_ss [] 450 \\ Cases_on `b \/ s_prefix <> ""` \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC []); 451 452val read_while_eval = (GEN_ALL o RW [APPEND_NIL,APPEND] o Q.SPECL [`xs`,`[]`] o prove)( 453 ``!xs zs. EVERY P xs /\ ~P y ==> (read_while P (xs ++ y::ys) zs = (zs ++ xs,y::ys))``, 454 Induct \\ ASM_SIMP_TAC std_ss [EVERY_DEF,APPEND,read_while_def,APPEND_NIL] 455 \\ SIMP_TAC std_ss [APPEND_NIL,GSYM APPEND_ASSOC,APPEND]); 456 457val read_while_entire = (GEN_ALL o RW [APPEND_NIL,APPEND] o Q.SPECL [`xs`,`[]`] o prove)( 458 ``!xs zs. EVERY P xs ==> (read_while P xs zs = (zs ++ xs,""))``, 459 Induct \\ ASM_SIMP_TAC std_ss [EVERY_DEF,APPEND,read_while_def,APPEND_NIL] 460 \\ SIMP_TAC std_ss [APPEND_NIL,GSYM APPEND_ASSOC,APPEND]); 461 462val read_while_lemma = prove( 463 ``(read_while number_char (num2str index ++ #"#"::xs) "" = (num2str index,#"#"::xs)) /\ 464 (read_while number_char (num2str index ++ #"="::xs) "" = (num2str index,#"="::xs))``, 465 REPEAT STRIP_TAC \\ MATCH_MP_TAC read_while_eval 466 \\ ASM_SIMP_TAC std_ss [str2num_num2str] \\ EVAL_TAC); 467 468val next_token_lemma = prove( 469 ``(s <> "" ==> MEM (HD s) " )") ==> 470 (next_token (STRCAT (num2str a) s) = ((Val a,Val 0), s)) /\ 471 (next_token (STRCAT (sym2str t) s) = ((Sym t,Val 0), s))``, 472 REPEAT STRIP_TAC THEN1 473 (Cases_on `num2str a` THEN1 METIS_TAC [str2num_num2str] 474 \\ ASM_SIMP_TAC std_ss [APPEND,next_token_def] 475 \\ `EVERY number_char (STRING h t)` by METIS_TAC [str2num_num2str] 476 \\ FULL_SIMP_TAC std_ss [EVERY_DEF] 477 \\ `~space_char h` by 478 (FULL_SIMP_TAC std_ss [number_char_def,space_char_def] \\ DECIDE_TAC) 479 \\ `~MEM h "(.)'#"` by 480 (FULL_SIMP_TAC std_ss [MEM] \\ REPEAT STRIP_TAC 481 \\ FULL_SIMP_TAC (srw_ss()) [number_char_def]) 482 \\ FULL_SIMP_TAC std_ss [MEM] 483 \\ `read_while number_char (STRCAT t s) "" = (t,s)` by 484 (Cases_on `s` \\ FULL_SIMP_TAC std_ss [APPEND_NIL,read_while_entire] 485 \\ MATCH_MP_TAC read_while_eval \\ FULL_SIMP_TAC std_ss [HD,NOT_CONS_NIL] 486 \\ EVAL_TAC) 487 \\ ASM_SIMP_TAC std_ss [LET_DEF] 488 \\ METIS_TAC [str2num_num2str]) 489 \\ SIMP_TAC std_ss [sym2str_def] 490 \\ Cases_on `identifier_string t /\ EVERY (\c. ~is_lower_case c) t` 491 \\ ASM_SIMP_TAC std_ss [] THEN1 492 (FULL_SIMP_TAC std_ss [identifier_string_def] 493 \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [APPEND,EVERY_DEF] 494 \\ FULL_SIMP_TAC std_ss [next_token_def,HD] 495 \\ FULL_SIMP_TAC std_ss [identifier_char_def,MEM,str2sym_def,HD,NOT_CONS_NIL,TL] 496 \\ `read_while identifier_char (STRCAT t' s) "" = (t',s)` by 497 (Cases_on `s` \\ FULL_SIMP_TAC std_ss [APPEND_NIL,read_while_entire] 498 \\ MATCH_MP_TAC read_while_eval \\ FULL_SIMP_TAC std_ss [HD,NOT_CONS_NIL] 499 \\ EVAL_TAC) 500 \\ ASM_SIMP_TAC std_ss [LET_DEF] 501 \\ `~(space_char h)` by (FULL_SIMP_TAC std_ss [space_char_def] \\ DECIDE_TAC) 502 \\ Cases_on `h = #"("` THEN1 (CCONTR_TAC \\ Q.PAT_X_ASSUM `42 <= bbb` MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 503 \\ Cases_on `h = #")"` THEN1 (CCONTR_TAC \\ Q.PAT_X_ASSUM `42 <= bbb` MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 504 \\ Cases_on `h = #"'"` THEN1 (CCONTR_TAC \\ Q.PAT_X_ASSUM `42 <= bbb` MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 505 \\ Cases_on `h = #"#"` THEN1 (CCONTR_TAC \\ Q.PAT_X_ASSUM `42 <= bbb` MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 506 \\ Cases_on `h = #"."` THEN1 (FULL_SIMP_TAC std_ss [EVAL ``ORD #"."``]) 507 \\ Cases_on `h = #"|"` THEN1 (FULL_SIMP_TAC std_ss [EVAL ``ORD #"|"``]) 508 \\ Cases_on `h = #";"` THEN1 (FULL_SIMP_TAC std_ss [EVAL ``ORD #";"``]) 509 \\ ASM_SIMP_TAC std_ss [] 510 \\ AP_TERM_TAC 511 \\ `EVERY (\c. ~is_lower_case c) (h::t')` by ASM_SIMP_TAC std_ss [EVERY_DEF] 512 \\ POP_ASSUM MP_TAC \\ Q.SPEC_TAC (`h::t'`,`xs`) 513 \\ Induct \\ ASM_SIMP_TAC std_ss [MAP,EVERY_DEF,upper_case_def]) 514 \\ SIMP_TAC (srw_ss()) [APPEND,next_token_def,EVAL ``space_char #"|"``, 515 EVAL ``number_char #"|"``,str2sym_def,LET_DEF] 516 \\ SIMP_TAC std_ss [str2sym_aux_sym2str_aux,LET_DEF]); 517 518val sexp_lex_SPACE = prove( 519 ``!xs. sexp_lex (#" "::xs) = sexp_lex xs``, 520 ONCE_REWRITE_TAC [sexp_lex_thm] 521 \\ SIMP_TAC std_ss [next_token_def,EVAL ``space_char #" "``]); 522 523fun FORCE_PBETA_CONV tm = let 524 val (tm1,tm2) = dest_comb tm 525 val vs = fst (pairSyntax.dest_pabs tm1) 526 fun expand_pair_conv tm = ISPEC tm (GSYM pairTheory.PAIR) 527 fun get_conv vs = let 528 val (x,y) = dest_pair vs 529 in expand_pair_conv THENC (RAND_CONV (get_conv y)) end 530 handle e => ALL_CONV 531 in (RAND_CONV (get_conv vs) THENC PairRules.PBETA_CONV) tm end; 532 533val sexp2abbrev_aux_FST = prove( 534 ``!exp s b abbrevs ps xs1 xs2 ps1 ps2. 535 (~(s = []) ==> MEM (HD s) " )") ==> 536 ((xs1,ps1) = sexp2abbrev_aux exp b abbrevs ps) ==> 537 ((xs2,ps2) = sexp2abbrevt_aux exp b abbrevs ps) ==> 538 (FST (sexp_lex (xs1 ++ s)) = xs2 ++ FST (sexp_lex s))``, 539 HO_MATCH_MP_TAC SExp_print_induct \\ NTAC 10 STRIP_TAC 540 \\ ONCE_REWRITE_TAC [sexp2abbrevt_aux_def,sexp2abbrev_aux_def] 541 \\ Q.ABBREV_TAC `index = abbrevs ' exp` 542 \\ SIMP_TAC std_ss [LET_DEF] 543 \\ Q.ABBREV_TAC `t_prefix = if exp IN FDOM abbrevs then [(Val index,Val 2)] else []` 544 \\ Q.ABBREV_TAC `s_prefix = if exp IN FDOM abbrevs then STRCAT (STRCAT "#" (num2str index)) "=" else ""` 545 \\ `?t_str1 t_ps1. sexp2abbrevt_aux (CAR exp) T abbrevs ps = (t_str1,t_ps1)` by METIS_TAC [PAIR] 546 \\ `?t_str2 t_ps2. sexp2abbrevt_aux (CDR exp) F abbrevs t_ps1 = (t_str2,t_ps2)` by METIS_TAC [PAIR] 547 \\ `?t_str3 t_ps3. sexp2abbrevt_aux (CAR (CDR exp)) T abbrevs ps = (t_str3,t_ps3)` by METIS_TAC [PAIR] 548 \\ `?s_str1 s_ps1. sexp2abbrev_aux (CAR exp) T abbrevs ps = (s_str1,s_ps1)` by METIS_TAC [PAIR] 549 \\ `?s_str2 s_ps2. sexp2abbrev_aux (CDR exp) F abbrevs s_ps1 = (s_str2,s_ps2)` by METIS_TAC [PAIR] 550 \\ `?s_str3 s_ps3. sexp2abbrev_aux (CAR (CDR exp)) T abbrevs ps = (s_str3,s_ps3)` by METIS_TAC [PAIR] 551 \\ ASM_SIMP_TAC std_ss [] 552 \\ Cases_on `Abbrev (exp IN FDOM abbrevs /\ exp IN ps)` 553 THEN1 (POP_ASSUM MP_TAC \\ SIMP_TAC std_ss [markerTheory.Abbrev_def] 554 \\ REPEAT STRIP_TAC 555 \\ SIMP_TAC std_ss [Once sexp_lex_thm] 556 \\ SIMP_TAC (srw_ss()) [APPEND,next_token_def,EVAL ``space_char #"#"``] 557 \\ SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND,read_while_lemma] 558 \\ SIMP_TAC std_ss [LET_DEF,NOT_CONS_NIL,TL,HD,SExp_distinct] 559 \\ Cases_on `sexp_lex s` \\ ASM_SIMP_TAC std_ss [str2num_num2str]) 560 \\ IMP_RES_TAC (METIS_PROVE [] ``~Abbrev b ==> ~b``) 561 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 562 \\ `(t_prefix = []) = (s_prefix = [])` by 563 (FULL_SIMP_TAC std_ss [APPEND] \\ METIS_TAC [NOT_CONS_NIL]) 564 \\ ASM_SIMP_TAC std_ss [] 565 \\ `!ss ts. 566 (FST (sexp_lex (STRCAT s_prefix (STRCAT ss s))) = 567 t_prefix ++ (ts ++ FST (sexp_lex s))) = 568 (FST (sexp_lex (STRCAT ss s)) = ts ++ FST (sexp_lex s))` by 569 (Q.UNABBREV_TAC `t_prefix` \\ Q.UNABBREV_TAC `s_prefix` 570 \\ REVERSE (Cases_on `exp IN FDOM abbrevs`) \\ ASM_SIMP_TAC std_ss [] 571 THEN1 (ASM_SIMP_TAC std_ss [APPEND]) 572 \\ SIMP_TAC std_ss [Once sexp_lex_thm] \\ SIMP_TAC std_ss [GSYM APPEND_ASSOC] 573 \\ SIMP_TAC (srw_ss()) [APPEND,next_token_def,EVAL ``space_char #"#"``] 574 \\ SIMP_TAC std_ss [GSYM APPEND_ASSOC] 575 \\ SIMP_TAC std_ss [APPEND,read_while_lemma,LET_DEF,NOT_CONS_NIL,TL,HD] 576 \\ SIMP_TAC std_ss [str2num_num2str,EVAL ``#"=" = #"#"``,SExp_distinct] 577 \\ REPEAT STRIP_TAC 578 \\ Cases_on `sexp_lex (STRCAT ss s)` \\ ASM_SIMP_TAC std_ss [CONS_11]) 579 \\ Cases_on `isVal exp` 580 THEN1 (FULL_SIMP_TAC std_ss [isVal_thm,isDot_def,isVal_def,SExp_11] 581 \\ ASM_SIMP_TAC std_ss [getVal_def,GSYM APPEND_ASSOC] 582 \\ REPEAT STRIP_TAC 583 \\ SIMP_TAC std_ss [Once sexp_lex_thm] \\ SIMP_TAC std_ss [GSYM APPEND_ASSOC] 584 \\ ASM_SIMP_TAC (srw_ss()) [APPEND,next_token_lemma] 585 \\ ASM_SIMP_TAC std_ss [LET_DEF,SExp_distinct] 586 \\ Cases_on `sexp_lex s` \\ ASM_SIMP_TAC std_ss []) 587 \\ Cases_on `isSym exp` 588 THEN1 (FULL_SIMP_TAC std_ss [isSym_thm,isDot_def,isSym_def,SExp_11] 589 \\ ASM_SIMP_TAC std_ss [getSym_def,GSYM APPEND_ASSOC] 590 \\ REPEAT STRIP_TAC 591 \\ SIMP_TAC std_ss [Once sexp_lex_thm] \\ SIMP_TAC std_ss [GSYM APPEND_ASSOC] 592 \\ ASM_SIMP_TAC (srw_ss()) [APPEND,next_token_lemma] 593 \\ ASM_SIMP_TAC std_ss [LET_DEF,SExp_distinct] 594 \\ Cases_on `sexp_lex s` \\ ASM_SIMP_TAC std_ss []) 595 \\ `isDot exp` by (Cases_on `exp` \\ FULL_SIMP_TAC std_ss [isVal_def,isSym_def,isDot_def]) 596 \\ ASM_SIMP_TAC std_ss [] 597 \\ `s_ps1 = t_ps1` by METIS_TAC [sexp2abbrev_aux_SND] 598 \\ Cases_on `isQuote exp` 599 THEN1 (FULL_SIMP_TAC std_ss [] 600 \\ Q.PAT_X_ASSUM `!ss ts. bbb` (ASSUME_TAC o Q.SPECL [`"'" ++ s_str3`,`[(Val 3,Val 1)] ++ t_str3`]) 601 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC] \\ REPEAT STRIP_TAC 602 \\ SIMP_TAC std_ss [Once sexp_lex_thm] 603 \\ SIMP_TAC (srw_ss()) [APPEND,next_token_def,EVAL ``space_char #"'"``,LET_DEF,SExp_distinct] 604 \\ CONV_TAC (DEPTH_CONV FORCE_PBETA_CONV) 605 \\ SIMP_TAC std_ss [FST,CONS_11] \\ METIS_TAC []) 606 \\ ASM_SIMP_TAC std_ss [] 607 \\ Q.ABBREV_TAC `s1 = if b \/ s_prefix <> "" then ("(") else ("")` 608 \\ Q.ABBREV_TAC `s2 = if b \/ s_prefix <> "" then (")") else ("")` 609 \\ Q.ABBREV_TAC `t1 = if b \/ s_prefix <> "" then ([(Val 0,Val 1)]) else ([])` 610 \\ Q.ABBREV_TAC `t2 = if b \/ s_prefix <> "" then ([(Val 2,Val 1)]) else ([])` 611 \\ `(if b \/ s_prefix <> "" then 612 ([(Val 0,Val 1)],[(Val 2,Val 1)]) 613 else 614 ([],[])) = (t1,t2)` by METIS_TAC [] 615 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 616 \\ `(if b \/ s_prefix <> "" then 617 ("(",")") 618 else 619 ([],[])) = (s1,s2)` by METIS_TAC [] 620 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 621 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 622 \\ Q.ABBREV_TAC `t3 = if CDR exp = Sym "NIL" then [] 623 else (if isAtom abbrevs (CDR exp) then [(Val 1,Val 1)] else []) ++ t_str2` 624 \\ Q.ABBREV_TAC `s3 = if CDR exp = Sym "NIL" then "" 625 else STRCAT (if isAtom abbrevs (CDR exp) then " . " else " ") s_str2` 626 \\ Q.PAT_X_ASSUM `!ss ts. bbb` (ASSUME_TAC o Q.SPECL [`s1 ++ s_str1 ++ s3 ++ s2`,`t1 ++ t_str1 ++ t3 ++ t2`]) 627 \\ FULL_SIMP_TAC std_ss [APPEND_ASSOC] \\ POP_ASSUM (K ALL_TAC) 628 \\ `FST (sexp_lex (STRCAT (STRCAT (STRCAT (s_str1) s3) s2) s)) = 629 t_str1 ++ t3 ++ t2 ++ FST (sexp_lex s)` suffices_by (STRIP_TAC THEN Cases_on `s1 = []` 630 THEN1 (`t1 = []` by METIS_TAC [NOT_CONS_NIL] \\ ASM_SIMP_TAC std_ss [APPEND]) 631 \\ `s1 = "("` by METIS_TAC [NOT_CONS_NIL] 632 \\ `t1 = [^TOKEN_OPEN]` by METIS_TAC [NOT_CONS_NIL] 633 \\ ASM_SIMP_TAC std_ss [APPEND] 634 \\ SIMP_TAC std_ss [Once sexp_lex_thm] 635 \\ SIMP_TAC std_ss [next_token_def,EVAL ``space_char #"("``,LET_DEF,SExp_distinct] 636 \\ CONV_TAC (DEPTH_CONV FORCE_PBETA_CONV) 637 \\ ASM_SIMP_TAC std_ss [FST,CONS_11]) 638 \\ `~(s3++s2++s = []) ==> MEM (HD (s3++s2++s)) " )"` by 639 (Q.UNABBREV_TAC `s3` \\ Q.UNABBREV_TAC `s2` 640 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss [MEM]) 641 \\ `FST (sexp_lex (STRCAT s_str1 (s3++s2++s))) = 642 t_str1 ++ FST (sexp_lex (s3++s2++s))` by 643 (Q.PAT_X_ASSUM `!s b abbrevs ps xs1 xs2 ps1 ps2. bbb` (K ALL_TAC) 644 \\ Q.PAT_X_ASSUM `!s b abbrevs ps xs1 xs2 ps1 ps2. bbb` (MATCH_MP_TAC o RW [AND_IMP_INTRO]) 645 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC []) 646 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND_11] 647 \\ (sg `FST (sexp_lex (STRCAT (s2) s)) = 648 t2 ++ FST (sexp_lex s)`) THEN1 649 (Cases_on `s2 = []` 650 THEN1 (`t2 = []` by METIS_TAC [NOT_CONS_NIL] \\ ASM_SIMP_TAC std_ss [APPEND]) 651 \\ `s2 = ")"` by METIS_TAC [NOT_CONS_NIL] 652 \\ `t2 = [^TOKEN_CLOSE]` by METIS_TAC [NOT_CONS_NIL] 653 \\ ASM_SIMP_TAC std_ss [APPEND] 654 \\ SIMP_TAC std_ss [Once sexp_lex_thm] 655 \\ SIMP_TAC (srw_ss()) [next_token_def,EVAL ``space_char #")"``,LET_DEF,SExp_distinct] 656 \\ CONV_TAC (DEPTH_CONV FORCE_PBETA_CONV) 657 \\ SIMP_TAC std_ss [FST]) 658 \\ Q.UNABBREV_TAC `s3` \\ Q.UNABBREV_TAC `t3` 659 \\ Cases_on `CDR exp = Sym "NIL"` \\ ASM_SIMP_TAC std_ss [APPEND] 660 \\ `FST (sexp_lex (STRCAT (STRCAT s_str2 s2) s)) = 661 t_str2 ++ t2 ++ FST (sexp_lex s)` suffices_by (STRIP_TAC THEN REVERSE (Cases_on `isAtom abbrevs (CDR exp)`) 662 \\ ASM_SIMP_TAC std_ss [APPEND,sexp_lex_SPACE] 663 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 664 \\ SIMP_TAC std_ss [Once sexp_lex_thm] 665 \\ SIMP_TAC (srw_ss()) [next_token_def,EVAL ``space_char #"."``,LET_DEF,sexp_lex_SPACE] 666 \\ CONV_TAC (DEPTH_CONV FORCE_PBETA_CONV) 667 \\ FULL_SIMP_TAC std_ss [FST,APPEND_ASSOC]) 668 \\ `~(s2++s = []) ==> MEM (HD (s2++s)) " )"` by 669 (Q.UNABBREV_TAC `s2` \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss [MEM]) 670 \\ `FST (sexp_lex (STRCAT s_str2 (s2++s))) = 671 t_str2 ++ FST (sexp_lex (s2++s))` by 672 (Q.PAT_X_ASSUM `!s b abbrevs ps xs1 xs2 ps1 ps2. bbb` (MATCH_MP_TAC o RW [AND_IMP_INTRO]) 673 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC []) 674 \\ FULL_SIMP_TAC std_ss [APPEND_ASSOC]); 675 676val sexp_lex_sexp2abbrev_aux = prove( 677 ``!exp b abbrevs ps. 678 FST (sexp_lex (FST (sexp2abbrev_aux exp b abbrevs ps))) = 679 FST (sexp2abbrevt_aux exp b abbrevs ps)``, 680 REPEAT STRIP_TAC 681 \\ MP_TAC (Q.SPECL [`exp`,`[]`] sexp2abbrev_aux_FST) 682 \\ ASM_SIMP_TAC std_ss [APPEND_NIL,EVAL ``sexp_lex ""``] 683 \\ METIS_TAC [PAIR]); 684 685 686(* Part 2 - section 2: algorithm for parsing a list of tokens *) 687 688val _ = Hol_datatype ` 689 lisp_parse_mode = 690 L_READ 691 | L_RETURN of SExp 692 | L_COLLECT of SExp`; 693 694val _ = Hol_datatype ` 695 lisp_parse_action = 696 L_CONS of SExp 697 | L_STOP 698 | L_DOT 699 | L_QUOTE 700 | L_STORE of num`; 701 702val (R_parse_rules,R_parse_ind,R_parse_cases) = Hol_reln ` 703 (* from mode: L_READ *) 704 (!ts s mem x. 705 R_parse ((x, Val 0)::ts,s,L_READ,mem) 706 (ts,s,L_RETURN x,mem)) 707 /\ 708 (!ts s mem. 709 R_parse ((^TOKEN_OPEN)::ts,s,L_READ,mem) 710 (ts,L_STOP::s,L_READ,mem)) 711 /\ 712 (!ts s mem. 713 R_parse ((^TOKEN_DOT)::ts,s,L_READ,mem) 714 (ts,L_DOT::s,L_READ,mem)) 715 /\ 716 (!ts s mem. 717 R_parse ((^TOKEN_QUOTE)::ts,s,L_READ,mem) 718 (ts,L_QUOTE::s,L_READ,mem)) 719 /\ 720 (!ts s mem. 721 R_parse ((^TOKEN_CLOSE)::ts,s,L_READ,mem) 722 (ts,s,L_COLLECT (Sym "NIL"),mem)) 723 /\ 724 (!ts s mem index. 725 R_parse ((^TOKEN_LOAD)::ts,s,L_READ,mem) 726 (ts,s,L_RETURN (mem index),mem)) 727 /\ 728 (!ts s mem index. 729 R_parse ((^TOKEN_SAVE)::ts,s,L_READ,mem) 730 (ts,L_STORE index::s,L_READ,mem)) 731 /\ 732 (* from mode: L_COLLECT *) 733 (!ts s mem exp. 734 R_parse (ts,L_STOP::s,L_COLLECT exp,mem) 735 (ts,s,L_RETURN exp,mem)) 736 /\ 737 (!ts s mem x exp. 738 R_parse (ts,L_CONS x::s,L_COLLECT exp,mem) 739 (ts,s,L_COLLECT (Dot x exp),mem)) 740 /\ 741 (!ts s mem exp. 742 R_parse (ts,L_DOT::s,L_COLLECT exp,mem) 743 (ts,s,L_COLLECT (CAR exp),mem)) 744 /\ 745 (* from mode: L_RETURN *) 746 (!ts s mem exp. 747 R_parse (ts,L_QUOTE::s,L_RETURN exp,mem) 748 (ts,s,L_RETURN (Dot (Sym "QUOTE") (Dot exp (Sym "NIL"))),mem)) 749 /\ 750 (!ts s mem n exp. 751 R_parse (ts,L_STORE n::s,L_RETURN exp,mem) 752 (ts,s,L_RETURN exp,(n =+ exp) mem)) 753 /\ 754 (!ts s mem exp. 755 ~(s = []) /\ ~(HD s = L_QUOTE) /\ ~(?k. HD s = L_STORE k) ==> 756 R_parse (ts,s,L_RETURN exp,mem) 757 (ts,L_CONS exp::s,L_READ,mem))` 758 759val READ_L_STORE_def = Define ` 760 (READ_L_STORE (L_STORE n) = SOME n) /\ 761 (READ_L_STORE _ = NONE)`; 762 763val READ_L_CONS_def = Define ` 764 (READ_L_CONS (L_CONS exp) = SOME exp) /\ 765 (READ_L_CONS _ = NONE)`; 766 767val NOT_NIL_IMP = prove( 768 ``!x. ~(x = []) ==> ?x1 x2. x = x1::x2``, 769 Cases \\ SRW_TAC [] []) 770 771val sexp_parse_aux_def = tDefine "sexp_parse_aux" ` 772 (sexp_parse_aux (ts,s,L_READ,mem) = 773 if ts = [] then Sym "NIL" else 774 let (t,ts) = (HD ts, TL ts) in 775 if SND t = Val 0 then sexp_parse_aux (ts,s,L_RETURN (FST t),mem) else 776 if (t = ^TOKEN_OPEN) then sexp_parse_aux (ts,L_STOP::s,L_READ,mem) else 777 if (t = ^TOKEN_DOT) then sexp_parse_aux (ts,L_DOT::s,L_READ,mem) else 778 if (t = ^TOKEN_QUOTE) then sexp_parse_aux (ts,L_QUOTE::s,L_READ,mem) else 779 if (t = ^TOKEN_CLOSE) then sexp_parse_aux (ts,s,L_COLLECT (Sym "NIL"),mem) else 780 if ~isVal (FST t) then Sym "NIL" else 781 if SND t = Val 3 then sexp_parse_aux (ts,s,L_RETURN (mem (getVal (FST t))),mem) else 782 if SND t = Val 2 then sexp_parse_aux (ts,L_STORE (getVal (FST t))::s,L_READ,mem) else 783 Sym "NIL") /\ 784 (sexp_parse_aux (ts,s,L_COLLECT exp,mem) = 785 if s = [] then Sym "NIL" else 786 let (x,s) = (HD s, TL s) in 787 if x = L_STOP then sexp_parse_aux (ts,s,L_RETURN exp,mem) else 788 if ~(READ_L_CONS x = NONE) then sexp_parse_aux (ts,s,L_COLLECT (Dot (THE (READ_L_CONS x)) exp),mem) else 789 if x = L_DOT then sexp_parse_aux (ts,s,L_COLLECT (CAR exp),mem) else 790 Sym "NIL") /\ 791 (sexp_parse_aux (ts,s,L_RETURN exp,mem) = 792 if s = [] then exp else 793 let (x,s) = (HD s, TL s) in 794 if x = L_QUOTE then sexp_parse_aux (ts,s,L_RETURN (Dot (Sym "QUOTE") (Dot exp (Sym "NIL"))),mem) else 795 if ~(READ_L_STORE x = NONE) then sexp_parse_aux (ts,s,L_RETURN exp,(THE (READ_L_STORE x) =+ exp) mem) else 796 sexp_parse_aux (ts,L_CONS exp::x::s,L_READ,mem))` 797 (WF_REL_TAC `measure (\(ts,s,mode,mem). 798 3 * LENGTH ts + LENGTH s + if mode = L_READ then 0 else 2)` 799 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC NOT_NIL_IMP 800 \\ FULL_SIMP_TAC (srw_ss()) [] \\ DECIDE_TAC) 801 802val RTC_parse_IMP_sexp_parse_aux = prove( 803 ``!x y. RTC R_parse x y ==> 804 !exp. (FST (SND (SND y)) = L_RETURN exp) /\ (FST (SND y) = []) ==> 805 (sexp_parse_aux x = exp)``, 806 HO_MATCH_MP_TAC RTC_INDUCT \\ REPEAT STRIP_TAC THEN1 807 (`?ts s mode mem. x = (ts,s,mode,mem)` by METIS_TAC [PAIR] 808 \\ FULL_SIMP_TAC std_ss [] \\ ONCE_REWRITE_TAC [sexp_parse_aux_def] 809 \\ ASM_SIMP_TAC std_ss []) 810 \\ `sexp_parse_aux x = sexp_parse_aux x'` suffices_by (STRIP_TAC THEN METIS_TAC []) 811 \\ Q.PAT_X_ASSUM `R_parse x x'` MP_TAC 812 \\ ONCE_REWRITE_TAC [R_parse_cases] 813 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 814 \\ SIMP_TAC std_ss [Once sexp_parse_aux_def] 815 \\ FULL_SIMP_TAC (srw_ss()) [isVal_def,isSym_def,LET_DEF,getVal_def, 816 DECIDE ``~(SUC (SUC n) < 2)``,READ_L_CONS_def,READ_L_STORE_def] 817 \\ IMP_RES_TAC NOT_NIL_IMP 818 \\ Cases_on `x1` 819 \\ FULL_SIMP_TAC (srw_ss()) [isVal_def,isSym_def,LET_DEF,getVal_def, 820 DECIDE ``~(SUC (SUC n) < 2)``,READ_L_CONS_def,READ_L_STORE_def]); 821 822val RTC_UNROLL = prove( 823 ``!x y z. R x y /\ RTC R y z ==> RTC R x z``, 824 METIS_TAC [RTC_RULES]); 825 826val RTC_UNROLL2 = prove( 827 ``!x y z. RTC R x y /\ R y z ==> RTC R x z``, 828 METIS_TAC [RTC_RULES_RIGHT1]); 829 830val R_parse_abbrev_def = Define ` 831 R_parse_abbrev abbrevs ps (mem:num->SExp) = 832 !s. s IN ps ==> s IN FDOM abbrevs /\ (mem (abbrevs ' s) = s)`; 833 834val FMAP_11_def = Define ` 835 FMAP_11 f = !x y. x IN FDOM f /\ y IN FDOM f ==> ((f ' x = f ' y) = (x = y))`; 836 837val cons_atoms_def = tDefine "cons_atoms" ` 838 cons_atoms abbrevs exp s = 839 if isAtom abbrevs exp then L_CONS exp :: s else 840 if CDR exp = Sym "NIL" then L_CONS (CAR exp) :: s else 841 if isAtom abbrevs (CDR exp) then L_CONS (CDR exp)::L_DOT::L_CONS (CAR exp)::s else 842 cons_atoms abbrevs (CDR exp) (L_CONS (CAR exp) :: s)` 843 (WF_REL_TAC `measure (LSIZE o FST o SND)` 844 \\ REPEAT STRIP_TAC \\ POP_ASSUM (K ALL_TAC) 845 \\ FULL_SIMP_TAC std_ss [isAtom_def,isDot_thm] \\ REPEAT STRIP_TAC 846 \\ FULL_SIMP_TAC std_ss [LSIZE_def,CDR_def] \\ DECIDE_TAC) 847 848val cons_atoms_lemma = prove( 849 ``~isAtom abbrevs (Dot a1 a2) /\ ~(a2 = Sym "NIL") ==> 850 (cons_atoms abbrevs (Dot a1 a2) s = 851 if isAtom abbrevs a2 then 852 L_CONS a2::L_DOT::L_CONS a1::s 853 else 854 cons_atoms abbrevs a2 (L_CONS a1::s))``, 855 REPEAT STRIP_TAC 856 \\ SIMP_TAC std_ss [Once cons_atoms_def] 857 \\ ASM_SIMP_TAC std_ss [CDR_def,CAR_def]); 858 859val MAP_L_CONS_COLLECT = prove( 860 ``!xs y. 861 RTC R_parse (ts,MAP L_CONS xs ++ [L_STOP] ++ s,L_COLLECT y,mem) 862 (ts,s,L_RETURN (FOLDL (\x y. Dot y x) y xs),mem)``, 863 Induct THEN1 864 (SIMP_TAC std_ss [MAP,FOLDL,APPEND] \\ REPEAT STRIP_TAC 865 \\ MATCH_MP_TAC RTC_SINGLE 866 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 867 \\ SIMP_TAC std_ss [MAP,FOLDL,APPEND] \\ REPEAT STRIP_TAC 868 \\ MATCH_MP_TAC RTC_UNROLL 869 \\ Q.EXISTS_TAC `(ts,(MAP L_CONS xs ++ [L_STOP] ++ s),L_COLLECT (Dot h y),mem)` 870 \\ STRIP_TAC 871 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 872 \\ ASM_SIMP_TAC std_ss []); 873 874val cons_atoms_FOLDL = prove( 875 ``!y xs. 876 ~(isAtom abbrevs y) ==> 877 RTC R_parse 878 (ts,cons_atoms abbrevs y (MAP L_CONS xs ++ [L_STOP] ++ s),L_COLLECT (Sym "NIL"),mem) 879 (ts,s,L_RETURN (FOLDL (\x y. Dot y x) y xs),mem)``, 880 completeInduct_on `LSIZE y` \\ REPEAT STRIP_TAC 881 \\ ONCE_REWRITE_TAC [cons_atoms_def] 882 \\ ASM_SIMP_TAC std_ss [] \\ SRW_TAC [] [] 883 THEN1 884 (`isDot y` by METIS_TAC [isAtom_def] 885 \\ FULL_SIMP_TAC std_ss [isDot_thm,CAR_def] \\ FULL_SIMP_TAC std_ss [CDR_def] 886 \\ MATCH_MP_TAC RTC_UNROLL 887 \\ Q.EXISTS_TAC `(ts,MAP L_CONS xs ++ [L_STOP] ++ s, L_COLLECT y,mem)` 888 \\ STRIP_TAC 889 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 890 \\ ASM_SIMP_TAC std_ss [MAP_L_CONS_COLLECT]) 891 THEN1 892 (`isDot y` by METIS_TAC [isAtom_def] 893 \\ FULL_SIMP_TAC std_ss [isDot_thm,CAR_def] \\ FULL_SIMP_TAC std_ss [CDR_def] 894 \\ MATCH_MP_TAC RTC_UNROLL 895 \\ Q.EXISTS_TAC `(ts,L_DOT::L_CONS a::(MAP L_CONS xs ++ [L_STOP] ++ s), L_COLLECT (Dot b (Sym "NIL")),mem)` 896 \\ STRIP_TAC 897 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 898 \\ MATCH_MP_TAC RTC_UNROLL 899 \\ Q.EXISTS_TAC `(ts,L_CONS a::(MAP L_CONS xs ++ [L_STOP] ++ s), L_COLLECT b,mem)` 900 \\ STRIP_TAC 901 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [CAR_def]) 902 \\ MATCH_MP_TAC RTC_UNROLL 903 \\ Q.EXISTS_TAC `(ts,(MAP L_CONS xs ++ [L_STOP] ++ s), L_COLLECT (Dot a b),mem)` 904 \\ STRIP_TAC 905 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [CAR_def]) 906 \\ ASM_SIMP_TAC std_ss [MAP_L_CONS_COLLECT]) 907 \\ `isDot y` by METIS_TAC [isAtom_def] 908 \\ FULL_SIMP_TAC std_ss [isDot_thm] 909 \\ FULL_SIMP_TAC std_ss [LSIZE_def,CDR_def,CAR_def] 910 \\ `LSIZE b < SUC (LSIZE a + LSIZE b)` by DECIDE_TAC 911 \\ RES_TAC \\ POP_ASSUM (MP_TAC o Q.SPEC `b`) 912 \\ Q.PAT_X_ASSUM `!m.bb` (K ALL_TAC) 913 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 914 \\ POP_ASSUM (MP_TAC o Q.SPEC `a::xs`) 915 \\ SIMP_TAC std_ss [APPEND,MAP,FOLDL]); 916 917val R_parse_lemma = prove( 918 ``!exp b ts s mem ps. 919 (~b ==> ~(s = []) /\ ~(HD s = L_QUOTE) /\ ~(?k. HD s = L_STORE k)) /\ 920 FMAP_11 abbrevs /\ R_parse_abbrev abbrevs ps mem ==> 921 ?ps5 mem5 str5. 922 (sexp2abbrevt_aux exp b abbrevs ps = (str5,ps5)) /\ 923 RTC R_parse (str5 ++ ts,s,L_READ,mem) 924 (if b then (ts,s,L_RETURN exp,mem5) 925 else (ts,cons_atoms abbrevs exp s,L_READ,mem5)) /\ 926 R_parse_abbrev abbrevs ps5 mem5``, 927 HO_MATCH_MP_TAC SExp_print_induct \\ REPEAT STRIP_TAC 928 \\ ONCE_REWRITE_TAC [sexp2abbrevt_aux_def] 929 \\ ASM_SIMP_TAC std_ss [LET_DEF] 930 \\ Q.ABBREV_TAC `index = abbrevs ' exp` 931 \\ Q.ABBREV_TAC `prefix = if exp IN FDOM abbrevs then [^TOKEN_SAVE] else []` 932 \\ Q.ABBREV_TAC `ps0 = if exp IN FDOM abbrevs then exp INSERT ps else ps` 933 \\ `(if exp IN FDOM abbrevs then 934 ([^TOKEN_SAVE],exp INSERT ps) 935 else 936 ([],ps)) = (prefix,ps0)` by METIS_TAC [] 937 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 938 \\ Cases_on `exp IN ps` \\ ASM_SIMP_TAC std_ss [] THEN1 939 (`exp IN FDOM abbrevs` by METIS_TAC [R_parse_abbrev_def] 940 \\ ASM_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `mem` 941 \\ ASM_SIMP_TAC std_ss [] 942 \\ MATCH_MP_TAC RTC_UNROLL 943 \\ FULL_SIMP_TAC std_ss [R_parse_abbrev_def] 944 \\ Q.UNABBREV_TAC `index` 945 \\ RES_TAC 946 \\ Q.EXISTS_TAC `(ts,s,L_RETURN exp,mem)` 947 \\ STRIP_TAC 948 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 949 \\ Cases_on `b` \\ FULL_SIMP_TAC std_ss [RTC_REFL] 950 \\ MATCH_MP_TAC RTC_SINGLE 951 \\ ONCE_REWRITE_TAC [cons_atoms_def] 952 \\ ASM_SIMP_TAC std_ss [isAtom_def] 953 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 954 \\ `?str1 ps1. sexp2abbrevt_aux (CAR exp) T abbrevs ps = (str1,ps1)` by METIS_TAC [PAIR] 955 \\ `?str2 ps2. sexp2abbrevt_aux (CDR exp) F abbrevs ps1 = (str2,ps2)` by METIS_TAC [PAIR] 956 \\ `?str3 ps3. sexp2abbrevt_aux (CAR (CDR exp)) T abbrevs ps = (str3,ps3)` by METIS_TAC [PAIR] 957 \\ ASM_SIMP_TAC std_ss [] 958 \\ Q.ABBREV_TAC `s1 = if b \/ prefix <> [] then [^TOKEN_OPEN] else []` 959 \\ Q.ABBREV_TAC `s2 = if b \/ prefix <> [] then [^TOKEN_CLOSE] else []` 960 \\ `(if b \/ prefix <> [] then ([^TOKEN_OPEN],[^TOKEN_CLOSE]) 961 else ([],[])) = (s1,s2)` by METIS_TAC [] 962 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 963 \\ `!tts. RTC R_parse (prefix ++ tts,s,L_READ,mem) 964 (tts,(if exp IN FDOM abbrevs 965 then (L_STORE (abbrevs ' exp))::s else s),L_READ,mem)` by 966 (Q.UNABBREV_TAC `prefix` 967 \\ REVERSE (Cases_on `exp IN FDOM abbrevs`) 968 \\ ASM_SIMP_TAC std_ss [APPEND,RTC_REFL] 969 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC RTC_SINGLE 970 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 971 \\ Q.ABBREV_TAC `s9 = if exp IN FDOM abbrevs then L_STORE (abbrevs ' exp)::s else s` 972 \\ Cases_on `~(isDot exp)` \\ ASM_SIMP_TAC std_ss [] THEN1 973 (ONCE_REWRITE_TAC [cons_atoms_def] \\ ASM_SIMP_TAC std_ss [isAtom_def,isDot_def] 974 \\ Q.EXISTS_TAC `if exp IN FDOM abbrevs then (abbrevs ' exp =+ exp) mem else mem` 975 \\ REVERSE STRIP_TAC THEN1 976 (Q.UNABBREV_TAC `ps0` \\ POP_ASSUM (ASSUME_TAC o GSYM) 977 \\ FULL_SIMP_TAC std_ss [] \\ Cases_on `exp IN FDOM abbrevs` 978 \\ ASM_SIMP_TAC std_ss [] 979 \\ FULL_SIMP_TAC std_ss [IN_INSERT,R_parse_abbrev_def,APPLY_UPDATE_THM] 980 \\ CONV_TAC (RAND_CONV (ALPHA_CONV ``exp2:SExp``)) \\ STRIP_TAC 981 \\ Cases_on `exp2 = exp` \\ ASM_SIMP_TAC std_ss [] 982 \\ REPEAT STRIP_TAC \\ RES_TAC \\ METIS_TAC [FMAP_11_def]) 983 \\ Q.ABBREV_TAC `mem2 = if exp IN FDOM abbrevs then (abbrevs ' exp =+ exp) mem else mem` 984 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 985 \\ Q.EXISTS_TAC `([(exp,Val 0)] ++ ts,s9,L_READ,mem)` 986 \\ ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 987 \\ MATCH_MP_TAC RTC_UNROLL 988 \\ Q.EXISTS_TAC `(ts,s9,L_RETURN exp,mem)` 989 \\ STRIP_TAC 990 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 991 \\ Q.UNABBREV_TAC `s9` 992 \\ Q.UNABBREV_TAC `mem2` 993 \\ REVERSE (Cases_on `exp IN FDOM abbrevs` \\ ASM_SIMP_TAC std_ss []) 994 THEN1 (Cases_on `b` \\ FULL_SIMP_TAC std_ss [RTC_REFL] \\ MATCH_MP_TAC RTC_SINGLE 995 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 996 \\ MATCH_MP_TAC RTC_UNROLL 997 \\ Q.EXISTS_TAC `(ts,s,L_RETURN exp,(abbrevs ' exp =+ exp) mem)` 998 \\ STRIP_TAC 999 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1000 THEN1 (Cases_on `b` \\ FULL_SIMP_TAC std_ss [RTC_REFL] \\ MATCH_MP_TAC RTC_SINGLE 1001 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [])) 1002 \\ Cases_on `isQuote exp` \\ ASM_SIMP_TAC std_ss [] THEN1 1003 (ONCE_REWRITE_TAC [cons_atoms_def] \\ ASM_SIMP_TAC std_ss [isAtom_def,isDot_def] 1004 \\ FULL_SIMP_TAC std_ss [isQuote_thm] \\ FULL_SIMP_TAC std_ss [CAR_def,CDR_def] 1005 \\ FULL_SIMP_TAC std_ss [] 1006 \\ Q.PAT_X_ASSUM `!b ts. bbb` (MP_TAC o Q.SPECL [`T`,`ts`,`L_QUOTE::s9`,`mem`,`ps`]) 1007 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 1008 \\ Q.ABBREV_TAC `mem6 = if exp IN FDOM abbrevs then (abbrevs ' exp =+ exp) mem5 else mem5` 1009 \\ Q.EXISTS_TAC `mem6` 1010 \\ REVERSE STRIP_TAC THEN1 1011 (Q.UNABBREV_TAC `mem6` \\ POP_ASSUM (ASSUME_TAC o GSYM) 1012 \\ FULL_SIMP_TAC std_ss [] \\ Cases_on `exp IN FDOM abbrevs` 1013 \\ ASM_SIMP_TAC std_ss [] 1014 \\ FULL_SIMP_TAC std_ss [IN_INSERT,R_parse_abbrev_def,APPLY_UPDATE_THM] 1015 \\ CONV_TAC (RAND_CONV (ALPHA_CONV ``exp2:SExp``)) \\ STRIP_TAC 1016 \\ Cases_on `exp2 = exp` \\ ASM_SIMP_TAC std_ss [] 1017 \\ Q.PAT_X_ASSUM `exp = bbbb` (ASSUME_TAC o GSYM) 1018 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,IN_INSERT] 1019 \\ REPEAT STRIP_TAC \\ RES_TAC \\ METIS_TAC [FMAP_11_def]) 1020 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1021 \\ Q.EXISTS_TAC `([^TOKEN_QUOTE] ++ str3 ++ ts,s9,L_READ,mem)` 1022 \\ ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 1023 \\ MATCH_MP_TAC RTC_UNROLL 1024 \\ Q.EXISTS_TAC `(str3 ++ ts,L_QUOTE::s9,L_READ,mem)` 1025 \\ STRIP_TAC 1026 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1027 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1028 \\ Q.EXISTS_TAC `(ts,L_QUOTE::s9,L_RETURN y,mem5)` 1029 \\ ASM_SIMP_TAC std_ss [] 1030 \\ MATCH_MP_TAC RTC_UNROLL 1031 \\ Q.EXISTS_TAC `(ts,s9,L_RETURN exp,mem5)` 1032 \\ STRIP_TAC 1033 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1034 \\ Q.PAT_X_ASSUM `exp = bbbb` (ASSUME_TAC o GSYM) 1035 \\ FULL_SIMP_TAC std_ss [] 1036 \\ Q.UNABBREV_TAC `s9` 1037 \\ Q.UNABBREV_TAC `mem6` 1038 \\ REVERSE (Cases_on `exp IN FDOM abbrevs` \\ ASM_SIMP_TAC std_ss []) 1039 THEN1 (Cases_on `b` \\ FULL_SIMP_TAC std_ss [RTC_REFL] \\ MATCH_MP_TAC RTC_SINGLE 1040 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1041 \\ MATCH_MP_TAC RTC_UNROLL 1042 \\ Q.EXISTS_TAC `(ts,s,L_RETURN exp,(abbrevs ' exp =+ exp) mem5)` 1043 \\ STRIP_TAC 1044 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1045 THEN1 (Cases_on `b` \\ FULL_SIMP_TAC std_ss [RTC_REFL] \\ MATCH_MP_TAC RTC_SINGLE 1046 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [])) 1047 \\ FULL_SIMP_TAC std_ss [] 1048 \\ `?a1 a2. exp = Dot a1 a2` by METIS_TAC [isDot_thm] 1049 \\ FULL_SIMP_TAC std_ss [CAR_def,CDR_def] 1050 \\ Cases_on `a2 = Sym "NIL"` \\ FULL_SIMP_TAC std_ss [APPEND_NIL] THEN1 1051 (Q.PAT_X_ASSUM `!b ts. bbb` (K ALL_TAC) 1052 \\ Q.ABBREV_TAC `s8 = if s1 = [] then s9 else L_STOP::s9` 1053 \\ Q.PAT_X_ASSUM `!b ts. bbb` (MP_TAC o Q.SPECL [`T`,`s2++ts`,`s8`,`mem`,`ps`]) 1054 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 1055 \\ Q.ABBREV_TAC `mem6 = if exp IN FDOM abbrevs then (abbrevs ' exp =+ exp) mem5 else mem5` 1056 \\ Q.EXISTS_TAC `mem6` 1057 \\ REVERSE STRIP_TAC THEN1 1058 (Q.UNABBREV_TAC `mem6` \\ POP_ASSUM (ASSUME_TAC o GSYM) 1059 \\ FULL_SIMP_TAC std_ss [] \\ Cases_on `exp IN FDOM abbrevs` 1060 \\ ASM_SIMP_TAC std_ss [] 1061 \\ FULL_SIMP_TAC std_ss [IN_INSERT,R_parse_abbrev_def,APPLY_UPDATE_THM] 1062 \\ CONV_TAC (RAND_CONV (ALPHA_CONV ``exp2:SExp``)) \\ STRIP_TAC 1063 \\ Cases_on `exp2 = exp` \\ ASM_SIMP_TAC std_ss [] 1064 \\ Q.PAT_X_ASSUM `exp = bbbb` (ASSUME_TAC o GSYM) 1065 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,IN_INSERT] 1066 \\ REPEAT STRIP_TAC \\ RES_TAC \\ METIS_TAC [FMAP_11_def]) 1067 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1068 \\ Q.EXISTS_TAC `(s1 ++ str1 ++ s2 ++ ts,s9,L_READ,mem)` 1069 \\ ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 1070 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1071 \\ Q.EXISTS_TAC `((str1 ++ (s2 ++ ts)),s8,L_READ,mem)` 1072 \\ STRIP_TAC THEN1 1073 (Q.UNABBREV_TAC `s8` \\ Cases_on `s1 = []` 1074 \\ ASM_SIMP_TAC std_ss [APPEND,RTC_REFL] 1075 \\ Q.UNABBREV_TAC `s1` \\ Cases_on `b \/ prefix <> []` 1076 \\ FULL_SIMP_TAC std_ss [NOT_CONS_NIL] 1077 \\ FULL_SIMP_TAC std_ss [NOT_CONS_NIL] 1078 \\ MATCH_MP_TAC RTC_SINGLE 1079 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1080 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1081 \\ Q.EXISTS_TAC `(s2 ++ ts,s8,L_RETURN a1,mem5)` 1082 \\ ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 1083 \\ MATCH_MP_TAC RTC_UNROLL 1084 \\ Q.EXISTS_TAC `(s2 ++ ts,L_CONS a1::s8,L_READ,mem5)` 1085 \\ STRIP_TAC 1086 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [] 1087 \\ FULL_SIMP_TAC std_ss [markerTheory.Abbrev_def] 1088 \\ Cases_on `b` \\ FULL_SIMP_TAC (srw_ss()) [NOT_CONS_NIL,HD] 1089 \\ METIS_TAC [NOT_CONS_NIL,fetch "-" "lisp_parse_action_distinct",HD,CONS_11]) 1090 \\ Cases_on `s2 = []` THEN1 1091 (`~b` by METIS_TAC [NOT_CONS_NIL] 1092 \\ `s1 = []` by METIS_TAC [NOT_CONS_NIL] 1093 \\ FULL_SIMP_TAC std_ss [APPEND] 1094 \\ Q.UNABBREV_TAC `s8` 1095 \\ `(s9 = s) /\ ~(exp IN FDOM abbrevs)` by METIS_TAC [NOT_CONS_NIL] 1096 \\ POP_ASSUM MP_TAC 1097 \\ ONCE_REWRITE_TAC [cons_atoms_def] \\ Q.UNABBREV_TAC `mem6` 1098 \\ ASM_SIMP_TAC std_ss [isAtom_def,CAR_def,CDR_def,RTC_REFL]) 1099 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1100 \\ Q.EXISTS_TAC `(ts,s9,L_RETURN exp,mem5)` 1101 \\ STRIP_TAC THEN1 1102 (`s2 = [^TOKEN_CLOSE]` by METIS_TAC [] \\ ASM_SIMP_TAC std_ss [APPEND] 1103 \\ `s8 = L_STOP::s9` by METIS_TAC [NOT_CONS_NIL] \\ ASM_SIMP_TAC std_ss [] 1104 \\ MATCH_MP_TAC RTC_UNROLL 1105 \\ Q.EXISTS_TAC `(ts,L_CONS a1::L_STOP::s9,L_COLLECT (Sym "NIL"),mem5)` 1106 \\ STRIP_TAC 1107 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1108 \\ MATCH_MP_TAC RTC_UNROLL 1109 \\ Q.EXISTS_TAC `(ts,L_STOP::s9,L_COLLECT (Dot a1 (Sym "NIL")),mem5)` 1110 \\ STRIP_TAC 1111 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1112 \\ MATCH_MP_TAC RTC_UNROLL 1113 \\ Q.EXISTS_TAC `(ts,s9,L_RETURN (Dot a1 (Sym "NIL")),mem5)` 1114 \\ STRIP_TAC 1115 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1116 \\ ASM_SIMP_TAC std_ss [RTC_REFL]) 1117 \\ Q.PAT_X_ASSUM `exp = bbbb` (ASSUME_TAC o GSYM) 1118 \\ FULL_SIMP_TAC std_ss [] 1119 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1120 \\ Q.EXISTS_TAC `(ts,s,L_RETURN exp,mem6)` 1121 \\ STRIP_TAC THEN1 1122 (Q.UNABBREV_TAC `s9` \\ Q.UNABBREV_TAC `mem6` 1123 \\ Cases_on `exp IN FDOM abbrevs` \\ ASM_SIMP_TAC std_ss [RTC_REFL] 1124 \\ MATCH_MP_TAC RTC_SINGLE 1125 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1126 \\ Cases_on `b` \\ FULL_SIMP_TAC std_ss [RTC_REFL] 1127 \\ ONCE_REWRITE_TAC [cons_atoms_def] 1128 \\ `isAtom abbrevs exp` by METIS_TAC [NOT_CONS_NIL,isAtom_def] 1129 \\ ASM_SIMP_TAC std_ss [] 1130 \\ MATCH_MP_TAC RTC_SINGLE 1131 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1132 \\ Q.PAT_X_ASSUM `!b ts. bbb` MP_TAC 1133 \\ Q.ABBREV_TAC `s8 = if s1 = [] then s9 else L_STOP::s9` 1134 \\ Q.ABBREV_TAC `s7 = if isAtom abbrevs a2 then L_DOT::L_CONS a1::s8 else L_CONS a1::s8` 1135 \\ `~(s7 = [])` by METIS_TAC [NOT_CONS_NIL] 1136 \\ `~(s8 = [])` by (FULL_SIMP_TAC std_ss [markerTheory.Abbrev_def] \\ Cases_on `b` 1137 \\ FULL_SIMP_TAC std_ss [NOT_CONS_NIL] \\ METIS_TAC [NOT_CONS_NIL]) 1138 \\ `HD s7 <> L_QUOTE /\ (!k. HD s7 <> L_STORE k)` by 1139 (METIS_TAC [NOT_CONS_NIL,fetch "-" "lisp_parse_action_distinct",HD,CONS_11]) 1140 \\ Q.PAT_X_ASSUM `!b ts. bbb` (MP_TAC o Q.SPECL [`T`,`((if isAtom (abbrevs:SExp|->num) a2 then [^TOKEN_DOT] else []) ++ str2) ++ s2++ts`,`s8`,`mem`,`ps`]) 1141 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 1142 \\ POP_ASSUM (MP_TAC o Q.SPECL [`F`,`s2++ts`,`s7`,`mem5`,`ps1`]) 1143 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 1144 \\ Q.ABBREV_TAC `mem6 = if exp IN FDOM abbrevs then (abbrevs ' exp =+ exp) mem5' else mem5'` 1145 \\ Q.EXISTS_TAC `mem6` 1146 \\ REVERSE STRIP_TAC THEN1 1147 (Q.UNABBREV_TAC `mem6` \\ POP_ASSUM (ASSUME_TAC o GSYM) 1148 \\ FULL_SIMP_TAC std_ss [] \\ Cases_on `exp IN FDOM abbrevs` 1149 \\ ASM_SIMP_TAC std_ss [] 1150 \\ FULL_SIMP_TAC std_ss [IN_INSERT,R_parse_abbrev_def,APPLY_UPDATE_THM] 1151 \\ CONV_TAC (RAND_CONV (ALPHA_CONV ``exp2:SExp``)) \\ STRIP_TAC 1152 \\ Cases_on `exp2 = exp` \\ ASM_SIMP_TAC std_ss [] 1153 \\ Q.PAT_X_ASSUM `exp = bbbb` (ASSUME_TAC o GSYM) 1154 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,IN_INSERT,R_parse_abbrev_def] 1155 \\ REPEAT STRIP_TAC \\ RES_TAC \\ METIS_TAC [FMAP_11_def]) 1156 \\ Q.ABBREV_TAC `dot = if isAtom abbrevs a2 then [^TOKEN_DOT] else []` 1157 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1158 \\ Q.EXISTS_TAC `(s1 ++ str1 ++ (dot ++ str2) ++ s2 ++ ts,s9,L_READ,mem)` 1159 \\ ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 1160 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1161 \\ Q.EXISTS_TAC `(str1 ++ (dot ++ (str2 ++ (s2 ++ ts))),s8,L_READ,mem)` 1162 \\ STRIP_TAC THEN1 1163 (Q.UNABBREV_TAC `s8` \\ Cases_on `s1 = []` 1164 \\ ASM_SIMP_TAC std_ss [APPEND,RTC_REFL] 1165 \\ Q.UNABBREV_TAC `s1` \\ Cases_on `b \/ prefix <> []` 1166 \\ FULL_SIMP_TAC std_ss [NOT_CONS_NIL] 1167 \\ FULL_SIMP_TAC std_ss [NOT_CONS_NIL] 1168 \\ MATCH_MP_TAC RTC_SINGLE 1169 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1170 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1171 \\ Q.EXISTS_TAC `(dot ++ str2 ++ s2 ++ ts,s8,L_RETURN a1,mem5)` 1172 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 1173 \\ MATCH_MP_TAC RTC_UNROLL 1174 \\ Q.EXISTS_TAC `(dot ++ (str2 ++ (s2 ++ ts)),L_CONS a1::s8,L_READ,mem5)` 1175 \\ STRIP_TAC 1176 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [] 1177 \\ METIS_TAC [NOT_CONS_NIL,fetch "-" "lisp_parse_action_distinct",HD,CONS_11]) 1178 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1179 \\ Q.EXISTS_TAC `(str2 ++ s2 ++ ts,s7,L_READ,mem5)` 1180 \\ STRIP_TAC THEN1 1181 (Q.UNABBREV_TAC `dot` \\ Q.UNABBREV_TAC `s7` 1182 \\ Cases_on `isAtom abbrevs a2` \\ ASM_SIMP_TAC std_ss [] 1183 \\ FULL_SIMP_TAC std_ss [RTC_REFL,APPEND,APPEND_ASSOC] 1184 \\ MATCH_MP_TAC RTC_SINGLE 1185 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1186 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1187 \\ Q.EXISTS_TAC `(s2 ++ ts,cons_atoms abbrevs a2 s7,L_READ,mem5')` 1188 \\ ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 1189 \\ Cases_on `s2 = []` THEN1 1190 (`~b` by METIS_TAC [NOT_CONS_NIL] 1191 \\ `s1 = []` by METIS_TAC [NOT_CONS_NIL] 1192 \\ FULL_SIMP_TAC std_ss [APPEND] 1193 \\ Q.UNABBREV_TAC `s8` 1194 \\ Q.UNABBREV_TAC `s7` 1195 \\ `(s9 = s) /\ ~(exp IN FDOM abbrevs)` by METIS_TAC [NOT_CONS_NIL] 1196 \\ POP_ASSUM MP_TAC 1197 \\ ASM_SIMP_TAC std_ss [] 1198 \\ Cases_on `isAtom abbrevs a2` \\ ASM_SIMP_TAC std_ss [] 1199 \\ Q.UNABBREV_TAC `mem6` 1200 \\ REPEAT STRIP_TAC 1201 \\ `~(isAtom abbrevs (Dot a1 a2))` by (FULL_SIMP_TAC std_ss [isAtom_def]) 1202 \\ ASM_SIMP_TAC std_ss [cons_atoms_lemma,RTC_REFL] 1203 \\ ONCE_REWRITE_TAC [cons_atoms_def] \\ ASM_SIMP_TAC std_ss [RTC_REFL]) 1204 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1205 \\ Q.EXISTS_TAC `(ts,s9,L_RETURN exp,mem5')` 1206 \\ STRIP_TAC THEN1 1207 (`s2 = [^TOKEN_CLOSE]` by METIS_TAC [] \\ ASM_SIMP_TAC std_ss [APPEND] 1208 \\ `s8 = L_STOP::s9` by METIS_TAC [NOT_CONS_NIL] \\ ASM_SIMP_TAC std_ss [] 1209 \\ MATCH_MP_TAC RTC_UNROLL 1210 \\ Q.EXISTS_TAC `(ts,cons_atoms abbrevs a2 s7,L_COLLECT (Sym "NIL"),mem5')` 1211 \\ STRIP_TAC 1212 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1213 \\ Q.UNABBREV_TAC `s7` \\ ASM_SIMP_TAC std_ss [] 1214 \\ Cases_on `isAtom abbrevs a2` \\ ASM_SIMP_TAC std_ss [] THEN1 1215 (ONCE_REWRITE_TAC [cons_atoms_def] \\ ASM_SIMP_TAC std_ss [] 1216 \\ MATCH_MP_TAC RTC_UNROLL 1217 \\ Q.EXISTS_TAC `(ts,L_DOT::L_CONS a1::L_STOP::s9,L_COLLECT (Dot a2 (Sym "NIL")),mem5')` 1218 \\ STRIP_TAC 1219 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1220 \\ MATCH_MP_TAC RTC_UNROLL 1221 \\ Q.EXISTS_TAC `(ts,L_CONS a1::L_STOP::s9,L_COLLECT a2,mem5')` 1222 \\ STRIP_TAC 1223 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [CAR_def]) 1224 \\ MATCH_MP_TAC RTC_UNROLL 1225 \\ Q.EXISTS_TAC `(ts,L_STOP::s9,L_COLLECT (Dot a1 a2),mem5')` 1226 \\ STRIP_TAC 1227 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [CAR_def]) 1228 \\ MATCH_MP_TAC RTC_UNROLL 1229 \\ Q.EXISTS_TAC `(ts,s9,L_RETURN (Dot a1 a2),mem5')` 1230 \\ STRIP_TAC 1231 THEN1 (ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) [CAR_def]) 1232 \\ ASM_SIMP_TAC std_ss [RTC_REFL]) 1233 \\ MATCH_MP_TAC (SIMP_RULE std_ss [MAP,APPEND,FOLDL] (Q.SPECL [`a2`,`[a1]`] cons_atoms_FOLDL)) 1234 \\ ASM_SIMP_TAC std_ss []) 1235 \\ Q.PAT_X_ASSUM `exp = bbbb` (ASSUME_TAC o GSYM) 1236 \\ FULL_SIMP_TAC std_ss [] 1237 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1238 \\ Q.EXISTS_TAC `(ts,s,L_RETURN exp,mem6)` 1239 \\ STRIP_TAC THEN1 1240 (Q.UNABBREV_TAC `s9` \\ Q.UNABBREV_TAC `mem6` 1241 \\ Cases_on `exp IN FDOM abbrevs` \\ ASM_SIMP_TAC std_ss [RTC_REFL] 1242 \\ MATCH_MP_TAC RTC_SINGLE 1243 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 1244 \\ Cases_on `b` \\ FULL_SIMP_TAC std_ss [RTC_REFL] 1245 \\ `exp IN FDOM abbrevs` by METIS_TAC [NOT_CONS_NIL] 1246 \\ ASM_SIMP_TAC std_ss [Once cons_atoms_def,isAtom_def] 1247 \\ MATCH_MP_TAC RTC_SINGLE 1248 \\ ONCE_REWRITE_TAC [R_parse_cases] \\ FULL_SIMP_TAC (srw_ss()) []); 1249 1250val R_parse_thm = prove( 1251 ``!exp ts s mem abbrevs. 1252 FMAP_11 abbrevs ==> 1253 ?mem2. 1254 RTC R_parse (FST (sexp2abbrevt_aux exp T abbrevs {}) ++ ts,s,L_READ,mem) 1255 (ts,s,L_RETURN exp,mem2)``, 1256 REPEAT STRIP_TAC 1257 \\ `?str ps. sexp2abbrevt_aux exp T abbrevs {} = (str,ps)` by METIS_TAC [PAIR] 1258 \\ MP_TAC (Q.SPECL [`exp`,`T`,`ts`,`s`,`mem`,`{}`] R_parse_lemma) 1259 \\ ASM_SIMP_TAC std_ss [R_parse_abbrev_def,NOT_IN_EMPTY] \\ METIS_TAC []); 1260 1261val sexp_parse_def = Define ` 1262 sexp_parse ts = sexp_parse_aux (ts,[],L_READ,\x.Sym "NIL")`; 1263 1264val sexp_parse_aux_sexp2abbrevt = prove( 1265 ``!exp ts abbrevs. 1266 FMAP_11 abbrevs ==> 1267 (sexp_parse (FST (sexp2abbrevt_aux exp T abbrevs {}) ++ ts) = exp)``, 1268 METIS_TAC [R_parse_thm,RTC_parse_IMP_sexp_parse_aux,FST,SND,sexp_parse_def]); 1269 1270val string2sexp_def = Define ` 1271 string2sexp str = (sexp_parse (FST (sexp_lex str)))`; 1272 1273val FDOM_sexp_abbrev_fmap_IMP = prove( 1274 ``!xs x k. x IN FDOM (sexp_abbrev_fmap xs k) ==> 1275 k <= sexp_abbrev_fmap xs k ' x``, 1276 Induct \\ SIMP_TAC (srw_ss()) [sexp_abbrev_fmap_def, 1277 FDOM_FEMPTY,FAPPLY_FUPDATE_THM] \\ REPEAT STRIP_TAC 1278 \\ ASM_SIMP_TAC std_ss [] \\ RES_TAC 1279 \\ METIS_TAC [LESS_EQ_REFL,DECIDE ``k <= k+1:num``,LESS_EQ_TRANS]); 1280 1281val FMAP_11_sexp_abbrev_fmap = prove( 1282 ``!xs k. FMAP_11 (sexp_abbrev_fmap xs k)``, 1283 Induct \\ SIMP_TAC (srw_ss()) [sexp_abbrev_fmap_def, 1284 FMAP_11_def,FDOM_FEMPTY,FAPPLY_FUPDATE_THM] 1285 \\ REVERSE (REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] \\ SRW_TAC [] []) 1286 THEN1 METIS_TAC [FMAP_11_def] 1287 \\ IMP_RES_TAC FDOM_sexp_abbrev_fmap_IMP \\ DECIDE_TAC); 1288 1289val string2sexp_sexp2abbrev = store_thm("string2sexp_sexp2abbrev", 1290 ``!exp abbrevs. string2sexp (sexp2abbrev exp abbrevs) = exp``, 1291 SIMP_TAC std_ss [string2sexp_def,sexp2abbrev_def,sexp_lex_sexp2abbrev_aux] 1292 \\ METIS_TAC [sexp_parse_aux_sexp2abbrevt,FMAP_11_sexp_abbrev_fmap,APPEND_NIL]); 1293 1294val string2sexp_sexp2string = store_thm("string2sexp_sexp2string", 1295 ``!exp. string2sexp (sexp2string exp) = exp``, 1296 ASM_SIMP_TAC std_ss [GSYM sexp2abbrev_NIL,string2sexp_sexp2abbrev]); 1297 1298 1299(* Part 2 - section 3: merge lexer and parser *) 1300 1301val next_token_IMP = prove( 1302 ``(((p,Val n),ds) = next_token cs) ==> LENGTH ds < LENGTH cs``, 1303 ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ REPEAT STRIP_TAC \\ IMP_RES_TAC next_token_LENGTH 1304 \\ FULL_SIMP_TAC std_ss [next_token_def,SExp_distinct]); 1305 1306val sexp_lex_parse_def = tDefine "sexp_lex_parse" ` 1307 (sexp_lex_parse (cs,s,L_READ,mem) = 1308 let (t,cs) = next_token cs in 1309 if SND t = Sym "NIL" then (Sym "NIL",cs) else (* error or end of input *) 1310 if SND t = Val 0 then sexp_lex_parse (cs,s,L_RETURN (FST t),mem) else 1311 if (t = ^TOKEN_OPEN) then sexp_lex_parse (cs,L_STOP::s,L_READ,mem) else 1312 if (t = ^TOKEN_DOT) then sexp_lex_parse (cs,L_DOT::s,L_READ,mem) else 1313 if (t = ^TOKEN_QUOTE) then sexp_lex_parse (cs,L_QUOTE::s,L_READ,mem) else 1314 if (t = ^TOKEN_CLOSE) then sexp_lex_parse (cs,s,L_COLLECT (Sym "NIL"),mem) else 1315 if ~isVal (FST t) then (Sym "NIL",cs) else 1316 if SND t = Val 3 then sexp_lex_parse (cs,s,L_RETURN (mem (getVal (FST t))),mem) else 1317 if SND t = Val 2 then sexp_lex_parse (cs,L_STORE (getVal (FST t))::s,L_READ,mem) else 1318 (Sym "NIL",cs)) /\ 1319 (sexp_lex_parse (cs,s,L_COLLECT exp,mem) = 1320 if s = [] then (Sym "NIL",cs) else 1321 let (x,s) = (HD s, TL s) in 1322 if x = L_STOP then sexp_lex_parse (cs,s,L_RETURN exp,mem) else 1323 if ~(READ_L_CONS x = NONE) then sexp_lex_parse (cs,s,L_COLLECT (Dot (THE (READ_L_CONS x)) exp),mem) else 1324 if x = L_DOT then sexp_lex_parse (cs,s,L_COLLECT (CAR exp),mem) else 1325 (Sym "NIL",cs)) /\ 1326 (sexp_lex_parse (cs,s,L_RETURN exp,mem) = 1327 if s = [] then (exp,cs) else 1328 let (x,s) = (HD s, TL s) in 1329 if x = L_QUOTE then sexp_lex_parse (cs,s,L_RETURN (Dot (Sym "QUOTE") (Dot exp (Sym "NIL"))),mem) else 1330 if ~(READ_L_STORE x = NONE) then sexp_lex_parse (cs,s,L_RETURN exp,(THE (READ_L_STORE x) =+ exp) mem) else 1331 sexp_lex_parse (cs,L_CONS exp::x::s,L_READ,mem))` 1332 (WF_REL_TAC `measure (\(cs,s,mode,mem). 1333 3 * LENGTH cs + LENGTH s + if mode = L_READ then 0 else 2)` 1334 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC NOT_NIL_IMP 1335 \\ IMP_RES_TAC next_token_IMP \\ FULL_SIMP_TAC (srw_ss()) [] \\ DECIDE_TAC); 1336 1337val sexp_parse_stream_def = Define ` 1338 sexp_parse_stream cs = sexp_lex_parse (cs,[],L_READ,\x.Sym "NIL")`; 1339 1340 1341(* 1342 1343val sexp_lex_parse_thm = prove( 1344 ``!cs ds s x mem. 1345 (~(ds = []) ==> MEM (HD ds) " )") ==> 1346 (sexp_lex_parse (cs++ds,s,x,mem) = 1347 (sexp_parse_aux (FST (sexp_lex (cs++ds)),s,x,mem),ds))``, 1348 1349val sexp_parse_stream_thm = store_thm("sexp_parse_stream_thm", 1350 ``!exp abbrevs s. 1351 (~(s = []) ==> MEM (HD s) " )") ==> 1352 (sexp_parse_stream (sexp2abbrev exp abbrevs ++ s) = (exp,s))``, 1353 SIMP_TAC std_ss [sexp_parse_stream_def] \\ REPEAT STRIP_TAC 1354 \\ IMP_RES_TAC sexp_lex_parse_thm \\ ASM_SIMP_TAC std_ss [] 1355 \\ ASM_SIMP_TAC std_ss [sexp2abbrev_def] 1356 \\ `?xs1 ps1. sexp2abbrev_aux exp T (sexp_abbrev_fmap abbrevs 0) {} = (xs1,ps1)` by METIS_TAC [PAIR] 1357 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (ASSUME_TAC o GSYM) 1358 \\ `?xs2 ps2. (xs2,ps2) = sexp2abbrevt_aux exp T (sexp_abbrev_fmap abbrevs 0) {}` by METIS_TAC [PAIR] 1359 \\ IMP_RES_TAC sexp2abbrev_aux_FST 1360 \\ ASM_SIMP_TAC std_ss [] 1361 \\ `xs2 = FST (sexp2abbrevt_aux exp T (sexp_abbrev_fmap abbrevs 0) {})` by 1362 (Cases_on `sexp2abbrevt_aux exp T (sexp_abbrev_fmap abbrevs 0) {}` 1363 \\ FULL_SIMP_TAC std_ss []) 1364 \\ ASM_SIMP_TAC std_ss [GSYM sexp_parse_def] 1365 \\ MATCH_MP_TAC sexp_parse_aux_sexp2abbrevt 1366 \\ ASM_SIMP_TAC std_ss [FMAP_11_sexp_abbrev_fmap]); 1367 1368*) 1369 1370val _ = export_theory(); 1371