author  nipkow 
Mon, 31 Aug 2009 14:09:42 +0200  
changeset 32456  341c83339aeb 
parent 32436  10cd49e0c067 
child 32596  bd68c04dace1 
permissions  rwrr 
8924  1 
(* Title: HOL/SetInterval.thy 
13735  2 
Author: Tobias Nipkow and Clemens Ballarin 
14485  3 
Additions by Jeremy Avigad in March 2004 
8957  4 
Copyright 2000 TU Muenchen 
8924  5 

13735  6 
lessThan, greaterThan, atLeast, atMost and twosided intervals 
8924  7 
*) 
8 

14577  9 
header {* Set intervals *} 
10 

15131  11 
theory SetInterval 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25560
diff
changeset

12 
imports Int 
15131  13 
begin 
8924  14 

24691  15 
context ord 
16 
begin 

17 
definition 

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

24691  20 

21 
definition 

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

24691  24 

25 
definition 

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

24691  28 

29 
definition 

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

24691  32 

33 
definition 

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

24691  36 

37 
definition 

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

24691  40 

41 
definition 

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

24691  44 

45 
definition 

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

24691  48 

49 
end 

8924  50 

13735  51 

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

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

14418  56 
syntax 
30384  57 
"@UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" 10) 
58 
"@UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" 10) 

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

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

14418  61 

30372  62 
syntax (xsymbols) 
30384  63 
"@UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _\<le>_./ _)" 10) 
64 
"@UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _<_./ _)" 10) 

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

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

14418  67 

30372  68 
syntax (latex output) 
30384  69 
"@UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ \<le> _)/ _)" 10) 
70 
"@UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ < _)/ _)" 10) 

71 
"@INTER_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ \<le> _)/ _)" 10) 

72 
"@INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ < _)/ _)" 10) 

14418  73 

74 
translations 

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

15045  76 
"UN i<n. A" == "UN i:{..<n}. A" 
14418  77 
"INT i<=n. A" == "INT i:{..n}. A" 
15045  78 
"INT i<n. A" == "INT i:{..<n}. A" 
14418  79 

80 

14485  81 
subsection {* Various equivalences *} 
13735  82 

25062  83 
lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i<k)" 
13850  84 
by (simp add: lessThan_def) 
13735  85 

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

86 
lemma Compl_lessThan [simp]: 
13735  87 
"!!k:: 'a::linorder. lessThan k = atLeast k" 
13850  88 
apply (auto simp add: lessThan_def atLeast_def) 
13735  89 
done 
90 

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

13735  93 

25062  94 
lemma (in ord) greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)" 
13850  95 
by (simp add: greaterThan_def) 
13735  96 

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

97 
lemma Compl_greaterThan [simp]: 
13735  98 
"!!k:: 'a::linorder. greaterThan k = atMost k" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25919
diff
changeset

99 
by (auto simp add: greaterThan_def atMost_def) 
13735  100 

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

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

103 
apply (rule double_complement) 
13735  104 
done 
105 

25062  106 
lemma (in ord) atLeast_iff [iff]: "(i: atLeast k) = (k<=i)" 
13850  107 
by (simp add: atLeast_def) 
13735  108 

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

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

111 
by (auto simp add: lessThan_def atLeast_def) 
13735  112 

25062  113 
lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i<=k)" 
13850  114 
by (simp add: atMost_def) 
13735  115 

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

13850  118 

119 

14485  120 
subsection {* Logical Equivalences for Set Inclusion and Equality *} 
13850  121 

122 
lemma atLeast_subset_iff [iff]: 

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

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

124 
by (blast intro: order_trans) 
13850  125 

126 
lemma atLeast_eq_iff [iff]: 

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

127 
"(atLeast x = atLeast y) = (x = (y::'a::linorder))" 
13850  128 
by (blast intro: order_antisym order_trans) 
129 

130 
lemma greaterThan_subset_iff [iff]: 

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

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

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

133 
apply (subst linorder_not_less [symmetric], blast) 
13850  134 
done 
135 

136 
lemma greaterThan_eq_iff [iff]: 

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

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

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

139 
apply (erule equalityE) 
29709  140 
apply simp_all 
13850  141 
done 
142 

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

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

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

146 
lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" 
13850  147 
by (blast intro: order_antisym order_trans) 
148 

149 
lemma lessThan_subset_iff [iff]: 

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

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

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

