(* Title: HOL/Rat.thy
Author: Markus Wenzel, TU Muenchen
*)
header {* Rational numbers *}
theory Rat
imports GCD Archimedean_Field
uses ("Tools/float_syntax.ML")
begin
subsection {* Rational numbers as quotient *}
subsubsection {* Construction of the type of rational numbers *}
definition
ratrel :: "(int \ int) \ (int \ int) \ bool" where
"ratrel = (\x y. snd x \ 0 \ snd y \ 0 \ fst x * snd y = fst y * snd x)"
lemma ratrel_iff [simp]:
"ratrel x y \ snd x \ 0 \ snd y \ 0 \ fst x * snd y = fst y * snd x"
by (simp add: ratrel_def)
lemma exists_ratrel_refl: "\x. ratrel x x"
by (auto intro!: one_neq_zero)
lemma symp_ratrel: "symp ratrel"
by (simp add: ratrel_def symp_def)
lemma transp_ratrel: "transp ratrel"
proof (rule transpI, unfold split_paired_all)
fix a b a' b' a'' b'' :: int
assume A: "ratrel (a, b) (a', b')"
assume B: "ratrel (a', b') (a'', b'')"
have "b' * (a * b'') = b'' * (a * b')" by simp
also from A have "a * b' = a' * b" by auto
also have "b'' * (a' * b) = b * (a' * b'')" by simp
also from B have "a' * b'' = a'' * b'" by auto
also have "b * (a'' * b') = b' * (a'' * b)" by simp
finally have "b' * (a * b'') = b' * (a'' * b)" .
moreover from B have "b' \ 0" by auto
ultimately have "a * b'' = a'' * b" by simp
with A B show "ratrel (a, b) (a'', b'')" by auto
qed
lemma part_equivp_ratrel: "part_equivp ratrel"
by (rule part_equivpI [OF exists_ratrel_refl symp_ratrel transp_ratrel])
quotient_type rat = "int \ int" / partial: "ratrel"
morphisms Rep_Rat Abs_Rat
by (rule part_equivp_ratrel)
declare rat.forall_transfer [transfer_rule del]
lemma forall_rat_transfer [transfer_rule]: (* TODO: generate automatically *)
"(fun_rel (fun_rel cr_rat op =) op =)
(transfer_bforall (\x. snd x \ 0)) transfer_forall"
using rat.forall_transfer by simp
subsubsection {* Representation and basic operations *}
lift_definition Fract :: "int \ int \ rat"
is "\a b. if b = 0 then (0, 1) else (a, b)"
by simp
lemma eq_rat:
shows "\a b c d. b \ 0 \ d \ 0 \ Fract a b = Fract c d \ a * d = c * b"
and "\a. Fract a 0 = Fract 0 1"
and "\a c. Fract 0 a = Fract 0 c"
by (transfer, simp)+
lemma Rat_cases [case_names Fract, cases type: rat]:
assumes "\a b. q = Fract a b \ b > 0 \ coprime a b \ C"
shows C
proof -
obtain a b :: int where "q = Fract a b" and "b \ 0"
by transfer simp
let ?a = "a div gcd a b"
let ?b = "b div gcd a b"
from `b \ 0` have "?b * gcd a b = b"
by (simp add: dvd_div_mult_self)
with `b \ 0` have "?b \ 0" by auto
from `q = Fract a b` `b \ 0` `?b \ 0` have q: "q = Fract ?a ?b"
by (simp add: eq_rat dvd_div_mult mult_commute [of a])
from `b \ 0` have coprime: "coprime ?a ?b"
by (auto intro: div_gcd_coprime_int)
show C proof (cases "b > 0")
case True
note assms
moreover note q
moreover from True have "?b > 0" by (simp add: nonneg1_imp_zdiv_pos_iff)
moreover note coprime
ultimately show C .
next
case False
note assms
moreover have "q = Fract (- ?a) (- ?b)" unfolding q by transfer simp
moreover from False `b \ 0` have "- ?b > 0" by (simp add: pos_imp_zdiv_neg_iff)
moreover from coprime have "coprime (- ?a) (- ?b)" by simp
ultimately show C .
qed
qed
lemma Rat_induct [case_names Fract, induct type: rat]:
assumes "\a b. b > 0 \ coprime a b \ P (Fract a b)"
shows "P q"
using assms by (cases q) simp
instantiation rat :: field_inverse_zero
begin
lift_definition zero_rat :: "rat" is "(0, 1)"
by simp
lift_definition one_rat :: "rat" is "(1, 1)"
by simp
lemma Zero_rat_def: "0 = Fract 0 1"
by transfer simp
lemma One_rat_def: "1 = Fract 1 1"
by transfer simp
lift_definition plus_rat :: "rat \ rat \ rat"
is "\x y. (fst x * snd y + fst y * snd x, snd x * snd y)"
by (clarsimp, simp add: left_distrib, simp add: mult_ac)
lemma add_rat [simp]:
assumes "b \ 0" and "d \ 0"
shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)"
using assms by transfer simp
lift_definition uminus_rat :: "rat \ rat" is "\x. (- fst x, snd x)"
by simp
lemma minus_rat [simp]: "- Fract a b = Fract (- a) b"
by transfer simp
lemma minus_rat_cancel [simp]: "Fract (- a) (- b) = Fract a b"
by (cases "b = 0") (simp_all add: eq_rat)
definition
diff_rat_def: "q - r = q + - (r::rat)"
lemma diff_rat [simp]:
assumes "b \ 0" and "d \ 0"
shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)"
using assms by (simp add: diff_rat_def)
lift_definition times_rat :: "rat \ rat \ rat"
is "\x y. (fst x * fst y, snd x * snd y)"
by (simp add: mult_ac)
lemma mult_rat [simp]: "Fract a b * Fract c d = Fract (a * c) (b * d)"
by transfer simp
lemma mult_rat_cancel:
assumes "c \ 0"
shows "Fract (c * a) (c * b) = Fract a b"
using assms by transfer simp
lift_definition inverse_rat :: "rat \ rat"
is "\x. if fst x = 0 then (0, 1) else (snd x, fst x)"
by (auto simp add: mult_commute)
lemma inverse_rat [simp]: "inverse (Fract a b) = Fract b a"
by transfer simp
definition
divide_rat_def: "q / r = q * inverse (r::rat)"
lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
by (simp add: divide_rat_def)
instance proof
fix q r s :: rat
show "(q * r) * s = q * (r * s)"
by transfer simp
show "q * r = r * q"
by transfer simp
show "1 * q = q"
by transfer simp
show "(q + r) + s = q + (r + s)"
by transfer (simp add: algebra_simps)
show "q + r = r + q"
by transfer simp
show "0 + q = q"
by transfer simp
show "- q + q = 0"
by transfer simp
show "q - r = q + - r"
by (fact diff_rat_def)
show "(q + r) * s = q * s + r * s"
by transfer (simp add: algebra_simps)
show "(0::rat) \ 1"
by transfer simp
{ assume "q \ 0" thus "inverse q * q = 1"
by transfer simp }
show "q / r = q * inverse r"
by (fact divide_rat_def)
show "inverse 0 = (0::rat)"
by transfer simp
qed
end
lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1"
by (induct k) (simp_all add: Zero_rat_def One_rat_def)
lemma of_int_rat: "of_int k = Fract k 1"
by (cases k rule: int_diff_cases) (simp add: of_nat_rat)
lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k"
by (rule of_nat_rat [symmetric])
lemma Fract_of_int_eq: "Fract k 1 = of_int k"
by (rule of_int_rat [symmetric])
lemma rat_number_collapse:
"Fract 0 k = 0"
"Fract 1 1 = 1"
"Fract (numeral w) 1 = numeral w"
"Fract (neg_numeral w) 1 = neg_numeral w"
"Fract k 0 = 0"
using Fract_of_int_eq [of "numeral w"]
using Fract_of_int_eq [of "neg_numeral w"]
by (simp_all add: Zero_rat_def One_rat_def eq_rat)
lemma rat_number_expand:
"0 = Fract 0 1"
"1 = Fract 1 1"
"numeral k = Fract (numeral k) 1"
"neg_numeral k = Fract (neg_numeral k) 1"
by (simp_all add: rat_number_collapse)
lemma Rat_cases_nonzero [case_names Fract 0]:
assumes Fract: "\a b. q = Fract a b \ b > 0 \ a \ 0 \ coprime a b \ C"
assumes 0: "q = 0 \ C"
shows C
proof (cases "q = 0")
case True then show C using 0 by auto
next
case False
then obtain a b where "q = Fract a b" and "b > 0" and "coprime a b" by (cases q) auto
moreover with False have "0 \ Fract a b" by simp
with `b > 0` have "a \ 0" by (simp add: Zero_rat_def eq_rat)
with Fract `q = Fract a b` `b > 0` `coprime a b` show C by blast
qed
subsubsection {* Function @{text normalize} *}
lemma Fract_coprime: "Fract (a div gcd a b) (b div gcd a b) = Fract a b"
proof (cases "b = 0")
case True then show ?thesis by (simp add: eq_rat)
next
case False
moreover have "b div gcd a b * gcd a b = b"
by (rule dvd_div_mult_self) simp
ultimately have "b div gcd a b \ 0" by auto
with False show ?thesis by (simp add: eq_rat dvd_div_mult mult_commute [of a])
qed
definition normalize :: "int \ int \ int \ int" where
"normalize p = (if snd p > 0 then (let a = gcd (fst p) (snd p) in (fst p div a, snd p div a))
else if snd p = 0 then (0, 1)
else (let a = - gcd (fst p) (snd p) in (fst p div a, snd p div a)))"
lemma normalize_crossproduct:
assumes "q \ 0" "s \ 0"
assumes "normalize (p, q) = normalize (r, s)"
shows "p * s = r * q"
proof -
have aux: "p * gcd r s = sgn (q * s) * r * gcd p q \ q * gcd r s = sgn (q * s) * s * gcd p q \ p * s = q * r"
proof -
assume "p * gcd r s = sgn (q * s) * r * gcd p q" and "q * gcd r s = sgn (q * s) * s * gcd p q"
then have "(p * gcd r s) * (sgn (q * s) * s * gcd p q) = (q * gcd r s) * (sgn (q * s) * r * gcd p q)" by simp
with assms show "p * s = q * r" by (auto simp add: mult_ac sgn_times sgn_0_0)
qed
from assms show ?thesis
by (auto simp add: normalize_def Let_def dvd_div_div_eq_mult mult_commute sgn_times split: if_splits intro: aux)
qed
lemma normalize_eq: "normalize (a, b) = (p, q) \ Fract p q = Fract a b"
by (auto simp add: normalize_def Let_def Fract_coprime dvd_div_neg rat_number_collapse
split:split_if_asm)
lemma normalize_denom_pos: "normalize r = (p, q) \ q > 0"
by (auto simp add: normalize_def Let_def dvd_div_neg pos_imp_zdiv_neg_iff nonneg1_imp_zdiv_pos_iff
split:split_if_asm)
lemma normalize_coprime: "normalize r = (p, q) \ coprime p q"
by (auto simp add: normalize_def Let_def dvd_div_neg div_gcd_coprime_int
split:split_if_asm)
lemma normalize_stable [simp]:
"q > 0 \ coprime p q \ normalize (p, q) = (p, q)"
by (simp add: normalize_def)
lemma normalize_denom_zero [simp]:
"normalize (p, 0) = (0, 1)"
by (simp add: normalize_def)
lemma normalize_negative [simp]:
"q < 0 \ normalize (p, q) = normalize (- p, - q)"
by (simp add: normalize_def Let_def dvd_div_neg dvd_neg_div)
text{*
Decompose a fraction into normalized, i.e. coprime numerator and denominator:
*}
definition quotient_of :: "rat \ int \ int" where
"quotient_of x = (THE pair. x = Fract (fst pair) (snd pair) &
snd pair > 0 & coprime (fst pair) (snd pair))"
lemma quotient_of_unique:
"\!p. r = Fract (fst p) (snd p) \ snd p > 0 \ coprime (fst p) (snd p)"
proof (cases r)
case (Fract a b)
then have "r = Fract (fst (a, b)) (snd (a, b)) \ snd (a, b) > 0 \ coprime (fst (a, b)) (snd (a, b))" by auto
then show ?thesis proof (rule ex1I)
fix p
obtain c d :: int where p: "p = (c, d)" by (cases p)
assume "r = Fract (fst p) (snd p) \ snd p > 0 \ coprime (fst p) (snd p)"
with p have Fract': "r = Fract c d" "d > 0" "coprime c d" by simp_all
have "c = a \ d = b"
proof (cases "a = 0")
case True with Fract Fract' show ?thesis by (simp add: eq_rat)
next
case False
with Fract Fract' have *: "c * b = a * d" and "c \ 0" by (auto simp add: eq_rat)
then have "c * b > 0 \ a * d > 0" by auto
with `b > 0` `d > 0` have "a > 0 \ c > 0" by (simp add: zero_less_mult_iff)
with `a \ 0` `c \ 0` have sgn: "sgn a = sgn c" by (auto simp add: not_less)
from `coprime a b` `coprime c d` have "\a\ * \d\ = \c\ * \b\ \ \a\ = \c\ \ \d\ = \b\"
by (simp add: coprime_crossproduct_int)
with `b > 0` `d > 0` have "\a\ * d = \c\ * b \ \a\ = \c\ \ d = b" by simp
then have "a * sgn a * d = c * sgn c * b \ a * sgn a = c * sgn c \ d = b" by (simp add: abs_sgn)
with sgn * show ?thesis by (auto simp add: sgn_0_0)
qed
with p show "p = (a, b)" by simp
qed
qed
lemma quotient_of_Fract [code]:
"quotient_of (Fract a b) = normalize (a, b)"
proof -
have "Fract a b = Fract (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?Fract)
by (rule sym) (auto intro: normalize_eq)
moreover have "0 < snd (normalize (a, b))" (is ?denom_pos)
by (cases "normalize (a, b)") (rule normalize_denom_pos, simp)
moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime)
by (rule normalize_coprime) simp
ultimately have "?Fract \ ?denom_pos \ ?coprime" by blast
with quotient_of_unique have
"(THE p. Fract a b = Fract (fst p) (snd p) \ 0 < snd p \ coprime (fst p) (snd p)) = normalize (a, b)"
by (rule the1_equality)
then show ?thesis by (simp add: quotient_of_def)
qed
lemma quotient_of_number [simp]:
"quotient_of 0 = (0, 1)"
"quotient_of 1 = (1, 1)"
"quotient_of (numeral k) = (numeral k, 1)"
"quotient_of (neg_numeral k) = (neg_numeral k, 1)"
by (simp_all add: rat_number_expand quotient_of_Fract)
lemma quotient_of_eq: "quotient_of (Fract a b) = (p, q) \ Fract p q = Fract a b"
by (simp add: quotient_of_Fract normalize_eq)
lemma quotient_of_denom_pos: "quotient_of r = (p, q) \ q > 0"
by (cases r) (simp add: quotient_of_Fract normalize_denom_pos)
lemma quotient_of_coprime: "quotient_of r = (p, q) \ coprime p q"
by (cases r) (simp add: quotient_of_Fract normalize_coprime)
lemma quotient_of_inject:
assumes "quotient_of a = quotient_of b"
shows "a = b"
proof -
obtain p q r s where a: "a = Fract p q"
and b: "b = Fract r s"
and "q > 0" and "s > 0" by (cases a, cases b)
with assms show ?thesis by (simp add: eq_rat quotient_of_Fract normalize_crossproduct)
qed
lemma quotient_of_inject_eq:
"quotient_of a = quotient_of b \ a = b"
by (auto simp add: quotient_of_inject)
subsubsection {* Various *}
lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l"
by (simp add: Fract_of_int_eq [symmetric])
lemma Fract_add_one: "n \ 0 ==> Fract (m + n) n = Fract m n + 1"
by (simp add: rat_number_expand)
subsubsection {* The ordered field of rational numbers *}
instantiation rat :: linorder
begin
lift_definition less_eq_rat :: "rat \ rat \ bool"
is "\x y. (fst x * snd y) * (snd x * snd y) \ (fst y * snd x) * (snd x * snd y)"
proof (clarsimp)
fix a b a' b' c d c' d'::int
assume neq: "b \ 0" "b' \ 0" "d \ 0" "d' \ 0"
assume eq1: "a * b' = a' * b"
assume eq2: "c * d' = c' * d"
let ?le = "\a b c d. ((a * d) * (b * d) \ (c * b) * (b * d))"
{
fix a b c d x :: int assume x: "x \ 0"
have "?le a b c d = ?le (a * x) (b * x) c d"
proof -
from x have "0 < x * x" by (auto simp add: zero_less_mult_iff)
hence "?le a b c d =
((a * d) * (b * d) * (x * x) \ (c * b) * (b * d) * (x * x))"
by (simp add: mult_le_cancel_right)
also have "... = ?le (a * x) (b * x) c d"
by (simp add: mult_ac)
finally show ?thesis .
qed
} note le_factor = this
let ?D = "b * d" and ?D' = "b' * d'"
from neq have D: "?D \ 0" by simp
from neq have "?D' \ 0" by simp
hence "?le a b c d = ?le (a * ?D') (b * ?D') c d"
by (rule le_factor)
also have "... = ((a * b') * ?D * ?D' * d * d' \ (c * d') * ?D * ?D' * b * b')"
by (simp add: mult_ac)
also have "... = ((a' * b) * ?D * ?D' * d * d' \ (c' * d) * ?D * ?D' * b * b')"
by (simp only: eq1 eq2)
also have "... = ?le (a' * ?D) (b' * ?D) c' d'"
by (simp add: mult_ac)
also from D have "... = ?le a' b' c' d'"
by (rule le_factor [symmetric])
finally show "?le a b c d = ?le a' b' c' d'" .
qed
lemma le_rat [simp]:
assumes "b \ 0" and "d \ 0"
shows "Fract a b \ Fract c d \ (a * d) * (b * d) \ (c * b) * (b * d)"
using assms by transfer simp
definition
less_rat_def: "z < (w::rat) \ z \ w \ z \ w"
lemma less_rat [simp]:
assumes "b \ 0" and "d \ 0"
shows "Fract a b < Fract c d \ (a * d) * (b * d) < (c * b) * (b * d)"
using assms by (simp add: less_rat_def eq_rat order_less_le)
instance proof
fix q r s :: rat
{
assume "q \ r" and "r \ s"
then show "q \ s"
proof (induct q, induct r, induct s)
fix a b c d e f :: int
assume neq: "b > 0" "d > 0" "f > 0"
assume 1: "Fract a b \ Fract c d" and 2: "Fract c d \ Fract e f"
show "Fract a b \ Fract e f"
proof -
from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f"
by (auto simp add: zero_less_mult_iff linorder_neq_iff)
have "(a * d) * (b * d) * (f * f) \ (c * b) * (b * d) * (f * f)"
proof -
from neq 1 have "(a * d) * (b * d) \ (c * b) * (b * d)"
by simp
with ff show ?thesis by (simp add: mult_le_cancel_right)
qed
also have "... = (c * f) * (d * f) * (b * b)" by algebra
also have "... \ (e * d) * (d * f) * (b * b)"
proof -
from neq 2 have "(c * f) * (d * f) \ (e * d) * (d * f)"
by simp
with bb show ?thesis by (simp add: mult_le_cancel_right)
qed
finally have "(a * f) * (b * f) * (d * d) \ e * b * (b * f) * (d * d)"
by (simp only: mult_ac)
with dd have "(a * f) * (b * f) \ (e * b) * (b * f)"
by (simp add: mult_le_cancel_right)
with neq show ?thesis by simp
qed
qed
next
assume "q \ r" and "r \ q"
then show "q = r"
proof (induct q, induct r)
fix a b c d :: int
assume neq: "b > 0" "d > 0"
assume 1: "Fract a b \ Fract c d" and 2: "Fract c d \ Fract a b"
show "Fract a b = Fract c d"
proof -
from neq 1 have "(a * d) * (b * d) \ (c * b) * (b * d)"
by simp
also have "... \ (a * d) * (b * d)"
proof -
from neq 2 have "(c * b) * (d * b) \ (a * d) * (d * b)"
by simp
thus ?thesis by (simp only: mult_ac)
qed
finally have "(a * d) * (b * d) = (c * b) * (b * d)" .
moreover from neq have "b * d \ 0" by simp
ultimately have "a * d = c * b" by simp
with neq show ?thesis by (simp add: eq_rat)
qed
qed
next
show "q \ q"
by (induct q) simp
show "(q < r) = (q \ r \ \ r \ q)"
by (induct q, induct r) (auto simp add: le_less mult_commute)
show "q \ r \ r \ q"
by (induct q, induct r)
(simp add: mult_commute, rule linorder_linear)
}
qed
end
instantiation rat :: "{distrib_lattice, abs_if, sgn_if}"
begin
definition
abs_rat_def: "\q\ = (if q < 0 then -q else (q::rat))"
lemma abs_rat [simp, code]: "\Fract a b\ = Fract \a\ \b\"
by (auto simp add: abs_rat_def zabs_def Zero_rat_def not_less le_less eq_rat zero_less_mult_iff)
definition
sgn_rat_def: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else - 1)"
lemma sgn_rat [simp, code]: "sgn (Fract a b) = of_int (sgn a * sgn b)"
unfolding Fract_of_int_eq
by (auto simp: zsgn_def sgn_rat_def Zero_rat_def eq_rat)
(auto simp: rat_number_collapse not_less le_less zero_less_mult_iff)
definition
"(inf \ rat \ rat \ rat) = min"
definition
"(sup \ rat \ rat \ rat) = max"
instance by intro_classes
(auto simp add: abs_rat_def sgn_rat_def min_max.sup_inf_distrib1 inf_rat_def sup_rat_def)
end
instance rat :: linordered_field_inverse_zero
proof
fix q r s :: rat
show "q \ r ==> s + q \ s + r"
proof (induct q, induct r, induct s)
fix a b c d e f :: int
assume neq: "b > 0" "d > 0" "f > 0"
assume le: "Fract a b \ Fract c d"
show "Fract e f + Fract a b \ Fract e f + Fract c d"
proof -
let ?F = "f * f" from neq have F: "0 < ?F"
by (auto simp add: zero_less_mult_iff)
from neq le have "(a * d) * (b * d) \ (c * b) * (b * d)"
by simp
with F have "(a * d) * (b * d) * ?F * ?F \ (c * b) * (b * d) * ?F * ?F"
by (simp add: mult_le_cancel_right)
with neq show ?thesis by (simp add: mult_ac int_distrib)
qed
qed
show "q < r ==> 0 < s ==> s * q < s * r"
proof (induct q, induct r, induct s)
fix a b c d e f :: int
assume neq: "b > 0" "d > 0" "f > 0"
assume le: "Fract a b < Fract c d"
assume gt: "0 < Fract e f"
show "Fract e f * Fract a b < Fract e f * Fract c d"
proof -
let ?E = "e * f" and ?F = "f * f"
from neq gt have "0 < ?E"
by (auto simp add: Zero_rat_def order_less_le eq_rat)
moreover from neq have "0 < ?F"
by (auto simp add: zero_less_mult_iff)
moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)"
by simp
ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F"
by (simp add: mult_less_cancel_right)
with neq show ?thesis
by (simp add: mult_ac)
qed
qed
qed auto
lemma Rat_induct_pos [case_names Fract, induct type: rat]:
assumes step: "\a b. 0 < b \ P (Fract a b)"
shows "P q"
proof (cases q)
have step': "\a b. b < 0 \ P (Fract a b)"
proof -
fix a::int and b::int
assume b: "b < 0"
hence "0 < -b" by simp
hence "P (Fract (-a) (-b))" by (rule step)
thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b])
qed
case (Fract a b)
thus "P q" by (force simp add: linorder_neq_iff step step')
qed
lemma zero_less_Fract_iff:
"0 < b \ 0 < Fract a b \ 0 < a"
by (simp add: Zero_rat_def zero_less_mult_iff)
lemma Fract_less_zero_iff:
"0 < b \ Fract a b < 0 \ a < 0"
by (simp add: Zero_rat_def mult_less_0_iff)
lemma zero_le_Fract_iff:
"0 < b \ 0 \ Fract a b \ 0 \ a"
by (simp add: Zero_rat_def zero_le_mult_iff)
lemma Fract_le_zero_iff:
"0 < b \ Fract a b \ 0 \ a \ 0"
by (simp add: Zero_rat_def mult_le_0_iff)
lemma one_less_Fract_iff:
"0 < b \ 1 < Fract a b \ b < a"
by (simp add: One_rat_def mult_less_cancel_right_disj)
lemma Fract_less_one_iff:
"0 < b \ Fract a b < 1 \ a < b"
by (simp add: One_rat_def mult_less_cancel_right_disj)
lemma one_le_Fract_iff:
"0 < b \ 1 \ Fract a b \ b \ a"
by (simp add: One_rat_def mult_le_cancel_right)
lemma Fract_le_one_iff:
"0 < b \ Fract a b \ 1 \ a \ b"
by (simp add: One_rat_def mult_le_cancel_right)
subsubsection {* Rationals are an Archimedean field *}
lemma rat_floor_lemma:
shows "of_int (a div b) \ Fract a b \ Fract a b < of_int (a div b + 1)"
proof -
have "Fract a b = of_int (a div b) + Fract (a mod b) b"
by (cases "b = 0", simp, simp add: of_int_rat)
moreover have "0 \ Fract (a mod b) b \ Fract (a mod b) b < 1"
unfolding Fract_of_int_quotient
by (rule linorder_cases [of b 0]) (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos)
ultimately show ?thesis by simp
qed
instance rat :: archimedean_field
proof
fix r :: rat
show "\z. r \ of_int z"
proof (induct r)
case (Fract a b)
have "Fract a b \ of_int (a div b + 1)"
using rat_floor_lemma [of a b] by simp
then show "\z. Fract a b \ of_int z" ..
qed
qed
instantiation rat :: floor_ceiling
begin
definition [code del]:
"floor (x::rat) = (THE z. of_int z \ x \ x < of_int (z + 1))"
instance proof
fix x :: rat
show "of_int (floor x) \ x \