author | paulson |
Fri, 21 Jan 2005 13:52:09 +0100 | |
changeset 15447 | 177ffdbabf80 |
parent 15409 | a063687d24eb |
child 15479 | fbc473ea9d3c |
permissions | -rw-r--r-- |
12396 | 1 |
(* Title: HOL/Finite_Set.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel |
|
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset
|
4 |
Additions by Jeremy Avigad in Feb 2004 |
15376 | 5 |
|
15402 | 6 |
Get rid of a couple of superfluous finiteness assumptions in lemmas |
7 |
about setsum and card - see FIXME. |
|
8 |
NB: the analogous lemmas for setprod should also be simplified! |
|
12396 | 9 |
*) |
10 |
||
11 |
header {* Finite sets *} |
|
12 |
||
15131 | 13 |
theory Finite_Set |
15140 | 14 |
imports Divides Power Inductive |
15131 | 15 |
begin |
12396 | 16 |
|
15392 | 17 |
subsection {* Definition and basic properties *} |
12396 | 18 |
|
19 |
consts Finites :: "'a set set" |
|
13737 | 20 |
syntax |
21 |
finite :: "'a set => bool" |
|
22 |
translations |
|
23 |
"finite A" == "A : Finites" |
|
12396 | 24 |
|
25 |
inductive Finites |
|
26 |
intros |
|
27 |
emptyI [simp, intro!]: "{} : Finites" |
|
28 |
insertI [simp, intro!]: "A : Finites ==> insert a A : Finites" |
|
29 |
||
30 |
axclass finite \<subseteq> type |
|
31 |
finite: "finite UNIV" |
|
32 |
||
13737 | 33 |
lemma ex_new_if_finite: -- "does not depend on def of finite at all" |
14661 | 34 |
assumes "\<not> finite (UNIV :: 'a set)" and "finite A" |
35 |
shows "\<exists>a::'a. a \<notin> A" |
|
36 |
proof - |
|
37 |
from prems have "A \<noteq> UNIV" by blast |
|
38 |
thus ?thesis by blast |
|
39 |
qed |
|
12396 | 40 |
|
41 |
lemma finite_induct [case_names empty insert, induct set: Finites]: |
|
42 |
"finite F ==> |
|
15327
0230a10582d3
changed the order of !!-quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset
|
43 |
P {} ==> (!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F" |
12396 | 44 |
-- {* Discharging @{text "x \<notin> F"} entails extra work. *} |
45 |
proof - |
|
13421 | 46 |
assume "P {}" and |
15327
0230a10582d3
changed the order of !!-quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset
|
47 |
insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)" |
12396 | 48 |
assume "finite F" |
49 |
thus "P F" |
|
50 |
proof induct |
|
51 |
show "P {}" . |
|
15327
0230a10582d3
changed the order of !!-quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset
|
52 |
fix x F assume F: "finite F" and P: "P F" |
12396 | 53 |
show "P (insert x F)" |
54 |
proof cases |
|
55 |
assume "x \<in> F" |
|
56 |
hence "insert x F = F" by (rule insert_absorb) |
|
57 |
with P show ?thesis by (simp only:) |
|
58 |
next |
|
59 |
assume "x \<notin> F" |
|
60 |
from F this P show ?thesis by (rule insert) |
|
61 |
qed |
|
62 |
qed |
|
63 |
qed |
|
64 |
||
65 |
lemma finite_subset_induct [consumes 2, case_names empty insert]: |
|
66 |
"finite F ==> F \<subseteq> A ==> |
|
15327
0230a10582d3
changed the order of !!-quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset
|
67 |
P {} ==> (!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==> |
12396 | 68 |
P F" |
69 |
proof - |
|
13421 | 70 |
assume "P {}" and insert: |
15327
0230a10582d3
changed the order of !!-quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset
|
71 |
"!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)" |
12396 | 72 |
assume "finite F" |
73 |
thus "F \<subseteq> A ==> P F" |
|
74 |
proof induct |
|
75 |
show "P {}" . |
|
15327
0230a10582d3
changed the order of !!-quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset
|
76 |
fix x F assume "finite F" and "x \<notin> F" |
12396 | 77 |
and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A" |
78 |
show "P (insert x F)" |
|
79 |
proof (rule insert) |
|
80 |
from i show "x \<in> A" by blast |
|
81 |
from i have "F \<subseteq> A" by blast |
|
82 |
with P show "P F" . |
|
83 |
qed |
|
84 |
qed |
|
85 |
qed |
|
86 |
||
15392 | 87 |
text{* Finite sets are the images of initial segments of natural numbers: *} |
88 |
||
89 |
lemma finite_imp_nat_seg_image: |
|
90 |
assumes fin: "finite A" shows "\<exists> (n::nat) f. A = f ` {i::nat. i<n}" |
|
91 |
using fin |
|
92 |
proof induct |
|
93 |
case empty |
|
94 |
show ?case |
|
95 |
proof show "\<exists>f. {} = f ` {i::nat. i < 0}" by(simp add:image_def) qed |
|
96 |
next |
|
97 |
case (insert a A) |
|
98 |
from insert.hyps obtain n f where "A = f ` {i::nat. i < n}" by blast |
|
99 |
hence "insert a A = (%i. if i<n then f i else a) ` {i. i < n+1}" |
|
100 |
by (auto simp add:image_def Ball_def) |
|
101 |
thus ?case by blast |
|
102 |
qed |
|
103 |
||
104 |
lemma nat_seg_image_imp_finite: |
|
105 |
"!!f A. A = f ` {i::nat. i<n} \<Longrightarrow> finite A" |
|
106 |
proof (induct n) |
|
107 |
case 0 thus ?case by simp |
|
108 |
next |
|
109 |
case (Suc n) |
|
110 |
let ?B = "f ` {i. i < n}" |
|
111 |
have finB: "finite ?B" by(rule Suc.hyps[OF refl]) |
|
112 |
show ?case |
|
113 |
proof cases |
|
114 |
assume "\<exists>k<n. f n = f k" |
|
115 |
hence "A = ?B" using Suc.prems by(auto simp:less_Suc_eq) |
|
116 |
thus ?thesis using finB by simp |
|
117 |
next |
|
118 |
assume "\<not>(\<exists> k<n. f n = f k)" |
|
119 |
hence "A = insert (f n) ?B" using Suc.prems by(auto simp:less_Suc_eq) |
|
120 |
thus ?thesis using finB by simp |
|
121 |
qed |
|
122 |
qed |
|
123 |
||
124 |
lemma finite_conv_nat_seg_image: |
|
125 |
"finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})" |
|
126 |
by(blast intro: finite_imp_nat_seg_image nat_seg_image_imp_finite) |
|
127 |
||
128 |
subsubsection{* Finiteness and set theoretic constructions *} |
|
129 |
||
12396 | 130 |
lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)" |
131 |
-- {* The union of two finite sets is finite. *} |
|
132 |
by (induct set: Finites) simp_all |
|
133 |
||
134 |
lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A" |
|
135 |
-- {* Every subset of a finite set is finite. *} |
|
136 |
proof - |
|
137 |
assume "finite B" |
|
138 |
thus "!!A. A \<subseteq> B ==> finite A" |
|
139 |
proof induct |
|
140 |
case empty |
|
141 |
thus ?case by simp |
|
142 |
next |
|
15327
0230a10582d3
changed the order of !!-quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset
|
143 |
case (insert x F A) |
12396 | 144 |
have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" . |
145 |
show "finite A" |
|
146 |
proof cases |
|
147 |
assume x: "x \<in> A" |
|
148 |
with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff) |
|
149 |
with r have "finite (A - {x})" . |
|
150 |
hence "finite (insert x (A - {x}))" .. |
|
151 |
also have "insert x (A - {x}) = A" by (rule insert_Diff) |
|
152 |
finally show ?thesis . |
|
153 |
next |
|
154 |
show "A \<subseteq> F ==> ?thesis" . |
|
155 |
assume "x \<notin> A" |
|
156 |
with A show "A \<subseteq> F" by (simp add: subset_insert_iff) |
|
157 |
qed |
|
158 |
qed |
|
159 |
qed |
|
160 |
||
161 |
lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)" |
|
162 |
by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI) |
|
163 |
||
164 |
lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)" |
|
165 |
-- {* The converse obviously fails. *} |
|
166 |
by (blast intro: finite_subset) |
|
167 |
||
168 |
lemma finite_insert [simp]: "finite (insert a A) = finite A" |
|
169 |
apply (subst insert_is_Un) |
|
14208 | 170 |
apply (simp only: finite_Un, blast) |
12396 | 171 |
done |
172 |
||
15281 | 173 |
lemma finite_Union[simp, intro]: |
174 |
"\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)" |
|
175 |
by (induct rule:finite_induct) simp_all |
|
176 |
||
12396 | 177 |
lemma finite_empty_induct: |
178 |
"finite A ==> |
|
179 |
P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}" |
|
180 |
proof - |
|
181 |
assume "finite A" |
|
182 |
and "P A" and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})" |
|
183 |
have "P (A - A)" |
|
184 |
proof - |
|
185 |
fix c b :: "'a set" |
|
186 |
presume c: "finite c" and b: "finite b" |
|
187 |
and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})" |
|
188 |
from c show "c \<subseteq> b ==> P (b - c)" |
|
189 |
proof induct |
|
190 |
case empty |
|
191 |
from P1 show ?case by simp |
|
192 |
next |
|
15327
0230a10582d3
changed the order of !!-quantifiers in finite set induction.
nipkow
parents:
15318
diff
changeset
|
193 |
case (insert x F) |
12396 | 194 |
have "P (b - F - {x})" |
195 |
proof (rule P2) |
|
196 |
from _ b show "finite (b - F)" by (rule finite_subset) blast |
|
197 |
from insert show "x \<in> b - F" by simp |
|
198 |
from insert show "P (b - F)" by simp |
|
199 |
qed |
|
200 |
also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric]) |
|
201 |
finally show ?case . |
|
202 |
qed |
|
203 |
next |
|
204 |
show "A \<subseteq> A" .. |
|
205 |
qed |
|
206 |
thus "P {}" by simp |
|
207 |
qed |
|
208 |
||
209 |
lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)" |
|
210 |
by (rule Diff_subset [THEN finite_subset]) |
|
211 |
||
212 |
lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)" |
|
213 |
apply (subst Diff_insert) |
|
214 |
apply (case_tac "a : A - B") |
|
215 |
apply (rule finite_insert [symmetric, THEN trans]) |
|
14208 | 216 |
apply (subst insert_Diff, simp_all) |
12396 | 217 |
done |
218 |
||
219 |
||
15392 | 220 |
text {* Image and Inverse Image over Finite Sets *} |
13825 | 221 |
|
222 |
lemma finite_imageI[simp]: "finite F ==> finite (h ` F)" |
|
223 |
-- {* The image of a finite set is finite. *} |
|
224 |
by (induct set: Finites) simp_all |
|
225 |
||
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset
|
226 |
lemma finite_surj: "finite A ==> B <= f ` A ==> finite B" |
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset
|
227 |
apply (frule finite_imageI) |
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset
|
228 |
apply (erule finite_subset, assumption) |
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset
|
229 |
done |
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset
|
230 |
|
13825 | 231 |
lemma finite_range_imageI: |
232 |
"finite (range g) ==> finite (range (%x. f (g x)))" |
|
14208 | 233 |
apply (drule finite_imageI, simp) |
13825 | 234 |
done |
235 |
||
12396 | 236 |
lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A" |
237 |
proof - |
|
238 |
have aux: "!!A. finite (A - {}) = finite A" by simp |
|
239 |
fix B :: "'a set" |
|
240 |
assume "finite B" |
|
241 |
thus "!!A. f`A = B ==> inj_on f A ==> finite A" |
|
242 |
apply induct |
|
243 |
apply simp |
|
244 |
apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})") |
|
245 |
apply clarify |
|
246 |
apply (simp (no_asm_use) add: inj_on_def) |
|
14208 | 247 |
apply (blast dest!: aux [THEN iffD1], atomize) |
12396 | 248 |
apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl) |
14208 | 249 |
apply (frule subsetD [OF equalityD2 insertI1], clarify) |
12396 | 250 |
apply (rule_tac x = xa in bexI) |
251 |
apply (simp_all add: inj_on_image_set_diff) |
|
252 |
done |
|
253 |
qed (rule refl) |
|
254 |
||
255 |
||
13825 | 256 |
lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}" |
257 |
-- {* The inverse image of a singleton under an injective function |
|
258 |
is included in a singleton. *} |
|
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset
|
259 |
apply (auto simp add: inj_on_def) |
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset
|
260 |
apply (blast intro: the_equality [symmetric]) |
13825 | 261 |
done |
262 |
||
263 |
lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)" |
|
264 |
-- {* The inverse image of a finite set under an injective function |
|
265 |
is finite. *} |
|
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset
|
266 |
apply (induct set: Finites, simp_all) |
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset
|
267 |
apply (subst vimage_insert) |
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset
|
268 |
apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) |
13825 | 269 |
done |
270 |
||
271 |
||
15392 | 272 |
text {* The finite UNION of finite sets *} |
12396 | 273 |
|
274 |
lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)" |
|
275 |
by (induct set: Finites) simp_all |
|
276 |
||
277 |
text {* |
|
278 |
Strengthen RHS to |
|
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset
|
279 |
@{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}? |
12396 | 280 |
|
281 |
We'd need to prove |
|
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset
|
282 |
@{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"} |
12396 | 283 |
by induction. *} |
284 |
||
285 |
lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))" |
|
286 |
by (blast intro: finite_UN_I finite_subset) |
|
287 |
||
288 |
||
15392 | 289 |
text {* Sigma of finite sets *} |
12396 | 290 |
|
291 |
lemma finite_SigmaI [simp]: |
|
292 |
"finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)" |
|
293 |
by (unfold Sigma_def) (blast intro!: finite_UN_I) |
|
294 |
||
15402 | 295 |
lemma finite_cartesian_product: "[| finite A; finite B |] ==> |
296 |
finite (A <*> B)" |
|
297 |
by (rule finite_SigmaI) |
|
298 |
||
12396 | 299 |
lemma finite_Prod_UNIV: |
300 |
"finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)" |
|
301 |
apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)") |
|
302 |
apply (erule ssubst) |
|
14208 | 303 |
apply (erule finite_SigmaI, auto) |
12396 | 304 |
done |
305 |
||
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
306 |
lemma finite_cartesian_productD1: |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
307 |
"[| finite (A <*> B); B \<noteq> {} |] ==> finite A" |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
308 |
apply (auto simp add: finite_conv_nat_seg_image) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
309 |
apply (drule_tac x=n in spec) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
310 |
apply (drule_tac x="fst o f" in spec) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
311 |
apply (auto simp add: o_def) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
312 |
prefer 2 apply (force dest!: equalityD2) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
313 |
apply (drule equalityD1) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
314 |
apply (rename_tac y x) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
315 |
apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
316 |
prefer 2 apply force |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
317 |
apply clarify |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
318 |
apply (rule_tac x=k in image_eqI, auto) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
319 |
done |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
320 |
|
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
321 |
lemma finite_cartesian_productD2: |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
322 |
"[| finite (A <*> B); A \<noteq> {} |] ==> finite B" |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
323 |
apply (auto simp add: finite_conv_nat_seg_image) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
324 |
apply (drule_tac x=n in spec) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
325 |
apply (drule_tac x="snd o f" in spec) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
326 |
apply (auto simp add: o_def) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
327 |
prefer 2 apply (force dest!: equalityD2) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
328 |
apply (drule equalityD1) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
329 |
apply (rename_tac x y) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
330 |
apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
331 |
prefer 2 apply force |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
332 |
apply clarify |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
333 |
apply (rule_tac x=k in image_eqI, auto) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
334 |
done |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
335 |
|
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
336 |
|
12396 | 337 |
instance unit :: finite |
338 |
proof |
|
339 |
have "finite {()}" by simp |
|
340 |
also have "{()} = UNIV" by auto |
|
341 |
finally show "finite (UNIV :: unit set)" . |
|
342 |
qed |
|
343 |
||
344 |
instance * :: (finite, finite) finite |
|
345 |
proof |
|
346 |
show "finite (UNIV :: ('a \<times> 'b) set)" |
|
347 |
proof (rule finite_Prod_UNIV) |
|
348 |
show "finite (UNIV :: 'a set)" by (rule finite) |
|
349 |
show "finite (UNIV :: 'b set)" by (rule finite) |
|
350 |
qed |
|
351 |
qed |
|
352 |
||
353 |
||
15392 | 354 |
text {* The powerset of a finite set *} |
12396 | 355 |
|
356 |
lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A" |
|
357 |
proof |
|
358 |
assume "finite (Pow A)" |
|
359 |
with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast |
|
360 |
thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp |
|
361 |
next |
|
362 |
assume "finite A" |
|
363 |
thus "finite (Pow A)" |
|
364 |
by induct (simp_all add: finite_UnI finite_imageI Pow_insert) |
|
365 |
qed |
|
366 |
||
15392 | 367 |
|
368 |
lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A" |
|
369 |
by(blast intro: finite_subset[OF subset_Pow_Union]) |
|
370 |
||
371 |
||
12396 | 372 |
lemma finite_converse [iff]: "finite (r^-1) = finite r" |
373 |
apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r") |
|
374 |
apply simp |
|
375 |
apply (rule iffI) |
|
376 |
apply (erule finite_imageD [unfolded inj_on_def]) |
|
377 |
apply (simp split add: split_split) |
|
378 |
apply (erule finite_imageI) |
|
14208 | 379 |
apply (simp add: converse_def image_def, auto) |
12396 | 380 |
apply (rule bexI) |
381 |
prefer 2 apply assumption |
|
382 |
apply simp |
|
383 |
done |
|
384 |
||
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset
|
385 |
|
15392 | 386 |
text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi |
387 |
Ehmety) *} |
|
12396 | 388 |
|
389 |
lemma finite_Field: "finite r ==> finite (Field r)" |
|
390 |
-- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *} |
|
391 |
apply (induct set: Finites) |
|
392 |
apply (auto simp add: Field_def Domain_insert Range_insert) |
|
393 |
done |
|
394 |
||
395 |
lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r" |
|
396 |
apply clarify |
|
397 |
apply (erule trancl_induct) |
|
398 |
apply (auto simp add: Field_def) |
|
399 |
done |
|
400 |
||
401 |
lemma finite_trancl: "finite (r^+) = finite r" |
|
402 |
apply auto |
|
403 |
prefer 2 |
|
404 |
apply (rule trancl_subset_Field2 [THEN finite_subset]) |
|
405 |
apply (rule finite_SigmaI) |
|
406 |
prefer 3 |
|
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
13595
diff
changeset
|
407 |
apply (blast intro: r_into_trancl' finite_subset) |
12396 | 408 |
apply (auto simp add: finite_Field) |
409 |
done |
|
410 |
||
411 |
||
15392 | 412 |
subsection {* A fold functional for finite sets *} |
413 |
||
414 |
text {* The intended behaviour is |
|
415 |
@{text "fold f g e {x\<^isub>1, ..., x\<^isub>n} = f (g x\<^isub>1) (\<dots> (f (g x\<^isub>n) e)\<dots>)"} |
|
416 |
if @{text f} is associative-commutative. For an application of @{text fold} |
|
417 |
se the definitions of sums and products over finite sets. |
|
418 |
*} |
|
419 |
||
420 |
consts |
|
421 |
foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \<times> 'a) set" |
|
422 |
||
423 |
inductive "foldSet f g e" |
|
424 |
intros |
|
425 |
emptyI [intro]: "({}, e) : foldSet f g e" |
|
426 |
insertI [intro]: "\<lbrakk> x \<notin> A; (A, y) : foldSet f g e \<rbrakk> |
|
427 |
\<Longrightarrow> (insert x A, f (g x) y) : foldSet f g e" |
|
428 |
||
429 |
inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g e" |
|
430 |
||
431 |
constdefs |
|
432 |
fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a" |
|
433 |
"fold f g e A == THE x. (A, x) : foldSet f g e" |
|
434 |
||
435 |
lemma Diff1_foldSet: |
|
436 |
"(A - {x}, y) : foldSet f g e ==> x: A ==> (A, f (g x) y) : foldSet f g e" |
|
437 |
by (erule insert_Diff [THEN subst], rule foldSet.intros, auto) |
|
438 |
||
439 |
lemma foldSet_imp_finite: "(A, x) : foldSet f g e ==> finite A" |
|
440 |
by (induct set: foldSet) auto |
|
441 |
||
442 |
lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f g e" |
|
443 |
by (induct set: Finites) auto |
|
444 |
||
445 |
||
446 |
subsubsection {* Commutative monoids *} |
|
447 |
locale ACf = |
|
448 |
fixes f :: "'a => 'a => 'a" (infixl "\<cdot>" 70) |
|
449 |
assumes commute: "x \<cdot> y = y \<cdot> x" |
|
450 |
and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" |
|
451 |
||
452 |
locale ACe = ACf + |
|
453 |
fixes e :: 'a |
|
454 |
assumes ident [simp]: "x \<cdot> e = x" |
|
455 |
||
456 |
lemma (in ACf) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" |
|
457 |
proof - |
|
458 |
have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute) |
|
459 |
also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc) |
|
460 |
also have "z \<cdot> x = x \<cdot> z" by (simp only: commute) |
|
461 |
finally show ?thesis . |
|
462 |
qed |
|
463 |
||
464 |
lemmas (in ACf) AC = assoc commute left_commute |
|
465 |
||
466 |
lemma (in ACe) left_ident [simp]: "e \<cdot> x = x" |
|
467 |
proof - |
|
468 |
have "x \<cdot> e = x" by (rule ident) |
|
469 |
thus ?thesis by (subst commute) |
|
470 |
qed |
|
471 |
||
15402 | 472 |
text{* Instantiation of locales: *} |
473 |
||
474 |
lemma ACf_add: "ACf (op + :: 'a::comm_monoid_add \<Rightarrow> 'a \<Rightarrow> 'a)" |
|
475 |
by(fastsimp intro: ACf.intro add_assoc add_commute) |
|
476 |
||
477 |
lemma ACe_add: "ACe (op +) (0::'a::comm_monoid_add)" |
|
478 |
by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_add) |
|
479 |
||
480 |
||
481 |
lemma ACf_mult: "ACf (op * :: 'a::comm_monoid_mult \<Rightarrow> 'a \<Rightarrow> 'a)" |
|
482 |
by(fast intro: ACf.intro mult_assoc ab_semigroup_mult.mult_commute) |
|
483 |
||
484 |
lemma ACe_mult: "ACe (op *) (1::'a::comm_monoid_mult)" |
|
485 |
by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_mult) |
|
486 |
||
487 |
||
15392 | 488 |
subsubsection{*From @{term foldSet} to @{term fold}*} |
489 |
||
490 |
lemma (in ACf) foldSet_determ_aux: |
|
491 |
"!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk> |
|
492 |
\<Longrightarrow> x' = x" |
|
493 |
proof (induct n) |
|
494 |
case 0 thus ?case by auto |
|
495 |
next |
|
496 |
case (Suc n) |
|
497 |
have IH: "!!A x x' h. \<lbrakk>A = h`{i::nat. i<n}; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk> |
|
498 |
\<Longrightarrow> x' = x" and card: "A = h`{i. i<Suc n}" |
|
499 |
and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" . |
|
500 |
show ?case |
|
501 |
proof cases |
|
502 |
assume "EX k<n. h n = h k" |
|
503 |
hence card': "A = h ` {i. i < n}" |
|
504 |
using card by (auto simp:image_def less_Suc_eq) |
|
505 |
show ?thesis by(rule IH[OF card' Afoldx Afoldy]) |
|
506 |
next |
|
507 |
assume new: "\<not>(EX k<n. h n = h k)" |
|
508 |
show ?thesis |
|
509 |
proof (rule foldSet.cases[OF Afoldx]) |
|
510 |
assume "(A, x) = ({}, e)" |
|
511 |
thus "x' = x" using Afoldy by (auto) |
|
512 |
next |
|
513 |
fix B b y |
|
514 |
assume eq1: "(A, x) = (insert b B, g b \<cdot> y)" |
|
515 |
and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B" |
|
516 |
hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto |
|
517 |
show ?thesis |
|
518 |
proof (rule foldSet.cases[OF Afoldy]) |
|
519 |
assume "(A,x') = ({}, e)" |
|
520 |
thus ?thesis using A1 by auto |
|
521 |
next |
|
522 |
fix C c z |
|
523 |
assume eq2: "(A,x') = (insert c C, g c \<cdot> z)" |
|
524 |
and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C" |
|
525 |
hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto |
|
526 |
let ?h = "%i. if h i = b then h n else h i" |
|
527 |
have less: "B = ?h`{i. i<n}" (is "_ = ?r") |
|
528 |
proof |
|
529 |
show "B \<subseteq> ?r" |
|
530 |
proof |
|
531 |
fix u assume "u \<in> B" |
|
532 |
hence uinA: "u \<in> A" and unotb: "u \<noteq> b" using A1 notinB by blast+ |
|
533 |
then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u" |
|
534 |
using card by(auto simp:image_def) |
|
535 |
show "u \<in> ?r" |
|
536 |
proof cases |
|
537 |
assume "i\<^isub>u < n" |
|
538 |
thus ?thesis using unotb by(fastsimp) |
|
539 |
next |
|
540 |
assume "\<not> i\<^isub>u < n" |
|
541 |
with below have [simp]: "i\<^isub>u = n" by arith |
|
542 |
obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "b = h i\<^isub>k" |
|
543 |
using A1 card by blast |
|
544 |
have "i\<^isub>k < n" |
|
545 |
proof (rule ccontr) |
|
546 |
assume "\<not> i\<^isub>k < n" |
|
547 |
hence "i\<^isub>k = n" using i\<^isub>k by arith |
|
548 |
thus False using unotb by simp |
|
549 |
qed |
|
550 |
thus ?thesis by(auto simp add:image_def) |
|
551 |
qed |
|
552 |
qed |
|
553 |
next |
|
554 |
show "?r \<subseteq> B" |
|
555 |
proof |
|
556 |
fix u assume "u \<in> ?r" |
|
557 |
then obtain i\<^isub>u where below: "i\<^isub>u < n" and |
|
558 |
or: "b = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u" |
|
559 |
by(auto simp:image_def) |
|
560 |
from or show "u \<in> B" |
|
561 |
proof |
|
562 |
assume [simp]: "b = h i\<^isub>u \<and> u = h n" |
|
563 |
have "u \<in> A" using card by auto |
|
564 |
moreover have "u \<noteq> b" using new below by auto |
|
565 |
ultimately show "u \<in> B" using A1 by blast |
|
566 |
next |
|
567 |
assume "h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u" |
|
568 |
moreover hence "u \<in> A" using card below by auto |
|
569 |
ultimately show "u \<in> B" using A1 by blast |
|
570 |
qed |
|
571 |
qed |
|
572 |
qed |
|
573 |
show ?thesis |
|
574 |
proof cases |
|
575 |
assume "b = c" |
|
576 |
then moreover have "B = C" using A1 A2 notinB notinC by auto |
|
577 |
ultimately show ?thesis using IH[OF less] y z x x' by auto |
|
578 |
next |
|
579 |
assume diff: "b \<noteq> c" |
|
580 |
let ?D = "B - {c}" |
|
581 |
have B: "B = insert c ?D" and C: "C = insert b ?D" |
|
582 |
using A1 A2 notinB notinC diff by(blast elim!:equalityE)+ |
|
15402 | 583 |
have "finite A" by(rule foldSet_imp_finite[OF Afoldx]) |
584 |
with A1 have "finite ?D" by simp |
|
15392 | 585 |
then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e" |
586 |
using finite_imp_foldSet by rules |
|
587 |
moreover have cinB: "c \<in> B" using B by(auto) |
|
588 |
ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e" |
|
589 |
by(rule Diff1_foldSet) |
|
590 |
hence "g c \<cdot> d = y" by(rule IH[OF less y]) |
|
591 |
moreover have "g b \<cdot> d = z" |
|
592 |
proof (rule IH[OF _ z]) |
|
593 |
let ?h = "%i. if h i = c then h n else h i" |
|
594 |
show "C = ?h`{i. i<n}" (is "_ = ?r") |
|
595 |
proof |
|
596 |
show "C \<subseteq> ?r" |
|
597 |
proof |
|
598 |
fix u assume "u \<in> C" |
|
599 |
hence uinA: "u \<in> A" and unotc: "u \<noteq> c" |
|
600 |
using A2 notinC by blast+ |
|
601 |
then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u" |
|
602 |
using card by(auto simp:image_def) |
|
603 |
show "u \<in> ?r" |
|
604 |
proof cases |
|
605 |
assume "i\<^isub>u < n" |
|
606 |
thus ?thesis using unotc by(fastsimp) |
|
607 |
next |
|
608 |
assume "\<not> i\<^isub>u < n" |
|
609 |
with below have [simp]: "i\<^isub>u = n" by arith |
|
610 |
obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "c = h i\<^isub>k" |
|
611 |
using A2 card by blast |
|
612 |
have "i\<^isub>k < n" |
|
613 |
proof (rule ccontr) |
|
614 |
assume "\<not> i\<^isub>k < n" |
|
615 |
hence "i\<^isub>k = n" using i\<^isub>k by arith |
|
616 |
thus False using unotc by simp |
|
617 |
qed |
|
618 |
thus ?thesis by(auto simp add:image_def) |
|
619 |
qed |
|
620 |
qed |
|
621 |
next |
|
622 |
show "?r \<subseteq> C" |
|
623 |
proof |
|
624 |
fix u assume "u \<in> ?r" |
|
625 |
then obtain i\<^isub>u where below: "i\<^isub>u < n" and |
|
626 |
or: "c = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> c \<and> h i\<^isub>u = u" |
|
627 |
by(auto simp:image_def) |
|
628 |
from or show "u \<in> C" |
|
629 |
proof |
|
630 |
assume [simp]: "c = h i\<^isub>u \<and> u = h n" |
|
631 |
have "u \<in> A" using card by auto |
|
632 |
moreover have "u \<noteq> c" using new below by auto |
|
633 |
ultimately show "u \<in> C" using A2 by blast |
|
634 |
next |
|
635 |
assume "h i\<^isub>u \<noteq> c \<and> h i\<^isub>u = u" |
|
636 |
moreover hence "u \<in> A" using card below by auto |
|
637 |
ultimately show "u \<in> C" using A2 by blast |
|
638 |
qed |
|
639 |
qed |
|
640 |
qed |
|
641 |
next |
|
642 |
show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd |
|
643 |
by fastsimp |
|
644 |
qed |
|
645 |
ultimately show ?thesis using x x' by(auto simp:AC) |
|
646 |
qed |
|
647 |
qed |
|
648 |
qed |
|
649 |
qed |
|
650 |
qed |
|
651 |
||
652 |
(* The same proof, but using card |
|
653 |
lemma (in ACf) foldSet_determ_aux: |
|
654 |
"!!A x x'. \<lbrakk> card A < n; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk> |
|
655 |
\<Longrightarrow> x' = x" |
|
656 |
proof (induct n) |
|
657 |
case 0 thus ?case by simp |
|
658 |
next |
|
659 |
case (Suc n) |
|
660 |
have IH: "!!A x x'. \<lbrakk>card A < n; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk> |
|
661 |
\<Longrightarrow> x' = x" and card: "card A < Suc n" |
|
662 |
and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" . |
|
663 |
from card have "card A < n \<or> card A = n" by arith |
|
664 |
thus ?case |
|
665 |
proof |
|
666 |
assume less: "card A < n" |
|
667 |
show ?thesis by(rule IH[OF less Afoldx Afoldy]) |
|
668 |
next |
|
669 |
assume cardA: "card A = n" |
|
670 |
show ?thesis |
|
671 |
proof (rule foldSet.cases[OF Afoldx]) |
|
672 |
assume "(A, x) = ({}, e)" |
|
673 |
thus "x' = x" using Afoldy by (auto) |
|
674 |
next |
|
675 |
fix B b y |
|
676 |
assume eq1: "(A, x) = (insert b B, g b \<cdot> y)" |
|
677 |
and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B" |
|
678 |
hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto |
|
679 |
show ?thesis |
|
680 |
proof (rule foldSet.cases[OF Afoldy]) |
|
681 |
assume "(A,x') = ({}, e)" |
|
682 |
thus ?thesis using A1 by auto |
|
683 |
next |
|
684 |
fix C c z |
|
685 |
assume eq2: "(A,x') = (insert c C, g c \<cdot> z)" |
|
686 |
and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C" |
|
687 |
hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto |
|
688 |
have finA: "finite A" by(rule foldSet_imp_finite[OF Afoldx]) |
|
689 |
with cardA A1 notinB have less: "card B < n" by simp |
|
690 |
show ?thesis |
|
691 |
proof cases |
|
692 |
assume "b = c" |
|
693 |
then moreover have "B = C" using A1 A2 notinB notinC by auto |
|
694 |
ultimately show ?thesis using IH[OF less] y z x x' by auto |
|
695 |
next |
|
696 |
assume diff: "b \<noteq> c" |
|
697 |
let ?D = "B - {c}" |
|
698 |
have B: "B = insert c ?D" and C: "C = insert b ?D" |
|
699 |
using A1 A2 notinB notinC diff by(blast elim!:equalityE)+ |
|
700 |
have "finite ?D" using finA A1 by simp |
|
701 |
then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e" |
|
702 |
using finite_imp_foldSet by rules |
|
703 |
moreover have cinB: "c \<in> B" using B by(auto) |
|
704 |
ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e" |
|
705 |
by(rule Diff1_foldSet) |
|
706 |
hence "g c \<cdot> d = y" by(rule IH[OF less y]) |
|
707 |
moreover have "g b \<cdot> d = z" |
|
708 |
proof (rule IH[OF _ z]) |
|
709 |
show "card C < n" using C cardA A1 notinB finA cinB |
|
710 |
by(auto simp:card_Diff1_less) |
|
711 |
next |
|
712 |
show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd |
|
713 |
by fastsimp |
|
714 |
qed |
|
715 |
ultimately show ?thesis using x x' by(auto simp:AC) |
|
716 |
qed |
|
717 |
qed |
|
718 |
qed |
|
719 |
qed |
|
720 |
qed |
|
721 |
*) |
|
722 |
||
723 |
lemma (in ACf) foldSet_determ: |
|
724 |
"(A, x) : foldSet f g e ==> (A, y) : foldSet f g e ==> y = x" |
|
725 |
apply(frule foldSet_imp_finite) |
|
726 |
apply(simp add:finite_conv_nat_seg_image) |
|
727 |
apply(blast intro: foldSet_determ_aux [rule_format]) |
|
728 |
done |
|
729 |
||
730 |
lemma (in ACf) fold_equality: "(A, y) : foldSet f g e ==> fold f g e A = y" |
|
731 |
by (unfold fold_def) (blast intro: foldSet_determ) |
|
732 |
||
733 |
text{* The base case for @{text fold}: *} |
|
734 |
||
735 |
lemma fold_empty [simp]: "fold f g e {} = e" |
|
736 |
by (unfold fold_def) blast |
|
737 |
||
738 |
lemma (in ACf) fold_insert_aux: "x \<notin> A ==> |
|
739 |
((insert x A, v) : foldSet f g e) = |
|
740 |
(EX y. (A, y) : foldSet f g e & v = f (g x) y)" |
|
741 |
apply auto |
|
742 |
apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE]) |
|
743 |
apply (fastsimp dest: foldSet_imp_finite) |
|
744 |
apply (blast intro: foldSet_determ) |
|
745 |
done |
|
746 |
||
747 |
text{* The recursion equation for @{text fold}: *} |
|
748 |
||
749 |
lemma (in ACf) fold_insert[simp]: |
|
750 |
"finite A ==> x \<notin> A ==> fold f g e (insert x A) = f (g x) (fold f g e A)" |
|
751 |
apply (unfold fold_def) |
|
752 |
apply (simp add: fold_insert_aux) |
|
753 |
apply (rule the_equality) |
|
754 |
apply (auto intro: finite_imp_foldSet |
|
755 |
cong add: conj_cong simp add: fold_def [symmetric] fold_equality) |
|
756 |
done |
|
757 |
||
758 |
declare |
|
759 |
empty_foldSetE [rule del] foldSet.intros [rule del] |
|
760 |
-- {* Delete rules to do with @{text foldSet} relation. *} |
|
761 |
||
762 |
subsubsection{*Lemmas about @{text fold}*} |
|
763 |
||
764 |
lemma (in ACf) fold_commute: |
|
765 |
"finite A ==> (!!e. f (g x) (fold f g e A) = fold f g (f (g x) e) A)" |
|
766 |
apply (induct set: Finites, simp) |
|
767 |
apply (simp add: left_commute) |
|
768 |
done |
|
769 |
||
770 |
lemma (in ACf) fold_nest_Un_Int: |
|
771 |
"finite A ==> finite B |
|
772 |
==> fold f g (fold f g e B) A = fold f g (fold f g e (A Int B)) (A Un B)" |
|
773 |
apply (induct set: Finites, simp) |
|
774 |
apply (simp add: fold_commute Int_insert_left insert_absorb) |
|
775 |
done |
|
776 |
||
777 |
lemma (in ACf) fold_nest_Un_disjoint: |
|
778 |
"finite A ==> finite B ==> A Int B = {} |
|
779 |
==> fold f g e (A Un B) = fold f g (fold f g e B) A" |
|
780 |
by (simp add: fold_nest_Un_Int) |
|
781 |
||
782 |
lemma (in ACf) fold_reindex: |
|
783 |
assumes fin: "finite B" |
|
784 |
shows "inj_on h B \<Longrightarrow> fold f g e (h ` B) = fold f (g \<circ> h) e B" |
|
785 |
using fin apply (induct) |
|
786 |
apply simp |
|
787 |
apply simp |
|
788 |
done |
|
789 |
||
790 |
lemma (in ACe) fold_Un_Int: |
|
791 |
"finite A ==> finite B ==> |
|
792 |
fold f g e A \<cdot> fold f g e B = |
|
793 |
fold f g e (A Un B) \<cdot> fold f g e (A Int B)" |
|
794 |
apply (induct set: Finites, simp) |
|
795 |
apply (simp add: AC insert_absorb Int_insert_left) |
|
796 |
done |
|
797 |
||
798 |
corollary (in ACe) fold_Un_disjoint: |
|
799 |
"finite A ==> finite B ==> A Int B = {} ==> |
|
800 |
fold f g e (A Un B) = fold f g e A \<cdot> fold f g e B" |
|
801 |
by (simp add: fold_Un_Int) |
|
802 |
||
803 |
lemma (in ACe) fold_UN_disjoint: |
|
804 |
"\<lbrakk> finite I; ALL i:I. finite (A i); |
|
805 |
ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk> |
|
806 |
\<Longrightarrow> fold f g e (UNION I A) = |
|
807 |
fold f (%i. fold f g e (A i)) e I" |
|
808 |
apply (induct set: Finites, simp, atomize) |
|
809 |
apply (subgoal_tac "ALL i:F. x \<noteq> i") |
|
810 |
prefer 2 apply blast |
|
811 |
apply (subgoal_tac "A x Int UNION F A = {}") |
|
812 |
prefer 2 apply blast |
|
813 |
apply (simp add: fold_Un_disjoint) |
|
814 |
done |
|
815 |
||
816 |
lemma (in ACf) fold_cong: |
|
817 |
"finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g a A = fold f h a A" |
|
818 |
apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold f g a C = fold f h a C") |
|
819 |
apply simp |
|
820 |
apply (erule finite_induct, simp) |
|
821 |
apply (simp add: subset_insert_iff, clarify) |
|
822 |
apply (subgoal_tac "finite C") |
|
823 |
prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl]) |
|
824 |
apply (subgoal_tac "C = insert x (C - {x})") |
|
825 |
prefer 2 apply blast |
|
826 |
apply (erule ssubst) |
|
827 |
apply (drule spec) |
|
828 |
apply (erule (1) notE impE) |
|
829 |
apply (simp add: Ball_def del: insert_Diff_single) |
|
830 |
done |
|
831 |
||
832 |
lemma (in ACe) fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==> |
|
833 |
fold f (%x. fold f (g x) e (B x)) e A = |
|
834 |
fold f (split g) e (SIGMA x:A. B x)" |
|
835 |
apply (subst Sigma_def) |
|
836 |
apply (subst fold_UN_disjoint) |
|
837 |
apply assumption |
|
838 |
apply simp |
|
839 |
apply blast |
|
840 |
apply (erule fold_cong) |
|
841 |
apply (subst fold_UN_disjoint) |
|
842 |
apply simp |
|
843 |
apply simp |
|
844 |
apply blast |
|
845 |
apply (simp) |
|
846 |
done |
|
847 |
||
848 |
lemma (in ACe) fold_distrib: "finite A \<Longrightarrow> |
|
849 |
fold f (%x. f (g x) (h x)) e A = f (fold f g e A) (fold f h e A)" |
|
850 |
apply (erule finite_induct) |
|
851 |
apply simp |
|
852 |
apply (simp add:AC) |
|
853 |
done |
|
854 |
||
855 |
||
15402 | 856 |
subsection {* Generalized summation over a set *} |
857 |
||
858 |
constdefs |
|
859 |
setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add" |
|
860 |
"setsum f A == if finite A then fold (op +) f 0 A else 0" |
|
861 |
||
862 |
text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is |
|
863 |
written @{text"\<Sum>x\<in>A. e"}. *} |
|
864 |
||
865 |
syntax |
|
866 |
"_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_. _)" [0, 51, 10] 10) |
|
867 |
syntax (xsymbols) |
|
868 |
"_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) |
|
869 |
syntax (HTML output) |
|
870 |
"_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) |
|
871 |
||
872 |
translations -- {* Beware of argument permutation! *} |
|
873 |
"SUM i:A. b" == "setsum (%i. b) A" |
|
874 |
"\<Sum>i\<in>A. b" == "setsum (%i. b) A" |
|
875 |
||
876 |
text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter |
|
877 |
@{text"\<Sum>x|P. e"}. *} |
|
878 |
||
879 |
syntax |
|
880 |
"_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10) |
|
881 |
syntax (xsymbols) |
|
882 |
"_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10) |
|
883 |
syntax (HTML output) |
|
884 |
"_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10) |
|
885 |
||
886 |
translations |
|
887 |
"SUM x|P. t" => "setsum (%x. t) {x. P}" |
|
888 |
"\<Sum>x|P. t" => "setsum (%x. t) {x. P}" |
|
889 |
||
890 |
text{* Finally we abbreviate @{term"\<Sum>x\<in>A. x"} by @{text"\<Sum>A"}. *} |
|
891 |
||
892 |
syntax |
|
893 |
"_Setsum" :: "'a set => 'a::comm_monoid_mult" ("\<Sum>_" [1000] 999) |
|
894 |
||
895 |
parse_translation {* |
|
896 |
let |
|
897 |
fun Setsum_tr [A] = Syntax.const "setsum" $ Abs ("", dummyT, Bound 0) $ A |
|
898 |
in [("_Setsum", Setsum_tr)] end; |
|
899 |
*} |
|
900 |
||
901 |
print_translation {* |
|
902 |
let |
|
903 |
fun setsum_tr' [Abs(_,_,Bound 0), A] = Syntax.const "_Setsum" $ A |
|
904 |
| setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = |
|
905 |
if x<>y then raise Match |
|
906 |
else let val x' = Syntax.mark_bound x |
|
907 |
val t' = subst_bound(x',t) |
|
908 |
val P' = subst_bound(x',P) |
|
909 |
in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end |
|
910 |
in |
|
911 |
[("setsum", setsum_tr')] |
|
912 |
end |
|
913 |
*} |
|
914 |
||
915 |
lemma setsum_empty [simp]: "setsum f {} = 0" |
|
916 |
by (simp add: setsum_def) |
|
917 |
||
918 |
lemma setsum_insert [simp]: |
|
919 |
"finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F" |
|
920 |
by (simp add: setsum_def ACf.fold_insert [OF ACf_add]) |
|
921 |
||
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
922 |
lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0" |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
923 |
by (simp add: setsum_def) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
924 |
|
15402 | 925 |
lemma setsum_reindex: |
926 |
"inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B" |
|
927 |
by(auto simp add: setsum_def ACf.fold_reindex[OF ACf_add] dest!:finite_imageD) |
|
928 |
||
929 |
lemma setsum_reindex_id: |
|
930 |
"inj_on f B ==> setsum f B = setsum id (f ` B)" |
|
931 |
by (auto simp add: setsum_reindex) |
|
932 |
||
933 |
lemma setsum_cong: |
|
934 |
"A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B" |
|
935 |
by(fastsimp simp: setsum_def intro: ACf.fold_cong[OF ACf_add]) |
|
936 |
||
937 |
lemma setsum_reindex_cong: |
|
938 |
"[|inj_on f A; B = f ` A; !!a. g a = h (f a)|] |
|
939 |
==> setsum h B = setsum g A" |
|
940 |
by (simp add: setsum_reindex cong: setsum_cong) |
|
941 |
||
942 |
lemma setsum_0: "setsum (%i. 0) A = 0" |
|
943 |
apply (clarsimp simp: setsum_def) |
|
944 |
apply (erule finite_induct, auto simp:ACf.fold_insert [OF ACf_add]) |
|
945 |
done |
|
946 |
||
947 |
lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0" |
|
948 |
apply (subgoal_tac "setsum f F = setsum (%x. 0) F") |
|
949 |
apply (erule ssubst, rule setsum_0) |
|
950 |
apply (rule setsum_cong, auto) |
|
951 |
done |
|
952 |
||
953 |
lemma setsum_Un_Int: "finite A ==> finite B ==> |
|
954 |
setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B" |
|
955 |
-- {* The reversed orientation looks more natural, but LOOPS as a simprule! *} |
|
956 |
by(simp add: setsum_def ACe.fold_Un_Int[OF ACe_add,symmetric]) |
|
957 |
||
958 |
lemma setsum_Un_disjoint: "finite A ==> finite B |
|
959 |
==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B" |
|
960 |
by (subst setsum_Un_Int [symmetric], auto) |
|
961 |
||
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
962 |
(*But we can't get rid of finite I. If infinite, although the rhs is 0, |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
963 |
the lhs need not be, since UNION I A could still be finite.*) |
15402 | 964 |
lemma setsum_UN_disjoint: |
965 |
"finite I ==> (ALL i:I. finite (A i)) ==> |
|
966 |
(ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==> |
|
967 |
setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))" |
|
968 |
by(simp add: setsum_def ACe.fold_UN_disjoint[OF ACe_add] cong: setsum_cong) |
|
969 |
||
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
970 |
text{*No need to assume that @{term C} is finite. If infinite, the rhs is |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
971 |
directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*} |
15402 | 972 |
lemma setsum_Union_disjoint: |
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
973 |
"[| (ALL A:C. finite A); |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
974 |
(ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
975 |
==> setsum f (Union C) = setsum (setsum f) C" |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
976 |
apply (cases "finite C") |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
977 |
prefer 2 apply (force dest: finite_UnionD simp add: setsum_def) |
15402 | 978 |
apply (frule setsum_UN_disjoint [of C id f]) |
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
979 |
apply (unfold Union_def id_def, assumption+) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
980 |
done |
15402 | 981 |
|
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
982 |
(*But we can't get rid of finite A. If infinite, although the lhs is 0, |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
983 |
the rhs need not be, since SIGMA A B could still be finite.*) |
15402 | 984 |
lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==> |
985 |
(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = |
|
986 |
(\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))" |
|
987 |
by(simp add:setsum_def ACe.fold_Sigma[OF ACe_add] split_def cong:setsum_cong) |
|
988 |
||
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
989 |
text{*Here we can eliminate the finiteness assumptions, by cases.*} |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
990 |
lemma setsum_cartesian_product: |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
991 |
"(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>z\<in>A <*> B. f (fst z) (snd z))" |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
992 |
apply (cases "finite A") |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
993 |
apply (cases "finite B") |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
994 |
apply (simp add: setsum_Sigma) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
995 |
apply (cases "A={}", simp) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
996 |
apply (simp add: setsum_0) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
997 |
apply (auto simp add: setsum_def |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
998 |
dest: finite_cartesian_productD1 finite_cartesian_productD2) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
999 |
done |
15402 | 1000 |
|
1001 |
lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)" |
|
1002 |
by(simp add:setsum_def ACe.fold_distrib[OF ACe_add]) |
|
1003 |
||
1004 |
||
1005 |
subsubsection {* Properties in more restricted classes of structures *} |
|
1006 |
||
1007 |
lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a" |
|
1008 |
apply (case_tac "finite A") |
|
1009 |
prefer 2 apply (simp add: setsum_def) |
|
1010 |
apply (erule rev_mp) |
|
1011 |
apply (erule finite_induct, auto) |
|
1012 |
done |
|
1013 |
||
1014 |
lemma setsum_eq_0_iff [simp]: |
|
1015 |
"finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))" |
|
1016 |
by (induct set: Finites) auto |
|
1017 |
||
1018 |
lemma setsum_Un_nat: "finite A ==> finite B ==> |
|
1019 |
(setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)" |
|
1020 |
-- {* For the natural numbers, we have subtraction. *} |
|
1021 |
by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps) |
|
1022 |
||
1023 |
lemma setsum_Un: "finite A ==> finite B ==> |
|
1024 |
(setsum f (A Un B) :: 'a :: ab_group_add) = |
|
1025 |
setsum f A + setsum f B - setsum f (A Int B)" |
|
1026 |
by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps) |
|
1027 |
||
1028 |
lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) = |
|
1029 |
(if a:A then setsum f A - f a else setsum f A)" |
|
1030 |
apply (case_tac "finite A") |
|
1031 |
prefer 2 apply (simp add: setsum_def) |
|
1032 |
apply (erule finite_induct) |
|
1033 |
apply (auto simp add: insert_Diff_if) |
|
1034 |
apply (drule_tac a = a in mk_disjoint_insert, auto) |
|
1035 |
done |
|
1036 |
||
1037 |
lemma setsum_diff1: "finite A \<Longrightarrow> |
|
1038 |
(setsum f (A - {a}) :: ('a::ab_group_add)) = |
|
1039 |
(if a:A then setsum f A - f a else setsum f A)" |
|
1040 |
by (erule finite_induct) (auto simp add: insert_Diff_if) |
|
1041 |
||
1042 |
(* By Jeremy Siek: *) |
|
1043 |
||
1044 |
lemma setsum_diff_nat: |
|
1045 |
assumes finB: "finite B" |
|
1046 |
shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)" |
|
1047 |
using finB |
|
1048 |
proof (induct) |
|
1049 |
show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp |
|
1050 |
next |
|
1051 |
fix F x assume finF: "finite F" and xnotinF: "x \<notin> F" |
|
1052 |
and xFinA: "insert x F \<subseteq> A" |
|
1053 |
and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F" |
|
1054 |
from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp |
|
1055 |
from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x" |
|
1056 |
by (simp add: setsum_diff1_nat) |
|
1057 |
from xFinA have "F \<subseteq> A" by simp |
|
1058 |
with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp |
|
1059 |
with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x" |
|
1060 |
by simp |
|
1061 |
from xnotinF have "A - insert x F = (A - F) - {x}" by auto |
|
1062 |
with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x" |
|
1063 |
by simp |
|
1064 |
from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp |
|
1065 |
with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" |
|
1066 |
by simp |
|
1067 |
thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp |
|
1068 |
qed |
|
1069 |
||
1070 |
lemma setsum_diff: |
|
1071 |
assumes le: "finite A" "B \<subseteq> A" |
|
1072 |
shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))" |
|
1073 |
proof - |
|
1074 |
from le have finiteB: "finite B" using finite_subset by auto |
|
1075 |
show ?thesis using finiteB le |
|
1076 |
proof (induct) |
|
1077 |
case empty |
|
1078 |
thus ?case by auto |
|
1079 |
next |
|
1080 |
case (insert x F) |
|
1081 |
thus ?case using le finiteB |
|
1082 |
by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb) |
|
1083 |
qed |
|
1084 |
qed |
|
1085 |
||
1086 |
lemma setsum_mono: |
|
1087 |
assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))" |
|
1088 |
shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)" |
|
1089 |
proof (cases "finite K") |
|
1090 |
case True |
|
1091 |
thus ?thesis using le |
|
1092 |
proof (induct) |
|
1093 |
case empty |
|
1094 |
thus ?case by simp |
|
1095 |
next |
|
1096 |
case insert |
|
1097 |
thus ?case using add_mono |
|
1098 |
by force |
|
1099 |
qed |
|
1100 |
next |
|
1101 |
case False |
|
1102 |
thus ?thesis |
|
1103 |
by (simp add: setsum_def) |
|
1104 |
qed |
|
1105 |
||
1106 |
lemma setsum_mono2_nat: |
|
1107 |
assumes fin: "finite B" and sub: "A \<subseteq> B" |
|
1108 |
shows "setsum f A \<le> (setsum f B :: nat)" |
|
1109 |
proof - |
|
1110 |
have "setsum f A \<le> setsum f A + setsum f (B-A)" by arith |
|
1111 |
also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin] |
|
1112 |
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) |
|
1113 |
also have "A \<union> (B-A) = B" using sub by blast |
|
1114 |
finally show ?thesis . |
|
1115 |
qed |
|
1116 |
||
1117 |
lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ab_group_add) A = |
|
1118 |
- setsum f A" |
|
1119 |
by (induct set: Finites, auto) |
|
1120 |
||
1121 |
lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ab_group_add) - g x) A = |
|
1122 |
setsum f A - setsum g A" |
|
1123 |
by (simp add: diff_minus setsum_addf setsum_negf) |
|
1124 |
||
1125 |
lemma setsum_nonneg: "[| finite A; |
|
1126 |
\<forall>x \<in> A. (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) \<le> f x |] ==> |
|
1127 |
0 \<le> setsum f A"; |
|
1128 |
apply (induct set: Finites, auto) |
|
1129 |
apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp) |
|
1130 |
apply (blast intro: add_mono) |
|
1131 |
done |
|
1132 |
||
1133 |
lemma setsum_nonpos: "[| finite A; |
|
1134 |
\<forall>x \<in> A. f x \<le> (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) |] ==> |
|
1135 |
setsum f A \<le> 0"; |
|
1136 |
apply (induct set: Finites, auto) |
|
1137 |
apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp) |
|
1138 |
apply (blast intro: add_mono) |
|
1139 |
done |
|
1140 |
||
1141 |
lemma setsum_mult: |
|
1142 |
fixes f :: "'a => ('b::semiring_0_cancel)" |
|
1143 |
shows "r * setsum f A = setsum (%n. r * f n) A" |
|
1144 |
proof (cases "finite A") |
|
1145 |
case True |
|
1146 |
thus ?thesis |
|
1147 |
proof (induct) |
|
1148 |
case empty thus ?case by simp |
|
1149 |
next |
|
1150 |
case (insert x A) thus ?case by (simp add: right_distrib) |
|
1151 |
qed |
|
1152 |
next |
|
1153 |
case False thus ?thesis by (simp add: setsum_def) |
|
1154 |
qed |
|
1155 |
||
1156 |
lemma setsum_abs: |
|
1157 |
fixes f :: "'a => ('b::lordered_ab_group_abs)" |
|
1158 |
assumes fin: "finite A" |
|
1159 |
shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A" |
|
1160 |
using fin |
|
1161 |
proof (induct) |
|
1162 |
case empty thus ?case by simp |
|
1163 |
next |
|
1164 |
case (insert x A) |
|
1165 |
thus ?case by (auto intro: abs_triangle_ineq order_trans) |
|
1166 |
qed |
|
1167 |
||
1168 |
lemma setsum_abs_ge_zero: |
|
1169 |
fixes f :: "'a => ('b::lordered_ab_group_abs)" |
|
1170 |
assumes fin: "finite A" |
|
1171 |
shows "0 \<le> setsum (%i. abs(f i)) A" |
|
1172 |
using fin |
|
1173 |
proof (induct) |
|
1174 |
case empty thus ?case by simp |
|
1175 |
next |
|
1176 |
case (insert x A) thus ?case by (auto intro: order_trans) |
|
1177 |
qed |
|
1178 |
||
1179 |
||
1180 |
subsection {* Generalized product over a set *} |
|
1181 |
||
1182 |
constdefs |
|
1183 |
setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult" |
|
1184 |
"setprod f A == if finite A then fold (op *) f 1 A else 1" |
|
1185 |
||
1186 |
syntax |
|
1187 |
"_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_:_. _)" [0, 51, 10] 10) |
|
1188 |
||
1189 |
syntax (xsymbols) |
|
1190 |
"_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) |
|
1191 |
syntax (HTML output) |
|
1192 |
"_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) |
|
1193 |
translations |
|
1194 |
"\<Prod>i:A. b" == "setprod (%i. b) A" -- {* Beware of argument permutation! *} |
|
1195 |
||
1196 |
syntax |
|
1197 |
"_Setprod" :: "'a set => 'a::comm_monoid_mult" ("\<Prod>_" [1000] 999) |
|
1198 |
||
1199 |
parse_translation {* |
|
1200 |
let |
|
1201 |
fun Setprod_tr [A] = Syntax.const "setprod" $ Abs ("", dummyT, Bound 0) $ A |
|
1202 |
in [("_Setprod", Setprod_tr)] end; |
|
1203 |
*} |
|
1204 |
print_translation {* |
|
1205 |
let fun setprod_tr' [Abs(x,Tx,t), A] = |
|
1206 |
if t = Bound 0 then Syntax.const "_Setprod" $ A else raise Match |
|
1207 |
in |
|
1208 |
[("setprod", setprod_tr')] |
|
1209 |
end |
|
1210 |
*} |
|
1211 |
||
1212 |
||
1213 |
lemma setprod_empty [simp]: "setprod f {} = 1" |
|
1214 |
by (auto simp add: setprod_def) |
|
1215 |
||
1216 |
lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==> |
|
1217 |
setprod f (insert a A) = f a * setprod f A" |
|
1218 |
by (simp add: setprod_def ACf.fold_insert [OF ACf_mult]) |
|
1219 |
||
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1220 |
lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1" |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1221 |
by (simp add: setprod_def) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1222 |
|
15402 | 1223 |
lemma setprod_reindex: |
1224 |
"inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B" |
|
1225 |
by(auto simp: setprod_def ACf.fold_reindex[OF ACf_mult] dest!:finite_imageD) |
|
1226 |
||
1227 |
lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)" |
|
1228 |
by (auto simp add: setprod_reindex) |
|
1229 |
||
1230 |
lemma setprod_cong: |
|
1231 |
"A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B" |
|
1232 |
by(fastsimp simp: setprod_def intro: ACf.fold_cong[OF ACf_mult]) |
|
1233 |
||
1234 |
lemma setprod_reindex_cong: "inj_on f A ==> |
|
1235 |
B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A" |
|
1236 |
by (frule setprod_reindex, simp) |
|
1237 |
||
1238 |
||
1239 |
lemma setprod_1: "setprod (%i. 1) A = 1" |
|
1240 |
apply (case_tac "finite A") |
|
1241 |
apply (erule finite_induct, auto simp add: mult_ac) |
|
1242 |
done |
|
1243 |
||
1244 |
lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1" |
|
1245 |
apply (subgoal_tac "setprod f F = setprod (%x. 1) F") |
|
1246 |
apply (erule ssubst, rule setprod_1) |
|
1247 |
apply (rule setprod_cong, auto) |
|
1248 |
done |
|
1249 |
||
1250 |
lemma setprod_Un_Int: "finite A ==> finite B |
|
1251 |
==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B" |
|
1252 |
by(simp add: setprod_def ACe.fold_Un_Int[OF ACe_mult,symmetric]) |
|
1253 |
||
1254 |
lemma setprod_Un_disjoint: "finite A ==> finite B |
|
1255 |
==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B" |
|
1256 |
by (subst setprod_Un_Int [symmetric], auto) |
|
1257 |
||
1258 |
lemma setprod_UN_disjoint: |
|
1259 |
"finite I ==> (ALL i:I. finite (A i)) ==> |
|
1260 |
(ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==> |
|
1261 |
setprod f (UNION I A) = setprod (%i. setprod f (A i)) I" |
|
1262 |
by(simp add: setprod_def ACe.fold_UN_disjoint[OF ACe_mult] cong: setprod_cong) |
|
1263 |
||
1264 |
lemma setprod_Union_disjoint: |
|
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1265 |
"[| (ALL A:C. finite A); |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1266 |
(ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1267 |
==> setprod f (Union C) = setprod (setprod f) C" |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1268 |
apply (cases "finite C") |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1269 |
prefer 2 apply (force dest: finite_UnionD simp add: setprod_def) |
15402 | 1270 |
apply (frule setprod_UN_disjoint [of C id f]) |
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1271 |
apply (unfold Union_def id_def, assumption+) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1272 |
done |
15402 | 1273 |
|
1274 |
lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==> |
|
1275 |
(\<Prod>x:A. (\<Prod>y: B x. f x y)) = |
|
1276 |
(\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))" |
|
1277 |
by(simp add:setprod_def ACe.fold_Sigma[OF ACe_mult] split_def cong:setprod_cong) |
|
1278 |
||
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1279 |
text{*Here we can eliminate the finiteness assumptions, by cases.*} |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1280 |
lemma setprod_cartesian_product: |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1281 |
"(\<Prod>x:A. (\<Prod>y: B. f x y)) = (\<Prod>z:(A <*> B). f (fst z) (snd z))" |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1282 |
apply (cases "finite A") |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1283 |
apply (cases "finite B") |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1284 |
apply (simp add: setprod_Sigma) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1285 |
apply (cases "A={}", simp) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1286 |
apply (simp add: setprod_1) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1287 |
apply (auto simp add: setprod_def |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1288 |
dest: finite_cartesian_productD1 finite_cartesian_productD2) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1289 |
done |
15402 | 1290 |
|
1291 |
lemma setprod_timesf: |
|
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1292 |
"setprod (%x. f x * g x) A = (setprod f A * setprod g A)" |
15402 | 1293 |
by(simp add:setprod_def ACe.fold_distrib[OF ACe_mult]) |
1294 |
||
1295 |
||
1296 |
subsubsection {* Properties in more restricted classes of structures *} |
|
1297 |
||
1298 |
lemma setprod_eq_1_iff [simp]: |
|
1299 |
"finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))" |
|
1300 |
by (induct set: Finites) auto |
|
1301 |
||
1302 |
lemma setprod_zero: |
|
1303 |
"finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0" |
|
1304 |
apply (induct set: Finites, force, clarsimp) |
|
1305 |
apply (erule disjE, auto) |
|
1306 |
done |
|
1307 |
||
1308 |
lemma setprod_nonneg [rule_format]: |
|
1309 |
"(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A" |
|
1310 |
apply (case_tac "finite A") |
|
1311 |
apply (induct set: Finites, force, clarsimp) |
|
1312 |
apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force) |
|
1313 |
apply (rule mult_mono, assumption+) |
|
1314 |
apply (auto simp add: setprod_def) |
|
1315 |
done |
|
1316 |
||
1317 |
lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x) |
|
1318 |
--> 0 < setprod f A" |
|
1319 |
apply (case_tac "finite A") |
|
1320 |
apply (induct set: Finites, force, clarsimp) |
|
1321 |
apply (subgoal_tac "0 * 0 < f x * setprod f F", force) |
|
1322 |
apply (rule mult_strict_mono, assumption+) |
|
1323 |
apply (auto simp add: setprod_def) |
|
1324 |
done |
|
1325 |
||
1326 |
lemma setprod_nonzero [rule_format]: |
|
1327 |
"(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==> |
|
1328 |
finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0" |
|
1329 |
apply (erule finite_induct, auto) |
|
1330 |
done |
|
1331 |
||
1332 |
lemma setprod_zero_eq: |
|
1333 |
"(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==> |
|
1334 |
finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)" |
|
1335 |
apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast) |
|
1336 |
done |
|
1337 |
||
1338 |
lemma setprod_nonzero_field: |
|
1339 |
"finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0" |
|
1340 |
apply (rule setprod_nonzero, auto) |
|
1341 |
done |
|
1342 |
||
1343 |
lemma setprod_zero_eq_field: |
|
1344 |
"finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)" |
|
1345 |
apply (rule setprod_zero_eq, auto) |
|
1346 |
done |
|
1347 |
||
1348 |
lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==> |
|
1349 |
(setprod f (A Un B) :: 'a ::{field}) |
|
1350 |
= setprod f A * setprod f B / setprod f (A Int B)" |
|
1351 |
apply (subst setprod_Un_Int [symmetric], auto) |
|
1352 |
apply (subgoal_tac "finite (A Int B)") |
|
1353 |
apply (frule setprod_nonzero_field [of "A Int B" f], assumption) |
|
1354 |
apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self) |
|
1355 |
done |
|
1356 |
||
1357 |
lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==> |
|
1358 |
(setprod f (A - {a}) :: 'a :: {field}) = |
|
1359 |
(if a:A then setprod f A / f a else setprod f A)" |
|
1360 |
apply (erule finite_induct) |
|
1361 |
apply (auto simp add: insert_Diff_if) |
|
1362 |
apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a") |
|
1363 |
apply (erule ssubst) |
|
1364 |
apply (subst times_divide_eq_right [THEN sym]) |
|
1365 |
apply (auto simp add: mult_ac times_divide_eq_right divide_self) |
|
1366 |
done |
|
1367 |
||
1368 |
lemma setprod_inversef: "finite A ==> |
|
1369 |
ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==> |
|
1370 |
setprod (inverse \<circ> f) A = inverse (setprod f A)" |
|
1371 |
apply (erule finite_induct) |
|
1372 |
apply (simp, simp) |
|
1373 |
done |
|
1374 |
||
1375 |
lemma setprod_dividef: |
|
1376 |
"[|finite A; |
|
1377 |
\<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|] |
|
1378 |
==> setprod (%x. f x / g x) A = setprod f A / setprod g A" |
|
1379 |
apply (subgoal_tac |
|
1380 |
"setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A") |
|
1381 |
apply (erule ssubst) |
|
1382 |
apply (subst divide_inverse) |
|
1383 |
apply (subst setprod_timesf) |
|
1384 |
apply (subst setprod_inversef, assumption+, rule refl) |
|
1385 |
apply (rule setprod_cong, rule refl) |
|
1386 |
apply (subst divide_inverse, auto) |
|
1387 |
done |
|
1388 |
||
12396 | 1389 |
subsection {* Finite cardinality *} |
1390 |
||
15402 | 1391 |
text {* This definition, although traditional, is ugly to work with: |
1392 |
@{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}. |
|
1393 |
But now that we have @{text setsum} things are easy: |
|
12396 | 1394 |
*} |
1395 |
||
1396 |
constdefs |
|
1397 |
card :: "'a set => nat" |
|
15402 | 1398 |
"card A == setsum (%x. 1::nat) A" |
12396 | 1399 |
|
1400 |
lemma card_empty [simp]: "card {} = 0" |
|
15402 | 1401 |
by (simp add: card_def) |
1402 |
||
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1403 |
lemma card_infinite [simp]: "~ finite A ==> card A = 0" |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1404 |
by (simp add: card_def) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1405 |
|
15402 | 1406 |
lemma card_eq_setsum: "card A = setsum (%x. 1) A" |
1407 |
by (simp add: card_def) |
|
12396 | 1408 |
|
1409 |
lemma card_insert_disjoint [simp]: |
|
1410 |
"finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)" |
|
15402 | 1411 |
by(simp add: card_def ACf.fold_insert[OF ACf_add]) |
1412 |
||
1413 |
lemma card_insert_if: |
|
1414 |
"finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))" |
|
1415 |
by (simp add: insert_absorb) |
|
12396 | 1416 |
|
1417 |
lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})" |
|
1418 |
apply auto |
|
14208 | 1419 |
apply (drule_tac a = x in mk_disjoint_insert, clarify) |
15402 | 1420 |
apply (auto) |
12396 | 1421 |
done |
1422 |
||
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1423 |
lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)" |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1424 |
by auto |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1425 |
|
12396 | 1426 |
lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A" |
14302 | 1427 |
apply(rule_tac t = A in insert_Diff [THEN subst], assumption) |
1428 |
apply(simp del:insert_Diff_single) |
|
1429 |
done |
|
12396 | 1430 |
|
1431 |
lemma card_Diff_singleton: |
|
1432 |
"finite A ==> x: A ==> card (A - {x}) = card A - 1" |
|
1433 |
by (simp add: card_Suc_Diff1 [symmetric]) |
|
1434 |
||
1435 |
lemma card_Diff_singleton_if: |
|
1436 |
"finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)" |
|
1437 |
by (simp add: card_Diff_singleton) |
|
1438 |
||
1439 |
lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))" |
|
1440 |
by (simp add: card_insert_if card_Suc_Diff1) |
|
1441 |
||
1442 |
lemma card_insert_le: "finite A ==> card A <= card (insert x A)" |
|
1443 |
by (simp add: card_insert_if) |
|
1444 |
||
15402 | 1445 |
lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B" |
1446 |
by (simp add: card_def setsum_mono2_nat) |
|
1447 |
||
12396 | 1448 |
lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)" |
14208 | 1449 |
apply (induct set: Finites, simp, clarify) |
12396 | 1450 |
apply (subgoal_tac "finite A & A - {x} <= F") |
14208 | 1451 |
prefer 2 apply (blast intro: finite_subset, atomize) |
12396 | 1452 |
apply (drule_tac x = "A - {x}" in spec) |
1453 |
apply (simp add: card_Diff_singleton_if split add: split_if_asm) |
|
14208 | 1454 |
apply (case_tac "card A", auto) |
12396 | 1455 |
done |
1456 |
||
1457 |
lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B" |
|
1458 |
apply (simp add: psubset_def linorder_not_le [symmetric]) |
|
1459 |
apply (blast dest: card_seteq) |
|
1460 |
done |
|
1461 |
||
1462 |
lemma card_Un_Int: "finite A ==> finite B |
|
1463 |
==> card A + card B = card (A Un B) + card (A Int B)" |
|
15402 | 1464 |
by(simp add:card_def setsum_Un_Int) |
12396 | 1465 |
|
1466 |
lemma card_Un_disjoint: "finite A ==> finite B |
|
1467 |
==> A Int B = {} ==> card (A Un B) = card A + card B" |
|
1468 |
by (simp add: card_Un_Int) |
|
1469 |
||
1470 |
lemma card_Diff_subset: |
|
15402 | 1471 |
"finite B ==> B <= A ==> card (A - B) = card A - card B" |
1472 |
by(simp add:card_def setsum_diff_nat) |
|
12396 | 1473 |
|
1474 |
lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A" |
|
1475 |
apply (rule Suc_less_SucD) |
|
1476 |
apply (simp add: card_Suc_Diff1) |
|
1477 |
done |
|
1478 |
||
1479 |
lemma card_Diff2_less: |
|
1480 |
"finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A" |
|
1481 |
apply (case_tac "x = y") |
|
1482 |
apply (simp add: card_Diff1_less) |
|
1483 |
apply (rule less_trans) |
|
1484 |
prefer 2 apply (auto intro!: card_Diff1_less) |
|
1485 |
done |
|
1486 |
||
1487 |
lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A" |
|
1488 |
apply (case_tac "x : A") |
|
1489 |
apply (simp_all add: card_Diff1_less less_imp_le) |
|
1490 |
done |
|
1491 |
||
1492 |
lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B" |
|
14208 | 1493 |
by (erule psubsetI, blast) |
12396 | 1494 |
|
14889 | 1495 |
lemma insert_partition: |
15402 | 1496 |
"\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk> |
1497 |
\<Longrightarrow> x \<inter> \<Union> F = {}" |
|
14889 | 1498 |
by auto |
1499 |
||
1500 |
(* main cardinality theorem *) |
|
1501 |
lemma card_partition [rule_format]: |
|
1502 |
"finite C ==> |
|
1503 |
finite (\<Union> C) --> |
|
1504 |
(\<forall>c\<in>C. card c = k) --> |
|
1505 |
(\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) --> |
|
1506 |
k * card(C) = card (\<Union> C)" |
|
1507 |
apply (erule finite_induct, simp) |
|
1508 |
apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition |
|
1509 |
finite_subset [of _ "\<Union> (insert x F)"]) |
|
1510 |
done |
|
1511 |
||
12396 | 1512 |
|
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1513 |
lemma setsum_constant_nat: "(\<Sum>x\<in>A. y) = (card A) * y" |
15402 | 1514 |
-- {* Generalized to any @{text comm_semiring_1_cancel} in |
1515 |
@{text IntDef} as @{text setsum_constant}. *} |
|
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1516 |
apply (cases "finite A") |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1517 |
apply (erule finite_induct, auto) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1518 |
done |
15402 | 1519 |
|
1520 |
lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::recpower)) = y^(card A)" |
|
1521 |
apply (erule finite_induct) |
|
1522 |
apply (auto simp add: power_Suc) |
|
1523 |
done |
|
1524 |
||
1525 |
||
1526 |
subsubsection {* Cardinality of unions *} |
|
1527 |
||
1528 |
lemma card_UN_disjoint: |
|
1529 |
"finite I ==> (ALL i:I. finite (A i)) ==> |
|
1530 |
(ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==> |
|
1531 |
card (UNION I A) = (\<Sum>i\<in>I. card(A i))" |
|
1532 |
apply (simp add: card_def) |
|
1533 |
apply (subgoal_tac |
|
1534 |
"setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I") |
|
1535 |
apply (simp add: setsum_UN_disjoint) |
|
1536 |
apply (simp add: setsum_constant_nat cong: setsum_cong) |
|
1537 |
done |
|
1538 |
||
1539 |
lemma card_Union_disjoint: |
|
1540 |
"finite C ==> (ALL A:C. finite A) ==> |
|
1541 |
(ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==> |
|
1542 |
card (Union C) = setsum card C" |
|
1543 |
apply (frule card_UN_disjoint [of C id]) |
|
1544 |
apply (unfold Union_def id_def, assumption+) |
|
1545 |
done |
|
1546 |
||
12396 | 1547 |
subsubsection {* Cardinality of image *} |
1548 |
||
15447 | 1549 |
text{*The image of a finite set can be expressed using @{term fold}.*} |
1550 |
lemma image_eq_fold: "finite A ==> f ` A = fold (op Un) (%x. {f x}) {} A" |
|
1551 |
apply (erule finite_induct, simp) |
|
1552 |
apply (subst ACf.fold_insert) |
|
1553 |
apply (auto simp add: ACf_def) |
|
1554 |
done |
|
1555 |
||
12396 | 1556 |
lemma card_image_le: "finite A ==> card (f ` A) <= card A" |
14208 | 1557 |
apply (induct set: Finites, simp) |
12396 | 1558 |
apply (simp add: le_SucI finite_imageI card_insert_if) |
1559 |
done |
|
1560 |
||
15402 | 1561 |
lemma card_image: "inj_on f A ==> card (f ` A) = card A" |
1562 |
by(simp add:card_def setsum_reindex o_def) |
|
12396 | 1563 |
|
1564 |
lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A" |
|
1565 |
by (simp add: card_seteq card_image) |
|
1566 |
||
15111 | 1567 |
lemma eq_card_imp_inj_on: |
1568 |
"[| finite A; card(f ` A) = card A |] ==> inj_on f A" |
|
1569 |
apply(induct rule:finite_induct) |
|
1570 |
apply simp |
|
1571 |
apply(frule card_image_le[where f = f]) |
|
1572 |
apply(simp add:card_insert_if split:if_splits) |
|
1573 |
done |
|
1574 |
||
1575 |
lemma inj_on_iff_eq_card: |
|
1576 |
"finite A ==> inj_on f A = (card(f ` A) = card A)" |
|
1577 |
by(blast intro: card_image eq_card_imp_inj_on) |
|
1578 |
||
12396 | 1579 |
|
15402 | 1580 |
lemma card_inj_on_le: |
1581 |
"[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B" |
|
1582 |
apply (subgoal_tac "finite A") |
|
1583 |
apply (force intro: card_mono simp add: card_image [symmetric]) |
|
1584 |
apply (blast intro: finite_imageD dest: finite_subset) |
|
1585 |
done |
|
1586 |
||
1587 |
lemma card_bij_eq: |
|
1588 |
"[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A; |
|
1589 |
finite A; finite B |] ==> card A = card B" |
|
1590 |
by (auto intro: le_anti_sym card_inj_on_le) |
|
1591 |
||
1592 |
||
1593 |
subsubsection {* Cardinality of products *} |
|
1594 |
||
1595 |
(* |
|
1596 |
lemma SigmaI_insert: "y \<notin> A ==> |
|
1597 |
(SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))" |
|
1598 |
by auto |
|
1599 |
*) |
|
1600 |
||
1601 |
lemma card_SigmaI [simp]: |
|
1602 |
"\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk> |
|
1603 |
\<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))" |
|
1604 |
by(simp add:card_def setsum_Sigma) |
|
1605 |
||
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1606 |
lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)" |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1607 |
apply (cases "finite A") |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1608 |
apply (cases "finite B") |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1609 |
apply (simp add: setsum_constant_nat) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1610 |
apply (auto simp add: card_eq_0_iff |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1611 |
dest: finite_cartesian_productD1 finite_cartesian_productD2) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1612 |
done |
15402 | 1613 |
|
1614 |
lemma card_cartesian_product_singleton: "card({x} <*> A) = card(A)" |
|
15409
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1615 |
by (simp add: card_cartesian_product) |
a063687d24eb
new and stronger lemmas and improved simplification for finite sets
paulson
parents:
15402
diff
changeset
|
1616 |
|
15402 | 1617 |
|
1618 |
||
12396 | 1619 |
subsubsection {* Cardinality of the Powerset *} |
1620 |
||
1621 |
lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A" (* FIXME numeral 2 (!?) *) |
|
1622 |
apply (induct set: Finites) |
|
1623 |
apply (simp_all add: Pow_insert) |
|
14208 | 1624 |
apply (subst card_Un_disjoint, blast) |
1625 |
apply (blast intro: finite_imageI, blast) |
|
12396 | 1626 |
apply (subgoal_tac "inj_on (insert x) (Pow F)") |
1627 |
apply (simp add: card_image Pow_insert) |
|
1628 |
apply (unfold inj_on_def) |
|
1629 |
apply (blast elim!: equalityE) |
|
1630 |
done |
|
1631 |
||
15392 | 1632 |
text {* Relates to equivalence classes. Based on a theorem of |
1633 |
F. Kammüller's. *} |
|
12396 | 1634 |
|
1635 |
lemma dvd_partition: |
|
15392 | 1636 |
"finite (Union C) ==> |
12396 | 1637 |
ALL c : C. k dvd card c ==> |
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14331
diff
changeset
|
1638 |
(ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==> |
12396 | 1639 |
k dvd card (Union C)" |
15392 | 1640 |
apply(frule finite_UnionD) |
1641 |
apply(rotate_tac -1) |
|
14208 | 1642 |
apply (induct set: Finites, simp_all, clarify) |
12396 | 1643 |
apply (subst card_Un_disjoint) |
1644 |
apply (auto simp add: dvd_add disjoint_eq_subset_Compl) |
|
1645 |
done |
|
1646 |
||
1647 |
||
15392 | 1648 |
subsubsection {* Theorems about @{text "choose"} *} |
12396 | 1649 |
|
1650 |
text {* |
|
15392 | 1651 |
\medskip Basic theorem about @{text "choose"}. By Florian |
1652 |
Kamm\"uller, tidied by LCP. |
|
12396 | 1653 |
*} |
1654 |
||
15392 | 1655 |
lemma card_s_0_eq_empty: |
1656 |
"finite A ==> card {B. B \<subseteq> A & card B = 0} = 1" |
|
1657 |
apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq]) |
|
1658 |
apply (simp cong add: rev_conj_cong) |
|
1659 |
done |
|
12396 | 1660 |
|
15392 | 1661 |
lemma choose_deconstruct: "finite M ==> x \<notin> M |
1662 |
==> {s. s <= insert x M & card(s) = Suc k} |
|
1663 |
= {s. s <= M & card(s) = Suc k} Un |
|
1664 |
{s. EX t. t <= M & card(t) = k & s = insert x t}" |
|
1665 |
apply safe |
|
1666 |
apply (auto intro: finite_subset [THEN card_insert_disjoint]) |
|
1667 |
apply (drule_tac x = "xa - {x}" in spec) |
|
1668 |
apply (subgoal_tac "x \<notin> xa", auto) |
|
1669 |
apply (erule rev_mp, subst card_Diff_singleton) |
|
1670 |
apply (auto intro: finite_subset) |
|
12396 | 1671 |
done |
1672 |
||
15392 | 1673 |
text{*There are as many subsets of @{term A} having cardinality @{term k} |
1674 |
as there are sets obtained from the former by inserting a fixed element |
|
1675 |
@{term x} into each.*} |
|
1676 |
lemma constr_bij: |
|
1677 |
"[|finite A; x \<notin> A|] ==> |
|
1678 |
card {B. EX C. C <= A & card(C) = k & B = insert x C} = |
|
1679 |
card {B. B <= A & card(B) = k}" |
|
1680 |
apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq) |
|
1681 |
apply (auto elim!: equalityE simp add: inj_on_def) |
|
1682 |
apply (subst Diff_insert0, auto) |
|
1683 |
txt {* finiteness of the two sets *} |
|
1684 |
apply (rule_tac [2] B = "Pow (A)" in finite_subset) |
|
1685 |
apply (rule_tac B = "Pow (insert x A)" in finite_subset) |
|
1686 |
apply fast+ |
|
12396 | 1687 |
done |
1688 |
||
15392 | 1689 |
text {* |
1690 |
Main theorem: combinatorial statement about number of subsets of a set. |
|
1691 |
*} |
|
12396 | 1692 |
|
15392 | 1693 |
lemma n_sub_lemma: |
1694 |
"!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)" |
|
1695 |
apply (induct k) |
|
1696 |
apply (simp add: card_s_0_eq_empty, atomize) |
|
1697 |
apply (rotate_tac -1, erule finite_induct) |
|
1698 |
apply (simp_all (no_asm_simp) cong add: conj_cong |
|
1699 |
add: card_s_0_eq_empty choose_deconstruct) |
|
1700 |
apply (subst card_Un_disjoint) |
|
1701 |
prefer 4 apply (force simp add: constr_bij) |
|
1702 |
prefer 3 apply force |
|
1703 |
prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2] |
|
1704 |
finite_subset [of _ "Pow (insert x F)", standard]) |
|
1705 |
apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset]) |
|
12396 | 1706 |
done |
1707 |
||
15392 | 1708 |
theorem n_subsets: |
1709 |
"finite A ==> card {B. B <= A & card B = k} = (card A choose k)" |
|
1710 |
by (simp add: n_sub_lemma) |
|
1711 |
||
1712 |
||
1713 |
subsection{* A fold functional for non-empty sets *} |
|
1714 |
||
1715 |
text{* Does not require start value. *} |
|
12396 | 1716 |
|
15392 | 1717 |
consts |
1718 |
foldSet1 :: "('a => 'a => 'a) => ('a set \<times> 'a) set" |
|
1719 |
||
1720 |
inductive "foldSet1 f" |
|
1721 |
intros |
|
1722 |
foldSet1_singletonI [intro]: "({a}, a) : foldSet1 f" |
|
1723 |
foldSet1_insertI [intro]: |
|
1724 |
"\<lbrakk> (A, x) : foldSet1 f; a \<notin> A; A \<noteq> {} \<rbrakk> |
|
1725 |
\<Longrightarrow> (insert a A, f a x) : foldSet1 f" |
|
12396 | 1726 |
|
15392 | 1727 |
constdefs |
1728 |
fold1 :: "('a => 'a => 'a) => 'a set => 'a" |
|
1729 |
"fold1 f A == THE x. (A, x) : foldSet1 f" |
|
1730 |
||
1731 |
lemma foldSet1_nonempty: |
|
1732 |
"(A, x) : foldSet1 f \<Longrightarrow> A \<noteq> {}" |
|
1733 |
by(erule foldSet1.cases, simp_all) |
|
1734 |
||
12396 | 1735 |
|
15392 | 1736 |
inductive_cases empty_foldSet1E [elim!]: "({}, x) : foldSet1 f" |
1737 |
||
1738 |
lemma foldSet1_sing[iff]: "(({a},b) : foldSet1 f) = (a = b)" |
|
1739 |
apply(rule iffI) |
|
1740 |
prefer 2 apply fast |
|
1741 |
apply (erule foldSet1.cases) |
|
1742 |
apply blast |
|
1743 |
apply (erule foldSet1.cases) |
|
1744 |
apply blast |
|
1745 |
apply blast |
|
15376 | 1746 |
done |
12396 | 1747 |
|
15392 | 1748 |
lemma Diff1_foldSet1: |
1749 |
"(A - {x}, y) : foldSet1 f ==> x: A ==> (A, f x y) : foldSet1 f" |
|
1750 |
by (erule insert_Diff [THEN subst], rule foldSet1.intros, |
|
1751 |
auto dest!:foldSet1_nonempty) |
|
12396 | 1752 |
|
15392 | 1753 |
lemma foldSet1_imp_finite: "(A, x) : foldSet1 f ==> finite A" |
1754 |
by (induct set: foldSet1) auto |
|
12396 | 1755 |
|
15392 | 1756 |
lemma finite_nonempty_imp_foldSet1: |
1757 |
"\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : foldSet1 f" |
|
1758 |
by (induct set: Finites) auto |
|
15376 | 1759 |
|
15392 | 1760 |
lemma (in ACf) foldSet1_determ_aux: |
1761 |
"!!A x y. \<lbrakk> card A < n; (A, x) : foldSet1 f; (A, y) : foldSet1 f \<rbrakk> \<Longrightarrow> y = x" |
|
1762 |
proof (induct n) |
|
1763 |
case 0 thus ?case by simp |
|
1764 |
next |
|
1765 |
case (Suc n) |
|
1766 |
have IH: "!!A x y. \<lbrakk>card A < n; (A, x) \<in> foldSet1 f; (A, y) \<in> foldSet1 f\<rbrakk> |
|
1767 |
\<Longrightarrow> y = x" and card: "card A < Suc n" |
|
1768 |
and Afoldx: "(A, x) \<in> foldSet1 f" and Afoldy: "(A, y) \<in> foldSet1 f" . |
|
1769 |
from card have "card A < n \<or> card A = n" by arith |
|
1770 |
thus ?case |
|
1771 |
proof |
|
1772 |
assume less: "card A < n" |
|
1773 |
show ?thesis by(rule IH[OF less Afoldx Afoldy]) |
|
1774 |
next |
|
1775 |
assume cardA: "card A = n" |
|
1776 |
show ?thesis |
|
1777 |
proof (rule foldSet1.cases[OF Afoldx]) |
|
1778 |
fix a assume "(A, x) = ({a}, a)" |
|
1779 |
thus "y = x" using Afoldy by (simp add:foldSet1_sing) |
|
1780 |
next |
|
1781 |
fix Ax ax x' |
|
1782 |
assume eq1: "(A, x) = (insert ax Ax, ax \<cdot> x')" |
|
1783 |
and x': "(Ax, x') \<in> foldSet1 f" and notinx: "ax \<notin> Ax" |
|
1784 |
and Axnon: "Ax \<noteq> {}" |
|
1785 |
hence A1: "A = insert ax Ax" and x: "x = ax \<cdot> x'" by auto |
|
1786 |
show ?thesis |
|
1787 |
proof (rule foldSet1.cases[OF Afoldy]) |
|
1788 |
fix ay assume "(A, y) = ({ay}, ay)" |
|
1789 |
thus ?thesis using eq1 x' Axnon notinx |
|
1790 |
by (fastsimp simp:foldSet1_sing) |
|
1791 |
next |
|
1792 |
fix Ay ay y' |
|
1793 |
assume eq2: "(A, y) = (insert ay Ay, ay \<cdot> y')" |
|
1794 |
and y': "(Ay, y') \<in> foldSet1 f" and notiny: "ay \<notin> Ay" |
|
1795 |
and Aynon: "Ay \<noteq> {}" |
|
1796 |
hence A2: "A = insert ay Ay" and y: "y = ay \<cdot> y'" by auto |
|
1797 |
have finA: "finite A" by(rule foldSet1_imp_finite[OF Afoldx]) |
|
1798 |
with cardA A1 notinx have less: "card Ax < n" by simp |
|
1799 |
show ?thesis |
|
1800 |
proof cases |
|
1801 |
assume "ax = ay" |
|
1802 |
then moreover have "Ax = Ay" using A1 A2 notinx notiny by auto |
|
1803 |
ultimately show ?thesis using IH[OF less x'] y' eq1 eq2 by auto |
|
1804 |
next |
|
1805 |
assume diff: "ax \<noteq> ay" |
|
1806 |
let ?B = "Ax - {ay}" |
|
1807 |
have Ax: "Ax = insert ay ?B" and Ay: "Ay = insert ax ?B" |
|
1808 |
using A1 A2 notinx notiny diff by(blast elim!:equalityE)+ |
|
1809 |
show ?thesis |
|
1810 |
proof cases |
|
1811 |
assume "?B = {}" |
|
1812 |
with Ax Ay show ?thesis using x' y' x y by(simp add:commute) |
|
1813 |
next |
|
1814 |
assume Bnon: "?B \<noteq> {}" |
|
1815 |
moreover have "finite ?B" using finA A1 by simp |
|
1816 |
ultimately obtain b where Bfoldb: "(?B,b) \<in> foldSet1 f" |
|
1817 |
using finite_nonempty_imp_foldSet1 by(blast) |
|
1818 |
moreover have ayinAx: "ay \<in> Ax" using Ax by(auto) |
|
1819 |
ultimately have "(Ax,ay\<cdot>b) \<in> foldSet1 f" by(rule Diff1_foldSet1) |
|
1820 |
hence "ay\<cdot>b = x'" by(rule IH[OF less x']) |
|
1821 |
moreover have "ax\<cdot>b = y'" |
|
1822 |
proof (rule IH[OF _ y']) |
|
1823 |
show "card Ay < n" using Ay cardA A1 notinx finA ayinAx |
|
1824 |
by(auto simp:card_Diff1_less) |
|
1825 |
next |
|
1826 |
show "(Ay,ax\<cdot>b) \<in> foldSet1 f" using Ay notinx Bfoldb Bnon |
|
1827 |
by fastsimp |
|
1828 |
qed |
|
1829 |
ultimately show ?thesis using x y by(auto simp:AC) |
|
1830 |
qed |
|
1831 |
qed |
|
1832 |
qed |
|
1833 |
qed |
|
1834 |
qed |
|
12396 | 1835 |
qed |
1836 |
||
15392 | 1837 |
|
1838 |
lemma (in ACf) foldSet1_determ: |
|
1839 |
"(A, x) : foldSet1 f ==> (A, y) : foldSet1 f ==> y = x" |
|
1840 |
by (blast intro: foldSet1_determ_aux [rule_format]) |
|
1841 |
||
1842 |
lemma (in ACf) foldSet1_equality: "(A, y) : foldSet1 f ==> fold1 f A = y" |
|
1843 |
by (unfold fold1_def) (blast intro: foldSet1_determ) |
|
1844 |
||
1845 |
lemma fold1_singleton: "fold1 f {a} = a" |
|
1846 |
by (unfold fold1_def) blast |
|
12396 | 1847 |
|
15392 | 1848 |
lemma (in ACf) foldSet1_insert_aux: "x \<notin> A ==> A \<noteq> {} \<Longrightarrow> |
1849 |
((insert x A, v) : foldSet1 f) = |
|
1850 |
(EX y. (A, y) : foldSet1 f & v = f x y)" |
|
1851 |
apply auto |
|
1852 |
apply (rule_tac A1 = A and f1 = f in finite_nonempty_imp_foldSet1 [THEN exE]) |
|
1853 |
apply (fastsimp dest: foldSet1_imp_finite) |
|
1854 |
apply blast |
|
1855 |
apply (blast intro: foldSet1_determ) |
|
1856 |
done |
|
15376 | 1857 |
|
15392 | 1858 |
lemma (in ACf) fold1_insert: |
1859 |
"finite A ==> x \<notin> A ==> A \<noteq> {} \<Longrightarrow> fold1 f (insert x A) = f x (fold1 f A)" |
|
1860 |
apply (unfold fold1_def) |
|
1861 |
apply (simp add: foldSet1_insert_aux) |
|
1862 |
apply (rule the_equality) |
|
1863 |
apply (auto intro: finite_nonempty_imp_foldSet1 |
|
1864 |
cong add: conj_cong simp add: fold1_def [symmetric] foldSet1_equality) |
|
1865 |
done |
|
15376 | 1866 |
|
15392 | 1867 |
locale ACIf = ACf + |
1868 |
assumes idem: "x \<cdot> x = x" |
|
12396 | 1869 |
|
15392 | 1870 |
lemma (in ACIf) fold1_insert2: |
1871 |
assumes finA: "finite A" and nonA: "A \<noteq> {}" |
|
1872 |
shows "fold1 f (insert a A) = f a (fold1 f A)" |
|
1873 |
proof cases |
|
1874 |
assume "a \<in> A" |
|
1875 |
then obtain B where A: "A = insert a B" and disj: "a \<notin> B" |
|
1876 |
by(blast dest: mk_disjoint_insert) |
|
1877 |
show ?thesis |
|
1878 |
proof cases |
|
1879 |
assume "B = {}" |
|
1880 |
thus ?thesis using A by(simp add:idem fold1_singleton) |
|
1881 |
next |
|
1882 |
assume nonB: "B \<noteq> {}" |
|
1883 |
from finA A have finB: "finite B" by(blast intro: finite_subset) |
|
1884 |
have "fold1 f (insert a A) = fold1 f (insert a B)" using A by simp |
|
1885 |
also have "\<dots> = f a (fold1 f B)" |
|
1886 |
using finB nonB disj by(simp add: fold1_insert) |
|
1887 |
also have "\<dots> = f a (fold1 f A)" |
|
1888 |
using A finB nonB disj by(simp add:idem fold1_insert assoc[symmetric]) |
|
1889 |
finally show ?thesis . |
|
1890 |
qed |
|
1891 |
next |
|
1892 |
assume "a \<notin> A" |
|
1893 |
with finA nonA show ?thesis by(simp add:fold1_insert) |
|
1894 |
qed |
|
1895 |
||
15376 | 1896 |
|
15392 | 1897 |
text{* Now the recursion rules for definitions: *} |
1898 |
||
1899 |
lemma fold1_singleton_def: "g \<equiv> fold1 f \<Longrightarrow> g {a} = a" |
|
1900 |
by(simp add:fold1_singleton) |
|
1901 |
||
1902 |
lemma (in ACf) fold1_insert_def: |
|
1903 |
"\<lbrakk> g \<equiv> fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)" |
|
1904 |
by(simp add:fold1_insert) |
|
1905 |
||
1906 |
lemma (in ACIf) fold1_insert2_def: |
|
1907 |
"\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)" |
|
1908 |
by(simp add:fold1_insert2) |
|
1909 |
||
15376 | 1910 |
|
15392 | 1911 |
subsection{*Min and Max*} |
1912 |
||
1913 |
text{* As an application of @{text fold1} we define the minimal and |
|
1914 |
maximal element of a (non-empty) set over a linear order. First we |
|
1915 |
show that @{text min} and @{text max} are ACI: *} |
|
1916 |
||
1917 |
lemma ACf_min: "ACf(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)" |
|
1918 |
apply(rule ACf.intro) |
|
1919 |
apply(auto simp:min_def) |
|
1920 |
done |
|
1921 |
||
1922 |
lemma ACIf_min: "ACIf(min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)" |
|
1923 |
apply(rule ACIf.intro[OF ACf_min]) |
|
1924 |
apply(rule ACIf_axioms.intro) |
|
1925 |
apply(auto simp:min_def) |
|
15376 | 1926 |
done |
1927 |
||
15392 | 1928 |
lemma ACf_max: "ACf(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)" |
1929 |
apply(rule ACf.intro) |
|
1930 |
apply(auto simp:max_def) |
|
1931 |
done |
|
1932 |
||
1933 |
lemma ACIf_max: "ACIf(max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)" |
|
1934 |
apply(rule ACIf.intro[OF ACf_max]) |
|
1935 |
apply(rule ACIf_axioms.intro) |
|
1936 |
apply(auto simp:max_def) |
|
15376 | 1937 |
done |
12396 | 1938 |
|
15392 | 1939 |
text{* Now we make the definitions: *} |
1940 |
||
1941 |
constdefs |
|
1942 |
Min :: "('a::linorder)set => 'a" |
|
1943 |
"Min == fold1 min" |
|
1944 |
||
1945 |
Max :: "('a::linorder)set => 'a" |
|
1946 |
"Max == fold1 max" |
|
1947 |
||
15402 | 1948 |
text{* Now we instantiate the recursion equations and declare them |
15392 | 1949 |
simplification rules: *} |
1950 |
||
1951 |
declare |
|
1952 |
fold1_singleton_def[OF Min_def, simp] |
|
1953 |
ACIf.fold1_insert2_def[OF ACIf_min Min_def, simp] |
|
1954 |
fold1_singleton_def[OF Max_def, simp] |
|
1955 |
ACIf.fold1_insert2_def[OF ACIf_max Max_def, simp] |
|
1956 |
||
1957 |
text{* Now we prove some properties by induction: *} |
|
1958 |
||
1959 |
lemma Min_in [simp]: |
|
1960 |
assumes a: "finite S" |
|
1961 |
shows "S \<noteq> {} \<Longrightarrow> Min S \<in> S" |
|
1962 |
using a |
|
1963 |
proof induct |
|
1964 |
case empty thus ?case by simp |
|
1965 |
next |
|
1966 |
case (insert x S) |
|
1967 |
show ?case |
|
1968 |
proof cases |
|
1969 |
assume "S = {}" thus ?thesis by simp |
|
1970 |
next |
|
1971 |
assume "S \<noteq> {}" thus ?thesis using insert by (simp add:min_def) |
|
1972 |
qed |
|
1973 |
qed |
|
1974 |
||
1975 |
lemma Min_le [simp]: |
|
1976 |
assumes a: "finite S" |
|
1977 |
shows "\<lbrakk> S \<noteq> {}; x \<in> S \<rbrakk> \<Longrightarrow> Min S \<le> x" |
|
1978 |
using a |
|
1979 |
proof induct |
|
1980 |
case empty thus ?case by simp |
|
1981 |
next |
|
1982 |
case (insert y S) |
|
1983 |
show ?case |
|
1984 |
proof cases |
|
1985 |
assume "S = {}" thus ?thesis using insert by simp |
|
1986 |
next |
|
1987 |
assume "S \<noteq> {}" thus ?thesis using insert by (auto simp add:min_def) |
|
1988 |
qed |
|
1989 |
qed |
|
1990 |
||
1991 |
lemma Max_in [simp]: |
|
1992 |
assumes a: "finite S" |
|
1993 |
shows "S \<noteq> {} \<Longrightarrow> Max S \<in> S" |
|
1994 |
using a |
|
1995 |
proof induct |
|
1996 |
case empty thus ?case by simp |
|
1997 |
next |
|
1998 |
case (insert x S) |
|
1999 |
show ?case |
|
2000 |
proof cases |
|
2001 |
assume "S = {}" thus ?thesis by simp |
|
2002 |
next |
|
2003 |
assume "S \<noteq> {}" thus ?thesis using insert by (simp add:max_def) |
|
2004 |
qed |
|
2005 |
qed |
|
2006 |
||
2007 |
lemma Max_le [simp]: |
|
2008 |
assumes a: "finite S" |
|
2009 |
shows "\<lbrakk> S \<noteq> {}; x \<in> S \<rbrakk> \<Longrightarrow> x \<le> Max S" |
|
2010 |
using a |
|
2011 |
proof induct |
|
2012 |
case empty thus ?case by simp |
|
2013 |
next |
|
2014 |
case (insert y S) |
|
2015 |
show ?case |
|
2016 |
proof cases |
|
2017 |
assume "S = {}" thus ?thesis using insert by simp |
|
2018 |
next |
|
2019 |
assume "S \<noteq> {}" thus ?thesis using insert by (auto simp add:max_def) |
|
2020 |
qed |
|
2021 |
qed |
|
2022 |
||
12396 | 2023 |
|
15042 | 2024 |
end |