# HG changeset patch # User paulson # Date 1091110482 -7200 # Node ID 5693a977a767c7128e13a33cf26101754df924d6 # Parent 07f7b158ef32fc17106bcbb737fd2a585aa0de4c removed some [iff] declarations from RealDef.thy, concerning inequalities diff -r 07f7b158ef32 -r 5693a977a767 src/HOL/Complex/CSeries.thy --- a/src/HOL/Complex/CSeries.thy Thu Jul 29 16:14:06 2004 +0200 +++ b/src/HOL/Complex/CSeries.thy Thu Jul 29 16:14:42 2004 +0200 @@ -146,28 +146,12 @@ ***) lemma sumr_cmod_ge_zero [iff]: "0 \ sumr m n (%n. cmod (f n))" -apply (induct_tac "n", auto) -apply (rule_tac j = 0 in real_le_trans, auto) -done +by (induct_tac "n", auto simp add: add_increasing) lemma rabs_sumc_cmod_cancel [simp]: "abs (sumr m n (%n. cmod (f n))) = (sumr m n (%n. cmod (f n)))" by (simp add: abs_if linorder_not_less) -lemma sumc_zero: - "\n. N \ n --> f n = 0 - ==> \m n. N \ m --> sumc m n f = 0" -apply safe -apply (induct_tac "n", auto) -done - -lemma fun_zero_sumc_zero: - "\n. N \ n --> f (Suc n) = 0 - ==> \m n. Suc N \ m --> sumc m n f = 0" -apply (rule sumc_zero, safe) -apply (drule_tac x = "n - 1" in spec, auto, arith) -done - lemma sumc_one_lb_complexpow_zero [simp]: "sumc 1 n (%n. f(n) * 0 ^ n) = 0" apply (induct_tac "n") apply (case_tac [2] "n", auto) @@ -210,8 +194,6 @@ val sumc_interval_const2 = thm "sumc_interval_const2"; val sumr_cmod_ge_zero = thm "sumr_cmod_ge_zero"; val rabs_sumc_cmod_cancel = thm "rabs_sumc_cmod_cancel"; -val sumc_zero = thm "sumc_zero"; -val fun_zero_sumc_zero = thm "fun_zero_sumc_zero"; val sumc_one_lb_complexpow_zero = thm "sumc_one_lb_complexpow_zero"; val sumc_diff = thm "sumc_diff"; val sumc_subst = thm "sumc_subst"; diff -r 07f7b158ef32 -r 5693a977a767 src/HOL/Complex/Complex.thy --- a/src/HOL/Complex/Complex.thy Thu Jul 29 16:14:06 2004 +0200 +++ b/src/HOL/Complex/Complex.thy Thu Jul 29 16:14:42 2004 +0200 @@ -7,7 +7,7 @@ header {* Complex Numbers: Rectangular and Polar Representations *} -theory Complex = HLog: +theory Complex = "../Hyperreal/HLog": datatype complex = Complex real real @@ -440,7 +440,8 @@ lemma complex_mod_eq_zero_cancel [simp]: "(cmod x = 0) = (x = 0)" apply (induct x) -apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 +apply (auto iff: real_0_le_add_iff + intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: complex_mod complex_zero_def power2_eq_square) done @@ -453,7 +454,7 @@ lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2" apply (induct z, simp add: complex_mod complex_cnj complex_mult) -apply (simp add: power2_eq_square abs_if linorder_not_less) +apply (simp add: power2_eq_square abs_if linorder_not_less real_0_le_add_iff) done lemma complex_mod_squared: "cmod(Complex x y) ^ 2 = x ^ 2 + y ^ 2" @@ -510,7 +511,7 @@ lemma complex_mod_triangle_ineq [simp]: "cmod (x + y) \ cmod(x) + cmod(y)" apply (rule_tac n = 1 in realpow_increasing) apply (auto intro: order_trans [OF _ complex_mod_ge_zero] - simp add: power2_eq_square [symmetric]) + simp add: add_increasing power2_eq_square [symmetric]) done lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \ cmod a" diff -r 07f7b158ef32 -r 5693a977a767 src/HOL/Complex/NSComplex.thy --- a/src/HOL/Complex/NSComplex.thy Thu Jul 29 16:14:06 2004 +0200 +++ b/src/HOL/Complex/NSComplex.thy Thu Jul 29 16:14:42 2004 +0200 @@ -988,8 +988,9 @@ apply (simp add: hsgn hcmod hIm hypreal_divide) done +(*????move to RealDef????*) lemma real_two_squares_add_zero_iff [simp]: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)" -by (auto intro: real_sum_squares_cancel) +by (auto intro: real_sum_squares_cancel iff: real_add_eq_0_iff) lemma hcomplex_inverse_complex_split: "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) = diff -r 07f7b158ef32 -r 5693a977a767 src/HOL/Hyperreal/HyperDef.thy --- a/src/HOL/Hyperreal/HyperDef.thy Thu Jul 29 16:14:06 2004 +0200 +++ b/src/HOL/Hyperreal/HyperDef.thy Thu Jul 29 16:14:42 2004 +0200 @@ -7,7 +7,7 @@ header{*Construction of Hyperreals Using Ultrafilters*} -theory HyperDef = Filter + Real +theory HyperDef = Filter + "../Real/Real" files ("fuf.ML"): (*Warning: file fuf.ML refers to the name Hyperdef!*) diff -r 07f7b158ef32 -r 5693a977a767 src/HOL/Hyperreal/HyperPow.thy --- a/src/HOL/Hyperreal/HyperPow.thy Thu Jul 29 16:14:06 2004 +0200 +++ b/src/HOL/Hyperreal/HyperPow.thy Thu Jul 29 16:14:42 2004 +0200 @@ -6,7 +6,7 @@ header{*Exponentials on the Hyperreals*} -theory HyperPow = HyperArith + HyperNat + RealPow: +theory HyperPow = HyperArith + HyperNat + "../Real/RealPow": instance hypreal :: power .. diff -r 07f7b158ef32 -r 5693a977a767 src/HOL/Hyperreal/Log.thy --- a/src/HOL/Hyperreal/Log.thy Thu Jul 29 16:14:06 2004 +0200 +++ b/src/HOL/Hyperreal/Log.thy Thu Jul 29 16:14:42 2004 +0200 @@ -127,6 +127,61 @@ by (simp add: linorder_not_less [symmetric]) +subsection{*Further Results Courtesy Jeremy Avigad*} + +lemma powr_realpow: "0 < x ==> x powr (real n) = x^n" + apply (induct n, simp) + apply (subgoal_tac "real(Suc n) = real n + 1") + apply (erule ssubst) + apply (subst powr_add, simp, simp) +done + +lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 + else x powr (real n))" + apply (case_tac "x = 0", simp, simp) + apply (rule powr_realpow [THEN sym], simp) +done + +lemma ln_pwr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x" +by (unfold powr_def, simp) + +lemma ln_bound: "1 <= x ==> ln x <= x" + apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1") + apply simp + apply (rule ln_add_one_self_le_self, simp) +done + +lemma powr_mono: "a <= b ==> 1 <= x ==> x powr a <= x powr b" + apply (case_tac "x = 1", simp) + apply (case_tac "a = b", simp) + apply (rule order_less_imp_le) + apply (rule powr_less_mono, auto) +done + +lemma ge_one_powr_ge_zero: "1 <= x ==> 0 <= a ==> 1 <= x powr a" + apply (subst powr_zero_eq_one [THEN sym]) + apply (rule powr_mono, assumption+) +done + +lemma powr_less_mono2: "0 < a ==> 0 < x ==> x < y ==> x powr a < + y powr a" + apply (unfold powr_def) + apply (rule exp_less_mono) + apply (rule mult_strict_left_mono) + apply (subst ln_less_cancel_iff, assumption) + apply (rule order_less_trans) + prefer 2 + apply assumption+ +done + +lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"; + apply (case_tac "a = 0", simp) + apply (case_tac "x = y", simp) + apply (rule order_less_imp_le) + apply (rule powr_less_mono2, auto) +done + + ML {* diff -r 07f7b158ef32 -r 5693a977a767 src/HOL/Hyperreal/NatStar.thy --- a/src/HOL/Hyperreal/NatStar.thy Thu Jul 29 16:14:06 2004 +0200 +++ b/src/HOL/Hyperreal/NatStar.thy Thu Jul 29 16:14:42 2004 +0200 @@ -7,7 +7,7 @@ header{*Star-transforms for the Hypernaturals*} -theory NatStar = RealPow + HyperPow: +theory NatStar = "../Real/RealPow" + HyperPow: text{*Extends sets of nats, and functions from the nats to nats or reals*} diff -r 07f7b158ef32 -r 5693a977a767 src/HOL/Hyperreal/NthRoot.thy --- a/src/HOL/Hyperreal/NthRoot.thy Thu Jul 29 16:14:06 2004 +0200 +++ b/src/HOL/Hyperreal/NthRoot.thy Thu Jul 29 16:14:42 2004 +0200 @@ -76,7 +76,8 @@ 0 < a; 0 < n |] ==> ALL k. a <= (u + inverse(real (Suc k))) ^ n" apply safe apply (frule lemma_nth_realpow_seq, safe) -apply (auto elim: order_less_asym simp add: linorder_not_less [symmetric]) +apply (auto elim: order_less_asym simp add: linorder_not_less [symmetric] + iff: real_0_less_add_iff) --{*legacy iff rule!*} apply (simp add: linorder_not_less) apply (rule order_less_trans [of _ 0]) apply (auto intro: lemma_nth_realpow_isLub_gt_zero) @@ -118,8 +119,7 @@ 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) -done +by (simp add: zero_le_mult_iff real_of_nat_inverse_le_iff real_0_le_add_iff) lemma lemma_nth_realpow_isLub_le: "[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u; diff -r 07f7b158ef32 -r 5693a977a767 src/HOL/Hyperreal/SEQ.thy --- a/src/HOL/Hyperreal/SEQ.thy Thu Jul 29 16:14:06 2004 +0200 +++ b/src/HOL/Hyperreal/SEQ.thy Thu Jul 29 16:14:42 2004 +0200 @@ -796,7 +796,7 @@ apply (rule_tac x = "1 + \X M\ " in exI) apply (rule_tac [2] x = "1 + \X M\ " in exI) apply (rule_tac [3] x = "\X m\ " in exI) -apply (auto elim!: lemma_Nat_covered, arith+) +apply (auto elim!: lemma_Nat_covered) done text{*A Cauchy sequence is bounded -- nonstandard version*} diff -r 07f7b158ef32 -r 5693a977a767 src/HOL/Hyperreal/Series.thy --- a/src/HOL/Hyperreal/Series.thy Thu Jul 29 16:14:06 2004 +0200 +++ b/src/HOL/Hyperreal/Series.thy Thu Jul 29 16:14:42 2004 +0200 @@ -270,7 +270,8 @@ apply (drule summable_sums) apply (auto simp add: sums_def LIMSEQ_def) apply (drule_tac x = "f (n) + f (n + 1) " in spec) -apply auto +apply (auto iff: real_0_less_add_iff) + --{*legacy proof: not necessarily better!*} apply (rule_tac [2] ccontr, drule_tac [2] linorder_not_less [THEN iffD1]) apply (frule_tac [2] no=no in sumr_pos_lt_pair_lemma) apply (drule_tac x = 0 in spec, simp) @@ -291,11 +292,9 @@ apply (auto simp add: linorder_not_less [symmetric]) done - +text{*A summable series of positive terms has limit that is at least as +great as any partial sum.*} -(*----------------------------------------------------------------- - Summable series of positive terms has limit >= any partial sum - ----------------------------------------------------------------*) lemma series_pos_le: "[| summable f; \m. n \ m --> 0 \ f(m) |] ==> sumr 0 n f \ suminf f" apply (drule summable_sums) @@ -314,9 +313,7 @@ apply (drule_tac x = m in spec, auto) done -(*------------------------------------------------------------------- - sum of geometric progression - -------------------------------------------------------------------*) +text{*Sum of a geometric progression.*} lemma sumr_geometric: "x ~= 1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - 1) / (x - 1)" apply (induct_tac "n", auto) @@ -334,9 +331,8 @@ apply (auto intro: LIMSEQ_const simp add: real_diff_def minus_divide_right LIMSEQ_rabs_realpow_zero2) done -(*------------------------------------------------------------------- - Cauchy-type criterion for convergence of series (c.f. Harrison) - -------------------------------------------------------------------*) +text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*} + lemma summable_convergent_sumr_iff: "summable f = convergent (%n. sumr 0 n f)" by (simp add: summable_def sums_def convergent_def) @@ -355,14 +351,8 @@ simp add: sumr_split_add_minus abs_minus_add_cancel) done -(*------------------------------------------------------------------- - Terms of a convergent series tend to zero - > Goalw [LIMSEQ_def] "summable f ==> f ----> 0" - Proved easily in HSeries after proving nonstandard case. - -------------------------------------------------------------------*) -(*------------------------------------------------------------------- - Comparison test - -------------------------------------------------------------------*) +text{*Comparison test*} + lemma summable_comparison_test: "[| \N. \n. N \ n --> abs(f n) \ g n; summable g |] ==> summable f" apply (auto simp add: summable_Cauchy) @@ -384,9 +374,8 @@ apply (auto simp add: abs_idempotent) done -(*------------------------------------------------------------------*) -(* Limit comparison property for series (c.f. jrh) *) -(*------------------------------------------------------------------*) +text{*Limit comparison property for series (c.f. jrh)*} + lemma summable_le: "[|\n. f n \ g n; summable f; summable g |] ==> suminf f \ suminf g" apply (drule summable_sums)+ @@ -402,9 +391,7 @@ apply (simp add: abs_le_interval_iff) done -(*------------------------------------------------------------------- - Absolute convergence imples normal convergence - -------------------------------------------------------------------*) +text{*Absolute convergence imples normal convergence*} lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f" apply (auto simp add: sumr_rabs summable_Cauchy) apply (drule spec, auto) @@ -414,9 +401,7 @@ apply (auto intro: sumr_rabs) done -(*------------------------------------------------------------------- - Absolute convergence of series - -------------------------------------------------------------------*) +text{*Absolute convergence of series*} lemma summable_rabs: "summable (%n. abs (f n)) ==> abs(suminf f) \ suminf (%n. abs(f n))" by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf sumr_rabs) @@ -469,9 +454,7 @@ done -(*--------------------------------------------------------------------------*) -(* Differentiation of finite sum *) -(*--------------------------------------------------------------------------*) +text{*Differentiation of finite sum*} lemma DERIV_sumr [rule_format (no_asm)]: "(\r. m \ r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) diff -r 07f7b158ef32 -r 5693a977a767 src/HOL/Hyperreal/Transcendental.thy --- a/src/HOL/Hyperreal/Transcendental.thy Thu Jul 29 16:14:06 2004 +0200 +++ b/src/HOL/Hyperreal/Transcendental.thy Thu Jul 29 16:14:42 2004 +0200 @@ -9,8 +9,6 @@ theory Transcendental = NthRoot + Fact + HSeries + EvenOdd + Lim: -(*????FOR RING_AND_FIELD*) - constdefs root :: "[nat,real] => real" "root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))" @@ -664,7 +662,7 @@ apply (auto simp add: add_commute) apply (drule_tac x="(\n. c n * (xa + x) ^ n)" in sums_diff, assumption) apply (drule_tac x = " (%n. c n * (xa + x) ^ n - c n * x ^ n) " and c = "inverse xa" in sums_mult) -apply (rule sums_unique [symmetric]) +apply (rule sums_unique) apply (simp add: diff_def divide_inverse add_ac mult_ac) apply (rule LIM_zero_cancel) apply (rule_tac g = "%h. suminf (%n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) - (real n * (x ^ (n - Suc 0))))) " in LIM_trans) @@ -690,7 +688,6 @@ apply (simp add: sums_summable [THEN suminf_mult2]) apply (frule_tac x = " (%n. inverse xa * (c n * ((xa + x) ^ n - x ^ n))) " and y = " (%n. real n * c n * x ^ (n - Suc 0))" in sums_diff) apply assumption -apply (subst minus_equation_iff, simp (no_asm)) apply (simp add: suminf_diff [OF sums_summable sums_summable] add_ac mult_ac) apply (rule_tac f = suminf in arg_cong) apply (rule ext) @@ -1268,35 +1265,39 @@ lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y" apply (cut_tac x = x and y = y in sin_cos_add) apply (auto dest!: real_sum_squares_cancel_a - simp add: numeral_2_eq_2 simp del: sin_cos_add) + simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_add) done lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y" apply (cut_tac x = x and y = y in sin_cos_add) apply (auto dest!: real_sum_squares_cancel_a - simp add: numeral_2_eq_2 simp del: sin_cos_add) + simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_add) done -lemma lemma_DERIV_sin_cos_minus: "\x. - DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0" +lemma lemma_DERIV_sin_cos_minus: + "\x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0" apply (safe, rule lemma_DERIV_subst) apply (best intro!: DERIV_intros intro: DERIV_chain2) apply (auto simp add: real_diff_def left_distrib right_distrib mult_ac add_ac) done -lemma sin_cos_minus [simp]: "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0" -apply (cut_tac y = 0 and x = x in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all]) +lemma sin_cos_minus [simp]: + "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0" +apply (cut_tac y = 0 and x = x + in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all]) apply (auto simp add: numeral_2_eq_2) done lemma sin_minus [simp]: "sin (-x) = -sin(x)" apply (cut_tac x = x in sin_cos_minus) -apply (auto dest!: real_sum_squares_cancel_a simp add: numeral_2_eq_2 simp del: sin_cos_minus) +apply (auto dest!: real_sum_squares_cancel_a + simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_minus) done lemma cos_minus [simp]: "cos (-x) = cos(x)" apply (cut_tac x = x in sin_cos_minus) -apply (auto dest!: real_sum_squares_cancel_a simp add: numeral_2_eq_2 simp del: sin_cos_minus) +apply (auto dest!: real_sum_squares_cancel_a + simp add: numeral_2_eq_2 simp del: sin_cos_minus) done lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y" @@ -1368,7 +1369,7 @@ apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric]) apply (subgoal_tac "x*x < 2*3", simp) apply (rule mult_strict_mono) -apply (auto simp add: real_of_nat_Suc simp del: fact_Suc) +apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc) apply (subst fact_Suc) apply (subst fact_Suc) apply (subst fact_Suc) @@ -1430,7 +1431,8 @@ apply (simp (no_asm) add: mult_assoc del: sumr_Suc) apply (rule sumr_pos_lt_pair) apply (erule sums_summable, safe) -apply (simp (no_asm) add: divide_inverse mult_assoc [symmetric] del: fact_Suc) +apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] + del: fact_Suc) apply (rule real_mult_inverse_cancel2) apply (rule real_of_nat_fact_gt_zero)+ apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc) @@ -1692,9 +1694,8 @@ apply (subgoal_tac "\n::nat. ~ even n & x + pi/2 = real n * (pi/2) ") apply (clarify, rule_tac x = "n - 1" in exI) apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib) -apply (rule cos_zero_lemma, clarify) -apply (rule minus_le_iff [THEN iffD1]) -apply (rule_tac y=0 in order_trans, auto) +apply (rule cos_zero_lemma) +apply (simp_all add: add_increasing) done @@ -1992,12 +1993,14 @@ simp del: realpow_Suc) done -lemma lemma_sin_cos_eq [simp]: "sin (xa + 1 / 2 * real (Suc m) * pi) = +text{*NEEDED??*} +lemma [simp]: "sin (xa + 1 / 2 * real (Suc m) * pi) = cos (xa + 1 / 2 * real (m) * pi)" apply (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib, auto) done -lemma lemma_sin_cos_eq2 [simp]: "sin (xa + real (Suc m) * pi / 2) = +text{*NEEDED??*} +lemma [simp]: "sin (xa + real (Suc m) * pi / 2) = cos (xa + real (m) * pi / 2)" apply (simp only: cos_add sin_add divide_inverse real_of_nat_Suc left_distrib right_distrib, auto) done @@ -2333,8 +2336,8 @@ 1 - (cos xa)\ = (y / sqrt (x * x + y * y)) ^ 2 |] ==> (cos xa)\ = (x / sqrt (x * x + y * y)) ^ 2" apply (auto simp add: realpow_divide power2_eq_square [symmetric]) -apply (rule add_commute [THEN subst]) -apply (rule lemma_divide_rearrange, simp) +apply (subst add_commute) +apply (rule lemma_divide_rearrange, simp add: real_add_eq_0_iff) apply (simp add: add_commute) done @@ -2395,22 +2398,24 @@ done lemma real_sum_squares_cancel2a: "x * x = -(y * y) ==> y = (0::real)" -by (auto intro: real_sum_squares_cancel) +by (auto intro: real_sum_squares_cancel iff: real_add_eq_0_iff) lemma polar_ex2: "[| x \ 0; y < 0 |] ==> \r a. x = r * cos a & y = r * sin a" apply (cut_tac x = 0 and y = x in linorder_less_linear, auto) apply (rule_tac x = "sqrt (x\ + y\) " in exI) apply (rule_tac x = "arcsin (y / sqrt (x * x + y * y))" in exI) -apply (auto dest: real_sum_squares_cancel2a simp add: power2_eq_square) +apply (auto dest: real_sum_squares_cancel2a + simp add: power2_eq_square real_0_le_add_iff real_add_eq_0_iff) apply (unfold arcsin_def) apply (cut_tac x1 = x and y1 = y in sin_total [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2]) apply (rule someI2_ex, blast) apply (erule_tac V = "EX! xa. - (pi/2) \ xa & xa \ pi/2 & sin xa = y / sqrt (x * x + y * y) " in thin_rl) -apply (cut_tac x=x and y=y in cos_x_y_disj, simp, blast, auto) +apply (cut_tac x=x and y=y in cos_x_y_disj, simp, blast) +apply (auto simp add: real_0_le_add_iff real_add_eq_0_iff) apply (drule cos_ge_zero, force) apply (drule_tac x = y in real_sqrt_divide_less_zero) -apply (auto simp add: real_add_commute) +apply (auto simp add: add_commute) apply (insert polar_ex1 [of x "-y"], simp, clarify) apply (rule_tac x = r in exI) apply (rule_tac x = "-a" in exI, simp) @@ -2539,8 +2544,7 @@ apply (drule_tac d = e in isCont_inj_range) prefer 2 apply (assumption, assumption, safe) apply (rule_tac x = ea in exI, auto) -apply (rotate_tac 4) -apply (drule_tac x = "f (x) + xa" in spec) +apply (drule_tac x = "f (x) + xa" and P = "%y. \y - f x\ \ ea \ (\z. \z - x\ \ e \ f z = y)" in spec) apply auto apply (drule sym, auto, arith) done @@ -2867,7 +2871,6 @@ val cos_x_y_disj = thm "cos_x_y_disj"; val real_sqrt_divide_less_zero = thm "real_sqrt_divide_less_zero"; val polar_ex1 = thm "polar_ex1"; -val real_sum_squares_cancel2a = thm "real_sum_squares_cancel2a"; val polar_ex2 = thm "polar_ex2"; val polar_Ex = thm "polar_Ex"; val real_sqrt_ge_abs1 = thm "real_sqrt_ge_abs1"; diff -r 07f7b158ef32 -r 5693a977a767 src/HOL/Real/RealDef.thy --- a/src/HOL/Real/RealDef.thy Thu Jul 29 16:14:06 2004 +0200 +++ b/src/HOL/Real/RealDef.thy Thu Jul 29 16:14:42 2004 +0200 @@ -765,19 +765,19 @@ lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)" by arith -lemma real_add_eq_0_iff [iff]: "(x+y = (0::real)) = (y = -x)" +lemma real_add_eq_0_iff: "(x+y = (0::real)) = (y = -x)" by auto -lemma real_add_less_0_iff [iff]: "(x+y < (0::real)) = (y < -x)" +lemma real_add_less_0_iff: "(x+y < (0::real)) = (y < -x)" by auto -lemma real_0_less_add_iff [iff]: "((0::real) < x+y) = (-x < y)" +lemma real_0_less_add_iff: "((0::real) < x+y) = (-x < y)" by auto -lemma real_add_le_0_iff [iff]: "(x+y \ (0::real)) = (y \ -x)" +lemma real_add_le_0_iff: "(x+y \ (0::real)) = (y \ -x)" by auto -lemma real_0_le_add_iff [iff]: "((0::real) \ x+y) = (-x \ y)" +lemma real_0_le_add_iff: "((0::real) \ x+y) = (-x \ y)" by auto @@ -860,12 +860,6 @@ ML {* val real_0_le_divide_iff = thm"real_0_le_divide_iff"; -val real_add_minus_iff = thm"real_add_minus_iff"; -val real_add_eq_0_iff = thm"real_add_eq_0_iff"; -val real_add_less_0_iff = thm"real_add_less_0_iff"; -val real_0_less_add_iff = thm"real_0_less_add_iff"; -val real_add_le_0_iff = thm"real_add_le_0_iff"; -val real_0_le_add_iff = thm"real_0_le_add_iff"; val real_0_less_diff_iff = thm"real_0_less_diff_iff"; val real_0_le_diff_iff = thm"real_0_le_diff_iff"; val real_lbound_gt_zero = thm"real_lbound_gt_zero"; diff -r 07f7b158ef32 -r 5693a977a767 src/HOL/Real/RealPow.thy --- a/src/HOL/Real/RealPow.thy Thu Jul 29 16:14:06 2004 +0200 +++ b/src/HOL/Real/RealPow.thy Thu Jul 29 16:14:42 2004 +0200 @@ -140,7 +140,9 @@ text{*Used several times in Hyperreal/Transcendental.ML*} lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0" - by (auto intro: real_sum_squares_cancel) + apply (auto dest: real_sum_squares_cancel simp add: real_add_eq_0_iff [symmetric]) + apply (auto dest: real_sum_squares_cancel simp add: add_commute) + done lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)" by (auto simp add: left_distrib right_distrib real_diff_def)