src/HOL/Hyperreal/HSeries.ML
changeset 14378 69c4d5997669
parent 14371 c78c7da09519
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Hyperreal/HSeries.ML	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/HSeries.ML	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -5,6 +5,8 @@
     1.4                    for hyperreals
     1.5  *) 
     1.6  
     1.7 +val hypreal_of_nat_eq = thm"hypreal_of_nat_eq";
     1.8 +
     1.9  Goalw [sumhr_def]
    1.10       "sumhr(M,N,f) =  \
    1.11  \       Abs_hypreal(UN X:Rep_hypnat(M). UN Y: Rep_hypnat(N). \
    1.12 @@ -125,12 +127,11 @@
    1.13  qed "sumhr_hrabs";
    1.14  
    1.15  (* other general version also needed *)
    1.16 -Goalw [hypnat_of_nat_def]
    1.17 -     "(ALL r. m <= r & r < n --> f r = g r) --> \
    1.18 +Goal "(ALL r. m <= r & r < n --> f r = g r) --> \
    1.19  \     sumhr(hypnat_of_nat m, hypnat_of_nat n, f) = \
    1.20  \     sumhr(hypnat_of_nat m, hypnat_of_nat n, g)";
    1.21  by (Step_tac 1 THEN dtac sumr_fun_eq 1);
    1.22 -by (auto_tac (claset(), simpset() addsimps [sumhr]));
    1.23 +by (auto_tac (claset(), simpset() addsimps [sumhr, hypnat_of_nat_eq]));
    1.24  qed "sumhr_fun_hypnat_eq";
    1.25  
    1.26  Goalw [hypnat_zero_def,hypreal_of_real_def]
    1.27 @@ -163,12 +164,11 @@
    1.28  by (auto_tac (claset(), simpset() addsimps [sumhr, hypreal_minus,sumr_minus]));
    1.29  qed "sumhr_minus";
    1.30  
    1.31 -Goalw [hypnat_of_nat_def]
    1.32 -     "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))";
    1.33 +Goal "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))";
    1.34  by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
    1.35  by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
    1.36  by (auto_tac (claset(),
    1.37 -              simpset() addsimps [sumhr, hypnat_add,sumr_shift_bounds]));
    1.38 +              simpset() addsimps [sumhr, hypnat_add,sumr_shift_bounds, hypnat_of_nat_eq]));
    1.39  qed "sumhr_shift_bounds";
    1.40  
    1.41  (*------------------------------------------------------------------
    1.42 @@ -196,12 +196,11 @@
    1.43  qed "sumhr_minus_one_realpow_zero";
    1.44  Addsimps [sumhr_minus_one_realpow_zero];
    1.45  
    1.46 -Goalw [hypnat_of_nat_def,hypreal_of_real_def]
    1.47 -     "(ALL n. m <= Suc n --> f n = r) & m <= na \
    1.48 +Goal "(ALL n. m <= Suc n --> f n = r) & m <= na \
    1.49  \          ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = \
    1.50  \          (hypreal_of_nat (na - m) * hypreal_of_real r)";
    1.51  by (auto_tac (claset() addSDs [sumr_interval_const],
    1.52 -              simpset() addsimps [sumhr,hypreal_of_nat_def,
    1.53 +              simpset() addsimps [hypreal_of_real_def, sumhr,hypreal_of_nat_eq, hypnat_of_nat_eq,
    1.54                                    hypreal_of_real_def, hypreal_mult]));
    1.55  qed "sumhr_interval_const";
    1.56