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