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