src/HOL/Library/More_List.thy
author haftmann
Sun Sep 07 09:49:05 2014 +0200 (2014-09-07)
changeset 58199 5fbe474b5da8
child 58295 c8a8e7c37986
permissions -rw-r--r--
explicit theory with additional, less commonly used list operations
haftmann@58199
     1
(* Author: Andreas Lochbihler, ETH Z├╝rich
haftmann@58199
     2
   Author: Florian Haftmann, TU Muenchen  *)
haftmann@58199
     3
haftmann@58199
     4
header \<open>Less common functions on lists\<close>
haftmann@58199
     5
haftmann@58199
     6
theory More_List
haftmann@58199
     7
imports Main
haftmann@58199
     8
begin
haftmann@58199
     9
haftmann@58199
    10
text \<open>FIXME adapted from @{file "~~/src/HOL/Library/Polynomial.thy"}; to be merged back\<close>
haftmann@58199
    11
haftmann@58199
    12
definition strip_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
haftmann@58199
    13
where
haftmann@58199
    14
  "strip_while P = rev \<circ> dropWhile P \<circ> rev"
haftmann@58199
    15
haftmann@58199
    16
lemma strip_while_Nil [simp]:
haftmann@58199
    17
  "strip_while P [] = []"
haftmann@58199
    18
  by (simp add: strip_while_def)
haftmann@58199
    19
haftmann@58199
    20
lemma strip_while_append [simp]:
haftmann@58199
    21
  "\<not> P x \<Longrightarrow> strip_while P (xs @ [x]) = xs @ [x]"
haftmann@58199
    22
  by (simp add: strip_while_def)
haftmann@58199
    23
haftmann@58199
    24
lemma strip_while_append_rec [simp]:
haftmann@58199
    25
  "P x \<Longrightarrow> strip_while P (xs @ [x]) = strip_while P xs"
haftmann@58199
    26
  by (simp add: strip_while_def)
haftmann@58199
    27
haftmann@58199
    28
lemma strip_while_Cons [simp]:
haftmann@58199
    29
  "\<not> P x \<Longrightarrow> strip_while P (x # xs) = x # strip_while P xs"
haftmann@58199
    30
  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
haftmann@58199
    31
haftmann@58199
    32
lemma strip_while_eq_Nil [simp]:
haftmann@58199
    33
  "strip_while P xs = [] \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
haftmann@58199
    34
  by (simp add: strip_while_def)
haftmann@58199
    35
haftmann@58199
    36
lemma strip_while_eq_Cons_rec:
haftmann@58199
    37
  "strip_while P (x # xs) = x # strip_while P xs \<longleftrightarrow> \<not> (P x \<and> (\<forall>x\<in>set xs. P x))"
haftmann@58199
    38
  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
haftmann@58199
    39
haftmann@58199
    40
lemma strip_while_not_last [simp]:
haftmann@58199
    41
  "\<not> P (last xs) \<Longrightarrow> strip_while P xs = xs"
haftmann@58199
    42
  by (cases xs rule: rev_cases) simp_all
haftmann@58199
    43
haftmann@58199
    44
lemma split_strip_while_append:
haftmann@58199
    45
  fixes xs :: "'a list"
haftmann@58199
    46
  obtains ys zs :: "'a list"
haftmann@58199
    47
  where "strip_while P xs = ys" and "\<forall>x\<in>set zs. P x" and "xs = ys @ zs"
haftmann@58199
    48
proof (rule that)
haftmann@58199
    49
  show "strip_while P xs = strip_while P xs" ..
haftmann@58199
    50
  show "\<forall>x\<in>set (rev (takeWhile P (rev xs))). P x" by (simp add: takeWhile_eq_all_conv [symmetric])
haftmann@58199
    51
  have "rev xs = rev (strip_while P xs @ rev (takeWhile P (rev xs)))"
haftmann@58199
    52
    by (simp add: strip_while_def)
haftmann@58199
    53
  then show "xs = strip_while P xs @ rev (takeWhile P (rev xs))"
haftmann@58199
    54
    by (simp only: rev_is_rev_conv)
haftmann@58199
    55
qed
haftmann@58199
    56
haftmann@58199
    57
lemma strip_while_snoc [simp]:
haftmann@58199
    58
  "strip_while P (xs @ [x]) = (if P x then strip_while P xs else xs @ [x])"
haftmann@58199
    59
  by (simp add: strip_while_def)
haftmann@58199
    60
haftmann@58199
    61
lemma strip_while_map:
haftmann@58199
    62
  "strip_while P (map f xs) = map f (strip_while (P \<circ> f) xs)"
haftmann@58199
    63
  by (simp add: strip_while_def rev_map dropWhile_map)
haftmann@58199
    64
haftmann@58199
    65
lemma dropWhile_idI:
haftmann@58199
    66
  "(xs \<noteq> [] \<Longrightarrow> \<not> P (hd xs)) \<Longrightarrow> dropWhile P xs = xs"
haftmann@58199
    67
  by (metis dropWhile.simps(1) dropWhile.simps(2) list.collapse)
haftmann@58199
    68
haftmann@58199
    69
lemma strip_while_idI:
haftmann@58199
    70
  "(xs \<noteq> [] \<Longrightarrow> \<not> P (last xs)) \<Longrightarrow> strip_while P xs = xs"
haftmann@58199
    71
  using dropWhile_idI [of "rev xs"] by (simp add: strip_while_def hd_rev)
