Email Gateway (Aug 19 2022 at 09:11): Email Gateway (Aug 19 2022 at 09:11):From: René Thiemann <rene.thiemann@uibk.ac.at>
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é
Email Gateway (Aug 19 2022 at 09:12):From: Johannes Hölzl <hoelzl@in.tum.de>
I added it to the Isabelle repository.
Last updated: Nov 21 2024 at 12:39 UTC