Theory Lenses_And_Other_Optics.Focus

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

(*<*)
theory Focus
  imports Lens Prism
begin
(*>*)

section‹Foci›

text‹A focus is a common generalization of focuses and prisms. With focuses roughly corresponding
to quotients and prisms to subsets, a focus can be seen as a way of representing a subquotient.

Typically, foci do not arise directly, but rather as the composition of (the liftings to foci of)
focuses and prisms.

Note that one could also use the type typ('a  'a)  ('s  's option) in the type of the
modification function, here, allowing the ``lifted'' function to return termNone on values
outside of the domain the view. Here, we instead expect (and axiomatize below) that the modification
function is simply the identity on those inputs:›
datatype_record ('s, 'a) focus_raw =
  focus_raw_view   :: 's  'a option
  focus_raw_update :: 'a  's  's

definition focus_raw_dom :: ('v, 'w) focus_raw  'v set where
  focus_raw_dom f  dom (focus_raw_view f)

lemma focus_raw_domI:
  assumes focus_raw_view l x = Some y
    shows x  focus_raw_dom l
using assms unfolding focus_raw_dom_def by auto

lemma focus_raw_domE:
  assumes x  focus_raw_dom l
      and y. focus_raw_view l x = Some y  R
    shows R
using assms unfolding focus_raw_dom_def by auto

text‹We never modify a value that's not in the domain of the focus, so the use of termthe in the 
following definition should not cause problems:›
definition focus_raw_modify :: ('s, 'a) focus_raw  ('a  'a)  's  's where
  focus_raw_modify l f s  focus_raw_update l (f (the (focus_raw_view l s))) s

abbreviation focus_raw_is_view :: ('s, 'a) focus_raw  's  'a  bool where
  focus_raw_is_view f s a  focus_raw_view f s = Some a

text ‹As generalisations of both focuses and prisms, a focus also has a notion of well-formedness.
Specifically, we have:
\begin{enumerate*}
\item
Viewing a focus after a modification is the same as applying the modification directly to the result
of viewing the focus,
\item
If a modification cannot be observed then applying the modification to a type has no effect,
\item
Applying two modifications in sequence is the same as applying a single, compound modification.
\item
Modifying a field is the same as updating a viewed field.
\end{enumerate*}

Note that these are straightforward generalisations of the laws of focus validity to focuses!›
definition is_valid_focus :: ('s, 'a) focus_raw  bool where
  is_valid_focus l 
      (x y0 y1. focus_raw_view l x = Some y0   focus_raw_view l (focus_raw_update l y1 x) = Some y1) 
      (x y. focus_raw_view l x = None   focus_raw_view l (focus_raw_update l y x) = None) 
      (x y. focus_raw_view l x = Some y  focus_raw_update l y x = x) 
      (x y. focus_raw_view l x = None  focus_raw_update l y x = x) 
      (x y0 y1 y2. focus_raw_view l x = Some y0  
          focus_raw_update l y2 (focus_raw_update l y1 x) = focus_raw_update l y2 x)

text‹Any two types admit a valid focus between them. This is irrelevant in practice, but technically
important because it allows us to form the subtype of valid foci later.›
definition dummy_focus :: ('a, 'b) focus_raw where
  dummy_focus  make_focus_raw (λ_. None) (λ_ x. x)

lemma dummy_focus_is_valid:
  shows is_valid_focus dummy_focus
by (simp add: dummy_focus_def is_valid_focus_def)

text ‹The following are basic introduction and elimination rules for working with the
‹is_valid_focus› predicate:›
lemma is_valid_focusI:
  assumes x y0 y1. focus_raw_view l x = Some y0  focus_raw_view l (focus_raw_update l y1 x) = Some y1
      and x y. focus_raw_view l x = None   focus_raw_view l (focus_raw_update l y x) = None
      and x y. focus_raw_view l x = Some y  focus_raw_update l y x = x
      and x y. focus_raw_view l x = None  focus_raw_update l y x = x
      and x y0 y1 y2. focus_raw_view l x = Some y0 
              focus_raw_update l y2 (focus_raw_update l y1 x) = focus_raw_update l y2 x
    shows is_valid_focus l
using assms by (auto simp add: is_valid_focus_def)

lemma is_valid_focusE:
  assumes is_valid_focus l
      and (x y0 y1. focus_raw_view l x = Some y0  focus_raw_view l (focus_raw_update l y1 x) = Some y1) 
              (x y. focus_raw_view l x = None   focus_raw_view l (focus_raw_update l y x) = None) 
              (x y. focus_raw_view l x = Some y  focus_raw_update l y x = x) 
              (x y. focus_raw_view l x = None  focus_raw_update l y x = x) 
              (x y0 y1 y2. focus_raw_view l x = Some y0 
                focus_raw_update l y2 (focus_raw_update l y1 x) = focus_raw_update l y2 x)  R
    shows R
using assms by (auto simp add: is_valid_focus_def)

lemma focus_raw_laws_update:
  assumes is_valid_focus l
    shows (x y0 y1. focus_raw_view l x = Some y0  focus_raw_view l (focus_raw_update l y1 x) = Some y1)
      and x y. focus_raw_view l x = None   focus_raw_view l (focus_raw_update l y x) = None
      and x y. focus_raw_view l x = Some y  focus_raw_update l y x = x
      and x y. focus_raw_view l x = None  focus_raw_update l y x = x
      and x y0 y1 y2. focus_raw_view l x = Some y0 
            focus_raw_update l y2 (focus_raw_update l y1 x) = focus_raw_update l y2 x
using assms by (auto elim: is_valid_focusE)

text‹The following is an alternative axiomatization of foci in terms of update functions:›
lemma is_valid_focus_via_modify:
  assumes is_valid_focus l
    shows f s. focus_raw_view l (focus_raw_modify l f s) = map_option f (focus_raw_view l s)
      and f s. map_option f (focus_raw_view l s) = focus_raw_view l s  focus_raw_modify l f s = s
      and f g s. focus_raw_modify l f (focus_raw_modify l g s) = focus_raw_modify l (λx. f (g x)) s
proof -
  fix f s show focus_raw_view l (focus_raw_modify l f s) = map_option f (focus_raw_view l s)
    using is_valid_focus l 
    by (cases focus_raw_view l s; auto elim!: is_valid_focusE simp add: focus_raw_modify_def)
next
  fix f s show map_option f (focus_raw_view l s) = focus_raw_view l s  focus_raw_modify l f s = s
    using is_valid_focus l 
    by (clarsimp elim!: is_valid_focusE simp add: focus_raw_modify_def)
       (metis option.exhaust_sel option.map_sel)
next
  fix f g s show focus_raw_modify l f (focus_raw_modify l g s) 
                     = focus_raw_modify l (λx. f (g x)) s
    using is_valid_focus l 
    by (cases focus_raw_view l s; auto elim!: is_valid_focusE simp add: focus_raw_modify_def)
qed

