author huffman Sun May 20 18:48:52 2007 +0200 (2007-05-20) changeset 23053 03fe1dafa418 parent 23052 0e36f0dbfa1c child 23054 d1bbe5afa279
define pi with THE instead of SOME; cleaned up
```     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.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.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.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.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.121 +declare sin_cos_eq [symmetric, simp]
1.122
1.123  lemma minus_sin_cos_eq: "-sin x = cos (x + pi/2)"