--- 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)) = \
--- 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);
--- 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*)
--- 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";
--- 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 < (0::real) |] ==> j*k < i*k"
- by (rule Ring_and_Field.mult_strict_right_mono_neg)
-
-lemma real_mult_less_mono2_neg: "[| i<j; k < (0::real) |] ==> 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<n) | (k < 0 & n<m))"
by (rule Ring_and_Field.mult_less_cancel_right)
@@ -109,15 +48,11 @@
by (rule Ring_and_Field.mult_cancel_right)
lemma real_mult_div_cancel1: "!!k::real. k~=0 ==> (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)
--- 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
--- 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 \<noteq> 0 ==> inverse (a::'a::field) = 1/a"
+by (simp add: divide_inverse)
+
lemma divide_self [simp]: "a \<noteq> 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\<noteq>0" and [simp]: "c\<noteq>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\<noteq>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 \<noteq> 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 \<noteq> 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 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"
+by (simp add: linorder_not_less [symmetric])
+
+lemma inverse_nonpositive_iff_nonpositive [simp]:
+ "(inverse a \<le> 0) = (a \<le> (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 \<le> inverse b) = (b \<le> (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}) \<le> a/b) =
+ (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
+by (simp add: divide_inverse_zero zero_le_mult_iff)
+
+lemma divide_le_0_iff:
+ "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) = (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> 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