theorem-prover/milawa-prover/milawa_coreScript.sml

141   ``!str str1.
142        ((F,str1) = is_eof str) ==>
144               LENGTH xs < LENGTH str``,
145   STRIP_TAC \\ completeInduct_on `LENGTH str` \\ STRIP_TAC
147   \\ POP_ASSUM MP_TAC \\ Cases_on `str` THEN1 EVAL_TAC
174   ``((F,str1) = is_eof str) /\ ((s,str2) = sexp_parse_stream str1) ==>
175     LENGTH str2 < LENGTH str``,
188   read_sexps str =
189     let (yes,str) = is_eof str in
191         let (s,str) = sexp_parse_stream str in
192           s::read_sexps str`
248        let (str,cs) = read_while number_char cs "" in
249          sexp_lex_parse (cs,s,L_RETURN (Val (str2num str)),mem)) /\
251        let (str,cs) = read_while number_char cs "" in
252          sexp_lex_parse (cs,s,L_RETURN (Val (10 ** STRLEN str + str2num str)),mem)) /\
254        let (str,cs) = read_while number_char cs "" in
255          sexp_lex_parse (cs,s,L_RETURN (Val (2 * 10 ** STRLEN str + str2num str)),mem)) /\
257        let (str,cs) = read_while number_char cs "" in
258          sexp_lex_parse (cs,s,L_RETURN (Val (3 * 10 ** STRLEN str + str2num str)),mem)) /\
260        let (str,cs) = read_while number_char cs "" in
261          sexp_lex_parse (cs,s,L_RETURN (Val (4 * 10 ** STRLEN str + str2num str)),mem)) /\
263        let (str,cs) = read_while number_char cs "" in
264          sexp_lex_parse (cs,s,L_RETURN (Val (5 * 10 ** STRLEN str + str2num str)),mem)) /\
266        let (str,cs) = read_while number_char cs "" in
267          sexp_lex_parse (cs,s,L_RETURN (Val (6 * 10 ** STRLEN str + str2num str)),mem)) /\
269        let (str,cs) = read_while number_char cs "" in
270          sexp_lex_parse (cs,s,L_RETURN (Val (7 * 10 ** STRLEN str + str2num str)),mem)) /\
272        let (str,cs) = read_while number_char cs "" in
273          sexp_lex_parse (cs,s,L_RETURN (Val (8 * 10 ** STRLEN str + str2num str)),mem)) /\
275        let (str,cs) = read_while number_char cs "" in
276          sexp_lex_parse (cs,s,L_RETURN (Val (9 * 10 ** STRLEN str + str2num str)),mem))``,
284       let (str,cs) = str2sym (STRING #"|" cs) in
285         sexp_lex_parse (cs,s,L_RETURN (Sym str),mem))``,
310           let (str,cs) = str2sym (STRING ^c cs) in
311             sexp_lex_parse (cs,s,L_RETURN (Sym str),mem))``,
357   val pattern = ``sexp_lex_parse (str,s,task,mem)``
358   val str_tm = ``str:string``
449   val pattern = ``read_sexps str``
450   val str_tm = ``str:string``