# HG changeset patch
# User huffman
# Date 1179679732 -7200
# Node ID 03fe1dafa4189a415d49608c1d173ef2a482d0d3
# Parent  0e36f0dbfa1c2a59fd1feb730e8abc63b06bff28
define pi with THE instead of SOME; cleaned up

diff -r 0e36f0dbfa1c -r 03fe1dafa418 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Sun May 20 17:49:10 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Sun May 20 18:48:52 2007 +0200
@@ -1150,7 +1150,7 @@
 
 definition
   pi :: "real" where
-  "pi = 2 * (@x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
+  "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
 
 text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"}; 
    hence define pi.*}
@@ -1244,7 +1244,7 @@
 lemma fact_lemma: "real (n::nat) * 4 = real (4 * n)"
 by simp
 
-lemma cos_two_less_zero: "cos (2) < 0"
+lemma cos_two_less_zero [simp]: "cos (2) < 0"
 apply (cut_tac x = 2 in cos_paired)
 apply (drule sums_minus)
 apply (rule neg_less_iff_less [THEN iffD1]) 
@@ -1270,9 +1270,9 @@
 apply (rule real_of_nat_less_iff [THEN iffD2])
 apply (rule fact_less_mono, auto)
 done
-declare cos_two_less_zero [simp]
-declare cos_two_less_zero [THEN less_imp_neq, simp]
-declare cos_two_less_zero [THEN order_less_imp_le, simp]
+
+lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq]
+lemmas cos_two_le_zero [simp] = cos_two_less_zero [THEN order_less_imp_le]
 
 lemma cos_is_zero: "EX! x. 0 \<le> x & x \<le> 2 & cos x = 0"
 apply (subgoal_tac "\<exists>x. 0 \<le> x & x \<le> 2 & cos x = 0")
@@ -1290,51 +1290,41 @@
 apply (drule_tac y1 = y in order_le_less_trans [THEN sin_gt_zero], assumption, simp_all) 
 done
     
-lemma pi_half: "pi/2 = (@x. 0 \<le> x & x \<le> 2 & cos x = 0)"
+lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
 by (simp add: pi_def)
 
 lemma cos_pi_half [simp]: "cos (pi / 2) = 0"
-apply (rule cos_is_zero [THEN ex1E])
-apply (auto intro!: someI2 simp add: pi_half)
+by (simp add: pi_half cos_is_zero [THEN theI'])
+
+lemma pi_half_gt_zero [simp]: "0 < pi / 2"
+apply (rule order_le_neq_trans)
+apply (simp add: pi_half cos_is_zero [THEN theI'])
+apply (rule notI, drule arg_cong [where f=cos], simp)
 done
 
-lemma pi_half_gt_zero: "0 < pi / 2"
-apply (rule cos_is_zero [THEN ex1E])
-apply (auto simp add: pi_half)
-apply (rule someI2, blast, safe)
-apply (drule_tac y = xa in order_le_imp_less_or_eq)
-apply (safe, simp)
-done
-declare pi_half_gt_zero [simp]
-declare pi_half_gt_zero [THEN less_imp_neq, THEN not_sym, simp]
-declare pi_half_gt_zero [THEN order_less_imp_le, simp]
+lemmas pi_half_neq_zero [simp] = pi_half_gt_zero [THEN less_imp_neq, symmetric]
+lemmas pi_half_ge_zero [simp] = pi_half_gt_zero [THEN order_less_imp_le]
 
-lemma pi_half_less_two: "pi / 2 < 2"
-apply (rule cos_is_zero [THEN ex1E])
-apply (auto simp add: pi_half)
-apply (rule someI2, blast, safe)
-apply (drule_tac x = xa in order_le_imp_less_or_eq)
-apply (safe, simp)
+lemma pi_half_less_two [simp]: "pi / 2 < 2"
+apply (rule order_le_neq_trans)
+apply (simp add: pi_half cos_is_zero [THEN theI'])
+apply (rule notI, drule arg_cong [where f=cos], simp)
 done
-declare pi_half_less_two [simp]
-declare pi_half_less_two [THEN less_imp_neq, simp]
-declare pi_half_less_two [THEN order_less_imp_le, simp]
+
+lemmas pi_half_neq_two [simp] = pi_half_less_two [THEN less_imp_neq]
+lemmas pi_half_le_two [simp] =  pi_half_less_two [THEN order_less_imp_le]
 
 lemma pi_gt_zero [simp]: "0 < pi"
-apply (insert pi_half_gt_zero) 
-apply (simp add: ); 
-done
+by (insert pi_half_gt_zero, simp)
+
+lemma pi_ge_zero [simp]: "0 \<le> pi"
+by (rule pi_gt_zero [THEN order_less_imp_le])
 
 lemma pi_neq_zero [simp]: "pi \<noteq> 0"
 by (rule pi_gt_zero [THEN less_imp_neq, THEN not_sym])
 
-lemma pi_not_less_zero [simp]: "~ (pi < 0)"
-apply (insert pi_gt_zero)
-apply (blast elim: order_less_asym) 
-done
-
-lemma pi_ge_zero [simp]: "0 \<le> pi"
-by (auto intro: order_less_imp_le)
+lemma pi_not_less_zero [simp]: "\<not> pi < 0"
+by (simp add: linorder_not_less)
 
 lemma minus_pi_half_less_zero [simp]: "-(pi/2) < 0"
 by auto
@@ -1342,7 +1332,7 @@
 lemma sin_pi_half [simp]: "sin(pi/2) = 1"
 apply (cut_tac x = "pi/2" in sin_cos_squared_add2)
 apply (cut_tac sin_gt_zero [OF pi_half_gt_zero pi_half_less_two])
-apply (auto simp add: numeral_2_eq_2)
+apply (simp add: power2_eq_square)
 done
 
 lemma cos_pi [simp]: "cos pi = -1"
@@ -1353,6 +1343,7 @@
 
 lemma sin_cos_eq: "sin x = cos (pi/2 - x)"
 by (simp add: diff_minus cos_add)
+declare sin_cos_eq [symmetric, simp]
 
 lemma minus_sin_cos_eq: "-sin x = cos (x + pi/2)"
 by (simp add: cos_add)
@@ -1360,7 +1351,7 @@
 
 lemma cos_sin_eq: "cos x = sin (pi/2 - x)"
 by (simp add: diff_minus sin_add)
-declare sin_cos_eq [symmetric, simp] cos_sin_eq [symmetric, simp]
+declare cos_sin_eq [symmetric, simp]
 
 lemma sin_periodic_pi [simp]: "sin (x + pi) = - sin x"
 by (simp add: sin_add)