[isabelle-dev] Strange behavior in Word library
matthews at galois.com
Tue Nov 20 01:06:28 CET 2007
If I turn on "show types" in Isabelle_19-Nov-2007 and run the
theory WordTest imports WordMain
lemma "P (ucast ((0b1110 :: 4 word) >> 1) :: 2 word)"
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"
is proved without problems. So it seems there is a bug in the way
word constants are printed out.
More information about the isabelle-dev