Re: [isabelle] Numeral is acting strangely

Hi Rafal,

actually, in general "Numeral0::'a" is NOT equal to "0::'a".

"Numeral0::'a" is equal to "number_of (Pls)", but "number_of(Pls)" is not necessary equal to "0::'a", because in general,
"number_of :: bin => 'a::number" is not defined.

If "'a::number_ring" though (this includes the cases "int" and "real"), or "'a::nat", then this equality actually holds; for "1::'a" the same is true.
The corresponding lemmas are


Hope this helps,


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?


Rafal Kolanski.

Steven Obua
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching

Tel: ++49 (0)89 / 289-17328
EMail: obua at
Raum: 01.11.059

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