author | nipkow |

Mon Jun 22 11:15:23 2015 +0200 (2015-06-22) | |

changeset 60541 | 4246da644cca |

parent 60540 | b7b71952c194 |

child 60542 | c5953e3a1e4f |

modernized name

src/HOL/Groups_List.thy | file | annotate | diff | revisions | |

src/HOL/List.thy | file | annotate | diff | revisions |

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)