# HG changeset patch
# User nipkow
# Date 1434964523 -7200
# Node ID 4246da644cca942c32d40e7996c01b1332f0c9c4
# Parent  b7b71952c1945ea910b173a0cbbefaa498c73c4a
modernized name

diff -r b7b71952c194 -r 4246da644cca src/HOL/Groups_List.thy
--- 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)"
diff -r b7b71952c194 -r 4246da644cca src/HOL/List.thy
--- 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)