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)"
    1.35    by (simp add: of_rat_add)