Theory Fibs

theory "Fibs"
  imports
    "../HOLCF_Prelude"
    "../Definedness"
begin

section ‹Fibonacci sequence›

text ‹
  In this example, we show that the self-recursive lazy definition of the
  fibonacci sequence is actually defined and correct.
›

fixrec fibs :: "[Integer]" where
  [simp del]: "fibs = 0 : 1 : zipWith⋅(+)⋅fibs⋅(tail⋅fibs)"

fun fib :: "int ⇒ int" where
  "fib n = (if n ≤ 0 then 0 else if n = 1 then 1 else fib (n - 1) + fib (n - 2))"

declare fib.simps [simp del]

lemma fibs_0 [simp]:
  "fibs !! 0 = 0"
  by (subst fibs.simps) simp

lemma fibs_1 [simp]:
  "fibs !! 1 = 1"
  by (subst fibs.simps) simp

text ‹And the proof that @{term "fibs !! i"} is defined and the fibs value.›

(* Strange isabelle simplifier bug? *)
lemma [simp]:"-1 + ⟦i⟧ = ⟦ i ⟧ - 1" by simp
lemma [simp]:"-2 + ⟦i⟧ = ⟦ i ⟧ - 2" by simp

lemma nth_fibs:
  assumes "defined i" and "⟦ i ⟧ ≥ 0" shows "defined (fibs !! i)" and "⟦ fibs !! i ⟧ = fib ⟦ i ⟧"
  using assms
proof(induction i rule:nonneg_full_Int_induct)
  case (Suc i)
  case 1
  with Suc show ?case
    apply (cases "⟦i⟧ = 0")
     apply (subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)
    apply (cases "⟦i⟧ = 1")
     apply (subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)
    apply (subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)
    done
qed (subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)+

end