[isabelle-dev] Strange behavior in Word library

[John Matthews]

Hi Gerwin,

For recent snapshots, I only have the Aug_08, Oct_10, and Nov_19  
versions. The problem shows up on both the Nov_19 and Oct_10  
snapshots. The Aug_08 snapshot doesn't contain the Word library, as  
far as I could tell. Hope this helps.

Cheers,
-john

On Nov 19, 2007, at 4:25 PM, Gerwin Klein wrote:

> John Matthews wrote:
>> If I turn on "show types" in Isabelle_19-Nov-2007 and run the   
>> following commands:
>>    theory WordTest imports WordMain
>>    begin
>>    lemma "P (ucast ((0b1110 :: 4 word) >> 1) :: 2 word)"
>>    apply simp
>> Isabelle displays the simplified subgoal as:
>>    goal (1 subgoal):
>>     1. P (7::2 word)
>>    variables:
>>     P :: 2 word :: bool
>> Notice the subterm "7::2 word" showing up in the subgoal, which  
>> isn't  right. On the other hand, the formula
>>    lemma "(ucast ((0b1110 :: 4 word) >> 1) :: 2 word) = 0b11"
>>    by simp
>> is proved without problems. So it seems there is a bug in the way   
>> word constants are printed out.
>
> The problem seems to be that the normalisation simp rules are not  
> used. The printing is ok (it's just the usual Isabelle integer  
> printing).
>
> It is true that "7 = 0b11" in 2 word, though, so it's not actually  
> showing something false, just something confusing. I'll  
> investigate. Do you know in which version this last worked correctly?
>
> Cheers,
> Gerwin