src/HOL/BNF_Examples/Stream_Processor.thy
author blanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 55076 1e73e090a514
parent 55075 b3d0a02a756d
child 55091 c43394c2e5ec
permissions -rw-r--r--
compile
     1 (*  Title:      HOL/BNF_Examples/Stream_Processor.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Andrei Popescu, TU Muenchen
     4     Copyright   2014
     5 
     6 Stream processors---a syntactic representation of continuous functions on streams
     7 *)
     8 
     9 header {* Stream Processors *}
    10 
    11 theory Stream_Processor
    12 imports Stream "~~/src/HOL/Library/BNF_Decl"
    13 begin
    14 
    15 section {* Continuous Functions on Streams *}
    16 
    17 datatype_new ('a, 'b, 'c) sp\<^sub>\<mu> = Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>" | Put "'b" "'c"
    18 codatatype ('a, 'b) sp\<^sub>\<nu> = In (out: "('a, 'b, ('a, 'b) sp\<^sub>\<nu>) sp\<^sub>\<mu>")
    19 
    20 primrec_new run\<^sub>\<mu> :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> 'a stream \<Rightarrow> ('b \<times> 'c) \<times> 'a stream" where
    21   "run\<^sub>\<mu> (Get f) s = run\<^sub>\<mu> (f (shd s)) (stl s)"
    22 | "run\<^sub>\<mu> (Put b sp) s = ((b, sp), s)"
    23 
    24 primcorec run\<^sub>\<nu> :: "('a, 'b) sp\<^sub>\<nu> \<Rightarrow> 'a stream \<Rightarrow> 'b stream" where
    25   "run\<^sub>\<nu> sp s = (let ((h, sp), s) = run\<^sub>\<mu> (out sp) s in h ## run\<^sub>\<nu> sp s)"
    26 
    27 primcorec copy :: "('a, 'a) sp\<^sub>\<nu>" where
    28   "copy = In (Get (\<lambda>a. Put a copy))"
    29 
    30 lemma run\<^sub>\<nu>_copy: "run\<^sub>\<nu> copy s = s"
    31   by (coinduction arbitrary: s) simp
    32 
    33 text {*
    34 To use the function package for the definition of composition the
    35 wellfoundedness of the subtree relation needs to be proved first.
    36 *}
    37 
    38 definition "sub \<equiv> {(f a, Get f) | a f. True}"
    39 
    40 lemma subI[intro]: "(f a, Get f) \<in> sub"
    41   unfolding sub_def by blast
    42 
    43 lemma wf_sub[simp, intro]: "wf sub"
    44 proof (rule wfUNIVI)
    45   fix P  :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> bool" and x
    46   assume "\<forall>x. (\<forall>y. (y, x) \<in> sub \<longrightarrow> P y) \<longrightarrow> P x"
    47   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
    48   show "P x" by (induct x) (auto intro: I)
    49 qed
    50 
    51 function
    52   sp\<^sub>\<mu>_comp :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> ('d, 'a, ('d, 'a) sp\<^sub>\<nu>) sp\<^sub>\<mu> \<Rightarrow> ('d, 'b, 'c \<times> ('d, 'a) sp\<^sub>\<nu>) sp\<^sub>\<mu>"
    53   (infixl "o\<^sub>\<mu>" 65)
    54 where
    55   "Put b sp o\<^sub>\<mu> fsp = Put b (sp, In fsp)"
    56 | "Get f o\<^sub>\<mu> Put b sp = f b o\<^sub>\<mu> out sp"
    57 | "Get f o\<^sub>\<mu> Get g = Get (\<lambda>a. Get f o\<^sub>\<mu> g a)"
    58 by pat_completeness auto
    59 termination by (relation "lex_prod sub sub") auto
    60 
    61 primcorec sp\<^sub>\<nu>_comp (infixl "o\<^sub>\<nu>" 65) where
    62   "out (sp o\<^sub>\<nu> sp') = map_sp\<^sub>\<mu> id (\<lambda>(sp, sp'). sp o\<^sub>\<nu> sp') (out sp o\<^sub>\<mu> out sp')"
    63 
    64 lemma run\<^sub>\<nu>_sp\<^sub>\<nu>_comp: "run\<^sub>\<nu> (sp o\<^sub>\<nu> sp') = run\<^sub>\<nu> sp o run\<^sub>\<nu> sp'"
    65 proof (rule ext, unfold comp_apply)
    66   fix s
    67   show "run\<^sub>\<nu> (sp o\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)"
    68   proof (coinduction arbitrary: sp sp' s)
    69     case Eq_stream
    70     show ?case
    71     proof (induct "out sp" "out sp'" arbitrary: sp sp' s rule: sp\<^sub>\<mu>_comp.induct)
    72       case (1 b sp'')
    73       show ?case by (auto simp add: 1[symmetric])
    74     next
    75       case (2 f b sp'')
    76       from 2(1)[of "In (f b)" sp''] show ?case by (simp add: 2(2,3)[symmetric])
    77     next
    78       case (3 f h)
    79       from 3(1)[of _ "shd s" "In (h (shd s))", OF 3(2)] show ?case by (simp add: 3(2,3)[symmetric])
    80     qed
    81   qed
    82 qed
    83 
    84 text {* Alternative definition of composition using primrec_new instead of function *}
    85 
    86 primrec_new sp\<^sub>\<mu>_comp2R  where
    87   "sp\<^sub>\<mu>_comp2R f (Put b sp) = f b (out sp)"
    88 | "sp\<^sub>\<mu>_comp2R f (Get h) = Get (sp\<^sub>\<mu>_comp2R f o h)"
    89 
    90 primrec_new sp\<^sub>\<mu>_comp2 (infixl "o\<^sup>*\<^sub>\<mu>" 65) where
    91   "Put b sp o\<^sup>*\<^sub>\<mu> fsp = Put b (sp, In fsp)"
    92 | "Get f o\<^sup>*\<^sub>\<mu> fsp = sp\<^sub>\<mu>_comp2R (op o\<^sup>*\<^sub>\<mu> o f) fsp"
    93 
    94 primcorec sp\<^sub>\<nu>_comp2 (infixl "o\<^sup>*\<^sub>\<nu>" 65) where
    95   "out (sp o\<^sup>*\<^sub>\<nu> sp') = map_sp\<^sub>\<mu> id (\<lambda>(sp, sp'). sp o\<^sup>*\<^sub>\<nu> sp') (out sp o\<^sup>*\<^sub>\<mu> out sp')"
    96 
    97 lemma run\<^sub>\<nu>_sp\<^sub>\<nu>_comp2: "run\<^sub>\<nu> (sp o\<^sup>*\<^sub>\<nu> sp') = run\<^sub>\<nu> sp o run\<^sub>\<nu> sp'"
    98 proof (rule ext, unfold comp_apply)
    99   fix s
   100   show "run\<^sub>\<nu> (sp o\<^sup>*\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)"
   101   proof (coinduction arbitrary: sp sp' s)
   102     case Eq_stream
   103     show ?case
   104     proof (induct "out sp" arbitrary: sp sp' s)
   105       case (Put b sp'')
   106       show ?case by (auto simp add: Put[symmetric])
   107     next
   108       case (Get f)
   109       then show ?case
   110       proof (induct "out sp'" arbitrary: sp sp' s)
   111         case (Put b sp'')
   112         from Put(2)[of "In (f b)" sp''] show ?case by (simp add: Put(1,3)[symmetric])
   113       next
   114         case (Get h)
   115         from Get(1)[OF _ Get(3,4), of "In (h (shd s))"] show ?case by (simp add: Get(2,4)[symmetric])
   116       qed
   117     qed
   118   qed
   119 qed
   120 
   121 text {* The two definitions are equivalent *}
   122 
   123 lemma sp\<^sub>\<mu>_comp_sp\<^sub>\<mu>_comp2[simp]: "sp o\<^sub>\<mu> sp' = sp o\<^sup>*\<^sub>\<mu> sp'"
   124   by (induct sp sp' rule: sp\<^sub>\<mu>_comp.induct) auto
   125 
   126 (*will be provided by the package*)
   127 lemma sp\<^sub>\<mu>_rel_map_map[unfolded vimage2p_def, simp]:
   128   "rel_sp\<^sub>\<mu> R1 R2 (map_sp\<^sub>\<mu> f1 f2 sp) (map_sp\<^sub>\<mu> g1 g2 sp') =
   129   rel_sp\<^sub>\<mu> (BNF_Def.vimage2p f1 g1 R1) (BNF_Def.vimage2p f2 g2 R2) sp sp'"
   130 by (tactic {*
   131   let val ks = 1 upto 2;
   132   in
   133     BNF_Tactics.unfold_thms_tac @{context}
   134       @{thms sp\<^sub>\<mu>.rel_compp sp\<^sub>\<mu>.rel_conversep sp\<^sub>\<mu>.rel_Grp vimage2p_Grp} THEN
   135     HEADGOAL (EVERY' [rtac iffI, rtac @{thm relcomppI}, rtac @{thm GrpI}, rtac refl, rtac CollectI,
   136       BNF_Util.CONJ_WRAP' (K (rtac @{thm subset_UNIV})) ks, rtac @{thm relcomppI}, atac,
   137       rtac @{thm conversepI}, rtac @{thm GrpI}, rtac refl, rtac CollectI,
   138       BNF_Util.CONJ_WRAP' (K (rtac @{thm subset_UNIV})) ks,
   139       REPEAT_DETERM o eresolve_tac @{thms relcomppE conversepE GrpE},
   140       hyp_subst_tac @{context}, atac])
   141   end
   142 *})
   143 
   144 lemma sp\<^sub>\<mu>_rel_self: "\<lbrakk>op = \<le> R1; op = \<le> R2\<rbrakk> \<Longrightarrow> rel_sp\<^sub>\<mu> R1 R2 x x"
   145   by (erule (1) predicate2D[OF sp\<^sub>\<mu>.rel_mono]) (simp only: sp\<^sub>\<mu>.rel_eq)
   146 
   147 lemma sp\<^sub>\<nu>_comp_sp\<^sub>\<nu>_comp2: "sp o\<^sub>\<nu> sp' = sp o\<^sup>*\<^sub>\<nu> sp'"
   148   by (coinduction arbitrary: sp sp') (auto intro!: sp\<^sub>\<mu>_rel_self)
   149 
   150 
   151 section {* Generalization to an Arbitrary BNF as Codomain *}
   152 
   153 bnf_decl ('a, 'b) F (map: F)
   154 
   155 definition \<theta> :: "('p,'a) F * 'b \<Rightarrow> ('p,'a * 'b) F" where
   156    "\<theta> xb = F id <id, \<lambda> a. (snd xb)> (fst xb)"
   157 
   158 (* The strength laws for \<theta>: *)
   159 lemma \<theta>_natural: "F id (map_pair f g) o \<theta> = \<theta> o map_pair (F id f) g"
   160   unfolding \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split_beta fst_conv snd_conv ..
   161 
   162 definition assl :: "'a * ('b * 'c) \<Rightarrow> ('a * 'b) * 'c" where
   163   "assl abc = ((fst abc, fst (snd abc)), snd (snd abc))"
   164 
   165 lemma \<theta>_rid: "F id fst o \<theta> = fst"
   166   unfolding \<theta>_def F.map_comp F.map_id comp_def id_apply convol_def fst_conv sym[OF id_def] ..
   167 
   168 lemma \<theta>_assl: "F id assl o \<theta> = \<theta> o map_pair \<theta> id o assl"
   169   unfolding assl_def \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split fst_conv snd_conv ..
   170 
   171 datatype_new ('a, 'b, 'c) spF\<^sub>\<mu> = GetF "'a \<Rightarrow> ('a, 'b, 'c) spF\<^sub>\<mu>" | PutF "('b,'c) F"
   172 codatatype ('a, 'b) spF\<^sub>\<nu> = InF (outF: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu>")
   173 
   174 codatatype 'b JF = Ctor (dtor: "('b, 'b JF) F")
   175 
   176 (* Definition of run for an arbitrary final coalgebra as codomain: *)
   177 
   178 primrec_new
   179   runF\<^sub>\<mu> :: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu> \<Rightarrow> 'a stream \<Rightarrow> (('b, ('a, 'b) spF\<^sub>\<nu>) F) \<times> 'a stream" 
   180 where
   181   "runF\<^sub>\<mu> (GetF f) s = (runF\<^sub>\<mu> o f) (shd s) (stl s)"
   182 | "runF\<^sub>\<mu> (PutF x) s = (x, s)"
   183 
   184 primcorec runF\<^sub>\<nu> :: "('a, 'b) spF\<^sub>\<nu> \<Rightarrow> 'a stream \<Rightarrow> 'b JF" where
   185   "runF\<^sub>\<nu> sp s = (let (x, s) = runF\<^sub>\<mu> (outF sp) s in Ctor (F id (\<lambda> sp. runF\<^sub>\<nu> sp s) x))"
   186 
   187 end