author  haftmann 
Mon, 08 Mar 2010 09:38:58 +0100  
changeset 35644  d20cf282342e 
parent 35580  0f74806cab22 
child 35828  46cfc4b8112e 
permissions  rwrr 
8924  1 
(* Title: HOL/SetInterval.thy 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

2 
Author: Tobias Nipkow 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

3 
Author: Clemens Ballarin 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

4 
Author: Jeremy Avigad 
8924  5 

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

14577  9 
header {* Set intervals *} 
10 

15131  11 
theory SetInterval 
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

12 
imports Int Nat_Transfer 
15131  13 
begin 
8924  14 

24691  15 
context ord 
16 
begin 

17 
definition 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

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

21 
definition 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

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

25 
definition 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

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

29 
definition 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

30 
atLeast :: "'a => 'a set" ("(1{_..})") where 
25062  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 
35115  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) 
35115  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) 
35115  69 
"_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ \<le> _)/ _)" 10) 
70 
"_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ < _)/ _)" 10) 

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

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

14418  73 

74 
translations 

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

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

80 

14485  81 
subsection {* Various equivalences *} 
13735  82 

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

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

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

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

13735  93 

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

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

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

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

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

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

103 
apply (rule double_complement) 
13735  104 
done 
105 

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

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

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

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

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

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

13850  118 

119 

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

122 
lemma atLeast_subset_iff [iff]: 

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

123 
"(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

124 
by (blast intro: order_trans) 
13850  125 

126 
lemma atLeast_eq_iff [iff]: 

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

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

130 
lemma greaterThan_subset_iff [iff]: 

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

131 
"(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

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

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

136 
lemma greaterThan_eq_iff [iff]: 

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

137 
"(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

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

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

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

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

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

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

149 
lemma lessThan_subset_iff [iff]: 

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

150 
"(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

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

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

155 
lemma lessThan_eq_iff [iff]: 

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

156 
"(lessThan x = lessThan y) = (x = (y::'a::linorder))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

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

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

162 

13850  163 
subsection {*Twosided intervals*} 
13735  164 

24691  165 
context ord 
166 
begin 

167 

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

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

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

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

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

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

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

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

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

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

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

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

187 

24691  188 
end 
13735  189 

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

24691  192 
context order 
193 
begin 

15554  194 

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

197 
by(auto simp: atLeastAtMost_def atLeast_def atMost_def) 

198 

199 
lemma atLeastatMost_empty_iff[simp]: 

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

201 
by auto (blast intro: order_trans) 

202 

203 
lemma atLeastatMost_empty_iff2[simp]: 

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

205 
by auto (blast intro: order_trans) 

206 

207 
lemma atLeastLessThan_empty[simp]: 

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

209 
by(auto simp: atLeastLessThan_def) 

24691  210 

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

213 
by auto (blast intro: le_less_trans) 

214 

215 
lemma atLeastLessThan_empty_iff2[simp]: 

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

217 
by auto (blast intro: le_less_trans) 

15554  218 

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

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

224 

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

226 
by auto (blast intro: less_le_trans) 

227 

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

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

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

236 
unfolding atLeastAtMost_def atLeast_def atMost_def 

237 
by (blast intro: order_trans) 

238 

239 
lemma atLeastatMost_psubset_iff: 

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

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

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

243 

24691  244 
end 
14485  245 

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

248 
apply (auto simp:subset_eq Ball_def) 

249 
apply(frule_tac x=a in spec) 

250 
apply(erule_tac x=d in allE) 

251 
apply (simp add: less_imp_le) 

252 
done 

253 

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

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

255 

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

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

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

258 

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

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

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

261 

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

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

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

264 

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

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

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

267 

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

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

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

270 

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

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

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

273 

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

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

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

276 

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

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

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

279 

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

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

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

282 

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

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

284 

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

285 

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

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

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

292 

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

294 
by (simp add: lessThan_def less_Suc_eq, blast) 

295 

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

