author  nipkow 
Thu, 15 Jul 2004 13:11:34 +0200  
changeset 15045  d59f7e2e18d3 
parent 15042  fa7d27ef7e59 
child 15047  fa62de5862b9 
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 

14485  12 
theory SetInterval = IntArith: 
8924  13 

14 
constdefs 

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

8924  17 

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

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

19 
"{..u} == {x. x<=u}" 
8924  20 

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

8924  23 

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

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

25 
"{l..} == {x. l<=x}" 
8924  26 

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

13735  29 

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

13735  32 

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

13735  35 

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

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

38 

15045  39 
(* Old syntax, will disappear! *) 
40 
syntax 

41 
"_lessThan" :: "('a::ord) => 'a set" ("(1{.._'(})") 

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

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

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

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

46 
translations 

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

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

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

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

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

52 

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

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

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

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

58 

59 
syntax (input) 

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

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

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

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

64 

65 
syntax (xsymbols) 

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

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

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

14418  70 

71 
translations 

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

15045  73 
"UN i<n. A" == "UN i:{..<n}. A" 
14418  74 
"INT i<=n. A" == "INT i:{..n}. A" 
15045  75 
"INT i<n. A" == "INT i:{..<n}. A" 
14418  76 

77 

14485  78 
subsection {* Various equivalences *} 
13735  79 

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

13735  82 

13850  83 
lemma Compl_lessThan [simp]: 
13735  84 
"!!k:: 'a::linorder. lessThan k = atLeast k" 
13850  85 
apply (auto simp add: lessThan_def atLeast_def) 
13735  86 
done 
87 

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

13735  90 

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

13735  93 

13850  94 
lemma Compl_greaterThan [simp]: 
13735  95 
"!!k:: 'a::linorder. greaterThan k = atMost k" 
13850  96 
apply (simp add: greaterThan_def atMost_def le_def, auto) 
13735  97 
done 
98 

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

101 
apply (rule double_complement) 

13735  102 
done 
103 

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

13735  106 

13850  107 
lemma Compl_atLeast [simp]: 
13735  108 
"!!k:: 'a::linorder. atLeast k = lessThan k" 
13850  109 
apply (simp add: lessThan_def atLeast_def le_def, auto) 
13735  110 
done 
111 

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

13735  114 

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

13850  117 

118 

14485  119 
subsection {* Logical Equivalences for Set Inclusion and Equality *} 
13850  120 

121 
lemma atLeast_subset_iff [iff]: 

122 
"(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))" 

123 
by (blast intro: order_trans) 

124 

125 
lemma atLeast_eq_iff [iff]: 

126 
"(atLeast x = atLeast y) = (x = (y::'a::linorder))" 

127 
by (blast intro: order_antisym order_trans) 

128 

129 
lemma greaterThan_subset_iff [iff]: 

130 
"(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))" 

131 
apply (auto simp add: greaterThan_def) 

132 
apply (subst linorder_not_less [symmetric], blast) 

133 
done 

134 

135 
lemma greaterThan_eq_iff [iff]: 

136 
"(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" 

137 
apply (rule iffI) 

138 
apply (erule equalityE) 

139 
apply (simp add: greaterThan_subset_iff order_antisym, simp) 

140 
done 

141 

142 
lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))" 

143 
by (blast intro: order_trans) 

144 

145 
lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" 

146 
by (blast intro: order_antisym order_trans) 

147 

148 
lemma lessThan_subset_iff [iff]: 

149 
"(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))" 

150 
apply (auto simp add: lessThan_def) 

151 
apply (subst linorder_not_less [symmetric], blast) 

152 
done 

153 

154 
lemma lessThan_eq_iff [iff]: 

155 
"(lessThan x = lessThan y) = (x = (y::'a::linorder))" 

156 
apply (rule iffI) 

157 
apply (erule equalityE) 

158 
apply (simp add: lessThan_subset_iff order_antisym, simp) 

13735  159 
done 
160 

161 

13850  162 
subsection {*Twosided intervals*} 
13735  163 

14577  164 
text {* @{text greaterThanLessThan} *} 
13735  165 

166 
lemma greaterThanLessThan_iff [simp]: 

15045  167 
"(i : {l<..<u}) = (l < i & i < u)" 
13735  168 
by (simp add: greaterThanLessThan_def) 
169 

14577  170 
text {* @{text atLeastLessThan} *} 
13735  171 

172 
lemma atLeastLessThan_iff [simp]: 

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

14577  176 
text {* @{text greaterThanAtMost} *} 
13735  177 

178 
lemma greaterThanAtMost_iff [simp]: 

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

14577  182 
text {* @{text atLeastAtMost} *} 
13735  183 

