src/HOL/Set.thy
changeset 7238 36e58620ffc8
parent 5931 325300576da7
child 7358 9e95b846ad42
     1.1 --- a/src/HOL/Set.thy	Tue Aug 17 22:11:05 1999 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Aug 17 22:13:23 1999 +0200
     1.3 @@ -44,14 +44,13 @@
     1.4  
     1.5  syntax
     1.6  
     1.7 -
     1.8    (* Infix syntax for non-membership *)
     1.9  
    1.10    "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
    1.11    "op ~:"       :: ['a, 'a set] => bool               ("(_/ ~: _)" [50, 51] 50)
    1.12  
    1.13 +
    1.14    "@Finset"     :: args => 'a set                     ("{(_)}")
    1.15 -
    1.16    "@Coll"       :: [pttrn, bool] => 'a set            ("(1{_./ _})")
    1.17    "@SetCompr"   :: ['a, idts, bool] => 'a set         ("(1{_ |/_./ _})")
    1.18  
    1.19 @@ -64,11 +63,12 @@
    1.20    "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3UN _:_./ _)" 10)
    1.21  
    1.22    (* Bounded Quantifiers *)
    1.23 +  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" [0, 0, 10] 10)
    1.24 +  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" [0, 0, 10] 10)
    1.25  
    1.26 -  "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3! _:_./ _)" [0, 0, 10] 10)
    1.27 -  "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" [0, 0, 10] 10)
    1.28 -  "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" [0, 0, 10] 10)
    1.29 -  "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" [0, 0, 10] 10)
    1.30 +syntax (HOL)
    1.31 +  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3! _:_./ _)" [0, 0, 10] 10)
    1.32 +  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" [0, 0, 10] 10)
    1.33  
    1.34  translations
    1.35    "range f"     == "f``UNIV"
    1.36 @@ -78,14 +78,12 @@
    1.37    "{x. P}"      == "Collect (%x. P)"
    1.38    "UN x y. B"   == "UN x. UN y. B"
    1.39    "UN x. B"     == "UNION UNIV (%x. B)"
    1.40 -  "INT x y. B"   == "INT x. INT y. B"
    1.41 +  "INT x y. B"  == "INT x. INT y. B"
    1.42    "INT x. B"    == "INTER UNIV (%x. B)"
    1.43    "UN x:A. B"   == "UNION A (%x. B)"
    1.44    "INT x:A. B"  == "INTER A (%x. B)"
    1.45 -  "! x:A. P"    == "Ball A (%x. P)"
    1.46 -  "? x:A. P"    == "Bex A (%x. P)"
    1.47 -  "ALL x:A. P"  => "Ball A (%x. P)"
    1.48 -  "EX x:A. P"   => "Bex A (%x. P)"
    1.49 +  "ALL x:A. P"  == "Ball A (%x. P)"
    1.50 +  "EX x:A. P"   == "Bex A (%x. P)"
    1.51  
    1.52  syntax ("" output)
    1.53    "_setle"      :: ['a set, 'a set] => bool           ("op <=")
    1.54 @@ -112,12 +110,8 @@
    1.55    "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter> _\\<in>_./ _)" 10)
    1.56    Union         :: (('a set) set) => 'a set           ("\\<Union> _" [90] 90)
    1.57    Inter         :: (('a set) set) => 'a set           ("\\<Inter> _" [90] 90)
    1.58 -  "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
    1.59 -  "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
    1.60 -
    1.61 -syntax (symbols output)
    1.62 -  "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
    1.63 -  "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
    1.64 +  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
    1.65 +  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
    1.66  
    1.67  translations
    1.68    "op \\<subseteq>" => "op <= :: [_ set, _ set] => bool"
    1.69 @@ -138,7 +132,6 @@
    1.70  
    1.71  
    1.72  defs
    1.73 -
    1.74    Ball_def      "Ball A P       == ! x. x:A --> P(x)"
    1.75    Bex_def       "Bex A P        == ? x. x:A & P(x)"
    1.76    subset_def    "A <= B         == ! x:A. x:B"
    1.77 @@ -157,6 +150,7 @@
    1.78    insert_def    "insert a B     == {x. x=a} Un B"
    1.79    image_def     "f``A           == {y. ? x:A. y=f(x)}"
    1.80  
    1.81 +
    1.82  end
    1.83  
    1.84  
    1.85 @@ -178,7 +172,7 @@
    1.86  (* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P}      *)
    1.87  (* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *)
    1.88  
    1.89 -val ex_tr = snd(mk_binder_tr("? ","Ex"));
    1.90 +val ex_tr = snd(mk_binder_tr("EX ","Ex"));
    1.91  
    1.92  fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1
    1.93    | nvars(_) = 1;
    1.94 @@ -208,7 +202,6 @@
    1.95  val parse_translation = [("@SetCompr", setcompr_tr)];
    1.96  val print_translation = [("Collect", setcompr_tr')];
    1.97  val typed_print_translation = [("op <=", le_tr'), ("op <", less_tr')];
    1.98 -val print_ast_translation =
    1.99 -  map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
   1.100 +
   1.101  
   1.102  end;