# HG changeset patch
# User traytel
# Date 1363338503 -3600
# Node ID e96447ea13c9b4dc399452076f95cc12a1e23522
# Parent  48eb29821bd9c988aa22fb354be310e2b82684b3
extended stream library (sdrop_while)

diff -r 48eb29821bd9 -r e96447ea13c9 src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Thu Mar 14 14:25:55 2013 +0100
+++ b/src/HOL/BNF/Examples/Stream.thy	Fri Mar 15 10:08:23 2013 +0100
@@ -207,6 +207,29 @@
 lemma sdrop_add[simp]: "sdrop n (sdrop m s) = sdrop (m + n) s"
   by (induct m arbitrary: s) auto
 
+partial_function (tailrec) sdrop_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where 
+  "sdrop_while P s = (if P (shd s) then sdrop_while P (stl s) else s)"
+
+lemma sdrop_while_Stream[code]:
+  "sdrop_while P (Stream a s) = (if P a then sdrop_while P s else Stream a s)"
+  by (subst sdrop_while.simps) simp
+
+lemma sdrop_while_sdrop_LEAST:
+  assumes "\<exists>n. P (s !! n)"
+  shows "sdrop_while (Not o P) s = sdrop (LEAST n. P (s !! n)) s"
+proof -
+  from assms obtain m where "P (s !! m)" "\<And>n. P (s !! n) \<Longrightarrow> m \<le> n"
+    and *: "(LEAST n. P (s !! n)) = m" by atomize_elim (auto intro: LeastI Least_le)
+  thus ?thesis unfolding *
+  proof (induct m arbitrary: s)
+    case (Suc m)
+    hence "sdrop_while (Not \<circ> P) (stl s) = sdrop m (stl s)"
+      by (metis (full_types) not_less_eq_eq snth.simps(2))
+    moreover from Suc(3) have "\<not> (P (s !! 0))" by blast
+    ultimately show ?case by (subst sdrop_while.simps) simp
+  qed (metis comp_apply sdrop.simps(1) sdrop_while.simps snth.simps(1))
+qed
+
 
 subsection {* unary predicates lifted to streams *}