src/HOL/Real/RealDef.thy
changeset 23289 0cf371d943b1
parent 23288 3e45b5464d2b
child 23431 25ca91279a9b
     1.1 --- a/src/HOL/Real/RealDef.thy	Thu Jun 07 03:45:56 2007 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Thu Jun 07 04:33:15 2007 +0200
     1.3 @@ -483,14 +483,6 @@
     1.4  
     1.5  subsection{*Theorems About the Ordering*}
     1.6  
     1.7 -text{*obsolete but used a lot*}
     1.8 -
     1.9 -lemma real_not_refl2: "x < y ==> x \<noteq> (y::real)"
    1.10 -by blast 
    1.11 -
    1.12 -lemma real_le_imp_less_or_eq: "!!(x::real). x \<le> y ==> x < y | x = y"
    1.13 -by (simp add: order_le_less)
    1.14 -
    1.15  lemma real_gt_zero_preal_Ex: "(0 < x) = (\<exists>y. x = real_of_preal y)"
    1.16  apply (auto simp add: real_of_preal_zero_less)
    1.17  apply (cut_tac x = x in real_of_preal_trichotomy)
    1.18 @@ -514,9 +506,6 @@
    1.19  lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x"
    1.20  by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1])
    1.21  
    1.22 -lemma real_le_square [simp]: "(0::real) \<le> x*x"
    1.23 - by (rule Ring_and_Field.zero_le_square)
    1.24 -
    1.25  
    1.26  subsection{*More Lemmas*}
    1.27  
    1.28 @@ -526,34 +515,24 @@
    1.29  lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
    1.30  by auto
    1.31  
    1.32 -text{*The precondition could be weakened to @{term "0\<le>x"}*}
    1.33 -lemma real_mult_less_mono:
    1.34 -     "[| u<v;  x<y;  (0::real) < v;  0 < x |] ==> u*x < v* y"
    1.35 - by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
    1.36 -
    1.37  lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
    1.38    by (force elim: order_less_asym
    1.39              simp add: Ring_and_Field.mult_less_cancel_right)
    1.40  
    1.41  lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)"
    1.42  apply (simp add: mult_le_cancel_right)
    1.43 -apply (blast intro: elim: order_less_asym) 
    1.44 +apply (blast intro: elim: order_less_asym)
    1.45  done
    1.46  
    1.47  lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
    1.48  by(simp add:mult_commute)
    1.49  
    1.50 -lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y"
    1.51 -by (rule add_pos_pos)
    1.52 -
    1.53 +(* FIXME: redundant, but used by Integration/Integral.thy in AFP *)
    1.54  lemma real_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::real) \<le> x + y"
    1.55  by (rule add_nonneg_nonneg)
    1.56  
    1.57 -lemma real_inverse_unique: "x*y = (1::real) ==> y = inverse x"
    1.58 -by (rule inverse_unique [symmetric])
    1.59 -
    1.60  lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x"
    1.61 -by (simp add: one_less_inverse_iff)
    1.62 +by (simp add: one_less_inverse_iff) (* TODO: generalize/move *)
    1.63  
    1.64  
    1.65  subsection{*Embedding the Integers into the Reals*}
    1.66 @@ -872,18 +851,6 @@
    1.67  setup real_arith_setup
    1.68  
    1.69  
    1.70 -lemma real_diff_mult_distrib:
    1.71 -  fixes a::real
    1.72 -  shows "a * (b - c) = a * b - a * c" 
    1.73 -proof -
    1.74 -  have "a * (b - c) = a * (b + -c)" by simp
    1.75 -  also have "\<dots> = (b + -c) * a" by simp
    1.76 -  also have "\<dots> = b*a + (-c)*a" by (rule real_add_mult_distrib)
    1.77 -  also have "\<dots> = a*b - a*c" by simp
    1.78 -  finally show ?thesis .
    1.79 -qed
    1.80 -
    1.81 -
    1.82  subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
    1.83  
    1.84  text{*Needed in this non-standard form by Hyperreal/Transcendental*}
    1.85 @@ -939,9 +906,7 @@
    1.86  lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
    1.87  by (simp add: abs_if)
    1.88  
    1.89 -lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))"
    1.90 -by (force simp add: Ring_and_Field.abs_less_iff)
    1.91 -
    1.92 +(* FIXME: redundant, but used by Integration/RealRandVar.thy in AFP *)
    1.93  lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
    1.94  by (force simp add: OrderedGroup.abs_le_iff)
    1.95