author  nipkow 
Fri, 13 Nov 2009 14:14:04 +0100  
changeset 33657  a4179bf442d1 
parent 32960  69916a850301 
child 35054  a5db9779b026 
permissions  rwrr 
14706  1 
(* Title: HOL/Algebra/FiniteProduct.thy 
13936  2 
Author: Clemens Ballarin, started 19 November 2002 
3 

4 
This file is largely based on HOL/Finite_Set.thy. 

5 
*) 

6 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
16638
diff
changeset

7 
theory FiniteProduct imports Group begin 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
16638
diff
changeset

8 

13936  9 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27699
diff
changeset

10 
subsection {* Product Operator for Commutative Monoids *} 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
16638
diff
changeset

11 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27699
diff
changeset

12 
subsubsection {* Inductive Definition of a Relation for Products over Sets *} 
13936  13 

14750  14 
text {* Instantiation of locale @{text LC} of theory @{text Finite_Set} is not 
15 
possible, because here we have explicit typing rules like 

16 
@{text "x \<in> carrier G"}. We introduce an explicit argument for the domain 

14651  17 
@{text D}. *} 
13936  18 

23746  19 
inductive_set 
13936  20 
foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set" 
23746  21 
for D :: "'a set" and f :: "'b => 'a => 'a" and e :: 'a 
22 
where 

14750  23 
emptyI [intro]: "e \<in> D ==> ({}, e) \<in> foldSetD D f e" 
23746  24 
 insertI [intro]: "[ x ~: A; f x y \<in> D; (A, y) \<in> foldSetD D f e ] ==> 
14750  25 
(insert x A, f x y) \<in> foldSetD D f e" 
13936  26 

14750  27 
inductive_cases empty_foldSetDE [elim!]: "({}, x) \<in> foldSetD D f e" 
13936  28 

29 
constdefs 

30 
foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a" 

14750  31 
"foldD D f e A == THE x. (A, x) \<in> foldSetD D f e" 
13936  32 

33 
lemma foldSetD_closed: 

14750  34 
"[ (A, z) \<in> foldSetD D f e ; e \<in> D; !!x y. [ x \<in> A; y \<in> D ] ==> f x y \<in> D 
35 
] ==> z \<in> D"; 

23746  36 
by (erule foldSetD.cases) auto 
13936  37 

38 
lemma Diff1_foldSetD: 

14750  39 
"[ (A  {x}, y) \<in> foldSetD D f e; x \<in> A; f x y \<in> D ] ==> 
40 
(A, f x y) \<in> foldSetD D f e" 

13936  41 
apply (erule insert_Diff [THEN subst], rule foldSetD.intros) 
42 
apply auto 

43 
done 

44 

14750  45 
lemma foldSetD_imp_finite [simp]: "(A, x) \<in> foldSetD D f e ==> finite A" 
13936  46 
by (induct set: foldSetD) auto 
47 

48 
lemma finite_imp_foldSetD: 

14750  49 
"[ finite A; e \<in> D; !!x y. [ x \<in> A; y \<in> D ] ==> f x y \<in> D ] ==> 
50 
EX x. (A, x) \<in> foldSetD D f e" 

22265  51 
proof (induct set: finite) 
13936  52 
case empty then show ?case by auto 
53 
next 

15328  54 
case (insert x F) 
14750  55 
then obtain y where y: "(F, y) \<in> foldSetD D f e" by auto 
56 
with insert have "y \<in> D" by (auto dest: foldSetD_closed) 

57 
with y and insert have "(insert x F, f x y) \<in> foldSetD D f e" 

13936  58 
by (intro foldSetD.intros) auto 
59 
then show ?case .. 

60 
qed 

61 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
16638
diff
changeset

62 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27699
diff
changeset

63 
text {* LeftCommutative Operations *} 
13936  64 

65 
locale LCD = 

66 
fixes B :: "'b set" 

67 
and D :: "'a set" 

68 
and f :: "'b => 'a => 'a" (infixl "\<cdot>" 70) 

69 
assumes left_commute: 

14750  70 
"[ x \<in> B; y \<in> B; z \<in> D ] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" 
71 
and f_closed [simp, intro!]: "!!x y. [ x \<in> B; y \<in> D ] ==> f x y \<in> D" 

13936  72 

73 
lemma (in LCD) foldSetD_closed [dest]: 

14750  74 
"(A, z) \<in> foldSetD D f e ==> z \<in> D"; 
23746  75 
by (erule foldSetD.cases) auto 
13936  76 

