# HG changeset patch
# User haftmann
# Date 1411578681 -7200
# Node ID 8d124c73c37adf0a1e42dbeecfbd08a1459a76c8
# Parent  fe9de4089345a80b4d712ca6083fe7392d1b0989
added lemmas

diff -r fe9de4089345 -r 8d124c73c37a src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Wed Sep 24 19:10:30 2014 +0200
+++ b/src/HOL/Groups_Big.thy	Wed Sep 24 19:11:21 2014 +0200
@@ -997,6 +997,10 @@
   finally show ?thesis by auto
 qed
 
+lemma (in ordered_comm_monoid_add) setsum_pos: 
+  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
+  by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
+
 
 subsubsection {* Cardinality of products *}
 
@@ -1192,8 +1196,4 @@
   "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
 
-lemma (in ordered_comm_monoid_add) setsum_pos: 
-  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
-  by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
-
 end
diff -r fe9de4089345 -r 8d124c73c37a src/HOL/Library/Groups_Big_Fun.thy
--- a/src/HOL/Library/Groups_Big_Fun.thy	Wed Sep 24 19:10:30 2014 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy	Wed Sep 24 19:11:21 2014 +0200
@@ -285,6 +285,12 @@
       setsum_product)
 qed
 
+lemma Sum_any_eq_zero_iff [simp]: 
+  fixes f :: "'a \<Rightarrow> nat"
+  assumes "finite {a. f a \<noteq> 0}"
+  shows "Sum_any f = 0 \<longleftrightarrow> f = (\<lambda>_. 0)"
+  using assms by (simp add: Sum_any.expand_set fun_eq_iff)
+
 
 subsection \<open>Concrete product\<close>
 
@@ -337,4 +343,15 @@
   shows "f a \<noteq> 0"
   using assms Prod_any_zero [of f] by blast
 
+lemma power_Sum_any:
+  assumes "finite {a. f a \<noteq> 0}"
+  shows "c ^ (\<Sum>a. f a) = (\<Prod>a. c ^ f a)"
+proof -
+  have "{a. c ^ f a \<noteq> 1} \<subseteq> {a. f a \<noteq> 0}"
+    by (auto intro: ccontr)
+  with assms show ?thesis
+    by (simp add: Sum_any.expand_set Prod_any.expand_superset power_setsum)
+qed
+
 end
+
diff -r fe9de4089345 -r 8d124c73c37a src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Wed Sep 24 19:10:30 2014 +0200
+++ b/src/HOL/Library/More_List.thy	Wed Sep 24 19:11:21 2014 +0200
@@ -182,47 +182,86 @@
 
 definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a"
 where
-  "nth_default x xs n = (if n < length xs then xs ! n else x)"
-
-lemma nth_default_Nil [simp]:
-  "nth_default y [] n = y"
-  by (simp add: nth_default_def)
-
-lemma nth_default_Cons_0 [simp]:
-  "nth_default y (x # xs) 0 = x"
-  by (simp add: nth_default_def)
-
-lemma nth_default_Cons_Suc [simp]:
-  "nth_default y (x # xs) (Suc n) = nth_default y xs n"
-  by (simp add: nth_default_def)
-
-lemma nth_default_map_eq:
-  "f y = x \<Longrightarrow> nth_default x (map f xs) n = f (nth_default y xs n)"
-  by (simp add: nth_default_def)
-
-lemma nth_default_strip_while_eq [simp]:
-  "nth_default x (strip_while (HOL.eq x) xs) n = nth_default x xs n"
-proof -
-  from split_strip_while_append obtain ys zs
-    where "strip_while (HOL.eq x) xs = ys" and "\<forall>z\<in>set zs. x = z" and "xs = ys @ zs" by blast
-  then show ?thesis by (simp add: nth_default_def not_less nth_append)
-qed
-
-lemma nth_default_Cons:
-  "nth_default y (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default y xs n')"
-  by (simp split: nat.split)
+  "nth_default dflt xs n = (if n < length xs then xs ! n else dflt)"
 
 lemma nth_default_nth:
