author  nipkow 
Mon, 08 Jun 2009 20:43:57 +0200  
changeset 31509  00ede188c5d6 
parent 31505  6f589131ba94 
child 31998  2c7a24f74db9 
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 

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

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

24691  187 
end 
13735  188 

15554  189 
subsubsection{* Emptyness and singletons *} 
190 

24691  191 
context order 
192 
begin 

15554  193 

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

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

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

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

25062  206 
lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}" 
24691  207 
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) 
208 

209 
end 

14485  210 

211 
subsection {* Intervals of natural numbers *} 

212 

15047  213 
subsubsection {* The Constant @{term lessThan} *} 
214 

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

217 

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

219 
by (simp add: lessThan_def less_Suc_eq, blast) 

220 

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

222 
by (simp add: lessThan_def atMost_def less_Suc_eq_le) 

223 

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

225 
by blast 

226 

15047  227 
subsubsection {* The Constant @{term greaterThan} *} 
228 

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

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

232 
done 

233 

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

235 
apply (simp add: greaterThan_def) 

236 
apply (auto elim: linorder_neqE) 

237 
done 

238 

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

240 
by blast 

241 

15047  242 
subsubsection {* The Constant @{term atLeast} *} 
243 

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

246 

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

248 
apply (simp add: atLeast_def) 

249 
apply (simp add: Suc_le_eq) 

250 
apply (simp add: order_le_less, blast) 

251 
done 

252 

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

254 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

255 

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

257 
by blast 

258 

15047  259 
subsubsection {* The Constant @{term atMost} *} 
260 

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

263 

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

265 
apply (simp add: atMost_def) 

266 
apply (simp add: less_Suc_eq order_le_less, blast) 

267 
done 

268 

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

270 
by blast 

271 

15047  272 
subsubsection {* The Constant @{term atLeastLessThan} *} 
273 

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

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

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

279 
specific concept to a more general one. *} 

28068  280 

15047  281 
lemma atLeast0LessThan: "{0::nat..<n} = {..<n}" 
15042  282 
by(simp add:lessThan_def atLeastLessThan_def) 
24449  283 

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

286 

24449  287 
declare atLeast0LessThan[symmetric, code unfold] 
28068  288 
atLeast0AtMost[symmetric, code unfold] 
24449  289 

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

15047  291 
by (simp add: atLeastLessThan_def) 
24449  292 

15047  293 
subsubsection {* Intervals of nats with @{term Suc} *} 
294 

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

296 
lemma atLeastLessThanSuc: 

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

298 
by (auto simp add: atLeastLessThan_def) 
15047  299 

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

300 
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 
15047  301 
by (auto simp add: atLeastLessThan_def) 
16041  302 
(* 
15047  303 
lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}" 
304 
by (induct k, simp_all add: atLeastLessThanSuc) 

305 

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

307 
by (auto simp add: atLeastLessThan_def) 

16041  308 
*) 
15045  309 
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" 
14485  310 
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) 
311 

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

312 
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

313 
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
14485  314 
greaterThanAtMost_def) 
315 

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

316 
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

317 
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
14485  318 
greaterThanLessThan_def) 
319 

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

322 

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

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

324 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

338 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

352 

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

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

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

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

356 

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

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

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

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

360 

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

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

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

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

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

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

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

14485  369 
subsubsection {* Finiteness *} 
370 

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

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

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

376 

377 
lemma finite_greaterThanLessThan [iff]: 

15045  378 
fixes l :: nat shows "finite {l<..<u}" 
14485  379 
by (simp add: greaterThanLessThan_def) 
380 

381 
lemma finite_atLeastLessThan [iff]: 

15045  382 
fixes l :: nat shows "finite {l..<u}" 
14485  383 
by (simp add: atLeastLessThan_def) 
384 

385 
lemma finite_greaterThanAtMost [iff]: 

15045  386 
fixes l :: nat shows "finite {l<..u}" 
14485  387 
by (simp add: greaterThanAtMost_def) 
388 

389 
lemma finite_atLeastAtMost [iff]: 

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

391 
by (simp add: atLeastAtMost_def) 

392 

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

398 
done 

399 

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

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

403 
proof 

404 
assume f:?F show ?B 

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

406 
next 

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

408 
qed 

409 

410 
lemma finite_nat_set_iff_bounded_le: 

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

412 
apply(simp add:finite_nat_set_iff_bounded) 

413 
apply(blast dest:less_imp_le_nat le_imp_less_Suc) 

414 
done 

415 

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

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

14485  419 

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

422 

423 
lemma subset_card_intvl_is_intvl: 

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

425 
proof cases 

426 
assume "finite A" 

427 
thus "PROP ?P" 

