Remove 2 TODOs in lexer_funScript:

1. asked if next_sym needed to return an option type. It seemed to me
   that indeed it should as this was the best way to indicate
   end-of-file, flowing onto the way next_token works as well. We
   don't have a separate token for EOF so I can't see a good
   alternative.

2. a stage in next_sym_LESS asked if something was
   simpler. (Literally: "TODO: simpler?") It wasn't clear to me if
   this was a question about what was there compared to what had come
   before, or if this was a question about whether or not what was
   there could be replaced by something that was simpler.

   I decided that what was there could be made more robust (no
   dependency on variable names). I also added more quantification to
   the theorem statement because the same proof breaks on the
   signatures branch when free variables in the theorem statement end
   up being identified with variables that arise in the course of the
   proof.

semantics/lexer_funScript.sml

@@ -134,9 +134,7 @@ val read_FFIcall_reduces_input = Q.store_thm(
 val isAlphaNumPrime_def = Define`
   isAlphaNumPrime c <=> isAlphaNum c \/ (c = #"'") \/ (c = #"_")`
 
-(* next_sym reads the next symbol from a string *)
-(* TODO: why do we need an option type? *)
-
+(* next_sym reads the next symbol from a string, returning NONE if at eof *)
 val next_sym_def = tDefine "next_sym" `
   (next_sym "" _ = NONE) /\
   (next_sym (c::str) loc =
@@ -255,15 +253,13 @@ val NOT_NIL_EXISTS_CONS = Q.prove(
    (list_CASE n F P ⇔ ∃h t. n = h :: t ∧ P h t)`,
   Cases_on `n` >> simp[]);
 
-val listeq = prove_case_eq_thm {case_def = listTheory.list_case_def,
-                                nchotomy = listTheory.list_CASES}
-val optioneq = prove_case_eq_thm { nchotomy = option_nchotomy,
-                                   case_def = option_case_def}
+val listeq = CaseEq "list"
+val optioneq = CaseEq "option"
 
 
 val next_sym_LESS = Q.store_thm("next_sym_LESS",
-  `!input l. (next_sym input l = SOME (s, l', rest))
-    ==> LENGTH rest < LENGTH input`,
+  `!input l s l' rest.
+     (next_sym input l = SOME (s, l', rest)) ==> LENGTH rest < LENGTH input`,
   ho_match_mp_tac (fetch "-" "next_sym_ind") >>
   simp[next_sym_def, bool_case_eq, listeq, optioneq] >> rw[] >> fs[] >>
   rpt (pairarg_tac >> fs[]) >> rveq >> fs[NOT_NIL_EXISTS_CONS] >>
@@ -276,10 +272,9 @@ val next_sym_LESS = Q.store_thm("next_sym_LESS",
        rpt (pairarg_tac>> fs[]) >> rveq >>
        imp_res_tac read_while_thm >> simp[] >> NO_TAC) >>
   TRY (rename1 `read_FFIcall` >>
-       imp_res_tac read_FFIcall_reduces_input >> simp[] >> NO_TAC)
-  (* TODO simpler? *)
-  >> `STRLEN rest < STRLEN input` by fs[]
-  >> fs[]);
+       imp_res_tac read_FFIcall_reduces_input >> simp[] >> NO_TAC) >>
+  qpat_x_assum ‘SOME _ = next_sym _ _’ (assume_tac o SYM) >>
+  first_x_assum drule >> simp[]);
 
 val _ = Define ` init_loc = <| row := 1; col := 1; offset := 0|>`