src/HOL/Set.thy
author wenzelm
Tue Dec 10 15:13:53 1996 +0100 (1996-12-10)
changeset 2372 a2999e19703b
parent 2368 d394336997cf
child 2388 d1f0505fc602
permissions -rw-r--r--
fixed alternative quantifier symbol syntax;
     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 types
    13   'a set
    14 
    15 arities
    16   set :: (term) term
    17 
    18 instance
    19   set :: (term) {ord, minus}
    20 
    21 consts
    22   "{}"          :: 'a set                           ("{}")
    23   insert        :: ['a, 'a set] => 'a set
    24   Collect       :: ('a => bool) => 'a set               (*comprehension*)
    25   Compl         :: ('a set) => 'a set                   (*complement*)
    26   Int           :: ['a set, 'a set] => 'a set       (infixl 70)
    27   Un            :: ['a set, 'a set] => 'a set       (infixl 65)
    28   UNION, INTER  :: ['a set, 'a => 'b set] => 'b set     (*general*)
    29   UNION1        :: ['a => 'b set] => 'b set         (binder "UN " 10)
    30   INTER1        :: ['a => 'b set] => 'b set         (binder "INT " 10)
    31   Union, Inter  :: (('a set) set) => 'a set             (*of a set*)
    32   Pow           :: 'a set => 'a set set                 (*powerset*)
    33   range         :: ('a => 'b) => 'b set                 (*of function*)
    34   Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
    35   inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
    36   inj_onto      :: ['a => 'b, 'a set] => bool
    37   "``"          :: ['a => 'b, 'a set] => ('b set)   (infixr 90)
    38   (*membership*)
    39   "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
    40 
    41 
    42 
    43 (** Additional concrete syntax **)
    44 
    45 syntax
    46 
    47   "op :"        :: ['a, 'a set] => bool               ("op :")
    48 
    49   UNIV          :: 'a set
    50 
    51   (* Infix syntax for non-membership *)
    52 
    53   "op ~:"       :: ['a, 'a set] => bool               ("(_/ ~: _)" [50, 51] 50)
    54   "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
    55 
    56   "@Finset"     :: args => 'a set                     ("{(_)}")
    57 
    58   "@Coll"       :: [pttrn, bool] => 'a set            ("(1{_./ _})")
    59   "@SetCompr"   :: ['a, idts, bool] => 'a set         ("(1{_ |/_./ _})")
    60 
    61   (* Big Intersection / Union *)
    62 
    63   "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3INT _:_./ _)" 10)
    64   "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3UN _:_./ _)" 10)
    65 
    66   (* Bounded Quantifiers *)
    67 
    68   "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3! _:_./ _)" [0, 0, 10] 10)
    69   "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" [0, 0, 10] 10)
    70   "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" [0, 0, 10] 10)
    71   "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" [0, 0, 10] 10)
    72 
    73 translations
    74   "UNIV"        == "Compl {}"
    75   "range f"     == "f``UNIV"
    76   "x ~: y"      == "~ (x : y)"
    77   "{x, xs}"     == "insert x {xs}"
    78   "{x}"         == "insert x {}"
    79   "{x. P}"      == "Collect (%x. P)"
    80   "INT x:A. B"  == "INTER A (%x. B)"
    81   "UN x:A. B"   == "UNION A (%x. B)"
    82   "! x:A. P"    == "Ball A (%x. P)"
    83   "? x:A. P"    == "Bex A (%x. P)"
    84   "ALL x:A. P"  => "Ball A (%x. P)"
    85   "EX x:A. P"   => "Bex A (%x. P)"
    86 
    87 
    88 syntax (symbols)
    89   "op Int"      :: ['a set, 'a set] => 'a set         (infixl "\\<inter>" 70)
    90   "op Un"       :: ['a set, 'a set] => 'a set         (infixl "\\<union>" 65)
    91   "op :"        :: ['a, 'a set] => bool               ("(_/ \\<in> _)" [50, 51] 50)
    92   "op :"        :: ['a, 'a set] => bool               ("op \\<in>")
    93   "op ~:"       :: ['a, 'a set] => bool               ("(_/ \\<notin> _)" [50, 51] 50)
    94   "op ~:"       :: ['a, 'a set] => bool               ("op \\<notin>")
    95   "UN "         :: [idts, bool] => bool               ("(3\\<Union> _./ _)" 10)
    96   "INT "        :: [idts, bool] => bool               ("(3\\<Inter> _./ _)" 10)
    97   "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Union> _\\<in>_./ _)" 10)
    98   "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter> _\\<in>_./ _)" 10)
    99   Union         :: (('a set) set) => 'a set           ("\\<Union> _" [90] 90)
   100   Inter         :: (('a set) set) => 'a set           ("\\<Inter> _" [90] 90)
   101   "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
   102   "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
   103 
   104 syntax (symbols output)
   105   "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
   106   "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
   107 
   108 
   109 
   110 (** Rules and definitions **)
   111 
   112 rules
   113 
   114   (* Isomorphisms between Predicates and Sets *)
   115 
   116   mem_Collect_eq    "(a : {x.P(x)}) = P(a)"
   117   Collect_mem_eq    "{x.x:A} = A"
   118 
   119 
   120 defs
   121 
   122   Ball_def      "Ball A P       == ! x. x:A --> P(x)"
   123   Bex_def       "Bex A P        == ? x. x:A & P(x)"
   124   subset_def    "A <= B         == ! x:A. x:B"
   125   Compl_def     "Compl(A)       == {x. ~x:A}"
   126   Un_def        "A Un B         == {x.x:A | x:B}"
   127   Int_def       "A Int B        == {x.x:A & x:B}"
   128   set_diff_def  "A - B          == {x. x:A & ~x:B}"
   129   INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
   130   UNION_def     "UNION A B      == {y. ? x:A. y: B(x)}"
   131   INTER1_def    "INTER1(B)      == INTER {x.True} B"
   132   UNION1_def    "UNION1(B)      == UNION {x.True} B"
   133   Inter_def     "Inter(S)       == (INT x:S. x)"
   134   Union_def     "Union(S)       == (UN x:S. x)"
   135   Pow_def       "Pow(A)         == {B. B <= A}"
   136   empty_def     "{}             == {x. False}"
   137   insert_def    "insert a B     == {x.x=a} Un B"
   138   image_def     "f``A           == {y. ? x:A. y=f(x)}"
   139   inj_def       "inj(f)         == ! x y. f(x)=f(y) --> x=y"
   140   inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
   141   surj_def      "surj(f)        == ! y. ? x. y=f(x)"
   142 
   143 (* start 8bit 1 *)
   144 (* end 8bit 1 *)
   145 
   146 end
   147 
   148 
   149 ML
   150 
   151 local
   152 
   153 (* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P}      *)
   154 (* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *)
   155 
   156 val ex_tr = snd(mk_binder_tr("? ","Ex"));
   157 
   158 fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1
   159   | nvars(_) = 1;
   160 
   161 fun setcompr_tr[e,idts,b] =
   162   let val eq = Syntax.const("op =") $ Bound(nvars(idts)) $ e
   163       val P = Syntax.const("op &") $ eq $ b
   164       val exP = ex_tr [idts,P]
   165   in Syntax.const("Collect") $ Abs("",dummyT,exP) end;
   166 
   167 val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY"));
   168 
   169 fun setcompr_tr'[Abs(_,_,P)] =
   170   let fun ok(Const("Ex",_)$Abs(_,_,P),n) = ok(P,n+1)
   171         | ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ e) $ _, n) =
   172             if n>0 andalso m=n andalso
   173               ((0 upto (n-1)) subset add_loose_bnos(e,0,[]))
   174             then () else raise Match
   175 
   176       fun tr'(_ $ abs) =
   177         let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs]
   178         in Syntax.const("@SetCompr") $ e $ idts $ Q end
   179   in ok(P,0); tr'(P) end;
   180 
   181 in
   182 
   183 val parse_translation = [("@SetCompr", setcompr_tr)];
   184 val print_translation = [("Collect", setcompr_tr')];
   185 val print_ast_translation =
   186   map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
   187 
   188 end;