src/HOL/Set.thy
author regensbu
Fri Oct 06 16:17:08 1995 +0100 (1995-10-06)
changeset 1273 6960ec882bca
parent 1068 e0f2dffab506
child 1370 7361ac9b024d
permissions -rw-r--r--
added 8bit pragmas
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
clasohm@923
     9
types
clasohm@923
    10
  'a set
clasohm@923
    11
clasohm@923
    12
arities
clasohm@923
    13
  set :: (term) term
clasohm@923
    14
clasohm@923
    15
instance
clasohm@923
    16
  set :: (term) {ord, minus}
clasohm@923
    17
clasohm@923
    18
consts
clasohm@923
    19
  "{}"          :: "'a set"                           ("{}")
clasohm@923
    20
  insert        :: "['a, 'a set] => 'a set"
clasohm@923
    21
  Collect       :: "('a => bool) => 'a set"               (*comprehension*)
clasohm@923
    22
  Compl         :: "('a set) => 'a set"                   (*complement*)
clasohm@923
    23
  Int           :: "['a set, 'a set] => 'a set"       (infixl 70)
clasohm@923
    24
  Un            :: "['a set, 'a set] => 'a set"       (infixl 65)
clasohm@923
    25
  UNION, INTER  :: "['a set, 'a => 'b set] => 'b set"     (*general*)
clasohm@923
    26
  UNION1        :: "['a => 'b set] => 'b set"         (binder "UN " 10)
clasohm@923
    27
  INTER1        :: "['a => 'b set] => 'b set"         (binder "INT " 10)
clasohm@923
    28
  Union, Inter  :: "(('a set)set) => 'a set"              (*of a set*)
clasohm@923
    29
  Pow           :: "'a set => 'a set set"                 (*powerset*)
clasohm@923
    30
  range         :: "('a => 'b) => 'b set"                 (*of function*)
clasohm@923
    31
  Ball, Bex     :: "['a set, 'a => bool] => bool"         (*bounded quantifiers*)
clasohm@923
    32
  inj, surj     :: "('a => 'b) => bool"                   (*inj/surjective*)
clasohm@923
    33
  inj_onto      :: "['a => 'b, 'a set] => bool"
clasohm@923
    34
  "``"          :: "['a => 'b, 'a set] => ('b set)"   (infixl 90)
clasohm@923
    35
  ":"           :: "['a, 'a set] => bool"             (infixl 50) (*membership*)
clasohm@923
    36
clasohm@923
    37
clasohm@923
    38
syntax
clasohm@923
    39
clasohm@923
    40
  "~:"          :: "['a, 'a set] => bool"             (infixl 50)
clasohm@923
    41
clasohm@923
    42
  "@Finset"     :: "args => 'a set"                   ("{(_)}")
clasohm@923
    43
nipkow@1068
    44
  "@Coll"       :: "[pttrn, bool] => 'a set"          ("(1{_./ _})")
clasohm@923
    45
  "@SetCompr"   :: "['a, idts, bool] => 'a set"       ("(1{_ |/_./ _})")
clasohm@923
    46
clasohm@923
    47
  (* Big Intersection / Union *)
clasohm@923
    48
nipkow@1068
    49
  "@INTER"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3INT _:_./ _)" 10)
nipkow@1068
    50
  "@UNION"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3UN _:_./ _)" 10)
clasohm@923
    51
clasohm@923
    52
  (* Bounded Quantifiers *)
clasohm@923
    53
nipkow@1068
    54
  "@Ball"       :: "[pttrn, 'a set, bool] => bool"      ("(3! _:_./ _)" 10)
nipkow@1068
    55
  "@Bex"        :: "[pttrn, 'a set, bool] => bool"      ("(3? _:_./ _)" 10)
nipkow@1068
    56
  "*Ball"       :: "[pttrn, 'a set, bool] => bool"      ("(3ALL _:_./ _)" 10)
nipkow@1068
    57
  "*Bex"        :: "[pttrn, 'a set, bool] => bool"      ("(3EX _:_./ _)" 10)
clasohm@923
    58
clasohm@923
    59
translations
clasohm@923
    60
  "x ~: y"      == "~ (x : y)"
clasohm@923
    61
  "{x, xs}"     == "insert x {xs}"
clasohm@923
    62
  "{x}"         == "insert x {}"
clasohm@923
    63
  "{x. P}"      == "Collect (%x. P)"
clasohm@923
    64
  "INT x:A. B"  == "INTER A (%x. B)"
clasohm@923
    65
  "UN x:A. B"   == "UNION A (%x. B)"
clasohm@923
    66
  "! x:A. P"    == "Ball A (%x. P)"
clasohm@923
    67
  "? x:A. P"    == "Bex A (%x. P)"
clasohm@923
    68
  "ALL x:A. P"  => "Ball A (%x. P)"
