src/HOL/NumberTheory/Fib.thy
author chaieb
Fri, 11 Nov 2005 10:50:43 +0100
changeset 18156 5a971b272f78
parent 16417 9bc16273c2d4
child 20272 0ca998e83447
permissions -rw-r--r--
a proof step corrected due to the changement in the presburger method.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
     1
(*  ID:         $Id$
9944
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     3
    Copyright   1997  University of Cambridge
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     4
*)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     5
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
     6
header {* The Fibonacci function *}
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 15628
diff changeset
     8
theory Fib imports Primes begin
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
     9
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    10
text {*
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    11
  Fibonacci numbers: proofs of laws taken from:
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    12
  R. L. Graham, D. E. Knuth, O. Patashnik.  Concrete Mathematics.
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    13
  (Addison-Wesley, 1989)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    14
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    15
  \bigskip
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    16
*}
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    17
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    18
consts fib :: "nat => nat"
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    19
recdef fib  "measure (\<lambda>x. x)"
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    20
   zero:    "fib 0  = 0"
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    21
   one:     "fib (Suc 0) = Suc 0"
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    22
   Suc_Suc: "fib (Suc (Suc x)) = fib x + fib (Suc x)"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    23
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    24
text {*
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    25
  \medskip The difficulty in these proofs is to ensure that the
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    26
  induction hypotheses are applied before the definition of @{term
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    27
  fib}.  Towards this end, the @{term fib} equations are not declared
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    28
  to the Simplifier and are applied very selectively at first.
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    29
*}
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    30
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    31
text{*We disable @{text fib.Suc_Suc} for simplification ...*}
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    32
declare fib.Suc_Suc [simp del]
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    33
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    34
text{*...then prove a version that has a more restrictive pattern.*}
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    35
lemma fib_Suc3: "fib (Suc (Suc (Suc n))) = fib (Suc n) + fib (Suc (Suc n))"
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    36
  by (rule fib.Suc_Suc)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    37
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    38
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    39
text {* \medskip Concrete Mathematics, page 280 *}
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    40
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    41
lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    42
  apply (induct n rule: fib.induct)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    43
    prefer 3
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    44
    txt {* simplify the LHS just enough to apply the induction hypotheses *}
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    45
    apply (simp add: fib_Suc3)
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    46
    apply (simp_all add: fib.Suc_Suc add_mult_distrib2)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    47
    done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    48
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    49
lemma fib_Suc_neq_0: "fib (Suc n) \<noteq> 0"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    50
  apply (induct n rule: fib.induct)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    51
    apply (simp_all add: fib.Suc_Suc)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    52
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    53
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    54
lemma fib_Suc_gr_0: "0 < fib (Suc n)"
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    55
  by (insert fib_Suc_neq_0 [of n], simp)  
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    56
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    57
lemma fib_gr_0: "0 < n ==> 0 < fib n"
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    58
  by (case_tac n, auto simp add: fib_Suc_gr_0) 
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    59
9944
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    60
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    61
text {*
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    62
  \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    63
  much easier using integers, not natural numbers!
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    64
*}
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    65
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    66
lemma fib_Cassini_int:
15003
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 11868
diff changeset
    67
 "int (fib (Suc (Suc n)) * fib n) =
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11786
diff changeset
    68
  (if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - 1
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11786
diff changeset
    69
   else int (fib (Suc n) * fib (Suc n)) + 1)"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    70
  apply (induct n rule: fib.induct)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    71
    apply (simp add: fib.Suc_Suc)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    72
   apply (simp add: fib.Suc_Suc mod_Suc)
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    73
  apply (simp add: fib.Suc_Suc add_mult_distrib add_mult_distrib2
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    74
                   mod_Suc zmult_int [symmetric])
18156
5a971b272f78 a proof step corrected due to the changement in the presburger method.
chaieb
parents: 16417
diff changeset
    75
  apply (presburger (no_abs))
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    76
  done
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    77
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    78
text{*We now obtain a version for the natural numbers via the coercion 
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    79
   function @{term int}.*}
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    80
theorem fib_Cassini:
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    81
 "fib (Suc (Suc n)) * fib n =
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    82
  (if n mod 2 = 0 then fib (Suc n) * fib (Suc n) - 1
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    83
   else fib (Suc n) * fib (Suc n) + 1)"
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    84
  apply (rule int_int_eq [THEN iffD1]) 
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    85
  apply (simp add: fib_Cassini_int) 
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    86
  apply (subst zdiff_int [symmetric]) 
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    87
   apply (insert fib_Suc_gr_0 [of n], simp_all)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    88
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    89
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    90
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
    91
text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    92
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11468
diff changeset
    93
lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = Suc 0"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    94
  apply (induct n rule: fib.induct)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    95
    prefer 3
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    96
    apply (simp add: gcd_commute fib_Suc3)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    97
   apply (simp_all add: fib.Suc_Suc)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    98
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
    99
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   100
lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
   101
  apply (simp add: gcd_commute [of "fib m"])
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
   102
  apply (case_tac m)
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
   103
   apply simp 
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   104
  apply (simp add: fib_add)
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
   105
  apply (simp add: add_commute gcd_non_0 [OF fib_Suc_gr_0])
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
   106
  apply (simp add: gcd_non_0 [OF fib_Suc_gr_0, symmetric])
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   107
  apply (simp add: gcd_fib_Suc_eq_1 gcd_mult_cancel)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   108
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   109
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   110
lemma gcd_fib_diff: "m \<le> n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
   111
  by (simp add: gcd_fib_add [symmetric, of _ "n-m"]) 
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   112
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   113
lemma gcd_fib_mod: "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   114
  apply (induct n rule: nat_less_induct)
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
   115
  apply (simp add: mod_if gcd_fib_diff mod_geq)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   116
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   117
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   118
lemma fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)"  -- {* Law 6.111 *}
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   119
  apply (induct m n rule: gcd_induct)
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
   120
  apply (simp_all add: gcd_non_0 gcd_commute gcd_fib_mod)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   121
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   122
15628
9f912f8fd2df tidied up
paulson
parents: 15439
diff changeset
   123
theorem fib_mult_eq_setsum:
11786
51ce34ef5113 setsum syntax;
wenzelm
parents: 11704
diff changeset
   124
    "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   125
  apply (induct n rule: fib.induct)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   126
    apply (auto simp add: atMost_Suc fib.Suc_Suc)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   127
  apply (simp add: add_mult_distrib add_mult_distrib2)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10147
diff changeset
   128
  done
9944
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   129
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   130
end