src/HOL/NumberTheory/Fib.thy
author wenzelm
Mon Oct 15 20:42:06 2001 +0200 (2001-10-15)
changeset 11786 51ce34ef5113
parent 11704 3c50a2cd6f00
child 11868 56db9f3a6b3e
permissions -rw-r--r--
setsum syntax;
wenzelm@11049
     1
(*  Title:      HOL/NumberTheory/Fib.thy
paulson@9944
     2
    ID:         $Id$
paulson@9944
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@9944
     4
    Copyright   1997  University of Cambridge
paulson@9944
     5
*)
paulson@9944
     6
wenzelm@11049
     7
header {* The Fibonacci function *}
wenzelm@11049
     8
wenzelm@11049
     9
theory Fib = Primes:
wenzelm@11049
    10
wenzelm@11049
    11
text {*
wenzelm@11049
    12
  Fibonacci numbers: proofs of laws taken from:
wenzelm@11049
    13
  R. L. Graham, D. E. Knuth, O. Patashnik.  Concrete Mathematics.
wenzelm@11049
    14
  (Addison-Wesley, 1989)
wenzelm@11049
    15
wenzelm@11049
    16
  \bigskip
wenzelm@11049
    17
*}
wenzelm@11049
    18
wenzelm@11049
    19
consts fib :: "nat => nat"
wenzelm@11049
    20
recdef fib  less_than
paulson@11468
    21
  zero: "fib 0  = 0"
wenzelm@11701
    22
  one:  "fib (Suc 0) = Suc 0"
wenzelm@11049
    23
  Suc_Suc: "fib (Suc (Suc x)) = fib x + fib (Suc x)"
wenzelm@11049
    24
wenzelm@11049
    25
text {*
wenzelm@11049
    26
  \medskip The difficulty in these proofs is to ensure that the
wenzelm@11049
    27
  induction hypotheses are applied before the definition of @{term
wenzelm@11049
    28
  fib}.  Towards this end, the @{term fib} equations are not declared
wenzelm@11049
    29
  to the Simplifier and are applied very selectively at first.
wenzelm@11049
    30
*}
wenzelm@11049
    31
wenzelm@11049
    32
declare fib.Suc_Suc [simp del]
wenzelm@11049
    33
wenzelm@11049
    34
lemma fib_Suc3: "fib (Suc (Suc (Suc n))) = fib (Suc n) + fib (Suc (Suc n))"
wenzelm@11049
    35
  apply (rule fib.Suc_Suc)
wenzelm@11049
    36
  done
wenzelm@11049
    37
wenzelm@11049
    38
wenzelm@11049
    39
text {* \medskip Concrete Mathematics, page 280 *}
wenzelm@11049
    40
wenzelm@11049
    41
lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
wenzelm@11049
    42
  apply (induct n rule: fib.induct)
wenzelm@11049
    43
    prefer 3
wenzelm@11049
    44
    txt {* simplify the LHS just enough to apply the induction hypotheses *}
wenzelm@11049
    45
    apply (simp add: fib.Suc_Suc [of "Suc (m + n)", standard])
wenzelm@11049
    46
    apply (simp_all (no_asm_simp) add: fib.Suc_Suc add_mult_distrib add_mult_distrib2)
wenzelm@11049
    47
    done
wenzelm@11049
    48
wenzelm@11049
    49
lemma fib_Suc_neq_0 [simp]: "fib (Suc n) \<noteq> 0"
wenzelm@11049
    50
  apply (induct n rule: fib.induct)
wenzelm@11049
    51
    apply (simp_all add: fib.Suc_Suc)
wenzelm@11049
    52
  done
wenzelm@11049
    53
wenzelm@11049
    54
lemma [simp]: "0 < fib (Suc n)"
wenzelm@11049
    55
  apply (simp add: neq0_conv [symmetric])
wenzelm@11049
    56
  done
wenzelm@11049
    57
wenzelm@11049
    58
lemma fib_gr_0: "0 < n ==> 0 < fib n"
wenzelm@11049
    59
  apply (rule not0_implies_Suc [THEN exE])
wenzelm@11049
    60
   apply auto
wenzelm@11049
    61
  done
wenzelm@11049
    62
paulson@9944
    63
