|
1 (* Title: Summation Operator for Abelian Groups |
|
2 ID: $Id$ |
|
3 Author: Clemens Ballarin, started 19 November 2002 |
|
4 |
|
5 This file is largely based on HOL/Finite_Set.thy. |
|
6 *) |
|
7 |
|
8 header {* Summation Operator *} |
|
9 |
|
10 theory FoldSet = Main: |
|
11 |
|
12 (* Instantiation of LC from Finite_Set.thy is not possible, |
|
13 because here we have explicit typing rules like x : carrier G. |
|
14 We introduce an explicit argument for the domain D *) |
|
15 |
|
16 consts |
|
17 foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set" |
|
18 |
|
19 inductive "foldSetD D f e" |
|
20 intros |
|
21 emptyI [intro]: "e : D ==> ({}, e) : foldSetD D f e" |
|
22 insertI [intro]: "[| x ~: A; f x y : D; (A, y) : foldSetD D f e |] ==> |
|
23 (insert x A, f x y) : foldSetD D f e" |
|
24 |
|
25 inductive_cases empty_foldSetDE [elim!]: "({}, x) : foldSetD D f e" |
|
26 |
|
27 constdefs |
|
28 foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a" |
|
29 "foldD D f e A == THE x. (A, x) : foldSetD D f e" |
|
30 |
|
31 lemma foldSetD_closed: |
|
32 "[| (A, z) : foldSetD D f e ; e : D; !!x y. [| x : A; y : D |] ==> f x y : D |
|
33 |] ==> z : D"; |
|
34 by (erule foldSetD.elims) auto |
|
35 |
|
36 lemma Diff1_foldSetD: |
|
37 "[| (A - {x}, y) : foldSetD D f e; x : A; f x y : D |] ==> |
|
38 (A, f x y) : foldSetD D f e" |
|
39 apply (erule insert_Diff [THEN subst], rule foldSetD.intros) |
|
40 apply auto |
|
41 done |
|
42 |
|
43 lemma foldSetD_imp_finite [simp]: "(A, x) : foldSetD D f e ==> finite A" |
|
44 by (induct set: foldSetD) auto |
|
45 |
|
46 lemma finite_imp_foldSetD: |
|
47 "[| finite A; e : D; !!x y. [| x : A; y : D |] ==> f x y : D |] ==> |
|
48 EX x. (A, x) : foldSetD D f e" |
|
49 proof (induct set: Finites) |
|
50 case empty then show ?case by auto |
|
51 next |
|
52 case (insert F x) |
|
53 then obtain y where y: "(F, y) : foldSetD D f e" by auto |
|
54 with insert have "y : D" by (auto dest: foldSetD_closed) |
|
55 with y and insert have "(insert x F, f x y) : foldSetD D f e" |
|
56 by (intro foldSetD.intros) auto |
|
57 then show ?case .. |
|
58 qed |
|
59 |
|
60 subsection {* Left-commutative operations *} |
|
61 |
|
62 locale LCD = |
|
63 fixes B :: "'b set" |
|
64 and D :: "'a set" |
|
65 and f :: "'b => 'a => 'a" (infixl "\<cdot>" 70) |
|
66 assumes left_commute: "[| x : B; y : B; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" |
|
67 and f_closed [simp, intro!]: "!!x y. [| x : B; y : D |] ==> f x y : D" |
|
68 |
|
69 lemma (in LCD) foldSetD_closed [dest]: |
|
70 "(A, z) : foldSetD D f e ==> z : D"; |
|
71 by (erule foldSetD.elims) auto |
|
72 |
|
73 lemma (in LCD) Diff1_foldSetD: |
|
74 "[| (A - {x}, y) : foldSetD D f e; x : A; A <= B |] ==> |
|
75 (A, f x y) : foldSetD D f e" |
|
76 apply (subgoal_tac "x : B") |
|
77 prefer 2 apply fast |
|
78 apply (erule insert_Diff [THEN subst], rule foldSetD.intros) |
|
79 apply auto |
|
80 done |
|
81 |
|
82 lemma (in LCD) foldSetD_imp_finite [simp]: |
|
83 "(A, x) : foldSetD D f e ==> finite A" |
|
84 by (induct set: foldSetD) auto |
|
85 |
|
86 lemma (in LCD) finite_imp_foldSetD: |
|
87 "[| finite A; A <= B; e : D |] ==> EX x. (A, x) : foldSetD D f e" |
|
88 proof (induct set: Finites) |
|
89 case empty then show ?case by auto |
|
90 next |
|
91 case (insert F x) |
|
92 then obtain y where y: "(F, y) : foldSetD D f e" by auto |
|
93 with insert have "y : D" by auto |
|
94 with y and insert have "(insert x F, f x y) : foldSetD D f e" |
|
95 by (intro foldSetD.intros) auto |
|
96 then show ?case .. |
|
97 qed |
|
98 |
|
99 lemma (in LCD) foldSetD_determ_aux: |
|
100 "e : D ==> ALL A x. A <= B & card A < n --> (A, x) : foldSetD D f e --> |
|
101 (ALL y. (A, y) : foldSetD D f e --> y = x)" |
|
102 apply (induct n) |
|
103 apply (auto simp add: less_Suc_eq) |
|
104 apply (erule foldSetD.cases) |
|
105 apply blast |
|
106 apply (erule foldSetD.cases) |
|
107 apply blast |
|
108 apply clarify |
|
109 txt {* force simplification of @{text "card A < card (insert ...)"}. *} |
|
110 apply (erule rev_mp) |
|
111 apply (simp add: less_Suc_eq_le) |
|
112 apply (rule impI) |
|
113 apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb") |
|
114 apply (subgoal_tac "Aa = Ab") |
|
115 prefer 2 apply (blast elim!: equalityE) |
|
116 apply blast |
|
117 txt {* case @{prop "xa \<notin> xb"}. *} |
|
118 apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab") |
|
119 prefer 2 apply (blast elim!: equalityE) |
|
120 apply clarify |
|
121 apply (subgoal_tac "Aa = insert xb Ab - {xa}") |
|
122 prefer 2 apply blast |
|
123 apply (subgoal_tac "card Aa <= card Ab") |
|
124 prefer 2 |
|
125 apply (rule Suc_le_mono [THEN subst]) |
|
126 apply (simp add: card_Suc_Diff1) |
|
127 apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE]) |
|
128 apply (blast intro: foldSetD_imp_finite finite_Diff) |
|
129 (* new subgoal from finite_imp_foldSetD *) |
|
130 apply best (* blast doesn't seem to solve this *) |
|
131 apply assumption |
|
132 apply (frule (1) Diff1_foldSetD) |
|
133 (* new subgoal from Diff1_foldSetD *) |
|
134 apply best |
|
135 (* |
|
136 apply (best del: foldSetD_closed elim: foldSetD_closed) |
|
137 apply (rule f_closed) apply assumption apply (rule foldSetD_closed) |
|
138 prefer 3 apply assumption apply (rule e_closed) |
|
139 apply (rule f_closed) apply force apply assumption |
|
140 *) |
|
141 apply (subgoal_tac "ya = f xb x") |
|
142 prefer 2 |
|
143 (* new subgoal to make IH applicable *) |
|
144 apply (subgoal_tac "Aa <= B") |
|
145 prefer 2 apply best |
|
146 apply (blast del: equalityCE) |
|
147 apply (subgoal_tac "(Ab - {xa}, x) : foldSetD D f e") |
|
148 prefer 2 apply simp |
|
149 apply (subgoal_tac "yb = f xa x") |
|
150 prefer 2 |
|
151 (* apply (drule_tac x = xa in Diff1_foldSetD) |
|
152 apply assumption |
|
153 apply (rule f_closed) apply best apply (rule foldSetD_closed) |
|
154 prefer 3 apply assumption apply (rule e_closed) |
|
155 apply (rule f_closed) apply best apply assumption |
|
156 *) |
|
157 apply (blast del: equalityCE dest: Diff1_foldSetD) |
|
158 apply (simp (no_asm_simp)) |
|
159 apply (rule left_commute) |
|
160 apply assumption apply best apply best |
|
161 done |
|
162 |
|
163 lemma (in LCD) foldSetD_determ: |
|
164 "[| (A, x) : foldSetD D f e; (A, y) : foldSetD D f e; e : D; A <= B |] |
|
165 ==> y = x" |
|
166 by (blast intro: foldSetD_determ_aux [rule_format]) |
|
167 |
|
168 lemma (in LCD) foldD_equality: |
|
169 "[| (A, y) : foldSetD D f e; e : D; A <= B |] ==> foldD D f e A = y" |
|
170 by (unfold foldD_def) (blast intro: foldSetD_determ) |
|
171 |
|
172 lemma foldD_empty [simp]: |
|
173 "e : D ==> foldD D f e {} = e" |
|
174 by (unfold foldD_def) blast |
|
175 |
|
176 lemma (in LCD) foldD_insert_aux: |
|
177 "[| x ~: A; x : B; e : D; A <= B |] ==> |
|
178 ((insert x A, v) : foldSetD D f e) = |
|
179 (EX y. (A, y) : foldSetD D f e & v = f x y)" |
|
180 apply auto |
|
181 apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE]) |
|
182 apply (fastsimp dest: foldSetD_imp_finite) |
|
183 (* new subgoal by finite_imp_foldSetD *) |
|
184 apply assumption |
|
185 apply assumption |
|
186 apply (blast intro: foldSetD_determ) |
|
187 done |
|
188 |
|
189 lemma (in LCD) foldD_insert: |
|
190 "[| finite A; x ~: A; x : B; e : D; A <= B |] ==> |
|
191 foldD D f e (insert x A) = f x (foldD D f e A)" |
|
192 apply (unfold foldD_def) |
|
193 apply (simp add: foldD_insert_aux) |
|
194 apply (rule the_equality) |
|
195 apply (auto intro: finite_imp_foldSetD |
|
196 cong add: conj_cong simp add: foldD_def [symmetric] foldD_equality) |
|
197 done |
|
198 |
|
199 lemma (in LCD) foldD_closed [simp]: |
|
200 "[| finite A; e : D; A <= B |] ==> foldD D f e A : D" |
|
201 proof (induct set: Finites) |
|
202 case empty then show ?case by (simp add: foldD_empty) |
|
203 next |
|
204 case insert then show ?case by (simp add: foldD_insert) |
|
205 qed |
|
206 |
|
207 lemma (in LCD) foldD_commute: |
|
208 "[| finite A; x : B; e : D; A <= B |] ==> |
|
209 f x (foldD D f e A) = foldD D f (f x e) A" |
|
210 apply (induct set: Finites) |
|
211 apply simp |
|
212 apply (auto simp add: left_commute foldD_insert) |
|
213 done |
|
214 |
|
215 lemma Int_mono2: |
|
216 "[| A <= C; B <= C |] ==> A Int B <= C" |
|
217 by blast |
|
218 |
|
219 lemma (in LCD) foldD_nest_Un_Int: |
|
220 "[| finite A; finite C; e : D; A <= B; C <= B |] ==> |
|
221 foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)" |
|
222 apply (induct set: Finites) |
|
223 apply simp |
|
224 apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb |
|
225 Int_mono2 Un_subset_iff) |
|
226 done |
|
227 |
|
228 lemma (in LCD) foldD_nest_Un_disjoint: |
|
229 "[| finite A; finite B; A Int B = {}; e : D; A <= B; C <= B |] |
|
230 ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A" |
|
231 by (simp add: foldD_nest_Un_Int) |
|
232 |
|
233 -- {* Delete rules to do with @{text foldSetD} relation. *} |
|
234 |
|
235 declare foldSetD_imp_finite [simp del] |
|
236 empty_foldSetDE [rule del] |
|
237 foldSetD.intros [rule del] |
|
238 declare (in LCD) |
|
239 foldSetD_closed [rule del] |
|
240 |
|
241 subsection {* Commutative monoids *} |
|
242 |
|
243 text {* |
|
244 We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"} |
|
245 instead of @{text "'b => 'a => 'a"}. |
|
246 *} |
|
247 |
|
248 locale ACeD = |
|
249 fixes D :: "'a set" |
|
250 and f :: "'a => 'a => 'a" (infixl "\<cdot>" 70) |
|
251 and e :: 'a |
|
252 assumes ident [simp]: "x : D ==> x \<cdot> e = x" |
|
253 and commute: "[| x : D; y : D |] ==> x \<cdot> y = y \<cdot> x" |
|
254 and assoc: "[| x : D; y : D; z : D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" |
|
255 and e_closed [simp]: "e : D" |
|
256 and f_closed [simp]: "[| x : D; y : D |] ==> x \<cdot> y : D" |
|
257 |
|
258 lemma (in ACeD) left_commute: |
|
259 "[| x : D; y : D; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" |
|
260 proof - |
|
261 assume D: "x : D" "y : D" "z : D" |
|
262 then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute) |
|
263 also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc) |
|
264 also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute) |
|
265 finally show ?thesis . |
|
266 qed |
|
267 |
|
268 lemmas (in ACeD) AC = assoc commute left_commute |
|
269 |
|
270 lemma (in ACeD) left_ident [simp]: "x : D ==> e \<cdot> x = x" |
|
271 proof - |
|
272 assume D: "x : D" |
|
273 have "x \<cdot> e = x" by (rule ident) |
|
274 with D show ?thesis by (simp add: commute) |
|
275 qed |
|
276 |
|
277 lemma (in ACeD) foldD_Un_Int: |
|
278 "[| finite A; finite B; A <= D; B <= D |] ==> |
|
279 foldD D f e A \<cdot> foldD D f e B = |
|
280 foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)" |
|
281 apply (induct set: Finites) |
|
282 apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]]) |
|
283 (* left_commute is required to show premise of LCD.intro *) |
|
284 apply (simp add: AC insert_absorb Int_insert_left |
|
285 LCD.foldD_insert [OF LCD.intro [of D]] |
|
286 LCD.foldD_closed [OF LCD.intro [of D]] |
|
287 Int_mono2 Un_subset_iff) |
|
288 done |
|
289 |
|
290 lemma (in ACeD) foldD_Un_disjoint: |
|
291 "[| finite A; finite B; A Int B = {}; A <= D; B <= D |] ==> |
|
292 foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B" |
|
293 by (simp add: foldD_Un_Int |
|
294 left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff) |
|
295 |
|
296 end |
|
297 |