Theory Show.Show_Instances
section ‹Instances of the Show Class for Standard Types›
theory Show_Instances
imports
Show
HOL.Rat
begin
definition showsp_unit :: "unit showsp"
where
"showsp_unit p x = shows_string ''()''"
lemma show_law_unit [show_law_intros]:
"show_law showsp_unit x"
by (rule show_lawI) (simp add: showsp_unit_def show_law_simps)
abbreviation showsp_char :: "char showsp"
where
"showsp_char ≡ shows_prec"
lemma show_law_char [show_law_intros]:
"show_law showsp_char x"
by (rule show_lawI) (simp add: show_law_simps)
primrec showsp_bool :: "bool showsp"
where
"showsp_bool p True = shows_string ''True''" |
"showsp_bool p False = shows_string ''False''"
lemma show_law_bool [show_law_intros]:
"show_law showsp_bool x"
by (rule show_lawI, cases x) (simp_all add: show_law_simps)
primrec pshowsp_prod :: "(shows × shows) showsp"
where
"pshowsp_prod p (x, y) = shows_string ''('' o x o shows_string '', '' o y o shows_string '')''"
definition showsp_prod :: "'a showsp ⇒ 'b showsp ⇒ ('a × 'b) showsp"
where
[code del]: "showsp_prod s1 s2 p = pshowsp_prod p o map_prod (s1 1) (s2 1)"
lemma showsp_prod_simps [simp, code]:
"showsp_prod s1 s2 p (x, y) =
shows_string ''('' o s1 1 x o shows_string '', '' o s2 1 y o shows_string '')''"
by (simp add: showsp_prod_def)
lemma show_law_prod [show_law_intros]:
"(⋀x. x ∈ Basic_BNFs.fsts y ⟹ show_law s1 x) ⟹
(⋀x. x ∈ Basic_BNFs.snds y ⟹ show_law s2 x) ⟹
show_law (showsp_prod s1 s2) y"
proof (induct y)
case (Pair x y)
note * = Pair [unfolded prod_set_simps]
show ?case
by (rule show_lawI)
(auto simp del: o_apply intro!: o_append intro: show_lawD * simp: show_law_simps)
qed
definition string_of_digit :: "nat ⇒ string"
where
"string_of_digit n =
(if n = 0 then ''0''
else if n = 1 then ''1''
else if n = 2 then ''2''
else if n = 3 then ''3''
else if n = 4 then ''4''
else if n = 5 then ''5''
else if n = 6 then ''6''
else if n = 7 then ''7''
else if n = 8 then ''8''
else ''9'')"
fun showsp_nat :: "nat showsp"
where
"showsp_nat p n =
(if n < 10 then shows_string (string_of_digit n)
else showsp_nat p (n div 10) o shows_string (string_of_digit (n mod 10)))"
declare showsp_nat.simps [simp del]
lemma show_law_nat [show_law_intros]:
"show_law showsp_nat n"
by (rule show_lawI, induct n rule: nat_less_induct) (simp add: show_law_simps showsp_nat.simps)
lemma showsp_nat_append [show_law_simps]:
"showsp_nat p n (x @ y) = showsp_nat p n x @ y"
by (intro show_lawD show_law_intros)
definition showsp_int :: "int showsp"
where
"showsp_int p i =
(if i < 0 then shows_string ''-'' o showsp_nat p (nat (- i)) else showsp_nat p (nat i))"
lemma show_law_int [show_law_intros]:
"show_law showsp_int i"
by (rule show_lawI, cases "i < 0") (simp_all add: showsp_int_def show_law_simps)
lemma showsp_int_append [show_law_simps]:
"showsp_int p i (x @ y) = showsp_int p i x @ y"
by (intro show_lawD show_law_intros)
definition showsp_rat :: "rat showsp"
where
"showsp_rat p x =
(case quotient_of x of (d, n) ⇒
if n = 1 then showsp_int p d else showsp_int p d o shows_string ''/'' o showsp_int p n)"
lemma show_law_rat [show_law_intros]:
"show_law showsp_rat r"
by (rule show_lawI, cases "quotient_of r") (simp add: showsp_rat_def show_law_simps)
lemma showsp_rat_append [show_law_simps]:
"showsp_rat p r (x @ y) = showsp_rat p r x @ y"
by (intro show_lawD show_law_intros)
text ‹
Automatic show functions are not used for @{type unit}, @{type prod}, and numbers:
for @{type unit} and @{type prod}, we do not want to display @{term "''Unity''"} and
@{term "''Pair''"}; for @{type nat}, we do not want to display
@{term "''Suc (Suc (... (Suc 0) ...))''"}; and neither @{type int}
nor @{type rat} are datatypes.
›
local_setup ‹
Show_Generator.register_foreign_partial_and_full_showsp @{type_name prod} 0
@{term "pshowsp_prod"}
@{term "showsp_prod"} (SOME @{thm showsp_prod_def})
@{term "map_prod"} (SOME @{thm prod.map_comp}) [true, true]
@{thm show_law_prod}
#> Show_Generator.register_foreign_showsp @{typ unit} @{term "showsp_unit"} @{thm show_law_unit}
#> Show_Generator.register_foreign_showsp @{typ bool} @{term "showsp_bool"} @{thm show_law_bool}
#> Show_Generator.register_foreign_showsp @{typ char} @{term "showsp_char"} @{thm show_law_char}
#> Show_Generator.register_foreign_showsp @{typ nat} @{term "showsp_nat"} @{thm show_law_nat}
#> Show_Generator.register_foreign_showsp @{typ int} @{term "showsp_int"} @{thm show_law_int}
#> Show_Generator.register_foreign_showsp @{typ rat} @{term "showsp_rat"} @{thm show_law_rat}
›
derive "show" option sum prod unit bool nat int rat
export_code
"shows_prec :: 'a::show option showsp"
"shows_prec :: ('a::show, 'b::show) sum showsp"
"shows_prec :: ('a::show × 'b::show) showsp"
"shows_prec :: unit showsp"
"shows_prec :: char showsp"
"shows_prec :: bool showsp"
"shows_prec :: nat showsp"
"shows_prec :: int showsp"
"shows_prec :: rat showsp"
checking
end