Theory Channel_Type

section ‹ Channel Types ›

theory Channel_Type
  imports Prisms
  keywords "chantype" :: "thy_defn"
begin

text ‹ A channel type is a simplified algebraic datatype where each constructor has exactly 
  one parameter, and it is wrapped up as a prism. It a dual of an alphabet type. ›

definition ctor_prism :: "('a ⇒ 'd) ⇒ ('d ⇒ bool) ⇒ ('d ⇒ 'a) ⇒ ('a ⟹⇩△ 'd)" where
[lens_defs]: 
"ctor_prism ctor disc sel = ⦇ prism_match = (λ d. if (disc d) then Some (sel d) else None)
                            , prism_build = ctor ⦈"

lemma wb_ctor_prism_intro:
  assumes 
    "⋀ v. disc (ctor v)" 
    "⋀ v. sel (ctor v) = v"
    "⋀ s. disc s ⟹ ctor (sel s) = s"
  shows "wb_prism (ctor_prism ctor disc sel)"
  by (unfold_locales, simp_all add: lens_defs assms)
     (metis assms(3) option.distinct(1) option.sel)

lemma ctor_codep_intro:
  assumes "⋀ x y. ctor1 x ≠ ctor2 y"
  shows "ctor_prism ctor1 disc1 sel1 ∇ ctor_prism ctor2 disc2 sel2"
  by (rule prism_diff_intro, simp add: lens_defs assms)

ML_file "Channel_Type.ML"

end