Beginning of Theories
User Manual Table of Contents.
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 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.
(* 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) -> thmAlso, 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.
val load_theory : string -> unit val extend_theory : string -> unitBecause 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.
- 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 refThe 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 = () : unitNow 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.
In hol90, is it possible to build four theories with the following dependence structure in one single SML session?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.a / \ b c \ / d
Beginning of Theories
User Manual Table of Contents.
(* Operations that write the theory to disk *) val export_theory : unit -> unit val close : unit -> unitIn 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!
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 -> unitThese 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 -> unitwhere 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.
(* 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.
The following are the files that build the theories available when hol90 starts up.