Email Gateway (Aug 17 2022 at 14:49): Email Gateway (Aug 17 2022 at 14:49):From: Makarius <makarius@sketis.net>
You seem to using a recent development snapshot. Here Numeral1 is a
first-class term abbreviation, i.e. it may appear as a Const at some
point, but is expanded eventually (during term certification at the
latest).
Your read ML function seems to refer to rather old internal interfaces,
based on Sign.read_def_terms. Try ProofContext.read_term to get the usual
user-level thing.
Makarius
Email Gateway (Aug 17 2022 at 14:49):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
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"
but
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".
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?
Cheers,
Rafal Kolanski.
Email Gateway (Aug 17 2022 at 14:49):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Steven Obua wrote:
Thank you, I get it now. It's so easy to get confused when thinking of
numbers as numbers! This also means that despite appearing strange, my
patch is actually functioning correctly.
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 09:29):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
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.
Email Gateway (Aug 18 2022 at 09:31):From: Lawrence Paulson <lp15@cam.ac.uk>
0 and 1 are constants in their own right. They are not made by
number_of. Their number_of equivalents are displayed as Numeral0 and
Numeral1. Having 0 and 1 as constants allows them to be involved in
many axiomatic type classes concerning algebraic properties. Users
normally should not notice.
A related issue: for type nat, while 1 = Suc 0, this is not a
syntactic identity.
Larry Paulson
Email Gateway (Aug 18 2022 at 09:31):From: Steven Obua <obua@in.tum.de>
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
Email Gateway (Aug 18 2022 at 09:31):From: Steven Obua <obua@in.tum.de>
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"but
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.
Steven
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?Cheers,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 09:32):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Lawrence Paulson wrote:
But there 's something more than this going on that seems odd.
read "Numeral1";
val it = Const ("Numeral.Numeral1", "'a::Numeral.number") : Term.term
So Numeral1 is a constant in its own right
(tc is a smarter version of thms_containing)
tc["Numeral1"];
Exception- ERROR "thms_containing: undeclared consts \"Numeral.Numeral1\""
raised
tc["Numeral.Numeral1"];
Exception- ERROR "thms_containing: undeclared consts \"Numeral.Numeral1\""
raised
Goal "Numeral1 = 1" ;
Level 0 (1 subgoal)
number_of (Numeral.Pls BIT bit.B1) = (1::'a)
1. number_of (Numeral.Pls BIT bit.B1) = (1::'a)
But here the constant "Numeral.Numeral1" somehow gets translated to
number_of (Numeral.Pls BIT bit.B1)
What is happening here?
Jeremy
Last updated: May 03 2024 at 08:18 UTC