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 nil 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, so two variables such as x : bool and x : α with the same name and different types are treated as distinct.
- term
- Higher order logic terms, such as 13 and ∀x. x. Terms are α-equivalent if they are equal up to a consistent renaming of bound variables, so λx y. p x y is α-equivalent to λy x. p y x but not to λy x. p x y.
- 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
- defineConstList [new in version 6]
- defineTypeOp [changed in version 6]
- eqMp
- hdTl [new in version 6]
- nil
- opType
- pop
- pragma [new in version 6]
- proveHyp [new in version 6]
- ref
- refl
- remove
- subst
- sym [new in version 6]
- thm
- trans [new in version 6]
- typeOp
- var
- varTerm
- varType
- version [new in version 6]
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]*
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 ::= ([^."\] | [\][."\])* 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 - 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 - 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 - assume
- Pop a term φ; push the
theorem { φ } ⊦ φ onto the stack.
Stack: Before: Term φ :: stack After: Thm ({ φ } ⊦ φ) :: stack - 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 t1, ..., Term tn] :: stack After: Thm ({ t1, ..., tn } ⊦ φ) :: stack Assumptions: Before: assumptions After: assumptions ∪ { { t1, ..., tn } ⊦ φ } - 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
Note: This command does not fail if φ is not in the hypothesis set Δ (in this case Δ - { φ } = Δ). - 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: Every type variable that appears in the type of a subterm of t must also appear in the type of t. - defineConstList [new in version 6]
- Pop a theorem { v1 = t1, ..., vk = tk } ⊦ φ; pop a list of name/variable pairs (ni,vi);
push a list of new constants ci with names ni; push the
theorem ⊦ φ[c1/v1, ..., ck/vk] onto the stack.
Stack: Before: Thm ({ v1 = t1, ..., vk = tk } ⊦ φ) :: List [List [Name n1, Var v1], ..., List [Name nk, Var vk]] :: stack After: Thm (⊦ φ[c1/v1, ..., ck/vk]) :: List [Const c1, ..., Const ck] :: stack
Constraint: The terms ti must have no free variables.
Constraint: The free variables of φ must be a subset of {v1, ..., vk}.
Constraint: For every term ti, every type variable that appears in the type of a subterm of ti must also appear in the type of ti. - defineTypeOp [changed in version 6]
- 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 ⊦ (λa. abs (rep a)) = λa. a; push the theorem ⊦ (λr. rep (abs r) = r) = λ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) = λr. φ r) :: Thm (⊦ (λa. abs (rep a)) = λa. a) :: Const rep :: Const abs :: TypeOp op :: stack
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 - hdTl [new in version 6]
- Pop a list h :: t; push the object h; push the list t onto the stack.
Stack: Before: List (h :: t) :: stack After: List t :: h :: stack - 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 ty1, ..., Type tyn] :: TypeOp op :: stack After: Type ((ty1, ..., tyn) op) :: stack - pop
- Pop an object from the top of the stack.
Stack: Before: x :: stack After: stack - pragma [new in version 6]
- Pop an object from the top of the stack, and
perform a reader-dependent operation.
Stack: Before: x :: stack After: stack - proveHyp [new in version 6]
- Pop a theorem Δ ⊦ ψ; pop a
theorem Γ ⊦ φ; push the
theorem Γ ∪ (Δ - { φ }) ⊦ ψ onto the stack.
Stack: Before: Thm (Δ ⊦ ψ) :: Thm (Γ ⊦ φ) :: stack After: Thm (Γ ∪ (Δ - { φ }) ⊦ ψ) :: 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
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]
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 ty1], ..., List [Name αm, Type tym]], List [List [Var v1, Term t1], ..., List [Var vn, Term tn]]] :: stack After: Thm ((θ[ty1/α1, ..., tym/αm])[t1/v1, ..., tn/vn]) :: stack
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. - sym [new in version 6]
- Pop a theorem Γ ⊦ t = u; push the theorem Γ ⊦ u = t onto the stack.
Stack: Before: Thm (Γ ⊦ t = u) :: stack After: Thm (Γ ⊦ u = t) :: stack - 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 t1, ..., Term tn] :: Thm (Δ ⊦ ψ) :: stack After: stack Theorems: Before: theorems After: theorems ∪ { { t1, ..., tn } ⊦ φ }
Constraint: The term set Δ must be α-equivalent to a subset of Γ. - trans [new in version 6]
- Pop a theorem Δ ⊦ t2' = t3; pop a
theorem Γ ⊦ t1 = t2; push the
theorem (Γ ∪ Δ) ⊦ t1 = t3 onto the stack.
Stack: Before: Thm (Δ ⊦ t2' = t3) :: Thm (Γ ⊦ t1 = t2) :: stack After: Thm ((Γ ∪ Δ) ⊦ t1 = t3) :: stack - 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 - 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
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 native 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 native HOL4 type variable with name "'a". - version [new in version 6]
- Pop a number k from the stack, and interpret the rest of
the article using the OpenTheory standard article file format
version k.
Stack: Before: Num k :: stack After: stack
Note: If there is no version command in an article file, the version is assumed to be 5.