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. The primitive Boolean type operator bool has name ([],"bool") (and arity 0), and the primitive function space type operator → has name ([],"->") (and arity 2). Type operators may be either external to the article or defined in the article. Two type operators are equal iff (i) they have the same name, and (ii) either they are both external or they are both defined with the same definition.
type
Higher order logic types, such as α and bool list.
const
Higher order logic constants, such as T and =. The primitive equality constant has name ([],"=") (and principal type α → α → bool). Constants may be either external to the article or defined in the article. Two constants are equal iff (i) they have the same name, and (ii) either they are both external or they are both defined with the same definition.
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 always contain a type (though it is often omitted for clarity), so these examples might be more fully written as 13 : Number.Natural.natural and (λ(x : α). (x : α)) : α → α. Terms are α-equivalent if they are equal up to a consistent renaming of bound variables, so λx y. x + y is α-equivalent to λy x. y + x but not to λy x. 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:

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.

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). Successfully reading an article proves that the theorems Δ derive from the assumptions Γ in higher order logic, which we write as the theory Γ ⊳ Δ.

Constraint: The set of theorems Δ must not reference two different type operators that have the same name, and similarly must not reference two different constants that have the same name. Allowing this would prevent articles that depend on Δ from unambiguously referring to these symbols using const or typeOp commands. The same constraint also holds for the set of assumptions Γ, but this almost never causes a problem because assumptions generally contain only external symbols.

Commands

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

  1. i — a decimal integer
  2. "s" — a quoted string
  3. absTerm
  4. absThm
  5. appTerm
  6. appThm
  7. assume
  8. axiom
  9. betaConv
  10. cons
  11. const
  12. constTerm
  13. deductAntisym
  14. def
  15. defineConst
  16. defineConstList [new in version 6]
  17. defineTypeOp [changed in version 6]
  18. eqMp
  19. hdTl [new in version 6]
  20. nil
  21. opType
  22. pop
  23. pragma [new in version 6]
  24. proveHyp [new in version 6]
  25. ref
  26. refl
  27. remove
  28. subst
  29. sym [new in version 6]
  30. thm
  31. trans [new in version 6]
  32. typeOp
  33. var
  34. varTerm
  35. varType
  36. 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]*

Treat the command string as an integer represented in decimal, and convert to the integer 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   ::=   ([^."\] | [\][."\])*
A string matching the regular expression COMPONENT is processed to a 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
Note: If the variable v has type σ and the term b has type τ, then the resulting term λv. b has type σ → τ.
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 type σ (the resulting term f x will have 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 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 t1, ..., Term tn]
:: stack
After: Thm ({ t1, ..., tn } ⊦ φ)
:: stack
Assumptions:     Before:     assumptions
After: assumptions ∪ { { t1, ..., tn } ⊦ φ }
Constraint: The terms t1, ..., tn and φ must have type bool.
Note: This command can be thought of as making an external reference to a theorem. That is, if the article is being read in an environment Δ containing a theorem th that is α-equivalent to { t1, ..., tn } ⊦ φ, then this command extracts the theorem th from the environment, pushes it onto the stack and adds it to the set of assumptions.
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 an external constant c with name n onto the stack.
Stack:     Before:     Name n
:: stack
After: Const c
:: stack
Note: This command makes an external reference to a constant. That is, if the article is being read in an environment Δ containing a constant c with name n, then this command extracts the constant c from the environment and pushes it onto the 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 Γ - { ψ } = Γ).
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 defined 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.
Note: If the type of t is τ, then the principal type of the defined constant c is τ.
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 defined 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 vi must be pairwise distinct variables.
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.
Note: If the type of ti is τi, then the principal type of the defined constant ci is τi.
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 defined type operator op with name n; push a defined constant abs with name abs; push a defined 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: The predicate φ must not contain any free term variables.
Constraint: A must list all the type variables in φ precisely once.
Note: The arity of the defined type operator op is k.
Note: If the type of t is τ, then the principal type of the defined constant abs is τ → (α1,...,αk) op and the principal type of the defined constant rep is (α1,...,αk) op → τ.
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.
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
Note: The only pragma currently supported by the opentheory tool is as follows: if the object x is the name debug, the reader prints debugging information about the state of the stack and dictionary.
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
Note: This command does not fail if φ is not in the hypothesis set Δ (in this case Γ ∪ (Δ - { φ }) = Γ ∪ Δ).
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 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
Constraint: The names αi must be in the global namespace (i.e., be of the form ([],si)).
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 [t1, ..., tn]; pop a theorem Γ ⊦ ψ from the stack; α-convert the theorem Γ ⊦ ψ to { t1, ..., tn } ⊦ φ 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 terms φ and ψ must be α-equivalent.
Constraint: The term set Γ must be α-equivalent to a subset of { t1, ..., tn }.
Constraint: The list of terms [t1, ..., tn] must be distinct with respect to α-equivalence.
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
Constraint: The terms t2 and t2' must be α-equivalent.
typeOp
Pop a name n; push an external type operator op with name n onto the stack.
Stack:     Before:     Name n
:: stack
After: TypeOp op
:: stack
Note: This command makes an external reference to a type operator. That is, if the article is being read in an environment Δ containing a type operator op with name n, then this command extracts the type operator op from the environment and pushes it onto the 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 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
Constraint: The version command may only occur as the very first command in an article file.
Note: If there is no version command in an article file, the version is assumed to be 5.