\lettrine[nindent=0ex]P{olemically} speaking, formal proofs are irrelevant -- only their existence matters. Once a proposition has been proved, and the proof has been checked by the theorem prover, this is all that matters to a reader interested in just the assurance that the proof is fine.

The same cannot be said for definitions and theorems: The machine cannot check whether these really state what the author claims them to state! Therefore, this appendix reproduces the Isabelle formulation of the main theorems of this thesis, together with all definitions required to understand them.

The intention is to enable the reader to check the formal results precisely, without reaching out for the actual Isabelle sources. Naturally, this does not protect against malice on the side of the author. To rule that out, you’d not only have to process the Isabelle sources yourself, but also verify each line of code for tricks such as introducing new axioms, using other unchecked commands or messing with the parser and printer to obtain misleading results. There is a certain level of assurance that this is not the case, as my work has been accepted in the Archive of Formal Proofs \cite{launchbury-isa,arity-afp}.

\pagebreak

The listings reproduce the Isabelle code as typed, and hence do not benefit from Isabelle’s pretty-printing abilities; the name of the Isabelle theory file that contains the code is printed next to the listing, unless the previous listing is from the same file.

For a few functions, not the actual, technical definition is given here, but rather a proposition involving the function that completely describes it. In these cases, the definition that one intuitively wants is not accepted by the definitory command (e.g.\ using \isa{\isacommand{definition}} to define a function in HOLCF’s type of continuous functions) or the proof obligations produced by such a command are hard to discharge, and a different formulation is easier to work with, and can later be shown to be equivalent to the desired formulation (e.g.\ with \isa{\isacommand{nominal{\isacharunderscore}function}}’s equivariance obligations). Also, in the cases where I use locales to abstract over similar definitions, reproducing the locale interface, the abstract function definition and the actual instantiation of the locale would obscure the view, so I describe the resulting function as if I had defined it directly.

In the end, in Isabelle/HOL, it does not matter whether a function is define with one set of equations or another: As long as they fully describe the function (i.e.\ if they are exhaustive and terminating), the resulting constant is identical for all purposes.

\section{Terms}

The definition of the type of terms requires that the type of variables are defined first. In order to use the Nominal machinery, I need to declare that type using the \isa{\isacommand{atom{\isacharunderscore}decl}} command. To us, the resulting type is abstract, and all that we know about it is that it is countably infinite:
\isainput{def-var}

Based on that, I define our type of lambda expressions is defined as follows. See \cref{sec:using-nominal} for an explanation of this construction:
\isainput{exp-definition}

The function \isa{atom} is provided by the Nominal package. It embeds our type \isa{var} into the type \isa{atom} encompassing all possible name types, but as we use only one such type in our formalisation, one can assume \isa{var} and \isa{atom} to be isomorphic.

%The function \isa{fv} returns all atoms of one such type occuring in an expression or similar object; in this development, this will always be the type \isa{var}.
%\isainput{def-fv}

Only lambda abstractions and Booleans are considered to be values, as characterised by the following function:
\isainput{def-isval}

The type \isa{heap} that occurs in some of the listing is but a type abbreviation:
\isainput{def-heap}

The domain of such a heap is the set of variables that are bound to some expression:
\isainput{def-domA}

As explained in \cref{sec:using-nominal}, the type \isa{assn} is but a work-around, and we’d really like the \isa{Let} constructor to have such an \isa{heap} as the parameter. Therefore, I define a conversion function and define \isa{Let} in terms of that; from then on, \isa{LetA} is not used:
\isainput{def-heapToAssn}
\isainput{def-Let}


We will use substitution of one variable for another, in variables, expressions and heaps. For variables, this is easily defined:
\isainput{def-subst-var}

For expressions and heaps, due to them being mutually recursive, the definition is more involved. In particular, I had to jump through a few hoops to be able to discharge the proof obligations produced by \isa{\isacommand{nominal{\isacharunderscore}function}}; the complex \isa{default} and \isa{invariant} annotations were required for that:
\isainput{def-subst}


\section{Semantics}

\subsection{Natural semantics}

Launchbury’s natural semantics is defined as an inductive predicate:
\isainput{def-launchbury}

The denotational semantics maps expressions to a denotational domain, which is defined using the HOLCF machinery:
\isainput{def-value}

\subsection{Small-step semantics}

Sestoft's mark-1 abstract machine is defined via the \isa{\isacommand{inductive}} command, which is convenient even if there is no recursion. I also introduce some nicer syntax for the transitive reflexive closure.
\isainput{def-step}

The type \isa{conf} in the signature of \isa{step} is also but a type synonym:
\isainput{def-conf}

\subsection{Denotational semantics}

