Theory Collections

section ‹ Collections ›

theory Collections
  imports Substitutions
begin

text ‹ A lens whose source is a collection type (e.g. a list or map) can be divided into several
  lenses, corresponding to each of the elements in the collection. This can be used to support
  update of an individual collection element, such as an array update. Here, we provide the
  infrastructure to support such collection lenses~\cite{Foster2020-LocalVars}.  ›

subsection ‹ Partial Lens Definedness ›

text ‹ Partial lenses (e.g. @{term mwb_lens}) are only defined for certain states. For example,
  the list lens is defined only when the source list is of a sufficient length. Below, we define
  a predicate that characterises the states in a which such a lens is defined. ›

definition lens_defined :: "('a ⟹ 's) ⇒ (bool, 's) expr" where
[expr_defs]: "lens_defined x = ($❙v ∈ 𝒮⇘«x»⇙)⇩e"

syntax "_lens_defined" :: "svid ⇒ logic" ("❙D'(_')")
translations "_lens_defined x" == "CONST lens_defined x"

expr_constructor lens_defined

subsection ‹ Dynamic Lenses ›

text ‹ Dynamics lenses~\cite{Foster2020-LocalVars} are used to model elements of a lens indexed 
  by some type @{typ "'i"}. The index is typically used to select different elements of a collection. 
  The lens is ``dynamic'' because the particular index is provided by an expression @{typ "'s ⇒ 'i"},
  which can change from state to state. We normally assume that this expression does not
  refer to the indexed lens itself. ›

definition dyn_lens :: "('i ⇒ ('a ⟹ 's)) ⇒ ('s ⇒ 'i) ⇒ ('a ⟹ 's)" where
[lens_defs]: "dyn_lens f x = ⦇ lens_get = (λ s. get⇘f (x s)⇙ s), lens_put = (λ s v. put⇘f (x s)⇙ s v) ⦈"

lemma dyn_lens_mwb [simp]: "⟦ ⋀ i. mwb_lens (f i); ⋀ i. $f(i) ♯ e ⟧ ⟹ mwb_lens (dyn_lens f e)"
  apply (unfold_locales, auto simp add: expr_defs lens_defs lens_indep.lens_put_irr2)
  apply (metis lens_override_def mwb_lens_weak weak_lens.put_get)
  apply (metis lens_override_def mwb_lens.put_put)
  done

lemma ind_lens_vwb [simp]: "⟦ ⋀ i. vwb_lens (f i); ⋀ i. $f(i) ♯ e ⟧ ⟹ vwb_lens (dyn_lens f e)"
  by (unfold_locales, auto simp add: lens_defs expr_defs lens_indep.lens_put_irr2 lens_scene_override)
     (metis mwb_lens_weak vwb_lens_mwb weak_lens.put_get, metis mwb_lens.put_put vwb_lens_mwb)

lemma src_dyn_lens: "⟦ ⋀ i. mwb_lens (f i); ⋀ i. $f(i) ♯ e ⟧ ⟹ 𝒮⇘dyn_lens f e⇙ = {s. s ∈ 𝒮⇘f (e s)⇙}"
  by (auto simp add: lens_defs expr_defs lens_source_def lens_scene_override unrest)
     (metis mwb_lens.put_put)+

lemma subst_lookup_dyn_lens [usubst]: "⟦ ⋀ i. f i ⨝ x ⟧ ⟹ ⟨subst_upd σ (dyn_lens f k) e⟩⇩s x = ⟨σ⟩⇩s x"
  by (expr_simp, metis (mono_tags, lifting) lens_indep.lens_put_irr2)

lemma get_upd_dyn_lens [usubst_eval]: "⟦ ⋀ i. f i ⨝ x ⟧ ⟹ get⇘x⇙ (subst_upd σ (dyn_lens f k) e s) = get⇘x⇙ (σ s)"
  by (expr_simp, metis lens_indep.lens_put_irr2)

subsection ‹ Overloaded Collection Lens ›

text ‹ The following polymorphic constant is used to provide implementations of different
  collection lenses. Type @{typ "'k"} is the index into the collection. For the list
  collection lens, the index has type @{typ "nat"}. ›

consts collection_lens :: "'k ⇒ ('a ⟹ 's)"

definition [lens_defs]: "fun_collection_lens = fun_lens"
definition [lens_defs]: "list_collection_lens = list_lens"

adhoc_overloading 
  collection_lens ⇌ fun_collection_lens and
  collection_lens ⇌ list_collection_lens  

lemma vwb_fun_collection_lens [simp]: "vwb_lens (fun_collection_lens k)"
  by (simp add: fun_collection_lens_def fun_vwb_lens)

lemma put_fun_collection_lens [simp]: 
  "put⇘fun_collection_lens i⇙ = (λf. fun_upd f i)"
  by (simp add: fun_collection_lens_def fun_lens_def)

lemma mwb_list_collection_lens [simp]: "mwb_lens (list_collection_lens i)"
  by (simp add: list_collection_lens_def list_mwb_lens)

lemma source_list_collection_lens: "𝒮⇘list_collection_lens i⇙ = {xs. i < length xs}"
  by (simp add: list_collection_lens_def source_list_lens)

lemma put_list_collection_lens [simp]: 
  "put⇘list_collection_lens i⇙ = (λ xs. list_augment xs i)"
  by (simp add: list_collection_lens_def list_lens_def)

subsection ‹ Syntax for Collection Lenses ›

text ‹ We add variable identifier syntax for collection lenses, which allows us to write
  @{text "x[i]"} for some collection and index. ›

abbreviation "dyn_lens_poly f x i ≡ dyn_lens (λ k. ns_alpha x (f k)) i"

syntax
  "_svid_collection" :: "svid ⇒ logic ⇒ svid" ("_[_]" [999, 0] 999)

translations
  "_svid_collection x e" == "CONST dyn_lens_poly CONST collection_lens x (e)⇩e"

lemma source_ns_alpha: "⟦ mwb_lens a; mwb_lens x ⟧ ⟹ 𝒮⇘ns_alpha a x⇙ = {s ∈ 𝒮⇘a⇙. get⇘a⇙ s ∈ 𝒮⇘x⇙}"
  by (simp add: ns_alpha_def source_lens_comp)

lemma defined_vwb_lens [simp]: "vwb_lens x ⟹ ❙D(x) = (True)⇩e"
  by (simp add: lens_defined_def)
     (metis UNIV_I vwb_lens_iff_mwb_UNIV_src)

lemma defined_list_collection_lens [simp]:
  "⟦ vwb_lens x; $x ♯ e ⟧ ⟹ ❙D(x[e]) = (e < length($x))⇩e"
  by (simp add: lens_defined_def src_dyn_lens unrest source_ns_alpha source_list_collection_lens)
     (simp add: lens_defs wb_lens.source_UNIV)

lemma lens_defined_list_code [code_unfold]: 
  "vwb_lens x ⟹ lens_defined (ns_alpha x (list_collection_lens i)) = («i» < length($x))⇩e"
  by (simp add: lens_defined_def src_dyn_lens unrest source_ns_alpha source_list_collection_lens)
     (simp add: lens_defs wb_lens.source_UNIV)

text ‹ The next theorem allows the simplification of a collection lens update. ›

lemma get_subst_upd_dyn_lens [simp]: 
  "mwb_lens x ⟹ get⇘x⇙ (subst_upd σ (dyn_lens_poly cl x (e)⇩e) v s)
                  = lens_put (cl (e (σ s))) (get⇘x⇙ (σ s)) (v s)"
  by expr_simp

end