Theory Introduction
chapter‹ETTS Case Studies: Introduction›
theory Introduction
imports "../ETTS/ETTS_Auxiliary"
begin
section‹Background›
subsection‹Purpose›
text‹
The remainder of this document presents several examples of the application
of the extension of the framework Types-To-Sets and provides the potential
users of the extension with a plethora of design
patterns to choose from for their own applied relativization needs.
›
subsection‹Related work›
text‹
Since the publication of the framework Types-To-Sets in
\<^cite>‹"blanchette_types_2016"›, there has been a growing interest
in its use in applied formalization. Some
of the examples of the application of the framework include
\<^cite>‹"divason_perron-frobenius_2016"›,
\<^cite>‹"maletzky_hilberts_2019"› and \<^cite>‹"immler_smooth_2019"›. However, this
list is not exhaustive. Arguably, the most significant application example
was developed in \<^cite>‹"immler_smooth_2019"›, where Fabian Immler and
Bohua Zhan performed the
relativization of over 200 theorems from the standard mathematics library
of Isabelle/HOL.
Nonetheless, it is likely that the work presented in this document
is the first significant application of the ETTS:
unsurprisingly, the content of this document was developed
in parallel with the extension of the framework itself. Also, perhaps, it is
the largest application of the framework Types-To-Sets
at the time of writing:
only one of the three libraries (SML Relativization) presented in the
context of this work contains the relativization of over 800 theorems
from the standard library of Isabelle/HOL.
›
section‹Examples: overview›
subsection‹Background›
text‹
The examples that are presented in this document were developed for the
demonstration of the impact of various aspects of the relativization process
on the outcome of the relativization.
Three libraries of relativized results were developed in the context
of this work:
\begin{itemize}
\item \textit{SML Relativization}: a relativization
of elements of the standard mathematics library of Isabelle/HOL
\item \textit{TTS Vector Spaces}: a renovation of the set-based
library that was developed in \<^cite>‹"immler_smooth_2019"› using the ETTS
instead of the existing interface for Types-To-Sets
\item \textit{TTS Foundations}: a relativization of a miniature type-based
library with every constant being parametric under the side
conditions compatible with Types-To-Sets
\end{itemize}
›
subsection‹SML Relativization›
text‹
The standard library that is associated with the
object logic Isabelle/HOL and provided as a part of the
standard distribution of Isabelle \<^cite>‹"noauthor_isabellehol_2020"›
contains a significant number of formalized results from a variety of
fields of mathematics. However, the formalization is performed using a
type-based approach: for example, the carrier sets associated with the
algebraic structures and the underlying sets of the topological spaces
consist of all terms of an arbitrary type.
The ETTS was applied to the relativization of a certain number of results from
the standard library.
The results that are formalized in the library
SML Relativization are taken from an array of topics that include
order theory, group theory, ring theory and topology.
However, only the
results whose relativization could be nearly fully automated using
the frameworks UD, CTR and ETTS with almost no additional proof effort
are included.
›
subsection‹TTS Vector Spaces›
text‹
The TTS Vector Spaces is a remake of the library of relativized results that
was developed in \<^cite>‹"immler_smooth_2019"› using the ETTS.
The theorems that are provided in the library TTS Vector Spaces are nearly
identical to the results that are provided in \<^cite>‹"immler_smooth_2019"›.
A detailed description of the original library has already
been given in \<^cite>‹"immler_smooth_2019"› and will not be restated.
The definitional frameworks that are used in \<^cite>‹"immler_smooth_2019"›
and the TTS Vector Spaces are similar. While the unoverloading
of most of the constants could be performed by using the
command @{command ud}, the command @{command ctr} could not
be used to establish that the unoverloaded constants are
parametric under a suitable set of side conditions. Therefore,
like in \<^cite>‹"immler_smooth_2019"›, the proofs of the transfer rules were
performed manually. However, the advantages
of using the ETTS become apparent during the relativization of
theorems: the complex infrastructure that was needed for
compiling out dependencies on overloaded constants, the manual invocation of the
attributes related to the individual steps of the relativization algorithm,
the repeated explicit references to the theorem as it undergoes the
transformations associated with the individual steps of
the relativization algorithm, the explicitly stated names of the set-based
theorems were no longer needed. Furthermore, the theorems synthesized by the
ETTS in TTS Vector Spaces appear in the formal proof documents in a format
that is similar to the canonical format of the Isabelle/Isar declarations
associated with the standard commands such as @{command lemma}.
›
subsection‹TTS Foundations›
text‹
The most challenging aspect of the relativization
process, perhaps, is related to the availability of the transfer rules for the
constants in the type-based theorems. Nonetheless, even if the transfer
rules are available, having to use the relativized constants in the set-based
theorems that are different from the original constants that are used in the
type-based theorems can be seen as unnatural and inconvenient.
Unfortunately, the library SML Relativization suffers from both
of the aforementioned problems. The library that was
developed in \<^cite>‹"immler_smooth_2019"›
(hence, also the library TTS Vector Spaces)
suffers, primarily, from the former problem, but, arguably, due to the methodology
that was chosen for the relativization, the library has a more restricted scope
of applicability.
The library TTS Foundations provides an example of a miniature
type-based library such that all constants associated with the operations on
mathematical structures (effectively, this excludes the
constants associated with the locale predicates)
in the library are parametric under the side conditions
compatible with Types-To-Sets. The relativization is
performed with respect to all possible type variables; in this case,
the type classes are not used in the type-based library. Currently,
the library includes the results from the areas of order theory and
semigroups. However, it is hoped that it can be seen
that the library can be extended to include most of the
content that is available in the main library of Isabelle/HOL.
The library TTS Foundations demonstrates that the development of a
set-based library can be nearly fully automated using the
existing infrastructure associated with the UD, CTR and ETTS,
and requires almost no explicit proofs on
behalf of the users of these frameworks.
›
end