author  bulwahn 
Sat, 19 Jul 2008 19:27:13 +0200  
changeset 27656  d4f6e64ee7cc 
parent 26105  ae06618225ec 
child 28068  f6b2d1995171 
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 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25560
diff
changeset

13 
imports Int 
15131  14 
begin 
8924  15 

24691  16 
context ord 
17 
begin 

18 
definition 

25062  19 
lessThan :: "'a => 'a set" ("(1{..<_})") where 
20 
"{..<u} == {x. x < u}" 

24691  21 

22 
definition 

25062  23 
atMost :: "'a => 'a set" ("(1{.._})") where 
24 
"{..u} == {x. x \<le> u}" 

24691  25 

26 
definition 

25062  27 
greaterThan :: "'a => 'a set" ("(1{_<..})") where 
28 
"{l<..} == {x. l<x}" 

24691  29 

30 
definition 

25062  31 
atLeast :: "'a => 'a set" ("(1{_..})") where 
32 
"{l..} == {x. l\<le>x}" 

24691  33 

34 
definition 

25062  35 
greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where 
36 
"{l<..<u} == {l<..} Int {..<u}" 

24691  37 

38 
definition 

25062  39 
atLeastLessThan :: "'a => 'a => 'a set" ("(1{_..<_})") where 
40 
"{l..<u} == {l..} Int {..<u}" 

24691  41 

42 
definition 

25062  43 
greaterThanAtMost :: "'a => 'a => 'a set" ("(1{_<.._})") where 
44 
"{l<..u} == {l<..} Int {..u}" 

24691  45 

46 
definition 

25062  47 
atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where 
48 
"{l..u} == {l..} Int {..u}" 

24691  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 

25062  109 
lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i<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 

25062  120 
lemma (in ord) greaterThan_iff [iff]: "(i: greaterThan k) = (k<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" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25919
diff
changeset

125 
by (auto simp add: greaterThan_def atMost_def) 
13735  126 

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

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

129 
apply (rule double_complement) 
13735  130 
done 
131 

25062  132 
lemma (in ord) atLeast_iff [iff]: "(i: atLeast k) = (k<=i)" 
13850  133 
by (simp add: atLeast_def) 
13735  134 

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

135 
lemma Compl_atLeast [simp]: 
13735  136 
"!!k:: 'a::linorder. atLeast k = lessThan k" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25919
diff
changeset

137 
by (auto simp add: lessThan_def atLeast_def) 
13735  138 

25062  139 
lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i<=k)" 
13850  140 
by (simp add: atMost_def) 
13735  141 

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

13850  144 

145 

14485  146 
subsection {* Logical Equivalences for Set Inclusion and Equality *} 
13850  147 

148 
lemma atLeast_subset_iff [iff]: 

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

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

150 
by (blast intro: order_trans) 
13850  151 

152 
lemma atLeast_eq_iff [iff]: 

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

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

156 
lemma greaterThan_subset_iff [iff]: 

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

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

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

159 
apply (subst linorder_not_less [symmetric], blast) 
13850  160 
done 
161 

162 
lemma greaterThan_eq_iff [iff]: 

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

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

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

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

166 
apply (simp_all add: greaterThan_subset_iff) 
13850  167 
done 
168 

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

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

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

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

175 
lemma lessThan_subset_iff [iff]: 

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

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

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

178 
apply (subst linorder_not_less [symmetric], blast) 
13850  179 
done 
180 

181 
lemma lessThan_eq_iff [iff]: 

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

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

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

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

185 
apply (simp_all add: lessThan_subset_iff) 
13735  186 
done 
187 

188 

13850  189 
subsection {*Twosided intervals*} 
13735  190 

24691  191 
context ord 
192 
begin 

193 

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

194 
lemma greaterThanLessThan_iff [simp,noatp]: 
25062  195 
"(i : {l<..<u}) = (l < i & i < u)" 
13735  196 
by (simp add: greaterThanLessThan_def) 
197 

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

