COMMON HOL PROOF OBJECT FILE FORMAT
VERSION 0.5
The Common HOL standard includes a standard file format for porting proof
objects between HOL systems. This file explains this file format. Please refer
to the HOL Glossary for definitions of terminology.
1 BASIC CONCEPTS
1.1 PROOF OBJECTS
A HOL proof object captures how to recreate a single HOL declaration, assertion
or proved theorem. Each proof object is stored in its own proof object file,
which has a .prf extension.
There are 12 types of proof object. These break down into 3 groups:
Stand-alone theorems
Axiom - an axiom assertion
Thm - a proved theorem with a textual name, no asms and no free vars
Othm - a proved theorem with a textual name
Nthm - a proved theorem with a numeric name
Type constant introduction
Typedecl - a type constant declaration
Basictypedef - a simple type constant definition
Typedef - a type constant definition (not currently used)
Constant introduction
Constdecl - a constant declaration
Basicdef - a simple constant definition
Def - a function definition (overlaps with Basicdef if has no args)
Spec - a specification of one or more constants (using an exists thm)
Typebij - abstraction and representation functions for a type constant
1.2 PROOF MODULES
A proof module is a collection of proof objects. A proof module is stored on
disk as a directory of proof object files.
As well as its proof object files, a proof module directory also has a SUMMARY
file. This gives version information about the HOL system on which the proof
module was originally created, together with a listing of all the proof module's
proof objects and their file names, in the same order as the proof objects were
created in the original system.
1.3 PROOF REPOSITORY
A proof repository is a directory storing a collection of proof module
directories. This directory should also contain a file called HOL_TRANS_TABLE,
for showing correspondences between different HOL systems.
2. LEXICAL SYNTAX
The same lexical syntax is used for proof object files, proof module SUMMARY
files and proof repository HOL_TRANS_TABLE files.
The whitespace characters are space and tab. These have no effect other than
separting adjacent lexical tokens that would otherwise be part of the same
token.
Newline is treated specially to separate out section entries and/or sections.
Comments start with a hash character ('#') and continue to the end of a line.
Numerals are one or more decimal digits.
General identifiers start with an uppercase letter, followed by zero or more
alphanumerics. In proof object files, they are used to refer to object
constructors and proof object types.
Special identifiers start with a lowercase letter, followed by one or more
digits. In proof object files, they are used to refer to preamble entries.
A string token has a doublequote ('"') as start and end delimiters, with any
series of characters in between. A backslash ('\') is used for the escape
character: backslash-backslash denotes a backslash character; backslash-
doublequote denotes a doublequote character; backslash followed by 3 digits
denotes the character with a decimal ASCII code of the 3 digits. In proof
object files, string tokens are used for referring to proof objects and
entities.
A heading token starts with '>' followed by zero or more alphanumerics.
A punctuation token is a single character from the following:
'(' ')' '[' ']' ';' ',' ':' '*' '+'
3. PROOF OBJECT SYNTAX
This section describes the syntax for proof object files.
3.1 FILE LAYOUT
Files are separated into sections by lines starting with a '>' heading token.
Some sections are optional, and can be excluded if they are empty for a given
proof object. Every file has an initial grouping of sections, called the
"header". Every file (other than those for type bijections) follows the header
by an empty '>' heading line, followed by the remaining sections, called the
"body". The sections appearing in the body depend on the proof object type.
They consist of optional preamble sections, a main section and potentially a
target term section at the end.
3.2 HEADER SECTIONS
The header consists of a title section and an optional inherit section.
The title section has the proof object type its the heading, followed by the
proof object name on the next line.
The inherit section has "Inherit" as its heading, followed by one line for each
direct ancestor proof object. Each line consists of the proof object's
type abbreviation followed by the proof object's name. The proof object type
abbreviations are as follows:
A Axiom
BD Basicdef
BZD Basictypedef
C Constdecl
D Def
N Nthm
O Othm
S Spec
T Thm
Z Typedecl
ZB Typebij
ZD Typedef
3.3 PREAMBLE SECTIONS
Preamble sections construct objects for use in subsequent sections of the file.
There can be preamble sections for types, terms, fetch theorems (i.e. theorems
resulting from other proof objects) and subproof theorems (i.e. theorems used in
the main proof section). Each preamble consists of a numbered list of entries,
with one entry per line. The numbering must be incremental and start at 1.
Each preamble entry is a (potentially compound) expression showing how to
recreate an object using constructors. The constructors are denoted by
identifier tokens. To enable meaningful and yet single-character identifiers
for most constructors (for file compactness reasons), the identifiers refer to
different constructors depending on the section they occur in.
The type preamble has "Types" as its heading. The constructors in the type
preamble are as follows:
F function type
K compound type
V type variable
The term preamble has "Terms" as its heading. The constructors used are as
follows:
A function application
B binary function application
C conjunction term
D disjunction term
E equality term
I implication term
K constant, followed by ordered type instantiation list (see Appendix A)
L lambda abstraction
M numeral
N not term
P pair expression
S select expression
U universal quantification
UX unique existential quantification
V variable
X existential quantification
The fetch preamble has "Fetches" as its heading. The constructors used are the
same proof object type abbreviations as used in the header ancestor section (see
above). However, in the fetch preamble, there may be an ordered type
instantiation list (see Appendix A) following the proof object name.
The subproof preamble has "Subproofs" as its heading. The constructors used are
the same as in the main proof section (see below).
Objects defined in preambles can be referred to in subsequent entries/sections
by using a special identifier token. This special identifier starts with a
lowercase character signifying the object's type, followed by the object's entry
number in its preamble. Letters correspond to object types as follows:
z type
t term
f fetch theorem
s subproof theorem
3.4 MAIN PROOF SECTION
The main proof section is a single line consisting of a (usually compound)
expression showing how to contruct a theorem from theorem constructors (i.e.
inference rules). The same syntax is used for subproof preamble entries.
The following theorem constructor abbreviations are used (illustrated here with
their HOL Zero and HOL Light rule names):
Abbrev HOL Zero rule HOL Light rule
A assume_rule ASSUME
AA add_asm_rule ADD_ASSUM
AL alpha_link_conv ALPHA
ALC alpha_conv ALPHA_CONV
B beta_conv BETA_CONV
C contr_rule CONTR
CC ccontr_rule CCONTR
CE1 conjunct1_rule CONJUNCT1
CE2 conjunct2_rule CONJUNCT2
CH choose_rule CHOOSE
CI conj_rule CONJ
D disch_rule DISCH
DAS deduct_antisym_rule DEDUCT_ANTISYM_RULE
DE disj_cases_rule DISJ_CASES
DI1 disj1_rule DISJ1
DI2 disj2_rule DISJ2
E eq_mp_rule EQ_MP
EE1 eq_imp_rule1 EQ_IMP_RULE (1st theorem)
EE2 eq_imp_rule2 EQ_IMP_RULE (2nd theorem)
EI imp_antisym_rule IMP_ANTISYM_RULE
EC eta_conv ETA_CONV
FE eqf_elim_rule EQF_ELIM
FI eqf_intro_rule EQF_INTRO
G gen_rule GEN
H prove_asm_rule PROVE_HYP
I inst_rule INST
IT imp_trans_rule IMP_TRANS
J inst_type_rule INST_TYPE
M mp_rule MP
M.. (see congruence rule list below)
NCSC eval_suc_conv NUM_SUC_CONV
NCPR eval_pre_conv NUM_PRE_CONV
NCA eval_add_conv NUM_ADD_CONV
NCS eval_sub_conv NUM_SUB_CONV
NCM eval_mult_conv NUM_MULT_CONV
NCE eval_exp_conv NUM_EXP_CONV
NCEV eval_even_conv NUM_EVEN_CONV
NCOD eval_odd_conv NUM_ODD_CONV
NCEQ eval_num_eq_conv NUM_EQ_CONV
NCLT eval_lt_conv NUM_LT_CONV
NCLE eval_le_conv NUM_LE_CONV
NCGT eval_gt_conv NUM_GT_CONV
NCGE eval_ge_conv NUM_GE_CONV
NE not_elim_rule NOT_ELIM
NI not_intro_rule NOT_INTRO
R refl_conv REFL
S spec_rule SPEC
SB subs_rule SUBS
SBC subs_conv SUBS_CONV
SR select_rule SELECT_RULE
ST subst_rule SUBST
STC subst_conv SUBST_CONV
T trans_rule TRANS
TE eqt_elim_rule EQT_ELIM
TI eqt_intro_rule EQT_INTRO
U undisch_rule UNDISCH
X exists_rule EXISTS
Y sym_rule SYM
YC sym_conv SYM_CONV
Multi-character theorem constructor abbreviations that start with "M" refer to
equality congruence rules, as follows:
MA mk_comb_rule MK_COMB
MA1 mk_comb1_rule AP_THM
MA2 mk_comb2_rule AP_TERM
MB mk_bin_rule -
MB1 mk_bin1_rule -
MB2 mk_bin2_rule -
MC mk_conj_rule MK_CONJ
MC1 mk_conj1_rule -
MC2 mk_conj2_rule -
MD mk_disj_rule MK_DISJ
MD1 mk_disj1_rule -
MD2 mk_disj2_rule -
ME mk_eq_rule -
ME1 mk_eq1_rule -
ME2 mk_eq2_rule -
MI mk_imp_rule -
MI1 mk_imp1_rule -
MI2 mk_imp2_rule -
ML mk_abs_rule ABS
MN mk_not_rule -
MP mk_pair_rule -
MP1 mk_pair1_rule -
MP2 mk_pair2_rule -
MS mk_select_rule -
MU mk_forall_rule MK_FORALL
MX mk_exists_rule MK_EXISTS
MUX mk_uexists_rule -
3.5 TARGET SECTION
Theorem proof object files contain a target section at the end. This presents
the conclusion of the theorem as a term object. This enables the importing
system to recreate the original theorem with its original binding variable
names. Note that otherwise, the theorem created by the main proof section might
have differing binding variable names, because the Common HOL standard only
mandates rules to work modulo alpha-equivalence.
The target section has "Target" as its heading, followed a single line referring
to a term object.
APPENDIX A: ORDERED TYPE INSTANTIATION LISTS
An ordered type instantiation list is a compact way of expressing an
instantiation for the type variables in a given fetch theorem / type constant's
generic type. It consists of a (potentially empty) series of type objects, with
one type object for each type variable in the fetch theorem / generic type. The
type objects occur in the same order in the series as the first occurrence of
their corresponding type variable in the fetch theorem / generic type.
For example, in the following generic type:
`:(B->A)->B->bool`
the type variables occur in order `:B`, `:A`, and thus the following ordered
type instantiation list:
`:C` `:B`
will result in the following generic type:
:(C->B)->C->bool`.