Renamed setsum_mult to setsum_right_distrib.
--- 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.
--- 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
--- 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 *}
--- 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)"
--- 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
--- 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)";
--- 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
--- 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}"
--- 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)
--- 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)
--- 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])