# OpenTheory Article File Format

## Overview

An
OpenTheory
*article* file encodes a
higher order logic
theory.
Articles take the form of text files using the
UTF-8
encoding, and contain commands which are processed by a
stack-based virtual machine. The result of reading an article is an
import set *Γ* of assumptions and an export
set *Δ* of theorems. The theory *Γ ⊳
Δ* encoded by the article consists of a proof that the
theorems in *Δ* logically derive from the assumptions in
*Γ*.

## Types

The primitive types processed by the virtual machine are:

`int`- Integers, such as
*0*,*42*and*-5*. `string`- Strings, such as
*"foo"*and*""*. `name`- Names in a hierarchical namespace, such as
*bool*or*Number.Natural.prime*. Names are represented by the type`string list * string`, where the namespace is represented by the`string list`component and the local name is represented by the`string`component. For example,*bool*is represented by*([],"bool")*, and*Number.Natural.prime*is represented by*(["Number","Natural"],"prime")*. The namespace represented by the empty`string list`is called the*global*namespace. `typeOp`- Higher order logic type operators, such as
*bool*and*list*. `type`- Higher order logic types, such as
*α*and*bool list*. `const`- Higher order logic constants, such as
*T*and*=*. Constants are identified by name. `var`- Higher order logic term variables, such as
*x*. Variables are identified by name and type. `term`- Higher order logic terms, such as
*13*and*∀x. x*. `thm`- Higher order logic theorems, such as ⊦
*x = x*and*{x = y, y = T}*⊦*x*. Theorems consist of a hypothesis`term set`and conclusion`term`, both of which are interpreted modulo α-equivalence.

When reading an article file, the virtual machine processes values
of type `object`, which has the following ML-like
definition:

datatype object = |
|||||

Num of int |
(* An integer *) | ||||

| |
Name of name |
(* A name in a hierarchical namespace *) | |||

| |
List of object list |
(* A list (or tuple) of objects *) | |||

| |
TypeOp of typeOp |
(* A higher order logic type operator *) | |||

| |
Type of type |
(* A higher order logic type *) | |||

| |
Const of const |
(* A higher order logic constant *) | |||

| |
Var of var |
(* A higher order logic term variable *) | |||

| |
Term of term |
(* A higher order logic term *) | |||

| |
Thm of thm |
(* A higher order logic theorem *) |

**Note:** Two `Thm` objects are
interchangeable if the theorems they contain are
α-equivalent.

## Virtual Machine

The virtual machine that reads in an article file is equipped with the following state:

- A
*stack*containing values of type`object`. - A
*dictionary*mapping keys of type`int`to values of type`object`. - A set of
*assumptions*of type`thm set`. - A set of
*theorems*of type`thm set`.

Initially the stack, dictionary, assumptions and theorems are all empty.

The virtual machine reads the article file line by line. Every line in an article file is either a comment line or a command line.

- A comment line has
`#`as its first character. Comment lines are discarded by the virtual machine. - A command line encodes exactly one command of the form below, and is immediately executed. Some commands can only be successfully executed in states that satisfy certain constraints. Before executing a command the virtual machine will check that the state satisfies the required constraints, and if not will report an error and terminate. As a result of executing a command, the stack, dictionary, assumptions or theorems may be altered. After a command has been executed it is discarded.

When the virtual machine has finished processing all the lines in the article file, the assumptions and theorems are the result of reading the article (the stack and dictionary are discarded).

## Commands

Here is the complete list of commands interpreted by the virtual machine:

*i*— a decimal integer*"s"*— a quoted string- absTerm
- absThm
- appTerm
- appThm
- assume
- axiom
- betaConv
- cons
- const
- constTerm
- deductAntisym
- def
- defineConst
- defineTypeOp
- eqMp
- nil
- opType
- pop
- ref
- refl
- remove
- subst
- thm
- typeOp
- var
- varTerm
- varType

The remainder of the section describes the precise effects of each command on the virtual machine state.

