14 begin |
14 begin |
15 |
15 |
16 context ord |
16 context ord |
17 begin |
17 begin |
18 definition |
18 definition |
19 lessThan :: "'a => 'a set" ("(1\<^loc>{..<_})") where |
19 lessThan :: "'a => 'a set" ("(1{..<_})") where |
20 "\<^loc>{..<u} == {x. x \<^loc>< u}" |
20 "{..<u} == {x. x < u}" |
21 |
21 |
22 definition |
22 definition |
23 atMost :: "'a => 'a set" ("(1\<^loc>{.._})") where |
23 atMost :: "'a => 'a set" ("(1{.._})") where |
24 "\<^loc>{..u} == {x. x \<^loc>\<le> u}" |
24 "{..u} == {x. x \<le> u}" |
25 |
25 |
26 definition |
26 definition |
27 greaterThan :: "'a => 'a set" ("(1\<^loc>{_<..})") where |
27 greaterThan :: "'a => 'a set" ("(1{_<..})") where |
28 "\<^loc>{l<..} == {x. l\<^loc><x}" |
28 "{l<..} == {x. l<x}" |
29 |
29 |
30 definition |
30 definition |
31 atLeast :: "'a => 'a set" ("(1\<^loc>{_..})") where |
31 atLeast :: "'a => 'a set" ("(1{_..})") where |
32 "\<^loc>{l..} == {x. l\<^loc>\<le>x}" |
32 "{l..} == {x. l\<le>x}" |
33 |
33 |
34 definition |
34 definition |
35 greaterThanLessThan :: "'a => 'a => 'a set" ("(1\<^loc>{_<..<_})") where |
35 greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where |
36 "\<^loc>{l<..<u} == \<^loc>{l<..} Int \<^loc>{..<u}" |
36 "{l<..<u} == {l<..} Int {..<u}" |
37 |
37 |
38 definition |
38 definition |
39 atLeastLessThan :: "'a => 'a => 'a set" ("(1\<^loc>{_..<_})") where |
39 atLeastLessThan :: "'a => 'a => 'a set" ("(1{_..<_})") where |
40 "\<^loc>{l..<u} == \<^loc>{l..} Int \<^loc>{..<u}" |
40 "{l..<u} == {l..} Int {..<u}" |
41 |
41 |
42 definition |
42 definition |
43 greaterThanAtMost :: "'a => 'a => 'a set" ("(1\<^loc>{_<.._})") where |
43 greaterThanAtMost :: "'a => 'a => 'a set" ("(1{_<.._})") where |
44 "\<^loc>{l<..u} == \<^loc>{l<..} Int \<^loc>{..u}" |
44 "{l<..u} == {l<..} Int {..u}" |
45 |
45 |
46 definition |
46 definition |
47 atLeastAtMost :: "'a => 'a => 'a set" ("(1\<^loc>{_.._})") where |
47 atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where |
48 "\<^loc>{l..u} == \<^loc>{l..} Int \<^loc>{..u}" |
48 "{l..u} == {l..} Int {..u}" |
49 |
49 |
50 end |
50 end |
51 (* |
51 (* |
52 constdefs |
52 constdefs |
53 lessThan :: "('a::ord) => 'a set" ("(1{..<_})") |
53 lessThan :: "('a::ord) => 'a set" ("(1{..<_})") |
104 "INT i<n. A" == "INT i:{..<n}. A" |
104 "INT i<n. A" == "INT i:{..<n}. A" |
105 |
105 |
106 |
106 |
107 subsection {* Various equivalences *} |
107 subsection {* Various equivalences *} |
108 |
108 |
109 lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i\<^loc><k)" |
109 lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i<k)" |
110 by (simp add: lessThan_def) |
110 by (simp add: lessThan_def) |
111 |
111 |
112 lemma Compl_lessThan [simp]: |
112 lemma Compl_lessThan [simp]: |
113 "!!k:: 'a::linorder. -lessThan k = atLeast k" |
113 "!!k:: 'a::linorder. -lessThan k = atLeast k" |
114 apply (auto simp add: lessThan_def atLeast_def) |
114 apply (auto simp add: lessThan_def atLeast_def) |
115 done |
115 done |
116 |
116 |
117 lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}" |
117 lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}" |
118 by auto |
118 by auto |
119 |
119 |
120 lemma (in ord) greaterThan_iff [iff]: "(i: greaterThan k) = (k\<^loc><i)" |
120 lemma (in ord) greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)" |
121 by (simp add: greaterThan_def) |
121 by (simp add: greaterThan_def) |
122 |
122 |
123 lemma Compl_greaterThan [simp]: |
123 lemma Compl_greaterThan [simp]: |
124 "!!k:: 'a::linorder. -greaterThan k = atMost k" |
124 "!!k:: 'a::linorder. -greaterThan k = atMost k" |
125 apply (simp add: greaterThan_def atMost_def le_def, auto) |
125 apply (simp add: greaterThan_def atMost_def le_def, auto) |
128 lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k" |
128 lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k" |
129 apply (subst Compl_greaterThan [symmetric]) |
129 apply (subst Compl_greaterThan [symmetric]) |
130 apply (rule double_complement) |
130 apply (rule double_complement) |
131 done |
131 done |
132 |
132 |
133 lemma (in ord) atLeast_iff [iff]: "(i: atLeast k) = (k\<^loc><=i)" |
133 lemma (in ord) atLeast_iff [iff]: "(i: atLeast k) = (k<=i)" |
134 by (simp add: atLeast_def) |
134 by (simp add: atLeast_def) |
135 |
135 |
136 lemma Compl_atLeast [simp]: |
136 lemma Compl_atLeast [simp]: |
137 "!!k:: 'a::linorder. -atLeast k = lessThan k" |
137 "!!k:: 'a::linorder. -atLeast k = lessThan k" |
138 apply (simp add: lessThan_def atLeast_def le_def, auto) |
138 apply (simp add: lessThan_def atLeast_def le_def, auto) |
139 done |
139 done |
140 |
140 |
141 lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i\<^loc><=k)" |
141 lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i<=k)" |
142 by (simp add: atMost_def) |
142 by (simp add: atMost_def) |
143 |
143 |
144 lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" |
144 lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" |
145 by (blast intro: order_antisym) |
145 by (blast intro: order_antisym) |
146 |
146 |
192 |
192 |
193 context ord |
193 context ord |
194 begin |
194 begin |
195 |
195 |
196 lemma greaterThanLessThan_iff [simp,noatp]: |
196 lemma greaterThanLessThan_iff [simp,noatp]: |
197 "(i : \<^loc>{l<..<u}) = (l \<^loc>< i & i \<^loc>< u)" |
197 "(i : {l<..<u}) = (l < i & i < u)" |
198 by (simp add: greaterThanLessThan_def) |
198 by (simp add: greaterThanLessThan_def) |
199 |
199 |
200 lemma atLeastLessThan_iff [simp,noatp]: |
200 lemma atLeastLessThan_iff [simp,noatp]: |
201 "(i : \<^loc>{l..<u}) = (l \<^loc><= i & i \<^loc>< u)" |
201 "(i : {l..<u}) = (l <= i & i < u)" |
202 by (simp add: atLeastLessThan_def) |
202 by (simp add: atLeastLessThan_def) |
203 |
203 |
204 lemma greaterThanAtMost_iff [simp,noatp]: |
204 lemma greaterThanAtMost_iff [simp,noatp]: |
205 "(i : \<^loc>{l<..u}) = (l \<^loc>< i & i \<^loc><= u)" |
205 "(i : {l<..u}) = (l < i & i <= u)" |
206 by (simp add: greaterThanAtMost_def) |
206 by (simp add: greaterThanAtMost_def) |
207 |
207 |
208 lemma atLeastAtMost_iff [simp,noatp]: |
208 lemma atLeastAtMost_iff [simp,noatp]: |
209 "(i : \<^loc>{l..u}) = (l \<^loc><= i & i \<^loc><= u)" |
209 "(i : {l..u}) = (l <= i & i <= u)" |
210 by (simp add: atLeastAtMost_def) |
210 by (simp add: atLeastAtMost_def) |
211 |
211 |
212 text {* The above four lemmas could be declared as iffs. |
212 text {* The above four lemmas could be declared as iffs. |
213 If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int} |
213 If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int} |
214 seems to take forever (more than one hour). *} |
214 seems to take forever (more than one hour). *} |
217 subsubsection{* Emptyness and singletons *} |
217 subsubsection{* Emptyness and singletons *} |
218 |
218 |
219 context order |
219 context order |
220 begin |
220 begin |
221 |
221 |
222 lemma atLeastAtMost_empty [simp]: "n \<^loc>< m ==> \<^loc>{m..n} = {}"; |
222 lemma atLeastAtMost_empty [simp]: "n < m ==> {m..n} = {}"; |
223 by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) |
223 by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) |
224 |
224 |
225 lemma atLeastLessThan_empty[simp]: "n \<^loc>\<le> m ==> \<^loc>{m..<n} = {}" |
225 lemma atLeastLessThan_empty[simp]: "n \<le> m ==> {m..<n} = {}" |
226 by (auto simp add: atLeastLessThan_def) |
226 by (auto simp add: atLeastLessThan_def) |
227 |
227 |
228 lemma greaterThanAtMost_empty[simp]:"l \<^loc>\<le> k ==> \<^loc>{k<..l} = {}" |
228 lemma greaterThanAtMost_empty[simp]:"l \<le> k ==> {k<..l} = {}" |
229 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) |
229 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) |
230 |
230 |
231 lemma greaterThanLessThan_empty[simp]:"l \<^loc>\<le> k ==> \<^loc>{k<..l} = {}" |
231 lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..l} = {}" |
232 by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def) |
232 by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def) |
233 |
233 |
234 lemma atLeastAtMost_singleton [simp]: "\<^loc>{a..a} = {a}" |
234 lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}" |
235 by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) |
235 by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) |
236 |
236 |
237 end |
237 end |
238 |
238 |
239 subsection {* Intervals of natural numbers *} |
239 subsection {* Intervals of natural numbers *} |