src/HOL/Library/Groups_Big_Fun.thy
author wenzelm
Wed Mar 08 10:50:59 2017 +0100 (2017-03-08)
changeset 65151 a7394aa4d21c
parent 64272 f76b6dda2e56
child 66804 3f9bb52082c4
permissions -rw-r--r--
tuned proofs;
haftmann@58197
     1
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@58197
     2
wenzelm@58881
     3
section \<open>Big sum and product over function bodies\<close>
haftmann@58197
     4
haftmann@58197
     5
theory Groups_Big_Fun
haftmann@58197
     6
imports
haftmann@58197
     7
  Main
haftmann@58197
     8
begin
haftmann@58197
     9
haftmann@58197
    10
subsection \<open>Abstract product\<close>
haftmann@58197
    11
haftmann@58197
    12
locale comm_monoid_fun = comm_monoid
haftmann@58197
    13
begin
haftmann@58197
    14
haftmann@58197
    15
definition G :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
haftmann@58197
    16
where
haftmann@63290
    17
  expand_set: "G g = comm_monoid_set.F f \<^bold>1 g {a. g a \<noteq> \<^bold>1}"
haftmann@58197
    18
haftmann@63290
    19
interpretation F: comm_monoid_set f "\<^bold>1"
haftmann@58197
    20
  ..
haftmann@58197
    21
haftmann@58197
    22
lemma expand_superset:
haftmann@63290
    23
  assumes "finite A" and "{a. g a \<noteq> \<^bold>1} \<subseteq> A"
haftmann@58197
    24
  shows "G g = F.F g A"
haftmann@58197
    25
  apply (simp add: expand_set)
haftmann@58197
    26
  apply (rule F.same_carrierI [of A])
haftmann@58197
    27
  apply (simp_all add: assms)
haftmann@58197
    28
  done
haftmann@58197
    29
haftmann@58197
    30
lemma conditionalize:
haftmann@58197
    31
  assumes "finite A"
haftmann@63290
    32
  shows "F.F g A = G (\<lambda>a. if a \<in> A then g a else \<^bold>1)"
haftmann@58197
    33
  using assms
haftmann@58197
    34
  apply (simp add: expand_set)
haftmann@58197
    35
  apply (rule F.same_carrierI [of A])
haftmann@58197
    36
  apply auto
haftmann@58197
    37
  done
haftmann@58197
    38
haftmann@58197
    39
lemma neutral [simp]:
haftmann@63290
    40
  "G (\<lambda>a. \<^bold>1) = \<^bold>1"
haftmann@58197
    41
  by (simp add: expand_set)
haftmann@58197
    42
haftmann@58197
    43
lemma update [simp]:
haftmann@63290
    44
  assumes "finite {a. g a \<noteq> \<^bold>1}"
haftmann@63290
    45
  assumes "g a = \<^bold>1"
haftmann@63290
    46
  shows "G (g(a := b)) = b \<^bold>* G g"
haftmann@63290
    47
proof (cases "b = \<^bold>1")
haftmann@63290
    48
  case True with \<open>g a = \<^bold>1\<close> show ?thesis
haftmann@58197
    49
    by (simp add: expand_set) (rule F.cong, auto)
haftmann@58197
    50
next
haftmann@58197
    51
  case False
haftmann@63290
    52
  moreover have "{a'. a' \<noteq> a \<longrightarrow> g a' \<noteq> \<^bold>1} = insert a {a. g a \<noteq> \<^bold>1}"
haftmann@58197
    53
    by auto
haftmann@63290
    54
  moreover from \<open>g a = \<^bold>1\<close> have "a \<notin> {a. g a \<noteq> \<^bold>1}"
haftmann@58197
    55
    by simp
haftmann@63290
    56
  moreover have "F.F (\<lambda>a'. if a' = a then b else g a') {a. g a \<noteq> \<^bold>1} = F.F g {a. g a \<noteq> \<^bold>1}"
haftmann@63290
    57
    by (rule F.cong) (auto simp add: \<open>g a = \<^bold>1\<close>)
haftmann@63290
    58
  ultimately show ?thesis using \<open>finite {a. g a \<noteq> \<^bold>1}\<close> by (simp add: expand_set)
haftmann@58197
    59
qed
haftmann@58197
    60
haftmann@58197
    61
