src/HOL/Corec_Examples/Stream_Processor.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 62726 5b2a7caa855b
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/Corec_Examples/Stream_Processor.thy
     2     Author:     Andreas Lochbihler, ETH Zuerich
     3     Author:     Dmitriy Traytel, ETH Zuerich
     4     Author:     Andrei Popescu, TU Muenchen
     5     Copyright   2014, 2016
     6 
     7 Stream processors---a syntactic representation of continuous functions on streams.
     8 *)
     9 
    10 section \<open>Stream Processors---A Syntactic Representation of Continuous Functions on Streams\<close>
    11 
    12 theory Stream_Processor
    13 imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/Stream"
    14 begin
    15 
    16 datatype (discs_sels) ('a, 'b, 'c) sp\<^sub>\<mu> =
    17   Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>"
    18 | Put "'b" "'c"
    19 
    20 codatatype ('a, 'b) sp\<^sub>\<nu> =
    21   In (out: "('a, 'b, ('a, 'b) sp\<^sub>\<nu>) sp\<^sub>\<mu>")
    22 
    23 definition "sub \<equiv> {(f a, Get f) | a f. True}"
    24 
    25 lemma subI[intro]: "(f a, Get f) \<in> sub"
    26   unfolding sub_def by blast
    27 
    28 lemma wf_sub[simp, intro]: "wf sub"
    29 proof (rule wfUNIVI)
    30   fix P  :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> bool" and x
    31   assume "\<forall>x. (\<forall>y. (y, x) \<in> sub \<longrightarrow> P y) \<longrightarrow> P x"
    32   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
    33   show "P x" by (induct x) (auto intro: I)
    34 qed
    35 
    36 definition get where
    37   "get f = In (Get (\<lambda>a. out (f a)))"
    38 
    39 corecursive run :: "('a, 'b) sp\<^sub>\<nu> \<Rightarrow> 'a stream \<Rightarrow> 'b stream" where
    40   "run sp s = (case out sp of
    41      Get f \<Rightarrow> run (In (f (shd s))) (stl s)
    42    | Put b sp \<Rightarrow> b ## run sp s)"
    43   by (relation "map_prod In In ` sub <*lex*> {}")
    44     (auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image)
    45 
    46 corec copy where
    47   "copy = In (Get (\<lambda>a. Put a copy))"
    48 
    49 friend_of_corec get where
    50   "get f = In (Get (\<lambda>a. out (f a)))"
    51   by (auto simp: rel_fun_def get_def sp\<^sub>\<mu>.rel_map rel_prod.simps, metis sndI)
    52 
    53 lemma run_simps [simp]:
    54   "run (In (Get f)) s = run (In (f (shd s))) (stl s)"
    55   "run (In (Put b sp)) s = b ## run sp s"
    56 by(subst run.code; simp; fail)+
    57 
    58 lemma copy_sel[simp]: "out copy = Get (\<lambda>a. Put a copy)"
    59   by (subst copy.code; simp)
    60 
    61 corecursive sp_comp (infixl "oo" 65) where
    62   "sp oo sp' = (case (out sp, out sp') of
    63       (Put b sp, _) \<Rightarrow> In (Put b (sp oo sp'))
    64     | (Get f, Put b sp) \<Rightarrow> In (f b) oo sp
    65     | (_, Get g) \<Rightarrow> get (\<lambda>a. (sp oo In (g a))))"
    66   by (relation "map_prod In In ` sub <*lex*> map_prod In In ` sub")
    67     (auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image)
    68 
    69 lemma run_copy_unique:
    70     "(\<And>s. h s = shd s ## h (stl s)) \<Longrightarrow> h = run copy"
    71 apply corec_unique
    72 apply(rule ext)
    73 apply(subst copy.code)
    74 apply simp
    75 done
    76 
    77 end