4.2 Low-level logical rules

　TAUTのような高い自動性をもつ規則関数と同様，HOL Lightには，繊細な推論用の「導入」と「除去」の規則関数があります．
　まず，２つのtheorem，A |- p，B |- qからtheorem A∪B |- p∧q を得る規則，つまり，∧を導入するのがCONJです．

let thp = ASSUME `p:bool`;;
val thp : thm = p |- p
let thq = ASSUME `q:bool`;;
val thq : thm = q |- q
let thpq = CONJ thp thq;;
val thpq : thm = p, q |- p /\ q

これに対して，上のthpqの結論から，p，qを取り出したtheoremを得るのが，それぞれCONJUNCT1，2です．

CONJUNCT1 thpq;;
val it : thm = p, q |- p
CONJUNCT2 thpq;;
val it : thm = p, q |- q

です．
　また，重要なmodus ponens，A |- p→q と B |- p から A∪B |- q を得る規則の実装が関数MPであり，例えば，ARITH_RULEと組み合わせると

let th1 = ARITH_RULE `x <= y ==> x < y + 1`;;
val th1 : thm = |- x <= y ==> x < y + 1
# let th2 = ASSUME `x <= y`;;
val th2 : thm = x <= y |- x <= y
MP th1 th2;;
val it : thm = x <= y |- x < y + 1

のようになります（th1 th2 の順に注意）．これを一気に行うには，UNDISCH_ALLを用います．

ARITH_RULE `x <= y ==> x < y + 1`;;
val it : thm = |- x <= y ==> x < y + 1
UNDISCH_ALL it;;
val it : thm = x <= y |- x < y + 1