src/HOL/Real/Rational.thy
author nipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131 c69542757a4d
parent 15013 34264f5e4691
child 15140 322485b816ac
permissions -rw-r--r--
New theory header syntax.
     1 (*  Title: HOL/Library/Rational.thy
     2     ID:    $Id$
     3     Author: Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 header {* Rational numbers *}
     7 
     8 theory Rational
     9 import Quotient
    10 files ("rat_arith.ML")
    11 begin
    12 
    13 subsection {* Fractions *}
    14 
    15 subsubsection {* The type of fractions *}
    16 
    17 typedef fraction = "{(a, b) :: int \<times> int | a b. b \<noteq> 0}"
    18 proof
    19   show "(0, 1) \<in> ?fraction" by simp
    20 qed
    21 
    22 constdefs
    23   fract :: "int => int => fraction"
    24   "fract a b == Abs_fraction (a, b)"
    25   num :: "fraction => int"
    26   "num Q == fst (Rep_fraction Q)"
    27   den :: "fraction => int"
    28   "den Q == snd (Rep_fraction Q)"
    29 
    30 lemma fract_num [simp]: "b \<noteq> 0 ==> num (fract a b) = a"
    31   by (simp add: fract_def num_def fraction_def Abs_fraction_inverse)
    32 
    33 lemma fract_den [simp]: "b \<noteq> 0 ==> den (fract a b) = b"
    34   by (simp add: fract_def den_def fraction_def Abs_fraction_inverse)
    35 
    36 lemma fraction_cases [case_names fract, cases type: fraction]:
    37   "(!!a b. Q = fract a b ==> b \<noteq> 0 ==> C) ==> C"
    38 proof -
    39   assume r: "!!a b. Q = fract a b ==> b \<noteq> 0 ==> C"
    40   obtain a b where "Q = fract a b" and "b \<noteq> 0"
    41     by (cases Q) (auto simp add: fract_def fraction_def)
    42   thus C by (rule r)
    43 qed
    44 
    45 lemma fraction_induct [case_names fract, induct type: fraction]:
    46     "(!!a b. b \<noteq> 0 ==> P (fract a b)) ==> P Q"
    47   by (cases Q) simp
    48 
    49 
    50 subsubsection {* Equivalence of fractions *}
    51 
    52 instance fraction :: eqv ..
    53 
    54 defs (overloaded)
    55   equiv_fraction_def: "Q \<sim> R == num Q * den R = num R * den Q"
    56 
    57 lemma equiv_fraction_iff [iff]:
    58     "b \<noteq> 0 ==> b' \<noteq> 0 ==> (fract a b \<sim> fract a' b') = (a * b' = a' * b)"
    59   by (simp add: equiv_fraction_def)
    60 
    61 instance fraction :: equiv
    62 proof
    63   fix Q R S :: fraction
    64   {
    65     show "Q \<sim> Q"
    66     proof (induct Q)
    67       fix a b :: int
    68       assume "b \<noteq> 0" and "b \<noteq> 0"
    69       with refl show "fract a b \<sim> fract a b" ..
    70     qed
    71   next
    72     assume "Q \<sim> R" and "R \<sim> S"
    73     show "Q \<sim> S"
    74     proof (insert prems, induct Q, induct R, induct S)
    75       fix a b a' b' a'' b'' :: int
    76       assume b: "b \<noteq> 0" and b': "b' \<noteq> 0" and b'': "b'' \<noteq> 0"
    77       assume "fract a b \<sim> fract a' b'" hence eq1: "a * b' = a' * b" ..
    78       assume "fract a' b' \<sim> fract a'' b''" hence eq2: "a' * b'' = a'' * b'" ..
    79       have "a * b'' = a'' * b"
    80       proof cases
    81         assume "a' = 0"
    82         with b' eq1 eq2 have "a = 0 \<and> a'' = 0" by auto
    83         thus ?thesis by simp
    84       next
    85         assume a': "a' \<noteq> 0"
    86         from eq1 eq2 have "(a * b') * (a' * b'') = (a' * b) * (a'' * b')" by simp
    87         hence "(a * b'') * (a' * b') = (a'' * b) * (a' * b')" by (simp only: mult_ac)
    88         with a' b' show ?thesis by simp
    89       qed
    90       thus "fract a b \<sim> fract a'' b''" ..
    91     qed
    92   next
    93     show "Q \<sim> R ==> R \<sim> Q"
    94     proof (induct Q, induct R)
    95       fix a b a' b' :: int
    96       assume b: "b \<noteq> 0" and b': "b' \<noteq> 0"
    97       assume "fract a b \<sim> fract a' b'"
    98       hence "a * b' = a' * b" ..
    99       hence "a' * b = a * b'" ..
   100       thus "fract a' b' \<sim> fract a b" ..
   101     qed
   102   }
   103 qed
   104 
   105 lemma eq_fraction_iff [iff]:
   106     "b \<noteq> 0 ==> b' \<noteq> 0 ==> (\<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor>) = (a * b' = a' * b)"
   107   by (simp add: equiv_fraction_iff quot_equality)
   108 
   109 
   110 subsubsection {* Operations on fractions *}
   111 
   112 text {*
   113  We define the basic arithmetic operations on fractions and
   114  demonstrate their ``well-definedness'', i.e.\ congruence with respect
   115  to equivalence of fractions.
   116 *}
   117 
   118 instance fraction :: "{zero, one, plus, minus, times, inverse, ord}" ..
   119 
   120 defs (overloaded)
   121   zero_fraction_def: "0 == fract 0 1"
   122   one_fraction_def: "1 == fract 1 1"
   123   add_fraction_def: "Q + R ==
   124     fract (num Q * den R + num R * den Q) (den Q * den R)"
   125   minus_fraction_def: "-Q == fract (-(num Q)) (den Q)"
   126   mult_fraction_def: "Q * R == fract (num Q * num R) (den Q * den R)"
   127   inverse_fraction_def: "inverse Q == fract (den Q) (num Q)"
   128   le_fraction_def: "Q \<le> R ==
   129     (num Q * den R) * (den Q * den R) \<le> (num R * den Q) * (den Q * den R)"
   130 
   131 lemma is_zero_fraction_iff: "b \<noteq> 0 ==> (\<lfloor>fract a b\<rfloor> = \<lfloor>0\<rfloor>) = (a = 0)"
   132   by (simp add: zero_fraction_def eq_fraction_iff)
   133 
   134 theorem add_fraction_cong:
   135   "\<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor> ==> \<lfloor>fract c d\<rfloor> = \<lfloor>fract c' d'\<rfloor>
   136     ==> b \<noteq> 0 ==> b' \<noteq> 0 ==> d \<noteq> 0 ==> d' \<noteq> 0
   137     ==> \<lfloor>fract a b + fract c d\<rfloor> = \<lfloor>fract a' b' + fract c' d'\<rfloor>"
   138 proof -
   139   assume neq: "b \<noteq> 0"  "b' \<noteq> 0"  "d \<noteq> 0"  "d' \<noteq> 0"
   140   assume "\<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor>" hence eq1: "a * b' = a' * b" ..
   141   assume "\<lfloor>fract c d\<rfloor> = \<lfloor>fract c' d'\<rfloor>" hence eq2: "c * d' = c' * d" ..
   142   have "\<lfloor>fract (a * d + c * b) (b * d)\<rfloor> = \<lfloor>fract (a' * d' + c' * b') (b' * d')\<rfloor>"
   143   proof
   144     show "(a * d + c * b) * (b' * d') = (a' * d' + c' * b') * (b * d)"
   145       (is "?lhs = ?rhs")
   146     proof -
   147       have "?lhs = (a * b') * (d * d') + (c * d') * (b * b')"
   148         by (simp add: int_distrib mult_ac)
   149       also have "... = (a' * b) * (d * d') + (c' * d) * (b * b')"
   150         by (simp only: eq1 eq2)
   151       also have "... = ?rhs"
   152         by (simp add: int_distrib mult_ac)
   153       finally show "?lhs = ?rhs" .
   154     qed
   155     from neq show "b * d \<noteq> 0" by simp
   156     from neq show "b' * d' \<noteq> 0" by simp
   157   qed
   158   with neq show ?thesis by (simp add: add_fraction_def)
   159 qed
   160 
   161 theorem minus_fraction_cong:
   162   "\<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor> ==> b \<noteq> 0 ==> b' \<noteq> 0
   163     ==> \<lfloor>-(fract a b)\<rfloor> = \<lfloor>-(fract a' b')\<rfloor>"
   164 proof -
   165   assume neq: "b \<noteq> 0"  "b' \<noteq> 0"
   166   assume "\<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor>"
   167   hence "a * b' = a' * b" ..
   168   hence "-a * b' = -a' * b" by simp
   169   hence "\<lfloor>fract (-a) b\<rfloor> = \<lfloor>fract (-a') b'\<rfloor>" ..
   170   with neq show ?thesis by (simp add: minus_fraction_def)
   171 qed
   172 
   173 theorem mult_fraction_cong:
   174   "\<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor> ==> \<lfloor>fract c d\<rfloor> = \<lfloor>fract c' d'\<rfloor>
   175     ==> b \<noteq> 0 ==> b' \<noteq> 0 ==> d \<noteq> 0 ==> d' \<noteq> 0
   176     ==> \<lfloor>fract a b * fract c d\<rfloor> = \<lfloor>fract a' b' * fract c' d'\<rfloor>"
   177 proof -
   178   assume neq: "b \<noteq> 0"  "b' \<noteq> 0"  "d \<noteq> 0"  "d' \<noteq> 0"
   179   assume "\<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor>" hence eq1: "a * b' = a' * b" ..
   180   assume "\<lfloor>fract c d\<rfloor> = \<lfloor>fract c' d'\<rfloor>" hence eq2: "c * d' = c' * d" ..
   181   have "\<lfloor>fract (a * c) (b * d)\<rfloor> = \<lfloor>fract (a' * c') (b' * d')\<rfloor>"
   182   proof
   183     from eq1 eq2 have "(a * b') * (c * d') = (a' * b) * (c' * d)" by simp
   184     thus "(a * c) * (b' * d') = (a' * c') * (b * d)" by (simp add: mult_ac)
   185     from neq show "b * d \<noteq> 0" by simp
   186     from neq show "b' * d' \<noteq> 0" by simp
   187   qed
   188   with neq show "\<lfloor>fract a b * fract c d\<rfloor> = \<lfloor>fract a' b' * fract c' d'\<rfloor>"
   189     by (simp add: mult_fraction_def)
   190 qed
   191 
   192 theorem inverse_fraction_cong:
   193   "\<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor> ==> \<lfloor>fract a b\<rfloor> \<noteq> \<lfloor>0\<rfloor> ==> \<lfloor>fract a' b'\<rfloor> \<noteq> \<lfloor>0\<rfloor>
   194     ==> b \<noteq> 0 ==> b' \<noteq> 0
   195     ==> \<lfloor>inverse (fract a b)\<rfloor> = \<lfloor>inverse (fract a' b')\<rfloor>"
   196 proof -
   197   assume neq: "b \<noteq> 0"  "b' \<noteq> 0"
   198   assume "\<lfloor>fract a b\<rfloor> \<noteq> \<lfloor>0\<rfloor>" and "\<lfloor>fract a' b'\<rfloor> \<noteq> \<lfloor>0\<rfloor>"
   199   with neq obtain "a \<noteq> 0" and "a' \<noteq> 0" by (simp add: is_zero_fraction_iff)
   200   assume "\<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor>"
   201   hence "a * b' = a' * b" ..
   202   hence "b * a' = b' * a" by (simp only: mult_ac)
   203   hence "\<lfloor>fract b a\<rfloor> = \<lfloor>fract b' a'\<rfloor>" ..
   204   with neq show ?thesis by (simp add: inverse_fraction_def)
   205 qed
   206 
   207 theorem le_fraction_cong:
   208   "\<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor> ==> \<lfloor>fract c d\<rfloor> = \<lfloor>fract c' d'\<rfloor>
   209     ==> b \<noteq> 0 ==> b' \<noteq> 0 ==> d \<noteq> 0 ==> d' \<noteq> 0
   210     ==> (fract a b \<le> fract c d) = (fract a' b' \<le> fract c' d')"
   211 proof -
   212   assume neq: "b \<noteq> 0"  "b' \<noteq> 0"  "d \<noteq> 0"  "d' \<noteq> 0"
   213   assume "\<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor>" hence eq1: "a * b' = a' * b" ..
   214   assume "\<lfloor>fract c d\<rfloor> = \<lfloor>fract c' d'\<rfloor>" hence eq2: "c * d' = c' * d" ..
   215 
   216   let ?le = "\<lambda>a b c d. ((a * d) * (b * d) \<le> (c * b) * (b * d))"
   217   {
   218     fix a b c d x :: int assume x: "x \<noteq> 0"
   219     have "?le a b c d = ?le (a * x) (b * x) c d"
   220     proof -
   221       from x have "0 < x * x" by (auto simp add: zero_less_mult_iff)
   222       hence "?le a b c d =
   223           ((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))"
   224         by (simp add: mult_le_cancel_right)
   225       also have "... = ?le (a * x) (b * x) c d"
   226         by (simp add: mult_ac)
   227       finally show ?thesis .
   228     qed
   229   } note le_factor = this
   230 
   231   let ?D = "b * d" and ?D' = "b' * d'"
   232   from neq have D: "?D \<noteq> 0" by simp
   233   from neq have "?D' \<noteq> 0" by simp
   234   hence "?le a b c d = ?le (a * ?D') (b * ?D') c d"
   235     by (rule le_factor)
   236   also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')"
   237     by (simp add: mult_ac)
   238   also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')"
   239     by (simp only: eq1 eq2)
   240   also have "... = ?le (a' * ?D) (b' * ?D) c' d'"
   241     by (simp add: mult_ac)
   242   also from D have "... = ?le a' b' c' d'"
   243     by (rule le_factor [symmetric])
   244   finally have "?le a b c d = ?le a' b' c' d'" .
   245   with neq show ?thesis by (simp add: le_fraction_def)
   246 qed
   247 
   248 
   249 subsection {* Rational numbers *}
   250 
   251 subsubsection {* The type of rational numbers *}
   252 
   253 typedef (Rat)
   254   rat = "UNIV :: fraction quot set" ..
   255 
   256 lemma RatI [intro, simp]: "Q \<in> Rat"
   257   by (simp add: Rat_def)
   258 
   259 constdefs
   260   fraction_of :: "rat => fraction"
   261   "fraction_of q == pick (Rep_Rat q)"
   262   rat_of :: "fraction => rat"
   263   "rat_of Q == Abs_Rat \<lfloor>Q\<rfloor>"
   264 
   265 theorem rat_of_equality [iff?]: "(rat_of Q = rat_of Q') = (\<lfloor>Q\<rfloor> = \<lfloor>Q'\<rfloor>)"
   266   by (simp add: rat_of_def Abs_Rat_inject)
   267 
   268 lemma rat_of: "\<lfloor>Q\<rfloor> = \<lfloor>Q'\<rfloor> ==> rat_of Q = rat_of Q'" ..
   269 
   270 constdefs
   271   Fract :: "int => int => rat"
   272   "Fract a b == rat_of (fract a b)"
   273 
   274 theorem Fract_inverse: "\<lfloor>fraction_of (Fract a b)\<rfloor> = \<lfloor>fract a b\<rfloor>"
   275   by (simp add: fraction_of_def rat_of_def Fract_def Abs_Rat_inverse pick_inverse)
   276 
   277 theorem Fract_equality [iff?]:
   278     "(Fract a b = Fract c d) = (\<lfloor>fract a b\<rfloor> = \<lfloor>fract c d\<rfloor>)"
   279   by (simp add: Fract_def rat_of_equality)
   280 
   281 theorem eq_rat:
   282     "b \<noteq> 0 ==> d \<noteq> 0 ==> (Fract a b = Fract c d) = (a * d = c * b)"
   283   by (simp add: Fract_equality eq_fraction_iff)
   284 
   285 theorem Rat_cases [case_names Fract, cases type: rat]:
   286   "(!!a b. q = Fract a b ==> b \<noteq> 0 ==> C) ==> C"
   287 proof -
   288   assume r: "!!a b. q = Fract a b ==> b \<noteq> 0 ==> C"
   289   obtain x where "q = Abs_Rat x" by (cases q)
   290   moreover obtain Q where "x = \<lfloor>Q\<rfloor>" by (cases x)
   291   moreover obtain a b where "Q = fract a b" and "b \<noteq> 0" by (cases Q)
   292   ultimately have "q = Fract a b" by (simp only: Fract_def rat_of_def)
   293   thus ?thesis by (rule r)
   294 qed
   295 
   296 theorem Rat_induct [case_names Fract, induct type: rat]:
   297     "(!!a b. b \<noteq> 0 ==> P (Fract a b)) ==> P q"
   298   by (cases q) simp
   299 
   300 
   301 subsubsection {* Canonical function definitions *}
   302 
   303 text {*
   304   Note that the unconditional version below is much easier to read.
   305 *}
   306 
   307 theorem rat_cond_function:
   308   "(!!q r. P \<lfloor>fraction_of q\<rfloor> \<lfloor>fraction_of r\<rfloor> ==>
   309       f q r == g (fraction_of q) (fraction_of r)) ==>
   310     (!!a b a' b' c d c' d'.
   311       \<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor> ==> \<lfloor>fract c d\<rfloor> = \<lfloor>fract c' d'\<rfloor> ==>
   312       P \<lfloor>fract a b\<rfloor> \<lfloor>fract c d\<rfloor> ==> P \<lfloor>fract a' b'\<rfloor> \<lfloor>fract c' d'\<rfloor> ==>
   313       b \<noteq> 0 ==> b' \<noteq> 0 ==> d \<noteq> 0 ==> d' \<noteq> 0 ==>
   314       g (fract a b) (fract c d) = g (fract a' b') (fract c' d')) ==>
   315     P \<lfloor>fract a b\<rfloor> \<lfloor>fract c d\<rfloor> ==>
   316       f (Fract a b) (Fract c d) = g (fract a b) (fract c d)"
   317   (is "PROP ?eq ==> PROP ?cong ==> ?P ==> _")
   318 proof -
   319   assume eq: "PROP ?eq" and cong: "PROP ?cong" and P: ?P
   320   have "f (Abs_Rat \<lfloor>fract a b\<rfloor>) (Abs_Rat \<lfloor>fract c d\<rfloor>) = g (fract a b) (fract c d)"
   321   proof (rule quot_cond_function)
   322     fix X Y assume "P X Y"
   323     with eq show "f (Abs_Rat X) (Abs_Rat Y) == g (pick X) (pick Y)"
   324       by (simp add: fraction_of_def pick_inverse Abs_Rat_inverse)
   325   next
   326     fix Q Q' R R' :: fraction
   327     show "\<lfloor>Q\<rfloor> = \<lfloor>Q'\<rfloor> ==> \<lfloor>R\<rfloor> = \<lfloor>R'\<rfloor> ==>
   328         P \<lfloor>Q\<rfloor> \<lfloor>R\<rfloor> ==> P \<lfloor>Q'\<rfloor> \<lfloor>R'\<rfloor> ==> g Q R = g Q' R'"
   329       by (induct Q, induct Q', induct R, induct R') (rule cong)
   330   qed
   331   thus ?thesis by (unfold Fract_def rat_of_def)
   332 qed
   333 
   334 theorem rat_function:
   335   "(!!q r. f q r == g (fraction_of q) (fraction_of r)) ==>
   336     (!!a b a' b' c d c' d'.
   337       \<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor> ==> \<lfloor>fract c d\<rfloor> = \<lfloor>fract c' d'\<rfloor> ==>
   338       b \<noteq> 0 ==> b' \<noteq> 0 ==> d \<noteq> 0 ==> d' \<noteq> 0 ==>
   339       g (fract a b) (fract c d) = g (fract a' b') (fract c' d')) ==>
   340     f (Fract a b) (Fract c d) = g (fract a b) (fract c d)"
   341 proof -
   342   case rule_context from this TrueI
   343   show ?thesis by (rule rat_cond_function)
   344 qed
   345 
   346 
   347 subsubsection {* Standard operations on rational numbers *}
   348 
   349 instance rat :: "{zero, one, plus, minus, times, inverse, ord}" ..
   350 
   351 defs (overloaded)
   352   zero_rat_def: "0 == rat_of 0"
   353   one_rat_def: "1 == rat_of 1"
   354   add_rat_def: "q + r == rat_of (fraction_of q + fraction_of r)"
   355   minus_rat_def: "-q == rat_of (-(fraction_of q))"
   356   diff_rat_def: "q - r == q + (-(r::rat))"
   357   mult_rat_def: "q * r == rat_of (fraction_of q * fraction_of r)"
   358   inverse_rat_def: "inverse q ==
   359                     if q=0 then 0 else rat_of (inverse (fraction_of q))"
   360   divide_rat_def: "q / r == q * inverse (r::rat)"
   361   le_rat_def: "q \<le> r == fraction_of q \<le> fraction_of r"
   362   less_rat_def: "q < r == q \<le> r \<and> q \<noteq> (r::rat)"
   363   abs_rat_def: "\<bar>q\<bar> == if q < 0 then -q else (q::rat)"
   364 
   365 theorem zero_rat: "0 = Fract 0 1"
   366   by (simp add: zero_rat_def zero_fraction_def rat_of_def Fract_def)
   367 
   368 theorem one_rat: "1 = Fract 1 1"
   369   by (simp add: one_rat_def one_fraction_def rat_of_def Fract_def)
   370 
   371 theorem add_rat: "b \<noteq> 0 ==> d \<noteq> 0 ==>
   372   Fract a b + Fract c d = Fract (a * d + c * b) (b * d)"
   373 proof -
   374   have "Fract a b + Fract c d = rat_of (fract a b + fract c d)"
   375     by (rule rat_function, rule add_rat_def, rule rat_of, rule add_fraction_cong)
   376   also
   377   assume "b \<noteq> 0"  "d \<noteq> 0"
   378   hence "fract a b + fract c d = fract (a * d + c * b) (b * d)"
   379     by (simp add: add_fraction_def)
   380   finally show ?thesis by (unfold Fract_def)
   381 qed
   382 
   383 theorem minus_rat: "b \<noteq> 0 ==> -(Fract a b) = Fract (-a) b"
   384 proof -
   385   have "-(Fract a b) = rat_of (-(fract a b))"
   386     by (rule rat_function, rule minus_rat_def, rule rat_of, rule minus_fraction_cong)
   387   also assume "b \<noteq> 0" hence "-(fract a b) = fract (-a) b"
   388     by (simp add: minus_fraction_def)
   389   finally show ?thesis by (unfold Fract_def)
   390 qed
   391 
   392 theorem diff_rat: "b \<noteq> 0 ==> d \<noteq> 0 ==>
   393     Fract a b - Fract c d = Fract (a * d - c * b) (b * d)"
   394   by (simp add: diff_rat_def add_rat minus_rat)
   395 
   396 theorem mult_rat: "b \<noteq> 0 ==> d \<noteq> 0 ==>
   397   Fract a b * Fract c d = Fract (a * c) (b * d)"
   398 proof -
   399   have "Fract a b * Fract c d = rat_of (fract a b * fract c d)"
   400     by (rule rat_function, rule mult_rat_def, rule rat_of, rule mult_fraction_cong)
   401   also
   402   assume "b \<noteq> 0"  "d \<noteq> 0"
   403   hence "fract a b * fract c d = fract (a * c) (b * d)"
   404     by (simp add: mult_fraction_def)
   405   finally show ?thesis by (unfold Fract_def)
   406 qed
   407 
   408 theorem inverse_rat: "Fract a b \<noteq> 0 ==> b \<noteq> 0 ==>
   409   inverse (Fract a b) = Fract b a"
   410 proof -
   411   assume neq: "b \<noteq> 0" and nonzero: "Fract a b \<noteq> 0"
   412   hence "\<lfloor>fract a b\<rfloor> \<noteq> \<lfloor>0\<rfloor>"
   413     by (simp add: zero_rat eq_rat is_zero_fraction_iff)
   414   with _ inverse_fraction_cong [THEN rat_of]
   415   have "inverse (Fract a b) = rat_of (inverse (fract a b))"
   416   proof (rule rat_cond_function)
   417     fix q assume cond: "\<lfloor>fraction_of q\<rfloor> \<noteq> \<lfloor>0\<rfloor>"
   418     have "q \<noteq> 0"
   419     proof (cases q)
   420       fix a b assume "b \<noteq> 0" and "q = Fract a b"
   421       from this cond show ?thesis
   422         by (simp add: Fract_inverse is_zero_fraction_iff zero_rat eq_rat)
   423     qed
   424     thus "inverse q == rat_of (inverse (fraction_of q))"
   425       by (simp add: inverse_rat_def)
   426   qed
   427   also from neq nonzero have "inverse (fract a b) = fract b a"
   428     by (simp add: inverse_fraction_def)
   429   finally show ?thesis by (unfold Fract_def)
   430 qed
   431 
   432 theorem divide_rat: "Fract c d \<noteq> 0 ==> b \<noteq> 0 ==> d \<noteq> 0 ==>
   433   Fract a b / Fract c d = Fract (a * d) (b * c)"
   434 proof -
   435   assume neq: "b \<noteq> 0"  "d \<noteq> 0" and nonzero: "Fract c d \<noteq> 0"
   436   hence "c \<noteq> 0" by (simp add: zero_rat eq_rat)
   437   with neq nonzero show ?thesis
   438     by (simp add: divide_rat_def inverse_rat mult_rat)
   439 qed
   440 
   441 theorem le_rat: "b \<noteq> 0 ==> d \<noteq> 0 ==>
   442   (Fract a b \<le> Fract c d) = ((a * d) * (b * d) \<le> (c * b) * (b * d))"
   443 proof -
   444   have "(Fract a b \<le> Fract c d) = (fract a b \<le> fract c d)"
   445     by (rule rat_function, rule le_rat_def, rule le_fraction_cong)
   446   also
   447   assume "b \<noteq> 0"  "d \<noteq> 0"
   448   hence "(fract a b \<le> fract c d) = ((a * d) * (b * d) \<le> (c * b) * (b * d))"
   449     by (simp add: le_fraction_def)
   450   finally show ?thesis .
   451 qed
   452 
   453 theorem less_rat: "b \<noteq> 0 ==> d \<noteq> 0 ==>
   454     (Fract a b < Fract c d) = ((a * d) * (b * d) < (c * b) * (b * d))"
   455   by (simp add: less_rat_def le_rat eq_rat order_less_le)
   456 
   457 theorem abs_rat: "b \<noteq> 0 ==> \<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
   458   by (simp add: abs_rat_def minus_rat zero_rat less_rat eq_rat)
   459      (auto simp add: mult_less_0_iff zero_less_mult_iff order_le_less
   460                 split: abs_split)
   461 
   462 
   463 subsubsection {* The ordered field of rational numbers *}
   464 
   465 lemma rat_add_assoc: "(q + r) + s = q + (r + (s::rat))"
   466   by (induct q, induct r, induct s)
   467      (simp add: add_rat add_ac mult_ac int_distrib)
   468 
   469 lemma rat_add_0: "0 + q = (q::rat)"
   470   by (induct q) (simp add: zero_rat add_rat)
   471 
   472 lemma rat_left_minus: "(-q) + q = (0::rat)"
   473   by (induct q) (simp add: zero_rat minus_rat add_rat eq_rat)
   474 
   475 
   476 instance rat :: field
   477 proof
   478   fix q r s :: rat
   479   show "(q + r) + s = q + (r + s)"
   480     by (rule rat_add_assoc)
   481   show "q + r = r + q"
   482     by (induct q, induct r) (simp add: add_rat add_ac mult_ac)
   483   show "0 + q = q"
   484     by (induct q) (simp add: zero_rat add_rat)
   485   show "(-q) + q = 0"
   486     by (rule rat_left_minus)
   487   show "q - r = q + (-r)"
   488     by (induct q, induct r) (simp add: add_rat minus_rat diff_rat)
   489   show "(q * r) * s = q * (r * s)"
   490     by (induct q, induct r, induct s) (simp add: mult_rat mult_ac)
   491   show "q * r = r * q"
   492     by (induct q, induct r) (simp add: mult_rat mult_ac)
   493   show "1 * q = q"
   494     by (induct q) (simp add: one_rat mult_rat)
   495   show "(q + r) * s = q * s + r * s"
   496     by (induct q, induct r, induct s)
   497        (simp add: add_rat mult_rat eq_rat int_distrib)
   498   show "q \<noteq> 0 ==> inverse q * q = 1"
   499     by (induct q) (simp add: inverse_rat mult_rat one_rat zero_rat eq_rat)
   500   show "q / r = q * inverse r"
   501     by (simp add: divide_rat_def)
   502   show "0 \<noteq> (1::rat)"
   503     by (simp add: zero_rat one_rat eq_rat)
   504 qed
   505 
   506 instance rat :: linorder
   507 proof
   508   fix q r s :: rat
   509   {
   510     assume "q \<le> r" and "r \<le> s"
   511     show "q \<le> s"
   512     proof (insert prems, induct q, induct r, induct s)
   513       fix a b c d e f :: int
   514       assume neq: "b \<noteq> 0"  "d \<noteq> 0"  "f \<noteq> 0"
   515       assume 1: "Fract a b \<le> Fract c d" and 2: "Fract c d \<le> Fract e f"
   516       show "Fract a b \<le> Fract e f"
   517       proof -
   518         from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f"
   519           by (auto simp add: zero_less_mult_iff linorder_neq_iff)
   520         have "(a * d) * (b * d) * (f * f) \<le> (c * b) * (b * d) * (f * f)"
   521         proof -
   522           from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)"
   523             by (simp add: le_rat)
   524           with ff show ?thesis by (simp add: mult_le_cancel_right)
   525         qed
   526         also have "... = (c * f) * (d * f) * (b * b)"
   527           by (simp only: mult_ac)
   528         also have "... \<le> (e * d) * (d * f) * (b * b)"
   529         proof -
   530           from neq 2 have "(c * f) * (d * f) \<le> (e * d) * (d * f)"
   531             by (simp add: le_rat)
   532           with bb show ?thesis by (simp add: mult_le_cancel_right)
   533         qed
   534         finally have "(a * f) * (b * f) * (d * d) \<le> e * b * (b * f) * (d * d)"
   535           by (simp only: mult_ac)
   536         with dd have "(a * f) * (b * f) \<le> (e * b) * (b * f)"
   537           by (simp add: mult_le_cancel_right)
   538         with neq show ?thesis by (simp add: le_rat)
   539       qed
   540     qed
   541   next
   542     assume "q \<le> r" and "r \<le> q"
   543     show "q = r"
   544     proof (insert prems, induct q, induct r)
   545       fix a b c d :: int
   546       assume neq: "b \<noteq> 0"  "d \<noteq> 0"
   547       assume 1: "Fract a b \<le> Fract c d" and 2: "Fract c d \<le> Fract a b"
   548       show "Fract a b = Fract c d"
   549       proof -
   550         from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)"
   551           by (simp add: le_rat)
   552         also have "... \<le> (a * d) * (b * d)"
   553         proof -
   554           from neq 2 have "(c * b) * (d * b) \<le> (a * d) * (d * b)"
   555             by (simp add: le_rat)
   556           thus ?thesis by (simp only: mult_ac)
   557         qed
   558         finally have "(a * d) * (b * d) = (c * b) * (b * d)" .
   559         moreover from neq have "b * d \<noteq> 0" by simp
   560         ultimately have "a * d = c * b" by simp
   561         with neq show ?thesis by (simp add: eq_rat)
   562       qed
   563     qed
   564   next
   565     show "q \<le> q"
   566       by (induct q) (simp add: le_rat)
   567     show "(q < r) = (q \<le> r \<and> q \<noteq> r)"
   568       by (simp only: less_rat_def)
   569     show "q \<le> r \<or> r \<le> q"
   570       by (induct q, induct r) (simp add: le_rat mult_ac, arith)
   571   }
   572 qed
   573 
   574 instance rat :: ordered_field
   575 proof
   576   fix q r s :: rat
   577   show "q \<le> r ==> s + q \<le> s + r"
   578   proof (induct q, induct r, induct s)
   579     fix a b c d e f :: int
   580     assume neq: "b \<noteq> 0"  "d \<noteq> 0"  "f \<noteq> 0"
   581     assume le: "Fract a b \<le> Fract c d"
   582     show "Fract e f + Fract a b \<le> Fract e f + Fract c d"
   583     proof -
   584       let ?F = "f * f" from neq have F: "0 < ?F"
   585         by (auto simp add: zero_less_mult_iff)
   586       from neq le have "(a * d) * (b * d) \<le> (c * b) * (b * d)"
   587         by (simp add: le_rat)
   588       with F have "(a * d) * (b * d) * ?F * ?F \<le> (c * b) * (b * d) * ?F * ?F"
   589         by (simp add: mult_le_cancel_right)
   590       with neq show ?thesis by (simp add: add_rat le_rat mult_ac int_distrib)
   591     qed
   592   qed
   593   show "q < r ==> 0 < s ==> s * q < s * r"
   594   proof (induct q, induct r, induct s)
   595     fix a b c d e f :: int
   596     assume neq: "b \<noteq> 0"  "d \<noteq> 0"  "f \<noteq> 0"
   597     assume le: "Fract a b < Fract c d"
   598     assume gt: "0 < Fract e f"
   599     show "Fract e f * Fract a b < Fract e f * Fract c d"
   600     proof -
   601       let ?E = "e * f" and ?F = "f * f"
   602       from neq gt have "0 < ?E"
   603         by (auto simp add: zero_rat less_rat le_rat order_less_le eq_rat)
   604       moreover from neq have "0 < ?F"
   605         by (auto simp add: zero_less_mult_iff)
   606       moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)"
   607         by (simp add: less_rat)
   608       ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F"
   609         by (simp add: mult_less_cancel_right)
   610       with neq show ?thesis
   611         by (simp add: less_rat mult_rat mult_ac)
   612     qed
   613   qed
   614   show "\<bar>q\<bar> = (if q < 0 then -q else q)"
   615     by (simp only: abs_rat_def)
   616 qed
   617 
   618 instance rat :: division_by_zero
   619 proof
   620   show "inverse 0 = (0::rat)"  by (simp add: inverse_rat_def)
   621 qed
   622 
   623 
   624 subsection {* Various Other Results *}
   625 
   626 lemma minus_rat_cancel [simp]: "b \<noteq> 0 ==> Fract (-a) (-b) = Fract a b"
   627 by (simp add: Fract_equality eq_fraction_iff)
   628 
   629 theorem Rat_induct_pos [case_names Fract, induct type: rat]:
   630   assumes step: "!!a b. 0 < b ==> P (Fract a b)"
   631     shows "P q"
   632 proof (cases q)
   633   have step': "!!a b. b < 0 ==> P (Fract a b)"
   634   proof -
   635     fix a::int and b::int
   636     assume b: "b < 0"
   637     hence "0 < -b" by simp
   638     hence "P (Fract (-a) (-b))" by (rule step)
   639     thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b])
   640   qed
   641   case (Fract a b)
   642   thus "P q" by (force simp add: linorder_neq_iff step step')
   643 qed
   644 
   645 lemma zero_less_Fract_iff:
   646      "0 < b ==> (0 < Fract a b) = (0 < a)"
   647 by (simp add: zero_rat less_rat order_less_imp_not_eq2 zero_less_mult_iff)
   648 
   649 lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1"
   650 apply (insert add_rat [of concl: m n 1 1])
   651 apply (simp add: one_rat  [symmetric])
   652 done
   653 
   654 lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k"
   655 apply (induct k)
   656 apply (simp add: zero_rat)
   657 apply (simp add: Fract_add_one)
   658 done
   659 
   660 lemma Fract_of_int_eq: "Fract k 1 = of_int k"
   661 proof (cases k rule: int_cases)
   662   case (nonneg n)
   663     thus ?thesis by (simp add: int_eq_of_nat Fract_of_nat_eq)
   664 next
   665   case (neg n)
   666     hence "Fract k 1 = - (Fract (of_nat (Suc n)) 1)"
   667       by (simp only: minus_rat int_eq_of_nat)
   668     also have "... =  - (of_nat (Suc n))"
   669       by (simp only: Fract_of_nat_eq)
   670     finally show ?thesis
   671       by (simp add: only: prems int_eq_of_nat of_int_minus of_int_of_nat_eq)
   672 qed
   673 
   674 
   675 subsection {* Numerals and Arithmetic *}
   676 
   677 instance rat :: number ..
   678 
   679 defs (overloaded)
   680   rat_number_of_def: "(number_of w :: rat) == of_int (Rep_Bin w)"
   681     --{*the type constraint is essential!*}
   682 
   683 instance rat :: number_ring
   684 by (intro_classes, simp add: rat_number_of_def) 
   685 
   686 declare diff_rat_def [symmetric]
   687 
   688 use "rat_arith.ML"
   689 
   690 setup rat_arith_setup
   691 
   692 end