author  paulson 
Thu, 06 Mar 2003 15:03:16 +0100  
changeset 13850  6d1bb3059818 
parent 13735  7de9342aca7a 
child 14398  c5c47703f763 
permissions  rwrr 
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 twosided 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 {*Twosided 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 twosided 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 twosided 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 twosided 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 twosided 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 