<commit_before>(*<*)
theory Types_and_funs
imports Main
begin
(*>*)
text{*
\vspace{-5ex}
\section{Type and function definitions}

Type synonyms are abbreviations for existing types, for example
*}

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}

The general form of a datatype definition looks like this:
\begin{quote}
\begin{tabular}{@ {}rclcll}
\isacom{datatype} @{text "('a\<^isub>1,\<dots>,'a\<^isub>n)t"}
     & = & $C_1 \ @{text"\""}\tau_{1,1}@{text"\""} \dots @{text"\""}\tau_{1,n_1}@{text"\""}$ \\
     & $|$ & \dots \\
     & $|$ & $C_k \ @{text"\""}\tau_{k,1}@{text"\""} \dots @{text"\""}\tau_{k,n_k}@{text"\""}$
\end{tabular}
\end{quote}
It introduces the constructors \
$C_i :: \tau_{i,1}\Rightarrow \cdots \Rightarrow \tau_{i,n_i} \Rightarrow$~@{text "('a\<^isub>1,\<dots>,'a\<^isub>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 structural induction rule: to show
$P~x$ for all $x$ of type @{text "('a\<^isub>1,\<dots>,'a\<^isub>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} =$~@{text "('a\<^isub>1,\<dots>,'a\<^isub>n)t"}.
Distinctness and injectivity are applied automatically by @{text auto}
and other proof methods. Induction must be applied explicitly.

Datatype values can be taken apart with case-expressions, for example
\begin{quote}
\noquotes{@{term[source] "(case xs of [] \<Rightarrow> 0 | x # _ \<Rightarrow> Suc x)"}}
\end{quote}
just like in functional programming languages. Case expressions
must be enclosed in parentheses.

As an example, consider binary trees:
*}

datatype 'a tree = Tip | Node  "'a tree"  'a  "'a tree"

text{* with a mirror function: *}

fun mirror :: "'a tree \<Rightarrow> 'a tree" where
"mirror Tip = Tip" |
"mirror (Node l a r) = Node (mirror r) a (mirror l)"

text{* The following lemma illustrates induction: *}

lemma "mirror(mirror t) = t"
apply(induction t)

txt{* yields
@{subgoals[display]}
The induction step contains two induction hypotheses, one for each subtree.
An application of @{text auto} finishes the proof.

A very simple but also very useful datatype is the predefined
@{datatype[display] option}
Its sole purpose is to add a new element @{const None} to an existing
type @{typ 'a}. To make sure that @{const None} is distinct from all the
elements of @{typ 'a}, you wrap them up in @{const Some} and call
the new type @{typ"'a option"}. A typical application is a lookup function
on a list of key-value pairs, often called an association list:
*}
(*<*)
apply auto
done
(*>*)
fun lookup :: "('a * 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" where
"lookup [] x = None" |
"lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"

text{*
Note that @{text"\<tau>\<^isub>1 * \<tau>\<^isub>2"} is the type of pairs, also written @{text"\<tau>\<^isub>1 \<times> \<tau>\<^isub>2"}.

\subsection{Definitions}

Non recursive functions can be defined as in the following example:
*}

definition sq :: "nat \<Rightarrow> nat" where
"sq n = n * n"

text{* Such definitions do not allow pattern matching but only
@{text"f x\<^isub>1 \<dots> x\<^isub>n = t"}, where @{text f} does not occur in @{text t}.

\subsection{Abbreviations}

Abbreviations are similar to definitions:
*}

abbreviation sq' :: "nat \<Rightarrow> nat" where
"sq' n == n * n"

text{* The key difference is that @{const sq'} is only syntactic sugar:
@{term"sq' t"} is replaced by \mbox{@{term"t*t"}} after parsing, and every
occurrence of a term @{term"u*u"} is replaced by \mbox{@{term"sq' u"}} before
printing.  Internally, @{const sq'} does not exist.  This is also the
advantage of abbreviations over definitions: definitions need to be expanded
explicitly (see \autoref{sec:rewr-defs}) whereas abbreviations are already
expanded upon parsing. However, abbreviations should be introduced sparingly:
if abused, they can lead to a confusing discrepancy between the internal and
external view of a term.<commit_msg>added pairs<commit_after>(*<*)
theory Types_and_funs
imports Main
begin
(*>*)
text{*
\vspace{-5ex}
\section{Type and function definitions}

Type synonyms are abbreviations for existing types, for example
*}

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}

The general form of a datatype definition looks like this:
\begin{quote}
\begin{tabular}{@ {}rclcll}
\isacom{datatype} @{text "('a\<^isub>1,\<dots>,'a\<^isub>n)t"}
     & = & $C_1 \ @{text"\""}\tau_{1,1}@{text"\""} \dots @{text"\""}\tau_{1,n_1}@{text"\""}$ \\
     & $|$ & \dots \\
     & $|$ & $C_k \ @{text"\""}\tau_{k,1}@{text"\""} \dots @{text"\""}\tau_{k,n_k}@{text"\""}$
\end{tabular}
\end{quote}
It introduces the constructors \
$C_i :: \tau_{i,1}\Rightarrow \cdots \Rightarrow \tau_{i,n_i} \Rightarrow$~@{text "('a\<^isub>1,\<dots>,'a\<^isub>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 structural induction rule: to show
$P~x$ for all $x$ of type @{text "('a\<^isub>1,\<dots>,'a\<^isub>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} =$~@{text "('a\<^isub>1,\<dots>,'a\<^isub>n)t"}.
Distinctness and injectivity are applied automatically by @{text auto}
and other proof methods. Induction must be applied explicitly.

Datatype values can be taken apart with case-expressions, for example
\begin{quote}
\noquotes{@{term[source] "(case xs of [] \<Rightarrow> 0 | x # _ \<Rightarrow> Suc x)"}}
\end{quote}
just like in functional programming languages. Case expressions
must be enclosed in parentheses.

As an example, consider binary trees:
*}

datatype 'a tree = Tip | Node  "'a tree"  'a  "'a tree"

text{* with a mirror function: *}

fun mirror :: "'a tree \<Rightarrow> 'a tree" where
"mirror Tip = Tip" |
"mirror (Node l a r) = Node (mirror r) a (mirror l)"

text{* The following lemma illustrates induction: *}

lemma "mirror(mirror t) = t"
apply(induction t)

txt{* yields
@{subgoals[display]}
The induction step contains two induction hypotheses, one for each subtree.
An application of @{text auto} finishes the proof.

A very simple but also very useful datatype is the predefined
@{datatype[display] option}
Its sole purpose is to add a new element @{const None} to an existing
type @{typ 'a}. To make sure that @{const None} is distinct from all the
elements of @{typ 'a}, you wrap them up in @{const Some} and call
the new type @{typ"'a option"}. A typical application is a lookup function
on a list of key-value pairs, often called an association list:
*}
(*<*)
apply auto
done
(*>*)
fun lookup :: "('a * 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" where
"lookup [] x = None" |
"lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"

text{*
Note that @{text"\<tau>\<^isub>1 * \<tau>\<^isub>2"} is the type of pairs, also written @{text"\<tau>\<^isub>1 \<times> \<tau>\<^isub>2"}.
Pairs can be taken apart either by pattern matching (as above) or with the
projection functions @{const fst} and @{const snd}: @{thm fst_conv} and @{thm snd_conv}. Tuples are simulated by pairs nested to the right: @{term"(a,b,c)"}
abbreviates @{text"(a, (b, c))"} and @{text "\<tau>\<^isub>1 \<times> \<tau>\<^isub>2 \<times> \<tau>\<^isub>3"} abbreviates
@{text "\<tau>\<^isub>1 \<times> (\<tau>\<^isub>2 \<times> \<tau>\<^isub>3)"}.

\subsection{Definitions}

Non recursive functions can be defined as in the following example:
*}

definition sq :: "nat \<Rightarrow> nat" where
"sq n = n * n"

text{* Such definitions do not allow pattern matching but only
@{text"f x\<^isub>1 \<dots> x\<^isub>n = t"}, where @{text f} does not occur in @{text t}.

\subsection{Abbreviations}

Abbreviations are similar to definitions:
*}

abbreviation sq' :: "nat \<Rightarrow> nat" where
"sq' n == n * n"

text{* The key difference is that @{const sq'} is only syntactic sugar:
@{term"sq' t"} is replaced by \mbox{@{term"t*t"}} after parsing, and every
occurrence of a term @{term"u*u"} is replaced by \mbox{@{term"sq' u"}} before
printing.  Internally, @{const sq'} does not exist.  This is also the
advantage of abbreviations over definitions: definitions need to be expanded
explicitly (see \autoref{sec:rewr-defs}) whereas abbreviations are already
expanded upon parsing. However, abbreviations should be introduced sparingly:
if abused, they can lead to a confusing discrepancy between the internal and
external view of a term.
{'fraction_non_alphanumeric': 0.15979166666666667, 'fraction_numerical': 0.005416666666666667, 'mean_word_length': 4.5561342592592595, 'pattern_counts': {'":': 0, '<': 85, '<?xml version=': 0, '>': 85, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4211740', 'n_tokens_mistral': 3423, 'n_tokens_neox': 3283, 'n_words': 1250}