src/HOL/Set.thy
changeset 15535 a0cf3a19ee36
parent 15524 2ef571f80a55
child 15554 03d4347b071d
     1.1 --- a/src/HOL/Set.thy	Wed Feb 16 19:00:49 2005 +0100
     1.2 +++ b/src/HOL/Set.thy	Fri Feb 18 11:48:42 2005 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4    "@Finset"     :: "args => 'a set"                       ("{(_)}")
     1.5    "@Coll"       :: "pttrn => bool => 'a set"              ("(1{_./ _})")
     1.6    "@SetCompr"   :: "'a => idts => bool => 'a set"         ("(1{_ |/_./ _})")
     1.7 -
     1.8 +  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ :/ _./ _})")
     1.9    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" 10)
    1.10    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" 10)
    1.11    "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" 10)
    1.12 @@ -75,6 +75,7 @@
    1.13    "{x, xs}"     == "insert x {xs}"
    1.14    "{x}"         == "insert x {}"
    1.15    "{x. P}"      == "Collect (%x. P)"
    1.16 +  "{x:A. P}"    => "{x. x:A & P}"
    1.17    "UN x y. B"   == "UN x. UN y. B"
    1.18    "UN x. B"     == "UNION UNIV (%x. B)"
    1.19    "UN x. B"     == "UN x:UNIV. B"
    1.20 @@ -123,6 +124,7 @@
    1.21    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
    1.22  
    1.23  syntax (xsymbols)
    1.24 +  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ \<in>/ _./ _})")
    1.25    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" 10)
    1.26    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" 10)
    1.27    "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" 10)
    1.28 @@ -282,8 +284,15 @@
    1.29            let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs]
    1.30            in Syntax.const "@SetCompr" $ e $ idts $ Q end;
    1.31      in if check (P, 0) then tr' P
    1.32 -       else let val (x,t) = atomic_abs_tr' abs
    1.33 -            in Syntax.const "@Coll" $ x $ t end
    1.34 +       else let val (x as _ $ Free(xN,_), t) = atomic_abs_tr' abs
    1.35 +                val M = Syntax.const "@Coll" $ x $ t
    1.36 +            in case t of
    1.37 +                 Const("op &",_)
    1.38 +                   $ (Const("op :",_) $ (Const("_bound",_) $ Free(yN,_)) $ A)
    1.39 +                   $ P =>
    1.40 +                   if xN=yN then Syntax.const "@Collect" $ x $ A $ P else M
    1.41 +               | _ => M
    1.42 +            end
    1.43      end;
    1.44    in [("Collect", setcompr_tr')] end;
    1.45  *}