# Theory Show.Show

```(*  Title:       Show
Author:      Christian Sternagel <c.sternagel@gmail.com>
Author:      René Thiemann <rene.thiemann@uibk.ac.at>
Maintainer:  Christian Sternagel <c.sternagel@gmail.com>
Maintainer:  René Thiemann <rene.thiemann@uibk.ac.at>
*)

section ‹Converting Arbitrary Values to Readable Strings›

text ‹
A type class similar to Haskell's \texttt{Show} class, allowing for constant-time concatenation of
strings using function composition.
›

theory Show
imports
Main
Deriving.Generator_Aux
Deriving.Derive_Manager
begin

type_synonym
"shows" = "string ⇒ string"

― ‹show-functions with precedence›
type_synonym
'a showsp = "nat ⇒ 'a ⇒ shows"

subsection ‹The Show-Law›

text ‹
The "show law", @{term "shows_prec p x (r @ s) = shows_prec p x r @ s"}, states that
show-functions do not temper with or depend on output produced so far.
›

named_theorems show_law_simps ‹simplification rules for proving the "show law"›
named_theorems show_law_intros ‹introduction rules for proving the "show law"›

definition show_law :: "'a showsp ⇒ 'a ⇒ bool"
where
"show_law s x ⟷ (∀p y z. s p x (y @ z) = s p x y @ z)"

lemma show_lawI:
"(⋀p y z. s p x (y @ z) = s p x y @ z) ⟹ show_law s x"

lemma show_lawE:
"show_law s x ⟹ (s p x (y @ z) = s p x y @ z ⟹ P) ⟹ P"
by (auto simp: show_law_def)

lemma show_lawD:
"show_law s x ⟹ s p x (y @ z) = s p x y @ z"
by (blast elim: show_lawE)

class "show" =
fixes shows_prec :: "'a showsp"
and shows_list :: "'a list ⇒ shows"
assumes shows_prec_append [show_law_simps]: "shows_prec p x (r @ s) = shows_prec p x r @ s" and
shows_list_append [show_law_simps]: "shows_list xs (r @ s) = shows_list xs r @ s"
begin

abbreviation "shows x ≡ shows_prec 0 x"
abbreviation "show x ≡ shows x ''''"

end

text ‹Convert a string to a show-function that simply prepends the string unchanged.›
definition shows_string :: "string ⇒ shows"
where
"shows_string = (@)"

lemma shows_string_append [show_law_simps]:
"shows_string x (r @ s) = shows_string x r @ s"

fun shows_sep :: "('a ⇒ shows) ⇒ shows ⇒ 'a list ⇒ shows"
where
"shows_sep s sep [] = shows_string ''''" |
"shows_sep s sep [x] = s x" |
"shows_sep s sep (x#xs) = s x o sep o shows_sep s sep xs"

lemma shows_sep_append [show_law_simps]:
assumes "⋀r s. ∀x ∈ set xs. showsx x (r @ s) = showsx x r @ s"
and "⋀r s. sep (r @ s) = sep r @ s"
shows "shows_sep showsx sep xs (r @ s) = shows_sep showsx sep xs r @ s"
using assms
proof (induct xs)
case (Cons x xs) then show ?case by (cases xs) (simp_all)

lemma shows_sep_map:
"shows_sep f sep (map g xs) = shows_sep (f o g) sep xs"
by (induct xs) (simp, case_tac xs, simp_all)

definition
shows_list_gen :: "('a ⇒ shows) ⇒ string ⇒ string ⇒ string ⇒ string ⇒ 'a list ⇒ shows"
where
"shows_list_gen showsx e l s r xs =
(if xs = [] then shows_string e
else shows_string l o shows_sep showsx (shows_string s) xs o shows_string r)"

lemma shows_list_gen_append [show_law_simps]:
assumes "⋀r s. ∀x∈set xs. showsx x (r @ s) = showsx x r @ s"
shows "shows_list_gen showsx e l sep r xs (s @ t) = shows_list_gen showsx e l sep r xs s @ t"
using assms by (cases xs) (simp_all add: shows_list_gen_def show_law_simps)

lemma shows_list_gen_map:
"shows_list_gen f e l sep r (map g xs) = shows_list_gen (f o g) e l sep r xs"

definition pshowsp_list :: "nat ⇒ shows list ⇒ shows"
where
"pshowsp_list p xs = shows_list_gen id ''[]'' ''['' '', '' '']'' xs"

definition showsp_list :: "'a showsp ⇒ nat ⇒ 'a list ⇒ shows"
where
[code del]: "showsp_list s p = pshowsp_list p o map (s 0)"

lemma showsp_list_code [code]:
"showsp_list s p xs = shows_list_gen (s 0) ''[]'' ''['' '', '' '']'' xs"
by (simp add: showsp_list_def pshowsp_list_def shows_list_gen_map)

lemma show_law_list [show_law_intros]:
"(⋀x. x ∈ set xs ⟹ show_law s x) ⟹ show_law (showsp_list s) xs"
by (simp add: show_law_def showsp_list_code show_law_simps)

lemma showsp_list_append [show_law_simps]:
"(⋀p y z. ∀x ∈ set xs. s p x (y @ z) = s p x y @ z) ⟹
showsp_list s p xs (y @ z) = showsp_list s p xs y @ z"
by (simp add: show_law_simps showsp_list_def pshowsp_list_def)

subsection ‹Show-Functions for Characters and Strings›

instantiation char :: "show"
begin

definition "shows_prec p (c::char) = (#) c"
definition "shows_list (cs::string) = shows_string cs"
instance
by standard (simp_all add: shows_prec_char_def shows_list_char_def show_law_simps)

end

definition "shows_nl = shows (CHR ''⏎'')"
definition "shows_space = shows (CHR '' '')"
definition "shows_paren s = shows (CHR ''('') o s o shows (CHR '')'')"
definition "shows_quote s = shows (CHR 0x27) o s o shows (CHR 0x27)"
abbreviation "apply_if b s ≡ (if b then s else id)" ― ‹conditional function application›
text ‹Parenthesize only if precedence is greater than @{term "0::nat"}.›
definition "shows_pl (p::nat) = apply_if (p > 0) (shows (CHR ''(''))"
definition "shows_pr (p::nat) = apply_if (p > 0) (shows (CHR '')''))"

lemma
shows_nl_append [show_law_simps]: "shows_nl (x @ y) = shows_nl x @ y" and
shows_space_append [show_law_simps]: "shows_space (x @ y) = shows_space x @ y" and
shows_paren_append [show_law_simps]:
"(⋀x y. s (x @ y) = s x @ y) ⟹ shows_paren s (x @ y) = shows_paren s x @ y" and
shows_quote_append [show_law_simps]:
"(⋀x y. s (x @ y) = s x @ y) ⟹ shows_quote s (x @ y) = shows_quote s x @ y" and
shows_pl_append [show_law_simps]: "shows_pl p (x @ y) = shows_pl p x @ y" and
shows_pr_append [show_law_simps]: "shows_pr p (x @ y) = shows_pr p x @ y"
by (simp_all add: shows_nl_def shows_space_def shows_paren_def shows_quote_def shows_pl_def shows_pr_def show_law_simps)

lemma o_append:
"(⋀x y. f (x @ y) = f x @ y) ⟹ g (x @ y) = g x @ y ⟹ (f o g) (x @ y) = (f o g) x @ y"
by simp

ML_file ‹show_generator.ML›

local_setup ‹
Show_Generator.register_foreign_partial_and_full_showsp @{type_name "list"} 0
@{term "pshowsp_list"}
@{term "showsp_list"} (SOME @{thm showsp_list_def})
@{term "map"} (SOME @{thm list.map_comp}) [true] @{thm show_law_list}
›

instantiation list :: ("show") "show"
begin

definition "shows_prec (p :: nat) (xs :: 'a list) = shows_list xs"
definition "shows_list (xss :: 'a list list) = showsp_list shows_prec 0 xss"

instance
by standard (simp_all add: show_law_simps shows_prec_list_def shows_list_list_def)

end

definition shows_lines :: "'a::show list ⇒ shows"
where
"shows_lines = shows_sep shows shows_nl"

definition shows_many :: "'a::show list ⇒ shows"
where
"shows_many = shows_sep shows id"

definition shows_words :: "'a::show list ⇒ shows"
where
"shows_words = shows_sep shows shows_space"

lemma shows_lines_append [show_law_simps]:
"shows_lines xs (r @ s) = shows_lines xs r @ s"

lemma shows_many_append [show_law_simps]:
"shows_many xs (r @ s) = shows_many xs r @ s"

lemma shows_words_append [show_law_simps]:
"shows_words xs (r @ s) = shows_words xs r @ s"

lemma shows_foldr_append [show_law_simps]:
assumes "⋀r s. ∀x ∈ set xs. showx x (r @ s) = showx x r @ s"
shows "foldr showx xs (r @ s) = foldr showx xs r @ s"
using assms by (induct xs) (simp_all)

lemma shows_sep_cong [fundef_cong]:
assumes "xs = ys" and "⋀x. x ∈ set ys ⟹ f x = g x"
shows "shows_sep f sep xs = shows_sep g sep ys"
using assms
proof (induct ys arbitrary: xs)
case (Cons y ys)
then show ?case by (cases ys) simp_all
qed simp

lemma shows_list_gen_cong [fundef_cong]:
assumes "xs = ys" and "⋀x. x ∈ set ys ⟹ f x = g x"
shows "shows_list_gen f e l sep r xs = shows_list_gen g e l sep r ys"
using shows_sep_cong [of xs ys f g] assms by (cases xs) (auto simp: shows_list_gen_def)

lemma showsp_list_cong [fundef_cong]:
"xs = ys ⟹ p = q ⟹
(⋀p x. x ∈ set ys ⟹ f p x = g p x) ⟹ showsp_list f p xs = showsp_list g q ys"
by (simp add: showsp_list_code cong: shows_list_gen_cong)

abbreviation (input) shows_cons :: "string ⇒ shows ⇒ shows" (infixr "+#+" 10)
where
"s +#+ p ≡ shows_string s ∘ p"

abbreviation (input) shows_append :: "shows ⇒ shows ⇒ shows" (infixr "+@+" 10)
where
"s +@+ p ≡ s ∘ p"

instantiation String.literal :: "show"
begin

definition shows_prec_literal :: "nat ⇒ String.literal ⇒ string ⇒ string"
where "shows_prec p s = shows_string (String.explode s)"

definition shows_list_literal :: "String.literal list ⇒ string ⇒ string"
where "shows_list ss = shows_string (concat (map String.explode ss))"

lemma shows_list_literal_code [code]:
"shows_list = foldr (λs. shows_string (String.explode s))"
proof
fix ss
show "shows_list ss = foldr (λs. shows_string (String.explode s)) ss"
by (induct ss) (simp_all add: shows_list_literal_def shows_string_def)
qed

instance by standard