src/HOL/Set.thy
author nipkow
Tue Jan 09 15:22:13 2001 +0100 (2001-01-09)
changeset 10832 e33b47e4246d
parent 10131 546686f0a6fb
child 10985 65a8a0e2d55b
permissions -rw-r--r--
`` -> and ``` -> ``
clasohm@923
     1
(*  Title:      HOL/Set.thy
clasohm@923
     2
    ID:         $Id$
clasohm@923
     3
    Author:     Tobias Nipkow
clasohm@923
     4
    Copyright   1993  University of Cambridge
clasohm@923
     5
*)
clasohm@923
     6
clasohm@923
     7
Set = Ord +
clasohm@923
     8
wenzelm@2261
     9
wenzelm@2261
    10
(** Core syntax **)
wenzelm@2261
    11
wenzelm@3947
    12
global
wenzelm@3947
    13
clasohm@923
    14
types
clasohm@923
    15
  'a set
clasohm@923
    16
clasohm@923
    17
arities
clasohm@923
    18
  set :: (term) term
clasohm@923
    19
clasohm@923
    20
instance
paulson@5780
    21
  set :: (term) {ord, minus}
clasohm@923
    22
wenzelm@3820
    23
syntax
wenzelm@3820
    24
  "op :"        :: ['a, 'a set] => bool             ("op :")
wenzelm@3820
    25
clasohm@923
    26
consts
clasohm@1370
    27
  "{}"          :: 'a set                           ("{}")
paulson@4159
    28
  UNIV          :: 'a set
clasohm@1370
    29
  insert        :: ['a, 'a set] => 'a set
clasohm@1370
    30
  Collect       :: ('a => bool) => 'a set               (*comprehension*)
clasohm@1370
    31
  Int           :: ['a set, 'a set] => 'a set       (infixl 70)
clasohm@1370
    32
  Un            :: ['a set, 'a set] => 'a set       (infixl 65)
clasohm@1370
    33
  UNION, INTER  :: ['a set, 'a => 'b set] => 'b set     (*general*)
wenzelm@2261
    34
  Union, Inter  :: (('a set) set) => 'a set             (*of a set*)
clasohm@1370
    35
  Pow           :: 'a set => 'a set set                 (*powerset*)
clasohm@1370
    36
  Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
nipkow@10832
    37
  "image"       :: ['a => 'b, 'a set] => ('b set)   (infixr "`" 90)
wenzelm@2261
    38
  (*membership*)
wenzelm@2261
    39
  "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
clasohm@923
    40
clasohm@923
    41
wenzelm@2261
    42
(** Additional concrete syntax **)
wenzelm@2261
    43
clasohm@923
    44
syntax
wenzelm@10131
    45
  range         :: ('a => 'b) => 'b set                 (*of function*)
clasohm@923
    46
wenzelm@2261
    47
  (* Infix syntax for non-membership *)
clasohm@923
    48
wenzelm@3820
    49
  "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
wenzelm@2261
    50
  "op ~:"       :: ['a, 'a set] => bool               ("(_/ ~: _)" [50, 51] 50)
clasohm@923
    51
wenzelm@7238
    52
wenzelm@2261
    53
  "@Finset"     :: args => 'a set                     ("{(_)}")
wenzelm@2261
    54
  "@Coll"       :: [pttrn, bool] => 'a set            ("(1{_./ _})")
wenzelm@2261
    55
  "@SetCompr"   :: ['a, idts, bool] => 'a set         ("(1{_ |/_./ _})")
clasohm@923
    56
clasohm@923
    57
  (* Big Intersection / Union *)
clasohm@923
    58
wenzelm@10106
    59
  "@INTER1"     :: [pttrns, 'b set] => 'b set         ("(3INT _./ _)" 10)
wenzelm@10106
    60
  "@UNION1"     :: [pttrns, 'b set] => 'b set         ("(3UN _./ _)" 10)
clasohm@1370
    61
  "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3INT _:_./ _)" 10)
clasohm@1370
    62
  "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3UN _:_./ _)" 10)
clasohm@923
    63
clasohm@923
    64
  (* Bounded Quantifiers *)
wenzelm@7238
    65
  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" [0, 0, 10] 10)
wenzelm@7238
    66
  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" [0, 0, 10] 10)
clasohm@923
    67
wenzelm@7238
    68
syntax (HOL)
wenzelm@7238
    69
  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3! _:_./ _)" [0, 0, 10] 10)
wenzelm@7238
    70
  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" [0, 0, 10] 10)
clasohm@923
    71
clasohm@923
    72
translations
nipkow@10832
    73
  "range f"     == "f`UNIV"
clasohm@923
    74
  "x ~: y"      == "~ (x : y)"
clasohm@923
    75
  "{x, xs}"     == "insert x {xs}"
