src/HOL/Number_Theory/Fib.thy
 changeset 36350 bc7982c54e37 parent 35644 d20cf282342e child 41541 1fa4725c4656
```     1.1 --- a/src/HOL/Number_Theory/Fib.thy	Mon Apr 26 11:34:17 2010 +0200
1.2 +++ b/src/HOL/Number_Theory/Fib.thy	Mon Apr 26 11:34:19 2010 +0200
1.3 @@ -143,9 +143,9 @@
1.4    apply (induct n rule: fib_induct_nat)
1.5    apply auto
1.6    apply (subst fib_reduce_nat)
1.7 -  apply (auto simp add: ring_simps)
1.8 +  apply (auto simp add: field_simps)
1.9    apply (subst (1 3 5) fib_reduce_nat)
1.10 -  apply (auto simp add: ring_simps Suc_eq_plus1)
1.11 +  apply (auto simp add: field_simps Suc_eq_plus1)
1.12  (* hmmm. Why doesn't "n + (1 + (1 + k))" simplify to "n + k + 2"? *)
1.13    apply (subgoal_tac "n + (k + 2) = n + (1 + (1 + k))")
1.14    apply (erule ssubst) back back
1.15 @@ -184,7 +184,7 @@
1.16  lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
1.17      (fib (int n + 1))^2 = (-1)^(n + 1)"
1.18    apply (induct n)
1.19 -  apply (auto simp add: ring_simps power2_eq_square fib_reduce_int
1.20 +  apply (auto simp add: field_simps power2_eq_square fib_reduce_int
1.22  done
1.23
1.24 @@ -222,7 +222,7 @@
1.25    apply (subst (2) fib_reduce_nat)
1.26    apply (auto simp add: Suc_eq_plus1) (* again, natdiff_cancel *)
1.28 -  apply (subst gcd_commute_nat, auto simp add: ring_simps)
1.29 +  apply (subst gcd_commute_nat, auto simp add: field_simps)
1.30  done
1.31
1.32  lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
1.33 @@ -305,7 +305,7 @@
1.34  theorem fib_mult_eq_setsum_nat:
1.35      "fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
1.36    apply (induct n)
1.37 -  apply (auto simp add: atMost_plus_one_nat fib_plus_2_nat ring_simps)
1.38 +  apply (auto simp add: atMost_plus_one_nat fib_plus_2_nat field_simps)
1.39  done
1.40
1.41  theorem fib_mult_eq_setsum'_nat:
```