--- 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 \<le> 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:
- "\<forall>n. N \<le> n --> f n = 0
- ==> \<forall>m n. N \<le> m --> sumc m n f = 0"
-apply safe
-apply (induct_tac "n", auto)
-done
-
-lemma fun_zero_sumc_zero:
- "\<forall>n. N \<le> n --> f (Suc n) = 0
- ==> \<forall>m n. Suc N \<le> 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";
--- 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) \<le> 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 \<le> cmod a"
--- 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) =
--- 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!*)
--- 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 ..
--- 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
{*
--- 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*}
--- 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;
--- 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 + \<bar>X M\<bar> " in exI)
apply (rule_tac [2] x = "1 + \<bar>X M\<bar> " in exI)
apply (rule_tac [3] x = "\<bar>X m\<bar> " in exI)
-apply (auto elim!: lemma_Nat_covered, arith+)
+apply (auto elim!: lemma_Nat_covered)
done
text{*A Cauchy sequence is bounded -- nonstandard version*}
--- 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; \<forall>m. n \<le> m --> 0 \<le> f(m) |] ==> sumr 0 n f \<le> 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:
"[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> 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:
"[|\<forall>n. f n \<le> g n; summable f; summable g |] ==> suminf f \<le> 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) \<le> 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)]:
"(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))
--- 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="(\<lambda>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: "\<forall>x.
- DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
+lemma lemma_DERIV_sin_cos_minus:
+ "\<forall>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 "\<exists>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)\<twosuperior> = (y / sqrt (x * x + y * y)) ^ 2 |]
==> (cos xa)\<twosuperior> = (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 \<noteq> 0; y < 0 |] ==> \<exists>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\<twosuperior> + y\<twosuperior>) " 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) \<le> xa & xa \<le> 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. \<bar>y - f x\<bar> \<le> ea \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> 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";
--- 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 \<le> (0::real)) = (y \<le> -x)"
+lemma real_add_le_0_iff: "(x+y \<le> (0::real)) = (y \<le> -x)"
by auto
-lemma real_0_le_add_iff [iff]: "((0::real) \<le> x+y) = (-x \<le> y)"
+lemma real_0_le_add_iff: "((0::real) \<le> x+y) = (-x \<le> 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";
--- 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)