spelling: rename arcos -> arccos
authorhuffman
Mon May 14 23:09:54 2007 +0200 (2007-05-14)
changeset 2297503085c441c14
parent 22974 08b0fa905ea0
child 22976 1d73b1feaacf
spelling: rename arcos -> arccos
src/HOL/Hyperreal/Transcendental.thy
     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.22 -apply (simp add: arcos_def)
    1.23 +      ==> 0 \<le> arccos y & arccos y \<le> pi & cos(arccos y) = y"
    1.24 +apply (simp add: arccos_def)
    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.65 -apply (simp add: arcos_def)
    1.66 +lemma arccos_cos: "[|0 \<le> x; x \<le> pi |] ==> arccos(cos x) = x"
    1.67 +apply (simp add: arccos_def)
    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.72 -apply (simp add: arcos_def)
    1.73 +lemma arccos_cos2: "[|x \<le> 0; -pi \<le> x |] ==> arccos(cos x) = -x"
    1.74 +apply (simp add: arccos_def)
    1.75  apply (auto intro!: some1_equality cos_total)
    1.76  done
    1.77  
    1.78 @@ -1990,11 +1990,11 @@
    1.79  apply (simp add: real_add_commute)
    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)
   1.130 -apply (simp add: arcos_def)
   1.131 +apply (simp add: arccos_def)
   1.132  apply (cut_tac x1 = x and y1 = y 
   1.133         in cos_total [OF cos_x_y_ge_minus_one cos_x_y_le_one])
   1.134  apply (rule someI2_ex, blast)