equal
deleted
inserted
replaced
61 apply auto |
61 apply auto |
62 apply (metis gcd_add1_nat add.commute) |
62 apply (metis gcd_add1_nat add.commute) |
63 done |
63 done |
64 |
64 |
65 lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)" |
65 lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)" |
66 apply (simp add: gcd_commute_nat [of "fib m"]) |
66 apply (simp add: gcd.commute [of "fib m"]) |
67 apply (cases m) |
67 apply (cases m) |
68 apply (auto simp add: fib_add) |
68 apply (auto simp add: fib_add) |
69 apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat |
69 apply (metis gcd.commute mult.commute coprime_fib_Suc_nat |
70 gcd_add_mult_nat gcd_mult_cancel_nat gcd.commute) |
70 gcd_add_mult_nat gcd_mult_cancel gcd.commute) |
71 done |
71 done |
72 |
72 |
73 lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" |
73 lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" |
74 by (simp add: gcd_fib_add [symmetric, of _ "n-m"]) |
74 by (simp add: gcd_fib_add [symmetric, of _ "n-m"]) |
75 |
75 |
96 qed |
96 qed |
97 qed |
97 qed |
98 |
98 |
99 lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" |
99 lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" |
100 -- \<open>Law 6.111\<close> |
100 -- \<open>Law 6.111\<close> |
101 by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod) |
101 by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd.commute gcd_fib_mod) |
102 |
102 |
103 theorem fib_mult_eq_setsum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)" |
103 theorem fib_mult_eq_setsum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)" |
104 by (induct n rule: nat.induct) (auto simp add: field_simps) |
104 by (induct n rule: nat.induct) (auto simp add: field_simps) |
105 |
105 |
106 |
106 |