Theory Prisms

section ‹Prisms›

theory Prisms
  imports Lenses
begin

subsection ‹ Signature and Axioms ›

text ‹Prisms are like lenses, but they act on sum types rather than product types~cite"Gibbons17".
  See \url{https://hackage.haskell.org/package/lens-4.15.2/docs/Control-Lens-Prism.html}
  for more information.›

record ('v, 's) prism =
  prism_match :: "'s  'v option" ("matchı")
  prism_build :: "'v  's" ("buildı")

type_notation
  prism (infixr "" 0)

locale wb_prism =
  fixes x :: "'v  's" (structure)
  assumes match_build: "match (build v) = Some v"
  and build_match: "match s = Some v  s = build v"
begin

  lemma build_match_iff: "match s = Some v  s = build v"
    using build_match match_build by blast

  lemma range_build: "range build = dom match"
    using build_match match_build by fastforce

  lemma inj_build: "inj build"
    by (metis injI match_build option.inject)

end

declare wb_prism.match_build [simp]
declare wb_prism.build_match [simp]

subsection ‹ Co-dependence ›

text ‹ The relation states that two prisms construct disjoint elements of the source. This
  can occur, for example, when the two prisms characterise different constructors of an
  algebraic datatype. ›

definition prism_diff :: "('a  's)  ('b  's)  bool" (infix "" 50) where
[lens_defs]: "prism_diff X Y = (range buildX range buildY= {})"

lemma prism_diff_intro:
  "( s1 s2. buildXs1 = buildYs2  False)  X  Y"
  by (auto simp add: prism_diff_def)

lemma prism_diff_irrefl: "¬ X  X"
  by (simp add: prism_diff_def)

lemma prism_diff_sym: "X  Y  Y  X"
  by (auto simp add: prism_diff_def)

lemma prism_diff_build: "X  Y  buildXu  buildYv"
  by (simp add: disjoint_iff_not_equal prism_diff_def)

lemma prism_diff_build_match: " wb_prism X; X  Y   matchX(buildYv) = None" 
  using UNIV_I wb_prism.range_build by (fastforce simp add: prism_diff_def)

subsection ‹ Canonical prisms ›

definition prism_id :: "('a  'a)" ("1") where
[lens_defs]: "prism_id =  prism_match = Some, prism_build = id "

lemma wb_prism_id: "wb_prism 1"
  unfolding prism_id_def wb_prism_def by simp

lemma prism_id_never_diff: "¬ 1  X"
  by (simp add: prism_diff_def prism_id_def)

subsection ‹ Summation ›

definition prism_plus :: "('a  's)  ('b  's)  'a + 'b  's" (infixl "+" 85) 
  where
[lens_defs]: "X + Y =  prism_match = (λ s. case (matchXs, matchYs) of
                                 (Some u, _)  Some (Inl u) |
                                 (None, Some v)  Some (Inr v) |
                                 (None, None)  None),
           prism_build = (λ v. case v of Inl x  buildXx | Inr y  buildYy) "

lemma prism_plus_wb [simp]: " wb_prism X; wb_prism Y; X  Y   wb_prism (X + Y)"
  apply (unfold_locales)
   apply (auto simp add: prism_plus_def sum.case_eq_if option.case_eq_if prism_diff_build_match)
  apply (metis map_option_case map_option_eq_Some option.exhaust option.sel sum.disc(2) sum.sel(1) wb_prism.build_match_iff)
  apply (metis (no_types, lifting) isl_def not_None_eq option.case_eq_if option.sel sum.sel(2) wb_prism.build_match)
  done

lemma build_plus_Inl [simp]: "buildc + d(Inl x) = buildcx"
  by (simp add: prism_plus_def)

lemma build_plus_Inr [simp]: "buildc + d(Inr y) = builddy"
  by (simp add: prism_plus_def)

lemma prism_diff_preserved_1 [simp]: " X  Y; X  Z   X  Y + Z"
  by (auto simp add: lens_defs sum.case_eq_if)

lemma prism_diff_preserved_2 [simp]: " X  Z; Y  Z   X + Y  Z"
  by (meson prism_diff_preserved_1 prism_diff_sym)

text ‹ The following two lemmas are useful for reasoning about prism sums ›

lemma Bex_Sum_iff: "(xA<+>B. P x)  ( xA. P (Inl x))  ( yB. P (Inr y))"
  by (auto)

