author | paulson |
Thu, 06 Mar 2003 15:03:16 +0100 | |
changeset 13850 | 6d1bb3059818 |
parent 13735 | 7de9342aca7a |
child 14398 | c5c47703f763 |
permissions | -rw-r--r-- |
8924 | 1 |
(* Title: HOL/SetInterval.thy |
2 |
ID: $Id$ |
|
13735 | 3 |
Author: Tobias Nipkow and Clemens Ballarin |
8957 | 4 |
Copyright 2000 TU Muenchen |
8924 | 5 |
|
13735 | 6 |
lessThan, greaterThan, atLeast, atMost and two-sided intervals |
8924 | 7 |
*) |
8 |
||
13735 | 9 |
theory SetInterval = NatArith: |
8924 | 10 |
|
11 |
constdefs |
|
11609
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset
|
12 |
lessThan :: "('a::ord) => 'a set" ("(1{.._'(})") |
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset
|
13 |
"{..u(} == {x. x<u}" |
8924 | 14 |
|
11609
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset
|
15 |
atMost :: "('a::ord) => 'a set" ("(1{.._})") |
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset
|
16 |
"{..u} == {x. x<=u}" |
8924 | 17 |
|
11609
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset
|
18 |
greaterThan :: "('a::ord) => 'a set" ("(1{')_..})") |
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset
|
19 |
"{)l..} == {x. l<x}" |
8924 | 20 |
|
11609
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset
|
21 |
atLeast :: "('a::ord) => 'a set" ("(1{_..})") |
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset
|
22 |
"{l..} == {x. l<=x}" |
8924 | 23 |
|
13735 | 24 |
greaterThanLessThan :: "['a::ord, 'a] => 'a set" ("(1{')_.._'(})") |
25 |
"{)l..u(} == {)l..} Int {..u(}" |
|
26 |
||
27 |
atLeastLessThan :: "['a::ord, 'a] => 'a set" ("(1{_.._'(})") |
|
28 |
"{l..u(} == {l..} Int {..u(}" |
|
29 |
||
30 |
greaterThanAtMost :: "['a::ord, 'a] => 'a set" ("(1{')_.._})") |
|
31 |
"{)l..u} == {)l..} Int {..u}" |
|
32 |
||
33 |
atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})") |
|
34 |
"{l..u} == {l..} Int {..u}" |
|
35 |
||
13850 | 36 |
|
37 |
subsection {* Setup of transitivity reasoner *} |
|
13735 | 38 |
|
39 |
ML {* |
|
40 |
||
41 |
structure Trans_Tac = Trans_Tac_Fun ( |
|
42 |
struct |
|
43 |
val less_reflE = thm "order_less_irrefl" RS thm "notE"; |
|
44 |
val le_refl = thm "order_refl"; |
|
45 |
val less_imp_le = thm "order_less_imp_le"; |
|
46 |
val not_lessI = thm "linorder_not_less" RS thm "iffD2"; |
|
47 |
val not_leI = thm "linorder_not_less" RS thm "iffD2"; |
|
48 |
val not_lessD = thm "linorder_not_less" RS thm "iffD1"; |
|
49 |
val not_leD = thm "linorder_not_le" RS thm "iffD1"; |
|
50 |
val eqI = thm "order_antisym"; |
|
51 |
val eqD1 = thm "order_eq_refl"; |
|
52 |
val eqD2 = thm "sym" RS thm "order_eq_refl"; |
|
53 |
val less_trans = thm "order_less_trans"; |
|
54 |
val less_le_trans = thm "order_less_le_trans"; |
|
55 |
val le_less_trans = thm "order_le_less_trans"; |
|
56 |
val le_trans = thm "order_trans"; |
|
57 |
fun decomp (Trueprop $ t) = |
|
58 |
let fun dec (Const ("Not", _) $ t) = ( |
|
59 |
case dec t of |
|
60 |
None => None |
|
61 |
| Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2)) |
|
62 |
| dec (Const (rel, _) $ t1 $ t2) = |
|
63 |
Some (t1, implode (drop (3, explode rel)), t2) |
|
64 |
| dec _ = None |
|
65 |
in dec t end |
|
66 |
| decomp _ = None |
|
67 |
end); |
|
68 |
||
69 |
val trans_tac = Trans_Tac.trans_tac; |
|
70 |
||
71 |
*} |
|
72 |
||
73 |
method_setup trans = |
|
74 |
{* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac)) *} |
|
75 |
{* simple transitivity reasoner *} |
|
76 |
||
77 |
||
13850 | 78 |
subsection {*lessThan*} |
13735 | 79 |
|
13850 | 80 |
lemma lessThan_iff [iff]: "(i: lessThan k) = (i<k)" |
81 |
by (simp add: lessThan_def) |
|
13735 | 82 |
|
13850 | 83 |
lemma lessThan_0 [simp]: "lessThan (0::nat) = {}" |
84 |
by (simp add: lessThan_def) |
|
13735 | 85 |
|
86 |
lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)" |
|
13850 | 87 |
by (simp add: lessThan_def less_Suc_eq, blast) |
13735 | 88 |
|
89 |
lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k" |
|
13850 | 90 |
by (simp add: lessThan_def atMost_def less_Suc_eq_le) |
13735 | 91 |
|
92 |
lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV" |
|
13850 | 93 |
by blast |
13735 | 94 |
|
13850 | 95 |
lemma Compl_lessThan [simp]: |
13735 | 96 |
"!!k:: 'a::linorder. -lessThan k = atLeast k" |
13850 | 97 |
apply (auto simp add: lessThan_def atLeast_def) |
98 |
apply (blast intro: linorder_not_less [THEN iffD1]) |
|
13735 | 99 |
apply (blast dest: order_le_less_trans) |
100 |
done |
|
101 |
||
13850 | 102 |
lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}" |
103 |
by auto |
|
13735 | 104 |
|
13850 | 105 |
subsection {*greaterThan*} |
13735 | 106 |
|
13850 | 107 |
lemma greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)" |
108 |
by (simp add: greaterThan_def) |
|
13735 | 109 |
|
13850 | 110 |
lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc" |
111 |
apply (simp add: greaterThan_def) |
|
13735 | 112 |
apply (blast dest: gr0_conv_Suc [THEN iffD1]) |
113 |
done |
|
114 |
||
115 |
lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}" |
|
13850 | 116 |
apply (simp add: greaterThan_def) |
13735 | 117 |
apply (auto elim: linorder_neqE) |
118 |
done |
|
119 |
||
120 |
lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}" |
|
13850 | 121 |
by blast |
13735 | 122 |
|
13850 | 123 |
lemma Compl_greaterThan [simp]: |
13735 | 124 |
"!!k:: 'a::linorder. -greaterThan k = atMost k" |
13850 | 125 |
apply (simp add: greaterThan_def atMost_def le_def, auto) |
13735 | 126 |
apply (blast intro: linorder_not_less [THEN iffD1]) |
127 |
apply (blast dest: order_le_less_trans) |
|
128 |
done |
|
129 |
||
13850 | 130 |
lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k" |
131 |
apply (subst Compl_greaterThan [symmetric]) |
|
132 |
apply (rule double_complement) |
|
13735 | 133 |
done |
134 |
||
135 |
||
13850 | 136 |
subsection {*atLeast*} |
13735 | 137 |
|
13850 | 138 |
lemma atLeast_iff [iff]: "(i: atLeast k) = (k<=i)" |
139 |
by (simp add: atLeast_def) |
|
13735 | 140 |
|
13850 | 141 |
lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV" |
142 |
by (unfold atLeast_def UNIV_def, simp) |
|
13735 | 143 |
|
144 |
lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}" |
|
13850 | 145 |
apply (simp add: atLeast_def) |
146 |
apply (simp add: Suc_le_eq) |
|
147 |
apply (simp add: order_le_less, blast) |
|
13735 | 148 |
done |
149 |
||
150 |
lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV" |
|
13850 | 151 |
by blast |
13735 | 152 |
|
13850 | 153 |
lemma Compl_atLeast [simp]: |
13735 | 154 |
"!!k:: 'a::linorder. -atLeast k = lessThan k" |
13850 | 155 |
apply (simp add: lessThan_def atLeast_def le_def, auto) |
13735 | 156 |
apply (blast intro: linorder_not_less [THEN iffD1]) |
157 |
apply (blast dest: order_le_less_trans) |
|
158 |
done |
|
159 |
||
160 |
||
13850 | 161 |
subsection {*atMost*} |
13735 | 162 |
|
13850 | 163 |
lemma atMost_iff [iff]: "(i: atMost k) = (i<=k)" |
164 |
by (simp add: atMost_def) |
|
13735 | 165 |
|
13850 | 166 |
lemma atMost_0 [simp]: "atMost (0::nat) = {0}" |
167 |
by (simp add: atMost_def) |
|
13735 | 168 |
|
169 |
lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)" |
|
13850 | 170 |
apply (simp add: atMost_def) |
171 |
apply (simp add: less_Suc_eq order_le_less, blast) |
|
13735 | 172 |
done |
173 |
||
174 |
lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV" |
|
13850 | 175 |
by blast |
176 |
||
177 |
||
178 |
subsection {*Logical Equivalences for Set Inclusion and Equality*} |
|
179 |
||
180 |
lemma atLeast_subset_iff [iff]: |
|
181 |
"(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))" |
|
182 |
by (blast intro: order_trans) |
|
183 |
||
184 |
lemma atLeast_eq_iff [iff]: |
|
185 |
"(atLeast x = atLeast y) = (x = (y::'a::linorder))" |
|
186 |
by (blast intro: order_antisym order_trans) |
|
187 |
||
188 |
lemma greaterThan_subset_iff [iff]: |
|
189 |
"(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))" |
|
190 |
apply (auto simp add: greaterThan_def) |
|
191 |
apply (subst linorder_not_less [symmetric], blast) |
|
192 |
apply (blast intro: order_le_less_trans) |
|
193 |
done |
|
194 |
||
195 |
lemma greaterThan_eq_iff [iff]: |
|
196 |
"(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" |
|
197 |
apply (rule iffI) |
|
198 |
apply (erule equalityE) |
|
199 |
apply (simp add: greaterThan_subset_iff order_antisym, simp) |
|
200 |
done |
|
201 |
||
202 |
lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))" |
|
203 |
by (blast intro: order_trans) |
|
204 |
||
205 |
lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" |
|
206 |
by (blast intro: order_antisym order_trans) |
|
207 |
||
208 |
lemma lessThan_subset_iff [iff]: |
|
209 |
"(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))" |
|
210 |
apply (auto simp add: lessThan_def) |
|
211 |
apply (subst linorder_not_less [symmetric], blast) |
|
212 |
apply (blast intro: order_less_le_trans) |
|
213 |
done |
|
214 |
||
215 |
lemma lessThan_eq_iff [iff]: |
|
216 |
"(lessThan x = lessThan y) = (x = (y::'a::linorder))" |
|
217 |
apply (rule iffI) |
|
218 |
apply (erule equalityE) |
|
219 |
apply (simp add: lessThan_subset_iff order_antisym, simp) |
|
13735 | 220 |
done |
221 |
||
222 |
||
13850 | 223 |
subsection {*Combined properties*} |
13735 | 224 |
|
225 |
lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" |
|
13850 | 226 |
by (blast intro: order_antisym) |
13735 | 227 |
|
13850 | 228 |
subsection {*Two-sided intervals*} |
13735 | 229 |
|
230 |
(* greaterThanLessThan *) |
|
231 |
||
232 |
lemma greaterThanLessThan_iff [simp]: |
|
233 |
"(i : {)l..u(}) = (l < i & i < u)" |
|
234 |
by (simp add: greaterThanLessThan_def) |
|
235 |
||
236 |
(* atLeastLessThan *) |
|
237 |
||
238 |
lemma atLeastLessThan_iff [simp]: |
|
239 |
"(i : {l..u(}) = (l <= i & i < u)" |
|
240 |
by (simp add: atLeastLessThan_def) |
|
241 |
||
242 |
(* greaterThanAtMost *) |
|
243 |
||
244 |
lemma greaterThanAtMost_iff [simp]: |
|
245 |
"(i : {)l..u}) = (l < i & i <= u)" |
|
246 |
by (simp add: greaterThanAtMost_def) |
|
247 |
||
248 |
(* atLeastAtMost *) |
|
249 |
||
250 |
lemma atLeastAtMost_iff [simp]: |
|
251 |
"(i : {l..u}) = (l <= i & i <= u)" |
|
252 |
by (simp add: atLeastAtMost_def) |
|
253 |
||
254 |
(* The above four lemmas could be declared as iffs. |
|
255 |
If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int |
|
256 |
seems to take forever (more than one hour). *) |
|
257 |
||
13850 | 258 |
subsection {*Lemmas useful with the summation operator setsum*} |
259 |
||
13735 | 260 |
(* For examples, see Algebra/poly/UnivPoly.thy *) |
261 |
||
262 |
(** Disjoint Unions **) |
|
263 |
||
264 |
(* Singletons and open intervals *) |
|
265 |
||
266 |
lemma ivl_disj_un_singleton: |
|
267 |
"{l::'a::linorder} Un {)l..} = {l..}" |
|
268 |
"{..u(} Un {u::'a::linorder} = {..u}" |
|
269 |
"(l::'a::linorder) < u ==> {l} Un {)l..u(} = {l..u(}" |
|
270 |
"(l::'a::linorder) < u ==> {)l..u(} Un {u} = {)l..u}" |
|
271 |
"(l::'a::linorder) <= u ==> {l} Un {)l..u} = {l..u}" |
|
272 |
"(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}" |
|
273 |
by auto (elim linorder_neqE | trans+)+ |
|
274 |
||
275 |
(* One- and two-sided intervals *) |
|
276 |
||
277 |
lemma ivl_disj_un_one: |
|
278 |
"(l::'a::linorder) < u ==> {..l} Un {)l..u(} = {..u(}" |
|
279 |
"(l::'a::linorder) <= u ==> {..l(} Un {l..u(} = {..u(}" |
|
280 |
"(l::'a::linorder) <= u ==> {..l} Un {)l..u} = {..u}" |
|
281 |
"(l::'a::linorder) <= u ==> {..l(} Un {l..u} = {..u}" |
|
282 |
"(l::'a::linorder) <= u ==> {)l..u} Un {)u..} = {)l..}" |
|
283 |
"(l::'a::linorder) < u ==> {)l..u(} Un {u..} = {)l..}" |
|
284 |
"(l::'a::linorder) <= u ==> {l..u} Un {)u..} = {l..}" |
|
285 |
"(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}" |
|
286 |
by auto trans+ |
|
287 |
||
288 |
(* Two- and two-sided intervals *) |
|
289 |
||
290 |
lemma ivl_disj_un_two: |
|
291 |
"[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u(} = {)l..u(}" |
|
292 |
"[| (l::'a::linorder) <= m; m < u |] ==> {)l..m} Un {)m..u(} = {)l..u(}" |
|
293 |
"[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u(} = {l..u(}" |
|
294 |
"[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {)m..u(} = {l..u(}" |
|
295 |
"[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u} = {)l..u}" |
|
296 |
"[| (l::'a::linorder) <= m; m <= u |] ==> {)l..m} Un {)m..u} = {)l..u}" |
|
297 |
"[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u} = {l..u}" |
|
298 |
"[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {)m..u} = {l..u}" |
|
299 |
by auto trans+ |
|
300 |
||
301 |
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two |
|
302 |
||
303 |
(** Disjoint Intersections **) |
|
304 |
||
305 |
(* Singletons and open intervals *) |
|
306 |
||
307 |
lemma ivl_disj_int_singleton: |
|
308 |
"{l::'a::order} Int {)l..} = {}" |
|
309 |
"{..u(} Int {u} = {}" |
|
310 |
"{l} Int {)l..u(} = {}" |
|
311 |
"{)l..u(} Int {u} = {}" |
|
312 |
"{l} Int {)l..u} = {}" |
|
313 |
"{l..u(} Int {u} = {}" |
|
314 |
by simp+ |
|
315 |
||
316 |
(* One- and two-sided intervals *) |
|
317 |
||
318 |
lemma ivl_disj_int_one: |
|
319 |
"{..l::'a::order} Int {)l..u(} = {}" |
|
320 |
"{..l(} Int {l..u(} = {}" |
|
321 |
"{..l} Int {)l..u} = {}" |
|
322 |
"{..l(} Int {l..u} = {}" |
|
323 |
"{)l..u} Int {)u..} = {}" |
|
324 |
"{)l..u(} Int {u..} = {}" |
|
325 |
"{l..u} Int {)u..} = {}" |
|
326 |
"{l..u(} Int {u..} = {}" |
|
327 |
by auto trans+ |
|
328 |
||
329 |
(* Two- and two-sided intervals *) |
|
330 |
||
331 |
lemma ivl_disj_int_two: |
|
332 |
"{)l::'a::order..m(} Int {m..u(} = {}" |
|
333 |
"{)l..m} Int {)m..u(} = {}" |
|
334 |
"{l..m(} Int {m..u(} = {}" |
|
335 |
"{l..m} Int {)m..u(} = {}" |
|
336 |
"{)l..m(} Int {m..u} = {}" |
|
337 |
"{)l..m} Int {)m..u} = {}" |
|
338 |
"{l..m(} Int {m..u} = {}" |
|
339 |
"{l..m} Int {)m..u} = {}" |
|
340 |
by auto trans+ |
|
341 |
||
342 |
lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two |
|
343 |
||
8924 | 344 |
end |