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