src/CCL/Set.thy
changeset 35113 1a0c129bb2e0
parent 35054 a5db9779b026
child 38499 8f0cd11238a7
equal deleted inserted replaced
35112:ff6f60e6ab85 35113:1a0c129bb2e0
    25   subset        :: "['a set, 'a set] => o"              (infixl "<=" 50)
    25   subset        :: "['a set, 'a set] => o"              (infixl "<=" 50)
    26   singleton     :: "'a => 'a set"                       ("{_}")
    26   singleton     :: "'a => 'a set"                       ("{_}")
    27   empty         :: "'a set"                             ("{}")
    27   empty         :: "'a set"                             ("{}")
    28 
    28 
    29 syntax
    29 syntax
    30   "@Coll"       :: "[idt, o] => 'a set"                 ("(1{_./ _})") (*collection*)
    30   "_Coll"       :: "[idt, o] => 'a set"                 ("(1{_./ _})") (*collection*)
    31 
    31 
    32   (* Big Intersection / Union *)
    32   (* Big Intersection / Union *)
    33 
    33 
    34   "@INTER"      :: "[idt, 'a set, 'b set] => 'b set"    ("(INT _:_./ _)" [0, 0, 0] 10)
    34   "_INTER"      :: "[idt, 'a set, 'b set] => 'b set"    ("(INT _:_./ _)" [0, 0, 0] 10)
    35   "@UNION"      :: "[idt, 'a set, 'b set] => 'b set"    ("(UN _:_./ _)" [0, 0, 0] 10)
    35   "_UNION"      :: "[idt, 'a set, 'b set] => 'b set"    ("(UN _:_./ _)" [0, 0, 0] 10)
    36 
    36 
    37   (* Bounded Quantifiers *)
    37   (* Bounded Quantifiers *)
    38 
    38 
    39   "@Ball"       :: "[idt, 'a set, o] => o"              ("(ALL _:_./ _)" [0, 0, 0] 10)
    39   "_Ball"       :: "[idt, 'a set, o] => o"              ("(ALL _:_./ _)" [0, 0, 0] 10)
    40   "@Bex"        :: "[idt, 'a set, o] => o"              ("(EX _:_./ _)" [0, 0, 0] 10)
    40   "_Bex"        :: "[idt, 'a set, o] => o"              ("(EX _:_./ _)" [0, 0, 0] 10)
    41 
    41 
    42 translations
    42 translations
    43   "{x. P}"      == "CONST Collect(%x. P)"
    43   "{x. P}"      == "CONST Collect(%x. P)"
    44   "INT x:A. B"  == "CONST INTER(A, %x. B)"
    44   "INT x:A. B"  == "CONST INTER(A, %x. B)"
    45   "UN x:A. B"   == "CONST UNION(A, %x. B)"
    45   "UN x:A. B"   == "CONST UNION(A, %x. B)"