[isabelle] quotient_of: missing lemma

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

Perhaps this might be added to the distribution.

Best regards,

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