# HG changeset patch # User nipkow # Date 1430504757 -7200 # Node ID 9a97407488cda52a7cf9572656d963e7434de534 # Parent 29c826137153659a8dc86796eb16ca090fb9c4a3 simplified statement and proof diff -r 29c826137153 -r 9a97407488cd src/HOL/Inequalities.thy --- a/src/HOL/Inequalities.thy Fri May 01 11:36:16 2015 +0100 +++ b/src/HOL/Inequalities.thy Fri May 01 20:25:57 2015 +0200 @@ -7,30 +7,22 @@ imports Real_Vector_Spaces begin -lemma gauss_sum_div2: "(2::'a::semiring_div) \ 0 \ - setsum of_nat {1..n} = of_nat n * (of_nat n + 1) div (2::'a)" -using gauss_sum[where n=n and 'a = 'a,symmetric] by auto - -lemma Setsum_Icc_int: assumes "0 \ m" and "(m::int) \ n" -shows "\ {m..n} = (n*(n+1) - m*(m-1)) div 2" -proof- - { fix k::int assume "k\0" - hence "\ {1..k::int} = k * (k+1) div 2" - by (rule gauss_sum_div2[where 'a = int, transferred]) simp - } note 1 = this - have "{m..n} = {0..n} - {0..m-1}" using `m\0` by auto - hence "\{m..n} = \{0..n} - \{0..m-1}" using assms - by (force intro!: setsum_diff) - also have "{0..n} = {0} Un {1..n}" using assms by auto - also have "\({0} \ {1..n}) = \{1..n}" by(simp add: setsum.union_disjoint) - also have "\ = n * (n+1) div 2" by(rule 1[OF order_trans[OF assms]]) - also have "{0..m-1} = (if m=0 then {} else {0} Un {1..m-1})" - using assms by auto - also have "\ \ = m*(m-1) div 2" using `m\0` by(simp add: 1 mult.commute) - also have "n*(n+1) div 2 - m*(m-1) div 2 = (n*(n+1) - m*(m-1)) div 2" - apply(subgoal_tac "even(n*(n+1)) \ even(m*(m-1))") - by (auto (*simp: even_def[symmetric]*)) - finally show ?thesis . +lemma Setsum_Icc_int: "(m::int) \ n \ \ {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 \ n-1" using Suc(2,3) by arith+ + have "\ {m..n} = \ {m..1+(n-1)}" by simp + also have "\ = \ {m..n-1} + n" using `m \ n` + by(subst atLeastAtMostPlus1_int_conv) simp_all + also have "\ = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n" + by(simp add: Suc(1)[OF 0]) + also have "\ = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp + also have "\ = (n*(n+1) - m*(m-1)) div 2" by(simp add: algebra_simps) + finally show ?case . qed lemma Setsum_Icc_nat: assumes "(m::nat) \ n" @@ -39,7 +31,7 @@ have "m*(m-1) \ n*(n + 1)" using assms by (meson diff_le_self order_trans le_add1 mult_le_mono) hence "int(\ {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms - by (auto simp add: Setsum_Icc_int[transferred, OF _ assms] zdiv_int int_mult + by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int int_mult split: zdiff_int_split) thus ?thesis by simp qed