# HG changeset patch # User huffman # Date 1179543063 -7200 # Node ID 3eae3140b4b267988cecd5870bb05c32f1e1c45b # Parent e6b5459f902897f7b2c915d4365ad4f01175f82a use THE instead of SOME diff -r e6b5459f9028 -r 3eae3140b4b2 src/HOL/Hyperreal/Transcendental.thy --- a/src/HOL/Hyperreal/Transcendental.thy Fri May 18 18:20:39 2007 +0200 +++ b/src/HOL/Hyperreal/Transcendental.thy Sat May 19 04:51:03 2007 +0200 @@ -31,7 +31,7 @@ definition ln :: "real => real" where - "ln x = (SOME u. exp u = x)" + "ln x = (THE u. exp u = x)" definition pi :: "real" where @@ -43,15 +43,15 @@ definition arcsin :: "real => real" where - "arcsin y = (SOME x. -(pi/2) \ x & x \ pi/2 & sin x = y)" + "arcsin y = (THE x. -(pi/2) \ x & x \ pi/2 & sin x = y)" definition arccos :: "real => real" where - "arccos y = (SOME x. 0 \ x & x \ pi & cos x = y)" + "arccos y = (THE x. 0 \ x & x \ pi & cos x = y)" definition arctan :: "real => real" where - "arctan y = (SOME x. -(pi/2) < x & x < pi/2 & tan x = y)" + "arctan y = (THE x. -(pi/2) < x & x < pi/2 & tan x = y)" subsection{*Exponential Function*} @@ -1678,23 +1678,17 @@ simp add: cos_gt_zero_pi [THEN less_imp_neq, THEN not_sym]) done -lemma arcsin_pi: - "[| -1 \ y; y \ 1 |] - ==> -(pi/2) \ arcsin y & arcsin y \ pi & sin(arcsin y) = y" -apply (drule sin_total, assumption) -apply (erule ex1E) -apply (simp add: arcsin_def) -apply (rule someI2, blast) -apply (force intro: order_trans) -done - lemma arcsin: "[| -1 \ y; y \ 1 |] ==> -(pi/2) \ arcsin y & arcsin y \ pi/2 & sin(arcsin y) = y" -apply (unfold arcsin_def) -apply (drule sin_total, assumption) -apply (fast intro: someI2) +unfolding arcsin_def by (rule theI' [OF sin_total]) + +lemma arcsin_pi: + "[| -1 \ y; y \ 1 |] + ==> -(pi/2) \ arcsin y & arcsin y \ pi & sin(arcsin y) = y" +apply (drule (1) arcsin) +apply (force intro: order_trans) done lemma sin_arcsin [simp]: "[| -1 \ y; y \ 1 |] ==> sin(arcsin y) = y" @@ -1723,17 +1717,14 @@ lemma arcsin_sin: "[|-(pi/2) \ x; x \ pi/2 |] ==> arcsin(sin x) = x" apply (unfold arcsin_def) -apply (rule some1_equality) +apply (rule the1_equality) apply (rule sin_total, auto) done lemma arccos: "[| -1 \ y; y \ 1 |] ==> 0 \ arccos y & arccos y \ pi & cos(arccos y) = y" -apply (simp add: arccos_def) -apply (drule cos_total, assumption) -apply (fast intro: someI2) -done +unfolding arccos_def by (rule theI' [OF cos_total]) lemma cos_arccos [simp]: "[| -1 \ y; y \ 1 |] ==> cos(arccos y) = y" by (blast dest: arccos) @@ -1760,20 +1751,17 @@ lemma arccos_cos: "[|0 \ x; x \ pi |] ==> arccos(cos x) = x" apply (simp add: arccos_def) -apply (auto intro!: some1_equality cos_total) +apply (auto intro!: the1_equality cos_total) done lemma arccos_cos2: "[|x \ 0; -pi \ x |] ==> arccos(cos x) = -x" apply (simp add: arccos_def) -apply (auto intro!: some1_equality cos_total) +apply (auto intro!: the1_equality cos_total) done lemma arctan [simp]: "- (pi/2) < arctan y & arctan y < pi/2 & tan (arctan y) = y" -apply (cut_tac y = y in tan_total) -apply (simp add: arctan_def) -apply (fast intro: someI2) -done +unfolding arctan_def by (rule theI' [OF tan_total]) lemma tan_arctan: "tan(arctan y) = y" by auto @@ -1790,7 +1778,7 @@ lemma arctan_tan: "[|-(pi/2) < x; x < pi/2 |] ==> arctan(tan x) = x" apply (unfold arctan_def) -apply (rule some1_equality) +apply (rule the1_equality) apply (rule tan_total, auto) done @@ -1966,8 +1954,7 @@ apply (simp add: cos_arccos_lemma1) apply (simp add: arccos_def) apply (cut_tac x1 = x and y1 = y in cos_total_lemma1) -apply (rule someI2_ex, blast) -apply (erule_tac V = "Ex1 ?P" in thin_rl) +apply (drule theI') apply (frule sin_x_y_disj, blast) apply (auto) apply (drule sin_ge_zero, assumption)