author  nipkow 
Wed, 26 Aug 2009 10:48:12 +0200  
changeset 32400  6c62363cf0d7 
parent 32006  0e209ff7f236 
child 32408  a1a85b0a26f7 
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 

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

24691  191 
context order 
192 
begin 

15554  193 

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

196 
by(auto simp: atLeastAtMost_def atLeast_def atMost_def) 

197 

198 
lemma atLeastatMost_empty_iff[simp]: 

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

200 
by auto (blast intro: order_trans) 

201 

202 
lemma atLeastatMost_empty_iff2[simp]: 

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

204 
by auto (blast intro: order_trans) 

205 

206 
lemma atLeastLessThan_empty[simp]: 

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

208 
by(auto simp: atLeastLessThan_def) 

24691  209 

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

212 
by auto (blast intro: le_less_trans) 

213 

214 
lemma atLeastLessThan_empty_iff2[simp]: 

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

216 
by auto (blast intro: le_less_trans) 

15554  217 

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

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

223 

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

225 
by auto (blast intro: less_le_trans) 

226 

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

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

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

235 
unfolding atLeastAtMost_def atLeast_def atMost_def 

236 
by (blast intro: order_trans) 

237 

238 
lemma atLeastatMost_psubset_iff: 

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

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

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

242 

24691  243 
end 
14485  244 

245 
subsection {* Intervals of natural numbers *} 

246 

15047  247 
subsubsection {* The Constant @{term lessThan} *} 
248 

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

251 

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

253 
by (simp add: lessThan_def less_Suc_eq, blast) 

254 

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

256 
by (simp add: lessThan_def atMost_def less_Suc_eq_le) 

257 

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

259 
by blast 

260 

15047  261 
subsubsection {* The Constant @{term greaterThan} *} 
262 

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

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

266 
done 

267 

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

269 
apply (simp add: greaterThan_def) 

270 
apply (auto elim: linorder_neqE) 

271 
done 

272 

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

274 
by blast 

275 

15047  276 
subsubsection {* The Constant @{term atLeast} *} 
277 

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

280 

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

282 
apply (simp add: atLeast_def) 

283 
apply (simp add: Suc_le_eq) 

284 
apply (simp add: order_le_less, blast) 

285 
done 

286 

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

288 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

289 

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

291 
by blast 

292 

15047  293 
subsubsection {* The Constant @{term atMost} *} 
294 

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

297 

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

299 
apply (simp add: atMost_def) 

300 
apply (simp add: less_Suc_eq order_le_less, blast) 

301 
done 

302 

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

304 
by blast 

305 

15047  306 
subsubsection {* The Constant @{term atLeastLessThan} *} 
307 

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

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

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

313 
specific concept to a more general one. *} 

28068  314 

15047  315 
lemma atLeast0LessThan: "{0::nat..<n} = {..<n}" 
15042  316 
by(simp add:lessThan_def atLeastLessThan_def) 
24449  317 

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

320 

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

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

322 
atLeast0AtMost[symmetric, code_unfold] 
24449  323 

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

15047  325 
by (simp add: atLeastLessThan_def) 
24449  326 

15047  327 
subsubsection {* Intervals of nats with @{term Suc} *} 
328 

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

330 
lemma atLeastLessThanSuc: 

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

332 
by (auto simp add: atLeastLessThan_def) 
15047  333 

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

334 
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 
15047  335 
by (auto simp add: atLeastLessThan_def) 
16041  336 
(* 
15047  337 
lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}" 
338 
by (induct k, simp_all add: atLeastLessThanSuc) 

339 

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

341 
by (auto simp add: atLeastLessThan_def) 

16041  342 
*) 
15045  343 
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" 
14485  344 
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) 
345 

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

346 
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

347 
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
14485  348 
greaterThanAtMost_def) 
349 

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

350 
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

351 
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
14485  352 
greaterThanLessThan_def) 
353 

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

356 

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

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

358 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

372 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

386 

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

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

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

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

390 

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

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

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

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

394 

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

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

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

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

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

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

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

401 

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

402 

14485  403 
subsubsection {* Finiteness *} 
404 

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

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

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

410 

411 
lemma finite_greaterThanLessThan [iff]: 

15045  412 
fixes l :: nat shows "finite {l<..<u}" 
14485  413 
by (simp add: greaterThanLessThan_def) 
414 

415 
lemma finite_atLeastLessThan [iff]: 

15045  416 
fixes l :: nat shows "finite {l..<u}" 
14485  417 
by (simp add: atLeastLessThan_def) 
418 

419 
lemma finite_greaterThanAtMost [iff]: 

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

423 
lemma finite_atLeastAtMost [iff]: 

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

425 
by (simp add: atLeastAtMost_def) 

426 

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

432 
done 

433 

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

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

437 
proof 

438 
assume f:?F show ?B 

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

440 
next 

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

442 
qed 

443 

