src/HOL/Library/More_List.thy
 author blanchet Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) changeset 58425 246985c6b20b parent 58295 c8a8e7c37986 child 58437 8d124c73c37a permissions -rw-r--r--
simpler proof
```     1 (* Author: Andreas Lochbihler, ETH Zürich
```
```     2    Author: Florian Haftmann, TU Muenchen  *)
```
```     3
```
```     4 header \<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   def ys \<equiv> "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 x xs n = (if n < length xs then xs ! n else x)"
```
```   186
```
```   187 lemma nth_default_Nil [simp]:
```
```   188   "nth_default y [] n = y"
```
```   189   by (simp add: nth_default_def)
```
```   190
```
```   191 lemma nth_default_Cons_0 [simp]:
```
```   192   "nth_default y (x # xs) 0 = x"
```
```   193   by (simp add: nth_default_def)
```
```   194
```
```   195 lemma nth_default_Cons_Suc [simp]:
```
```   196   "nth_default y (x # xs) (Suc n) = nth_default y xs n"
```
```   197   by (simp add: nth_default_def)
```
```   198
```
```   199 lemma nth_default_map_eq:
```
```   200   "f y = x \<Longrightarrow> nth_default x (map f xs) n = f (nth_default y xs n)"
```
```   201   by (simp add: nth_default_def)
```
```   202
```
```   203 lemma nth_default_strip_while_eq [simp]:
```
```   204   "nth_default x (strip_while (HOL.eq x) xs) n = nth_default x xs n"
```
```   205 proof -
```
```   206   from split_strip_while_append obtain ys zs
```
```   207     where "strip_while (HOL.eq x) xs = ys" and "\<forall>z\<in>set zs. x = z" and "xs = ys @ zs" by blast
```
```   208   then show ?thesis by (simp add: nth_default_def not_less nth_append)
```
```   209 qed
```
```   210
```
```   211 lemma nth_default_Cons:
```
```   212   "nth_default y (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default y xs n')"
```
```   213   by (simp split: nat.split)
```
```   214
```
```   215 lemma nth_default_nth:
```
```   216   "n < length xs \<Longrightarrow> nth_default y xs n = xs ! n"
```
```   217   by (simp add: nth_default_def)
```
```   218
```
```   219 lemma nth_default_beyond:
```
```   220   "length xs \<le> n \<Longrightarrow> nth_default y xs n = y"
```
```   221   by (simp add: nth_default_def)
```
```   222
```
```   223 lemma range_nth_default [simp]:
```
```   224   "range (nth_default dflt xs) = insert dflt (set xs)"
```
```   225   by (auto simp add: nth_default_def[abs_def] in_set_conv_nth)
```
```   226
```
```   227 lemma nth_strip_while:
```
```   228   assumes "n < length (strip_while P xs)"
```
```   229   shows "strip_while P xs ! n = xs ! n"
```
```   230 proof -
```
```   231   have "length (dropWhile P (rev xs)) + length (takeWhile P (rev xs)) = length xs"
```
```   232     by (subst add.commute)
```
```   233       (simp add: arg_cong [where f=length, OF takeWhile_dropWhile_id, unfolded length_append])
```
```   234   then show ?thesis using assms
```
```   235     by (simp add: strip_while_def rev_nth dropWhile_nth)
```
```   236 qed
```
```   237
```
```   238 lemma length_strip_while_le:
```
```   239   "length (strip_while P xs) \<le> length xs"
```
```   240   unfolding strip_while_def o_def length_rev
```
```   241   by (subst (2) length_rev[symmetric])
```
```   242     (simp add: strip_while_def length_dropWhile_le del: length_rev)
```
```   243
```
```   244 lemma finite_nth_default_neq_default [simp]:
```
```   245   "finite {k. nth_default dflt xs k \<noteq> dflt}"
```
```   246   by (simp add: nth_default_def)
```
```   247
```
```   248 lemma sorted_list_of_set_nth_default:
```
```   249   "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))"
```
```   250   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)
```
```   251
```
```   252 lemma nth_default_snoc_default [simp]:
```
```   253   "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
```
```   254   by (auto simp add: nth_default_def fun_eq_iff nth_append)
```
```   255
```
```   256 lemma nth_default_strip_while_dflt [simp]:
```
```   257  "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs"
```
```   258   by (induct xs rule: rev_induct) auto
```
```   259
```
```   260 lemma nth_default_eq_dflt_iff:
```
```   261   "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
```
```   262   by (simp add: nth_default_def)
```
```   263
```
```   264 end
```
```   265
```