added lemmas
authorhaftmann
Wed Sep 24 19:11:21 2014 +0200 (2014-09-24)
changeset 584378d124c73c37a
parent 58436 fe9de4089345
child 58438 566117a31cc0
added lemmas
src/HOL/Groups_Big.thy
src/HOL/Library/Groups_Big_Fun.thy
src/HOL/Library/More_List.thy
src/HOL/List.thy
src/HOL/Power.thy
     1.1 --- a/src/HOL/Groups_Big.thy	Wed Sep 24 19:10:30 2014 +0200
     1.2 +++ b/src/HOL/Groups_Big.thy	Wed Sep 24 19:11:21 2014 +0200
     1.3 @@ -997,6 +997,10 @@
     1.4    finally show ?thesis by auto
     1.5  qed
     1.6  
     1.7 +lemma (in ordered_comm_monoid_add) setsum_pos: 
     1.8 +  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
     1.9 +  by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
    1.10 +
    1.11  
    1.12  subsubsection {* Cardinality of products *}
    1.13  
    1.14 @@ -1192,8 +1196,4 @@
    1.15    "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
    1.16  using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
    1.17  
    1.18 -lemma (in ordered_comm_monoid_add) setsum_pos: 
    1.19 -  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
    1.20 -  by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
    1.21 -
    1.22  end
     2.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Wed Sep 24 19:10:30 2014 +0200
     2.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Wed Sep 24 19:11:21 2014 +0200
     2.3 @@ -285,6 +285,12 @@
     2.4        setsum_product)
     2.5  qed
     2.6  
     2.7 +lemma Sum_any_eq_zero_iff [simp]: 
     2.8 +  fixes f :: "'a \<Rightarrow> nat"
     2.9 +  assumes "finite {a. f a \<noteq> 0}"
    2.10 +  shows "Sum_any f = 0 \<longleftrightarrow> f = (\<lambda>_. 0)"
    2.11 +  using assms by (simp add: Sum_any.expand_set fun_eq_iff)
    2.12 +
    2.13  
    2.14  subsection \<open>Concrete product\<close>
    2.15  
    2.16 @@ -337,4 +343,15 @@
    2.17    shows "f a \<noteq> 0"
    2.18    using assms Prod_any_zero [of f] by blast
    2.19  
    2.20 +lemma power_Sum_any:
    2.21 +  assumes "finite {a. f a \<noteq> 0}"
    2.22 +  shows "c ^ (\<Sum>a. f a) = (\<Prod>a. c ^ f a)"
    2.23 +proof -
    2.24 +  have "{a. c ^ f a \<noteq> 1} \<subseteq> {a. f a \<noteq> 0}"
    2.25 +    by (auto intro: ccontr)
    2.26 +  with assms show ?thesis
    2.27 +    by (simp add: Sum_any.expand_set Prod_any.expand_superset power_setsum)
    2.28 +qed
    2.29 +
    2.30  end
    2.31 +
     3.1 --- a/src/HOL/Library/More_List.thy	Wed Sep 24 19:10:30 2014 +0200
     3.2 +++ b/src/HOL/Library/More_List.thy	Wed Sep 24 19:11:21 2014 +0200
     3.3 @@ -182,47 +182,86 @@
     3.4  
     3.5  definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a"
     3.6  where
     3.7 -  "nth_default x xs n = (if n < length xs then xs ! n else x)"
     3.8 -
     3.9 -lemma nth_default_Nil [simp]:
    3.10 -  "nth_default y [] n = y"
    3.11 -  by (simp add: nth_default_def)
    3.12 -
    3.13 -lemma nth_default_Cons_0 [simp]:
    3.14 -  "nth_default y (x # xs) 0 = x"
    3.15 -  by (simp add: nth_default_def)
    3.16 -
    3.17 -lemma nth_default_Cons_Suc [simp]:
    3.18 -  "nth_default y (x # xs) (Suc n) = nth_default y xs n"
    3.19 -  by (simp add: nth_default_def)
    3.20 -
    3.21 -lemma nth_default_map_eq:
    3.22 -  "f y = x \<Longrightarrow> nth_default x (map f xs) n = f (nth_default y xs n)"
    3.23 -  by (simp add: nth_default_def)
    3.24 -
    3.25 -lemma nth_default_strip_while_eq [simp]:
    3.26 -  "nth_default x (strip_while (HOL.eq x) xs) n = nth_default x xs n"
    3.27 -proof -
    3.28 -  from split_strip_while_append obtain ys zs
    3.29 -    where "strip_while (HOL.eq x) xs = ys" and "\<forall>z\<in>set zs. x = z" and "xs = ys @ zs" by blast
    3.30 -  then show ?thesis by (simp add: nth_default_def not_less nth_append)
    3.31 -qed
    3.32 -
    3.33 -lemma nth_default_Cons:
    3.34 -  "nth_default y (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default y xs n')"
    3.35 -  by (simp split: nat.split)
    3.36 +  "nth_default dflt xs n = (if n < length xs then xs ! n else dflt)"
    3.37  
    3.38  lemma nth_default_nth:
    3.39 -  "n < length xs \<Longrightarrow> nth_default y xs n = xs ! n"
    3.40 +  "n < length xs \<Longrightarrow> nth_default dflt xs n = xs ! n"
    3.41    by (simp add: nth_default_def)
    3.42  
    3.43  lemma nth_default_beyond:
    3.44 -  "length xs \<le> n \<Longrightarrow> nth_default y xs n = y"
    3.45 +  "length xs \<le> n \<Longrightarrow> nth_default dflt xs n = dflt"
    3.46 +  by (simp add: nth_default_def)
    3.47 +
    3.48 +lemma nth_default_Nil [simp]:
    3.49 +  "nth_default dflt [] n = dflt"
    3.50 +  by (simp add: nth_default_def)
    3.51 +
    3.52 +lemma nth_default_Cons:
    3.53 +  "nth_default dflt (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default dflt xs n')"
    3.54 +  by (simp add: nth_default_def split: nat.split)
    3.55 +
    3.56 +lemma nth_default_Cons_0 [simp]:
    3.57 +  "nth_default dflt (x # xs) 0 = x"
    3.58 +  by (simp add: nth_default_Cons)
    3.59 +
    3.60 +lemma nth_default_Cons_Suc [simp]:
    3.61 +  "nth_default dflt (x # xs) (Suc n) = nth_default dflt xs n"
    3.62 +  by (simp add: nth_default_Cons)
    3.63 +
    3.64 +lemma nth_default_replicate_dflt [simp]:
    3.65 +  "nth_default dflt (replicate n dflt) m = dflt"
    3.66    by (simp add: nth_default_def)
    3.67  
    3.68 +lemma nth_default_append:
    3.69 +  "nth_default dflt (xs @ ys) n =
    3.70 +    (if n < length xs then nth xs n else nth_default dflt ys (n - length xs))"
    3.71 +  by (auto simp add: nth_default_def nth_append)
    3.72 +
    3.73 +lemma nth_default_append_trailing [simp]:
    3.74 +  "nth_default dflt (xs @ replicate n dflt) = nth_default dflt xs"
    3.75 +  by (simp add: fun_eq_iff nth_default_append) (simp add: nth_default_def)
    3.76 +
    3.77 +lemma nth_default_snoc_default [simp]:
    3.78 +  "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
    3.79 +  by (auto simp add: nth_default_def fun_eq_iff nth_append)
    3.80 +
    3.81 +lemma nth_default_eq_dflt_iff:
    3.82 +  "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
    3.83 +  by (simp add: nth_default_def)
    3.84 +
    3.85 +lemma in_enumerate_iff_nth_default_eq:
    3.86 +  "x \<noteq> dflt \<Longrightarrow> (n, x) \<in> set (enumerate 0 xs) \<longleftrightarrow> nth_default dflt xs n = x"
    3.87 +  by (auto simp add: nth_default_def in_set_conv_nth enumerate_eq_zip)
    3.88 +
    3.89 +lemma last_conv_nth_default:
    3.90 +  assumes "xs \<noteq> []"
    3.91 +  shows "last xs = nth_default dflt xs (length xs - 1)"
    3.92 +  using assms by (simp add: nth_default_def last_conv_nth)
    3.93 +  
    3.94 +lemma nth_default_map_eq:
    3.95 +  "f dflt' = dflt \<Longrightarrow> nth_default dflt (map f xs) n = f (nth_default dflt' xs n)"
    3.96 +  by (simp add: nth_default_def)
    3.97 +
    3.98 +lemma finite_nth_default_neq_default [simp]:
    3.99 +  "finite {k. nth_default dflt xs k \<noteq> dflt}"
   3.100 +  by (simp add: nth_default_def)
   3.101 +
   3.102 +lemma sorted_list_of_set_nth_default:
   3.103 +  "sorted_list_of_set {k. nth_default dflt xs k \<noteq> dflt} = map fst (filter (\<lambda>(_, x). x \<noteq> dflt) (enumerate 0 xs))"
   3.104 +  by (rule sorted_distinct_set_unique) (auto simp add: nth_default_def in_set_conv_nth
   3.105 +    sorted_filter distinct_map_filter enumerate_eq_zip intro: rev_image_eqI)
   3.106 +
   3.107 +lemma map_nth_default:
   3.108 +  "map (nth_default x xs) [0..<length xs] = xs"
   3.109 +proof -
   3.110 +  have *: "map (nth_default x xs) [0..<length xs] = map (List.nth xs) [0..<length xs]"
   3.111 +    by (rule map_cong) (simp_all add: nth_default_nth)
   3.112 +  show ?thesis by (simp add: * map_nth)
   3.113 +qed
   3.114 +
   3.115  lemma range_nth_default [simp]:
   3.116    "range (nth_default dflt xs) = insert dflt (set xs)"
   3.117 -  by (auto simp add: nth_default_def[abs_def] in_set_conv_nth)
   3.118 +  by (auto simp add: nth_default_def [abs_def] in_set_conv_nth)
   3.119  
   3.120  lemma nth_strip_while:
   3.121    assumes "n < length (strip_while P xs)"
   3.122 @@ -241,25 +280,59 @@
   3.123    by (subst (2) length_rev[symmetric])
   3.124      (simp add: strip_while_def length_dropWhile_le del: length_rev)
   3.125  
   3.126 -lemma finite_nth_default_neq_default [simp]:
   3.127 -  "finite {k. nth_default dflt xs k \<noteq> dflt}"
   3.128 -  by (simp add: nth_default_def)
   3.129 -
   3.130 -lemma sorted_list_of_set_nth_default:
   3.131 -  "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))"
   3.132 -  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)
   3.133 -
   3.134 -lemma nth_default_snoc_default [simp]:
   3.135 -  "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
   3.136 -  by (auto simp add: nth_default_def fun_eq_iff nth_append)
   3.137 -
   3.138  lemma nth_default_strip_while_dflt [simp]:
   3.139 - "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs"
   3.140 +  "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs"
   3.141    by (induct xs rule: rev_induct) auto
   3.142  
   3.143 -lemma nth_default_eq_dflt_iff:
   3.144 -  "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
   3.145 -  by (simp add: nth_default_def)
   3.146 +lemma nth_default_eq_iff:
   3.147 +  "nth_default dflt xs = nth_default dflt ys
   3.148 +     \<longleftrightarrow> strip_while (HOL.eq dflt) xs = strip_while (HOL.eq dflt) ys" (is "?P \<longleftrightarrow> ?Q")
   3.149 +proof
   3.150 +  let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
   3.151 +  assume ?P
   3.152 +  then have eq: "nth_default dflt ?xs = nth_default dflt ?ys"
   3.153 +    by simp
   3.154 +  have len: "length ?xs = length ?ys"
   3.155 +  proof (rule ccontr)
   3.156 +    assume len: "length ?xs \<noteq> length ?ys"
   3.157 +    { fix xs ys :: "'a list"
   3.158 +      let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
   3.159 +      assume eq: "nth_default dflt ?xs = nth_default dflt ?ys"
   3.160 +      assume len: "length ?xs < length ?ys"
   3.161 +      then have "length ?ys > 0" by arith
   3.162 +      then have "?ys \<noteq> []" by simp
   3.163 +      with last_conv_nth_default [of ?ys dflt]
   3.164 +      have "last ?ys = nth_default dflt ?ys (length ?ys - 1)"
   3.165 +        by auto
   3.166 +      moreover from `?ys \<noteq> []` no_trailing_strip_while [of "HOL.eq dflt" ys]
   3.167 +        have "last ?ys \<noteq> dflt" by (simp add: no_trailing_unfold)
   3.168 +      ultimately have "nth_default dflt ?xs (length ?ys - 1) \<noteq> dflt"
   3.169 +        using eq by simp
   3.170 +      moreover from len have "length ?ys - 1 \<ge> length ?xs" by simp
   3.171 +      ultimately have False by (simp only: nth_default_beyond) simp
   3.172 +    } 
   3.173 +    from this [of xs ys] this [of ys xs] len eq show False
   3.174 +      by (auto simp only: linorder_class.neq_iff)
   3.175 +  qed
   3.176 +  then show ?Q
   3.177 +  proof (rule nth_equalityI [rule_format])
   3.178 +    fix n
   3.179 +    assume "n < length ?xs"
   3.180 +    moreover with len have "n < length ?ys"
   3.181 +      by simp
   3.182 +    ultimately have xs: "nth_default dflt ?xs n = ?xs ! n"
   3.183 +      and ys: "nth_default dflt ?ys n = ?ys ! n"
   3.184 +      by (simp_all only: nth_default_nth)
   3.185 +    with eq show "?xs ! n = ?ys ! n"
   3.186 +      by simp
   3.187 +  qed
   3.188 +next
   3.189 +  assume ?Q
   3.190 +  then have "nth_default dflt (strip_while (HOL.eq dflt) xs) = nth_default dflt (strip_while (HOL.eq dflt) ys)"
   3.191 +    by simp
   3.192 +  then show ?P
   3.193 +    by simp
   3.194 +qed
   3.195  
   3.196  end
   3.197  
     4.1 --- a/src/HOL/List.thy	Wed Sep 24 19:10:30 2014 +0200
     4.2 +++ b/src/HOL/List.thy	Wed Sep 24 19:11:21 2014 +0200
     4.3 @@ -2796,6 +2796,10 @@
     4.4    "fold g (map f xs) = fold (g o f) xs"
     4.5    by (induct xs) simp_all
     4.6  
     4.7 +lemma fold_filter:
     4.8 +  "fold f (filter P xs) = fold (\<lambda>x. if P x then f x else id) xs"
     4.9 +  by (induct xs) simp_all
    4.10 +
    4.11  lemma fold_rev:
    4.12    assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
    4.13    shows "fold f (rev xs) = fold f xs"
    4.14 @@ -2942,6 +2946,10 @@
    4.15    "foldr g (map f xs) a = foldr (g o f) xs a"
    4.16    by (simp add: foldr_conv_fold fold_map rev_map)
    4.17  
    4.18 +lemma foldr_filter:
    4.19 +  "foldr f (filter P xs) = foldr (\<lambda>x. if P x then f x else id) xs"
    4.20 +  by (simp add: foldr_conv_fold rev_filter fold_filter)
    4.21 +  
    4.22  lemma foldl_map [code_unfold]:
    4.23    "foldl g a (map f xs) = foldl (\<lambda>a x. g a (f x)) a xs"
    4.24    by (simp add: foldl_conv_fold fold_map comp_def)
    4.25 @@ -3030,6 +3038,7 @@
    4.26    "map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]"
    4.27    by (induct n) simp_all
    4.28  
    4.29 + 
    4.30  lemma nth_take_lemma:
    4.31    "k <= length xs ==> k <= length ys ==>
    4.32       (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
    4.33 @@ -3479,6 +3488,18 @@
    4.34    by (induct xs rule: remdups_adj.induct, 
    4.35        auto simp add: injD[OF assms])
    4.36  
    4.37 +lemma remdups_upt [simp]:
    4.38 +  "remdups [m..<n] = [m..<n]"
    4.39 +proof (cases "m \<le> n")
    4.40 +  case False then show ?thesis by simp
    4.41 +next
    4.42 +  case True then obtain q where "n = m + q"
    4.43 +    by (auto simp add: le_iff_add)
    4.44 +  moreover have "remdups [m..<m + q] = [m..<m + q]"
    4.45 +    by (induct q) simp_all
    4.46 +  ultimately show ?thesis by simp
    4.47 +qed
    4.48 +
    4.49  
    4.50  subsubsection {* @{const insert} *}
    4.51  
    4.52 @@ -3699,6 +3720,15 @@
    4.53  lemma length_replicate [simp]: "length (replicate n x) = n"
    4.54  by (induct n) auto
    4.55  
    4.56 +lemma replicate_eqI:
    4.57 +  assumes "length xs = n" and "\<And>y. y \<in> set xs \<Longrightarrow> y = x"
    4.58 +  shows "xs = replicate n x"
    4.59 +using assms proof (induct xs arbitrary: n)
    4.60 +  case Nil then show ?case by simp
    4.61 +next
    4.62 +  case (Cons x xs) then show ?case by (cases n) simp_all
    4.63 +qed
    4.64 +
    4.65  lemma Ex_list_of_length: "\<exists>xs. length xs = n"
    4.66  by (rule exI[of _ "replicate n undefined"]) simp
    4.67  
    4.68 @@ -3951,6 +3981,18 @@
    4.69    "distinct (enumerate n xs)"
    4.70    by (simp add: enumerate_eq_zip distinct_zipI1)
    4.71  
    4.72 +lemma enumerate_append_eq:
    4.73 +  "enumerate n (xs @ ys) = enumerate n xs @ enumerate (n + length xs) ys"
    4.74 +  unfolding enumerate_eq_zip apply auto
    4.75 +  apply (subst zip_append [symmetric]) apply simp
    4.76 +  apply (subst upt_add_eq_append [symmetric])
    4.77 +  apply (simp_all add: ac_simps)
    4.78 +  done
    4.79 +
    4.80 +lemma enumerate_map_upt:
    4.81 +  "enumerate n (map f [n..<m]) = map (\<lambda>k. (k, f k)) [n..<m]"
    4.82 +  by (cases "n \<le> m") (simp_all add: zip_map2 zip_same_conv_map enumerate_eq_zip)
    4.83 +  
    4.84  
    4.85  subsubsection {* @{const rotate1} and @{const rotate} *}
    4.86  
    4.87 @@ -4755,6 +4797,10 @@
    4.88  lemma sorted_upt[simp]: "sorted[i..<j]"
    4.89  by (induct j) (simp_all add:sorted_append)
    4.90  
    4.91 +lemma sort_upt [simp]:
    4.92 +  "sort [m..<n] = [m..<n]"
    4.93 +  by (rule sorted_sort_id) simp
    4.94 +
    4.95  lemma sorted_upto[simp]: "sorted[i..j]"
    4.96  apply(induct i j rule:upto.induct)
    4.97  apply(subst upto.simps)
    4.98 @@ -4777,6 +4823,10 @@
    4.99    qed
   4.100  qed
   4.101  
   4.102 +lemma sorted_enumerate [simp]:
   4.103 +  "sorted (map fst (enumerate n xs))"
   4.104 +  by (simp add: enumerate_eq_zip)
   4.105 +
   4.106  
   4.107  subsubsection {* @{const transpose} on sorted lists *}
   4.108  
     5.1 --- a/src/HOL/Power.thy	Wed Sep 24 19:10:30 2014 +0200
     5.2 +++ b/src/HOL/Power.thy	Wed Sep 24 19:11:21 2014 +0200
     5.3 @@ -795,6 +795,10 @@
     5.4      by simp
     5.5  qed
     5.6  
     5.7 +lemma power_setsum:
     5.8 +  "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
     5.9 +  by (induct A rule: infinite_finite_induct) (simp_all add: power_add)
    5.10 +
    5.11  lemma setprod_gen_delta:
    5.12    assumes fS: "finite S"
    5.13    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)"