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