Theory Optics.Lens_Order

section ‹Order and Equivalence on Lenses›

theory Lens_Order
imports Lens_Algebra
begin

subsection ‹Sub-lens Relation›
  
text ‹A lens $X$ is a sub-lens of $Y$ if there is a well-behaved lens $Z$ such that $X = Z \lcomp Y$,
  or in other words if $X$ can be expressed purely in terms of $Y$.›

definition sublens :: "('a ⟹ 'c) ⇒ ('b ⟹ 'c) ⇒ bool" (infix "⊆⇩L" 55) where
[lens_defs]: "sublens X Y = (∃ Z :: ('a, 'b) lens. vwb_lens Z ∧ X = Z ;⇩L Y)"

text ‹Various lens classes are downward closed under the sublens relation.›

lemma sublens_pres_mwb:
  "⟦ mwb_lens Y; X ⊆⇩L Y ⟧ ⟹ mwb_lens X"
  by (unfold_locales, auto simp add: sublens_def lens_comp_def)

lemma sublens_pres_wb:
  "⟦ wb_lens Y; X ⊆⇩L Y ⟧ ⟹ wb_lens X"
  by (unfold_locales, auto simp add: sublens_def lens_comp_def)

lemma sublens_pres_vwb:
  "⟦ vwb_lens Y; X ⊆⇩L Y ⟧ ⟹ vwb_lens X"
  by (unfold_locales, auto simp add: sublens_def lens_comp_def)

text ‹Sublens is a preorder as the following two theorems show.›
    
lemma sublens_refl [simp]:
  "X ⊆⇩L X"
  using id_vwb_lens sublens_def by fastforce

lemma sublens_trans [trans]:
  "⟦ X ⊆⇩L Y; Y ⊆⇩L Z ⟧ ⟹ X ⊆⇩L Z"
  apply (auto simp add: sublens_def lens_comp_assoc)
  apply (rename_tac Z⇩1 Z⇩2)
  apply (rule_tac x="Z⇩1 ;⇩L Z⇩2" in exI)
  apply (simp add: lens_comp_assoc)
  using comp_vwb_lens apply blast
done

text ‹Sublens has a least element -- @{text "0⇩L"} -- and a greatest element -- @{text "1⇩L"}. 
  Intuitively, this shows that sublens orders how large a portion of the source type a particular
  lens views, with @{text "0⇩L"} observing the least, and @{text "1⇩L"} observing the most.›
  
lemma sublens_least: "wb_lens X ⟹ 0⇩L ⊆⇩L X"
  using sublens_def unit_vwb_lens by fastforce

lemma sublens_greatest: "vwb_lens X ⟹ X ⊆⇩L 1⇩L"
  by (simp add: sublens_def)

text ‹If $Y$ is a sublens of $X$ then any put using $X$ will necessarily erase any put using $Y$.
  Similarly, any two source types are observationally equivalent by $Y$ when performed
  following a put using $X$.›
    
lemma sublens_put_put:
  "⟦ mwb_lens X; Y ⊆⇩L X ⟧ ⟹ put⇘X⇙ (put⇘Y⇙ σ v) u = put⇘X⇙ σ u"
  by (auto simp add: sublens_def lens_comp_def)

lemma sublens_obs_get:
  "⟦ mwb_lens X; Y ⊆⇩L X ⟧ ⟹  get⇘Y⇙ (put⇘X⇙ σ v) = get⇘Y⇙ (put⇘X⇙ ρ v)"
  by (auto simp add: sublens_def lens_comp_def)

text ‹Sublens preserves independence; in other words if $Y$ is independent of $Z$, then also
  any $X$ smaller than $Y$ is independent of $Z$.›
    
lemma sublens_pres_indep:
  "⟦ X ⊆⇩L Y; Y ⨝ Z ⟧ ⟹ X ⨝ Z"
  apply (auto intro!:lens_indepI simp add: sublens_def lens_comp_def lens_indep_comm)
  apply (simp add: lens_indep_sym)
done

lemma sublens_pres_indep':
  "⟦ X ⊆⇩L Y; Z ⨝ Y ⟧ ⟹ Z ⨝ X"
  by (meson lens_indep_sym sublens_pres_indep)

lemma sublens_compat: "⟦ vwb_lens X; vwb_lens Y; X ⊆⇩L Y ⟧ ⟹ X ##⇩L Y"
  unfolding lens_compat_def lens_override_def
  by (metis (no_types, opaque_lifting) sublens_obs_get sublens_put_put vwb_lens_mwb vwb_lens_wb wb_lens.get_put)

text ‹Well-behavedness of lens quotient has sublens as a proviso. This is because we can only
  remove $X$ from $Y$ if $X$ is smaller than $Y$. ›
  
lemma lens_quotient_mwb:
  "⟦ mwb_lens Y; X ⊆⇩L Y ⟧ ⟹ mwb_lens (X /⇩L Y)"
  by (unfold_locales, auto simp add: lens_quotient_def lens_create_def sublens_def lens_comp_def comp_def)

subsection ‹Lens Equivalence›
    
text ‹Using our preorder, we can also derive an equivalence on lenses as follows. It should be
  noted that this equality, like sublens, is heterogeneously typed -- it can compare lenses whose
  view types are different, so long as the source types are the same. We show that it is reflexive, 
  symmetric, and transitive. ›
    
