--- /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")];
+