444 
lemma finite_nat_set_iff_bounded_le: 

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

446 
apply(simp add:finite_nat_set_iff_bounded) 

447 
apply(blast dest:less_imp_le_nat le_imp_less_Suc) 

448 
done 

449 

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

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

14485  453 

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

456 

457 
lemma subset_card_intvl_is_intvl: 

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

459 
proof cases 

460 
assume "finite A" 

461 
thus "PROP ?P" 

32006  462 
proof(induct A rule:finite_linorder_max_induct) 
24853  463 
case empty thus ?case by auto 
464 
next 

465 
case (insert A b) 

466 
moreover hence "b ~: A" by auto 

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

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

469 
ultimately show ?case by auto 

470 
qed 

471 
next 

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

473 
qed 

474 

475 

14485  476 
subsubsection {* Cardinality *} 
477 

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

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

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

483 

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

14485  486 
apply (erule ssubst, rule card_lessThan) 
15045  487 
apply (subgoal_tac "(%x. x + l) ` {..<ul} = {l..<u}") 
14485  488 
apply (erule subst) 
489 
apply (rule card_image) 

490 
apply (simp add: inj_on_def) 

491 
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) 

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

493 
apply arith 

494 
done 

495 

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

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

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

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

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

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

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

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

507 
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

508 
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

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

510 

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

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

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

513 
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

514 

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

517 
apply(drule ex_bij_betw_finite_nat) 

518 
apply(drule ex_bij_betw_nat_finite) 

519 
apply(auto intro!:bij_betw_trans) 

520 
done 

521 

522 
lemma ex_bij_betw_nat_finite_1: 

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

524 
by (rule finite_same_card_bij) auto 

525 

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

526 

14485  527 
subsection {* Intervals of integers *} 
528 

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

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

532 
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" 
14485  533 
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 
534 

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

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

536 
"{l+1..<u} = {l<..<u::int}" 
14485  537 
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 
538 

539 
subsubsection {* Finiteness *} 

540 

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

