Theories

In the HOL world a theory is used as a means of encapsulating logical entities. Typically, a theory is a related collection of types, constants, axioms, definitions, and theorems. Here we describe, in some detail, although not precisely, the hol90 theory facilities.

The current theory

When you use HOL, you are always in a theory, which is called the current theory. (Most theory-related functions will treat the "dash" ("-") as a synonym for the name of the current theory.) When HOL starts up, the current theory you are in is named HOL. This theory represents the culmination of a fair bit of logical development, and as a result the HOL theory has many ancestors.

Ancestry

Every theory except for the initial theory (named min in hol90) has one or more parent theories (found by calling parents). If you follow the parentage all the way back to min, accumulating all the theories you go through, you will have computed the ancestry of the theory (there is a function called ancestry that will do this for you). All the types, constants, axioms, definitions, and theorems of the ancestors of a theory are accessible in the theory.(Note: what we are calling "theories" here are called "theory segments" in the HOL manual/book.)

The entire collection of theories is held in a hierarchical graph structure (a directed acyclic graph with a single root node). Some elements of this structure are held on disk; others are in the ML heap. The HOL system tries to make the location of a theory transparent to the user.

Note. The function ancestry, like many theory-related functions, can only be given the name of a theory that is either the current theory, or an ancestor of the current theory.

```  - ancestry"-";
val it =
["pair","num","BASIC_HOL","prim_rec","arithmetic",
"list","tree", "ltree","rec_type","one","combin",
"sum","min","bool","restr_binder"] : string list

- ancestry"min";
val it = [] : string list

- ancestry "string" handle e => Raise e;

Exception raised at Theory_graph.ancestry:
"string" is not in the theory graph.
```
Notice that ancestry does not include the name of the current theory.

Information functions

The following functions can be used to find out information about items in any theory in the ancestry of the current theory:
```    (* Information on constants *)
val arity : string -> int    (* arity of a type constant *)
val fixity : string -> Thm.Term.fixity
val precedence : string -> int
val const_decl : string -> {const:Thm.Term.term,
theory : string,
place: Thm.Term.fixity}

val is_constant : string -> bool
val is_type : string -> bool
val is_binder : string -> bool
val is_infix : string -> bool

(* Information on the current theory, or an ancestor *)
val draft_mode : unit -> bool
val current_theory : unit -> string
val parents : string -> string list
val ancestry : string -> string list

(* singular *)
val axiom : string -> string -> Thm.thm
val definition : string -> string -> Thm.thm
val theorem : string -> string -> Thm.thm

(* plural *)
val types : string -> {Name : string, Arity : int} list
val constants : string -> Thm.Term.term list
val infixes : string -> Thm.Term.term list
val binders : string -> Thm.Term.term list
val axioms : string -> (string * Thm.thm) list
val definitions : string -> (string * Thm.thm) list
val theorems : string -> (string * Thm.thm) list

(* The whole picture *)
val print_theory : string -> unit
val html_theory : string -> unit
```

Building a theory

One makes a theory by a call to new_theory. A theory built with new_theory has as parent the current theory at the time of the call to new_theory. Once you have called new_theory, you are in draft mode (a call to draft_mode will verify this): now you can freely make definitions for types and constants.
```    (* Operations that change the current theory *)
val new_theory : string -> unit
val close_theory : unit -> unit

(* Adding to the current theory *)
val new_parent : string -> unit
val new_type : {Name : string, Arity : int} -> unit
val new_constant :{Name : string, Ty : hol_type} -> unit
val new_infix : {Name : string, Ty : hol_type, Prec :int} -> unit
val new_binder : {Name : string, Ty : hol_type} -> unit

(* Introduce an axiom *)
val new_open_axiom : (string * term) -> Thm.thm

(* Constant specification *)
val new_specification
: {name :string, sat_thm : thm,
consts : {fixity :fixity,const_name : string} list}
-> thm

(* Definitions *)
val new_definition : (string * term) -> thm
val new_infix_definition :(string * term * int) -> thm
val new_binder_definition : (string *  term) -> thm
val new_type_definition
: {name:string, pred:term, inhab_thm : thm} -> thm

val save_thm : (string * thm) -> thm
```
Also, while in draft mode you can freely make any theory a parent theory with a call to new_parent. If theory X is made a new parent, the entire ancestry of X becomes accessible. Seen from a graph level, new_parent adds an edge to the theory graph, while new_theory adds a new node and a new edge to the graph. (Note: a theory in draft mode has no descendants. This prevents cycles in the graph.) Draft mode is exited by calling close_theory. One can prove and store theorems in the current theory regardless of the draft mode.

When new_theory is called, the contents of the current theory are written to disk before the new theory is constructed. That is, unless the theory is already consistent with disk (this is kept track of internally).

Going to an existing theory

One "goes to" a theory with a call to load_theory (or in rare cases, extend_theory).
```    val load_theory : string -> unit
val extend_theory : string -> unit
```
Because of the ancestry relation, there are some subtle issues with these operations. With a call to load_theory or extend_theory, you can go to any theory provided that it is a descendant of the current theory. As with new_parent, the entire ancestry of the "gone-to" theory will then become accessible. The semantics of load_theory is somewhat confusing, but it is necessary in order to maintain consistency of the system. Once you have loaded a theory, you may prove theorems and store them in the theory, but you may not add new definitions (if you want to do that, use extend_theory instead of load_theory). You can not load or extend an ancestor of the current theory.

