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
```