--- a/NEWS Mon Oct 30 16:02:59 2017 +0000
+++ b/NEWS Mon Oct 30 16:03:21 2017 +0000
@@ -63,6 +63,9 @@
* Session HOL-Analysis: Moebius functions and the Riemann mapping
theorem.
+* Class linordered_semiring_1 covers zero_less_one also, ruling out
+pathologic instances. Minor INCOMPATIBILITY.
+
*** System ***
--- a/src/HOL/Analysis/Gamma_Function.thy Mon Oct 30 16:02:59 2017 +0000
+++ b/src/HOL/Analysis/Gamma_Function.thy Mon Oct 30 16:03:21 2017 +0000
@@ -152,10 +152,10 @@
fix z
show "(\<Sum>n. of_real (sin_coeff (n+1)) * z^n) = ?f z"
by (cases "z = 0") (insert sin_z_over_z_series'[of z],
- simp_all add: scaleR_conv_of_real sums_iff powser_zero sin_coeff_def)
+ simp_all add: scaleR_conv_of_real sums_iff sin_coeff_def)
qed
also have "(\<Sum>n. diffs (\<lambda>n. of_real (sin_coeff (n + 1))) n * (0::'a) ^ n) =
- diffs (\<lambda>n. of_real (sin_coeff (Suc n))) 0" by (simp add: powser_zero)
+ diffs (\<lambda>n. of_real (sin_coeff (Suc n))) 0" by simp
also have "\<dots> = 0" by (simp add: sin_coeff_def diffs_def)
finally show "((\<lambda>z::'a. if z = 0 then 1 else sin z / z) has_field_derivative 0) (at 0)" .
qed
@@ -520,7 +520,7 @@
unfolding pochhammer_prod
by (simp add: prod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
also have "of_nat n powr z / (pochhammer z (Suc n) / fact n) = Gamma_series z n"
- unfolding Gamma_series_def using assms by (simp add: divide_simps powr_def Ln_of_nat)
+ unfolding Gamma_series_def using assms by (simp add: divide_simps powr_def)
finally show ?thesis .
qed
@@ -656,8 +656,7 @@
also have "(\<Sum>n\<in>\<dots>. f n) = (\<Sum>n<k. f n) + (\<Sum>n=k..<m+k. f n)"
by (rule sum.union_disjoint) auto
also have "(\<Sum>n=k..<m+k. f n) = (\<Sum>n=0..<m+k-k. f (n + k))"
- by (intro sum.reindex_cong[of "\<lambda>n. n + k"])
- (simp, subst image_add_atLeastLessThan, auto)
+ using sum_shift_bounds_nat_ivl [of f 0 k m] by simp
finally show "(\<Sum>n<k. f n) + (\<Sum>n<m. f (n + k)) = (\<Sum>n<m+k. f n)" by (simp add: atLeast0LessThan)
qed
finally have "(\<lambda>a. sum f {..<a}) \<longlonglongrightarrow> lim (\<lambda>m. sum f {..<m + k})"
@@ -2295,7 +2294,7 @@
unfolding h_def using that by (auto intro!: Reals_mult Reals_add Reals_diff Polygamma_Real)
from h'_zero h_h'_2 have "\<exists>c. \<forall>z\<in>UNIV. h z = c"
- by (intro has_field_derivative_zero_constant) (simp_all add: dist_0_norm)
+ by (intro has_field_derivative_zero_constant) simp_all
then obtain c where c: "\<And>z. h z = c" by auto
have "\<exists>u. u \<in> closed_segment 0 1 \<and> Re (g 1) - Re (g 0) = Re (h u * g u * (1 - 0))"
by (intro complex_mvt_line g_g')
@@ -2861,7 +2860,7 @@
have "((\<lambda>x. exp ((z - 1) * of_real (ln x)) * (1 - of_real x / of_nat n) ^ n)
has_integral (?I * exp ((z - 1) * ln (of_nat n)))) {0..real n}" (is ?P)
by (insert B, subst (asm) mult.assoc [symmetric], subst (asm) exp_add [symmetric])
- (simp add: Ln_of_nat algebra_simps)
+ (simp add: algebra_simps)
also have "?P \<longleftrightarrow> ((\<lambda>x. of_real x powr (z - 1) * (1 - of_real x / of_nat n) ^ n)
has_integral (?I * exp ((z - 1) * ln (of_nat n)))) {0..real n}"
by (intro has_integral_spike_finite_eq[of "{0}"]) (simp_all add: powr_def Ln_of_real)
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy Mon Oct 30 16:02:59 2017 +0000
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Mon Oct 30 16:03:21 2017 +0000
@@ -1424,7 +1424,7 @@
define A where "A = Abs_multiset f"
from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
with S(2) have nz: "n \<noteq> 0" by auto
- from S_eq \<open>finite S\<close> have count_A: "count A x = f x" for x
+ from S_eq \<open>finite S\<close> have count_A: "count A = f"
unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def)
from S_eq count_A have set_mset_A: "set_mset A = S"
by (simp only: set_mset_def)
@@ -1452,7 +1452,8 @@
also from S(1) p
have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A"
by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other)
- also have "sum_mset \<dots> = f p" by (simp add: sum_mset_delta' count_A)
+ also have "sum_mset \<dots> = f p"
+ by (simp add: semiring_1_class.sum_mset_delta' count_A)
finally show "f p = multiplicity p n" ..
qed
qed
--- a/src/HOL/GCD.thy Mon Oct 30 16:02:59 2017 +0000
+++ b/src/HOL/GCD.thy Mon Oct 30 16:03:21 2017 +0000
@@ -1600,13 +1600,10 @@
by simp
next
case False
- then have "inj (times b)"
- by (rule inj_times)
show ?thesis proof (cases "finite A")
case False
- moreover from \<open>inj (times b)\<close>
- have "inj_on (times b) A"
- by (rule inj_on_subset) simp
+ moreover have "inj_on (times b) A"
+ using \<open>b \<noteq> 0\<close> by (rule inj_on_mult)
ultimately have "infinite (times b ` A)"
by (simp add: finite_image_iff)
with False show ?thesis
--- a/src/HOL/Groups_Big.thy Mon Oct 30 16:02:59 2017 +0000
+++ b/src/HOL/Groups_Big.thy Mon Oct 30 16:03:21 2017 +0000
@@ -761,31 +761,16 @@
"finite F \<Longrightarrow> (sum f F = 0) = (\<forall>a\<in>F. f a = 0)"
by (intro ballI sum_nonneg_eq_0_iff zero_le)
-lemma sum_distrib_left: "r * sum f A = sum (\<lambda>n. r * f n) A"
- for f :: "'a \<Rightarrow> 'b::semiring_0"
-proof (induct A rule: infinite_finite_induct)
- case infinite
- then show ?case by simp
-next
- case empty
- then show ?case by simp
-next
- case insert
- then show ?case by (simp add: distrib_left)
-qed
+context semiring_0
+begin
+
+lemma sum_distrib_left: "r * sum f A = (\<Sum>n\<in>A. r * f n)"
+ by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)
lemma sum_distrib_right: "sum f A * r = (\<Sum>n\<in>A. f n * r)"
- for r :: "'a::semiring_0"
-proof (induct A rule: infinite_finite_induct)
- case infinite
- then show ?case by simp
-next
- case empty
- then show ?case by simp
-next
- case insert
- then show ?case by (simp add: distrib_right)
-qed
+ by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)
+
+end
lemma sum_divide_distrib: "sum f A / r = (\<Sum>n\<in>A. f n / r)"
for r :: "'a::field"
@@ -958,8 +943,14 @@
by (simp add: card.eq_fold sum.eq_fold)
qed
-lemma sum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
- by (induct A rule: infinite_finite_induct) (auto simp: algebra_simps)
+context semiring_1
+begin
+
+lemma sum_constant [simp]:
+ "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
+ by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)
+
+end
lemma sum_Suc: "sum (\<lambda>x. Suc(f x)) A = sum f A + card A"
using sum.distrib[of f "\<lambda>_. 1" A] by simp
--- a/src/HOL/Inequalities.thy Mon Oct 30 16:02:59 2017 +0000
+++ b/src/HOL/Inequalities.thy Mon Oct 30 16:03:21 2017 +0000
@@ -7,49 +7,6 @@
imports Real_Vector_Spaces
begin
-lemma Sum_Icc_int: "(m::int) \<le> n \<Longrightarrow> \<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
-proof(induct i == "nat(n-m)" arbitrary: m n)
- case 0
- hence "m = n" by arith
- thus ?case by (simp add: algebra_simps)
-next
- case (Suc i)
- have 0: "i = nat((n-1) - m)" "m \<le> n-1" using Suc(2,3) by arith+
- have "\<Sum> {m..n} = \<Sum> {m..1+(n-1)}" by simp
- also have "\<dots> = \<Sum> {m..n-1} + n" using \<open>m \<le> n\<close>
- by(subst atLeastAtMostPlus1_int_conv) simp_all
- also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n"
- by(simp add: Suc(1)[OF 0])
- also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp
- also have "\<dots> = (n*(n+1) - m*(m-1)) div 2" by(simp add: algebra_simps)
- finally show ?case .
-qed
-
-lemma Sum_Icc_nat: assumes "(m::nat) \<le> n"
-shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
-proof -
- have "m*(m-1) \<le> n*(n + 1)"
- using assms by (meson diff_le_self order_trans le_add1 mult_le_mono)
- hence "int(\<Sum> {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms
- by (auto simp: Sum_Icc_int[transferred, OF assms] zdiv_int of_nat_mult simp del: of_nat_sum
- split: zdiff_int_split)
- thus ?thesis
- using of_nat_eq_iff by blast
-qed
-
-lemma Sum_Ico_nat: assumes "(m::nat) \<le> n"
-shows "\<Sum> {m..<n} = (n*(n-1) - m*(m-1)) div 2"
-proof cases
- assume "m < n"
- hence "{m..<n} = {m..n-1}" by auto
- hence "\<Sum>{m..<n} = \<Sum>{m..n-1}" by simp
- also have "\<dots> = (n*(n-1) - m*(m-1)) div 2"
- using assms \<open>m < n\<close> by (simp add: Sum_Icc_nat mult.commute)
- finally show ?thesis .
-next
- assume "\<not> m < n" with assms show ?thesis by simp
-qed
-
lemma Chebyshev_sum_upper:
fixes a b::"nat \<Rightarrow> 'a::linordered_idom"
assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> a i \<le> a j"
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Mon Oct 30 16:02:59 2017 +0000
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Mon Oct 30 16:03:21 2017 +0000
@@ -42,7 +42,7 @@
have "(\<Sum>j<k + i. f j) = (\<Sum>j=i..<k + i. f j) + (\<Sum>j=0..<i. f j)"
by (subst sum.union_disjoint[symmetric]) (auto intro!: sum.cong)
also have "(\<Sum>j=i..<k + i. f j) = (\<Sum>j\<in>(\<lambda>n. n + i)`{0..<k}. f j)"
- unfolding image_add_atLeastLessThan by simp
+ unfolding image_add_atLeast_lessThan by simp
finally have "(\<Sum>j<k + i. f j) = (\<Sum>n<k. f (n + i)) + (\<Sum>j<i. f j)"
by (auto simp: inj_on_def atLeast0LessThan sum.reindex) }
ultimately have "(\<lambda>k. (\<Sum>n<k + i. f n)) \<longlonglongrightarrow> l + (\<Sum>j<i. f j)"
--- a/src/HOL/Library/Extended_Real.thy Mon Oct 30 16:02:59 2017 +0000
+++ b/src/HOL/Library/Extended_Real.thy Mon Oct 30 16:03:21 2017 +0000
@@ -3381,18 +3381,20 @@
shows "(\<Sum>i. f (i + k)) \<le> suminf f"
proof -
have "(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k))"
- using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
+ using summable_sums[OF summable_ereal_pos]
+ by (simp add: sums_def atLeast0LessThan f)
moreover have "(\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> (\<Sum>i. f i)"
- using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
+ using summable_sums[OF summable_ereal_pos]
+ by (simp add: sums_def atLeast0LessThan f)
then have "(\<lambda>n. \<Sum>i<n + k. f i) \<longlonglongrightarrow> (\<Sum>i. f i)"
by (rule LIMSEQ_ignore_initial_segment)
ultimately show ?thesis
proof (rule LIMSEQ_le, safe intro!: exI[of _ k])
fix n assume "k \<le> n"
- have "(\<Sum>i<n. f (i + k)) = (\<Sum>i<n. (f \<circ> (\<lambda>i. i + k)) i)"
- by simp
- also have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
- by (subst sum.reindex) auto
+ have "(\<Sum>i<n. f (i + k)) = (\<Sum>i<n. (f \<circ> plus k) i)"
+ by (simp add: ac_simps)
+ also have "\<dots> = (\<Sum>i\<in>(plus k) ` {..<n}. f i)"
+ by (rule sum.reindex [symmetric]) simp
also have "\<dots> \<le> sum f {..<n + k}"
by (intro sum_mono2) (auto simp: f)
finally show "(\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}" .
--- a/src/HOL/Library/Multiset.thy Mon Oct 30 16:02:59 2017 +0000
+++ b/src/HOL/Library/Multiset.thy Mon Oct 30 16:03:21 2017 +0000
@@ -2247,52 +2247,12 @@
sublocale sum_mset: comm_monoid_mset plus 0
defines sum_mset = sum_mset.F ..
-lemma (in semiring_1) sum_mset_replicate_mset [simp]:
- "sum_mset (replicate_mset n a) = of_nat n * a"
- by (induct n) (simp_all add: algebra_simps)
-
lemma sum_unfold_sum_mset:
"sum f A = sum_mset (image_mset f (mset_set A))"
by (cases "finite A") (induct A rule: finite_induct, simp_all)
-lemma sum_mset_delta: "sum_mset (image_mset (\<lambda>x. if x = y then c else 0) A) = c * count A y"
- by (induction A) simp_all
-
-lemma sum_mset_delta': "sum_mset (image_mset (\<lambda>x. if y = x then c else 0) A) = c * count A y"
- by (induction A) simp_all
-
end
-lemma of_nat_sum_mset [simp]:
- "of_nat (sum_mset M) = sum_mset (image_mset of_nat M)"
-by (induction M) auto
-
-lemma sum_mset_0_iff [simp]:
- "sum_mset M = (0::'a::canonically_ordered_monoid_add)
- \<longleftrightarrow> (\<forall>x \<in> set_mset M. x = 0)"
-by(induction M) auto
-
-lemma sum_mset_diff:
- fixes M N :: "('a :: ordered_cancel_comm_monoid_diff) multiset"
- shows "N \<subseteq># M \<Longrightarrow> sum_mset (M - N) = sum_mset M - sum_mset N"
- by (metis add_diff_cancel_right' sum_mset.union subset_mset.diff_add)
-
-lemma size_eq_sum_mset: "size M = sum_mset (image_mset (\<lambda>_. 1) M)"
-proof (induct M)
- case empty then show ?case by simp
-next
- case (add x M) then show ?case
- by (cases "x \<in> set_mset M")
- (simp_all add: size_multiset_overloaded_eq not_in_iff sum.If_cases Diff_eq[symmetric]
- sum.remove)
-qed
-
-lemma size_mset_set [simp]: "size (mset_set A) = card A"
-by (simp only: size_eq_sum_mset card_eq_sum sum_unfold_sum_mset)
-
-lemma sum_mset_sum_list: "sum_mset (mset xs) = sum_list xs"
- by (induction xs) auto
-
syntax (ASCII)
"_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3SUM _:#_. _)" [0, 51, 10] 10)
syntax
@@ -2300,31 +2260,95 @@
translations
"\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST sum_mset (CONST image_mset (\<lambda>i. b) A)"
+context comm_monoid_add
+begin
+
+lemma sum_mset_sum_list:
+ "sum_mset (mset xs) = sum_list xs"
+ by (induction xs) auto
+
+end
+
+context canonically_ordered_monoid_add
+begin
+
+lemma sum_mset_0_iff [simp]:
+ "sum_mset M = 0 \<longleftrightarrow> (\<forall>x \<in> set_mset M. x = 0)"
+ by (induction M) auto
+
+end
+
+context ordered_comm_monoid_add
+begin
+
+lemma sum_mset_mono:
+ "sum_mset (image_mset f K) \<le> sum_mset (image_mset g K)"
+ if "\<And>i. i \<in># K \<Longrightarrow> f i \<le> g i"
+ using that by (induction K) (simp_all add: add_mono)
+
+end
+
+context ordered_cancel_comm_monoid_diff
+begin
+
+lemma sum_mset_diff:
+ "sum_mset (M - N) = sum_mset M - sum_mset N" if "N \<subseteq># M" for M N :: "'a multiset"
+ using that by (auto simp add: subset_mset.le_iff_add)
+
+end
+
+context semiring_0
+begin
+
lemma sum_mset_distrib_left:
- fixes f :: "'a \<Rightarrow> 'b::semiring_0"
- shows "c * (\<Sum>x \<in># M. f x) = (\<Sum>x \<in># M. c * f(x))"
-by (induction M) (simp_all add: distrib_left)
+ "c * (\<Sum>x \<in># M. f x) = (\<Sum>x \<in># M. c * f(x))"
+ by (induction M) (simp_all add: algebra_simps)
lemma sum_mset_distrib_right:
- fixes f :: "'a \<Rightarrow> 'b::semiring_0"
- shows "(\<Sum>b \<in># B. f b) * a = (\<Sum>b \<in># B. f b * a)"
- by (induction B) (auto simp: distrib_right)
+ "(\<Sum>x \<in># M. f x) * c = (\<Sum>x \<in># M. f x * c)"
+ by (induction M) (simp_all add: algebra_simps)
+
+end
+
+lemma sum_mset_product:
+ fixes f :: "'a::{comm_monoid_add,times} \<Rightarrow> 'b::semiring_0"
+ shows "(\<Sum>i \<in># A. f i) * (\<Sum>i \<in># B. g i) = (\<Sum>i\<in>#A. \<Sum>j\<in>#B. f i * g j)"
+ by (subst sum_mset.commute) (simp add: sum_mset_distrib_left sum_mset_distrib_right)
+
+context semiring_1
+begin
+
+lemma sum_mset_replicate_mset [simp]:
+ "sum_mset (replicate_mset n a) = of_nat n * a"
+ by (induction n) (simp_all add: algebra_simps)
+
+lemma sum_mset_delta:
+ "sum_mset (image_mset (\<lambda>x. if x = y then c else 0) A) = c * of_nat (count A y)"
+ by (induction A) (simp_all add: algebra_simps)
+
+lemma sum_mset_delta':
+ "sum_mset (image_mset (\<lambda>x. if y = x then c else 0) A) = c * of_nat (count A y)"
+ by (induction A) (simp_all add: algebra_simps)
+
+end
+
+lemma of_nat_sum_mset [simp]:
+ "of_nat (sum_mset A) = sum_mset (image_mset of_nat A)"
+ by (induction A) auto
+
+lemma size_eq_sum_mset:
+ "size M = (\<Sum>a\<in>#M. 1)"
+ using image_mset_const_eq [of "1::nat" M] by simp
+
+lemma size_mset_set [simp]:
+ "size (mset_set A) = card A"
+ by (simp only: size_eq_sum_mset card_eq_sum sum_unfold_sum_mset)
lemma sum_mset_constant [simp]:
fixes y :: "'b::semiring_1"
shows \<open>(\<Sum>x\<in>#A. y) = of_nat (size A) * y\<close>
by (induction A) (auto simp: algebra_simps)
-lemma (in ordered_comm_monoid_add) sum_mset_mono:
- assumes "\<And>i. i \<in># K \<Longrightarrow> f i \<le> g i"
- shows "sum_mset (image_mset f K) \<le> sum_mset (image_mset g K)"
- using assms by (induction K) (simp_all add: local.add_mono)
-
-lemma sum_mset_product:
- fixes f :: "'a::{comm_monoid_add,times} \<Rightarrow> 'b::semiring_0"
- shows "(\<Sum>i \<in># A. f i) * (\<Sum>i \<in># B. g i) = (\<Sum>i\<in>#A. \<Sum>j\<in>#B. f i * g j)"
- by (subst sum_mset.commute) (simp add: sum_mset_distrib_left sum_mset_distrib_right)
-
abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset" ("\<Union>#_" [900] 900)
where "\<Union># MM \<equiv> sum_mset MM" \<comment> \<open>FIXME ambiguous notation --
could likewise refer to \<open>\<Squnion>#\<close>\<close>
@@ -2347,6 +2371,7 @@
lemma Union_mset_empty_conv[simp]: "\<Union># M = {#} \<longleftrightarrow> (\<forall>i\<in>#M. i = {#})"
by (induction M) auto
+
context comm_monoid_mult
begin
@@ -2365,6 +2390,10 @@
"prod_mset (A + B) = prod_mset A * prod_mset B"
by (fact prod_mset.union)
+lemma prod_mset_prod_list:
+ "prod_mset (mset xs) = prod_list xs"
+ by (induct xs) auto
+
lemma prod_mset_replicate_mset [simp]:
"prod_mset (replicate_mset n a) = a ^ n"
by (induct n) simp_all
@@ -2383,6 +2412,21 @@
lemma prod_mset_delta': "prod_mset (image_mset (\<lambda>x. if y = x then c else 1) A) = c ^ count A y"
by (induction A) simp_all
+lemma prod_mset_subset_imp_dvd:
+ assumes "A \<subseteq># B"
+ shows "prod_mset A dvd prod_mset B"
+proof -
+ from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
+ also have "prod_mset \<dots> = prod_mset (B - A) * prod_mset A" by simp
+ also have "prod_mset A dvd \<dots>" by simp
+ finally show ?thesis .
+qed
+
+lemma dvd_prod_mset:
+ assumes "x \<in># A"
+ shows "x dvd prod_mset A"
+ using assms prod_mset_subset_imp_dvd [of "{#x#}" A] by simp
+
end
syntax (ASCII)
@@ -2395,21 +2439,6 @@
lemma prod_mset_constant [simp]: "(\<Prod>_\<in>#A. c) = c ^ size A"
by (simp add: image_mset_const_eq)
-lemma (in comm_monoid_mult) prod_mset_subset_imp_dvd:
- assumes "A \<subseteq># B"
- shows "prod_mset A dvd prod_mset B"
-proof -
- from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
- also have "prod_mset \<dots> = prod_mset (B - A) * prod_mset A" by simp
- also have "prod_mset A dvd \<dots>" by simp
- finally show ?thesis .
-qed
-
-lemma (in comm_monoid_mult) dvd_prod_mset:
- assumes "x \<in># A"
- shows "x dvd prod_mset A"
- using assms prod_mset_subset_imp_dvd [of "{#x#}" A] by simp
-
lemma (in semidom) prod_mset_zero_iff [iff]:
"prod_mset A = 0 \<longleftrightarrow> 0 \<in># A"
by (induct A) auto
@@ -2445,9 +2474,6 @@
then show ?thesis by (simp add: normalize_prod_mset)
qed
-lemma prod_mset_prod_list: "prod_mset (mset xs) = prod_list xs"
- by (induct xs) auto
-
subsection \<open>Alternative representations\<close>
--- a/src/HOL/Library/Numeral_Type.thy Mon Oct 30 16:02:59 2017 +0000
+++ b/src/HOL/Library/Numeral_Type.thy Mon Oct 30 16:03:21 2017 +0000
@@ -168,7 +168,7 @@
shows "P"
apply (cases x rule: type_definition.Abs_cases [OF type])
apply (rule_tac z="y" in 1)
-apply (simp_all add: of_int_eq mod_pos_pos_trivial)
+apply (simp_all add: of_int_eq)
done
lemma induct:
@@ -229,7 +229,7 @@
"Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
"Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
apply (rule mod_type.intro)
-apply (simp add: of_nat_mult type_definition_bit0)
+apply (simp add: type_definition_bit0)
apply (rule one_less_int_card)
apply (rule zero_bit0_def)
apply (rule one_bit0_def)
@@ -244,7 +244,7 @@
"Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
apply (rule mod_type.intro)
-apply (simp add: of_nat_mult type_definition_bit1)
+apply (simp add: type_definition_bit1)
apply (rule one_less_int_card)
apply (rule zero_bit1_def)
apply (rule one_bit1_def)
@@ -411,12 +411,12 @@
instance
proof(intro_classes)
show "distinct (enum_class.enum :: 'a bit0 list)"
- by (simp add: enum_bit0_def distinct_map inj_on_def Abs_bit0'_def Abs_bit0_inject mod_pos_pos_trivial)
+ by (simp add: enum_bit0_def distinct_map inj_on_def Abs_bit0'_def Abs_bit0_inject)
show univ_eq: "(UNIV :: 'a bit0 set) = set enum_class.enum"
unfolding enum_bit0_def type_definition.Abs_image[OF type_definition_bit0, symmetric]
- by(simp add: image_comp [symmetric] inj_on_Abs_bit0 card_image image_int_atLeastLessThan)
- (auto intro!: image_cong[OF refl] simp add: Abs_bit0'_def mod_pos_pos_trivial)
+ by (simp add: image_comp [symmetric] inj_on_Abs_bit0 card_image image_int_atLeast_lessThan)
+ (auto intro!: image_cong[OF refl] simp add: Abs_bit0'_def)
fix P :: "'a bit0 \<Rightarrow> bool"
show "enum_class.enum_all P = Ball UNIV P"
@@ -439,8 +439,8 @@
show univ_eq: "(UNIV :: 'a bit1 set) = set enum_class.enum"
unfolding enum_bit1_def type_definition.Abs_image[OF type_definition_bit1, symmetric]
- by(simp add: image_comp [symmetric] inj_on_Abs_bit1 card_image image_int_atLeastLessThan)
- (auto intro!: image_cong[OF refl] simp add: Abs_bit1'_def mod_pos_pos_trivial)
+ by(simp add: image_comp [symmetric] inj_on_Abs_bit1 card_image image_int_atLeast_lessThan)
+ (auto intro!: image_cong[OF refl] simp add: Abs_bit1'_def)
fix P :: "'a bit1 \<Rightarrow> bool"
show "enum_class.enum_all P = Ball UNIV P"
--- a/src/HOL/Library/Uprod.thy Mon Oct 30 16:02:59 2017 +0000
+++ b/src/HOL/Library/Uprod.thy Mon Oct 30 16:03:21 2017 +0000
@@ -206,13 +206,13 @@
apply(rule card_image)
using bij[THEN bij_betw_imp_inj_on]
by(simp add: inj_on_def Ball_def)(metis leD le_eq_less_or_eq le_less_trans)
- also have "\<dots> = sum (\<lambda>n. n + 1) {0..<?A}"
- by(subst card_SigmaI) simp_all
- also have "\<dots> = 2 * sum of_nat {1..?A} div 2"
- using sum.reindex[where g="of_nat :: nat \<Rightarrow> nat" and h="\<lambda>x. x + 1" and A="{0..<?A}", symmetric] True
- by(simp del: sum_op_ivl_Suc add: atLeastLessThanSuc_atLeastAtMost)
+ also have "\<dots> = sum Suc {0..<?A}"
+ by (subst card_SigmaI) simp_all
+ also have "\<dots> = sum of_nat {Suc 0..?A}"
+ using sum.atLeast_lessThan_reindex [symmetric, of Suc 0 ?A id]
+ by (simp del: sum_op_ivl_Suc add: atLeastLessThanSuc_atLeastAtMost)
also have "\<dots> = ?A * (?A + 1) div 2"
- by(subst gauss_sum) simp
+ using gauss_sum_from_Suc_0 [of ?A, where ?'a = nat] by simp
finally show ?thesis .
qed simp
--- a/src/HOL/Nat.thy Mon Oct 30 16:02:59 2017 +0000
+++ b/src/HOL/Nat.thy Mon Oct 30 16:03:21 2017 +0000
@@ -166,9 +166,36 @@
text \<open>Injectiveness and distinctness lemmas\<close>
-lemma (in semidom_divide) inj_times:
- "inj (times a)" if "a \<noteq> 0"
-proof (rule injI)
+context cancel_ab_semigroup_add
+begin
+
+lemma inj_on_add [simp]:
+ "inj_on (plus a) A"
+proof (rule inj_onI)
+ fix b c
+ assume "a + b = a + c"
+ then have "a + b - a = a + c - a"
+ by (simp only:)
+ then show "b = c"
+ by simp
+qed
+
+lemma inj_on_add' [simp]:
+ "inj_on (\<lambda>b. b + a) A"
+ using inj_on_add [of a A] by (simp add: add.commute [of _ a])
+
+lemma bij_betw_add [simp]:
+ "bij_betw (plus a) A B \<longleftrightarrow> plus a ` A = B"
+ by (simp add: bij_betw_def)
+
+end
+
+context semidom_divide
+begin
+
+lemma inj_on_mult:
+ "inj_on (times a) A" if "a \<noteq> 0"
+proof (rule inj_onI)
fix b c
assume "a * b = a * c"
then have "a * b div a = a * c div a"
@@ -177,20 +204,16 @@
by simp
qed
-lemma (in cancel_ab_semigroup_add) inj_plus:
- "inj (plus a)"
-proof (rule injI)
- fix b c
- assume "a + b = a + c"
- then have "a + b - a = a + c - a"
- by (simp only:)
- then show "b = c"
- by simp
-qed
-
-lemma inj_Suc[simp]: "inj_on Suc N"
+end
+
+lemma inj_Suc [simp]:
+ "inj_on Suc N"
by (simp add: inj_on_def)
+lemma bij_betw_Suc [simp]:
+ "bij_betw Suc M N \<longleftrightarrow> Suc ` M = N"
+ by (simp add: bij_betw_def)
+
lemma Suc_neq_Zero: "Suc m = 0 \<Longrightarrow> R"
by (rule notE) (rule Suc_not_Zero)
@@ -338,16 +361,9 @@
for m n :: nat
by (induct m) simp_all
-lemma inj_on_add_nat [simp]: "inj_on (\<lambda>n. n + k) N"
- for k :: nat
-proof (induct k)
- case 0
- then show ?case by simp
-next
- case (Suc k)
- show ?case
- using comp_inj_on [OF Suc inj_Suc] by (simp add: o_def)
-qed
+lemma plus_1_eq_Suc:
+ "plus 1 = Suc"
+ by (simp add: fun_eq_iff)
lemma Suc_eq_plus1: "Suc n = n + 1"
by simp
--- a/src/HOL/Num.thy Mon Oct 30 16:02:59 2017 +0000
+++ b/src/HOL/Num.thy Mon Oct 30 16:03:21 2017 +0000
@@ -522,6 +522,10 @@
lemma mult_2_right: "z * 2 = z + z"
by (simp add: one_add_one [symmetric] distrib_left)
+lemma left_add_twice:
+ "a + (a + b) = 2 * a + b"
+ by (simp add: mult_2 ac_simps)
+
end
--- a/src/HOL/Orderings.thy Mon Oct 30 16:02:59 2017 +0000
+++ b/src/HOL/Orderings.thy Mon Oct 30 16:03:21 2017 +0000
@@ -1178,6 +1178,21 @@
qed
qed
+lemma mono_strict_invE:
+ fixes f :: "'a \<Rightarrow> 'b::order"
+ assumes "mono f"
+ assumes "f x < f y"
+ obtains "x < y"
+proof
+ show "x < y"
+ proof (rule ccontr)
+ assume "\<not> x < y"
+ then have "y \<le> x" by simp
+ with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
+ with \<open>f x < f y\<close> show False by simp
+ qed
+qed
+
lemma strict_mono_eq:
assumes "strict_mono f"
shows "f x = f y \<longleftrightarrow> x = y"
@@ -1243,6 +1258,7 @@
shows "max x (min x y) = x" "max (min x y) x = x" "max (min x y) y = y" "max y (min x y) = y"
by(auto simp add: max_def min_def)
+
subsection \<open>(Unique) top and bottom elements\<close>
class bot =
--- a/src/HOL/Power.thy Mon Oct 30 16:02:59 2017 +0000
+++ b/src/HOL/Power.thy Mon Oct 30 16:03:21 2017 +0000
@@ -306,6 +306,20 @@
end
+context semidom_divide
+begin
+
+lemma power_diff:
+ "a ^ (m - n) = (a ^ m) div (a ^ n)" if "a \<noteq> 0" and "n \<le> m"
+proof -
+ define q where "q = m - n"
+ with \<open>n \<le> m\<close> have "m = q + n" by simp
+ with \<open>a \<noteq> 0\<close> q_def show ?thesis
+ by (simp add: power_add)
+qed
+
+end
+
context algebraic_semidom
begin
@@ -370,11 +384,6 @@
context field
begin
-lemma power_diff:
- assumes "a \<noteq> 0"
- shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
- by (induct m n rule: diff_induct) (simp_all add: assms power_not_zero)
-
lemma power_divide [field_simps, divide_simps]: "(a / b) ^ n = a ^ n / b ^ n"
by (induct n) simp_all
--- a/src/HOL/Rings.thy Mon Oct 30 16:02:59 2017 +0000
+++ b/src/HOL/Rings.thy Mon Oct 30 16:03:21 2017 +0000
@@ -1738,7 +1738,10 @@
end
-class linordered_semiring_1 = linordered_semiring + semiring_1
+class zero_less_one = order + zero + one +
+ assumes zero_less_one [simp]: "0 < 1"
+
+class linordered_semiring_1 = linordered_semiring + semiring_1 + zero_less_one
begin
lemma convex_bound_le:
@@ -1847,7 +1850,7 @@
end
-class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
+class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1 + zero_less_one
begin
subclass linordered_semiring_1 ..
@@ -2124,9 +2127,6 @@
end
-class zero_less_one = order + zero + one +
- assumes zero_less_one [simp]: "0 < 1"
-
class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one
begin
@@ -2200,22 +2200,26 @@
end
-class linordered_idom =
- comm_ring_1 + linordered_comm_semiring_strict + ordered_ab_group_add + abs_if + sgn +
+class linordered_idom = comm_ring_1 + linordered_comm_semiring_strict +
+ ordered_ab_group_add + abs_if + sgn +
assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
begin
-subclass linordered_semiring_1_strict ..
subclass linordered_ring_strict ..
+
+subclass linordered_semiring_1_strict
+proof
+ have "0 \<le> 1 * 1"
+ by (fact zero_le_square)
+ then show "0 < 1"
+ by (simp add: le_less)
+qed
+
subclass ordered_comm_ring ..
subclass idom ..
subclass linordered_semidom
-proof
- have "0 \<le> 1 * 1" by (rule zero_le_square)
- then show "0 < 1" by (simp add: le_less)
- show "b \<le> a \<Longrightarrow> a - b + b = a" for a b by simp
-qed
+ by standard simp
subclass idom_abs_sgn
by standard
--- a/src/HOL/Set_Interval.thy Mon Oct 30 16:02:59 2017 +0000
+++ b/src/HOL/Set_Interval.thy Mon Oct 30 16:03:21 2017 +0000
@@ -218,6 +218,10 @@
lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \<inter> {..< b }"
by auto
+lemma (in order) atLeast_lessThan_eq_atLeast_atMost_diff:
+ "{a..<b} = {a..b} - {b}"
+ by (auto simp add: atLeastLessThan_def atLeastAtMost_def)
+
end
subsubsection\<open>Emptyness, singletons, subset\<close>
@@ -842,6 +846,7 @@
apply (simp_all add: atLeastLessThanSuc)
done
+
subsubsection \<open>Intervals and numerals\<close>
lemma lessThan_nat_numeral: \<comment>\<open>Evaluation for specific numerals\<close>
@@ -858,32 +863,74 @@
else {})"
by (simp add: numeral_eq_Suc atLeastLessThanSuc)
+
subsubsection \<open>Image\<close>
-lemma image_add_atLeastAtMost [simp]:
- fixes k ::"'a::linordered_semidom"
- shows "(\<lambda>n. n+k) ` {i..j} = {i+k..j+k}" (is "?A = ?B")
+context linordered_semidom
+begin
+
+lemma image_add_atLeast_atMost [simp]:
+ "plus k ` {i..j} = {i + k..j + k}" (is "?A = ?B")
proof
- show "?A \<subseteq> ?B" by auto
+ show "?A \<subseteq> ?B"
+ by (auto simp add: ac_simps)
next
show "?B \<subseteq> ?A"
proof
- fix n assume a: "n : ?B"
- hence "n - k : {i..j}"
- by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le)
- moreover have "n = (n - k) + k" using a
+ fix n
+ assume "n \<in> ?B"
+ then have "i \<le> n - k"
+ by (simp add: add_le_imp_le_diff)
+ have "n = n - k + k"
proof -
- have "k + i \<le> n"
- by (metis a add.commute atLeastAtMost_iff)
- hence "k + (n - k) = n"
- by (metis (no_types) ab_semigroup_add_class.add_ac(1) add_diff_cancel_left' le_add_diff_inverse)
- thus ?thesis
- by (simp add: add.commute)
+ from \<open>n \<in> ?B\<close> have "n = n - (i + k) + (i + k)"
+ by simp
+ also have "\<dots> = n - k - i + i + k"
+ by (simp add: algebra_simps)
+ also have "\<dots> = n - k + k"
+ using \<open>i \<le> n - k\<close> by simp
+ finally show ?thesis .
qed
- ultimately show "n : ?A" by blast
+ moreover have "n - k \<in> {i..j}"
+ using \<open>n \<in> ?B\<close>
+ by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le)
+ ultimately show "n \<in> ?A"
+ by (simp add: ac_simps)
qed
qed
+lemma image_add_atLeast_atMost' [simp]:
+ "(\<lambda>n. n + k) ` {i..j} = {i + k..j + k}"
+ by (simp add: add.commute [of _ k])
+
+lemma image_add_atLeast_lessThan [simp]:
+ "plus k ` {i..<j} = {i + k..<j + k}"
+ by (simp add: image_set_diff atLeast_lessThan_eq_atLeast_atMost_diff ac_simps)
+
+lemma image_add_atLeast_lessThan' [simp]:
+ "(\<lambda>n. n + k) ` {i..<j} = {i + k..<j + k}"
+ by (simp add: add.commute [of _ k])
+
+end
+
+lemma image_Suc_atLeast_atMost [simp]:
+ "Suc ` {i..j} = {Suc i..Suc j}"
+ using image_add_atLeast_atMost [of 1 i j]
+ by (simp only: plus_1_eq_Suc) simp
+
+lemma image_Suc_atLeast_lessThan [simp]:
+ "Suc ` {i..<j} = {Suc i..<Suc j}"
+ using image_add_atLeast_lessThan [of 1 i j]
+ by (simp only: plus_1_eq_Suc) simp
+
+corollary image_Suc_atMost:
+ "Suc ` {..n} = {1..Suc n}"
+ by (simp add: atMost_atLeast0 atLeastLessThanSuc_atLeastAtMost)
+
+corollary image_Suc_lessThan:
+ "Suc ` {..<n} = {1..n}"
+ by (simp add: lessThan_atLeast0 atLeastLessThanSuc_atLeastAtMost)
+
lemma image_diff_atLeastAtMost [simp]:
fixes d::"'a::linordered_idom" shows "(op - d ` {a..b}) = {d-b..d-a}"
apply auto
@@ -930,38 +977,6 @@
using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]
by (simp add: field_class.field_divide_inverse algebra_simps)
-lemma image_add_atLeastLessThan:
- "(%n::nat. n+k) ` {i..<j} = {i+k..<j+k}" (is "?A = ?B")
-proof
- show "?A \<subseteq> ?B" by auto
-next
- show "?B \<subseteq> ?A"
- proof
- fix n assume a: "n : ?B"
- hence "n - k : {i..<j}" by auto
- moreover have "n = (n - k) + k" using a by auto
- ultimately show "n : ?A" by blast
- qed
-qed
-
-corollary image_Suc_lessThan:
- "Suc ` {..<n} = {1..n}"
- using image_add_atLeastLessThan [of 1 0 n]
- by (auto simp add: lessThan_Suc_atMost atLeast0LessThan)
-
-corollary image_Suc_atMost:
- "Suc ` {..n} = {1..Suc n}"
- using image_add_atLeastLessThan [of 1 0 "Suc n"]
- by (auto simp add: lessThan_Suc_atMost atLeast0LessThan)
-
-corollary image_Suc_atLeastAtMost[simp]:
- "Suc ` {i..j} = {Suc i..Suc j}"
-using image_add_atLeastAtMost[where k="Suc 0"] by simp
-
-corollary image_Suc_atLeastLessThan[simp]:
- "Suc ` {i..<j} = {Suc i..<Suc j}"
-using image_add_atLeastLessThan[where k="Suc 0"] by simp
-
lemma atLeast1_lessThan_eq_remove0:
"{Suc 0..<n} = {..<n} - {0}"
by auto
@@ -994,7 +1009,12 @@
qed
qed auto
-lemma image_int_atLeastLessThan: "int ` {a..<b} = {int a..<int b}"
+lemma image_int_atLeast_lessThan:
+ "int ` {a..<b} = {int a..<int b}"
+ by (auto intro!: image_eqI [where x = "nat x" for x])
+
+lemma image_int_atLeast_atMost:
+ "int ` {a..b} = {int a..int b}"
by (auto intro!: image_eqI [where x = "nat x" for x])
context ordered_ab_group_add
@@ -1532,42 +1552,73 @@
subsection \<open>Generic big monoid operation over intervals\<close>
-lemma inj_on_add_nat' [simp]:
- "inj_on (plus k) N" for k :: nat
+context semiring_char_0
+begin
+
+lemma inj_on_of_nat [simp]:
+ "inj_on of_nat N"
by rule simp
+lemma bij_betw_of_nat [simp]:
+ "bij_betw of_nat N A \<longleftrightarrow> of_nat ` N = A"
+ by (simp add: bij_betw_def)
+
+end
+
context comm_monoid_set
begin
-lemma atLeast_lessThan_shift_bounds:
- fixes m n k :: nat
- shows "F g {m + k..<n + k} = F (g \<circ> plus k) {m..<n}"
+lemma atLeast_lessThan_reindex:
+ "F g {h m..<h n} = F (g \<circ> h) {m..<n}"
+ if "bij_betw h {m..<n} {h m..<h n}" for m n ::nat
proof -
- have "{m + k..<n + k} = plus k ` {m..<n}"
- by (auto simp add: image_add_atLeastLessThan [symmetric])
- also have "F g (plus k ` {m..<n}) = F (g \<circ> plus k) {m..<n}"
- by (rule reindex) simp
- finally show ?thesis .
+ from that have "inj_on h {m..<n}" and "h ` {m..<n} = {h m..<h n}"
+ by (simp_all add: bij_betw_def)
+ then show ?thesis
+ using reindex [of h "{m..<n}" g] by simp
qed
+lemma atLeast_atMost_reindex:
+ "F g {h m..h n} = F (g \<circ> h) {m..n}"
+ if "bij_betw h {m..n} {h m..h n}" for m n ::nat
+proof -
+ from that have "inj_on h {m..n}" and "h ` {m..n} = {h m..h n}"
+ by (simp_all add: bij_betw_def)
+ then show ?thesis
+ using reindex [of h "{m..n}" g] by simp
+qed
+
+lemma atLeast_lessThan_shift_bounds:
+ "F g {m + k..<n + k} = F (g \<circ> plus k) {m..<n}"
+ for m n k :: nat
+ using atLeast_lessThan_reindex [of "plus k" m n g]
+ by (simp add: ac_simps)
+
lemma atLeast_atMost_shift_bounds:
- fixes m n k :: nat
- shows "F g {m + k..n + k} = F (g \<circ> plus k) {m..n}"
-proof -
- have "{m + k..n + k} = plus k ` {m..n}"
- by (auto simp del: image_add_atLeastAtMost simp add: image_add_atLeastAtMost [symmetric])
- also have "F g (plus k ` {m..n}) = F (g \<circ> plus k) {m..n}"
- by (rule reindex) simp
- finally show ?thesis .
-qed
+ "F g {m + k..n + k} = F (g \<circ> plus k) {m..n}"
+ for m n k :: nat
+ using atLeast_atMost_reindex [of "plus k" m n g]
+ by (simp add: ac_simps)
lemma atLeast_Suc_lessThan_Suc_shift:
"F g {Suc m..<Suc n} = F (g \<circ> Suc) {m..<n}"
- using atLeast_lessThan_shift_bounds [of _ _ 1] by simp
+ using atLeast_lessThan_shift_bounds [of _ _ 1]
+ by (simp add: plus_1_eq_Suc)
lemma atLeast_Suc_atMost_Suc_shift:
"F g {Suc m..Suc n} = F (g \<circ> Suc) {m..n}"
- using atLeast_atMost_shift_bounds [of _ _ 1] by simp
+ using atLeast_atMost_shift_bounds [of _ _ 1]
+ by (simp add: plus_1_eq_Suc)
+
+lemma atLeast_int_lessThan_int_shift:
+ "F g {int m..<int n} = F (g \<circ> int) {m..<n}"
+ by (rule atLeast_lessThan_reindex)
+ (simp add: image_int_atLeast_lessThan)
+
+lemma atLeast_int_atMost_int_shift:
+ "F g {int m..int n} = F (g \<circ> int) {m..n}"
+ by (rule atLeast_atMost_reindex)
+ (simp add: image_int_atLeast_atMost)
lemma atLeast0_lessThan_Suc:
"F g {0..<Suc n} = F g {0..<n} \<^bold>* g n"
@@ -1780,6 +1831,9 @@
lemma nat_diff_sum_reindex: "(\<Sum>i<n. f (n - Suc i)) = (\<Sum>i<n. f i)"
by (rule sum.reindex_bij_witness[where i="\<lambda>i. n - Suc i" and j="\<lambda>i. n - Suc i"]) auto
+lemma sum_diff_distrib: "\<forall>x. Q x \<le> P x \<Longrightarrow> (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x :: nat)"
+ by (subst sum_subtractf_nat) auto
+
subsubsection \<open>Shifting bounds\<close>
@@ -1799,15 +1853,45 @@
"sum f {Suc m..<Suc n} = sum (%i. f(Suc i)){m..<n}"
by (simp add:sum_shift_bounds_nat_ivl[where k="Suc 0", simplified])
-lemma sum_shift_lb_Suc0_0:
- "f(0::nat) = (0::nat) \<Longrightarrow> sum f {Suc 0..k} = sum f {0..k}"
-by(simp add:sum_head_Suc)
+context comm_monoid_add
+begin
+
+context
+ fixes f :: "nat \<Rightarrow> 'a"
+ assumes "f 0 = 0"
+begin
lemma sum_shift_lb_Suc0_0_upt:
- "f(0::nat) = 0 \<Longrightarrow> sum f {Suc 0..<k} = sum f {0..<k}"
-apply(cases k)apply simp
-apply(simp add:sum_head_upt_Suc)
-done
+ "sum f {Suc 0..<k} = sum f {0..<k}"
+proof (cases k)
+ case 0
+ then show ?thesis
+ by simp
+next
+ case (Suc k)
+ moreover have "{0..<Suc k} = insert 0 {Suc 0..<Suc k}"
+ by auto
+ ultimately show ?thesis
+ using \<open>f 0 = 0\<close> by simp
+qed
+
+lemma sum_shift_lb_Suc0_0:
+ "sum f {Suc 0..k} = sum f {0..k}"
+proof (cases k)
+ case 0
+ with \<open>f 0 = 0\<close> show ?thesis
+ by simp
+next
+ case (Suc k)
+ moreover have "{0..Suc k} = insert 0 {Suc 0..Suc k}"
+ by auto
+ ultimately show ?thesis
+ using \<open>f 0 = 0\<close> by simp
+qed
+
+end
+
+end
lemma sum_atMost_Suc_shift:
fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
@@ -1892,7 +1976,7 @@
by (induction m) (simp_all add: algebra_simps)
-subsection \<open>The formula for geometric sums\<close>
+subsubsection \<open>The formula for geometric sums\<close>
lemma sum_power2: "(\<Sum>i=0..<k. (2::nat)^i) = 2^k-1"
by (induction k) (auto simp: mult_2)
@@ -1991,7 +2075,8 @@
using sum_gp_multiplied [of m n x] apply auto
by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
-subsection\<open>Geometric progressions\<close>
+
+subsubsection\<open>Geometric progressions\<close>
lemma sum_gp0:
fixes x :: "'a::{comm_ring,division_ring}"
@@ -2016,67 +2101,125 @@
shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
by (induct n) (auto simp: algebra_simps divide_simps)
-subsubsection \<open>The formula for arithmetic sums\<close>
+
+subsubsection \<open>The formulae for arithmetic sums\<close>
+
+context comm_semiring_1
+begin
+
+lemma double_gauss_sum:
+ "2 * (\<Sum>i = 0..n. of_nat i) = of_nat n * (of_nat n + 1)"
+ by (induct n) (simp_all add: sum.atLeast0_atMost_Suc algebra_simps left_add_twice)
+
+lemma double_gauss_sum_from_Suc_0:
+ "2 * (\<Sum>i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1)"
+proof -
+ have "sum of_nat {Suc 0..n} = sum of_nat (insert 0 {Suc 0..n})"
+ by simp
+ also have "\<dots> = sum of_nat {0..n}"
+ by (cases n) (simp_all add: atLeast0_atMost_Suc_eq_insert_0)
+ finally show ?thesis
+ by (simp add: double_gauss_sum)
+qed
+
+lemma double_arith_series:
+ "2 * (\<Sum>i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d)"
+proof -
+ have "(\<Sum>i = 0..n. a + of_nat i * d) = ((\<Sum>i = 0..n. a) + (\<Sum>i = 0..n. of_nat i * d))"
+ by (rule sum.distrib)
+ also have "\<dots> = (of_nat (Suc n) * a + d * (\<Sum>i = 0..n. of_nat i))"
+ by (simp add: sum_distrib_left algebra_simps)
+ finally show ?thesis
+ by (simp add: algebra_simps double_gauss_sum left_add_twice)
+qed
+
+end
+
+context semiring_parity
+begin
lemma gauss_sum:
- "(2::'a::comm_semiring_1)*(\<Sum>i\<in>{1..n}. of_nat i) = of_nat n*((of_nat n)+1)"
-proof (induct n)
- case 0
- show ?case by simp
-next
- case (Suc n)
- then show ?case
- by (simp add: algebra_simps add: one_add_one [symmetric] del: one_add_one)
- (* FIXME: make numeral cancellation simprocs work for semirings *)
-qed
-
-theorem arith_series_general:
- "(2::'a::comm_semiring_1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
- of_nat n * (a + (a + of_nat(n - 1)*d))"
-proof cases
- assume ngt1: "n > 1"
- let ?I = "\<lambda>i. of_nat i" and ?n = "of_nat n"
- have
- "(\<Sum>i\<in>{..<n}. a+?I i*d) =
- ((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))"
- by (rule sum.distrib)
- 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))"
- unfolding One_nat_def
- by (simp add: sum_distrib_left atLeast0LessThan[symmetric] sum_shift_lb_Suc0_0_upt ac_simps)
- also have "2*\<dots> = 2*?n*a + d*2*(\<Sum>i\<in>{1..<n}. ?I i)"
- by (simp add: algebra_simps)
- also from ngt1 have "{1..<n} = {1..n - 1}"
- by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
- also from ngt1
- have "2*?n*a + d*2*(\<Sum>i\<in>{1..n - 1}. ?I i) = (2*?n*a + d*?I (n - 1)*?I n)"
- by (simp only: mult.assoc gauss_sum [of "n - 1"], unfold One_nat_def)
- (simp add: mult.commute trans [OF add.commute of_nat_Suc [symmetric]])
- finally show ?thesis
- unfolding mult_2 by (simp add: algebra_simps)
-next
- assume "\<not>(n > 1)"
- hence "n = 1 \<or> n = 0" by auto
- thus ?thesis by (auto simp: mult_2)
-qed
+ "(\<Sum>i = 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2"
+ using double_gauss_sum [of n, symmetric] by simp
+
+lemma gauss_sum_from_Suc_0:
+ "(\<Sum>i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2"
+ using double_gauss_sum_from_Suc_0 [of n, symmetric] by simp
+
+lemma arith_series:
+ "(\<Sum>i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d) div 2"
+ using double_arith_series [of a d n, symmetric] by simp
+
+end
+
+lemma gauss_sum_nat:
+ "\<Sum>{0..n} = (n * Suc n) div 2"
+ using gauss_sum [of n, where ?'a = nat] by simp
lemma arith_series_nat:
- "(2::nat) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n - 1)*d))"
+ "(\<Sum>i = 0..n. a + i * d) = Suc n * (2 * a + n * d) div 2"
+ using arith_series [of a d n] by simp
+
+lemma Sum_Icc_int:
+ "\<Sum>{m..n} = (n * (n + 1) - m * (m - 1)) div 2"
+ if "m \<le> n" for m n :: int
+using that proof (induct i \<equiv> "nat (n - m)" arbitrary: m n)
+ case 0
+ then have "m = n"
+ by arith
+ then show ?case
+ by (simp add: algebra_simps mult_2 [symmetric])
+next
+ case (Suc i)
+ have 0: "i = nat((n-1) - m)" "m \<le> n-1" using Suc(2,3) by arith+
+ have "\<Sum> {m..n} = \<Sum> {m..1+(n-1)}" by simp
+ also have "\<dots> = \<Sum> {m..n-1} + n" using \<open>m \<le> n\<close>
+ by(subst atLeastAtMostPlus1_int_conv) simp_all
+ also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n"
+ by(simp add: Suc(1)[OF 0])
+ also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp
+ also have "\<dots> = (n*(n+1) - m*(m-1)) div 2"
+ by (simp add: algebra_simps mult_2_right)
+ finally show ?case .
+qed
+
+lemma Sum_Icc_nat:
+ "\<Sum>{m..n} = (n * (n + 1) - m * (m - 1)) div 2"
+ if "m \<le> n" for m n :: nat
proof -
- have
- "2 * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
- of_nat(n) * (a + (a + of_nat(n - 1)*d))"
- by (rule arith_series_general)
- thus ?thesis
- unfolding One_nat_def by auto
+ have *: "m * (m - 1) \<le> n * (n + 1)"
+ using that by (meson diff_le_self order_trans le_add1 mult_le_mono)
+ have "int (\<Sum>{m..n}) = (\<Sum>{int m..int n})"
+ by (simp add: sum.atLeast_int_atMost_int_shift)
+ also have "\<dots> = (int n * (int n + 1) - int m * (int m - 1)) div 2"
+ using that by (simp add: Sum_Icc_int)
+ also have "\<dots> = int ((n * (n + 1) - m * (m - 1)) div 2)"
+ using le_square * by (simp add: algebra_simps of_nat_div of_nat_diff)
+ finally show ?thesis
+ by (simp only: of_nat_eq_iff)
qed
-lemma arith_series_int:
- "2 * (\<Sum>i\<in>{..<n}. a + int i * d) = int n * (a + (a + int(n - 1)*d))"
- by (fact arith_series_general) (* FIXME: duplicate *)
-
-lemma sum_diff_distrib: "\<forall>x. Q x \<le> P x \<Longrightarrow> (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x :: nat)"
- by (subst sum_subtractf_nat) auto
+lemma Sum_Ico_nat:
+ "\<Sum>{m..<n} = (n * (n - 1) - m * (m - 1)) div 2"
+ if "m \<le> n" for m n :: nat
+proof -
+ from that consider "m < n" | "m = n"
+ by (auto simp add: less_le)
+ then show ?thesis proof cases
+ case 1
+ then have "{m..<n} = {m..n - 1}"
+ by auto
+ then have "\<Sum>{m..<n} = \<Sum>{m..n - 1}"
+ by simp
+ also have "\<dots> = (n * (n - 1) - m * (m - 1)) div 2"
+ using \<open>m < n\<close> by (simp add: Sum_Icc_nat mult.commute)
+ finally show ?thesis .
+ next
+ case 2
+ then show ?thesis
+ by simp
+ qed
+qed
subsubsection \<open>Division remainder\<close>
--- a/src/HOL/ex/Function_Growth.thy Mon Oct 30 16:02:59 2017 +0000
+++ b/src/HOL/ex/Function_Growth.thy Mon Oct 30 16:03:21 2017 +0000
@@ -10,40 +10,6 @@
"HOL-Library.Discrete"
begin
-(* FIXME move *)
-
-context linorder
-begin
-
-lemma mono_invE:
- fixes f :: "'a \<Rightarrow> 'b::order"
- assumes "mono f"
- assumes "f x < f y"
- obtains "x < y"
-proof
- show "x < y"
- proof (rule ccontr)
- assume "\<not> x < y"
- then have "y \<le> x" by simp
- with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
- with \<open>f x < f y\<close> show False by simp
- qed
-qed
-
-end
-
-lemma (in semidom_divide) power_diff:
- fixes a :: 'a
- assumes "a \<noteq> 0"
- assumes "m \<ge> n"
- shows "a ^ (m - n) = (a ^ m) div (a ^ n)"
-proof -
- define q where "q = m - n"
- with assms have "m = q + n" by (simp add: q_def)
- with q_def show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
-qed
-
-
subsection \<open>Motivation\<close>
text \<open>