author  nipkow 
Mon, 21 Feb 2005 19:23:46 +0100  
changeset 15542  ee6cd48cf840 
parent 15539  333a88244569 
child 15554  03d4347b071d 
permissions  rwrr 
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 twosided 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 {*Twosided 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 {..<ul}") 

14485  345 
apply (erule ssubst, rule card_lessThan) 
15045  346 
apply (subgoal_tac "(%x. x + l) ` {..<ul} = {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..<ul} = {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..<ul} = {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..<ul}") 

14485  431 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 
15045  432 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {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, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

466 
by auto 
13735  467 

14577  468 
text {* One and twosided 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, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

479 
by auto 
13735  480 

14577  481 
text {* Two and twosided 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, graphbased 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 twosided 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, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

520 
by auto 
13735  521 

14577  522 
text {* Two and twosided 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, graphbased 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 

15542  537 
subsubsection {* Some Differences *} 
538 

539 
lemma ivl_diff[simp]: 

540 
"i \<le> n \<Longrightarrow> {i..<m}  {i..<n} = {n..<(m::'a::linorder)}" 

541 
by(auto) 

542 

543 

544 
subsubsection {* Some Subset Conditions *} 

545 

546 
lemma ivl_subset[simp]: 

547 
"({i..<j} \<subseteq> {m..<n}) = (j \<le> i  m \<le> i & j \<le> (n::'a::linorder))" 

548 
apply(auto simp:linorder_not_le) 

549 
apply(rule ccontr) 

550 
apply(insert linorder_le_less_linear[of i n]) 

551 
apply(clarsimp simp:linorder_not_le) 

552 
apply(fastsimp) 

553 
done 

554 

15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

555 

15042  556 
subsection {* Summation indexed over intervals *} 
557 

558 
syntax 

559 
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) 

15048  560 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) 
561 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10) 

15042  562 
syntax (xsymbols) 
563 
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) 

15048  564 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) 
565 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) 

15042  566 
syntax (HTML output) 
567 
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) 

15048  568 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) 
569 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) 

15056  570 
syntax (latex_sum output) 
15052  571 
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
572 
("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) 

573 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 

574 
("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) 

575 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 

576 
("(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

577 

15048  578 
translations 
579 
"\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}" 

580 
"\<Sum>x=a..<b. t" == "setsum (%x. t) {a..<b}" 

581 
"\<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

582 

15052  583 
text{* The above introduces some pretty alternative syntaxes for 
15056  584 
summation over intervals: 
15052  585 
\begin{center} 
586 
\begin{tabular}{lll} 

15056  587 
Old & New & \LaTeX\\ 
588 
@{term[source]"\<Sum>x\<in>{a..b}. e"} & @{term"\<Sum>x=a..b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..b. e"}\\ 

589 
@{term[source]"\<Sum>x\<in>{a..<b}. e"} & @{term"\<Sum>x=a..<b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..<b. e"}\\ 

590 
@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"} 

15052  591 
\end{tabular} 
592 
\end{center} 

15056  593 
The left column shows the term before introduction of the new syntax, 
594 
the middle column shows the new (default) syntax, and the right column 

595 
shows a special syntax. The latter is only meaningful for latex output 

596 
and has to be activated explicitly by setting the print mode to 

597 
\texttt{latex\_sum} (e.g.\ via \texttt{mode=latex\_sum} in 

598 
antiquotations). It is not the default \LaTeX\ output because it only 

599 
works well with italicstyle formulae, not ttstyle. 

15052  600 

601 
Note that for uniformity on @{typ nat} it is better to use 

602 
@{term"\<Sum>x::nat=0..<n. e"} rather than @{text"\<Sum>x<n. e"}: @{text setsum} may 

603 
not provide all lemmas available for @{term"{m..<n}"} also in the 

604 
special form for @{term"{..<n}"}. *} 

605 

15542  606 
(* FIXME change the simplifier's treatment of congruence rules?? *) 
607 

608 
text{* This congruence rule should be used for sums over intervals as 

609 
the standard theorem @{text[source]setsum_cong} does not work well 

610 
with the simplifier who adds the unsimplified premise @{term"x:B"} to 

611 
the context. *} 

612 

613 
lemma setsum_ivl_cong: 

614 
"\<lbrakk>a = c; b = d; !!x. \<lbrakk> c \<le> x; x < d \<rbrakk> \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> 

615 
setsum f {a..<b} = setsum g {c..<d}" 

616 
by(rule setsum_cong, simp_all) 

15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

617 

a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

618 
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

619 
by (simp add:lessThan_Suc) 
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

620 

15539  621 
lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> 
622 
setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}" 

623 
by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un) 

624 

625 
lemma setsum_diff_nat_ivl: 

626 
fixes f :: "nat \<Rightarrow> 'a::ab_group_add" 

627 
shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> 

628 
setsum f {m..<p}  setsum f {m..<n} = setsum f {n..<p}" 

629 
using setsum_add_nat_ivl [of m n p f,symmetric] 

630 
apply (simp add: add_ac) 

631 
done 

632 

633 
lemma setsum_shift_bounds_nat_ivl: 

634 
"setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}" 

635 
by (induct "n", auto simp:atLeastLessThanSuc) 

636 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

637 

e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

638 
ML 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

639 
{* 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

640 
val Compl_atLeast = thm "Compl_atLeast"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

641 
val Compl_atMost = thm "Compl_atMost"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

642 
val Compl_greaterThan = thm "Compl_greaterThan"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

643 
val Compl_lessThan = thm "Compl_lessThan"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

644 
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

645 
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

646 
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

647 
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

648 
val atLeastAtMost_def = thm "atLeastAtMost_def"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

649 
val atLeastAtMost_iff = thm "atLeastAtMost_iff"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

650 
val atLeastLessThan_def = thm "atLeastLessThan_def"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

651 
val atLeastLessThan_iff = thm "atLeastLessThan_iff"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

652 
val atLeast_0 = thm "atLeast_0"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

653 
val atLeast_Suc = thm "atLeast_Suc"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

654 
val atLeast_def = thm "atLeast_def"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

655 
val atLeast_iff = thm "atLeast_iff"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

656 
val atMost_0 = thm "atMost_0"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

657 
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

658 
val atMost_Suc = thm "atMost_Suc"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

659 
val atMost_def = thm "atMost_def"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

660 
val atMost_iff = thm "atMost_iff"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

661 
val greaterThanAtMost_def = thm "greaterThanAtMost_def"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

662 
val greaterThanAtMost_iff = thm "greaterThanAtMost_iff"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

663 
val greaterThanLessThan_def = thm "greaterThanLessThan_def"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

664 
val greaterThanLessThan_iff = thm "greaterThanLessThan_iff"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

665 
val greaterThan_0 = thm "greaterThan_0"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

666 
val greaterThan_Suc = thm "greaterThan_Suc"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

667 
val greaterThan_def = thm "greaterThan_def"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

668 
val greaterThan_iff = thm "greaterThan_iff"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

669 
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

670 
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

671 
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

672 
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

673 
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

674 
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

675 
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

676 
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

677 
val lessThan_0 = thm "lessThan_0"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

678 
val lessThan_Suc = thm "lessThan_Suc"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

679 
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

680 
val lessThan_def = thm "lessThan_def"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

681 
val lessThan_iff = thm "lessThan_iff"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

682 
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

683 

e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

684 
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

685 
val finite_atMost = thm "finite_atMost"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

686 
val finite_lessThan = thm "finite_lessThan"; 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

687 
*} 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

688 

8924  689 
end 