77 
lemma (in LCD) Diff1_foldSetD: 

14750  78 
"[ (A  {x}, y) \<in> foldSetD D f e; x \<in> A; A \<subseteq> B ] ==> 
79 
(A, f x y) \<in> foldSetD D f e" 

80 
apply (subgoal_tac "x \<in> B") 

13936  81 
prefer 2 apply fast 
82 
apply (erule insert_Diff [THEN subst], rule foldSetD.intros) 

83 
apply auto 

84 
done 

85 

86 
lemma (in LCD) foldSetD_imp_finite [simp]: 

14750  87 
"(A, x) \<in> foldSetD D f e ==> finite A" 
13936  88 
by (induct set: foldSetD) auto 
89 

90 
lemma (in LCD) finite_imp_foldSetD: 

14750  91 
"[ finite A; A \<subseteq> B; e \<in> D ] ==> EX x. (A, x) \<in> foldSetD D f e" 
22265  92 
proof (induct set: finite) 
13936  93 
case empty then show ?case by auto 
94 
next 

15328  95 
case (insert x F) 
14750  96 
then obtain y where y: "(F, y) \<in> foldSetD D f e" by auto 
97 
with insert have "y \<in> D" by auto 

98 
with y and insert have "(insert x F, f x y) \<in> foldSetD D f e" 

13936  99 
by (intro foldSetD.intros) auto 
100 
then show ?case .. 

101 
qed 

102 

103 
lemma (in LCD) foldSetD_determ_aux: 

14750  104 
"e \<in> D ==> \<forall>A x. A \<subseteq> B & card A < n > (A, x) \<in> foldSetD D f e > 
105 
(\<forall>y. (A, y) \<in> foldSetD D f e > y = x)" 

13936  106 
apply (induct n) 
107 
apply (auto simp add: less_Suc_eq) (* slow *) 

108 
apply (erule foldSetD.cases) 

109 
apply blast 

110 
apply (erule foldSetD.cases) 

111 
apply blast 

112 
apply clarify 

113 
txt {* force simplification of @{text "card A < card (insert ...)"}. *} 

114 
apply (erule rev_mp) 

115 
apply (simp add: less_Suc_eq_le) 

116 
apply (rule impI) 

23746  117 
apply (rename_tac xa Aa ya xb Ab yb, case_tac "xa = xb") 
13936  118 
apply (subgoal_tac "Aa = Ab") 
119 
prefer 2 apply (blast elim!: equalityE) 

120 
apply blast 

121 
txt {* case @{prop "xa \<notin> xb"}. *} 

14750  122 
apply (subgoal_tac "Aa  {xb} = Ab  {xa} & xb \<in> Aa & xa \<in> Ab") 
13936  123 
prefer 2 apply (blast elim!: equalityE) 
124 
apply clarify 

125 
apply (subgoal_tac "Aa = insert xb Ab  {xa}") 

126 
prefer 2 apply blast 

14750  127 
apply (subgoal_tac "card Aa \<le> card Ab") 
13936  128 
prefer 2 
129 
apply (rule Suc_le_mono [THEN subst]) 

130 
apply (simp add: card_Suc_Diff1) 

131 
apply (rule_tac A1 = "Aa  {xb}" in finite_imp_foldSetD [THEN exE]) 

132 
apply (blast intro: foldSetD_imp_finite finite_Diff) 

133 
apply best 

134 
apply assumption 

135 
apply (frule (1) Diff1_foldSetD) 

136 
apply best 

137 
apply (subgoal_tac "ya = f xb x") 

138 
prefer 2 

14750  139 
apply (subgoal_tac "Aa \<subseteq> B") 
13936  140 
prefer 2 apply best (* slow *) 
141 
apply (blast del: equalityCE) 

14750  142 
apply (subgoal_tac "(Ab  {xa}, x) \<in> foldSetD D f e") 
13936  143 
prefer 2 apply simp 
144 
apply (subgoal_tac "yb = f xa x") 

145 
prefer 2 

146 
apply (blast del: equalityCE dest: Diff1_foldSetD) 

147 
apply (simp (no_asm_simp)) 

148 
apply (rule left_commute) 

149 
apply assumption 

150 
apply best (* slow *) 

151 
apply best 

152 
done 

153 

154 
lemma (in LCD) foldSetD_determ: 

14750  155 
"[ (A, x) \<in> foldSetD D f e; (A, y) \<in> foldSetD D f e; e \<in> D; A \<subseteq> B ] 
13936  156 
==> y = x" 
157 
by (blast intro: foldSetD_determ_aux [rule_format]) 

