(*  Title:      Doc/Datatypes/Datatypes.thy

    Author:     Julian Biendarra, TU Muenchen

    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.

*)

theory Datatypes

imports

  Setup

  "~~/src/HOL/Library/BNF_Axiomatization"

  "~~/src/HOL/Library/Cardinal_Notations"

  "~~/src/HOL/Library/Countable"

  "~~/src/HOL/Library/FSet"

  "~~/src/HOL/Library/Simps_Case_Conv"

begin

section \<open>Introduction

  \label{sec:introduction}\<close>

text \<open>

The 2013 edition of Isabelle introduced a definitional package for freely

generated datatypes and codatatypes. This package replaces the earlier

implementation due to Berghofer and Wenzel @{cite "Berghofer-Wenzel:1999:TPHOL"}.

Perhaps the main advantage of the new package is that it supports recursion

through a large class of non-datatypes, such as finite sets:

\<close>

    datatype '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 \<open>

\noindent

Another strong point is the support for local definitions:

\<close>

    context linorder

    begin

    datatype flag = Less | Eq | Greater

    end

text \<open>

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

\<close>

(*<*)

    locale early

    locale late

(*>*)

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

text \<open>

\noindent

Mixed inductive--coinductive recursion is possible via nesting. Compare the

following four Rose tree examples:

\<close>

    datatype (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"

    datatype (*<*)(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 \<open>

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 \<^file>\<open>~~/src/HOL/Library/BNF_Axiomatization.thy\<close>.

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 omitted

if the @{text quick_and_dirty} option is enabled.}

The package is described in a number of scientific papers

@{cite "traytel-et-al-2012" and "blanchette-et-al-2014-impl" and

"panny-et-al-2014" and "blanchette-et-al-2015-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} command.

\item Section \ref{sec:defining-primitively-recursive-functions}, ``Defining

Primitively Recursive Functions,'' describes how to specify functions

using @{command primrec}. (A separate tutorial @{cite "isabelle-function"}

describes the more powerful \keyw{fun} and \keyw{function} commands.)

\item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''

describes how to specify codatatypes using the @{command codatatype} command.

\item Section \ref{sec:defining-primitively-corecursive-functions},

``Defining Primitively Corecursive Functions,'' describes how to specify

functions using the @{command primcorec} and

@{command primcorecursive} commands. (A separate tutorial

@{cite "isabelle-corec"} describes the more powerful \keyw{corec} and

\keyw{corecursive} 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 free_constructors} to derive destructor constants

and theorems for freely generated types, as performed internally by

@{command datatype} and @{command codatatype}.

%\item Section \ref{sec:using-the-standard-ml-interface}, ``Using the Standard

%ML Interface,'' describes the package's programmatic interface.

\item Section \ref{sec:selecting-plugins}, ``Selecting Plugins,'' is concerned

with the package's interoperability with other Isabelle packages and tools, such

as the code generator, Transfer, Lifting, and Quickcheck.

\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and

Limitations,'' concludes with known open issues.

\end{itemize}

\newbox\boxA

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

\newcommand\authoremaili{\texttt{jasmin.blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak

gmail.\allowbreak com}}

Comments and bug reports concerning either the package or this tutorial should

be directed to the second author at \authoremaili{} or to the

\texttt{cl-isabelle-users} mailing list.

\<close>

section \<open>Defining Datatypes

  \label{sec:defining-datatypes}\<close>

text \<open>

Datatypes can be specified using the @{command datatype} command.

\<close>

subsection \<open>Introductory Examples

  \label{ssec:datatype-introductory-examples}\<close>

text \<open>

Datatypes are illustrated through concrete examples featuring different flavors

of recursion. More examples can be found in the directory

\<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>.

\<close>

subsubsection \<open>Nonrecursive Types

  \label{sssec:datatype-nonrecursive-types}\<close>

text \<open>

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:

\<close>

    datatype trool = Truue | Faalse | Perhaaps

text \<open>

\noindent

@{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:

\<close>

(*<*)

    hide_const None Some map_option

    hide_type option

(*>*)

    datatype 'a option = None | Some 'a

text \<open>

\noindent

The constructors are @{text "None :: 'a option"} and

@{text "Some :: 'a \<Rightarrow> 'a option"}.

The next example has three type parameters:

\<close>

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

text \<open>

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

\<close>

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

text \<open>

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

\<close>

subsubsection \<open>Simple Recursion

  \label{sssec:datatype-simple-recursion}\<close>

text \<open>

Natural numbers are the simplest example of a recursive type:

\<close>

    datatype nat = Zero | Succ nat

text \<open>

\noindent

Lists were shown in the introduction. Terminated lists are a variant that

stores a value of type @{typ 'b} at the very end:

\<close>

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

subsubsection \<open>Mutual Recursion

  \label{sssec:datatype-mutual-recursion}\<close>

text \<open>

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

\<close>

    datatype even_nat = Even_Zero | Even_Succ odd_nat

    and odd_nat = Odd_Succ even_nat

text \<open>

\noindent

Arithmetic expressions are defined via terms, terms via factors, and factors via

expressions:

\<close>

    datatype ('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 \<open>Nested Recursion

  \label{sssec:datatype-nested-recursion}\<close>

text \<open>

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

\<close>

    datatype 'a btree =

      BNode 'a "'a btree option" "'a btree option"

text \<open>

\noindent

Not all nestings are admissible. For example, this command will fail:

\<close>

    datatype 'a wrong = W1 | W2 (*<*)'a

    typ (*>*)"'a wrong \<Rightarrow> 'a"

text \<open>

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

\<close>

    datatype ('a, 'b) fun_copy = Fun "'a \<Rightarrow> 'b"

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

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

text \<open>

\noindent

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

\<close>

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

text \<open>

\noindent

And so is the definition of hereditarily finite sets:

\<close>

    datatype hfset = HFSet "hfset fset"

text \<open>

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

\<close>

    datatype 'a pow_list = PNil 'a (*<*)'a

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

text \<open>

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

\<close>

subsubsection \<open>Auxiliary Constants

  \label{sssec:datatype-auxiliary-constants}\<close>

text \<open>

The @{command datatype} command introduces various constants in addition to

the constructors. With each datatype are associated set functions, a map

function, a predicator, 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}:

\<close>

(*<*)

    no_translations

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

      "[x]" == "x # []"

    no_notation

      Nil ("[]") and

      Cons (infixr "#" 65)

    hide_type list

    hide_const Nil Cons case_list hd tl set map list_all2 rec_list size_list list_all

    context early

    begin

(*>*)

    datatype (set: 'a) list =

      null: Nil

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

    for

      map: map

      rel: list_all2

      pred: list_all

    where

      "tl Nil = Nil"

text \<open>

\noindent

The types of the constants that appear in the specification are listed below.

\medskip

\begin{tabular}{@ {}ll@ {}}

Constructors: &

  @{text "Nil :: 'a list"} \\

&

  @{text "Cons :: 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"} \\

Discriminator: &

  @{text "null :: 'a list \<Rightarrow> bool"} \\

Selectors: &

  @{text "hd :: 'a list \<Rightarrow> 'a"} \\

&

  @{text "tl :: 'a list \<Rightarrow> 'a list"} \\

Set function: &

  @{text "set :: 'a list \<Rightarrow> 'a set"} \\

Map function: &

  @{text "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"} \\

Relator: &

  @{text "list_all2 :: ('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.

In the example, 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:

\<close>

(*<*)

    end

(*>*)

    datatype ('a, 'b) prod (infixr "*" 20) = Pair 'a 'b

text \<open>\blankline\<close>

    datatype (set: 'a) list =

      null: Nil ("[]")

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

    for

      map: map

      rel: list_all2

      pred: list_all

text \<open>

\noindent

Incidentally, this is how the traditional syntax can be set up:

\<close>

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

text \<open>\blankline\<close>

    translations

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

      "[x]" == "x # []"

subsection \<open>Command Syntax

  \label{ssec:datatype-command-syntax}\<close>

subsubsection \<open>\keyw{datatype}

  \label{sssec:datatype}\<close>

text \<open>

\begin{matharray}{rcl}

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

\end{matharray}

@{rail \<open>

  @@{command datatype} target? @{syntax dt_options}? @{syntax dt_spec}

  ;

  @{syntax_def dt_options}: '(' ((@{syntax plugins} | 'discs_sels') + ',') ')'

  ;

  @{syntax_def plugins}: 'plugins' ('only' | 'del') ':' (name +)

  ;

  @{syntax_def dt_spec}: (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') \<newline>

     @{syntax map_rel_pred}? (@'where' (prop + '|'))? + @'and')

  ;

  @{syntax_def map_rel_pred}: @'for' ((('map' | 'rel' | 'pred') ':' name) +)

\<close>}

\medskip

\noindent

The @{command datatype} 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 a combination of the following

options:

\begin{itemize}

\setlength{\itemsep}{0pt}

\item

The @{text plugins} option indicates which plugins should be enabled

(@{text only}) or disabled (@{text del}). By default, all plugins are enabled.

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

\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. If discriminators are enabled (cf.\ the

@{text "discs_sels"} option) but no name is supplied, the default 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. The same selector name can be reused for

arguments to several constructors as long as the arguments share the same type.

If selectors are enabled (cf.\ the @{text "discs_sels"} option) but no name is

supplied, the default name is @{text un_C\<^sub>ji}.

\<close>

subsubsection \<open>\keyw{datatype_compat}

  \label{sssec:datatype-compat}\<close>

text \<open>

\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 and invokes the old-style plugins. For example:

\<close>

    datatype_compat even_nat odd_nat

text \<open>\blankline\<close>

    ML \<open>Old_Datatype_Data.get_info @{theory} @{type_name even_nat}\<close>

text \<open>

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

The command is sometimes useful when migrating from the old datatype package to

the new one.

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}, @{text compat_tree.inducts}, and

@{text compat_tree.rec}). These theorems should be identical to the ones

generated by the old datatype package, \emph{up to the order of the

premises}---meaning that the subgoals generated by the @{text induct} or

@{text induction} method may be in a different order than before.

\item All types through which recursion takes place must be new-style datatypes

or the function type.

\end{itemize}

\<close>

subsection \<open>Generated Constants

  \label{ssec:datatype-generated-constants}\<close>

text \<open>

Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"} with $m$ 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}

\end{tabular}

\medskip

\noindent

The discriminators and selectors are generated only if the @{text "discs_sels"}

option is enabled or if names are specified for discriminators or selectors.

The set functions, map function, predicator, and relator are generated only if $m > 0$.

In addition, some of the plugins introduce their own constants

(Section~\ref{sec:selecting-plugins}). 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.

\<close>

subsection \<open>Generated Theorems

  \label{ssec:datatype-generated-theorems}\<close>

text \<open>

The characteristic theorems generated by @{command datatype} 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 by issuing the command

\keyw{print_theorems} immediately after the datatype definition. This list

includes theorems produced by plugins (Section~\ref{sec:selecting-plugins}),

but normally excludes low-level theorems that reveal internal constructions.

To make these accessible, add the line

\<close>

    declare [[bnf_internals]]

(*<*)

    declare [[bnf_internals = false]]

(*>*)

subsubsection \<open>Free Constructor Theorems

  \label{sssec:free-constructor-theorems}\<close>

(*<*)

    consts nonnull :: 'a

(*>*)

text \<open>

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

The @{text "[code]"} attribute is set by the @{text code} plugin

(Section~\ref{ssec:code-generator}).

\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{case_distrib}\rm:] ~ \\

@{thm list.case_distrib[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]} \\

The @{text "[code]"} attribute is set by the @{text code} plugin

(Section~\ref{ssec:code-generator}).

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

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

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

The @{text "[simp]"} attribute is exceptionally omitted for datatypes equipped

with a single nullary constructor, because a property of the form

@{prop "x = C"} is not suitable as a simplification rule.

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

These properties are missing for @{typ "'a list"} because there is only one

proper discriminator. If the datatype had been introduced with a second

discriminator called @{const nonnull}, they would have read as follows: \\[\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]}

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

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

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

\end{description}

\end{indentblock}

\noindent

In addition, equational versions of @{text t.disc} are registered with the

@{text "[code]"} attribute. The @{text "[code]"} attribute is set by the

@{text code} plugin (Section~\ref{ssec:code-generator}).

\<close>

subsubsection \<open>Functorial Theorems

  \label{sssec:functorial-theorems}\<close>

text \<open>

The functorial theorems are generated for type constructors with at least

one live type argument (e.g., @{typ "'a list"}). They 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,

the predicator, or the relator:

\begin{indentblock}

\begin{description}

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

@{thm list.case_transfer[no_vars]} \\

This property is generated by the @{text transfer} plugin

(Section~\ref{ssec:transfer}).

%The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin

%(Section~\ref{ssec:transfer}).

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

This property is missing for @{typ "'a list"} because there is no common

selector to all constructors. \\

The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin

(Section~\ref{ssec:transfer}).

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

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

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

The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin

(Section~\ref{ssec:transfer}) .

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

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

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

The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin

(Section~\ref{ssec:transfer}).

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

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

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

The @{text "[code]"} attribute is set by the @{text code} plugin

(Section~\ref{ssec:code-generator}).

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

The @{text "[code]"} attribute is set by the @{text code} plugin

(Section~\ref{ssec:code-generator}).

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

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

@{thm list.pred_inject(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]}

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

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

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

\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

@{text "[code]"} attribute is set by the @{text code} plugin

(Section~\ref{ssec:code-generator}).

The second subgroup consists of more abstract properties of the set functions,

the map function, the predicator, 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{map_comp}\rm:] ~ \\

@{thm list.map_comp[no_vars]}

\item[@{text "t."}\hthm{map_cong0}\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_pred}\rm:] ~ \\

@{thm list.map_cong_pred[no_vars]}

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

@{thm list.map_cong_simp[no_vars]}

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

@{thm list.map_id0[no_vars]}

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

@{thm list.map_id[no_vars]}

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

@{thm list.map_ident[no_vars]}

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

@{thm list.map_transfer[no_vars]} \\

The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin

(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.

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

@{thm list.pred_cong[no_vars]}

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

@{thm list.pred_cong_simp[no_vars]}

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

@{thm list.pred_map[no_vars]}