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