src/HOL/Set.thy
changeset 13763 f94b569cd610
parent 13653 ef123b9e8089
child 13764 3e180bf68496
     1.1 --- a/src/HOL/Set.thy	Sun Dec 22 10:42:09 2002 +0100
     1.2 +++ b/src/HOL/Set.thy	Sun Dec 22 10:43:43 2002 +0100
     1.3 @@ -74,15 +74,15 @@
     1.4    "x ~: y"      == "~ (x : y)"
     1.5    "{x, xs}"     == "insert x {xs}"
     1.6    "{x}"         == "insert x {}"
     1.7 -  "{x. P}"      == "Collect (%x. P)"
     1.8 +  "{x. P}"      => "Collect (%x. P)"
     1.9    "UN x y. B"   == "UN x. UN y. B"
    1.10    "UN x. B"     == "UNION UNIV (%x. B)"
    1.11    "INT x y. B"  == "INT x. INT y. B"
    1.12    "INT x. B"    == "INTER UNIV (%x. B)"
    1.13 -  "UN x:A. B"   == "UNION A (%x. B)"
    1.14 -  "INT x:A. B"  == "INTER A (%x. B)"
    1.15 -  "ALL x:A. P"  == "Ball A (%x. P)"
    1.16 -  "EX x:A. P"   == "Bex A (%x. P)"
    1.17 +  "UN x:A. B"   => "UNION A (%x. B)"
    1.18 +  "INT x:A. B"  => "INTER A (%x. B)"
    1.19 +  "ALL x:A. P"  => "Ball A (%x. P)"
    1.20 +  "EX x:A. P"   => "Bex A (%x. P)"
    1.21  
    1.22  syntax (output)
    1.23    "_setle"      :: "'a set => 'a set => bool"             ("op <=")
    1.24 @@ -150,22 +150,36 @@
    1.25    in [("@SetCompr", setcompr_tr)] end;
    1.26  *}
    1.27  
    1.28 +(* To avoid eta-contraction of body: *)
    1.29  print_translation {*
    1.30 -  let
    1.31 -    val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY"));
    1.32 -
    1.33 -    fun setcompr_tr' [Abs (_, _, P)] =
    1.34 -      let
    1.35 -        fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1)
    1.36 -          | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
    1.37 -              if n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
    1.38 -                ((0 upto (n - 1)) subset add_loose_bnos (e, 0, [])) then ()
    1.39 -              else raise Match;
    1.40 +let
    1.41 +  fun btr' syn [A,Abs abs] =
    1.42 +    let val (x,t) = atomic_abs_tr' abs
    1.43 +    in Syntax.const syn $ x $ A $ t end
    1.44 +in
    1.45 +[("Ball", btr' "_Ball"),("Bex", btr' "_Bex"),
    1.46 + ("UNION", btr' "@UNION"),("INTER", btr' "@INTER")]
    1.47 +end
    1.48 +*}
    1.49 +
    1.50 +print_translation {*
    1.51 +let
    1.52 +  val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY"));
    1.53 +
    1.54 +  fun setcompr_tr' [Abs (abs as (_, _, P))] =
    1.55 +    let
    1.56 +      fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1)
    1.57 +        | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
    1.58 +            n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
    1.59 +            ((0 upto (n - 1)) subset add_loose_bnos (e, 0, []))
    1.60  
    1.61          fun tr' (_ $ abs) =
    1.62            let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs]
    1.63            in Syntax.const "@SetCompr" $ e $ idts $ Q end;
    1.64 -      in check (P, 0); tr' P end;
    1.65 +    in if check (P, 0) then tr' P
    1.66 +       else let val (x,t) = atomic_abs_tr' abs
    1.67 +            in Syntax.const "@Coll" $ x $ t end
    1.68 +    end;
    1.69    in [("Collect", setcompr_tr')] end;
    1.70  *}
    1.71