-  "n < length xs \<Longrightarrow> nth_default y xs n = xs ! n"
+  "n < length xs \<Longrightarrow> nth_default dflt xs n = xs ! n"
   by (simp add: nth_default_def)
 
 lemma nth_default_beyond:
-  "length xs \<le> n \<Longrightarrow> nth_default y xs n = y"
+  "length xs \<le> n \<Longrightarrow> nth_default dflt xs n = dflt"
+  by (simp add: nth_default_def)
+
+lemma nth_default_Nil [simp]:
+  "nth_default dflt [] n = dflt"
+  by (simp add: nth_default_def)
+
+lemma nth_default_Cons:
+  "nth_default dflt (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default dflt xs n')"
+  by (simp add: nth_default_def split: nat.split)
+
+lemma nth_default_Cons_0 [simp]:
+  "nth_default dflt (x # xs) 0 = x"
+  by (simp add: nth_default_Cons)
+
+lemma nth_default_Cons_Suc [simp]:
+  "nth_default dflt (x # xs) (Suc n) = nth_default dflt xs n"
+  by (simp add: nth_default_Cons)
+
+lemma nth_default_replicate_dflt [simp]:
+  "nth_default dflt (replicate n dflt) m = dflt"
   by (simp add: nth_default_def)
 
+lemma nth_default_append:
+  "nth_default dflt (xs @ ys) n =
+    (if n < length xs then nth xs n else nth_default dflt ys (n - length xs))"
+  by (auto simp add: nth_default_def nth_append)
+
+lemma nth_default_append_trailing [simp]:
+  "nth_default dflt (xs @ replicate n dflt) = nth_default dflt xs"
+  by (simp add: fun_eq_iff nth_default_append) (simp add: nth_default_def)
+
+lemma nth_default_snoc_default [simp]:
+  "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
+  by (auto simp add: nth_default_def fun_eq_iff nth_append)
+
+lemma nth_default_eq_dflt_iff:
+  "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
+  by (simp add: nth_default_def)
+
+lemma in_enumerate_iff_nth_default_eq:
+  "x \<noteq> dflt \<Longrightarrow> (n, x) \<in> set (enumerate 0 xs) \<longleftrightarrow> nth_default dflt xs n = x"
+  by (auto simp add: nth_default_def in_set_conv_nth enumerate_eq_zip)
+
+lemma last_conv_nth_default:
+  assumes "xs \<noteq> []"
+  shows "last xs = nth_default dflt xs (length xs - 1)"
+  using assms by (simp add: nth_default_def last_conv_nth)
+  
+lemma nth_default_map_eq:
+  "f dflt' = dflt \<Longrightarrow> nth_default dflt (map f xs) n = f (nth_default dflt' xs n)"
+  by (simp add: nth_default_def)
+
+lemma finite_nth_default_neq_default [simp]:
+  "finite {k. nth_default dflt xs k \<noteq> dflt}"
+  by (simp add: nth_default_def)
+
+lemma sorted_list_of_set_nth_default:
+  "sorted_list_of_set {k. nth_default dflt xs k \<noteq> dflt} = map fst (filter (\<lambda>(_, x). x \<noteq> dflt) (enumerate 0 xs))"
+  by (rule sorted_distinct_set_unique) (auto simp add: nth_default_def in_set_conv_nth
+    sorted_filter distinct_map_filter enumerate_eq_zip intro: rev_image_eqI)
+
+lemma map_nth_default:
+  "map (nth_default x xs) [0..<length xs] = xs"
+proof -
+  have *: "map (nth_default x xs) [0..<length xs] = map (List.nth xs) [0..<length xs]"
+    by (rule map_cong) (simp_all add: nth_default_nth)
+  show ?thesis by (simp add: * map_nth)
+qed
+
 lemma range_nth_default [simp]:
   "range (nth_default dflt xs) = insert dflt (set xs)"
-  by (auto simp add: nth_default_def[abs_def] in_set_conv_nth)
+  by (auto simp add: nth_default_def [abs_def] in_set_conv_nth)
 
 lemma nth_strip_while:
   assumes "n < length (strip_while P xs)"
