src/CCL/Set.thy
 author clasohm Thu, 17 Mar 1994 11:24:31 +0100 changeset 278 523518f44286 parent 0 a5a9c433f639 child 3837 d7f033c74b38 permissions -rw-r--r--
adapted type definition to new syntax
```
(*  Title:      CCL/set.thy
ID:         \$Id\$

Modified version of HOL/set.thy that extends FOL

*)

Set = FOL +

types
'a set

arities
set :: (term) term

consts
Collect       :: "['a => o] => 'a set"                    (*comprehension*)
Compl         :: "('a set) => 'a set"                     (*complement*)
Int           :: "['a set, 'a set] => 'a set"         (infixl 70)
Un            :: "['a set, 'a set] => 'a set"         (infixl 65)
Union, Inter  :: "(('a set)set) => 'a set"                (*...of a set*)
UNION, INTER  :: "['a set, 'a => 'b set] => 'b set"       (*general*)
Ball, Bex     :: "['a set, 'a => o] => o"                 (*bounded quants*)
mono          :: "['a set => 'b set] => o"                (*monotonicity*)
":"           :: "['a, 'a set] => o"                  (infixl 50) (*membership*)
"<="          :: "['a set, 'a set] => o"              (infixl 50)
singleton     :: "'a => 'a set"                       ("{_}")
empty         :: "'a set"                             ("{}")
"oo"          :: "['b => 'c, 'a => 'b, 'a] => 'c"     (infixr 50) (*composition*)

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

(* Big Intersection / Union *)

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

(* Bounded Quantifiers *)

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

translations
"{x. P}"      == "Collect(%x. P)"
"INT x:A. B"  == "INTER(A, %x. B)"
"UN x:A. B"   == "UNION(A, %x. B)"
"ALL x:A. P"  == "Ball(A, %x. P)"
"EX x:A. P"   == "Bex(A, %x. P)"

rules
mem_Collect_iff       "(a : {x.P(x)}) <-> P(a)"
set_extension         "A=B <-> (ALL x.x:A <-> x:B)"

Ball_def      "Ball(A, P)  == ALL x. x:A --> P(x)"
Bex_def       "Bex(A, P)   == EX x. x:A & P(x)"
mono_def      "mono(f)     == (ALL A B. A <= B --> f(A) <= f(B))"
subset_def    "A <= B      == ALL x:A. x:B"
singleton_def "{a}         == {x.x=a}"
empty_def     "{}          == {x.False}"
Un_def        "A Un B      == {x.x:A | x:B}"
Int_def       "A Int B     == {x.x:A & x:B}"
Compl_def     "Compl(A)    == {x. ~x:A}"
INTER_def     "INTER(A, B) == {y. ALL x:A. y: B(x)}"
UNION_def     "UNION(A, B) == {y. EX x:A. y: B(x)}"
Inter_def     "Inter(S)    == (INT x:S. x)"
Union_def     "Union(S)    == (UN x:S. x)"

end

```