# HG changeset patch
# User ballarin
# Date 1142586267 -3600
# Node ID 48b527d0331b09cf812104bf486733910ee84682
# Parent  4d762b77d319d5684982e0dd455e6f6bf964419c
Renamed setsum_mult to setsum_right_distrib.

diff -r 4d762b77d319 -r 48b527d0331b NEWS
--- a/NEWS	Fri Mar 17 09:57:25 2006 +0100
+++ b/NEWS	Fri Mar 17 10:04:27 2006 +0100
@@ -346,7 +346,7 @@
 25 like -->); output depends on the "iff" print_mode, the default is
 "A = B" (with priority 50).
 
-* Renamed some (legacy-named) constants in HOL.thy and Orderings.thy:
+* Renamed constants in HOL.thy and Orderings.thy:
     op +   ~> HOL.plus
     op -   ~> HOL.minus
     uminus ~> HOL.uminus
@@ -385,6 +385,8 @@
 
 * Theorem Cons_eq_map_conv no longer has attribute `simp'.
 
+* Theorem setsum_mult renamed to setsum_right_distrib.
+
 * Prefer ex1I over ex_ex1I in single-step reasoning, e.g. by the
 'rule' method.
 
diff -r 4d762b77d319 -r 48b527d0331b src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Fri Mar 17 09:57:25 2006 +0100
+++ b/src/HOL/Binomial.thy	Fri Mar 17 10:04:27 2006 +0100
@@ -170,7 +170,7 @@
     by(rule nat_distrib)
   also have "\<dots> = (\<Sum>k=0..n. (n choose k) * a^(k+1) * b^(n-k)) +
                   (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k+1))"
-    by(simp add: setsum_mult mult_ac)
+    by(simp add: setsum_right_distrib mult_ac)
   also have "\<dots> = (\<Sum>k=0..n. (n choose k) * a^k * b^(n+1-k)) +
                   (\<Sum>k=1..n+1. (n choose (k - 1)) * a^k * b^(n+1-k))"
     by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le
diff -r 4d762b77d319 -r 48b527d0331b src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Mar 17 09:57:25 2006 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Mar 17 10:04:27 2006 +0100
@@ -1145,10 +1145,7 @@
   apply auto
 done
 
-(* FIXME: this is distributitivty, name as such! *)
-(* suggested name: setsum_right_distrib (CB) *)
-
-lemma setsum_mult: 
+lemma setsum_right_distrib: 
   fixes f :: "'a => ('b::semiring_0_cancel)"
   shows "r * setsum f A = setsum (%n. r * f n) A"
 proof (cases "finite A")
@@ -1270,6 +1267,11 @@
   finally show "?s = ?t" .
 qed
 
+lemma setsum_product:
+  fixes f :: "nat => ('a::semiring_0_cancel)"
+  shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
+  by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
+
 
 subsection {* Generalized product over a set *}
 
diff -r 4d762b77d319 -r 48b527d0331b src/HOL/Hyperreal/HSeries.thy
--- a/src/HOL/Hyperreal/HSeries.thy	Fri Mar 17 09:57:25 2006 +0100
+++ b/src/HOL/Hyperreal/HSeries.thy	Fri Mar 17 10:04:27 2006 +0100
@@ -73,7 +73,7 @@
 
 lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
 apply (cases m, cases n)
-apply (simp add: sumhr star_of_def star_n_mult setsum_mult)
+apply (simp add: sumhr star_of_def star_n_mult setsum_right_distrib)
 done
 
 lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
diff -r 4d762b77d319 -r 48b527d0331b src/HOL/Hyperreal/Integration.thy
--- a/src/HOL/Hyperreal/Integration.thy	Fri Mar 17 09:57:25 2006 +0100
+++ b/src/HOL/Hyperreal/Integration.thy	Fri Mar 17 10:04:27 2006 +0100
@@ -345,7 +345,7 @@
 lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c)  (c*(b - a))"
 apply (auto simp add: order_le_less rsum_def Integral_def)
 apply (rule_tac x = "%x. b - a" in exI)
-apply (auto simp add: setsum_mult [symmetric] gauge_def abs_interval_iff 
+apply (auto simp add: setsum_right_distrib [symmetric] gauge_def abs_interval_iff 
                right_diff_distrib [symmetric] partition tpart_def)
 done
 
@@ -353,7 +353,7 @@
      "[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
 apply (auto simp add: order_le_less 
             dest: Integral_unique [OF order_refl Integral_zero])
-apply (auto simp add: rsum_def Integral_def setsum_mult[symmetric] mult_assoc)
+apply (auto simp add: rsum_def Integral_def setsum_right_distrib[symmetric] mult_assoc)
 apply (rule_tac a2 = c in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
  prefer 2 apply force
 apply (drule_tac x = "e/abs c" in spec, auto)
@@ -463,7 +463,7 @@
 apply (simp add: abs_minus_commute)
 apply (rule_tac t = ea in ssubst, assumption)
 apply (rule setsum_mono)
-apply (rule_tac [2] setsum_mult [THEN subst])
+apply (rule_tac [2] setsum_right_distrib [THEN subst])
 apply (auto simp add: partition_rhs partition_lhs partition_lb partition_ub
           fine_def)
 done
diff -r 4d762b77d319 -r 48b527d0331b src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Fri Mar 17 09:57:25 2006 +0100
+++ b/src/HOL/Hyperreal/Series.thy	Fri Mar 17 10:04:27 2006 +0100
@@ -168,7 +168,7 @@
 done;
   
 lemma sums_mult: "f sums a ==> (%n. c * f n) sums (c * a)"
-by (auto simp add: sums_def setsum_mult [symmetric]
+by (auto simp add: sums_def setsum_right_distrib [symmetric]
          intro!: LIMSEQ_mult intro: LIMSEQ_const)
 
 lemma summable_mult: "summable f ==> summable (%n. c * f n)";
diff -r 4d762b77d319 -r 48b527d0331b src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Fri Mar 17 09:57:25 2006 +0100
+++ b/src/HOL/Hyperreal/Transcendental.thy	Fri Mar 17 10:04:27 2006 +0100
@@ -360,7 +360,7 @@
 lemma lemma_realpow_diff_sumr:
      "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ ((Suc n) - p)) =  
       y * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))::real)"
-by (auto simp add: setsum_mult lemma_realpow_diff mult_ac
+by (auto simp add: setsum_right_distrib lemma_realpow_diff mult_ac
   simp del: setsum_op_ivl_Suc cong: strong_setsum_cong)
 
 lemma lemma_realpow_diff_sumr2:
@@ -491,10 +491,10 @@
             simp del: realpow_Suc setsum_op_ivl_Suc)
 apply (auto simp add: lemma_realpow_rev_sumr simp del: setsum_op_ivl_Suc)
 apply (auto simp add: real_of_nat_Suc sumr_diff_mult_const left_distrib 
-                sumdiff lemma_termdiff1 setsum_mult)
+                sumdiff lemma_termdiff1 setsum_right_distrib)
 apply (auto intro!: setsum_cong[OF refl] simp add: diff_minus real_add_assoc)
 apply (simp add: diff_minus [symmetric] less_iff_Suc_add)
-apply (auto simp add: setsum_mult lemma_realpow_diff_sumr2 mult_ac simp
+apply (auto simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac simp
                  del: setsum_op_ivl_Suc realpow_Suc)
 done
 
diff -r 4d762b77d319 -r 48b527d0331b src/HOL/Library/ASeries.thy
--- a/src/HOL/Library/ASeries.thy	Fri Mar 17 09:57:25 2006 +0100
+++ b/src/HOL/Library/ASeries.thy	Fri Mar 17 10:04:27 2006 +0100
@@ -73,7 +73,7 @@
     by (rule setsum_addf)
   also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
   also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
-    by (simp add: setsum_mult setsum_head_upt)
+    by (simp add: setsum_right_distrib setsum_head_upt)
   also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
     by simp
   also from ngt1 have "{1..<n} = {1..n - 1}"
diff -r 4d762b77d319 -r 48b527d0331b src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Fri Mar 17 09:57:25 2006 +0100
+++ b/src/HOL/Library/BigO.thy	Fri Mar 17 10:04:27 2006 +0100
@@ -582,7 +582,7 @@
   apply (subst abs_of_nonneg) back back
   apply (rule setsum_nonneg)
   apply force
-  apply (subst setsum_mult)
+  apply (subst setsum_right_distrib)
   apply (rule allI)
   apply (rule order_trans)
   apply (rule setsum_abs)
diff -r 4d762b77d319 -r 48b527d0331b src/HOL/Real/RealPow.thy
--- a/src/HOL/Real/RealPow.thy	Fri Mar 17 09:57:25 2006 +0100
+++ b/src/HOL/Real/RealPow.thy	Fri Mar 17 10:04:27 2006 +0100
@@ -231,6 +231,32 @@
 lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
 by (auto simp add: power2_eq_square)
 
+(* The following theorem is by Benjamin Porter *)
+lemma real_sq_order:
+  fixes x::real
+  assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2"
+  shows "x \<le> y"
+proof (rule ccontr)
+  assume "\<not>(x \<le> y)"
+  then have ylx: "y < x" by simp
+  hence "y \<le> x" by simp
+  with xgt0 have "x*y \<le> x*x"
+    by (simp add: pordered_comm_semiring_class.mult_mono)
+  moreover
+  have "\<not> (y = 0)"
+  proof
+    assume "y = 0"
+    with ylx have xg0: "0 < x" by simp
+    from xg0 xg0 have "0 < x*x" by (rule real_mult_order)
+    moreover have "y*y = 0" by simp
+    ultimately show False using sq by auto
+  qed
+  with ygt0 have "0 < y" by simp
+  with ylx have "y*y < x*y" by auto
+  ultimately have "y*y < x*x" by simp
+  with sq show False by (auto simp add: power2_eq_square [symmetric])
+qed
+
 lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
 by (case_tac "n", auto)
 
diff -r 4d762b77d319 -r 48b527d0331b src/HOL/ex/ThreeDivides.thy
--- a/src/HOL/ex/ThreeDivides.thy	Fri Mar 17 09:57:25 2006 +0100
+++ b/src/HOL/ex/ThreeDivides.thy	Fri Mar 17 10:04:27 2006 +0100
@@ -197,7 +197,7 @@
       "m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp
     also have
       "\<dots> = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^(x+1)) + c"
-      by (subst setsum_mult) (simp add: mult_ac)
+      by (subst setsum_right_distrib) (simp add: mult_ac)
     also have
       "\<dots> = (\<Sum>x<nd. m div 10^(Suc x) mod 10 * 10^(Suc x)) + c"
       by (simp add: div_mult2_eq[symmetric])