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)))"


find_theorems "list_update"


lemma [simp]: "map_nth i f [] = []"
  by(simp_all add: map_nth_def)

lemma [simp]: "map_nth i f (a#R) = (case i of 0 ⇒ (f a) # R | Suc j ⇒ a # map_nth j f R)"
  by(simp add: Nitpick.case_nat_unfold map_nth_def)

lemma [simp]: "map_nth n (λx. x) S = S"
  by(induct S, simp_all add: map_nth_def)
 
lemma [simp]: "length(map_nth n f S) = length S"
  by(simp add: map_nth_def)

lemma [simp]: "n < length S ⟹ (map_nth n f S) ! n = f (S ! n)"
  by (simp add: map_nth_def)

lemma [simp]: "n < length S ⟹ m < length S ⟹ n≠m ⟹ (map_nth m f S) ! n = S ! n"
  by (simp add: map_nth_def)

lemma [simp]: "n < length S ⟹ (map_nth n f (map_nth n g S)) = (map_nth n (f o g) S)"
  by (simp add: map_nth_def)

(* and more *)

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