definition lens_equiv :: "('a ⟹ 'c) ⇒ ('b ⟹ 'c) ⇒ bool" (infix "≈⇩L" 51) where
[lens_defs]: "lens_equiv X Y = (X ⊆⇩L Y ∧ Y ⊆⇩L X)"

lemma lens_equivI [intro]:
  "⟦ X ⊆⇩L Y; Y ⊆⇩L X ⟧ ⟹ X ≈⇩L Y"
  by (simp add: lens_equiv_def)

lemma lens_equiv_refl [simp]:
  "X ≈⇩L X"
  by (simp add: lens_equiv_def)

lemma lens_equiv_sym:
  "X ≈⇩L Y ⟹ Y ≈⇩L X"
  by (simp add: lens_equiv_def)

lemma lens_equiv_trans [trans]:
  "⟦ X ≈⇩L Y; Y ≈⇩L Z ⟧ ⟹ X ≈⇩L Z"
  by (auto intro: sublens_trans simp add: lens_equiv_def)

lemma lens_equiv_pres_indep:
  "⟦ X ≈⇩L Y; Y ⨝ Z ⟧ ⟹ X ⨝ Z"
  using lens_equiv_def sublens_pres_indep by blast

lemma lens_equiv_pres_indep':
  "⟦ X ≈⇩L Y; Z ⨝ Y ⟧ ⟹ Z ⨝ X"
  using lens_equiv_def sublens_pres_indep' by blast

lemma lens_comp_cong_1: "X ≈⇩L Y ⟹ X ;⇩L Z ≈⇩L Y ;⇩L Z"
  unfolding lens_equiv_def
  by (metis (no_types, lifting) lens_comp_assoc sublens_def)

subsection ‹Further Algebraic Laws›

text ‹This law explains the behaviour of lens quotient.›

lemma lens_quotient_comp:
  "⟦ weak_lens Y; X ⊆⇩L Y ⟧ ⟹ (X /⇩L Y) ;⇩L Y = X"
  by (auto simp add: lens_quotient_def lens_comp_def comp_def sublens_def)

text ‹Plus distributes through quotient.›
    
lemma lens_quotient_plus:
  "⟦ mwb_lens Z; X ⊆⇩L Z; Y ⊆⇩L Z ⟧ ⟹ (X +⇩L Y) /⇩L Z = (X /⇩L Z) +⇩L (Y /⇩L Z)"
  apply (auto simp add: lens_quotient_def lens_plus_def sublens_def lens_comp_def comp_def)
  apply (rule ext)
  apply (rule ext)
  apply (simp add: prod.case_eq_if)
done

text ‹Laws for for lens plus on the denominator. These laws allow us to extract compositions
  of @{term "fst⇩L"} and @{term "snd⇩L"} terms. ›

lemma lens_quotient_plus_den1: 
  "⟦ weak_lens x; weak_lens y; x ⨝ y ⟧ ⟹ x /⇩L (x +⇩L y) = fst⇩L"
  by (auto simp add: lens_defs prod.case_eq_if fun_eq_iff, metis (lifting) lens_indep_def weak_lens.put_get)

lemma lens_quotient_plus_den2: "⟦ weak_lens x; weak_lens z; x ⨝ z; y ⊆⇩L z ⟧ ⟹ y /⇩L (x +⇩L z) = (y /⇩L z) ;⇩L snd⇩L "
  by (auto simp add: lens_defs prod.case_eq_if fun_eq_iff lens_indep.lens_put_irr2)

text ‹There follows a number of laws relating sublens and summation. Firstly, sublens is preserved
  by summation. ›
  
lemma plus_pred_sublens: "⟦ mwb_lens Z; X ⊆⇩L Z; Y ⊆⇩L Z; X ⨝ Y ⟧ ⟹ (X +⇩L Y) ⊆⇩L Z"
  apply (auto simp add: sublens_def)
  apply (rename_tac Z⇩1 Z⇩2)
  apply (rule_tac x="Z⇩1 +⇩L Z⇩2" in exI)
  apply (auto intro!: plus_wb_lens)
   apply (simp add: lens_comp_indep_cong_left)
  apply (simp add: plus_lens_distr)
done

text ‹Intuitively, lens plus is associative. However we cannot prove this using HOL equality due
  to monomorphic typing of this operator. But since sublens and lens equivalence are both heterogeneous
  we can now prove this in the following three lemmas.›
  
