# 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:

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

Here is an example theory file:

name: unit

version: 1.0

description: Standard theory of the unit type

author: Joe Leslie-Hurd <joe@gilith.com>

license: MIT

requires: bool

show: "Data.Bool"

show: "Data.Unit"

def {

package: unit-def-1.0

}

thm {

import: def

package: unit-thm-1.0

}

main {

import: def

import: thm

}

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):

BLOCK-NAME {

import: BLOCK-NAME ...

interpret: type "TYPE-OPERATOR-NAME" as "TYPE-OPERATOR-NAME" ...

interpret: const "CONSTANT-NAME" as "CONSTANT-NAME" ...

interpretation: "FILENAME.int" ...

article: "FILENAME.art"

}

Suppose the blocks named by the *n* import: lines compute the theories *Γ _{1} ⊳ Δ_{1} ... Γ_{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

*(Γ*.

_{1}∪ ... ∪ Γ_{n}∪ (Γ[σ] - (Δ_{1}∪ ... ∪ Δ_{n}))) ⊳ Δ[σ]### Package Blocks

A package block has this general form:

BLOCK-NAME {

import: BLOCK-NAME ...

interpret: type "TYPE-OPERATOR-NAME" as "TYPE-OPERATOR-NAME" ...

interpret: const "CONSTANT-NAME" as "CONSTANT-NAME" ...

interpretation: "FILENAME.int" ...

package: PACKAGE-NAME-VERSION

checksum: CHECKSUM

}

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 *Γ _{1} ⊳ Δ_{1} ... Γ_{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

*(Γ*.

_{1}∪ ... ∪ Γ_{n}∪ (Γ[σ] - (Δ_{1}∪ ... ∪ Δ_{n}))) ⊳ Δ[σ]### Union Blocks

A union block has this general form:

BLOCK-NAME {

import: BLOCK-NAME ...

}

Suppose the blocks named by the *n* import: lines compute the theories *Γ _{1} ⊳ Δ_{1} ... Γ_{n} ⊳ Δ_{n}*. Then the theory computed by the union block is

*(Γ*.

_{1}∪ ... ∪ Γ_{n}) ⊳ (Δ_{1}∪ ... ∪ Δ_{n})