src/HOL/Set.thy
changeset 4159 4aff9b7e5597
parent 4151 5c19cd418c33
child 4761 1681b32dd134
     1.1 --- a/src/HOL/Set.thy	Wed Nov 05 13:29:47 1997 +0100
     1.2 +++ b/src/HOL/Set.thy	Wed Nov 05 13:32:07 1997 +0100
     1.3 @@ -25,14 +25,13 @@
     1.4  
     1.5  consts
     1.6    "{}"          :: 'a set                           ("{}")
     1.7 +  UNIV          :: 'a set
     1.8    insert        :: ['a, 'a set] => 'a set
     1.9    Collect       :: ('a => bool) => 'a set               (*comprehension*)
    1.10    Compl         :: ('a set) => 'a set                   (*complement*)
    1.11    Int           :: ['a set, 'a set] => 'a set       (infixl 70)
    1.12    Un            :: ['a set, 'a set] => 'a set       (infixl 65)
    1.13    UNION, INTER  :: ['a set, 'a => 'b set] => 'b set     (*general*)
    1.14 -  UNION1        :: ['a => 'b set] => 'b set         (binder "UN " 10)
    1.15 -  INTER1        :: ['a => 'b set] => 'b set         (binder "INT " 10)
    1.16    Union, Inter  :: (('a set) set) => 'a set             (*of a set*)
    1.17    Pow           :: 'a set => 'a set set                 (*powerset*)
    1.18    range         :: ('a => 'b) => 'b set                 (*of function*)
    1.19 @@ -47,8 +46,6 @@
    1.20  
    1.21  syntax
    1.22  
    1.23 -  UNIV          :: 'a set
    1.24 -
    1.25    (* Infix syntax for non-membership *)
    1.26  
    1.27    "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
    1.28 @@ -61,6 +58,9 @@
    1.29  
    1.30    (* Big Intersection / Union *)
    1.31  
    1.32 +  INTER1        :: [pttrns, 'a => 'b set] => 'b set   ("(3INT _./ _)" 10)
    1.33 +  UNION1        :: [pttrns, 'a => 'b set] => 'b set   ("(3UN _./ _)" 10)
    1.34 +
    1.35    "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3INT _:_./ _)" 10)
    1.36    "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3UN _:_./ _)" 10)
    1.37  
    1.38 @@ -72,14 +72,17 @@
    1.39    "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" [0, 0, 10] 10)
    1.40  
    1.41  translations
    1.42 -  "UNIV"        == "Compl {}"
    1.43    "range f"     == "f``UNIV"
    1.44    "x ~: y"      == "~ (x : y)"
    1.45    "{x, xs}"     == "insert x {xs}"
    1.46    "{x}"         == "insert x {}"
    1.47    "{x. P}"      == "Collect (%x. P)"
    1.48 +  "UN x y. B"   == "UN x. UN y. B"
    1.49 +  "UN x. B"     == "UNION UNIV (%x. B)"
    1.50 +  "INT x y. B"   == "INT x. INT y. B"
    1.51 +  "INT x. B"    == "INTER UNIV (%x. B)"
    1.52 +  "UN x:A. B"   == "UNION A (%x. B)"
    1.53    "INT x:A. B"  == "INTER A (%x. B)"
    1.54 -  "UN x:A. B"   == "UNION A (%x. B)"
    1.55    "! x:A. P"    == "Ball A (%x. P)"
    1.56    "? x:A. P"    == "Bex A (%x. P)"
    1.57    "ALL x:A. P"  => "Ball A (%x. P)"
    1.58 @@ -104,6 +107,8 @@
    1.59    "op ~:"       :: ['a, 'a set] => bool               ("(_/ \\<notin> _)" [50, 51] 50)
    1.60    "UN "         :: [idts, bool] => bool               ("(3\\<Union> _./ _)" 10)
    1.61    "INT "        :: [idts, bool] => bool               ("(3\\<Inter> _./ _)" 10)
    1.62 +  "UNION1"      :: [pttrn, 'b set] => 'b set          ("(3\\<Union> _./ _)" 10)
    1.63 +  "INTER1"      :: [pttrn, 'b set] => 'b set          ("(3\\<Inter> _./ _)" 10)
    1.64    "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Union> _\\<in>_./ _)" 10)
    1.65    "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter> _\\<in>_./ _)" 10)
    1.66    Union         :: (('a set) set) => 'a set           ("\\<Union> _" [90] 90)
    1.67 @@ -145,12 +150,11 @@
    1.68    set_diff_def  "A - B          == {x. x:A & ~x:B}"
    1.69    INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
    1.70    UNION_def     "UNION A B      == {y. ? x:A. y: B(x)}"
    1.71 -  INTER1_def    "INTER1 B       == INTER {x. True} B"
    1.72 -  UNION1_def    "UNION1 B       == UNION {x. True} B"
    1.73    Inter_def     "Inter S        == (INT x:S. x)"
    1.74    Union_def     "Union S        == (UN x:S. x)"
    1.75    Pow_def       "Pow A          == {B. B <= A}"
    1.76    empty_def     "{}             == {x. False}"
    1.77 +  UNIV_def      "UNIV           == {x. True}"
    1.78    insert_def    "insert a B     == {x. x=a} Un B"
    1.79    image_def     "f``A           == {y. ? x:A. y=f(x)}"
    1.80