- Theory information facilities
- Building a theory
- Going to an existing theory
- Theories and the file system
- The theory cache
- System theories

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

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

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

**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

- load_theory "set"; Loading theory "set" Theory "HOL" already consistent with disk, hence not exported. val it = () : unitNow try to load the theory

- 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 builda / \ 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

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

- 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

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.

- 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

User Manual Table of Contents.

Konrad Slind, slind@informatik.tu-muenchen.de