haftmann@58197: (* Author: Florian Haftmann, TU Muenchen *)
haftmann@58197: 
haftmann@58197: header \<open>Big sum and product over function bodies\<close>
haftmann@58197: 
haftmann@58197: theory Groups_Big_Fun
haftmann@58197: imports
haftmann@58197:   Main
haftmann@58197:   "~~/src/Tools/Permanent_Interpretation"
haftmann@58197: begin
haftmann@58197: 
haftmann@58197: subsection \<open>Abstract product\<close>
haftmann@58197: 
haftmann@58197: no_notation times (infixl "*" 70)
haftmann@58197: no_notation Groups.one ("1")
haftmann@58197: 
haftmann@58197: locale comm_monoid_fun = comm_monoid
haftmann@58197: begin
haftmann@58197: 
haftmann@58197: definition G :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
haftmann@58197: where
haftmann@58197:   expand_set: "G g = comm_monoid_set.F f 1 g {a. g a \<noteq> 1}"
haftmann@58197: 
haftmann@58197: interpretation F!: comm_monoid_set f 1
haftmann@58197:   ..
haftmann@58197: 
haftmann@58197: lemma expand_superset:
haftmann@58197:   assumes "finite A" and "{a. g a \<noteq> 1} \<subseteq> A"
haftmann@58197:   shows "G g = F.F g A"
haftmann@58197:   apply (simp add: expand_set)
haftmann@58197:   apply (rule F.same_carrierI [of A])
haftmann@58197:   apply (simp_all add: assms)
haftmann@58197:   done
haftmann@58197: 
haftmann@58197: lemma conditionalize:
haftmann@58197:   assumes "finite A"
haftmann@58197:   shows "F.F g A = G (\<lambda>a. if a \<in> A then g a else 1)"
haftmann@58197:   using assms
haftmann@58197:   apply (simp add: expand_set)
haftmann@58197:   apply (rule F.same_carrierI [of A])
haftmann@58197:   apply auto
haftmann@58197:   done
haftmann@58197: 
haftmann@58197: lemma neutral [simp]:
haftmann@58197:   "G (\<lambda>a. 1) = 1"
haftmann@58197:   by (simp add: expand_set)
haftmann@58197: 
haftmann@58197: lemma update [simp]:
haftmann@58197:   assumes "finite {a. g a \<noteq> 1}"
haftmann@58197:   assumes "g a = 1"
haftmann@58197:   shows "G (g(a := b)) = b * G g"
haftmann@58197: proof (cases "b = 1")
haftmann@58197:   case True with `g a = 1` show ?thesis
haftmann@58197:     by (simp add: expand_set) (rule F.cong, auto)
haftmann@58197: next
haftmann@58197:   case False
haftmann@58197:   moreover have "{a'. a' \<noteq> a \<longrightarrow> g a' \<noteq> 1} = insert a {a. g a \<noteq> 1}"
haftmann@58197:     by auto
haftmann@58197:   moreover from `g a = 1` have "a \<notin> {a. g a \<noteq> 1}"
haftmann@58197:     by simp
haftmann@58197:   moreover have "F.F (\<lambda>a'. if a' = a then b else g a') {a. g a \<noteq> 1} = F.F g {a. g a \<noteq> 1}"
haftmann@58197:     by (rule F.cong) (auto simp add: `g a = 1`)
haftmann@58197:   ultimately show ?thesis using `finite {a. g a \<noteq> 1}` by (simp add: expand_set)
haftmann@58197: qed
haftmann@58197: 
haftmann@58197: lemma infinite [simp]:
haftmann@58197:   "\<not> finite {a. g a \<noteq> 1} \<Longrightarrow> G g = 1"
haftmann@58197:   by (simp add: expand_set)
haftmann@58197: 
haftmann@58197: lemma cong:
haftmann@58197:   assumes "\<And>a. g a = h a"
haftmann@58197:   shows "G g = G h"
haftmann@58197:   using assms by (simp add: expand_set)
haftmann@58197: 
haftmann@58197: lemma strong_cong [cong]:
haftmann@58197:   assumes "\<And>a. g a = h a"
haftmann@58197:   shows "G (\<lambda>a. g a) = G (\<lambda>a. h a)"
haftmann@58197:   using assms by (fact cong)
haftmann@58197: 
haftmann@58197: lemma not_neutral_obtains_not_neutral:
haftmann@58197:   assumes "G g \<noteq> 1"
haftmann@58197:   obtains a where "g a \<noteq> 1"
haftmann@58197:   using assms by (auto elim: F.not_neutral_contains_not_neutral simp add: expand_set)
haftmann@58197: 
haftmann@58197: lemma reindex_cong:
haftmann@58197:   assumes "bij l"
haftmann@58197:   assumes "g \<circ> l = h"
haftmann@58197:   shows "G g = G h"
haftmann@58197: proof -
haftmann@58197:   from assms have unfold: "h = g \<circ> l" by simp
haftmann@58197:   from `bij l` have "inj l" by (rule bij_is_inj)
haftmann@58197:   then have "inj_on l {a. h a \<noteq> 1}" by (rule subset_inj_on) simp
haftmann@58197:   moreover from `bij l` have "{a. g a \<noteq> 1} = l ` {a. h a \<noteq> 1}"
haftmann@58197:     by (auto simp add: image_Collect unfold elim: bij_pointE)
haftmann@58197:   moreover have "\<And>x. x \<in> {a. h a \<noteq> 1} \<Longrightarrow> g (l x) = h x"
haftmann@58197:     by (simp add: unfold)
haftmann@58197:   ultimately have "F.F g {a. g a \<noteq> 1} = F.F h {a. h a \<noteq> 1}"
haftmann@58197:     by (rule F.reindex_cong)
haftmann@58197:   then show ?thesis by (simp add: expand_set)
haftmann@58197: qed
haftmann@58197: 
haftmann@58197: lemma distrib:
haftmann@58197:   assumes "finite {a. g a \<noteq> 1}" and "finite {a. h a \<noteq> 1}"
haftmann@58197:   shows "G (\<lambda>a. g a * h a) = G g * G h"
haftmann@58197: proof -
haftmann@58197:   from assms have "finite ({a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1})" by simp
haftmann@58197:   moreover have "{a. g a * h a \<noteq> 1} \<subseteq> {a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1}"
haftmann@58197:     by auto (drule sym, simp)
haftmann@58197:   ultimately show ?thesis
haftmann@58197:     using assms
haftmann@58197:     by (simp add: expand_superset [of "{a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1}"] F.distrib)
haftmann@58197: qed
haftmann@58197: 
haftmann@58197: lemma commute:
haftmann@58197:   assumes "finite C"
haftmann@58197:   assumes subset: "{a. \<exists>b. g a b \<noteq> 1} \<times> {b. \<exists>a. g a b \<noteq> 1} \<subseteq> C" (is "?A \<times> ?B \<subseteq> C")
haftmann@58197:   shows "G (\<lambda>a. G (g a)) = G (\<lambda>b. G (\<lambda>a. g a b))"
haftmann@58197: proof -
haftmann@58197:   from `finite C` subset
haftmann@58197:     have "finite ({a. \<exists>b. g a b \<noteq> 1} \<times> {b. \<exists>a. g a b \<noteq> 1})"
haftmann@58197:     by (rule rev_finite_subset)
haftmann@58197:   then have fins:
haftmann@58197:     "finite {b. \<exists>a. g a b \<noteq> 1}" "finite {a. \<exists>b. g a b \<noteq> 1}"
haftmann@58197:     by (auto simp add: finite_cartesian_product_iff)
haftmann@58197:   have subsets: "\<And>a. {b. g a b \<noteq> 1} \<subseteq> {b. \<exists>a. g a b \<noteq> 1}"
haftmann@58197:     "\<And>b. {a. g a b \<noteq> 1} \<subseteq> {a. \<exists>b. g a b \<noteq> 1}"
haftmann@58197:     "{a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1} \<noteq> 1} \<subseteq> {a. \<exists>b. g a b \<noteq> 1}"
haftmann@58197:     "{a. F.F (\<lambda>aa. g aa a) {a. \<exists>b. g a b \<noteq> 1} \<noteq> 1} \<subseteq> {b. \<exists>a. g a b \<noteq> 1}"
haftmann@58197:     by (auto elim: F.not_neutral_contains_not_neutral)
haftmann@58197:   from F.commute have
haftmann@58197:     "F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) {a. \<exists>b. g a b \<noteq> 1} =
haftmann@58197:       F.F (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> 1}) {b. \<exists>a. g a b \<noteq> 1}" .
haftmann@58197:   with subsets fins have "G (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) =
haftmann@58197:     G (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> 1})"
haftmann@58197:     by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> 1}"]
haftmann@58197:       expand_superset [of "{a. \<exists>b. g a b \<noteq> 1}"])
haftmann@58197:   with subsets fins show ?thesis
haftmann@58197:     by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> 1}"]
haftmann@58197:       expand_superset [of "{a. \<exists>b. g a b \<noteq> 1}"])
haftmann@58197: qed
haftmann@58197: 
haftmann@58197: lemma cartesian_product:
haftmann@58197:   assumes "finite C"
haftmann@58197:   assumes subset: "{a. \<exists>b. g a b \<noteq> 1} \<times> {b. \<exists>a. g a b \<noteq> 1} \<subseteq> C" (is "?A \<times> ?B \<subseteq> C")
haftmann@58197:   shows "G (\<lambda>a. G (g a)) = G (\<lambda>(a, b). g a b)"
haftmann@58197: proof -
haftmann@58197:   from subset `finite C` have fin_prod: "finite (?A \<times> ?B)"
haftmann@58197:     by (rule finite_subset)
haftmann@58197:   from fin_prod have "finite ?A" and "finite ?B"
haftmann@58197:     by (auto simp add: finite_cartesian_product_iff)
haftmann@58197:   have *: "G (\<lambda>a. G (g a)) =
haftmann@58197:     (F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) {a. \<exists>b. g a b \<noteq> 1})"
haftmann@58197:     apply (subst expand_superset [of "?B"])
haftmann@58197:     apply (rule `finite ?B`)
haftmann@58197:     apply auto
haftmann@58197:     apply (subst expand_superset [of "?A"])
haftmann@58197:     apply (rule `finite ?A`)
haftmann@58197:     apply auto
haftmann@58197:     apply (erule F.not_neutral_contains_not_neutral)
haftmann@58197:     apply auto
haftmann@58197:     done
haftmann@58197:   have "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> 1} \<subseteq> ?A \<times> ?B"
haftmann@58197:     by auto
haftmann@58197:   with subset have **: "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> 1} \<subseteq> C"
haftmann@58197:     by blast
haftmann@58197:   show ?thesis
haftmann@58197:     apply (simp add: *)
haftmann@58197:     apply (simp add: F.cartesian_product)
haftmann@58197:     apply (subst expand_superset [of C])
haftmann@58197:     apply (rule `finite C`)
haftmann@58197:     apply (simp_all add: **)
haftmann@58197:     apply (rule F.same_carrierI [of C])
haftmann@58197:     apply (rule `finite C`)
haftmann@58197:     apply (simp_all add: subset)
haftmann@58197:     apply auto
haftmann@58197:     done
haftmann@58197: qed
haftmann@58197: 
haftmann@58197: lemma cartesian_product2:
haftmann@58197:   assumes fin: "finite D"
haftmann@58197:   assumes subset: "{(a, b). \<exists>c. g a b c \<noteq> 1} \<times> {c. \<exists>a b. g a b c \<noteq> 1} \<subseteq> D" (is "?AB \<times> ?C \<subseteq> D")
haftmann@58197:   shows "G (\<lambda>(a, b). G (g a b)) = G (\<lambda>(a, b, c). g a b c)"
haftmann@58197: proof -
haftmann@58197:   have bij: "bij (\<lambda>(a, b, c). ((a, b), c))"
haftmann@58197:     by (auto intro!: bijI injI simp add: image_def)
haftmann@58197:   have "{p. \<exists>c. g (fst p) (snd p) c \<noteq> 1} \<times> {c. \<exists>p. g (fst p) (snd p) c \<noteq> 1} \<subseteq> D"
haftmann@58197:     by auto (insert subset, auto)
haftmann@58197:   with fin have "G (\<lambda>p. G (g (fst p) (snd p))) = G (\<lambda>(p, c). g (fst p) (snd p) c)"
haftmann@58197:     by (rule cartesian_product)
haftmann@58197:   then have "G (\<lambda>(a, b). G (g a b)) = G (\<lambda>((a, b), c). g a b c)"
haftmann@58197:     by (auto simp add: split_def)
haftmann@58197:   also have "G (\<lambda>((a, b), c). g a b c) = G (\<lambda>(a, b, c). g a b c)"
haftmann@58197:     using bij by (rule reindex_cong [of "\<lambda>(a, b, c). ((a, b), c)"]) (simp add: fun_eq_iff)
haftmann@58197:   finally show ?thesis .
haftmann@58197: qed
haftmann@58197: 
haftmann@58197: lemma delta [simp]:
haftmann@58197:   "G (\<lambda>b. if b = a then g b else 1) = g a"
haftmann@58197: proof -
haftmann@58197:   have "{b. (if b = a then g b else 1) \<noteq> 1} \<subseteq> {a}" by auto
haftmann@58197:   then show ?thesis by (simp add: expand_superset [of "{a}"])
haftmann@58197: qed
haftmann@58197: 
haftmann@58197: lemma delta' [simp]:
haftmann@58197:   "G (\<lambda>b. if a = b then g b else 1) = g a"
haftmann@58197: proof -
haftmann@58197:   have "(\<lambda>b. if a = b then g b else 1) = (\<lambda>b. if b = a then g b else 1)"
haftmann@58197:     by (simp add: fun_eq_iff)
haftmann@58197:   then have "G (\<lambda>b. if a = b then g b else 1) = G (\<lambda>b. if b = a then g b else 1)"
haftmann@58197:     by (simp cong del: strong_cong)
haftmann@58197:   then show ?thesis by simp
haftmann@58197: qed
haftmann@58197: 
haftmann@58197: end
haftmann@58197: 
haftmann@58197: notation times (infixl "*" 70)
haftmann@58197: notation Groups.one ("1")
haftmann@58197: 
haftmann@58197: 
haftmann@58197: subsection \<open>Concrete sum\<close>
haftmann@58197: 
haftmann@58197: context comm_monoid_add
haftmann@58197: begin
haftmann@58197: 
haftmann@58197: definition Sum_any :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
haftmann@58197: where
haftmann@58197:   "Sum_any = comm_monoid_fun.G plus 0"
haftmann@58197: 
haftmann@58197: permanent_interpretation Sum_any!: comm_monoid_fun plus 0
haftmann@58197: where
haftmann@58197:   "comm_monoid_fun.G plus 0 = Sum_any" and
haftmann@58197:   "comm_monoid_set.F plus 0 = setsum"
haftmann@58197: proof -
haftmann@58197:   show "comm_monoid_fun plus 0" ..
haftmann@58197:   then interpret Sum_any!: comm_monoid_fun plus 0 .
haftmann@58197:   from Sum_any_def show "comm_monoid_fun.G plus 0 = Sum_any" by rule
haftmann@58197:   from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
haftmann@58197: qed
haftmann@58197: 
haftmann@58197: end
haftmann@58197: 
haftmann@58197: syntax
haftmann@58197:   "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3SUM _. _)" [0, 10] 10)
haftmann@58197: syntax (xsymbols)
haftmann@58197:   "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3\<Sum>_. _)" [0, 10] 10)
haftmann@58197: syntax (HTML output)
haftmann@58197:   "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3\<Sum>_. _)" [0, 10] 10)
haftmann@58197: 
haftmann@58197: translations
haftmann@58197:   "\<Sum>a. b" == "CONST Sum_any (\<lambda>a. b)"
haftmann@58197: 
haftmann@58197: lemma Sum_any_left_distrib:
haftmann@58197:   fixes r :: "'a :: semiring_0"
haftmann@58197:   assumes "finite {a. g a \<noteq> 0}"
haftmann@58197:   shows "Sum_any g * r = (\<Sum>n. g n * r)"
haftmann@58197: proof -
haftmann@58197:   note assms
haftmann@58197:   moreover have "{a. g a * r \<noteq> 0} \<subseteq> {a. g a \<noteq> 0}" by auto
haftmann@58197:   ultimately show ?thesis
haftmann@58197:     by (simp add: setsum_left_distrib Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
haftmann@58197: qed  
haftmann@58197: 
haftmann@58197: lemma Sum_any_right_distrib:
haftmann@58197:   fixes r :: "'a :: semiring_0"
haftmann@58197:   assumes "finite {a. g a \<noteq> 0}"
haftmann@58197:   shows "r * Sum_any g = (\<Sum>n. r * g n)"
haftmann@58197: proof -
haftmann@58197:   note assms
haftmann@58197:   moreover have "{a. r * g a \<noteq> 0} \<subseteq> {a. g a \<noteq> 0}" by auto
haftmann@58197:   ultimately show ?thesis
haftmann@58197:     by (simp add: setsum_right_distrib Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
haftmann@58197: qed
haftmann@58197: 
haftmann@58197: lemma Sum_any_product:
haftmann@58197:   fixes f g :: "'b \<Rightarrow> 'a::semiring_0"
haftmann@58197:   assumes "finite {a. f a \<noteq> 0}" and "finite {b. g b \<noteq> 0}"
haftmann@58197:   shows "Sum_any f * Sum_any g = (\<Sum>a. \<Sum>b. f a * g b)"
haftmann@58197: proof -
haftmann@58197:   have subset_f: "{a. (\<Sum>b. f a * g b) \<noteq> 0} \<subseteq> {a. f a \<noteq> 0}"
haftmann@58197:     by rule (simp, rule, auto)
haftmann@58197:   moreover have subset_g: "\<And>a. {b. f a * g b \<noteq> 0} \<subseteq> {b. g b \<noteq> 0}"
haftmann@58197:     by rule (simp, rule, auto)
haftmann@58197:   ultimately show ?thesis using assms
haftmann@58197:     by (auto simp add: Sum_any.expand_set [of f] Sum_any.expand_set [of g]
haftmann@58197:       Sum_any.expand_superset [of "{a. f a \<noteq> 0}"] Sum_any.expand_superset [of "{b. g b \<noteq> 0}"]
haftmann@58197:       setsum_product)
haftmann@58197: qed
haftmann@58197: 
haftmann@58197: 
haftmann@58197: subsection \<open>Concrete product\<close>
haftmann@58197: 
haftmann@58197: context comm_monoid_mult
haftmann@58197: begin
haftmann@58197: 
haftmann@58197: definition Prod_any :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
haftmann@58197: where
haftmann@58197:   "Prod_any = comm_monoid_fun.G times 1"
haftmann@58197: 
haftmann@58197: permanent_interpretation Prod_any!: comm_monoid_fun times 1
haftmann@58197: where
haftmann@58197:   "comm_monoid_fun.G times 1 = Prod_any" and
haftmann@58197:   "comm_monoid_set.F times 1 = setprod"
haftmann@58197: proof -
haftmann@58197:   show "comm_monoid_fun times 1" ..
haftmann@58197:   then interpret Prod_any!: comm_monoid_fun times 1 .
haftmann@58197:   from Prod_any_def show "comm_monoid_fun.G times 1 = Prod_any" by rule
haftmann@58197:   from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
haftmann@58197: qed
haftmann@58197: 
haftmann@58197: end
haftmann@58197: 
haftmann@58197: syntax
haftmann@58197:   "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3PROD _. _)" [0, 10] 10)
haftmann@58197: syntax (xsymbols)
haftmann@58197:   "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3\<Prod>_. _)" [0, 10] 10)
haftmann@58197: syntax (HTML output)
haftmann@58197:   "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3\<Prod>_. _)" [0, 10] 10)
haftmann@58197: 
haftmann@58197: translations
haftmann@58197:   "\<Prod>a. b" == "CONST Prod_any (\<lambda>a. b)"
haftmann@58197: 
haftmann@58197: lemma Prod_any_zero:
haftmann@58197:   fixes f :: "'b \<Rightarrow> 'a :: comm_semiring_1"
haftmann@58197:   assumes "finite {a. f a \<noteq> 1}"
haftmann@58197:   assumes "f a = 0"
haftmann@58197:   shows "(\<Prod>a. f a) = 0"
haftmann@58197: proof -
haftmann@58197:   from `f a = 0` have "f a \<noteq> 1" by simp
haftmann@58197:   with `f a = 0` have "\<exists>a. f a \<noteq> 1 \<and> f a = 0" by blast
haftmann@58197:   with `finite {a. f a \<noteq> 1}` show ?thesis
haftmann@58197:     by (simp add: Prod_any.expand_set setprod_zero)
haftmann@58197: qed
haftmann@58197: 
haftmann@58197: lemma Prod_any_not_zero:
haftmann@58197:   fixes f :: "'b \<Rightarrow> 'a :: comm_semiring_1"
haftmann@58197:   assumes "finite {a. f a \<noteq> 1}"
haftmann@58197:   assumes "(\<Prod>a. f a) \<noteq> 0"
haftmann@58197:   shows "f a \<noteq> 0"
haftmann@58197:   using assms Prod_any_zero [of f] by blast
haftmann@58197: 
haftmann@58197: end