# HG changeset patch
# User nipkow
# Date 1426580537 -3600
# Node ID 0bb88aa3476886355ebc99d316f6f82bafdf5366
# Parent  5b0003211207747af7eae48ada7e0fddb4c18960
added lemmas

diff -r 5b0003211207 -r 0bb88aa34768 src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Sun Mar 15 23:46:00 2015 +0100
+++ b/src/HOL/Groups_List.thy	Tue Mar 17 09:22:17 2015 +0100
@@ -237,6 +237,38 @@
   "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
   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)"
+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)
+    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"
+      by (simp add: setsum.insert_remove eq_commute)
+    finally show ?thesis .
+  next
+    assume "x \<notin> set xs"
+    hence "\<And>xa. xa \<in> set xs \<Longrightarrow> x \<noteq> xa" by blast
+    thus ?thesis by (simp add: Cons.IH `x \<notin> set xs`)
+  qed
+qed simp
+
+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"
+proof-
+  let ?F = "\<lambda>x. List.count 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)"
+    using assms(2)
+    by(simp add: setsum.union_disjoint[OF _ _ Diff_disjoint] del: Un_Diff_cancel)
+  finally show ?thesis by(simp add:listsum_map_eq_setsum_count)
+qed
+
 
 subsection {* Further facts about @{const List.n_lists} *}
 
diff -r 5b0003211207 -r 0bb88aa34768 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Mar 15 23:46:00 2015 +0100
+++ b/src/HOL/List.thy	Tue Mar 17 09:22:17 2015 +0100
@@ -183,6 +183,12 @@
 
 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
+
 definition
    "extract" :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> ('a list * 'a * 'a list) option"
 where "extract P xs =
@@ -298,6 +304,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 "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}\\
@@ -2151,6 +2158,12 @@
   ultimately show ?thesis by auto
 qed
   
+lemma take_update_cancel[simp]: "n \<le> m \<Longrightarrow> take n (xs[m := y]) = take n xs"
+by(simp add: list_eq_iff_nth_eq)
+
+lemma drop_update_cancel[simp]: "n < m \<Longrightarrow> drop m (xs[n := x]) = drop m xs"
+by(simp add: list_eq_iff_nth_eq)
+
 lemma upd_conv_take_nth_drop:
   "i < length xs \<Longrightarrow> xs[i:=a] = take i xs @ a # drop (Suc i) xs"
 proof -
@@ -2162,6 +2175,22 @@
   finally show ?thesis .
 qed
 
+lemma take_update_swap: "n < m \<Longrightarrow> take m (xs[n := x]) = (take m xs)[n := x]"
+apply(cases "n \<ge> length xs")
+ apply simp
+apply(simp add: upd_conv_take_nth_drop take_Cons drop_take min_def diff_Suc
+  split: nat.split)
+done
+
+lemma drop_update_swap: "m \<le> n \<Longrightarrow> drop m (xs[n := x]) = (drop m xs)[n-m := x]"
+apply(cases "n \<ge> length xs")
+ apply simp
+apply(simp add: upd_conv_take_nth_drop drop_take)
+done
+
+lemma nth_image: "l \<le> size xs \<Longrightarrow> nth xs ` {0..<l} = set(take l xs)"
+by(auto simp: set_conv_nth image_def) (metis Suc_le_eq nth_take order_trans)
+
 
 subsubsection {* @{const takeWhile} and @{const dropWhile} *}
 
@@ -3211,6 +3240,9 @@
   "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
 by(auto simp: distinct_conv_nth)
 
+lemma inj_on_nth: "distinct xs \<Longrightarrow> \<forall>i \<in> I. i < length xs \<Longrightarrow> inj_on (nth xs) I"
+by (rule inj_onI) (simp add: nth_eq_iff_index_eq)
+
 lemma set_update_distinct: "\<lbrakk> distinct xs;  n < length xs \<rbrakk> \<Longrightarrow>
   set(xs[n := x]) = insert x (set xs - {xs!n})"
 by(auto simp: set_eq_iff in_set_conv_nth nth_list_update nth_eq_iff_index_eq)
@@ -3669,6 +3701,22 @@
 by (induct xs) simp_all
 
 
+subsubsection {* @{const List.count} *}
+
+lemma count_notin[simp]: "x \<notin> set xs \<Longrightarrow> List.count xs x = 0"
+by (induction xs) auto
+
+lemma count_le_length: "List.count 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"
+apply(induction xs arbitrary: X)
+ apply simp
+apply (simp add: setsum.If_cases)
+by (metis Diff_eq setsum.remove)
+
+
 subsubsection {* @{const List.extract} *}
 
 lemma extract_None_iff: "List.extract P xs = None \<longleftrightarrow> \<not> (\<exists> x\<in>set xs. P x)"