23 lines
673 B
Text
23 lines
673 B
Text
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
|