Theory Separation_Lenses.SLens

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

theory SLens
  imports 
    Lenses_And_Other_Optics.Lens
    Shallow_Separation_Logic.Separation_Algebra 
begin

section ‹Separation lenses›

text‹A ∗‹separation lens› is a lens between two separation algebras that is
compatible with the separation algebra structures.

Separation lenses are an axiomatic description of product separation algebras.

We primarily care about separation lenses as they allow for the 'pullback' of
various constructions (programs, specifications, proofs), thereby providing a
convenient way to extend implementations of the standard interfaces (e.g. references,
physical memory) to larger separation algebras and thereby making them composable.›

subsection‹Definition›

definition is_valid_slens :: ‹('a::sepalg, 'b::sepalg) lens ⇒ bool› where
  [simplified Let_def]: ‹is_valid_slens l ≡
     let view = lens_view l in
     let update = lens_update l
     in
       (is_valid_lens l) ∧
       (∀x y. x ♯ y ⟶ view x ♯ view y) ∧
       (∀x y. x ♯ y ⟶ view (x + y) = view x + view y) ∧
       (∀f x y. x ♯ y
          ⟶ f (view x) ♯ view y
          ⟶ f (view x + view y) = f (view x) + view y
          ⟶ lens_modify l f (x + y) = lens_modify l f x + y) ∧
       (∀f x y. x ♯ y
          ⟶ f (view x) ♯ view y
          ⟶ f (view x + view y) = f(view x) + view y
          ⟶ lens_modify l f x ♯ y)›

lemma is_valid_slensI:
  assumes ‹is_valid_lens l›
      and ‹⋀x y. x ♯ y ⟹ lens_view l x ♯ lens_view l y›
      and ‹⋀x y. x ♯ y ⟹ lens_view l (x + y) = lens_view l x + lens_view l y›
      and ‹⋀f x y.
          x ♯ y
          ⟹ f (lens_view l x) ♯ lens_view l y
          ⟹ f (lens_view l x + lens_view l y) = f (lens_view l x) + lens_view l y
          ⟹ lens_modify l f (x + y) = lens_modify l f x + y›
      and ‹⋀f x y.
          x ♯ y
          ⟹ f (lens_view l x) ♯ lens_view l y
          ⟹ f(lens_view l x + lens_view l y) = f(lens_view l x) + lens_view l y
          ⟹ lens_modify l f x ♯ y›
    shows ‹is_valid_slens l›
  using assms unfolding is_valid_slens_def by auto

lemma is_valid_slensE:
  assumes ‹is_valid_slens l›
      and ‹is_valid_lens l
           ⟹ (⋀x y. x ♯ y ⟹ lens_view l x ♯ lens_view l y)
           ⟹ (⋀x y. x ♯ y ⟹ lens_view l (x + y) = lens_view l x + lens_view l y)
           ⟹ (⋀f x y.
                    x ♯ y
                    ⟹ f (lens_view l x) ♯ lens_view l y
                    ⟹ f (lens_view l x + lens_view l y) = f (lens_view l x) + lens_view l y
                    ⟹ lens_modify l f (x + y) = lens_modify l f x + y)
           ⟹ (⋀f x y.
                    x ♯ y
                    ⟹ f (lens_view l x) ♯ lens_view l y
                    ⟹ f(lens_view l x + lens_view l y) = f(lens_view l x) + lens_view l y
                    ⟹ lens_modify l f x ♯ y)
           ⟹ R›
    shows ‹R›
  using assms unfolding is_valid_slens_def by auto

locale slens =
  fixes l :: ‹('s::sepalg, 't::sepalg) lens›
  assumes slens_valid: ‹is_valid_slens l›
declare slens_def[simp]

context slens
begin

lemma is_valid_slens_facts:
  shows lens_valid: ‹is_valid_lens l›
    and slens_view_local1: ‹⋀x y. x ♯ y ⟹ lens_view l x ♯ lens_view l y›
    and slens_view_local2: ‹⋀x y. x ♯ y ⟹ lens_view l (x + y) = lens_view l x + lens_view l y›
    and slens_update_local1: ‹⋀x y. 
          x ♯ y
          ⟹ f (lens_view l x) ♯ lens_view l y
          ⟹ f (lens_view l x + lens_view l y) = f (lens_view l x) + lens_view l y 
          ⟹ lens_modify l f (x + y) = lens_modify l f x + y› 
    and slens_update_local2: ‹⋀x y. 
          x ♯ y
          ⟹ f (lens_view l x) ♯ lens_view l y
          ⟹ f (lens_view l x + lens_view l y) = f (lens_view l x) + lens_view l y 
          ⟹ lens_modify l f x ♯ y› 
  using slens_valid by (auto elim: is_valid_slensE)

