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