297 
by (simp add: lessThan_def atMost_def less_Suc_eq_le) 

298 

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

300 
by blast 

301 

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

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

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

307 
done 

308 

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

310 
apply (simp add: greaterThan_def) 

311 
apply (auto elim: linorder_neqE) 

312 
done 

313 

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

315 
by blast 

316 

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

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

321 

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

323 
apply (simp add: atLeast_def) 

324 
apply (simp add: Suc_le_eq) 

325 
apply (simp add: order_le_less, blast) 

326 
done 

327 

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

329 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

330 

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

332 
by blast 

333 

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

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

338 

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

340 
apply (simp add: atMost_def) 

341 
apply (simp add: less_Suc_eq order_le_less, blast) 

342 
done 

343 

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

345 
by blast 

346 

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

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

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

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

354 
specific concept to a more general one. *} 

28068  355 

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

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

361 

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

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

363 
atLeast0AtMost[symmetric, code_unfold] 
24449  364 

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

15047  366 
by (simp add: atLeastLessThan_def) 
24449  367 

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

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

371 
lemma atLeastLessThanSuc: 

372 
"{m..<Suc n} = (if m \<le> n then insert n {m..<n} else {})" 

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

373 
by (auto simp add: atLeastLessThan_def) 
15047  374 

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

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

380 

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

382 
by (auto simp add: atLeastLessThan_def) 

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

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

387 
lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

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

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

391 
lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

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

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

397 

33044  398 
lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}" 
399 
apply (induct k) 

400 
apply (simp_all add: atLeastLessThanSuc) 

401 
done 

402 

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

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

404 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

418 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

432 

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

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

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

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

436 

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

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

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

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

440 

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

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

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

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

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

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

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

447 

35580  448 
context ordered_ab_group_add 
449 
begin 

450 

451 
lemma 

452 
fixes x :: 'a 

453 
shows image_uminus_greaterThan[simp]: "uminus ` {x<..} = {..<x}" 

454 
and image_uminus_atLeast[simp]: "uminus ` {x..} = {..x}" 

455 
proof safe 

456 
fix y assume "y < x" 

457 
hence *: "x < y" using neg_less_iff_less[of "y" x] by simp 

458 
have " (y) \<in> uminus ` {x<..}" 

459 
by (rule imageI) (simp add: *) 

460 
thus "y \<in> uminus ` {x<..}" by simp 

461 
next 

462 
fix y assume "y \<le> x" 

463 
have " (y) \<in> uminus ` {x..}" 

464 
by (rule imageI) (insert `y \<le> x`[THEN le_imp_neg_le], simp) 

465 
thus "y \<in> uminus ` {x..}" by simp 

466 
qed simp_all 

467 

468 
lemma 

469 
fixes x :: 'a 

470 
shows image_uminus_lessThan[simp]: "uminus ` {..<x} = {x<..}" 

471 
and image_uminus_atMost[simp]: "uminus ` {..x} = {x..}" 

472 
proof  

473 
have "uminus ` {..<x} = uminus ` uminus ` {x<..}" 

474 
and "uminus ` {..x} = uminus ` uminus ` {x..}" by simp_all 

475 
thus "uminus ` {..<x} = {x<..}" and "uminus ` {..x} = {x..}" 

476 
by (simp_all add: image_image 

477 
del: image_uminus_greaterThan image_uminus_atLeast) 

478 
qed 

479 

480 
lemma 

481 
fixes x :: 'a 

482 
shows image_uminus_atLeastAtMost[simp]: "uminus ` {x..y} = {y..x}" 

483 
and image_uminus_greaterThanAtMost[simp]: "uminus ` {x<..y} = {y..<x}" 

484 
and image_uminus_atLeastLessThan[simp]: "uminus ` {x..<y} = {y<..x}" 

485 
and image_uminus_greaterThanLessThan[simp]: "uminus ` {x<..<y} = {y<..<x}" 

486 
by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def 

487 
greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute) 

488 
end 

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

489 

