Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] quotient_of: missing lemma


view this post on Zulip 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é

view this post on Zulip 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: Mar 28 2024 at 08:18 UTC