[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.