14485  490 
subsubsection {* Finiteness *} 
491 

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

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

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

497 

498 
lemma finite_greaterThanLessThan [iff]: 

15045  499 
fixes l :: nat shows "finite {l<..<u}" 
14485  500 
by (simp add: greaterThanLessThan_def) 
501 

502 
lemma finite_atLeastLessThan [iff]: 

15045  503 
fixes l :: nat shows "finite {l..<u}" 
14485  504 
by (simp add: atLeastLessThan_def) 
505 

506 
lemma finite_greaterThanAtMost [iff]: 

15045  507 
fixes l :: nat shows "finite {l<..u}" 
14485  508 
by (simp add: greaterThanAtMost_def) 
509 

510 
lemma finite_atLeastAtMost [iff]: 

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

512 
by (simp add: atLeastAtMost_def) 

513 

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

519 
done 

520 

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

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

524 
proof 

525 
assume f:?F show ?B 

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

527 
next 

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

529 
qed 

530 

531 
lemma finite_nat_set_iff_bounded_le: 

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

533 
apply(simp add:finite_nat_set_iff_bounded) 

534 
apply(blast dest:less_imp_le_nat le_imp_less_Suc) 

535 
done 

536 

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

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

14485  540 

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

543 

544 
lemma subset_card_intvl_is_intvl: 

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

546 
proof cases 

547 
assume "finite A" 

548 
thus "PROP ?P" 

32006  549 
proof(induct A rule:finite_linorder_max_induct) 
24853  550 
case empty thus ?case by auto 
551 
next 

33434  552 
case (insert b A) 
24853  553 
moreover hence "b ~: A" by auto 
554 
moreover have "A <= {k..<k+card A}" and "b = k+card A" 

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

556 
ultimately show ?case by auto 

557 
qed 

558 
next 

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

560 
qed 

561 

562 

32596
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

563 
subsubsection {* Proving Inclusions and Equalities between Unions *} 
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

564 

bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

565 
lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)" 
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

566 
by (auto simp add: atLeast0LessThan) 
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

567 

bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

568 
lemma UN_finite_subset: "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C" 
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

569 
by (subst UN_UN_finite_eq [symmetric]) blast 
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

570 

33044  571 
lemma UN_finite2_subset: 
572 
"(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n+k}. B i)) \<Longrightarrow> (\<Union>n. A n) \<subseteq> (\<Union>n. B n)" 

573 
apply (rule UN_finite_subset) 

574 
apply (subst UN_UN_finite_eq [symmetric, of B]) 

575 
apply blast 

576 
done 

32596
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

577 

bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

578 
lemma UN_finite2_eq: 
33044  579 
"(!!n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n+k}. B i)) \<Longrightarrow> (\<Union>n. A n) = (\<Union>n. B n)" 
580 
apply (rule subset_antisym) 

581 
apply (rule UN_finite2_subset, blast) 

582 
apply (rule UN_finite2_subset [where k=k]) 

35216  583 
apply (force simp add: atLeastLessThan_add_Un [of 0]) 
33044  584 
done 
32596
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

585 

bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

586 

14485  587 
subsubsection {* Cardinality *} 
588 

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

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

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

594 

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

14485  597 
apply (erule ssubst, rule card_lessThan) 
15045  598 
apply (subgoal_tac "(%x. x + l) ` {..<ul} = {l..<u}") 
14485  599 
apply (erule subst) 
600 
apply (rule card_image) 

601 
apply (simp add: inj_on_def) 

602 
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) 

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

604 
apply arith 

605 
done 

606 

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

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

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

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

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

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

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

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

618 
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

619 
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

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

621 

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

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

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

624 
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

625 

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

628 
apply(drule ex_bij_betw_finite_nat) 

629 
apply(drule ex_bij_betw_nat_finite) 

630 
apply(auto intro!:bij_betw_trans) 

631 
done 

632 

633 
lemma ex_bij_betw_nat_finite_1: 

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

635 
by (rule finite_same_card_bij) auto 

