src/HOL/Real/Rational.thy
 author nipkow Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) changeset 15140 322485b816ac parent 15131 c69542757a4d child 16417 9bc16273c2d4 permissions -rw-r--r--
import -> imports
```     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 imports 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
```