@@ -241,25 +280,59 @@
   by (subst (2) length_rev[symmetric])
     (simp add: strip_while_def length_dropWhile_le del: length_rev)
 
-lemma finite_nth_default_neq_default [simp]:
-  "finite {k. nth_default dflt xs k \<noteq> dflt}"
-  by (simp add: nth_default_def)
-
-lemma sorted_list_of_set_nth_default:
-  "sorted_list_of_set {k. nth_default dflt xs k \<noteq> dflt} = map fst (filter (\<lambda>(_, x). x \<noteq> dflt) (zip [0..<length xs] xs))"
-  by (rule sorted_distinct_set_unique) (auto simp add: nth_default_def in_set_conv_nth sorted_filter distinct_map_filter intro: rev_image_eqI)
-
-lemma nth_default_snoc_default [simp]:
-  "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
-  by (auto simp add: nth_default_def fun_eq_iff nth_append)
-
 lemma nth_default_strip_while_dflt [simp]:
- "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs"
+  "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs"
   by (induct xs rule: rev_induct) auto
 
-lemma nth_default_eq_dflt_iff:
-  "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
-  by (simp add: nth_default_def)
+lemma nth_default_eq_iff:
+  "nth_default dflt xs = nth_default dflt ys
+     \<longleftrightarrow> strip_while (HOL.eq dflt) xs = strip_while (HOL.eq dflt) ys" (is "?P \<longleftrightarrow> ?Q")
+proof
+  let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
+  assume ?P
+  then have eq: "nth_default dflt ?xs = nth_default dflt ?ys"
+    by simp
+  have len: "length ?xs = length ?ys"
+  proof (rule ccontr)
+    assume len: "length ?xs \<noteq> length ?ys"
+    { fix xs ys :: "'a list"
+      let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
+      assume eq: "nth_default dflt ?xs = nth_default dflt ?ys"
+      assume len: "length ?xs < length ?ys"
+      then have "length ?ys > 0" by arith
+      then have "?ys \<noteq> []" by simp
+      with last_conv_nth_default [of ?ys dflt]
+      have "last ?ys = nth_default dflt ?ys (length ?ys - 1)"
+        by auto
+      moreover from `?ys \<noteq> []` no_trailing_strip_while [of "HOL.eq dflt" ys]
+        have "last ?ys \<noteq> dflt" by (simp add: no_trailing_unfold)
+      ultimately have "nth_default dflt ?xs (length ?ys - 1) \<noteq> dflt"
+        using eq by simp
+      moreover from len have "length ?ys - 1 \<ge> length ?xs" by simp
+      ultimately have False by (simp only: nth_default_beyond) simp
+    } 
+    from this [of xs ys] this [of ys xs] len eq show False
+      by (auto simp only: linorder_class.neq_iff)
+  qed
+  then show ?Q
+  proof (rule nth_equalityI [rule_format])
+    fix n
+    assume "n < length ?xs"
+    moreover with len have "n < length ?ys"
+      by simp
+    ultimately have xs: "nth_default dflt ?xs n = ?xs ! n"
+      and ys: "nth_default dflt ?ys n = ?ys ! n"
+      by (simp_all only: nth_default_nth)
+    with eq show "?xs ! n = ?ys ! n"
+      by simp
+  qed
+next
+  assume ?Q
+  then have "nth_default dflt (strip_while (HOL.eq dflt) xs) = nth_default dflt (strip_while (HOL.eq dflt) ys)"
+    by simp
+  then show ?P
+    by simp
+qed
 
 end
 
diff -r fe9de4089345 -r 8d124c73c37a src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Sep 24 19:10:30 2014 +0200
+++ b/src/HOL/List.thy	Wed Sep 24 19:11:21 2014 +0200
@@ -2796,6 +2796,10 @@
   "fold g (map f xs) = fold (g o f) xs"
   by (induct xs) simp_all
 
+lemma fold_filter:
+  "fold f (filter P xs) = fold (\<lambda>x. if P x then f x else id) xs"
+  by (induct xs) simp_all
+
 lemma fold_rev:
   assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
   shows "fold f (rev xs) = fold f xs"
