theory about sum and product on function bodies
authorhaftmann
Sat Sep 06 20:12:36 2014 +0200 (2014-09-06)
changeset 581974fd7f47ead6c
parent 58196 1b3fbfb85980
child 58198 099ca49b5231
theory about sum and product on function bodies
src/HOL/Library/Groups_Big_Fun.thy
src/HOL/Library/Library.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Sat Sep 06 20:12:36 2014 +0200
     1.3 @@ -0,0 +1,340 @@
     1.4 +(* Author: Florian Haftmann, TU Muenchen *)
     1.5 +
     1.6 +header \<open>Big sum and product over function bodies\<close>
     1.7 +
     1.8 +theory Groups_Big_Fun
     1.9 +imports
    1.10 +  Main
    1.11 +  "~~/src/Tools/Permanent_Interpretation"
    1.12 +begin
    1.13 +
    1.14 +subsection \<open>Abstract product\<close>
    1.15 +
    1.16 +no_notation times (infixl "*" 70)
    1.17 +no_notation Groups.one ("1")
    1.18 +
    1.19 +locale comm_monoid_fun = comm_monoid
    1.20 +begin
    1.21 +
    1.22 +definition G :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.23 +where
    1.24 +  expand_set: "G g = comm_monoid_set.F f 1 g {a. g a \<noteq> 1}"
    1.25 +
    1.26 +interpretation F!: comm_monoid_set f 1
    1.27 +  ..
    1.28 +
    1.29 +lemma expand_superset:
    1.30 +  assumes "finite A" and "{a. g a \<noteq> 1} \<subseteq> A"
    1.31 +  shows "G g = F.F g A"
    1.32 +  apply (simp add: expand_set)
    1.33 +  apply (rule F.same_carrierI [of A])
    1.34 +  apply (simp_all add: assms)
    1.35 +  done
    1.36 +
    1.37 +lemma conditionalize:
    1.38 +  assumes "finite A"
    1.39 +  shows "F.F g A = G (\<lambda>a. if a \<in> A then g a else 1)"
    1.40 +  using assms
    1.41 +  apply (simp add: expand_set)
    1.42 +  apply (rule F.same_carrierI [of A])
    1.43 +  apply auto
    1.44 +  done
    1.45 +
    1.46 +lemma neutral [simp]:
    1.47 +  "G (\<lambda>a. 1) = 1"
    1.48 +  by (simp add: expand_set)
    1.49 +
    1.50 +lemma update [simp]:
    1.51 +  assumes "finite {a. g a \<noteq> 1}"
    1.52 +  assumes "g a = 1"
    1.53 +  shows "G (g(a := b)) = b * G g"
    1.54 +proof (cases "b = 1")
    1.55 +  case True with `g a = 1` show ?thesis
    1.56 +    by (simp add: expand_set) (rule F.cong, auto)
    1.57 +next
    1.58 +  case False
    1.59 +  moreover have "{a'. a' \<noteq> a \<longrightarrow> g a' \<noteq> 1} = insert a {a. g a \<noteq> 1}"
    1.60 +    by auto
    1.61 +  moreover from `g a = 1` have "a \<notin> {a. g a \<noteq> 1}"
    1.62 +    by simp
    1.63 +  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}"
    1.64 +    by (rule F.cong) (auto simp add: `g a = 1`)
    1.65 +  ultimately show ?thesis using `finite {a. g a \<noteq> 1}` by (simp add: expand_set)
    1.66 +qed
    1.67 +
    1.68 +lemma infinite [simp]:
    1.69 +  "\<not> finite {a. g a \<noteq> 1} \<Longrightarrow> G g = 1"
    1.70 +  by (simp add: expand_set)
    1.71 +
    1.72 +lemma cong:
    1.73 +  assumes "\<And>a. g a = h a"
    1.74 +  shows "G g = G h"
    1.75 +  using assms by (simp add: expand_set)
    1.76 +
    1.77 +lemma strong_cong [cong]:
    1.78 +  assumes "\<And>a. g a = h a"
    1.79 +  shows "G (\<lambda>a. g a) = G (\<lambda>a. h a)"
    1.80 +  using assms by (fact cong)
    1.81 +
    1.82 +lemma not_neutral_obtains_not_neutral:
    1.83 +  assumes "G g \<noteq> 1"
    1.84 +  obtains a where "g a \<noteq> 1"
    1.85 +  using assms by (auto elim: F.not_neutral_contains_not_neutral simp add: expand_set)
    1.86 +
    1.87 +lemma reindex_cong:
    1.88 +  assumes "bij l"
    1.89 +  assumes "g \<circ> l = h"
    1.90 +  shows "G g = G h"
    1.91 +proof -
    1.92 +  from assms have unfold: "h = g \<circ> l" by simp
    1.93 +  from `bij l` have "inj l" by (rule bij_is_inj)
    1.94 +  then have "inj_on l {a. h a \<noteq> 1}" by (rule subset_inj_on) simp
    1.95 +  moreover from `bij l` have "{a. g a \<noteq> 1} = l ` {a. h a \<noteq> 1}"
    1.96 +    by (auto simp add: image_Collect unfold elim: bij_pointE)
    1.97 +  moreover have "\<And>x. x \<in> {a. h a \<noteq> 1} \<Longrightarrow> g (l x) = h x"
    1.98 +    by (simp add: unfold)
    1.99 +  ultimately have "F.F g {a. g a \<noteq> 1} = F.F h {a. h a \<noteq> 1}"
   1.100 +    by (rule F.reindex_cong)
   1.101 +  then show ?thesis by (simp add: expand_set)
   1.102 +qed
   1.103 +
   1.104 +lemma distrib:
   1.105 +  assumes "finite {a. g a \<noteq> 1}" and "finite {a. h a \<noteq> 1}"
   1.106 +  shows "G (\<lambda>a. g a * h a) = G g * G h"
   1.107 +proof -
   1.108 +  from assms have "finite ({a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1})" by simp
   1.109 +  moreover have "{a. g a * h a \<noteq> 1} \<subseteq> {a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1}"
   1.110 +    by auto (drule sym, simp)
   1.111 +  ultimately show ?thesis
   1.112 +    using assms
   1.113 +    by (simp add: expand_superset [of "{a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1}"] F.distrib)
   1.114 +qed
   1.115 +
   1.116 +lemma commute:
   1.117 +  assumes "finite C"
   1.118 +  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")
   1.119 +  shows "G (\<lambda>a. G (g a)) = G (\<lambda>b. G (\<lambda>a. g a b))"
   1.120 +proof -
   1.121 +  from `finite C` subset
   1.122 +    have "finite ({a. \<exists>b. g a b \<noteq> 1} \<times> {b. \<exists>a. g a b \<noteq> 1})"
   1.123 +    by (rule rev_finite_subset)
   1.124 +  then have fins:
   1.125 +    "finite {b. \<exists>a. g a b \<noteq> 1}" "finite {a. \<exists>b. g a b \<noteq> 1}"
   1.126 +    by (auto simp add: finite_cartesian_product_iff)
   1.127 +  have subsets: "\<And>a. {b. g a b \<noteq> 1} \<subseteq> {b. \<exists>a. g a b \<noteq> 1}"
   1.128 +    "\<And>b. {a. g a b \<noteq> 1} \<subseteq> {a. \<exists>b. g a b \<noteq> 1}"
   1.129 +    "{a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1} \<noteq> 1} \<subseteq> {a. \<exists>b. g a b \<noteq> 1}"
   1.130 +    "{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}"
   1.131 +    by (auto elim: F.not_neutral_contains_not_neutral)
   1.132 +  from F.commute have
   1.133 +    "F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) {a. \<exists>b. g a b \<noteq> 1} =
   1.134 +      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}" .
   1.135 +  with subsets fins have "G (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) =
   1.136 +    G (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> 1})"
   1.137 +    by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> 1}"]
   1.138 +      expand_superset [of "{a. \<exists>b. g a b \<noteq> 1}"])
   1.139 +  with subsets fins show ?thesis
   1.140 +    by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> 1}"]
   1.141 +      expand_superset [of "{a. \<exists>b. g a b \<noteq> 1}"])
   1.142 +qed
   1.143 +
   1.144 +lemma cartesian_product:
   1.145 +  assumes "finite C"
   1.146 +  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")
   1.147 +  shows "G (\<lambda>a. G (g a)) = G (\<lambda>(a, b). g a b)"
   1.148 +proof -
   1.149 +  from subset `finite C` have fin_prod: "finite (?A \<times> ?B)"
   1.150 +    by (rule finite_subset)
   1.151 +  from fin_prod have "finite ?A" and "finite ?B"
   1.152 +    by (auto simp add: finite_cartesian_product_iff)
   1.153 +  have *: "G (\<lambda>a. G (g a)) =
   1.154 +    (F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) {a. \<exists>b. g a b \<noteq> 1})"
   1.155 +    apply (subst expand_superset [of "?B"])
   1.156 +    apply (rule `finite ?B`)
   1.157 +    apply auto
   1.158 +    apply (subst expand_superset [of "?A"])
   1.159 +    apply (rule `finite ?A`)
   1.160 +    apply auto
   1.161 +    apply (erule F.not_neutral_contains_not_neutral)
   1.162 +    apply auto
   1.163 +    done
   1.164 +  have "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> 1} \<subseteq> ?A \<times> ?B"
   1.165 +    by auto
   1.166 +  with subset have **: "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> 1} \<subseteq> C"
   1.167 +    by blast
   1.168 +  show ?thesis
   1.169 +    apply (simp add: *)
   1.170 +    apply (simp add: F.cartesian_product)
   1.171 +    apply (subst expand_superset [of C])
   1.172 +    apply (rule `finite C`)
   1.173 +    apply (simp_all add: **)
   1.174 +    apply (rule F.same_carrierI [of C])
   1.175 +    apply (rule `finite C`)
   1.176 +    apply (simp_all add: subset)
   1.177 +    apply auto
   1.178 +    done
   1.179 +qed
   1.180 +
   1.181 +lemma cartesian_product2:
   1.182 +  assumes fin: "finite D"
   1.183 +  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")
   1.184 +  shows "G (\<lambda>(a, b). G (g a b)) = G (\<lambda>(a, b, c). g a b c)"
   1.185 +proof -
   1.186 +  have bij: "bij (\<lambda>(a, b, c). ((a, b), c))"
   1.187 +    by (auto intro!: bijI injI simp add: image_def)
   1.188 +  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"
   1.189 +    by auto (insert subset, auto)
   1.190 +  with fin have "G (\<lambda>p. G (g (fst p) (snd p))) = G (\<lambda>(p, c). g (fst p) (snd p) c)"
   1.191 +    by (rule cartesian_product)
   1.192 +  then have "G (\<lambda>(a, b). G (g a b)) = G (\<lambda>((a, b), c). g a b c)"
   1.193 +    by (auto simp add: split_def)
   1.194 +  also have "G (\<lambda>((a, b), c). g a b c) = G (\<lambda>(a, b, c). g a b c)"
   1.195 +    using bij by (rule reindex_cong [of "\<lambda>(a, b, c). ((a, b), c)"]) (simp add: fun_eq_iff)
   1.196 +  finally show ?thesis .
   1.197 +qed
   1.198 +
   1.199 +lemma delta [simp]:
   1.200 +  "G (\<lambda>b. if b = a then g b else 1) = g a"
   1.201 +proof -
   1.202 +  have "{b. (if b = a then g b else 1) \<noteq> 1} \<subseteq> {a}" by auto
   1.203 +  then show ?thesis by (simp add: expand_superset [of "{a}"])
   1.204 +qed
   1.205 +
   1.206 +lemma delta' [simp]:
   1.207 +  "G (\<lambda>b. if a = b then g b else 1) = g a"
   1.208 +proof -
   1.209 +  have "(\<lambda>b. if a = b then g b else 1) = (\<lambda>b. if b = a then g b else 1)"
   1.210 +    by (simp add: fun_eq_iff)
   1.211 +  then have "G (\<lambda>b. if a = b then g b else 1) = G (\<lambda>b. if b = a then g b else 1)"
   1.212 +    by (simp cong del: strong_cong)
   1.213 +  then show ?thesis by simp
   1.214 +qed
   1.215 +
   1.216 +end
   1.217 +
   1.218 +notation times (infixl "*" 70)
   1.219 +notation Groups.one ("1")
   1.220 +
   1.221 +
   1.222 +subsection \<open>Concrete sum\<close>
   1.223 +
   1.224 +context comm_monoid_add
   1.225 +begin
   1.226 +
   1.227 +definition Sum_any :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
   1.228 +where
   1.229 +  "Sum_any = comm_monoid_fun.G plus 0"
   1.230 +
   1.231 +permanent_interpretation Sum_any!: comm_monoid_fun plus 0
   1.232 +where
   1.233 +  "comm_monoid_fun.G plus 0 = Sum_any" and
   1.234 +  "comm_monoid_set.F plus 0 = setsum"
   1.235 +proof -
   1.236 +  show "comm_monoid_fun plus 0" ..
   1.237 +  then interpret Sum_any!: comm_monoid_fun plus 0 .
   1.238 +  from Sum_any_def show "comm_monoid_fun.G plus 0 = Sum_any" by rule
   1.239 +  from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
   1.240 +qed
   1.241 +
   1.242 +end
   1.243 +
   1.244 +syntax
   1.245 +  "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3SUM _. _)" [0, 10] 10)
   1.246 +syntax (xsymbols)
   1.247 +  "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3\<Sum>_. _)" [0, 10] 10)
   1.248 +syntax (HTML output)
   1.249 +  "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3\<Sum>_. _)" [0, 10] 10)
   1.250 +
   1.251 +translations
   1.252 +  "\<Sum>a. b" == "CONST Sum_any (\<lambda>a. b)"
   1.253 +
   1.254 +lemma Sum_any_left_distrib:
   1.255 +  fixes r :: "'a :: semiring_0"
   1.256 +  assumes "finite {a. g a \<noteq> 0}"
   1.257 +  shows "Sum_any g * r = (\<Sum>n. g n * r)"
   1.258 +proof -
   1.259 +  note assms
   1.260 +  moreover have "{a. g a * r \<noteq> 0} \<subseteq> {a. g a \<noteq> 0}" by auto
   1.261 +  ultimately show ?thesis
   1.262 +    by (simp add: setsum_left_distrib Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
   1.263 +qed  
   1.264 +
   1.265 +lemma Sum_any_right_distrib:
   1.266 +  fixes r :: "'a :: semiring_0"
   1.267 +  assumes "finite {a. g a \<noteq> 0}"
   1.268 +  shows "r * Sum_any g = (\<Sum>n. r * g n)"
   1.269 +proof -
   1.270 +  note assms
   1.271 +  moreover have "{a. r * g a \<noteq> 0} \<subseteq> {a. g a \<noteq> 0}" by auto
   1.272 +  ultimately show ?thesis
   1.273 +    by (simp add: setsum_right_distrib Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
   1.274 +qed
   1.275 +
   1.276 +lemma Sum_any_product:
   1.277 +  fixes f g :: "'b \<Rightarrow> 'a::semiring_0"
   1.278 +  assumes "finite {a. f a \<noteq> 0}" and "finite {b. g b \<noteq> 0}"
   1.279 +  shows "Sum_any f * Sum_any g = (\<Sum>a. \<Sum>b. f a * g b)"
   1.280 +proof -
   1.281 +  have subset_f: "{a. (\<Sum>b. f a * g b) \<noteq> 0} \<subseteq> {a. f a \<noteq> 0}"
   1.282 +    by rule (simp, rule, auto)
   1.283 +  moreover have subset_g: "\<And>a. {b. f a * g b \<noteq> 0} \<subseteq> {b. g b \<noteq> 0}"
   1.284 +    by rule (simp, rule, auto)
   1.285 +  ultimately show ?thesis using assms
   1.286 +    by (auto simp add: Sum_any.expand_set [of f] Sum_any.expand_set [of g]
   1.287 +      Sum_any.expand_superset [of "{a. f a \<noteq> 0}"] Sum_any.expand_superset [of "{b. g b \<noteq> 0}"]
   1.288 +      setsum_product)
   1.289 +qed
   1.290 +
   1.291 +
   1.292 +subsection \<open>Concrete product\<close>
   1.293 +
   1.294 +context comm_monoid_mult
   1.295 +begin
   1.296 +
   1.297 +definition Prod_any :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
   1.298 +where
   1.299 +  "Prod_any = comm_monoid_fun.G times 1"
   1.300 +
   1.301 +permanent_interpretation Prod_any!: comm_monoid_fun times 1
   1.302 +where
   1.303 +  "comm_monoid_fun.G times 1 = Prod_any" and
   1.304 +  "comm_monoid_set.F times 1 = setprod"
   1.305 +proof -
   1.306 +  show "comm_monoid_fun times 1" ..
   1.307 +  then interpret Prod_any!: comm_monoid_fun times 1 .
   1.308 +  from Prod_any_def show "comm_monoid_fun.G times 1 = Prod_any" by rule
   1.309 +  from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
   1.310 +qed
   1.311 +
   1.312 +end
   1.313 +
   1.314 +syntax
   1.315 +  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3PROD _. _)" [0, 10] 10)
   1.316 +syntax (xsymbols)
   1.317 +  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3\<Prod>_. _)" [0, 10] 10)
   1.318 +syntax (HTML output)
   1.319 +  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3\<Prod>_. _)" [0, 10] 10)
   1.320 +
   1.321 +translations
   1.322 +  "\<Prod>a. b" == "CONST Prod_any (\<lambda>a. b)"
   1.323 +
   1.324 +lemma Prod_any_zero:
   1.325 +  fixes f :: "'b \<Rightarrow> 'a :: comm_semiring_1"
   1.326 +  assumes "finite {a. f a \<noteq> 1}"
   1.327 +  assumes "f a = 0"
   1.328 +  shows "(\<Prod>a. f a) = 0"
   1.329 +proof -
   1.330 +  from `f a = 0` have "f a \<noteq> 1" by simp
   1.331 +  with `f a = 0` have "\<exists>a. f a \<noteq> 1 \<and> f a = 0" by blast
   1.332 +  with `finite {a. f a \<noteq> 1}` show ?thesis
   1.333 +    by (simp add: Prod_any.expand_set setprod_zero)
   1.334 +qed
   1.335 +
   1.336 +lemma Prod_any_not_zero:
   1.337 +  fixes f :: "'b \<Rightarrow> 'a :: comm_semiring_1"
   1.338 +  assumes "finite {a. f a \<noteq> 1}"
   1.339 +  assumes "(\<Prod>a. f a) \<noteq> 0"
   1.340 +  shows "f a \<noteq> 0"
   1.341 +  using assms Prod_any_zero [of f] by blast
   1.342 +
   1.343 +end
     2.1 --- a/src/HOL/Library/Library.thy	Sat Sep 06 20:12:34 2014 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Sat Sep 06 20:12:36 2014 +0200
     2.3 @@ -27,6 +27,7 @@
     2.4    Function_Growth
     2.5    Fundamental_Theorem_Algebra
     2.6    Fun_Lexorder
     2.7 +  Groups_Big_Fun
     2.8    Indicator_Function
     2.9    Infinite_Set
    2.10    Inner_Product