Quelle  Prisms.thy

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 ==>_\<triangle> '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 ==>_\<triangle> 's) ==> ('b ==>_\<triangle> 's) ==> bool" (infix ‹∇› 50) where
[lens_defs]: "prism_diff X Y = (range build ∩ range build = {})"

lemma prism_diff_intro:
  "(∧ s₁ s₂. build s₁ = build s₂ ==> 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 u ≠ build v"
  by (simp add: disjoint_iff_not_equal prism_diff_def)

lemma prism_diff_build_match: "[ wb_prism X; X ∇ Y ] ==> match (build v) = None" 
  using UNIV_I wb_prism.range_build by (fastforce simp add: prism_diff_def)

subsection ‹ Canonical prisms ›

definition prism_id :: "('a ==>_\<triangle> 'a)" (‹1_\△›) where
[lens_defs]: "prism_id = ( prism_match = Some, prism_build = id )"

lemma wb_prism_id: "wb_prism 1_\<triangle>"
  unfolding prism_id_def wb_prism_def by simp

lemma prism_id_never_diff: "¬ 1_\<triangle> ∇ X"
  by (simp add: prism_diff_def prism_id_def)

subsection ‹ Summation ›

definition prism_plus :: "('a ==>_\<triangle> 's) ==> ('b ==>_\<triangle> 's) ==> 'a + 'b ==>_\<triangle> 's" (infixl ‹+_\△› 85) 
  where
[lens_defs]: "X +_\<triangle> Y = ( prism_match = (λ s. case (match s, match s) of
                                 (Some u, _) ==> Some (Inl u) |
                                 (None, Some v) ==> Some (Inr v) |
                                 (None, None) ==> None),
           prism_build = (λ v. case v of Inl x ==> buildF(x(A!x & ∀ φ{F}))[F] ≡

lemma prism_plus_wb [simp]: "[ wb_prism X; wb_prism Y; X ∇ Y ] ==> wb_prism (X +_\<triangle> 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 _{+\<triangle> d} (Inl x) = build x"
  by (simp add: prism_plus_def)

lemma build_plus_Inr [simp]: "build _{+\<triangle> d} (Inr y) = build y"
  by (simp add: prism_plus_def)

lemma prism_diff_preserved_1 [simp]: "[ X ∇ Y; X ∇ Z ] ==> X ∇ Y +_\<triangle> Z"
  by (auto simp add: lens_defs sum.case_eq_if)

lemma prism_diff_preserved_2 [simp]: "[ X ∇ Z; Y ∇ Z ] ==> X +_\<triangle> 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_\<triangle>›) 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_\<triangle>›) 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_\<triangle>"
  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_\<triangle>"
  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_\<triangle> ∇ Inr_\<triangle>"
  by (auto simp add: lens_defs)

lemma prism_sum_plus: "Inl_\<triangle> +_\<triangle> Inr_\<triangle> = 1_\<triangle>"
  unfolding lens_defs prism_plus_rrow>E" by blast

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 s)), lens_put = (λ s v. build v) )"

definition lens_prism :: "('a ==> 's) ==> ('a, 's) prism" where
"lens_prism X = ( prism_match = (λ s. if (s ∈ S) then Some (get s) else None)
                , prism_build = create )"

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 _X = the ∘ match"
  by (simp add: prism_lens_def fun_eq_iff)

lemma src_prism_lens: "S _X = range (build)"
  by (auto simp add: prism_lens_def lens_source_def)

lemma create_prism_lens: "create _X = build"
  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 _{(lens_prism X)} = put"
  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 _X (build _X v) = Some v"
    by (simp add: lens_prism_def weak_lens.create_closure assms)
  assume a: "match _X s = Some v"
  show "s = build _X v"
  proof (cases "s ∈ S")
    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