more material on lists
authorhaftmann
Wed Sep 10 22:52:46 2014 +0200 (2014-09-10)
changeset 58295c8a8e7c37986
parent 58294 7f990b3d5189
child 58296 759e47518d80
more material on lists
src/HOL/Library/More_List.thy
     1.1 --- a/src/HOL/Library/More_List.thy	Wed Sep 10 14:58:02 2014 +0200
     1.2 +++ b/src/HOL/Library/More_List.thy	Wed Sep 10 22:52:46 2014 +0200
     1.3 @@ -7,12 +7,14 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -text \<open>FIXME adapted from @{file "~~/src/HOL/Library/Polynomial.thy"}; to be merged back\<close>
     1.8 -
     1.9  definition strip_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.10  where
    1.11    "strip_while P = rev \<circ> dropWhile P \<circ> rev"
    1.12  
    1.13 +lemma strip_while_rev [simp]:
    1.14 +  "strip_while P (rev xs) = rev (dropWhile P xs)"
    1.15 +  by (simp add: strip_while_def)
    1.16 +  
    1.17  lemma strip_while_Nil [simp]:
    1.18    "strip_while P [] = []"
    1.19    by (simp add: strip_while_def)
    1.20 @@ -62,13 +64,120 @@
    1.21    "strip_while P (map f xs) = map f (strip_while (P \<circ> f) xs)"
    1.22    by (simp add: strip_while_def rev_map dropWhile_map)
    1.23  
    1.24 -lemma dropWhile_idI:
    1.25 -  "(xs \<noteq> [] \<Longrightarrow> \<not> P (hd xs)) \<Longrightarrow> dropWhile P xs = xs"
    1.26 -  by (metis dropWhile.simps(1) dropWhile.simps(2) list.collapse)
    1.27 +
    1.28 +definition no_leading :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
    1.29 +where
    1.30 +  "no_leading P xs \<longleftrightarrow> (xs \<noteq> [] \<longrightarrow> \<not> P (hd xs))"
    1.31 +
    1.32 +lemma no_leading_Nil [simp, intro!]:
    1.33 +  "no_leading P []"
    1.34 +  by (simp add: no_leading_def)
    1.35 +
    1.36 +lemma no_leading_Cons [simp, intro!]:
    1.37 +  "no_leading P (x # xs) \<longleftrightarrow> \<not> P x"
    1.38 +  by (simp add: no_leading_def)
    1.39 +
    1.40 +lemma no_leading_append [simp]:
    1.41 +  "no_leading P (xs @ ys) \<longleftrightarrow> no_leading P xs \<and> (xs = [] \<longrightarrow> no_leading P ys)"
    1.42 +  by (induct xs) simp_all
    1.43 +
    1.44 +lemma no_leading_dropWhile [simp]:
    1.45 +  "no_leading P (dropWhile P xs)"
    1.46 +  by (induct xs) simp_all
    1.47 +
    1.48 +lemma dropWhile_eq_obtain_leading:
    1.49 +  assumes "dropWhile P xs = ys"
    1.50 +  obtains zs where "xs = zs @ ys" and "\<And>z. z \<in> set zs \<Longrightarrow> P z" and "no_leading P ys"
    1.51 +proof -
    1.52 +  from assms have "\<exists>zs. xs = zs @ ys \<and> (\<forall>z \<in> set zs. P z) \<and> no_leading P ys"
    1.53 +  proof (induct xs arbitrary: ys)
    1.54 +    case Nil then show ?case by simp
    1.55 +  next
    1.56 +    case (Cons x xs ys)
    1.57 +    show ?case proof (cases "P x")
    1.58 +      case True with Cons.hyps [of ys] Cons.prems
    1.59 +      have "\<exists>zs. xs = zs @ ys \<and> (\<forall>a\<in>set zs. P a) \<and> no_leading P ys"
    1.60 +        by simp
    1.61 +      then obtain zs where "xs = zs @ ys" and "\<And>z. z \<in> set zs \<Longrightarrow> P z"
    1.62 +        and *: "no_leading P ys"
    1.63 +        by blast
    1.64 +      with True have "x # xs = (x # zs) @ ys" and "\<And>z. z \<in> set (x # zs) \<Longrightarrow> P z"
    1.65 +        by auto
    1.66 +      with * show ?thesis
    1.67 +        by blast    next
    1.68 +      case False
    1.69 +      with Cons show ?thesis by (cases ys) simp_all
    1.70 +    qed
    1.71 +  qed
    1.72 +  with that show thesis
    1.73 +    by blast
    1.74 +qed
    1.75 +
    1.76 +lemma dropWhile_idem_iff:
    1.77 +  "dropWhile P xs = xs \<longleftrightarrow> no_leading P xs"
    1.78 +  by (cases xs) (auto elim: dropWhile_eq_obtain_leading)
    1.79 +
    1.80  
    1.81 -lemma strip_while_idI:
    1.82 -  "(xs \<noteq> [] \<Longrightarrow> \<not> P (last xs)) \<Longrightarrow> strip_while P xs = xs"
    1.83 -  using dropWhile_idI [of "rev xs"] by (simp add: strip_while_def hd_rev)
    1.84 +abbreviation no_trailing :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
    1.85 +where
    1.86 +  "no_trailing P xs \<equiv> no_leading P (rev xs)"
    1.87 +
    1.88 +lemma no_trailing_unfold:
    1.89 +  "no_trailing P xs \<longleftrightarrow> (xs \<noteq> [] \<longrightarrow> \<not> P (last xs))"
    1.90 +  by (induct xs) simp_all
    1.91 +
    1.92 +lemma no_trailing_Nil [simp, intro!]:
    1.93 +  "no_trailing P []"
    1.94 +  by simp
    1.95 +
    1.96 +lemma no_trailing_Cons [simp]:
    1.97 +  "no_trailing P (x # xs) \<longleftrightarrow> no_trailing P xs \<and> (xs = [] \<longrightarrow> \<not> P x)"
    1.98 +  by simp
    1.99 +
   1.100 +lemma no_trailing_append_Cons [simp]:
   1.101 +  "no_trailing P (xs @ y # ys) \<longleftrightarrow> no_trailing P (y # ys)"
   1.102 +  by simp
   1.103 +
   1.104 +lemma no_trailing_strip_while [simp]:
   1.105 +  "no_trailing P (strip_while P xs)"
   1.106 +  by (induct xs rule: rev_induct) simp_all
   1.107 +
   1.108 +lemma strip_while_eq_obtain_trailing:
   1.109 +  assumes "strip_while P xs = ys"
   1.110 +  obtains zs where "xs = ys @ zs" and "\<And>z. z \<in> set zs \<Longrightarrow> P z" and "no_trailing P ys"
   1.111 +proof -
   1.112 +  from assms have "rev (rev (dropWhile P (rev xs))) = rev ys"
   1.113 +    by (simp add: strip_while_def)
   1.114 +  then have "dropWhile P (rev xs) = rev ys"
   1.115 +    by simp
   1.116 +  then obtain zs where A: "rev xs = zs @ rev ys" and B: "\<And>z. z \<in> set zs \<Longrightarrow> P z"
   1.117 +    and C: "no_trailing P ys"
   1.118 +    using dropWhile_eq_obtain_leading by blast
   1.119 +  from A have "rev (rev xs) = rev (zs @ rev ys)"
   1.120 +    by simp
   1.121 +  then have "xs = ys @ rev zs"
   1.122 +    by simp
   1.123 +  moreover from B have "\<And>z. z \<in> set (rev zs) \<Longrightarrow> P z"
   1.124 +    by simp
   1.125 +  ultimately show thesis using that C by blast
   1.126 +qed
   1.127 +
   1.128 +lemma strip_while_idem_iff:
   1.129 +  "strip_while P xs = xs \<longleftrightarrow> no_trailing P xs"
   1.130 +proof -
   1.131 +  def ys \<equiv> "rev xs"
   1.132 +  moreover have "strip_while P (rev ys) = rev ys \<longleftrightarrow> no_trailing P (rev ys)"
   1.133 +    by (simp add: dropWhile_idem_iff)
   1.134 +  ultimately show ?thesis by simp
   1.135 +qed
   1.136 +
   1.137 +lemma no_trailing_map:
   1.138 +  "no_trailing P (map f xs) = no_trailing (P \<circ> f) xs"
   1.139 +  by (simp add: last_map no_trailing_unfold)
   1.140 +
   1.141 +lemma no_trailing_upt [simp]:
   1.142 +  "no_trailing P [n..<m] \<longleftrightarrow> (n < m \<longrightarrow> \<not> P (m - 1))"
   1.143 +  by (auto simp add: no_trailing_unfold)
   1.144  
   1.145  
   1.146  definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a"
   1.147 @@ -153,3 +262,4 @@
   1.148    by (simp add: nth_default_def)
   1.149  
   1.150  end
   1.151 +