lemma focus_raw_laws_modify:
  assumes is_valid_focus l
    shows f s. focus_raw_view l (focus_raw_modify l f s) = map_option f (focus_raw_view l s)
      and f s. map_option f (focus_raw_view l s) = focus_raw_view l s  focus_raw_modify l f s = s
      and f g s. focus_raw_modify l f (focus_raw_modify l g s) = focus_raw_modify l (λx. f (g x)) s
using assms by (auto simp add: is_valid_focus_via_modify)

lemmas focus_raw_laws = focus_raw_laws_update focus_raw_laws_modify

lemma is_valid_focus_via_modifyE:
  assumes is_valid_focus l
      and (f s. focus_raw_view l (focus_raw_modify l f s) = map_option f (focus_raw_view l s)) 
              (f s. map_option f (focus_raw_view l s) = focus_raw_view l s  focus_raw_modify l f s = s) 
              (f g s. focus_raw_modify l f (focus_raw_modify l g s) = focus_raw_modify l (λx. f (g x)) s)  R
    shows R
by (simp add: assms is_valid_focus_via_modify)

text‹The axioms in ‹is_valid_focus_via_modify› are indeed sufficient to construct a valid focus:›
definition is_valid_view_modify :: ('a  'b option)  (('b  'b)  ('a  'a))  bool where
  is_valid_view_modify view modify 
     ((f s. view (modify f s) = map_option f (view s)) 
      (f s. map_option f (view s) = view s  modify f s = s) 
      (f g s. modify f (modify g s) = modify (λx. f (g x)) s))

lemma is_valid_view_modify_modify_via_update:
  assumes is_valid_view_modify view modify  
    shows modify f x = modify (λ_. f (the (view x))) x
proof -
  { assume x  dom view then have ?thesis 
    by (metis assms domIff is_valid_view_modify_def option.simps(8)) }
  moreover { assume x  dom view
    then obtain y where view x = Some y 
      by blast
    then have map_option (λ_. f y) (view (modify f x)) = view (modify f x) 
      by (metis assms is_valid_view_modify_def option.simps(9))
    from this and is_valid_view_modify view modify  
    have modify (λ_. f y) (modify f x) = modify f x 
      by (metis is_valid_view_modify_def) 
    moreover from view x = Some y and is_valid_view_modify view modify  
      have modify (λ_. f y) (modify f x) = modify (λ_. f y) x
      by (clarsimp simp add: is_valid_view_modify_def)
    ultimately have ?thesis 
      using view x = Some y by fastforce
  }
  ultimately show ?thesis by auto
qed

lemma is_valid_focus_via_modify':
  assumes is_valid_focus l
    shows is_valid_view_modify (focus_raw_view l) (focus_raw_modify l)
using assms by (elim is_valid_focus_via_modifyE; clarsimp simp add: is_valid_view_modify_def)

definition make_focus_raw_via_view_modify :: ('v  'w option)  (('w  'w)  'v  'v) 
      ('v, 'w) focus_raw where
  make_focus_raw_via_view_modify view modify  make_focus_raw view (λy. modify (λ_. y))

lemma is_valid_focus_via_modifyI:
  assumes f s. view (modify f s) = map_option f (view s)
      and f s. map_option f (view s) = view s  modify f s = s
      and f g s. modify f (modify g s) = modify (λx. f (g x)) s
    shows is_valid_focus (make_focus_raw_via_view_modify view modify)
using assms by (intro is_valid_focusI) (auto simp add: make_focus_raw_via_view_modify_def)

lemma is_valid_focus_via_modifyI':
  assumes is_valid_view_modify view modify
    shows is_valid_focus (make_focus_raw_via_view_modify view modify)
using assms by (intro is_valid_focus_via_modifyI) (auto simp add: is_valid_view_modify_def)

lemma make_focus_raw_via_view_modify_components:
  shows focus_raw_view (make_focus_raw_via_view_modify view modify) = view
    and focus_raw_update (make_focus_raw_via_view_modify view modify) = (λy. modify (λ_. y))
    and is_valid_view_modify view modify  focus_raw_modify (make_focus_raw_via_view_modify view modify) = modify
proof -
  show focus_raw_view (make_focus_raw_via_view_modify view modify) = view
    by (clarsimp simp add: make_focus_raw_via_view_modify_def)
next
  show focus_raw_update (make_focus_raw_via_view_modify view modify) = (λy. modify (λ_. y))
    by (clarsimp simp add: make_focus_raw_via_view_modify_def)
next
  assume is_valid_view_modify view modify
  moreover {
    fix x y
    from calculation have focus_raw_modify (make_focus_raw_via_view_modify view modify) x y = modify x y
      by (clarsimp simp add: focus_raw_modify_def) (metis focus_raw.sel(1) focus_raw.sel(2)
        is_valid_view_modify_modify_via_update make_focus_raw_via_view_modify_def)
  }
  from this show focus_raw_modify (make_focus_raw_via_view_modify view modify) = modify
    by (intro ext) force
qed

text ‹A lens can also be viewed as a focus:›
definition lens_to_focus_raw :: ('s, 'a) lens  ('s, 'a) focus_raw ("∫''l") where
  lens_to_focus_raw l  make_focus_raw (λs. Some (lens_view l s)) (lens_update l)

lemma lens_to_focus_raw_components:
  shows focus_raw_view (lens_to_focus_raw l) x = Some (lens_view l x)
    and focus_raw_update (lens_to_focus_raw l) = lens_update l
    and focus_raw_modify (lens_to_focus_raw l) f v = lens_modify l f v
proof -
  show focus_raw_view (lens_to_focus_raw l) x = Some (lens_view l x)
    by transfer (simp add: lens_to_focus_raw_def)
next
  show focus_raw_update (lens_to_focus_raw l) = lens_update l
    by transfer (simp add: lens_to_focus_raw_def)
next
  show focus_raw_modify (lens_to_focus_raw l) f v = lens_modify l f v
    by transfer (simp add: focus_raw_modify_def lens_modify_def lens_to_focus_raw_def)
qed

text‹Lifting a valid focus into a focus grants us a valid focus:›
lemma lens_to_focus_raw_valid:
  assumes is_valid_lens l
    shows is_valid_focus (lens_to_focus_raw l)
using assms by (intro is_valid_focusI) (auto simp add: lens_to_focus_raw_def is_valid_lens_def)

text‹A prism can also be viewed as a focus:›
definition prism_to_focus_raw :: ('s, 'a) prism  ('s, 'a) focus_raw ("∫''p") where
  prism_to_focus_raw p 
      let view  = λy. prism_project p y;
          update = λy x. if prism_project p x = None then x else prism_embed p y
      in make_focus_raw view update

lemma prism_to_focus_raw_components:
  shows focus_raw_view (prism_to_focus_raw p) = prism_project p
    and focus_raw_update (prism_to_focus_raw p) y x = (if x  prism_dom p then prism_embed p y else x)
    and focus_raw_modify (prism_to_focus_raw p) f x =
        (if prism_project p x  None then prism_embed p (f (the (prism_project p x))) else x)
