src/HOL/Isar_Examples/Fibonacci.thy
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 57512 cc97b347b301
child 58614 7338eb25226c
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     1 (*  Title:      HOL/Isar_Examples/Fibonacci.thy
     2     Author:     Gertrud Bauer
     3     Copyright   1999 Technische Universitaet Muenchen
     4 
     5 The Fibonacci function.  Original
     6 tactic script by Lawrence C Paulson.
     7 
     8 Fibonacci numbers: proofs of laws taken from
     9 
    10   R. L. Graham, D. E. Knuth, O. Patashnik.
    11   Concrete Mathematics.
    12   (Addison-Wesley, 1989)
    13 *)
    14 
    15 header {* Fib and Gcd commute *}
    16 
    17 theory Fibonacci
    18 imports "../Number_Theory/Primes"
    19 begin
    20 
    21 text_raw {* \footnote{Isar version by Gertrud Bauer.  Original tactic
    22   script by Larry Paulson.  A few proofs of laws taken from
    23   \cite{Concrete-Math}.} *}
    24 
    25 
    26 declare One_nat_def [simp]
    27 
    28 
    29 subsection {* Fibonacci numbers *}
    30 
    31 fun fib :: "nat \<Rightarrow> nat" where
    32   "fib 0 = 0"
    33 | "fib (Suc 0) = 1"
    34 | "fib (Suc (Suc x)) = fib x + fib (Suc x)"
    35 
    36 lemma [simp]: "fib (Suc n) > 0"
    37   by (induct n rule: fib.induct) simp_all
    38 
    39 
    40 text {* Alternative induction rule. *}
    41 
    42 theorem fib_induct:
    43   fixes n :: nat
    44   shows "P 0 \<Longrightarrow> P 1 \<Longrightarrow> (\<And>n. P (n + 1) \<Longrightarrow> P n \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
    45   by (induct rule: fib.induct) simp_all
    46 
    47 
    48 subsection {* Fib and gcd commute *}
    49 
    50 text {* A few laws taken from \cite{Concrete-Math}. *}
    51 
    52 lemma fib_add:
    53   "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
    54   (is "?P n")
    55   -- {* see \cite[page 280]{Concrete-Math} *}
    56 proof (induct n rule: fib_induct)
    57   show "?P 0" by simp
    58   show "?P 1" by simp
    59   fix n
    60   have "fib (n + 2 + k + 1)
    61     = fib (n + k + 1) + fib (n + 1 + k + 1)" by simp
    62   also assume "fib (n + k + 1)
    63     = fib (k + 1) * fib (n + 1) + fib k * fib n"
    64       (is " _ = ?R1")
    65   also assume "fib (n + 1 + k + 1)
    66     = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
    67       (is " _ = ?R2")
    68   also have "?R1 + ?R2
    69     = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
    70     by (simp add: add_mult_distrib2)
    71   finally show "?P (n + 2)" .
    72 qed
    73 
    74 lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1" (is "?P n")
    75 proof (induct n rule: fib_induct)
    76   show "?P 0" by simp
    77   show "?P 1" by simp
    78   fix n
    79   have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
    80     by simp
    81   also have "\<dots> = fib (n + 2) + fib (n + 1)"
    82     by simp
    83   also have "gcd (fib (n + 2)) \<dots> = gcd (fib (n + 2)) (fib (n + 1))"
    84     by (rule gcd_add2_nat)
    85   also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
    86     by (simp add: gcd_commute_nat)
    87   also assume "\<dots> = 1"
    88   finally show "?P (n + 2)" .
    89 qed
    90 
    91 lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n"
    92 proof -
    93   assume "0 < n"
    94   then have "gcd (n * k + m) n = gcd n (m mod n)"
    95     by (simp add: gcd_non_0_nat add.commute)
    96   also from `0 < n` have "\<dots> = gcd m n"
    97     by (simp add: gcd_non_0_nat)
    98   finally show ?thesis .
    99 qed
   100 
   101 lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
   102 proof (cases m)
   103   case 0
   104   then show ?thesis by simp
   105 next
   106   case (Suc k)
   107   then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
   108     by (simp add: gcd_commute_nat)
   109   also have "fib (n + k + 1)
   110       = fib (k + 1) * fib (n + 1) + fib k * fib n"
   111     by (rule fib_add)
   112   also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
   113     by (simp add: gcd_mult_add)
   114   also have "\<dots> = gcd (fib n) (fib (k + 1))"
   115     by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel_nat)
   116   also have "\<dots> = gcd (fib m) (fib n)"
   117     using Suc by (simp add: gcd_commute_nat)
   118   finally show ?thesis .
   119 qed
   120 
   121 lemma gcd_fib_diff:
   122   assumes "m \<le> n"
   123   shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
   124 proof -
   125   have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
   126     by (simp add: gcd_fib_add)
   127   also from `m \<le> n` have "n - m + m = n"
   128     by simp
   129   finally show ?thesis .
   130 qed
   131 
   132 lemma gcd_fib_mod:
   133   assumes "0 < m"
   134   shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   135 proof (induct n rule: nat_less_induct)
   136   case (1 n) note hyp = this
   137   show ?case
   138   proof -
   139     have "n mod m = (if n < m then n else (n - m) mod m)"
   140       by (rule mod_if)
   141     also have "gcd (fib m) (fib \<dots>) = gcd (fib m) (fib n)"
   142     proof (cases "n < m")
   143       case True
   144       then show ?thesis by simp
   145     next
   146       case False
   147       then have "m \<le> n" by simp
   148       from `0 < m` and False have "n - m < n"
   149         by simp
   150       with hyp have "gcd (fib m) (fib ((n - m) mod m))
   151           = gcd (fib m) (fib (n - m))" by simp
   152       also have "\<dots> = gcd (fib m) (fib n)"
   153         using `m \<le> n` by (rule gcd_fib_diff)
   154       finally have "gcd (fib m) (fib ((n - m) mod m)) =
   155           gcd (fib m) (fib n)" .
   156       with False show ?thesis by simp
   157     qed
   158     finally show ?thesis .
   159   qed
   160 qed
   161 
   162 theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n")
   163 proof (induct m n rule: gcd_nat_induct)
   164   fix m
   165   show "fib (gcd m 0) = gcd (fib m) (fib 0)"
   166     by simp
   167   fix n :: nat
   168   assume n: "0 < n"
   169   then have "gcd m n = gcd n (m mod n)"
   170     by (simp add: gcd_non_0_nat)
   171   also assume hyp: "fib \<dots> = gcd (fib n) (fib (m mod n))"
   172   also from n have "\<dots> = gcd (fib n) (fib m)"
   173     by (rule gcd_fib_mod)
   174   also have "\<dots> = gcd (fib m) (fib n)"
   175     by (rule gcd_commute_nat)
   176   finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
   177 qed
   178 
   179 end