OpenTheory Theory File Format

Overview

An OpenTheory theory file encodes a higher order logic theory package. Theory files take the form of text files using the UTF-8 encoding, and describe package information and a logical theory constructed from proof article files, symbol interpretation files and other theory packages.

The structure of a theory file is as follows:

1. A sequence of package information lines, each of which has the format NAME: VALUE
2. A sequence of named theory blocks, which must include a theory block named main

Here is an example theory file:

The remainder of this document describes the package information and theory blocks in more detail.

Package Information

Each package information line must have the format NAME: VALUE. A string is a valid NAME if and only if it satisfies the regular expression [a-z][a-z0-9]*(-[a-z][a-z0-9]*)*. Any string is a valid VALUE if it doesn't contain a new line.

Any sequence of NAME: VALUE lines can appear in the package information section, and the NAME fields need not be unique. However, the following NAME package information lines are treated specially:

author

There must be a unique author: AUTHOR-NAME <AUTHOR-EMAIL> package information line.

description

There must be a unique description: DESCRIPTION package information line.

license

There must be a unique license: LICENSE package information line.

name

There must be a unique name: PACKAGE-NAME package information line, where PACKAGE-NAME satisfies the regular expression [a-z]+(-[a-z]+)* and is the name of the theory package.

requires

There may be any number of requires: PACKAGE-NAME package information lines, which declare a list of packages that collectively satisfy the assumptions of the theory package.

show

There may be any number of show: "NAMESPACE" and show: "NAMESPACE" as "NAMESPACE" package information lines, which control how the theory package is presented.

version

There must be a unique version: PACKAGE-VERSION package information line, where PACKAGE-VERSION satisfies the regular expression [0-9]+([.][0-9]+)* and is the version of the theory package.

*-file

There may be any number of *-file: "FILENAME" package information lines, which register additional files to be included in the theory package. For example, a source-file: "THEORY.ml" package information line could be used to include a proof script file in the theory package.

Theory Blocks

There are three kinds of theory blocks: article blocks, package blocks and union blocks. Each block has a unique BLOCK-NAME, and blocks import other blocks using their BLOCK-NAME (the block import graph must be acyclic). Every block computes a theory Γ ⊳ Δ (where the theorems in Δ logically derive from the assumptions in Γ), and the theory of the required main block is exported by the theory package.

Article Blocks

An article block has this general form (the ... indicate that zero or more of these lines may be present):

Suppose the blocks named by the n import: lines compute the theories Γ₁ ⊳ Δ₁ ... Γ_n ⊳ Δ_n, let σ represent the renaming of type operators and constants encoded by the interpret: lines and interpretation files in the interpretation: lines, and suppose the article file in the article: line encodes the theory Γ ⊳ Δ. Then the theory computed by the article block is (Γ₁ ∪ ... ∪ Γ_n ∪ (Γ[σ] - (Δ₁ ∪ ... ∪ Δ_n))) ⊳ Δ[σ].

Package Blocks

A package block has this general form:

A PACKAGE-NAME-VERSION satisfies the regular expression PACKAGE-NAME-PACKAGE-VERSION, and specifies a package name and version to be used. The optional checksum: field may be used to ensure that the package used has the correct CHECKSUM. Suppose the blocks named by the n import: lines compute the theories Γ₁ ⊳ Δ₁ ... Γ_n ⊳ Δ_n, let σ represent the renaming of type operators and constants encoded by the interpret: lines and interpretation files in the interpretation: lines, and suppose the package specified by the package: and checksum: lines contains the theory Γ ⊳ Δ. Then the theory computed by the package block is (Γ₁ ∪ ... ∪ Γ_n ∪ (Γ[σ] - (Δ₁ ∪ ... ∪ Δ_n))) ⊳ Δ[σ].

Union Blocks

A union block has this general form:

Suppose the blocks named by the n import: lines compute the theories Γ₁ ⊳ Δ₁ ... Γ_n ⊳ Δ_n. Then the theory computed by the union block is (Γ₁ ∪ ... ∪ Γ_n) ⊳ (Δ₁ ∪ ... ∪ Δ_n).

OpenTheory standard theory file format version 2, published on 10 September 2011.