author  ballarin 
Thu, 28 Nov 2002 10:50:42 +0100  
changeset 13735  7de9342aca7a 
parent 11609  3f3d1add4d94 
child 13850  6d1bb3059818 
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 

36 
(* Setup of transitivity reasoner *) 

37 

38 
ML {* 

39 

40 
structure Trans_Tac = Trans_Tac_Fun ( 

41 
struct 

42 
val less_reflE = thm "order_less_irrefl" RS thm "notE"; 

43 
val le_refl = thm "order_refl"; 

44 
val less_imp_le = thm "order_less_imp_le"; 

45 
val not_lessI = thm "linorder_not_less" RS thm "iffD2"; 

46 
val not_leI = thm "linorder_not_less" RS thm "iffD2"; 

47 
val not_lessD = thm "linorder_not_less" RS thm "iffD1"; 

48 
val not_leD = thm "linorder_not_le" RS thm "iffD1"; 

49 
val eqI = thm "order_antisym"; 

50 
val eqD1 = thm "order_eq_refl"; 

51 
val eqD2 = thm "sym" RS thm "order_eq_refl"; 

52 
val less_trans = thm "order_less_trans"; 

53 
val less_le_trans = thm "order_less_le_trans"; 

54 
val le_less_trans = thm "order_le_less_trans"; 

55 
val le_trans = thm "order_trans"; 

56 
fun decomp (Trueprop $ t) = 

57 
let fun dec (Const ("Not", _) $ t) = ( 

58 
case dec t of 

59 
None => None 

60 
 Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2)) 

61 
 dec (Const (rel, _) $ t1 $ t2) = 

62 
Some (t1, implode (drop (3, explode rel)), t2) 

63 
 dec _ = None 

64 
in dec t end 

65 
 decomp _ = None 

66 
end); 

67 

68 
val trans_tac = Trans_Tac.trans_tac; 

69 

70 
*} 

71 

72 
method_setup trans = 

73 
{* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac)) *} 

74 
{* simple transitivity reasoner *} 

75 

76 
(*** lessThan ***) 

77 

78 
lemma lessThan_iff: "(i: lessThan k) = (i<k)" 

79 

80 
apply (unfold lessThan_def) 

81 
apply blast 

82 
done 

83 
declare lessThan_iff [iff] 

84 

85 
lemma lessThan_0: "lessThan (0::nat) = {}" 

86 
apply (unfold lessThan_def) 

87 
apply (simp (no_asm)) 

88 
done 

89 
declare lessThan_0 [simp] 

90 

91 
lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)" 

92 
apply (unfold lessThan_def) 

93 
apply (simp (no_asm) add: less_Suc_eq) 

94 
apply blast 

95 
done 

96 

97 
lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k" 

98 
apply (unfold lessThan_def atMost_def) 

99 
apply (simp (no_asm) add: less_Suc_eq_le) 

100 
done 

101 

102 
lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV" 

103 
apply blast 

104 
done 

105 

106 
lemma Compl_lessThan: 

107 
"!!k:: 'a::linorder. lessThan k = atLeast k" 

108 
apply (unfold lessThan_def atLeast_def) 

109 
apply auto 

110 
apply (blast intro: linorder_not_less [THEN iffD1]) 

111 
apply (blast dest: order_le_less_trans) 

112 
done 

113 

114 
lemma single_Diff_lessThan: "!!k:: 'a::order. {k}  lessThan k = {k}" 

115 
apply auto 

116 
done 

117 
declare single_Diff_lessThan [simp] 

118 

119 
(*** greaterThan ***) 

120 

121 
lemma greaterThan_iff: "(i: greaterThan k) = (k<i)" 

122 

123 
apply (unfold greaterThan_def) 

124 
apply blast 

125 
done 

126 
declare greaterThan_iff [iff] 

127 

128 
lemma greaterThan_0: "greaterThan 0 = range Suc" 

129 
apply (unfold greaterThan_def) 

130 
apply (blast dest: gr0_conv_Suc [THEN iffD1]) 

131 
done 

132 
declare greaterThan_0 [simp] 

133 

134 
lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k  {Suc k}" 

135 
apply (unfold greaterThan_def) 

136 
apply (auto elim: linorder_neqE) 

