author | nipkow |
Mon, 21 Feb 2005 15:04:10 +0100 | |
changeset 15539 | 333a88244569 |
parent 15418 | e28853da5df5 |
child 15542 | ee6cd48cf840 |
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 |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
90 |
lemma Compl_lessThan [simp]: |
13735 | 91 |
"!!k:: 'a::linorder. -lessThan k = atLeast k" |
13850 | 92 |
apply (auto simp add: lessThan_def atLeast_def) |
13735 | 93 |
done |
94 |
||
13850 | 95 |
lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}" |
96 |
by auto |
|
13735 | 97 |
|
13850 | 98 |
lemma greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)" |
99 |
by (simp add: greaterThan_def) |
|
13735 | 100 |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
101 |
lemma Compl_greaterThan [simp]: |
13735 | 102 |
"!!k:: 'a::linorder. -greaterThan k = atMost k" |
13850 | 103 |
apply (simp add: greaterThan_def atMost_def le_def, auto) |
13735 | 104 |
done |
105 |
||
13850 | 106 |
lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k" |
107 |
apply (subst Compl_greaterThan [symmetric]) |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
108 |
apply (rule double_complement) |
13735 | 109 |
done |
110 |
||
13850 | 111 |
lemma atLeast_iff [iff]: "(i: atLeast k) = (k<=i)" |
112 |
by (simp add: atLeast_def) |
|
13735 | 113 |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
114 |
lemma Compl_atLeast [simp]: |
13735 | 115 |
"!!k:: 'a::linorder. -atLeast k = lessThan k" |
13850 | 116 |
apply (simp add: lessThan_def atLeast_def le_def, auto) |
13735 | 117 |
done |
118 |
||
13850 | 119 |
lemma atMost_iff [iff]: "(i: atMost k) = (i<=k)" |
120 |
by (simp add: atMost_def) |
|
13735 | 121 |
|
14485 | 122 |
lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" |
123 |
by (blast intro: order_antisym) |
|
13850 | 124 |
|
125 |
||
14485 | 126 |
subsection {* Logical Equivalences for Set Inclusion and Equality *} |
13850 | 127 |
|
128 |
lemma atLeast_subset_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
129 |
"(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))" |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
130 |
by (blast intro: order_trans) |
13850 | 131 |
|
132 |
lemma atLeast_eq_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
133 |
"(atLeast x = atLeast y) = (x = (y::'a::linorder))" |
13850 | 134 |
by (blast intro: order_antisym order_trans) |
135 |
||
136 |
lemma greaterThan_subset_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
137 |
"(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))" |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
138 |
apply (auto simp add: greaterThan_def) |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
139 |
apply (subst linorder_not_less [symmetric], blast) |
13850 | 140 |
done |
141 |
||
142 |
lemma greaterThan_eq_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
143 |
"(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
144 |
apply (rule iffI) |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
145 |
apply (erule equalityE) |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
146 |
apply (simp_all add: greaterThan_subset_iff) |
13850 | 147 |
done |
148 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
149 |
lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))" |
13850 | 150 |
by (blast intro: order_trans) |
151 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
152 |
lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" |
13850 | 153 |
by (blast intro: order_antisym order_trans) |
154 |
||
155 |
lemma lessThan_subset_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
156 |
"(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))" |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
157 |
apply (auto simp add: lessThan_def) |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
158 |
apply (subst linorder_not_less [symmetric], blast) |
13850 | 159 |
done |
160 |
||
161 |
lemma lessThan_eq_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
162 |
"(lessThan x = lessThan y) = (x = (y::'a::linorder))" |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
163 |
apply (rule iffI) |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
164 |
apply (erule equalityE) |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
165 |
apply (simp_all add: lessThan_subset_iff) |
13735 | 166 |
done |
167 |
||
168 |
||
13850 | 169 |
subsection {*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 {})" |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
282 |
by (auto simp add: atLeastLessThan_def) |
15047 | 283 |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
284 |
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" |
15047 | 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 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
296 |
lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}" |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
297 |
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def |
14485 | 298 |
greaterThanAtMost_def) |
299 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
300 |
lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}" |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
301 |
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def |
14485 | 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 (simp add: inj_on_def) |
|
350 |
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) |
|
351 |
apply arith |
|
352 |
apply (rule_tac x = "x - l" in exI) |
|
353 |
apply arith |
|
354 |
done |
|
355 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
356 |
lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l" |
14485 | 357 |
by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp) |
358 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
359 |
lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l" |
14485 | 360 |
by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp) |
361 |
||
15045 | 362 |
lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l" |
14485 | 363 |
by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp) |
364 |
||
365 |
subsection {* Intervals of integers *} |
|
366 |
||
15045 | 367 |
lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}" |
14485 | 368 |
by (auto simp add: atLeastAtMost_def atLeastLessThan_def) |
369 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
370 |
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" |
14485 | 371 |
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) |
372 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
373 |
lemma atLeastPlusOneLessThan_greaterThanLessThan_int: |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
374 |
"{l+1..<u} = {l<..<u::int}" |
14485 | 375 |
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) |
376 |
||
377 |
subsubsection {* Finiteness *} |
|
378 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
379 |
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> |
15045 | 380 |
{(0::int)..<u} = int ` {..<nat u}" |
14485 | 381 |
apply (unfold image_def lessThan_def) |
382 |
apply auto |
|
383 |
apply (rule_tac x = "nat x" in exI) |
|
384 |
apply (auto simp add: zless_nat_conj zless_nat_eq_int_zless [THEN sym]) |
|
385 |
done |
|
386 |
||
15045 | 387 |
lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}" |
14485 | 388 |
apply (case_tac "0 \<le> u") |
389 |
apply (subst image_atLeastZeroLessThan_int, assumption) |
|
390 |
apply (rule finite_imageI) |
|
391 |
apply auto |
|
15045 | 392 |
apply (subgoal_tac "{0..<u} = {}") |
14485 | 393 |
apply auto |
394 |
done |
|
395 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
396 |
lemma image_atLeastLessThan_int_shift: |
15045 | 397 |
"(%x. x + (l::int)) ` {0..<u-l} = {l..<u}" |
14485 | 398 |
apply (auto simp add: image_def atLeastLessThan_iff) |
399 |
apply (rule_tac x = "x - l" in bexI) |
|
400 |
apply auto |
|
401 |
done |
|
402 |
||
15045 | 403 |
lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}" |
404 |
apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}") |
|
14485 | 405 |
apply (erule subst) |
406 |
apply (rule finite_imageI) |
|
407 |
apply (rule finite_atLeastZeroLessThan_int) |
|
408 |
apply (rule image_atLeastLessThan_int_shift) |
|
409 |
done |
|
410 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
411 |
lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}" |
14485 | 412 |
by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp) |
413 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
414 |
lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}" |
14485 | 415 |
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) |
416 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
417 |
lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}" |
14485 | 418 |
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) |
419 |
||
420 |
subsubsection {* Cardinality *} |
|
421 |
||
15045 | 422 |
lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u" |
14485 | 423 |
apply (case_tac "0 \<le> u") |
424 |
apply (subst image_atLeastZeroLessThan_int, assumption) |
|
425 |
apply (subst card_image) |
|
426 |
apply (auto simp add: inj_on_def) |
|
427 |
done |
|
428 |
||
15045 | 429 |
lemma card_atLeastLessThan_int [simp]: "card {l..<u} = nat (u - l)" |
430 |
apply (subgoal_tac "card {l..<u} = card {0..<u-l}") |
|
14485 | 431 |
apply (erule ssubst, rule card_atLeastZeroLessThan_int) |
15045 | 432 |
apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}") |
14485 | 433 |
apply (erule subst) |
434 |
apply (rule card_image) |
|
435 |
apply (simp add: inj_on_def) |
|
436 |
apply (rule image_atLeastLessThan_int_shift) |
|
437 |
done |
|
438 |
||
439 |
lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)" |
|
440 |
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) |
|
441 |
apply (auto simp add: compare_rls) |
|
442 |
done |
|
443 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
444 |
lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)" |
14485 | 445 |
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) |
446 |
||
15045 | 447 |
lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u - (l + 1))" |
14485 | 448 |
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) |
449 |
||
450 |
||
13850 | 451 |
subsection {*Lemmas useful with the summation operator setsum*} |
452 |
||
14577 | 453 |
text {* For examples, see Algebra/poly/UnivPoly.thy *} |
13735 | 454 |
|
14577 | 455 |
subsubsection {* Disjoint Unions *} |
13735 | 456 |
|
14577 | 457 |
text {* Singletons and open intervals *} |
13735 | 458 |
|
459 |
lemma ivl_disj_un_singleton: |
|
15045 | 460 |
"{l::'a::linorder} Un {l<..} = {l..}" |
461 |
"{..<u} Un {u::'a::linorder} = {..u}" |
|
462 |
"(l::'a::linorder) < u ==> {l} Un {l<..<u} = {l..<u}" |
|
463 |
"(l::'a::linorder) < u ==> {l<..<u} Un {u} = {l<..u}" |
|
464 |
"(l::'a::linorder) <= u ==> {l} Un {l<..u} = {l..u}" |
|
465 |
"(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
|
466 |
by auto |
13735 | 467 |
|
14577 | 468 |
text {* One- and two-sided intervals *} |
13735 | 469 |
|
470 |
lemma ivl_disj_un_one: |
|
15045 | 471 |
"(l::'a::linorder) < u ==> {..l} Un {l<..<u} = {..<u}" |
472 |
"(l::'a::linorder) <= u ==> {..<l} Un {l..<u} = {..<u}" |
|
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<..u} Un {u<..} = {l<..}" |
|
476 |
"(l::'a::linorder) < u ==> {l<..<u} Un {u..} = {l<..}" |
|
477 |
"(l::'a::linorder) <= u ==> {l..u} Un {u<..} = {l..}" |
|
478 |
"(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
|
479 |
by auto |
13735 | 480 |
|
14577 | 481 |
text {* Two- and two-sided intervals *} |
13735 | 482 |
|
483 |
lemma ivl_disj_un_two: |
|
15045 | 484 |
"[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..<u} = {l<..<u}" |
485 |
"[| (l::'a::linorder) <= m; m < u |] ==> {l<..m} Un {m<..<u} = {l<..<u}" |
|
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}" |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset
|
492 |
by auto |
13735 | 493 |
|
494 |
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two |
|
495 |
||
14577 | 496 |
subsubsection {* Disjoint Intersections *} |
13735 | 497 |
|
14577 | 498 |
text {* Singletons and open intervals *} |
13735 | 499 |
|
500 |
lemma ivl_disj_int_singleton: |
|
15045 | 501 |
"{l::'a::order} Int {l<..} = {}" |
502 |
"{..<u} Int {u} = {}" |
|
503 |
"{l} Int {l<..<u} = {}" |
|
504 |
"{l<..<u} Int {u} = {}" |
|
505 |
"{l} Int {l<..u} = {}" |
|
506 |
"{l..<u} Int {u} = {}" |
|
13735 | 507 |
by simp+ |
508 |
||
14577 | 509 |
text {* One- and two-sided intervals *} |
13735 | 510 |
|
511 |
lemma ivl_disj_int_one: |
|
15045 | 512 |
"{..l::'a::order} Int {l<..<u} = {}" |
513 |
"{..<l} Int {l..<u} = {}" |
|
514 |
"{..l} Int {l<..u} = {}" |
|
515 |
"{..<l} Int {l..u} = {}" |
|
516 |
"{l<..u} Int {u<..} = {}" |
|
517 |
"{l<..<u} Int {u..} = {}" |
|
518 |
"{l..u} Int {u<..} = {}" |
|
519 |
"{l..<u} Int {u..} = {}" |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset
|
520 |
by auto |
13735 | 521 |
|
14577 | 522 |
text {* Two- and two-sided intervals *} |
13735 | 523 |
|
524 |
lemma ivl_disj_int_two: |
|
15045 | 525 |
"{l::'a::order<..<m} Int {m..<u} = {}" |
526 |
"{l<..m} Int {m<..<u} = {}" |
|
527 |
"{l..<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} = {}" |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset
|
533 |
by auto |
13735 | 534 |
|
535 |
lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two |
|
536 |
||
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset
|
537 |
|
15042 | 538 |
subsection {* Summation indexed over intervals *} |
539 |
||
540 |
syntax |
|
541 |
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) |
|
15048 | 542 |
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) |
543 |
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10) |
|
15042 | 544 |
syntax (xsymbols) |
545 |
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) |
|
15048 | 546 |
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) |
547 |
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) |
|
15042 | 548 |
syntax (HTML output) |
549 |
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) |
|
15048 | 550 |
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) |
551 |
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) |
|
15056 | 552 |
syntax (latex_sum output) |
15052 | 553 |
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" |
554 |
("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) |
|
555 |
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" |
|
556 |
("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) |
|
557 |
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" |
|
558 |
("(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
|
559 |
|
15048 | 560 |
translations |
561 |
"\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}" |
|
562 |
"\<Sum>x=a..<b. t" == "setsum (%x. t) {a..<b}" |
|
563 |
"\<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
|
564 |
|
15052 | 565 |
text{* The above introduces some pretty alternative syntaxes for |
15056 | 566 |
summation over intervals: |
15052 | 567 |
\begin{center} |
568 |
\begin{tabular}{lll} |
|
15056 | 569 |
Old & New & \LaTeX\\ |
570 |
@{term[source]"\<Sum>x\<in>{a..b}. e"} & @{term"\<Sum>x=a..b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..b. e"}\\ |
|
571 |
@{term[source]"\<Sum>x\<in>{a..<b}. e"} & @{term"\<Sum>x=a..<b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..<b. e"}\\ |
|
572 |
@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"} |
|
15052 | 573 |
\end{tabular} |
574 |
\end{center} |
|
15056 | 575 |
The left column shows the term before introduction of the new syntax, |
576 |
the middle column shows the new (default) syntax, and the right column |
|
577 |
shows a special syntax. The latter is only meaningful for latex output |
|
578 |
and has to be activated explicitly by setting the print mode to |
|
579 |
\texttt{latex\_sum} (e.g.\ via \texttt{mode=latex\_sum} in |
|
580 |
antiquotations). It is not the default \LaTeX\ output because it only |
|
581 |
works well with italic-style formulae, not tt-style. |
|
15052 | 582 |
|
583 |
Note that for uniformity on @{typ nat} it is better to use |
|
584 |
@{term"\<Sum>x::nat=0..<n. e"} rather than @{text"\<Sum>x<n. e"}: @{text setsum} may |
|
585 |
not provide all lemmas available for @{term"{m..<n}"} also in the |
|
586 |
special form for @{term"{..<n}"}. *} |
|
587 |
||
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset
|
588 |
|
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset
|
589 |
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
|
590 |
by (simp add:lessThan_Suc) |
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset
|
591 |
|
15539 | 592 |
lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> |
593 |
setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}" |
|
594 |
by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un) |
|
595 |
||
596 |
lemma setsum_diff_nat_ivl: |
|
597 |
fixes f :: "nat \<Rightarrow> 'a::ab_group_add" |
|
598 |
shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> |
|
599 |
setsum f {m..<p} - setsum f {m..<n} = setsum f {n..<p}" |
|
600 |
using setsum_add_nat_ivl [of m n p f,symmetric] |
|
601 |
apply (simp add: add_ac) |
|
602 |
done |
|
603 |
||
604 |
lemma setsum_shift_bounds_nat_ivl: |
|
605 |
"setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}" |
|
606 |
by (induct "n", auto simp:atLeastLessThanSuc) |
|
607 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
608 |
|
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
609 |
ML |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
610 |
{* |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
611 |
val Compl_atLeast = thm "Compl_atLeast"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
612 |
val Compl_atMost = thm "Compl_atMost"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
613 |
val Compl_greaterThan = thm "Compl_greaterThan"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
614 |
val Compl_lessThan = thm "Compl_lessThan"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
615 |
val INT_greaterThan_UNIV = thm "INT_greaterThan_UNIV"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
616 |
val UN_atLeast_UNIV = thm "UN_atLeast_UNIV"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
617 |
val UN_atMost_UNIV = thm "UN_atMost_UNIV"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
618 |
val UN_lessThan_UNIV = thm "UN_lessThan_UNIV"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
619 |
val atLeastAtMost_def = thm "atLeastAtMost_def"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
620 |
val atLeastAtMost_iff = thm "atLeastAtMost_iff"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
621 |
val atLeastLessThan_def = thm "atLeastLessThan_def"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
622 |
val atLeastLessThan_iff = thm "atLeastLessThan_iff"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
623 |
val atLeast_0 = thm "atLeast_0"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
624 |
val atLeast_Suc = thm "atLeast_Suc"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
625 |
val atLeast_def = thm "atLeast_def"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
626 |
val atLeast_iff = thm "atLeast_iff"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
627 |
val atMost_0 = thm "atMost_0"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
628 |
val atMost_Int_atLeast = thm "atMost_Int_atLeast"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
629 |
val atMost_Suc = thm "atMost_Suc"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
630 |
val atMost_def = thm "atMost_def"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
631 |
val atMost_iff = thm "atMost_iff"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
632 |
val greaterThanAtMost_def = thm "greaterThanAtMost_def"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
633 |
val greaterThanAtMost_iff = thm "greaterThanAtMost_iff"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
634 |
val greaterThanLessThan_def = thm "greaterThanLessThan_def"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
635 |
val greaterThanLessThan_iff = thm "greaterThanLessThan_iff"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
636 |
val greaterThan_0 = thm "greaterThan_0"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
637 |
val greaterThan_Suc = thm "greaterThan_Suc"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
638 |
val greaterThan_def = thm "greaterThan_def"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
639 |
val greaterThan_iff = thm "greaterThan_iff"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
640 |
val ivl_disj_int = thms "ivl_disj_int"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
641 |
val ivl_disj_int_one = thms "ivl_disj_int_one"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
642 |
val ivl_disj_int_singleton = thms "ivl_disj_int_singleton"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
643 |
val ivl_disj_int_two = thms "ivl_disj_int_two"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
644 |
val ivl_disj_un = thms "ivl_disj_un"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
645 |
val ivl_disj_un_one = thms "ivl_disj_un_one"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
646 |
val ivl_disj_un_singleton = thms "ivl_disj_un_singleton"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
647 |
val ivl_disj_un_two = thms "ivl_disj_un_two"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
648 |
val lessThan_0 = thm "lessThan_0"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
649 |
val lessThan_Suc = thm "lessThan_Suc"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
650 |
val lessThan_Suc_atMost = thm "lessThan_Suc_atMost"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
651 |
val lessThan_def = thm "lessThan_def"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
652 |
val lessThan_iff = thm "lessThan_iff"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
653 |
val single_Diff_lessThan = thm "single_Diff_lessThan"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
654 |
|
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
655 |
val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
656 |
val finite_atMost = thm "finite_atMost"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
657 |
val finite_lessThan = thm "finite_lessThan"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
658 |
*} |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
659 |
|
8924 | 660 |
end |