(*  
    Author:      René Thiemann 
    License:     LGPL
*)
section ‹Show for Real Numbers -- Interface›

text ‹We just demand that there is some function from reals to string and register this
 as show-function. Implementations are available in one of the theories \textit{Show-Real-Impl}
 and \textit{../Algebraic-Numbers/Show-Real-...}.›

theory Show_Real
imports 
  HOL.Real
  Show
  Shows_Literal
begin

consts show_real :: "real → string"

definition showsp_real :: "real showsp"
where
  "showsp_real p x y =
    (show_real x @ y)"

lemma show_law_real [show_law_intros]:
  "show_law showsp_real r"
  by (rule show_lawI) (simp add: showsp_real_def show_law_simps)

lemma showsp_real_append [show_law_simps]:
  "showsp_real p r (x @ y) = showsp_real p r x @ y"
  by (intro show_lawD show_law_intros)

local_setup ‹
 Show_Generator.register_foreign_showsp @{typ real} @{term "showsp_real"} @{thm show_law_real}
 ›

derive "show" real

instantiation real :: showl
begin
definition "showsl (x :: real) = showsl_lit (String.implode (show_real x))" 
definition "showsl_list (xs :: real list) = default_showsl_list showsl xs"
instance ..
end

end