src/HOL/Real/RealDef.thy
changeset 22962 4bb05ba38939
parent 22958 b3a5569a81e5
child 22970 b5910e3dec4c
     1.1 --- a/src/HOL/Real/RealDef.thy	Mon May 14 09:27:24 2007 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Mon May 14 09:33:18 2007 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4  
     1.5    real_less_def: "(x < (y::real)) == (x \<le> y & x \<noteq> y)"
     1.6  
     1.7 -  real_abs_def:  "abs (r::real) == (if 0 \<le> r then r else -r)"
     1.8 +  real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)"
     1.9  
    1.10  
    1.11  
    1.12 @@ -293,9 +293,6 @@
    1.13    show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
    1.14  qed
    1.15  
    1.16 -lemma real_mult_1_right: "z * (1::real) = z"
    1.17 -  by (rule OrderedGroup.mult_1_right)
    1.18 -
    1.19  
    1.20  subsection{*The @{text "\<le>"} Ordering*}
    1.21  
    1.22 @@ -418,11 +415,6 @@
    1.23  apply (simp add: right_distrib)
    1.24  done
    1.25  
    1.26 -text{*lemma for proving @{term "0<(1::real)"}*}
    1.27 -lemma real_zero_le_one: "0 \<le> (1::real)"
    1.28 -by (simp add: real_zero_def real_one_def real_le 
    1.29 -                 preal_self_less_add_left order_less_imp_le)
    1.30 -
    1.31  instance real :: distrib_lattice
    1.32    "inf x y \<equiv> min x y"
    1.33    "sup x y \<equiv> max x y"
    1.34 @@ -435,9 +427,8 @@
    1.35  proof
    1.36    fix x y z :: real
    1.37    show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
    1.38 -  show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2)
    1.39 -  show "\<bar>x\<bar> = (if x < 0 then -x else x)"
    1.40 -    by (auto dest: order_le_less_trans simp add: real_abs_def linorder_not_le)
    1.41 +  show "x < y ==> 0 < z ==> z * x < z * y" by (rule real_mult_less_mono2)
    1.42 +  show "\<bar>x\<bar> = (if x < 0 then -x else x)" by (simp only: real_abs_def)
    1.43  qed
    1.44  
    1.45  text{*The function @{term real_of_preal} requires many proofs, but it seems
    1.46 @@ -537,13 +528,6 @@
    1.47  lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x"
    1.48  by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1])
    1.49  
    1.50 -lemma real_add_less_le_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::real)"
    1.51 -  by (rule OrderedGroup.add_less_le_mono)
    1.52 -
    1.53 -lemma real_add_le_less_mono:
    1.54 -     "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"
    1.55 -  by (rule OrderedGroup.add_le_less_mono)
    1.56 -
    1.57  lemma real_le_square [simp]: "(0::real) \<le> x*x"
    1.58   by (rule Ring_and_Field.zero_le_square)
    1.59  
    1.60 @@ -573,11 +557,6 @@
    1.61  lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
    1.62  by(simp add:mult_commute)
    1.63  
    1.64 -text{*Only two uses?*}
    1.65 -lemma real_mult_less_mono':
    1.66 -     "[| x < y;  r1 < r2;  (0::real) \<le> r1;  0 \<le> x|] ==> r1 * x < r2 * y"
    1.67 - by (rule Ring_and_Field.mult_strict_mono')
    1.68 -
    1.69  text{*FIXME: delete or at least combine the next two lemmas*}
    1.70  lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
    1.71  apply (drule OrderedGroup.equals_zero_I [THEN sym])