HOL4 の使い方(1)

HOL4 のインストールスクリプト
http://d.hatena.ne.jp/ehito/20130219/1361260859
に書きましたが,システムとして HOL Light と大きく異なる点を幾つか述べます.

まず,ライブラリーのロードとオープンについてです.

デフォルトでの起動では,例えば

- Induct;
> val it = fn : term list * term -> (term list * term) list * (thm list -> thm)

は良くても

- INDUCT_TAC;
! Toplevel input:
! INDUCT_TAC;
! ^^^^^^^^^^
! Unbound value identifier: INDUCT_TAC

のように知らぬ素振です.ところが help で尋ねると

- help"INDUCT_TAC";

    ----------------------------------------------------------------------
    |   1 | HOL numLib.INDUCT_TAC (help/Docfiles/numLib.INDUCT_TAC.adoc) |
    |   2 | val  numLib.INDUCT_TAC                                       |
    ----------------------------------------------------------------------

Choose number to browse, or quit: q
> val it = () : unit

のようにご存知なので,フルネームで呼べば

- numLib.INDUCT_TAC;
> val it = fn : term list * term -> (term list * term) list * (thm list -> thm)

と答えてくれます.

これは HOL4 が起動時に INDUCT_TAC が収められている numlib.uo をロードするものの,下の名前だけで使えるようにオープンはしないことが原因です.

実際,loaded() を用いて,ロードされてるライブラリーを確認すると

