14.3 Some cardinal arithmetic (1)
前節の基数の大小関係の2通りの特徴付けのうち，単射Ｎ×Ｎ→Ｎの存在を示して，|Ｎ×Ｎ|≦|Ｎ|を確かめましょう．実際
# let cantor = new_definition
`cantor(x,y) = ((x + y) EXP 2 + 3 * x + y) DIV 2`;;
val cantor : thm = |- !x y. cantor (x,y) = ((x + y) EXP 2 + 3 * x + y) DIV 2
がその単射です．なぜなら，x+y≧a+b+1ならば
(x+y)^2 + 3*x+y ≧ (x+y)^2 + (x+y)≧(a+b+1)^2+a+b+1=(a+b)^2+ (a+b) + 2*(a+b+1)
となるからです．sos.mlをロードすれば
# # let CANTOR_LEMMA = prove
(`cantor(x,y) = cantor(a,b) ==> x + y = a + b`,
REWRITE_TAC[cantor] THEN CONV_TAC SOS_RULE);;
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
val ( CANTOR_LEMMA ) : thm =
|- cantor (x,y) = cantor (a,b) ==> x + y = a + b
と示せます．後は，((x+y) EXP 2 + 3*x+y) DIV 2 = ((x+y) EXP 2 + x+y) DIV 2 +x により，x=x'と連立するだけです．
パッケージとして実行すると
# let CANTOR_INJ = prove(
`cantor(x,y)=cantor(a,b) ==> (x=a /\ y=b)`,
let cantor = new_definition
`cantor(x,y) = *1 ) THEN
( ASM_REWRITE_TAC[ARITH_RULE`!a b c. (a+3*b+c) DIV 2 = (a+b+c) DIV 2 +b`;EQ_A
DD_LCANCEL] ) THEN
( ASM_ARITH_TAC ) );;
Warning: Benign redefinition
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
val ( CANTOR_INJ ) : thm = |- cantor (x,y) = cantor (a,b) ==> x = a /\ y = b
となります．DISCH_THENで切取った前件を戻して，同じ前件とLEMMAとからMATCH_MPで得た(x+y=a+b)を仮定に置く処理をDISCH_TEN(func thm->f(thm))として実現していることに注意します．なお，辺々から同じ項のキャンセルには
# EQ_ADD_LCANCEL;;
val it : thm = |- !m n p. m + n = m + p <=> n = p
を用いています．
:num#numの元として表現したいなら
# [FORALL_PAIR_THM; PAIR_EQ];;
val it : thm list =
[|- !P. (!p. P p) <=> (!p1 p2. P (p1,p2));
|- !x y a b. x,y = a,b <=> x = a /\ y = b]
を用いて
# prove(`!w:num#num z:num#num. cantor w = cantor z ==> w = z`,
REWRITE_TAC[FORALL_PAIR_THM; PAIR_EQ] THEN
MESON_TAC[CANTOR_INJ] );;
0..0..1..solved at 5
0..0..1..solved at 4
val it : thm = |- !w z. cantor w = cantor z ==> w = z
とすれば良いでしょう．
