added "op :", "op ~:" syntax;
authorwenzelm
Wed Nov 27 16:57:38 1996 +0100 (1996-11-27)
changeset 2261d926157c0a6a
parent 2260 b59781f2b809
child 2262 c7ee913746fd
added "op :", "op ~:" syntax;
added symbols syntax;
src/HOL/Set.thy
     1.1 --- a/src/HOL/Set.thy	Wed Nov 27 16:51:15 1996 +0100
     1.2 +++ b/src/HOL/Set.thy	Wed Nov 27 16:57:38 1996 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4  
     1.5  Set = Ord +
     1.6  
     1.7 +
     1.8 +(** Core syntax **)
     1.9 +
    1.10  types
    1.11    'a set
    1.12  
    1.13 @@ -25,28 +28,35 @@
    1.14    UNION, INTER  :: ['a set, 'a => 'b set] => 'b set     (*general*)
    1.15    UNION1        :: ['a => 'b set] => 'b set         (binder "UN " 10)
    1.16    INTER1        :: ['a => 'b set] => 'b set         (binder "INT " 10)
    1.17 -  Union, Inter  :: (('a set)set) => 'a set              (*of a set*)
    1.18 +  Union, Inter  :: (('a set) set) => 'a set             (*of a set*)
    1.19    Pow           :: 'a set => 'a set set                 (*powerset*)
    1.20    range         :: ('a => 'b) => 'b set                 (*of function*)
    1.21    Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
    1.22    inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
    1.23    inj_onto      :: ['a => 'b, 'a set] => bool
    1.24    "``"          :: ['a => 'b, 'a set] => ('b set)   (infixr 90)
    1.25 -     (*membership*)
    1.26 -  "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50,51] 50)
    1.27 +  (*membership*)
    1.28 +  "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
    1.29  
    1.30  
    1.31 +
    1.32 +(** Additional concrete syntax **)
    1.33 +
    1.34  syntax
    1.35  
    1.36 -  UNIV         :: 'a set
    1.37 +  "op :"        :: ['a, 'a set] => bool               ("op :")
    1.38  
    1.39 -     (*infix synatx for non-membership*)
    1.40 -  "op ~:"        :: ['a, 'a set] => bool             ("(_/ ~: _)" [50,51] 50)
    1.41 +  UNIV          :: 'a set
    1.42 +
    1.43 +  (* Infix syntax for non-membership *)
    1.44  
    1.45 -  "@Finset"     :: args => 'a set                   ("{(_)}")
    1.46 +  "op ~:"       :: ['a, 'a set] => bool               ("(_/ ~: _)" [50, 51] 50)
    1.47 +  "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
    1.48  
    1.49 -  "@Coll"       :: [pttrn, bool] => 'a set          ("(1{_./ _})")
    1.50 -  "@SetCompr"   :: ['a, idts, bool] => 'a set       ("(1{_ |/_./ _})")
    1.51 +  "@Finset"     :: args => 'a set                     ("{(_)}")
    1.52 +
    1.53 +  "@Coll"       :: [pttrn, bool] => 'a set            ("(1{_./ _})")
    1.54 +  "@SetCompr"   :: ['a, idts, bool] => 'a set         ("(1{_ |/_./ _})")
    1.55  
    1.56    (* Big Intersection / Union *)
    1.57  
    1.58 @@ -62,7 +72,7 @@
    1.59  
    1.60  translations
    1.61    "UNIV"        == "Compl {}"
    1.62 -  "range(f)"    == "f``UNIV"
    1.63 +  "range f"     == "f``UNIV"
    1.64    "x ~: y"      == "~ (x : y)"
    1.65    "{x, xs}"     == "insert x {xs}"
    1.66    "{x}"         == "insert x {}"
    1.67 @@ -75,6 +85,28 @@
    1.68    "EX x:A. P"   => "Bex A (%x. P)"
    1.69  
    1.70  
    1.71 +syntax (symbols)
    1.72 +  "op Int"      :: ['a set, 'a set] => 'a set         (infixl "\\<inter>" 70)
    1.73 +  "op Un"       :: ['a set, 'a set] => 'a set         (infixl "\\<union>" 65)
    1.74 +  "op :"        :: ['a, 'a set] => bool               ("(_/ \\<in> _)" [50, 51] 50)
    1.75 +  "op :"        :: ['a, 'a set] => bool               ("op \\<in>")
    1.76 +  "op ~:"       :: ['a, 'a set] => bool               ("(_/ \\<notin> _)" [50, 51] 50)
    1.77 +  "op ~:"       :: ['a, 'a set] => bool               ("op \\<notin>")
    1.78 +  "UN "         :: [idts, bool] => bool               ("(3\\<Union> _./ _)" 10)
    1.79 +  "INT "        :: [idts, bool] => bool               ("(3\\<Inter> _./ _)" 10)
    1.80 +  "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Union> _\\<in>_./ _)" 10)
    1.81 +  "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter> _\\<in>_./ _)" 10)
    1.82 +  Union         :: (('a set) set) => 'a set           ("\\<Union> _" [90] 90)
    1.83 +  Inter         :: (('a set) set) => 'a set           ("\\<Inter> _" [90] 90)
    1.84 +  "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" 10)
    1.85 +  "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" 10)
    1.86 +  "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" 10)
    1.87 +  "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" 10)
    1.88 +
    1.89 +
    1.90 +
    1.91 +(** Rules and definitions **)
    1.92 +
    1.93  rules
    1.94  
    1.95    (* Isomorphisms between Predicates and Sets *)
    1.96 @@ -84,6 +116,7 @@
    1.97  
    1.98  
    1.99  defs
   1.100 +
   1.101    Ball_def      "Ball A P       == ! x. x:A --> P(x)"
   1.102    Bex_def       "Bex A P        == ? x. x:A & P(x)"
   1.103    subset_def    "A <= B         == ! x:A. x:B"
   1.104 @@ -110,6 +143,7 @@
   1.105  
   1.106  end
   1.107  
   1.108 +
   1.109  ML
   1.110  
   1.111  local
   1.112 @@ -150,4 +184,3 @@
   1.113    map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
   1.114  
   1.115  end;
   1.116 -