198 
lemma atLeastLessThan_iff [simp,noatp]: 
25062  199 
"(i : {l..<u}) = (l <= i & i < u)" 
13735  200 
by (simp add: atLeastLessThan_def) 
201 

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

202 
lemma greaterThanAtMost_iff [simp,noatp]: 
25062  203 
"(i : {l<..u}) = (l < i & i <= u)" 
13735  204 
by (simp add: greaterThanAtMost_def) 
205 

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

206 
lemma atLeastAtMost_iff [simp,noatp]: 
25062  207 
"(i : {l..u}) = (l <= i & i <= u)" 
13735  208 
by (simp add: atLeastAtMost_def) 
209 

14577  210 
text {* The above four lemmas could be declared as iffs. 
211 
If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int} 

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

24691  213 
end 
13735  214 

15554  215 
subsubsection{* Emptyness and singletons *} 
216 

24691  217 
context order 
218 
begin 

15554  219 

25062  220 
lemma atLeastAtMost_empty [simp]: "n < m ==> {m..n} = {}"; 
24691  221 
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) 
222 

25062  223 
lemma atLeastLessThan_empty[simp]: "n \<le> m ==> {m..<n} = {}" 
15554  224 
by (auto simp add: atLeastLessThan_def) 
225 

25062  226 
lemma greaterThanAtMost_empty[simp]:"l \<le> k ==> {k<..l} = {}" 
17719  227 
by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) 
228 

25062  229 
lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..l} = {}" 
17719  230 
by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def) 
231 

25062  232 
lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}" 
24691  233 
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) 
234 

235 
end 

14485  236 

237 
subsection {* Intervals of natural numbers *} 

238 

15047  239 
subsubsection {* The Constant @{term lessThan} *} 
240 

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

243 

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

245 
by (simp add: lessThan_def less_Suc_eq, blast) 

246 

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

248 
by (simp add: lessThan_def atMost_def less_Suc_eq_le) 

249 

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

251 
by blast 

252 

15047  253 
subsubsection {* The Constant @{term greaterThan} *} 
254 

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

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

258 
done 

259 

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

261 
apply (simp add: greaterThan_def) 

262 
apply (auto elim: linorder_neqE) 

263 
done 

264 

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

266 
by blast 

267 

15047  268 
subsubsection {* The Constant @{term atLeast} *} 
269 

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

272 

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

274 
apply (simp add: atLeast_def) 

275 
apply (simp add: Suc_le_eq) 

276 
apply (simp add: order_le_less, blast) 

277 
done 

278 

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

280 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

281 

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

283 
by blast 

284 

15047  285 
subsubsection {* The Constant @{term atMost} *} 
286 

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

289 

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

291 
apply (simp add: atMost_def) 

292 
apply (simp add: less_Suc_eq order_le_less, blast) 

293 
done 

294 

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

296 
by blast 

297 

15047  298 
subsubsection {* The Constant @{term atLeastLessThan} *} 
299 

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

302 
in this theory  the reverse orientation complicates proofs (eg 

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

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

305 
specific concept to a more general one. *} 

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

309 
declare atLeast0LessThan[symmetric, code unfold] 

310 

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

15047  312 
by (simp add: atLeastLessThan_def) 
24449  313 

15047  314 
subsubsection {* Intervals of nats with @{term Suc} *} 
315 

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

317 
lemma atLeastLessThanSuc: 

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

319 
by (auto simp add: atLeastLessThan_def) 
15047  320 

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

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

326 

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

328 
by (auto simp add: atLeastLessThan_def) 

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

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

333 
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

334 
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
14485  335 
greaterThanAtMost_def) 
336 

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

337 
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

338 
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
14485  339 
greaterThanLessThan_def) 
340 

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

343 

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

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

345 

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

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

347 
"(%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

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

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

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

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

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

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

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

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

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

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

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

359 

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

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

361 
"(%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

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

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

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

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

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

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

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

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

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

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

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

373 

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

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

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

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

377 

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

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

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

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

