Session Show

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"
  by (simp add: show_law_def)

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"
  by (simp add: shows_string_def)

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)
qed (simp add: show_law_simps)

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. xset 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"
  by (simp_all add: shows_list_gen_def shows_sep_map)

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"
  by (simp add: shows_lines_def show_law_simps)

lemma shows_many_append [show_law_simps]:
  "shows_many xs (r @ s) = shows_many xs r @ s"
  by (simp add: shows_many_def show_law_simps)

lemma shows_words_append [show_law_simps]:
  "shows_words xs (r @ s) = shows_words xs r @ s"
  by (simp add: shows_words_def show_law_simps)

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
  (simp_all add: shows_prec_literal_def shows_list_literal_def shows_string_def)

end

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

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 =>
    add_info tyco
      {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
      |> Generator_Aux.define_overloaded_generic
        ((Binding.name ("shows_prec_" ^ name ^ "_def"), @{attributes [code]}), shows_prec_def)
      ||>> Generator_Aux.define_overloaded_generic
        ((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]
        THEN REPEAT1 (HEADGOAL show_append_tac)
     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 '')''"
  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

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 
    License:     LPGL
*)
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 
    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
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 
    License:     LGPL
*)
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 
    License:     LGPL
*)

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}.›
overloading show_real  show_real
begin
  definition show_real
    where "show_real x 
      (if ( y. x = Ratreal y) then show (THE y. x = Ratreal y) else ''Irrational'')"
end

lemma show_real_code[code]: "show_real (Ratreal x) = show x"
  unfolding show_real_def by auto

end