5.3 Equational reasoning (2)

　ここでSYMがどのように定義されているかを見るため，幾つか準備します．
・先の挙げたMPの等式版関数にEQ_MPがあり，それは A |- p ⇔ q と B |- p から A∪B |- q を得るもので

let e1=ARITH_RULE `1=1 <=> 1+1=2`;;
val e1 : thm = |- 1 = 1 <=> 1 + 1 = 2
let e2 =ARITH_RULE `1=1`;;
val e2 : thm = |- 1 = 1
EQ_MP e1 e2;;
val it : thm = |- 1 + 1 = 2

のように働きます．
・以下のような階層的な構成により，任意の深さの定義と表現が可能となります．

::= let
::=
　　　　　　| and
::= =
::=
　　　　　　　| in

　次の1つ目のxは大域変数，2つ目のxはin付きなので局所変数です．　

let x = 1 and y = 2;
val x : int = 1
val y : int = 2
let x = 10 and y = 20 in x + y;;
val it : int = 30
x;;
val it : int = 1

　なお，bindingは

let x,y = (1,2);;
val x : int = 1
val y : int = 2
let (x,y) = (`1`,`2`);;
val x : term = `1`
val y : term = `2`

のように変数のみではなく，より一般のpatternに対して可能です．
・AP_TERMは先に述べたMK_COMBと同等の働きですが

MK_COMB;;
val it : thm * thm -> thm =
AP_TERM;;
val it : term -> thm -> thm =

なので

MK_COMB( REFL`(*)1`,REFL`x:num` );;
val it : thm = |- 1 * x = 1 * x
AP_TERM `(*)1` (REFL`x:num`);;
val it : thm = |- 1 * x = 1 * x

のような違いがあります．
　では，導出された推論規則であるSYMの定義を見ましょう

let SYM th =
　let tm = concl th in
　let l,r = dest_eq tm in
　let lth = REFL l in
　EQ_MP (MK_COMB(AP_TERM (rator (rator tm)) th,lth)) lth;;

各ステップを |- 1+1=2 から |- 2=1+1 を得る場合を例に実行して見ます．

# let th = ARITH_RULE`1+1=2`;;
val th : thm = |- 1 + 1 = 2
# let tm = concl th;;
val tm : term = `1 + 1 = 2`
# let l,r=dest_eq tm;;
val l : term = `1 + 1`
val r : term = `2`
# let lth = REFL l;;
val lth : thm = |- 1 + 1 = 1 + 1
# rator tm;;
val it : term = `(=) (1 + 1)`
# (rator (rator tm));;
val it : term = `(=)`
# AP_TERM it th;;
val it : thm = |- (=) (1 + 1) = (=) 2
# MK_COMB( it , lth );;
val it : thm = |- 1 + 1 = 1 + 1 <=> 2 = 1 + 1
# EQ_MP it lth;;
val it : thm = |- 2 = 1 + 1

以上を一気に行うのが

# th;;
val it : thm = |- 1 + 1 = 2
# SYM th;;
val it : thm = |- 2 = 1 + 1

と言うわけです．