# HG changeset patch # User paulson # Date 1070644259 -3600 # Node ID ad66687ece6e37d2c598a36af3362533c92b0316 # Parent 950c121390160d0429a81f66896bf52c4f967e53 more field division lemmas transferred from Real to Ring_and_Field diff -r 950c12139016 -r ad66687ece6e src/HOL/Hyperreal/Integration.ML --- a/src/HOL/Hyperreal/Integration.ML Fri Dec 05 12:58:18 2003 +0100 +++ b/src/HOL/Hyperreal/Integration.ML Fri Dec 05 18:10:59 2003 +0100 @@ -539,7 +539,7 @@ by (dtac spec 1 THEN Auto_tac); by (REPEAT(dtac spec 1) THEN Auto_tac); by (dres_inst_tac [("e","ea/(b - a)")] lemma_straddle 1); -by (auto_tac (claset(),simpset() addsimps [real_0_less_divide_iff])); +by (auto_tac (claset(),simpset() addsimps [thm"Ring_and_Field.zero_less_divide_iff"])); by (rtac exI 1); by (auto_tac (claset(),simpset() addsimps [tpart_def,rsum_def])); by (subgoal_tac "sumr 0 (psize D) (%n. f(D(Suc n)) - f(D n)) = \ diff -r 950c12139016 -r ad66687ece6e src/HOL/Hyperreal/Transcendental.ML --- a/src/HOL/Hyperreal/Transcendental.ML Fri Dec 05 12:58:18 2003 +0100 +++ b/src/HOL/Hyperreal/Transcendental.ML Fri Dec 05 18:10:59 2003 +0100 @@ -3035,7 +3035,8 @@ by (res_inst_tac [("y","u/sqrt 2")] order_le_less_trans 1); by (etac lemma_real_divide_sqrt_less 2); by (res_inst_tac [("n","1")] realpow_increasing 1); -by (auto_tac (claset(),simpset() addsimps [real_0_le_divide_iff,realpow_divide, +by (auto_tac (claset(), + simpset() addsimps [real_0_le_divide_iff,realpow_divide, real_sqrt_gt_zero_pow2,two_eq_Suc_Suc RS sym] delsimps [realpow_Suc])); by (res_inst_tac [("t","u ^ 2")] (real_sum_of_halves RS subst) 1); by (rtac real_add_le_mono 1); diff -r 950c12139016 -r ad66687ece6e src/HOL/Integ/Bin.thy --- a/src/HOL/Integ/Bin.thy Fri Dec 05 12:58:18 2003 +0100 +++ b/src/HOL/Integ/Bin.thy Fri Dec 05 18:10:59 2003 +0100 @@ -236,24 +236,30 @@ declare left_diff_distrib [of _ _ "number_of v", standard, simp] declare right_diff_distrib [of "number_of v", standard, simp] +text{*These are actually for fields, like real: but where else to put them?*} +declare zero_less_divide_iff [of "number_of w", standard, simp] +declare divide_less_0_iff [of "number_of w", standard, simp] +declare zero_le_divide_iff [of "number_of w", standard, simp] +declare divide_le_0_iff [of "number_of w", standard, simp] + text{*These laws simplify inequalities, moving unary minus from a term into the literal.*} -declare zless_zminus [of "number_of v", standard, simp] -declare zle_zminus [of "number_of v", standard, simp] -declare equation_zminus [of "number_of v", standard, simp] +declare less_minus_iff [of "number_of v", standard, simp] +declare le_minus_iff [of "number_of v", standard, simp] +declare equation_minus_iff [of "number_of v", standard, simp] -declare zminus_zless [of _ "number_of v", standard, simp] -declare zminus_zle [of _ "number_of v", standard, simp] -declare zminus_equation [of _ "number_of v", standard, simp] +declare minus_less_iff [of _ "number_of v", standard, simp] +declare minus_le_iff [of _ "number_of v", standard, simp] +declare minus_equation_iff [of _ "number_of v", standard, simp] text{*These simplify inequalities where one side is the constant 1.*} -declare zless_zminus [of 1, simplified, simp] -declare zle_zminus [of 1, simplified, simp] +declare less_minus_iff [of 1, simplified, simp] +declare le_minus_iff [of 1, simplified, simp] declare equation_zminus [of 1, simplified, simp] -declare zminus_zless [of _ 1, simplified, simp] -declare zminus_zle [of _ 1, simplified, simp] -declare zminus_equation [of _ 1, simplified, simp] +declare minus_less_iff [of _ 1, simplified, simp] +declare minus_le_iff [of _ 1, simplified, simp] +declare minus_equation_iff [of _ 1, simplified, simp] (*Moving negation out of products*) diff -r 950c12139016 -r ad66687ece6e src/HOL/Real/RealArith0.ML --- a/src/HOL/Real/RealArith0.ML Fri Dec 05 12:58:18 2003 +0100 +++ b/src/HOL/Real/RealArith0.ML Fri Dec 05 18:10:59 2003 +0100 @@ -7,24 +7,8 @@ *) val real_diff_minus_eq = thm"real_diff_minus_eq"; -val real_0_divide = thm"real_0_divide"; -val real_0_less_inverse_iff = thm"real_0_less_inverse_iff"; -val real_inverse_less_0_iff = thm"real_inverse_less_0_iff"; -val real_0_le_inverse_iff = thm"real_0_le_inverse_iff"; -val real_inverse_le_0_iff = thm"real_inverse_le_0_iff"; val real_inverse_eq_divide = thm"real_inverse_eq_divide"; -val real_0_less_divide_iff = thm"real_0_less_divide_iff"; -val real_divide_less_0_iff = thm"real_divide_less_0_iff"; val real_0_le_divide_iff = thm"real_0_le_divide_iff"; -val real_divide_le_0_iff = thm"real_divide_le_0_iff"; -val real_inverse_zero_iff = thm"real_inverse_zero_iff"; -val real_divide_eq_0_iff = thm"real_divide_eq_0_iff"; -val real_divide_self_eq = thm"real_divide_self_eq"; -val real_minus_less_minus = thm"real_minus_less_minus"; -val real_mult_less_mono1_neg = thm"real_mult_less_mono1_neg"; -val real_mult_less_mono2_neg = thm"real_mult_less_mono2_neg"; -val real_mult_le_mono1_neg = thm"real_mult_le_mono1_neg"; -val real_mult_le_mono2_neg = thm"real_mult_le_mono2_neg"; val real_mult_less_cancel2 = thm"real_mult_less_cancel2"; val real_mult_le_cancel2 = thm"real_mult_le_cancel2"; val real_mult_less_cancel1 = thm"real_mult_less_cancel1"; diff -r 950c12139016 -r ad66687ece6e src/HOL/Real/RealArith0.thy --- a/src/HOL/Real/RealArith0.thy Fri Dec 05 12:58:18 2003 +0100 +++ b/src/HOL/Real/RealArith0.thy Fri Dec 05 18:10:59 2003 +0100 @@ -3,7 +3,7 @@ setup real_arith_setup -subsection{*Assorted facts that need binary literals and the arithmetic decision procedure*} +subsection{*Facts that need the Arithmetic Decision Procedure*} lemma real_diff_minus_eq: "x - - y = x + (y::real)" by simp @@ -11,59 +11,13 @@ (** Division and inverse **) -lemma real_0_divide: "0/x = (0::real)" -by (simp add: real_divide_def) -declare real_0_divide [simp] - -lemma real_0_less_inverse_iff: "((0::real) < inverse x) = (0 < x)" -apply (case_tac "x=0") -apply (auto dest: real_inverse_less_0 simp add: linorder_neq_iff real_inverse_gt_0) -done -declare real_0_less_inverse_iff [simp] - -lemma real_inverse_less_0_iff: "(inverse x < (0::real)) = (x < 0)" -apply (case_tac "x=0") -apply (auto dest: real_inverse_less_0 simp add: linorder_neq_iff real_inverse_gt_0) -done -declare real_inverse_less_0_iff [simp] - -lemma real_0_le_inverse_iff: "((0::real) <= inverse x) = (0 <= x)" -by (simp add: linorder_not_less [symmetric]) -declare real_0_le_inverse_iff [simp] - -lemma real_inverse_le_0_iff: "(inverse x <= (0::real)) = (x <= 0)" -by (simp add: linorder_not_less [symmetric]) -declare real_inverse_le_0_iff [simp] - lemma real_inverse_eq_divide: "inverse (x::real) = 1/x" -by (simp add: real_divide_def) + by (rule Ring_and_Field.inverse_eq_divide) -lemma real_0_less_divide_iff: "((0::real) < x/y) = (0 < x & 0 < y | x < 0 & y < 0)" -by (simp add: real_divide_def real_0_less_mult_iff) -declare real_0_less_divide_iff [of "number_of w", standard, simp] - -lemma real_divide_less_0_iff: "(x/y < (0::real)) = (0 < x & y < 0 | x < 0 & 0 < y)" -by (simp add: real_divide_def real_mult_less_0_iff) -declare real_divide_less_0_iff [of "number_of w", standard, simp] - -lemma real_0_le_divide_iff: "((0::real) <= x/y) = ((x <= 0 | 0 <= y) & (0 <= x | y <= 0))" +text{*Needed in this non-standard form by Hyperreal/Transcendental*} +lemma real_0_le_divide_iff: + "((0::real) <= x/y) = ((x <= 0 | 0 <= y) & (0 <= x | y <= 0))" by (simp add: real_divide_def real_0_le_mult_iff, auto) -declare real_0_le_divide_iff [of "number_of w", standard, simp] - -lemma real_divide_le_0_iff: "(x/y <= (0::real)) = ((x <= 0 | y <= 0) & (0 <= x | 0 <= y))" -by (simp add: real_divide_def real_mult_le_0_iff, auto) -declare real_divide_le_0_iff [of "number_of w", standard, simp] - -lemma real_inverse_zero_iff: "(inverse(x::real) = 0) = (x = 0)" - by (rule Ring_and_Field.inverse_nonzero_iff_nonzero) - -lemma real_divide_eq_0_iff: "(x/y = 0) = (x=0 | y=(0::real))" -by (auto simp add: real_divide_def) -declare real_divide_eq_0_iff [simp] - -lemma real_divide_self_eq: "h ~= (0::real) ==> h/h = 1" - by (rule Ring_and_Field.divide_self) - (**** Factor cancellation theorems for "real" ****) @@ -71,21 +25,6 @@ (** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =, but not (yet?) for k*m < n*k. **) -lemma real_minus_less_minus: "(-y < -x) = ((x::real) < y)" - by (rule Ring_and_Field.neg_less_iff_less) - -lemma real_mult_less_mono1_neg: "[| i j*k < i*k" - by (rule Ring_and_Field.mult_strict_right_mono_neg) - -lemma real_mult_less_mono2_neg: "[| i k*j < k*i" - by (rule Ring_and_Field.mult_strict_left_mono_neg) - -lemma real_mult_le_mono1_neg: "[| i <= j; k <= (0::real) |] ==> j*k <= i*k" - by (rule Ring_and_Field.mult_right_mono_neg) - -lemma real_mult_le_mono2_neg: "[| i <= j; k <= (0::real) |] ==> k*j <= k*i" - by (rule Ring_and_Field.mult_left_mono_neg) - lemma real_mult_less_cancel2: "(m*k < n*k) = (((0::real) < k & m (k*m) / (k*n) = (m/n)" -apply (simp add: real_divide_def real_inverse_distrib) -apply (subgoal_tac "k * m * (inverse k * inverse n) = (k * inverse k) * (m * inverse n) ") -apply simp -apply (simp only: mult_ac) -done + by (rule Ring_and_Field.mult_divide_cancel_left) -(*For ExtractCommonTerm*) -lemma real_mult_div_cancel_disj: "(k*m) / (k*n) = (if k = (0::real) then 0 else m/n)" -by (simp add: real_mult_div_cancel1) +lemma real_mult_div_cancel_disj: + "(k*m) / (k*n) = (if k = (0::real) then 0 else m/n)" + by (rule Ring_and_Field.mult_divide_cancel_eq_if) diff -r 950c12139016 -r ad66687ece6e src/HOL/Real/RealOrd.thy --- a/src/HOL/Real/RealOrd.thy Fri Dec 05 12:58:18 2003 +0100 +++ b/src/HOL/Real/RealOrd.thy Fri Dec 05 18:10:59 2003 +0100 @@ -565,10 +565,10 @@ subsection{*Inverse and Division*} lemma real_inverse_gt_0: "0 < x ==> 0 < inverse (x::real)" - by (rule Ring_and_Field.inverse_gt_0) + by (rule Ring_and_Field.positive_imp_inverse_positive) lemma real_inverse_less_0: "x < 0 ==> inverse (x::real) < 0" - by (rule Ring_and_Field.inverse_less_0) + by (rule Ring_and_Field.negative_imp_inverse_negative) lemma real_mult_less_cancel1: "[| (0::real) < z; x * z < y * z |] ==> x < y" by (force simp add: Ring_and_Field.mult_less_cancel_right diff -r 950c12139016 -r ad66687ece6e src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Fri Dec 05 12:58:18 2003 +0100 +++ b/src/HOL/Ring_and_Field.thy Fri Dec 05 18:10:59 2003 +0100 @@ -187,6 +187,9 @@ } qed +lemma nonzero_inverse_eq_divide: "a \ 0 ==> inverse (a::'a::field) = 1/a" +by (simp add: divide_inverse) + lemma divide_self [simp]: "a \ 0 ==> a / (a::'a::field) = 1" by (simp add: divide_inverse) @@ -534,6 +537,8 @@ apply (blast dest: zero_less_mult_pos) done +text{*A field has no "zero divisors", so this theorem should hold without the + assumption of an ordering. See @{text field_mult_eq_0_iff} below.*} lemma mult_eq_0_iff [simp]: "(a*b = (0::'a::ordered_ring)) = (a = 0 | b = 0)" apply (case_tac "a < 0") apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff) @@ -685,6 +690,17 @@ subsection {* Fields *} +lemma divide_inverse_zero: "a/b = a * inverse(b::'a::{field,division_by_zero})" +apply (case_tac "b = 0") +apply (simp_all add: divide_inverse) +done + +lemma divide_zero_left [simp]: "0/a = (0::'a::{field,division_by_zero})" +by (simp add: divide_inverse_zero) + +lemma inverse_eq_divide: "inverse (a::'a::{field,division_by_zero}) = 1/a" +by (simp add: divide_inverse_zero) + text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement of an ordering.*} lemma field_mult_eq_0_iff: "(a*b = (0::'a::field)) = (a = 0 | b = 0)" @@ -735,6 +751,9 @@ thus False by (simp add: eq_commute) qed + +subsection{*Basic Properties of @{term inverse}*} + lemma inverse_zero_imp_zero: "inverse a = 0 ==> a = (0::'a::field)" apply (rule ccontr) apply (blast dest: nonzero_imp_inverse_nonzero) @@ -855,10 +874,37 @@ apply (simp add: mult_assoc [symmetric] add_commute) done +lemma nonzero_mult_divide_cancel_left: + assumes [simp]: "b\0" and [simp]: "c\0" + shows "(c*a)/(c*b) = a/(b::'a::field)" +proof - + have "(c*a)/(c*b) = c * a * (inverse b * inverse c)" + by (simp add: field_mult_eq_0_iff divide_inverse + nonzero_inverse_mult_distrib) + also have "... = a * inverse b * (inverse c * c)" + by (simp only: mult_ac) + also have "... = a * inverse b" + by simp + finally show ?thesis + by (simp add: divide_inverse) +qed + +lemma mult_divide_cancel_left: + "c\0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})" +apply (case_tac "b = 0") +apply (simp_all add: nonzero_mult_divide_cancel_left) +done + +(*For ExtractCommonTerm*) +lemma mult_divide_cancel_eq_if: + "(c*a) / (c*b) = + (if c=0 then 0 else a / (b::'a::{field,division_by_zero}))" + by (simp add: mult_divide_cancel_left) + subsection {* Ordered Fields *} -lemma inverse_gt_0: +lemma positive_imp_inverse_positive: assumes a_gt_0: "0 < a" shows "0 < inverse (a::'a::ordered_field)" proof - have "0 < a * inverse a" @@ -867,9 +913,9 @@ by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff) qed -lemma inverse_less_0: +lemma negative_imp_inverse_negative: "a < 0 ==> inverse a < (0::'a::ordered_field)" - by (insert inverse_gt_0 [of "-a"], + by (insert positive_imp_inverse_positive [of "-a"], simp add: nonzero_inverse_minus_eq order_less_imp_not_eq) lemma inverse_le_imp_le: @@ -890,6 +936,51 @@ by (simp add: mult_assoc apos bpos order_less_imp_not_eq2) qed +lemma inverse_positive_imp_positive: + assumes inv_gt_0: "0 < inverse a" + and [simp]: "a \ 0" + shows "0 < (a::'a::ordered_field)" + proof - + have "0 < inverse (inverse a)" + by (rule positive_imp_inverse_positive) + thus "0 < a" + by (simp add: nonzero_inverse_inverse_eq) + qed + +lemma inverse_positive_iff_positive [simp]: + "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))" +apply (case_tac "a = 0", simp) +apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive) +done + +lemma inverse_negative_imp_negative: + assumes inv_less_0: "inverse a < 0" + and [simp]: "a \ 0" + shows "a < (0::'a::ordered_field)" + proof - + have "inverse (inverse a) < 0" + by (rule negative_imp_inverse_negative) + thus "a < 0" + by (simp add: nonzero_inverse_inverse_eq) + qed + +lemma inverse_negative_iff_negative [simp]: + "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))" +apply (case_tac "a = 0", simp) +apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative) +done + +lemma inverse_nonnegative_iff_nonnegative [simp]: + "(0 \ inverse a) = (0 \ (a::'a::{ordered_field,division_by_zero}))" +by (simp add: linorder_not_less [symmetric]) + +lemma inverse_nonpositive_iff_nonpositive [simp]: + "(inverse a \ 0) = (a \ (0::'a::{ordered_field,division_by_zero}))" +by (simp add: linorder_not_less [symmetric]) + + +subsection{*Anti-Monotonicity of @{term inverse}*} + lemma less_imp_inverse_less: assumes less: "a < b" and apos: "0 < a" @@ -972,4 +1063,30 @@ ==> (inverse a \ inverse b) = (b \ (a::'a::ordered_field))" by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) + +subsection{*Division and Signs*} + +lemma zero_less_divide_iff: + "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)" +by (simp add: divide_inverse_zero zero_less_mult_iff) + +lemma divide_less_0_iff: + "(a/b < (0::'a::{ordered_field,division_by_zero})) = + (0 < a & b < 0 | a < 0 & 0 < b)" +by (simp add: divide_inverse_zero mult_less_0_iff) + +lemma zero_le_divide_iff: + "((0::'a::{ordered_field,division_by_zero}) \ a/b) = + (0 \ a & 0 \ b | a \ 0 & b \ 0)" +by (simp add: divide_inverse_zero zero_le_mult_iff) + +lemma divide_le_0_iff: + "(a/b \ (0::'a::{ordered_field,division_by_zero})) = (0 \ a & b \ 0 | a \ 0 & 0 \ b)" +by (simp add: divide_inverse_zero mult_le_0_iff) + +lemma divide_eq_0_iff [simp]: + "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))" +by (simp add: divide_inverse_zero field_mult_eq_0_iff) + + end