author  kleing 
Wed, 26 Apr 2006 07:01:33 +0200  
changeset 19469  958d2f2dd8d4 
parent 19376  529b735edbf2 
child 19538  ae6d01fa2d8a 
permissions  rwrr 
8924  1 
(* Title: HOL/SetInterval.thy 
2 
ID: $Id$ 

13735  3 
Author: Tobias Nipkow and Clemens Ballarin 
14485  4 
Additions by Jeremy Avigad in March 2004 
8957  5 
Copyright 2000 TU Muenchen 
8924  6 

13735  7 
lessThan, greaterThan, atLeast, atMost and twosided intervals 
8924  8 
*) 
9 

14577  10 
header {* Set intervals *} 
11 

15131  12 
theory SetInterval 
15140  13 
imports IntArith 
15131  14 
begin 
8924  15 

16 
constdefs 

15045  17 
lessThan :: "('a::ord) => 'a set" ("(1{..<_})") 
18 
"{..<u} == {x. x<u}" 

8924  19 

11609
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset

20 
atMost :: "('a::ord) => 'a set" ("(1{.._})") 
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset

21 
"{..u} == {x. x<=u}" 
8924  22 

15045  23 
greaterThan :: "('a::ord) => 'a set" ("(1{_<..})") 
24 
"{l<..} == {x. l<x}" 

8924  25 

11609
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset

26 
atLeast :: "('a::ord) => 'a set" ("(1{_..})") 
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset

27 
"{l..} == {x. l<=x}" 
8924  28 

15045  29 
greaterThanLessThan :: "['a::ord, 'a] => 'a set" ("(1{_<..<_})") 
30 
"{l<..<u} == {l<..} Int {..<u}" 

13735  31 

15045  32 
atLeastLessThan :: "['a::ord, 'a] => 'a set" ("(1{_..<_})") 
33 
"{l..<u} == {l..} Int {..<u}" 

13735  34 

15045  35 
greaterThanAtMost :: "['a::ord, 'a] => 'a set" ("(1{_<.._})") 
36 
"{l<..u} == {l<..} Int {..u}" 

13735  37 

38 
atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})") 

39 
"{l..u} == {l..} Int {..u}" 

40 

19376  41 
(* Old syntax, no longer supported: 
15045  42 
syntax 
43 
"_lessThan" :: "('a::ord) => 'a set" ("(1{.._'(})") 

44 
"_greaterThan" :: "('a::ord) => 'a set" ("(1{')_..})") 

45 
"_greaterThanLessThan" :: "['a::ord, 'a] => 'a set" ("(1{')_.._'(})") 

46 
"_atLeastLessThan" :: "['a::ord, 'a] => 'a set" ("(1{_.._'(})") 

47 
"_greaterThanAtMost" :: "['a::ord, 'a] => 'a set" ("(1{')_.._})") 

48 
translations 

49 
"{..m(}" => "{..<m}" 

50 
"{)m..}" => "{m<..}" 

51 
"{)m..n(}" => "{m<..<n}" 

52 
"{m..n(}" => "{m..<n}" 

53 
"{)m..n}" => "{m<..n}" 

19376  54 
*) 
15048  55 

56 
text{* A note of warning when using @{term"{..<n}"} on type @{typ 

57 
nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving 

15052  58 
@{term"{m..<n}"} may not exist in @{term"{..<n}"}form as well. *} 
15048  59 

14418  60 
syntax 
61 
"@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3UN _<=_./ _)" 10) 

62 
"@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3UN _<_./ _)" 10) 

63 
"@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3INT _<=_./ _)" 10) 

64 
"@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3INT _<_./ _)" 10) 

65 

66 
syntax (input) 

67 
"@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3\<Union> _\<le>_./ _)" 10) 

68 
"@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3\<Union> _<_./ _)" 10) 

69 
"@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3\<Inter> _\<le>_./ _)" 10) 

70 
"@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\<Inter> _<_./ _)" 10) 

71 

72 
syntax (xsymbols) 

14846  73 
"@UNION_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10) 
74 
"@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_ < _\<^esub>)/ _)" 10) 

75 
"@INTER_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10) 

76 
"@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_ < _\<^esub>)/ _)" 10) 

14418  77 

78 
translations 

79 
"UN i<=n. A" == "UN i:{..n}. A" 

15045  80 
"UN i<n. A" == "UN i:{..<n}. A" 
14418  81 
"INT i<=n. A" == "INT i:{..n}. A" 
15045  82 
"INT i<n. A" == "INT i:{..<n}. A" 
14418  83 

84 

14485  85 
subsection {* Various equivalences *} 
13735  86 

13850  87 
lemma lessThan_iff [iff]: "(i: lessThan k) = (i<k)" 
88 
by (simp add: lessThan_def) 

13735  89 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

90 
lemma Compl_lessThan [simp]: 
13735  91 
"!!k:: 'a::linorder. lessThan k = atLeast k" 
13850  92 
apply (auto simp add: lessThan_def atLeast_def) 
13735  93 
done 
94 

13850  95 
lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k}  lessThan k = {k}" 
96 
by auto 

13735  97 

13850  98 
lemma greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)" 
99 
by (simp add: greaterThan_def) 

13735  100 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

