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