Re: [isabelle] Problem with pretty printing rationals



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:
> 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
> 







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