lemma infinite [simp]:
haftmann@63290
    62
  "\<not> finite {a. g a \<noteq> \<^bold>1} \<Longrightarrow> G g = \<^bold>1"
haftmann@58197
    63
  by (simp add: expand_set)
haftmann@58197
    64
haftmann@58197
    65
lemma cong:
haftmann@58197
    66
  assumes "\<And>a. g a = h a"
haftmann@58197
    67
  shows "G g = G h"
haftmann@58197
    68
  using assms by (simp add: expand_set)
haftmann@58197
    69
haftmann@58197
    70
lemma strong_cong [cong]:
haftmann@58197
    71
  assumes "\<And>a. g a = h a"
haftmann@58197
    72
  shows "G (\<lambda>a. g a) = G (\<lambda>a. h a)"
haftmann@58197
    73
  using assms by (fact cong)
haftmann@58197
    74
haftmann@58197
    75
lemma not_neutral_obtains_not_neutral:
haftmann@63290
    76
  assumes "G g \<noteq> \<^bold>1"
haftmann@63290
    77
  obtains a where "g a \<noteq> \<^bold>1"
haftmann@58197
    78
  using assms by (auto elim: F.not_neutral_contains_not_neutral simp add: expand_set)
haftmann@58197
    79
haftmann@58197
    80
lemma reindex_cong:
haftmann@58197
    81
  assumes "bij l"
haftmann@58197
    82
  assumes "g \<circ> l = h"
haftmann@58197
    83
  shows "G g = G h"
haftmann@58197
    84
proof -
haftmann@58197
    85
  from assms have unfold: "h = g \<circ> l" by simp
wenzelm@60500
    86
  from \<open>bij l\<close> have "inj l" by (rule bij_is_inj)
haftmann@63290
    87
  then have "inj_on l {a. h a \<noteq> \<^bold>1}" by (rule subset_inj_on) simp
haftmann@63290
    88
  moreover from \<open>bij l\<close> have "{a. g a \<noteq> \<^bold>1} = l ` {a. h a \<noteq> \<^bold>1}"
haftmann@58197
    89
    by (auto simp add: image_Collect unfold elim: bij_pointE)
haftmann@63290
    90
  moreover have "\<And>x. x \<in> {a. h a \<noteq> \<^bold>1} \<Longrightarrow> g (l x) = h x"
haftmann@58197
    91
    by (simp add: unfold)
haftmann@63290
    92
  ultimately have "F.F g {a. g a \<noteq> \<^bold>1} = F.F h {a. h a \<noteq> \<^bold>1}"
haftmann@58197
    93
    by (rule F.reindex_cong)
haftmann@58197
    94
  then show ?thesis by (simp add: expand_set)
haftmann@58197
    95
qed
haftmann@58197
    96
haftmann@58197
    97
lemma distrib:
haftmann@63290
    98
  assumes "finite {a. g a \<noteq> \<^bold>1}" and "finite {a. h a \<noteq> \<^bold>1}"
haftmann@63290
    99
  shows "G (\<lambda>a. g a \<^bold>* h a) = G g \<^bold>* G h"
haftmann@58197
   100
proof -
haftmann@63290
   101
  from assms have "finite ({a. g a \<noteq> \<^bold>1} \<union> {a. h a \<noteq> \<^bold>1})" by simp
haftmann@63290
   102
  moreover have "{a. g a \<^bold>* h a \<noteq> \<^bold>1} \<subseteq> {a. g a \<noteq> \<^bold>1} \<union> {a. h a \<noteq> \<^bold>1}"
haftmann@58197
   103
    by auto (drule sym, simp)
haftmann@58197
   104
  ultimately show ?thesis
haftmann@58197
   105
    using assms
haftmann@63290
   106
    by (simp add: expand_superset [of "{a. g a \<noteq> \<^bold>1} \<union> {a. h a \<noteq> \<^bold>1}"] F.distrib)
haftmann@58197
   107
qed
haftmann@58197
   108
haftmann@58197
   109
lemma commute:
haftmann@58197
   110
  assumes "finite C"
haftmann@63290
   111
  assumes subset: "{a. \<exists>b. g a b \<noteq> \<^bold>1} \<times> {b. \<exists>a. g a b \<noteq> \<^bold>1} \<subseteq> C" (is "?A \<times> ?B \<subseteq> C")
