Quelle  Optics.thy

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