1.1 --- a/thys/WorkerWrapper/Streams.thy Sun Nov 01 16:17:44 2009 +0100
1.2 +++ b/thys/WorkerWrapper/Streams.thy Mon Nov 02 18:43:26 2009 +0100
1.3 @@ -219,7 +219,8 @@
1.4 proof -
1.5 let ?wb = "\<Lambda> r. Nat_case\<cdot>1\<cdot>(Nat_case\<cdot>1\<cdot>(\<Lambda> n'. r !! n' + r !! (n' + 1)))"
1.6 let ?mr = "\<Lambda> \<langle>fwf :: Nat Stream, fff\<rangle>. \<langle>smap\<cdot>fff\<cdot>nats, ?wb\<cdot>fwf\<rangle>"
1.7 - have "?lhs = cfst\<cdot>(fix\<cdot>?mr)" by (simp add: fib_work_final_def)
1.8 + have "?lhs = cfst\<cdot>(fix\<cdot>?mr)"
1.9 + by (simp add: fib_work_final_def split_def csplit_def cfst_def csnd_def cpair_def)
1.10 also have "\<dots> = (\<mu> fwf. cfst\<cdot>(?mr\<cdot>\<langle>fwf, \<mu> fff. csnd\<cdot>(?mr\<cdot>\<langle>fwf, fff\<rangle>)\<rangle>))"
1.11 using fix_cprod[where F="?mr"] by simp
1.12 also have "\<dots> = (\<mu> fwf. smap\<cdot>(\<mu> fff. ?wb\<cdot>fwf)\<cdot>nats)" by simp