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.
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
