src/HOL/Datatype_Examples/Stream_Processor.thy
changeset 62694 f50d7efc8fe3
parent 61260 e6f03fae14d5
child 63167 0909deb8059b
     1.1 --- a/src/HOL/Datatype_Examples/Stream_Processor.thy	Tue Mar 22 12:39:37 2016 +0100
     1.2 +++ b/src/HOL/Datatype_Examples/Stream_Processor.thy	Tue Mar 22 12:39:37 2016 +0100
     1.3 @@ -17,8 +17,12 @@
     1.4  
     1.5  section {* Continuous Functions on Streams *}
     1.6  
     1.7 -datatype ('a, 'b, 'c) sp\<^sub>\<mu> = Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>" | Put "'b" "'c"
     1.8 -codatatype ('a, 'b) sp\<^sub>\<nu> = In (out: "('a, 'b, ('a, 'b) sp\<^sub>\<nu>) sp\<^sub>\<mu>")
     1.9 +datatype ('a, 'b, 'c) sp\<^sub>\<mu> =
    1.10 +  Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>"
    1.11 +| Put "'b" "'c"
    1.12 +
    1.13 +codatatype ('a, 'b) sp\<^sub>\<nu> =
    1.14 +  In (out: "('a, 'b, ('a, 'b) sp\<^sub>\<nu>) sp\<^sub>\<mu>")
    1.15  
    1.16  primrec run\<^sub>\<mu> :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> 'a stream \<Rightarrow> ('b \<times> 'c) \<times> 'a stream" where
    1.17    "run\<^sub>\<mu> (Get f) s = run\<^sub>\<mu> (f (shd s)) (stl s)"