Note. Once new_theory has been called implicitly or explicitly in a session, load_theory is not invocable. Why? Because a) a theory in draft mode has no descendants, and b) nothing that can happen after leaving draft mode can add descendants to the current theory.

Example

Suppose the following is the theory path when the hol90 system is started:
``` - theory_path;
val it =
ref
["",
"/hol/working/theories/ascii/",
"/hol/working/library/fixpoint/theories/ascii/",
"/hol/working/library/wellorder/theories/ascii/",
"/hol/working/library/real/theories/ascii/",
"/hol/working/library/pair/theories/ascii/",
"/hol/working/library/prog_logic/theories/ascii/",
"/hol/working/library/unity/theories/ascii/",
"/hol/working/library/integer/theories/ascii/",
"/hol/working/library/group/theories/ascii/",
"/hol/working/library/pred_set/theories/ascii/",
"/hol/working/library/set/theories/ascii/",
"/hol/working/library/string/theories/ascii/"]
: string list ref
```
The current theory is HOL. Now load the theory set, which has the HOL theory as a parent.
``` - load_theory "set";

Theory "HOL" already consistent with disk, hence not exported.
val it = () : unit
```
Now try to load the theory string. You can't! Why? Because string does not have set as a parent.
```  - load_theory "string" handle e => Raise e;

Theory "set" already consistent with disk, hence not exported.

Exception raised at Theory_ops.goto_theory:

uncaught exception HOL_ERR
```

Another example

In hol90, is it possible to build four theories with the following dependence structure in one single SML session?
```      a
/  \
b    c
\  /
d
```
The answer is "No", although the hol90 implementors are thinking of changing the implementation so that this example is possible. To build b, you need to do a new_theory when in theory a. Likewise with building c. However, when you do a new_theory, you advance along in the partial order and you can't go back. Also, you can't have two independent theories in the same session, unless they are in the ancestry of the current theory. To get the picture above, you could build b and c in separate sessions, and then, in a third session, load_theory on either b or c, and then do a new_theory "d", followed by a new_parent on b or c, depending on which was not in the ancestry of d.

Theories and the file system

HOL supports persistent theories: once a user has finished working on a theory, it can be written out to a file, to be loaded or extended at a later date. The current theory is held in the ML heap, but the large number of theories in the HOL system implies that they usually do not all need to be in the heap at the same time. Theory operations make use of the theory path to manipulate theories that are on disk.
```    (* Operations that write the theory to disk *)
val export_theory : unit -> unit
val close : unit -> unit
```
In hol88, the Lisp artifact quit is used to end a session. If the session is in draft mode, this has the side-effect of writing the current theory to disk. In hol90, quit is not implemented; instead, export_theory will write the current theory to disk. Until it is called, the disk file will not be written (or even opened). Ending a session with hol90 is via ^D. If you are building a theory and hit ^D before calling export_theory, no work will be saved on a theory file, since there won't even be a theory file!

In hol90, hol88-style autoloading is not available. The replacement for it is found in the structure Add_to_sml.
```    val add_to_sml : (string * thm) list -> unit
val add_axioms_to_sml : string -> unit
val add_definitions_to_sml : string -> unit
val add_theorems_to_sml : string -> unit
val add_theory_to_sml : string -> unit
```
These calls map theory-level bindings which are of type string * thm to SML-level bindings. Their argument string must be an ancestor of the current theory. For example,
```    - Add_to_sml.add_definitions_to_sml "one";
val one_DEF = |- one = (@x. T) : thm
val oneTY_DEF = |- ?rep. TYPE_DEFINITION (\b. b) rep : thm
val it = () : unit
-
```
One can declare which bindings in a theory are to be reflected into SML by using the function
```    set_autoloads : autoload_info -> unit
```
where autoload_info is a type abbreviation:
```    type autoload_info = {Theory : string,
Axioms : string list,
Definitions : string list,
Theorems : string list}
```

The theory cache

The theory cache is a crude "virtual memory" mechanism at the level of theories. Typically, only the minimum information is kept internally for an ancestor theory. However, once the user requests any information about an ancestor, e.g., the definitions that have been made in it, all the information about that theory is loaded into the theory cache. This can have deleterious effects on the amount of memory available to do proofs in, particularly if the user only needs a small bit of the theory. Therefore, we provide some user control over the theory cache.
```    (* Cache operations *)
val delete_cache : unit -> unit
val delete_theory_from_cache : string -> unit
val theories_in_cache : unit -> string list
```

System theories

There is a map to the entire theory hierarchy accessible in hol90 when it starts up. Note that the HOL theory is current when the system starts up. Only theories that are ancestors of the HOL theory are accessible when the system starts up. Descendants of the HOL theory can be accessed via theory operations (e.g., new_parent and load_theory) or library operations, i.e., load_library.

The following are the files that build the theories available when hol90 starts up.

• Min - the starting theory of HOL
• The existential quantifier
• Bool - definitions of logical constants and axioms
• Pairs
• Restricted binders
• Combinators
• The unit type
• Sum type
• Numbers
• Primitive Recursion Theorem
• Arithmetic
• Lists
• More definitions and theorems about lists
• Unlabelled trees
• Labelled trees
• Support for recursive type definitions

Beginning of Theories