author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 37672  645eb9fec794 
child 54892  64c2d4f8d981 
permissions  rwrr 
33026  1 
(* Title: HOL/Isar_Examples/Fibonacci.thy 
8051  2 
Author: Gertrud Bauer 
3 
Copyright 1999 Technische Universitaet Muenchen 

4 

5 
The Fibonacci function. Demonstrates the use of recdef. Original 

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 
(AddisonWesley, 1989) 

13 
*) 

14 

10007  15 
header {* Fib and Gcd commute *} 
8051  16 

27366  17 
theory Fibonacci 
37672  18 
imports "../Number_Theory/Primes" 
27366  19 
begin 
8051  20 

37671  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{ConcreteMath}.} *} 

8051  24 

25 

37672  26 
declare One_nat_def [simp] 
27 

28 

10007  29 
subsection {* Fibonacci numbers *} 
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 

10007  40 
text {* Alternative induction rule. *} 
8051  41 

8304  42 
theorem fib_induct: 
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

43 
"P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)" 
18153  44 
by (induct rule: fib.induct) simp_all 
8051  45 

46 

10007  47 
subsection {* Fib and gcd commute *} 
8051  48 

10007  49 
text {* A few laws taken from \cite{ConcreteMath}. *} 
8051  50 

9659  51 
lemma fib_add: 
8051  52 
"fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n" 
9659  53 
(is "?P n") 
10007  54 
 {* see \cite[page 280]{ConcreteMath} *} 
11809  55 
proof (induct n rule: fib_induct) 
10007  56 
show "?P 0" by simp 
57 
show "?P 1" by simp 

58 
fix n 

11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

59 
have "fib (n + 2 + k + 1) 
10007  60 
= fib (n + k + 1) + fib (n + 1 + k + 1)" by simp 
61 
also assume "fib (n + k + 1) 

8051  62 
= fib (k + 1) * fib (n + 1) + fib k * fib n" 
10007  63 
(is " _ = ?R1") 
64 
also assume "fib (n + 1 + k + 1) 

8051  65 
= fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)" 
10007  66 
(is " _ = ?R2") 
67 
also have "?R1 + ?R2 

11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

68 
= fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)" 
10007  69 
by (simp add: add_mult_distrib2) 
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

70 
finally show "?P (n + 2)" . 
10007  71 
qed 
8051  72 

27556  73 
lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1" (is "?P n") 
11809  74 
proof (induct n rule: fib_induct) 
10007  75 
show "?P 0" by simp 
76 
show "?P 1" by simp 

77 
fix n 

11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

78 
have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)" 
10007  79 
by simp 
37672  80 
also have "... = fib (n + 2) + fib (n + 1)" by simp 
27556  81 
also have "gcd (fib (n + 2)) ... = gcd (fib (n + 2)) (fib (n + 1))" 
37672  82 
by (rule gcd_add2_nat) 
27556  83 
also have "... = gcd (fib (n + 1)) (fib (n + 1 + 1))" 
37672  84 
by (simp add: gcd_commute_nat) 
10007  85 
also assume "... = 1" 
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

86 
finally show "?P (n + 2)" . 
10007  87 
qed 
8051  88 

37672  89 
lemma gcd_mult_add: "(0::nat) < n ==> gcd (n * k + m) n = gcd m n" 
10007  90 
proof  
91 
assume "0 < n" 

27556  92 
then have "gcd (n * k + m) n = gcd n (m mod n)" 
37672  93 
by (simp add: gcd_non_0_nat add_commute) 
94 
also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0_nat) 

10007  95 
finally show ?thesis . 
96 
qed 

8051  97 

27556  98 
lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)" 
10007  99 
proof (cases m) 
18153  100 
case 0 
101 
then show ?thesis by simp 

10007  102 
next 
18153  103 
case (Suc k) 
27556  104 
then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))" 
37672  105 
by (simp add: gcd_commute_nat) 
10007  106 
also have "fib (n + k + 1) 
37671  107 
= fib (k + 1) * fib (n + 1) + fib k * fib n" 
10007  108 
by (rule fib_add) 
27556  109 
also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))" 
10007  110 
by (simp add: gcd_mult_add) 
27556  111 
also have "... = gcd (fib n) (fib (k + 1))" 
37672  112 
by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel_nat) 
27556  113 
also have "... = gcd (fib m) (fib n)" 
37672  114 
using Suc by (simp add: gcd_commute_nat) 
10007  115 
finally show ?thesis . 
116 
qed 

8051  117 

9659  118 
lemma gcd_fib_diff: 
18153  119 
assumes "m <= n" 
27556  120 
shows "gcd (fib m) (fib (n  m)) = gcd (fib m) (fib n)" 
10007  121 
proof  
27556  122 
have "gcd (fib m) (fib (n  m)) = gcd (fib m) (fib (n  m + m))" 
10007  123 
by (simp add: gcd_fib_add) 
18153  124 
also from `m <= n` have "n  m + m = n" by simp 
10007  125 
finally show ?thesis . 
126 
qed 

8051  127 

9659  128 
lemma gcd_fib_mod: 
18241  129 
assumes "0 < m" 
27556  130 
shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" 
18153  131 
proof (induct n rule: nat_less_induct) 
132 
case (1 n) note hyp = this 

133 
show ?case 

134 
proof  

135 
have "n mod m = (if n < m then n else (n  m) mod m)" 

136 
by (rule mod_if) 

27556  137 
also have "gcd (fib m) (fib ...) = gcd (fib m) (fib n)" 
18153  138 
proof (cases "n < m") 
139 
case True then show ?thesis by simp 

140 
next 

141 
case False then have "m <= n" by simp 

18241  142 
from `0 < m` and False have "n  m < n" by simp 
27556  143 
with hyp have "gcd (fib m) (fib ((n  m) mod m)) 
37671  144 
= gcd (fib m) (fib (n  m))" by simp 
27556  145 
also have "... = gcd (fib m) (fib n)" 
18153  146 
using `m <= n` by (rule gcd_fib_diff) 
27556  147 
finally have "gcd (fib m) (fib ((n  m) mod m)) = 
37671  148 
gcd (fib m) (fib n)" . 
18153  149 
with False show ?thesis by simp 
10408  150 
qed 
18153  151 
finally show ?thesis . 
10007  152 
qed 
153 
qed 

8051  154 

27556  155 
theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n") 
37672  156 
proof (induct m n rule: gcd_nat_induct) 
27556  157 
fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp 
10007  158 
fix n :: nat assume n: "0 < n" 
37672  159 
then have "gcd m n = gcd n (m mod n)" by (simp add: gcd_non_0_nat) 
27556  160 
also assume hyp: "fib ... = gcd (fib n) (fib (m mod n))" 
161 
also from n have "... = gcd (fib n) (fib m)" by (rule gcd_fib_mod) 

37672  162 
also have "... = gcd (fib m) (fib n)" by (rule gcd_commute_nat) 
27556  163 
finally show "fib (gcd m n) = gcd (fib m) (fib n)" . 
10007  164 
qed 
8051  165 

10007  166 
end 