\( \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} \)
UP | HOME

Definitions - HOL Light

Table of Contents

1. Type definitions

New types are introduced by a rule of type definition, that it is bijective with a nonempty subset of an existing type.

2. Constant Definitions

Constants are introduced using a rule of constant definition, new_definition, as found in drule.ml

Given some closed term (with some suitable restrictions on type variables) \(t\) and a fresh constant name \(c\) we can define \(c\) and get the new theorem:

\begin{equation} \vdash c = t \end{equation}

Both terms and type definitions give conservative extensions and so in particular preserve logical consistency.

3. References

  • Rob Arthan,
    "HOL Constant Definition Done Right".
    PDF, ITP 2014: Interactive Theorem Proving, Springer pp 531-536
  • Rob Arthan,
    "On Definitions of Constants and Types in HOL".
    Journal of Automated Reasoning 56 (2016) 205–219
    doi:10.1007/s10817-016-9366-4
  • Freek Wiedijk,
    "Stateless HOL".
    arXiv:1103.3322, 15 pages

Last Updated 2024-06-08 Sat 08:07.