381 

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

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

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

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

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

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

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

388 

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

389 

14485  390 
subsubsection {* Finiteness *} 
391 

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

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

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

397 

398 
lemma finite_greaterThanLessThan [iff]: 

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

402 
lemma finite_atLeastLessThan [iff]: 

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

406 
lemma finite_greaterThanAtMost [iff]: 

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

410 
lemma finite_atLeastAtMost [iff]: 

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

412 
by (simp add: atLeastAtMost_def) 

413 

414 
lemma bounded_nat_set_is_finite: 

24853  415 
"(ALL i:N. i < (n::nat)) ==> finite N" 
14485  416 
 {* A bounded set of natural numbers is finite. *} 
417 
apply (rule finite_subset) 

418 
apply (rule_tac [2] finite_lessThan, auto) 

419 
done 

420 

24853  421 
text{* Any subset of an interval of natural numbers the size of the 
422 
subset is exactly that interval. *} 

423 

424 
lemma subset_card_intvl_is_intvl: 

425 
"A <= {k..<k+card A} \<Longrightarrow> A = {k..<k+card A}" (is "PROP ?P") 

426 
proof cases 

427 
assume "finite A" 

428 
thus "PROP ?P" 

429 
proof(induct A rule:finite_linorder_induct) 

430 
case empty thus ?case by auto 

431 
next 

432 
case (insert A b) 

433 
moreover hence "b ~: A" by auto 

434 
moreover have "A <= {k..<k+card A}" and "b = k+card A" 

435 
using `b ~: A` insert by fastsimp+ 

436 
ultimately show ?case by auto 

437 
qed 

438 
next 

439 
assume "~finite A" thus "PROP ?P" by simp 

440 
qed 

441 

442 

14485  443 
subsubsection {* Cardinality *} 
444 

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

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

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

450 

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

14485  453 
apply (erule ssubst, rule card_lessThan) 
15045  454 
apply (subgoal_tac "(%x. x + l) ` {..<ul} = {l..<u}") 
14485  455 
apply (erule subst) 
456 
apply (rule card_image) 

457 
apply (simp add: inj_on_def) 

458 
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) 

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

460 
apply arith 

461 
done 

462 

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

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

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

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

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

26105
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

472 

ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

473 
lemma ex_bij_betw_nat_finite: 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

474 
"finite M \<Longrightarrow> \<exists>h. bij_betw h {0..<card M} M" 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

475 
apply(drule finite_imp_nat_seg_image_inj_on) 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

476 
apply(auto simp:atLeast0LessThan[symmetric] lessThan_def[symmetric] card_image bij_betw_def) 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

477 
done 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

478 

ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

479 
lemma ex_bij_betw_finite_nat: 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

480 
"finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}" 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

481 
by (blast dest: ex_bij_betw_nat_finite bij_betw_inv) 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

482 

ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

483 

14485  484 
subsection {* Intervals of integers *} 
485 

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

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

489 
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" 
14485  490 
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 
491 

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

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

493 
"{l+1..<u} = {l<..<u::int}" 
14485  494 
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 
495 

496 
subsubsection {* Finiteness *} 

497 

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

