src/HOL/Real/RealDef.thy
 changeset 27652 818666de6c24 parent 27544 5b293a8cf476 child 27668 6eb20b2cecf8
```     1.1 --- a/src/HOL/Real/RealDef.thy	Fri Jul 18 18:25:53 2008 +0200
1.2 +++ b/src/HOL/Real/RealDef.thy	Fri Jul 18 18:25:56 2008 +0200
1.3 @@ -1003,30 +1003,11 @@
1.4
1.5  end
1.6
1.7 -lemma Ratreal_INum: "Ratreal (Fract k l) = INum (k, l)"
1.8 -  by (auto simp add: expand_fun_eq INum_def Fract_of_int_quotient of_rat_divide)
1.9 -
1.10  lemma real_less_eq_code [code]: "Ratreal x \<le> Ratreal y \<longleftrightarrow> x \<le> y"
1.11 -proof -
1.12 -  obtain k l r s where x: "x = Fract k l" and y: "y = Fract r s"
1.13 -    by (cases x, cases y) simp
1.14 -  have "normNum (k, l) \<le>\<^sub>N normNum (r, s) \<longleftrightarrow> INum (normNum (k, l)) \<le> (INum (normNum (r, s)) :: real)"
1.15 -    by (simp del: normNum)
1.16 -  then have "Ratreal (Fract k l) \<le> Ratreal (Fract r s) \<longleftrightarrow> Fract k l \<le> Fract r s"
1.17 -    by (simp add: Ratreal_INum rat_less_eq_code del: Ratreal_def)
1.18 -  with x y show ?thesis by simp
1.19 -qed
1.20 +  by (simp add: of_rat_less_eq)
1.21
1.22  lemma real_less_code [code]: "Ratreal x < Ratreal y \<longleftrightarrow> x < y"
1.23 -proof -
1.24 -  obtain k l r s where x: "x = Fract k l" and y: "y = Fract r s"
1.25 -    by (cases x, cases y) simp
1.26 -  have "normNum (k, l) <\<^sub>N normNum (r, s) \<longleftrightarrow> INum (normNum (k, l)) < (INum (normNum (r, s)) :: real)"
1.27 -    by (simp del: normNum)
1.28 -  then have "Ratreal (Fract k l) < Ratreal (Fract r s) \<longleftrightarrow> Fract k l < Fract r s"
1.29 -    by (simp add: Ratreal_INum rat_less_code del: Ratreal_def)
1.30 -  with x y show ?thesis by simp
1.31 -qed
1.32 +  by (simp add: of_rat_less)
1.33
1.34  lemma real_plus_code [code]: "Ratreal x + Ratreal y = Ratreal (x + y)"