# HG changeset patch
# User huffman
# Date 1166048139 -3600
# Node ID 1701f05aa1b09c1ed17f9ad5e9b573a0b7ca889d
# Parent  e3a7205fcb011201afd316d5b1b5307b10eaa10a
remove uses of star_n and FreeUltrafilterNat

diff -r e3a7205fcb01 -r 1701f05aa1b0 src/HOL/Hyperreal/HSeries.thy
--- a/src/HOL/Hyperreal/HSeries.thy	Wed Dec 13 21:46:34 2006 +0100
+++ b/src/HOL/Hyperreal/HSeries.thy	Wed Dec 13 23:15:39 2006 +0100
@@ -28,102 +28,70 @@
   NSsuminf   :: "(nat=>real) => real" where
   "NSsuminf f = (THE s. f NSsums s)"
 
-
-lemma sumhr:
-     "sumhr(star_n M, star_n N, f) =  
-      star_n (%n. setsum f {M n..<N n})"
-by (simp add: sumhr_def starfun2_star_n)
+lemma sumhr_app: "sumhr(M,N,f) = ( *f2* (\<lambda>m n. setsum f {m..<n})) M N"
+by (simp add: sumhr_def)
 
 text{*Base case in definition of @{term sumr}*}
-lemma sumhr_zero [simp]: "sumhr (m,0,f) = 0"
-apply (cases m)
-apply (simp add: star_n_zero_num sumhr symmetric)
-done
+lemma sumhr_zero [simp]: "!!m. sumhr (m,0,f) = 0"
+unfolding sumhr_app by transfer simp
 
 text{*Recursive case in definition of @{term sumr}*}
 lemma sumhr_if: 
-     "sumhr(m,n+1,f) = 
+     "!!m n. sumhr(m,n+1,f) = 
       (if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *f* f) n)"
-apply (cases m, cases n)
-apply (auto simp add: star_n_one_num sumhr star_n_add star_n_le starfun
-           star_n_zero_num star_n_eq_iff, ultra+)
-done
+unfolding sumhr_app by transfer simp
 
-lemma sumhr_Suc_zero [simp]: "sumhr (n + 1, n, f) = 0"
-apply (cases n)
-apply (simp add: star_n_one_num sumhr star_n_add star_n_zero_num)
-done
+lemma sumhr_Suc_zero [simp]: "!!n. sumhr (n + 1, n, f) = 0"
+unfolding sumhr_app by transfer simp
 
-lemma sumhr_eq_bounds [simp]: "sumhr (n,n,f) = 0"
-apply (cases n)
-apply (simp add: sumhr star_n_zero_num)
-done
+lemma sumhr_eq_bounds [simp]: "!!n. sumhr (n,n,f) = 0"
+unfolding sumhr_app by transfer simp
+
+lemma sumhr_Suc [simp]: "!!m. sumhr (m,m + 1,f) = ( *f* f) m"
+unfolding sumhr_app by transfer simp
 
-lemma sumhr_Suc [simp]: "sumhr (m,m + 1,f) = ( *f* f) m"
-apply (cases m)
-apply (simp add: sumhr star_n_one_num star_n_add starfun)
-done
+lemma sumhr_add_lbound_zero [simp]: "!!k m. sumhr(m+k,k,f) = 0"
+unfolding sumhr_app by transfer simp
 
-lemma sumhr_add_lbound_zero [simp]: "sumhr(m+k,k,f) = 0"
-apply (cases m, cases k)
-apply (simp add: sumhr star_n_add star_n_zero_num)
-done
+lemma sumhr_add:
+  "!!m n. sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
+unfolding sumhr_app by transfer (rule setsum_addf [symmetric])
 
-lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
-apply (cases m, cases n)
-apply (simp add: sumhr star_n_add setsum_addf)
-done
+lemma sumhr_mult:
+  "!!m n. hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
+unfolding sumhr_app by transfer (rule setsum_right_distrib)
 
-lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
-apply (cases m, cases n)
-apply (simp add: sumhr star_of_def star_n_mult setsum_right_distrib)
-done
-
-lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
-apply (cases n, cases p)
-apply (auto elim!: FreeUltrafilterNat_subset simp 
-            add: star_n_zero_num sumhr star_n_add star_n_less setsum_add_nat_ivl star_n_eq_iff)
-done
+lemma sumhr_split_add:
+  "!!n p. n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
+unfolding sumhr_app by transfer (simp add: setsum_add_nat_ivl)
 
 lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)"
 by (drule_tac f = f in sumhr_split_add [symmetric], simp)
 
-lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
-apply (cases n, cases m)
-apply (simp add: sumhr star_n_le star_n_abs setsum_abs)
-done
+lemma sumhr_hrabs: "!!m n. abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
+unfolding sumhr_app by transfer (rule setsum_abs)
 
 text{* other general version also needed *}
 lemma sumhr_fun_hypnat_eq:
    "(\<forall>r. m \<le> r & r < n --> f r = g r) -->  
       sumhr(hypnat_of_nat m, hypnat_of_nat n, f) =  
       sumhr(hypnat_of_nat m, hypnat_of_nat n, g)"
-by (fastsimp simp add: sumhr hypnat_of_nat_eq intro:setsum_cong)
-
+unfolding sumhr_app by transfer simp
 
 lemma sumhr_const:
-     "sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
-apply (cases n)
-apply (simp add: sumhr star_n_zero_num hypreal_of_hypnat 
-                 star_of_def star_n_mult real_of_nat_def)
-done
+     "!!n. sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
+unfolding sumhr_app by transfer (simp add: real_of_nat_def)
 
-lemma sumhr_less_bounds_zero [simp]: "n < m ==> sumhr(m,n,f) = 0"
-apply (cases m, cases n)
-apply (auto elim: FreeUltrafilterNat_subset
-            simp add: sumhr star_n_less star_n_zero_num star_n_eq_iff)
-done
+lemma sumhr_less_bounds_zero [simp]: "!!m n. n < m ==> sumhr(m,n,f) = 0"
+unfolding sumhr_app by transfer simp
 
-lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
-apply (cases m, cases n)
-apply (simp add: sumhr star_n_minus setsum_negf)
-done
+lemma sumhr_minus: "!!m n. sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
+unfolding sumhr_app by transfer (rule setsum_negf)
 
 lemma sumhr_shift_bounds:
-     "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))"
-apply (cases m, cases n)
-apply (simp add: sumhr star_n_add setsum_shift_bounds_nat_ivl hypnat_of_nat_eq)
-done
+  "!!m n. sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) =
+          sumhr(m,n,%i. f(i + k))"
+unfolding sumhr_app by transfer (rule setsum_shift_bounds_nat_ivl)
 
 
 subsection{*Nonstandard Sums*}
@@ -132,30 +100,30 @@
  (such as @{term whn})*}
 lemma sumhr_hypreal_of_hypnat_omega: 
       "sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn"
-by (simp add: hypnat_omega_def star_n_zero_num sumhr hypreal_of_hypnat
-              real_of_nat_def)
+by (simp add: sumhr_const)
 
 lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = omega - 1"
-by (simp add: hypnat_omega_def star_n_zero_num omega_def star_n_one_num
-              sumhr star_n_diff real_of_nat_def)
+apply (simp add: sumhr_const)
+(* FIXME: need lemma: hypreal_of_hypnat whn = omega - 1 *)
+(* maybe define omega = hypreal_of_hypnat whn + 1 *)
+apply (unfold star_class_defs omega_def hypnat_omega_def
+              hypreal_of_hypnat_def star_of_def)
+apply (simp add: starfun_star_n starfun2_star_n real_of_nat_def)
+done
 
 lemma sumhr_minus_one_realpow_zero [simp]: 