158 

159 
lemma (in LCD) foldD_equality: 

14750  160 
"[ (A, y) \<in> foldSetD D f e; e \<in> D; A \<subseteq> B ] ==> foldD D f e A = y" 
13936  161 
by (unfold foldD_def) (blast intro: foldSetD_determ) 
162 

163 
lemma foldD_empty [simp]: 

14750  164 
"e \<in> D ==> foldD D f e {} = e" 
13936  165 
by (unfold foldD_def) blast 
166 

167 
lemma (in LCD) foldD_insert_aux: 

14750  168 
"[ x ~: A; x \<in> B; e \<in> D; A \<subseteq> B ] ==> 
169 
((insert x A, v) \<in> foldSetD D f e) = 

170 
(EX y. (A, y) \<in> foldSetD D f e & v = f x y)" 

13936  171 
apply auto 
172 
apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE]) 

173 
apply (fastsimp dest: foldSetD_imp_finite) 

174 
apply assumption 

175 
apply assumption 

176 
apply (blast intro: foldSetD_determ) 

177 
done 

178 

179 
lemma (in LCD) foldD_insert: 

14750  180 
"[ finite A; x ~: A; x \<in> B; e \<in> D; A \<subseteq> B ] ==> 
13936  181 
foldD D f e (insert x A) = f x (foldD D f e A)" 
182 
apply (unfold foldD_def) 

183 
apply (simp add: foldD_insert_aux) 

184 
apply (rule the_equality) 

185 
apply (auto intro: finite_imp_foldSetD 

186 
cong add: conj_cong simp add: foldD_def [symmetric] foldD_equality) 

187 
done 

188 

189 
lemma (in LCD) foldD_closed [simp]: 

14750  190 
"[ finite A; e \<in> D; A \<subseteq> B ] ==> foldD D f e A \<in> D" 
22265  191 
proof (induct set: finite) 
13936  192 
case empty then show ?case by (simp add: foldD_empty) 
193 
next 

194 
case insert then show ?case by (simp add: foldD_insert) 

195 
qed 

196 

197 
lemma (in LCD) foldD_commute: 

14750  198 
"[ finite A; x \<in> B; e \<in> D; A \<subseteq> B ] ==> 
13936  199 
f x (foldD D f e A) = foldD D f (f x e) A" 
22265  200 
apply (induct set: finite) 
13936  201 
apply simp 
202 
apply (auto simp add: left_commute foldD_insert) 

203 
done 

204 

205 
lemma Int_mono2: 

14750  206 
"[ A \<subseteq> C; B \<subseteq> C ] ==> A Int B \<subseteq> C" 
13936  207 
by blast 
208 

209 
lemma (in LCD) foldD_nest_Un_Int: 

14750  210 
"[ finite A; finite C; e \<in> D; A \<subseteq> B; C \<subseteq> B ] ==> 
13936  211 
foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)" 
22265  212 
apply (induct set: finite) 
13936  213 
apply simp 
214 
apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb 

32693  215 
Int_mono2) 
13936  216 
done 
217 

218 
lemma (in LCD) foldD_nest_Un_disjoint: 

14750  219 
"[ finite A; finite B; A Int B = {}; e \<in> D; A \<subseteq> B; C \<subseteq> B ] 
13936  220 
==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A" 
221 
by (simp add: foldD_nest_Un_Int) 

222 

223 
 {* Delete rules to do with @{text foldSetD} relation. *} 

224 

225 
declare foldSetD_imp_finite [simp del] 

226 
empty_foldSetDE [rule del] 

227 
foldSetD.intros [rule del] 

228 
declare (in LCD) 

229 
foldSetD_closed [rule del] 

230 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
16638
diff
changeset

231 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27699
diff
changeset

232 
text {* Commutative Monoids *} 
13936  233 

234 
text {* 

235 
We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"} 

236 
instead of @{text "'b => 'a => 'a"}. 

237 
*} 

238 

239 
locale ACeD = 

240 
fixes D :: "'a set" 

241 
and f :: "'a => 'a => 'a" (infixl "\<cdot>" 70) 

242 
and e :: 'a 

14750  243 
assumes ident [simp]: "x \<in> D ==> x \<cdot> e = x" 
244 
and commute: "[ x \<in> D; y \<in> D ] ==> x \<cdot> y = y \<cdot> x" 

245 
and assoc: "[ x \<in> D; y \<in> D; z \<in> D ] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" 

