author | paulson |
Thu, 25 Mar 2004 10:32:21 +0100 | |
changeset 14485 | ea2707645af8 |
parent 14478 | bdf6b7adc3ec |
child 14577 | dbb95b825244 |
permissions | -rw-r--r-- |
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 two-sided 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 {*Two-sided 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 {..u-l(}") |
|
284 |
apply (erule ssubst, rule card_lessThan) |
|
285 |
apply (subgoal_tac "(%x. x + l) ` {..u-l(} = {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..u-l(} = {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..u-l(} = {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..u-l(}") |
|
371 |
apply (erule ssubst, rule card_atLeastZeroLessThan_int) |
|
372 |
apply (subgoal_tac "(%x. x + l) ` {0..u-l(} = {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, graph-based reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset
|
407 |
by auto |
13735 | 408 |
|
409 |
(* One- and two-sided 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, graph-based reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset
|
420 |
by auto |
13735 | 421 |
|
422 |
(* Two- and two-sided 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, graph-based 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 two-sided 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, graph-based reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset
|
461 |
by auto |
13735 | 462 |
|
463 |
(* Two- and two-sided 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, graph-based 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 |