src/HOL/Library/More_List.thy
changeset 58199 5fbe474b5da8
child 58295 c8a8e7c37986
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/More_List.thy	Sun Sep 07 09:49:05 2014 +0200
     1.3 @@ -0,0 +1,155 @@
     1.4 +(* Author: Andreas Lochbihler, ETH Z├╝rich
     1.5 +   Author: Florian Haftmann, TU Muenchen  *)
     1.6 +
     1.7 +header \<open>Less common functions on lists\<close>
     1.8 +
     1.9 +theory More_List
    1.10 +imports Main
    1.11 +begin
    1.12 +
    1.13 +text \<open>FIXME adapted from @{file "~~/src/HOL/Library/Polynomial.thy"}; to be merged back\<close>
    1.14 +
    1.15 +definition strip_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.16 +where
    1.17 +  "strip_while P = rev \<circ> dropWhile P \<circ> rev"
    1.18 +
    1.19 +lemma strip_while_Nil [simp]:
    1.20 +  "strip_while P [] = []"
    1.21 +  by (simp add: strip_while_def)
    1.22 +
    1.23 +lemma strip_while_append [simp]:
    1.24 +  "\<not> P x \<Longrightarrow> strip_while P (xs @ [x]) = xs @ [x]"
    1.25 +  by (simp add: strip_while_def)
    1.26 +
    1.27 +lemma strip_while_append_rec [simp]:
    1.28 +  "P x \<Longrightarrow> strip_while P (xs @ [x]) = strip_while P xs"
    1.29 +  by (simp add: strip_while_def)
    1.30 +
    1.31 +lemma strip_while_Cons [simp]:
    1.32 +  "\<not> P x \<Longrightarrow> strip_while P (x # xs) = x # strip_while P xs"
    1.33 +  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
    1.34 +
    1.35 +lemma strip_while_eq_Nil [simp]:
    1.36 +  "strip_while P xs = [] \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
    1.37 +  by (simp add: strip_while_def)
    1.38 +
    1.39 +lemma strip_while_eq_Cons_rec:
    1.40 +  "strip_while P (x # xs) = x # strip_while P xs \<longleftrightarrow> \<not> (P x \<and> (\<forall>x\<in>set xs. P x))"
    1.41 +  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
    1.42 +
    1.43 +lemma strip_while_not_last [simp]:
    1.44 +  "\<not> P (last xs) \<Longrightarrow> strip_while P xs = xs"
    1.45 +  by (cases xs rule: rev_cases) simp_all
    1.46 +
    1.47 +lemma split_strip_while_append:
    1.48 +  fixes xs :: "'a list"
    1.49 +  obtains ys zs :: "'a list"
    1.50 +  where "strip_while P xs = ys" and "\<forall>x\<in>set zs. P x" and "xs = ys @ zs"
    1.51 +proof (rule that)
    1.52 +  show "strip_while P xs = strip_while P xs" ..
    1.53 +  show "\<forall>x\<in>set (rev (takeWhile P (rev xs))). P x" by (simp add: takeWhile_eq_all_conv [symmetric])
    1.54 +  have "rev xs = rev (strip_while P xs @ rev (takeWhile P (rev xs)))"
    1.55 +    by (simp add: strip_while_def)
    1.56 +  then show "xs = strip_while P xs @ rev (takeWhile P (rev xs))"
    1.57 +    by (simp only: rev_is_rev_conv)
    1.58 +qed
    1.59 +
    1.60 +lemma strip_while_snoc [simp]:
    1.61 +  "strip_while P (xs @ [x]) = (if P x then strip_while P xs else xs @ [x])"
    1.62 +  by (simp add: strip_while_def)
    1.63 +
    1.64 +lemma strip_while_map:
    1.65 +  "strip_while P (map f xs) = map f (strip_while (P \<circ> f) xs)"
    1.66 +  by (simp add: strip_while_def rev_map dropWhile_map)
    1.67 +
    1.68 +lemma dropWhile_idI:
    1.69 +  "(xs \<noteq> [] \<Longrightarrow> \<not> P (hd xs)) \<Longrightarrow> dropWhile P xs = xs"
    1.70 +  by (metis dropWhile.simps(1) dropWhile.simps(2) list.collapse)
    1.71 +
    1.72 +lemma strip_while_idI:
    1.73 +  "(xs \<noteq> [] \<Longrightarrow> \<not> P (last xs)) \<Longrightarrow> strip_while P xs = xs"
    1.74 +  using dropWhile_idI [of "rev xs"] by (simp add: strip_while_def hd_rev)
    1.75 +
    1.76 +
    1.77 +definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a"
    1.78 +where
    1.79 +  "nth_default x xs n = (if n < length xs then xs ! n else x)"
    1.80 +
    1.81 +lemma nth_default_Nil [simp]:
    1.82 +  "nth_default y [] n = y"
    1.83 +  by (simp add: nth_default_def)
    1.84 +
    1.85 +lemma nth_default_Cons_0 [simp]:
    1.86 +  "nth_default y (x # xs) 0 = x"
    1.87 +  by (simp add: nth_default_def)
    1.88 +
    1.89 +lemma nth_default_Cons_Suc [simp]:
    1.90 +  "nth_default y (x # xs) (Suc n) = nth_default y xs n"
    1.91 +  by (simp add: nth_default_def)
    1.92 +
    1.93 +lemma nth_default_map_eq:
    1.94 +  "f y = x \<Longrightarrow> nth_default x (map f xs) n = f (nth_default y xs n)"
    1.95 +  by (simp add: nth_default_def)
    1.96 +
    1.97 +lemma nth_default_strip_while_eq [simp]:
    1.98 +  "nth_default x (strip_while (HOL.eq x) xs) n = nth_default x xs n"
    1.99 +proof -
   1.100 +  from split_strip_while_append obtain ys zs
   1.101 +    where "strip_while (HOL.eq x) xs = ys" and "\<forall>z\<in>set zs. x = z" and "xs = ys @ zs" by blast
   1.102 +  then show ?thesis by (simp add: nth_default_def not_less nth_append)
   1.103 +qed
   1.104 +
   1.105 +lemma nth_default_Cons:
   1.106 +  "nth_default y (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default y xs n')"
   1.107 +  by (simp split: nat.split)
   1.108 +
   1.109 +lemma nth_default_nth:
   1.110 +  "n < length xs \<Longrightarrow> nth_default y xs n = xs ! n"
   1.111 +  by (simp add: nth_default_def)
   1.112 +
   1.113 +lemma nth_default_beyond:
   1.114 +  "length xs \<le> n \<Longrightarrow> nth_default y xs n = y"
   1.115 +  by (simp add: nth_default_def)
   1.116 +
   1.117 +lemma range_nth_default [simp]:
   1.118 +  "range (nth_default dflt xs) = insert dflt (set xs)"
   1.119 +  by (auto simp add: nth_default_def[abs_def] in_set_conv_nth)
   1.120 +
   1.121 +lemma nth_strip_while:
   1.122 +  assumes "n < length (strip_while P xs)"
   1.123 +  shows "strip_while P xs ! n = xs ! n"
   1.124 +proof -
   1.125 +  have "length (dropWhile P (rev xs)) + length (takeWhile P (rev xs)) = length xs"
   1.126 +    by (subst add.commute)
   1.127 +      (simp add: arg_cong [where f=length, OF takeWhile_dropWhile_id, unfolded length_append])
   1.128 +  then show ?thesis using assms
   1.129 +    by (simp add: strip_while_def rev_nth dropWhile_nth)
   1.130 +qed
   1.131 +
   1.132 +lemma length_strip_while_le:
   1.133 +  "length (strip_while P xs) \<le> length xs"
   1.134 +  unfolding strip_while_def o_def length_rev
   1.135 +  by (subst (2) length_rev[symmetric])
   1.136 +    (simp add: strip_while_def length_dropWhile_le del: length_rev)
   1.137 +
   1.138 +lemma finite_nth_default_neq_default [simp]:
   1.139 +  "finite {k. nth_default dflt xs k \<noteq> dflt}"
   1.140 +  by (simp add: nth_default_def)
   1.141 +
   1.142 +lemma sorted_list_of_set_nth_default:
   1.143 +  "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.144 +  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.145 +
   1.146 +lemma nth_default_snoc_default [simp]:
   1.147 +  "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
   1.148 +  by (auto simp add: nth_default_def fun_eq_iff nth_append)
   1.149 +
   1.150 +lemma nth_default_strip_while_dflt [simp]:
   1.151 + "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs"
   1.152 +  by (induct xs rule: rev_induct) auto
   1.153 +
   1.154 +lemma nth_default_eq_dflt_iff:
   1.155 +  "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
   1.156 +  by (simp add: nth_default_def)
   1.157 +
   1.158 +end