Complete this form and hit the "Save Changes" button!
No ratings
Are you sure you want to delete this code? Please type DELETE in the box below to confirm.
Are you sure you want to verify this code?
Are you sure you want to publish this code?
Are you sure you want to unpublish this code?
Are you sure you want to autogenerate the summary + description for this code?
xxxxxxxxxx
theory IsabelleFibTest
imports Main
begin
text "The code in this file is from https://isabelle.in.tum.de/doc/codegen.pdf"
section "The specification for Fibonnaci"
fun fib :: "nat \<Rightarrow> nat" where
"fib 0 = 0" |
"fib (Suc 0) = Suc 0" |
"fib (Suc (Suc n)) = fib n + fib (Suc n)"
value "fib (Suc 0)"
value "fib (Suc (Suc 0))"
value "fib (Suc (Suc (Suc 0)))"
value "fib (Suc (Suc (Suc (Suc 0))))"
value "fib (Suc (Suc (Suc (Suc (Suc 0)))))"
value "fib (Suc (Suc (Suc (Suc (Suc (Suc 0))))))"
definition fib_step :: "nat \<Rightarrow> nat \<times> nat" where
"fib_step n = (fib (Suc n), fib n)"
section "The proofs for the correctness of the implementation wrt the specification"
lemma [code]:
"fib_step 0 = (Suc 0, 0)"
"fib_step (Suc n) = (let (m, q) = fib_step n in (m + q, m))"
by (simp_all add: fib_step_def )
lemma fib [code]:
"fib 0 = 0"
"fib (Suc n) = fst (fib_step n)"
section "The executable code for Fibonnaci is generated"
export_code
fib
in Haskell
end
