--- a/NEWS Wed Sep 14 22:07:11 2016 +0200
+++ b/NEWS Thu Sep 15 11:48:20 2016 +0200
@@ -251,6 +251,10 @@
* Theory Set_Interval.thy: substantial new theorems on indexed sums
and products.
+* Theory List.thy:
+ listsum ~> sum_list
+ listprod ~> prod_list
+
* Theory Library/LaTeXsugar.thy: New style "dummy_pats" for displaying
equations in functional programming style: variables present on the
left-hand but not on the righ-hand side are replaced by underscores.
--- a/src/HOL/Binomial.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Binomial.thy Thu Sep 15 11:48:20 2016 +0200
@@ -1521,28 +1521,28 @@
qed
text \<open>The number of nat lists of length \<open>m\<close> summing to \<open>N\<close> is @{term "(N + m - 1) choose N"}:\<close>
-lemma card_length_listsum_rec:
+lemma card_length_sum_list_rec:
assumes "m \<ge> 1"
- shows "card {l::nat list. length l = m \<and> listsum l = N} =
- card {l. length l = (m - 1) \<and> listsum l = N} +
- card {l. length l = m \<and> listsum l + 1 = N}"
+ shows "card {l::nat list. length l = m \<and> sum_list l = N} =
+ card {l. length l = (m - 1) \<and> sum_list l = N} +
+ card {l. length l = m \<and> sum_list l + 1 = N}"
(is "card ?C = card ?A + card ?B")
proof -
- let ?A' = "{l. length l = m \<and> listsum l = N \<and> hd l = 0}"
- let ?B' = "{l. length l = m \<and> listsum l = N \<and> hd l \<noteq> 0}"
+ let ?A' = "{l. length l = m \<and> sum_list l = N \<and> hd l = 0}"
+ let ?B' = "{l. length l = m \<and> sum_list l = N \<and> hd l \<noteq> 0}"
let ?f = "\<lambda>l. 0 # l"
let ?g = "\<lambda>l. (hd l + 1) # tl l"
have 1: "xs \<noteq> [] \<Longrightarrow> x = hd xs \<Longrightarrow> x # tl xs = xs" for x xs
by simp
- have 2: "xs \<noteq> [] \<Longrightarrow> listsum(tl xs) = listsum xs - hd xs" for xs :: "nat list"
+ have 2: "xs \<noteq> [] \<Longrightarrow> sum_list(tl xs) = sum_list xs - hd xs" for xs :: "nat list"
by (auto simp add: neq_Nil_conv)
have f: "bij_betw ?f ?A ?A'"
apply (rule bij_betw_byWitness[where f' = tl])
using assms
apply (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv)
done
- have 3: "xs \<noteq> [] \<Longrightarrow> hd xs + (listsum xs - hd xs) = listsum xs" for xs :: "nat list"
- by (metis 1 listsum_simps(2) 2)
+ have 3: "xs \<noteq> [] \<Longrightarrow> hd xs + (sum_list xs - hd xs) = sum_list xs" for xs :: "nat list"
+ by (metis 1 sum_list_simps(2) 2)
have g: "bij_betw ?g ?B ?B'"
apply (rule bij_betw_byWitness[where f' = "\<lambda>l. (hd l - 1) # tl l"])
using assms
@@ -1552,10 +1552,10 @@
using finite_lists_length_eq[OF finite_atLeastLessThan] conj_commute by auto
have fin_A: "finite ?A" using fin[of _ "N+1"]
by (intro finite_subset[where ?A = "?A" and ?B = "{xs. size xs = m - 1 \<and> set xs \<subseteq> {0..<N+1}}"])
- (auto simp: member_le_listsum_nat less_Suc_eq_le)
+ (auto simp: member_le_sum_list_nat less_Suc_eq_le)
have fin_B: "finite ?B"
by (intro finite_subset[where ?A = "?B" and ?B = "{xs. size xs = m \<and> set xs \<subseteq> {0..<N}}"])
- (auto simp: member_le_listsum_nat less_Suc_eq_le fin)
+ (auto simp: member_le_sum_list_nat less_Suc_eq_le fin)
have uni: "?C = ?A' \<union> ?B'"
by auto
have disj: "?A' \<inter> ?B' = {}"
@@ -1569,7 +1569,7 @@
finally show ?thesis .
qed
-lemma card_length_listsum: "card {l::nat list. size l = m \<and> listsum l = N} = (N + m - 1) choose N"
+lemma card_length_sum_list: "card {l::nat list. size l = m \<and> sum_list l = N} = (N + m - 1) choose N"
\<comment> "by Holden Lee, tidied by Tobias Nipkow"
proof (cases m)
case 0
@@ -1590,7 +1590,7 @@
by simp
next
case (Suc k)
- have c1: "card {l::nat list. size l = (m - 1) \<and> listsum l = N} = (N + (m - 1) - 1) choose N"
+ have c1: "card {l::nat list. size l = (m - 1) \<and> sum_list l = N} = (N + (m - 1) - 1) choose N"
proof (cases "m = 1")
case True
with Suc.hyps have "N \<ge> 1"
@@ -1602,23 +1602,23 @@
then show ?thesis
using Suc by fastforce
qed
- from Suc have c2: "card {l::nat list. size l = m \<and> listsum l + 1 = N} =
+ from Suc have c2: "card {l::nat list. size l = m \<and> sum_list l + 1 = N} =
(if N > 0 then ((N - 1) + m - 1) choose (N - 1) else 0)"
proof -
have *: "n > 0 \<Longrightarrow> Suc m = n \<longleftrightarrow> m = n - 1" for m n
by arith
from Suc have "N > 0 \<Longrightarrow>
- card {l::nat list. size l = m \<and> listsum l + 1 = N} =
+ card {l::nat list. size l = m \<and> sum_list l + 1 = N} =
((N - 1) + m - 1) choose (N - 1)"
by (simp add: *)
then show ?thesis
by auto
qed
- from Suc.prems have "(card {l::nat list. size l = (m - 1) \<and> listsum l = N} +
- card {l::nat list. size l = m \<and> listsum l + 1 = N}) = (N + m - 1) choose N"
+ from Suc.prems have "(card {l::nat list. size l = (m - 1) \<and> sum_list l = N} +
+ card {l::nat list. size l = m \<and> sum_list l + 1 = N}) = (N + m - 1) choose N"
by (auto simp: c1 c2 choose_reduce_nat[of "N + m - 1" N] simp del: One_nat_def)
then show ?case
- using card_length_listsum_rec[OF Suc.prems] by auto
+ using card_length_sum_list_rec[OF Suc.prems] by auto
qed
qed
--- a/src/HOL/GCD.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/GCD.thy Thu Sep 15 11:48:20 2016 +0200
@@ -865,7 +865,7 @@
apply (auto simp add: gcd_mult_cancel)
done
-lemma listprod_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (listprod xs) y"
+lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y"
by (induct xs) (simp_all add: gcd_mult_cancel)
lemma coprime_divisors:
--- a/src/HOL/Groups_List.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Groups_List.thy Thu Sep 15 11:48:20 2016 +0200
@@ -55,32 +55,32 @@
context monoid_add
begin
-sublocale listsum: monoid_list plus 0
+sublocale sum_list: monoid_list plus 0
defines
- listsum = listsum.F ..
+ sum_list = sum_list.F ..
end
context comm_monoid_add
begin
-sublocale listsum: comm_monoid_list plus 0
+sublocale sum_list: comm_monoid_list plus 0
rewrites
- "monoid_list.F plus 0 = listsum"
+ "monoid_list.F plus 0 = sum_list"
proof -
show "comm_monoid_list plus 0" ..
- then interpret listsum: comm_monoid_list plus 0 .
- from listsum_def show "monoid_list.F plus 0 = listsum" by simp
+ then interpret sum_list: comm_monoid_list plus 0 .
+ from sum_list_def show "monoid_list.F plus 0 = sum_list" by simp
qed
sublocale setsum: comm_monoid_list_set plus 0
rewrites
- "monoid_list.F plus 0 = listsum"
+ "monoid_list.F plus 0 = sum_list"
and "comm_monoid_set.F plus 0 = setsum"
proof -
show "comm_monoid_list_set plus 0" ..
then interpret setsum: comm_monoid_list_set plus 0 .
- from listsum_def show "monoid_list.F plus 0 = listsum" by simp
+ from sum_list_def show "monoid_list.F plus 0 = sum_list" by simp
from setsum_def show "comm_monoid_set.F plus 0 = setsum" by (auto intro: sym)
qed
@@ -88,39 +88,39 @@
text \<open>Some syntactic sugar for summing a function over a list:\<close>
syntax (ASCII)
- "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
+ "_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
syntax
- "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
+ "_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
translations \<comment> \<open>Beware of argument permutation!\<close>
- "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (\<lambda>x. b) xs)"
+ "\<Sum>x\<leftarrow>xs. b" == "CONST sum_list (CONST map (\<lambda>x. b) xs)"
text \<open>TODO duplicates\<close>
-lemmas listsum_simps = listsum.Nil listsum.Cons
-lemmas listsum_append = listsum.append
-lemmas listsum_rev = listsum.rev
+lemmas sum_list_simps = sum_list.Nil sum_list.Cons
+lemmas sum_list_append = sum_list.append
+lemmas sum_list_rev = sum_list.rev
-lemma (in monoid_add) fold_plus_listsum_rev:
- "fold plus xs = plus (listsum (rev xs))"
+lemma (in monoid_add) fold_plus_sum_list_rev:
+ "fold plus xs = plus (sum_list (rev xs))"
proof
fix x
- have "fold plus xs x = listsum (rev xs @ [x])"
- by (simp add: foldr_conv_fold listsum.eq_foldr)
- also have "\<dots> = listsum (rev xs) + x"
+ have "fold plus xs x = sum_list (rev xs @ [x])"
+ by (simp add: foldr_conv_fold sum_list.eq_foldr)
+ also have "\<dots> = sum_list (rev xs) + x"
by simp
- finally show "fold plus xs x = listsum (rev xs) + x"
+ finally show "fold plus xs x = sum_list (rev xs) + x"
.
qed
-lemma (in comm_monoid_add) listsum_map_remove1:
- "x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))"
+lemma (in comm_monoid_add) sum_list_map_remove1:
+ "x \<in> set xs \<Longrightarrow> sum_list (map f xs) = f x + sum_list (map f (remove1 x xs))"
by (induct xs) (auto simp add: ac_simps)
-lemma (in monoid_add) size_list_conv_listsum:
- "size_list f xs = listsum (map f xs) + size xs"
+lemma (in monoid_add) size_list_conv_sum_list:
+ "size_list f xs = sum_list (map f xs) + size xs"
by (induct xs) auto
lemma (in monoid_add) length_concat:
- "length (concat xss) = listsum (map length xss)"
+ "length (concat xss) = sum_list (map length xss)"
by (induct xss) simp_all
lemma (in monoid_add) length_product_lists:
@@ -129,96 +129,96 @@
case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def)
qed simp
-lemma (in monoid_add) listsum_map_filter:
+lemma (in monoid_add) sum_list_map_filter:
assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0"
- shows "listsum (map f (filter P xs)) = listsum (map f xs)"
+ shows "sum_list (map f (filter P xs)) = sum_list (map f xs)"
using assms by (induct xs) auto
-lemma (in comm_monoid_add) distinct_listsum_conv_Setsum:
- "distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)"
+lemma (in comm_monoid_add) distinct_sum_list_conv_Setsum:
+ "distinct xs \<Longrightarrow> sum_list xs = Setsum (set xs)"
by (induct xs) simp_all
-lemma listsum_upt[simp]:
- "m \<le> n \<Longrightarrow> listsum [m..<n] = \<Sum> {m..<n}"
-by(simp add: distinct_listsum_conv_Setsum)
+lemma sum_list_upt[simp]:
+ "m \<le> n \<Longrightarrow> sum_list [m..<n] = \<Sum> {m..<n}"
+by(simp add: distinct_sum_list_conv_Setsum)
-lemma listsum_eq_0_nat_iff_nat [simp]:
- "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
+lemma sum_list_eq_0_nat_iff_nat [simp]:
+ "sum_list ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
by (induct ns) simp_all
-lemma member_le_listsum_nat:
- "(n :: nat) \<in> set ns \<Longrightarrow> n \<le> listsum ns"
+lemma member_le_sum_list_nat:
+ "(n :: nat) \<in> set ns \<Longrightarrow> n \<le> sum_list ns"
by (induct ns) auto
-lemma elem_le_listsum_nat:
- "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"
- by (rule member_le_listsum_nat) simp
+lemma elem_le_sum_list_nat:
+ "k < size ns \<Longrightarrow> ns ! k \<le> sum_list (ns::nat list)"
+ by (rule member_le_sum_list_nat) simp
-lemma listsum_update_nat:
- "k < size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k"
+lemma sum_list_update_nat:
+ "k < size ns \<Longrightarrow> sum_list (ns[k := (n::nat)]) = sum_list ns + n - ns ! k"
apply(induct ns arbitrary:k)
apply (auto split:nat.split)
-apply(drule elem_le_listsum_nat)
+apply(drule elem_le_sum_list_nat)
apply arith
done
-lemma (in monoid_add) listsum_triv:
+lemma (in monoid_add) sum_list_triv:
"(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
by (induct xs) (simp_all add: distrib_right)
-lemma (in monoid_add) listsum_0 [simp]:
+lemma (in monoid_add) sum_list_0 [simp]:
"(\<Sum>x\<leftarrow>xs. 0) = 0"
by (induct xs) (simp_all add: distrib_right)
text\<open>For non-Abelian groups \<open>xs\<close> needs to be reversed on one side:\<close>
-lemma (in ab_group_add) uminus_listsum_map:
- "- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)"
+lemma (in ab_group_add) uminus_sum_list_map:
+ "- sum_list (map f xs) = sum_list (map (uminus \<circ> f) xs)"
by (induct xs) simp_all
-lemma (in comm_monoid_add) listsum_addf:
- "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
+lemma (in comm_monoid_add) sum_list_addf:
+ "(\<Sum>x\<leftarrow>xs. f x + g x) = sum_list (map f xs) + sum_list (map g xs)"
by (induct xs) (simp_all add: algebra_simps)
-lemma (in ab_group_add) listsum_subtractf:
- "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
+lemma (in ab_group_add) sum_list_subtractf:
+ "(\<Sum>x\<leftarrow>xs. f x - g x) = sum_list (map f xs) - sum_list (map g xs)"
by (induct xs) (simp_all add: algebra_simps)
-lemma (in semiring_0) listsum_const_mult:
+lemma (in semiring_0) sum_list_const_mult:
"(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
by (induct xs) (simp_all add: algebra_simps)
-lemma (in semiring_0) listsum_mult_const:
+lemma (in semiring_0) sum_list_mult_const:
"(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
by (induct xs) (simp_all add: algebra_simps)
-lemma (in ordered_ab_group_add_abs) listsum_abs:
- "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
+lemma (in ordered_ab_group_add_abs) sum_list_abs:
+ "\<bar>sum_list xs\<bar> \<le> sum_list (map abs xs)"
by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq])
-lemma listsum_mono:
+lemma sum_list_mono:
fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}"
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)"
by (induct xs) (simp, simp add: add_mono)
-lemma (in monoid_add) listsum_distinct_conv_setsum_set:
- "distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)"
+lemma (in monoid_add) sum_list_distinct_conv_setsum_set:
+ "distinct xs \<Longrightarrow> sum_list (map f xs) = setsum f (set xs)"
by (induct xs) simp_all
-lemma (in monoid_add) interv_listsum_conv_setsum_set_nat:
- "listsum (map f [m..<n]) = setsum f (set [m..<n])"
- by (simp add: listsum_distinct_conv_setsum_set)
+lemma (in monoid_add) interv_sum_list_conv_setsum_set_nat:
+ "sum_list (map f [m..<n]) = setsum f (set [m..<n])"
+ by (simp add: sum_list_distinct_conv_setsum_set)
-lemma (in monoid_add) interv_listsum_conv_setsum_set_int:
- "listsum (map f [k..l]) = setsum f (set [k..l])"
- by (simp add: listsum_distinct_conv_setsum_set)
+lemma (in monoid_add) interv_sum_list_conv_setsum_set_int:
+ "sum_list (map f [k..l]) = setsum f (set [k..l])"
+ by (simp add: sum_list_distinct_conv_setsum_set)
-text \<open>General equivalence between @{const listsum} and @{const setsum}\<close>
-lemma (in monoid_add) listsum_setsum_nth:
- "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
- using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
+text \<open>General equivalence between @{const sum_list} and @{const setsum}\<close>
+lemma (in monoid_add) sum_list_setsum_nth:
+ "sum_list xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
+ using interv_sum_list_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
-lemma listsum_map_eq_setsum_count:
- "listsum (map f xs) = setsum (\<lambda>x. count_list xs x * f x) (set xs)"
+lemma sum_list_map_eq_setsum_count:
+ "sum_list (map f xs) = setsum (\<lambda>x. count_list xs x * f x) (set xs)"
proof(induction xs)
case (Cons x xs)
show ?case (is "?l = ?r")
@@ -236,9 +236,9 @@
qed
qed simp
-lemma listsum_map_eq_setsum_count2:
+lemma sum_list_map_eq_setsum_count2:
assumes "set xs \<subseteq> X" "finite X"
-shows "listsum (map f xs) = setsum (\<lambda>x. count_list xs x * f x) X"
+shows "sum_list (map f xs) = setsum (\<lambda>x. count_list xs x * f x) X"
proof-
let ?F = "\<lambda>x. count_list xs x * f x"
have "setsum ?F X = setsum ?F (set xs \<union> (X - set xs))"
@@ -246,23 +246,23 @@
also have "\<dots> = setsum ?F (set xs)"
using assms(2)
by(simp add: setsum.union_disjoint[OF _ _ Diff_disjoint] del: Un_Diff_cancel)
- finally show ?thesis by(simp add:listsum_map_eq_setsum_count)
+ finally show ?thesis by(simp add:sum_list_map_eq_setsum_count)
qed
-lemma listsum_nonneg:
- "(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> listsum xs \<ge> 0"
+lemma sum_list_nonneg:
+ "(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> sum_list xs \<ge> 0"
by (induction xs) simp_all
-lemma (in monoid_add) listsum_map_filter':
- "listsum (map f (filter P xs)) = listsum (map (\<lambda>x. if P x then f x else 0) xs)"
+lemma (in monoid_add) sum_list_map_filter':
+ "sum_list (map f (filter P xs)) = sum_list (map (\<lambda>x. if P x then f x else 0) xs)"
by (induction xs) simp_all
-lemma listsum_cong [fundef_cong]:
+lemma sum_list_cong [fundef_cong]:
assumes "xs = ys"
assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = g x"
- shows "listsum (map f xs) = listsum (map g ys)"
+ shows "sum_list (map f xs) = sum_list (map g ys)"
proof -
- from assms(2) have "listsum (map f xs) = listsum (map g xs)"
+ from assms(2) have "sum_list (map f xs) = sum_list (map g xs)"
by (induction xs) simp_all
with assms(1) show ?thesis by simp
qed
@@ -271,7 +271,7 @@
subsection \<open>Further facts about @{const List.n_lists}\<close>
lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n"
- by (induct n) (auto simp add: comp_def length_concat listsum_triv)
+ by (induct n) (auto simp add: comp_def length_concat sum_list_triv)
lemma distinct_n_lists:
assumes "distinct xs"
@@ -300,20 +300,20 @@
lemmas setsum_code = setsum.set_conv_list
-lemma setsum_set_upto_conv_listsum_int [code_unfold]:
- "setsum f (set [i..j::int]) = listsum (map f [i..j])"
- by (simp add: interv_listsum_conv_setsum_set_int)
+lemma setsum_set_upto_conv_sum_list_int [code_unfold]:
+ "setsum f (set [i..j::int]) = sum_list (map f [i..j])"
+ by (simp add: interv_sum_list_conv_setsum_set_int)
-lemma setsum_set_upt_conv_listsum_nat [code_unfold]:
- "setsum f (set [m..<n]) = listsum (map f [m..<n])"
- by (simp add: interv_listsum_conv_setsum_set_nat)
+lemma setsum_set_upt_conv_sum_list_nat [code_unfold]:
+ "setsum f (set [m..<n]) = sum_list (map f [m..<n])"
+ by (simp add: interv_sum_list_conv_setsum_set_nat)
-lemma listsum_transfer[transfer_rule]:
+lemma sum_list_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "A 0 0"
assumes [transfer_rule]: "(A ===> A ===> A) op + op +"
- shows "(list_all2 A ===> A) listsum listsum"
- unfolding listsum.eq_foldr [abs_def]
+ shows "(list_all2 A ===> A) sum_list sum_list"
+ unfolding sum_list.eq_foldr [abs_def]
by transfer_prover
@@ -322,58 +322,58 @@
context monoid_mult
begin
-sublocale listprod: monoid_list times 1
+sublocale prod_list: monoid_list times 1
defines
- listprod = listprod.F ..
+ prod_list = prod_list.F ..
end
context comm_monoid_mult
begin
-sublocale listprod: comm_monoid_list times 1
+sublocale prod_list: comm_monoid_list times 1
rewrites
- "monoid_list.F times 1 = listprod"
+ "monoid_list.F times 1 = prod_list"
proof -
show "comm_monoid_list times 1" ..
- then interpret listprod: comm_monoid_list times 1 .
- from listprod_def show "monoid_list.F times 1 = listprod" by simp
+ then interpret prod_list: comm_monoid_list times 1 .
+ from prod_list_def show "monoid_list.F times 1 = prod_list" by simp
qed
sublocale setprod: comm_monoid_list_set times 1
rewrites
- "monoid_list.F times 1 = listprod"
+ "monoid_list.F times 1 = prod_list"
and "comm_monoid_set.F times 1 = setprod"
proof -
show "comm_monoid_list_set times 1" ..
then interpret setprod: comm_monoid_list_set times 1 .
- from listprod_def show "monoid_list.F times 1 = listprod" by simp
+ from prod_list_def show "monoid_list.F times 1 = prod_list" by simp
from setprod_def show "comm_monoid_set.F times 1 = setprod" by (auto intro: sym)
qed
end
-lemma listprod_cong [fundef_cong]:
+lemma prod_list_cong [fundef_cong]:
assumes "xs = ys"
assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = g x"
- shows "listprod (map f xs) = listprod (map g ys)"
+ shows "prod_list (map f xs) = prod_list (map g ys)"
proof -
- from assms(2) have "listprod (map f xs) = listprod (map g xs)"
+ from assms(2) have "prod_list (map f xs) = prod_list (map g xs)"
by (induction xs) simp_all
with assms(1) show ?thesis by simp
qed
-lemma listprod_zero_iff:
- "listprod xs = 0 \<longleftrightarrow> (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \<in> set xs"
+lemma prod_list_zero_iff:
+ "prod_list xs = 0 \<longleftrightarrow> (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \<in> set xs"
by (induction xs) simp_all
text \<open>Some syntactic sugar:\<close>
syntax (ASCII)
- "_listprod" :: "pttrn => 'a list => 'b => 'b" ("(3PROD _<-_. _)" [0, 51, 10] 10)
+ "_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3PROD _<-_. _)" [0, 51, 10] 10)
syntax
- "_listprod" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
+ "_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
translations \<comment> \<open>Beware of argument permutation!\<close>
- "\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST listprod (CONST map (\<lambda>x. b) xs)"
+ "\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST prod_list (CONST map (\<lambda>x. b) xs)"
end
--- a/src/HOL/IMP/Abs_Int0.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy Thu Sep 15 11:48:20 2016 +0200
@@ -329,14 +329,14 @@
by(cases opt)(auto simp add: m_s_h le_SucI dest: m_s_h)
definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^sub>c") where
-"m_c C = listsum (map (\<lambda>a. m_o a (vars C)) (annos C))"
+"m_c C = sum_list (map (\<lambda>a. m_o a (vars C)) (annos C))"
text{* Upper complexity bound: *}
lemma m_c_h: "m_c C \<le> size(annos C) * (h * card(vars C) + 1)"
proof-
let ?X = "vars C" let ?n = "card ?X" let ?a = "size(annos C)"
have "m_c C = (\<Sum>i<?a. m_o (annos C ! i) ?X)"
- by(simp add: m_c_def listsum_setsum_nth atLeast0LessThan)
+ by(simp add: m_c_def sum_list_setsum_nth atLeast0LessThan)
also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
apply(rule setsum_mono) using m_o_h[OF finite_Cvars] by simp
also have "\<dots> = ?a * (h * ?n + 1)" by simp
@@ -455,7 +455,7 @@
< (\<Sum>i<size(annos C2). m_o (annos C1 ! i) ?X)"
apply(rule setsum_strict_mono_ex1) using 1 2 by (auto)
thus ?thesis
- by(simp add: m_c_def vars_acom_def strip_eq listsum_setsum_nth atLeast0LessThan size_annos_same[OF strip_eq])
+ by(simp add: m_c_def vars_acom_def strip_eq sum_list_setsum_nth atLeast0LessThan size_annos_same[OF strip_eq])
qed
end
--- a/src/HOL/IMP/Abs_Int1.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy Thu Sep 15 11:48:20 2016 +0200
@@ -118,14 +118,14 @@
by(auto simp add: m_o_def m_s_h le_SucI split: option.split dest:m_s_h)
definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^sub>c") where
-"m_c C = listsum (map (\<lambda>a. m_o a (vars C)) (annos C))"
+"m_c C = sum_list (map (\<lambda>a. m_o a (vars C)) (annos C))"
text{* Upper complexity bound: *}
lemma m_c_h: "m_c C \<le> size(annos C) * (h * card(vars C) + 1)"
proof-
let ?X = "vars C" let ?n = "card ?X" let ?a = "size(annos C)"
have "m_c C = (\<Sum>i<?a. m_o (annos C ! i) ?X)"
- by(simp add: m_c_def listsum_setsum_nth atLeast0LessThan)
+ by(simp add: m_c_def sum_list_setsum_nth atLeast0LessThan)
also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
apply(rule setsum_mono) using m_o_h[OF finite_Cvars] by simp
also have "\<dots> = ?a * (h * ?n + 1)" by simp
@@ -239,7 +239,7 @@
< (\<Sum>i<size(annos C2). m_o (annos C1 ! i) ?X)"
apply(rule setsum_strict_mono_ex1) using 1 2 by (auto)
thus ?thesis
- by(simp add: m_c_def vars_acom_def strip_eq listsum_setsum_nth atLeast0LessThan size_annos_same[OF strip_eq])
+ by(simp add: m_c_def vars_acom_def strip_eq sum_list_setsum_nth atLeast0LessThan size_annos_same[OF strip_eq])
qed
end
--- a/src/HOL/IMP/Abs_Int3.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy Thu Sep 15 11:48:20 2016 +0200
@@ -390,7 +390,7 @@
lemma m_c_widen:
"strip C1 = strip C2 \<Longrightarrow> top_on_acom C1 (-vars C1) \<Longrightarrow> top_on_acom C2 (-vars C2)
\<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
-apply(auto simp: m_c_def widen_acom_def map2_acom_def size_annos[symmetric] anno_def[symmetric]listsum_setsum_nth)
+apply(auto simp: m_c_def widen_acom_def map2_acom_def size_annos[symmetric] anno_def[symmetric]sum_list_setsum_nth)
apply(subgoal_tac "length(annos C2) = length(annos C1)")
prefer 2 apply (simp add: size_annos_same2)
apply (auto)
@@ -437,7 +437,7 @@
definition n_c :: "'av st option acom \<Rightarrow> nat" ("n\<^sub>c") where
-"n\<^sub>c C = listsum (map (\<lambda>a. n\<^sub>o a (vars C)) (annos C))"
+"n\<^sub>c C = sum_list (map (\<lambda>a. n\<^sub>o a (vars C)) (annos C))"
lemma less_annos_iff: "(C1 < C2) = (C1 \<le> C2 \<and>
(\<exists>i<length (annos C1). annos C1 ! i < annos C2 ! i))"
@@ -446,7 +446,7 @@
lemma n_c_narrow: "strip C1 = strip C2
\<Longrightarrow> top_on_acom C1 (- vars C1) \<Longrightarrow> top_on_acom C2 (- vars C2)
\<Longrightarrow> C2 \<le> C1 \<Longrightarrow> C1 \<triangle> C2 < C1 \<Longrightarrow> n\<^sub>c (C1 \<triangle> C2) < n\<^sub>c C1"
-apply(auto simp: n_c_def narrow_acom_def listsum_setsum_nth)
+apply(auto simp: n_c_def narrow_acom_def sum_list_setsum_nth)
apply(subgoal_tac "length(annos C2) = length(annos C1)")
prefer 2 apply (simp add: size_annos_same2)
apply (auto)
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Sep 15 11:48:20 2016 +0200
@@ -951,16 +951,16 @@
lemma setsum_ennreal[simp]: "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Sum>i\<in>I. ennreal (f i)) = ennreal (setsum f I)"
by (induction I rule: infinite_finite_induct) (auto simp: setsum_nonneg)
-lemma listsum_ennreal[simp]:
+lemma sum_list_ennreal[simp]:
assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<ge> 0"
- shows "listsum (map (\<lambda>x. ennreal (f x)) xs) = ennreal (listsum (map f xs))"
+ shows "sum_list (map (\<lambda>x. ennreal (f x)) xs) = ennreal (sum_list (map f xs))"
using assms
proof (induction xs)
case (Cons x xs)
- from Cons have "(\<Sum>x\<leftarrow>x # xs. ennreal (f x)) = ennreal (f x) + ennreal (listsum (map f xs))"
+ from Cons have "(\<Sum>x\<leftarrow>x # xs. ennreal (f x)) = ennreal (f x) + ennreal (sum_list (map f xs))"
by simp
- also from Cons.prems have "\<dots> = ennreal (f x + listsum (map f xs))"
- by (intro ennreal_plus [symmetric] listsum_nonneg) auto
+ also from Cons.prems have "\<dots> = ennreal (f x + sum_list (map f xs))"
+ by (intro ennreal_plus [symmetric] sum_list_nonneg) auto
finally show ?case by simp
qed simp_all
--- a/src/HOL/Library/Extended_Real.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy Thu Sep 15 11:48:20 2016 +0200
@@ -771,7 +771,7 @@
then show ?thesis by simp
qed
-lemma listsum_ereal [simp]: "listsum (map (\<lambda>x. ereal (f x)) xs) = ereal (listsum (map f xs))"
+lemma sum_list_ereal [simp]: "sum_list (map (\<lambda>x. ereal (f x)) xs) = ereal (sum_list (map f xs))"
by (induction xs) simp_all
lemma setsum_Pinfty:
--- a/src/HOL/Library/Formal_Power_Series.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Thu Sep 15 11:48:20 2016 +0200
@@ -2107,7 +2107,7 @@
subsubsection \<open>Rule 4 in its more general form: generalizes Rule 3 for an arbitrary
finite product of FPS, also the relvant instance of powers of a FPS\<close>
-definition "natpermute n k = {l :: nat list. length l = k \<and> listsum l = n}"
+definition "natpermute n k = {l :: nat list. length l = k \<and> sum_list l = n}"
lemma natlist_trivial_1: "natpermute n 1 = {[n]}"
apply (auto simp add: natpermute_def)
@@ -2117,14 +2117,14 @@
lemma append_natpermute_less_eq:
assumes "xs @ ys \<in> natpermute n k"
- shows "listsum xs \<le> n"
- and "listsum ys \<le> n"
+ shows "sum_list xs \<le> n"
+ and "sum_list ys \<le> n"
proof -
- from assms have "listsum (xs @ ys) = n"
+ from assms have "sum_list (xs @ ys) = n"
by (simp add: natpermute_def)
- then have "listsum xs + listsum ys = n"
+ then have "sum_list xs + sum_list ys = n"
by simp
- then show "listsum xs \<le> n" and "listsum ys \<le> n"
+ then show "sum_list xs \<le> n" and "sum_list ys \<le> n"
by simp_all
qed
@@ -2142,9 +2142,9 @@
and xs: "xs \<in> natpermute m h"
and ys: "ys \<in> natpermute (n - m) (k - h)"
and leq: "l = xs@ys" by blast
- from xs have xs': "listsum xs = m"
+ from xs have xs': "sum_list xs = m"
by (simp add: natpermute_def)
- from ys have ys': "listsum ys = n - m"
+ from ys have ys': "sum_list ys = n - m"
by (simp add: natpermute_def)
show "l \<in> ?L" using leq xs ys h
apply (clarsimp simp add: natpermute_def)
@@ -2160,12 +2160,12 @@
assume l: "l \<in> natpermute n k"
let ?xs = "take h l"
let ?ys = "drop h l"
- let ?m = "listsum ?xs"
- from l have ls: "listsum (?xs @ ?ys) = n"
+ let ?m = "sum_list ?xs"
+ from l have ls: "sum_list (?xs @ ?ys) = n"
by (simp add: natpermute_def)
have xs: "?xs \<in> natpermute ?m h" using l assms
by (simp add: natpermute_def)
- have l_take_drop: "listsum l = listsum (take h l @ drop h l)"
+ have l_take_drop: "sum_list l = sum_list (take h l @ drop h l)"
by simp
then have ys: "?ys \<in> natpermute (n - ?m) (k - h)"
using l assms ls by (auto simp add: natpermute_def simp del: append_take_drop_id)
@@ -2230,7 +2230,7 @@
using i by auto
from H have "n = setsum (nth xs) {0..k}"
apply (simp add: natpermute_def)
- apply (auto simp add: atLeastLessThanSuc_atLeastAtMost listsum_setsum_nth)
+ apply (auto simp add: atLeastLessThanSuc_atLeastAtMost sum_list_setsum_nth)
done
also have "\<dots> = n + setsum (nth xs) ({0..k} - {i})"
unfolding setsum.union_disjoint[OF f d, unfolded eqs] using i by simp
@@ -2265,8 +2265,8 @@
done
have xsl: "length xs = k + 1"
by (simp only: xs length_replicate length_list_update)
- have "listsum xs = setsum (nth xs) {0..<k+1}"
- unfolding listsum_setsum_nth xsl ..
+ have "sum_list xs = setsum (nth xs) {0..<k+1}"
+ unfolding sum_list_setsum_nth xsl ..
also have "\<dots> = setsum (\<lambda>j. if j = i then n else 0) {0..< k+1}"
by (rule setsum.cong) (simp_all add: xs del: replicate.simps)
also have "\<dots> = n" using i by (simp add: setsum.delta)
@@ -2421,9 +2421,9 @@
by (auto simp: set_conv_nth A_def natpermute_def less_Suc_eq_le)
then guess j by (elim exE conjE) note j = this
- from v have "k = listsum v" by (simp add: A_def natpermute_def)
+ from v have "k = sum_list v" by (simp add: A_def natpermute_def)
also have "\<dots> = (\<Sum>i=0..m. v ! i)"
- by (simp add: listsum_setsum_nth atLeastLessThanSuc_atLeastAtMost del: setsum_op_ivl_Suc)
+ by (simp add: sum_list_setsum_nth atLeastLessThanSuc_atLeastAtMost del: setsum_op_ivl_Suc)
also from j have "{0..m} = insert j ({0..m}-{j})" by auto
also from j have "(\<Sum>i\<in>\<dots>. v ! i) = k + (\<Sum>i\<in>{0..m}-{j}. v ! i)"
by (subst setsum.insert) simp_all
@@ -2469,7 +2469,7 @@
g $ k * (of_nat (Suc m) * (f $ 0) ^ m) + ?h g" using assms
by (simp add: mult_ac del: power_Suc of_nat_Suc)
also have "v ! i < k" if "v \<in> {v\<in>natpermute k (m+1). k \<notin> set v}" "i \<le> m" for v i
- using that elem_le_listsum_nat[of i v] unfolding natpermute_def
+ using that elem_le_sum_list_nat[of i v] unfolding natpermute_def
by (auto simp: set_conv_nth dest!: spec[of _ i])
hence "?h f = ?h g"
by (intro setsum.cong refl setprod.cong less lessI) (auto simp: natpermute_def)
@@ -2599,10 +2599,10 @@
by auto
have eqs: "{0..<Suc k} = {0 ..< i} \<union> ({i} \<union> {i+1 ..< Suc k})"
using i by auto
- from xs have "Suc n = listsum xs"
+ from xs have "Suc n = sum_list xs"
by (simp add: natpermute_def)
also have "\<dots> = setsum (nth xs) {0..<Suc k}" using xs
- by (simp add: natpermute_def listsum_setsum_nth)
+ by (simp add: natpermute_def sum_list_setsum_nth)
also have "\<dots> = xs!i + setsum (nth xs) {0..<i} + setsum (nth xs) {i+1..<Suc k}"
unfolding eqs setsum.union_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)]
unfolding setsum.union_disjoint[OF fths(2) fths(3) d(2)]
@@ -2853,10 +2853,10 @@
by auto
have eqs: "{0..<Suc k} = {0 ..< i} \<union> ({i} \<union> {i+1 ..< Suc k})"
using i by auto
- from xs have "n = listsum xs"
+ from xs have "n = sum_list xs"
by (simp add: natpermute_def)
also have "\<dots> = setsum (nth xs) {0..<Suc k}"
- using xs by (simp add: natpermute_def listsum_setsum_nth)
+ using xs by (simp add: natpermute_def sum_list_setsum_nth)
also have "\<dots> = xs!i + setsum (nth xs) {0..<i} + setsum (nth xs) {i+1..<Suc k}"
unfolding eqs setsum.union_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)]
unfolding setsum.union_disjoint[OF fths(2) fths(3) d(2)]
--- a/src/HOL/Library/ListVector.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Library/ListVector.thy Thu Sep 15 11:48:20 2016 +0200
@@ -119,7 +119,7 @@
done
lemma iprod_uminus[simp]: "\<langle>-xs,ys\<rangle> = -\<langle>xs,ys\<rangle>"
-by(simp add: iprod_def uminus_listsum_map o_def split_def map_zip_map list_uminus_def)
+by(simp add: iprod_def uminus_sum_list_map o_def split_def map_zip_map list_uminus_def)
lemma iprod_left_add_distrib: "\<langle>xs + ys,zs\<rangle> = \<langle>xs,zs\<rangle> + \<langle>ys,zs\<rangle>"
apply(induct xs arbitrary: ys zs)
--- a/src/HOL/Library/Multiset.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Thu Sep 15 11:48:20 2016 +0200
@@ -3188,7 +3188,7 @@
end
-lemma [code]: "sum_mset (mset xs) = listsum xs"
+lemma [code]: "sum_mset (mset xs) = sum_list xs"
by (induct xs) simp_all
lemma [code]: "prod_mset (mset xs) = fold times xs 1"
--- a/src/HOL/Library/Polynomial.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Library/Polynomial.thy Thu Sep 15 11:48:20 2016 +0200
@@ -2946,7 +2946,7 @@
lemma lead_coeff_0[simp]:"lead_coeff 0 =0"
unfolding lead_coeff_def by auto
-lemma coeff_0_listprod: "coeff (listprod xs) 0 = listprod (map (\<lambda>p. coeff p 0) xs)"
+lemma coeff_0_prod_list: "coeff (prod_list xs) 0 = prod_list (map (\<lambda>p. coeff p 0) xs)"
by (induction xs) (simp_all add: coeff_mult)
lemma coeff_0_power: "coeff (p ^ n) 0 = coeff p 0 ^ n"
@@ -3214,9 +3214,9 @@
setprod (\<lambda>x. reflect_poly (f x)) A"
by (cases "finite A", induction rule: finite_induct) (simp_all add: reflect_poly_mult)
-lemma reflect_poly_listprod:
- "reflect_poly (listprod (xs :: _ :: {comm_semiring_0,semiring_no_zero_divisors} poly list)) =
- listprod (map reflect_poly xs)"
+lemma reflect_poly_prod_list:
+ "reflect_poly (prod_list (xs :: _ :: {comm_semiring_0,semiring_no_zero_divisors} poly list)) =
+ prod_list (map reflect_poly xs)"
by (induction xs) (simp_all add: reflect_poly_mult)
lemma reflect_poly_Poly_nz:
@@ -3225,7 +3225,7 @@
lemmas reflect_poly_simps =
reflect_poly_0 reflect_poly_1 reflect_poly_const reflect_poly_smult reflect_poly_mult
- reflect_poly_power reflect_poly_setprod reflect_poly_listprod
+ reflect_poly_power reflect_poly_setprod reflect_poly_prod_list
subsection \<open>Derivatives of univariate polynomials\<close>
--- a/src/HOL/Library/Polynomial_FPS.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Library/Polynomial_FPS.thy Thu Sep 15 11:48:20 2016 +0200
@@ -64,13 +64,13 @@
lemma fps_of_poly_setsum: "fps_of_poly (setsum f A) = setsum (\<lambda>x. fps_of_poly (f x)) A"
by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_add)
-lemma fps_of_poly_listsum: "fps_of_poly (listsum xs) = listsum (map fps_of_poly xs)"
+lemma fps_of_poly_sum_list: "fps_of_poly (sum_list xs) = sum_list (map fps_of_poly xs)"
by (induction xs) (simp_all add: fps_of_poly_add)
lemma fps_of_poly_setprod: "fps_of_poly (setprod f A) = setprod (\<lambda>x. fps_of_poly (f x)) A"
by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_mult)
-lemma fps_of_poly_listprod: "fps_of_poly (listprod xs) = listprod (map fps_of_poly xs)"
+lemma fps_of_poly_prod_list: "fps_of_poly (prod_list xs) = prod_list (map fps_of_poly xs)"
by (induction xs) (simp_all add: fps_of_poly_mult)
lemma fps_of_poly_pCons:
@@ -144,7 +144,7 @@
lemmas fps_of_poly_simps =
fps_of_poly_0 fps_of_poly_1 fps_of_poly_numeral fps_of_poly_const fps_of_poly_X
fps_of_poly_add fps_of_poly_diff fps_of_poly_uminus fps_of_poly_mult fps_of_poly_smult
- fps_of_poly_setsum fps_of_poly_listsum fps_of_poly_setprod fps_of_poly_listprod
+ fps_of_poly_setsum fps_of_poly_sum_list fps_of_poly_setprod fps_of_poly_prod_list
fps_of_poly_pCons fps_of_poly_pderiv fps_of_poly_power fps_of_poly_monom
fps_of_poly_divide_numeral
--- a/src/HOL/Nitpick.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Nitpick.thy Thu Sep 15 11:48:20 2016 +0200
@@ -73,7 +73,7 @@
"card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
definition setsum' :: "('a \<Rightarrow> 'b::comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where
- "setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
+ "setsum' f A \<equiv> if finite A then sum_list (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" where
"fold_graph' f z {} z" |
--- a/src/HOL/Nominal/Examples/Standardization.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Nominal/Examples/Standardization.thy Thu Sep 15 11:48:20 2016 +0200
@@ -213,8 +213,8 @@
prefer 2
apply (erule allE, erule impE, rule refl, erule spec)
apply simp
- apply (simp only: foldl_conv_fold add.commute fold_plus_listsum_rev)
- apply (fastforce simp add: listsum_map_remove1)
+ apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
+ apply (fastforce simp add: sum_list_map_remove1)
apply clarify
apply (subgoal_tac "\<exists>y::name. y \<sharp> (x, u, z)")
prefer 2
@@ -235,8 +235,8 @@
prefer 2
apply blast
apply simp
- apply (simp only: foldl_conv_fold add.commute fold_plus_listsum_rev)
- apply (fastforce simp add: listsum_map_remove1)
+ apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
+ apply (fastforce simp add: sum_list_map_remove1)
done
theorem Apps_lam_induct:
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Thu Sep 15 11:48:20 2016 +0200
@@ -306,14 +306,14 @@
lemma sparsify_length: "(i, x) \<in> set (sparsify xs) \<Longrightarrow> i < length xs"
by (auto simp: sparsify_def set_zip)
-lemma listsum_sparsify[simp]:
+lemma sum_list_sparsify[simp]:
fixes v :: "('a :: semiring_0) list"
assumes "length w = length v"
shows "(\<Sum>x\<leftarrow>sparsify w. (\<lambda>(i, x). v ! i) x * snd x) = scalar_product v w"
(is "(\<Sum>x\<leftarrow>_. ?f x) = _")
unfolding sparsify_def scalar_product_def
- using assms listsum_map_filter[where f="?f" and P="\<lambda> i. snd i \<noteq> (0::'a)"]
- by (simp add: listsum_setsum)
+ using assms sum_list_map_filter[where f="?f" and P="\<lambda> i. snd i \<noteq> (0::'a)"]
+ by (simp add: sum_list_setsum)
*)
definition [simp]: "unzip w = (map fst w, map snd w)"
@@ -338,7 +338,7 @@
"jad = apsnd transpose o length_permutate o map sparsify"
definition
- "jad_mv v = inflate o case_prod zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))"
+ "jad_mv v = inflate o case_prod zip o apsnd (map sum_list o transpose o map (map (\<lambda> (i, x). v ! i * x)))"
lemma "matrix (M::int list list) rs cs \<Longrightarrow> False"
quickcheck[tester = smart_exhaustive, size = 6]
--- a/src/HOL/Probability/PMF_Impl.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Probability/PMF_Impl.thy Thu Sep 15 11:48:20 2016 +0200
@@ -396,10 +396,10 @@
lemma mapping_of_pmf_pmf_of_list:
- assumes "\<And>x. x \<in> snd ` set xs \<Longrightarrow> x > 0" "listsum (map snd xs) = 1"
+ assumes "\<And>x. x \<in> snd ` set xs \<Longrightarrow> x > 0" "sum_list (map snd xs) = 1"
shows "mapping_of_pmf (pmf_of_list xs) =
Mapping.tabulate (remdups (map fst xs))
- (\<lambda>x. listsum (map snd (filter (\<lambda>z. fst z = x) xs)))"
+ (\<lambda>x. sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
proof -
from assms have wf: "pmf_of_list_wf xs" by (intro pmf_of_list_wfI) force
with assms have "set_pmf (pmf_of_list xs) = fst ` set xs"
@@ -413,7 +413,7 @@
defines "xs' \<equiv> filter (\<lambda>z. snd z \<noteq> 0) xs"
shows "mapping_of_pmf (pmf_of_list xs) =
Mapping.tabulate (remdups (map fst xs'))
- (\<lambda>x. listsum (map snd (filter (\<lambda>z. fst z = x) xs')))" (is "_ = ?rhs")
+ (\<lambda>x. sum_list (map snd (filter (\<lambda>z. fst z = x) xs')))" (is "_ = ?rhs")
proof -
have wf: "pmf_of_list_wf xs'" unfolding xs'_def by (rule pmf_of_list_remove_zeros) fact
have pos: "\<forall>x\<in>snd`set xs'. x > 0" using assms(1) unfolding xs'_def
@@ -426,7 +426,7 @@
qed
lemma pmf_of_list_wf_code [code]:
- "pmf_of_list_wf xs \<longleftrightarrow> list_all (\<lambda>z. snd z \<ge> 0) xs \<and> listsum (map snd xs) = 1"
+ "pmf_of_list_wf xs \<longleftrightarrow> list_all (\<lambda>z. snd z \<ge> 0) xs \<and> sum_list (map snd xs) = 1"
by (auto simp add: pmf_of_list_wf_def list_all_def)
lemma pmf_of_list_code [code abstract]:
@@ -434,7 +434,7 @@
if pmf_of_list_wf xs then
let xs' = filter (\<lambda>z. snd z \<noteq> 0) xs
in Mapping.tabulate (remdups (map fst xs'))
- (\<lambda>x. listsum (map snd (filter (\<lambda>z. fst z = x) xs')))
+ (\<lambda>x. sum_list (map snd (filter (\<lambda>z. fst z = x) xs')))
else
Code.abort (STR ''Invalid list for pmf_of_list'') (\<lambda>_. mapping_of_pmf (pmf_of_list xs)))"
using mapping_of_pmf_pmf_of_list'[of xs] by (simp add: Let_def)
--- a/src/HOL/Probability/Probability_Mass_Function.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Thu Sep 15 11:48:20 2016 +0200
@@ -1843,13 +1843,13 @@
subsection \<open>PMFs from assiciation lists\<close>
definition pmf_of_list ::" ('a \<times> real) list \<Rightarrow> 'a pmf" where
- "pmf_of_list xs = embed_pmf (\<lambda>x. listsum (map snd (filter (\<lambda>z. fst z = x) xs)))"
+ "pmf_of_list xs = embed_pmf (\<lambda>x. sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
definition pmf_of_list_wf where
- "pmf_of_list_wf xs \<longleftrightarrow> (\<forall>x\<in>set (map snd xs) . x \<ge> 0) \<and> listsum (map snd xs) = 1"
+ "pmf_of_list_wf xs \<longleftrightarrow> (\<forall>x\<in>set (map snd xs) . x \<ge> 0) \<and> sum_list (map snd xs) = 1"
lemma pmf_of_list_wfI:
- "(\<And>x. x \<in> set (map snd xs) \<Longrightarrow> x \<ge> 0) \<Longrightarrow> listsum (map snd xs) = 1 \<Longrightarrow> pmf_of_list_wf xs"
+ "(\<And>x. x \<in> set (map snd xs) \<Longrightarrow> x \<ge> 0) \<Longrightarrow> sum_list (map snd xs) = 1 \<Longrightarrow> pmf_of_list_wf xs"
unfolding pmf_of_list_wf_def by simp
context
@@ -1857,12 +1857,12 @@
private lemma pmf_of_list_aux:
assumes "\<And>x. x \<in> set (map snd xs) \<Longrightarrow> x \<ge> 0"
- assumes "listsum (map snd xs) = 1"
- shows "(\<integral>\<^sup>+ x. ennreal (listsum (map snd [z\<leftarrow>xs . fst z = x])) \<partial>count_space UNIV) = 1"
+ assumes "sum_list (map snd xs) = 1"
+ shows "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])) \<partial>count_space UNIV) = 1"
proof -
- have "(\<integral>\<^sup>+ x. ennreal (listsum (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) =
- (\<integral>\<^sup>+ x. ennreal (listsum (map (\<lambda>(x',p). indicator {x'} x * p) xs)) \<partial>count_space UNIV)"
- by (intro nn_integral_cong ennreal_cong, subst listsum_map_filter') (auto intro: listsum_cong)
+ have "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) =
+ (\<integral>\<^sup>+ x. ennreal (sum_list (map (\<lambda>(x',p). indicator {x'} x * p) xs)) \<partial>count_space UNIV)"
+ by (intro nn_integral_cong ennreal_cong, subst sum_list_map_filter') (auto intro: sum_list_cong)
also have "\<dots> = (\<Sum>(x',p)\<leftarrow>xs. (\<integral>\<^sup>+ x. ennreal (indicator {x'} x * p) \<partial>count_space UNIV))"
using assms(1)
proof (induction xs)
@@ -1874,11 +1874,11 @@
(\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) +
ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
by (intro nn_integral_cong, subst ennreal_plus [symmetric])
- (auto simp: case_prod_unfold indicator_def intro!: listsum_nonneg)
+ (auto simp: case_prod_unfold indicator_def intro!: sum_list_nonneg)
also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) \<partial>count_space UNIV) +
(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
by (intro nn_integral_add)
- (force intro!: listsum_nonneg AE_I2 intro: Cons simp: indicator_def)+
+ (force intro!: sum_list_nonneg AE_I2 intro: Cons simp: indicator_def)+
also have "(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV) =
(\<Sum>(x', p)\<leftarrow>xs. (\<integral>\<^sup>+ y. ennreal (indicator {x'} y * p) \<partial>count_space UNIV))"
using Cons(1) by (intro Cons) simp_all
@@ -1886,19 +1886,19 @@
qed simp
also have "\<dots> = (\<Sum>(x',p)\<leftarrow>xs. ennreal p * (\<integral>\<^sup>+ x. indicator {x'} x \<partial>count_space UNIV))"
using assms(1)
- by (intro listsum_cong, simp only: case_prod_unfold, subst nn_integral_cmult [symmetric])
+ by (intro sum_list_cong, simp only: case_prod_unfold, subst nn_integral_cmult [symmetric])
(auto intro!: assms(1) simp: max_def times_ereal.simps [symmetric] mult_ac ereal_indicator
simp del: times_ereal.simps)+
- also from assms have "\<dots> = listsum (map snd xs)" by (simp add: case_prod_unfold listsum_ennreal)
+ also from assms have "\<dots> = sum_list (map snd xs)" by (simp add: case_prod_unfold sum_list_ennreal)
also have "\<dots> = 1" using assms(2) by simp
finally show ?thesis .
qed
lemma pmf_pmf_of_list:
assumes "pmf_of_list_wf xs"
- shows "pmf (pmf_of_list xs) x = listsum (map snd (filter (\<lambda>z. fst z = x) xs))"
+ shows "pmf (pmf_of_list xs) x = sum_list (map snd (filter (\<lambda>z. fst z = x) xs))"
using assms pmf_of_list_aux[of xs] unfolding pmf_of_list_def pmf_of_list_wf_def
- by (subst pmf_embed_pmf) (auto intro!: listsum_nonneg)
+ by (subst pmf_embed_pmf) (auto intro!: sum_list_nonneg)
end
@@ -1930,16 +1930,16 @@
lemma emeasure_pmf_of_list:
assumes "pmf_of_list_wf xs"
- shows "emeasure (pmf_of_list xs) A = ennreal (listsum (map snd (filter (\<lambda>x. fst x \<in> A) xs)))"
+ shows "emeasure (pmf_of_list xs) A = ennreal (sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs)))"
proof -
have "emeasure (pmf_of_list xs) A = nn_integral (measure_pmf (pmf_of_list xs)) (indicator A)"
by simp
also from assms
- have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (listsum (map snd [z\<leftarrow>xs . fst z = x])))"
+ have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])))"
by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list)
also from assms
- have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. listsum (map snd [z\<leftarrow>xs . fst z = x]))"
- by (subst setsum_ennreal) (auto simp: pmf_of_list_wf_def intro!: listsum_nonneg)
+ have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. sum_list (map snd [z\<leftarrow>xs . fst z = x]))"
+ by (subst setsum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg)
also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A.
indicator A x * pmf (pmf_of_list xs) x)" (is "_ = ennreal ?S")
using assms by (intro ennreal_cong setsum.cong) (auto simp: pmf_pmf_of_list)
@@ -1948,13 +1948,13 @@
also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x * pmf (pmf_of_list xs) x)"
using assms by (intro setsum.mono_neutral_left set_pmf_of_list) (auto simp: set_pmf_eq)
also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x *
- listsum (map snd (filter (\<lambda>z. fst z = x) xs)))"
+ sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
using assms by (simp add: pmf_pmf_of_list)
- also have "\<dots> = (\<Sum>x\<in>set (map fst xs). listsum (map snd (filter (\<lambda>z. fst z = x \<and> x \<in> A) xs)))"
+ also have "\<dots> = (\<Sum>x\<in>set (map fst xs). sum_list (map snd (filter (\<lambda>z. fst z = x \<and> x \<in> A) xs)))"
by (intro setsum.cong) (auto simp: indicator_def)
also have "\<dots> = (\<Sum>x\<in>set (map fst xs). (\<Sum>xa = 0..<length xs.
if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
- by (intro setsum.cong refl, subst listsum_map_filter', subst listsum_setsum_nth) simp
+ by (intro setsum.cong refl, subst sum_list_map_filter', subst sum_list_setsum_nth) simp
also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs).
if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
by (rule setsum.commute)
@@ -1963,30 +1963,30 @@
by (auto intro!: setsum.cong setsum.neutral)
also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then snd (xs ! xa) else 0)"
by (intro setsum.cong refl) (simp_all add: setsum.delta)
- also have "\<dots> = listsum (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
- by (subst listsum_map_filter', subst listsum_setsum_nth) simp_all
+ also have "\<dots> = sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
+ by (subst sum_list_map_filter', subst sum_list_setsum_nth) simp_all
finally show ?thesis .
qed
lemma measure_pmf_of_list:
assumes "pmf_of_list_wf xs"
- shows "measure (pmf_of_list xs) A = listsum (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
+ shows "measure (pmf_of_list xs) A = sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
using assms unfolding pmf_of_list_wf_def Sigma_Algebra.measure_def
- by (subst emeasure_pmf_of_list [OF assms], subst enn2real_ennreal) (auto intro!: listsum_nonneg)
+ by (subst emeasure_pmf_of_list [OF assms], subst enn2real_ennreal) (auto intro!: sum_list_nonneg)
(* TODO Move? *)
-lemma listsum_nonneg_eq_zero_iff:
+lemma sum_list_nonneg_eq_zero_iff:
fixes xs :: "'a :: linordered_ab_group_add list"
- shows "(\<And>x. x \<in> set xs \<Longrightarrow> x \<ge> 0) \<Longrightarrow> listsum xs = 0 \<longleftrightarrow> set xs \<subseteq> {0}"
+ shows "(\<And>x. x \<in> set xs \<Longrightarrow> x \<ge> 0) \<Longrightarrow> sum_list xs = 0 \<longleftrightarrow> set xs \<subseteq> {0}"
proof (induction xs)
case (Cons x xs)
- from Cons.prems have "listsum (x#xs) = 0 \<longleftrightarrow> x = 0 \<and> listsum xs = 0"
- unfolding listsum_simps by (subst add_nonneg_eq_0_iff) (auto intro: listsum_nonneg)
+ from Cons.prems have "sum_list (x#xs) = 0 \<longleftrightarrow> x = 0 \<and> sum_list xs = 0"
+ unfolding sum_list_simps by (subst add_nonneg_eq_0_iff) (auto intro: sum_list_nonneg)
with Cons.IH Cons.prems show ?case by simp
qed simp_all
-lemma listsum_filter_nonzero:
- "listsum (filter (\<lambda>x. x \<noteq> 0) xs) = listsum xs"
+lemma sum_list_filter_nonzero:
+ "sum_list (filter (\<lambda>x. x \<noteq> 0) xs) = sum_list xs"
by (induction xs) simp_all
(* END MOVE *)
@@ -1997,11 +1997,11 @@
{
fix x assume A: "x \<in> fst ` set xs" and B: "x \<notin> set_pmf (pmf_of_list xs)"
then obtain y where y: "(x, y) \<in> set xs" by auto
- from B have "listsum (map snd [z\<leftarrow>xs. fst z = x]) = 0"
+ from B have "sum_list (map snd [z\<leftarrow>xs. fst z = x]) = 0"
by (simp add: pmf_pmf_of_list[OF assms(1)] set_pmf_eq)
moreover from y have "y \<in> snd ` {xa \<in> set xs. fst xa = x}" by force
ultimately have "y = 0" using assms(1)
- by (subst (asm) listsum_nonneg_eq_zero_iff) (auto simp: pmf_of_list_wf_def)
+ by (subst (asm) sum_list_nonneg_eq_zero_iff) (auto simp: pmf_of_list_wf_def)
with assms(2) y have False by force
}
thus "fst ` set xs \<subseteq> set_pmf (pmf_of_list xs)" by blast
@@ -2015,8 +2015,8 @@
have "map snd [z\<leftarrow>xs . snd z \<noteq> 0] = filter (\<lambda>x. x \<noteq> 0) (map snd xs)"
by (induction xs) simp_all
with assms(1) show wf: "pmf_of_list_wf xs'"
- by (auto simp: pmf_of_list_wf_def xs'_def listsum_filter_nonzero)
- have "listsum (map snd [z\<leftarrow>xs' . fst z = i]) = listsum (map snd [z\<leftarrow>xs . fst z = i])" for i
+ by (auto simp: pmf_of_list_wf_def xs'_def sum_list_filter_nonzero)
+ have "sum_list (map snd [z\<leftarrow>xs' . fst z = i]) = sum_list (map snd [z\<leftarrow>xs . fst z = i])" for i
unfolding xs'_def by (induction xs) simp_all
with assms(1) wf show "pmf_of_list xs' = pmf_of_list xs"
by (intro pmf_eqI) (simp_all add: pmf_pmf_of_list)
--- a/src/HOL/Proofs/Lambda/ListApplication.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Proofs/Lambda/ListApplication.thy Thu Sep 15 11:48:20 2016 +0200
@@ -110,8 +110,8 @@
prefer 2
apply (erule allE, erule mp, rule refl)
apply simp
- apply (simp only: foldl_conv_fold add.commute fold_plus_listsum_rev)
- apply (fastforce simp add: listsum_map_remove1)
+ apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
+ apply (fastforce simp add: sum_list_map_remove1)
apply clarify
apply (rule assms)
apply (erule allE, erule impE)
@@ -126,8 +126,8 @@
apply (rule le_imp_less_Suc)
apply (rule trans_le_add1)
apply (rule trans_le_add2)
- apply (simp only: foldl_conv_fold add.commute fold_plus_listsum_rev)
- apply (simp add: member_le_listsum_nat)
+ apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
+ apply (simp add: member_le_sum_list_nat)
done
theorem Apps_dB_induct:
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Thu Sep 15 11:48:20 2016 +0200
@@ -204,7 +204,7 @@
oops
lemma
- "ns ! k < length ns ==> k <= listsum ns"
+ "ns ! k < length ns ==> k <= sum_list ns"
quickcheck[random, iterations = 10000, finite_types = false, quiet]
quickcheck[exhaustive, finite_types = false, expect = counterexample]
oops
--- a/src/HOL/Random.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Random.thy Thu Sep 15 11:48:20 2016 +0200
@@ -79,7 +79,7 @@
"pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))"
lemma pick_member:
- "i < listsum (map fst xs) \<Longrightarrow> pick xs i \<in> set (map snd xs)"
+ "i < sum_list (map fst xs) \<Longrightarrow> pick xs i \<in> set (map snd xs)"
by (induct xs arbitrary: i) (simp_all add: less_natural_def)
lemma pick_drop_zero:
@@ -95,17 +95,17 @@
qed
definition select_weight :: "(natural \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
- "select_weight xs = range (listsum (map fst xs))
+ "select_weight xs = range (sum_list (map fst xs))
\<circ>\<rightarrow> (\<lambda>k. Pair (pick xs k))"
lemma select_weight_member:
- assumes "0 < listsum (map fst xs)"
+ assumes "0 < sum_list (map fst xs)"
shows "fst (select_weight xs s) \<in> set (map snd xs)"
proof -
from range assms
- have "fst (range (listsum (map fst xs)) s) < listsum (map fst xs)" .
+ have "fst (range (sum_list (map fst xs)) s) < sum_list (map fst xs)" .
with pick_member
- have "pick xs (fst (range (listsum (map fst xs)) s)) \<in> set (map snd xs)" .
+ have "pick xs (fst (range (sum_list (map fst xs)) s)) \<in> set (map snd xs)" .
then show ?thesis by (simp add: select_weight_def scomp_def split_def)
qed
@@ -116,7 +116,7 @@
lemma select_weight_drop_zero:
"select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
proof -
- have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
+ have "sum_list (map fst [(k, _)\<leftarrow>xs . 0 < k]) = sum_list (map fst xs)"
by (induct xs) (auto simp add: less_natural_def natural_eq_iff)
then show ?thesis by (simp only: select_weight_def pick_drop_zero)
qed
@@ -127,7 +127,7 @@
proof -
have less: "\<And>s. fst (range (natural_of_nat (length xs)) s) < natural_of_nat (length xs)"
using assms by (intro range) (simp add: less_natural_def)
- moreover have "listsum (map fst (map (Pair 1) xs)) = natural_of_nat (length xs)"
+ moreover have "sum_list (map fst (map (Pair 1) xs)) = natural_of_nat (length xs)"
by (induct xs) simp_all
ultimately show ?thesis
by (auto simp add: select_weight_def select_def scomp_def split_def
--- a/src/HOL/UNITY/Comp/AllocBase.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Thu Sep 15 11:48:20 2016 +0200
@@ -14,7 +14,7 @@
abbreviation (input) tokens :: "nat list \<Rightarrow> nat"
where
- "tokens \<equiv> listsum"
+ "tokens \<equiv> sum_list"
abbreviation (input)
"bag_of \<equiv> mset"
--- a/src/HOL/ex/Gauge_Integration.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/ex/Gauge_Integration.thy Thu Sep 15 11:48:20 2016 +0200
@@ -204,7 +204,7 @@
ultimately show ?case by simp
qed auto
-lemma fine_listsum_eq_diff:
+lemma fine_sum_list_eq_diff:
fixes f :: "real \<Rightarrow> real"
shows "fine \<delta> (a, b) D \<Longrightarrow> (\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
by (induct set: fine) simp_all
@@ -249,7 +249,7 @@
by (induct D, auto simp add: algebra_simps)
lemma rsum_append: "rsum (D1 @ D2) f = rsum D1 f + rsum D2 f"
-unfolding rsum_def map_append listsum_append ..
+unfolding rsum_def map_append sum_list_append ..
subsection \<open>Gauge integrability (definite)\<close>
@@ -594,22 +594,22 @@
proof (clarify)
fix D assume D: "fine \<delta> (a, b) D"
hence "(\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
- by (rule fine_listsum_eq_diff)
+ by (rule fine_sum_list_eq_diff)
hence "\<bar>rsum D f' - (f b - f a)\<bar> = \<bar>rsum D f' - (\<Sum>(u, x, v)\<leftarrow>D. f v - f u)\<bar>"
by simp
also have "\<dots> = \<bar>(\<Sum>(u, x, v)\<leftarrow>D. f v - f u) - rsum D f'\<bar>"
by (rule abs_minus_commute)
also have "\<dots> = \<bar>\<Sum>(u, x, v)\<leftarrow>D. (f v - f u) - f' x * (v - u)\<bar>"
- by (simp only: rsum_def listsum_subtractf split_def)
+ by (simp only: rsum_def sum_list_subtractf split_def)
also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. \<bar>(f v - f u) - f' x * (v - u)\<bar>)"
- by (rule ord_le_eq_trans [OF listsum_abs], simp add: o_def split_def)
+ by (rule ord_le_eq_trans [OF sum_list_abs], simp add: o_def split_def)
also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))"
- apply (rule listsum_mono, clarify, rename_tac u x v)
+ apply (rule sum_list_mono, clarify, rename_tac u x v)
using D apply (simp add: \<delta> mem_fine mem_fine2 mem_fine3)
done
also have "\<dots> = e"
- using fine_listsum_eq_diff [OF D, where f="\<lambda>x. x"]
- unfolding split_def listsum_const_mult
+ using fine_sum_list_eq_diff [OF D, where f="\<lambda>x. x"]
+ unfolding split_def sum_list_const_mult
using \<open>a < b\<close> by simp
finally show "\<bar>rsum D f' - (f b - f a)\<bar> \<le> e" .
qed
--- a/src/HOL/ex/Parallel_Example.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/ex/Parallel_Example.thy Thu Sep 15 11:48:20 2016 +0200
@@ -9,7 +9,7 @@
subsubsection \<open>Fragments of the harmonic series\<close>
definition harmonic :: "nat \<Rightarrow> rat" where
- "harmonic n = listsum (map (\<lambda>n. 1 / of_nat n) [1..<n])"
+ "harmonic n = sum_list (map (\<lambda>n. 1 / of_nat n) [1..<n])"
subsubsection \<open>The sieve of Erathostenes\<close>
--- a/src/HOL/ex/Perm_Fragments.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/ex/Perm_Fragments.thy Thu Sep 15 11:48:20 2016 +0200
@@ -11,8 +11,8 @@
text \<open>On cycles\<close>
-lemma cycle_listprod:
- "\<langle>a # as\<rangle> = listprod (map (\<lambda>b. \<langle>a\<leftrightarrow>b\<rangle>) (rev as))"
+lemma cycle_prod_list:
+ "\<langle>a # as\<rangle> = prod_list (map (\<lambda>b. \<langle>a\<leftrightarrow>b\<rangle>) (rev as))"
by (induct as) simp_all
lemma cycle_append [simp]:
--- a/src/HOL/ex/Primrec.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/ex/Primrec.thy Thu Sep 15 11:48:20 2016 +0200
@@ -224,16 +224,16 @@
text \<open>MAIN RESULT\<close>
-lemma SC_case: "SC l < ack 1 (listsum l)"
+lemma SC_case: "SC l < ack 1 (sum_list l)"
apply (unfold SC_def)
apply (induct l)
apply (simp_all add: le_add1 le_imp_less_Suc)
done
-lemma CONSTANT_case: "CONSTANT k l < ack k (listsum l)"
+lemma CONSTANT_case: "CONSTANT k l < ack k (sum_list l)"
by simp
-lemma PROJ_case: "PROJ i l < ack 0 (listsum l)"
+lemma PROJ_case: "PROJ i l < ack 0 (sum_list l)"
apply (simp add: PROJ_def)
apply (induct l arbitrary:i)
apply (auto simp add: drop_Cons split: nat.split)
@@ -243,8 +243,8 @@
text \<open>@{term COMP} case\<close>
-lemma COMP_map_aux: "\<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (listsum l))
- ==> \<exists>k. \<forall>l. listsum (map (\<lambda>f. f l) fs) < ack k (listsum l)"
+lemma COMP_map_aux: "\<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (sum_list l))
+ ==> \<exists>k. \<forall>l. sum_list (map (\<lambda>f. f l) fs) < ack k (sum_list l)"
apply (induct fs)
apply (rule_tac x = 0 in exI)
apply simp
@@ -253,9 +253,9 @@
done
lemma COMP_case:
- "\<forall>l. g l < ack kg (listsum l) ==>
- \<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (listsum l))
- ==> \<exists>k. \<forall>l. COMP g fs l < ack k (listsum l)"
+ "\<forall>l. g l < ack kg (sum_list l) ==>
+ \<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (sum_list l))
+ ==> \<exists>k. \<forall>l. COMP g fs l < ack k (sum_list l)"
apply (unfold COMP_def)
apply (drule COMP_map_aux)
apply (meson ack_less_mono2 ack_nest_bound less_trans)
@@ -265,9 +265,9 @@
text \<open>@{term PREC} case\<close>
lemma PREC_case_aux:
- "\<forall>l. f l + listsum l < ack kf (listsum l) ==>
- \<forall>l. g l + listsum l < ack kg (listsum l) ==>
- PREC f g l + listsum l < ack (Suc (kf + kg)) (listsum l)"
+ "\<forall>l. f l + sum_list l < ack kf (sum_list l) ==>
+ \<forall>l. g l + sum_list l < ack kg (sum_list l) ==>
+ PREC f g l + sum_list l < ack (Suc (kf + kg)) (sum_list l)"
apply (unfold PREC_def)
apply (case_tac l)
apply simp_all
@@ -290,12 +290,12 @@
done
lemma PREC_case:
- "\<forall>l. f l < ack kf (listsum l) ==>
- \<forall>l. g l < ack kg (listsum l) ==>
- \<exists>k. \<forall>l. PREC f g l < ack k (listsum l)"
+ "\<forall>l. f l < ack kf (sum_list l) ==>
+ \<forall>l. g l < ack kg (sum_list l) ==>
+ \<exists>k. \<forall>l. PREC f g l < ack k (sum_list l)"
by (metis le_less_trans [OF le_add1 PREC_case_aux] ack_add_bound2)
-lemma ack_bounds_PRIMREC: "PRIMREC f ==> \<exists>k. \<forall>l. f l < ack k (listsum l)"
+lemma ack_bounds_PRIMREC: "PRIMREC f ==> \<exists>k. \<forall>l. f l < ack k (sum_list l)"
apply (erule PRIMREC.induct)
apply (blast intro: SC_case CONSTANT_case PROJ_case COMP_case PREC_case)+
done
--- a/src/HOL/ex/Transfer_Int_Nat.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/ex/Transfer_Int_Nat.thy Thu Sep 15 11:48:20 2016 +0200
@@ -116,7 +116,7 @@
text \<open>For derived operations, we can use the \<open>transfer_prover\<close>
method to help generate transfer rules.\<close>
-lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum"
+lemma ZN_sum_list [transfer_rule]: "(list_all2 ZN ===> ZN) sum_list sum_list"
by transfer_prover
end
@@ -178,8 +178,8 @@
lemma
assumes "\<And>x y z::int. \<lbrakk>0 \<le> x; 0 \<le> y; 0 \<le> z\<rbrakk> \<Longrightarrow>
- listsum [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
- shows "listsum [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
+ sum_list [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
+ shows "sum_list [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
apply transfer
apply fact
done
@@ -189,8 +189,8 @@
lemma
assumes "\<And>xs::int list. list_all (\<lambda>x. x \<ge> 0) xs \<Longrightarrow>
- (listsum xs = 0) = list_all (\<lambda>x. x = 0) xs"
- shows "listsum xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs"
+ (sum_list xs = 0) = list_all (\<lambda>x. x = 0) xs"
+ shows "sum_list xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs"
apply transfer
apply fact
done
@@ -200,8 +200,8 @@
lemma
assumes "\<And>xs::int list. \<lbrakk>list_all (\<lambda>x. x \<ge> 0) xs; xs \<noteq> []\<rbrakk> \<Longrightarrow>
- listsum xs < listsum (map (\<lambda>x. x + 1) xs)"
- shows "xs \<noteq> [] \<Longrightarrow> listsum xs < listsum (map Suc xs)"
+ sum_list xs < sum_list (map (\<lambda>x. x + 1) xs)"
+ shows "xs \<noteq> [] \<Longrightarrow> sum_list xs < sum_list (map Suc xs)"
apply transfer
apply fact
done