haftmann@58199
    72
haftmann@58199
    73
haftmann@58199
    74
definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a"
haftmann@58199
    75
where
haftmann@58199
    76
  "nth_default x xs n = (if n < length xs then xs ! n else x)"
haftmann@58199
    77
haftmann@58199
    78
lemma nth_default_Nil [simp]:
haftmann@58199
    79
  "nth_default y [] n = y"
haftmann@58199
    80
  by (simp add: nth_default_def)
haftmann@58199
    81
haftmann@58199
    82
lemma nth_default_Cons_0 [simp]:
haftmann@58199
    83
  "nth_default y (x # xs) 0 = x"
haftmann@58199
    84
  by (simp add: nth_default_def)
haftmann@58199
    85
haftmann@58199
    86
lemma nth_default_Cons_Suc [simp]:
haftmann@58199
    87
  "nth_default y (x # xs) (Suc n) = nth_default y xs n"
haftmann@58199
    88
  by (simp add: nth_default_def)
haftmann@58199
    89
haftmann@58199
    90
lemma nth_default_map_eq:
haftmann@58199
    91
  "f y = x \<Longrightarrow> nth_default x (map f xs) n = f (nth_default y xs n)"
haftmann@58199
    92
  by (simp add: nth_default_def)
haftmann@58199
    93
haftmann@58199
    94
lemma nth_default_strip_while_eq [simp]:
haftmann@58199
    95
  "nth_default x (strip_while (HOL.eq x) xs) n = nth_default x xs n"
haftmann@58199
    96
proof -
haftmann@58199
    97
  from split_strip_while_append obtain ys zs
haftmann@58199
    98
    where "strip_while (HOL.eq x) xs = ys" and "\<forall>z\<in>set zs. x = z" and "xs = ys @ zs" by blast
haftmann@58199
    99
  then show ?thesis by (simp add: nth_default_def not_less nth_append)
haftmann@58199
   100
qed
haftmann@58199
   101
haftmann@58199
   102
lemma nth_default_Cons:
haftmann@58199
   103
  "nth_default y (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default y xs n')"
haftmann@58199
   104
  by (simp split: nat.split)
haftmann@58199
   105
haftmann@58199
   106
lemma nth_default_nth:
haftmann@58199
   107
  "n < length xs \<Longrightarrow> nth_default y xs n = xs ! n"
haftmann@58199
   108
  by (simp add: nth_default_def)
haftmann@58199
   109
haftmann@58199
   110
lemma nth_default_beyond:
haftmann@58199
   111
  "length xs \<le> n \<Longrightarrow> nth_default y xs n = y"
haftmann@58199
   112
  by (simp add: nth_default_def)
haftmann@58199
   113
haftmann@58199
   114
lemma range_nth_default [simp]:
haftmann@58199
   115
  "range (nth_default dflt xs) = insert dflt (set xs)"
haftmann@58199
   116
  by (auto simp add: nth_default_def[abs_def] in_set_conv_nth)
haftmann@58199
   117
haftmann@58199
   118
lemma nth_strip_while:
haftmann@58199
   119
  assumes "n < length (strip_while P xs)"
haftmann@58199
   120
  shows "strip_while P xs ! n = xs ! n"
haftmann@58199
   121
proof -
haftmann@58199
   122
  have "length (dropWhile P (rev xs)) + length (takeWhile P (rev xs)) = length xs"
haftmann@58199
   123
    by (subst add.commute)
haftmann@58199
   124
      (simp add: arg_cong [where f=length, OF takeWhile_dropWhile_id, unfolded length_append])
haftmann@58199
   125
  then show ?thesis using assms
haftmann@58199
   126
    by (simp add: strip_while_def rev_nth dropWhile_nth)
haftmann@58199
   127
qed
haftmann@58199
   128
haftmann@58199
   129
lemma length_strip_while_le:
haftmann@58199
   130
  "length (strip_while P xs) \<le> length xs"
haftmann@58199
   131
  unfolding strip_while_def o_def length_rev
haftmann@58199
   132
  by (subst (2) length_rev[symmetric])
haftmann@58199
   133
    (simp add: strip_while_def length_dropWhile_le del: length_rev)
haftmann@58199
   134
haftmann@58199
   135
lemma finite_nth_default_neq_default [simp]:
haftmann@58199
   136
  "finite {k. nth_default dflt xs k \<noteq> dflt}"
haftmann@58199
   137
  by (simp add: nth_default_def)
haftmann@58199
   138
haftmann@58199
   139
lemma sorted_list_of_set_nth_default:
haftmann@58199
   140
  "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))"
haftmann@58199
   141
  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)
haftmann@58199
   142
haftmann@58199
   143
lemma nth_default_snoc_default [simp]:
haftmann@58199
   144
  "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
haftmann@58199
   145
  by (auto simp add: nth_default_def fun_eq_iff nth_append)
haftmann@58199
   146
haftmann@58199
   147
lemma nth_default_strip_while_dflt [simp]:
haftmann@58199
   148
 "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs"
haftmann@58199
   149
  by (induct xs rule: rev_induct) auto
haftmann@58199
   150
haftmann@58199
   151
lemma nth_default_eq_dflt_iff:
haftmann@58199
   152
  "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
haftmann@58199
   153
  by (simp add: nth_default_def)
haftmann@58199
   154
haftmann@58199
   155
end