[isabelle] Numeral is acting strangely
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
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and