theory MultByAddDemo
imports AutoCorres
begin

install_C_file "mult_by_add.c"

autocorres "mult_by_add.c"

context mult_by_add begin

lemma
  "ovalid (\<lambda>_. True) (mult_by_add' a b) (\<lambda>r s. r = a * b)"
  apply(unfold mult_by_add'_def)
  apply(subst owhile_add_inv[where I="\<lambda>(x, result) _. x*b + result = a*b"])
  apply wp
    apply clarsimp
    apply (simp add: add.commute mult.commute right_diff_distrib)
   apply clarsimp
   using word_neq_0_conv apply fastforce
  apply clarsimp
  done

end

end