proof -
  show focus_raw_view (prism_to_focus_raw p) = prism_project p
    by transfer (simp add: prism_to_focus_raw_def)
next
  show focus_raw_update (prism_to_focus_raw p) y x = (if x  prism_dom p then prism_embed p y else x)
    by transfer (simp add: domIff prism_dom_def prism_to_focus_raw_def)
next
  show focus_raw_modify (∫'p p) f x = (if prism_project p x  None then prism_embed p (f (the (prism_project p x))) else x)
    by transfer (simp add: focus_raw_modify_def prism_to_focus_raw_def)
qed

text ‹Lifting a valid prism into a focus grants us a valid focus:›
lemma prism_to_focus_raw_valid:
  assumes is_valid_prism p
    shows is_valid_focus (prism_to_focus_raw p)
using assms by (intro is_valid_focusI) (auto simp add: is_valid_prism_def prism_to_focus_raw_def
  prism_dom_def)

text‹The following builds a focus out of a pair of mutually inverse bijections:›
definition iso_focus_raw :: ('a  'b)  ('b  'a)  ('a, 'b) focus_raw ("iso") where
  iso_focus_raw g h  prism_to_focus_raw (iso_prism g h)

lemma iso_focus_raw_components:
  shows focus_raw_view (iso_focus_raw  g h) x = Some (g x)
    and focus_raw_update (iso_focus_raw g h) y x = h y  
by (auto simp add: iso_focus_raw_def iso_prism_def prism_to_focus_raw_def)

lemma iso_focus_raw_valid:
  assumes x. f (g x) = x
      and y. g (f y) = y
    shows is_valid_focus (iso_focus_raw f g)
by (simp add: assms iso_focus_raw_def iso_prism_valid prism_to_focus_raw_valid)
  
text‹Like lenses, we may also provide a library of basic focuses. The following is the analogue of
the unit focus, the ‹unit› focus, which has no effect:›
definition unit_focus_raw :: ('a, 'a) focus_raw where
  unit_focus_raw  make_focus_raw Some (λy x. y)

text‹The unit focus is necessarily a valid, well-behaved focus:›
lemma unit_focus_raw_valid:
  shows is_valid_focus unit_focus_raw
by (auto simp add: unit_focus_raw_def is_valid_focus_def focus_raw_update_def)

text‹Similarly, we may ‹compose› focuses together to produce larger, more complex, compound
focuses:›
lemma focus_raw_compose_valid_core:
  assumes is_valid_focus l1
      and is_valid_focus l2
    shows is_valid_view_modify
             (λx. Option.bind (focus_raw_view l1 x) (focus_raw_view l2))
             (λf. focus_raw_modify l1 (focus_raw_modify l2 f))
using assms by (elim is_valid_focus_via_modifyE) (auto simp add: is_valid_view_modify_def split!:
  Option.bind_splits)

definition focus_raw_compose :: ('a, 'b) focus_raw  ('b, 'c) focus_raw  ('a, 'c) focus_raw where
  focus_raw_compose l1 l2 
     make_focus_raw_via_view_modify (λx. Option.bind (focus_raw_view l1 x) (focus_raw_view l2))
        (λf. focus_raw_modify l1 (focus_raw_modify l2 f))
notation focus_raw_compose (infixr "⋄''" 59)

text‹Composing two valid focusses together grants us another valid focus:›
lemma focus_raw_compose_valid:
  assumes is_valid_focus l1
      and is_valid_focus l2
    shows is_valid_focus (focus_raw_compose l1 l2)
by (simp add: assms focus_raw_compose_def focus_raw_compose_valid_core is_valid_focus_via_modifyI')

lemma focus_raw_compose_components:
  assumes is_valid_focus l1
      and is_valid_focus l2
    shows focus_raw_view (focus_raw_compose l1 l2)
              = (λx. Option.bind (focus_raw_view l1 x) (focus_raw_view l2))
      and focus_raw_modify (focus_raw_compose l1 l2)
              = (λf. focus_raw_modify l1 (focus_raw_modify l2 f))
      and focus_raw_update (focus_raw_compose l1 l2)
              = (λy. focus_raw_modify l1 (focus_raw_modify l2 (λ_. y)))
using assms by (auto simp add: focus_raw_compose_def make_focus_raw_via_view_modify_components
  focus_raw_compose_valid_core)

text‹Prism-to-focus conversion is compatible with prism/focus composition:›
lemma prism_to_focus_raw_compose:
  assumes is_valid_prism pA
    shows ∫'p (pA p pB) = (∫'p pA) ⋄' (∫'p pB)
using assms by (auto simp add: is_valid_prism_def prism_compose_def focus_raw_compose_def
  prism_to_focus_raw_def focus_raw_modify_def prism_dom_def bind_eq_Some_conv
  make_focus_raw_via_view_modify_def intro!:ext)

text‹The following pair of lemmas state that composing any other focus with the unit focus has no
effect:›
lemma focus_raw_compose_unit [focus_simps]:
  shows unit_focus_raw ⋄' l = l
by (cases l) (auto intro!: ext simp add: make_focus_raw_via_view_modify_def focus_raw_modify_def
  unit_focus_raw_def focus_raw_compose_def) 

lemma focus_raw_compose_unit2 [focus_simps]:
  shows l ⋄' unit_focus_raw = l
by (cases l) (auto intro!: ext simp add: make_focus_raw_via_view_modify_def focus_raw_modify_def 
  unit_focus_raw_def focus_raw_compose_def) 

text‹The following are technical introduction, elimination, and destruction rules for working with
views of (potentially composed) ‹focus_raw›s:›
lemma focus_raw_view_composeI [focus_intros]:
  assumes focus_raw_view l1 v = Some v'
      and focus_raw_view l2 v' = Some v''
    shows focus_raw_view (focus_raw_compose l1 l2) v = Some v''
using assms by (clarsimp simp add: focus_raw_compose_def make_focus_raw_via_view_modify_def)

lemma focus_raw_view_compose_destruct:
  assumes focus_raw_view (focus_raw_compose l1 l2) v = Some v''
  obtains v' where focus_raw_view l1 v = Some v' and focus_raw_view l2 v' = Some v''
using assms by (clarsimp simp add: focus_raw_compose_def make_focus_raw_via_view_modify_def)
  (meson focus_raw_compose_def bind_eq_Some_conv)

lemma focus_raw_view_composeE [focus_elims]:
  assumes focus_raw_view (focus_raw_compose l1 l2) v = Some v''
      and v'. focus_raw_view l1 v = Some v'  focus_raw_view l2 v' = Some v''  R
    shows R
using assms focus_raw_view_compose_destruct by metis

text‹Composition of focuses is associative, just like focuses:›
lemma focus_raw_compose_assoc:
  assumes is_valid_focus l1
      and is_valid_focus l2
      and is_valid_focus l3
    shows (l1 ⋄' l2) ⋄' l3 = l1 ⋄' (l2 ⋄' l3)