428 
proof(induct A rule:finite_linorder_induct) 

429 
case empty thus ?case by auto 

430 
next 

431 
case (insert A b) 

432 
moreover hence "b ~: A" by auto 

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

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

435 
ultimately show ?case by auto 

436 
qed 

437 
next 

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

439 
qed 

440 

441 

14485  442 
subsubsection {* Cardinality *} 
443 

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

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

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

449 

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

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

456 
apply (simp add: inj_on_def) 

457 
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) 

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

459 
apply arith 

460 
done 

461 

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

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

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

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

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

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

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

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

473 
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

474 
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

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

476 

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

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

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

479 
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

480 

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

483 
apply(drule ex_bij_betw_finite_nat) 

484 
apply(drule ex_bij_betw_nat_finite) 

485 
apply(auto intro!:bij_betw_trans) 

486 
done 

487 

488 
lemma ex_bij_betw_nat_finite_1: 

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

490 
by (rule finite_same_card_bij) auto 

491 

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

492 

14485  493 
subsection {* Intervals of integers *} 
494 

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

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

498 
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" 
14485  499 
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 
500 

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

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

502 
"{l+1..<u} = {l<..<u::int}" 
14485  503 
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 
504 

505 
subsubsection {* Finiteness *} 

506 

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

507 
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
15045  508 
{(0::int)..<u} = int ` {..<nat u}" 
14485  509 
apply (unfold image_def lessThan_def) 
510 
apply auto 

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

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

513 
done 

514 

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

518 
apply (rule finite_imageI) 

519 
apply auto 

520 
done 

521 

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

14485  524 
apply (erule subst) 
525 
apply (rule finite_imageI) 

526 
apply (rule finite_atLeastZeroLessThan_int) 

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

527 
apply (rule image_add_int_atLeastLessThan) 
14485  528 
done 
529 

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

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

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

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

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

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

24853  539 

14485  540 
subsubsection {* Cardinality *} 
541 

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

545 
apply (subst card_image) 

546 
apply (auto simp add: inj_on_def) 

547 
done 

548 

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

14485  551 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 
15045  552 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 
14485  553 
apply (erule subst) 
554 
apply (rule card_image) 

555 
apply (simp add: inj_on_def) 

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

556 
apply (rule image_add_int_atLeastLessThan) 
14485  557 
done 
558 

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

29667  560 
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 
561 
apply (auto simp add: algebra_simps) 

562 
done 

14485  563 

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

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

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

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

570 
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

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

572 
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

573 
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

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

575 

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

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

577 
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

578 
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

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

580 
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

581 
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

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

583 

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

584 
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

585 
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

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

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

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

589 
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

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

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

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

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

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

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

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

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

598 

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

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

600 
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

601 
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

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

603 
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

604 
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

605 
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

606 
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

607 
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

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

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

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

611 
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

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

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

614 
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

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

616 

14485  617 

13850  618 
subsection {*Lemmas useful with the summation operator setsum*} 
619 

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

620 
text {* For examples, see Algebra/poly/UnivPoly2.thy *} 
13735  621 

14577  622 
subsubsection {* Disjoint Unions *} 
13735  623 

14577  624 
text {* Singletons and open intervals *} 
13735  625 

626 
lemma ivl_disj_un_singleton: 

15045  627 
"{l::'a::linorder} Un {l<..} = {l..}" 
628 
"{..<u} Un {u::'a::linorder} = {..u}" 

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

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

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

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

633 
by auto 
13735  634 

14577  635 
text {* One and twosided intervals *} 
13735  636 

637 
lemma ivl_disj_un_one: 

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

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

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

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

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

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

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

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

646 
by auto 
13735  647 

14577  648 
text {* Two and twosided intervals *} 
13735  649 

650 
lemma ivl_disj_un_two: 

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

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

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

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

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

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

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

659 
by auto 
13735  660 

661 
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two 

662 

14577  663 
subsubsection {* Disjoint Intersections *} 
13735  664 

14577  665 
text {* Singletons and open intervals *} 
13735  666 

667 
lemma ivl_disj_int_singleton: 

15045  668 
"{l::'a::order} Int {l<..} = {}" 
669 
"{..<u} Int {u} = {}" 

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

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

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

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

13735  674 
by simp+ 
675 

14577  676 
text {* One and twosided intervals *} 
13735  677 

678 
lemma ivl_disj_int_one: 

15045  679 
"{..l::'a::order} Int {l<..<u} = {}" 
680 
"{..<l} Int {l..<u} = {}" 

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

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

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

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

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

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

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

687 
by auto 
13735  688 

14577  689 
text {* Two and twosided intervals *} 
13735  690 

691 
lemma ivl_disj_int_two: 

15045  692 
"{l::'a::order<..<m} Int {m..<u} = {}" 
693 
"{l<..m} Int {m<..<u} = {}" 

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

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

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

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

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

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

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

700 
by auto 
13735  701 

702 
lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two 

703 

15542  704 
subsubsection {* Some Differences *} 
705 

706 
lemma ivl_diff[simp]: 

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

708 
by(auto) 

709 

710 

711 
subsubsection {* Some Subset Conditions *} 

712 

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

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

716 
apply(rule ccontr) 

717 
apply(insert linorder_le_less_linear[of i n]) 

718 
apply(clarsimp simp:linorder_not_le) 

719 
apply(fastsimp) 

720 
done 

721 

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

722 

15042  723 
subsection {* Summation indexed over intervals *} 
724 

725 
syntax 

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

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

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

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

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

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

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

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

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

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

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

749 

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

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

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

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

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

755 

15052  756 
text{* The above introduces some pretty alternative syntaxes for 
15056  757 
summation over intervals: 
15052  758 
\begin{center} 
759 
\begin{tabular}{lll} 

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

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

16052  763 
@{term[source]"\<Sum>x\<in>{..b}. e"} & @{term"\<Sum>x\<le>b. e"} & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\ 
15056  764 
@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"} 
15052  765 
\end{tabular} 
766 
\end{center} 

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

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

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

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

15052  774 

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

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

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

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

779 

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

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

783 
the context. *} 

784 

785 
lemma setsum_ivl_cong: 

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

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

788 
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

789 

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

792 

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

795 

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

798 

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

802 

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

16041  806 
(* 
15561  807 
lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==> 
808 
(\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)" 

809 
by (auto simp:add_ac atLeastAtMostSuc_conv) 

16041  810 
*) 
28068  811 

812 
lemma setsum_head: 

813 
fixes n :: nat 

814 
assumes mn: "m <= n" 

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

816 
proof  

817 
from mn 

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

819 
by (auto intro: ivl_disj_un_singleton) 

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

821 
by (simp add: atLeast0LessThan) 

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

823 
finally show ?thesis . 

824 
qed 

825 

826 
lemma setsum_head_Suc: 

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

828 
by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost) 

829 

830 
lemma setsum_head_upt_Suc: 

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

832 
apply(insert setsum_head_Suc[of m "n  Suc 0" f]) 
29667  833 
apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps) 
28068  834 
done 
835 

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

838 
proof 

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

840 
thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint 

841 
atLeastSucAtMost_greaterThanAtMost) 

842 
qed 

28068  843 

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

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

847 

848 
lemma setsum_diff_nat_ivl: 

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

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

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

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

853 
apply (simp add: add_ac) 

854 
done 

855 

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

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

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

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

861 

31509  862 
lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def] 
863 

864 
lemma setsum_setsum_restrict: 

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

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

867 
(rule setsum_commute) 

868 

869 
lemma setsum_image_gen: assumes fS: "finite S" 

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

871 
proof 

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

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

874 
by simp 

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

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

877 
finally show ?thesis . 

878 
qed 

879 

880 
lemma setsum_multicount_gen: 

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

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

883 
proof 

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

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

886 
using assms(3) by auto 

887 
finally show ?thesis . 

888 
qed 

889 

890 
lemma setsum_multicount: 

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

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

893 
proof 

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

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

896 
finally show ?thesis by auto 

897 
qed 

898 

28068  899 

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

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

901 

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

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

905 

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

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

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

908 
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

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

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

911 

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

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

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

914 
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

915 

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

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

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

918 
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

919 

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

922 
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

923 

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

926 
apply(cases k)apply simp 

927 
apply(simp add:setsum_head_upt_Suc) 

928 
done 

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

929 

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

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

931 

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

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

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

936 

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

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

938 

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

939 
lemma gauss_sum: 
23277  940 
"((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

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

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

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

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

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

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

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

949 

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

950 
theorem arith_series_general: 
23277  951 
"((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

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

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

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

955 
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

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

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

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

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

960 
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

961 
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

962 
unfolding One_nat_def 
28068  963 
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

964 
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

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

966 
also from ngt1 have "{1..<n} = {1..n  1}" 
28068  967 
by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost) 
968 
also from ngt1 

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

969 
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

970 
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

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

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

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

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

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

978 

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

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

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

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

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

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

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

985 
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

986 
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

987 
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

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

989 

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

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

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

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

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

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

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

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

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

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

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

1000 

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

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

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

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

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

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

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

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

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

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

1010 

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

1011 
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

1012 
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

1013 

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

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

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

1016 
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

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

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

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

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

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

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

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

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

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

1026 

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

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

1028 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1053 

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

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

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

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

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

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

1059 

8924  1060 
end 