Theory Arrays_Impl

(*
  File: Arrays_Impl.thy
  Author: Bohua Zhan
*)

section ‹Implementation of arrays›

theory Arrays_Impl
  imports SepAuto "../Functional/Arrays_Ex"
begin

text ‹
  Imperative implementations of common array operations.

  Imperative reverse on arrays is also verified in theory Imperative\_Reverse
  in Imperative\_HOL/ex in the Isabelle library.
›

subsection ‹Array copy›

fun array_copy :: "'a::heap array ⇒ 'a array ⇒ nat ⇒ unit Heap" where
  "array_copy a b 0 = (return ())"
| "array_copy a b (Suc n) = do {
      array_copy a b n;
      x ← Array.nth a n;
      Array.upd n x b;
      return () }"

lemma array_copy_rule [hoare_triple]:
  "n ≤ length as ⟹ n ≤ length bs ⟹
   <a ↦⇩a as * b ↦⇩a bs>
    array_copy a b n
   <λ_. a ↦⇩a as * b ↦⇩a Arrays_Ex.array_copy as bs n>"
@proof @induct n @qed

subsection ‹Swap›

definition swap :: "'a::heap array ⇒ nat ⇒ nat ⇒ unit Heap" where
  "swap a i j = do {
     x ← Array.nth a i;
     y ← Array.nth a j;
     Array.upd i y a;
     Array.upd j x a;
     return ()
   }"

lemma swap_rule [hoare_triple]:
  "i < length xs ⟹ j < length xs ⟹
   <p ↦⇩a xs>
   swap p i j
   <λ_. p ↦⇩a list_swap xs i j>" by auto2

subsection ‹Reverse›

fun rev :: "'a::heap array ⇒ nat ⇒ nat ⇒ unit Heap" where
  "rev a i j = (if i < j then do {
     swap a i j;
     rev a (i + 1) (j - 1)
   }
   else return ())"

lemma rev_to_fun [hoare_triple]:
  "j < length xs ⟹
   <p ↦⇩a xs>
   rev p i j
   <λ_. p ↦⇩a rev_swap xs i j>"
@proof @fun_induct "rev_swap xs i j" @unfold "rev_swap xs i j" @qed

text ‹Correctness of imperative reverse.›
theorem rev_is_rev [hoare_triple]:
  "xs ≠ [] ⟹
   <p ↦⇩a xs>
   rev p 0 (length xs - 1)
   <λ_. p ↦⇩a List.rev xs>" by auto2

end