theory PlusDemo
imports AutoCorres
begin

install_C_file "plus.c"

autocorres "plus.c"

context plus begin

thm plus'_def plus2'_def

term ovalid
lemma plus2_correct:
  "ovalid (\<lambda>s. True) (plus2' a b) (\<lambda>r s. r = plus' a b)"
  apply(unfold plus2'_def)
  apply(subst owhile_add_inv[where I="(\<lambda>(x,y) s. plus' x y = plus' a b)"])
  apply wp
    apply(clarsimp simp: plus'_def)
   apply(clarsimp simp: plus'_def)
   apply(unat_arith) (* could also use sledgehammer here *)
  apply clarsimp
  done
 
end

end