# HG changeset patch # User nipkow # Date 1220289400 -7200 # Node ID f6b2d19951710840d2fc8747c4550b5b5dd78e7b # Parent 4b6783d3f0d99415235d1014c8964994b7024217 cleaned up code generation for {.._} and {..<_} moved lemmas into SetInterval where they belong diff -r 4b6783d3f0d9 -r f6b2d1995171 src/HOL/List.thy --- a/src/HOL/List.thy Mon Sep 01 10:28:04 2008 +0200 +++ b/src/HOL/List.thy Mon Sep 01 19:16:40 2008 +0200 @@ -3626,14 +3626,6 @@ text {* Code for bounded quantification and summation over nats. *} -lemma atMost_upto [code unfold]: - "{..n} = set [0.. 'a set" ("(1{..<_})") - "{.. 'a set" ("(1{.._})") - "{..u} == {x. x<=u}" - - greaterThan :: "('a::ord) => 'a set" ("(1{_<..})") - "{l<..} == {x. l 'a set" ("(1{_..})") - "{l..} == {x. l<=x}" - - greaterThanLessThan :: "['a::ord, 'a] => 'a set" ("(1{_<..<_})") - "{l<.. 'a set" ("(1{_..<_})") - "{l.. 'a set" ("(1{_<.._})") - "{l<..u} == {l<..} Int {..u}" - - atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})") - "{l..u} == {l..} Int {..u}" -*) text{* A note of warning when using @{term"{.. finite N" - -- {* A bounded set of natural numbers is finite. *} - apply (rule finite_subset) - apply (rule_tac [2] finite_lessThan, auto) - done +apply (rule finite_subset) + apply (rule_tac [2] finite_lessThan, auto) +done + +lemma finite_less_ub: + "!!f::nat=>nat. (!!n. n \ f n) ==> finite {n. f n \ u}" +by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans) text{* Any subset of an interval of natural numbers the size of the subset is exactly that interval. *} @@ -800,6 +784,32 @@ (\i=n..m+1. f i) = (\i=n..m. f i) + f(m + 1)" by (auto simp:add_ac atLeastAtMostSuc_conv) *) + +lemma setsum_head: + fixes n :: nat + assumes mn: "m <= n" + shows "(\x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs") +proof - + from mn + have "{m..n} = {m} \ {m<..n}" + by (auto intro: ivl_disj_un_singleton) + hence "?lhs = (\x\{m} \ {m<..n}. P x)" + by (simp add: atLeast0LessThan) + also have "\ = ?rhs" by simp + finally show ?thesis . +qed + +lemma setsum_head_Suc: + "m \ n \ setsum f {m..n} = f m + setsum f {Suc m..n}" +by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost) + +lemma setsum_head_upt_Suc: + "m < n \ setsum f {m.. m \ n; n \ p \ \ setsum f {m..x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs") -proof - - from mn - have "{m..n} = {m} \ {m<..n}" - by (auto intro: ivl_disj_un_singleton) - hence "?lhs = (\x\{m} \ {m<..n}. P x)" - by (simp add: atLeast0LessThan) - also have "\ = ?rhs" by simp - finally show ?thesis . -qed +lemma setsum_shift_lb_Suc0_0: + "f(0::nat) = (0::nat) \ setsum f {Suc 0..k} = setsum f {0..k}" +by(simp add:setsum_head_Suc) -lemma setsum_head_upt: - fixes m::nat - assumes m: "0 < m" - shows "(\xx\{1..xx\{0.. = (\x\{0..m - 1}. P x)" - by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost) - also - have "\ = P 0 + (\x\{0<..m - 1}. P x)" - by (simp add: setsum_head) - also - from m - have "{0<..m - 1} = {1.. setsum f {Suc 0.. = ?n*a + (\i\{.. = (?n*a + d*(\i\{1.. = (1+1)*?n*a + d*(1+1)*(\i\{1..i\{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)" by (simp only: mult_ac gauss_sum [of "n - 1"]) (simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]])