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