summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Mon, 22 Jun 2015 11:15:23 +0200 | |

changeset 60541 | 4246da644cca |

parent 60540 | b7b71952c194 |

child 60542 | c5953e3a1e4f |

modernized name

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

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

--- 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)