184 
lemma atLeastAtMost_iff [simp]: 

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

186 
by (simp add: atLeastAtMost_def) 

187 

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

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

13735  191 

14485  192 

193 
subsection {* Intervals of natural numbers *} 

194 

195 
lemma lessThan_0 [simp]: "lessThan (0::nat) = {}" 

196 
by (simp add: lessThan_def) 

197 

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

199 
by (simp add: lessThan_def less_Suc_eq, blast) 

200 

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

202 
by (simp add: lessThan_def atMost_def less_Suc_eq_le) 

203 

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

205 
by blast 

206 

207 
lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc" 

208 
apply (simp add: greaterThan_def) 

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

210 
done 

211 

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

213 
apply (simp add: greaterThan_def) 

214 
apply (auto elim: linorder_neqE) 

215 
done 

216 

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

218 
by blast 

219 

220 
lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV" 

221 
by (unfold atLeast_def UNIV_def, simp) 

222 

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

224 
apply (simp add: atLeast_def) 

225 
apply (simp add: Suc_le_eq) 

226 
apply (simp add: order_le_less, blast) 

227 
done 

228 

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

230 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

231 

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

233 
by blast 

234 

235 
lemma atMost_0 [simp]: "atMost (0::nat) = {0}" 

236 
by (simp add: atMost_def) 

237 

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

239 
apply (simp add: atMost_def) 

240 
apply (simp add: less_Suc_eq order_le_less, blast) 

241 
done 

242 

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

244 
by blast 

245 

15045  246 
lemma atLeast0LessThan [simp]: "{0::nat..<n} = {..<n}" 
15042  247 
by(simp add:lessThan_def atLeastLessThan_def) 
248 

14577  249 
text {* Intervals of nats with @{text Suc} *} 
14485  250 

15045  251 
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" 
14485  252 
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) 
253 

15045  254 
lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}" 
14485  255 
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
256 
greaterThanAtMost_def) 

257 

15045  258 
lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}" 
14485  259 
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
260 
greaterThanLessThan_def) 

261 

262 
subsubsection {* Finiteness *} 

263 

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

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

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

269 

270 
lemma finite_greaterThanLessThan [iff]: 

15045  271 
fixes l :: nat shows "finite {l<..<u}" 
14485  272 
by (simp add: greaterThanLessThan_def) 
273 

274 
lemma finite_atLeastLessThan [iff]: 

15045  275 
fixes l :: nat shows "finite {l..<u}" 
14485  276 
by (simp add: atLeastLessThan_def) 
277 

278 
lemma finite_greaterThanAtMost [iff]: 

15045  279 
fixes l :: nat shows "finite {l<..u}" 
14485  280 
by (simp add: greaterThanAtMost_def) 
281 

282 
lemma finite_atLeastAtMost [iff]: 

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

284 
by (simp add: atLeastAtMost_def) 

285 

286 
lemma bounded_nat_set_is_finite: 

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

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

289 
apply (rule finite_subset) 

290 
apply (rule_tac [2] finite_lessThan, auto) 

291 
done 

292 

293 
subsubsection {* Cardinality *} 

294 

15045  295 
lemma card_lessThan [simp]: "card {..<u} = u" 
14485  296 
by (induct_tac u, simp_all add: lessThan_Suc) 
297 

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

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

300 

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

14485  303 
apply (erule ssubst, rule card_lessThan) 
15045  304 
apply (subgoal_tac "(%x. x + l) ` {..<ul} = {l..<u}") 
14485  305 
apply (erule subst) 
306 
apply (rule card_image) 

307 
apply (rule finite_lessThan) 

308 
apply (simp add: inj_on_def) 

309 
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) 

310 
apply arith 

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

312 
apply arith 

313 
done 

314 

315 
lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u  l" 

316 
by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp) 

317 

15045  318 
lemma card_greaterThanAtMost [simp]: "card {l<..u} = u  l" 
14485  319 
by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp) 
320 

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

324 
subsection {* Intervals of integers *} 

325 

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

15045  329 
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" 
14485  330 
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 
331 

332 
lemma atLeastPlusOneLessThan_greaterThanLessThan_int: 

15045  333 
"{l+1..<u} = {l<..<u::int}" 
14485  334 
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 
335 

336 
subsubsection {* Finiteness *} 

337 

338 
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 