*i*— a decimal integer- A number command is a string that matches the following regular
expression:
`0|[-]?[1-9][0-9]*`*i*. Push the object`Num`*i*onto the stack.Stack: Before: `stack`After: `Num`*i*`:: stack` *"s"*— a quoted string- A name command is a string that matches the regular expression NAME, which is defined using the following grammar:
NAME ::= `["]`NAMESPACE COMPONENT`["]`NAMESPACE ::= (COMPONENT `[.]`)*COMPONENT ::= ( `[^."\]`|`[\][."\]`)*`string`value by converting all occurrences of`\`*c*to*c*. A string matching the regular expression NAMESPACE is processed to a`string list`value by processing its constituent COMPONENT strings in order. A string matching the regular expression NAME is processed to a`string list * string`value by discarding its outer double quotes and processing its constituent NAMESPACE and COMPONENT strings. A name command is executed by processing the NAME to*(ns,s)*, and pushing the object`Name (`*ns*`,`*s*`)`onto the stack.Stack: Before: `stack`After: `Name (`*ns*`,`*s*`)``:: stack` `absTerm`- Pop a term
*b*; pop a variable*v*; push the lambda abstraction term*λv. b*onto the stack.Stack: Before: `Term`*b*`:: Var`*v*`:: stack`After: `Term (`*λv. b*`)``:: stack` `absThm`- Pop a theorem
*Γ ⊦ t = u*; pop a variable*v*; push the theorem*Γ ⊦ (λv. t) = (λv. u)*onto the stack.Stack: Before: `Thm (`*Γ ⊦ t = u*`)``:: Var`*v*`:: stack`After: `Thm (`*Γ ⊦ (λv. t) = (λv. u)*`)``:: stack`**Constraint:**The variable*v*must not be free in*Γ*. `appTerm`- Pop a term
*x*; pop a term*f*; push the function application term*f x*onto the stack.Stack: Before: `Term`*x*`:: Term`*f*`:: stack`After: `Term (`*f x*`)``:: stack`**Constraint:**The term*f*must have a type of the form*σ → τ*, and the term*x*must have a matching type*σ*. `appThm`- Pop a theorem
*Δ ⊦ x = y*; pop a theorem*Γ ⊦ f = g*; push the theorem*Γ∪Δ ⊦ f x = g y*onto the stack.Stack: Before: `Thm (`*Δ ⊦ x = y*`)``:: Thm (`*Γ ⊦ f = g*`)``:: stack`After: `Thm (`*Γ∪Δ ⊦ f x = g y*`)``:: stack`**Constraint:**The term*f*must have a type of the form*σ → τ*, and the term*x*must have a matching type*σ*. `assume`- Pop a term
*φ*; push the theorem*{φ} ⊦ φ*onto the stack.Stack: Before: `Term`*φ*`:: stack`After: `Thm (`*{φ} ⊦ φ*`)``:: stack`**Constraint:**The term*φ*must have type*bool*. `axiom`- Pop a term
*φ*; pop a list of terms*Γ*; push the theorem*Γ ⊦ φ*onto the stack and add it to the article assumptions.Stack: Before: `Term`*φ*`:: List [Term`*t*_{1}`, ..., Term`*t*_{n}`]``:: stack`After: `Thm (`*{t*_{1}, ..., t_{n}} ⊦ φ`)``:: stack`Assumptions: Before: `assumptions`After: `assumptions`*∪ {{t*_{1}, ..., t_{n}} ⊦ φ}**Constraint:**The terms*t*and_{1}, ..., t_{n}*φ*must have type*bool*. `betaConv`- Pop a term
*(λv. t) u*; push the theorem*⊦ (λv. t) u = t[u/v]*onto the stack.Stack: Before: `Term (`*(λv. t) u*`)``:: stack`After: `Thm (`*⊦ (λv. t) u = t[u/v]*`)``:: stack` `cons`- Pop a list
*t*; pop an object*h*; push the list*h :: t*onto the stack.Stack: Before: `List`*t*`::`*h*`:: stack`After: `List (`*h :: t*`)``:: stack` `const`- Pop a name
*n*; push a new constant*c*with name*n*onto the stack.Stack: Before: `Name`*n*`:: stack`After: `Const`*c*`:: stack` `constTerm`- Pop a type
*ty*; pop a constant*c*; push a constant term*t*with constant*c*and type*ty*.Stack: Before: `Type`*ty*`:: Const`*c*`:: stack`After: `Term`*t*`:: stack` `deductAntisym`- Pop a theorem
*Δ ⊦ ψ*; pop a theorem*Γ ⊦ φ*; push the theorem*(Γ - {ψ}) ∪ (Δ - {φ}) ⊦ φ = ψ*onto the stack.Stack: Before: `Thm (`*Δ ⊦ ψ*`)``:: Thm (`*Γ ⊦ φ*`)``:: stack`After: `Thm (`*(Γ - {ψ}) ∪ (Δ - {φ}) ⊦ φ = ψ*`)``:: stack` `def`- Pop a number
*k*; peek an object*x*on the stack; update the dictionary so that key*k*maps to object*x*.Stack: Before: `Num`*k*`::`*x*`:: stack`After: *x*`:: stack`Dictionary: Before: `dict`After: `dict[`*k → x*`]` `defineConst`- Pop a term
*t*; pop a name*n*; push a new constant*c*with name*n*; push the theorem*⊦ c = t*onto the stack.Stack: Before: `Term`*t*`:: Name`*n*`:: stack`After: `Thm (`*⊦ c = t*`)``:: Const`*c*`:: stack`**Constraint:**The term*t*must not have any free term variables.

**Constraint:**Every type variable that appears in the type of a subterm of*t*must also appear in the type of*t*. `defineTypeOp`- Pop a theorem
*⊦ φ t*; pop a list of names*A*; pop a name*rep*; pop a name*abs*; pop a name*n*; push a new type operator*op*with name*n*; push a new constant*abs*with name*abs*; push a new constant*rep*with name*rep*; push the theorem*⊦ abs (rep a) = a*; push the theorem*⊦ φ r = (rep (abs r) = r)*onto the stack.Stack: Before: `Thm (`*⊦ φ t*`)``:: List [Name`*α*_{1}`, ..., Name`*α*_{k}`]``:: Name`*rep*`:: Name`*abs*`:: Name`*n*`:: stack`After: `Thm (`*⊦ φ r = (rep (abs r) = r)*`)``:: Thm (`*⊦ abs (rep a) = a*`)``:: Const`*rep*`:: Const`*abs*`:: TypeOp`*op*`:: stack`**Constraint:**The predicate*φ*must not contain any free term variables.

**Constraint:***A*must list all the type variables in*φ*precisely once. `eqMp`- Pop a theorem
*Γ ⊦ φ*; pop a theorem*Δ ⊦ φ' = ψ*; push the theorem*Γ ∪ Δ ⊦ ψ*onto the stack.Stack: Before: `Thm (`*Γ ⊦ φ*`)``:: Thm (`*Δ ⊦ φ' = ψ*`)``:: stack`After: `Thm (`*Γ ∪ Δ ⊦ ψ*`)``:: stack`**Constraint:**The terms*φ*and*φ'*must be*α*-equivalent. `nil`- Push the empty list
*[]*onto the stack.Stack: Before: `stack`After: `List`*[]*`:: stack` `opType`- Pop a list of types
*tys*; pop a type operator*op*; push a type with type operator*op*and arguments*tys*.Stack: Before: `List [Type`*ty*_{1}`, ..., Type`*ty*_{n}`]``:: TypeOp`*op*`:: stack`After: `Type (`*(ty*_{1}, ..., ty_{n}) op`)``:: stack` `pop`- Pop an object from the top of the stack.
Stack: Before: *x*`:: stack`After: `stack` `ref`- Pop a number
*k*from the stack; look up key*k*in the dictionary to get an object*x*; push the object*x*onto the stack.Stack: Before: `Num`*k*`:: stack`After: `dict[`*k*`]``:: stack`**Constraint:**The number*k*must be in the domain of the dictionary.

**Note:**This command reads the dictionary, but does not change it. `refl`- Pop a term
*t*; push the theorem*⊦ t = t*onto the stack.Stack: Before: `Term`*t*`:: stack`After: `Thm (`*⊦ t = t*`)``:: stack` `remove`- Pop a number
*k*from the stack; look up key*k*in the dictionary to get an object*x*; push the object*x*onto the stack; delete the entry for key*k*from the dictionary.Stack: Before: `Num`*k*`:: stack`After: `dict[`*k*`]``:: stack`Dictionary: Before: `dict`After: `dict[`*entry k deleted*`]`**Constraint:**The number*k*must be in the domain of the dictionary.

**Note:**This command is exactly the same as the`ref`command, except that it also deletes the entry from the dictionary. `subst`- Pop a theorem
*Γ ⊦ φ*; pop a substitution*σ*; push the theorem*Γ[σ] ⊦ φ[σ]*onto the stack.Stack: Before: `Thm`*θ*`:: List [List [List [Name`*α*_{1}`, Type`*ty*_{1}`], ..., List [Name`*α*_{m}`, Type`*ty*_{m}`]],``List [List [Var`*v*_{1}`, Term`*t*_{1}`], ..., List [Var`*v*_{n}`, Term`*t*_{n}`]]]``:: stack`After: `Thm (`*(θ[ty*_{1}/α_{1}, ..., ty_{m}/α_{m}])[t_{1}/v_{1}, ..., t_{n}/v_{n}]`)``:: stack`**Constraint:**The names*α*must be in the global namespace (i.e., be of the form_{i}*([],s*)._{i})

**Note:**Both the hypothesis set and conclusion of the theorem is instantiated by this rule.

**Note:**The type variables are instantiated first, followed by the term variables.

**Note:**Bound variables will be renamed if necessary to prevent distinct variables becoming identical after the instantiation. `thm`- Pop a term
*φ*; pop a list of terms*Γ*; pop a theorem*Δ ⊦ ψ*from the stack;*α*-convert the theorem*Δ ⊦ ψ*to*Γ ⊦ φ*and add it to the article theorems.Stack: Before: `Term`*φ*`:: List [Term`*t*_{1}`, ..., Term`*t*_{n}`]``:: Thm (`*Δ ⊦ ψ*`)``:: stack`After: `stack`Theorems: Before: `theorems`After: `theorems`*∪ {{t*_{1}, ..., t_{n}} ⊦ φ}**Constraint:**The terms*φ*and*ψ*must be*α*-equivalent.

**Constraint:**The term set*Δ*must be*α*-equivalent to a subset of*Γ*. `typeOp`- Pop a name
*n*; push a new type operator*op*with name*n*onto the stack.Stack: Before: `Name`*n*`:: stack`After: `TypeOp`*op*`:: stack` `var`- Pop a type
*ty*; pop a name*n*; push a term variable*v*with name*n*and type*ty*onto the stack.Stack: Before: `Type`*ty*`:: Name`*n*`:: stack`After: `Var`*v*`:: stack`**Constraint:**The name*n*must be in the global namespace (i.e., be of the form*([],s)*). `varTerm`- Pop a term variable
*v*; push a variable term*t*with variable*v*onto the stack.Stack: Before: `Var`*v*`:: stack`After: `Term`*t*`:: stack` `varType`- Pop a name
*n*; push a type variable*ty*with name*n*onto the stack.Stack: Before: `Name`*n*`:: stack`After: `Type`*ty*`:: stack`**Constraint:**The name*n*must be in the global namespace (i.e., be of the form*([],s)*).

**Note:**The OpenTheory standard theory library adopts the HOL Light convention of naming type variables with capital letters, and theorem provers are expected to map them to local conventions as part of processing articles. For example, in HOL4 it would be natural to map an OpenTheory type variable with name*"A"*to a local type variable with name "'a".