src/HOL/Isar_Examples/Fibonacci.thy
 author wenzelm Tue Sep 26 20:54:40 2017 +0200 (23 months ago) changeset 66695 91500c024c7f parent 66453 cc19f7ca2ed6 child 67051 e7e54a0b9197 permissions -rw-r--r--
tuned;
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 section \<open>Fib and Gcd commute\<close>
17 theory Fibonacci
18   imports "HOL-Computational_Algebra.Primes"
19 begin
21 text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
22   Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\<close>\<close>
25 declare One_nat_def [simp]
28 subsection \<open>Fibonacci numbers\<close>
30 fun fib :: "nat \<Rightarrow> nat"
31   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 \<open>Alternative induction rule.\<close>
42 theorem fib_induct: "P 0 \<Longrightarrow> P 1 \<Longrightarrow> (\<And>n. P (n + 1) \<Longrightarrow> P n \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
43   for n :: nat
44   by (induct rule: fib.induct) simp_all
47 subsection \<open>Fib and gcd commute\<close>
49 text \<open>A few laws taken from @{cite "Concrete-Math"}.\<close>
51 lemma fib_add: "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
52   (is "?P n")
53   \<comment> \<open>see @{cite \<open>page 280\<close> "Concrete-Math"}\<close>
54 proof (induct n rule: fib_induct)
55   show "?P 0" by simp
56   show "?P 1" by simp
57   fix n
58   have "fib (n + 2 + k + 1)
59     = fib (n + k + 1) + fib (n + 1 + k + 1)" by simp
60   also assume "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n" (is " _ = ?R1")
61   also assume "fib (n + 1 + k + 1) = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
62     (is " _ = ?R2")
63   also have "?R1 + ?R2 = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
65   finally show "?P (n + 2)" .
66 qed
68 lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1"
69   (is "?P n")
70 proof (induct n rule: fib_induct)
71   show "?P 0" by simp
72   show "?P 1" by simp
73   fix n
74   have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
75     by simp
76   also have "\<dots> = fib (n + 2) + fib (n + 1)"
77     by simp
78   also have "gcd (fib (n + 2)) \<dots> = gcd (fib (n + 2)) (fib (n + 1))"
80   also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
82   also assume "\<dots> = 1"
83   finally show "?P (n + 2)" .
84 qed
86 lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n"
87 proof -
88   assume "0 < n"
89   then have "gcd (n * k + m) n = gcd n (m mod n)"
91   also from \<open>0 < n\<close> have "\<dots> = gcd m n"
93   finally show ?thesis .
94 qed
96 lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
97 proof (cases m)
98   case 0
99   then show ?thesis by simp
100 next
101   case (Suc k)
102   then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
104   also have "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
106   also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
108   also have "\<dots> = gcd (fib n) (fib (k + 1))"
109     by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
110   also have "\<dots> = gcd (fib m) (fib n)"
111     using Suc by (simp add: gcd.commute)
112   finally show ?thesis .
113 qed
115 lemma gcd_fib_diff: "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" if "m \<le> n"
116 proof -
117   have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
119   also from \<open>m \<le> n\<close> have "n - m + m = n"
120     by simp
121   finally show ?thesis .
122 qed
124 lemma gcd_fib_mod: "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" if "0 < m"
125 proof (induct n rule: nat_less_induct)
126   case hyp: (1 n)
127   show ?case
128   proof -
129     have "n mod m = (if n < m then n else (n - m) mod m)"
130       by (rule mod_if)
131     also have "gcd (fib m) (fib \<dots>) = gcd (fib m) (fib n)"
132     proof (cases "n < m")
133       case True
134       then show ?thesis by simp
135     next
136       case False
137       then have "m \<le> n" by simp
138       from \<open>0 < m\<close> and False have "n - m < n"
139         by simp
140       with hyp have "gcd (fib m) (fib ((n - m) mod m))
141           = gcd (fib m) (fib (n - m))" by simp
142       also have "\<dots> = gcd (fib m) (fib n)"
143         using \<open>m \<le> n\<close> by (rule gcd_fib_diff)
144       finally have "gcd (fib m) (fib ((n - m) mod m)) =
145           gcd (fib m) (fib n)" .
146       with False show ?thesis by simp
147     qed
148     finally show ?thesis .
149   qed
150 qed
152 theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
153   (is "?P m n")
154 proof (induct m n rule: gcd_nat_induct)
155   fix m n :: nat
156   show "fib (gcd m 0) = gcd (fib m) (fib 0)"
157     by simp
158   assume n: "0 < n"
159   then have "gcd m n = gcd n (m mod n)"