101 
lemma Compl_greaterThan [simp]: 
13735  102 
"!!k:: 'a::linorder. greaterThan k = atMost k" 
13850  103 
apply (simp add: greaterThan_def atMost_def le_def, auto) 
13735  104 
done 
105 

13850  106 
lemma Compl_atMost [simp]: "!!k:: 'a::linorder. atMost k = greaterThan k" 
107 
apply (subst Compl_greaterThan [symmetric]) 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

108 
apply (rule double_complement) 
13735  109 
done 
110 

13850  111 
lemma atLeast_iff [iff]: "(i: atLeast k) = (k<=i)" 
112 
by (simp add: atLeast_def) 

13735  113 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

114 
lemma Compl_atLeast [simp]: 
13735  115 
"!!k:: 'a::linorder. atLeast k = lessThan k" 
13850  116 
apply (simp add: lessThan_def atLeast_def le_def, auto) 
13735  117 
done 
118 

13850  119 
lemma atMost_iff [iff]: "(i: atMost k) = (i<=k)" 
120 
by (simp add: atMost_def) 

13735  121 

14485  122 
lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" 
123 
by (blast intro: order_antisym) 

13850  124 

125 

14485  126 
subsection {* Logical Equivalences for Set Inclusion and Equality *} 
13850  127 

128 
lemma atLeast_subset_iff [iff]: 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

129 
"(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

130 
by (blast intro: order_trans) 
13850  131 

132 
lemma atLeast_eq_iff [iff]: 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

133 
"(atLeast x = atLeast y) = (x = (y::'a::linorder))" 
13850  134 
by (blast intro: order_antisym order_trans) 
135 

136 
lemma greaterThan_subset_iff [iff]: 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

137 
"(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

138 
apply (auto simp add: greaterThan_def) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

139 
apply (subst linorder_not_less [symmetric], blast) 
13850  140 
done 
141 

142 
lemma greaterThan_eq_iff [iff]: 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

143 
"(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

144 
apply (rule iffI) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

145 
apply (erule equalityE) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

146 
apply (simp_all add: greaterThan_subset_iff) 
13850  147 
done 
148 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

149 
lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))" 
13850  150 
by (blast intro: order_trans) 
151 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

152 
lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" 
13850  153 
by (blast intro: order_antisym order_trans) 
154 

155 
lemma lessThan_subset_iff [iff]: 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

156 
"(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

157 
apply (auto simp add: lessThan_def) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

158 
apply (subst linorder_not_less [symmetric], blast) 
13850  159 
done 
160 

161 
lemma lessThan_eq_iff [iff]: 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

162 
"(lessThan x = lessThan y) = (x = (y::'a::linorder))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

163 
apply (rule iffI) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

164 
apply (erule equalityE) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

165 
apply (simp_all add: lessThan_subset_iff) 
13735  166 
done 
167 

168 

13850  169 
subsection {*Twosided intervals*} 
13735  170 

171 
lemma greaterThanLessThan_iff [simp]: 

15045  172 
"(i : {l<..<u}) = (l < i & i < u)" 
13735  173 
by (simp add: greaterThanLessThan_def) 
174 

175 
lemma atLeastLessThan_iff [simp]: 

15045  176 
"(i : {l..<u}) = (l <= i & i < u)" 
13735  177 
by (simp add: atLeastLessThan_def) 
178 

179 
lemma greaterThanAtMost_iff [simp]: 

15045  180 
"(i : {l<..u}) = (l < i & i <= u)" 
13735  181 
by (simp add: greaterThanAtMost_def) 
182 

183 
lemma atLeastAtMost_iff [simp]: 

184 
"(i : {l..u}) = (l <= i & i <= u)" 

185 
by (simp add: atLeastAtMost_def) 

186 

14577  187 
text {* The above four lemmas could be declared as iffs. 
188 
If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int} 

189 
seems to take forever (more than one hour). *} 

13735  190 

15554  191 
subsubsection{* Emptyness and singletons *} 
192 

193 
lemma atLeastAtMost_empty [simp]: "n < m ==> {m::'a::order..n} = {}"; 

194 
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def); 

195 

196 
lemma atLeastLessThan_empty[simp]: "n \<le> m ==> {m..<n::'a::order} = {}" 

197 
by (auto simp add: atLeastLessThan_def) 

198 

17719  199 
lemma greaterThanAtMost_empty[simp]:"l \<le> k ==> {k<..(l::'a::order)} = {}" 
200 
by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) 

201 

202 
lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..(l::'a::order)} = {}" 

203 
by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def) 

204 

15554  205 
lemma atLeastAtMost_singleton [simp]: "{a::'a::order..a} = {a}"; 
17719  206 
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def); 
14485  207 

208 
subsection {* Intervals of natural numbers *} 

209 

15047  210 
subsubsection {* The Constant @{term lessThan} *} 
211 

14485  212 
lemma lessThan_0 [simp]: "lessThan (0::nat) = {}" 
213 
by (simp add: lessThan_def) 

214 

215 
lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)" 

216 
by (simp add: lessThan_def less_Suc_eq, blast) 

217 

218 
lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k" 

219 
by (simp add: lessThan_def atMost_def less_Suc_eq_le) 

220 

221 
lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV" 

222 
by blast 

223 

15047  224 
subsubsection {* The Constant @{term greaterThan} *} 
225 

