161 lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel] |
161 lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel] |
162 |
162 |
163 |
163 |
164 subsubsection {* Standard operations on rational numbers *} |
164 subsubsection {* Standard operations on rational numbers *} |
165 |
165 |
166 instance rat :: zero |
166 instantiation rat :: "{zero, one, plus, minus, times, inverse, ord, abs, sgn}" |
167 Zero_rat_def: "0 == Fract 0 1" .. |
167 begin |
168 lemmas [code func del] = Zero_rat_def |
168 |
169 |
169 definition |
170 instance rat :: one |
170 Zero_rat_def [code func del]: "0 = Fract 0 1" |
171 One_rat_def: "1 == Fract 1 1" .. |
171 |
172 lemmas [code func del] = One_rat_def |
172 definition |
173 |
173 One_rat_def [code func del]: "1 = Fract 1 1" |
174 instance rat :: plus |
174 |
175 add_rat_def: |
175 definition |
176 "q + r == |
176 add_rat_def [code func del]: |
|
177 "q + r = |
177 Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. |
178 Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. |
178 ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)})" .. |
179 ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)})" |
179 lemmas [code func del] = add_rat_def |
180 |
180 |
181 definition |
181 instance rat :: minus |
182 minus_rat_def [code func del]: |
182 minus_rat_def: |
183 "- q = Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel``{(- fst x, snd x)})" |
183 "- q == Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel``{(- fst x, snd x)})" |
184 |
184 diff_rat_def: "q - r == q + - (r::rat)" .. |
185 definition |
185 lemmas [code func del] = minus_rat_def diff_rat_def |
186 diff_rat_def [code func del]: "q - r = q + - (r::rat)" |
186 |
187 |
187 instance rat :: times |
188 definition |
188 mult_rat_def: |
189 mult_rat_def [code func del]: |
189 "q * r == |
190 "q * r = |
190 Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. |
191 Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. |
191 ratrel``{(fst x * fst y, snd x * snd y)})" .. |
192 ratrel``{(fst x * fst y, snd x * snd y)})" |
192 lemmas [code func del] = mult_rat_def |
193 |
193 |
194 definition |
194 instance rat :: inverse |
195 inverse_rat_def [code func del]: |
195 inverse_rat_def: |
196 "inverse q = |
196 "inverse q == |
|
197 Abs_Rat (\<Union>x \<in> Rep_Rat q. |
197 Abs_Rat (\<Union>x \<in> Rep_Rat q. |
198 ratrel``{if fst x=0 then (0,1) else (snd x, fst x)})" |
198 ratrel``{if fst x=0 then (0,1) else (snd x, fst x)})" |
199 divide_rat_def: "q / r == q * inverse (r::rat)" .. |
199 |
200 lemmas [code func del] = inverse_rat_def divide_rat_def |
200 definition |
201 |
201 divide_rat_def [code func del]: "q / r = q * inverse (r::rat)" |
202 instance rat :: ord |
202 |
203 le_rat_def: |
203 definition |
204 "q \<le> r == contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. |
204 le_rat_def [code func del]: |
|
205 "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r. |
205 {(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})" |
206 {(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})" |
206 less_rat_def: "(z < (w::rat)) == (z \<le> w & z \<noteq> w)" .. |
207 |
207 lemmas [code func del] = le_rat_def less_rat_def |
208 definition |
208 |
209 less_rat_def [code func del]: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w" |
209 instance rat :: abs |
210 |
210 abs_rat_def: "\<bar>q\<bar> == if q < 0 then -q else (q::rat)" .. |
211 definition |
211 |
212 abs_rat_def: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))" |
212 instance rat :: sgn |
213 |
213 sgn_rat_def: "sgn(q::rat) == (if q=0 then 0 else if 0<q then 1 else - 1)" .. |
214 definition |
214 |
215 sgn_rat_def: "sgn (q::rat) = (if q=0 then 0 else if 0<q then 1 else - 1)" |
215 instance rat :: power .. |
216 |
216 |
217 instance .. |
217 primrec (rat) |
218 |
218 rat_power_0: "q ^ 0 = 1" |
219 end |
219 rat_power_Suc: "q ^ (Suc n) = (q::rat) * (q ^ n)" |
220 |
|
221 instantiation rat :: power |
|
222 begin |
|
223 |
|
224 primrec power_rat |
|
225 where |
|
226 rat_power_0: "q ^ 0 = (1\<Colon>rat)" |
|
227 | rat_power_Suc: "q ^ (Suc n) = (q\<Colon>rat) * (q ^ n)" |
|
228 |
|
229 instance .. |
|
230 |
|
231 end |
220 |
232 |
221 theorem eq_rat: "b \<noteq> 0 ==> d \<noteq> 0 ==> |
233 theorem eq_rat: "b \<noteq> 0 ==> d \<noteq> 0 ==> |
222 (Fract a b = Fract c d) = (a * d = c * b)" |
234 (Fract a b = Fract c d) = (a * d = c * b)" |
223 by (simp add: Fract_def) |
235 by (simp add: Fract_def) |
224 |
236 |
359 by (induct q, induct r) |
371 by (induct q, induct r) |
360 (simp add: le_rat mult_commute, rule linorder_linear) |
372 (simp add: le_rat mult_commute, rule linorder_linear) |
361 } |
373 } |
362 qed |
374 qed |
363 |
375 |
364 instance rat :: distrib_lattice |
376 instantiation rat :: distrib_lattice |
365 "inf \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat \<equiv> min" |
377 begin |
366 "sup \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat \<equiv> max" |
378 |
|
379 definition |
|
380 "(inf \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat) = min" |
|
381 |
|
382 definition |
|
383 "(sup \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat) = max" |
|
384 |
|
385 instance |
367 by default (auto simp add: min_max.sup_inf_distrib1 inf_rat_def sup_rat_def) |
386 by default (auto simp add: min_max.sup_inf_distrib1 inf_rat_def sup_rat_def) |
|
387 |
|
388 end |
368 |
389 |
369 instance rat :: ordered_field |
390 instance rat :: ordered_field |
370 proof |
391 proof |
371 fix q r s :: rat |
392 fix q r s :: rat |
372 show "q \<le> r ==> s + q \<le> s + r" |
393 show "q \<le> r ==> s + q \<le> s + r" |
472 by (auto simp add: Fract_zero Fract_of_int_eq [symmetric] divide_rat) |
493 by (auto simp add: Fract_zero Fract_of_int_eq [symmetric] divide_rat) |
473 |
494 |
474 |
495 |
475 subsection {* Numerals and Arithmetic *} |
496 subsection {* Numerals and Arithmetic *} |
476 |
497 |
477 instance rat :: number |
498 instantiation rat :: number_ring |
478 rat_number_of_def: "(number_of w :: rat) \<equiv> of_int w" .. |
499 begin |
479 |
500 |
480 instance rat :: number_ring |
501 definition |
481 by default (simp add: rat_number_of_def) |
502 rat_number_of_def: "number_of w = (of_int w \<Colon> rat)" |
|
503 |
|
504 instance |
|
505 by default (simp add: rat_number_of_def) |
|
506 |
|
507 end |
482 |
508 |
483 use "rat_arith.ML" |
509 use "rat_arith.ML" |
484 declaration {* K rat_arith_setup *} |
510 declaration {* K rat_arith_setup *} |
485 |
511 |
486 |
512 |
487 subsection {* Embedding from Rationals to other Fields *} |
513 subsection {* Embedding from Rationals to other Fields *} |
488 |
514 |
489 class field_char_0 = field + ring_char_0 |
515 class field_char_0 = field + ring_char_0 |
490 |
516 |
491 instance ordered_field < field_char_0 .. |
517 instance ordered_field < field_char_0 .. |
492 |
518 |
493 definition |
519 definition |
494 of_rat :: "rat \<Rightarrow> 'a::field_char_0" |
520 of_rat :: "rat \<Rightarrow> 'a::field_char_0" |
495 where |
521 where |
496 [code func del]: "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})" |
522 [code func del]: "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})" |