# HG changeset patch
# User haftmann
# Date 1184052194 -7200
# Node ID 7cd68def72b2c5f011bacb553dc1eef5efa6125d
# Parent  06884f7ffb18bb6725e15ab8338462113b3c1f83
expanded fragile proof

diff -r 06884f7ffb18 -r 7cd68def72b2 src/HOL/NumberTheory/Fib.thy
--- a/src/HOL/NumberTheory/Fib.thy	Tue Jul 10 09:23:13 2007 +0200
+++ b/src/HOL/NumberTheory/Fib.thy	Tue Jul 10 09:23:14 2007 +0200
@@ -114,9 +114,25 @@
   by (simp add: gcd_fib_add [symmetric, of _ "n-m"]) 
 
 lemma gcd_fib_mod: "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
-  apply (induct n rule: nat_less_induct)
-  apply (simp add: mod_if gcd_fib_diff mod_geq)
-  done
+proof (induct n rule: less_induct)
+  case (less n)
+  from less.prems have pos_m: "0 < m" .
+  show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
+  proof (cases "m < n")
+    case True note m_n = True
+    then have m_n': "m \<le> n" by auto
+    with pos_m have pos_n: "0 < n" by auto
+    with pos_m m_n have diff: "n - m < n" by auto
+    have "gcd (fib m, fib (n mod m)) = gcd (fib m, fib ((n - m) mod m))"
+    by (simp add: mod_if [of n]) (insert m_n, auto)
+    also have "\<dots> = gcd (fib m, fib (n - m))" by (simp add: less.hyps diff pos_m)
+    also have "\<dots> = gcd (fib m, fib n)" by (simp add: gcd_fib_diff m_n')
+    finally show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" .
+  next
+    case False then show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
+    by (cases "m = n") auto
+  qed
+qed
 
 lemma fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)"  -- {* Law 6.111 *}
   apply (induct m n rule: gcd_induct)