Theory Old_Show_Generator

(*
Copyright 2009-2014 Christian Sternagel, René Thiemann

This file is part of IsaFoR/CeTA.

IsaFoR/CeTA is free software: you can redistribute it and/or modify it under the
terms of the GNU Lesser General Public License as published by the Free Software
Foundation, either version 3 of the License, or (at your option) any later
version.

IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE.  See the GNU Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public License along
with IsaFoR/CeTA. If not, see <http://www.gnu.org/licenses/>.
*)

section ‹Generating Show-Functions for Data Types›

theory Old_Show_Generator
imports
  Datatype_Order_Generator.Derive_Aux
  Old_Show
begin

subsection ‹Introduction›

text ‹
  The show-generator registers itself at the derive-manager for the class @{class show}. To be more
  precise, it automatically generates the functions @{const shows_prec} and @{const shows_list} for
  some data type ‹dtyp› and proves the following instantiation.
  \begin{itemize}
  \item ‹instantiation dtyp :: (show, ..., show) show›
  \end{itemize}
  All the non-recursive types that are used in the data type must have a similar instantiation. For
  recursive type-dependencies this is automatically generated.

  For example, for the data type ‹datatype tree = Leaf nat | Node (tree list)› we require
  that ‹nat› is already in @{class show}, whereas for type @{typ "'a list"} nothing is
  required, since it is used recursively.

  However, if we define ‹datatype tree = Leaf (nat list) | Node tree tree› then also
  @{typ "'a list"} must provide a @{class show} instance.
›

subsection ‹Implementation Notes›

text ‹
  The generator uses the recursors from the data type package to define the show function.
  Constructors are displayed by their short names and arguments are separated by blanks and
  surrounded by parenthesis.

  The associativity is proven using the induction theorem from the data type package.
›

subsection ‹Features and Limitations›

text ‹
  The show-generator has been developed mainly for data types without explicit mutual recursion. For
  mutual recursive data types -- like ‹datatype a = C b and b = D a a› -- only for the first
  mentioned data type -- here ‹a› -- instantiations of the @{class show} are derived.

  Indirect recursion like in ‹datatype tree = Leaf nat | Node (tree list)› should work
  without problems.
›

subsection ‹Installing the Generator›

definition shows_sep_paren :: "shows ⇒ shows"
where
  "shows_sep_paren s = ('' ('' +#+ s +@+ shows '')'')"

text ‹
  The four crucial properties which are used to ensure associativity.
›
lemma append_assoc_trans:
  assumes "⋀r s. b r @ s = b (r @ s)"
  shows "((@) a +@+ b) r @ s = ((@) a +@+ b) (r @ s)"
  using assms by simp

lemma shows_sep_paren:
  assumes "⋀r s. a r @ s = a (r @ s)"
    and "⋀r s. b r @ s = b (r @ s)"
  shows "(shows_sep_paren a +@+ b) r @ s = (shows_sep_paren a +@+ b) (r @ s)"
  unfolding shows_sep_paren_def by (simp add: assms)

lemma shows_sep_paren_final:
  assumes "⋀r s. a r @ s = a (r @ s)"
  shows "(shows_sep_paren a) r @ s = (shows_sep_paren a) (r @ s)"
  unfolding shows_sep_paren_def by (simp add: assms)

ML_file ‹old_show_generator.ML›

end