Theory Optics

text‹This is an excerpt of the Optics library 
     🌐‹https://www.isa-afp.org/entries/Optics.html› by Frank Zeyda and
     Simon Foster. It provides a rich infrastructure for ∗‹algebraic lenses›,
     an abstract theory allowing to describe parts of memory and their 
     independence. We use it to abstractly model typed program variables and
     framing conditions. 

     Optics provides a rich framework for lense compositions and sub-lenses
     which we will not use in the context of Clean; even the offered concept
     of a list-lense, a possible means to model the stack-infrastructure 
     required for local variables, is actually richer than needed.

     Since Clean strives for minimality, we restrict ourselves to this "proxy"
     theory for Optics.
›

theory Optics
  imports Lens_Laws
begin


fun      upd_hd :: "('a ⇒ 'a) ⇒ 'a list ⇒ 'a list" 
  where "upd_hd f [] = []"
      | "upd_hd f (a#S) = f a # S"

lemma [simp] :"tl (upd_hd f S) = tl S" 
  by (metis list.sel(3) upd_hd.elims)


definition upd2put :: "(('d ⇒ 'b) ⇒ 'a ⇒ 'c) ⇒ 'a ⇒ 'b ⇒ 'c"
  where   "upd2put f = (λσ. λ b. f (λ_. b) σ)"

definition create⇩L 
  where "create⇩L getv updv = ⦇lens_get = getv,lens_put = upd2put updv⦈"

definition "hd⇩L = create⇩L hd upd_hd"   (* works since no partial lenses needed in Clean*)

definition "map_nth i = (λf l. list_update l i (f (l ! i)))"

lemma indep_list_lift : 
     "X ⨝ create⇩L getv updv 
      ⟹ (λf σ. updv (λ_. f (getv σ)) σ) = updv 
      ⟹ X ⨝ create⇩L (hd ∘ getv ) (updv ∘ upd_hd)"
  unfolding create⇩L_def o_def Lens_Laws.lens_indep_def upd2put_def
  by (auto,metis (no_types)) (metis (no_types))

end