OpenTheory Article Format

Overview

An OpenTheory article file encodes a higher order logic theory. Articles take the form of text files using the UTF-8 character set, and contain commands which are processed by a stack-based virtual machine. The result of reading an article is an import list and an export list of theorems. The theory encoded by the article depends on the theorems in the import list, and uses them to prove the theorems in the export list.

Types

The primitive types processed by the virtual machine are:

int
Integers, such as 0, 42 and -5.
string
Strings, such as "foo" and "".
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 =.
var
Higher order logic term variables, such as x.
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.

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       (* A number *)
| Name of string (* A name *)
| 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. 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. 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:

  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. defineTypeOp
  17. eqMp
  18. nil
  19. opType
  20. pop
  21. ref
  22. refl
  23. remove
  24. subst
  25. thm
  26. typeOp
  27. var
  28. varTerm
  29. varType

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

i — an integer i represented in decimal as 0|[-]?[1-9][0-9]*
Push the object Num i on to the stack.
Stack:     Before:     stack
After: Num i
:: stack
"s" — a quoted string s
Push the object Name s on to the stack.
Stack:     Before:     stack
After: Name s
:: stack
absTerm
Pop a term b; pop a variable v; push the lambda abstraction term λv. b on to 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) on to the stack.
Stack:     Before:     Thm (Γ ⊦ t = u)
:: Var v
:: stack
After: Thm (Γ ⊦ (λv. t) = (λv. u))
:: stack
Note: The variable v must not be free in Γ.
appTerm
Pop a term x; pop a term f; push the function application term f x on to 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 on to 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 {φ} ⊦ φ on to the stack.
Stack:     Before:     Term φ
:: stack
After: Thm ({φ} ⊦ φ)
:: stack
Note: The term φ must have type bool.
axiom
Pop a term φ; pop a list of terms Γ; push the theorem Γ ⊦ φ on to 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} ⊦ φ}
Note: The terms t1, ..., tn and φ must have type bool.
betaConv
Pop a term (λv. t) u; push the theorem ⊦ (λv. t) u = t[u/v] on to 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 on to 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 and definition null on to 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 (Γ - {ψ}) ∪ (Δ - {φ}) ⊦ φ = ψ on to 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 and definition def(t); push the theorem ⊦ c = t on to the stack.
Stack:     Before:     Term t
:: Name n
:: stack
After: Thm (⊦ c = t)
:: Const c
:: stack
Note: The term t must not have any free term variables.
Note: 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 and definition def(φ,A); push a new constant abs with name abs and definition abs(φ,A); push a new constant rep with name rep and definition rep(φ,A); push the theorem ⊦ abs (rep a) = a; push the theorem ⊦ φ r = (rep (abs r) = r) on to 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
Note: A must list all the type variables in φ precisely once.
eqMp
Pop a theorem Δ ⊦ φ' = ψ; pop a theorem Γ ⊦ φ; push the theorem Γ ∪ Δ ⊦ ψ on to the stack.
Stack:     Before:     Thm (Δ ⊦ φ' = ψ)
:: Thm (Γ ⊦ φ)
:: stack
After: Thm (Γ ∪ Δ ⊦ ψ)
:: stack
Note: The terms φ and φ' must be α-equivalent.
nil
Push the empty list [] on to 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
ref
Pop a number k from the stack; look up key k in the dictionary to get an object x; push the object x on to 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 on to 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 on to 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 ref, except that it deletes the entry from the dictionary.
subst
Pop a theorem Γ ⊦ φ; pop a substitution σ; push the theorem Γ[σ] ⊦ φ[σ] on to 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.
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} ⊦ φ}
Note: The terms φ and ψ must be α-equivalent.
Note: The term sets {t1, ..., tn} and Δ must be α-equivalent.
typeOp
Pop a name n; push a new type operator op with name n and definition null on to 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 on to 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 on to the stack.
Stack:     Before:     Var v
:: stack
After: Term t
:: stack
varType
Pop a name n; push a type variable ty with name n on to the stack.
Stack:     Before:     Name n
:: stack
After: Type ty
:: stack
Note: An initial apostrophe is not added to the name.