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 @@
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
-
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)"
-
-     "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"
-
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)"