Theory Lib_Numbers_toString

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