246 
and e_closed [simp]: "e \<in> D" 

247 
and f_closed [simp]: "[ x \<in> D; y \<in> D ] ==> x \<cdot> y \<in> D" 

13936  248 

249 
lemma (in ACeD) left_commute: 

14750  250 
"[ x \<in> D; y \<in> D; z \<in> D ] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" 
13936  251 
proof  
14750  252 
assume D: "x \<in> D" "y \<in> D" "z \<in> D" 
13936  253 
then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute) 
254 
also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc) 

255 
also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute) 

256 
finally show ?thesis . 

257 
qed 

258 

259 
lemmas (in ACeD) AC = assoc commute left_commute 

260 

14750  261 
lemma (in ACeD) left_ident [simp]: "x \<in> D ==> e \<cdot> x = x" 
13936  262 
proof  
23350  263 
assume "x \<in> D" 
264 
then have "x \<cdot> e = x" by (rule ident) 

265 
with `x \<in> D` show ?thesis by (simp add: commute) 

13936  266 
qed 
267 

268 
lemma (in ACeD) foldD_Un_Int: 

14750  269 
"[ finite A; finite B; A \<subseteq> D; B \<subseteq> D ] ==> 
13936  270 
foldD D f e A \<cdot> foldD D f e B = 
271 
foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)" 

22265  272 
apply (induct set: finite) 
13936  273 
apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]]) 
274 
apply (simp add: AC insert_absorb Int_insert_left 

275 
LCD.foldD_insert [OF LCD.intro [of D]] 

276 
LCD.foldD_closed [OF LCD.intro [of D]] 

32693  277 
Int_mono2) 
13936  278 
done 
279 

280 
lemma (in ACeD) foldD_Un_disjoint: 

14750  281 
"[ finite A; finite B; A Int B = {}; A \<subseteq> D; B \<subseteq> D ] ==> 
13936  282 
foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B" 
283 
by (simp add: foldD_Un_Int 

32693  284 
left_commute LCD.foldD_closed [OF LCD.intro [of D]]) 
13936  285 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
16638
diff
changeset

286 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27699
diff
changeset

287 
subsubsection {* Products over Finite Sets *} 
13936  288 

14651  289 
constdefs (structure G) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
14750
diff
changeset

290 
finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b" 
13936  291 
"finprod G f A == if finite A 
14651  292 
then foldD (carrier G) (mult G o f) \<one> A 
28524  293 
else undefined" 
13936  294 

14651  295 
syntax 
296 
"_finprod" :: "index => idt => 'a set => 'b => 'b" 

14666  297 
("(3\<Otimes>__:_. _)" [1000, 0, 51, 10] 10) 
14651  298 
syntax (xsymbols) 
299 
"_finprod" :: "index => idt => 'a set => 'b => 'b" 

14666  300 
("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10) 
14651  301 
syntax (HTML output) 
302 
"_finprod" :: "index => idt => 'a set => 'b => 'b" 

14666  303 
("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10) 
14651  304 
translations 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
14750
diff
changeset

305 
"\<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

306 
 {* Beware of argument permutation! *} 
13936  307 

308 
lemma (in comm_monoid) finprod_empty [simp]: 

309 
"finprod G f {} = \<one>" 

310 
by (simp add: finprod_def) 

311 

312 
declare funcsetI [intro] 

313 
funcset_mem [dest] 

314 

27933  315 
context comm_monoid begin 
316 

317 
lemma finprod_insert [simp]: 

13936  318 
"[ finite F; a \<notin> F; f \<in> F > carrier G; f a \<in> carrier G ] ==> 
319 
finprod G f (insert a F) = f a \<otimes> finprod G f F" 

320 
apply (rule trans) 

321 
apply (simp add: finprod_def) 

322 
apply (rule trans) 

323 
apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]]) 

324 
apply simp 

325 
apply (rule m_lcomm) 

326 
apply fast 

327 
apply fast 

328 
apply assumption 

329 
apply (fastsimp intro: m_closed) 

330 
apply simp+ 

331 
apply fast 

332 
apply (auto simp add: finprod_def) 

333 
done 

334 

27933  335 
lemma finprod_one [simp]: 
14651  336 
"finite A ==> (\<Otimes>i:A. \<one>) = \<one>" 
22265  337 
proof (induct set: finite) 
13936  338 
case empty show ?case by simp 
339 
next 