498 
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
15045  499 
{(0::int)..<u} = int ` {..<nat u}" 
14485  500 
apply (unfold image_def lessThan_def) 
501 
apply auto 

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

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

504 
done 

505 

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

509 
apply (rule finite_imageI) 

510 
apply auto 

511 
done 

512 

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

14485  515 
apply (erule subst) 
516 
apply (rule finite_imageI) 

517 
apply (rule finite_atLeastZeroLessThan_int) 

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

518 
apply (rule image_add_int_atLeastLessThan) 
14485  519 
done 
520 

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

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

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

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

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

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

24853  530 

14485  531 
subsubsection {* Cardinality *} 
532 

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

536 
apply (subst card_image) 

537 
apply (auto simp add: inj_on_def) 

538 
done 

539 

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

14485  542 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 
15045  543 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 
14485  544 
apply (erule subst) 
545 
apply (rule card_image) 

546 
apply (simp add: inj_on_def) 

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

547 
apply (rule image_add_int_atLeastLessThan) 
14485  548 
done 
549 

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

551 
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 

552 
apply (auto simp add: compare_rls) 

553 
done 

554 

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

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

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

27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

561 
lemma finite_M_bounded_by_nat: "finite {k. P k \<and> k < (i::nat)}" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

562 
proof  
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

563 
have "{k. P k \<and> k < i} \<subseteq> {..<i}" by auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

564 
with finite_lessThan[of "i"] show ?thesis by (simp add: finite_subset) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

565 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

566 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

567 
lemma card_less: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

568 
assumes zero_in_M: "0 \<in> M" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

569 
shows "card {k \<in> M. k < Suc i} \<noteq> 0" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

570 
proof  
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

571 
from zero_in_M have "{k \<in> M. k < Suc i} \<noteq> {}" by auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

572 
with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

573 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

574 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

575 
lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

576 
apply (rule card_bij_eq [of "Suc" _ _ "\<lambda>x. x  1"]) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

577 
apply simp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

578 
apply fastsimp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

579 
apply auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

580 
apply (rule inj_on_diff_nat) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

581 
apply auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

582 
apply (case_tac x) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

583 
apply auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

584 
apply (case_tac xa) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

585 
apply auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

586 
apply (case_tac xa) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

587 
apply auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

588 
apply (auto simp add: finite_M_bounded_by_nat) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

589 
done 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

590 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

591 
lemma card_less_Suc: 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

592 
assumes zero_in_M: "0 \<in> M" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

593 
shows "Suc (card {k. Suc k \<in> M \<and> k < i}) = card {k \<in> M. k < Suc i}" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

594 
proof  
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

595 
from assms have a: "0 \<in> {k \<in> M. k < Suc i}" by simp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

596 
hence c: "{k \<in> M. k < Suc i} = insert 0 ({k \<in> M. k < Suc i}  {0})" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

597 
by (auto simp only: insert_Diff) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

598 
have b: "{k \<in> M. k < Suc i}  {0} = {k \<in> M  {0}. k < Suc i}" by auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

599 
from finite_M_bounded_by_nat[of "\<lambda>x. x \<in> M" "Suc i"] have "Suc (card {k. Suc k \<in> M \<and> k < i}) = card (insert 0 ({k \<in> M. k < Suc i}  {0}))" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

600 
apply (subst card_insert) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

601 
apply simp_all 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

602 
apply (subst b) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

603 
apply (subst card_less_Suc2[symmetric]) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

604 
apply simp_all 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

605 
done 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

606 
with c show ?thesis by simp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

607 
qed 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

608 

14485  609 

13850  610 
subsection {*Lemmas useful with the summation operator setsum*} 
611 

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

612 
text {* For examples, see Algebra/poly/UnivPoly2.thy *} 
13735  613 

14577  614 
subsubsection {* Disjoint Unions *} 
13735  615 

14577  616 
text {* Singletons and open intervals *} 
13735  617 

618 
lemma ivl_disj_un_singleton: 

15045  619 
"{l::'a::linorder} Un {l<..} = {l..}" 
620 
"{..<u} Un {u::'a::linorder} = {..u}" 

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

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

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

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

625 
by auto 
13735  626 

14577  627 
text {* One and twosided intervals *} 
13735  628 

629 
lemma ivl_disj_un_one: 

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

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

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

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

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

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

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

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

638 
by auto 
13735  639 

14577  640 
text {* Two and twosided intervals *} 
13735  641 

642 
lemma ivl_disj_un_two: 

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

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

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

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

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

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

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

651 
by auto 
13735  652 

653 
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two 

654 

14577  655 
subsubsection {* Disjoint Intersections *} 
13735  656 

14577  657 
text {* Singletons and open intervals *} 
13735  658 

659 
lemma ivl_disj_int_singleton: 

15045  660 
"{l::'a::order} Int {l<..} = {}" 
661 
"{..<u} Int {u} = {}" 

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

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

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

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

13735  666 
by simp+ 
667 

14577  668 
text {* One and twosided intervals *} 
13735  669 

670 
lemma ivl_disj_int_one: 

15045  671 
"{..l::'a::order} Int {l<..<u} = {}" 
672 
"{..<l} Int {l..<u} = {}" 

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

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

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

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

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

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

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

679 
by auto 
13735  680 

14577  681 
text {* Two and twosided intervals *} 
13735  682 

683 
lemma ivl_disj_int_two: 

15045  684 
"{l::'a::order<..<m} Int {m..<u} = {}" 
685 
"{l<..m} Int {m<..<u} = {}" 

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

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

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

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

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

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

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

692 
by auto 
13735  693 

694 
lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two 

695 

15542  696 
subsubsection {* Some Differences *} 
697 

698 
lemma ivl_diff[simp]: 

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

700 
by(auto) 

701 

702 

703 
subsubsection {* Some Subset Conditions *} 

704 

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

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

708 
apply(rule ccontr) 

709 
apply(insert linorder_le_less_linear[of i n]) 

710 
apply(clarsimp simp:linorder_not_le) 

711 
apply(fastsimp) 

712 
done 

713 

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

714 

15042  715 
subsection {* Summation indexed over intervals *} 
716 

717 
syntax 

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

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

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

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

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

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

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

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

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

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

15052  739 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
16052  740 
("(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

741 

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

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

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

747 

15052  748 
text{* The above introduces some pretty alternative syntaxes for 
15056  749 
summation over intervals: 
15052  750 
\begin{center} 
751 
\begin{tabular}{lll} 

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

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

16052  755 
@{term[source]"\<Sum>x\<in>{..b}. e"} & @{term"\<Sum>x\<le>b. e"} & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\ 
15056  756 
@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"} 
15052  757 
\end{tabular} 
758 
\end{center} 

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

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

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

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

15052  766 

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

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

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

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

771 

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

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

775 
the context. *} 

776 

777 
lemma setsum_ivl_cong: 

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

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

780 
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

781 

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

784 

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

787 

16041  788 
lemma setsum_lessThan_Suc[simp]: "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n" 
789 
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

790 

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

794 

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

16041  798 
(* 
15561  799 
lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==> 
800 
(\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)" 

801 
by (auto simp:add_ac atLeastAtMostSuc_conv) 

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

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

806 

807 
lemma setsum_diff_nat_ivl: 

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

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

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

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

812 
apply (simp add: add_ac) 

813 
done 

814 

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

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

816 

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

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

820 

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

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

822 
"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

823 
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

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

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

826 

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

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

828 
"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

829 
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

830 

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

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

832 
"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

833 
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

834 

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

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

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

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

838 
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

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

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

841 
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

842 
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

843 
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

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

845 
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

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

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

848 

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

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

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

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

852 
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

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

854 
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

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

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

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

858 
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

859 
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

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

861 
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

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

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

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

865 
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

866 
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

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

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

869 

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

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

871 

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

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

873 
"x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = 
22713  874 
(x ^ n  1) / (x  1::'a::{field, recpower})" 
23496  875 
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

876 

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

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

878 

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

879 
lemma gauss_sum: 
23277  880 
"((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

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

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

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

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

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

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

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

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

889 

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

890 
theorem arith_series_general: 
23277  891 
"((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

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

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

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

895 
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

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

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

898 
((\<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

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

900 
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

901 
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

902 
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

903 
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

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

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

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

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

908 
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

909 
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

910 
(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

911 
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

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

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

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

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

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

917 

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

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

919 
"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

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

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

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

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

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

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

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

927 

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

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

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

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

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

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

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

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

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

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

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

938 

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

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

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

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

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

943 
(\<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

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

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

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

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

948 

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

949 
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

950 
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

951 

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

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

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

954 
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

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

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

957 
"(\<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

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

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

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

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

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

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

964 

8924  965 
end 