--- a/src/HOL/Isar_examples/Fibonacci.thy Fri Jul 11 23:17:25 2008 +0200
+++ b/src/HOL/Isar_examples/Fibonacci.thy Mon Jul 14 11:04:42 2008 +0200
@@ -70,55 +70,55 @@
finally show "?P (n + 2)" .
qed
-lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n")
+lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1" (is "?P n")
proof (induct n rule: fib_induct)
show "?P 0" by simp
show "?P 1" by simp
fix n
have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
by simp
- also have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))"
+ also have "gcd (fib (n + 2)) ... = gcd (fib (n + 2)) (fib (n + 1))"
by (simp only: gcd_add2')
- also have "... = gcd (fib (n + 1), fib (n + 1 + 1))"
+ also have "... = gcd (fib (n + 1)) (fib (n + 1 + 1))"
by (simp add: gcd_commute)
also assume "... = 1"
finally show "?P (n + 2)" .
qed
-lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)"
+lemma gcd_mult_add: "0 < n ==> gcd (n * k + m) n = gcd m n"
proof -
assume "0 < n"
- then have "gcd (n * k + m, n) = gcd (n, m mod n)"
+ then have "gcd (n * k + m) n = gcd n (m mod n)"
by (simp add: gcd_non_0 add_commute)
- also from `0 < n` have "... = gcd (m, n)" by (simp add: gcd_non_0)
+ also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0)
finally show ?thesis .
qed
-lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"
+lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
proof (cases m)
case 0
then show ?thesis by simp
next
case (Suc k)
- then have "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))"
+ then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
by (simp add: gcd_commute)
also have "fib (n + k + 1)
= fib (k + 1) * fib (n + 1) + fib k * fib n"
by (rule fib_add)
- also have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))"
+ also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
by (simp add: gcd_mult_add)
- also have "... = gcd (fib n, fib (k + 1))"
+ also have "... = gcd (fib n) (fib (k + 1))"
by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
- also have "... = gcd (fib m, fib n)"
+ also have "... = gcd (fib m) (fib n)"
using Suc by (simp add: gcd_commute)
finally show ?thesis .
qed
lemma gcd_fib_diff:
assumes "m <= n"
- shows "gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"
+ shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
proof -
- have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))"
+ have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
by (simp add: gcd_fib_add)
also from `m <= n` have "n - m + m = n" by simp
finally show ?thesis .
@@ -126,25 +126,25 @@
lemma gcd_fib_mod:
assumes "0 < m"
- shows "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
+ shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
proof (induct n rule: nat_less_induct)
case (1 n) note hyp = this
show ?case
proof -
have "n mod m = (if n < m then n else (n - m) mod m)"
by (rule mod_if)
- also have "gcd (fib m, fib ...) = gcd (fib m, fib n)"
+ also have "gcd (fib m) (fib ...) = gcd (fib m) (fib n)"
proof (cases "n < m")
case True then show ?thesis by simp
next
case False then have "m <= n" by simp
from `0 < m` and False have "n - m < n" by simp
- with hyp have "gcd (fib m, fib ((n - m) mod m))
- = gcd (fib m, fib (n - m))" by simp
- also have "... = gcd (fib m, fib n)"
+ with hyp have "gcd (fib m) (fib ((n - m) mod m))
+ = gcd (fib m) (fib (n - m))" by simp
+ also have "... = gcd (fib m) (fib n)"
using `m <= n` by (rule gcd_fib_diff)
- finally have "gcd (fib m, fib ((n - m) mod m)) =
- gcd (fib m, fib n)" .
+ finally have "gcd (fib m) (fib ((n - m) mod m)) =
+ gcd (fib m) (fib n)" .
with False show ?thesis by simp
qed
finally show ?thesis .
@@ -152,15 +152,15 @@
qed
-theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n")
+theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n")
proof (induct m n rule: gcd_induct)
- fix m show "fib (gcd (m, 0)) = gcd (fib m, fib 0)" by simp
+ fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp
fix n :: nat assume n: "0 < n"
- then have "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0)
- also assume hyp: "fib ... = gcd (fib n, fib (m mod n))"
- also from n have "... = gcd (fib n, fib m)" by (rule gcd_fib_mod)
- also have "... = gcd (fib m, fib n)" by (rule gcd_commute)
- finally show "fib (gcd (m, n)) = gcd (fib m, fib n)" .
+ then have "gcd m n = gcd n (m mod n)" by (rule gcd_non_0)
+ also assume hyp: "fib ... = gcd (fib n) (fib (m mod n))"
+ also from n have "... = gcd (fib n) (fib m)" by (rule gcd_fib_mod)
+ also have "... = gcd (fib m) (fib n)" by (rule gcd_commute)
+ finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
qed
end