[isabelle-dev] Strange behavior in Word library

[Gerwin Klein]

Hi John,

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

Thanks. Further checking reveals that this probably never worked for arbitrary 
P (I've checked as far back as Dec 2006).

It shouldn't actually be hard to implement. I think it will come down to a 
simp proc on word literals of concrete numeral type, normalising them to 
their respective word length by truncating the binary representation at the 
right position. The theorems for that are already there, I believe, but they 
can't be just declared as [simp], because they would loop. 

Since this requires a bit of ML coding and we are already in feature freeze 
for the release, I'd say we postpone this to after Isabelle2007. Note that 
this only applies to literals occurring as a deep sub term, things like 
"7 = (0b11::2 word)" are still shown automatically by simp.

It should be possible to provide this in a separate theory such that no 
upgrading to new Isabelle development releases would be necessary to use the 
normalisation. 

Cheers,
Gerwin


> 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