152 
apply (subst linorder_not_less [symmetric], blast) 
13850  153 
done 
154 

155 
lemma lessThan_eq_iff [iff]: 

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

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

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

158 
apply (erule equalityE) 
29709  159 
apply simp_all 
13735  160 
done 
161 

162 

13850  163 
subsection {*Twosided intervals*} 
13735  164 

24691  165 
context ord 
166 
begin 

167 

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

168 
lemma greaterThanLessThan_iff [simp,noatp]: 
25062  169 
"(i : {l<..<u}) = (l < i & i < u)" 
13735  170 
by (simp add: greaterThanLessThan_def) 
171 

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

172 
lemma atLeastLessThan_iff [simp,noatp]: 
25062  173 
"(i : {l..<u}) = (l <= i & i < u)" 
13735  174 
by (simp add: atLeastLessThan_def) 
175 

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

176 
lemma greaterThanAtMost_iff [simp,noatp]: 
25062  177 
"(i : {l<..u}) = (l < i & i <= u)" 
13735  178 
by (simp add: greaterThanAtMost_def) 
179 

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

180 
lemma atLeastAtMost_iff [simp,noatp]: 
25062  181 
"(i : {l..u}) = (l <= i & i <= u)" 
13735  182 
by (simp add: atLeastAtMost_def) 
183 

32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32408
diff
changeset

184 
text {* The above four lemmas could be declared as iffs. Unfortunately this 
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32408
diff
changeset

185 
breaks many proofs. Since it only helps blast, it is better to leave well 
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32408
diff
changeset

186 
alone *} 
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32408
diff
changeset

187 

24691  188 
end 
13735  189 

32400  190 
subsubsection{* Emptyness, singletons, subset *} 
15554  191 

24691  192 
context order 
193 
begin 

15554  194 

32400  195 
lemma atLeastatMost_empty[simp]: 
196 
"b < a \<Longrightarrow> {a..b} = {}" 

197 
by(auto simp: atLeastAtMost_def atLeast_def atMost_def) 

198 

199 
lemma atLeastatMost_empty_iff[simp]: 

200 
"{a..b} = {} \<longleftrightarrow> (~ a <= b)" 

201 
by auto (blast intro: order_trans) 

202 

203 
lemma atLeastatMost_empty_iff2[simp]: 

204 
"{} = {a..b} \<longleftrightarrow> (~ a <= b)" 

205 
by auto (blast intro: order_trans) 

206 

207 
lemma atLeastLessThan_empty[simp]: 

208 
"b <= a \<Longrightarrow> {a..<b} = {}" 

209 
by(auto simp: atLeastLessThan_def) 

24691  210 

32400  211 
lemma atLeastLessThan_empty_iff[simp]: 
212 
"{a..<b} = {} \<longleftrightarrow> (~ a < b)" 

213 
by auto (blast intro: le_less_trans) 

214 

215 
lemma atLeastLessThan_empty_iff2[simp]: 

216 
"{} = {a..<b} \<longleftrightarrow> (~ a < b)" 

217 
by auto (blast intro: le_less_trans) 

15554  218 

32400  219 
lemma greaterThanAtMost_empty[simp]: "l \<le> k ==> {k<..l} = {}" 
17719  220 
by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) 
221 

32400  222 
lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \<longleftrightarrow> ~ k < l" 
223 
by auto (blast intro: less_le_trans) 

224 

225 
lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \<longleftrightarrow> ~ k < l" 

226 
by auto (blast intro: less_le_trans) 

227 

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

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

32400  234 
lemma atLeastatMost_subset_iff[simp]: 
235 
"{a..b} <= {c..d} \<longleftrightarrow> (~ a <= b)  c <= a & b <= d" 

236 
unfolding atLeastAtMost_def atLeast_def atMost_def 

237 
by (blast intro: order_trans) 

238 

239 
lemma atLeastatMost_psubset_iff: 

240 
"{a..b} < {c..d} \<longleftrightarrow> 

241 
((~ a <= b)  c <= a & b <= d & (c < a  b < d)) & c <= d" 

242 
by(simp add: psubset_eq expand_set_eq less_le_not_le)(blast intro: order_trans) 

243 

24691  244 
end 
14485  245 

32408  246 
lemma (in linorder) atLeastLessThan_subset_iff: 
247 
"{a..<b} <= {c..<d} \<Longrightarrow> b <= a  c<=a & b<=d" 