15328  340 
case (insert a A) 
13936  341 
have "(%i. \<one>) \<in> A > carrier G" by auto 
342 
with insert show ?case by simp 

343 
qed 

344 

27933  345 
lemma finprod_closed [simp]: 
13936  346 
fixes A 
347 
assumes fin: "finite A" and f: "f \<in> A > carrier G" 

348 
shows "finprod G f A \<in> carrier G" 

349 
using fin f 

350 
proof induct 

351 
case empty show ?case by simp 

352 
next 

15328  353 
case (insert a A) 
13936  354 
then have a: "f a \<in> carrier G" by fast 
355 
from insert have A: "f \<in> A > carrier G" by fast 

356 
from insert A a show ?case by simp 

357 
qed 

358 

359 
lemma funcset_Int_left [simp, intro]: 

360 
"[ f \<in> A > C; f \<in> B > C ] ==> f \<in> A Int B > C" 

361 
by fast 

362 

363 
lemma funcset_Un_left [iff]: 

364 
"(f \<in> A Un B > C) = (f \<in> A > C & f \<in> B > C)" 

365 
by fast 

366 

27933  367 
lemma finprod_Un_Int: 
13936  368 
"[ finite A; finite B; g \<in> A > carrier G; g \<in> B > carrier G ] ==> 
369 
finprod G g (A Un B) \<otimes> finprod G g (A Int B) = 

370 
finprod G g A \<otimes> finprod G g B" 

371 
 {* The reversed orientation looks more natural, but LOOPS as a simprule! *} 

22265  372 
proof (induct set: finite) 
13936  373 
case empty then show ?case by (simp add: finprod_closed) 
374 
next 

15328  375 
case (insert a A) 
13936  376 
then have a: "g a \<in> carrier G" by fast 
377 
from insert have A: "g \<in> A > carrier G" by fast 

378 
from insert A a show ?case 

379 
by (simp add: m_ac Int_insert_left insert_absorb finprod_closed 

32693  380 
Int_mono2) 
13936  381 
qed 
382 

27933  383 
lemma finprod_Un_disjoint: 
13936  384 
"[ finite A; finite B; A Int B = {}; 
385 
g \<in> A > carrier G; g \<in> B > carrier G ] 

386 
==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B" 

387 
apply (subst finprod_Un_Int [symmetric]) 

388 
apply (auto simp add: finprod_closed) 

389 
done 

390 

27933  391 
lemma finprod_multf: 
13936  392 
"[ finite A; f \<in> A > carrier G; g \<in> A > carrier G ] ==> 
393 
finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)" 

22265  394 
proof (induct set: finite) 
13936  395 
case empty show ?case by simp 
396 
next 

15328  397 
case (insert a A) then 
14750  398 
have fA: "f \<in> A > carrier G" by fast 
399 
from insert have fa: "f a \<in> carrier G" by fast 

400 
from insert have gA: "g \<in> A > carrier G" by fast 

401 
from insert have ga: "g a \<in> carrier G" by fast 

402 
from insert have fgA: "(%x. f x \<otimes> g x) \<in> A > carrier G" 

13936  403 
by (simp add: Pi_def) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
14750
diff
changeset

404 
show ?case 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
14750
diff
changeset

405 
by (simp add: insert fA fa gA ga fgA m_ac) 
13936  406 
qed 
407 

27933  408 
lemma finprod_cong': 
14750  409 
"[ A = B; g \<in> B > carrier G; 
410 
!!i. i \<in> B ==> f i = g i ] ==> finprod G f A = finprod G g B" 

13936  411 
proof  
14750  412 
assume prems: "A = B" "g \<in> B > carrier G" 
413 
"!!i. i \<in> B ==> f i = g i" 

13936  414 
show ?thesis 
415 
proof (cases "finite B") 

416 
case True 

14750  417 
then have "!!A. [ A = B; g \<in> B > carrier G; 
418 
!!i. i \<in> B ==> f i = g i ] ==> finprod G f A = finprod G g B" 

13936  419 
proof induct 
420 
case empty thus ?case by simp 

421 
next 

15328  422 
case (insert x B) 
13936  423 
then have "finprod G f A = finprod G f (insert x B)" by simp 
424 
also from insert have "... = f x \<otimes> finprod G f B" 

425 
proof (intro finprod_insert) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32693
diff
changeset

426 
show "finite B" by fact 
13936  427 
next 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32693
diff
changeset

428 
show "x ~: B" by fact 
13936  429 
next 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32693
diff
changeset

430 
assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32693
diff
changeset

