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.21        power_add)
    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.27    apply (subst add_commute, auto)
    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: