7.3 Matching

　|- p ==> q と |- p から |- q を得るMP(: thm -> thm -> thm = )を用いる際

# LT_IMP_LE;;
val it : thm = |- !m n. m < n ==> m <= n
# MP (SPECL[`1`;`2`] it) (ARITH_RULE`1<2`);;
val it : thm = |- 1 <= 2

のように，SEPC(: term -> thm -> thm = )，SEPCL(: term list -> thm -> thm = )，INST(: (term * term) list -> thm -> thm = )などを用いて，pを完全に同じtermに揃える前処理は面倒でしょう．この全称量化の束縛変数や自由変数への代入をパターンマッチにより代行してくれるのが，MATCH_MP(: thm -> thm -> thm = )です．

# LT_IMP_LE;;
val it : thm = |- !m n. m < n ==> m <= n
# MATCH_MP it (ARITH_RULE`1<2`);;
val it : thm = |- 1 <= 2

　termの書き換え(rewriting)の基礎となる REWR_CONV(: thm -> term -> thm = )は，第一引数 |- !x. s=t または |- s=t に対して，第二引数 s'がsにマッチするとき，|- s'=t'を返します．例えば

# ADD_SYM;;
val it : thm = |- !m n. m + n = n + m
# REWR_CONV ADD_SYM `1+2`;;
val it : thm = |- 1 + 2 = 2 + 1

もちろん，:boolの要素なら=は<=>です．

# LE_LT;;
val it : thm = |- !m n. m <= n <=> m < n \/ m = n
# REWR_CONV LE_LT `1<=2`;;
val it : thm = |- 1 <= 2 <=> 1 < 2 \/ 1 = 2

　マッチングはabstractionに対しても適用され，これを高階マッチングと呼びます．次の例は，ド・モルガン則の無限版です．

# NOT_FORALL_THM;;
val it : thm = |- !P. ~(!x. P x) <=> (?x. ~P x)
# let NOT_FORALL_CONV = REWR_CONV NOT_FORALL_THM;;
val ( NOT_FORALL_CONV ) : term -> thm =

これが

# NOT_FORALL_CONV `~(!n. EVEN n)`;;
val it : thm = |- ~(!n. EVEN n) <=> (?n. ~EVEN n)

のように働くのは見易いですが，次にもマッチします．

# NOT_FORALL_CONV `~(!n. n * n = n + n)`;;
val it : thm = |- ~(!n. n * n = n + n) <=> (?n. ~(n * n = n + n))

この処理は，!nの本体をabsで表した状態のものを評価し，それをbeta変換することで実現されています．

# NOT_FORALL_CONV `~(!n. (\k. k * k = k + k) n)`;;
val it : thm =
|- ~(!n. (\k. k * k = k + k) n) <=> (?n. ~(\k. k * k = k + k) n)
# CONV_RULE(ONCE_DEPTH_CONV BETA_CONV) it;;
val it : thm = |- ~(!n. n * n = n + n) <=> (?n. ~(n * n = n + n))

　このCONV_RULE(: conv -> thm -> thm = )は

# ARITH_RULE`(1+2)+3=2+(2+2)`;;
val it : thm = |- (1 + 2) + 3 = 2 + 2 + 2
# CONV_RULE(ONCE_DEPTH_CONV NUM_ADD_CONV) it;;
val it : thm = |- 3 + 3 = 2 + 4
# CONV_RULE(ONCE_DEPTH_CONV NUM_ADD_CONV) it;;
val it : thm = |- 6 = 6

のように，CONV_RULE conv thm により，convを用いてthmを書き換えたthm'を返す，REWR_CONVのthm適用版（推論規則版）です．