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