# HG changeset patch
# User huffman
# Date 1158935115 -7200
# Node ID cecff1f514319f62d9c853d227f134e687629fb1
# Parent  0e4df994ad348628b6065a8f48bd956e9f3d9792
define constants with THE instead of SOME

diff -r 0e4df994ad34 -r cecff1f51431 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Fri Sep 22 14:36:23 2006 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Fri Sep 22 16:25:15 2006 +0200
@@ -26,19 +26,19 @@
 
   lim :: "(nat => real) => real"
     --{*Standard definition of limit using choice operator*}
-  "lim X = (SOME L. (X ----> L))"
+  "lim X = (THE L. X ----> L)"
 
   nslim :: "(nat => real) => real"
     --{*Nonstandard definition of limit using choice operator*}
-  "nslim X = (SOME L. (X ----NS> L))"
+  "nslim X = (THE L. X ----NS> L)"
 
   convergent :: "(nat => 'a::real_normed_vector) => bool"
     --{*Standard definition of convergence*}
-  "convergent X = (\<exists>L. (X ----> L))"
+  "convergent X = (\<exists>L. X ----> L)"
 
   NSconvergent :: "(nat => 'a::real_normed_vector) => bool"
     --{*Nonstandard definition of convergence*}
-  "NSconvergent X = (\<exists>L. (X ----NS> L))"
+  "NSconvergent X = (\<exists>L. X ----NS> L)"
 
   Bseq :: "(nat => 'a::real_normed_vector) => bool"
     --{*Standard definition for bounded sequence*}
@@ -413,10 +413,10 @@
 by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)
 
 lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X ----NS> nslim X)"
-by (auto intro: someI simp add: NSconvergent_def nslim_def)
+by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def)
 
 lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
-by (auto intro: someI simp add: convergent_def lim_def)
+by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def)
 
 text{*Subsequence (alternative definition, (e.g. Hoskins)*}
 
diff -r 0e4df994ad34 -r cecff1f51431 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Fri Sep 22 14:36:23 2006 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Fri Sep 22 16:25:15 2006 +0200
@@ -13,7 +13,7 @@
 
 definition
   root :: "[nat,real] => real"
-  "root n x = (SOME u. ((0::real) < x --> 0 < u) & (u ^ n = x))"
+  "root n x = (THE u. ((0::real) < x --> 0 < u) & (u ^ n = x))"
 
   sqrt :: "real => real"
   "sqrt x = root 2 x"
@@ -53,23 +53,23 @@
 
 lemma real_root_zero [simp]: "root (Suc n) 0 = 0"
 apply (simp add: root_def)
-apply (safe intro!: some_equality power_0_Suc elim!: realpow_zero_zero)
+apply (safe intro!: the_equality power_0_Suc elim!: realpow_zero_zero)
 done
 
 lemma real_root_pow_pos: 
-     "0 < x ==> (root(Suc n) x) ^ (Suc n) = x"
-apply (simp add: root_def)
-apply (drule_tac n = n in realpow_pos_nth2)
-apply (auto intro: someI2)
+     "0 < x ==> (root (Suc n) x) ^ (Suc n) = x"
+apply (simp add: root_def del: realpow_Suc)
+apply (drule_tac n="Suc n" in realpow_pos_nth_unique, simp)
+apply (erule theI' [THEN conjunct2])
 done
 
-lemma real_root_pow_pos2: "0 \<le> x ==> (root(Suc n) x) ^ (Suc n) = x"
+lemma real_root_pow_pos2: "0 \<le> x ==> (root (Suc n) x) ^ (Suc n) = x"
 by (auto dest!: real_le_imp_less_or_eq dest: real_root_pow_pos)
 
 lemma real_root_pos: 
      "0 < x ==> root(Suc n) (x ^ (Suc n)) = x"
 apply (simp add: root_def)
-apply (rule some_equality)
+apply (rule the_equality)
 apply (frule_tac [2] n = n in zero_less_power)
 apply (auto simp add: zero_less_mult_iff)
 apply (rule_tac x = u and y = x in linorder_cases)
@@ -81,21 +81,23 @@
 lemma real_root_pos2: "0 \<le> x ==> root(Suc n) (x ^ (Suc n)) = x"
 by (auto dest!: real_le_imp_less_or_eq real_root_pos)
 
+lemma real_root_gt_zero:
+     "0 < x ==> 0 < root (Suc n) x"
+apply (simp add: root_def del: realpow_Suc)
+apply (drule_tac n="Suc n" in realpow_pos_nth_unique, simp)
+apply (erule theI' [THEN conjunct1])
+done
+
 lemma real_root_pos_pos: 
      "0 < x ==> 0 \<le> root(Suc n) x"
-apply (simp add: root_def)
-apply (drule_tac n = n in realpow_pos_nth2)
-apply (safe, rule someI2)
-apply (auto intro!: order_less_imp_le dest: zero_less_power 
-            simp add: zero_less_mult_iff)
-done
+by (rule real_root_gt_zero [THEN order_less_imp_le])
 
 lemma real_root_pos_pos_le: "0 \<le> x ==> 0 \<le> root(Suc n) x"
-by (auto dest!: real_le_imp_less_or_eq dest: real_root_pos_pos)
+by (auto simp add: order_le_less real_root_gt_zero)
 
 lemma real_root_one [simp]: "root (Suc n) 1 = 1"
 apply (simp add: root_def)
-apply (rule some_equality, auto)
+apply (rule the_equality, auto)
 apply (rule ccontr)
 apply (rule_tac x = u and y = 1 in linorder_cases)
 apply (drule_tac n = n in realpow_Suc_less_one)
@@ -159,10 +161,7 @@
 done
 
 lemma real_sqrt_gt_zero: "0 < x ==> 0 < sqrt(x)"
-apply (simp add: sqrt_def root_def)
-apply (drule realpow_pos_nth2 [where n=1], safe)
-apply (rule someI2, auto)
-done
+by (simp add: sqrt_def real_root_gt_zero)
 
 lemma real_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> sqrt(x)"
 by (auto intro: real_sqrt_gt_zero simp add: order_le_less)
@@ -180,10 +179,9 @@
 *)
 
 lemma sqrt_eqI: "[|r\<twosuperior> = a; 0 \<le> r|] ==> sqrt a = r"
-apply (unfold sqrt_def root_def) 
-apply (rule someI2 [of _ r], auto) 
-apply (auto simp add: numeral_2_eq_2 simp del: realpow_Suc 
-            dest: power_inject_base) 
+apply (erule subst)
+apply (simp add: sqrt_def numeral_2_eq_2 del: realpow_Suc)
+apply (erule real_root_pos2)
 done
 
 lemma real_sqrt_mult_distrib: