John Harrison recently added the following two operators to HOL Light. Should we follow suit?


Added two natural infix constants "UNION_OF" and "INTERSECTION_OF" for the
useful and otherwise longwinded idiom that a set is a suitable (e.g. finite or
countable or pairwise disjoint) union/intersection of "somethings". Typical
examples are topological: `fsigma = COUNTABLE UNION_OF closed` etc.

        UNION_OF =
          |- !P Q. P UNION_OF Q =
                   (\s. ?u. P u /\ (!c. c IN u ==> Q c) /\ UNIONS u = s)

          |- !P Q. P INTERSECTION_OF Q =
                   (\s. ?u. P u /\ (!c. c IN u ==> Q c) /\ INTERS u = s)

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.