636 

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

637 

14485  638 
subsection {* Intervals of integers *} 
639 

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

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

643 
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" 
14485  644 
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 
645 

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

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

647 
"{l+1..<u} = {l<..<u::int}" 
14485  648 
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 
649 

650 
subsubsection {* Finiteness *} 

651 

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

652 
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
15045  653 
{(0::int)..<u} = int ` {..<nat u}" 
14485  654 
apply (unfold image_def lessThan_def) 
655 
apply auto 

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

35216  657 
apply (auto simp add: zless_nat_eq_int_zless [THEN sym]) 
14485  658 
done 
659 

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

663 
apply (rule finite_imageI) 

664 
apply auto 

665 
done 

666 

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

14485  669 
apply (erule subst) 
670 
apply (rule finite_imageI) 

671 
apply (rule finite_atLeastZeroLessThan_int) 

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

672 
apply (rule image_add_int_atLeastLessThan) 
14485  673 
done 
674 

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

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

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

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

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

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

24853  684 

14485  685 
subsubsection {* Cardinality *} 
686 

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

690 
apply (subst card_image) 

691 
apply (auto simp add: inj_on_def) 

692 
done 

693 

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

14485  696 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 
15045  697 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 
14485  698 
apply (erule subst) 
699 
apply (rule card_image) 

700 
apply (simp add: inj_on_def) 

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

701 
apply (rule image_add_int_atLeastLessThan) 
14485  702 
done 
703 

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

29667  705 
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 
706 
apply (auto simp add: algebra_simps) 

707 
done 

14485  708 

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

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

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

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

715 
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

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

717 
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

718 
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

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

720 

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

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

722 
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

723 
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

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

725 
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

726 
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

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

728 

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

729 
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

730 
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

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

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

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

734 
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

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

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

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

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

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

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

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

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

743 

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

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

745 
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

746 
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

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

748 
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

749 
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

750 
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

751 
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

752 
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

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

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

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

756 
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

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

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

759 
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

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

761 

14485  762 

13850  763 
subsection {*Lemmas useful with the summation operator setsum*} 
764 

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

765 
text {* For examples, see Algebra/poly/UnivPoly2.thy *} 
13735  766 

14577  767 
subsubsection {* Disjoint Unions *} 
13735  768 

14577  769 
text {* Singletons and open intervals *} 
13735  770 

771 
lemma ivl_disj_un_singleton: 

15045  772 
"{l::'a::linorder} Un {l<..} = {l..}" 
773 
"{..<u} Un {u::'a::linorder} = {..u}" 

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

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

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

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

778 
by auto 
13735  779 

14577  780 
text {* One and twosided intervals *} 
13735  781 

782 
lemma ivl_disj_un_one: 

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

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

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

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

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

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

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

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

791 
by auto 
13735  792 

14577  793 
text {* Two and twosided intervals *} 
13735  794 

795 
lemma ivl_disj_un_two: 

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

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

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

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

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

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

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

804 
by auto 
13735  805 

806 
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two 

807 

14577  808 
subsubsection {* Disjoint Intersections *} 
13735  809 

14577  810 
text {* One and twosided intervals *} 
13735  811 

812 
lemma ivl_disj_int_one: 

15045  813 
"{..l::'a::order} Int {l<..<u} = {}" 
814 
"{..<l} Int {l..<u} = {}" 

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

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

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

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

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

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

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

821 
by auto 
13735  822 

14577  823 
text {* Two and twosided intervals *} 
13735  824 

825 
lemma ivl_disj_int_two: 

15045  826 
"{l::'a::order<..<m} Int {m..<u} = {}" 
827 
"{l<..m} Int {m<..<u} = {}" 

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

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

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

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

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

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

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

834 
by auto 
13735  835 

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

836 
lemmas ivl_disj_int = ivl_disj_int_one ivl_disj_int_two 
13735  837 

15542  838 
subsubsection {* Some Differences *} 
839 

840 
lemma ivl_diff[simp]: 

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

842 
by(auto) 

843 

844 

845 
subsubsection {* Some Subset Conditions *} 

846 

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

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

850 
apply(rule ccontr) 

851 
apply(insert linorder_le_less_linear[of i n]) 

852 
apply(clarsimp simp:linorder_not_le) 

853 
apply(fastsimp) 

854 
done 

855 

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

856 

15042  857 
subsection {* Summation indexed over intervals *} 
858 

859 
syntax 

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

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

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

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

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

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

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

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

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

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

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

883 

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

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

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

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

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

889 

15052  890 
text{* The above introduces some pretty alternative syntaxes for 
15056  891 
summation over intervals: 
15052  892 
\begin{center} 
893 
\begin{tabular}{lll} 

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

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

16052  897 
@{term[source]"\<Sum>x\<in>{..b}. e"} & @{term"\<Sum>x\<le>b. e"} & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\ 
15056  898 
@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"} 
15052  899 
\end{tabular} 
900 
\end{center} 

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

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

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

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

15052  908 

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

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

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

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

913 

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

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

917 
the context. *} 

918 

919 
lemma setsum_ivl_cong: 

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

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

922 
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

923 

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

926 

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

929 

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

932 

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

936 

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

16041  940 
(* 
15561  941 
lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==> 
942 
(\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)" 

943 
by (auto simp:add_ac atLeastAtMostSuc_conv) 

16041  944 
*) 
28068  945 

946 
lemma setsum_head: 

947 
fixes n :: nat 

948 
assumes mn: "m <= n" 

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

950 
proof  

951 
from mn 

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

953 
by (auto intro: ivl_disj_un_singleton) 

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

955 
by (simp add: atLeast0LessThan) 

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

957 
finally show ?thesis . 

958 
qed 

959 

960 
lemma setsum_head_Suc: 

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

962 
by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost) 

963 

964 
lemma setsum_head_upt_Suc: 

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

966 
apply(insert setsum_head_Suc[of m "n  Suc 0" f]) 
29667  967 
apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps) 
28068  968 
done 
969 

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

972 
proof 

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

974 
thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint 

975 
atLeastSucAtMost_greaterThanAtMost) 

976 
qed 

28068  977 

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

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

981 

982 
lemma setsum_diff_nat_ivl: 

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

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

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

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

987 
apply (simp add: add_ac) 

988 
done 

989 

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

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

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

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

995 

31509  996 
lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def] 
997 

998 
lemma setsum_setsum_restrict: 

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

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

1001 
(rule setsum_commute) 

1002 

1003 
lemma setsum_image_gen: assumes fS: "finite S" 

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

1005 
proof 

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

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

1008 
by simp 

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

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

1011 
finally show ?thesis . 

1012 
qed 

1013 

35171
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1014 
lemma setsum_le_included: 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1015 
fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add,ordered_ab_semigroup_add_imp_le}" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1016 
assumes "finite s" "finite t" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1017 
and "\<forall>y\<in>t. 0 \<le> g y" "(\<forall>x\<in>s. \<exists>y\<in>t. i y = x \<and> f x \<le> g y)" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1018 
shows "setsum f s \<le> setsum g t" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1019 
proof  
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1020 
have "setsum f s \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) s" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1021 
proof (rule setsum_mono) 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1022 
fix y assume "y \<in> s" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1023 
with assms obtain z where z: "z \<in> t" "y = i z" "f y \<le> g z" by auto 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1024 
with assms show "f y \<le> setsum g {x \<in> t. i x = y}" (is "?A y \<le> ?B y") 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1025 
using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro] 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1026 
by (auto intro!: setsum_mono2) 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1027 
qed 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1028 
also have "... \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) (i ` t)" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1029 
using assms(24) by (auto intro!: setsum_mono2 setsum_nonneg) 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1030 
also have "... \<le> setsum g t" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1031 
using assms by (auto simp: setsum_image_gen[symmetric]) 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1032 
finally show ?thesis . 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1033 
qed 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1034 

