Theory Challenge1_short

section ‹Shorter Solution›
theory Challenge1_short
imports "lib/VTcomp"
begin

text ‹Small specification of textbuffer ADT,
  and its implementation by a gap buffer.
  
  Annotated and elaborated version of just the challenge requirements.
›
subsection ‹Abstract Specification›

  datatype 'a textbuffer = BUF ("pos": "nat") ("text": "'a list")
  ― ‹Note that we do not model the abstract invariant --- pos in range --- here,
    as it is not strictly required for the challenge spec.›

  text ‹These are the operations that were specified in the challenge.
    Note: Isabelle has type inference, so we do not need to specify types.
    Note: We exploit that, in Isabelle, we have @{lemma "(0::nat)-1=0" by simp}.
  ›
  primrec move_left where "move_left (BUF p t) = BUF (p-1) t" 
  primrec move_right where "move_right (BUF p t) = BUF (min (length t) (p+1)) t"
  primrec insert where "insert x (BUF p t) = BUF (p+1) (take p t@x#drop p t)"
  primrec delete where "delete (BUF p t) = BUF (p-1) (take (p-1) t@drop p t)"
  
subsection ‹Refinement 1: List with Gap›  
  
  subsection ‹Implementation on List-Level›  
  type_synonym 'a gap_buffer = "nat × nat × 'a list"

  subsubsection ‹Abstraction Relation›
  text ‹We define an invariant on the concrete gap-buffer, and its mapping to the
    abstract model. From these two, we define a relation ‹gap_rel› between
    concrete and abstract buffers. ›
  definition "gap_α ≡ λ(l,r,buf). BUF l (take l buf @ drop r buf)"
  definition "gap_invar ≡ λ(l,r,buf). l≤r ∧ r≤length buf"
  abbreviation "gap_rel ≡ br gap_α gap_invar"

  subsubsection ‹Left›
  
  text ‹For the operations, we insert assertions. These are not required to prove
    the list-level specification correct (during the proof, they are inferred easily).
    However, they are required in the subsequent automatic refinement step to arrays,
    to give our tool the information that all indexes are, indeed, in bounds.›
  
  definition "move_left1 ≡ λ(l,r,buf). doN {
    if l≠0 then doN {
      ASSERT(r-1<length buf ∧ l-1<length buf);
      RETURN (l-1,r-1,buf[r-1:=buf!(l-1)])
    } else RETURN (l,r,buf)
  }"

  lemma move_left1_correct: 
    "(move_left1, RETURN o move_left) ∈ gap_rel → ⟨gap_rel⟩nres_rel"
    apply clarsimp
    unfolding move_left1_def
    apply refine_vcg
    apply (auto 
      simp: in_br_conv gap_α_def gap_invar_def move_left1_def 
      split: prod.splits)
    (* sledgehammer! *)  
    by (smt Cons_nth_drop_Suc Suc_pred append.assoc append_Cons append_Nil 
      diff_Suc_less drop_update_cancel hd_drop_conv_nth length_list_update 
      less_le_trans nth_list_update_eq take_hd_drop)  

  subsubsection ‹Right›        
  definition "move_right1 ≡ λ(l,r,buf). doN {
    if r<length buf then doN {
      ASSERT (l<length buf);
      RETURN (l+1,r+1,buf[l:=buf!r])
    } else RETURN (l,r,buf)
  }"
    
  lemma move_right1_correct: 
    "(move_right1,RETURN o move_right) ∈ gap_rel → ⟨gap_rel⟩nres_rel"
    apply clarsimp
    unfolding move_right1_def
    apply refine_vcg
    unfolding gap_α_def gap_invar_def
    apply (auto simp: in_br_conv split: prod.split)
    apply (rule nth_equalityI)
     apply (simp_all add: Cons_nth_drop_Suc take_update_last)
    done

  subsubsection ‹Insert and Grow›
     
  definition "can_insert ≡ λ(l,r,buf). l<r"
  
  definition "grow1 K ≡ λ(l,r,buf). doN {
    let b = op_array_replicate (length buf + K) default;
    b ← mop_list_blit buf 0 b 0 l;
    b ← mop_list_blit buf r b (r+K) (length buf - r);
    RETURN (l,r+K,b)
  }"
  ― ‹Note: Most operations have also a variant prefixed with ‹mop›.
    These are defined in the refinement monad and already contain the assertion 
    of their precondition. The backside is that they cannot be easily used in as part
    of expressions, e.g., in @{term "buf[l:=buf!r]"}, we would have to explicitly bind
    each intermediate value: @{term "doN { v ← mop_list_get buf r; mop_list_set buf l v }"}.
  ›
  
  lemma grow1_correct[THEN SPEC_trans, refine_vcg]: 
    ― ‹Declares this as a rule to be used by the VCG›
    assumes "gap_invar gb"
    shows "grow1 K gb ≤ (SPEC (λgb'. 
        gap_invar gb' 
      ∧ gap_α gb' = gap_α gb 
      ∧ (K>0 ⟶ can_insert gb')))"
    unfolding grow1_def
    apply refine_vcg    
    using assms
    unfolding gap_α_def gap_invar_def can_insert_def
    apply (auto simp: op_list_blit_def)
    done  
  
  definition "insert1 x ≡ λ(l,r,buf). doN {
    (l,r,buf) ← 
      if (l=r) then grow1 (length buf+1) (l,r,buf) else RETURN (l,r,buf);
    ASSERT (l<length buf);
    RETURN (l+1,r,buf[l:=x])
  }" 
  
  lemma insert1_correct: 
    "(insert1,RETURN oo insert) ∈ Id → gap_rel → ⟨gap_rel⟩nres_rel"
    apply clarsimp
    unfolding insert1_def
    apply refine_vcg ― ‹VCG knows the rule for grow1 already›
    unfolding insert_def gap_α_def gap_invar_def can_insert_def
    apply (auto simp: in_br_conv take_update_last split: prod.split)
    done
  

  subsubsection ‹Delete›
  definition "delete1 
    ≡ λ(l,r,buf). if l>0 then RETURN (l-1,r,buf) else RETURN (l,r,buf)" 
  lemma delete1_correct: 
    "(delete1,RETURN o delete) ∈ gap_rel → ⟨gap_rel⟩nres_rel"
    apply clarsimp
    unfolding delete1_def
    apply refine_vcg
    unfolding gap_α_def gap_invar_def
    by (auto simp: in_br_conv butlast_take split: prod.split)
  
