theory LexList
  imports
    Main
    "~~/src/HOL/Library/Char_ord"
    "~~/src/HOL/Library/List_Lexorder"
begin

definition ord_ascii_zero :: nat where
  "ord_ascii_zero == of_char (CHR ''0'')"

text‹Get the string representation for a single digit.›
definition ascii_of_digit :: "nat ⇒ string" where
  "ascii_of_digit n ≡ if n ≥ 10 then undefined else [char_of (n + ord_ascii_zero)]"

fun ascii_of :: "nat ⇒ string" where
  "ascii_of n = (if n < 10
                  then ascii_of_digit n
                  else ascii_of (n div 10) @ ascii_of_digit (n mod 10))"

lemma ‹ascii_of 123 = ''123''› by code_simp

value ‹sort (map ascii_of (upt 1 13))›
end