14485  226 
lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc" 
227 
apply (simp add: greaterThan_def) 

228 
apply (blast dest: gr0_conv_Suc [THEN iffD1]) 

229 
done 

230 

231 
lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k  {Suc k}" 

232 
apply (simp add: greaterThan_def) 

233 
apply (auto elim: linorder_neqE) 

234 
done 

235 

236 
lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}" 

237 
by blast 

238 

15047  239 
subsubsection {* The Constant @{term atLeast} *} 
240 

14485  241 
lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV" 
242 
by (unfold atLeast_def UNIV_def, simp) 

243 

244 
lemma atLeast_Suc: "atLeast (Suc k) = atLeast k  {k}" 

245 
apply (simp add: atLeast_def) 

246 
apply (simp add: Suc_le_eq) 

247 
apply (simp add: order_le_less, blast) 

248 
done 

249 

250 
lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k" 

251 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

252 

253 
lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV" 

254 
by blast 

255 

15047  256 
subsubsection {* The Constant @{term atMost} *} 
257 

14485  258 
lemma atMost_0 [simp]: "atMost (0::nat) = {0}" 
259 
by (simp add: atMost_def) 

260 

261 
lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)" 

262 
apply (simp add: atMost_def) 

263 
apply (simp add: less_Suc_eq order_le_less, blast) 

264 
done 

265 

266 
lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV" 

267 
by blast 

268 

15047  269 
subsubsection {* The Constant @{term atLeastLessThan} *} 
270 

271 
text{*But not a simprule because some concepts are better left in terms 

272 
of @{term atLeastLessThan}*} 

273 
lemma atLeast0LessThan: "{0::nat..<n} = {..<n}" 

15042  274 
by(simp add:lessThan_def atLeastLessThan_def) 
16041  275 
(* 
15047  276 
lemma atLeastLessThan0 [simp]: "{m..<0::nat} = {}" 
277 
by (simp add: atLeastLessThan_def) 

16041  278 
*) 
15047  279 
subsubsection {* Intervals of nats with @{term Suc} *} 
280 

281 
text{*Not a simprule because the RHS is too messy.*} 

282 
lemma atLeastLessThanSuc: 

283 
"{m..<Suc n} = (if m \<le> n then insert n {m..<n} else {})" 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

284 
by (auto simp add: atLeastLessThan_def) 
15047  285 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

286 
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 
15047  287 
by (auto simp add: atLeastLessThan_def) 
16041  288 
(* 
15047  289 
lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}" 
290 
by (induct k, simp_all add: atLeastLessThanSuc) 

291 

292 
lemma atLeastSucLessThan [simp]: "{Suc n..<n} = {}" 

293 
by (auto simp add: atLeastLessThan_def) 

16041  294 
*) 
15045  295 
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" 
14485  296 
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) 
297 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

298 
lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

299 
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
14485  300 
greaterThanAtMost_def) 
301 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

302 
lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

303 
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
14485  304 
greaterThanLessThan_def) 
305 

15554  306 
lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}" 
307 
by (auto simp add: atLeastAtMost_def) 

308 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

309 
subsubsection {* Image *} 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

310 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

311 
lemma image_add_atLeastAtMost: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

312 
"(%n::nat. n+k) ` {i..j} = {i+k..j+k}" (is "?A = ?B") 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

313 
proof 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

314 
show "?A \<subseteq> ?B" by auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

315 
next 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

316 
show "?B \<subseteq> ?A" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

317 
proof 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

318 
fix n assume a: "n : ?B" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

319 
hence "n  k : {i..j}" by auto arith+ 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

320 
moreover have "n = (n  k) + k" using a by auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

321 
ultimately show "n : ?A" by blast 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

322 
qed 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

323 
qed 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

324 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

325 
lemma image_add_atLeastLessThan: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

326 
"(%n::nat. n+k) ` {i..<j} = {i+k..<j+k}" (is "?A = ?B") 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

327 
proof 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

328 
show "?A \<subseteq> ?B" by auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

329 
next 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

330 
show "?B \<subseteq> ?A" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

331 
proof 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

332 
fix n assume a: "n : ?B" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

333 
hence "n  k : {i..<j}" by auto arith+ 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

334 
moreover have "n = (n  k) + k" using a by auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

335 
ultimately show "n : ?A" by blast 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

336 
qed 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

337 
qed 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

338 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

339 
corollary image_Suc_atLeastAtMost[simp]: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

340 
"Suc ` {i..j} = {Suc i..Suc j}" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

341 
using image_add_atLeastAtMost[where k=1] by simp 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

342 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

343 
corollary image_Suc_atLeastLessThan[simp]: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

344 
"Suc ` {i..<j} = {Suc i..<Suc j}" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

345 
using image_add_atLeastLessThan[where k=1] by simp 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

346 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

347 
lemma image_add_int_atLeastLessThan: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

348 
"(%x. x + (l::int)) ` {0..<ul} = {l..<u}" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

349 
apply (auto simp add: image_def) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

350 
apply (rule_tac x = "x  l" in bexI) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

351 
apply auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

352 
done 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

353 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

354 

14485  355 
subsubsection {* Finiteness *} 
356 

15045  357 
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}" 
14485  358 
by (induct k) (simp_all add: lessThan_Suc) 
359 

360 
lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}" 

361 
by (induct k) (simp_all add: atMost_Suc) 

