1 (* Title: HOL/Library/Fraction_Field.thy |
|
2 Author: Amine Chaieb, University of Cambridge |
|
3 *) |
|
4 |
|
5 section\<open>A formalization of the fraction field of any integral domain; |
|
6 generalization of theory Rat from int to any integral domain\<close> |
|
7 |
|
8 theory Fraction_Field |
|
9 imports Main |
|
10 begin |
|
11 |
|
12 subsection \<open>General fractions construction\<close> |
|
13 |
|
14 subsubsection \<open>Construction of the type of fractions\<close> |
|
15 |
|
16 context idom begin |
|
17 |
|
18 definition fractrel :: "'a \<times> 'a \<Rightarrow> 'a * 'a \<Rightarrow> bool" where |
|
19 "fractrel = (\<lambda>x y. snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x)" |
|
20 |
|
21 lemma fractrel_iff [simp]: |
|
22 "fractrel x y \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x" |
|
23 by (simp add: fractrel_def) |
|
24 |
|
25 lemma symp_fractrel: "symp fractrel" |
|
26 by (simp add: symp_def) |
|
27 |
|
28 lemma transp_fractrel: "transp fractrel" |
|
29 proof (rule transpI, unfold split_paired_all) |
|
30 fix a b a' b' a'' b'' :: 'a |
|
31 assume A: "fractrel (a, b) (a', b')" |
|
32 assume B: "fractrel (a', b') (a'', b'')" |
|
33 have "b' * (a * b'') = b'' * (a * b')" by (simp add: ac_simps) |
|
34 also from A have "a * b' = a' * b" by auto |
|
35 also have "b'' * (a' * b) = b * (a' * b'')" by (simp add: ac_simps) |
|
36 also from B have "a' * b'' = a'' * b'" by auto |
|
37 also have "b * (a'' * b') = b' * (a'' * b)" by (simp add: ac_simps) |
|
38 finally have "b' * (a * b'') = b' * (a'' * b)" . |
|
39 moreover from B have "b' \<noteq> 0" by auto |
|
40 ultimately have "a * b'' = a'' * b" by simp |
|
41 with A B show "fractrel (a, b) (a'', b'')" by auto |
|
42 qed |
|
43 |
|
44 lemma part_equivp_fractrel: "part_equivp fractrel" |
|
45 using _ symp_fractrel transp_fractrel |
|
46 by(rule part_equivpI)(rule exI[where x="(0, 1)"]; simp) |
|
47 |
|
48 end |
|
49 |
|
50 quotient_type (overloaded) 'a fract = "'a :: idom \<times> 'a" / partial: "fractrel" |
|
51 by(rule part_equivp_fractrel) |
|
52 |
|
53 subsubsection \<open>Representation and basic operations\<close> |
|
54 |
|
55 lift_definition Fract :: "'a :: idom \<Rightarrow> 'a \<Rightarrow> 'a fract" |
|
56 is "\<lambda>a b. if b = 0 then (0, 1) else (a, b)" |
|
57 by simp |
|
58 |
|
59 lemma Fract_cases [cases type: fract]: |
|
60 obtains (Fract) a b where "q = Fract a b" "b \<noteq> 0" |
|
61 by transfer simp |
|
62 |
|
63 lemma Fract_induct [case_names Fract, induct type: fract]: |
|
64 "(\<And>a b. b \<noteq> 0 \<Longrightarrow> P (Fract a b)) \<Longrightarrow> P q" |
|
65 by (cases q) simp |
|
66 |
|
67 lemma eq_fract: |
|
68 shows "\<And>a b c d. b \<noteq> 0 \<Longrightarrow> d \<noteq> 0 \<Longrightarrow> Fract a b = Fract c d \<longleftrightarrow> a * d = c * b" |
|
69 and "\<And>a. Fract a 0 = Fract 0 1" |
|
70 and "\<And>a c. Fract 0 a = Fract 0 c" |
|
71 by(transfer; simp)+ |
|
72 |
|
73 instantiation fract :: (idom) comm_ring_1 |
|
74 begin |
|
75 |
|
76 lift_definition zero_fract :: "'a fract" is "(0, 1)" by simp |
|
77 |
|
78 lemma Zero_fract_def: "0 = Fract 0 1" |
|
79 by transfer simp |
|
80 |
|
81 lift_definition one_fract :: "'a fract" is "(1, 1)" by simp |
|
82 |
|
83 lemma One_fract_def: "1 = Fract 1 1" |
|
84 by transfer simp |
|
85 |
|
86 lift_definition plus_fract :: "'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract" |
|
87 is "\<lambda>q r. (fst q * snd r + fst r * snd q, snd q * snd r)" |
|
88 by(auto simp add: algebra_simps) |
|
89 |
|
90 lemma add_fract [simp]: |
|
91 "\<lbrakk> b \<noteq> 0; d \<noteq> 0 \<rbrakk> \<Longrightarrow> Fract a b + Fract c d = Fract (a * d + c * b) (b * d)" |
|
92 by transfer simp |
|
93 |
|
94 lift_definition uminus_fract :: "'a fract \<Rightarrow> 'a fract" |
|
95 is "\<lambda>x. (- fst x, snd x)" |
|
96 by simp |
|
97 |
|
98 lemma minus_fract [simp]: |
|
99 fixes a b :: "'a::idom" |
|
100 shows "- Fract a b = Fract (- a) b" |
|
101 by transfer simp |
|
102 |
|
103 lemma minus_fract_cancel [simp]: "Fract (- a) (- b) = Fract a b" |
|
104 by (cases "b = 0") (simp_all add: eq_fract) |
|
105 |
|
106 definition diff_fract_def: "q - r = q + - (r::'a fract)" |
|
107 |
|
108 lemma diff_fract [simp]: |
|
109 "\<lbrakk> b \<noteq> 0; d \<noteq> 0 \<rbrakk> \<Longrightarrow> Fract a b - Fract c d = Fract (a * d - c * b) (b * d)" |
|
110 by (simp add: diff_fract_def) |
|
111 |
|
112 lift_definition times_fract :: "'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract" |
|
113 is "\<lambda>q r. (fst q * fst r, snd q * snd r)" |
|
114 by(simp add: algebra_simps) |
|
115 |
|
116 lemma mult_fract [simp]: "Fract (a::'a::idom) b * Fract c d = Fract (a * c) (b * d)" |
|
117 by transfer simp |
|
118 |
|
119 lemma mult_fract_cancel: |
|
120 "c \<noteq> 0 \<Longrightarrow> Fract (c * a) (c * b) = Fract a b" |
|
121 by transfer simp |
|
122 |
|
123 instance |
|
124 proof |
|
125 fix q r s :: "'a fract" |
|
126 show "(q * r) * s = q * (r * s)" |
|
127 by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps) |
|
128 show "q * r = r * q" |
|
129 by (cases q, cases r) (simp add: eq_fract algebra_simps) |
|
130 show "1 * q = q" |
|
131 by (cases q) (simp add: One_fract_def eq_fract) |
|
132 show "(q + r) + s = q + (r + s)" |
|
133 by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps) |
|
134 show "q + r = r + q" |
|
135 by (cases q, cases r) (simp add: eq_fract algebra_simps) |
|
136 show "0 + q = q" |
|
137 by (cases q) (simp add: Zero_fract_def eq_fract) |
|
138 show "- q + q = 0" |
|
139 by (cases q) (simp add: Zero_fract_def eq_fract) |
|
140 show "q - r = q + - r" |
|
141 by (cases q, cases r) (simp add: eq_fract) |
|
142 show "(q + r) * s = q * s + r * s" |
|
143 by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps) |
|
144 show "(0::'a fract) \<noteq> 1" |
|
145 by (simp add: Zero_fract_def One_fract_def eq_fract) |
|
146 qed |
|
147 |
|
148 end |
|
149 |
|
150 lemma of_nat_fract: "of_nat k = Fract (of_nat k) 1" |
|
151 by (induct k) (simp_all add: Zero_fract_def One_fract_def) |
|
152 |
|
153 lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k" |
|
154 by (rule of_nat_fract [symmetric]) |
|
155 |
|
156 lemma fract_collapse: |
|
157 "Fract 0 k = 0" |
|
158 "Fract 1 1 = 1" |
|
159 "Fract k 0 = 0" |
|
160 by(transfer; simp)+ |
|
161 |
|
162 lemma fract_expand: |
|
163 "0 = Fract 0 1" |
|
164 "1 = Fract 1 1" |
|
165 by (simp_all add: fract_collapse) |
|
166 |
|
167 lemma Fract_cases_nonzero: |
|
168 obtains (Fract) a b where "q = Fract a b" and "b \<noteq> 0" and "a \<noteq> 0" |
|
169 | (0) "q = 0" |
|
170 proof (cases "q = 0") |
|
171 case True |
|
172 then show thesis using 0 by auto |
|
173 next |
|
174 case False |
|
175 then obtain a b where "q = Fract a b" and "b \<noteq> 0" by (cases q) auto |
|
176 with False have "0 \<noteq> Fract a b" by simp |
|
177 with \<open>b \<noteq> 0\<close> have "a \<noteq> 0" by (simp add: Zero_fract_def eq_fract) |
|
178 with Fract \<open>q = Fract a b\<close> \<open>b \<noteq> 0\<close> show thesis by auto |
|
179 qed |
|
180 |
|
181 |
|
182 subsubsection \<open>The field of rational numbers\<close> |
|
183 |
|
184 context idom |
|
185 begin |
|
186 |
|
187 subclass ring_no_zero_divisors .. |
|
188 |
|
189 end |
|
190 |
|
191 instantiation fract :: (idom) field |
|
192 begin |
|
193 |
|
194 lift_definition inverse_fract :: "'a fract \<Rightarrow> 'a fract" |
|
195 is "\<lambda>x. if fst x = 0 then (0, 1) else (snd x, fst x)" |
|
196 by(auto simp add: algebra_simps) |
|
197 |
|
198 lemma inverse_fract [simp]: "inverse (Fract a b) = Fract (b::'a::idom) a" |
|
199 by transfer simp |
|
200 |
|
201 definition divide_fract_def: "q div r = q * inverse (r:: 'a fract)" |
|
202 |
|
203 lemma divide_fract [simp]: "Fract a b div Fract c d = Fract (a * d) (b * c)" |
|
204 by (simp add: divide_fract_def) |
|
205 |
|
206 instance |
|
207 proof |
|
208 fix q :: "'a fract" |
|
209 assume "q \<noteq> 0" |
|
210 then show "inverse q * q = 1" |
|
211 by (cases q rule: Fract_cases_nonzero) |
|
212 (simp_all add: fract_expand eq_fract mult.commute) |
|
213 next |
|
214 fix q r :: "'a fract" |
|
215 show "q div r = q * inverse r" by (simp add: divide_fract_def) |
|
216 next |
|
217 show "inverse 0 = (0:: 'a fract)" |
|
218 by (simp add: fract_expand) (simp add: fract_collapse) |
|
219 qed |
|
220 |
|
221 end |
|
222 |
|
223 |
|
224 subsubsection \<open>The ordered field of fractions over an ordered idom\<close> |
|
225 |
|
226 instantiation fract :: (linordered_idom) linorder |
|
227 begin |
|
228 |
|
229 lemma less_eq_fract_respect: |
|
230 fixes a b a' b' c d c' d' :: 'a |
|
231 assumes neq: "b \<noteq> 0" "b' \<noteq> 0" "d \<noteq> 0" "d' \<noteq> 0" |
|
232 assumes eq1: "a * b' = a' * b" |
|
233 assumes eq2: "c * d' = c' * d" |
|
234 shows "((a * d) * (b * d) \<le> (c * b) * (b * d)) \<longleftrightarrow> ((a' * d') * (b' * d') \<le> (c' * b') * (b' * d'))" |
|
235 proof - |
|
236 let ?le = "\<lambda>a b c d. ((a * d) * (b * d) \<le> (c * b) * (b * d))" |
|
237 { |
|
238 fix a b c d x :: 'a |
|
239 assume x: "x \<noteq> 0" |
|
240 have "?le a b c d = ?le (a * x) (b * x) c d" |
|
241 proof - |
|
242 from x have "0 < x * x" |
|
243 by (auto simp add: zero_less_mult_iff) |
|
244 then have "?le a b c d = |
|
245 ((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))" |
|
246 by (simp add: mult_le_cancel_right) |
|
247 also have "... = ?le (a * x) (b * x) c d" |
|
248 by (simp add: ac_simps) |
|
249 finally show ?thesis . |
|
250 qed |
|
251 } note le_factor = this |
|
252 |
|
253 let ?D = "b * d" and ?D' = "b' * d'" |
|
254 from neq have D: "?D \<noteq> 0" by simp |
|
255 from neq have "?D' \<noteq> 0" by simp |
|
256 then have "?le a b c d = ?le (a * ?D') (b * ?D') c d" |
|
257 by (rule le_factor) |
|
258 also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')" |
|
259 by (simp add: ac_simps) |
|
260 also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')" |
|
261 by (simp only: eq1 eq2) |
|
262 also have "... = ?le (a' * ?D) (b' * ?D) c' d'" |
|
263 by (simp add: ac_simps) |
|
264 also from D have "... = ?le a' b' c' d'" |
|
265 by (rule le_factor [symmetric]) |
|
266 finally show "?le a b c d = ?le a' b' c' d'" . |
|
267 qed |
|
268 |
|
269 lift_definition less_eq_fract :: "'a fract \<Rightarrow> 'a fract \<Rightarrow> bool" |
|
270 is "\<lambda>q r. (fst q * snd r) * (snd q * snd r) \<le> (fst r * snd q) * (snd q * snd r)" |
|
271 by (clarsimp simp add: less_eq_fract_respect) |
|
272 |
|
273 definition less_fract_def: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z" |
|
274 |
|
275 lemma le_fract [simp]: |
|
276 "\<lbrakk> b \<noteq> 0; d \<noteq> 0 \<rbrakk> \<Longrightarrow> Fract a b \<le> Fract c d \<longleftrightarrow> (a * d) * (b * d) \<le> (c * b) * (b * d)" |
|
277 by transfer simp |
|
278 |
|
279 lemma less_fract [simp]: |
|
280 "\<lbrakk> b \<noteq> 0; d \<noteq> 0 \<rbrakk> \<Longrightarrow> Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)" |
|
281 by (simp add: less_fract_def less_le_not_le ac_simps) |
|
282 |
|
283 instance |
|
284 proof |
|
285 fix q r s :: "'a fract" |
|
286 assume "q \<le> r" and "r \<le> s" |
|
287 then show "q \<le> s" |
|
288 proof (induct q, induct r, induct s) |
|
289 fix a b c d e f :: 'a |
|
290 assume neq: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" |
|
291 assume 1: "Fract a b \<le> Fract c d" |
|
292 assume 2: "Fract c d \<le> Fract e f" |
|
293 show "Fract a b \<le> Fract e f" |
|
294 proof - |
|
295 from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f" |
|
296 by (auto simp add: zero_less_mult_iff linorder_neq_iff) |
|
297 have "(a * d) * (b * d) * (f * f) \<le> (c * b) * (b * d) * (f * f)" |
|
298 proof - |
|
299 from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)" |
|
300 by simp |
|
301 with ff show ?thesis by (simp add: mult_le_cancel_right) |
|
302 qed |
|
303 also have "... = (c * f) * (d * f) * (b * b)" |
|
304 by (simp only: ac_simps) |
|
305 also have "... \<le> (e * d) * (d * f) * (b * b)" |
|
306 proof - |
|
307 from neq 2 have "(c * f) * (d * f) \<le> (e * d) * (d * f)" |
|
308 by simp |
|
309 with bb show ?thesis by (simp add: mult_le_cancel_right) |
|
310 qed |
|
311 finally have "(a * f) * (b * f) * (d * d) \<le> e * b * (b * f) * (d * d)" |
|
312 by (simp only: ac_simps) |
|
313 with dd have "(a * f) * (b * f) \<le> (e * b) * (b * f)" |
|
314 by (simp add: mult_le_cancel_right) |
|
315 with neq show ?thesis by simp |
|
316 qed |
|
317 qed |
|
318 next |
|
319 fix q r :: "'a fract" |
|
320 assume "q \<le> r" and "r \<le> q" |
|
321 then show "q = r" |
|
322 proof (induct q, induct r) |
|
323 fix a b c d :: 'a |
|
324 assume neq: "b \<noteq> 0" "d \<noteq> 0" |
|
325 assume 1: "Fract a b \<le> Fract c d" |
|
326 assume 2: "Fract c d \<le> Fract a b" |
|
327 show "Fract a b = Fract c d" |
|
328 proof - |
|
329 from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)" |
|
330 by simp |
|
331 also have "... \<le> (a * d) * (b * d)" |
|
332 proof - |
|
333 from neq 2 have "(c * b) * (d * b) \<le> (a * d) * (d * b)" |
|
334 by simp |
|
335 then show ?thesis by (simp only: ac_simps) |
|
336 qed |
|
337 finally have "(a * d) * (b * d) = (c * b) * (b * d)" . |
|
338 moreover from neq have "b * d \<noteq> 0" by simp |
|
339 ultimately have "a * d = c * b" by simp |
|
340 with neq show ?thesis by (simp add: eq_fract) |
|
341 qed |
|
342 qed |
|
343 next |
|
344 fix q r :: "'a fract" |
|
345 show "q \<le> q" |
|
346 by (induct q) simp |
|
347 show "(q < r) = (q \<le> r \<and> \<not> r \<le> q)" |
|
348 by (simp only: less_fract_def) |
|
349 show "q \<le> r \<or> r \<le> q" |
|
350 by (induct q, induct r) |
|
351 (simp add: mult.commute, rule linorder_linear) |
|
352 qed |
|
353 |
|
354 end |
|
355 |
|
356 instantiation fract :: (linordered_idom) linordered_field |
|
357 begin |
|
358 |
|
359 definition abs_fract_def2: |
|
360 "\<bar>q\<bar> = (if q < 0 then -q else (q::'a fract))" |
|
361 |
|
362 definition sgn_fract_def: |
|
363 "sgn (q::'a fract) = (if q = 0 then 0 else if 0 < q then 1 else - 1)" |
|
364 |
|
365 theorem abs_fract [simp]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>" |
|
366 unfolding abs_fract_def2 not_le [symmetric] |
|
367 by transfer (auto simp add: zero_less_mult_iff le_less) |
|
368 |
|
369 instance proof |
|
370 fix q r s :: "'a fract" |
|
371 assume "q \<le> r" |
|
372 then show "s + q \<le> s + r" |
|
373 proof (induct q, induct r, induct s) |
|
374 fix a b c d e f :: 'a |
|
375 assume neq: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" |
|
376 assume le: "Fract a b \<le> Fract c d" |
|
377 show "Fract e f + Fract a b \<le> Fract e f + Fract c d" |
|
378 proof - |
|
379 let ?F = "f * f" from neq have F: "0 < ?F" |
|
380 by (auto simp add: zero_less_mult_iff) |
|
381 from neq le have "(a * d) * (b * d) \<le> (c * b) * (b * d)" |
|
382 by simp |
|
383 with F have "(a * d) * (b * d) * ?F * ?F \<le> (c * b) * (b * d) * ?F * ?F" |
|
384 by (simp add: mult_le_cancel_right) |
|
385 with neq show ?thesis by (simp add: field_simps) |
|
386 qed |
|
387 qed |
|
388 next |
|
389 fix q r s :: "'a fract" |
|
390 assume "q < r" and "0 < s" |
|
391 then show "s * q < s * r" |
|
392 proof (induct q, induct r, induct s) |
|
393 fix a b c d e f :: 'a |
|
394 assume neq: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" |
|
395 assume le: "Fract a b < Fract c d" |
|
396 assume gt: "0 < Fract e f" |
|
397 show "Fract e f * Fract a b < Fract e f * Fract c d" |
|
398 proof - |
|
399 let ?E = "e * f" and ?F = "f * f" |
|
400 from neq gt have "0 < ?E" |
|
401 by (auto simp add: Zero_fract_def order_less_le eq_fract) |
|
402 moreover from neq have "0 < ?F" |
|
403 by (auto simp add: zero_less_mult_iff) |
|
404 moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)" |
|
405 by simp |
|
406 ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F" |
|
407 by (simp add: mult_less_cancel_right) |
|
408 with neq show ?thesis |
|
409 by (simp add: ac_simps) |
|
410 qed |
|
411 qed |
|
412 qed (fact sgn_fract_def abs_fract_def2)+ |
|
413 |
|
414 end |
|
415 |
|
416 instantiation fract :: (linordered_idom) distrib_lattice |
|
417 begin |
|
418 |
|
419 definition inf_fract_def: |
|
420 "(inf :: 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = min" |
|
421 |
|
422 definition sup_fract_def: |
|
423 "(sup :: 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = max" |
|
424 |
|
425 instance |
|
426 by standard (simp_all add: inf_fract_def sup_fract_def max_min_distrib2) |
|
427 |
|
428 end |
|
429 |
|
430 lemma fract_induct_pos [case_names Fract]: |
|
431 fixes P :: "'a::linordered_idom fract \<Rightarrow> bool" |
|
432 assumes step: "\<And>a b. 0 < b \<Longrightarrow> P (Fract a b)" |
|
433 shows "P q" |
|
434 proof (cases q) |
|
435 case (Fract a b) |
|
436 { |
|
437 fix a b :: 'a |
|
438 assume b: "b < 0" |
|
439 have "P (Fract a b)" |
|
440 proof - |
|
441 from b have "0 < - b" by simp |
|
442 then have "P (Fract (- a) (- b))" |
|
443 by (rule step) |
|
444 then show "P (Fract a b)" |
|
445 by (simp add: order_less_imp_not_eq [OF b]) |
|
446 qed |
|
447 } |
|
448 with Fract show "P q" |
|
449 by (auto simp add: linorder_neq_iff step) |
|
450 qed |
|
451 |
|
452 lemma zero_less_Fract_iff: "0 < b \<Longrightarrow> 0 < Fract a b \<longleftrightarrow> 0 < a" |
|
453 by (auto simp add: Zero_fract_def zero_less_mult_iff) |
|
454 |
|
455 lemma Fract_less_zero_iff: "0 < b \<Longrightarrow> Fract a b < 0 \<longleftrightarrow> a < 0" |
|
456 by (auto simp add: Zero_fract_def mult_less_0_iff) |
|
457 |
|
458 lemma zero_le_Fract_iff: "0 < b \<Longrightarrow> 0 \<le> Fract a b \<longleftrightarrow> 0 \<le> a" |
|
459 by (auto simp add: Zero_fract_def zero_le_mult_iff) |
|
460 |
|
461 lemma Fract_le_zero_iff: "0 < b \<Longrightarrow> Fract a b \<le> 0 \<longleftrightarrow> a \<le> 0" |
|
462 by (auto simp add: Zero_fract_def mult_le_0_iff) |
|
463 |
|
464 lemma one_less_Fract_iff: "0 < b \<Longrightarrow> 1 < Fract a b \<longleftrightarrow> b < a" |
|
465 by (auto simp add: One_fract_def mult_less_cancel_right_disj) |
|
466 |
|
467 lemma Fract_less_one_iff: "0 < b \<Longrightarrow> Fract a b < 1 \<longleftrightarrow> a < b" |
|
468 by (auto simp add: One_fract_def mult_less_cancel_right_disj) |
|
469 |
|
470 lemma one_le_Fract_iff: "0 < b \<Longrightarrow> 1 \<le> Fract a b \<longleftrightarrow> b \<le> a" |
|
471 by (auto simp add: One_fract_def mult_le_cancel_right) |
|
472 |
|
473 lemma Fract_le_one_iff: "0 < b \<Longrightarrow> Fract a b \<le> 1 \<longleftrightarrow> a \<le> b" |
|
474 by (auto simp add: One_fract_def mult_le_cancel_right) |
|
475 |
|
476 end |
|