HOL4 の使い方（２）
前回紹介したライブラリーのロード，オープン以外にも，グローバル変数の設定や，自作の定理，tacticなどを起動時に読み込ませるには，ホームディレクトリ（WindowsではC:\Users\ユーザー名）に
hol-config.sml
hol-config.ML
.hol-config
.hol-config.sml
.hol-config.ML
の何れかの名のファイルとして記述しておけば
---------------------------------------------------------------------
HOL-4 [Kananaskis 8 (stdknl, built Tue Feb 19 09:22:24 2013)]
For introductory HOL help, type: help "hol";
---------------------------------------------------------------------
[Use-ing configuration file /home/knoppix/hol-config.sml]
[loading theories and proof tools ************** ]
[closing file "/home/knoppix/CAS/hol-kananaskis-8/tools/end-init-boss.sml"]
-
のように利用してくれます．
ただし，この方法でオープンするとその内容が表示されないので，rlwrap などを用いるならコンプリーションファイルが必要になるかも知れません．
また，余り多くオープンすると名前の干渉など，エラーの原因ともなります．
なお，基本的なセオリーやライブラリーの幾つかは help "HOL" ; の中にも挙がっています．
- help"HOL";
+ Entering expressions
+ --------------------
+
+ The HOL type parser is called "Type".
+
+ Example: Type `:bool -> ('a -> bool) -> ind`
+
+ The HOL term parser is called "Term".
+
+ Example: Term `!x. ?y. x = y`
+
+ Types and terms can also be entered using double backquotes.
+
+ Example: ``:bool -> ('a -> bool) -> ind``
+ ``!x. ?y. x = y``
+
+ Goals are typically set with "g", which is an abbreviation
+ for "set_goal".
+
+ Example: g `!x. ?y. x = y`
+ set_goal ([], ``!x. ?y. x = y``)
+
+
+ Theories
+ --------
+
+ In HOL, theories are represented by ML structures. The theories listed
+ below are some of those that come pre-built in the system.
+
+ ------------------------------------------------------------------
+ | minTheory | the origin theory |
+ | boolTheory | basic logical operators |
+ | pairTheory | theory of pairs |
+ |------------------------------------------------------------------|
+ | numTheory | Peano's axioms from the axiom of infinity |
+ | prim_recTheory | primitive recursion theorem |
+ | arithmeticTheory | Peano arithmetic development |
+ | intTheory | integers |
+ | transcTheory | real numbers and analysis |
+ |------------------------------------------------------------------|
+ | | transitive closure of a relation |
+ | relationTheory | wellfoundedness, induction, and recursion |
+ | | wellfoundedness at useful types |
+ |---------------------------------------------------------------- |
+ | setTheory | sets as a type (includes finite sets) |
+ | pred_setTheory | sets as predicates (includes finite sets) |
+ | bagTheory | multisets (includes finite multisets) |
+ |------------------------------------------------------------------|
+ | listTheory | basic theory of lists |
+ | rich_listTheory | extended theory of lists |
+ | llistTheory | theory of lazy lists |
+ |------------------------------------------------------------------|
+ | combinTheory | combinators |
+ | optionTheory | the "option" type |
+ | sumTheory | the disjoint sum type operator |
+ | finite_mapTheory | finite maps from 'a to 'b |
+ |------------------------------------------------------------------|
+ | res_quanTheory | restricted quantifier support |
+ |------------------------------------------------------------------|
+ | stringTheory | strings |
+ |------------------------------------------------------------------|
+ | wordsTheory | theory of bitstrings |
+ |------------------------------------------------------------------|
+ | Temporal_LogicTheory | linear time temporal logic |
+ | Omega_AutomataTheory | infinite state automata |
+ ------------------------------------------------------------------
+
+ An invocation of HOL provides theories of lists, natural numbers,
+ booleans, sums, and pairs. To gain access to any other theory when
+ working interactively, simply invoke
+
+ load "xTheory";
+
+ where "x" is the name of the theory. Once the theory has been loaded
+ by the system, access to its contents is through the `dot' notation of
+ ML, e.g.,
+
+ xTheory.FOO_DEF,
+
+ or if you prefer, by `open'ing the structure and then directly
+ accessing its contents.
+
+
+ Libraries
+ ---------
+
+ As for theories, a library is represented by an ML structure and can
+ thus be brought into an interactive session by invoking `load', e.g.,
+
+ load "xLib";
+
+ One difference between libraries and theories is that a library can in
+ general consist of a collection of theories and support ML structures.
+ Thus sometimes, but not always, the functionality of a library is
+ distributed through a collection of ML structures, all of which have
+ been brought into the interactive session by the call to `load'. It
+ currently (unhappily) falls to the user to know about the
+ functionality of a library. Some libraries provide `help' and manuals
+ for their use; others do not.
+
+ HOL currently offers the following libraries.
+
+ ----------------------------------------------------------------
+ | boolLib | derived rules, tactics, convs, rewriting |
+ | bossLib | suite of automatic tools |
+ | simpLib | Isabelle-style simplifier |
+ | numLib | support library for numbers |
+ | intLib | support library for integers |
+ | realLib | support library for real numbers |
+ | probLib | probability theories |
+ | temporalLib | temporal logic and Buechi automata |
+ | goalstackLib | simple manager for building tactic proofs |
+ | IndDefLib | inductive definitions package |
+ | optionLib | option type |
+ | pairLib | extended support for pairs |
+ | pred_setLib | sets as predicates |
+ | listLib | extensive development of lists |
+ | stringLib | characters and strings |
+ | wordsLib | theories and proof support for bitstrings |
+ | unwindLib | unwinding existential quantifiers |
+ | res_quanLib | bounded quantification |
+ | refuteLib | support for refutation procedures |
+ | reduceLib | basic reasoners for nums and bools |
+ | tautLib | tautology prover |
+ | HolBddLib | BDD-based state-exploration tools |
+ | HolSatLib | support for external satisfiability tools |
+ | HolSmtLib | support for external SMT tools |
+ | hol88Lib | support for hol88 compatibility |
+ | liteLib | support for HOL-Light portability |
+ ----------------------------------------------------------------
