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…