author huffman Mon May 14 23:09:54 2007 +0200 (2007-05-14) changeset 22975 03085c441c14 parent 22974 08b0fa905ea0 child 22976 1d73b1feaacf
spelling: rename arcos -> arccos
```     1.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Mon May 14 22:32:51 2007 +0200
1.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Mon May 14 23:09:54 2007 +0200
1.3 @@ -46,8 +46,8 @@
1.4    "arcsin y = (SOME x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
1.5
1.6  definition
1.7 -  arcos :: "real => real" where
1.8 -  "arcos y = (SOME x. 0 \<le> x & x \<le> pi & cos x = y)"
1.9 +  arccos :: "real => real" where
1.10 +  "arccos y = (SOME x. 0 \<le> x & x \<le> pi & cos x = y)"
1.11
1.12  definition
1.13    arctan :: "real => real" where
1.14 @@ -1727,44 +1727,44 @@
1.15  apply (rule sin_total, auto)
1.16  done
1.17
1.18 -lemma arcos:
1.19 +lemma arccos:
1.20       "[| -1 \<le> y; y \<le> 1 |]
1.21 -      ==> 0 \<le> arcos y & arcos y \<le> pi & cos(arcos y) = y"
1.23 +      ==> 0 \<le> arccos y & arccos y \<le> pi & cos(arccos y) = y"
1.25  apply (drule cos_total, assumption)
1.26  apply (fast intro: someI2)
1.27  done
1.28
1.29 -lemma cos_arcos [simp]: "[| -1 \<le> y; y \<le> 1 |] ==> cos(arcos y) = y"
1.30 -by (blast dest: arcos)
1.31 +lemma cos_arccos [simp]: "[| -1 \<le> y; y \<le> 1 |] ==> cos(arccos y) = y"
1.32 +by (blast dest: arccos)
1.33
1.34 -lemma arcos_bounded: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arcos y & arcos y \<le> pi"
1.35 -by (blast dest: arcos)
1.36 +lemma arccos_bounded: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y & arccos y \<le> pi"
1.37 +by (blast dest: arccos)
1.38
1.39 -lemma arcos_lbound: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arcos y"
1.40 -by (blast dest: arcos)
1.41 +lemma arccos_lbound: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y"
1.42 +by (blast dest: arccos)
1.43
1.44 -lemma arcos_ubound: "[| -1 \<le> y; y \<le> 1 |] ==> arcos y \<le> pi"
1.45 -by (blast dest: arcos)
1.46 +lemma arccos_ubound: "[| -1 \<le> y; y \<le> 1 |] ==> arccos y \<le> pi"
1.47 +by (blast dest: arccos)
1.48
1.49 -lemma arcos_lt_bounded:
1.50 +lemma arccos_lt_bounded:
1.51       "[| -1 < y; y < 1 |]
1.52 -      ==> 0 < arcos y & arcos y < pi"
1.53 +      ==> 0 < arccos y & arccos y < pi"
1.54  apply (frule order_less_imp_le)
1.55  apply (frule_tac y = y in order_less_imp_le)
1.56 -apply (frule arcos_bounded, auto)
1.57 -apply (drule_tac y = "arcos y" in order_le_imp_less_or_eq)
1.58 +apply (frule arccos_bounded, auto)
1.59 +apply (drule_tac y = "arccos y" in order_le_imp_less_or_eq)
1.60  apply (drule_tac [2] y = pi in order_le_imp_less_or_eq, auto)
1.61  apply (drule_tac [!] f = cos in arg_cong, auto)
1.62  done
1.63
1.64 -lemma arcos_cos: "[|0 \<le> x; x \<le> pi |] ==> arcos(cos x) = x"
1.66 +lemma arccos_cos: "[|0 \<le> x; x \<le> pi |] ==> arccos(cos x) = x"
1.68  apply (auto intro!: some1_equality cos_total)
1.69  done
1.70
1.71 -lemma arcos_cos2: "[|x \<le> 0; -pi \<le> x |] ==> arcos(cos x) = -x"
1.73 +lemma arccos_cos2: "[|x \<le> 0; -pi \<le> x |] ==> arccos(cos x) = -x"
1.75  apply (auto intro!: some1_equality cos_total)
1.76  done
1.77
1.78 @@ -1990,11 +1990,11 @@
1.80  done
1.81
1.82 -declare cos_arcos [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp]
1.83 -declare arcos_bounded [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp]
1.84 +declare cos_arccos [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp]
1.85 +declare arccos_bounded [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp]
1.86
1.87 -declare cos_arcos [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2, simp]
1.88 -declare arcos_bounded [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2, simp]
1.89 +declare cos_arccos [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2, simp]
1.90 +declare arccos_bounded [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2, simp]
1.91
1.92  lemma cos_abs_x_y_ge_minus_one [simp]:
1.93       "-1 \<le> \<bar>x\<bar> / sqrt (x * x + y * y)"
1.94 @@ -2007,8 +2007,8 @@
1.95              simp del: real_sqrt_gt_0_iff real_sqrt_eq_0_iff)
1.96  done
1.97
1.98 -declare cos_arcos [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp]
1.99 -declare arcos_bounded [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp]
1.100 +declare cos_arccos [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp]
1.101 +declare arccos_bounded [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp]
1.102
1.103  lemma minus_pi_less_zero: "-pi < 0"
1.104  by simp
1.105 @@ -2016,12 +2016,12 @@
1.106  declare minus_pi_less_zero [simp]
1.107  declare minus_pi_less_zero [THEN order_less_imp_le, simp]
1.108
1.109 -lemma arcos_ge_minus_pi: "[| -1 \<le> y; y \<le> 1 |] ==> -pi \<le> arcos y"
1.110 +lemma arccos_ge_minus_pi: "[| -1 \<le> y; y \<le> 1 |] ==> -pi \<le> arccos y"
1.111  apply (rule real_le_trans)
1.112 -apply (rule_tac [2] arcos_lbound, auto)
1.113 +apply (rule_tac [2] arccos_lbound, auto)
1.114  done
1.115
1.116 -declare arcos_ge_minus_pi [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp]
1.117 +declare arccos_ge_minus_pi [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp]
1.118
1.119  (* How tedious! *)
1.120  lemma lemma_divide_rearrange:
1.121 @@ -2095,11 +2095,11 @@
1.122  lemma polar_ex1:
1.123       "[| x \<noteq> 0; 0 < y |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
1.124  apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>)" in exI)
1.125 -apply (rule_tac x = "arcos (x / sqrt (x * x + y * y))" in exI)
1.126 +apply (rule_tac x = "arccos (x / sqrt (x * x + y * y))" in exI)
1.127  apply auto
1.128  apply (drule_tac y2 = y in real_sqrt_sum_squares_gt_zero3 [THEN real_not_refl2, THEN not_sym])
1.129  apply (auto simp add: power2_eq_square)