src/HOL/Isar_Examples/Fibonacci.thy
 author haftmann Sat Nov 11 18:41:08 2017 +0000 (19 months ago) changeset 67051 e7e54a0b9197 parent 66453 cc19f7ca2ed6 permissions -rw-r--r--
dedicated definition for coprimality
```     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 section \<open>Fib and Gcd commute\<close>
```
```    16
```
```    17 theory Fibonacci
```
```    18   imports "HOL-Computational_Algebra.Primes"
```
```    19 begin
```
```    20
```
```    21 text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
```
```    22   Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\<close>\<close>
```
```    23
```
```    24 subsection \<open>Fibonacci numbers\<close>
```
```    25
```
```    26 fun fib :: "nat \<Rightarrow> nat"
```
```    27   where
```
```    28     "fib 0 = 0"
```
```    29   | "fib (Suc 0) = 1"
```
```    30   | "fib (Suc (Suc x)) = fib x + fib (Suc x)"
```
```    31
```
```    32 lemma [simp]: "fib (Suc n) > 0"
```
```    33   by (induct n rule: fib.induct) simp_all
```
```    34
```
```    35
```
```    36 text \<open>Alternative induction rule.\<close>
```
```    37
```
```    38 theorem fib_induct: "P 0 \<Longrightarrow> P 1 \<Longrightarrow> (\<And>n. P (n + 1) \<Longrightarrow> P n \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
```
```    39   for n :: nat
```
```    40   by (induct rule: fib.induct) simp_all
```
```    41
```
```    42
```
```    43 subsection \<open>Fib and gcd commute\<close>
```
```    44
```
```    45 text \<open>A few laws taken from @{cite "Concrete-Math"}.\<close>
```
```    46
```
```    47 lemma fib_add: "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
```
```    48   (is "?P n")
```
```    49   \<comment> \<open>see @{cite \<open>page 280\<close> "Concrete-Math"}\<close>
```
```    50 proof (induct n rule: fib_induct)
```
```    51   show "?P 0" by simp
```
```    52   show "?P 1" by simp
```
```    53   fix n
```
```    54   have "fib (n + 2 + k + 1)
```
```    55     = fib (n + k + 1) + fib (n + 1 + k + 1)" by simp
```
```    56   also assume "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n" (is " _ = ?R1")
```
```    57   also assume "fib (n + 1 + k + 1) = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
```
```    58     (is " _ = ?R2")
```
```    59   also have "?R1 + ?R2 = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
```
```    60     by (simp add: add_mult_distrib2)
```
```    61   finally show "?P (n + 2)" .
```
```    62 qed
```
```    63
```
```    64 lemma coprime_fib_Suc: "coprime (fib n) (fib (n + 1))"
```
```    65   (is "?P n")
```
```    66 proof (induct n rule: fib_induct)
```
```    67   show "?P 0" by simp
```
```    68   show "?P 1" by simp
```
```    69   fix n
```
```    70   assume P: "coprime (fib (n + 1)) (fib (n + 1 + 1))"
```
```    71   have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
```
```    72     by simp
```
```    73   also have "\<dots> = fib (n + 2) + fib (n + 1)"
```
```    74     by simp
```
```    75   also have "gcd (fib (n + 2)) \<dots> = gcd (fib (n + 2)) (fib (n + 1))"
```
```    76     by (rule gcd_add2)
```
```    77   also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
```
```    78     by (simp add: gcd.commute)
```
```    79   also have "\<dots> = 1"
```
```    80     using P by simp
```
```    81   finally show "?P (n + 2)"
```
```    82     by (simp add: coprime_iff_gcd_eq_1)
```
```    83 qed
```
```    84
```
```    85 lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n"
```
```    86 proof -
```
```    87   assume "0 < n"
```
```    88   then have "gcd (n * k + m) n = gcd n (m mod n)"
```
```    89     by (simp add: gcd_non_0_nat add.commute)
```
```    90   also from \<open>0 < n\<close> have "\<dots> = gcd m n"
```
```    91     by (simp add: gcd_non_0_nat)
```
```    92   finally show ?thesis .
```
```    93 qed
```
```    94
```
```    95 lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
```
```    96 proof (cases m)
```
```    97   case 0
```
```    98   then show ?thesis by simp
```
```    99 next
```
```   100   case (Suc k)
```
```   101   then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
```
```   102     by (simp add: gcd.commute)
```
```   103   also have "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
```
```   104     by (rule fib_add)
```
```   105   also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
```
```   106     by (simp add: gcd_mult_add)
```
```   107   also have "\<dots> = gcd (fib n) (fib (k + 1))"
```
```   108     using coprime_fib_Suc [of k] gcd_mult_left_right_cancel [of "fib (k + 1)" "fib k" "fib n"]
```
```   109     by (simp add: ac_simps)
```
```   110   also have "\<dots> = gcd (fib m) (fib n)"
```
```   111     using Suc by (simp add: gcd.commute)
```
```   112   finally show ?thesis .
```
```   113 qed
```
```   114
```
```   115 lemma gcd_fib_diff: "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" if "m \<le> n"
```
```   116 proof -
```
```   117   have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
```
```   118     by (simp add: gcd_fib_add)
```
```   119   also from \<open>m \<le> n\<close> have "n - m + m = n"
```
```   120     by simp
```
```   121   finally show ?thesis .
```
```   122 qed
```
```   123
```
```   124 lemma gcd_fib_mod: "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" if "0 < m"
```
```   125 proof (induct n rule: nat_less_induct)
```
```   126   case hyp: (1 n)
```
```   127   show ?case
```
```   128   proof -
```
```   129     have "n mod m = (if n < m then n else (n - m) mod m)"
```
```   130       by (rule mod_if)
```
```   131     also have "gcd (fib m) (fib \<dots>) = gcd (fib m) (fib n)"
```
```   132     proof (cases "n < m")
```
```   133       case True
```
```   134       then show ?thesis by simp
```
```   135     next
```
```   136       case False
```
```   137       then have "m \<le> n" by simp
```
```   138       from \<open>0 < m\<close> and False have "n - m < n"
```
```   139         by simp
```
```   140       with hyp have "gcd (fib m) (fib ((n - m) mod m))
```
```   141           = gcd (fib m) (fib (n - m))" by simp
```
```   142       also have "\<dots> = gcd (fib m) (fib n)"
```
```   143         using \<open>m \<le> n\<close> by (rule gcd_fib_diff)
```
```   144       finally have "gcd (fib m) (fib ((n - m) mod m)) =
```
```   145           gcd (fib m) (fib n)" .
```
```   146       with False show ?thesis by simp
```
```   147     qed
```
```   148     finally show ?thesis .
```
```   149   qed
```
```   150 qed
```
```   151
```
```   152 theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
```
```   153   (is "?P m n")
```
```   154 proof (induct m n rule: gcd_nat_induct)
```
```   155   fix m n :: nat
```
```   156   show "fib (gcd m 0) = gcd (fib m) (fib 0)"
```
```   157     by simp
```
```   158   assume n: "0 < n"
```
```   159   then have "gcd m n = gcd n (m mod n)"
```
```   160     by (simp add: gcd_non_0_nat)
```
```   161   also assume hyp: "fib \<dots> = gcd (fib n) (fib (m mod n))"
```
```   162   also from n have "\<dots> = gcd (fib n) (fib m)"
```
```   163     by (rule gcd_fib_mod)
```
```   164   also have "\<dots> = gcd (fib m) (fib n)"
```
```   165     by (rule gcd.commute)
```
```   166   finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
```
```   167 qed
```
```   168
```
```   169 end
```