1.1 --- a/src/HOL/Hyperreal/HSeries.ML	Fri Oct 05 21:50:37 2001 +0200
     1.2 +++ b/src/HOL/Hyperreal/HSeries.ML	Fri Oct 05 21:52:39 2001 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  
     1.5  (* Theorem corresponding to base case in def of sumr *)
     1.6  Goalw [hypnat_zero_def]
     1.7 -     "sumhr (m,0,f) = #0";
     1.8 +     "sumhr (m,0,f) = Numeral0";
     1.9  by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
    1.10  by (auto_tac (claset(), 
    1.11                simpset() addsimps [sumhr, symmetric hypreal_zero_def]));
    1.12 @@ -44,7 +44,7 @@
    1.13  
    1.14  (* Theorem corresponding to recursive case in def of sumr *)
    1.15  Goalw [hypnat_one_def]
    1.16 -     "sumhr(m,n+1hn,f) = (if n + 1hn <= m then #0 \
    1.17 +     "sumhr(m,n+1hn,f) = (if n + 1hn <= m then Numeral0 \
    1.18  \                         else sumhr(m,n,f) + (*fNat* f) n)";
    1.19  by (simp_tac (HOL_ss addsimps
    1.20               [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1); 
    1.21 @@ -55,7 +55,7 @@
    1.22  by (ALLGOALS(Ultra_tac));
    1.23  qed "sumhr_if";
    1.24  
    1.25 -Goalw [hypnat_one_def] "sumhr (n + 1hn, n, f) = #0";
    1.26 +Goalw [hypnat_one_def] "sumhr (n + 1hn, n, f) = Numeral0";
    1.27  by (simp_tac (HOL_ss addsimps
    1.28               [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1); 
    1.29  by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
    1.30 @@ -64,7 +64,7 @@
    1.31  qed "sumhr_Suc_zero";
    1.32  Addsimps [sumhr_Suc_zero];
    1.33  
    1.34 -Goal "sumhr (n,n,f) = #0";
    1.35 +Goal "sumhr (n,n,f) = Numeral0";
    1.36  by (simp_tac (HOL_ss addsimps
    1.37               [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1); 
    1.38  by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
    1.39 @@ -80,7 +80,7 @@
    1.40  qed "sumhr_Suc";
    1.41  Addsimps [sumhr_Suc];
    1.42  
    1.43 -Goal "sumhr(m+k,k,f) = #0";
    1.44 +Goal "sumhr(m+k,k,f) = Numeral0";
    1.45  by (simp_tac (HOL_ss addsimps
    1.46               [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1); 
    1.47  by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
    1.48 @@ -156,7 +156,7 @@
    1.49  		    hypreal_minus,sumr_add RS sym]) 1);
    1.50  qed "sumhr_add_mult_const";
    1.51  
    1.52 -Goal "n < m ==> sumhr (m,n,f) = #0";
    1.53 +Goal "n < m ==> sumhr (m,n,f) = Numeral0";
    1.54  by (simp_tac (HOL_ss addsimps
    1.55               [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1); 
    1.56  by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
    1.57 @@ -185,13 +185,13 @@
    1.58        by summing to some infinite hypernatural (such as whn)
    1.59   -----------------------------------------------------------------*)
    1.60  Goalw [hypnat_omega_def,hypnat_zero_def] 
    1.61 -      "sumhr(0,whn,%i. #1) = hypreal_of_hypnat whn";
    1.62 +      "sumhr(0,whn,%i. Numeral1) = hypreal_of_hypnat whn";
    1.63  by (auto_tac (claset(),
    1.64                simpset() addsimps [sumhr, hypreal_of_hypnat]));
    1.65  qed "sumhr_hypreal_of_hypnat_omega";
    1.66  
    1.67  Goalw [hypnat_omega_def,hypnat_zero_def,omega_def]  
    1.68 -     "sumhr(0, whn, %i. #1) = omega - #1";
    1.69 +     "sumhr(0, whn, %i. Numeral1) = omega - Numeral1";
    1.70  by (simp_tac (HOL_ss addsimps
    1.71               [one_eq_numeral_1 RS sym, hypreal_one_def]) 1); 
    1.72  by (auto_tac (claset(),
    1.73 @@ -199,7 +199,7 @@
    1.74  qed "sumhr_hypreal_omega_minus_one";
    1.75  
    1.76  Goalw [hypnat_zero_def, hypnat_omega_def]
    1.77 -     "sumhr(0, whn + whn, %i. (-#1) ^ (i+1)) = #0";
    1.78 +     "sumhr(0, whn + whn, %i. (-Numeral1) ^ (i+1)) = Numeral0";
    1.79  by (simp_tac (HOL_ss addsimps
    1.80               [zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1); 
    1.81  by (simp_tac (simpset() addsimps [sumhr,hypnat_add,double_lemma] 
    1.82 @@ -223,7 +223,7 @@
    1.83  qed "starfunNat_sumr";
    1.84  
    1.85  Goal "sumhr (0, M, f) @= sumhr (0, N, f) \
    1.86 -\     ==> abs (sumhr (M, N, f)) @= #0";
    1.87 +\     ==> abs (sumhr (M, N, f)) @= Numeral0";
    1.88  by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1);
    1.89  by (auto_tac (claset(), simpset() addsimps [approx_refl]));
    1.90  by (dtac (approx_sym RS (approx_minus_iff RS iffD1)) 1);
    1.91 @@ -265,12 +265,12 @@
    1.92                           sums_unique]) 1);
    1.93  qed "NSsums_unique";
    1.94  
    1.95 -Goal "ALL m. n <= Suc m --> f(m) = #0 ==> f NSsums (sumr 0 n f)";
    1.96 +Goal "ALL m. n <= Suc m --> f(m) = Numeral0 ==> f NSsums (sumr 0 n f)";
    1.97  by (asm_simp_tac (simpset() addsimps [sums_NSsums_iff RS sym, series_zero]) 1);
    1.98  qed "NSseries_zero";
    1.99  
   1.100  Goal "NSsummable f = \
   1.101 -\     (ALL M: HNatInfinite. ALL N: HNatInfinite. abs (sumhr(M,N,f)) @= #0)";
   1.102 +\     (ALL M: HNatInfinite. ALL N: HNatInfinite. abs (sumhr(M,N,f)) @= Numeral0)";
   1.103  by (auto_tac (claset(),
   1.104                simpset() addsimps [summable_NSsummable_iff RS sym,
   1.105                   summable_convergent_sumr_iff, convergent_NSconvergent_iff,
   1.106 @@ -287,7 +287,7 @@
   1.107  (*-------------------------------------------------------------------
   1.108           Terms of a convergent series tend to zero
   1.109   -------------------------------------------------------------------*)
   1.110 -Goalw [NSLIMSEQ_def] "NSsummable f ==> f ----NS> #0";
   1.111 +Goalw [NSLIMSEQ_def] "NSsummable f ==> f ----NS> Numeral0";
   1.112  by (auto_tac (claset(), simpset() addsimps [NSsummable_NSCauchy]));
   1.113  by (dtac bspec 1 THEN Auto_tac);
   1.114  by (dres_inst_tac [("x","N + 1hn")] bspec 1);
   1.115 @@ -297,7 +297,7 @@
   1.116  qed "NSsummable_NSLIMSEQ_zero";
   1.117  
   1.118  (* Easy to prove stsandard case now *)
   1.119 -Goal "summable f ==> f ----> #0";
   1.120 +Goal "summable f ==> f ----> Numeral0";
   1.121  by (auto_tac (claset(),
   1.122          simpset() addsimps [summable_NSsummable_iff,
   1.123                              LIMSEQ_NSLIMSEQ_iff, NSsummable_NSLIMSEQ_zero]));