author | haftmann |
Fri, 17 Jun 2005 16:12:49 +0200 | |
changeset 16417 | 9bc16273c2d4 |
parent 15328 | 35951e6a7855 |
child 16638 | 3dc904d93767 |
permissions | -rw-r--r-- |
14706 | 1 |
(* Title: HOL/Algebra/FiniteProduct.thy |
13936 | 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 |
||
14706 | 8 |
header {* Product Operator for Commutative Monoids *} |
13936 | 9 |
|
16417 | 10 |
theory FiniteProduct imports Group begin |
13936 | 11 |
|
14750 | 12 |
text {* Instantiation of locale @{text LC} of theory @{text Finite_Set} is not |
13 |
possible, because here we have explicit typing rules like |
|
14 |
@{text "x \<in> carrier G"}. We introduce an explicit argument for the domain |
|
14651 | 15 |
@{text D}. *} |
13936 | 16 |
|
17 |
consts |
|
18 |
foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set" |
|
19 |
||
20 |
inductive "foldSetD D f e" |
|
21 |
intros |
|
14750 | 22 |
emptyI [intro]: "e \<in> D ==> ({}, e) \<in> foldSetD D f e" |
23 |
insertI [intro]: "[| x ~: A; f x y \<in> D; (A, y) \<in> foldSetD D f e |] ==> |
|
24 |
(insert x A, f x y) \<in> foldSetD D f e" |
|
13936 | 25 |
|
14750 | 26 |
inductive_cases empty_foldSetDE [elim!]: "({}, x) \<in> foldSetD D f e" |
13936 | 27 |
|
28 |
constdefs |
|
29 |
foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a" |
|
14750 | 30 |
"foldD D f e A == THE x. (A, x) \<in> foldSetD D f e" |
13936 | 31 |
|
32 |
lemma foldSetD_closed: |
|
14750 | 33 |
"[| (A, z) \<in> foldSetD D f e ; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> D |
34 |
|] ==> z \<in> D"; |
|
13936 | 35 |
by (erule foldSetD.elims) auto |
36 |
||
37 |
lemma Diff1_foldSetD: |
|
14750 | 38 |
"[| (A - {x}, y) \<in> foldSetD D f e; x \<in> A; f x y \<in> D |] ==> |
39 |
(A, f x y) \<in> foldSetD D f e" |
|
13936 | 40 |
apply (erule insert_Diff [THEN subst], rule foldSetD.intros) |
41 |
apply auto |
|
42 |
done |
|
43 |
||
14750 | 44 |
lemma foldSetD_imp_finite [simp]: "(A, x) \<in> foldSetD D f e ==> finite A" |
13936 | 45 |
by (induct set: foldSetD) auto |
46 |
||
47 |
lemma finite_imp_foldSetD: |
|
14750 | 48 |
"[| finite A; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> D |] ==> |
49 |
EX x. (A, x) \<in> foldSetD D f e" |
|
13936 | 50 |
proof (induct set: Finites) |
51 |
case empty then show ?case by auto |
|
52 |
next |
|
15328 | 53 |
case (insert x F) |
14750 | 54 |
then obtain y where y: "(F, y) \<in> foldSetD D f e" by auto |
55 |
with insert have "y \<in> D" by (auto dest: foldSetD_closed) |
|
56 |
with y and insert have "(insert x F, f x y) \<in> foldSetD D f e" |
|
13936 | 57 |
by (intro foldSetD.intros) auto |
58 |
then show ?case .. |
|
59 |
qed |
|
60 |
||
61 |
subsection {* Left-commutative operations *} |
|
62 |
||
63 |
locale LCD = |
|
64 |
fixes B :: "'b set" |
|
65 |
and D :: "'a set" |
|
66 |
and f :: "'b => 'a => 'a" (infixl "\<cdot>" 70) |
|
67 |
assumes left_commute: |
|
14750 | 68 |
"[| x \<in> B; y \<in> B; z \<in> D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" |
69 |
and f_closed [simp, intro!]: "!!x y. [| x \<in> B; y \<in> D |] ==> f x y \<in> D" |
|
13936 | 70 |
|
71 |
lemma (in LCD) foldSetD_closed [dest]: |
|
14750 | 72 |
"(A, z) \<in> foldSetD D f e ==> z \<in> D"; |
13936 | 73 |
by (erule foldSetD.elims) auto |
74 |
||
75 |
lemma (in LCD) Diff1_foldSetD: |
|
14750 | 76 |
"[| (A - {x}, y) \<in> foldSetD D f e; x \<in> A; A \<subseteq> B |] ==> |
77 |
(A, f x y) \<in> foldSetD D f e" |
|
78 |
apply (subgoal_tac "x \<in> B") |
|
13936 | 79 |
prefer 2 apply fast |
80 |
apply (erule insert_Diff [THEN subst], rule foldSetD.intros) |
|
81 |
apply auto |
|
82 |
done |
|
83 |
||
84 |
lemma (in LCD) foldSetD_imp_finite [simp]: |
|
14750 | 85 |
"(A, x) \<in> foldSetD D f e ==> finite A" |
13936 | 86 |
by (induct set: foldSetD) auto |
87 |
||
88 |
lemma (in LCD) finite_imp_foldSetD: |
|
14750 | 89 |
"[| finite A; A \<subseteq> B; e \<in> D |] ==> EX x. (A, x) \<in> foldSetD D f e" |
13936 | 90 |
proof (induct set: Finites) |
91 |
case empty then show ?case by auto |
|
92 |
next |
|
15328 | 93 |
case (insert x F) |
14750 | 94 |
then obtain y where y: "(F, y) \<in> foldSetD D f e" by auto |
95 |
with insert have "y \<in> D" by auto |
|
96 |
with y and insert have "(insert x F, f x y) \<in> foldSetD D f e" |
|
13936 | 97 |
by (intro foldSetD.intros) auto |
98 |
then show ?case .. |
|
99 |
qed |
|
100 |
||
101 |
lemma (in LCD) foldSetD_determ_aux: |
|
14750 | 102 |
"e \<in> D ==> \<forall>A x. A \<subseteq> B & card A < n --> (A, x) \<in> foldSetD D f e --> |
103 |
(\<forall>y. (A, y) \<in> foldSetD D f e --> y = x)" |
|
13936 | 104 |
apply (induct n) |
105 |
apply (auto simp add: less_Suc_eq) (* slow *) |
|
106 |
apply (erule foldSetD.cases) |
|
107 |
apply blast |
|
108 |
apply (erule foldSetD.cases) |
|
109 |
apply blast |
|
110 |
apply clarify |
|
111 |
txt {* force simplification of @{text "card A < card (insert ...)"}. *} |
|
112 |
apply (erule rev_mp) |
|
113 |
apply (simp add: less_Suc_eq_le) |
|
114 |
apply (rule impI) |
|
115 |
apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb") |
|
116 |
apply (subgoal_tac "Aa = Ab") |
|
117 |
prefer 2 apply (blast elim!: equalityE) |
|
118 |
apply blast |
|
119 |
txt {* case @{prop "xa \<notin> xb"}. *} |
|
14750 | 120 |
apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb \<in> Aa & xa \<in> Ab") |
13936 | 121 |
prefer 2 apply (blast elim!: equalityE) |
122 |
apply clarify |
|
123 |
apply (subgoal_tac "Aa = insert xb Ab - {xa}") |
|
124 |
prefer 2 apply blast |
|
14750 | 125 |
apply (subgoal_tac "card Aa \<le> card Ab") |
13936 | 126 |
prefer 2 |
127 |
apply (rule Suc_le_mono [THEN subst]) |
|
128 |
apply (simp add: card_Suc_Diff1) |
|
129 |
apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE]) |
|
130 |
apply (blast intro: foldSetD_imp_finite finite_Diff) |
|
131 |
apply best |
|
132 |
apply assumption |
|
133 |
apply (frule (1) Diff1_foldSetD) |
|
134 |
apply best |
|
135 |
apply (subgoal_tac "ya = f xb x") |
|
136 |
prefer 2 |
|
14750 | 137 |
apply (subgoal_tac "Aa \<subseteq> B") |
13936 | 138 |
prefer 2 apply best (* slow *) |
139 |
apply (blast del: equalityCE) |
|
14750 | 140 |
apply (subgoal_tac "(Ab - {xa}, x) \<in> foldSetD D f e") |
13936 | 141 |
prefer 2 apply simp |
142 |
apply (subgoal_tac "yb = f xa x") |
|
143 |
prefer 2 |
|
144 |
apply (blast del: equalityCE dest: Diff1_foldSetD) |
|
145 |
apply (simp (no_asm_simp)) |
|
146 |
apply (rule left_commute) |
|
147 |
apply assumption |
|
148 |
apply best (* slow *) |
|
149 |
apply best |
|
150 |
done |
|
151 |
||
152 |
lemma (in LCD) foldSetD_determ: |
|
14750 | 153 |
"[| (A, x) \<in> foldSetD D f e; (A, y) \<in> foldSetD D f e; e \<in> D; A \<subseteq> B |] |
13936 | 154 |
==> y = x" |
155 |
by (blast intro: foldSetD_determ_aux [rule_format]) |
|
156 |
||
157 |
lemma (in LCD) foldD_equality: |
|
14750 | 158 |
"[| (A, y) \<in> foldSetD D f e; e \<in> D; A \<subseteq> B |] ==> foldD D f e A = y" |
13936 | 159 |
by (unfold foldD_def) (blast intro: foldSetD_determ) |
160 |
||
161 |
lemma foldD_empty [simp]: |
|
14750 | 162 |
"e \<in> D ==> foldD D f e {} = e" |
13936 | 163 |
by (unfold foldD_def) blast |
164 |
||
165 |
lemma (in LCD) foldD_insert_aux: |
|
14750 | 166 |
"[| x ~: A; x \<in> B; e \<in> D; A \<subseteq> B |] ==> |
167 |
((insert x A, v) \<in> foldSetD D f e) = |
|
168 |
(EX y. (A, y) \<in> foldSetD D f e & v = f x y)" |
|
13936 | 169 |
apply auto |
170 |
apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE]) |
|
171 |
apply (fastsimp dest: foldSetD_imp_finite) |
|
172 |
apply assumption |
|
173 |
apply assumption |
|
174 |
apply (blast intro: foldSetD_determ) |
|
175 |
done |
|
176 |
||
177 |
lemma (in LCD) foldD_insert: |
|
14750 | 178 |
"[| finite A; x ~: A; x \<in> B; e \<in> D; A \<subseteq> B |] ==> |
13936 | 179 |
foldD D f e (insert x A) = f x (foldD D f e A)" |
180 |
apply (unfold foldD_def) |
|
181 |
apply (simp add: foldD_insert_aux) |
|
182 |
apply (rule the_equality) |
|
183 |
apply (auto intro: finite_imp_foldSetD |
|
184 |
cong add: conj_cong simp add: foldD_def [symmetric] foldD_equality) |
|
185 |
done |
|
186 |
||
187 |
lemma (in LCD) foldD_closed [simp]: |
|
14750 | 188 |
"[| finite A; e \<in> D; A \<subseteq> B |] ==> foldD D f e A \<in> D" |
13936 | 189 |
proof (induct set: Finites) |
190 |
case empty then show ?case by (simp add: foldD_empty) |
|
191 |
next |
|
192 |
case insert then show ?case by (simp add: foldD_insert) |
|
193 |
qed |
|
194 |
||
195 |
lemma (in LCD) foldD_commute: |
|
14750 | 196 |
"[| finite A; x \<in> B; e \<in> D; A \<subseteq> B |] ==> |
13936 | 197 |
f x (foldD D f e A) = foldD D f (f x e) A" |
198 |
apply (induct set: Finites) |
|
199 |
apply simp |
|
200 |
apply (auto simp add: left_commute foldD_insert) |
|
201 |
done |
|
202 |
||
203 |
lemma Int_mono2: |
|
14750 | 204 |
"[| A \<subseteq> C; B \<subseteq> C |] ==> A Int B \<subseteq> C" |
13936 | 205 |
by blast |
206 |
||
207 |
lemma (in LCD) foldD_nest_Un_Int: |
|
14750 | 208 |
"[| finite A; finite C; e \<in> D; A \<subseteq> B; C \<subseteq> B |] ==> |
13936 | 209 |
foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)" |
210 |
apply (induct set: Finites) |
|
211 |
apply simp |
|
212 |
apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb |
|
213 |
Int_mono2 Un_subset_iff) |
|
214 |
done |
|
215 |
||
216 |
lemma (in LCD) foldD_nest_Un_disjoint: |
|
14750 | 217 |
"[| finite A; finite B; A Int B = {}; e \<in> D; A \<subseteq> B; C \<subseteq> B |] |
13936 | 218 |
==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A" |
219 |
by (simp add: foldD_nest_Un_Int) |
|
220 |
||
221 |
-- {* Delete rules to do with @{text foldSetD} relation. *} |
|
222 |
||
223 |
declare foldSetD_imp_finite [simp del] |
|
224 |
empty_foldSetDE [rule del] |
|
225 |
foldSetD.intros [rule del] |
|
226 |
declare (in LCD) |
|
227 |
foldSetD_closed [rule del] |
|
228 |
||
229 |
subsection {* Commutative monoids *} |
|
230 |
||
231 |
text {* |
|
232 |
We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"} |
|
233 |
instead of @{text "'b => 'a => 'a"}. |
|
234 |
*} |
|
235 |
||
236 |
locale ACeD = |
|
237 |
fixes D :: "'a set" |
|
238 |
and f :: "'a => 'a => 'a" (infixl "\<cdot>" 70) |
|
239 |
and e :: 'a |
|
14750 | 240 |
assumes ident [simp]: "x \<in> D ==> x \<cdot> e = x" |
241 |
and commute: "[| x \<in> D; y \<in> D |] ==> x \<cdot> y = y \<cdot> x" |
|
242 |
and assoc: "[| x \<in> D; y \<in> D; z \<in> D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" |
|
243 |
and e_closed [simp]: "e \<in> D" |
|
244 |
and f_closed [simp]: "[| x \<in> D; y \<in> D |] ==> x \<cdot> y \<in> D" |
|
13936 | 245 |
|
246 |
lemma (in ACeD) left_commute: |
|
14750 | 247 |
"[| x \<in> D; y \<in> D; z \<in> D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" |
13936 | 248 |
proof - |
14750 | 249 |
assume D: "x \<in> D" "y \<in> D" "z \<in> D" |
13936 | 250 |
then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute) |
251 |
also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc) |
|
252 |
also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute) |
|
253 |
finally show ?thesis . |
|
254 |
qed |
|
255 |
||
256 |
lemmas (in ACeD) AC = assoc commute left_commute |
|
257 |
||
14750 | 258 |
lemma (in ACeD) left_ident [simp]: "x \<in> D ==> e \<cdot> x = x" |
13936 | 259 |
proof - |
14750 | 260 |
assume D: "x \<in> D" |
13936 | 261 |
have "x \<cdot> e = x" by (rule ident) |
262 |
with D show ?thesis by (simp add: commute) |
|
263 |
qed |
|
264 |
||
265 |
lemma (in ACeD) foldD_Un_Int: |
|
14750 | 266 |
"[| finite A; finite B; A \<subseteq> D; B \<subseteq> D |] ==> |
13936 | 267 |
foldD D f e A \<cdot> foldD D f e B = |
268 |
foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)" |
|
269 |
apply (induct set: Finites) |
|
270 |
apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]]) |
|
271 |
apply (simp add: AC insert_absorb Int_insert_left |
|
272 |
LCD.foldD_insert [OF LCD.intro [of D]] |
|
273 |
LCD.foldD_closed [OF LCD.intro [of D]] |
|
274 |
Int_mono2 Un_subset_iff) |
|
275 |
done |
|
276 |
||
277 |
lemma (in ACeD) foldD_Un_disjoint: |
|
14750 | 278 |
"[| finite A; finite B; A Int B = {}; A \<subseteq> D; B \<subseteq> D |] ==> |
13936 | 279 |
foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B" |
280 |
by (simp add: foldD_Un_Int |
|
281 |
left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff) |
|
282 |
||
283 |
subsection {* Products over Finite Sets *} |
|
284 |
||
14651 | 285 |
constdefs (structure G) |
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
14750
diff
changeset
|
286 |
finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b" |
13936 | 287 |
"finprod G f A == if finite A |
14651 | 288 |
then foldD (carrier G) (mult G o f) \<one> A |
13936 | 289 |
else arbitrary" |
290 |
||
14651 | 291 |
syntax |
292 |
"_finprod" :: "index => idt => 'a set => 'b => 'b" |
|
14666 | 293 |
("(3\<Otimes>__:_. _)" [1000, 0, 51, 10] 10) |
14651 | 294 |
syntax (xsymbols) |
295 |
"_finprod" :: "index => idt => 'a set => 'b => 'b" |
|
14666 | 296 |
("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10) |
14651 | 297 |
syntax (HTML output) |
298 |
"_finprod" :: "index => idt => 'a set => 'b => 'b" |
|
14666 | 299 |
("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10) |
14651 | 300 |
translations |
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
14750
diff
changeset
|
301 |
"\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A" |
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
14750
diff
changeset
|
302 |
-- {* Beware of argument permutation! *} |
13936 | 303 |
|
304 |
ML_setup {* |
|
14590 | 305 |
simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; |
13936 | 306 |
*} |
307 |
||
308 |
lemma (in comm_monoid) finprod_empty [simp]: |
|
309 |
"finprod G f {} = \<one>" |
|
310 |
by (simp add: finprod_def) |
|
311 |
||
312 |
ML_setup {* |
|
14590 | 313 |
simpset_ref() := simpset() setsubgoaler asm_simp_tac; |
13936 | 314 |
*} |
315 |
||
316 |
declare funcsetI [intro] |
|
317 |
funcset_mem [dest] |
|
318 |
||
319 |
lemma (in comm_monoid) finprod_insert [simp]: |
|
320 |
"[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==> |
|
321 |
finprod G f (insert a F) = f a \<otimes> finprod G f F" |
|
322 |
apply (rule trans) |
|
323 |
apply (simp add: finprod_def) |
|
324 |
apply (rule trans) |
|
325 |
apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]]) |
|
326 |
apply simp |
|
327 |
apply (rule m_lcomm) |
|
328 |
apply fast |
|
329 |
apply fast |
|
330 |
apply assumption |
|
331 |
apply (fastsimp intro: m_closed) |
|
332 |
apply simp+ |
|
333 |
apply fast |
|
334 |
apply (auto simp add: finprod_def) |
|
335 |
done |
|
336 |
||
337 |
lemma (in comm_monoid) finprod_one [simp]: |
|
14651 | 338 |
"finite A ==> (\<Otimes>i:A. \<one>) = \<one>" |
13936 | 339 |
proof (induct set: Finites) |
340 |
case empty show ?case by simp |
|
341 |
next |
|
15328 | 342 |
case (insert a A) |
13936 | 343 |
have "(%i. \<one>) \<in> A -> carrier G" by auto |
344 |
with insert show ?case by simp |
|
345 |
qed |
|
346 |
||
347 |
lemma (in comm_monoid) finprod_closed [simp]: |
|
348 |
fixes A |
|
349 |
assumes fin: "finite A" and f: "f \<in> A -> carrier G" |
|
350 |
shows "finprod G f A \<in> carrier G" |
|
351 |
using fin f |
|
352 |
proof induct |
|
353 |
case empty show ?case by simp |
|
354 |
next |
|
15328 | 355 |
case (insert a A) |
13936 | 356 |
then have a: "f a \<in> carrier G" by fast |
357 |
from insert have A: "f \<in> A -> carrier G" by fast |
|
358 |
from insert A a show ?case by simp |
|
359 |
qed |
|
360 |
||
361 |
lemma funcset_Int_left [simp, intro]: |
|
362 |
"[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C" |
|
363 |
by fast |
|
364 |
||
365 |
lemma funcset_Un_left [iff]: |
|
366 |
"(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)" |
|
367 |
by fast |
|
368 |
||
369 |
lemma (in comm_monoid) finprod_Un_Int: |
|
370 |
"[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==> |
|
371 |
finprod G g (A Un B) \<otimes> finprod G g (A Int B) = |
|
372 |
finprod G g A \<otimes> finprod G g B" |
|
373 |
-- {* The reversed orientation looks more natural, but LOOPS as a simprule! *} |
|
374 |
proof (induct set: Finites) |
|
375 |
case empty then show ?case by (simp add: finprod_closed) |
|
376 |
next |
|
15328 | 377 |
case (insert a A) |
13936 | 378 |
then have a: "g a \<in> carrier G" by fast |
379 |
from insert have A: "g \<in> A -> carrier G" by fast |
|
380 |
from insert A a show ?case |
|
381 |
by (simp add: m_ac Int_insert_left insert_absorb finprod_closed |
|
382 |
Int_mono2 Un_subset_iff) |
|
383 |
qed |
|
384 |
||
385 |
lemma (in comm_monoid) finprod_Un_disjoint: |
|
386 |
"[| finite A; finite B; A Int B = {}; |
|
387 |
g \<in> A -> carrier G; g \<in> B -> carrier G |] |
|
388 |
==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B" |
|
389 |
apply (subst finprod_Un_Int [symmetric]) |
|
390 |
apply (auto simp add: finprod_closed) |
|
391 |
done |
|
392 |
||
393 |
lemma (in comm_monoid) finprod_multf: |
|
394 |
"[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==> |
|
395 |
finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)" |
|
396 |
proof (induct set: Finites) |
|
397 |
case empty show ?case by simp |
|
398 |
next |
|
15328 | 399 |
case (insert a A) then |
14750 | 400 |
have fA: "f \<in> A -> carrier G" by fast |
401 |
from insert have fa: "f a \<in> carrier G" by fast |
|
402 |
from insert have gA: "g \<in> A -> carrier G" by fast |
|
403 |
from insert have ga: "g a \<in> carrier G" by fast |
|
404 |
from insert have fgA: "(%x. f x \<otimes> g x) \<in> A -> carrier G" |
|
13936 | 405 |
by (simp add: Pi_def) |
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
14750
diff
changeset
|
406 |
show ?case |
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
14750
diff
changeset
|
407 |
by (simp add: insert fA fa gA ga fgA m_ac) |
13936 | 408 |
qed |
409 |
||
410 |
lemma (in comm_monoid) finprod_cong': |
|
14750 | 411 |
"[| A = B; g \<in> B -> carrier G; |
412 |
!!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B" |
|
13936 | 413 |
proof - |
14750 | 414 |
assume prems: "A = B" "g \<in> B -> carrier G" |
415 |
"!!i. i \<in> B ==> f i = g i" |
|
13936 | 416 |
show ?thesis |
417 |
proof (cases "finite B") |
|
418 |
case True |
|
14750 | 419 |
then have "!!A. [| A = B; g \<in> B -> carrier G; |
420 |
!!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B" |
|
13936 | 421 |
proof induct |
422 |
case empty thus ?case by simp |
|
423 |
next |
|
15328 | 424 |
case (insert x B) |
13936 | 425 |
then have "finprod G f A = finprod G f (insert x B)" by simp |
426 |
also from insert have "... = f x \<otimes> finprod G f B" |
|
427 |
proof (intro finprod_insert) |
|
428 |
show "finite B" . |
|
429 |
next |
|
430 |
show "x ~: B" . |
|
431 |
next |
|
432 |
assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i" |
|
433 |
"g \<in> insert x B \<rightarrow> carrier G" |
|
14750 | 434 |
thus "f \<in> B -> carrier G" by fastsimp |
13936 | 435 |
next |
436 |
assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i" |
|
437 |
"g \<in> insert x B \<rightarrow> carrier G" |
|
438 |
thus "f x \<in> carrier G" by fastsimp |
|
439 |
qed |
|
440 |
also from insert have "... = g x \<otimes> finprod G g B" by fastsimp |
|
441 |
also from insert have "... = finprod G g (insert x B)" |
|
442 |
by (intro finprod_insert [THEN sym]) auto |
|
443 |
finally show ?case . |
|
444 |
qed |
|
445 |
with prems show ?thesis by simp |
|
446 |
next |
|
447 |
case False with prems show ?thesis by (simp add: finprod_def) |
|
448 |
qed |
|
449 |
qed |
|
450 |
||
451 |
lemma (in comm_monoid) finprod_cong: |
|
14750 | 452 |
"[| A = B; f \<in> B -> carrier G = True; |
453 |
!!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B" |
|
14213
7bf882b0a51e
Changed order of prems in finprod_cong. Slight speedup.
ballarin
parents:
13936
diff
changeset
|
454 |
(* This order of prems is slightly faster (3%) than the last two swapped. *) |
7bf882b0a51e
Changed order of prems in finprod_cong. Slight speedup.
ballarin
parents:
13936
diff
changeset
|
455 |
by (rule finprod_cong') force+ |
13936 | 456 |
|
457 |
text {*Usually, if this rule causes a failed congruence proof error, |
|
14750 | 458 |
the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown. |
13936 | 459 |
Adding @{thm [source] Pi_def} to the simpset is often useful. |
460 |
For this reason, @{thm [source] comm_monoid.finprod_cong} |
|
461 |
is not added to the simpset by default. |
|
462 |
*} |
|
463 |
||
464 |
declare funcsetI [rule del] |
|
465 |
funcset_mem [rule del] |
|
466 |
||
467 |
lemma (in comm_monoid) finprod_0 [simp]: |
|
14750 | 468 |
"f \<in> {0::nat} -> carrier G ==> finprod G f {..0} = f 0" |
13936 | 469 |
by (simp add: Pi_def) |
470 |
||
471 |
lemma (in comm_monoid) finprod_Suc [simp]: |
|
14750 | 472 |
"f \<in> {..Suc n} -> carrier G ==> |
13936 | 473 |
finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})" |
474 |
by (simp add: Pi_def atMost_Suc) |
|
475 |
||
476 |
lemma (in comm_monoid) finprod_Suc2: |
|
14750 | 477 |
"f \<in> {..Suc n} -> carrier G ==> |
13936 | 478 |
finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)" |
479 |
proof (induct n) |
|
480 |
case 0 thus ?case by (simp add: Pi_def) |
|
481 |
next |
|
482 |
case Suc thus ?case by (simp add: m_assoc Pi_def) |
|
483 |
qed |
|
484 |
||
485 |
lemma (in comm_monoid) finprod_mult [simp]: |
|
14750 | 486 |
"[| f \<in> {..n} -> carrier G; g \<in> {..n} -> carrier G |] ==> |
13936 | 487 |
finprod G (%i. f i \<otimes> g i) {..n::nat} = |
488 |
finprod G f {..n} \<otimes> finprod G g {..n}" |
|
489 |
by (induct n) (simp_all add: m_ac Pi_def) |
|
490 |
||
491 |
end |
|
492 |