5.2 Pairing

　curringは，OCamlの殆ど，HOL Lightの全ての中置き２項演算子に使われていますが，順序対がないわけではなく，OCaml，HOL Light，それぞれにおいて

# 1,2;;
val it : int * int = (1, 2)
# type_of `1,2`;;
val it : hol_type = `:num#num`

のようになっています．なお

# 1,2;;
val it : int * int = (1, 2)
# (1,2);;
val it : int * int = (1, 2)
# `1,2`;;
val it : term = `1,2`
# `(1,2)`;;
val it : term = `1,2`

のように，OCamlでは括弧付き，HOL Lightでは括弧なしの出力になっています．そして，HOL Lightでは

# get_infix_status ",";;
val it : int * string = (14, "right")

なので，順序対もcurringにより実装されていることが判ります．そのことは

# `(1,(2,(3)))`=`1,2,3`;;
（注：この=はOCamlのものなので直ちに評価される）
val it : bool = true

のように確認できます．
　なお，順序対の要素の抽出には，7.4で述べるREWRITE_CONV(: thm list -> conv = )が参照する

# basic_rewrites();;

で表示されるtheoremsのリストにあるFST(x,y)，SND(x,y)が，それぞれx，yであり

# ARITH_RULE `FST(1,2)=1`;;
val it : thm = |- FST (1,2) = 1

となります．
　また，幾つかの関数はcurryingではなく，順序対を引数として定義されています．
　関数のtermと，それが作用できるような引数のtermの順序対に対して，その関数値を返すmk_combは

# type_of`(+) x`;;
val it : hol_type = `:num->num`
# mk_comb(`(+) x`,`y:num`);;
val it : term = `x + y`

のように働き，このtheorem版MK_COMBは，theoremの順序対 ( A |- f=g , B |- x=y )からtheorem A∪B |- f x = g yを得るもので

# ( ASSUME`(+) 2 = (+) (1 + 1)` , ARITH_RULE`3 + 3 = 6` );;
val it : thm * thm =
((+) 2 = (+) (1 + 1) |- (+) 2 = (+) (1 + 1), |- 3 + 3 = 6)
# MK_COMB it;;
val it : thm = (+) 2 = (+) (1 + 1) |- 2 + 3 + 3 = (1 + 1) + 6

のように働き，推論規則CONJ_PAIRは，A |- p /\ q というtheoremからtheoremの順序対 ( A |- p , A |- q ) を得るもので，分解には fst, snd (: 'a * 'b -> 'a = )を用います．

# ASSUME `p /\ q`;;
val it : thm = p /\ q |- p /\ q
# let pq = CONJ_PAIR it;;
val it : thm * thm = (p /\ q |- p, p /\ q |- q)
# fst pq;;
val it : thm = p /\ q |- p
# snd pq;;
val it : thm = p /\ q |- q

のように働きます．