248 
apply (auto simp:subset_eq Ball_def) 

249 
apply(frule_tac x=a in spec) 

250 
apply(erule_tac x=d in allE) 

251 
apply (simp add: less_imp_le) 

252 
done 

253 

32456
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

254 
subsubsection {* Intersection *} 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

255 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

256 
context linorder 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

257 
begin 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

258 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

259 
lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

260 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

261 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

262 
lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

263 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

264 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

265 
lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

266 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

267 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

268 
lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

269 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

270 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

271 
lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

272 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

273 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

274 
lemma Int_atLeastLessThan[simp]: "{a..<b} Int {c..<d} = {max a c ..< min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

275 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

276 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

277 
lemma Int_greaterThanAtMost[simp]: "{a<..b} Int {c<..d} = {max a c <.. min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

278 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

279 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

280 
lemma Int_greaterThanLessThan[simp]: "{a<..<b} Int {c<..<d} = {max a c <..< min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

281 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

282 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

283 
end 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

284 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

285 

14485  286 
subsection {* Intervals of natural numbers *} 
287 

15047  288 
subsubsection {* The Constant @{term lessThan} *} 
289 

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

292 

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

294 
by (simp add: lessThan_def less_Suc_eq, blast) 

295 

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

297 
by (simp add: lessThan_def atMost_def less_Suc_eq_le) 

298 

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

300 
by blast 

301 

15047  302 
subsubsection {* The Constant @{term greaterThan} *} 
303 

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

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

307 
done 

308 

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

310 
apply (simp add: greaterThan_def) 

311 
apply (auto elim: linorder_neqE) 

312 
done 

313 

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

315 
by blast 

316 

15047  317 
subsubsection {* The Constant @{term atLeast} *} 
318 

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

321 

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

323 
apply (simp add: atLeast_def) 

324 
apply (simp add: Suc_le_eq) 

325 
apply (simp add: order_le_less, blast) 

326 
done 

327 

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

329 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

330 

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

332 
by blast 

333 

15047  334 
subsubsection {* The Constant @{term atMost} *} 
335 

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

338 

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

340 
apply (simp add: atMost_def) 

341 
apply (simp add: less_Suc_eq order_le_less, blast) 

342 
done 

343 

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

345 
by blast 

346 

15047  347 
subsubsection {* The Constant @{term atLeastLessThan} *} 
348 

28068  349 
text{*The orientation of the following 2 rules is tricky. The lhs is 
24449  350 
defined in terms of the rhs. Hence the chosen orientation makes sense 
351 
in this theory  the reverse orientation complicates proofs (eg 

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

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

354 
specific concept to a more general one. *} 

28068  355 

15047  356 
lemma atLeast0LessThan: "{0::nat..<n} = {..<n}" 
15042  357 
by(simp add:lessThan_def atLeastLessThan_def) 
24449  358 

28068  359 
lemma atLeast0AtMost: "{0..n::nat} = {..n}" 
360 
by(simp add:atMost_def atLeastAtMost_def) 

361 

31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31509
diff
changeset

362 
declare atLeast0LessThan[symmetric, code_unfold] 
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31509
diff
changeset

363 
atLeast0AtMost[symmetric, code_unfold] 
24449  364 

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

15047  366 
by (simp add: atLeastLessThan_def) 
24449  367 

15047  368 
subsubsection {* Intervals of nats with @{term Suc} *} 
369 

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

371 
lemma atLeastLessThanSuc: 

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

373 
by (auto simp add: atLeastLessThan_def) 
15047  374 

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

375 
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 
15047  376 
by (auto simp add: atLeastLessThan_def) 
16041  377 
(* 
15047  378 
lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}" 
379 
by (induct k, simp_all add: atLeastLessThanSuc) 

380 

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

382 
by (auto simp add: atLeastLessThan_def) 

16041  383 
*) 
15045  384 
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" 
14485  385 
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) 
386 

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

387 
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

388 
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
14485  389 
greaterThanAtMost_def) 
390 

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

391 
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

392 
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
14485  393 
greaterThanLessThan_def) 
394 

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

397 

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

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

399 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

413 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

427 

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

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

429 
"Suc ` {i..j} = {Suc i..Suc j}" 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29960
diff
changeset

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

431 

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

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

433 
"Suc ` {i..<j} = {Suc i..<Suc j}" 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29960
diff
changeset

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

