Theory Show.Show_Real
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