src/HOL/Isar_Examples/Fibonacci.thy
 author blanchet Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) changeset 58306 117ba6cbe414 parent 57512 cc97b347b301 child 58614 7338eb25226c permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
1 (*  Title:      HOL/Isar_Examples/Fibonacci.thy
2     Author:     Gertrud Bauer
3     Copyright   1999 Technische Universitaet Muenchen
5 The Fibonacci function.  Original
6 tactic script by Lawrence C Paulson.
8 Fibonacci numbers: proofs of laws taken from
10   R. L. Graham, D. E. Knuth, O. Patashnik.
11   Concrete Mathematics.
13 *)
15 header {* Fib and Gcd commute *}
17 theory Fibonacci
18 imports "../Number_Theory/Primes"
19 begin
21 text_raw {* \footnote{Isar version by Gertrud Bauer.  Original tactic
22   script by Larry Paulson.  A few proofs of laws taken from
23   \cite{Concrete-Math}.} *}
26 declare One_nat_def [simp]
29 subsection {* Fibonacci numbers *}
31 fun fib :: "nat \<Rightarrow> nat" where
32   "fib 0 = 0"
33 | "fib (Suc 0) = 1"
34 | "fib (Suc (Suc x)) = fib x + fib (Suc x)"
36 lemma [simp]: "fib (Suc n) > 0"
37   by (induct n rule: fib.induct) simp_all
40 text {* Alternative induction rule. *}
42 theorem fib_induct:
43   fixes n :: nat
44   shows "P 0 \<Longrightarrow> P 1 \<Longrightarrow> (\<And>n. P (n + 1) \<Longrightarrow> P n \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
45   by (induct rule: fib.induct) simp_all
48 subsection {* Fib and gcd commute *}
50 text {* A few laws taken from \cite{Concrete-Math}. *}
53   "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
54   (is "?P n")
55   -- {* see \cite[page 280]{Concrete-Math} *}
56 proof (induct n rule: fib_induct)
57   show "?P 0" by simp
58   show "?P 1" by simp
59   fix n
60   have "fib (n + 2 + k + 1)
61     = fib (n + k + 1) + fib (n + 1 + k + 1)" by simp
62   also assume "fib (n + k + 1)
63     = fib (k + 1) * fib (n + 1) + fib k * fib n"
64       (is " _ = ?R1")
65   also assume "fib (n + 1 + k + 1)
66     = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
67       (is " _ = ?R2")
68   also have "?R1 + ?R2
69     = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
71   finally show "?P (n + 2)" .
72 qed
74 lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1" (is "?P n")
75 proof (induct n rule: fib_induct)
76   show "?P 0" by simp
77   show "?P 1" by simp
78   fix n
79   have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
80     by simp
81   also have "\<dots> = fib (n + 2) + fib (n + 1)"
82     by simp
83   also have "gcd (fib (n + 2)) \<dots> = gcd (fib (n + 2)) (fib (n + 1))"
84     by (rule gcd_add2_nat)
85   also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
86     by (simp add: gcd_commute_nat)
87   also assume "\<dots> = 1"
88   finally show "?P (n + 2)" .
89 qed
91 lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n"
92 proof -
93   assume "0 < n"
94   then have "gcd (n * k + m) n = gcd n (m mod n)"
96   also from `0 < n` have "\<dots> = gcd m n"
97     by (simp add: gcd_non_0_nat)
98   finally show ?thesis .
99 qed
101 lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
102 proof (cases m)
103   case 0
104   then show ?thesis by simp
105 next
106   case (Suc k)
107   then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
108     by (simp add: gcd_commute_nat)
109   also have "fib (n + k + 1)
110       = fib (k + 1) * fib (n + 1) + fib k * fib n"
111     by (rule fib_add)
112   also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
114   also have "\<dots> = gcd (fib n) (fib (k + 1))"
115     by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel_nat)
116   also have "\<dots> = gcd (fib m) (fib n)"
117     using Suc by (simp add: gcd_commute_nat)
118   finally show ?thesis .
119 qed
121 lemma gcd_fib_diff:
122   assumes "m \<le> n"
123   shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
124 proof -
125   have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
127   also from `m \<le> n` have "n - m + m = n"
128     by simp
129   finally show ?thesis .
130 qed
132 lemma gcd_fib_mod:
133   assumes "0 < m"
134   shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
135 proof (induct n rule: nat_less_induct)
136   case (1 n) note hyp = this
137   show ?case
138   proof -
139     have "n mod m = (if n < m then n else (n - m) mod m)"
140       by (rule mod_if)
141     also have "gcd (fib m) (fib \<dots>) = gcd (fib m) (fib n)"
142     proof (cases "n < m")
143       case True
144       then show ?thesis by simp
145     next
146       case False
147       then have "m \<le> n" by simp
148       from `0 < m` and False have "n - m < n"
149         by simp
150       with hyp have "gcd (fib m) (fib ((n - m) mod m))
151           = gcd (fib m) (fib (n - m))" by simp
152       also have "\<dots> = gcd (fib m) (fib n)"
153         using `m \<le> n` by (rule gcd_fib_diff)
154       finally have "gcd (fib m) (fib ((n - m) mod m)) =
155           gcd (fib m) (fib n)" .
156       with False show ?thesis by simp
157     qed
158     finally show ?thesis .
159   qed
160 qed
162 theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n")
163 proof (induct m n rule: gcd_nat_induct)
164   fix m
165   show "fib (gcd m 0) = gcd (fib m) (fib 0)"
166     by simp
167   fix n :: nat
168   assume n: "0 < n"
169   then have "gcd m n = gcd n (m mod n)"
170     by (simp add: gcd_non_0_nat)
171   also assume hyp: "fib \<dots> = gcd (fib n) (fib (m mod n))"
172   also from n have "\<dots> = gcd (fib n) (fib m)"
173     by (rule gcd_fib_mod)
174   also have "\<dots> = gcd (fib m) (fib n)"
175     by (rule gcd_commute_nat)
176   finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
177 qed
179 end