435 

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

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

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

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

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

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

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

442 

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

443 

14485  444 
subsubsection {* Finiteness *} 
445 

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

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

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

451 

452 
lemma finite_greaterThanLessThan [iff]: 

15045  453 
fixes l :: nat shows "finite {l<..<u}" 
14485  454 
by (simp add: greaterThanLessThan_def) 
455 

456 
lemma finite_atLeastLessThan [iff]: 

15045  457 
fixes l :: nat shows "finite {l..<u}" 
14485  458 
by (simp add: atLeastLessThan_def) 
459 

460 
lemma finite_greaterThanAtMost [iff]: 

15045  461 
fixes l :: nat shows "finite {l<..u}" 
14485  462 
by (simp add: greaterThanAtMost_def) 
463 

464 
lemma finite_atLeastAtMost [iff]: 

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

466 
by (simp add: atLeastAtMost_def) 

467 

28068  468 
text {* A bounded set of natural numbers is finite. *} 
14485  469 
lemma bounded_nat_set_is_finite: 
24853  470 
"(ALL i:N. i < (n::nat)) ==> finite N" 
28068  471 
apply (rule finite_subset) 
472 
apply (rule_tac [2] finite_lessThan, auto) 

473 
done 

474 

31044  475 
text {* A set of natural numbers is finite iff it is bounded. *} 
476 
lemma finite_nat_set_iff_bounded: 

477 
"finite(N::nat set) = (EX m. ALL n:N. n<m)" (is "?F = ?B") 

478 
proof 

479 
assume f:?F show ?B 

480 
using Max_ge[OF `?F`, simplified less_Suc_eq_le[symmetric]] by blast 

481 
next 

482 
assume ?B show ?F using `?B` by(blast intro:bounded_nat_set_is_finite) 

483 
qed 

484 

485 
lemma finite_nat_set_iff_bounded_le: 

486 
"finite(N::nat set) = (EX m. ALL n:N. n<=m)" 

487 
apply(simp add:finite_nat_set_iff_bounded) 

488 
apply(blast dest:less_imp_le_nat le_imp_less_Suc) 

489 
done 

490 

28068  491 
lemma finite_less_ub: 
492 
"!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}" 

493 
by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans) 

14485  494 

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

497 

498 
lemma subset_card_intvl_is_intvl: 

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

500 
proof cases 

501 
assume "finite A" 

502 
thus "PROP ?P" 

32006  503 
proof(induct A rule:finite_linorder_max_induct) 
24853  504 
case empty thus ?case by auto 
505 
next 

506 
case (insert A b) 

507 
moreover hence "b ~: A" by auto 

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

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

510 
ultimately show ?case by auto 

511 
qed 

512 
next 

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

514 
qed 

515 

516 

14485  517 
subsubsection {* Cardinality *} 
518 

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

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

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

524 

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

14485  527 
apply (erule ssubst, rule card_lessThan) 
15045  528 
apply (subgoal_tac "(%x. x + l) ` {..<ul} = {l..<u}") 
14485  529 
apply (erule subst) 
530 
apply (rule card_image) 

531 
apply (simp add: inj_on_def) 

532 
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) 

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

534 
apply arith 

535 
done 

536 

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

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

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

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

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

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

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

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

548 
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

549 
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

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

551 

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

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

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

554 
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

555 

31438  556 
lemma finite_same_card_bij: 
557 
"finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow> EX h. bij_betw h A B" 

558 
apply(drule ex_bij_betw_finite_nat) 

559 
apply(drule ex_bij_betw_nat_finite) 

560 
apply(auto intro!:bij_betw_trans) 

561 
done 

562 

563 
lemma ex_bij_betw_nat_finite_1: 

564 
"finite M \<Longrightarrow> \<exists>h. bij_betw h {1 .. card M} M" 

565 
by (rule finite_same_card_bij) auto 

566 

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

567 

14485  568 
subsection {* Intervals of integers *} 
569 

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

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

573 
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" 
14485  574 
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 
575 

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

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

577 
"{l+1..<u} = {l<..<u::int}" 
14485  578 
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 
579 

580 
subsubsection {* Finiteness *} 

581 

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

