--- a/src/HOL/Hyperreal/Transcendental.ML Sat Dec 06 07:52:17 2003 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML Sun Dec 07 16:30:06 2003 +0100
@@ -1732,7 +1732,9 @@
Goal "0 < pi";
by (multr_by_tac "inverse 2" 1);
-by Auto_tac;
+by (Simp_tac 1);
+by (cut_facts_tac [pi_half_gt_zero] 1);
+by (full_simp_tac (HOL_ss addsimps [thm"mult_left_zero", real_divide_def]) 1);
qed "pi_gt_zero";
Addsimps [pi_gt_zero];
Addsimps [(pi_gt_zero RS real_not_refl2) RS not_sym];
@@ -1842,8 +1844,9 @@
Goal "[| 0 < x; x < pi/2 |] ==> 0 < sin x";
by (rtac sin_gt_zero 1);
-by (rtac real_less_trans 2 THEN assume_tac 2);
-by Auto_tac;
+by (assume_tac 1);
+by (rtac real_less_trans 1 THEN assume_tac 1);
+by (rtac pi_half_less_two 1);
qed "sin_gt_zero2";
Goal "[| - pi/2 < x; x < 0 |] ==> sin x < 0";
@@ -1854,13 +1857,22 @@
by Auto_tac;
qed "sin_less_zero";
+Goal "pi < 4";
+by (cut_facts_tac [pi_half_less_two] 1);
+by Auto_tac;
+qed "pi_less_4";
+
Goal "[| 0 < x; x < pi/2 |] ==> 0 < cos x";
+by (cut_facts_tac [pi_less_4] 1);
by (cut_inst_tac [("f","cos"),("a","0"),("b","x"),("y","0")] IVT2_objl 1);
by (Step_tac 1);
by (cut_facts_tac [cos_is_zero] 5);
by (Step_tac 5);
by (dres_inst_tac [("x","xa")] spec 5);
by (dres_inst_tac [("x","pi/2")] spec 5);
+by (force_tac (claset(), simpset() addsimps []) 1);
+by (force_tac (claset(), simpset() addsimps []) 1);
+by (force_tac (claset(), simpset() addsimps []) 1);
by (auto_tac (claset() addSDs [ pi_half_less_two RS order_less_trans,
CLAIM "~ m <= n ==> n < (m::real)"]
addIs [DERIV_isCont,DERIV_cos],simpset()));
@@ -2323,7 +2335,7 @@
qed "tan_arctan";
Goal "- (pi/2) < arctan y & arctan y < pi/2";
-by (Auto_tac);
+by (asm_full_simp_tac (HOL_ss addsimps [arctan]) 1);
qed "arctan_bounded";
Goal "- (pi/2) < arctan y";
@@ -2331,7 +2343,7 @@
qed "arctan_lbound";
Goal "arctan y < pi/2";
-by (Auto_tac);
+by (asm_full_simp_tac (HOL_ss addsimps [arctan]) 1);
qed "arctan_ubound";
Goalw [arctan_def]
@@ -2842,10 +2854,13 @@
Goal "[| 0 < x * x + y * y; \
\ 1 - cos xa ^ 2 = (y / sqrt (x * x + y * y)) ^ 2 \
\ |] ==> cos xa ^ 2 = (x / sqrt (x * x + y * y)) ^ 2";
-by (auto_tac (claset(),simpset() addsimps [realpow_divide,
- real_sqrt_gt_zero_pow2,realpow_two_eq_mult RS sym]));
+by (auto_tac (claset(),
+ simpset() addsimps [realpow_divide,
+ real_sqrt_gt_zero_pow2,realpow_two_eq_mult RS sym]));
by (rtac (real_add_commute RS subst) 1);
-by (auto_tac (claset() addIs [lemma_divide_rearrange],simpset()));
+by (rtac lemma_divide_rearrange 1);
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
qed "lemma_sin_cos_eq";
Goal "[| x ~= 0; \
@@ -2863,18 +2878,6 @@
delsimps [realpow_Suc]));
qed "sin_x_y_disj";
-(*
-Goal "(x / sqrt (x * x + y * y)) ^ 2 = (x * x) / (x * x + y * y)";
-by Auto_tac;
-val lemma = result();
-Addsimps [lemma];
-
-Goal "(x / sqrt (x * x + y * y)) * (x / sqrt (x * x + y * y)) = \
-\ (x * x) / (x * x + y * y)";
-val lemma_too = result();
-Addsimps [lemma_too];
-*)
-
Goal "y ~= 0 ==> x / sqrt (x * x + y * y) ~= -(1::real)";
by Auto_tac;
by (dres_inst_tac [("f","%x. x ^ 2")] arg_cong 1);
--- a/src/HOL/Integ/Bin.thy Sat Dec 06 07:52:17 2003 +0100
+++ b/src/HOL/Integ/Bin.thy Sun Dec 07 16:30:06 2003 +0100
@@ -242,6 +242,9 @@
declare zero_le_divide_iff [of "number_of w", standard, simp]
declare divide_le_0_iff [of "number_of w", standard, simp]
+(*Replaces "inverse #nn" by 1/#nn *)
+declare inverse_eq_divide [of "number_of w", standard, simp]
+
text{*These laws simplify inequalities, moving unary minus from a term
into the literal.*}
declare less_minus_iff [of "number_of v", standard, simp]
--- a/src/HOL/Real/RealArith0.ML Sat Dec 06 07:52:17 2003 +0100
+++ b/src/HOL/Real/RealArith0.ML Sun Dec 07 16:30:06 2003 +0100
@@ -207,290 +207,33 @@
test "a*(b*c)/(y*z) = d*(b::real)*(x*a)/z";
*)
-
-(*** Simplification of inequalities involving literal divisors ***)
-
-Goal "0<z ==> ((x::real) <= y/z) = (x*z <= y)";
-by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
-qed "pos_real_le_divide_eq";
-Addsimps [inst "z" "number_of ?w" pos_real_le_divide_eq];
-
-Goal "z<0 ==> ((x::real) <= y/z) = (y <= x*z)";
-by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
-qed "neg_real_le_divide_eq";
-Addsimps [inst "z" "number_of ?w" neg_real_le_divide_eq];
-
-Goal "0<z ==> (y/z <= (x::real)) = (y <= x*z)";
-by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
-qed "pos_real_divide_le_eq";
-Addsimps [inst "z" "number_of ?w" pos_real_divide_le_eq];
-
-Goal "z<0 ==> (y/z <= (x::real)) = (x*z <= y)";
-by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
-qed "neg_real_divide_le_eq";
-Addsimps [inst "z" "number_of ?w" neg_real_divide_le_eq];
-
-Goal "0<z ==> ((x::real) < y/z) = (x*z < y)";
-by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
-qed "pos_real_less_divide_eq";
-Addsimps [inst "z" "number_of ?w" pos_real_less_divide_eq];
-
-Goal "z<0 ==> ((x::real) < y/z) = (y < x*z)";
-by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
-qed "neg_real_less_divide_eq";
-Addsimps [inst "z" "number_of ?w" neg_real_less_divide_eq];
-
-Goal "0<z ==> (y/z < (x::real)) = (y < x*z)";
-by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
-qed "pos_real_divide_less_eq";
-Addsimps [inst "z" "number_of ?w" pos_real_divide_less_eq];
-
-Goal "z<0 ==> (y/z < (x::real)) = (x*z < y)";
-by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
-qed "neg_real_divide_less_eq";
-Addsimps [inst "z" "number_of ?w" neg_real_divide_less_eq];
-
-Goal "z~=0 ==> ((x::real) = y/z) = (x*z = y)";
-by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_eq_cancel2 1);
-by (Asm_simp_tac 1);
-qed "real_eq_divide_eq";
-Addsimps [inst "z" "number_of ?w" real_eq_divide_eq];
-
-Goal "z~=0 ==> (y/z = (x::real)) = (y = x*z)";
-by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
-by (etac ssubst 1);
-by (stac real_mult_eq_cancel2 1);
-by (Asm_simp_tac 1);
-qed "real_divide_eq_eq";
-Addsimps [inst "z" "number_of ?w" real_divide_eq_eq];
-
-Goal "(m/k = n/k) = (k = 0 | m = (n::real))";
-by (case_tac "k=0" 1);
-by (asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_eq_eq, real_eq_divide_eq,
- real_mult_eq_cancel2]) 1);
-qed "real_divide_eq_cancel2";
-
-Goal "(k/m = k/n) = (k = 0 | m = (n::real))";
-by (case_tac "m=0 | n = 0" 1);
-by (auto_tac (claset(),
- simpset() addsimps [DIVISION_BY_ZERO, real_divide_eq_eq,
- real_eq_divide_eq, real_mult_eq_cancel1]));
-qed "real_divide_eq_cancel1";
-
-Goal "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)";
-by (auto_tac (claset() addIs [real_inverse_less_swap], simpset()));
-qed "real_inverse_less_iff";
-
-Goal "[| 0 < r; 0 < x|] ==> (inverse x <= inverse r) = (r <= (x::real))";
-by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
- real_inverse_less_iff]) 1);
-qed "real_inverse_le_iff";
-
-(** Division by 1, -1 **)
-
-Goal "(x::real)/1 = x";
-by (simp_tac (simpset() addsimps [real_divide_def]) 1);
-qed "real_divide_1";
-Addsimps [real_divide_1];
-
-Goal "x/-1 = -(x::real)";
-by (Simp_tac 1);
-qed "real_divide_minus1";
-Addsimps [real_divide_minus1];
-
-Goal "-1/(x::real) = - (1/x)";
-by (simp_tac (simpset() addsimps [real_divide_def, real_minus_inverse]) 1);
-qed "real_minus1_divide";
-Addsimps [real_minus1_divide];
-
-Goal "[| (0::real) < d1; 0 < d2 |] ==> EX e. 0 < e & e < d1 & e < d2";
-by (res_inst_tac [("x","(min d1 d2)/2")] exI 1);
-by (asm_simp_tac (simpset() addsimps [min_def]) 1);
-qed "real_lbound_gt_zero";
+val real_add_minus_iff = thm"real_add_minus_iff";
+val real_add_eq_0_iff = thm"real_add_eq_0_iff";
+val real_add_less_0_iff = thm"real_add_less_0_iff";
+val real_0_less_add_iff = thm"real_0_less_add_iff";
+val real_add_le_0_iff = thm"real_add_le_0_iff";
+val real_0_le_add_iff = thm"real_0_le_add_iff";
+val real_0_less_diff_iff = thm"real_0_less_diff_iff";
+val real_0_le_diff_iff = thm"real_0_le_diff_iff";
+val real_divide_eq_cancel2 = thm"real_divide_eq_cancel2";
+val real_divide_eq_cancel1 = thm"real_divide_eq_cancel1";
+val real_inverse_less_iff = thm"real_inverse_less_iff";
+val real_inverse_le_iff = thm"real_inverse_le_iff";
+val real_divide_1 = thm"real_divide_1";
+val real_divide_minus1 = thm"real_divide_minus1";
+val real_minus1_divide = thm"real_minus1_divide";
+val real_lbound_gt_zero = thm"real_lbound_gt_zero";
+val real_less_half_sum = thm"real_less_half_sum";
+val real_gt_half_sum = thm"real_gt_half_sum";
+val real_dense = thm"real_dense";
-Goal "(inverse x = inverse y) = (x = (y::real))";
-by (case_tac "x=0 | y=0" 1);
-by (auto_tac (claset(),
- simpset() addsimps [real_inverse_eq_divide,
- DIVISION_BY_ZERO]));
-by (dres_inst_tac [("f","%u. x*y*u")] arg_cong 1);
-by (Asm_full_simp_tac 1);
-qed "real_inverse_eq_iff";
-Addsimps [real_inverse_eq_iff];
-
-Goal "(z/x = z/y) = (z = 0 | x = (y::real))";
-by (case_tac "x=0 | y=0" 1);
-by (auto_tac (claset(),
- simpset() addsimps [DIVISION_BY_ZERO]));
-by (dres_inst_tac [("f","%u. x*y*u")] arg_cong 1);
-by Auto_tac;
-qed "real_divide_eq_iff";
-Addsimps [real_divide_eq_iff];
-
-
-(*** General rewrites to improve automation, like those for type "int" ***)
-
-(** The next several equations can make the simplifier loop! **)
-
-Goal "(x < - y) = (y < - (x::real))";
-by Auto_tac;
-qed "real_less_minus";
-
-Goal "(- x < y) = (- y < (x::real))";
-by Auto_tac;
-qed "real_minus_less";
-
-Goal "(x <= - y) = (y <= - (x::real))";
-by Auto_tac;
-qed "real_le_minus";
-
-Goal "(- x <= y) = (- y <= (x::real))";
-by Auto_tac;
-qed "real_minus_le";
-
-Goal "(x = - y) = (y = - (x::real))";
-by Auto_tac;
-qed "real_equation_minus";
-
-Goal "(- x = y) = (- (y::real) = x)";
-by Auto_tac;
-qed "real_minus_equation";
-
-
-Goal "(x + - a = (0::real)) = (x=a)";
-by (arith_tac 1);
-qed "real_add_minus_iff";
-Addsimps [real_add_minus_iff];
-
-Goal "(-b = -a) = (b = (a::real))";
-by (arith_tac 1);
-qed "real_minus_eq_cancel";
-Addsimps [real_minus_eq_cancel];
-
-
-(*Distributive laws for literals*)
-Addsimps (map (inst "w" "number_of ?v")
- [real_add_mult_distrib, real_add_mult_distrib2,
- real_diff_mult_distrib, real_diff_mult_distrib2]);
-
-Addsimps (map (inst "x" "number_of ?v")
- [real_less_minus, real_le_minus, real_equation_minus]);
-Addsimps (map (inst "y" "number_of ?v")
- [real_minus_less, real_minus_le, real_minus_equation]);
-
-(*Equations and inequations involving 1*)
-Addsimps (map (simplify (simpset()) o inst "x" "1")
- [real_less_minus, real_le_minus, real_equation_minus]);
-Addsimps (map (simplify (simpset()) o inst "y" "1")
- [real_minus_less, real_minus_le, real_minus_equation]);
-
-(*** Simprules combining x+y and 0 ***)
-
-Goal "(x+y = (0::real)) = (y = -x)";
-by Auto_tac;
-qed "real_add_eq_0_iff";
-AddIffs [real_add_eq_0_iff];
-
-Goal "(x+y < (0::real)) = (y < -x)";
-by Auto_tac;
-qed "real_add_less_0_iff";
-AddIffs [real_add_less_0_iff];
-
-Goal "((0::real) < x+y) = (-x < y)";
-by Auto_tac;
-qed "real_0_less_add_iff";
-AddIffs [real_0_less_add_iff];
-
-Goal "(x+y <= (0::real)) = (y <= -x)";
-by Auto_tac;
-qed "real_add_le_0_iff";
-AddIffs [real_add_le_0_iff];
-
-Goal "((0::real) <= x+y) = (-x <= y)";
-by Auto_tac;
-qed "real_0_le_add_iff";
-AddIffs [real_0_le_add_iff];
-
-
-(** Simprules combining x-y and 0; see also real_less_iff_diff_less_0, etc.,
- in RealBin
-**)
-
-Goal "((0::real) < x-y) = (y < x)";
-by Auto_tac;
-qed "real_0_less_diff_iff";
-AddIffs [real_0_less_diff_iff];
-
-Goal "((0::real) <= x-y) = (y <= x)";
-by Auto_tac;
-qed "real_0_le_diff_iff";
-AddIffs [real_0_le_diff_iff];
-
-(*
-FIXME: we should have this, as for type int, but many proofs would break.
-It replaces x+-y by x-y.
-Addsimps [symmetric real_diff_def];
-*)
-
-Goal "-(x-y) = y - (x::real)";
-by (arith_tac 1);
-qed "real_minus_diff_eq";
-Addsimps [real_minus_diff_eq];
-
-
-(*** Density of the Reals ***)
-
-Goal "x < y ==> x < (x+y) / (2::real)";
-by Auto_tac;
-qed "real_less_half_sum";
-
-Goal "x < y ==> (x+y)/(2::real) < y";
-by Auto_tac;
-qed "real_gt_half_sum";
-
-Goal "x < y ==> EX r::real. x < r & r < y";
-by (blast_tac (claset() addSIs [real_less_half_sum, real_gt_half_sum]) 1);
-qed "real_dense";
-
-
-(*Replaces "inverse #nn" by 1/#nn *)
-Addsimps [inst "x" "number_of ?w" real_inverse_eq_divide];
-
-
+val pos_real_less_divide_eq = thm"pos_real_less_divide_eq";
+val neg_real_less_divide_eq = thm"neg_real_less_divide_eq";
+val pos_real_divide_less_eq = thm"pos_real_divide_less_eq";
+val neg_real_divide_less_eq = thm"neg_real_divide_less_eq";
+val pos_real_le_divide_eq = thm"pos_real_le_divide_eq";
+val neg_real_le_divide_eq = thm"neg_real_le_divide_eq";
+val pos_real_divide_le_eq = thm"pos_real_divide_le_eq";
+val neg_real_divide_le_eq = thm"neg_real_divide_le_eq";
+val real_eq_divide_eq = thm"real_eq_divide_eq";
+val real_divide_eq_eq = thm"real_divide_eq_eq";
--- a/src/HOL/Real/RealArith0.thy Sat Dec 06 07:52:17 2003 +0100
+++ b/src/HOL/Real/RealArith0.thy Sun Dec 07 16:30:06 2003 +0100
@@ -1,6 +1,8 @@
theory RealArith0 = RealBin
files "real_arith0.ML":
+(*FIXME: move results further down to Ring_and_Field*)
+
setup real_arith_setup
subsection{*Facts that need the Arithmetic Decision Procedure*}
@@ -54,6 +56,215 @@
"(k*m) / (k*n) = (if k = (0::real) then 0 else m/n)"
by (rule Ring_and_Field.mult_divide_cancel_eq_if)
+subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
+
+lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)"
+by arith
+
+lemma real_add_eq_0_iff [iff]: "(x+y = (0::real)) = (y = -x)"
+by auto
+
+lemma real_add_less_0_iff [iff]: "(x+y < (0::real)) = (y < -x)"
+by auto
+
+lemma real_0_less_add_iff [iff]: "((0::real) < x+y) = (-x < y)"
+by auto
+
+lemma real_add_le_0_iff [iff]: "(x+y \<le> (0::real)) = (y \<le> -x)"
+by auto
+
+lemma real_0_le_add_iff [iff]: "((0::real) \<le> x+y) = (-x \<le> y)"
+by auto
+
+
+(** Simprules combining x-y and 0; see also real_less_iff_diff_less_0, etc.,
+ in RealBin
+**)
+
+lemma real_0_less_diff_iff [iff]: "((0::real) < x-y) = (y < x)"
+by auto
+
+lemma real_0_le_diff_iff [iff]: "((0::real) \<le> x-y) = (y \<le> x)"
+by auto
+
+(*
+FIXME: we should have this, as for type int, but many proofs would break.
+It replaces x+-y by x-y.
+Addsimps [symmetric real_diff_def]
+*)
+
+
+(*FIXME: move most of these to Ring_and_Field*)
+
+subsection{*Simplification of Inequalities Involving Literal Divisors*}
+
+lemma pos_real_le_divide_eq: "0<z ==> ((x::real) \<le> y/z) = (x*z \<le> y)"
+apply (subgoal_tac " (x*z \<le> y) = (x*z \<le> (y/z) *z) ")
+ prefer 2 apply (simp add: real_divide_def real_mult_assoc)
+apply (erule ssubst)
+apply (subst real_mult_le_cancel2, simp)
+done
+
+lemma neg_real_le_divide_eq: "z<0 ==> ((x::real) \<le> y/z) = (y \<le> x*z)"
+apply (subgoal_tac " (y \<le> x*z) = ((y/z) *z \<le> x*z) ")
+ prefer 2 apply (simp add: real_divide_def real_mult_assoc)
+apply (erule ssubst)
+apply (subst real_mult_le_cancel2, simp)
+done
+
+lemma real_le_divide_eq:
+ "((x::real) \<le> y/z) = (if 0<z then x*z \<le> y
+ else if z<0 then y \<le> x*z
+ else x\<le>0)"
+apply (case_tac "z=0", simp)
+apply (simp add: pos_real_le_divide_eq neg_real_le_divide_eq)
+done
+
+declare real_le_divide_eq [of _ _ "number_of w", standard, simp]
+
+lemma pos_real_divide_le_eq: "0<z ==> (y/z \<le> (x::real)) = (y \<le> x*z)"
+apply (subgoal_tac " (y \<le> x*z) = ((y/z) *z \<le> x*z) ")
+ prefer 2 apply (simp add: real_divide_def real_mult_assoc)
+apply (erule ssubst)
+apply (subst real_mult_le_cancel2, simp)
+done
+
+lemma neg_real_divide_le_eq: "z<0 ==> (y/z \<le> (x::real)) = (x*z \<le> y)"
+apply (subgoal_tac " (x*z \<le> y) = (x*z \<le> (y/z) *z) ")
+ prefer 2 apply (simp add: real_divide_def real_mult_assoc)
+apply (erule ssubst)
+apply (subst real_mult_le_cancel2, simp)
+done
+
+
+lemma real_divide_le_eq:
+ "(y/z \<le> (x::real)) = (if 0<z then y \<le> x*z
+ else if z<0 then x*z \<le> y
+ else 0 \<le> x)"
+apply (case_tac "z=0", simp)
+apply (simp add: pos_real_divide_le_eq neg_real_divide_le_eq)
+done
+
+declare real_divide_le_eq [of _ "number_of w", standard, simp]
+lemma pos_real_less_divide_eq: "0<z ==> ((x::real) < y/z) = (x*z < y)"
+apply (subgoal_tac " (x*z < y) = (x*z < (y/z) *z) ")
+ prefer 2 apply (simp add: real_divide_def real_mult_assoc)
+apply (erule ssubst)
+apply (subst real_mult_less_cancel2, simp)
+done
+
+lemma neg_real_less_divide_eq: "z<0 ==> ((x::real) < y/z) = (y < x*z)"
+apply (subgoal_tac " (y < x*z) = ((y/z) *z < x*z) ")
+ prefer 2 apply (simp add: real_divide_def real_mult_assoc)
+apply (erule ssubst)
+apply (subst real_mult_less_cancel2, simp)
+done
+
+lemma real_less_divide_eq:
+ "((x::real) < y/z) = (if 0<z then x*z < y
+ else if z<0 then y < x*z
+ else x<0)"
+apply (case_tac "z=0", simp)
+apply (simp add: pos_real_less_divide_eq neg_real_less_divide_eq)
+done
+
+declare real_less_divide_eq [of _ _ "number_of w", standard, simp]
+
+lemma pos_real_divide_less_eq: "0<z ==> (y/z < (x::real)) = (y < x*z)"
+apply (subgoal_tac " (y < x*z) = ((y/z) *z < x*z) ")
+ prefer 2 apply (simp add: real_divide_def real_mult_assoc)
+apply (erule ssubst)
+apply (subst real_mult_less_cancel2, simp)
+done
+
+lemma neg_real_divide_less_eq: "z<0 ==> (y/z < (x::real)) = (x*z < y)"
+apply (subgoal_tac " (x*z < y) = (x*z < (y/z) *z) ")
+ prefer 2 apply (simp add: real_divide_def real_mult_assoc)
+apply (erule ssubst)
+apply (subst real_mult_less_cancel2, simp)
+done
+
+lemma real_divide_less_eq:
+ "(y/z < (x::real)) = (if 0<z then y < x*z
+ else if z<0 then x*z < y
+ else 0 < x)"
+apply (case_tac "z=0", simp)
+apply (simp add: pos_real_divide_less_eq neg_real_divide_less_eq)
+done
+
+declare real_divide_less_eq [of _ "number_of w", standard, simp]
+
+lemma nonzero_real_eq_divide_eq: "z\<noteq>0 ==> ((x::real) = y/z) = (x*z = y)"
+apply (subgoal_tac " (x*z = y) = (x*z = (y/z) *z) ")
+ prefer 2 apply (simp add: real_divide_def real_mult_assoc)
+apply (erule ssubst)
+apply (subst real_mult_eq_cancel2, simp)
+done
+
+lemma real_eq_divide_eq:
+ "((x::real) = y/z) = (if z\<noteq>0 then x*z = y else x=0)"
+by (simp add: nonzero_real_eq_divide_eq)
+
+declare real_eq_divide_eq [of _ _ "number_of w", standard, simp]
+
+lemma nonzero_real_divide_eq_eq: "z\<noteq>0 ==> (y/z = (x::real)) = (y = x*z)"
+apply (subgoal_tac " (y = x*z) = ((y/z) *z = x*z) ")
+ prefer 2 apply (simp add: real_divide_def real_mult_assoc)
+apply (erule ssubst)
+apply (subst real_mult_eq_cancel2, simp)
+done
+
+lemma real_divide_eq_eq:
+ "(y/z = (x::real)) = (if z\<noteq>0 then y = x*z else x=0)"
+by (simp add: nonzero_real_divide_eq_eq)
+
+declare real_divide_eq_eq [of _ "number_of w", standard, simp]
+
+lemma real_divide_eq_cancel2: "(m/k = n/k) = (k = 0 | m = (n::real))"
+apply (case_tac "k=0", simp)
+apply (simp add:divide_inverse)
+done
+
+lemma real_divide_eq_cancel1: "(k/m = k/n) = (k = 0 | m = (n::real))"
+by (force simp add: real_divide_eq_eq real_eq_divide_eq)
+
+lemma real_inverse_less_iff:
+ "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)"
+by (rule Ring_and_Field.inverse_less_iff_less)
+
+lemma real_inverse_le_iff:
+ "[| 0 < r; 0 < x|] ==> (inverse x \<le> inverse r) = (r \<le> (x::real))"
+by (rule Ring_and_Field.inverse_le_iff_le)
+
+
+(** Division by 1, -1 **)
+
+lemma real_divide_1: "(x::real)/1 = x"
+by (simp add: real_divide_def)
+
+lemma real_divide_minus1 [simp]: "x/-1 = -(x::real)"
+by simp
+
+lemma real_minus1_divide [simp]: "-1/(x::real) = - (1/x)"
+by (simp add: real_divide_def real_minus_inverse)
+
+lemma real_lbound_gt_zero:
+ "[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2"
+apply (rule_tac x = " (min d1 d2) /2" in exI)
+apply (simp add: min_def)
+done
+
+(*** Density of the Reals ***)
+
+lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)"
+by auto
+
+lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y"
+by auto
+
+lemma real_dense: "x < y ==> \<exists>r::real. x < r & r < y"
+by (blast intro!: real_less_half_sum real_gt_half_sum)
+
end
--- a/src/HOL/Real/RealOrd.thy Sat Dec 06 07:52:17 2003 +0100
+++ b/src/HOL/Real/RealOrd.thy Sun Dec 07 16:30:06 2003 +0100
@@ -360,16 +360,9 @@
lemma real_le_add_right_cancel: "!!(A::real). A + C \<le> B + C ==> A \<le> B"
by (rule Ring_and_Field.add_le_imp_le_right)
- lemma add_le_imp_le_left:
- "c + a \<le> c + b ==> a \<le> (b::'a::ordered_ring)"
- by simp
-
lemma real_le_add_left_cancel: "!!(A::real). C + A \<le> C + B ==> A \<le> B"
by (rule (*Ring_and_Field.*)add_le_imp_le_left)
-lemma real_minus_diff_eq: "- (z - y) = y - (z::real)"
- by (rule Ring_and_Field.minus_diff_eq)
-
lemma real_add_right_cancel_less [simp]: "(v+z < w+z) = (v < (w::real))"
by (rule Ring_and_Field.add_less_cancel_right)
@@ -910,7 +903,6 @@
val real_sum_gt_zero_less = thm"real_sum_gt_zero_less";
val real_less_sum_gt_0_iff = thm"real_less_sum_gt_0_iff";
-val real_minus_diff_eq = thm "real_minus_diff_eq";
val real_gt_zero_preal_Ex = thm "real_gt_zero_preal_Ex";
val real_gt_preal_preal_Ex = thm "real_gt_preal_preal_Ex";
val real_ge_preal_preal_Ex = thm "real_ge_preal_preal_Ex";
--- a/src/HOL/Ring_and_Field.thy Sat Dec 06 07:52:17 2003 +0100
+++ b/src/HOL/Ring_and_Field.thy Sun Dec 07 16:30:06 2003 +0100
@@ -901,6 +901,9 @@
(if c=0 then 0 else a / (b::'a::{field,division_by_zero}))"
by (simp add: mult_divide_cancel_left)
+lemma divide_1 [simp]: "a/1 = (a::'a::field)"
+ by (simp add: divide_inverse [OF not_sym])
+
subsection {* Ordered Fields *}
@@ -1088,5 +1091,4 @@
"(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
by (simp add: divide_inverse_zero field_mult_eq_0_iff)
-
end