src/HOL/Number_Theory/Fib.thy
author haftmann
Fri, 04 Jul 2014 20:18:47 +0200
changeset 57512 cc97b347b301
parent 54713 6666fc0b9ebc
child 58889 5b7a9633cfa8
permissions -rw-r--r--
reduced name variants for assoc and commute on plus and mult
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 41541
diff changeset
     1
(*  Title:      HOL/Number_Theory/Fib.thy
b460124855b8 tuned headers;
wenzelm
parents: 41541
diff changeset
     2
    Author:     Lawrence C. Paulson
b460124855b8 tuned headers;
wenzelm
parents: 41541
diff changeset
     3
    Author:     Jeremy Avigad
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     4
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     5
Defines the fibonacci function.
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     6
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     7
The original "Fib" is due to Lawrence C. Paulson, and was adapted by
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     8
Jeremy Avigad.
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     9
*)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    10
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    11
header {* Fib *}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    12
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    13
theory Fib
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    14
imports Binomial
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    15
begin
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    16
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    17
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    18
subsection {* Main definitions *}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    19
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    20
fun fib :: "nat \<Rightarrow> nat"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    21
where
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    22
    fib0: "fib 0 = 0"
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    23
  | fib1: "fib (Suc 0) = 1"
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    24
  | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    25
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    26
subsection {* Fibonacci numbers *}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    27
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    28
lemma fib_1 [simp]: "fib (1::nat) = 1"
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    29
  by (metis One_nat_def fib1)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    30
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    31
lemma fib_2 [simp]: "fib (2::nat) = 1"
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    32
  using fib.simps(3) [of 0]
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    33
  by (simp add: numeral_2_eq_2)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    34
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    35
lemma fib_plus_2: "fib (n + 2) = fib (n + 1) + fib n"
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    36
  by (metis Suc_eq_plus1 add_2_eq_Suc' fib.simps(3))
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    37
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    38
lemma fib_add: "fib (Suc (n+k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    39
  by (induct n rule: fib.induct) (auto simp add: field_simps)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    40
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    41
lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    42
  by (induct n rule: fib.induct) (auto simp add: )
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    43
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    44
text {*
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    45
  \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    46
  much easier using integers, not natural numbers!
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    47
*}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    48
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    49
lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    50
  by (induction n rule: fib.induct)  (auto simp add: field_simps power2_eq_square power_add)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    51
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    52
lemma fib_Cassini_nat:
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    53
    "fib (Suc (Suc n)) * fib n =
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    54
       (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    55
using fib_Cassini_int [of n] by auto
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    56
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    57
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    58
text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    59
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    60
lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    61
  apply (induct n rule: fib.induct)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    62
  apply auto
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 54713
diff changeset
    63
  apply (metis gcd_add1_nat add.commute)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    64
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    65
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    66
lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
    67
  apply (simp add: gcd_commute_nat [of "fib m"])
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    68
  apply (cases m)
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    69
  apply (auto simp add: fib_add)
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
    70
  apply (subst gcd_commute_nat)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 54713
diff changeset
    71
  apply (subst mult.commute)
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    72
  apply (metis coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    73
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    74
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    75
lemma gcd_fib_diff: "m \<le> n \<Longrightarrow>
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    76
    gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    77
  by (simp add: gcd_fib_add [symmetric, of _ "n-m"])
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    78
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    79
lemma gcd_fib_mod: "0 < m \<Longrightarrow>
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    80
    gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    81
proof (induct n rule: less_induct)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    82
  case (less n)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    83
  from less.prems have pos_m: "0 < m" .
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    84
  show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    85
  proof (cases "m < n")
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    86
    case True
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    87
    then have "m \<le> n" by auto
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    88
    with pos_m have pos_n: "0 < n" by auto
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    89
    with pos_m `m < n` have diff: "n - m < n" by auto
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    90
    have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    91
      by (simp add: mod_if [of n]) (insert `m < n`, auto)
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    92
    also have "\<dots> = gcd (fib m)  (fib (n - m))"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    93
      by (simp add: less.hyps diff pos_m)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    94
    also have "\<dots> = gcd (fib m) (fib n)"
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    95
      by (simp add: gcd_fib_diff `m \<le> n`)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    96
    finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    97
  next
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    98
    case False
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    99
    then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   100
      by (cases "m = n") auto
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   101
  qed
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   102
qed
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   103
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
   104
lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   105
    -- {* Law 6.111 *}
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
   106
  by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   107
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   108
theorem fib_mult_eq_setsum_nat:
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   109
    "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
   110
  by (induct n rule: nat.induct) (auto simp add:  field_simps)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   111
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   112
end
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
   113