author huffman Mon May 14 23:25:16 2007 +0200 (2007-05-14) changeset 22976 1d73b1feaacf parent 22975 03085c441c14 child 22977 04fd6cc1c4a9
tuned proofs
```     1.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Mon May 14 23:09:54 2007 +0200
1.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Mon May 14 23:25:16 2007 +0200
1.3 @@ -1905,18 +1905,12 @@
1.4  subsection{*Theorems About Sqrt, Transcendental Functions for Complex*}
1.5
1.6  lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"
1.7 -proof (rule order_trans)
1.8 -  show "x \<le> sqrt(x*x)" by (simp add: abs_if)
1.9 -  show "sqrt (x * x) \<le> sqrt (x * x + y * y)"
1.10 -    by (rule real_sqrt_le_mono, auto)
1.11 -qed
1.12 +by (simp add: power2_eq_square [symmetric])
1.13
1.14  lemma minus_le_real_sqrt_sumsq [simp]: "-x \<le> sqrt (x * x + y * y)"
1.15 -proof (rule order_trans)
1.16 -  show "-x \<le> sqrt(x*x)" by (simp add: abs_if)
1.17 -  show "sqrt (x * x) \<le> sqrt (x * x + y * y)"
1.18 -    by (rule real_sqrt_le_mono, auto)
1.19 -qed
1.20 +apply (simp add: power2_eq_square [symmetric])
1.21 +apply (rule power2_le_imp_le, simp_all)
1.22 +done
1.23
1.24  lemma lemma_real_divide_sqrt_ge_minus_one:
1.25       "0 < x ==> -1 \<le> x/(sqrt (x * x + y * y))"
1.26 @@ -1924,16 +1918,10 @@
1.27           del: real_sqrt_le_0_iff real_sqrt_ge_0_iff)
1.28
1.29  lemma real_sqrt_sum_squares_gt_zero1: "x < 0 ==> 0 < sqrt (x * x + y * y)"
1.30 -apply (rule real_sqrt_gt_zero)
1.31 -apply (subgoal_tac "0 < x*x & 0 \<le> y*y", arith)
1.32 -apply (auto simp add: zero_less_mult_iff)
1.33 -done
1.35
1.36  lemma real_sqrt_sum_squares_gt_zero2: "0 < x ==> 0 < sqrt (x * x + y * y)"
1.37 -apply (rule real_sqrt_gt_zero)
1.38 -apply (subgoal_tac "0 < x*x & 0 \<le> y*y", arith)
1.39 -apply (auto simp add: zero_less_mult_iff)
1.40 -done
1.42
1.43  lemma real_sqrt_sum_squares_gt_zero3: "x \<noteq> 0 ==> 0 < sqrt(x\<twosuperior> + y\<twosuperior>)"
1.45 @@ -1942,15 +1930,13 @@
1.47
1.48  lemma real_sqrt_sum_squares_eq_cancel: "sqrt(x\<twosuperior> + y\<twosuperior>) = x ==> y = 0"
1.49 -by (drule_tac f = "%x. x\<twosuperior>" in arg_cong, auto)
1.50 +by (drule_tac f = "%x. x\<twosuperior>" in arg_cong, simp)
1.51
1.52  lemma real_sqrt_sum_squares_eq_cancel2: "sqrt(x\<twosuperior> + y\<twosuperior>) = y ==> x = 0"
1.53 -apply (rule_tac x = y in real_sqrt_sum_squares_eq_cancel)
1.55 -done
1.56 +by (drule_tac f = "%x. x\<twosuperior>" in arg_cong, simp)
1.57
1.58  lemma lemma_real_divide_sqrt_le_one: "x < 0 ==> x/(sqrt (x * x + y * y)) \<le> 1"
1.59 -by (insert lemma_real_divide_sqrt_ge_minus_one [of "-x" y], simp)
1.60 +by (simp add: divide_le_eq not_sum_squares_lt_zero)
1.61
1.62  lemma lemma_real_divide_sqrt_ge_minus_one2:
1.63       "x < 0 ==> -1 \<le> x/(sqrt (x * x + y * y))"
1.64 @@ -1960,7 +1946,7 @@
1.65  done
1.66
1.67  lemma lemma_real_divide_sqrt_le_one2: "0 < x ==> x/(sqrt (x * x + y * y)) \<le> 1"
1.68 -by (cut_tac x = "-x" and y = y in lemma_real_divide_sqrt_ge_minus_one2, auto)
1.69 +by (simp add: divide_le_eq not_sum_squares_lt_zero)
1.70
1.71  lemma minus_sqrt_le: "- sqrt (x * x + y * y) \<le> x"
1.72  by (insert minus_le_real_sqrt_sumsq [of x y], arith)
1.73 @@ -1969,8 +1955,7 @@
1.75
1.76  lemma not_neg_sqrt_sumsq: "~ sqrt (x * x + y * y) < 0"
1.78 -         del: real_sqrt_lt_0_iff real_sqrt_ge_0_iff)
1.80
1.81  lemma cos_x_y_ge_minus_one: "-1 \<le> x / sqrt (x * x + y * y)"
1.82  by (simp add: minus_sqrt_le not_neg_sqrt_sumsq divide_const_simps
1.83 @@ -1980,21 +1965,24 @@
1.85
1.86  lemma cos_x_y_le_one [simp]: "x / sqrt (x * x + y * y) \<le> 1"
1.87 -apply (cut_tac x = x and y = 0 in linorder_less_linear, safe)
1.88 -apply (rule lemma_real_divide_sqrt_le_one)
1.89 -apply (rule_tac [3] lemma_real_divide_sqrt_le_one2, auto)
1.90 -done
1.91 +by (simp add: divide_le_eq not_sum_squares_lt_zero)
1.92
1.93  lemma cos_x_y_le_one2 [simp]: "y / sqrt (x * x + y * y) \<le> 1"
1.94  apply (cut_tac x = y and y = x in cos_x_y_le_one)
1.96  done
1.97
1.98 -declare cos_arccos [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp]
1.99 -declare arccos_bounded [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp]
1.100 +lemmas cos_arccos_lemma1 =
1.101 +  cos_arccos [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp]
1.102 +
1.103 +lemmas arccos_bounded_lemma1 =
1.104 +  arccos_bounded [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp]
1.105
1.106 -declare cos_arccos [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2, simp]
1.107 -declare arccos_bounded [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2, simp]
1.108 +lemmas cos_arccos_lemma2 =
1.109 +  cos_arccos [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2, simp]
1.110 +
1.111 +lemmas arccos_bounded_lemma2 =
1.112 +  arccos_bounded [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2, simp]
1.113
1.114  lemma cos_abs_x_y_ge_minus_one [simp]:
1.115       "-1 \<le> \<bar>x\<bar> / sqrt (x * x + y * y)"
1.116 @@ -2007,21 +1995,25 @@
1.117              simp del: real_sqrt_gt_0_iff real_sqrt_eq_0_iff)
1.118  done
1.119
1.120 -declare cos_arccos [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp]
1.121 -declare arccos_bounded [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp]
1.122 +lemmas cos_arccos_lemma3 =
1.123 +  cos_arccos [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp]
1.124
1.125 -lemma minus_pi_less_zero: "-pi < 0"
1.126 +lemmas arccos_bounded_lemma3 =
1.127 +  arccos_bounded [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp]
1.128 +
1.129 +lemma minus_pi_less_zero [simp]: "-pi < 0"
1.130  by simp
1.131
1.132 -declare minus_pi_less_zero [simp]
1.133 -declare minus_pi_less_zero [THEN order_less_imp_le, simp]
1.134 +lemma minus_pi_le_zero [simp]: "-pi \<le> 0"
1.135 +by simp
1.136
1.137  lemma arccos_ge_minus_pi: "[| -1 \<le> y; y \<le> 1 |] ==> -pi \<le> arccos y"
1.138  apply (rule real_le_trans)
1.139  apply (rule_tac [2] arccos_lbound, auto)
1.140  done
1.141
1.142 -declare arccos_ge_minus_pi [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp]
1.143 +lemmas arccos_ge_minus_pi_lemma =
1.144 +  arccos_ge_minus_pi [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp]
1.145
1.146  (* How tedious! *)
1.147  lemma lemma_divide_rearrange:
```