haftmann@58197
   112
  shows "G (\<lambda>a. G (g a)) = G (\<lambda>b. G (\<lambda>a. g a b))"
haftmann@58197
   113
proof -
wenzelm@60500
   114
  from \<open>finite C\<close> subset
haftmann@63290
   115
    have "finite ({a. \<exists>b. g a b \<noteq> \<^bold>1} \<times> {b. \<exists>a. g a b \<noteq> \<^bold>1})"
haftmann@58197
   116
    by (rule rev_finite_subset)
haftmann@58197
   117
  then have fins:
haftmann@63290
   118
    "finite {b. \<exists>a. g a b \<noteq> \<^bold>1}" "finite {a. \<exists>b. g a b \<noteq> \<^bold>1}"
haftmann@58197
   119
    by (auto simp add: finite_cartesian_product_iff)
haftmann@63290
   120
  have subsets: "\<And>a. {b. g a b \<noteq> \<^bold>1} \<subseteq> {b. \<exists>a. g a b \<noteq> \<^bold>1}"
haftmann@63290
   121
    "\<And>b. {a. g a b \<noteq> \<^bold>1} \<subseteq> {a. \<exists>b. g a b \<noteq> \<^bold>1}"
haftmann@63290
   122
    "{a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1} \<noteq> \<^bold>1} \<subseteq> {a. \<exists>b. g a b \<noteq> \<^bold>1}"
haftmann@63290
   123
    "{a. F.F (\<lambda>aa. g aa a) {a. \<exists>b. g a b \<noteq> \<^bold>1} \<noteq> \<^bold>1} \<subseteq> {b. \<exists>a. g a b \<noteq> \<^bold>1}"
haftmann@58197
   124
    by (auto elim: F.not_neutral_contains_not_neutral)
haftmann@58197
   125
  from F.commute have
haftmann@63290
   126
    "F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1}) {a. \<exists>b. g a b \<noteq> \<^bold>1} =
haftmann@63290
   127
      F.F (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> \<^bold>1}) {b. \<exists>a. g a b \<noteq> \<^bold>1}" .
haftmann@63290
   128
  with subsets fins have "G (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1}) =
haftmann@63290
   129
    G (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> \<^bold>1})"
haftmann@63290
   130
    by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> \<^bold>1}"]
haftmann@63290
   131
      expand_superset [of "{a. \<exists>b. g a b \<noteq> \<^bold>1}"])
haftmann@58197
   132
  with subsets fins show ?thesis
haftmann@63290
   133
    by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> \<^bold>1}"]
haftmann@63290
   134
      expand_superset [of "{a. \<exists>b. g a b \<noteq> \<^bold>1}"])
haftmann@58197
   135
qed
haftmann@58197
   136
haftmann@58197
   137
lemma cartesian_product:
haftmann@58197
   138
  assumes "finite C"
haftmann@63290
   139
  assumes subset: "{a. \<exists>b. g a b \<noteq> \<^bold>1} \<times> {b. \<exists>a. g a b \<noteq> \<^bold>1} \<subseteq> C" (is "?A \<times> ?B \<subseteq> C")
haftmann@58197
   140
  shows "G (\<lambda>a. G (g a)) = G (\<lambda>(a, b). g a b)"
haftmann@58197
   141
proof -
wenzelm@60500
   142
  from subset \<open>finite C\<close> have fin_prod: "finite (?A \<times> ?B)"
haftmann@58197
   143
    by (rule finite_subset)
haftmann@58197
   144
  from fin_prod have "finite ?A" and "finite ?B"
haftmann@58197
   145
    by (auto simp add: finite_cartesian_product_iff)
haftmann@58197
   146
  have *: "G (\<lambda>a. G (g a)) =
haftmann@63290
   147
    (F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1}) {a. \<exists>b. g a b \<noteq> \<^bold>1})"
haftmann@58197
   148
    apply (subst expand_superset [of "?B"])
wenzelm@60500
   149
    apply (rule \<open>finite ?B\<close>)
haftmann@58197
   150
    apply auto
haftmann@58197
   151
    apply (subst expand_superset [of "?A"])
wenzelm@60500
   152
    apply (rule \<open>finite ?A\<close>)
haftmann@58197
   153
    apply auto
haftmann@58197
   154
    apply (erule F.not_neutral_contains_not_neutral)
haftmann@58197
   155
    apply auto