- printLength:=10000; (* PolyML.print_depth 10000; *)
> val it = () : unit
- loaded();
> val it =
    ["mlibArbnum", "mlibStream", "Norm_bool", "pairLib", "TypeBase", "Word",
     "Nonce", "Binarymap", "numLib", "reduceLib", "mlibMeson", "boolLib",
     "Absyn", "Process", "Raw-sig", "Globals", "PairedLambda", "listTheory",
     "ind_types", "Rsyntax", "term_grammar", "Char", "operatorTheory",
     "IndDefLib", "Canon_Port", "clauses", "Parse_support", "metisTools",
     "mlibClauseset", "History", "Hol_pp", "term_pp", "Lib", "CharArraySlice",
     "mlibTermnet", "Travrules", "markerTheory", "RecordType", "liteLib",
     "boolSyntax", "Pretype", "TheoryDelta", "base_tokens", "EvalRef",
     "equations", "Psyntax", "Date", "Lift", "GenPolyCanon", "errormonad",
     "Preterm", "parse_type", "locn", "pred_setLib", "Norm_ineqs",
     "dimacsTools", "ParseExtras", "HOLtokens", "CharSet", "UnicodeChars",
     "CommandLine", "Net-sig", "folMapping", "mlibArbint", "Term_coeffs",
     "pairSyntax", "optionTheory", "parse_term", "FunctionalRecordUpdate",
     "Vector", "numSimps", "mlibParser", "mlibPortable", "PairRules",
     "ThmSetData", "InductiveDefinition", "term_pp_utils", "FinalThm-sig",
     "basicSizeTheory", "NumRelNorms", "Sol_ranges", "mlibRewrite", "Mutual",
     "pureSimps", "Trace", "Manager", "TexTokenMap", "compute_rules", "Drule",
     "Theory", "Strbase", "Redblackset", "type_pp", "SharingTables", "mlibThm",
     "arithmeticTheory", "prim_recTheory", "mesonLib", "HolSatLib",
     "combinTheory", "Ho_Net", "basicSize", "Prenex", "matchTools",
     "jrhTactics", "Tactical", "optionSimps", "Intset", "relationTheory",
     "Tactic", "Misc", "Real", "Mosml", "Induction", "Arithconv", "refuteLib",
     "type_tokens", "MLstring", "Byte", "KernelSig", "Exists_arith",
     "Theorems", "Thm_cont", "ProvideUnicode", "IO", "boolSimps",
     "minisatParse", "HOLgrammars", "Subst", "KernelTypes", "BasicProvers",
     "Binaryset", "Help", "Instance", "Solve_ineqs", "def_cnf",
     "BoundedRewrites", "GrammarSpecials", "TypeNet", "FileSys", "sumSyntax",
     "numSyntax", "pairTools", "Arbrat", "boolTheory", "Bool", "TextIO",
     "Defn", "Abbrev", "Lexis", "mlibClause", "normalFormsTheory",
     "MLSYSPortable", "Num_conv", "base_lexer", "PP", "ParseDatatype",
     "Thm_convs", "Word8", "FinalType-sig", "mlibTptp", "mlibMetis",
     "mlibPatricia", "SatSolvers", "term_tokens", "Tag", "Susp", "listSimps",
     "EnumType", "GenRelNorm", "pairTheory", "minisatResolve", "satTools",
     "Arbnum", "Type", "pred_setSyntax", "minisatProve", "Dynarray",
     "Holmake_types", "Pmatch", "Random", "Ho_Rewrite", "DefnBase",
     "type_grammar", "qbuf", "Word8ArraySlice", "Thm", "tautLib", "dpll",
     "Prim_rec", "Term", "Solve", "Unwind", "markerLib", "Traverse",
     "PFset_conv", "TotalDefn", "DataSize", "mlibMeter", "mlibTermorder",
     "IndDefRules", "CoreKernel-sig", "Word8Array", "mlibSubst", "Cond_rewr",
     "TermCoding", "smpp", "Word8Vector", "folTools", "mlibSolver",
     "mlibOmegaint", "PPBackEnd", "Obj", "HolKernel", "sumSimps", "Arith",
     "Overload", "pred_setSimps", "proofManagerLib", "ind_typeTheory",
     "mlibSupport", "Rewrite", "ListPair", "oneSyntax", "Cache", "pairSimps",
     "AC", "seq", "Math", "BasicIO", "Portable", "Time", "UniversalType",
     "Array2", "Boolconv", "metisLib", "mlibMatch", "Overlay",
     "mlibResolution", "mlibLiteralnet", "mlibOmega", "Substring", "HOLPP",
     "OS", "List", "mlibUseful", "sumTheory", "Arbint", "TypeBasePure",
     "VectorSlice", "Array", "numTheory", "simpfrag", "ArraySlice",
     "FinalTerm-sig", "FinalTag-sig", "Canon", "internal_functions",
     "Arbintcore", "TermParse", "Feedback", "normalForms", "StringCvt", "Net",
     "PGspec", "numeralTheory", "Option", "Int", "bossLib", "listSyntax",
     "mlibHeap", "goalTree", "LVTermNet", "String", "Rules", "seqmonad",
     "optmonad", "CharVectorSlice", "pred_setTheory", "Sup_Inf",
     "markerSyntax", "CharArray", "Norm_arith", "RW", "Listsort", "Rationals",
     "Path", "Count", "Gen_arith", "Streams", "Polyhash", "Q", "Parse",
     "Systeml", "CharVector", "numpairTheory", "mlibKernel", "satConfig", "DB",
     "stmonad", "combinSimps", "goalStack", "PSet_ind", "Int_extra", "UTF8",
     "HOLset", "Redblackmap", "optionSyntax", "Datatype", "TheoryPP",
     "Arbnumcore", "whileTheory", "Opening", "UTF8Set", "Coding", "Arith_cons",
     "ReadHMF", "Conv", "Word8VectorSlice", "basicSizeSyntax", "mlibModel",
     "mlibCanon", "Intmap", "RJBConv", "oneTheory", "satTheory", "computeLib",
     "Sub_and_cond", "mlibUnits", "mlibSubsume", "satCommonTools", "Timer",
     "EmitTeX", "Functional", "wfrecUtils", "Literal", "mlibMultiset",
     "mlibTerm", "combinSyntax", "BoolExtractShared", "simpLib",
     "term_pp_types", "BinIO"] : string list

のようになっており,"numLib" も上から2行目に表示されています.

以降,下の名前 INDUCT_TAC のみで呼べるようにするには,open を用いて

- open numLib;
> type validation = thm list -> thm
  type 'a quotation = 'a frag/1 list
  type defn = defn
  type thm = thm
  type term = term
  type rule = thm -> thm
  type thm_tactic =
  thm -> term list * term -> (term list * term) list * (thm list -> thm)
  type thm_tactical =
  (thm -> term list * term -> (term list * term) list * (thm list -> thm)) ->
  thm -> term list * term -> (term list * term) list * (thm list -> thm)
  type goal = term list * term
  type hol_type = hol_type
  type conv = term -> thm
  type tactic = term list * term -> (term list * term) list * (thm list -> thm)
  type ppstream = ppstream/1
  type ('a, 'b) subst = {redex : 'a, residue : 'b} list
  val dest_div2 = fn : term -> term
  val dest_even = fn : term -> term
  val DECIDE = fn : term -> thm

