1.1 --- a/src/HOL/Rational.thy Fri Nov 20 07:23:36 2009 +0100
1.2 +++ b/src/HOL/Rational.thy Fri Nov 20 07:24:08 2009 +0100
1.3 @@ -243,6 +243,166 @@
1.4 with Fract `q = Fract a b` `b \<noteq> 0` show C by auto
1.5 qed
1.6
1.7 +subsubsection {* Function @{text normalize} *}
1.8 +
1.9 +text{*
1.10 +Decompose a fraction into normalized, i.e. coprime numerator and denominator:
1.11 +*}
1.12 +
1.13 +definition normalize :: "rat \<Rightarrow> int \<times> int" where
1.14 +"normalize x \<equiv> THE pair. x = Fract (fst pair) (snd pair) &
1.15 + snd pair > 0 & gcd (fst pair) (snd pair) = 1"
1.16 +
1.17 +declare normalize_def[code del]
1.18 +
1.19 +lemma Fract_norm: "Fract (a div gcd a b) (b div gcd a b) = Fract a b"
1.20 +proof (cases "a = 0 | b = 0")
1.21 + case True then show ?thesis by (auto simp add: eq_rat)
1.22 +next
1.23 + let ?c = "gcd a b"
1.24 + case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
1.25 + then have "?c \<noteq> 0" by simp
1.26 + then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat)
1.27 + moreover have "Fract (a div ?c * ?c + a mod ?c) (b div ?c * ?c + b mod ?c) = Fract a b"
1.28 + by (simp add: semiring_div_class.mod_div_equality)
1.29 + moreover have "a mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
1.30 + moreover have "b mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
1.31 + ultimately show ?thesis
1.32 + by (simp add: mult_rat [symmetric])
1.33 +qed
1.34 +
1.35 +text{* Proof by Ren\'e Thiemann: *}
1.36 +lemma normalize_code[code]:
1.37 +"normalize (Fract a b) =
1.38 + (if b > 0 then (let g = gcd a b in (a div g, b div g))
1.39 + else if b = 0 then (0,1)
1.40 + else (let g = - gcd a b in (a div g, b div g)))"
1.41 +proof -
1.42 + let ?cond = "% r p. r = Fract (fst p) (snd p) & snd p > 0 &
1.43 + gcd (fst p) (snd p) = 1"
1.44 + show ?thesis
1.45 + proof (cases "b = 0")
1.46 + case True
1.47 + thus ?thesis
1.48 + proof (simp add: normalize_def)
1.49 + show "(THE pair. ?cond (Fract a 0) pair) = (0,1)"
1.50 + proof
1.51 + show "?cond (Fract a 0) (0,1)"
1.52 + by (simp add: rat_number_collapse)
1.53 + next
1.54 + fix pair
1.55 + assume cond: "?cond (Fract a 0) pair"
1.56 + show "pair = (0,1)"
1.57 + proof (cases pair)
1.58 + case (Pair den num)
1.59 + with cond have num: "num > 0" by auto
1.60 + with Pair cond have den: "den = 0" by (simp add: eq_rat)
1.61 + show ?thesis
1.62 + proof (cases "num = 1", simp add: Pair den)
1.63 + case False
1.64 + with num have gr: "num > 1" by auto
1.65 + with den have "gcd den num = num" by auto
1.66 + with Pair cond False gr show ?thesis by auto
1.67 + qed
1.68 + qed
1.69 + qed
1.70 + qed
1.71 + next
1.72 + { fix a b :: int assume b: "b > 0"
1.73 + hence b0: "b \<noteq> 0" and "b >= 0" by auto
1.74 + let ?g = "gcd a b"
1.75 + from b0 have g0: "?g \<noteq> 0" by auto
1.76 + then have gp: "?g > 0" by simp
1.77 + then have gs: "?g <= b" by (metis b gcd_le2_int)
1.78 + from gcd_dvd1_int[of a b] obtain a' where a': "a = ?g * a'"
1.79 + unfolding dvd_def by auto
1.80 + from gcd_dvd2_int[of a b] obtain b' where b': "b = ?g * b'"
1.81 + unfolding dvd_def by auto
1.82 + hence b'2: "b' * ?g = b" by (simp add: ring_simps)
1.83 + with b0 have b'0: "b' \<noteq> 0" by auto
1.84 + from b b' zero_less_mult_iff[of ?g b'] gp have b'p: "b' > 0" by arith
1.85 + have "normalize (Fract a b) = (a div ?g, b div ?g)"
1.86 + proof (simp add: normalize_def)
1.87 + show "(THE pair. ?cond (Fract a b) pair) = (a div ?g, b div ?g)"
1.88 + proof
1.89 + have "1 = b div b" using b0 by auto
1.90 + also have "\<dots> <= b div ?g" by (rule zdiv_mono2[OF `b >= 0` gp gs])
1.91 + finally have div0: "b div ?g > 0" by simp
1.92 + show "?cond (Fract a b) (a div ?g, b div ?g)"
1.93 + by (simp add: b0 Fract_norm div_gcd_coprime_int div0)
1.94 + next
1.95 + fix pair assume cond: "?cond (Fract a b) pair"
1.96 + show "pair = (a div ?g, b div ?g)"
1.97 + proof (cases pair)
1.98 + case (Pair den num)
1.99 + with cond
1.100 + have num: "num > 0" and num0: "num \<noteq> 0" and gcd: "gcd den num = 1"
1.101 + by auto
1.102 + obtain g where g: "g = ?g" by auto
1.103 + with gp have gg0: "g > 0" by auto
1.104 + from cond Pair eq_rat(1)[OF b0 num0]
1.105 + have eq: "a * num = den * b" by auto
1.106 + hence "a' * g * num = den * g * b'"
1.107 + using a'[simplified g[symmetric]] b'[simplified g[symmetric]]
1.108 + by simp
1.109 + hence "a' * num * g = b' * den * g" by (simp add: algebra_simps)
1.110 + hence eq2: "a' * num = b' * den" using gg0 by auto
1.111 + have "a div ?g = ?g * a' div ?g" using a' by force
1.112 + hence adiv: "a div ?g = a'" using g0 by auto
1.113 + have "b div ?g = ?g * b' div ?g" using b' by force
1.114 + hence bdiv: "b div ?g = b'" using g0 by auto
1.115 + from div_gcd_coprime_int[of a b] b0
1.116 + have "gcd (a div ?g) (b div ?g) = 1" by auto
1.117 + with adiv bdiv have gcd2: "gcd a' b' = 1" by auto
1.118 + from gcd have gcd3: "gcd num den = 1"
1.119 + by (simp add: gcd_commute_int[of den num])
1.120 + from gcd2 have gcd4: "gcd b' a' = 1"
1.121 + by (simp add: gcd_commute_int[of a' b'])
1.122 + have one: "num dvd b'"
1.123 + by (rule coprime_dvd_mult_int[OF gcd3], simp add: dvd_def, rule exI[of _ a'], simp add: eq2 algebra_simps)
1.124 + have two: "b' dvd num" by (rule coprime_dvd_mult_int[OF gcd4], simp add: dvd_def, rule exI[of _ den], simp add: eq2 algebra_simps)
1.125 + from one two
1.126 + obtain k k' where k: "num = b' * k" and k': "b' = num * k'"
1.127 + unfolding dvd_def by auto
1.128 + hence "num = num * (k * k')" by (simp add: algebra_simps)
1.129 + with num0 have prod: "k * k' = 1" by auto
1.130 + from zero_less_mult_iff[of b' k] b'p num k have kp: "k > 0"
1.131 + by auto
1.132 + from prod pos_zmult_eq_1_iff[OF kp, of k'] have "k = 1" by auto
1.133 + with k have numb': "num = b'" by auto
1.134 + with eq2 b'0 have "a' = den" by auto
1.135 + with numb' adiv bdiv Pair show ?thesis by simp
1.136 + qed
1.137 + qed
1.138 + qed
1.139 + }
1.140 + note main = this
1.141 + assume "b \<noteq> 0"
1.142 + hence "b > 0 | b < 0" by arith
1.143 + thus ?thesis
1.144 + proof
1.145 + assume b: "b > 0" thus ?thesis by (simp add: Let_def main[OF b])
1.146 + next
1.147 + assume b: "b < 0"
1.148 + thus ?thesis
1.149 + by(simp add:main Let_def minus_rat_cancel[of a b, symmetric]
1.150 + zdiv_zminus2 del:minus_rat_cancel)
1.151 + qed
1.152 + qed
1.153 +qed
1.154 +
1.155 +lemma normalize_id: "normalize (Fract a b) = (p,q) \<Longrightarrow> Fract p q = Fract a b"
1.156 +by(auto simp add: normalize_code Let_def Fract_norm dvd_div_neg rat_number_collapse
1.157 + split:split_if_asm)
1.158 +
1.159 +lemma normalize_denom_pos: "normalize (Fract a b) = (p,q) \<Longrightarrow> q > 0"
1.160 +by(auto simp add: normalize_code Let_def dvd_div_neg pos_imp_zdiv_neg_iff nonneg1_imp_zdiv_pos_iff
1.161 + split:split_if_asm)
1.162 +
1.163 +lemma normalize_coprime: "normalize (Fract a b) = (p,q) \<Longrightarrow> coprime p q"
1.164 +by(auto simp add: normalize_code Let_def dvd_div_neg div_gcd_coprime_int
1.165 + split:split_if_asm)
1.166 +
1.167
1.168 subsubsection {* The field of rational numbers *}
1.169
1.170 @@ -851,22 +1011,6 @@
1.171
1.172 subsection {* Implementation of rational numbers as pairs of integers *}
1.173
1.174 -lemma Fract_norm: "Fract (a div gcd a b) (b div gcd a b) = Fract a b"
1.175 -proof (cases "a = 0 \<or> b = 0")
1.176 - case True then show ?thesis by (auto simp add: eq_rat)
1.177 -next
1.178 - let ?c = "gcd a b"
1.179 - case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
1.180 - then have "?c \<noteq> 0" by simp
1.181 - then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat)
1.182 - moreover have "Fract (a div ?c * ?c + a mod ?c) (b div ?c * ?c + b mod ?c) = Fract a b"
1.183 - by (simp add: semiring_div_class.mod_div_equality)
1.184 - moreover have "a mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
1.185 - moreover have "b mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
1.186 - ultimately show ?thesis
1.187 - by (simp add: mult_rat [symmetric])
1.188 -qed
1.189 -
1.190 definition Fract_norm :: "int \<Rightarrow> int \<Rightarrow> rat" where
1.191 [simp, code del]: "Fract_norm a b = Fract a b"
1.192