author  nipkow 
Mon, 24 Sep 2007 19:34:55 +0200  
changeset 24691  e7f46ee04809 
parent 24449  2f05cb7fed85 
child 24748  ee0a0eb6b738 
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 

24691  16 
context ord 
17 
begin 

18 
definition 

19 
lessThan :: "'a => 'a set" ("(1\<^loc>{..<_})") where 

20 
"\<^loc>{..<u} == {x. x \<sqsubset> u}" 

21 

22 
definition 

23 
atMost :: "'a => 'a set" ("(1\<^loc>{.._})") where 

24 
"\<^loc>{..u} == {x. x \<sqsubseteq> u}" 

25 

26 
definition 

27 
greaterThan :: "'a => 'a set" ("(1\<^loc>{_<..})") where 

28 
"\<^loc>{l<..} == {x. l\<sqsubset>x}" 

29 

30 
definition 

31 
atLeast :: "'a => 'a set" ("(1\<^loc>{_..})") where 

32 
"\<^loc>{l..} == {x. l\<sqsubseteq>x}" 

33 

34 
definition 

35 
greaterThanLessThan :: "'a => 'a => 'a set" ("(1\<^loc>{_<..<_})") where 

36 
"\<^loc>{l<..<u} == \<^loc>{l<..} Int \<^loc>{..<u}" 

37 

38 
definition 

39 
atLeastLessThan :: "'a => 'a => 'a set" ("(1\<^loc>{_..<_})") where 

40 
"\<^loc>{l..<u} == \<^loc>{l..} Int \<^loc>{..<u}" 

41 

42 
definition 

43 
greaterThanAtMost :: "'a => 'a => 'a set" ("(1\<^loc>{_<.._})") where 

44 
"\<^loc>{l<..u} == \<^loc>{l<..} Int \<^loc>{..u}" 

45 

46 
definition 

47 
atLeastAtMost :: "'a => 'a => 'a set" ("(1\<^loc>{_.._})") where 

48 
"\<^loc>{l..u} == \<^loc>{l..} Int \<^loc>{..u}" 

49 

50 
end 

51 
(* 

8924  52 
constdefs 
15045  53 
lessThan :: "('a::ord) => 'a set" ("(1{..<_})") 
54 
"{..<u} == {x. x<u}" 

8924  55 

11609
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset

56 
atMost :: "('a::ord) => 'a set" ("(1{.._})") 
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset

57 
"{..u} == {x. x<=u}" 
8924  58 

15045  59 
greaterThan :: "('a::ord) => 'a set" ("(1{_<..})") 
60 
"{l<..} == {x. l<x}" 

8924  61 

11609
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset

62 
atLeast :: "('a::ord) => 'a set" ("(1{_..})") 
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset

63 
"{l..} == {x. l<=x}" 
8924  64 

15045  65 
greaterThanLessThan :: "['a::ord, 'a] => 'a set" ("(1{_<..<_})") 
66 
"{l<..<u} == {l<..} Int {..<u}" 

13735  67 

15045  68 
atLeastLessThan :: "['a::ord, 'a] => 'a set" ("(1{_..<_})") 
69 
"{l..<u} == {l..} Int {..<u}" 

13735  70 

15045  71 
greaterThanAtMost :: "['a::ord, 'a] => 'a set" ("(1{_<.._})") 
72 
"{l<..u} == {l<..} Int {..u}" 

13735  73 

74 
atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})") 

75 
"{l..u} == {l..} Int {..u}" 

24691  76 
*) 
13735  77 

15048  78 
text{* A note of warning when using @{term"{..<n}"} on type @{typ 
79 
nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving 

15052  80 
@{term"{m..<n}"} may not exist in @{term"{..<n}"}form as well. *} 
15048  81 

14418  82 
syntax 
83 
"@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3UN _<=_./ _)" 10) 

84 
"@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3UN _<_./ _)" 10) 

85 
"@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3INT _<=_./ _)" 10) 

86 
"@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3INT _<_./ _)" 10) 

87 

88 
syntax (input) 

89 
"@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3\<Union> _\<le>_./ _)" 10) 

90 
"@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3\<Union> _<_./ _)" 10) 

91 
"@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3\<Inter> _\<le>_./ _)" 10) 

92 
"@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\<Inter> _<_./ _)" 10) 

93 

94 
syntax (xsymbols) 

14846  95 
"@UNION_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10) 
96 
"@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_ < _\<^esub>)/ _)" 10) 

