author  paulson 
Thu, 25 Mar 2004 10:32:21 +0100  
changeset 14485  ea2707645af8 
parent 14478  bdf6b7adc3ec 
child 14577  dbb95b825244 
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 

14485  10 
theory SetInterval = IntArith: 
8924  11 

12 
constdefs 

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

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

14 
"{..u(} == {x. x<u}" 
8924  15 

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

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

17 
"{..u} == {x. x<=u}" 
8924  18 

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

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

20 
"{)l..} == {x. l<x}" 
8924  21 

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

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

23 
"{l..} == {x. l<=x}" 
8924  24 

13735  25 
greaterThanLessThan :: "['a::ord, 'a] => 'a set" ("(1{')_.._'(})") 
26 
"{)l..u(} == {)l..} Int {..u(}" 

27 

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

29 
"{l..u(} == {l..} Int {..u(}" 

30 

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

32 
"{)l..u} == {)l..} Int {..u}" 

33 

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

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

36 

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

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

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

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

42 

43 
syntax (input) 

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

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

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

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

48 

49 
syntax (xsymbols) 

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

51 
"@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>\<^bsub>_ < _\<^esub>/ _)" 10) 

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

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

54 

55 
translations 

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

57 
"UN i<n. A" == "UN i:{..n(}. A" 

58 
"INT i<=n. A" == "INT i:{..n}. A" 

59 
"INT i<n. A" == "INT i:{..n(}. A" 

60 

61 

14485  62 
subsection {* Various equivalences *} 
13735  63 

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

13735  66 

13850  67 
lemma Compl_lessThan [simp]: 
13735  68 
"!!k:: 'a::linorder. lessThan k = atLeast k" 
13850  69 
apply (auto simp add: lessThan_def atLeast_def) 
13735  70 
done 
71 

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

13735  74 

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

13735  77 

13850  78 
lemma Compl_greaterThan [simp]: 
13735  79 
"!!k:: 'a::linorder. greaterThan k = atMost k" 
13850  80 
apply (simp add: greaterThan_def atMost_def le_def, auto) 
13735  81 
done 
82 

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

85 
apply (rule double_complement) 

13735  86 
done 
87 

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

13735  90 

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

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

13735  98 

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

13850  101 

102 

14485  103 
subsection {* Logical Equivalences for Set Inclusion and Equality *} 
13850  104 

105 
lemma atLeast_subset_iff [iff]: 

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

107 
by (blast intro: order_trans) 

108 

109 
lemma atLeast_eq_iff [iff]: 

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

111 
by (blast intro: order_antisym order_trans) 

112 

113 
lemma greaterThan_subset_iff [iff]: 

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

115 
apply (auto simp add: greaterThan_def) 

116 
apply (subst linorder_not_less [symmetric], blast) 

117 
done 

118 

119 
lemma greaterThan_eq_iff [iff]: 

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

121 
apply (rule iffI) 

122 
apply (erule equalityE) 

123 
apply (simp add: greaterThan_subset_iff order_antisym, simp) 

124 
done 

125 

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

127 
by (blast intro: order_trans) 

128 

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

130 
by (blast intro: order_antisym order_trans) 

131 

132 
lemma lessThan_subset_iff [iff]: 

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

134 
apply (auto simp add: lessThan_def) 

135 
apply (subst linorder_not_less [symmetric], blast) 

136 
done 

137 

138 
lemma lessThan_eq_iff [iff]: 

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

140 
apply (rule iffI) 

141 
apply (erule equalityE) 

142 
apply (simp add: lessThan_subset_iff order_antisym, simp) 

13735  143 
done 
144 

145 

13850  146 
subsection {*Twosided intervals*} 
13735  147 

148 
(* greaterThanLessThan *) 

149 

150 
lemma greaterThanLessThan_iff [simp]: 

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

152 
by (simp add: greaterThanLessThan_def) 

153 

154 
(* atLeastLessThan *) 

155 

156 
lemma atLeastLessThan_iff [simp]: 

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

158 
by (simp add: atLeastLessThan_def) 

159 

160 
(* greaterThanAtMost *) 

161 

162 
lemma greaterThanAtMost_iff [simp]: 

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

164 
by (simp add: greaterThanAtMost_def) 

165 

166 
(* atLeastAtMost *) 

167 

168 
lemma atLeastAtMost_iff [simp]: 

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

170 
by (simp add: atLeastAtMost_def) 

171 

