Filter
Top Products
Chapter 13
Examples
A few examples are included in Examples directory. These just give some indication
of how the system can be used. They aren’t held up as particularly good examples
exploiting HOL Light’s facilities; indeed many of them are crudely ported from
older versions of HOL. A few of them might be useful to some readers, but they are
generally not polished or documented.
• analysis.ml is a development of elementary real analysis, e.g. sequences,
series, limits, continuity, differentiation and integration.
• lagrange.ml shows how to prove some numerical identities using ordered
rewriting and/or decision procedures.
• mizar.ml is a system for writing HOL proofs in a more readable declarative
style based on Trybulec’s Mizar system (Rudnicki 1992).
• prog.ml is a simple embedding of the semantics of a toy imperative program-
ming language, derivation of weakest preconditions and Floyd-Hoare rules,
and a tactic that performs verification condition generation on an annotated
program.
• rectypes.ml defines a wide variety of (mutual, nested) recursive types.
• reduct.ml defines some basic notions for reductions, e.g. confluence, nor-
malization, and proves a few theorems like Newman’s Lemma. It requires
rstc.ml to have been loaded first.
• rstc.ml defines various combinations of reflexive, symmetric and transitive
closures of binary relations, and proves a comprehensive set of theorems about
them.
• transc.ml defines and proves properties of the elementary transcendental
functions like exp, sin and ln. It requires analysis.ml to have been loaded
first.
• wo.ml proves some important version of the Axiom of Choice, e.g. the wellorder-
ing principle and Zorn’s Lemma.
101