1.1 --- a/src/HOL/Import/HOL/real.imp	Sun May 09 09:39:01 2010 -0700
     1.2 +++ b/src/HOL/Import/HOL/real.imp	Sun May 09 14:21:44 2010 -0700
     1.3 @@ -247,7 +247,7 @@
     1.4    "REAL_INV_POS" > "Rings.positive_imp_inverse_positive"
     1.5    "REAL_INV_NZ" > "Rings.nonzero_imp_inverse_nonzero"
     1.6    "REAL_INV_MUL" > "HOL4Real.real.REAL_INV_MUL"
     1.7 -  "REAL_INV_LT1" > "RealDef.real_inverse_gt_one"
     1.8 +  "REAL_INV_LT1" > "Fields.one_less_inverse"
     1.9    "REAL_INV_INV" > "Rings.inverse_inverse_eq"
    1.10    "REAL_INV_EQ_0" > "Rings.inverse_nonzero_iff_nonzero"
    1.11    "REAL_INV_1OVER" > "Rings.inverse_eq_divide"

     2.1 --- a/src/HOL/RealDef.thy	Sun May 09 09:39:01 2010 -0700
     2.2 +++ b/src/HOL/RealDef.thy	Sun May 09 14:21:44 2010 -0700
     2.3 @@ -506,26 +506,24 @@
     2.4  
     2.5  subsection{*More Lemmas*}
     2.6  
     2.7 +text {* BH: These lemmas should not be necessary; they should be
     2.8 +covered by existing simp rules and simplification procedures. *}
     2.9 +
    2.10  lemma real_mult_left_cancel: "(c::real) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
    2.11 -by auto
    2.12 +by simp (* redundant with mult_cancel_left *)
    2.13  
    2.14  lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
    2.15 -by auto
    2.16 +by simp (* redundant with mult_cancel_right *)
    2.17  
    2.18  lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
    2.19 -  by (force elim: order_less_asym
    2.20 -            simp add: mult_less_cancel_right)
    2.21 +by simp (* solved by linordered_ring_less_cancel_factor simproc *)
    2.22  
    2.23  lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)"
    2.24 -apply (simp add: mult_le_cancel_right)
    2.25 -apply (blast intro: elim: order_less_asym)
    2.26 -done
    2.27 +by simp (* solved by linordered_ring_le_cancel_factor simproc *)
    2.28  
    2.29  lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
    2.30 -by(simp add:mult_commute)
    2.31 -
    2.32 -lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x"
    2.33 -by (simp add: one_less_inverse_iff) (* TODO: generalize/move *)
    2.34 +by (rule mult_le_cancel_left_pos)
    2.35 +(* BH: Why doesn't "simp" prove this one, like it does the last one? *)
    2.36  
    2.37  
    2.38  subsection {* Embedding numbers into the Reals *}
    2.39 @@ -773,10 +771,6 @@
    2.40  lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0"
    2.41  by (simp add: add: real_of_nat_def)
    2.42  
    2.43 -(* FIXME: duplicates real_of_nat_ge_zero *)
    2.44 -lemma real_of_nat_ge_zero_cancel_iff: "(0 \<le> real (n::nat))"
    2.45 -by (simp add: add: real_of_nat_def)
    2.46 -
    2.47  lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)"
    2.48    apply (subgoal_tac "real n + 1 = real (Suc n)")
    2.49    apply simp
    2.50 @@ -1013,12 +1007,6 @@
    2.51  by auto
    2.52  
    2.53  
    2.54 -(*
    2.55 -FIXME: we should have this, as for type int, but many proofs would break.
    2.56 -It replaces x+-y by x-y.
    2.57 -declare real_diff_def [symmetric, simp]
    2.58 -*)
    2.59 -
    2.60  subsubsection{*Density of the Reals*}
    2.61  
    2.62  lemma real_lbound_gt_zero:

     3.1 --- a/src/HOL/SEQ.thy	Sun May 09 09:39:01 2010 -0700
     3.2 +++ b/src/HOL/SEQ.thy	Sun May 09 14:21:44 2010 -0700
     3.3 @@ -1289,7 +1289,7 @@
     3.4    hence x0: "0 < x" by simp
     3.5    assume x1: "x < 1"
     3.6    from x0 x1 have "1 < inverse x"
     3.7 -    by (rule real_inverse_gt_one)
     3.8 +    by (rule one_less_inverse)
     3.9    hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
    3.10      by (rule LIMSEQ_inverse_realpow_zero)
    3.11    thus ?thesis by (simp add: power_inverse)

     4.1 --- a/src/HOL/Transcendental.thy	Sun May 09 09:39:01 2010 -0700
     4.2 +++ b/src/HOL/Transcendental.thy	Sun May 09 14:21:44 2010 -0700
     4.3 @@ -1089,7 +1089,7 @@
     4.4  apply (rule_tac x = 1 and y = y in linorder_cases)
     4.5  apply (drule order_less_imp_le [THEN lemma_exp_total])
     4.6  apply (rule_tac [2] x = 0 in exI)
     4.7 -apply (frule_tac [3] real_inverse_gt_one)
     4.8 +apply (frule_tac [3] one_less_inverse)
     4.9  apply (drule_tac [4] order_less_imp_le [THEN lemma_exp_total], auto)
    4.10  apply (rule_tac x = "-x" in exI)
    4.11  apply (simp add: exp_minus)