# HG changeset patch
# User huffman
# Date 1179176994 -7200
# Node ID 03085c441c14e789656dadddba7298405a776c4b
# Parent  08b0fa905ea0896fcbfbf4096278abf589b44bef
spelling: rename arcos -> arccos

diff -r 08b0fa905ea0 -r 03085c441c14 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Mon May 14 22:32:51 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Mon May 14 23:09:54 2007 +0200
@@ -46,8 +46,8 @@
   "arcsin y = (SOME x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
 
 definition
-  arcos :: "real => real" where
-  "arcos y = (SOME x. 0 \<le> x & x \<le> pi & cos x = y)"
+  arccos :: "real => real" where
+  "arccos y = (SOME x. 0 \<le> x & x \<le> pi & cos x = y)"
 
 definition     
   arctan :: "real => real" where
@@ -1727,44 +1727,44 @@
 apply (rule sin_total, auto)
 done
 
-lemma arcos:
+lemma arccos:
      "[| -1 \<le> y; y \<le> 1 |]  
-      ==> 0 \<le> arcos y & arcos y \<le> pi & cos(arcos y) = y"
-apply (simp add: arcos_def)
+      ==> 0 \<le> arccos y & arccos y \<le> pi & cos(arccos y) = y"
+apply (simp add: arccos_def)
 apply (drule cos_total, assumption)
 apply (fast intro: someI2)
 done
 
-lemma cos_arcos [simp]: "[| -1 \<le> y; y \<le> 1 |] ==> cos(arcos y) = y"
-by (blast dest: arcos)
+lemma cos_arccos [simp]: "[| -1 \<le> y; y \<le> 1 |] ==> cos(arccos y) = y"
+by (blast dest: arccos)
       
-lemma arcos_bounded: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arcos y & arcos y \<le> pi"
-by (blast dest: arcos)
+lemma arccos_bounded: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y & arccos y \<le> pi"
+by (blast dest: arccos)
 
-lemma arcos_lbound: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arcos y"
-by (blast dest: arcos)
+lemma arccos_lbound: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y"
+by (blast dest: arccos)
 
-lemma arcos_ubound: "[| -1 \<le> y; y \<le> 1 |] ==> arcos y \<le> pi"
-by (blast dest: arcos)
+lemma arccos_ubound: "[| -1 \<le> y; y \<le> 1 |] ==> arccos y \<le> pi"
+by (blast dest: arccos)
 
-lemma arcos_lt_bounded:
+lemma arccos_lt_bounded:
      "[| -1 < y; y < 1 |]  
-      ==> 0 < arcos y & arcos y < pi"
+      ==> 0 < arccos y & arccos y < pi"
 apply (frule order_less_imp_le)
 apply (frule_tac y = y in order_less_imp_le)
-apply (frule arcos_bounded, auto)
-apply (drule_tac y = "arcos y" in order_le_imp_less_or_eq)
+apply (frule arccos_bounded, auto)
+apply (drule_tac y = "arccos y" in order_le_imp_less_or_eq)
 apply (drule_tac [2] y = pi in order_le_imp_less_or_eq, auto)
 apply (drule_tac [!] f = cos in arg_cong, auto)
 done
 
-lemma arcos_cos: "[|0 \<le> x; x \<le> pi |] ==> arcos(cos x) = x"
-apply (simp add: arcos_def)
+lemma arccos_cos: "[|0 \<le> x; x \<le> pi |] ==> arccos(cos x) = x"
+apply (simp add: arccos_def)
 apply (auto intro!: some1_equality cos_total)
 done
 
-lemma arcos_cos2: "[|x \<le> 0; -pi \<le> x |] ==> arcos(cos x) = -x"
-apply (simp add: arcos_def)
+lemma arccos_cos2: "[|x \<le> 0; -pi \<le> x |] ==> arccos(cos x) = -x"
+apply (simp add: arccos_def)
 apply (auto intro!: some1_equality cos_total)
 done
 
@@ -1990,11 +1990,11 @@
 apply (simp add: real_add_commute)
 done
 
-declare cos_arcos [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp] 
-declare arcos_bounded [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp] 
+declare cos_arccos [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp] 
+declare arccos_bounded [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp] 
 
-declare cos_arcos [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2, simp] 
-declare arcos_bounded [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2, simp] 
+declare cos_arccos [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2, simp] 
+declare arccos_bounded [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2, simp] 
 
 lemma cos_abs_x_y_ge_minus_one [simp]:
      "-1 \<le> \<bar>x\<bar> / sqrt (x * x + y * y)"
@@ -2007,8 +2007,8 @@
             simp del: real_sqrt_gt_0_iff real_sqrt_eq_0_iff)
 done
 
-declare cos_arcos [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp] 
-declare arcos_bounded [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp] 
+declare cos_arccos [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp] 
+declare arccos_bounded [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp] 
 
 lemma minus_pi_less_zero: "-pi < 0"
 by simp
@@ -2016,12 +2016,12 @@
 declare minus_pi_less_zero [simp]
 declare minus_pi_less_zero [THEN order_less_imp_le, simp]
 
-lemma arcos_ge_minus_pi: "[| -1 \<le> y; y \<le> 1 |] ==> -pi \<le> arcos y"
+lemma arccos_ge_minus_pi: "[| -1 \<le> y; y \<le> 1 |] ==> -pi \<le> arccos y"
 apply (rule real_le_trans)
-apply (rule_tac [2] arcos_lbound, auto)
+apply (rule_tac [2] arccos_lbound, auto)
 done
 
-declare arcos_ge_minus_pi [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp] 
+declare arccos_ge_minus_pi [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp] 
 
 (* How tedious! *)
 lemma lemma_divide_rearrange:
@@ -2095,11 +2095,11 @@
 lemma polar_ex1:
      "[| x \<noteq> 0; 0 < y |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
 apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>)" in exI)
-apply (rule_tac x = "arcos (x / sqrt (x * x + y * y))" in exI)
+apply (rule_tac x = "arccos (x / sqrt (x * x + y * y))" in exI)
 apply auto
 apply (drule_tac y2 = y in real_sqrt_sum_squares_gt_zero3 [THEN real_not_refl2, THEN not_sym])
 apply (auto simp add: power2_eq_square)
-apply (simp add: arcos_def)
+apply (simp add: arccos_def)
 apply (cut_tac x1 = x and y1 = y 
        in cos_total [OF cos_x_y_ge_minus_one cos_x_y_le_one])
 apply (rule someI2_ex, blast)