clasohm@923
    76
  "{x}"         == "insert x {}"
clasohm@923
    77
  "{x. P}"      == "Collect (%x. P)"
paulson@4159
    78
  "UN x y. B"   == "UN x. UN y. B"
paulson@4159
    79
  "UN x. B"     == "UNION UNIV (%x. B)"
wenzelm@7238
    80
  "INT x y. B"  == "INT x. INT y. B"
paulson@4159
    81
  "INT x. B"    == "INTER UNIV (%x. B)"
paulson@4159
    82
  "UN x:A. B"   == "UNION A (%x. B)"
clasohm@923
    83
  "INT x:A. B"  == "INTER A (%x. B)"
wenzelm@7238
    84
  "ALL x:A. P"  == "Ball A (%x. P)"
wenzelm@7238
    85
  "EX x:A. P"   == "Bex A (%x. P)"
clasohm@923
    86
wenzelm@2388
    87
syntax ("" output)
wenzelm@3820
    88
  "_setle"      :: ['a set, 'a set] => bool           ("op <=")
wenzelm@2388
    89
  "_setle"      :: ['a set, 'a set] => bool           ("(_/ <= _)" [50, 51] 50)
wenzelm@3820
    90
  "_setless"    :: ['a set, 'a set] => bool           ("op <")
wenzelm@2684
    91
  "_setless"    :: ['a set, 'a set] => bool           ("(_/ < _)" [50, 51] 50)
clasohm@923
    92
wenzelm@2261
    93
syntax (symbols)
wenzelm@3820
    94
  "_setle"      :: ['a set, 'a set] => bool           ("op \\<subseteq>")
wenzelm@2388
    95
  "_setle"      :: ['a set, 'a set] => bool           ("(_/ \\<subseteq> _)" [50, 51] 50)
wenzelm@3820
    96
  "_setless"    :: ['a set, 'a set] => bool           ("op \\<subset>")
wenzelm@2684
    97
  "_setless"    :: ['a set, 'a set] => bool           ("(_/ \\<subset> _)" [50, 51] 50)
wenzelm@2261
    98
  "op Int"      :: ['a set, 'a set] => 'a set         (infixl "\\<inter>" 70)
wenzelm@2261
    99
  "op Un"       :: ['a set, 'a set] => 'a set         (infixl "\\<union>" 65)
wenzelm@3820
   100
  "op :"        :: ['a, 'a set] => bool               ("op \\<in>")
wenzelm@2261
   101
  "op :"        :: ['a, 'a set] => bool               ("(_/ \\<in> _)" [50, 51] 50)
wenzelm@3820
   102
  "op ~:"       :: ['a, 'a set] => bool               ("op \\<notin>")
wenzelm@2261
   103
  "op ~:"       :: ['a, 'a set] => bool               ("(_/ \\<notin> _)" [50, 51] 50)
wenzelm@10106
   104
  "@UNION1"     :: [pttrns, 'b set] => 'b set         ("(3\\<Union>_./ _)" 10)
wenzelm@10106
   105
  "@INTER1"     :: [pttrns, 'b set] => 'b set         ("(3\\<Inter>_./ _)" 10)
oheimb@8148
   106
  "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Union>_\\<in>_./ _)" 10)
oheimb@8148
   107
  "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter>_\\<in>_./ _)" 10)