362 

363 
lemma finite_greaterThanLessThan [iff]: 

15045  364 
fixes l :: nat shows "finite {l<..<u}" 
14485  365 
by (simp add: greaterThanLessThan_def) 
366 

367 
lemma finite_atLeastLessThan [iff]: 

15045  368 
fixes l :: nat shows "finite {l..<u}" 
14485  369 
by (simp add: atLeastLessThan_def) 
370 

371 
lemma finite_greaterThanAtMost [iff]: 

15045  372 
fixes l :: nat shows "finite {l<..u}" 
14485  373 
by (simp add: greaterThanAtMost_def) 
374 

375 
lemma finite_atLeastAtMost [iff]: 

376 
fixes l :: nat shows "finite {l..u}" 

377 
by (simp add: atLeastAtMost_def) 

378 

379 
lemma bounded_nat_set_is_finite: 

380 
"(ALL i:N. i < (n::nat)) ==> finite N" 

381 
 {* A bounded set of natural numbers is finite. *} 

382 
apply (rule finite_subset) 

383 
apply (rule_tac [2] finite_lessThan, auto) 

384 
done 

385 

386 
subsubsection {* Cardinality *} 

387 

15045  388 
lemma card_lessThan [simp]: "card {..<u} = u" 
15251  389 
by (induct u, simp_all add: lessThan_Suc) 
14485  390 

391 
lemma card_atMost [simp]: "card {..u} = Suc u" 

392 
by (simp add: lessThan_Suc_atMost [THEN sym]) 

393 

15045  394 
lemma card_atLeastLessThan [simp]: "card {l..<u} = u  l" 
395 
apply (subgoal_tac "card {l..<u} = card {..<ul}") 

14485  396 
apply (erule ssubst, rule card_lessThan) 
15045  397 
apply (subgoal_tac "(%x. x + l) ` {..<ul} = {l..<u}") 
14485  398 
apply (erule subst) 
399 
apply (rule card_image) 

400 
apply (simp add: inj_on_def) 

401 
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) 

402 
apply arith 

403 
apply (rule_tac x = "x  l" in exI) 

404 
apply arith 

405 
done 

406 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

407 
lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u  l" 
14485  408 
by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp) 
409 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

410 
lemma card_greaterThanAtMost [simp]: "card {l<..u} = u  l" 
14485  411 
by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp) 
412 

15045  413 
lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u  Suc l" 
14485  414 
by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp) 
415 

416 
subsection {* Intervals of integers *} 

417 

15045  418 
lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}" 
14485  419 
by (auto simp add: atLeastAtMost_def atLeastLessThan_def) 
420 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

421 
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" 
14485  422 
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 
423 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

424 
lemma atLeastPlusOneLessThan_greaterThanLessThan_int: 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

425 
"{l+1..<u} = {l<..<u::int}" 
14485  426 
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 
427 

428 
subsubsection {* Finiteness *} 

429 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