...

  val REDUCE_TAC = fn :
  term list * term -> (term list * term) list * (thm list -> thm)
  val REDUCE_CONV = fn : term -> thm
  val mk_div2 = fn : term -> term
  val mk_even = fn : term -> term
  val SUC_ELIM_CONV = fn : term -> thm
  val is_odd = fn : term -> bool
  val dest_mod_2exp = fn : term -> term * term
  val list_mk_plus = fn : term list -> term
  val dest_cmeasure = fn : term -> term
  val is_while = fn : term -> bool
  val mult_tm = ``$*`` : term
  val is_least = fn : term -> bool
- 

のようにすれば

- INDUCT_TAC ;
> val it = fn : term list * term -> (term list * term) list * (thm list -> thm)

となります.

次は明示的なロードです.例えば

- NUM_RING_CONV;
! Toplevel input:
! NUM_RING_CONV;
! ^^^^^^^^^^^^^
! Unbound value identifier: NUM_RING_CONV
- help"NUM_RING_CONV";

+ signature numRingLib =
+ sig
+   include Abbrev
+ 
+   val NUM_NORM_CONV : conv
@>  val NUM_RING_CONV : conv
+ 
+   val NUM_NORM_TAC : tactic
+   val NUM_RING_TAC : tactic
+ 
+   val NUM_NORM_RULE : thm -> thm
+   val NUM_RING_RULE : thm -> thm
+ 
+ end
> val it = () : unit

なので,フルネームで呼んでみても,今度は

- numRingLib.NUM_RING_CONV;
! Toplevel input:
! numRingLib.NUM_RING_CONV;
! ^^^^^^^^^^^^^^^^^^^^^^^^
! Cannot access unit numRingLib before it has been loaded.

と叱られます.実際,loaded() で表示されたリストに "numRingLib" はありません.そこで,load を用いて

- load "numRingLib";
> val it = () : unit

とロードすれば

- numRingLib.NUM_RING_CONV;
> val it = fn : term -> thm

さらに,先と同様にオープンすれば

- open numRingLib;
> type validation = thm list -> thm
  type 'a quotation = 'a frag/1 list
  type defn = defn
  type thm = thm
  type term = term
  type rule = thm -> thm
  type thm_tactic =
  thm -> term list * term -> (term list * term) list * (thm list -> thm)
  type thm_tactical =
  (thm -> term list * term -> (term list * term) list * (thm list -> thm)) ->
  thm -> term list * term -> (term list * term) list * (thm list -> thm)
  type goal = term list * term
  type hol_type = hol_type
  type conv = term -> thm
  type tactic = term list * term -> (term list * term) list * (thm list -> thm)
  type ppstream = ppstream/1
  type ('a, 'b) subst = {redex : 'a, residue : 'b} list
  val NUM_NORM_TAC = fn :
  term list * term -> (term list * term) list * (thm list -> thm)
  val NUM_RING_RULE = fn : thm -> thm
  val NUM_RING_TAC = fn :
  term list * term -> (term list * term) list * (thm list -> thm)
  val NUM_NORM_CONV = fn : term -> thm
  val NUM_NORM_RULE = fn : thm -> thm
  val NUM_RING_CONV = fn : term -> thm
- NUM_RING_CONV;
> val it = fn : term -> thm
-

のように下の名前で呼べるようになります.

以上をまとめると,定理やプルーフツールを用いるには,一般にはそれらが定義されているライブラリーを

load "ライブラリー名" ;

とロードして,更に,それらを下の名前で使いたければ

open ライブラリー名 ;

とするということです.なお,複数のライブラリーを処理するには,app で load をリストへ作用させて

app load ["ライブラリー名1", ... ,"ライブラリー名n"] ; 

ML である open はそのまま

open ライブラリー名1 ... ライブラリー名n ;

とします.ML については

http://tutorial.jp/prog/ml/mlkouza.txt

などをご参照ください.