author | wenzelm |
Sun, 02 Nov 2014 17:23:48 +0100 | |
changeset 58882 | 6e2010ab8bd9 |
parent 58614 | 7338eb25226c |
child 61799 | 4cf66f21b764 |
permissions | -rw-r--r-- |
33026 | 1 |
(* Title: HOL/Isar_Examples/Fibonacci.thy |
8051 | 2 |
Author: Gertrud Bauer |
3 |
Copyright 1999 Technische Universitaet Muenchen |
|
4 |
||
54892 | 5 |
The Fibonacci function. Original |
8051 | 6 |
tactic script by Lawrence C Paulson. |
7 |
||
8 |
Fibonacci numbers: proofs of laws taken from |
|
9 |
||
10 |
R. L. Graham, D. E. Knuth, O. Patashnik. |
|
11 |
Concrete Mathematics. |
|
12 |
(Addison-Wesley, 1989) |
|
13 |
*) |
|
14 |
||
58882 | 15 |
section \<open>Fib and Gcd commute\<close> |
8051 | 16 |
|
27366 | 17 |
theory Fibonacci |
37672 | 18 |
imports "../Number_Theory/Primes" |
27366 | 19 |
begin |
8051 | 20 |
|
58614 | 21 |
text_raw \<open>\footnote{Isar version by Gertrud Bauer. Original tactic |
37671 | 22 |
script by Larry Paulson. A few proofs of laws taken from |
58614 | 23 |
@{cite "Concrete-Math"}.}\<close> |
8051 | 24 |
|
25 |
||
37672 | 26 |
declare One_nat_def [simp] |
27 |
||
28 |
||
58614 | 29 |
subsection \<open>Fibonacci numbers\<close> |
8051 | 30 |
|
27366 | 31 |
fun fib :: "nat \<Rightarrow> nat" where |
18153 | 32 |
"fib 0 = 0" |
37671 | 33 |
| "fib (Suc 0) = 1" |
34 |
| "fib (Suc (Suc x)) = fib x + fib (Suc x)" |
|
8051 | 35 |
|
37672 | 36 |
lemma [simp]: "fib (Suc n) > 0" |
18153 | 37 |
by (induct n rule: fib.induct) simp_all |
8051 | 38 |
|
39 |
||
58614 | 40 |
text \<open>Alternative induction rule.\<close> |
8051 | 41 |
|
8304 | 42 |
theorem fib_induct: |
55640 | 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" |
|
18153 | 45 |
by (induct rule: fib.induct) simp_all |
8051 | 46 |
|
47 |
||
58614 | 48 |
subsection \<open>Fib and gcd commute\<close> |
8051 | 49 |
|
58614 | 50 |
text \<open>A few laws taken from @{cite "Concrete-Math"}.\<close> |
8051 | 51 |
|
9659 | 52 |
lemma fib_add: |
8051 | 53 |
"fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n" |
9659 | 54 |
(is "?P n") |
58614 | 55 |
-- \<open>see @{cite \<open>page 280\<close> "Concrete-Math"}\<close> |
11809 | 56 |
proof (induct n rule: fib_induct) |
10007 | 57 |
show "?P 0" by simp |
58 |
show "?P 1" by simp |
|
59 |
fix n |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
60 |
have "fib (n + 2 + k + 1) |
10007 | 61 |
= fib (n + k + 1) + fib (n + 1 + k + 1)" by simp |
62 |
also assume "fib (n + k + 1) |
|
8051 | 63 |
= fib (k + 1) * fib (n + 1) + fib k * fib n" |
10007 | 64 |
(is " _ = ?R1") |
65 |
also assume "fib (n + 1 + k + 1) |
|
8051 | 66 |
= fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)" |
10007 | 67 |
(is " _ = ?R2") |
68 |
also have "?R1 + ?R2 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
69 |
= fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)" |
10007 | 70 |
by (simp add: add_mult_distrib2) |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
71 |
finally show "?P (n + 2)" . |
10007 | 72 |
qed |
8051 | 73 |
|
27556 | 74 |
lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1" (is "?P n") |
11809 | 75 |
proof (induct n rule: fib_induct) |
10007 | 76 |
show "?P 0" by simp |
77 |
show "?P 1" by simp |
|
78 |
fix n |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
79 |
have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)" |
10007 | 80 |
by simp |
55640 | 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))" |
|
37672 | 84 |
by (rule gcd_add2_nat) |
55640 | 85 |
also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))" |
37672 | 86 |
by (simp add: gcd_commute_nat) |
55640 | 87 |
also assume "\<dots> = 1" |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
88 |
finally show "?P (n + 2)" . |
10007 | 89 |
qed |
8051 | 90 |
|
55640 | 91 |
lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n" |
10007 | 92 |
proof - |
93 |
assume "0 < n" |
|
27556 | 94 |
then have "gcd (n * k + m) n = gcd n (m mod n)" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55656
diff
changeset
|
95 |
by (simp add: gcd_non_0_nat add.commute) |
58614 | 96 |
also from \<open>0 < n\<close> have "\<dots> = gcd m n" |
55640 | 97 |
by (simp add: gcd_non_0_nat) |
10007 | 98 |
finally show ?thesis . |
99 |
qed |
|
8051 | 100 |
|
27556 | 101 |
lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)" |
10007 | 102 |
proof (cases m) |
18153 | 103 |
case 0 |
104 |
then show ?thesis by simp |
|
10007 | 105 |
next |
18153 | 106 |
case (Suc k) |
27556 | 107 |
then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))" |
37672 | 108 |
by (simp add: gcd_commute_nat) |
10007 | 109 |
also have "fib (n + k + 1) |
37671 | 110 |
= fib (k + 1) * fib (n + 1) + fib k * fib n" |
10007 | 111 |
by (rule fib_add) |
55640 | 112 |
also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))" |
10007 | 113 |
by (simp add: gcd_mult_add) |
55640 | 114 |
also have "\<dots> = gcd (fib n) (fib (k + 1))" |
37672 | 115 |
by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel_nat) |
55640 | 116 |
also have "\<dots> = gcd (fib m) (fib n)" |
37672 | 117 |
using Suc by (simp add: gcd_commute_nat) |
10007 | 118 |
finally show ?thesis . |
119 |
qed |
|
8051 | 120 |
|
9659 | 121 |
lemma gcd_fib_diff: |
55640 | 122 |
assumes "m \<le> n" |
27556 | 123 |
shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" |
10007 | 124 |
proof - |
27556 | 125 |
have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))" |
10007 | 126 |
by (simp add: gcd_fib_add) |
58614 | 127 |
also from \<open>m \<le> n\<close> have "n - m + m = n" |
55640 | 128 |
by simp |
10007 | 129 |
finally show ?thesis . |
130 |
qed |
|
8051 | 131 |
|
9659 | 132 |
lemma gcd_fib_mod: |
18241 | 133 |
assumes "0 < m" |
27556 | 134 |
shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" |
18153 | 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) |
|
55640 | 141 |
also have "gcd (fib m) (fib \<dots>) = gcd (fib m) (fib n)" |
18153 | 142 |
proof (cases "n < m") |
55640 | 143 |
case True |
144 |
then show ?thesis by simp |
|
18153 | 145 |
next |
55640 | 146 |
case False |
147 |
then have "m \<le> n" by simp |
|
58614 | 148 |
from \<open>0 < m\<close> and False have "n - m < n" |
55640 | 149 |
by simp |
27556 | 150 |
with hyp have "gcd (fib m) (fib ((n - m) mod m)) |
37671 | 151 |
= gcd (fib m) (fib (n - m))" by simp |
55640 | 152 |
also have "\<dots> = gcd (fib m) (fib n)" |
58614 | 153 |
using \<open>m \<le> n\<close> by (rule gcd_fib_diff) |
27556 | 154 |
finally have "gcd (fib m) (fib ((n - m) mod m)) = |
37671 | 155 |
gcd (fib m) (fib n)" . |
18153 | 156 |
with False show ?thesis by simp |
10408 | 157 |
qed |
18153 | 158 |
finally show ?thesis . |
10007 | 159 |
qed |
160 |
qed |
|
8051 | 161 |
|
27556 | 162 |
theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n") |
37672 | 163 |
proof (induct m n rule: gcd_nat_induct) |
55640 | 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) |
|
27556 | 176 |
finally show "fib (gcd m n) = gcd (fib m) (fib n)" . |
10007 | 177 |
qed |
8051 | 178 |
|
10007 | 179 |
end |