# HG changeset patch
# User hoelzl
# Date 1397473697 -7200
# Node ID f4635657d66fac591c9df7c086f6d075b49f42e3
# Parent  282f3b06fa86b84bbddc5ef42915a5c47191e7b6
added divide_nonneg_nonneg and co; made it a simp rule

diff -r 282f3b06fa86 -r f4635657d66f src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -778,7 +778,7 @@
       also have "\<dots> \<le> cos x"
       proof -
         from even[OF `even n`] `0 < ?fact` `0 < ?pow`
-        have "0 \<le> (?rest / ?fact) * ?pow" by (simp add: divide_nonneg_pos)
+        have "0 \<le> (?rest / ?fact) * ?pow" by simp
         thus ?thesis unfolding cos_eq by auto
       qed
       finally have "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> cos x" .
@@ -891,7 +891,7 @@
       also have "\<dots> \<le> sin x"
       proof -
         from even[OF `even n`] `0 < ?fact` `0 < ?pow`
-        have "0 \<le> (?rest / ?fact) * ?pow" by (simp add: divide_nonneg_pos less_imp_le)
+        have "0 \<le> (?rest / ?fact) * ?pow" by simp
         thus ?thesis unfolding sin_eq by auto
       qed
       finally have "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le> sin x" .
@@ -1344,7 +1344,7 @@
       obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_even n. real x ^ m / real (fact m)) + exp t / real (fact (get_even n)) * (real x) ^ (get_even n)"
         using Maclaurin_exp_le unfolding atLeast0LessThan by blast
       moreover have "0 \<le> exp t / real (fact (get_even n)) * (real x) ^ (get_even n)"
-        by (auto simp: divide_nonneg_pos zero_le_even_power)
+        by (auto simp: zero_le_even_power)
       ultimately show ?thesis using get_odd exp_gt_zero by auto
     qed
     finally have "lb_exp_horner prec (get_even n) 1 1 x \<le> exp x" .
diff -r 282f3b06fa86 -r f4635657d66f src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Fields.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -1083,6 +1083,21 @@
   "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
 by (auto simp add: divide_less_eq)
 
+lemma divide_nonneg_nonneg [simp]:
+  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x / y"
+  by (auto simp add: divide_simps)
+
+lemma divide_nonpos_nonpos:
+  "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> 0 \<le> x / y"
+  by (auto simp add: divide_simps)
+
+lemma divide_nonneg_nonpos:
+  "0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> x / y \<le> 0"
+  by (auto simp add: divide_simps)
+
+lemma divide_nonpos_nonneg:
+  "x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x / y \<le> 0"
+  by (auto simp add: divide_simps)
 
 text {*Conditional Simplification Rules: No Case Splits*}
 
diff -r 282f3b06fa86 -r f4635657d66f src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Library/Convex.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -138,7 +138,7 @@
     with `0 \<le> setsum a s` have "0 < setsum a s" by simp
     then have "(\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C"
       using `\<forall>j\<in>s. 0 \<le> a j` and `\<forall>j\<in>s. y j \<in> C`
-      by (simp add: IH divide_nonneg_pos setsum_divide_distrib [symmetric])
+      by (simp add: IH setsum_divide_distrib [symmetric])
     from `convex C` and `y i \<in> C` and this and `0 \<le> a i`
       and `0 \<le> setsum a s` and `a i + setsum a s = 1`
     have "a i *\<^sub>R y i + setsum a s *\<^sub>R (\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C"
@@ -432,9 +432,7 @@
     then have "a i < 1" using asm by auto
     then have i0: "1 - a i > 0" by auto
     let ?a = "\<lambda>j. a j / (1 - a i)"
