We describe the mechanisation of a variant of *model-theoretic conservativity* for HOL with ad-hoc overloading. For a more general introduction, see also our extended abstract at LFMTP 2020. 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://code.cakeml.org/tree/master/candle/overloading

The main additions are within the files

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

Below we describe how to build the mechanisation, and we introduce some of the important theorems.

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.

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 an extension of a theory (by an *update*).

Therein,

`ctxt`

: is a definitional theory,`us`

: is 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`

: is 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 definition `indep_frag_def`

is fed with the proper symbols for each update.

For example 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.