14.2 Function calculus
20世紀の数学の中で最も劇的な進展は，無限集合の体系的利用でしょう．その基礎は，濃度（基数）と順序数の概念です．それらは有限集合の大きさの数え上げと比較のアイデアを無限集合に拡張したものです．
■ まず，述語 FINITE で特徴付けられる，有限集合に対して，その基数を返す関数 CARD の性質を見てみます．
# CARD_UNION;;
val it : thm =
|- !s t.
FINITE s /\ FINITE t /\ s INTER t = {}
==> CARD (s UNION t) = CARD s + CARD t
中置関数 HAS_SIZE は，有限集合の基数を返します．
# HAS_SIZE;;
val it : thm = |- !s n. s HAS_SIZE n <=> FINITE s /\ CARD s = n
■ 無限集合を考えましょう．集合A,Bの基数|A|,|B|の大小関係 |A|≦|B| の定義としてもっともらしいものに
(*単射f:A->Bが存在する*)
`?f:A->B. !a1:A a2:A. f(a1)=f(a2)==>A1=a2`;;(*全射g:B->Aが存在する*)
`?g:B->A. !a:A. ?b:B. g(b)=a` ;;
の２つがありますが，以下のようにこれらは等価です．証明は
(?f:A->B. !a1:A a2:A. f(a1)=f(a2) ==> a1=a2)<=>
(?f:A->B. !b:B. ?a1:A. !a2:A. f a2 = b ==> a2 = a1)<=>
(?f:A->B. ?g:B->A. !a:A. g(f(a))=a)<=> ( by SWAP_EXISTS_THM )
(?g:B->A. ?f:A->B. !a:A. g(f(a))=a)<=> ( <== by SKOLEM_THM )
(?g:B->A. !a:A. ?b:B. g(b)=a)
のように推移させます．具体的にはtacticsの列の前に，lemmma を in を用いて局所的に定義するのが便利です．実行すると
# prove(`(?f:A->B. !a1:A a2:A. f(a1)=f(a2) ==> a1=a2)
<=>(?g:B->A. !a:A. ?b:B. g(b)=a)`,
let lemma1, lemma2, lemma3, lemma4 =
MESON`(?f:A->B. !a1:A a2:A. f(a1)=f(a2) ==> a1=a2)
<=>(?f:A->B. !b:B. ?a1:A. !a2:A. f a2 = b ==> a2 = a1)`,
MESON`(?f:A->B. !b:B. ?a1:A. !a2:A. f a2 = b ==> a2 = a1)
<=>(?f:A->B. ?g:B->A. !a:A. g(f(a))=a)`,
prove( `(?f:A->B. ?g:B->A. !a:A. g(f(a))=a)
<=>(?g:B->A. ?f:A->B. !a:A. g(f(a))=a)`,REWRITE_TAC[SWAP_EXISTS_THM] ),
prove( `(?g:B->A. ?f:A->B. !a:A. g(f(a))=a)
<=>(?g:B->A. !a:A. ?b:B. g(b)=a)`,REWRITE_TAC[SKOLEM_THM] ) in
REWRITE_TAC[TRANS lemma1 (TRANS lemma2 (TRANS lemma3 lemma4))] );;
0..0..1..2..5..solved at 11
0..0..1..2..7..15..solved at 24
0..0..1..3..8..19..37..74..124..209..366..solved at 376
0..0..1..2..7..13..25..39..57..77..111..146..197..solved at 212
val it : thm =
|- (?f. !a1 a2. f a1 = f a2 ==> a1 = a2) <=> (?g. !a. ?b. g b = a)
となります．
ここで，特称量化子の交換則 SWAP_EXISTS_THM
- !P. (?x y. P x y) <=> (?y x. P x y)
を参照するrewriteは，MATCH_ACCEPT_TAC thm により，thmの具体化として得ることもできます．
# prove( `(?f:A->B. ?g:B->A. !a:A. g(f(a))=a)<=>(?g:B->A. ?f:A->B. !a:A. g(f(a))=a)`,MATCH_ACCEPT_TAC SWAP_EXISTS_THM );;
val it : thm = |- (?f g. !a. g (f a) = a) <=> (?g f. !a. g (f a) = a)
なお，全称量化子の交換則
- !P. (!x y. P x y) <=> (!y x. P x y))
は SWAP_FORALL_THM です．
また，中間の
(!a:A. g(f(a))=a)
の代わりに関数の等式
(g o f = I)
を用いたいなら
# [o_DEF; I_DEF; FUN_EQ_THM];;
val it : thm list =
[|- !f g. f o g = (\x. f (g x)); |- I = (\x. x);
|- !f g. f = g <=> (!x. f x = g x)]
を参照すれば
# prove( `g o f = I<=>(!a:A. g(f(a))=a)`,
REWRITE_TAC[o_DEF; I_DEF; FUN_EQ_THM] );;
Warning: inventing type variables
val it : thm = |- g o f = I <=> (!a. g (f a) = a)
とrewrite出来ます．
お気付きのように，MASON[]は，SKOLEM_THMやSWAP_EXISTS_THMを知っています．従って，全てMESONで片付けることもできます．
# prove(`(?f:A->B. !a1:A a2:A. f(a1)=f(a2) ==> a1=a2)<=>(?g:B->A. !a:A. ?b:B. g(b)=a)`,MESON_TAC[MESON[]`
*1/\
*2`] );;
0..0..1..3..8..19..37..74..124..209..366..solved at 376
0..0..1..2..7..13..25..39..57..77..111..146..197..solved at 212
0..0..1..2..5..solved at 11
0..0..1..2..7..15..solved at 24
0..0..solved at 2
0..0..1..solved at 5
...
...
0..0..13..solved at 21
0..0..solved at 13
val it : thm =
|- (?f. !a1 a2. f a1 = f a2 ==> a1 = a2) <=> (?g. !a. ?b. g b = a)
ただし，自明な処理をさせるのは良いとしても，どんなthmを用いているかを把握しないままMESON[]任せにするのは頂けません．
