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.

User Manual Table of Contents

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.

Beginning of Theories
User Manual Table of Contents.

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.

Beginning of Theories
User Manual Table of Contents.

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

Beginning of Theories
User Manual Table of Contents.

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).

Beginning of Theories
User Manual Table of Contents.

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";

 Loading 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;

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

  Exception raised at Theory_ops.goto_theory:
  cannot load/extend given theory

  uncaught exception HOL_ERR

Beginning of Theories
User Manual Table of Contents.

Another example

A user asked:
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.

Beginning of Theories
User Manual Table of Contents.

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!

Autoloading

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}

Beginning of Theories
User Manual Table of Contents.

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

Beginning of Theories
User Manual Table of Contents.

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.

Beginning of Theories
User Manual Table of Contents.
Konrad Slind, slind@informatik.tu-muenchen.de