[isabelle-dev] Strange behavior in Word library

[Gerwin Klein]

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