Renamed setsum_mult to setsum_right_distrib.
authorballarin
Fri Mar 17 10:04:27 2006 +0100 (2006-03-17)
changeset 1927948b527d0331b
parent 19278 4d762b77d319
child 19280 5091dc43817b
Renamed setsum_mult to setsum_right_distrib.
NEWS
src/HOL/Binomial.thy
src/HOL/Finite_Set.thy
src/HOL/Hyperreal/HSeries.thy
src/HOL/Hyperreal/Integration.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/Library/ASeries.thy
src/HOL/Library/BigO.thy
src/HOL/Real/RealPow.thy
src/HOL/ex/ThreeDivides.thy
     1.1 --- a/NEWS	Fri Mar 17 09:57:25 2006 +0100
     1.2 +++ b/NEWS	Fri Mar 17 10:04:27 2006 +0100
     1.3 @@ -346,7 +346,7 @@
     1.4  25 like -->); output depends on the "iff" print_mode, the default is
     1.5  "A = B" (with priority 50).
     1.6  
     1.7 -* Renamed some (legacy-named) constants in HOL.thy and Orderings.thy:
     1.8 +* Renamed constants in HOL.thy and Orderings.thy:
     1.9      op +   ~> HOL.plus
    1.10      op -   ~> HOL.minus
    1.11      uminus ~> HOL.uminus
    1.12 @@ -385,6 +385,8 @@
    1.13  
    1.14  * Theorem Cons_eq_map_conv no longer has attribute `simp'.
    1.15  
    1.16 +* Theorem setsum_mult renamed to setsum_right_distrib.
    1.17 +
    1.18  * Prefer ex1I over ex_ex1I in single-step reasoning, e.g. by the
    1.19  'rule' method.
    1.20  
     2.1 --- a/src/HOL/Binomial.thy	Fri Mar 17 09:57:25 2006 +0100
     2.2 +++ b/src/HOL/Binomial.thy	Fri Mar 17 10:04:27 2006 +0100
     2.3 @@ -170,7 +170,7 @@
     2.4      by(rule nat_distrib)
     2.5    also have "\<dots> = (\<Sum>k=0..n. (n choose k) * a^(k+1) * b^(n-k)) +
     2.6                    (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k+1))"
     2.7 -    by(simp add: setsum_mult mult_ac)
     2.8 +    by(simp add: setsum_right_distrib mult_ac)
     2.9    also have "\<dots> = (\<Sum>k=0..n. (n choose k) * a^k * b^(n+1-k)) +
    2.10                    (\<Sum>k=1..n+1. (n choose (k - 1)) * a^k * b^(n+1-k))"
    2.11      by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le
     3.1 --- a/src/HOL/Finite_Set.thy	Fri Mar 17 09:57:25 2006 +0100
     3.2 +++ b/src/HOL/Finite_Set.thy	Fri Mar 17 10:04:27 2006 +0100
     3.3 @@ -1145,10 +1145,7 @@
     3.4    apply auto
     3.5  done
     3.6  
     3.7 -(* FIXME: this is distributitivty, name as such! *)
     3.8 -(* suggested name: setsum_right_distrib (CB) *)
     3.9 -
    3.10 -lemma setsum_mult: 
    3.11 +lemma setsum_right_distrib: 
    3.12    fixes f :: "'a => ('b::semiring_0_cancel)"
    3.13    shows "r * setsum f A = setsum (%n. r * f n) A"
    3.14  proof (cases "finite A")
    3.15 @@ -1270,6 +1267,11 @@
    3.16    finally show "?s = ?t" .
    3.17  qed
    3.18  
    3.19 +lemma setsum_product:
    3.20 +  fixes f :: "nat => ('a::semiring_0_cancel)"
    3.21 +  shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
    3.22 +  by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
    3.23 +
    3.24  
    3.25  subsection {* Generalized product over a set *}
    3.26  
     4.1 --- a/src/HOL/Hyperreal/HSeries.thy	Fri Mar 17 09:57:25 2006 +0100
     4.2 +++ b/src/HOL/Hyperreal/HSeries.thy	Fri Mar 17 10:04:27 2006 +0100
     4.3 @@ -73,7 +73,7 @@
     4.4  
     4.5  lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
     4.6  apply (cases m, cases n)
     4.7 -apply (simp add: sumhr star_of_def star_n_mult setsum_mult)
     4.8 +apply (simp add: sumhr star_of_def star_n_mult setsum_right_distrib)
     4.9  done
    4.10  
    4.11  lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
     5.1 --- a/src/HOL/Hyperreal/Integration.thy	Fri Mar 17 09:57:25 2006 +0100
     5.2 +++ b/src/HOL/Hyperreal/Integration.thy	Fri Mar 17 10:04:27 2006 +0100
     5.3 @@ -345,7 +345,7 @@
     5.4  lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c)  (c*(b - a))"
     5.5  apply (auto simp add: order_le_less rsum_def Integral_def)
     5.6  apply (rule_tac x = "%x. b - a" in exI)
     5.7 -apply (auto simp add: setsum_mult [symmetric] gauge_def abs_interval_iff 
     5.8 +apply (auto simp add: setsum_right_distrib [symmetric] gauge_def abs_interval_iff 
     5.9                 right_diff_distrib [symmetric] partition tpart_def)
    5.10  done
    5.11  
    5.12 @@ -353,7 +353,7 @@
    5.13       "[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
    5.14  apply (auto simp add: order_le_less 
    5.15              dest: Integral_unique [OF order_refl Integral_zero])
    5.16 -apply (auto simp add: rsum_def Integral_def setsum_mult[symmetric] mult_assoc)
    5.17 +apply (auto simp add: rsum_def Integral_def setsum_right_distrib[symmetric] mult_assoc)
    5.18  apply (rule_tac a2 = c in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
    5.19   prefer 2 apply force
    5.20  apply (drule_tac x = "e/abs c" in spec, auto)
    5.21 @@ -463,7 +463,7 @@
    5.22  apply (simp add: abs_minus_commute)
    5.23  apply (rule_tac t = ea in ssubst, assumption)
    5.24  apply (rule setsum_mono)
    5.25 -apply (rule_tac [2] setsum_mult [THEN subst])
    5.26 +apply (rule_tac [2] setsum_right_distrib [THEN subst])
    5.27  apply (auto simp add: partition_rhs partition_lhs partition_lb partition_ub
    5.28            fine_def)
    5.29  done
     6.1 --- a/src/HOL/Hyperreal/Series.thy	Fri Mar 17 09:57:25 2006 +0100
     6.2 +++ b/src/HOL/Hyperreal/Series.thy	Fri Mar 17 10:04:27 2006 +0100
     6.3 @@ -168,7 +168,7 @@
     6.4  done;
     6.5    
     6.6  lemma sums_mult: "f sums a ==> (%n. c * f n) sums (c * a)"
     6.7 -by (auto simp add: sums_def setsum_mult [symmetric]
     6.8 +by (auto simp add: sums_def setsum_right_distrib [symmetric]
     6.9           intro!: LIMSEQ_mult intro: LIMSEQ_const)
    6.10  
    6.11  lemma summable_mult: "summable f ==> summable (%n. c * f n)";
     7.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Fri Mar 17 09:57:25 2006 +0100
     7.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Fri Mar 17 10:04:27 2006 +0100
     7.3 @@ -360,7 +360,7 @@
     7.4  lemma lemma_realpow_diff_sumr:
     7.5       "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ ((Suc n) - p)) =  
     7.6        y * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))::real)"
     7.7 -by (auto simp add: setsum_mult lemma_realpow_diff mult_ac
     7.8 +by (auto simp add: setsum_right_distrib lemma_realpow_diff mult_ac
     7.9    simp del: setsum_op_ivl_Suc cong: strong_setsum_cong)
    7.10  
    7.11  lemma lemma_realpow_diff_sumr2:
    7.12 @@ -491,10 +491,10 @@
    7.13              simp del: realpow_Suc setsum_op_ivl_Suc)
    7.14  apply (auto simp add: lemma_realpow_rev_sumr simp del: setsum_op_ivl_Suc)
    7.15  apply (auto simp add: real_of_nat_Suc sumr_diff_mult_const left_distrib 
    7.16 -                sumdiff lemma_termdiff1 setsum_mult)
    7.17 +                sumdiff lemma_termdiff1 setsum_right_distrib)
    7.18  apply (auto intro!: setsum_cong[OF refl] simp add: diff_minus real_add_assoc)
    7.19  apply (simp add: diff_minus [symmetric] less_iff_Suc_add)
    7.20 -apply (auto simp add: setsum_mult lemma_realpow_diff_sumr2 mult_ac simp
    7.21 +apply (auto simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac simp
    7.22                   del: setsum_op_ivl_Suc realpow_Suc)
    7.23  done
    7.24  
     8.1 --- a/src/HOL/Library/ASeries.thy	Fri Mar 17 09:57:25 2006 +0100
     8.2 +++ b/src/HOL/Library/ASeries.thy	Fri Mar 17 10:04:27 2006 +0100
     8.3 @@ -73,7 +73,7 @@
     8.4      by (rule setsum_addf)
     8.5    also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
     8.6    also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
     8.7 -    by (simp add: setsum_mult setsum_head_upt)
     8.8 +    by (simp add: setsum_right_distrib setsum_head_upt)
     8.9    also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
    8.10      by simp
    8.11    also from ngt1 have "{1..<n} = {1..n - 1}"
     9.1 --- a/src/HOL/Library/BigO.thy	Fri Mar 17 09:57:25 2006 +0100
     9.2 +++ b/src/HOL/Library/BigO.thy	Fri Mar 17 10:04:27 2006 +0100
     9.3 @@ -582,7 +582,7 @@
     9.4    apply (subst abs_of_nonneg) back back
     9.5    apply (rule setsum_nonneg)
     9.6    apply force
     9.7 -  apply (subst setsum_mult)
     9.8 +  apply (subst setsum_right_distrib)
     9.9    apply (rule allI)
    9.10    apply (rule order_trans)
    9.11    apply (rule setsum_abs)
    10.1 --- a/src/HOL/Real/RealPow.thy	Fri Mar 17 09:57:25 2006 +0100
    10.2 +++ b/src/HOL/Real/RealPow.thy	Fri Mar 17 10:04:27 2006 +0100
    10.3 @@ -231,6 +231,32 @@
    10.4  lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
    10.5  by (auto simp add: power2_eq_square)
    10.6  
    10.7 +(* The following theorem is by Benjamin Porter *)
    10.8 +lemma real_sq_order:
    10.9 +  fixes x::real
   10.10 +  assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2"
   10.11 +  shows "x \<le> y"
   10.12 +proof (rule ccontr)
   10.13 +  assume "\<not>(x \<le> y)"
   10.14 +  then have ylx: "y < x" by simp
   10.15 +  hence "y \<le> x" by simp
   10.16 +  with xgt0 have "x*y \<le> x*x"
   10.17 +    by (simp add: pordered_comm_semiring_class.mult_mono)
   10.18 +  moreover
   10.19 +  have "\<not> (y = 0)"
   10.20 +  proof
   10.21 +    assume "y = 0"
   10.22 +    with ylx have xg0: "0 < x" by simp
   10.23 +    from xg0 xg0 have "0 < x*x" by (rule real_mult_order)
   10.24 +    moreover have "y*y = 0" by simp
   10.25 +    ultimately show False using sq by auto
   10.26 +  qed
   10.27 +  with ygt0 have "0 < y" by simp
   10.28 +  with ylx have "y*y < x*y" by auto
   10.29 +  ultimately have "y*y < x*x" by simp
   10.30 +  with sq show False by (auto simp add: power2_eq_square [symmetric])
   10.31 +qed
   10.32 +
   10.33  lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
   10.34  by (case_tac "n", auto)
   10.35  
    11.1 --- a/src/HOL/ex/ThreeDivides.thy	Fri Mar 17 09:57:25 2006 +0100
    11.2 +++ b/src/HOL/ex/ThreeDivides.thy	Fri Mar 17 10:04:27 2006 +0100
    11.3 @@ -197,7 +197,7 @@
    11.4        "m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp
    11.5      also have
    11.6        "\<dots> = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^(x+1)) + c"
    11.7 -      by (subst setsum_mult) (simp add: mult_ac)
    11.8 +      by (subst setsum_right_distrib) (simp add: mult_ac)
    11.9      also have
   11.10        "\<dots> = (\<Sum>x<nd. m div 10^(Suc x) mod 10 * 10^(Suc x)) + c"
   11.11        by (simp add: div_mult2_eq[symmetric])