# HG changeset patch
# User traytel
# Date 1375956062 -7200
# Node ID 41ebc19276eacf2b4d8ed68ecf7b565b319828c1
# Parent  f8fca14c8cbd6d10f80059c7b1f11771c74b3fbd
filter function on streams

diff -r f8fca14c8cbd -r 41ebc19276ea src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Thu Aug 08 12:00:45 2013 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy	Thu Aug 08 12:01:02 2013 +0200
@@ -239,6 +239,17 @@
   qed (metis comp_apply sdrop.simps(1) sdrop_while.simps snth.simps(1))
 qed
 
+definition "sfilter P = stream_unfold (shd o sdrop_while (Not o P)) (stl o sdrop_while (Not o P))"
+
+lemma sfilter_Stream: "sfilter P (x ## s) = (if P x then x ## sfilter P s else sfilter P s)"
+proof (cases "P x")
+  case True thus ?thesis unfolding sfilter_def
+    by (subst stream.unfold) (simp add: sdrop_while_Stream)
+next
+  case False thus ?thesis unfolding sfilter_def
+    by (subst (1 2) stream.unfold) (simp add: sdrop_while_Stream)
+qed
+
 
 subsection {* unary predicates lifted to streams *}