summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Wed, 05 Apr 2017 13:47:38 +0200 | |

changeset 65388 | a8d868477bc0 |

parent 65387 | 5dbe02addca5 |

child 65389 | 6f9c6ae27984 |

more on lists

--- a/src/HOL/Library/More_List.thy Wed Apr 05 10:26:28 2017 +0200 +++ b/src/HOL/Library/More_List.thy Wed Apr 05 13:47:38 2017 +0200 @@ -39,10 +39,6 @@ "strip_while P (x # xs) = x # strip_while P xs \<longleftrightarrow> \<not> (P x \<and> (\<forall>x\<in>set xs. P x))" by (induct xs rule: rev_induct) (simp_all add: strip_while_def) -lemma strip_while_not_last [simp]: - "\<not> P (last xs) \<Longrightarrow> strip_while P xs = xs" - by (cases xs rule: rev_cases) simp_all - lemma split_strip_while_append: fixes xs :: "'a list" obtains ys zs :: "'a list" @@ -64,6 +60,32 @@ "strip_while P (map f xs) = map f (strip_while (P \<circ> f) xs)" by (simp add: strip_while_def rev_map dropWhile_map) +lemma strip_while_dropWhile_commute: + "strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)" +proof (induct xs) + case Nil + then show ?case + by simp +next + case (Cons x xs) + show ?case + proof (cases "\<forall>y\<in>set xs. P y") + case True + with dropWhile_append2 [of "rev xs"] show ?thesis + by (auto simp add: strip_while_def dest: set_dropWhileD) + next + case False + then obtain y where "y \<in> set xs" and "\<not> P y" + by blast + with Cons dropWhile_append3 [of P y "rev xs"] show ?thesis + by (simp add: strip_while_def) + qed +qed + +lemma dropWhile_strip_while_commute: + "dropWhile P (strip_while Q xs) = strip_while Q (dropWhile P xs)" + by (simp add: strip_while_dropWhile_commute) + definition no_leading :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where @@ -134,6 +156,10 @@ "no_trailing P (x # xs) \<longleftrightarrow> no_trailing P xs \<and> (xs = [] \<longrightarrow> \<not> P x)" by simp +lemma no_trailing_append: + "no_trailing P (xs @ ys) \<longleftrightarrow> no_trailing P ys \<and> (ys = [] \<longrightarrow> no_trailing P xs)" + by (induct xs) simp_all + lemma no_trailing_append_Cons [simp]: "no_trailing P (xs @ y # ys) \<longleftrightarrow> no_trailing P (y # ys)" by simp @@ -142,6 +168,10 @@ "no_trailing P (strip_while P xs)" by (induct xs rule: rev_induct) simp_all +lemma strip_while_idem [simp]: + "no_trailing P xs \<Longrightarrow> strip_while P xs = xs" + by (cases xs rule: rev_cases) simp_all + lemma strip_while_eq_obtain_trailing: assumes "strip_while P xs = ys" obtains zs where "xs = ys @ zs" and "\<And>z. z \<in> set zs \<Longrightarrow> P z" and "no_trailing P ys" @@ -172,9 +202,18 @@ qed lemma no_trailing_map: - "no_trailing P (map f xs) = no_trailing (P \<circ> f) xs" + "no_trailing P (map f xs) \<longleftrightarrow> no_trailing (P \<circ> f) xs" by (simp add: last_map no_trailing_unfold) +lemma no_trailing_drop [simp]: + "no_trailing P (drop n xs)" if "no_trailing P xs" +proof - + from that have "no_trailing P (take n xs @ drop n xs)" + by simp + then show ?thesis + by (simp only: no_trailing_append) +qed + lemma no_trailing_upt [simp]: "no_trailing P [n..<m] \<longleftrightarrow> (n < m \<longrightarrow> \<not> P (m - 1))" by (auto simp add: no_trailing_unfold)