remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
authorhuffman
Sat Aug 20 15:54:26 2011 -0700 (2011-08-20)
changeset 44349f057535311c5
parent 44348 40101794c52f
child 44350 63cddfbc5a09
remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/NthRoot.thy
src/HOL/RealDef.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sat Aug 20 13:07:00 2011 -0700
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Aug 20 15:54:26 2011 -0700
     1.3 @@ -712,7 +712,7 @@
     1.4          case False
     1.5          hence "real ?DIV \<le> 1" unfolding less_float_def by auto
     1.6  
     1.7 -        have "0 \<le> x / ?R" using `0 \<le> real x` `0 < ?R` unfolding real_0_le_divide_iff by auto
     1.8 +        have "0 \<le> x / ?R" using `0 \<le> real x` `0 < ?R` unfolding zero_le_divide_iff by auto
     1.9          hence "0 \<le> real ?DIV" using monotone by (rule order_trans)
    1.10  
    1.11          have "arctan x = 2 * arctan (x / ?R)" using arctan_half unfolding numeral_2_eq_2 power_Suc2 power_0 mult_1_left .
     2.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Aug 20 13:07:00 2011 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Aug 20 15:54:26 2011 -0700
     2.3 @@ -1168,7 +1168,7 @@
     2.4        thus ?thesis unfolding obt1(5) obt2(5) unfolding * and ** using False
     2.5          apply(rule_tac x="((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI) defer
     2.6          apply(rule convex_convex_hull[of s, unfolded convex_def, rule_format]) using obt1(4) obt2(4)
     2.7 -        unfolding add_divide_distrib[THEN sym] and real_0_le_divide_iff
     2.8 +        unfolding add_divide_distrib[THEN sym] and zero_le_divide_iff
     2.9          by (auto simp add: scaleR_left_distrib scaleR_right_distrib)
    2.10      qed note * = this
    2.11      have u1:"u1 \<le> 1" unfolding obt1(3)[THEN sym] and not_le using obt1(2) by auto
     3.1 --- a/src/HOL/NthRoot.thy	Sat Aug 20 13:07:00 2011 -0700
     3.2 +++ b/src/HOL/NthRoot.thy	Sat Aug 20 15:54:26 2011 -0700
     3.3 @@ -629,7 +629,7 @@
     3.4  apply (rule_tac y = "u/sqrt 2" in order_le_less_trans)
     3.5  apply (erule_tac [2] lemma_real_divide_sqrt_less)
     3.6  apply (rule power2_le_imp_le)
     3.7 -apply (auto simp add: real_0_le_divide_iff power_divide)
     3.8 +apply (auto simp add: zero_le_divide_iff power_divide)
     3.9  apply (rule_tac t = "u\<twosuperior>" in real_sum_of_halves [THEN subst])
    3.10  apply (rule add_mono)
    3.11  apply (auto simp add: four_x_squared intro: power_mono)
     4.1 --- a/src/HOL/RealDef.thy	Sat Aug 20 13:07:00 2011 -0700
     4.2 +++ b/src/HOL/RealDef.thy	Sat Aug 20 15:54:26 2011 -0700
     4.3 @@ -1553,11 +1553,6 @@
     4.4  
     4.5  subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
     4.6  
     4.7 -text{*Needed in this non-standard form by Hyperreal/Transcendental*}
     4.8 -lemma real_0_le_divide_iff:
     4.9 -     "((0::real) \<le> x/y) = ((x \<le> 0 | 0 \<le> y) & (0 \<le> x | y \<le> 0))"
    4.10 -by (auto simp add: zero_le_divide_iff)
    4.11 -
    4.12  lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)" 
    4.13  by arith
    4.14