[isabelle-dev] Strange behavior in Word library
gerwin.klein at nicta.com.au
Tue Nov 20 12:44:12 CET 2007
> 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
> 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
More information about the isabelle-dev