Theory Types_and_funs
theory Types_and_funs
imports Main
begin
text‹
\vspace{-5ex}
\section{Type and Function Definitions}
Type synonyms are abbreviations for existing types, for example
\index{string@‹string›}›
type_synonym string = "char list"
text‹
Type synonyms are expanded after parsing and are not present in internal representation and output. They are mere conveniences for the reader.
\subsection{Datatypes}
\label{sec:datatypes}
The general form of a datatype definition looks like this:
\begin{quote}
\begin{tabular}{@ {}rclcll}
\indexed{\isacom{datatype}}{datatype} ‹('a⇩1,…,'a⇩n)t›
& = & $C_1 \ ‹"›\tau_{1,1}‹"› \dots ‹"›\tau_{1,n_1}‹"›$ \\
& $|$ & \dots \\
& $|$ & $C_k \ ‹"›\tau_{k,1}‹"› \dots ‹"›\tau_{k,n_k}‹"›$
\end{tabular}
\end{quote}
It introduces the constructors \
$C_i :: \tau_{i,1}\Rightarrow \cdots \Rightarrow \tau_{i,n_i} \Rightarrow$~‹('a⇩1,…,'a⇩n)t› \ and expresses that any value of this type is built from these constructors in a unique manner. Uniqueness is implied by the following
properties of the constructors:
\begin{itemize}
\item \emph{Distinctness:} $C_i\ \ldots \neq C_j\ \dots$ \quad if $i \neq j$
\item \emph{Injectivity:}
\begin{tabular}[t]{l}
$(C_i \ x_1 \dots x_{n_i} = C_i \ y_1 \dots y_{n_i}) =$\\
$(x_1 = y_1 \land \dots \land x_{n_i} = y_{n_i})$
\end{tabular}
\end{itemize}
The fact that any value of the datatype is built from the constructors implies
the \concept{structural induction}\index{induction} rule: to show
$P~x$ for all $x$ of type ‹('a⇩1,…,'a⇩n)t›,
one needs to show $P(C_i\ x_1 \dots x_{n_i})$ (for each $i$) assuming
$P(x_j)$ for all $j$ where $\tau_{i,j} =$~‹('a⇩1,…,'a⇩n)t›.
Distinctness and injectivity are applied automatically by ‹auto›
and other proof methods. Induction must be applied explicitly.
Like in functional programming languages, datatype values can be taken apart
with case expressions\index{case expression}\index{case expression@‹case ... of›}, for example
\begin{quote}
\noquotes{@{term[source] "(case xs of [] ⇒ 0 | x # _ ⇒ Suc x)"}}
\end{quote}
Case expressions must be enclosed in parentheses.
As an example of a datatype beyond \<^typ>‹nat› and ‹list›, consider binary trees:
›