■ HOL Lightにおいては，集合は，述語と見做せるよう定義されています． let IN = new_definition `!P:A->bool. !x. x IN P P x`;; ■ 集合のconstantには (typ) (typは:num，:realなどのhol.type) EMPTY or {} UNIV があり，UNIVは # `x+ &1 IN UNIV`;; val …

HOL Light上で関数を定義する道具としては，new_definition(: term -> thm = )は既に述べましたが，例えば # let fib = new_definition `fib n = if n = 0 \/ n = 1 then 1 else fib(n - 1) + fib(n - 2)`;; Exception: Failure "new_definition: term not c…

m:numから始まる帰納法の原理numm_INDUCTIONを証明し，それを適用するtactic，INDUCTm_TACを定義しましょう． まずは肩慣らしに，1から始まるものを証明して見ます． g ( `!P. P 1 /\ (!n. 1 P n ==> P (SUC n) ) ==> (!n. 1 P n)` );; e ( STRIP_TAC THEN S…

これまでの知識＋αを用いて，帰納法による証明を幾つか作って見ましょう．■ :num 上の不等式についてのthm |- !n. 2 EXP n >= 1 + n ポイントは # EXP;; val it : thm = |- (!m. m EXP 0 = 1) /\ (!m n. m EXP SUC n = m * m EXP n) および，帰納法の仮定の…

今回は # g( `!p q. p*p=2*q*q ==> q=0` );; val it : goalstack = 1 subgoal (1 total)`!p q. p * p = 2 * q * q ==> q = 0` をpについての wellfounded induction で証明します．方針は，p*p=2*q*qならばpは偶数，p=2r従って2*r*r=q*qと表せて仮定が使える…

通常の帰納法の原理 # num_INDUCTION;; val it : thm = |- !P. P 0 /\ (!n. P n ==> P (SUC n)) ==> (!n. P n) を用いて，Wellfounded induction（整礎帰納法）の原理 # num_WF;; val it : thm = |- !P. (!n. (!m. m P m) ==> P n) ==> (!n. P n) を証明して…

今回は，特称量化にも対応した一般の半代数系の prover についてです．■ まず，:num，:intにおける線形系のそれは #use "Examples/cooper.ml";; とロードして使う，Cooperのアルゴリズムに基づく関数，COOPER_RULE，INT_COOPERです． # ARITH_RULE `?x. 0=x`…

では，非線形系の自動処理はどの程度実装されているのでしょう？ まず，変数どうしの積を含む方程式系の評価，つまり，環における prover として，NUM_RING，REAL_RINGがあります（INT_RINGはありませんが，環の構造を提供する関数RINGを用いれば実装可能で…

■ prover ARITH_RULE(: term -> thm = )の:int版，:real版としてINT_ARITH，REAL_ARITHがあるわけですが，それらの特徴は ・代数的な並び替えなら非線形でも扱える # INT_ARITH `!a b a' b' D:int. (a pow 2 - D * b pow 2) * (a' pow 2 - D * b' pow 2) = (…

今回は，HOL Lightにおける数の体系のお話です． これまでも多くの例で扱ってきたhol_typeが:numであり，これは自然数（非負整数）全体の集合でした．同様に，hol.mlのロードだけで利用できる:int，:realは整数，実数全体の集合であり #use "./Complex/make.…

今回は の帰納法による証明です．まず，左辺の和を # NSUM_CLAUSES_NUMSEG;; val it : thm = |- (!m. nsum (m..0) f = (if m = 0 then f 0 else 0)) /\ (!m n. nsum (m..SUC n) f = (if m という性質を持つnsumで表すと，goalは # g(`!n. nsum(0..n)(\k.2*k)…

便利なtheorem-tacticとtheorem-tacticalを幾つか述べます． ■ ASSUME_TAC thmとして仮定を追加する代わりに，LABELTAC_TAC "ラベル" thm とすると，その仮定にラベルが付けられます（というより，LABEL_TAC "" がASSUME_TACの実体です）．■ また，結論がimp…

前回残した ... val it : goalstack = 1 subgoal (1 total) 0 [`&0 `&0 &0 は，先のsubgoalのx,yを交換したものなので，同様に # e ( DISJ_CASES_TAC ( REAL_ARITH `&0 &0 0 [`&0 1 [`&0 `&0 &0 # e ( ASM_REWRITE_TAC[] );; val it : goalstack = 1 subgoal…

今回は，量化，論理結合，対称式を含んだ # g `!x y:real. &0 (&0 &0 val it : goalstack = 1 subgoal (1 total)`!x y. &0 (&0 &0 を場合分けを用いて証明します．なお，証明自体は，REAL_FIELDでは # REAL_FIELD `!x y. &0 (&0 &0 と失敗しますが，MESONに …

前回述べたように，HOL Lightでは，goalの集まりであるgoalstackを用いて対話的に証明が作成できます．具体的には，*_TAC の名前を持つ，tactic（戦略関数) を，必要に応じてやり直し・訂正を加えながら，goalstackに段階的に適用することで，その中にある自…

HOL Lightでは，CONJやMPといった推論規則を順次適用する証明作成も原理的には可能ですが，得られる中間結果の授受は少し退屈です．これに対して，証明したい論理式termをgoalとして，それを展開してより簡単なsubgoalsの証明に帰する，下から上への証明作成…

さて，rewritingは数学においてごく普通の処理ですから，HOL Lightは，複数のtheoremsを合わせて参照する，より高度なrewriting conversionを提供します． その最も一般的なものが GEN_REWRITE_CONV convl [th1; ...; thn] (: (conv -> conv) -> thm list ->…

このREWR_CONV(: thm -> term -> thm = )を先のdepth conversions(: conv -> conv = )のもとで用いれば，等式についてのtheoremから導ける限りのtermの書き換えが可能になります． 例えば # let tm = `(a + b) + ((c + d) + e) + f + g + h` ;; val tm : ter…

|- p ==> q と |- p から |- q を得るMP(: thm -> thm -> thm = )を用いる際 # LT_IMP_LE;; val it : thm = |- !m n. m m # MP (SPECL[`1`;`2`] it) (ARITH_RULE`1 val it : thm = |- 1 のように，SEPC(: term -> thm -> thm = )，SEPCL(: term list -> thm …

termの中に現れるtermのconversionには，個々のconvを適用する位置や回数，順序などを指定するconversional関数(: conv -> conv = )を用います． RAND_CONV conv tm における RAND_CONV は，tm内のrand tmにconvを適用します．例えば rand `1 + 2 + 3`;; val…

conversionsによる処理の優位性は，それらを制御して，より複雑なconversionを生成するconversionalと呼ばれる関数(: conv -> conv = )の存在にあります． 今回はその中でも，複数のconversionsを組み合わせるものを紹介します．■ まず，次に定義するTHENC関…

HOL Lightは，あるtermが別のtermと等価である（:numなどの場合は=，:boolの場合はで結ばれる）ことを，体系的な変形を経て示す為，様々なconversionsを提供します． conversionはterm -> thm typeの関数で，typeはARITH_RULEやMESON[]などのproverと同じで…

量化子のネストにおいて変数の依存関係に注意が必要であることは，連続と一様連続との違いを持ち出すまでもなく，明らかでしょう． さて，先に述べたトートロジーprover TAUTでは，自明でない量化された式の評価はできません，HOL Light には，model elimina…

HOL Lightの変数の束縛は，abstractionによるもののみですから，例えば，全称量化子 `(!)` も，述語Pをlambda-abstractionと見て，それが任意のxに対して，Tを返すlambda-abstraction (\x.T) と一致することとして定義されます． # FORALL_DEF;; val it : th…

(* 本章より，入力行の先頭の#記号も記しますが，それ自体は入力ではありません．*) 前の章の最初に挙げたtermの４つの目の種類，abstractionsについて述べます． 3.3で紹介したINSTのtypeは # INST;; val it : (term * term) list -> thm -> thm = なので，…

HOL Lightでは新たなconstant（固定された数や関数など）を定義することもできます．それにはnew_definition関数を用いて，その定義をtheoremにすればよいのです． let def_of_wordlimit = new_definition `wordlimit = 2 EXP 32`;; val def_of_wordlimit : …

ここでSYMがどのように定義されているかを見るため，幾つか準備します． ・先の挙げたMPの等式版関数にEQ_MPがあり，それは A |- p ⇔ q と B |- p から A∪B |- q を得るもので let e1=ARITH_RULE `1=1 1+1=2`;; val e1 : thm = |- 1 = 1 1 + 1 = 2 let e2 =A…

HOL Lightにおいて等式は，数学におけるそれよりも特に基本的です．例えば，Iffは=記号にしても構いません．ただし，結合の強さと向き，typeの推量機能のため，時に括弧が必要です． `p /\ x = 1 q`;; val it : term = `p /\ x = 1 q` `p /\ x = 1 = q`;; va…