17456

1 
(* Title: CCL/Set.thy

0

2 
ID: $Id$


3 
*)


4 

17456

5 
header {* Extending FOL by a modified version of HOL set theory *}


6 


7 
theory Set


8 
imports FOL


9 
begin

0

10 

3935

11 
global


12 

17456

13 
typedecl 'a set


14 
arities set :: ("term") "term"

0

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)

17456

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


22 
Inter :: "(('a set)set) => 'a set" (*...of a set*)


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


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


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


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

0

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


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


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


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


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


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


33 

3935

34 
syntax

0

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


36 


37 
(* Big Intersection / Union *)


38 


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


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


41 


42 
(* Bounded Quantifiers *)


43 


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


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


46 


47 
translations


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


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


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


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


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


53 

3935

54 
local

0

55 

17456

56 
axioms


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


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

0

59 

17456

60 
defs


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


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


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


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


65 
singleton_def: "{a} == {x. x=a}"


66 
empty_def: "{} == {x. False}"


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


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


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


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


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


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


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


74 


75 
ML {* use_legacy_bindings (the_context ()) *}

0

76 


77 
end


78 