The denotational semantics is defined by instantiating a more abstract locale, as explained in \cref{sec:abstracting-over-semantics}. The following equations fully describe the result, though.
\isainput{def-esem-syntax}
\isainput{def-esem}

Towards defining the recursive heap semantics, the function \isa{evalHeap} maps a given evaluation function (e.g.\ the \isa{HSem} above) over the heap, producing a function from variable names to values. As this definition is yet abstract in the choices of expression and value types, its signature contains lots of type variables:
\isainput{def-evalheap}

I introduce nicer syntax for this operation and then define the heap semantics using the fixed-point operator from HOLCF:
\isainput{def-hsem}


The following listings will mention the restriction of an environment to a set, which is defined as follows:
\isainput{def-env-restr}


\section{Correctness and adequacy theorems}

The main results from \cref{ch:launchbury} are the correctness and adequacy of the natural semantics with regard to the standard denotational semantics.

The correctness theorem (\cref{thm:thm2}) is as follows. Note that the assumption of closedness is written out explicitly.
\isainput{thm-correctness}

The adequacy theorem (\cref{thm:adequacy}) corresponds even closer to the original formulation. Note that the set \isa{S} of variables to avoid is unconstrained, i.e.\ the theorem can produce a judgement for every choice of \isa{S}. This only works because the set is represented as a list in the formalisation, otherwise finiteness of the set would have to be required explicitly.
\isainput{thm-adequacy}

\section{Call Arity}

For the formalisation of \cref{ch:provingcallarity}, I introduce a few custom data types.

\subsection{Arities}

I define the type \isa{Arity} as an isomorphic copy the type of naturals:
\isainput{def-arity}

Having a dedicated type for arities allows me to define the partial order required here. Note that it swaps the arguments of $\le$:
\isainput{def-arity-order}

On the other hand, this additional abstraction layers requires me to lift a few definitions from the naturals, in particular zero and the predecessor and successor functions.  The latter are defined in two steps: First lifting the function to \isa{Arity}, and then into \isa{HOLCF}’s type of continuous functions:
\isainput{def-arity-zero}
\isainput{def-arity-inc-pre}
\isainput{def-arity-inc}

The type \isa{AEnv} of arity environments is simply \isa{var {\isasymRightarrow} $Arity_\bot$}. The following functions provide some useful operations on such and similar environments: The domain of an environments, singleton environments, and removal of one entry.
\isainput{def-edom}
\isainput{def-esing}
\isainput{def-env-delete}

\subsection{Co-call graphs}

The type \isa{CoCalls} of co-call Graphs is defined to be isomorphic to the set of symmetric relations on \isa{var}:
\isainput{def-cocalls}

The relevant operations are the calculation of the field of the relation, the member relation, the removal of a node from the graph,  the restriction to a set, the Cartesian products and the set of neighbours.
\isainput{def-ccfield}
\isainput{def-incc}
\isainput{def-ccdelete}
\isainput{def-ccrestr}
\isainput{def-ccprod}
\isainput{def-ccsquare}
\isainput{def-ccneighbors}



\subsection{The Call Arity analysis}

The equations for the arity analysis are mutually recursive with a few auxiliary functions to handle the heap.
\isainput{def-aexp}
\isainput{def-ccexp}

A superscripted $\bot$ indicates that the function is lifted to $\isa{Arity}_\bot$:
\isainput{def-aexp-bot}
\goodbreak
\isainput{def-ccexp-bot}

The function \isa{Afix}, building on \isa{ABinds} and \isa{ABind}, implements the fix-pointing in the arity analysis:
\isainput{def-abind}
\isainput{def-abinds}
\isainput{def-afix}

In the non-recursive case, the function \isa{ABind{\isacharunderscore}nonrec} is used; this is where the arity analysis depends on the co-call cardinality analysis.
\isainput{def-abind-nonrec}


The fixed-point calculation of the co-call-graph is defined similarly:
\isainput{def-ccbind}
\isainput{def-ccbinds}
\isainput{def-ccbindsextra}
\isainput{def-ccfix}


Finally, the actual transformation, which uses the arity analysis, is
\isainput{def-transform}
where the auxiliary function \isa{map{\isacharunderscore}transform} applies a transformation of type \isa{Arity {\isasymRightarrow} exp {\isasymRightarrow}} to an Arity environment and a \isa{heap}:
\isainput{def-lift-transform}
\isainput{def-map-transform}

\subsection{Call Arity theorems}

The Call Arity transformation is functionally correct, i.e. does not change the semantics (\cref{thm:call-arity-correct}):
\isainput{arity-transformation-correct}

The main safety theorem for Call Arity (\cref{thm:cocallsafety}) reads as follows:
\isainput{call-artiy-safe-end2end}