src/HOL/NewNumberTheory/Fib.thy
author nipkow
Wed, 24 Jun 2009 17:50:49 +0200
changeset 31792 d5a6096b94ad
parent 31719 29f5b20e8ee8
child 31952 40501bb2d57c
permissions -rw-r--r--
Replaced Suc_remove by Suc_eq_plus1
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     1
(*  Title:      Fib.thy
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     2
    Authors:    Lawrence C. Paulson, Jeremy Avigad
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
     3
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
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    12
header {* Fib *}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    13
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    14
theory Fib
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    15
imports Binomial
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    16
begin
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    17
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    18
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    19
subsection {* Main definitions *}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    20
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    21
class fib =
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    22
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    23
fixes 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    24
  fib :: "'a \<Rightarrow> 'a"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    25
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    26
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    27
(* definition for the natural numbers *)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    28
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    29
instantiation nat :: fib
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    30
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    31
begin 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    32
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    33
fun 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    34
  fib_nat :: "nat \<Rightarrow> nat"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    35
where
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    36
  "fib_nat n =
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    37
   (if n = 0 then 0 else
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    38
   (if n = 1 then 1 else
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    39
     fib (n - 1) + fib (n - 2)))"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    40
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    41
instance proof qed
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    42
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    43
end
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    44
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    45
(* definition for the integers *)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    46
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    47
instantiation int :: fib
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    48
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    49
begin 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    50
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    51
definition
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    52
  fib_int :: "int \<Rightarrow> int"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    53
where  
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    54
  "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    55
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    56
instance proof qed
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    57
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    58
end
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    59
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    60
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    61
subsection {* Set up Transfer *}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    62
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    63
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    64
lemma transfer_nat_int_fib:
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    65
  "(x::int) >= 0 \<Longrightarrow> fib (nat x) = nat (fib x)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    66
  unfolding fib_int_def by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    67
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    68
lemma transfer_nat_int_fib_closure:
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    69
  "n >= (0::int) \<Longrightarrow> fib n >= 0"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    70
  by (auto simp add: fib_int_def)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    71
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    72
declare TransferMorphism_nat_int[transfer add return: 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    73
    transfer_nat_int_fib transfer_nat_int_fib_closure]
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    74
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    75
lemma transfer_int_nat_fib:
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    76
  "fib (int n) = int (fib n)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    77
  unfolding fib_int_def by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    78
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    79
lemma transfer_int_nat_fib_closure:
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    80
  "is_nat n \<Longrightarrow> fib n >= 0"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    81
  unfolding fib_int_def by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    82
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    83
declare TransferMorphism_int_nat[transfer add return: 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    84
    transfer_int_nat_fib transfer_int_nat_fib_closure]
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    85
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    86
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    87
subsection {* Fibonacci numbers *}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    88
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    89
lemma nat_fib_0 [simp]: "fib (0::nat) = 0"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    90
  by simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    91
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    92
lemma int_fib_0 [simp]: "fib (0::int) = 0"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    93
  unfolding fib_int_def by simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    94
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    95
lemma nat_fib_1 [simp]: "fib (1::nat) = 1"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    96
  by simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    97
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    98
lemma nat_fib_Suc_0 [simp]: "fib (Suc 0) = Suc 0"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
    99
  by simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   100
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   101
lemma int_fib_1 [simp]: "fib (1::int) = 1"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   102
  unfolding fib_int_def by simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   103
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   104
lemma nat_fib_reduce: "(n::nat) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   105
  by simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   106
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   107
declare fib_nat.simps [simp del]
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   108
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   109
lemma int_fib_reduce: "(n::int) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   110
  unfolding fib_int_def
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   111
  by (auto simp add: nat_fib_reduce nat_diff_distrib)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   112
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   113
lemma int_fib_neg [simp]: "(n::int) < 0 \<Longrightarrow> fib n = 0"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   114
  unfolding fib_int_def by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   115
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   116
lemma nat_fib_2 [simp]: "fib (2::nat) = 1"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   117
  by (subst nat_fib_reduce, auto)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   118
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   119
lemma int_fib_2 [simp]: "fib (2::int) = 1"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   120
  by (subst int_fib_reduce, auto)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   121
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   122
lemma nat_fib_plus_2: "fib ((n::nat) + 2) = fib (n + 1) + fib n"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   123
  by (subst nat_fib_reduce, auto simp add: One_nat_def)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   124
(* the need for One_nat_def is due to the natdiff_cancel_numerals
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   125
   procedure *)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   126
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   127
lemma nat_fib_induct: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow> 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   128
    (!!n. P n \<Longrightarrow> P (n + 1) \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   129
  apply (atomize, induct n rule: nat_less_induct)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   130
  apply auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   131
  apply (case_tac "n = 0", force)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   132
  apply (case_tac "n = 1", force)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   133
  apply (subgoal_tac "n >= 2")
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   134
  apply (frule_tac x = "n - 1" in spec)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   135
  apply (drule_tac x = "n - 2" in spec)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   136
  apply (drule_tac x = "n - 2" in spec)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   137
  apply auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   138
  apply (auto simp add: One_nat_def) (* again, natdiff_cancel *)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   139
done
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   140
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   141
lemma nat_fib_add: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) + 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   142
    fib k * fib n"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   143
  apply (induct n rule: nat_fib_induct)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   144
  apply auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   145
  apply (subst nat_fib_reduce)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   146
  apply (auto simp add: ring_simps)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   147
  apply (subst (1 3 5) nat_fib_reduce)
31792
d5a6096b94ad Replaced Suc_remove by Suc_eq_plus1
nipkow
parents: 31719
diff changeset
   148
  apply (auto simp add: ring_simps Suc_eq_plus1)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   149
(* hmmm. Why doesn't "n + (1 + (1 + k))" simplify to "n + k + 2"? *)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   150
  apply (subgoal_tac "n + (k + 2) = n + (1 + (1 + k))")
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   151
  apply (erule ssubst) back back
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   152
  apply (erule ssubst) back 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   153
  apply auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   154
done
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   155
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   156
lemma nat_fib_add': "fib (n + Suc k) = fib (Suc k) * fib (Suc n) + 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   157
    fib k * fib n"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   158
  using nat_fib_add by (auto simp add: One_nat_def)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   159
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   160
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   161
(* transfer from nats to ints *)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   162
lemma int_fib_add [rule_format]: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   163
    fib (n + k + 1) = fib (k + 1) * fib (n + 1) + 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   164
    fib k * fib n "
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   165
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   166
  by (rule nat_fib_add [transferred])
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   167
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   168
lemma nat_fib_neq_0: "(n::nat) > 0 \<Longrightarrow> fib n ~= 0"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   169
  apply (induct n rule: nat_fib_induct)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   170
  apply (auto simp add: nat_fib_plus_2)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   171
done
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   172
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   173
lemma nat_fib_gr_0: "(n::nat) > 0 \<Longrightarrow> fib n > 0"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   174
  by (frule nat_fib_neq_0, simp)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   175
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   176
lemma int_fib_gr_0: "(n::int) > 0 \<Longrightarrow> fib n > 0"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   177
  unfolding fib_int_def by (simp add: nat_fib_gr_0)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   178
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   179
text {*
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   180
  \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   181
  much easier using integers, not natural numbers!
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   182
*}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   183
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   184
lemma int_fib_Cassini_aux: "fib (int n + 2) * fib (int n) - 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   185
    (fib (int n + 1))^2 = (-1)^(n + 1)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   186
  apply (induct n)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   187
  apply (auto simp add: ring_simps power2_eq_square int_fib_reduce
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   188
      power_add)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   189
done
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   190
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   191
lemma int_fib_Cassini: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n - 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   192
    (fib (n + 1))^2 = (-1)^(nat n + 1)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   193
  by (insert int_fib_Cassini_aux [of "nat n"], auto)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   194
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   195
(*
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   196
lemma int_fib_Cassini': "n >= 0 \<Longrightarrow> fib (n + 2) * fib n = 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   197
    (fib (n + 1))^2 + (-1)^(nat n + 1)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   198
  by (frule int_fib_Cassini, simp) 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   199
*)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   200
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   201
lemma int_fib_Cassini': "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   202
  (if even n then tsub ((fib (n + 1))^2) 1
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   203
   else (fib (n + 1))^2 + 1)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   204
  apply (frule int_fib_Cassini, auto simp add: pos_int_even_equiv_nat_even)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   205
  apply (subst tsub_eq)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   206
  apply (insert int_fib_gr_0 [of "n + 1"], force)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   207
  apply auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   208
done
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   209
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   210
lemma nat_fib_Cassini: "fib ((n::nat) + 2) * fib n =
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   211
  (if even n then (fib (n + 1))^2 - 1
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   212
   else (fib (n + 1))^2 + 1)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   213
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   214
  by (rule int_fib_Cassini' [transferred, of n], auto)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   215
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   216
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   217
text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   218
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   219
lemma nat_coprime_fib_plus_1: "coprime (fib (n::nat)) (fib (n + 1))"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   220
  apply (induct n rule: nat_fib_induct)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   221
  apply auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   222
  apply (subst (2) nat_fib_reduce)
31792
d5a6096b94ad Replaced Suc_remove by Suc_eq_plus1
nipkow
parents: 31719
diff changeset
   223
  apply (auto simp add: Suc_eq_plus1) (* again, natdiff_cancel *)
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   224
  apply (subst add_commute, auto)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   225
  apply (subst nat_gcd_commute, auto simp add: ring_simps)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   226
done
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   227
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   228
lemma nat_coprime_fib_Suc: "coprime (fib n) (fib (Suc n))"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   229
  using nat_coprime_fib_plus_1 by (simp add: One_nat_def)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   230
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   231
lemma int_coprime_fib_plus_1: 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   232
    "n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   233
  by (erule nat_coprime_fib_plus_1 [transferred])
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   234
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   235
lemma nat_gcd_fib_add: "gcd (fib (m::nat)) (fib (n + m)) = gcd (fib m) (fib n)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   236
  apply (simp add: nat_gcd_commute [of "fib m"])
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   237
  apply (rule nat_cases [of _ m])
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   238
  apply simp
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   239
  apply (subst add_assoc [symmetric])
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   240
  apply (simp add: nat_fib_add)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   241
  apply (subst nat_gcd_commute)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   242
  apply (subst mult_commute)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   243
  apply (subst nat_gcd_add_mult)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   244
  apply (subst nat_gcd_commute)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   245
  apply (rule nat_gcd_mult_cancel)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   246
  apply (rule nat_coprime_fib_plus_1)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   247
done
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   248
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   249
lemma int_gcd_fib_add [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow> 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   250
    gcd (fib (m::int)) (fib (n + m)) = gcd (fib m) (fib n)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   251
  by (erule nat_gcd_fib_add [transferred])
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   252
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   253
lemma nat_gcd_fib_diff: "(m::nat) \<le> n \<Longrightarrow> 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   254
    gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   255
  by (simp add: nat_gcd_fib_add [symmetric, of _ "n-m"])
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   256
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   257
lemma int_gcd_fib_diff: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow> 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   258
    gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   259
  by (simp add: int_gcd_fib_add [symmetric, of _ "n-m"])
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   260
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   261
lemma nat_gcd_fib_mod: "0 < (m::nat) \<Longrightarrow> 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   262
    gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   263
proof (induct n rule: less_induct)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   264
  case (less n)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   265
  from less.prems have pos_m: "0 < m" .
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   266
  show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   267
  proof (cases "m < n")
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   268
    case True note m_n = True
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   269
    then have m_n': "m \<le> n" by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   270
    with pos_m have pos_n: "0 < n" by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   271
    with pos_m m_n have diff: "n - m < n" by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   272
    have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   273
    by (simp add: mod_if [of n]) (insert m_n, auto)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   274
    also have "\<dots> = gcd (fib m)  (fib (n - m))" 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   275
      by (simp add: less.hyps diff pos_m)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   276
    also have "\<dots> = gcd (fib m) (fib n)" by (simp add: nat_gcd_fib_diff m_n')
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   277
    finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   278
  next
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   279
    case False then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   280
    by (cases "m = n") auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   281
  qed
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   282
qed
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   283
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   284
lemma int_gcd_fib_mod: 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   285
  assumes "0 < (m::int)" and "0 <= n"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   286
  shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   287
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   288
  apply (rule nat_gcd_fib_mod [transferred])
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   289
  using prems apply auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   290
done
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   291
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   292
lemma nat_fib_gcd: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"  
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   293
    -- {* Law 6.111 *}
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   294
  apply (induct m n rule: nat_gcd_induct)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   295
  apply (simp_all add: nat_gcd_non_0 nat_gcd_commute nat_gcd_fib_mod)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   296
done
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   297
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   298
lemma int_fib_gcd: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   299
    fib (gcd (m::int) n) = gcd (fib m) (fib n)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   300
  by (erule nat_fib_gcd [transferred])
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   301
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   302
lemma nat_atMost_plus_one: "{..(k::nat) + 1} = insert (k + 1) {..k}" 
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   303
  by auto
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   304
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   305
theorem nat_fib_mult_eq_setsum:
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   306
    "fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   307
  apply (induct n)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   308
  apply (auto simp add: nat_atMost_plus_one nat_fib_plus_2 ring_simps)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   309
done
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   310
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   311
theorem nat_fib_mult_eq_setsum':
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   312
    "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   313
  using nat_fib_mult_eq_setsum by (simp add: One_nat_def)
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   314
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   315
theorem int_fib_mult_eq_setsum [rule_format]:
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   316
    "n >= 0 \<Longrightarrow> fib ((n::int) + 1) * fib n = (\<Sum>k \<in> {0..n}. fib k * fib k)"
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   317
  by (erule nat_fib_mult_eq_setsum [transferred])
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   318
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents:
diff changeset
   319
end