*To*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Subject*: Re: [isabelle] Numeral is acting strangely*From*: Steven Obua <obua at in.tum.de>*Date*: Tue, 04 Jul 2006 11:37:07 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <44A8DB95.7010908@cse.unsw.edu.au>*References*: <44A8DB95.7010908@cse.unsw.edu.au>*User-agent*: Mozilla/5.0 (X11; U; SunOS sun4u; en-US; rv:1.7.3) Gecko/20040915

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

"number_of :: bin => 'a::number" is not defined.

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 hexand 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) BADIf I restrict either side to a particular type, it will work, but Iget lemmas "Numeral1 = 1" and "Numeral0 = 0". The problem exists onlyfor 1 and 0. I've checked the code which generates the constants, andthey are fine.Now to the point. After debugging this thing for much longer than Iprobably 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 Ididn'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

**Follow-Ups**:**Re: [isabelle] Numeral is acting strangely***From:*Rafal Kolanski

**References**:**[isabelle] Numeral is acting strangely***From:*Rafal Kolanski

- Previous by Date: Re: [isabelle] Numeral is acting strangely
- Next by Date: Re: [isabelle] Numeral is acting strangely
- Previous by Thread: Re: [isabelle] Exception- ERROR "congc result" raised
- Next by Thread: Re: [isabelle] Numeral is acting strangely
- Cl-isabelle-users July 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list