avoid using real-specific versions of generic lemmas
authorhuffman
Sun May 09 17:47:43 2010 -0700 (2010-05-09)
changeset 36777be5461582d0f
parent 36776 c137ae7673d3
child 36778 739a9379e29b
avoid using real-specific versions of generic lemmas
src/HOL/Complex.thy
src/HOL/Deriv.thy
src/HOL/Ln.thy
src/HOL/Log.thy
src/HOL/RealPow.thy
src/HOL/SupInf.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Complex.thy	Sun May 09 14:21:44 2010 -0700
     1.2 +++ b/src/HOL/Complex.thy	Sun May 09 17:47:43 2010 -0700
     1.3 @@ -676,12 +676,12 @@
     1.4  by (simp add: divide_inverse rcis_def)
     1.5  
     1.6  lemma cis_divide: "cis a / cis b = cis (a - b)"
     1.7 -by (simp add: complex_divide_def cis_mult real_diff_def)
     1.8 +by (simp add: complex_divide_def cis_mult diff_def)
     1.9  
    1.10  lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
    1.11  apply (simp add: complex_divide_def)
    1.12  apply (case_tac "r2=0", simp)
    1.13 -apply (simp add: rcis_inverse rcis_mult real_diff_def)
    1.14 +apply (simp add: rcis_inverse rcis_mult diff_def)
    1.15  done
    1.16  
    1.17  lemma Re_cis [simp]: "Re(cis a) = cos a"
     2.1 --- a/src/HOL/Deriv.thy	Sun May 09 14:21:44 2010 -0700
     2.2 +++ b/src/HOL/Deriv.thy	Sun May 09 17:47:43 2010 -0700
     2.3 @@ -482,8 +482,7 @@
     2.4    shows "\<lbrakk>\<forall>n. f n \<le> f (Suc n); convergent f\<rbrakk> \<Longrightarrow> f n \<le> lim f"
     2.5  apply (rule linorder_not_less [THEN iffD1])
     2.6  apply (auto simp add: convergent_LIMSEQ_iff LIMSEQ_iff monoseq_Suc)
     2.7 -apply (drule real_less_sum_gt_zero)
     2.8 -apply (drule_tac x = "f n + - lim f" in spec, safe)
     2.9 +apply (drule_tac x = "f n - lim f" in spec, clarsimp)
    2.10  apply (drule_tac P = "%na. no\<le>na --> ?Q na" and x = "no + n" in spec, auto)
    2.11  apply (subgoal_tac "lim f \<le> f (no + n) ")
    2.12  apply (drule_tac no=no and m=n in lemma_f_mono_add)
    2.13 @@ -706,7 +705,7 @@
    2.14  apply safe
    2.15  apply simp_all
    2.16  apply (rename_tac x xa ya M Ma)
    2.17 -apply (metis linorder_not_less order_le_less real_le_trans)
    2.18 +apply (metis linorder_not_less order_le_less order_trans)
    2.19  apply (case_tac "a \<le> x & x \<le> b")
    2.20   prefer 2
    2.21   apply (rule_tac x = 1 in exI, force)
    2.22 @@ -1235,16 +1234,16 @@
    2.23        using assms
    2.24        apply auto
    2.25        apply (metis DERIV_isCont)
    2.26 -     apply (metis differentiableI real_less_def)
    2.27 +     apply (metis differentiableI less_le)
    2.28      done
    2.29    then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
    2.30        and "f b - f a = (b - a) * l"
    2.31      by auto
    2.32    
    2.33    from prems have "~(l > 0)"
    2.34 -    by (metis linorder_not_le mult_le_0_iff real_le_eq_diff)
    2.35 +    by (metis linorder_not_le mult_le_0_iff diff_le_0_iff_le)
    2.36    with prems show False
    2.37 -    by (metis DERIV_unique real_less_def)
    2.38 +    by (metis DERIV_unique less_le)
    2.39  qed
    2.40  
    2.41  lemma DERIV_nonneg_imp_nonincreasing:
    2.42 @@ -1264,13 +1263,13 @@
    2.43      apply (rule MVT)
    2.44        apply auto
    2.45        apply (metis DERIV_isCont)
    2.46 -     apply (metis differentiableI real_less_def)
    2.47 +     apply (metis differentiableI less_le)
    2.48      done
    2.49    then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
    2.50        and "f b - f a = (b - a) * l"
    2.51      by auto
    2.52    from prems have "~(l >= 0)"
    2.53 -    by (metis diff_self le_eqI le_iff_diff_le_0 real_le_antisym real_le_linear
    2.54 +    by (metis diff_self le_eqI le_iff_diff_le_0 order_antisym linear
    2.55                split_mult_pos_le)
    2.56    with prems show False
    2.57      by (metis DERIV_unique order_less_imp_le)
     3.1 --- a/src/HOL/Ln.thy	Sun May 09 14:21:44 2010 -0700
     3.2 +++ b/src/HOL/Ln.thy	Sun May 09 17:47:43 2010 -0700
     3.3 @@ -206,7 +206,7 @@
     3.4      apply auto
     3.5      done
     3.6    also have "... = exp (-x)"
     3.7 -    by (auto simp add: exp_minus real_divide_def)
     3.8 +    by (auto simp add: exp_minus divide_inverse)
     3.9    finally have "1 - x <= exp (- x)" .
    3.10    also have "1 - x = exp (ln (1 - x))"
    3.11    proof -
     4.1 --- a/src/HOL/Log.thy	Sun May 09 14:21:44 2010 -0700
     4.2 +++ b/src/HOL/Log.thy	Sun May 09 17:47:43 2010 -0700
     4.3 @@ -64,7 +64,7 @@
     4.4  by (simp add: powr_def)
     4.5  
     4.6  lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a"
     4.7 -by (simp add: powr_powr real_mult_commute)
     4.8 +by (simp add: powr_powr mult_commute)
     4.9  
    4.10  lemma powr_minus: "x powr (-a) = inverse (x powr a)"
    4.11  by (simp add: powr_def exp_minus [symmetric])
     5.1 --- a/src/HOL/RealPow.thy	Sun May 09 14:21:44 2010 -0700
     5.2 +++ b/src/HOL/RealPow.thy	Sun May 09 17:47:43 2010 -0700
     5.3 @@ -95,7 +95,7 @@
     5.4  by (intro add_nonneg_nonneg zero_le_power2)
     5.5  
     5.6  lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
     5.7 -by (rule_tac j = 0 in real_le_trans, auto)
     5.8 +by (rule_tac y = 0 in order_trans, auto)
     5.9  
    5.10  lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
    5.11  by (auto simp add: power2_eq_square)
    5.12 @@ -145,7 +145,7 @@
    5.13       "[|(0::real) < x; 0 < x1; x1 * y < x * u |] 
    5.14        ==> inverse x * y < inverse x1 * u"
    5.15  apply (rule_tac c=x in mult_less_imp_less_left) 
    5.16 -apply (auto simp add: real_mult_assoc [symmetric])
    5.17 +apply (auto simp add: mult_assoc [symmetric])
    5.18  apply (simp (no_asm) add: mult_ac)
    5.19  apply (rule_tac c=x1 in mult_less_imp_less_right) 
    5.20  apply (auto simp add: mult_ac)
     6.1 --- a/src/HOL/SupInf.thy	Sun May 09 14:21:44 2010 -0700
     6.2 +++ b/src/HOL/SupInf.thy	Sun May 09 17:47:43 2010 -0700
     6.3 @@ -74,7 +74,7 @@
     6.4  lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
     6.5    fixes x :: real
     6.6    shows "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
     6.7 -  by (metis Sup_upper real_le_trans)
     6.8 +  by (metis Sup_upper order_trans)
     6.9  
    6.10  lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*)
    6.11    fixes z :: real
    6.12 @@ -86,7 +86,7 @@
    6.13    shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a) 
    6.14          \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a"
    6.15    by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb
    6.16 -        insert_not_empty real_le_antisym)
    6.17 +        insert_not_empty order_antisym)
    6.18  
    6.19  lemma Sup_le:
    6.20    fixes S :: "real set"
    6.21 @@ -109,28 +109,28 @@
    6.22      apply (simp add: max_def)
    6.23      apply (rule Sup_eq_maximum)
    6.24      apply (rule insertI1)
    6.25 -    apply (metis Sup_upper [OF _ z] insertE real_le_linear real_le_trans)
    6.26 +    apply (metis Sup_upper [OF _ z] insertE linear order_trans)
    6.27      done
    6.28  next
    6.29    case False
    6.30    hence 1:"a < Sup X" by simp
    6.31    have "Sup X \<le> Sup (insert a X)"
    6.32      apply (rule Sup_least)
    6.33 -    apply (metis empty_psubset_nonempty psubset_eq x)
    6.34 +    apply (metis ex_in_conv x)
    6.35      apply (rule Sup_upper_EX) 
    6.36      apply blast
    6.37 -    apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
    6.38 +    apply (metis insert_iff linear order_refl order_trans z)
    6.39      done
    6.40    moreover 
    6.41    have "Sup (insert a X) \<le> Sup X"
    6.42      apply (rule Sup_least)
    6.43      apply blast
    6.44 -    apply (metis False Sup_upper insertE real_le_linear z) 
    6.45 +    apply (metis False Sup_upper insertE linear z)
    6.46      done
    6.47    ultimately have "Sup (insert a X) = Sup X"
    6.48      by (blast intro:  antisym )
    6.49    thus ?thesis
    6.50 -    by (metis 1 min_max.le_iff_sup real_less_def)
    6.51 +    by (metis 1 min_max.le_iff_sup less_le)
    6.52  qed
    6.53  
    6.54  lemma Sup_insert_if: 
    6.55 @@ -177,7 +177,7 @@
    6.56    fixes S :: "real set"
    6.57    assumes fS: "finite S" and Se: "S \<noteq> {}"
    6.58    shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
    6.59 -by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS real_le_trans)
    6.60 +by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS order_trans)
    6.61  
    6.62  lemma Sup_finite_gt_iff: 
    6.63    fixes S :: "real set"
    6.64 @@ -291,19 +291,19 @@
    6.65  lemma Inf_lower2:
    6.66    fixes x :: real
    6.67    shows "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
    6.68 -  by (metis Inf_lower real_le_trans)
    6.69 +  by (metis Inf_lower order_trans)
    6.70  
    6.71  lemma Inf_real_iff:
    6.72    fixes z :: real
    6.73    shows "X \<noteq> {} \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> Inf X < y"
    6.74 -  by (metis Inf_greatest Inf_lower less_le_not_le real_le_linear 
    6.75 +  by (metis Inf_greatest Inf_lower less_le_not_le linear
    6.76              order_less_le_trans)
    6.77  
    6.78  lemma Inf_eq:
    6.79    fixes a :: real
    6.80    shows "(!!x. x \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> Inf X = a"
    6.81    by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel
    6.82 -        insert_absorb insert_not_empty real_le_antisym)
    6.83 +        insert_absorb insert_not_empty order_antisym)
    6.84  
    6.85  lemma Inf_ge: 
    6.86    fixes S :: "real set"
    6.87 @@ -324,27 +324,27 @@
    6.88    case True
    6.89    thus ?thesis
    6.90      by (simp add: min_def)
    6.91 -       (blast intro: Inf_eq_minimum real_le_refl real_le_trans z)
    6.92 +       (blast intro: Inf_eq_minimum order_trans z)
    6.93  next
    6.94    case False
    6.95    hence 1:"Inf X < a" by simp
    6.96    have "Inf (insert a X) \<le> Inf X"
    6.97      apply (rule Inf_greatest)
    6.98 -    apply (metis empty_psubset_nonempty psubset_eq x)
    6.99 +    apply (metis ex_in_conv x)
   6.100      apply (rule Inf_lower_EX)
   6.101      apply (erule insertI2)
   6.102 -    apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
   6.103 +    apply (metis insert_iff linear order_refl order_trans z)
   6.104      done
   6.105    moreover 
   6.106    have "Inf X \<le> Inf (insert a X)"
   6.107      apply (rule Inf_greatest)
   6.108      apply blast
   6.109 -    apply (metis False Inf_lower insertE real_le_linear z) 
   6.110 +    apply (metis False Inf_lower insertE linear z) 
   6.111      done
   6.112    ultimately have "Inf (insert a X) = Inf X"
   6.113      by (blast intro:  antisym )
   6.114    thus ?thesis
   6.115 -    by (metis False min_max.inf_absorb2 real_le_linear)
   6.116 +    by (metis False min_max.inf_absorb2 linear)
   6.117  qed
   6.118  
   6.119  lemma Inf_insert_if: 
   6.120 @@ -377,13 +377,13 @@
   6.121  lemma Inf_finite_ge_iff: 
   6.122    fixes S :: "real set"
   6.123    shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
   6.124 -by (metis Inf_finite_Min Inf_finite_in Min_le real_le_trans)
   6.125 +by (metis Inf_finite_Min Inf_finite_in Min_le order_trans)
   6.126  
   6.127  lemma Inf_finite_le_iff:
   6.128    fixes S :: "real set"
   6.129    shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
   6.130  by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le
   6.131 -          real_le_antisym real_le_linear)
   6.132 +          order_antisym linear)
   6.133  
   6.134  lemma Inf_finite_gt_iff: 
   6.135    fixes S :: "real set"
   6.136 @@ -417,7 +417,7 @@
   6.137    also have "... \<le> e" 
   6.138      apply (rule Sup_asclose) 
   6.139      apply (auto simp add: S)
   6.140 -    apply (metis abs_minus_add_cancel b add_commute real_diff_def) 
   6.141 +    apply (metis abs_minus_add_cancel b add_commute diff_def)
   6.142      done
   6.143    finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
   6.144    thus ?thesis
   6.145 @@ -474,13 +474,13 @@
   6.146  proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
   6.147    show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
   6.148      by (rule SupInf.Sup_upper [where z=b], auto)
   6.149 -       (metis `a < b` `\<not> P b` real_le_linear real_less_def)
   6.150 +       (metis `a < b` `\<not> P b` linear less_le)
   6.151  next
   6.152    show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
   6.153      apply (rule SupInf.Sup_least) 
   6.154      apply (auto simp add: )
   6.155      apply (metis less_le_not_le)
   6.156 -    apply (metis `a<b` `~ P b` real_le_linear real_less_def) 
   6.157 +    apply (metis `a<b` `~ P b` linear less_le)
   6.158      done
   6.159  next
   6.160    fix x
   6.161 @@ -495,7 +495,7 @@
   6.162      assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
   6.163      thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
   6.164        by (rule_tac z="b" in SupInf.Sup_upper, auto) 
   6.165 -         (metis `a<b` `~ P b` real_le_linear real_less_def) 
   6.166 +         (metis `a<b` `~ P b` linear less_le)
   6.167  qed
   6.168  
   6.169  end
     7.1 --- a/src/HOL/Transcendental.thy	Sun May 09 14:21:44 2010 -0700
     7.2 +++ b/src/HOL/Transcendental.thy	Sun May 09 17:47:43 2010 -0700
     7.3 @@ -779,7 +779,7 @@
     7.4              finally show "\<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> \<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>" unfolding abs_real_of_nat_cancel abs_of_nonneg[OF zero_le_power[OF less_imp_le[OF `0 < R'`]]] .
     7.5              show "0 \<le> \<bar>f n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult[symmetric] by auto
     7.6            qed
     7.7 -          also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult real_mult_assoc[symmetric] by algebra
     7.8 +          also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult mult_assoc[symmetric] by algebra
     7.9            finally show ?thesis .
    7.10          qed }
    7.11        { fix n show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
    7.12 @@ -792,7 +792,7 @@
    7.13            show "\<bar>f n * x ^ n\<bar> \<le> norm (f n * real (Suc n) * x ^ n)" unfolding real_norm_def abs_mult
    7.14              by (rule mult_right_mono, auto simp add: le[unfolded mult_1_right])
    7.15          qed
    7.16 -        from this[THEN summable_mult2[where c=x], unfolded real_mult_assoc, unfolded real_mult_commute]
    7.17 +        from this[THEN summable_mult2[where c=x], unfolded mult_assoc, unfolded mult_commute]
    7.18          show "summable (?f x)" by auto }
    7.19        show "summable (?f' x0)" using converges[OF `x0 \<in> {-R <..< R}`] .
    7.20        show "x0 \<in> {-R' <..< R'}" using `x0 \<in> {-R' <..< R'}` .
    7.21 @@ -1022,7 +1022,7 @@
    7.22  lemma exp_ge_add_one_self_aux: "0 \<le> (x::real) ==> (1 + x) \<le> exp(x)"
    7.23  apply (drule order_le_imp_less_or_eq, auto)
    7.24  apply (simp add: exp_def)
    7.25 -apply (rule real_le_trans)
    7.26 +apply (rule order_trans)
    7.27  apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le)
    7.28  apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_mult_iff)
    7.29  done
    7.30 @@ -1228,7 +1228,7 @@
    7.31      have "1 / x = 1 / (1 - (1 - x))" by auto
    7.32      also have "\<dots> = (\<Sum> n. (1 - x)^n)" using geometric_sums[OF `norm (1 - x) < 1`] by (rule sums_unique)
    7.33      also have "\<dots> = suminf (?f' x)" unfolding power_mult_distrib[symmetric] by (rule arg_cong[where f=suminf], rule arg_cong[where f="op ^"], auto)
    7.34 -    finally have "DERIV ln x :> suminf (?f' x)" using DERIV_ln[OF `0 < x`] unfolding real_divide_def by auto
    7.35 +    finally have "DERIV ln x :> suminf (?f' x)" using DERIV_ln[OF `0 < x`] unfolding divide_inverse by auto
    7.36      moreover
    7.37      have repos: "\<And> h x :: real. h - 1 + x = h + x - 1" by auto
    7.38      have "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> (\<Sum>n. (-1)^n * (1 / real (n + 1)) * real (Suc n) * (x - 1) ^ n)"
    7.39 @@ -1388,7 +1388,7 @@
    7.40  
    7.41  lemma DERIV_sin_realpow2 [simp]:
    7.42       "DERIV (%x. (sin x)\<twosuperior>) x :> cos(x) * sin(x) + cos(x) * sin(x)"
    7.43 -by (auto simp add: numeral_2_eq_2 real_mult_assoc [symmetric])
    7.44 +by (auto simp add: numeral_2_eq_2 mult_assoc [symmetric])
    7.45  
    7.46  lemma DERIV_sin_realpow2a [simp]:
    7.47       "DERIV (%x. (sin x)\<twosuperior>) x :> 2 * cos(x) * sin(x)"
    7.48 @@ -1406,7 +1406,7 @@
    7.49  
    7.50  lemma DERIV_cos_realpow2 [simp]:
    7.51       "DERIV (%x. (cos x)\<twosuperior>) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
    7.52 -by (auto simp add: numeral_2_eq_2 real_mult_assoc [symmetric])
    7.53 +by (auto simp add: numeral_2_eq_2 mult_assoc [symmetric])
    7.54  
    7.55  lemma DERIV_cos_realpow2a [simp]:
    7.56       "DERIV (%x. (cos x)\<twosuperior>) x :> -2 * cos(x) * sin(x)"
    7.57 @@ -1705,8 +1705,8 @@
    7.58  apply (drule_tac f = cos in Rolle)
    7.59  apply (drule_tac [5] f = cos in Rolle)
    7.60  apply (auto dest!: DERIV_cos [THEN DERIV_unique] simp add: differentiable_def)
    7.61 -apply (metis order_less_le_trans real_less_def sin_gt_zero)
    7.62 -apply (metis order_less_le_trans real_less_def sin_gt_zero)
    7.63 +apply (metis order_less_le_trans less_le sin_gt_zero)
    7.64 +apply (metis order_less_le_trans less_le sin_gt_zero)
    7.65  done
    7.66  
    7.67  lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
    7.68 @@ -2138,9 +2138,9 @@
    7.69  apply (auto simp add: tan_def)
    7.70  apply (rule inverse_less_iff_less [THEN iffD1])
    7.71  apply (auto simp add: divide_inverse)
    7.72 -apply (rule real_mult_order) 
    7.73 +apply (rule mult_pos_pos)
    7.74  apply (subgoal_tac [3] "0 < sin e & 0 < cos e")
    7.75 -apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: mult_commute) 
    7.76 +apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: mult_commute)
    7.77  done
    7.78  
    7.79  lemma tan_total_pos: "0 \<le> y ==> \<exists>x. 0 \<le> x & x < pi/2 & tan x = y"
    7.80 @@ -2193,7 +2193,7 @@
    7.81    hence "0 < cos z" using cos_gt_zero_pi by auto
    7.82    hence inv_pos: "0 < inverse ((cos z)\<twosuperior>)" by auto
    7.83    have "0 < x - y" using `y < x` by auto
    7.84 -  from real_mult_order[OF this inv_pos]
    7.85 +  from mult_pos_pos [OF this inv_pos]
    7.86    have "0 < tan x - tan y" unfolding tan_diff by auto
    7.87    thus ?thesis by auto
    7.88  qed
    7.89 @@ -2226,7 +2226,7 @@
    7.90  lemma tan_periodic_nat[simp]: fixes n :: nat shows "tan (x + real n * pi) = tan x" 
    7.91  proof (induct n arbitrary: x)
    7.92    case (Suc n)
    7.93 -  have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_eq_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
    7.94 +  have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_eq_plus1 real_of_nat_add real_of_one left_distrib by auto
    7.95    show ?case unfolding split_pi_off using Suc by auto
    7.96  qed auto
    7.97  
    7.98 @@ -2439,7 +2439,7 @@
    7.99  apply (subgoal_tac "isCont arctan (tan (arctan x))", simp)
   7.100  apply (erule (1) isCont_inverse_function2 [where f=tan])
   7.101  apply (metis arctan_tan order_le_less_trans order_less_le_trans)
   7.102 -apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans real_less_def)
   7.103 +apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le)
   7.104  done
   7.105  
   7.106  lemma DERIV_arcsin:
   7.107 @@ -2953,7 +2953,7 @@
   7.108        }
   7.109        hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
   7.110        moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
   7.111 -        unfolding real_diff_def divide_inverse
   7.112 +        unfolding diff_def divide_inverse
   7.113          by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum)
   7.114        ultimately have "0 \<le> ?a 1 n - ?diff 1 n" by (rule LIM_less_bound)
   7.115        hence "?diff 1 n \<le> ?a 1 n" by auto
   7.116 @@ -2969,7 +2969,7 @@
   7.117          have "norm (?diff 1 n - 0) < r" by auto }
   7.118        thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
   7.119      qed
   7.120 -    from this[unfolded LIMSEQ_rabs_zero real_diff_def add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus]
   7.121 +    from this[unfolded LIMSEQ_rabs_zero diff_def add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus]
   7.122      have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
   7.123      hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
   7.124