# 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

numeral_0_eq_0
numeral_1_eq_1
nat_numeral_0_eq_0
nat_numeral_1_eq_1

Hope this helps,

Steven

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

```
```

--
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 in.tum.de
Raum: 01.11.059

```

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