31509  1035 
lemma setsum_multicount_gen: 
1036 
assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)" 

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

1038 
proof 

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

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

1041 
using assms(3) by auto 

1042 
finally show ?thesis . 

1043 
qed 

1044 

1045 
lemma setsum_multicount: 

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

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

1048 
proof 

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

35216  1050 
also have "\<dots> = ?r" by(simp add: mult_commute) 
31509  1051 
finally show ?thesis by auto 
1052 
qed 

1053 

28068  1054 

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

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

1056 

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

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

1060 

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

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

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

1063 
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

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

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

1066 

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

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

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

1069 
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

1070 

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

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

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

1073 
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

1074 

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

1077 
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

1078 

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

1081 
apply(cases k)apply simp 

1082 
apply(simp add:setsum_head_upt_Suc) 

1083 
done 

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

1084 

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

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

1086 

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

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

1088 
"x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = 
31017  1089 
(x ^ n  1) / (x  1::'a::{field})" 
35216  1090 
by (induct "n") (simp_all add: field_simps) 
17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

1091 

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

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

1093 

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

1094 
lemma gauss_sum: 
23277  1095 
"((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

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

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

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

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

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

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

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

1104 

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

1105 
theorem arith_series_general: 
23277  1106 
"((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

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

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

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

1110 
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

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

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

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

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

1115 
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

1116 
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

1117 
unfolding One_nat_def 
28068  1118 
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

1119 
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

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

1121 
also from ngt1 have "{1..<n} = {1..n  1}" 
28068  1122 
by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost) 
1123 
also from ngt1 

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

