src/HOL/Number_Theory/Fib.thy
author wenzelm
Sat, 10 Sep 2011 23:27:32 +0200
changeset 44872 a98ef45122f3
parent 41959 b460124855b8
child 53077 a1b3784f8129
permissions -rw-r--r--
misc tuning;
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
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    20
class fib =
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    21
  fixes fib :: "'a \<Rightarrow> 'a"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    22
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    23
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    24
(* definition for the natural numbers *)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    25
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    26
instantiation nat :: fib
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    27
begin
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    28
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    29
fun fib_nat :: "nat \<Rightarrow> nat"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    30
where
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    31
  "fib_nat n =
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    32
   (if n = 0 then 0 else
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    33
   (if n = 1 then 1 else
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    34
     fib (n - 1) + fib (n - 2)))"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    35
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    36
instance ..
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    37
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    38
end
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    39
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    40
(* definition for the integers *)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    41
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    42
instantiation int :: fib
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    43
begin
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    44
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    45
definition fib_int :: "int \<Rightarrow> int"
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    46
  where "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    47
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    48
instance ..
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    49
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    50
end
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    51
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    52
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    53
subsection {* Set up Transfer *}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    54
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    55
lemma transfer_nat_int_fib:
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    56
  "(x::int) >= 0 \<Longrightarrow> fib (nat x) = nat (fib x)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    57
  unfolding fib_int_def by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    58
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    59
lemma transfer_nat_int_fib_closure:
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    60
  "n >= (0::int) \<Longrightarrow> fib n >= 0"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    61
  by (auto simp add: fib_int_def)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    62
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    63
declare transfer_morphism_nat_int[transfer add return:
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    64
    transfer_nat_int_fib transfer_nat_int_fib_closure]
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    65
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    66
lemma transfer_int_nat_fib: "fib (int n) = int (fib n)"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    67
  unfolding fib_int_def by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    68
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    69
lemma transfer_int_nat_fib_closure: "is_nat n \<Longrightarrow> fib n >= 0"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    70
  unfolding fib_int_def by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    71
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
    72
declare transfer_morphism_int_nat[transfer add return:
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    73
    transfer_int_nat_fib transfer_int_nat_fib_closure]
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    74
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    75
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    76
subsection {* Fibonacci numbers *}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    77
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
    78
lemma fib_0_nat [simp]: "fib (0::nat) = 0"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    79
  by simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    80
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
    81
lemma fib_0_int [simp]: "fib (0::int) = 0"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    82
  unfolding fib_int_def by simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    83
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
    84
lemma fib_1_nat [simp]: "fib (1::nat) = 1"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    85
  by simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    86
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
    87
lemma fib_Suc_0_nat [simp]: "fib (Suc 0) = Suc 0"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    88
  by simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    89
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
    90
lemma fib_1_int [simp]: "fib (1::int) = 1"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    91
  unfolding fib_int_def by simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    92
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
    93
lemma fib_reduce_nat: "(n::nat) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    94
  by simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    95
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    96
declare fib_nat.simps [simp del]
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    97
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
    98
lemma fib_reduce_int: "(n::int) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    99
  unfolding fib_int_def
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   100
  by (auto simp add: fib_reduce_nat nat_diff_distrib)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   101
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   102
lemma fib_neg_int [simp]: "(n::int) < 0 \<Longrightarrow> fib n = 0"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   103
  unfolding fib_int_def by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   104
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   105
lemma fib_2_nat [simp]: "fib (2::nat) = 1"
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   106
  by (subst fib_reduce_nat, auto)
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
lemma fib_2_int [simp]: "fib (2::int) = 1"
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   109
  by (subst fib_reduce_int, auto)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   110
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   111
lemma fib_plus_2_nat: "fib ((n::nat) + 2) = fib (n + 1) + fib n"
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   112
  by (subst fib_reduce_nat, auto simp add: One_nat_def)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   113
