summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Groups_List.thy

author | blanchet |

Wed Sep 03 00:06:24 2014 +0200 (2014-09-03) | |

changeset 58152 | 6fe60a9a5bad |

parent 58101 | e7ebe5554281 |

child 58320 | 351810c45a48 |

permissions | -rw-r--r-- |

use 'datatype_new' in 'Main'

2 (* Author: Tobias Nipkow, TU Muenchen *)

4 header {* Summation over lists *}

6 theory Groups_List

7 imports List

8 begin

10 definition (in monoid_add) listsum :: "'a list \<Rightarrow> 'a" where

11 "listsum xs = foldr plus xs 0"

13 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}

15 lemma (in monoid_add) listsum_simps [simp]:

16 "listsum [] = 0"

17 "listsum (x # xs) = x + listsum xs"

18 by (simp_all add: listsum_def)

20 lemma (in monoid_add) listsum_append [simp]:

21 "listsum (xs @ ys) = listsum xs + listsum ys"

22 by (induct xs) (simp_all add: add.assoc)

24 lemma (in comm_monoid_add) listsum_rev [simp]:

25 "listsum (rev xs) = listsum xs"

26 by (simp add: listsum_def foldr_fold fold_rev fun_eq_iff add_ac)

28 lemma (in monoid_add) fold_plus_listsum_rev:

29 "fold plus xs = plus (listsum (rev xs))"

30 proof

31 fix x

32 have "fold plus xs x = fold plus xs (x + 0)" by simp

33 also have "\<dots> = fold plus (x # xs) 0" by simp

34 also have "\<dots> = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_conv_fold)

35 also have "\<dots> = listsum (rev xs @ [x])" by (simp add: listsum_def)

36 also have "\<dots> = listsum (rev xs) + listsum [x]" by simp

37 finally show "fold plus xs x = listsum (rev xs) + x" by simp

38 qed

40 text{* Some syntactic sugar for summing a function over a list: *}

42 syntax

43 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)

44 syntax (xsymbols)

45 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)

46 syntax (HTML output)

47 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)

49 translations -- {* Beware of argument permutation! *}

50 "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"

51 "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"

53 lemma (in comm_monoid_add) listsum_map_remove1:

54 "x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))"

55 by (induct xs) (auto simp add: ac_simps)

57 lemma (in monoid_add) size_list_conv_listsum:

58 "size_list f xs = listsum (map f xs) + size xs"

59 by (induct xs) auto

61 lemma (in monoid_add) length_concat:

62 "length (concat xss) = listsum (map length xss)"

63 by (induct xss) simp_all

65 lemma (in monoid_add) length_product_lists:

66 "length (product_lists xss) = foldr op * (map length xss) 1"

67 proof (induct xss)

68 case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def)

69 qed simp

71 lemma (in monoid_add) listsum_map_filter:

72 assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0"

73 shows "listsum (map f (filter P xs)) = listsum (map f xs)"

74 using assms by (induct xs) auto

76 lemma (in comm_monoid_add) distinct_listsum_conv_Setsum:

77 "distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)"

78 by (induct xs) simp_all

80 lemma listsum_eq_0_nat_iff_nat [simp]:

81 "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"

82 by (induct ns) simp_all

84 lemma member_le_listsum_nat:

85 "(n :: nat) \<in> set ns \<Longrightarrow> n \<le> listsum ns"

86 by (induct ns) auto

88 lemma elem_le_listsum_nat:

89 "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"

90 by (rule member_le_listsum_nat) simp

92 lemma listsum_update_nat:

93 "k < size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k"

94 apply(induct ns arbitrary:k)

95 apply (auto split:nat.split)

96 apply(drule elem_le_listsum_nat)

97 apply arith

98 done

100 lemma (in monoid_add) listsum_triv:

101 "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"

102 by (induct xs) (simp_all add: distrib_right)

104 lemma (in monoid_add) listsum_0 [simp]:

105 "(\<Sum>x\<leftarrow>xs. 0) = 0"

