QUICK_REFERENCE

　今回からは，QUICK_REFERENCE.txt，VERYQUICK_REFERENCE.txtに沿って進みたいと思います．

■ thm: (HOL Light's 10 primitive inference rules) + α

REFL `x` gives `|- x = x`

# REFL `x:num` ;;
val it : thm = |- x = x
# REFL `x:bool` ;;
val it : thm = |- x <=> x

ASSUME `a` gives `a |- a`

# ASSUME`x=1`;;
val it : thm = x = 1 |- x = 1

TRANS `ASM1 |- a = b` `ASM2 |- b = c`
gives `ASM1+ASM2 |- a = c`

# TRANS (ASSUME`p:bool=q`) (ASSUME`q:bool=r`);;
val it : thm = p <=> q, q <=> r |- p <=> r
# TRANS (ARITH_RULE`x=1<=>2*x=2`) (ARITH_RULE`2*x=2<=>2*x+1=3`);;
val it : thm = |- x = 1 <=> 2 * x + 1 = 3

IMP_TRANS `ASM1 |- a ==> b` `ASM2 |- b ==> c`
gives `ASM1+ASM2 |- a ==> c`

# IMP_TRANS (ARITH_RULE`x=1==>2*x=2`) (ARITH_RULE`2*x=2==>2*x+1=3`);;
val it : thm = |- x = 1 ==> 2 * x + 1 = 3

ABS `x` `ASM1-{x} |- a=b`
gives `ASM1 |- \x.a = \x.b`

# ABS `x:num` (ASSUME`x=1:num`);;
Exception: Failure "ABS".
# ABS `y:num` (ASSUME`x=1:num`);;
val it : thm = x = 1 |- (\y. x) = (\y. 1)

MK_COMB (`ASM1 |- f = g`, `ASM2 |- a = b`)
gives `ASM1+ASM2 |- (f a) = (g b)`

# let fg, xy= (ABS `x:num` (ARITH_RULE`x+1=1+x`)), (ARITH_RULE`2*3=6`);;
val fg : thm = |- (\x. x + 1) = (\x. 1 + x)
val xy : thm = |- 2 * 3 = 6
# MK_COMB(fg,xy);;
val it : thm = |- (\x. x + 1) (2 * 3) = (\x. 1 + x) 6

BETA is useless; use BETA_CONV

# BETA `(\x. x+1) x`;;
val it : thm = |- (\x. x + 1) x = x + 1
# BETA `(\x. x+1) y`;;
Exception: Failure "BETA: not a trivial beta-redex".
# BETA_CONV `(\x. x+1) y`;;
val it : thm = |- (\x. x + 1) y = y + 1

EQ_MP `ASM1 |- a = b` `ASM2 |- a`
gives `ASM1+ASM2 |- b`

# EQ_MP (ARITH_RULE`x=1<=>2*x=2`) (ASSUME`x=1`);;
val it : thm = x = 1 |- 2 * x = 2

MP `ASM1 |- a ==> b` `ASM2 |- a`
gives `ASM1+ASM2 |- b`

# MP (ARITH_RULE`x=1==>2*x=2`) (ASSUME`x=1`);;
val it : thm = x = 1 |- 2 * x = 2

MATCH_MP ith th is like MP,
except it uses matching
instead of requiring an exact match.

# MP (ARITH_RULE`x=1==>2*x=2`) (ASSUME`y=1`);;
Exception: Failure "MP: theorems do not agree".
# MATCH_MP (ARITH_RULE`x=1==>2*x=2`) (ASSUME`y=1`);;
val it : thm = y = 1 |- 2 * y = 2
# MATCH_MP (ARITH_RULE`!x. x=1==>2*x=2`) (ASSUME`y=1`);;
val it : thm = y = 1 |- 2 * y = 2

DEDUCT_ANTISYM_RULE `ASM1 |- a` `ASM2 |- b`
gives `(ASM1-{b})+(ASM2-{a}) |- a=b`
つまり，`ASM1 |- a` を `ASM1-{b} |- b==>a`，
`ASM2 |- b` を `ASM2-{a} |- a==>b` にDISCH`b`,DISCH`a`して，CONJしたもの．従って

# let th1,th2 = SYM(ASSUME `x:num = y`) ,SYM(ASSUME `y:num = x`);;
val th1 : thm = x = y |- y = x
val th2 : thm = y = x |- x = y
# DEDUCT_ANTISYM_RULE th1 th2;;
val it : thm = |- y = x <=> x = y

INST_TYPE instantiation theorem
gives a new theorem with type variables instantiated

# SPECL [`a:num`; `b:num`] EQ_SYM_EQ ;;
Exception: Failure "SPECL".
# SPECL [`a:num`; `b:num`] (INST_TYPE [`:num`,`:A`] EQ_SYM_EQ) ;;
val it : thm = |- a = b <=> b = a

INST instantiation:(new term * free term in theorem)list theorem
gives a new theorem with variables instantiated

# let th = SPEC_ALL ADD_SYM;;
val th : thm = |- m + n = n + m
# INST [`1`,`m:num`; `x:num`,`n:num`] th;;
val it : thm = |- 1 + x = x + 1