author  nipkow 
Wed, 02 Aug 2017 18:22:02 +0200  
changeset 66308  b6a0d95b94be 
parent 64272  f76b6dda2e56 
child 66311  037aaa0b6daf 
permissions  rwrr 
58101  1 
(* Author: Tobias Nipkow, TU Muenchen *) 
2 

60758  3 
section \<open>Sum and product over lists\<close> 
58101  4 

5 
theory Groups_List 

6 
imports List 

7 
begin 

8 

58320  9 
locale monoid_list = monoid 
10 
begin 

11 

12 
definition F :: "'a list \<Rightarrow> 'a" 

13 
where 

63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
63101
diff
changeset

14 
eq_foldr [code]: "F xs = foldr f xs \<^bold>1" 
58320  15 

16 
lemma Nil [simp]: 

63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
63101
diff
changeset

17 
"F [] = \<^bold>1" 
58320  18 
by (simp add: eq_foldr) 
19 

20 
lemma Cons [simp]: 

63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
63101
diff
changeset

21 
"F (x # xs) = x \<^bold>* F xs" 
58320  22 
by (simp add: eq_foldr) 
23 

24 
lemma append [simp]: 

63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
63101
diff
changeset

25 
"F (xs @ ys) = F xs \<^bold>* F ys" 
58320  26 
by (induct xs) (simp_all add: assoc) 
27 

28 
end 

58101  29 

58320  30 
locale comm_monoid_list = comm_monoid + monoid_list 
31 
begin 

32 

33 
lemma rev [simp]: 

34 
"F (rev xs) = F xs" 

35 
by (simp add: eq_foldr foldr_fold fold_rev fun_eq_iff assoc left_commute) 

36 

37 
end 

38 

39 
locale comm_monoid_list_set = list: comm_monoid_list + set: comm_monoid_set 

40 
begin 

58101  41 

58320  42 
lemma distinct_set_conv_list: 
43 
"distinct xs \<Longrightarrow> set.F g (set xs) = list.F (map g xs)" 

44 
by (induct xs) simp_all 

58101  45 

58320  46 
lemma set_conv_list [code]: 
47 
"set.F g (set xs) = list.F (map g (remdups xs))" 

48 
by (simp add: distinct_set_conv_list [symmetric]) 

49 

50 
end 

51 

52 

60758  53 
subsection \<open>List summation\<close> 
58320  54 

55 
context monoid_add 

56 
begin 

57 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

58 
sublocale sum_list: monoid_list plus 0 
61776  59 
defines 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

60 
sum_list = sum_list.F .. 
58320  61 

62 
end 

63 

64 
context comm_monoid_add 

65 
begin 

66 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

67 
sublocale sum_list: comm_monoid_list plus 0 
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset

68 
rewrites 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

69 
"monoid_list.F plus 0 = sum_list" 
58320  70 
proof  
71 
show "comm_monoid_list plus 0" .. 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

72 
then interpret sum_list: comm_monoid_list plus 0 . 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

73 
from sum_list_def show "monoid_list.F plus 0 = sum_list" by simp 
58101  74 
qed 
75 

64267  76 
sublocale sum: comm_monoid_list_set plus 0 
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset

77 
rewrites 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

78 
"monoid_list.F plus 0 = sum_list" 
64267  79 
and "comm_monoid_set.F plus 0 = sum" 
58320  80 
proof  
81 
show "comm_monoid_list_set plus 0" .. 

64267  82 
then interpret sum: comm_monoid_list_set plus 0 . 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

83 
from sum_list_def show "monoid_list.F plus 0 = sum_list" by simp 
64267  84 
from sum_def show "comm_monoid_set.F plus 0 = sum" by (auto intro: sym) 
58320  85 
qed 
86 

87 
end 

88 

60758  89 
text \<open>Some syntactic sugar for summing a function over a list:\<close> 
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset

90 
syntax (ASCII) 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

91 
"_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<_. _)" [0, 51, 10] 10) 
58101  92 
syntax 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

93 
"_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10) 
61799  94 
translations \<comment> \<open>Beware of argument permutation!\<close> 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

95 
"\<Sum>x\<leftarrow>xs. b" == "CONST sum_list (CONST map (\<lambda>x. b) xs)" 
58101  96 

60758  97 
text \<open>TODO duplicates\<close> 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

98 
lemmas sum_list_simps = sum_list.Nil sum_list.Cons 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

99 
lemmas sum_list_append = sum_list.append 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

100 
lemmas sum_list_rev = sum_list.rev 
58320  101 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