text‹We begin by proving that ▩‹slens_update_local{1,2}› imply their counterparts for updates
on ∗‹constant› functions. This can be safely skipped.›

lemma slens_update_local_constant:
  assumes ‹x = x0 + x1›
      and ‹x0 ♯ x1›
      and ‹y0' ♯ lens_view l x1›
    shows ‹lens_update l (y0' + lens_view l x1) x = lens_update l y0' x0 + x1›
      and ‹lens_update l y0' x0 ♯ x1›
proof -
  from assms have view_add: ‹lens_view l (x0 + x1) = lens_view l x0 + lens_view l x1›
    using slens_view_local2 by fastforce
  let ?f = ‹λt. if t = lens_view l x0 + lens_view l x1 then y0' + lens_view l x1 else y0'›
  { assume ‹lens_view l x0 ≠ lens_view l x0 + lens_view l x1›
    from this and assms have ‹lens_update l (y0' + lens_view l x1) x = lens_update l y0' x0 + x1›
      using slens_update_local1[of x0 x1 ‹?f›] slens_update_local2[of x0 x1 ‹?f›] 
      by (simp add: lens_modify_def view_add) }
  moreover { assume ‹lens_view l x0 = lens_view l x0 + lens_view l x1›
    from this have ‹lens_view l x1 = 0›
      by (metis assms(2) sepalg_apart_plus slens_view_local1 unique)
    from this have ‹lens_update l (y0' + lens_view l x1) x = lens_update l y0' x0 + x1›
      using assms slens_update_local1[of x0 x1 ‹?f›] slens_update_local2[of x0 x1 ‹?f›]
      by (simp add: lens_modify_def view_add) }
  ultimately show ‹lens_update l (y0' + lens_view l x1) x = lens_update l y0' x0 + x1›
    by auto
next
  let ?f = ‹λt. if t = lens_view l x0 + lens_view l x1 then y0' + lens_view l x1 else y0'›
  { assume ‹lens_view l x0 ≠ lens_view l x0 + lens_view l x1›
    from this and assms have ‹lens_update l y0' x0 ♯ x1›
      using slens_update_local2[of x0 x1 ‹?f›] 
      by (force simp add: lens_modify_def) }
  moreover { assume ‹lens_view l x0 = lens_view l x0 + lens_view l x1›
    from this have ‹lens_view l x1 = 0›
      by (metis assms(2) sepalg_apart_plus slens_view_local1 unique)
    from this and ‹lens_view l x0 = lens_view l x0 + lens_view l x1› have ‹lens_update l y0' x0 ♯ x1›
      using assms lens_valid slens_update_local2[where f=‹?f›]
      by (force simp add: lens_modify_def) }
  ultimately show ‹lens_update l y0' x0 ♯ x1›
    by auto
qed

lemma slens_update_local3: ‹⋀x x0 x1 y0'. x = x0 + x1 ⟹ x0 ♯ x1 ⟹  y0' ♯ lens_view l x1 ⟹
          lens_update l (y0' + lens_view l x1) x = lens_update l y0' x0 + x1›
  using slens_update_local_constant(1) by blast

lemma slens_update_local4: ‹⋀x x0 x1 y0'. x = x0 + x1 ⟹ x0 ♯ x1 ⟹  y0' ♯ lens_view l x1 ⟹
          lens_update l y0' x0 ♯ x1›
  using slens_update_local_constant(2) by blast

subsection‹Separation lenses as product projections›

text‹Our goal, now, is to show that the separation lens axioms imply that the ▩‹'s› is (isomorphic to)
the ∗‹separation algebra product› of ▩‹'t› and the ∗‹kernel› of ▩‹lens_view l :: 's ⇒ 't›: Those elements ▩‹x›
where ▩‹lens_view l x = 0›. The corresponding embedding ▩‹'t ⇒ 's› is given by ▩‹y ↦ lens_update l (λ_. y) 0›, and
the projection of ▩‹'s› onto the kernel of ▩‹view› is ▩‹x ↦ lens_update l 0 x›.›

abbreviation slens_embed :: ‹'t ⇒ 's› where
  ‹slens_embed x ≡ lens_update l x 0›

abbreviation slens_proj0 :: ‹'s ⇒ 's› where
  ‹slens_proj0 x ≡ slens_embed (lens_view l x)›

abbreviation slens_proj1 :: ‹'s ⇒ 's› where
  ‹slens_proj1 x ≡ lens_update l 0 x›

abbreviation ‹slens_view ≡ lens_view l›

notation slens_embed ("ι")
notation slens_view ("π")
notation slens_proj0 ("ρ⇩0")
notation slens_proj1 ("ρ⇩1")

text‹First, we show that indeed every element is the disjoint sum of its two projections:›

lemmas slens_lens_laws = lens_laws[OF lens_valid, simplified]

lemma slens_decompose:
  shows ‹x = ρ⇩0 x + ρ⇩1 x›
    and ‹ρ⇩0 x ♯ ρ⇩1 x›
proof -
  have ‹x = lens_update l (π x) x›
    by (simp add: slens_lens_laws)
  moreover from this have ‹ρ⇩0 x + ρ⇩1 x = lens_update l (π x) (0 + ρ⇩1 x)›
    using slens_lens_laws
    by (metis (no_types, lifting) sepalg_ident sepalg_ident2 slens_update_local3 zero_disjoint
      zero_disjoint2)
  moreover have ‹lens_update l (π x) (0 + ρ⇩1 x) = lens_update l (π x) (ρ⇩1 x)›
    by simp
  moreover have ‹lens_update l (π x) (ρ⇩1 x) = x›
    using slens_lens_laws  by presburger
  ultimately show ‹x = ρ⇩0 x + ρ⇩1 x›
    by simp
  show ‹ρ⇩0 x ♯ ρ⇩1 x›
    using slens_lens_laws slens_update_local4 by auto
qed

text‹We also note that the two projections are idempotent:›

―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma slens_proj0_idempotent:
  shows ‹ρ⇩0 (ρ⇩0 x) = ρ⇩0 x›
  by (simp add: slens_lens_laws)

―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma slens_proj1_idempotent:
  shows ‹ρ⇩1 (ρ⇩1 x) = ρ⇩1 x›
  by (simp add: slens_lens_laws)

lemma slens_complement_disj:
  shows ‹x ♯ ι y ⟷ π x ♯ y›
  using slens_lens_laws by (metis disjoint_sym slens_update_local4 slens_view_local1 zero_disjoint2)

text‹The images of the two projections are disjoint:›

lemma slens_proj_disjoint:
  shows ‹ρ⇩0 x ♯ ρ⇩1 y›
  using slens_lens_laws  slens_update_local4 by force

text‹If we know a decomposition of an element into its ▩‹ρ⇩0› and ▩‹ρ⇩1›-components,
applying ▩‹ρ⇩0› forgets the ▩‹ρ⇩1›-component:›

lemma slens_proj0_sum:
  shows ‹ρ⇩0 (ρ⇩0 x + ρ⇩1 y) = ρ⇩0 x›
  using slens_lens_laws by (metis slens_decompose(1))

text‹Before establishing the analogue of ▩‹slens_proj0_sum› for ▩‹ρ⇩1›, we first prove the following
useful characterization of ▩‹update› as updating the ▩‹ρ⇩0›-component only:›
corollary slens_update_components:
  shows ‹ρ⇩0 (lens_update l y x) = ι y›
    and ‹ρ⇩1 (lens_update l y x) = ρ⇩1 x›
  using slens_lens_laws by force+

lemma slens_update_alt:
  shows ‹lens_update l y x = ρ⇩1 x + ι y›
    and ‹ρ⇩1 x ♯ ι y›
  using slens_lens_laws
  apply (metis sepalg_comm slens_decompose(1) slens_proj_disjoint)
  using slens_lens_laws slens_update_local2
  apply (simp add: slens_complement_disj)
  done

―‹NOTE: This lemma is not used at present, but seems worth keeping.›
lemma slens_proj1_sum:
  shows ‹ρ⇩1 (ρ⇩0 x + ρ⇩1 y) = ρ⇩1 y›
  using slens_lens_laws by (metis slens_decompose(1))

text‹Next, we establish that the 'extension-by-0' embedding ▩‹ι: 't ⇒ 's› is additive:›

lemma slens_embed_additive:
  assumes ‹y0 ♯ y1›
  shows ‹ι y0 ♯ ι y1›
    and ‹ ι (y0 + y1) = ι y0 + ι y1›
  using slens_lens_laws apply -
  apply (simp add: assms slens_complement_disj)
  apply (metis assms slens_update_alt(1) slens_update_alt(2) slens_update_local3)
  done

lemma slens_complement_cancel_core:
  assumes ‹π x = 0›
  shows ‹ρ⇩1 (x + ι y) = x›
  using slens_lens_laws by (metis assms slens_update_alt(1))

lemma slens_complement_cancel:
  assumes ‹x ♯ lens_update l y 0›
  shows ‹ρ⇩1 (x + ι y) = ρ⇩1 x›
proof -
  have ‹x = ρ⇩1 x + ρ⇩0 x›
    using slens_decompose by simp
  from this have ‹ρ⇩1 (x + ι y) = ρ⇩1 (ρ⇩1 x + (ρ⇩0 x + ι y))›
    by (metis assms sepalg_assoc slens_update_alt(2) slens_update_local4 slens_view_local1 zero_disjoint2)
  moreover have ‹ρ⇩0 x + ι y = ι (π x + y)›
     by (metis assms slens_complement_disj slens_embed_additive(2))
  moreover from calculation have ‹ρ⇩1 (x + ι y) = ρ⇩1 (ρ⇩1 x + ι (π x + y))›
    by presburger
  moreover have ‹... = ρ⇩1 (ρ⇩1 x)›
    using slens_lens_laws by (metis slens_update_alt(1))
  ultimately show ?thesis
    using slens_lens_laws by presburger
qed

lemma slens_complement_additive:
  assumes ‹x0 ♯ x1›
  shows ‹ρ⇩1 x0 ♯ ρ⇩1 x1›
    and ‹ρ⇩1 (x0 + x1) = ρ⇩1 x0 + ρ⇩1 x1›
proof -
  let ?x00 = ‹lens_update l (π x0) 0›
  let ?x01 = ‹lens_update l 0 x0›
  let ?x10 = ‹lens_update l (π x1) 0›
  let ?x11 = ‹lens_update l 0 x1›
  have dec_x0: ‹x0 = ?x00 + ?x01›
    and dec_x1: ‹x1 = ?x10 + ?x11›
    and dec_x0_disj: ‹?x00 ♯ ?x01›
    and dec_x1_disj: ‹?x10 ♯ ?x11›
    using slens_decompose by blast+
  moreover from this and ‹x0 ♯ x1› have ‹?x00 ♯ ?x10› and ‹?x00 ♯ ?x11›
    and ‹?x01 ♯ ?x10› and ‹?x01 ♯ ?x11›
    using slens_update_local4 slens_view_local1 by auto
  moreover from this show ‹?x01 ♯ ?x11› by simp
  moreover from calculation have ‹lens_update l 0 (x0 + x1)
     = lens_update l 0 (?x00 + ?x01 + ?x11 + ?x10)›
    by (metis assms disjoint_sym sepalg_apart_plus2 sepalg_assoc sepalg_comm)
  moreover from calculation have ‹?x00 + ?x01 + ?x11 + ?x10 = (?x00 + ?x01 + ?x11) + ?x10›
    by blast
  moreover have ‹lens_update l 0 ((?x00 + ?x01 + ?x11) + ?x10) = lens_update l 0 (?x00 + ?x01 + ?x11)›
    using slens_complement_cancel
    by (metis assms dec_x0 dec_x1 sepalg_apart_assoc2 sepalg_comm slens_update_alt(2))
  ultimately show ‹lens_update l 0 (x0 + x1) = ?x01 + ?x11›
    by (metis sepalg_ident2 slens_lens_laws(1,3) slens_update_local3 zero_disjoint slens_update_local4)
qed

text‹Finally, we can show that ▩‹update› can be computed componentwise for disjoint decompositions.
Note that the separation lens axioms only give this in the case where one factor is unmodified.›

lemma slens_update_general:
  assumes ‹x0 ♯ x1›
      and ‹y0 ♯ y1›
      and ‹y0' ♯ y1'›
    shows ‹lens_update l (y0' + y1') (x0 + x1) = lens_update l y0' x0 + lens_update l y1' x1›
proof -
  obtain #: ‹ρ⇩1 x0 ♯ ρ⇩1 x1› ‹ρ⇩1 x0 ♯ ι y0'› ‹ρ⇩1 x0 ♯ ι y1'› ‹ ι y0' ♯ ρ⇩1 x1›
    using assms(1) slens_complement_additive(1) slens_update_alt(2) by auto
  with assms obtain disj: ‹ρ⇩1 x0 ♯ ρ⇩1 x1 + ι y1'› ‹ι y0' ♯ ρ⇩1 x1 + ι y1'›
    by (metis disjoint_sym slens_lens_laws(1) slens_update_alt(1) slens_update_local4 zero_disjoint2)
  have ‹lens_update l (y0' + y1') (x0 + x1) = ρ⇩1 (x0 + x1) + ι (y0' + y1')›
    using slens_update_alt(1) by blast
  also have ‹... = ρ⇩1 x0 + ρ⇩1 x1 + (ι y0' + ι y1')›
    using assms(1) assms(3) slens_complement_additive(2) slens_embed_additive(2) by presburger
  also have ‹... = ρ⇩1 x0 + (ρ⇩1 x1 + (ι y0' + ι y1'))›
    using # assms
    by (metis sepalg_assoc slens.slens_update_alt(2) slens_axioms slens_embed_additive(2))
  also have ‹ρ⇩1 x1 + (ι y0' + ι y1') = ρ⇩1 x1 + ι y0' + ι y1'›
    by (metis assms(3) sepalg_assoc slens_embed_additive(1) slens_update_alt(2))
  also have ‹... = ι y0' + (ρ⇩1 x1 + ι y1')›
    using disj # assms
    by (metis sepalg_assoc sepalg_comm slens_embed_additive(1) slens_update_alt(2))
  also have ‹ρ⇩1 x0 + (ι y0' + (ρ⇩1 x1 + ι y1')) = ρ⇩1 x0 + ι y0' + (ρ⇩1 x1 + ι y1')›
    using disj # sepalg_assoc by blast
  also have ‹... = lens_update l y0' x0 + lens_update l y1' x1›
    by (metis slens_update_alt(1))
  finally show ?thesis .
qed

lemma slens_update_disjoint:
  assumes ‹y0' ♯ y1›
    shows ‹lens_update l (y0' + y1) x0 = lens_update l y0' x0 + lens_update l y1 0›
  by (metis assms sepalg_ident2 slens_update_general zero_disjoint)

text‹As a simple corollary to the decomposition of ▩‹'s› into ▩‹'t› and its complement, we obtain
liftability of decompositions in ▩‹'t› to ▩‹'s›:›

lemma slens_lift_decomposition:
  assumes ‹π x = y0 + y1›
     and ‹y0 ♯ y1›
   obtains x0 x1 where ‹π x0 = y0› and ‹π x1 = y1› and ‹x0 ♯ x1› and ‹x = x0 + x1›
proof -
  let ?x0 = ‹lens_update l y0 0›
  let ?x1 = ‹lens_update l y1 x›
  have ‹lens_view l ?x0 = y0› and ‹lens_view l ?x1 = y1›
    using slens_lens_laws by simp+
  moreover have ‹?x0 ♯ ?x1›
    using slens_lens_laws by (metis assms(2) disjoint_sym slens_complement_disj)
  moreover have ‹x = ?x0 + ?x1›
    using slens_lens_laws
    by (metis (no_types, opaque_lifting) assms sepalg_ident slens_update_general zero_disjoint2)
  ultimately show ?thesis
    using that by blast
qed

no_notation slens_embed ("ι")
no_notation slens_view ("π")
no_notation slens_proj0 ("ρ⇩0")
no_notation slens_proj1 ("ρ⇩1")

end

end