On 18/08/2012, at 4:18, Cris Perdue <c...@perdues.com> wrote:
> REWRITE_CONV [IN_ELIM_THM] `{x + y | x IN P /\ 10 < y}`
>
> it won't be disturbed because it doesn't have that external `x IN` at the
> front.
>
> It appears to me that Michael is trying to make a point here that I'm not
> grasping, and that maybe his code snippet is not successful in demonstrating.
I was trying to make the point that IN_ELIM_thm is a rewrite you can include as
an argument to REWRITE without having your rewrite “destroying” normal set
comprehension terms (which is what using [SETSPEC; GSPEC] would do).
The fact that REWRITE_CONV [IN_ELIM_thm] left your set comprehensions unchanged
demonstrated this “safety property”. Crafting rewrites so as to avoid what
John nicely described as “collateral damage” is quite an art.
Michael
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
