Model-Theoretic Conservative Extension for HOL with Ad-hoc Overloading

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

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

Building the Mechanisation

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:

  1. Get PolyML version 5.7 (commit 44b7b88e1a46757dfcddaab0166ca86c7024f198), following the links and instructions at polyml.org. Unfortunately, newer versions may induce HOL4 to crash randomly.
  2. 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.
  3. 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.
  4. 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.

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

Therein,

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.