lemma Ball_Sum_iff: "(xA<+>B. P x)  ( xA. P (Inl x))  ( yB. P (Inr y))"
  by (auto)

subsection ‹ Instances ›

definition prism_suml :: "('a, 'a + 'b) prism" ("Inl") where
[lens_defs]: "prism_suml =  prism_match = (λ v. case v of Inl x  Some x | _  None), prism_build = Inl "

definition prism_sumr :: "('b, 'a + 'b) prism" ("Inr") where
[lens_defs]: "prism_sumr =  prism_match = (λ v. case v of Inr x  Some x | _  None), prism_build = Inr "

lemma wb_prim_suml [simp]: "wb_prism Inl"
  apply (unfold_locales)
   apply (simp_all add: prism_suml_def sum.case_eq_if)
  apply (metis option.inject option.simps(3) sum.collapse(1))
  done

lemma wb_prim_sumr [simp]: "wb_prism Inr"
  apply (unfold_locales)
   apply (simp_all add: prism_sumr_def sum.case_eq_if)
  apply (metis option.distinct(1) option.inject sum.collapse(2))
  done

lemma prism_suml_indep_sumr [simp]: "Inl  Inr"
  by (auto simp add: lens_defs)

lemma prism_sum_plus: "Inl + Inr = 1"
  unfolding lens_defs prism_plus_def by (auto simp add: Inr_Inl_False sum.case_eq_if)

subsection ‹ Lens correspondence ›

text ‹ Every well-behaved prism can be represented by a partial bijective lens. We prove 
  this by exhibiting conversion functions and showing they are (almost) inverses. ›

definition prism_lens :: "('a, 's) prism  ('a  's)" where
"prism_lens X =  lens_get = (λ s. the (matchXs)), lens_put = (λ s v. buildXv) "

definition lens_prism :: "('a  's)  ('a, 's) prism" where
"lens_prism X =  prism_match = (λ s. if (s  𝒮X) then Some (getXs) else None)
                , prism_build = createX"

lemma mwb_prism_lens: "wb_prism a  mwb_lens (prism_lens a)"
  by (simp add: mwb_lens_axioms_def mwb_lens_def weak_lens_def prism_lens_def)

lemma get_prism_lens: "getprism_lens X= the  matchX⇙"
  by (simp add: prism_lens_def fun_eq_iff)

lemma src_prism_lens: "𝒮prism_lens X= range (buildX)"
  by (auto simp add: prism_lens_def lens_source_def)

lemma create_prism_lens: "createprism_lens X= buildX⇙"
  by (simp add: prism_lens_def lens_create_def fun_eq_iff)

lemma prism_lens_inverse:
  "wb_prism X  lens_prism (prism_lens X) = X"
  unfolding lens_prism_def src_prism_lens create_prism_lens get_prism_lens
  by (auto intro: prism.equality simp add: fun_eq_iff domIff wb_prism.range_build)

text ‹ Function @{const lens_prism} is almost inverted by @{const prism_lens}. The $put$
  functions are identical, but the $get$ functions differ when applied to a source where
  the prism @{term X} is undefined. ›

lemma lens_prism_put_inverse:
  "pbij_lens X  putprism_lens (lens_prism X)= putX⇙"
  unfolding prism_lens_def lens_prism_def
  by (auto simp add: fun_eq_iff pbij_lens.put_is_create)

lemma wb_prism_implies_pbij_lens:
  "wb_prism X  pbij_lens (prism_lens X)"
  by (unfold_locales, simp_all add: prism_lens_def)

lemma pbij_lens_implies_wb_prism:
  assumes "pbij_lens X" 
  shows "wb_prism (lens_prism X)"
proof (unfold_locales)
  fix s v
  show "matchlens_prism X(buildlens_prism Xv) = Some v"
    by (simp add: lens_prism_def weak_lens.create_closure assms)
  assume a: "matchlens_prism Xs = Some v"
  show "s = buildlens_prism Xv"
  proof (cases "s  𝒮X⇙")
    case True
    with a assms show ?thesis 
      by (simp add: lens_prism_def lens_create_def, 
          metis mwb_lens.weak_get_put pbij_lens.put_det pbij_lens_mwb)
  next
    case False
    with a assms show ?thesis by (simp add: lens_prism_def)
  qed
qed

ML_file ‹Prism_Lib.ML›

end