src/HOL/Isar_examples/Fibonacci.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 16417 9bc16273c2d4 child 18153 a084aa91f701 permissions -rw-r--r--
Constant "If" is now local
1 (*  Title:      HOL/Isar_examples/Fibonacci.thy
2     ID:         \$Id\$
3     Author:     Gertrud Bauer
4     Copyright   1999 Technische Universitaet Muenchen
6 The Fibonacci function.  Demonstrates the use of recdef.  Original
7 tactic script by Lawrence C Paulson.
9 Fibonacci numbers: proofs of laws taken from
11   R. L. Graham, D. E. Knuth, O. Patashnik.
12   Concrete Mathematics.
14 *)
16 header {* Fib and Gcd commute *}
18 theory Fibonacci imports Primes begin
20 text_raw {*
21  \footnote{Isar version by Gertrud Bauer.  Original tactic script by
22  Larry Paulson.  A few proofs of laws taken from
23  \cite{Concrete-Math}.}
24 *}
27 subsection {* Fibonacci numbers *}
29 consts fib :: "nat => nat"
30 recdef fib less_than
31  "fib 0 = 0"
32  "fib (Suc 0) = 1"
33  "fib (Suc (Suc x)) = fib x + fib (Suc x)"
35 lemma [simp]: "0 < fib (Suc n)"
36   by (induct n rule: fib.induct) (simp+)
39 text {* Alternative induction rule. *}
41 theorem fib_induct:
42     "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)"
43   by (induct rule: fib.induct, simp+)
47 subsection {* Fib and gcd commute *}
49 text {* A few laws taken from \cite{Concrete-Math}. *}
52   "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
53   (is "?P n")
54   -- {* see \cite[page 280]{Concrete-Math} *}
55 proof (induct n rule: fib_induct)
56   show "?P 0" by simp
57   show "?P 1" by simp
58   fix n
59   have "fib (n + 2 + k + 1)
60     = fib (n + k + 1) + fib (n + 1 + k + 1)" by simp
61   also assume "fib (n + k + 1)
62     = fib (k + 1) * fib (n + 1) + fib k * fib n"
63       (is " _ = ?R1")
64   also assume "fib (n + 1 + k + 1)
65     = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
66       (is " _ = ?R2")
67   also have "?R1 + ?R2
68     = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
70   finally show "?P (n + 2)" .
71 qed
73 lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n")
74 proof (induct n rule: fib_induct)
75   show "?P 0" by simp
76   show "?P 1" by simp
77   fix n
78   have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
79     by simp
80   also have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))"
81     by (simp only: gcd_add2')
82   also have "... = gcd (fib (n + 1), fib (n + 1 + 1))"
83     by (simp add: gcd_commute)
84   also assume "... = 1"
85   finally show "?P (n + 2)" .
86 qed
88 lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)"
89 proof -
90   assume "0 < n"
91   hence "gcd (n * k + m, n) = gcd (n, m mod n)"
93   also have "... = gcd (m, n)" by (simp! add: gcd_non_0)
94   finally show ?thesis .
95 qed
97 lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"
98 proof (cases m)
99   assume "m = 0"
100   thus ?thesis by simp
101 next
102   fix k assume "m = Suc k"
103   hence "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))"
104     by (simp add: gcd_commute)
105   also have "fib (n + k + 1)
106     = fib (k + 1) * fib (n + 1) + fib k * fib n"
107     by (rule fib_add)
108   also have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))"
110   also have "... = gcd (fib n, fib (k + 1))"
111     by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
112   also have "... = gcd (fib m, fib n)"
113     by (simp! add: gcd_commute)
114   finally show ?thesis .
115 qed
117 lemma gcd_fib_diff:
118   "m <= n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"
119 proof -
120   assume "m <= n"
121   have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))"
123   also have "n - m + m = n" by (simp!)
124   finally show ?thesis .
125 qed
127 lemma gcd_fib_mod:
128   "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
129 proof -
130   assume m: "0 < m"
131   show ?thesis
132   proof (induct n rule: nat_less_induct)
133     fix n
134     assume hyp: "ALL ma. ma < n
135       --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)"
136     show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
137     proof -
138       have "n mod m = (if n < m then n else (n - m) mod m)"
139 	by (rule mod_if)
140       also have "gcd (fib m, fib ...) = gcd (fib m, fib n)"
141       proof cases
142 	assume "n < m" thus ?thesis by simp
143       next
144 	assume not_lt: "~ n < m" hence le: "m <= n" by simp
145 	have "n - m < n" by (simp!)
146 	with hyp have "gcd (fib m, fib ((n - m) mod m))
147 	  = gcd (fib m, fib (n - m))" by simp
148 	also from le have "... = gcd (fib m, fib n)"
149 	  by (rule gcd_fib_diff)
150 	finally have "gcd (fib m, fib ((n - m) mod m)) =
151 	  gcd (fib m, fib n)" .
152 	with not_lt show ?thesis by simp
153       qed
154       finally show ?thesis .
155     qed
156   qed
157 qed
160 theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n")
161 proof (induct m n rule: gcd_induct)
162   fix m show "fib (gcd (m, 0)) = gcd (fib m, fib 0)" by simp
163   fix n :: nat assume n: "0 < n"
164   hence "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0)
165   also assume hyp: "fib ... = gcd (fib n, fib (m mod n))"
166   also from n have "... = gcd (fib n, fib m)" by (rule gcd_fib_mod)
167   also have "... = gcd (fib m, fib n)" by (rule gcd_commute)
168   finally show "fib (gcd (m, n)) = gcd (fib m, fib n)" .
169 qed
171 end