# HG changeset patch
# User huffman
# Date 1273440104 25200
# Node ID c137ae7673d3f6c3585273e1ba1ae74d7465b68e
# Parent  ba2a7096dd2bf414b938f690e48287533378465e
remove a couple of redundant lemmas; simplify some proofs

diff -r ba2a7096dd2b -r c137ae7673d3 src/HOL/Import/HOL/real.imp
--- a/src/HOL/Import/HOL/real.imp	Sun May 09 09:39:01 2010 -0700
+++ b/src/HOL/Import/HOL/real.imp	Sun May 09 14:21:44 2010 -0700
@@ -247,7 +247,7 @@
   "REAL_INV_POS" > "Rings.positive_imp_inverse_positive"
   "REAL_INV_NZ" > "Rings.nonzero_imp_inverse_nonzero"
   "REAL_INV_MUL" > "HOL4Real.real.REAL_INV_MUL"
-  "REAL_INV_LT1" > "RealDef.real_inverse_gt_one"
+  "REAL_INV_LT1" > "Fields.one_less_inverse"
   "REAL_INV_INV" > "Rings.inverse_inverse_eq"
   "REAL_INV_EQ_0" > "Rings.inverse_nonzero_iff_nonzero"
   "REAL_INV_1OVER" > "Rings.inverse_eq_divide"
diff -r ba2a7096dd2b -r c137ae7673d3 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Sun May 09 09:39:01 2010 -0700
+++ b/src/HOL/RealDef.thy	Sun May 09 14:21:44 2010 -0700
@@ -506,26 +506,24 @@
 
 subsection{*More Lemmas*}
 
+text {* BH: These lemmas should not be necessary; they should be
+covered by existing simp rules and simplification procedures. *}
+
 lemma real_mult_left_cancel: "(c::real) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
-by auto
+by simp (* redundant with mult_cancel_left *)
 
 lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
-by auto
+by simp (* redundant with mult_cancel_right *)
 
 lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
-  by (force elim: order_less_asym
-            simp add: mult_less_cancel_right)
+by simp (* solved by linordered_ring_less_cancel_factor simproc *)
 
 lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)"
-apply (simp add: mult_le_cancel_right)
-apply (blast intro: elim: order_less_asym)
-done
+by simp (* solved by linordered_ring_le_cancel_factor simproc *)
 
 lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
-by(simp add:mult_commute)
-
-lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x"
-by (simp add: one_less_inverse_iff) (* TODO: generalize/move *)
+by (rule mult_le_cancel_left_pos)
+(* BH: Why doesn't "simp" prove this one, like it does the last one? *)
 
 
 subsection {* Embedding numbers into the Reals *}
@@ -773,10 +771,6 @@
 lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0"
 by (simp add: add: real_of_nat_def)
 
-(* FIXME: duplicates real_of_nat_ge_zero *)
-lemma real_of_nat_ge_zero_cancel_iff: "(0 \<le> real (n::nat))"
-by (simp add: add: real_of_nat_def)
-
 lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)"
   apply (subgoal_tac "real n + 1 = real (Suc n)")
   apply simp
@@ -1013,12 +1007,6 @@
 by auto
 
 
-(*
-FIXME: we should have this, as for type int, but many proofs would break.
-It replaces x+-y by x-y.
-declare real_diff_def [symmetric, simp]
-*)
-
 subsubsection{*Density of the Reals*}
 
 lemma real_lbound_gt_zero:
diff -r ba2a7096dd2b -r c137ae7673d3 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Sun May 09 09:39:01 2010 -0700
+++ b/src/HOL/SEQ.thy	Sun May 09 14:21:44 2010 -0700
@@ -1289,7 +1289,7 @@
   hence x0: "0 < x" by simp
   assume x1: "x < 1"
   from x0 x1 have "1 < inverse x"
-    by (rule real_inverse_gt_one)
+    by (rule one_less_inverse)
   hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
     by (rule LIMSEQ_inverse_realpow_zero)
   thus ?thesis by (simp add: power_inverse)
diff -r ba2a7096dd2b -r c137ae7673d3 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun May 09 09:39:01 2010 -0700
+++ b/src/HOL/Transcendental.thy	Sun May 09 14:21:44 2010 -0700
@@ -1089,7 +1089,7 @@
 apply (rule_tac x = 1 and y = y in linorder_cases)
 apply (drule order_less_imp_le [THEN lemma_exp_total])
 apply (rule_tac [2] x = 0 in exI)
-apply (frule_tac [3] real_inverse_gt_one)
+apply (frule_tac [3] one_less_inverse)
 apply (drule_tac [4] order_less_imp_le [THEN lemma_exp_total], auto)
 apply (rule_tac x = "-x" in exI)
 apply (simp add: exp_minus)