src/HOL/Library/More_List.thy
author wenzelm
Wed Mar 08 10:50:59 2017 +0100 (2017-03-08)
changeset 65151 a7394aa4d21c
parent 63540 f8652d0534fa
child 65388 a8d868477bc0
permissions -rw-r--r--
tuned proofs;
     1 (* Author: Andreas Lochbihler, ETH Z├╝rich
     2    Author: Florian Haftmann, TU Muenchen  *)
     3 
     4 section \<open>Less common functions on lists\<close>
     5 
     6 theory More_List
     7 imports Main
     8 begin
     9 
    10 definition strip_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
    11 where
    12   "strip_while P = rev \<circ> dropWhile P \<circ> rev"
    13 
    14 lemma strip_while_rev [simp]:
    15   "strip_while P (rev xs) = rev (dropWhile P xs)"
    16   by (simp add: strip_while_def)
    17   
    18 lemma strip_while_Nil [simp]:
    19   "strip_while P [] = []"
    20   by (simp add: strip_while_def)
    21 
    22 lemma strip_while_append [simp]:
    23   "\<not> P x \<Longrightarrow> strip_while P (xs @ [x]) = xs @ [x]"
    24   by (simp add: strip_while_def)
    25 
    26 lemma strip_while_append_rec [simp]:
    27   "P x \<Longrightarrow> strip_while P (xs @ [x]) = strip_while P xs"
    28   by (simp add: strip_while_def)
    29 
    30 lemma strip_while_Cons [simp]:
    31   "\<not> P x \<Longrightarrow> strip_while P (x # xs) = x # strip_while P xs"
    32   by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
    33 
    34 lemma strip_while_eq_Nil [simp]:
    35   "strip_while P xs = [] \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
    36   by (simp add: strip_while_def)
    37 
    38 lemma strip_while_eq_Cons_rec:
    39   "strip_while P (x # xs) = x # strip_while P xs \<longleftrightarrow> \<not> (P x \<and> (\<forall>x\<in>set xs. P x))"
    40   by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
    41 
    42 lemma strip_while_not_last [simp]:
    43   "\<not> P (last xs) \<Longrightarrow> strip_while P xs = xs"
    44   by (cases xs rule: rev_cases) simp_all
    45 
    46 lemma split_strip_while_append:
    47   fixes xs :: "'a list"
    48   obtains ys zs :: "'a list"
    49   where "strip_while P xs = ys" and "\<forall>x\<in>set zs. P x" and "xs = ys @ zs"
    50 proof (rule that)
    51   show "strip_while P xs = strip_while P xs" ..
    52   show "\<forall>x\<in>set (rev (takeWhile P (rev xs))). P x" by (simp add: takeWhile_eq_all_conv [symmetric])
    53   have "rev xs = rev (strip_while P xs @ rev (takeWhile P (rev xs)))"
    54     by (simp add: strip_while_def)
    55   then show "xs = strip_while P xs @ rev (takeWhile P (rev xs))"
    56     by (simp only: rev_is_rev_conv)
    57 qed
    58 
    59 lemma strip_while_snoc [simp]:
    60   "strip_while P (xs @ [x]) = (if P x then strip_while P xs else xs @ [x])"
    61   by (simp add: strip_while_def)
    62 
    63 lemma strip_while_map:
    64   "strip_while P (map f xs) = map f (strip_while (P \<circ> f) xs)"
    65   by (simp add: strip_while_def rev_map dropWhile_map)
    66 
    67 
    68 definition no_leading :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
    69 where
    70   "no_leading P xs \<longleftrightarrow> (xs \<noteq> [] \<longrightarrow> \<not> P (hd xs))"
    71 
    72 lemma no_leading_Nil [simp, intro!]:
    73   "no_leading P []"
    74   by (simp add: no_leading_def)
    75 
    76 lemma no_leading_Cons [simp, intro!]:
    77   "no_leading P (x # xs) \<longleftrightarrow> \<not> P x"
    78   by (simp add: no_leading_def)
    79 
    80 lemma no_leading_append [simp]:
    81   "no_leading P (xs @ ys) \<longleftrightarrow> no_leading P xs \<and> (xs = [] \<longrightarrow> no_leading P ys)"
    82   by (induct xs) simp_all
    83 
    84 lemma no_leading_dropWhile [simp]:
    85   "no_leading P (dropWhile P xs)"
    86   by (induct xs) simp_all
    87 
    88 lemma dropWhile_eq_obtain_leading:
    89   assumes "dropWhile P xs = ys"
    90   obtains zs where "xs = zs @ ys" and "\<And>z. z \<in> set zs \<Longrightarrow> P z" and "no_leading P ys"
    91 proof -
    92   from assms have "\<exists>zs. xs = zs @ ys \<and> (\<forall>z \<in> set zs. P z) \<and> no_leading P ys"
    93   proof (induct xs arbitrary: ys)
    94     case Nil then show ?case by simp
    95   next
    96     case (Cons x xs ys)
    97     show ?case proof (cases "P x")
    98       case True with Cons.hyps [of ys] Cons.prems
    99       have "\<exists>zs. xs = zs @ ys \<and> (\<forall>a\<in>set zs. P a) \<and> no_leading P ys"
   100         by simp
   101       then obtain zs where "xs = zs @ ys" and "\<And>z. z \<in> set zs \<Longrightarrow> P z"
   102         and *: "no_leading P ys"
   103         by blast
   104       with True have "x # xs = (x # zs) @ ys" and "\<And>z. z \<in> set (x # zs) \<Longrightarrow> P z"
   105         by auto
   106       with * show ?thesis
   107         by blast    next
   108       case False
   109       with Cons show ?thesis by (cases ys) simp_all
   110     qed
   111   qed
   112   with that show thesis
   113     by blast
   114 qed
   115 
   116 lemma dropWhile_idem_iff:
   117   "dropWhile P xs = xs \<longleftrightarrow> no_leading P xs"
   118   by (cases xs) (auto elim: dropWhile_eq_obtain_leading)
   119 
   120 
   121 abbreviation no_trailing :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
   122 where
   123   "no_trailing P xs \<equiv> no_leading P (rev xs)"
   124 
   125 lemma no_trailing_unfold:
   126   "no_trailing P xs \<longleftrightarrow> (xs \<noteq> [] \<longrightarrow> \<not> P (last xs))"
   127   by (induct xs) simp_all
   128 
   129 lemma no_trailing_Nil [simp, intro!]:
   130   "no_trailing P []"
   131   by simp
   132 
   133 lemma no_trailing_Cons [simp]:
   134   "no_trailing P (x # xs) \<longleftrightarrow> no_trailing P xs \<and> (xs = [] \<longrightarrow> \<not> P x)"
   135   by simp
   136 
   137 lemma no_trailing_append_Cons [simp]:
   138   "no_trailing P (xs @ y # ys) \<longleftrightarrow> no_trailing P (y # ys)"
   139   by simp
   140 
   141 lemma no_trailing_strip_while [simp]:
   142   "no_trailing P (strip_while P xs)"
   143   by (induct xs rule: rev_induct) simp_all
   144 
   145 lemma strip_while_eq_obtain_trailing:
   146   assumes "strip_while P xs = ys"
   147   obtains zs where "xs = ys @ zs" and "\<And>z. z \<in> set zs \<Longrightarrow> P z" and "no_trailing P ys"
   148 proof -
   149   from assms have "rev (rev (dropWhile P (rev xs))) = rev ys"
   150     by (simp add: strip_while_def)
   151   then have "dropWhile P (rev xs) = rev ys"
   152     by simp
   153   then obtain zs where A: "rev xs = zs @ rev ys" and B: "\<And>z. z \<in> set zs \<Longrightarrow> P z"
   154     and C: "no_trailing P ys"
   155     using dropWhile_eq_obtain_leading by blast
   156   from A have "rev (rev xs) = rev (zs @ rev ys)"
   157     by simp
   158   then have "xs = ys @ rev zs"
   159     by simp
   160   moreover from B have "\<And>z. z \<in> set (rev zs) \<Longrightarrow> P z"
   161     by simp
   162   ultimately show thesis using that C by blast
   163 qed
   164 
   165 lemma strip_while_idem_iff:
   166   "strip_while P xs = xs \<longleftrightarrow> no_trailing P xs"
   167 proof -
   168   define ys where "ys = rev xs"
   169   moreover have "strip_while P (rev ys) = rev ys \<longleftrightarrow> no_trailing P (rev ys)"
   170     by (simp add: dropWhile_idem_iff)
   171   ultimately show ?thesis by simp
   172 qed
   173 
   174 lemma no_trailing_map:
   175   "no_trailing P (map f xs) = no_trailing (P \<circ> f) xs"
   176   by (simp add: last_map no_trailing_unfold)
   177 
   178 lemma no_trailing_upt [simp]:
   179   "no_trailing P [n..<m] \<longleftrightarrow> (n < m \<longrightarrow> \<not> P (m - 1))"
   180   by (auto simp add: no_trailing_unfold)
   181 
   182 
   183 definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a"
   184 where
   185   "nth_default dflt xs n = (if n < length xs then xs ! n else dflt)"
   186 
   187 lemma nth_default_nth:
   188   "n < length xs \<Longrightarrow> nth_default dflt xs n = xs ! n"
   189   by (simp add: nth_default_def)
   190 
   191 lemma nth_default_beyond:
   192   "length xs \<le> n \<Longrightarrow> nth_default dflt xs n = dflt"
   193   by (simp add: nth_default_def)
   194 
   195 lemma nth_default_Nil [simp]:
   196   "nth_default dflt [] n = dflt"
   197   by (simp add: nth_default_def)
   198 
   199 lemma nth_default_Cons:
   200   "nth_default dflt (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default dflt xs n')"
   201   by (simp add: nth_default_def split: nat.split)
   202 
   203 lemma nth_default_Cons_0 [simp]:
   204   "nth_default dflt (x # xs) 0 = x"
   205   by (simp add: nth_default_Cons)
   206 
   207 lemma nth_default_Cons_Suc [simp]:
   208   "nth_default dflt (x # xs) (Suc n) = nth_default dflt xs n"
   209   by (simp add: nth_default_Cons)
   210 
   211 lemma nth_default_replicate_dflt [simp]:
   212   "nth_default dflt (replicate n dflt) m = dflt"
   213   by (simp add: nth_default_def)
   214 
   215 lemma nth_default_append:
   216   "nth_default dflt (xs @ ys) n =
   217     (if n < length xs then nth xs n else nth_default dflt ys (n - length xs))"
   218   by (auto simp add: nth_default_def nth_append)
   219 
   220 lemma nth_default_append_trailing [simp]:
   221   "nth_default dflt (xs @ replicate n dflt) = nth_default dflt xs"
   222   by (simp add: fun_eq_iff nth_default_append) (simp add: nth_default_def)
   223 
   224 lemma nth_default_snoc_default [simp]:
   225   "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
   226   by (auto simp add: nth_default_def fun_eq_iff nth_append)
   227 
   228 lemma nth_default_eq_dflt_iff:
   229   "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
   230   by (simp add: nth_default_def)
   231 
   232 lemma in_enumerate_iff_nth_default_eq:
   233   "x \<noteq> dflt \<Longrightarrow> (n, x) \<in> set (enumerate 0 xs) \<longleftrightarrow> nth_default dflt xs n = x"
   234   by (auto simp add: nth_default_def in_set_conv_nth enumerate_eq_zip)
   235 
   236 lemma last_conv_nth_default:
   237   assumes "xs \<noteq> []"
   238   shows "last xs = nth_default dflt xs (length xs - 1)"
   239   using assms by (simp add: nth_default_def last_conv_nth)
   240   
   241 lemma nth_default_map_eq:
   242   "f dflt' = dflt \<Longrightarrow> nth_default dflt (map f xs) n = f (nth_default dflt' xs n)"
   243   by (simp add: nth_default_def)
   244 
   245 lemma finite_nth_default_neq_default [simp]:
   246   "finite {k. nth_default dflt xs k \<noteq> dflt}"
   247   by (simp add: nth_default_def)
   248 
   249 lemma sorted_list_of_set_nth_default:
   250   "sorted_list_of_set {k. nth_default dflt xs k \<noteq> dflt} = map fst (filter (\<lambda>(_, x). x \<noteq> dflt) (enumerate 0 xs))"
   251   by (rule sorted_distinct_set_unique) (auto simp add: nth_default_def in_set_conv_nth
   252     sorted_filter distinct_map_filter enumerate_eq_zip intro: rev_image_eqI)
   253 
   254 lemma map_nth_default:
   255   "map (nth_default x xs) [0..<length xs] = xs"
   256 proof -
   257   have *: "map (nth_default x xs) [0..<length xs] = map (List.nth xs) [0..<length xs]"
   258     by (rule map_cong) (simp_all add: nth_default_nth)
   259   show ?thesis by (simp add: * map_nth)
   260 qed
   261 
   262 lemma range_nth_default [simp]:
   263   "range (nth_default dflt xs) = insert dflt (set xs)"
   264   by (auto simp add: nth_default_def [abs_def] in_set_conv_nth)
   265 
   266 lemma nth_strip_while:
   267   assumes "n < length (strip_while P xs)"
   268   shows "strip_while P xs ! n = xs ! n"
   269 proof -
   270   have "length (dropWhile P (rev xs)) + length (takeWhile P (rev xs)) = length xs"
   271     by (subst add.commute)
   272       (simp add: arg_cong [where f=length, OF takeWhile_dropWhile_id, unfolded length_append])
   273   then show ?thesis using assms
   274     by (simp add: strip_while_def rev_nth dropWhile_nth)
   275 qed
   276 
   277 lemma length_strip_while_le:
   278   "length (strip_while P xs) \<le> length xs"
   279   unfolding strip_while_def o_def length_rev
   280   by (subst (2) length_rev[symmetric])
   281     (simp add: strip_while_def length_dropWhile_le del: length_rev)
   282 
   283 lemma nth_default_strip_while_dflt [simp]:
   284   "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs"
   285   by (induct xs rule: rev_induct) auto
   286 
   287 lemma nth_default_eq_iff:
   288   "nth_default dflt xs = nth_default dflt ys
   289      \<longleftrightarrow> strip_while (HOL.eq dflt) xs = strip_while (HOL.eq dflt) ys" (is "?P \<longleftrightarrow> ?Q")
   290 proof
   291   let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
   292   assume ?P
   293   then have eq: "nth_default dflt ?xs = nth_default dflt ?ys"
   294     by simp
   295   have len: "length ?xs = length ?ys"
   296   proof (rule ccontr)
   297     assume len: "length ?xs \<noteq> length ?ys"
   298     { fix xs ys :: "'a list"
   299       let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
   300       assume eq: "nth_default dflt ?xs = nth_default dflt ?ys"
   301       assume len: "length ?xs < length ?ys"
   302       then have "length ?ys > 0" by arith
   303       then have "?ys \<noteq> []" by simp
   304       with last_conv_nth_default [of ?ys dflt]
   305       have "last ?ys = nth_default dflt ?ys (length ?ys - 1)"
   306         by auto
   307       moreover from \<open>?ys \<noteq> []\<close> no_trailing_strip_while [of "HOL.eq dflt" ys]
   308         have "last ?ys \<noteq> dflt" by (simp add: no_trailing_unfold)
   309       ultimately have "nth_default dflt ?xs (length ?ys - 1) \<noteq> dflt"
   310         using eq by simp
   311       moreover from len have "length ?ys - 1 \<ge> length ?xs" by simp
   312       ultimately have False by (simp only: nth_default_beyond) simp
   313     } 
   314     from this [of xs ys] this [of ys xs] len eq show False
   315       by (auto simp only: linorder_class.neq_iff)
   316   qed
   317   then show ?Q
   318   proof (rule nth_equalityI [rule_format])
   319     fix n
   320     assume n: "n < length ?xs"
   321     with len have "n < length ?ys"
   322       by simp
   323     with n have xs: "nth_default dflt ?xs n = ?xs ! n"
   324       and ys: "nth_default dflt ?ys n = ?ys ! n"
   325       by (simp_all only: nth_default_nth)
   326     with eq show "?xs ! n = ?ys ! n"
   327       by simp
   328   qed
   329 next
   330   assume ?Q
   331   then have "nth_default dflt (strip_while (HOL.eq dflt) xs) = nth_default dflt (strip_while (HOL.eq dflt) ys)"
   332     by simp
   333   then show ?P
   334     by simp
   335 qed
   336 
   337 end
   338