14 Sets and functions

■　HOL Lightにおいては，集合は，述語と見做せるよう定義されています．

let IN = new_definition
`!P:A->bool. !x. x IN P <=> P x`;;

■　集合のconstantには

(typ) (typは:num，:realなどのhol.type)
EMPTY or {}
UNIV

があり，UNIVは

# `x+ &1 IN UNIV`;;
val it : term = `x + &1 IN (:real)`

のように直ちに書き換えられます．

■　集合についての作用子には

x IN s
s SUBSET t
s PSUBSET t (Is proper subset ?)
s DISJOINT t
SING s (Is singleton ?)

s UNION t
s INTER t
s DIFF t
x INSERT s (Insertion of x into s)
s DELETE x (Deletion of x from s)
UNIONS s (Union of all members of s)
INTERS s (Intersection of all members of s)

がありますが，述語，集合の別を設けない点に注意しましょう．
　これらの性質もthmになっています．

# SUBSET;;
val it : thm = |- !s t. s SUBSET t <=> (!x. x IN s ==> x IN t)
# NOT_IN_EMPTY;;
val it : thm = |- !x. ~(x IN {})
# IN_INTER;;
val it : thm = |- !s t x. x IN s INTER t <=> x IN s /\ x IN t
# IN_UNION;;
val it : thm = |- !s t x. x IN s UNION t <=> x IN s \/ x IN t
# IN_INSERT;;
val it : thm = |- !x y s. x IN y INSERT s <=> x = y \/ x IN s
# IN_DIFF;;
val it : thm = |- !s t x. x IN s DIFF t <=> x IN s /\ ~(x IN t)

■　述語 p，関数 f から集合 {x|p(x)} や {f(x)|p(x)} も作れます．

# `{ x | ?n. ODD(n) /\ x = n * n }`;;
val it : term = `{x | ?n. ODD n /\ x = n * n}`
# `{ n * n | ODD(n) }`;;
val it : term = `{n * n | ODD n}`

　逆に，e IN {x|p(x)} を p(e) に，また，e IN {f(x)|p(x)} を ?x. p(x) /\ e=f(x) にrewriteするには，IN_ELIM_THM を参照します．

# REWRITE_CONV[IN_ELIM_THM]`e IN {n|ODD(n)}`;;
val it : thm = |- e IN {n | ODD n} <=> ODD e
# REWRITE_CONV[IN_ELIM_THM]`e IN {n*n|ODD(n)}`;;
val it : thm = |- e IN {n * n | ODD n} <=> (?n. ODD n /\ e = n * n)

■　列挙による集合の表現です．

# `{1,2,3}`;;
val it : term = `{1, 2, 3}`
# `1 INSERT 2 INSERT 3 INSERT EMPTY`;;
val it : term = `{1, 2, 3}`

　所謂，外延性の公理

# EXTENSION;;
val it : thm = |- !s t. s = t <=> (!x. x IN s <=> x IN t)

は

# FUN_EQ_THM;;
val it : thm = |- !f g. f = g <=> (!x. f x = g x)

を IN に適用したものです．

let EXTENSION = prove
(`!s t. (s = t) <=> !x:A. x IN s <=> x IN t`,
REWRITE_TAC[IN; FUN_EQ_THM]);;

■　集合の理論における prover は SET_RULE

# SET_RULE `UNIV DIFF {a} = {x| ~(x=a)}` ;;
Warning: inventing type variables
val it : thm = |- (:?108270) DIFF {a} = {x | ~(x = a)}

# SET_RULE `!a:num. UNIV DIFF {a} = {x| ~(x=a)}` ;;
val it : thm = |- !a. (:num) DIFF {a} = {x | ~(x = a)}

# SET_RULE `{x | P x /\ Q x} = {x | P x} INTER {y | Q y}`;;
Warning: inventing type variables
val it : thm = |- {x | P x /\ Q x} = {x | P x} INTER {y | Q y}

# SET_RULE `a IN s ==> (s = a INSERT (s DELETE a))`;;
Warning: inventing type variables
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 3
val it : thm = |- a IN s ==> s = a INSERT (s DELETE a)