subsection ‹Imperative Arrays›  
  text ‹The following indicates how we will further refine the gap-buffer:
    The list will become an array, the indices and the content will not be 
    refined (expressed by @{const nat_assn} and @{const id_assn}).
  ›
  abbreviation "gap_impl_assn ≡ nat_assn ×a nat_assn ×a array_assn id_assn"  
  
  sepref_definition move_left_impl 
    is move_left1 :: "gap_impl_assnd→agap_impl_assn"
    unfolding move_left1_def by sepref

  sepref_definition move_right_impl 
    is move_right1 :: "gap_impl_assnd→agap_impl_assn"
    unfolding move_right1_def by sepref
  
  sepref_definition insert_impl 
    is "uncurry insert1" :: "id_assnk*agap_impl_assnd→agap_impl_assn"
    unfolding insert1_def grow1_def by sepref 
    ― ‹We inline @{const grow1} here›
    
  sepref_definition delete_impl 
    is delete1 :: "gap_impl_assnd→agap_impl_assn"
    unfolding delete1_def by sepref
  
  
  text ‹Finally, we combine the two refinement steps, to get overall correctness theorems›  
  definition "gap_assn ≡ hr_comp gap_impl_assn gap_rel" 
    ― ‹@{const hr_comp} is composition of refinement relations›
  context notes gap_assn_def[symmetric,fcomp_norm_unfold] begin
    lemmas move_left_impl_correct = move_left_impl.refine[FCOMP move_left1_correct]
       and move_right_impl_correct = move_right_impl.refine[FCOMP move_right1_correct]
       and insert_impl_correct = insert_impl.refine[FCOMP insert1_correct]
       and delete_impl_correct = delete_impl.refine[FCOMP delete1_correct]
    text ‹Proves:
      @{thm [display] move_left_impl_correct}
      @{thm [display] move_right_impl_correct}
      @{thm [display] insert_impl_correct}
      @{thm [display] delete_impl_correct}
    ›
       
  
  end
  
subsection ‹Executable Code›  
  text ‹Isabelle/HOL can generate code in various target languages.›

  export_code move_left_impl move_right_impl insert_impl delete_impl  
    in SML_imp module_name Gap_Buffer
    in OCaml_imp module_name Gap_Buffer
    in Haskell module_name Gap_Buffer
    in Scala module_name Gap_Buffer
    
        
end