431 
"g \<in> insert x B \<rightarrow> carrier G" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32693
diff
changeset

432 
thus "f \<in> B > carrier G" by fastsimp 
13936  433 
next 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32693
diff
changeset

434 
assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32693
diff
changeset

435 
"g \<in> insert x B \<rightarrow> carrier G" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32693
diff
changeset

436 
thus "f x \<in> carrier G" by fastsimp 
13936  437 
qed 
438 
also from insert have "... = g x \<otimes> finprod G g B" by fastsimp 

439 
also from insert have "... = finprod G g (insert x B)" 

440 
by (intro finprod_insert [THEN sym]) auto 

441 
finally show ?case . 

442 
qed 

443 
with prems show ?thesis by simp 

444 
next 

445 
case False with prems show ?thesis by (simp add: finprod_def) 

446 
qed 

447 
qed 

448 

27933  449 
lemma finprod_cong: 
14750  450 
"[ A = B; f \<in> B > carrier G = True; 
451 
!!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

452 
(* 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

453 
by (rule finprod_cong') force+ 
13936  454 

455 
text {*Usually, if this rule causes a failed congruence proof error, 

14750  456 
the reason is that the premise @{text "g \<in> B > carrier G"} cannot be shown. 
13936  457 
Adding @{thm [source] Pi_def} to the simpset is often useful. 
458 
For this reason, @{thm [source] comm_monoid.finprod_cong} 

459 
is not added to the simpset by default. 

460 
*} 

461 

27933  462 
end 
463 

13936  464 
declare funcsetI [rule del] 
465 
funcset_mem [rule del] 

466 

27933  467 
context comm_monoid begin 
468 

469 
lemma finprod_0 [simp]: 

14750  470 
"f \<in> {0::nat} > carrier G ==> finprod G f {..0} = f 0" 
13936  471 
by (simp add: Pi_def) 
472 

27933  473 
lemma finprod_Suc [simp]: 
14750  474 
"f \<in> {..Suc n} > carrier G ==> 
13936  475 
finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})" 
476 
by (simp add: Pi_def atMost_Suc) 

477 

27933  478 
lemma finprod_Suc2: 
14750  479 
"f \<in> {..Suc n} > carrier G ==> 
13936  480 
finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)" 
481 
proof (induct n) 

482 
case 0 thus ?case by (simp add: Pi_def) 

483 
next 

484 
case Suc thus ?case by (simp add: m_assoc Pi_def) 

485 
qed 

486 

27933  487 
lemma finprod_mult [simp]: 
14750  488 
"[ f \<in> {..n} > carrier G; g \<in> {..n} > carrier G ] ==> 
13936  489 
finprod G (%i. f i \<otimes> g i) {..n::nat} = 
490 
finprod G f {..n} \<otimes> finprod G g {..n}" 

491 
by (induct n) (simp_all add: m_ac Pi_def) 

492 

27699  493 
(* The following two were contributed by Jeremy Avigad. *) 
494 

27933  495 
lemma finprod_reindex: 
27699  496 
assumes fin: "finite A" 
497 
shows "f : (h ` A) \<rightarrow> carrier G \<Longrightarrow> 

498 
inj_on h A ==> finprod G f (h ` A) = finprod G (%x. f (h x)) A" 

499 
using fin apply induct 

500 
apply (auto simp add: finprod_insert Pi_def) 

501 
done 

502 

27933  503 
lemma finprod_const: 
27699  504 
assumes fin [simp]: "finite A" 
505 
and a [simp]: "a : carrier G" 

506 
shows "finprod G (%x. a) A = a (^) card A" 

507 
using fin apply induct 

508 
apply force 

509 
apply (subst finprod_insert) 

510 
apply auto 

511 
apply (subst m_comm) 

512 
apply auto 

513 
done 

514 

27933  515 
(* The following lemma was contributed by Jesus Aransay. *) 
516 

517 
lemma finprod_singleton: 

518 
assumes i_in_A: "i \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> carrier G" 

519 
shows "(\<Otimes>j\<in>A. if i = j then f j else \<one>) = f i" 

29237  520 
using i_in_A finprod_insert [of "A  {i}" i "(\<lambda>j. if i = j then f j else \<one>)"] 
521 
fin_A f_Pi finprod_one [of "A  {i}"] 

522 
finprod_cong [of "A  {i}" "A  {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"] 

27933  523 
unfolding Pi_def simp_implies_def by (force simp add: insert_absorb) 
524 

13936  525 
end 
27933  526 

527 
end 