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); bb←b 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: "lb≤ub"
  assumes I0: "I lb σ0"
  assumes IS: "⋀i σ. ⟦ lb≤i; i<ub; I i σ; c σ ⟧ ⟹ f i σ ≤ SPEC (I (i+1))"
  assumes FNC: "⋀i σ. ⟦ lb≤i; i≤ub; 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 (lb≤ub);
  (_,σ) ← EWHILET (λ(i,σ). i<ub) (λ(i,σ). doE { σ ← f i σ; ERETURN (i+1,σ) }) (lb,σ);
  ERETURN σ
}"  
  
lemma efor_rule:
  assumes INTV: "lb≤ub"
  assumes I0: "I lb σ0"
  assumes IS: "⋀i σ. ⟦ lb≤i; 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,σ). lb≤i ∧ i≤ub ∧ 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)

syntax_consts
  "_doN_block" "_doN_bind" "_doN_cons" "_thenM" ⇌ bind_doE and
  "_doN_let" ⇌ Let

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  
        ((((⟨A⟩list_rel ×⇩r nat_rel) ×⇩r ⟨A⟩list_rel) ×⇩r nat_rel) ×⇩r nat_rel) → ⟨A⟩list_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_array⇧k*⇩anat_assn⇧k*⇩ais_array⇧d*⇩anat_assn⇧k*⇩anat_assn⇧k →⇩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