diff -r 000000000000 -r 7949f97df77a set.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/set.thy	Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,111 @@
+(*  Title:      HOL/set.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1993  University of Cambridge
+*)
+
+Set = Ord +
+
+types
+  set 1
+
+arities
+  set :: (term) term
+  set :: (term) ord
+  set :: (term) minus
+
+
+consts
+
+  (* Constants *)
+
+  Collect       :: "('a => bool) => 'a set"                 (*comprehension*)
+  Compl         :: "('a set) => 'a set"                     (*complement*)
+  Int           :: "['a set, 'a set] => 'a set"         (infixl 70)
+  Un            :: "['a set, 'a set] => 'a set"         (infixl 65)
+  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*)
+  range         :: "('a => 'b) => 'b set"                   (*of function*)
+  Ball, Bex     :: "['a set, 'a => bool] => bool"           (*bounded quantifiers*)
+  inj, surj     :: "('a => 'b) => bool"                     (*injective/surjective*)
+  inj_onto      :: "['a => 'b, 'a set] => bool"
+  "``"          :: "['a => 'b, 'a set] => ('b set)"     (infixl 90)
+  ":"           :: "['a, 'a set] => bool" (infixl 50)       (*membership*)
+
+  (* Finite Sets *)
+
+  insert        :: "['a, 'a set] => 'a set"
+  "{}"          :: "'a set"                             ("{}")
+  "@Finset"     :: "args => 'a set"                     ("{(_)}")
+
+
+  (** Binding Constants **)
+
+  "@Coll"       :: "[idt, bool] => 'a set"              ("(1{_./ _})")  (*collection*)
+
+  (* Big Intersection / Union *)
+
+  "@INTER"      :: "[idt, 'a set, 'b set] => 'b set"    ("(3INT _:_./ _)" 10)
+  "@UNION"      :: "[idt, 'a set, 'b set] => 'b set"    ("(3UN _:_./ _)" 10)
+
+  (* Bounded Quantifiers *)
+
+  "@Ball"       :: "[idt, 'a set, bool] => bool"        ("(3! _:_./ _)" 10)
+  "@Bex"        :: "[idt, 'a set, bool] => bool"        ("(3? _:_./ _)" 10)
+  "*Ball"       :: "[idt, 'a set, bool] => bool"        ("(3ALL _:_./ _)" 10)
+  "*Bex"        :: "[idt, 'a set, bool] => bool"        ("(3EX _:_./ _)" 10)
+
+
+translations
+  "{x. P}"      == "Collect(%x. P)"
+  "INT x:A. B"  == "INTER(A, %x. B)"
+  "UN x:A. B"   == "UNION(A, %x. B)"
+  "! x:A. P"    == "Ball(A, %x. P)"
+  "? x:A. P"    == "Bex(A, %x. P)"
+  "ALL x:A. P"  => "Ball(A, %x. P)"
+  "EX x:A. P"   => "Bex(A, %x. P)"
+
+  "{x, xs}"     == "insert(x, {xs})"
+  "{x}"         == "insert(x, {})"
+
+
+rules
+
+  (* Isomorphisms between Predicates and Sets *)
+
+  mem_Collect_eq    "(a : {x.P(x)}) = P(a)"
+  Collect_mem_eq    "{x.x:A} = A"
+
+  (* Definitions *)
+
+  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"
+  Compl_def     "Compl(A)       == {x. ~x:A}"
+  Un_def        "A Un B         == {x.x:A | x:B}"
+  Int_def       "A Int B        == {x.x:A & x:B}"
+  set_diff_def  "A-B            == {x. x:A & ~x:B}"
+  INTER_def     "INTER(A, B)    == {y. ! x:A. y: B(x)}"
+  UNION_def     "UNION(A, B)    == {y. ? x:A. y: B(x)}"
+  INTER1_def    "INTER1(B)      == INTER({x.True}, B)"
+  UNION1_def    "UNION1(B)      == UNION({x.True}, B)"
+  Inter_def     "Inter(S)       == (INT x:S. x)"
+  Union_def     "Union(S)       == (UN x:S. x)"
+  empty_def     "{}             == {x. False}"
+  insert_def    "insert(a, B)   == {x.x=a} Un B"
+  range_def     "range(f)       == {y. ? x. y=f(x)}"
+  image_def     "f``A           == {y. ? x:A. y=f(x)}"
+  inj_def       "inj(f)         == ! x y. f(x)=f(y) --> x=y"
+  inj_onto_def  "inj_onto(f, A) == ! x:A. ! y:A. f(x)=f(y) --> x=y"
+  surj_def      "surj(f)        == ! y. ? x. y=f(x)"
+
+end
+
+
+ML
+
+val print_ast_translation =
+  map HOL.mk_alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
+