Theory ETTS_Theory
section‹ETTS and ERA›
theory ETTS_Theory
imports ETTS_Introduction
begin
subsection‹Background›
text‹
In this section, we describe our implementation of the prototype software
framework ETTS that offers the integration of Types-To-Sets with the
Isabelle/Isar infrastructure and full automation of the application of
the ERA under favorable conditions.
The design of the framework rests largely on our
interpretation of several ideas expressed by the authors
of \<^cite>‹"kuncar_types_2019"› and \<^cite>‹"immler_smooth_2019"›.
It has already been mentioned that the primary functionality of the ETTS
is available via the Isabelle/Isar
\<^cite>‹"bertot_isar_1999" and "wenzel_isabelleisar_2007"›
commands @{command tts_context}, @{command tts_lemmas} and @{command tts_lemma}.
There also exist secondary commands aimed at resolving certain specific
problems that one may encounter during relativization:
@{command tts_register_sbts} and @{command tts_find_sbts}.
More specifically, these commands provide means for using transfer rules
stated in a local context during the step of the ERA that is similar
to step 5 of the RA. The functionality of these commands is
explained in more detail in subsection \ref{sec:sbts} below.
It is important to note that the description of the ETTS presented
in this subsection is only a simplified model
of its programmatic implementation in
\textit{Isabelle/ML} \<^cite>‹"milner_definition_1997" and "wenzel_isabelle/isar_2019"›.
›
subsection‹Preliminaries›
text‹
The ERA is an extension of the RA that
provides means for the automation of a design pattern similar
to the one that was proposed in \<^cite>‹"immler_smooth_2019"›,
as well as several additional steps for pre-processing of the input
and post-processing of the result of the relativization.
In a certain restricted sense the ERA can be seen as
a localized form of the RA, as it provides additional infrastructure
aimed specifically at making the relativization of theorems stated in the
context of Isabelle's \textit{locales}
\<^cite>‹"kammuller_locales_1999" and "berardi_locales_2004" and "ballarin_locales_2014"›
more convenient.
In what follows, assume the existence of an underlying well-formed
theory $D$ that contains all definitional axioms that appear in the
standard library of Isabelle/HOL.
If \mbox{$\Gamma \vdash {}_{\alpha}(\beta \approx U)_{\mathsf{Rep}}^{\mathsf{Abs}}$}
and $\beta, U_{\alpha\ \mathsf{set}}, \mathsf{Rep}_{\beta\rightarrow\alpha}, \mathsf{Abs}_{\alpha\rightarrow\beta} \in \Gamma$,
then the 4-tuple $(U_{\alpha\ \mathsf{set}}, \beta, \mathsf{Rep}_{\beta\rightarrow\alpha}, \mathsf{Abs}_{\alpha\rightarrow\beta})$,
will be referred to as a \textit{relativization isomorphism} (RI) \textit{with respect to} $\Gamma$ (or RI, if $\Gamma$ can be inferred).
Given the RI $(U_{\alpha\ \mathsf{set}},\beta,\mathsf{Rep}_{\beta\rightarrow\alpha},\mathsf{Abs}_{\alpha\rightarrow\beta})$,
the term $U_{\alpha\ \mathsf{set}}$ will be referred to as
the \textit{set associated with the RI}, $\beta$ will be referred to as
the \textit{type variable associated with the RI},
$\mathsf{Rep}_{\beta\rightarrow\alpha}$ will be referred to as
the \textit{representation associated with the RI} and $\mathsf{Abs}_{\alpha\rightarrow\beta}$
will be referred to as the \textit{abstraction associated with the RI}.
Moreover, any typed term variable $T_{\alpha\rightarrow\beta\rightarrow\mathbb{B}}$
such that $\Gamma \vdash T = (\lambda x\ y.\ \mathsf{Rep}\ y = x)$
will be referred to as the \textit{transfer relation associated with the RI}.
$\Gamma \vdash Domainp\ T = (\lambda x.\ x \in U)$ that holds for this transfer
relation will be referred to as the \textit{transfer domain rule associated
with the RI}, $\Gamma \vdash bi\_ unique\ T$ and $\Gamma \vdash right\_ total\ T$
will be referred to as the \textit{side conditions associated with the RI}.
For brevity, the abbreviation
$\mathsf{dbr}[T_{\alpha\rightarrow\beta\rightarrow\mathbb{B}},U_{\alpha\ \mathsf{set}}]$
will be used to mean that $Domainp\ T = (\lambda x.\ x \in U)$, $bi\_ unique\ T$
and $right\_ total\ T$ for any $\alpha$, $\beta$,
$T_{\alpha\rightarrow\beta\rightarrow\mathbb{B}}$ and $U_{\alpha\ \mathsf{set}}$.
›
subsection‹Set-based terms and their registration\label{sec:sbts}›
text‹
Perhaps, one of the most challenging aspects of the automation of the
relativization process is related to the application of Transfer during
step 5 of the RA: a suitable transfer rule for a given constant-instance
may exist only under non-conventional side conditions:
an important example that showcases this issue is the built-in constant
$\varepsilon$ (see \<^cite>‹"kuncar_types_2019"› and \<^cite>‹"immler_smooth_2019"›
for further information).
Unfortunately, the ETTS does not offer a fundamental solution to this problem:
the responsibility for providing suitable transfer rules for the application
of the ERA remains at the discretion of the user.
Nonetheless, the ETTS does provide
additional infrastructure that may improve the user experience when
dealing with the transfer rules that can only be conveniently stated in
an explicitly relativized local context (usually a relativized
locale): a common problem that was already explored in
\<^cite>‹"immler_smooth_2019"›.
The authors of \<^cite>‹"immler_smooth_2019"› choose to perform the relativization
of theorems that stem from their specifications in a locale context
from within another dedicated relativized locale context.
The relativized operations that are represented either by the locale parameters
of the relativized locale or remain overloaded constants associated with
a given class constraint are lifted to the type variables associated with the
RIs that are used for the application of a variant of the relativization
algorithm. This variant includes a step during which the
variables introduced during unoverloading are substituted (albeit implicitly)
for the terms that represent the lifted locale parameters and constants.
The additional infrastructure and the additional step
are needed, primarily, for the relativization of the constants
whose transfer rules can only be stated conveniently in the context
of the relativized locale.
A similar approach is used in the ETTS. However, instead of explicitly
declaring the lifted constants in advance of the application of the RA,
the user is expected to perform the registration of the so-called
\textit{set-based term} (sbterm) for each term of interest that
is a relativization of a given concept.
The inputs to the algorithm that is associated with the registration of the
sbterms are a context $\Gamma$, a term $t : \bar{\alpha}\ K$
($K$, applied using a postfix notation, contains all information about
the type constructors of the type $\bar{\alpha}\ K$) and a
sequence of $n$ distinct typed variables $\bar{U}$ with distinct types of the
form ${\alpha\ \mathsf{set}}$, such that $\bar{\alpha}$ is also of length $n$,
all free variables and free type variables that occur in
$t : \bar{\alpha}\ K$ also appear free in $\Gamma$
and $\bar{U}_i : \bar{\alpha}_i\ \mathsf{set}$ for all $i$,
$1 \leq i \leq n$.
Firstly, a term
$
\exists b.
\ R\left[\bar{A}\right]_{\bar{\alpha}\ K \rightarrow \bar{\beta}\ K\rightarrow \mathbb{B}}\ t\ b
$
is formed, such
that $R\left[\bar{A}\right]$ is a parametricity relation associated with
some type $\bar{\gamma}\ K$ for $\bar{\gamma}$ of length $n$, such that the sets
of the elements of $\bar{\alpha}$, $\bar{\beta}$ and $\bar{\gamma}$ are pairwise
disjoint, $\bar{A}$ and $\bar{\beta}$ are both of length $n$,
the elements of $\bar{A}$, $\bar{\beta}$ and $\bar{\gamma}$
are fresh for $\Gamma$ and
$\bar{A}_i : \bar{\alpha}_i\rightarrow \bar{\beta}_i\rightarrow\mathbb{B}$
for all $i$ such that $1 \leq i \leq n$. Secondly, the context $\Gamma'$ is built
incrementally starting from $\Gamma$ by adding the formulae
$\mathsf{dbr}[\bar{A}_i, \bar{U}_i]$
for each $i$ such that $1 \leq i \leq n$.
The term presented above serves as a goal that is meant to be
discharged by the user in $\Gamma'$, resulting in the deduction
\[
\Gamma \vdash
\mathsf{dbr}[?\bar{A}_i, \bar{U}_i] \longrightarrow
\exists b.
\ R\left[?\bar{A}\right]_{\bar{\alpha}\ K \rightarrow ?\bar{\beta}\ K\rightarrow \mathbb{B}}\ t\ b
\]
(the index $i$ is distributed over $n$)
after the export to the context $\Gamma$.
Once the proof is completed, the result is registered in the so-called
\textit{sbt-database} allowing a lookup of such results by the
sbterm $t$ (the terms and results are allowed to morph
when the lookup is performed from within a context different
from $\Gamma$ \<^cite>‹"kauers_context_2007"›).
›
subsection‹Parameterization of the ERA\label{sec:par-ERA}›
text‹
Assuming the existence of some context $\Gamma$, the ERA is parameterized by
the \textit{RI specification}, \textit{the sbterm specification},
the \textit{rewrite rules for the set-based theorem},
the \textit{known premises for the set-based theorem},
the \textit{specification of the elimination of premises
in the set-based theorem} and
the \textit{attributes for the set-based theorem}.
A sequence of the entities in the list above will be
referred to as the \textit{ERA-parameterization for} $\Gamma$.
The RI Specification is a finite non-empty sequence of pairs of
variables \mbox{$\left(?\gamma, U_{\alpha\ \mathsf{set}} \right)$},
such that $U_{\alpha\ \mathsf{set}} \in \Gamma$. The individual elements of
the RI specification will be referred to as
the \textit{RI specification elements}.
The first element of the RI specification element will be referred to as
the \textit{schematic type variable associated with the RI specification element},
the second element will be referred to as the
\textit{set associated with the RI specification element}.
The sbterm specification is a finite sequence of
pairs \mbox{$(t : ?\bar{\alpha}\ K,\ u : \bar{\beta}\ K)$},
where $t$ is either a constant-instance or a schematic typed term variable
and $u$ is an sbterm with respect to $\Gamma$. The notation for the elements
of the sbterm specification follows a convention similar to the one
introduced for the RI specification elements.
The rewrite rules for the set-based theorem can be any set of
valid rules for the Isabelle simplifier \<^cite>‹"wenzel_isabelle/isar_2019-1"›;
the known premises for the set-based theorem can be any finite
sequence of deductions in $\Gamma$;
the specification of the elimination of premises in the set-based theorem
is a pair $(\bar{t}, m)$, where $\bar{t}$ is a sequence of formulae and $m$
is a proof method; the attributes for the set-based theorem
is a sequence of attributes of Isabelle
(e.g., see \<^cite>‹"wenzel_isabelle/isar_2019-1"›).
›
subsection‹Definition of the ERA\label{sec:def-ERA}›
text‹
The relativization is performed inside a local context $\Gamma$ with an
associated ERA-parameterization (such a context-parameterization pair will
be called a \textit{tts context}). The ERA provides explicit support for
handling the transfer rules local to the context through the infrastructure
for the registration of sbterms, as explained in
subsection \ref{sec:sbts}. Apart from this, the main part of
the ERA largely follows the outline of the RA. However,
the ERA also provides several tools for post-processing of the raw result
of the relativization. The ERA also has an initialization stage, but this
stage is largely hidden from the end-user. Thus, the ERA can be divided
in three distinct parts:
\textit{initialization of the relativization context},
\textit{kernel of the ERA} (KERA) and \textit{post-processing}.
Assume that the context $\Gamma$ contains the variable
$U_{\alpha\ \mathsf{set}}$ and the finite sequences of
variables $\bar{g}$ and $\bar{f}$ indexed by $I$ and $J$, respectively,
such that $\bar{g}_i : \alpha\ \bar{K}_i$ and
$\bar{f}_j : \alpha\ \bar{L}_j$ for all $i \in I$ and $j \in J$
for some sequences of functions $\bar{K}$ and $\bar{L}$ also
indexed by $I$ and $J$, respectively, representing the type constructors.
Also, assume that the input to the relativization algorithm is
the type-based theorem
$\vdash\phi\left[?\alpha_{\Upsilon}, ?\bar{h}\left[?\alpha_{\Upsilon}\right]\right]$
such that $?\bar{h}$ is indexed by $I$ and $\Upsilon$ depends on the
overloaded constants $\bar{*}$ indexed by $J$. Finally, assume that the
ERA is parameterized by the RI specification
$\left(?\alpha_{\Upsilon}, U_{\alpha\ \mathsf{set}}\right)$
and the sbterm specification elements
$(?\bar{h}_i, \bar{g}_i)$ and $(\bar{*}_j, \bar{f}_j)$
for all $i \in I$ and $j \in J$.
\textbf{Initialization of the relativization context}.
Prior to the application of the relativization algorithm, the formula
$\exists \mathsf{Rep}\ \mathsf{Abs}.\ {}_{\alpha}(\beta \approx U)_{\mathsf{Rep}}^{\mathsf{Abs}}$
is added to the context $\Gamma$, with the type variable $\beta$ being fresh for
$\Gamma$, resulting in a new context $\Gamma'$ such that
$\Gamma \subseteq \Gamma'$ and
\mbox{$\exists \mathsf{Rep}\ \mathsf{Abs}.\ {}_{\alpha}(\beta \approx U)_{\mathsf{Rep}}^{\mathsf{Abs}} \in \Gamma'$}.
Then, the properties of the Hilbert choice $\varepsilon$ are used for the
definition of $\mathsf{Rep}$ and $\mathsf{Abs}$ such that
\mbox{$\Gamma' \vdash {}_{\alpha}(\beta \approx U)_{\mathsf{Rep}}^{\mathsf{Abs}}$}
(e.g., see \<^cite>‹"kuncar_types_2015"›).
In this case, \mbox{$(U_{\alpha\ \mathsf{set}},\beta,\mathsf{Rep}_{\beta\rightarrow\alpha},\mathsf{Abs}_{\alpha\rightarrow\beta})$}
is an RI with respect to $\Gamma'$. Furthermore, a fresh
$T_{\alpha\rightarrow\beta\rightarrow\mathbb{B}}$ (for $\Gamma$) is defined as a transfer
relation associated with the RI. Finally, the transfer domain rule associated
with the RI and the side conditions associated with the RI are proved for $T$
with respect to $\Gamma'$.
For each $\bar{g}_i$ such that $i \in I$, the sbt-database contains a deduction
\mbox{$\Gamma \vdash\mathsf{dbr}[?A, U] \longrightarrow \exists a.\ R\left[?A\right]_{\alpha\ \bar{K}_i \rightarrow ?\delta\ \bar{K}_i\rightarrow \mathbb{B}}\ \bar{g}_i\ a$}.
Thence, for each $i \in I$, $?\delta$ is instantiated as
$\beta$ and $?A_{\alpha\rightarrow?\delta\rightarrow\mathbb{B}}$ is instantiated
as $T_{\alpha\rightarrow\beta\rightarrow\mathbb{B}}$. The resulting theorems
are used for the definition of a fresh (for $\Gamma$) sequence of variables $\bar{a}$ such that
\mbox{$\Gamma' \vdash R\left[T_{\alpha\rightarrow\beta\rightarrow\mathbb{B}}\right]_{\alpha\ \bar{K}_i \rightarrow \beta\ \bar{K}_i\rightarrow \mathbb{B}}\ \bar{g}_i\ \bar{a}_i$}.
Similar deductions are also established for the sequence $\bar{f}$, with the
sequence of the variables appearing on the right-hand side of the transfer rules
denoted by $\bar{b}$. These deductions are meant to be used by the transfer
infrastructure during the step of the ERA that is equivalent to step 5 of the RA,
as shown below. Thus, at the end of the initialization of the relativization context,
the theorem is transformed into a deduction of the form
\mbox{$\Gamma'\vdash\phi\left[?\alpha_{\Upsilon}, ?\bar{h}\left[?\alpha_{\Upsilon}\right]\right]$},
where the context $\Gamma'$ (called the \textit{relativization context})
is such that $\Gamma \subseteq \Gamma'$
and it has an associated relativization isomorphism
$(U_{\alpha\ \mathsf{set}}, \beta, \mathsf{Rep}_{\beta\rightarrow\alpha}, \mathsf{Abs}_{\alpha\rightarrow\beta})$
for some fresh $\beta$, the associated fresh transfer relation $T$ and fresh
variables $\bar{a}$ and $\bar{b}$ indexed by $I$ and $J$
(with freshness being assessed with respect to $\Gamma$).
Also, the following transfer rules are provided for all $i \in I$ and $j \in J$:
\mbox{$\Gamma' \vdash \bar{R}_i\left[T\right]\ \bar{g}_i\ \bar{a}_i$} and
\mbox{$\Gamma' \vdash \bar{R'}_j\left[T\right]\ \bar{f}_j\ \bar{b}_j$}
($\bar{R}$ and $\bar{R'}$ are sequences of parametricity relations indexed
by $I$ and $J$, respectively).
\textbf{Kernel of ERA}. The KERA is similar to the RA:
\[
\infer[(7)]
{
\Gamma\vdash U \neq\emptyset\longrightarrow
U\downarrow\bar{g},\bar{f}\longrightarrow
\Upsilon^{\mathsf{on}}_{\mathsf{with}}\ U\ \bar{f} \longrightarrow
\phi^{\mathsf{on}}_{\mathsf{with}}\left[\alpha,U,\bar{g},\bar{f}\right]
}
{
\infer[(6)]
{
\Gamma
\vdash \exists \mathsf{Rep}\ \mathsf{Abs}.{}_{\alpha}(\beta \approx U)_{\mathsf{Rep}}^{\mathsf{Abs}}
\longrightarrow
U\downarrow\bar{g},\bar{f}\longrightarrow
\Upsilon^{\mathsf{on}}_{\mathsf{with}}\ U\ \bar{f}\longrightarrow
\phi^{\mathsf{on}}_{\mathsf{with}}\left[\alpha,U,\bar{g},\bar{f}\right]
}
{
\infer[(5)]
{
\Gamma'
\vdash U\downarrow\bar{g},\bar{f}\longrightarrow
\Upsilon^{\mathsf{on}}_{\mathsf{with}}\ U\ \bar{f}\longrightarrow
\phi^{\mathsf{on}}_{\mathsf{with}}\left[\alpha,U,\bar{g},\bar{f}\right]
}
{
\infer[(4)]
{
\Gamma'
\vdash\Upsilon_{\mathsf{with}}\ \bar{b}\longrightarrow
\phi_{\mathsf{with}}\left[\beta,\bar{a},\bar{b}\right]
}
{
\infer[(3)]
{
\Gamma'
\vdash\Upsilon_{\mathsf{with}}\ ?\bar{f}\left[\beta\right]\longrightarrow
\phi_{\mathsf{with}}\left[\beta,?\bar{h}\left[\beta\right],?\bar{f}\right]
}
{
\infer[(2)]
{
\Gamma'\vdash\Upsilon_{\mathsf{with}}\ ?\bar{f}\left[?\alpha\right]\longrightarrow
\phi_{\mathsf{with}}\left[?\alpha,?\bar{h}\left[?\alpha\right],?\bar{f}\right]
}
{
\infer[(1)]
{
\Gamma'\vdash\phi_{\mathsf{with}}\left[?\alpha_{\Upsilon}, ?\bar{h}\left[?\alpha_{\Upsilon}\right], \bar{*} \right]
}
{
\Gamma'\vdash\phi\left[?\alpha_{\Upsilon}, ?\bar{h}\left[?\alpha_{\Upsilon}\right]\right]
}
}
}
}
}
}
}
\]
Thus, step 1 will be referred to as the first step
of the dictionary construction (similar to step 1 of the RA); step 2 will
be referred to as unoverloading of the type $?\alpha_{\Upsilon}$:
it includes class internalization and the application of the
UO (similar to step 2 of the RA); in step 3, $?\alpha$ is instantiated
as $\beta$ using the RI specification (similar to step 4 in the RA);
in step 4, the sbterm specification is used for the instantiation
of $?\bar{h}$ as $\bar{a}$ and $?\bar{f}$ as $\bar{b}$;
step 5 refers to the application of transfer, including the transfer rules
associated with the sbterms (similar to step 5 in the RA);
in step 6, the result is exported from $\Gamma'$ to $\Gamma$, providing the
additional premise
$\exists \mathsf{Rep}\ \mathsf{Abs}.\ {}_{\alpha}(\beta \approx U)_{\mathsf{Rep}}^{\mathsf{Abs}}$;
step 7 is the application of the attribute
@{attribute cancel_type_definition}
(similar to step 6 in the RA).
The RI specification and the sbterm specification provide the information that
is necessary to perform the type and term substitutions in steps 3 and 4 of
the KERA. If the specifications are viewed as finite maps, their domains
morph along the transformations that the theorem undergoes until step 4.
\textbf{Post-processing}. The deduction that is obtained in the final step of
the KERA can often be simplified further. The following post-processing steps
were created to allow for the presentation
of the set-based theorem in a format that is both desirable and convenient
for the usual applications:
\begin{enumerate}
\item \textit{Simplification}. The rewriting is performed using the rewrite
rules for the set-based theorem: the implementation relies on the
functionality of the Isabelle's simplifier.
\item \textit{Substitution of known premises}. The known premises for the
set-based theorem are matched with the premises of the set-based theorem,
allowing for their elimination.
\item \textit{Elimination of premises}. Each premise is matched against each
term in the specification of the elimination of premises in the
set-based theorem; the associated method is applied in an attempt to eliminate
the matching premises (this can be useful for the elimination of the
premises of the form $U \neq \emptyset$).
\item \textit{Application of the attributes for the set-based theorem}.
The attributes for the set-based theorem are applied as the final step
during post-processing.
\end{enumerate}
Generally, the desired form of the result after a successful application
of post-processing is similar to
\mbox{$\Gamma\vdash\phi^{\mathsf{on}}_{\mathsf{with}}\left[\alpha,U,\bar{g},\bar{f}\right]$}
with the premises \mbox{$U \neq \emptyset$, $U\downarrow\bar{g},\bar{f}$} and
\mbox{$\Upsilon^{\mathsf{on}}_{\mathsf{with}}\ U\ \bar{f}$} eliminated completely
(these premises can often be inferred from the context $\Gamma$).
›
text‹\newpage›
end