# HG changeset patch
# User huffman
# Date 1179198541 -7200
# Node ID 04fd6cc1c4a9c942bda0dae777fbe080e9c22a07
# Parent  1d73b1feaacf40af74af68e2cefa2d328cfcd542
remove simp attribute from various polar_Ex lemmas

diff -r 1d73b1feaacf -r 04fd6cc1c4a9 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Mon May 14 23:25:16 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Tue May 15 05:09:01 2007 +0200
@@ -1961,50 +1961,50 @@
 by (simp add: minus_sqrt_le not_neg_sqrt_sumsq divide_const_simps
          del: real_sqrt_gt_0_iff real_sqrt_lt_0_iff)
 
-lemma cos_x_y_ge_minus_one1a [simp]: "-1 \<le> y / sqrt (x * x + y * y)"
+lemma cos_x_y_ge_minus_one1a (*[simp]*): "-1 \<le> y / sqrt (x * x + y * y)"
 by (subst add_commute, simp add: cos_x_y_ge_minus_one)
 
-lemma cos_x_y_le_one [simp]: "x / sqrt (x * x + y * y) \<le> 1" 
+lemma cos_x_y_le_one (*[simp]*): "x / sqrt (x * x + y * y) \<le> 1" 
 by (simp add: divide_le_eq not_sum_squares_lt_zero)
 
-lemma cos_x_y_le_one2 [simp]: "y / sqrt (x * x + y * y) \<le> 1"
+lemma cos_x_y_le_one2 (*[simp]*): "y / sqrt (x * x + y * y) \<le> 1"
 apply (cut_tac x = y and y = x in cos_x_y_le_one)
 apply (simp add: real_add_commute)
 done
 
-lemmas cos_arccos_lemma1 =
-  cos_arccos [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp]
+lemmas cos_arccos_lemma1 = (* used by polar_ex1 *)
+  cos_arccos [OF cos_x_y_ge_minus_one cos_x_y_le_one]
 
 lemmas arccos_bounded_lemma1 =
-  arccos_bounded [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp] 
+  arccos_bounded [OF cos_x_y_ge_minus_one cos_x_y_le_one]
 
 lemmas cos_arccos_lemma2 =
-  cos_arccos [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2, simp] 
+  cos_arccos [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2]
 
 lemmas arccos_bounded_lemma2 =
-  arccos_bounded [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2, simp] 
+  arccos_bounded [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2]
 
-lemma cos_abs_x_y_ge_minus_one [simp]:
+lemma cos_abs_x_y_ge_minus_one (*[simp]*):
      "-1 \<le> \<bar>x\<bar> / sqrt (x * x + y * y)"
 by (auto simp add: divide_const_simps abs_if linorder_not_le [symmetric]
          simp del: real_sqrt_ge_0_iff real_sqrt_le_0_iff)
 
-lemma cos_abs_x_y_le_one [simp]: "\<bar>x\<bar> / sqrt (x * x + y * y) \<le> 1"
+lemma cos_abs_x_y_le_one (*[simp]*): "\<bar>x\<bar> / sqrt (x * x + y * y) \<le> 1"
 apply (insert minus_le_real_sqrt_sumsq [of x y] le_real_sqrt_sumsq [of x y])
 apply (auto simp add: divide_const_simps abs_if linorder_neq_iff
             simp del: real_sqrt_gt_0_iff real_sqrt_eq_0_iff)
 done
 
 lemmas cos_arccos_lemma3 =
-  cos_arccos [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp] 
+  cos_arccos [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one]
 
 lemmas arccos_bounded_lemma3 =
-  arccos_bounded [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp] 
+  arccos_bounded [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one]
 
-lemma minus_pi_less_zero [simp]: "-pi < 0"
+lemma minus_pi_less_zero (*[simp]*): "-pi < 0"
 by simp
 
-lemma minus_pi_le_zero [simp]: "-pi \<le> 0"
+lemma minus_pi_le_zero (*[simp]*): "-pi \<le> 0"
 by simp
 
 lemma arccos_ge_minus_pi: "[| -1 \<le> y; y \<le> 1 |] ==> -pi \<le> arccos y"
@@ -2090,7 +2090,7 @@
 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 (auto simp add: power2_eq_square cos_arccos_lemma1)
 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])
@@ -2110,7 +2110,8 @@
      "[| 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 (rule_tac x = "arcsin (y / sqrt (x * x + y * y))" in exI)
+apply (subst sin_arcsin [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2])
 apply (auto dest: real_sum_squares_cancel2a 
             simp add: power2_eq_square real_0_le_add_iff real_add_eq_0_iff)
 apply (unfold arcsin_def)