(*  Title:      Doc/Datatypes/Datatypes.thy

    Author:     Jasmin Blanchette, TU Muenchen

    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/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.

To use the package, it is necessary to import the @{theory BNF} theory, which

can be precompiled into the \texttt{HOL-BNF} image. The following commands show

how to launch jEdit/PIDE with the image loaded and how to build the image

without launching jEdit:

*}

text {*

\noindent

\ \ \ \ \texttt{isabelle jedit -l HOL-BNF} \\

\noindent

\hbox{}\ \ \ \ \texttt{isabelle build -b HOL-BNF}

*}

text {*

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{If the @{text quick_and_dirty} option is enabled, some of the

internal constructions and most of the internal proof obligations are skipped.}

The package's metatheory is described in a pair of papers

\cite{traytel-et-al-2012,blanchette-et-al-wit}. 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_new}, \keyw{fun}, and \keyw{function}.

\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:registering-bounded-natural-functors}, ``Registering

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 wrap_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{lore{\color{white}NOSPAM}\kern-\wd\boxA{}nz.panny@\allowbreak

\allowbreak tum.\allowbreak de}}

\newcommand\authoremailiii{\texttt{pope{\color{white}NOSPAM}\kern-\wd\boxA{}scua@\allowbreak

in.\allowbreak tum.\allowbreak de}}

\newcommand\authoremailiv{\texttt{tray{\color{white}NOSPAM}\kern-\wd\boxA{}tel@\allowbreak

in.\allowbreak tum.\allowbreak de}}

The commands @{command datatype_new} and @{command primrec_new} are expected to

replace \keyw{datatype} and \keyw{primrec} 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,

and \authoremailiv.

*}

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

(*>*)

    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) fn = Fn "'a \<Rightarrow> 'b"

    datatype_new 'a also_wrong = W1 | W2 (*<*)'a

    typ (*>*)"('a also_wrong, 'a) fn"

text {*

\noindent

This is legal:

*}

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

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) fn"}, 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:registering-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 one 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

    context early begin