97 
"@INTER_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10) 

98 
"@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_ < _\<^esub>)/ _)" 10) 

14418  99 

100 
translations 

101 
"UN i<=n. A" == "UN i:{..n}. A" 

15045  102 
"UN i<n. A" == "UN i:{..<n}. A" 
14418  103 
"INT i<=n. A" == "INT i:{..n}. A" 
15045  104 
"INT i<n. A" == "INT i:{..<n}. A" 
14418  105 

106 

14485  107 
subsection {* Various equivalences *} 
13735  108 

24691  109 
lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i\<^loc><k)" 
13850  110 
by (simp add: lessThan_def) 
13735  111 

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

112 
lemma Compl_lessThan [simp]: 
13735  113 
"!!k:: 'a::linorder. lessThan k = atLeast k" 
13850  114 
apply (auto simp add: lessThan_def atLeast_def) 
13735  115 
done 
116 

13850  117 
lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k}  lessThan k = {k}" 
118 
by auto 

13735  119 

24691  120 
lemma (in ord) greaterThan_iff [iff]: "(i: greaterThan k) = (k\<^loc><i)" 
13850  121 
by (simp add: greaterThan_def) 
13735  122 

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

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 
done 
127 

13850  128 
lemma Compl_atMost [simp]: "!!k:: 'a::linorder. atMost k = greaterThan k" 
129 
apply (subst Compl_greaterThan [symmetric]) 

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

130 
apply (rule double_complement) 
13735  131 
done 
132 

24691  133 
lemma (in ord) atLeast_iff [iff]: "(i: atLeast k) = (k\<^loc><=i)" 
13850  134 
by (simp add: atLeast_def) 
13735  135 

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

136 
lemma Compl_atLeast [simp]: 
13735  137 
"!!k:: 'a::linorder. atLeast k = lessThan k" 
13850  138 
apply (simp add: lessThan_def atLeast_def le_def, auto) 
13735  139 
done 
140 

24691  141 
lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i\<^loc><=k)" 
13850  142 
by (simp add: atMost_def) 
13735  143 

14485  144 
lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" 
145 
by (blast intro: order_antisym) 

13850  146 

147 

14485  148 
subsection {* Logical Equivalences for Set Inclusion and Equality *} 
13850  149 

150 
lemma atLeast_subset_iff [iff]: 

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

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

152 
by (blast intro: order_trans) 
13850  153 

154 
lemma atLeast_eq_iff [iff]: 

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

155 
"(atLeast x = atLeast y) = (x = (y::'a::linorder))" 
13850  156 
by (blast intro: order_antisym order_trans) 
157 

158 
lemma greaterThan_subset_iff [iff]: 

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

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

160 
apply (auto simp add: greaterThan_def) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

161 
apply (subst linorder_not_less [symmetric], blast) 
13850  162 
done 
163 

164 
lemma greaterThan_eq_iff [iff]: 

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

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

166 
apply (rule iffI) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

167 
apply (erule equalityE) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

168 
apply (simp_all add: greaterThan_subset_iff) 
13850  169 
done 
170 

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

171 
lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))" 
13850  172 
by (blast intro: order_trans) 
173 

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

174 
lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" 
13850  175 
by (blast intro: order_antisym order_trans) 
176 

177 
lemma lessThan_subset_iff [iff]: 

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

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

179 
apply (auto simp add: lessThan_def) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

180 
apply (subst linorder_not_less [symmetric], blast) 
13850  181 
done 
182 

183 
lemma lessThan_eq_iff [iff]: 

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

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

185 
apply (rule iffI) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

186 
apply (erule equalityE) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

187 
apply (simp_all add: lessThan_subset_iff) 
13735  188 
done 
189 

190 

13850  191 
subsection {*Twosided intervals*} 
13735  192 

24691  193 
context ord 
194 
begin 

195 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23496
diff
changeset

196 
lemma greaterThanLessThan_iff [simp,noatp]: 
24691  197 
"(i : \<^loc>{l<..<u}) = (l \<^loc>< i & i \<^loc>< u)" 
13735  198 
by (simp add: greaterThanLessThan_def) 
199 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23496
diff
changeset

200 
lemma atLeastLessThan_iff [simp,noatp]: 
24691  201 
"(i : \<^loc>{l..<u}) = (l \<^loc><= i & i \<^loc>< u)" 
13735  202 
by (simp add: atLeastLessThan_def) 
203 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23496
diff
changeset

