tuned proofs
authorhuffman
Mon May 14 23:25:16 2007 +0200 (2007-05-14)
changeset 229761d73b1feaacf
parent 22975 03085c441c14
child 22977 04fd6cc1c4a9
tuned proofs
src/HOL/Hyperreal/Transcendental.thy
     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.34 +by (simp add: sum_squares_gt_zero_iff)
    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.41 +by (simp add: sum_squares_gt_zero_iff)
    1.42  
    1.43  lemma real_sqrt_sum_squares_gt_zero3: "x \<noteq> 0 ==> 0 < sqrt(x\<twosuperior> + y\<twosuperior>)"
    1.44  by (simp add: add_pos_nonneg)
    1.45 @@ -1942,15 +1930,13 @@
    1.46  by (simp add: add_nonneg_pos)
    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.54 -apply (simp add: real_add_commute)
    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.74  by (subst add_commute, simp add: minus_sqrt_le) 
    1.75  
    1.76  lemma not_neg_sqrt_sumsq: "~ sqrt (x * x + y * y) < 0"
    1.77 -by (simp add: linorder_not_less
    1.78 -         del: real_sqrt_lt_0_iff real_sqrt_ge_0_iff)
    1.79 +by (simp add: not_sum_squares_lt_zero)
    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.84  by (subst add_commute, simp add: cos_x_y_ge_minus_one)
    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.95  apply (simp add: real_add_commute)
    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: