src/HOL/Corec_Examples/Stream_Processor.thy
changeset 62694 f50d7efc8fe3
child 62698 9d706e37ddab
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Corec_Examples/Stream_Processor.thy	Tue Mar 22 12:39:37 2016 +0100
     1.3 @@ -0,0 +1,77 @@
     1.4 +(*  Title:      HOL/Corec_Examples/Stream_Processor.thy
     1.5 +    Author:     Andreas Lochbihler, ETH Zuerich
     1.6 +    Author:     Dmitriy Traytel, ETH Zuerich
     1.7 +    Author:     Andrei Popescu, TU Muenchen
     1.8 +    Copyright   2014, 2016
     1.9 +
    1.10 +Stream processors---a syntactic representation of continuous functions on streams.
    1.11 +*)
    1.12 +
    1.13 +section {* Stream Processors---A Syntactic Representation of Continuous Functions on Streams *}
    1.14 +
    1.15 +theory Stream_Processor
    1.16 +imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/Stream"
    1.17 +begin
    1.18 +
    1.19 +datatype (discs_sels) ('a, 'b, 'c) sp\<^sub>\<mu> =
    1.20 +  Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>"
    1.21 +| Put "'b" "'c"
    1.22 +
    1.23 +codatatype ('a, 'b) sp\<^sub>\<nu> =
    1.24 +  In (out: "('a, 'b, ('a, 'b) sp\<^sub>\<nu>) sp\<^sub>\<mu>")
    1.25 +
    1.26 +definition "sub \<equiv> {(f a, Get f) | a f. True}"
    1.27 +
    1.28 +lemma subI[intro]: "(f a, Get f) \<in> sub"
    1.29 +  unfolding sub_def by blast
    1.30 +
    1.31 +lemma wf_sub[simp, intro]: "wf sub"
    1.32 +proof (rule wfUNIVI)
    1.33 +  fix P  :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> bool" and x
    1.34 +  assume "\<forall>x. (\<forall>y. (y, x) \<in> sub \<longrightarrow> P y) \<longrightarrow> P x"
    1.35 +  hence I: "\<And>x. (\<forall>y. (\<exists>a f. y = f a \<and> x = Get f) \<longrightarrow> P y) \<Longrightarrow> P x" unfolding sub_def by blast
    1.36 +  show "P x" by (induct x) (auto intro: I)
    1.37 +qed
    1.38 +
    1.39 +definition get where
    1.40 +  "get f = In (Get (\<lambda>a. out (f a)))"
    1.41 +
    1.42 +corecursive run :: "('a, 'b) sp\<^sub>\<nu> \<Rightarrow> 'a stream \<Rightarrow> 'b stream" where
    1.43 +  "run sp s = (case out sp of
    1.44 +     Get f \<Rightarrow> run (In (f (shd s))) (stl s)
    1.45 +   | Put b sp \<Rightarrow> b ## run sp s)"
    1.46 +  by (relation "map_prod In In ` sub <*lex*> {}")
    1.47 +    (auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image)
    1.48 +
    1.49 +corec copy where
    1.50 +  "copy = In (Get (\<lambda>a. Put a copy))"
    1.51 +
    1.52 +friend_of_corec get where
    1.53 +  "get f = In (Get (\<lambda>a. out (f a)))"
    1.54 +  by (auto simp: rel_fun_def get_def sp\<^sub>\<mu>.rel_map rel_prod.simps, metis sndI)
    1.55 +
    1.56 +lemma run_simps [simp]:
    1.57 +  "run (In (Get f)) s = run (In (f (shd s))) (stl s)"
    1.58 +  "run (In (Put b sp)) s = b ## run sp s"
    1.59 +by(subst run.code; simp; fail)+
    1.60 +
    1.61 +lemma copy_sel[simp]: "out copy = Get (\<lambda>a. Put a copy)"
    1.62 +  by (subst copy.code; simp)
    1.63 +
    1.64 +corecursive sp_comp (infixl "oo" 65) where
    1.65 +  "sp oo sp' = (case (out sp, out sp') of
    1.66 +      (Put b sp, _) \<Rightarrow> In (Put b (sp oo sp'))
    1.67 +    | (Get f, Put b sp) \<Rightarrow> In (f b) oo sp
    1.68 +    | (_, Get g) \<Rightarrow> get (\<lambda>a. (sp oo In (g a))))"
    1.69 +  by (relation "map_prod In In ` sub <*lex*> map_prod In In ` sub")
    1.70 +    (auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image)
    1.71 +
    1.72 +lemma run_copy_unique: 
    1.73 +    "(\<And>s. h s = shd s ## h (stl s)) \<Longrightarrow> h = run copy"
    1.74 +apply corec_unique
    1.75 +apply(rule ext)
    1.76 +apply(subst copy.code)
    1.77 +apply simp
    1.78 +done
    1.79 +
    1.80 +end