# HG changeset patch
# User huffman
# Date 1179127998 -7200
# Node ID 4bb05ba389394a61e271cf26f7db5068817c3e2f
# Parent  e499ded5d0fcb23ffa1745f662c4bc16ffbd1be3
remove redundant lemmas

diff -r e499ded5d0fc -r 4bb05ba38939 src/HOL/Real/RealDef.thy
--- 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])
diff -r e499ded5d0fc -r 4bb05ba38939 src/HOL/Real/RealPow.thy
--- a/src/HOL/Real/RealPow.thy	Mon May 14 09:27:24 2007 +0200
+++ b/src/HOL/Real/RealPow.thy	Mon May 14 09:33:18 2007 +0200
@@ -28,9 +28,6 @@
 qed
 
 
-lemma realpow_not_zero: "r \<noteq> (0::real) ==> r ^ n \<noteq> 0"
-  by (rule field_power_not_zero)
-
 lemma realpow_zero_zero: "r ^ n = (0::real) ==> r = 0"
 by simp
 
@@ -59,16 +56,13 @@
 apply (induct "n")
 apply (auto simp add: real_of_nat_Suc)
 apply (subst mult_2)
-apply (rule real_add_less_le_mono)
+apply (rule add_less_le_mono)
 apply (auto simp add: two_realpow_ge_one)
 done
 
 lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r"
 by (insert power_decreasing [of 1 "Suc n" r], simp)
 
-lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"
-by (rule power_Suc_less_one)
-
 lemma realpow_minus_mult [rule_format]:
      "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" 
 apply (simp split add: nat_diff_split)
@@ -103,21 +97,12 @@
 apply (auto simp add: real_of_nat_mult zero_less_mult_iff)
 done
 
+(* used by AFP Integration theory *)
 lemma realpow_increasing:
      "[|(0::real) \<le> x; 0 \<le> y; x ^ Suc n \<le> y ^ Suc n|] ==> x \<le> y"
   by (rule power_le_imp_le_base)
 
 
-lemma zero_less_realpow_abs_iff [simp]:
-     "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)" 
-apply (induct "n")
-apply (auto simp add: zero_less_mult_iff)
-done
-
-lemma zero_le_realpow_abs [simp]: "(0::real) \<le> (abs x)^n"
-by (rule zero_le_power_abs)
-
-
 subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*}
 
 lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)"
diff -r e499ded5d0fc -r 4bb05ba38939 src/HOL/Real/real_arith.ML
--- a/src/HOL/Real/real_arith.ML	Mon May 14 09:27:24 2007 +0200
+++ b/src/HOL/Real/real_arith.ML	Mon May 14 09:33:18 2007 +0200
@@ -20,7 +20,6 @@
 val real_mult_commute = thm"real_mult_commute";
 val real_mult_assoc = thm"real_mult_assoc";
 val real_mult_1 = thm"real_mult_1";
-val real_mult_1_right = thm"real_mult_1_right";
 val preal_le_linear = thm"preal_le_linear";
 val real_mult_inverse_left = thm"real_mult_inverse_left";
 val real_not_refl2 = thm"real_not_refl2";
@@ -43,8 +42,6 @@
 val real_less_all_real2 = thm "real_less_all_real2";
 val real_of_preal_le_iff = thm "real_of_preal_le_iff";
 val real_mult_order = thm "real_mult_order";
-val real_add_less_le_mono = thm "real_add_less_le_mono";
-val real_add_le_less_mono = thm "real_add_le_less_mono";
 val real_add_order = thm "real_add_order";
 val real_le_add_order = thm "real_le_add_order";
 val real_le_square = thm "real_le_square";
@@ -54,7 +51,6 @@
 val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1";
 val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2";
 val real_mult_less_mono = thm "real_mult_less_mono";
-val real_mult_less_mono' = thm "real_mult_less_mono'";
 val real_sum_squares_cancel = thm "real_sum_squares_cancel";
 val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2";