We describe the mechanisation of a variant of model-theoretic conservativity for HOL with ad-hoc overloading. If a theory update overloads constants, we must assign a new interpretation to certain constants and types, namely to constants and types that depend on the new overloads. As a corollary of model-theoretic conservativity, we obtain consistency of HOL with ad-hoc overloading.
The mechanisation of model-theoretic conservativity for HOL with ad-hoc overloading is examinable from the CakeML development repository at
The main additions are within the files
Below we introduce some of the important theorems, and we describe how to build the mechanisation.
We discuss the main definitions and theorems, and link each to the corresponding lines of our proof development.
We establish different dependencies and define the independent
which contains all symbols that are not depending on what is introduced
by an update. It takes the arguments
indep_frag ctxt us frag
ctxt: a definitional theory,
us: a list of symbols. Anything that depends on any of these symbols shall be excluded from the resulting fragment. In the implementation a theory extension may introduce several new symbols as a slightly different definition mechanism is used (in comparison to the earlier paper).
frag: the parent fragment of the independent fragment.
The proven theorem
states that the above described
indep_frag gives a
fragment, even for arbitrary lists
the above definition is fed with the proper symbols for each update,
e.g. a type definition
TypeDefn name predicate rep abs
introduces a new type
Tyapp name l where
as many distinct type variables as the defining predicate contains. The
independent fragment is maximal in the sense, that each of its types’
non-builtin subtypes is also in the fragment, see
says that the independent fragment cuts off anything from the update,
and thus its symbols are among the old symbols. (The old
symbols are notated there as
total_fragment (sigof ctxt), whereas the parent fragment is
total_fragment (sigof (upd::ctxt))). This lemma is
essential to the main claim.
extends a model of a theory to accomodate for a theory update and all
changes that are introduced by the update. The model extension keeps
interpretations for symbols within the independent fragment, which the
confirms. Apart from six lines (see half of the changes)
the model construction is according to A Mechanised Semantics for HOL
with Ad-hoc Overloading.
Our incremental model construction extends models
ctxt that interpret introduced constants equal
to their witnesses, which the predicate
models_ConstSpec_witnesses Δ Γ ctxt
ensures. Any extended model also satisfies this property, see
states that the construction indeed gives a model. It is used in the
to prove that any theory of definitions and admissible axioms has a
For an inspection in the HOL theorem prover please follow the following instructions, which are adapted from the appendix of A Mechanised Semantics for HOL with Ad-hoc Overloading.
The mechanisation currently only runs on a highly specific development version of HOL4. Here’s how to build and run it:
44b7b88e1a46757dfcddaab0166ca86c7024f198), following the links and instructions at polyml.org. Unfortunately, newer versions may induce HOL4 to crash randomly.
f8ad83efa9d8ea2344e5b67bc06a8970b79e8cd2from the HOL4 repository, and follow the installation instructions in the
INSTALLfile. Make sure the
bin/folder in the HOL directory is in your
3dd03770c2570c713ae82dc6150f99b3608cac3dfrom the CakeML development repository, and run
Holmakein the directory
candle/overloading/semantics/to compile all proofs of our mechanisation and their dependencies.