using assms by (auto simp add: focus_raw_compose_def make_focus_raw_via_view_modify_def
  focus_raw_modify_def elim!: is_valid_focusE intro!: ext) (metis (full_types) bind.bind_lunit
  option.collapse)

lemma focus_raw_view_lens_assoc:
  shows focus_raw_view (focus_raw_compose (lens_to_focus_raw l) f) v =
            focus_raw_view f (lens_view l v)
by (simp add: focus_raw_compose_def lens_to_focus_raw_def make_focus_raw_via_view_modify_def)

text ‹Similarly, there is also a notion of disjointedness for focuses.  Note that the laws governing
this are straightforward generalisations of the laws for disjoint focuses:›
definition disjoint_focus :: ('s, 'a) focus_raw  ('s, 'w) focus_raw  bool where
  disjoint_focus r1 r2  (b f g.
     focus_raw_modify r1 f (focus_raw_modify r2 g b) = focus_raw_modify r2 g (focus_raw_modify r1 f b) 
     focus_raw_view r1 (focus_raw_modify r2 g b) = focus_raw_view r1 b 
     focus_raw_view r2 (focus_raw_modify r1 f b) = focus_raw_view r2 b)

text ‹The following are technical introduction and elimination rules for working with disjoint
focuses in proofs:›
lemma disjoint_focus_raw_updateI [focus_intros]:
  assumes b f g. focus_raw_modify r1 f (focus_raw_modify r2 g b) = focus_raw_modify r2 g (focus_raw_modify r1 f b)
      and b f g. focus_raw_view r1 (focus_raw_modify r2 g b) = focus_raw_view r1 b
      and b f g. focus_raw_view r2 (focus_raw_modify r1 f b) = focus_raw_view r2 b
    shows disjoint_focus r1 r2
using assms by (auto simp add: disjoint_focus_def)

lemma disjoint_focusE [focus_elims]:
  assumes disjoint_focus r1 r2
      and b f g. focus_raw_modify r1 f (focus_raw_modify r2 g b) = focus_raw_modify r2 g (focus_raw_modify r1 f b) 
             focus_raw_view r1 (focus_raw_modify r2 g b) = focus_raw_view r1 b 
              focus_raw_view r2 (focus_raw_modify r1 f b) = focus_raw_view r2 b  R
    shows R
using assms by (auto simp add: disjoint_focus_def)

