Set.thy

   "@Finset"     :: "args => 'a set"                   ("{(_)}")
 
 
   (** Binding Constants **)
 
-  "@Coll"       :: "[idt, bool] => 'a set"            ("(1{_./ _})") (*collection*)
+  "@Coll"       :: "[idt, bool] => 'a set"            ("(1{_./ _})")
+  "@SetCompr"   :: "['a, idts, bool] => 'a set"       ("{_ |/_./ _}")
 
   (* Big Intersection / Union *)
 
   "@INTER"      :: "[idt, 'a set, 'b set] => 'b set"  ("(3INT _:_./ _)" 10)
   "@UNION"      :: "[idt, 'a set, 'b set] => 'b set"  ("(3UN _:_./ _)" 10)

   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
 
-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;
+