Re: [isabelle] quotient_of: missing lemma



I added it to the Isabelle repository.

 - Johannes

Am Freitag, den 23.11.2012, 12:18 +0100 schrieb René Thiemann:
> Dear all,
> 
> recently I had to work with rational numbers which I had to split into denominator and numerator. To this end, quotient_of can be used, but there was one essential lemma missing, namely that the rational number is exactly numerator / denominator.
> 
> lemma quotient_of_div: assumes r: "quotient_of r = (n,d)"
>   shows "r = of_int n / of_int d"
> proof -
>   from theI'[OF quotient_of_unique[of r], unfolded r[unfolded quotient_of_def]] 
>   have "r = Fract n d" by simp
>   thus ?thesis using Fract_of_int_quotient by simp
> qed
> 
> Perhaps this might be added to the distribution.
> 
> Best regards,
> René







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