text‹The following definition intuitively captures that the given focus factors through the
(focus of the) prism associated to the given subset.›
abbreviation focus_raw_factors :: ('v set)  ('v, 'w) focus_raw  bool where
  focus_raw_factors P f  focus_raw_dom f  P

lemma focus_raw_dom_compose:
  shows focus_raw_dom (f0 ⋄' f1)  focus_raw_dom f0 
by (clarsimp simp add: focus_raw_dom_def focus_raw_compose_def make_focus_raw_via_view_modify_def
  bind_eq_Some_conv)

lemma prism_to_focus_raw_dom[simp]:
  shows focus_raw_dom (∫'p p) = prism_dom p
by (simp add: focus_raw_dom_def prism_dom_def prism_to_focus_raw_def)

definition factor_focus_through_prism :: ('v, 't) focus_raw  ('v, 'w) prism  ('w, 't) focus_raw where
  factor_focus_through_prism f p 
     let view   = λw. focus_raw_view f (prism_embed p w);
         update = λ(y::'t) (w::'w). the (prism_project p (focus_raw_update f y (prism_embed p w)))
      in make_focus_raw view update

lemma focus_raw_factors_prism_core:
    fixes p :: ('v, 'w) prism
      and f :: ('v, 't) focus_raw
  assumes is_valid_prism p
      and is_valid_focus f
      and focus_raw_dom f  prism_dom p
    shows let f' = factor_focus_through_prism f p in
            f = ∫'p p ⋄' f'
proof -
  let ?f'_view = λw. focus_raw_view f (prism_embed p w)
  let ?f'_update = λ(y :: 't) (w :: 'w). the (prism_project p (focus_raw_update f y (prism_embed p w)))
  let ?f' = make_focus_raw ?f'_view ?f'_update
  from focus_raw_dom f  prism_dom p have f = ∫'p p ⋄' ?f'
  proof -
  { fix x :: 'v
    have focus_raw_view f x = focus_raw_view (∫'p p ⋄' ?f') x
    proof -
    { assume x  prism_dom p
      moreover from this have x  focus_raw_dom f
        using focus_raw_factors (prism_dom p) f by auto
        ultimately have focus_raw_view f x = None and focus_raw_view (∫'p p ⋄' ?f') x = None
        apply (simp add: domIff focus_raw_dom_def)
        using x  prism_dom p focus_raw_dom_compose focus_raw_dom_def apply fastforce
        done
      then have ?thesis
        by simp 
    }
    moreover { 
      assume x  prism_dom p
      from this and is_valid_prism p obtain w where x = prism_embed p w
        using prism_domE' by metis
      from this and is_valid_prism p have ?thesis 
        by (simp add: focus_raw_compose_def is_valid_prism_def make_focus_raw_via_view_modify_def 
          prism_to_focus_raw_def) }
      ultimately show ?thesis 
        by auto
      qed
    }
    note A = this
    { fix y :: 't and x :: 'v
      have focus_raw_update f y x = focus_raw_update (∫'p p ⋄' ?f') y x
      proof -
      { assume x  prism_dom p
        then have x  focus_raw_dom f 
          using focus_raw_dom f  prism_dom p by blast
        from this and is_valid_focus f have focus_raw_update f y x = x  
          by (simp add: domIff focus_raw_dom_def focus_raw_modify_def is_valid_focus_def)
        moreover from x  prism_dom p have focus_raw_update (∫'p p ⋄' ?f') y x = x
          by (clarsimp simp add: prism_dom_def focus_raw_compose_def prism_to_focus_raw_def
            make_focus_raw_via_view_modify_def focus_raw_modify_def split!: option.splits)
        ultimately have ?thesis
          by auto 
      }
      moreover {
        assume x  prism_dom p and x  focus_raw_dom f
        from this and is_valid_prism p obtain w where x = prism_embed p w 
          using prism_domE' by metis
        moreover from assms and x  focus_raw_dom f have focus_raw_update f y x = x 
          by (simp add: assms(2) domIff focus_raw_dom_def is_valid_focus_def)
        ultimately have ?thesis
          using  is_valid_prism p by (clarsimp simp add: is_valid_prism_def focus_raw_compose_def 
            prism_to_focus_raw_def focus_raw_dom_def make_focus_raw_via_view_modify_def focus_raw_modify_def)
      } 
      moreover {
        assume x  focus_raw_dom f
        from this have x  prism_dom p 
          using focus_raw_dom f  prism_dom p by blast 
        moreover from x  focus_raw_dom f have focus_raw_update f y x  focus_raw_dom f
          by (clarsimp simp add: domIff focus_raw_dom_def) (meson assms(2) is_valid_focusE)
        moreover from this have focus_raw_update f y x  prism_dom p
          using focus_raw_dom f  prism_dom p  by blast 
        moreover from this and is_valid_prism p obtain w' where focus_raw_update f y x = prism_embed p w' 
          using prism_domE' by metis
        ultimately have ?thesis
          using  is_valid_prism p by (clarsimp simp add: is_valid_prism_def focus_raw_compose_def 
            prism_to_focus_raw_def focus_raw_dom_def make_focus_raw_via_view_modify_def focus_raw_modify_def
            split!: option.splits elim!: prism_domE) 
      }
      ultimately show ?thesis 
        by blast
      qed 
    }
    note B = this
    from A and B show ?thesis
      by (intro focus_raw.expand; safe; blast)
  qed
  from this show ?thesis 
    by (simp add: factor_focus_through_prism_def)
qed

text‹The following validates our intuition for ‹focus_raw_factors P f›: If ‹P = prism_dom p› for
some valid prism ‹p›, then indeed ‹focus_raw_factors P f› captures that ‹f› factors through
‹∫'p p›:›
lemma focus_raw_factors_prism:
    fixes p :: ('v, 'w) prism
      and f :: ('v, 't) focus_raw
  assumes is_valid_prism p
      and is_valid_focus f
    shows (focus_raw_dom f  prism_dom p)  (f' :: ('w, 't) focus_raw. f = ∫'p p ⋄' f')
proof -
  { fix f' :: ('w, 't) focus_raw 
    assume is_valid_focus f' and f = ∫'p p ⋄' f'
    then have focus_raw_dom f  prism_dom p 
      using focus_raw_dom_compose by force }
  moreover {
    assume focus_raw_dom f  prism_dom p
    then have (f' :: ('w, 't) focus_raw. f = ∫'p p ⋄' f') 
      by (meson assms focus_raw_factors_prism_core)
  }
  ultimately show ?thesis 
    by (metis focus_raw_dom_compose prism_to_focus_raw_dom)
qed

lemma focus_raw_factors_prism_update:
    fixes p :: ('v, 'w) prism
      and f :: ('v, 't) focus_raw
  assumes is_valid_prism p
      and is_valid_focus f
      and focus_raw_dom f  prism_dom p
    shows Some (focus_raw_update (factor_focus_through_prism f p) y x) = 
             prism_project p (focus_raw_update f y (prism_embed p x))
      and prism_embed p (focus_raw_update (factor_focus_through_prism f p) y x)
             = focus_raw_update f y (prism_embed p x)
proof -
  let ?f' = factor_focus_through_prism f p
  from focus_raw_factors_prism_core have 
    x. focus_raw_update (∫'p p ⋄' ?f') y x = focus_raw_update f y x
    using assms by fastforce
  from this have focus_raw_update (∫'p p ⋄' ?f') y (prism_embed p x) = focus_raw_update f y (prism_embed p x)
    by simp
  from this show Some (focus_raw_update (factor_focus_through_prism f p) y x) = 
             prism_project p (focus_raw_update f y (prism_embed p x))
    using is_valid_prism p apply (clarsimp simp add: is_valid_prism_def prism_to_focus_raw_def 
      focus_raw_compose_def make_focus_raw_via_view_modify_def focus_raw_modify_def split!: option.splits) 
    by (metis bind.bind_lunit domIff option.distinct(1) option.sel prism_dom_def)
  from this show prism_embed p (focus_raw_update (factor_focus_through_prism f p) y x)
             = focus_raw_update f y (prism_embed p x) 
    by (metis assms(1) is_valid_prism_def)
qed

lemma focus_raw_factors_prism_modify:
    fixes p :: ('v, 'w) prism
      and f :: ('v, 't) focus_raw
  assumes is_valid_prism p
      and is_valid_focus f
      and focus_raw_dom f  prism_dom p
    shows Some (focus_raw_modify (factor_focus_through_prism f p) g x) = 
             prism_project p (focus_raw_modify f g (prism_embed p x))
      and prism_embed p (focus_raw_modify (factor_focus_through_prism f p) g x)
             = focus_raw_modify f g (prism_embed p x)
  using assms by (auto simp add: focus_raw_modify_def focus_raw_factors_prism_update)
    (auto simp add: factor_focus_through_prism_def)

text‹If a focus factors through a prism, the factorization is unique:›
lemma focus_raw_factors_prism_unique:
    fixes f :: ('v, 't) focus_raw 
      and p :: ('v, 'w) prism
      and f' :: ('w, 't) focus_raw
  assumes is_valid_focus f
      and is_valid_prism p
      and f = ∫'p p ⋄' f'
    shows f' = factor_focus_through_prism f p (is _ = ?f'')
proof -
  let ?f'_view = λw. focus_raw_view f (prism_embed p w)
  have x. focus_raw_view f' x = ?f'_view x
  proof -
    fix x
    have Some x = prism_project p (prism_embed p x) 
      by (metis assms(2) is_valid_prism_def)
    moreover from this have Option.bind (Some x) (focus_raw_view f')
       = Option.bind (focus_raw_view (∫'p p) (prism_embed p x)) (focus_raw_view f') 
      by (simp add: prism_to_focus_raw_def)
    moreover from this and f = ∫'p p ⋄' f' have ... =  focus_raw_view f (prism_embed p x) 
      by (simp add: focus_raw_compose_def make_focus_raw_via_view_modify_def)
    ultimately show focus_raw_view f' x = ?f'_view x
      by (metis bind.bind_lunit)
  qed
  from this have focus_raw_view f' = focus_raw_view ?f'' 
    by (clarsimp simp add: factor_focus_through_prism_def intro!:ext)
  note A = this
  let ?f'_update = λ(y :: 't) (w :: 'w). the (prism_project p (focus_raw_update f y (prism_embed p w)))
  have x y. focus_raw_update f' y x = ?f'_update y x
  proof -
    fix x y
    have Some (focus_raw_update f' y x) = focus_raw_view (∫'p p) (prism_embed p (focus_raw_update f' y x))  
      using assms by (clarsimp simp add: prism_to_focus_raw_def is_valid_prism_def)
    moreover have ... = focus_raw_view (∫'p p) (focus_raw_modify (∫'p p) (focus_raw_update f' y) (prism_embed p x)) 
      using is_valid_prism p by (clarsimp simp add: is_valid_prism_def prism_to_focus_raw_def
        assms(2) focus_raw_modify_def prism_domI')
    moreover have ... = focus_raw_view (∫'p p) (focus_raw_update f y (prism_embed p x)) 
      using f = ∫'p p ⋄' f' by (simp add: focus_raw_compose_def focus_raw_modify_def 
        make_focus_raw_via_view_modify_components(2))
    ultimately have Some (focus_raw_update f' y x) = prism_project p (focus_raw_update f y (prism_embed p x))
      by (simp add: prism_to_focus_raw_def)
    from this show focus_raw_update f' y x = ?f'_update y x 
      by (metis option.sel)
  qed
  from this have focus_raw_update f' = focus_raw_update ?f''
    by (clarsimp simp add: factor_focus_through_prism_def intro!: ext)
  note B = this
  from A B show ?thesis 
    by (clarsimp simp add: focus_raw.expand) 
qed

text‹If a valid focus factors through a valid prism, the factorization is also a valid focus:›
lemma focus_raw_factors_prism_valid:
    fixes f :: ('v, 't) focus_raw 
      and p :: ('v, 'w) prism
      and f' :: ('w, 't) focus_raw
  assumes is_valid_focus f
      and is_valid_prism p
      and f = ∫'p p ⋄' f'
    shows is_valid_focus f' 
proof -
  from assms have eq: f' = factor_focus_through_prism f p 
    using focus_raw_factors_prism_unique by blast
  {
    fix x y
    have focus_raw_update f y (prism_embed p x)  prism_dom p  
      by (simp add: assms focus_raw_compose_def focus_raw_modify_def make_focus_raw_via_view_modify_def 
        prism_domI' prism_to_focus_raw_def)
    from this have eq': map_option (prism_embed p) (prism_project p (focus_raw_update f y (prism_embed p x))) =
              Some (focus_raw_update f y (prism_embed p x))
      by (metis (no_types, opaque_lifting) assms(2) is_valid_prism_def option.simps(9) prism_domE')
    have focus_raw_view f' (focus_raw_update f' y x) = Option.bind (Some (focus_raw_update f' y x)) (focus_raw_view f') 
      by simp
    also have  = Option.bind (prism_project p (focus_raw_update f y (prism_embed p x))) (focus_raw_view f') 
      using eq' by (clarsimp simp add: eq factor_focus_through_prism_def)
    also have ... = Option.bind (prism_project p (focus_raw_update f y (prism_embed p x)))
                           (focus_raw_view f  prism_embed p)  
      by (metis comp_apply eq factor_focus_through_prism_def focus_raw.sel(1))
    also have ... = Option.bind (map_option (prism_embed p) (prism_project p (focus_raw_update f y (prism_embed p x))))
                                 (focus_raw_view f) 
      by (simp add: bind_map_option)
    also from eq' have ... = Option.bind (Some (focus_raw_update f y (prism_embed p x))) (focus_raw_view f) 
      by force
    also have ... = focus_raw_view f (focus_raw_update f y (prism_embed p x)) 
      by simp
    also have ... = map_option (λ_. y) (focus_raw_view f (prism_embed p x))
      using assms(1) by (metis focus_raw_modify_def is_valid_focus_via_modifyE)
    finally have focus_raw_view f' (focus_raw_update f' y x) = map_option (λ_. y) (focus_raw_view f' x) 
      by (simp add: eq factor_focus_through_prism_def)
  }
  note A = this
  { 
    fix y x
    assume map_option (λ_. y) (focus_raw_view f' x) = focus_raw_view f' x
    then have map_option (λ_. y) (focus_raw_view f (prism_embed p x)) = focus_raw_view f (prism_embed p x)
      using is_valid_prism p by (clarsimp simp add: f = ∫'p p ⋄' f' focus_raw_compose_def 
        prism_to_focus_raw_def is_valid_prism_def make_focus_raw_via_view_modify_def) 
    from this have focus_raw_update f y (prism_embed p x) = prism_embed p x
      using is_valid_focus f is_valid_focus_def by (metis focus_raw_modify_def is_valid_focus_via_modify(2))
    from this have Some (focus_raw_update f' y x) = Some x 
      using is_valid_prism p 
      by (clarsimp simp add: is_valid_prism_def  eq factor_focus_through_prism_def)
    from this have focus_raw_update f' y x = x  
      by simp
  }
  note B = this
  { fix x y y'
    have Some (focus_raw_update f' y (focus_raw_update f' y' x)) = 
              prism_project p (focus_raw_update f y (prism_embed p (focus_raw_update f' y' x)))  
      by (metis assms eq focus_raw_dom_compose focus_raw_factors_prism_update(1) prism_to_focus_raw_dom)
    also have ... = prism_project p (focus_raw_update f y (focus_raw_update f y' (prism_embed p x))) 
      using assms eq focus_raw_dom_compose focus_raw_factors_prism_update(2) by fastforce
    also have ... = prism_project p (focus_raw_update f y (prism_embed p x)) 
      by (metis assms(1) is_valid_focusE not_Some_eq)
    also have ... = Some (focus_raw_update f' y x)
      by (metis assms eq focus_raw_dom_compose focus_raw_factors_prism_update(1) prism_to_focus_raw_dom)
    finally have focus_raw_update f' y (focus_raw_update f' y' x) = focus_raw_update f' y x 
      by force
  }  
  note C = this
  from A B C show ?thesis
    by (intro is_valid_focusI; clarsimp)
qed

lemma focus_raw_factors_prism_valid':
  assumes is_valid_prism p
      and is_valid_focus (∫'p p ⋄' f)
    shows is_valid_focus f
using assms focus_raw_factors_prism_valid by blast
  
text‹One can form the product of foci:›
definition pair_option :: 'a option × 'b option  ('a × 'b) option where
  pair_option t  case t of (Some x, Some y)  Some (x,y) | _  None

definition product_focus_raw :: ('a, 'b) focus_raw  ('c, 'd) focus_raw 
      ('a × 'c, 'b × 'd) focus_raw where
  product_focus_raw f0 f1  
     let view   = λ(x0,x1). pair_option (focus_raw_view f0 x0, focus_raw_view f1 x1);
         update = λ(y0,y1) (x0,x1). 
        ― ‹There's a pitfall here: we can't just update component-wise, because the axioms force
            us to do nothing in case the view is ‹None›.›
        case view (x0,x1) of None  (x0,x1)
           | _  (focus_raw_update f0 y0 x0, focus_raw_update f1 y1 x1)
      in make_focus_raw view update

lemma product_focus_raw_valid:
  assumes is_valid_focus f0
      and  is_valid_focus f1
    shows  is_valid_focus (product_focus_raw f0 f1)
using assms by (auto intro!: is_valid_focusI elim!: is_valid_focusE simp add: pair_option_def
  product_focus_raw_def Let_def   split!: option.splits)

subsection‹Type of valid foci›

subsubsection‹Definition›

typedef (overloaded) ('a, 'b) focus = { l :: ('a, 'b) focus_raw . is_valid_focus l }
  by (rule_tac x=dummy_focus in exI; clarsimp simp add: dummy_focus_is_valid)

setup_lifting type_definition_focus

instantiation focus :: (type,type)equal
begin

definition equal_focus :: ('a, 'b) focus  ('a, 'b) focus  bool where
  equal_focus f g  f = g

instance
proof
  fix x y :: ('a, 'b) focus
  show equal_class.equal x y  (x = y)
    by (auto simp add: equal_focus_def)
qed

end

lift_definition focus_view   :: ('a, 'b) focus  'a  'b option is focus_raw_view .
lift_definition focus_update :: ('a, 'b) focus  'b  'a  'a is focus_raw_update .
lift_definition focus_modify :: ('a, 'b) focus  ('b  'b)  'a  'a is focus_raw_modify .
lift_definition focus_dom    :: ('a, 'b) focus  'a set is focus_raw_dom .

abbreviation focus_is_view :: ('s, 'a) focus  's  'a  bool where
  focus_is_view f s a  focus_view f s = Some a

notation focus_is_view ("↓{_} _  _" [0,1000,59]59)
notation focus_update ("↑{_/ / _}" [59,59]59)
notation focus_modify ("∇{_}" [0]1000)

lemma focus_modify_def':
  shows focus_modify l f s  focus_update l (f (the (focus_view l s))) s
by (simp add: focus_modify.rep_eq focus_raw_modify_def focus_update.rep_eq focus_view.rep_eq)

lemma focus_laws_modify:
  shows f s. focus_view l (focus_modify l f s) = map_option f (focus_view l s)
    and f s. map_option f (focus_view l s) = focus_view l s  focus_modify l f s = s
    and f g s. focus_modify l f (focus_modify l g s) = focus_modify l (λx. f (g x)) s
by (transfer; elim is_valid_focus_via_modifyE; clarsimp)+

lemma focus_laws_update:
  shows (x y0 y1. focus_view l x = Some y0  focus_view l (focus_update l y1 x) = Some y1)
    and x y. focus_view l x = None   focus_view l (focus_update l y x) = None
    and x y. focus_view l x = Some y  focus_update l y x = x
    and x y. focus_view l x = None  focus_update l y x = x
    and x y0 y1 y2. focus_view l x = Some y0 
            focus_update l y2 (focus_update l y1 x) = focus_update l y2 x
by (transfer; elim is_valid_focusE; simp)+

lemmas focus_laws = focus_laws_update focus_laws_modify

lift_definition focus_compose:: ('a, 'b) focus  ('b, 'c) focus  ('a, 'c) focus (infixr "" 59)
  is λ(f0 :: ('a, 'b) focus_raw) (f1 :: ('b, 'c) focus_raw). focus_raw_compose f0 f1
by (simp add: focus_raw_compose_valid)

lemma focus_compose_components:
  shows focus_view (f0  f1) x = Option.bind (focus_view f0 x) (focus_view f1)
    and [focus_components]: focus_modify (f0  f1) f = focus_modify f0 (focus_modify f1 f)
    and [focus_components]: focus_update (f0  f1) y = focus_modify f0 (focus_modify f1 (λ_. y))
by (transfer; simp add: focus_raw_compose_components)+

lift_definition product_focus :: ('a, 'b) focus  ('c, 'd) focus  ('a × 'c, 'b × 'd) focus (infixr "×" 49)
  is product_focus_raw
by (simp add: product_focus_raw_valid)

lemma product_focus_components[focus_components]:
  shows focus_view (f0 × f1) (x0, x1) = pair_option (focus_view f0 x0, focus_view f1 x1)
    and focus_update (f0 × f1) (y0, y1) (x0, x1) =
        (case focus_view (f0 × f1) (x0, x1) of None  (x0,x1)
           | _  (focus_update f0 y0 x0, focus_update f1 y1 x1))
by (transfer; clarsimp simp add: product_focus_raw_def)+

lemma focus_compose_assoc[focus_simps]:
  shows f0  (f1  f2) = (f0  f1)  f2
by (transfer; simp add: focus_raw_compose_assoc)

lemma lens_to_focus_raw_components':
  assumes is_valid_lens l
    shows focus_view (Abs_focus (lens_to_focus_raw l)) x = Some (lens_view l x)
      and focus_update (Abs_focus (lens_to_focus_raw l)) = lens_update l
      and focus_modify (Abs_focus (lens_to_focus_raw l)) f v = lens_modify l f v
using assms by (auto simp add: eq_onp_same_args focus_view.abs_eq lens_to_focus_raw_components
  Abs_focus_inverse lens_to_focus_raw_valid focus_update.rep_eq focus_modify.abs_eq)

lemma prism_to_focus_components':
  assumes is_valid_prism p
    shows focus_view (Abs_focus (prism_to_focus_raw p)) = prism_project p
      and focus_update (Abs_focus (prism_to_focus_raw p)) y x = 
              (if x  prism_dom p then prism_embed p y else x)
      and focus_modify (Abs_focus (prism_to_focus_raw p)) f x =
              (if x  prism_dom p then prism_embed p (f (the (prism_project p x))) else x)
using assms by (auto simp add: eq_onp_same_args focus_view.abs_eq prism_to_focus_raw_components
  prism_to_focus_raw_valid Abs_focus_inverse focus_update.rep_eq focus_modify.abs_eq
  prism_dom_def domIff)

context
    fixes l :: ('a, 'b) lens
  assumes is_valid_lens l
begin

lift_definition lens_to_focus :: ('a, 'b) focus is lens_to_focus_raw l 
by (simp add: is_valid_lens l lens_to_focus_raw_valid)

lemma lens_to_focus_components:
  shows focus_view lens_to_focus = Some  lens_view l
    and focus_update (lens_to_focus) = lens_update l
    and focus_modify (lens_to_focus) = lens_modify l
by (auto intro!: ext simp add: is_valid_lens l lens_to_focus.abs_eq lens_to_focus_raw_components')

end

context
    fixes p :: ('a, 'b) prism
  assumes is_valid_prism p
begin

lift_definition prism_to_focus :: ('a, 'b) focus is prism_to_focus_raw p 
by (simp add: is_valid_prism p prism_to_focus_raw_valid)

lemma prism_to_focus_components:
  shows [focus_components]: focus_view prism_to_focus = prism_project p
    and focus_update prism_to_focus y x = 
            (if x  prism_dom p then prism_embed p y else x)
    and focus_modify prism_to_focus f x =
            (if x  prism_dom p then prism_embed p (f (the (prism_project p x))) else x)
by (auto intro!: ext simp add: is_valid_prism p prism_to_focus.abs_eq prism_to_focus_components')

lemma prism_to_focus_dom[focus_components]:
  shows focus_dom prism_to_focus = prism_dom p
by transfer (auto simp add: focus_raw_dom_def prism_dom_def prism_to_focus_raw_components)

end

notation lens_to_focus ("l")
notation prism_to_focus ("p")

text‹The following definition intuitively captures that the given focus factors through the
(focus of the) prism associated to the given subset.›
abbreviation focus_factors :: ('v set)  ('v, 'w) focus  bool where
  focus_factors P f  focus_dom f  P

lemma focus_factors_modify:
  assumes focus_factors P f
    shows v g. v  P  focus_modify f g v  P 
using assms by transfer (metis focus_raw_domI focus_raw_modify_def in_mono is_valid_focus_def
  option.collapse)

lemma focus_factors_trans[focus_intros]:
  assumes focus_factors P f
    shows focus_factors P (f  g) 
using assms by transfer (meson dual_order.trans focus_raw_dom_compose)

subsubsection‹Examples›

text‹The identity focus:›
lift_definition focus_id :: ('v, 'v) focus ("id") is make_focus_raw Some (λy _. y) 
by (metis unit_focus_raw_def unit_focus_raw_valid)

lemma focus_id_components[focus_components]:
  shows focus_view focus_id = Some
    and focus_update focus_id y x = y
by (transfer, clarsimp)+

text‹The point/zero focus›
lift_definition focus_zero :: ('v, unit) focus ("0")
  is make_focus_raw (λ_. Some ()) (λ_. id)
by (simp add: is_valid_focusI)

lemma focus_zero_components[focus_components]:
  shows focus_view focus_zero = (λ_. Some ())
    and focus_update focus_zero y = id 
by (transfer, clarsimp)+

text‹Projection foci›

lift_definition focus_fst :: ('a × 'b, 'a) focus ("fst") is ∫'l lens_fst 
  by (simp add: lens_fst_is_valid_lensI lens_to_focus_raw_valid)
lift_definition focus_snd :: ('a × 'b, 'b) focus ("snd") is ∫'l lens_snd 
  by (simp add: lens_snd_is_valid_lensI lens_to_focus_raw_valid)

text‹Use eta expansion during code generation to avoid ML value restriction›
definition focus_fst_lazy (uu :: unit) = focus_fst
declare focus_fst_lazy_def[of (), symmetric, code_unfold]
declare focus_fst_lazy_def[THEN  arg_cong[where f="Rep_focus"], simplified focus_fst.rep_eq, code]

definition focus_snd_lazy (uu :: unit) = focus_snd
declare focus_snd_lazy_def[of (), symmetric, code_unfold]
declare focus_snd_lazy_def[THEN  arg_cong[where f="Rep_focus"], simplified focus_snd.rep_eq, code]

lemma focus_fst_snd_components[focus_components]:
  shows focus_view focus_fst (x,y) = Some x
    and focus_view focus_snd (x,y) = Some y
    and focus_update focus_fst x (x0,y0) = (x,y0)
    and focus_update focus_snd y (x0,y0) = (x0,y)
by (transfer; clarsimp simp add: lens_to_focus_raw_components;
    clarsimp simp add: lens_fst_def lens_snd_def)+

lift_definition option_focus :: ('v option, 'v) focus
  is make_focus_raw (λx. x) (λy x. Option.bind x (λ_. Some y))
by (auto simp add: option.map_comp Fun.comp_def is_valid_focus_def focus_raw_update_def)

lemma option_focus_components[focus_components]:
  shows focus_view option_focus = id
    and focus_update option_focus y x = Option.bind x (λ_. Some y)
by (transfer, auto)+

lemma focus_view_modify:
  shows focus_view l (focus_modify l f s) = map_option f (focus_view l s)
by (auto simp add: focus_laws)

lemma focus_view_update:
  shows focus_view l (focus_update l y s) = map_option (λ_. y) (focus_view l s)
by (metis focus_laws_modify(1) focus_modify_def')

subsection‹Automation setup›

text‹In this section, we single out specific formulations of the focus laws which are suitable
for proof automation, marking them as ‹focus_simps› or ‹focus_intros› as appropriate:›

lemma focus_modify_compose [focus_simps]:
  shows focus_modify l f (focus_modify l g s) = focus_modify l (λx. f (g x)) s
by (auto simp add: focus_laws)

lemma focus_modify_localI[focus_intros]:
  assumes focus_is_view l s t
      and f t = g t
    shows focus_modify l f s = focus_modify l g s
using assms by (simp add: focus_modify_def')

text ‹Modifying a valid focus with a degenerate update function, which merely returns the contents
of the field, has no effect:›
lemma focus_modify_selfI [focus_intros]:
  assumes focus_is_view f g v
    shows focus_modify f (λ_. v) g = g
by (simp add: assms focus_laws_modify)

lemma focus_update_selfI [focus_intros]:
  assumes focus_is_view f g v
    shows focus_update f v g = g
by (simp add: assms focus_laws_update)

lemma focus_update_selfI':
  assumes focus_is_view f g v
      and v = v'
    shows focus_update f v' g = g
by (simp add: assms focus_laws_update)

declare focus_update_selfI'[focus_intros]
declare focus_update_selfI'[symmetric, focus_intros]

lemma focus_modify_selfI':
  assumes focus_is_view l s t
      and f t = t
    shows focus_modify l f s = s
by (simp add: assms focus_laws_modify)

declare focus_modify_selfI'[focus_intros]
declare focus_modify_selfI'[symmetric, focus_intros]

text‹The following two versions of ‹focus_raw_view_modify› would work for weaker focus axioms 
not predescribing any behavior of ‹focus_raw_modify l f› on elements outside of the domain of the
focus:›
lemma focus_view_modify':
  assumes focus_is_view l s t
    shows focus_is_view l (focus_modify l f s) (f t)
using assms by (simp add: focus_view_modify)

lemma focus_raw_view_modify'I[focus_rules]:
  assumes focus_is_view l s t
      and t' = f t
    shows focus_is_view l (focus_modify l f s) t'
using assms by (simp add: focus_view_modify)

lemma focus_raw_view_update'I[focus_rules]:
  assumes focus_is_view l s t
      and t' = y
    shows focus_is_view l (focus_update l y s) t'
using assms by (simp add: focus_laws_update)

lemma focus_compose_is_view[focus_intros]:
  assumes focus_is_view f0 x y
      and focus_is_view f1 y z
    shows focus_is_view (f0  f1) x z
using assms by transfer (simp add: focus_raw_compose_components)

lemma focus_is_view_modify_partial[focus_intros]:
  assumes focus_is_view f0 x y'
      and f0 = f0'
      and y = focus_modify f1 op y'
    shows focus_is_view f0 (focus_modify (f0'  f1) op x) y
using assms by transfer (simp add: focus_raw_compose_components(2) focus_raw_laws_update(1)
  focus_raw_modify_def)

text‹Make this ‹focus_elim› to avoid build-up of redundant hypotheses?›
lemma focus_compose_view_dropE:
  assumes focus_is_view (f0  f1) (focus_modify f2 op x) y
      and R
    shows R
using assms by simp

lemma focus_is_view_elim:
  assumes focus_is_view l (focus_modify l op x) y
      and y'. focus_is_view l x y'  y = op y'  R
    shows R
using assms by (metis focus_laws_update(2) focus_modify_def' focus_raw_view_modify'I option.collapse
  option.simps(1))

text‹This should be added to ‹focus_intros› after specialization for a particular prism:›
lemma prism_to_focus_modify_update:
  assumes is_valid_prism p
      and prism_project p x = Some y
    shows focus_update (prism_to_focus p) y x = prism_embed p y
      and focus_modify (prism_to_focus p) f x = prism_embed p (f y)
using assms by (auto simp add: prism_to_focus_components prism_dom_def)

(*<*)
end
(*>*)