author haftmann Tue Jul 10 09:23:14 2007 +0200 (2007-07-10) changeset 23688 7cd68def72b2 parent 23687 06884f7ffb18 child 23689 0410269099dc
expanded fragile proof
```     1.1 --- a/src/HOL/NumberTheory/Fib.thy	Tue Jul 10 09:23:13 2007 +0200
1.2 +++ b/src/HOL/NumberTheory/Fib.thy	Tue Jul 10 09:23:14 2007 +0200
1.3 @@ -114,9 +114,25 @@
1.5
1.6  lemma gcd_fib_mod: "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
1.7 -  apply (induct n rule: nat_less_induct)
1.8 -  apply (simp add: mod_if gcd_fib_diff mod_geq)
1.9 -  done
1.10 +proof (induct n rule: less_induct)
1.11 +  case (less n)
1.12 +  from less.prems have pos_m: "0 < m" .
1.13 +  show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
1.14 +  proof (cases "m < n")
1.15 +    case True note m_n = True
1.16 +    then have m_n': "m \<le> n" by auto
1.17 +    with pos_m have pos_n: "0 < n" by auto
1.18 +    with pos_m m_n have diff: "n - m < n" by auto
1.19 +    have "gcd (fib m, fib (n mod m)) = gcd (fib m, fib ((n - m) mod m))"
1.20 +    by (simp add: mod_if [of n]) (insert m_n, auto)
1.21 +    also have "\<dots> = gcd (fib m, fib (n - m))" by (simp add: less.hyps diff pos_m)
1.22 +    also have "\<dots> = gcd (fib m, fib n)" by (simp add: gcd_fib_diff m_n')
1.23 +    finally show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" .
1.24 +  next
1.25 +    case False then show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
1.26 +    by (cases "m = n") auto
1.27 +  qed
1.28 +qed
1.29
1.30  lemma fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)"  -- {* Law 6.111 *}
1.31    apply (induct m n rule: gcd_induct)
```