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
+  qed
+qed
+
+lemma dropWhile_strip_while_commute:
+  "dropWhile P (strip_while Q xs) = strip_while Q (dropWhile P xs)"
+

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"