102 
lemma (in monoid_add) fold_plus_sum_list_rev: 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

103 
"fold plus xs = plus (sum_list (rev xs))" 
58320  104 
proof 
105 
fix x 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

106 
have "fold plus xs x = sum_list (rev xs @ [x])" 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

107 
by (simp add: foldr_conv_fold sum_list.eq_foldr) 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

108 
also have "\<dots> = sum_list (rev xs) + x" 
58320  109 
by simp 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

110 
finally show "fold plus xs x = sum_list (rev xs) + x" 
58320  111 
. 
112 
qed 

113 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

114 
lemma (in comm_monoid_add) sum_list_map_remove1: 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

115 
"x \<in> set xs \<Longrightarrow> sum_list (map f xs) = f x + sum_list (map f (remove1 x xs))" 
58101  116 
by (induct xs) (auto simp add: ac_simps) 
117 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

118 
lemma (in monoid_add) size_list_conv_sum_list: 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

119 
"size_list f xs = sum_list (map f xs) + size xs" 
58101  120 
by (induct xs) auto 
121 

122 
lemma (in monoid_add) length_concat: 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

123 
"length (concat xss) = sum_list (map length xss)" 
58101  124 
by (induct xss) simp_all 
125 

126 
lemma (in monoid_add) length_product_lists: 

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

128 
proof (induct xss) 

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

130 
qed simp 

131 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

132 
lemma (in monoid_add) sum_list_map_filter: 
58101  133 
assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0" 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

134 
shows "sum_list (map f (filter P xs)) = sum_list (map f xs)" 
58101  135 
using assms by (induct xs) auto 
136 

64267  137 
lemma (in comm_monoid_add) distinct_sum_list_conv_Sum: 
138 
"distinct xs \<Longrightarrow> sum_list xs = Sum (set xs)" 

58101  139 
by (induct xs) simp_all 
140 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

141 
lemma sum_list_upt[simp]: 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

142 
"m \<le> n \<Longrightarrow> sum_list [m..<n] = \<Sum> {m..<n}" 
64267  143 
by(simp add: distinct_sum_list_conv_Sum) 
58995  144 

66308  145 
lemma (in canonically_ordered_monoid_add) sum_list_eq_0_iff [simp]: 
146 
"sum_list ns = 0 \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)" 

147 
by (induct ns) simp_all 

58101  148 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

149 
lemma member_le_sum_list_nat: 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

150 
"(n :: nat) \<in> set ns \<Longrightarrow> n \<le> sum_list ns" 
58101  151 
by (induct ns) auto 
152 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

153 
lemma elem_le_sum_list_nat: 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

154 
"k < size ns \<Longrightarrow> ns ! k \<le> sum_list (ns::nat list)" 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

155 
by (rule member_le_sum_list_nat) simp 
58101  156 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

157 
lemma sum_list_update_nat: 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

158 
"k < size ns \<Longrightarrow> sum_list (ns[k := (n::nat)]) = sum_list ns + n  ns ! k" 
58101  159 
apply(induct ns arbitrary:k) 
160 
apply (auto split:nat.split) 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

161 
apply(drule elem_le_sum_list_nat) 
58101  162 
apply arith 
163 
done 

164 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

165 
lemma (in monoid_add) sum_list_triv: 
58101  166 
"(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r" 
167 
by (induct xs) (simp_all add: distrib_right) 

168 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

169 
lemma (in monoid_add) sum_list_0 [simp]: 
58101  170 
"(\<Sum>x\<leftarrow>xs. 0) = 0" 
171 
by (induct xs) (simp_all add: distrib_right) 

172 

61799  173 
text\<open>For nonAbelian groups \<open>xs\<close> needs to be reversed on one side:\<close> 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

174 
lemma (in ab_group_add) uminus_sum_list_map: 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

175 
" sum_list (map f xs) = sum_list (map (uminus \<circ> f) xs)" 
58101  176 
by (induct xs) simp_all 
177 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

178 
lemma (in comm_monoid_add) sum_list_addf: 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

179 
"(\<Sum>x\<leftarrow>xs. f x + g x) = sum_list (map f xs) + sum_list (map g xs)" 
58101  180 
by (induct xs) (simp_all add: algebra_simps) 
181 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

182 
lemma (in ab_group_add) sum_list_subtractf: 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

183 
"(\<Sum>x\<leftarrow>xs. f x  g x) = sum_list (map f xs)  sum_list (map g xs)" 
58101  184 
by (induct xs) (simp_all add: algebra_simps) 
185 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

