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.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.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.152
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.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
```