430 
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
15045  431 
{(0::int)..<u} = int ` {..<nat u}" 
14485  432 
apply (unfold image_def lessThan_def) 
433 
apply auto 

434 
apply (rule_tac x = "nat x" in exI) 

435 
apply (auto simp add: zless_nat_conj zless_nat_eq_int_zless [THEN sym]) 

436 
done 

437 

15045  438 
lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}" 
14485  439 
apply (case_tac "0 \<le> u") 
440 
apply (subst image_atLeastZeroLessThan_int, assumption) 

441 
apply (rule finite_imageI) 

442 
apply auto 

443 
done 

444 

15045  445 
lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}" 
446 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 

14485  447 
apply (erule subst) 
448 
apply (rule finite_imageI) 

449 
apply (rule finite_atLeastZeroLessThan_int) 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

450 
apply (rule image_add_int_atLeastLessThan) 
14485  451 
done 
452 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

453 
lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}" 
14485  454 
by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp) 
455 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

456 
lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}" 
14485  457 
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) 
458 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

459 
lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}" 
14485  460 
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) 
461 

462 
subsubsection {* Cardinality *} 

463 

15045  464 
lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u" 
14485  465 
apply (case_tac "0 \<le> u") 
466 
apply (subst image_atLeastZeroLessThan_int, assumption) 

467 
apply (subst card_image) 

468 
apply (auto simp add: inj_on_def) 

469 
done 

470 

15045  471 
lemma card_atLeastLessThan_int [simp]: "card {l..<u} = nat (u  l)" 
472 
apply (subgoal_tac "card {l..<u} = card {0..<ul}") 

14485  473 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 
15045  474 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 
14485  475 
apply (erule subst) 
476 
apply (rule card_image) 

477 
apply (simp add: inj_on_def) 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

478 
apply (rule image_add_int_atLeastLessThan) 
14485  479 
done 
480 

481 
lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u  l + 1)" 

482 
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 

483 
apply (auto simp add: compare_rls) 

484 
done 

485 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

486 
lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u  l)" 
14485  487 
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) 
488 

15045  489 
lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u  (l + 1))" 
14485  490 
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) 
491 

492 

13850  493 
subsection {*Lemmas useful with the summation operator setsum*} 
494 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16052
diff
changeset

495 
text {* For examples, see Algebra/poly/UnivPoly2.thy *} 
13735  496 

14577  497 
subsubsection {* Disjoint Unions *} 
13735  498 

14577  499 
text {* Singletons and open intervals *} 
13735  500 

501 
lemma ivl_disj_un_singleton: 

15045  502 
"{l::'a::linorder} Un {l<..} = {l..}" 
503 
"{..<u} Un {u::'a::linorder} = {..u}" 

504 
"(l::'a::linorder) < u ==> {l} Un {l<..<u} = {l..<u}" 

505 
"(l::'a::linorder) < u ==> {l<..<u} Un {u} = {l<..u}" 

506 
"(l::'a::linorder) <= u ==> {l} Un {l<..u} = {l..u}" 

507 
"(l::'a::linorder) <= u ==> {l..<u} Un {u} = {l..u}" 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

508 
by auto 
13735  509 

14577  510 
text {* One and twosided intervals *} 
13735  511 

512 
lemma ivl_disj_un_one: 

15045  513 
"(l::'a::linorder) < u ==> {..l} Un {l<..<u} = {..<u}" 
514 
"(l::'a::linorder) <= u ==> {..<l} Un {l..<u} = {..<u}" 

515 
"(l::'a::linorder) <= u ==> {..l} Un {l<..u} = {..u}" 

516 
"(l::'a::linorder) <= u ==> {..<l} Un {l..u} = {..u}" 

517 
"(l::'a::linorder) <= u ==> {l<..u} Un {u<..} = {l<..}" 

518 
"(l::'a::linorder) < u ==> {l<..<u} Un {u..} = {l<..}" 

519 
"(l::'a::linorder) <= u ==> {l..u} Un {u<..} = {l..}" 

520 
"(l::'a::linorder) <= u ==> {l..<u} Un {u..} = {l..}" 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

521 
by auto 
13735  522 

14577  523 
text {* Two and twosided intervals *} 
13735  524 

525 
lemma ivl_disj_un_two: 

15045  526 
"[ (l::'a::linorder) < m; m <= u ] ==> {l<..<m} Un {m..<u} = {l<..<u}" 
527 
"[ (l::'a::linorder) <= m; m < u ] ==> {l<..m} Un {m<..<u} = {l<..<u}" 

528 
"[ (l::'a::linorder) <= m; m <= u ] ==> {l..<m} Un {m..<u} = {l..<u}" 

529 
"[ (l::'a::linorder) <= m; m < u ] ==> {l..m} Un {m<..<u} = {l..<u}" 

530 
"[ (l::'a::linorder) < m; m <= u ] ==> {l<..<m} Un {m..u} = {l<..u}" 

531 
"[ (l::'a::linorder) <= m; m <= u ] ==> {l<..m} Un {m<..u} = {l<..u}" 

532 
"[ (l::'a::linorder) <= m; m <= u ] ==> {l..<m} Un {m..u} = {l..u}" 

533 
"[ (l::'a::linorder) <= m; m <= u ] ==> {l..m} Un {m<..u} = {l..u}" 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

534 
by auto 
13735  535 

536 
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two 

537 

14577  538 
subsubsection {* Disjoint Intersections *} 
13735  539 

14577  540 
text {* Singletons and open intervals *} 
13735  541 

542 
lemma ivl_disj_int_singleton: 

15045  543 
"{l::'a::order} Int {l<..} = {}" 
544 
"{..<u} Int {u} = {}" 

545 
"{l} Int {l<..<u} = {}" 

546 
"{l<..<u} Int {u} = {}" 

547 
"{l} Int {l<..u} = {}" 

548 
"{l..<u} Int {u} = {}" 

13735  549 
by simp+ 
550 

14577  551 
text {* One and twosided intervals *} 
13735  552 

553 
lemma ivl_disj_int_one: 

15045  554 
"{..l::'a::order} Int {l<..<u} = {}" 
555 
"{..<l} Int {l..<u} = {}" 

556 
"{..l} Int {l<..u} = {}" 

557 
"{..<l} Int {l..u} = {}" 

558 
"{l<..u} Int {u<..} = {}" 

559 
"{l<..<u} Int {u..} = {}" 

560 
"{l..u} Int {u<..} = {}" 

561 
"{l..<u} Int {u..} = {}" 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

562 
by auto 
13735  563 

14577  564 
text {* Two and twosided intervals *} 
13735  565 

566 
lemma ivl_disj_int_two: 

15045  567 
"{l::'a::order<..<m} Int {m..<u} = {}" 
568 
"{l<..m} Int {m<..<u} = {}" 

569 
"{l..<m} Int {m..<u} = {}" 

570 
"{l..m} Int {m<..<u} = {}" 

571 
"{l<..<m} Int {m..u} = {}" 

572 
"{l<..m} Int {m<..u} = {}" 

573 
"{l..<m} Int {m..u} = {}" 

574 
"{l..m} Int {m<..u} = {}" 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

575 
by auto 
13735  576 

577 
lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two 

578 

15542  579 
subsubsection {* Some Differences *} 
580 

581 
lemma ivl_diff[simp]: 

582 
"i \<le> n \<Longrightarrow> {i..<m}  {i..<n} = {n..<(m::'a::linorder)}" 

583 
by(auto) 

584 

585 

586 
subsubsection {* Some Subset Conditions *} 

587 

588 
lemma ivl_subset[simp]: 

589 
"({i..<j} \<subseteq> {m..<n}) = (j \<le> i  m \<le> i & j \<le> (n::'a::linorder))" 

590 
apply(auto simp:linorder_not_le) 

591 
apply(rule ccontr) 

592 
apply(insert linorder_le_less_linear[of i n]) 

593 
apply(clarsimp simp:linorder_not_le) 

594 
apply(fastsimp) 

595 
done 

596 

15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

597 

15042  598 
subsection {* Summation indexed over intervals *} 
599 

600 
syntax 

601 
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) 

15048  602 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) 
16052  603 
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10) 
604 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<=_./ _)" [0,0,10] 10) 

15042  605 
syntax (xsymbols) 
606 
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) 

15048  607 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) 
16052  608 
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) 
609 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10) 

15042  610 
syntax (HTML output) 
611 
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) 

15048  612 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) 
16052  613 
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) 
614 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10) 

15056  615 
syntax (latex_sum output) 
15052  616 
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
617 
("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) 

618 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 

619 
("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) 

16052  620 
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
621 
("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10) 

15052  622 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
16052  623 
("(3\<^raw:$\sum_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10) 
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

624 

15048  625 
translations 
626 
"\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}" 

627 
"\<Sum>x=a..<b. t" == "setsum (%x. t) {a..<b}" 

16052  628 
"\<Sum>i\<le>n. t" == "setsum (\<lambda>i. t) {..n}" 
15048  629 
"\<Sum>i<n. t" == "setsum (\<lambda>i. t) {..<n}" 
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

630 

15052  631 
text{* The above introduces some pretty alternative syntaxes for 
15056  632 
summation over intervals: 
15052  633 
\begin{center} 
634 
\begin{tabular}{lll} 

15056  635 
Old & New & \LaTeX\\ 
636 
@{term[source]"\<Sum>x\<in>{a..b}. e"} & @{term"\<Sum>x=a..b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..b. e"}\\ 

637 
@{term[source]"\<Sum>x\<in>{a..<b}. e"} & @{term"\<Sum>x=a..<b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..<b. e"}\\ 

16052  638 
@{term[source]"\<Sum>x\<in>{..b}. e"} & @{term"\<Sum>x\<le>b. e"} & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\ 
15056  639 
@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"} 
15052  640 
\end{tabular} 
641 
\end{center} 

15056  642 
The left column shows the term before introduction of the new syntax, 
643 
the middle column shows the new (default) syntax, and the right column 

644 
shows a special syntax. The latter is only meaningful for latex output 

645 
and has to be activated explicitly by setting the print mode to 

646 
\texttt{latex\_sum} (e.g.\ via \texttt{mode=latex\_sum} in 

647 
antiquotations). It is not the default \LaTeX\ output because it only 

648 
works well with italicstyle formulae, not ttstyle. 

15052  649 

650 
Note that for uniformity on @{typ nat} it is better to use 

651 
@{term"\<Sum>x::nat=0..<n. e"} rather than @{text"\<Sum>x<n. e"}: @{text setsum} may 

652 
not provide all lemmas available for @{term"{m..<n}"} also in the 

653 
special form for @{term"{..<n}"}. *} 

654 

15542  655 
text{* This congruence rule should be used for sums over intervals as 
656 
the standard theorem @{text[source]setsum_cong} does not work well 

657 
with the simplifier who adds the unsimplified premise @{term"x:B"} to 

658 
the context. *} 

659 

660 
lemma setsum_ivl_cong: 

661 
"\<lbrakk>a = c; b = d; !!x. \<lbrakk> c \<le> x; x < d \<rbrakk> \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> 

662 
setsum f {a..<b} = setsum g {c..<d}" 

663 
by(rule setsum_cong, simp_all) 

15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

664 

16041  665 
(* FIXME why are the following simp rules but the corresponding eqns 
666 
on intervals are not? *) 

667 

16052  668 
lemma setsum_atMost_Suc[simp]: "(\<Sum>i \<le> Suc n. f i) = (\<Sum>i \<le> n. f i) + f(Suc n)" 
669 
by (simp add:atMost_Suc add_ac) 

670 

16041  671 
lemma setsum_lessThan_Suc[simp]: "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n" 
672 
by (simp add:lessThan_Suc add_ac) 

15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

673 

15911  674 
lemma setsum_cl_ivl_Suc[simp]: 
15561  675 
"setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))" 
676 
by (auto simp:add_ac atLeastAtMostSuc_conv) 

677 

15911  678 
lemma setsum_op_ivl_Suc[simp]: 
15561  679 
"setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))" 
680 
by (auto simp:add_ac atLeastLessThanSuc) 

16041  681 
(* 
15561  682 
lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==> 
683 
(\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)" 

684 
by (auto simp:add_ac atLeastAtMostSuc_conv) 

16041  685 
*) 
15539  686 
lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> 
687 
setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}" 

688 
by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un) 

689 

690 
lemma setsum_diff_nat_ivl: 

691 
fixes f :: "nat \<Rightarrow> 'a::ab_group_add" 

692 
shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> 

693 
setsum f {m..<p}  setsum f {m..<n} = setsum f {n..<p}" 

694 
using setsum_add_nat_ivl [of m n p f,symmetric] 

695 
apply (simp add: add_ac) 

696 
done 

697 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

698 
subsection{* Shifting bounds *} 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

699 

15539  700 
lemma setsum_shift_bounds_nat_ivl: 
701 
"setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}" 

702 
by (induct "n", auto simp:atLeastLessThanSuc) 

703 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

704 
lemma setsum_shift_bounds_cl_nat_ivl: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

705 
"setsum f {m+k..n+k} = setsum (%i. f(i + k)){m..n::nat}" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

706 
apply (insert setsum_reindex[OF inj_on_add_nat, where h=f and B = "{m..n}"]) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

707 
apply (simp add:image_add_atLeastAtMost o_def) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

708 
done 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

709 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

710 
corollary setsum_shift_bounds_cl_Suc_ivl: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

711 
"setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

712 
by (simp add:setsum_shift_bounds_cl_nat_ivl[where k=1,simplified]) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

713 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

714 
corollary setsum_shift_bounds_Suc_ivl: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

715 
"setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

716 
by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified]) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

717 

19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

718 
lemma setsum_head: 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

719 
fixes n :: nat 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

720 
assumes mn: "m <= n" 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

721 
shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs") 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

722 
proof  
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

723 
from mn 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

724 
have "{m..n} = {m} \<union> {m<..n}" 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

725 
by (auto intro: ivl_disj_un_singleton) 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

726 
hence "?lhs = (\<Sum>x\<in>{m} \<union> {m<..n}. P x)" 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

727 
by (simp add: atLeast0LessThan) 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

728 
also have "\<dots> = ?rhs" by simp 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

729 
finally show ?thesis . 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

730 
qed 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

731 

6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

732 
lemma setsum_head_upt: 
19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

733 
fixes m::nat 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

734 
assumes m: "0 < m" 
19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

735 
shows "(\<Sum>x<m. P x) = P 0 + (\<Sum>x\<in>{1..<m}. P x)" 
19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

736 
proof  
19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

737 
have "(\<Sum>x<m. P x) = (\<Sum>x\<in>{0..<m}. P x)" 
19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

738 
by (simp add: atLeast0LessThan) 
19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

739 
also 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

740 
from m 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

741 
have "\<dots> = (\<Sum>x\<in>{0..m  1}. P x)" 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

742 
by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost) 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

743 
also 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

744 
have "\<dots> = P 0 + (\<Sum>x\<in>{0<..m  1}. P x)" 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

745 
by (simp add: setsum_head) 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

746 
also 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

747 
from m 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

748 
have "{0<..m  1} = {1..<m}" 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

749 
by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost) 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

750 
finally show ?thesis . 
19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

751 
qed 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

752 

17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

753 
subsection {* The formula for geometric sums *} 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

754 

e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

755 
lemma geometric_sum: 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

756 
"x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

757 
(x ^ n  1) / (x  1::'a::{field, recpower, division_by_zero})" 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

758 
apply (induct "n", auto) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

759 
apply (rule_tac c = "x  1" in field_mult_cancel_right_lemma) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

760 
apply (auto simp add: mult_assoc left_distrib) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

761 
apply (simp add: right_distrib diff_minus mult_commute power_Suc) 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

762 
done 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

763 

e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

764 

19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

765 
subsection {* The formula for arithmetic sums *} 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

766 

958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

767 
lemma gauss_sum: 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

768 
"((1::'a::comm_semiring_1_cancel) + 1)*(\<Sum>i\<in>{1..n}. of_nat i) = 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

769 
of_nat n*((of_nat n)+1)" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

770 
proof (induct n) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

771 
case 0 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

772 
show ?case by simp 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

773 
next 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

774 
case (Suc n) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

775 
then show ?case by (simp add: right_distrib add_assoc mult_ac) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

776 
qed 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

777 

958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

778 
theorem arith_series_general: 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

779 
"((1::'a::comm_semiring_1_cancel) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

780 
of_nat n * (a + (a + of_nat(n  1)*d))" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

781 
proof cases 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

782 
assume ngt1: "n > 1" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

783 
let ?I = "\<lambda>i. of_nat i" and ?n = "of_nat n" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

784 
have 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

785 
"(\<Sum>i\<in>{..<n}. a+?I i*d) = 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

786 
((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

787 
by (rule setsum_addf) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

788 
also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

789 
also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

790 
by (simp add: setsum_right_distrib setsum_head_upt mult_ac) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

791 
also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

792 
by (simp add: left_distrib right_distrib) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

793 
also from ngt1 have "{1..<n} = {1..n  1}" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

794 
by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

795 
also from ngt1 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

796 
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)" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

797 
by (simp only: mult_ac gauss_sum [of "n  1"]) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

798 
(simp add: mult_ac of_nat_Suc [symmetric]) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

799 
finally show ?thesis by (simp add: mult_ac add_ac right_distrib) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

800 
next 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

801 
assume "\<not>(n > 1)" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

802 
hence "n = 1 \<or> n = 0" by auto 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

803 
thus ?thesis by (auto simp: mult_ac right_distrib) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

804 
qed 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

805 

958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

806 
lemma arith_series_nat: 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

807 
"Suc (Suc 0) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n  1)*d))" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

808 
proof  
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

809 
have 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

810 
"((1::nat) + 1) * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) = 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

811 
of_nat(n) * (a + (a + of_nat(n  1)*d))" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

812 
by (rule arith_series_general) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

813 
thus ?thesis by (auto simp add: of_nat_id) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

814 
qed 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

815 

958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

816 
lemma arith_series_int: 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

817 
"(2::int) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

818 
of_nat n * (a + (a + of_nat(n  1)*d))" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

819 
proof  
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

820 
have 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

821 
"((1::int) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

822 
of_nat(n) * (a + (a + of_nat(n  1)*d))" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

823 
by (rule arith_series_general) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

824 
thus ?thesis by simp 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

825 
qed 
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

826 

19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

827 
lemma sum_diff_distrib: 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

828 
fixes P::"nat\<Rightarrow>nat" 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

829 
shows 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

830 
"\<forall>x. Q x \<le> P x \<Longrightarrow> 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

831 
(\<Sum>x<n. P x)  (\<Sum>x<n. Q x) = (\<Sum>x<n. P x  Q x)" 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

832 
proof (induct n) 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

833 
case 0 show ?case by simp 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

834 
next 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

835 
case (Suc n) 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

836 

0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

837 
let ?lhs = "(\<Sum>x<n. P x)  (\<Sum>x<n. Q x)" 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

838 
let ?rhs = "\<Sum>x<n. P x  Q x" 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

839 

0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

840 
from Suc have "?lhs = ?rhs" by simp 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

841 
moreover 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

842 
from Suc have "?lhs + P n  Q n = ?rhs + (P n  Q n)" by simp 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

843 
moreover 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

844 
from Suc have 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

845 
"(\<Sum>x<n. P x) + P n  ((\<Sum>x<n. Q x) + Q n) = ?rhs + (P n  Q n)" 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

846 
by (subst diff_diff_left[symmetric], 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

847 
subst diff_add_assoc2) 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

848 
(auto simp: diff_add_assoc2 intro: setsum_mono) 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

849 
ultimately 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

850 
show ?case by simp 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

851 
qed 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

852 

0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

853 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

854 
ML 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

855 
{* 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

856 
val Compl_atLeast = thm "Compl_atLeast"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

857 
val Compl_atMost = thm "Compl_atMost"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

858 
val Compl_greaterThan = thm "Compl_greaterThan"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

859 
val Compl_lessThan = thm "Compl_lessThan"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

860 
val INT_greaterThan_UNIV = thm "INT_greaterThan_UNIV"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

861 
val UN_atLeast_UNIV = thm "UN_atLeast_UNIV"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

862 
val UN_atMost_UNIV = thm "UN_atMost_UNIV"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

863 
val UN_lessThan_UNIV = thm "UN_lessThan_UNIV"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

864 
val atLeastAtMost_def = thm "atLeastAtMost_def"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

865 
val atLeastAtMost_iff = thm "atLeastAtMost_iff"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

866 
val atLeastLessThan_def = thm "atLeastLessThan_def"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

867 
val atLeastLessThan_iff = thm "atLeastLessThan_iff"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

868 
val atLeast_0 = thm "atLeast_0"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

869 
val atLeast_Suc = thm "atLeast_Suc"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

870 
val atLeast_def = thm "atLeast_def"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

871 
val atLeast_iff = thm "atLeast_iff"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

872 
val atMost_0 = thm "atMost_0"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

873 
val atMost_Int_atLeast = thm "atMost_Int_atLeast"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

874 
val atMost_Suc = thm "atMost_Suc"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

875 
val atMost_def = thm "atMost_def"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

876 
val atMost_iff = thm "atMost_iff"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

877 
val greaterThanAtMost_def = thm "greaterThanAtMost_def"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

878 
val greaterThanAtMost_iff = thm "greaterThanAtMost_iff"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

879 
val greaterThanLessThan_def = thm "greaterThanLessThan_def"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

880 
val greaterThanLessThan_iff = thm "greaterThanLessThan_iff"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

881 
val greaterThan_0 = thm "greaterThan_0"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

882 
val greaterThan_Suc = thm "greaterThan_Suc"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

883 
val greaterThan_def = thm "greaterThan_def"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

884 
val greaterThan_iff = thm "greaterThan_iff"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

885 
val ivl_disj_int = thms "ivl_disj_int"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

886 
val ivl_disj_int_one = thms "ivl_disj_int_one"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

887 
val ivl_disj_int_singleton = thms "ivl_disj_int_singleton"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

888 
val ivl_disj_int_two = thms "ivl_disj_int_two"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

889 
val ivl_disj_un = thms "ivl_disj_un"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

890 
val ivl_disj_un_one = thms "ivl_disj_un_one"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

891 
val ivl_disj_un_singleton = thms "ivl_disj_un_singleton"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

892 
val ivl_disj_un_two = thms "ivl_disj_un_two"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

893 
val lessThan_0 = thm "lessThan_0"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

894 
val lessThan_Suc = thm "lessThan_Suc"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

895 
val lessThan_Suc_atMost = thm "lessThan_Suc_atMost"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

896 
val lessThan_def = thm "lessThan_def"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

897 
val lessThan_iff = thm "lessThan_iff"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

898 
val single_Diff_lessThan = thm "single_Diff_lessThan"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

899 

e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

900 
val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

901 
val finite_atMost = thm "finite_atMost"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

902 
val finite_lessThan = thm "finite_lessThan"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

903 
*} 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

904 

8924  905 
end 