--- a/Set.thy Fri Sep 16 15:48:20 1994 +0200
+++ b/Set.thy Wed Sep 21 15:40:41 1994 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/set.thy
+(* Title: HOL/Set.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 1993 University of Cambridge
@@ -11,14 +11,13 @@
arities
set :: (term) term
- set :: (term) ord
- set :: (term) minus
+instance
+ set :: (term) {ord, minus}
consts
-
- (* Constants *)
-
+ "{}" :: "'a set" ("{}")
+ insert :: "['a, 'a set] => 'a set"
Collect :: "('a => bool) => 'a set" (*comprehension*)
Compl :: "('a set) => 'a set" (*complement*)
Int :: "['a set, 'a set] => 'a set" (infixl 70)
@@ -27,23 +26,20 @@
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*)
- Pow :: "'a set => 'a set set" (*powerset*)
+ 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)" (infixl 90)
":" :: "['a, 'a set] => bool" (infixl 50) (*membership*)
- "~:" :: "['a, 'a set] => bool" ("(_ ~:/ _)" [50, 51] 50)
-
- (* Finite Sets *)
-
- insert :: "['a, 'a set] => 'a set"
- "{}" :: "'a set" ("{}")
- "@Finset" :: "args => 'a set" ("{(_)}")
- (** Binding Constants **)
+syntax
+
+ "~:" :: "['a, 'a set] => bool" (infixl 50)
+
+ "@Finset" :: "args => 'a set" ("{(_)}")
"@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})")
"@SetCompr" :: "['a, idts, bool] => 'a set" ("(1{_ |/_./ _})")
@@ -60,7 +56,6 @@
"*Ball" :: "[idt, 'a set, bool] => bool" ("(3ALL _:_./ _)" 10)
"*Bex" :: "[idt, 'a set, bool] => bool" ("(3EX _:_./ _)" 10)
-
translations
"x ~: y" == "~ (x : y)"
"{x, xs}" == "insert(x, {xs})"
@@ -89,14 +84,14 @@
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}"
+ 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)"
- Pow_def "Pow(A) == {B. B <= A}"
+ Pow_def "Pow(A) == {B. B <= A}"
empty_def "{} == {x. False}"
insert_def "insert(a, B) == {x.x=a} Un B"
range_def "range(f) == {y. ? x. y=f(x)}"
@@ -113,18 +108,16 @@
(* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P} *)
-fun dummyC(s) = Const(s,dummyT);
-
val ex_tr = snd(mk_binder_tr("? ","Ex"));
fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1
| nvars(_) = 1;
fun setcompr_tr[e,idts,b] =
- let val eq = dummyC("op =") $ Bound(nvars(idts)) $ e
- val P = dummyC("op &") $ eq $ b
+ let val eq = Syntax.const("op =") $ Bound(nvars(idts)) $ e
+ val P = Syntax.const("op &") $ eq $ b
val exP = ex_tr [idts,P]
- in dummyC("Collect") $ Abs("",dummyT,exP) end;
+ in Syntax.const("Collect") $ Abs("",dummyT,exP) end;
val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY"));
@@ -135,14 +128,13 @@
fun tr'(_ $ abs) =
let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs]
- in dummyC("@SetCompr") $ e $ idts $ Q end
+ in Syntax.const("@SetCompr") $ e $ idts $ Q end
in ok(P,0); tr'(P) end;
in
-val parse_translation = [("@SetCompr",setcompr_tr)];
-val print_translation = [("Collect",setcompr_tr')];
-
+val parse_translation = [("@SetCompr", setcompr_tr)];
+val print_translation = [("Collect", setcompr_tr')];
val print_ast_translation =
map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];