(* the need for One_nat_def is due to the natdiff_cancel_numerals
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   114
   procedure *)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   115
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   116
lemma fib_induct_nat: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow>
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   117
    (!!n. P n \<Longrightarrow> P (n + 1) \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   118
  apply (atomize, induct n rule: nat_less_induct)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   119
  apply auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   120
  apply (case_tac "n = 0", force)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   121
  apply (case_tac "n = 1", force)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   122
  apply (subgoal_tac "n >= 2")
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   123
  apply (frule_tac x = "n - 1" in spec)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   124
  apply (drule_tac x = "n - 2" in spec)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   125
  apply (drule_tac x = "n - 2" in spec)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   126
  apply auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   127
  apply (auto simp add: One_nat_def) (* again, natdiff_cancel *)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   128
done
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   129
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   130
lemma fib_add_nat: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) +
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   131
    fib k * fib n"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   132
  apply (induct n rule: fib_induct_nat)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   133
  apply auto
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   134
  apply (subst fib_reduce_nat)
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 35644
diff changeset
   135
  apply (auto simp add: field_simps)
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   136
  apply (subst (1 3 5) fib_reduce_nat)
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 35644
diff changeset
   137
  apply (auto simp add: field_simps Suc_eq_plus1)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   138
(* hmmm. Why doesn't "n + (1 + (1 + k))" simplify to "n + k + 2"? *)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   139
  apply (subgoal_tac "n + (k + 2) = n + (1 + (1 + k))")
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   140
  apply (erule ssubst) back back
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   141
  apply (erule ssubst) back
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   142
  apply auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   143
done
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   144
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   145
lemma fib_add'_nat: "fib (n + Suc k) =
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   146
    fib (Suc k) * fib (Suc n) + fib k * fib n"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   147
  using fib_add_nat by (auto simp add: One_nat_def)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   148
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   149
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   150
(* transfer from nats to ints *)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   151
lemma fib_add_int: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   152
    fib (n + k + 1) = fib (k + 1) * fib (n + 1) +  fib k * fib n "
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   153
  by (rule fib_add_nat [transferred])
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   154
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   155
lemma fib_neq_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n ~= 0"
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   156
  apply (induct n rule: fib_induct_nat)
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   157
  apply (auto simp add: fib_plus_2_nat)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   158
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   159
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   160
lemma fib_gr_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n > 0"
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   161
  by (frule fib_neq_0_nat, simp)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   162
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   163
lemma fib_gr_0_int: "(n::int) > 0 \<Longrightarrow> fib n > 0"
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   164
  unfolding fib_int_def by (simp add: fib_gr_0_nat)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   165
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   166
text {*
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   167
  \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   168
  much easier using integers, not natural numbers!
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   169
*}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   170
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   171
lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   172
    (fib (int n + 1))^2 = (-1)^(n + 1)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   173
  apply (induct n)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   174
  apply (auto simp add: field_simps power2_eq_square fib_reduce_int power_add)
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   175
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   176
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   177
lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   178
    (fib (n + 1))^2 = (-1)^(nat n + 1)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   179
  by (insert fib_Cassini_aux_int [of "nat n"], auto)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   180
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   181
(*
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   182
lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   183
    (fib (n + 1))^2 + (-1)^(nat n + 1)"
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   184
  by (frule fib_Cassini_int, simp)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   185
*)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   186
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   187
lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   188
  (if even n then tsub ((fib (n + 1))^2) 1
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   189
   else (fib (n + 1))^2 + 1)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   190
  apply (frule fib_Cassini_int, auto simp add: pos_int_even_equiv_nat_even)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   191
  apply (subst tsub_eq)
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   192
  apply (insert fib_gr_0_int [of "n + 1"], force)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   193
  apply auto
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   194
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   195
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   196
lemma fib_Cassini_nat: "fib ((n::nat) + 2) * fib n =
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   197
    (if even n then (fib (n + 1))^2 - 1
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   198
     else (fib (n + 1))^2 + 1)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   199
  by (rule fib_Cassini'_int [transferred, of n], auto)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   200
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   201
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   202
text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   203
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   204
lemma coprime_fib_plus_1_nat: "coprime (fib (n::nat)) (fib (n + 1))"
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   205
  apply (induct n rule: fib_induct_nat)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   206
  apply auto
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   207
  apply (subst (2) fib_reduce_nat)
31792
d5a6096b94ad Replaced Suc_remove by Suc_eq_plus1
nipkow
parents: 31719
diff changeset
   208
  apply (auto simp add: Suc_eq_plus1) (* again, natdiff_cancel *)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   209
  apply (subst add_commute, auto)
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 35644
diff changeset
   210
  apply (subst gcd_commute_nat, auto simp add: field_simps)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   211
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   212
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   213
lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   214
  using coprime_fib_plus_1_nat by (simp add: One_nat_def)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   215
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   216
lemma coprime_fib_plus_1_int: "n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   217
  by (erule coprime_fib_plus_1_nat [transferred])
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   218
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   219
lemma gcd_fib_add_nat: "gcd (fib (m::nat)) (fib (n + m)) = gcd (fib m) (fib n)"
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   220
  apply (simp add: gcd_commute_nat [of "fib m"])
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   221
  apply (rule cases_nat [of _ m])
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   222
  apply simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   223
  apply (subst add_assoc [symmetric])
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   224
  apply (simp add: fib_add_nat)
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   225
  apply (subst gcd_commute_nat)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   226
  apply (subst mult_commute)
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   227
  apply (subst gcd_add_mult_nat)
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   228
  apply (subst gcd_commute_nat)
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   229
  apply (rule gcd_mult_cancel_nat)
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   230
  apply (rule coprime_fib_plus_1_nat)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   231
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   232
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   233
lemma gcd_fib_add_int [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   234
    gcd (fib (m::int)) (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
   235
  by (erule gcd_fib_add_nat [transferred])
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   236
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   237
lemma gcd_fib_diff_nat: "(m::nat) \<le> n \<Longrightarrow>
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   238
    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
   239
  by (simp add: gcd_fib_add_nat [symmetric, of _ "n-m"])
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   240
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   241
lemma gcd_fib_diff_int: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow>
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   242
    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
   243
  by (simp add: gcd_fib_add_int [symmetric, of _ "n-m"])
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   244
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   245
lemma gcd_fib_mod_nat: "0 < (m::nat) \<Longrightarrow>
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   246
    gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   247
proof (induct n rule: less_induct)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   248
  case (less n)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   249
  from less.prems have pos_m: "0 < m" .
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   250
  show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   251
  proof (cases "m < n")
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   252
    case True
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   253
    then have "m \<le> n" by auto
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   254
    with pos_m have pos_n: "0 < n" by auto
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   255
    with pos_m `m < n` have diff: "n - m < n" by auto
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   256
    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
   257
      by (simp add: mod_if [of n]) (insert `m < n`, auto)
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   258
    also have "\<dots> = gcd (fib m)  (fib (n - m))"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   259
      by (simp add: less.hyps diff pos_m)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   260
    also have "\<dots> = gcd (fib m) (fib n)"
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   261
      by (simp add: gcd_fib_diff_nat `m \<le> n`)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   262
    finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   263
  next
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   264
    case False
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   265
    then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   266
      by (cases "m = n") auto
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   267
  qed
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   268
qed
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   269
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   270
lemma gcd_fib_mod_int:
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   271
  assumes "0 < (m::int)" and "0 <= n"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   272
  shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   273
  apply (rule gcd_fib_mod_nat [transferred])
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 36350
diff changeset
   274
  using assms apply auto
1fa4725c4656 eliminated global prems;
wenzelm
parents: 36350
diff changeset
   275
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   276
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   277
lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   278
    -- {* Law 6.111 *}
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   279
  apply (induct m n rule: gcd_nat_induct)
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   280
  apply (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod_nat)
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 36350
diff changeset
   281
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   282
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   283
lemma fib_gcd_int: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   284
    fib (gcd (m::int) n) = gcd (fib m) (fib n)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   285
  by (erule fib_gcd_nat [transferred])
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   286
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 41959
diff changeset
   287
lemma atMost_plus_one_nat: "{..(k::nat) + 1} = insert (k + 1) {..k}"
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   288
  by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   289
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   290
theorem fib_mult_eq_setsum_nat:
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   291
    "fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   292
  apply (induct n)
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 35644
diff changeset
   293
  apply (auto simp add: atMost_plus_one_nat fib_plus_2_nat field_simps)
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 36350
diff changeset
   294
  done
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   295
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   296
theorem fib_mult_eq_setsum'_nat:
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   297
    "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   298
  using fib_mult_eq_setsum_nat by (simp add: One_nat_def)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   299
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   300
theorem fib_mult_eq_setsum_int [rule_format]:
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   301
    "n >= 0 \<Longrightarrow> fib ((n::int) + 1) * fib n = (\<Sum>k \<in> {0..n}. fib k * fib k)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31792
diff changeset
   302
  by (erule fib_mult_eq_setsum_nat [transferred])
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   303
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   304
end