wenzelm@11049
    64
text {*
wenzelm@11049
    65
  \medskip Concrete Mathematics, page 278: Cassini's identity.  It is
wenzelm@11049
    66
  much easier to prove using integers!
wenzelm@11049
    67
*}
wenzelm@11049
    68
wenzelm@11049
    69
lemma fib_Cassini: "int (fib (Suc (Suc n)) * fib n) =
wenzelm@11704
    70
  (if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - Numeral1
wenzelm@11701
    71
   else int (fib (Suc n) * fib (Suc n)) + Numeral1)"
wenzelm@11049
    72
  apply (induct n rule: fib.induct)
wenzelm@11049
    73
    apply (simp add: fib.Suc_Suc)
wenzelm@11049
    74
   apply (simp add: fib.Suc_Suc mod_Suc)
wenzelm@11049
    75
  apply (simp add: fib.Suc_Suc
wenzelm@11049
    76
    add_mult_distrib add_mult_distrib2 mod_Suc zmult_int [symmetric] zmult_ac)
wenzelm@11704
    77
  apply (subgoal_tac "x mod 2 < 2", arith)
paulson@11377
    78
  apply simp
wenzelm@11049
    79
  done
wenzelm@11049
    80
wenzelm@11049
    81
wenzelm@11049
    82
text {* \medskip Towards Law 6.111 of Concrete Mathematics *}
wenzelm@11049
    83
wenzelm@11701
    84
lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = Suc 0"
wenzelm@11049
    85
  apply (induct n rule: fib.induct)
wenzelm@11049
    86
    prefer 3
wenzelm@11049
    87
    apply (simp add: gcd_commute fib_Suc3)
wenzelm@11049
    88
   apply (simp_all add: fib.Suc_Suc)
wenzelm@11049
    89
  done
wenzelm@11049
    90
wenzelm@11049
    91
lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"
wenzelm@11049
    92
  apply (simp (no_asm) add: gcd_commute [of "fib m"])
wenzelm@11049
    93
  apply (case_tac "m = 0")
wenzelm@11049
    94
   apply simp
wenzelm@11049
    95
  apply (clarify dest!: not0_implies_Suc)
wenzelm@11049
    96
  apply (simp add: fib_add)
wenzelm@11049
    97
  apply (simp add: add_commute gcd_non_0)
wenzelm@11049
    98
  apply (simp add: gcd_non_0 [symmetric])
wenzelm@11049
    99
  apply (simp add: gcd_fib_Suc_eq_1 gcd_mult_cancel)
wenzelm@11049
   100
  done
wenzelm@11049
   101
wenzelm@11049
   102
lemma gcd_fib_diff: "m \<le> n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"
wenzelm@11049
   103
  apply (rule gcd_fib_add [symmetric, THEN trans])
wenzelm@11049
   104
  apply simp
wenzelm@11049
   105
  done
wenzelm@11049
   106
wenzelm@11049
   107
lemma gcd_fib_mod: "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
wenzelm@11049
   108
  apply (induct n rule: nat_less_induct)
wenzelm@11049
   109
  apply (subst mod_if)
wenzelm@11049
   110
  apply (simp add: gcd_fib_diff mod_geq not_less_iff_le diff_less)
wenzelm@11049
   111
  done
wenzelm@11049
   112
wenzelm@11049
   113
lemma fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)"  -- {* Law 6.111 *}
wenzelm@11049
   114
  apply (induct m n rule: gcd_induct)
wenzelm@11049
   115
   apply simp
wenzelm@11049
   116
  apply (simp add: gcd_non_0)
wenzelm@11049
   117
  apply (simp add: gcd_commute gcd_fib_mod)
wenzelm@11049
   118
  done
wenzelm@11049
   119
wenzelm@11049
   120
lemma fib_mult_eq_setsum:
wenzelm@11786
   121
    "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
wenzelm@11049
   122
  apply (induct n rule: fib.induct)
wenzelm@11049
   123
    apply (auto simp add: atMost_Suc fib.Suc_Suc)
wenzelm@11049
   124
  apply (simp add: add_mult_distrib add_mult_distrib2)
wenzelm@11049
   125
  done
paulson@9944
   126
paulson@9944
   127
end