section ‹ Examples using Prisms ›

theory Prisms_Examples
  imports Prisms
begin

text ‹ We demonstrate prisms for manipulating an algebraic data type with three constructors . ›

datatype D = A int | B string | C bool

fun fromA :: "D → int option" where "fromA (A x) = Some x" | "fromA _ = None"
fun fromB :: "D → string option" where "fromB (B x) = Some x" | "fromB _ = None"
fun fromC :: "D → bool option" where "fromC (C x) = Some x" | "fromC _ = None"

text ‹ We create a prism for each of the three constructors. ›

definition A_{_}prism :: "int ==>_\<triangle> D" ("A_\<triangle>") where
[lens_defs]: "A_\<triangle> = ( prism_match = fromA, prism_build = A )"

definition B_prism :: "string ==>_\<triangle> D" ("B_\<triangle>") where
[lens_defs]: "B_\<triangle> = ( prism_match = fromB, prism_build = B )"

definition C_prism :: "bool ==>_\<triangle> D" ("C_\<triangle>") where
[lens_defs]: "C_\<triangle> = ( prism_match = fromC, prism_build = C )"

text ‹ All three are well-behaved. ›

lemma A_wb_prism [simp]: "wb_prism A_\<triangle>"
  using fromA.elims by (unfold_locales, auto simp add: lens_defs)

lemma B_wb_prism [simp]: "wb_prism B_\<triangle>"
  using fromB.elims by (unfold_locales, auto simp add: lens_defs)

lemma C_wb_prism [simp]: "wb_prism C_\<triangle>"
  using fromC.elims by (unfold_locales, auto simp add: lens_defs)

text ‹ All three prisms are codependent with each other. ›

lemma D_codeps: "A_\<triangle> ∇ B_\<triangle>" "A_\<triangle> ∇ C_\<triangle>" "B_\<triangle> ∇ C_\<triangle>"
  by (rule prism_diff_intro, simp add: lens_defs)+

end