theory PlusDemo
imports AutoCorres
begin

install_C_file "plus.c"

autocorres "plus.c"

context plus begin

thm plus'_def plus2'_def

thm ovalid_def
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) _. a + b = x + y"])
  apply wp
    apply clarsimp
   apply (clarsimp simp: plus'_def)
   using word_neq_0_conv apply blast
  apply clarsimp
  done
 
end

end