1.1 --- a/src/HOL/List.thy Mon Sep 01 10:28:04 2008 +0200
1.2 +++ b/src/HOL/List.thy Mon Sep 01 19:16:40 2008 +0200
1.3 @@ -3626,14 +3626,6 @@
1.4
1.5 text {* Code for bounded quantification and summation over nats. *}
1.6
1.7 -lemma atMost_upto [code unfold]:
1.8 - "{..n} = set [0..<Suc n]"
1.9 -by auto
1.10 -
1.11 -lemma atLeast_upt [code unfold]:
1.12 - "{..<n} = set [0..<n]"
1.13 -by auto
1.14 -
1.15 lemma greaterThanLessThan_upt [code unfold]:
1.16 "{n<..<m} = set [Suc n..<m]"
1.17 by auto
2.1 --- a/src/HOL/SetInterval.thy Mon Sep 01 10:28:04 2008 +0200
2.2 +++ b/src/HOL/SetInterval.thy Mon Sep 01 19:16:40 2008 +0200
2.3 @@ -48,32 +48,7 @@
2.4 "{l..u} == {l..} Int {..u}"
2.5
2.6 end
2.7 -(*
2.8 -constdefs
2.9 - lessThan :: "('a::ord) => 'a set" ("(1{..<_})")
2.10 - "{..<u} == {x. x<u}"
2.11
2.12 - atMost :: "('a::ord) => 'a set" ("(1{.._})")
2.13 - "{..u} == {x. x<=u}"
2.14 -
2.15 - greaterThan :: "('a::ord) => 'a set" ("(1{_<..})")
2.16 - "{l<..} == {x. l<x}"
2.17 -
2.18 - atLeast :: "('a::ord) => 'a set" ("(1{_..})")
2.19 - "{l..} == {x. l<=x}"
2.20 -
2.21 - greaterThanLessThan :: "['a::ord, 'a] => 'a set" ("(1{_<..<_})")
2.22 - "{l<..<u} == {l<..} Int {..<u}"
2.23 -
2.24 - atLeastLessThan :: "['a::ord, 'a] => 'a set" ("(1{_..<_})")
2.25 - "{l..<u} == {l..} Int {..<u}"
2.26 -
2.27 - greaterThanAtMost :: "['a::ord, 'a] => 'a set" ("(1{_<.._})")
2.28 - "{l<..u} == {l<..} Int {..u}"
2.29 -
2.30 - atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})")
2.31 - "{l..u} == {l..} Int {..u}"
2.32 -*)
2.33
2.34 text{* A note of warning when using @{term"{..<n}"} on type @{typ
2.35 nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving
2.36 @@ -297,16 +272,21 @@
2.37
2.38 subsubsection {* The Constant @{term atLeastLessThan} *}
2.39
2.40 -text{*The orientation of the following rule is tricky. The lhs is
2.41 +text{*The orientation of the following 2 rules is tricky. The lhs is
2.42 defined in terms of the rhs. Hence the chosen orientation makes sense
2.43 in this theory --- the reverse orientation complicates proofs (eg
2.44 nontermination). But outside, when the definition of the lhs is rarely
2.45 used, the opposite orientation seems preferable because it reduces a
2.46 specific concept to a more general one. *}
2.47 +
2.48 lemma atLeast0LessThan: "{0::nat..<n} = {..<n}"
2.49 by(simp add:lessThan_def atLeastLessThan_def)
2.50
2.51 +lemma atLeast0AtMost: "{0..n::nat} = {..n}"
2.52 +by(simp add:atMost_def atLeastAtMost_def)
2.53 +
2.54 declare atLeast0LessThan[symmetric, code unfold]
2.55 + atLeast0AtMost[symmetric, code unfold]
2.56
2.57 lemma atLeastLessThan0: "{m..<0::nat} = {}"
2.58 by (simp add: atLeastLessThan_def)
2.59 @@ -411,12 +391,16 @@
2.60 fixes l :: nat shows "finite {l..u}"
2.61 by (simp add: atLeastAtMost_def)
2.62
2.63 +text {* A bounded set of natural numbers is finite. *}
2.64 lemma bounded_nat_set_is_finite:
2.65 "(ALL i:N. i < (n::nat)) ==> finite N"
2.66 - -- {* A bounded set of natural numbers is finite. *}
2.67 - apply (rule finite_subset)
2.68 - apply (rule_tac [2] finite_lessThan, auto)
2.69 - done
2.70 +apply (rule finite_subset)
2.71 + apply (rule_tac [2] finite_lessThan, auto)
2.72 +done
2.73 +
2.74 +lemma finite_less_ub:
2.75 + "!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}"
2.76 +by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
2.77
2.78 text{* Any subset of an interval of natural numbers the size of the
2.79 subset is exactly that interval. *}
2.80 @@ -800,6 +784,32 @@
2.81 (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
2.82 by (auto simp:add_ac atLeastAtMostSuc_conv)
2.83 *)
2.84 +
2.85 +lemma setsum_head:
2.86 + fixes n :: nat
2.87 + assumes mn: "m <= n"
2.88 + shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs")
2.89 +proof -
2.90 + from mn
2.91 + have "{m..n} = {m} \<union> {m<..n}"
2.92 + by (auto intro: ivl_disj_un_singleton)
2.93 + hence "?lhs = (\<Sum>x\<in>{m} \<union> {m<..n}. P x)"
2.94 + by (simp add: atLeast0LessThan)
2.95 + also have "\<dots> = ?rhs" by simp
2.96 + finally show ?thesis .
2.97 +qed
2.98 +
2.99 +lemma setsum_head_Suc:
2.100 + "m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {Suc m..n}"
2.101 +by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)
2.102 +
2.103 +lemma setsum_head_upt_Suc:
2.104 + "m < n \<Longrightarrow> setsum f {m..<n} = f m + setsum f {Suc m..<n}"
2.105 +apply(insert setsum_head_Suc[of m "n - 1" f])
2.106 +apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] ring_simps)
2.107 +done
2.108 +
2.109 +
2.110 lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
2.111 setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
2.112 by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)
2.113 @@ -812,6 +822,7 @@
2.114 apply (simp add: add_ac)
2.115 done
2.116
2.117 +
2.118 subsection{* Shifting bounds *}
2.119
2.120 lemma setsum_shift_bounds_nat_ivl:
2.121 @@ -832,40 +843,15 @@
2.122 "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
2.123 by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified])
2.124
2.125 -lemma setsum_head:
2.126 - fixes n :: nat
2.127 - assumes mn: "m <= n"
2.128 - shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs")
2.129 -proof -
2.130 - from mn
2.131 - have "{m..n} = {m} \<union> {m<..n}"
2.132 - by (auto intro: ivl_disj_un_singleton)
2.133 - hence "?lhs = (\<Sum>x\<in>{m} \<union> {m<..n}. P x)"
2.134 - by (simp add: atLeast0LessThan)
2.135 - also have "\<dots> = ?rhs" by simp
2.136 - finally show ?thesis .
2.137 -qed
2.138 +lemma setsum_shift_lb_Suc0_0:
2.139 + "f(0::nat) = (0::nat) \<Longrightarrow> setsum f {Suc 0..k} = setsum f {0..k}"
2.140 +by(simp add:setsum_head_Suc)
2.141
2.142 -lemma setsum_head_upt:
2.143 - fixes m::nat
2.144 - assumes m: "0 < m"
2.145 - shows "(\<Sum>x<m. P x) = P 0 + (\<Sum>x\<in>{1..<m}. P x)"
2.146 -proof -
2.147 - have "(\<Sum>x<m. P x) = (\<Sum>x\<in>{0..<m}. P x)"
2.148 - by (simp add: atLeast0LessThan)
2.149 - also
2.150 - from m
2.151 - have "\<dots> = (\<Sum>x\<in>{0..m - 1}. P x)"
2.152 - by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost)
2.153 - also
2.154 - have "\<dots> = P 0 + (\<Sum>x\<in>{0<..m - 1}. P x)"
2.155 - by (simp add: setsum_head)
2.156 - also
2.157 - from m
2.158 - have "{0<..m - 1} = {1..<m}"
2.159 - by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost)
2.160 - finally show ?thesis .
2.161 -qed
2.162 +lemma setsum_shift_lb_Suc0_0_upt:
2.163 + "f(0::nat) = 0 \<Longrightarrow> setsum f {Suc 0..<k} = setsum f {0..<k}"
2.164 +apply(cases k)apply simp
2.165 +apply(simp add:setsum_head_upt_Suc)
2.166 +done
2.167
2.168 subsection {* The formula for geometric sums *}
2.169
2.170 @@ -899,12 +885,12 @@
2.171 by (rule setsum_addf)
2.172 also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
2.173 also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
2.174 - by (simp add: setsum_right_distrib setsum_head_upt mult_ac)
2.175 + by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac)
2.176 also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
2.177 by (simp add: left_distrib right_distrib)
2.178 also from ngt1 have "{1..<n} = {1..n - 1}"
2.179 - by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
2.180 - also from ngt1
2.181 + by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
2.182 + also from ngt1
2.183 have "(1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)"
2.184 by (simp only: mult_ac gauss_sum [of "n - 1"])
2.185 (simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]])