-     "sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0"
-by (simp del: realpow_Suc 
-         add: sumhr star_n_add nat_mult_2 [symmetric] star_n_zero_num 
-              star_n_zero_num hypnat_omega_def)
+     "!!N. sumhr(0, N + N, %i. (-1) ^ (i+1)) = 0"
+unfolding sumhr_app
+by transfer (simp del: realpow_Suc add: nat_mult_2 [symmetric])
 
 lemma sumhr_interval_const:
      "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na  
       ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) =  
           (hypreal_of_nat (na - m) * hypreal_of_real r)"
-by(simp add: sumhr hypreal_of_nat_eq hypnat_of_nat_eq
-             real_of_nat_def star_of_def star_n_mult cong: setsum_ivl_cong)
+unfolding sumhr_app by transfer simp
 
-lemma starfunNat_sumr: "( *f* (%n. setsum f {0..<n})) N = sumhr(0,N,f)"
-apply (cases N)
-apply (simp add: star_n_zero_num starfun sumhr)
-done
+lemma starfunNat_sumr: "!!N. ( *f* (%n. setsum f {0..<n})) N = sumhr(0,N,f)"
+unfolding sumhr_app by transfer (rule refl)
 
 lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) @= sumhr(0, N, f)  
       ==> abs (sumhr(M, N, f)) @= 0"
diff -r e3a7205fcb01 -r 1701f05aa1b0 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Wed Dec 13 21:46:34 2006 +0100
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Wed Dec 13 23:15:39 2006 +0100
@@ -242,22 +242,28 @@
 
 lemma exphr_zero [simp]: "exphr 0 = 1"
 apply (simp add: exphr_def sumhr_split_add
-                   [OF hypnat_one_less_hypnat_omega, symmetric]) 
-apply (simp add: sumhr star_n_zero_num starfun star_n_one_num star_n_add
-                 hypnat_omega_def
-            del: OrderedGroup.add_0)
-apply (simp add: star_n_one_num [symmetric])
+                   [OF hypnat_one_less_hypnat_omega, symmetric])
+apply (rule st_unique, simp)
+apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
+apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
+apply (rule_tac x="whn" in spec)
+apply (unfold sumhr_app, transfer, simp)
 done
 
 lemma coshr_zero [simp]: "coshr 0 = 1"
 apply (simp add: coshr_def sumhr_split_add
                    [OF hypnat_one_less_hypnat_omega, symmetric]) 
-apply (simp add: sumhr star_n_zero_num star_n_one_num hypnat_omega_def)
-apply (simp add: star_n_one_num [symmetric] star_n_zero_num [symmetric])
+apply (rule st_unique, simp)
+apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
+apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
+apply (rule_tac x="whn" in spec)
+apply (unfold sumhr_app, transfer, simp)
 done
 
 lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) 0 @= 1"
-by (simp add: star_n_zero_num star_n_one_num starfun)
+apply (subgoal_tac "( *f* exp) 0 = 1", simp)
+apply (transfer, simp)
+done
 
 lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) x @= 1"
 apply (case_tac "x = 0")
@@ -276,24 +282,21 @@
 by (auto intro: STAR_exp_Infinitesimal)
 
 lemma STAR_exp_add: "!!x y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
-by (transfer, rule exp_add)
+by transfer (rule exp_add)
 
 lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)"
 apply (simp add: exphr_def)
