src/Doc/Datatypes/Datatypes.thy

document 'set_transfer'

(*  Title:      Doc/Datatypes/Datatypes.thy
    Author:     Jasmin Blanchette, TU Muenchen
    Author:     Martin Desharnais, Ecole de technologie superieure
    Author:     Lorenz Panny, TU Muenchen
    Author:     Andrei Popescu, TU Muenchen
    Author:     Dmitriy Traytel, TU Muenchen

Tutorial for (co)datatype definitions with the new package.
*)

theory Datatypes
imports
  Setup
  "~~/src/HOL/Library/BNF_Axiomatization"
  "~~/src/HOL/Library/Cardinal_Notations"
  "~~/src/HOL/Library/FSet"
  "~~/src/HOL/Library/Simps_Case_Conv"
begin

section {* Introduction
  \label{sec:introduction} *}

text {*
The 2013 edition of Isabelle introduced a new definitional package for freely
generated datatypes and codatatypes. The datatype support is similar to that
provided by the earlier package due to Berghofer and Wenzel
\cite{Berghofer-Wenzel:1999:TPHOL}, documented in the Isar reference manual
\cite{isabelle-isar-ref}; indeed, replacing the keyword \keyw{datatype} by
@{command datatype_new} is usually all that is needed to port existing theories
to use the new package.

Perhaps the main advantage of the new package is that it supports recursion
through a large class of non-datatypes, such as finite sets:
*}

    datatype_new 'a tree\<^sub>f\<^sub>s = Node\<^sub>f\<^sub>s (lbl\<^sub>f\<^sub>s: 'a) (sub\<^sub>f\<^sub>s: "'a tree\<^sub>f\<^sub>s fset")

text {*
\noindent
Another strong point is the support for local definitions:
*}

    context linorder
    begin
    datatype_new flag = Less | Eq | Greater
    end

text {*
\noindent
Furthermore, the package provides a lot of convenience, including automatically
generated discriminators, selectors, and relators as well as a wealth of
properties about them.

In addition to inductive datatypes, the new package supports coinductive
datatypes, or \emph{codatatypes}, which allow infinite values. For example, the
following command introduces the type of lazy lists, which comprises both finite
and infinite values:
*}

(*<*)
    locale early
    locale late
(*>*)
    codatatype (*<*)(in early) (*>*)'a llist = LNil | LCons 'a "'a llist"