106 by (induct xs) (simp_all add: distrib_right)

108 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}

109 lemma (in ab_group_add) uminus_listsum_map:

110 "- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)"

111 by (induct xs) simp_all

113 lemma (in comm_monoid_add) listsum_addf:

114 "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"

115 by (induct xs) (simp_all add: algebra_simps)

117 lemma (in ab_group_add) listsum_subtractf:

118 "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"

119 by (induct xs) (simp_all add: algebra_simps)

121 lemma (in semiring_0) listsum_const_mult:

122 "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"

123 by (induct xs) (simp_all add: algebra_simps)

125 lemma (in semiring_0) listsum_mult_const:

126 "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"

127 by (induct xs) (simp_all add: algebra_simps)

129 lemma (in ordered_ab_group_add_abs) listsum_abs:

130 "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"

131 by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq])

133 lemma listsum_mono:

134 fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}"

135 shows "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sum>x\<leftarrow>xs. f x) \<le> (\<Sum>x\<leftarrow>xs. g x)"

136 by (induct xs) (simp, simp add: add_mono)

138 lemma (in monoid_add) listsum_distinct_conv_setsum_set:

139 "distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)"

140 by (induct xs) simp_all

142 lemma (in monoid_add) interv_listsum_conv_setsum_set_nat:

143 "listsum (map f [m..<n]) = setsum f (set [m..<n])"

144 by (simp add: listsum_distinct_conv_setsum_set)

146 lemma (in monoid_add) interv_listsum_conv_setsum_set_int:

147 "listsum (map f [k..l]) = setsum f (set [k..l])"

148 by (simp add: listsum_distinct_conv_setsum_set)

150 text {* General equivalence between @{const listsum} and @{const setsum} *}

151 lemma (in monoid_add) listsum_setsum_nth:

152 "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"

153 using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)

156 subsection {* Further facts about @{const List.n_lists} *}

158 lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n"

159 by (induct n) (auto simp add: comp_def length_concat listsum_triv)

161 lemma distinct_n_lists:

162 assumes "distinct xs"

163 shows "distinct (List.n_lists n xs)"

164 proof (rule card_distinct)

165 from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)

166 have "card (set (List.n_lists n xs)) = card (set xs) ^ n"

167 proof (induct n)

168 case 0 then show ?case by simp

169 next

170 case (Suc n)

171 moreover have "card (\<Union>ys\<in>set (List.n_lists n xs). (\<lambda>y. y # ys) ` set xs)

172 = (\<Sum>ys\<in>set (List.n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"

173 by (rule card_UN_disjoint) auto

174 moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"

175 by (rule card_image) (simp add: inj_on_def)

176 ultimately show ?case by auto

177 qed

178 also have "\<dots> = length xs ^ n" by (simp add: card_length)

179 finally show "card (set (List.n_lists n xs)) = length (List.n_lists n xs)"

180 by (simp add: length_n_lists)

181 qed

184 subsection {* Tools setup *}

186 lemma setsum_set_upto_conv_listsum_int [code_unfold]:

187 "setsum f (set [i..j::int]) = listsum (map f [i..j])"

188 by (simp add: interv_listsum_conv_setsum_set_int)

190 lemma setsum_set_upt_conv_listsum_nat [code_unfold]:

191 "setsum f (set [m..<n]) = listsum (map f [m..<n])"

192 by (simp add: interv_listsum_conv_setsum_set_nat)

194 lemma setsum_code [code]:

195 "setsum f (set xs) = listsum (map f (remdups xs))"

196 by (simp add: listsum_distinct_conv_setsum_set)

198 context

199 begin

201 interpretation lifting_syntax .

203 lemma listsum_transfer[transfer_rule]:

204 assumes [transfer_rule]: "A 0 0"

205 assumes [transfer_rule]: "(A ===> A ===> A) op + op +"

206 shows "(list_all2 A ===> A) listsum listsum"

207 unfolding listsum_def[abs_def]

208 by transfer_prover

210 end

212 end