# HG changeset patch
# User hoelzl
# Date 1353691680 -3600
# Node ID ad52ddd35c3acc2d80d8dc32cd6f25a88637db6f
# Parent  2006c50172c92832913b80984d0562027412b438
add quotient_of_div

diff -r 2006c50172c9 -r ad52ddd35c3a src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Fri Nov 23 17:24:12 2012 +0100
+++ b/src/HOL/Rat.thy	Fri Nov 23 18:28:00 2012 +0100
@@ -396,6 +396,14 @@
 lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1"
   by (simp add: rat_number_expand)
 
+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
 
 subsubsection {* The ordered field of rational numbers *}