author huffman Tue, 15 May 2007 05:09:01 +0200 changeset 22977 04fd6cc1c4a9 parent 22976 1d73b1feaacf child 22978 1cd8cc21a7c3
remove simp attribute from various polar_Ex lemmas
```--- 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)"

-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"

-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)
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 cos_arccos_lemma1)