-    { fix j assume "j \<in> s"
-      then have "?a j \<ge> 0"
-        using i0 asms divide_nonneg_pos
+    { fix j assume "j \<in> s" with i0 asms have "?a j \<ge> 0"
         by fastforce }
     note a_nonneg = this
     have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
diff -r 282f3b06fa86 -r f4635657d66f src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Library/Float.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -1108,7 +1108,7 @@
   shows "0 \<le> real (lapprox_rat n x y)"
 using assms unfolding lapprox_rat_def p_def[symmetric] round_down_def real_of_int_minus[symmetric]
    powr_int[of 2, simplified]
-  by (auto simp add: inverse_eq_divide intro!: mult_nonneg_nonneg divide_nonneg_pos)
+  by auto
 
 lemma rapprox_rat: "real x / real y \<le> real (rapprox_rat prec x y)"
   using round_up by (simp add: rapprox_rat_def)
diff -r 282f3b06fa86 -r f4635657d66f src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -64,11 +64,6 @@
   apply auto
   done
 
-lemma divide_nonneg_nonneg:
-  fixes a b :: "'a :: {linordered_field, field_inverse_zero}"
-  shows "a \<ge> 0 \<Longrightarrow> b \<ge> 0 \<Longrightarrow> 0 \<le> a / b"
-  by (cases "b = 0") (auto intro!: divide_nonneg_pos)
-
 lemma setsum_Un_disjoint':
   assumes "finite A"
     and "finite B"
diff -r 282f3b06fa86 -r f4635657d66f src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -2262,10 +2262,7 @@
       using Min_ge_iff[of i 0 ] and obt(1)
       unfolding t_def i_def
       using obt(4)[unfolded le_less]
-      apply auto
-      unfolding divide_le_0_iff
-      apply auto
-      done
+      by (auto simp: divide_le_0_iff)
     have t: "\<forall>v\<in>s. u v + t * w v \<ge> 0"
     proof
       fix v
@@ -5056,7 +5053,7 @@
     apply(rule *[OF _ assms(2)])
     unfolding mem_Collect_eq
     using `b > 0` assms(3)
-    apply (auto intro!: divide_nonneg_pos)
+    apply auto
     done
   ultimately obtain u y where obt: "u\<ge>0" "u \<le> b / norm x" "y = u *\<^sub>R x"
     "y \<in> ?A" "y \<in> s" "\<forall>z\<in>?A \<inter> s. dist 0 z \<le> dist 0 y"
@@ -5218,8 +5215,6 @@
     from nor have y: "y = norm y *\<^sub>R ((inverse (norm x)) *\<^sub>R x)"
       unfolding as(3)[unfolded pi_def] by auto
     have "0 \<le> norm y * inverse (norm x)" and "0 \<le> norm x * inverse (norm y)"
-      unfolding divide_inverse[symmetric]
-      apply (rule_tac[!] divide_nonneg_pos)
       using nor
       apply auto
       done
@@ -5230,7 +5225,7 @@
       using x y and front_smul[THEN bspec, OF as(1), THEN spec[where x="norm y * (inverse (norm x))"]]
       using front_smul[THEN bspec, OF as(2), THEN spec[where x="norm x * (inverse (norm y))"]]
       using xys nor
-      apply (auto simp add:field_simps divide_le_eq_1 divide_inverse[symmetric])
+      apply (auto simp add: field_simps)
       done
     then show "x = y"
       apply (subst injpi[symmetric])
@@ -6412,9 +6407,7 @@
   next
     assume as: "dist a b = dist a x + dist x b"
     have "norm (a - x) / norm (a - b) \<le> 1"
-      unfolding divide_le_eq_1_pos[OF Fal2]
-      unfolding as[unfolded dist_norm] norm_ge_zero
-      by auto
+      using Fal2 unfolding as[unfolded dist_norm] norm_ge_zero by auto
     then show "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1"
       apply (rule_tac x="dist a x / dist a b" in exI)
       unfolding dist_norm
@@ -6422,8 +6415,7 @@
       apply rule
       defer
       apply rule
-      apply (rule divide_nonneg_pos)
-      prefer 4
+      prefer 3
       apply rule
     proof -
       fix i :: 'a
diff -r 282f3b06fa86 -r f4635657d66f src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -16,11 +16,6 @@
 lemma axis_in_Basis: "a \<in> Basis \<Longrightarrow> axis i a \<in> Basis"
   by (auto simp add: Basis_vec_def axis_eq_axis)
 
-lemma divide_nonneg_nonneg:
-  fixes a b :: "'a :: {linordered_field, field_inverse_zero}"
-  shows "a \<ge> 0 \<Longrightarrow> b \<ge> 0 \<Longrightarrow> 0 \<le> a / b"
-  by (cases "b = 0") (auto intro!: divide_nonneg_pos)
-
 subsection {*Bijections between intervals. *}
 
 definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
@@ -60,7 +55,7 @@
   have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i"
     using assms(1)[unfolded mem_box] using i by auto
   have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
-    using * x by (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
+    using * x by auto
   then show "u \<bullet> i \<le> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
     using * by auto
   have "((x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (v \<bullet> i - u \<bullet> i) \<le> 1 * (v \<bullet> i - u \<bullet> i)"
diff -r 282f3b06fa86 -r f4635657d66f src/HOL/Probability/Distributions.thy
--- a/src/HOL/Probability/Distributions.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Probability/Distributions.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -277,7 +277,7 @@
     unfolding emeasure_eq_ereal_measure[OF fin] using A by (simp add: measure_def)
   finally show "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) =
     ereal (measure lborel (A \<inter> {..a}) / r)" .
-qed (auto intro!: divide_nonneg_nonneg measure_nonneg)
+qed (auto simp: measure_nonneg)
 
 lemma (in prob_space) uniform_distrI_borel_atLeastAtMost:
   fixes a b :: real
diff -r 282f3b06fa86 -r f4635657d66f src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Probability/Information.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -130,7 +130,7 @@
     KL_divergence b (density M f) (density (density M f) (\<lambda>x. g x / f x))"
     using f g ac by (subst density_density_divide) simp_all
   also have "\<dots> = (\<integral>x. (g x / f x) * log b (g x / f x) \<partial>density M f)"
-    using f g `1 < b` by (intro Mf.KL_density) (auto simp: AE_density divide_nonneg_nonneg)
+    using f g `1 < b` by (intro Mf.KL_density) (auto simp: AE_density)
   also have "\<dots> = (\<integral>x. g x * log b (g x / f x) \<partial>M)"
     using ac f g `1 < b` by (subst integral_density) (auto intro!: integral_cong_AE)
   finally show ?thesis .
@@ -332,7 +332,7 @@
     from f g show "(\<lambda>x. g x / f x) \<in> borel_measurable (density M f)"
       by auto
     show "AE x in density M f. 0 \<le> g x / f x"
-      using f g by (auto simp: AE_density divide_nonneg_nonneg)
+      using f g by (auto simp: AE_density)
     show "integrable (density M f) (\<lambda>x. g x / f x * log b (g x / f x))"
       using `1 < b` f g ac
       by (subst integral_density)
@@ -804,8 +804,7 @@
     using D
     apply (subst eq_commute)
     apply (intro RN_deriv_unique_sigma_finite)
-    apply (auto intro: divide_nonneg_nonneg measure_nonneg
-             simp: distributed_distr_eq_density[symmetric, OF X] sf)
+    apply (auto simp: distributed_distr_eq_density[symmetric, OF X] sf measure_nonneg)
     done
 qed
 
@@ -1102,7 +1101,7 @@
     apply (rule positive_integral_mono_AE)
     using ae5 ae6 ae7 ae8
     apply eventually_elim
-    apply (auto intro!: divide_nonneg_nonneg)
+    apply auto
     done
   also have "\<dots> = (\<integral>\<^sup>+(y, z). \<integral>\<^sup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^sub>M P)"
     by (subst STP.positive_integral_snd_measurable[symmetric]) (auto simp add: split_beta')
@@ -1115,7 +1114,7 @@
       "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
     then show "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
       by (subst positive_integral_multc)
-         (auto intro!: divide_nonneg_nonneg split: prod.split)
+         (auto split: prod.split)
   qed
   also have "\<dots> = 1"
     using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
@@ -1151,7 +1150,7 @@
     apply simp
     using ae5 ae6 ae7 ae8
     apply eventually_elim
-    apply (auto intro!: divide_nonneg_nonneg)
+    apply auto
     done
 
   have I3: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
@@ -1347,7 +1346,7 @@
     apply (rule positive_integral_mono_AE)
     using ae5 ae6 ae7 ae8
     apply eventually_elim
-    apply (auto intro!: divide_nonneg_nonneg)
+    apply auto
     done
   also have "\<dots> = (\<integral>\<^sup>+(y, z). \<integral>\<^sup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^sub>M P)"
     by (subst STP.positive_integral_snd_measurable[symmetric])
@@ -1360,7 +1359,7 @@
     fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
       "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
     then show "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
-      by (subst positive_integral_multc) (auto intro!: divide_nonneg_nonneg)
+      by (subst positive_integral_multc) auto
   qed
   also have "\<dots> = 1"
     using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
@@ -1396,7 +1395,7 @@
     apply (auto simp: split_beta') []
     using ae5 ae6 ae7 ae8
     apply eventually_elim
-    apply (auto intro!: divide_nonneg_nonneg)
+    apply auto
     done
 
   have I3: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
diff -r 282f3b06fa86 -r f4635657d66f src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -303,7 +303,7 @@
                                      mult_nonpos_nonneg)
     next
       fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> ?g i x \<le> y"
-      have "\<And>i. 0 \<le> ?g i x" by (auto simp: divide_nonneg_pos)
+      have "\<And>i. 0 \<le> ?g i x" by auto
       from order_trans[OF this *] have "0 \<le> y" by simp
       show "max 0 (u x) \<le> y"
       proof (cases y)
@@ -330,7 +330,7 @@
         then show "max 0 (u x) \<le> y" using real ux by simp
       qed (insert `0 \<le> y`, auto)
     qed
-  qed (auto simp: divide_nonneg_pos)
+  qed auto
 qed
 
 lemma borel_measurable_implies_simple_function_sequence':
diff -r 282f3b06fa86 -r f4635657d66f src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Rat.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -578,7 +578,7 @@
     by (cases "b = 0", simp, simp add: of_int_rat)
   moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1"
     unfolding Fract_of_int_quotient
-    by (rule linorder_cases [of b 0]) (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos)
+    by (rule linorder_cases [of b 0]) (simp_all add: divide_nonpos_neg)
   ultimately show ?thesis by simp
 qed
 
diff -r 282f3b06fa86 -r f4635657d66f src/HOL/Real.thy
--- a/src/HOL/Real.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Real.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -1136,8 +1136,6 @@
   apply (simp add: algebra_simps)
   apply (subst real_of_int_div_aux)
   apply simp
-  apply (subst zero_le_divide_iff)
-  apply auto
   apply (simp add: algebra_simps)
   apply (subst real_of_int_div_aux)
   apply simp
@@ -1269,8 +1267,6 @@
 apply (simp add: algebra_simps)
 apply (subst real_of_nat_div_aux)
 apply simp
-apply (subst zero_le_divide_iff)
-apply simp
 done
 
 lemma real_of_nat_div3:
diff -r 282f3b06fa86 -r f4635657d66f src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Transcendental.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -1494,10 +1494,7 @@
   also have "- (x / (1 - x)) <= ..."
   proof -
     have "ln (1 + x / (1 - x)) <= x / (1 - x)"
-      apply (rule ln_add_one_self_le_self)
-      apply (rule divide_nonneg_pos)
-      using a c apply auto
-      done
+      using a c by (intro ln_add_one_self_le_self) auto
     thus ?thesis
       by auto
   qed
@@ -1586,11 +1583,8 @@
   also have "... = 1 + (y - x) / x"
     using x a by (simp add: field_simps)
   also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
-    apply (rule mult_left_mono)
-    apply (rule ln_add_one_self_le_self)
-    apply (rule divide_nonneg_pos)
-    using x a apply simp_all
-    done
+    using x a 
+    by (intro mult_left_mono ln_add_one_self_le_self) simp_all
   also have "... = y - x" using a by simp
   also have "... = (y - x) * ln (exp 1)" by simp
   also have "... <= (y - x) * ln x"
@@ -3906,9 +3900,6 @@
   hence low2: "- (pi / 2) < y / 2" and high2: "y / 2 < pi / 2"
     by auto
 
-  have divide_nonzero_divide: "\<And>A B C :: real. C \<noteq> 0 \<Longrightarrow> A / B = (A / C) / (B / C)"
-    by auto
-
   have "0 < cos y" using cos_gt_zero_pi[OF low high] .
   hence "cos y \<noteq> 0" and cos_sqrt: "sqrt ((cos y)\<^sup>2) = cos y"
     by auto
@@ -3922,7 +3913,7 @@
   finally have "1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2" .
 
   have "sin y / (cos y + 1) = tan y / ((cos y + 1) / cos y)"
-    unfolding tan_def divide_nonzero_divide[OF `cos y \<noteq> 0`, symmetric] ..
+    unfolding tan_def using `cos y \<noteq> 0` by (simp add: field_simps)
   also have "\<dots> = tan y / (1 + 1 / cos y)"
     using `cos y \<noteq> 0` unfolding add_divide_distrib by auto
   also have "\<dots> = tan y / (1 + 1 / sqrt ((cos y)\<^sup>2))"