(*>*)

    datatype_new (set: 'a) list (map: map rel: list_all2) =

      null: Nil (defaults tl: Nil)

    | Cons (hd: 'a) (tl: "'a list")

text {*

\noindent

\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}

The discriminator @{const null} and the selectors @{const hd} and @{const tl}

are characterized as follows:

%

\[@{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 @{text defaults} clause following the @{const Nil} constructor specifies a

default value for selectors associated with other constructors. 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 specified by

entering ``@{text "="}'' instead of the identifier @{const null}. Although this

may look appealing, 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 (map: map rel: list_all2) =

      null: Nil ("[]")

    | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)

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 "

  @@{command datatype_new} target? @{syntax dt_options}? \\

    (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')

  ;

  @{syntax_def dt_options}: '(' (('no_discs_sels' | 'rep_compat') + ',') ')'

"}

The syntactic entity \synt{target} can be used to specify a local

context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference

manual \cite{isabelle-isar-ref}.

%

The optional target is optionally followed by datatype-specific options:

\begin{itemize}

\setlength{\itemsep}{0pt}

\item

The @{text "no_discs_sels"} option indicates that no discriminators or selectors

should be generated.

\item

The @{text "rep_compat"} option indicates that the generated names should

contain optional (and normally not displayed) ``@{text "new."}'' components to

prevent clashes with a later call to \keyw{rep\_datatype}. See

Section~\ref{ssec:datatype-compatibility-issues} for details.

\end{itemize}

The left-hand sides of the datatype equations specify the name of the type to

define, its type parameters, and additional information:

@{rail "

  @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?

  ;

  @{syntax_def tyargs}: typefree | '(' ((name ':')? typefree + ',') ')'

  ;

  @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'

"}

\noindent

The syntactic entity \synt{name} denotes an identifier, \synt{typefree}

denotes fixed type variable (@{typ 'a}, @{typ 'b}, \ldots), and \synt{mixfix}

denotes the usual parenthesized mixfix notation. They are documented in the Isar

reference manual \cite{isabelle-isar-ref}.

The optional names preceding the type variables allow to override the default

names of the set functions (@{text set1_t}, \ldots, @{text setM_t}).

Inside a mutually recursive specification, all defined datatypes must

mention exactly the same type variables in the same order.

@{rail "

  @{syntax_def ctor}: (name ':')? name (@{syntax ctor_arg} * ) \\

    @{syntax dt_sel_defaults}? mixfix?

"}

\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 name

(@{text t.is_C\<^sub>j}).

@{rail "

  @{syntax_def ctor_arg}: type | '(' name ':' type ')'

"}

\medskip

\noindent

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.

@{rail "

  @{syntax_def dt_sel_defaults}: '(' 'defaults' (name ':' term +) ')'

"}

\noindent

Given a constructor

@{text "C \<Colon> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<sigma>"},

default values can be specified for any selector

@{text "un_D \<Colon> \<sigma> \<Rightarrow> \<tau>"}

associated with other constructors. The specified default value must be of type

@{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<tau>"}

(i.e., it may depend on @{text C}'s arguments).

*}

subsubsection {* \keyw{datatype\_new\_compat}

  \label{sssec:datatype-new-compat} *}

text {*

\begin{matharray}{rcl}

  @{command_def "datatype_new_compat"} & : & @{text "local_theory \<rightarrow> local_theory"}

\end{matharray}

@{rail "

  @@{command datatype_new_compat} names

"}

\noindent

The old datatype package provides some functionality that is not yet replicated

in the new package:

\begin{itemize}

\setlength{\itemsep}{0pt}

\item It is integrated with \keyw{fun} and \keyw{function}

\cite{isabelle-function}, Nitpick \cite{isabelle-nitpick}, Quickcheck,

and other packages.

\item It is extended by various add-ons, notably to produce instances of the

@{const size} function.

\end{itemize}

\noindent

New-style datatypes can in most cases be registered as old-style datatypes using

@{command datatype_new_compat}. The \textit{names} argument is a space-separated

list of type names that are mutually recursive. For example:

*}

    datatype_new_compat even_nat odd_nat

text {* \blankline *}

    thm even_nat_odd_nat.size

text {* \blankline *}

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

text {*

A few remarks concern nested recursive datatypes only:

\begin{itemize}

\setlength{\itemsep}{0pt}

\item The old-style, nested-as-mutual induction rule, iterator theorems, 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 the command does not support this 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 makes it impossible to use

the old \keyw{primrec} command.

\end{itemize}

An alternative to @{command datatype_new_compat} is to use the old package's

\keyw{rep\_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:

\begin{itemize}

\setlength{\itemsep}{0pt}

\item \relax{Case combinator}: @{text t.case_t} (rendered using the familiar

@{text case}--@{text of} syntax)

\item \relax{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots,

@{text "t.is_C\<^sub>n"}

\item \relax{Selectors}:

@{text t.un_C\<^sub>11}$, \ldots, @{text t.un_C\<^sub>1k\<^sub>1}, \\

\phantom{\relax{Selectors:}} \quad\vdots \\

\phantom{\relax{Selectors:}} @{text t.un_C\<^sub>n1}$, \ldots, @{text t.un_C\<^sub>nk\<^sub>n}.

\item \relax{Set functions} (or \relax{natural transformations}):

@{text set1_t}, \ldots, @{text t.setm_t}

\item \relax{Map function} (or \relax{functorial action}): @{text t.map_t}

\item \relax{Relator}: @{text t.rel_t}

\item \relax{Iterator}: @{text t.fold_t}

\item \relax{Recursor}: @{text t.rec_t}

\end{itemize}

\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.

*}

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} are properties about the constructors

and destructors that can be derived for any freely generated type. Internally,

the derivation is performed by @{command wrap_free_constructors}.

\item The \emph{functorial theorems} are properties of datatypes related to

their BNF nature.

\item The \emph{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 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}\rm:] ~ \\

@{thm list.case_cong[no_vars]}

\item[@{text "t."}\hthm{weak\_case\_cong} @{text "[cong]"}\rm:] ~ \\

@{thm list.weak_case_cong[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 and last 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{disc\_exclude} @{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{disc\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\

@{thm list.disc_exhaust[no_vars]}

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

@{thm list.sel_exhaust[no_vars]}

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

@{thm list.expand[no_vars]}

\item[@{text "t."}\hthm{sel\_split}\rm:] ~ \\

@{thm list.sel_split[no_vars]}

\item[@{text "t."}\hthm{sel\_split\_asm}\rm:] ~ \\

@{thm list.sel_split_asm[no_vars]}

\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 BNF-related theorem are as follows:

\begin{indentblock}

\begin{description}

\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{map} @{text "[simp, code]"}\rm:] ~ \\

@{thm list.map(1)[no_vars]} \\

@{thm list.map(2)[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]}

\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.

*}

subsubsection {* Inductive Theorems

  \label{sssec:inductive-theorems} *}

text {*

The inductive theorems are as follows:

\begin{indentblock}

\begin{description}

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

@{thm list.induct[no_vars]}

\item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\

Given $m > 1$ mutually recursive datatypes, this induction rule can be used to

prove $m$ properties simultaneously.

\item[@{text "t."}\hthm{fold} @{text "[simp, code]"}\rm:] ~ \\

@{thm list.fold(1)[no_vars]} \\

@{thm list.fold(2)[no_vars]}

\item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\

@{thm list.rec(1)[no_vars]} \\

@{thm list.rec(2)[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.fold} @{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. Little has been done so far in this direction. Whenever possible, it

is recommended to use @{command datatype_new_compat} or \keyw{rep\_datatype}

to register new-style datatypes as old-style datatypes.

\item \emph{The constants @{text t_case} and @{text t_rec} are now called

@{text case_t} and @{text rec_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_new}, as explained in

Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via

new-style datatypes.

\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_new}, as explained in

Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via

new-style datatypes.

\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{A few theorems have different names.}

The properties @{text t.cases} and @{text t.recs} have been renamed

@{text t.case} and @{text t.rec}. For non-mutually recursive datatypes,

@{text t.inducts} is available as @{text t.induct}.

For $m > 1$ mutually recursive datatypes,

@{text "t\<^sub>1_\<dots>_t\<^sub>m.inducts(i)"} has been renamed

@{text "t\<^sub>i.induct"}.

\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:registering-bounded-natural-functors}). If the goal is

to derive discriminators and selectors, this can be achieved using @{command

wrap_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_new} command, which supports primitive recursion, or using the more

general \keyw{fun} and \keyw{function} commands. Here, the focus is on @{command

primrec_new}; 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} *}