Theory Lenses_And_Other_Optics.Prism

(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
   SPDX-License-Identifier: MIT *)

(*<*)
theory Prism
  imports Main "HOL-Library.Datatype_Records"
begin
(*>*)

(*<*)
named_theorems focus_rules
named_theorems focus_intros
named_theorems focus_elims
named_theorems focus_simps
named_theorems focus_components
(*>*)

section‹Prisms›

text‹Prisms are types that describe how one type acts as a subtype of another. They are defined as a
pair of an embedding of the subtype into the larger, compound type, and a partial projection
in the other direction.  If lenses describe the interaction of modifications and reads of deeply-nested
fields within a record or product-like type, then prisms describe the interactions of modifications
and reads of deeply-nested fields within a sum-like type, such as a disjoint union.

Mathematically, one can think of prisms as ∗‹subsets/embeddings›.›
datatype_record ('s, 'a) prism =
  prism_embed :: ‹'a ⇒ 's›
  prism_project :: ‹'s ⇒ 'a option›

text ‹Like lenses, prisms also have a notion of ∗‹validity› that governs how their operations
interact.  Specifically:
\begin{itemize*}
\item
Embedding a field into a sum-like type and then immediately projecting it back out again
successfully returns the embedded field,
\item
If projecting a field out of a sum-like type is successful then embedding that projected-out value
into the sum-like type has no effect.
\end{itemize*}›
definition is_valid_prism :: ‹('s, 'a) prism ⇒ bool› where
  ‹is_valid_prism p ⟷
     (∀a. prism_project p (prism_embed p a) = Some a) ∧
     (∀s a. (prism_project p) s = Some a ⟶ s = (prism_embed p) a)›

lemma prism_laws:
  assumes ‹is_valid_prism p›
  shows [focus_simps]: ‹prism_project p (prism_embed p a) = Some a›
    and ‹prism_project p s = Some a ⟷ s = prism_embed p a›
  using assms unfolding is_valid_prism_def by auto

definition prism_dom :: ‹('a, 'b) prism ⇒ 'a set› where
  ‹prism_dom p ≡ dom (prism_project p)›

lemma prism_dom_alt: 
  assumes ‹is_valid_prism p›
  shows ‹prism_dom p = prism_embed p ` UNIV›
  using assms by (auto simp add: is_valid_prism_def image_def prism_dom_def)

lemma prism_dom_alt': 
  assumes ‹is_valid_prism p›
  shows ‹prism_embed p x ∈ prism_dom p›
  using assms by (simp add: prism_dom_alt)

lemma prism_domI:
  assumes ‹prism_project p x ≠ None›
    shows ‹x ∈ prism_dom p›
  using assms unfolding prism_dom_def by auto

lemma prism_domI':
  assumes ‹is_valid_prism p›
     and ‹x = prism_embed p y›
   shows ‹x ∈ prism_dom p›
  using assms by (simp add: prism_dom_alt)

lemma prism_domE:
  assumes ‹x ∈ prism_dom p›
      and ‹prism_project p x ≠ None ⟹ R›
    shows R
  using assms prism_dom_def by fastforce

lemma prism_domE':
  assumes ‹x ∈ prism_dom p›
      and ‹is_valid_prism p›
      and ‹⋀y. x = prism_embed p y ⟹ R›
    shows R
  using assms prism_dom_alt by fastforce

definition prism_compose :: ‹('a, 'b) prism ⇒ ('b, 'c) prism ⇒ ('a, 'c) prism› (infixr "⋄⇩p" 59)
  where ‹prism_compose pA pB ≡
    make_prism ((prism_embed pA) ∘ (prism_embed pB))
                (λx. Option.bind (prism_project pA x) (prism_project pB))›

lemma prism_compose_valid:
  assumes ‹is_valid_prism pA›
      and ‹is_valid_prism pB›
    shows ‹is_valid_prism (pA ⋄⇩p pB)›
  using assms by (auto simp add: is_valid_prism_def prism_compose_def bind_eq_Some_conv
    split:option.splits)

text‹Prisms are preserved under the ▩‹option› type constructor:›

definition option_prism :: ‹('c, 'a option) prism ⇒ ('a, 'b) prism ⇒ ('c, 'b option) prism›
  where
  ‹option_prism rawp elp ≡
    make_prism (λx. prism_embed rawp (map_option (prism_embed elp) x))
               (λg. Option.bind (prism_project rawp g)
                      (λx. case x of None ⇒ Some None | Some v ⇒ Option.bind (prism_project elp v) (λv'. Some (Some v'))))›

lemma option_prism_valid [focus_intros]:
  assumes
    ‹is_valid_prism rawp›
    ‹is_valid_prism elp›
  shows
    ‹is_valid_prism (option_prism rawp elp)›
  using assms unfolding is_valid_prism_def option_prism_def
  by (auto split: option.splits Option.bind_split)

fun list_option_distrib :: ‹'a option list ⇒ 'a list option› where
  ‹list_option_distrib [] = Some []› |
  ‹list_option_distrib (None#l) = None› |
  ‹list_option_distrib (Some x#l) = Option.bind (list_option_distrib l) (λl'. Some (x#l'))›

text‹Prisms are preserved under the ▩‹option› type constructor:›

definition list_prism :: ‹('c, 'a list) prism ⇒ ('a, 'b) prism ⇒ ('c, 'b list) prism›
  where
  ‹list_prism lp elp ≡
     make_prism (λl. prism_embed lp (List.map (prism_embed elp) l))
                (λg. Option.bind (prism_project lp g) (λl. list_option_distrib (List.map (prism_project elp) l)))›

lemma list_option_distrib_Some:
  ‹list_option_distrib xs = Some ys ⟷ xs = list.map Some ys›
  apply (induction xs arbitrary: ys, auto split: Option.bind_split)
  apply (case_tac a; simp?)
  apply (case_tac ‹list_option_distrib xs›; clarsimp)
  apply fast
  done

corollary list_option_distrib_map_Some:
  ‹list_option_distrib (list.map Some xs) = Some xs›
  using list_option_distrib_Some by auto

lemma list_option_distrib_None:
  ‹list_option_distrib xs = None ⟷ None∈set xs›
  apply (induction xs, auto)
  apply (case_tac a; simp)
  apply (case_tac a; simp)
  done

lemma list_prism_valid [focus_intros]:
  assumes
    ‹is_valid_prism lp›
    ‹is_valid_prism elp›
  shows
    ‹is_valid_prism (list_prism lp elp)›
proof -
  have ‹prism_project elp ∘ prism_embed elp = Some›
    using assms unfolding is_valid_prism_def comp_def by auto
  moreover {
    fix v a
    have ‹list.map (prism_project elp) v = list.map Some a ⟹ v = list.map (prism_embed elp) a›
    using assms unfolding is_valid_prism_def by (induction v arbitrary: a; clarsimp)
  }
  then show ?thesis
    using assms unfolding is_valid_prism_def list_prism_def
    by (auto simp add: list_option_distrib_Some split: Option.bind_split)
qed

text‹Isomorphisms are special cases of prisms:›

text‹The following builds a prism out of a pair of mutually inverse bijections:›
definition iso_prism :: ‹('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ ('a, 'b) prism›
  where ‹iso_prism f g ≡ make_prism g (Some ∘ f)›

lemma iso_prism_valid:
  assumes ‹⋀x. f (g x) = x›
      and ‹⋀y. g (f y) = y›
  shows ‹is_valid_prism (iso_prism f g)›
  using assms by (auto simp add: iso_prism_def is_valid_prism_def)

(*<*)
end
(*>*)