lemma lens_plus_sub_assoc_1:
  "X +⇩L Y +⇩L Z ⊆⇩L (X +⇩L Y) +⇩L Z"
  apply (simp add: sublens_def)
  apply (rule_tac x="(fst⇩L ;⇩L fst⇩L) +⇩L (snd⇩L ;⇩L fst⇩L) +⇩L snd⇩L" in exI)
  apply (auto)
   apply (rule plus_vwb_lens)
     apply (simp add: comp_vwb_lens fst_vwb_lens)
    apply (rule plus_vwb_lens)
      apply (simp add: comp_vwb_lens fst_vwb_lens snd_vwb_lens)
     apply (simp add: snd_vwb_lens)
    apply (simp add: lens_indep_left_ext)
   apply (rule lens_indep_sym)
   apply (rule plus_pres_lens_indep)
    using fst_snd_lens_indep fst_vwb_lens lens_indep_left_comp lens_indep_sym vwb_lens_mwb apply blast
   using fst_snd_lens_indep lens_indep_left_ext lens_indep_sym apply blast
  apply (auto simp add: lens_plus_def lens_comp_def fst_lens_def snd_lens_def prod.case_eq_if split_beta')[1]
done

lemma lens_plus_sub_assoc_2:
  "(X +⇩L Y) +⇩L Z ⊆⇩L X +⇩L Y +⇩L Z"
  apply (simp add: sublens_def)
  apply (rule_tac x="(fst⇩L +⇩L (fst⇩L ;⇩L snd⇩L)) +⇩L (snd⇩L ;⇩L snd⇩L)" in exI)
  apply (auto)
   apply (rule plus_vwb_lens)
     apply (rule plus_vwb_lens)
       apply (simp add: fst_vwb_lens)
      apply (simp add: comp_vwb_lens fst_vwb_lens snd_vwb_lens)
     apply (rule lens_indep_sym)
     apply (rule lens_indep_left_ext)
     using fst_snd_lens_indep lens_indep_sym apply blast
    apply (auto intro: comp_vwb_lens simp add: snd_vwb_lens)
   apply (rule plus_pres_lens_indep)
    apply (simp add: lens_indep_left_ext lens_indep_sym)
   apply (simp add: snd_vwb_lens)
  apply (auto simp add: lens_plus_def lens_comp_def fst_lens_def snd_lens_def prod.case_eq_if split_beta')[1]
done

lemma lens_plus_assoc:
  "(X +⇩L Y) +⇩L Z ≈⇩L X +⇩L Y +⇩L Z"
  by (simp add: lens_equivI lens_plus_sub_assoc_1 lens_plus_sub_assoc_2)

text ‹We can similarly show that it is commutative.›
    
lemma lens_plus_sub_comm: "X ⨝ Y ⟹ X +⇩L Y ⊆⇩L Y +⇩L X"
  apply (simp add: sublens_def)
  apply (rule_tac x="snd⇩L +⇩L fst⇩L" in exI)
  apply (auto)
   apply (simp add: fst_vwb_lens lens_indep_sym snd_vwb_lens)
  apply (simp add: lens_indep_sym lens_plus_swap)
done

lemma lens_plus_comm: "X ⨝ Y ⟹ X +⇩L Y ≈⇩L Y +⇩L X"
  by (simp add: lens_equivI lens_indep_sym lens_plus_sub_comm)

text ‹Any composite lens is larger than an element of the lens, as demonstrated by the following
  four laws.›
    
lemma lens_plus_ub [simp]: "wb_lens Y ⟹ X ⊆⇩L X +⇩L Y"
  by (metis fst_lens_plus fst_vwb_lens sublens_def)

lemma lens_plus_right_sublens:
  "⟦ vwb_lens Y; Y ⨝ Z; X ⊆⇩L Z ⟧ ⟹ X ⊆⇩L Y +⇩L Z"
  apply (auto simp add: sublens_def)
  apply (rename_tac Z')
  apply (rule_tac x="Z' ;⇩L snd⇩L" in exI)
  apply (auto)
  using comp_vwb_lens snd_vwb_lens apply blast
  apply (metis lens_comp_assoc snd_lens_plus vwb_lens_def)
  done
    
lemma lens_plus_mono_left:
  "⟦ Y ⨝ Z; X ⊆⇩L Y ⟧ ⟹ X +⇩L Z ⊆⇩L Y +⇩L Z"
  apply (auto simp add: sublens_def)
  apply (rename_tac Z')
  apply (rule_tac x="Z' ×⇩L 1⇩L" in exI)
  apply (subst prod_lens_comp_plus)
   apply (simp_all)
  using id_vwb_lens prod_vwb_lens apply blast
  done
    
lemma lens_plus_mono_right:
  "⟦ X ⨝ Z; Y ⊆⇩L Z ⟧ ⟹ X +⇩L Y ⊆⇩L X +⇩L Z"
  by (metis prod_lens_comp_plus prod_vwb_lens sublens_def sublens_refl)
    
text ‹If we compose a lens $X$ with lens $Y$ then naturally the resulting lens must be smaller
  than $Y$, as $X$ views a part of $Y$. ›
  
lemma lens_comp_lb [simp]: "vwb_lens X ⟹ X ;⇩L Y ⊆⇩L Y"
  by (auto simp add: sublens_def)

lemma sublens_comp [simp]:
  assumes "vwb_lens b" "c ⊆⇩L a"
  shows "(b ;⇩L c) ⊆⇩L a"
  by (metis assms sublens_def sublens_trans)

text ‹We can now also show that @{text "0⇩L"} is the unit of lens plus›
    
lemma lens_unit_plus_sublens_1: "X ⊆⇩L 0⇩L +⇩L X"
  by (metis lens_comp_lb snd_lens_plus snd_vwb_lens zero_lens_indep unit_wb_lens)

lemma lens_unit_prod_sublens_2: "0⇩L +⇩L X ⊆⇩L X"
  apply (auto simp add: sublens_def)
  apply (rule_tac x="0⇩L +⇩L 1⇩L" in exI)
  apply (auto)
  apply (auto simp add: lens_plus_def zero_lens_def lens_comp_def id_lens_def prod.case_eq_if comp_def)
  apply (rule ext)
  apply (rule ext)
  apply (auto)
done

lemma lens_plus_left_unit: "0⇩L +⇩L X ≈⇩L X"
  by (simp add: lens_equivI lens_unit_plus_sublens_1 lens_unit_prod_sublens_2)

lemma lens_plus_right_unit: "X +⇩L 0⇩L ≈⇩L X"
  using lens_equiv_trans lens_indep_sym lens_plus_comm lens_plus_left_unit zero_lens_indep by blast

text ‹We can also show that both sublens and equivalence are congruences with respect to lens plus
  and lens product.›
    
lemma lens_plus_subcong: "⟦ Y⇩1 ⨝ Y⇩2; X⇩1 ⊆⇩L Y⇩1; X⇩2 ⊆⇩L Y⇩2 ⟧ ⟹ X⇩1 +⇩L X⇩2 ⊆⇩L Y⇩1 +⇩L Y⇩2"
  by (metis prod_lens_comp_plus prod_vwb_lens sublens_def)

lemma lens_plus_eq_left: "⟦ X ⨝ Z; X ≈⇩L Y ⟧ ⟹ X +⇩L Z ≈⇩L Y +⇩L Z"
  by (meson lens_equiv_def lens_plus_mono_left sublens_pres_indep)

lemma lens_plus_eq_right: "⟦ X ⨝ Y; Y ≈⇩L Z ⟧ ⟹ X +⇩L Y ≈⇩L X +⇩L Z"
  by (meson lens_equiv_def lens_indep_sym lens_plus_mono_right sublens_pres_indep)

lemma lens_plus_cong:
  assumes "X⇩1 ⨝ X⇩2" "X⇩1 ≈⇩L Y⇩1" "X⇩2 ≈⇩L Y⇩2"
  shows "X⇩1 +⇩L X⇩2 ≈⇩L Y⇩1 +⇩L Y⇩2"
proof -
  have "X⇩1 +⇩L X⇩2 ≈⇩L Y⇩1 +⇩L X⇩2"
    by (simp add: assms(1) assms(2) lens_plus_eq_left)
  moreover have "... ≈⇩L Y⇩1 +⇩L Y⇩2"
    using assms(1) assms(2) assms(3) lens_equiv_def lens_plus_eq_right sublens_pres_indep by blast
  ultimately show ?thesis
    using lens_equiv_trans by blast
qed

lemma prod_lens_sublens_cong:
  "⟦ X⇩1 ⊆⇩L X⇩2; Y⇩1 ⊆⇩L Y⇩2 ⟧ ⟹ (X⇩1 ×⇩L Y⇩1) ⊆⇩L (X⇩2 ×⇩L Y⇩2)"
  apply (auto simp add: sublens_def)
  apply (rename_tac Z⇩1 Z⇩2)
  apply (rule_tac x="Z⇩1 ×⇩L Z⇩2" in exI)
  apply (auto)
   using prod_vwb_lens apply blast
  apply (auto simp add: lens_prod_def lens_comp_def prod.case_eq_if)
  apply (rule ext, rule ext)
  apply (auto simp add: lens_prod_def lens_comp_def prod.case_eq_if)
done

lemma prod_lens_equiv_cong:
  "⟦ X⇩1 ≈⇩L X⇩2; Y⇩1 ≈⇩L Y⇩2 ⟧ ⟹ (X⇩1 ×⇩L Y⇩1) ≈⇩L (X⇩2 ×⇩L Y⇩2)"
  by (simp add: lens_equiv_def prod_lens_sublens_cong)

text ‹We also have the following "exchange" law that allows us to switch over a lens product and plus.› 
    
lemma lens_plus_prod_exchange:
  "(X⇩1 +⇩L X⇩2) ×⇩L (Y⇩1 +⇩L Y⇩2) ≈⇩L (X⇩1 ×⇩L Y⇩1) +⇩L (X⇩2 ×⇩L Y⇩2)"
proof (rule lens_equivI)
  show "(X⇩1 +⇩L X⇩2) ×⇩L (Y⇩1 +⇩L Y⇩2) ⊆⇩L (X⇩1 ×⇩L Y⇩1) +⇩L (X⇩2 ×⇩L Y⇩2)"
    apply (simp add: sublens_def)
    apply (rule_tac x="((fst⇩L ;⇩L fst⇩L) +⇩L (fst⇩L ;⇩L snd⇩L)) +⇩L ((snd⇩L ;⇩L fst⇩L) +⇩L (snd⇩L ;⇩L snd⇩L))" in exI)
    apply (auto)
     apply (auto intro!: plus_vwb_lens comp_vwb_lens fst_vwb_lens snd_vwb_lens lens_indep_right_comp)
       apply (auto intro!: lens_indepI simp add: lens_comp_def lens_plus_def fst_lens_def snd_lens_def)
    apply (auto simp add: lens_prod_def lens_plus_def lens_comp_def fst_lens_def snd_lens_def prod.case_eq_if comp_def)[1]
    apply (rule ext, rule ext, auto simp add: prod.case_eq_if)
  done
  show "(X⇩1 ×⇩L Y⇩1) +⇩L (X⇩2 ×⇩L Y⇩2) ⊆⇩L (X⇩1 +⇩L X⇩2) ×⇩L (Y⇩1 +⇩L Y⇩2)"
    apply (simp add: sublens_def)
    apply (rule_tac x="((fst⇩L ;⇩L fst⇩L) +⇩L (fst⇩L ;⇩L snd⇩L)) +⇩L ((snd⇩L ;⇩L fst⇩L) +⇩L (snd⇩L ;⇩L snd⇩L))" in exI)
    apply (auto)
     apply (auto intro!: plus_vwb_lens comp_vwb_lens fst_vwb_lens snd_vwb_lens lens_indep_right_comp)
       apply (auto intro!: lens_indepI simp add: lens_comp_def lens_plus_def fst_lens_def snd_lens_def)
     apply (auto simp add: lens_prod_def lens_plus_def lens_comp_def fst_lens_def snd_lens_def prod.case_eq_if comp_def)[1]
    apply (rule ext, rule ext, auto simp add: lens_prod_def prod.case_eq_if)
  done
qed

lemma lens_get_put_quasi_commute:
  "⟦ vwb_lens Y; X ⊆⇩L Y ⟧ ⟹ get⇘Y⇙ (put⇘X⇙ s v) = put⇘X /⇩L Y⇙ (get⇘Y⇙ s) v"
proof -
  assume a1: "vwb_lens Y"
  assume a2: "X ⊆⇩L Y"
  have "⋀l la. put⇘l ;⇩L la⇙ = (λb c. put⇘la⇙ (b::'b) (put⇘l⇙ (get⇘la⇙ b::'a) (c::'c)))"
    by (simp add: lens_comp_def)
  then have "⋀l la b c. get⇘l⇙ (put⇘la ;⇩L l⇙ (b::'b) (c::'c)) = put⇘la⇙ (get⇘l⇙ b::'a) c ∨ ¬ weak_lens l"
    by force
  then show ?thesis
    using a2 a1 by (metis lens_quotient_comp vwb_lens_wb wb_lens_def)
qed
  
lemma lens_put_of_quotient:
  "⟦ vwb_lens Y; X ⊆⇩L Y ⟧ ⟹ put⇘Y⇙ s (put⇘X /⇩L Y⇙ v⇩2 v⇩1) = put⇘X⇙ (put⇘Y⇙ s v⇩2) v⇩1"
proof -
  assume a1: "vwb_lens Y"
  assume a2: "X ⊆⇩L Y"
  have f3: "⋀l b. put⇘l⇙ (b::'b) (get⇘l⇙ b::'a) = b ∨ ¬ vwb_lens l"
    by force
  have f4: "⋀b c. put⇘X /⇩L Y⇙ (get⇘Y⇙ b) c = get⇘Y⇙ (put⇘X⇙ b c)"
    using a2 a1 by (simp add: lens_get_put_quasi_commute)
  have "⋀b c a. put⇘Y⇙ (put⇘X⇙ b c) a = put⇘Y⇙ b a"
    using a2 a1 by (simp add: sublens_put_put)
  then show ?thesis
    using f4 f3 a1 by (metis mwb_lens.put_put mwb_lens_def vwb_lens_mwb weak_lens.put_get)
qed

text ‹ If two lenses are both independent and equivalent then they must be ineffectual. ›

lemma indep_and_equiv_implies_ief:
  assumes "wb_lens x" "x ⨝ y" "x ≈⇩L y"
  shows "ief_lens x"
proof -
  have "x ⨝ x"
    using assms(2) assms(3) lens_equiv_pres_indep' by blast
  thus ?thesis
    using assms(1) lens_indep_quasi_irrefl vwb_lens_wb wb_lens_weak by blast
qed

lemma indep_eff_implies_not_equiv [simp]:
  fixes x :: "'a::two ⟹ 'b"
  assumes "wb_lens x" "x ⨝ y"
  shows "¬ (x ≈⇩L y)"
  using assms indep_and_equiv_implies_ief no_ief_two_view by blast

subsection ‹Bijective Lens Equivalences›
  
text ‹A bijective lens, like a bijective function, is its own inverse. Thus, if we compose its inverse
  with itself we get @{term "1⇩L"}.›
  
lemma bij_lens_inv_left:
  "bij_lens X ⟹ inv⇩L X ;⇩L X = 1⇩L"
  by (auto simp add: lens_inv_def lens_comp_def lens_create_def comp_def id_lens_def, rule ext, auto)

lemma bij_lens_inv_right:
  "bij_lens X ⟹ X ;⇩L inv⇩L X = 1⇩L"
  by (auto simp add: lens_inv_def lens_comp_def comp_def id_lens_def, rule ext, auto)

text ‹The following important results shows that bijective lenses are precisely those that are 
  equivalent to identity. In other words, a bijective lens views all of the source type.›

lemma bij_lens_equiv_id:
  "bij_lens X ⟷ X ≈⇩L 1⇩L"
  apply (auto)
   apply (rule lens_equivI)
    apply (simp_all add: sublens_def)
   apply (rule_tac x="lens_inv X" in exI)
   apply (simp add: bij_lens_inv_left lens_inv_bij)
  apply (auto simp add: lens_equiv_def sublens_def id_lens_def lens_comp_def comp_def)
  apply (unfold_locales)
   apply (simp)
  apply (simp)
  apply (metis (no_types, lifting) vwb_lens_wb wb_lens_weak weak_lens.put_get)
done

text ‹For this reason, by transitivity, any two bijective lenses with the same source type must be equivalent.›
  
lemma bij_lens_equiv:
  "⟦ bij_lens X; X ≈⇩L Y ⟧ ⟹ bij_lens Y"
  by (meson bij_lens_equiv_id lens_equiv_def sublens_trans)

lemma bij_lens_cong:
  "X ≈⇩L Y ⟹ bij_lens X = bij_lens Y"
  by (meson bij_lens_equiv lens_equiv_sym)

text ‹We can also show that the identity lens @{term "1⇩L"} is unique. That is to say it is the only
  lens which when compose with $Y$ will yield $Y$.›
    
lemma lens_id_unique:
  "weak_lens Y ⟹ Y = X ;⇩L Y ⟹ X = 1⇩L"
  apply (cases Y)
  apply (cases X)
  apply (auto simp add: lens_comp_def comp_def id_lens_def fun_eq_iff)
   apply (metis select_convs(1) weak_lens.create_get)
  apply (metis select_convs(1) select_convs(2) weak_lens.put_get)
done

text ‹Consequently, if composition of two lenses $X$ and $Y$ yields @{text "1⇩L"}, then both
  of the composed lenses must be bijective.›
  
lemma bij_lens_via_comp_id_left:
  "⟦ wb_lens X; wb_lens Y; X ;⇩L Y = 1⇩L ⟧ ⟹ bij_lens X"
  apply (cases Y)
  apply (cases X)
  apply (auto simp add: lens_comp_def comp_def id_lens_def fun_eq_iff)
  apply (unfold_locales)
   apply (simp_all)
   using vwb_lens_wb wb_lens_weak weak_lens.put_get apply fastforce
  apply (metis select_convs(1) select_convs(2) wb_lens_weak weak_lens.put_get)
done

lemma bij_lens_via_comp_id_right:
  "⟦ wb_lens X; wb_lens Y; X ;⇩L Y = 1⇩L ⟧ ⟹ bij_lens Y"
  apply (cases Y)
  apply (cases X)
  apply (auto simp add: lens_comp_def comp_def id_lens_def fun_eq_iff)
  apply (unfold_locales)
   apply (simp_all)
   using vwb_lens_wb wb_lens_weak weak_lens.put_get apply fastforce
  apply (metis select_convs(1) select_convs(2) wb_lens_weak weak_lens.put_get)
done

text ‹Importantly, an equivalence between two lenses can be demonstrated by showing that one lens
  can be converted to the other by application of a suitable bijective lens $Z$. This $Z$ lens
  converts the view type of one to the view type of the other.›

lemma lens_equiv_via_bij:
  assumes "bij_lens Z" "X = Z ;⇩L Y"
  shows "X ≈⇩L Y"
  using assms
  apply (auto simp add: lens_equiv_def sublens_def)
   using bij_lens_vwb apply blast
  apply (rule_tac x="lens_inv Z" in exI)
  apply (auto simp add: lens_comp_assoc bij_lens_inv_left)
   using bij_lens_vwb lens_inv_bij apply blast
done

text ‹Indeed, we actually have a stronger result than this -- the equivalent lenses are precisely
  those than can be converted to one another through a suitable bijective lens. Bijective lenses
  can thus be seen as a special class of "adapter" lens.›
  
lemma lens_equiv_iff_bij:
  assumes "weak_lens Y"
  shows "X ≈⇩L Y ⟷ (∃ Z. bij_lens Z ∧ X = Z ;⇩L Y)"
  apply (rule iffI)
   apply (auto simp add: lens_equiv_def sublens_def lens_id_unique)[1]
   apply (rename_tac Z⇩1 Z⇩2)
   apply (rule_tac x="Z⇩1" in exI)
   apply (simp)
   apply (subgoal_tac "Z⇩2 ;⇩L Z⇩1 = 1⇩L")
    apply (meson bij_lens_via_comp_id_right vwb_lens_wb)
   apply (metis assms lens_comp_assoc lens_id_unique)
  using lens_equiv_via_bij apply blast
done

lemma pbij_plus_commute:
  "⟦ a ⨝ b; mwb_lens a; mwb_lens b; pbij_lens (b +⇩L a) ⟧ ⟹ pbij_lens (a +⇩L b)"
  apply (unfold_locales, simp_all add:lens_defs lens_indep_sym prod.case_eq_if)
  using lens_indep.lens_put_comm pbij_lens.put_det apply fastforce
  done

subsection ‹Lens Override Laws›
  
text ‹The following laws are analogus to the equivalent laws for functions.›
  
lemma lens_override_id [simp]:
  "S⇩1 ⊕⇩L S⇩2 on 1⇩L = S⇩2"
  by (simp add: lens_override_def id_lens_def)

lemma lens_override_unit [simp]:
  "S⇩1 ⊕⇩L S⇩2 on 0⇩L = S⇩1"
  by (simp add: lens_override_def zero_lens_def)

lemma lens_override_overshadow:
  assumes "mwb_lens Y"  "X ⊆⇩L Y"
  shows "(S⇩1 ⊕⇩L S⇩2 on X) ⊕⇩L S⇩3 on Y = S⇩1 ⊕⇩L S⇩3 on Y"
  using assms by (simp add: lens_override_def sublens_put_put)

lemma lens_override_irr:
  assumes "X ⨝ Y"
  shows "S⇩1 ⊕⇩L (S⇩2 ⊕⇩L S⇩3 on Y) on X = S⇩1 ⊕⇩L S⇩2 on X"
  using assms by (simp add: lens_override_def)

lemma lens_override_overshadow_left:
  assumes "mwb_lens X"
  shows "(S⇩1 ⊕⇩L S⇩2 on X) ⊕⇩L S⇩3 on X = S⇩1 ⊕⇩L S⇩3 on X"
  by (simp add: assms lens_override_def)

lemma lens_override_overshadow_right:
  assumes "mwb_lens X"
  shows "S⇩1 ⊕⇩L (S⇩2  ⊕⇩L S⇩3 on X) on X = S⇩1 ⊕⇩L S⇩3 on X"
  by (simp add: assms lens_override_def)

lemma lens_override_plus:
  "X ⨝ Y ⟹ S⇩1 ⊕⇩L S⇩2 on (X +⇩L Y) = (S⇩1 ⊕⇩L S⇩2 on X) ⊕⇩L S⇩2 on Y"
  by (simp add: lens_indep_comm lens_override_def lens_plus_def)

lemma lens_override_idem [simp]:
  "vwb_lens X ⟹ S ⊕⇩L S on X = S"
  by (simp add: lens_override_def)

lemma lens_override_mwb_idem [simp]:
  "⟦ mwb_lens X; S ∈ 𝒮⇘X⇙ ⟧ ⟹ S ⊕⇩L S on X = S"
  by (simp add: lens_override_def)

lemma lens_override_put_right_in:
  "⟦ vwb_lens A; X ⊆⇩L A ⟧ ⟹ S⇩1 ⊕⇩L (put⇘X⇙ S⇩2 v) on A = put⇘X⇙ (S⇩1 ⊕⇩L S⇩2 on A) v"
  by (simp add: lens_override_def lens_get_put_quasi_commute lens_put_of_quotient)

lemma lens_override_put_right_out:
  "⟦ vwb_lens A; X ⨝ A ⟧ ⟹ S⇩1 ⊕⇩L (put⇘X⇙ S⇩2 v) on A = (S⇩1 ⊕⇩L S⇩2 on A)"
  by (simp add: lens_override_def  lens_indep.lens_put_irr2)

lemma lens_indep_overrideI:
  assumes "vwb_lens X" "vwb_lens Y" "(⋀ s⇩1 s⇩2 s⇩3. s⇩1 ⊕⇩L s⇩2 on X ⊕⇩L s⇩3 on Y = s⇩1 ⊕⇩L s⇩3 on Y ⊕⇩L s⇩2 on X)"
  shows "X ⨝ Y"
  using assms
  apply (unfold_locales)
  apply (simp_all add: lens_override_def)
  apply (metis mwb_lens_def vwb_lens_mwb weak_lens.put_get)
  apply (metis lens_override_def lens_override_idem mwb_lens_def vwb_lens_mwb weak_lens.put_get)
  apply (metis mwb_lens_weak vwb_lens_mwb vwb_lens_wb wb_lens.get_put weak_lens.put_get)
  done  

lemma lens_indep_override_def:
  assumes "vwb_lens X" "vwb_lens Y"
  shows "X ⨝ Y ⟷ (∀ s⇩1 s⇩2 s⇩3. s⇩1 ⊕⇩L s⇩2 on X ⊕⇩L s⇩3 on Y = s⇩1 ⊕⇩L s⇩3 on Y ⊕⇩L s⇩2 on X)"
  by (metis assms(1) assms(2) lens_indep_comm lens_indep_overrideI lens_override_def)

text ‹ Alternative characterisation of very-well behaved lenses: override is idempotent. ›

lemma override_idem_implies_vwb:
  "⟦ mwb_lens X; ⋀ s. s ⊕⇩L s on X = s ⟧ ⟹ vwb_lens X"
  by (unfold_locales, simp_all add: lens_defs)

subsection ‹ Alternative Sublens Characterisation ›

text ‹ The following definition is equivalent to the above when the two lenses are very well behaved. ›

definition sublens' :: "('a ⟹ 'c) ⇒ ('b ⟹ 'c) ⇒ bool" (infix "⊆⇩L''" 55) where
[lens_defs]: "sublens' X Y = (∀ s⇩1 s⇩2 s⇩3. s⇩1 ⊕⇩L s⇩2 on Y ⊕⇩L s⇩3 on X = s⇩1 ⊕⇩L s⇩2 ⊕⇩L s⇩3 on X on Y)"

text ‹ We next prove some characteristic properties of our alternative definition of sublens. ›

lemma sublens'_prop1:
  assumes "vwb_lens X" "X ⊆⇩L' Y"
  shows "put⇘X⇙ (put⇘Y⇙ s⇩1 (get⇘Y⇙ s⇩2)) s⇩3 = put⇘Y⇙ s⇩1 (get⇘Y⇙ (put⇘X⇙ s⇩2 s⇩3))"
  using assms
  by (simp add: sublens'_def, metis lens_override_def mwb_lens_def vwb_lens_mwb weak_lens.put_get)

lemma sublens'_prop2:
  assumes "vwb_lens X" "X ⊆⇩L' Y"
  shows "get⇘X⇙ (put⇘Y⇙ s⇩1 (get⇘Y⇙ s⇩2)) = get⇘X⇙ s⇩2"
  using assms unfolding sublens'_def
  by (metis lens_override_def vwb_lens_wb wb_lens_axioms_def wb_lens_def weak_lens.put_get)

lemma sublens'_prop3:
  assumes "vwb_lens X" "vwb_lens Y" "X ⊆⇩L' Y"
  shows "put⇘Y⇙ σ (get⇘Y⇙ (put⇘X⇙ (put⇘Y⇙ ρ (get⇘Y⇙ σ)) v)) = put⇘X⇙ σ v"
  by (metis assms(1) assms(2) assms(3) mwb_lens_def sublens'_prop1 vwb_lens.put_eq vwb_lens_mwb weak_lens.put_get)

text ‹ Finally we show our two definitions of sublens are equivalent, assuming very well behaved lenses. ›

lemma sublens'_implies_sublens:
  assumes "vwb_lens X" "vwb_lens Y" "X ⊆⇩L' Y"
  shows "X ⊆⇩L Y"
proof -
  have "vwb_lens (X /⇩L Y)"
    by (unfold_locales
       ,auto simp add: assms lens_quotient_def lens_comp_def lens_create_def sublens'_prop1 sublens'_prop2)
  moreover have "X = X /⇩L Y ;⇩L Y"
  proof -
    have "get⇘X⇙ = (λσ. get⇘X⇙ (create⇘Y⇙ σ)) ∘ get⇘Y⇙"
      by (rule ext, simp add: assms(1) assms(3) lens_create_def sublens'_prop2)
    moreover have "put⇘X⇙ = (λσ v. put⇘Y⇙ σ (get⇘Y⇙ (put⇘X⇙ (create⇘Y⇙ (get⇘Y⇙ σ)) v)))"
      by (rule ext, rule ext, simp add: assms(1) assms(2) assms(3) lens_create_def sublens'_prop3)
    ultimately show ?thesis
      by (simp add: lens_quotient_def lens_comp_def)
  qed
  ultimately show ?thesis
    using sublens_def by blast
qed

lemma sublens_implies_sublens':
  assumes "vwb_lens Y" "X ⊆⇩L Y"
  shows "X ⊆⇩L' Y"
  by (metis assms lens_override_def lens_override_put_right_in sublens'_def)

lemma sublens_iff_sublens':
  assumes "vwb_lens X" "vwb_lens Y"
  shows "X ⊆⇩L Y ⟷ X ⊆⇩L' Y"
  using assms sublens'_implies_sublens sublens_implies_sublens' by blast

text ‹ We can also prove the closure law for lens quotient ›

lemma lens_quotient_vwb: "⟦ vwb_lens x; vwb_lens y; x ⊆⇩L y ⟧ ⟹ vwb_lens (x /⇩L y)"
  by (unfold_locales)
     (simp_all add: sublens'_def lens_quotient_def lens_quotient_mwb sublens_iff_sublens' lens_create_def sublens'_prop1 sublens'_prop2)

lemma lens_quotient_indep: 
  "⟦ vwb_lens x; vwb_lens y; vwb_lens a; x ⨝ y; x ⊆⇩L a; y ⊆⇩L a ⟧ ⟹ (x /⇩L a) ⨝ (y /⇩L a)"
  by (unfold_locales)
     (simp_all add: lens_quotient_def sublens_iff_sublens' lens_create_def lens_indep.lens_put_comm sublens'_prop1 sublens'_prop2 lens_indep.lens_put_irr2)

lemma lens_quotient_bij: "⟦ vwb_lens x; vwb_lens y; y ≈⇩L x ⟧ ⟹ bij_lens (x /⇩L y)"
  by (metis lens_comp_quotient lens_equiv_iff_bij lens_equiv_sym vwb_lens_wb wb_lens_weak)

subsection ‹ Alternative Equivalence Characterisation ›

definition lens_equiv' :: "('a ⟹ 'c) ⇒ ('b ⟹ 'c) ⇒ bool" (infix "≈⇩L''" 51) where
[lens_defs]: "lens_equiv' X Y = (∀ s⇩1 s⇩2. (s⇩1 ⊕⇩L s⇩2 on X = s⇩1 ⊕⇩L s⇩2 on Y))"

lemma lens_equiv_iff_lens_equiv':
  assumes "vwb_lens X" "vwb_lens Y"
  shows "X ≈⇩L Y ⟷ X ≈⇩L' Y"
  apply (simp add: lens_equiv_def sublens_iff_sublens' assms)
  apply (auto simp add: lens_defs assms)
  apply (metis assms(2) mwb_lens.put_put vwb_lens_mwb vwb_lens_wb wb_lens.get_put)
  done

subsection ‹ Ineffectual Lenses as Zero Elements ›

lemma ief_lens_then_zero: "ief_lens x ⟹ x ≈⇩L 0⇩L"
  by (simp add: lens_equiv_iff_lens_equiv' lens_equiv'_def)
     (simp add: ief_lens.put_inef lens_override_def)

lemma ief_lens_iff_zero: "vwb_lens x ⟹ ief_lens x ⟷ x ≈⇩L 0⇩L"
  by (metis ief_lens_axioms_def ief_lens_def ief_lens_then_zero lens_equiv_def lens_override_def lens_override_unit sublens'_prop3 sublens_implies_sublens' unit_vwb_lens vwb_lens_wb wb_lens_weak)

end