6.1 Quantifiers

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

# FORALL_DEF;;
val it : thm = |- (!) = (\P. P = (\x. T))
# `(!) (\n. n>=0)`;;
val it : term = `!n. n >= 0`
# dest_comb it;;
val it : term * term = (`(!)`, `\n. n >= 0`)
# mk_comb it;;
val it : term = `!n. n >= 0`

　lambdaや量化子は変数を束縛するように見えることからbinderと呼ばれ，当面，重要な量化子は

!　For all　∀
?　There exists　∃
?!　There exists a unique　∃!

の３つです．
　また，λx.(λy.F) は λx y.F と略せます．

# `\x. \y. x+y`;;
val it : term = `\x y. x + y`

同様に

# `!m. !n. m+n=n+m`;;
val it : term = `!m n. m + n = n + m`

となります．
　全ての量化子には導入と除去の推論規則があります
．全称量化子に対しては，theoremの１つの自由変数を全称量化する GEN(: term -> thm -> thm = )，逆にtheoremの全称量化された変数にtermを当てはめる SPEC(: term -> thm -> thm = )，それぞれのリスト版 GENL，SPECL(: term list -> thm -> thm = )があり，SPECLは量化子に続く順に当てはめられます．

# REFL `x=1`;;
val it : thm = |- x = 1 <=> x = 1
# GEN `x:num` (REFL `x=1`);;
val it : thm = |- !x. x = 1 <=> x = 1
# SPEC `2` it;;
val it : thm = |- 2 = 1 <=> 2 = 1
# GENL [`x:num`;`y:num`] (REFL `x=y:num`);;
val it : thm = |- !x y. x = y <=> x = y
# SPECL [`2`;`1`] it;;
val it : thm = |- 2 = 1 <=> 1 = 2

　なお，GEN，GENLを用いて，仮定に現れる自由変数を量化することできません．

# ASSUME`x=1`;;
val it : thm = x = 1 |- x = 1
# GEN `x:num` it;;
Exception: Failure "ABS".

　また，theoremは，その全称閉包と等価ですから，例えば

# ARITH_RULE`p:bool<=>(!x:num.p)`;;
val it : thm = |- p <=> (!x. p)

のようになります．
　一方，SPEC，SPECLは全称で述べられた既存のtheoremを利用する際に役立ちます．

# #use "Library/analysis.ml";;
...
# let th1 = SPEC `&1 / &2` SEQ_POWER and
　　　th2 = REAL_FIELD `abs(&1/ &2)< &1`;;
1 basis elements and 0 critical pairs
val th1 : thm =
|- abs (&1 / &2) < &1 ==> (\n. (&1 / &2) pow n) tends_num_real &0
val th2 : thm = |- abs (&1 / &2) < &1
# MP th1 th2;;
val it : thm = |- (\n. (&1 / &2) pow n) tends_num_real &0