186 
lemma (in semiring_0) sum_list_const_mult: 
58101  187 
"(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)" 
188 
by (induct xs) (simp_all add: algebra_simps) 

189 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

190 
lemma (in semiring_0) sum_list_mult_const: 
58101  191 
"(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c" 
192 
by (induct xs) (simp_all add: algebra_simps) 

193 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

194 
lemma (in ordered_ab_group_add_abs) sum_list_abs: 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

195 
"\<bar>sum_list xs\<bar> \<le> sum_list (map abs xs)" 
58101  196 
by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq]) 
197 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

198 
lemma sum_list_mono: 
58101  199 
fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}" 
200 
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)" 

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

202 

64267  203 
lemma (in monoid_add) sum_list_distinct_conv_sum_set: 
204 
"distinct xs \<Longrightarrow> sum_list (map f xs) = sum f (set xs)" 

58101  205 
by (induct xs) simp_all 
206 

64267  207 
lemma (in monoid_add) interv_sum_list_conv_sum_set_nat: 
208 
"sum_list (map f [m..<n]) = sum f (set [m..<n])" 

209 
by (simp add: sum_list_distinct_conv_sum_set) 

58101  210 

64267  211 
lemma (in monoid_add) interv_sum_list_conv_sum_set_int: 
212 
"sum_list (map f [k..l]) = sum f (set [k..l])" 

213 
by (simp add: sum_list_distinct_conv_sum_set) 

58101  214 

64267  215 
text \<open>General equivalence between @{const sum_list} and @{const sum}\<close> 
216 
lemma (in monoid_add) sum_list_sum_nth: 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

217 
"sum_list xs = (\<Sum> i = 0 ..< length xs. xs ! i)" 
64267  218 
using interv_sum_list_conv_sum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth) 
58101  219 

64267  220 
lemma sum_list_map_eq_sum_count: 
221 
"sum_list (map f xs) = sum (\<lambda>x. count_list xs x * f x) (set xs)" 

59728  222 
proof(induction xs) 
223 
case (Cons x xs) 

224 
show ?case (is "?l = ?r") 

225 
proof cases 

226 
assume "x \<in> set xs" 

60541  227 
have "?l = f x + (\<Sum>x\<in>set xs. count_list xs x * f x)" by (simp add: Cons.IH) 
60758  228 
also have "set xs = insert x (set xs  {x})" using \<open>x \<in> set xs\<close>by blast 
60541  229 
also have "f x + (\<Sum>x\<in>insert x (set xs  {x}). count_list xs x * f x) = ?r" 
64267  230 
by (simp add: sum.insert_remove eq_commute) 
59728  231 
finally show ?thesis . 
232 
next 

233 
assume "x \<notin> set xs" 

234 
hence "\<And>xa. xa \<in> set xs \<Longrightarrow> x \<noteq> xa" by blast 

60758  235 
thus ?thesis by (simp add: Cons.IH \<open>x \<notin> set xs\<close>) 
59728  236 
qed 
237 
qed simp 

238 

64267  239 
lemma sum_list_map_eq_sum_count2: 
59728  240 
assumes "set xs \<subseteq> X" "finite X" 
64267  241 
shows "sum_list (map f xs) = sum (\<lambda>x. count_list xs x * f x) X" 
59728  242 
proof 
60541  243 
let ?F = "\<lambda>x. count_list xs x * f x" 
64267  244 
have "sum ?F X = sum ?F (set xs \<union> (X  set xs))" 
59728  245 
using Un_absorb1[OF assms(1)] by(simp) 
64267  246 
also have "\<dots> = sum ?F (set xs)" 
59728  247 
using assms(2) 
64267  248 
by(simp add: sum.union_disjoint[OF _ _ Diff_disjoint] del: Un_Diff_cancel) 
249 
finally show ?thesis by(simp add:sum_list_map_eq_sum_count) 

59728  250 
qed 
251 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

252 
lemma sum_list_nonneg: 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

253 
"(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> sum_list xs \<ge> 0" 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

254 
by (induction xs) simp_all 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

255 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

256 
lemma (in monoid_add) sum_list_map_filter': 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

257 
"sum_list (map f (filter P xs)) = sum_list (map (\<lambda>x. if P x then f x else 0) xs)" 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

258 
by (induction xs) simp_all 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

259 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

260 
lemma sum_list_cong [fundef_cong]: 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

261 
assumes "xs = ys" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

262 
assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = g x" 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

263 
shows "sum_list (map f xs) = sum_list (map g ys)" 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

264 
proof  
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

265 
from assms(2) have "sum_list (map f xs) = sum_list (map g xs)" 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

