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
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 fragwhere
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:
44b7b88e1a46757dfcddaab0166ca86c7024f198), following the
links and instructions at polyml.org. Unfortunately,
newer versions may induce HOL4 to crash randomly.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.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.