14.1 Choice and the select operator

　これまで述べなかった述語あるいは集合に対する作用子の一つとして，選択関数@(:(A->bool)->bool)があります．それは，!や?と同じくbinder（従って，括弧付きで用いられるもの）であり，述語 P に対して (@)P は，Pを満たす元があるならその一つ（何れかは不明）を表し，もしなければ返し任意の元を表します．すなわち

# SELECT_AX;;
val it : thm = |- !P x. P x ==> P ((@) P)

であり，例えば

# SET_RULE `(@)(:num) IN (:num)`;;
val it : thm = |- (@) (:num) IN (:num)
# ARITH_RULE `(@)(:num)>=0`;;
val it : thm = |- (@) (:num) >= 0

となります．

　そして，absとしての述語 \x.P(x) に作用させたものは，@x. P(x) と略記できます．所謂，x s.t. P(x) です．

# SET_RULE `(@x. (:num) x) IN (:num)`;;
val it : thm = |- (@x. (:num) x) IN (:num)

# SET_RULE `(@n:num. n=0 \/ n=1) IN {0,1}`;;
0..0..solved at 2
val it : thm = |- (@n. n = 0 \/ n = 1) IN {0, 1}

　簡単なものは，MESONにも通じます．

# MESON[] `(!x. P x ==> Q x) /\ P a ==> Q(@x. P x)`;;
Warning: inventing type variables
0..0..1..3..solved at 7
val it : thm = |- (!x. P x ==> Q x) /\ P a ==> Q (@x. P x)

　この@は他の定理の証明において用いるのが一般的であり，その最も重要な例の一つが選択公理です．選択公理は，例えば，任意の述語pに対して「任意のxに対してyが存在してp(x,y)となるならば，関数fが存在して任意のxに対してp(x,f(x))となる」と表現される性質であり，HOL Lightでは，選択関数により証明可能なthmとなります．すなわち

# g ( `!p. (!x:A. ?y:B. p(x,y)) ==> (?f:A->B. !x. p(x,f(x)) )` ) ;;
val it : goalstack = 1 subgoal (1 total)

`!p. (!x. ?y. p (x,y)) ==> (?f. !x. p (x,f x))`

# e (REPEAT STRIP_TAC);;
val it : goalstack = 1 subgoal (1 total)

0 [`!x. ?y. p (x,y)`]

`?f. !x. p (x,f x)`

# e( EXISTS_TAC `( \x. (@y. (p:A#B->bool)(x,y) ) )` );;
val it : goalstack = 1 subgoal (1 total)

0 [`!x. ?y. p (x,y)`]

`!x. p (x,(\x. @y. p (x,y)) x)`

# e(ASM_MESON_TAC[]);;
0..0..1..solved at 4
val it : goalstack = No subgoals

# top_thm();;
val it : thm = |- !p. (!x. ?y. p (x,y)) ==> (?f. !x. p (x,f x))

　なお，所謂，スコーレム化 ( http://en.wikipedia.org/wiki/Skolem_normal_form )

# SKOLEM_THM;;
val it : thm = |- !P. (!x. ?y. P x y) <=> (?y. !x. P x (y x))

を参照するなら

# prove( `!p. (!x:A. ?y:B. p(x,y)) ==> (?f:A->B. !x. p(x,f(x)) )` , MESON_TAC[S
KOLEM_THM] ) ;;
Warning: No useful-looking instantiations of lemma
0..0..solved at 2
val it : thm = |- !p. (!x. ?y. p (x,y)) ==> (?f. !x. p (x,f x))

と簡単ですが，Warningの通り，参照しなくても

# prove( `!p. (!x:A. ?y:B. p(x,y)) ==> (?f:A->B. !x. p(x,f(x)) )` , MESON_TAC[]
) ;;
0..0..solved at 2
val it : thm = |- !p. (!x. ?y. p (x,y)) ==> (?f. !x. p (x,f x))

と出来てしまいます．