204 
lemma greaterThanAtMost_iff [simp,noatp]: 
24691  205 
"(i : \<^loc>{l<..u}) = (l \<^loc>< i & i \<^loc><= u)" 
13735  206 
by (simp add: greaterThanAtMost_def) 
207 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23496
diff
changeset

208 
lemma atLeastAtMost_iff [simp,noatp]: 
24691  209 
"(i : \<^loc>{l..u}) = (l \<^loc><= i & i \<^loc><= u)" 
13735  210 
by (simp add: atLeastAtMost_def) 
211 

14577  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} 

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

24691  215 
end 
13735  216 

15554  217 
subsubsection{* Emptyness and singletons *} 
218 

24691  219 
context order 
220 
begin 

15554  221 

24691  222 
lemma atLeastAtMost_empty [simp]: "n \<^loc>< m ==> \<^loc>{m..n} = {}"; 
223 
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) 

224 

225 
lemma atLeastLessThan_empty[simp]: "n \<^loc>\<le> m ==> \<^loc>{m..<n} = {}" 

15554  226 
by (auto simp add: atLeastLessThan_def) 
227 

24691  228 
lemma greaterThanAtMost_empty[simp]:"l \<^loc>\<le> k ==> \<^loc>{k<..l} = {}" 
17719  229 
by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) 
230 

24691  231 
lemma greaterThanLessThan_empty[simp]:"l \<^loc>\<le> k ==> \<^loc>{k<..l} = {}" 
17719  232 
by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def) 
233 

24691  234 
lemma atLeastAtMost_singleton [simp]: "\<^loc>{a..a} = {a}" 
235 
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) 

236 

237 
end 

14485  238 

239 
subsection {* Intervals of natural numbers *} 

240 

15047  241 
subsubsection {* The Constant @{term lessThan} *} 
242 

14485  243 
lemma lessThan_0 [simp]: "lessThan (0::nat) = {}" 
244 
by (simp add: lessThan_def) 

245 

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

247 
by (simp add: lessThan_def less_Suc_eq, blast) 

248 

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

250 
by (simp add: lessThan_def atMost_def less_Suc_eq_le) 

251 

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

253 
by blast 

254 

15047  255 
subsubsection {* The Constant @{term greaterThan} *} 
256 

14485  257 
lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc" 
258 
apply (simp add: greaterThan_def) 

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

260 
done 

261 

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

263 
apply (simp add: greaterThan_def) 

264 
apply (auto elim: linorder_neqE) 

265 
done 

266 

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

268 
by blast 

269 

15047  270 
subsubsection {* The Constant @{term atLeast} *} 
271 

14485  272 
lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV" 
273 
by (unfold atLeast_def UNIV_def, simp) 

274 

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

276 
apply (simp add: atLeast_def) 

277 
apply (simp add: Suc_le_eq) 

278 
apply (simp add: order_le_less, blast) 

279 
done 

280 

281 
lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k" 

282 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

283 

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

285 
by blast 

286 

15047  287 
subsubsection {* The Constant @{term atMost} *} 
288 

14485  289 
lemma atMost_0 [simp]: "atMost (0::nat) = {0}" 
290 
by (simp add: atMost_def) 

291 

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

293 
apply (simp add: atMost_def) 

294 
apply (simp add: less_Suc_eq order_le_less, blast) 

295 
done 

296 

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

298 
by blast 

299 

15047  300 
subsubsection {* The Constant @{term atLeastLessThan} *} 
301 

24449  302 
text{*The orientation of the following rule is tricky. The lhs is 
303 
defined in terms of the rhs. Hence the chosen orientation makes sense 

304 
in this theory  the reverse orientation complicates proofs (eg 

305 
nontermination). But outside, when the definition of the lhs is rarely 

306 
used, the opposite orientation seems preferable because it reduces a 

307 
specific concept to a more general one. *} 

15047  308 
lemma atLeast0LessThan: "{0::nat..<n} = {..<n}" 
15042  309 
by(simp add:lessThan_def atLeastLessThan_def) 
24449  310 

311 
declare atLeast0LessThan[symmetric, code unfold] 

312 

313 
lemma atLeastLessThan0: "{m..<0::nat} = {}" 

15047  314 
by (simp add: atLeastLessThan_def) 
24449  315 

15047  316 
subsubsection {* Intervals of nats with @{term Suc} *} 
317 

318 
text{*Not a simprule because the RHS is too messy.*} 

