# HG changeset patch # User paulson # Date 1071304432 -3600 # Node ID f4d806fd72ced144042d764b310159118845c2f1 # Parent 22542982bffd1e0ca0d74786fa2f5bc7bb03c06c absolute value theorems moved to HOL/Ring_and_Field diff -r 22542982bffd -r f4d806fd72ce src/HOL/Hyperreal/HyperNat.ML --- a/src/HOL/Hyperreal/HyperNat.ML Fri Dec 12 15:05:18 2003 +0100 +++ b/src/HOL/Hyperreal/HyperNat.ML Sat Dec 13 09:33:52 2003 +0100 @@ -1317,8 +1317,6 @@ by Auto_tac; by (dres_inst_tac [("x","m + 1")] spec 1); by (Ultra_tac 1); -by (subgoal_tac "abs(inverse (real (Y x))) = inverse(real (Y x))" 1); -by (auto_tac (claset() addSIs [abs_eqI2],simpset())); qed "HNatInfinite_inverse_Infinitesimal"; Addsimps [HNatInfinite_inverse_Infinitesimal]; diff -r 22542982bffd -r f4d806fd72ce src/HOL/Hyperreal/Integration.ML --- a/src/HOL/Hyperreal/Integration.ML Fri Dec 12 15:05:18 2003 +0100 +++ b/src/HOL/Hyperreal/Integration.ML Sat Dec 13 09:33:52 2003 +0100 @@ -398,7 +398,7 @@ simpset())); by (auto_tac (claset(),simpset() addsimps [rsum_def,Integral_def, sumr_mult RS sym,real_mult_assoc])); -by (res_inst_tac [("x2","c")] ((abs_ge_zero RS real_le_imp_less_or_eq) +by (res_inst_tac [("a2","c")] ((abs_ge_zero RS real_le_imp_less_or_eq) RS disjE) 1); by (dtac sym 2); by (Asm_full_simp_tac 2 THEN Blast_tac 2); @@ -470,8 +470,9 @@ by (res_inst_tac [("z1","abs(inverse(z - x))")] (real_mult_le_cancel_iff2 RS iffD1) 2); by (Asm_full_simp_tac 2); -by (asm_full_simp_tac (simpset() addsimps [abs_mult RS sym, - real_mult_assoc RS sym]) 2); +by (asm_full_simp_tac (simpset() + delsimps [abs_inverse] + addsimps [abs_mult RS sym, real_mult_assoc RS sym]) 2); by (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) = \ \ (f z - f x)/(z - x) - f' x" 2); by (asm_full_simp_tac (simpset() addsimps [abs_mult RS sym] @ real_mult_ac) 2); diff -r 22542982bffd -r f4d806fd72ce src/HOL/Hyperreal/Lim.ML --- a/src/HOL/Hyperreal/Lim.ML Fri Dec 12 15:05:18 2003 +0100 +++ b/src/HOL/Hyperreal/Lim.ML Sat Dec 13 09:33:52 2003 +0100 @@ -132,7 +132,7 @@ by (REPEAT(dres_inst_tac [("x","xa")] spec 3) THEN step_tac (claset() addSEs [order_less_trans]) 3); by (ALLGOALS(res_inst_tac [("t","r")] (real_mult_1 RS subst))); -by (ALLGOALS(rtac abs_mult_less2)); +by (ALLGOALS(rtac abs_mult_less)); by Auto_tac; qed "LIM_mult_zero"; @@ -1665,7 +1665,7 @@ by (cut_inst_tac [("x","f x"),("y","y")] linorder_less_linear 1); by Safe_tac; by (dres_inst_tac [("x","ba - x")] spec 1); -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [abs_iff]))); +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [thm"abs_if"]))); by (dres_inst_tac [("x","aa - x")] spec 1); by (case_tac "x \\ aa" 1); by (ALLGOALS Asm_full_simp_tac); diff -r 22542982bffd -r f4d806fd72ce src/HOL/Hyperreal/Transcendental.ML --- a/src/HOL/Hyperreal/Transcendental.ML Fri Dec 12 15:05:18 2003 +0100 +++ b/src/HOL/Hyperreal/Transcendental.ML Sat Dec 13 09:33:52 2003 +0100 @@ -461,7 +461,7 @@ simpset() addsimps [real_mult_assoc,realpow_abs])); by (dres_inst_tac [("x","0")] spec 2 THEN Force_tac 2); by (auto_tac (claset(),simpset() addsimps [abs_mult,realpow_abs] @ real_mult_ac)); -by (res_inst_tac [("x2","z ^ n")] (abs_ge_zero RS real_le_imp_less_or_eq +by (res_inst_tac [("a2","z ^ n")] (abs_ge_zero RS real_le_imp_less_or_eq RS disjE) 1 THEN dtac sym 2); by (auto_tac (claset() addSIs [real_mult_le_le_mono2], simpset() addsimps [real_mult_assoc RS sym, @@ -473,10 +473,12 @@ by (auto_tac (claset(),simpset() addsimps [realpow_abs RS sym])); by (subgoal_tac "x ~= 0" 1); by (subgoal_tac "x ~= 0" 3); -by (auto_tac (claset(),simpset() addsimps - [abs_inverse RS sym,realpow_not_zero,abs_mult - RS sym,realpow_inverse,realpow_mult RS sym])); -by (auto_tac (claset() addSIs [geometric_sums],simpset() addsimps +by (auto_tac (claset(), + simpset() delsimps [abs_inverse] + addsimps [abs_inverse RS sym, realpow_not_zero, abs_mult RS sym, + realpow_inverse, realpow_mult RS sym])); +by (auto_tac (claset() addSIs [geometric_sums], + simpset() addsimps [realpow_abs,real_divide_eq_inverse RS sym])); by (res_inst_tac [("z","abs(x)")] (CLAIM_SIMP "[|(0::real) x a --> P a) & (a < 0 --> P(-a)))" +by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) + subsection{*Misc Results*} diff -r 22542982bffd -r f4d806fd72ce src/HOL/Real/RealArith.thy --- a/src/HOL/Real/RealArith.thy Fri Dec 12 15:05:18 2003 +0100 +++ b/src/HOL/Real/RealArith.thy Sat Dec 13 09:33:52 2003 +0100 @@ -9,7 +9,7 @@ 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))" + "((0::real) \ x/y) = ((x \ 0 | 0 \ y) & (0 \ x | y \ 0))" by (simp add: real_divide_def zero_le_mult_iff, auto) lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)" @@ -76,8 +76,6 @@ subsection{*Absolute Value Function for the Reals*} -(** abs (absolute value) **) - lemma abs_nat_number_of: "abs (number_of v :: real) = (if neg (number_of v) then number_of (bin_minus v) @@ -87,30 +85,14 @@ declare abs_nat_number_of [simp] -lemma abs_split [arith_split]: - "P(abs (x::real)) = ((0 <= x --> P x) & (x < 0 --> P(-x)))" -apply (unfold real_abs_def, auto) -done - (*---------------------------------------------------------------------------- Properties of the absolute value function over the reals (adapted version of previously proved theorems about abs) ----------------------------------------------------------------------------*) -lemma abs_iff: "abs (r::real) = (if 0<=r then r else -r)" -apply (unfold real_abs_def, auto) -done - -lemma abs_zero: "abs 0 = (0::real)" -by (unfold real_abs_def, auto) -declare abs_zero [simp] - -lemma abs_one: "abs (1::real) = 1" -by (unfold real_abs_def, simp) -declare abs_one [simp] - -lemma abs_eqI1: "(0::real)<=x ==> abs x = x" +text{*FIXME: these should go!*} +lemma abs_eqI1: "(0::real)\x ==> abs x = x" by (unfold real_abs_def, simp) lemma abs_eqI2: "(0::real) < x ==> abs x = x" @@ -119,103 +101,37 @@ lemma abs_minus_eqI2: "x < (0::real) ==> abs x = -x" by (unfold real_abs_def real_le_def, simp) -lemma abs_minus_eqI1: "x<=(0::real) ==> abs x = -x" -by (unfold real_abs_def, simp) - -lemma abs_ge_zero: "(0::real)<= abs x" -by (unfold real_abs_def, simp) -declare abs_ge_zero [simp] - -lemma abs_idempotent: "abs(abs x)=abs (x::real)" -by (unfold real_abs_def, simp) -declare abs_idempotent [simp] - -lemma abs_zero_iff: "(abs x = 0) = (x=(0::real))" -by (unfold real_abs_def, simp) -declare abs_zero_iff [iff] - -lemma abs_ge_self: "x<=abs (x::real)" -by (unfold real_abs_def, simp) - -lemma abs_ge_minus_self: "-x<=abs (x::real)" -by (unfold real_abs_def, simp) - -lemma abs_mult: "abs (x * y) = abs x * abs (y::real)" -apply (unfold real_abs_def) -apply (auto dest!: order_antisym simp add: real_0_le_mult_iff) -done - -lemma abs_inverse: "abs(inverse(x::real)) = inverse(abs(x))" -apply (unfold real_abs_def) -apply (case_tac "x=0") -apply (auto simp add: real_minus_inverse real_le_less INVERSE_ZERO real_inverse_gt_0) -done - lemma abs_mult_inverse: "abs (x * inverse y) = (abs x) * inverse (abs (y::real))" by (simp add: abs_mult abs_inverse) -lemma abs_triangle_ineq: "abs(x+y) <= abs x + abs (y::real)" +text{*Much easier to prove using arithmetic than abstractly!!*} +lemma abs_triangle_ineq: "abs(x+y) \ abs x + abs (y::real)" by (unfold real_abs_def, simp) (*Unused, but perhaps interesting as an example*) -lemma abs_triangle_ineq_four: "abs(w + x + y + z) <= abs(w) + abs(x) + abs(y) + abs(z::real)" +lemma abs_triangle_ineq_four: "abs(w + x + y + z) \ abs(w) + abs(x) + abs(y) + abs(z::real)" by (simp add: abs_triangle_ineq [THEN order_trans]) -lemma abs_minus_cancel: "abs(-x)=abs(x::real)" -by (unfold real_abs_def, simp) -declare abs_minus_cancel [simp] - lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))" by (unfold real_abs_def, simp) -lemma abs_triangle_minus_ineq: "abs(x + (-y)) <= abs x + abs (y::real)" +lemma abs_triangle_minus_ineq: "abs(x + (-y)) \ abs x + abs (y::real)" by (unfold real_abs_def, simp) lemma abs_add_less [rule_format (no_asm)]: "abs x < r --> abs y < s --> abs(x+y) < r+(s::real)" by (unfold real_abs_def, simp) -lemma abs_add_minus_less: "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)" +lemma abs_add_minus_less: + "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)" by (unfold real_abs_def, simp) -(* lemmas manipulating terms *) -lemma real_mult_0_less: "((0::real)*x < r)=(0 < r)" -by simp - -lemma real_mult_less_trans: "[| (0::real) < y; x < r; y*r < t*s |] ==> y*x < t*s" -by (blast intro!: real_mult_less_mono2 intro: order_less_trans) - -(*USED ONLY IN NEXT THM*) -lemma real_mult_le_less_trans: - "[| (0::real)<=y; x < r; y*r < t*s; 0 < t*s|] ==> y*x < t*s" -apply (drule order_le_imp_less_or_eq) -apply (fast elim: real_mult_0_less [THEN iffD2] real_mult_less_trans) -done - -lemma abs_mult_less: "[| abs x < r; abs y < s |] ==> abs(x*y) < r*(s::real)" -apply (simp add: abs_mult) -apply (rule real_mult_le_less_trans) -apply (rule abs_ge_zero, assumption) -apply (rule_tac [2] real_mult_order) -apply (auto intro!: real_mult_less_mono1 abs_ge_zero intro: order_le_less_trans) -done - -lemma abs_mult_less2: "[| abs x < r; abs y < s |] ==> abs(x)*abs(y) < r*(s::real)" -by (auto intro: abs_mult_less simp add: abs_mult [symmetric]) - -lemma abs_less_gt_zero: "abs(x) < r ==> (0::real) < r" -by (blast intro!: order_le_less_trans abs_ge_zero) - -lemma abs_minus_one: "abs (-1) = (1::real)" +lemma abs_minus_one [simp]: "abs (-1) = (1::real)" by (unfold real_abs_def, simp) -declare abs_minus_one [simp] - -lemma abs_disj: "abs x =x | abs x = -(x::real)" -by (unfold real_abs_def, auto) lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))" by (unfold real_abs_def, auto) -lemma abs_le_interval_iff: "(abs x <= r) = (-r<=x & x<=(r::real))" +lemma abs_le_interval_iff: "(abs x \ r) = (-r\x & x\(r::real))" by (unfold real_abs_def, auto) lemma abs_add_pos_gt_zero: "(0::real) < k ==> 0 < k + abs(x)" @@ -225,21 +141,9 @@ by (unfold real_abs_def, auto) declare abs_add_one_gt_zero [simp] -lemma abs_not_less_zero: "~ abs x < (0::real)" -by (unfold real_abs_def, auto) -declare abs_not_less_zero [simp] - lemma abs_circle: "abs h < abs y - abs x ==> abs (x + h) < abs (y::real)" by (auto intro: abs_triangle_ineq [THEN order_le_less_trans]) -lemma abs_le_zero_iff: "(abs x <= (0::real)) = (x = 0)" -by (unfold real_abs_def, auto) -declare abs_le_zero_iff [simp] - -lemma real_0_less_abs_iff: "((0::real) < abs x) = (x ~= 0)" -by (simp add: real_abs_def, arith) -declare real_0_less_abs_iff [simp] - lemma abs_real_of_nat_cancel: "abs (real x) = real (x::nat)" by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero) declare abs_real_of_nat_cancel [simp] @@ -251,18 +155,18 @@ declare abs_add_one_not_less_self [simp] (* used in vector theory *) -lemma abs_triangle_ineq_three: "abs(w + x + (y::real)) <= abs(w) + abs(x) + abs(y)" +lemma abs_triangle_ineq_three: "abs(w + x + (y::real)) \ abs(w) + abs(x) + abs(y)" by (auto intro!: abs_triangle_ineq [THEN order_trans] real_add_left_mono simp add: real_add_assoc) lemma abs_diff_less_imp_gt_zero: "abs(x - y) < y ==> (0::real) < y" apply (unfold real_abs_def) -apply (case_tac "0 <= x - y", auto) +apply (case_tac "0 \ x - y", auto) done lemma abs_diff_less_imp_gt_zero2: "abs(x - y) < x ==> (0::real) < x" apply (unfold real_abs_def) -apply (case_tac "0 <= x - y", auto) +apply (case_tac "0 \ x - y", auto) done lemma abs_diff_less_imp_gt_zero3: "abs(x - y) < y ==> (0::real) < x" @@ -272,11 +176,11 @@ by (auto simp add: abs_interval_iff) lemma abs_triangle_ineq_minus_cancel: - "abs(x) <= abs(x + (-y)) + abs((y::real))" + "abs(x) \ abs(x + (-y)) + abs((y::real))" apply (unfold real_abs_def, auto) done -lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) <= abs(x + -l) + abs(y + -m)" +lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \ abs(x + -l) + abs(y + -m)" apply (simp add: real_add_assoc) apply (rule_tac x1 = y in real_add_left_commute [THEN ssubst]) apply (rule real_add_assoc [THEN subst]) @@ -305,13 +209,10 @@ val abs_nat_number_of = thm"abs_nat_number_of"; val abs_split = thm"abs_split"; -val abs_iff = thm"abs_iff"; val abs_zero = thm"abs_zero"; -val abs_one = thm"abs_one"; val abs_eqI1 = thm"abs_eqI1"; val abs_eqI2 = thm"abs_eqI2"; val abs_minus_eqI2 = thm"abs_minus_eqI2"; -val abs_minus_eqI1 = thm"abs_minus_eqI1"; val abs_ge_zero = thm"abs_ge_zero"; val abs_idempotent = thm"abs_idempotent"; val abs_zero_iff = thm"abs_zero_iff"; @@ -327,22 +228,13 @@ val abs_triangle_minus_ineq = thm"abs_triangle_minus_ineq"; val abs_add_less = thm"abs_add_less"; val abs_add_minus_less = thm"abs_add_minus_less"; -val real_mult_0_less = thm"real_mult_0_less"; -val real_mult_less_trans = thm"real_mult_less_trans"; -val real_mult_le_less_trans = thm"real_mult_le_less_trans"; -val abs_mult_less = thm"abs_mult_less"; -val abs_mult_less2 = thm"abs_mult_less2"; -val abs_less_gt_zero = thm"abs_less_gt_zero"; val abs_minus_one = thm"abs_minus_one"; -val abs_disj = thm"abs_disj"; val abs_interval_iff = thm"abs_interval_iff"; val abs_le_interval_iff = thm"abs_le_interval_iff"; val abs_add_pos_gt_zero = thm"abs_add_pos_gt_zero"; val abs_add_one_gt_zero = thm"abs_add_one_gt_zero"; -val abs_not_less_zero = thm"abs_not_less_zero"; val abs_circle = thm"abs_circle"; val abs_le_zero_iff = thm"abs_le_zero_iff"; -val real_0_less_abs_iff = thm"real_0_less_abs_iff"; val abs_real_of_nat_cancel = thm"abs_real_of_nat_cancel"; val abs_add_one_not_less_self = thm"abs_add_one_not_less_self"; val abs_triangle_ineq_three = thm"abs_triangle_ineq_three"; @@ -352,6 +244,8 @@ val abs_diff_less_imp_gt_zero4 = thm"abs_diff_less_imp_gt_zero4"; val abs_triangle_ineq_minus_cancel = thm"abs_triangle_ineq_minus_cancel"; val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq"; + +val abs_mult_less = thm"abs_mult_less"; *} end diff -r 22542982bffd -r f4d806fd72ce src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Fri Dec 12 15:05:18 2003 +0100 +++ b/src/HOL/Ring_and_Field.thy Sat Dec 13 09:33:52 2003 +0100 @@ -1360,26 +1360,94 @@ subsection {* Absolute Value *} -text{*But is it really better than just rewriting with @{text abs_if}?*} -lemma abs_split: - "P(abs(a::'a::ordered_ring)) = ((0 \ a --> P a) & (a < 0 --> P(-a)))" -by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) - lemma abs_zero [simp]: "abs 0 = (0::'a::ordered_ring)" by (simp add: abs_if) -lemma abs_mult: "abs (x * y) = abs x * abs (y::'a::ordered_ring)" -apply (case_tac "x=0 | y=0", force) +lemma abs_one [simp]: "abs 1 = (1::'a::ordered_ring)" + by (simp add: abs_if zero_less_one [THEN order_less_not_sym]) + +lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_ring)" +apply (case_tac "a=0 | b=0", force) apply (auto elim: order_less_asym simp add: abs_if mult_less_0_iff linorder_neq_iff minus_mult_left [symmetric] minus_mult_right [symmetric]) done -lemma abs_eq_0 [simp]: "(abs x = 0) = (x = (0::'a::ordered_ring))" +lemma abs_eq_0 [simp]: "(abs a = 0) = (a = (0::'a::ordered_ring))" +by (simp add: abs_if) + +lemma zero_less_abs_iff [simp]: "(0 < abs a) = (a \ (0::'a::ordered_ring))" +by (simp add: abs_if linorder_neq_iff) + +lemma abs_not_less_zero [simp]: "~ abs a < (0::'a::ordered_ring)" +by (simp add: abs_if order_less_not_sym [of a 0]) + +lemma abs_le_zero_iff [simp]: "(abs a \ (0::'a::ordered_ring)) = (a = 0)" +by (simp add: order_le_less) + +lemma abs_minus_cancel [simp]: "abs (-a) = abs(a::'a::ordered_ring)" +apply (auto simp add: abs_if linorder_not_less order_less_not_sym [of 0 a]) +apply (drule order_antisym, assumption, simp) +done + +lemma abs_ge_zero [simp]: "(0::'a::ordered_ring) \ abs a" +apply (simp add: abs_if order_less_imp_le) +apply (simp add: linorder_not_less) +done + +lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::ordered_ring)" + by (force elim: order_less_asym simp add: abs_if) + +lemma abs_zero_iff [iff]: "(abs a = 0) = (a = (0::'a::ordered_ring))" by (simp add: abs_if) -lemma zero_less_abs_iff [simp]: "(0 < abs x) = (x ~= (0::'a::ordered_ring))" -by (simp add: abs_if linorder_neq_iff) +lemma abs_ge_self: "a \ abs (a::'a::ordered_ring)" +apply (simp add: abs_if) +apply (simp add: order_less_imp_le order_trans [of _ 0]) +done + +lemma abs_ge_minus_self: "-a \ abs (a::'a::ordered_ring)" +by (insert abs_ge_self [of "-a"], simp) + +lemma nonzero_abs_inverse: + "a \ 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)" +apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq + negative_imp_inverse_negative) +apply (blast intro: positive_imp_inverse_positive elim: order_less_asym) +done + +lemma abs_inverse [simp]: + "abs (inverse (a::'a::{ordered_field,division_by_zero})) = + inverse (abs a)" +apply (case_tac "a=0", simp) +apply (simp add: nonzero_abs_inverse) +done + + +lemma nonzero_abs_divide: + "b \ 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b" +by (simp add: divide_inverse abs_mult nonzero_abs_inverse) + +lemma abs_divide: + "abs (a / (b::'a::{ordered_field,division_by_zero})) = abs a / abs b" +apply (case_tac "b=0", simp) +apply (simp add: nonzero_abs_divide) +done + +(*TOO DIFFICULT: 6 CASES +lemma abs_triangle_ineq: "abs (a+b) \ abs a + abs (b::'a::ordered_ring)" +apply (simp add: abs_if) +apply (auto ); +*) + +lemma abs_mult_less: + "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_ring)" +proof - + assume ac: "abs a < c" + hence cpos: "0