1124 
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

1125 
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

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

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

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

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

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

1133 

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

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

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

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

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

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

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

1140 
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

1141 
thus ?thesis 
35216  1142 
unfolding One_nat_def by auto 
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

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

1144 

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

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

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

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

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

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

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

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

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

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

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

1155 

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

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

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

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

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

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

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

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

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

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

1165 

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

1166 
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

1167 
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

1168 

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

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

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

1171 
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

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

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

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

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

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

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

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

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

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

1181 

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

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

1183 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1208 

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

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

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

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

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

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

1214 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1215 
subsection {* Transfer setup *} 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1216 

ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1217 
lemma transfer_nat_int_set_functions: 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1218 
"{..n} = nat ` {0..int n}" 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1219 
"{m..n} = nat ` {int m..int n}" (* need all variants of these! *) 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1220 
apply (auto simp add: image_def) 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1221 
apply (rule_tac x = "int x" in bexI) 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1222 
apply auto 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1223 
apply (rule_tac x = "int x" in bexI) 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1224 
apply auto 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1225 
done 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1226 

ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1227 
lemma transfer_nat_int_set_function_closures: 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1228 
"x >= 0 \<Longrightarrow> nat_set {x..y}" 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1229 
by (simp add: nat_set_def) 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1230 

35644  1231 
declare transfer_morphism_nat_int[transfer add 
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1232 
return: transfer_nat_int_set_functions 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1233 
transfer_nat_int_set_function_closures 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1234 
] 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1235 

ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1236 
lemma transfer_int_nat_set_functions: 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1237 
"is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}" 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1238 
by (simp only: is_nat_def transfer_nat_int_set_functions 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1239 
transfer_nat_int_set_function_closures 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1240 
transfer_nat_int_set_return_embed nat_0_le 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1241 
cong: transfer_nat_int_set_cong) 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1242 

ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1243 
lemma transfer_int_nat_set_function_closures: 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1244 
"is_nat x \<Longrightarrow> nat_set {x..y}" 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1245 
by (simp only: transfer_nat_int_set_function_closures is_nat_def) 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1246 

35644  1247 
declare transfer_morphism_int_nat[transfer add 
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1248 
return: transfer_int_nat_set_functions 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1249 
transfer_int_nat_set_function_closures 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1250 
] 
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

1251 

8924  1252 
end 