172 
(* The above four lemmas could be declared as iffs. 

173 
If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int 

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

175 

14485  176 

177 
subsection {* Intervals of natural numbers *} 

178 

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

180 
by (simp add: lessThan_def) 

181 

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

183 
by (simp add: lessThan_def less_Suc_eq, blast) 

184 

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

186 
by (simp add: lessThan_def atMost_def less_Suc_eq_le) 

187 

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

189 
by blast 

190 

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

192 
apply (simp add: greaterThan_def) 

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

194 
done 

195 

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

197 
apply (simp add: greaterThan_def) 

198 
apply (auto elim: linorder_neqE) 

199 
done 

200 

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

202 
by blast 

203 

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

205 
by (unfold atLeast_def UNIV_def, simp) 

206 

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

208 
apply (simp add: atLeast_def) 

209 
apply (simp add: Suc_le_eq) 

210 
apply (simp add: order_le_less, blast) 

211 
done 

212 

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

214 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

215 

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

217 
by blast 

218 

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

220 
by (simp add: atMost_def) 

221 

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

223 
apply (simp add: atMost_def) 

224 
apply (simp add: less_Suc_eq order_le_less, blast) 

225 
done 

226 

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

228 
by blast 

229 

230 
(* Intervals of nats with Suc *) 

231 

232 
lemma atLeastLessThanSuc_atLeastAtMost: "{l..Suc u(} = {l..u}" 

233 
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) 

234 

235 
lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {)l..u}" 

236 
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 

237 
greaterThanAtMost_def) 

238 

239 
lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..u(} = {)l..u(}" 

240 
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 

241 
greaterThanLessThan_def) 

242 

243 
subsubsection {* Finiteness *} 

244 

245 
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}" 

246 
by (induct k) (simp_all add: lessThan_Suc) 

247 

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

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

250 

251 
lemma finite_greaterThanLessThan [iff]: 

252 
fixes l :: nat shows "finite {)l..u(}" 

253 
by (simp add: greaterThanLessThan_def) 

254 

255 
lemma finite_atLeastLessThan [iff]: 

256 
fixes l :: nat shows "finite {l..u(}" 

257 
by (simp add: atLeastLessThan_def) 

258 

259 
lemma finite_greaterThanAtMost [iff]: 

260 
fixes l :: nat shows "finite {)l..u}" 

261 
by (simp add: greaterThanAtMost_def) 

262 

263 
lemma finite_atLeastAtMost [iff]: 

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

265 
by (simp add: atLeastAtMost_def) 

266 

267 
lemma bounded_nat_set_is_finite: 

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

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

270 
apply (rule finite_subset) 

271 
apply (rule_tac [2] finite_lessThan, auto) 

272 
done 

273 

274 
subsubsection {* Cardinality *} 

275 

276 
lemma card_lessThan [simp]: "card {..u(} = u" 

277 
by (induct_tac u, simp_all add: lessThan_Suc) 

278 

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

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

281 

282 
lemma card_atLeastLessThan [simp]: "card {l..u(} = u  l" 

283 
apply (subgoal_tac "card {l..u(} = card {..ul(}") 

284 
apply (erule ssubst, rule card_lessThan) 

285 
apply (subgoal_tac "(%x. x + l) ` {..ul(} = {l..u(}") 

286 
apply (erule subst) 

287 
apply (rule card_image) 

288 
apply (rule finite_lessThan) 

289 
apply (simp add: inj_on_def) 

290 
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) 

291 
apply arith 

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

293 
apply arith 

294 
done 

295 

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

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

298 

299 
lemma card_greaterThanAtMost [simp]: "card {)l..u} = u  l" 

300 
by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp) 

301 

302 
lemma card_greaterThanLessThan [simp]: "card {)l..u(} = u  Suc l" 

303 
by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp) 

304 

305 
subsection {* Intervals of integers *} 

306 

307 
lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..u+1(} = {l..(u::int)}" 

308 
by (auto simp add: atLeastAtMost_def atLeastLessThan_def) 

309 

310 
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {)l..(u::int)}" 

311 
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 

312 

313 
lemma atLeastPlusOneLessThan_greaterThanLessThan_int: 

314 
"{l+1..u(} = {)l..(u::int)(}" 

315 
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 

316 

317 
subsubsection {* Finiteness *} 

318 

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

