renamed theory Rational to Rat
authorhaftmann
Wed Feb 24 14:34:40 2010 +0100 (2010-02-24)
changeset 35372ca158c7b1144
parent 35371 6c92eb394e3c
child 35373 f759782e35ac
renamed theory Rational to Rat
NEWS
src/HOL/IsaMakefile
src/HOL/Library/Binomial.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Nitpick_Examples/Typedef_Nits.thy
src/HOL/PReal.thy
src/HOL/Rat.thy
src/HOL/Rational.thy
src/HOL/ex/NormalForm.thy
     1.1 --- a/NEWS	Wed Feb 24 14:19:54 2010 +0100
     1.2 +++ b/NEWS	Wed Feb 24 14:34:40 2010 +0100
     1.3 @@ -52,6 +52,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc.
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10  * New set of rules "ac_simps" provides combined assoc / commute rewrites
    1.11  for all interpretations of the appropriate generic locales.
    1.12  
     2.1 --- a/src/HOL/IsaMakefile	Wed Feb 24 14:19:54 2010 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Wed Feb 24 14:34:40 2010 +0100
     2.3 @@ -352,7 +352,7 @@
     2.4    PReal.thy \
     2.5    Parity.thy \
     2.6    RComplete.thy \
     2.7 -  Rational.thy \
     2.8 +  Rat.thy \
     2.9    Real.thy \
    2.10    RealDef.thy \
    2.11    RealPow.thy \
     3.1 --- a/src/HOL/Library/Binomial.thy	Wed Feb 24 14:19:54 2010 +0100
     3.2 +++ b/src/HOL/Library/Binomial.thy	Wed Feb 24 14:34:40 2010 +0100
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      HOL/Binomial.thy
     3.5 +(*  Title:      HOL/Library/Binomial.thy
     3.6      Author:     Lawrence C Paulson, Amine Chaieb
     3.7      Copyright   1997  University of Cambridge
     3.8  *)
     3.9 @@ -6,7 +6,7 @@
    3.10  header {* Binomial Coefficients *}
    3.11  
    3.12  theory Binomial
    3.13 -imports Fact SetInterval Presburger Main Rational
    3.14 +imports Complex_Main
    3.15  begin
    3.16  
    3.17  text {* This development is based on the work of Andy Gordon and
     4.1 --- a/src/HOL/Library/Fraction_Field.thy	Wed Feb 24 14:19:54 2010 +0100
     4.2 +++ b/src/HOL/Library/Fraction_Field.thy	Wed Feb 24 14:34:40 2010 +0100
     4.3 @@ -1,12 +1,12 @@
     4.4 -(*  Title:      Fraction_Field.thy
     4.5 +(*  Title:      HOL/Library/Fraction_Field.thy
     4.6      Author:     Amine Chaieb, University of Cambridge
     4.7  *)
     4.8  
     4.9  header{* A formalization of the fraction field of any integral domain 
    4.10 -         A generalization of Rational.thy from int to any integral domain *}
    4.11 +         A generalization of Rat.thy from int to any integral domain *}
    4.12  
    4.13  theory Fraction_Field
    4.14 -imports Main (* Equiv_Relations Plain *)
    4.15 +imports Main
    4.16  begin
    4.17  
    4.18  subsection {* General fractions construction *}
     5.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Wed Feb 24 14:19:54 2010 +0100
     5.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Wed Feb 24 14:34:40 2010 +0100
     5.3 @@ -8,7 +8,7 @@
     5.4  header {* Examples Featuring Nitpick Applied to Typedefs *}
     5.5  
     5.6  theory Typedef_Nits
     5.7 -imports Main Rational
     5.8 +imports Complex_Main
     5.9  begin
    5.10  
    5.11  nitpick_params [card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1,
     6.1 --- a/src/HOL/PReal.thy	Wed Feb 24 14:19:54 2010 +0100
     6.2 +++ b/src/HOL/PReal.thy	Wed Feb 24 14:34:40 2010 +0100
     6.3 @@ -9,7 +9,7 @@
     6.4  header {* Positive real numbers *}
     6.5  
     6.6  theory PReal
     6.7 -imports Rational 
     6.8 +imports Rat
     6.9  begin
    6.10  
    6.11  text{*Could be generalized and moved to @{text Groups}*}
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Rat.thy	Wed Feb 24 14:34:40 2010 +0100
     7.3 @@ -0,0 +1,1194 @@
     7.4 +(*  Title:  HOL/Rat.thy
     7.5 +    Author: Markus Wenzel, TU Muenchen
     7.6 +*)
     7.7 +
     7.8 +header {* Rational numbers *}
     7.9 +
    7.10 +theory Rat
    7.11 +imports GCD Archimedean_Field
    7.12 +begin
    7.13 +
    7.14 +subsection {* Rational numbers as quotient *}
    7.15 +
    7.16 +subsubsection {* Construction of the type of rational numbers *}
    7.17 +
    7.18 +definition
    7.19 +  ratrel :: "((int \<times> int) \<times> (int \<times> int)) set" where
    7.20 +  "ratrel = {(x, y). snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x}"
    7.21 +
    7.22 +lemma ratrel_iff [simp]:
    7.23 +  "(x, y) \<in> ratrel \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x"
    7.24 +  by (simp add: ratrel_def)
    7.25 +
    7.26 +lemma refl_on_ratrel: "refl_on {x. snd x \<noteq> 0} ratrel"
    7.27 +  by (auto simp add: refl_on_def ratrel_def)
    7.28 +
    7.29 +lemma sym_ratrel: "sym ratrel"
    7.30 +  by (simp add: ratrel_def sym_def)
    7.31 +
    7.32 +lemma trans_ratrel: "trans ratrel"
    7.33 +proof (rule transI, unfold split_paired_all)
    7.34 +  fix a b a' b' a'' b'' :: int
    7.35 +  assume A: "((a, b), (a', b')) \<in> ratrel"
    7.36 +  assume B: "((a', b'), (a'', b'')) \<in> ratrel"
    7.37 +  have "b' * (a * b'') = b'' * (a * b')" by simp
    7.38 +  also from A have "a * b' = a' * b" by auto
    7.39 +  also have "b'' * (a' * b) = b * (a' * b'')" by simp
    7.40 +  also from B have "a' * b'' = a'' * b'" by auto
    7.41 +  also have "b * (a'' * b') = b' * (a'' * b)" by simp
    7.42 +  finally have "b' * (a * b'') = b' * (a'' * b)" .
    7.43 +  moreover from B have "b' \<noteq> 0" by auto
    7.44 +  ultimately have "a * b'' = a'' * b" by simp
    7.45 +  with A B show "((a, b), (a'', b'')) \<in> ratrel" by auto
    7.46 +qed
    7.47 +  
    7.48 +lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel"
    7.49 +  by (rule equiv.intro [OF refl_on_ratrel sym_ratrel trans_ratrel])
    7.50 +
    7.51 +lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel]
    7.52 +lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel]
    7.53 +
    7.54 +lemma equiv_ratrel_iff [iff]: 
    7.55 +  assumes "snd x \<noteq> 0" and "snd y \<noteq> 0"
    7.56 +  shows "ratrel `` {x} = ratrel `` {y} \<longleftrightarrow> (x, y) \<in> ratrel"
    7.57 +  by (rule eq_equiv_class_iff, rule equiv_ratrel) (auto simp add: assms)
    7.58 +
    7.59 +typedef (Rat) rat = "{x. snd x \<noteq> 0} // ratrel"
    7.60 +proof
    7.61 +  have "(0::int, 1::int) \<in> {x. snd x \<noteq> 0}" by simp
    7.62 +  then show "ratrel `` {(0, 1)} \<in> {x. snd x \<noteq> 0} // ratrel" by (rule quotientI)
    7.63 +qed
    7.64 +
    7.65 +lemma ratrel_in_Rat [simp]: "snd x \<noteq> 0 \<Longrightarrow> ratrel `` {x} \<in> Rat"
    7.66 +  by (simp add: Rat_def quotientI)
    7.67 +
    7.68 +declare Abs_Rat_inject [simp] Abs_Rat_inverse [simp]
    7.69 +
    7.70 +
    7.71 +subsubsection {* Representation and basic operations *}
    7.72 +
    7.73 +definition
    7.74 +  Fract :: "int \<Rightarrow> int \<Rightarrow> rat" where
    7.75 +  "Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})"
    7.76 +
    7.77 +lemma eq_rat:
    7.78 +  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"
    7.79 +  and "\<And>a. Fract a 0 = Fract 0 1"
    7.80 +  and "\<And>a c. Fract 0 a = Fract 0 c"
    7.81 +  by (simp_all add: Fract_def)
    7.82 +
    7.83 +lemma Rat_cases [case_names Fract, cases type: rat]:
    7.84 +  assumes "\<And>a b. q = Fract a b \<Longrightarrow> b > 0 \<Longrightarrow> coprime a b \<Longrightarrow> C"
    7.85 +  shows C
    7.86 +proof -
    7.87 +  obtain a b :: int where "q = Fract a b" and "b \<noteq> 0"
    7.88 +    by (cases q) (clarsimp simp add: Fract_def Rat_def quotient_def)
    7.89 +  let ?a = "a div gcd a b"
    7.90 +  let ?b = "b div gcd a b"
    7.91 +  from `b \<noteq> 0` have "?b * gcd a b = b"
    7.92 +    by (simp add: dvd_div_mult_self)
    7.93 +  with `b \<noteq> 0` have "?b \<noteq> 0" by auto
    7.94 +  from `q = Fract a b` `b \<noteq> 0` `?b \<noteq> 0` have q: "q = Fract ?a ?b"
    7.95 +    by (simp add: eq_rat dvd_div_mult mult_commute [of a])
    7.96 +  from `b \<noteq> 0` have coprime: "coprime ?a ?b"
    7.97 +    by (auto intro: div_gcd_coprime_int)
    7.98 +  show C proof (cases "b > 0")
    7.99 +    case True
   7.100 +    note assms
   7.101 +    moreover note q
   7.102 +    moreover from True have "?b > 0" by (simp add: nonneg1_imp_zdiv_pos_iff)
   7.103 +    moreover note coprime
   7.104 +    ultimately show C .
   7.105 +  next
   7.106 +    case False
   7.107 +    note assms
   7.108 +    moreover from q have "q = Fract (- ?a) (- ?b)" by (simp add: Fract_def)
   7.109 +    moreover from False `b \<noteq> 0` have "- ?b > 0" by (simp add: pos_imp_zdiv_neg_iff)
   7.110 +    moreover from coprime have "coprime (- ?a) (- ?b)" by simp
   7.111 +    ultimately show C .
   7.112 +  qed
   7.113 +qed
   7.114 +
   7.115 +lemma Rat_induct [case_names Fract, induct type: rat]:
   7.116 +  assumes "\<And>a b. b > 0 \<Longrightarrow> coprime a b \<Longrightarrow> P (Fract a b)"
   7.117 +  shows "P q"
   7.118 +  using assms by (cases q) simp
   7.119 +
   7.120 +instantiation rat :: comm_ring_1
   7.121 +begin
   7.122 +
   7.123 +definition
   7.124 +  Zero_rat_def: "0 = Fract 0 1"
   7.125 +
   7.126 +definition
   7.127 +  One_rat_def: "1 = Fract 1 1"
   7.128 +
   7.129 +definition
   7.130 +  add_rat_def:
   7.131 +  "q + r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
   7.132 +    ratrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})"
   7.133 +
   7.134 +lemma add_rat [simp]:
   7.135 +  assumes "b \<noteq> 0" and "d \<noteq> 0"
   7.136 +  shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)"
   7.137 +proof -
   7.138 +  have "(\<lambda>x y. ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)})
   7.139 +    respects2 ratrel"
   7.140 +  by (rule equiv_ratrel [THEN congruent2_commuteI]) (simp_all add: left_distrib)
   7.141 +  with assms show ?thesis by (simp add: Fract_def add_rat_def UN_ratrel2)
   7.142 +qed
   7.143 +
   7.144 +definition
   7.145 +  minus_rat_def:
   7.146 +  "- q = Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel `` {(- fst x, snd x)})"
   7.147 +
   7.148 +lemma minus_rat [simp]: "- Fract a b = Fract (- a) b"
   7.149 +proof -
   7.150 +  have "(\<lambda>x. ratrel `` {(- fst x, snd x)}) respects ratrel"
   7.151 +    by (simp add: congruent_def)
   7.152 +  then show ?thesis by (simp add: Fract_def minus_rat_def UN_ratrel)
   7.153 +qed
   7.154 +
   7.155 +lemma minus_rat_cancel [simp]: "Fract (- a) (- b) = Fract a b"
   7.156 +  by (cases "b = 0") (simp_all add: eq_rat)
   7.157 +
   7.158 +definition
   7.159 +  diff_rat_def: "q - r = q + - (r::rat)"
   7.160 +
   7.161 +lemma diff_rat [simp]:
   7.162 +  assumes "b \<noteq> 0" and "d \<noteq> 0"
   7.163 +  shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)"
   7.164 +  using assms by (simp add: diff_rat_def)
   7.165 +
   7.166 +definition
   7.167 +  mult_rat_def:
   7.168 +  "q * r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
   7.169 +    ratrel``{(fst x * fst y, snd x * snd y)})"
   7.170 +
   7.171 +lemma mult_rat [simp]: "Fract a b * Fract c d = Fract (a * c) (b * d)"
   7.172 +proof -
   7.173 +  have "(\<lambda>x y. ratrel `` {(fst x * fst y, snd x * snd y)}) respects2 ratrel"
   7.174 +    by (rule equiv_ratrel [THEN congruent2_commuteI]) simp_all
   7.175 +  then show ?thesis by (simp add: Fract_def mult_rat_def UN_ratrel2)
   7.176 +qed
   7.177 +
   7.178 +lemma mult_rat_cancel:
   7.179 +  assumes "c \<noteq> 0"
   7.180 +  shows "Fract (c * a) (c * b) = Fract a b"
   7.181 +proof -
   7.182 +  from assms have "Fract c c = Fract 1 1" by (simp add: Fract_def)
   7.183 +  then show ?thesis by (simp add: mult_rat [symmetric])
   7.184 +qed
   7.185 +
   7.186 +instance proof
   7.187 +  fix q r s :: rat show "(q * r) * s = q * (r * s)" 
   7.188 +    by (cases q, cases r, cases s) (simp add: eq_rat)
   7.189 +next
   7.190 +  fix q r :: rat show "q * r = r * q"
   7.191 +    by (cases q, cases r) (simp add: eq_rat)
   7.192 +next
   7.193 +  fix q :: rat show "1 * q = q"
   7.194 +    by (cases q) (simp add: One_rat_def eq_rat)
   7.195 +next
   7.196 +  fix q r s :: rat show "(q + r) + s = q + (r + s)"
   7.197 +    by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps)
   7.198 +next
   7.199 +  fix q r :: rat show "q + r = r + q"
   7.200 +    by (cases q, cases r) (simp add: eq_rat)
   7.201 +next
   7.202 +  fix q :: rat show "0 + q = q"
   7.203 +    by (cases q) (simp add: Zero_rat_def eq_rat)
   7.204 +next
   7.205 +  fix q :: rat show "- q + q = 0"
   7.206 +    by (cases q) (simp add: Zero_rat_def eq_rat)
   7.207 +next
   7.208 +  fix q r :: rat show "q - r = q + - r"
   7.209 +    by (cases q, cases r) (simp add: eq_rat)
   7.210 +next
   7.211 +  fix q r s :: rat show "(q + r) * s = q * s + r * s"
   7.212 +    by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps)
   7.213 +next
   7.214 +  show "(0::rat) \<noteq> 1" by (simp add: Zero_rat_def One_rat_def eq_rat)
   7.215 +qed
   7.216 +
   7.217 +end
   7.218 +
   7.219 +lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1"
   7.220 +  by (induct k) (simp_all add: Zero_rat_def One_rat_def)
   7.221 +
   7.222 +lemma of_int_rat: "of_int k = Fract k 1"
   7.223 +  by (cases k rule: int_diff_cases) (simp add: of_nat_rat)
   7.224 +
   7.225 +lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k"
   7.226 +  by (rule of_nat_rat [symmetric])
   7.227 +
   7.228 +lemma Fract_of_int_eq: "Fract k 1 = of_int k"
   7.229 +  by (rule of_int_rat [symmetric])
   7.230 +
   7.231 +instantiation rat :: number_ring
   7.232 +begin
   7.233 +
   7.234 +definition
   7.235 +  rat_number_of_def: "number_of w = Fract w 1"
   7.236 +
   7.237 +instance proof
   7.238 +qed (simp add: rat_number_of_def of_int_rat)
   7.239 +
   7.240 +end
   7.241 +
   7.242 +lemma rat_number_collapse:
   7.243 +  "Fract 0 k = 0"
   7.244 +  "Fract 1 1 = 1"
   7.245 +  "Fract (number_of k) 1 = number_of k"
   7.246 +  "Fract k 0 = 0"
   7.247 +  by (cases "k = 0")
   7.248 +    (simp_all add: Zero_rat_def One_rat_def number_of_is_id number_of_eq of_int_rat eq_rat Fract_def)
   7.249 +
   7.250 +lemma rat_number_expand [code_unfold]:
   7.251 +  "0 = Fract 0 1"
   7.252 +  "1 = Fract 1 1"
   7.253 +  "number_of k = Fract (number_of k) 1"
   7.254 +  by (simp_all add: rat_number_collapse)
   7.255 +
   7.256 +lemma iszero_rat [simp]:
   7.257 +  "iszero (number_of k :: rat) \<longleftrightarrow> iszero (number_of k :: int)"
   7.258 +  by (simp add: iszero_def rat_number_expand number_of_is_id eq_rat)
   7.259 +
   7.260 +lemma Rat_cases_nonzero [case_names Fract 0]:
   7.261 +  assumes Fract: "\<And>a b. q = Fract a b \<Longrightarrow> b > 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> C"
   7.262 +  assumes 0: "q = 0 \<Longrightarrow> C"
   7.263 +  shows C
   7.264 +proof (cases "q = 0")
   7.265 +  case True then show C using 0 by auto
   7.266 +next
   7.267 +  case False
   7.268 +  then obtain a b where "q = Fract a b" and "b > 0" and "coprime a b" by (cases q) auto
   7.269 +  moreover with False have "0 \<noteq> Fract a b" by simp
   7.270 +  with `b > 0` have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat)
   7.271 +  with Fract `q = Fract a b` `b > 0` `coprime a b` show C by blast
   7.272 +qed
   7.273 +
   7.274 +subsubsection {* Function @{text normalize} *}
   7.275 +
   7.276 +lemma Fract_coprime: "Fract (a div gcd a b) (b div gcd a b) = Fract a b"
   7.277 +proof (cases "b = 0")
   7.278 +  case True then show ?thesis by (simp add: eq_rat)
   7.279 +next
   7.280 +  case False
   7.281 +  moreover have "b div gcd a b * gcd a b = b"
   7.282 +    by (rule dvd_div_mult_self) simp
   7.283 +  ultimately have "b div gcd a b \<noteq> 0" by auto
   7.284 +  with False show ?thesis by (simp add: eq_rat dvd_div_mult mult_commute [of a])
   7.285 +qed
   7.286 +
   7.287 +definition normalize :: "int \<times> int \<Rightarrow> int \<times> int" where
   7.288 +  "normalize p = (if snd p > 0 then (let a = gcd (fst p) (snd p) in (fst p div a, snd p div a))
   7.289 +    else if snd p = 0 then (0, 1)
   7.290 +    else (let a = - gcd (fst p) (snd p) in (fst p div a, snd p div a)))"
   7.291 +
   7.292 +lemma normalize_crossproduct:
   7.293 +  assumes "q \<noteq> 0" "s \<noteq> 0"
   7.294 +  assumes "normalize (p, q) = normalize (r, s)"
   7.295 +  shows "p * s = r * q"
   7.296 +proof -
   7.297 +  have aux: "p * gcd r s = sgn (q * s) * r * gcd p q \<Longrightarrow> q * gcd r s = sgn (q * s) * s * gcd p q \<Longrightarrow> p * s = q * r"
   7.298 +  proof -
   7.299 +    assume "p * gcd r s = sgn (q * s) * r * gcd p q" and "q * gcd r s = sgn (q * s) * s * gcd p q"
   7.300 +    then have "(p * gcd r s) * (sgn (q * s) * s * gcd p q) = (q * gcd r s) * (sgn (q * s) * r * gcd p q)" by simp
   7.301 +    with assms show "p * s = q * r" by (auto simp add: mult_ac sgn_times sgn_0_0)
   7.302 +  qed
   7.303 +  from assms show ?thesis
   7.304 +    by (auto simp add: normalize_def Let_def dvd_div_div_eq_mult mult_commute sgn_times split: if_splits intro: aux)
   7.305 +qed
   7.306 +
   7.307 +lemma normalize_eq: "normalize (a, b) = (p, q) \<Longrightarrow> Fract p q = Fract a b"
   7.308 +  by (auto simp add: normalize_def Let_def Fract_coprime dvd_div_neg rat_number_collapse
   7.309 +    split:split_if_asm)
   7.310 +
   7.311 +lemma normalize_denom_pos: "normalize r = (p, q) \<Longrightarrow> q > 0"
   7.312 +  by (auto simp add: normalize_def Let_def dvd_div_neg pos_imp_zdiv_neg_iff nonneg1_imp_zdiv_pos_iff
   7.313 +    split:split_if_asm)
   7.314 +
   7.315 +lemma normalize_coprime: "normalize r = (p, q) \<Longrightarrow> coprime p q"
   7.316 +  by (auto simp add: normalize_def Let_def dvd_div_neg div_gcd_coprime_int
   7.317 +    split:split_if_asm)
   7.318 +
   7.319 +lemma normalize_stable [simp]:
   7.320 +  "q > 0 \<Longrightarrow> coprime p q \<Longrightarrow> normalize (p, q) = (p, q)"
   7.321 +  by (simp add: normalize_def)
   7.322 +
   7.323 +lemma normalize_denom_zero [simp]:
   7.324 +  "normalize (p, 0) = (0, 1)"
   7.325 +  by (simp add: normalize_def)
   7.326 +
   7.327 +lemma normalize_negative [simp]:
   7.328 +  "q < 0 \<Longrightarrow> normalize (p, q) = normalize (- p, - q)"
   7.329 +  by (simp add: normalize_def Let_def dvd_div_neg dvd_neg_div)
   7.330 +
   7.331 +text{*
   7.332 +  Decompose a fraction into normalized, i.e. coprime numerator and denominator:
   7.333 +*}
   7.334 +
   7.335 +definition quotient_of :: "rat \<Rightarrow> int \<times> int" where
   7.336 +  "quotient_of x = (THE pair. x = Fract (fst pair) (snd pair) &
   7.337 +                   snd pair > 0 & coprime (fst pair) (snd pair))"
   7.338 +
   7.339 +lemma quotient_of_unique:
   7.340 +  "\<exists>!p. r = Fract (fst p) (snd p) \<and> snd p > 0 \<and> coprime (fst p) (snd p)"
   7.341 +proof (cases r)
   7.342 +  case (Fract a b)
   7.343 +  then have "r = Fract (fst (a, b)) (snd (a, b)) \<and> snd (a, b) > 0 \<and> coprime (fst (a, b)) (snd (a, b))" by auto
   7.344 +  then show ?thesis proof (rule ex1I)
   7.345 +    fix p
   7.346 +    obtain c d :: int where p: "p = (c, d)" by (cases p)
   7.347 +    assume "r = Fract (fst p) (snd p) \<and> snd p > 0 \<and> coprime (fst p) (snd p)"
   7.348 +    with p have Fract': "r = Fract c d" "d > 0" "coprime c d" by simp_all
   7.349 +    have "c = a \<and> d = b"
   7.350 +    proof (cases "a = 0")
   7.351 +      case True with Fract Fract' show ?thesis by (simp add: eq_rat)
   7.352 +    next
   7.353 +      case False
   7.354 +      with Fract Fract' have *: "c * b = a * d" and "c \<noteq> 0" by (auto simp add: eq_rat)
   7.355 +      then have "c * b > 0 \<longleftrightarrow> a * d > 0" by auto
   7.356 +      with `b > 0` `d > 0` have "a > 0 \<longleftrightarrow> c > 0" by (simp add: zero_less_mult_iff)
   7.357 +      with `a \<noteq> 0` `c \<noteq> 0` have sgn: "sgn a = sgn c" by (auto simp add: not_less)
   7.358 +      from `coprime a b` `coprime c d` have "\<bar>a\<bar> * \<bar>d\<bar> = \<bar>c\<bar> * \<bar>b\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>c\<bar> \<and> \<bar>d\<bar> = \<bar>b\<bar>"
   7.359 +        by (simp add: coprime_crossproduct_int)
   7.360 +      with `b > 0` `d > 0` have "\<bar>a\<bar> * d = \<bar>c\<bar> * b \<longleftrightarrow> \<bar>a\<bar> = \<bar>c\<bar> \<and> d = b" by simp
   7.361 +      then have "a * sgn a * d = c * sgn c * b \<longleftrightarrow> a * sgn a = c * sgn c \<and> d = b" by (simp add: abs_sgn)
   7.362 +      with sgn * show ?thesis by (auto simp add: sgn_0_0)
   7.363 +    qed
   7.364 +    with p show "p = (a, b)" by simp
   7.365 +  qed
   7.366 +qed
   7.367 +
   7.368 +lemma quotient_of_Fract [code]:
   7.369 +  "quotient_of (Fract a b) = normalize (a, b)"
   7.370 +proof -
   7.371 +  have "Fract a b = Fract (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?Fract)
   7.372 +    by (rule sym) (auto intro: normalize_eq)
   7.373 +  moreover have "0 < snd (normalize (a, b))" (is ?denom_pos) 
   7.374 +    by (cases "normalize (a, b)") (rule normalize_denom_pos, simp)
   7.375 +  moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime)
   7.376 +    by (rule normalize_coprime) simp
   7.377 +  ultimately have "?Fract \<and> ?denom_pos \<and> ?coprime" by blast
   7.378 +  with quotient_of_unique have
   7.379 +    "(THE p. Fract a b = Fract (fst p) (snd p) \<and> 0 < snd p \<and> coprime (fst p) (snd p)) = normalize (a, b)"
   7.380 +    by (rule the1_equality)
   7.381 +  then show ?thesis by (simp add: quotient_of_def)
   7.382 +qed
   7.383 +
   7.384 +lemma quotient_of_number [simp]:
   7.385 +  "quotient_of 0 = (0, 1)"
   7.386 +  "quotient_of 1 = (1, 1)"
   7.387 +  "quotient_of (number_of k) = (number_of k, 1)"
   7.388 +  by (simp_all add: rat_number_expand quotient_of_Fract)
   7.389 +
   7.390 +lemma quotient_of_eq: "quotient_of (Fract a b) = (p, q) \<Longrightarrow> Fract p q = Fract a b"
   7.391 +  by (simp add: quotient_of_Fract normalize_eq)
   7.392 +
   7.393 +lemma quotient_of_denom_pos: "quotient_of r = (p, q) \<Longrightarrow> q > 0"
   7.394 +  by (cases r) (simp add: quotient_of_Fract normalize_denom_pos)
   7.395 +
   7.396 +lemma quotient_of_coprime: "quotient_of r = (p, q) \<Longrightarrow> coprime p q"
   7.397 +  by (cases r) (simp add: quotient_of_Fract normalize_coprime)
   7.398 +
   7.399 +lemma quotient_of_inject:
   7.400 +  assumes "quotient_of a = quotient_of b"
   7.401 +  shows "a = b"
   7.402 +proof -
   7.403 +  obtain p q r s where a: "a = Fract p q"
   7.404 +    and b: "b = Fract r s"
   7.405 +    and "q > 0" and "s > 0" by (cases a, cases b)
   7.406 +  with assms show ?thesis by (simp add: eq_rat quotient_of_Fract normalize_crossproduct)
   7.407 +qed
   7.408 +
   7.409 +lemma quotient_of_inject_eq:
   7.410 +  "quotient_of a = quotient_of b \<longleftrightarrow> a = b"
   7.411 +  by (auto simp add: quotient_of_inject)
   7.412 +
   7.413 +
   7.414 +subsubsection {* The field of rational numbers *}
   7.415 +
   7.416 +instantiation rat :: "{field, division_by_zero}"
   7.417 +begin
   7.418 +
   7.419 +definition
   7.420 +  inverse_rat_def:
   7.421 +  "inverse q = Abs_Rat (\<Union>x \<in> Rep_Rat q.
   7.422 +     ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})"
   7.423 +
   7.424 +lemma inverse_rat [simp]: "inverse (Fract a b) = Fract b a"
   7.425 +proof -
   7.426 +  have "(\<lambda>x. ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)}) respects ratrel"
   7.427 +    by (auto simp add: congruent_def mult_commute)
   7.428 +  then show ?thesis by (simp add: Fract_def inverse_rat_def UN_ratrel)
   7.429 +qed
   7.430 +
   7.431 +definition
   7.432 +  divide_rat_def: "q / r = q * inverse (r::rat)"
   7.433 +
   7.434 +lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
   7.435 +  by (simp add: divide_rat_def)
   7.436 +
   7.437 +instance proof
   7.438 +  show "inverse 0 = (0::rat)" by (simp add: rat_number_expand)
   7.439 +    (simp add: rat_number_collapse)
   7.440 +next
   7.441 +  fix q :: rat
   7.442 +  assume "q \<noteq> 0"
   7.443 +  then show "inverse q * q = 1" by (cases q rule: Rat_cases_nonzero)
   7.444 +   (simp_all add: rat_number_expand eq_rat)
   7.445 +next
   7.446 +  fix q r :: rat
   7.447 +  show "q / r = q * inverse r" by (simp add: divide_rat_def)
   7.448 +qed
   7.449 +
   7.450 +end
   7.451 +
   7.452 +
   7.453 +subsubsection {* Various *}
   7.454 +
   7.455 +lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1"
   7.456 +  by (simp add: rat_number_expand)
   7.457 +
   7.458 +lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l"
   7.459 +  by (simp add: Fract_of_int_eq [symmetric])
   7.460 +
   7.461 +lemma Fract_number_of_quotient:
   7.462 +  "Fract (number_of k) (number_of l) = number_of k / number_of l"
   7.463 +  unfolding Fract_of_int_quotient number_of_is_id number_of_eq ..
   7.464 +
   7.465 +lemma Fract_1_number_of:
   7.466 +  "Fract 1 (number_of k) = 1 / number_of k"
   7.467 +  unfolding Fract_of_int_quotient number_of_eq by simp
   7.468 +
   7.469 +subsubsection {* The ordered field of rational numbers *}
   7.470 +
   7.471 +instantiation rat :: linorder
   7.472 +begin
   7.473 +
   7.474 +definition
   7.475 +  le_rat_def:
   7.476 +   "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
   7.477 +      {(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})"
   7.478 +
   7.479 +lemma le_rat [simp]:
   7.480 +  assumes "b \<noteq> 0" and "d \<noteq> 0"
   7.481 +  shows "Fract a b \<le> Fract c d \<longleftrightarrow> (a * d) * (b * d) \<le> (c * b) * (b * d)"
   7.482 +proof -
   7.483 +  have "(\<lambda>x y. {(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})
   7.484 +    respects2 ratrel"
   7.485 +  proof (clarsimp simp add: congruent2_def)
   7.486 +    fix a b a' b' c d c' d'::int
   7.487 +    assume neq: "b \<noteq> 0"  "b' \<noteq> 0"  "d \<noteq> 0"  "d' \<noteq> 0"
   7.488 +    assume eq1: "a * b' = a' * b"
   7.489 +    assume eq2: "c * d' = c' * d"
   7.490 +
   7.491 +    let ?le = "\<lambda>a b c d. ((a * d) * (b * d) \<le> (c * b) * (b * d))"
   7.492 +    {
   7.493 +      fix a b c d x :: int assume x: "x \<noteq> 0"
   7.494 +      have "?le a b c d = ?le (a * x) (b * x) c d"
   7.495 +      proof -
   7.496 +        from x have "0 < x * x" by (auto simp add: zero_less_mult_iff)
   7.497 +        hence "?le a b c d =
   7.498 +            ((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))"
   7.499 +          by (simp add: mult_le_cancel_right)
   7.500 +        also have "... = ?le (a * x) (b * x) c d"
   7.501 +          by (simp add: mult_ac)
   7.502 +        finally show ?thesis .
   7.503 +      qed
   7.504 +    } note le_factor = this
   7.505 +
   7.506 +    let ?D = "b * d" and ?D' = "b' * d'"
   7.507 +    from neq have D: "?D \<noteq> 0" by simp
   7.508 +    from neq have "?D' \<noteq> 0" by simp
   7.509 +    hence "?le a b c d = ?le (a * ?D') (b * ?D') c d"
   7.510 +      by (rule le_factor)
   7.511 +    also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')" 
   7.512 +      by (simp add: mult_ac)
   7.513 +    also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')"
   7.514 +      by (simp only: eq1 eq2)
   7.515 +    also have "... = ?le (a' * ?D) (b' * ?D) c' d'"
   7.516 +      by (simp add: mult_ac)
   7.517 +    also from D have "... = ?le a' b' c' d'"
   7.518 +      by (rule le_factor [symmetric])
   7.519 +    finally show "?le a b c d = ?le a' b' c' d'" .
   7.520 +  qed
   7.521 +  with assms show ?thesis by (simp add: Fract_def le_rat_def UN_ratrel2)
   7.522 +qed
   7.523 +
   7.524 +definition
   7.525 +  less_rat_def: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
   7.526 +
   7.527 +lemma less_rat [simp]:
   7.528 +  assumes "b \<noteq> 0" and "d \<noteq> 0"
   7.529 +  shows "Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)"
   7.530 +  using assms by (simp add: less_rat_def eq_rat order_less_le)
   7.531 +
   7.532 +instance proof
   7.533 +  fix q r s :: rat
   7.534 +  {
   7.535 +    assume "q \<le> r" and "r \<le> s"
   7.536 +    then show "q \<le> s" 
   7.537 +    proof (induct q, induct r, induct s)
   7.538 +      fix a b c d e f :: int
   7.539 +      assume neq: "b > 0"  "d > 0"  "f > 0"
   7.540 +      assume 1: "Fract a b \<le> Fract c d" and 2: "Fract c d \<le> Fract e f"
   7.541 +      show "Fract a b \<le> Fract e f"
   7.542 +      proof -
   7.543 +        from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f"
   7.544 +          by (auto simp add: zero_less_mult_iff linorder_neq_iff)
   7.545 +        have "(a * d) * (b * d) * (f * f) \<le> (c * b) * (b * d) * (f * f)"
   7.546 +        proof -
   7.547 +          from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)"
   7.548 +            by simp
   7.549 +          with ff show ?thesis by (simp add: mult_le_cancel_right)
   7.550 +        qed
   7.551 +        also have "... = (c * f) * (d * f) * (b * b)" by algebra
   7.552 +        also have "... \<le> (e * d) * (d * f) * (b * b)"
   7.553 +        proof -
   7.554 +          from neq 2 have "(c * f) * (d * f) \<le> (e * d) * (d * f)"
   7.555 +            by simp
   7.556 +          with bb show ?thesis by (simp add: mult_le_cancel_right)
   7.557 +        qed
   7.558 +        finally have "(a * f) * (b * f) * (d * d) \<le> e * b * (b * f) * (d * d)"
   7.559 +          by (simp only: mult_ac)
   7.560 +        with dd have "(a * f) * (b * f) \<le> (e * b) * (b * f)"
   7.561 +          by (simp add: mult_le_cancel_right)
   7.562 +        with neq show ?thesis by simp
   7.563 +      qed
   7.564 +    qed
   7.565 +  next
   7.566 +    assume "q \<le> r" and "r \<le> q"
   7.567 +    then show "q = r"
   7.568 +    proof (induct q, induct r)
   7.569 +      fix a b c d :: int
   7.570 +      assume neq: "b > 0"  "d > 0"
   7.571 +      assume 1: "Fract a b \<le> Fract c d" and 2: "Fract c d \<le> Fract a b"
   7.572 +      show "Fract a b = Fract c d"
   7.573 +      proof -
   7.574 +        from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)"
   7.575 +          by simp
   7.576 +        also have "... \<le> (a * d) * (b * d)"
   7.577 +        proof -
   7.578 +          from neq 2 have "(c * b) * (d * b) \<le> (a * d) * (d * b)"
   7.579 +            by simp
   7.580 +          thus ?thesis by (simp only: mult_ac)
   7.581 +        qed
   7.582 +        finally have "(a * d) * (b * d) = (c * b) * (b * d)" .
   7.583 +        moreover from neq have "b * d \<noteq> 0" by simp
   7.584 +        ultimately have "a * d = c * b" by simp
   7.585 +        with neq show ?thesis by (simp add: eq_rat)
   7.586 +      qed
   7.587 +    qed
   7.588 +  next
   7.589 +    show "q \<le> q"
   7.590 +      by (induct q) simp
   7.591 +    show "(q < r) = (q \<le> r \<and> \<not> r \<le> q)"
   7.592 +      by (induct q, induct r) (auto simp add: le_less mult_commute)
   7.593 +    show "q \<le> r \<or> r \<le> q"
   7.594 +      by (induct q, induct r)
   7.595 +         (simp add: mult_commute, rule linorder_linear)
   7.596 +  }
   7.597 +qed
   7.598 +
   7.599 +end
   7.600 +
   7.601 +instantiation rat :: "{distrib_lattice, abs_if, sgn_if}"
   7.602 +begin
   7.603 +
   7.604 +definition
   7.605 +  abs_rat_def: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))"
   7.606 +
   7.607 +lemma abs_rat [simp, code]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
   7.608 +  by (auto simp add: abs_rat_def zabs_def Zero_rat_def not_less le_less eq_rat zero_less_mult_iff)
   7.609 +
   7.610 +definition
   7.611 +  sgn_rat_def: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else - 1)"
   7.612 +
   7.613 +lemma sgn_rat [simp, code]: "sgn (Fract a b) = of_int (sgn a * sgn b)"
   7.614 +  unfolding Fract_of_int_eq
   7.615 +  by (auto simp: zsgn_def sgn_rat_def Zero_rat_def eq_rat)
   7.616 +    (auto simp: rat_number_collapse not_less le_less zero_less_mult_iff)
   7.617 +
   7.618 +definition
   7.619 +  "(inf \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat) = min"
   7.620 +
   7.621 +definition
   7.622 +  "(sup \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat) = max"
   7.623 +
   7.624 +instance by intro_classes
   7.625 +  (auto simp add: abs_rat_def sgn_rat_def min_max.sup_inf_distrib1 inf_rat_def sup_rat_def)
   7.626 +
   7.627 +end
   7.628 +
   7.629 +instance rat :: linordered_field
   7.630 +proof
   7.631 +  fix q r s :: rat
   7.632 +  show "q \<le> r ==> s + q \<le> s + r"
   7.633 +  proof (induct q, induct r, induct s)
   7.634 +    fix a b c d e f :: int
   7.635 +    assume neq: "b > 0"  "d > 0"  "f > 0"
   7.636 +    assume le: "Fract a b \<le> Fract c d"
   7.637 +    show "Fract e f + Fract a b \<le> Fract e f + Fract c d"
   7.638 +    proof -
   7.639 +      let ?F = "f * f" from neq have F: "0 < ?F"
   7.640 +        by (auto simp add: zero_less_mult_iff)
   7.641 +      from neq le have "(a * d) * (b * d) \<le> (c * b) * (b * d)"
   7.642 +        by simp
   7.643 +      with F have "(a * d) * (b * d) * ?F * ?F \<le> (c * b) * (b * d) * ?F * ?F"
   7.644 +        by (simp add: mult_le_cancel_right)
   7.645 +      with neq show ?thesis by (simp add: mult_ac int_distrib)
   7.646 +    qed
   7.647 +  qed
   7.648 +  show "q < r ==> 0 < s ==> s * q < s * r"
   7.649 +  proof (induct q, induct r, induct s)
   7.650 +    fix a b c d e f :: int
   7.651 +    assume neq: "b > 0"  "d > 0"  "f > 0"
   7.652 +    assume le: "Fract a b < Fract c d"
   7.653 +    assume gt: "0 < Fract e f"
   7.654 +    show "Fract e f * Fract a b < Fract e f * Fract c d"
   7.655 +    proof -
   7.656 +      let ?E = "e * f" and ?F = "f * f"
   7.657 +      from neq gt have "0 < ?E"
   7.658 +        by (auto simp add: Zero_rat_def order_less_le eq_rat)
   7.659 +      moreover from neq have "0 < ?F"
   7.660 +        by (auto simp add: zero_less_mult_iff)
   7.661 +      moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)"
   7.662 +        by simp
   7.663 +      ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F"
   7.664 +        by (simp add: mult_less_cancel_right)
   7.665 +      with neq show ?thesis
   7.666 +        by (simp add: mult_ac)
   7.667 +    qed
   7.668 +  qed
   7.669 +qed auto
   7.670 +
   7.671 +lemma Rat_induct_pos [case_names Fract, induct type: rat]:
   7.672 +  assumes step: "\<And>a b. 0 < b \<Longrightarrow> P (Fract a b)"
   7.673 +  shows "P q"
   7.674 +proof (cases q)
   7.675 +  have step': "\<And>a b. b < 0 \<Longrightarrow> P (Fract a b)"
   7.676 +  proof -
   7.677 +    fix a::int and b::int
   7.678 +    assume b: "b < 0"
   7.679 +    hence "0 < -b" by simp
   7.680 +    hence "P (Fract (-a) (-b))" by (rule step)
   7.681 +    thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b])
   7.682 +  qed
   7.683 +  case (Fract a b)
   7.684 +  thus "P q" by (force simp add: linorder_neq_iff step step')
   7.685 +qed
   7.686 +
   7.687 +lemma zero_less_Fract_iff:
   7.688 +  "0 < b \<Longrightarrow> 0 < Fract a b \<longleftrightarrow> 0 < a"
   7.689 +  by (simp add: Zero_rat_def zero_less_mult_iff)
   7.690 +
   7.691 +lemma Fract_less_zero_iff:
   7.692 +  "0 < b \<Longrightarrow> Fract a b < 0 \<longleftrightarrow> a < 0"
   7.693 +  by (simp add: Zero_rat_def mult_less_0_iff)
   7.694 +
   7.695 +lemma zero_le_Fract_iff:
   7.696 +  "0 < b \<Longrightarrow> 0 \<le> Fract a b \<longleftrightarrow> 0 \<le> a"
   7.697 +  by (simp add: Zero_rat_def zero_le_mult_iff)
   7.698 +
   7.699 +lemma Fract_le_zero_iff:
   7.700 +  "0 < b \<Longrightarrow> Fract a b \<le> 0 \<longleftrightarrow> a \<le> 0"
   7.701 +  by (simp add: Zero_rat_def mult_le_0_iff)
   7.702 +
   7.703 +lemma one_less_Fract_iff:
   7.704 +  "0 < b \<Longrightarrow> 1 < Fract a b \<longleftrightarrow> b < a"
   7.705 +  by (simp add: One_rat_def mult_less_cancel_right_disj)
   7.706 +
   7.707 +lemma Fract_less_one_iff:
   7.708 +  "0 < b \<Longrightarrow> Fract a b < 1 \<longleftrightarrow> a < b"
   7.709 +  by (simp add: One_rat_def mult_less_cancel_right_disj)
   7.710 +
   7.711 +lemma one_le_Fract_iff:
   7.712 +  "0 < b \<Longrightarrow> 1 \<le> Fract a b \<longleftrightarrow> b \<le> a"
   7.713 +  by (simp add: One_rat_def mult_le_cancel_right)
   7.714 +
   7.715 +lemma Fract_le_one_iff:
   7.716 +  "0 < b \<Longrightarrow> Fract a b \<le> 1 \<longleftrightarrow> a \<le> b"
   7.717 +  by (simp add: One_rat_def mult_le_cancel_right)
   7.718 +
   7.719 +
   7.720 +subsubsection {* Rationals are an Archimedean field *}
   7.721 +
   7.722 +lemma rat_floor_lemma:
   7.723 +  shows "of_int (a div b) \<le> Fract a b \<and> Fract a b < of_int (a div b + 1)"
   7.724 +proof -
   7.725 +  have "Fract a b = of_int (a div b) + Fract (a mod b) b"
   7.726 +    by (cases "b = 0", simp, simp add: of_int_rat)
   7.727 +  moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1"
   7.728 +    unfolding Fract_of_int_quotient
   7.729 +    by (rule linorder_cases [of b 0])
   7.730 +       (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos)
   7.731 +  ultimately show ?thesis by simp
   7.732 +qed
   7.733 +
   7.734 +instance rat :: archimedean_field
   7.735 +proof
   7.736 +  fix r :: rat
   7.737 +  show "\<exists>z. r \<le> of_int z"
   7.738 +  proof (induct r)
   7.739 +    case (Fract a b)
   7.740 +    have "Fract a b \<le> of_int (a div b + 1)"
   7.741 +      using rat_floor_lemma [of a b] by simp
   7.742 +    then show "\<exists>z. Fract a b \<le> of_int z" ..
   7.743 +  qed
   7.744 +qed
   7.745 +
   7.746 +lemma floor_Fract: "floor (Fract a b) = a div b"
   7.747 +  using rat_floor_lemma [of a b]
   7.748 +  by (simp add: floor_unique)
   7.749 +
   7.750 +
   7.751 +subsection {* Linear arithmetic setup *}
   7.752 +
   7.753 +declaration {*
   7.754 +  K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
   7.755 +    (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *)
   7.756 +  #> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_int_eq_iff} RS iffD2]
   7.757 +    (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
   7.758 +  #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
   7.759 +      @{thm True_implies_equals},
   7.760 +      read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
   7.761 +      @{thm divide_1}, @{thm divide_zero_left},
   7.762 +      @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
   7.763 +      @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
   7.764 +      @{thm of_int_minus}, @{thm of_int_diff},
   7.765 +      @{thm of_int_of_nat_eq}]
   7.766 +  #> Lin_Arith.add_simprocs Numeral_Simprocs.field_cancel_numeral_factors
   7.767 +  #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"})
   7.768 +  #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"}))
   7.769 +*}
   7.770 +
   7.771 +
   7.772 +subsection {* Embedding from Rationals to other Fields *}
   7.773 +
   7.774 +class field_char_0 = field + ring_char_0
   7.775 +
   7.776 +subclass (in linordered_field) field_char_0 ..
   7.777 +
   7.778 +context field_char_0
   7.779 +begin
   7.780 +
   7.781 +definition of_rat :: "rat \<Rightarrow> 'a" where
   7.782 +  "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
   7.783 +
   7.784 +end
   7.785 +
   7.786 +lemma of_rat_congruent:
   7.787 +  "(\<lambda>(a, b). {of_int a / of_int b :: 'a::field_char_0}) respects ratrel"
   7.788 +apply (rule congruent.intro)
   7.789 +apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq)
   7.790 +apply (simp only: of_int_mult [symmetric])
   7.791 +done
   7.792 +
   7.793 +lemma of_rat_rat: "b \<noteq> 0 \<Longrightarrow> of_rat (Fract a b) = of_int a / of_int b"
   7.794 +  unfolding Fract_def of_rat_def by (simp add: UN_ratrel of_rat_congruent)
   7.795 +
   7.796 +lemma of_rat_0 [simp]: "of_rat 0 = 0"
   7.797 +by (simp add: Zero_rat_def of_rat_rat)
   7.798 +
   7.799 +lemma of_rat_1 [simp]: "of_rat 1 = 1"
   7.800 +by (simp add: One_rat_def of_rat_rat)
   7.801 +
   7.802 +lemma of_rat_add: "of_rat (a + b) = of_rat a + of_rat b"
   7.803 +by (induct a, induct b, simp add: of_rat_rat add_frac_eq)
   7.804 +
   7.805 +lemma of_rat_minus: "of_rat (- a) = - of_rat a"
   7.806 +by (induct a, simp add: of_rat_rat)
   7.807 +
   7.808 +lemma of_rat_diff: "of_rat (a - b) = of_rat a - of_rat b"
   7.809 +by (simp only: diff_minus of_rat_add of_rat_minus)
   7.810 +
   7.811 +lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b"
   7.812 +apply (induct a, induct b, simp add: of_rat_rat)
   7.813 +apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac)
   7.814 +done
   7.815 +
   7.816 +lemma nonzero_of_rat_inverse:
   7.817 +  "a \<noteq> 0 \<Longrightarrow> of_rat (inverse a) = inverse (of_rat a)"
   7.818 +apply (rule inverse_unique [symmetric])
   7.819 +apply (simp add: of_rat_mult [symmetric])
   7.820 +done
   7.821 +
   7.822 +lemma of_rat_inverse:
   7.823 +  "(of_rat (inverse a)::'a::{field_char_0,division_by_zero}) =
   7.824 +   inverse (of_rat a)"
   7.825 +by (cases "a = 0", simp_all add: nonzero_of_rat_inverse)
   7.826 +
   7.827 +lemma nonzero_of_rat_divide:
   7.828 +  "b \<noteq> 0 \<Longrightarrow> of_rat (a / b) = of_rat a / of_rat b"
   7.829 +by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse)
   7.830 +
   7.831 +lemma of_rat_divide:
   7.832 +  "(of_rat (a / b)::'a::{field_char_0,division_by_zero})
   7.833 +   = of_rat a / of_rat b"
   7.834 +by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
   7.835 +
   7.836 +lemma of_rat_power:
   7.837 +  "(of_rat (a ^ n)::'a::field_char_0) = of_rat a ^ n"
   7.838 +by (induct n) (simp_all add: of_rat_mult)
   7.839 +
   7.840 +lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)"
   7.841 +apply (induct a, induct b)
   7.842 +apply (simp add: of_rat_rat eq_rat)
   7.843 +apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq)
   7.844 +apply (simp only: of_int_mult [symmetric] of_int_eq_iff)
   7.845 +done
   7.846 +
   7.847 +lemma of_rat_less:
   7.848 +  "(of_rat r :: 'a::linordered_field) < of_rat s \<longleftrightarrow> r < s"
   7.849 +proof (induct r, induct s)
   7.850 +  fix a b c d :: int
   7.851 +  assume not_zero: "b > 0" "d > 0"
   7.852 +  then have "b * d > 0" by (rule mult_pos_pos)
   7.853 +  have of_int_divide_less_eq:
   7.854 +    "(of_int a :: 'a) / of_int b < of_int c / of_int d
   7.855 +      \<longleftrightarrow> (of_int a :: 'a) * of_int d < of_int c * of_int b"
   7.856 +    using not_zero by (simp add: pos_less_divide_eq pos_divide_less_eq)
   7.857 +  show "(of_rat (Fract a b) :: 'a::linordered_field) < of_rat (Fract c d)
   7.858 +    \<longleftrightarrow> Fract a b < Fract c d"
   7.859 +    using not_zero `b * d > 0`
   7.860 +    by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult)
   7.861 +qed
   7.862 +
   7.863 +lemma of_rat_less_eq:
   7.864 +  "(of_rat r :: 'a::linordered_field) \<le> of_rat s \<longleftrightarrow> r \<le> s"
   7.865 +  unfolding le_less by (auto simp add: of_rat_less)
   7.866 +
   7.867 +lemmas of_rat_eq_0_iff [simp] = of_rat_eq_iff [of _ 0, simplified]
   7.868 +
   7.869 +lemma of_rat_eq_id [simp]: "of_rat = id"
   7.870 +proof
   7.871 +  fix a
   7.872 +  show "of_rat a = id a"
   7.873 +  by (induct a)
   7.874 +     (simp add: of_rat_rat Fract_of_int_eq [symmetric])
   7.875 +qed
   7.876 +
   7.877 +text{*Collapse nested embeddings*}
   7.878 +lemma of_rat_of_nat_eq [simp]: "of_rat (of_nat n) = of_nat n"
   7.879 +by (induct n) (simp_all add: of_rat_add)
   7.880 +
   7.881 +lemma of_rat_of_int_eq [simp]: "of_rat (of_int z) = of_int z"
   7.882 +by (cases z rule: int_diff_cases) (simp add: of_rat_diff)
   7.883 +
   7.884 +lemma of_rat_number_of_eq [simp]:
   7.885 +  "of_rat (number_of w) = (number_of w :: 'a::{number_ring,field_char_0})"
   7.886 +by (simp add: number_of_eq)
   7.887 +
   7.888 +lemmas zero_rat = Zero_rat_def
   7.889 +lemmas one_rat = One_rat_def
   7.890 +
   7.891 +abbreviation
   7.892 +  rat_of_nat :: "nat \<Rightarrow> rat"
   7.893 +where
   7.894 +  "rat_of_nat \<equiv> of_nat"
   7.895 +
   7.896 +abbreviation
   7.897 +  rat_of_int :: "int \<Rightarrow> rat"
   7.898 +where
   7.899 +  "rat_of_int \<equiv> of_int"
   7.900 +
   7.901 +subsection {* The Set of Rational Numbers *}
   7.902 +
   7.903 +context field_char_0
   7.904 +begin
   7.905 +
   7.906 +definition
   7.907 +  Rats  :: "'a set" where
   7.908 +  "Rats = range of_rat"
   7.909 +
   7.910 +notation (xsymbols)
   7.911 +  Rats  ("\<rat>")
   7.912 +
   7.913 +end
   7.914 +
   7.915 +lemma Rats_of_rat [simp]: "of_rat r \<in> Rats"
   7.916 +by (simp add: Rats_def)
   7.917 +
   7.918 +lemma Rats_of_int [simp]: "of_int z \<in> Rats"
   7.919 +by (subst of_rat_of_int_eq [symmetric], rule Rats_of_rat)
   7.920 +
   7.921 +lemma Rats_of_nat [simp]: "of_nat n \<in> Rats"
   7.922 +by (subst of_rat_of_nat_eq [symmetric], rule Rats_of_rat)
   7.923 +
   7.924 +lemma Rats_number_of [simp]:
   7.925 +  "(number_of w::'a::{number_ring,field_char_0}) \<in> Rats"
   7.926 +by (subst of_rat_number_of_eq [symmetric], rule Rats_of_rat)
   7.927 +
   7.928 +lemma Rats_0 [simp]: "0 \<in> Rats"
   7.929 +apply (unfold Rats_def)
   7.930 +apply (rule range_eqI)
   7.931 +apply (rule of_rat_0 [symmetric])
   7.932 +done
   7.933 +
   7.934 +lemma Rats_1 [simp]: "1 \<in> Rats"
   7.935 +apply (unfold Rats_def)
   7.936 +apply (rule range_eqI)
   7.937 +apply (rule of_rat_1 [symmetric])
   7.938 +done
   7.939 +
   7.940 +lemma Rats_add [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a + b \<in> Rats"
   7.941 +apply (auto simp add: Rats_def)
   7.942 +apply (rule range_eqI)
   7.943 +apply (rule of_rat_add [symmetric])
   7.944 +done
   7.945 +
   7.946 +lemma Rats_minus [simp]: "a \<in> Rats \<Longrightarrow> - a \<in> Rats"
   7.947 +apply (auto simp add: Rats_def)
   7.948 +apply (rule range_eqI)
   7.949 +apply (rule of_rat_minus [symmetric])
   7.950 +done
   7.951 +
   7.952 +lemma Rats_diff [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a - b \<in> Rats"
   7.953 +apply (auto simp add: Rats_def)
   7.954 +apply (rule range_eqI)
   7.955 +apply (rule of_rat_diff [symmetric])
   7.956 +done
   7.957 +
   7.958 +lemma Rats_mult [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a * b \<in> Rats"
   7.959 +apply (auto simp add: Rats_def)
   7.960 +apply (rule range_eqI)
   7.961 +apply (rule of_rat_mult [symmetric])
   7.962 +done
   7.963 +
   7.964 +lemma nonzero_Rats_inverse:
   7.965 +  fixes a :: "'a::field_char_0"
   7.966 +  shows "\<lbrakk>a \<in> Rats; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> Rats"
   7.967 +apply (auto simp add: Rats_def)
   7.968 +apply (rule range_eqI)
   7.969 +apply (erule nonzero_of_rat_inverse [symmetric])
   7.970 +done
   7.971 +
   7.972 +lemma Rats_inverse [simp]:
   7.973 +  fixes a :: "'a::{field_char_0,division_by_zero}"
   7.974 +  shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats"
   7.975 +apply (auto simp add: Rats_def)
   7.976 +apply (rule range_eqI)
   7.977 +apply (rule of_rat_inverse [symmetric])
   7.978 +done
   7.979 +
   7.980 +lemma nonzero_Rats_divide:
   7.981 +  fixes a b :: "'a::field_char_0"
   7.982 +  shows "\<lbrakk>a \<in> Rats; b \<in> Rats; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
   7.983 +apply (auto simp add: Rats_def)
   7.984 +apply (rule range_eqI)
   7.985 +apply (erule nonzero_of_rat_divide [symmetric])
   7.986 +done
   7.987 +
   7.988 +lemma Rats_divide [simp]:
   7.989 +  fixes a b :: "'a::{field_char_0,division_by_zero}"
   7.990 +  shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
   7.991 +apply (auto simp add: Rats_def)
   7.992 +apply (rule range_eqI)
   7.993 +apply (rule of_rat_divide [symmetric])
   7.994 +done
   7.995 +
   7.996 +lemma Rats_power [simp]:
   7.997 +  fixes a :: "'a::field_char_0"
   7.998 +  shows "a \<in> Rats \<Longrightarrow> a ^ n \<in> Rats"
   7.999 +apply (auto simp add: Rats_def)
  7.1000 +apply (rule range_eqI)
  7.1001 +apply (rule of_rat_power [symmetric])
  7.1002 +done
  7.1003 +
  7.1004 +lemma Rats_cases [cases set: Rats]:
  7.1005 +  assumes "q \<in> \<rat>"
  7.1006 +  obtains (of_rat) r where "q = of_rat r"
  7.1007 +  unfolding Rats_def
  7.1008 +proof -
  7.1009 +  from `q \<in> \<rat>` have "q \<in> range of_rat" unfolding Rats_def .
  7.1010 +  then obtain r where "q = of_rat r" ..
  7.1011 +  then show thesis ..
  7.1012 +qed
  7.1013 +
  7.1014 +lemma Rats_induct [case_names of_rat, induct set: Rats]:
  7.1015 +  "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
  7.1016 +  by (rule Rats_cases) auto
  7.1017 +
  7.1018 +
  7.1019 +subsection {* Implementation of rational numbers as pairs of integers *}
  7.1020 +
  7.1021 +definition Frct :: "int \<times> int \<Rightarrow> rat" where
  7.1022 +  [simp]: "Frct p = Fract (fst p) (snd p)"
  7.1023 +
  7.1024 +code_abstype Frct quotient_of
  7.1025 +proof (rule eq_reflection)
  7.1026 +  show "Frct (quotient_of x) = x" by (cases x) (auto intro: quotient_of_eq)
  7.1027 +qed
  7.1028 +
  7.1029 +lemma Frct_code_post [code_post]:
  7.1030 +  "Frct (0, k) = 0"
  7.1031 +  "Frct (k, 0) = 0"
  7.1032 +  "Frct (1, 1) = 1"
  7.1033 +  "Frct (number_of k, 1) = number_of k"
  7.1034 +  "Frct (1, number_of k) = 1 / number_of k"
  7.1035 +  "Frct (number_of k, number_of l) = number_of k / number_of l"
  7.1036 +  by (simp_all add: rat_number_collapse Fract_number_of_quotient Fract_1_number_of)
  7.1037 +
  7.1038 +declare quotient_of_Fract [code abstract]
  7.1039 +
  7.1040 +lemma rat_zero_code [code abstract]:
  7.1041 +  "quotient_of 0 = (0, 1)"
  7.1042 +  by (simp add: Zero_rat_def quotient_of_Fract normalize_def)
  7.1043 +
  7.1044 +lemma rat_one_code [code abstract]:
  7.1045 +  "quotient_of 1 = (1, 1)"
  7.1046 +  by (simp add: One_rat_def quotient_of_Fract normalize_def)
  7.1047 +
  7.1048 +lemma rat_plus_code [code abstract]:
  7.1049 +  "quotient_of (p + q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q
  7.1050 +     in normalize (a * d + b * c, c * d))"
  7.1051 +  by (cases p, cases q) (simp add: quotient_of_Fract)
  7.1052 +
  7.1053 +lemma rat_uminus_code [code abstract]:
  7.1054 +  "quotient_of (- p) = (let (a, b) = quotient_of p in (- a, b))"
  7.1055 +  by (cases p) (simp add: quotient_of_Fract)
  7.1056 +
  7.1057 +lemma rat_minus_code [code abstract]:
  7.1058 +  "quotient_of (p - q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q
  7.1059 +     in normalize (a * d - b * c, c * d))"
  7.1060 +  by (cases p, cases q) (simp add: quotient_of_Fract)
  7.1061 +
  7.1062 +lemma rat_times_code [code abstract]:
  7.1063 +  "quotient_of (p * q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q
  7.1064 +     in normalize (a * b, c * d))"
  7.1065 +  by (cases p, cases q) (simp add: quotient_of_Fract)
  7.1066 +
  7.1067 +lemma rat_inverse_code [code abstract]:
  7.1068 +  "quotient_of (inverse p) = (let (a, b) = quotient_of p
  7.1069 +    in if a = 0 then (0, 1) else (sgn a * b, \<bar>a\<bar>))"
  7.1070 +proof (cases p)
  7.1071 +  case (Fract a b) then show ?thesis
  7.1072 +    by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract gcd_int.commute)
  7.1073 +qed
  7.1074 +
  7.1075 +lemma rat_divide_code [code abstract]:
  7.1076 +  "quotient_of (p / q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q
  7.1077 +     in normalize (a * d, c * b))"
  7.1078 +  by (cases p, cases q) (simp add: quotient_of_Fract)
  7.1079 +
  7.1080 +lemma rat_abs_code [code abstract]:
  7.1081 +  "quotient_of \<bar>p\<bar> = (let (a, b) = quotient_of p in (\<bar>a\<bar>, b))"
  7.1082 +  by (cases p) (simp add: quotient_of_Fract)
  7.1083 +
  7.1084 +lemma rat_sgn_code [code abstract]:
  7.1085 +  "quotient_of (sgn p) = (sgn (fst (quotient_of p)), 1)"
  7.1086 +proof (cases p)
  7.1087 +  case (Fract a b) then show ?thesis
  7.1088 +  by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract)
  7.1089 +qed
  7.1090 +
  7.1091 +instantiation rat :: eq
  7.1092 +begin
  7.1093 +
  7.1094 +definition [code]:
  7.1095 +  "eq_class.eq a b \<longleftrightarrow> quotient_of a = quotient_of b"
  7.1096 +
  7.1097 +instance proof
  7.1098 +qed (simp add: eq_rat_def quotient_of_inject_eq)
  7.1099 +
  7.1100 +lemma rat_eq_refl [code nbe]:
  7.1101 +  "eq_class.eq (r::rat) r \<longleftrightarrow> True"
  7.1102 +  by (rule HOL.eq_refl)
  7.1103 +
  7.1104 +end
  7.1105 +
  7.1106 +lemma rat_less_eq_code [code]:
  7.1107 +  "p \<le> q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d \<le> c * b)"
  7.1108 +  by (cases p, cases q) (simp add: quotient_of_Fract times.commute)
  7.1109 +
  7.1110 +lemma rat_less_code [code]:
  7.1111 +  "p < q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d < c * b)"
  7.1112 +  by (cases p, cases q) (simp add: quotient_of_Fract times.commute)
  7.1113 +
  7.1114 +lemma [code]:
  7.1115 +  "of_rat p = (let (a, b) = quotient_of p in of_int a / of_int b)"
  7.1116 +  by (cases p) (simp add: quotient_of_Fract of_rat_rat)
  7.1117 +
  7.1118 +definition (in term_syntax)
  7.1119 +  valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
  7.1120 +  [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l"
  7.1121 +
  7.1122 +notation fcomp (infixl "o>" 60)
  7.1123 +notation scomp (infixl "o\<rightarrow>" 60)
  7.1124 +
  7.1125 +instantiation rat :: random
  7.1126 +begin
  7.1127 +
  7.1128 +definition
  7.1129 +  "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
  7.1130 +     let j = Code_Numeral.int_of (denom + 1)
  7.1131 +     in valterm_fract num (j, \<lambda>u. Code_Evaluation.term_of j))))"
  7.1132 +
  7.1133 +instance ..
  7.1134 +
  7.1135 +end
  7.1136 +
  7.1137 +no_notation fcomp (infixl "o>" 60)
  7.1138 +no_notation scomp (infixl "o\<rightarrow>" 60)
  7.1139 +
  7.1140 +text {* Setup for SML code generator *}
  7.1141 +
  7.1142 +types_code
  7.1143 +  rat ("(int */ int)")
  7.1144 +attach (term_of) {*
  7.1145 +fun term_of_rat (p, q) =
  7.1146 +  let
  7.1147 +    val rT = Type ("Rat.rat", [])
  7.1148 +  in
  7.1149 +    if q = 1 orelse p = 0 then HOLogic.mk_number rT p
  7.1150 +    else @{term "op / \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"} $
  7.1151 +      HOLogic.mk_number rT p $ HOLogic.mk_number rT q
  7.1152 +  end;
  7.1153 +*}
  7.1154 +attach (test) {*
  7.1155 +fun gen_rat i =
  7.1156 +  let
  7.1157 +    val p = random_range 0 i;
  7.1158 +    val q = random_range 1 (i + 1);
  7.1159 +    val g = Integer.gcd p q;
  7.1160 +    val p' = p div g;
  7.1161 +    val q' = q div g;
  7.1162 +    val r = (if one_of [true, false] then p' else ~ p',
  7.1163 +      if p' = 0 then 1 else q')
  7.1164 +  in
  7.1165 +    (r, fn () => term_of_rat r)
  7.1166 +  end;
  7.1167 +*}
  7.1168 +
  7.1169 +consts_code
  7.1170 +  Fract ("(_,/ _)")
  7.1171 +
  7.1172 +consts_code
  7.1173 +  "of_int :: int \<Rightarrow> rat" ("\<module>rat'_of'_int")
  7.1174 +attach {*
  7.1175 +fun rat_of_int i = (i, 1);
  7.1176 +*}
  7.1177 +
  7.1178 +setup {*
  7.1179 +  Nitpick.register_frac_type @{type_name rat}
  7.1180 +   [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
  7.1181 +    (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
  7.1182 +    (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
  7.1183 +    (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}),
  7.1184 +    (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
  7.1185 +    (@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}),
  7.1186 +    (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
  7.1187 +    (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
  7.1188 +    (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
  7.1189 +    (@{const_name field_char_0_class.Rats}, @{const_name UNIV})]
  7.1190 +*}
  7.1191 +
  7.1192 +lemmas [nitpick_def] = inverse_rat_inst.inverse_rat
  7.1193 +  number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat
  7.1194 +  plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
  7.1195 +  zero_rat_inst.zero_rat
  7.1196 +
  7.1197 +end
     8.1 --- a/src/HOL/Rational.thy	Wed Feb 24 14:19:54 2010 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,1194 +0,0 @@
     8.4 -(*  Title:  HOL/Rational.thy
     8.5 -    Author: Markus Wenzel, TU Muenchen
     8.6 -*)
     8.7 -
     8.8 -header {* Rational numbers *}
     8.9 -
    8.10 -theory Rational
    8.11 -imports GCD Archimedean_Field
    8.12 -begin
    8.13 -
    8.14 -subsection {* Rational numbers as quotient *}
    8.15 -
    8.16 -subsubsection {* Construction of the type of rational numbers *}
    8.17 -
    8.18 -definition
    8.19 -  ratrel :: "((int \<times> int) \<times> (int \<times> int)) set" where
    8.20 -  "ratrel = {(x, y). snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x}"
    8.21 -
    8.22 -lemma ratrel_iff [simp]:
    8.23 -  "(x, y) \<in> ratrel \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x"
    8.24 -  by (simp add: ratrel_def)
    8.25 -
    8.26 -lemma refl_on_ratrel: "refl_on {x. snd x \<noteq> 0} ratrel"
    8.27 -  by (auto simp add: refl_on_def ratrel_def)
    8.28 -
    8.29 -lemma sym_ratrel: "sym ratrel"
    8.30 -  by (simp add: ratrel_def sym_def)
    8.31 -
    8.32 -lemma trans_ratrel: "trans ratrel"
    8.33 -proof (rule transI, unfold split_paired_all)
    8.34 -  fix a b a' b' a'' b'' :: int
    8.35 -  assume A: "((a, b), (a', b')) \<in> ratrel"
    8.36 -  assume B: "((a', b'), (a'', b'')) \<in> ratrel"
    8.37 -  have "b' * (a * b'') = b'' * (a * b')" by simp
    8.38 -  also from A have "a * b' = a' * b" by auto
    8.39 -  also have "b'' * (a' * b) = b * (a' * b'')" by simp
    8.40 -  also from B have "a' * b'' = a'' * b'" by auto
    8.41 -  also have "b * (a'' * b') = b' * (a'' * b)" by simp
    8.42 -  finally have "b' * (a * b'') = b' * (a'' * b)" .
    8.43 -  moreover from B have "b' \<noteq> 0" by auto
    8.44 -  ultimately have "a * b'' = a'' * b" by simp
    8.45 -  with A B show "((a, b), (a'', b'')) \<in> ratrel" by auto
    8.46 -qed
    8.47 -  
    8.48 -lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel"
    8.49 -  by (rule equiv.intro [OF refl_on_ratrel sym_ratrel trans_ratrel])
    8.50 -
    8.51 -lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel]
    8.52 -lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel]
    8.53 -
    8.54 -lemma equiv_ratrel_iff [iff]: 
    8.55 -  assumes "snd x \<noteq> 0" and "snd y \<noteq> 0"
    8.56 -  shows "ratrel `` {x} = ratrel `` {y} \<longleftrightarrow> (x, y) \<in> ratrel"
    8.57 -  by (rule eq_equiv_class_iff, rule equiv_ratrel) (auto simp add: assms)
    8.58 -
    8.59 -typedef (Rat) rat = "{x. snd x \<noteq> 0} // ratrel"
    8.60 -proof
    8.61 -  have "(0::int, 1::int) \<in> {x. snd x \<noteq> 0}" by simp
    8.62 -  then show "ratrel `` {(0, 1)} \<in> {x. snd x \<noteq> 0} // ratrel" by (rule quotientI)
    8.63 -qed
    8.64 -
    8.65 -lemma ratrel_in_Rat [simp]: "snd x \<noteq> 0 \<Longrightarrow> ratrel `` {x} \<in> Rat"
    8.66 -  by (simp add: Rat_def quotientI)
    8.67 -
    8.68 -declare Abs_Rat_inject [simp] Abs_Rat_inverse [simp]
    8.69 -
    8.70 -
    8.71 -subsubsection {* Representation and basic operations *}
    8.72 -
    8.73 -definition
    8.74 -  Fract :: "int \<Rightarrow> int \<Rightarrow> rat" where
    8.75 -  "Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})"
    8.76 -
    8.77 -lemma eq_rat:
    8.78 -  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"
    8.79 -  and "\<And>a. Fract a 0 = Fract 0 1"
    8.80 -  and "\<And>a c. Fract 0 a = Fract 0 c"
    8.81 -  by (simp_all add: Fract_def)
    8.82 -
    8.83 -lemma Rat_cases [case_names Fract, cases type: rat]:
    8.84 -  assumes "\<And>a b. q = Fract a b \<Longrightarrow> b > 0 \<Longrightarrow> coprime a b \<Longrightarrow> C"
    8.85 -  shows C
    8.86 -proof -
    8.87 -  obtain a b :: int where "q = Fract a b" and "b \<noteq> 0"
    8.88 -    by (cases q) (clarsimp simp add: Fract_def Rat_def quotient_def)
    8.89 -  let ?a = "a div gcd a b"
    8.90 -  let ?b = "b div gcd a b"
    8.91 -  from `b \<noteq> 0` have "?b * gcd a b = b"
    8.92 -    by (simp add: dvd_div_mult_self)
    8.93 -  with `b \<noteq> 0` have "?b \<noteq> 0" by auto
    8.94 -  from `q = Fract a b` `b \<noteq> 0` `?b \<noteq> 0` have q: "q = Fract ?a ?b"
    8.95 -    by (simp add: eq_rat dvd_div_mult mult_commute [of a])
    8.96 -  from `b \<noteq> 0` have coprime: "coprime ?a ?b"
    8.97 -    by (auto intro: div_gcd_coprime_int)
    8.98 -  show C proof (cases "b > 0")
    8.99 -    case True
   8.100 -    note assms
   8.101 -    moreover note q
   8.102 -    moreover from True have "?b > 0" by (simp add: nonneg1_imp_zdiv_pos_iff)
   8.103 -    moreover note coprime
   8.104 -    ultimately show C .
   8.105 -  next
   8.106 -    case False
   8.107 -    note assms
   8.108 -    moreover from q have "q = Fract (- ?a) (- ?b)" by (simp add: Fract_def)
   8.109 -    moreover from False `b \<noteq> 0` have "- ?b > 0" by (simp add: pos_imp_zdiv_neg_iff)
   8.110 -    moreover from coprime have "coprime (- ?a) (- ?b)" by simp
   8.111 -    ultimately show C .
   8.112 -  qed
   8.113 -qed
   8.114 -
   8.115 -lemma Rat_induct [case_names Fract, induct type: rat]:
   8.116 -  assumes "\<And>a b. b > 0 \<Longrightarrow> coprime a b \<Longrightarrow> P (Fract a b)"
   8.117 -  shows "P q"
   8.118 -  using assms by (cases q) simp
   8.119 -
   8.120 -instantiation rat :: comm_ring_1
   8.121 -begin
   8.122 -
   8.123 -definition
   8.124 -  Zero_rat_def: "0 = Fract 0 1"
   8.125 -
   8.126 -definition
   8.127 -  One_rat_def: "1 = Fract 1 1"
   8.128 -
   8.129 -definition
   8.130 -  add_rat_def:
   8.131 -  "q + r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
   8.132 -    ratrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})"
   8.133 -
   8.134 -lemma add_rat [simp]:
   8.135 -  assumes "b \<noteq> 0" and "d \<noteq> 0"
   8.136 -  shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)"
   8.137 -proof -
   8.138 -  have "(\<lambda>x y. ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)})
   8.139 -    respects2 ratrel"
   8.140 -  by (rule equiv_ratrel [THEN congruent2_commuteI]) (simp_all add: left_distrib)
   8.141 -  with assms show ?thesis by (simp add: Fract_def add_rat_def UN_ratrel2)
   8.142 -qed
   8.143 -
   8.144 -definition
   8.145 -  minus_rat_def:
   8.146 -  "- q = Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel `` {(- fst x, snd x)})"
   8.147 -
   8.148 -lemma minus_rat [simp]: "- Fract a b = Fract (- a) b"
   8.149 -proof -
   8.150 -  have "(\<lambda>x. ratrel `` {(- fst x, snd x)}) respects ratrel"
   8.151 -    by (simp add: congruent_def)
   8.152 -  then show ?thesis by (simp add: Fract_def minus_rat_def UN_ratrel)
   8.153 -qed
   8.154 -
   8.155 -lemma minus_rat_cancel [simp]: "Fract (- a) (- b) = Fract a b"
   8.156 -  by (cases "b = 0") (simp_all add: eq_rat)
   8.157 -
   8.158 -definition
   8.159 -  diff_rat_def: "q - r = q + - (r::rat)"
   8.160 -
   8.161 -lemma diff_rat [simp]:
   8.162 -  assumes "b \<noteq> 0" and "d \<noteq> 0"
   8.163 -  shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)"
   8.164 -  using assms by (simp add: diff_rat_def)
   8.165 -
   8.166 -definition
   8.167 -  mult_rat_def:
   8.168 -  "q * r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
   8.169 -    ratrel``{(fst x * fst y, snd x * snd y)})"
   8.170 -
   8.171 -lemma mult_rat [simp]: "Fract a b * Fract c d = Fract (a * c) (b * d)"
   8.172 -proof -
   8.173 -  have "(\<lambda>x y. ratrel `` {(fst x * fst y, snd x * snd y)}) respects2 ratrel"
   8.174 -    by (rule equiv_ratrel [THEN congruent2_commuteI]) simp_all
   8.175 -  then show ?thesis by (simp add: Fract_def mult_rat_def UN_ratrel2)
   8.176 -qed
   8.177 -
   8.178 -lemma mult_rat_cancel:
   8.179 -  assumes "c \<noteq> 0"
   8.180 -  shows "Fract (c * a) (c * b) = Fract a b"
   8.181 -proof -
   8.182 -  from assms have "Fract c c = Fract 1 1" by (simp add: Fract_def)
   8.183 -  then show ?thesis by (simp add: mult_rat [symmetric])
   8.184 -qed
   8.185 -
   8.186 -instance proof
   8.187 -  fix q r s :: rat show "(q * r) * s = q * (r * s)" 
   8.188 -    by (cases q, cases r, cases s) (simp add: eq_rat)
   8.189 -next
   8.190 -  fix q r :: rat show "q * r = r * q"
   8.191 -    by (cases q, cases r) (simp add: eq_rat)
   8.192 -next
   8.193 -  fix q :: rat show "1 * q = q"
   8.194 -    by (cases q) (simp add: One_rat_def eq_rat)
   8.195 -next
   8.196 -  fix q r s :: rat show "(q + r) + s = q + (r + s)"
   8.197 -    by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps)
   8.198 -next
   8.199 -  fix q r :: rat show "q + r = r + q"
   8.200 -    by (cases q, cases r) (simp add: eq_rat)
   8.201 -next
   8.202 -  fix q :: rat show "0 + q = q"
   8.203 -    by (cases q) (simp add: Zero_rat_def eq_rat)
   8.204 -next
   8.205 -  fix q :: rat show "- q + q = 0"
   8.206 -    by (cases q) (simp add: Zero_rat_def eq_rat)
   8.207 -next
   8.208 -  fix q r :: rat show "q - r = q + - r"
   8.209 -    by (cases q, cases r) (simp add: eq_rat)
   8.210 -next
   8.211 -  fix q r s :: rat show "(q + r) * s = q * s + r * s"
   8.212 -    by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps)
   8.213 -next
   8.214 -  show "(0::rat) \<noteq> 1" by (simp add: Zero_rat_def One_rat_def eq_rat)
   8.215 -qed
   8.216 -
   8.217 -end
   8.218 -
   8.219 -lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1"
   8.220 -  by (induct k) (simp_all add: Zero_rat_def One_rat_def)
   8.221 -
   8.222 -lemma of_int_rat: "of_int k = Fract k 1"
   8.223 -  by (cases k rule: int_diff_cases) (simp add: of_nat_rat)
   8.224 -
   8.225 -lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k"
   8.226 -  by (rule of_nat_rat [symmetric])
   8.227 -
   8.228 -lemma Fract_of_int_eq: "Fract k 1 = of_int k"
   8.229 -  by (rule of_int_rat [symmetric])
   8.230 -
   8.231 -instantiation rat :: number_ring
   8.232 -begin
   8.233 -
   8.234 -definition
   8.235 -  rat_number_of_def: "number_of w = Fract w 1"
   8.236 -
   8.237 -instance proof
   8.238 -qed (simp add: rat_number_of_def of_int_rat)
   8.239 -
   8.240 -end
   8.241 -
   8.242 -lemma rat_number_collapse:
   8.243 -  "Fract 0 k = 0"
   8.244 -  "Fract 1 1 = 1"
   8.245 -  "Fract (number_of k) 1 = number_of k"
   8.246 -  "Fract k 0 = 0"
   8.247 -  by (cases "k = 0")
   8.248 -    (simp_all add: Zero_rat_def One_rat_def number_of_is_id number_of_eq of_int_rat eq_rat Fract_def)
   8.249 -
   8.250 -lemma rat_number_expand [code_unfold]:
   8.251 -  "0 = Fract 0 1"
   8.252 -  "1 = Fract 1 1"
   8.253 -  "number_of k = Fract (number_of k) 1"
   8.254 -  by (simp_all add: rat_number_collapse)
   8.255 -
   8.256 -lemma iszero_rat [simp]:
   8.257 -  "iszero (number_of k :: rat) \<longleftrightarrow> iszero (number_of k :: int)"
   8.258 -  by (simp add: iszero_def rat_number_expand number_of_is_id eq_rat)
   8.259 -
   8.260 -lemma Rat_cases_nonzero [case_names Fract 0]:
   8.261 -  assumes Fract: "\<And>a b. q = Fract a b \<Longrightarrow> b > 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> C"
   8.262 -  assumes 0: "q = 0 \<Longrightarrow> C"
   8.263 -  shows C
   8.264 -proof (cases "q = 0")
   8.265 -  case True then show C using 0 by auto
   8.266 -next
   8.267 -  case False
   8.268 -  then obtain a b where "q = Fract a b" and "b > 0" and "coprime a b" by (cases q) auto
   8.269 -  moreover with False have "0 \<noteq> Fract a b" by simp
   8.270 -  with `b > 0` have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat)
   8.271 -  with Fract `q = Fract a b` `b > 0` `coprime a b` show C by blast
   8.272 -qed
   8.273 -
   8.274 -subsubsection {* Function @{text normalize} *}
   8.275 -
   8.276 -lemma Fract_coprime: "Fract (a div gcd a b) (b div gcd a b) = Fract a b"
   8.277 -proof (cases "b = 0")
   8.278 -  case True then show ?thesis by (simp add: eq_rat)
   8.279 -next
   8.280 -  case False
   8.281 -  moreover have "b div gcd a b * gcd a b = b"
   8.282 -    by (rule dvd_div_mult_self) simp
   8.283 -  ultimately have "b div gcd a b \<noteq> 0" by auto
   8.284 -  with False show ?thesis by (simp add: eq_rat dvd_div_mult mult_commute [of a])
   8.285 -qed
   8.286 -
   8.287 -definition normalize :: "int \<times> int \<Rightarrow> int \<times> int" where
   8.288 -  "normalize p = (if snd p > 0 then (let a = gcd (fst p) (snd p) in (fst p div a, snd p div a))
   8.289 -    else if snd p = 0 then (0, 1)
   8.290 -    else (let a = - gcd (fst p) (snd p) in (fst p div a, snd p div a)))"
   8.291 -
   8.292 -lemma normalize_crossproduct:
   8.293 -  assumes "q \<noteq> 0" "s \<noteq> 0"
   8.294 -  assumes "normalize (p, q) = normalize (r, s)"
   8.295 -  shows "p * s = r * q"
   8.296 -proof -
   8.297 -  have aux: "p * gcd r s = sgn (q * s) * r * gcd p q \<Longrightarrow> q * gcd r s = sgn (q * s) * s * gcd p q \<Longrightarrow> p * s = q * r"
   8.298 -  proof -
   8.299 -    assume "p * gcd r s = sgn (q * s) * r * gcd p q" and "q * gcd r s = sgn (q * s) * s * gcd p q"
   8.300 -    then have "(p * gcd r s) * (sgn (q * s) * s * gcd p q) = (q * gcd r s) * (sgn (q * s) * r * gcd p q)" by simp
   8.301 -    with assms show "p * s = q * r" by (auto simp add: mult_ac sgn_times sgn_0_0)
   8.302 -  qed
   8.303 -  from assms show ?thesis
   8.304 -    by (auto simp add: normalize_def Let_def dvd_div_div_eq_mult mult_commute sgn_times split: if_splits intro: aux)
   8.305 -qed
   8.306 -
   8.307 -lemma normalize_eq: "normalize (a, b) = (p, q) \<Longrightarrow> Fract p q = Fract a b"
   8.308 -  by (auto simp add: normalize_def Let_def Fract_coprime dvd_div_neg rat_number_collapse
   8.309 -    split:split_if_asm)
   8.310 -
   8.311 -lemma normalize_denom_pos: "normalize r = (p, q) \<Longrightarrow> q > 0"
   8.312 -  by (auto simp add: normalize_def Let_def dvd_div_neg pos_imp_zdiv_neg_iff nonneg1_imp_zdiv_pos_iff
   8.313 -    split:split_if_asm)
   8.314 -
   8.315 -lemma normalize_coprime: "normalize r = (p, q) \<Longrightarrow> coprime p q"
   8.316 -  by (auto simp add: normalize_def Let_def dvd_div_neg div_gcd_coprime_int
   8.317 -    split:split_if_asm)
   8.318 -
   8.319 -lemma normalize_stable [simp]:
   8.320 -  "q > 0 \<Longrightarrow> coprime p q \<Longrightarrow> normalize (p, q) = (p, q)"
   8.321 -  by (simp add: normalize_def)
   8.322 -
   8.323 -lemma normalize_denom_zero [simp]:
   8.324 -  "normalize (p, 0) = (0, 1)"
   8.325 -  by (simp add: normalize_def)
   8.326 -
   8.327 -lemma normalize_negative [simp]:
   8.328 -  "q < 0 \<Longrightarrow> normalize (p, q) = normalize (- p, - q)"
   8.329 -  by (simp add: normalize_def Let_def dvd_div_neg dvd_neg_div)
   8.330 -
   8.331 -text{*
   8.332 -  Decompose a fraction into normalized, i.e. coprime numerator and denominator:
   8.333 -*}
   8.334 -
   8.335 -definition quotient_of :: "rat \<Rightarrow> int \<times> int" where
   8.336 -  "quotient_of x = (THE pair. x = Fract (fst pair) (snd pair) &
   8.337 -                   snd pair > 0 & coprime (fst pair) (snd pair))"
   8.338 -
   8.339 -lemma quotient_of_unique:
   8.340 -  "\<exists>!p. r = Fract (fst p) (snd p) \<and> snd p > 0 \<and> coprime (fst p) (snd p)"
   8.341 -proof (cases r)
   8.342 -  case (Fract a b)
   8.343 -  then have "r = Fract (fst (a, b)) (snd (a, b)) \<and> snd (a, b) > 0 \<and> coprime (fst (a, b)) (snd (a, b))" by auto
   8.344 -  then show ?thesis proof (rule ex1I)
   8.345 -    fix p
   8.346 -    obtain c d :: int where p: "p = (c, d)" by (cases p)
   8.347 -    assume "r = Fract (fst p) (snd p) \<and> snd p > 0 \<and> coprime (fst p) (snd p)"
   8.348 -    with p have Fract': "r = Fract c d" "d > 0" "coprime c d" by simp_all
   8.349 -    have "c = a \<and> d = b"
   8.350 -    proof (cases "a = 0")
   8.351 -      case True with Fract Fract' show ?thesis by (simp add: eq_rat)
   8.352 -    next
   8.353 -      case False
   8.354 -      with Fract Fract' have *: "c * b = a * d" and "c \<noteq> 0" by (auto simp add: eq_rat)
   8.355 -      then have "c * b > 0 \<longleftrightarrow> a * d > 0" by auto
   8.356 -      with `b > 0` `d > 0` have "a > 0 \<longleftrightarrow> c > 0" by (simp add: zero_less_mult_iff)
   8.357 -      with `a \<noteq> 0` `c \<noteq> 0` have sgn: "sgn a = sgn c" by (auto simp add: not_less)
   8.358 -      from `coprime a b` `coprime c d` have "\<bar>a\<bar> * \<bar>d\<bar> = \<bar>c\<bar> * \<bar>b\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>c\<bar> \<and> \<bar>d\<bar> = \<bar>b\<bar>"
   8.359 -        by (simp add: coprime_crossproduct_int)
   8.360 -      with `b > 0` `d > 0` have "\<bar>a\<bar> * d = \<bar>c\<bar> * b \<longleftrightarrow> \<bar>a\<bar> = \<bar>c\<bar> \<and> d = b" by simp
   8.361 -      then have "a * sgn a * d = c * sgn c * b \<longleftrightarrow> a * sgn a = c * sgn c \<and> d = b" by (simp add: abs_sgn)
   8.362 -      with sgn * show ?thesis by (auto simp add: sgn_0_0)
   8.363 -    qed
   8.364 -    with p show "p = (a, b)" by simp
   8.365 -  qed
   8.366 -qed
   8.367 -
   8.368 -lemma quotient_of_Fract [code]:
   8.369 -  "quotient_of (Fract a b) = normalize (a, b)"
   8.370 -proof -
   8.371 -  have "Fract a b = Fract (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?Fract)
   8.372 -    by (rule sym) (auto intro: normalize_eq)
   8.373 -  moreover have "0 < snd (normalize (a, b))" (is ?denom_pos) 
   8.374 -    by (cases "normalize (a, b)") (rule normalize_denom_pos, simp)
   8.375 -  moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime)
   8.376 -    by (rule normalize_coprime) simp
   8.377 -  ultimately have "?Fract \<and> ?denom_pos \<and> ?coprime" by blast
   8.378 -  with quotient_of_unique have
   8.379 -    "(THE p. Fract a b = Fract (fst p) (snd p) \<and> 0 < snd p \<and> coprime (fst p) (snd p)) = normalize (a, b)"
   8.380 -    by (rule the1_equality)
   8.381 -  then show ?thesis by (simp add: quotient_of_def)
   8.382 -qed
   8.383 -
   8.384 -lemma quotient_of_number [simp]:
   8.385 -  "quotient_of 0 = (0, 1)"
   8.386 -  "quotient_of 1 = (1, 1)"
   8.387 -  "quotient_of (number_of k) = (number_of k, 1)"
   8.388 -  by (simp_all add: rat_number_expand quotient_of_Fract)
   8.389 -
   8.390 -lemma quotient_of_eq: "quotient_of (Fract a b) = (p, q) \<Longrightarrow> Fract p q = Fract a b"
   8.391 -  by (simp add: quotient_of_Fract normalize_eq)
   8.392 -
   8.393 -lemma quotient_of_denom_pos: "quotient_of r = (p, q) \<Longrightarrow> q > 0"
   8.394 -  by (cases r) (simp add: quotient_of_Fract normalize_denom_pos)
   8.395 -
   8.396 -lemma quotient_of_coprime: "quotient_of r = (p, q) \<Longrightarrow> coprime p q"
   8.397 -  by (cases r) (simp add: quotient_of_Fract normalize_coprime)
   8.398 -
   8.399 -lemma quotient_of_inject:
   8.400 -  assumes "quotient_of a = quotient_of b"
   8.401 -  shows "a = b"
   8.402 -proof -
   8.403 -  obtain p q r s where a: "a = Fract p q"
   8.404 -    and b: "b = Fract r s"
   8.405 -    and "q > 0" and "s > 0" by (cases a, cases b)
   8.406 -  with assms show ?thesis by (simp add: eq_rat quotient_of_Fract normalize_crossproduct)
   8.407 -qed
   8.408 -
   8.409 -lemma quotient_of_inject_eq:
   8.410 -  "quotient_of a = quotient_of b \<longleftrightarrow> a = b"
   8.411 -  by (auto simp add: quotient_of_inject)
   8.412 -
   8.413 -
   8.414 -subsubsection {* The field of rational numbers *}
   8.415 -
   8.416 -instantiation rat :: "{field, division_by_zero}"
   8.417 -begin
   8.418 -
   8.419 -definition
   8.420 -  inverse_rat_def:
   8.421 -  "inverse q = Abs_Rat (\<Union>x \<in> Rep_Rat q.
   8.422 -     ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})"
   8.423 -
   8.424 -lemma inverse_rat [simp]: "inverse (Fract a b) = Fract b a"
   8.425 -proof -
   8.426 -  have "(\<lambda>x. ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)}) respects ratrel"
   8.427 -    by (auto simp add: congruent_def mult_commute)
   8.428 -  then show ?thesis by (simp add: Fract_def inverse_rat_def UN_ratrel)
   8.429 -qed
   8.430 -
   8.431 -definition
   8.432 -  divide_rat_def: "q / r = q * inverse (r::rat)"
   8.433 -
   8.434 -lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
   8.435 -  by (simp add: divide_rat_def)
   8.436 -
   8.437 -instance proof
   8.438 -  show "inverse 0 = (0::rat)" by (simp add: rat_number_expand)
   8.439 -    (simp add: rat_number_collapse)
   8.440 -next
   8.441 -  fix q :: rat
   8.442 -  assume "q \<noteq> 0"
   8.443 -  then show "inverse q * q = 1" by (cases q rule: Rat_cases_nonzero)
   8.444 -   (simp_all add: rat_number_expand eq_rat)
   8.445 -next
   8.446 -  fix q r :: rat
   8.447 -  show "q / r = q * inverse r" by (simp add: divide_rat_def)
   8.448 -qed
   8.449 -
   8.450 -end
   8.451 -
   8.452 -
   8.453 -subsubsection {* Various *}
   8.454 -
   8.455 -lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1"
   8.456 -  by (simp add: rat_number_expand)
   8.457 -
   8.458 -lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l"
   8.459 -  by (simp add: Fract_of_int_eq [symmetric])
   8.460 -
   8.461 -lemma Fract_number_of_quotient:
   8.462 -  "Fract (number_of k) (number_of l) = number_of k / number_of l"
   8.463 -  unfolding Fract_of_int_quotient number_of_is_id number_of_eq ..
   8.464 -
   8.465 -lemma Fract_1_number_of:
   8.466 -  "Fract 1 (number_of k) = 1 / number_of k"
   8.467 -  unfolding Fract_of_int_quotient number_of_eq by simp
   8.468 -
   8.469 -subsubsection {* The ordered field of rational numbers *}
   8.470 -
   8.471 -instantiation rat :: linorder
   8.472 -begin
   8.473 -
   8.474 -definition
   8.475 -  le_rat_def:
   8.476 -   "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
   8.477 -      {(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})"
   8.478 -
   8.479 -lemma le_rat [simp]:
   8.480 -  assumes "b \<noteq> 0" and "d \<noteq> 0"
   8.481 -  shows "Fract a b \<le> Fract c d \<longleftrightarrow> (a * d) * (b * d) \<le> (c * b) * (b * d)"
   8.482 -proof -
   8.483 -  have "(\<lambda>x y. {(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})
   8.484 -    respects2 ratrel"
   8.485 -  proof (clarsimp simp add: congruent2_def)
   8.486 -    fix a b a' b' c d c' d'::int
   8.487 -    assume neq: "b \<noteq> 0"  "b' \<noteq> 0"  "d \<noteq> 0"  "d' \<noteq> 0"
   8.488 -    assume eq1: "a * b' = a' * b"
   8.489 -    assume eq2: "c * d' = c' * d"
   8.490 -
   8.491 -    let ?le = "\<lambda>a b c d. ((a * d) * (b * d) \<le> (c * b) * (b * d))"
   8.492 -    {
   8.493 -      fix a b c d x :: int assume x: "x \<noteq> 0"
   8.494 -      have "?le a b c d = ?le (a * x) (b * x) c d"
   8.495 -      proof -
   8.496 -        from x have "0 < x * x" by (auto simp add: zero_less_mult_iff)
   8.497 -        hence "?le a b c d =
   8.498 -            ((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))"
   8.499 -          by (simp add: mult_le_cancel_right)
   8.500 -        also have "... = ?le (a * x) (b * x) c d"
   8.501 -          by (simp add: mult_ac)
   8.502 -        finally show ?thesis .
   8.503 -      qed
   8.504 -    } note le_factor = this
   8.505 -
   8.506 -    let ?D = "b * d" and ?D' = "b' * d'"
   8.507 -    from neq have D: "?D \<noteq> 0" by simp
   8.508 -    from neq have "?D' \<noteq> 0" by simp
   8.509 -    hence "?le a b c d = ?le (a * ?D') (b * ?D') c d"
   8.510 -      by (rule le_factor)
   8.511 -    also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')" 
   8.512 -      by (simp add: mult_ac)
   8.513 -    also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')"
   8.514 -      by (simp only: eq1 eq2)
   8.515 -    also have "... = ?le (a' * ?D) (b' * ?D) c' d'"
   8.516 -      by (simp add: mult_ac)
   8.517 -    also from D have "... = ?le a' b' c' d'"
   8.518 -      by (rule le_factor [symmetric])
   8.519 -    finally show "?le a b c d = ?le a' b' c' d'" .
   8.520 -  qed
   8.521 -  with assms show ?thesis by (simp add: Fract_def le_rat_def UN_ratrel2)
   8.522 -qed
   8.523 -
   8.524 -definition
   8.525 -  less_rat_def: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
   8.526 -
   8.527 -lemma less_rat [simp]:
   8.528 -  assumes "b \<noteq> 0" and "d \<noteq> 0"
   8.529 -  shows "Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)"
   8.530 -  using assms by (simp add: less_rat_def eq_rat order_less_le)
   8.531 -
   8.532 -instance proof
   8.533 -  fix q r s :: rat
   8.534 -  {
   8.535 -    assume "q \<le> r" and "r \<le> s"
   8.536 -    then show "q \<le> s" 
   8.537 -    proof (induct q, induct r, induct s)
   8.538 -      fix a b c d e f :: int
   8.539 -      assume neq: "b > 0"  "d > 0"  "f > 0"
   8.540 -      assume 1: "Fract a b \<le> Fract c d" and 2: "Fract c d \<le> Fract e f"
   8.541 -      show "Fract a b \<le> Fract e f"
   8.542 -      proof -
   8.543 -        from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f"
   8.544 -          by (auto simp add: zero_less_mult_iff linorder_neq_iff)
   8.545 -        have "(a * d) * (b * d) * (f * f) \<le> (c * b) * (b * d) * (f * f)"
   8.546 -        proof -
   8.547 -          from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)"
   8.548 -            by simp
   8.549 -          with ff show ?thesis by (simp add: mult_le_cancel_right)
   8.550 -        qed
   8.551 -        also have "... = (c * f) * (d * f) * (b * b)" by algebra
   8.552 -        also have "... \<le> (e * d) * (d * f) * (b * b)"
   8.553 -        proof -
   8.554 -          from neq 2 have "(c * f) * (d * f) \<le> (e * d) * (d * f)"
   8.555 -            by simp
   8.556 -          with bb show ?thesis by (simp add: mult_le_cancel_right)
   8.557 -        qed
   8.558 -        finally have "(a * f) * (b * f) * (d * d) \<le> e * b * (b * f) * (d * d)"
   8.559 -          by (simp only: mult_ac)
   8.560 -        with dd have "(a * f) * (b * f) \<le> (e * b) * (b * f)"
   8.561 -          by (simp add: mult_le_cancel_right)
   8.562 -        with neq show ?thesis by simp
   8.563 -      qed
   8.564 -    qed
   8.565 -  next
   8.566 -    assume "q \<le> r" and "r \<le> q"
   8.567 -    then show "q = r"
   8.568 -    proof (induct q, induct r)
   8.569 -      fix a b c d :: int
   8.570 -      assume neq: "b > 0"  "d > 0"
   8.571 -      assume 1: "Fract a b \<le> Fract c d" and 2: "Fract c d \<le> Fract a b"
   8.572 -      show "Fract a b = Fract c d"
   8.573 -      proof -
   8.574 -        from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)"
   8.575 -          by simp
   8.576 -        also have "... \<le> (a * d) * (b * d)"
   8.577 -        proof -
   8.578 -          from neq 2 have "(c * b) * (d * b) \<le> (a * d) * (d * b)"
   8.579 -            by simp
   8.580 -          thus ?thesis by (simp only: mult_ac)
   8.581 -        qed
   8.582 -        finally have "(a * d) * (b * d) = (c * b) * (b * d)" .
   8.583 -        moreover from neq have "b * d \<noteq> 0" by simp
   8.584 -        ultimately have "a * d = c * b" by simp
   8.585 -        with neq show ?thesis by (simp add: eq_rat)
   8.586 -      qed
   8.587 -    qed
   8.588 -  next
   8.589 -    show "q \<le> q"
   8.590 -      by (induct q) simp
   8.591 -    show "(q < r) = (q \<le> r \<and> \<not> r \<le> q)"
   8.592 -      by (induct q, induct r) (auto simp add: le_less mult_commute)
   8.593 -    show "q \<le> r \<or> r \<le> q"
   8.594 -      by (induct q, induct r)
   8.595 -         (simp add: mult_commute, rule linorder_linear)
   8.596 -  }
   8.597 -qed
   8.598 -
   8.599 -end
   8.600 -
   8.601 -instantiation rat :: "{distrib_lattice, abs_if, sgn_if}"
   8.602 -begin
   8.603 -
   8.604 -definition
   8.605 -  abs_rat_def: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))"
   8.606 -
   8.607 -lemma abs_rat [simp, code]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
   8.608 -  by (auto simp add: abs_rat_def zabs_def Zero_rat_def not_less le_less eq_rat zero_less_mult_iff)
   8.609 -
   8.610 -definition
   8.611 -  sgn_rat_def: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else - 1)"
   8.612 -
   8.613 -lemma sgn_rat [simp, code]: "sgn (Fract a b) = of_int (sgn a * sgn b)"
   8.614 -  unfolding Fract_of_int_eq
   8.615 -  by (auto simp: zsgn_def sgn_rat_def Zero_rat_def eq_rat)
   8.616 -    (auto simp: rat_number_collapse not_less le_less zero_less_mult_iff)
   8.617 -
   8.618 -definition
   8.619 -  "(inf \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat) = min"
   8.620 -
   8.621 -definition
   8.622 -  "(sup \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat) = max"
   8.623 -
   8.624 -instance by intro_classes
   8.625 -  (auto simp add: abs_rat_def sgn_rat_def min_max.sup_inf_distrib1 inf_rat_def sup_rat_def)
   8.626 -
   8.627 -end
   8.628 -
   8.629 -instance rat :: linordered_field
   8.630 -proof
   8.631 -  fix q r s :: rat
   8.632 -  show "q \<le> r ==> s + q \<le> s + r"
   8.633 -  proof (induct q, induct r, induct s)
   8.634 -    fix a b c d e f :: int
   8.635 -    assume neq: "b > 0"  "d > 0"  "f > 0"
   8.636 -    assume le: "Fract a b \<le> Fract c d"
   8.637 -    show "Fract e f + Fract a b \<le> Fract e f + Fract c d"
   8.638 -    proof -
   8.639 -      let ?F = "f * f" from neq have F: "0 < ?F"
   8.640 -        by (auto simp add: zero_less_mult_iff)
   8.641 -      from neq le have "(a * d) * (b * d) \<le> (c * b) * (b * d)"
   8.642 -        by simp
   8.643 -      with F have "(a * d) * (b * d) * ?F * ?F \<le> (c * b) * (b * d) * ?F * ?F"
   8.644 -        by (simp add: mult_le_cancel_right)
   8.645 -      with neq show ?thesis by (simp add: mult_ac int_distrib)
   8.646 -    qed
   8.647 -  qed
   8.648 -  show "q < r ==> 0 < s ==> s * q < s * r"
   8.649 -  proof (induct q, induct r, induct s)
   8.650 -    fix a b c d e f :: int
   8.651 -    assume neq: "b > 0"  "d > 0"  "f > 0"
   8.652 -    assume le: "Fract a b < Fract c d"
   8.653 -    assume gt: "0 < Fract e f"
   8.654 -    show "Fract e f * Fract a b < Fract e f * Fract c d"
   8.655 -    proof -
   8.656 -      let ?E = "e * f" and ?F = "f * f"
   8.657 -      from neq gt have "0 < ?E"
   8.658 -        by (auto simp add: Zero_rat_def order_less_le eq_rat)
   8.659 -      moreover from neq have "0 < ?F"
   8.660 -        by (auto simp add: zero_less_mult_iff)
   8.661 -      moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)"
   8.662 -        by simp
   8.663 -      ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F"
   8.664 -        by (simp add: mult_less_cancel_right)
   8.665 -      with neq show ?thesis
   8.666 -        by (simp add: mult_ac)
   8.667 -    qed
   8.668 -  qed
   8.669 -qed auto
   8.670 -
   8.671 -lemma Rat_induct_pos [case_names Fract, induct type: rat]:
   8.672 -  assumes step: "\<And>a b. 0 < b \<Longrightarrow> P (Fract a b)"
   8.673 -  shows "P q"
   8.674 -proof (cases q)
   8.675 -  have step': "\<And>a b. b < 0 \<Longrightarrow> P (Fract a b)"
   8.676 -  proof -
   8.677 -    fix a::int and b::int
   8.678 -    assume b: "b < 0"
   8.679 -    hence "0 < -b" by simp
   8.680 -    hence "P (Fract (-a) (-b))" by (rule step)
   8.681 -    thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b])
   8.682 -  qed
   8.683 -  case (Fract a b)
   8.684 -  thus "P q" by (force simp add: linorder_neq_iff step step')
   8.685 -qed
   8.686 -
   8.687 -lemma zero_less_Fract_iff:
   8.688 -  "0 < b \<Longrightarrow> 0 < Fract a b \<longleftrightarrow> 0 < a"
   8.689 -  by (simp add: Zero_rat_def zero_less_mult_iff)
   8.690 -
   8.691 -lemma Fract_less_zero_iff:
   8.692 -  "0 < b \<Longrightarrow> Fract a b < 0 \<longleftrightarrow> a < 0"
   8.693 -  by (simp add: Zero_rat_def mult_less_0_iff)
   8.694 -
   8.695 -lemma zero_le_Fract_iff:
   8.696 -  "0 < b \<Longrightarrow> 0 \<le> Fract a b \<longleftrightarrow> 0 \<le> a"
   8.697 -  by (simp add: Zero_rat_def zero_le_mult_iff)
   8.698 -
   8.699 -lemma Fract_le_zero_iff:
   8.700 -  "0 < b \<Longrightarrow> Fract a b \<le> 0 \<longleftrightarrow> a \<le> 0"
   8.701 -  by (simp add: Zero_rat_def mult_le_0_iff)
   8.702 -
   8.703 -lemma one_less_Fract_iff:
   8.704 -  "0 < b \<Longrightarrow> 1 < Fract a b \<longleftrightarrow> b < a"
   8.705 -  by (simp add: One_rat_def mult_less_cancel_right_disj)
   8.706 -
   8.707 -lemma Fract_less_one_iff:
   8.708 -  "0 < b \<Longrightarrow> Fract a b < 1 \<longleftrightarrow> a < b"
   8.709 -  by (simp add: One_rat_def mult_less_cancel_right_disj)
   8.710 -
   8.711 -lemma one_le_Fract_iff:
   8.712 -  "0 < b \<Longrightarrow> 1 \<le> Fract a b \<longleftrightarrow> b \<le> a"
   8.713 -  by (simp add: One_rat_def mult_le_cancel_right)
   8.714 -
   8.715 -lemma Fract_le_one_iff:
   8.716 -  "0 < b \<Longrightarrow> Fract a b \<le> 1 \<longleftrightarrow> a \<le> b"
   8.717 -  by (simp add: One_rat_def mult_le_cancel_right)
   8.718 -
   8.719 -
   8.720 -subsubsection {* Rationals are an Archimedean field *}
   8.721 -
   8.722 -lemma rat_floor_lemma:
   8.723 -  shows "of_int (a div b) \<le> Fract a b \<and> Fract a b < of_int (a div b + 1)"
   8.724 -proof -
   8.725 -  have "Fract a b = of_int (a div b) + Fract (a mod b) b"
   8.726 -    by (cases "b = 0", simp, simp add: of_int_rat)
   8.727 -  moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1"
   8.728 -    unfolding Fract_of_int_quotient
   8.729 -    by (rule linorder_cases [of b 0])
   8.730 -       (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos)
   8.731 -  ultimately show ?thesis by simp
   8.732 -qed
   8.733 -
   8.734 -instance rat :: archimedean_field
   8.735 -proof
   8.736 -  fix r :: rat
   8.737 -  show "\<exists>z. r \<le> of_int z"
   8.738 -  proof (induct r)
   8.739 -    case (Fract a b)
   8.740 -    have "Fract a b \<le> of_int (a div b + 1)"
   8.741 -      using rat_floor_lemma [of a b] by simp
   8.742 -    then show "\<exists>z. Fract a b \<le> of_int z" ..
   8.743 -  qed
   8.744 -qed
   8.745 -
   8.746 -lemma floor_Fract: "floor (Fract a b) = a div b"
   8.747 -  using rat_floor_lemma [of a b]
   8.748 -  by (simp add: floor_unique)
   8.749 -
   8.750 -
   8.751 -subsection {* Linear arithmetic setup *}
   8.752 -
   8.753 -declaration {*
   8.754 -  K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
   8.755 -    (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *)
   8.756 -  #> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_int_eq_iff} RS iffD2]
   8.757 -    (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
   8.758 -  #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
   8.759 -      @{thm True_implies_equals},
   8.760 -      read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
   8.761 -      @{thm divide_1}, @{thm divide_zero_left},
   8.762 -      @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
   8.763 -      @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
   8.764 -      @{thm of_int_minus}, @{thm of_int_diff},
   8.765 -      @{thm of_int_of_nat_eq}]
   8.766 -  #> Lin_Arith.add_simprocs Numeral_Simprocs.field_cancel_numeral_factors
   8.767 -  #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"})
   8.768 -  #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"}))
   8.769 -*}
   8.770 -
   8.771 -
   8.772 -subsection {* Embedding from Rationals to other Fields *}
   8.773 -
   8.774 -class field_char_0 = field + ring_char_0
   8.775 -
   8.776 -subclass (in linordered_field) field_char_0 ..
   8.777 -
   8.778 -context field_char_0
   8.779 -begin
   8.780 -
   8.781 -definition of_rat :: "rat \<Rightarrow> 'a" where
   8.782 -  "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
   8.783 -
   8.784 -end
   8.785 -
   8.786 -lemma of_rat_congruent:
   8.787 -  "(\<lambda>(a, b). {of_int a / of_int b :: 'a::field_char_0}) respects ratrel"
   8.788 -apply (rule congruent.intro)
   8.789 -apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq)
   8.790 -apply (simp only: of_int_mult [symmetric])
   8.791 -done
   8.792 -
   8.793 -lemma of_rat_rat: "b \<noteq> 0 \<Longrightarrow> of_rat (Fract a b) = of_int a / of_int b"
   8.794 -  unfolding Fract_def of_rat_def by (simp add: UN_ratrel of_rat_congruent)
   8.795 -
   8.796 -lemma of_rat_0 [simp]: "of_rat 0 = 0"
   8.797 -by (simp add: Zero_rat_def of_rat_rat)
   8.798 -
   8.799 -lemma of_rat_1 [simp]: "of_rat 1 = 1"
   8.800 -by (simp add: One_rat_def of_rat_rat)
   8.801 -
   8.802 -lemma of_rat_add: "of_rat (a + b) = of_rat a + of_rat b"
   8.803 -by (induct a, induct b, simp add: of_rat_rat add_frac_eq)
   8.804 -
   8.805 -lemma of_rat_minus: "of_rat (- a) = - of_rat a"
   8.806 -by (induct a, simp add: of_rat_rat)
   8.807 -
   8.808 -lemma of_rat_diff: "of_rat (a - b) = of_rat a - of_rat b"
   8.809 -by (simp only: diff_minus of_rat_add of_rat_minus)
   8.810 -
   8.811 -lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b"
   8.812 -apply (induct a, induct b, simp add: of_rat_rat)
   8.813 -apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac)
   8.814 -done
   8.815 -
   8.816 -lemma nonzero_of_rat_inverse:
   8.817 -  "a \<noteq> 0 \<Longrightarrow> of_rat (inverse a) = inverse (of_rat a)"
   8.818 -apply (rule inverse_unique [symmetric])
   8.819 -apply (simp add: of_rat_mult [symmetric])
   8.820 -done
   8.821 -
   8.822 -lemma of_rat_inverse:
   8.823 -  "(of_rat (inverse a)::'a::{field_char_0,division_by_zero}) =
   8.824 -   inverse (of_rat a)"
   8.825 -by (cases "a = 0", simp_all add: nonzero_of_rat_inverse)
   8.826 -
   8.827 -lemma nonzero_of_rat_divide:
   8.828 -  "b \<noteq> 0 \<Longrightarrow> of_rat (a / b) = of_rat a / of_rat b"
   8.829 -by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse)
   8.830 -
   8.831 -lemma of_rat_divide:
   8.832 -  "(of_rat (a / b)::'a::{field_char_0,division_by_zero})
   8.833 -   = of_rat a / of_rat b"
   8.834 -by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
   8.835 -
   8.836 -lemma of_rat_power:
   8.837 -  "(of_rat (a ^ n)::'a::field_char_0) = of_rat a ^ n"
   8.838 -by (induct n) (simp_all add: of_rat_mult)
   8.839 -
   8.840 -lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)"
   8.841 -apply (induct a, induct b)
   8.842 -apply (simp add: of_rat_rat eq_rat)
   8.843 -apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq)
   8.844 -apply (simp only: of_int_mult [symmetric] of_int_eq_iff)
   8.845 -done
   8.846 -
   8.847 -lemma of_rat_less:
   8.848 -  "(of_rat r :: 'a::linordered_field) < of_rat s \<longleftrightarrow> r < s"
   8.849 -proof (induct r, induct s)
   8.850 -  fix a b c d :: int
   8.851 -  assume not_zero: "b > 0" "d > 0"
   8.852 -  then have "b * d > 0" by (rule mult_pos_pos)
   8.853 -  have of_int_divide_less_eq:
   8.854 -    "(of_int a :: 'a) / of_int b < of_int c / of_int d
   8.855 -      \<longleftrightarrow> (of_int a :: 'a) * of_int d < of_int c * of_int b"
   8.856 -    using not_zero by (simp add: pos_less_divide_eq pos_divide_less_eq)
   8.857 -  show "(of_rat (Fract a b) :: 'a::linordered_field) < of_rat (Fract c d)
   8.858 -    \<longleftrightarrow> Fract a b < Fract c d"
   8.859 -    using not_zero `b * d > 0`
   8.860 -    by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult)
   8.861 -qed
   8.862 -
   8.863 -lemma of_rat_less_eq:
   8.864 -  "(of_rat r :: 'a::linordered_field) \<le> of_rat s \<longleftrightarrow> r \<le> s"
   8.865 -  unfolding le_less by (auto simp add: of_rat_less)
   8.866 -
   8.867 -lemmas of_rat_eq_0_iff [simp] = of_rat_eq_iff [of _ 0, simplified]
   8.868 -
   8.869 -lemma of_rat_eq_id [simp]: "of_rat = id"
   8.870 -proof
   8.871 -  fix a
   8.872 -  show "of_rat a = id a"
   8.873 -  by (induct a)
   8.874 -     (simp add: of_rat_rat Fract_of_int_eq [symmetric])
   8.875 -qed
   8.876 -
   8.877 -text{*Collapse nested embeddings*}
   8.878 -lemma of_rat_of_nat_eq [simp]: "of_rat (of_nat n) = of_nat n"
   8.879 -by (induct n) (simp_all add: of_rat_add)
   8.880 -
   8.881 -lemma of_rat_of_int_eq [simp]: "of_rat (of_int z) = of_int z"
   8.882 -by (cases z rule: int_diff_cases) (simp add: of_rat_diff)
   8.883 -
   8.884 -lemma of_rat_number_of_eq [simp]:
   8.885 -  "of_rat (number_of w) = (number_of w :: 'a::{number_ring,field_char_0})"
   8.886 -by (simp add: number_of_eq)
   8.887 -
   8.888 -lemmas zero_rat = Zero_rat_def
   8.889 -lemmas one_rat = One_rat_def
   8.890 -
   8.891 -abbreviation
   8.892 -  rat_of_nat :: "nat \<Rightarrow> rat"
   8.893 -where
   8.894 -  "rat_of_nat \<equiv> of_nat"
   8.895 -
   8.896 -abbreviation
   8.897 -  rat_of_int :: "int \<Rightarrow> rat"
   8.898 -where
   8.899 -  "rat_of_int \<equiv> of_int"
   8.900 -
   8.901 -subsection {* The Set of Rational Numbers *}
   8.902 -
   8.903 -context field_char_0
   8.904 -begin
   8.905 -
   8.906 -definition
   8.907 -  Rats  :: "'a set" where
   8.908 -  "Rats = range of_rat"
   8.909 -
   8.910 -notation (xsymbols)
   8.911 -  Rats  ("\<rat>")
   8.912 -
   8.913 -end
   8.914 -
   8.915 -lemma Rats_of_rat [simp]: "of_rat r \<in> Rats"
   8.916 -by (simp add: Rats_def)
   8.917 -
   8.918 -lemma Rats_of_int [simp]: "of_int z \<in> Rats"
   8.919 -by (subst of_rat_of_int_eq [symmetric], rule Rats_of_rat)
   8.920 -
   8.921 -lemma Rats_of_nat [simp]: "of_nat n \<in> Rats"
   8.922 -by (subst of_rat_of_nat_eq [symmetric], rule Rats_of_rat)
   8.923 -
   8.924 -lemma Rats_number_of [simp]:
   8.925 -  "(number_of w::'a::{number_ring,field_char_0}) \<in> Rats"
   8.926 -by (subst of_rat_number_of_eq [symmetric], rule Rats_of_rat)
   8.927 -
   8.928 -lemma Rats_0 [simp]: "0 \<in> Rats"
   8.929 -apply (unfold Rats_def)
   8.930 -apply (rule range_eqI)
   8.931 -apply (rule of_rat_0 [symmetric])
   8.932 -done
   8.933 -
   8.934 -lemma Rats_1 [simp]: "1 \<in> Rats"
   8.935 -apply (unfold Rats_def)
   8.936 -apply (rule range_eqI)
   8.937 -apply (rule of_rat_1 [symmetric])
   8.938 -done
   8.939 -
   8.940 -lemma Rats_add [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a + b \<in> Rats"
   8.941 -apply (auto simp add: Rats_def)
   8.942 -apply (rule range_eqI)
   8.943 -apply (rule of_rat_add [symmetric])
   8.944 -done
   8.945 -
   8.946 -lemma Rats_minus [simp]: "a \<in> Rats \<Longrightarrow> - a \<in> Rats"
   8.947 -apply (auto simp add: Rats_def)
   8.948 -apply (rule range_eqI)
   8.949 -apply (rule of_rat_minus [symmetric])
   8.950 -done
   8.951 -
   8.952 -lemma Rats_diff [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a - b \<in> Rats"
   8.953 -apply (auto simp add: Rats_def)
   8.954 -apply (rule range_eqI)
   8.955 -apply (rule of_rat_diff [symmetric])
   8.956 -done
   8.957 -
   8.958 -lemma Rats_mult [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a * b \<in> Rats"
   8.959 -apply (auto simp add: Rats_def)
   8.960 -apply (rule range_eqI)
   8.961 -apply (rule of_rat_mult [symmetric])
   8.962 -done
   8.963 -
   8.964 -lemma nonzero_Rats_inverse:
   8.965 -  fixes a :: "'a::field_char_0"
   8.966 -  shows "\<lbrakk>a \<in> Rats; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> Rats"
   8.967 -apply (auto simp add: Rats_def)
   8.968 -apply (rule range_eqI)
   8.969 -apply (erule nonzero_of_rat_inverse [symmetric])
   8.970 -done
   8.971 -
   8.972 -lemma Rats_inverse [simp]:
   8.973 -  fixes a :: "'a::{field_char_0,division_by_zero}"
   8.974 -  shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats"
   8.975 -apply (auto simp add: Rats_def)
   8.976 -apply (rule range_eqI)
   8.977 -apply (rule of_rat_inverse [symmetric])
   8.978 -done
   8.979 -
   8.980 -lemma nonzero_Rats_divide:
   8.981 -  fixes a b :: "'a::field_char_0"
   8.982 -  shows "\<lbrakk>a \<in> Rats; b \<in> Rats; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
   8.983 -apply (auto simp add: Rats_def)
   8.984 -apply (rule range_eqI)
   8.985 -apply (erule nonzero_of_rat_divide [symmetric])
   8.986 -done
   8.987 -
   8.988 -lemma Rats_divide [simp]:
   8.989 -  fixes a b :: "'a::{field_char_0,division_by_zero}"
   8.990 -  shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
   8.991 -apply (auto simp add: Rats_def)
   8.992 -apply (rule range_eqI)
   8.993 -apply (rule of_rat_divide [symmetric])
   8.994 -done
   8.995 -
   8.996 -lemma Rats_power [simp]:
   8.997 -  fixes a :: "'a::field_char_0"
   8.998 -  shows "a \<in> Rats \<Longrightarrow> a ^ n \<in> Rats"
   8.999 -apply (auto simp add: Rats_def)
  8.1000 -apply (rule range_eqI)
  8.1001 -apply (rule of_rat_power [symmetric])
  8.1002 -done
  8.1003 -
  8.1004 -lemma Rats_cases [cases set: Rats]:
  8.1005 -  assumes "q \<in> \<rat>"
  8.1006 -  obtains (of_rat) r where "q = of_rat r"
  8.1007 -  unfolding Rats_def
  8.1008 -proof -
  8.1009 -  from `q \<in> \<rat>` have "q \<in> range of_rat" unfolding Rats_def .
  8.1010 -  then obtain r where "q = of_rat r" ..
  8.1011 -  then show thesis ..
  8.1012 -qed
  8.1013 -
  8.1014 -lemma Rats_induct [case_names of_rat, induct set: Rats]:
  8.1015 -  "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
  8.1016 -  by (rule Rats_cases) auto
  8.1017 -
  8.1018 -
  8.1019 -subsection {* Implementation of rational numbers as pairs of integers *}
  8.1020 -
  8.1021 -definition Frct :: "int \<times> int \<Rightarrow> rat" where
  8.1022 -  [simp]: "Frct p = Fract (fst p) (snd p)"
  8.1023 -
  8.1024 -code_abstype Frct quotient_of
  8.1025 -proof (rule eq_reflection)
  8.1026 -  show "Frct (quotient_of x) = x" by (cases x) (auto intro: quotient_of_eq)
  8.1027 -qed
  8.1028 -
  8.1029 -lemma Frct_code_post [code_post]:
  8.1030 -  "Frct (0, k) = 0"
  8.1031 -  "Frct (k, 0) = 0"
  8.1032 -  "Frct (1, 1) = 1"
  8.1033 -  "Frct (number_of k, 1) = number_of k"
  8.1034 -  "Frct (1, number_of k) = 1 / number_of k"
  8.1035 -  "Frct (number_of k, number_of l) = number_of k / number_of l"
  8.1036 -  by (simp_all add: rat_number_collapse Fract_number_of_quotient Fract_1_number_of)
  8.1037 -
  8.1038 -declare quotient_of_Fract [code abstract]
  8.1039 -
  8.1040 -lemma rat_zero_code [code abstract]:
  8.1041 -  "quotient_of 0 = (0, 1)"
  8.1042 -  by (simp add: Zero_rat_def quotient_of_Fract normalize_def)
  8.1043 -
  8.1044 -lemma rat_one_code [code abstract]:
  8.1045 -  "quotient_of 1 = (1, 1)"
  8.1046 -  by (simp add: One_rat_def quotient_of_Fract normalize_def)
  8.1047 -
  8.1048 -lemma rat_plus_code [code abstract]:
  8.1049 -  "quotient_of (p + q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q
  8.1050 -     in normalize (a * d + b * c, c * d))"
  8.1051 -  by (cases p, cases q) (simp add: quotient_of_Fract)
  8.1052 -
  8.1053 -lemma rat_uminus_code [code abstract]:
  8.1054 -  "quotient_of (- p) = (let (a, b) = quotient_of p in (- a, b))"
  8.1055 -  by (cases p) (simp add: quotient_of_Fract)
  8.1056 -
  8.1057 -lemma rat_minus_code [code abstract]:
  8.1058 -  "quotient_of (p - q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q
  8.1059 -     in normalize (a * d - b * c, c * d))"
  8.1060 -  by (cases p, cases q) (simp add: quotient_of_Fract)
  8.1061 -
  8.1062 -lemma rat_times_code [code abstract]:
  8.1063 -  "quotient_of (p * q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q
  8.1064 -     in normalize (a * b, c * d))"
  8.1065 -  by (cases p, cases q) (simp add: quotient_of_Fract)
  8.1066 -
  8.1067 -lemma rat_inverse_code [code abstract]:
  8.1068 -  "quotient_of (inverse p) = (let (a, b) = quotient_of p
  8.1069 -    in if a = 0 then (0, 1) else (sgn a * b, \<bar>a\<bar>))"
  8.1070 -proof (cases p)
  8.1071 -  case (Fract a b) then show ?thesis
  8.1072 -    by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract gcd_int.commute)
  8.1073 -qed
  8.1074 -
  8.1075 -lemma rat_divide_code [code abstract]:
  8.1076 -  "quotient_of (p / q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q
  8.1077 -     in normalize (a * d, c * b))"
  8.1078 -  by (cases p, cases q) (simp add: quotient_of_Fract)
  8.1079 -
  8.1080 -lemma rat_abs_code [code abstract]:
  8.1081 -  "quotient_of \<bar>p\<bar> = (let (a, b) = quotient_of p in (\<bar>a\<bar>, b))"
  8.1082 -  by (cases p) (simp add: quotient_of_Fract)
  8.1083 -
  8.1084 -lemma rat_sgn_code [code abstract]:
  8.1085 -  "quotient_of (sgn p) = (sgn (fst (quotient_of p)), 1)"
  8.1086 -proof (cases p)
  8.1087 -  case (Fract a b) then show ?thesis
  8.1088 -  by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract)
  8.1089 -qed
  8.1090 -
  8.1091 -instantiation rat :: eq
  8.1092 -begin
  8.1093 -
  8.1094 -definition [code]:
  8.1095 -  "eq_class.eq a b \<longleftrightarrow> quotient_of a = quotient_of b"
  8.1096 -
  8.1097 -instance proof
  8.1098 -qed (simp add: eq_rat_def quotient_of_inject_eq)
  8.1099 -
  8.1100 -lemma rat_eq_refl [code nbe]:
  8.1101 -  "eq_class.eq (r::rat) r \<longleftrightarrow> True"
  8.1102 -  by (rule HOL.eq_refl)
  8.1103 -
  8.1104 -end
  8.1105 -
  8.1106 -lemma rat_less_eq_code [code]:
  8.1107 -  "p \<le> q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d \<le> c * b)"
  8.1108 -  by (cases p, cases q) (simp add: quotient_of_Fract times.commute)
  8.1109 -
  8.1110 -lemma rat_less_code [code]:
  8.1111 -  "p < q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d < c * b)"
  8.1112 -  by (cases p, cases q) (simp add: quotient_of_Fract times.commute)
  8.1113 -
  8.1114 -lemma [code]:
  8.1115 -  "of_rat p = (let (a, b) = quotient_of p in of_int a / of_int b)"
  8.1116 -  by (cases p) (simp add: quotient_of_Fract of_rat_rat)
  8.1117 -
  8.1118 -definition (in term_syntax)
  8.1119 -  valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
  8.1120 -  [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l"
  8.1121 -
  8.1122 -notation fcomp (infixl "o>" 60)
  8.1123 -notation scomp (infixl "o\<rightarrow>" 60)
  8.1124 -
  8.1125 -instantiation rat :: random
  8.1126 -begin
  8.1127 -
  8.1128 -definition
  8.1129 -  "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
  8.1130 -     let j = Code_Numeral.int_of (denom + 1)
  8.1131 -     in valterm_fract num (j, \<lambda>u. Code_Evaluation.term_of j))))"
  8.1132 -
  8.1133 -instance ..
  8.1134 -
  8.1135 -end
  8.1136 -
  8.1137 -no_notation fcomp (infixl "o>" 60)
  8.1138 -no_notation scomp (infixl "o\<rightarrow>" 60)
  8.1139 -
  8.1140 -text {* Setup for SML code generator *}
  8.1141 -
  8.1142 -types_code
  8.1143 -  rat ("(int */ int)")
  8.1144 -attach (term_of) {*
  8.1145 -fun term_of_rat (p, q) =
  8.1146 -  let
  8.1147 -    val rT = Type ("Rational.rat", [])
  8.1148 -  in
  8.1149 -    if q = 1 orelse p = 0 then HOLogic.mk_number rT p
  8.1150 -    else @{term "op / \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"} $
  8.1151 -      HOLogic.mk_number rT p $ HOLogic.mk_number rT q
  8.1152 -  end;
  8.1153 -*}
  8.1154 -attach (test) {*
  8.1155 -fun gen_rat i =
  8.1156 -  let
  8.1157 -    val p = random_range 0 i;
  8.1158 -    val q = random_range 1 (i + 1);
  8.1159 -    val g = Integer.gcd p q;
  8.1160 -    val p' = p div g;
  8.1161 -    val q' = q div g;
  8.1162 -    val r = (if one_of [true, false] then p' else ~ p',
  8.1163 -      if p' = 0 then 1 else q')
  8.1164 -  in
  8.1165 -    (r, fn () => term_of_rat r)
  8.1166 -  end;
  8.1167 -*}
  8.1168 -
  8.1169 -consts_code
  8.1170 -  Fract ("(_,/ _)")
  8.1171 -
  8.1172 -consts_code
  8.1173 -  "of_int :: int \<Rightarrow> rat" ("\<module>rat'_of'_int")
  8.1174 -attach {*
  8.1175 -fun rat_of_int i = (i, 1);
  8.1176 -*}
  8.1177 -
  8.1178 -setup {*
  8.1179 -  Nitpick.register_frac_type @{type_name rat}
  8.1180 -   [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
  8.1181 -    (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
  8.1182 -    (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
  8.1183 -    (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}),
  8.1184 -    (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
  8.1185 -    (@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}),
  8.1186 -    (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
  8.1187 -    (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
  8.1188 -    (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
  8.1189 -    (@{const_name field_char_0_class.Rats}, @{const_name UNIV})]
  8.1190 -*}
  8.1191 -
  8.1192 -lemmas [nitpick_def] = inverse_rat_inst.inverse_rat
  8.1193 -  number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat
  8.1194 -  plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
  8.1195 -  zero_rat_inst.zero_rat
  8.1196 -
  8.1197 -end
     9.1 --- a/src/HOL/ex/NormalForm.thy	Wed Feb 24 14:19:54 2010 +0100
     9.2 +++ b/src/HOL/ex/NormalForm.thy	Wed Feb 24 14:34:40 2010 +0100
     9.3 @@ -3,7 +3,7 @@
     9.4  header {* Testing implementation of normalization by evaluation *}
     9.5  
     9.6  theory NormalForm
     9.7 -imports Main Rational
     9.8 +imports Complex_Main
     9.9  begin
    9.10  
    9.11  lemma "True" by normalization