clasohm@923
    69
  "EX x:A. P"   => "Bex A (%x. P)"
clasohm@923
    70
clasohm@923
    71
clasohm@923
    72
rules
clasohm@923
    73
clasohm@923
    74
  (* Isomorphisms between Predicates and Sets *)
clasohm@923
    75
clasohm@923
    76
  mem_Collect_eq    "(a : {x.P(x)}) = P(a)"
clasohm@923
    77
  Collect_mem_eq    "{x.x:A} = A"
clasohm@923
    78
clasohm@923
    79
clasohm@923
    80
defs
clasohm@923
    81
  Ball_def      "Ball A P       == ! x. x:A --> P(x)"
clasohm@923
    82
  Bex_def       "Bex A P        == ? x. x:A & P(x)"
clasohm@923
    83
  subset_def    "A <= B         == ! x:A. x:B"
clasohm@923
    84
  Compl_def     "Compl(A)       == {x. ~x:A}"
clasohm@923
    85
  Un_def        "A Un B         == {x.x:A | x:B}"
clasohm@923
    86
  Int_def       "A Int B        == {x.x:A & x:B}"
clasohm@923
    87
  set_diff_def  "A - B          == {x. x:A & ~x:B}"
clasohm@923
    88
  INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
clasohm@923
    89
  UNION_def     "UNION A B      == {y. ? x:A. y: B(x)}"
clasohm@923
    90
  INTER1_def    "INTER1(B)      == INTER {x.True} B"
clasohm@923
    91
  UNION1_def    "UNION1(B)      == UNION {x.True} B"
clasohm@923
    92
  Inter_def     "Inter(S)       == (INT x:S. x)"
clasohm@923
    93
  Union_def     "Union(S)       == (UN x:S. x)"
clasohm@923
    94
  Pow_def       "Pow(A)         == {B. B <= A}"
clasohm@923
    95
  empty_def     "{}             == {x. False}"
clasohm@923
    96
  insert_def    "insert a B     == {x.x=a} Un B"
clasohm@923
    97
  range_def     "range(f)       == {y. ? x. y=f(x)}"
clasohm@923
    98
  image_def     "f``A           == {y. ? x:A. y=f(x)}"
clasohm@923
    99
  inj_def       "inj(f)         == ! x y. f(x)=f(y) --> x=y"
clasohm@923
   100
  inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
clasohm@923
   101
  surj_def      "surj(f)        == ! y. ? x. y=f(x)"
clasohm@923
   102
regensbu@1273
   103
(* start 8bit 1 *)
regensbu@1273
   104
(* end 8bit 1 *)
regensbu@1273
   105
clasohm@923
   106
end
clasohm@923
   107
clasohm@923
   108
ML
clasohm@923
   109
clasohm@923
   110
local
clasohm@923
   111
clasohm@923
   112
(* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P}      *)
clasohm@923
   113
(* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *)
clasohm@923
   114
clasohm@923
   115
val ex_tr = snd(mk_binder_tr("? ","Ex"));
clasohm@923
   116
clasohm@923
   117
fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1
clasohm@923
   118
  | nvars(_) = 1;
clasohm@923
   119
clasohm@923
   120
fun setcompr_tr[e,idts,b] =
clasohm@923
   121
  let val eq = Syntax.const("op =") $ Bound(nvars(idts)) $ e
clasohm@923
   122
      val P = Syntax.const("op &") $ eq $ b
clasohm@923
   123
      val exP = ex_tr [idts,P]
clasohm@923
   124
  in Syntax.const("Collect") $ Abs("",dummyT,exP) end;
clasohm@923
   125
clasohm@923
   126
val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY"));
clasohm@923
   127
clasohm@923
   128
fun setcompr_tr'[Abs(_,_,P)] =
clasohm@923
   129
  let fun ok(Const("Ex",_)$Abs(_,_,P),n) = ok(P,n+1)
clasohm@923
   130
        | ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ e) $ _, n) =
clasohm@923
   131
            if n>0 andalso m=n andalso
clasohm@923
   132
              ((0 upto (n-1)) subset add_loose_bnos(e,0,[]))
clasohm@923
   133
            then () else raise Match
clasohm@923
   134
clasohm@923
   135
      fun tr'(_ $ abs) =
clasohm@923
   136
        let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs]
clasohm@923
   137
        in Syntax.const("@SetCompr") $ e $ idts $ Q end
clasohm@923
   138
  in ok(P,0); tr'(P) end;
clasohm@923
   139
clasohm@923
   140
in
clasohm@923
   141
clasohm@923
   142
val parse_translation = [("@SetCompr", setcompr_tr)];
clasohm@923
   143
val print_translation = [("Collect", setcompr_tr')];
clasohm@923
   144
val print_ast_translation =
clasohm@923
   145
  map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
clasohm@923
   146
clasohm@923
   147
end;
clasohm@923
   148