319 
lemma atLeastLessThanSuc: 

320 
"{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

321 
by (auto simp add: atLeastLessThan_def) 
15047  322 

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

323 
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 
15047  324 
by (auto simp add: atLeastLessThan_def) 
16041  325 
(* 
15047  326 
lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}" 
327 
by (induct k, simp_all add: atLeastLessThanSuc) 

328 

329 
lemma atLeastSucLessThan [simp]: "{Suc n..<n} = {}" 

330 
by (auto simp add: atLeastLessThan_def) 

16041  331 
*) 
15045  332 
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" 
14485  333 
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) 
334 

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

335 
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

336 
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
14485  337 
greaterThanAtMost_def) 
338 

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

339 
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

340 
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
14485  341 
greaterThanLessThan_def) 
342 

15554  343 
lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}" 
344 
by (auto simp add: atLeastAtMost_def) 

345 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

346 
subsubsection {* Image *} 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

347 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

348 
lemma image_add_atLeastAtMost: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

349 
"(%n::nat. n+k) ` {i..j} = {i+k..j+k}" (is "?A = ?B") 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

350 
proof 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

351 
show "?A \<subseteq> ?B" by auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

352 
next 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

353 
show "?B \<subseteq> ?A" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

354 
proof 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

355 
fix n assume a: "n : ?B" 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19538
diff
changeset

356 
hence "n  k : {i..j}" by auto 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

357 
moreover have "n = (n  k) + k" using a by auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

358 
ultimately show "n : ?A" by blast 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

359 
qed 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

360 
qed 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

361 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

362 
lemma image_add_atLeastLessThan: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

363 
"(%n::nat. n+k) ` {i..<j} = {i+k..<j+k}" (is "?A = ?B") 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

364 
proof 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

365 
show "?A \<subseteq> ?B" by auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

366 
next 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

367 
show "?B \<subseteq> ?A" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

368 
proof 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

369 
fix n assume a: "n : ?B" 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19538
diff
changeset

370 
hence "n  k : {i..<j}" by auto 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

371 
moreover have "n = (n  k) + k" using a by auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

372 
ultimately show "n : ?A" by blast 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

373 
qed 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

374 
qed 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

375 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

376 
corollary image_Suc_atLeastAtMost[simp]: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

377 
"Suc ` {i..j} = {Suc i..Suc j}" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

378 
using image_add_atLeastAtMost[where k=1] by simp 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

379 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

380 
corollary image_Suc_atLeastLessThan[simp]: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

381 
"Suc ` {i..<j} = {Suc i..<Suc j}" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

382 
using image_add_atLeastLessThan[where k=1] by simp 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

383 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

384 
lemma image_add_int_atLeastLessThan: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

385 
"(%x. x + (l::int)) ` {0..<ul} = {l..<u}" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

386 
apply (auto simp add: image_def) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

387 
apply (rule_tac x = "x  l" in bexI) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

388 
apply auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

389 
done 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

390 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

391 

14485  392 
subsubsection {* Finiteness *} 
393 

15045  394 
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}" 
14485  395 
by (induct k) (simp_all add: lessThan_Suc) 
396 

397 
lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}" 

398 
by (induct k) (simp_all add: atMost_Suc) 

399 

400 
lemma finite_greaterThanLessThan [iff]: 

15045  401 
fixes l :: nat shows "finite {l<..<u}" 
14485  402 
by (simp add: greaterThanLessThan_def) 
403 

404 
lemma finite_atLeastLessThan [iff]: 

15045  405 
fixes l :: nat shows "finite {l..<u}" 
14485  406 
by (simp add: atLeastLessThan_def) 
407 

408 
lemma finite_greaterThanAtMost [iff]: 

15045  409 
fixes l :: nat shows "finite {l<..u}" 
14485  410 
by (simp add: greaterThanAtMost_def) 
411 

412 
lemma finite_atLeastAtMost [iff]: 

413 
fixes l :: nat shows "finite {l..u}" 

414 
by (simp add: atLeastAtMost_def) 

415 

416 
lemma bounded_nat_set_is_finite: 

417 
"(ALL i:N. i < (n::nat)) ==> finite N" 

418 
 {* A bounded set of natural numbers is finite. *} 

419 
apply (rule finite_subset) 

420 
apply (rule_tac [2] finite_lessThan, auto) 

421 
done 

422 

423 
subsubsection {* Cardinality *} 

424 

