author  nipkow 
Fri, 28 Aug 2009 18:52:41 +0200  
changeset 32436  10cd49e0c067 
parent 32408  a1a85b0a26f7 
child 32456  341c83339aeb 
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 

14485  254 
subsection {* Intervals of natural numbers *} 
255 

15047  256 
subsubsection {* The Constant @{term lessThan} *} 
257 

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

260 

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

262 
by (simp add: lessThan_def less_Suc_eq, blast) 

263 

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

265 
by (simp add: lessThan_def atMost_def less_Suc_eq_le) 

266 

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

268 
by blast 

269 

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

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

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

275 
done 

276 

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

278 
apply (simp add: greaterThan_def) 

279 
apply (auto elim: linorder_neqE) 

280 
done 

281 

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

283 
by blast 

284 

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

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

289 

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

291 
apply (simp add: atLeast_def) 

292 
apply (simp add: Suc_le_eq) 

293 
apply (simp add: order_le_less, blast) 

294 
done 

295 

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

297 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

298 

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

300 
by blast 

301 

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

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

306 

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

308 
apply (simp add: atMost_def) 

309 
apply (simp add: less_Suc_eq order_le_less, blast) 

310 
done 

311 

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

313 
by blast 

314 

15047  315 
subsubsection {* The Constant @{term atLeastLessThan} *} 
316 

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

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

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

322 
specific concept to a more general one. *} 

28068  323 

15047  324 
lemma atLeast0LessThan: "{0::nat..<n} = {..<n}" 
15042  325 
by(simp add:lessThan_def atLeastLessThan_def) 
24449  326 

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

329 

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

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

331 
atLeast0AtMost[symmetric, code_unfold] 
24449  332 

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

15047  334 
by (simp add: atLeastLessThan_def) 
24449  335 

15047  336 
subsubsection {* Intervals of nats with @{term Suc} *} 
337 

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

339 
lemma atLeastLessThanSuc: 

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

341 
by (auto simp add: atLeastLessThan_def) 
15047  342 

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

343 
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 
15047  344 
by (auto simp add: atLeastLessThan_def) 
16041  345 
(* 
15047  346 
lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}" 
347 
by (induct k, simp_all add: atLeastLessThanSuc) 

348 

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

350 
by (auto simp add: atLeastLessThan_def) 

16041  351 
*) 
15045  352 
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" 
14485  353 
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) 
354 

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

355 
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

356 
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
14485  357 
greaterThanAtMost_def) 
358 

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

359 
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

360 
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
14485  361 
greaterThanLessThan_def) 
362 

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

365 

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

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

367 

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

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

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

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

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

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

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

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

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

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

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

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

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

380 
qed 
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_atLeastLessThan: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

395 

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

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

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

398 
using image_add_atLeastAtMost[where k="Suc 0"] by simp 
16733
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 
corollary image_Suc_atLeastLessThan[simp]: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

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

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

403 

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

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

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

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

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

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

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

410 

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

411 

14485  412 
subsubsection {* Finiteness *} 
413 

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

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

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

419 

420 
lemma finite_greaterThanLessThan [iff]: 

15045  421 
fixes l :: nat shows "finite {l<..<u}" 
14485  422 
by (simp add: greaterThanLessThan_def) 
423 

424 
lemma finite_atLeastLessThan [iff]: 

15045  425 
fixes l :: nat shows "finite {l..<u}" 
14485  426 
by (simp add: atLeastLessThan_def) 
427 

428 
lemma finite_greaterThanAtMost [iff]: 

15045  429 
fixes l :: nat shows "finite {l<..u}" 
14485  430 
by (simp add: greaterThanAtMost_def) 
431 

432 
lemma finite_atLeastAtMost [iff]: 

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

434 
by (simp add: atLeastAtMost_def) 

435 

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

441 
done 

442 

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

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

446 
proof 

447 
assume f:?F show ?B 

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

449 
next 

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

451 
qed 

452 

453 
lemma finite_nat_set_iff_bounded_le: 

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

455 
apply(simp add:finite_nat_set_iff_bounded) 

456 
apply(blast dest:less_imp_le_nat le_imp_less_Suc) 

457 
done 

458 

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

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

14485  462 

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

465 

466 
lemma subset_card_intvl_is_intvl: 

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

468 
proof cases 

469 
assume "finite A" 

470 
thus "PROP ?P" 

32006  471 
proof(induct A rule:finite_linorder_max_induct) 
24853  472 
case empty thus ?case by auto 
473 
next 

474 
case (insert A b) 

475 
moreover hence "b ~: A" by auto 

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

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

478 
ultimately show ?case by auto 

479 
qed 

480 
next 

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

482 
qed 

483 

484 

14485  485 
subsubsection {* Cardinality *} 
486 

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

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

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

492 

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

