0

1 
(* Title: CCL/set.thy


2 
ID: $Id$


3 


4 
Modified version of HOL/set.thy that extends FOL


5 


6 
*)


7 


8 
Set = FOL +


9 


10 
types


11 
set 1


12 


13 
arities


14 
set :: (term) term


15 


16 
consts


17 
Collect :: "['a => o] => 'a set" (*comprehension*)


18 
Compl :: "('a set) => 'a set" (*complement*)


19 
Int :: "['a set, 'a set] => 'a set" (infixl 70)


20 
Un :: "['a set, 'a set] => 'a set" (infixl 65)


21 
Union, Inter :: "(('a set)set) => 'a set" (*...of a set*)


22 
UNION, INTER :: "['a set, 'a => 'b set] => 'b set" (*general*)


23 
Ball, Bex :: "['a set, 'a => o] => o" (*bounded quants*)


24 
mono :: "['a set => 'b set] => o" (*monotonicity*)


25 
":" :: "['a, 'a set] => o" (infixl 50) (*membership*)


26 
"<=" :: "['a set, 'a set] => o" (infixl 50)


27 
singleton :: "'a => 'a set" ("{_}")


28 
empty :: "'a set" ("{}")


29 
"oo" :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50) (*composition*)


30 


31 
"@Coll" :: "[idt, o] => 'a set" ("(1{_./ _})") (*collection*)


32 


33 
(* Big Intersection / Union *)


34 


35 
"@INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(INT _:_./ _)" [0, 0, 0] 10)


36 
"@UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(UN _:_./ _)" [0, 0, 0] 10)


37 


38 
(* Bounded Quantifiers *)


39 


40 
"@Ball" :: "[idt, 'a set, o] => o" ("(ALL _:_./ _)" [0, 0, 0] 10)


41 
"@Bex" :: "[idt, 'a set, o] => o" ("(EX _:_./ _)" [0, 0, 0] 10)


42 


43 


44 
translations


45 
"{x. P}" == "Collect(%x. P)"


46 
"INT x:A. B" == "INTER(A, %x. B)"


47 
"UN x:A. B" == "UNION(A, %x. B)"


48 
"ALL x:A. P" == "Ball(A, %x. P)"


49 
"EX x:A. P" == "Bex(A, %x. P)"


50 


51 


52 
rules


53 
mem_Collect_iff "(a : {x.P(x)}) <> P(a)"


54 
set_extension "A=B <> (ALL x.x:A <> x:B)"


55 


56 
Ball_def "Ball(A, P) == ALL x. x:A > P(x)"


57 
Bex_def "Bex(A, P) == EX x. x:A & P(x)"


58 
mono_def "mono(f) == (ALL A B. A <= B > f(A) <= f(B))"


59 
subset_def "A <= B == ALL x:A. x:B"


60 
singleton_def "{a} == {x.x=a}"


61 
empty_def "{} == {x.False}"


62 
Un_def "A Un B == {x.x:A  x:B}"


63 
Int_def "A Int B == {x.x:A & x:B}"


64 
Compl_def "Compl(A) == {x. ~x:A}"


65 
INTER_def "INTER(A, B) == {y. ALL x:A. y: B(x)}"


66 
UNION_def "UNION(A, B) == {y. EX x:A. y: B(x)}"


67 
Inter_def "Inter(S) == (INT x:S. x)"


68 
Union_def "Union(S) == (UN x:S. x)"


69 


70 
end


71 
