change definitions from SOME to THE
authorhuffman
Sun Sep 24 03:38:36 2006 +0200 (2006-09-24)
changeset 20688690d866a165d
parent 20687 fedb901be392
child 20689 4950e45442b8
change definitions from SOME to THE
src/HOL/Hyperreal/HSeries.thy
src/HOL/Hyperreal/Series.thy
     1.1 --- a/src/HOL/Hyperreal/HSeries.thy	Sun Sep 24 02:56:59 2006 +0200
     1.2 +++ b/src/HOL/Hyperreal/HSeries.thy	Sun Sep 24 03:38:36 2006 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4    "NSsummable f = (\<exists>s. f NSsums s)"
     1.5  
     1.6    NSsuminf   :: "(nat=>real) => real"
     1.7 -  "NSsuminf f = (SOME s. f NSsums s)"
     1.8 +  "NSsuminf f = (THE s. f NSsums s)"
     1.9  
    1.10  
    1.11  lemma sumhr:
    1.12 @@ -179,8 +179,8 @@
    1.13  by (simp add: NSsums_def NSsummable_def, blast)
    1.14  
    1.15  lemma NSsummable_NSsums: "NSsummable f ==> f NSsums (NSsuminf f)"
    1.16 -apply (simp add: NSsummable_def NSsuminf_def)
    1.17 -apply (blast intro: someI2)
    1.18 +apply (simp add: NSsummable_def NSsuminf_def NSsums_def)
    1.19 +apply (blast intro: theI NSLIMSEQ_unique)
    1.20  done
    1.21  
    1.22  lemma NSsums_unique: "f NSsums s ==> (s = NSsuminf f)"
     2.1 --- a/src/HOL/Hyperreal/Series.thy	Sun Sep 24 02:56:59 2006 +0200
     2.2 +++ b/src/HOL/Hyperreal/Series.thy	Sun Sep 24 03:38:36 2006 +0200
     2.3 @@ -24,7 +24,7 @@
     2.4     "summable f = (\<exists>s. f sums s)"
     2.5  
     2.6     suminf   :: "(nat=>real) => real"
     2.7 -   "suminf f = (SOME s. f sums s)"
     2.8 +   "suminf f = (THE s. f sums s)"
     2.9  
    2.10  syntax
    2.11    "_suminf" :: "idt => real => real"    ("\<Sum>_. _" [0, 10] 10)
    2.12 @@ -97,15 +97,13 @@
    2.13  by (simp add: sums_def summable_def, blast)
    2.14  
    2.15  lemma summable_sums: "summable f ==> f sums (suminf f)"
    2.16 -apply (simp add: summable_def suminf_def)
    2.17 -apply (blast intro: someI2)
    2.18 +apply (simp add: summable_def suminf_def sums_def)
    2.19 +apply (blast intro: theI LIMSEQ_unique)
    2.20  done
    2.21  
    2.22  lemma summable_sumr_LIMSEQ_suminf: 
    2.23       "summable f ==> (%n. setsum f {0..<n}) ----> (suminf f)"
    2.24 -apply (simp add: summable_def suminf_def sums_def)
    2.25 -apply (blast intro: someI2)
    2.26 -done
    2.27 +by (rule summable_sums [unfolded sums_def])
    2.28  
    2.29  (*-------------------
    2.30      sum is unique