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

https://github.com/CakeML/cakeml/tree/master/candle/overloading

The main additions are within the files

- semantics/holModelConservativityScript.sml
- syntax/holSyntaxExtraScript.sml
- semantics/holConsistencyScript.sml

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
fragment `indep_frag_def`

which contains all symbols that are not depending on what is introduced
by an update. It takes the arguments

`indep_frag ctxt us frag`

where

`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 `indep_frag_is_frag`

states that the above described `indep_frag`

gives a
fragment, even for arbitrary lists `us`

.

Within `indep_frag_upd_def`

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 `l`

are
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 `indep_frag_allTypes`

and `indep_frag_allTypes_types_of_frag`

.

The lemma `indep_frag_upd_frag_reduce`

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.

The function `type_interpretation_ext_of_def`

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
theorem `model_conservative_extension_prop`

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 `(Δ,Γ)`

of theories `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 `models_ConstSpec_witnesses_model_ext`

.

The theorem `interpretation_is_model`

states that the construction indeed gives a model. It is used in the
theorem `interpretation_exists_model`

to prove that any theory of definitions and admissible axioms has a
model.

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:

- Get PolyML
version 5.7 (commit
`44b7b88e1a46757dfcddaab0166ca86c7024f198`

), following the links and instructions at polyml.org. Unfortunately, newer versions may induce HOL4 to crash randomly. - Check out commit
`f8ad83efa9d8ea2344e5b67bc06a8970b79e8cd2`

from the HOL4 repository, and follow the installation instructions in the`INSTALL`

file. Make sure the`bin/`

folder in the HOL directory is in your`$PATH`

. - Check out commit
`3dd03770c2570c713ae82dc6150f99b3608cac3d`

from the CakeML development repository, and run`Holmake`

in the directory`candle/overloading/semantics/`

to compile all proofs of our mechanisation and their dependencies. - To browse the theories interactively, follow the instructions in the HOL4 documentation to set up HOL4 interaction with your choice of emacs or vim. If you only want to read the theories, any text editor with unicode support should be alright.