add quotient_of_div
authorhoelzl
Fri Nov 23 18:28:00 2012 +0100 (2012-11-23)
changeset 50178ad52ddd35c3a
parent 50177 2006c50172c9
child 50179 978200ae8473
child 50180 c6626861c31a
add quotient_of_div
src/HOL/Rat.thy
     1.1 --- a/src/HOL/Rat.thy	Fri Nov 23 17:24:12 2012 +0100
     1.2 +++ b/src/HOL/Rat.thy	Fri Nov 23 18:28:00 2012 +0100
     1.3 @@ -396,6 +396,14 @@
     1.4  lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1"
     1.5    by (simp add: rat_number_expand)
     1.6  
     1.7 +lemma quotient_of_div:
     1.8 +  assumes r: "quotient_of r = (n,d)"
     1.9 +  shows "r = of_int n / of_int d"
    1.10 +proof -
    1.11 +  from theI'[OF quotient_of_unique[of r], unfolded r[unfolded quotient_of_def]]
    1.12 +  have "r = Fract n d" by simp
    1.13 +  thus ?thesis using Fract_of_int_quotient by simp
    1.14 +qed
    1.15  
    1.16  subsubsection {* The ordered field of rational numbers *}
    1.17