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