Theory VTcomp

theory VTcomp
  imports Exc_Nres_Monad
begin

section ‹Library›

text ‹
This theory contains a collection of auxiliary material that was used as a library for the contest.
›

lemma monadic_WHILEIT_unfold:
  "monadic_WHILEIT I b f s = do {
    ASSERT (I s); bbb s; if bb then do { s  f s; monadic_WHILEIT I b f s } else RETURN s
  }"      
  unfolding monadic_WHILEIT_def
  apply (subst RECT_unfold)
  apply refine_mono
  by simp

no_notation Ref.lookup ("!_" 61)
no_notation Ref.update ("_ := _" 62)

subsection ‹Specialized Rules for Foreach-Loops›
lemma nfoldli_upt_rule:
  assumes INTV: "lbub"
  assumes I0: "I lb σ0"
  assumes IS: "i σ.  lbi; i<ub; I i σ; c σ   f i σ  SPEC (I (i+1))"
  assumes FNC: "i σ.  lbi; iub; I i σ; ¬c σ   P σ"
  assumes FC: "σ.  I ub σ; c σ   P σ"
  shows "nfoldli [lb..<ub] c f σ0  SPEC P"
  apply (rule nfoldli_rule[where I="λl _ σ. I (lb+length l) σ"])
  apply simp_all
  apply (simp add: I0)
  subgoal using IS
    by (metis Suc_eq_plus1 add_diff_cancel_left' eq_diff_iff le_add1 length_upt upt_eq_lel_conv)
  subgoal for l1 l2 σ 
    apply (rule FNC[where i="lb + length l1"])
    apply (auto simp: INTV)
    using INTV upt_eq_append_conv by auto
  apply (rule FC) using INTV 
  by auto  


definition [enres_unfolds]: "efor (lb::int) ub f σ  doE {
  EASSERT (lbub);
  (_,σ)  EWHILET (λ(i,σ). i<ub) (λ(i,σ). doE { σ  f i σ; ERETURN (i+1,σ) }) (lb,σ);
  ERETURN σ
}"  
  
lemma efor_rule:
  assumes INTV: "lbub"
  assumes I0: "I lb σ0"
  assumes IS: "i σ.  lbi; i<ub; I i σ   f i σ  ESPEC E (I (i+1))"
  assumes FC: "σ.  I ub σ   P σ"
  shows "efor lb ub f σ0  ESPEC E P"
  unfolding efor_def
  supply EWHILET_rule[where R="measure (λ(i,_). nat (ub-i))" and I="λ(i,σ). lbi  iub  I i σ", refine_vcg]
  apply refine_vcg
  apply auto
  using assms apply auto
  done
  
  
subsection ‹Improved Do-Notation for the nres›-Monad›  

abbreviation (do_notation) bind_doN where "bind_doN  Refine_Basic.bind"

notation (output) bind_doN (infixl "" 54)
notation (ASCII output) bind_doN (infixl ">>=" 54)

nonterminal doN_binds and doN_bind
syntax
  "_doN_block" :: "doN_binds  'a" ("doN {//(2  _)//}" [12] 62)
  "_doN_bind"  :: "[pttrn, 'a]  doN_bind" ("(2_ / _)" 13)
  "_doN_let" :: "[pttrn, 'a]  doN_bind" ("(2let _ =/ _)" [1000, 13] 13)
  "_doN_then" :: "'a  doN_bind" ("_" [14] 13)
  "_doN_final" :: "'a  doN_binds" ("_")
  "_doN_cons" :: "[doN_bind, doN_binds]  doN_binds" ("_;//_" [13, 12] 12)
  "_thenM" :: "['a, 'b]  'c" (infixl "" 54)

syntax (ASCII)
  "_doN_bind" :: "[pttrn, 'a]  doN_bind" ("(2_ <-/ _)" 13)
  "_thenM" :: "['a, 'b]  'c" (infixl ">>" 54)

translations
  "_doN_block (_doN_cons (_doN_then t) (_doN_final e))"
     "CONST bind_doN t (λ_. e)"
  "_doN_block (_doN_cons (_doN_bind p t) (_doN_final e))"
     "CONST bind_doN t (λp. e)"
  "_doN_block (_doN_cons (_doN_let p t) bs)"
     "let p = t in _doN_block bs"
  "_doN_block (_doN_cons b (_doN_cons c cs))"
     "_doN_block (_doN_cons b (_doN_final (_doN_block (_doN_cons c cs))))"
  "_doN_cons (_doN_let p t) (_doN_final s)"
     "_doN_final (let p = t in s)"
  "_doN_block (_doN_final e)"  "e"
  "(m  n)"  "(m  (λ_. n))"

subsection ‹Array Blit exposed to Sepref›  

  definition "op_list_blit src si dst di len  
    (take di dst @ take len (drop si src) @ drop (di+len) dst)"

  context 
    notes op_list_blit_def[simp] 
  begin  
    sepref_decl_op (no_def) list_blit : 
      "op_list_blit" 
      :: "[λ((((src,si),dst),di),len). si+len  length src  di+len  length dst]f  
        ((((Alist_rel ×r nat_rel) ×r Alist_rel) ×r nat_rel) ×r nat_rel)  Alist_rel" .
  end

  lemma blit_len[simp]: "si + len  length src  di + len  length dst 
     length (op_list_blit src si dst di len) = length dst"
    by (auto simp: op_list_blit_def)
  
    
  context 
    notes [fcomp_norm_unfold] = array_assn_def[symmetric]
  begin    
    lemma array_blit_hnr_aux: 
          "(uncurry4 (λsrc si dst di len. do { blit src si dst di len; return dst }), 
            uncurry4 mop_list_blit) 
       is_arrayk*anat_assnk*ais_arrayd*anat_assnk*anat_assnk a is_array"
      apply sepref_to_hoare
      apply (clarsimp simp: refine_pw_simps)
      apply (sep_auto simp: is_array_def op_list_blit_def)
      done
    
    sepref_decl_impl (ismop) array_blit: array_blit_hnr_aux .
  end  

end