Added set comprehension as a syntactic abbreviation:
{e | x1..xn. P} means {u. ? x1 .. xn. u=e & P}
--- a/Set.thy Wed Jun 01 13:24:54 1994 +0200
+++ b/Set.thy Wed Jun 15 19:28:35 1994 +0200
@@ -44,7 +44,8 @@
(** Binding Constants **)
- "@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})") (*collection*)
+ "@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})")
+ "@SetCompr" :: "['a, idts, bool] => 'a set" ("{_ |/_./ _}")
(* Big Intersection / Union *)
@@ -104,9 +105,44 @@
end
+ML
-ML
+local
+
+(* 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
+ val exP = ex_tr [idts,P]
+ in dummyC("Collect") $ Abs("",dummyT,exP) end;
+
+val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY"));
+
+fun setcompr_tr'[Abs(_,_,P)] =
+ let fun ok(Const("Ex",_)$Abs(_,_,P),n) = ok(P,n+1)
+ | ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ _) $ _, n) =
+ if n>0 andalso m=n then () else raise Match
+
+ fun tr'(_ $ abs) =
+ let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs]
+ in dummyC("@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 print_ast_translation =
map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
+end;
+