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