1.1 --- a/src/HOL/Library/More_List.thy Wed Sep 24 19:10:30 2014 +0200
1.2 +++ b/src/HOL/Library/More_List.thy Wed Sep 24 19:11:21 2014 +0200
1.3 @@ -182,47 +182,86 @@
1.4
1.5 definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a"
1.6 where
1.7 - "nth_default x xs n = (if n < length xs then xs ! n else x)"
1.8 -
1.9 -lemma nth_default_Nil [simp]:
1.10 - "nth_default y [] n = y"
1.11 - by (simp add: nth_default_def)
1.12 -
1.13 -lemma nth_default_Cons_0 [simp]:
1.14 - "nth_default y (x # xs) 0 = x"
1.15 - by (simp add: nth_default_def)
1.16 -
1.17 -lemma nth_default_Cons_Suc [simp]:
1.18 - "nth_default y (x # xs) (Suc n) = nth_default y xs n"
1.19 - by (simp add: nth_default_def)
1.20 -
1.21 -lemma nth_default_map_eq:
1.22 - "f y = x \<Longrightarrow> nth_default x (map f xs) n = f (nth_default y xs n)"
1.23 - by (simp add: nth_default_def)
1.24 -
1.25 -lemma nth_default_strip_while_eq [simp]:
1.26 - "nth_default x (strip_while (HOL.eq x) xs) n = nth_default x xs n"
1.27 -proof -
1.28 - from split_strip_while_append obtain ys zs
1.29 - where "strip_while (HOL.eq x) xs = ys" and "\<forall>z\<in>set zs. x = z" and "xs = ys @ zs" by blast
1.30 - then show ?thesis by (simp add: nth_default_def not_less nth_append)
1.31 -qed
1.32 -
1.33 -lemma nth_default_Cons:
1.34 - "nth_default y (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default y xs n')"
1.35 - by (simp split: nat.split)
1.36 + "nth_default dflt xs n = (if n < length xs then xs ! n else dflt)"
1.37
1.38 lemma nth_default_nth:
1.39 - "n < length xs \<Longrightarrow> nth_default y xs n = xs ! n"
1.40 + "n < length xs \<Longrightarrow> nth_default dflt xs n = xs ! n"
1.41 by (simp add: nth_default_def)
1.42
1.43 lemma nth_default_beyond:
1.44 - "length xs \<le> n \<Longrightarrow> nth_default y xs n = y"
1.45 + "length xs \<le> n \<Longrightarrow> nth_default dflt xs n = dflt"
1.46 + by (simp add: nth_default_def)
1.47 +
1.48 +lemma nth_default_Nil [simp]:
1.49 + "nth_default dflt [] n = dflt"
1.50 + by (simp add: nth_default_def)
1.51 +
1.52 +lemma nth_default_Cons:
1.53 + "nth_default dflt (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default dflt xs n')"
1.54 + by (simp add: nth_default_def split: nat.split)
1.55 +
1.56 +lemma nth_default_Cons_0 [simp]:
1.57 + "nth_default dflt (x # xs) 0 = x"
1.58 + by (simp add: nth_default_Cons)
1.59 +
1.60 +lemma nth_default_Cons_Suc [simp]:
1.61 + "nth_default dflt (x # xs) (Suc n) = nth_default dflt xs n"
1.62 + by (simp add: nth_default_Cons)
1.63 +
1.64 +lemma nth_default_replicate_dflt [simp]:
1.65 + "nth_default dflt (replicate n dflt) m = dflt"
1.66 by (simp add: nth_default_def)
1.67
1.68 +lemma nth_default_append:
1.69 + "nth_default dflt (xs @ ys) n =
1.70 + (if n < length xs then nth xs n else nth_default dflt ys (n - length xs))"
1.71 + by (auto simp add: nth_default_def nth_append)
1.72 +
1.73 +lemma nth_default_append_trailing [simp]:
1.74 + "nth_default dflt (xs @ replicate n dflt) = nth_default dflt xs"
1.75 + by (simp add: fun_eq_iff nth_default_append) (simp add: nth_default_def)
1.76 +
1.77 +lemma nth_default_snoc_default [simp]:
1.78 + "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
1.79 + by (auto simp add: nth_default_def fun_eq_iff nth_append)
1.80 +
1.81 +lemma nth_default_eq_dflt_iff:
1.82 + "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
1.83 + by (simp add: nth_default_def)
1.84 +
1.85 +lemma in_enumerate_iff_nth_default_eq:
1.86 + "x \<noteq> dflt \<Longrightarrow> (n, x) \<in> set (enumerate 0 xs) \<longleftrightarrow> nth_default dflt xs n = x"
1.87 + by (auto simp add: nth_default_def in_set_conv_nth enumerate_eq_zip)
1.88 +
1.89 +lemma last_conv_nth_default:
1.90 + assumes "xs \<noteq> []"
1.91 + shows "last xs = nth_default dflt xs (length xs - 1)"
1.92 + using assms by (simp add: nth_default_def last_conv_nth)
1.93 +
1.94 +lemma nth_default_map_eq:
1.95 + "f dflt' = dflt \<Longrightarrow> nth_default dflt (map f xs) n = f (nth_default dflt' xs n)"
1.96 + by (simp add: nth_default_def)
1.97 +
1.98 +lemma finite_nth_default_neq_default [simp]:
1.99 + "finite {k. nth_default dflt xs k \<noteq> dflt}"
1.100 + by (simp add: nth_default_def)
1.101 +
1.102 +lemma sorted_list_of_set_nth_default:
1.103 + "sorted_list_of_set {k. nth_default dflt xs k \<noteq> dflt} = map fst (filter (\<lambda>(_, x). x \<noteq> dflt) (enumerate 0 xs))"
1.104 + by (rule sorted_distinct_set_unique) (auto simp add: nth_default_def in_set_conv_nth
1.105 + sorted_filter distinct_map_filter enumerate_eq_zip intro: rev_image_eqI)
1.106 +
1.107 +lemma map_nth_default:
1.108 + "map (nth_default x xs) [0..<length xs] = xs"
1.109 +proof -
1.110 + have *: "map (nth_default x xs) [0..<length xs] = map (List.nth xs) [0..<length xs]"
1.111 + by (rule map_cong) (simp_all add: nth_default_nth)
1.112 + show ?thesis by (simp add: * map_nth)
1.113 +qed
1.114 +
1.115 lemma range_nth_default [simp]:
1.116 "range (nth_default dflt xs) = insert dflt (set xs)"
1.117 - by (auto simp add: nth_default_def[abs_def] in_set_conv_nth)
1.118 + by (auto simp add: nth_default_def [abs_def] in_set_conv_nth)
1.119
1.120 lemma nth_strip_while:
1.121 assumes "n < length (strip_while P xs)"
1.122 @@ -241,25 +280,59 @@
1.123 by (subst (2) length_rev[symmetric])
1.124 (simp add: strip_while_def length_dropWhile_le del: length_rev)
1.125
1.126 -lemma finite_nth_default_neq_default [simp]:
1.127 - "finite {k. nth_default dflt xs k \<noteq> dflt}"
1.128 - by (simp add: nth_default_def)
1.129 -
1.130 -lemma sorted_list_of_set_nth_default:
1.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))"
1.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)
1.133 -
1.134 -lemma nth_default_snoc_default [simp]:
1.135 - "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
1.136 - by (auto simp add: nth_default_def fun_eq_iff nth_append)
1.137 -
1.138 lemma nth_default_strip_while_dflt [simp]:
1.139 - "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs"
1.140 + "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs"
1.141 by (induct xs rule: rev_induct) auto
1.142
1.143 -lemma nth_default_eq_dflt_iff:
1.144 - "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
1.145 - by (simp add: nth_default_def)
1.146 +lemma nth_default_eq_iff:
1.147 + "nth_default dflt xs = nth_default dflt ys
1.148 + \<longleftrightarrow> strip_while (HOL.eq dflt) xs = strip_while (HOL.eq dflt) ys" (is "?P \<longleftrightarrow> ?Q")
1.149 +proof
1.150 + let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
1.151 + assume ?P
1.152 + then have eq: "nth_default dflt ?xs = nth_default dflt ?ys"
1.153 + by simp
1.154 + have len: "length ?xs = length ?ys"
1.155 + proof (rule ccontr)
1.156 + assume len: "length ?xs \<noteq> length ?ys"
1.157 + { fix xs ys :: "'a list"
1.158 + let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
1.159 + assume eq: "nth_default dflt ?xs = nth_default dflt ?ys"
1.160 + assume len: "length ?xs < length ?ys"
1.161 + then have "length ?ys > 0" by arith
1.162 + then have "?ys \<noteq> []" by simp
1.163 + with last_conv_nth_default [of ?ys dflt]
1.164 + have "last ?ys = nth_default dflt ?ys (length ?ys - 1)"
1.165 + by auto
1.166 + moreover from `?ys \<noteq> []` no_trailing_strip_while [of "HOL.eq dflt" ys]
1.167 + have "last ?ys \<noteq> dflt" by (simp add: no_trailing_unfold)
1.168 + ultimately have "nth_default dflt ?xs (length ?ys - 1) \<noteq> dflt"
1.169 + using eq by simp
1.170 + moreover from len have "length ?ys - 1 \<ge> length ?xs" by simp
1.171 + ultimately have False by (simp only: nth_default_beyond) simp
1.172 + }
1.173 + from this [of xs ys] this [of ys xs] len eq show False
1.174 + by (auto simp only: linorder_class.neq_iff)
1.175 + qed
1.176 + then show ?Q
1.177 + proof (rule nth_equalityI [rule_format])
1.178 + fix n
1.179 + assume "n < length ?xs"
1.180 + moreover with len have "n < length ?ys"
1.181 + by simp
1.182 + ultimately have xs: "nth_default dflt ?xs n = ?xs ! n"
1.183 + and ys: "nth_default dflt ?ys n = ?ys ! n"
1.184 + by (simp_all only: nth_default_nth)
1.185 + with eq show "?xs ! n = ?ys ! n"
1.186 + by simp
1.187 + qed
1.188 +next
1.189 + assume ?Q
1.190 + then have "nth_default dflt (strip_while (HOL.eq dflt) xs) = nth_default dflt (strip_while (HOL.eq dflt) ys)"
1.191 + by simp
1.192 + then show ?P
1.193 + by simp
1.194 +qed
1.195
1.196 end
1.197