Re: [isabelle] Numeral is acting strangely

Rafal Kolanski wrote:

Steven Obua wrote:

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

I figured that out. What I can't figure out is why

term "0" is    "0::'a" :: "'a"
term "1" is    "1::'a" :: "'a"
term "2" is    "2::'a" :: "'a"


term "00" is    "Numeral0" :: "'a"
term "01" is    "Numeral1" :: "'a"
term "02" is    "2::'a" :: "'a"

Does that make any sense to you? 00 is intuitively just 0, just like 01 is 1. Instead we get "Numeral0" and "Numeral1", but for 02 we get "2".

As Larry already pointed out, "0" and "1" are actually declared global constants (see HOL.thy in the isabelle/src/HOL directory), while "2", "3" and so on are not. Therefore the parser recognizes these global constants first. "00" is not a declared constant, therefore it is passed on to the functions in numeral_syntax.ML. So to me it makes perfect sense (it may not be intuitive, though :-)).

"2::'a" is just a pretty-printed version of a more complex term. You cannot pretty-print "Numeral0" in that way, because then "Numeral0" would have to become "0", but as you already figured out, "Numeral0" is not the same as "0", therefore this pretty-printing would be maybe intuitive, but wrong.


In the hex input modification, I want 0x0 to be 0, and 0x1 to be 1. I'm already getting 0x2 to be 2.

Larry Paulson already indicated that 0 and 1 are "special", but it isn't clear to me how it applies to this case. Does isabelle actually single out 1 and 0 before we get to the functions in HOL/Tools/numeral_syntax.ML?


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.