src/HOL/Algebra/FiniteProduct.thy
author paulson <lp15@cam.ac.uk>
Sun Jun 17 22:00:43 2018 +0100 (11 months ago)
changeset 68458 023b353911c5
parent 68447 0beb927eed89
child 68517 6b5f15387353
permissions -rw-r--r--
Algebra tidy-up
     1 (*  Title:      HOL/Algebra/FiniteProduct.thy
     2     Author:     Clemens Ballarin, started 19 November 2002
     3 
     4 This file is largely based on HOL/Finite_Set.thy.
     5 *)
     6 
     7 theory FiniteProduct
     8 imports Group
     9 begin
    10 
    11 subsection \<open>Product Operator for Commutative Monoids\<close>
    12 
    13 subsubsection \<open>Inductive Definition of a Relation for Products over Sets\<close>
    14 
    15 text \<open>Instantiation of locale \<open>LC\<close> of theory \<open>Finite_Set\<close> is not
    16   possible, because here we have explicit typing rules like
    17   \<open>x \<in> carrier G\<close>.  We introduce an explicit argument for the domain
    18   \<open>D\<close>.\<close>
    19 
    20 inductive_set
    21   foldSetD :: "['a set, 'b \<Rightarrow> 'a \<Rightarrow> 'a, 'a] \<Rightarrow> ('b set * 'a) set"
    22   for D :: "'a set" and f :: "'b \<Rightarrow> 'a \<Rightarrow> 'a" and e :: 'a
    23   where
    24     emptyI [intro]: "e \<in> D \<Longrightarrow> ({}, e) \<in> foldSetD D f e"
    25   | insertI [intro]: "\<lbrakk>x \<notin> A; f x y \<in> D; (A, y) \<in> foldSetD D f e\<rbrakk> \<Longrightarrow>
    26                       (insert x A, f x y) \<in> foldSetD D f e"
    27 
    28 inductive_cases empty_foldSetDE [elim!]: "({}, x) \<in> foldSetD D f e"
    29 
    30 definition
    31   foldD :: "['a set, 'b \<Rightarrow> 'a \<Rightarrow> 'a, 'a, 'b set] \<Rightarrow> 'a"
    32   where "foldD D f e A = (THE x. (A, x) \<in> foldSetD D f e)"
    33 
    34 lemma foldSetD_closed:
    35   "\<lbrakk>(A, z) \<in> foldSetD D f e; e \<in> D; \<And>x y. \<lbrakk>x \<in> A; y \<in> D\<rbrakk> \<Longrightarrow> f x y \<in> D\<rbrakk>
    36     \<Longrightarrow> z \<in> D"
    37   by (erule foldSetD.cases) auto
    38 
    39 lemma Diff1_foldSetD:
    40   "\<lbrakk>(A - {x}, y) \<in> foldSetD D f e; x \<in> A; f x y \<in> D\<rbrakk> \<Longrightarrow>
    41    (A, f x y) \<in> foldSetD D f e"
    42   by (metis Diff_insert_absorb foldSetD.insertI mk_disjoint_insert)
    43 
    44 lemma foldSetD_imp_finite [simp]: "(A, x) \<in> foldSetD D f e \<Longrightarrow> finite A"
    45   by (induct set: foldSetD) auto
    46 
    47 lemma finite_imp_foldSetD:
    48   "\<lbrakk>finite A; e \<in> D; \<And>x y. \<lbrakk>x \<in> A; y \<in> D\<rbrakk> \<Longrightarrow> f x y \<in> D\<rbrakk>
    49     \<Longrightarrow> \<exists>x. (A, x) \<in> foldSetD D f e"
    50 proof (induct set: finite)
    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
    60 
    61 
    62 text \<open>Left-Commutative Operations\<close>
    63 
    64 locale LCD =
    65   fixes B :: "'b set"
    66   and D :: "'a set"
    67   and f :: "'b \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)
    68   assumes left_commute:
    69     "\<lbrakk>x \<in> B; y \<in> B; z \<in> D\<rbrakk> \<Longrightarrow> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
    70   and f_closed [simp, intro!]: "!!x y. \<lbrakk>x \<in> B; y \<in> D\<rbrakk> \<Longrightarrow> f x y \<in> D"
    71 
    72 lemma (in LCD) foldSetD_closed [dest]: "(A, z) \<in> foldSetD D f e \<Longrightarrow> z \<in> D"
    73   by (erule foldSetD.cases) auto
    74 
    75 lemma (in LCD) Diff1_foldSetD:
    76   "\<lbrakk>(A - {x}, y) \<in> foldSetD D f e; x \<in> A; A \<subseteq> B\<rbrakk> \<Longrightarrow>
    77   (A, f x y) \<in> foldSetD D f e"
    78   by (meson Diff1_foldSetD f_closed local.foldSetD_closed subsetCE)
    79 
    80 lemma (in LCD) finite_imp_foldSetD:
    81   "\<lbrakk>finite A; A \<subseteq> B; e \<in> D\<rbrakk> \<Longrightarrow> \<exists>x. (A, x) \<in> foldSetD D f e"
    82 proof (induct set: finite)
    83   case empty then show ?case by auto
    84 next
    85   case (insert x F)
    86   then obtain y where y: "(F, y) \<in> foldSetD D f e" by auto
    87   with insert have "y \<in> D" by auto
    88   with y and insert have "(insert x F, f x y) \<in> foldSetD D f e"
    89     by (intro foldSetD.intros) auto
    90   then show ?case ..
    91 qed
    92 
    93 
    94 lemma (in LCD) foldSetD_determ_aux:
    95   assumes "e \<in> D" and A: "card A < n" "A \<subseteq> B" "(A, x) \<in> foldSetD D f e" "(A, y) \<in> foldSetD D f e"
    96   shows "y = x"
    97   using A
    98 proof (induction n arbitrary: A x y)
    99   case 0
   100   then show ?case
   101     by auto
   102 next
   103   case (Suc n)
   104   then consider "card A = n" | "card A < n"
   105     by linarith
   106   then show ?case
   107   proof cases
   108     case 1
   109     show ?thesis
   110       using foldSetD.cases [OF \<open>(A,x) \<in> foldSetD D (\<cdot>) e\<close>]
   111     proof cases
   112       case 1
   113       then show ?thesis
   114         using \<open>(A,y) \<in> foldSetD D (\<cdot>) e\<close> by auto
   115     next
   116       case (2 x' A' y')
   117       note A' = this
   118       show ?thesis
   119         using foldSetD.cases [OF \<open>(A,y) \<in> foldSetD D (\<cdot>) e\<close>]
   120       proof cases
   121         case 1
   122         then show ?thesis
   123           using \<open>(A,x) \<in> foldSetD D (\<cdot>) e\<close> by auto
   124       next
   125         case (2 x'' A'' y'')
   126         note A'' = this
   127         show ?thesis
   128         proof (cases "x' = x''")
   129           case True
   130           show ?thesis
   131           proof (cases "y' = y''")
   132             case True
   133             then show ?thesis
   134               using A' A'' \<open>x' = x''\<close> by (blast elim!: equalityE)
   135           next
   136             case False
   137             then show ?thesis
   138               using A' A'' \<open>x' = x''\<close> 
   139               by (metis \<open>card A = n\<close> Suc.IH Suc.prems(2) card_insert_disjoint foldSetD_imp_finite insert_eq_iff insert_subset lessI)
   140           qed
   141         next
   142           case False
   143           then have *: "A' - {x''} = A'' - {x'}" "x'' \<in> A'" "x' \<in> A''"
   144             using A' A'' by fastforce+
   145           then have "A' = insert x'' A'' - {x'}"
   146             using \<open>x' \<notin> A'\<close> by blast
   147           then have card: "card A' \<le> card A''"
   148             using A' A'' * by (metis card_Suc_Diff1 eq_refl foldSetD_imp_finite)
   149           obtain u where u: "(A' - {x''}, u) \<in> foldSetD D (\<cdot>) e"
   150             using finite_imp_foldSetD [of "A' - {x''}"] A' Diff_insert \<open>A \<subseteq> B\<close> \<open>e \<in> D\<close> by fastforce
   151           have "y' = f x'' u"
   152             using Diff1_foldSetD [OF u] \<open>x'' \<in> A'\<close> \<open>card A = n\<close> A' Suc.IH \<open>A \<subseteq> B\<close> by auto
   153           then have "(A'' - {x'}, u) \<in> foldSetD D f e"
   154             using "*"(1) u by auto
   155           then have "y'' = f x' u"
   156             using A'' by (metis * \<open>card A = n\<close> A'(1) Diff1_foldSetD Suc.IH \<open>A \<subseteq> B\<close>
   157                 card card_Suc_Diff1 card_insert_disjoint foldSetD_imp_finite insert_subset le_imp_less_Suc)
   158           then show ?thesis
   159             using A' A''
   160             by (metis \<open>A \<subseteq> B\<close> \<open>y' = x'' \<cdot> u\<close> insert_subset left_commute local.foldSetD_closed u)
   161         qed   
   162       qed
   163     qed
   164   next
   165     case 2 with Suc show ?thesis by blast
   166   qed
   167 qed
   168 
   169 lemma (in LCD) foldSetD_determ:
   170   "\<lbrakk>(A, x) \<in> foldSetD D f e; (A, y) \<in> foldSetD D f e; e \<in> D; A \<subseteq> B\<rbrakk>
   171   \<Longrightarrow> y = x"
   172   by (blast intro: foldSetD_determ_aux [rule_format])
   173 
   174 lemma (in LCD) foldD_equality:
   175   "\<lbrakk>(A, y) \<in> foldSetD D f e; e \<in> D; A \<subseteq> B\<rbrakk> \<Longrightarrow> foldD D f e A = y"
   176   by (unfold foldD_def) (blast intro: foldSetD_determ)
   177 
   178 lemma foldD_empty [simp]:
   179   "e \<in> D \<Longrightarrow> foldD D f e {} = e"
   180   by (unfold foldD_def) blast
   181 
   182 lemma (in LCD) foldD_insert_aux:
   183   "\<lbrakk>x \<notin> A; x \<in> B; e \<in> D; A \<subseteq> B\<rbrakk>
   184     \<Longrightarrow> ((insert x A, v) \<in> foldSetD D f e) \<longleftrightarrow> (\<exists>y. (A, y) \<in> foldSetD D f e \<and> v = f x y)"
   185   apply auto
   186   by (metis Diff_insert_absorb f_closed finite_Diff foldSetD.insertI foldSetD_determ foldSetD_imp_finite insert_subset local.finite_imp_foldSetD local.foldSetD_closed)
   187 
   188 lemma (in LCD) foldD_insert:
   189   assumes "finite A" "x \<notin> A" "x \<in> B" "e \<in> D" "A \<subseteq> B"
   190   shows "foldD D f e (insert x A) = f x (foldD D f e A)"
   191 proof -
   192   have "(THE v. \<exists>y. (A, y) \<in> foldSetD D (\<cdot>) e \<and> v = x \<cdot> y) = x \<cdot> (THE y. (A, y) \<in> foldSetD D (\<cdot>) e)"
   193     by (rule the_equality) (use assms foldD_def foldD_equality foldD_def finite_imp_foldSetD in \<open>metis+\<close>)
   194   then show ?thesis
   195     unfolding foldD_def using assms by (simp add: foldD_insert_aux)
   196 qed
   197 
   198 lemma (in LCD) foldD_closed [simp]:
   199   "\<lbrakk>finite A; e \<in> D; A \<subseteq> B\<rbrakk> \<Longrightarrow> foldD D f e A \<in> D"
   200 proof (induct set: finite)
   201   case empty then show ?case by simp
   202 next
   203   case insert then show ?case by (simp add: foldD_insert)
   204 qed
   205 
   206 lemma (in LCD) foldD_commute:
   207   "\<lbrakk>finite A; x \<in> B; e \<in> D; A \<subseteq> B\<rbrakk> \<Longrightarrow>
   208    f x (foldD D f e A) = foldD D f (f x e) A"
   209   by (induct set: finite) (auto simp add: left_commute foldD_insert)
   210 
   211 lemma Int_mono2:
   212   "\<lbrakk>A \<subseteq> C; B \<subseteq> C\<rbrakk> \<Longrightarrow> A Int B \<subseteq> C"
   213   by blast
   214 
   215 lemma (in LCD) foldD_nest_Un_Int:
   216   "\<lbrakk>finite A; finite C; e \<in> D; A \<subseteq> B; C \<subseteq> B\<rbrakk> \<Longrightarrow>
   217    foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
   218 proof (induction set: finite)
   219   case (insert x F)
   220   then show ?case 
   221     by (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb Int_mono2)
   222 qed simp
   223 
   224 lemma (in LCD) foldD_nest_Un_disjoint:
   225   "\<lbrakk>finite A; finite B; A Int B = {}; e \<in> D; A \<subseteq> B; C \<subseteq> B\<rbrakk>
   226     \<Longrightarrow> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
   227   by (simp add: foldD_nest_Un_Int)
   228 
   229 \<comment> \<open>Delete rules to do with \<open>foldSetD\<close> relation.\<close>
   230 
   231 declare foldSetD_imp_finite [simp del]
   232   empty_foldSetDE [rule del]
   233   foldSetD.intros [rule del]
   234 declare (in LCD)
   235   foldSetD_closed [rule del]
   236 
   237 
   238 text \<open>Commutative Monoids\<close>
   239 
   240 text \<open>
   241   We enter a more restrictive context, with \<open>f :: 'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   242   instead of \<open>'b \<Rightarrow> 'a \<Rightarrow> 'a\<close>.
   243 \<close>
   244 
   245 locale ACeD =
   246   fixes D :: "'a set"
   247     and f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)
   248     and e :: 'a
   249   assumes ident [simp]: "x \<in> D \<Longrightarrow> x \<cdot> e = x"
   250     and commute: "\<lbrakk>x \<in> D; y \<in> D\<rbrakk> \<Longrightarrow> x \<cdot> y = y \<cdot> x"
   251     and assoc: "\<lbrakk>x \<in> D; y \<in> D; z \<in> D\<rbrakk> \<Longrightarrow> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   252     and e_closed [simp]: "e \<in> D"
   253     and f_closed [simp]: "\<lbrakk>x \<in> D; y \<in> D\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> D"
   254 
   255 lemma (in ACeD) left_commute:
   256   "\<lbrakk>x \<in> D; y \<in> D; z \<in> D\<rbrakk> \<Longrightarrow> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   257 proof -
   258   assume D: "x \<in> D" "y \<in> D" "z \<in> D"
   259   then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute)
   260   also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc)
   261   also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute)
   262   finally show ?thesis .
   263 qed
   264 
   265 lemmas (in ACeD) AC = assoc commute left_commute
   266 
   267 lemma (in ACeD) left_ident [simp]: "x \<in> D \<Longrightarrow> e \<cdot> x = x"
   268 proof -
   269   assume "x \<in> D"
   270   then have "x \<cdot> e = x" by (rule ident)
   271   with \<open>x \<in> D\<close> show ?thesis by (simp add: commute)
   272 qed
   273 
   274 lemma (in ACeD) foldD_Un_Int:
   275   "\<lbrakk>finite A; finite B; A \<subseteq> D; B \<subseteq> D\<rbrakk> \<Longrightarrow>
   276     foldD D f e A \<cdot> foldD D f e B =
   277     foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)"
   278 proof (induction set: finite)
   279   case empty
   280   then show ?case 
   281     by(simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
   282 next
   283   case (insert x F)
   284   then show ?case
   285     by(simp add: AC insert_absorb Int_insert_left Int_mono2
   286                  LCD.foldD_insert [OF LCD.intro [of D]]
   287                  LCD.foldD_closed [OF LCD.intro [of D]])
   288 qed
   289 
   290 lemma (in ACeD) foldD_Un_disjoint:
   291   "\<lbrakk>finite A; finite B; A Int B = {}; A \<subseteq> D; B \<subseteq> D\<rbrakk> \<Longrightarrow>
   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]])
   295 
   296 
   297 subsubsection \<open>Products over Finite Sets\<close>
   298 
   299 definition
   300   finprod :: "[('b, 'm) monoid_scheme, 'a \<Rightarrow> 'b, 'a set] \<Rightarrow> 'b"
   301   where "finprod G f A =
   302    (if finite A
   303     then foldD (carrier G) (mult G \<circ> f) \<one>\<^bsub>G\<^esub> A
   304     else \<one>\<^bsub>G\<^esub>)"
   305 
   306 syntax
   307   "_finprod" :: "index \<Rightarrow> idt \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"
   308       ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
   309 translations
   310   "\<Otimes>\<^bsub>G\<^esub>i\<in>A. b" \<rightleftharpoons> "CONST finprod G (%i. b) A"
   311   \<comment> \<open>Beware of argument permutation!\<close>
   312 
   313 lemma (in comm_monoid) finprod_empty [simp]:
   314   "finprod G f {} = \<one>"
   315   by (simp add: finprod_def)
   316 
   317 lemma (in comm_monoid) finprod_infinite[simp]:
   318   "\<not> finite A \<Longrightarrow> finprod G f A = \<one>"
   319   by (simp add: finprod_def)
   320 
   321 declare funcsetI [intro]
   322   funcset_mem [dest]
   323 
   324 context comm_monoid begin
   325 
   326 lemma finprod_insert [simp]:
   327   assumes "finite F" "a \<notin> F" "f \<in> F \<rightarrow> carrier G" "f a \<in> carrier G"
   328   shows "finprod G f (insert a F) = f a \<otimes> finprod G f F"
   329 proof -
   330   have "finprod G f (insert a F) = foldD (carrier G) ((\<otimes>) \<circ> f) \<one> (insert a F)"
   331     by (simp add: finprod_def assms)
   332   also have "... = ((\<otimes>) \<circ> f) a (foldD (carrier G) ((\<otimes>) \<circ> f) \<one> F)"
   333     by (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
   334       (use assms in \<open>auto simp: m_lcomm Pi_iff\<close>)
   335   also have "... = f a \<otimes> finprod G f F"
   336     using \<open>finite F\<close> by (auto simp add: finprod_def)
   337   finally show ?thesis .
   338 qed
   339 
   340 lemma finprod_one_eqI: "(\<And>x. x \<in> A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
   341 proof (induct A rule: infinite_finite_induct)
   342   case empty show ?case by simp
   343 next
   344   case (insert a A)
   345   have "(\<lambda>i. \<one>) \<in> A \<rightarrow> carrier G" by auto
   346   with insert show ?case by simp
   347 qed simp
   348 
   349 lemma finprod_one [simp]: "(\<Otimes>i\<in>A. \<one>) = \<one>"
   350   by (simp add: finprod_one_eqI)
   351 
   352 lemma finprod_closed [simp]:
   353   fixes A
   354   assumes f: "f \<in> A \<rightarrow> carrier G"
   355   shows "finprod G f A \<in> carrier G"
   356 using f
   357 proof (induct A rule: infinite_finite_induct)
   358   case empty show ?case by simp
   359 next
   360   case (insert a A)
   361   then have a: "f a \<in> carrier G" by fast
   362   from insert have A: "f \<in> A \<rightarrow> carrier G" by fast
   363   from insert A a show ?case by simp
   364 qed simp
   365 
   366 lemma funcset_Int_left [simp, intro]:
   367   "\<lbrakk>f \<in> A \<rightarrow> C; f \<in> B \<rightarrow> C\<rbrakk> \<Longrightarrow> f \<in> A Int B \<rightarrow> C"
   368   by fast
   369 
   370 lemma funcset_Un_left [iff]:
   371   "(f \<in> A Un B \<rightarrow> C) = (f \<in> A \<rightarrow> C \<and> f \<in> B \<rightarrow> C)"
   372   by fast
   373 
   374 lemma finprod_Un_Int:
   375   "\<lbrakk>finite A; finite B; g \<in> A \<rightarrow> carrier G; g \<in> B \<rightarrow> carrier G\<rbrakk> \<Longrightarrow>
   376      finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
   377      finprod G g A \<otimes> finprod G g B"
   378 \<comment> \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
   379 proof (induct set: finite)
   380   case empty then show ?case by simp
   381 next
   382   case (insert a A)
   383   then have a: "g a \<in> carrier G" by fast
   384   from insert have A: "g \<in> A \<rightarrow> carrier G" by fast
   385   from insert A a show ?case
   386     by (simp add: m_ac Int_insert_left insert_absorb Int_mono2)
   387 qed
   388 
   389 lemma finprod_Un_disjoint:
   390   "\<lbrakk>finite A; finite B; A Int B = {};
   391       g \<in> A \<rightarrow> carrier G; g \<in> B \<rightarrow> carrier G\<rbrakk>
   392    \<Longrightarrow> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
   393   by (metis Pi_split_domain finprod_Un_Int finprod_closed finprod_empty r_one)
   394 
   395 lemma finprod_multf:
   396   "\<lbrakk>f \<in> A \<rightarrow> carrier G; g \<in> A \<rightarrow> carrier G\<rbrakk> \<Longrightarrow>
   397    finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
   398 proof (induct A rule: infinite_finite_induct)
   399   case empty show ?case by simp
   400 next
   401   case (insert a A) then
   402   have fA: "f \<in> A \<rightarrow> carrier G" by fast
   403   from insert have fa: "f a \<in> carrier G" by fast
   404   from insert have gA: "g \<in> A \<rightarrow> carrier G" by fast
   405   from insert have ga: "g a \<in> carrier G" by fast
   406   from insert have fgA: "(%x. f x \<otimes> g x) \<in> A \<rightarrow> carrier G"
   407     by (simp add: Pi_def)
   408   show ?case
   409     by (simp add: insert fA fa gA ga fgA m_ac)
   410 qed simp
   411 
   412 lemma finprod_cong':
   413   "\<lbrakk>A = B; g \<in> B \<rightarrow> carrier G;
   414       !!i. i \<in> B \<Longrightarrow> f i = g i\<rbrakk> \<Longrightarrow> finprod G f A = finprod G g B"
   415 proof -
   416   assume prems: "A = B" "g \<in> B \<rightarrow> carrier G"
   417     "!!i. i \<in> B \<Longrightarrow> f i = g i"
   418   show ?thesis
   419   proof (cases "finite B")
   420     case True
   421     then have "!!A. \<lbrakk>A = B; g \<in> B \<rightarrow> carrier G;
   422       !!i. i \<in> B \<Longrightarrow> f i = g i\<rbrakk> \<Longrightarrow> finprod G f A = finprod G g B"
   423     proof induct
   424       case empty thus ?case by simp
   425     next
   426       case (insert x B)
   427       then have "finprod G f A = finprod G f (insert x B)" by simp
   428       also from insert have "... = f x \<otimes> finprod G f B"
   429       proof (intro finprod_insert)
   430         show "finite B" by fact
   431       next
   432         show "x \<notin> B" by fact
   433       next
   434         assume "x \<notin> B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   435           "g \<in> insert x B \<rightarrow> carrier G"
   436         thus "f \<in> B \<rightarrow> carrier G" by fastforce
   437       next
   438         assume "x \<notin> B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   439           "g \<in> insert x B \<rightarrow> carrier G"
   440         thus "f x \<in> carrier G" by fastforce
   441       qed
   442       also from insert have "... = g x \<otimes> finprod G g B" by fastforce
   443       also from insert have "... = finprod G g (insert x B)"
   444       by (intro finprod_insert [THEN sym]) auto
   445       finally show ?case .
   446     qed
   447     with prems show ?thesis by simp
   448   next
   449     case False with prems show ?thesis by simp
   450   qed
   451 qed
   452 
   453 lemma finprod_cong:
   454   "\<lbrakk>A = B; f \<in> B \<rightarrow> carrier G = True;
   455       \<And>i. i \<in> B =simp=> f i = g i\<rbrakk> \<Longrightarrow> finprod G f A = finprod G g B"
   456   (* This order of prems is slightly faster (3%) than the last two swapped. *)
   457   by (rule finprod_cong') (auto simp add: simp_implies_def)
   458 
   459 text \<open>Usually, if this rule causes a failed congruence proof error,
   460   the reason is that the premise \<open>g \<in> B \<rightarrow> carrier G\<close> cannot be shown.
   461   Adding @{thm [source] Pi_def} to the simpset is often useful.
   462   For this reason, @{thm [source] finprod_cong}
   463   is not added to the simpset by default.
   464 \<close>
   465 
   466 end
   467 
   468 declare funcsetI [rule del]
   469   funcset_mem [rule del]
   470 
   471 context comm_monoid begin
   472 
   473 lemma finprod_0 [simp]:
   474   "f \<in> {0::nat} \<rightarrow> carrier G \<Longrightarrow> finprod G f {..0} = f 0"
   475 by (simp add: Pi_def)
   476 
   477 lemma finprod_Suc [simp]:
   478   "f \<in> {..Suc n} \<rightarrow> carrier G \<Longrightarrow>
   479    finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})"
   480 by (simp add: Pi_def atMost_Suc)
   481 
   482 lemma finprod_Suc2:
   483   "f \<in> {..Suc n} \<rightarrow> carrier G \<Longrightarrow>
   484    finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)"
   485 proof (induct n)
   486   case 0 thus ?case by (simp add: Pi_def)
   487 next
   488   case Suc thus ?case by (simp add: m_assoc Pi_def)
   489 qed
   490 
   491 lemma finprod_mult [simp]:
   492   "\<lbrakk>f \<in> {..n} \<rightarrow> carrier G; g \<in> {..n} \<rightarrow> carrier G\<rbrakk> \<Longrightarrow>
   493      finprod G (%i. f i \<otimes> g i) {..n::nat} =
   494      finprod G f {..n} \<otimes> finprod G g {..n}"
   495   by (induct n) (simp_all add: m_ac Pi_def)
   496 
   497 (* The following two were contributed by Jeremy Avigad. *)
   498 
   499 lemma finprod_reindex:
   500   "f \<in> (h ` A) \<rightarrow> carrier G \<Longrightarrow>
   501         inj_on h A \<Longrightarrow> finprod G f (h ` A) = finprod G (\<lambda>x. f (h x)) A"
   502 proof (induct A rule: infinite_finite_induct)
   503   case (infinite A)
   504   hence "\<not> finite (h ` A)"
   505     using finite_imageD by blast
   506   with \<open>\<not> finite A\<close> show ?case by simp
   507 qed (auto simp add: Pi_def)
   508 
   509 lemma finprod_const:
   510   assumes a [simp]: "a \<in> carrier G"
   511     shows "finprod G (\<lambda>x. a) A = a [^] card A"
   512 proof (induct A rule: infinite_finite_induct)
   513   case (insert b A)
   514   show ?case
   515   proof (subst finprod_insert[OF insert(1-2)])
   516     show "a \<otimes> (\<Otimes>x\<in>A. a) = a [^] card (insert b A)"
   517       by (insert insert, auto, subst m_comm, auto)
   518   qed auto
   519 qed auto
   520 
   521 (* The following lemma was contributed by Jesus Aransay. *)
   522 
   523 lemma finprod_singleton:
   524   assumes i_in_A: "i \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> carrier G"
   525   shows "(\<Otimes>j\<in>A. if i = j then f j else \<one>) = f i"
   526   using i_in_A finprod_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<one>)"]
   527     fin_A f_Pi finprod_one [of "A - {i}"]
   528     finprod_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"]
   529   unfolding Pi_def simp_implies_def by (force simp add: insert_absorb)
   530 
   531 end
   532 
   533 (* Jeremy Avigad. This should be generalized to arbitrary groups, not just commutative
   534    ones, using Lagrange's theorem. *)
   535 
   536 lemma (in comm_group) power_order_eq_one:
   537   assumes fin [simp]: "finite (carrier G)"
   538     and a [simp]: "a \<in> carrier G"
   539   shows "a [^] card(carrier G) = one G"
   540 proof -
   541   have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
   542     by (subst (2) finprod_reindex [symmetric],
   543       auto simp add: Pi_def inj_on_cmult surj_const_mult)
   544   also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
   545     by (auto simp add: finprod_multf Pi_def)
   546   also have "(\<Otimes>x\<in>carrier G. a) = a [^] card(carrier G)"
   547     by (auto simp add: finprod_const)
   548   finally show ?thesis
   549 (* uses the preceeding lemma *)
   550     by auto
   551 qed
   552 
   553 lemma (in comm_monoid) finprod_UN_disjoint:
   554   assumes
   555     "finite I" "\<And>i. i \<in> I \<Longrightarrow> finite (A i)" "pairwise (\<lambda>i j. disjnt (A i) (A j)) I"
   556     "\<And>i x. i \<in> I \<Longrightarrow> x \<in> A i \<Longrightarrow> g x \<in> carrier G"
   557 shows "finprod G g (UNION I A) = finprod G (\<lambda>i. finprod G g (A i)) I"
   558   using assms
   559 proof (induction set: finite)
   560   case empty
   561   then show ?case
   562     by force
   563 next
   564   case (insert i I)
   565   then show ?case
   566     unfolding pairwise_def disjnt_def
   567     apply clarsimp
   568     apply (subst finprod_Un_disjoint)
   569          apply (fastforce intro!: funcsetI finprod_closed)+
   570     done
   571 qed
   572 
   573 lemma (in comm_monoid) finprod_Union_disjoint:
   574   "\<lbrakk>finite C; \<And>A. A \<in> C \<Longrightarrow> finite A \<and> (\<forall>x\<in>A. f x \<in> carrier G); pairwise disjnt C\<rbrakk> \<Longrightarrow>
   575     finprod G f (\<Union>C) = finprod G (finprod G f) C"
   576   apply (frule finprod_UN_disjoint [of C id f])
   577   apply auto
   578   done
   579 
   580 end