haftmann@58197
   156
    done
haftmann@63290
   157
  have "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> \<^bold>1} \<subseteq> ?A \<times> ?B"
haftmann@58197
   158
    by auto
haftmann@63290
   159
  with subset have **: "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> \<^bold>1} \<subseteq> C"
haftmann@58197
   160
    by blast
haftmann@58197
   161
  show ?thesis
haftmann@58197
   162
    apply (simp add: *)
haftmann@58197
   163
    apply (simp add: F.cartesian_product)
haftmann@58197
   164
    apply (subst expand_superset [of C])
wenzelm@60500
   165
    apply (rule \<open>finite C\<close>)
haftmann@58197
   166
    apply (simp_all add: **)
haftmann@58197
   167
    apply (rule F.same_carrierI [of C])
wenzelm@60500
   168
    apply (rule \<open>finite C\<close>)
haftmann@58197
   169
    apply (simp_all add: subset)
haftmann@58197
   170
    apply auto
haftmann@58197
   171
    done
haftmann@58197
   172
qed
haftmann@58197
   173
haftmann@58197
   174
lemma cartesian_product2:
haftmann@58197
   175
  assumes fin: "finite D"
haftmann@63290
   176
  assumes subset: "{(a, b). \<exists>c. g a b c \<noteq> \<^bold>1} \<times> {c. \<exists>a b. g a b c \<noteq> \<^bold>1} \<subseteq> D" (is "?AB \<times> ?C \<subseteq> D")
haftmann@58197
   177
  shows "G (\<lambda>(a, b). G (g a b)) = G (\<lambda>(a, b, c). g a b c)"
haftmann@58197
   178
proof -
haftmann@58197
   179
  have bij: "bij (\<lambda>(a, b, c). ((a, b), c))"
haftmann@58197
   180
    by (auto intro!: bijI injI simp add: image_def)
haftmann@63290
   181
  have "{p. \<exists>c. g (fst p) (snd p) c \<noteq> \<^bold>1} \<times> {c. \<exists>p. g (fst p) (snd p) c \<noteq> \<^bold>1} \<subseteq> D"
haftmann@61424
   182
    by auto (insert subset, blast)
haftmann@58197
   183
  with fin have "G (\<lambda>p. G (g (fst p) (snd p))) = G (\<lambda>(p, c). g (fst p) (snd p) c)"
haftmann@58197
   184
    by (rule cartesian_product)
haftmann@58197
   185
  then have "G (\<lambda>(a, b). G (g a b)) = G (\<lambda>((a, b), c). g a b c)"
haftmann@58197
   186
    by (auto simp add: split_def)
haftmann@58197
   187
  also have "G (\<lambda>((a, b), c). g a b c) = G (\<lambda>(a, b, c). g a b c)"
haftmann@58197
   188
    using bij by (rule reindex_cong [of "\<lambda>(a, b, c). ((a, b), c)"]) (simp add: fun_eq_iff)
haftmann@58197
   189
  finally show ?thesis .
haftmann@58197
   190
qed
haftmann@58197
   191
haftmann@58197
   192
lemma delta [simp]:
haftmann@63290
   193
  "G (\<lambda>b. if b = a then g b else \<^bold>1) = g a"
haftmann@58197
   194
proof -
haftmann@63290
   195
  have "{b. (if b = a then g b else \<^bold>1) \<noteq> \<^bold>1} \<subseteq> {a}" by auto
haftmann@58197
   196
  then show ?thesis by (simp add: expand_superset [of "{a}"])
haftmann@58197
   197
qed
haftmann@58197
   198
haftmann@58197
   199
lemma delta' [simp]:
haftmann@63290
   200
  "G (\<lambda>b. if a = b then g b else \<^bold>1) = g a"
haftmann@58197
   201
proof -
haftmann@63290
   202
  have "(\<lambda>b. if a = b then g b else \<^bold>1) = (\<lambda>b. if b = a then g b else \<^bold>1)"
haftmann@58197
   203
    by (simp add: fun_eq_iff)
haftmann@63290
   204
  then have "G (\<lambda>b. if a = b then g b else \<^bold>1) = G (\<lambda>b. if b = a then g b else \<^bold>1)"
haftmann@58197
   205
    by (simp cong del: strong_cong)
haftmann@58197
   206
  then show ?thesis by simp