320 
{(0::int)..u(} = int ` {..nat u(}" 

321 
apply (unfold image_def lessThan_def) 

322 
apply auto 

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

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

325 
done 

326 

327 
lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..u(}" 

328 
apply (case_tac "0 \<le> u") 

329 
apply (subst image_atLeastZeroLessThan_int, assumption) 

330 
apply (rule finite_imageI) 

331 
apply auto 

332 
apply (subgoal_tac "{0..u(} = {}") 

333 
apply auto 

334 
done 

335 

336 
lemma image_atLeastLessThan_int_shift: 

337 
"(%x. x + (l::int)) ` {0..ul(} = {l..u(}" 

338 
apply (auto simp add: image_def atLeastLessThan_iff) 

339 
apply (rule_tac x = "x  l" in bexI) 

340 
apply auto 

341 
done 

342 

343 
lemma finite_atLeastLessThan_int [iff]: "finite {l..(u::int)(}" 

344 
apply (subgoal_tac "(%x. x + l) ` {0..ul(} = {l..u(}") 

345 
apply (erule subst) 

346 
apply (rule finite_imageI) 

347 
apply (rule finite_atLeastZeroLessThan_int) 

348 
apply (rule image_atLeastLessThan_int_shift) 

349 
done 

350 

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

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

353 

354 
lemma finite_greaterThanAtMost_int [iff]: "finite {)l..(u::int)}" 

355 
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) 

356 

357 
lemma finite_greaterThanLessThan_int [iff]: "finite {)l..(u::int)(}" 

358 
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) 

359 

360 
subsubsection {* Cardinality *} 

361 

362 
lemma card_atLeastZeroLessThan_int: "card {(0::int)..u(} = nat u" 

363 
apply (case_tac "0 \<le> u") 

364 
apply (subst image_atLeastZeroLessThan_int, assumption) 

365 
apply (subst card_image) 

366 
apply (auto simp add: inj_on_def) 

367 
done 

368 

369 
lemma card_atLeastLessThan_int [simp]: "card {l..u(} = nat (u  l)" 

370 
apply (subgoal_tac "card {l..u(} = card {0..ul(}") 

371 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 

372 
apply (subgoal_tac "(%x. x + l) ` {0..ul(} = {l..u(}") 

373 
apply (erule subst) 

374 
apply (rule card_image) 

375 
apply (rule finite_atLeastZeroLessThan_int) 

376 
apply (simp add: inj_on_def) 

377 
apply (rule image_atLeastLessThan_int_shift) 

378 
done 

379 

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

381 
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 

382 
apply (auto simp add: compare_rls) 

383 
done 

384 

385 
lemma card_greaterThanAtMost_int [simp]: "card {)l..u} = nat (u  l)" 

386 
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) 

387 

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

389 
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) 

390 

391 

13850  392 
subsection {*Lemmas useful with the summation operator setsum*} 
393 

13735  394 
(* For examples, see Algebra/poly/UnivPoly.thy *) 
395 

396 
(** Disjoint Unions **) 

397 

398 
(* Singletons and open intervals *) 

399 

400 
lemma ivl_disj_un_singleton: 

401 
"{l::'a::linorder} Un {)l..} = {l..}" 

402 
"{..u(} Un {u::'a::linorder} = {..u}" 

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

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

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

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

407 
by auto 
13735  408 

409 
(* One and twosided intervals *) 

410 

411 
lemma ivl_disj_un_one: 

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

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

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

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

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

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

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

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

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

420 
by auto 
13735  421 

422 
(* Two and twosided intervals *) 

423 

424 
lemma ivl_disj_un_two: 

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

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

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

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

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

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

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

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

433 
by auto 
13735  434 

435 
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two 

436 

437 
(** Disjoint Intersections **) 

438 

439 
(* Singletons and open intervals *) 

440 

441 
lemma ivl_disj_int_singleton: 

442 
"{l::'a::order} Int {)l..} = {}" 

443 
"{..u(} Int {u} = {}" 

444 
"{l} Int {)l..u(} = {}" 

445 
"{)l..u(} Int {u} = {}" 

446 
"{l} Int {)l..u} = {}" 

447 
"{l..u(} Int {u} = {}" 

448 
by simp+ 

449 

450 
(* One and twosided intervals *) 

451 

452 
lemma ivl_disj_int_one: 

453 
"{..l::'a::order} Int {)l..u(} = {}" 

454 
"{..l(} Int {l..u(} = {}" 

455 
"{..l} Int {)l..u} = {}" 

456 
"{..l(} Int {l..u} = {}" 

457 
"{)l..u} Int {)u..} = {}" 

458 
"{)l..u(} Int {u..} = {}" 

459 
"{l..u} Int {)u..} = {}" 

460 
"{l..u(} Int {u..} = {}" 

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

461 
by auto 
13735  462 

463 
(* Two and twosided intervals *) 

464 

465 
lemma ivl_disj_int_two: 

466 
"{)l::'a::order..m(} Int {m..u(} = {}" 

467 
"{)l..m} Int {)m..u(} = {}" 

468 
"{l..m(} Int {m..u(} = {}" 

469 
"{l..m} Int {)m..u(} = {}" 

470 
"{)l..m(} Int {m..u} = {}" 

471 
"{)l..m} Int {)m..u} = {}" 

472 
"{l..m(} Int {m..u} = {}" 

473 
"{l..m} Int {)m..u} = {}" 

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

474 
by auto 
13735  475 

476 
lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two 

477 

8924  478 
end 