src/HOL/Real/RealDef.thy
changeset 22962 4bb05ba38939
parent 22958 b3a5569a81e5
child 22970 b5910e3dec4c
--- a/src/HOL/Real/RealDef.thy	Mon May 14 09:27:24 2007 +0200
+++ b/src/HOL/Real/RealDef.thy	Mon May 14 09:33:18 2007 +0200
@@ -72,7 +72,7 @@
 
   real_less_def: "(x < (y::real)) == (x \<le> y & x \<noteq> y)"
 
-  real_abs_def:  "abs (r::real) == (if 0 \<le> r then r else -r)"
+  real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)"
 
 
 
@@ -293,9 +293,6 @@
   show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
 qed
 
-lemma real_mult_1_right: "z * (1::real) = z"
-  by (rule OrderedGroup.mult_1_right)
-
 
 subsection{*The @{text "\<le>"} Ordering*}
 
@@ -418,11 +415,6 @@
 apply (simp add: right_distrib)
 done
 
-text{*lemma for proving @{term "0<(1::real)"}*}
-lemma real_zero_le_one: "0 \<le> (1::real)"
-by (simp add: real_zero_def real_one_def real_le 
-                 preal_self_less_add_left order_less_imp_le)
-
 instance real :: distrib_lattice
   "inf x y \<equiv> min x y"
   "sup x y \<equiv> max x y"
@@ -435,9 +427,8 @@
 proof
   fix x y z :: real
   show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
-  show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2)
-  show "\<bar>x\<bar> = (if x < 0 then -x else x)"
-    by (auto dest: order_le_less_trans simp add: real_abs_def linorder_not_le)
+  show "x < y ==> 0 < z ==> z * x < z * y" by (rule real_mult_less_mono2)
+  show "\<bar>x\<bar> = (if x < 0 then -x else x)" by (simp only: real_abs_def)
 qed
 
 text{*The function @{term real_of_preal} requires many proofs, but it seems
@@ -537,13 +528,6 @@
 lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x"
 by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1])
 
-lemma real_add_less_le_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::real)"
-  by (rule OrderedGroup.add_less_le_mono)
-
-lemma real_add_le_less_mono:
-     "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"
-  by (rule OrderedGroup.add_le_less_mono)
-
 lemma real_le_square [simp]: "(0::real) \<le> x*x"
  by (rule Ring_and_Field.zero_le_square)
 
@@ -573,11 +557,6 @@
 lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
 by(simp add:mult_commute)
 
-text{*Only two uses?*}
-lemma real_mult_less_mono':
-     "[| x < y;  r1 < r2;  (0::real) \<le> r1;  0 \<le> x|] ==> r1 * x < r2 * y"
- by (rule Ring_and_Field.mult_strict_mono')
-
 text{*FIXME: delete or at least combine the next two lemmas*}
 lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
 apply (drule OrderedGroup.equals_zero_I [THEN sym])