haftmann@58197
   207
qed
haftmann@58197
   208
haftmann@58197
   209
end
haftmann@58197
   210
haftmann@58197
   211
haftmann@58197
   212
subsection \<open>Concrete sum\<close>
haftmann@58197
   213
haftmann@58197
   214
context comm_monoid_add
haftmann@58197
   215
begin
haftmann@58197
   216
haftmann@61776
   217
sublocale Sum_any: comm_monoid_fun plus 0
wenzelm@63433
   218
  defines Sum_any = Sum_any.G
nipkow@64267
   219
  rewrites "comm_monoid_set.F plus 0 = sum"
haftmann@58197
   220
proof -
haftmann@58197
   221
  show "comm_monoid_fun plus 0" ..
wenzelm@61605
   222
  then interpret Sum_any: comm_monoid_fun plus 0 .
nipkow@64267
   223
  from sum_def show "comm_monoid_set.F plus 0 = sum" by (auto intro: sym)
haftmann@58197
   224
qed
haftmann@58197
   225
haftmann@58197
   226
end
haftmann@58197
   227
wenzelm@61955
   228
syntax (ASCII)
haftmann@58197
   229
  "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3SUM _. _)" [0, 10] 10)
wenzelm@61955
   230
syntax
haftmann@58197
   231
  "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3\<Sum>_. _)" [0, 10] 10)
haftmann@58197
   232
translations
wenzelm@61955
   233
  "\<Sum>a. b" \<rightleftharpoons> "CONST Sum_any (\<lambda>a. b)"
haftmann@58197
   234
haftmann@58197
   235
lemma Sum_any_left_distrib:
haftmann@58197
   236
  fixes r :: "'a :: semiring_0"
haftmann@58197
   237
  assumes "finite {a. g a \<noteq> 0}"
haftmann@58197
   238
  shows "Sum_any g * r = (\<Sum>n. g n * r)"
haftmann@58197
   239
proof -
haftmann@58197
   240
  note assms
haftmann@58197
   241
  moreover have "{a. g a * r \<noteq> 0} \<subseteq> {a. g a \<noteq> 0}" by auto
haftmann@58197
   242
  ultimately show ?thesis
nipkow@64267
   243
    by (simp add: sum_distrib_right Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
haftmann@58197
   244
qed  
haftmann@58197
   245
haftmann@58197
   246
lemma Sum_any_right_distrib:
haftmann@58197
   247
  fixes r :: "'a :: semiring_0"
haftmann@58197
   248
  assumes "finite {a. g a \<noteq> 0}"
haftmann@58197
   249
  shows "r * Sum_any g = (\<Sum>n. r * g n)"
haftmann@58197
   250
proof -
haftmann@58197
   251
  note assms
haftmann@58197
   252
  moreover have "{a. r * g a \<noteq> 0} \<subseteq> {a. g a \<noteq> 0}" by auto
haftmann@58197
   253
  ultimately show ?thesis
nipkow@64267
   254
    by (simp add: sum_distrib_left Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
haftmann@58197
   255
qed
haftmann@58197
   256
haftmann@58197
   257
lemma Sum_any_product:
haftmann@58197
   258
  fixes f g :: "'b \<Rightarrow> 'a::semiring_0"
haftmann@58197
   259
  assumes "finite {a. f a \<noteq> 0}" and "finite {b. g b \<noteq> 0}"
haftmann@58197
   260
  shows "Sum_any f * Sum_any g = (\<Sum>a. \<Sum>b. f a * g b)"
haftmann@58197
   261
proof -
haftmann@58197
   262
  have subset_f: "{a. (\<Sum>b. f a * g b) \<noteq> 0} \<subseteq> {a. f a \<noteq> 0}"
haftmann@58197
   263
    by rule (simp, rule, auto)
haftmann@58197
   264
  moreover have subset_g: "\<And>a. {b. f a * g b \<noteq> 0} \<subseteq> {b. g b \<noteq> 0}"
haftmann@58197
   265
    by rule (simp, rule, auto)
haftmann@58197
   266
  ultimately show ?thesis using assms
haftmann@58197
   267
    by (auto simp add: Sum_any.expand_set [of f] Sum_any.expand_set [of g]
haftmann@58197
   268
      Sum_any.expand_superset [of "{a. f a \<noteq> 0}"] Sum_any.expand_superset [of "{b. g b \<noteq> 0}"]
nipkow@64267
   269
      sum_product)
haftmann@58197
   270
qed
haftmann@58197
   271
haftmann@58437
   272
lemma Sum_any_eq_zero_iff [simp]: 
haftmann@58437
   273
  fixes f :: "'a \<Rightarrow> nat"
haftmann@58437
   274
  assumes "finite {a. f a \<noteq> 0}"
haftmann@58437
   275
  shows "Sum_any f = 0 \<longleftrightarrow> f = (\<lambda>_. 0)"
haftmann@58437
   276
  using assms by (simp add: Sum_any.expand_set fun_eq_iff)
haftmann@58437
   277
haftmann@58197
   278
haftmann@58197
   279
subsection \<open>Concrete product\<close>
haftmann@58197
   280
haftmann@58197
   281
context comm_monoid_mult
haftmann@58197
   282
begin
haftmann@58197
   283
haftmann@61776
   284
sublocale Prod_any: comm_monoid_fun times 1
wenzelm@63433
   285
  defines Prod_any = Prod_any.G
nipkow@64272
   286
  rewrites "comm_monoid_set.F times 1 = prod"
haftmann@58197
   287
proof -
haftmann@58197
   288
  show "comm_monoid_fun times 1" ..
wenzelm@61605
   289
  then interpret Prod_any: comm_monoid_fun times 1 .
nipkow@64272
   290
  from prod_def show "comm_monoid_set.F times 1 = prod" by (auto intro: sym)
haftmann@58197
   291
qed
haftmann@58197
   292
haftmann@58197
   293
end
haftmann@58197
   294
wenzelm@61955
   295
syntax (ASCII)
wenzelm@61955
   296
  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3PROD _. _)" [0, 10] 10)
haftmann@58197
   297
syntax
wenzelm@61955
   298
  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3\<Prod>_. _)" [0, 10] 10)
