equal
deleted
inserted
replaced
14 thus ?case by (simp add: algebra_simps) |
14 thus ?case by (simp add: algebra_simps) |
15 next |
15 next |
16 case (Suc i) |
16 case (Suc i) |
17 have 0: "i = nat((n-1) - m)" "m \<le> n-1" using Suc(2,3) by arith+ |
17 have 0: "i = nat((n-1) - m)" "m \<le> n-1" using Suc(2,3) by arith+ |
18 have "\<Sum> {m..n} = \<Sum> {m..1+(n-1)}" by simp |
18 have "\<Sum> {m..n} = \<Sum> {m..1+(n-1)}" by simp |
19 also have "\<dots> = \<Sum> {m..n-1} + n" using `m \<le> n` |
19 also have "\<dots> = \<Sum> {m..n-1} + n" using \<open>m \<le> n\<close> |
20 by(subst atLeastAtMostPlus1_int_conv) simp_all |
20 by(subst atLeastAtMostPlus1_int_conv) simp_all |
21 also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n" |
21 also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n" |
22 by(simp add: Suc(1)[OF 0]) |
22 by(simp add: Suc(1)[OF 0]) |
23 also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp |
23 also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp |
24 also have "\<dots> = (n*(n+1) - m*(m-1)) div 2" by(simp add: algebra_simps) |
24 also have "\<dots> = (n*(n+1) - m*(m-1)) div 2" by(simp add: algebra_simps) |
41 proof cases |
41 proof cases |
42 assume "m < n" |
42 assume "m < n" |
43 hence "{m..<n} = {m..n-1}" by auto |
43 hence "{m..<n} = {m..n-1}" by auto |
44 hence "\<Sum>{m..<n} = \<Sum>{m..n-1}" by simp |
44 hence "\<Sum>{m..<n} = \<Sum>{m..n-1}" by simp |
45 also have "\<dots> = (n*(n-1) - m*(m-1)) div 2" |
45 also have "\<dots> = (n*(n-1) - m*(m-1)) div 2" |
46 using assms `m < n` by (simp add: Setsum_Icc_nat mult.commute) |
46 using assms \<open>m < n\<close> by (simp add: Setsum_Icc_nat mult.commute) |
47 finally show ?thesis . |
47 finally show ?thesis . |
48 next |
48 next |
49 assume "\<not> m < n" with assms show ?thesis by simp |
49 assume "\<not> m < n" with assms show ?thesis by simp |
50 qed |
50 qed |
51 |
51 |