src/HOL/Library/More_List.thy
changeset 58437 8d124c73c37a
parent 58295 c8a8e7c37986
child 58881 b9556a055632
     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