# [isabelle] Numeral is acting strangely

Hi All,

`I just made a small change to Isabelle to allow input of unsigned hex
``and binary constants:
`
lemma "0x20 = 32" by (rule refl)
lemma "(0x20::nat) = 32" by simp
lemma "(0b11111111::word8) = -1" by simp
Unfortunately, it's got some quirks with the numbers 1 and 0:
lemma "2 = 2" yields (2 :: 'a) = (2 :: 'a) OK, by simp
lemma "0x2 = 2" yields (2 :: 'a) = (2 :: 'a) OK, by simp
lemma "0x02 = 2" yields (2 :: 'a) = (2 :: 'a) OK, by simp
lemma "0x01 = 1" yields Numeral1 = (1 :: 'a) BAD
lemma "0x1 = 1" yields Numeral1 = (1 :: 'a) BAD
lemma "0x0 = 0" yields Numeral0 = (0 :: 'a) BAD

`If I restrict either side to a particular type, it will work, but I get
``lemmas "Numeral1 = 1" and "Numeral0 = 0". The problem exists only for 1
``and 0. I've checked the code which generates the constants, and they are
``fine.
`

`Now to the point. After debugging this thing for much longer than I
``probably should have, I found this:
`lemma "00 = 0" yields Numeral0 = (0 :: 'a)

`This exhibits all the problems I outlined in the previous paragraph.
``This keeps happening even if I revert all my changes to Isabelle, so I
``didn't introduce it.
`As far as I can understand numerals, both sides should be number_of(Pls).
Gentlemen, what gives?
Sincerely,
Rafal Kolanski.

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*