Tried to speed up the lexer

get_token does a 53 long linear if-then-else to decide if a string is a
keyword or AlphaT/SymbolT.  So I wrote a tree-structured if-then-else.
Which should do 7 or 8 comparisons at most.  However, I don't now how to
do the proof.  I think I want the 256-way case split on the first
character of the string, but I don't know of a good way to get that in
HOL.

Perhaps I really must first prove
`!c. c = CHR 0 \/ c = CHR 1 \/ ... c = CHR 254 \/ c = CHR 255`
but there should be a better way.