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 build⇘X⇙ ∩ range build⇘Y⇙ = {})"

lemma prism_diff_intro:
  "(⋀ s⇩1 s⇩2. build⇘X⇙ s⇩1 = build⇘Y⇙ s⇩2 ⟹ 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 ⟹ build⇘X⇙ u ≠ build⇘Y⇙ v"
  by (simp add: disjoint_iff_not_equal prism_diff_def)

lemma prism_diff_build_match: "⟦ wb_prism X; X ∇ Y ⟧ ⟹ match⇘X⇙ (build⇘Y⇙ v) = 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 (match⇘X⇙ s, match⇘Y⇙ s) of
                                 (Some u, _) ⇒ Some (Inl u) |
                                 (None, Some v) ⇒ Some (Inr v) |
                                 (None, None) ⇒ None),
           prism_build = (λ v. case v of Inl x ⇒ build⇘X⇙ x | Inr y ⇒ build⇘Y⇙ y) ⦈"

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]: "build⇘c +⇩△ d⇙ (Inl x) = build⇘c⇙ x"
  by (simp add: prism_plus_def)

lemma build_plus_Inr [simp]: "build⇘c +⇩△ d⇙ (Inr y) = build⇘d⇙ y"
  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: "(∃x∈A<+>B. P x) ⟷ (∃ x∈A. P (Inl x)) ∨ (∃ y∈B. P (Inr y))"
  by (auto)

lemma Ball_Sum_iff: "(∀x∈A<+>B. P x) ⟷ (∀ x∈A. P (Inl x)) ∧ (∀ y∈B. 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 (match⇘X⇙ s)), lens_put = (λ s v. build⇘X⇙ v) ⦈"

definition lens_prism :: "('a ⟹ 's) ⇒ ('a, 's) prism" where
"lens_prism X = ⦇ prism_match = (λ s. if (s ∈ 𝒮⇘X⇙) then Some (get⇘X⇙ s) else None)
                , prism_build = create⇘X⇙ ⦈"

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: "get⇘prism_lens X⇙ = the ∘ match⇘X⇙"
  by (simp add: prism_lens_def fun_eq_iff)

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

lemma create_prism_lens: "create⇘prism_lens X⇙ = build⇘X⇙"
  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 ⟹ put⇘prism_lens (lens_prism X)⇙ = put⇘X⇙"
  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 "match⇘lens_prism X⇙ (build⇘lens_prism X⇙ v) = Some v"
    by (simp add: lens_prism_def weak_lens.create_closure assms)
  assume a: "match⇘lens_prism X⇙ s = Some v"
  show "s = build⇘lens_prism X⇙ v"
  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