137 
done 

138 

139 
lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}" 

140 
apply blast 

141 
done 

142 

143 
lemma Compl_greaterThan: 

144 
"!!k:: 'a::linorder. greaterThan k = atMost k" 

145 
apply (unfold greaterThan_def atMost_def le_def) 

146 
apply auto 

147 
apply (blast intro: linorder_not_less [THEN iffD1]) 

148 
apply (blast dest: order_le_less_trans) 

149 
done 

150 

151 
lemma Compl_atMost: "!!k:: 'a::linorder. atMost k = greaterThan k" 

152 
apply (simp (no_asm) add: Compl_greaterThan [symmetric]) 

153 
done 

154 

155 
declare Compl_greaterThan [simp] Compl_atMost [simp] 

156 

157 
(*** atLeast ***) 

158 

159 
lemma atLeast_iff: "(i: atLeast k) = (k<=i)" 

160 

161 
apply (unfold atLeast_def) 

162 
apply blast 

163 
done 

164 
declare atLeast_iff [iff] 

165 

166 
lemma atLeast_0: "atLeast (0::nat) = UNIV" 

167 
apply (unfold atLeast_def UNIV_def) 

168 
apply (simp (no_asm)) 

169 
done 

170 
declare atLeast_0 [simp] 

171 

172 
lemma atLeast_Suc: "atLeast (Suc k) = atLeast k  {k}" 

173 
apply (unfold atLeast_def) 

174 
apply (simp (no_asm) add: Suc_le_eq) 

175 
apply (simp (no_asm) add: order_le_less) 

176 
apply blast 

177 
done 

178 

179 
lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV" 

180 
apply blast 

181 
done 

182 

183 
lemma Compl_atLeast: 

184 
"!!k:: 'a::linorder. atLeast k = lessThan k" 

185 
apply (unfold lessThan_def atLeast_def le_def) 

186 
apply auto 

187 
apply (blast intro: linorder_not_less [THEN iffD1]) 

188 
apply (blast dest: order_le_less_trans) 

189 
done 

190 

191 
declare Compl_lessThan [simp] Compl_atLeast [simp] 

192 

193 
(*** atMost ***) 

194 

195 
lemma atMost_iff: "(i: atMost k) = (i<=k)" 

196 

197 
apply (unfold atMost_def) 

198 
apply blast 

199 
done 

200 
declare atMost_iff [iff] 

201 

202 
lemma atMost_0: "atMost (0::nat) = {0}" 

203 
apply (unfold atMost_def) 

204 
apply (simp (no_asm)) 

205 
done 

206 
declare atMost_0 [simp] 

207 

208 
lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)" 

209 
apply (unfold atMost_def) 

210 
apply (simp (no_asm) add: less_Suc_eq order_le_less) 

211 
apply blast 

212 
done 

213 

214 
lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV" 

215 
apply blast 

216 
done 

217 

218 

219 
(*** Combined properties ***) 

220 

221 
lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" 

222 
apply (blast intro: order_antisym) 

223 
done 

224 

225 
(*** Twosided intervals ***) 

226 

227 
(* greaterThanLessThan *) 

228 

229 
lemma greaterThanLessThan_iff [simp]: 

230 
"(i : {)l..u(}) = (l < i & i < u)" 

231 
by (simp add: greaterThanLessThan_def) 

232 

233 
(* atLeastLessThan *) 

234 

235 
lemma atLeastLessThan_iff [simp]: 

236 
"(i : {l..u(}) = (l <= i & i < u)" 

237 
by (simp add: atLeastLessThan_def) 

238 

239 
(* greaterThanAtMost *) 

240 

241 
lemma greaterThanAtMost_iff [simp]: 

242 
"(i : {)l..u}) = (l < i & i <= u)" 

243 
by (simp add: greaterThanAtMost_def) 

244 

245 
(* atLeastAtMost *) 

246 

247 
lemma atLeastAtMost_iff [simp]: 

248 
"(i : {l..u}) = (l <= i & i <= u)" 

249 
by (simp add: atLeastAtMost_def) 

250 

251 
(* The above four lemmas could be declared as iffs. 

252 
If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int 

253 
seems to take forever (more than one hour). *) 

254 

