Theory Optics.Scenes

section ‹ Scenes ›

theory Scenes
  imports Lens_Symmetric
begin

text ‹ Like lenses, scenes characterise a region of a source type. However, unlike lenses, scenes
  do not explicitly assign a view type to this region, and consequently they have just one type
  parameter. This means they can be more flexibly composed, and in particular it is possible to
  show they form nice algebraic structures in Isabelle/HOL. They are mainly of use in characterising
  sets of variables, where, of course, we do not care about the types of those variables and
  therefore representing them as lenses is inconvenient. ›

subsection ‹ Overriding Functions ›

text ‹ Overriding functions provide an abstract way of replacing a region of an existing source
  with the corresponding region of another source. ›

locale overrider =
  fixes F  :: "'s ⇒ 's ⇒ 's" (infixl ‹▹› 65)
  assumes 
    ovr_overshadow_left: "x ▹ y ▹ z = x ▹ z" and
    ovr_overshadow_right: "x ▹ (y ▹ z) = x ▹ z"
begin
  lemma ovr_assoc: "x ▹ (y ▹ z) = x ▹ y ▹ z"
    by (simp add: ovr_overshadow_left ovr_overshadow_right)
end

locale idem_overrider = overrider +
  assumes ovr_idem: "x ▹ x = x"

declare overrider.ovr_overshadow_left [simp]
declare overrider.ovr_overshadow_right [simp]
declare idem_overrider.ovr_idem [simp]

subsection ‹ Scene Type ›

typedef 's scene = "{F :: 's ⇒ 's ⇒ 's. overrider F}"
  by (rule_tac x="λ x y. x" in exI, simp, unfold_locales, simp_all)

setup_lifting type_definition_scene

lift_definition idem_scene :: "'s scene ⇒ bool" is idem_overrider .

lift_definition region :: "'s scene ⇒ 's rel" 
is "λ F. {(s1, s2). (∀ s. F s s1 = F s s2)}" .

lift_definition coregion :: "'s scene ⇒ 's rel" 
is "λ F. {(s1, s2). (∀ s. F s1 s = F s2 s)}" .

lemma equiv_region: "equiv UNIV (region X)"
  apply (transfer)
  apply (rule equivI)
    apply (rule refl_onI)
     apply (auto)
   apply (rule symI)
   apply (auto)
  apply (rule transI)
  apply (auto)
  done

lemma equiv_coregion: "equiv UNIV (coregion X)"
  apply (transfer)
  apply (rule equivI)
    apply (rule refl_onI)
     apply (auto)
   apply (rule symI)
   apply (auto)
  apply (rule transI)
  apply (auto)
  done

lemma region_coregion_Id:
  "idem_scene X ⟹ region X ∩ coregion X = Id"
  by (transfer, auto, metis idem_overrider.ovr_idem)

lemma state_eq_iff: "idem_scene S ⟹ x = y ⟷ (x, y) ∈ region S ∧ (x, y) ∈ coregion S"
  by (metis IntE IntI pair_in_Id_conv region_coregion_Id)

lift_definition scene_override :: "'a ⇒ 'a ⇒ ('a scene) ⇒ 'a" (‹_ ⊕S _ on _› [95,0,96] 95)
is "λ s1 s2 F. F s1 s2" .

abbreviation (input) scene_copy :: "'a scene ⇒ 'a ⇒ ('a ⇒ 'a)" (‹cp⇘_⇙›) where
"cp⇘A⇙ s ≡ (λ s'. s' ⊕S s on A)"

lemma scene_override_idem [simp]: "idem_scene X ⟹ s ⊕S s on X = s"
  by (transfer, simp)

lemma scene_override_overshadow_left [simp]:
  "S1 ⊕S S2 on X ⊕S S3 on X = S1 ⊕S S3 on X"
  by (transfer, simp)

lemma scene_override_overshadow_right [simp]:
  "S1 ⊕S (S2 ⊕S S3 on X) on X = S1 ⊕S S3 on X"
  by (transfer, simp)

definition scene_equiv :: "'a ⇒ 'a ⇒ ('a scene) ⇒ bool" (‹_ ≈S _ on _› [65,0,66] 65) where
[lens_defs]: "S1 ≈S S2 on X = (S1 ⊕S S2 on X = S1)"

lemma scene_equiv_region: "idem_scene X ⟹ region X = {(S1, S2). S1 ≈S S2 on X}"
  by (simp add: lens_defs, transfer, auto)
     (metis idem_overrider.ovr_idem, metis overrider.ovr_overshadow_right)