haftmann@58197
   299
translations
haftmann@58197
   300
  "\<Prod>a. b" == "CONST Prod_any (\<lambda>a. b)"
haftmann@58197
   301
haftmann@58197
   302
lemma Prod_any_zero:
haftmann@58197
   303
  fixes f :: "'b \<Rightarrow> 'a :: comm_semiring_1"
haftmann@58197
   304
  assumes "finite {a. f a \<noteq> 1}"
haftmann@58197
   305
  assumes "f a = 0"
haftmann@58197
   306
  shows "(\<Prod>a. f a) = 0"
haftmann@58197
   307
proof -
wenzelm@60500
   308
  from \<open>f a = 0\<close> have "f a \<noteq> 1" by simp
wenzelm@60500
   309
  with \<open>f a = 0\<close> have "\<exists>a. f a \<noteq> 1 \<and> f a = 0" by blast
wenzelm@60500
   310
  with \<open>finite {a. f a \<noteq> 1}\<close> show ?thesis
nipkow@64272
   311
    by (simp add: Prod_any.expand_set prod_zero)
haftmann@58197
   312
qed
haftmann@58197
   313
haftmann@58197
   314
lemma Prod_any_not_zero:
haftmann@58197
   315
  fixes f :: "'b \<Rightarrow> 'a :: comm_semiring_1"
haftmann@58197
   316
  assumes "finite {a. f a \<noteq> 1}"
haftmann@58197
   317
  assumes "(\<Prod>a. f a) \<noteq> 0"
haftmann@58197
   318
  shows "f a \<noteq> 0"
haftmann@58197
   319
  using assms Prod_any_zero [of f] by blast
haftmann@58197
   320
haftmann@58437
   321
lemma power_Sum_any:
haftmann@58437
   322
  assumes "finite {a. f a \<noteq> 0}"
haftmann@58437
   323
  shows "c ^ (\<Sum>a. f a) = (\<Prod>a. c ^ f a)"
haftmann@58437
   324
proof -
haftmann@58437
   325
  have "{a. c ^ f a \<noteq> 1} \<subseteq> {a. f a \<noteq> 0}"
haftmann@58437
   326
    by (auto intro: ccontr)
haftmann@58437
   327
  with assms show ?thesis
nipkow@64267
   328
    by (simp add: Sum_any.expand_set Prod_any.expand_superset power_sum)
haftmann@58437
   329
qed
haftmann@58437
   330
haftmann@58197
   331
end