72 translations |
72 translations |
73 "range f" == "f`UNIV" |
73 "range f" == "f`UNIV" |
74 "x ~: y" == "~ (x : y)" |
74 "x ~: y" == "~ (x : y)" |
75 "{x, xs}" == "insert x {xs}" |
75 "{x, xs}" == "insert x {xs}" |
76 "{x}" == "insert x {}" |
76 "{x}" == "insert x {}" |
77 "{x. P}" => "Collect (%x. P)" |
77 "{x. P}" == "Collect (%x. P)" |
78 "UN x y. B" == "UN x. UN y. B" |
78 "UN x y. B" == "UN x. UN y. B" |
79 "UN x. B" == "UNION UNIV (%x. B)" |
79 "UN x. B" == "UNION UNIV (%x. B)" |
80 "INT x y. B" == "INT x. INT y. B" |
80 "INT x y. B" == "INT x. INT y. B" |
81 "INT x. B" == "INTER UNIV (%x. B)" |
81 "INT x. B" == "INTER UNIV (%x. B)" |
82 "UN x:A. B" => "UNION A (%x. B)" |
82 "UN x:A. B" == "UNION A (%x. B)" |
83 "INT x:A. B" => "INTER A (%x. B)" |
83 "INT x:A. B" == "INTER A (%x. B)" |
84 "ALL x:A. P" => "Ball A (%x. P)" |
84 "ALL x:A. P" == "Ball A (%x. P)" |
85 "EX x:A. P" => "Bex A (%x. P)" |
85 "EX x:A. P" == "Bex A (%x. P)" |
86 |
86 |
87 syntax (output) |
87 syntax (output) |
88 "_setle" :: "'a set => 'a set => bool" ("op <=") |
88 "_setle" :: "'a set => 'a set => bool" ("op <=") |
89 "_setle" :: "'a set => 'a set => bool" ("(_/ <= _)" [50, 51] 50) |
89 "_setle" :: "'a set => 'a set => bool" ("(_/ <= _)" [50, 51] 50) |
90 "_setless" :: "'a set => 'a set => bool" ("op <") |
90 "_setless" :: "'a set => 'a set => bool" ("op <") |
170 let |
170 let |
171 fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1) |
171 fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1) |
172 | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) = |
172 | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) = |
173 n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso |
173 n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso |
174 ((0 upto (n - 1)) subset add_loose_bnos (e, 0, [])) |
174 ((0 upto (n - 1)) subset add_loose_bnos (e, 0, [])) |
|
175 | check _ = false |
175 |
176 |
176 fun tr' (_ $ abs) = |
177 fun tr' (_ $ abs) = |
177 let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs] |
178 let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs] |
178 in Syntax.const "@SetCompr" $ e $ idts $ Q end; |
179 in Syntax.const "@SetCompr" $ e $ idts $ Q end; |
179 in if check (P, 0) then tr' P |
180 in if check (P, 0) then tr' P |