*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] quotient_of: missing lemma*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Fri, 23 Nov 2012 12:18:31 +0100

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é

**Follow-Ups**:**Re: [isabelle] quotient_of: missing lemma***From:*Johannes Hölzl

- Previous by Date: [isabelle] Title of "Programming and Proving" [Re: ?spam? Re: Simpler theorem statements, and proofs for them]
- Next by Date: Re: [isabelle] Title of "Programming and Proving" [Re: ?spam? Re: Simpler theorem statements, and proofs for them]
- Previous by Thread: Re: [isabelle] Context Free Language
- Next by Thread: Re: [isabelle] quotient_of: missing lemma
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list