src/HOL/Algebra/FiniteProduct.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 16417 9bc16273c2d4 child 16638 3dc904d93767 permissions -rw-r--r--
Constant "If" is now local
1 (*  Title:      HOL/Algebra/FiniteProduct.thy
2     ID:         \$Id\$
3     Author:     Clemens Ballarin, started 19 November 2002
5 This file is largely based on HOL/Finite_Set.thy.
6 *)
8 header {* Product Operator for Commutative Monoids *}
10 theory FiniteProduct imports Group begin
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
15   @{text D}. *}
17 consts
18   foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
20 inductive "foldSetD D f e"
21   intros
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"
26 inductive_cases empty_foldSetDE [elim!]: "({}, x) \<in> foldSetD D f e"
28 constdefs
29   foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
30   "foldD D f e A == THE x. (A, x) \<in> foldSetD D f e"
32 lemma foldSetD_closed:
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";
35   by (erule foldSetD.elims) auto
37 lemma Diff1_foldSetD:
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"
40   apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
41     apply auto
42   done
44 lemma foldSetD_imp_finite [simp]: "(A, x) \<in> foldSetD D f e ==> finite A"
45   by (induct set: foldSetD) auto
47 lemma finite_imp_foldSetD:
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"
50 proof (induct set: Finites)
51   case empty then show ?case by auto
52 next
53   case (insert x F)
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"
57     by (intro foldSetD.intros) auto
58   then show ?case ..
59 qed
61 subsection {* Left-commutative operations *}
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:
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"
71 lemma (in LCD) foldSetD_closed [dest]:
72   "(A, z) \<in> foldSetD D f e ==> z \<in> D";
73   by (erule foldSetD.elims) auto
75 lemma (in LCD) Diff1_foldSetD:
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")
79    prefer 2 apply fast
80   apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
81     apply auto
82   done
84 lemma (in LCD) foldSetD_imp_finite [simp]:
85   "(A, x) \<in> foldSetD D f e ==> finite A"
86   by (induct set: foldSetD) auto
88 lemma (in LCD) finite_imp_foldSetD:
89   "[| finite A; A \<subseteq> B; e \<in> D |] ==> EX x. (A, x) \<in> foldSetD D f e"
90 proof (induct set: Finites)
91   case empty then show ?case by auto
92 next
93   case (insert x F)
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"
97     by (intro foldSetD.intros) auto
98   then show ?case ..
99 qed
101 lemma (in LCD) foldSetD_determ_aux:
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)"
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"}. *}
120   apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb \<in> Aa & xa \<in> Ab")
121    prefer 2 apply (blast elim!: equalityE)
122   apply clarify
123   apply (subgoal_tac "Aa = insert xb Ab - {xa}")
124    prefer 2 apply blast
125   apply (subgoal_tac "card Aa \<le> card Ab")
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
137    apply (subgoal_tac "Aa \<subseteq> B")
138     prefer 2 apply best (* slow *)
139    apply (blast del: equalityCE)
140   apply (subgoal_tac "(Ab - {xa}, x) \<in> foldSetD D f e")
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
152 lemma (in LCD) foldSetD_determ:
153   "[| (A, x) \<in> foldSetD D f e; (A, y) \<in> foldSetD D f e; e \<in> D; A \<subseteq> B |]
154   ==> y = x"
155   by (blast intro: foldSetD_determ_aux [rule_format])
157 lemma (in LCD) foldD_equality:
158   "[| (A, y) \<in> foldSetD D f e; e \<in> D; A \<subseteq> B |] ==> foldD D f e A = y"
159   by (unfold foldD_def) (blast intro: foldSetD_determ)
161 lemma foldD_empty [simp]:
162   "e \<in> D ==> foldD D f e {} = e"
163   by (unfold foldD_def) blast
165 lemma (in LCD) foldD_insert_aux:
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)"
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
177 lemma (in LCD) foldD_insert:
178     "[| finite A; x ~: A; x \<in> B; e \<in> D; A \<subseteq> B |] ==>
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
187 lemma (in LCD) foldD_closed [simp]:
188   "[| finite A; e \<in> D; A \<subseteq> B |] ==> foldD D f e A \<in> D"
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
195 lemma (in LCD) foldD_commute:
196   "[| finite A; x \<in> B; e \<in> D; A \<subseteq> B |] ==>
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
203 lemma Int_mono2:
204   "[| A \<subseteq> C; B \<subseteq> C |] ==> A Int B \<subseteq> C"
205   by blast
207 lemma (in LCD) foldD_nest_Un_Int:
208   "[| finite A; finite C; e \<in> D; A \<subseteq> B; C \<subseteq> B |] ==>
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
216 lemma (in LCD) foldD_nest_Un_disjoint:
217   "[| finite A; finite B; A Int B = {}; e \<in> D; A \<subseteq> B; C \<subseteq> B |]
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)
221 -- {* Delete rules to do with @{text foldSetD} relation. *}
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]
229 subsection {* Commutative monoids *}
231 text {*
232   We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
233   instead of @{text "'b => 'a => 'a"}.
234 *}
236 locale ACeD =
237   fixes D :: "'a set"
238     and f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
239     and e :: 'a
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"
246 lemma (in ACeD) left_commute:
247   "[| x \<in> D; y \<in> D; z \<in> D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
248 proof -
249   assume D: "x \<in> D" "y \<in> D" "z \<in> D"
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
256 lemmas (in ACeD) AC = assoc commute left_commute
258 lemma (in ACeD) left_ident [simp]: "x \<in> D ==> e \<cdot> x = x"
259 proof -
260   assume D: "x \<in> D"
261   have "x \<cdot> e = x" by (rule ident)
262   with D show ?thesis by (simp add: commute)
263 qed
265 lemma (in ACeD) foldD_Un_Int:
266   "[| finite A; finite B; A \<subseteq> D; B \<subseteq> D |] ==>
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
277 lemma (in ACeD) foldD_Un_disjoint:
278   "[| finite A; finite B; A Int B = {}; A \<subseteq> D; B \<subseteq> D |] ==>
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)
283 subsection {* Products over Finite Sets *}
285 constdefs (structure G)
286   finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
287   "finprod G f A == if finite A
288       then foldD (carrier G) (mult G o f) \<one> A
289       else arbitrary"
291 syntax
292   "_finprod" :: "index => idt => 'a set => 'b => 'b"
293       ("(3\<Otimes>__:_. _)" [1000, 0, 51, 10] 10)
294 syntax (xsymbols)
295   "_finprod" :: "index => idt => 'a set => 'b => 'b"
296       ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
297 syntax (HTML output)
298   "_finprod" :: "index => idt => 'a set => 'b => 'b"
299       ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
300 translations
301   "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A"
302   -- {* Beware of argument permutation! *}
304 ML_setup {*
305   simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
306 *}
308 lemma (in comm_monoid) finprod_empty [simp]:
309   "finprod G f {} = \<one>"
310   by (simp add: finprod_def)
312 ML_setup {*
313   simpset_ref() := simpset() setsubgoaler asm_simp_tac;
314 *}
316 declare funcsetI [intro]
317   funcset_mem [dest]
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
337 lemma (in comm_monoid) finprod_one [simp]:
338   "finite A ==> (\<Otimes>i:A. \<one>) = \<one>"
339 proof (induct set: Finites)
340   case empty show ?case by simp
341 next
342   case (insert a A)
343   have "(%i. \<one>) \<in> A -> carrier G" by auto
344   with insert show ?case by simp
345 qed
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
355   case (insert a A)
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
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
365 lemma funcset_Un_left [iff]:
366   "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
367   by fast
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
377   case (insert a A)
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
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
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
399   case (insert a A) then
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"
405     by (simp add: Pi_def)
406   show ?case
407     by (simp add: insert fA fa gA ga fgA m_ac)
408 qed
410 lemma (in comm_monoid) finprod_cong':
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"
413 proof -
414   assume prems: "A = B" "g \<in> B -> carrier G"
415     "!!i. i \<in> B ==> f i = g i"
416   show ?thesis
417   proof (cases "finite B")
418     case True
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"
421     proof induct
422       case empty thus ?case by simp
423     next
424       case (insert x B)
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"
434 	thus "f \<in> B -> carrier G" by fastsimp
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
451 lemma (in comm_monoid) finprod_cong:
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"
454   (* This order of prems is slightly faster (3%) than the last two swapped. *)
455   by (rule finprod_cong') force+
457 text {*Usually, if this rule causes a failed congruence proof error,
458   the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
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 *}
464 declare funcsetI [rule del]
465   funcset_mem [rule del]
467 lemma (in comm_monoid) finprod_0 [simp]:
468   "f \<in> {0::nat} -> carrier G ==> finprod G f {..0} = f 0"
469 by (simp add: Pi_def)
471 lemma (in comm_monoid) finprod_Suc [simp]:
472   "f \<in> {..Suc n} -> carrier G ==>
473    finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})"
474 by (simp add: Pi_def atMost_Suc)
476 lemma (in comm_monoid) finprod_Suc2:
477   "f \<in> {..Suc n} -> carrier G ==>
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
485 lemma (in comm_monoid) finprod_mult [simp]:
486   "[| f \<in> {..n} -> carrier G; g \<in> {..n} -> carrier G |] ==>
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)
491 end