# Theory 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

end

text ‹
Don't use Haskell's existing "Show" class for code-generation, since it is not compatible to the
formalized class.
›

end


# File ‹show_generator.ML›

(*  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>

Generate/register show functions for arbitrary types.

Precedence is used to determine parenthesization of subexpressions. In the automatically generated
functions 0 means "no parentheses" and 1 means "parenthesize".
*)

signature SHOW_GENERATOR =
sig

(*generate show functions for the given datatype*)
val generate_showsp : string -> local_theory -> local_theory

val register_foreign_partial_and_full_showsp :
string ->     (*type name*)
int ->        (*default precedence for type parameters*)
term ->       (*partial show function*)
term ->       (*show function*)
thm option -> (*definition of show function via partial show function*)
term ->       (*map function*)
thm option -> (*compositionality theorem of map function*)
bool list ->  (*indicate which positions of type parameters are used*)
thm ->        (*show law intro rule*)
local_theory -> local_theory

(*for type constants (i.e., nullary type constructors) partial and full show functions
coincide and no other information is necessary.*)
val register_foreign_showsp : typ -> term -> thm -> local_theory -> local_theory

(*automatically derive a "show" class instance for the given datatype*)
val show_instance : string -> theory -> theory

end

structure Show_Generator : SHOW_GENERATOR =
struct

open Generator_Aux

val mk_prec = HOLogic.mk_number @{typ nat}
val prec0 = mk_prec 0
val prec1 = mk_prec 1
val showS = @{sort "show"}
val showsT = @{typ "shows"}
fun showspT T = @{typ nat} --> T --> showsT
val showsify_typ = map_atyps (K showsT)
val showsify = map_types showsify_typ
fun show_law_const T = Const (@{const_name show_law}, showspT T --> T --> HOLogic.boolT)
fun shows_prec_const T = Const (@{const_name shows_prec}, showspT T)
fun shows_list_const T = Const (@{const_name shows_list}, HOLogic.listT T --> showsT)
fun showsp_list_const T = Const (@{const_name showsp_list}, showspT T --> showspT (HOLogic.listT T))
val dest_showspT = binder_types #> tl #> hd

type info =
{prec : int,
pshowsp : term,
showsp : term,
show_def : thm option,
map : term,
map_comp : thm option,
used_positions : bool list,
show_law_intro : thm}

