# Theory VTcomp

```theory VTcomp
begin

section ‹Library›

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

"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
}"
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
subgoal using IS
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)

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
```