[isabelle-dev] Strange behavior in Word library
matthews at galois.com
Tue Nov 20 01:41:47 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.
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
>> 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)
>> 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
> 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?
More information about the isabelle-dev