structure Data = Generic_Data
(type T = info Symtab.table
val empty = Symtab.empty
val extend = I
val merge = Symtab.merge (fn (info1, info2) => #pshowsp info1 = #pshowsp info2))

fun add_info tyco info = Data.map (Symtab.update_new (tyco, info))
val get_info = Context.Proof #> Data.get #> Symtab.lookup

fun the_info ctxt tyco =
(case get_info ctxt tyco of
SOME info => info
| NONE => error ("no show function available for type " ^ quote tyco))

fun declare_info tyco p pshow show show_def m m_comp used_pos law_thm =
Local_Theory.declaration {syntax = false, pervasive = false} (fn phi =>
{prec = p,
pshowsp = Morphism.term phi pshow,
showsp = Morphism.term phi show,
show_def = Option.map (Morphism.thm phi) show_def,
map = Morphism.term phi m,
map_comp = Option.map (Morphism.thm phi) m_comp,
used_positions = used_pos,
show_law_intro = Morphism.thm phi law_thm})

val register_foreign_partial_and_full_showsp = declare_info

fun register_foreign_showsp T show =
let val tyco = (case T of Type (tyco, []) => tyco | _ => error "expected type constant")
in register_foreign_partial_and_full_showsp tyco 0 show show NONE (HOLogic.id_const T) NONE [] end

fun shows_string c =
@{const "shows_string"} $HOLogic.mk_string (Long_Name.base_name c) fun mk_shows_parens _ [t] = t | mk_shows_parens p ts = Library.foldl1 HOLogic.mk_comp (@{const shows_pl}$ p :: separate @{const shows_space} ts @ [@{const shows_pr} $p]) fun simp_only_tac ctxt ths = CHANGED o full_simp_tac (clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths) fun generate_showsp tyco lthy = let val (tycos, Ts) = mutual_recursive_types tyco lthy val _ = map (fn tyco => "generating show function for type " ^ quote tyco) tycos |> cat_lines |> writeln val maps = Bnf_Access.map_terms lthy tycos val map_simps = Bnf_Access.map_simps lthy tycos val map_comps = Bnf_Access.map_comps lthy tycos val (tfrees, used_tfrees) = type_parameters (hd Ts) lthy val used_positions = map (member (op =) used_tfrees o TFree) tfrees val ss = map (subT "show") used_tfrees val show_Ts = map showspT used_tfrees val arg_shows = map Free (ss ~~ show_Ts) val dep_tycos = fold (add_used_tycos lthy) tycos [] fun mk_pshowsp (tyco, T) = ("pshowsp_" ^ Long_Name.base_name tyco, showspT T |> showsify_typ) fun default_show T = absdummy T (mk_id @{typ string}) fun constr_terms lthy = Bnf_Access.constr_terms lthy #> map (apsnd (fst o strip_type) o dest_Const) (* primrec definitions of partial show functions *) fun generate_pshow_eqs lthy (tyco, T) = let val constrs = constr_terms lthy tyco |> map (fn (c, Ts) => let val Ts' = map showsify_typ Ts in (Const (c, Ts' ---> T) |> showsify, Ts') end) fun shows_arg (x, T) = let val m = Generator_Aux.create_map default_show (fn (tyco, T) => fn p => Free (mk_pshowsp (tyco, T))$ p) prec1
(equal @{typ "shows"})
(#used_positions oo the_info) (#map oo the_info)
(curry (op $) o #pshowsp oo the_info) tycos (mk_prec o #prec oo the_info) T lthy val pshow = Generator_Aux.create_partial prec1 (equal @{typ "shows"}) (#used_positions oo the_info) (#map oo the_info) (curry (op$) o #pshowsp oo the_info)
tycos (mk_prec o #prec oo the_info) T lthy
in pshow $(m$ Free (x, T)) |> infer_type lthy end

fun generate_eq lthy (c, arg_Ts) =
let
val (p, xs) = Name.variant "p" (Variable.names_of lthy) |>> Free o rpair @{typ nat}
||> (fn ctxt => Name.invent_names ctxt "x" arg_Ts)
val lhs = Free (mk_pshowsp (tyco, T)) $p$ list_comb (c, map Free xs)
val rhs = shows_string (dest_Const c |> fst) :: map shows_arg xs
|> mk_shows_parens p
in HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) end
in map (generate_eq lthy) constrs end

val eqs = map (generate_pshow_eqs lthy) (tycos ~~ Ts) |> flat
val bindings = tycos ~~ Ts |> map mk_pshowsp
|> map (fn (name, T) => (Binding.name name, T |> showsify_typ |> SOME, NoSyn))

val ((pshows, pshow_simps), lthy) =
lthy
|> Local_Theory.begin_nested
|> snd
|> BNF_LFP_Rec_Sugar.primrec false [] bindings
(map (fn t => ((Binding.empty_atts, t), [], [])) eqs)
|> Local_Theory.end_nested_result
(fn phi => fn (pshows, _, pshow_simps) => (map (Morphism.term phi) pshows, map (Morphism.fact phi) pshow_simps))

(* definitions of show functions via partial show functions and map *)

fun generate_show_defs tyco lthy =
let
val ss = map (subT "show") used_tfrees
val arg_Ts = map showspT used_tfrees
val arg_shows = map Free (ss ~~ arg_Ts)
val p = Name.invent (Variable.names_of lthy) "p" 1 |> the_single |> Free o rpair @{typ nat}
val (pshow, m) = AList.lookup (op =) (tycos ~~ (pshows ~~ maps)) tyco |> the
val ts = tfrees |> map TFree |> map (fn T =>
AList.lookup (op =) (used_tfrees ~~ map (fn x => x $prec1) arg_shows) T |> the_default (default_show T)) val args = arg_shows @ [p] val rhs = HOLogic.mk_comp (pshow$ p, list_comb (m, ts)) |> infer_type lthy
val abs_def = fold_rev lambda args rhs
val name = "showsp_" ^ Long_Name.base_name tyco
val ((showsp, (_, prethm)), lthy) =
Local_Theory.define ((Binding.name name, NoSyn), (Binding.empty_atts, abs_def)) lthy
val eq = Logic.mk_equals (list_comb (showsp, args), rhs)
val thm = Goal.prove_future lthy (map (fst o dest_Free) args) [] eq (K (unfold_tac lthy [prethm]))
in
Local_Theory.note ((Binding.name (name ^ "_def"), []), [thm]) lthy
|>> the_single o snd
|>> (K showsp)
end

val ((shows, show_defs), lthy) =
lthy
|> Local_Theory.begin_nested
|> snd
|> fold_map generate_show_defs tycos
|>> split_list
|> Local_Theory.end_nested_result
(fn phi => fn (shows, show_defs) => (map (Morphism.term phi) shows, map (Morphism.thm phi) show_defs))

(* alternative simp-rules for show functions *)

fun generate_show_simps (tyco, T) lthy =
let
val constrs = constr_terms lthy tyco |> map (apsnd (map freeify_tvars))
|> map (fn (c, Ts) => (Const (c, Ts ---> T), Ts))

fun shows_arg (x, T) =
let
fun create_show (T as TFree _) = AList.lookup (op =) (used_tfrees ~~ arg_shows) T |> the
| create_show (Type (tyco, Ts)) =
(case AList.lookup (op =) (tycos ~~ shows) tyco of
SOME show_const => list_comb (show_const, arg_shows)
| NONE =>
let
val {showsp = s, used_positions = up, ...} = the_info lthy tyco
val ts = (up ~~ Ts) |> map_filter (fn (b, T) =>
if b then SOME (create_show T) else NONE)
in list_comb (s, ts) end)
| create_show T =
error ("unexpected schematic variable " ^ quote (Syntax.string_of_typ lthy T))

val show = create_show T |> infer_type lthy
in show $prec1$ Free (x, T) end

fun generate_eq_thm lthy (c, arg_Ts) =
let
val (p, xs) = Name.variant "p" (Variable.names_of lthy) |>> Free o rpair @{typ nat}
||> (fn ctxt => Name.invent_names ctxt "x" arg_Ts)
val show_const = AList.lookup (op =) (tycos ~~ shows) tyco |> the
val lhs = list_comb (show_const, arg_shows) $p$ list_comb (c, map Free xs)
val rhs = shows_string (dest_Const c |> fst) :: map shows_arg xs
|> mk_shows_parens p
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |> infer_type lthy
val dep_show_defs = map_filter (#show_def o the_info lthy) dep_tycos
val dep_map_comps = map_filter (#map_comp o the_info lthy) dep_tycos
val thm = Goal.prove_future lthy (fst (dest_Free p) :: map fst xs @ ss) [] eq
(fn {context = ctxt, ...} => unfold_tac ctxt
(@{thms id_def o_def} @
flat pshow_simps @
dep_map_comps @ show_defs @ dep_show_defs @ flat map_simps))
in thm end

val thms = map (generate_eq_thm lthy) constrs
val name = "showsp_" ^ Long_Name.base_name tyco
in
lthy
|> Local_Theory.note ((Binding.name (name ^ "_simps"), @{attributes [simp, code]}), thms)
|> apfst snd
end

val (show_simps, lthy) =
lthy
|> Local_Theory.begin_nested
|> snd
|> fold_map generate_show_simps (tycos ~~ Ts)
|> Local_Theory.end_nested_result
(fn phi => map (Morphism.fact phi))

(* show law theorems *)

val induct_thms = Bnf_Access.induct_thms lthy tycos
val set_simps = Bnf_Access.set_simps lthy tycos
val sets = Bnf_Access.set_terms lthy tycos

fun generate_show_law_thms (tyco, x) =
let
val sets = AList.lookup (op =) (tycos ~~ sets) tyco |> the
val used_sets = map (the o AList.lookup (op =) (map TFree tfrees ~~ sets)) used_tfrees
fun mk_prem ((show, set), T) =
let
(*val y = singleton (Name.variant_list [fst x]) "y" |> Free o rpair T*)
val y = Free (subT "x" T, T)
val lhs = HOLogic.mk_mem (y, set $Free x) |> HOLogic.mk_Trueprop val rhs = show_law_const T$ show $y |> HOLogic.mk_Trueprop in Logic.all y (Logic.mk_implies (lhs, rhs)) end val prems = map mk_prem (arg_shows ~~ used_sets ~~ used_tfrees) val (show_const, T) = AList.lookup (op =) (tycos ~~ (shows ~~ Ts)) tyco |> the val concl = show_law_const T$ list_comb (show_const, arg_shows) $Free x |> HOLogic.mk_Trueprop in Logic.list_implies (prems, concl) |> infer_type lthy end val xs = Name.invent_names (Variable.names_of lthy) "x" Ts val show_law_prethms = map generate_show_law_thms (tycos ~~ xs) val rec_info = (the_info lthy, #used_positions, tycos) val split_IHs = split_IHs rec_info val recursor_tac = std_recursor_tac rec_info used_tfrees #show_law_intro fun show_law_tac ctxt xs = let val constr_Ts = tycos |> map (#ctrXs_Tss o #fp_ctr_sugar o the o BNF_FP_Def_Sugar.fp_sugar_of ctxt) val ind_case_to_idxs = let fun number n (i, j) ((_ :: xs) :: ys) = (n, (i, j)) :: number (n + 1) (i, j + 1) (xs :: ys) | number n (i, _) ([] :: ys) = number n (i + 1, 0) ys | number _ _ [] = [] in AList.lookup (op =) (number 0 (0, 0) constr_Ts) #> the end fun instantiate_IHs IHs assms = map (fn IH => OF_option IH (replicate (Thm.nprems_of IH - length assms) NONE @ map SOME assms)) IHs fun induct_tac ctxt f = (DETERM o Induction.induction_tac ctxt false (map (fn x => [SOME (NONE, (x, false))]) xs) [] [] (SOME induct_thms) []) THEN_ALL_NEW (fn st => Subgoal.SUBPROOF (fn {context = ctxt, prems, params, ...} => f ctxt (st - 1) prems params) ctxt st) (*do not use full "show_law_simps" here, since otherwise too many subgoals might be solved (so that the number of subgoals does no longer match the number of IHs)*) val show_law_simps_less = @{thms shows_string_append shows_pl_append shows_pr_append shows_space_append} fun o_append_intro_tac ctxt f = HEADGOAL ( K (Method.try_intros_tac ctxt @{thms o_append} []) THEN_ALL_NEW K (unfold_tac ctxt show_law_simps_less) THEN_ALL_NEW (fn i => Subgoal.SUBPROOF (fn {context = ctxt', ...} => f (i - 1) ctxt') ctxt i)) fun solve_tac ctxt case_num prems params = let val (i, _) = ind_case_to_idxs case_num (*(constructor number, argument number)*) val k = length prems - length used_tfrees val (IHs, assms) = chop k prems in resolve_tac ctxt @{thms show_lawI} 1 THEN Subgoal.FOCUS (fn {context = ctxt, ...} => let val assms = map (Local_Defs.unfold ctxt (nth set_simps i)) assms val Ts = map (fastype_of o Thm.term_of o snd) params val IHs = instantiate_IHs IHs assms |> split_IHs Ts in unfold_tac ctxt (nth show_simps i) THEN o_append_intro_tac ctxt (fn i => fn ctxt' => resolve_tac ctxt' @{thms show_lawD} 1 THEN recursor_tac assms (nth Ts i) (nth IHs i) ctxt') end) ctxt 1 end in induct_tac ctxt solve_tac end val show_law_thms = prove_multi_future lthy (map fst xs @ ss) [] show_law_prethms (fn {context = ctxt, ...} => HEADGOAL (show_law_tac ctxt (map Free xs))) val (show_law_thms, lthy) = lthy |> Local_Theory.begin_nested |> snd |> fold_map (fn (tyco, thm) => Local_Theory.note ((Binding.name ("show_law_" ^ Long_Name.base_name tyco), @{attributes [show_law_intros]}), [thm]) #> apfst (the_single o snd)) (tycos ~~ show_law_thms) |> Local_Theory.end_nested_result Morphism.fact in lthy |> fold (fn ((((((tyco, pshow), show), show_def), m), m_comp), law_thm) => declare_info tyco 1 pshow show (SOME show_def) m (SOME m_comp) used_positions law_thm) (tycos ~~ pshows ~~ shows ~~ show_defs ~~ maps ~~ map_comps ~~ show_law_thms) end fun ensure_info tyco lthy = (case get_info lthy tyco of SOME _ => lthy | NONE => generate_showsp tyco lthy) (* proving show instances *) fun dest_showsp showsp = dest_Const showsp ||> ( binder_types #> chop_prefix (fn T => T <> @{typ nat}) #>> map (freeify_tvars o dest_showspT) ##> map (dest_TFree o freeify_tvars) o snd o dest_Type o hd o tl) fun show_instance tyco thy = let val _ = Sorts.has_instance (Sign.classes_of thy) tyco showS andalso error ("type " ^ quote tyco ^ " is already an instance of class \"show\"") val _ = writeln ("deriving \"show\" instance for type " ^ quote tyco) val thy = Named_Target.theory_map (ensure_info tyco) thy val lthy = Named_Target.theory_init thy val {showsp, ...} = the_info lthy tyco val (showspN, (used_tfrees, tfrees)) = dest_showsp showsp val tfrees' = tfrees |> map (fn (x, S) => if member (op =) used_tfrees (TFree (x, S)) then (x, showS) else (x, S)) val used_tfrees' = map (dest_TFree #> fst #> rpair showS #> TFree) used_tfrees val T = Type (tyco, map TFree tfrees') val arg_Ts = map showspT used_tfrees' val showsp' = Const (showspN, arg_Ts ---> showspT T) val shows_prec_def = Logic.mk_equals (shows_prec_const T, list_comb (showsp', map shows_prec_const used_tfrees')) val shows_list_def = Logic.mk_equals (shows_list_const T, showsp_list_const T$ shows_prec_const T \$ prec0)
val name = Long_Name.base_name tyco
val ((shows_prec_thm, shows_list_thm), lthy) =
Class.instantiation ([tyco], tfrees', showS) thy
((Binding.name ("shows_prec_" ^ name ^ "_def"), @{attributes [code]}), shows_prec_def)
((Binding.name ("shows_list_" ^ name ^ "_def"), @{attributes [code]}), shows_list_def)
in
Class.prove_instantiation_exit (fn ctxt =>
let
val show_law_intros = Named_Theorems.get ctxt @{named_theorems "show_law_intros"}
val show_law_simps = Named_Theorems.get ctxt @{named_theorems "show_law_simps"}
val show_append_tac = resolve_tac ctxt @{thms show_lawD}
THEN' REPEAT_ALL_NEW (resolve_tac ctxt show_law_intros)
THEN_ALL_NEW (
resolve_tac ctxt @{thms show_lawI}
THEN' simp_only_tac ctxt show_law_simps)
in
Class.intro_classes_tac ctxt []
THEN unfold_tac ctxt [shows_prec_thm, shows_list_thm]
end) lthy
end

val _ =
Theory.setup
(Derive_Manager.register_derive "show" "generate show instance" (K o show_instance))

end


# Theory Show_Instances

(*  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 ‹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 '')''"

(*NOTE: in order to be compatible with automatically generated show funtions,
show-arguments of "map"-functions need to get precedence 1 (which may lead to
redundant parentheses in the output, but seems unavoidable in the current setup,
i.e., pshowsp via primrec followed by defining showsp via pshowsp composed with map).*)
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 '')''"

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

fun 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



# Theory Show_Poly

(*
Author:      René Thiemann
*)
subsection ‹Displaying Polynomials›

text ‹We define a method which converts polynomials to strings and registers it in the Show class.›

theory Show_Poly
imports
Show_Instances
"HOL-Computational_Algebra.Polynomial"
begin

fun show_factor :: "nat ⇒ string" where
"show_factor 0 = []"
| "show_factor (Suc 0) = ''x''"
| "show_factor n = ''x^'' @ show n"

fun show_coeff_factor where
"show_coeff_factor c n = (if n = 0 then show c else if c = 1 then show_factor n else show c @ show_factor n)"

fun show_poly_main :: "nat ⇒ 'a :: {zero,one,show} list ⇒ string" where
"show_poly_main _ [] = ''0''"
| "show_poly_main n [c] = show_coeff_factor c n"
| "show_poly_main n (c # cs) = (if c = 0 then show_poly_main (Suc n) cs else
show_coeff_factor c n @ '' + '' @ show_poly_main (Suc n) cs)"

definition show_poly :: "'a :: {zero,one,show}poly ⇒ string" where
"show_poly p = show_poly_main 0 (coeffs p)"

definition showsp_poly :: "'a :: {zero,one,show}poly showsp"
where
"showsp_poly p x = shows_string (show_poly x)"

instantiation poly :: ("{show,one,zero}") "show"
begin

definition "shows_prec p (x :: 'a poly) = showsp_poly p x"
definition "shows_list (ps :: 'a poly list) = showsp_list shows_prec 0 ps"

lemma show_law_poly [show_law_simps]:
"shows_prec p (a :: 'a poly) (r @ s) = shows_prec p a r @ s"
by (simp add: shows_prec_poly_def showsp_poly_def show_law_simps)

instance by standard (auto simp: shows_list_poly_def show_law_simps)

end

end


# Theory Show_Real

(*
Author:      René Thiemann
*)
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
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
end


# Theory Show_Complex

(*
Author:      René Thiemann
*)
section ‹Show for Complex Numbers›

text ‹We print complex numbers as real and imaginary parts. Note that by transitivity, this theory
demands that an implementations for \textit{show-real} is available, e.g., by using
one of the theories \textit{Show-Real-Impl} or \textit{../Algebraic-Numbers/Show-Real-...}.›
theory Show_Complex
imports
HOL.Complex
Show_Real
begin

definition "show_complex x = (
let r = Re x; i = Im x in
if (i = 0) then show_real r else if
r = 0 then show_real i @ ''i'' else
''('' @ show_real r @ ''+'' @ show_real i @ ''i)'')"

definition showsp_complex :: "complex showsp"
where
"showsp_complex p x y =
(show_complex x @ y)"

lemma show_law_complex [show_law_intros]:
"show_law showsp_complex r"
by (rule show_lawI) (simp add: showsp_complex_def show_law_simps)

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

local_setup ‹
Show_Generator.register_foreign_showsp @{typ complex} @{term "showsp_complex"} @{thm show_law_complex}
›

derive "show" complex
end


# Theory Show_Real_Impl

(*
Author:      René Thiemann
*)

section ‹Show Implemetation for Real Numbers via Rational Numbers›

text ‹We just provide an implementation for show of real numbers where we assume
that real numbers are implemented via rational numbers.›

theory Show_Real_Impl
imports
Show_Real
Show_Instances
begin

text ‹We now define @{const show_real}.›
`