-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathFibonacci.thy
89 lines (81 loc) · 2.68 KB
/
Fibonacci.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
(* Fibonacci.thy
-- Equivalence of definitions of the Fibonacci function.
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Seville, August 29, 2024
-- ------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
-- In Isabelle/HOL, the Fibonacci function can be defined as
-- fun fibonacci :: "nat \<Rightarrow> nat"
-- where
-- "fibonacci 0 = 0"
-- | "fibonacci (Suc 0) = 1"
-- | "fibonacci (Suc (Suc n)) = fibonacci n + fibonacci (Suc n)"
--
-- Another definition is
-- fun fibAux :: "nat => nat × nat"
-- where
-- "fibAux 0 = (0, 1)"
-- | "fibAux (Suc n) = (let (a, b) = fibAux n in (b, a + b))"
--
-- definition fib :: "nat \<Rightarrow> nat" where
-- "fib n = (fst (fibAux n))"
--
-- Prove that both definitions are equivalent; that is,
-- fibonacci n = fib n
-- ------------------------------------------------------------------ *)
theory Fibonacci
imports Main
begin
fun fibonacci :: "nat ⇒ nat"
where
"fibonacci 0 = 0"
| "fibonacci (Suc 0) = 1"
| "fibonacci (Suc (Suc n)) = fibonacci n + fibonacci (Suc n)"
fun fibAux :: "nat => nat × nat"
where
"fibAux 0 = (0, 1)"
| "fibAux (Suc n) = (let (a, b) = fibAux n in (b, a + b))"
definition fib :: "nat ⇒ nat" where
"fib n = fst (fibAux n)"
lemma fib_suma :
"fib (Suc (Suc n)) = fib n + fib (Suc n)"
proof (induct n)
show "fib (Suc (Suc 0)) = fib 0 + fib (Suc 0)"
by (simp add: fib_def)
next
fix n
assume IH : "fib (Suc (Suc n)) = fib n + fib (Suc n)"
have "fib (Suc (Suc (Suc n))) = fst (fibAux (Suc (Suc (Suc n))))"
by (simp add: fib_def)
also have "… = snd (fibAux (Suc (Suc n)))"
by (simp add: prod.case_eq_if)
also have "… = fst (fibAux (Suc n)) + snd (fibAux (Suc n))"
by (metis fibAux.simps(2) snd_conv split_def)
also have "… = fib (Suc n) + snd (fibAux (Suc n))"
using fib_def by auto
also have "… = fib (Suc n) + fib (Suc (Suc n))"
by (simp add: fib_def prod.case_eq_if)
finally show "fib (Suc (Suc (Suc n))) = fib (Suc n) + fib (Suc (Suc n))"
by this
qed
lemma "fibonacci n = fib n"
proof (induct n rule: fibonacci.induct)
show "fibonacci 0 = fib 0"
by (simp add: fib_def)
next
show "fibonacci (Suc 0) = fib (Suc 0)"
by (simp add: fib_def)
next
fix n
assume IH1 : "fibonacci n = fib n"
assume IH2 : "fibonacci (Suc n) = fib (Suc n)"
have "fibonacci (Suc (Suc n)) = fibonacci n + fibonacci (Suc n)"
by simp
also have "… = fib n + fib (Suc n)"
by (simp add: IH1 IH2)
also have "… = fib (Suc (Suc n))"
by (simp add: fib_suma)
finally show "fibonacci (Suc (Suc n)) = fib (Suc (Suc n))"
by this
qed
end