@@ -2942,6 +2946,10 @@
   "foldr g (map f xs) a = foldr (g o f) xs a"
   by (simp add: foldr_conv_fold fold_map rev_map)
 
+lemma foldr_filter:
+  "foldr f (filter P xs) = foldr (\<lambda>x. if P x then f x else id) xs"
+  by (simp add: foldr_conv_fold rev_filter fold_filter)
+  
 lemma foldl_map [code_unfold]:
   "foldl g a (map f xs) = foldl (\<lambda>a x. g a (f x)) a xs"
   by (simp add: foldl_conv_fold fold_map comp_def)
@@ -3030,6 +3038,7 @@
   "map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]"
   by (induct n) simp_all
 
+ 
 lemma nth_take_lemma:
   "k <= length xs ==> k <= length ys ==>
      (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
@@ -3479,6 +3488,18 @@
   by (induct xs rule: remdups_adj.induct, 
       auto simp add: injD[OF assms])
 
+lemma remdups_upt [simp]:
+  "remdups [m..<n] = [m..<n]"
+proof (cases "m \<le> n")
+  case False then show ?thesis by simp
+next
+  case True then obtain q where "n = m + q"
+    by (auto simp add: le_iff_add)
+  moreover have "remdups [m..<m + q] = [m..<m + q]"
+    by (induct q) simp_all
+  ultimately show ?thesis by simp
+qed
+
 
 subsubsection {* @{const insert} *}
 
@@ -3699,6 +3720,15 @@
 lemma length_replicate [simp]: "length (replicate n x) = n"
 by (induct n) auto
 
+lemma replicate_eqI:
+  assumes "length xs = n" and "\<And>y. y \<in> set xs \<Longrightarrow> y = x"
+  shows "xs = replicate n x"
+using assms proof (induct xs arbitrary: n)
+  case Nil then show ?case by simp
+next
+  case (Cons x xs) then show ?case by (cases n) simp_all
+qed
+
 lemma Ex_list_of_length: "\<exists>xs. length xs = n"
 by (rule exI[of _ "replicate n undefined"]) simp
 
@@ -3951,6 +3981,18 @@
   "distinct (enumerate n xs)"
   by (simp add: enumerate_eq_zip distinct_zipI1)
 
+lemma enumerate_append_eq:
+  "enumerate n (xs @ ys) = enumerate n xs @ enumerate (n + length xs) ys"
+  unfolding enumerate_eq_zip apply auto
+  apply (subst zip_append [symmetric]) apply simp
+  apply (subst upt_add_eq_append [symmetric])
+  apply (simp_all add: ac_simps)
+  done
+
+lemma enumerate_map_upt:
+  "enumerate n (map f [n..<m]) = map (\<lambda>k. (k, f k)) [n..<m]"
+  by (cases "n \<le> m") (simp_all add: zip_map2 zip_same_conv_map enumerate_eq_zip)
+  
 
 subsubsection {* @{const rotate1} and @{const rotate} *}
 
@@ -4755,6 +4797,10 @@
 lemma sorted_upt[simp]: "sorted[i..<j]"
 by (induct j) (simp_all add:sorted_append)
 
+lemma sort_upt [simp]:
+  "sort [m..<n] = [m..<n]"
+  by (rule sorted_sort_id) simp
+
 lemma sorted_upto[simp]: "sorted[i..j]"
 apply(induct i j rule:upto.induct)
 apply(subst upto.simps)
@@ -4777,6 +4823,10 @@
   qed
 qed
 
+lemma sorted_enumerate [simp]:
+  "sorted (map fst (enumerate n xs))"
+  by (simp add: enumerate_eq_zip)
+
 
 subsubsection {* @{const transpose} on sorted lists *}
 
diff -r fe9de4089345 -r 8d124c73c37a src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Sep 24 19:10:30 2014 +0200
+++ b/src/HOL/Power.thy	Wed Sep 24 19:11:21 2014 +0200
@@ -795,6 +795,10 @@
     by simp
 qed
 
+lemma power_setsum:
+  "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
+  by (induct A rule: infinite_finite_induct) (simp_all add: power_add)
+
 lemma setprod_gen_delta:
   assumes fS: "finite S"
   shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)"