# HG changeset patch # User paulson # Date 1072947992 -3600 # Node ID 6137d24eef7911d2e951da6956e4728cf8ec9b76 # Parent 14f29eb097a3a018442dcb169191f4e9b0a57f82 tweaking of lemmas in RealDef, RealOrd diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Complex/CLim.ML --- a/src/HOL/Complex/CLim.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Complex/CLim.ML Thu Jan 01 10:06:32 2004 +0100 @@ -50,7 +50,7 @@ \ cmod(xa - x) < inverse(real(Suc n)) & r <= cmod(f xa - L)"; by (Clarify_tac 1); by (cut_inst_tac [("n1","n")] - (real_of_nat_Suc_gt_zero RS real_inverse_gt_0) 1); + (real_of_nat_Suc_gt_zero RS positive_imp_inverse_positive) 1); by Auto_tac; val lemma_CLIM = result(); @@ -132,7 +132,7 @@ \ cmod(xa - x) < inverse(real(Suc n)) & r <= abs (f xa - L)"; by (Clarify_tac 1); by (cut_inst_tac [("n1","n")] - (real_of_nat_Suc_gt_zero RS real_inverse_gt_0) 1); + (real_of_nat_Suc_gt_zero RS positive_imp_inverse_positive) 1); by Auto_tac; val lemma_CRLIM = result(); diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Complex/CSeries.ML --- a/src/HOL/Complex/CSeries.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Complex/CSeries.ML Thu Jan 01 10:06:32 2004 +0100 @@ -30,7 +30,7 @@ Goal "sumc m n f + sumc m n g = sumc m n (%n. f n + g n)"; by (induct_tac "n" 1); -by (auto_tac (claset(),simpset() addsimps real_add_ac)); +by (auto_tac (claset(),simpset() addsimps add_ac)); qed "sumc_add"; Goal "r * sumc m n f = sumc m n (%n. r * f n)"; @@ -107,7 +107,7 @@ Goal "(ALL n. m <= Suc n --> f n = r) & m <= na \ \ --> sumc m na f = (complex_of_real(real (na - m)) * r)"; by (induct_tac "na" 1); -by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib, Suc_diff_n, +by (auto_tac (claset(),simpset() addsimps [left_distrib, Suc_diff_n, real_of_nat_Suc,complex_of_real_add RS sym, complex_add_mult_distrib])); qed_spec_mp "sumc_interval_const"; @@ -115,7 +115,7 @@ Goal "(ALL n. m <= n --> f n = r) & m <= na \ \ --> sumc m na f = (complex_of_real(real (na - m)) * r)"; by (induct_tac "na" 1); -by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib, Suc_diff_n, +by (auto_tac (claset(),simpset() addsimps [left_distrib, Suc_diff_n, real_of_nat_Suc,complex_of_real_add RS sym, complex_add_mult_distrib])); qed_spec_mp "sumc_interval_const2"; @@ -128,15 +128,15 @@ by (ALLGOALS(dres_inst_tac [("x","n")] spec)); by (Step_tac 1); by (dtac le_imp_less_or_eq 1 THEN Step_tac 1); -by (dtac real_add_le_mono 2); -by (dres_inst_tac [("i","sumr 0 m f")] (order_refl RS real_add_le_mono) 1); +by (dtac add_mono 2); +by (dres_inst_tac [("i","sumr 0 m f")] (order_refl RS add_mono) 1); by (Auto_tac); qed_spec_mp "sumc_le"; Goal "!!f g. (ALL r. m <= r & r < n --> f r <= g r) \ \ --> sumc m n f <= sumc m n g"; by (induct_tac "n" 1); -by (auto_tac (claset() addIs [real_add_le_mono], +by (auto_tac (claset() addIs [add_mono], simpset() addsimps [le_def])); qed_spec_mp "sumc_le2"; diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Complex/Complex.thy --- a/src/HOL/Complex/Complex.thy Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Complex/Complex.thy Thu Jan 01 10:06:32 2004 +0100 @@ -127,14 +127,11 @@ declare inj_Abs_complex [THEN injD, simp] lemma Abs_complex_cancel_iff: "(Abs_complex x = Abs_complex y) = (x = y)" -apply (auto dest: inj_Abs_complex [THEN injD]) -done +by (auto dest: inj_Abs_complex [THEN injD]) declare Abs_complex_cancel_iff [simp] lemma pair_mem_complex: "(x,y) : complex" -apply (unfold complex_def) -apply auto -done +by (unfold complex_def, auto) declare pair_mem_complex [simp] lemma Abs_complex_inverse2: "Rep_complex (Abs_complex (x,y)) = (x,y)" @@ -144,7 +141,7 @@ lemma eq_Abs_complex: "(!!x y. z = Abs_complex(x,y) ==> P) ==> P" apply (rule_tac p = "Rep_complex z" in PairE) -apply (drule_tac f = "Abs_complex" in arg_cong) +apply (drule_tac f = Abs_complex in arg_cong) apply (force simp add: Rep_complex_inverse) done @@ -161,14 +158,14 @@ declare Im [simp] lemma Abs_complex_cancel: "Abs_complex(Re(z),Im(z)) = z" -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (simp (no_asm_simp)) done declare Abs_complex_cancel [simp] lemma complex_Re_Im_cancel_iff: "(w=z) = (Re(w) = Re(z) & Im(w) = Im(z))" -apply (rule_tac z = "w" in eq_Abs_complex) -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = w in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (auto dest: inj_Abs_complex [THEN injD]) done @@ -196,15 +193,11 @@ declare complex_Im_one [simp] lemma complex_Re_i: "Re(ii) = 0" -apply (unfold i_def) -apply auto -done +by (unfold i_def, auto) declare complex_Re_i [simp] lemma complex_Im_i: "Im(ii) = 1" -apply (unfold i_def) -apply auto -done +by (unfold i_def, auto) declare complex_Im_i [simp] lemma Re_complex_of_real_zero: "Re(complex_of_real 0) = 0" @@ -232,15 +225,11 @@ declare Im_complex_of_real_one [simp] lemma Re_complex_of_real: "Re(complex_of_real z) = z" -apply (unfold complex_of_real_def) -apply auto -done +by (unfold complex_of_real_def, auto) declare Re_complex_of_real [simp] lemma Im_complex_of_real: "Im(complex_of_real z) = 0" -apply (unfold complex_of_real_def) -apply auto -done +by (unfold complex_of_real_def, auto) declare Im_complex_of_real [simp] @@ -253,13 +242,13 @@ lemma complex_Re_minus: "Re (-z) = - Re z" apply (unfold Re_def) -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (auto simp add: complex_minus) done lemma complex_Im_minus: "Im (-z) = - Im z" apply (unfold Im_def) -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (auto simp add: complex_minus) done @@ -271,8 +260,7 @@ lemma inj_complex_minus: "inj(%r::complex. -r)" apply (rule inj_onI) -apply (drule_tac f = "uminus" in arg_cong) -apply simp +apply (drule_tac f = uminus in arg_cong, simp) done lemma complex_minus_zero: "-(0::complex) = 0" @@ -282,20 +270,18 @@ declare complex_minus_zero [simp] lemma complex_minus_zero_iff: "(-x = 0) = (x = (0::complex))" -apply (rule_tac z = "x" in eq_Abs_complex) +apply (rule_tac z = x in eq_Abs_complex) apply (auto dest: inj_Abs_complex [THEN injD] simp add: complex_zero_def complex_minus) done declare complex_minus_zero_iff [simp] lemma complex_minus_zero_iff2: "(0 = -x) = (x = (0::real))" -apply (auto dest: sym) -done +by (auto dest: sym) declare complex_minus_zero_iff2 [simp] lemma complex_minus_not_zero_iff: "(-x ~= 0) = (x ~= (0::complex))" -apply auto -done +by auto subsection{*Addition*} @@ -308,15 +294,15 @@ lemma complex_Re_add: "Re(x + y) = Re(x) + Re(y)" apply (unfold Re_def) -apply (rule_tac z = "x" in eq_Abs_complex) -apply (rule_tac z = "y" in eq_Abs_complex) +apply (rule_tac z = x in eq_Abs_complex) +apply (rule_tac z = y in eq_Abs_complex) apply (auto simp add: complex_add) done lemma complex_Im_add: "Im(x + y) = Im(x) + Im(y)" apply (unfold Im_def) -apply (rule_tac z = "x" in eq_Abs_complex) -apply (rule_tac z = "y" in eq_Abs_complex) +apply (rule_tac z = x in eq_Abs_complex) +apply (rule_tac z = y in eq_Abs_complex) apply (auto simp add: complex_add) done @@ -332,7 +318,7 @@ lemma complex_add_left_commute: "(x::complex) + (y + z) = y + (x + z)" apply (unfold complex_add_def) -apply (simp (no_asm) add: real_add_left_commute) +apply (simp (no_asm) add: add_left_commute) done lemmas complex_add_ac = complex_add_assoc complex_add_commute @@ -375,18 +361,17 @@ declare complex_add_minus_cancel [simp] complex_minus_add_cancel [simp] lemma complex_add_minus_eq_minus: "x + y = (0::complex) ==> x = -y" -apply (auto simp add: complex_Re_Im_cancel_iff complex_Re_add complex_Im_add complex_Re_minus complex_Im_minus) -done +by (auto simp add: complex_Re_Im_cancel_iff complex_Re_add complex_Im_add complex_Re_minus complex_Im_minus) lemma complex_minus_add_distrib: "-(x + y) = -x + -(y::complex)" -apply (rule_tac z = "x" in eq_Abs_complex) -apply (rule_tac z = "y" in eq_Abs_complex) +apply (rule_tac z = x in eq_Abs_complex) +apply (rule_tac z = y in eq_Abs_complex) apply (auto simp add: complex_minus complex_add) done declare complex_minus_add_distrib [simp] lemma complex_add_left_cancel: "((x::complex) + y = x + z) = (y = z)" -apply (safe) +apply safe apply (drule_tac f = "%t.-x + t" in arg_cong) apply (simp add: complex_add_assoc [symmetric]) done @@ -398,15 +383,13 @@ declare complex_add_right_cancel [simp] lemma complex_eq_minus_iff: "((x::complex) = y) = (0 = x + - y)" -apply (safe) -apply (rule_tac [2] x1 = "-y" in complex_add_right_cancel [THEN iffD1]) -apply auto +apply safe +apply (rule_tac [2] x1 = "-y" in complex_add_right_cancel [THEN iffD1], auto) done lemma complex_eq_minus_iff2: "((x::complex) = y) = (x + - y = 0)" -apply (safe) -apply (rule_tac [2] x1 = "-y" in complex_add_right_cancel [THEN iffD1]) -apply auto +apply safe +apply (rule_tac [2] x1 = "-y" in complex_add_right_cancel [THEN iffD1], auto) done lemma complex_diff_0: "(0::complex) - x = -x" @@ -430,8 +413,7 @@ done lemma complex_diff_eq_eq: "((x::complex) - y = z) = (x = z + y)" -apply (auto simp add: complex_diff_def complex_add_assoc) -done +by (auto simp add: complex_diff_def complex_add_assoc) subsection{*Multiplication*} @@ -450,12 +432,12 @@ lemma complex_mult_assoc: "((u::complex) * v) * w = u * (v * w)" apply (unfold complex_mult_def) -apply (simp (no_asm) add: complex_Re_Im_cancel_iff real_mult_assoc real_diff_mult_distrib2 real_add_mult_distrib2 real_diff_mult_distrib real_add_mult_distrib real_mult_left_commute) +apply (simp (no_asm) add: complex_Re_Im_cancel_iff real_mult_assoc right_diff_distrib right_distrib left_diff_distrib left_distrib mult_left_commute) done lemma complex_mult_left_commute: "(x::complex) * (y * z) = y * (x * z)" apply (unfold complex_mult_def) -apply (simp (no_asm) add: complex_Re_Im_cancel_iff real_mult_left_commute real_diff_mult_distrib2 real_add_mult_distrib2) +apply (simp (no_asm) add: complex_Re_Im_cancel_iff mult_left_commute right_diff_distrib right_distrib) done lemmas complex_mult_ac = complex_mult_assoc complex_mult_commute @@ -463,7 +445,7 @@ lemma complex_mult_one_left: "(1::complex) * z = z" apply (unfold complex_one_def) -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (simp (no_asm_simp) add: complex_mult) done declare complex_mult_one_left [simp] @@ -475,7 +457,7 @@ lemma complex_mult_zero_left: "(0::complex) * z = 0" apply (unfold complex_zero_def) -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (simp (no_asm_simp) add: complex_mult) done declare complex_mult_zero_left [simp] @@ -486,20 +468,18 @@ declare complex_mult_zero_right [simp] lemma complex_divide_zero: "0 / z = (0::complex)" -apply (unfold complex_divide_def) -apply auto -done +by (unfold complex_divide_def, auto) declare complex_divide_zero [simp] lemma complex_minus_mult_eq1: "-(x * y) = -x * (y::complex)" -apply (rule_tac z = "x" in eq_Abs_complex) -apply (rule_tac z = "y" in eq_Abs_complex) +apply (rule_tac z = x in eq_Abs_complex) +apply (rule_tac z = y in eq_Abs_complex) apply (auto simp add: complex_mult complex_minus real_diff_def) done lemma complex_minus_mult_eq2: "-(x * y) = x * -(y::complex)" -apply (rule_tac z = "x" in eq_Abs_complex) -apply (rule_tac z = "y" in eq_Abs_complex) +apply (rule_tac z = x in eq_Abs_complex) +apply (rule_tac z = y in eq_Abs_complex) apply (auto simp add: complex_mult complex_minus real_diff_def) done @@ -526,10 +506,10 @@ done lemma complex_add_mult_distrib: "((z1::complex) + z2) * w = (z1 * w) + (z2 * w)" -apply (rule_tac z = "z1" in eq_Abs_complex) -apply (rule_tac z = "z2" in eq_Abs_complex) -apply (rule_tac z = "w" in eq_Abs_complex) -apply (auto simp add: complex_mult complex_add real_add_mult_distrib real_diff_def real_add_ac) +apply (rule_tac z = z1 in eq_Abs_complex) +apply (rule_tac z = z2 in eq_Abs_complex) +apply (rule_tac z = w in eq_Abs_complex) +apply (auto simp add: complex_mult complex_add left_distrib real_diff_def add_ac) done lemma complex_add_mult_distrib2: "(w::complex) * (z1 + z2) = (w * z1) + (w * z2)" @@ -555,26 +535,23 @@ done lemma COMPLEX_INVERSE_ZERO: "inverse 0 = (0::complex)" -apply (unfold complex_inverse_def complex_zero_def) -apply auto -done +by (unfold complex_inverse_def complex_zero_def, auto) lemma COMPLEX_DIVISION_BY_ZERO: "a / (0::complex) = 0" apply (simp (no_asm) add: complex_divide_def COMPLEX_INVERSE_ZERO) done lemma complex_mult_inv_left: "z ~= (0::complex) ==> inverse(z) * z = 1" -apply (rule_tac z = "z" in eq_Abs_complex) -apply (auto simp add: complex_mult complex_inverse complex_one_def complex_zero_def real_add_divide_distrib [symmetric] real_power_two mult_ac) -apply (drule_tac y = "y" in real_sum_squares_not_zero) -apply (drule_tac [2] x = "x" in real_sum_squares_not_zero2) -apply auto +apply (rule_tac z = z in eq_Abs_complex) +apply (auto simp add: complex_mult complex_inverse complex_one_def + complex_zero_def add_divide_distrib [symmetric] real_power_two mult_ac) +apply (drule_tac y = y in real_sum_squares_not_zero) +apply (drule_tac [2] x = x in real_sum_squares_not_zero2, auto) done declare complex_mult_inv_left [simp] lemma complex_mult_inv_right: "z ~= (0::complex) ==> z * inverse(z) = 1" -apply (auto intro: complex_mult_commute [THEN subst]) -done +by (auto intro: complex_mult_commute [THEN subst]) declare complex_mult_inv_right [simp] lemma complex_mult_left_cancel: "(c::complex) ~= 0 ==> (c*a=c*b) = (a=b)" @@ -584,21 +561,21 @@ done lemma complex_mult_right_cancel: "(c::complex) ~= 0 ==> (a*c=b*c) = (a=b)" -apply (safe) +apply safe apply (drule_tac f = "%x. x*inverse c" in arg_cong) apply (simp add: complex_mult_ac) done lemma complex_inverse_not_zero: "z ~= 0 ==> inverse(z::complex) ~= 0" -apply (safe) +apply safe apply (frule complex_mult_right_cancel [THEN iffD2]) apply (erule_tac [2] V = "inverse z = 0" in thin_rl) -apply (assumption , auto) +apply (assumption, auto) done declare complex_inverse_not_zero [simp] lemma complex_mult_not_zero: "!!x. [| x ~= 0; y ~= (0::complex) |] ==> x * y ~= 0" -apply (safe) +apply safe apply (drule_tac f = "%z. inverse x*z" in arg_cong) apply (simp add: complex_mult_assoc [symmetric]) done @@ -621,10 +598,8 @@ lemma complex_minus_inverse: "inverse(-x) = -inverse(x::complex)" apply (case_tac "x = 0", simp add: COMPLEX_INVERSE_ZERO) -apply (rule_tac c1 = "-x" in complex_mult_right_cancel [THEN iffD1]) -apply force -apply (subst complex_mult_inv_left) -apply auto +apply (rule_tac c1 = "-x" in complex_mult_right_cancel [THEN iffD1], force) +apply (subst complex_mult_inv_left, auto) done lemma complex_inverse_distrib: "inverse(x*y) = inverse x * inverse (y::complex)" @@ -699,8 +674,7 @@ declare complex_of_real_zero [simp] lemma complex_of_real_eq_iff: "(complex_of_real x = complex_of_real y) = (x = y)" -apply (auto dest: inj_complex_of_real [THEN injD]) -done +by (auto dest: inj_complex_of_real [THEN injD]) declare complex_of_real_eq_iff [iff] lemma complex_of_real_minus: "complex_of_real(-x) = - complex_of_real x" @@ -710,7 +684,8 @@ lemma complex_of_real_inverse: "complex_of_real(inverse x) = inverse(complex_of_real x)" apply (case_tac "x=0") apply (simp add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO) -apply (simp add: complex_inverse complex_of_real_def real_divide_def real_inverse_distrib real_power_two) +apply (simp add: complex_inverse complex_of_real_def real_divide_def + inverse_mult_distrib real_power_two) done lemma complex_of_real_add: "complex_of_real x + complex_of_real y = complex_of_real (x + y)" @@ -750,9 +725,7 @@ declare complex_mod_zero [simp] lemma complex_mod_one: "cmod(1) = 1" -apply (unfold cmod_def) -apply (simp add: ); -done +by (unfold cmod_def, simp) declare complex_mod_one [simp] lemma complex_mod_complex_of_real: "cmod(complex_of_real x) = abs x" @@ -779,8 +752,7 @@ done lemma complex_cnj_cancel_iff: "(cnj x = cnj y) = (x = y)" -apply (auto dest: inj_cnj [THEN injD]) -done +by (auto dest: inj_cnj [THEN injD]) declare complex_cnj_cancel_iff [simp] lemma complex_cnj_cnj: "cnj (cnj z) = z" @@ -796,7 +768,7 @@ declare complex_cnj_complex_of_real [simp] lemma complex_mod_cnj: "cmod (cnj z) = cmod z" -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (simp (no_asm_simp) add: complex_cnj complex_mod real_power_two) done declare complex_mod_cnj [simp] @@ -807,13 +779,13 @@ done lemma complex_cnj_inverse: "cnj(inverse z) = inverse(cnj z)" -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (simp (no_asm_simp) add: complex_cnj complex_inverse real_power_two) done lemma complex_cnj_add: "cnj(w + z) = cnj(w) + cnj(z)" -apply (rule_tac z = "w" in eq_Abs_complex) -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = w in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (simp (no_asm_simp) add: complex_cnj complex_add) done @@ -823,8 +795,8 @@ done lemma complex_cnj_mult: "cnj(w * z) = cnj(w) * cnj(z)" -apply (rule_tac z = "w" in eq_Abs_complex) -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = w in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (simp (no_asm_simp) add: complex_cnj complex_mult) done @@ -845,28 +817,27 @@ done lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re(z))" -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (simp (no_asm_simp) add: complex_add complex_cnj complex_of_real_def) done lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii" -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (simp (no_asm_simp) add: complex_add complex_cnj complex_of_real_def complex_diff_def complex_minus i_def complex_mult) done lemma complex_cnj_zero: "cnj 0 = 0" -apply (simp add: cnj_def complex_zero_def) -done +by (simp add: cnj_def complex_zero_def) declare complex_cnj_zero [simp] lemma complex_cnj_zero_iff: "(cnj z = 0) = (z = 0)" -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (auto simp add: complex_zero_def complex_cnj) done declare complex_cnj_zero_iff [iff] lemma complex_mult_cnj: "z * cnj z = complex_of_real (Re(z) ^ 2 + Im(z) ^ 2)" -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (auto simp add: complex_cnj complex_mult complex_of_real_def real_power_two) done @@ -881,8 +852,8 @@ lemma complex_add_left_cancel_zero: "(x + y = x) = (y = (0::complex))" apply (unfold complex_zero_def) -apply (rule_tac z = "x" in eq_Abs_complex) -apply (rule_tac z = "y" in eq_Abs_complex) +apply (rule_tac z = x in eq_Abs_complex) +apply (rule_tac z = y in eq_Abs_complex) apply (auto simp add: complex_add) done declare complex_add_left_cancel_zero [simp] @@ -910,7 +881,7 @@ *) lemma complex_mod_eq_zero_cancel: "(cmod x = 0) = (x = 0)" -apply (rule_tac z = "x" in eq_Abs_complex) +apply (rule_tac z = x in eq_Abs_complex) apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: complex_mod complex_zero_def real_power_two) done declare complex_mod_eq_zero_cancel [simp] @@ -921,21 +892,19 @@ declare complex_mod_complex_of_real_of_nat [simp] lemma complex_mod_minus: "cmod (-x) = cmod(x)" -apply (rule_tac z = "x" in eq_Abs_complex) +apply (rule_tac z = x in eq_Abs_complex) apply (simp (no_asm_simp) add: complex_mod complex_minus real_power_two) done declare complex_mod_minus [simp] lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2" -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (simp (no_asm_simp) add: complex_mod complex_cnj complex_mult); apply (simp (no_asm) add: real_power_two real_abs_def) done lemma complex_mod_squared: "cmod(Abs_complex(x,y)) ^ 2 = x ^ 2 + y ^ 2" -apply (unfold cmod_def) -apply auto -done +by (unfold cmod_def, auto) lemma complex_mod_ge_zero: "0 <= cmod x" apply (unfold cmod_def) @@ -944,41 +913,40 @@ declare complex_mod_ge_zero [simp] lemma abs_cmod_cancel: "abs(cmod x) = cmod x" -apply (auto intro: abs_eqI1) -done +by (auto intro: abs_eqI1) declare abs_cmod_cancel [simp] lemma complex_mod_mult: "cmod(x*y) = cmod(x) * cmod(y)" -apply (rule_tac z = "x" in eq_Abs_complex) -apply (rule_tac z = "y" in eq_Abs_complex) +apply (rule_tac z = x in eq_Abs_complex) +apply (rule_tac z = y in eq_Abs_complex) apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2 [symmetric] simp del: realpow_Suc) -apply (rule_tac n = "1" in realpow_Suc_cancel_eq) +apply (rule_tac n = 1 in realpow_Suc_cancel_eq) apply (auto simp add: real_power_two [symmetric] simp del: realpow_Suc) -apply (auto simp add: real_diff_def real_power_two real_add_mult_distrib2 real_add_mult_distrib real_add_ac real_mult_ac) +apply (auto simp add: real_diff_def real_power_two right_distrib left_distrib add_ac mult_ac) done lemma complex_mod_add_squared_eq: "cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)" -apply (rule_tac z = "x" in eq_Abs_complex) -apply (rule_tac z = "y" in eq_Abs_complex) +apply (rule_tac z = x in eq_Abs_complex) +apply (rule_tac z = y in eq_Abs_complex) apply (auto simp add: complex_add complex_mod_squared complex_mult complex_cnj real_diff_def simp del: realpow_Suc) -apply (auto simp add: real_add_mult_distrib2 real_add_mult_distrib real_power_two real_mult_ac real_add_ac) +apply (auto simp add: right_distrib left_distrib real_power_two mult_ac add_ac) done lemma complex_Re_mult_cnj_le_cmod: "Re(x * cnj y) <= cmod(x * cnj y)" -apply (rule_tac z = "x" in eq_Abs_complex) -apply (rule_tac z = "y" in eq_Abs_complex) +apply (rule_tac z = x in eq_Abs_complex) +apply (rule_tac z = y in eq_Abs_complex) apply (auto simp add: complex_mod complex_mult complex_cnj real_diff_def simp del: realpow_Suc) done declare complex_Re_mult_cnj_le_cmod [simp] lemma complex_Re_mult_cnj_le_cmod2: "Re(x * cnj y) <= cmod(x * y)" -apply (cut_tac x = "x" and y = "y" in complex_Re_mult_cnj_le_cmod) +apply (cut_tac x = x and y = y in complex_Re_mult_cnj_le_cmod) apply (simp add: complex_mod_mult) done declare complex_Re_mult_cnj_le_cmod2 [simp] lemma real_sum_squared_expand: "((x::real) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y" -apply (simp (no_asm) add: real_add_mult_distrib real_add_mult_distrib2 real_power_two) +apply (simp (no_asm) add: left_distrib right_distrib real_power_two) done lemma complex_mod_triangle_squared: "cmod (x + y) ^ 2 <= (cmod(x) + cmod(y)) ^ 2" @@ -993,38 +961,36 @@ declare complex_mod_minus_le_complex_mod [simp] lemma complex_mod_triangle_ineq: "cmod (x + y) <= cmod(x) + cmod(y)" -apply (rule_tac n = "1" in realpow_increasing) +apply (rule_tac n = 1 in realpow_increasing) apply (auto intro: order_trans [OF _ complex_mod_ge_zero] simp add: real_power_two [symmetric]) done declare complex_mod_triangle_ineq [simp] lemma complex_mod_triangle_ineq2: "cmod(b + a) - cmod b <= cmod a" -apply (cut_tac x1 = "b" and y1 = "a" and z = "-cmod b" in complex_mod_triangle_ineq [THEN real_add_le_mono1]) +apply (cut_tac x1 = b and y1 = a and c = "-cmod b" + in complex_mod_triangle_ineq [THEN add_right_mono]) apply (simp (no_asm)) done declare complex_mod_triangle_ineq2 [simp] lemma complex_mod_diff_commute: "cmod (x - y) = cmod (y - x)" -apply (rule_tac z = "x" in eq_Abs_complex) -apply (rule_tac z = "y" in eq_Abs_complex) -apply (auto simp add: complex_diff complex_mod real_diff_mult_distrib2 real_power_two real_diff_mult_distrib real_add_ac real_mult_ac) +apply (rule_tac z = x in eq_Abs_complex) +apply (rule_tac z = y in eq_Abs_complex) +apply (auto simp add: complex_diff complex_mod right_diff_distrib real_power_two left_diff_distrib add_ac mult_ac) done lemma complex_mod_add_less: "[| cmod x < r; cmod y < s |] ==> cmod (x + y) < r + s" -apply (auto intro: order_le_less_trans complex_mod_triangle_ineq) -done +by (auto intro: order_le_less_trans complex_mod_triangle_ineq) lemma complex_mod_mult_less: "[| cmod x < r; cmod y < s |] ==> cmod (x * y) < r * s" -apply (auto intro: real_mult_less_mono' simp add: complex_mod_mult) -done +by (auto intro: real_mult_less_mono' simp add: complex_mod_mult) lemma complex_mod_diff_ineq: "cmod(a) - cmod(b) <= cmod(a + b)" apply (rule linorder_cases [of "cmod(a)" "cmod (b)"]) apply auto -apply (rule order_trans [of _ 0] , rule order_less_imp_le) -apply (simp add: compare_rls) -apply (simp add: ); +apply (rule order_trans [of _ 0], rule order_less_imp_le) +apply (simp add: compare_rls, simp) apply (simp add: compare_rls) apply (rule complex_mod_minus [THEN subst]) apply (rule order_trans) @@ -1034,15 +1000,14 @@ declare complex_mod_diff_ineq [simp] lemma complex_Re_le_cmod: "Re z <= cmod z" -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (auto simp add: complex_mod simp del: realpow_Suc) done declare complex_Re_le_cmod [simp] lemma complex_mod_gt_zero: "z ~= 0 ==> 0 < cmod z" -apply (cut_tac x = "z" in complex_mod_ge_zero) -apply (drule order_le_imp_less_or_eq) -apply auto +apply (cut_tac x = z in complex_mod_ge_zero) +apply (drule order_le_imp_less_or_eq, auto) done @@ -1054,12 +1019,10 @@ done lemma complexpow_minus: "(-x::complex) ^ n = (if even n then (x ^ n) else -(x ^ n))" -apply (induct_tac "n") -apply auto -done +by (induct_tac "n", auto) lemma complex_inverse_minus: "inverse (-x) = - inverse (x::complex)" -apply (rule_tac z = "x" in eq_Abs_complex) +apply (rule_tac z = x in eq_Abs_complex) apply (simp (no_asm_simp) add: complex_inverse complex_minus real_power_two) done @@ -1097,8 +1060,7 @@ subsection{*More Exponentiation*} lemma complexpow_zero: "(0::complex) ^ (Suc n) = 0" -apply auto -done +by auto declare complexpow_zero [simp] lemma complexpow_not_zero [rule_format (no_asm)]: "r ~= (0::complex) --> r ^ n ~= 0" @@ -1109,8 +1071,7 @@ declare complexpow_not_zero [intro] lemma complexpow_zero_zero: "r ^ n = (0::complex) ==> r = 0" -apply (blast intro: ccontr dest: complexpow_not_zero) -done +by (blast intro: ccontr dest: complexpow_not_zero) lemma complexpow_i_squared: "ii ^ 2 = -(1::complex)" apply (unfold i_def) @@ -1119,22 +1080,17 @@ declare complexpow_i_squared [simp] lemma complex_i_not_zero: "ii ~= 0" -apply (unfold i_def complex_zero_def) -apply auto -done +by (unfold i_def complex_zero_def, auto) declare complex_i_not_zero [simp] lemma complex_mult_eq_zero_cancel1: "x * y ~= (0::complex) ==> x ~= 0" -apply auto -done +by auto lemma complex_mult_eq_zero_cancel2: "x * y ~= 0 ==> y ~= (0::complex)" -apply auto -done +by auto lemma complex_mult_not_eq_zero_iff: "(x * y ~= 0) = (x ~= 0 & y ~= (0::complex))" -apply auto -done +by auto declare complex_mult_not_eq_zero_iff [iff] lemma complexpow_inverse: "inverse ((r::complex) ^ n) = (inverse r) ^ n" @@ -1160,9 +1116,7 @@ declare sgn_one [simp] lemma sgn_minus: "sgn (-z) = - sgn(z)" -apply (unfold sgn_def) -apply auto -done +by (unfold sgn_def, auto) lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)" @@ -1171,18 +1125,16 @@ done lemma complex_split: "EX x y. z = complex_of_real(x) + ii * complex_of_real(y)" -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (auto simp add: complex_of_real_def i_def complex_mult complex_add) done lemma Re_complex_i: "Re(complex_of_real(x) + ii * complex_of_real(y)) = x" -apply (auto simp add: complex_of_real_def i_def complex_mult complex_add) -done +by (auto simp add: complex_of_real_def i_def complex_mult complex_add) declare Re_complex_i [simp] lemma Im_complex_i: "Im(complex_of_real(x) + ii * complex_of_real(y)) = y" -apply (auto simp add: complex_of_real_def i_def complex_mult complex_add) -done +by (auto simp add: complex_of_real_def i_def complex_mult complex_add) declare Im_complex_i [simp] lemma i_mult_eq: "ii * ii = complex_of_real (-1)" @@ -1243,7 +1195,7 @@ lemma complex_eq_cancel_iff2: "(complex_of_real x + ii * complex_of_real y = complex_of_real xa) = (x = xa & y = 0)" -apply (cut_tac xa = "x" and ya = "y" and xb = "xa" and yb = "0" in complex_eq_cancel_iff) +apply (cut_tac xa = x and ya = y and xb = xa and yb = 0 in complex_eq_cancel_iff) apply (simp del: complex_eq_cancel_iff) done declare complex_eq_cancel_iff2 [simp] @@ -1256,7 +1208,7 @@ lemma complex_eq_cancel_iff3: "(complex_of_real x + ii * complex_of_real y = ii * complex_of_real ya) = (x = 0 & y = ya)" -apply (cut_tac xa = "x" and ya = "y" and xb = "0" and yb = "ya" in complex_eq_cancel_iff) +apply (cut_tac xa = x and ya = y and xb = 0 and yb = ya in complex_eq_cancel_iff) apply (simp del: complex_eq_cancel_iff) done declare complex_eq_cancel_iff3 [simp] @@ -1284,7 +1236,7 @@ lemma Re_sgn: "Re(sgn z) = Re(z)/cmod z" apply (unfold sgn_def complex_divide_def) -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (auto simp add: complex_of_real_inverse [symmetric]) apply (auto simp add: complex_of_real_def complex_mult real_divide_def) done @@ -1293,7 +1245,7 @@ lemma Im_sgn: "Im(sgn z) = Im(z)/cmod z" apply (unfold sgn_def complex_divide_def) -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (auto simp add: complex_of_real_inverse [symmetric]) apply (auto simp add: complex_of_real_def complex_mult real_divide_def) done @@ -1337,10 +1289,8 @@ "0 < y ==> cos (arg(ii * complex_of_real y)) = 0" apply (unfold arg_def) apply (auto simp add: abs_eqI2) -apply (rule_tac a = "pi/2" in someI2) -apply auto -apply (rule order_less_trans [of _ 0]) -apply auto +apply (rule_tac a = "pi/2" in someI2, auto) +apply (rule order_less_trans [of _ 0], auto) done declare cos_arg_i_mult_zero [simp] @@ -1348,31 +1298,25 @@ "y < 0 ==> cos (arg(ii * complex_of_real y)) = 0" apply (unfold arg_def) apply (auto simp add: abs_minus_eqI2) -apply (rule_tac a = "- pi/2" in someI2) -apply auto -apply (rule order_trans [of _ 0]) -apply auto +apply (rule_tac a = "- pi/2" in someI2, auto) +apply (rule order_trans [of _ 0], auto) done declare cos_arg_i_mult_zero2 [simp] lemma complex_of_real_not_zero_iff: "(complex_of_real y ~= 0) = (y ~= 0)" -apply (unfold complex_zero_def complex_of_real_def) -apply auto +apply (unfold complex_zero_def complex_of_real_def, auto) done declare complex_of_real_not_zero_iff [simp] lemma complex_of_real_zero_iff: "(complex_of_real y = 0) = (y = 0)" apply auto -apply (rule ccontr , drule complex_of_real_not_zero_iff [THEN iffD2]) -apply simp +apply (rule ccontr, drule complex_of_real_not_zero_iff [THEN iffD2], simp) done declare complex_of_real_zero_iff [simp] lemma cos_arg_i_mult_zero3: "y ~= 0 ==> cos (arg(ii * complex_of_real y)) = 0" -apply (cut_tac x = "y" and y = "0" in linorder_less_linear) -apply auto -done +by (cut_tac x = y and y = 0 in linorder_less_linear, auto) declare cos_arg_i_mult_zero3 [simp] @@ -1380,7 +1324,7 @@ lemma complex_split_polar: "EX r a. z = complex_of_real r * (complex_of_real(cos a) + ii * complex_of_real(sin a))" -apply (cut_tac z = "z" in complex_split) +apply (cut_tac z = z in complex_split) apply (auto simp add: polar_Ex complex_add_mult_distrib2 complex_of_real_mult complex_mult_ac) done @@ -1396,9 +1340,7 @@ declare Re_complex_polar [simp] lemma Re_rcis: "Re(rcis r a) = r * cos a" -apply (unfold rcis_def cis_def) -apply auto -done +by (unfold rcis_def cis_def, auto) declare Re_rcis [simp] lemma Im_complex_polar: "Im(complex_of_real r * @@ -1408,21 +1350,17 @@ declare Im_complex_polar [simp] lemma Im_rcis: "Im(rcis r a) = r * sin a" -apply (unfold rcis_def cis_def) -apply auto -done +by (unfold rcis_def cis_def, auto) declare Im_rcis [simp] lemma complex_mod_complex_polar: "cmod (complex_of_real r * (complex_of_real(cos a) + ii * complex_of_real(sin a))) = abs r" -apply (auto simp add: complex_add_mult_distrib2 cmod_i complex_of_real_mult real_add_mult_distrib2 [symmetric] realpow_mult complex_mult_ac real_mult_ac simp del: realpow_Suc) +apply (auto simp add: complex_add_mult_distrib2 cmod_i complex_of_real_mult right_distrib [symmetric] realpow_mult complex_mult_ac mult_ac simp del: realpow_Suc) done declare complex_mod_complex_polar [simp] lemma complex_mod_rcis: "cmod(rcis r a) = abs r" -apply (unfold rcis_def cis_def) -apply auto -done +by (unfold rcis_def cis_def, auto) declare complex_mod_rcis [simp] lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))" @@ -1432,53 +1370,53 @@ done lemma complex_Re_cnj: "Re(cnj z) = Re z" -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (auto simp add: complex_cnj) done declare complex_Re_cnj [simp] lemma complex_Im_cnj: "Im(cnj z) = - Im z" -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (auto simp add: complex_cnj) done declare complex_Im_cnj [simp] lemma complex_In_mult_cnj_zero: "Im (z * cnj z) = 0" -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (auto simp add: complex_cnj complex_mult) done declare complex_In_mult_cnj_zero [simp] lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)" -apply (rule_tac z = "z" in eq_Abs_complex) -apply (rule_tac z = "w" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) +apply (rule_tac z = w in eq_Abs_complex) apply (auto simp add: complex_mult) done lemma complex_Re_mult_complex_of_real: "Re (z * complex_of_real c) = Re(z) * c" apply (unfold complex_of_real_def) -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (auto simp add: complex_mult) done declare complex_Re_mult_complex_of_real [simp] lemma complex_Im_mult_complex_of_real: "Im (z * complex_of_real c) = Im(z) * c" apply (unfold complex_of_real_def) -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (auto simp add: complex_mult) done declare complex_Im_mult_complex_of_real [simp] lemma complex_Re_mult_complex_of_real2: "Re (complex_of_real c * z) = c * Re(z)" apply (unfold complex_of_real_def) -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (auto simp add: complex_mult) done declare complex_Re_mult_complex_of_real2 [simp] lemma complex_Im_mult_complex_of_real2: "Im (complex_of_real c * z) = c * Im(z)" apply (unfold complex_of_real_def) -apply (rule_tac z = "z" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) apply (auto simp add: complex_mult) done declare complex_Im_mult_complex_of_real2 [simp] @@ -1498,7 +1436,7 @@ apply (auto simp add: cos_add sin_add complex_add_mult_distrib2 complex_add_mult_distrib complex_mult_ac complex_add_ac) apply (auto simp add: complex_add_mult_distrib2 [symmetric] complex_mult_assoc [symmetric] complex_of_real_mult complex_of_real_add complex_add_assoc [symmetric] i_mult_eq simp del: i_mult_eq2) apply (auto simp add: complex_add_ac) -apply (auto simp add: complex_add_assoc [symmetric] complex_of_real_add real_add_mult_distrib2 real_diff_def mult_ac add_ac) +apply (auto simp add: complex_add_assoc [symmetric] complex_of_real_add right_distrib real_diff_def mult_ac add_ac) done lemma cis_mult: "cis a * cis b = cis (a + b)" @@ -1506,15 +1444,11 @@ done lemma cis_zero: "cis 0 = 1" -apply (unfold cis_def) -apply auto -done +by (unfold cis_def, auto) declare cis_zero [simp] lemma cis_zero2: "cis 0 = complex_of_real 1" -apply (unfold cis_def) -apply auto -done +by (unfold cis_def, auto) declare cis_zero2 [simp] lemma rcis_zero_mod: "rcis 0 a = 0" @@ -1548,7 +1482,7 @@ lemma cis_real_of_nat_Suc_mult: "cis (real (Suc n) * a) = cis a * cis (real n * a)" apply (unfold cis_def) -apply (auto simp add: real_of_nat_Suc real_add_mult_distrib cos_add sin_add complex_add_mult_distrib complex_add_mult_distrib2 complex_of_real_add complex_of_real_mult complex_mult_ac complex_add_ac) +apply (auto simp add: real_of_nat_Suc left_distrib cos_add sin_add complex_add_mult_distrib complex_add_mult_distrib2 complex_of_real_add complex_of_real_mult complex_mult_ac complex_add_ac) apply (auto simp add: complex_add_mult_distrib2 [symmetric] complex_mult_assoc [symmetric] i_mult_eq complex_of_real_mult complex_of_real_add complex_add_assoc [symmetric] complex_of_real_minus [symmetric] real_diff_def mult_ac simp del: i_mult_eq2) done @@ -1572,8 +1506,8 @@ lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)" apply (case_tac "r=0") apply (simp (no_asm_simp) add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO) -apply (auto simp add: complex_inverse_complex_split complex_add_mult_distrib2 complex_of_real_mult rcis_def cis_def real_power_two complex_mult_ac real_mult_ac) -apply (auto simp add: real_add_mult_distrib2 [symmetric] complex_of_real_minus complex_diff_def) +apply (auto simp add: complex_inverse_complex_split complex_add_mult_distrib2 complex_of_real_mult rcis_def cis_def real_power_two complex_mult_ac mult_ac) +apply (auto simp add: right_distrib [symmetric] complex_of_real_minus complex_diff_def) done lemma cis_divide: "cis a / cis b = cis (a - b)" @@ -1590,36 +1524,28 @@ done lemma Re_cis: "Re(cis a) = cos a" -apply (unfold cis_def) -apply auto -done +by (unfold cis_def, auto) declare Re_cis [simp] lemma Im_cis: "Im(cis a) = sin a" -apply (unfold cis_def) -apply auto -done +by (unfold cis_def, auto) declare Im_cis [simp] lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)" -apply (auto simp add: DeMoivre) -done +by (auto simp add: DeMoivre) lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)" -apply (auto simp add: DeMoivre) -done +by (auto simp add: DeMoivre) lemma expi_Im_split: "expi (ii * complex_of_real y) = complex_of_real (cos y) + ii * complex_of_real (sin y)" -apply (unfold expi_def cis_def) -apply auto +apply (unfold expi_def cis_def, auto) done lemma expi_Im_cis: "expi (ii * complex_of_real y) = cis y" -apply (unfold expi_def) -apply auto +apply (unfold expi_def, auto) done lemma expi_add: "expi(a + b) = expi(a) * expi(b)" @@ -1630,54 +1556,50 @@ lemma expi_complex_split: "expi(complex_of_real x + ii * complex_of_real y) = complex_of_real (exp(x)) * cis y" -apply (unfold expi_def) -apply auto +apply (unfold expi_def, auto) done lemma expi_zero: "expi (0::complex) = 1" -apply (unfold expi_def) -apply auto -done +by (unfold expi_def, auto) declare expi_zero [simp] lemma complex_Re_mult_eq: "Re (w * z) = Re w * Re z - Im w * Im z" -apply (rule_tac z = "z" in eq_Abs_complex) -apply (rule_tac z = "w" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) +apply (rule_tac z = w in eq_Abs_complex) apply (auto simp add: complex_mult) done lemma complex_Im_mult_eq: "Im (w * z) = Re w * Im z + Im w * Re z" -apply (rule_tac z = "z" in eq_Abs_complex) -apply (rule_tac z = "w" in eq_Abs_complex) +apply (rule_tac z = z in eq_Abs_complex) +apply (rule_tac z = w in eq_Abs_complex) apply (auto simp add: complex_mult) done lemma complex_expi_Ex: "EX a r. z = complex_of_real r * expi a" -apply (cut_tac z = "z" in rcis_Ex) +apply (cut_tac z = z in rcis_Ex) apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric] complex_of_real_mult) -apply (rule_tac x = "ii * complex_of_real a" in exI) -apply auto +apply (rule_tac x = "ii * complex_of_real a" in exI, auto) done (**** Goal "[| - pi < a; a <= pi |] ==> (-pi < a & a <= 0) | (0 <= a & a <= pi)" -by Auto_tac; +by Auto_tac qed "lemma_split_interval"; Goalw [arg_def] "[| r ~= 0; - pi < a; a <= pi |] \ \ ==> arg(complex_of_real r * \ \ (complex_of_real(cos a) + ii * complex_of_real(sin a))) = a"; -by Auto_tac; +by Auto_tac by (cut_inst_tac [("x","0"),("y","r")] linorder_less_linear 1); by (auto_tac (claset(),simpset() addsimps (map (full_rename_numerals thy) [rabs_eqI2,rabs_minus_eqI2,real_minus_rinv]) [real_divide_def, - real_minus_mult_eq2 RS sym] real_mult_ac)); + minus_mult_right RS sym] mult_ac)); by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym])); -by (dtac lemma_split_interval 1 THEN safe); +by (dtac lemma_split_interval 1 THEN safe) ****) diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Complex/NSCA.ML --- a/src/HOL/Complex/NSCA.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Complex/NSCA.ML Thu Jan 01 10:06:32 2004 +0100 @@ -644,7 +644,7 @@ by (res_inst_tac [("e","hcmod u"),("e'","- hcmod u")] Infinitesimal_interval2 1); by (auto_tac (claset() addDs [capprox_approx_zero_iff RS iffD1], simpset() addsimps [mem_infmal_iff RS sym,hypreal_diff_def])); -by (res_inst_tac [("C","hcmod x")] hypreal_le_add_left_cancel 1); +by (res_inst_tac [("c1","hcmod x")] (add_le_cancel_left RS iffD1) 1); by (auto_tac (claset(),simpset() addsimps [symmetric hypreal_diff_def])); qed "Infinitesimal_hcmod_add_diff"; @@ -868,7 +868,7 @@ by (Ultra_tac 1); by (dtac sym 1 THEN res_inst_tac [("z","X x")] eq_Abs_complex 1); by (auto_tac (claset(),simpset() addsimps [complex_mod,numeral_2_eq_2] delsimps [realpow_Suc])); -by (rtac ccontr 1 THEN dtac real_leI 1); +by (rtac ccontr 1 THEN dtac (linorder_not_less RS iffD1) 1); by (dtac order_less_le_trans 1 THEN assume_tac 1); by (dtac (real_sqrt_ge_abs1 RSN (2,order_less_le_trans)) 1); by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2 RS sym])); @@ -883,7 +883,7 @@ by (Ultra_tac 1); by (dtac sym 1 THEN res_inst_tac [("z","X x")] eq_Abs_complex 1); by (auto_tac (claset(),simpset() addsimps [complex_mod] delsimps [realpow_Suc])); -by (rtac ccontr 1 THEN dtac real_leI 1); +by (rtac ccontr 1 THEN dtac (linorder_not_less RS iffD1) 1); by (dtac order_less_le_trans 1 THEN assume_tac 1); by (dtac (real_sqrt_ge_abs2 RSN (2,order_less_le_trans)) 1); by Auto_tac; diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Complex/ROOT.ML --- a/src/HOL/Complex/ROOT.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Complex/ROOT.ML Thu Jan 01 10:06:32 2004 +0100 @@ -5,6 +5,6 @@ The Complex Numbers *) -with_path "../Real" use_thy "Real"; +with_path "../Real" use_thy "Real"; with_path "../Hyperreal" use_thy "Hyperreal"; time_use_thy "Complex_Main"; diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/Fact.ML --- a/src/HOL/Hyperreal/Fact.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/Fact.ML Thu Jan 01 10:06:32 2004 +0100 @@ -51,7 +51,7 @@ qed "fact_less_mono"; Goal "0 < inverse (real (fact n))"; -by (auto_tac (claset(),simpset() addsimps [real_inverse_gt_0])); +by (auto_tac (claset(),simpset() addsimps [positive_imp_inverse_positive])); qed "inv_real_of_nat_fact_gt_zero"; Addsimps [inv_real_of_nat_fact_gt_zero]; diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/HLog.ML --- a/src/HOL/Hyperreal/HLog.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/HLog.ML Thu Jan 01 10:06:32 2004 +0100 @@ -226,13 +226,13 @@ Goal "[| 0 < a; a ~= 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x"; by (res_inst_tac [("a1","hlog a x")] (add_left_cancel RS iffD1) 1); by (auto_tac (claset(),simpset() addsimps [hypreal_not_refl2 RS not_sym, - hlog_mult RS sym,hypreal_inverse_gt_0])); + hlog_mult RS sym,positive_imp_inverse_positive])); qed "hlog_inverse"; Goal "[| 0 < a; a ~= 1; 0 < x; 0 < y|] \ \ ==> hlog a (x/y) = hlog a x - hlog a y"; by (auto_tac (claset(), - simpset() addsimps [hypreal_inverse_gt_0,hlog_mult, hlog_inverse,hypreal_diff_def,hypreal_divide_def])); + simpset() addsimps [positive_imp_inverse_positive,hlog_mult, hlog_inverse,hypreal_diff_def,hypreal_divide_def])); qed "hlog_divide"; Goal "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"; diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/HTranscendental.ML --- a/src/HOL/Hyperreal/HTranscendental.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/HTranscendental.ML Thu Jan 01 10:06:32 2004 +0100 @@ -466,7 +466,7 @@ (* we do proof by considering ln of 1/x *) Goal "[| x : Infinitesimal; 0 < x |] ==> ( *f* ln) x : HInfinite"; by (dtac Infinitesimal_inverse_HInfinite 1); -by (ftac hypreal_inverse_gt_0 1); +by (ftac positive_imp_inverse_positive 1); by (dtac starfun_ln_HInfinite 2); by (auto_tac (claset(),simpset() addsimps [starfun_ln_inverse, HInfinite_minus_iff])); diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/HyperBin.ML --- a/src/HOL/Hyperreal/HyperBin.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/HyperBin.ML Thu Jan 01 10:06:32 2004 +0100 @@ -615,23 +615,4 @@ hypreal_of_real_le_number_of_iff, hypreal_of_real_less_number_of_iff, number_of_le_hypreal_of_real_iff, number_of_less_hypreal_of_real_iff]); -(** <= monotonicity results: needed for arithmetic **) - -Goal "[| i <= j; (0::hypreal) <= k |] ==> i*k <= j*k"; -by (auto_tac (claset(), - simpset() addsimps [order_le_less, hypreal_mult_less_mono1])); -qed "hypreal_mult_le_mono1"; - -Goal "[| i <= j; (0::hypreal) <= k |] ==> k*i <= k*j"; -by (dtac hypreal_mult_le_mono1 1); -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]))); -qed "hypreal_mult_le_mono2"; - -Goal "[| u <= v; x <= y; 0 <= v; (0::hypreal) <= x |] ==> u * x <= v * y"; -by (etac (hypreal_mult_le_mono1 RS order_trans) 1); -by (assume_tac 1); -by (etac hypreal_mult_le_mono2 1); -by (assume_tac 1); -qed "hypreal_mult_le_mono"; - Addsimps [hypreal_minus_1_eq_m1]; diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/HyperDef.thy --- a/src/HOL/Hyperreal/HyperDef.thy Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/HyperDef.thy Thu Jan 01 10:06:32 2004 +0100 @@ -326,7 +326,7 @@ lemma hypreal_add_commute: "(z::hypreal) + w = w + z" apply (rule_tac z = z in eq_Abs_hypreal) apply (rule_tac z = w in eq_Abs_hypreal) -apply (simp add: real_add_ac hypreal_add) +apply (simp add: add_ac hypreal_add) done lemma hypreal_add_assoc: "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)" @@ -419,7 +419,7 @@ apply (rule_tac z = z1 in eq_Abs_hypreal) apply (rule_tac z = z2 in eq_Abs_hypreal) apply (rule_tac z = w in eq_Abs_hypreal) -apply (simp add: hypreal_mult hypreal_add real_add_mult_distrib) +apply (simp add: hypreal_mult hypreal_add left_distrib) done text{*one and zero are distinct*} @@ -452,7 +452,7 @@ apply (rule_tac z = x in eq_Abs_hypreal) apply (simp add: hypreal_inverse hypreal_mult) apply (drule FreeUltrafilterNat_Compl_mem) -apply (blast intro!: real_mult_inv_right FreeUltrafilterNat_subset) +apply (blast intro!: right_inverse FreeUltrafilterNat_subset) done lemma hypreal_mult_inverse_left: @@ -476,10 +476,6 @@ show "y \ 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def) qed -(*Pull negations out*) -declare minus_mult_right [symmetric, simp] - minus_mult_left [symmetric, simp] - lemma HYPREAL_INVERSE_ZERO: "inverse 0 = (0::hypreal)" by (simp add: hypreal_inverse hypreal_zero_def) diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/HyperOrd.thy --- a/src/HOL/Hyperreal/HyperOrd.thy Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/HyperOrd.thy Thu Jan 01 10:06:32 2004 +0100 @@ -25,20 +25,9 @@ apply (erule add_strict_left_mono) done -lemma hypreal_less_add_right_cancel: "(A::hypreal) + C < B + C ==> A < B" -apply (simp (no_asm_use)) -done - lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \ y|] ==> r < x + y" by (auto dest: hypreal_add_less_le_mono) -lemma hypreal_le_add_left_cancel: "!!(A::hypreal). C + A \ C + B ==> A \ B" -apply simp -done - -lemma hypreal_le_square [simp]: "(0::hypreal) \ x*x" - by (rule Ring_and_Field.zero_le_square) - lemma hypreal_add_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y" apply (erule order_less_trans) apply (drule hypreal_add_less_mono2, simp) @@ -54,12 +43,6 @@ "[| u u*x < v* y" by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) -lemma hypreal_inverse_gt_0: "0 < x ==> 0 < inverse (x::hypreal)" - by (rule Ring_and_Field.positive_imp_inverse_positive) - -lemma hypreal_inverse_less_0: "x < 0 ==> inverse (x::hypreal) < 0" - by (rule Ring_and_Field.negative_imp_inverse_negative) - subsection{*Existence of Infinite Hyperreal Number*} @@ -68,9 +51,11 @@ apply (rule Rep_hypreal) done -(* existence of infinite number not corresponding to any real number *) -(* use assumption that member FreeUltrafilterNat is not finite *) -(* a few lemmas first *) +text{*Existence of infinite number not corresponding to any real number. +Use assumption that member @{term FreeUltrafilterNat} is not finite.*} + + +text{*A few lemmas first*} lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} | (\y. {n::nat. x = real n} = {y})" @@ -82,16 +67,18 @@ lemma not_ex_hypreal_of_real_eq_omega: "~ (\x. hypreal_of_real x = omega)" apply (unfold omega_def hypreal_of_real_def) -apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] lemma_finite_omega_set [THEN FreeUltrafilterNat_finite]) +apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] + lemma_finite_omega_set [THEN FreeUltrafilterNat_finite]) done lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \ omega" by (cut_tac not_ex_hypreal_of_real_eq_omega, auto) -(* existence of infinitesimal number also not *) -(* corresponding to any real number *) +text{*Existence of infinitesimal number also not corresponding to any + real number*} -lemma lemma_epsilon_empty_singleton_disj: "{n::nat. x = inverse(real(Suc n))} = {} | +lemma lemma_epsilon_empty_singleton_disj: + "{n::nat. x = inverse(real(Suc n))} = {} | (\y. {n::nat. x = inverse(real(Suc n))} = {y})" apply (auto simp add: inj_real_of_nat [THEN inj_eq]) done @@ -123,15 +110,10 @@ val hypreal_add_left_le_mono1 = thm"hypreal_add_left_le_mono1"; val hypreal_add_less_le_mono = thm"hypreal_add_less_le_mono"; val hypreal_add_le_less_mono = thm"hypreal_add_le_less_mono"; -val hypreal_less_add_right_cancel = thm"hypreal_less_add_right_cancel"; val hypreal_add_zero_less_le_mono = thm"hypreal_add_zero_less_le_mono"; -val hypreal_le_add_left_cancel = thm"hypreal_le_add_left_cancel"; -val hypreal_le_square = thm"hypreal_le_square"; val hypreal_mult_less_mono1 = thm"hypreal_mult_less_mono1"; val hypreal_mult_less_mono2 = thm"hypreal_mult_less_mono2"; val hypreal_mult_less_mono = thm"hypreal_mult_less_mono"; -val hypreal_inverse_gt_0 = thm"hypreal_inverse_gt_0"; -val hypreal_inverse_less_0 = thm"hypreal_inverse_less_0"; val Rep_hypreal_omega = thm"Rep_hypreal_omega"; val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj"; val lemma_finite_omega_set = thm"lemma_finite_omega_set"; diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/HyperPow.ML --- a/src/HOL/Hyperreal/HyperPow.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/HyperPow.ML Thu Jan 01 10:06:32 2004 +0100 @@ -52,7 +52,7 @@ Goal "x <= y & (0::hypreal) < x --> x ^ n <= y ^ n"; by (induct_tac "n" 1); -by (auto_tac (claset() addSIs [hypreal_mult_le_mono], simpset())); +by (auto_tac (claset() addSIs [mult_mono], simpset())); by (asm_simp_tac (simpset() addsimps [hrealpow_ge_zero]) 1); qed_spec_mp "hrealpow_le"; @@ -104,7 +104,7 @@ qed "hypreal_add_nonneg_eq_0_iff"; Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"; -by (simp_tac (HOL_ss addsimps [hypreal_le_square, hypreal_le_add_order, +by (simp_tac (HOL_ss addsimps [zero_le_square, hypreal_le_add_order, hypreal_add_nonneg_eq_0_iff]) 1); by Auto_tac; qed "hypreal_three_squares_add_zero_iff"; diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/Integration.ML --- a/src/HOL/Hyperreal/Integration.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/Integration.ML Thu Jan 01 10:06:32 2004 +0100 @@ -355,9 +355,9 @@ by (subgoal_tac "abs((rsum(D,p) f - k2) - (rsum(D,p) f - k1)) < abs(k1 - k2)" 1); by (arith_tac 1); -by (dtac real_add_less_mono 1 THEN assume_tac 1); +by (dtac add_strict_mono 1 THEN assume_tac 1); by (auto_tac (claset(), - HOL_ss addsimps [real_add_mult_distrib RS sym, + HOL_ss addsimps [left_distrib RS sym, real_mult_2_right RS sym, mult_less_cancel_right])); by (ALLGOALS(arith_tac)); qed "Integral_unique"; @@ -390,7 +390,7 @@ by (res_inst_tac [("x","%x. b - a")] exI 1); by (auto_tac (claset(),simpset() addsimps [sumr_mult RS sym,gauge_def,abs_interval_iff, - real_diff_mult_distrib2 RS sym,partition,tpart_def])); + right_diff_distrib RS sym,partition,tpart_def])); qed "Integral_mult_const"; Goal "[| a <= b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"; @@ -404,15 +404,17 @@ by (dtac sym 2); by (Asm_full_simp_tac 2 THEN Blast_tac 2); by (dres_inst_tac [("x","e/abs c")] spec 1 THEN Auto_tac); -by (asm_full_simp_tac (simpset() addsimps [real_0_less_mult_iff, +by (asm_full_simp_tac (simpset() addsimps [zero_less_mult_iff, real_divide_def]) 1); by (rtac exI 1 THEN Auto_tac); by (REPEAT(dtac spec 1) THEN Auto_tac); by (res_inst_tac [("z1","inverse(abs c)")] (real_mult_less_iff1 RS iffD1) 1); by (fold_tac [real_divide_def]); -by (auto_tac (claset(),simpset() addsimps [real_diff_mult_distrib2 - RS sym,abs_mult,real_mult_assoc RS sym, - ARITH_PROVE "c ~= 0 ==> abs (c::real) ~= 0",real_inverse_gt_0])); +by (auto_tac (claset(), + simpset() addsimps [right_diff_distrib RS sym, + abs_mult, real_mult_assoc RS sym, + ARITH_PROVE "c ~= 0 ==> abs (c::real) ~= 0", + positive_imp_inverse_positive])); qed "Integral_mult"; (* ------------------------------------------------------------------------ *) @@ -476,15 +478,15 @@ 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); +by (asm_full_simp_tac (simpset() addsimps [abs_mult RS sym] @ mult_ac) 2); by (asm_full_simp_tac (simpset() addsimps [real_diff_def]) 2); by (rtac (real_mult_commute RS subst) 2); -by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib, +by (asm_full_simp_tac (simpset() addsimps [left_distrib, real_diff_def]) 2); by (dtac (CLAIM "z ~= x ==> z + -x ~= (0::real)") 2); by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc, real_divide_def]) 2); -by (simp_tac (simpset() addsimps [real_add_mult_distrib]) 2); +by (simp_tac (simpset() addsimps [left_distrib]) 2); by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac); by (res_inst_tac [("u1","u"),("v1","v")] (ARITH_PROVE "u < v | v <= (u::real)" RS disjE) 1); @@ -494,10 +496,10 @@ by (res_inst_tac [("j","abs((f(v) - f(x)) - (f'(x) * (v - x))) + \ \ abs((f(x) - f(u)) - (f'(x) * (x - u)))")] real_le_trans 1); by (rtac (abs_triangle_ineq RSN (2,real_le_trans)) 1); -by (asm_full_simp_tac (simpset() addsimps [real_diff_mult_distrib2]) 1); +by (asm_full_simp_tac (simpset() addsimps [right_diff_distrib]) 1); by (arith_tac 1); by (res_inst_tac [("t","e*(v - u)")] (real_sum_of_halves RS subst) 1); -by (rtac real_add_le_mono 1); +by (rtac add_mono 1); by (res_inst_tac [("j","(e / 2) * abs(v - x)")] real_le_trans 1); by (Asm_full_simp_tac 2 THEN arith_tac 2); @@ -511,7 +513,7 @@ by (subgoal_tac "abs (f u - f x - f' x * (u - x)) = \ \ abs (f x - f u - f' x * (x - u))" 1); by (Asm_full_simp_tac 1); -by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2, +by (asm_full_simp_tac (simpset() addsimps [right_distrib, real_diff_def]) 2); by (arith_tac 2); by(rtac real_le_trans 1); @@ -521,8 +523,8 @@ Goal "((number_of c - 1) * x <= 0) =((number_of c ::real) * x <= x)"; by (rtac ((ARITH_PROVE "(x <= y) = (x - y <= (0::real))") RS ssubst) 1); -by (simp_tac (simpset() addsimps [real_diff_mult_distrib, - CLAIM_SIMP "c * x - x = (c - 1) * (x::real)" [real_diff_mult_distrib]]) 1); +by (simp_tac (simpset() addsimps [left_diff_distrib, + CLAIM_SIMP "c * x - x = (c - 1) * (x::real)" [left_diff_distrib]]) 1); qed "lemma_number_of_mult_le"; @@ -615,7 +617,7 @@ Goal "tpart(a,c) (D,p) ==> p = (%n. if D n < c then p n else c)"; by (rtac ext 1); by (auto_tac (claset(),simpset() addsimps [tpart_def])); -by (dtac real_leI 1); +by (dtac (linorder_not_less RS iffD1) 1); by (dres_inst_tac [("r","Suc n")] partition_ub 1); by (dres_inst_tac [("x","n")] spec 1); by Auto_tac; @@ -859,10 +861,10 @@ tpart_tag_eq RS sym])); by (ftac (tpart_partition RSN (3,lemma_additivity1)) 1); by (auto_tac (claset(),simpset() addsimps [tpart_def])); -by (dtac (real_leI RS real_le_imp_less_or_eq) 2); +by (dtac ((linorder_not_less RS iffD1) RS real_le_imp_less_or_eq) 2); by (Auto_tac); by (blast_tac (claset() addDs [lemma_additivity3]) 2); -by (dtac real_leI 2 THEN dres_inst_tac [("x","na")] spec 2); +by (dtac (linorder_not_less RS iffD1) 2 THEN dres_inst_tac [("x","na")] spec 2); by (arith_tac 2); by (ftac lemma_additivity4_psize_eq 1); by (REPEAT(assume_tac 1)); @@ -889,7 +891,7 @@ by (ALLGOALS(dres_inst_tac [("x","na")] spec)); by Auto_tac; by (asm_full_simp_tac (simpset() addsimps [split_if]) 1); -by (dtac (real_leI RS real_le_imp_less_or_eq) 1); +by (dtac ((linorder_not_less RS iffD1) RS real_le_imp_less_or_eq) 1); by (Step_tac 1); by (blast_tac (claset() addDs [lemma_additivity3a]) 1); by (dtac sym 1 THEN Auto_tac); @@ -935,7 +937,7 @@ Goalw [rsum_def] "rsum (D, p) (%x. f x + g x) = rsum (D, p) f + rsum(D, p) g"; -by (auto_tac (claset(),simpset() addsimps [sumr_add,real_add_mult_distrib])); +by (auto_tac (claset(),simpset() addsimps [sumr_add,left_distrib])); qed "rsum_add"; (* Bartle/Sherbert: Theorem 10.1.5 p. 278 *) @@ -950,10 +952,10 @@ by Auto_tac; by (dtac fine_min 1); by (REPEAT(dtac spec 1) THEN Auto_tac); -by (dres_inst_tac [("R1.0","abs (rsum (D, p) f - k1)* 2"), - ("R2.0","abs (rsum (D, p) g - k2) * 2")] - real_add_less_mono 1 THEN assume_tac 1); -by (auto_tac (claset(),HOL_ss addsimps [rsum_add,real_add_mult_distrib RS sym, +by (dres_inst_tac [("a","abs (rsum (D, p) f - k1)* 2"), + ("c","abs (rsum (D, p) g - k2) * 2")] + add_strict_mono 1 THEN assume_tac 1); +by (auto_tac (claset(),HOL_ss addsimps [rsum_add,left_distrib RS sym, real_mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"])); by (arith_tac 1); qed "Integral_add_fun"; @@ -1011,8 +1013,8 @@ by (subgoal_tac "abs((rsum(D,p) f - k1) - (rsum(D,p) g - k2)) < abs(k1 - k2)" 1); by (arith_tac 1); -by (dtac real_add_less_mono 1 THEN assume_tac 1); -by (auto_tac (claset(),HOL_ss addsimps [real_add_mult_distrib RS sym, +by (dtac add_strict_mono 1 THEN assume_tac 1); +by (auto_tac (claset(),HOL_ss addsimps [left_distrib RS sym, real_mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"])); by (arith_tac 1); qed "Integral_le"; @@ -1033,8 +1035,8 @@ by (forw_inst_tac [("x","D2")] spec 1); by (REPEAT(dtac spec 1) THEN Auto_tac); by (thin_tac "0 < e" 1); -by (dtac real_add_less_mono 1 THEN assume_tac 1); -by (auto_tac (claset(),HOL_ss addsimps [real_add_mult_distrib RS sym, +by (dtac add_strict_mono 1 THEN assume_tac 1); +by (auto_tac (claset(),HOL_ss addsimps [left_distrib RS sym, real_mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"])); by (arith_tac 1); qed "Integral_imp_Cauchy"; diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/Lim.ML --- a/src/HOL/Hyperreal/Lim.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/Lim.ML Thu Jan 01 10:06:32 2004 +0100 @@ -5,11 +5,6 @@ differentiation of real=>real functions *) -val times_divide_eq_right = thm"times_divide_eq_right"; - -val inverse_mult_distrib = thm"inverse_mult_distrib"; -val inverse_minus_eq = thm "inverse_minus_eq"; - fun ARITH_PROVE str = prove_goal thy str (fn prems => [cut_facts_tac prems 1,arith_tac 1]); @@ -51,7 +46,7 @@ THEN step_tac (claset() addSEs [order_less_trans]) 3); by (ALLGOALS(rtac (abs_sum_triangle_ineq RS order_le_less_trans))); by (ALLGOALS(rtac (real_sum_of_halves RS subst))); -by (auto_tac (claset() addIs [real_add_less_mono],simpset())); +by (auto_tac (claset() addIs [add_strict_mono],simpset())); qed "LIM_add"; Goalw [LIM_def] "f -- a --> L ==> (%x. -f(x)) -- a --> -L"; @@ -72,7 +67,7 @@ LIM_zero ----------------------------------------------*) Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> 0"; -by (res_inst_tac [("z1","l")] ((real_add_minus RS subst)) 1); +by (res_inst_tac [("a1","l")] ((right_minus RS subst)) 1); by (rtac LIM_add_minus 1 THEN Auto_tac); qed "LIM_zero"; @@ -119,8 +114,7 @@ by (dres_inst_tac [("x","1")] spec 1); by (dres_inst_tac [("x","r")] spec 1); by (cut_facts_tac [real_zero_less_one] 1); -by (asm_full_simp_tac (simpset() addsimps - [abs_mult]) 1); +by (asm_full_simp_tac (simpset() addsimps [abs_mult]) 1); by (Clarify_tac 1); by (res_inst_tac [("R1.0","s"),("R2.0","sa")] real_linear_less2 1); @@ -193,7 +187,7 @@ \ abs(xa + -x) < inverse(real(Suc n)) & r \\ abs(f xa + -L)"; by (Clarify_tac 1); by (cut_inst_tac [("n1","n")] - (real_of_nat_Suc_gt_zero RS real_inverse_gt_0) 1); + (real_of_nat_Suc_gt_zero RS positive_imp_inverse_positive) 1); by Auto_tac; val lemma_LIM = result(); @@ -341,7 +335,7 @@ NSLIM_zero ------------------------------*) Goal "f -- a --NS> l ==> (%x. f(x) + -l) -- a --NS> 0"; -by (res_inst_tac [("z1","l")] ((real_add_minus RS subst)) 1); +by (res_inst_tac [("a1","l")] ((right_minus RS subst)) 1); by (rtac NSLIM_add_minus 1 THEN Auto_tac); qed "NSLIM_zero"; @@ -702,7 +696,7 @@ \ r \\ abs(f z + -f y)"; by (Clarify_tac 1); by (cut_inst_tac [("n1","n")] - (real_of_nat_Suc_gt_zero RS real_inverse_gt_0) 1); + (real_of_nat_Suc_gt_zero RS positive_imp_inverse_positive) 1); by Auto_tac; val lemma_LIMu = result(); @@ -980,7 +974,7 @@ by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def]) 1 THEN REPEAT (Step_tac 1)); by (auto_tac (claset(), - simpset() addsimps [hypreal_add_divide_distrib])); + simpset() addsimps [add_divide_distrib])); by (dres_inst_tac [("b","hypreal_of_real Da"), ("d","hypreal_of_real Db")] approx_add 1); by (auto_tac (claset(), simpset() addsimps add_ac)); @@ -1020,7 +1014,7 @@ by (REPEAT (Step_tac 1)); by (auto_tac (claset(), simpset() addsimps [starfun_lambda_cancel, lemma_nsderiv1])); -by (simp_tac (simpset() addsimps [hypreal_add_divide_distrib]) 1); +by (simp_tac (simpset() addsimps [add_divide_distrib]) 1); by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1)); by (auto_tac (claset(), simpset() delsimps [times_divide_eq_right] @@ -1052,7 +1046,7 @@ \ ==> NSDERIV (%x. c * f x) x :> c*D"; by (asm_full_simp_tac (HOL_ss addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff, - real_minus_mult_eq2, real_add_mult_distrib2 RS sym]) 1); + minus_mult_right, right_distrib RS sym]) 1); by (etac (NSLIM_const RS NSLIM_mult) 1); qed "NSDERIV_cmult"; @@ -1064,7 +1058,7 @@ \ ==> DERIV (%x. c * f x) x :> c*D"; by (asm_full_simp_tac (HOL_ss addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff, - real_minus_mult_eq2, real_add_mult_distrib2 RS sym]) 1); + minus_mult_right, right_distrib RS sym]) 1); by (etac (LIM_const RS LIM_mult2) 1); qed "DERIV_cmult"; @@ -1295,7 +1289,7 @@ by (induct_tac "n" 1); by (dtac (DERIV_Id RS DERIV_mult) 2); by (auto_tac (claset(), - simpset() addsimps [real_of_nat_Suc, real_add_mult_distrib])); + simpset() addsimps [real_of_nat_Suc, left_distrib])); by (case_tac "0 < n" 1); by (dres_inst_tac [("x","x")] realpow_minus_mult 1); by (auto_tac (claset(), @@ -1354,7 +1348,7 @@ Goal "[| DERIV f x :> d; f(x) \\ 0 |] \ \ ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"; by (rtac (real_mult_commute RS subst) 1); -by (asm_simp_tac (HOL_ss addsimps [real_minus_mult_eq1, realpow_inverse]) 1); +by (asm_simp_tac (HOL_ss addsimps [minus_mult_left, realpow_inverse]) 1); by (fold_goals_tac [o_def]); by (blast_tac (claset() addSIs [DERIV_chain,DERIV_inverse]) 1); qed "DERIV_inverse_fun"; @@ -1374,10 +1368,9 @@ by (dtac DERIV_mult 2); by (REPEAT(assume_tac 1)); by (asm_full_simp_tac - (simpset() addsimps [real_divide_def, real_add_mult_distrib2, - realpow_inverse,real_minus_mult_eq1] @ real_mult_ac - delsimps [realpow_Suc, real_mult_minus_eq1, real_mult_minus_eq2, - minus_mult_right RS sym, minus_mult_left RS sym]) 1); + (simpset() addsimps [real_divide_def, right_distrib, + realpow_inverse,minus_mult_left] @ mult_ac + delsimps [realpow_Suc, minus_mult_right RS sym, minus_mult_left RS sym]) 1); qed "DERIV_quotient"; Goal "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \\ 0 |] \ @@ -1456,7 +1449,7 @@ qed "f_inc_g_dec_Beq_g"; Goal "[| \\n. f n \\ f (Suc n); convergent f |] ==> f n \\ lim f"; -by (rtac real_leI 1); +by (rtac (linorder_not_less RS iffD1) 1); by (auto_tac (claset(), simpset() addsimps [convergent_LIMSEQ_iff, LIMSEQ_iff, monoseq_Suc])); by (dtac real_less_sum_gt_zero 1); @@ -1551,7 +1544,7 @@ \ (b-a) / (2 ^ n)"; by (induct_tac "n" 1); by (auto_tac (claset(), - simpset() addsimps [eq_divide_2_times_iff, real_add_divide_distrib, + simpset() addsimps [eq_divide_2_times_iff, add_divide_distrib, Let_def, split_def])); by (auto_tac (claset(), simpset() addsimps (add_ac@[Bolzano_bisect_le, real_diff_def]))); @@ -1615,7 +1608,7 @@ order_le_less_trans 1); by (asm_simp_tac (simpset() addsimps [real_abs_def]) 1); by (rtac (real_sum_of_halves RS subst) 1); -by (rtac real_add_less_mono 1); +by (rtac add_strict_mono 1); by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [symmetric real_diff_def]))); qed "lemma_BOLZANO"; @@ -1708,7 +1701,7 @@ Addsimps [abs_real_of_nat_cancel]; Goal "~ abs(x) + (1::real) < x"; -by (rtac real_leD 1); +by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1); by (auto_tac (claset() addIs [abs_ge_self RS order_trans],simpset())); qed "abs_add_one_not_less_self"; Addsimps [abs_add_one_not_less_self]; @@ -1770,7 +1763,7 @@ by (rtac exI 1 THEN Auto_tac); by (REPEAT(dtac spec 1) THEN Auto_tac); by (dres_inst_tac [("x","x")] spec 1); -by (auto_tac (claset() addSIs [real_leI],simpset())); +by (auto_tac (claset() addSIs [(linorder_not_less RS iffD1)],simpset())); qed "isCont_has_Ub"; (*----------------------------------------------------------------------------*) @@ -1786,7 +1779,7 @@ by (Asm_full_simp_tac 1); by (rtac ccontr 1); by (subgoal_tac "\\x. a \\ x & x \\ b --> f x < M" 1 THEN Step_tac 1); -by (rtac ccontr 2 THEN dtac real_leI 2); +by (rtac ccontr 2 THEN dtac (linorder_not_less RS iffD1) 2); by (dres_inst_tac [("z","M")] real_le_anti_sym 2); by (REPEAT(Blast_tac 2)); by (subgoal_tac "\\x. a \\ x & x \\ b --> isCont (%x. inverse(M - f x)) x" 1); @@ -1806,16 +1799,16 @@ "\\x. a \\ x & x \\ b --> (%x. inverse(M - (f x))) x < (k + 1)" 1); by Safe_tac; by (res_inst_tac [("y","k")] order_le_less_trans 2); -by (asm_full_simp_tac (simpset() addsimps [real_zero_less_one]) 3); +by (asm_full_simp_tac (simpset() addsimps [zero_less_one]) 3); by (Asm_full_simp_tac 2); by (subgoal_tac "\\x. a \\ x & x \\ b --> \ \ inverse(k + 1) < inverse((%x. inverse(M - (f x))) x)" 1); by Safe_tac; -by (rtac real_inverse_less_swap 2); +by (rtac less_imp_inverse_less 2); by (ALLGOALS Asm_full_simp_tac); by (dres_inst_tac [("P", "%N. N ?Q N"), ("x","M - inverse(k + 1)")] spec 1); -by (Step_tac 1 THEN dtac real_leI 1); +by (Step_tac 1 THEN dtac (linorder_not_less RS iffD1) 1); by (dtac (le_diff_eq RS iffD1) 1); by (REPEAT(dres_inst_tac [("x","a")] spec 1)); by (Asm_full_simp_tac 1); @@ -2047,10 +2040,8 @@ by (asm_full_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1); by (res_inst_tac [("c1","b - a")] (real_mult_left_cancel RS iffD1) 1); by (arith_tac 1); -by (auto_tac (claset(), - simpset() addsimps [real_diff_mult_distrib2])); -by (auto_tac (claset(), - simpset() addsimps [real_diff_mult_distrib])); +by (auto_tac (claset(), simpset() addsimps [right_diff_distrib])); +by (auto_tac (claset(), simpset() addsimps [left_diff_distrib])); qed "lemma_MVT"; Goal "[| a < b; \ @@ -2134,7 +2125,7 @@ by (auto_tac (claset() addDs [DERIV_isCont,DERIV_unique],simpset() addsimps [differentiable_def])); by (auto_tac (claset() addDs [DERIV_unique], - simpset() addsimps [real_add_mult_distrib, real_diff_def])); + simpset() addsimps [left_distrib, real_diff_def])); qed "DERIV_const_ratio_const"; Goal "[|a \\ b; \\x. DERIV f x :> k |] ==> (f(b) - f(a))/(b - a) = k"; diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/Log.ML --- a/src/HOL/Hyperreal/Log.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/Log.ML Thu Jan 01 10:06:32 2004 +0100 @@ -25,7 +25,7 @@ Goalw [powr_def] "[| 0 < x; 0 < y |] ==> (x * y) powr a = (x powr a) * (y powr a)"; by (asm_simp_tac (simpset() addsimps [exp_add RS sym,ln_mult, - real_add_mult_distrib2]) 1); + right_distrib]) 1); qed "powr_mult"; Goalw [powr_def] "0 < x powr a"; @@ -39,19 +39,18 @@ Addsimps [powr_not_zero]; Goal "[| 0 < x; 0 < y |] ==> (x / y) powr a = (x powr a)/(y powr a)"; -by (asm_simp_tac (simpset() addsimps [real_divide_def,real_inverse_gt_0, - powr_mult]) 1); +by (asm_simp_tac (simpset() addsimps [real_divide_def,positive_imp_inverse_positive, powr_mult]) 1); by (asm_simp_tac (simpset() addsimps [powr_def,exp_minus RS sym, exp_add RS sym,ln_inverse]) 1); qed "powr_divide"; Goalw [powr_def] "x powr (a + b) = (x powr a) * (x powr b)"; by (asm_simp_tac (simpset() addsimps [exp_add RS sym, - real_add_mult_distrib]) 1); + left_distrib]) 1); qed "powr_add"; Goalw [powr_def] "(x powr a) powr b = x powr (a * b)"; -by (simp_tac (simpset() addsimps real_mult_ac) 1); +by (simp_tac (simpset() addsimps mult_ac) 1); qed "powr_powr"; Goal "(x powr a) powr b = (x powr b) powr a"; @@ -108,7 +107,7 @@ "[| 0 < a; a ~= 1; 0 < x; 0 < y |] \ \ ==> log a (x * y) = log a x + log a y"; by (auto_tac (claset(),simpset() addsimps [ln_mult,real_divide_def, - real_add_mult_distrib])); + left_distrib])); qed "log_mult"; Goalw [log_def,real_divide_def] @@ -138,7 +137,7 @@ Addsimps [log_eq_one]; Goal "[| 0 < a; a ~= 1; 0 < x |] ==> log a (inverse x) = - log a x"; -by (res_inst_tac [("x1","log a x")] (real_add_left_cancel RS iffD1) 1); +by (res_inst_tac [("a1","log a x")] (add_left_cancel RS iffD1) 1); by (auto_tac (claset(),simpset() addsimps [log_mult RS sym])); qed "log_inverse"; diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/MacLaurin.ML --- a/src/HOL/Hyperreal/MacLaurin.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/MacLaurin.ML Thu Jan 01 10:06:32 2004 +0100 @@ -101,9 +101,9 @@ by (rtac DERIV_quotient 3); by (rtac DERIV_const 4); by (rtac DERIV_pow 3); -by (asm_simp_tac (simpset() addsimps [real_inverse_distrib, +by (asm_simp_tac (simpset() addsimps [inverse_mult_distrib, CLAIM_SIMP "(a::real) * b * c * (d * e) = a * b * (c * d) * e" - real_mult_ac,fact_diff_Suc]) 4); + mult_ac,fact_diff_Suc]) 4); by (Asm_simp_tac 3); by (forw_inst_tac [("m","ma")] less_add_one 2); by (Clarify_tac 2); @@ -126,8 +126,8 @@ by DERIV_tac; by (stac fact_Suc 2); by (stac real_of_nat_mult 2); -by (simp_tac (simpset() addsimps [real_inverse_distrib] @ - real_mult_ac) 2); +by (simp_tac (simpset() addsimps [inverse_mult_distrib] @ + mult_ac) 2); by (subgoal_tac "ALL ma. ma < n --> \ \ (EX t. 0 < t & t < h & difg (Suc ma) t = 0)" 1); by (rotate_tac 11 1); @@ -267,7 +267,7 @@ ("h","-h"),("n","n")] Maclaurin_objl 1); by (Asm_full_simp_tac 1); by (etac impE 1 THEN Step_tac 1); -by (stac real_minus_mult_eq2 1); +by (stac minus_mult_right 1); by (rtac DERIV_cmult 1); by (rtac lemma_DERIV_subst 1); by (rtac (read_instantiate [("g","uminus")] DERIV_chain2) 1); @@ -446,7 +446,7 @@ qed "lemma_exhaust_less_4"; bind_thm ("real_mult_le_lemma", - simplify (simpset()) (inst "y" "1" real_mult_le_le_mono2)); + simplify (simpset()) (inst "b" "1" mult_right_mono)); Goal "abs(sin x - \ @@ -489,7 +489,7 @@ by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2,real_divide_def]) 1); by (dtac lemma_odd_mod_4_div_2 1); by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2, real_divide_def]) 1); -by (auto_tac (claset() addSIs [real_mult_le_lemma,real_mult_le_le_mono2], +by (auto_tac (claset() addSIs [real_mult_le_lemma,mult_right_mono], simpset() addsimps [real_divide_def,abs_mult,abs_inverse,realpow_abs RS sym])); qed "Maclaurin_sin_bound"; @@ -660,7 +660,7 @@ by (rtac sumr_fun_eq 1); by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym])); by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex, - even_mult_two_ex,real_add_mult_distrib,cos_add] delsimps + even_mult_two_ex,left_distrib,cos_add] delsimps [fact_Suc,realpow_Suc])); by (auto_tac (claset(),simpset() addsimps [real_mult_commute])); qed "Maclaurin_cos_expansion"; @@ -687,7 +687,7 @@ by (rtac sumr_fun_eq 1); by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym])); by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex, - even_mult_two_ex,real_add_mult_distrib,cos_add] delsimps + even_mult_two_ex,left_distrib,cos_add] delsimps [fact_Suc,realpow_Suc])); by (auto_tac (claset(),simpset() addsimps [real_mult_commute])); qed "Maclaurin_cos_expansion2"; @@ -714,7 +714,7 @@ by (rtac sumr_fun_eq 1); by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym])); by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex, - even_mult_two_ex,real_add_mult_distrib,cos_add] delsimps + even_mult_two_ex,left_distrib,cos_add] delsimps [fact_Suc,realpow_Suc])); by (auto_tac (claset(),simpset() addsimps [real_mult_commute])); qed "Maclaurin_minus_cos_expansion"; diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/NSA.ML --- a/src/HOL/Hyperreal/NSA.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/NSA.ML Thu Jan 01 10:06:32 2004 +0100 @@ -347,8 +347,8 @@ "x: HInfinite ==> inverse x: Infinitesimal"; by Auto_tac; by (eres_inst_tac [("x","inverse r")] ballE 1); -by (forw_inst_tac [("x1","r"),("z","abs x")] - (hypreal_inverse_gt_0 RS order_less_trans) 1); +by (forw_inst_tac [("a1","r"),("z","abs x")] + (positive_imp_inverse_positive RS order_less_trans) 1); by (assume_tac 1); by (dtac ((inverse_inverse_eq RS sym) RS subst) 1); by (rtac (inverse_less_iff_less RS iffD1) 1); @@ -457,8 +457,8 @@ by (eres_inst_tac [("x","r*ra")] ballE 1); by (fast_tac (claset() addIs [SReal_mult]) 2); by (auto_tac (claset(), simpset() addsimps [zero_less_mult_iff])); -by (cut_inst_tac [("x","ra"),("y","abs y"), - ("u","r"),("v","abs x")] hypreal_mult_le_mono 1); +by (cut_inst_tac [("c","ra"),("d","abs y"), + ("a","r"),("b","abs x")] mult_mono 1); by Auto_tac; qed "not_Infinitesimal_mult"; @@ -1514,7 +1514,7 @@ "[| u: Infinitesimal; hypreal_of_real x + u <= hypreal_of_real y |] \ \ ==> hypreal_of_real x <= hypreal_of_real y"; by (EVERY1 [rtac notI, rtac contrapos_np, assume_tac]); -by (res_inst_tac [("C","-u")] hypreal_less_add_right_cancel 1); +by (res_inst_tac [("c1","-u")] (add_less_cancel_right RS iffD1) 1); by (Asm_full_simp_tac 1); by (dtac (Infinitesimal_minus_iff RS iffD2) 1); by (dtac Infinitesimal_add_hypreal_of_real_less 1); @@ -1560,16 +1560,16 @@ Goal "x*x + y*y : Infinitesimal ==> x*x : Infinitesimal"; by (rtac Infinitesimal_interval2 1); -by (rtac hypreal_le_square 3); +by (rtac zero_le_square 3); by (assume_tac 1); -by Auto_tac; +by (auto_tac (claset(), simpset() addsimps [zero_le_square])); qed "Infinitesimal_square_cancel"; Addsimps [Infinitesimal_square_cancel]; Goal "x*x + y*y : HFinite ==> x*x : HFinite"; by (rtac HFinite_bounded 1); by (assume_tac 1); -by Auto_tac; +by (auto_tac (claset(), simpset() addsimps [zero_le_square])); qed "HFinite_square_cancel"; Addsimps [HFinite_square_cancel]; @@ -1590,7 +1590,7 @@ Goal "x*x + y*y + z*z : Infinitesimal ==> x*x : Infinitesimal"; by (rtac Infinitesimal_interval2 1); by (assume_tac 1); -by (rtac hypreal_le_square 2); +by (rtac zero_le_square 2); by (Asm_full_simp_tac 1); by (cut_inst_tac [("a","y")] (thm"zero_le_square") 1); by (cut_inst_tac [("a","z")] (thm"zero_le_square") 1); @@ -1601,7 +1601,7 @@ Goal "x*x + y*y + z*z : HFinite ==> x*x : HFinite"; by (rtac HFinite_bounded 1); by (assume_tac 1); -by (rtac hypreal_le_square 2); +by (rtac zero_le_square 2); by (cut_inst_tac [("a","y")] (thm"zero_le_square") 1); by (cut_inst_tac [("a","z")] (thm"zero_le_square") 1); by (asm_simp_tac (simpset() addsimps []) 1); @@ -2073,7 +2073,7 @@ by (dres_inst_tac [("x","inverse (hypreal_of_real(real (Suc n)))")] bspec 1); by (full_simp_tac (simpset() addsimps [SReal_inverse]) 1); -by (rtac (real_of_nat_Suc_gt_zero RS real_inverse_gt_0 RS +by (rtac (real_of_nat_Suc_gt_zero RS positive_imp_inverse_positive RS (hypreal_of_real_less_iff RS iffD2) RSN(2,impE)) 1); by (assume_tac 2); by (asm_full_simp_tac (simpset() addsimps @@ -2156,7 +2156,7 @@ --------------------------------------------------------------*) Goal "- {n::nat. real n <= u} = {n. u < real n}"; by (auto_tac (claset() addSDs [order_le_less_trans], - simpset() addsimps [not_real_leE])); + simpset() addsimps [linorder_not_le])); val lemma = result(); (*----------------------------------------------- @@ -2274,7 +2274,7 @@ Goal "- {n. u <= inverse(real(Suc n))} = \ \ {n. inverse(real(Suc n)) < u}"; by (auto_tac (claset() addSDs [order_le_less_trans], - simpset() addsimps [not_real_leE])); + simpset() addsimps [linorder_not_le])); val lemma = result(); Goal "0 < u ==> \ diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/NthRoot.thy --- a/src/HOL/Hyperreal/NthRoot.thy Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/NthRoot.thy Thu Jan 01 10:06:32 2004 +0100 @@ -18,9 +18,9 @@ "[| (0::real) < a; 0 < n |] ==> \s. s : {x. x ^ n <= a & 0 < x}" apply (case_tac "1 <= a") apply (rule_tac x = "1" in exI) -apply (drule_tac [2] not_real_leE) +apply (drule_tac [2] linorder_not_le [THEN iffD1]) apply (drule_tac [2] less_not_refl2 [THEN not0_implies_Suc]) -apply (auto intro!: realpow_Suc_le_self simp add: real_zero_less_one) +apply (auto intro!: realpow_Suc_le_self simp add: zero_less_one) done lemma lemma_nth_realpow_isUb_ex: @@ -28,20 +28,20 @@ ==> \u. isUb (UNIV::real set) {x. x ^ n <= a & 0 < x} u" apply (case_tac "1 <= a") apply (rule_tac x = "a" in exI) -apply (drule_tac [2] not_real_leE) +apply (drule_tac [2] linorder_not_le [THEN iffD1]) apply (rule_tac [2] x = "1" in exI) apply (rule_tac [!] setleI [THEN isUbI]) apply safe apply (simp_all (no_asm)) apply (rule_tac [!] ccontr) -apply (drule_tac [!] not_real_leE) +apply (drule_tac [!] linorder_not_le [THEN iffD1]) apply (drule realpow_ge_self2 , assumption) apply (drule_tac n = "n" in realpow_less) apply (assumption+) apply (drule real_le_trans , assumption) apply (drule_tac y = "y ^ n" in order_less_le_trans) apply (assumption , erule real_less_irrefl) -apply (drule_tac n = "n" in real_zero_less_one [THEN realpow_less]) +apply (drule_tac n = "n" in zero_less_one [THEN realpow_less]) apply auto done @@ -86,7 +86,7 @@ {x. x ^ n <= a & 0 < x} u |] ==> a <= u ^ n" apply (frule lemma_nth_realpow_isLub_ge , safe) apply (rule LIMSEQ_inverse_real_of_nat_add [THEN LIMSEQ_pow, THEN LIMSEQ_le_const]) -apply (auto simp add: real_of_nat_def real_of_posnat_Suc) +apply (auto simp add: real_of_nat_def) done subsection{*Second Half*} @@ -109,15 +109,16 @@ done lemma real_mult_less_self: "0 < r ==> r * (1 + -inverse(real (Suc n))) < r" -apply (simp (no_asm) add: real_add_mult_distrib2) -apply (rule_tac C = "-r" in real_less_add_left_cancel) -apply (auto intro: real_mult_order simp add: real_add_assoc [symmetric] real_minus_zero_less_iff2) +apply (simp (no_asm) add: right_distrib) +apply (rule add_less_cancel_left [of "-r", THEN iffD1]) +apply (auto intro: mult_pos + simp add: add_assoc [symmetric] neg_less_0_iff_less) done lemma real_mult_add_one_minus_ge_zero: "0 < r ==> 0 <= r*(1 + -inverse(real (Suc n)))" apply (simp add: zero_le_mult_iff real_of_nat_inverse_le_iff) -apply (simp add: RealOrd.real_of_nat_Suc) +apply (simp add: real_of_nat_Suc) done lemma lemma_nth_realpow_isLub_le: @@ -141,7 +142,7 @@ {x. x ^ n <= a & 0 < x} u |] ==> u ^ n <= a" apply (frule lemma_nth_realpow_isLub_le , safe) apply (rule LIMSEQ_inverse_real_of_nat_add_minus_mult [THEN LIMSEQ_pow, THEN LIMSEQ_le_const2]) -apply (auto simp add: real_of_nat_def real_of_posnat_Suc) +apply (auto simp add: real_of_nat_def) done (*----------- The theorem at last! -----------*) diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/Poly.ML --- a/src/HOL/Hyperreal/Poly.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/Poly.ML Thu Jan 01 10:06:32 2004 +0100 @@ -68,7 +68,7 @@ by (rtac allI 2 ); by (case_tac "q" 2); by (Asm_simp_tac 2); -by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib2] ) 2); +by (asm_simp_tac (simpset() addsimps [right_distrib] ) 2); by (Asm_simp_tac 1); qed "poly_cmult_distr"; @@ -92,14 +92,14 @@ by (induct_tac "p1" 2); by Auto_tac; by (case_tac "p2" 1); -by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2])); +by (auto_tac (claset(),simpset() addsimps [right_distrib])); qed "poly_add"; Goal "poly (c %* p) x = c * poly p x"; by (induct_tac "p" 1); by (case_tac "x=0" 2); -by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2] - @ real_mult_ac)); +by (auto_tac (claset(),simpset() addsimps [right_distrib] + @ mult_ac)); qed "poly_cmult"; Goalw [poly_minus_def] "poly (-- p) x = - (poly p x)"; @@ -113,7 +113,7 @@ by (auto_tac (claset(),simpset() addsimps [poly_cmult])); by (case_tac "list" 1); by (auto_tac (claset(),simpset() addsimps [poly_cmult,poly_add, - real_add_mult_distrib,real_add_mult_distrib2] @ real_mult_ac)); + left_distrib,right_distrib] @ mult_ac)); qed "poly_mult"; Goal "poly (p %^ n) x = (poly p x) ^ n"; @@ -178,7 +178,7 @@ \ x ^ n * poly (pderiv_aux (Suc n) p) x "; by (induct_tac "p" 1); by (auto_tac (claset() addSIs [DERIV_add,DERIV_cmult2],simpset() addsimps - [pderiv_def,real_add_mult_distrib2,real_mult_assoc RS sym] delsimps + [pderiv_def,right_distrib,real_mult_assoc RS sym] delsimps [realpow_Suc])); by (rtac (real_mult_commute RS subst) 1); by (simp_tac (simpset() delsimps [realpow_Suc]) 1); @@ -232,7 +232,7 @@ Goal "[| a < b; 0 < poly p a; poly p b < 0 |] \ \ ==> EX x. a < x & x < b & (poly p x = 0)"; by (blast_tac (claset() addIs [full_simplify (simpset() - addsimps [poly_minus, rename_numerals real_minus_zero_less_iff2]) + addsimps [poly_minus, rename_numerals neg_less_0_iff_less]) (read_instantiate [("p","-- p")] poly_IVT_pos)]) 1); qed "poly_IVT_neg"; @@ -256,7 +256,7 @@ by (induct_tac "p1" 1); by (Step_tac 2); by (case_tac "p2" 2); -by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2])); +by (auto_tac (claset(),simpset() addsimps [right_distrib])); qed "lemma_poly_pderiv_aux_add"; Goal "poly (pderiv_aux n (p1 +++ p2)) x = \ @@ -266,7 +266,7 @@ Goal "ALL n. poly (pderiv_aux n (c %* p) ) x = poly (c %* pderiv_aux n p) x"; by (induct_tac "p" 1); -by (auto_tac (claset(),simpset() addsimps [poly_cmult] @ real_mult_ac)); +by (auto_tac (claset(),simpset() addsimps [poly_cmult] @ mult_ac)); qed "lemma_poly_pderiv_aux_cmult"; Goal "poly (pderiv_aux n (c %* p) ) x = poly (c %* pderiv_aux n p) x"; @@ -281,7 +281,7 @@ Goal "ALL n. poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x"; by (induct_tac "p" 1); by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc, - real_add_mult_distrib])); + left_distrib])); qed "lemma_poly_pderiv_aux_mult1"; Goal "poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x"; @@ -326,8 +326,8 @@ by (rtac (lemma_poly_mult_pderiv RS ssubst) 1); by (rtac (poly_add RS ssubst) 1); by (rtac (poly_add RS ssubst) 1); -by (asm_simp_tac (simpset() addsimps [poly_mult,real_add_mult_distrib2] - @ real_add_ac @ real_mult_ac) 1); +by (asm_simp_tac (simpset() addsimps [poly_mult,right_distrib] + @ add_ac @ mult_ac) 1); qed "poly_pderiv_mult"; Goal "poly (pderiv (p %^ (Suc n))) x = \ @@ -335,8 +335,8 @@ by (induct_tac "n" 1); by (auto_tac (claset(),simpset() addsimps [poly_add,poly_pderiv_cmult, poly_cmult,poly_pderiv_mult,real_of_nat_zero,poly_mult, - real_of_nat_Suc,real_add_mult_distrib2,real_add_mult_distrib] - @ real_mult_ac)); + real_of_nat_Suc,right_distrib,left_distrib] + @ mult_ac)); qed "poly_pderiv_exp"; Goal "poly (pderiv ([-a, 1] %^ (Suc n))) x = \ @@ -372,7 +372,7 @@ Goal "(poly p a = 0) = ((p = []) | (EX q. p = [-a, 1] *** q))"; by (auto_tac (claset(),simpset() addsimps [poly_add,poly_cmult, - real_add_mult_distrib2])); + right_distrib])); by (case_tac "p" 1); by (cut_inst_tac [("h","aa"),("t","list"),("a","a")] poly_linear_rem 2); by (Step_tac 2); @@ -439,8 +439,7 @@ Goal "(poly (p *** q) x ~= poly [] x) = \ \ (poly p x ~= poly [] x & poly q x ~= poly [] x)"; -by (auto_tac (claset(),simpset() addsimps [poly_mult,rename_numerals - real_mult_not_zero])); +by (auto_tac (claset(),simpset() addsimps [poly_mult])); qed "poly_mult_not_eq_poly_Nil"; Addsimps [poly_mult_not_eq_poly_Nil]; @@ -571,7 +570,7 @@ Goal "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"; by (auto_tac (claset(),simpset() addsimps [poly_add,poly_minus_def, - fun_eq,poly_mult,poly_cmult,real_add_mult_distrib2])); + fun_eq,poly_mult,poly_cmult,right_distrib])); qed "poly_add_minus_mult_eq"; Goal "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)"; @@ -686,14 +685,14 @@ Goal "([a, 1] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)"; by (auto_tac (claset(),simpset() addsimps [divides_def,fun_eq,poly_mult, - poly_add,poly_cmult,real_add_mult_distrib RS sym])); + poly_add,poly_cmult,left_distrib RS sym])); by (dres_inst_tac [("x","-a")] spec 1); by (auto_tac (claset(),simpset() addsimps [poly_linear_divides,poly_add, - poly_cmult,real_add_mult_distrib RS sym])); + poly_cmult,left_distrib RS sym])); by (res_inst_tac [("x","qa *** q")] exI 1); by (res_inst_tac [("x","p *** qa")] exI 2); by (auto_tac (claset(),simpset() addsimps [poly_add,poly_mult, - poly_cmult] @ real_mult_ac)); + poly_cmult] @ mult_ac)); qed "poly_primes"; Goalw [divides_def] "p divides p"; @@ -721,7 +720,7 @@ by (auto_tac (claset(),simpset() addsimps [divides_def])); by (res_inst_tac [("x","p")] exI 1); by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq] - @ real_mult_ac)); + @ mult_ac)); qed "poly_divides_exp"; Goal "[| (p %^ n) divides q; m <= n |] ==> (p %^ m) divides q"; @@ -733,7 +732,7 @@ by Auto_tac; by (res_inst_tac [("x","qa +++ qaa")] exI 1); by (auto_tac (claset(),simpset() addsimps [poly_add,fun_eq,poly_mult, - real_add_mult_distrib2])); + right_distrib])); qed "poly_divides_add"; Goalw [divides_def] @@ -741,14 +740,14 @@ by Auto_tac; by (res_inst_tac [("x","qaa +++ -- qa")] exI 1); by (auto_tac (claset(),simpset() addsimps [poly_add,fun_eq,poly_mult, - poly_minus,real_add_mult_distrib2, + poly_minus,right_distrib, ARITH_PROVE "(x = y + -z) = (z + x = (y::real))"])); qed "poly_divides_diff"; Goal "[| p divides r; p divides (q +++ r) |] ==> p divides q"; by (etac poly_divides_diff 1); by (auto_tac (claset(),simpset() addsimps [poly_add,fun_eq,poly_mult, - divides_def] @ real_add_ac)); + divides_def] @ add_ac)); qed "poly_divides_diff2"; Goalw [divides_def] "poly p = poly [] ==> q divides p"; @@ -793,7 +792,7 @@ by (induct_tac "n" 1); by (Simp_tac 1); by (asm_simp_tac (simpset() addsimps [poly_add,poly_cmult,poly_mult, - real_add_mult_distrib2] @ real_mult_ac) 1); + right_distrib] @ mult_ac) 1); by (Step_tac 1); by (rotate_tac 2 1); by (rtac swap 1 THEN assume_tac 2); @@ -916,7 +915,7 @@ by (Step_tac 1); by (dres_inst_tac [("x","qa")] spec 1); by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq,poly_exp] - @ real_mult_ac delsimps [pmult_Cons])); + @ mult_ac delsimps [pmult_Cons])); qed "order_decomp"; (* ------------------------------------------------------------------------- *) @@ -934,7 +933,7 @@ poly_mult] delsimps [pmult_Cons]) 1); by (Step_tac 1); by (res_inst_tac [("x","qa *** qaa")] exI 1); -by (asm_full_simp_tac (simpset() addsimps [poly_mult] @ real_mult_ac +by (asm_full_simp_tac (simpset() addsimps [poly_mult] @ mult_ac delsimps [pmult_Cons]) 1); by (REPEAT(dres_inst_tac [("a","a")] order_decomp 1)); by (Step_tac 1); @@ -955,7 +954,7 @@ by (dtac (poly_mult_left_cancel RS iffD1) 1); by (Force_tac 1); by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_exp_add,poly_mult] - @ real_mult_ac delsimps [pmult_Cons]) 1); + @ mult_ac delsimps [pmult_Cons]) 1); qed "order_mult"; (* FIXME: too too long! *) @@ -980,10 +979,10 @@ [("x","[-a, 1] *** (pderiv q) +++ real (Suc n) %* q")] exI 1); by (asm_full_simp_tac (simpset() addsimps [poly_pderiv_mult, poly_pderiv_exp_prime,poly_add,poly_mult,poly_cmult, - real_add_mult_distrib2] @ real_mult_ac + right_distrib] @ mult_ac delsimps [pmult_Cons,pexp_Suc]) 1); -by (asm_full_simp_tac (simpset() addsimps [poly_mult,real_add_mult_distrib2, - real_add_mult_distrib] @ real_mult_ac delsimps [pmult_Cons]) 1); +by (asm_full_simp_tac (simpset() addsimps [poly_mult,right_distrib, + left_distrib] @ mult_ac delsimps [pmult_Cons]) 1); by (thin_tac "ALL r. \ \ r divides pderiv p = \ \ r divides pderiv ([- a, 1] %^ Suc n *** q)" 1); @@ -1010,11 +1009,11 @@ by (Simp_tac 1); by (rtac ((CLAIM_SIMP "a * (b * (c * (d * e))) = e * (b * (c * (d * (a::real))))" - real_mult_ac) RS ssubst) 1); + mult_ac) RS ssubst) 1); by (rotate_tac 2 1); by (dres_inst_tac [("x","xa")] spec 1); by (asm_full_simp_tac (simpset() - addsimps [real_add_mult_distrib] @ real_mult_ac + addsimps [left_distrib] @ mult_ac delsimps [pmult_Cons]) 1); qed_spec_mp "lemma_order_pderiv"; @@ -1063,7 +1062,7 @@ by (Step_tac 2); by (res_inst_tac [("x","r *** qa +++ s *** qaa")] exI 2); by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_add,poly_mult, - real_add_mult_distrib, real_add_mult_distrib2] @ real_mult_ac + left_distrib, right_distrib] @ mult_ac delsimps [pexp_Suc,pmult_Cons]) 2); by Auto_tac; qed "poly_squarefree_decomp_order"; @@ -1199,7 +1198,7 @@ by Auto_tac; by (res_inst_tac [("j","abs a + abs(x * poly list x)")] real_le_trans 1); by (rtac abs_triangle_ineq 1); -by (auto_tac (claset() addSIs [real_mult_le_mono],simpset() +by (auto_tac (claset() addSIs [mult_mono],simpset() addsimps [abs_mult])); by (arith_tac 1); qed_spec_mp "poly_mono"; diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/SEQ.ML --- a/src/HOL/Hyperreal/SEQ.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/SEQ.ML Thu Jan 01 10:06:32 2004 +0100 @@ -914,7 +914,7 @@ ---------------------------------------------------------*) Goalw [Cauchy_def,Bseq_def] "Cauchy X ==> Bseq X"; by (dres_inst_tac [("x","1")] spec 1); -by (etac (real_zero_less_one RSN (2,impE)) 1); +by (etac (zero_less_one RSN (2,impE)) 1); by (Step_tac 1); by (dres_inst_tac [("x","M")] spec 1); by (Asm_full_simp_tac 1); @@ -1126,9 +1126,9 @@ by (dres_inst_tac [("x","inverse r")] spec 1 THEN Step_tac 1); by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1); by (dtac spec 1 THEN Auto_tac); -by (ftac real_inverse_gt_0 1); +by (ftac positive_imp_inverse_positive 1); by (ftac order_less_trans 1 THEN assume_tac 1); -by (forw_inst_tac [("x","f n")] real_inverse_gt_0 1); +by (forw_inst_tac [("a","f n")] positive_imp_inverse_positive 1); by (asm_simp_tac (simpset() addsimps [abs_eqI2]) 1); by (res_inst_tac [("t","r")] (inverse_inverse_eq RS subst) 1); by (auto_tac (claset() addIs [inverse_less_iff_less RS iffD2], diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/Series.ML --- a/src/HOL/Hyperreal/Series.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/Series.ML Thu Jan 01 10:06:32 2004 +0100 @@ -30,14 +30,14 @@ Goal "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)"; by (induct_tac "n" 1); -by (auto_tac (claset(),simpset() addsimps real_add_ac)); +by (auto_tac (claset(),simpset() addsimps add_ac)); qed "sumr_add"; Goal "r * sumr m n f = sumr m n (%n. r * f n)"; by (induct_tac "n" 1); by (Auto_tac); by (auto_tac (claset(),simpset() addsimps - [real_add_mult_distrib2])); + [right_distrib])); qed "sumr_mult"; Goal "n < p --> sumr 0 n f + sumr n p f = sumr 0 p f"; @@ -49,7 +49,7 @@ Goal "n < p ==> sumr 0 p f + \ \ - sumr 0 n f = sumr n p f"; by (dres_inst_tac [("f1","f")] (sumr_split_add RS sym) 1); -by (asm_simp_tac (simpset() addsimps real_add_ac) 1); +by (asm_simp_tac (simpset() addsimps add_ac) 1); qed "sumr_split_add_minus"; Goal "0 < n --> n < p --> sumr (Suc 0) n f + sumr n p f = sumr (Suc 0) p f"; @@ -66,7 +66,7 @@ Goal "abs(sumr m n f) <= sumr m n (%i. abs(f i))"; by (induct_tac "n" 1); by (auto_tac (claset() addIs [abs_triangle_ineq RS order_trans, - real_add_le_mono1], + add_right_mono], simpset())); qed "sumr_rabs"; @@ -79,13 +79,13 @@ Goal "sumr 0 n (%i. r) = real n * r"; by (induct_tac "n" 1); by (auto_tac (claset(), - simpset() addsimps [real_add_mult_distrib,real_of_nat_zero, + simpset() addsimps [left_distrib,real_of_nat_zero, real_of_nat_Suc])); qed "sumr_const"; Addsimps [sumr_const]; Goal "sumr 0 n f + -(real n * r) = sumr 0 n (%i. f i + -r)"; -by (full_simp_tac (HOL_ss addsimps [sumr_add RS sym, real_minus_mult_eq2]) 1); +by (full_simp_tac (HOL_ss addsimps [sumr_add RS sym, minus_mult_right]) 1); by (Simp_tac 1); qed "sumr_add_mult_const"; @@ -103,8 +103,7 @@ Goal "sumr m n (%i. - f i) = - sumr m n f"; by (induct_tac "n" 1); by (case_tac "Suc n <= m" 2); -by (auto_tac (claset(),simpset() addsimps - [real_minus_add_distrib])); +by (auto_tac (claset(),simpset() addsimps [minus_add_distrib])); qed "sumr_minus"; Goal "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"; @@ -131,7 +130,7 @@ by (Step_tac 1); by (dres_inst_tac [("x","n")] spec 3); by (auto_tac (claset() addSDs [le_imp_less_or_eq], simpset())); -by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib, Suc_diff_n, +by (asm_simp_tac (simpset() addsimps [left_distrib, Suc_diff_n, real_of_nat_Suc]) 1); qed_spec_mp "sumr_interval_const"; @@ -144,7 +143,7 @@ by (dres_inst_tac [("x","n")] spec 3); by (auto_tac (claset() addSDs [le_imp_less_or_eq], simpset())); -by (asm_simp_tac (simpset() addsimps [Suc_diff_n, real_add_mult_distrib, +by (asm_simp_tac (simpset() addsimps [Suc_diff_n, left_distrib, real_of_nat_Suc]) 1); qed_spec_mp "sumr_interval_const2"; @@ -155,15 +154,15 @@ by (ALLGOALS(dres_inst_tac [("x","n")] spec)); by (Step_tac 1); by (dtac le_imp_less_or_eq 1 THEN Step_tac 1); -by (dtac real_add_le_mono 2); -by (dres_inst_tac [("i","sumr 0 m f")] (order_refl RS real_add_le_mono) 1); +by (dres_inst_tac [("a","sumr 0 m f")] add_mono 2); +by (dres_inst_tac [("a","sumr 0 m f")] (order_refl RS add_mono) 1); by (Auto_tac); qed_spec_mp "sumr_le"; Goal "!!f g. (ALL r. m <= r & r < n --> f r <= g r) \ \ --> sumr m n f <= sumr m n g"; by (induct_tac "n" 1); -by (auto_tac (claset() addIs [real_add_le_mono], +by (auto_tac (claset() addIs [add_mono], simpset() addsimps [le_def])); qed_spec_mp "sumr_le2"; @@ -228,15 +227,15 @@ Goal "(ALL p. m <= p & p < m + n --> (f(p) <= K)) \ \ --> (sumr m (m + n) f <= (real n * K))"; by (induct_tac "n" 1); -by (auto_tac (claset() addIs [real_add_le_mono], - simpset() addsimps [real_add_mult_distrib, real_of_nat_Suc])); +by (auto_tac (claset() addIs [add_mono], + simpset() addsimps [left_distrib, real_of_nat_Suc])); qed_spec_mp "sumr_bound"; Goal "(ALL p. 0 <= p & p < n --> (f(p) <= K)) \ \ --> (sumr 0 n f <= (real n * K))"; by (induct_tac "n" 1); -by (auto_tac (claset() addIs [real_add_le_mono], - simpset() addsimps [real_add_mult_distrib, real_of_nat_Suc])); +by (auto_tac (claset() addIs [add_mono], + simpset() addsimps [left_distrib, real_of_nat_Suc])); qed_spec_mp "sumr_bound2"; Goal "sumr 0 n (%m. sumr (m * k) (m*k + k) f) = sumr 0 (n * k) f"; @@ -358,7 +357,7 @@ by (auto_tac (claset(),simpset() addsimps [sums_def,LIMSEQ_def])); by (dres_inst_tac [("x","f(n) + f(n + 1)")] spec 1); by (Auto_tac); -by (rtac ccontr 2 THEN dtac real_leI 2); +by (rtac ccontr 2 THEN dtac (linorder_not_less RS iffD1) 2); by (subgoal_tac "sumr 0 (n + Suc (Suc 0)) f <= sumr 0 (Suc (Suc 0) * (Suc no) + n) f" 2); by (induct_tac "no" 3 THEN Simp_tac 3); by (res_inst_tac [("y","sumr 0 (Suc (Suc 0)*(Suc na)+n) f")] order_trans 3); @@ -419,9 +418,9 @@ by (Auto_tac); by (res_inst_tac [("c1","x - 1")] (real_mult_right_cancel RS iffD1) 1); by (auto_tac (claset(), - simpset() addsimps [real_mult_assoc, real_add_mult_distrib])); + simpset() addsimps [real_mult_assoc, left_distrib])); by (auto_tac (claset(), - simpset() addsimps [real_add_mult_distrib2, + simpset() addsimps [right_distrib, real_diff_def, real_mult_commute])); qed "sumr_geometric"; @@ -429,7 +428,7 @@ by (case_tac "x = 1" 1); by (auto_tac (claset() addSDs [LIMSEQ_rabs_realpow_zero2], simpset() addsimps [sumr_geometric ,sums_def, - real_diff_def, real_add_divide_distrib])); + real_diff_def, add_divide_distrib])); by (subgoal_tac "1 / (1 + -x) = 0/(x - 1) + - 1/(x - 1)" 1); by (asm_full_simp_tac (simpset() addsimps [thm"minus_divide_right"]) 2); by (etac ssubst 1); @@ -542,7 +541,7 @@ by Auto_tac; by (subgoal_tac "0 <= c * abs y" 1); by (arith_tac 2); -by (asm_full_simp_tac (simpset() addsimps [real_0_le_mult_iff]) 1); +by (asm_full_simp_tac (simpset() addsimps [zero_le_mult_iff]) 1); qed "rabs_ratiotest_lemma"; (* lemmas *) @@ -579,9 +578,9 @@ by (auto_tac (claset(),simpset() addsimps [realpow_add, realpow_not_zero])); by (induct_tac "na" 1 THEN Auto_tac); by (res_inst_tac [("y","c*abs(f(N + n))")] order_trans 1); -by (auto_tac (claset() addIs [real_mult_le_mono1], +by (auto_tac (claset() addIs [mult_right_mono], simpset() addsimps [summable_def])); -by (asm_full_simp_tac (simpset() addsimps real_mult_ac) 1); +by (asm_full_simp_tac (simpset() addsimps mult_ac) 1); by (res_inst_tac [("x","abs(f N) * (1/(1 - c)) / (c ^ N)")] exI 1); by (rtac sums_divide 1); by (rtac sums_mult 1); diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/Transcendental.ML --- a/src/HOL/Hyperreal/Transcendental.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/Transcendental.ML Thu Jan 01 10:06:32 2004 +0100 @@ -35,7 +35,7 @@ "0 < x ==> root(Suc n) (x ^ (Suc n)) = x"; by (rtac some_equality 1); by (forw_inst_tac [("n","n")] realpow_gt_zero 2); -by (auto_tac (claset(),simpset() addsimps [real_0_less_mult_iff])); +by (auto_tac (claset(),simpset() addsimps [zero_less_mult_iff])); by (res_inst_tac [("R1.0","u"),("R2.0","x")] real_linear_less2 1); by (dres_inst_tac [("n1","n"),("x","u")] (zero_less_Suc RSN (3, realpow_less)) 1); by (dres_inst_tac [("n1","n"),("x","x")] (zero_less_Suc RSN (3, realpow_less)) 4); @@ -52,7 +52,7 @@ by (dres_inst_tac [("n","n")] realpow_pos_nth2 1); by (Safe_tac THEN rtac someI2 1); by (auto_tac (claset() addSIs [order_less_imp_le] - addDs [realpow_gt_zero],simpset() addsimps [real_0_less_mult_iff])); + addDs [realpow_gt_zero],simpset() addsimps [zero_less_mult_iff])); qed "real_root_pos_pos"; Goal "0 <= x ==> 0 <= root(Suc n) x"; @@ -151,7 +151,7 @@ by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1); by Auto_tac; by (ftac (real_mult_order) 2); -by (asm_full_simp_tac (simpset() addsimps [real_0_less_mult_iff]) 1); +by (asm_full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 1); by Auto_tac; qed "not_real_square_gt_zero"; Addsimps [not_real_square_gt_zero]; @@ -171,7 +171,7 @@ by (Asm_full_simp_tac 1 THEN Asm_full_simp_tac 1); by (res_inst_tac [("a","xa * x")] someI2 1); by (auto_tac (claset() addEs [real_less_asym], - simpset() addsimps real_mult_ac@[realpow_mult RS sym,realpow_two_disj, + simpset() addsimps mult_ac@[realpow_mult RS sym,realpow_two_disj, realpow_gt_zero, real_mult_order] delsimps [realpow_Suc])); qed "real_sqrt_mult_distrib"; @@ -204,14 +204,14 @@ Goal "0 <= sqrt ((x ^ 2 + y ^ 2)*(xa ^ 2 + ya ^ 2))"; by (auto_tac (claset() addSIs [real_sqrt_ge_zero],simpset() - addsimps [real_0_le_mult_iff])); + addsimps [zero_le_mult_iff])); qed "real_sqrt_sum_squares_mult_ge_zero"; Addsimps [real_sqrt_sum_squares_mult_ge_zero]; Goal "sqrt ((x ^ 2 + y ^ 2) * (xa ^ 2 + ya ^ 2)) ^ 2 = \ \ (x ^ 2 + y ^ 2) * (xa ^ 2 + ya ^ 2)"; by (auto_tac (claset(),simpset() addsimps [real_sqrt_pow2_iff, - real_0_le_mult_iff] delsimps [realpow_Suc])); + zero_le_mult_iff] delsimps [realpow_Suc])); qed "real_sqrt_sum_squares_mult_squared_eq"; Addsimps [real_sqrt_sum_squares_mult_squared_eq]; @@ -283,21 +283,21 @@ (*-------------------------------------------------------------------------*) Goal "summable (%n. inverse (real (fact n)) * x ^ n)"; -by (cut_facts_tac [real_zero_less_one RS real_dense] 1); +by (cut_facts_tac [zero_less_one RS real_dense] 1); by (Step_tac 1); by (cut_inst_tac [("x","r")] reals_Archimedean3 1); by Auto_tac; by (dres_inst_tac [("x","abs x")] spec 1 THEN Safe_tac); by (res_inst_tac [("N","n"),("c","r")] ratio_test 1); -by (auto_tac (claset(),simpset() addsimps [abs_mult,real_mult_assoc RS sym] - delsimps [fact_Suc])); -by (rtac real_mult_le_le_mono2 1); -by (res_inst_tac [("b1","abs x")] (mult_commute RS ssubst) 2); -by (stac fact_Suc 2); -by (stac real_of_nat_mult 2); -by (auto_tac (claset(),simpset() addsimps [abs_mult,real_inverse_distrib])); +by (auto_tac (claset(), + simpset() addsimps [abs_mult,mult_assoc RS sym] delsimps [fact_Suc])); +by (rtac mult_right_mono 1); +by (res_inst_tac [("b1","abs x")] (mult_commute RS ssubst) 1); +by (stac fact_Suc 1); +by (stac real_of_nat_mult 1); +by (auto_tac (claset(),simpset() addsimps [abs_mult,inverse_mult_distrib])); by (auto_tac (claset(), simpset() addsimps - [mult_assoc RS sym, abs_eqI2, real_inverse_gt_0])); + [mult_assoc RS sym, abs_eqI2, positive_imp_inverse_positive])); by (rtac order_less_imp_le 1); by (res_inst_tac [("z1","real (Suc na)")] (real_mult_less_iff1 RS iffD1) 1); @@ -321,9 +321,9 @@ by (rtac summable_exp 2); by (res_inst_tac [("x","0")] exI 1); by (auto_tac (claset(), simpset() addsimps [realpow_abs RS sym, - abs_mult,real_0_le_mult_iff])); -by (auto_tac (claset() addIs [real_mult_le_le_mono2], - simpset() addsimps [real_inverse_gt_0,abs_eqI2])); + abs_mult,zero_le_mult_iff])); +by (auto_tac (claset() addIs [mult_right_mono], + simpset() addsimps [positive_imp_inverse_positive,abs_eqI2])); qed "summable_sin"; Goalw [real_divide_def] @@ -335,9 +335,9 @@ by (rtac summable_exp 2); by (res_inst_tac [("x","0")] exI 1); by (auto_tac (claset(), simpset() addsimps [realpow_abs RS sym,abs_mult, - real_0_le_mult_iff])); -by (auto_tac (claset() addSIs [real_mult_le_le_mono2], - simpset() addsimps [real_inverse_gt_0,abs_eqI2])); + zero_le_mult_iff])); +by (auto_tac (claset() addSIs [mult_right_mono], + simpset() addsimps [positive_imp_inverse_positive,abs_eqI2])); qed "summable_cos"; Goal "(if even n then 0 \ @@ -408,7 +408,7 @@ by (rtac sumr_subst 1); by (strip_tac 1); by (stac lemma_realpow_diff 1); -by (auto_tac (claset(),simpset() addsimps real_mult_ac)); +by (auto_tac (claset(),simpset() addsimps mult_ac)); qed "lemma_realpow_diff_sumr"; Goal "x ^ (Suc n) - y ^ (Suc n) = \ @@ -418,8 +418,8 @@ by (stac sumr_Suc 1); by (dtac sym 1); by (auto_tac (claset(),simpset() addsimps [lemma_realpow_diff_sumr, - real_add_mult_distrib2,real_diff_def] @ - real_mult_ac delsimps [sumr_Suc])); + right_distrib,real_diff_def] @ + mult_ac delsimps [sumr_Suc])); qed "lemma_realpow_diff_sumr2"; Goal "sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p))) = \ @@ -428,8 +428,8 @@ by (auto_tac (claset(),simpset() addsimps [real_mult_commute, realpow_add RS sym] delsimps [sumr_Suc])); by (res_inst_tac [("c1","x - y")] (real_mult_left_cancel RS iffD1) 1); -by (rtac (real_minus_minus RS subst) 2); -by (stac real_minus_mult_eq1 2); +by (rtac (minus_minus RS subst) 2); +by (stac minus_mult_left 2); by (auto_tac (claset(),simpset() addsimps [lemma_realpow_diff_sumr2 RS sym] delsimps [sumr_Suc])); qed "lemma_realpow_rev_sumr"; @@ -460,12 +460,11 @@ by (auto_tac (claset(), 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 (auto_tac (claset(),simpset() addsimps [abs_mult,realpow_abs] @ mult_ac)); 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, - realpow_abs,summable_def])); +by (auto_tac (claset() addSIs [mult_right_mono], + simpset() addsimps [mult_assoc RS sym, realpow_abs,summable_def])); by (res_inst_tac [("x","K * inverse(1 - (abs(z) * inverse(abs x)))")] exI 1); by (auto_tac (claset() addSIs [sums_mult],simpset() addsimps [real_mult_assoc])); by (subgoal_tac @@ -543,9 +542,9 @@ \ sumr 0 m (%p. (z ^ p) * \ \ (((z + h) ^ (m - p)) - (z ^ (m - p))))"; by (rtac sumr_subst 1); -by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2, +by (auto_tac (claset(),simpset() addsimps [right_distrib, real_diff_def,realpow_add RS sym] - @ real_mult_ac)); + @ mult_ac)); qed "lemma_termdiff1"; (* proved elsewhere? *) @@ -563,23 +562,23 @@ \ sumr 0 ((n - Suc 0) - p) \ \ (%q. ((z + h) ^ q) * (z ^ (((n - 2) - p) - q))))"; by (rtac (real_mult_left_cancel RS iffD1) 1 THEN Asm_simp_tac 1); -by (asm_full_simp_tac (simpset() addsimps [real_diff_mult_distrib2] - @ real_mult_ac) 1); +by (asm_full_simp_tac (simpset() addsimps [right_diff_distrib] + @ mult_ac) 1); by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1); by (case_tac "n" 1 THEN auto_tac (claset(),simpset() addsimps [lemma_realpow_diff_sumr2, - real_diff_mult_distrib2 RS sym,real_mult_assoc] + right_diff_distrib RS sym,real_mult_assoc] delsimps [realpow_Suc,sumr_Suc])); by (auto_tac (claset(),simpset() addsimps [lemma_realpow_rev_sumr] delsimps [sumr_Suc])); by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc,sumr_diff_mult_const, - real_add_mult_distrib,CLAIM "(a + b) - (c + d) = a - c + b - (d::real)", + left_distrib,CLAIM "(a + b) - (c + d) = a - c + b - (d::real)", lemma_termdiff1,sumr_mult])); by (auto_tac (claset() addSIs [sumr_subst],simpset() addsimps [real_diff_def,real_add_assoc])); by (fold_tac [real_diff_def] THEN dtac less_add_one 1); by (auto_tac (claset(),simpset() addsimps [sumr_mult,lemma_realpow_diff_sumr2] - @ real_mult_ac delsimps [sumr_Suc,realpow_Suc])); + @ mult_ac delsimps [sumr_Suc,realpow_Suc])); qed "lemma_termdiff2"; Goal "[| h ~= 0; abs z <= K; abs (z + h) <= K |] \ @@ -595,9 +594,9 @@ by (case_tac "n" 1 THEN Auto_tac); by (dtac less_add_one 1); by (auto_tac (claset(),simpset() addsimps [realpow_add,real_add_assoc RS sym, - CLAIM_SIMP "(a * b) * c = a * (c * (b::real))" real_mult_ac] + CLAIM_SIMP "(a * b) * c = a * (c * (b::real))" mult_ac] delsimps [sumr_Suc])); -by (auto_tac (claset() addSIs [real_mult_le_mono],simpset()delsimps [sumr_Suc])); +by (auto_tac (claset() addSIs [mult_mono],simpset()delsimps [sumr_Suc])); by (auto_tac (claset() addSIs [realpow_le2],simpset() addsimps [realpow_abs] delsimps [sumr_Suc] )); by (res_inst_tac [("j","real (Suc d) * (K ^ d)")] real_le_trans 1); @@ -606,8 +605,9 @@ by (dres_inst_tac [("n","d")] realpow_ge_zero2 2); by (auto_tac (claset(),simpset() delsimps [sumr_Suc] )); by (rtac (sumr_rabs RS real_le_trans) 1); -by (rtac sumr_bound2 1 THEN auto_tac (claset() addSDs [less_add_one] - addSIs [real_mult_le_mono],simpset() addsimps [abs_mult, realpow_add])); +by (rtac sumr_bound2 1 THEN + auto_tac (claset() addSDs [less_add_one] + addSIs [mult_mono], simpset() addsimps [abs_mult, realpow_add])); by (auto_tac (claset() addSIs [realpow_le2,realpow_ge_zero],simpset() addsimps [realpow_abs])); by (ALLGOALS(arith_tac)); @@ -632,8 +632,8 @@ by (REPEAT(rtac (real_mult_order) 2)); by (dres_inst_tac [("d1.0","r * inverse K * inverse 2"),("d2.0","k")] real_lbound_gt_zero 1); -by (auto_tac (claset(),simpset() addsimps [real_inverse_gt_0, - real_0_less_mult_iff])); +by (auto_tac (claset(),simpset() addsimps [positive_imp_inverse_positive, + zero_less_mult_iff])); by (rtac real_le_trans 2 THEN assume_tac 3 THEN Auto_tac); by (res_inst_tac [("x","e")] exI 1 THEN Auto_tac); by (res_inst_tac [("y","K * abs x")] order_le_less_trans 1); @@ -659,7 +659,7 @@ by (simp_tac (simpset() addsimps [summable_def]) 3); by (res_inst_tac [("x","suminf f * abs h")] exI 3); by (dres_inst_tac [("c","abs h")] sums_mult 3); -by (asm_full_simp_tac (simpset() addsimps real_mult_ac) 3); +by (asm_full_simp_tac (simpset() addsimps mult_ac) 3); by (subgoal_tac "summable (%n. abs(g(h::real)(n::nat)))" 2); by (res_inst_tac [("g","%n. f(n::nat) * abs(h)")] summable_comparison_test 3); by (res_inst_tac [("x","0")] exI 3); @@ -701,7 +701,7 @@ ("c","inverse xa")] sums_mult 1); by (rtac (sums_unique RS sym) 1); by (asm_full_simp_tac (simpset() addsimps [real_diff_def, - real_divide_def] @ real_add_ac @ real_mult_ac) 1); + real_divide_def] @ add_ac @ mult_ac) 1); by (rtac LIM_zero_cancel 1); by (res_inst_tac [("g","%h. suminf (%n. c(n) * (((((x + h) ^ n) - \ \ (x ^ n)) * inverse h) - (real n * (x ^ (n - Suc 0)))))")] LIM_trans 1); @@ -728,7 +728,7 @@ by (forw_inst_tac [("x","(%n. c n * (xa + x) ^ n)"), ("y","(%n. c n * x ^ n)")] sums_diff 1 THEN assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [[sums_summable,sums_summable] - MRS suminf_diff,real_diff_mult_distrib2 RS sym]) 1); + MRS suminf_diff,right_diff_distrib RS sym]) 1); by (forw_inst_tac [("x","(%n. c n * ((xa + x) ^ n - x ^ n))"), ("c","inverse xa")] sums_mult 1); by (asm_full_simp_tac (simpset() addsimps [sums_summable RS suminf_mult2]) 1); @@ -737,11 +737,11 @@ by (assume_tac 1); by (rtac (ARITH_PROVE "z - y = x ==> - x = (y::real) - z") 1); by (asm_full_simp_tac (simpset() addsimps [[sums_summable,sums_summable] - MRS suminf_diff] @ real_add_ac @ real_mult_ac ) 1); + MRS suminf_diff] @ add_ac @ mult_ac ) 1); by (res_inst_tac [("f","suminf")] arg_cong 1); by (rtac ext 1); by (asm_full_simp_tac (simpset() addsimps [real_diff_def, - real_add_mult_distrib2] @ real_add_ac @ real_mult_ac) 1); + right_distrib] @ add_ac @ mult_ac) 1); (* 46 *) by (dtac real_dense 1 THEN Step_tac 1); by (ftac (real_less_sum_gt_zero) 1); @@ -766,7 +766,7 @@ THEN asm_full_simp_tac (simpset() addsimps [diffs_def]) 2); by (dtac diffs_equiv 1); by (dtac sums_summable 1); -by (asm_full_simp_tac (simpset() addsimps [diffs_def] @ real_mult_ac) 1); +by (asm_full_simp_tac (simpset() addsimps [diffs_def] @ mult_ac) 1); by (subgoal_tac "(%n. real n * (real (Suc n) * (abs(c(Suc n)) * \ \ (r ^ (n - Suc 0))))) = (%n. diffs(%m. real (m - Suc 0) * \ \ abs(c m) * inverse r) n * (r ^ n))" 1); @@ -777,7 +777,7 @@ by Auto_tac; (* 69 *) by (dtac (abs_ge_zero RS order_le_less_trans) 2); -by (asm_full_simp_tac (simpset() addsimps real_mult_ac) 2); +by (asm_full_simp_tac (simpset() addsimps mult_ac) 2); by (dtac diffs_equiv 1); by (dtac sums_summable 1); by (res_inst_tac [("a","summable (%n. real n * \ @@ -785,7 +785,7 @@ (CLAIM "(a = b) ==> a ==> b") 1 THEN assume_tac 2); by (res_inst_tac [("f","summable")] arg_cong 1 THEN rtac ext 1); by (dtac (abs_ge_zero RS order_le_less_trans) 2); -by (asm_full_simp_tac (simpset() addsimps real_mult_ac) 2); +by (asm_full_simp_tac (simpset() addsimps mult_ac) 2); (* 77 *) by (case_tac "n" 1); by Auto_tac; @@ -794,13 +794,13 @@ by (dtac (abs_ge_zero RS order_le_less_trans) 1); by (auto_tac (claset(),simpset() addsimps [CLAIM_SIMP "(a::real) * (b * (c * d)) = a * (b * c) * d" - real_mult_ac])); + mult_ac])); by (dtac (abs_ge_zero RS order_le_less_trans) 1); by (asm_full_simp_tac (simpset() addsimps [abs_mult,real_mult_assoc]) 1); -by (rtac real_mult_le_le_mono1 1); -by (rtac (real_add_commute RS subst) 2); -by (simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 2); -by (rtac lemma_termdiff3 2); +by (rtac mult_left_mono 1); +by (rtac (add_commute RS subst) 1); +by (simp_tac (simpset() addsimps [mult_assoc RS sym]) 1); +by (rtac lemma_termdiff3 1); by (auto_tac (claset() addIs [(abs_triangle_ineq RS real_le_trans)], simpset())); by (arith_tac 1); @@ -815,7 +815,7 @@ by (rtac ext 1); by (stac fact_Suc 1); by (stac real_of_nat_mult 1); -by (stac real_inverse_distrib 1); +by (stac inverse_mult_distrib 1); by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym])); qed "exp_fdiffs"; @@ -829,7 +829,7 @@ by (stac fact_Suc 1); by (stac real_of_nat_mult 1); by (stac even_Suc 1); -by (stac real_inverse_distrib 1); +by (stac inverse_mult_distrib 1); by Auto_tac; qed "sin_fdiffs"; @@ -842,7 +842,7 @@ by (stac fact_Suc 1); by (stac real_of_nat_mult 1); by (stac even_Suc 1); -by (stac real_inverse_distrib 1); +by (stac inverse_mult_distrib 1); by Auto_tac; qed "sin_fdiffs2"; @@ -856,7 +856,7 @@ by (stac fact_Suc 1); by (stac real_of_nat_mult 1); by (stac even_Suc 1); -by (stac real_inverse_distrib 1); +by (stac inverse_mult_distrib 1); by (res_inst_tac [("z1","real (Suc n)")] (real_mult_commute RS ssubst) 1); by (res_inst_tac [("z1","inverse(real (Suc n))")] (real_mult_commute RS ssubst) 1); @@ -873,7 +873,7 @@ by (stac fact_Suc 1); by (stac real_of_nat_mult 1); by (stac even_Suc 1); -by (stac real_inverse_distrib 1); +by (stac inverse_mult_distrib 1); by (res_inst_tac [("z1","real (Suc n)")] (real_mult_commute RS ssubst) 1); by (res_inst_tac [("z1","inverse (real (Suc n))")] (real_mult_commute RS ssubst) 1); @@ -932,7 +932,7 @@ Goal "DERIV cos x :> -sin(x)"; by (stac lemma_cos_ext 1); by (auto_tac (claset(),simpset() addsimps [lemma_sin_minus, - cos_fdiffs2 RS sym,real_minus_mult_eq1])); + cos_fdiffs2 RS sym,minus_mult_left])); by (res_inst_tac [("K","1 + abs(x)")] termdiffs 1); by (auto_tac (claset() addIs [sin_converges,cos_converges, sums_summable] addSIs [sums_minus RS sums_summable], @@ -962,7 +962,7 @@ by (res_inst_tac [("n","2"),("f","(%n. inverse (real (fact n)) * x ^ n)")] series_pos_le 2); by (auto_tac (claset() addIs [summable_exp],simpset() - addsimps [numeral_2_eq_2,realpow_ge_zero,real_0_le_mult_iff])); + addsimps [numeral_2_eq_2,realpow_ge_zero,zero_le_mult_iff])); qed "exp_ge_add_one_self"; Addsimps [exp_ge_add_one_self]; @@ -978,7 +978,7 @@ [CLAIM_SIMP "(%x. exp (x + y)) = exp o (%x. x + y)" [ext]])); by (rtac (real_mult_1_right RS subst) 1); by (rtac DERIV_chain 1); -by (rtac (real_add_zero_right RS subst) 2); +by (rtac (add_zero_right RS subst) 2); by (rtac DERIV_add 2); by Auto_tac; qed "DERIV_exp_add_const"; @@ -988,8 +988,8 @@ by (auto_tac (claset(),simpset() addsimps [CLAIM_SIMP "(%x. exp(-x)) = exp o (%x. - x)" [ext]])); by (rtac (real_mult_1_right RS subst) 1); -by (rtac (real_minus_mult_eq1 RS subst) 1); -by (stac real_minus_mult_eq2 1); +by (rtac (minus_mult_left RS subst) 1); +by (stac minus_mult_right 1); by (rtac DERIV_chain 1); by (rtac DERIV_minus 2); by Auto_tac; @@ -999,7 +999,7 @@ Goal "DERIV (%x. exp (x + y) * exp (- x)) x :> 0"; by (cut_inst_tac [("x","x"),("y2","y")] ([DERIV_exp_add_const, DERIV_exp_minus] MRS DERIV_mult) 1); -by (auto_tac (claset(),simpset() addsimps real_mult_ac)); +by (auto_tac (claset(),simpset() addsimps mult_ac)); qed "DERIV_exp_exp_zero"; Addsimps [DERIV_exp_exp_zero]; @@ -1031,7 +1031,7 @@ (exp_add_mult_minus RS (CLAIM "x = y ==> z * y = z * (x::real)")) 1); by (asm_full_simp_tac HOL_ss 1); by (asm_full_simp_tac (simpset() delsimps [exp_add_mult_minus] - addsimps real_mult_ac) 1); + addsimps mult_ac) 1); qed "exp_add"; Goal "0 <= exp x"; @@ -1053,7 +1053,7 @@ Addsimps [exp_gt_zero]; Goal "0 < inverse(exp x)"; -by (auto_tac (claset() addIs [real_inverse_gt_0],simpset())); +by (auto_tac (claset() addIs [positive_imp_inverse_positive],simpset())); qed "inv_exp_gt_zero"; Addsimps [inv_exp_gt_zero]; @@ -1065,7 +1065,7 @@ Goal "exp(real n * x) = exp(x) ^ n"; by (induct_tac "n" 1); by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc, - real_add_mult_distrib2,exp_add,real_mult_commute])); + right_distrib,exp_add,real_mult_commute])); qed "exp_real_of_nat_mult"; Goalw [real_diff_def,real_divide_def] @@ -1080,7 +1080,7 @@ qed "exp_less_mono"; Goal "exp x < exp y ==> x < y"; -by (EVERY1[rtac ccontr, dtac real_leI, dtac real_le_imp_less_or_eq]); +by (EVERY1[rtac ccontr, dtac (linorder_not_less RS iffD1), dtac real_le_imp_less_or_eq]); by (auto_tac (claset() addDs [exp_less_mono],simpset())); qed "exp_less_cancel"; @@ -1155,13 +1155,13 @@ Addsimps [ln_one]; Goal "0 < x ==> ln(inverse x) = - ln x"; -by (res_inst_tac [("x1","ln x")] (real_add_left_cancel RS iffD1) 1); -by (auto_tac (claset(),simpset() addsimps [real_inverse_gt_0,ln_mult RS sym])); +by (res_inst_tac [("a1","ln x")] (add_left_cancel RS iffD1) 1); +by (auto_tac (claset(),simpset() addsimps [positive_imp_inverse_positive,ln_mult RS sym])); qed "ln_inverse"; Goalw [real_divide_def] "[|0 < x; 0 < y|] ==> ln(x/y) = ln x - ln y"; -by (auto_tac (claset(),simpset() addsimps [real_inverse_gt_0, +by (auto_tac (claset(),simpset() addsimps [positive_imp_inverse_positive, ln_mult,ln_inverse])); qed "ln_div"; @@ -1284,7 +1284,7 @@ Goal "DERIV (%x. cos(x)*cos(x)) x :> -2 * cos(x) * sin(x)"; by (cut_inst_tac [("x","x")] DERIV_cos_cos_mult 1); -by (auto_tac (claset(),simpset() addsimps real_mult_ac)); +by (auto_tac (claset(),simpset() addsimps mult_ac)); qed "DERIV_cos_cos_mult2"; Addsimps [DERIV_cos_cos_mult2]; @@ -1351,12 +1351,12 @@ Addsimps [sin_cos_squared_add3]; Goal "(sin(x) ^ 2) = 1 - (cos(x) ^ 2)"; -by (res_inst_tac [("x1","(cos(x) ^ 2)")] (real_add_right_cancel RS iffD1) 1); +by (res_inst_tac [("a1","(cos(x) ^ 2)")] (add_right_cancel RS iffD1) 1); by (simp_tac (simpset() delsimps [realpow_Suc]) 1); qed "sin_squared_eq"; Goal "(cos(x) ^ 2) = 1 - (sin(x) ^ 2)"; -by (res_inst_tac [("x1","(sin(x) ^ 2)")] (real_add_right_cancel RS iffD1) 1); +by (res_inst_tac [("a1","(sin(x) ^ 2)")] (add_right_cancel RS iffD1) 1); by (simp_tac (simpset() delsimps [realpow_Suc]) 1); qed "cos_squared_eq"; @@ -1472,8 +1472,8 @@ by (Step_tac 1 THEN rtac lemma_DERIV_subst 1); by DERIV_tac; by (auto_tac (claset(),simpset() addsimps [real_diff_def, - real_add_mult_distrib,real_add_mult_distrib2] @ - real_mult_ac @ real_add_ac)); + left_distrib,right_distrib] @ + mult_ac @ add_ac)); val lemma_DERIV_sin_cos_add = result(); Goal "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 + \ @@ -1500,8 +1500,8 @@ by (Step_tac 1 THEN rtac lemma_DERIV_subst 1); by DERIV_tac; by (auto_tac (claset(),simpset() addsimps [real_diff_def, - real_add_mult_distrib,real_add_mult_distrib2] - @ real_mult_ac @ real_add_ac)); + left_distrib,right_distrib] + @ mult_ac @ add_ac)); val lemma_DERIV_sin_cos_minus = result(); Goal "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"; @@ -1587,7 +1587,7 @@ by (asm_full_simp_tac (simpset() addsimps []) 1); by (asm_simp_tac (simpset() addsimps [numeral_2_eq_2 RS sym, real_mult_assoc RS sym]) 1); by (stac (CLAIM "6 = 2 * (3::real)") 1); -by (rtac real_mult_less_mono 1); +by (rtac real_mult_less_mono 1); (*mult_strict_mono would be stronger*) by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc] delsimps [fact_Suc])); by (stac fact_Suc 1); by (stac fact_Suc 1); @@ -1598,7 +1598,7 @@ by (stac real_of_nat_mult 1); by (stac real_of_nat_mult 1); by (simp_tac (simpset() addsimps [real_divide_def, - real_inverse_distrib] delsimps [fact_Suc]) 1); + inverse_mult_distrib] delsimps [fact_Suc]) 1); by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym] delsimps [fact_Suc])); by (multr_by_tac "real (Suc (Suc (4*m)))" 1); @@ -1613,7 +1613,7 @@ by (subgoal_tac "0 < x ^ (4 * m)" 1); by (asm_simp_tac (simpset() addsimps [realpow_gt_zero]) 2); by (asm_simp_tac (simpset() addsimps [mult_less_cancel_left]) 1); -by (rtac real_mult_less_mono 1); +by (rtac real_mult_less_mono 1); (*mult_strict_mono would be stronger*) by (ALLGOALS(Asm_simp_tac)); by (TRYALL(rtac real_less_trans)); by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc] delsimps [fact_Suc])); @@ -1626,10 +1626,11 @@ qed "sin_gt_zero1"; Goal "[| 0 < x; x < 2 |] ==> cos (2 * x) < 1"; -by (auto_tac (claset(),simpset() addsimps [cos_squared_eq, - real_minus_add_distrib RS sym, real_minus_zero_less_iff2,sin_gt_zero1, - real_add_order,realpow_gt_zero,cos_double] delsimps - [realpow_Suc,real_minus_add_distrib])); +by (auto_tac (claset(), + simpset() addsimps [cos_squared_eq, + minus_add_distrib RS sym, neg_less_0_iff_less,sin_gt_zero1, + real_add_order,realpow_gt_zero,cos_double] + delsimps [realpow_Suc,minus_add_distrib])); qed "cos_double_less_one"; Goal "(%n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) \ @@ -1666,7 +1667,7 @@ by (stac fact_Suc 1); by (stac real_of_nat_mult 1); by (stac real_of_nat_mult 1); -by (rtac real_mult_less_mono 1); +by (rtac real_mult_less_mono 1); (*mult_strict_mono would be stronger*) by (Force_tac 1); by (Force_tac 2); by (rtac real_of_nat_fact_gt_zero 2); @@ -1820,14 +1821,14 @@ Goal "cos (real n * pi) = (-(1::real)) ^ n"; by (induct_tac "n" 1); by (auto_tac (claset(),simpset() addsimps - [real_of_nat_Suc,real_add_mult_distrib])); + [real_of_nat_Suc,left_distrib])); qed "cos_npi"; Addsimps [cos_npi]; Goal "sin (real (n::nat) * pi) = 0"; by (induct_tac "n" 1); by (auto_tac (claset(),simpset() addsimps - [real_of_nat_Suc,real_add_mult_distrib])); + [real_of_nat_Suc,left_distrib])); qed "sin_npi"; Addsimps [sin_npi]; @@ -1977,7 +1978,7 @@ \ (cos(x - real n * pi) = 0)" 1); by (Step_tac 1); by (asm_full_simp_tac (simpset() addsimps [real_of_nat_Suc, - real_add_mult_distrib]) 2); + left_distrib]) 2); by (asm_full_simp_tac (simpset() addsimps [cos_diff]) 1); by (asm_full_simp_tac (simpset() addsimps [cos_diff]) 2); by (subgoal_tac "EX! x. 0 <= x & x <= pi & cos x = 0" 1); @@ -1988,7 +1989,7 @@ by (asm_full_simp_tac (simpset() addsimps [cos_diff]) 1); by (res_inst_tac [("x","Suc (2 * n)")] exI 1); by (asm_full_simp_tac (simpset() addsimps [real_of_nat_Suc, - real_add_mult_distrib]) 1); + left_distrib]) 1); by Auto_tac; qed "cos_zero_lemma"; @@ -2003,7 +2004,7 @@ by (rtac real_le_trans 2 THEN assume_tac 3); by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym, odd_Suc_mult_two_ex,real_of_nat_Suc, - real_add_mult_distrib,real_mult_assoc RS sym])); + left_distrib,real_mult_assoc RS sym])); qed "sin_zero_lemma"; (* also spoilt by numeral arithmetic *) @@ -2019,7 +2020,7 @@ by (Step_tac 1); by (dtac (CLAIM "-x = y ==> x = -(y::real)") 2); by (auto_tac (claset(),HOL_ss addsimps [odd_not_even RS sym, - odd_Suc_mult_two_ex,real_of_nat_Suc,real_add_mult_distrib])); + odd_Suc_mult_two_ex,real_of_nat_Suc,left_distrib])); by (auto_tac (claset(),simpset() addsimps [cos_add])); qed "cos_zero_iff"; @@ -2058,7 +2059,7 @@ Addsimps [tan_npi]; Goalw [tan_def] "tan (-x) = - tan x"; -by (simp_tac (simpset() addsimps [real_minus_mult_eq1]) 1); +by (simp_tac (simpset() addsimps [minus_mult_left]) 1); qed "tan_minus"; Addsimps [tan_minus]; @@ -2072,12 +2073,11 @@ \ ==> 1 - tan(x)*tan(y) = cos (x + y)/(cos x * cos y)"; by (auto_tac (claset(), simpset() delsimps [thm"Ring_and_Field.inverse_mult_distrib"] - addsimps [real_inverse_distrib RS sym] @ real_mult_ac)); + addsimps [inverse_mult_distrib RS sym] @ mult_ac)); by (res_inst_tac [("c1","cos x * cos y")] (real_mult_right_cancel RS subst) 1); by (auto_tac (claset(), simpset() delsimps [thm"Ring_and_Field.inverse_mult_distrib"] - addsimps [real_mult_assoc, - real_mult_not_zero,real_diff_mult_distrib,cos_add])); + addsimps [mult_assoc, left_diff_distrib,cos_add])); val lemma_tan_add1 = result(); Addsimps [lemma_tan_add1]; @@ -2085,8 +2085,7 @@ "[| cos x ~= 0; cos y ~= 0 |] \ \ ==> tan x + tan y = sin(x + y)/(cos x * cos y)"; by (res_inst_tac [("c1","cos x * cos y")] (real_mult_right_cancel RS subst) 1); -by (auto_tac (claset(), simpset() addsimps [real_mult_assoc, - real_mult_not_zero,real_add_mult_distrib])); +by (auto_tac (claset(), simpset() addsimps [mult_assoc, left_distrib])); by (simp_tac (simpset() addsimps [sin_add]) 1); qed "add_tan_eq"; @@ -2106,8 +2105,7 @@ Goalw [tan_def,real_divide_def] "[| 0 < x; x < pi/2 |] ==> 0 < tan x"; by (auto_tac (claset() addSIs [sin_gt_zero2,cos_gt_zero_pi] - addSIs [real_mult_order, - real_inverse_gt_0],simpset())); + addSIs [real_mult_order, positive_imp_inverse_positive],simpset())); qed "tan_gt_zero"; Goal "[| - pi/2 < x; x < 0 |] ==> tan x < 0"; @@ -2131,9 +2129,9 @@ Goalw [real_divide_def] "(%x. cos(x)/sin(x)) -- pi/2 --> 0"; -by (res_inst_tac [("z1","1")] ((real_mult_0) RS subst) 1); +by (res_inst_tac [("a1","1")] ((mult_left_zero) RS subst) 1); by (rtac LIM_mult2 1); -by (rtac ((real_inverse_1) RS subst) 2); +by (rtac (inverse_1 RS subst) 2); by (rtac LIM_inverse 2); by (fold_tac [real_divide_def]); by (auto_tac (claset() addSIs [DERIV_isCont],simpset() @@ -2163,10 +2161,10 @@ by (subgoal_tac "0 < sin e" 3); by (subgoal_tac "0 < cos e" 3); by (auto_tac (claset() addIs [cos_gt_zero,sin_gt_zero2],simpset() - addsimps [real_inverse_distrib,abs_mult])); -by (dres_inst_tac [("x","cos e")] (real_inverse_gt_0) 1); + addsimps [inverse_mult_distrib,abs_mult])); +by (dres_inst_tac [("a","cos e")] (positive_imp_inverse_positive) 1); by (dres_inst_tac [("x","inverse (cos e)")] abs_eqI2 1); -by (auto_tac (claset() addSDs [abs_eqI2],simpset() addsimps real_mult_ac)); +by (auto_tac (claset() addSDs [abs_eqI2],simpset() addsimps mult_ac)); qed "lemma_tan_total"; @@ -2376,9 +2374,9 @@ by (case_tac "n" 3); by (cut_inst_tac [("y","x")] arctan_ubound 2); by (cut_inst_tac [("y","x")] arctan_lbound 4); -by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc, - real_add_mult_distrib,real_le_def, - real_mult_less_0_iff] delsimps [arctan])); +by (auto_tac (claset(), + simpset() addsimps [real_of_nat_Suc, left_distrib,real_le_def, mult_less_0_iff] + delsimps [arctan])); qed "cos_arctan_not_zero"; Addsimps [cos_arctan_not_zero]; @@ -2386,7 +2384,7 @@ by (rtac (realpow_inverse RS subst) 1); by (res_inst_tac [("c1","cos(x) ^ 2")] (real_mult_right_cancel RS iffD1) 1); by (auto_tac (claset() addDs [realpow_not_zero], simpset() addsimps - [realpow_mult,real_add_mult_distrib,realpow_divide, + [realpow_mult,left_distrib,realpow_divide, tan_def,real_mult_assoc,realpow_inverse RS sym] delsimps [realpow_Suc])); qed "tan_sec"; @@ -2399,7 +2397,7 @@ Goal "sin (xa + 1 / 2 * real (Suc m) * pi) = \ \ cos (xa + 1 / 2 * real (m) * pi)"; by (simp_tac (HOL_ss addsimps [cos_add,sin_add, - real_of_nat_Suc,real_add_mult_distrib,real_add_mult_distrib2]) 1); + real_of_nat_Suc,left_distrib,right_distrib]) 1); by Auto_tac; qed "lemma_sin_cos_eq"; Addsimps [lemma_sin_cos_eq]; @@ -2407,7 +2405,7 @@ Goal "sin (xa + real (Suc m) * pi / 2) = \ \ cos (xa + real (m) * pi / 2)"; by (simp_tac (HOL_ss addsimps [cos_add,sin_add,real_divide_def, - real_of_nat_Suc,real_add_mult_distrib,real_add_mult_distrib2]) 1); + real_of_nat_Suc,left_distrib,right_distrib]) 1); by Auto_tac; qed "lemma_sin_cos_eq2"; Addsimps [lemma_sin_cos_eq2]; @@ -2422,15 +2420,15 @@ (* which further simplifies to (- 1 ^ m) !! *) Goal "sin ((real m + 1/2) * pi) = cos (real m * pi)"; -by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2, - sin_add,real_add_mult_distrib] @ real_mult_ac)); +by (auto_tac (claset(),simpset() addsimps [right_distrib, + sin_add,left_distrib] @ mult_ac)); qed "sin_cos_npi"; Addsimps [sin_cos_npi]; Goal "sin (real (Suc (2 * n)) * pi / 2) = (- 1) ^ n"; by (cut_inst_tac [("m","n")] sin_cos_npi 1); by (auto_tac (claset(),HOL_ss addsimps [real_of_nat_Suc, - real_add_mult_distrib,real_divide_def])); + left_distrib,real_divide_def])); by Auto_tac; qed "sin_cos_npi2"; Addsimps [ sin_cos_npi2]; @@ -2444,8 +2442,8 @@ Goal "cos (3 / 2 * pi) = 0"; by (rtac (CLAIM "(1::real) + 1/2 = 3/2" RS subst) 1); -by (stac real_add_mult_distrib 1); -by (auto_tac (claset(),simpset() addsimps [cos_add] @ real_mult_ac)); +by (stac left_distrib 1); +by (auto_tac (claset(),simpset() addsimps [cos_add] @ mult_ac)); qed "cos_3over2_pi"; Addsimps [cos_3over2_pi]; @@ -2456,16 +2454,16 @@ Goal "sin (3 / 2 * pi) = - 1"; by (rtac (CLAIM "(1::real) + 1/2 = 3/2" RS subst) 1); -by (stac real_add_mult_distrib 1); -by (auto_tac (claset(),simpset() addsimps [sin_add] @real_mult_ac)); +by (stac left_distrib 1); +by (auto_tac (claset(),simpset() addsimps [sin_add] @mult_ac)); qed "sin_3over2_pi"; Addsimps [sin_3over2_pi]; Goal "cos(xa + 1 / 2 * real (Suc m) * pi) = \ \ -sin (xa + 1 / 2 * real (m) * pi)"; by (simp_tac (HOL_ss addsimps [cos_add,sin_add, - real_of_nat_Suc,real_add_mult_distrib2,real_add_mult_distrib, - real_minus_mult_eq2]) 1); + real_of_nat_Suc,right_distrib,left_distrib, + minus_mult_right]) 1); by Auto_tac; qed "lemma_cos_sin_eq"; Addsimps [lemma_cos_sin_eq]; @@ -2473,14 +2471,14 @@ Goal "cos (xa + real (Suc m) * pi / 2) = \ \ -sin (xa + real (m) * pi / 2)"; by (simp_tac (HOL_ss addsimps [cos_add,sin_add,real_divide_def, - real_of_nat_Suc,real_add_mult_distrib,real_add_mult_distrib2]) 1); + real_of_nat_Suc,left_distrib,right_distrib]) 1); by Auto_tac; qed "lemma_cos_sin_eq2"; Addsimps [lemma_cos_sin_eq2]; Goal "cos (pi * real (Suc (2 * m)) / 2) = 0"; by (simp_tac (HOL_ss addsimps [cos_add,sin_add,real_divide_def, - real_of_nat_Suc,real_add_mult_distrib,real_add_mult_distrib2]) 1); + real_of_nat_Suc,left_distrib,right_distrib]) 1); by Auto_tac; qed "cos_pi_eq_zero"; Addsimps [cos_pi_eq_zero]; @@ -2559,7 +2557,7 @@ Goal "[| 0 <= x; 0 <= y |] ==> (root(Suc n) x < root(Suc n) y) = (x < y)"; by (auto_tac (claset() addIs [real_root_less_mono],simpset())); -by (rtac ccontr 1 THEN dtac real_leI 1); +by (rtac ccontr 1 THEN dtac (linorder_not_less RS iffD1) 1); by (dres_inst_tac [("x","y"),("n","n")] real_root_le_mono 1); by Auto_tac; qed "real_root_less_iff"; @@ -2591,7 +2589,7 @@ \ ==> root(Suc n) (x * y) = root(Suc n) x * root(Suc n) y"; by (rtac real_root_pos_unique 1); by (auto_tac (claset() addSIs [real_root_pos_pos_le],simpset() - addsimps [realpow_mult,real_0_le_mult_iff, + addsimps [realpow_mult,zero_le_mult_iff, real_root_pow_pos2] delsimps [realpow_Suc])); qed "real_root_mult"; @@ -2651,7 +2649,7 @@ Goalw [real_divide_def] "(((r::real) * a) / (r * r)) = a / r"; by (case_tac "r=0" 1); -by (auto_tac (claset(),simpset() addsimps [real_inverse_distrib] @ real_mult_ac)); +by (auto_tac (claset(),simpset() addsimps [inverse_mult_distrib] @ mult_ac)); qed "real_divide_square_eq"; Addsimps [real_divide_square_eq]; @@ -2677,13 +2675,13 @@ Goal "x < 0 ==> 0 < sqrt (x * x + y * y)"; by (rtac real_sqrt_gt_zero 1); by (rtac (ARITH_PROVE "[| 0 < x; 0 <= y |] ==> (0::real) < x + y") 1); -by (auto_tac (claset(),simpset() addsimps [real_0_less_mult_iff])); +by (auto_tac (claset(),simpset() addsimps [zero_less_mult_iff])); qed "real_sqrt_sum_squares_gt_zero1"; Goal "0 < x ==> 0 < sqrt (x * x + y * y)"; by (rtac real_sqrt_gt_zero 1); by (rtac (ARITH_PROVE "[| 0 < x; 0 <= y |] ==> (0::real) < x + y") 1); -by (auto_tac (claset(),simpset() addsimps [real_0_less_mult_iff])); +by (auto_tac (claset(),simpset() addsimps [zero_less_mult_iff])); qed "real_sqrt_sum_squares_gt_zero2"; Goal "x ~= 0 ==> 0 < sqrt(x ^ 2 + y ^ 2)"; @@ -2725,7 +2723,7 @@ by (case_tac "y = 0" 1); by Auto_tac; by (ftac abs_minus_eqI2 1); -by (auto_tac (claset(),simpset() addsimps [real_minus_inverse])); +by (auto_tac (claset(),simpset() addsimps [inverse_minus_eq])); by (rtac order_less_imp_le 1); by (res_inst_tac [("z1","sqrt(x * x + y * y)")] (real_mult_less_iff1 RS iffD1) 1); @@ -2733,7 +2731,7 @@ (real_sqrt_sum_squares_gt_zero1 RS real_not_refl2 RS not_sym) 2); by (auto_tac (claset() addIs [real_sqrt_sum_squares_gt_zero1], - simpset() addsimps real_mult_ac)); + simpset() addsimps mult_ac)); by (rtac (ARITH_PROVE "-x < y ==> -y < (x::real)") 1); by (cut_inst_tac [("x","-x"),("y","y")] real_sqrt_sum_squares_ge1 1); by (dtac real_le_imp_less_or_eq 1); @@ -2836,8 +2834,8 @@ by (thin_tac "(1 - z) * (x + y) = x /(x + y) * (x + y)" 2); by (thin_tac "1 - z = x /(x + y)" 2); by (auto_tac (claset(),simpset() addsimps [real_mult_assoc])); -by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2, - real_diff_mult_distrib])); +by (auto_tac (claset(),simpset() addsimps [right_distrib, + left_diff_distrib])); qed "lemma_divide_rearrange"; Goal "[| 0 < x * x + y * y; \ @@ -2901,7 +2899,7 @@ Goalw [real_divide_def] "x ~= 0 ==> x / sqrt (x * x + y * y) ~= 0"; by (forw_inst_tac [("y3","y")] (real_sqrt_sum_squares_gt_zero3 - RS real_not_refl2 RS not_sym RS real_inverse_not_zero) 1); + RS real_not_refl2 RS not_sym RS nonzero_imp_inverse_nonzero) 1); by (auto_tac (claset(),simpset() addsimps [real_power_two])); qed "lemma_cos_not_eq_zero"; @@ -2925,7 +2923,7 @@ by (case_tac "x = 0" 1); by (auto_tac (claset(),simpset() addsimps [abs_eqI2])); by (dres_inst_tac [("y","y")] real_sqrt_sum_squares_gt_zero3 1); -by (auto_tac (claset(),simpset() addsimps [real_0_less_mult_iff, +by (auto_tac (claset(),simpset() addsimps [zero_less_mult_iff, real_divide_def,real_power_two])); qed "real_sqrt_divide_less_zero"; @@ -3039,7 +3037,7 @@ simpset() addsimps [real_0_le_divide_iff,realpow_divide, real_sqrt_gt_zero_pow2,numeral_2_eq_2 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); +by (rtac add_mono 1); by (auto_tac (claset(),simpset() delsimps [realpow_Suc])); by (ALLGOALS(rtac ((CLAIM "(2::real) ^ 2 = 4") RS subst))); by (ALLGOALS(rtac (realpow_mult RS subst))); diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/hypreal_arith.ML --- a/src/HOL/Hyperreal/hypreal_arith.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/hypreal_arith.ML Thu Jan 01 10:06:32 2004 +0100 @@ -214,8 +214,8 @@ val hypreal_mult_mono_thms = [(rotate_prems 1 hypreal_mult_less_mono2, cvar(hypreal_mult_less_mono2, hd(prems_of hypreal_mult_less_mono2))), - (hypreal_mult_le_mono2, - cvar(hypreal_mult_le_mono2, hd(tl(prems_of hypreal_mult_le_mono2))))] + (mult_left_mono, + cvar(mult_left_mono, hd(tl(prems_of mult_left_mono))))] in diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Hyperreal/hypreal_arith0.ML --- a/src/HOL/Hyperreal/hypreal_arith0.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Hyperreal/hypreal_arith0.ML Thu Jan 01 10:06:32 2004 +0100 @@ -14,8 +14,7 @@ add_hypreal_number_of, minus_hypreal_number_of, diff_hypreal_number_of, mult_hypreal_number_of, eq_hypreal_number_of, less_hypreal_number_of, le_hypreal_number_of_eq_not_less, hypreal_diff_def, - minus_add_distrib, minus_minus, hypreal_mult_assoc, - minus_zero, + minus_add_distrib, minus_minus, mult_assoc, minus_zero, hypreal_add_zero_left, hypreal_add_zero_right, hypreal_add_minus, hypreal_add_minus_left, mult_left_zero, mult_right_zero, @@ -49,8 +48,8 @@ val hypreal_mult_mono_thms = [(rotate_prems 1 hypreal_mult_less_mono2, cvar(hypreal_mult_less_mono2, hd(prems_of hypreal_mult_less_mono2))), - (hypreal_mult_le_mono2, - cvar(hypreal_mult_le_mono2, hd(tl(prems_of hypreal_mult_le_mono2))))] + (mult_left_mono, + cvar(mult_left_mono, hd(tl(prems_of mult_left_mono))))] in diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/IsaMakefile Thu Jan 01 10:06:32 2004 +0100 @@ -144,8 +144,7 @@ Real/RealArith0.thy Real/real_arith0.ML \ Real/RealArith.thy Real/real_arith.ML Real/RealBin.ML \ Real/RealBin.thy Real/RealDef.thy \ - Real/RealInt.thy Real/RealOrd.thy \ - Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\ + Real/RealInt.thy Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\ Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \ Hyperreal/Fact.ML Hyperreal/Fact.thy\ Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HRealAbs.ML\ diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Real/Complex_Numbers.thy --- a/src/HOL/Real/Complex_Numbers.thy Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Real/Complex_Numbers.thy Thu Jan 01 10:06:32 2004 +0100 @@ -120,10 +120,10 @@ thus ?thesis by rule (insert ge, arith+) qed with neq show "Re (inverse w * w) = Re 1" - by (simp add: inverse_complex_def real_power_two real_add_divide_distrib [symmetric]) + by (simp add: inverse_complex_def real_power_two add_divide_distrib [symmetric]) from neq show "Im (inverse w * w) = Im 1" by (simp add: inverse_complex_def real_power_two - real_mult_ac real_add_divide_distrib [symmetric]) + mult_ac add_divide_distrib [symmetric]) qed qed diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Real/HahnBanach/Aux.thy --- a/src/HOL/Real/HahnBanach/Aux.thy Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Real/HahnBanach/Aux.thy Thu Jan 01 10:06:32 2004 +0100 @@ -3,7 +3,7 @@ Author: Gertrud Bauer, TU Munich *) -header {* Auxiliary theorems *} (* FIXME clean *) +header {* Auxiliary theorems *} (* FIXME clean: many are in Ring_and_Field *) theory Aux = Real + Bounds + Zorn: @@ -38,45 +38,16 @@ lemma real_mult_le_le_mono1a: "(0::real) \ z \ x \ y \ z * x \ z * y" - by (simp add: real_mult_le_mono2) + by (simp add: mult_left_mono) -lemma real_mult_le_le_mono2: - "(0::real) \ z \ x \ y \ x * z \ y * z" -proof - - assume "(0::real) \ z" "x \ y" - hence "x < y \ x = y" by (auto simp add: order_le_less) - thus ?thesis - proof - assume "x < y" - show ?thesis by (rule real_mult_le_less_mono1) (simp!) - next - assume "x = y" - thus ?thesis by simp - qed -qed - +text{*The next two results are needlessly weak*} lemma real_mult_less_le_anti: "z < (0::real) \ x \ y \ z * y \ z * x" -proof - - assume "z < 0" "x \ y" - hence "0 < - z" by simp - hence "0 \ - z" by (rule order_less_imp_le) - hence "x * (- z) \ y * (- z)" - by (rule real_mult_le_le_mono2) - hence "- (x * z) \ - (y * z)" - by (simp only: real_mult_minus_eq2) - thus ?thesis by (simp only: real_mult_commute) -qed + by (simp add: mult_left_mono_neg order_less_imp_le) lemma real_mult_less_le_mono: "(0::real) < z \ x \ y \ z * x \ z * y" -proof - - assume "0 < z" "x \ y" - have "0 \ z" by (rule order_less_imp_le) - hence "x * z \ y * z" - by (rule real_mult_le_le_mono2) - thus ?thesis by (simp only: real_mult_commute) -qed + by (simp add: mult_left_mono order_less_imp_le) lemma real_mult_inv_right1: "(x::real) \ 0 \ x * inverse x = 1" by simp @@ -86,14 +57,14 @@ lemma real_le_mult_order1a: "(0::real) \ x \ 0 \ y \ 0 \ x * y" - by (simp add: real_0_le_mult_iff) + by (simp add: zero_le_mult_iff) lemma real_mult_diff_distrib: "a * (- x - (y::real)) = - a * x - a * y" proof - have "- x - y = - x + - y" by simp also have "a * ... = a * - x + a * - y" - by (simp only: real_add_mult_distrib2) + by (simp only: right_distrib) also have "... = - a * x - a * y" by simp finally show ?thesis . @@ -103,7 +74,7 @@ proof - have "x - y = x + - y" by simp also have "a * ... = a * x + a * - y" - by (simp only: real_add_mult_distrib2) + by (simp only: right_distrib) also have "... = a * x - a * y" by simp finally show ?thesis . diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Real/HahnBanach/FunctionNorm.thy --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Thu Jan 01 10:06:32 2004 +0100 @@ -127,9 +127,10 @@ note y_rep also have "\f x\ * inverse \x\ \ (c * \x\) * inverse \x\" - proof (rule real_mult_le_le_mono2) + proof (rule mult_right_mono) from c show "\f x\ \ c * \x\" .. - from gt have "0 < inverse \x\" by (rule real_inverse_gt_0) + from gt have "0 < inverse \x\" + by (rule positive_imp_inverse_positive) thus "0 \ inverse \x\" by (rule order_less_imp_le) qed also have "\ = c * (\x\ * inverse \x\)" @@ -211,7 +212,7 @@ with x have neq: "\x\ \ 0" by simp then have "\f x\ = (\f x\ * inverse \x\) * \x\" by simp also have "\ \ \f\\V * \x\" - proof (rule real_mult_le_le_mono2) + proof (rule mult_right_mono) from x show "0 \ \x\" .. from x and neq have "\f x\ * inverse \x\ \ B V f" by (auto simp add: B_def real_divide_def) @@ -246,7 +247,7 @@ by (auto simp add: B_def real_divide_def) note b_rep also have "\f x\ * inverse \x\ \ (c * \x\) * inverse \x\" - proof (rule real_mult_le_le_mono2) + proof (rule mult_right_mono) have "0 < \x\" .. then show "0 \ inverse \x\" by simp from ineq and x show "\f x\ \ c * \x\" .. diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Real/HahnBanach/HahnBanach.thy --- a/src/HOL/Real/HahnBanach/HahnBanach.thy Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Jan 01 10:06:32 2004 +0100 @@ -382,7 +382,7 @@ show "0 \ \f\\F" by (rule ge_zero) from x y show "\x + y\ \ \x\ + \y\" .. qed - also have "\ = \f\\F * \x\ + \f\\F * \y\" by (simp only: real_add_mult_distrib2) + also have "\ = \f\\F * \x\ + \f\\F * \y\" by (simp only: right_distrib) also have "\ = p x + p y" by (simp only: p_def) finally show ?thesis . qed diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Jan 01 10:06:32 2004 +0100 @@ -134,7 +134,7 @@ also from y1 y2 have "h (y1 + y2) = h y1 + h y2" by simp also have "\ + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)" - by (simp add: real_add_mult_distrib) + by (simp add: left_distrib) also from h'_def x1_rep _ HE y1 x0 have "h y1 + a1 * xi = h' x1" by (rule h'_definite [symmetric]) @@ -173,7 +173,7 @@ also from y1 have "h (c \ y1) = c * h y1" by simp also have "\ + (c * a1) * xi = c * (h y1 + a1 * xi)" - by (simp only: real_add_mult_distrib2) + by (simp only: right_distrib) also from h'_def x1_rep _ HE y1 x0 have "h y1 + a1 * xi = h' x1" by (rule h'_definite [symmetric]) finally show ?thesis . diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Real/RComplete.ML --- a/src/HOL/Real/RComplete.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Real/RComplete.ML Thu Jan 01 10:06:32 2004 +0100 @@ -162,7 +162,7 @@ THEN assume_tac 2); by (full_simp_tac (simpset() addsimps [real_diff_def, diff_le_eq RS sym] @ - real_add_ac) 2); + add_ac) 2); by (rtac (setleI RS isUbI) 1); by (Step_tac 1); by (res_inst_tac [("R1.0","x"),("R2.0","y")] real_linear_less2 1); @@ -179,9 +179,9 @@ by (blast_tac (claset() addSIs [isLubD2]) 1 THEN Step_tac 1); by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1); by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI] - addIs [real_add_le_mono1]) 1); + addIs [add_right_mono]) 1); by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI] - addIs [real_add_le_mono1]) 1); + addIs [add_right_mono]) 1); by (Auto_tac); qed "reals_complete"; @@ -202,7 +202,7 @@ (simpset() addsimps [linorder_not_less, inverse_eq_divide]) 2); by (Clarify_tac 2); by (dres_inst_tac [("x","n")] spec 2); -by (dres_inst_tac [("k","real (Suc n)")] (real_mult_le_mono1) 2); +by (dres_inst_tac [("c","real (Suc n)")] (mult_right_mono) 2); by (rtac real_of_nat_ge_zero 2); by (asm_full_simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero RS real_not_refl2 RS not_sym, @@ -214,7 +214,7 @@ by (auto_tac (claset() addIs [isUbI,setleI],simpset())); by (subgoal_tac "ALL m. x*(real(Suc m)) <= t" 1); by (asm_full_simp_tac (simpset() addsimps - [real_of_nat_Suc, real_add_mult_distrib2]) 1); + [real_of_nat_Suc, right_distrib]) 1); by (blast_tac (claset() addIs [isLubD2]) 2); by (asm_full_simp_tac (simpset() addsimps [le_diff_eq RS sym, real_diff_def]) 1); @@ -223,7 +223,7 @@ by (blast_tac (claset() addSIs [isUbI,setleI]) 2); by (dres_inst_tac [("y","t+(-x)")] isLub_le_isUb 1); by (auto_tac (claset(), - simpset() addsimps [real_of_nat_Suc,real_add_mult_distrib2])); + simpset() addsimps [real_of_nat_Suc,right_distrib])); qed "reals_Archimedean"; (*There must be other proofs, e.g. Suc of the largest integer in the @@ -234,20 +234,17 @@ by (res_inst_tac [("x","1")] exI 2); by (auto_tac (claset() addEs [order_less_trans], simpset() addsimps [real_of_nat_one])); -by (ftac (real_inverse_gt_0 RS reals_Archimedean) 1); +by (ftac (positive_imp_inverse_positive RS reals_Archimedean) 1); by (Step_tac 1 THEN res_inst_tac [("x","Suc n")] exI 1); -by (forw_inst_tac [("y","inverse x")] real_mult_less_mono1 1); +by (forw_inst_tac [("b","inverse x")] mult_strict_right_mono 1); by Auto_tac; -by (rtac (thm "less_imp_inverse_less") 1); -by (assume_tac 1); -by (assume_tac 1); qed "reals_Archimedean2"; Goal "0 < x ==> ALL y. EX (n::nat). y < real n * x"; by (Step_tac 1); by (cut_inst_tac [("x","y*inverse(x)")] reals_Archimedean2 1); by (Step_tac 1); -by (forw_inst_tac [("x","y * inverse x")] (real_mult_less_mono1) 1); +by (forw_inst_tac [("a","y * inverse x")] (mult_strict_right_mono) 1); by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,real_of_nat_def])); qed "reals_Archimedean3"; diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Real/RealArith.thy --- a/src/HOL/Real/RealArith.thy Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Real/RealArith.thy Thu Jan 01 10:06:32 2004 +0100 @@ -51,7 +51,7 @@ by simp lemma real_minus1_divide [simp]: "-1/(x::real) = - (1/x)" -by (simp add: real_divide_def real_minus_inverse) +by (simp add: real_divide_def inverse_minus_eq) lemma real_lbound_gt_zero: "[| (0::real) < d1; 0 < d2 |] ==> \e. 0 < e & e < d1 & e < d2" @@ -116,14 +116,14 @@ by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero) lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x" -apply (rule real_leD) +apply (simp add: linorder_not_less) apply (auto intro: abs_ge_self [THEN order_trans]) done text{*Used only in Hyperreal/Lim.ML*} 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_tac a1 = y in add_left_commute [THEN ssubst]) apply (rule real_add_assoc [THEN subst]) apply (rule abs_triangle_ineq) done diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Real/RealBin.ML --- a/src/HOL/Real/RealBin.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Real/RealBin.ML Thu Jan 01 10:06:32 2004 +0100 @@ -65,7 +65,7 @@ (*For specialist use: NOT as default simprules*) Goal "2 * z = (z+z::real)"; -by (simp_tac (simpset () addsimps [lemma, real_add_mult_distrib]) 1); +by (simp_tac (simpset () addsimps [lemma, left_distrib]) 1); qed "real_mult_2"; Goal "z * 2 = (z+z::real)"; @@ -115,8 +115,7 @@ qed "real_minus_1_eq_m1"; Goal "-1 * z = -(z::real)"; -by (simp_tac (simpset() addsimps [real_minus_1_eq_m1 RS sym, - real_mult_minus_1]) 1); +by (simp_tac (simpset() addsimps [real_minus_1_eq_m1 RS sym]) 1); qed "real_mult_minus1"; Goal "z * -1 = -(z::real)"; @@ -195,7 +194,7 @@ (** For combine_numerals **) Goal "i*u + (j*u + k) = (i+j)*u + (k::real)"; -by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib] @ add_ac) 1); +by (asm_simp_tac (simpset() addsimps [left_distrib] @ add_ac) 1); qed "left_real_add_mult_distrib"; @@ -207,33 +206,33 @@ [less_iff_diff_less_0, eq_iff_diff_eq_0, le_iff_diff_le_0]; Goal "!!i::real. (i*u + m = j*u + n) = ((i-j)*u + m = n)"; -by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]@ - real_add_ac@rel_iff_rel_0_rls) 1); +by (asm_simp_tac (simpset() addsimps [real_diff_def, left_distrib]@ + add_ac@rel_iff_rel_0_rls) 1); qed "real_eq_add_iff1"; Goal "!!i::real. (i*u + m = j*u + n) = (m = (j-i)*u + n)"; -by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]@ - real_add_ac@rel_iff_rel_0_rls) 1); +by (asm_simp_tac (simpset() addsimps [real_diff_def, left_distrib]@ + add_ac@rel_iff_rel_0_rls) 1); qed "real_eq_add_iff2"; Goal "!!i::real. (i*u + m < j*u + n) = ((i-j)*u + m < n)"; -by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]@ - real_add_ac@rel_iff_rel_0_rls) 1); +by (asm_simp_tac (simpset() addsimps [real_diff_def, left_distrib]@ + add_ac@rel_iff_rel_0_rls) 1); qed "real_less_add_iff1"; Goal "!!i::real. (i*u + m < j*u + n) = (m < (j-i)*u + n)"; -by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]@ - real_add_ac@rel_iff_rel_0_rls) 1); +by (asm_simp_tac (simpset() addsimps [real_diff_def, left_distrib]@ + add_ac@rel_iff_rel_0_rls) 1); qed "real_less_add_iff2"; Goal "!!i::real. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"; -by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]@ - real_add_ac@rel_iff_rel_0_rls) 1); +by (asm_simp_tac (simpset() addsimps [real_diff_def, left_distrib]@ + add_ac@rel_iff_rel_0_rls) 1); qed "real_le_add_iff1"; Goal "!!i::real. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"; -by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib] - @real_add_ac@rel_iff_rel_0_rls) 1); +by (asm_simp_tac (simpset() addsimps [real_diff_def, left_distrib] + @add_ac@rel_iff_rel_0_rls) 1); qed "real_le_add_iff2"; @@ -344,21 +343,15 @@ bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min]; (*To let us treat subtraction as addition*) -val diff_simps = [real_diff_def, real_minus_add_distrib, real_minus_minus]; - -(*push the unary minus down: - x * y = x * - y -val real_minus_mult_eq_1_to_2 = - [real_minus_mult_eq1 RS sym, real_minus_mult_eq2] MRS trans |> standard; -same as real_minus_mult_commute -*) +val diff_simps = [real_diff_def, minus_add_distrib, minus_minus]; (*to extract again any uncancelled minuses*) val real_minus_from_mult_simps = - [real_minus_minus, real_mult_minus_eq1, real_mult_minus_eq2]; + [minus_minus, minus_mult_left RS sym, minus_mult_right RS sym]; (*combine unary minus with numeric literals, however nested within a product*) val real_mult_minus_simps = - [real_mult_assoc, real_minus_mult_eq1, real_minus_mult_commute]; + [real_mult_assoc, minus_mult_left, real_minus_mult_commute]; (*Apply the given rewrite (if present) just once*) fun trans_tac None = all_tac @@ -367,8 +360,8 @@ (*Final simplification: cancel + and * *) val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq - [real_add_zero_left, real_add_zero_right, - real_mult_0, real_mult_0_right, real_mult_1, real_mult_1_right]; + [add_0, add_0_right, + mult_left_zero, mult_right_zero, mult_1, mult_1_right]; fun prep_simproc (name, pats, proc) = Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc; @@ -383,11 +376,11 @@ val trans_tac = trans_tac val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ - real_minus_simps@real_add_ac)) + real_minus_simps@add_ac)) THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@real_mult_minus_simps)) THEN ALLGOALS (simp_tac (HOL_ss addsimps real_minus_from_mult_simps@ - real_add_ac@real_mult_ac)) + add_ac@mult_ac)) val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) val simplify_meta_eq = simplify_meta_eq end; @@ -451,10 +444,10 @@ val trans_tac = trans_tac val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@ - diff_simps@real_minus_simps@real_add_ac)) + diff_simps@real_minus_simps@add_ac)) THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@real_mult_minus_simps)) THEN ALLGOALS (simp_tac (HOL_ss addsimps real_minus_from_mult_simps@ - real_add_ac@real_mult_ac)) + add_ac@mult_ac)) val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) val simplify_meta_eq = @@ -582,7 +575,7 @@ val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) val T = HOLogic.realT val plus = Const ("op *", [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) - val add_ac = real_mult_ac + val add_ac = mult_ac end; structure Real_Times_Assoc = Assoc_Fold (Real_Times_Assoc_Data); @@ -594,23 +587,4 @@ AddIffs [eq_iff_diff_eq_0 RS sym]; AddIffs [le_iff_diff_le_0 RS sym]; -(** <= monotonicity results: needed for arithmetic **) - -Goal "[| i <= j; (0::real) <= k |] ==> i*k <= j*k"; -by (auto_tac (claset(), - simpset() addsimps [order_le_less, real_mult_less_mono1])); -qed "real_mult_le_mono1"; - -Goal "[| i <= j; (0::real) <= k |] ==> k*i <= k*j"; -by (dtac real_mult_le_mono1 1); -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [real_mult_commute]))); -qed "real_mult_le_mono2"; - -Goal "[| (i::real) <= j; k <= l; 0 <= j; 0 <= k |] ==> i*k <= j*l"; -by (etac (real_mult_le_mono1 RS order_trans) 1); -by (assume_tac 1); -by (etac real_mult_le_mono2 1); -by (assume_tac 1); -qed "real_mult_le_mono"; - Addsimps [real_minus_1_eq_m1]; diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Real/RealDef.thy --- a/src/HOL/Real/RealDef.thy Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Real/RealDef.thy Thu Jan 01 10:06:32 2004 +0100 @@ -107,6 +107,9 @@ real_le_def: "P \ (Q::real) == ~(Q < P)" + real_abs_def: "abs (r::real) == (if 0 \ r then r else -r)" + + syntax (xsymbols) Reals :: "'a set" ("\") Nats :: "'a set" ("\") @@ -182,48 +185,6 @@ apply (simp add: Rep_REAL_inverse) done -(**** real_minus: additive inverse on real ****) - -lemma real_minus_congruent: - "congruent realrel (%p. (%(x,y). realrel``{(y,x)}) p)" -apply (unfold congruent_def, clarify) -apply (simp add: preal_add_commute) -done - -lemma real_minus: - "- (Abs_REAL(realrel``{(x,y)})) = Abs_REAL(realrel `` {(y,x)})" -apply (unfold real_minus_def) -apply (rule_tac f = Abs_REAL in arg_cong) -apply (simp add: realrel_in_real [THEN Abs_REAL_inverse] - UN_equiv_class [OF equiv_realrel real_minus_congruent]) -done - -lemma real_minus_minus: "- (- z) = (z::real)" -apply (rule_tac z = z in eq_Abs_REAL) -apply (simp add: real_minus) -done - -declare real_minus_minus [simp] - -lemma inj_real_minus: "inj(%r::real. -r)" -apply (rule inj_onI) -apply (drule_tac f = uminus in arg_cong) -apply (simp add: real_minus_minus) -done - -lemma real_minus_zero: "- 0 = (0::real)" -apply (unfold real_zero_def) -apply (simp add: real_minus) -done - -declare real_minus_zero [simp] - -lemma real_minus_zero_iff: "(-x = 0) = (x = (0::real))" -apply (rule_tac z = x in eq_Abs_REAL) -apply (auto simp add: real_zero_def real_minus preal_add_ac) -done - -declare real_minus_zero_iff [simp] subsection{*Congruence property for addition*} @@ -258,27 +219,14 @@ apply (simp add: real_add preal_add_assoc) done -(*For AC rewriting*) -lemma real_add_left_commute: "(x::real)+(y+z)=y+(x+z)" - apply (rule mk_left_commute [of "op +"]) - apply (rule real_add_assoc) - apply (rule real_add_commute) - done - - -(* real addition is an AC operator *) -lemmas real_add_ac = real_add_assoc real_add_commute real_add_left_commute - lemma real_add_zero_left: "(0::real) + z = z" apply (unfold real_of_preal_def real_zero_def) apply (rule_tac z = z in eq_Abs_REAL) apply (simp add: real_add preal_add_ac) done -declare real_add_zero_left [simp] lemma real_add_zero_right: "z + (0::real) = z" -by (simp add: real_add_commute) -declare real_add_zero_right [simp] +by (simp add: real_add_zero_left real_add_commute) instance real :: plus_ac0 by (intro_classes, @@ -286,16 +234,27 @@ rule real_add_commute real_add_assoc real_add_zero_left)+) -lemma real_add_minus: "z + (-z) = (0::real)" +subsection{*Additive Inverse on real*} + +lemma real_minus_congruent: + "congruent realrel (%p. (%(x,y). realrel``{(y,x)}) p)" +apply (unfold congruent_def, clarify) +apply (simp add: preal_add_commute) +done + +lemma real_minus: + "- (Abs_REAL(realrel``{(x,y)})) = Abs_REAL(realrel `` {(y,x)})" +apply (unfold real_minus_def) +apply (rule_tac f = Abs_REAL in arg_cong) +apply (simp add: realrel_in_real [THEN Abs_REAL_inverse] + UN_equiv_class [OF equiv_realrel real_minus_congruent]) +done + +lemma real_add_minus_left: "(-z) + z = (0::real)" apply (unfold real_zero_def) apply (rule_tac z = z in eq_Abs_REAL) apply (simp add: real_minus real_add preal_add_commute) done -declare real_add_minus [simp] - -lemma real_add_minus_left: "(-z) + z = (0::real)" -by (simp add: real_add_commute) -declare real_add_minus_left [simp] subsection{*Congruence property for multiplication*} @@ -340,77 +299,12 @@ apply (simp add: preal_add_mult_distrib2 real_mult preal_add_ac preal_mult_ac) done - -(*For AC rewriting*) -lemma real_mult_left_commute: "(x::real)*(y*z)=y*(x*z)" - apply (rule mk_left_commute [of "op *"]) - apply (rule real_mult_assoc) - apply (rule real_mult_commute) - done - -(* real multiplication is an AC operator *) -lemmas real_mult_ac = real_mult_assoc real_mult_commute real_mult_left_commute - lemma real_mult_1: "(1::real) * z = z" apply (unfold real_one_def pnat_one_def) apply (rule_tac z = z in eq_Abs_REAL) -apply (simp add: real_mult preal_add_mult_distrib2 preal_mult_1_right preal_mult_ac preal_add_ac) -done - -declare real_mult_1 [simp] - -lemma real_mult_1_right: "z * (1::real) = z" -by (simp add: real_mult_commute) - -declare real_mult_1_right [simp] - -lemma real_mult_0: "0 * z = (0::real)" -apply (unfold real_zero_def pnat_one_def) -apply (rule_tac z = z in eq_Abs_REAL) -apply (simp add: real_mult preal_add_mult_distrib2 preal_mult_1_right preal_mult_ac preal_add_ac) -done - -lemma real_mult_0_right: "z * 0 = (0::real)" -by (simp add: real_mult_commute real_mult_0) - -declare real_mult_0_right [simp] real_mult_0 [simp] - -lemma real_mult_minus_eq1: "(-x) * (y::real) = -(x * y)" -apply (rule_tac z = x in eq_Abs_REAL) -apply (rule_tac z = y in eq_Abs_REAL) -apply (auto simp add: real_minus real_mult preal_mult_ac preal_add_ac) +apply (simp add: real_mult preal_add_mult_distrib2 preal_mult_1_right + preal_mult_ac preal_add_ac) done -declare real_mult_minus_eq1 [simp] - -lemmas real_minus_mult_eq1 = real_mult_minus_eq1 [symmetric, standard] - -lemma real_mult_minus_eq2: "x * (- y :: real) = -(x * y)" -by (simp add: real_mult_commute [of x]) -declare real_mult_minus_eq2 [simp] - -lemmas real_minus_mult_eq2 = real_mult_minus_eq2 [symmetric, standard] - -lemma real_mult_minus_1: "(- (1::real)) * z = -z" -by simp -declare real_mult_minus_1 [simp] - -lemma real_mult_minus_1_right: "z * (- (1::real)) = -z" -by (subst real_mult_commute, simp) -declare real_mult_minus_1_right [simp] - -lemma real_minus_mult_cancel: "(-x) * (-y) = x * (y::real)" -by simp - -declare real_minus_mult_cancel [simp] - -lemma real_minus_mult_commute: "(-x) * y = x * (- y :: real)" -by simp - -(** Lemmas **) - -lemma real_add_assoc_cong: - "(z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)" -by (simp add: real_add_assoc [symmetric]) lemma real_add_mult_distrib: "((z1::real) + z2) * w = (z1 * w) + (z2 * w)" apply (rule_tac z = z1 in eq_Abs_REAL) @@ -419,17 +313,6 @@ apply (simp add: preal_add_mult_distrib2 real_add real_mult preal_add_ac preal_mult_ac) done -lemma real_add_mult_distrib2: "(w::real) * (z1 + z2) = (w * z1) + (w * z2)" -by (simp add: real_mult_commute [of w] real_add_mult_distrib) - -lemma real_diff_mult_distrib: "((z1::real) - z2) * w = (z1 * w) - (z2 * w)" -apply (unfold real_diff_def) -apply (simp add: real_add_mult_distrib) -done - -lemma real_diff_mult_distrib2: "(w::real) * (z1 - z2) = (w * z1) - (w * z2)" -by (simp add: real_mult_commute [of w] real_diff_mult_distrib) - text{*one and zero are distinct*} lemma real_zero_not_eq_one: "0 ~= (1::real)" apply (unfold real_zero_def real_one_def) @@ -443,36 +326,77 @@ apply (auto simp add: preal_add_commute) done -lemma real_mult_inv_right_ex: - "!!(x::real). x ~= 0 ==> \y. x*y = (1::real)" +lemma real_mult_inv_left_ex: "x ~= 0 ==> \y. y*x = (1::real)" apply (unfold real_zero_def real_one_def) apply (rule_tac z = x in eq_Abs_REAL) apply (cut_tac x = xa and y = y in linorder_less_linear) apply (auto dest!: preal_less_add_left_Ex simp add: real_zero_iff [symmetric]) -apply (rule_tac x = "Abs_REAL (realrel `` { (preal_of_prat (prat_of_pnat 1), pinv (D) + preal_of_prat (prat_of_pnat 1))}) " in exI) -apply (rule_tac [2] x = "Abs_REAL (realrel `` { (pinv (D) + preal_of_prat (prat_of_pnat 1), preal_of_prat (prat_of_pnat 1))}) " in exI) +apply (rule_tac + x = "Abs_REAL (realrel `` { (preal_of_prat (prat_of_pnat 1), + pinv (D) + preal_of_prat (prat_of_pnat 1))}) " + in exI) +apply (rule_tac [2] + x = "Abs_REAL (realrel `` { (pinv (D) + preal_of_prat (prat_of_pnat 1), + preal_of_prat (prat_of_pnat 1))})" + in exI) apply (auto simp add: real_mult pnat_one_def preal_mult_1_right preal_add_mult_distrib2 preal_add_mult_distrib preal_mult_1 preal_mult_inv_right preal_add_ac preal_mult_ac) done -lemma real_mult_inv_left_ex: "x ~= 0 ==> \y. y*x = (1::real)" -apply (drule real_mult_inv_right_ex) -apply (auto simp add: real_mult_commute) -done - lemma real_mult_inv_left: "x ~= 0 ==> inverse(x)*x = (1::real)" apply (unfold real_inverse_def) apply (frule real_mult_inv_left_ex, safe) apply (rule someI2, auto) done -declare real_mult_inv_left [simp] + +instance real :: field +proof + fix x y z :: real + show "(x + y) + z = x + (y + z)" by (rule real_add_assoc) + show "x + y = y + x" by (rule real_add_commute) + show "0 + x = x" by simp + show "- x + x = 0" by (rule real_add_minus_left) + show "x - y = x + (-y)" by (simp add: real_diff_def) + show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc) + show "x * y = y * x" by (rule real_mult_commute) + show "1 * x = x" by (rule real_mult_1) + show "(x + y) * z = x * z + y * z" by (simp add: real_add_mult_distrib) + show "0 \ (1::real)" by (rule real_zero_not_eq_one) + show "x \ 0 ==> inverse x * x = 1" by (rule real_mult_inv_left) + show "y \ 0 ==> x / y = x * inverse y" by (simp add: real_divide_def) +qed + + +(** Inverse of zero! Useful to simplify certain equations **) -lemma real_mult_inv_right: "x ~= 0 ==> x*inverse(x) = (1::real)" -apply (subst real_mult_commute) -apply (auto simp add: real_mult_inv_left) +lemma INVERSE_ZERO: "inverse 0 = (0::real)" +apply (unfold real_inverse_def) +apply (rule someI2) +apply (auto simp add: zero_neq_one) done -declare real_mult_inv_right [simp] + +lemma DIVISION_BY_ZERO: "a / (0::real) = 0" + by (simp add: real_divide_def INVERSE_ZERO) + +instance real :: division_by_zero +proof + fix x :: real + show "inverse 0 = (0::real)" by (rule INVERSE_ZERO) + show "x/0 = 0" by (rule DIVISION_BY_ZERO) +qed + + +(*Pull negations out*) +declare minus_mult_right [symmetric, simp] + minus_mult_left [symmetric, simp] + +text{*Used in RealBin*} +lemma real_minus_mult_commute: "(-x) * y = x * (- y :: real)" +by simp + +lemma real_mult_1_right: "z * (1::real) = z" + by (rule Ring_and_Field.mult_1_right) subsection{*Theorems for Ordering*} @@ -714,8 +638,6 @@ apply (blast intro!: real_of_preal_minus_less_rev1 real_of_preal_minus_less_rev2) done -declare real_of_preal_minus_less_rev_iff [simp] - subsection{*Linearity of the Ordering*} @@ -724,7 +646,8 @@ apply (rule_tac [!] x = y in real_of_preal_trichotomyE) apply (auto dest!: preal_le_anti_sym simp add: preal_less_le_iff real_of_preal_minus_less_zero - real_of_preal_zero_less real_of_preal_minus_less_all) + real_of_preal_zero_less real_of_preal_minus_less_all + real_of_preal_minus_less_rev_iff) done lemma real_neq_iff: "!!w::real. (w ~= z) = (w y ==> x < y | x = y" +apply (unfold real_le_def) +apply (cut_tac real_linear) +apply (blast elim: real_less_irrefl real_less_asym) +done + +lemma real_less_or_eq_imp_le: "z z \(w::real)" +apply (unfold real_le_def) +apply (cut_tac real_linear) +apply (fast elim: real_less_irrefl real_less_asym) +done + +lemma real_le_less: "(x \ (y::real)) = (x < y | x=y)" +by (blast intro!: real_less_or_eq_imp_le dest!: real_le_imp_less_or_eq) + +lemma real_le_refl: "w \ (w::real)" +by (simp add: real_le_less) + +lemma real_le_trans: "[| i \ j; j \ k |] ==> i \ (k::real)" +apply (drule real_le_imp_less_or_eq) +apply (drule real_le_imp_less_or_eq) +apply (rule real_less_or_eq_imp_le) +apply (blast intro: real_less_trans) +done + +lemma real_le_anti_sym: "[| z \ w; w \ z |] ==> z = (w::real)" +apply (drule real_le_imp_less_or_eq) +apply (drule real_le_imp_less_or_eq) +apply (fast elim: real_less_irrefl real_less_asym) +done + +(* Axiom 'order_less_le' of class 'order': *) +lemma real_less_le: "((w::real) < z) = (w \ z & w \ z)" +apply (simp add: real_le_def real_neq_iff) +apply (blast elim!: real_less_asym) +done + +instance real :: order + by (intro_classes, + (assumption | + rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+) + +(* Axiom 'linorder_linear' of class 'linorder': *) +lemma real_le_linear: "(z::real) \ w | w \ z" +apply (simp add: real_le_less) +apply (cut_tac real_linear, blast) +done + +instance real :: linorder + by (intro_classes, rule real_le_linear) + + +subsection{*Theorems About the Ordering*} + +lemma real_gt_zero_preal_Ex: "(0 < x) = (\y. x = real_of_preal y)" +apply (auto simp add: real_of_preal_zero_less) +apply (cut_tac x = x in real_of_preal_trichotomy) +apply (blast elim!: real_less_irrefl real_of_preal_not_minus_gt_zero [THEN notE]) +done + +lemma real_gt_preal_preal_Ex: + "real_of_preal z < x ==> \y. x = real_of_preal y" +by (blast dest!: real_of_preal_zero_less [THEN real_less_trans] + intro: real_gt_zero_preal_Ex [THEN iffD1]) + +lemma real_ge_preal_preal_Ex: + "real_of_preal z \ x ==> \y. x = real_of_preal y" +by (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex) + +lemma real_less_all_preal: "y \ 0 ==> \x. y < real_of_preal x" +by (auto elim: order_le_imp_less_or_eq [THEN disjE] + intro: real_of_preal_zero_less [THEN [2] real_less_trans] + simp add: real_of_preal_zero_less) + +lemma real_less_all_real2: "~ 0 < y ==> \x. y < real_of_preal x" +by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1]) + +lemma real_of_preal_le_iff: + "(real_of_preal m1 \ real_of_preal m2) = (m1 \ m2)" +apply (auto intro!: preal_leI simp add: linorder_not_less [symmetric]) +done + + +subsection{*Monotonicity of Addition*} + +lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y" +apply (auto simp add: real_gt_zero_preal_Ex) +apply (rule_tac x = "y*ya" in exI) +apply (simp (no_asm_use) add: real_of_preal_mult) +done + +(*Alternative definition for real_less*) +lemma real_less_add_positive_left_Ex: "R < S ==> \T::real. 0 < T & R + T = S" +apply (rule_tac x = R in real_of_preal_trichotomyE) +apply (rule_tac [!] x = S in real_of_preal_trichotomyE) +apply (auto dest!: preal_less_add_left_Ex simp add: real_of_preal_not_minus_gt_all real_of_preal_add real_of_preal_not_less_zero real_less_not_refl real_of_preal_not_minus_gt_zero real_of_preal_minus_less_rev_iff) +apply (rule real_of_preal_zero_less) +apply (rule_tac [1] x = "real_of_preal m+real_of_preal ma" in exI) +apply (rule_tac [2] x = "real_of_preal D" in exI) +apply (auto simp add: real_of_preal_minus_less_rev_iff real_of_preal_zero_less real_of_preal_sum_zero_less real_add_assoc) +apply (simp add: real_add_assoc [symmetric]) +done + +lemma real_less_sum_gt_zero: "(W < S) ==> (0 < S + (-W::real))" +apply (drule real_less_add_positive_left_Ex) +apply (auto simp add: add_ac) +done + +lemma real_lemma_change_eq_subj: "!!S::real. T = S + W ==> S = T + (-W)" +by (simp add: add_ac) + +(* FIXME: long! *) +lemma real_sum_gt_zero_less: "(0 < S + (-W::real)) ==> (W < S)" +apply (rule ccontr) +apply (drule linorder_not_less [THEN iffD1, THEN real_le_imp_less_or_eq]) +apply (auto simp add: real_less_not_refl) +apply (drule real_less_add_positive_left_Ex, clarify, simp) +apply (drule real_lemma_change_eq_subj, auto) +apply (drule real_less_sum_gt_zero) +apply (auto elim: real_less_asym simp add: add_left_commute [of W] add_ac) +done + +lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y" +apply (rule real_sum_gt_zero_less) +apply (drule real_less_sum_gt_zero [of x y]) +apply (drule real_mult_order, assumption) +apply (simp add: right_distrib) +done + +lemma real_less_sum_gt_0_iff: "(0 < S + (-W::real)) = (W < S)" +by (blast intro: real_less_sum_gt_zero real_sum_gt_zero_less) + +lemma real_less_eq_diff: "(x (x (y\x) = (y'\x')" +apply (drule real_less_eqI) +apply (simp add: real_le_def) +done + +lemma real_add_left_mono: "x \ y ==> z + x \ z + (y::real)" +apply (rule real_le_eqI [THEN iffD1]) + prefer 2 apply assumption +apply (simp add: real_diff_def add_ac) +done + + +subsection{*The Reals Form an Ordered Field*} + +instance real :: ordered_field +proof + fix x y z :: real + show "x \ y ==> z + x \ z + y" by (rule real_add_left_mono) + show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2) + show "\x\ = (if x < 0 then -x else x)" + by (auto dest: order_le_less_trans simp add: real_abs_def linorder_not_le) +qed + +text{*These two need to be proved in @{text Ring_and_Field}*} +lemma real_add_less_le_mono: "[| w'z |] ==> w' + z' < w + (z::real)" +apply (erule add_strict_right_mono [THEN order_less_le_trans]) +apply (erule add_left_mono) +done + +lemma real_add_le_less_mono: + "!!z z'::real. [| w'\w; z' w' + z' < w + z" +apply (erule add_right_mono [THEN order_le_less_trans]) +apply (erule add_strict_left_mono) +done + +lemma real_zero_less_one: "0 < (1::real)" + by (rule Ring_and_Field.zero_less_one) + +lemma real_le_square [simp]: "(0::real) \ x*x" + by (rule Ring_and_Field.zero_le_square) + + +subsection{*More Lemmas*} + +lemma real_mult_left_cancel: "(c::real) \ 0 ==> (c*a=c*b) = (a=b)" +by auto + +lemma real_mult_right_cancel: "(c::real) \ 0 ==> (a*c=b*c) = (a=b)" +by auto + +text{*The precondition could be weakened to @{term "0\x"}*} +lemma real_mult_less_mono: + "[| u u*x < v* y" + by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) + +lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)" + by (force elim: order_less_asym + simp add: Ring_and_Field.mult_less_cancel_right) + +lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \ y*z) = (x\y)" +by (auto simp add: real_le_def) + +lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \ z*y) = (x\y)" + by (force elim: order_less_asym + simp add: Ring_and_Field.mult_le_cancel_left) + +text{*Only two uses?*} +lemma real_mult_less_mono': + "[| x < y; r1 < r2; (0::real) \ r1; 0 \ x|] ==> r1 * x < r2 * y" + by (rule Ring_and_Field.mult_strict_mono') + +text{*FIXME: delete or at least combine the next two lemmas*} +lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)" +apply (drule Ring_and_Field.equals_zero_I [THEN sym]) +apply (cut_tac x = y in real_le_square) +apply (auto, drule real_le_anti_sym, auto) +done + +lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)" +apply (rule_tac y = x in real_sum_squares_cancel) +apply (simp add: real_add_commute) +done + + +lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y" +apply (drule add_strict_mono [of concl: 0 0], assumption) +apply simp +done + +lemma real_le_add_order: "[| 0 \ x; 0 \ y |] ==> (0::real) \ x + y" +apply (drule order_le_imp_less_or_eq)+ +apply (auto intro: real_add_order order_less_imp_le) +done + + +subsection{*An Embedding of the Naturals in the Reals*} + +lemma real_of_posnat_one: "real_of_posnat 0 = (1::real)" +by (simp add: real_of_posnat_def pnat_one_iff [symmetric] + real_of_preal_def symmetric real_one_def) + +lemma real_of_posnat_two: "real_of_posnat (Suc 0) = (1::real) + (1::real)" +by (simp add: real_of_posnat_def real_of_preal_def real_one_def pnat_two_eq + real_add + prat_of_pnat_add [symmetric] preal_of_prat_add [symmetric] + pnat_add_ac) + +lemma real_of_posnat_add: + "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + (1::real)" +apply (unfold real_of_posnat_def) +apply (simp (no_asm_use) add: real_of_posnat_one [symmetric] real_of_posnat_def real_of_preal_add [symmetric] preal_of_prat_add [symmetric] prat_of_pnat_add [symmetric] pnat_of_nat_add) +done + +lemma real_of_posnat_add_one: + "real_of_posnat (n + 1) = real_of_posnat n + (1::real)" +apply (rule_tac a1 = " (1::real) " in add_right_cancel [THEN iffD1]) +apply (rule real_of_posnat_add [THEN subst]) +apply (simp (no_asm_use) add: real_of_posnat_two real_add_assoc) +done + +lemma real_of_posnat_Suc: + "real_of_posnat (Suc n) = real_of_posnat n + (1::real)" +by (subst real_of_posnat_add_one [symmetric], simp) + +lemma inj_real_of_posnat: "inj(real_of_posnat)" +apply (rule inj_onI) +apply (unfold real_of_posnat_def) +apply (drule inj_real_of_preal [THEN injD]) +apply (drule inj_preal_of_prat [THEN injD]) +apply (drule inj_prat_of_pnat [THEN injD]) +apply (erule inj_pnat_of_nat [THEN injD]) +done + +lemma real_of_nat_zero [simp]: "real (0::nat) = 0" +by (simp add: real_of_nat_def real_of_posnat_one) + +lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)" +by (simp add: real_of_nat_def real_of_posnat_two real_add_assoc) + +lemma real_of_nat_add [simp]: + "real (m + n) = real (m::nat) + real n" +apply (simp add: real_of_nat_def add_ac) +apply (simp add: real_of_posnat_add add_assoc [symmetric]) +apply (simp add: add_commute) +apply (simp add: add_assoc [symmetric]) +done + +(*Not for addsimps: often the LHS is used to represent a positive natural*) +lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)" +by (simp add: real_of_nat_def real_of_posnat_Suc add_ac) + +lemma real_of_nat_less_iff [iff]: + "(real (n::nat) < real m) = (n < m)" +by (auto simp add: real_of_nat_def real_of_posnat_def) + +lemma real_of_nat_le_iff [iff]: "(real (n::nat) \ real m) = (n \ m)" +by (simp add: linorder_not_less [symmetric]) + +lemma inj_real_of_nat: "inj (real :: nat => real)" +apply (rule inj_onI) +apply (auto intro!: inj_real_of_posnat [THEN injD] + simp add: real_of_nat_def add_right_cancel) +done + +lemma real_of_nat_ge_zero [iff]: "0 \ real (n::nat)" +apply (induct_tac "n") +apply (auto simp add: real_of_nat_Suc) +apply (drule real_add_le_less_mono) +apply (rule zero_less_one) +apply (simp add: order_less_imp_le) +done + +lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n" +apply (induct_tac "m") +apply (auto simp add: real_of_nat_Suc left_distrib add_commute) +done + +lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)" +by (auto dest: inj_real_of_nat [THEN injD]) + +lemma real_of_nat_diff [rule_format]: + "n \ m --> real (m - n) = real (m::nat) - real n" +apply (induct_tac "m", simp) +apply (simp add: real_diff_def Suc_diff_le le_Suc_eq real_of_nat_Suc add_ac) +apply (simp add: add_left_commute [of _ "- 1"]) +done + +lemma real_of_nat_zero_iff: "(real (n::nat) = 0) = (n = 0)" + proof + assume "real n = 0" + have "real n = real (0::nat)" by simp + then show "n = 0" by (simp only: real_of_nat_inject) + next + show "n = 0 \ real n = 0" by simp + qed + +lemma real_of_nat_neg_int [simp]: "neg z ==> real (nat z) = 0" +by (simp add: neg_nat real_of_nat_zero) + + +lemma real_inverse_unique: "x*y = (1::real) ==> y = inverse x" +apply (case_tac "x \ 0") +apply (rule_tac c1 = x in real_mult_left_cancel [THEN iffD1], auto) +done + +lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x" +by (auto dest: less_imp_inverse_less) + +lemma real_of_nat_gt_zero_cancel_iff: "(0 < real (n::nat)) = (0 < n)" +by (rule real_of_nat_less_iff [THEN subst], auto) +declare real_of_nat_gt_zero_cancel_iff [simp] + +lemma real_of_nat_le_zero_cancel_iff: "(real (n::nat) <= 0) = (n = 0)" +apply (rule real_of_nat_zero [THEN subst]) +apply (subst real_of_nat_le_iff, auto) +done +declare real_of_nat_le_zero_cancel_iff [simp] + +lemma not_real_of_nat_less_zero: "~ real (n::nat) < 0" +apply (simp (no_asm) add: real_le_def [symmetric] real_of_nat_ge_zero) +done +declare not_real_of_nat_less_zero [simp] + +lemma real_of_nat_ge_zero_cancel_iff [simp]: + "(0 <= real (n::nat)) = (0 <= n)" +apply (simp add: real_le_def le_def) +done + +lemma real_mult_self_sum_ge_zero: "(0::real) \ x*x + y*y" +proof - + have "0 + 0 \ x*x + y*y" by (blast intro: add_mono zero_le_square) + thus ?thesis by simp +qed + + +ML +{* +val real_abs_def = thm "real_abs_def"; + +val real_less_eq_diff = thm "real_less_eq_diff"; + +val real_mult = thm"real_mult"; +val real_mult_commute = thm"real_mult_commute"; +val real_mult_assoc = thm"real_mult_assoc"; +val real_mult_1 = thm"real_mult_1"; +val real_mult_1_right = thm"real_mult_1_right"; +val real_minus_mult_commute = thm"real_minus_mult_commute"; +val preal_le_linear = thm"preal_le_linear"; +val real_mult_inv_left = thm"real_mult_inv_left"; +val real_less_not_refl = thm"real_less_not_refl"; +val real_less_irrefl = thm"real_less_irrefl"; +val real_not_refl2 = thm"real_not_refl2"; +val preal_lemma_trans = thm"preal_lemma_trans"; +val real_less_trans = thm"real_less_trans"; +val real_less_not_sym = thm"real_less_not_sym"; +val real_less_asym = thm"real_less_asym"; +val real_of_preal_add = thm"real_of_preal_add"; +val real_of_preal_mult = thm"real_of_preal_mult"; +val real_of_preal_ExI = thm"real_of_preal_ExI"; +val real_of_preal_ExD = thm"real_of_preal_ExD"; +val real_of_preal_iff = thm"real_of_preal_iff"; +val real_of_preal_trichotomy = thm"real_of_preal_trichotomy"; +val real_of_preal_trichotomyE = thm"real_of_preal_trichotomyE"; +val real_of_preal_lessD = thm"real_of_preal_lessD"; +val real_of_preal_lessI = thm"real_of_preal_lessI"; +val real_of_preal_less_iff1 = thm"real_of_preal_less_iff1"; +val real_of_preal_minus_less_self = thm"real_of_preal_minus_less_self"; +val real_of_preal_minus_less_zero = thm"real_of_preal_minus_less_zero"; +val real_of_preal_not_minus_gt_zero = thm"real_of_preal_not_minus_gt_zero"; +val real_of_preal_zero_less = thm"real_of_preal_zero_less"; +val real_of_preal_not_less_zero = thm"real_of_preal_not_less_zero"; +val real_minus_minus_zero_less = thm"real_minus_minus_zero_less"; +val real_of_preal_sum_zero_less = thm"real_of_preal_sum_zero_less"; +val real_of_preal_minus_less_all = thm"real_of_preal_minus_less_all"; +val real_of_preal_not_minus_gt_all = thm"real_of_preal_not_minus_gt_all"; +val real_of_preal_minus_less_rev1 = thm"real_of_preal_minus_less_rev1"; +val real_of_preal_minus_less_rev2 = thm"real_of_preal_minus_less_rev2"; +val real_linear = thm"real_linear"; +val real_neq_iff = thm"real_neq_iff"; +val real_linear_less2 = thm"real_linear_less2"; +val real_le_imp_less_or_eq = thm"real_le_imp_less_or_eq"; +val real_less_or_eq_imp_le = thm"real_less_or_eq_imp_le"; +val real_le_less = thm"real_le_less"; +val real_le_refl = thm"real_le_refl"; +val real_le_linear = thm"real_le_linear"; +val real_le_trans = thm"real_le_trans"; +val real_le_anti_sym = thm"real_le_anti_sym"; +val real_less_le = thm"real_less_le"; +val real_less_sum_gt_zero = thm"real_less_sum_gt_zero"; +val real_sum_gt_zero_less = thm"real_sum_gt_zero_less"; + +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"; +val real_less_all_preal = thm "real_less_all_preal"; +val real_less_all_real2 = thm "real_less_all_real2"; +val real_of_preal_le_iff = thm "real_of_preal_le_iff"; +val real_mult_order = thm "real_mult_order"; +val real_zero_less_one = thm "real_zero_less_one"; +val real_add_less_le_mono = thm "real_add_less_le_mono"; +val real_add_le_less_mono = thm "real_add_le_less_mono"; +val real_add_order = thm "real_add_order"; +val real_le_add_order = thm "real_le_add_order"; +val real_le_square = thm "real_le_square"; +val real_mult_less_mono2 = thm "real_mult_less_mono2"; + +val real_mult_less_iff1 = thm "real_mult_less_iff1"; +val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1"; +val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2"; +val real_mult_less_mono = thm "real_mult_less_mono"; +val real_mult_less_mono' = thm "real_mult_less_mono'"; +val real_sum_squares_cancel = thm "real_sum_squares_cancel"; +val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2"; + +val real_mult_left_cancel = thm"real_mult_left_cancel"; +val real_mult_right_cancel = thm"real_mult_right_cancel"; +val real_of_posnat_one = thm "real_of_posnat_one"; +val real_of_posnat_two = thm "real_of_posnat_two"; +val real_of_posnat_add = thm "real_of_posnat_add"; +val real_of_posnat_add_one = thm "real_of_posnat_add_one"; +val real_of_nat_zero = thm "real_of_nat_zero"; +val real_of_nat_one = thm "real_of_nat_one"; +val real_of_nat_add = thm "real_of_nat_add"; +val real_of_nat_Suc = thm "real_of_nat_Suc"; +val real_of_nat_less_iff = thm "real_of_nat_less_iff"; +val real_of_nat_le_iff = thm "real_of_nat_le_iff"; +val inj_real_of_nat = thm "inj_real_of_nat"; +val real_of_nat_ge_zero = thm "real_of_nat_ge_zero"; +val real_of_nat_mult = thm "real_of_nat_mult"; +val real_of_nat_inject = thm "real_of_nat_inject"; +val real_of_nat_diff = thm "real_of_nat_diff"; +val real_of_nat_zero_iff = thm "real_of_nat_zero_iff"; +val real_of_nat_neg_int = thm "real_of_nat_neg_int"; +val real_inverse_unique = thm "real_inverse_unique"; +val real_inverse_gt_one = thm "real_inverse_gt_one"; +val real_of_nat_gt_zero_cancel_iff = thm "real_of_nat_gt_zero_cancel_iff"; +val real_of_nat_le_zero_cancel_iff = thm "real_of_nat_le_zero_cancel_iff"; +val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero"; +val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff"; +*} end diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Real/RealInt.thy --- a/src/HOL/Real/RealInt.thy Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Real/RealInt.thy Thu Jan 01 10:06:32 2004 +0100 @@ -6,7 +6,7 @@ header{*Embedding the Integers into the Reals*} -theory RealInt = RealOrd: +theory RealInt = RealDef: defs (overloaded) real_of_int_def: @@ -106,9 +106,8 @@ apply (rule ccontr, drule linorder_not_less [THEN iffD1]) apply (auto simp add: zle_iff_zadd real_of_int_add [symmetric] real_of_int_real_of_nat linorder_not_le [symmetric]) apply (subgoal_tac "~ real y + 0 \ real y + real n") - prefer 2 apply (simp add: ); -apply (simp only: add_le_cancel_left) -apply (simp add: ); + prefer 2 apply simp +apply (simp only: add_le_cancel_left, simp) done lemma real_of_int_inject [iff]: "(real (x::int) = real y) = (x = y)" diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Real/RealOrd.thy --- a/src/HOL/Real/RealOrd.thy Mon Dec 29 06:49:26 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,769 +0,0 @@ -(* Title: Real/RealOrd.thy - ID: $Id$ - Author: Jacques D. Fleuriot and Lawrence C. Paulson - Copyright: 1998 University of Cambridge -*) - -header{*The Reals Form an Ordered Field, etc.*} - -theory RealOrd = RealDef: - -defs (overloaded) - real_abs_def: "abs (r::real) == (if 0 \ r then r else -r)" - - - -subsection{*Properties of Less-Than Or Equals*} - -lemma real_leI: "~(w < z) ==> z \ (w::real)" -by (unfold real_le_def, assumption) - -lemma real_leD: "z\w ==> ~(w<(z::real))" -by (unfold real_le_def, assumption) - -lemma not_real_leE: "~ z \ w ==> w<(z::real)" -by (unfold real_le_def, blast) - -lemma real_le_imp_less_or_eq: "!!(x::real). x \ y ==> x < y | x = y" -apply (unfold real_le_def) -apply (cut_tac real_linear) -apply (blast elim: real_less_irrefl real_less_asym) -done - -lemma real_less_or_eq_imp_le: "z z \(w::real)" -apply (unfold real_le_def) -apply (cut_tac real_linear) -apply (fast elim: real_less_irrefl real_less_asym) -done - -lemma real_le_less: "(x \ (y::real)) = (x < y | x=y)" -by (blast intro!: real_less_or_eq_imp_le dest!: real_le_imp_less_or_eq) - -lemma real_le_refl: "w \ (w::real)" -by (simp add: real_le_less) - -lemma real_le_trans: "[| i \ j; j \ k |] ==> i \ (k::real)" -apply (drule real_le_imp_less_or_eq) -apply (drule real_le_imp_less_or_eq) -apply (rule real_less_or_eq_imp_le) -apply (blast intro: real_less_trans) -done - -lemma real_le_anti_sym: "[| z \ w; w \ z |] ==> z = (w::real)" -apply (drule real_le_imp_less_or_eq) -apply (drule real_le_imp_less_or_eq) -apply (fast elim: real_less_irrefl real_less_asym) -done - -(* Axiom 'order_less_le' of class 'order': *) -lemma real_less_le: "((w::real) < z) = (w \ z & w \ z)" -apply (simp add: real_le_def real_neq_iff) -apply (blast elim!: real_less_asym) -done - -instance real :: order - by (intro_classes, - (assumption | - rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+) - -(* Axiom 'linorder_linear' of class 'linorder': *) -lemma real_le_linear: "(z::real) \ w | w \ z" -apply (simp add: real_le_less) -apply (cut_tac real_linear, blast) -done - -instance real :: linorder - by (intro_classes, rule real_le_linear) - - -subsection{*Theorems About the Ordering*} - -lemma real_gt_zero_preal_Ex: "(0 < x) = (\y. x = real_of_preal y)" -apply (auto simp add: real_of_preal_zero_less) -apply (cut_tac x = x in real_of_preal_trichotomy) -apply (blast elim!: real_less_irrefl real_of_preal_not_minus_gt_zero [THEN notE]) -done - -lemma real_gt_preal_preal_Ex: - "real_of_preal z < x ==> \y. x = real_of_preal y" -by (blast dest!: real_of_preal_zero_less [THEN real_less_trans] - intro: real_gt_zero_preal_Ex [THEN iffD1]) - -lemma real_ge_preal_preal_Ex: - "real_of_preal z \ x ==> \y. x = real_of_preal y" -by (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex) - -lemma real_less_all_preal: "y \ 0 ==> \x. y < real_of_preal x" -by (auto elim: order_le_imp_less_or_eq [THEN disjE] - intro: real_of_preal_zero_less [THEN [2] real_less_trans] - simp add: real_of_preal_zero_less) - -lemma real_less_all_real2: "~ 0 < y ==> \x. y < real_of_preal x" -by (blast intro!: real_less_all_preal real_leI) - -lemma real_of_preal_le_iff: - "(real_of_preal m1 \ real_of_preal m2) = (m1 \ m2)" -apply (auto intro!: preal_leI simp add: linorder_not_less [symmetric]) -done - - -subsection{*Monotonicity of Addition*} - -lemma real_add_left_cancel: "((x::real) + y = x + z) = (y = z)" -apply safe -apply (drule_tac f = "%t. (-x) + t" in arg_cong) -apply (simp add: real_add_assoc [symmetric]) -done - - -lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y" -apply (auto simp add: real_gt_zero_preal_Ex) -apply (rule_tac x = "y*ya" in exI) -apply (simp (no_asm_use) add: real_of_preal_mult) -done - -lemma real_minus_add_distrib [simp]: "-(x + y) = (-x) + (- y :: real)" -apply (rule_tac z = x in eq_Abs_REAL) -apply (rule_tac z = y in eq_Abs_REAL) -apply (auto simp add: real_minus real_add) -done - -(*Alternative definition for real_less*) -lemma real_less_add_positive_left_Ex: "R < S ==> \T::real. 0 < T & R + T = S" -apply (rule_tac x = R in real_of_preal_trichotomyE) -apply (rule_tac [!] x = S in real_of_preal_trichotomyE) -apply (auto dest!: preal_less_add_left_Ex simp add: real_of_preal_not_minus_gt_all real_of_preal_add real_of_preal_not_less_zero real_less_not_refl real_of_preal_not_minus_gt_zero) -apply (rule_tac x = "real_of_preal D" in exI) -apply (rule_tac [2] x = "real_of_preal m+real_of_preal ma" in exI) -apply (rule_tac [3] x = "real_of_preal D" in exI) -apply (auto simp add: real_of_preal_zero_less real_of_preal_sum_zero_less real_add_assoc) -apply (simp add: real_add_assoc [symmetric]) -done - -lemma real_less_sum_gt_zero: "(W < S) ==> (0 < S + (-W::real))" -apply (drule real_less_add_positive_left_Ex) -apply (auto simp add: real_add_minus real_add_zero_right real_add_ac) -done - -lemma real_lemma_change_eq_subj: "!!S::real. T = S + W ==> S = T + (-W)" -by (simp add: real_add_ac) - -(* FIXME: long! *) -lemma real_sum_gt_zero_less: "(0 < S + (-W::real)) ==> (W < S)" -apply (rule ccontr) -apply (drule real_leI [THEN real_le_imp_less_or_eq]) -apply (auto simp add: real_less_not_refl) -apply (drule real_less_add_positive_left_Ex, clarify, simp) -apply (drule real_lemma_change_eq_subj, auto) -apply (drule real_less_sum_gt_zero) -apply (auto elim: real_less_asym simp add: real_add_left_commute [of W] real_add_ac) -done - -lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y" -apply (rule real_sum_gt_zero_less) -apply (drule real_less_sum_gt_zero [of x y]) -apply (drule real_mult_order, assumption) -apply (simp add: real_add_mult_distrib2) -done - -lemma real_less_sum_gt_0_iff: "(0 < S + (-W::real)) = (W < S)" -by (blast intro: real_less_sum_gt_zero real_sum_gt_zero_less) - -lemma real_less_eq_diff: "(x (x (y\x) = (y'\x')" -apply (drule real_less_eqI) -apply (simp add: real_le_def) -done - -lemma real_add_left_mono: "x \ y ==> z + x \ z + (y::real)" -apply (rule real_le_eqI [THEN iffD1]) - prefer 2 apply assumption -apply (simp add: real_diff_def real_add_ac) -done - - -subsection{*The Reals Form an Ordered Field*} - -instance real :: inverse .. - -instance real :: ordered_field -proof - fix x y z :: real - show "(x + y) + z = x + (y + z)" by (rule real_add_assoc) - show "x + y = y + x" by (rule real_add_commute) - show "0 + x = x" by simp - show "- x + x = 0" by simp - show "x - y = x + (-y)" by (simp add: real_diff_def) - show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc) - show "x * y = y * x" by (rule real_mult_commute) - show "1 * x = x" by simp - show "(x + y) * z = x * z + y * z" by (simp add: real_add_mult_distrib) - show "0 \ (1::real)" by (rule real_zero_not_eq_one) - show "x \ y ==> z + x \ z + y" by (rule real_add_left_mono) - show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2) - show "\x\ = (if x < 0 then -x else x)" - by (auto dest: order_le_less_trans simp add: real_abs_def linorder_not_le) - show "x \ 0 ==> inverse x * x = 1" by simp - show "y \ 0 ==> x / y = x * inverse y" by (simp add: real_divide_def) -qed - - -lemma real_zero_less_one: "0 < (1::real)" - by (rule Ring_and_Field.zero_less_one) - -lemma real_add_less_mono: "[| R1 < S1; R2 < S2 |] ==> R1+R2 < S1+(S2::real)" - by (rule Ring_and_Field.add_strict_mono) - -lemma real_add_le_mono: "[|i\j; k\l |] ==> i + k \ j + (l::real)" - by (rule Ring_and_Field.add_mono) - -lemma real_le_minus_iff: "(-s \ -r) = ((r::real) \ s)" - by (rule Ring_and_Field.neg_le_iff_le) - -lemma real_le_square [simp]: "(0::real) \ x*x" - by (rule Ring_and_Field.zero_le_square) - - -subsection{*Division Lemmas*} - -(** Inverse of zero! Useful to simplify certain equations **) - -lemma INVERSE_ZERO: "inverse 0 = (0::real)" -apply (unfold real_inverse_def) -apply (rule someI2) -apply (auto simp add: real_zero_not_eq_one) -done - -lemma DIVISION_BY_ZERO: "a / (0::real) = 0" - by (simp add: real_divide_def INVERSE_ZERO) - -instance real :: division_by_zero -proof - fix x :: real - show "inverse 0 = (0::real)" by (rule INVERSE_ZERO) - show "x/0 = 0" by (rule DIVISION_BY_ZERO) -qed - -lemma real_mult_left_cancel: "(c::real) \ 0 ==> (c*a=c*b) = (a=b)" -by auto - -lemma real_mult_right_cancel: "(c::real) \ 0 ==> (a*c=b*c) = (a=b)" -by auto - -lemma real_mult_left_cancel_ccontr: "c*a \ c*b ==> a \ b" -by auto - -lemma real_mult_right_cancel_ccontr: "a*c \ b*c ==> a \ b" -by auto - -lemma real_inverse_not_zero: "x \ 0 ==> inverse(x::real) \ 0" - by (rule Ring_and_Field.nonzero_imp_inverse_nonzero) - -lemma real_mult_not_zero: "[| x \ 0; y \ 0 |] ==> x * y \ (0::real)" -by simp - -lemma real_inverse_1: "inverse((1::real)) = (1::real)" - by (rule Ring_and_Field.inverse_1) - -lemma real_minus_inverse: "inverse(-x) = -inverse(x::real)" - by (rule Ring_and_Field.inverse_minus_eq) - -lemma real_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::real)" - by (rule Ring_and_Field.inverse_mult_distrib) - -lemma real_add_divide_distrib: "(x+y)/(z::real) = x/z + y/z" - by (rule Ring_and_Field.add_divide_distrib) - - -subsection{*More Lemmas*} - -lemma real_add_right_cancel: "(y + (x::real)= z + x) = (y = z)" - by (rule Ring_and_Field.add_right_cancel) - -lemma real_add_less_mono1: "v < (w::real) ==> v + z < w + z" - by (rule Ring_and_Field.add_strict_right_mono) - -lemma real_add_le_mono1: "v \ (w::real) ==> v + z \ w + z" - by (rule Ring_and_Field.add_right_mono) - -lemma real_add_less_le_mono: "[| w'z |] ==> w' + z' < w + (z::real)" -apply (erule add_strict_right_mono [THEN order_less_le_trans]) -apply (erule add_left_mono) -done - -lemma real_add_le_less_mono: - "!!z z'::real. [| w'\w; z' w' + z' < w + z" -apply (erule add_right_mono [THEN order_le_less_trans]) -apply (erule add_strict_left_mono) -done - -lemma real_less_add_right_cancel: "!!(A::real). A + C < B + C ==> A < B" - by (rule Ring_and_Field.add_less_imp_less_right) - -lemma real_less_add_left_cancel: "!!(A::real). C + A < C + B ==> A < B" - by (rule Ring_and_Field.add_less_imp_less_left) - -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 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_add_right_cancel_less: "(v+z < w+z) = (v < (w::real))" - by (rule Ring_and_Field.add_less_cancel_right) - -lemma real_add_left_cancel_less: "(z+v < z+w) = (v < (w::real))" - by (rule Ring_and_Field.add_less_cancel_left) - -lemma real_add_right_cancel_le: "(v+z \ w+z) = (v \ (w::real))" - by (rule Ring_and_Field.add_le_cancel_right) - -lemma real_add_left_cancel_le: "(z+v \ z+w) = (v \ (w::real))" - by (rule Ring_and_Field.add_le_cancel_left) - - -subsection{*Inverse and Division*} - -lemma real_inverse_gt_0: "0 < x ==> 0 < inverse (x::real)" - 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.negative_imp_inverse_negative) - -lemma real_mult_less_mono1: "[| (0::real) < z; x < y |] ==> x*z < y*z" - by (rule Ring_and_Field.mult_strict_right_mono) - -text{*The precondition could be weakened to @{term "0\x"}*} -lemma real_mult_less_mono: - "[| u u*x < v* y" - by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) - -lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)" - by (force elim: order_less_asym - simp add: Ring_and_Field.mult_less_cancel_right) - -lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \ y*z) = (x\y)" -by (auto simp add: real_le_def) - -lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \ z*y) = (x\y)" - by (force elim: order_less_asym - simp add: Ring_and_Field.mult_le_cancel_left) - -text{*Only two uses?*} -lemma real_mult_less_mono': - "[| x < y; r1 < r2; (0::real) \ r1; 0 \ x|] ==> r1 * x < r2 * y" - by (rule Ring_and_Field.mult_strict_mono') - -lemma real_inverse_less_swap: - "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)" - by (rule Ring_and_Field.less_imp_inverse_less) - -(*FIXME: remove the [iff], since the general theorem is already [simp]*) -lemma real_mult_is_0 [iff]: "(x*y = 0) = (x = 0 | y = (0::real))" -by (rule Ring_and_Field.mult_eq_0_iff) - -lemma real_inverse_add: - "[| x \ 0; y \ 0 |] - ==> inverse x + inverse y = (x + y) * inverse (x * (y::real))" -by (simp add: Ring_and_Field.inverse_add mult_assoc) - -text{*FIXME: delete or at least combine the next two lemmas*} -lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)" -apply (drule Ring_and_Field.equals_zero_I [THEN sym]) -apply (cut_tac x = y in real_le_square) -apply (auto, drule real_le_anti_sym, auto) -done - -lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)" -apply (rule_tac y = x in real_sum_squares_cancel) -apply (simp add: real_add_commute) -done - - -subsection{*Convenient Biconditionals for Products of Signs*} - -lemma real_0_less_mult_iff: "((0::real) < x*y) = (0x*y) = (0\x & 0\y | x\0 & y\0)" - by (rule Ring_and_Field.zero_le_mult_iff) - -lemma real_mult_less_0_iff: "(x*y < (0::real)) = (0 (0::real)) = (0\x & y\0 | x\0 & 0\y)" - by (rule Ring_and_Field.mult_le_0_iff) - -subsection{*Hardly Used Theorems to be Deleted*} - -lemma real_add_less_mono2: "!!(A::real). A < B ==> C + A < C + B" -by simp - -lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y" -apply (erule order_less_trans) -apply (drule real_add_less_mono2, simp) -done - -lemma real_le_add_order: "[| 0 \ x; 0 \ y |] ==> (0::real) \ x + y" -apply (drule order_le_imp_less_or_eq)+ -apply (auto intro: real_add_order order_less_imp_le) -done - - -subsection{*An Embedding of the Naturals in the Reals*} - -lemma real_of_posnat_one: "real_of_posnat 0 = (1::real)" -by (simp add: real_of_posnat_def pnat_one_iff [symmetric] - real_of_preal_def symmetric real_one_def) - -lemma real_of_posnat_two: "real_of_posnat (Suc 0) = (1::real) + (1::real)" -by (simp add: real_of_posnat_def real_of_preal_def real_one_def pnat_two_eq - real_add - prat_of_pnat_add [symmetric] preal_of_prat_add [symmetric] - pnat_add_ac) - -lemma real_of_posnat_add: - "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + (1::real)" -apply (unfold real_of_posnat_def) -apply (simp (no_asm_use) add: real_of_posnat_one [symmetric] real_of_posnat_def real_of_preal_add [symmetric] preal_of_prat_add [symmetric] prat_of_pnat_add [symmetric] pnat_of_nat_add) -done - -lemma real_of_posnat_add_one: - "real_of_posnat (n + 1) = real_of_posnat n + (1::real)" -apply (rule_tac x1 = " (1::real) " in real_add_right_cancel [THEN iffD1]) -apply (rule real_of_posnat_add [THEN subst]) -apply (simp (no_asm_use) add: real_of_posnat_two real_add_assoc) -done - -lemma real_of_posnat_Suc: - "real_of_posnat (Suc n) = real_of_posnat n + (1::real)" -by (subst real_of_posnat_add_one [symmetric], simp) - -lemma inj_real_of_posnat: "inj(real_of_posnat)" -apply (rule inj_onI) -apply (unfold real_of_posnat_def) -apply (drule inj_real_of_preal [THEN injD]) -apply (drule inj_preal_of_prat [THEN injD]) -apply (drule inj_prat_of_pnat [THEN injD]) -apply (erule inj_pnat_of_nat [THEN injD]) -done - -lemma real_of_nat_zero [simp]: "real (0::nat) = 0" -by (simp add: real_of_nat_def real_of_posnat_one) - -lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)" -by (simp add: real_of_nat_def real_of_posnat_two real_add_assoc) - -lemma real_of_nat_add [simp]: - "real (m + n) = real (m::nat) + real n" -apply (simp add: real_of_nat_def add_ac) -apply (simp add: real_of_posnat_add add_assoc [symmetric]) -apply (simp add: add_commute) -apply (simp add: add_assoc [symmetric]) -done - -(*Not for addsimps: often the LHS is used to represent a positive natural*) -lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)" -by (simp add: real_of_nat_def real_of_posnat_Suc real_add_ac) - -lemma real_of_nat_less_iff [iff]: - "(real (n::nat) < real m) = (n < m)" -by (auto simp add: real_of_nat_def real_of_posnat_def) - -lemma real_of_nat_le_iff [iff]: "(real (n::nat) \ real m) = (n \ m)" -by (simp add: linorder_not_less [symmetric]) - -lemma inj_real_of_nat: "inj (real :: nat => real)" -apply (rule inj_onI) -apply (auto intro!: inj_real_of_posnat [THEN injD] - simp add: real_of_nat_def real_add_right_cancel) -done - -lemma real_of_nat_ge_zero [iff]: "0 \ real (n::nat)" -apply (induct_tac "n") -apply (auto simp add: real_of_nat_Suc) -apply (drule real_add_le_less_mono) -apply (rule real_zero_less_one) -apply (simp add: order_less_imp_le) -done - -lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n" -apply (induct_tac "m") -apply (auto simp add: real_of_nat_Suc real_add_mult_distrib real_add_commute) -done - -lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)" -by (auto dest: inj_real_of_nat [THEN injD]) - -lemma real_of_nat_diff [rule_format]: - "n \ m --> real (m - n) = real (m::nat) - real n" -apply (induct_tac "m", simp) -apply (simp add: real_diff_def Suc_diff_le le_Suc_eq real_of_nat_Suc add_ac) -apply (simp add: add_left_commute [of _ "- 1"]) -done - -lemma real_of_nat_zero_iff: "(real (n::nat) = 0) = (n = 0)" - proof - assume "real n = 0" - have "real n = real (0::nat)" by simp - then show "n = 0" by (simp only: real_of_nat_inject) - next - show "n = 0 \ real n = 0" by simp - qed - -lemma real_of_nat_neg_int [simp]: "neg z ==> real (nat z) = 0" -by (simp add: neg_nat real_of_nat_zero) - - -lemma real_mult_le_le_mono1: "[| (0::real) <=z; x<=y |] ==> z*x<=z*y" - by (rule Ring_and_Field.mult_left_mono) - -lemma real_mult_le_le_mono2: "[| (0::real)<=z; x<=y |] ==> x*z<=y*z" - by (rule Ring_and_Field.mult_right_mono) - -(*Used just below and in HahnBanach/Aux.thy*) -lemma real_mult_le_less_mono1: "[| (0::real) \ z; x < y |] ==> x*z \ y*z" -apply (rule real_less_or_eq_imp_le) -apply (drule order_le_imp_less_or_eq) -apply (auto intro: real_mult_less_mono1) -done - -lemma real_inverse_unique: "x*y = (1::real) ==> y = inverse x" -apply (case_tac "x \ 0") -apply (rule_tac c1 = x in real_mult_left_cancel [THEN iffD1], auto) -done - -lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x" -by (auto dest: real_inverse_less_swap) - -lemma real_of_nat_gt_zero_cancel_iff: "(0 < real (n::nat)) = (0 < n)" -by (rule real_of_nat_less_iff [THEN subst], auto) -declare real_of_nat_gt_zero_cancel_iff [simp] - -lemma real_of_nat_le_zero_cancel_iff: "(real (n::nat) <= 0) = (n = 0)" -apply (rule real_of_nat_zero [THEN subst]) -apply (subst real_of_nat_le_iff, auto) -done -declare real_of_nat_le_zero_cancel_iff [simp] - -lemma not_real_of_nat_less_zero: "~ real (n::nat) < 0" -apply (simp (no_asm) add: real_le_def [symmetric] real_of_nat_ge_zero) -done -declare not_real_of_nat_less_zero [simp] - -lemma real_of_nat_ge_zero_cancel_iff: - "(0 <= real (n::nat)) = (0 <= n)" -apply (unfold real_le_def le_def) -apply (simp (no_asm)) -done -declare real_of_nat_ge_zero_cancel_iff [simp] - -lemma real_of_nat_num_if: - "real n = (if n=0 then 0 else 1 + real ((n::nat) - 1))" -apply (case_tac "n", simp) -apply (simp add: real_of_nat_Suc add_commute) -done - -lemma real_mult_self_sum_ge_zero: "(0::real) \ x*x + y*y" -proof - - have "0 + 0 \ x*x + y*y" by (blast intro: add_mono zero_le_square) - thus ?thesis by simp -qed - -declare real_mult_self_sum_ge_zero [simp] - -ML -{* -val real_abs_def = thm "real_abs_def"; - -val real_less_eq_diff = thm "real_less_eq_diff"; - -val real_add_right_cancel = thm"real_add_right_cancel"; -val real_mult_congruent2_lemma = thm"real_mult_congruent2_lemma"; -val real_mult_congruent2 = thm"real_mult_congruent2"; -val real_mult = thm"real_mult"; -val real_mult_commute = thm"real_mult_commute"; -val real_mult_assoc = thm"real_mult_assoc"; -val real_mult_left_commute = thm"real_mult_left_commute"; -val real_mult_1 = thm"real_mult_1"; -val real_mult_1_right = thm"real_mult_1_right"; -val real_mult_0 = thm"real_mult_0"; -val real_mult_0_right = thm"real_mult_0_right"; -val real_mult_minus_eq1 = thm"real_mult_minus_eq1"; -val real_minus_mult_eq1 = thm"real_minus_mult_eq1"; -val real_mult_minus_eq2 = thm"real_mult_minus_eq2"; -val real_minus_mult_eq2 = thm"real_minus_mult_eq2"; -val real_mult_minus_1 = thm"real_mult_minus_1"; -val real_mult_minus_1_right = thm"real_mult_minus_1_right"; -val real_minus_mult_cancel = thm"real_minus_mult_cancel"; -val real_minus_mult_commute = thm"real_minus_mult_commute"; -val real_add_assoc_cong = thm"real_add_assoc_cong"; -val real_add_mult_distrib = thm"real_add_mult_distrib"; -val real_add_mult_distrib2 = thm"real_add_mult_distrib2"; -val real_diff_mult_distrib = thm"real_diff_mult_distrib"; -val real_diff_mult_distrib2 = thm"real_diff_mult_distrib2"; -val real_zero_not_eq_one = thm"real_zero_not_eq_one"; -val real_zero_iff = thm"real_zero_iff"; -val preal_le_linear = thm"preal_le_linear"; -val real_mult_inv_right_ex = thm"real_mult_inv_right_ex"; -val real_mult_inv_left_ex = thm"real_mult_inv_left_ex"; -val real_mult_inv_left = thm"real_mult_inv_left"; -val real_mult_inv_right = thm"real_mult_inv_right"; -val preal_lemma_eq_rev_sum = thm"preal_lemma_eq_rev_sum"; -val preal_add_left_commute_cancel = thm"preal_add_left_commute_cancel"; -val preal_lemma_for_not_refl = thm"preal_lemma_for_not_refl"; -val real_less_not_refl = thm"real_less_not_refl"; -val real_less_irrefl = thm"real_less_irrefl"; -val real_not_refl2 = thm"real_not_refl2"; -val preal_lemma_trans = thm"preal_lemma_trans"; -val real_less_trans = thm"real_less_trans"; -val real_less_not_sym = thm"real_less_not_sym"; -val real_less_asym = thm"real_less_asym"; -val real_of_preal_add = thm"real_of_preal_add"; -val real_of_preal_mult = thm"real_of_preal_mult"; -val real_of_preal_ExI = thm"real_of_preal_ExI"; -val real_of_preal_ExD = thm"real_of_preal_ExD"; -val real_of_preal_iff = thm"real_of_preal_iff"; -val real_of_preal_trichotomy = thm"real_of_preal_trichotomy"; -val real_of_preal_trichotomyE = thm"real_of_preal_trichotomyE"; -val real_of_preal_lessD = thm"real_of_preal_lessD"; -val real_of_preal_lessI = thm"real_of_preal_lessI"; -val real_of_preal_less_iff1 = thm"real_of_preal_less_iff1"; -val real_of_preal_minus_less_self = thm"real_of_preal_minus_less_self"; -val real_of_preal_minus_less_zero = thm"real_of_preal_minus_less_zero"; -val real_of_preal_not_minus_gt_zero = thm"real_of_preal_not_minus_gt_zero"; -val real_of_preal_zero_less = thm"real_of_preal_zero_less"; -val real_of_preal_not_less_zero = thm"real_of_preal_not_less_zero"; -val real_minus_minus_zero_less = thm"real_minus_minus_zero_less"; -val real_of_preal_sum_zero_less = thm"real_of_preal_sum_zero_less"; -val real_of_preal_minus_less_all = thm"real_of_preal_minus_less_all"; -val real_of_preal_not_minus_gt_all = thm"real_of_preal_not_minus_gt_all"; -val real_of_preal_minus_less_rev1 = thm"real_of_preal_minus_less_rev1"; -val real_of_preal_minus_less_rev2 = thm"real_of_preal_minus_less_rev2"; -val real_of_preal_minus_less_rev_iff = thm"real_of_preal_minus_less_rev_iff"; -val real_linear = thm"real_linear"; -val real_neq_iff = thm"real_neq_iff"; -val real_linear_less2 = thm"real_linear_less2"; -val real_leI = thm"real_leI"; -val real_leD = thm"real_leD"; -val not_real_leE = thm"not_real_leE"; -val real_le_imp_less_or_eq = thm"real_le_imp_less_or_eq"; -val real_less_or_eq_imp_le = thm"real_less_or_eq_imp_le"; -val real_le_less = thm"real_le_less"; -val real_le_refl = thm"real_le_refl"; -val real_le_linear = thm"real_le_linear"; -val real_le_trans = thm"real_le_trans"; -val real_le_anti_sym = thm"real_le_anti_sym"; -val real_less_le = thm"real_less_le"; -val real_minus_zero_less_iff = thm"real_minus_zero_less_iff"; -val real_minus_zero_less_iff2 = thm"real_minus_zero_less_iff2"; -val real_less_add_positive_left_Ex = thm"real_less_add_positive_left_Ex"; -val real_less_sum_gt_zero = thm"real_less_sum_gt_zero"; -val real_sum_gt_zero_less = thm"real_sum_gt_zero_less"; - -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"; -val real_less_all_preal = thm "real_less_all_preal"; -val real_less_all_real2 = thm "real_less_all_real2"; -val real_of_preal_le_iff = thm "real_of_preal_le_iff"; -val real_mult_order = thm "real_mult_order"; -val real_zero_less_one = thm "real_zero_less_one"; -val real_add_right_cancel_less = thm "real_add_right_cancel_less"; -val real_add_left_cancel_less = thm "real_add_left_cancel_less"; -val real_add_right_cancel_le = thm "real_add_right_cancel_le"; -val real_add_left_cancel_le = thm "real_add_left_cancel_le"; -val real_add_less_mono1 = thm "real_add_less_mono1"; -val real_add_le_mono1 = thm "real_add_le_mono1"; -val real_add_less_le_mono = thm "real_add_less_le_mono"; -val real_add_le_less_mono = thm "real_add_le_less_mono"; -val real_add_less_mono2 = thm "real_add_less_mono2"; -val real_less_add_right_cancel = thm "real_less_add_right_cancel"; -val real_less_add_left_cancel = thm "real_less_add_left_cancel"; -val real_le_add_right_cancel = thm "real_le_add_right_cancel"; -val real_le_add_left_cancel = thm "real_le_add_left_cancel"; -val real_add_order = thm "real_add_order"; -val real_le_add_order = thm "real_le_add_order"; -val real_add_less_mono = thm "real_add_less_mono"; -val real_add_le_mono = thm "real_add_le_mono"; -val real_le_minus_iff = thm "real_le_minus_iff"; -val real_le_square = thm "real_le_square"; -val real_mult_less_mono1 = thm "real_mult_less_mono1"; -val real_mult_less_mono2 = thm "real_mult_less_mono2"; - -val real_inverse_gt_0 = thm "real_inverse_gt_0"; -val real_inverse_less_0 = thm "real_inverse_less_0"; -val real_mult_less_iff1 = thm "real_mult_less_iff1"; -val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1"; -val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2"; -val real_mult_less_mono = thm "real_mult_less_mono"; -val real_mult_less_mono' = thm "real_mult_less_mono'"; -val real_inverse_less_swap = thm "real_inverse_less_swap"; -val real_mult_is_0 = thm "real_mult_is_0"; -val real_inverse_add = thm "real_inverse_add"; -val real_sum_squares_cancel = thm "real_sum_squares_cancel"; -val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2"; -val real_0_less_mult_iff = thm "real_0_less_mult_iff"; -val real_0_le_mult_iff = thm "real_0_le_mult_iff"; -val real_mult_less_0_iff = thm "real_mult_less_0_iff"; -val real_mult_le_0_iff = thm "real_mult_le_0_iff"; - -val INVERSE_ZERO = thm"INVERSE_ZERO"; -val DIVISION_BY_ZERO = thm"DIVISION_BY_ZERO"; -val real_mult_left_cancel = thm"real_mult_left_cancel"; -val real_mult_right_cancel = thm"real_mult_right_cancel"; -val real_mult_left_cancel_ccontr = thm"real_mult_left_cancel_ccontr"; -val real_mult_right_cancel_ccontr = thm"real_mult_right_cancel_ccontr"; -val real_inverse_not_zero = thm"real_inverse_not_zero"; -val real_mult_not_zero = thm"real_mult_not_zero"; -val real_inverse_1 = thm"real_inverse_1"; -val real_minus_inverse = thm"real_minus_inverse"; -val real_inverse_distrib = thm"real_inverse_distrib"; -val real_add_divide_distrib = thm"real_add_divide_distrib"; - -val real_of_posnat_one = thm "real_of_posnat_one"; -val real_of_posnat_two = thm "real_of_posnat_two"; -val real_of_posnat_add = thm "real_of_posnat_add"; -val real_of_posnat_add_one = thm "real_of_posnat_add_one"; -val real_of_posnat_Suc = thm "real_of_posnat_Suc"; -val inj_real_of_posnat = thm "inj_real_of_posnat"; -val real_of_nat_zero = thm "real_of_nat_zero"; -val real_of_nat_one = thm "real_of_nat_one"; -val real_of_nat_add = thm "real_of_nat_add"; -val real_of_nat_Suc = thm "real_of_nat_Suc"; -val real_of_nat_less_iff = thm "real_of_nat_less_iff"; -val real_of_nat_le_iff = thm "real_of_nat_le_iff"; -val inj_real_of_nat = thm "inj_real_of_nat"; -val real_of_nat_ge_zero = thm "real_of_nat_ge_zero"; -val real_of_nat_mult = thm "real_of_nat_mult"; -val real_of_nat_inject = thm "real_of_nat_inject"; -val real_of_nat_diff = thm "real_of_nat_diff"; -val real_of_nat_zero_iff = thm "real_of_nat_zero_iff"; -val real_of_nat_neg_int = thm "real_of_nat_neg_int"; - -val real_mult_le_le_mono1 = thm "real_mult_le_le_mono1"; -val real_mult_le_le_mono2 = thm "real_mult_le_le_mono2"; -val real_inverse_unique = thm "real_inverse_unique"; -val real_inverse_gt_one = thm "real_inverse_gt_one"; -val real_of_nat_gt_zero_cancel_iff = thm "real_of_nat_gt_zero_cancel_iff"; -val real_of_nat_le_zero_cancel_iff = thm "real_of_nat_le_zero_cancel_iff"; -val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero"; -val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff"; -val real_of_nat_num_if = thm "real_of_nat_num_if"; - -val real_minus_add_distrib = thm"real_minus_add_distrib"; -val real_add_left_cancel = thm"real_add_left_cancel"; -val real_mult_self_sum_ge_zero = thm "real_mult_self_sum_ge_zero"; -*} - -end diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Real/RealPow.thy --- a/src/HOL/Real/RealPow.thy Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Real/RealPow.thy Thu Jan 01 10:06:32 2004 +0100 @@ -28,7 +28,7 @@ lemma realpow_inverse: "inverse ((r::real) ^ n) = (inverse r) ^ n" apply (induct_tac "n") -apply (auto simp add: real_inverse_distrib) +apply (auto simp add: inverse_mult_distrib) done lemma realpow_abs: "abs(r ^ n) = abs(r::real) ^ n" @@ -38,7 +38,7 @@ lemma realpow_add: "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)" apply (induct_tac "n") -apply (auto simp add: real_mult_ac) +apply (auto simp add: mult_ac) done lemma realpow_one [simp]: "(r::real) ^ 1 = r" @@ -49,17 +49,17 @@ lemma realpow_gt_zero [rule_format]: "(0::real) < r --> 0 < r ^ n" apply (induct_tac "n") -apply (auto intro: real_mult_order simp add: real_zero_less_one) +apply (auto intro: real_mult_order simp add: zero_less_one) done lemma realpow_ge_zero [rule_format]: "(0::real) \ r --> 0 \ r ^ n" apply (induct_tac "n") -apply (auto simp add: real_0_le_mult_iff) +apply (auto simp add: zero_le_mult_iff) done lemma realpow_le [rule_format]: "(0::real) \ x & x \ y --> x ^ n \ y ^ n" apply (induct_tac "n") -apply (auto intro!: real_mult_le_mono) +apply (auto intro!: mult_mono) apply (simp (no_asm_simp) add: realpow_ge_zero) done @@ -90,7 +90,7 @@ lemma realpow_mult: "((r::real) * s) ^ n = (r ^ n) * (s ^ n)" apply (induct_tac "n") -apply (auto simp add: real_mult_ac) +apply (auto simp add: mult_ac) done lemma realpow_two_le [simp]: "(0::real) \ r^ Suc (Suc 0)" @@ -106,14 +106,15 @@ apply auto apply (cut_tac real_zero_less_one) apply (frule_tac x = 0 in order_less_trans, assumption) -apply (drule_tac z = r and x = 1 in real_mult_less_mono1) -apply (auto intro: order_less_trans) +apply (frule_tac c = r and a = 1 in mult_strict_right_mono) +apply assumption; +apply (simp add: ); done lemma realpow_ge_one [rule_format]: "(1::real) < r --> 1 \ r ^ n" apply (induct_tac "n", auto) apply (subgoal_tac "1*1 \ r * r^n") -apply (rule_tac [2] real_mult_le_mono, auto) +apply (rule_tac [2] mult_mono, auto) done lemma realpow_ge_one2: "(1::real) \ r ==> 1 \ r ^ n" @@ -170,7 +171,7 @@ apply (simp_all (no_asm_simp)) apply clarify apply (subgoal_tac "r * r ^ na \ 1 * r ^ n", simp) -apply (rule real_mult_le_mono) +apply (rule mult_mono) apply (auto simp add: realpow_ge_zero less_Suc_eq) done @@ -237,7 +238,7 @@ lemma realpow_two_diff: "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)" apply (unfold real_diff_def) -apply (simp add: real_add_mult_distrib2 real_add_mult_distrib real_mult_ac) +apply (simp add: right_distrib left_distrib mult_ac) done lemma realpow_two_disj: "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)" @@ -247,7 +248,7 @@ (* used in Transc *) lemma realpow_diff: "[|(x::real) \ 0; m \ n |] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)" -by (auto simp add: le_eq_less_or_eq less_iff_Suc_add realpow_add realpow_not_zero real_mult_ac) +by (auto simp add: le_eq_less_or_eq less_iff_Suc_add realpow_add realpow_not_zero mult_ac) lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)" apply (induct_tac "n") @@ -256,7 +257,7 @@ lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)" apply (induct_tac "n") -apply (auto simp add: real_of_nat_mult real_0_less_mult_iff) +apply (auto simp add: real_of_nat_mult zero_less_mult_iff) done lemma realpow_increasing: @@ -284,12 +285,12 @@ lemma zero_less_realpow_abs_iff [simp]: "(0 < (abs x)^n) = (x \ (0::real) | n=0)" apply (induct_tac "n") -apply (auto simp add: real_0_less_mult_iff) +apply (auto simp add: zero_less_mult_iff) done lemma zero_le_realpow_abs [simp]: "(0::real) \ (abs x)^n" apply (induct_tac "n") -apply (auto simp add: real_0_le_mult_iff) +apply (auto simp add: zero_le_mult_iff) done @@ -332,7 +333,7 @@ by (auto intro: real_sum_squares_cancel) lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)" -apply (auto simp add: real_add_mult_distrib real_add_mult_distrib2 real_diff_def) +apply (auto simp add: left_distrib right_distrib real_diff_def) done lemma real_mult_is_one: "(x*x = (1::real)) = (x = 1 | x = - 1)" @@ -357,14 +358,14 @@ ==> inverse x * y < inverse x1 * u" apply (rule_tac c=x in mult_less_imp_less_left) apply (auto simp add: real_mult_assoc [symmetric]) -apply (simp (no_asm) add: real_mult_ac) +apply (simp (no_asm) add: mult_ac) apply (rule_tac c=x1 in mult_less_imp_less_right) -apply (auto simp add: real_mult_ac) +apply (auto simp add: mult_ac) done text{*Used once: in Hyperreal/Transcendental.ML*} lemma real_mult_inverse_cancel2: "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1" -apply (auto dest: real_mult_inverse_cancel simp add: real_mult_ac) +apply (auto dest: real_mult_inverse_cancel simp add: mult_ac) done lemma inverse_real_of_nat_gt_zero: "0 < inverse (real (Suc n))" @@ -403,18 +404,18 @@ lemma realpow_ge_zero2 [rule_format (no_asm)]: "(0::real) \ r --> 0 \ r ^ n" apply (induct_tac "n") -apply (auto simp add: real_0_le_mult_iff) +apply (auto simp add: zero_le_mult_iff) done lemma realpow_le2 [rule_format (no_asm)]: "(0::real) \ x & x \ y --> x ^ n \ y ^ n" apply (induct_tac "n") -apply (auto intro!: real_mult_le_mono simp add: realpow_ge_zero2) +apply (auto intro!: mult_mono simp add: realpow_ge_zero2) done lemma realpow_Suc_gt_one: "(1::real) < r ==> 1 < r ^ (Suc n)" apply (frule_tac n = "n" in realpow_ge_one) apply (drule real_le_imp_less_or_eq, safe) -apply (frule real_zero_less_one [THEN real_less_trans]) +apply (frule zero_less_one [THEN real_less_trans]) apply (drule_tac y = "r ^ n" in real_mult_less_mono2) apply assumption apply (auto dest: real_less_trans) diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Real/real_arith.ML --- a/src/HOL/Real/real_arith.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Real/real_arith.ML Thu Jan 01 10:06:32 2004 +0100 @@ -34,7 +34,7 @@ val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps real_minus_from_mult_simps @ mult_1s)) THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps)) - THEN ALLGOALS (simp_tac (HOL_ss addsimps real_mult_ac)) + THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac)) val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps rel_real_number_of@bin_simps)) val simplify_meta_eq = simplify_meta_eq @@ -155,7 +155,7 @@ val dest_coeff = dest_coeff val find_first = find_first [] val trans_tac = trans_tac - val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@real_mult_ac)) + val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac)) end; structure EqCancelFactor = ExtractCommonTermFun @@ -210,16 +210,11 @@ (****Augmentation of real linear arithmetic with rational coefficient handling****) -val divide_1 = thm"divide_1"; - -val times_divide_eq_left = thm"times_divide_eq_left"; -val times_divide_eq_right = thm"times_divide_eq_right"; - local (* reduce contradictory <= to False *) val simps = [True_implies_equals, - inst "w" "number_of ?v" real_add_mult_distrib2, + inst "a" "(number_of ?v)::real" right_distrib, divide_1,times_divide_eq_right,times_divide_eq_left]; val simprocs = [real_cancel_numeral_factors_divide, @@ -230,8 +225,8 @@ val real_mult_mono_thms = [(rotate_prems 1 real_mult_less_mono2, cvar(real_mult_less_mono2, hd(prems_of real_mult_less_mono2))), - (real_mult_le_mono2, - cvar(real_mult_le_mono2, hd(tl(prems_of real_mult_le_mono2))))] + (real_mult_left_mono, + cvar(real_mult_left_mono, hd(tl(prems_of real_mult_left_mono))))] in diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Real/real_arith0.ML --- a/src/HOL/Real/real_arith0.ML Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Real/real_arith0.ML Thu Jan 01 10:06:32 2004 +0100 @@ -6,6 +6,11 @@ Instantiation of the generic linear arithmetic package for type real. *) +val add_zero_left = thm"Ring_and_Field.add_0"; +val add_zero_right = thm"Ring_and_Field.add_0_right"; + +val real_mult_left_mono = + read_instantiate_sg(sign_of RealBin.thy) [("a","?a::real")] mult_left_mono; local @@ -17,20 +22,17 @@ add_real_number_of, minus_real_number_of, diff_real_number_of, mult_real_number_of, eq_real_number_of, less_real_number_of, le_real_number_of_eq_not_less, real_diff_def, - real_minus_add_distrib, real_minus_minus, real_mult_assoc, - real_minus_zero, - real_add_zero_left, real_add_zero_right, - real_add_minus, real_add_minus_left, - real_mult_0, real_mult_0_right, - real_mult_1, real_mult_1_right, - real_mult_minus_eq1, real_mult_minus_eq2]; + minus_add_distrib, minus_minus, mult_assoc, minus_zero, + add_zero_left, add_zero_right, left_minus, right_minus, + mult_left_zero, mult_right_zero, mult_1, mult_1_right, + minus_mult_left RS sym, minus_mult_right RS sym]; val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@ Real_Numeral_Simprocs.cancel_numerals @ Real_Numeral_Simprocs.eval_numerals; val mono_ss = simpset() addsimps - [real_add_le_mono,real_add_less_mono, + [add_mono,add_strict_mono, real_add_less_le_mono,real_add_le_less_mono]; val add_mono_thms_real = @@ -51,8 +53,8 @@ val real_mult_mono_thms = [(rotate_prems 1 real_mult_less_mono2, cvar(real_mult_less_mono2, hd(prems_of real_mult_less_mono2))), - (real_mult_le_mono2, - cvar(real_mult_le_mono2, hd(tl(prems_of real_mult_le_mono2))))] + (real_mult_left_mono, + cvar(real_mult_left_mono, hd(tl(prems_of real_mult_left_mono))))] in diff -r 14f29eb097a3 -r 6137d24eef79 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Mon Dec 29 06:49:26 2003 +0100 +++ b/src/HOL/Ring_and_Field.thy Thu Jan 01 10:06:32 2004 +0100 @@ -1505,8 +1505,20 @@ ML {* +val add_assoc = thm"add_assoc"; +val add_commute = thm"add_commute"; +val mult_assoc = thm"mult_assoc"; +val mult_commute = thm"mult_commute"; +val zero_neq_one = thm"zero_neq_one"; +val diff_minus = thm"diff_minus"; +val abs_if = thm"abs_if"; +val divide_inverse = thm"divide_inverse"; +val inverse_zero = thm"inverse_zero"; +val divide_zero = thm"divide_zero"; +val add_0 = thm"add_0"; val add_0_right = thm"add_0_right"; val add_left_commute = thm"add_left_commute"; +val left_minus = thm"left_minus"; val right_minus = thm"right_minus"; val right_minus_eq = thm"right_minus_eq"; val add_left_cancel = thm"add_left_cancel"; @@ -1523,10 +1535,12 @@ val neg_0_equal_iff_equal = thm"neg_0_equal_iff_equal"; val equation_minus_iff = thm"equation_minus_iff"; val minus_equation_iff = thm"minus_equation_iff"; +val mult_1 = thm"mult_1"; val mult_1_right = thm"mult_1_right"; val mult_left_commute = thm"mult_left_commute"; val mult_left_zero = thm"mult_left_zero"; val mult_right_zero = thm"mult_right_zero"; +val left_distrib = thm "left_distrib"; val right_distrib = thm"right_distrib"; val combine_common_factor = thm"combine_common_factor"; val minus_add_distrib = thm"minus_add_distrib"; @@ -1536,6 +1550,7 @@ val right_diff_distrib = thm"right_diff_distrib"; val left_diff_distrib = thm"left_diff_distrib"; val minus_diff_eq = thm"minus_diff_eq"; +val add_left_mono = thm"add_left_mono"; val add_right_mono = thm"add_right_mono"; val add_mono = thm"add_mono"; val add_strict_left_mono = thm"add_strict_left_mono"; @@ -1579,6 +1594,7 @@ val less_add_iff2 = thm"less_add_iff2"; val le_add_iff1 = thm"le_add_iff1"; val le_add_iff2 = thm"le_add_iff2"; +val mult_strict_left_mono = thm"mult_strict_left_mono"; val mult_strict_right_mono = thm"mult_strict_right_mono"; val mult_left_mono = thm"mult_left_mono"; val mult_right_mono = thm"mult_right_mono";