# HG changeset patch
# User huffman
# Date 1181183595 -7200
# Node ID 0cf371d943b15caf3850c5446f6f5a02c6b7ceba
# Parent  3e45b5464d2bb9ef0569cd6244e852baab4ba592
remove redundant lemmas

diff -r 3e45b5464d2b -r 0cf371d943b1 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Thu Jun 07 03:45:56 2007 +0200
+++ b/src/HOL/Real/RealDef.thy	Thu Jun 07 04:33:15 2007 +0200
@@ -483,14 +483,6 @@
 
 subsection{*Theorems About the Ordering*}
 
-text{*obsolete but used a lot*}
-
-lemma real_not_refl2: "x < y ==> x \<noteq> (y::real)"
-by blast 
-
-lemma real_le_imp_less_or_eq: "!!(x::real). x \<le> y ==> x < y | x = y"
-by (simp add: order_le_less)
-
 lemma real_gt_zero_preal_Ex: "(0 < x) = (\<exists>y. x = real_of_preal y)"
 apply (auto simp add: real_of_preal_zero_less)
 apply (cut_tac x = x in real_of_preal_trichotomy)
@@ -514,9 +506,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_le_square [simp]: "(0::real) \<le> x*x"
- by (rule Ring_and_Field.zero_le_square)
-
 
 subsection{*More Lemmas*}
 
@@ -526,34 +515,24 @@
 lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
 by auto
 
-text{*The precondition could be weakened to @{term "0\<le>x"}*}
-lemma real_mult_less_mono:
-     "[| u<v;  x<y;  (0::real) < v;  0 < x |] ==> u*x < v* y"
- by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
-
 lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
   by (force elim: order_less_asym
             simp add: Ring_and_Field.mult_less_cancel_right)
 
 lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)"
 apply (simp add: mult_le_cancel_right)
-apply (blast intro: elim: order_less_asym) 
+apply (blast intro: elim: order_less_asym)
 done
 
 lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
 by(simp add:mult_commute)
 
-lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y"
-by (rule add_pos_pos)
-
+(* FIXME: redundant, but used by Integration/Integral.thy in AFP *)
 lemma real_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::real) \<le> x + y"
 by (rule add_nonneg_nonneg)
 
-lemma real_inverse_unique: "x*y = (1::real) ==> y = inverse x"
-by (rule inverse_unique [symmetric])
-
 lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x"
-by (simp add: one_less_inverse_iff)
+by (simp add: one_less_inverse_iff) (* TODO: generalize/move *)
 
 
 subsection{*Embedding the Integers into the Reals*}
@@ -872,18 +851,6 @@
 setup real_arith_setup
 
 
-lemma real_diff_mult_distrib:
-  fixes a::real
-  shows "a * (b - c) = a * b - a * c" 
-proof -
-  have "a * (b - c) = a * (b + -c)" by simp
-  also have "\<dots> = (b + -c) * a" by simp
-  also have "\<dots> = b*a + (-c)*a" by (rule real_add_mult_distrib)
-  also have "\<dots> = a*b - a*c" by simp
-  finally show ?thesis .
-qed
-
-
 subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
 
 text{*Needed in this non-standard form by Hyperreal/Transcendental*}
@@ -939,9 +906,7 @@
 lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
 by (simp add: abs_if)
 
-lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))"
-by (force simp add: Ring_and_Field.abs_less_iff)
-
+(* FIXME: redundant, but used by Integration/RealRandVar.thy in AFP *)
 lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
 by (force simp add: OrderedGroup.abs_le_iff)