582 
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
15045  583 
{(0::int)..<u} = int ` {..<nat u}" 
14485  584 
apply (unfold image_def lessThan_def) 
585 
apply auto 

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

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

588 
done 

589 

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

593 
apply (rule finite_imageI) 

594 
apply auto 

595 
done 

596 

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

14485  599 
apply (erule subst) 
600 
apply (rule finite_imageI) 

601 
apply (rule finite_atLeastZeroLessThan_int) 

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

602 
apply (rule image_add_int_atLeastLessThan) 
14485  603 
done 
604 

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

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

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

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

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

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

24853  614 

14485  615 
subsubsection {* Cardinality *} 
616 

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

620 
apply (subst card_image) 

621 
apply (auto simp add: inj_on_def) 

622 
done 

623 

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

14485  626 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 
15045  627 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 
14485  628 
apply (erule subst) 
629 
apply (rule card_image) 

630 
apply (simp add: inj_on_def) 

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

631 
apply (rule image_add_int_atLeastLessThan) 
14485  632 
done 
633 

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

29667  635 
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 
636 
apply (auto simp add: algebra_simps) 

637 
done 

14485  638 

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

639 
lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u  l)" 
29667  640 
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) 
14485  641 

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

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

645 
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

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

647 
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

648 
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

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

650 

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

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

652 
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

653 
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

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

655 
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

656 
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

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

658 

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

659 
lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}" 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29960
diff
changeset

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

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

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

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

664 
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

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

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

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

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

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

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

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

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

673 

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

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

675 
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

676 
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

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

678 
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

679 
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

680 
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

681 
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

682 
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

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

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

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

686 
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

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

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

689 
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

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

691 

14485  692 

13850  693 
subsection {*Lemmas useful with the summation operator setsum*} 
694 

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

695 
text {* For examples, see Algebra/poly/UnivPoly2.thy *} 
13735  696 

14577  697 
subsubsection {* Disjoint Unions *} 
13735  698 

14577  699 
text {* Singletons and open intervals *} 
13735  700 

701 
lemma ivl_disj_un_singleton: 

15045  702 
"{l::'a::linorder} Un {l<..} = {l..}" 
703 
"{..<u} Un {u::'a::linorder} = {..u}" 

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

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

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

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

708 
by auto 
13735  709 

14577  710 
text {* One and twosided intervals *} 
13735  711 

712 
lemma ivl_disj_un_one: 

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

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

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

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

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

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

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

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

721 
by auto 
13735  722 

14577  723 
text {* Two and twosided intervals *} 
13735  724 

725 
lemma ivl_disj_un_two: 

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

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

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

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

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

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

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

734 
by auto 
13735  735 

736 
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two 

737 

14577  738 
subsubsection {* Disjoint Intersections *} 
13735  739 

14577  740 
text {* One and twosided intervals *} 
13735  741 

742 
lemma ivl_disj_int_one: 

15045  743 
"{..l::'a::order} Int {l<..<u} = {}" 
744 
"{..<l} Int {l..<u} = {}" 

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

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

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

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

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

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

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

751 
by auto 
13735  752 

14577  753 
text {* Two and twosided intervals *} 
13735  754 

755 
lemma ivl_disj_int_two: 

15045  756 
"{l::'a::order<..<m} Int {m..<u} = {}" 
757 
"{l<..m} Int {m<..<u} = {}" 

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

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

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

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

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

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

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

764 
by auto 
13735  765 

32456
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

766 
lemmas ivl_disj_int = ivl_disj_int_one ivl_disj_int_two 
13735  767 

15542  768 
subsubsection {* Some Differences *} 
769 

770 
lemma ivl_diff[simp]: 

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

772 
by(auto) 

773 

774 

775 
subsubsection {* Some Subset Conditions *} 

776 

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

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

780 
apply(rule ccontr) 

781 
apply(insert linorder_le_less_linear[of i n]) 

782 
apply(clarsimp simp:linorder_not_le) 

783 
apply(fastsimp) 

784 
done 

785 

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

786 

15042  787 
subsection {* Summation indexed over intervals *} 
788 

789 
syntax 

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

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

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

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

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

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

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

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

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

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

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

813 

15048  814 
translations 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28068
diff
changeset

815 
"\<Sum>x=a..b. t" == "CONST setsum (%x. t) {a..b}" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28068
diff
changeset

816 
"\<Sum>x=a..<b. t" == "CONST setsum (%x. t) {a..<b}" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28068
diff
changeset

817 
"\<Sum>i\<le>n. t" == "CONST setsum (\<lambda>i. t) {..n}" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28068
diff
changeset

818 
"\<Sum>i<n. t" == "CONST setsum (\<lambda>i. t) {..<n}" 
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

819 

15052  820 
text{* The above introduces some pretty alternative syntaxes for 
15056  821 
summation over intervals: 
15052  822 
\begin{center} 
823 
\begin{tabular}{lll} 

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

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

16052  827 
@{term[source]"\<Sum>x\<in>{..b}. e"} & @{term"\<Sum>x\<le>b. e"} & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\ 
15056  828 
@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"} 
15052  829 
\end{tabular} 
830 
\end{center} 

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

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

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

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

15052  838 

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

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

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

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

843 

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

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

847 
the context. *} 

848 

849 
lemma setsum_ivl_cong: 

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

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

852 
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

853 

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

856 

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

859 

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

862 

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

866 

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

16041  870 
(* 
15561  871 
lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==> 
872 
(\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)" 

873 
by (auto simp:add_ac atLeastAtMostSuc_conv) 

16041  874 
*) 
28068  875 

876 
lemma setsum_head: 

877 
fixes n :: nat 

878 
assumes mn: "m <= n" 

879 
shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs") 

880 
proof  

881 
from mn 

882 
have "{m..n} = {m} \<union> {m<..n}" 

883 
by (auto intro: ivl_disj_un_singleton) 

884 
hence "?lhs = (\<Sum>x\<in>{m} \<union> {m<..n}. P x)" 

885 
by (simp add: atLeast0LessThan) 

886 
also have "\<dots> = ?rhs" by simp 

887 
finally show ?thesis . 

888 
qed 

889 

890 
lemma setsum_head_Suc: 

891 
"m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {Suc m..n}" 

892 
by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost) 

893 

894 
lemma setsum_head_upt_Suc: 

895 
"m < n \<Longrightarrow> setsum f {m..<n} = f m + setsum f {Suc m..<n}" 

30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29960
diff
changeset

896 
apply(insert setsum_head_Suc[of m "n  Suc 0" f]) 
29667  897 
apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps) 
28068  898 
done 
899 

31501  900 
lemma setsum_ub_add_nat: assumes "(m::nat) \<le> n + 1" 
901 
shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}" 

902 
proof 

903 
have "{m .. n+p} = {m..n} \<union> {n+1..n+p}" using `m \<le> n+1` by auto 

904 
thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint 

905 
atLeastSucAtMost_greaterThanAtMost) 

906 
qed 

28068  907 

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

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

911 

912 
lemma setsum_diff_nat_ivl: 

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

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

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

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

917 
apply (simp add: add_ac) 

918 
done 

919 

31505  920 
lemma setsum_natinterval_difff: 
921 
fixes f:: "nat \<Rightarrow> ('a::ab_group_add)" 

922 
shows "setsum (\<lambda>k. f k  f(k + 1)) {(m::nat) .. n} = 

923 
(if m <= n then f m  f(n + 1) else 0)" 

924 
by (induct n, auto simp add: algebra_simps not_le le_Suc_eq) 

925 

31509  926 
lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def] 
927 

928 
lemma setsum_setsum_restrict: 

929 
"finite S \<Longrightarrow> finite T \<Longrightarrow> setsum (\<lambda>x. setsum (\<lambda>y. f x y) {y. y\<in> T \<and> R x y}) S = setsum (\<lambda>y. setsum (\<lambda>x. f x y) {x. x \<in> S \<and> R x y}) T" 

930 
by (simp add: setsum_restrict_set'[unfolded mem_def] mem_def) 

931 
(rule setsum_commute) 

932 

933 
lemma setsum_image_gen: assumes fS: "finite S" 

934 
shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" 

935 
proof 

936 
{ fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto } 

937 
hence "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S" 

938 
by simp 

939 
also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" 

940 
by (rule setsum_setsum_restrict[OF fS finite_imageI[OF fS]]) 

941 
finally show ?thesis . 

942 
qed 

943 

944 
lemma setsum_multicount_gen: 

945 
assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)" 

946 
shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" (is "?l = ?r") 

947 
proof 

948 
have "?l = setsum (\<lambda>i. setsum (\<lambda>x.1) {j\<in>t. R i j}) s" by auto 

949 
also have "\<dots> = ?r" unfolding setsum_setsum_restrict[OF assms(12)] 

950 
using assms(3) by auto 

951 
finally show ?thesis . 

952 
qed 

953 

954 
lemma setsum_multicount: 

955 
assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)" 

956 
shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r") 

957 
proof 

958 
have "?l = setsum (\<lambda>i. k) T" by(rule setsum_multicount_gen)(auto simp:assms) 

959 
also have "\<dots> = ?r" by(simp add: setsum_constant mult_commute) 

960 
finally show ?thesis by auto 

961 
qed 

962 

28068  963 

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

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

965 

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

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

969 

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

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

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

972 
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

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

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

975 

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

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

977 
"setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}" 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29960
diff
changeset

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

979 

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

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

981 
"setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}" 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29960
diff
changeset

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

983 

28068  984 
lemma setsum_shift_lb_Suc0_0: 
985 
"f(0::nat) = (0::nat) \<Longrightarrow> setsum f {Suc 0..k} = setsum f {0..k}" 

986 
by(simp add:setsum_head_Suc) 

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

987 

28068  988 
lemma setsum_shift_lb_Suc0_0_upt: 
989 
"f(0::nat) = 0 \<Longrightarrow> setsum f {Suc 0..<k} = setsum f {0..<k}" 

990 
apply(cases k)apply simp 

991 
apply(simp add:setsum_head_upt_Suc) 

992 
done 

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

993 

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

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

995 

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

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

997 
"x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = 
31017  998 
(x ^ n  1) / (x  1::'a::{field})" 
23496  999 
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

1000 

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

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

1002 

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

1003 
lemma gauss_sum: 
23277  1004 
"((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

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

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

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

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

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

1010 
case (Suc n) 
29667  1011 
then show ?case by (simp add: algebra_simps) 
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

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

1013 

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

1014 
theorem arith_series_general: 
23277  1015 
"((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

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

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

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

1019 
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

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

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

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

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

1024 
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

1025 
also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))" 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29960
diff
changeset

1026 
unfolding One_nat_def 
28068  1027 
by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac) 
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1028 
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

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

1030 
also from ngt1 have "{1..<n} = {1..n  1}" 
28068  1031 
by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost) 
1032 
also from ngt1 

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

1033 
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)" 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29960
diff
changeset

1034 
by (simp only: mult_ac gauss_sum [of "n  1"], unfold One_nat_def) 
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

1035 
(simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]]) 
29667  1036 
finally show ?thesis by (simp add: algebra_simps) 
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

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

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

1039 
hence "n = 1 \<or> n = 0" by auto 
29667  1040 
thus ?thesis by (auto simp: algebra_simps) 
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

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

1042 

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

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

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

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

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

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

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

1049 
by (rule arith_series_general) 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29960
diff
changeset

1050 
thus ?thesis 
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29960
diff
changeset

1051 
unfolding One_nat_def by (auto simp add: of_nat_id) 
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

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

1053 

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

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

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

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

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

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

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

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

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

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

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

1064 

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

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

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

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

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

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

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

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

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

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

1074 

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

1075 
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

1076 
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

1077 

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

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

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

1080 
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

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

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

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

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

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

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

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

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

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

1090 

29960
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1091 
subsection {* Products indexed over intervals *} 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1092 

9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1093 
syntax 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1094 
"_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1095 
"_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1096 
"_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<_./ _)" [0,0,10] 10) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1097 
"_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<=_./ _)" [0,0,10] 10) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1098 
syntax (xsymbols) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1099 
"_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1100 
"_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1101 
"_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1102 
"_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1103 
syntax (HTML output) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1104 
"_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1105 
"_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1106 
"_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1107 
"_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1108 
syntax (latex_prod output) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1109 
"_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1110 
("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1111 
"_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1112 
("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1113 
"_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1114 
("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1115 
"_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1116 
("(3\<^raw:$\prod_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10) 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1117 

9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1118 
translations 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1119 
"\<Prod>x=a..b. t" == "CONST setprod (%x. t) {a..b}" 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1120 
"\<Prod>x=a..<b. t" == "CONST setprod (%x. t) {a..<b}" 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1121 
"\<Prod>i\<le>n. t" == "CONST setprod (\<lambda>i. t) {..n}" 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1122 
"\<Prod>i<n. t" == "CONST setprod (\<lambda>i. t) {..<n}" 
9d5c6f376768
Syntactic support for products over set intervals
paulson
parents:
29920
diff
changeset

1123 

8924  1124 
end 