\( \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

Inductive Definitions - HOL Light

Table of Contents

1. Overview

I understand that:

The new_inductive_definition function automates inductive definitions, using a Knaster-Tarski type derivation under the surface. It can cope with infinitary definitions, parameters, and user-defined monotone operators.

The new_inductive_definition function returns three theorems:

  1. A "rule" theorem (the inductively defined predicate is closed under the rules)
  2. An "induction" [or minimality] theorem asserting the inductively defined predicate is the last such predicate;
  3. A "cases" theorem that each element arises by virtue of one of the rules.

This is programmed up in ind_defs.ml in about 380 lines of code.

2. Inductive Types

This takes quite a bit more work than inductive predicates, it's defined in ind_types.ml as define_type.

3. References

  • Thomas F. Mehlam,
    "Automating recursive type definitions in higher order logic".
    UCAM-CL-TR-146, September 1988, Eprint.
  • Thomas F. Melham,
    "A Package for Inductive Relation Definitions in HOL". Proceedings Of The 1991 International Workshop On The Hol Theorem Proving System And Its Applications, 1991, PDF
  • Juanito Camilleri, Tom Melham,
    "Reasoning with inductively defined relations in the HOL theorem prover".
    Tech Report 265, Cambridge University Dept. of Computer Science, August 1992, eprint

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