--- a/src/HOL/Groups_List.thy Sat Jun 20 22:38:39 2015 +0200
+++ b/src/HOL/Groups_List.thy Mon Jun 22 11:15:23 2015 +0200
@@ -238,15 +238,15 @@
using interv_listsum_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. List.count xs x * f x) (set xs)"
+ "listsum (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")
proof cases
assume "x \<in> set xs"
- have "?l = f x + (\<Sum>x\<in>set xs. List.count xs x * f x)" by (simp add: Cons.IH)
+ have "?l = f x + (\<Sum>x\<in>set xs. count_list xs x * f x)" by (simp add: Cons.IH)
also have "set xs = insert x (set xs - {x})" using `x \<in> set xs`by blast
- also have "f x + (\<Sum>x\<in>insert x (set xs - {x}). List.count xs x * f x) = ?r"
+ also have "f x + (\<Sum>x\<in>insert x (set xs - {x}). count_list xs x * f x) = ?r"
by (simp add: setsum.insert_remove eq_commute)
finally show ?thesis .
next
@@ -258,9 +258,9 @@
lemma listsum_map_eq_setsum_count2:
assumes "set xs \<subseteq> X" "finite X"
-shows "listsum (map f xs) = setsum (\<lambda>x. List.count xs x * f x) X"
+shows "listsum (map f xs) = setsum (\<lambda>x. count_list xs x * f x) X"
proof-
- let ?F = "\<lambda>x. List.count xs x * f x"
+ let ?F = "\<lambda>x. count_list xs x * f x"
have "setsum ?F X = setsum ?F (set xs \<union> (X - set xs))"
using Un_absorb1[OF assms(1)] by(simp)
also have "\<dots> = setsum ?F (set xs)"
--- a/src/HOL/List.thy Sat Jun 20 22:38:39 2015 +0200
+++ b/src/HOL/List.thy Mon Jun 22 11:15:23 2015 +0200
@@ -181,13 +181,11 @@
"find _ [] = None" |
"find P (x#xs) = (if P x then Some x else find P xs)"
-hide_const (open) find
-
-primrec count :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where
-"count [] y = 0" |
-"count (x#xs) y = (if x=y then count xs y + 1 else count xs y)"
-
-hide_const (open) count
+text \<open>In the context of multisets, @{text count_list} is equivalent to
+ @{term "count o mset"} and it it advisable to use the latter.\<close>
+primrec count_list :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where
+"count_list [] y = 0" |
+"count_list (x#xs) y = (if x=y then count_list xs y + 1 else count_list xs y)"
definition
"extract" :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> ('a list * 'a * 'a list) option"
@@ -304,7 +302,7 @@
@{lemma "List.union [2,3,4] [0::int,1,2] = [4,3,0,1,2]" by (simp add: List.insert_def List.union_def)}\\
@{lemma "List.find (%i::int. i>0) [0,0] = None" by simp}\\
@{lemma "List.find (%i::int. i>0) [0,1,0,2] = Some 1" by simp}\\
-@{lemma "List.count [0,1,0,2::int] 0 = 2" by (simp)}\\
+@{lemma "count_list [0,1,0,2::int] 0 = 2" by (simp)}\\
@{lemma "List.extract (%i::int. i>0) [0,0] = None" by(simp add: extract_def)}\\
@{lemma "List.extract (%i::int. i>0) [0,1,0,2] = Some([0], 1, [0,2])" by(simp add: extract_def)}\\
@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
@@ -3717,16 +3715,16 @@
by (induct xs) simp_all
-subsubsection {* @{const List.count} *}
-
-lemma count_notin[simp]: "x \<notin> set xs \<Longrightarrow> List.count xs x = 0"
+subsubsection {* @{const count_list} *}
+
+lemma count_notin[simp]: "x \<notin> set xs \<Longrightarrow> count_list xs x = 0"
by (induction xs) auto
-lemma count_le_length: "List.count xs x \<le> length xs"
+lemma count_le_length: "count_list xs x \<le> length xs"
by (induction xs) auto
lemma setsum_count_set:
- "set xs \<subseteq> X \<Longrightarrow> finite X \<Longrightarrow> setsum (List.count xs) X = length xs"
+ "set xs \<subseteq> X \<Longrightarrow> finite X \<Longrightarrow> setsum (count_list xs) X = length xs"
apply(induction xs arbitrary: X)
apply simp
apply (simp add: setsum.If_cases)