HOL-Theorem-Prover
Consider HOL Light style set comprehension
As described in http://article.gmane.org/gmane.comp.mathematics.hol/2118 the HOL Light approach to this has the advantage over our current set up of not depending on pairs, and not using paired-abstractions.
It iterates mk_exists instead of mk_pabs, and uses another auxiliary constant, SET_SPEC.
Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.
A comment from Rob Arthan on the hol-info mailing list points out that one disadvantage of the HOL Light approach is that you will get
`{ x | x > 6}` <> `{x | x > 6}`;;
because each parse will use a fresh genvar. This makes me rather less keen on the idea of switching to this implementation (though I still hate paired abstractions).
Of course, one shouldn't be use = on terms anyway. One would still have
aconv ``{x | x > 6}`` ``{x | x > 6}``
in a possible HOL4 implementation of this idea.
Another argument in favour of this idea is that it seems impossible to make a congruence rule for GSPEC as we have it, but the congruence rule for HOL Light's approach is trivial. A congruence rule is critical to get termination conditions for things like
wave G i = MAX_SET { wave g j + 1 | j ∈ iters G ⋀ j -<G>-> i }
a function I want to define right now.
As the gmane link has died, here is a brief description of the HOL Light approach. There's a GSPEC constant outermost that is a signal to the printer (like our NUMERAL constant), but is semantically the identity. Then, there’s SETSPEC with definition
SETSPEC v P t <=> P /\ v = t
This is used to translate a simple case like { x | x < 6} into
GSPEC (\gv. ?x. SETSPEC gv (x < 6) x)
The P is the boolean expression to the right of the |; the t is the term to its left; the v is the genvar (gv above) that Rob Arthan complained about. In a more complicated case like { x + y | x * y = 20}, you get
GSPEC (\gv. ?x y. SETSPEC gv (x * y = 20) (x + y))
If you use the double | syntax, that just controls which variables get existentially quantified. So { x + y * z | x,y | x * y - z = 20} turns into
GSPEC (\gv. ?x y. SETSPEC gv (x * y - z = 20) (x + y * z))
with z free, as desired.