15045  425 
lemma card_lessThan [simp]: "card {..<u} = u" 
15251  426 
by (induct u, simp_all add: lessThan_Suc) 
14485  427 

428 
lemma card_atMost [simp]: "card {..u} = Suc u" 

429 
by (simp add: lessThan_Suc_atMost [THEN sym]) 

430 

15045  431 
lemma card_atLeastLessThan [simp]: "card {l..<u} = u  l" 
432 
apply (subgoal_tac "card {l..<u} = card {..<ul}") 

14485  433 
apply (erule ssubst, rule card_lessThan) 
15045  434 
apply (subgoal_tac "(%x. x + l) ` {..<ul} = {l..<u}") 
14485  435 
apply (erule subst) 
436 
apply (rule card_image) 

437 
apply (simp add: inj_on_def) 

438 
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) 

439 
apply (rule_tac x = "x  l" in exI) 

440 
apply arith 

441 
done 

442 

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

443 
lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u  l" 
14485  444 
by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp) 
445 

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

446 
lemma card_greaterThanAtMost [simp]: "card {l<..u} = u  l" 
14485  447 
by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp) 
448 

15045  449 
lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u  Suc l" 
14485  450 
by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp) 
451 

452 
subsection {* Intervals of integers *} 

453 

15045  454 
lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}" 
14485  455 
by (auto simp add: atLeastAtMost_def atLeastLessThan_def) 
456 

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

457 
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" 
14485  458 
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 
459 

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

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

461 
"{l+1..<u} = {l<..<u::int}" 
14485  462 
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 
463 

464 
subsubsection {* Finiteness *} 

465 

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