-apply (rule st_hypreal_of_real [THEN subst])
-apply (rule approx_st_eq, auto)
-apply (rule approx_minus_iff [THEN iffD2])
-apply (simp only: mem_infmal_iff [symmetric])
-apply (auto simp add: mem_infmal_iff [symmetric] star_of_def star_n_zero_num hypnat_omega_def sumhr star_n_diff)
-apply (rule NSLIMSEQ_zero_Infinitesimal_hypreal)
-apply (insert exp_converges [of x]) 
-apply (simp add: sums_def) 
-apply (drule LIMSEQ_const [THEN [2] LIMSEQ_diff, where b = "exp x"])
-apply (simp add: LIMSEQ_NSLIMSEQ_iff)
+apply (rule st_unique, simp)
+apply (subst starfunNat_sumr [symmetric])
+apply (rule NSLIMSEQ_D [THEN approx_sym])
+apply (rule LIMSEQ_NSLIMSEQ)
+apply (subst sums_def [symmetric])
+apply (rule exp_converges)
+apply (rule HNatInfinite_whn)
 done
 
 lemma starfun_exp_ge_add_one_self [simp]: "!!x. 0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
-by (transfer, rule exp_ge_add_one_self_aux)
+by transfer (rule exp_ge_add_one_self_aux)
 
 (* exp (oo) is infinite *)
 lemma starfun_exp_HInfinite:
@@ -304,7 +307,7 @@
 done
 
 lemma starfun_exp_minus: "!!x. ( *f* exp) (-x) = inverse(( *f* exp) x)"
-by (transfer, rule exp_minus)
+by transfer (rule exp_minus)
 
 (* exp (-oo) is infinitesimal *)
 lemma starfun_exp_Infinitesimal:
@@ -316,7 +319,7 @@
 done
 
 lemma starfun_exp_gt_one [simp]: "!!x. 0 < x ==> 1 < ( *f* exp) x"
-by (transfer, simp)
+by transfer (rule exp_gt_one)
 
 (* needs derivative of inverse function
    TRY a NS one today!!!
@@ -332,25 +335,25 @@
 
 
 lemma starfun_ln_exp [simp]: "!!x. ( *f* ln) (( *f* exp) x) = x"
-by (transfer, simp)
+by transfer (rule ln_exp)
 
 lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* ln) x) = x) = (0 < x)"
-by (transfer, simp)
+by transfer (rule exp_ln_iff)
 
-lemma starfun_exp_ln_eq: "( *f* exp) u = x ==> ( *f* ln) x = u"
-by auto
+lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* ln) x = u"
+by transfer (rule exp_ln_eq)
 
 lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* ln) x < x"
-by (transfer, simp)
+by transfer (rule ln_less_self)
 
 lemma starfun_ln_ge_zero [simp]: "!!x. 1 \<le> x ==> 0 \<le> ( *f* ln) x"
-by (transfer, simp)
+by transfer (rule ln_ge_zero)
 
 lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* ln) x"
-by (transfer, simp)
+by transfer (rule ln_gt_zero)
 
 lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
-by (transfer, simp)
+by transfer simp
 
 lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* ln) x \<in> HFinite"
 apply (rule HFinite_bounded)
@@ -359,7 +362,7 @@
 done
 
 lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
-by (transfer, rule ln_inverse)
+by transfer (rule ln_inverse)
 
 lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) x\<bar> = ( *f* exp) x"
 by transfer (rule abs_exp_cancel)
@@ -416,7 +419,7 @@
 done
 
 lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
-by (transfer, simp)
+by transfer (rule ln_less_zero)
 
 lemma starfun_ln_Infinitesimal_less_zero:
      "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0"
@@ -443,7 +446,7 @@
 done
 
 lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
-by (transfer, simp)
+by transfer (rule sin_zero)
 
 lemma STAR_sin_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* sin) x @= x"
 apply (case_tac "x = 0")
@@ -465,7 +468,7 @@
                    summable_convergent_sumr_iff [symmetric] summable_cos)
 
 lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
-by (simp add: starfun star_n_zero_num star_n_one_num)
+by transfer (rule cos_zero)
 
 lemma STAR_cos_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* cos) x @= 1"
 apply (case_tac "x = 0")
@@ -481,7 +484,7 @@
 done
 
 lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
-by (simp add: starfun star_n_zero_num)
+by transfer (rule tan_zero)
 
 lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x @= x"
 apply (case_tac "x = 0")