14485  495 
apply (erule ssubst, rule card_lessThan) 
15045  496 
apply (subgoal_tac "(%x. x + l) ` {..<ul} = {l..<u}") 
14485  497 
apply (erule subst) 
498 
apply (rule card_image) 

499 
apply (simp add: inj_on_def) 

500 
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) 

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

502 
apply arith 

503 
done 

504 

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

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

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

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

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

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

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

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

516 
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

517 
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

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

519 

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

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

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

522 
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

523 

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

526 
apply(drule ex_bij_betw_finite_nat) 

527 
apply(drule ex_bij_betw_nat_finite) 

528 
apply(auto intro!:bij_betw_trans) 

529 
done 

530 

531 
lemma ex_bij_betw_nat_finite_1: 

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

533 
by (rule finite_same_card_bij) auto 

534 

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

535 

14485  536 
subsection {* Intervals of integers *} 
537 

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

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

541 
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" 
14485  542 
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 
543 

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

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

545 
"{l+1..<u} = {l<..<u::int}" 
14485  546 
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 
547 

548 
subsubsection {* Finiteness *} 

549 

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

550 
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
15045  551 
{(0::int)..<u} = int ` {..<nat u}" 
14485  552 
apply (unfold image_def lessThan_def) 
553 
apply auto 

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

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

556 
done 

557 

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

561 
apply (rule finite_imageI) 

562 
apply auto 

563 
done 

564 

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

14485  567 
apply (erule subst) 
568 
apply (rule finite_imageI) 

569 
apply (rule finite_atLeastZeroLessThan_int) 

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

570 
apply (rule image_add_int_atLeastLessThan) 
14485  571 
done 
572 

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

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

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

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

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

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

24853  582 

14485  583 
subsubsection {* Cardinality *} 
584 

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

588 
apply (subst card_image) 

589 
apply (auto simp add: inj_on_def) 

590 
done 

591 

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

14485  594 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 
15045  595 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 
14485  596 
apply (erule subst) 
597 
apply (rule card_image) 

598 
apply (simp add: inj_on_def) 

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

599 
apply (rule image_add_int_atLeastLessThan) 
14485  600 
done 
601 

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

29667  603 
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 
604 
apply (auto simp add: algebra_simps) 

605 
done 

14485  606 

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

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

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

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

613 
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

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

615 
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

616 
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

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

618 

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

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

620 
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

621 
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

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

623 
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

624 
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

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

626 

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

627 
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

628 
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

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

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

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

632 
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

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

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

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

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

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

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

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

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

641 

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

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

643 
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

644 
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

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

646 
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

647 
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

648 
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

649 
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

650 
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

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

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

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

654 
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

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

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

657 
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

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

659 

14485  660 

13850  661 
subsection {*Lemmas useful with the summation operator setsum*} 
662 

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

663 
text {* For examples, see Algebra/poly/UnivPoly2.thy *} 
13735  664 

14577  665 
subsubsection {* Disjoint Unions *} 
13735  666 

14577  667 
text {* Singletons and open intervals *} 
13735  668 

669 
lemma ivl_disj_un_singleton: 

15045  670 
"{l::'a::linorder} Un {l<..} = {l..}" 
671 
"{..<u} Un {u::'a::linorder} = {..u}" 

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

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

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

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

676 
by auto 
13735  677 

14577  678 
text {* One and twosided intervals *} 
13735  679 

680 
lemma ivl_disj_un_one: 

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

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

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

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

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

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

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

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

689 
by auto 
13735  690 

14577  691 
text {* Two and twosided intervals *} 
13735  692 

693 
lemma ivl_disj_un_two: 

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

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

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

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

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

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

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

702 
by auto 
13735  703 

704 
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two 

705 

14577  706 
subsubsection {* Disjoint Intersections *} 
13735  707 

14577  708 
text {* Singletons and open intervals *} 
13735  709 

710 
lemma ivl_disj_int_singleton: 

15045  711 
"{l::'a::order} Int {l<..} = {}" 
712 
"{..<u} Int {u} = {}" 

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

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

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

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

13735  717 
by simp+ 
718 

14577  719 
text {* One and twosided intervals *} 
13735  720 

721 
lemma ivl_disj_int_one: 

15045  722 
"{..l::'a::order} Int {l<..<u} = {}" 
723 
"{..<l} Int {l..<u} = {}" 

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

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

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

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

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

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

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

730 
by auto 
13735  731 

14577  732 
text {* Two and twosided intervals *} 
13735  733 

734 
lemma ivl_disj_int_two: 

15045  735 
"{l::'a::order<..<m} Int {m..<u} = {}" 
736 
"{l<..m} Int {m<..<u} = {}" 

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

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

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

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

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

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

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

743 
by auto 
13735  744 

745 
lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two 

746 

15542  747 
subsubsection {* Some Differences *} 
748 

749 
lemma ivl_diff[simp]: 

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

751 
by(auto) 

752 

753 

754 
subsubsection {* Some Subset Conditions *} 

755 

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

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

759 
apply(rule ccontr) 

760 
apply(insert linorder_le_less_linear[of i n]) 

761 
apply(clarsimp simp:linorder_not_le) 

762 
apply(fastsimp) 

763 
done 

764 

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

765 

15042  766 
subsection {* Summation indexed over intervals *} 
767 

768 
syntax 

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

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

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

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

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

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

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

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

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

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

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

792 

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

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

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

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

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

798 

15052  799 
text{* The above introduces some pretty alternative syntaxes for 
15056  800 
summation over intervals: 
15052  801 
\begin{center} 
802 
\begin{tabular}{lll} 

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

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

16052  806 
@{term[source]"\<Sum>x\<in>{..b}. e"} & @{term"\<Sum>x\<le>b. e"} & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\ 
15056  807 
@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"} 
15052  808 
\end{tabular} 
809 
\end{center} 

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

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

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

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

15052  817 

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

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

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

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

822 

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

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

826 
the context. *} 

827 

828 
lemma setsum_ivl_cong: 

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

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

831 
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

832 

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

835 

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

838 

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

841 

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

845 

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

16041  849 
(* 
15561  850 
lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==> 
851 
(\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)" 

852 
by (auto simp:add_ac atLeastAtMostSuc_conv) 

16041  853 
*) 
28068  854 

855 
lemma setsum_head: 

856 
fixes n :: nat 

857 
assumes mn: "m <= n" 

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

859 
proof  

860 
from mn 

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

862 
by (auto intro: ivl_disj_un_singleton) 

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

864 
by (simp add: atLeast0LessThan) 

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

866 
finally show ?thesis . 

867 
qed 

868 

869 
lemma setsum_head_Suc: 

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

871 
by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost) 

872 

873 
lemma setsum_head_upt_Suc: 

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

875 
apply(insert setsum_head_Suc[of m "n  Suc 0" f]) 
29667  876 
apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps) 
28068  877 
done 
878 

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

881 
proof 

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

883 
thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint 

884 
atLeastSucAtMost_greaterThanAtMost) 

885 
qed 

28068  886 

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

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

890 

891 
lemma setsum_diff_nat_ivl: 

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

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

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

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

896 
apply (simp add: add_ac) 

897 
done 

898 

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

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

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

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

904 

31509  905 
lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def] 
906 

907 
lemma setsum_setsum_restrict: 

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

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

910 
(rule setsum_commute) 

911 

912 
lemma setsum_image_gen: assumes fS: "finite S" 

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

914 
proof 

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

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

917 
by simp 

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

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

920 
finally show ?thesis . 

921 
qed 

922 

923 
lemma setsum_multicount_gen: 

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

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

926 
proof 

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

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

929 
using assms(3) by auto 

930 
finally show ?thesis . 

931 
qed 

932 

933 
lemma setsum_multicount: 

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

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

936 
proof 

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

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

939 
finally show ?thesis by auto 

940 
qed 

941 

28068  942 

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

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

944 

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

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

948 

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

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

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

951 
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

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

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

954 

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

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

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

957 
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

958 

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

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

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

961 
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

962 

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

965 
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

966 

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

969 
apply(cases k)apply simp 

970 
apply(simp add:setsum_head_upt_Suc) 

971 
done 

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

972 

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

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

974 

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

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

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

979 

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

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

981 

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

982 
lemma gauss_sum: 
23277  983 
"((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

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

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

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

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

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

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

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

992 

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

993 
theorem arith_series_general: 
23277  994 
"((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

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

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

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

998 
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

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

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

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

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

1003 
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

1004 
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

1005 
unfolding One_nat_def 
28068  1006 
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

1007 
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

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

1009 
also from ngt1 have "{1..<n} = {1..n  1}" 
28068  1010 
by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost) 
1011 
also from ngt1 

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

1012 
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

1013 
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

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

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

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

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

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

1021 

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

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

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

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

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

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

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

1028 
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

1029 
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

1030 
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

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

1032 

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

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

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

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

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

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

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

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

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

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

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

1043 

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

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

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

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

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

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

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

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

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

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

1053 

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

1054 
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

1055 
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

1056 

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

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

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

1059 
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

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

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

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

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

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

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

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

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

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

1069 

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

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

1071 

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

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

1073 
"_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

1074 
"_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

1075 
"_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

1076 
"_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

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

1078 
"_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

1079 
"_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

1080 
"_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

1081 
"_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

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

1083 
"_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

1084 
"_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

1085 
"_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

1086 
"_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

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

1088 
"_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

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

1090 
"_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

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

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

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

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

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

1096 

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

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

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

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

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

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

1102 

8924  1103 
end 