Email Gateway (Aug 18 2022 at 14:16): Email Gateway (Aug 18 2022 at 14:16):From: Alexander Krauss <krauss@in.tum.de>
Hi René,
I just encountered the following problem. When writing a pretty printer
for rational numbers the standard function I would like to write is:show_rat (Fract a b) = (if b = 1 then show_int a else show_int a @ ''/''
@ show_int b)"However, since Fract is a only a code_datatype and not a datatype,
Isabelle refused this function definition. (And it must refuse, since
Fract 1 2 = Fract 2 4, but show_rat .. = 1/2 != 2/4 = show_rat ..
Hence, show_rat is not a function.)
Right. This cannot work.
Are there for example
functions like "get_numerator" and "get_denominator" which return unique
results independent of whether using (Fract 1 2) or (Fract 2 4) which I
overlooked in Rational.thy?
There aren't, but it seems that they should be there, so contributions
are welcome (probably a function that returns (int * int) is best). It
can be defined using THE.
Alex
Email Gateway (Aug 18 2022 at 14:16):From: Tobias Nipkow <nipkow@in.tum.de>
The function should be called "normalize :: rat => int * int" and should
also take care of the sign: the denominator should be positive. Since
gcd is there already, it is easy to define directly. Any takers?
Tobias
Alexander Krauss wrote:
Email Gateway (Aug 18 2022 at 14:16):From: René Thiemann <rene.thiemann@uibk.ac.at>
The function should be called "normalize :: rat => int * int" and
should
also take care of the sign: the denominator should be positive. Since
gcd is there already, it is easy to define directly. Any takers?
I have a solution which (I think) is too long for this mailing list.
However, please contact me if you want to have the theory-file.
Cheers,
René
Tobias
Alexander Krauss wrote:
Hi René,
I just encountered the following problem. When writing a pretty
printer for rational numbers the standard function I would like to
write is:show_rat (Fract a b) = (if b = 1 then show_int a else show_int a @
''/'' @ show_int b)"However, since Fract is a only a code_datatype and not a datatype,
Isabelle refused this function definition. (And it must refuse,
since
Fract 1 2 = Fract 2 4, but show_rat .. = 1/2 != 2/4 = show_rat ..
Hence, show_rat is not a function.)Right. This cannot work.
Are there for example functions like "get_numerator" and
"get_denominator" which return unique results independent of whether
using (Fract 1 2) or (Fract 2 4) which I overlooked in Rational.thy?There aren't, but it seems that they should be there, so
contributions
are welcome (probably a function that returns (int * int) is best).
It
can be defined using THE.Alex
Email Gateway (Aug 18 2022 at 14:22):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,
I just encountered the following problem. When writing a pretty
printer for rational numbers the standard function I would like to
write is:
show_rat (Fract a b) = (if b = 1 then show_int a else show_int a @
''/'' @ show_int b)"
However, since Fract is a only a code_datatype and not a datatype,
Isabelle refused this function definition. (And it must refuse, since
Fract 1 2 = Fract 2 4, but show_rat .. = 1/2 != 2/4 = show_rat ..
Hence, show_rat is not a function.)
Instead, I now added an axiom
consts show_rat
axioms show_rat_def[code]: "show_rat (Fract a b) = (if b = 1 then
show_int a else show_int a @ ''/'' @ show_int b)"
Now, the code-generator is working. However, I do not like to add
axioms to my theory, so is there a better way around? Are there for
example functions like "get_numerator" and "get_denominator" which
return unique results independent of whether using (Fract 1 2) or
(Fract 2 4) which I overlooked in Rational.thy?
Thanks a lot,
René
Last updated: Apr 24 2024 at 04:17 UTC