466 
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
15045  467 
{(0::int)..<u} = int ` {..<nat u}" 
14485  468 
apply (unfold image_def lessThan_def) 
469 
apply auto 

470 
apply (rule_tac x = "nat x" in exI) 

471 
apply (auto simp add: zless_nat_conj zless_nat_eq_int_zless [THEN sym]) 

472 
done 

473 

15045  474 
lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}" 
14485  475 
apply (case_tac "0 \<le> u") 
476 
apply (subst image_atLeastZeroLessThan_int, assumption) 

477 
apply (rule finite_imageI) 

478 
apply auto 

479 
done 

480 

15045  481 
lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}" 
482 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 

14485  483 
apply (erule subst) 
484 
apply (rule finite_imageI) 

485 
apply (rule finite_atLeastZeroLessThan_int) 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

486 
apply (rule image_add_int_atLeastLessThan) 
14485  487 
done 
488 

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

489 
lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}" 
14485  490 
by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp) 
491 

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

492 
lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}" 
14485  493 
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) 
494 

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

495 
lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}" 
14485  496 
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) 
497 

498 
subsubsection {* Cardinality *} 

499 

15045  500 
lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u" 
14485  501 
apply (case_tac "0 \<le> u") 
502 
apply (subst image_atLeastZeroLessThan_int, assumption) 

503 
apply (subst card_image) 

504 
apply (auto simp add: inj_on_def) 

505 
done 

506 

15045  507 
lemma card_atLeastLessThan_int [simp]: "card {l..<u} = nat (u  l)" 
508 
apply (subgoal_tac "card {l..<u} = card {0..<ul}") 

14485  509 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 
15045  510 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 
14485  511 
apply (erule subst) 
512 
apply (rule card_image) 

513 
apply (simp add: inj_on_def) 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

514 
apply (rule image_add_int_atLeastLessThan) 
14485  515 
done 
516 

517 
lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u  l + 1)" 

518 
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 

519 
apply (auto simp add: compare_rls) 

520 
done 

521 

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

522 
lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u  l)" 
14485  523 
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) 
524 

15045  525 
lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u  (l + 1))" 
14485  526 
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) 
527 

528 

13850  529 
subsection {*Lemmas useful with the summation operator setsum*} 
530 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16052
diff
changeset

531 
text {* For examples, see Algebra/poly/UnivPoly2.thy *} 
13735  532 

14577  533 
subsubsection {* Disjoint Unions *} 
13735  534 

14577  535 
text {* Singletons and open intervals *} 
13735  536 

537 
lemma ivl_disj_un_singleton: 

15045  538 
"{l::'a::linorder} Un {l<..} = {l..}" 
539 
"{..<u} Un {u::'a::linorder} = {..u}" 

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

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

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

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

544 
by auto 
13735  545 

14577  546 
text {* One and twosided intervals *} 
13735  547 

548 
lemma ivl_disj_un_one: 

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

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

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

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

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

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

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

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

557 
by auto 
13735  558 

14577  559 
text {* Two and twosided intervals *} 
13735  560 

561 
lemma ivl_disj_un_two: 

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

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

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

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

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

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

569 
"[ (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

570 
by auto 
13735  571 

572 
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two 

573 

14577  574 
subsubsection {* Disjoint Intersections *} 
13735  575 

14577  576 
text {* Singletons and open intervals *} 
13735  577 

578 
lemma ivl_disj_int_singleton: 

15045  579 
"{l::'a::order} Int {l<..} = {}" 
580 
"{..<u} Int {u} = {}" 

581 
"{l} Int {l<..<u} = {}" 

582 
"{l<..<u} Int {u} = {}" 

583 
"{l} Int {l<..u} = {}" 

584 
"{l..<u} Int {u} = {}" 

13735  585 
by simp+ 
586 

14577  587 
text {* One and twosided intervals *} 
13735  588 

589 
lemma ivl_disj_int_one: 

15045  590 
"{..l::'a::order} Int {l<..<u} = {}" 
591 
"{..<l} Int {l..<u} = {}" 

592 
"{..l} Int {l<..u} = {}" 

593 
"{..<l} Int {l..u} = {}" 

594 
"{l<..u} Int {u<..} = {}" 

595 
"{l<..<u} Int {u..} = {}" 

596 
"{l..u} Int {u<..} = {}" 

597 
"{l..<u} Int {u..} = {}" 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

598 
by auto 
13735  599 

14577  600 
text {* Two and twosided intervals *} 
13735  601 

602 
lemma ivl_disj_int_two: 

15045  603 
"{l::'a::order<..<m} Int {m..<u} = {}" 
604 
"{l<..m} Int {m<..<u} = {}" 

605 
"{l..<m} Int {m..<u} = {}" 

606 
"{l..m} Int {m<..<u} = {}" 

607 
"{l<..<m} Int {m..u} = {}" 

608 
"{l<..m} Int {m<..u} = {}" 

609 
"{l..<m} Int {m..u} = {}" 

610 
"{l..m} Int {m<..u} = {}" 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

611 
by auto 
13735  612 

613 
lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two 

614 

15542  615 
subsubsection {* Some Differences *} 
616 

617 
lemma ivl_diff[simp]: 

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

619 
by(auto) 

620 

621 

622 
subsubsection {* Some Subset Conditions *} 

623 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23496
diff
changeset

624 
lemma ivl_subset [simp,noatp]: 
15542  625 
"({i..<j} \<subseteq> {m..<n}) = (j \<le> i  m \<le> i & j \<le> (n::'a::linorder))" 
626 
apply(auto simp:linorder_not_le) 

627 
apply(rule ccontr) 

628 
apply(insert linorder_le_less_linear[of i n]) 

629 
apply(clarsimp simp:linorder_not_le) 

630 
apply(fastsimp) 

631 
done 

632 

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

633 

15042  634 
subsection {* Summation indexed over intervals *} 
635 

636 
syntax 

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

15048  638 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) 
16052  639 
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10) 
640 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<=_./ _)" [0,0,10] 10) 

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

15048  643 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) 
16052  644 
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) 
645 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10) 

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

15048  648 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) 
16052  649 
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) 
650 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10) 

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

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

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

16052  656 
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
657 
("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10) 

15052  658 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
16052  659 
("(3\<^raw:$\sum_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10) 
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

660 

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

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

16052  664 
"\<Sum>i\<le>n. t" == "setsum (\<lambda>i. t) {..n}" 
15048  665 
"\<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

666 

15052  667 
text{* The above introduces some pretty alternative syntaxes for 
15056  668 
summation over intervals: 
15052  669 
\begin{center} 
670 
\begin{tabular}{lll} 

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

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

16052  674 
@{term[source]"\<Sum>x\<in>{..b}. e"} & @{term"\<Sum>x\<le>b. e"} & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\ 
15056  675 
@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"} 
15052  676 
\end{tabular} 
677 
\end{center} 

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

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

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

21502  682 
@{text latex_sum} (e.g.\ via @{text "mode = latex_sum"} in 
15056  683 
antiquotations). It is not the default \LaTeX\ output because it only 
684 
works well with italicstyle formulae, not ttstyle. 

15052  685 

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

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

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

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

690 

15542  691 
text{* This congruence rule should be used for sums over intervals as 
692 
the standard theorem @{text[source]setsum_cong} does not work well 

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

694 
the context. *} 

695 

696 
lemma setsum_ivl_cong: 

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

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

699 
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

700 

16041  701 
(* FIXME why are the following simp rules but the corresponding eqns 
702 
on intervals are not? *) 

703 

16052  704 
lemma setsum_atMost_Suc[simp]: "(\<Sum>i \<le> Suc n. f i) = (\<Sum>i \<le> n. f i) + f(Suc n)" 
705 
by (simp add:atMost_Suc add_ac) 

706 

16041  707 
lemma setsum_lessThan_Suc[simp]: "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n" 
708 
by (simp add:lessThan_Suc add_ac) 

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

709 

15911  710 
lemma setsum_cl_ivl_Suc[simp]: 
15561  711 
"setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))" 
712 
by (auto simp:add_ac atLeastAtMostSuc_conv) 

713 

15911  714 
lemma setsum_op_ivl_Suc[simp]: 
15561  715 
"setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))" 
716 
by (auto simp:add_ac atLeastLessThanSuc) 

16041  717 
(* 
15561  718 
lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==> 
719 
(\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)" 

720 
by (auto simp:add_ac atLeastAtMostSuc_conv) 

16041  721 
*) 
15539  722 
lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> 
723 
setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}" 

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

725 

726 
lemma setsum_diff_nat_ivl: 

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

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

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

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

731 
apply (simp add: add_ac) 

732 
done 

733 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

734 
subsection{* Shifting bounds *} 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

735 

15539  736 
lemma setsum_shift_bounds_nat_ivl: 
737 
"setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}" 

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

739 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

740 
lemma setsum_shift_bounds_cl_nat_ivl: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

741 
"setsum f {m+k..n+k} = setsum (%i. f(i + k)){m..n::nat}" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

742 
apply (insert setsum_reindex[OF inj_on_add_nat, where h=f and B = "{m..n}"]) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

743 
apply (simp add:image_add_atLeastAtMost o_def) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

744 
done 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

745 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

746 
corollary setsum_shift_bounds_cl_Suc_ivl: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

747 
"setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

748 
by (simp add:setsum_shift_bounds_cl_nat_ivl[where k=1,simplified]) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

749 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

750 
corollary setsum_shift_bounds_Suc_ivl: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

751 
"setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

752 
by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified]) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

753 

19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

754 
lemma setsum_head: 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

755 
fixes n :: nat 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

756 
assumes mn: "m <= n" 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

757 
shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs") 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

758 
proof  
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

759 
from mn 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

760 
have "{m..n} = {m} \<union> {m<..n}" 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

761 
by (auto intro: ivl_disj_un_singleton) 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

762 
hence "?lhs = (\<Sum>x\<in>{m} \<union> {m<..n}. P x)" 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

763 
by (simp add: atLeast0LessThan) 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

764 
also have "\<dots> = ?rhs" by simp 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

765 
finally show ?thesis . 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

766 
qed 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

767 

6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

768 
lemma setsum_head_upt: 
19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

769 
fixes m::nat 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

770 
assumes m: "0 < m" 
19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

771 
shows "(\<Sum>x<m. P x) = P 0 + (\<Sum>x\<in>{1..<m}. P x)" 
19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

772 
proof  
19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

773 
have "(\<Sum>x<m. P x) = (\<Sum>x\<in>{0..<m}. P x)" 
19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

774 
by (simp add: atLeast0LessThan) 
19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

775 
also 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

776 
from m 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

777 
have "\<dots> = (\<Sum>x\<in>{0..m  1}. P x)" 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

778 
by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost) 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

779 
also 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

780 
have "\<dots> = P 0 + (\<Sum>x\<in>{0<..m  1}. P x)" 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

781 
by (simp add: setsum_head) 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

782 
also 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

783 
from m 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

784 
have "{0<..m  1} = {1..<m}" 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

785 
by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost) 
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

786 
finally show ?thesis . 
19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

787 
qed 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

788 

17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

789 
subsection {* The formula for geometric sums *} 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

790 

e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

791 
lemma geometric_sum: 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

792 
"x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = 
22713  793 
(x ^ n  1) / (x  1::'a::{field, recpower})" 
23496  794 
by (induct "n") (simp_all add:field_simps power_Suc) 
17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

795 

19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

796 
subsection {* The formula for arithmetic sums *} 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

797 

958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

798 
lemma gauss_sum: 
23277  799 
"((1::'a::comm_semiring_1) + 1)*(\<Sum>i\<in>{1..n}. of_nat i) = 
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

800 
of_nat n*((of_nat n)+1)" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

801 
proof (induct n) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

802 
case 0 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

803 
show ?case by simp 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

804 
next 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

805 
case (Suc n) 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23431
diff
changeset

806 
then show ?case by (simp add: ring_simps) 
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

807 
qed 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

808 

958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

809 
theorem arith_series_general: 
23277  810 
"((1::'a::comm_semiring_1) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = 
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

811 
of_nat n * (a + (a + of_nat(n  1)*d))" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

812 
proof cases 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

813 
assume ngt1: "n > 1" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

814 
let ?I = "\<lambda>i. of_nat i" and ?n = "of_nat n" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

815 
have 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

816 
"(\<Sum>i\<in>{..<n}. a+?I i*d) = 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

817 
((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

818 
by (rule setsum_addf) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

819 
also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

820 
also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

821 
by (simp add: setsum_right_distrib setsum_head_upt mult_ac) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

822 
also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

823 
by (simp add: left_distrib right_distrib) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

824 
also from ngt1 have "{1..<n} = {1..n  1}" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

825 
by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

826 
also from ngt1 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

827 
have "(1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..n  1}. ?I i) = ((1+1)*?n*a + d*?I (n  1)*?I n)" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

828 
by (simp only: mult_ac gauss_sum [of "n  1"]) 
23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23413
diff
changeset

829 
(simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]]) 
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

830 
finally show ?thesis by (simp add: mult_ac add_ac right_distrib) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

831 
next 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

832 
assume "\<not>(n > 1)" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

833 
hence "n = 1 \<or> n = 0" by auto 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

834 
thus ?thesis by (auto simp: mult_ac right_distrib) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

835 
qed 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

836 

958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

837 
lemma arith_series_nat: 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

838 
"Suc (Suc 0) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n  1)*d))" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

839 
proof  
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

840 
have 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

841 
"((1::nat) + 1) * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) = 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

842 
of_nat(n) * (a + (a + of_nat(n  1)*d))" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

843 
by (rule arith_series_general) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

844 
thus ?thesis by (auto simp add: of_nat_id) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

845 
qed 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

846 

958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

847 
lemma arith_series_int: 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

848 
"(2::int) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

849 
of_nat n * (a + (a + of_nat(n  1)*d))" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

850 
proof  
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

851 
have 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

852 
"((1::int) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

853 
of_nat(n) * (a + (a + of_nat(n  1)*d))" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

854 
by (rule arith_series_general) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

855 
thus ?thesis by simp 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

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

857 

19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

858 
lemma sum_diff_distrib: 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

859 
fixes P::"nat\<Rightarrow>nat" 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

860 
shows 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

861 
"\<forall>x. Q x \<le> P x \<Longrightarrow> 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

862 
(\<Sum>x<n. P x)  (\<Sum>x<n. Q x) = (\<Sum>x<n. P x  Q x)" 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

863 
proof (induct n) 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

864 
case 0 show ?case by simp 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

865 
next 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

866 
case (Suc n) 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

867 

0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

868 
let ?lhs = "(\<Sum>x<n. P x)  (\<Sum>x<n. Q x)" 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

869 
let ?rhs = "\<Sum>x<n. P x  Q x" 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

870 

0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

871 
from Suc have "?lhs = ?rhs" by simp 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

872 
moreover 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

873 
from Suc have "?lhs + P n  Q n = ?rhs + (P n  Q n)" by simp 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

874 
moreover 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

875 
from Suc have 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

876 
"(\<Sum>x<n. P x) + P n  ((\<Sum>x<n. Q x) + Q n) = ?rhs + (P n  Q n)" 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

877 
by (subst diff_diff_left[symmetric], 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

878 
subst diff_add_assoc2) 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

879 
(auto simp: diff_add_assoc2 intro: setsum_mono) 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

880 
ultimately 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

881 
show ?case by simp 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

882 
qed 
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

883 

0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

884 

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

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

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

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

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

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

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

891 
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

892 
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

893 
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

894 
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

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

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

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

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

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

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

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

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

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

904 
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

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

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

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

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

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

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

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

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

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

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

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

916 
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

917 
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

918 
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

919 
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

920 
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

921 
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

922 
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

923 
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

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

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

926 
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

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

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

929 
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

930 

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

931 
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

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

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

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

935 

8924  936 
end 