(* Author: Florian Haftmann, TU Muenchen *)
section \<open>Big sum and product over function bodies\<close>
theory Groups_Big_Fun
imports
Main
begin
subsection \<open>Abstract product\<close>
locale comm_monoid_fun = comm_monoid
begin
definition G :: "('b \ 'a) \ 'a"
where
expand_set: "G g = comm_monoid_set.F f \<^bold>1 g {a. g a \ \<^bold>1}"
interpretation F: comm_monoid_set f "\<^bold>1"
..
lemma expand_superset:
assumes "finite A" and "{a. g a \ \<^bold>1} \ A"
shows "G g = F.F g A"
apply (simp add: expand_set)
apply (rule F.same_carrierI [of A])
apply (simp_all add: assms)
done
lemma conditionalize:
assumes "finite A"
shows "F.F g A = G (\a. if a \ A then g a else \<^bold>1)"
using assms
apply (simp add: expand_set)
apply (rule F.same_carrierI [of A])
apply auto
done
lemma neutral [simp]:
"G (\a. \<^bold>1) = \<^bold>1"
by (simp add: expand_set)
lemma update [simp]:
assumes "finite {a. g a \ \<^bold>1}"
assumes "g a = \<^bold>1"
shows "G (g(a := b)) = b \<^bold>* G g"
proof (cases "b = \<^bold>1")
case True with \<open>g a = \<^bold>1\<close> show ?thesis
by (simp add: expand_set) (rule F.cong, auto)
next
case False
moreover have "{a'. a' \ a \ g a' \ \<^bold>1} = insert a {a. g a \ \<^bold>1}"
by auto
moreover from \<open>g a = \<^bold>1\<close> have "a \<notin> {a. g a \<noteq> \<^bold>1}"
by simp
moreover have "F.F (\a'. if a' = a then b else g a') {a. g a \ \<^bold>1} = F.F g {a. g a \ \<^bold>1}"
by (rule F.cong) (auto simp add: \<open>g a = \<^bold>1\<close>)
ultimately show ?thesis using \<open>finite {a. g a \<noteq> \<^bold>1}\<close> by (simp add: expand_set)
qed
lemma infinite [simp]:
"\ finite {a. g a \ \<^bold>1} \ G g = \<^bold>1"
by (simp add: expand_set)
lemma cong [cong]:
assumes "\a. g a = h a"
shows "G g = G h"
using assms by (simp add: expand_set)
lemma not_neutral_obtains_not_neutral:
assumes "G g \ \<^bold>1"
obtains a where "g a \ \<^bold>1"
using assms by (auto elim: F.not_neutral_contains_not_neutral simp add: expand_set)
lemma reindex_cong:
assumes "bij l"
assumes "g \ l = h"
shows "G g = G h"
proof -
from assms have unfold: "h = g \ l" by simp
from \<open>bij l\<close> have "inj l" by (rule bij_is_inj)
then have "inj_on l {a. h a \ \<^bold>1}" by (rule subset_inj_on) simp
moreover from \<open>bij l\<close> have "{a. g a \<noteq> \<^bold>1} = l ` {a. h a \<noteq> \<^bold>1}"
by (auto simp add: image_Collect unfold elim: bij_pointE)
moreover have "\x. x \ {a. h a \ \<^bold>1} \ g (l x) = h x"
by (simp add: unfold)
ultimately have "F.F g {a. g a \ \<^bold>1} = F.F h {a. h a \ \<^bold>1}"
by (rule F.reindex_cong)
then show ?thesis by (simp add: expand_set)
qed
lemma distrib:
assumes "finite {a. g a \ \<^bold>1}" and "finite {a. h a \ \<^bold>1}"
shows "G (\a. g a \<^bold>* h a) = G g \<^bold>* G h"
proof -
from assms have "finite ({a. g a \ \<^bold>1} \ {a. h a \ \<^bold>1})" by simp
moreover have "{a. g a \<^bold>* h a \ \<^bold>1} \ {a. g a \ \<^bold>1} \ {a. h a \ \<^bold>1}"
by auto (drule sym, simp)
ultimately show ?thesis
using assms
by (simp add: expand_superset [of "{a. g a \ \<^bold>1} \ {a. h a \ \<^bold>1}"] F.distrib)
qed
lemma swap:
assumes "finite C"
assumes subset: "{a. \b. g a b \ \<^bold>1} \ {b. \a. g a b \ \<^bold>1} \ C" (is "?A \ ?B \ C")
shows "G (\a. G (g a)) = G (\b. G (\a. g a b))"
proof -
from \<open>finite C\<close> subset
have "finite ({a. \b. g a b \ \<^bold>1} \ {b. \a. g a b \ \<^bold>1})"
by (rule rev_finite_subset)
then have fins:
"finite {b. \a. g a b \ \<^bold>1}" "finite {a. \b. g a b \ \<^bold>1}"
by (auto simp add: finite_cartesian_product_iff)
have subsets: "\a. {b. g a b \ \<^bold>1} \ {b. \a. g a b \ \<^bold>1}"
"\b. {a. g a b \ \<^bold>1} \ {a. \b. g a b \ \<^bold>1}"
"{a. F.F (g a) {b. \a. g a b \ \<^bold>1} \ \<^bold>1} \ {a. \b. g a b \ \<^bold>1}"
"{a. F.F (\aa. g aa a) {a. \b. g a b \ \<^bold>1} \ \<^bold>1} \ {b. \a. g a b \ \<^bold>1}"
by (auto elim: F.not_neutral_contains_not_neutral)
from F.swap have
"F.F (\a. F.F (g a) {b. \a. g a b \ \<^bold>1}) {a. \b. g a b \ \<^bold>1} =
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}" .
with subsets fins have "G (\a. F.F (g a) {b. \a. g a b \ \<^bold>1}) =
G (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> \<^bold>1})"
by (auto simp add: expand_superset [of "{b. \a. g a b \ \<^bold>1}"]
expand_superset [of "{a. \b. g a b \ \<^bold>1}"])
with subsets fins show ?thesis
by (auto simp add: expand_superset [of "{b. \a. g a b \ \<^bold>1}"]
expand_superset [of "{a. \b. g a b \ \<^bold>1}"])
qed
lemma cartesian_product:
assumes "finite C"
assumes subset: "{a. \b. g a b \ \<^bold>1} \ {b. \a. g a b \ \<^bold>1} \ C" (is "?A \ ?B \ C")
shows "G (\a. G (g a)) = G (\(a, b). g a b)"
proof -
from subset \<open>finite C\<close> have fin_prod: "finite (?A \<times> ?B)"
by (rule finite_subset)
from fin_prod have "finite ?A" and "finite ?B"
by (auto simp add: finite_cartesian_product_iff)
have *: "G (\a. G (g a)) =
(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})"
apply (subst expand_superset [of "?B"])
apply (rule \<open>finite ?B\<close>)
apply auto
apply (subst expand_superset [of "?A"])
apply (rule \<open>finite ?A\<close>)
apply auto
apply (erule F.not_neutral_contains_not_neutral)
apply auto
done
have "{p. (case p of (a, b) \ g a b) \ \<^bold>1} \ ?A \ ?B"
by auto
with subset have **: "{p. (case p of (a, b) \ g a b) \ \<^bold>1} \ C"
by blast
show ?thesis
apply (simp add: *)
apply (simp add: F.cartesian_product)
apply (subst expand_superset [of C])
apply (rule \<open>finite C\<close>)
apply (simp_all add: **)
apply (rule F.same_carrierI [of C])
apply (rule \<open>finite C\<close>)
apply (simp_all add: subset)
apply auto
done
qed
lemma cartesian_product2:
assumes fin: "finite D"
assumes subset: "{(a, b). \c. g a b c \ \<^bold>1} \ {c. \a b. g a b c \ \<^bold>1} \ D" (is "?AB \ ?C \ D")
shows "G (\(a, b). G (g a b)) = G (\(a, b, c). g a b c)"
proof -
have bij: "bij (\(a, b, c). ((a, b), c))"
by (auto intro!: bijI injI simp add: image_def)
have "{p. \c. g (fst p) (snd p) c \ \<^bold>1} \ {c. \p. g (fst p) (snd p) c \ \<^bold>1} \ D"
by auto (insert subset, blast)
with fin have "G (\p. G (g (fst p) (snd p))) = G (\(p, c). g (fst p) (snd p) c)"
by (rule cartesian_product)
then have "G (\(a, b). G (g a b)) = G (\((a, b), c). g a b c)"
by (auto simp add: split_def)
also have "G (\((a, b), c). g a b c) = G (\(a, b, c). g a b c)"
using bij by (rule reindex_cong [of "\(a, b, c). ((a, b), c)"]) (simp add: fun_eq_iff)
finally show ?thesis .
qed
lemma delta [simp]:
"G (\b. if b = a then g b else \<^bold>1) = g a"
proof -
have "{b. (if b = a then g b else \<^bold>1) \ \<^bold>1} \ {a}" by auto
then show ?thesis by (simp add: expand_superset [of "{a}"])
qed
lemma delta' [simp]:
"G (\b. if a = b then g b else \<^bold>1) = g a"
proof -
have "(\b. if a = b then g b else \<^bold>1) = (\b. if b = a then g b else \<^bold>1)"
by (simp add: fun_eq_iff)
then have "G (\b. if a = b then g b else \<^bold>1) = G (\b. if b = a then g b else \<^bold>1)"
by (simp cong del: cong)
then show ?thesis by simp
qed
end
subsection \<open>Concrete sum\<close>
context comm_monoid_add
begin
sublocale Sum_any: comm_monoid_fun plus 0
rewrites "comm_monoid_set.F plus 0 = sum"
defines Sum_any = Sum_any.G
proof -
show "comm_monoid_fun plus 0" ..
then interpret Sum_any: comm_monoid_fun plus 0 .
from sum_def show "comm_monoid_set.F plus 0 = sum" by (auto intro: sym)
qed
end
syntax (ASCII)
"_Sum_any" :: "pttrn \ 'a \ 'a::comm_monoid_add" ("(3SUM _. _)" [0, 10] 10)
syntax
"_Sum_any" :: "pttrn \ 'a \ 'a::comm_monoid_add" ("(3\_. _)" [0, 10] 10)
translations
"\a. b" \ "CONST Sum_any (\a. b)"
lemma Sum_any_left_distrib:
fixes r :: "'a :: semiring_0"
assumes "finite {a. g a \ 0}"
shows "Sum_any g * r = (\n. g n * r)"
proof -
note assms
moreover have "{a. g a * r \ 0} \ {a. g a \ 0}" by auto
ultimately show ?thesis
by (simp add: sum_distrib_right Sum_any.expand_superset [of "{a. g a \ 0}"])
qed
lemma Sum_any_right_distrib:
fixes r :: "'a :: semiring_0"
assumes "finite {a. g a \ 0}"
shows "r * Sum_any g = (\n. r * g n)"
proof -
note assms
moreover have "{a. r * g a \ 0} \ {a. g a \ 0}" by auto
ultimately show ?thesis
by (simp add: sum_distrib_left Sum_any.expand_superset [of "{a. g a \ 0}"])
qed
lemma Sum_any_product:
fixes f g :: "'b \ 'a::semiring_0"
assumes "finite {a. f a \ 0}" and "finite {b. g b \ 0}"
shows "Sum_any f * Sum_any g = (\a. \b. f a * g b)"
proof -
have subset_f: "{a. (\b. f a * g b) \ 0} \ {a. f a \ 0}"
by rule (simp, rule, auto)
moreover have subset_g: "\a. {b. f a * g b \ 0} \ {b. g b \ 0}"
by rule (simp, rule, auto)
ultimately show ?thesis using assms
by (auto simp add: Sum_any.expand_set [of f] Sum_any.expand_set [of g]
Sum_any.expand_superset [of "{a. f a \ 0}"] Sum_any.expand_superset [of "{b. g b \ 0}"]
sum_product)
qed
lemma Sum_any_eq_zero_iff [simp]:
fixes f :: "'a \ nat"
assumes "finite {a. f a \ 0}"
shows "Sum_any f = 0 \ f = (\_. 0)"
using assms by (simp add: Sum_any.expand_set fun_eq_iff)
subsection \<open>Concrete product\<close>
context comm_monoid_mult
begin
sublocale Prod_any: comm_monoid_fun times 1
rewrites "comm_monoid_set.F times 1 = prod"
defines Prod_any = Prod_any.G
proof -
show "comm_monoid_fun times 1" ..
then interpret Prod_any: comm_monoid_fun times 1 .
from prod_def show "comm_monoid_set.F times 1 = prod" by (auto intro: sym)
qed
end
syntax (ASCII)
"_Prod_any" :: "pttrn \ 'a \ 'a::comm_monoid_mult" ("(3PROD _. _)" [0, 10] 10)
syntax
"_Prod_any" :: "pttrn \ 'a \ 'a::comm_monoid_mult" ("(3\_. _)" [0, 10] 10)
translations
"\a. b" == "CONST Prod_any (\a. b)"
lemma Prod_any_zero:
fixes f :: "'b \ 'a :: comm_semiring_1"
assumes "finite {a. f a \ 1}"
assumes "f a = 0"
shows "(\a. f a) = 0"
proof -
from \<open>f a = 0\<close> have "f a \<noteq> 1" by simp
with \<open>f a = 0\<close> have "\<exists>a. f a \<noteq> 1 \<and> f a = 0" by blast
with \<open>finite {a. f a \<noteq> 1}\<close> show ?thesis
by (simp add: Prod_any.expand_set prod_zero)
qed
lemma Prod_any_not_zero:
fixes f :: "'b \ 'a :: comm_semiring_1"
assumes "finite {a. f a \ 1}"
assumes "(\a. f a) \ 0"
shows "f a \ 0"
using assms Prod_any_zero [of f] by blast
lemma power_Sum_any:
assumes "finite {a. f a \ 0}"
shows "c ^ (\a. f a) = (\a. c ^ f a)"
proof -
have "{a. c ^ f a \ 1} \ {a. f a \ 0}"
by (auto intro: ccontr)
with assms show ?thesis
by (simp add: Sum_any.expand_set Prod_any.expand_superset power_sum)
qed
end
¤ Dauer der Verarbeitung: 0.25 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|