src/HOL/RComplete.thy
changeset 29667 53103fc8ffa3
parent 28952 15a4b2cf8c34
child 30097 57df8626c23b
child 30240 5b25fee0362c
     1.1 --- a/src/HOL/RComplete.thy	Sun Jan 18 13:58:17 2009 +0100
     1.2 +++ b/src/HOL/RComplete.thy	Wed Jan 28 16:29:16 2009 +0100
     1.3 @@ -376,7 +376,7 @@
     1.4    hence "real (Suc n) * (inverse (real (Suc n)) * x) < real (Suc n) * 1"
     1.5      by (rule mult_strict_left_mono) simp
     1.6    hence "x < real (Suc n)"
     1.7 -    by (simp add: ring_simps)
     1.8 +    by (simp add: algebra_simps)
     1.9    thus "\<exists>(n::nat). x < real n" ..
    1.10  qed
    1.11  
    1.12 @@ -391,9 +391,9 @@
    1.13    hence "y * inverse x * x < real n * x"
    1.14      using x_greater_zero by (simp add: mult_strict_right_mono)
    1.15    hence "x * inverse x * y < x * real n"
    1.16 -    by (simp add: ring_simps)
    1.17 +    by (simp add: algebra_simps)
    1.18    hence "y < real (n::nat) * x"
    1.19 -    using x_not_zero by (simp add: ring_simps)
    1.20 +    using x_not_zero by (simp add: algebra_simps)
    1.21    thus "\<exists>(n::nat). y < real n * x" ..
    1.22  qed
    1.23  
    1.24 @@ -1084,9 +1084,7 @@
    1.25  done
    1.26  
    1.27  lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)"
    1.28 -  apply (simp add: compare_rls)
    1.29 -  apply (rule real_natfloor_add_one_gt)
    1.30 -done
    1.31 +using real_natfloor_add_one_gt by (simp add: algebra_simps)
    1.32  
    1.33  lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n"
    1.34    apply (subgoal_tac "z < real(natfloor z) + 1")
    1.35 @@ -1279,7 +1277,7 @@
    1.36      by simp
    1.37    also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /
    1.38      real y + (x - real(natfloor x)) / real y"
    1.39 -    by (auto simp add: ring_simps add_divide_distrib
    1.40 +    by (auto simp add: algebra_simps add_divide_distrib
    1.41        diff_divide_distrib prems)
    1.42    finally have "natfloor (x / real y) = natfloor(...)" by simp
    1.43    also have "... = natfloor(real((natfloor x) mod y) /
    1.44 @@ -1293,7 +1291,7 @@
    1.45      apply simp
    1.46      apply (simp add: prems)
    1.47      apply (rule divide_nonneg_pos)
    1.48 -    apply (simp add: compare_rls)
    1.49 +    apply (simp add: algebra_simps)
    1.50      apply (rule real_natfloor_le)
    1.51      apply (insert prems, auto)
    1.52      done
    1.53 @@ -1306,7 +1304,7 @@
    1.54      apply force
    1.55      apply (force simp add: prems)
    1.56      apply (rule divide_nonneg_pos)
    1.57 -    apply (simp add: compare_rls)
    1.58 +    apply (simp add: algebra_simps)
    1.59      apply (rule real_natfloor_le)
    1.60      apply (auto simp add: prems)
    1.61      apply (insert prems, arith)
    1.62 @@ -1314,8 +1312,8 @@
    1.63      apply (subgoal_tac "real y = real y - 1 + 1")
    1.64      apply (erule ssubst)
    1.65      apply (rule add_le_less_mono)
    1.66 -    apply (simp add: compare_rls)
    1.67 -    apply (subgoal_tac "real(natfloor x mod y) + 1 =
    1.68 +    apply (simp add: algebra_simps)
    1.69 +    apply (subgoal_tac "1 + real(natfloor x mod y) =
    1.70        real(natfloor x mod y + 1)")
    1.71      apply (erule ssubst)
    1.72      apply (subst real_of_nat_le_iff)
    1.73 @@ -1323,9 +1321,8 @@
    1.74      apply arith
    1.75      apply (rule mod_less_divisor)
    1.76      apply auto
    1.77 -    apply (simp add: compare_rls)
    1.78 -    apply (subst add_commute)
    1.79 -    apply (rule real_natfloor_add_one_gt)
    1.80 +    using real_natfloor_add_one_gt
    1.81 +    apply (simp add: algebra_simps)
    1.82      done
    1.83    finally show ?thesis by simp
    1.84  qed