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