--- a/src/HOL/Set.thy Wed Nov 27 16:51:15 1996 +0100
+++ b/src/HOL/Set.thy Wed Nov 27 16:57:38 1996 +0100
@@ -6,6 +6,9 @@
Set = Ord +
+
+(** Core syntax **)
+
types
'a set
@@ -25,28 +28,35 @@
UNION, INTER :: ['a set, 'a => 'b set] => 'b set (*general*)
UNION1 :: ['a => 'b set] => 'b set (binder "UN " 10)
INTER1 :: ['a => 'b set] => 'b set (binder "INT " 10)
- Union, Inter :: (('a set)set) => 'a set (*of a set*)
+ Union, Inter :: (('a set) set) => 'a set (*of a set*)
Pow :: 'a set => 'a set set (*powerset*)
range :: ('a => 'b) => 'b set (*of function*)
Ball, Bex :: ['a set, 'a => bool] => bool (*bounded quantifiers*)
inj, surj :: ('a => 'b) => bool (*inj/surjective*)
inj_onto :: ['a => 'b, 'a set] => bool
"``" :: ['a => 'b, 'a set] => ('b set) (infixr 90)
- (*membership*)
- "op :" :: ['a, 'a set] => bool ("(_/ : _)" [50,51] 50)
+ (*membership*)
+ "op :" :: ['a, 'a set] => bool ("(_/ : _)" [50, 51] 50)
+
+(** Additional concrete syntax **)
+
syntax
- UNIV :: 'a set
+ "op :" :: ['a, 'a set] => bool ("op :")
- (*infix synatx for non-membership*)
- "op ~:" :: ['a, 'a set] => bool ("(_/ ~: _)" [50,51] 50)
+ UNIV :: 'a set
+
+ (* Infix syntax for non-membership *)
- "@Finset" :: args => 'a set ("{(_)}")
+ "op ~:" :: ['a, 'a set] => bool ("(_/ ~: _)" [50, 51] 50)
+ "op ~:" :: ['a, 'a set] => bool ("op ~:")
- "@Coll" :: [pttrn, bool] => 'a set ("(1{_./ _})")
- "@SetCompr" :: ['a, idts, bool] => 'a set ("(1{_ |/_./ _})")
+ "@Finset" :: args => 'a set ("{(_)}")
+
+ "@Coll" :: [pttrn, bool] => 'a set ("(1{_./ _})")
+ "@SetCompr" :: ['a, idts, bool] => 'a set ("(1{_ |/_./ _})")
(* Big Intersection / Union *)
@@ -62,7 +72,7 @@
translations
"UNIV" == "Compl {}"
- "range(f)" == "f``UNIV"
+ "range f" == "f``UNIV"
"x ~: y" == "~ (x : y)"
"{x, xs}" == "insert x {xs}"
"{x}" == "insert x {}"
@@ -75,6 +85,28 @@
"EX x:A. P" => "Bex A (%x. P)"
+syntax (symbols)
+ "op Int" :: ['a set, 'a set] => 'a set (infixl "\\<inter>" 70)
+ "op Un" :: ['a set, 'a set] => 'a set (infixl "\\<union>" 65)
+ "op :" :: ['a, 'a set] => bool ("(_/ \\<in> _)" [50, 51] 50)
+ "op :" :: ['a, 'a set] => bool ("op \\<in>")
+ "op ~:" :: ['a, 'a set] => bool ("(_/ \\<notin> _)" [50, 51] 50)
+ "op ~:" :: ['a, 'a set] => bool ("op \\<notin>")
+ "UN " :: [idts, bool] => bool ("(3\\<Union> _./ _)" 10)
+ "INT " :: [idts, bool] => bool ("(3\\<Inter> _./ _)" 10)
+ "@UNION" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Union> _\\<in>_./ _)" 10)
+ "@INTER" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Inter> _\\<in>_./ _)" 10)
+ Union :: (('a set) set) => 'a set ("\\<Union> _" [90] 90)
+ Inter :: (('a set) set) => 'a set ("\\<Inter> _" [90] 90)
+ "@Ball" :: [pttrn, 'a set, bool] => bool ("(3\\<forall> _\\<in>_./ _)" 10)
+ "@Bex" :: [pttrn, 'a set, bool] => bool ("(3\\<exists> _\\<in>_./ _)" 10)
+ "*Ball" :: [pttrn, 'a set, bool] => bool ("(3\\<forall> _\\<in>_./ _)" 10)
+ "*Bex" :: [pttrn, 'a set, bool] => bool ("(3\\<exists> _\\<in>_./ _)" 10)
+
+
+
+(** Rules and definitions **)
+
rules
(* Isomorphisms between Predicates and Sets *)
@@ -84,6 +116,7 @@
defs
+
Ball_def "Ball A P == ! x. x:A --> P(x)"
Bex_def "Bex A P == ? x. x:A & P(x)"
subset_def "A <= B == ! x:A. x:B"
@@ -110,6 +143,7 @@
end
+
ML
local
@@ -150,4 +184,3 @@
map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
end;
-