tuned some proofs and added some lemmas
authorhaftmann
Mon Oct 30 13:18:41 2017 +0000 (19 months ago)
changeset 66936cf8d8fc23891
parent 66935 d0f12783cd80
child 66937 a1a4a5e2933a
tuned some proofs and added some lemmas
src/HOL/Analysis/Gamma_Function.thy
src/HOL/GCD.thy
src/HOL/Groups_Big.thy
src/HOL/Inequalities.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/Uprod.thy
src/HOL/Nat.thy
src/HOL/Num.thy
src/HOL/Orderings.thy
src/HOL/Power.thy
src/HOL/Set_Interval.thy
src/HOL/ex/Function_Growth.thy
     1.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Sun Oct 29 19:39:03 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Mon Oct 30 13:18:41 2017 +0000
     1.3 @@ -152,10 +152,10 @@
     1.4      fix z
     1.5      show "(\<Sum>n. of_real (sin_coeff (n+1)) * z^n)  = ?f z"
     1.6        by (cases "z = 0") (insert sin_z_over_z_series'[of z],
     1.7 -            simp_all add: scaleR_conv_of_real sums_iff powser_zero sin_coeff_def)
     1.8 +            simp_all add: scaleR_conv_of_real sums_iff sin_coeff_def)
     1.9    qed
    1.10    also have "(\<Sum>n. diffs (\<lambda>n. of_real (sin_coeff (n + 1))) n * (0::'a) ^ n) =
    1.11 -                 diffs (\<lambda>n. of_real (sin_coeff (Suc n))) 0" by (simp add: powser_zero)
    1.12 +                 diffs (\<lambda>n. of_real (sin_coeff (Suc n))) 0" by simp
    1.13    also have "\<dots> = 0" by (simp add: sin_coeff_def diffs_def)
    1.14    finally show "((\<lambda>z::'a. if z = 0 then 1 else sin z / z) has_field_derivative 0) (at 0)" .
    1.15  qed
    1.16 @@ -520,7 +520,7 @@
    1.17      unfolding pochhammer_prod
    1.18      by (simp add: prod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
    1.19    also have "of_nat n powr z / (pochhammer z (Suc n) / fact n) = Gamma_series z n"
    1.20 -    unfolding Gamma_series_def using assms by (simp add: divide_simps powr_def Ln_of_nat)
    1.21 +    unfolding Gamma_series_def using assms by (simp add: divide_simps powr_def)
    1.22    finally show ?thesis .
    1.23  qed
    1.24  
    1.25 @@ -656,8 +656,7 @@
    1.26      also have "(\<Sum>n\<in>\<dots>. f n) = (\<Sum>n<k. f n) + (\<Sum>n=k..<m+k. f n)"
    1.27        by (rule sum.union_disjoint) auto
    1.28      also have "(\<Sum>n=k..<m+k. f n) = (\<Sum>n=0..<m+k-k. f (n + k))"
    1.29 -      by (intro sum.reindex_cong[of "\<lambda>n. n + k"])
    1.30 -         (simp, subst image_add_atLeastLessThan, auto)
    1.31 +      using sum_shift_bounds_nat_ivl [of f 0 k m] by simp
    1.32      finally show "(\<Sum>n<k. f n) + (\<Sum>n<m. f (n + k)) = (\<Sum>n<m+k. f n)" by (simp add: atLeast0LessThan)
    1.33    qed
    1.34    finally have "(\<lambda>a. sum f {..<a}) \<longlonglongrightarrow> lim (\<lambda>m. sum f {..<m + k})"
    1.35 @@ -2295,7 +2294,7 @@
    1.36      unfolding h_def using that by (auto intro!: Reals_mult Reals_add Reals_diff Polygamma_Real)
    1.37  
    1.38    from h'_zero h_h'_2 have "\<exists>c. \<forall>z\<in>UNIV. h z = c"
    1.39 -    by (intro has_field_derivative_zero_constant) (simp_all add: dist_0_norm)
    1.40 +    by (intro has_field_derivative_zero_constant) simp_all
    1.41    then obtain c where c: "\<And>z. h z = c" by auto
    1.42    have "\<exists>u. u \<in> closed_segment 0 1 \<and> Re (g 1) - Re (g 0) = Re (h u * g u * (1 - 0))"
    1.43      by (intro complex_mvt_line g_g')
    1.44 @@ -2861,7 +2860,7 @@
    1.45      have "((\<lambda>x. exp ((z - 1) * of_real (ln x)) * (1 - of_real x / of_nat n) ^ n)
    1.46              has_integral (?I * exp ((z - 1) * ln (of_nat n)))) {0..real n}" (is ?P)
    1.47        by (insert B, subst (asm) mult.assoc [symmetric], subst (asm) exp_add [symmetric])
    1.48 -         (simp add: Ln_of_nat algebra_simps)
    1.49 +         (simp add: algebra_simps)
    1.50      also have "?P \<longleftrightarrow> ((\<lambda>x. of_real x powr (z - 1) * (1 - of_real x / of_nat n) ^ n)
    1.51              has_integral (?I * exp ((z - 1) * ln (of_nat n)))) {0..real n}"
    1.52        by (intro has_integral_spike_finite_eq[of "{0}"]) (simp_all add: powr_def Ln_of_real)
     2.1 --- a/src/HOL/GCD.thy	Sun Oct 29 19:39:03 2017 +0100
     2.2 +++ b/src/HOL/GCD.thy	Mon Oct 30 13:18:41 2017 +0000
     2.3 @@ -1600,13 +1600,10 @@
     2.4      by simp
     2.5  next
     2.6    case False
     2.7 -  then have "inj (times b)"
     2.8 -    by (rule inj_times)
     2.9    show ?thesis proof (cases "finite A")
    2.10      case False
    2.11 -    moreover from \<open>inj (times b)\<close>
    2.12 -    have "inj_on (times b) A"
    2.13 -      by (rule inj_on_subset) simp
    2.14 +    moreover have "inj_on (times b) A"
    2.15 +      using \<open>b \<noteq> 0\<close> by (rule inj_on_mult)
    2.16      ultimately have "infinite (times b ` A)"
    2.17        by (simp add: finite_image_iff)
    2.18      with False show ?thesis
     3.1 --- a/src/HOL/Groups_Big.thy	Sun Oct 29 19:39:03 2017 +0100
     3.2 +++ b/src/HOL/Groups_Big.thy	Mon Oct 30 13:18:41 2017 +0000
     3.3 @@ -761,31 +761,16 @@
     3.4    "finite F \<Longrightarrow> (sum f F = 0) = (\<forall>a\<in>F. f a = 0)"
     3.5    by (intro ballI sum_nonneg_eq_0_iff zero_le)
     3.6  
     3.7 -lemma sum_distrib_left: "r * sum f A = sum (\<lambda>n. r * f n) A"
     3.8 -  for f :: "'a \<Rightarrow> 'b::semiring_0"
     3.9 -proof (induct A rule: infinite_finite_induct)
    3.10 -  case infinite
    3.11 -  then show ?case by simp
    3.12 -next
    3.13 -  case empty
    3.14 -  then show ?case by simp
    3.15 -next
    3.16 -  case insert
    3.17 -  then show ?case by (simp add: distrib_left)
    3.18 -qed
    3.19 +context semiring_0
    3.20 +begin
    3.21 +
    3.22 +lemma sum_distrib_left: "r * sum f A = (\<Sum>n\<in>A. r * f n)"
    3.23 +  by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)
    3.24  
    3.25  lemma sum_distrib_right: "sum f A * r = (\<Sum>n\<in>A. f n * r)"
    3.26 -  for r :: "'a::semiring_0"
    3.27 -proof (induct A rule: infinite_finite_induct)
    3.28 -  case infinite
    3.29 -  then show ?case by simp
    3.30 -next
    3.31 -  case empty
    3.32 -  then show ?case by simp
    3.33 -next
    3.34 -  case insert
    3.35 -  then show ?case by (simp add: distrib_right)
    3.36 -qed
    3.37 +  by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)
    3.38 +
    3.39 +end
    3.40  
    3.41  lemma sum_divide_distrib: "sum f A / r = (\<Sum>n\<in>A. f n / r)"
    3.42    for r :: "'a::field"
    3.43 @@ -958,8 +943,14 @@
    3.44      by (simp add: card.eq_fold sum.eq_fold)
    3.45  qed
    3.46  
    3.47 -lemma sum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
    3.48 -  by (induct A rule: infinite_finite_induct) (auto simp: algebra_simps)
    3.49 +context semiring_1
    3.50 +begin
    3.51 +
    3.52 +lemma sum_constant [simp]:
    3.53 +  "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
    3.54 +  by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)
    3.55 +
    3.56 +end
    3.57  
    3.58  lemma sum_Suc: "sum (\<lambda>x. Suc(f x)) A = sum f A + card A"
    3.59    using sum.distrib[of f "\<lambda>_. 1" A] by simp
     4.1 --- a/src/HOL/Inequalities.thy	Sun Oct 29 19:39:03 2017 +0100
     4.2 +++ b/src/HOL/Inequalities.thy	Mon Oct 30 13:18:41 2017 +0000
     4.3 @@ -7,49 +7,6 @@
     4.4    imports Real_Vector_Spaces
     4.5  begin
     4.6  
     4.7 -lemma Sum_Icc_int: "(m::int) \<le> n \<Longrightarrow> \<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
     4.8 -proof(induct i == "nat(n-m)" arbitrary: m n)
     4.9 -  case 0
    4.10 -  hence "m = n" by arith
    4.11 -  thus ?case by (simp add: algebra_simps)
    4.12 -next
    4.13 -  case (Suc i)
    4.14 -  have 0: "i = nat((n-1) - m)" "m \<le> n-1" using Suc(2,3) by arith+
    4.15 -  have "\<Sum> {m..n} = \<Sum> {m..1+(n-1)}" by simp
    4.16 -  also have "\<dots> = \<Sum> {m..n-1} + n" using \<open>m \<le> n\<close>
    4.17 -    by(subst atLeastAtMostPlus1_int_conv) simp_all
    4.18 -  also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n"
    4.19 -    by(simp add: Suc(1)[OF 0])
    4.20 -  also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp
    4.21 -  also have "\<dots> = (n*(n+1) - m*(m-1)) div 2" by(simp add: algebra_simps)
    4.22 -  finally show ?case .
    4.23 -qed
    4.24 -
    4.25 -lemma Sum_Icc_nat: assumes "(m::nat) \<le> n"
    4.26 -shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
    4.27 -proof -
    4.28 -  have "m*(m-1) \<le> n*(n + 1)"
    4.29 -   using assms by (meson diff_le_self order_trans le_add1 mult_le_mono)
    4.30 -  hence "int(\<Sum> {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms
    4.31 -    by (auto simp: Sum_Icc_int[transferred, OF assms] zdiv_int of_nat_mult simp del: of_nat_sum
    4.32 -          split: zdiff_int_split)
    4.33 -  thus ?thesis
    4.34 -    using of_nat_eq_iff by blast
    4.35 -qed
    4.36 -
    4.37 -lemma Sum_Ico_nat: assumes "(m::nat) \<le> n"
    4.38 -shows "\<Sum> {m..<n} = (n*(n-1) - m*(m-1)) div 2"
    4.39 -proof cases
    4.40 -  assume "m < n"
    4.41 -  hence "{m..<n} = {m..n-1}" by auto
    4.42 -  hence "\<Sum>{m..<n} = \<Sum>{m..n-1}" by simp
    4.43 -  also have "\<dots> = (n*(n-1) - m*(m-1)) div 2"
    4.44 -    using assms \<open>m < n\<close> by (simp add: Sum_Icc_nat mult.commute)
    4.45 -  finally show ?thesis .
    4.46 -next
    4.47 -  assume "\<not> m < n" with assms show ?thesis by simp
    4.48 -qed
    4.49 -
    4.50  lemma Chebyshev_sum_upper:
    4.51    fixes a b::"nat \<Rightarrow> 'a::linordered_idom"
    4.52    assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> a i \<le> a j"
     5.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Sun Oct 29 19:39:03 2017 +0100
     5.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Mon Oct 30 13:18:41 2017 +0000
     5.3 @@ -42,7 +42,7 @@
     5.4      have "(\<Sum>j<k + i. f j) = (\<Sum>j=i..<k + i. f j) + (\<Sum>j=0..<i. f j)"
     5.5        by (subst sum.union_disjoint[symmetric]) (auto intro!: sum.cong)
     5.6      also have "(\<Sum>j=i..<k + i. f j) = (\<Sum>j\<in>(\<lambda>n. n + i)`{0..<k}. f j)"
     5.7 -      unfolding image_add_atLeastLessThan by simp
     5.8 +      unfolding image_add_atLeast_lessThan by simp
     5.9      finally have "(\<Sum>j<k + i. f j) = (\<Sum>n<k. f (n + i)) + (\<Sum>j<i. f j)"
    5.10        by (auto simp: inj_on_def atLeast0LessThan sum.reindex) }
    5.11    ultimately have "(\<lambda>k. (\<Sum>n<k + i. f n)) \<longlonglongrightarrow> l + (\<Sum>j<i. f j)"
     6.1 --- a/src/HOL/Library/Extended_Real.thy	Sun Oct 29 19:39:03 2017 +0100
     6.2 +++ b/src/HOL/Library/Extended_Real.thy	Mon Oct 30 13:18:41 2017 +0000
     6.3 @@ -3381,18 +3381,20 @@
     6.4    shows "(\<Sum>i. f (i + k)) \<le> suminf f"
     6.5  proof -
     6.6    have "(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k))"
     6.7 -    using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
     6.8 +    using summable_sums[OF summable_ereal_pos]
     6.9 +    by (simp add: sums_def atLeast0LessThan f)
    6.10    moreover have "(\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> (\<Sum>i. f i)"
    6.11 -    using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
    6.12 +    using summable_sums[OF summable_ereal_pos]
    6.13 +    by (simp add: sums_def atLeast0LessThan f)
    6.14    then have "(\<lambda>n. \<Sum>i<n + k. f i) \<longlonglongrightarrow> (\<Sum>i. f i)"
    6.15      by (rule LIMSEQ_ignore_initial_segment)
    6.16    ultimately show ?thesis
    6.17    proof (rule LIMSEQ_le, safe intro!: exI[of _ k])
    6.18      fix n assume "k \<le> n"
    6.19 -    have "(\<Sum>i<n. f (i + k)) = (\<Sum>i<n. (f \<circ> (\<lambda>i. i + k)) i)"
    6.20 -      by simp
    6.21 -    also have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
    6.22 -      by (subst sum.reindex) auto
    6.23 +    have "(\<Sum>i<n. f (i + k)) = (\<Sum>i<n. (f \<circ> plus k) i)"
    6.24 +      by (simp add: ac_simps)
    6.25 +    also have "\<dots> = (\<Sum>i\<in>(plus k) ` {..<n}. f i)"
    6.26 +      by (rule sum.reindex [symmetric]) simp
    6.27      also have "\<dots> \<le> sum f {..<n + k}"
    6.28        by (intro sum_mono2) (auto simp: f)
    6.29      finally show "(\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}" .
     7.1 --- a/src/HOL/Library/Numeral_Type.thy	Sun Oct 29 19:39:03 2017 +0100
     7.2 +++ b/src/HOL/Library/Numeral_Type.thy	Mon Oct 30 13:18:41 2017 +0000
     7.3 @@ -168,7 +168,7 @@
     7.4    shows "P"
     7.5  apply (cases x rule: type_definition.Abs_cases [OF type])
     7.6  apply (rule_tac z="y" in 1)
     7.7 -apply (simp_all add: of_int_eq mod_pos_pos_trivial)
     7.8 +apply (simp_all add: of_int_eq)
     7.9  done
    7.10  
    7.11  lemma induct:
    7.12 @@ -229,7 +229,7 @@
    7.13             "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
    7.14             "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
    7.15  apply (rule mod_type.intro)
    7.16 -apply (simp add: of_nat_mult type_definition_bit0)
    7.17 +apply (simp add: type_definition_bit0)
    7.18  apply (rule one_less_int_card)
    7.19  apply (rule zero_bit0_def)
    7.20  apply (rule one_bit0_def)
    7.21 @@ -244,7 +244,7 @@
    7.22             "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
    7.23             "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
    7.24  apply (rule mod_type.intro)
    7.25 -apply (simp add: of_nat_mult type_definition_bit1)
    7.26 +apply (simp add: type_definition_bit1)
    7.27  apply (rule one_less_int_card)
    7.28  apply (rule zero_bit1_def)
    7.29  apply (rule one_bit1_def)
    7.30 @@ -411,12 +411,12 @@
    7.31  instance
    7.32  proof(intro_classes)
    7.33    show "distinct (enum_class.enum :: 'a bit0 list)"
    7.34 -    by (simp add: enum_bit0_def distinct_map inj_on_def Abs_bit0'_def Abs_bit0_inject mod_pos_pos_trivial)
    7.35 +    by (simp add: enum_bit0_def distinct_map inj_on_def Abs_bit0'_def Abs_bit0_inject)
    7.36  
    7.37    show univ_eq: "(UNIV :: 'a bit0 set) = set enum_class.enum"
    7.38      unfolding enum_bit0_def type_definition.Abs_image[OF type_definition_bit0, symmetric]
    7.39 -    by(simp add: image_comp [symmetric] inj_on_Abs_bit0 card_image image_int_atLeastLessThan)
    7.40 -      (auto intro!: image_cong[OF refl] simp add: Abs_bit0'_def mod_pos_pos_trivial)
    7.41 +    by (simp add: image_comp [symmetric] inj_on_Abs_bit0 card_image image_int_atLeast_lessThan)
    7.42 +      (auto intro!: image_cong[OF refl] simp add: Abs_bit0'_def)
    7.43  
    7.44    fix P :: "'a bit0 \<Rightarrow> bool"
    7.45    show "enum_class.enum_all P = Ball UNIV P"
    7.46 @@ -439,8 +439,8 @@
    7.47  
    7.48    show univ_eq: "(UNIV :: 'a bit1 set) = set enum_class.enum"
    7.49      unfolding enum_bit1_def type_definition.Abs_image[OF type_definition_bit1, symmetric]
    7.50 -    by(simp add: image_comp [symmetric] inj_on_Abs_bit1 card_image image_int_atLeastLessThan)
    7.51 -      (auto intro!: image_cong[OF refl] simp add: Abs_bit1'_def mod_pos_pos_trivial)
    7.52 +    by(simp add: image_comp [symmetric] inj_on_Abs_bit1 card_image image_int_atLeast_lessThan)
    7.53 +      (auto intro!: image_cong[OF refl] simp add: Abs_bit1'_def)
    7.54  
    7.55    fix P :: "'a bit1 \<Rightarrow> bool"
    7.56    show "enum_class.enum_all P = Ball UNIV P"
     8.1 --- a/src/HOL/Library/Uprod.thy	Sun Oct 29 19:39:03 2017 +0100
     8.2 +++ b/src/HOL/Library/Uprod.thy	Mon Oct 30 13:18:41 2017 +0000
     8.3 @@ -206,13 +206,13 @@
     8.4      apply(rule card_image)
     8.5      using bij[THEN bij_betw_imp_inj_on]
     8.6      by(simp add: inj_on_def Ball_def)(metis leD le_eq_less_or_eq le_less_trans)
     8.7 -  also have "\<dots> = sum (\<lambda>n. n + 1) {0..<?A}"
     8.8 -    by(subst card_SigmaI) simp_all
     8.9 -  also have "\<dots> = 2 * sum of_nat {1..?A} div 2"
    8.10 -    using sum.reindex[where g="of_nat :: nat \<Rightarrow> nat" and h="\<lambda>x. x + 1" and A="{0..<?A}", symmetric] True
    8.11 -    by(simp del: sum_op_ivl_Suc add: atLeastLessThanSuc_atLeastAtMost)
    8.12 +  also have "\<dots> = sum Suc {0..<?A}"
    8.13 +    by (subst card_SigmaI) simp_all
    8.14 +  also have "\<dots> = sum of_nat {Suc 0..?A}"
    8.15 +    using sum.atLeast_lessThan_reindex [symmetric, of Suc 0 ?A id]
    8.16 +    by (simp del: sum_op_ivl_Suc add: atLeastLessThanSuc_atLeastAtMost)
    8.17    also have "\<dots> = ?A * (?A + 1) div 2"
    8.18 -    by(subst gauss_sum) simp
    8.19 +    using gauss_sum_from_Suc_0 [of ?A, where ?'a = nat] by simp
    8.20    finally show ?thesis .
    8.21  qed simp
    8.22  
     9.1 --- a/src/HOL/Nat.thy	Sun Oct 29 19:39:03 2017 +0100
     9.2 +++ b/src/HOL/Nat.thy	Mon Oct 30 13:18:41 2017 +0000
     9.3 @@ -166,9 +166,36 @@
     9.4  
     9.5  text \<open>Injectiveness and distinctness lemmas\<close>
     9.6  
     9.7 -lemma (in semidom_divide) inj_times:
     9.8 -  "inj (times a)" if "a \<noteq> 0"
     9.9 -proof (rule injI)
    9.10 +context cancel_ab_semigroup_add
    9.11 +begin
    9.12 +
    9.13 +lemma inj_on_add [simp]:
    9.14 +  "inj_on (plus a) A"
    9.15 +proof (rule inj_onI)
    9.16 +  fix b c
    9.17 +  assume "a + b = a + c"
    9.18 +  then have "a + b - a = a + c - a"
    9.19 +    by (simp only:)
    9.20 +  then show "b = c"
    9.21 +    by simp
    9.22 +qed
    9.23 +
    9.24 +lemma inj_on_add' [simp]:
    9.25 +  "inj_on (\<lambda>b. b + a) A"
    9.26 +  using inj_on_add [of a A] by (simp add: add.commute [of _ a])
    9.27 +
    9.28 +lemma bij_betw_add [simp]:
    9.29 +  "bij_betw (plus a) A B \<longleftrightarrow> plus a ` A = B"
    9.30 +  by (simp add: bij_betw_def)
    9.31 +
    9.32 +end
    9.33 +
    9.34 +context semidom_divide
    9.35 +begin
    9.36 +
    9.37 +lemma inj_on_mult:
    9.38 +  "inj_on (times a) A" if "a \<noteq> 0"
    9.39 +proof (rule inj_onI)
    9.40    fix b c
    9.41    assume "a * b = a * c"
    9.42    then have "a * b div a = a * c div a"
    9.43 @@ -177,20 +204,16 @@
    9.44      by simp
    9.45  qed
    9.46  
    9.47 -lemma (in cancel_ab_semigroup_add) inj_plus:
    9.48 -  "inj (plus a)"
    9.49 -proof (rule injI)
    9.50 -  fix b c
    9.51 -  assume "a + b = a + c"
    9.52 -  then have "a + b - a = a + c - a"
    9.53 -    by (simp only:)
    9.54 -  then show "b = c"
    9.55 -    by simp
    9.56 -qed
    9.57 -
    9.58 -lemma inj_Suc[simp]: "inj_on Suc N"
    9.59 +end
    9.60 +
    9.61 +lemma inj_Suc [simp]:
    9.62 +  "inj_on Suc N"
    9.63    by (simp add: inj_on_def)
    9.64  
    9.65 +lemma bij_betw_Suc [simp]:
    9.66 +  "bij_betw Suc M N \<longleftrightarrow> Suc ` M = N"
    9.67 +  by (simp add: bij_betw_def)
    9.68 +
    9.69  lemma Suc_neq_Zero: "Suc m = 0 \<Longrightarrow> R"
    9.70    by (rule notE) (rule Suc_not_Zero)
    9.71  
    9.72 @@ -338,16 +361,9 @@
    9.73    for m n :: nat
    9.74    by (induct m) simp_all
    9.75  
    9.76 -lemma inj_on_add_nat [simp]: "inj_on (\<lambda>n. n + k) N"
    9.77 -  for k :: nat
    9.78 -proof (induct k)
    9.79 -  case 0
    9.80 -  then show ?case by simp
    9.81 -next
    9.82 -  case (Suc k)
    9.83 -  show ?case
    9.84 -    using comp_inj_on [OF Suc inj_Suc] by (simp add: o_def)
    9.85 -qed
    9.86 +lemma plus_1_eq_Suc:
    9.87 +  "plus 1 = Suc"
    9.88 +  by (simp add: fun_eq_iff)
    9.89  
    9.90  lemma Suc_eq_plus1: "Suc n = n + 1"
    9.91    by simp
    10.1 --- a/src/HOL/Num.thy	Sun Oct 29 19:39:03 2017 +0100
    10.2 +++ b/src/HOL/Num.thy	Mon Oct 30 13:18:41 2017 +0000
    10.3 @@ -522,6 +522,10 @@
    10.4  lemma mult_2_right: "z * 2 = z + z"
    10.5    by (simp add: one_add_one [symmetric] distrib_left)
    10.6  
    10.7 +lemma left_add_twice:
    10.8 +  "a + (a + b) = 2 * a + b"
    10.9 +  by (simp add: mult_2 ac_simps)
   10.10 +
   10.11  end
   10.12  
   10.13  
    11.1 --- a/src/HOL/Orderings.thy	Sun Oct 29 19:39:03 2017 +0100
    11.2 +++ b/src/HOL/Orderings.thy	Mon Oct 30 13:18:41 2017 +0000
    11.3 @@ -1178,6 +1178,21 @@
    11.4    qed
    11.5  qed
    11.6  
    11.7 +lemma mono_strict_invE:
    11.8 +  fixes f :: "'a \<Rightarrow> 'b::order"
    11.9 +  assumes "mono f"
   11.10 +  assumes "f x < f y"
   11.11 +  obtains "x < y"
   11.12 +proof
   11.13 +  show "x < y"
   11.14 +  proof (rule ccontr)
   11.15 +    assume "\<not> x < y"
   11.16 +    then have "y \<le> x" by simp
   11.17 +    with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
   11.18 +    with \<open>f x < f y\<close> show False by simp
   11.19 +  qed
   11.20 +qed
   11.21 +
   11.22  lemma strict_mono_eq:
   11.23    assumes "strict_mono f"
   11.24    shows "f x = f y \<longleftrightarrow> x = y"
   11.25 @@ -1243,6 +1258,7 @@
   11.26    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"
   11.27  by(auto simp add: max_def min_def)
   11.28  
   11.29 +
   11.30  subsection \<open>(Unique) top and bottom elements\<close>
   11.31  
   11.32  class bot =
    12.1 --- a/src/HOL/Power.thy	Sun Oct 29 19:39:03 2017 +0100
    12.2 +++ b/src/HOL/Power.thy	Mon Oct 30 13:18:41 2017 +0000
    12.3 @@ -306,6 +306,20 @@
    12.4  
    12.5  end
    12.6  
    12.7 +context semidom_divide
    12.8 +begin
    12.9 +
   12.10 +lemma power_diff:
   12.11 +  "a ^ (m - n) = (a ^ m) div (a ^ n)" if "a \<noteq> 0" and "n \<le> m"
   12.12 +proof -
   12.13 +  define q where "q = m - n"
   12.14 +  with \<open>n \<le> m\<close> have "m = q + n" by simp
   12.15 +  with \<open>a \<noteq> 0\<close> q_def show ?thesis
   12.16 +    by (simp add: power_add)
   12.17 +qed
   12.18 +
   12.19 +end
   12.20 +
   12.21  context algebraic_semidom
   12.22  begin
   12.23  
   12.24 @@ -370,11 +384,6 @@
   12.25  context field
   12.26  begin
   12.27  
   12.28 -lemma power_diff:
   12.29 -  assumes "a \<noteq> 0"
   12.30 -  shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
   12.31 -  by (induct m n rule: diff_induct) (simp_all add: assms power_not_zero)
   12.32 -
   12.33  lemma power_divide [field_simps, divide_simps]: "(a / b) ^ n = a ^ n / b ^ n"
   12.34    by (induct n) simp_all
   12.35  
    13.1 --- a/src/HOL/Set_Interval.thy	Sun Oct 29 19:39:03 2017 +0100
    13.2 +++ b/src/HOL/Set_Interval.thy	Mon Oct 30 13:18:41 2017 +0000
    13.3 @@ -218,6 +218,10 @@
    13.4  lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \<inter> {..< b }"
    13.5    by auto
    13.6  
    13.7 +lemma (in order) atLeast_lessThan_eq_atLeast_atMost_diff:
    13.8 +  "{a..<b} = {a..b} - {b}"
    13.9 +  by (auto simp add: atLeastLessThan_def atLeastAtMost_def)
   13.10 +
   13.11  end
   13.12  
   13.13  subsubsection\<open>Emptyness, singletons, subset\<close>
   13.14 @@ -842,6 +846,7 @@
   13.15    apply (simp_all add: atLeastLessThanSuc)
   13.16    done
   13.17  
   13.18 +
   13.19  subsubsection \<open>Intervals and numerals\<close>
   13.20  
   13.21  lemma lessThan_nat_numeral:  \<comment>\<open>Evaluation for specific numerals\<close>
   13.22 @@ -858,32 +863,74 @@
   13.23                   else {})"
   13.24    by (simp add: numeral_eq_Suc atLeastLessThanSuc)
   13.25  
   13.26 +
   13.27  subsubsection \<open>Image\<close>
   13.28  
   13.29 -lemma image_add_atLeastAtMost [simp]:
   13.30 -  fixes k ::"'a::linordered_semidom"
   13.31 -  shows "(\<lambda>n. n+k) ` {i..j} = {i+k..j+k}" (is "?A = ?B")
   13.32 +context linordered_semidom
   13.33 +begin
   13.34 +
   13.35 +lemma image_add_atLeast_atMost [simp]:
   13.36 +  "plus k ` {i..j} = {i + k..j + k}" (is "?A = ?B")
   13.37  proof
   13.38 -  show "?A \<subseteq> ?B" by auto
   13.39 +  show "?A \<subseteq> ?B"
   13.40 +    by (auto simp add: ac_simps)
   13.41  next
   13.42    show "?B \<subseteq> ?A"
   13.43    proof
   13.44 -    fix n assume a: "n : ?B"
   13.45 -    hence "n - k : {i..j}"
   13.46 -      by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le)
   13.47 -    moreover have "n = (n - k) + k" using a
   13.48 +    fix n
   13.49 +    assume "n \<in> ?B"
   13.50 +    then have "i \<le> n - k"
   13.51 +      by (simp add: add_le_imp_le_diff)
   13.52 +    have "n = n - k + k"
   13.53      proof -
   13.54 -      have "k + i \<le> n"
   13.55 -        by (metis a add.commute atLeastAtMost_iff)
   13.56 -      hence "k + (n - k) = n"
   13.57 -        by (metis (no_types) ab_semigroup_add_class.add_ac(1) add_diff_cancel_left' le_add_diff_inverse)
   13.58 -      thus ?thesis
   13.59 -        by (simp add: add.commute)
   13.60 +      from \<open>n \<in> ?B\<close> have "n = n - (i + k) + (i + k)"
   13.61 +        by simp
   13.62 +      also have "\<dots> = n - k - i + i + k"
   13.63 +        by (simp add: algebra_simps)
   13.64 +      also have "\<dots> = n - k + k"
   13.65 +        using \<open>i \<le> n - k\<close> by simp
   13.66 +      finally show ?thesis .
   13.67      qed
   13.68 -    ultimately show "n : ?A" by blast
   13.69 +    moreover have "n - k \<in> {i..j}"
   13.70 +      using \<open>n \<in> ?B\<close>
   13.71 +      by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le)
   13.72 +    ultimately show "n \<in> ?A"
   13.73 +      by (simp add: ac_simps) 
   13.74    qed
   13.75  qed
   13.76  
   13.77 +lemma image_add_atLeast_atMost' [simp]:
   13.78 +  "(\<lambda>n. n + k) ` {i..j} = {i + k..j + k}"
   13.79 +  by (simp add: add.commute [of _ k])
   13.80 +
   13.81 +lemma image_add_atLeast_lessThan [simp]:
   13.82 +  "plus k ` {i..<j} = {i + k..<j + k}"
   13.83 +  by (simp add: image_set_diff atLeast_lessThan_eq_atLeast_atMost_diff ac_simps)
   13.84 +
   13.85 +lemma image_add_atLeast_lessThan' [simp]:
   13.86 +  "(\<lambda>n. n + k) ` {i..<j} = {i + k..<j + k}"
   13.87 +  by (simp add: add.commute [of _ k])
   13.88 +
   13.89 +end
   13.90 +
   13.91 +lemma image_Suc_atLeast_atMost [simp]:
   13.92 +  "Suc ` {i..j} = {Suc i..Suc j}"
   13.93 +  using image_add_atLeast_atMost [of 1 i j]
   13.94 +    by (simp only: plus_1_eq_Suc) simp
   13.95 +
   13.96 +lemma image_Suc_atLeast_lessThan [simp]:
   13.97 +  "Suc ` {i..<j} = {Suc i..<Suc j}"
   13.98 +  using image_add_atLeast_lessThan [of 1 i j]
   13.99 +    by (simp only: plus_1_eq_Suc) simp
  13.100 +
  13.101 +corollary image_Suc_atMost:
  13.102 +  "Suc ` {..n} = {1..Suc n}"
  13.103 +  by (simp add: atMost_atLeast0 atLeastLessThanSuc_atLeastAtMost)
  13.104 +
  13.105 +corollary image_Suc_lessThan:
  13.106 +  "Suc ` {..<n} = {1..n}"
  13.107 +  by (simp add: lessThan_atLeast0 atLeastLessThanSuc_atLeastAtMost)
  13.108 +  
  13.109  lemma image_diff_atLeastAtMost [simp]:
  13.110    fixes d::"'a::linordered_idom" shows "(op - d ` {a..b}) = {d-b..d-a}"
  13.111    apply auto
  13.112 @@ -930,38 +977,6 @@
  13.113    using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]
  13.114    by (simp add: field_class.field_divide_inverse algebra_simps)
  13.115  
  13.116 -lemma image_add_atLeastLessThan:
  13.117 -  "(%n::nat. n+k) ` {i..<j} = {i+k..<j+k}" (is "?A = ?B")
  13.118 -proof
  13.119 -  show "?A \<subseteq> ?B" by auto
  13.120 -next
  13.121 -  show "?B \<subseteq> ?A"
  13.122 -  proof
  13.123 -    fix n assume a: "n : ?B"
  13.124 -    hence "n - k : {i..<j}" by auto
  13.125 -    moreover have "n = (n - k) + k" using a by auto
  13.126 -    ultimately show "n : ?A" by blast
  13.127 -  qed
  13.128 -qed
  13.129 -
  13.130 -corollary image_Suc_lessThan:
  13.131 -  "Suc ` {..<n} = {1..n}"
  13.132 -  using image_add_atLeastLessThan [of 1 0 n]
  13.133 -  by (auto simp add: lessThan_Suc_atMost atLeast0LessThan)
  13.134 -
  13.135 -corollary image_Suc_atMost:
  13.136 -  "Suc ` {..n} = {1..Suc n}"
  13.137 -  using image_add_atLeastLessThan [of 1 0 "Suc n"]
  13.138 -  by (auto simp add: lessThan_Suc_atMost atLeast0LessThan)
  13.139 -
  13.140 -corollary image_Suc_atLeastAtMost[simp]:
  13.141 -  "Suc ` {i..j} = {Suc i..Suc j}"
  13.142 -using image_add_atLeastAtMost[where k="Suc 0"] by simp
  13.143 -
  13.144 -corollary image_Suc_atLeastLessThan[simp]:
  13.145 -  "Suc ` {i..<j} = {Suc i..<Suc j}"
  13.146 -using image_add_atLeastLessThan[where k="Suc 0"] by simp
  13.147 -
  13.148  lemma atLeast1_lessThan_eq_remove0:
  13.149    "{Suc 0..<n} = {..<n} - {0}"
  13.150    by auto
  13.151 @@ -994,7 +1009,12 @@
  13.152    qed
  13.153  qed auto
  13.154  
  13.155 -lemma image_int_atLeastLessThan: "int ` {a..<b} = {int a..<int b}"
  13.156 +lemma image_int_atLeast_lessThan:
  13.157 +  "int ` {a..<b} = {int a..<int b}"
  13.158 +  by (auto intro!: image_eqI [where x = "nat x" for x])
  13.159 +
  13.160 +lemma image_int_atLeast_atMost:
  13.161 +  "int ` {a..b} = {int a..int b}"
  13.162    by (auto intro!: image_eqI [where x = "nat x" for x])
  13.163  
  13.164  context ordered_ab_group_add
  13.165 @@ -1532,42 +1552,73 @@
  13.166  
  13.167  subsection \<open>Generic big monoid operation over intervals\<close>
  13.168  
  13.169 -lemma inj_on_add_nat' [simp]:
  13.170 -  "inj_on (plus k) N" for k :: nat
  13.171 +context semiring_char_0
  13.172 +begin
  13.173 +
  13.174 +lemma inj_on_of_nat [simp]:
  13.175 +  "inj_on of_nat N"
  13.176    by rule simp
  13.177  
  13.178 +lemma bij_betw_of_nat [simp]:
  13.179 +  "bij_betw of_nat N A \<longleftrightarrow> of_nat ` N = A"
  13.180 +  by (simp add: bij_betw_def)
  13.181 +
  13.182 +end
  13.183 +
  13.184  context comm_monoid_set
  13.185  begin
  13.186  
  13.187 -lemma atLeast_lessThan_shift_bounds:
  13.188 -  fixes m n k :: nat
  13.189 -  shows "F g {m + k..<n + k} = F (g \<circ> plus k) {m..<n}"
  13.190 +lemma atLeast_lessThan_reindex:
  13.191 +  "F g {h m..<h n} = F (g \<circ> h) {m..<n}"
  13.192 +  if "bij_betw h {m..<n} {h m..<h n}" for m n ::nat
  13.193  proof -
  13.194 -  have "{m + k..<n + k} = plus k ` {m..<n}"
  13.195 -    by (auto simp add: image_add_atLeastLessThan [symmetric])
  13.196 -  also have "F g (plus k ` {m..<n}) = F (g \<circ> plus k) {m..<n}"
  13.197 -    by (rule reindex) simp
  13.198 -  finally show ?thesis .
  13.199 +  from that have "inj_on h {m..<n}" and "h ` {m..<n} = {h m..<h n}"
  13.200 +    by (simp_all add: bij_betw_def)
  13.201 +  then show ?thesis
  13.202 +    using reindex [of h "{m..<n}" g] by simp
  13.203  qed
  13.204  
  13.205 +lemma atLeast_atMost_reindex:
  13.206 +  "F g {h m..h n} = F (g \<circ> h) {m..n}"
  13.207 +  if "bij_betw h {m..n} {h m..h n}" for m n ::nat
  13.208 +proof -
  13.209 +  from that have "inj_on h {m..n}" and "h ` {m..n} = {h m..h n}"
  13.210 +    by (simp_all add: bij_betw_def)
  13.211 +  then show ?thesis
  13.212 +    using reindex [of h "{m..n}" g] by simp
  13.213 +qed
  13.214 +
  13.215 +lemma atLeast_lessThan_shift_bounds:
  13.216 +  "F g {m + k..<n + k} = F (g \<circ> plus k) {m..<n}"
  13.217 +  for m n k :: nat
  13.218 +  using atLeast_lessThan_reindex [of "plus k" m n g]
  13.219 +  by (simp add: ac_simps)
  13.220 +
  13.221  lemma atLeast_atMost_shift_bounds:
  13.222 -  fixes m n k :: nat
  13.223 -  shows "F g {m + k..n + k} = F (g \<circ> plus k) {m..n}"
  13.224 -proof -
  13.225 -  have "{m + k..n + k} = plus k ` {m..n}"
  13.226 -    by (auto simp del: image_add_atLeastAtMost simp add: image_add_atLeastAtMost [symmetric])
  13.227 -  also have "F g (plus k ` {m..n}) = F (g \<circ> plus k) {m..n}"
  13.228 -    by (rule reindex) simp
  13.229 -  finally show ?thesis .
  13.230 -qed
  13.231 +  "F g {m + k..n + k} = F (g \<circ> plus k) {m..n}"
  13.232 +  for m n k :: nat
  13.233 +  using atLeast_atMost_reindex [of "plus k" m n g]
  13.234 +  by (simp add: ac_simps)
  13.235  
  13.236  lemma atLeast_Suc_lessThan_Suc_shift:
  13.237    "F g {Suc m..<Suc n} = F (g \<circ> Suc) {m..<n}"
  13.238 -  using atLeast_lessThan_shift_bounds [of _ _ 1] by simp
  13.239 +  using atLeast_lessThan_shift_bounds [of _ _ 1]
  13.240 +  by (simp add: plus_1_eq_Suc)
  13.241  
  13.242  lemma atLeast_Suc_atMost_Suc_shift:
  13.243    "F g {Suc m..Suc n} = F (g \<circ> Suc) {m..n}"
  13.244 -  using atLeast_atMost_shift_bounds [of _ _ 1] by simp
  13.245 +  using atLeast_atMost_shift_bounds [of _ _ 1]
  13.246 +  by (simp add: plus_1_eq_Suc)
  13.247 +
  13.248 +lemma atLeast_int_lessThan_int_shift:
  13.249 +  "F g {int m..<int n} = F (g \<circ> int) {m..<n}"
  13.250 +  by (rule atLeast_lessThan_reindex)
  13.251 +    (simp add: image_int_atLeast_lessThan)
  13.252 +
  13.253 +lemma atLeast_int_atMost_int_shift:
  13.254 +  "F g {int m..int n} = F (g \<circ> int) {m..n}"
  13.255 +  by (rule atLeast_atMost_reindex)
  13.256 +    (simp add: image_int_atLeast_atMost)
  13.257  
  13.258  lemma atLeast0_lessThan_Suc:
  13.259    "F g {0..<Suc n} = F g {0..<n} \<^bold>* g n"
  13.260 @@ -1780,6 +1831,9 @@
  13.261  lemma nat_diff_sum_reindex: "(\<Sum>i<n. f (n - Suc i)) = (\<Sum>i<n. f i)"
  13.262    by (rule sum.reindex_bij_witness[where i="\<lambda>i. n - Suc i" and j="\<lambda>i. n - Suc i"]) auto
  13.263  
  13.264 +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)"
  13.265 +  by (subst sum_subtractf_nat) auto
  13.266 +
  13.267  
  13.268  subsubsection \<open>Shifting bounds\<close>
  13.269  
  13.270 @@ -1799,15 +1853,45 @@
  13.271    "sum f {Suc m..<Suc n} = sum (%i. f(Suc i)){m..<n}"
  13.272  by (simp add:sum_shift_bounds_nat_ivl[where k="Suc 0", simplified])
  13.273  
  13.274 -lemma sum_shift_lb_Suc0_0:
  13.275 -  "f(0::nat) = (0::nat) \<Longrightarrow> sum f {Suc 0..k} = sum f {0..k}"
  13.276 -by(simp add:sum_head_Suc)
  13.277 +context comm_monoid_add
  13.278 +begin
  13.279 +
  13.280 +context
  13.281 +  fixes f :: "nat \<Rightarrow> 'a"
  13.282 +  assumes "f 0 = 0"
  13.283 +begin
  13.284  
  13.285  lemma sum_shift_lb_Suc0_0_upt:
  13.286 -  "f(0::nat) = 0 \<Longrightarrow> sum f {Suc 0..<k} = sum f {0..<k}"
  13.287 -apply(cases k)apply simp
  13.288 -apply(simp add:sum_head_upt_Suc)
  13.289 -done
  13.290 +  "sum f {Suc 0..<k} = sum f {0..<k}"
  13.291 +proof (cases k)
  13.292 +  case 0
  13.293 +  then show ?thesis
  13.294 +    by simp
  13.295 +next
  13.296 +  case (Suc k)
  13.297 +  moreover have "{0..<Suc k} = insert 0 {Suc 0..<Suc k}"
  13.298 +    by auto
  13.299 +  ultimately show ?thesis
  13.300 +    using \<open>f 0 = 0\<close> by simp
  13.301 +qed
  13.302 +
  13.303 +lemma sum_shift_lb_Suc0_0:
  13.304 +  "sum f {Suc 0..k} = sum f {0..k}"
  13.305 +proof (cases k)
  13.306 +  case 0
  13.307 +  with \<open>f 0 = 0\<close> show ?thesis
  13.308 +    by simp
  13.309 +next
  13.310 +  case (Suc k)
  13.311 +  moreover have "{0..Suc k} = insert 0 {Suc 0..Suc k}"
  13.312 +    by auto
  13.313 +  ultimately show ?thesis
  13.314 +    using \<open>f 0 = 0\<close> by simp
  13.315 +qed
  13.316 +
  13.317 +end
  13.318 +
  13.319 +end
  13.320  
  13.321  lemma sum_atMost_Suc_shift:
  13.322    fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
  13.323 @@ -1892,7 +1976,7 @@
  13.324    by (induction m) (simp_all add: algebra_simps)
  13.325  
  13.326  
  13.327 -subsection \<open>The formula for geometric sums\<close>
  13.328 +subsubsection \<open>The formula for geometric sums\<close>
  13.329  
  13.330  lemma sum_power2: "(\<Sum>i=0..<k. (2::nat)^i) = 2^k-1"
  13.331  by (induction k) (auto simp: mult_2)
  13.332 @@ -1991,7 +2075,8 @@
  13.333  using sum_gp_multiplied [of m n x] apply auto
  13.334  by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
  13.335  
  13.336 -subsection\<open>Geometric progressions\<close>
  13.337 +
  13.338 +subsubsection\<open>Geometric progressions\<close>
  13.339  
  13.340  lemma sum_gp0:
  13.341    fixes x :: "'a::{comm_ring,division_ring}"
  13.342 @@ -2016,67 +2101,125 @@
  13.343    shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
  13.344    by (induct n) (auto simp: algebra_simps divide_simps)
  13.345  
  13.346 -subsubsection \<open>The formula for arithmetic sums\<close>
  13.347 +
  13.348 +subsubsection \<open>The formulae for arithmetic sums\<close>
  13.349 +
  13.350 +context comm_semiring_1
  13.351 +begin
  13.352 +
  13.353 +lemma double_gauss_sum:
  13.354 +  "2 * (\<Sum>i = 0..n. of_nat i) = of_nat n * (of_nat n + 1)"
  13.355 +  by (induct n) (simp_all add: sum.atLeast0_atMost_Suc algebra_simps left_add_twice)
  13.356 +
  13.357 +lemma double_gauss_sum_from_Suc_0:
  13.358 +  "2 * (\<Sum>i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1)"
  13.359 +proof -
  13.360 +  have "sum of_nat {Suc 0..n} = sum of_nat (insert 0 {Suc 0..n})"
  13.361 +    by simp
  13.362 +  also have "\<dots> = sum of_nat {0..n}"
  13.363 +    by (cases n) (simp_all add: atLeast0_atMost_Suc_eq_insert_0)
  13.364 +  finally show ?thesis
  13.365 +    by (simp add: double_gauss_sum)
  13.366 +qed
  13.367 +
  13.368 +lemma double_arith_series:
  13.369 +  "2 * (\<Sum>i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d)"
  13.370 +proof -
  13.371 +  have "(\<Sum>i = 0..n. a + of_nat i * d) = ((\<Sum>i = 0..n. a) + (\<Sum>i = 0..n. of_nat i * d))"
  13.372 +    by (rule sum.distrib)
  13.373 +  also have "\<dots> = (of_nat (Suc n) * a + d * (\<Sum>i = 0..n. of_nat i))"
  13.374 +    by (simp add: sum_distrib_left algebra_simps)
  13.375 +  finally show ?thesis
  13.376 +    by (simp add: algebra_simps double_gauss_sum left_add_twice)
  13.377 +qed
  13.378 +
  13.379 +end
  13.380 +
  13.381 +context semiring_parity
  13.382 +begin
  13.383  
  13.384  lemma gauss_sum:
  13.385 -  "(2::'a::comm_semiring_1)*(\<Sum>i\<in>{1..n}. of_nat i) = of_nat n*((of_nat n)+1)"
  13.386 -proof (induct n)
  13.387 -  case 0
  13.388 -  show ?case by simp
  13.389 -next
  13.390 -  case (Suc n)
  13.391 -  then show ?case
  13.392 -    by (simp add: algebra_simps add: one_add_one [symmetric] del: one_add_one)
  13.393 -      (* FIXME: make numeral cancellation simprocs work for semirings *)
  13.394 -qed
  13.395 -
  13.396 -theorem arith_series_general:
  13.397 -  "(2::'a::comm_semiring_1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
  13.398 -  of_nat n * (a + (a + of_nat(n - 1)*d))"
  13.399 -proof cases
  13.400 -  assume ngt1: "n > 1"
  13.401 -  let ?I = "\<lambda>i. of_nat i" and ?n = "of_nat n"
  13.402 -  have
  13.403 -    "(\<Sum>i\<in>{..<n}. a+?I i*d) =
  13.404 -     ((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))"
  13.405 -    by (rule sum.distrib)
  13.406 -  also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
  13.407 -  also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
  13.408 -    unfolding One_nat_def
  13.409 -    by (simp add: sum_distrib_left atLeast0LessThan[symmetric] sum_shift_lb_Suc0_0_upt ac_simps)
  13.410 -  also have "2*\<dots> = 2*?n*a + d*2*(\<Sum>i\<in>{1..<n}. ?I i)"
  13.411 -    by (simp add: algebra_simps)
  13.412 -  also from ngt1 have "{1..<n} = {1..n - 1}"
  13.413 -    by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
  13.414 -  also from ngt1
  13.415 -  have "2*?n*a + d*2*(\<Sum>i\<in>{1..n - 1}. ?I i) = (2*?n*a + d*?I (n - 1)*?I n)"
  13.416 -    by (simp only: mult.assoc gauss_sum [of "n - 1"], unfold One_nat_def)
  13.417 -      (simp add:  mult.commute trans [OF add.commute of_nat_Suc [symmetric]])
  13.418 -  finally show ?thesis
  13.419 -    unfolding mult_2 by (simp add: algebra_simps)
  13.420 -next
  13.421 -  assume "\<not>(n > 1)"
  13.422 -  hence "n = 1 \<or> n = 0" by auto
  13.423 -  thus ?thesis by (auto simp: mult_2)
  13.424 -qed
  13.425 +  "(\<Sum>i = 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2"
  13.426 +  using double_gauss_sum [of n, symmetric] by simp
  13.427 +
  13.428 +lemma gauss_sum_from_Suc_0:
  13.429 +  "(\<Sum>i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2"
  13.430 +  using double_gauss_sum_from_Suc_0 [of n, symmetric] by simp
  13.431 +
  13.432 +lemma arith_series:
  13.433 +  "(\<Sum>i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d) div 2"
  13.434 +  using double_arith_series [of a d n, symmetric] by simp
  13.435 +
  13.436 +end
  13.437 +
  13.438 +lemma gauss_sum_nat:
  13.439 +  "\<Sum>{0..n} = (n * Suc n) div 2"
  13.440 +  using gauss_sum [of n, where ?'a = nat] by simp
  13.441  
  13.442  lemma arith_series_nat:
  13.443 -  "(2::nat) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n - 1)*d))"
  13.444 +  "(\<Sum>i = 0..n. a + i * d) = Suc n * (2 * a + n * d) div 2"
  13.445 +  using arith_series [of a d n] by simp
  13.446 +
  13.447 +lemma Sum_Icc_int:
  13.448 +  "\<Sum>{m..n} = (n * (n + 1) - m * (m - 1)) div 2"
  13.449 +  if "m \<le> n" for m n :: int
  13.450 +using that proof (induct i \<equiv> "nat (n - m)" arbitrary: m n)
  13.451 +  case 0
  13.452 +  then have "m = n"
  13.453 +    by arith
  13.454 +  then show ?case
  13.455 +    by (simp add: algebra_simps mult_2 [symmetric])
  13.456 +next
  13.457 +  case (Suc i)
  13.458 +  have 0: "i = nat((n-1) - m)" "m \<le> n-1" using Suc(2,3) by arith+
  13.459 +  have "\<Sum> {m..n} = \<Sum> {m..1+(n-1)}" by simp
  13.460 +  also have "\<dots> = \<Sum> {m..n-1} + n" using \<open>m \<le> n\<close>
  13.461 +    by(subst atLeastAtMostPlus1_int_conv) simp_all
  13.462 +  also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n"
  13.463 +    by(simp add: Suc(1)[OF 0])
  13.464 +  also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp
  13.465 +  also have "\<dots> = (n*(n+1) - m*(m-1)) div 2"
  13.466 +    by (simp add: algebra_simps mult_2_right)
  13.467 +  finally show ?case .
  13.468 +qed
  13.469 +
  13.470 +lemma Sum_Icc_nat:
  13.471 +  "\<Sum>{m..n} = (n * (n + 1) - m * (m - 1)) div 2"
  13.472 +  if "m \<le> n" for m n :: nat
  13.473  proof -
  13.474 -  have
  13.475 -    "2 * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
  13.476 -    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
  13.477 -    by (rule arith_series_general)
  13.478 -  thus ?thesis
  13.479 -    unfolding One_nat_def by auto
  13.480 +  have *: "m * (m - 1) \<le> n * (n + 1)"
  13.481 +    using that by (meson diff_le_self order_trans le_add1 mult_le_mono)
  13.482 +  have "int (\<Sum>{m..n}) = (\<Sum>{int m..int n})"
  13.483 +    by (simp add: sum.atLeast_int_atMost_int_shift)
  13.484 +  also have "\<dots> = (int n * (int n + 1) - int m * (int m - 1)) div 2"
  13.485 +    using that by (simp add: Sum_Icc_int)
  13.486 +  also have "\<dots> = int ((n * (n + 1) - m * (m - 1)) div 2)"
  13.487 +    using le_square * by (simp add: algebra_simps of_nat_div of_nat_diff)
  13.488 +  finally show ?thesis
  13.489 +    by (simp only: of_nat_eq_iff)
  13.490  qed
  13.491  
  13.492 -lemma arith_series_int:
  13.493 -  "2 * (\<Sum>i\<in>{..<n}. a + int i * d) = int n * (a + (a + int(n - 1)*d))"
  13.494 -  by (fact arith_series_general) (* FIXME: duplicate *)
  13.495 -
  13.496 -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)"
  13.497 -  by (subst sum_subtractf_nat) auto
  13.498 +lemma Sum_Ico_nat: 
  13.499 +  "\<Sum>{m..<n} = (n * (n - 1) - m * (m - 1)) div 2"
  13.500 +  if "m \<le> n" for m n :: nat
  13.501 +proof -
  13.502 +  from that consider "m < n" | "m = n"
  13.503 +    by (auto simp add: less_le)
  13.504 +  then show ?thesis proof cases
  13.505 +    case 1
  13.506 +    then have "{m..<n} = {m..n - 1}"
  13.507 +      by auto
  13.508 +    then have "\<Sum>{m..<n} = \<Sum>{m..n - 1}"
  13.509 +      by simp
  13.510 +    also have "\<dots> = (n * (n - 1) - m * (m - 1)) div 2"
  13.511 +      using \<open>m < n\<close> by (simp add: Sum_Icc_nat mult.commute)
  13.512 +    finally show ?thesis .
  13.513 +  next
  13.514 +    case 2
  13.515 +    then show ?thesis
  13.516 +      by simp
  13.517 +  qed
  13.518 +qed
  13.519  
  13.520  
  13.521  subsubsection \<open>Division remainder\<close>
    14.1 --- a/src/HOL/ex/Function_Growth.thy	Sun Oct 29 19:39:03 2017 +0100
    14.2 +++ b/src/HOL/ex/Function_Growth.thy	Mon Oct 30 13:18:41 2017 +0000
    14.3 @@ -10,40 +10,6 @@
    14.4    "HOL-Library.Discrete"
    14.5  begin
    14.6  
    14.7 -(* FIXME move *)
    14.8 -
    14.9 -context linorder
   14.10 -begin
   14.11 -
   14.12 -lemma mono_invE:
   14.13 -  fixes f :: "'a \<Rightarrow> 'b::order"
   14.14 -  assumes "mono f"
   14.15 -  assumes "f x < f y"
   14.16 -  obtains "x < y"
   14.17 -proof
   14.18 -  show "x < y"
   14.19 -  proof (rule ccontr)
   14.20 -    assume "\<not> x < y"
   14.21 -    then have "y \<le> x" by simp
   14.22 -    with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
   14.23 -    with \<open>f x < f y\<close> show False by simp
   14.24 -  qed
   14.25 -qed
   14.26 -
   14.27 -end
   14.28 -
   14.29 -lemma (in semidom_divide) power_diff:
   14.30 -  fixes a :: 'a
   14.31 -  assumes "a \<noteq> 0"
   14.32 -  assumes "m \<ge> n"
   14.33 -  shows "a ^ (m - n) = (a ^ m) div (a ^ n)"
   14.34 -proof -
   14.35 -  define q where "q = m - n"
   14.36 -  with assms have "m = q + n" by (simp add: q_def)
   14.37 -  with q_def show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
   14.38 -qed
   14.39 -
   14.40 -
   14.41  subsection \<open>Motivation\<close>
   14.42  
   14.43  text \<open>