modernized name
authornipkow
Mon Jun 22 11:15:23 2015 +0200 (2015-06-22)
changeset 605414246da644cca
parent 60540 b7b71952c194
child 60542 c5953e3a1e4f
modernized name
src/HOL/Groups_List.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Groups_List.thy	Sat Jun 20 22:38:39 2015 +0200
     1.2 +++ b/src/HOL/Groups_List.thy	Mon Jun 22 11:15:23 2015 +0200
     1.3 @@ -238,15 +238,15 @@
     1.4    using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
     1.5  
     1.6  lemma listsum_map_eq_setsum_count:
     1.7 -  "listsum (map f xs) = setsum (\<lambda>x. List.count xs x * f x) (set xs)"
     1.8 +  "listsum (map f xs) = setsum (\<lambda>x. count_list xs x * f x) (set xs)"
     1.9  proof(induction xs)
    1.10    case (Cons x xs)
    1.11    show ?case (is "?l = ?r")
    1.12    proof cases
    1.13      assume "x \<in> set xs"
    1.14 -    have "?l = f x + (\<Sum>x\<in>set xs. List.count xs x * f x)" by (simp add: Cons.IH)
    1.15 +    have "?l = f x + (\<Sum>x\<in>set xs. count_list xs x * f x)" by (simp add: Cons.IH)
    1.16      also have "set xs = insert x (set xs - {x})" using `x \<in> set xs`by blast
    1.17 -    also have "f x + (\<Sum>x\<in>insert x (set xs - {x}). List.count xs x * f x) = ?r"
    1.18 +    also have "f x + (\<Sum>x\<in>insert x (set xs - {x}). count_list xs x * f x) = ?r"
    1.19        by (simp add: setsum.insert_remove eq_commute)
    1.20      finally show ?thesis .
    1.21    next
    1.22 @@ -258,9 +258,9 @@
    1.23  
    1.24  lemma listsum_map_eq_setsum_count2:
    1.25  assumes "set xs \<subseteq> X" "finite X"
    1.26 -shows "listsum (map f xs) = setsum (\<lambda>x. List.count xs x * f x) X"
    1.27 +shows "listsum (map f xs) = setsum (\<lambda>x. count_list xs x * f x) X"
    1.28  proof-
    1.29 -  let ?F = "\<lambda>x. List.count xs x * f x"
    1.30 +  let ?F = "\<lambda>x. count_list xs x * f x"
    1.31    have "setsum ?F X = setsum ?F (set xs \<union> (X - set xs))"
    1.32      using Un_absorb1[OF assms(1)] by(simp)
    1.33    also have "\<dots> = setsum ?F (set xs)"
     2.1 --- a/src/HOL/List.thy	Sat Jun 20 22:38:39 2015 +0200
     2.2 +++ b/src/HOL/List.thy	Mon Jun 22 11:15:23 2015 +0200
     2.3 @@ -181,13 +181,11 @@
     2.4  "find _ [] = None" |
     2.5  "find P (x#xs) = (if P x then Some x else find P xs)"
     2.6  
     2.7 -hide_const (open) find
     2.8 -
     2.9 -primrec count :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where
    2.10 -"count [] y = 0" |
    2.11 -"count (x#xs) y = (if x=y then count xs y + 1 else count xs y)"
    2.12 -
    2.13 -hide_const (open) count
    2.14 +text \<open>In the context of multisets, @{text count_list} is equivalent to
    2.15 +  @{term "count o mset"} and it it advisable to use the latter.\<close>
    2.16 +primrec count_list :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where
    2.17 +"count_list [] y = 0" |
    2.18 +"count_list (x#xs) y = (if x=y then count_list xs y + 1 else count_list xs y)"
    2.19  
    2.20  definition
    2.21     "extract" :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> ('a list * 'a * 'a list) option"
    2.22 @@ -304,7 +302,7 @@
    2.23  @{lemma "List.union [2,3,4] [0::int,1,2] = [4,3,0,1,2]" by (simp add: List.insert_def List.union_def)}\\
    2.24  @{lemma "List.find (%i::int. i>0) [0,0] = None" by simp}\\
    2.25  @{lemma "List.find (%i::int. i>0) [0,1,0,2] = Some 1" by simp}\\
    2.26 -@{lemma "List.count [0,1,0,2::int] 0 = 2" by (simp)}\\
    2.27 +@{lemma "count_list [0,1,0,2::int] 0 = 2" by (simp)}\\
    2.28  @{lemma "List.extract (%i::int. i>0) [0,0] = None" by(simp add: extract_def)}\\
    2.29  @{lemma "List.extract (%i::int. i>0) [0,1,0,2] = Some([0], 1, [0,2])" by(simp add: extract_def)}\\
    2.30  @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
    2.31 @@ -3717,16 +3715,16 @@
    2.32  by (induct xs) simp_all
    2.33  
    2.34  
    2.35 -subsubsection {* @{const List.count} *}
    2.36 -
    2.37 -lemma count_notin[simp]: "x \<notin> set xs \<Longrightarrow> List.count xs x = 0"
    2.38 +subsubsection {* @{const count_list} *}
    2.39 +
    2.40 +lemma count_notin[simp]: "x \<notin> set xs \<Longrightarrow> count_list xs x = 0"
    2.41  by (induction xs) auto
    2.42  
    2.43 -lemma count_le_length: "List.count xs x \<le> length xs"
    2.44 +lemma count_le_length: "count_list xs x \<le> length xs"
    2.45  by (induction xs) auto
    2.46  
    2.47  lemma setsum_count_set:
    2.48 -  "set xs \<subseteq> X \<Longrightarrow> finite X \<Longrightarrow> setsum (List.count xs) X = length xs"
    2.49 +  "set xs \<subseteq> X \<Longrightarrow> finite X \<Longrightarrow> setsum (count_list xs) X = length xs"
    2.50  apply(induction xs arbitrary: X)
    2.51   apply simp
    2.52  apply (simp add: setsum.If_cases)