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