src/HOL/Hyperreal/Transcendental.thy
 changeset 15085 5693a977a767 parent 15081 32402f5624d1 child 15086 e6a2a98d5ef5
```--- 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 (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 (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 (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
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
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)
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])
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
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 (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)
+            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)
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)"
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)"
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 lemma_divide_rearrange, simp)
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
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 (drule cos_ge_zero, force)
apply (drule_tac x = y in real_sqrt_divide_less_zero)
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";```