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.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)