src/HOL/Rat.thy
changeset 47906 09a896d295bd
parent 47108 2a1953f0d20d
child 47907 54e3847f1669
     1.1 --- a/src/HOL/Rat.thy	Thu May 10 16:56:23 2012 +0200
     1.2 +++ b/src/HOL/Rat.thy	Thu May 10 21:18:41 2012 +0200
     1.3 @@ -14,24 +14,24 @@
     1.4  subsubsection {* Construction of the type of rational numbers *}
     1.5  
     1.6  definition
     1.7 -  ratrel :: "((int \<times> int) \<times> (int \<times> int)) set" where
     1.8 -  "ratrel = {(x, y). snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x}"
     1.9 +  ratrel :: "(int \<times> int) \<Rightarrow> (int \<times> int) \<Rightarrow> bool" where
    1.10 +  "ratrel = (\<lambda>x y. snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x)"
    1.11  
    1.12  lemma ratrel_iff [simp]:
    1.13 -  "(x, y) \<in> ratrel \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x"
    1.14 +  "ratrel x y \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x"
    1.15    by (simp add: ratrel_def)
    1.16  
    1.17 -lemma refl_on_ratrel: "refl_on {x. snd x \<noteq> 0} ratrel"
    1.18 -  by (auto simp add: refl_on_def ratrel_def)
    1.19 +lemma exists_ratrel_refl: "\<exists>x. ratrel x x"
    1.20 +  by (auto intro!: one_neq_zero)
    1.21  
    1.22 -lemma sym_ratrel: "sym ratrel"
    1.23 -  by (simp add: ratrel_def sym_def)
    1.24 +lemma symp_ratrel: "symp ratrel"
    1.25 +  by (simp add: ratrel_def symp_def)
    1.26  
    1.27 -lemma trans_ratrel: "trans ratrel"
    1.28 -proof (rule transI, unfold split_paired_all)
    1.29 +lemma transp_ratrel: "transp ratrel"
    1.30 +proof (rule transpI, unfold split_paired_all)
    1.31    fix a b a' b' a'' b'' :: int
    1.32 -  assume A: "((a, b), (a', b')) \<in> ratrel"
    1.33 -  assume B: "((a', b'), (a'', b'')) \<in> ratrel"
    1.34 +  assume A: "ratrel (a, b) (a', b')"
    1.35 +  assume B: "ratrel (a', b') (a'', b'')"
    1.36    have "b' * (a * b'') = b'' * (a * b')" by simp
    1.37    also from A have "a * b' = a' * b" by auto
    1.38    also have "b'' * (a' * b) = b * (a' * b'')" by simp
    1.39 @@ -40,54 +40,42 @@
    1.40    finally have "b' * (a * b'') = b' * (a'' * b)" .
    1.41    moreover from B have "b' \<noteq> 0" by auto
    1.42    ultimately have "a * b'' = a'' * b" by simp
    1.43 -  with A B show "((a, b), (a'', b'')) \<in> ratrel" by auto
    1.44 -qed
    1.45 -  
    1.46 -lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel"
    1.47 -  by (rule equivI [OF refl_on_ratrel sym_ratrel trans_ratrel])
    1.48 -
    1.49 -lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel]
    1.50 -lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel]
    1.51 -
    1.52 -lemma equiv_ratrel_iff [iff]: 
    1.53 -  assumes "snd x \<noteq> 0" and "snd y \<noteq> 0"
    1.54 -  shows "ratrel `` {x} = ratrel `` {y} \<longleftrightarrow> (x, y) \<in> ratrel"
    1.55 -  by (rule eq_equiv_class_iff, rule equiv_ratrel) (auto simp add: assms)
    1.56 -
    1.57 -definition "Rat = {x. snd x \<noteq> 0} // ratrel"
    1.58 -
    1.59 -typedef (open) rat = Rat
    1.60 -  morphisms Rep_Rat Abs_Rat
    1.61 -  unfolding Rat_def
    1.62 -proof
    1.63 -  have "(0::int, 1::int) \<in> {x. snd x \<noteq> 0}" by simp
    1.64 -  then show "ratrel `` {(0, 1)} \<in> {x. snd x \<noteq> 0} // ratrel" by (rule quotientI)
    1.65 +  with A B show "ratrel (a, b) (a'', b'')" by auto
    1.66  qed
    1.67  
    1.68 -lemma ratrel_in_Rat [simp]: "snd x \<noteq> 0 \<Longrightarrow> ratrel `` {x} \<in> Rat"
    1.69 -  by (simp add: Rat_def quotientI)
    1.70 +lemma part_equivp_ratrel: "part_equivp ratrel"
    1.71 +  by (rule part_equivpI [OF exists_ratrel_refl symp_ratrel transp_ratrel])
    1.72 +
    1.73 +quotient_type rat = "int \<times> int" / partial: "ratrel"
    1.74 +  morphisms Rep_Rat Abs_Rat
    1.75 +  by (rule part_equivp_ratrel)
    1.76  
    1.77 -declare Abs_Rat_inject [simp] Abs_Rat_inverse [simp]
    1.78 +declare rat.forall_transfer [transfer_rule del]
    1.79 +
    1.80 +lemma forall_rat_transfer [transfer_rule]: (* TODO: generate automatically *)
    1.81 +  "(fun_rel (fun_rel cr_rat op =) op =)
    1.82 +    (transfer_bforall (\<lambda>x. snd x \<noteq> 0)) transfer_forall"
    1.83 +  using rat.forall_transfer by simp
    1.84  
    1.85  
    1.86  subsubsection {* Representation and basic operations *}
    1.87  
    1.88 -definition
    1.89 -  Fract :: "int \<Rightarrow> int \<Rightarrow> rat" where
    1.90 -  "Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})"
    1.91 +lift_definition Fract :: "int \<Rightarrow> int \<Rightarrow> rat"
    1.92 +  is "\<lambda>a b. if b = 0 then (0, 1) else (a, b)"
    1.93 +  by simp
    1.94  
    1.95  lemma eq_rat:
    1.96    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"
    1.97    and "\<And>a. Fract a 0 = Fract 0 1"
    1.98    and "\<And>a c. Fract 0 a = Fract 0 c"
    1.99 -  by (simp_all add: Fract_def)
   1.100 +  by (transfer, simp)+
   1.101  
   1.102  lemma Rat_cases [case_names Fract, cases type: rat]:
   1.103    assumes "\<And>a b. q = Fract a b \<Longrightarrow> b > 0 \<Longrightarrow> coprime a b \<Longrightarrow> C"
   1.104    shows C
   1.105  proof -
   1.106    obtain a b :: int where "q = Fract a b" and "b \<noteq> 0"
   1.107 -    by (cases q) (clarsimp simp add: Fract_def Rat_def quotient_def)
   1.108 +    by transfer simp
   1.109    let ?a = "a div gcd a b"
   1.110    let ?b = "b div gcd a b"
   1.111    from `b \<noteq> 0` have "?b * gcd a b = b"
   1.112 @@ -107,7 +95,7 @@
   1.113    next
   1.114      case False
   1.115      note assms
   1.116 -    moreover from q have "q = Fract (- ?a) (- ?b)" by (simp add: Fract_def)
   1.117 +    moreover have "q = Fract (- ?a) (- ?b)" unfolding q by transfer simp
   1.118      moreover from False `b \<noteq> 0` have "- ?b > 0" by (simp add: pos_imp_zdiv_neg_iff)
   1.119      moreover from coprime have "coprime (- ?a) (- ?b)" by simp
   1.120      ultimately show C .
   1.121 @@ -119,40 +107,35 @@
   1.122    shows "P q"
   1.123    using assms by (cases q) simp
   1.124  
   1.125 -instantiation rat :: comm_ring_1
   1.126 +instantiation rat :: field_inverse_zero
   1.127  begin
   1.128  
   1.129 -definition
   1.130 -  Zero_rat_def: "0 = Fract 0 1"
   1.131 +lift_definition zero_rat :: "rat" is "(0, 1)"
   1.132 +  by simp
   1.133 +
   1.134 +lift_definition one_rat :: "rat" is "(1, 1)"
   1.135 +  by simp
   1.136  
   1.137 -definition
   1.138 -  One_rat_def: "1 = Fract 1 1"
   1.139 +lemma Zero_rat_def: "0 = Fract 0 1"
   1.140 +  by transfer simp
   1.141  
   1.142 -definition
   1.143 -  add_rat_def:
   1.144 -  "q + r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
   1.145 -    ratrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})"
   1.146 +lemma One_rat_def: "1 = Fract 1 1"
   1.147 +  by transfer simp
   1.148 +
   1.149 +lift_definition plus_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat"
   1.150 +  is "\<lambda>x y. (fst x * snd y + fst y * snd x, snd x * snd y)"
   1.151 +  by (clarsimp, simp add: left_distrib, simp add: mult_ac)
   1.152  
   1.153  lemma add_rat [simp]:
   1.154    assumes "b \<noteq> 0" and "d \<noteq> 0"
   1.155    shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)"
   1.156 -proof -
   1.157 -  have "(\<lambda>x y. ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)})
   1.158 -    respects2 ratrel"
   1.159 -  by (rule equiv_ratrel [THEN congruent2_commuteI]) (simp_all add: left_distrib)
   1.160 -  with assms show ?thesis by (simp add: Fract_def add_rat_def UN_ratrel2)
   1.161 -qed
   1.162 +  using assms by transfer simp
   1.163  
   1.164 -definition
   1.165 -  minus_rat_def:
   1.166 -  "- q = Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel `` {(- fst x, snd x)})"
   1.167 +lift_definition uminus_rat :: "rat \<Rightarrow> rat" is "\<lambda>x. (- fst x, snd x)"
   1.168 +  by simp
   1.169  
   1.170  lemma minus_rat [simp]: "- Fract a b = Fract (- a) b"
   1.171 -proof -
   1.172 -  have "(\<lambda>x. ratrel `` {(- fst x, snd x)}) respects ratrel"
   1.173 -    by (simp add: congruent_def split_paired_all)
   1.174 -  then show ?thesis by (simp add: Fract_def minus_rat_def UN_ratrel)
   1.175 -qed
   1.176 +  by transfer simp
   1.177  
   1.178  lemma minus_rat_cancel [simp]: "Fract (- a) (- b) = Fract a b"
   1.179    by (cases "b = 0") (simp_all add: eq_rat)
   1.180 @@ -165,55 +148,59 @@
   1.181    shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)"
   1.182    using assms by (simp add: diff_rat_def)
   1.183  
   1.184 -definition
   1.185 -  mult_rat_def:
   1.186 -  "q * r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
   1.187 -    ratrel``{(fst x * fst y, snd x * snd y)})"
   1.188 +lift_definition times_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat"
   1.189 +  is "\<lambda>x y. (fst x * fst y, snd x * snd y)"
   1.190 +  by (simp add: mult_ac)
   1.191  
   1.192  lemma mult_rat [simp]: "Fract a b * Fract c d = Fract (a * c) (b * d)"
   1.193 -proof -
   1.194 -  have "(\<lambda>x y. ratrel `` {(fst x * fst y, snd x * snd y)}) respects2 ratrel"
   1.195 -    by (rule equiv_ratrel [THEN congruent2_commuteI]) simp_all
   1.196 -  then show ?thesis by (simp add: Fract_def mult_rat_def UN_ratrel2)
   1.197 -qed
   1.198 +  by transfer simp
   1.199  
   1.200  lemma mult_rat_cancel:
   1.201    assumes "c \<noteq> 0"
   1.202    shows "Fract (c * a) (c * b) = Fract a b"
   1.203 -proof -
   1.204 -  from assms have "Fract c c = Fract 1 1" by (simp add: Fract_def)
   1.205 -  then show ?thesis by (simp add: mult_rat [symmetric])
   1.206 -qed
   1.207 +  using assms by transfer simp
   1.208 +
   1.209 +lift_definition inverse_rat :: "rat \<Rightarrow> rat"
   1.210 +  is "\<lambda>x. if fst x = 0 then (0, 1) else (snd x, fst x)"
   1.211 +  by (auto simp add: mult_commute)
   1.212 +
   1.213 +lemma inverse_rat [simp]: "inverse (Fract a b) = Fract b a"
   1.214 +  by transfer simp
   1.215 +
   1.216 +definition
   1.217 +  divide_rat_def: "q / r = q * inverse (r::rat)"
   1.218 +
   1.219 +lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
   1.220 +  by (simp add: divide_rat_def)
   1.221  
   1.222  instance proof
   1.223 -  fix q r s :: rat show "(q * r) * s = q * (r * s)" 
   1.224 -    by (cases q, cases r, cases s) (simp add: eq_rat)
   1.225 -next
   1.226 -  fix q r :: rat show "q * r = r * q"
   1.227 -    by (cases q, cases r) (simp add: eq_rat)
   1.228 -next
   1.229 -  fix q :: rat show "1 * q = q"
   1.230 -    by (cases q) (simp add: One_rat_def eq_rat)
   1.231 -next
   1.232 -  fix q r s :: rat show "(q + r) + s = q + (r + s)"
   1.233 -    by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps)
   1.234 -next
   1.235 -  fix q r :: rat show "q + r = r + q"
   1.236 -    by (cases q, cases r) (simp add: eq_rat)
   1.237 -next
   1.238 -  fix q :: rat show "0 + q = q"
   1.239 -    by (cases q) (simp add: Zero_rat_def eq_rat)
   1.240 -next
   1.241 -  fix q :: rat show "- q + q = 0"
   1.242 -    by (cases q) (simp add: Zero_rat_def eq_rat)
   1.243 -next
   1.244 -  fix q r :: rat show "q - r = q + - r"
   1.245 -    by (cases q, cases r) (simp add: eq_rat)
   1.246 -next
   1.247 -  fix q r s :: rat show "(q + r) * s = q * s + r * s"
   1.248 -    by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps)
   1.249 -next
   1.250 -  show "(0::rat) \<noteq> 1" by (simp add: Zero_rat_def One_rat_def eq_rat)
   1.251 +  fix q r s :: rat
   1.252 +  show "(q * r) * s = q * (r * s)"
   1.253 +    by transfer simp
   1.254 +  show "q * r = r * q"
   1.255 +    by transfer simp
   1.256 +  show "1 * q = q"
   1.257 +    by transfer simp
   1.258 +  show "(q + r) + s = q + (r + s)"
   1.259 +    by transfer (simp add: algebra_simps)
   1.260 +  show "q + r = r + q"
   1.261 +    by transfer simp
   1.262 +  show "0 + q = q"
   1.263 +    by transfer simp
   1.264 +  show "- q + q = 0"
   1.265 +    by transfer simp
   1.266 +  show "q - r = q + - r"
   1.267 +    by (fact diff_rat_def)
   1.268 +  show "(q + r) * s = q * s + r * s"
   1.269 +    by transfer (simp add: algebra_simps)
   1.270 +  show "(0::rat) \<noteq> 1"
   1.271 +    by transfer simp
   1.272 +  { assume "q \<noteq> 0" thus "inverse q * q = 1"
   1.273 +    by transfer simp }
   1.274 +  show "q / r = q * inverse r"
   1.275 +    by (fact divide_rat_def)
   1.276 +  show "inverse 0 = (0::rat)"
   1.277 +    by transfer simp
   1.278  qed
   1.279  
   1.280  end
   1.281 @@ -402,44 +389,6 @@
   1.282    by (auto simp add: quotient_of_inject)
   1.283  
   1.284  
   1.285 -subsubsection {* The field of rational numbers *}
   1.286 -
   1.287 -instantiation rat :: field_inverse_zero
   1.288 -begin
   1.289 -
   1.290 -definition
   1.291 -  inverse_rat_def:
   1.292 -  "inverse q = Abs_Rat (\<Union>x \<in> Rep_Rat q.
   1.293 -     ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})"
   1.294 -
   1.295 -lemma inverse_rat [simp]: "inverse (Fract a b) = Fract b a"
   1.296 -proof -
   1.297 -  have "(\<lambda>x. ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)}) respects ratrel"
   1.298 -    by (auto simp add: congruent_def mult_commute)
   1.299 -  then show ?thesis by (simp add: Fract_def inverse_rat_def UN_ratrel)
   1.300 -qed
   1.301 -
   1.302 -definition
   1.303 -  divide_rat_def: "q / r = q * inverse (r::rat)"
   1.304 -
   1.305 -lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
   1.306 -  by (simp add: divide_rat_def)
   1.307 -
   1.308 -instance proof
   1.309 -  fix q :: rat
   1.310 -  assume "q \<noteq> 0"
   1.311 -  then show "inverse q * q = 1" by (cases q rule: Rat_cases_nonzero)
   1.312 -   (simp_all add: rat_number_expand eq_rat)
   1.313 -next
   1.314 -  fix q r :: rat
   1.315 -  show "q / r = q * inverse r" by (simp add: divide_rat_def)
   1.316 -next
   1.317 -  show "inverse 0 = (0::rat)" by (simp add: rat_number_expand, simp add: rat_number_collapse)
   1.318 -qed
   1.319 -
   1.320 -end
   1.321 -
   1.322 -
   1.323  subsubsection {* Various *}
   1.324  
   1.325  lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l"
   1.326 @@ -454,55 +403,49 @@
   1.327  instantiation rat :: linorder
   1.328  begin
   1.329  
   1.330 -definition
   1.331 -  le_rat_def:
   1.332 -   "q \<le> r \<longleftrightarrow> the_elem (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
   1.333 -      {(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})"
   1.334 +lift_definition less_eq_rat :: "rat \<Rightarrow> rat \<Rightarrow> bool"
   1.335 +  is "\<lambda>x y. (fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)"
   1.336 +proof (clarsimp)
   1.337 +  fix a b a' b' c d c' d'::int
   1.338 +  assume neq: "b \<noteq> 0"  "b' \<noteq> 0"  "d \<noteq> 0"  "d' \<noteq> 0"
   1.339 +  assume eq1: "a * b' = a' * b"
   1.340 +  assume eq2: "c * d' = c' * d"
   1.341 +
   1.342 +  let ?le = "\<lambda>a b c d. ((a * d) * (b * d) \<le> (c * b) * (b * d))"
   1.343 +  {
   1.344 +    fix a b c d x :: int assume x: "x \<noteq> 0"
   1.345 +    have "?le a b c d = ?le (a * x) (b * x) c d"
   1.346 +    proof -
   1.347 +      from x have "0 < x * x" by (auto simp add: zero_less_mult_iff)
   1.348 +      hence "?le a b c d =
   1.349 +        ((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))"
   1.350 +        by (simp add: mult_le_cancel_right)
   1.351 +      also have "... = ?le (a * x) (b * x) c d"
   1.352 +        by (simp add: mult_ac)
   1.353 +      finally show ?thesis .
   1.354 +    qed
   1.355 +  } note le_factor = this
   1.356 +  
   1.357 +  let ?D = "b * d" and ?D' = "b' * d'"
   1.358 +  from neq have D: "?D \<noteq> 0" by simp
   1.359 +  from neq have "?D' \<noteq> 0" by simp
   1.360 +  hence "?le a b c d = ?le (a * ?D') (b * ?D') c d"
   1.361 +    by (rule le_factor)
   1.362 +  also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')" 
   1.363 +    by (simp add: mult_ac)
   1.364 +  also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')"
   1.365 +    by (simp only: eq1 eq2)
   1.366 +  also have "... = ?le (a' * ?D) (b' * ?D) c' d'"
   1.367 +    by (simp add: mult_ac)
   1.368 +  also from D have "... = ?le a' b' c' d'"
   1.369 +    by (rule le_factor [symmetric])
   1.370 +  finally show "?le a b c d = ?le a' b' c' d'" .
   1.371 +qed
   1.372  
   1.373  lemma le_rat [simp]:
   1.374    assumes "b \<noteq> 0" and "d \<noteq> 0"
   1.375    shows "Fract a b \<le> Fract c d \<longleftrightarrow> (a * d) * (b * d) \<le> (c * b) * (b * d)"
   1.376 -proof -
   1.377 -  have "(\<lambda>x y. {(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})
   1.378 -    respects2 ratrel"
   1.379 -  proof (clarsimp simp add: congruent2_def)
   1.380 -    fix a b a' b' c d c' d'::int
   1.381 -    assume neq: "b \<noteq> 0"  "b' \<noteq> 0"  "d \<noteq> 0"  "d' \<noteq> 0"
   1.382 -    assume eq1: "a * b' = a' * b"
   1.383 -    assume eq2: "c * d' = c' * d"
   1.384 -
   1.385 -    let ?le = "\<lambda>a b c d. ((a * d) * (b * d) \<le> (c * b) * (b * d))"
   1.386 -    {
   1.387 -      fix a b c d x :: int assume x: "x \<noteq> 0"
   1.388 -      have "?le a b c d = ?le (a * x) (b * x) c d"
   1.389 -      proof -
   1.390 -        from x have "0 < x * x" by (auto simp add: zero_less_mult_iff)
   1.391 -        hence "?le a b c d =
   1.392 -            ((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))"
   1.393 -          by (simp add: mult_le_cancel_right)
   1.394 -        also have "... = ?le (a * x) (b * x) c d"
   1.395 -          by (simp add: mult_ac)
   1.396 -        finally show ?thesis .
   1.397 -      qed
   1.398 -    } note le_factor = this
   1.399 -
   1.400 -    let ?D = "b * d" and ?D' = "b' * d'"
   1.401 -    from neq have D: "?D \<noteq> 0" by simp
   1.402 -    from neq have "?D' \<noteq> 0" by simp
   1.403 -    hence "?le a b c d = ?le (a * ?D') (b * ?D') c d"
   1.404 -      by (rule le_factor)
   1.405 -    also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')" 
   1.406 -      by (simp add: mult_ac)
   1.407 -    also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')"
   1.408 -      by (simp only: eq1 eq2)
   1.409 -    also have "... = ?le (a' * ?D) (b' * ?D) c' d'"
   1.410 -      by (simp add: mult_ac)
   1.411 -    also from D have "... = ?le a' b' c' d'"
   1.412 -      by (rule le_factor [symmetric])
   1.413 -    finally show "?le a b c d = ?le a' b' c' d'" .
   1.414 -  qed
   1.415 -  with assms show ?thesis by (simp add: Fract_def le_rat_def UN_ratrel2)
   1.416 -qed
   1.417 +  using assms by transfer simp
   1.418  
   1.419  definition
   1.420    less_rat_def: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
   1.421 @@ -775,38 +718,34 @@
   1.422  context field_char_0
   1.423  begin
   1.424  
   1.425 -definition of_rat :: "rat \<Rightarrow> 'a" where
   1.426 -  "of_rat q = the_elem (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
   1.427 -
   1.428 -end
   1.429 -
   1.430 -lemma of_rat_congruent:
   1.431 -  "(\<lambda>(a, b). {of_int a / of_int b :: 'a::field_char_0}) respects ratrel"
   1.432 -apply (rule congruentI)
   1.433 +lift_definition of_rat :: "rat \<Rightarrow> 'a"
   1.434 +  is "\<lambda>x. of_int (fst x) / of_int (snd x)"
   1.435  apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq)
   1.436  apply (simp only: of_int_mult [symmetric])
   1.437  done
   1.438  
   1.439 +end
   1.440 +
   1.441  lemma of_rat_rat: "b \<noteq> 0 \<Longrightarrow> of_rat (Fract a b) = of_int a / of_int b"
   1.442 -  unfolding Fract_def of_rat_def by (simp add: UN_ratrel of_rat_congruent)
   1.443 +  by transfer simp
   1.444  
   1.445  lemma of_rat_0 [simp]: "of_rat 0 = 0"
   1.446 -by (simp add: Zero_rat_def of_rat_rat)
   1.447 +  by transfer simp
   1.448  
   1.449  lemma of_rat_1 [simp]: "of_rat 1 = 1"
   1.450 -by (simp add: One_rat_def of_rat_rat)
   1.451 +  by transfer simp
   1.452  
   1.453  lemma of_rat_add: "of_rat (a + b) = of_rat a + of_rat b"
   1.454 -by (induct a, induct b, simp add: of_rat_rat add_frac_eq)
   1.455 +  by transfer (simp add: add_frac_eq)
   1.456  
   1.457  lemma of_rat_minus: "of_rat (- a) = - of_rat a"
   1.458 -by (induct a, simp add: of_rat_rat)
   1.459 +  by transfer simp
   1.460  
   1.461  lemma of_rat_diff: "of_rat (a - b) = of_rat a - of_rat b"
   1.462  by (simp only: diff_minus of_rat_add of_rat_minus)
   1.463  
   1.464  lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b"
   1.465 -apply (induct a, induct b, simp add: of_rat_rat)
   1.466 +apply transfer
   1.467  apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac)
   1.468  done
   1.469  
   1.470 @@ -835,8 +774,7 @@
   1.471  by (induct n) (simp_all add: of_rat_mult)
   1.472  
   1.473  lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)"
   1.474 -apply (induct a, induct b)
   1.475 -apply (simp add: of_rat_rat eq_rat)
   1.476 +apply transfer
   1.477  apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq)
   1.478  apply (simp only: of_int_mult [symmetric] of_int_eq_iff)
   1.479  done
   1.480 @@ -1007,7 +945,6 @@
   1.481  lemma Rats_cases [cases set: Rats]:
   1.482    assumes "q \<in> \<rat>"
   1.483    obtains (of_rat) r where "q = of_rat r"
   1.484 -  unfolding Rats_def
   1.485  proof -
   1.486    from `q \<in> \<rat>` have "q \<in> range of_rat" unfolding Rats_def .
   1.487    then obtain r where "q = of_rat r" ..
   1.488 @@ -1259,4 +1196,15 @@
   1.489  
   1.490  hide_const (open) normalize
   1.491  
   1.492 +lemmas [transfer_rule del] =
   1.493 +  rat.All_transfer rat.Ex_transfer rat.rel_eq_transfer forall_rat_transfer
   1.494 +  Fract.transfer zero_rat.transfer one_rat.transfer plus_rat.transfer
   1.495 +  uminus_rat.transfer times_rat.transfer inverse_rat.transfer
   1.496 +  less_eq_rat.transfer of_rat.transfer
   1.497 +
   1.498 +text {* De-register @{text "rat"} as a quotient type: *}
   1.499 +
   1.500 +setup {* Context.theory_map (Lifting_Info.update_quotients @{type_name rat}
   1.501 +  {quot_thm = @{thm identity_quotient [where 'a=rat]}}) *}
   1.502 +
   1.503  end