lift_definition scene_indep :: "'a scene ⇒ 'a scene ⇒ bool" (infix ‹⨝S› 50)
is "λ F G. (∀ s1 s2 s3. G (F s1 s2) s3 = F (G s1 s3) s2)" .

lemma scene_indep_override:
  "X ⨝S Y = (∀ s1 s2 s3. s1 ⊕S s2 on X ⊕S s3 on Y = s1 ⊕S s3 on Y ⊕S s2 on X)"
  by (transfer, auto)

lemma scene_indep_copy:
  "X ⨝S Y = (∀ s1  s2. cp⇘X⇙ s1 ∘ cp⇘Y⇙ s2 = cp⇘Y⇙ s2 ∘ cp⇘X⇙ s1)"
  by (auto simp add: scene_indep_override comp_def fun_eq_iff)

lemma scene_indep_sym:
  "X ⨝S Y ⟹ Y ⨝S X"
  by (transfer, auto)  

text ‹ Compatibility is a weaker notion than independence; the scenes can overlap but they must
  agree when they do. ›

lift_definition scene_compat :: "'a scene ⇒ 'a scene ⇒ bool" (infix ‹##S› 50)
is "λ F G. (∀ s1 s2. G (F s1 s2) s2 = F (G s1 s2) s2)" .

lemma scene_compat_copy:
  "X ##S Y = (∀ s. cp⇘X⇙ s ∘ cp⇘Y⇙ s = cp⇘Y⇙ s ∘ cp⇘X⇙ s)"
  by (transfer, auto simp add: fun_eq_iff)

lemma scene_indep_compat [simp]: "X ⨝S Y ⟹ X ##S Y"
  by (transfer, auto)

lemma scene_compat_refl: "X ##S X"
  by (transfer, simp)

lemma scene_compat_sym: "X ##S Y ⟹ Y ##S X"
  by (transfer, simp)

lemma scene_override_commute_indep:
  assumes "X ⨝S Y"
  shows "S1 ⊕S S2 on X ⊕S S3 on Y = S1 ⊕S S3 on Y ⊕S S2 on X"
  using assms
  by (transfer, auto)

instantiation scene :: (type) "{bot, top, uminus, sup, inf}"
begin
  lift_definition bot_scene    :: "'a scene" is "λ x y. x" by (unfold_locales, simp_all)
  lift_definition top_scene    :: "'a scene" is "λ x y. y" by (unfold_locales, simp_all)
  lift_definition uminus_scene :: "'a scene ⇒ 'a scene" is "λ F x y. F y x"
    by (unfold_locales, simp_all)
  text ‹ Scene union requires that the two scenes are at least compatible. If they are not, the
        result is the bottom scene. ›
  lift_definition sup_scene :: "'a scene ⇒ 'a scene ⇒ 'a scene" 
    is "λ F G. if (∀ s1 s2. G (F s1 s2) s2 = F (G s1 s2) s2) then (λ s1 s2. G (F s1 s2) s2) else (λ s1 s2. s1)"
    by (unfold_locales, auto, metis overrider.ovr_overshadow_right)
  definition inf_scene :: "'a scene ⇒ 'a scene ⇒ 'a scene" where
    [lens_defs]: "inf_scene X Y = - (sup (- X) (- Y))"
  instance ..
end

abbreviation union_scene :: "'s scene ⇒ 's scene ⇒ 's scene" (infixl ‹⊔S› 65)
where "union_scene ≡ sup"

abbreviation inter_scene :: "'s scene ⇒ 's scene ⇒ 's scene" (infixl ‹⊓S› 70)
where "inter_scene ≡ inf"

abbreviation top_scene :: "'s scene" (‹⊤S›)
where "top_scene ≡ top"

abbreviation bot_scene :: "'s scene" (‹⊥S›)
where "bot_scene ≡ bot"

instantiation scene :: (type) "minus"
begin
  definition minus_scene :: "'a scene ⇒ 'a scene ⇒ 'a scene" where
    "minus_scene A B = A ⊓S (- B)"
instance ..
end

lemma bot_idem_scene [simp]: "idem_scene ⊥S"
  by (transfer, unfold_locales, simp_all)

lemma top_idem_scene [simp]: "idem_scene ⊤S"
  by (transfer, unfold_locales, simp_all)

lemma uminus_top_scene [simp]: "- ⊤S = ⊥S"
  by (transfer, simp)

lemma uminus_bot_scene [simp]: "- ⊥S = ⊤S"
  by (transfer, simp)

lemma uminus_scene_twice: "- (- (X :: 's scene)) = X"
  by (transfer, simp)

lemma scene_override_id [simp]: "S1 ⊕S S2 on ⊤S = S2"
  by (transfer, simp)

lemma scene_override_unit [simp]: "S1 ⊕S S2 on ⊥S = S1"
  by (transfer, simp)

lemma scene_override_commute: "S2 ⊕S S1 on (- X) = S1 ⊕S S2 on X"
  by (transfer, simp)

lemma scene_union_incompat: "¬ X ##S Y ⟹ X ⊔S Y = ⊥S"
  by (transfer, auto)

lemma scene_override_union: "X ##S Y ⟹ S1 ⊕S S2 on (X ⊔S Y) = (S1 ⊕S S2 on X) ⊕S S2 on Y"
  by (transfer, auto)

lemma scene_override_inter: "-X ##S -Y ⟹ S1 ⊕S S2 on (X ⊓S Y) = S1 ⊕S S1 ⊕S S2 on X on Y"
  by (simp add: inf_scene_def scene_override_commute scene_override_union)

lemma scene_equiv_bot [simp]: "a ≈S b on ⊥S"
  by (simp add: scene_equiv_def)

lemma scene_equiv_refl [simp]: "idem_scene a ⟹ s ≈S s on a"
  by (simp add: scene_equiv_def)

lemma scene_equiv_sym [simp]: "idem_scene a ⟹ s1 ≈S s2 on a ⟹ s2 ≈S s1 on a"
  by (metis scene_equiv_def scene_override_idem scene_override_overshadow_right)

lemma scene_union_unit [simp]: "X ⊔S ⊥S = X" "⊥S ⊔S X = X"
  by (transfer, simp)+

lemma scene_indep_bot [simp]: "X ⨝S ⊥S"
  by (transfer, simp)

text ‹ A unitary scene admits only one element, and therefore top and bottom are the same. ›

lemma unit_scene_top_eq_bot: "(⊥S :: unit scene) = ⊤S"
  by (transfer, simp)

lemma idem_scene_union [simp]: "⟦ idem_scene A; idem_scene B ⟧ ⟹ idem_scene (A ⊔S B)"
  apply (transfer, auto)
   apply (unfold_locales, auto)
   apply (metis overrider.ovr_overshadow_left)
  apply (metis overrider.ovr_overshadow_right)
  done

lemma scene_union_annhil: "idem_scene X ⟹ X ⊔S ⊤S = ⊤S"
  by (transfer, simp)

lemma scene_union_pres_compat: "⟦ A ##S B; A ##S C ⟧ ⟹ A ##S (B ⊔S C)"
  by (transfer, auto)

lemma scene_indep_pres_compat: "⟦ A ⨝S B; A ⨝S C ⟧ ⟹ A ⨝S (B ⊔S C)"
  by (transfer, auto)

lemma scene_indep_self_compl: "A ⨝S -A"
  by (transfer, simp)

lemma scene_compat_self_compl: "A ##S -A"
  by (transfer, simp)

lemma scene_compat_bot [simp]: "a ##S ⊥S" "⊥S ##S a"
  by (transfer, simp)+

lemma scene_compat_top [simp]: 
  "idem_scene a ⟹ a ##S ⊤S" 
  "idem_scene a ⟹ ⊤S ##S a"
  by (transfer, simp)+

lemma scene_union_assoc: 
  assumes "X ##S Y" "X ##S Z" "Y ##S Z"
  shows "X ⊔S (Y ⊔S Z) = (X ⊔S Y) ⊔S Z"
  using assms by (transfer, auto)

lemma scene_inter_indep:
  assumes "idem_scene X" "idem_scene Y" "X ⨝S Y"
  shows "X ⊓S Y = ⊥S"
  using assms
  unfolding lens_defs
  apply (transfer, auto)
   apply (metis (no_types, opaque_lifting) idem_overrider.ovr_idem overrider.ovr_assoc overrider.ovr_overshadow_right)
  apply (metis (no_types, opaque_lifting) idem_overrider.ovr_idem overrider.ovr_overshadow_right)
  done

lemma scene_union_indep_uniq:
  assumes "idem_scene X" "idem_scene Y" "idem_scene Z" "X ⨝S Z" "Y ⨝S Z" "X ⊔S Z = Y ⊔S Z"
  shows "X = Y"
  using assms apply (transfer, simp)
  by (metis (no_types, opaque_lifting) ext idem_overrider.ovr_idem overrider_def)

lemma scene_union_idem: "X ⊔S X = X"
  by (transfer, simp)

lemma scene_union_compl: "idem_scene X ⟹ X ⊔S - X = ⊤S"
  by (transfer, auto)

lemma scene_inter_idem: "X ⊓S X = X"
  by (simp add: inf_scene_def, transfer, auto)

lemma scene_union_commute: "X ⊔S Y = Y ⊔S X"
  by (transfer, auto)

lemma scene_inter_compl: "idem_scene X ⟹ X ⊓S - X = ⊥S"
  by (simp add: inf_scene_def, transfer, auto)

lemma scene_demorgan1: "-(X ⊔S Y) = -X ⊓S -Y"
  by (simp add: inf_scene_def, transfer, auto)

lemma scene_demorgan2: "-(X ⊓S Y) = -X ⊔S -Y"
  by (simp add: inf_scene_def, transfer, auto)

lemma scene_inter_commute: "X ⊓S Y = Y ⊓S X"
  by (simp add: inf_scene_def scene_union_commute)

lemma scene_union_inter_distrib:
  "⟦ idem_scene x; x ⨝S y; x ⨝S z; y ##S z ⟧ ⟹ x ⊔S y ⊓S z = (x ⊔S y) ⊓S (x ⊔S z)"
  apply (simp add: inf_scene_def, transfer)
  apply (auto simp add: fun_eq_iff)
     apply (unfold overrider_def idem_overrider_def idem_overrider_axioms_def)
     apply metis+
  done  

lemma idem_scene_uminus [simp]: "idem_scene X ⟹ idem_scene (- X)"
  by (simp add: uminus_scene_def idem_scene_def Abs_scene_inverse idem_overrider_axioms_def idem_overrider_def overrider.intro)

lemma scene_minus_cancel: "⟦ a ⨝S b; idem_scene a; idem_scene b ⟧ ⟹ a ⊔S (b ⊓S - a) = a ⊔S b"
  apply (simp add: lens_defs, transfer, auto simp add: fun_eq_iff)
   apply (metis (mono_tags, lifting) overrider.ovr_overshadow_left)
  apply (metis (no_types, opaque_lifting) idem_overrider.ovr_idem overrider.ovr_overshadow_right)
  done

instantiation scene :: (type) ord
begin
  text ‹ $X$ is a subscene of $Y$ provided that overriding with first $Y$ and then $X$ can
         be rewritten using the complement of $X$. ›
  definition less_eq_scene :: "'a scene ⇒ 'a scene ⇒ bool" where
  [lens_defs]: "less_eq_scene X Y = (∀ s1 s2 s3. s1 ⊕S s2 on Y ⊕S s3 on X = s1 ⊕S (s2 ⊕S s3 on X) on Y)"
  definition less_scene :: "'a scene ⇒ 'a scene ⇒ bool" where
  [lens_defs]: "less_scene x y = (x ≤ y ∧ ¬ y ≤ x)"
instance ..
end

abbreviation subscene :: "'a scene ⇒ 'a scene ⇒ bool" (infix ‹⊆S› 55)
where "subscene X Y ≡ X ≤ Y"

lemma subscene_refl: "X ⊆S X"
  by (simp add: less_eq_scene_def)

lemma subscene_trans: "⟦ idem_scene Y; X ⊆S Y; Y ⊆S Z ⟧ ⟹ X ⊆S Z"
  by (simp add: less_eq_scene_def, transfer, auto, metis (no_types, opaque_lifting) idem_overrider.ovr_idem)

lemma subscene_antisym: "⟦ idem_scene Y; X ⊆S Y; Y ⊆S X ⟧ ⟹ X = Y"
  apply (simp add: less_eq_scene_def, transfer, auto)
  apply (rule ext)
  apply (rule ext)
  apply (metis (full_types) idem_overrider.ovr_idem overrider.ovr_overshadow_left)
  done

lemma subscene_copy_def:
  assumes "idem_scene X" "idem_scene Y"
  shows "X ⊆S Y = (∀ s1 s2. cp⇘X⇙ s1 ∘ cp⇘Y⇙ s2 = cp⇘Y⇙ (cp⇘X⇙ s1 s2))"
  using assms
  by (simp add: less_eq_scene_def fun_eq_iff, transfer, auto)

lemma subscene_eliminate:
  "⟦ idem_scene Y; X ≤ Y ⟧ ⟹ s1 ⊕S s2 on X ⊕S s3 on Y = s1 ⊕S s3 on Y"
  by (metis less_eq_scene_def scene_override_overshadow_left scene_override_idem)
    
lemma scene_bot_least: "⊥S ≤ X"
  unfolding less_eq_scene_def by (transfer, auto)

lemma scene_top_greatest: "X ≤ ⊤S"
  unfolding less_eq_scene_def by (transfer, auto)

lemma scene_union_ub: "⟦ idem_scene Y; X ⨝S Y ⟧ ⟹ X ≤ (X ⊔S Y)"
  by (simp add: less_eq_scene_def, transfer, auto)
     (metis (no_types, opaque_lifting) idem_overrider.ovr_idem overrider.ovr_overshadow_right)

lemma scene_union_lb: "⟦ a ##S b; a ≤ c; b ≤ c ⟧ ⟹ a ⊔S b ≤ c"
  by (simp add: less_eq_scene_def scene_override_union)

lemma scene_union_mono: "⟦ a ⊆S c; b ⊆S c; a ##S b; idem_scene a; idem_scene b ⟧ ⟹ a ⊔S b ⊆S c"
  by (simp add: less_eq_scene_def, transfer, auto)

lemma scene_le_then_compat: "⟦ idem_scene X; idem_scene Y; X ≤ Y ⟧ ⟹ X ##S Y"
  unfolding less_eq_scene_def
  by (transfer, auto, metis (no_types, lifting) idem_overrider.ovr_idem overrider_def)

lemma indep_then_compl_in: "A ⨝S B ⟹ A ≤ -B"
  unfolding less_eq_scene_def by (transfer, simp)

lemma scene_le_iff_indep_inv:
  "A ⨝S - B ⟷ A ≤ B"
  by (auto simp add: less_eq_scene_def scene_indep_override scene_override_commute)

lift_definition scene_comp :: "'a scene ⇒ ('a ⟹ 'b) ⇒ 'b scene" (infixl ‹;S› 80)
is "λ S X a b. if (vwb_lens X) then put⇘X⇙ a (S (get⇘X⇙ a) (get⇘X⇙ b)) else a"
  by (unfold_locales, auto)

lemma scene_comp_idem [simp]: "idem_scene S ⟹ idem_scene (S ;S X)"
  by (transfer, unfold_locales, simp_all)

lemma scene_comp_lens_indep [simp]: "X ⨝ Y ⟹ (A ;S X) ⨝S (A ;S Y)"
  by (transfer, auto simp add: lens_indep.lens_put_comm lens_indep.lens_put_irr2)

lemma scene_comp_indep [simp]: "A ⨝S B ⟹ (A ;S X) ⨝S (B ;S X)"
  by (transfer, auto)

lemma scene_comp_bot [simp]: "⊥S ;S x = ⊥S"
  by (transfer, auto)

lemma scene_comp_id_lens [simp]: "A ;S 1L = A"
  by (transfer, auto, simp add: id_lens_def)

lemma scene_union_comp_distl: "a ##S b ⟹ (a ⊔S b) ;S x = (a ;S x) ⊔S (b ;S x)"
  by (transfer, auto simp add: fun_eq_iff)

lemma scene_comp_assoc: "⟦ vwb_lens X; vwb_lens Y ⟧ ⟹ A ;S X ;S Y = A ;S (X ;L Y)"
  by (transfer, auto simp add: lens_comp_def fun_eq_iff)
     (metis comp_vwb_lens lens_comp_def)

lift_definition scene_quotient :: "'b scene ⇒ ('a ⟹ 'b) ⇒ 'a scene" (infixl ‹'/S› 80)
is "λ S X a b. if (vwb_lens X ∧ (∀s1 s2 s3. S (s1 ◃⇘X⇙ s2) s3 = s1 ◃⇘X⇙ S s2 s3)) then get⇘X⇙ (S (create⇘X⇙ a) (create⇘X⇙ b)) else a"
  by (unfold_locales, auto simp add: lens_create_def lens_override_def)
     (metis (no_types, lifting) overrider.ovr_overshadow_right)

lemma scene_quotient_idem: "idem_scene S ⟹ idem_scene (S /S X)"
  by (transfer, unfold_locales, auto simp add: lens_create_def lens_override_def)
     (metis (no_types, lifting) overrider.ovr_overshadow_right) 

lemma scene_quotient_indep: "A ⨝S B ⟹ (A /S X) ⨝S (B /S X)"
  by (transfer, auto simp add: lens_create_def lens_override_def)

lemma scene_bot_quotient [simp]: "⊥S /S X = ⊥S"
  by (transfer, auto)

lemma scene_comp_quotient: "vwb_lens X ⟹ (A ;S X) /S X = A"
  by (transfer, auto simp add: fun_eq_iff lens_override_def)

lemma scene_quot_id_lens [simp]: "(A /S 1L) = A"
  by (transfer, simp, simp add: lens_defs)

subsection ‹ Linking Scenes and Lenses ›

text ‹ The following function extracts a scene from a very well behaved lens ›

lift_definition lens_scene :: "('v ⟹ 's) ⇒ 's scene" (‹⟦_⟧∼›) is
"λ X s1 s2. if (mwb_lens X) then s1 ⊕L s2 on X else s1"
  by (unfold_locales, auto simp add: lens_override_def)

lemma vwb_impl_idem_scene [simp]:
  "vwb_lens X ⟹ idem_scene ⟦X⟧∼"
  by (transfer, unfold_locales, auto simp add: lens_override_overshadow_left lens_override_overshadow_right)

lemma idem_scene_impl_vwb:
  "⟦ mwb_lens X; idem_scene ⟦X⟧∼ ⟧ ⟹ vwb_lens X"
  apply (cases "mwb_lens X")
   apply (transfer, unfold idem_overrider_def overrider_def, auto)
  apply (simp add: idem_overrider_axioms_def override_idem_implies_vwb)
  done

lemma lens_compat_scene: "⟦ mwb_lens X; mwb_lens Y ⟧ ⟹ X ##L Y ⟷ ⟦X⟧∼ ##S ⟦Y⟧∼"
  by (auto simp add: lens_scene.rep_eq scene_compat.rep_eq lens_defs)

text ‹ Next we show some important congruence properties ›

lemma zero_lens_scene: "⟦0L⟧∼ = ⊥S"
  by (transfer, simp)

lemma one_lens_scene: "⟦1L⟧∼ = ⊤S"
  by (transfer, simp)

lemma scene_comp_top_scene [simp]: "vwb_lens x ⟹ ⊤S ;S x = ⟦x⟧∼"
  by (transfer, simp add: fun_eq_iff lens_override_def)

lemma scene_comp_lens_scene_indep [simp]: "x ⨝ y ⟹ ⟦x⟧∼ ⨝S a ;S y"
  by (transfer, simp add: lens_indep.lens_put_comm lens_indep.lens_put_irr2 lens_override_def)

lemma lens_scene_override: 
  "mwb_lens X ⟹ s1 ⊕S s2 on ⟦X⟧∼ = s1 ⊕L s2 on X"
  by (transfer, simp)

lemma lens_indep_scene:
  assumes "vwb_lens X" "vwb_lens Y"
  shows "(X ⨝ Y) ⟷ ⟦X⟧∼ ⨝S ⟦Y⟧∼"
  using assms
  by (auto, (simp add: scene_indep_override, transfer, simp add: lens_indep_override_def)+)

lemma lens_indep_impl_scene_indep [simp]:
  "(X ⨝ Y) ⟹ ⟦X⟧∼ ⨝S ⟦Y⟧∼"
  by (transfer, auto simp add: lens_indep_comm lens_override_def)

lemma get_scene_override_indep: "⟦ vwb_lens x; ⟦x⟧∼ ⨝S a ⟧ ⟹ get⇘x⇙ (s ⊕S s' on a) = get⇘x⇙ s"
proof -
  assume a1: "⟦x⟧∼ ⨝S a"
  assume a2: "vwb_lens x"
  then have "∀b ba bb. bb ⊕S b ⊕S ba on a on ⟦x⟧∼ = bb ⊕S b on ⟦x⟧∼"
    using a1 by (metis idem_scene_uminus indep_then_compl_in scene_indep_sym scene_override_commute subscene_eliminate vwb_impl_idem_scene)
  then show ?thesis
    using a2 by (metis lens_override_def lens_scene_override mwb_lens_def vwb_lens_mwb weak_lens.put_get)
qed

lemma put_scene_override_indep:
  "⟦ vwb_lens x; ⟦x⟧∼ ⨝S a ⟧ ⟹ put⇘x⇙ s v ⊕S s' on a = put⇘x⇙ (s ⊕S s' on a) v"
  by (transfer, auto)
     (metis lens_override_def mwb_lens_weak vwb_lens_mwb weak_lens.put_get)

lemma get_scene_override_le: "⟦ vwb_lens x; ⟦x⟧∼ ≤ a ⟧ ⟹ get⇘x⇙ (s ⊕S s' on a) = get⇘x⇙ s'"
  by (metis get_scene_override_indep scene_le_iff_indep_inv scene_override_commute)

lemma put_scene_override_le: "⟦ vwb_lens x; idem_scene a; ⟦x⟧∼ ≤ a ⟧ ⟹  put⇘x⇙ s v ⊕S s' on a = s ⊕S s' on a"
  by (metis lens_override_idem lens_override_put_right_in lens_scene_override sublens_refl subscene_eliminate vwb_lens_mwb)

lemma put_scene_override_le_distrib: 
  "⟦ vwb_lens x; idem_scene A; ⟦x⟧∼ ≤ A ⟧ ⟹ put⇘x⇙ (s1 ⊕S s2 on A) v = (put⇘x⇙ s1 v) ⊕S (put⇘x⇙ s2 v) on A"
  by (metis put_scene_override_indep put_scene_override_le scene_le_iff_indep_inv scene_override_commute)

lemma lens_plus_scene:
  "⟦ vwb_lens X; vwb_lens Y; X ⨝ Y ⟧ ⟹ ⟦X +L Y⟧∼ = ⟦X⟧∼ ⊔S ⟦Y⟧∼"
  by (transfer, auto simp add: lens_override_plus lens_indep_override_def lens_indep_overrideI)

lemma subscene_implies_sublens': "⟦ vwb_lens X; vwb_lens Y ⟧ ⟹ ⟦X⟧∼ ≤ ⟦Y⟧∼ ⟷ X ⊆L' Y"
  by (simp add: lens_defs, transfer, simp add: lens_override_def)

lemma sublens'_implies_subscene: "⟦ vwb_lens X; vwb_lens Y; X ⊆L' Y ⟧ ⟹ ⟦X⟧∼ ≤ ⟦Y⟧∼"
  by (simp add: lens_defs, auto simp add: lens_override_def lens_scene_override)

lemma sublens_iff_subscene:
  assumes "vwb_lens X" "vwb_lens Y"
  shows "X ⊆L Y ⟷ ⟦X⟧∼ ≤ ⟦Y⟧∼"
  by (simp add: assms sublens_iff_sublens' subscene_implies_sublens')

lemma lens_scene_indep_compl [simp]: 
  assumes "vwb_lens x" "vwb_lens y"
  shows "⟦x⟧∼ ⨝S - ⟦y⟧∼ ⟷ x ⊆L y"
  by (simp add: assms scene_le_iff_indep_inv sublens_iff_subscene)

lemma lens_scene_comp: "⟦ vwb_lens X; vwb_lens Y ⟧ ⟹ ⟦X ;L Y⟧∼ = ⟦X⟧∼ ;S Y"
  by (transfer, simp add: fun_eq_iff comp_vwb_lens)
     (simp add: lens_comp_def lens_override_def)

lemma scene_comp_pres_indep: "⟦ idem_scene a; idem_scene b; a ⨝S ⟦x⟧∼ ⟧ ⟹ a ⨝S b ;S x"
  by (transfer, auto)
     (metis (no_types, opaque_lifting) lens_override_def lens_override_idem vwb_lens_def wb_lens_weak weak_lens.put_get)

lemma scene_comp_le: "A ;S X ≤ ⟦X⟧∼"
  unfolding less_eq_scene_def by (transfer, auto simp add: fun_eq_iff lens_override_def)

lemma scene_quotient_comp: "⟦ vwb_lens X; idem_scene A; A ≤ ⟦X⟧∼ ⟧ ⟹ (A /S X) ;S X = A"
  unfolding less_eq_scene_def
proof (transfer, simp add: fun_eq_iff, safe)
  fix Xa :: "'a ⟹ 'b" and Aa :: "'b ⇒ 'b ⇒ 'b" and x :: 'b and xa :: 'b
  assume a1: "vwb_lens Xa"
  assume a2: "overrider Aa"
  assume a3: "idem_overrider Aa"
  assume a4: "∀s1 s2 s3. Aa (s1 ◃⇘Xa⇙ s2) s3 = s1 ◃⇘Xa⇙ Aa s2 s3"
  have "⋀b. Aa b b = b"
    using a3 by simp
  then have "Aa x (put⇘Xa⇙ src⇘Xa⇙ (get⇘Xa⇙ xa)) = Aa x xa"
    by (metis a2 a4 lens_override_def overrider.ovr_overshadow_right)
  then show "put⇘Xa⇙ x (get⇘Xa⇙ (Aa (create⇘Xa⇙ (get⇘Xa⇙ x)) (create⇘Xa⇙ (get⇘Xa⇙ xa)))) = Aa x xa"
    using a4 a1 by (metis lens_create_def lens_override_def vwb_lens_def wb_lens.get_put wb_lens_weak weak_lens.put_get)
qed

lemma lens_scene_quotient: "⟦ vwb_lens Y; X ⊆L Y ⟧ ⟹ ⟦X /L Y⟧∼ = ⟦X⟧∼ /S Y"
  by (metis lens_quotient_comp lens_quotient_vwb lens_scene_comp scene_comp_quotient sublens_pres_vwb vwb_lens_def wb_lens_weak)

lemma scene_union_quotient: "⟦ A ##S B; A ≤ ⟦X⟧∼; B ≤ ⟦X⟧∼ ⟧ ⟹ (A ⊔S B) /S X = (A /S X) ⊔S (B /S X)"
  unfolding less_eq_scene_def
  by (case_tac "vwb_lens X"; transfer, auto simp add: lens_create_def lens_override_def)

text ‹ Equality on scenes is sound and complete with respect to lens equivalence. ›

lemma lens_equiv_scene:
  assumes "vwb_lens X" "vwb_lens Y"
  shows "X ≈L Y ⟷ ⟦X⟧∼ = ⟦Y⟧∼"
proof
  assume a: "X ≈L Y"
  show "⟦X⟧∼ = ⟦Y⟧∼"
    by (meson a assms lens_equiv_def sublens_iff_subscene subscene_antisym vwb_impl_idem_scene)
next
  assume b: "⟦X⟧∼ = ⟦Y⟧∼"
  show "X ≈L Y"
    by (simp add: assms b lens_equiv_def sublens_iff_subscene subscene_refl)
qed

lemma lens_scene_top_iff_bij_lens: "mwb_lens x ⟹ ⟦x⟧∼ = ⊤S ⟷ bij_lens x"
  apply (transfer)
  apply (auto simp add: fun_eq_iff lens_override_def)
  apply (unfold_locales)
   apply auto
  done

subsection ‹ Function Domain Scene ›

lift_definition fun_dom_scene :: "'a set ⇒ ('a ⇒ 'b::two) scene" (‹fds›) is
"λ A f g. override_on f g A" by (unfold_locales, simp_all add: override_on_def fun_eq_iff)

lemma fun_dom_scene_empty: "fds({}) = ⊥S"
  by (transfer, simp)

lemma fun_dom_scene_union: "fds(A ∪ B) = fds(A) ⊔S fds(B)"
  by (transfer, auto simp add: fun_eq_iff override_on_def)

lemma fun_dom_scene_compl: "fds(- A) = - fds(A)"
  by (transfer, auto simp add: fun_eq_iff override_on_def)

lemma fun_dom_scene_inter: "fds(A ∩ B) = fds(A) ⊓S fds(B)"
  by (simp add: inf_scene_def fun_dom_scene_union[THEN sym] fun_dom_scene_compl[THEN sym])

lemma fun_dom_scene_UNIV: "fds(UNIV) = ⊤S"
  by (transfer, auto simp add: fun_eq_iff override_on_def)

lemma fun_dom_scene_indep [simp]:   
  "fds(A) ⨝S fds(B) ⟷ A ∩ B = {}"
  by (transfer, auto simp add: override_on_def fun_eq_iff, meson two_diff)

lemma fun_dom_scene_always_compat [simp]: "fds(A) ##S fds(B)"
  by (transfer, simp add: override_on_def fun_eq_iff)

lemma fun_dom_scene_le [simp]: "fds(A) ⊆S fds(B) ⟷ A ⊆ B"
  unfolding less_eq_scene_def
  by (transfer, auto simp add: override_on_def fun_eq_iff, meson two_diff)

text ‹ Hide implementation details for scenes ›  

lifting_update scene.lifting
lifting_forget scene.lifting

end