On Thu, Apr 14, 2011 at 1:08 AM, Lu Zhao <[email protected]> wrote: > On 04/13/2011 05:54 PM, Michael Norrish wrote: >> On 14/04/11 08:35, Lu Zhao wrote: >>> when I use SIMP_CONV (std_ss++PRED_SET_ss) [] s1, I want to get >>> something like: >> >>> {(0x1w,8); (0x1w,4)} = {(0x1w,x)} >> >>> where x is either 8 or 4, since I don't care about it. >> >> This is impossible. The cardinality of the set on the left is 2, the >> cardinality of the set on the right is 1. You could trivially derive a >> contradiction if the equation above was a theorem. > > I used the above example, since I tried this: > > val s1 = mk_insert(e1, mk_insert(e1,``{}:(word32#num) set``)) > > and "SIMP_CONV (std_ss++PRED_SET_ss) [] s1" gives: > > > val it = [] |- {(0x1w,4); (0x1w,4)} = {(0x1w,4)}: thm > > and I guessed there was something that could be done. I don't know that > this is the cardinality issue. What I really need is an expression like > > !e. e IN s1 ==> something > > which only cares about the first element of e.
You can certainly write !e. e IN s1 ==> P (FST e1), for some predicate P... You could also try IMAGE FST s1, to turn a set of pairs into a set of first elements only. > > Since it's impossible, using a mapping seems to be the only solution now. > > Thanks a lot. > Lu > > ------------------------------------------------------------------------------ > Benefiting from Server Virtualization: Beyond Initial Workload > Consolidation -- Increasing the use of server virtualization is a top > priority.Virtualization can reduce costs, simplify management, and improve > application availability and disaster protection. Learn more about boosting > the value of server virtualization. http://p.sf.net/sfu/vmware-sfdev2dev > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > ------------------------------------------------------------------------------ Benefiting from Server Virtualization: Beyond Initial Workload Consolidation -- Increasing the use of server virtualization is a top priority.Virtualization can reduce costs, simplify management, and improve application availability and disaster protection. Learn more about boosting the value of server virtualization. http://p.sf.net/sfu/vmware-sfdev2dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
