src/HOL/Library/More_List.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (4 months ago) changeset 69946 494934c30f38 parent 67730 f91c437f6f68 permissions -rw-r--r--
improved code equations taken over from AFP
```     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 split_strip_while_append:
```
```    43   fixes xs :: "'a list"
```
```    44   obtains ys zs :: "'a list"
```
```    45   where "strip_while P xs = ys" and "\<forall>x\<in>set zs. P x" and "xs = ys @ zs"
```
```    46 proof (rule that)
```
```    47   show "strip_while P xs = strip_while P xs" ..
```
```    48   show "\<forall>x\<in>set (rev (takeWhile P (rev xs))). P x" by (simp add: takeWhile_eq_all_conv [symmetric])
```
```    49   have "rev xs = rev (strip_while P xs @ rev (takeWhile P (rev xs)))"
```
```    50     by (simp add: strip_while_def)
```
```    51   then show "xs = strip_while P xs @ rev (takeWhile P (rev xs))"
```
```    52     by (simp only: rev_is_rev_conv)
```
```    53 qed
```
```    54
```
```    55 lemma strip_while_snoc [simp]:
```
```    56   "strip_while P (xs @ [x]) = (if P x then strip_while P xs else xs @ [x])"
```
```    57   by (simp add: strip_while_def)
```
```    58
```
```    59 lemma strip_while_map:
```
```    60   "strip_while P (map f xs) = map f (strip_while (P \<circ> f) xs)"
```
```    61   by (simp add: strip_while_def rev_map dropWhile_map)
```
```    62
```
```    63 lemma strip_while_dropWhile_commute:
```
```    64   "strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)"
```
```    65 proof (induct xs)
```
```    66   case Nil
```
```    67   then show ?case
```
```    68     by simp
```
```    69 next
```
```    70   case (Cons x xs)
```
```    71   show ?case
```
```    72   proof (cases "\<forall>y\<in>set xs. P y")
```
```    73     case True
```
```    74     with dropWhile_append2 [of "rev xs"] show ?thesis
```
```    75       by (auto simp add: strip_while_def dest: set_dropWhileD)
```
```    76   next
```
```    77     case False
```
```    78     then obtain y where "y \<in> set xs" and "\<not> P y"
```
```    79       by blast
```
```    80     with Cons dropWhile_append3 [of P y "rev xs"] show ?thesis
```
```    81       by (simp add: strip_while_def)
```
```    82   qed
```
```    83 qed
```
```    84
```
```    85 lemma dropWhile_strip_while_commute:
```
```    86   "dropWhile P (strip_while Q xs) = strip_while Q (dropWhile P xs)"
```
```    87   by (simp add: strip_while_dropWhile_commute)
```
```    88
```
```    89
```
```    90 definition no_leading :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
```
```    91 where
```
```    92   "no_leading P xs \<longleftrightarrow> (xs \<noteq> [] \<longrightarrow> \<not> P (hd xs))"
```
```    93
```
```    94 lemma no_leading_Nil [simp, intro!]:
```
```    95   "no_leading P []"
```
```    96   by (simp add: no_leading_def)
```
```    97
```
```    98 lemma no_leading_Cons [simp, intro!]:
```
```    99   "no_leading P (x # xs) \<longleftrightarrow> \<not> P x"
```
```   100   by (simp add: no_leading_def)
```
```   101
```
```   102 lemma no_leading_append [simp]:
```
```   103   "no_leading P (xs @ ys) \<longleftrightarrow> no_leading P xs \<and> (xs = [] \<longrightarrow> no_leading P ys)"
```
```   104   by (induct xs) simp_all
```
```   105
```
```   106 lemma no_leading_dropWhile [simp]:
```
```   107   "no_leading P (dropWhile P xs)"
```
```   108   by (induct xs) simp_all
```
```   109
```
```   110 lemma dropWhile_eq_obtain_leading:
```
```   111   assumes "dropWhile P xs = ys"
```
```   112   obtains zs where "xs = zs @ ys" and "\<And>z. z \<in> set zs \<Longrightarrow> P z" and "no_leading P ys"
```
```   113 proof -
```
```   114   from assms have "\<exists>zs. xs = zs @ ys \<and> (\<forall>z \<in> set zs. P z) \<and> no_leading P ys"
```
```   115   proof (induct xs arbitrary: ys)
```
```   116     case Nil then show ?case by simp
```
```   117   next
```
```   118     case (Cons x xs ys)
```
```   119     show ?case proof (cases "P x")
```
```   120       case True with Cons.hyps [of ys] Cons.prems
```
```   121       have "\<exists>zs. xs = zs @ ys \<and> (\<forall>a\<in>set zs. P a) \<and> no_leading P ys"
```
```   122         by simp
```
```   123       then obtain zs where "xs = zs @ ys" and "\<And>z. z \<in> set zs \<Longrightarrow> P z"
```
```   124         and *: "no_leading P ys"
```
```   125         by blast
```
```   126       with True have "x # xs = (x # zs) @ ys" and "\<And>z. z \<in> set (x # zs) \<Longrightarrow> P z"
```
```   127         by auto
```
```   128       with * show ?thesis
```
```   129         by blast    next
```
```   130       case False
```
```   131       with Cons show ?thesis by (cases ys) simp_all
```
```   132     qed
```
```   133   qed
```
```   134   with that show thesis
```
```   135     by blast
```
```   136 qed
```
```   137
```
```   138 lemma dropWhile_idem_iff:
```
```   139   "dropWhile P xs = xs \<longleftrightarrow> no_leading P xs"
```
```   140   by (cases xs) (auto elim: dropWhile_eq_obtain_leading)
```
```   141
```
```   142
```
```   143 abbreviation no_trailing :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
```
```   144 where
```
```   145   "no_trailing P xs \<equiv> no_leading P (rev xs)"
```
```   146
```
```   147 lemma no_trailing_unfold:
```
```   148   "no_trailing P xs \<longleftrightarrow> (xs \<noteq> [] \<longrightarrow> \<not> P (last xs))"
```
```   149   by (induct xs) simp_all
```
```   150
```
```   151 lemma no_trailing_Nil [simp, intro!]:
```
```   152   "no_trailing P []"
```
```   153   by simp
```
```   154
```
```   155 lemma no_trailing_Cons [simp]:
```
```   156   "no_trailing P (x # xs) \<longleftrightarrow> no_trailing P xs \<and> (xs = [] \<longrightarrow> \<not> P x)"
```
```   157   by simp
```
```   158
```
```   159 lemma no_trailing_append:
```
```   160   "no_trailing P (xs @ ys) \<longleftrightarrow> no_trailing P ys \<and> (ys = [] \<longrightarrow> no_trailing P xs)"
```
```   161   by (induct xs) simp_all
```
```   162
```
```   163 lemma no_trailing_append_Cons [simp]:
```
```   164   "no_trailing P (xs @ y # ys) \<longleftrightarrow> no_trailing P (y # ys)"
```
```   165   by simp
```
```   166
```
```   167 lemma no_trailing_strip_while [simp]:
```
```   168   "no_trailing P (strip_while P xs)"
```
```   169   by (induct xs rule: rev_induct) simp_all
```
```   170
```
```   171 lemma strip_while_idem [simp]:
```
```   172   "no_trailing P xs \<Longrightarrow> strip_while P xs = xs"
```
```   173   by (cases xs rule: rev_cases) simp_all
```
```   174
```
```   175 lemma strip_while_eq_obtain_trailing:
```
```   176   assumes "strip_while P xs = ys"
```
```   177   obtains zs where "xs = ys @ zs" and "\<And>z. z \<in> set zs \<Longrightarrow> P z" and "no_trailing P ys"
```
```   178 proof -
```
```   179   from assms have "rev (rev (dropWhile P (rev xs))) = rev ys"
```
```   180     by (simp add: strip_while_def)
```
```   181   then have "dropWhile P (rev xs) = rev ys"
```
```   182     by simp
```
```   183   then obtain zs where A: "rev xs = zs @ rev ys" and B: "\<And>z. z \<in> set zs \<Longrightarrow> P z"
```
```   184     and C: "no_trailing P ys"
```
```   185     using dropWhile_eq_obtain_leading by blast
```
```   186   from A have "rev (rev xs) = rev (zs @ rev ys)"
```
```   187     by simp
```
```   188   then have "xs = ys @ rev zs"
```
```   189     by simp
```
```   190   moreover from B have "\<And>z. z \<in> set (rev zs) \<Longrightarrow> P z"
```
```   191     by simp
```
```   192   ultimately show thesis using that C by blast
```
```   193 qed
```
```   194
```
```   195 lemma strip_while_idem_iff:
```
```   196   "strip_while P xs = xs \<longleftrightarrow> no_trailing P xs"
```
```   197 proof -
```
```   198   define ys where "ys = rev xs"
```
```   199   moreover have "strip_while P (rev ys) = rev ys \<longleftrightarrow> no_trailing P (rev ys)"
```
```   200     by (simp add: dropWhile_idem_iff)
```
```   201   ultimately show ?thesis by simp
```
```   202 qed
```
```   203
```
```   204 lemma no_trailing_map:
```
```   205   "no_trailing P (map f xs) \<longleftrightarrow> no_trailing (P \<circ> f) xs"
```
```   206   by (simp add: last_map no_trailing_unfold)
```
```   207
```
```   208 lemma no_trailing_drop [simp]:
```
```   209   "no_trailing P (drop n xs)" if "no_trailing P xs"
```
```   210 proof -
```
```   211   from that have "no_trailing P (take n xs @ drop n xs)"
```
```   212     by simp
```
```   213   then show ?thesis
```
```   214     by (simp only: no_trailing_append)
```
```   215 qed
```
```   216
```
```   217 lemma no_trailing_upt [simp]:
```
```   218   "no_trailing P [n..<m] \<longleftrightarrow> (n < m \<longrightarrow> \<not> P (m - 1))"
```
```   219   by (auto simp add: no_trailing_unfold)
```
```   220
```
```   221
```
```   222 definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a"
```
```   223 where
```
```   224   "nth_default dflt xs n = (if n < length xs then xs ! n else dflt)"
```
```   225
```
```   226 lemma nth_default_nth:
```
```   227   "n < length xs \<Longrightarrow> nth_default dflt xs n = xs ! n"
```
```   228   by (simp add: nth_default_def)
```
```   229
```
```   230 lemma nth_default_beyond:
```
```   231   "length xs \<le> n \<Longrightarrow> nth_default dflt xs n = dflt"
```
```   232   by (simp add: nth_default_def)
```
```   233
```
```   234 lemma nth_default_Nil [simp]:
```
```   235   "nth_default dflt [] n = dflt"
```
```   236   by (simp add: nth_default_def)
```
```   237
```
```   238 lemma nth_default_Cons:
```
```   239   "nth_default dflt (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default dflt xs n')"
```
```   240   by (simp add: nth_default_def split: nat.split)
```
```   241
```
```   242 lemma nth_default_Cons_0 [simp]:
```
```   243   "nth_default dflt (x # xs) 0 = x"
```
```   244   by (simp add: nth_default_Cons)
```
```   245
```
```   246 lemma nth_default_Cons_Suc [simp]:
```
```   247   "nth_default dflt (x # xs) (Suc n) = nth_default dflt xs n"
```
```   248   by (simp add: nth_default_Cons)
```
```   249
```
```   250 lemma nth_default_replicate_dflt [simp]:
```
```   251   "nth_default dflt (replicate n dflt) m = dflt"
```
```   252   by (simp add: nth_default_def)
```
```   253
```
```   254 lemma nth_default_append:
```
```   255   "nth_default dflt (xs @ ys) n =
```
```   256     (if n < length xs then nth xs n else nth_default dflt ys (n - length xs))"
```
```   257   by (auto simp add: nth_default_def nth_append)
```
```   258
```
```   259 lemma nth_default_append_trailing [simp]:
```
```   260   "nth_default dflt (xs @ replicate n dflt) = nth_default dflt xs"
```
```   261   by (simp add: fun_eq_iff nth_default_append) (simp add: nth_default_def)
```
```   262
```
```   263 lemma nth_default_snoc_default [simp]:
```
```   264   "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
```
```   265   by (auto simp add: nth_default_def fun_eq_iff nth_append)
```
```   266
```
```   267 lemma nth_default_eq_dflt_iff:
```
```   268   "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
```
```   269   by (simp add: nth_default_def)
```
```   270
```
```   271 lemma nth_default_take_eq:
```
```   272   "nth_default dflt (take m xs) n =
```
```   273     (if n < m then nth_default dflt xs n else dflt)"
```
```   274   by (simp add: nth_default_def)
```
```   275
```
```   276 lemma in_enumerate_iff_nth_default_eq:
```
```   277   "x \<noteq> dflt \<Longrightarrow> (n, x) \<in> set (enumerate 0 xs) \<longleftrightarrow> nth_default dflt xs n = x"
```
```   278   by (auto simp add: nth_default_def in_set_conv_nth enumerate_eq_zip)
```
```   279
```
```   280 lemma last_conv_nth_default:
```
```   281   assumes "xs \<noteq> []"
```
```   282   shows "last xs = nth_default dflt xs (length xs - 1)"
```
```   283   using assms by (simp add: nth_default_def last_conv_nth)
```
```   284
```
```   285 lemma nth_default_map_eq:
```
```   286   "f dflt' = dflt \<Longrightarrow> nth_default dflt (map f xs) n = f (nth_default dflt' xs n)"
```
```   287   by (simp add: nth_default_def)
```
```   288
```
```   289 lemma finite_nth_default_neq_default [simp]:
```
```   290   "finite {k. nth_default dflt xs k \<noteq> dflt}"
```
```   291   by (simp add: nth_default_def)
```
```   292
```
```   293 lemma sorted_list_of_set_nth_default:
```
```   294   "sorted_list_of_set {k. nth_default dflt xs k \<noteq> dflt} = map fst (filter (\<lambda>(_, x). x \<noteq> dflt) (enumerate 0 xs))"
```
```   295   by (rule sorted_distinct_set_unique) (auto simp add: nth_default_def in_set_conv_nth
```
```   296     sorted_filter distinct_map_filter enumerate_eq_zip intro: rev_image_eqI)
```
```   297
```
```   298 lemma map_nth_default:
```
```   299   "map (nth_default x xs) [0..<length xs] = xs"
```
```   300 proof -
```
```   301   have *: "map (nth_default x xs) [0..<length xs] = map (List.nth xs) [0..<length xs]"
```
```   302     by (rule map_cong) (simp_all add: nth_default_nth)
```
```   303   show ?thesis by (simp add: * map_nth)
```
```   304 qed
```
```   305
```
```   306 lemma range_nth_default [simp]:
```
```   307   "range (nth_default dflt xs) = insert dflt (set xs)"
```
```   308   by (auto simp add: nth_default_def [abs_def] in_set_conv_nth)
```
```   309
```
```   310 lemma nth_strip_while:
```
```   311   assumes "n < length (strip_while P xs)"
```
```   312   shows "strip_while P xs ! n = xs ! n"
```
```   313 proof -
```
```   314   have "length (dropWhile P (rev xs)) + length (takeWhile P (rev xs)) = length xs"
```
```   315     by (subst add.commute)
```
```   316       (simp add: arg_cong [where f=length, OF takeWhile_dropWhile_id, unfolded length_append])
```
```   317   then show ?thesis using assms
```
```   318     by (simp add: strip_while_def rev_nth dropWhile_nth)
```
```   319 qed
```
```   320
```
```   321 lemma length_strip_while_le:
```
```   322   "length (strip_while P xs) \<le> length xs"
```
```   323   unfolding strip_while_def o_def length_rev
```
```   324   by (subst (2) length_rev[symmetric])
```
```   325     (simp add: strip_while_def length_dropWhile_le del: length_rev)
```
```   326
```
```   327 lemma nth_default_strip_while_dflt [simp]:
```
```   328   "nth_default dflt (strip_while ((=) dflt) xs) = nth_default dflt xs"
```
```   329   by (induct xs rule: rev_induct) auto
```
```   330
```
```   331 lemma nth_default_eq_iff:
```
```   332   "nth_default dflt xs = nth_default dflt ys
```
```   333      \<longleftrightarrow> strip_while (HOL.eq dflt) xs = strip_while (HOL.eq dflt) ys" (is "?P \<longleftrightarrow> ?Q")
```
```   334 proof
```
```   335   let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
```
```   336   assume ?P
```
```   337   then have eq: "nth_default dflt ?xs = nth_default dflt ?ys"
```
```   338     by simp
```
```   339   have len: "length ?xs = length ?ys"
```
```   340   proof (rule ccontr)
```
```   341     assume len: "length ?xs \<noteq> length ?ys"
```
```   342     { fix xs ys :: "'a list"
```
```   343       let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
```
```   344       assume eq: "nth_default dflt ?xs = nth_default dflt ?ys"
```
```   345       assume len: "length ?xs < length ?ys"
```
```   346       then have "length ?ys > 0" by arith
```
```   347       then have "?ys \<noteq> []" by simp
```
```   348       with last_conv_nth_default [of ?ys dflt]
```
```   349       have "last ?ys = nth_default dflt ?ys (length ?ys - 1)"
```
```   350         by auto
```
```   351       moreover from \<open>?ys \<noteq> []\<close> no_trailing_strip_while [of "HOL.eq dflt" ys]
```
```   352         have "last ?ys \<noteq> dflt" by (simp add: no_trailing_unfold)
```
```   353       ultimately have "nth_default dflt ?xs (length ?ys - 1) \<noteq> dflt"
```
```   354         using eq by simp
```
```   355       moreover from len have "length ?ys - 1 \<ge> length ?xs" by simp
```
```   356       ultimately have False by (simp only: nth_default_beyond) simp
```
```   357     }
```
```   358     from this [of xs ys] this [of ys xs] len eq show False
```
```   359       by (auto simp only: linorder_class.neq_iff)
```
```   360   qed
```
```   361   then show ?Q
```
```   362   proof (rule nth_equalityI [rule_format])
```
```   363     fix n
```
```   364     assume n: "n < length ?xs"
```
```   365     with len have "n < length ?ys"
```
```   366       by simp
```
```   367     with n have xs: "nth_default dflt ?xs n = ?xs ! n"
```
```   368       and ys: "nth_default dflt ?ys n = ?ys ! n"
```
```   369       by (simp_all only: nth_default_nth)
```
```   370     with eq show "?xs ! n = ?ys ! n"
```
```   371       by simp
```
```   372   qed
```
```   373 next
```
```   374   assume ?Q
```
```   375   then have "nth_default dflt (strip_while (HOL.eq dflt) xs) = nth_default dflt (strip_while (HOL.eq dflt) ys)"
```
```   376     by simp
```
```   377   then show ?P
```
```   378     by simp
```
```   379 qed
```
```   380
```
```   381 end
```
```   382
```