author | paulson |
Fri, 29 Oct 2004 15:16:02 +0200 | |
changeset 15270 | 8b3f707a78a7 |
parent 15251 | bb6f072c8d10 |
child 15402 | 97204f3b4705 |
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 |
||
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 |
||
15045 | 41 |
(* Old syntax, will disappear! *) |
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}" |
|
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 |
|
13850 | 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 |
|
13850 | 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]) |
|
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 |
|
13850 | 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]: |
|
129 |
"(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))" |
|
130 |
by (blast intro: order_trans) |
|
131 |
||
132 |
lemma atLeast_eq_iff [iff]: |
|
133 |
"(atLeast x = atLeast y) = (x = (y::'a::linorder))" |
|
134 |
by (blast intro: order_antisym order_trans) |
|
135 |
||
136 |
lemma greaterThan_subset_iff [iff]: |
|
137 |
"(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))" |
|
138 |
apply (auto simp add: greaterThan_def) |
|
139 |
apply (subst linorder_not_less [symmetric], blast) |
|
140 |
done |
|
141 |
||
142 |
lemma greaterThan_eq_iff [iff]: |
|
143 |
"(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" |
|
144 |
apply (rule iffI) |
|
145 |
apply (erule equalityE) |
|
146 |
apply (simp add: greaterThan_subset_iff order_antisym, simp) |
|
147 |
done |
|
148 |
||
149 |
lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))" |
|
150 |
by (blast intro: order_trans) |
|
151 |
||
152 |
lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" |
|
153 |
by (blast intro: order_antisym order_trans) |
|
154 |
||
155 |
lemma lessThan_subset_iff [iff]: |
|
156 |
"(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))" |
|
157 |
apply (auto simp add: lessThan_def) |
|
158 |
apply (subst linorder_not_less [symmetric], blast) |
|
159 |
done |
|
160 |
||
161 |
lemma lessThan_eq_iff [iff]: |
|
162 |
"(lessThan x = lessThan y) = (x = (y::'a::linorder))" |
|
163 |
apply (rule iffI) |
|
164 |
apply (erule equalityE) |
|
165 |
apply (simp add: lessThan_subset_iff order_antisym, simp) |
|
13735 | 166 |
done |
167 |
||
168 |
||
13850 | 169 |
subsection {*Two-sided intervals*} |
13735 | 170 |
|
14577 | 171 |
text {* @{text greaterThanLessThan} *} |
13735 | 172 |
|
173 |
lemma greaterThanLessThan_iff [simp]: |
|
15045 | 174 |
"(i : {l<..<u}) = (l < i & i < u)" |
13735 | 175 |
by (simp add: greaterThanLessThan_def) |
176 |
||
14577 | 177 |
text {* @{text atLeastLessThan} *} |
13735 | 178 |
|
179 |
lemma atLeastLessThan_iff [simp]: |
|
15045 | 180 |
"(i : {l..<u}) = (l <= i & i < u)" |
13735 | 181 |
by (simp add: atLeastLessThan_def) |
182 |
||
14577 | 183 |
text {* @{text greaterThanAtMost} *} |
13735 | 184 |
|
185 |
lemma greaterThanAtMost_iff [simp]: |
|
15045 | 186 |
"(i : {l<..u}) = (l < i & i <= u)" |
13735 | 187 |
by (simp add: greaterThanAtMost_def) |
188 |
||
14577 | 189 |
text {* @{text atLeastAtMost} *} |
13735 | 190 |
|
191 |
lemma atLeastAtMost_iff [simp]: |
|
192 |
"(i : {l..u}) = (l <= i & i <= u)" |
|
193 |
by (simp add: atLeastAtMost_def) |
|
194 |
||
14577 | 195 |
text {* The above four lemmas could be declared as iffs. |
196 |
If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int} |
|
197 |
seems to take forever (more than one hour). *} |
|
13735 | 198 |
|
14485 | 199 |
|
200 |
subsection {* Intervals of natural numbers *} |
|
201 |
||
15047 | 202 |
subsubsection {* The Constant @{term lessThan} *} |
203 |
||
14485 | 204 |
lemma lessThan_0 [simp]: "lessThan (0::nat) = {}" |
205 |
by (simp add: lessThan_def) |
|
206 |
||
207 |
lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)" |
|
208 |
by (simp add: lessThan_def less_Suc_eq, blast) |
|
209 |
||
210 |
lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k" |
|
211 |
by (simp add: lessThan_def atMost_def less_Suc_eq_le) |
|
212 |
||
213 |
lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV" |
|
214 |
by blast |
|
215 |
||
15047 | 216 |
subsubsection {* The Constant @{term greaterThan} *} |
217 |
||
14485 | 218 |
lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc" |
219 |
apply (simp add: greaterThan_def) |
|
220 |
apply (blast dest: gr0_conv_Suc [THEN iffD1]) |
|
221 |
done |
|
222 |
||
223 |
lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}" |
|
224 |
apply (simp add: greaterThan_def) |
|
225 |
apply (auto elim: linorder_neqE) |
|
226 |
done |
|
227 |
||
228 |
lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}" |
|
229 |
by blast |
|
230 |
||
15047 | 231 |
subsubsection {* The Constant @{term atLeast} *} |
232 |
||
14485 | 233 |
lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV" |
234 |
by (unfold atLeast_def UNIV_def, simp) |
|
235 |
||
236 |
lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}" |
|
237 |
apply (simp add: atLeast_def) |
|
238 |
apply (simp add: Suc_le_eq) |
|
239 |
apply (simp add: order_le_less, blast) |
|
240 |
done |
|
241 |
||
242 |
lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k" |
|
243 |
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) |
|
244 |
||
245 |
lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV" |
|
246 |
by blast |
|
247 |
||
15047 | 248 |
subsubsection {* The Constant @{term atMost} *} |
249 |
||
14485 | 250 |
lemma atMost_0 [simp]: "atMost (0::nat) = {0}" |
251 |
by (simp add: atMost_def) |
|
252 |
||
253 |
lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)" |
|
254 |
apply (simp add: atMost_def) |
|
255 |
apply (simp add: less_Suc_eq order_le_less, blast) |
|
256 |
done |
|
257 |
||
258 |
lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV" |
|
259 |
by blast |
|
260 |
||
15047 | 261 |
subsubsection {* The Constant @{term atLeastLessThan} *} |
262 |
||
263 |
text{*But not a simprule because some concepts are better left in terms |
|
264 |
of @{term atLeastLessThan}*} |
|
265 |
lemma atLeast0LessThan: "{0::nat..<n} = {..<n}" |
|
15042 | 266 |
by(simp add:lessThan_def atLeastLessThan_def) |
267 |
||
15047 | 268 |
lemma atLeastLessThan0 [simp]: "{m..<0::nat} = {}" |
269 |
by (simp add: atLeastLessThan_def) |
|
270 |
||
271 |
lemma atLeastLessThan_self [simp]: "{n::'a::order..<n} = {}" |
|
272 |
by (auto simp add: atLeastLessThan_def) |
|
273 |
||
274 |
lemma atLeastLessThan_empty: "n \<le> m ==> {m..<n::'a::order} = {}" |
|
275 |
by (auto simp add: atLeastLessThan_def) |
|
276 |
||
277 |
subsubsection {* Intervals of nats with @{term Suc} *} |
|
278 |
||
279 |
text{*Not a simprule because the RHS is too messy.*} |
|
280 |
lemma atLeastLessThanSuc: |
|
281 |
"{m..<Suc n} = (if m \<le> n then insert n {m..<n} else {})" |
|
282 |
by (auto simp add: atLeastLessThan_def) |
|
283 |
||
284 |
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" |
|
285 |
by (auto simp add: atLeastLessThan_def) |
|
286 |
||
287 |
lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}" |
|
288 |
by (induct k, simp_all add: atLeastLessThanSuc) |
|
289 |
||
290 |
lemma atLeastSucLessThan [simp]: "{Suc n..<n} = {}" |
|
291 |
by (auto simp add: atLeastLessThan_def) |
|
14485 | 292 |
|
15045 | 293 |
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" |
14485 | 294 |
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) |
295 |
||
15045 | 296 |
lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}" |
14485 | 297 |
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def |
298 |
greaterThanAtMost_def) |
|
299 |
||
15045 | 300 |
lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}" |
14485 | 301 |
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def |
302 |
greaterThanLessThan_def) |
|
303 |
||
304 |
subsubsection {* Finiteness *} |
|
305 |
||
15045 | 306 |
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}" |
14485 | 307 |
by (induct k) (simp_all add: lessThan_Suc) |
308 |
||
309 |
lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}" |
|
310 |
by (induct k) (simp_all add: atMost_Suc) |
|
311 |
||
312 |
lemma finite_greaterThanLessThan [iff]: |
|
15045 | 313 |
fixes l :: nat shows "finite {l<..<u}" |
14485 | 314 |
by (simp add: greaterThanLessThan_def) |
315 |
||
316 |
lemma finite_atLeastLessThan [iff]: |
|
15045 | 317 |
fixes l :: nat shows "finite {l..<u}" |
14485 | 318 |
by (simp add: atLeastLessThan_def) |
319 |
||
320 |
lemma finite_greaterThanAtMost [iff]: |
|
15045 | 321 |
fixes l :: nat shows "finite {l<..u}" |
14485 | 322 |
by (simp add: greaterThanAtMost_def) |
323 |
||
324 |
lemma finite_atLeastAtMost [iff]: |
|
325 |
fixes l :: nat shows "finite {l..u}" |
|
326 |
by (simp add: atLeastAtMost_def) |
|
327 |
||
328 |
lemma bounded_nat_set_is_finite: |
|
329 |
"(ALL i:N. i < (n::nat)) ==> finite N" |
|
330 |
-- {* A bounded set of natural numbers is finite. *} |
|
331 |
apply (rule finite_subset) |
|
332 |
apply (rule_tac [2] finite_lessThan, auto) |
|
333 |
done |
|
334 |
||
335 |
subsubsection {* Cardinality *} |
|
336 |
||
15045 | 337 |
lemma card_lessThan [simp]: "card {..<u} = u" |
15251 | 338 |
by (induct u, simp_all add: lessThan_Suc) |
14485 | 339 |
|
340 |
lemma card_atMost [simp]: "card {..u} = Suc u" |
|
341 |
by (simp add: lessThan_Suc_atMost [THEN sym]) |
|
342 |
||
15045 | 343 |
lemma card_atLeastLessThan [simp]: "card {l..<u} = u - l" |
344 |
apply (subgoal_tac "card {l..<u} = card {..<u-l}") |
|
14485 | 345 |
apply (erule ssubst, rule card_lessThan) |
15045 | 346 |
apply (subgoal_tac "(%x. x + l) ` {..<u-l} = {l..<u}") |
14485 | 347 |
apply (erule subst) |
348 |
apply (rule card_image) |
|
349 |
apply (rule finite_lessThan) |
|
350 |
apply (simp add: inj_on_def) |
|
351 |
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) |
|
352 |
apply arith |
|
353 |
apply (rule_tac x = "x - l" in exI) |
|
354 |
apply arith |
|
355 |
done |
|
356 |
||
15047 | 357 |
lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l" |
14485 | 358 |
by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp) |
359 |
||
15045 | 360 |
lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l" |
14485 | 361 |
by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp) |
362 |
||
15045 | 363 |
lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l" |
14485 | 364 |
by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp) |
365 |
||
366 |
subsection {* Intervals of integers *} |
|
367 |
||
15045 | 368 |
lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}" |
14485 | 369 |
by (auto simp add: atLeastAtMost_def atLeastLessThan_def) |
370 |
||
15045 | 371 |
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" |
14485 | 372 |
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) |
373 |
||
374 |
lemma atLeastPlusOneLessThan_greaterThanLessThan_int: |
|
15045 | 375 |
"{l+1..<u} = {l<..<u::int}" |
14485 | 376 |
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) |
377 |
||
378 |
subsubsection {* Finiteness *} |
|
379 |
||
380 |
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> |
|
15045 | 381 |
{(0::int)..<u} = int ` {..<nat u}" |
14485 | 382 |
apply (unfold image_def lessThan_def) |
383 |
apply auto |
|
384 |
apply (rule_tac x = "nat x" in exI) |
|
385 |
apply (auto simp add: zless_nat_conj zless_nat_eq_int_zless [THEN sym]) |
|
386 |
done |
|
387 |
||
15045 | 388 |
lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}" |
14485 | 389 |
apply (case_tac "0 \<le> u") |
390 |
apply (subst image_atLeastZeroLessThan_int, assumption) |
|
391 |
apply (rule finite_imageI) |
|
392 |
apply auto |
|
15045 | 393 |
apply (subgoal_tac "{0..<u} = {}") |
14485 | 394 |
apply auto |
395 |
done |
|
396 |
||
397 |
lemma image_atLeastLessThan_int_shift: |
|
15045 | 398 |
"(%x. x + (l::int)) ` {0..<u-l} = {l..<u}" |
14485 | 399 |
apply (auto simp add: image_def atLeastLessThan_iff) |
400 |
apply (rule_tac x = "x - l" in bexI) |
|
401 |
apply auto |
|
402 |
done |
|
403 |
||
15045 | 404 |
lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}" |
405 |
apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}") |
|
14485 | 406 |
apply (erule subst) |
407 |
apply (rule finite_imageI) |
|
408 |
apply (rule finite_atLeastZeroLessThan_int) |
|
409 |
apply (rule image_atLeastLessThan_int_shift) |
|
410 |
done |
|
411 |
||
412 |
lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}" |
|
413 |
by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp) |
|
414 |
||
15045 | 415 |
lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}" |
14485 | 416 |
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) |
417 |
||
15045 | 418 |
lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}" |
14485 | 419 |
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) |
420 |
||
421 |
subsubsection {* Cardinality *} |
|
422 |
||
15045 | 423 |
lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u" |
14485 | 424 |
apply (case_tac "0 \<le> u") |
425 |
apply (subst image_atLeastZeroLessThan_int, assumption) |
|
426 |
apply (subst card_image) |
|
427 |
apply (auto simp add: inj_on_def) |
|
428 |
done |
|
429 |
||
15045 | 430 |
lemma card_atLeastLessThan_int [simp]: "card {l..<u} = nat (u - l)" |
431 |
apply (subgoal_tac "card {l..<u} = card {0..<u-l}") |
|
14485 | 432 |
apply (erule ssubst, rule card_atLeastZeroLessThan_int) |
15045 | 433 |
apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}") |
14485 | 434 |
apply (erule subst) |
435 |
apply (rule card_image) |
|
436 |
apply (rule finite_atLeastZeroLessThan_int) |
|
437 |
apply (simp add: inj_on_def) |
|
438 |
apply (rule image_atLeastLessThan_int_shift) |
|
439 |
done |
|
440 |
||
441 |
lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)" |
|
442 |
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) |
|
443 |
apply (auto simp add: compare_rls) |
|
444 |
done |
|
445 |
||
15045 | 446 |
lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)" |
14485 | 447 |
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) |
448 |
||
15045 | 449 |
lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u - (l + 1))" |
14485 | 450 |
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) |
451 |
||
452 |
||
13850 | 453 |
subsection {*Lemmas useful with the summation operator setsum*} |
454 |
||
14577 | 455 |
text {* For examples, see Algebra/poly/UnivPoly.thy *} |
13735 | 456 |
|
14577 | 457 |
subsubsection {* Disjoint Unions *} |
13735 | 458 |
|
14577 | 459 |
text {* Singletons and open intervals *} |
13735 | 460 |
|
461 |
lemma ivl_disj_un_singleton: |
|
15045 | 462 |
"{l::'a::linorder} Un {l<..} = {l..}" |
463 |
"{..<u} Un {u::'a::linorder} = {..u}" |
|
464 |
"(l::'a::linorder) < u ==> {l} Un {l<..<u} = {l..<u}" |
|
465 |
"(l::'a::linorder) < u ==> {l<..<u} Un {u} = {l<..u}" |
|
466 |
"(l::'a::linorder) <= u ==> {l} Un {l<..u} = {l..u}" |
|
467 |
"(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
|
468 |
by auto |
13735 | 469 |
|
14577 | 470 |
text {* One- and two-sided intervals *} |
13735 | 471 |
|
472 |
lemma ivl_disj_un_one: |
|
15045 | 473 |
"(l::'a::linorder) < u ==> {..l} Un {l<..<u} = {..<u}" |
474 |
"(l::'a::linorder) <= u ==> {..<l} Un {l..<u} = {..<u}" |
|
475 |
"(l::'a::linorder) <= u ==> {..l} Un {l<..u} = {..u}" |
|
476 |
"(l::'a::linorder) <= u ==> {..<l} Un {l..u} = {..u}" |
|
477 |
"(l::'a::linorder) <= u ==> {l<..u} Un {u<..} = {l<..}" |
|
478 |
"(l::'a::linorder) < u ==> {l<..<u} Un {u..} = {l<..}" |
|
479 |
"(l::'a::linorder) <= u ==> {l..u} Un {u<..} = {l..}" |
|
480 |
"(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
|
481 |
by auto |
13735 | 482 |
|
14577 | 483 |
text {* Two- and two-sided intervals *} |
13735 | 484 |
|
485 |
lemma ivl_disj_un_two: |
|
15045 | 486 |
"[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..<u} = {l<..<u}" |
487 |
"[| (l::'a::linorder) <= m; m < u |] ==> {l<..m} Un {m<..<u} = {l<..<u}" |
|
488 |
"[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..<u} = {l..<u}" |
|
489 |
"[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {m<..<u} = {l..<u}" |
|
490 |
"[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..u} = {l<..u}" |
|
491 |
"[| (l::'a::linorder) <= m; m <= u |] ==> {l<..m} Un {m<..u} = {l<..u}" |
|
492 |
"[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..u} = {l..u}" |
|
493 |
"[| (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
|
494 |
by auto |
13735 | 495 |
|
496 |
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two |
|
497 |
||
14577 | 498 |
subsubsection {* Disjoint Intersections *} |
13735 | 499 |
|
14577 | 500 |
text {* Singletons and open intervals *} |
13735 | 501 |
|
502 |
lemma ivl_disj_int_singleton: |
|
15045 | 503 |
"{l::'a::order} Int {l<..} = {}" |
504 |
"{..<u} Int {u} = {}" |
|
505 |
"{l} Int {l<..<u} = {}" |
|
506 |
"{l<..<u} Int {u} = {}" |
|
507 |
"{l} Int {l<..u} = {}" |
|
508 |
"{l..<u} Int {u} = {}" |
|
13735 | 509 |
by simp+ |
510 |
||
14577 | 511 |
text {* One- and two-sided intervals *} |
13735 | 512 |
|
513 |
lemma ivl_disj_int_one: |
|
15045 | 514 |
"{..l::'a::order} Int {l<..<u} = {}" |
515 |
"{..<l} Int {l..<u} = {}" |
|
516 |
"{..l} Int {l<..u} = {}" |
|
517 |
"{..<l} Int {l..u} = {}" |
|
518 |
"{l<..u} Int {u<..} = {}" |
|
519 |
"{l<..<u} Int {u..} = {}" |
|
520 |
"{l..u} Int {u<..} = {}" |
|
521 |
"{l..<u} Int {u..} = {}" |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset
|
522 |
by auto |
13735 | 523 |
|
14577 | 524 |
text {* Two- and two-sided intervals *} |
13735 | 525 |
|
526 |
lemma ivl_disj_int_two: |
|
15045 | 527 |
"{l::'a::order<..<m} Int {m..<u} = {}" |
528 |
"{l<..m} Int {m<..<u} = {}" |
|
529 |
"{l..<m} Int {m..<u} = {}" |
|
530 |
"{l..m} Int {m<..<u} = {}" |
|
531 |
"{l<..<m} Int {m..u} = {}" |
|
532 |
"{l<..m} Int {m<..u} = {}" |
|
533 |
"{l..<m} Int {m..u} = {}" |
|
534 |
"{l..m} Int {m<..u} = {}" |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset
|
535 |
by auto |
13735 | 536 |
|
537 |
lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two |
|
538 |
||
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset
|
539 |
|
15042 | 540 |
subsection {* Summation indexed over intervals *} |
541 |
||
542 |
syntax |
|
543 |
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) |
|
15048 | 544 |
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) |
545 |
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10) |
|
15042 | 546 |
syntax (xsymbols) |
547 |
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) |
|
15048 | 548 |
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) |
549 |
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) |
|
15042 | 550 |
syntax (HTML output) |
551 |
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) |
|
15048 | 552 |
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) |
553 |
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) |
|
15056 | 554 |
syntax (latex_sum output) |
15052 | 555 |
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" |
556 |
("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) |
|
557 |
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" |
|
558 |
("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) |
|
559 |
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" |
|
560 |
("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10) |
|
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset
|
561 |
|
15048 | 562 |
translations |
563 |
"\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}" |
|
564 |
"\<Sum>x=a..<b. t" == "setsum (%x. t) {a..<b}" |
|
565 |
"\<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
|
566 |
|
15052 | 567 |
text{* The above introduces some pretty alternative syntaxes for |
15056 | 568 |
summation over intervals: |
15052 | 569 |
\begin{center} |
570 |
\begin{tabular}{lll} |
|
15056 | 571 |
Old & New & \LaTeX\\ |
572 |
@{term[source]"\<Sum>x\<in>{a..b}. e"} & @{term"\<Sum>x=a..b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..b. e"}\\ |
|
573 |
@{term[source]"\<Sum>x\<in>{a..<b}. e"} & @{term"\<Sum>x=a..<b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..<b. e"}\\ |
|
574 |
@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"} |
|
15052 | 575 |
\end{tabular} |
576 |
\end{center} |
|
15056 | 577 |
The left column shows the term before introduction of the new syntax, |
578 |
the middle column shows the new (default) syntax, and the right column |
|
579 |
shows a special syntax. The latter is only meaningful for latex output |
|
580 |
and has to be activated explicitly by setting the print mode to |
|
581 |
\texttt{latex\_sum} (e.g.\ via \texttt{mode=latex\_sum} in |
|
582 |
antiquotations). It is not the default \LaTeX\ output because it only |
|
583 |
works well with italic-style formulae, not tt-style. |
|
15052 | 584 |
|
585 |
Note that for uniformity on @{typ nat} it is better to use |
|
586 |
@{term"\<Sum>x::nat=0..<n. e"} rather than @{text"\<Sum>x<n. e"}: @{text setsum} may |
|
587 |
not provide all lemmas available for @{term"{m..<n}"} also in the |
|
588 |
special form for @{term"{..<n}"}. *} |
|
589 |
||
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset
|
590 |
|
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset
|
591 |
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
|
592 |
by (simp add:lessThan_Suc) |
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset
|
593 |
|
8924 | 594 |
end |