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
などをご参照ください.