extended stream library a little more
authortraytel
Tue, 05 Mar 2013 17:18:02 +0100
changeset 51353 ae707530c359
parent 51352 fdecc2cd5649
child 51356 877edf1fc5dd
extended stream library a little more
src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Tue Mar 05 17:10:49 2013 +0100
+++ b/src/HOL/BNF/Examples/Stream.thy	Tue Mar 05 17:18:02 2013 +0100
@@ -52,6 +52,9 @@
   "shift [] s = s"
 | "shift (x # xs) s = x ## shift xs s"
 
+lemma stream_map_shift[simp]: "stream_map f (xs @- s) = map f xs @- stream_map f s"
+  by (induct xs) auto
+
 lemma shift_append[simp]: "(xs @ ys) @- s = xs @- ys @- s"
   by (induct xs) auto