src/HOL/Library/Groups_Big_Fun.thy
 author haftmann Wed Sep 24 19:11:21 2014 +0200 (2014-09-24) changeset 58437 8d124c73c37a parent 58197 4fd7f47ead6c child 58881 b9556a055632 permissions -rw-r--r--
```     1 (* Author: Florian Haftmann, TU Muenchen *)
```
```     2
```
```     3 header \<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 `g a = 1` 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 `g a = 1` 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: `g a = 1`)
```
```    62   ultimately show ?thesis using `finite {a. g a \<noteq> 1}` 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 `bij l` 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 `bij l` 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 `finite C` 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 `finite C` 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 `finite ?B`)
```
```   154     apply auto
```
```   155     apply (subst expand_superset [of "?A"])
```
```   156     apply (rule `finite ?A`)
```
```   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 `finite C`)
```
```   170     apply (simp_all add: **)
```
```   171     apply (rule F.same_carrierI [of C])
```
```   172     apply (rule `finite C`)
```
```   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 syntax (HTML output)
```
```   246   "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3\<Sum>_. _)" [0, 10] 10)
```
```   247
```
```   248 translations
```
```   249   "\<Sum>a. b" == "CONST Sum_any (\<lambda>a. b)"
```
```   250
```
```   251 lemma Sum_any_left_distrib:
```
```   252   fixes r :: "'a :: semiring_0"
```
```   253   assumes "finite {a. g a \<noteq> 0}"
```
```   254   shows "Sum_any g * r = (\<Sum>n. g n * r)"
```
```   255 proof -
```
```   256   note assms
```
```   257   moreover have "{a. g a * r \<noteq> 0} \<subseteq> {a. g a \<noteq> 0}" by auto
```
```   258   ultimately show ?thesis
```
```   259     by (simp add: setsum_left_distrib Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
```
```   260 qed
```
```   261
```
```   262 lemma Sum_any_right_distrib:
```
```   263   fixes r :: "'a :: semiring_0"
```
```   264   assumes "finite {a. g a \<noteq> 0}"
```
```   265   shows "r * Sum_any g = (\<Sum>n. r * g n)"
```
```   266 proof -
```
```   267   note assms
```
```   268   moreover have "{a. r * g a \<noteq> 0} \<subseteq> {a. g a \<noteq> 0}" by auto
```
```   269   ultimately show ?thesis
```
```   270     by (simp add: setsum_right_distrib Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
```
```   271 qed
```
```   272
```
```   273 lemma Sum_any_product:
```
```   274   fixes f g :: "'b \<Rightarrow> 'a::semiring_0"
```
```   275   assumes "finite {a. f a \<noteq> 0}" and "finite {b. g b \<noteq> 0}"
```
```   276   shows "Sum_any f * Sum_any g = (\<Sum>a. \<Sum>b. f a * g b)"
```
```   277 proof -
```
```   278   have subset_f: "{a. (\<Sum>b. f a * g b) \<noteq> 0} \<subseteq> {a. f a \<noteq> 0}"
```
```   279     by rule (simp, rule, auto)
```
```   280   moreover have subset_g: "\<And>a. {b. f a * g b \<noteq> 0} \<subseteq> {b. g b \<noteq> 0}"
```
```   281     by rule (simp, rule, auto)
```
```   282   ultimately show ?thesis using assms
```
```   283     by (auto simp add: Sum_any.expand_set [of f] Sum_any.expand_set [of g]
```
```   284       Sum_any.expand_superset [of "{a. f a \<noteq> 0}"] Sum_any.expand_superset [of "{b. g b \<noteq> 0}"]
```
```   285       setsum_product)
```
```   286 qed
```
```   287
```
```   288 lemma Sum_any_eq_zero_iff [simp]:
```
```   289   fixes f :: "'a \<Rightarrow> nat"
```
```   290   assumes "finite {a. f a \<noteq> 0}"
```
```   291   shows "Sum_any f = 0 \<longleftrightarrow> f = (\<lambda>_. 0)"
```
```   292   using assms by (simp add: Sum_any.expand_set fun_eq_iff)
```
```   293
```
```   294
```
```   295 subsection \<open>Concrete product\<close>
```
```   296
```
```   297 context comm_monoid_mult
```
```   298 begin
```
```   299
```
```   300 definition Prod_any :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
```
```   301 where
```
```   302   "Prod_any = comm_monoid_fun.G times 1"
```
```   303
```
```   304 permanent_interpretation Prod_any!: comm_monoid_fun times 1
```
```   305 where
```
```   306   "comm_monoid_fun.G times 1 = Prod_any" and
```
```   307   "comm_monoid_set.F times 1 = setprod"
```
```   308 proof -
```
```   309   show "comm_monoid_fun times 1" ..
```
```   310   then interpret Prod_any!: comm_monoid_fun times 1 .
```
```   311   from Prod_any_def show "comm_monoid_fun.G times 1 = Prod_any" by rule
```
```   312   from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
```
```   313 qed
```
```   314
```
```   315 end
```
```   316
```
```   317 syntax
```
```   318   "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3PROD _. _)" [0, 10] 10)
```
```   319 syntax (xsymbols)
```
```   320   "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3\<Prod>_. _)" [0, 10] 10)
```
```   321 syntax (HTML output)
```
```   322   "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3\<Prod>_. _)" [0, 10] 10)
```
```   323
```
```   324 translations
```
```   325   "\<Prod>a. b" == "CONST Prod_any (\<lambda>a. b)"
```
```   326
```
```   327 lemma Prod_any_zero:
```
```   328   fixes f :: "'b \<Rightarrow> 'a :: comm_semiring_1"
```
```   329   assumes "finite {a. f a \<noteq> 1}"
```
```   330   assumes "f a = 0"
```
```   331   shows "(\<Prod>a. f a) = 0"
```
```   332 proof -
```
```   333   from `f a = 0` have "f a \<noteq> 1" by simp
```
```   334   with `f a = 0` have "\<exists>a. f a \<noteq> 1 \<and> f a = 0" by blast
```
```   335   with `finite {a. f a \<noteq> 1}` show ?thesis
```
```   336     by (simp add: Prod_any.expand_set setprod_zero)
```
```   337 qed
```
```   338
```
```   339 lemma Prod_any_not_zero:
```
```   340   fixes f :: "'b \<Rightarrow> 'a :: comm_semiring_1"
```
```   341   assumes "finite {a. f a \<noteq> 1}"
```
```   342   assumes "(\<Prod>a. f a) \<noteq> 0"
```
```   343   shows "f a \<noteq> 0"
```
```   344   using assms Prod_any_zero [of f] by blast
```
```   345
```
```   346 lemma power_Sum_any:
```
```   347   assumes "finite {a. f a \<noteq> 0}"
```
```   348   shows "c ^ (\<Sum>a. f a) = (\<Prod>a. c ^ f a)"
```
```   349 proof -
```
```   350   have "{a. c ^ f a \<noteq> 1} \<subseteq> {a. f a \<noteq> 0}"
```
```   351     by (auto intro: ccontr)
```
```   352   with assms show ?thesis
```
```   353     by (simp add: Sum_any.expand_set Prod_any.expand_superset power_setsum)
```
```   354 qed
```
```   355
```
```   356 end
```
```   357
```