src/HOL/Set.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8148 5ef0b624aadb
child 10106 1b63e30437ee
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
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
2261
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
     9
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
    10
(** Core syntax **)
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
    11
3947
eb707467f8c5 adapted to qualified names;
wenzelm
parents: 3842
diff changeset
    12
global
eb707467f8c5 adapted to qualified names;
wenzelm
parents: 3842
diff changeset
    13
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
types
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    15
  'a set
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    16
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    17
arities
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    18
  set :: (term) term
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    19
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    20
instance
5780
0187f936685a Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed
paulson
parents: 5492
diff changeset
    21
  set :: (term) {ord, minus}
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    22
3820
46b255e140dc fixed infix syntax;
wenzelm
parents: 3370
diff changeset
    23
syntax
46b255e140dc fixed infix syntax;
wenzelm
parents: 3370
diff changeset
    24
  "op :"        :: ['a, 'a set] => bool             ("op :")
46b255e140dc fixed infix syntax;
wenzelm
parents: 3370
diff changeset
    25
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    26
consts
1370
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1273
diff changeset
    27
  "{}"          :: 'a set                           ("{}")
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4151
diff changeset
    28
  UNIV          :: 'a set
1370
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1273
diff changeset
    29
  insert        :: ['a, 'a set] => 'a set
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1273
diff changeset
    30
  Collect       :: ('a => bool) => 'a set               (*comprehension*)
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1273
diff changeset
    31
  Int           :: ['a set, 'a set] => 'a set       (infixl 70)
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1273
diff changeset
    32
  Un            :: ['a set, 'a set] => 'a set       (infixl 65)
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1273
diff changeset
    33
  UNION, INTER  :: ['a set, 'a => 'b set] => 'b set     (*general*)
2261
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
    34
  Union, Inter  :: (('a set) set) => 'a set             (*of a set*)
1370
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1273
diff changeset
    35
  Pow           :: 'a set => 'a set set                 (*powerset*)
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1273
diff changeset
    36
  range         :: ('a => 'b) => 'b set                 (*of function*)
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1273
diff changeset
    37
  Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
8005
b64d86018785 new-style infix declaration for "image"
paulson
parents: 7358
diff changeset
    38
  "image"       :: ['a => 'b, 'a set] => ('b set)   (infixr "``" 90)
2261
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
    39
  (*membership*)
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
    40
  "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    41
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    42
2261
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
    43
(** Additional concrete syntax **)
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
    44
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    45
syntax
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    46
2261
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
    47
  (* Infix syntax for non-membership *)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    48
3820
46b255e140dc fixed infix syntax;
wenzelm
parents: 3370
diff changeset
    49
  "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
2261
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
    50
  "op ~:"       :: ['a, 'a set] => bool               ("(_/ ~: _)" [50, 51] 50)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    51
7238
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 5931
diff changeset
    52
2261
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
    53
  "@Finset"     :: args => 'a set                     ("{(_)}")
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
    54
  "@Coll"       :: [pttrn, bool] => 'a set            ("(1{_./ _})")
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
    55
  "@SetCompr"   :: ['a, idts, bool] => 'a set         ("(1{_ |/_./ _})")
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    56
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    57
  (* Big Intersection / Union *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    58
7358
9e95b846ad42 a little tidying; also FIXED BAD TYPE in INTER1, UNION1
paulson
parents: 7238
diff changeset
    59
  "@INTER1"     :: [pttrns, 'b set] => 'b set   ("(3INT _./ _)" 10)
9e95b846ad42 a little tidying; also FIXED BAD TYPE in INTER1, UNION1
paulson
parents: 7238
diff changeset
    60
  "@UNION1"     :: [pttrns, 'b set] => 'b set   ("(3UN _./ _)" 10)
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4151
diff changeset
    61
1370
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 1273
diff changeset
    62
  "@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
    63
  "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3UN _:_./ _)" 10)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    64
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    65
  (* Bounded Quantifiers *)
7238
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 5931
diff changeset
    66
  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" [0, 0, 10] 10)
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 5931
diff changeset
    67
  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" [0, 0, 10] 10)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    68
7238
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 5931
diff changeset
    69
syntax (HOL)
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 5931
diff changeset
    70
  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3! _:_./ _)" [0, 0, 10] 10)
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 5931
diff changeset
    71
  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" [0, 0, 10] 10)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    72
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    73
translations
2261
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
    74
  "range f"     == "f``UNIV"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    75
  "x ~: y"      == "~ (x : y)"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    76
  "{x, xs}"     == "insert x {xs}"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    77
  "{x}"         == "insert x {}"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    78
  "{x. P}"      == "Collect (%x. P)"
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4151
diff changeset
    79
  "UN x y. B"   == "UN x. UN y. B"
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4151
diff changeset
    80
  "UN x. B"     == "UNION UNIV (%x. B)"
7238
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 5931
diff changeset
    81
  "INT x y. B"  == "INT x. INT y. B"
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4151
diff changeset
    82
  "INT x. B"    == "INTER UNIV (%x. B)"
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4151
diff changeset
    83
  "UN x:A. B"   == "UNION A (%x. B)"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    84
  "INT x:A. B"  == "INTER A (%x. B)"
7238
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 5931
diff changeset
    85
  "ALL x:A. P"  == "Ball A (%x. P)"
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 5931
diff changeset
    86
  "EX x:A. P"   == "Bex A (%x. P)"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    87
2388
d1f0505fc602 added set inclusion symbol syntax;
wenzelm
parents: 2372
diff changeset
    88
syntax ("" output)
3820
46b255e140dc fixed infix syntax;
wenzelm
parents: 3370
diff changeset
    89
  "_setle"      :: ['a set, 'a set] => bool           ("op <=")
2388
d1f0505fc602 added set inclusion symbol syntax;
wenzelm
parents: 2372
diff changeset
    90
  "_setle"      :: ['a set, 'a set] => bool           ("(_/ <= _)" [50, 51] 50)
3820
46b255e140dc fixed infix syntax;
wenzelm
parents: 3370
diff changeset
    91
  "_setless"    :: ['a set, 'a set] => bool           ("op <")
2684
9781d63ef063 added proper subset symbols syntax;
wenzelm
parents: 2412
diff changeset
    92
  "_setless"    :: ['a set, 'a set] => bool           ("(_/ < _)" [50, 51] 50)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    93
2261
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
    94
syntax (symbols)
3820
46b255e140dc fixed infix syntax;
wenzelm
parents: 3370
diff changeset
    95
  "_setle"      :: ['a set, 'a set] => bool           ("op \\<subseteq>")
2388
d1f0505fc602 added set inclusion symbol syntax;
wenzelm
parents: 2372
diff changeset
    96
  "_setle"      :: ['a set, 'a set] => bool           ("(_/ \\<subseteq> _)" [50, 51] 50)
3820
46b255e140dc fixed infix syntax;
wenzelm
parents: 3370
diff changeset
    97
  "_setless"    :: ['a set, 'a set] => bool           ("op \\<subset>")
2684
9781d63ef063 added proper subset symbols syntax;
wenzelm
parents: 2412
diff changeset
    98
  "_setless"    :: ['a set, 'a set] => bool           ("(_/ \\<subset> _)" [50, 51] 50)
2261
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
    99
  "op Int"      :: ['a set, 'a set] => 'a set         (infixl "\\<inter>" 70)
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
   100
  "op Un"       :: ['a set, 'a set] => 'a set         (infixl "\\<union>" 65)
3820
46b255e140dc fixed infix syntax;
wenzelm
parents: 3370
diff changeset
   101
  "op :"        :: ['a, 'a set] => bool               ("op \\<in>")
2261
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
   102
  "op :"        :: ['a, 'a set] => bool               ("(_/ \\<in> _)" [50, 51] 50)
3820
46b255e140dc fixed infix syntax;
wenzelm
parents: 3370
diff changeset
   103
  "op ~:"       :: ['a, 'a set] => bool               ("op \\<notin>")
2261
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
   104
  "op ~:"       :: ['a, 'a set] => bool               ("(_/ \\<notin> _)" [50, 51] 50)
8148
5ef0b624aadb beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents: 8005
diff changeset
   105
  "UN "         :: [idts, bool] => bool               ("(3\\<Union>_./ _)" 10)
5ef0b624aadb beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents: 8005
diff changeset
   106
  "INT "        :: [idts, bool] => bool               ("(3\\<Inter>_./ _)" 10)
5ef0b624aadb beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents: 8005
diff changeset
   107
  "@UNION1"     :: [pttrn, 'b set] => 'b set          ("(3\\<Union>_./ _)" 10)
5ef0b624aadb beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents: 8005
diff changeset
   108
  "@INTER1"     :: [pttrn, 'b set] => 'b set          ("(3\\<Inter>_./ _)" 10)
5ef0b624aadb beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents: 8005
diff changeset
   109
  "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Union>_\\<in>_./ _)" 10)
5ef0b624aadb beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents: 8005
diff changeset
   110
  "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter>_\\<in>_./ _)" 10)
5ef0b624aadb beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents: 8005
diff changeset
   111
  Union         :: (('a set) set) => 'a set           ("\\<Union>_" [90] 90)
5ef0b624aadb beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents: 8005
diff changeset
   112
  Inter         :: (('a set) set) => 'a set           ("\\<Inter>_" [90] 90)
5ef0b624aadb beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents: 8005
diff changeset
   113
  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall>_\\<in>_./ _)" [0, 0, 10] 10)
5ef0b624aadb beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents: 8005
diff changeset
   114
  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists>_\\<in>_./ _)" [0, 0, 10] 10)
2261
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
   115
2412
025e80ed698d fixed \<subseteq> input;
wenzelm
parents: 2393
diff changeset
   116
translations
2965
afbda7e26f15 improved translations for subset symbols syntax: constraints;
wenzelm
parents: 2912
diff changeset
   117
  "op \\<subseteq>" => "op <= :: [_ set, _ set] => bool"
afbda7e26f15 improved translations for subset symbols syntax: constraints;
wenzelm
parents: 2912
diff changeset
   118
  "op \\<subset>" => "op <  :: [_ set, _ set] => bool"
2412
025e80ed698d fixed \<subseteq> input;
wenzelm
parents: 2393
diff changeset
   119
2261
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
   120
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
   121
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
   122
(** Rules and definitions **)
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
   123
3947
eb707467f8c5 adapted to qualified names;
wenzelm
parents: 3842
diff changeset
   124
local
eb707467f8c5 adapted to qualified names;
wenzelm
parents: 3842
diff changeset
   125
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   126
rules
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   127
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   128
  (* Isomorphisms between Predicates and Sets *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   129
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3820
diff changeset
   130
  mem_Collect_eq    "(a : {x. P(x)}) = P(a)"
b55686a7b22c fixed dots;
wenzelm
parents: 3820
diff changeset
   131
  Collect_mem_eq    "{x. x:A} = A"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   132
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   133
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   134
defs
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   135
  Ball_def      "Ball A P       == ! x. x:A --> P(x)"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   136
  Bex_def       "Bex A P        == ? x. x:A & P(x)"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   137
  subset_def    "A <= B         == ! x:A. x:B"
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2965
diff changeset
   138
  psubset_def   "A < B          == (A::'a set) <= B & ~ A=B"
5492
d9fc3457554e From Compl(A) to -A
paulson
parents: 5254
diff changeset
   139
  Compl_def     "- A            == {x. ~x:A}"
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3820
diff changeset
   140
  Un_def        "A Un B         == {x. x:A | x:B}"
b55686a7b22c fixed dots;
wenzelm
parents: 3820
diff changeset
   141
  Int_def       "A Int B        == {x. x:A & x:B}"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   142
  set_diff_def  "A - B          == {x. x:A & ~x:B}"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   143
  INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   144
  UNION_def     "UNION A B      == {y. ? x:A. y: B(x)}"
2393
651fce76c86c adaptions for symbol font
oheimb
parents: 2388
diff changeset
   145
  Inter_def     "Inter S        == (INT x:S. x)"
651fce76c86c adaptions for symbol font
oheimb
parents: 2388
diff changeset
   146
  Union_def     "Union S        == (UN x:S. x)"
651fce76c86c adaptions for symbol font
oheimb
parents: 2388
diff changeset
   147
  Pow_def       "Pow A          == {B. B <= A}"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   148
  empty_def     "{}             == {x. False}"
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4151
diff changeset
   149
  UNIV_def      "UNIV           == {x. True}"
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3820
diff changeset
   150
  insert_def    "insert a B     == {x. x=a} Un B"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   151
  image_def     "f``A           == {y. ? x:A. y=f(x)}"
1273
6960ec882bca added 8bit pragmas
regensbu
parents: 1068
diff changeset
   152
7238
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 5931
diff changeset
   153
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   154
end
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   155
2261
d926157c0a6a added "op :", "op ~:" syntax;
wenzelm
parents: 2006
diff changeset
   156
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   157
ML
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   158
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   159
local
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   160
2388
d1f0505fc602 added set inclusion symbol syntax;
wenzelm
parents: 2372
diff changeset
   161
(* Set inclusion *)
d1f0505fc602 added set inclusion symbol syntax;
wenzelm
parents: 2372
diff changeset
   162
4151
5c19cd418c33 adapted typed_print_translation;
wenzelm
parents: 3947
diff changeset
   163
fun le_tr' _ (*op <=*) (Type ("fun", (Type ("set", _) :: _))) ts =
2388
d1f0505fc602 added set inclusion symbol syntax;
wenzelm
parents: 2372
diff changeset
   164
      list_comb (Syntax.const "_setle", ts)
4151
5c19cd418c33 adapted typed_print_translation;
wenzelm
parents: 3947
diff changeset
   165
  | le_tr' _ (*op <=*) _ _ = raise Match;
2388
d1f0505fc602 added set inclusion symbol syntax;
wenzelm
parents: 2372
diff changeset
   166
4151
5c19cd418c33 adapted typed_print_translation;
wenzelm
parents: 3947
diff changeset
   167
fun less_tr' _ (*op <*) (Type ("fun", (Type ("set", _) :: _))) ts =
2684
9781d63ef063 added proper subset symbols syntax;
wenzelm
parents: 2412
diff changeset
   168
      list_comb (Syntax.const "_setless", ts)
4151
5c19cd418c33 adapted typed_print_translation;
wenzelm
parents: 3947
diff changeset
   169
  | less_tr' _ (*op <*) _ _ = raise Match;
2684
9781d63ef063 added proper subset symbols syntax;
wenzelm
parents: 2412
diff changeset
   170
2388
d1f0505fc602 added set inclusion symbol syntax;
wenzelm
parents: 2372
diff changeset
   171
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   172
(* 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
   173
(* {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
   174
7238
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 5931
diff changeset
   175
val ex_tr = snd(mk_binder_tr("EX ","Ex"));
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   176
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   177
fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   178
  | nvars(_) = 1;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   179
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   180
fun setcompr_tr[e,idts,b] =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   181
  let val eq = Syntax.const("op =") $ Bound(nvars(idts)) $ e
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   182
      val P = Syntax.const("op &") $ eq $ b
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   183
      val exP = ex_tr [idts,P]
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   184
  in Syntax.const("Collect") $ Abs("",dummyT,exP) end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   185
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   186
val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY"));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   187
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   188
fun setcompr_tr'[Abs(_,_,P)] =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   189
  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
   190
        | ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ e) $ _, n) =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   191
            if n>0 andalso m=n andalso
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   192
              ((0 upto (n-1)) subset add_loose_bnos(e,0,[]))
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   193
            then () else raise Match
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   194
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   195
      fun tr'(_ $ abs) =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   196
        let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs]
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   197
        in Syntax.const("@SetCompr") $ e $ idts $ Q end
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   198
  in ok(P,0); tr'(P) end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   199
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   200
in
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   201
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   202
val parse_translation = [("@SetCompr", setcompr_tr)];
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   203
val print_translation = [("Collect", setcompr_tr')];
2684
9781d63ef063 added proper subset symbols syntax;
wenzelm
parents: 2412
diff changeset
   204
val typed_print_translation = [("op <=", le_tr'), ("op <", less_tr')];
7238
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 5931
diff changeset
   205
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   206
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   207
end;