theory FibDemo
imports AutoCorres
begin

install_C_file "fib.c"

autocorres  [unsigned_word_abs = fib_linear] "fib.c"

fun 
  fib :: "nat \<Rightarrow> nat"
where
  "fib 0 = 0" |
  "fib (Suc 0) = 1" |
  "fib (Suc (Suc n)) = fib (Suc n) + fib n"


context fib begin

lemma
  "ovalid (\<lambda>s. True) (fib_linear' n) (\<lambda>r s. r = fib n)"
  apply(unfold fib_linear'_def)
  apply(subst owhile_add_inv[where I="(\<lambda> (a,b,n') _. a + b = fib (n - n') + 1 \<and> n' \<le> n)"])
  apply wp
  apply (auto simp: Suc_diff_le)
  done
  
end
end