# HG changeset patch # User paulson # Date 1070811006 -3600 # Node ID f1abe67c448ab51c91677c02525b397489068a0a # Parent 516358ca7b42e798b3a3df7d077e839fa84240d8 re-organisation of Real/RealArith0.ML; more `Isar scripts diff -r 516358ca7b42 -r f1abe67c448a src/HOL/Hyperreal/Transcendental.ML --- 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); diff -r 516358ca7b42 -r f1abe67c448a src/HOL/Integ/Bin.thy --- 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] diff -r 516358ca7b42 -r f1abe67c448a src/HOL/Real/RealArith0.ML --- 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 ((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 (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 ((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 (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"; diff -r 516358ca7b42 -r f1abe67c448a src/HOL/Real/RealArith0.thy --- 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 \ (0::real)) = (y \ -x)" +by auto + +lemma real_0_le_add_iff [iff]: "((0::real) \ x+y) = (-x \ 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) \ x-y) = (y \ 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 ((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_le_cancel2, simp) +done + +lemma neg_real_le_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_le_cancel2, simp) +done + +lemma real_le_divide_eq: + "((x::real) \ y/z) = (if 0 y + else if z<0 then y \ x*z + else x\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 (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_le_cancel2, simp) +done + +lemma neg_real_divide_le_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_le_cancel2, simp) +done + + +lemma real_divide_le_eq: + "(y/z \ (x::real)) = (if 0 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_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 ((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 (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 00 ==> ((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\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\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\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 \ inverse r) = (r \ (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 |] ==> \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 ==> \r::real. x < r & r < y" +by (blast intro!: real_less_half_sum real_gt_half_sum) + end diff -r 516358ca7b42 -r f1abe67c448a src/HOL/Real/RealOrd.thy --- 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 \ B + C ==> A \ B" by (rule Ring_and_Field.add_le_imp_le_right) - lemma add_le_imp_le_left: - "c + a \ c + b ==> a \ (b::'a::ordered_ring)" - by simp - lemma real_le_add_left_cancel: "!!(A::real). C + A \ C + B ==> A \ 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"; diff -r 516358ca7b42 -r f1abe67c448a src/HOL/Ring_and_Field.thy --- 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