text {*
\noindent
Mixed inductive--coinductive recursion is possible via nesting. Compare the
following four Rose tree examples:
*}

    datatype_new (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
    datatype_new (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
    codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>f = Node\<^sub>i\<^sub>f 'a "'a tree\<^sub>i\<^sub>f list"
    codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i 'a "'a tree\<^sub>i\<^sub>i llist"

text {*
The first two tree types allow only paths of finite length, whereas the last two
allow infinite paths. Orthogonally, the nodes in the first and third types have
finitely many direct subtrees, whereas those of the second and fourth may have
infinite branching.

The package is part of @{theory Main}. Additional functionality is provided by
the theory @{theory BNF_Axiomatization}, located in the directory
\verb|~~/src/HOL/Library|.

The package, like its predecessor, fully adheres to the LCF philosophy
\cite{mgordon79}: The characteristic theorems associated with the specified
(co)datatypes are derived rather than introduced axiomatically.%
\footnote{However, some of the
internal constructions and most of the internal proof obligations are skipped
if the @{text quick_and_dirty} option is enabled.}
The package is described in a number of papers
\cite{traytel-et-al-2012,blanchette-et-al-wit,blanchette-et-al-2014-impl,panny-et-al-2014}.
The central notion is that of a \emph{bounded natural functor} (BNF)---a
well-behaved type constructor for which nested (co)recursion is supported.

This tutorial is organized as follows:

\begin{itemize}
\setlength{\itemsep}{0pt}

\item Section \ref{sec:defining-datatypes}, ``Defining Datatypes,''
describes how to specify datatypes using the @{command datatype_new} command.

\item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive
Functions,'' describes how to specify recursive functions using
@{command primrec}.

\item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
describes how to specify codatatypes using the @{command codatatype} command.

\item Section \ref{sec:defining-corecursive-functions}, ``Defining Corecursive
Functions,'' describes how to specify corecursive functions using the
@{command primcorec} and @{command primcorecursive} commands.

\item Section \ref{sec:introducing-bounded-natural-functors}, ``Introducing
Bounded Natural Functors,'' explains how to use the @{command bnf} command
to register arbitrary type constructors as BNFs.

\item Section
\ref{sec:deriving-destructors-and-theorems-for-free-constructors},
``Deriving Destructors and Theorems for Free Constructors,'' explains how to
use the command @{command free_constructors} to derive destructor constants
and theorems for freely generated types, as performed internally by @{command
datatype_new} and @{command codatatype}.

%\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,''
%describes the package's programmatic interface.

%\item Section \ref{sec:interoperability}, ``Interoperability,''
%is concerned with the packages' interaction with other Isabelle packages and
%tools, such as the code generator and the counterexample generators.

%\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and
%Limitations,'' concludes with known open issues at the time of writing.
\end{itemize}


\newbox\boxA
\setbox\boxA=\hbox{\texttt{NOSPAM}}

\newcommand\authoremaili{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak
in.\allowbreak tum.\allowbreak de}}
\newcommand\authoremailii{\texttt{desh{\color{white}NOSPAM}\kern-\wd\boxA{}arna@\allowbreak
in.\allowbreak tum.\allowbreak de}}
\newcommand\authoremailiii{\texttt{lore{\color{white}NOSPAM}\kern-\wd\boxA{}nz.panny@\allowbreak
in.\allowbreak tum.\allowbreak de}}
\newcommand\authoremailiv{\texttt{pope{\color{white}NOSPAM}\kern-\wd\boxA{}scua@\allowbreak
in.\allowbreak tum.\allowbreak de}}
\newcommand\authoremailv{\texttt{tray{\color{white}NOSPAM}\kern-\wd\boxA{}tel@\allowbreak
in.\allowbreak tum.\allowbreak de}}

The command @{command datatype_new} is expected to replace \keyw{datatype} in a
future release. Authors of new theories are encouraged to use the new commands,
and maintainers of older theories may want to consider upgrading.

Comments and bug reports concerning either the tool or this tutorial should be
directed to the authors at \authoremaili, \authoremailii, \authoremailiii,
\authoremailiv, and \authoremailv.
*}


section {* Defining Datatypes
  \label{sec:defining-datatypes} *}

text {*
Datatypes can be specified using the @{command datatype_new} command.
*}


subsection {* Introductory Examples
  \label{ssec:datatype-introductory-examples} *}

text {*
Datatypes are illustrated through concrete examples featuring different flavors
of recursion. More examples can be found in the directory
\verb|~~/src/HOL/|\allowbreak\verb|BNF/Examples|.
*}

subsubsection {* Nonrecursive Types
  \label{sssec:datatype-nonrecursive-types} *}

text {*
Datatypes are introduced by specifying the desired names and argument types for
their constructors. \emph{Enumeration} types are the simplest form of datatype.
All their constructors are nullary:
*}

    datatype_new trool = Truue | Faalse | Perhaaps

text {*
\noindent
Here, @{const Truue}, @{const Faalse}, and @{const Perhaaps} have the type @{typ trool}.

Polymorphic types are possible, such as the following option type, modeled after
its homologue from the @{theory Option} theory:
*}

(*<*)
    hide_const None Some map_option
    hide_type option
(*>*)
    datatype_new 'a option = None | Some 'a

text {*
\noindent
The constructors are @{text "None :: 'a option"} and
@{text "Some :: 'a \<Rightarrow> 'a option"}.

The next example has three type parameters:
*}

    datatype_new ('a, 'b, 'c) triple = Triple 'a 'b 'c

text {*
\noindent
The constructor is
@{text "Triple :: 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a, 'b, 'c) triple"}.
Unlike in Standard ML, curried constructors are supported. The uncurried variant
is also possible:
*}

    datatype_new ('a, 'b, 'c) triple\<^sub>u = Triple\<^sub>u "'a * 'b * 'c"

text {*
\noindent
Occurrences of nonatomic types on the right-hand side of the equal sign must be
enclosed in double quotes, as is customary in Isabelle.
*}


subsubsection {* Simple Recursion
  \label{sssec:datatype-simple-recursion} *}

text {*
Natural numbers are the simplest example of a recursive type:
*}

    datatype_new nat = Zero | Suc nat

text {*
\noindent
Lists were shown in the introduction. Terminated lists are a variant that
stores a value of type @{typ 'b} at the very end:
*}

    datatype_new (*<*)(in early) (*>*)('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"


subsubsection {* Mutual Recursion
  \label{sssec:datatype-mutual-recursion} *}

text {*
\emph{Mutually recursive} types are introduced simultaneously and may refer to
each other. The example below introduces a pair of types for even and odd
natural numbers:
*}

    datatype_new even_nat = Even_Zero | Even_Suc odd_nat
    and odd_nat = Odd_Suc even_nat

text {*
\noindent
Arithmetic expressions are defined via terms, terms via factors, and factors via
expressions:
*}

    datatype_new ('a, 'b) exp =
      Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
    and ('a, 'b) trm =
      Factor "('a, 'b) fct" | Prod "('a, 'b) fct" "('a, 'b) trm"
    and ('a, 'b) fct =
      Const 'a | Var 'b | Expr "('a, 'b) exp"


subsubsection {* Nested Recursion
  \label{sssec:datatype-nested-recursion} *}

text {*
\emph{Nested recursion} occurs when recursive occurrences of a type appear under
a type constructor. The introduction showed some examples of trees with nesting
through lists. A more complex example, that reuses our @{type option} type,
follows:
*}

    datatype_new 'a btree =
      BNode 'a "'a btree option" "'a btree option"

text {*
\noindent
Not all nestings are admissible. For example, this command will fail:
*}

    datatype_new 'a wrong = W1 | W2 (*<*)'a
    typ (*>*)"'a wrong \<Rightarrow> 'a"

text {*
\noindent
The issue is that the function arrow @{text "\<Rightarrow>"} allows recursion
only through its right-hand side. This issue is inherited by polymorphic
datatypes defined in terms of~@{text "\<Rightarrow>"}:
*}

    datatype_new ('a, 'b) fun_copy = Fun "'a \<Rightarrow> 'b"
    datatype_new 'a also_wrong = W1 | W2 (*<*)'a
    typ (*>*)"('a also_wrong, 'a) fun_copy"

text {*
\noindent
The following definition of @{typ 'a}-branching trees is legal:
*}

    datatype_new 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"

text {*
\noindent
And so is the definition of hereditarily finite sets:
*}

    datatype_new hfset = HFSet "hfset fset"

text {*
\noindent
In general, type constructors @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
allow recursion on a subset of their type arguments @{text 'a\<^sub>1}, \ldots,
@{text 'a\<^sub>m}. These type arguments are called \emph{live}; the remaining
type arguments are called \emph{dead}. In @{typ "'a \<Rightarrow> 'b"} and
@{typ "('a, 'b) fun_copy"}, the type variable @{typ 'a} is dead and
@{typ 'b} is live.

Type constructors must be registered as BNFs to have live arguments. This is
done automatically for datatypes and codatatypes introduced by the @{command
datatype_new} and @{command codatatype} commands.
Section~\ref{sec:introducing-bounded-natural-functors} explains how to
register arbitrary type constructors as BNFs.

Here is another example that fails:
*}

    datatype_new 'a pow_list = PNil 'a (*<*)'a
    datatype_new 'a pow_list' = PNil' 'a (*>*)| PCons "('a * 'a) pow_list"

text {*
\noindent
This attempted definition features a different flavor of nesting, where the
recursive call in the type specification occurs around (rather than inside)
another type constructor.
*}

subsubsection {* Auxiliary Constants and Properties
  \label{sssec:datatype-auxiliary-constants-and-properties} *}

text {*
The @{command datatype_new} command introduces various constants in addition to
the constructors. With each datatype are associated set functions, a map
function, a relator, discriminators, and selectors, all of which can be given
custom names. In the example below, the familiar names @{text null}, @{text hd},
@{text tl}, @{text set}, @{text map}, and @{text list_all2}, override the
default names @{text is_Nil}, @{text un_Cons1}, @{text un_Cons2},
@{text set_list}, @{text map_list}, and @{text rel_list}:
*}

(*<*)
    no_translations
      "[x, xs]" == "x # [xs]"
      "[x]" == "x # []"

    no_notation
      Nil ("[]") and
      Cons (infixr "#" 65)

    hide_type list
    hide_const Nil Cons hd tl set map list_all2 rec_list size_list

    context early begin
(*>*)
    datatype_new (set: 'a) list =
      null: Nil
    | Cons (hd: 'a) (tl: "'a list")
    for
      map: map
      rel: list_all2
    where
      "tl Nil = Nil"

text {*
\noindent
The types of the constants that appear in the specification are listed below.

\medskip

\begin{tabular}{@ {}ll@ {}}
Constructors: &
  @{text "Nil \<Colon> 'a list"} \\
&
  @{text "Cons \<Colon> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"} \\
Discriminator: &
  @{text "null \<Colon> 'a list \<Rightarrow> bool"} \\
Selectors: &
  @{text "hd \<Colon> 'a list \<Rightarrow> 'a"} \\
&
  @{text "tl \<Colon> 'a list \<Rightarrow> 'a list"} \\
Set function: &
  @{text "set \<Colon> 'a list \<Rightarrow> 'a set"} \\
Map function: &
  @{text "map \<Colon> ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"} \\
Relator: &
  @{text "list_all2 \<Colon> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool"}
\end{tabular}

\medskip

The discriminator @{const null} and the selectors @{const hd} and @{const tl}
are characterized by the following conditional equations:
%
\[@{thm list.collapse(1)[of xs, no_vars]}
  \qquad @{thm list.collapse(2)[of xs, no_vars]}\]
%
For two-constructor datatypes, a single discriminator constant is sufficient.
The discriminator associated with @{const Cons} is simply
@{term "\<lambda>xs. \<not> null xs"}.

The \keyw{where} clause at the end of the command specifies a default value for
selectors applied to constructors on which they are not a priori specified.
Here, it is used to ensure that the tail of the empty list is itself (instead of
being left unspecified).

Because @{const Nil} is nullary, it is also possible to use
@{term "\<lambda>xs. xs = Nil"} as a discriminator. This is the default behavior
if we omit the identifier @{const null} and the associated colon. Some users
argue against this, because the mixture of constructors and selectors in the
characteristic theorems can lead Isabelle's automation to switch between the
constructor and the destructor view in surprising ways.

The usual mixfix syntax annotations are available for both types and
constructors. For example:
*}

(*<*)
    end
(*>*)
    datatype_new ('a, 'b) prod (infixr "*" 20) = Pair 'a 'b

text {* \blankline *}

    datatype_new (set: 'a) list =
      null: Nil ("[]")
    | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
    for
      map: map
      rel: list_all2

text {*
\noindent
Incidentally, this is how the traditional syntax can be set up:
*}

    syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]")

text {* \blankline *}

    translations
      "[x, xs]" == "x # [xs]"
      "[x]" == "x # []"


subsection {* Command Syntax
  \label{ssec:datatype-command-syntax} *}


subsubsection {* \keyw{datatype_new}
  \label{sssec:datatype-new} *}

text {*
\begin{matharray}{rcl}
  @{command_def "datatype_new"} & : & @{text "local_theory \<rightarrow> local_theory"}
\end{matharray}

@{rail \<open>
  @@{command datatype_new} target? @{syntax dt_options}? \<newline>
    (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') \<newline>
     @{syntax map_rel}? (@'where' (prop + '|'))? + @'and')
  ;
  @{syntax_def dt_options}: '(' (('discs_sels' | 'no_code') + ',') ')'
  ;
  @{syntax_def map_rel}: @'for' ((('map' | 'rel') ':' name) +)
\<close>}

\medskip

\noindent
The @{command datatype_new} command introduces a set of mutually recursive
datatypes specified by their constructors.

The syntactic entity \synt{target} can be used to specify a local
context (e.g., @{text "(in linorder)"} \cite{isabelle-isar-ref}),
and \synt{prop} denotes a HOL proposition.

The optional target is optionally followed by one or both of the following
options:

\begin{itemize}
\setlength{\itemsep}{0pt}

\item
The @{text "discs_sels"} option indicates that discriminators and selectors
should be generated. The option is implicitly enabled if names are specified for
discriminators or selectors.

\item
The @{text "no_code"} option indicates that the datatype should not be
registered for code generation.
\end{itemize}

The optional \keyw{where} clause specifies default values for selectors.
Each proposition must be an equation of the form
@{text "un_D (C \<dots>) = \<dots>"}, where @{text C} is a constructor and
@{text un_D} is a selector.

The left-hand sides of the datatype equations specify the name of the type to
define, its type parameters, and additional information:

@{rail \<open>
  @{syntax_def dt_name}: @{syntax tyargs}? name mixfix?
  ;
  @{syntax_def tyargs}: typefree | '(' (('dead' | name ':')? typefree + ',') ')'
\<close>}

\medskip

\noindent
The syntactic entity \synt{name} denotes an identifier, \synt{mixfix} denotes
the usual parenthesized mixfix notation, and \synt{typefree} denotes fixed type
variable (@{typ 'a}, @{typ 'b}, \ldots) \cite{isabelle-isar-ref}.

The optional names preceding the type variables allow to override the default
names of the set functions (@{text set\<^sub>1_t}, \ldots, @{text set\<^sub>m_t}). Type
arguments can be marked as dead by entering ``@{text dead}'' in front of the
type variable (e.g., ``@{text "(dead 'a)"}''); otherwise, they are live or dead
(and a set function is generated or not) depending on where they occur in the
right-hand sides of the definition. Declaring a type argument as dead can speed
up the type definition but will prevent any later (co)recursion through that
type argument.

Inside a mutually recursive specification, all defined datatypes must
mention exactly the same type variables in the same order.

@{rail \<open>
  @{syntax_def dt_ctor}: (name ':')? name (@{syntax dt_ctor_arg} * ) mixfix?
\<close>}

\medskip

\noindent
The main constituents of a constructor specification are the name of the
constructor and the list of its argument types. An optional discriminator name
can be supplied at the front to override the default, which is
@{text "\<lambda>x. x = C\<^sub>j"} for nullary constructors and
@{text t.is_C\<^sub>j} otherwise.

@{rail \<open>
  @{syntax_def dt_ctor_arg}: type | '(' name ':' type ')'
\<close>}

\medskip

\noindent
The syntactic entity \synt{type} denotes a HOL type \cite{isabelle-isar-ref}.

In addition to the type of a constructor argument, it is possible to specify a
name for the corresponding selector to override the default name
(@{text un_C\<^sub>ji}). The same selector names can be reused for several
constructors as long as they share the same type.
*}


subsubsection {* \keyw{datatype_compat}
  \label{sssec:datatype-compat} *}

text {*
\begin{matharray}{rcl}
  @{command_def "datatype_compat"} & : & @{text "local_theory \<rightarrow> local_theory"}
\end{matharray}

@{rail \<open>
  @@{command datatype_compat} (name +)
\<close>}

\medskip

\noindent
The @{command datatype_compat} command registers new-style datatypes as
old-style datatypes. For example:
*}

    datatype_compat even_nat odd_nat

text {* \blankline *}

    ML {* Datatype_Data.get_info @{theory} @{type_name even_nat} *}

text {*
The syntactic entity \synt{name} denotes an identifier \cite{isabelle-isar-ref}.

The command is interesting because the old datatype package provides some
functionality that is not yet replicated in the new package, such as the
integration with Quickcheck.

A few remarks concern nested recursive datatypes:

\begin{itemize}
\setlength{\itemsep}{0pt}

\item The old-style, nested-as-mutual induction rule and recursor theorems are
generated under their usual names but with ``@{text "compat_"}'' prefixed
(e.g., @{text compat_tree.induct}).

\item All types through which recursion takes place must be new-style datatypes
or the function type. In principle, it should be possible to support old-style
datatypes as well, but this has not been implemented yet (and there is currently
no way to register old-style datatypes as new-style datatypes).

\item The recursor produced for types that recurse through functions has a
different signature than with the old package. This might affect the behavior of
some third-party extensions.
\end{itemize}

An alternative to @{command datatype_compat} is to use the old package's
\keyw{rep_\allowbreak datatype} command. The associated proof obligations must then be
discharged manually.
*}


subsection {* Generated Constants
  \label{ssec:datatype-generated-constants} *}

text {*
Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
with $m > 0$ live type variables and $n$ constructors
@{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the
following auxiliary constants are introduced:

\medskip

\begin{tabular}{@ {}ll@ {}}
Case combinator: &
  @{text t.case_t} (rendered using the familiar @{text case}--@{text of} syntax) \\
Discriminators: &
  @{text t.is_C\<^sub>1}$, \ldots, $@{text t.is_C\<^sub>n} \\
Selectors: &
  @{text t.un_C\<^sub>11}$, \ldots, $@{text t.un_C\<^sub>1k\<^sub>1} \\
& \quad\vdots \\
& @{text t.un_C\<^sub>n1}$, \ldots, $@{text t.un_C\<^sub>nk\<^sub>n} \\
Set functions: &
  @{text t.set\<^sub>1_t}, \ldots, @{text t.set\<^sub>m_t} \\
Map function: &
  @{text t.map_t} \\
Relator: &
  @{text t.rel_t} \\
Recursor: &
  @{text t.rec_t} \\
Size function: &
  @{text t.size_t}
\end{tabular}

\medskip

\noindent
The case combinator, discriminators, and selectors are collectively called
\emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the
names and is normally hidden.

In addition to the above, the @{class size} class is instantiated to overload the
@{const size} function based on @{text t.size_t}.
*}


subsection {* Generated Theorems
  \label{ssec:datatype-generated-theorems} *}

text {*
The characteristic theorems generated by @{command datatype_new} are grouped in
three broad categories:

\begin{itemize}
\setlength{\itemsep}{0pt}

\item The \emph{free constructor theorems}
(Section~\ref{sssec:free-constructor-theorems}) are properties of the
constructors and destructors that can be derived for any freely generated type.
Internally, the derivation is performed by @{command free_constructors}.

\item The \emph{functorial theorems} (Section~\ref{sssec:functorial-theorems})
are properties of datatypes related to their BNF nature.

\item The \emph{inductive theorems} (Section~\ref{sssec:inductive-theorems})
are properties of datatypes related to their inductive nature.

\end{itemize}

\noindent
The full list of named theorems can be obtained as usual by entering the
command \keyw{print_theorems} immediately after the datatype definition.
This list normally excludes low-level theorems that reveal internal
constructions. To make these accessible, add the line
*}

    declare [[bnf_note_all]]
(*<*)
    declare [[bnf_note_all = false]]
(*>*)

text {*
\noindent
to the top of the theory file.
*}

subsubsection {* Free Constructor Theorems
  \label{sssec:free-constructor-theorems} *}

(*<*)
    consts nonnull :: 'a
(*>*)

text {*
The free constructor theorems are partitioned in three subgroups. The first
subgroup of properties is concerned with the constructors. They are listed below
for @{typ "'a list"}:

\begin{indentblock}
\begin{description}

\item[@{text "t."}\hthm{inject} @{text "[iff, induct_simp]"}\rm:] ~ \\
@{thm list.inject[no_vars]}

\item[@{text "t."}\hthm{distinct} @{text "[simp, induct_simp]"}\rm:] ~ \\
@{thm list.distinct(1)[no_vars]} \\
@{thm list.distinct(2)[no_vars]}

\item[@{text "t."}\hthm{exhaust} @{text "[cases t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
@{thm list.exhaust[no_vars]}

\item[@{text "t."}\hthm{nchotomy}\rm:] ~ \\
@{thm list.nchotomy[no_vars]}

\end{description}
\end{indentblock}

\noindent
In addition, these nameless theorems are registered as safe elimination rules:

\begin{indentblock}
\begin{description}

\item[@{text "t."}\hthm{distinct {\upshape[}THEN notE}@{text ", elim!"}\hthm{\upshape]}\rm:] ~ \\
@{thm list.distinct(1)[THEN notE, elim!, no_vars]} \\
@{thm list.distinct(2)[THEN notE, elim!, no_vars]}

\end{description}
\end{indentblock}

\noindent
The next subgroup is concerned with the case combinator:

\begin{indentblock}
\begin{description}

\item[@{text "t."}\hthm{case} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.case(1)[no_vars]} \\
@{thm list.case(2)[no_vars]}

\item[@{text "t."}\hthm{case_cong} @{text "[fundef_cong]"}\rm:] ~ \\
@{thm list.case_cong[no_vars]}

\item[@{text "t."}\hthm{case_cong_weak} @{text "[cong]"}\rm:] ~ \\
@{thm list.case_cong_weak[no_vars]}

\item[@{text "t."}\hthm{split}\rm:] ~ \\
@{thm list.split[no_vars]}

\item[@{text "t."}\hthm{split_asm}\rm:] ~ \\
@{thm list.split_asm[no_vars]}

\item[@{text "t."}\hthm{splits} = @{text "split split_asm"}]

\end{description}
\end{indentblock}

\noindent
The third subgroup revolves around discriminators and selectors:

\begin{indentblock}
\begin{description}

\item[@{text "t."}\hthm{disc} @{text "[simp]"}\rm:] ~ \\
@{thm list.disc(1)[no_vars]} \\
@{thm list.disc(2)[no_vars]}

\item[@{text "t."}\hthm{discI}\rm:] ~ \\
@{thm list.discI(1)[no_vars]} \\
@{thm list.discI(2)[no_vars]}

\item[@{text "t."}\hthm{sel} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.sel(1)[no_vars]} \\
@{thm list.sel(2)[no_vars]}

\item[@{text "t."}\hthm{collapse} @{text "[simp]"}\rm:] ~ \\
@{thm list.collapse(1)[no_vars]} \\
@{thm list.collapse(2)[no_vars]}

\item[@{text "t."}\hthm{distinct_disc} @{text "[dest]"}\rm:] ~ \\
These properties are missing for @{typ "'a list"} because there is only one
proper discriminator. Had the datatype been introduced with a second
discriminator called @{const nonnull}, they would have read thusly: \\[\jot]
@{prop "null list \<Longrightarrow> \<not> nonnull list"} \\
@{prop "nonnull list \<Longrightarrow> \<not> null list"}

\item[@{text "t."}\hthm{exhaust_disc} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
@{thm list.exhaust_disc[no_vars]}

\item[@{text "t."}\hthm{exhaust_sel} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
@{thm list.exhaust_sel[no_vars]}

\item[@{text "t."}\hthm{expand}\rm:] ~ \\
@{thm list.expand[no_vars]}

\item[@{text "t."}\hthm{split_sel}\rm:] ~ \\
@{thm list.split_sel[no_vars]}

\item[@{text "t."}\hthm{split_sel_asm}\rm:] ~ \\
@{thm list.split_sel_asm[no_vars]}

\item[@{text "t."}\hthm{split_sels} = @{text "split_sel split_sel_asm"}]

\item[@{text "t."}\hthm{case_eq_if}\rm:] ~ \\
@{thm list.case_eq_if[no_vars]}

\end{description}
\end{indentblock}

\noindent
In addition, equational versions of @{text t.disc} are registered with the @{text "[code]"}
attribute.
*}


subsubsection {* Functorial Theorems
  \label{sssec:functorial-theorems} *}

text {*
The functorial theorems are partitioned in two subgroups. The first subgroup
consists of properties involving the constructors or the destructors and either
a set function, the map function, or the relator:

\begin{indentblock}
\begin{description}

\item[@{text "t."}\hthm{case_transfer}\rm:] ~ \\
@{thm list.case_transfer[no_vars]}

\item[@{text "t."}\hthm{ctr_transfer}\rm:] ~ \\
@{thm list.ctr_transfer(1)[no_vars]} \\
@{thm list.ctr_transfer(2)[no_vars]}

\item[@{text "t."}\hthm{disc_transfer}\rm:] ~ \\
@{thm list.disc_transfer(1)[no_vars]} \\
@{thm list.disc_transfer(2)[no_vars]}

\item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.set(1)[no_vars]} \\
@{thm list.set(2)[no_vars]}

\item[@{text "t."}\hthm{set_cases} @{text "[consumes 1, cases set: set\<^sub>i_t]"}\rm:] ~ \\
@{thm list.set_cases[no_vars]}

\item[@{text "t."}\hthm{set_intros}\rm:] ~ \\
@{thm list.set_intros(1)[no_vars]} \\
@{thm list.set_intros(2)[no_vars]}

\item[@{text "t."}\hthm{set_sel}\rm:] ~ \\
@{thm list.set_sel[no_vars]}

\item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.map(1)[no_vars]} \\
@{thm list.map(2)[no_vars]}

\item[@{text "t."}\hthm{map_disc_iff} @{text "[simp]"}\rm:] ~ \\
@{thm list.map_disc_iff[no_vars]}

\item[@{text "t."}\hthm{map_sel}\rm:] ~ \\
@{thm list.map_sel[no_vars]}

\item[@{text "t."}\hthm{rel_inject} @{text "[simp]"}\rm:] ~ \\
@{thm list.rel_inject(1)[no_vars]} \\
@{thm list.rel_inject(2)[no_vars]}

\item[@{text "t."}\hthm{rel_distinct} @{text "[simp]"}\rm:] ~ \\
@{thm list.rel_distinct(1)[no_vars]} \\
@{thm list.rel_distinct(2)[no_vars]}

\item[@{text "t."}\hthm{rel_intros}\rm:] ~ \\
@{thm list.rel_intros(1)[no_vars]} \\
@{thm list.rel_intros(2)[no_vars]}

% FIXME (and add @ before antiquotation below)
%\item[@{text "t."}\hthm{rel_cases} @{text "[consumes 1, case_names t\<^sub>1 \<dots> t\<^sub>m, cases pred]"}\rm:] ~ \\
%{thm list.rel_cases[no_vars]}

\item[@{text "t."}\hthm{rel_sel}\rm:] ~ \\
@{thm list.rel_sel[no_vars]}

\end{description}
\end{indentblock}

\noindent
In addition, equational versions of @{text t.rel_inject} and @{text
rel_distinct} are registered with the @{text "[code]"} attribute.

The second subgroup consists of more abstract properties of the set functions,
the map function, and the relator:

\begin{indentblock}
\begin{description}

\item[@{text "t."}\hthm{inj_map}\rm:] ~ \\
@{thm list.inj_map[no_vars]}

\item[@{text "t."}\hthm{inj_map_strong}\rm:] ~ \\
@{thm list.inj_map_strong[no_vars]}

\item[@{text "t."}\hthm{set_map}\rm:] ~ \\
@{thm list.set_map[no_vars]}

\item[@{text "t."}\hthm{set_transfer}\rm:] ~ \\
@{thm list.set_transfer[no_vars]}

\item[@{text "t."}\hthm{map_comg0}\rm:] ~ \\
@{thm list.map_cong0[no_vars]}

\item[@{text "t."}\hthm{map_cong} @{text "[fundef_cong]"}\rm:] ~ \\
@{thm list.map_cong[no_vars]}

\item[@{text "t."}\hthm{map_cong_simp}\rm:] ~ \\
@{thm list.map_cong_simp[no_vars]}

\item[@{text "t."}\hthm{map_id}\rm:] ~ \\
@{thm list.map_id[no_vars]}

\item[@{text "t."}\hthm{map_id0}\rm:] ~ \\
@{thm list.map_id0[no_vars]}

\item[@{text "t."}\hthm{map_ident}\rm:] ~ \\
@{thm list.map_ident[no_vars]}

\item[@{text "t."}\hthm{map_transfer}\rm:] ~ \\
@{thm list.map_transfer[no_vars]}

\item[@{text "t."}\hthm{rel_compp}\rm:] ~ \\
@{thm list.rel_compp[no_vars]}

\item[@{text "t."}\hthm{rel_conversep}\rm:] ~ \\
@{thm list.rel_conversep[no_vars]}

\item[@{text "t."}\hthm{rel_eq}\rm:] ~ \\
@{thm list.rel_eq[no_vars]}

\item[@{text "t."}\hthm{rel_flip}\rm:] ~ \\
@{thm list.rel_flip[no_vars]}

\item[@{text "t."}\hthm{rel_map}\rm:] ~ \\
@{thm list.rel_map(1)[no_vars]} \\
@{thm list.rel_map(2)[no_vars]}

\item[@{text "t."}\hthm{rel_mono}\rm:] ~ \\
@{thm list.rel_mono[no_vars]}

\item[@{text "t."}\hthm{rel_transfer}\rm:] ~ \\
@{thm list.rel_transfer[no_vars]}

\end{description}
\end{indentblock}
*}


subsubsection {* Inductive Theorems
  \label{sssec:inductive-theorems} *}

text {*
The inductive theorems are as follows:

\begin{indentblock}
\begin{description}

\item[@{text "t."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n, induct t]"}\rm:] ~ \\
@{thm list.induct[no_vars]}

\item[@{text "t."}\hthm{rel_induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n, induct pred]"}\rm:] ~ \\
@{thm list.rel_induct[no_vars]}

\item[\begin{tabular}{@ {}l@ {}}
  @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm: \\
  @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel_induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm: \\
\end{tabular}] ~ \\
Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
prove $m$ properties simultaneously.

\item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.rec(1)[no_vars]} \\
@{thm list.rec(2)[no_vars]}

\item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\
@{thm list.rec_o_map[no_vars]}

\item[@{text "t."}\hthm{size} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.size(1)[no_vars]} \\
@{thm list.size(2)[no_vars]} \\
@{thm list.size(3)[no_vars]} \\
@{thm list.size(4)[no_vars]}

\item[@{text "t."}\hthm{size_o_map}\rm:] ~ \\
@{thm list.size_o_map[no_vars]}

\end{description}
\end{indentblock}

\noindent
For convenience, @{command datatype_new} also provides the following collection:

\begin{indentblock}
\begin{description}

\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.map} @{text t.rel_inject}] ~ \\
@{text t.rel_distinct} @{text t.set}

\end{description}
\end{indentblock}
*}


subsection {* Compatibility Issues
  \label{ssec:datatype-compatibility-issues} *}

text {*
The command @{command datatype_new} has been designed to be highly compatible
with the old \keyw{datatype}, to ease migration. There are nonetheless a few
incompatibilities that may arise when porting to the new package:

\begin{itemize}
\setlength{\itemsep}{0pt}

\item \emph{The Standard ML interfaces are different.} Tools and extensions
written to call the old ML interfaces will need to be adapted to the new
interfaces. This concerns Quickcheck in particular. Whenever possible, it is
recommended to use @{command datatype_compat} to register new-style datatypes
as old-style datatypes.

\item \emph{The constants @{text t_case}, @{text t_rec}, and @{text t_size} are
now called @{text case_t}, @{text rec_t}, and @{text size_t}.}

\item \emph{The recursor @{text rec_t} has a different signature for nested
recursive datatypes.} In the old package, nested recursion through non-functions
was internally reduced to mutual recursion. This reduction was visible in the
type of the recursor, used by \keyw{primrec}. Recursion through functions was
handled specially. In the new package, nested recursion (for functions and
non-functions) is handled in a more modular fashion. The old-style recursor can
be generated on demand using @{command primrec} if the recursion is via
new-style datatypes, as explained in
Section~\ref{sssec:primrec-nested-as-mutual-recursion}.

\item \emph{Accordingly, the induction rule is different for nested recursive
datatypes.} Again, the old-style induction rule can be generated on demand using
@{command primrec} if the recursion is via new-style datatypes, as explained in
Section~\ref{sssec:primrec-nested-as-mutual-recursion}.

\item \emph{The internal constructions are completely different.} Proof texts
that unfold the definition of constants introduced by \keyw{datatype} will be
difficult to port.

\item \emph{Some theorems have different names.}
For non-mutually recursive datatypes,
the alias @{text t.inducts} for @{text t.induct} is no longer generated.
For $m > 1$ mutually recursive datatypes,
@{text "t\<^sub>1_\<dots>_t\<^sub>m.inducts(i)"} has been renamed
@{text "t\<^sub>i.induct"} for each @{text "i \<in> {1, \<dots>, t}"}, and similarly the
collection @{text "t\<^sub>1_\<dots>_t\<^sub>m.size"} has been divided into @{text "t\<^sub>1.size"},
\ldots, @{text "t\<^sub>m.size"}.

\item \emph{The @{text t.simps} collection has been extended.}
Previously available theorems are available at the same index.

\item \emph{Variables in generated properties have different names.} This is
rarely an issue, except in proof texts that refer to variable names in the
@{text "[where \<dots>]"} attribute. The solution is to use the more robust
@{text "[of \<dots>]"} syntax.
\end{itemize}

In the other direction, there is currently no way to register old-style
datatypes as new-style datatypes. If the goal is to define new-style datatypes
with nested recursion through old-style datatypes, the old-style
datatypes can be registered as a BNF
(Section~\ref{sec:introducing-bounded-natural-functors}). If the goal is
to derive discriminators and selectors, this can be achieved using
@{command free_constructors}
(Section~\ref{sec:deriving-destructors-and-theorems-for-free-constructors}).
*}


section {* Defining Recursive Functions
  \label{sec:defining-recursive-functions} *}

text {*
Recursive functions over datatypes can be specified using the @{command primrec}
command, which supports primitive recursion, or using the more general
\keyw{fun} and \keyw{function} commands. Here, the focus is on
@{command primrec}; the other two commands are described in a separate
tutorial \cite{isabelle-function}.

%%% TODO: partial_function
*}


subsection {* Introductory Examples
  \label{ssec:primrec-introductory-examples} *}

text {*
Primitive recursion is illustrated through concrete examples based on the
datatypes defined in Section~\ref{ssec:datatype-introductory-examples}. More
examples can be found in the directory \verb|~~/src/HOL/BNF_Examples|.
*}


subsubsection {* Nonrecursive Types
  \label{sssec:primrec-nonrecursive-types} *}

text {*
Primitive recursion removes one layer of constructors on the left-hand side in
each equation. For example:
*}

    primrec bool_of_trool :: "trool \<Rightarrow> bool" where
      "bool_of_trool Faalse \<longleftrightarrow> False" |
      "bool_of_trool Truue \<longleftrightarrow> True"

text {* \blankline *}

    primrec the_list :: "'a option \<Rightarrow> 'a list" where
      "the_list None = []" |
      "the_list (Some a) = [a]"

text {* \blankline *}

    primrec the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
      "the_default d None = d" |
      "the_default _ (Some a) = a"

text {* \blankline *}

    primrec mirrror :: "('a, 'b, 'c) triple \<Rightarrow> ('c, 'b, 'a) triple" where
      "mirrror (Triple a b c) = Triple c b a"

text {*
\noindent
The equations can be specified in any order, and it is acceptable to leave out
some cases, which are then unspecified. Pattern matching on the left-hand side
is restricted to a single datatype, which must correspond to the same argument
in all equations.
*}


subsubsection {* Simple Recursion
  \label{sssec:primrec-simple-recursion} *}

text {*
For simple recursive types, recursive calls on a constructor argument are
allowed on the right-hand side:
*}

    primrec replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
      "replicate Zero _ = []" |
      "replicate (Suc n) x = x # replicate n x"

text {* \blankline *}

    primrec at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
      "at (x # xs) j =
         (case j of
            Zero \<Rightarrow> x
          | Suc j' \<Rightarrow> at xs j')"

text {* \blankline *}

    primrec (*<*)(in early) (*>*)tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
      "tfold _ (TNil y) = y" |
      "tfold f (TCons x xs) = f x (tfold f xs)"

text {*
\noindent
Pattern matching is only available for the argument on which the recursion takes
place. Fortunately, it is easy to generate pattern-maching equations using the
\keyw{simps_of_case} command provided by the theory
\verb|~~/src/HOL/|\allowbreak\verb|Library/|\allowbreak\verb|Simps_Case_Conv|.
*}

    simps_of_case at_simps: at.simps

text {*
This generates the lemma collection @{thm [source] at_simps}:
%
\[@{thm at_simps(1)[no_vars]}
  \qquad @{thm at_simps(2)[no_vars]}\]
%
The next example is defined using \keyw{fun} to escape the syntactic
restrictions imposed on primitively recursive functions. The
@{command datatype_compat} command is needed to register new-style datatypes
for use with \keyw{fun} and \keyw{function}
(Section~\ref{sssec:datatype-compat}):
*}

    datatype_compat nat

text {* \blankline *}

    fun at_least_two :: "nat \<Rightarrow> bool" where
      "at_least_two (Suc (Suc _)) \<longleftrightarrow> True" |
      "at_least_two _ \<longleftrightarrow> False"


subsubsection {* Mutual Recursion
  \label{sssec:primrec-mutual-recursion} *}

text {*
The syntax for mutually recursive functions over mutually recursive datatypes
is straightforward:
*}

    primrec
      nat_of_even_nat :: "even_nat \<Rightarrow> nat" and
      nat_of_odd_nat :: "odd_nat \<Rightarrow> nat"
    where
      "nat_of_even_nat Even_Zero = Zero" |
      "nat_of_even_nat (Even_Suc n) = Suc (nat_of_odd_nat n)" |
      "nat_of_odd_nat (Odd_Suc n) = Suc (nat_of_even_nat n)"

text {* \blankline *}

    primrec
      eval\<^sub>e :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) exp \<Rightarrow> int" and
      eval\<^sub>t :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) trm \<Rightarrow> int" and