bool(5) - ATPとCASのこと

!の定義．

FORALL_DEF: `(!) = \P:A->bool. P = \x. T`
SPEC `a` `ASM |- !x.P[x]` gives `ASM |- P[a]`
SPECL [`a`;`b`;`c`] `ASM |- !x y z.P[x,y,z]` gives `ASM |- P[a,b,c]`
SPEC_VAR `ASM |- !x.P[x]` gives (`x17`, `ASM |- P[x17]`)
SPEC_ALL repeats SPEC_VAR until the conclusion is not a "forall", and returns
         the final theorem.
ISPEC is like SPEC, except that the specialized term may be an instance
      of the type of the quantified variable (in which case the theorem
      is type-instantiated first), rather than matching exactly.
ISPECL is like SPECL with type instantiations.
GEN `x` `ASM |- P[x]` gives `ASM |- !x. P[x]` (if x is not free in ASM)
GENL [`x`;`y`;`z`] `ASM |- P[x,y,z]` gives `ASM |- !x y z. P[x,y,z]`
GEN_ALL generalizes over all variables free in the conclusion but not
        in the assumptions

# ARITH_RULE `n + SUC m = m + n + 1` ;;
val it : thm = |- n + SUC m = m + n + 1
# GEN_ALL it;;
val it : thm = |- !m n. n + SUC m = m + n + 1
# ADD_ASSUM `n = 0` it;;
val it : thm = n = 0 |- !m n. n + SUC m = m + n + 1
# SPEC_ALL it;;
val it : thm = n = 0 |- n' + SUC m = m + n' + 1
# GEN_ALL it;;
val it : thm = n = 0 |- !m n'. n' + SUC m = m + n' + 1
# SPEC `n:num` it;;
val it : thm = n = 0 |- !n'. n' + SUC n = n + n' + 1

?の定義．

EXISTS_DEF: `(?) = \P:A->bool. !Q. (!x. P x ==> Q) ==> Q`
EXISTS (`?x. P[x]`,`a`) `ASM |- P[a]` gives `ASM |- ?x. P[x]`
SIMPLE_EXISTS `x` `ASM |- P[x]` gives `ASM |- ?x. P[x]`
CHOOSE (`x`,`ASM1 |- ?y.P[y]`) `ASM2,P[x] |- a` gives `ASM1+ASM2 |- a`
SIMPLE_CHOOSE `x` `ASM,P[x] |- a` gives `ASM,?x.P[x] |- a` (P[x] must be
              the first hypothesis)

EXISTS_TAC のもとになる推論．

# ARITH_RULE `1 EXP 3 + 1 = 2`;;
val it : thm = |- 1 EXP 3 + 1 = 2
# EXISTS (`?x:num. x EXP 3 + x = 2`, `1`) it ;;
val it : thm = |- ?x. x EXP 3 + x = 2

SIMPLE_EXISTS は結論への?の導入ですが，EXISTS のように項をwitnessにはできません．．

# ASSUME `x EXP 3 + x = 2`;;
val it : thm = x EXP 3 + x = 2 |- x EXP 3 + x = 2
# SIMPLE_EXISTS `x:num` it;;
val it : thm = x EXP 3 + x = 2 |- ?x. x EXP 3 + x = 2

CHOOSE は仮定への?の導入に利用でき，`ASM1,P[a:A],ASM2 |- Q`（ただし，`a`はP[a:A]以外には出現のない変数）というthmから``ASM1,?x.P[x],ASM2 |- P`` を得るには
CHOOSE (`a:A`,(ASSUME`?x:A. p[x:A]`)) thm
とします．

# UNDISCH(ARITH_RULE `(1 < a /\ a < y) ==> 1 < y`);;
val it : thm = 1 < a /\ a < y |- 1 < y
# CHOOSE(`a:num`, ASSUME(`?x. (1 < x /\ x < y)`)) it;;
val it : thm = ?x. 1 < x /\ x < y |- 1 < y

# ASSUME `?n. n = 0` ;;
val it : thm = ?n. n = 0 |- ?n. n = 0
# ADD_ASSUM `a = 1` it;;
val it : thm = ?n. n = 0, a = 1 |- ?n. n = 0
# CHOOSE (`a:num`, ASSUME(`?n. n = 1`)) it;;
val it : thm = ?n. n = 0, ?n. n = 1 |- ?n. n = 0

SIMPLE_CHOOS は仮定（リスト）の先頭への?の導入で，推論は下式に現れない自由変数を特称量化するものなので，SIMPLE_EXISTSと異なり本質的ですが，CHOOSEのように目的のtermおよび量化後の変数名を指定できず，変数名は量化前後で同じ，そしてその変数が仮定に全く現れないか，仮定の先頭のtermのみに現れる場合のみに適用できます．

# ASSUME `x = 0`;;
val it : thm = x = 0 |- x = 0
# ADD_ASSUM `y=0` it;;
val it : thm = x = 0, y = 0 |- x = 0
# SIMPLE_CHOOSE `y:num` it;;
Exception: Failure "CHOOSE".
# SIMPLE_CHOOSE `x:num` it;;
Exception: Failure "CHOOSE".
# ADD_ASSUM `a=0` it;;
val it : thm = a = 0, x = 0, y = 0 |- x = 0
# SIMPLE_CHOOSE `a:num` it;;
val it : thm = ?a. a = 0, x = 0, y = 0 |- x = 0

?!の定義．

EXISTS_UNIQUE_DEF: `(?!) = \P:A->bool. ((?) P) /\ (!x y. ((P x) /\ (P y)) ==> (x = y))`
EXISTENCE `ASM |- ?!x. P[x]` gives `ASM |- ?x. P[x]`