define pi with THE instead of SOME; cleaned up
authorhuffman
Sun May 20 18:48:52 2007 +0200 (2007-05-20)
changeset 2305303fe1dafa418
parent 23052 0e36f0dbfa1c
child 23054 d1bbe5afa279
define pi with THE instead of SOME; cleaned up
src/HOL/Hyperreal/Transcendental.thy
     1.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Sun May 20 17:49:10 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Sun May 20 18:48:52 2007 +0200
     1.3 @@ -1150,7 +1150,7 @@
     1.4  
     1.5  definition
     1.6    pi :: "real" where
     1.7 -  "pi = 2 * (@x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
     1.8 +  "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
     1.9  
    1.10  text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"}; 
    1.11     hence define pi.*}
    1.12 @@ -1244,7 +1244,7 @@
    1.13  lemma fact_lemma: "real (n::nat) * 4 = real (4 * n)"
    1.14  by simp
    1.15  
    1.16 -lemma cos_two_less_zero: "cos (2) < 0"
    1.17 +lemma cos_two_less_zero [simp]: "cos (2) < 0"
    1.18  apply (cut_tac x = 2 in cos_paired)
    1.19  apply (drule sums_minus)
    1.20  apply (rule neg_less_iff_less [THEN iffD1]) 
    1.21 @@ -1270,9 +1270,9 @@
    1.22  apply (rule real_of_nat_less_iff [THEN iffD2])
    1.23  apply (rule fact_less_mono, auto)
    1.24  done
    1.25 -declare cos_two_less_zero [simp]
    1.26 -declare cos_two_less_zero [THEN less_imp_neq, simp]
    1.27 -declare cos_two_less_zero [THEN order_less_imp_le, simp]
    1.28 +
    1.29 +lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq]
    1.30 +lemmas cos_two_le_zero [simp] = cos_two_less_zero [THEN order_less_imp_le]
    1.31  
    1.32  lemma cos_is_zero: "EX! x. 0 \<le> x & x \<le> 2 & cos x = 0"
    1.33  apply (subgoal_tac "\<exists>x. 0 \<le> x & x \<le> 2 & cos x = 0")
    1.34 @@ -1290,51 +1290,41 @@
    1.35  apply (drule_tac y1 = y in order_le_less_trans [THEN sin_gt_zero], assumption, simp_all) 
    1.36  done
    1.37      
    1.38 -lemma pi_half: "pi/2 = (@x. 0 \<le> x & x \<le> 2 & cos x = 0)"
    1.39 +lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
    1.40  by (simp add: pi_def)
    1.41  
    1.42  lemma cos_pi_half [simp]: "cos (pi / 2) = 0"
    1.43 -apply (rule cos_is_zero [THEN ex1E])
    1.44 -apply (auto intro!: someI2 simp add: pi_half)
    1.45 +by (simp add: pi_half cos_is_zero [THEN theI'])
    1.46 +
    1.47 +lemma pi_half_gt_zero [simp]: "0 < pi / 2"
    1.48 +apply (rule order_le_neq_trans)
    1.49 +apply (simp add: pi_half cos_is_zero [THEN theI'])
    1.50 +apply (rule notI, drule arg_cong [where f=cos], simp)
    1.51  done
    1.52  
    1.53 -lemma pi_half_gt_zero: "0 < pi / 2"
    1.54 -apply (rule cos_is_zero [THEN ex1E])
    1.55 -apply (auto simp add: pi_half)
    1.56 -apply (rule someI2, blast, safe)
    1.57 -apply (drule_tac y = xa in order_le_imp_less_or_eq)
    1.58 -apply (safe, simp)
    1.59 -done
    1.60 -declare pi_half_gt_zero [simp]
    1.61 -declare pi_half_gt_zero [THEN less_imp_neq, THEN not_sym, simp]
    1.62 -declare pi_half_gt_zero [THEN order_less_imp_le, simp]
    1.63 +lemmas pi_half_neq_zero [simp] = pi_half_gt_zero [THEN less_imp_neq, symmetric]
    1.64 +lemmas pi_half_ge_zero [simp] = pi_half_gt_zero [THEN order_less_imp_le]
    1.65  
    1.66 -lemma pi_half_less_two: "pi / 2 < 2"
    1.67 -apply (rule cos_is_zero [THEN ex1E])
    1.68 -apply (auto simp add: pi_half)
    1.69 -apply (rule someI2, blast, safe)
    1.70 -apply (drule_tac x = xa in order_le_imp_less_or_eq)
    1.71 -apply (safe, simp)
    1.72 +lemma pi_half_less_two [simp]: "pi / 2 < 2"
    1.73 +apply (rule order_le_neq_trans)
    1.74 +apply (simp add: pi_half cos_is_zero [THEN theI'])
    1.75 +apply (rule notI, drule arg_cong [where f=cos], simp)
    1.76  done
    1.77 -declare pi_half_less_two [simp]
    1.78 -declare pi_half_less_two [THEN less_imp_neq, simp]
    1.79 -declare pi_half_less_two [THEN order_less_imp_le, simp]
    1.80 +
    1.81 +lemmas pi_half_neq_two [simp] = pi_half_less_two [THEN less_imp_neq]
    1.82 +lemmas pi_half_le_two [simp] =  pi_half_less_two [THEN order_less_imp_le]
    1.83  
    1.84  lemma pi_gt_zero [simp]: "0 < pi"
    1.85 -apply (insert pi_half_gt_zero) 
    1.86 -apply (simp add: ); 
    1.87 -done
    1.88 +by (insert pi_half_gt_zero, simp)
    1.89 +
    1.90 +lemma pi_ge_zero [simp]: "0 \<le> pi"
    1.91 +by (rule pi_gt_zero [THEN order_less_imp_le])
    1.92  
    1.93  lemma pi_neq_zero [simp]: "pi \<noteq> 0"
    1.94  by (rule pi_gt_zero [THEN less_imp_neq, THEN not_sym])
    1.95  
    1.96 -lemma pi_not_less_zero [simp]: "~ (pi < 0)"
    1.97 -apply (insert pi_gt_zero)
    1.98 -apply (blast elim: order_less_asym) 
    1.99 -done
   1.100 -
   1.101 -lemma pi_ge_zero [simp]: "0 \<le> pi"
   1.102 -by (auto intro: order_less_imp_le)
   1.103 +lemma pi_not_less_zero [simp]: "\<not> pi < 0"
   1.104 +by (simp add: linorder_not_less)
   1.105  
   1.106  lemma minus_pi_half_less_zero [simp]: "-(pi/2) < 0"
   1.107  by auto
   1.108 @@ -1342,7 +1332,7 @@
   1.109  lemma sin_pi_half [simp]: "sin(pi/2) = 1"
   1.110  apply (cut_tac x = "pi/2" in sin_cos_squared_add2)
   1.111  apply (cut_tac sin_gt_zero [OF pi_half_gt_zero pi_half_less_two])
   1.112 -apply (auto simp add: numeral_2_eq_2)
   1.113 +apply (simp add: power2_eq_square)
   1.114  done
   1.115  
   1.116  lemma cos_pi [simp]: "cos pi = -1"
   1.117 @@ -1353,6 +1343,7 @@
   1.118  
   1.119  lemma sin_cos_eq: "sin x = cos (pi/2 - x)"
   1.120  by (simp add: diff_minus cos_add)
   1.121 +declare sin_cos_eq [symmetric, simp]
   1.122  
   1.123  lemma minus_sin_cos_eq: "-sin x = cos (x + pi/2)"
   1.124  by (simp add: cos_add)
   1.125 @@ -1360,7 +1351,7 @@
   1.126  
   1.127  lemma cos_sin_eq: "cos x = sin (pi/2 - x)"
   1.128  by (simp add: diff_minus sin_add)
   1.129 -declare sin_cos_eq [symmetric, simp] cos_sin_eq [symmetric, simp]
   1.130 +declare cos_sin_eq [symmetric, simp]
   1.131  
   1.132  lemma sin_periodic_pi [simp]: "sin (x + pi) = - sin x"
   1.133  by (simp add: sin_add)