Theory Stream_Processor

(*  Title:      HOL/Datatype_Examples/Stream_Processor.thy
    Author:     Dmitriy Traytel, TU Muenchen
    Author:     Andrei Popescu, TU Muenchen
    Copyright   2014

Stream processors---a syntactic representation of continuous functions on streams.
*)

section ‹Stream Processors---A Syntactic Representation of Continuous Functions on Streams›

theory Stream_Processor
imports "HOL-Library.Stream" "HOL-Library.BNF_Axiomatization"
begin

declare [[typedef_overloaded]]


section ‹Continuous Functions on Streams›

datatype ('a, 'b, 'c) sp⇩μ =
  Get "'a ⇒ ('a, 'b, 'c) sp⇩μ"
| Put "'b" "'c"

codatatype ('a, 'b) sp⇩ν =
  In (out: "('a, 'b, ('a, 'b) sp⇩ν) sp⇩μ")

primrec run⇩μ :: "('a, 'b, 'c) sp⇩μ ⇒ 'a stream ⇒ ('b × 'c) × 'a stream" where
  "run⇩μ (Get f) s = run⇩μ (f (shd s)) (stl s)"
| "run⇩μ (Put b sp) s = ((b, sp), s)"

primcorec run⇩ν :: "('a, 'b) sp⇩ν ⇒ 'a stream ⇒ 'b stream" where
  "run⇩ν sp s = (let ((h, sp), s) = run⇩μ (out sp) s in h ## run⇩ν sp s)"

primcorec copy :: "('a, 'a) sp⇩ν" where
  "copy = In (Get (λa. Put a copy))"

lemma run⇩ν_copy: "run⇩ν copy s = s"
  by (coinduction arbitrary: s) simp

text ‹
To use the function package for the definition of composition the
wellfoundedness of the subtree relation needs to be proved first.
›

definition "sub ≡ {(f a, Get f) | a f. True}"

lemma subI[intro]: "(f a, Get f) ∈ sub"
  unfolding sub_def by blast

lemma wf_sub[simp, intro]: "wf sub"
proof (rule wfUNIVI)
  fix P  :: "('a, 'b, 'c) sp⇩μ ⇒ bool" and x
  assume "∀x. (∀y. (y, x) ∈ sub ⟶ P y) ⟶ P x"
  hence I: "⋀x. (∀y. (∃a f. y = f a ∧ x = Get f) ⟶ P y) ⟹ P x" unfolding sub_def by blast
  show "P x" by (induct x) (auto intro: I)
qed

lemma neq_Get [simp]: "f b ≠ Get f"
  by (metis subI wf_asym wf_sub)


function
  sp⇩μ_comp :: "('a, 'b, 'c) sp⇩μ ⇒ ('d, 'a, ('d, 'a) sp⇩ν) sp⇩μ ⇒ ('d, 'b, 'c × ('d, 'a) sp⇩ν) sp⇩μ"
  (infixl "o⇩μ" 65)
where
  "Put b sp o⇩μ fsp = Put b (sp, In fsp)"
| "Get f o⇩μ Put b sp = f b o⇩μ out sp"
| "Get f o⇩μ Get g = Get (λa. Get f o⇩μ g a)"
by pat_completeness auto
termination
  by (relation "lex_prod sub sub") auto

primcorec sp⇩ν_comp (infixl "o⇩ν" 65) where
  "out (sp o⇩ν sp') = map_sp⇩μ id (λ(sp, sp'). sp o⇩ν sp') (out sp o⇩μ out sp')"

lemma run⇩ν_sp⇩ν_comp: "run⇩ν (sp o⇩ν sp') = run⇩ν sp o run⇩ν sp'"
proof (rule ext, unfold comp_apply)
  fix s
  show "run⇩ν (sp o⇩ν sp') s = run⇩ν sp (run⇩ν sp' s)"
  proof (coinduction arbitrary: sp sp' s)
    case Eq_stream
    show ?case
    proof (induct "out sp" "out sp'" arbitrary: sp sp' s rule: sp⇩μ_comp.induct)
      case (1 b sp'')
      show ?case by (auto simp add: 1[symmetric])
    next
      case (2 f b sp'')
      from 2(1)[of "In (f b)" sp''] show ?case by (simp add: 2(2,3)[symmetric])
    next
      case (3 f h)
      from 3(1)[of _ "shd s" "In (h (shd s))", OF 3(2)] show ?case by (simp add: 3(2,3)[symmetric])
    qed
  qed
qed

text ‹Alternative definition of composition using primrec instead of function›

primrec sp⇩μ_comp2R  where
  "sp⇩μ_comp2R f (Put b sp) = f b (out sp)"
| "sp⇩μ_comp2R f (Get h) = Get (sp⇩μ_comp2R f o h)"

primrec sp⇩μ_comp2 (infixl "o⇧*⇩μ" 65) where
  "Put b sp o⇧*⇩μ fsp = Put b (sp, In fsp)"
| "Get f o⇧*⇩μ fsp = sp⇩μ_comp2R ((o⇧*⇩μ) o f) fsp"

primcorec sp⇩ν_comp2 (infixl "o⇧*⇩ν" 65) where
  "out (sp o⇧*⇩ν sp') = map_sp⇩μ id (λ(sp, sp'). sp o⇧*⇩ν sp') (out sp o⇧*⇩μ out sp')"

lemma run⇩ν_sp⇩ν_comp2: "run⇩ν (sp o⇧*⇩ν sp') = run⇩ν sp o run⇩ν sp'"
proof (rule ext, unfold comp_apply)
  fix s
  show "run⇩ν (sp o⇧*⇩ν sp') s = run⇩ν sp (run⇩ν sp' s)"
  proof (coinduction arbitrary: sp sp' s)
    case Eq_stream
    show ?case
    proof (induct "out sp" arbitrary: sp sp' s)
      case (Put b sp'')
      show ?case by (auto simp add: Put[symmetric])
    next
      case (Get f)
      then show ?case
      proof (induct "out sp'" arbitrary: sp sp' s)
        case (Put b sp'')
        from Put(2)[of "In (f b)" sp''] show ?case by (simp add: Put(1,3)[symmetric])
      next
        case (Get h)
        from Get(1)[OF _ Get(3,4), of "In (h (shd s))"] show ?case by (simp add: Get(2,4)[symmetric])
      qed
    qed
  qed
qed

text ‹The two definitions are equivalent›

lemma sp⇩μ_comp_sp⇩μ_comp2[simp]: "sp o⇩μ sp' = sp o⇧*⇩μ sp'"
  by (induct sp sp' rule: sp⇩μ_comp.induct) auto

(*will be provided by the package*)
lemma sp⇩μ_rel_map_map[unfolded vimage2p_def, simp]:
  "rel_sp⇩μ R1 R2 (map_sp⇩μ f1 f2 sp) (map_sp⇩μ g1 g2 sp') =
  rel_sp⇩μ (BNF_Def.vimage2p f1 g1 R1) (BNF_Def.vimage2p f2 g2 R2) sp sp'"
by (tactic ‹
  let
    val ks = 1 upto 2;
    val ctxt = \<^context>;
  in
    BNF_Tactics.unfold_thms_tac ctxt
      @{thms sp⇩μ.rel_compp sp⇩μ.rel_conversep sp⇩μ.rel_Grp vimage2p_Grp} THEN
    HEADGOAL (EVERY' [resolve_tac ctxt [iffI],
      resolve_tac ctxt @{thms relcomppI},
      resolve_tac ctxt @{thms GrpI},
      resolve_tac ctxt [refl],
      resolve_tac ctxt [CollectI],
      BNF_Util.CONJ_WRAP' (K (resolve_tac ctxt @{thms subset_UNIV})) ks,
      resolve_tac ctxt @{thms relcomppI}, assume_tac ctxt,
      resolve_tac ctxt @{thms conversepI},
      resolve_tac ctxt @{thms GrpI},
      resolve_tac ctxt [refl],
      resolve_tac ctxt [CollectI],
      BNF_Util.CONJ_WRAP' (K (resolve_tac ctxt @{thms subset_UNIV})) ks,
      REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE},
      hyp_subst_tac ctxt,
      assume_tac ctxt])
  end
›)

lemma sp⇩μ_rel_self: "⟦(=) ≤ R1; (=) ≤ R2⟧ ⟹ rel_sp⇩μ R1 R2 x x"
  by (erule (1) predicate2D[OF sp⇩μ.rel_mono]) (simp only: sp⇩μ.rel_eq)

lemma sp⇩ν_comp_sp⇩ν_comp2: "sp o⇩ν sp' = sp o⇧*⇩ν sp'"
  by (coinduction arbitrary: sp sp') (auto intro!: sp⇩μ_rel_self)


section ‹Generalization to an Arbitrary BNF as Codomain›

bnf_axiomatization ('a, 'b) F for map: F

notation BNF_Def.convol ("⟨(_,/ _)⟩")

definition θ :: "('p,'a) F * 'b ⇒ ('p,'a * 'b) F" where
  "θ xb = F id ⟨id, λ a. (snd xb)⟩ (fst xb)"

(* The strength laws for θ: *)
lemma θ_natural: "F id (map_prod f g) o θ = θ o map_prod (F id f) g"
  unfolding θ_def F.map_comp comp_def id_apply convol_def map_prod_def split_beta fst_conv snd_conv ..

definition assl :: "'a * ('b * 'c) ⇒ ('a * 'b) * 'c" where
  "assl abc = ((fst abc, fst (snd abc)), snd (snd abc))"

lemma θ_rid: "F id fst o θ = fst"
  unfolding θ_def F.map_comp F.map_id comp_def id_apply convol_def fst_conv sym[OF id_def] ..

lemma θ_assl: "F id assl o θ = θ o map_prod θ id o assl"
  unfolding assl_def θ_def F.map_comp comp_def id_apply convol_def map_prod_def split fst_conv snd_conv ..

datatype ('a, 'b, 'c) spF⇩μ = GetF "'a ⇒ ('a, 'b, 'c) spF⇩μ" | PutF "('b,'c) F"
codatatype ('a, 'b) spF⇩ν = InF (outF: "('a, 'b, ('a, 'b) spF⇩ν) spF⇩μ")

codatatype 'b JF = Ctor (dtor: "('b, 'b JF) F")

(* Definition of run for an arbitrary final coalgebra as codomain: *)

primrec
  runF⇩μ :: "('a, 'b, ('a, 'b) spF⇩ν) spF⇩μ ⇒ 'a stream ⇒ (('b, ('a, 'b) spF⇩ν) F) × 'a stream" 
where
  "runF⇩μ (GetF f) s = (runF⇩μ o f) (shd s) (stl s)"
| "runF⇩μ (PutF x) s = (x, s)"

primcorec runF⇩ν :: "('a, 'b) spF⇩ν ⇒ 'a stream ⇒ 'b JF" where
  "runF⇩ν sp s = (let (x, s) = runF⇩μ (outF sp) s in Ctor (F id (λ sp. runF⇩ν sp s) x))"

end