oheimb@8148
   108
  Union         :: (('a set) set) => 'a set           ("\\<Union>_" [90] 90)
oheimb@8148
   109
  Inter         :: (('a set) set) => 'a set           ("\\<Inter>_" [90] 90)
oheimb@8148
   110
  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall>_\\<in>_./ _)" [0, 0, 10] 10)
oheimb@8148
   111
  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists>_\\<in>_./ _)" [0, 0, 10] 10)
wenzelm@2261
   112
wenzelm@2412
   113
translations
wenzelm@2965
   114
  "op \\<subseteq>" => "op <= :: [_ set, _ set] => bool"
wenzelm@2965
   115
  "op \\<subset>" => "op <  :: [_ set, _ set] => bool"
wenzelm@2412
   116
wenzelm@2261
   117
wenzelm@2261
   118
wenzelm@2261
   119
(** Rules and definitions **)
wenzelm@2261
   120
wenzelm@3947
   121
local
wenzelm@3947
   122
clasohm@923
   123
rules
clasohm@923
   124
clasohm@923
   125
  (* Isomorphisms between Predicates and Sets *)
clasohm@923
   126
wenzelm@3842
   127
  mem_Collect_eq    "(a : {x. P(x)}) = P(a)"
wenzelm@3842
   128
  Collect_mem_eq    "{x. x:A} = A"
clasohm@923
   129
clasohm@923
   130
clasohm@923
   131
defs
clasohm@923
   132
  Ball_def      "Ball A P       == ! x. x:A --> P(x)"
clasohm@923
   133
  Bex_def       "Bex A P        == ? x. x:A & P(x)"
clasohm@923
   134
  subset_def    "A <= B         == ! x:A. x:B"
nipkow@3222
   135
  psubset_def   "A < B          == (A::'a set) <= B & ~ A=B"
paulson@5492
   136
  Compl_def     "- A            == {x. ~x:A}"
wenzelm@3842
   137
  Un_def        "A Un B         == {x. x:A | x:B}"
wenzelm@3842
   138
  Int_def       "A Int B        == {x. x:A & x:B}"
clasohm@923
   139
  set_diff_def  "A - B          == {x. x:A & ~x:B}"
clasohm@923
   140
  INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
clasohm@923
   141
  UNION_def     "UNION A B      == {y. ? x:A. y: B(x)}"
oheimb@2393
   142
  Inter_def     "Inter S        == (INT x:S. x)"
oheimb@2393
   143
  Union_def     "Union S        == (UN x:S. x)"
oheimb@2393
   144
  Pow_def       "Pow A          == {B. B <= A}"
clasohm@923
   145
  empty_def     "{}             == {x. False}"
paulson@4159
   146
  UNIV_def      "UNIV           == {x. True}"
wenzelm@3842
   147
  insert_def    "insert a B     == {x. x=a} Un B"
nipkow@10832
   148
  image_def     "f`A           == {y. ? x:A. y=f(x)}"
regensbu@1273
   149
wenzelm@7238
   150
clasohm@923
   151
end
clasohm@923
   152
wenzelm@2261
   153
clasohm@923
   154
ML
clasohm@923
   155
clasohm@923
   156
local
clasohm@923
   157
wenzelm@2388
   158
(* Set inclusion *)
wenzelm@2388
   159
wenzelm@4151
   160
fun le_tr' _ (*op <=*) (Type ("fun", (Type ("set", _) :: _))) ts =
wenzelm@2388
   161
      list_comb (Syntax.const "_setle", ts)
wenzelm@4151
   162
  | le_tr' _ (*op <=*) _ _ = raise Match;
wenzelm@2388
   163
wenzelm@4151
   164
fun less_tr' _ (*op <*) (Type ("fun", (Type ("set", _) :: _))) ts =
wenzelm@2684
   165
      list_comb (Syntax.const "_setless", ts)
wenzelm@4151
   166
  | less_tr' _ (*op <*) _ _ = raise Match;
wenzelm@2684
   167
wenzelm@2388
   168
clasohm@923
   169
(* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P}      *)
clasohm@923
   170
(* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *)
clasohm@923
   171
wenzelm@7238
   172
val ex_tr = snd(mk_binder_tr("EX ","Ex"));
clasohm@923
   173
clasohm@923
   174
fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1
clasohm@923
   175
  | nvars(_) = 1;
clasohm@923
   176
clasohm@923
   177
fun setcompr_tr[e,idts,b] =
clasohm@923
   178
  let val eq = Syntax.const("op =") $ Bound(nvars(idts)) $ e
clasohm@923
   179
      val P = Syntax.const("op &") $ eq $ b
clasohm@923
   180
      val exP = ex_tr [idts,P]
clasohm@923
   181
  in Syntax.const("Collect") $ Abs("",dummyT,exP) end;
clasohm@923
   182
clasohm@923
   183
val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY"));
clasohm@923
   184
clasohm@923
   185
fun setcompr_tr'[Abs(_,_,P)] =
clasohm@923
   186
  let fun ok(Const("Ex",_)$Abs(_,_,P),n) = ok(P,n+1)
clasohm@923
   187
        | ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ e) $ _, n) =
clasohm@923
   188
            if n>0 andalso m=n andalso
clasohm@923
   189
              ((0 upto (n-1)) subset add_loose_bnos(e,0,[]))
clasohm@923
   190
            then () else raise Match
clasohm@923
   191
clasohm@923
   192
      fun tr'(_ $ abs) =
clasohm@923
   193
        let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs]
clasohm@923
   194
        in Syntax.const("@SetCompr") $ e $ idts $ Q end
clasohm@923
   195
  in ok(P,0); tr'(P) end;
clasohm@923
   196
clasohm@923
   197
in
clasohm@923
   198
clasohm@923
   199
val parse_translation = [("@SetCompr", setcompr_tr)];
clasohm@923
   200
val print_translation = [("Collect", setcompr_tr')];
wenzelm@2684
   201
val typed_print_translation = [("op <=", le_tr'), ("op <", less_tr')];
wenzelm@7238
   202
clasohm@923
   203
clasohm@923
   204
end;