author huffman Mon, 14 May 2007 09:16:47 +0200 changeset 22960 114cf1906681 parent 22959 07a7c2900877 child 22961 e499ded5d0fc
remove redundant lemmas
```--- a/src/HOL/Hyperreal/Transcendental.thy	Mon May 14 09:11:30 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Mon May 14 09:16:47 2007 +0200
@@ -1817,7 +1817,7 @@
lemma tan_sec: "cos x \<noteq> 0 ==> 1 + tan(x) ^ 2 = inverse(cos x) ^ 2"
apply (rule power_inverse [THEN subst])
apply (rule_tac c1 = "(cos x)\<twosuperior>" in real_mult_right_cancel [THEN iffD1])
-apply (auto dest: realpow_not_zero
+apply (auto dest: field_power_not_zero
simp add: power_mult_distrib left_distrib power_divide tan_def
mult_assoc power_inverse [symmetric]
simp del: realpow_Suc)
@@ -1927,7 +1927,7 @@
qed

lemma lemma_real_divide_sqrt_ge_minus_one:
-     "0 < x ==> -1 \<le> x/(sqrt (x * x + y * y))"
+     "0 < x ==> -1 \<le> x/(sqrt (x * x + y * y))"
by (simp add: divide_const_simps linorder_not_le [symmetric]
del: real_sqrt_le_0_iff real_sqrt_ge_0_iff)

@@ -2159,14 +2159,10 @@
done

lemma real_sqrt_ge_abs1 [simp]: "\<bar>x\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
-apply (rule_tac n = 1 in realpow_increasing)
-apply (auto simp add: numeral_2_eq_2 [symmetric] power2_abs)
-done
+by (rule power2_le_imp_le, simp_all)

lemma real_sqrt_ge_abs2 [simp]: "\<bar>y\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
-apply (rule real_sqrt_ge_abs1)
-done
+by (rule power2_le_imp_le, simp_all)

lemma real_sqrt_two_gt_zero [simp]: "0 < sqrt 2"
by simp
@@ -2192,9 +2188,8 @@
"[| 0 < u; x < u/2; y < u/2; 0 \<le> x; 0 \<le> y |] ==> sqrt (x\<twosuperior> + y\<twosuperior>) < u"
apply (rule_tac y = "u/sqrt 2" in order_le_less_trans)
apply (erule_tac [2] lemma_real_divide_sqrt_less)
-apply (rule_tac n = 1 in realpow_increasing)
-apply (auto simp add: real_0_le_divide_iff power_divide numeral_2_eq_2 [symmetric]
-        simp del: realpow_Suc)
+apply (rule power2_le_imp_le)
+apply (auto simp add: real_0_le_divide_iff power_divide)
apply (rule_tac t = "u\<twosuperior>" in real_sum_of_halves [THEN subst])