tuned proofs -- fewer warnings;
authorwenzelm
Tue Aug 05 16:58:19 2014 +0200 (2014-08-05)
changeset 57865dcfb33c26f50
parent 57864 7cf01ece66e4
child 57866 1dbc506289bb
tuned proofs -- fewer warnings;
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Algebra/Divisibility.thy	Tue Aug 05 16:21:27 2014 +0200
     1.2 +++ b/src/HOL/Algebra/Divisibility.thy	Tue Aug 05 16:58:19 2014 +0200
     1.3 @@ -74,7 +74,7 @@
     1.4    have c: "inv (a \<otimes> b) \<otimes> a \<in> carrier G" by simp
     1.5  
     1.6    have "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = inv (a \<otimes> b) \<otimes> (a \<otimes> b)" by (simp add: m_assoc)
     1.7 -  also have "\<dots> = \<one>" by (simp add: Units_l_inv)
     1.8 +  also have "\<dots> = \<one>" by simp
     1.9    finally have li: "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = \<one>" .
    1.10  
    1.11    have "\<one> = inv a \<otimes> a" by (simp add: Units_l_inv[symmetric])
    1.12 @@ -83,7 +83,7 @@
    1.13         by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv)
    1.14    also have "\<dots> = ((inv a \<otimes> a) \<otimes> b) \<otimes> inv (a \<otimes> b) \<otimes> a"
    1.15      by (simp add: m_assoc del: Units_l_inv)
    1.16 -  also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by (simp add: Units_l_inv)
    1.17 +  also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by simp
    1.18    also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> a)" by (simp add: m_assoc)
    1.19    finally have ri: "b \<otimes> (inv (a \<otimes> b) \<otimes> a) = \<one> " by simp
    1.20  
    1.21 @@ -327,7 +327,7 @@
    1.22  unfolding a
    1.23  apply (intro associatedI)
    1.24   apply (rule dividesI[of "inv u"], simp)
    1.25 - apply (simp add: m_assoc Units_closed Units_r_inv)
    1.26 + apply (simp add: m_assoc Units_closed)
    1.27  apply fast
    1.28  done
    1.29  
    1.30 @@ -1764,7 +1764,7 @@
    1.31    note [simp] = acarr Units_closed[OF uunit] Units_inv_closed[OF uunit]
    1.32  
    1.33    have "a = a \<otimes> \<one>" by simp
    1.34 -  also have "\<dots> = a \<otimes> (u \<otimes> inv u)" by (simp add: Units_r_inv uunit)
    1.35 +  also have "\<dots> = a \<otimes> (u \<otimes> inv u)" by (simp add: uunit)
    1.36    also have "\<dots> = a' \<otimes> inv u" by (simp add: m_assoc[symmetric] a'[symmetric])
    1.37    finally
    1.38         have a: "a = a' \<otimes> inv u" .
    1.39 @@ -2646,7 +2646,7 @@
    1.40      hence yb: "fmset G ys \<le> fmset G bs" by (rule divides_fmsubset) fact+
    1.41  
    1.42      from ya yb csmset
    1.43 -    have "fmset G ys \<le> fmset G cs" by (simp add: mset_le_def multiset_inter_count)
    1.44 +    have "fmset G ys \<le> fmset G cs" by (simp add: mset_le_def)
    1.45      thus "y divides c" by (rule fmsubset_divides) fact+
    1.46    qed
    1.47  
    1.48 @@ -3208,7 +3208,7 @@
    1.49            and nyx: "\<not> y \<sim> x"
    1.50            by - (fast elim: properfactorE2)+
    1.51        hence "\<exists>z. z \<in> carrier G \<and> x = y \<otimes> z"
    1.52 -          by (fast elim: dividesE)
    1.53 +          by fast
    1.54  
    1.55        from this obtain z
    1.56            where zcarr: "z \<in> carrier G"
    1.57 @@ -3327,7 +3327,7 @@
    1.58        and afs': "wfactors G as' a"
    1.59      hence ahdvda: "ah divides a"
    1.60        by (intro wfactors_dividesI[of "ah#as" "a"], simp+)
    1.61 -    hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by (fast elim: dividesE)
    1.62 +    hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by fast
    1.63      from this obtain a'
    1.64        where a'carr: "a' \<in> carrier G"
    1.65        and a: "a = ah \<otimes> a'"
    1.66 @@ -3360,7 +3360,7 @@
    1.67        have asicarr[simp]: "as'!i \<in> carrier G" by (unfold set_conv_nth, force)
    1.68      note carr = carr asicarr
    1.69  
    1.70 -    from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by (fast elim: dividesE)
    1.71 +    from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by fast
    1.72      from this obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" by auto
    1.73  
    1.74      with carr irrasi[simplified asi]
    1.75 @@ -3454,7 +3454,7 @@
    1.76      next
    1.77        show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'"
    1.78        apply (simp add: list_all2_append)
    1.79 -      apply (simp add: asiah[symmetric] ahcarr asicarr)
    1.80 +      apply (simp add: asiah[symmetric])
    1.81        done
    1.82      qed
    1.83  
    1.84 @@ -3463,12 +3463,12 @@
    1.85      also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
    1.86        (take i as' @ as' ! i # drop (Suc i) as')"
    1.87        apply (intro essentially_equalI)
    1.88 -      apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~> 
    1.89 +       apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~> 
    1.90          take i as' @ as' ! i # drop (Suc i) as'")
    1.91 -  apply simp
    1.92 +        apply simp
    1.93         apply (rule perm_append_Cons)
    1.94        apply simp
    1.95 -    done
    1.96 +      done
    1.97      finally
    1.98        have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')" by simp
    1.99      then show "essentially_equal G (ah # as) as'" by (subst as', assumption)
   1.100 @@ -3617,7 +3617,7 @@
   1.101      also from ccarr acarr cunit
   1.102          have "\<dots> = a \<otimes> (c \<otimes> inv c)" by (fast intro: m_assoc)
   1.103      also from ccarr cunit
   1.104 -        have "\<dots> = a \<otimes> \<one>" by (simp add: Units_r_inv)
   1.105 +        have "\<dots> = a \<otimes> \<one>" by simp
   1.106      also from acarr
   1.107          have "\<dots> = a" by simp
   1.108      finally have "a = b \<otimes> inv c" by simp
   1.109 @@ -3706,7 +3706,7 @@
   1.110    shows "(divisor_chain_condition_monoid G \<and> gcd_condition_monoid G) = factorial_monoid G"
   1.111  apply rule
   1.112  proof clarify
   1.113 -    assume dcc: "divisor_chain_condition_monoid G"
   1.114 +  assume dcc: "divisor_chain_condition_monoid G"
   1.115       and gc: "gcd_condition_monoid G"
   1.116    interpret divisor_chain_condition_monoid "G" by (rule dcc)
   1.117    interpret gcd_condition_monoid "G" by (rule gc)
     2.1 --- a/src/HOL/Algebra/Exponent.thy	Tue Aug 05 16:21:27 2014 +0200
     2.2 +++ b/src/HOL/Algebra/Exponent.thy	Tue Aug 05 16:58:19 2014 +0200
     2.3 @@ -249,7 +249,7 @@
     2.4  apply (simp (no_asm))
     2.5  (*induction step*)
     2.6  apply (subgoal_tac "(Suc (j+k) choose Suc k) > 0")
     2.7 - prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
     2.8 + prefer 2 apply (simp, clarify)
     2.9  apply (subgoal_tac "exponent p ((Suc (j+k) choose Suc k) * Suc k) = 
    2.10                      exponent p (Suc k)")
    2.11   txt{*First, use the assumed equation.  We simplify the LHS to
    2.12 @@ -260,7 +260,7 @@
    2.13     @{text Suc_times_binomial_eq} ...*}
    2.14  apply (simp del: bad_Sucs add: Suc_times_binomial_eq [symmetric])
    2.15  txt{*...then @{text exponent_mult_add} and the quantified premise.*}
    2.16 -apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add)
    2.17 +apply (simp del: bad_Sucs add: exponent_mult_add)
    2.18  done
    2.19  
    2.20  (*The lemma above, with two changes of variables*)
     3.1 --- a/src/HOL/Algebra/UnivPoly.thy	Tue Aug 05 16:21:27 2014 +0200
     3.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Tue Aug 05 16:58:19 2014 +0200
     3.3 @@ -528,7 +528,7 @@
     3.4      case 0 with R show ?thesis by simp
     3.5    next
     3.6      case Suc with R show ?thesis
     3.7 -      using R.finsum_Suc2 by (simp del: R.finsum_Suc add: R.r_null Pi_def)
     3.8 +      using R.finsum_Suc2 by (simp del: R.finsum_Suc add: Pi_def)
     3.9    qed
    3.10  qed (simp_all add: R)
    3.11  
     4.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Aug 05 16:21:27 2014 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Aug 05 16:58:19 2014 +0200
     4.3 @@ -137,17 +137,17 @@
     4.4  end
     4.5  *} "lift trivial vector statements to real arith statements"
     4.6  
     4.7 -lemma vec_0[simp]: "vec 0 = 0" by (vector zero_vec_def)
     4.8 -lemma vec_1[simp]: "vec 1 = 1" by (vector one_vec_def)
     4.9 +lemma vec_0[simp]: "vec 0 = 0" by vector
    4.10 +lemma vec_1[simp]: "vec 1 = 1" by vector
    4.11  
    4.12  lemma vec_inj[simp]: "vec x = vec y \<longleftrightarrow> x = y" by vector
    4.13  
    4.14  lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
    4.15  
    4.16 -lemma vec_add: "vec(x + y) = vec x + vec y"  by (vector vec_def)
    4.17 -lemma vec_sub: "vec(x - y) = vec x - vec y" by (vector vec_def)
    4.18 -lemma vec_cmul: "vec(c * x) = c *s vec x " by (vector vec_def)
    4.19 -lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def)
    4.20 +lemma vec_add: "vec(x + y) = vec x + vec y"  by vector
    4.21 +lemma vec_sub: "vec(x - y) = vec x - vec y" by vector
    4.22 +lemma vec_cmul: "vec(c * x) = c *s vec x " by vector
    4.23 +lemma vec_neg: "vec(- x) = - vec x " by vector
    4.24  
    4.25  lemma vec_setsum:
    4.26    assumes "finite S"
    4.27 @@ -164,7 +164,7 @@
    4.28  text{* Obvious "component-pushing". *}
    4.29  
    4.30  lemma vec_component [simp]: "vec x $ i = x"
    4.31 -  by (vector vec_def)
    4.32 +  by vector
    4.33  
    4.34  lemma vector_mult_component [simp]: "(x * y)$i = x$i * y$i"
    4.35    by vector
    4.36 @@ -330,7 +330,7 @@
    4.37    assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"
    4.38    shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) *  e"
    4.39    using setsum_norm_allsubsets_bound[OF assms]
    4.40 -  by (simp add: DIM_cart Basis_real_def)
    4.41 +  by simp
    4.42  
    4.43  subsection {* Matrix operations *}
    4.44  
     5.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Aug 05 16:21:27 2014 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Aug 05 16:58:19 2014 +0200
     5.3 @@ -1502,7 +1502,7 @@
     5.4        by (intro convex_linear_vimage convex_translation convex_convex_hull,
     5.5          simp add: linear_iff)
     5.6      also have "?S = {y. (x, y) \<in> convex hull (s \<times> t)}"
     5.7 -      by (auto simp add: uminus_add_conv_diff image_def Bex_def)
     5.8 +      by (auto simp add: image_def Bex_def)
     5.9      finally show "convex {y. (x, y) \<in> convex hull (s \<times> t)}" .
    5.10    next
    5.11      show "convex {x. \<forall>y\<in>convex hull t. (x, y) \<in> convex hull (s \<times> t)}"
    5.12 @@ -1512,7 +1512,7 @@
    5.13        by (intro convex_linear_vimage convex_translation convex_convex_hull,
    5.14          simp add: linear_iff)
    5.15        also have "?S = {x. (x, y) \<in> convex hull (s \<times> t)}"
    5.16 -        by (auto simp add: uminus_add_conv_diff image_def Bex_def)
    5.17 +        by (auto simp add: image_def Bex_def)
    5.18        finally show "convex {x. (x, y) \<in> convex hull (s \<times> t)}" .
    5.19      qed
    5.20    qed
    5.21 @@ -5504,12 +5504,12 @@
    5.22      using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` s",
    5.23        OF convex_affinity compact_affinity]
    5.24      using assms(1,2)
    5.25 -    by (auto simp add: uminus_add_conv_diff scaleR_right_diff_distrib)
    5.26 +    by (auto simp add: scaleR_right_diff_distrib)
    5.27    then show ?thesis
    5.28      apply (rule_tac homeomorphic_trans[OF _ homeomorphic_balls(2)[of 1 _ ?n]])
    5.29      apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" s "?d *\<^sub>R -a"]])
    5.30      using `d>0` `e>0`
    5.31 -    apply (auto simp add: uminus_add_conv_diff scaleR_right_diff_distrib)
    5.32 +    apply (auto simp add: scaleR_right_diff_distrib)
    5.33      done
    5.34  qed
    5.35  
    5.36 @@ -5808,7 +5808,7 @@
    5.37    apply (rule_tac f="\<lambda>x. a + x" in arg_cong)
    5.38    apply (rule setsum.cong [OF refl])
    5.39    apply clarsimp
    5.40 -  apply (fast intro: set_plus_intro)
    5.41 +  apply fast
    5.42    done
    5.43  
    5.44  lemma box_eq_set_setsum_Basis:
    5.45 @@ -5895,7 +5895,7 @@
    5.46      apply (rule image_eqI[where x="{i. i\<in>Basis \<and> x\<bullet>i = 1}"])
    5.47      using as
    5.48      apply (subst euclidean_eq_iff)
    5.49 -    apply (auto simp: inner_setsum_left_Basis)
    5.50 +    apply auto
    5.51      done
    5.52  qed auto
    5.53  
    5.54 @@ -6430,7 +6430,7 @@
    5.55          apply (subst (asm) euclidean_eq_iff)
    5.56          using i
    5.57          apply (erule_tac x=i in ballE)
    5.58 -        apply (auto simp add:field_simps inner_simps)
    5.59 +        apply (auto simp add: field_simps inner_simps)
    5.60          done
    5.61        finally show "x \<bullet> i =
    5.62          ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) \<bullet> i"
    5.63 @@ -8138,8 +8138,7 @@
    5.64      and "convex S"
    5.65      and "rel_open S"
    5.66    shows "convex (f ` S) \<and> rel_open (f ` S)"
    5.67 -  by (metis assms convex_linear_image rel_interior_convex_linear_image
    5.68 -    linear_conv_bounded_linear rel_open_def)
    5.69 +  by (metis assms convex_linear_image rel_interior_convex_linear_image rel_open_def)
    5.70  
    5.71  lemma convex_rel_open_linear_preimage:
    5.72    fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
     6.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Aug 05 16:21:27 2014 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Aug 05 16:58:19 2014 +0200
     6.3 @@ -69,7 +69,7 @@
     6.4  lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
     6.5      bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x within s)"
     6.6    unfolding has_derivative_def Lim
     6.7 -  by (auto simp add: netlimit_within inverse_eq_divide field_simps)
     6.8 +  by (auto simp add: netlimit_within field_simps)
     6.9  
    6.10  lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
    6.11      bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x)"
    6.12 @@ -1773,9 +1773,9 @@
    6.13          apply (rule lem3[rule_format])+
    6.14          done
    6.15        obtain N where N: "\<forall>h. norm (f' N x h - g' x h) \<le> 1 * norm h"
    6.16 -        using assms(3) `x \<in> s` by (fast intro: zero_less_one order_refl)
    6.17 +        using assms(3) `x \<in> s` by (fast intro: zero_less_one)
    6.18        have "bounded_linear (f' N x)"
    6.19 -        using assms(2) `x \<in> s` by (fast dest: has_derivative_bounded_linear)
    6.20 +        using assms(2) `x \<in> s` by fast
    6.21        from bounded_linear.bounded [OF this]
    6.22        obtain K where K: "\<forall>h. norm (f' N x h) \<le> norm h * K" ..
    6.23        {
     7.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Aug 05 16:21:27 2014 +0200
     7.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Aug 05 16:58:19 2014 +0200
     7.3 @@ -1125,7 +1125,7 @@
     7.4    note fin = this
     7.5    have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
     7.6      using f
     7.7 -    by (auto intro!: summable_ereal_pos summable_sums simp: ereal_le_real_iff zero_ereal_def)
     7.8 +    by (auto intro!: summable_ereal_pos simp: ereal_le_real_iff zero_ereal_def)
     7.9    also have "\<dots> = ereal r"
    7.10      using fin r by (auto simp: ereal_real)
    7.11    finally show "\<exists>r. (\<lambda>i. real (f i)) sums r"
    7.12 @@ -1252,7 +1252,8 @@
    7.13    apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union)
    7.14    apply (drule sym)
    7.15    apply auto
    7.16 -  by (metis INF_absorb centre_in_ball)
    7.17 +  apply (metis INF_absorb centre_in_ball)
    7.18 +  done
    7.19  
    7.20  
    7.21  lemma suminf_ereal_offset_le:
     8.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Aug 05 16:21:27 2014 +0200
     8.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Aug 05 16:58:19 2014 +0200
     8.3 @@ -343,7 +343,7 @@
     8.4                  using Basis_le_norm[OF k, of "?z - y"] unfolding dist_norm by auto
     8.5                then have "y\<bullet>k < a\<bullet>k"
     8.6                  using e[THEN conjunct1] k
     8.7 -                by (auto simp add: field_simps abs_less_iff as inner_Basis inner_simps)
     8.8 +                by (auto simp add: field_simps abs_less_iff as inner_simps)
     8.9                then have "y \<notin> i"
    8.10                  unfolding ab mem_box by (auto intro!: bexI[OF _ k])
    8.11                then show False using yi by auto
    8.12 @@ -12092,7 +12092,7 @@
    8.13      by (induct I) (auto intro!: bounded_linear_add bounded_linear_zero)
    8.14  next
    8.15    case False
    8.16 -  then show ?thesis by (simp add: bounded_linear_zero)
    8.17 +  then show ?thesis by simp
    8.18  qed
    8.19  
    8.20  lemma absolutely_integrable_vector_abs:
     9.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 05 16:21:27 2014 +0200
     9.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 05 16:58:19 2014 +0200
     9.3 @@ -7307,27 +7307,27 @@
     9.4  
     9.5  lemma real_affinity_le:
     9.6   "0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c \<le> y \<longleftrightarrow> x \<le> inverse(m) * y + -(c / m))"
     9.7 -  by (simp add: field_simps inverse_eq_divide)
     9.8 +  by (simp add: field_simps)
     9.9  
    9.10  lemma real_le_affinity:
    9.11   "0 < (m::'a::linordered_field) \<Longrightarrow> (y \<le> m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) \<le> x)"
    9.12 -  by (simp add: field_simps inverse_eq_divide)
    9.13 +  by (simp add: field_simps)
    9.14  
    9.15  lemma real_affinity_lt:
    9.16   "0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c < y \<longleftrightarrow> x < inverse(m) * y + -(c / m))"
    9.17 -  by (simp add: field_simps inverse_eq_divide)
    9.18 +  by (simp add: field_simps)
    9.19  
    9.20  lemma real_lt_affinity:
    9.21   "0 < (m::'a::linordered_field) \<Longrightarrow> (y < m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) < x)"
    9.22 -  by (simp add: field_simps inverse_eq_divide)
    9.23 +  by (simp add: field_simps)
    9.24  
    9.25  lemma real_affinity_eq:
    9.26   "(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (m * x + c = y \<longleftrightarrow> x = inverse(m) * y + -(c / m))"
    9.27 -  by (simp add: field_simps inverse_eq_divide)
    9.28 +  by (simp add: field_simps)
    9.29  
    9.30  lemma real_eq_affinity:
    9.31   "(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (y = m * x + c  \<longleftrightarrow> inverse(m) * y + -(c / m) = x)"
    9.32 -  by (simp add: field_simps inverse_eq_divide)
    9.33 +  by (simp add: field_simps)
    9.34  
    9.35  
    9.36  subsection {* Banach fixed point theorem (not really topological...) *}