theory Lib_Numbers_toString imports Main begin section‹Printing Numbers› (*http://stackoverflow.com/questions/23864965/string-of-nat-in-isabelle*) fun string_of_nat :: "nat ⇒ string" where "string_of_nat n = (if n < 10 then [char_of (48 + n)] else string_of_nat (n div 10) @ [char_of (48 + (n mod 10))])" definition string_of_int :: "int ⇒ string" where "string_of_int i = (if i < 0 then ''-'' @ string_of_nat (nat (- i)) else string_of_nat (nat i))" lemma "string_of_nat 123456 = ''123456''" by eval declare string_of_nat.simps[simp del] end