author haftmann Wed Sep 10 22:52:46 2014 +0200 (2014-09-10) changeset 58295 c8a8e7c37986 parent 58294 7f990b3d5189 child 58296 759e47518d80
more material on lists
```     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.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.35 +
1.37 +  "no_leading P (x # xs) \<longleftrightarrow> \<not> P x"
1.39 +
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.45 +  "no_leading P (dropWhile P xs)"
1.46 +  by (induct xs) simp_all
1.47 +
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 @@