expanded fragile proof
authorhaftmann
Tue Jul 10 09:23:14 2007 +0200 (2007-07-10)
changeset 236887cd68def72b2
parent 23687 06884f7ffb18
child 23689 0410269099dc
expanded fragile proof
src/HOL/NumberTheory/Fib.thy
     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.4    by (simp add: gcd_fib_add [symmetric, of _ "n-m"]) 
     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)