# SET_RULE `{2,3,2} ={2,3} INTER UNIV` ;;
0..0..solved at 3
0..0..solved at 2
0..0..solved at 3
0..0..solved at 3
0..0..solved at 2
val it : thm = |- {2, 3, 2} = {2, 3} INTER (:num)

そのtactic版は SET_TAC[] で，仮定を参照させるには，ASM を冠して用います．

g `!a:real b c d X. X={a,b,c} ==> X DIFF {b,d} = X DELETE b` ;;
e ( REPEAT STRIP_TAC ) ;;
e ( ASM SET_TAC[] ) ;;

　これらは集合論の基本的な同値性を検証した上で，MESON[] を呼んでいます．なお，集合のhol.typeは述語と同じく，:bool値の関数です．

# type_of `{1}` ;;
val it : hol_type = `:num->bool`

# SET_RULE `!s:A->bool t. s UNION t = s UNION (t DIFF s)` ;;
0..0..solved at 3
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 3
0..0..solved at 3
val it : thm = |- !s t. s UNION t = s UNION t DIFF s

■　DIFF に関して，例えば

# prove( `{1,2} DIFF {2} = {1}` , SET_TAC );;
0..0..solved at 3
0..0..solved at 2
0..0..solved at 3
0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0.
.0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..Excepti
on: Failure "solve_goal: Too deep".

# prove( `{1,2} DIFF {2,3} = {1}` , SET_TAC );;
0..0..solved at 4
0..0..solved at 3
0..0..solved at 3
0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0.
.0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..0..Excepti
on: Failure "solve_goal: Too deep".

のようになります．これは，SET_TACやMESONが1,2,3が異なることを知らない為なので，ARITHを参照させると

# prove( `{1,2} DIFF {2} = {1}` , SET_TAC[ARITH] );;
0..0..solved at 3
0..0..solved at 2
0..0..solved at 3
0..0..15..solved at 28
val it : thm = |- {1, 2} DIFF {2} = {1}
# prove( `{1,2} DIFF {2,3} = {1}` , SET_TAC[ARITH] );;
0..0..solved at 4
0..0..solved at 3
0..0..solved at 3
0..0..15..solved at 28
0..0..15..93..solved at 249
val it : thm = |- {1, 2} DIFF {2, 3} = {1}

となり，変数の場合には

# prove( `!a b c. ~a=c /\ ~a=b ==> {a} = {a,b} DIFF {b,c}` , SET_TAC[] );;
val it : thm =
|- !a b c. (~a <=> c) /\ (~a <=> b) ==> {a} = {a, b} DIFF {b, c}

のような注意が必要です．

■　簡単な証明ですが，SET_TAC[ARITH] では無理なようです．

# let set12 = `{n|n=1 \/ n=2}={n|0

しかし，rewrite方法を指定すると

# g set12;;
val it : goalstack = 1 subgoal (1 total)

`{n | n = 1 \/ n = 2} = {n | 0 < n /\ n < 3}`

# e ( REWRITE_TAC[EXTENSION;IN_ELIM_THM] );;
val it : goalstack = 1 subgoal (1 total)

`!x. x = 1 \/ x = 2 <=> 0 < x /\ x < 3`

# e( ARITH_TAC );;
val it : goalstack = No subgoals

となります．勿論，述語を書き換えてしまえば，直ちに

# prove( set12 , REWRITE_TAC[ARITH_RULE`n=1 \/ n=2 <=> 0

となります．

■　より簡単な例ですが

# prove( `0 IN (:num)` , SET_TAC[] );;
val it : thm = |- 0 IN (:num)

は良くても

# prove( `(:num)0` , SET_TAC[IN] );;
0..0..1..2..3..4..5..6..7..8..9..10..11..12..13..14..15..16..17..18..19..20..21.
.22..23..24..25..26..27..28..29..30..31..32..33..34..35..36..37..38..39..40..41.
.42..43..44..45..46..47..48..49..Exception: Failure "solve_goal: Too deep".

は無理で

# prove( `(:num)0` , ONCE_REWRITE_TAC[GSYM(IN)] THEN SET_TAC[] );;
val it : thm = |- (:num) 0

のような前処理が必要です．