541 
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
15045  542 
{(0::int)..<u} = int ` {..<nat u}" 
14485  543 
apply (unfold image_def lessThan_def) 
544 
apply auto 

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

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

547 
done 

548 

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

552 
apply (rule finite_imageI) 

553 
apply auto 

554 
done 

555 

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

14485  558 
apply (erule subst) 
559 
apply (rule finite_imageI) 

560 
apply (rule finite_atLeastZeroLessThan_int) 

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

561 
apply (rule image_add_int_atLeastLessThan) 
14485  562 
done 
563 

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

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

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

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

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

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

24853  573 

14485  574 
subsubsection {* Cardinality *} 
575 

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

579 
apply (subst card_image) 

580 
apply (auto simp add: inj_on_def) 

581 
done 

582 

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

14485  585 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 
15045  586 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 
14485  587 
apply (erule subst) 
588 
apply (rule card_image) 

589 
apply (simp add: inj_on_def) 

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

590 
apply (rule image_add_int_atLeastLessThan) 
14485  591 
done 
592 

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

29667  594 
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 
595 
apply (auto simp add: algebra_simps) 

596 
done 

14485  597 

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

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

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

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

604 
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

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

606 
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

607 
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

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

609 

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

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

611 
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

612 
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

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

614 
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

615 
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

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

617 

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

618 
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

619 
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

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

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

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

623 
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

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

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

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

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

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

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

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

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

632 

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

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

634 
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

635 
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

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

637 
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

638 
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

639 
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

640 
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

641 
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

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

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

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

645 
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

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

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

648 
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

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

650 

14485  651 

13850  652 
subsection {*Lemmas useful with the summation operator setsum*} 
653 

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

654 
text {* For examples, see Algebra/poly/UnivPoly2.thy *} 
13735  655 

14577  656 
subsubsection {* Disjoint Unions *} 
13735  657 

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

660 
lemma ivl_disj_un_singleton: 

15045  661 
"{l::'a::linorder} Un {l<..} = {l..}" 
662 
"{..<u} Un {u::'a::linorder} = {..u}" 

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

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

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

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

667 
by auto 
13735  668 

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

671 
lemma ivl_disj_un_one: 

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

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

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

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

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

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

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

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

680 
by auto 
13735  681 

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

684 
lemma ivl_disj_un_two: 

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

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

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

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

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

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

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

693 
by auto 
13735  694 

695 
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two 

696 

14577  697 
subsubsection {* Disjoint Intersections *} 
13735  698 

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

701 
lemma ivl_disj_int_singleton: 

15045  702 
"{l::'a::order} Int {l<..} = {}" 
703 
"{..<u} Int {u} = {}" 

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

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

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

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

13735  708 
by simp+ 
709 

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

712 
lemma ivl_disj_int_one: 

15045  713 
"{..l::'a::order} Int {l<..<u} = {}" 
714 
"{..<l} Int {l..<u} = {}" 

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

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

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

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

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

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

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

721 
by auto 
13735  722 

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

725 
lemma ivl_disj_int_two: 

15045  726 
"{l::'a::order<..<m} Int {m..<u} = {}" 
727 
"{l<..m} Int {m<..<u} = {}" 

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

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

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

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

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

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

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

734 
by auto 
13735  735 

736 
lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two 

737 

15542  738 
subsubsection {* Some Differences *} 
739 

740 
lemma ivl_diff[simp]: 

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

742 
by(auto) 

743 

744 

745 
subsubsection {* Some Subset Conditions *} 

746 

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

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

750 
apply(rule ccontr) 

751 
apply(insert linorder_le_less_linear[of i n]) 

752 
apply(clarsimp simp:linorder_not_le) 

753 
apply(fastsimp) 

754 
done 

755 

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

756 

15042  757 
subsection {* Summation indexed over intervals *} 
758 

759 
syntax 

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

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

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

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

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

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

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

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

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

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

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

783 

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

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

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

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

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

789 

15052  790 
text{* The above introduces some pretty alternative syntaxes for 
15056  791 
summation over intervals: 
15052  792 
\begin{center} 
793 
\begin{tabular}{lll} 

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

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

16052  797 
@{term[source]"\<Sum>x\<in>{..b}. e"} & @{term"\<Sum>x\<le>b. e"} & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\ 
15056  798 
@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"} 
15052  799 
\end{tabular} 
800 
\end{center} 

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

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

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

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

15052  808 

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

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

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

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

813 

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

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

817 
the context. *} 

818 

819 
lemma setsum_ivl_cong: 

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

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

822 
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

823 

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

826 

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

829 

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

832 

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

836 

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

16041  840 
(* 
15561  841 
lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==> 
842 
(\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)" 

843 
by (auto simp:add_ac atLeastAtMostSuc_conv) 

16041  844 
*) 
28068  845 

846 
lemma setsum_head: 

847 
fixes n :: nat 

848 
assumes mn: "m <= n" 

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

850 
proof  

851 
from mn 

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

853 
by (auto intro: ivl_disj_un_singleton) 

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

855 
by (simp add: atLeast0LessThan) 

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

857 
finally show ?thesis . 

858 
qed 

859 

860 
lemma setsum_head_Suc: 

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

862 
by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost) 

863 

864 
lemma setsum_head_upt_Suc: 

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

866 
apply(insert setsum_head_Suc[of m "n  Suc 0" f]) 
29667  867 
apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps) 
28068  868 
done 
869 

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

872 
proof 

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

874 
thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint 

875 
atLeastSucAtMost_greaterThanAtMost) 

876 
qed 

28068  877 

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

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

881 

882 
lemma setsum_diff_nat_ivl: 

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

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

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

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

887 
apply (simp add: add_ac) 

888 
done 

889 

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

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

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

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

895 

31509  896 
lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def] 
897 

898 
lemma setsum_setsum_restrict: 

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

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

901 
(rule setsum_commute) 

902 

903 
lemma setsum_image_gen: assumes fS: "finite S" 

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

905 
proof 

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

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

908 
by simp 

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

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

911 
finally show ?thesis . 

912 
qed 

913 

914 
lemma setsum_multicount_gen: 

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

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

917 
proof 

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

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

920 
using assms(3) by auto 

921 
finally show ?thesis . 

922 
qed 

923 

924 
lemma setsum_multicount: 

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

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

927 
proof 

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

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

930 
finally show ?thesis by auto 

931 
qed 

932 

28068  933 

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

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

935 

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

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

939 

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

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

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

942 
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

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

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

945 

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

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

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

948 
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

949 

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

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

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

952 
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

953 

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

956 
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

957 

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

960 
apply(cases k)apply simp 

961 
apply(simp add:setsum_head_upt_Suc) 

962 
done 

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

963 

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

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

965 

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

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

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

970 

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

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

972 

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

973 
lemma gauss_sum: 
23277  974 
"((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

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

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

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

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

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

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

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

983 

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

984 
theorem arith_series_general: 
23277  985 
"((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

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

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

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

989 
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

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

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

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

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

994 
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

995 
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

996 
unfolding One_nat_def 
28068  997 
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

998 
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

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

1000 
also from ngt1 have "{1..<n} = {1..n  1}" 
28068  1001 
by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost) 
1002 
also from ngt1 

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

1003 
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

1004 
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

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

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

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

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

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

1012 

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

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

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

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

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

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

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

1019 
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

1020 
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

1021 
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

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

1023 

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

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

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

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

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

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

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

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

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

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

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

1034 

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

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

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

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

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

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

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

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

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

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

1044 

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

1045 
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

1046 
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

1047 

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

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

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

1050 
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

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

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

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

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

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

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

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

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

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

1060 

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

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

1062 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1087 

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

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

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

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

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

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

1093 

8924  1094 
end 