266 
by (induction xs) simp_all 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

267 
with assms(1) show ?thesis by simp 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

268 
qed 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

269 

58101  270 

60758  271 
subsection \<open>Further facts about @{const List.n_lists}\<close> 
58101  272 

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

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

274 
by (induct n) (auto simp add: comp_def length_concat sum_list_triv) 
58101  275 

276 
lemma distinct_n_lists: 

277 
assumes "distinct xs" 

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

279 
proof (rule card_distinct) 

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

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

282 
proof (induct n) 

283 
case 0 then show ?case by simp 

284 
next 

285 
case (Suc n) 

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

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

288 
by (rule card_UN_disjoint) auto 

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

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

291 
ultimately show ?case by auto 

292 
qed 

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

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

295 
by (simp add: length_n_lists) 

296 
qed 

297 

298 

60758  299 
subsection \<open>Tools setup\<close> 
58101  300 

64267  301 
lemmas sum_code = sum.set_conv_list 
58320  302 

64267  303 
lemma sum_set_upto_conv_sum_list_int [code_unfold]: 
304 
"sum f (set [i..j::int]) = sum_list (map f [i..j])" 

305 
by (simp add: interv_sum_list_conv_sum_set_int) 

58101  306 

64267  307 
lemma sum_set_upt_conv_sum_list_nat [code_unfold]: 
308 
"sum f (set [m..<n]) = sum_list (map f [m..<n])" 

309 
by (simp add: interv_sum_list_conv_sum_set_nat) 

58101  310 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

311 
lemma sum_list_transfer[transfer_rule]: 
63343  312 
includes lifting_syntax 
58101  313 
assumes [transfer_rule]: "A 0 0" 
314 
assumes [transfer_rule]: "(A ===> A ===> A) op + op +" 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

315 
shows "(list_all2 A ===> A) sum_list sum_list" 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

316 
unfolding sum_list.eq_foldr [abs_def] 
58101  317 
by transfer_prover 
318 

58368  319 

60758  320 
subsection \<open>List product\<close> 
58368  321 

322 
context monoid_mult 

323 
begin 

324 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

325 
sublocale prod_list: monoid_list times 1 
61776  326 
defines 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

327 
prod_list = prod_list.F .. 
58368  328 

58320  329 
end 
58368  330 

331 
context comm_monoid_mult 

332 
begin 

333 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

334 
sublocale prod_list: comm_monoid_list times 1 
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset

335 
rewrites 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

336 
"monoid_list.F times 1 = prod_list" 
58368  337 
proof  
338 
show "comm_monoid_list times 1" .. 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

339 
then interpret prod_list: comm_monoid_list times 1 . 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

340 
from prod_list_def show "monoid_list.F times 1 = prod_list" by simp 
58368  341 
qed 
342 

64272  343 
sublocale prod: comm_monoid_list_set times 1 
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset

344 
rewrites 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

345 
"monoid_list.F times 1 = prod_list" 
64272  346 
and "comm_monoid_set.F times 1 = prod" 
58368  347 
proof  
348 
show "comm_monoid_list_set times 1" .. 

64272  349 
then interpret prod: comm_monoid_list_set times 1 . 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

350 
from prod_list_def show "monoid_list.F times 1 = prod_list" by simp 
64272  351 
from prod_def show "comm_monoid_set.F times 1 = prod" by (auto intro: sym) 
58368  352 
qed 
353 

354 
end 

355 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

356 
lemma prod_list_cong [fundef_cong]: 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

357 
assumes "xs = ys" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

358 
assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = g x" 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

359 
shows "prod_list (map f xs) = prod_list (map g ys)" 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

360 
proof  
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

361 
from assms(2) have "prod_list (map f xs) = prod_list (map g xs)" 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

362 
by (induction xs) simp_all 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

363 
with assms(1) show ?thesis by simp 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

364 
qed 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset

365 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

366 
lemma prod_list_zero_iff: 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

367 
"prod_list xs = 0 \<longleftrightarrow> (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \<in> set xs" 
63317
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63290
diff
changeset

368 
by (induction xs) simp_all 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63290
diff
changeset

369 

60758  370 
text \<open>Some syntactic sugar:\<close> 
58368  371 

61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset

372 
syntax (ASCII) 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

373 
"_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3PROD _<_. _)" [0, 51, 10] 10) 
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset

374 
syntax 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

375 
"_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10) 
61799  376 
translations \<comment> \<open>Beware of argument permutation!\<close> 
63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset

377 
"\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST prod_list (CONST map (\<lambda>x. b) xs)" 
58368  378 

379 
end 