255 
(*** The following lemmas are useful with the summation operator setsum ***) 

256 
(* For examples, see Algebra/poly/UnivPoly.thy *) 

257 

258 
(** Disjoint Unions **) 

259 

260 
(* Singletons and open intervals *) 

261 

262 
lemma ivl_disj_un_singleton: 

263 
"{l::'a::linorder} Un {)l..} = {l..}" 

264 
"{..u(} Un {u::'a::linorder} = {..u}" 

265 
"(l::'a::linorder) < u ==> {l} Un {)l..u(} = {l..u(}" 

266 
"(l::'a::linorder) < u ==> {)l..u(} Un {u} = {)l..u}" 

267 
"(l::'a::linorder) <= u ==> {l} Un {)l..u} = {l..u}" 

268 
"(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}" 

269 
by auto (elim linorder_neqE  trans+)+ 

270 

271 
(* One and twosided intervals *) 

272 

273 
lemma ivl_disj_un_one: 

274 
"(l::'a::linorder) < u ==> {..l} Un {)l..u(} = {..u(}" 

275 
"(l::'a::linorder) <= u ==> {..l(} Un {l..u(} = {..u(}" 

276 
"(l::'a::linorder) <= u ==> {..l} Un {)l..u} = {..u}" 

277 
"(l::'a::linorder) <= u ==> {..l(} Un {l..u} = {..u}" 

278 
"(l::'a::linorder) <= u ==> {)l..u} Un {)u..} = {)l..}" 

279 
"(l::'a::linorder) < u ==> {)l..u(} Un {u..} = {)l..}" 

280 
"(l::'a::linorder) <= u ==> {l..u} Un {)u..} = {l..}" 

281 
"(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}" 

282 
by auto trans+ 

283 

284 
(* Two and twosided intervals *) 

285 

286 
lemma ivl_disj_un_two: 

287 
"[ (l::'a::linorder) < m; m <= u ] ==> {)l..m(} Un {m..u(} = {)l..u(}" 

288 
"[ (l::'a::linorder) <= m; m < u ] ==> {)l..m} Un {)m..u(} = {)l..u(}" 

289 
"[ (l::'a::linorder) <= m; m <= u ] ==> {l..m(} Un {m..u(} = {l..u(}" 

290 
"[ (l::'a::linorder) <= m; m < u ] ==> {l..m} Un {)m..u(} = {l..u(}" 

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 
by auto trans+ 

296 

297 
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two 

298 

299 
(** Disjoint Intersections **) 

300 

301 
(* Singletons and open intervals *) 

302 

303 
lemma ivl_disj_int_singleton: 

304 
"{l::'a::order} Int {)l..} = {}" 

305 
"{..u(} Int {u} = {}" 

306 
"{l} Int {)l..u(} = {}" 

307 
"{)l..u(} Int {u} = {}" 

308 
"{l} Int {)l..u} = {}" 

309 
"{l..u(} Int {u} = {}" 

310 
by simp+ 

311 

312 
(* One and twosided intervals *) 

313 

314 
lemma ivl_disj_int_one: 

315 
"{..l::'a::order} Int {)l..u(} = {}" 

316 
"{..l(} Int {l..u(} = {}" 

317 
"{..l} Int {)l..u} = {}" 

318 
"{..l(} Int {l..u} = {}" 

319 
"{)l..u} Int {)u..} = {}" 

320 
"{)l..u(} Int {u..} = {}" 

321 
"{l..u} Int {)u..} = {}" 

322 
"{l..u(} Int {u..} = {}" 

323 
by auto trans+ 

324 

325 
(* Two and twosided intervals *) 

326 

327 
lemma ivl_disj_int_two: 

328 
"{)l::'a::order..m(} Int {m..u(} = {}" 

329 
"{)l..m} Int {)m..u(} = {}" 

330 
"{l..m(} Int {m..u(} = {}" 

331 
"{l..m} Int {)m..u(} = {}" 

332 
"{)l..m(} Int {m..u} = {}" 

333 
"{)l..m} Int {)m..u} = {}" 

334 
"{l..m(} Int {m..u} = {}" 

335 
"{l..m} Int {)m..u} = {}" 

336 
by auto trans+ 

337 

338 
lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two 

339 

8924  340 
end 