src/HOL/Number_Theory/Fib.thy
author haftmann
Thu, 08 Nov 2018 09:11:52 +0100
changeset 69260 0a9688695a1b
parent 67051 e7e54a0b9197
child 69597 ff784d5a5bfb
permissions -rw-r--r--
removed relics of ASCII syntax for indexed big operators
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
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
     4
    Author:     Manuel Eberl
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     5
*)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     6
60527
eb431a5651fe tuned proofs;
wenzelm
parents: 60526
diff changeset
     7
section \<open>The fibonacci function\<close>
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     8
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     9
theory Fib
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    10
  imports Complex_Main
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    11
begin
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    12
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    13
60526
fad653acf58f isabelle update_cartouches;
wenzelm
parents: 60141
diff changeset
    14
subsection \<open>Fibonacci numbers\<close>
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    15
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    16
fun fib :: "nat \<Rightarrow> nat"
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    17
  where
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    18
    fib0: "fib 0 = 0"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    19
  | fib1: "fib (Suc 0) = 1"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    20
  | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
60527
eb431a5651fe tuned proofs;
wenzelm
parents: 60526
diff changeset
    21
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    22
60526
fad653acf58f isabelle update_cartouches;
wenzelm
parents: 60141
diff changeset
    23
subsection \<open>Basic Properties\<close>
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    24
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    25
lemma fib_1 [simp]: "fib 1 = 1"
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    26
  by (metis One_nat_def fib1)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    27
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    28
lemma fib_2 [simp]: "fib 2 = 1"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    29
  using fib.simps(3) [of 0] by (simp add: numeral_2_eq_2)
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_plus_2: "fib (n + 2) = fib (n + 1) + fib n"
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    32
  by (metis Suc_eq_plus1 add_2_eq_Suc' fib.simps(3))
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    33
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    34
lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    35
  by (induct n rule: fib.induct) (auto simp add: field_simps)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    36
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    37
lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    38
  by (induct n rule: fib.induct) auto
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    39
60527
eb431a5651fe tuned proofs;
wenzelm
parents: 60526
diff changeset
    40
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    41
subsection \<open>More efficient code\<close>
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    42
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    43
text \<open>
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    44
  The naive approach is very inefficient since the branching recursion leads to many
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    45
  values of @{term fib} being computed multiple times. We can avoid this by ``remembering''
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    46
  the last two values in the sequence, yielding a tail-recursive version.
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    47
  This is far from optimal (it takes roughly $O(n\cdot M(n))$ time where $M(n)$ is the
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    48
  time required to multiply two $n$-bit integers), but much better than the naive version,
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    49
  which is exponential.
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    50
\<close>
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    51
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    52
fun gen_fib :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    53
  where
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    54
    "gen_fib a b 0 = a"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    55
  | "gen_fib a b (Suc 0) = b"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    56
  | "gen_fib a b (Suc (Suc n)) = gen_fib b (a + b) (Suc n)"
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    57
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    58
lemma gen_fib_recurrence: "gen_fib a b (Suc (Suc n)) = gen_fib a b n + gen_fib a b (Suc n)"
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    59
  by (induct a b n rule: gen_fib.induct) simp_all
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    60
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    61
lemma gen_fib_fib: "gen_fib (fib n) (fib (Suc n)) m = fib (n + m)"
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    62
  by (induct m rule: fib.induct) (simp_all del: gen_fib.simps(3) add: gen_fib_recurrence)
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    63
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    64
lemma fib_conv_gen_fib: "fib n = gen_fib 0 1 n"
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    65
  using gen_fib_fib[of 0 n] by simp
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    66
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    67
declare fib_conv_gen_fib [code]
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    68
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
    69
60526
fad653acf58f isabelle update_cartouches;
wenzelm
parents: 60141
diff changeset
    70
subsection \<open>A Few Elementary Results\<close>
60141
833adf7db7d8 New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
    71
60526
fad653acf58f isabelle update_cartouches;
wenzelm
parents: 60141
diff changeset
    72
text \<open>
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    73
  \<^medskip> Concrete Mathematics, page 278: Cassini's identity.  The proof is
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    74
  much easier using integers, not natural numbers!
60526
fad653acf58f isabelle update_cartouches;
wenzelm
parents: 60141
diff changeset
    75
\<close>
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    76
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    77
lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    78
  by (induct 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
    79
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    80
lemma fib_Cassini_nat:
60527
eb431a5651fe tuned proofs;
wenzelm
parents: 60526
diff changeset
    81
  "fib (Suc (Suc n)) * fib n =
eb431a5651fe tuned proofs;
wenzelm
parents: 60526
diff changeset
    82
     (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    83
  using fib_Cassini_int [of n] by (auto simp del: of_nat_mult of_nat_power)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    84
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    85
60526
fad653acf58f isabelle update_cartouches;
wenzelm
parents: 60141
diff changeset
    86
subsection \<open>Law 6.111 of Concrete Mathematics\<close>
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    87
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
    88
lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
    89
  apply (induct n rule: fib.induct)
67051
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
    90
    apply (simp_all add: coprime_iff_gcd_eq_1 algebra_simps)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
    91
  apply (simp add: add.assoc [symmetric])
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    92
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    93
67051
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
    94
lemma gcd_fib_add:
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
    95
  "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
    96
proof (cases m)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
    97
  case 0
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
    98
  then show ?thesis
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
    99
    by simp
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   100
next
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   101
  case (Suc q)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   102
  from coprime_fib_Suc_nat [of q]
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   103
  have "coprime (fib (Suc q)) (fib q)"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   104
    by (simp add: ac_simps)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   105
  have "gcd (fib q) (fib (Suc q)) = Suc 0"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   106
    using coprime_fib_Suc_nat [of q] by simp
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   107
  then have *: "gcd (fib n * fib q) (fib n * fib (Suc q)) = fib n"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   108
    by (simp add: gcd_mult_distrib_nat [symmetric])
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   109
  moreover have "gcd (fib (Suc q)) (fib n * fib q + fib (Suc n) * fib (Suc q)) =
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   110
    gcd (fib (Suc q)) (fib n * fib q)"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   111
    using gcd_add_mult [of "fib (Suc q)"] by (simp add: ac_simps)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   112
  moreover have "gcd (fib (Suc q)) (fib n * fib (Suc q)) = fib (Suc q)"
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   113
    by simp
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   114
  ultimately show ?thesis
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   115
    using Suc \<open>coprime (fib (Suc q)) (fib q)\<close>
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   116
    by (auto simp add: fib_add algebra_simps gcd_mult_right_right_cancel)
e7e54a0b9197 dedicated definition for coprimality
haftmann
parents: 65393
diff changeset
   117
qed
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   118
60527
eb431a5651fe tuned proofs;
wenzelm
parents: 60526
diff changeset
   119
lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
54713
6666fc0b9ebc Fib: Who needs the int version?
paulson
parents: 53077
diff changeset
   120
  by (simp add: gcd_fib_add [symmetric, of _ "n-m"])
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   121
60527
eb431a5651fe tuned proofs;
wenzelm
parents: 60526
diff changeset
   122
lemma gcd_fib_mod: "0 < m \<Longrightarrow> gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   123
proof (induct n rule: less_induct)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   124
  case (less n)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   125
  show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   126
  proof (cases "m < n")
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   127
    case True
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   128
    then have "m \<le> n" by auto
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   129
    with \<open>0 < m\<close> have "0 < n" by auto
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   130
    with \<open>0 < m\<close> \<open>m < n\<close> have *: "n - m < n" by auto
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   131
    have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   132
      by (simp add: mod_if [of n]) (use \<open>m < n\<close> in auto)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   133
    also have "\<dots> = gcd (fib m)  (fib (n - m))"
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   134
      by (simp add: less.hyps * \<open>0 < m\<close>)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   135
    also have "\<dots> = gcd (fib m) (fib n)"
60526
fad653acf58f isabelle update_cartouches;
wenzelm
parents: 60141
diff changeset
   136
      by (simp add: gcd_fib_diff \<open>m \<le> n\<close>)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   137
    finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   138
  next
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   139
    case False
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   140
    then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   141
      by (cases "m = n") auto
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   142
  qed
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   143
qed
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   144
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   145
lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"  \<comment> \<open>Law 6.111\<close>
62348
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 61649
diff changeset
   146
  by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd.commute gcd_fib_mod)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   147
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63167
diff changeset
   148
theorem fib_mult_eq_sum_nat: "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
   149
  by (induct n rule: nat.induct) (auto simp add:  field_simps)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   150
60527
eb431a5651fe tuned proofs;
wenzelm
parents: 60526
diff changeset
   151
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   152
subsection \<open>Closed form\<close>
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   153
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   154
lemma fib_closed_form:
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   155
  fixes \<phi> \<psi> :: real
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   156
  defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   157
    and "\<psi> \<equiv> (1 - sqrt 5) / 2"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   158
  shows "of_nat (fib n) = (\<phi> ^ n - \<psi> ^ n) / sqrt 5"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   159
proof (induct n rule: fib.induct)
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   160
  fix n :: nat
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   161
  assume IH1: "of_nat (fib n) = (\<phi> ^ n - \<psi> ^ n) / sqrt 5"
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   162
  assume IH2: "of_nat (fib (Suc n)) = (\<phi> ^ Suc n - \<psi> ^ Suc n) / sqrt 5"
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   163
  have "of_nat (fib (Suc (Suc n))) = of_nat (fib (Suc n)) + of_nat (fib n)" by simp
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   164
  also have "\<dots> = (\<phi>^n * (\<phi> + 1) - \<psi>^n * (\<psi> + 1)) / sqrt 5"
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   165
    by (simp add: IH1 IH2 field_simps)
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   166
  also have "\<phi> + 1 = \<phi>\<^sup>2" by (simp add: \<phi>_def field_simps power2_eq_square)
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   167
  also have "\<psi> + 1 = \<psi>\<^sup>2" by (simp add: \<psi>_def field_simps power2_eq_square)
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   168
  also have "\<phi>^n * \<phi>\<^sup>2 - \<psi>^n * \<psi>\<^sup>2 = \<phi> ^ Suc (Suc n) - \<psi> ^ Suc (Suc n)"
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   169
    by (simp add: power2_eq_square)
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   170
  finally show "of_nat (fib (Suc (Suc n))) = (\<phi> ^ Suc (Suc n) - \<psi> ^ Suc (Suc n)) / sqrt 5" .
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   171
qed (simp_all add: \<phi>_def \<psi>_def field_simps)
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   172
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   173
lemma fib_closed_form':
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   174
  fixes \<phi> \<psi> :: real
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   175
  defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   176
    and "\<psi> \<equiv> (1 - sqrt 5) / 2"
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   177
  assumes "n > 0"
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   178
  shows "fib n = round (\<phi> ^ n / sqrt 5)"
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   179
proof (rule sym, rule round_unique')
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   180
  have "\<bar>\<phi> ^ n / sqrt 5 - of_int (int (fib n))\<bar> = \<bar>\<psi>\<bar> ^ n / sqrt 5"
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   181
    by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] field_simps power_abs)
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   182
  also {
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   183
    from assms have "\<bar>\<psi>\<bar>^n \<le> \<bar>\<psi>\<bar>^1"
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   184
      by (intro power_decreasing) (simp_all add: algebra_simps real_le_lsqrt)
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   185
    also have "\<dots> < sqrt 5 / 2" by (simp add: \<psi>_def field_simps)
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   186
    finally have "\<bar>\<psi>\<bar>^n / sqrt 5 < 1/2" by (simp add: field_simps)
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   187
  }
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   188
  finally show "\<bar>\<phi> ^ n / sqrt 5 - of_int (int (fib n))\<bar> < 1/2" .
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   189
qed
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   190
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   191
lemma fib_asymptotics:
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   192
  fixes \<phi> :: real
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   193
  defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   194
  shows "(\<lambda>n. real (fib n) / (\<phi> ^ n / sqrt 5)) \<longlonglongrightarrow> 1"
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   195
proof -
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   196
  define \<psi> :: real where "\<psi> \<equiv> (1 - sqrt 5) / 2"
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   197
  have "\<phi> > 1" by (simp add: \<phi>_def)
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   198
  then have *: "\<phi> \<noteq> 0" by auto
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   199
  have "(\<lambda>n. (\<psi> / \<phi>) ^ n) \<longlonglongrightarrow> 0"
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   200
    by (rule LIMSEQ_power_zero) (simp_all add: \<phi>_def \<psi>_def field_simps add_pos_pos)
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   201
  then have "(\<lambda>n. 1 - (\<psi> / \<phi>) ^ n) \<longlonglongrightarrow> 1 - 0"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   202
    by (intro tendsto_diff tendsto_const)
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   203
  with * show ?thesis
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   204
    by (simp add: divide_simps fib_closed_form [folded \<phi>_def \<psi>_def])
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   205
qed
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   206
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   207
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   208
subsection \<open>Divide-and-Conquer recurrence\<close>
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   209
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   210
text \<open>
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   211
  The following divide-and-conquer recurrence allows for a more efficient computation
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   212
  of Fibonacci numbers; however, it requires memoisation of values to be reasonably
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   213
  efficient, cutting the number of values to be computed to logarithmically many instead of
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   214
  linearly many. The vast majority of the computation time is then actually spent on the
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   215
  multiplication, since the output number is exponential in the input number.
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   216
\<close>
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   217
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   218
lemma fib_rec_odd:
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   219
  fixes \<phi> \<psi> :: real
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   220
  defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   221
    and "\<psi> \<equiv> (1 - sqrt 5) / 2"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   222
  shows "fib (Suc (2 * n)) = fib n^2 + fib (Suc n)^2"
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   223
proof -
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   224
  have "of_nat (fib n^2 + fib (Suc n)^2) = ((\<phi> ^ n - \<psi> ^ n)\<^sup>2 + (\<phi> * \<phi> ^ n - \<psi> * \<psi> ^ n)\<^sup>2)/5"
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   225
    by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] field_simps power2_eq_square)
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   226
  also
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   227
  let ?A = "\<phi>^(2 * n) + \<psi>^(2 * n) - 2*(\<phi> * \<psi>)^n + \<phi>^(2 * n + 2) + \<psi>^(2 * n + 2) - 2*(\<phi> * \<psi>)^(n + 1)"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   228
  have "(\<phi> ^ n - \<psi> ^ n)\<^sup>2 + (\<phi> * \<phi> ^ n - \<psi> * \<psi> ^ n)\<^sup>2 = ?A"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   229
    by (simp add: power2_eq_square algebra_simps power_mult power_mult_distrib)
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   230
  also have "\<phi> * \<psi> = -1"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   231
    by (simp add: \<phi>_def \<psi>_def field_simps)
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   232
  then have "?A = \<phi>^(2 * n + 1) * (\<phi> + inverse \<phi>) + \<psi>^(2 * n + 1) * (\<psi> + inverse \<psi>)"
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   233
    by (auto simp: field_simps power2_eq_square)
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   234
  also have "1 + sqrt 5 > 0"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   235
    by (auto intro: add_pos_pos)
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   236
  then have "\<phi> + inverse \<phi> = sqrt 5"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   237
    by (simp add: \<phi>_def field_simps)
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   238
  also have "\<psi> + inverse \<psi> = -sqrt 5"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   239
    by (simp add: \<psi>_def field_simps)
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   240
  also have "(\<phi> ^ (2 * n + 1) * sqrt 5 + \<psi> ^ (2 * n + 1) * - sqrt 5) / 5 =
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   241
    (\<phi> ^ (2 * n + 1) - \<psi> ^ (2 * n + 1)) * (sqrt 5 / 5)"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   242
    by (simp add: field_simps)
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   243
  also have "sqrt 5 / 5 = inverse (sqrt 5)"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   244
    by (simp add: field_simps)
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   245
  also have "(\<phi> ^ (2 * n + 1) - \<psi> ^ (2 * n + 1)) * \<dots> = of_nat (fib (Suc (2 * n)))"
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   246
    by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] divide_inverse)
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   247
  finally show ?thesis
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   248
    by (simp only: of_nat_eq_iff)
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   249
qed
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   250
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   251
lemma fib_rec_even: "fib (2 * n) = (fib (n - 1) + fib (n + 1)) * fib n"
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   252
proof (induct n)
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   253
  case 0
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   254
  then show ?case by simp
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   255
next
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   256
  case (Suc n)
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   257
  let ?rfib = "\<lambda>x. real (fib x)"
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   258
  have "2 * (Suc n) = Suc (Suc (2 * n))" by simp
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   259
  also have "real (fib \<dots>) = ?rfib n^2 + ?rfib (Suc n)^2 + (?rfib (n - 1) + ?rfib (n + 1)) * ?rfib n"
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   260
    by (simp add: fib_rec_odd Suc)
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   261
  also have "(?rfib (n - 1) + ?rfib (n + 1)) * ?rfib n = (2 * ?rfib (n + 1) - ?rfib n) * ?rfib n"
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   262
    by (cases n) simp_all
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   263
  also have "?rfib n^2 + ?rfib (Suc n)^2 + \<dots> = (?rfib (Suc n) + 2 * ?rfib n) * ?rfib (Suc n)"
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   264
    by (simp add: algebra_simps power2_eq_square)
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   265
  also have "\<dots> = real ((fib (Suc n - 1) + fib (Suc n + 1)) * fib (Suc n))" by simp
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   266
  finally show ?case by (simp only: of_nat_eq_iff)
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   267
qed
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   268
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   269
lemma fib_rec_even': "fib (2 * n) = (2 * fib (n - 1) + fib n) * fib n"
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   270
  by (subst fib_rec_even, cases n) simp_all
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   271
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   272
lemma fib_rec:
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   273
  "fib n =
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   274
    (if n = 0 then 0 else if n = 1 then 1
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   275
     else if even n then let n' = n div 2; fn = fib n' in (2 * fib (n' - 1) + fn) * fn
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   276
     else let n' = n div 2 in fib n' ^ 2 + fib (Suc n') ^ 2)"
64317
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   277
  by (auto elim: evenE oddE simp: fib_rec_odd fib_rec_even' Let_def)
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   278
029e6247210e More on Fibonacci numbers
eberlm <eberlm@in.tum.de>
parents: 64267
diff changeset
   279
60526
fad653acf58f isabelle update_cartouches;
wenzelm
parents: 60141
diff changeset
   280
subsection \<open>Fibonacci and Binomial Coefficients\<close>
60141
833adf7db7d8 New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   281
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63167
diff changeset
   282
lemma sum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)"
60141
833adf7db7d8 New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   283
  by (induct n) auto
833adf7db7d8 New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   284
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63167
diff changeset
   285
lemma sum_choose_drop_zero:
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   286
  "(\<Sum>k = 0..Suc n. if k = 0 then 0 else (Suc n - k) choose (k - 1)) =
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   287
    (\<Sum>j = 0..n. (n-j) choose j)"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63167
diff changeset
   288
  by (rule trans [OF sum.cong sum_drop_zero]) auto
60141
833adf7db7d8 New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   289
60527
eb431a5651fe tuned proofs;
wenzelm
parents: 60526
diff changeset
   290
lemma ne_diagonal_fib: "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
60141
833adf7db7d8 New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   291
proof (induct n rule: fib.induct)
60527
eb431a5651fe tuned proofs;
wenzelm
parents: 60526
diff changeset
   292
  case 1
eb431a5651fe tuned proofs;
wenzelm
parents: 60526
diff changeset
   293
  show ?case by simp
60141
833adf7db7d8 New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   294
next
60527
eb431a5651fe tuned proofs;
wenzelm
parents: 60526
diff changeset
   295
  case 2
eb431a5651fe tuned proofs;
wenzelm
parents: 60526
diff changeset
   296
  show ?case by simp
60141
833adf7db7d8 New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   297
next
833adf7db7d8 New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   298
  case (3 n)
833adf7db7d8 New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   299
  have "(\<Sum>k = 0..Suc n. Suc (Suc n) - k choose k) =
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   300
     (\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k = 0 then 0 else (Suc n - k choose (k - 1))))"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63167
diff changeset
   301
    by (rule sum.cong) (simp_all add: choose_reduce_nat)
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   302
  also have "\<dots> =
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   303
    (\<Sum>k = 0..Suc n. Suc n - k choose k) +
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   304
    (\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63167
diff changeset
   305
    by (simp add: sum.distrib)
65393
079a6f850c02 misc tuning and modernization;
wenzelm
parents: 64317
diff changeset
   306
  also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) + (\<Sum>j = 0..n. n - j choose j)"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63167
diff changeset
   307
    by (metis sum_choose_drop_zero)
60141
833adf7db7d8 New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   308
  finally show ?case using 3
833adf7db7d8 New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   309
    by simp
833adf7db7d8 New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   310
qed
833adf7db7d8 New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   311
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   312
end