author | wenzelm |
Wed, 29 Aug 2007 11:10:28 +0200 | |
changeset 24470 | 41c81e23c08d |
parent 24449 | 2f05cb7fed85 |
child 24691 | e7f46ee04809 |
permissions | -rw-r--r-- |
8924 | 1 |
(* Title: HOL/SetInterval.thy |
2 |
ID: $Id$ |
|
13735 | 3 |
Author: Tobias Nipkow and Clemens Ballarin |
14485 | 4 |
Additions by Jeremy Avigad in March 2004 |
8957 | 5 |
Copyright 2000 TU Muenchen |
8924 | 6 |
|
13735 | 7 |
lessThan, greaterThan, atLeast, atMost and two-sided intervals |
8924 | 8 |
*) |
9 |
||
14577 | 10 |
header {* Set intervals *} |
11 |
||
15131 | 12 |
theory SetInterval |
15140 | 13 |
imports IntArith |
15131 | 14 |
begin |
8924 | 15 |
|
16 |
constdefs |
|
15045 | 17 |
lessThan :: "('a::ord) => 'a set" ("(1{..<_})") |
18 |
"{..<u} == {x. x<u}" |
|
8924 | 19 |
|
11609
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset
|
20 |
atMost :: "('a::ord) => 'a set" ("(1{.._})") |
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset
|
21 |
"{..u} == {x. x<=u}" |
8924 | 22 |
|
15045 | 23 |
greaterThan :: "('a::ord) => 'a set" ("(1{_<..})") |
24 |
"{l<..} == {x. l<x}" |
|
8924 | 25 |
|
11609
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset
|
26 |
atLeast :: "('a::ord) => 'a set" ("(1{_..})") |
3f3d1add4d94
eliminated theories "equalities" and "mono" (made part of "Typedef",
wenzelm
parents:
10214
diff
changeset
|
27 |
"{l..} == {x. l<=x}" |
8924 | 28 |
|
15045 | 29 |
greaterThanLessThan :: "['a::ord, 'a] => 'a set" ("(1{_<..<_})") |
30 |
"{l<..<u} == {l<..} Int {..<u}" |
|
13735 | 31 |
|
15045 | 32 |
atLeastLessThan :: "['a::ord, 'a] => 'a set" ("(1{_..<_})") |
33 |
"{l..<u} == {l..} Int {..<u}" |
|
13735 | 34 |
|
15045 | 35 |
greaterThanAtMost :: "['a::ord, 'a] => 'a set" ("(1{_<.._})") |
36 |
"{l<..u} == {l<..} Int {..u}" |
|
13735 | 37 |
|
38 |
atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})") |
|
39 |
"{l..u} == {l..} Int {..u}" |
|
40 |
||
15048 | 41 |
text{* A note of warning when using @{term"{..<n}"} on type @{typ |
42 |
nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving |
|
15052 | 43 |
@{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *} |
15048 | 44 |
|
14418 | 45 |
syntax |
46 |
"@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3UN _<=_./ _)" 10) |
|
47 |
"@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3UN _<_./ _)" 10) |
|
48 |
"@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3INT _<=_./ _)" 10) |
|
49 |
"@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3INT _<_./ _)" 10) |
|
50 |
||
51 |
syntax (input) |
|
52 |
"@UNION_le" :: "nat => nat => 'b set => 'b set" ("(3\<Union> _\<le>_./ _)" 10) |
|
53 |
"@UNION_less" :: "nat => nat => 'b set => 'b set" ("(3\<Union> _<_./ _)" 10) |
|
54 |
"@INTER_le" :: "nat => nat => 'b set => 'b set" ("(3\<Inter> _\<le>_./ _)" 10) |
|
55 |
"@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\<Inter> _<_./ _)" 10) |
|
56 |
||
57 |
syntax (xsymbols) |
|
14846 | 58 |
"@UNION_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10) |
59 |
"@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_ < _\<^esub>)/ _)" 10) |
|
60 |
"@INTER_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10) |
|
61 |
"@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_ < _\<^esub>)/ _)" 10) |
|
14418 | 62 |
|
63 |
translations |
|
64 |
"UN i<=n. A" == "UN i:{..n}. A" |
|
15045 | 65 |
"UN i<n. A" == "UN i:{..<n}. A" |
14418 | 66 |
"INT i<=n. A" == "INT i:{..n}. A" |
15045 | 67 |
"INT i<n. A" == "INT i:{..<n}. A" |
14418 | 68 |
|
69 |
||
14485 | 70 |
subsection {* Various equivalences *} |
13735 | 71 |
|
13850 | 72 |
lemma lessThan_iff [iff]: "(i: lessThan k) = (i<k)" |
73 |
by (simp add: lessThan_def) |
|
13735 | 74 |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
75 |
lemma Compl_lessThan [simp]: |
13735 | 76 |
"!!k:: 'a::linorder. -lessThan k = atLeast k" |
13850 | 77 |
apply (auto simp add: lessThan_def atLeast_def) |
13735 | 78 |
done |
79 |
||
13850 | 80 |
lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}" |
81 |
by auto |
|
13735 | 82 |
|
13850 | 83 |
lemma greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)" |
84 |
by (simp add: greaterThan_def) |
|
13735 | 85 |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
86 |
lemma Compl_greaterThan [simp]: |
13735 | 87 |
"!!k:: 'a::linorder. -greaterThan k = atMost k" |
13850 | 88 |
apply (simp add: greaterThan_def atMost_def le_def, auto) |
13735 | 89 |
done |
90 |
||
13850 | 91 |
lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k" |
92 |
apply (subst Compl_greaterThan [symmetric]) |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
93 |
apply (rule double_complement) |
13735 | 94 |
done |
95 |
||
13850 | 96 |
lemma atLeast_iff [iff]: "(i: atLeast k) = (k<=i)" |
97 |
by (simp add: atLeast_def) |
|
13735 | 98 |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
99 |
lemma Compl_atLeast [simp]: |
13735 | 100 |
"!!k:: 'a::linorder. -atLeast k = lessThan k" |
13850 | 101 |
apply (simp add: lessThan_def atLeast_def le_def, auto) |
13735 | 102 |
done |
103 |
||
13850 | 104 |
lemma atMost_iff [iff]: "(i: atMost k) = (i<=k)" |
105 |
by (simp add: atMost_def) |
|
13735 | 106 |
|
14485 | 107 |
lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" |
108 |
by (blast intro: order_antisym) |
|
13850 | 109 |
|
110 |
||
14485 | 111 |
subsection {* Logical Equivalences for Set Inclusion and Equality *} |
13850 | 112 |
|
113 |
lemma atLeast_subset_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
114 |
"(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
|
115 |
by (blast intro: order_trans) |
13850 | 116 |
|
117 |
lemma atLeast_eq_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
118 |
"(atLeast x = atLeast y) = (x = (y::'a::linorder))" |
13850 | 119 |
by (blast intro: order_antisym order_trans) |
120 |
||
121 |
lemma greaterThan_subset_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
122 |
"(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
|
123 |
apply (auto simp add: greaterThan_def) |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
124 |
apply (subst linorder_not_less [symmetric], blast) |
13850 | 125 |
done |
126 |
||
127 |
lemma greaterThan_eq_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
128 |
"(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
|
129 |
apply (rule iffI) |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
130 |
apply (erule equalityE) |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
131 |
apply (simp_all add: greaterThan_subset_iff) |
13850 | 132 |
done |
133 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
134 |
lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))" |
13850 | 135 |
by (blast intro: order_trans) |
136 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
137 |
lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" |
13850 | 138 |
by (blast intro: order_antisym order_trans) |
139 |
||
140 |
lemma lessThan_subset_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
141 |
"(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
|
142 |
apply (auto simp add: lessThan_def) |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
143 |
apply (subst linorder_not_less [symmetric], blast) |
13850 | 144 |
done |
145 |
||
146 |
lemma lessThan_eq_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
147 |
"(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
|
148 |
apply (rule iffI) |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
149 |
apply (erule equalityE) |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
150 |
apply (simp_all add: lessThan_subset_iff) |
13735 | 151 |
done |
152 |
||
153 |
||
13850 | 154 |
subsection {*Two-sided intervals*} |
13735 | 155 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23496
diff
changeset
|
156 |
lemma greaterThanLessThan_iff [simp,noatp]: |
15045 | 157 |
"(i : {l<..<u}) = (l < i & i < u)" |
13735 | 158 |
by (simp add: greaterThanLessThan_def) |
159 |
||
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23496
diff
changeset
|
160 |
lemma atLeastLessThan_iff [simp,noatp]: |
15045 | 161 |
"(i : {l..<u}) = (l <= i & i < u)" |
13735 | 162 |
by (simp add: atLeastLessThan_def) |
163 |
||
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23496
diff
changeset
|
164 |
lemma greaterThanAtMost_iff [simp,noatp]: |
15045 | 165 |
"(i : {l<..u}) = (l < i & i <= u)" |
13735 | 166 |
by (simp add: greaterThanAtMost_def) |
167 |
||
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23496
diff
changeset
|
168 |
lemma atLeastAtMost_iff [simp,noatp]: |
13735 | 169 |
"(i : {l..u}) = (l <= i & i <= u)" |
170 |
by (simp add: atLeastAtMost_def) |
|
171 |
||
14577 | 172 |
text {* The above four lemmas could be declared as iffs. |
173 |
If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int} |
|
174 |
seems to take forever (more than one hour). *} |
|
13735 | 175 |
|
15554 | 176 |
subsubsection{* Emptyness and singletons *} |
177 |
||
178 |
lemma atLeastAtMost_empty [simp]: "n < m ==> {m::'a::order..n} = {}"; |
|
179 |
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def); |
|
180 |
||
181 |
lemma atLeastLessThan_empty[simp]: "n \<le> m ==> {m..<n::'a::order} = {}" |
|
182 |
by (auto simp add: atLeastLessThan_def) |
|
183 |
||
17719 | 184 |
lemma greaterThanAtMost_empty[simp]:"l \<le> k ==> {k<..(l::'a::order)} = {}" |
185 |
by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) |
|
186 |
||
187 |
lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..(l::'a::order)} = {}" |
|
188 |
by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def) |
|
189 |
||
15554 | 190 |
lemma atLeastAtMost_singleton [simp]: "{a::'a::order..a} = {a}"; |
17719 | 191 |
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def); |
14485 | 192 |
|
193 |
subsection {* Intervals of natural numbers *} |
|
194 |
||
15047 | 195 |
subsubsection {* The Constant @{term lessThan} *} |
196 |
||
14485 | 197 |
lemma lessThan_0 [simp]: "lessThan (0::nat) = {}" |
198 |
by (simp add: lessThan_def) |
|
199 |
||
200 |
lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)" |
|
201 |
by (simp add: lessThan_def less_Suc_eq, blast) |
|
202 |
||
203 |
lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k" |
|
204 |
by (simp add: lessThan_def atMost_def less_Suc_eq_le) |
|
205 |
||
206 |
lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV" |
|
207 |
by blast |
|
208 |
||
15047 | 209 |
subsubsection {* The Constant @{term greaterThan} *} |
210 |
||
14485 | 211 |
lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc" |
212 |
apply (simp add: greaterThan_def) |
|
213 |
apply (blast dest: gr0_conv_Suc [THEN iffD1]) |
|
214 |
done |
|
215 |
||
216 |
lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}" |
|
217 |
apply (simp add: greaterThan_def) |
|
218 |
apply (auto elim: linorder_neqE) |
|
219 |
done |
|
220 |
||
221 |
lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}" |
|
222 |
by blast |
|
223 |
||
15047 | 224 |
subsubsection {* The Constant @{term atLeast} *} |
225 |
||
14485 | 226 |
lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV" |
227 |
by (unfold atLeast_def UNIV_def, simp) |
|
228 |
||
229 |
lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}" |
|
230 |
apply (simp add: atLeast_def) |
|
231 |
apply (simp add: Suc_le_eq) |
|
232 |
apply (simp add: order_le_less, blast) |
|
233 |
done |
|
234 |
||
235 |
lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k" |
|
236 |
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) |
|
237 |
||
238 |
lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV" |
|
239 |
by blast |
|
240 |
||
15047 | 241 |
subsubsection {* The Constant @{term atMost} *} |
242 |
||
14485 | 243 |
lemma atMost_0 [simp]: "atMost (0::nat) = {0}" |
244 |
by (simp add: atMost_def) |
|
245 |
||
246 |
lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)" |
|
247 |
apply (simp add: atMost_def) |
|
248 |
apply (simp add: less_Suc_eq order_le_less, blast) |
|
249 |
done |
|
250 |
||
251 |
lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV" |
|
252 |
by blast |
|
253 |
||
15047 | 254 |
subsubsection {* The Constant @{term atLeastLessThan} *} |
255 |
||
24449 | 256 |
text{*The orientation of the following rule is tricky. The lhs is |
257 |
defined in terms of the rhs. Hence the chosen orientation makes sense |
|
258 |
in this theory --- the reverse orientation complicates proofs (eg |
|
259 |
nontermination). But outside, when the definition of the lhs is rarely |
|
260 |
used, the opposite orientation seems preferable because it reduces a |
|
261 |
specific concept to a more general one. *} |
|
15047 | 262 |
lemma atLeast0LessThan: "{0::nat..<n} = {..<n}" |
15042 | 263 |
by(simp add:lessThan_def atLeastLessThan_def) |
24449 | 264 |
|
265 |
declare atLeast0LessThan[symmetric, code unfold] |
|
266 |
||
267 |
lemma atLeastLessThan0: "{m..<0::nat} = {}" |
|
15047 | 268 |
by (simp add: atLeastLessThan_def) |
24449 | 269 |
|
15047 | 270 |
subsubsection {* Intervals of nats with @{term Suc} *} |
271 |
||
272 |
text{*Not a simprule because the RHS is too messy.*} |
|
273 |
lemma atLeastLessThanSuc: |
|
274 |
"{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
|
275 |
by (auto simp add: atLeastLessThan_def) |
15047 | 276 |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
277 |
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" |
15047 | 278 |
by (auto simp add: atLeastLessThan_def) |
16041 | 279 |
(* |
15047 | 280 |
lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}" |
281 |
by (induct k, simp_all add: atLeastLessThanSuc) |
|
282 |
||
283 |
lemma atLeastSucLessThan [simp]: "{Suc n..<n} = {}" |
|
284 |
by (auto simp add: atLeastLessThan_def) |
|
16041 | 285 |
*) |
15045 | 286 |
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" |
14485 | 287 |
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) |
288 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
289 |
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
|
290 |
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def |
14485 | 291 |
greaterThanAtMost_def) |
292 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
293 |
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
|
294 |
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def |
14485 | 295 |
greaterThanLessThan_def) |
296 |
||
15554 | 297 |
lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}" |
298 |
by (auto simp add: atLeastAtMost_def) |
|
299 |
||
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
300 |
subsubsection {* Image *} |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
301 |
|
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
302 |
lemma image_add_atLeastAtMost: |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
303 |
"(%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
|
304 |
proof |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
305 |
show "?A \<subseteq> ?B" by auto |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
306 |
next |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
307 |
show "?B \<subseteq> ?A" |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
308 |
proof |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
309 |
fix n assume a: "n : ?B" |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19538
diff
changeset
|
310 |
hence "n - k : {i..j}" by auto |
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
311 |
moreover have "n = (n - k) + k" using a by auto |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
312 |
ultimately show "n : ?A" by blast |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
313 |
qed |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
314 |
qed |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
315 |
|
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
316 |
lemma image_add_atLeastLessThan: |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
317 |
"(%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
|
318 |
proof |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
319 |
show "?A \<subseteq> ?B" by auto |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
320 |
next |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
321 |
show "?B \<subseteq> ?A" |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
322 |
proof |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
323 |
fix n assume a: "n : ?B" |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19538
diff
changeset
|
324 |
hence "n - k : {i..<j}" by auto |
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
325 |
moreover have "n = (n - k) + k" using a by auto |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
326 |
ultimately show "n : ?A" by blast |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
327 |
qed |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
328 |
qed |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
329 |
|
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
330 |
corollary image_Suc_atLeastAtMost[simp]: |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
331 |
"Suc ` {i..j} = {Suc i..Suc j}" |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
332 |
using image_add_atLeastAtMost[where k=1] by simp |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
333 |
|
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
334 |
corollary image_Suc_atLeastLessThan[simp]: |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
335 |
"Suc ` {i..<j} = {Suc i..<Suc j}" |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
336 |
using image_add_atLeastLessThan[where k=1] by simp |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
337 |
|
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
338 |
lemma image_add_int_atLeastLessThan: |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
339 |
"(%x. x + (l::int)) ` {0..<u-l} = {l..<u}" |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
340 |
apply (auto simp add: image_def) |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
341 |
apply (rule_tac x = "x - l" in bexI) |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
342 |
apply auto |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
343 |
done |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
344 |
|
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
345 |
|
14485 | 346 |
subsubsection {* Finiteness *} |
347 |
||
15045 | 348 |
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}" |
14485 | 349 |
by (induct k) (simp_all add: lessThan_Suc) |
350 |
||
351 |
lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}" |
|
352 |
by (induct k) (simp_all add: atMost_Suc) |
|
353 |
||
354 |
lemma finite_greaterThanLessThan [iff]: |
|
15045 | 355 |
fixes l :: nat shows "finite {l<..<u}" |
14485 | 356 |
by (simp add: greaterThanLessThan_def) |
357 |
||
358 |
lemma finite_atLeastLessThan [iff]: |
|
15045 | 359 |
fixes l :: nat shows "finite {l..<u}" |
14485 | 360 |
by (simp add: atLeastLessThan_def) |
361 |
||
362 |
lemma finite_greaterThanAtMost [iff]: |
|
15045 | 363 |
fixes l :: nat shows "finite {l<..u}" |
14485 | 364 |
by (simp add: greaterThanAtMost_def) |
365 |
||
366 |
lemma finite_atLeastAtMost [iff]: |
|
367 |
fixes l :: nat shows "finite {l..u}" |
|
368 |
by (simp add: atLeastAtMost_def) |
|
369 |
||
370 |
lemma bounded_nat_set_is_finite: |
|
371 |
"(ALL i:N. i < (n::nat)) ==> finite N" |
|
372 |
-- {* A bounded set of natural numbers is finite. *} |
|
373 |
apply (rule finite_subset) |
|
374 |
apply (rule_tac [2] finite_lessThan, auto) |
|
375 |
done |
|
376 |
||
377 |
subsubsection {* Cardinality *} |
|
378 |
||
15045 | 379 |
lemma card_lessThan [simp]: "card {..<u} = u" |
15251 | 380 |
by (induct u, simp_all add: lessThan_Suc) |
14485 | 381 |
|
382 |
lemma card_atMost [simp]: "card {..u} = Suc u" |
|
383 |
by (simp add: lessThan_Suc_atMost [THEN sym]) |
|
384 |
||
15045 | 385 |
lemma card_atLeastLessThan [simp]: "card {l..<u} = u - l" |
386 |
apply (subgoal_tac "card {l..<u} = card {..<u-l}") |
|
14485 | 387 |
apply (erule ssubst, rule card_lessThan) |
15045 | 388 |
apply (subgoal_tac "(%x. x + l) ` {..<u-l} = {l..<u}") |
14485 | 389 |
apply (erule subst) |
390 |
apply (rule card_image) |
|
391 |
apply (simp add: inj_on_def) |
|
392 |
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) |
|
393 |
apply (rule_tac x = "x - l" in exI) |
|
394 |
apply arith |
|
395 |
done |
|
396 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
397 |
lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l" |
14485 | 398 |
by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp) |
399 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
400 |
lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l" |
14485 | 401 |
by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp) |
402 |
||
15045 | 403 |
lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l" |
14485 | 404 |
by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp) |
405 |
||
406 |
subsection {* Intervals of integers *} |
|
407 |
||
15045 | 408 |
lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}" |
14485 | 409 |
by (auto simp add: atLeastAtMost_def atLeastLessThan_def) |
410 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
411 |
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" |
14485 | 412 |
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) |
413 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
414 |
lemma atLeastPlusOneLessThan_greaterThanLessThan_int: |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
415 |
"{l+1..<u} = {l<..<u::int}" |
14485 | 416 |
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) |
417 |
||
418 |
subsubsection {* Finiteness *} |
|
419 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
420 |
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> |
15045 | 421 |
{(0::int)..<u} = int ` {..<nat u}" |
14485 | 422 |
apply (unfold image_def lessThan_def) |
423 |
apply auto |
|
424 |
apply (rule_tac x = "nat x" in exI) |
|
425 |
apply (auto simp add: zless_nat_conj zless_nat_eq_int_zless [THEN sym]) |
|
426 |
done |
|
427 |
||
15045 | 428 |
lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}" |
14485 | 429 |
apply (case_tac "0 \<le> u") |
430 |
apply (subst image_atLeastZeroLessThan_int, assumption) |
|
431 |
apply (rule finite_imageI) |
|
432 |
apply auto |
|
433 |
done |
|
434 |
||
15045 | 435 |
lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}" |
436 |
apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}") |
|
14485 | 437 |
apply (erule subst) |
438 |
apply (rule finite_imageI) |
|
439 |
apply (rule finite_atLeastZeroLessThan_int) |
|
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
440 |
apply (rule image_add_int_atLeastLessThan) |
14485 | 441 |
done |
442 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
443 |
lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}" |
14485 | 444 |
by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp) |
445 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
446 |
lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}" |
14485 | 447 |
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) |
448 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
449 |
lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}" |
14485 | 450 |
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) |
451 |
||
452 |
subsubsection {* Cardinality *} |
|
453 |
||
15045 | 454 |
lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u" |
14485 | 455 |
apply (case_tac "0 \<le> u") |
456 |
apply (subst image_atLeastZeroLessThan_int, assumption) |
|
457 |
apply (subst card_image) |
|
458 |
apply (auto simp add: inj_on_def) |
|
459 |
done |
|
460 |
||
15045 | 461 |
lemma card_atLeastLessThan_int [simp]: "card {l..<u} = nat (u - l)" |
462 |
apply (subgoal_tac "card {l..<u} = card {0..<u-l}") |
|
14485 | 463 |
apply (erule ssubst, rule card_atLeastZeroLessThan_int) |
15045 | 464 |
apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}") |
14485 | 465 |
apply (erule subst) |
466 |
apply (rule card_image) |
|
467 |
apply (simp add: inj_on_def) |
|
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
468 |
apply (rule image_add_int_atLeastLessThan) |
14485 | 469 |
done |
470 |
||
471 |
lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)" |
|
472 |
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) |
|
473 |
apply (auto simp add: compare_rls) |
|
474 |
done |
|
475 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
476 |
lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)" |
14485 | 477 |
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) |
478 |
||
15045 | 479 |
lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u - (l + 1))" |
14485 | 480 |
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) |
481 |
||
482 |
||
13850 | 483 |
subsection {*Lemmas useful with the summation operator setsum*} |
484 |
||
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16052
diff
changeset
|
485 |
text {* For examples, see Algebra/poly/UnivPoly2.thy *} |
13735 | 486 |
|
14577 | 487 |
subsubsection {* Disjoint Unions *} |
13735 | 488 |
|
14577 | 489 |
text {* Singletons and open intervals *} |
13735 | 490 |
|
491 |
lemma ivl_disj_un_singleton: |
|
15045 | 492 |
"{l::'a::linorder} Un {l<..} = {l..}" |
493 |
"{..<u} Un {u::'a::linorder} = {..u}" |
|
494 |
"(l::'a::linorder) < u ==> {l} Un {l<..<u} = {l..<u}" |
|
495 |
"(l::'a::linorder) < u ==> {l<..<u} Un {u} = {l<..u}" |
|
496 |
"(l::'a::linorder) <= u ==> {l} Un {l<..u} = {l..u}" |
|
497 |
"(l::'a::linorder) <= u ==> {l..<u} Un {u} = {l..u}" |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset
|
498 |
by auto |
13735 | 499 |
|
14577 | 500 |
text {* One- and two-sided intervals *} |
13735 | 501 |
|
502 |
lemma ivl_disj_un_one: |
|
15045 | 503 |
"(l::'a::linorder) < u ==> {..l} Un {l<..<u} = {..<u}" |
504 |
"(l::'a::linorder) <= u ==> {..<l} Un {l..<u} = {..<u}" |
|
505 |
"(l::'a::linorder) <= u ==> {..l} Un {l<..u} = {..u}" |
|
506 |
"(l::'a::linorder) <= u ==> {..<l} Un {l..u} = {..u}" |
|
507 |
"(l::'a::linorder) <= u ==> {l<..u} Un {u<..} = {l<..}" |
|
508 |
"(l::'a::linorder) < u ==> {l<..<u} Un {u..} = {l<..}" |
|
509 |
"(l::'a::linorder) <= u ==> {l..u} Un {u<..} = {l..}" |
|
510 |
"(l::'a::linorder) <= u ==> {l..<u} Un {u..} = {l..}" |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset
|
511 |
by auto |
13735 | 512 |
|
14577 | 513 |
text {* Two- and two-sided intervals *} |
13735 | 514 |
|
515 |
lemma ivl_disj_un_two: |
|
15045 | 516 |
"[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..<u} = {l<..<u}" |
517 |
"[| (l::'a::linorder) <= m; m < u |] ==> {l<..m} Un {m<..<u} = {l<..<u}" |
|
518 |
"[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..<u} = {l..<u}" |
|
519 |
"[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {m<..<u} = {l..<u}" |
|
520 |
"[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..u} = {l<..u}" |
|
521 |
"[| (l::'a::linorder) <= m; m <= u |] ==> {l<..m} Un {m<..u} = {l<..u}" |
|
522 |
"[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..u} = {l..u}" |
|
523 |
"[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m<..u} = {l..u}" |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset
|
524 |
by auto |
13735 | 525 |
|
526 |
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two |
|
527 |
||
14577 | 528 |
subsubsection {* Disjoint Intersections *} |
13735 | 529 |
|
14577 | 530 |
text {* Singletons and open intervals *} |
13735 | 531 |
|
532 |
lemma ivl_disj_int_singleton: |
|
15045 | 533 |
"{l::'a::order} Int {l<..} = {}" |
534 |
"{..<u} Int {u} = {}" |
|
535 |
"{l} Int {l<..<u} = {}" |
|
536 |
"{l<..<u} Int {u} = {}" |
|
537 |
"{l} Int {l<..u} = {}" |
|
538 |
"{l..<u} Int {u} = {}" |
|
13735 | 539 |
by simp+ |
540 |
||
14577 | 541 |
text {* One- and two-sided intervals *} |
13735 | 542 |
|
543 |
lemma ivl_disj_int_one: |
|
15045 | 544 |
"{..l::'a::order} Int {l<..<u} = {}" |
545 |
"{..<l} Int {l..<u} = {}" |
|
546 |
"{..l} Int {l<..u} = {}" |
|
547 |
"{..<l} Int {l..u} = {}" |
|
548 |
"{l<..u} Int {u<..} = {}" |
|
549 |
"{l<..<u} Int {u..} = {}" |
|
550 |
"{l..u} Int {u<..} = {}" |
|
551 |
"{l..<u} Int {u..} = {}" |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset
|
552 |
by auto |
13735 | 553 |
|
14577 | 554 |
text {* Two- and two-sided intervals *} |
13735 | 555 |
|
556 |
lemma ivl_disj_int_two: |
|
15045 | 557 |
"{l::'a::order<..<m} Int {m..<u} = {}" |
558 |
"{l<..m} Int {m<..<u} = {}" |
|
559 |
"{l..<m} Int {m..<u} = {}" |
|
560 |
"{l..m} Int {m<..<u} = {}" |
|
561 |
"{l<..<m} Int {m..u} = {}" |
|
562 |
"{l<..m} Int {m<..u} = {}" |
|
563 |
"{l..<m} Int {m..u} = {}" |
|
564 |
"{l..m} Int {m<..u} = {}" |
|
14398
c5c47703f763
Efficient, graph-based reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset
|
565 |
by auto |
13735 | 566 |
|
567 |
lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two |
|
568 |
||
15542 | 569 |
subsubsection {* Some Differences *} |
570 |
||
571 |
lemma ivl_diff[simp]: |
|
572 |
"i \<le> n \<Longrightarrow> {i..<m} - {i..<n} = {n..<(m::'a::linorder)}" |
|
573 |
by(auto) |
|
574 |
||
575 |
||
576 |
subsubsection {* Some Subset Conditions *} |
|
577 |
||
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23496
diff
changeset
|
578 |
lemma ivl_subset [simp,noatp]: |
15542 | 579 |
"({i..<j} \<subseteq> {m..<n}) = (j \<le> i | m \<le> i & j \<le> (n::'a::linorder))" |
580 |
apply(auto simp:linorder_not_le) |
|
581 |
apply(rule ccontr) |
|
582 |
apply(insert linorder_le_less_linear[of i n]) |
|
583 |
apply(clarsimp simp:linorder_not_le) |
|
584 |
apply(fastsimp) |
|
585 |
done |
|
586 |
||
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset
|
587 |
|
15042 | 588 |
subsection {* Summation indexed over intervals *} |
589 |
||
590 |
syntax |
|
591 |
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) |
|
15048 | 592 |
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) |
16052 | 593 |
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10) |
594 |
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<=_./ _)" [0,0,10] 10) |
|
15042 | 595 |
syntax (xsymbols) |
596 |
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) |
|
15048 | 597 |
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) |
16052 | 598 |
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) |
599 |
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10) |
|
15042 | 600 |
syntax (HTML output) |
601 |
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) |
|
15048 | 602 |
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) |
16052 | 603 |
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) |
604 |
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10) |
|
15056 | 605 |
syntax (latex_sum output) |
15052 | 606 |
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" |
607 |
("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) |
|
608 |
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" |
|
609 |
("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) |
|
16052 | 610 |
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" |
611 |
("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10) |
|
15052 | 612 |
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" |
16052 | 613 |
("(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
|
614 |
|
15048 | 615 |
translations |
616 |
"\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}" |
|
617 |
"\<Sum>x=a..<b. t" == "setsum (%x. t) {a..<b}" |
|
16052 | 618 |
"\<Sum>i\<le>n. t" == "setsum (\<lambda>i. t) {..n}" |
15048 | 619 |
"\<Sum>i<n. t" == "setsum (\<lambda>i. t) {..<n}" |
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset
|
620 |
|
15052 | 621 |
text{* The above introduces some pretty alternative syntaxes for |
15056 | 622 |
summation over intervals: |
15052 | 623 |
\begin{center} |
624 |
\begin{tabular}{lll} |
|
15056 | 625 |
Old & New & \LaTeX\\ |
626 |
@{term[source]"\<Sum>x\<in>{a..b}. e"} & @{term"\<Sum>x=a..b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..b. e"}\\ |
|
627 |
@{term[source]"\<Sum>x\<in>{a..<b}. e"} & @{term"\<Sum>x=a..<b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..<b. e"}\\ |
|
16052 | 628 |
@{term[source]"\<Sum>x\<in>{..b}. e"} & @{term"\<Sum>x\<le>b. e"} & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\ |
15056 | 629 |
@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"} |
15052 | 630 |
\end{tabular} |
631 |
\end{center} |
|
15056 | 632 |
The left column shows the term before introduction of the new syntax, |
633 |
the middle column shows the new (default) syntax, and the right column |
|
634 |
shows a special syntax. The latter is only meaningful for latex output |
|
635 |
and has to be activated explicitly by setting the print mode to |
|
21502 | 636 |
@{text latex_sum} (e.g.\ via @{text "mode = latex_sum"} in |
15056 | 637 |
antiquotations). It is not the default \LaTeX\ output because it only |
638 |
works well with italic-style formulae, not tt-style. |
|
15052 | 639 |
|
640 |
Note that for uniformity on @{typ nat} it is better to use |
|
641 |
@{term"\<Sum>x::nat=0..<n. e"} rather than @{text"\<Sum>x<n. e"}: @{text setsum} may |
|
642 |
not provide all lemmas available for @{term"{m..<n}"} also in the |
|
643 |
special form for @{term"{..<n}"}. *} |
|
644 |
||
15542 | 645 |
text{* This congruence rule should be used for sums over intervals as |
646 |
the standard theorem @{text[source]setsum_cong} does not work well |
|
647 |
with the simplifier who adds the unsimplified premise @{term"x:B"} to |
|
648 |
the context. *} |
|
649 |
||
650 |
lemma setsum_ivl_cong: |
|
651 |
"\<lbrakk>a = c; b = d; !!x. \<lbrakk> c \<le> x; x < d \<rbrakk> \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> |
|
652 |
setsum f {a..<b} = setsum g {c..<d}" |
|
653 |
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
|
654 |
|
16041 | 655 |
(* FIXME why are the following simp rules but the corresponding eqns |
656 |
on intervals are not? *) |
|
657 |
||
16052 | 658 |
lemma setsum_atMost_Suc[simp]: "(\<Sum>i \<le> Suc n. f i) = (\<Sum>i \<le> n. f i) + f(Suc n)" |
659 |
by (simp add:atMost_Suc add_ac) |
|
660 |
||
16041 | 661 |
lemma setsum_lessThan_Suc[simp]: "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n" |
662 |
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
|
663 |
|
15911 | 664 |
lemma setsum_cl_ivl_Suc[simp]: |
15561 | 665 |
"setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))" |
666 |
by (auto simp:add_ac atLeastAtMostSuc_conv) |
|
667 |
||
15911 | 668 |
lemma setsum_op_ivl_Suc[simp]: |
15561 | 669 |
"setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))" |
670 |
by (auto simp:add_ac atLeastLessThanSuc) |
|
16041 | 671 |
(* |
15561 | 672 |
lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==> |
673 |
(\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)" |
|
674 |
by (auto simp:add_ac atLeastAtMostSuc_conv) |
|
16041 | 675 |
*) |
15539 | 676 |
lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> |
677 |
setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}" |
|
678 |
by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un) |
|
679 |
||
680 |
lemma setsum_diff_nat_ivl: |
|
681 |
fixes f :: "nat \<Rightarrow> 'a::ab_group_add" |
|
682 |
shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> |
|
683 |
setsum f {m..<p} - setsum f {m..<n} = setsum f {n..<p}" |
|
684 |
using setsum_add_nat_ivl [of m n p f,symmetric] |
|
685 |
apply (simp add: add_ac) |
|
686 |
done |
|
687 |
||
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
688 |
subsection{* Shifting bounds *} |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
689 |
|
15539 | 690 |
lemma setsum_shift_bounds_nat_ivl: |
691 |
"setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}" |
|
692 |
by (induct "n", auto simp:atLeastLessThanSuc) |
|
693 |
||
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
694 |
lemma setsum_shift_bounds_cl_nat_ivl: |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
695 |
"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
|
696 |
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
|
697 |
apply (simp add:image_add_atLeastAtMost o_def) |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
698 |
done |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
699 |
|
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
700 |
corollary setsum_shift_bounds_cl_Suc_ivl: |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
701 |
"setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}" |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
702 |
by (simp add:setsum_shift_bounds_cl_nat_ivl[where k=1,simplified]) |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
703 |
|
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
704 |
corollary setsum_shift_bounds_Suc_ivl: |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
705 |
"setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}" |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
706 |
by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified]) |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
707 |
|
19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
708 |
lemma setsum_head: |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
709 |
fixes n :: nat |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
710 |
assumes mn: "m <= n" |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
711 |
shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs") |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
712 |
proof - |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
713 |
from mn |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
714 |
have "{m..n} = {m} \<union> {m<..n}" |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
715 |
by (auto intro: ivl_disj_un_singleton) |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
716 |
hence "?lhs = (\<Sum>x\<in>{m} \<union> {m<..n}. P x)" |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
717 |
by (simp add: atLeast0LessThan) |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
718 |
also have "\<dots> = ?rhs" by simp |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
719 |
finally show ?thesis . |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
720 |
qed |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
721 |
|
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
722 |
lemma setsum_head_upt: |
19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
723 |
fixes m::nat |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
724 |
assumes m: "0 < m" |
19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
725 |
shows "(\<Sum>x<m. P x) = P 0 + (\<Sum>x\<in>{1..<m}. P x)" |
19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
726 |
proof - |
19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
727 |
have "(\<Sum>x<m. P x) = (\<Sum>x\<in>{0..<m}. P x)" |
19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
728 |
by (simp add: atLeast0LessThan) |
19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
729 |
also |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
730 |
from m |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
731 |
have "\<dots> = (\<Sum>x\<in>{0..m - 1}. P x)" |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
732 |
by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost) |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
733 |
also |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
734 |
have "\<dots> = P 0 + (\<Sum>x\<in>{0<..m - 1}. P x)" |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
735 |
by (simp add: setsum_head) |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
736 |
also |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
737 |
from m |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
738 |
have "{0<..m - 1} = {1..<m}" |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
739 |
by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost) |
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset
|
740 |
finally show ?thesis . |
19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
741 |
qed |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
742 |
|
17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset
|
743 |
subsection {* The formula for geometric sums *} |
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset
|
744 |
|
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset
|
745 |
lemma geometric_sum: |
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset
|
746 |
"x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = |
22713 | 747 |
(x ^ n - 1) / (x - 1::'a::{field, recpower})" |
23496 | 748 |
by (induct "n") (simp_all add:field_simps power_Suc) |
17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset
|
749 |
|
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
750 |
subsection {* The formula for arithmetic sums *} |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
751 |
|
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
752 |
lemma gauss_sum: |
23277 | 753 |
"((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
|
754 |
of_nat n*((of_nat n)+1)" |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
755 |
proof (induct n) |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
756 |
case 0 |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
757 |
show ?case by simp |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
758 |
next |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
759 |
case (Suc n) |
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23431
diff
changeset
|
760 |
then show ?case by (simp add: ring_simps) |
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
761 |
qed |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
762 |
|
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
763 |
theorem arith_series_general: |
23277 | 764 |
"((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
|
765 |
of_nat n * (a + (a + of_nat(n - 1)*d))" |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
766 |
proof cases |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
767 |
assume ngt1: "n > 1" |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
768 |
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
|
769 |
have |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
770 |
"(\<Sum>i\<in>{..<n}. a+?I i*d) = |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
771 |
((\<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
|
772 |
by (rule setsum_addf) |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
773 |
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
|
774 |
also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))" |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
775 |
by (simp add: setsum_right_distrib setsum_head_upt mult_ac) |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
776 |
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
|
777 |
by (simp add: left_distrib right_distrib) |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
778 |
also from ngt1 have "{1..<n} = {1..n - 1}" |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
779 |
by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost) |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
780 |
also from ngt1 |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
781 |
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)" |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
782 |
by (simp only: mult_ac gauss_sum [of "n - 1"]) |
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
|
783 |
(simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]]) |
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
784 |
finally show ?thesis by (simp add: mult_ac add_ac right_distrib) |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
785 |
next |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
786 |
assume "\<not>(n > 1)" |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
787 |
hence "n = 1 \<or> n = 0" by auto |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
788 |
thus ?thesis by (auto simp: mult_ac right_distrib) |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
789 |
qed |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
790 |
|
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
791 |
lemma arith_series_nat: |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
792 |
"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
|
793 |
proof - |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
794 |
have |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
795 |
"((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
|
796 |
of_nat(n) * (a + (a + of_nat(n - 1)*d))" |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
797 |
by (rule arith_series_general) |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
798 |
thus ?thesis by (auto simp add: of_nat_id) |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
799 |
qed |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
800 |
|
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
801 |
lemma arith_series_int: |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
802 |
"(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
|
803 |
of_nat n * (a + (a + of_nat(n - 1)*d))" |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
804 |
proof - |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
805 |
have |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
806 |
"((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
|
807 |
of_nat(n) * (a + (a + of_nat(n - 1)*d))" |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
808 |
by (rule arith_series_general) |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
809 |
thus ?thesis by simp |
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset
|
810 |
qed |
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
811 |
|
19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
812 |
lemma sum_diff_distrib: |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
813 |
fixes P::"nat\<Rightarrow>nat" |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
814 |
shows |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
815 |
"\<forall>x. Q x \<le> P x \<Longrightarrow> |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
816 |
(\<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
|
817 |
proof (induct n) |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
818 |
case 0 show ?case by simp |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
819 |
next |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
820 |
case (Suc n) |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
821 |
|
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
822 |
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
|
823 |
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
|
824 |
|
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
825 |
from Suc have "?lhs = ?rhs" by simp |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
826 |
moreover |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
827 |
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
|
828 |
moreover |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
829 |
from Suc have |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
830 |
"(\<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
|
831 |
by (subst diff_diff_left[symmetric], |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
832 |
subst diff_add_assoc2) |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
833 |
(auto simp: diff_add_assoc2 intro: setsum_mono) |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
834 |
ultimately |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
835 |
show ?case by simp |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
836 |
qed |
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
837 |
|
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset
|
838 |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
839 |
ML |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
840 |
{* |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
841 |
val Compl_atLeast = thm "Compl_atLeast"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
842 |
val Compl_atMost = thm "Compl_atMost"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
843 |
val Compl_greaterThan = thm "Compl_greaterThan"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
844 |
val Compl_lessThan = thm "Compl_lessThan"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
845 |
val INT_greaterThan_UNIV = thm "INT_greaterThan_UNIV"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
846 |
val UN_atLeast_UNIV = thm "UN_atLeast_UNIV"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
847 |
val UN_atMost_UNIV = thm "UN_atMost_UNIV"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
848 |
val UN_lessThan_UNIV = thm "UN_lessThan_UNIV"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
849 |
val atLeastAtMost_def = thm "atLeastAtMost_def"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
850 |
val atLeastAtMost_iff = thm "atLeastAtMost_iff"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
851 |
val atLeastLessThan_def = thm "atLeastLessThan_def"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
852 |
val atLeastLessThan_iff = thm "atLeastLessThan_iff"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
853 |
val atLeast_0 = thm "atLeast_0"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
854 |
val atLeast_Suc = thm "atLeast_Suc"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
855 |
val atLeast_def = thm "atLeast_def"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
856 |
val atLeast_iff = thm "atLeast_iff"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
857 |
val atMost_0 = thm "atMost_0"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
858 |
val atMost_Int_atLeast = thm "atMost_Int_atLeast"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
859 |
val atMost_Suc = thm "atMost_Suc"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
860 |
val atMost_def = thm "atMost_def"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
861 |
val atMost_iff = thm "atMost_iff"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
862 |
val greaterThanAtMost_def = thm "greaterThanAtMost_def"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
863 |
val greaterThanAtMost_iff = thm "greaterThanAtMost_iff"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
864 |
val greaterThanLessThan_def = thm "greaterThanLessThan_def"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
865 |
val greaterThanLessThan_iff = thm "greaterThanLessThan_iff"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
866 |
val greaterThan_0 = thm "greaterThan_0"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
867 |
val greaterThan_Suc = thm "greaterThan_Suc"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
868 |
val greaterThan_def = thm "greaterThan_def"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
869 |
val greaterThan_iff = thm "greaterThan_iff"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
870 |
val ivl_disj_int = thms "ivl_disj_int"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
871 |
val ivl_disj_int_one = thms "ivl_disj_int_one"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
872 |
val ivl_disj_int_singleton = thms "ivl_disj_int_singleton"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
873 |
val ivl_disj_int_two = thms "ivl_disj_int_two"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
874 |
val ivl_disj_un = thms "ivl_disj_un"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
875 |
val ivl_disj_un_one = thms "ivl_disj_un_one"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
876 |
val ivl_disj_un_singleton = thms "ivl_disj_un_singleton"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
877 |
val ivl_disj_un_two = thms "ivl_disj_un_two"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
878 |
val lessThan_0 = thm "lessThan_0"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
879 |
val lessThan_Suc = thm "lessThan_Suc"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
880 |
val lessThan_Suc_atMost = thm "lessThan_Suc_atMost"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
881 |
val lessThan_def = thm "lessThan_def"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
882 |
val lessThan_iff = thm "lessThan_iff"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
883 |
val single_Diff_lessThan = thm "single_Diff_lessThan"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
884 |
|
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
885 |
val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
886 |
val finite_atMost = thm "finite_atMost"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
887 |
val finite_lessThan = thm "finite_lessThan"; |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
888 |
*} |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
889 |
|
8924 | 890 |
end |