15045  339 
{(0::int)..<u} = int ` {..<nat u}" 
14485  340 
apply (unfold image_def lessThan_def) 
341 
apply auto 

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

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

344 
done 

345 

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

349 
apply (rule finite_imageI) 

350 
apply auto 

15045  351 
apply (subgoal_tac "{0..<u} = {}") 
14485  352 
apply auto 
353 
done 

354 

355 
lemma image_atLeastLessThan_int_shift: 

15045  356 
"(%x. x + (l::int)) ` {0..<ul} = {l..<u}" 
14485  357 
apply (auto simp add: image_def atLeastLessThan_iff) 
358 
apply (rule_tac x = "x  l" in bexI) 

359 
apply auto 

360 
done 

361 

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

14485  364 
apply (erule subst) 
365 
apply (rule finite_imageI) 

366 
apply (rule finite_atLeastZeroLessThan_int) 

367 
apply (rule image_atLeastLessThan_int_shift) 

368 
done 

369 

370 
lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}" 

371 
by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp) 

372 

15045  373 
lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}" 
14485  374 
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) 
375 

15045  376 
lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}" 
14485  377 
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) 
378 

379 
subsubsection {* Cardinality *} 

380 

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

384 
apply (subst card_image) 

385 
apply (auto simp add: inj_on_def) 

386 
done 

387 

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

14485  390 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 
15045  391 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 
14485  392 
apply (erule subst) 
393 
apply (rule card_image) 

394 
apply (rule finite_atLeastZeroLessThan_int) 

395 
apply (simp add: inj_on_def) 

396 
apply (rule image_atLeastLessThan_int_shift) 

397 
done 

398 

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

400 
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 

401 
apply (auto simp add: compare_rls) 

402 
done 

403 

15045  404 
lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u  l)" 
14485  405 
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) 
406 

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

410 

13850  411 
subsection {*Lemmas useful with the summation operator setsum*} 
412 

14577  413 
text {* For examples, see Algebra/poly/UnivPoly.thy *} 
13735  414 

14577  415 
subsubsection {* Disjoint Unions *} 
13735  416 

14577  417 
text {* Singletons and open intervals *} 
13735  418 

419 
lemma ivl_disj_un_singleton: 

15045  420 
"{l::'a::linorder} Un {l<..} = {l..}" 
421 
"{..<u} Un {u::'a::linorder} = {..u}" 

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

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

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

425 
"(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

426 
by auto 
13735  427 

14577  428 
text {* One and twosided intervals *} 
13735  429 

430 
lemma ivl_disj_un_one: 

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

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

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

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

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

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

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

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

439 
by auto 
13735  440 

14577  441 
text {* Two and twosided intervals *} 
13735  442 

443 
lemma ivl_disj_un_two: 

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

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

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

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

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

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

451 
"[ (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

452 
by auto 
13735  453 

454 
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two 

455 

14577  456 
subsubsection {* Disjoint Intersections *} 
13735  457 

14577  458 
text {* Singletons and open intervals *} 
13735  459 

460 
lemma ivl_disj_int_singleton: 

15045  461 
"{l::'a::order} Int {l<..} = {}" 
462 
"{..<u} Int {u} = {}" 

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

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

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

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

13735  467 
by simp+ 
468 

14577  469 
text {* One and twosided intervals *} 
13735  470 

471 
lemma ivl_disj_int_one: 

15045  472 
"{..l::'a::order} Int {l<..<u} = {}" 
473 
"{..<l} Int {l..<u} = {}" 

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

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

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

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

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

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

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

480 
by auto 
13735  481 

14577  482 
text {* Two and twosided intervals *} 
13735  483 

484 
lemma ivl_disj_int_two: 

15045  485 
"{l::'a::order<..<m} Int {m..<u} = {}" 
486 
"{l<..m} Int {m<..<u} = {}" 

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

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

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

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

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

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

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

493 
by auto 
13735  494 

495 
lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two 

496 

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

497 

15042  498 
subsection {* Summation indexed over intervals *} 
499 

500 
text{* We introduce the obvious syntax @{text"\<Sum>x=a..b. e"} for 

501 
@{term"\<Sum>x\<in>{a..b}. e"}. *} 

502 

503 
syntax 

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

505 
syntax (xsymbols) 

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

507 
syntax (HTML output) 

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

509 

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

511 

512 

513 
subsection {* Summation up to *} 

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

514 

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

515 
text{* Legacy, only used in HoareParallel and IsarExamples. Really 
15042  516 
needed? Probably better to replace it with above syntax. *} 
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

517 

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

518 
syntax 
15042  519 
"_Summation" :: "idt => 'a => 'b => 'b" ("\<Sum>_<_. _" [0, 51, 10] 10) 
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

520 
translations 
15045  521 
"\<Sum>i < n. b" == "setsum (\<lambda>i. b) {..<n}" 
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

522 

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

523 
lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)" 
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

524 
by (simp add:lessThan_Suc) 
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

525 

8924  526 
end 