more tidying, especially to remove real_of_posnat
authorpaulson
Thu Jan 04 10:23:01 2001 +0100 (2001-01-04)
changeset 107782c6605049646
parent 10777 a5a6255748c3
child 10779 b0d961105f46
more tidying, especially to remove real_of_posnat
src/HOL/Hyperreal/HRealAbs.ML
src/HOL/Hyperreal/HRealAbs.thy
src/HOL/Hyperreal/HSeries.ML
src/HOL/Hyperreal/HyperBin.ML
src/HOL/Hyperreal/HyperDef.ML
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/HyperNat.ML
src/HOL/Hyperreal/HyperNat.thy
src/HOL/Hyperreal/HyperOrd.ML
src/HOL/Hyperreal/HyperPow.ML
src/HOL/Hyperreal/HyperPow.thy
src/HOL/Hyperreal/Lim.ML
src/HOL/Hyperreal/NSA.ML
src/HOL/Hyperreal/NatStar.ML
src/HOL/Hyperreal/NatStar.thy
src/HOL/Hyperreal/SEQ.ML
src/HOL/Hyperreal/Series.ML
src/HOL/Hyperreal/Star.ML
src/HOL/Real/RComplete.ML
src/HOL/Real/RealArith0.ML
src/HOL/Real/RealDef.thy
src/HOL/Real/RealOrd.ML
src/HOL/Real/RealPow.ML
     1.1 --- a/src/HOL/Hyperreal/HRealAbs.ML	Thu Jan 04 10:22:33 2001 +0100
     1.2 +++ b/src/HOL/Hyperreal/HRealAbs.ML	Thu Jan 04 10:23:01 2001 +0100
     1.3 @@ -204,3 +204,52 @@
     1.4      "abs (hypreal_of_real r) = hypreal_of_real (abs r)";
     1.5  by (auto_tac (claset(), simpset() addsimps [hypreal_hrabs]));
     1.6  qed "hypreal_of_real_hrabs";
     1.7 +
     1.8 +
     1.9 +(*----------------------------------------------------------------------------
    1.10 +             Embedding of the naturals in the hyperreals
    1.11 + ----------------------------------------------------------------------------*)
    1.12 +
    1.13 +Goalw [hypreal_of_nat_def]
    1.14 +     "hypreal_of_nat n1 + hypreal_of_nat n2 = hypreal_of_nat (n1 + n2)";
    1.15 +by (simp_tac (simpset() addsimps [hypreal_of_real_add, real_of_nat_add]) 1);
    1.16 +qed "hypreal_of_nat_add";
    1.17 +
    1.18 +Goalw [hypreal_of_nat_def] 
    1.19 +      "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)";
    1.20 +by (auto_tac (claset() addIs [hypreal_add_less_mono1], simpset()));
    1.21 +qed "hypreal_of_nat_less_iff";
    1.22 +Addsimps [hypreal_of_nat_less_iff RS sym];
    1.23 +
    1.24 +(*------------------------------------------------------------*)
    1.25 +(* naturals embedded in hyperreals                            *)
    1.26 +(* is a hyperreal c.f. NS extension                           *)
    1.27 +(*------------------------------------------------------------*)
    1.28 +
    1.29 +Goalw [hypreal_of_nat_def, hypreal_of_real_def, real_of_nat_def] 
    1.30 +     "hypreal_of_nat  m = Abs_hypreal(hyprel^^{%n. real_of_nat m})";
    1.31 +by Auto_tac;
    1.32 +qed "hypreal_of_nat_iff";
    1.33 +
    1.34 +Goal "inj hypreal_of_nat";
    1.35 +by (simp_tac (simpset() addsimps [inj_on_def, hypreal_of_nat_def]) 1);
    1.36 +qed "inj_hypreal_of_nat";
    1.37 +
    1.38 +Goalw [hypreal_of_nat_def] 
    1.39 +     "hypreal_of_nat (Suc n) = hypreal_of_nat n + 1hr";
    1.40 +by (simp_tac (simpset() addsimps [real_of_nat_Suc]) 1);
    1.41 +qed "hypreal_of_nat_Suc";
    1.42 +
    1.43 +(*"neg" is used in rewrite rules for binary comparisons*)
    1.44 +Goal "hypreal_of_nat (number_of v :: nat) = \
    1.45 +\        (if neg (number_of v) then #0 \
    1.46 +\         else (number_of v :: hypreal))";
    1.47 +by (simp_tac (simpset() addsimps [hypreal_of_nat_def]) 1);
    1.48 +qed "hypreal_of_nat_number_of";
    1.49 +Addsimps [hypreal_of_nat_number_of];
    1.50 +
    1.51 +Goal "hypreal_of_nat 0 = #0";
    1.52 +by (simp_tac (simpset() delsimps [numeral_0_eq_0]
    1.53 +			addsimps [numeral_0_eq_0 RS sym]) 1);
    1.54 +qed "hypreal_of_nat_zero";
    1.55 +Addsimps [hypreal_of_nat_zero];
     2.1 --- a/src/HOL/Hyperreal/HRealAbs.thy	Thu Jan 04 10:22:33 2001 +0100
     2.2 +++ b/src/HOL/Hyperreal/HRealAbs.thy	Thu Jan 04 10:23:01 2001 +0100
     2.3 @@ -9,4 +9,9 @@
     2.4  defs
     2.5      hrabs_def "abs r  == if (0::hypreal) <=r then r else -r" 
     2.6  
     2.7 +constdefs
     2.8 +  
     2.9 +  hypreal_of_nat :: nat => hypreal                   
    2.10 +  "hypreal_of_nat n     == hypreal_of_real (real_of_nat n)"
    2.11 +
    2.12  end
    2.13 \ No newline at end of file
     3.1 --- a/src/HOL/Hyperreal/HSeries.ML	Thu Jan 04 10:22:33 2001 +0100
     3.2 +++ b/src/HOL/Hyperreal/HSeries.ML	Thu Jan 04 10:23:01 2001 +0100
     3.3 @@ -195,7 +195,7 @@
     3.4  by (simp_tac (HOL_ss addsimps
     3.5               [one_eq_numeral_1 RS sym, hypreal_one_def]) 1); 
     3.6  by (auto_tac (claset(),
     3.7 -              simpset() addsimps [sumhr, hypreal_diff, real_of_nat_def]));
     3.8 +              simpset() addsimps [sumhr, hypreal_diff, real_of_nat_Suc]));
     3.9  qed "sumhr_hypreal_omega_minus_one";
    3.10  
    3.11  Goalw [hypnat_zero_def, hypnat_omega_def]
    3.12 @@ -211,8 +211,8 @@
    3.13  \          ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = \
    3.14  \          (hypreal_of_nat (na - m) * hypreal_of_real r)";
    3.15  by (auto_tac (claset() addSDs [sumr_interval_const],
    3.16 -    simpset() addsimps [sumhr,hypreal_of_nat_real_of_nat,
    3.17 -              hypreal_of_real_def,hypreal_mult]));
    3.18 +              simpset() addsimps [sumhr,hypreal_of_nat_def,
    3.19 +                                  hypreal_of_real_def, hypreal_mult]));
    3.20  qed "sumhr_interval_const";
    3.21  
    3.22  Goalw [hypnat_zero_def]
     4.1 --- a/src/HOL/Hyperreal/HyperBin.ML	Thu Jan 04 10:22:33 2001 +0100
     4.2 +++ b/src/HOL/Hyperreal/HyperBin.ML	Thu Jan 04 10:23:01 2001 +0100
     4.3 @@ -172,15 +172,6 @@
     4.4  	  hypreal_add_number_of_diff1, hypreal_add_number_of_diff2]; 
     4.5  
     4.6  
     4.7 -(*"neg" is used in rewrite rules for binary comparisons*)
     4.8 -Goal "hypreal_of_nat (number_of v :: nat) = \
     4.9 -\        (if neg (number_of v) then #0 \
    4.10 -\         else (number_of v :: hypreal))";
    4.11 -by (simp_tac (simpset() addsimps [hypreal_of_nat_real_of_nat]) 1);
    4.12 -qed "hypreal_of_nat_number_of";
    4.13 -Addsimps [hypreal_of_nat_number_of];
    4.14 -
    4.15 -
    4.16  (**** Simprocs for numeric literals ****)
    4.17  
    4.18  (** Combining of literal coefficients in sums of products **)
     5.1 --- a/src/HOL/Hyperreal/HyperDef.ML	Thu Jan 04 10:22:33 2001 +0100
     5.2 +++ b/src/HOL/Hyperreal/HyperDef.ML	Thu Jan 04 10:23:01 2001 +0100
     5.3 @@ -1227,49 +1227,6 @@
     5.4  qed "hypreal_minus_eq_cancel";
     5.5  Addsimps [hypreal_minus_eq_cancel];
     5.6  
     5.7 -Goal "x < x + 1hr";
     5.8 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
     5.9 -by (auto_tac (claset(),
    5.10 -              simpset() addsimps [hypreal_add, hypreal_one_def,hypreal_less]));
    5.11 -qed "hypreal_less_self_add_one";
    5.12 -Addsimps [hypreal_less_self_add_one];
    5.13 -
    5.14 -(*??DELETE MOST OF THE FOLLOWING??*)
    5.15 -Goal "((x::hypreal) + x = y + y) = (x = y)";
    5.16 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    5.17 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
    5.18 -by (auto_tac (claset(),simpset() addsimps [hypreal_add]));
    5.19 -by (ALLGOALS(Ultra_tac));
    5.20 -qed "hypreal_add_self_cancel";
    5.21 -Addsimps [hypreal_add_self_cancel];
    5.22 -
    5.23 -Goal "(y = x + - y + x) = (y = (x::hypreal))";
    5.24 -by Auto_tac;
    5.25 -by (dres_inst_tac [("x1","y")] 
    5.26 -    (hypreal_add_right_cancel RS iffD2) 1);
    5.27 -by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
    5.28 -qed "hypreal_add_self_minus_cancel";
    5.29 -Addsimps [hypreal_add_self_minus_cancel];
    5.30 -
    5.31 -Goal "(y = x + (- y + x)) = (y = (x::hypreal))";
    5.32 -by (asm_full_simp_tac (simpset() addsimps 
    5.33 -         [hypreal_add_assoc RS sym])1);
    5.34 -qed "hypreal_add_self_minus_cancel2";
    5.35 -Addsimps [hypreal_add_self_minus_cancel2];
    5.36 -
    5.37 -(* of course, can prove this by "transfer" as well *)
    5.38 -Goal "z + -x = y + (y + (-x + -z)) = (y = (z::hypreal))";
    5.39 -by Auto_tac;
    5.40 -by (dres_inst_tac [("x1","z")] 
    5.41 -    (hypreal_add_right_cancel RS iffD2) 1);
    5.42 -by (asm_full_simp_tac (simpset() addsimps 
    5.43 -    [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac
    5.44 -    delsimps [hypreal_minus_add_distrib]) 1);
    5.45 -by (asm_full_simp_tac (simpset() addsimps 
    5.46 -     [hypreal_add_assoc RS sym,hypreal_add_right_cancel]) 1);
    5.47 -qed "hypreal_add_self_minus_cancel3";
    5.48 -Addsimps [hypreal_add_self_minus_cancel3];
    5.49 -
    5.50  Goalw [hypreal_diff_def] "(x<y) = (x-y < (0::hypreal))";
    5.51  by (rtac hypreal_less_minus_iff2 1);
    5.52  qed "hypreal_less_eq_diff";
     6.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Thu Jan 04 10:22:33 2001 +0100
     6.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Jan 04 10:23:01 2001 +0100
     6.3 @@ -44,11 +44,11 @@
     6.4  
     6.5    (* an infinite number = [<1,2,3,...>] *)
     6.6    omega_def
     6.7 -  "whr == Abs_hypreal(hyprel^^{%n::nat. real_of_posnat n})"
     6.8 +  "whr == Abs_hypreal(hyprel^^{%n::nat. real_of_nat (Suc n)})"
     6.9      
    6.10    (* an infinitesimal number = [<1,1/2,1/3,...>] *)
    6.11    epsilon_def
    6.12 -  "ehr == Abs_hypreal(hyprel^^{%n::nat. inverse (real_of_posnat n)})"
    6.13 +  "ehr == Abs_hypreal(hyprel^^{%n::nat. inverse (real_of_nat (Suc n))})"
    6.14  
    6.15    hypreal_minus_def
    6.16    "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel^^{%n::nat. - (X n)})"
    6.17 @@ -67,14 +67,6 @@
    6.18  
    6.19    hypreal_of_real  :: real => hypreal                 
    6.20    "hypreal_of_real r         == Abs_hypreal(hyprel^^{%n::nat. r})"
    6.21 -  
    6.22 -  (* n::nat --> (n+1)::hypreal *)
    6.23 -  hypreal_of_posnat :: nat => hypreal                
    6.24 -  "hypreal_of_posnat n  == (hypreal_of_real(real_of_preal
    6.25 -                            (preal_of_prat(prat_of_pnat(pnat_of_nat n)))))"
    6.26 -
    6.27 -  hypreal_of_nat :: nat => hypreal                   
    6.28 -  "hypreal_of_nat n      == hypreal_of_posnat n + -1hr"
    6.29  
    6.30  defs 
    6.31  
     7.1 --- a/src/HOL/Hyperreal/HyperNat.ML	Thu Jan 04 10:22:33 2001 +0100
     7.2 +++ b/src/HOL/Hyperreal/HyperNat.ML	Thu Jan 04 10:23:01 2001 +0100
     7.3 @@ -41,7 +41,7 @@
     7.4  AddSEs [hypnatrelE];
     7.5  
     7.6  Goalw [hypnatrel_def] "(x,x): hypnatrel";
     7.7 -by (Auto_tac);
     7.8 +by Auto_tac;
     7.9  qed "hypnatrel_refl";
    7.10  
    7.11  Goalw [hypnatrel_def] "(x,y): hypnatrel --> (y,x):hypnatrel";
    7.12 @@ -50,7 +50,7 @@
    7.13  
    7.14  Goalw [hypnatrel_def]
    7.15       "(x,y): hypnatrel --> (y,z):hypnatrel --> (x,z):hypnatrel";
    7.16 -by (Auto_tac);
    7.17 +by Auto_tac;
    7.18  by (Fuf_tac 1);
    7.19  qed_spec_mp "hypnatrel_trans";
    7.20  
    7.21 @@ -87,7 +87,7 @@
    7.22  
    7.23  Goalw [hypnatrel_def] "x: hypnatrel ^^ {x}";
    7.24  by (Step_tac 1);
    7.25 -by (Auto_tac);
    7.26 +by Auto_tac;
    7.27  qed "lemma_hypnatrel_refl";
    7.28  
    7.29  Addsimps [lemma_hypnatrel_refl];
    7.30 @@ -100,7 +100,7 @@
    7.31  
    7.32  Goal "Rep_hypnat x ~= {}";
    7.33  by (cut_inst_tac [("x","x")] Rep_hypnat 1);
    7.34 -by (Auto_tac);
    7.35 +by Auto_tac;
    7.36  qed "Rep_hypnat_nonempty";
    7.37  
    7.38  Addsimps [Rep_hypnat_nonempty];
    7.39 @@ -117,7 +117,7 @@
    7.40  by (rtac equiv_hypnatrel 1);
    7.41  by (Fast_tac 1);
    7.42  by (rtac ccontr 1 THEN rotate_tac 1 1);
    7.43 -by (Auto_tac);
    7.44 +by Auto_tac;
    7.45  qed "inj_hypnat_of_nat";
    7.46  
    7.47  val [prem] = Goal
    7.48 @@ -376,7 +376,7 @@
    7.49  
    7.50  (*** (hypnat) one and zero are distinct ***)
    7.51  Goalw [hypnat_zero_def,hypnat_one_def] "(0::hypnat) ~= 1hn";
    7.52 -by (Auto_tac);
    7.53 +by Auto_tac;
    7.54  qed "hypnat_zero_not_eq_one";
    7.55  Addsimps [hypnat_zero_not_eq_one];
    7.56  Addsimps [hypnat_zero_not_eq_one RS not_sym];
    7.57 @@ -404,7 +404,7 @@
    7.58  qed "hypnat_less_iff";
    7.59  
    7.60  Goalw [hypnat_less_def]
    7.61 - "!!P. [| {n. X n < Y n} : FreeUltrafilterNat; \
    7.62 + "[| {n. X n < Y n} : FreeUltrafilterNat; \
    7.63  \         X : Rep_hypnat(P); \
    7.64  \         Y : Rep_hypnat(Q) |] ==> P < (Q::hypnat)";
    7.65  by (Fast_tac 1);
    7.66 @@ -416,11 +416,11 @@
    7.67  \         !!X. X : Rep_hypnat(R1) ==> P; \ 
    7.68  \         !!Y. Y : Rep_hypnat(R2) ==> P |] \
    7.69  \     ==> P";
    7.70 -by (Auto_tac);
    7.71 +by Auto_tac;
    7.72  qed "hypnat_lessE";
    7.73  
    7.74  Goalw [hypnat_less_def]
    7.75 - "!!R1. R1 < (R2::hypnat) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \
    7.76 + "R1 < (R2::hypnat) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \
    7.77  \                                  X : Rep_hypnat(R1) & \
    7.78  \                                  Y : Rep_hypnat(R2))";
    7.79  by (Fast_tac 1);
    7.80 @@ -437,7 +437,7 @@
    7.81  
    7.82  Goalw [hypnat_less_def,hypnat_zero_def] "~ n<(0::hypnat)";
    7.83  by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
    7.84 -by (Auto_tac);
    7.85 +by Auto_tac;
    7.86  by (Fuf_empty_tac 1);
    7.87  qed "hypnat_not_less0";
    7.88  AddIffs [hypnat_not_less0];
    7.89 @@ -460,9 +460,9 @@
    7.90  by (res_inst_tac [("z","R3")] eq_Abs_hypnat 1);
    7.91  by (auto_tac (claset(),simpset() addsimps [hypnat_less_def]));
    7.92  by (res_inst_tac [("x","X")] exI 1);
    7.93 -by (Auto_tac);
    7.94 +by Auto_tac;
    7.95  by (res_inst_tac [("x","Ya")] exI 1);
    7.96 -by (Auto_tac);
    7.97 +by Auto_tac;
    7.98  by (Fuf_tac 1);
    7.99  qed "hypnat_less_trans";
   7.100  
   7.101 @@ -530,12 +530,12 @@
   7.102  Goalw [hypnatrel_def] "EX x. x: hypnatrel ^^ {%n. 0}";
   7.103  by (res_inst_tac [("x","%n. 0")] exI 1);
   7.104  by (Step_tac 1);
   7.105 -by (Auto_tac);
   7.106 +by Auto_tac;
   7.107  qed "lemma_hypnatrel_0_mem";
   7.108  
   7.109  (* linearity is actually proved further down! *)
   7.110 -Goalw [hypnat_zero_def,
   7.111 -       hypnat_less_def]"(0::hypnat) <  x | x = 0 | x < 0";
   7.112 +Goalw [hypnat_zero_def, hypnat_less_def]
   7.113 +     "(0::hypnat) <  x | x = 0 | x < 0";
   7.114  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   7.115  by (Auto_tac );
   7.116  by (REPEAT(Step_tac 1));
   7.117 @@ -543,29 +543,28 @@
   7.118  by (Fuf_tac 1);
   7.119  qed "hypnat_trichotomy";
   7.120  
   7.121 -Goal "!!x. [| (0::hypnat) < x ==> P; \
   7.122 -\                 x = 0 ==> P; \
   7.123 -\                 x < 0 ==> P |] ==> P";
   7.124 +Goal "!!P. [| (0::hypnat) < x ==> P; \
   7.125 +\             x = 0 ==> P; \
   7.126 +\             x < 0 ==> P |] ==> P";
   7.127  by (cut_inst_tac [("x","x")] hypnat_trichotomy 1);
   7.128 -by (Auto_tac);
   7.129 +by Auto_tac;
   7.130  qed "hypnat_trichotomyE";
   7.131  
   7.132 -(*------------------------------------------------------------------------------
   7.133 +(*----------------------------------------------------------------------------
   7.134              More properties of <
   7.135 - ------------------------------------------------------------------------------*)
   7.136 + ----------------------------------------------------------------------------*)
   7.137  Goal "!!(A::hypnat). A < B ==> A + C < B + C";
   7.138  by (res_inst_tac [("z","A")] eq_Abs_hypnat 1);
   7.139  by (res_inst_tac [("z","B")] eq_Abs_hypnat 1);
   7.140  by (res_inst_tac [("z","C")] eq_Abs_hypnat 1);
   7.141 -by (auto_tac (claset(),simpset() addsimps 
   7.142 -    [hypnat_less_def,hypnat_add]));
   7.143 +by (auto_tac (claset(), simpset() addsimps [hypnat_less_def,hypnat_add]));
   7.144  by (REPEAT(Step_tac 1));
   7.145  by (Fuf_tac 1);
   7.146  qed "hypnat_add_less_mono1";
   7.147  
   7.148  Goal "!!(A::hypnat). A < B ==> C + A < C + B";
   7.149  by (auto_tac (claset() addIs [hypnat_add_less_mono1],
   7.150 -    simpset() addsimps [hypnat_add_commute]));
   7.151 +              simpset() addsimps [hypnat_add_commute]));
   7.152  qed "hypnat_add_less_mono2";
   7.153  
   7.154  Goal "!!k l::hypnat. [|i<j;  k<l |] ==> i + k < j + l";
   7.155 @@ -598,16 +597,27 @@
   7.156  by (Fuf_tac 1);
   7.157  qed "hypnat_linear";
   7.158  
   7.159 -Goal
   7.160 -    "!!(x::hypnat). [| x < y ==> P;  x = y ==> P; \
   7.161 -\          y < x ==> P |] ==> P";
   7.162 +Goal "!!(x::hypnat). [| x < y ==> P;  x = y ==> P; \
   7.163 +\                       y < x ==> P |] ==> P";
   7.164  by (cut_inst_tac [("x","x"),("y","y")] hypnat_linear 1);
   7.165 -by (Auto_tac);
   7.166 +by Auto_tac;
   7.167  qed "hypnat_linear_less2";
   7.168  
   7.169 -(*------------------------------------------------------------------------------
   7.170 +Goal "((w::hypnat) ~= z) = (w<z | z<w)";
   7.171 +by (cut_facts_tac [hypnat_linear] 1);
   7.172 +by Auto_tac;
   7.173 +qed "hypnat_neq_iff";
   7.174 +
   7.175 +(* Axiom 'order_less_le' of class 'order': *)
   7.176 +Goal "(w::hypnat) < z = (w <= z & w ~= z)";
   7.177 +by (simp_tac (simpset() addsimps [hypnat_le_def, hypnat_neq_iff]) 1);
   7.178 +by (blast_tac (claset() addIs [hypnat_less_asym]) 1);
   7.179 +qed "hypnat_less_le";
   7.180 +
   7.181 +(*----------------------------------------------------------------------------
   7.182                              Properties of <=
   7.183 - ------------------------------------------------------------------------------*)
   7.184 + ----------------------------------------------------------------------------*)
   7.185 +
   7.186  (*------ hypnat le iff nat le a.e ------*)
   7.187  Goalw [hypnat_le_def,le_def]
   7.188        "(Abs_hypnat(hypnatrel^^{%n. X n}) <= \
   7.189 @@ -620,25 +630,8 @@
   7.190  
   7.191  (*---------------------------------------------------------*)
   7.192  (*---------------------------------------------------------*)
   7.193 -Goalw [hypnat_le_def] "!!w. ~(w < z) ==> z <= (w::hypnat)";
   7.194 -by (assume_tac 1);
   7.195 -qed "hypnat_leI";
   7.196  
   7.197 -Goalw [hypnat_le_def] "!!w. z<=w ==> ~(w<(z::hypnat))";
   7.198 -by (assume_tac 1);
   7.199 -qed "hypnat_leD";
   7.200 -
   7.201 -val hypnat_leE = make_elim hypnat_leD;
   7.202 -
   7.203 -Goal "!!w. (~(w < z)) = (z <= (w::hypnat))";
   7.204 -by (fast_tac (claset() addSIs [hypnat_leI,hypnat_leD]) 1);
   7.205 -qed "hypnat_less_le_iff";
   7.206 -
   7.207 -Goalw [hypnat_le_def] "!!z. ~ z <= w ==> w<(z::hypnat)";
   7.208 -by (Fast_tac 1);
   7.209 -qed "not_hypnat_leE";
   7.210 -
   7.211 -Goalw [hypnat_le_def] "!!z. z < w ==> z <= (w::hypnat)";
   7.212 +Goalw [hypnat_le_def] "z < w ==> z <= (w::hypnat)";
   7.213  by (fast_tac (claset() addEs [hypnat_less_asym]) 1);
   7.214  qed "hypnat_less_imp_le";
   7.215  
   7.216 @@ -647,59 +640,53 @@
   7.217  by (fast_tac (claset() addEs [hypnat_less_irrefl,hypnat_less_asym]) 1);
   7.218  qed "hypnat_le_imp_less_or_eq";
   7.219  
   7.220 -Goalw [hypnat_le_def] "!!z. z<w | z=w ==> z <=(w::hypnat)";
   7.221 +Goalw [hypnat_le_def] "z<w | z=w ==> z <=(w::hypnat)";
   7.222  by (cut_facts_tac [hypnat_linear] 1);
   7.223 -by (fast_tac (claset() addEs [hypnat_less_irrefl,hypnat_less_asym]) 1);
   7.224 +by (blast_tac (claset() addDs [hypnat_less_irrefl,hypnat_less_asym]) 1);
   7.225  qed "hypnat_less_or_eq_imp_le";
   7.226  
   7.227  Goal "(x <= (y::hypnat)) = (x < y | x=y)";
   7.228 -by (REPEAT(ares_tac [iffI, hypnat_less_or_eq_imp_le, hypnat_le_imp_less_or_eq] 1));
   7.229 -qed "hypnat_le_eq_less_or_eq";
   7.230 +by (REPEAT(ares_tac [iffI, hypnat_less_or_eq_imp_le, 
   7.231 +                     hypnat_le_imp_less_or_eq] 1));
   7.232 +qed "hypnat_le_less";
   7.233 +
   7.234 +(* Axiom 'linorder_linear' of class 'linorder': *)
   7.235 +Goal "(z::hypnat) <= w | w <= z";
   7.236 +by (simp_tac (simpset() addsimps [hypnat_le_less]) 1);
   7.237 +by (cut_facts_tac [hypnat_linear] 1);
   7.238 +by (Blast_tac 1);
   7.239 +qed "hypnat_le_linear";
   7.240  
   7.241  Goal "w <= (w::hypnat)";
   7.242 -by (simp_tac (simpset() addsimps [hypnat_le_eq_less_or_eq]) 1);
   7.243 +by (simp_tac (simpset() addsimps [hypnat_le_less]) 1);
   7.244  qed "hypnat_le_refl";
   7.245  Addsimps [hypnat_le_refl];
   7.246  
   7.247 -val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::hypnat)";
   7.248 -by (dtac hypnat_le_imp_less_or_eq 1);
   7.249 -by (fast_tac (claset() addIs [hypnat_less_trans]) 1);
   7.250 -qed "hypnat_le_less_trans";
   7.251 -
   7.252 -Goal "!! (i::hypnat). [| i < j; j <= k |] ==> i < k";
   7.253 -by (dtac hypnat_le_imp_less_or_eq 1);
   7.254 -by (fast_tac (claset() addIs [hypnat_less_trans]) 1);
   7.255 -qed "hypnat_less_le_trans";
   7.256 -
   7.257 -Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::hypnat)";
   7.258 +Goal "[| i <= j; j <= k |] ==> i <= (k::hypnat)";
   7.259  by (EVERY1 [dtac hypnat_le_imp_less_or_eq, dtac hypnat_le_imp_less_or_eq,
   7.260 -            rtac hypnat_less_or_eq_imp_le, fast_tac (claset() addIs [hypnat_less_trans])]);
   7.261 +            rtac hypnat_less_or_eq_imp_le, 
   7.262 +            fast_tac (claset() addIs [hypnat_less_trans])]);
   7.263  qed "hypnat_le_trans";
   7.264  
   7.265 -Goal "!!z. [| z <= w; w <= z |] ==> z = (w::hypnat)";
   7.266 +Goal "[| z <= w; w <= z |] ==> z = (w::hypnat)";
   7.267  by (EVERY1 [dtac hypnat_le_imp_less_or_eq, dtac hypnat_le_imp_less_or_eq,
   7.268              fast_tac (claset() addEs [hypnat_less_irrefl,hypnat_less_asym])]);
   7.269  qed "hypnat_le_anti_sym";
   7.270  
   7.271 -Goal "!!x. [| ~ y < x; y ~= x |] ==> x < (y::hypnat)";
   7.272 -by (rtac not_hypnat_leE 1);
   7.273 -by (fast_tac (claset() addDs [hypnat_le_imp_less_or_eq]) 1);
   7.274 -qed "not_less_not_eq_hypnat_less";
   7.275 -
   7.276 -Goal "!!x. [| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x * y";
   7.277 +Goal "[| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x * y";
   7.278  by (REPEAT(dtac hypnat_le_imp_less_or_eq 1));
   7.279 -by (auto_tac (claset() addIs [hypnat_mult_order,
   7.280 -    hypnat_less_imp_le],simpset() addsimps [hypnat_le_refl]));
   7.281 +by (auto_tac (claset() addIs [hypnat_mult_order, hypnat_less_imp_le],
   7.282 +              simpset() addsimps [hypnat_le_refl]));
   7.283  qed "hypnat_le_mult_order";
   7.284  
   7.285  Goalw [hypnat_one_def,hypnat_zero_def,hypnat_less_def] 
   7.286        "(0::hypnat) < 1hn";
   7.287  by (res_inst_tac [("x","%n. 0")] exI 1);
   7.288  by (res_inst_tac [("x","%n. 1")] exI 1);
   7.289 -by (Auto_tac);
   7.290 +by Auto_tac;
   7.291  qed "hypnat_zero_less_one";
   7.292  
   7.293 -Goal "!!x. [| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x + y";
   7.294 +Goal "[| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x + y";
   7.295  by (REPEAT(dtac hypnat_le_imp_less_or_eq 1));
   7.296  by (auto_tac (claset() addIs [hypnat_add_order,
   7.297      hypnat_less_imp_le],simpset() addsimps [hypnat_le_refl]));
   7.298 @@ -752,7 +739,7 @@
   7.299  Goal "(x::hypnat) < x + 1hn";
   7.300  by (cut_facts_tac [hypnat_zero_less_one 
   7.301           RS hypnat_add_less_mono2] 1);
   7.302 -by (Auto_tac);
   7.303 +by Auto_tac;
   7.304  qed "hypnat_add_one_self_less";
   7.305  Addsimps [hypnat_add_one_self_less];
   7.306  
   7.307 @@ -816,7 +803,7 @@
   7.308  
   7.309  Goalw [hypnat_le_def,le_def] 
   7.310        "(z1 <= z2) = (hypnat_of_nat z1 <= hypnat_of_nat z2)";
   7.311 -by (Auto_tac);
   7.312 +by Auto_tac;
   7.313  qed "hypnat_of_nat_le_iff";
   7.314  
   7.315  Goalw [hypnat_of_nat_def,hypnat_one_def] "hypnat_of_nat  1 = 1hn";
   7.316 @@ -837,8 +824,8 @@
   7.317  by (full_simp_tac (simpset() addsimps [hypnat_of_nat_zero_iff]) 1);
   7.318  qed "hypnat_of_nat_not_zero_iff";
   7.319  
   7.320 -goalw HyperNat.thy [hypnat_of_nat_def,hypnat_one_def]
   7.321 -      "hypnat_of_nat (Suc n) = hypnat_of_nat n + 1hn";
   7.322 +Goalw [hypnat_of_nat_def,hypnat_one_def]
   7.323 +     "hypnat_of_nat (Suc n) = hypnat_of_nat n + 1hn";
   7.324  by (auto_tac (claset(),simpset() addsimps [hypnat_add]));
   7.325  qed "hypnat_of_nat_Suc";
   7.326  
   7.327 @@ -847,7 +834,7 @@
   7.328   ---------------------------------------------------------------------------------*)
   7.329  
   7.330  Goal "hypnatrel^^{%n::nat. n} : hypnat";
   7.331 -by (Auto_tac);
   7.332 +by Auto_tac;
   7.333  qed "hypnat_omega";
   7.334  
   7.335  Goalw [hypnat_omega_def] "Rep_hypnat(whn) : hypnat";
   7.336 @@ -867,111 +854,110 @@
   7.337  
   7.338  Goal "hypnat_of_nat x ~= whn";
   7.339  by (cut_facts_tac [not_ex_hypnat_of_nat_eq_omega] 1);
   7.340 -by (Auto_tac);
   7.341 +by Auto_tac;
   7.342  qed "hypnat_of_nat_not_eq_omega";
   7.343  Addsimps [hypnat_of_nat_not_eq_omega RS not_sym];
   7.344  
   7.345  (*-----------------------------------------------------------
   7.346 -    Properties of the set SHNat of embedded natural numbers
   7.347 +    Properties of the set SNat of embedded natural numbers
   7.348                (cf. set SReal in NSA.thy/NSA.ML)
   7.349   ----------------------------------------------------------*)
   7.350  
   7.351 -(* Infinite hypernatural not in embedded SHNat *)
   7.352 -Goalw [SHNat_def] "whn ~: SHNat";
   7.353 -by (Auto_tac);
   7.354 +(* Infinite hypernatural not in embedded SNat *)
   7.355 +Goalw [SHNat_def] "whn ~: SNat";
   7.356 +by Auto_tac;
   7.357  qed "SHNAT_omega_not_mem";
   7.358  Addsimps [SHNAT_omega_not_mem];
   7.359  
   7.360  (*-----------------------------------------------------------------------
   7.361 -     Closure laws for members of (embedded) set standard naturals SHNat
   7.362 +     Closure laws for members of (embedded) set standard naturals SNat
   7.363   -----------------------------------------------------------------------*)
   7.364  Goalw [SHNat_def] 
   7.365 -      "!!x. [| x: SHNat; y: SHNat |] ==> x + y: SHNat";
   7.366 +     "!!x::hypnat. [| x: SNat; y: SNat |] ==> x + y: SNat";
   7.367  by (Step_tac 1);
   7.368  by (res_inst_tac [("x","N + Na")] exI 1);
   7.369  by (simp_tac (simpset() addsimps [hypnat_of_nat_add]) 1);
   7.370  qed "SHNat_add";
   7.371  
   7.372  Goalw [SHNat_def] 
   7.373 -      "!!x. [| x: SHNat; y: SHNat |] ==> x - y: SHNat";
   7.374 +     "!!x::hypnat. [| x: SNat; y: SNat |] ==> x - y: SNat";
   7.375  by (Step_tac 1);
   7.376  by (res_inst_tac [("x","N - Na")] exI 1);
   7.377  by (simp_tac (simpset() addsimps [hypnat_of_nat_minus]) 1);
   7.378  qed "SHNat_minus";
   7.379  
   7.380  Goalw [SHNat_def] 
   7.381 -      "!!x. [| x: SHNat; y: SHNat |] ==> x * y: SHNat";
   7.382 +     "!!x::hypnat. [| x: SNat; y: SNat |] ==> x * y: SNat";
   7.383  by (Step_tac 1);
   7.384  by (res_inst_tac [("x","N * Na")] exI 1);
   7.385  by (simp_tac (simpset() addsimps [hypnat_of_nat_mult]) 1);
   7.386  qed "SHNat_mult";
   7.387  
   7.388 -Goal "!!x. [| x + y : SHNat; y: SHNat |] ==> x: SHNat";
   7.389 +Goal"!!x::hypnat. [| x + y : SNat; y: SNat |] ==> x: SNat";
   7.390  by (dres_inst_tac [("x","x+y")] SHNat_minus 1);
   7.391 -by (Auto_tac);
   7.392 +by Auto_tac;
   7.393  qed "SHNat_add_cancel";
   7.394  
   7.395 -Goalw [SHNat_def] "hypnat_of_nat x : SHNat";
   7.396 +Goalw [SHNat_def] "hypnat_of_nat x : SNat";
   7.397  by (Blast_tac 1);
   7.398  qed "SHNat_hypnat_of_nat";
   7.399  Addsimps [SHNat_hypnat_of_nat];
   7.400  
   7.401 -Goal "hypnat_of_nat 1 : SHNat";
   7.402 +Goal "hypnat_of_nat 1 : SNat";
   7.403  by (Simp_tac 1);
   7.404  qed "SHNat_hypnat_of_nat_one";
   7.405  
   7.406 -Goal "hypnat_of_nat 0 : SHNat";
   7.407 +Goal "hypnat_of_nat 0 : SNat";
   7.408  by (Simp_tac 1);
   7.409  qed "SHNat_hypnat_of_nat_zero";
   7.410  
   7.411 -Goal "1hn : SHNat";
   7.412 +Goal "1hn : SNat";
   7.413  by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_one,
   7.414      hypnat_of_nat_one RS sym]) 1);
   7.415  qed "SHNat_one";
   7.416  
   7.417 -Goal "0 : SHNat";
   7.418 +Goal "(0::hypnat) : SNat";
   7.419  by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_zero,
   7.420 -    hypnat_of_nat_zero RS sym]) 1);
   7.421 +                                  hypnat_of_nat_zero RS sym]) 1);
   7.422  qed "SHNat_zero";
   7.423  
   7.424  Addsimps [SHNat_hypnat_of_nat_one,SHNat_hypnat_of_nat_zero,
   7.425            SHNat_one,SHNat_zero];
   7.426  
   7.427 -Goal "1hn + 1hn : SHNat";
   7.428 +Goal "1hn + 1hn : SNat";
   7.429  by (rtac ([SHNat_one,SHNat_one] MRS SHNat_add) 1);
   7.430  qed "SHNat_two";
   7.431  
   7.432 -Goalw [SHNat_def] "{x. hypnat_of_nat x : SHNat} = (UNIV::nat set)";
   7.433 -by (Auto_tac);
   7.434 +Goalw [SHNat_def] "{x. hypnat_of_nat x : SNat} = (UNIV::nat set)";
   7.435 +by Auto_tac;
   7.436  qed "SHNat_UNIV_nat";
   7.437  
   7.438 -Goalw [SHNat_def] "(x: SHNat) = (EX y. x = hypnat_of_nat  y)";
   7.439 -by (Auto_tac);
   7.440 +Goalw [SHNat_def] "(x: SNat) = (EX y. x = hypnat_of_nat  y)";
   7.441 +by Auto_tac;
   7.442  qed "SHNat_iff";
   7.443  
   7.444 -Goalw [SHNat_def] "hypnat_of_nat ``(UNIV::nat set) = SHNat";
   7.445 -by (Auto_tac);
   7.446 +Goalw [SHNat_def] "hypnat_of_nat ``(UNIV::nat set) = SNat";
   7.447 +by Auto_tac;
   7.448  qed "hypnat_of_nat_image";
   7.449  
   7.450 -Goalw [SHNat_def] "inv hypnat_of_nat ``SHNat = (UNIV::nat set)";
   7.451 -by (Auto_tac);
   7.452 +Goalw [SHNat_def] "inv hypnat_of_nat ``SNat = (UNIV::nat set)";
   7.453 +by Auto_tac;
   7.454  by (rtac (inj_hypnat_of_nat RS inv_f_f RS subst) 1);
   7.455  by (Blast_tac 1);
   7.456  qed "inv_hypnat_of_nat_image";
   7.457  
   7.458  Goalw [SHNat_def] 
   7.459 -      "!!P. [| EX x. x: P; P <= SHNat |] ==> \
   7.460 -\           EX Q. P = hypnat_of_nat `` Q";
   7.461 +     "[| EX x. x: P; P <= SNat |] ==> EX Q. P = hypnat_of_nat `` Q";
   7.462  by (Best_tac 1); 
   7.463  qed "SHNat_hypnat_of_nat_image";
   7.464  
   7.465  Goalw [SHNat_def] 
   7.466 -      "SHNat = hypnat_of_nat `` (UNIV::nat set)";
   7.467 -by (Auto_tac);
   7.468 +      "SNat = hypnat_of_nat `` (UNIV::nat set)";
   7.469 +by Auto_tac;
   7.470  qed "SHNat_hypnat_of_nat_iff";
   7.471  
   7.472 -Goalw [SHNat_def] "SHNat <= (UNIV::hypnat set)";
   7.473 -by (Auto_tac);
   7.474 +Goalw [SHNat_def] "SNat <= (UNIV::hypnat set)";
   7.475 +by Auto_tac;
   7.476  qed "SHNat_subset_UNIV";
   7.477  
   7.478  Goal "{n. n <= Suc m} = {n. n <= m} Un {n. n = Suc m}";
   7.479 @@ -990,9 +976,8 @@
   7.480  qed "lemma_unbounded_set";
   7.481  Addsimps [lemma_unbounded_set];
   7.482  
   7.483 -Goalw [SHNat_def,hypnat_of_nat_def,
   7.484 -           hypnat_less_def,hypnat_omega_def] 
   7.485 -           "ALL n: SHNat. n < whn";
   7.486 +Goalw [SHNat_def,hypnat_of_nat_def, hypnat_less_def,hypnat_omega_def] 
   7.487 +     "ALL n: SNat. n < whn";
   7.488  by (Clarify_tac 1);
   7.489  by (auto_tac (claset() addSIs [exI],simpset()));
   7.490  qed "hypnat_omega_gt_SHNat";
   7.491 @@ -1000,7 +985,7 @@
   7.492  Goal "hypnat_of_nat n < whn";
   7.493  by (cut_facts_tac [hypnat_omega_gt_SHNat] 1);
   7.494  by (dres_inst_tac [("x","hypnat_of_nat n")] bspec 1);
   7.495 -by (Auto_tac);
   7.496 +by Auto_tac;
   7.497  qed "hypnat_of_nat_less_whn";
   7.498  Addsimps [hypnat_of_nat_less_whn];
   7.499  
   7.500 @@ -1011,13 +996,13 @@
   7.501  
   7.502  Goal "0 < whn";
   7.503  by (rtac (hypnat_omega_gt_SHNat RS ballE) 1);
   7.504 -by (Auto_tac);
   7.505 +by Auto_tac;
   7.506  qed "hypnat_zero_less_hypnat_omega";
   7.507  Addsimps [hypnat_zero_less_hypnat_omega];
   7.508  
   7.509  Goal "1hn < whn";
   7.510  by (rtac (hypnat_omega_gt_SHNat RS ballE) 1);
   7.511 -by (Auto_tac);
   7.512 +by Auto_tac;
   7.513  qed "hypnat_one_less_hypnat_omega";
   7.514  Addsimps [hypnat_one_less_hypnat_omega];
   7.515  
   7.516 @@ -1025,43 +1010,43 @@
   7.517       Theorems about infinite hypernatural numbers -- HNatInfinite
   7.518   -------------------------------------------------------------------------*)
   7.519  Goalw [HNatInfinite_def,SHNat_def] "whn : HNatInfinite";
   7.520 -by (Auto_tac);
   7.521 +by Auto_tac;
   7.522  qed "HNatInfinite_whn";
   7.523  Addsimps [HNatInfinite_whn];
   7.524  
   7.525 -Goalw [HNatInfinite_def] "!!x. x: SHNat ==> x ~: HNatInfinite";
   7.526 +Goalw [HNatInfinite_def] "x: SNat ==> x ~: HNatInfinite";
   7.527  by (Simp_tac 1);
   7.528  qed "SHNat_not_HNatInfinite";
   7.529  
   7.530 -Goalw [HNatInfinite_def] "!!x. x ~: HNatInfinite ==> x: SHNat";
   7.531 +Goalw [HNatInfinite_def] "x ~: HNatInfinite ==> x: SNat";
   7.532  by (Asm_full_simp_tac 1);
   7.533  qed "not_HNatInfinite_SHNat";
   7.534  
   7.535 -Goalw [HNatInfinite_def] "!!x. x ~: SHNat ==> x: HNatInfinite";
   7.536 +Goalw [HNatInfinite_def] "x ~: SNat ==> x: HNatInfinite";
   7.537  by (Simp_tac 1);
   7.538  qed "not_SHNat_HNatInfinite";
   7.539  
   7.540 -Goalw [HNatInfinite_def] "!!x. x: HNatInfinite ==> x ~: SHNat";
   7.541 +Goalw [HNatInfinite_def] "x: HNatInfinite ==> x ~: SNat";
   7.542  by (Asm_full_simp_tac 1);
   7.543  qed "HNatInfinite_not_SHNat";
   7.544  
   7.545 -Goal "(x: SHNat) = (x ~: HNatInfinite)";
   7.546 +Goal "(x: SNat) = (x ~: HNatInfinite)";
   7.547  by (blast_tac (claset() addSIs [SHNat_not_HNatInfinite,
   7.548      not_HNatInfinite_SHNat]) 1);
   7.549  qed "SHNat_not_HNatInfinite_iff";
   7.550  
   7.551 -Goal "(x ~: SHNat) = (x: HNatInfinite)";
   7.552 +Goal "(x ~: SNat) = (x: HNatInfinite)";
   7.553  by (blast_tac (claset() addSIs [not_SHNat_HNatInfinite,
   7.554      HNatInfinite_not_SHNat]) 1);
   7.555  qed "not_SHNat_HNatInfinite_iff";
   7.556  
   7.557 -Goal "x : SHNat | x : HNatInfinite";
   7.558 +Goal "x : SNat | x : HNatInfinite";
   7.559  by (simp_tac (simpset() addsimps [SHNat_not_HNatInfinite_iff]) 1);
   7.560  qed "SHNat_HNatInfinite_disj";
   7.561  
   7.562  (*-------------------------------------------------------------------
   7.563     Proof of alternative definition for set of Infinite hypernatural 
   7.564 -   numbers --- HNatInfinite = {N. ALL n: SHNat. n < N}
   7.565 +   numbers --- HNatInfinite = {N. ALL n: SNat. n < N}
   7.566   -------------------------------------------------------------------*)
   7.567  Goal "!!N (xa::nat=>nat). \
   7.568  \         (ALL N. {n. xa n ~= N} : FreeUltrafilterNat) ==> \
   7.569 @@ -1078,7 +1063,7 @@
   7.570  
   7.571  (*** alternative definition ***)
   7.572  Goalw [HNatInfinite_def,SHNat_def,hypnat_of_nat_def] 
   7.573 -      "HNatInfinite = {N. ALL n:SHNat. n < N}";
   7.574 +     "HNatInfinite = {N. ALL n:SNat. n < N}";
   7.575  by (Step_tac 1);
   7.576  by (dres_inst_tac [("x","Abs_hypnat \
   7.577  \        (hypnatrel ^^ {%n. N})")] bspec 2);
   7.578 @@ -1094,8 +1079,8 @@
   7.579  (*--------------------------------------------------------------------
   7.580     Alternative definition for HNatInfinite using Free ultrafilter
   7.581   --------------------------------------------------------------------*)
   7.582 -Goal "!!x. x : HNatInfinite ==> EX X: Rep_hypnat x. \
   7.583 -\          ALL u. {n. u < X n}:  FreeUltrafilterNat";
   7.584 +Goal "x : HNatInfinite ==> EX X: Rep_hypnat x. \
   7.585 +\                           ALL u. {n. u < X n}:  FreeUltrafilterNat";
   7.586  by (auto_tac (claset(),simpset() addsimps [hypnat_less_def,
   7.587      HNatInfinite_iff,SHNat_iff,hypnat_of_nat_def]));
   7.588  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   7.589 @@ -1108,26 +1093,25 @@
   7.590  by (Fuf_tac 1);
   7.591  qed "HNatInfinite_FreeUltrafilterNat";
   7.592  
   7.593 -Goal "!!x. EX X: Rep_hypnat x. \
   7.594 -\          ALL u. {n. u < X n}:  FreeUltrafilterNat \
   7.595 -\          ==> x: HNatInfinite";
   7.596 +Goal "EX X: Rep_hypnat x. ALL u. {n. u < X n}:  FreeUltrafilterNat \
   7.597 +\     ==> x: HNatInfinite";
   7.598  by (auto_tac (claset(),simpset() addsimps [hypnat_less_def,
   7.599      HNatInfinite_iff,SHNat_iff,hypnat_of_nat_def]));
   7.600  by (rtac exI 1 THEN Auto_tac);
   7.601  qed "FreeUltrafilterNat_HNatInfinite";
   7.602  
   7.603 -Goal "!!x. (x : HNatInfinite) = (EX X: Rep_hypnat x. \
   7.604 +Goal "(x : HNatInfinite) = (EX X: Rep_hypnat x. \
   7.605  \          ALL u. {n. u < X n}:  FreeUltrafilterNat)";
   7.606  by (blast_tac (claset() addIs [HNatInfinite_FreeUltrafilterNat,
   7.607      FreeUltrafilterNat_HNatInfinite]) 1);
   7.608  qed "HNatInfinite_FreeUltrafilterNat_iff";
   7.609  
   7.610 -Goal "!!x. x : HNatInfinite ==> 1hn < x";
   7.611 +Goal "x : HNatInfinite ==> 1hn < x";
   7.612  by (auto_tac (claset(),simpset() addsimps [HNatInfinite_iff]));
   7.613  qed "HNatInfinite_gt_one";
   7.614  Addsimps [HNatInfinite_gt_one];
   7.615  
   7.616 -Goal "!!x. 0 ~: HNatInfinite";
   7.617 +Goal "0 ~: HNatInfinite";
   7.618  by (auto_tac (claset(),simpset() 
   7.619      addsimps [HNatInfinite_iff]));
   7.620  by (dres_inst_tac [("a","1hn")] equals0D 1);
   7.621 @@ -1135,11 +1119,11 @@
   7.622  qed "zero_not_mem_HNatInfinite";
   7.623  Addsimps [zero_not_mem_HNatInfinite];
   7.624  
   7.625 -Goal "!!x. x : HNatInfinite ==> x ~= 0";
   7.626 -by (Auto_tac);
   7.627 +Goal "x : HNatInfinite ==> x ~= 0";
   7.628 +by Auto_tac;
   7.629  qed "HNatInfinite_not_eq_zero";
   7.630  
   7.631 -Goal "!!x. x : HNatInfinite ==> 1hn <= x";
   7.632 +Goal "x : HNatInfinite ==> 1hn <= x";
   7.633  by (blast_tac (claset() addIs [hypnat_less_imp_le,
   7.634           HNatInfinite_gt_one]) 1);
   7.635  qed "HNatInfinite_ge_one";
   7.636 @@ -1148,7 +1132,7 @@
   7.637  (*--------------------------------------------------
   7.638                     Closure Rules
   7.639   --------------------------------------------------*)
   7.640 -Goal "!!x. [| x: HNatInfinite; y: HNatInfinite |] \
   7.641 +Goal "[| x: HNatInfinite; y: HNatInfinite |] \
   7.642  \           ==> x + y: HNatInfinite";
   7.643  by (auto_tac (claset(),simpset() addsimps [HNatInfinite_iff]));
   7.644  by (dtac bspec 1 THEN assume_tac 1);
   7.645 @@ -1157,16 +1141,14 @@
   7.646  by (Asm_full_simp_tac 1);
   7.647  qed "HNatInfinite_add";
   7.648  
   7.649 -Goal "!!x. [| x: HNatInfinite; y: SHNat |] \
   7.650 -\                       ==> x + y: HNatInfinite";
   7.651 +Goal "[| x: HNatInfinite; y: SNat |] ==> x + y: HNatInfinite";
   7.652  by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1);
   7.653  by (dres_inst_tac [("x","x + y")] SHNat_minus 1);
   7.654  by (auto_tac (claset(),simpset() addsimps 
   7.655      [SHNat_not_HNatInfinite_iff]));
   7.656  qed "HNatInfinite_SHNat_add";
   7.657  
   7.658 -goal HyperNat.thy "!!x. [| x: HNatInfinite; y: SHNat |] \
   7.659 -\                       ==> x - y: HNatInfinite";
   7.660 +Goal "[| x: HNatInfinite; y: SNat |] ==> x - y: HNatInfinite";
   7.661  by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1);
   7.662  by (dres_inst_tac [("x","x - y")] SHNat_add 1);
   7.663  by (subgoal_tac "y <= x" 2);
   7.664 @@ -1176,23 +1158,21 @@
   7.665      simpset() addsimps [not_SHNat_HNatInfinite_iff,HNatInfinite_iff]));
   7.666  qed "HNatInfinite_SHNat_diff";
   7.667  
   7.668 -Goal 
   7.669 -     "!!x. x: HNatInfinite ==> x + 1hn: HNatInfinite";
   7.670 +Goal "x: HNatInfinite ==> x + 1hn: HNatInfinite";
   7.671  by (auto_tac (claset() addIs [HNatInfinite_SHNat_add],
   7.672                simpset()));
   7.673  qed "HNatInfinite_add_one";
   7.674  
   7.675 -Goal 
   7.676 -     "!!x. x: HNatInfinite ==> x - 1hn: HNatInfinite";
   7.677 +Goal "x: HNatInfinite ==> x - 1hn: HNatInfinite";
   7.678  by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1);
   7.679  by (dres_inst_tac [("x","x - 1hn"),("y","1hn")] SHNat_add 1);
   7.680  by (auto_tac (claset(),simpset() addsimps 
   7.681      [not_SHNat_HNatInfinite_iff RS sym]));
   7.682  qed "HNatInfinite_minus_one";
   7.683  
   7.684 -Goal "!!x. x : HNatInfinite ==> EX y. x = y + 1hn";
   7.685 +Goal "x : HNatInfinite ==> EX y. x = y + 1hn";
   7.686  by (res_inst_tac [("x","x - 1hn")] exI 1);
   7.687 -by (Auto_tac);
   7.688 +by Auto_tac;
   7.689  qed "HNatInfinite_is_Suc";
   7.690  
   7.691  (*---------------------------------------------------------------
   7.692 @@ -1200,23 +1180,21 @@
   7.693         Obtained using the NS extension of the naturals
   7.694   --------------------------------------------------------------*)
   7.695   
   7.696 -Goalw [HNat_def,starset_def,
   7.697 -         hypreal_of_posnat_def,hypreal_of_real_def] 
   7.698 -         "hypreal_of_posnat N : HNat";
   7.699 -by (Auto_tac);
   7.700 +Goalw [HNat_def,starset_def, hypreal_of_nat_def,hypreal_of_real_def] 
   7.701 +     "hypreal_of_nat N : HNat";
   7.702 +by Auto_tac;
   7.703  by (Ultra_tac 1);
   7.704 -by (res_inst_tac [("x","Suc N")] exI 1);
   7.705 -by (dtac sym 1 THEN auto_tac (claset(),simpset() 
   7.706 -    addsimps [real_of_preal_real_of_nat_Suc]));
   7.707 -qed "HNat_hypreal_of_posnat";
   7.708 -Addsimps [HNat_hypreal_of_posnat];
   7.709 +by (res_inst_tac [("x","N")] exI 1);
   7.710 +by Auto_tac;  
   7.711 +qed "HNat_hypreal_of_nat";
   7.712 +Addsimps [HNat_hypreal_of_nat];
   7.713  
   7.714  Goalw [HNat_def,starset_def]
   7.715       "[| x: HNat; y: HNat |] ==> x + y: HNat";
   7.716  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   7.717  by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   7.718  by (auto_tac (claset() addSDs [bspec] addIs [lemma_hyprel_refl],
   7.719 -    simpset() addsimps [hypreal_add]));
   7.720 +              simpset() addsimps [hypreal_add]));
   7.721  by (Ultra_tac 1);
   7.722  by (dres_inst_tac [("t","Y xb")] sym 1);
   7.723  by (auto_tac (claset(),simpset() addsimps [real_of_nat_add RS sym]));
   7.724 @@ -1236,10 +1214,10 @@
   7.725  (*---------------------------------------------------------------
   7.726      Embedding of the hypernaturals into the hyperreal
   7.727   --------------------------------------------------------------*)
   7.728 -(*** A lemma that should have been derived a long time ago! ***)
   7.729 +
   7.730  Goal "(Ya : hyprel ^^{%n. f(n)}) = \
   7.731 -\         ({n. f n = Ya n} : FreeUltrafilterNat)";
   7.732 -by (Auto_tac);
   7.733 +\     ({n. f n = Ya n} : FreeUltrafilterNat)";
   7.734 +by Auto_tac;
   7.735  qed "lemma_hyprel_FUFN";
   7.736  
   7.737  Goalw [hypreal_of_hypnat_def]
   7.738 @@ -1255,8 +1233,7 @@
   7.739  by (rtac injI 1);
   7.740  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   7.741  by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
   7.742 -by (auto_tac (claset(),simpset() addsimps 
   7.743 -    [hypreal_of_hypnat,real_of_nat_eq_cancel]));
   7.744 +by (auto_tac (claset(), simpset() addsimps [hypreal_of_hypnat]));
   7.745  qed "inj_hypreal_of_hypnat";
   7.746  
   7.747  Goal "(hypreal_of_hypnat n = hypreal_of_hypnat m) = (n = m)";
   7.748 @@ -1326,7 +1303,7 @@
   7.749  Addsimps [hypnat_not_all_eq_zero];
   7.750  
   7.751  Goal "n ~= 0 ==> (n <= 1hn) = (n = 1hn)";
   7.752 -by (auto_tac (claset(),simpset() addsimps [hypnat_le_eq_less_or_eq]));
   7.753 +by (auto_tac (claset(), simpset() addsimps [hypnat_le_less]));
   7.754  qed "hypnat_le_one_eq_one";
   7.755  Addsimps [hypnat_le_one_eq_one];
   7.756  
     8.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Thu Jan 04 10:22:33 2001 +0100
     8.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Thu Jan 04 10:23:01 2001 +0100
     8.3 @@ -21,29 +21,12 @@
     8.4    "1hn"       :: hypnat               ("1hn")  
     8.5    "whn"       :: hypnat               ("whn")  
     8.6  
     8.7 -defs
     8.8 -
     8.9 -  hypnat_zero_def      "0 == Abs_hypnat(hypnatrel^^{%n::nat. 0})"
    8.10 -  hypnat_one_def       "1hn == Abs_hypnat(hypnatrel^^{%n::nat. 1})"
    8.11 -
    8.12 -  (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
    8.13 -  hypnat_omega_def     "whn == Abs_hypnat(hypnatrel^^{%n::nat. n})"
    8.14 - 
    8.15 -
    8.16  constdefs
    8.17  
    8.18    (* embedding the naturals in the hypernaturals *)
    8.19    hypnat_of_nat   :: nat => hypnat
    8.20    "hypnat_of_nat m  == Abs_hypnat(hypnatrel^^{%n::nat. m})"
    8.21  
    8.22 -  (* set of naturals embedded in the hypernaturals*)
    8.23 -  SHNat         :: "hypnat set"
    8.24 -  "SHNat        == {n. EX N. n = hypnat_of_nat N}"  
    8.25 - 
    8.26 -  (* embedding the naturals in the hyperreals*)
    8.27 -  SNat         :: "hypreal set"
    8.28 -  "SNat        == {n. EX N. n = hypreal_of_nat N}"  
    8.29 -
    8.30    (* hypernaturals as members of the hyperreals; the set is defined as  *)
    8.31    (* the nonstandard extension of set of naturals embedded in the reals *)
    8.32    HNat         :: "hypreal set"
    8.33 @@ -51,7 +34,7 @@
    8.34  
    8.35    (* the set of infinite hypernatural numbers *)
    8.36    HNatInfinite :: "hypnat set"
    8.37 -  "HNatInfinite == {n. n ~: SHNat}"
    8.38 +  "HNatInfinite == {n. n ~: SNat}"
    8.39  
    8.40    (* explicit embedding of the hypernaturals in the hyperreals *)    
    8.41    hypreal_of_hypnat :: hypnat => hypreal
    8.42 @@ -59,6 +42,23 @@
    8.43                              hyprel^^{%n::nat. real_of_nat (X n)})"
    8.44    
    8.45  defs
    8.46 +
    8.47 +  (** the overloaded constant "SNat" **)
    8.48 +  
    8.49 +  (* set of naturals embedded in the hyperreals*)
    8.50 +  SNat_def             "SNat == {n. EX N. n = hypreal_of_nat N}"  
    8.51 +
    8.52 +  (* set of naturals embedded in the hypernaturals*)
    8.53 +  SHNat_def            "SNat == {n. EX N. n = hypnat_of_nat N}"  
    8.54 +
    8.55 +  (** hypernatural arithmetic **)
    8.56 +  
    8.57 +  hypnat_zero_def      "0 == Abs_hypnat(hypnatrel^^{%n::nat. 0})"
    8.58 +  hypnat_one_def       "1hn == Abs_hypnat(hypnatrel^^{%n::nat. 1})"
    8.59 +
    8.60 +  (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
    8.61 +  hypnat_omega_def     "whn == Abs_hypnat(hypnatrel^^{%n::nat. n})"
    8.62 + 
    8.63    hypnat_add_def  
    8.64    "P + Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q).
    8.65                  hypnatrel^^{%n::nat. X n + Y n})"
     9.1 --- a/src/HOL/Hyperreal/HyperOrd.ML	Thu Jan 04 10:22:33 2001 +0100
     9.2 +++ b/src/HOL/Hyperreal/HyperOrd.ML	Thu Jan 04 10:23:01 2001 +0100
     9.3 @@ -102,22 +102,22 @@
     9.4  qed "hypreal_lt_zero_iff";
     9.5  
     9.6  Goalw [hypreal_le_def] "((0::hypreal) <= x) = (-x <= x)";
     9.7 -by (auto_tac (claset(),simpset() addsimps [hypreal_lt_zero_iff RS sym]));
     9.8 +by (auto_tac (claset(), simpset() addsimps [hypreal_lt_zero_iff RS sym]));
     9.9  qed "hypreal_ge_zero_iff";
    9.10  
    9.11  Goalw [hypreal_le_def] "(x <= (0::hypreal)) = (x <= -x)";
    9.12 -by (auto_tac (claset(),simpset() addsimps [hypreal_gt_zero_iff RS sym]));
    9.13 +by (auto_tac (claset(), simpset() addsimps [hypreal_gt_zero_iff RS sym]));
    9.14  qed "hypreal_le_zero_iff";
    9.15  
    9.16  Goalw [hypreal_zero_def] 
    9.17        "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y";
    9.18  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    9.19  by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
    9.20 -by (auto_tac (claset(),simpset() addsimps
    9.21 -    [hypreal_less_def,hypreal_add]));
    9.22 -by (auto_tac (claset() addSIs [exI],simpset() addsimps
    9.23 -    [hypreal_less_def,hypreal_add]));
    9.24 -by (ultra_tac (claset() addIs [real_add_order],simpset()) 1);
    9.25 +by (auto_tac (claset(),
    9.26 +              simpset() addsimps [hypreal_less_def,hypreal_add]));
    9.27 +by (auto_tac (claset() addSIs [exI],
    9.28 +              simpset() addsimps [hypreal_less_def,hypreal_add]));
    9.29 +by (ultra_tac (claset() addIs [real_add_order], simpset()) 1);
    9.30  qed "hypreal_add_order";
    9.31  
    9.32  Goal "[| 0 < x; 0 <= y |] ==> (0::hypreal) < x + y";
    9.33 @@ -130,8 +130,8 @@
    9.34            "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y";
    9.35  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    9.36  by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
    9.37 -by (auto_tac (claset() addSIs [exI],simpset() addsimps
    9.38 -    [hypreal_less_def,hypreal_mult]));
    9.39 +by (auto_tac (claset() addSIs [exI],
    9.40 +              simpset() addsimps [hypreal_less_def,hypreal_mult]));
    9.41  by (ultra_tac (claset() addIs [rename_numerals real_mult_order],
    9.42  	       simpset()) 1);
    9.43  qed "hypreal_mult_order";
    9.44 @@ -142,31 +142,6 @@
    9.45  by (Asm_full_simp_tac 1);
    9.46  qed "hypreal_mult_less_zero1";
    9.47  
    9.48 -Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x * y";
    9.49 -by (REPEAT(dtac order_le_imp_less_or_eq 1));
    9.50 -by (auto_tac (claset() addIs [hypreal_mult_order, order_less_imp_le],
    9.51 -              simpset()));
    9.52 -qed "hypreal_le_mult_order";
    9.53 -
    9.54 -
    9.55 -Goal "[| x <= 0; y <= 0 |] ==> (0::hypreal) <= x * y";
    9.56 -by (rtac hypreal_less_or_eq_imp_le 1);
    9.57 -by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1);
    9.58 -by Auto_tac;
    9.59 -by (dtac order_le_imp_less_or_eq 1);
    9.60 -by (auto_tac (claset() addDs [hypreal_mult_less_zero1],simpset()));
    9.61 -qed "hypreal_mult_le_zero1";
    9.62 -
    9.63 -Goal "[| 0 <= x; y < 0 |] ==> x * y <= (0::hypreal)";
    9.64 -by (rtac hypreal_less_or_eq_imp_le 1);
    9.65 -by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1);
    9.66 -by Auto_tac;
    9.67 -by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
    9.68 -by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
    9.69 -by (blast_tac (claset() addDs [hypreal_mult_order] 
    9.70 -    addIs [hypreal_minus_mult_eq2 RS ssubst]) 1);
    9.71 -qed "hypreal_mult_le_zero";
    9.72 -
    9.73  Goal "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)";
    9.74  by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
    9.75  by (dtac hypreal_mult_order 1 THEN assume_tac 1);
    9.76 @@ -181,22 +156,6 @@
    9.77          simpset() addsimps [real_zero_less_one, FreeUltrafilterNat_Nat_set]));
    9.78  qed "hypreal_zero_less_one";
    9.79  
    9.80 -Goal "1hr < 1hr + 1hr";
    9.81 -by (rtac (hypreal_less_minus_iff RS iffD2) 1);
    9.82 -by (full_simp_tac (simpset() addsimps [hypreal_zero_less_one,
    9.83 -    hypreal_add_assoc]) 1);
    9.84 -qed "hypreal_one_less_two";
    9.85 -
    9.86 -Goal "0 < 1hr + 1hr";
    9.87 -by (rtac ([hypreal_zero_less_one,
    9.88 -          hypreal_one_less_two] MRS order_less_trans) 1);
    9.89 -qed "hypreal_zero_less_two";
    9.90 -
    9.91 -Goal "1hr + 1hr ~= 0";
    9.92 -by (rtac (hypreal_zero_less_two RS hypreal_not_refl2 RS not_sym) 1);
    9.93 -qed "hypreal_two_not_zero";
    9.94 -Addsimps [hypreal_two_not_zero];
    9.95 -
    9.96  Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x + y";
    9.97  by (REPEAT(dtac order_le_imp_less_or_eq 1));
    9.98  by (auto_tac (claset() addIs [hypreal_add_order, order_less_imp_le],
    9.99 @@ -232,9 +191,9 @@
   9.100  by (dtac hypreal_add_order 1 THEN assume_tac 1);
   9.101  by (thin_tac "0 < y2 + - z2" 1);
   9.102  by (dres_inst_tac [("C","z1 + z2")] hypreal_add_less_mono1 1);
   9.103 -by (auto_tac (claset(),simpset() addsimps 
   9.104 -    [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac
   9.105 -    delsimps [hypreal_minus_add_distrib]));
   9.106 +by (auto_tac (claset(),
   9.107 +      simpset() addsimps [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac
   9.108 +                delsimps [hypreal_minus_add_distrib]));
   9.109  qed "hypreal_add_less_mono";
   9.110  
   9.111  Goal "(q1::hypreal) <= q2  ==> x + q1 <= x + q2";
   9.112 @@ -322,7 +281,7 @@
   9.113  
   9.114  Goal "[| (0::hypreal)<=z; x<y |] ==> x*z<=y*z";
   9.115  by (EVERY1 [rtac hypreal_less_or_eq_imp_le, dtac order_le_imp_less_or_eq]);
   9.116 -by (auto_tac (claset() addIs [hypreal_mult_less_mono1],simpset()));
   9.117 +by (auto_tac (claset() addIs [hypreal_mult_less_mono1], simpset()));
   9.118  qed "hypreal_mult_le_less_mono1";
   9.119  
   9.120  Goal "[| (0::hypreal)<=z; x<y |] ==> z*x<=z*y";
   9.121 @@ -397,12 +356,6 @@
   9.122  by (blast_tac (claset() addDs [hypreal_mult_zero_disj]) 1);
   9.123  qed "hypreal_mult_is_0";
   9.124  
   9.125 -Goal "(x*x + y*y = 0) = (x = 0 & y = (0::hypreal))";
   9.126 -by (simp_tac (HOL_ss addsimps [hypreal_le_square, hypreal_add_nonneg_eq_0_iff, 
   9.127 -                               hypreal_mult_is_0]) 1);
   9.128 -qed "hypreal_squares_add_zero_iff";
   9.129 -Addsimps [hypreal_squares_add_zero_iff];
   9.130 -
   9.131  Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))";
   9.132  by (simp_tac (HOL_ss addsimps [hypreal_le_square, hypreal_le_add_order, 
   9.133                           hypreal_add_nonneg_eq_0_iff, hypreal_mult_is_0]) 1);
   9.134 @@ -435,58 +388,8 @@
   9.135  
   9.136  
   9.137  (*----------------------------------------------------------------------------
   9.138 -             Embedding of the naturals in the hyperreals
   9.139 +               Existence of infinite hyperreal number
   9.140   ----------------------------------------------------------------------------*)
   9.141 -Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 0 = 1hr";
   9.142 -by (full_simp_tac (simpset() addsimps 
   9.143 -    [pnat_one_iff RS sym,real_of_preal_def]) 1);
   9.144 -by (fold_tac [real_one_def]);
   9.145 -by (simp_tac (simpset() addsimps [hypreal_of_real_one]) 1);
   9.146 -qed "hypreal_of_posnat_one";
   9.147 -
   9.148 -Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr";
   9.149 -by (full_simp_tac (simpset() addsimps 
   9.150 -		   [real_of_preal_def,
   9.151 -		    rename_numerals (real_one_def RS meta_eq_to_obj_eq),
   9.152 -		    hypreal_add,hypreal_of_real_def,pnat_two_eq,
   9.153 -		    hypreal_one_def, real_add,
   9.154 -		    prat_of_pnat_add RS sym, preal_of_prat_add RS sym] @ 
   9.155 -		    pnat_add_ac) 1);
   9.156 -qed "hypreal_of_posnat_two";
   9.157 -
   9.158 -(*FIXME: delete this and all posnat*)
   9.159 -Goalw [hypreal_of_posnat_def]
   9.160 -     "hypreal_of_posnat n1 + hypreal_of_posnat n2 = \
   9.161 -\     hypreal_of_posnat (n1 + n2) + 1hr";
   9.162 -by (full_simp_tac (HOL_ss addsimps [hypreal_of_posnat_one RS sym,
   9.163 -    hypreal_of_real_add RS sym,hypreal_of_posnat_def,real_of_preal_add RS sym,
   9.164 -    preal_of_prat_add RS sym,prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
   9.165 -qed "hypreal_of_posnat_add";
   9.166 -
   9.167 -Goal "hypreal_of_posnat (n + 1) = hypreal_of_posnat n + 1hr";
   9.168 -by (res_inst_tac [("x1","1hr")] (hypreal_add_right_cancel RS iffD1) 1);
   9.169 -by (rtac (hypreal_of_posnat_add RS subst) 1);
   9.170 -by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,hypreal_add_assoc]) 1);
   9.171 -qed "hypreal_of_posnat_add_one";
   9.172 -
   9.173 -Goalw [real_of_posnat_def,hypreal_of_posnat_def] 
   9.174 -      "hypreal_of_posnat n = hypreal_of_real (real_of_posnat n)";
   9.175 -by (rtac refl 1);
   9.176 -qed "hypreal_of_real_of_posnat";
   9.177 -
   9.178 -Goalw [hypreal_of_posnat_def] 
   9.179 -      "(n < m) = (hypreal_of_posnat n < hypreal_of_posnat m)";
   9.180 -by Auto_tac;
   9.181 -qed "hypreal_of_posnat_less_iff";
   9.182 -
   9.183 -Addsimps [hypreal_of_posnat_less_iff RS sym];
   9.184 -(*---------------------------------------------------------------------------------
   9.185 -               Existence of infinite hyperreal number
   9.186 - ---------------------------------------------------------------------------------*)
   9.187 -
   9.188 -Goal "hyprel^^{%n::nat. real_of_posnat n} : hypreal";
   9.189 -by Auto_tac;
   9.190 -qed "hypreal_omega";
   9.191  
   9.192  Goalw [omega_def] "Rep_hypreal(whr) : hypreal";
   9.193  by (rtac Rep_hypreal 1);
   9.194 @@ -496,20 +399,21 @@
   9.195  (* use assumption that member FreeUltrafilterNat is not finite       *)
   9.196  (* a few lemmas first *)
   9.197  
   9.198 -Goal "{n::nat. x = real_of_posnat n} = {} | \
   9.199 -\     (EX y. {n::nat. x = real_of_posnat n} = {y})";
   9.200 -by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],simpset()));
   9.201 +Goal "{n::nat. x = real_of_nat n} = {} | \
   9.202 +\     (EX y. {n::nat. x = real_of_nat n} = {y})";
   9.203 +by (auto_tac (claset() addDs [inj_real_of_nat RS injD], simpset()));
   9.204  qed "lemma_omega_empty_singleton_disj";
   9.205  
   9.206 -Goal "finite {n::nat. x = real_of_posnat n}";
   9.207 +Goal "finite {n::nat. x = real_of_nat n}";
   9.208  by (cut_inst_tac [("x","x")] lemma_omega_empty_singleton_disj 1);
   9.209  by Auto_tac;
   9.210  qed "lemma_finite_omega_set";
   9.211  
   9.212  Goalw [omega_def,hypreal_of_real_def] 
   9.213        "~ (EX x. hypreal_of_real x = whr)";
   9.214 -by (auto_tac (claset(),simpset() addsimps [lemma_finite_omega_set 
   9.215 -    RS FreeUltrafilterNat_finite]));
   9.216 +by (auto_tac (claset(),
   9.217 +    simpset() addsimps [real_of_nat_Suc, real_diff_eq_eq RS sym, 
   9.218 +                    lemma_finite_omega_set RS FreeUltrafilterNat_finite]));
   9.219  qed "not_ex_hypreal_of_real_eq_omega";
   9.220  
   9.221  Goal "hypreal_of_real x ~= whr";
   9.222 @@ -520,21 +424,25 @@
   9.223  (* existence of infinitesimal number also not *)
   9.224  (* corresponding to any real number *)
   9.225  
   9.226 -Goal "{n::nat. x = inverse(real_of_posnat n)} = {} | \
   9.227 -\     (EX y. {n::nat. x = inverse(real_of_posnat n)} = {y})";
   9.228 -by (Step_tac 1 THEN Step_tac 1);
   9.229 -by (auto_tac (claset() addIs [real_of_posnat_inverse_inj],simpset()));
   9.230 +Goal "inverse (real_of_nat x) = inverse (real_of_nat y) ==> x = y";
   9.231 +by (rtac (inj_real_of_nat RS injD) 1);
   9.232 +by (Asm_full_simp_tac 1); 
   9.233 +qed "real_of_nat_inverse_inj";
   9.234 +
   9.235 +Goal "{n::nat. x = inverse(real_of_nat(Suc n))} = {} | \
   9.236 +\     (EX y. {n::nat. x = inverse(real_of_nat(Suc n))} = {y})";
   9.237 +by (auto_tac (claset(), simpset() addsimps [inj_real_of_nat RS inj_eq]));
   9.238  qed "lemma_epsilon_empty_singleton_disj";
   9.239  
   9.240 -Goal "finite {n::nat. x = inverse(real_of_posnat n)}";
   9.241 +Goal "finite {n::nat. x = inverse(real_of_nat(Suc n))}";
   9.242  by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1);
   9.243  by Auto_tac;
   9.244  qed "lemma_finite_epsilon_set";
   9.245  
   9.246  Goalw [epsilon_def,hypreal_of_real_def] 
   9.247        "~ (EX x. hypreal_of_real x = ehr)";
   9.248 -by (auto_tac (claset(),simpset() addsimps [lemma_finite_epsilon_set 
   9.249 -    RS FreeUltrafilterNat_finite]));
   9.250 +by (auto_tac (claset(),
   9.251 +  simpset() addsimps [lemma_finite_epsilon_set RS FreeUltrafilterNat_finite]));
   9.252  qed "not_ex_hypreal_of_real_eq_epsilon";
   9.253  
   9.254  Goal "hypreal_of_real x ~= ehr";
   9.255 @@ -543,96 +451,28 @@
   9.256  qed "hypreal_of_real_not_eq_epsilon";
   9.257  
   9.258  Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0";
   9.259 +by Auto_tac;  
   9.260  by (auto_tac (claset(),
   9.261 -     simpset() addsimps [rename_numerals real_of_posnat_not_eq_zero]));
   9.262 +     simpset() addsimps [real_of_nat_Suc_gt_zero RS real_not_refl2 RS not_sym]));
   9.263  qed "hypreal_epsilon_not_zero";
   9.264  
   9.265 -Addsimps [rename_numerals real_of_posnat_not_eq_zero];
   9.266 -Goalw [omega_def,hypreal_zero_def] "whr ~= 0";
   9.267 -by (Simp_tac 1);
   9.268 -qed "hypreal_omega_not_zero";
   9.269 -
   9.270  Goal "ehr = inverse(whr)";
   9.271  by (asm_full_simp_tac (simpset() addsimps 
   9.272                       [hypreal_inverse, omega_def, epsilon_def]) 1);
   9.273  qed "hypreal_epsilon_inverse_omega";
   9.274  
   9.275 -(*----------------------------------------------------------------
   9.276 -     Another embedding of the naturals in the 
   9.277 -    hyperreals (see hypreal_of_posnat)
   9.278 - ----------------------------------------------------------------*)
   9.279 -Goalw [hypreal_of_nat_def] "hypreal_of_nat 0 = 0";
   9.280 -by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one]) 1);
   9.281 -qed "hypreal_of_nat_zero";
   9.282 -
   9.283 -Goalw [hypreal_of_nat_def] "hypreal_of_nat 1 = 1hr";
   9.284 -by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,
   9.285 -                                       hypreal_add_assoc]) 1);
   9.286 -qed "hypreal_of_nat_one";
   9.287 -
   9.288 -Goalw [hypreal_of_nat_def]
   9.289 -     "hypreal_of_nat n1 + hypreal_of_nat n2 = hypreal_of_nat (n1 + n2)";
   9.290 -by (full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
   9.291 -by (simp_tac (simpset() addsimps [hypreal_of_posnat_add,
   9.292 -                                  hypreal_add_assoc RS sym]) 1);
   9.293 -qed "hypreal_of_nat_add";
   9.294 -
   9.295 -Goal "hypreal_of_nat 2 = 1hr + 1hr";
   9.296 -by (simp_tac (simpset() addsimps [hypreal_of_nat_one 
   9.297 -    RS sym,hypreal_of_nat_add]) 1);
   9.298 -qed "hypreal_of_nat_two";
   9.299 -
   9.300 -Goalw [hypreal_of_nat_def] 
   9.301 -      "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)";
   9.302 -by (auto_tac (claset() addIs [hypreal_add_less_mono1],simpset()));
   9.303 -qed "hypreal_of_nat_less_iff";
   9.304 -Addsimps [hypreal_of_nat_less_iff RS sym];
   9.305 -
   9.306 -(*------------------------------------------------------------*)
   9.307 -(* naturals embedded in hyperreals                            *)
   9.308 -(* is a hyperreal c.f. NS extension                           *)
   9.309 -(*------------------------------------------------------------*)
   9.310 -
   9.311 -Goalw [hypreal_of_nat_def,real_of_nat_def] 
   9.312 -      "hypreal_of_nat  m = Abs_hypreal(hyprel^^{%n. real_of_nat m})";
   9.313 -by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def,
   9.314 -    hypreal_of_real_of_posnat,hypreal_minus,hypreal_one_def,hypreal_add]));
   9.315 -qed "hypreal_of_nat_iff";
   9.316 -
   9.317 -Goal "inj hypreal_of_nat";
   9.318 -by (rtac injI 1);
   9.319 -by (auto_tac (claset() addSDs [FreeUltrafilterNat_P],
   9.320 -        simpset() addsimps [split_if_mem1, hypreal_of_nat_iff,
   9.321 -        real_add_right_cancel,inj_real_of_nat RS injD]));
   9.322 -qed "inj_hypreal_of_nat";
   9.323 -
   9.324 -Goalw [hypreal_of_nat_def,hypreal_of_real_def,hypreal_of_posnat_def,
   9.325 -       real_of_posnat_def,hypreal_one_def,real_of_nat_def] 
   9.326 -       "hypreal_of_nat n = hypreal_of_real (real_of_nat n)";
   9.327 -by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1);
   9.328 -qed "hypreal_of_nat_real_of_nat";
   9.329 -
   9.330 -Goal "hypreal_of_posnat (Suc n) = hypreal_of_posnat n + 1hr";
   9.331 -by (stac (hypreal_of_posnat_add_one RS sym) 1);
   9.332 -by (Simp_tac 1);
   9.333 -qed "hypreal_of_posnat_Suc";
   9.334 -
   9.335 -Goalw [hypreal_of_nat_def] 
   9.336 -      "hypreal_of_nat (Suc n) = hypreal_of_nat n + 1hr";
   9.337 -by (simp_tac (simpset() addsimps [hypreal_of_posnat_Suc] @ hypreal_add_ac) 1);
   9.338 -qed "hypreal_of_nat_Suc";
   9.339  
   9.340  (* this proof is so much simpler than one for reals!! *)
   9.341  Goal "[| 0 < r; r < x |] ==> inverse x < inverse (r::hypreal)";
   9.342  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   9.343  by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   9.344 -by (auto_tac (claset(),simpset() addsimps [hypreal_inverse,
   9.345 -    hypreal_less,hypreal_zero_def]));
   9.346 -by (ultra_tac (claset() addIs [real_inverse_less_swap],simpset()) 1);
   9.347 +by (auto_tac (claset(),
   9.348 +      simpset() addsimps [hypreal_inverse, hypreal_less,hypreal_zero_def]));
   9.349 +by (ultra_tac (claset() addIs [real_inverse_less_swap], simpset()) 1);
   9.350  qed "hypreal_inverse_less_swap";
   9.351  
   9.352  Goal "[| 0 < r; 0 < x|] ==> (r < x) = (inverse x < inverse (r::hypreal))";
   9.353 -by (auto_tac (claset() addIs [hypreal_inverse_less_swap],simpset()));
   9.354 +by (auto_tac (claset() addIs [hypreal_inverse_less_swap], simpset()));
   9.355  by (res_inst_tac [("t","r")] (hypreal_inverse_inverse RS subst) 1);
   9.356  by (res_inst_tac [("t","x")] (hypreal_inverse_inverse RS subst) 1);
   9.357  by (rtac hypreal_inverse_less_swap 1);
    10.1 --- a/src/HOL/Hyperreal/HyperPow.ML	Thu Jan 04 10:22:33 2001 +0100
    10.2 +++ b/src/HOL/Hyperreal/HyperPow.ML	Thu Jan 04 10:23:01 2001 +0100
    10.3 @@ -3,6 +3,7 @@
    10.4      Copyright   : 1998  University of Cambridge
    10.5      Description : Natural Powers of hyperreals theory
    10.6  
    10.7 +Exponentials on the hyperreals
    10.8  *)
    10.9  
   10.10  Goal "(#0::hypreal) ^ (Suc n) = 0";
   10.11 @@ -136,15 +137,13 @@
   10.12  Goal "(#1::hypreal) <= #2 ^ n";
   10.13  by (res_inst_tac [("y","#1 ^ n")] order_trans 1);
   10.14  by (rtac hrealpow_le 2);
   10.15 -by (auto_tac (claset() addIs [order_less_imp_le],
   10.16 -         simpset() addsimps [hypreal_zero_less_one, hypreal_one_less_two]));
   10.17 +by Auto_tac;
   10.18  qed "two_hrealpow_ge_one";
   10.19  
   10.20  Goal "hypreal_of_nat n < #2 ^ n";
   10.21  by (induct_tac "n" 1);
   10.22  by (auto_tac (claset(),
   10.23 -        simpset() addsimps [hypreal_of_nat_Suc,hypreal_of_nat_zero,
   10.24 -          hypreal_zero_less_one,hypreal_add_mult_distrib,hypreal_of_nat_one]));
   10.25 +        simpset() addsimps [hypreal_of_nat_Suc, hypreal_add_mult_distrib]));
   10.26  by (cut_inst_tac [("n","n")] two_hrealpow_ge_one 1);
   10.27  by (arith_tac 1);
   10.28  qed "two_hrealpow_gt";
   10.29 @@ -189,9 +188,9 @@
   10.30  
   10.31  Goal "(x + (y::hypreal)) ^ 2 = \
   10.32  \     x ^ 2 + y ^ 2 + (hypreal_of_nat 2)*x*y";
   10.33 -by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2,
   10.34 -               hypreal_add_mult_distrib,hypreal_of_nat_two] 
   10.35 -                @ hypreal_add_ac @ hypreal_mult_ac) 1);
   10.36 +by (simp_tac (simpset() addsimps
   10.37 +              [hypreal_add_mult_distrib2, hypreal_add_mult_distrib, 
   10.38 +               hypreal_of_nat_zero, hypreal_of_nat_Suc]) 1);
   10.39  qed "hrealpow_sum_square_expand";
   10.40  
   10.41  (*---------------------------------------------------------------
   10.42 @@ -391,8 +390,7 @@
   10.43  Goal "(#1::hypreal) <= #2 pow n";
   10.44  by (res_inst_tac [("y","#1 pow n")] order_trans 1);
   10.45  by (rtac hyperpow_le 2);
   10.46 -by (auto_tac (claset() addIs [order_less_imp_le],
   10.47 -          simpset() addsimps [hypreal_zero_less_one, hypreal_one_less_two]));
   10.48 +by Auto_tac;
   10.49  qed "two_hyperpow_ge_one";
   10.50  Addsimps [two_hyperpow_ge_one];
   10.51  
   10.52 @@ -455,7 +453,7 @@
   10.53  qed "hyperpow_less_le2";
   10.54  
   10.55  Goal "[| #0 <= r;  r < (#1::hypreal);  N : HNatInfinite |]  \
   10.56 -\     ==> ALL n:SHNat. r pow N <= r pow n";
   10.57 +\     ==> ALL n: SNat. r pow N <= r pow n";
   10.58  by (auto_tac (claset() addSIs [hyperpow_less_le],
   10.59                simpset() addsimps [HNatInfinite_iff]));
   10.60  qed "hyperpow_SHNat_le";
   10.61 @@ -493,18 +491,16 @@
   10.62  qed "hyperpow_Suc_le_self2";
   10.63  
   10.64  Goalw [Infinitesimal_def]
   10.65 -     "[| x : Infinitesimal; 0 < N |] ==> (abs x) pow N <= abs x";
   10.66 +     "[| x : Infinitesimal; 0 < N |] ==> abs (x pow N) <= abs x";
   10.67  by (auto_tac (claset() addSIs [hyperpow_Suc_le_self2],
   10.68 -    simpset() addsimps [hyperpow_hrabs RS sym,
   10.69 -                        hypnat_gt_zero_iff2, hrabs_ge_zero,
   10.70 -                        hypreal_zero_less_one]));
   10.71 +              simpset() addsimps [hyperpow_hrabs RS sym,
   10.72 +                                  hypnat_gt_zero_iff2, hrabs_ge_zero]));
   10.73  qed "lemma_Infinitesimal_hyperpow";
   10.74  
   10.75  Goal "[| x : Infinitesimal; 0 < N |] ==> x pow N : Infinitesimal";
   10.76  by (rtac hrabs_le_Infinitesimal 1);
   10.77 -by (dtac Infinitesimal_hrabs 1);
   10.78 -by (auto_tac (claset() addSIs [lemma_Infinitesimal_hyperpow],
   10.79 -    simpset() addsimps [hyperpow_hrabs RS sym]));
   10.80 +by (rtac lemma_Infinitesimal_hyperpow 2); 
   10.81 +by Auto_tac;  
   10.82  qed "Infinitesimal_hyperpow";
   10.83  
   10.84  Goalw [hypnat_of_nat_def] 
    11.1 --- a/src/HOL/Hyperreal/HyperPow.thy	Thu Jan 04 10:22:33 2001 +0100
    11.2 +++ b/src/HOL/Hyperreal/HyperPow.thy	Thu Jan 04 10:23:01 2001 +0100
    11.3 @@ -6,6 +6,16 @@
    11.4  
    11.5  HyperPow = HRealAbs + HyperNat + RealPow +  
    11.6  
    11.7 +(** First: hypnat is linearly ordered **)
    11.8 +
    11.9 +instance hypnat :: order (hypnat_le_refl,hypnat_le_trans,hypnat_le_anti_sym,
   11.10 +                          hypnat_less_le)
   11.11 +instance hypnat :: linorder (hypnat_le_linear)
   11.12 +
   11.13 +instance hypnat :: plus_ac0(hypnat_add_commute,hypnat_add_assoc,
   11.14 +                            hypnat_add_zero_left)
   11.15 +
   11.16 +
   11.17  instance hypreal :: {power}
   11.18  
   11.19  consts hpowr :: "[hypreal,nat] => hypreal"  
    12.1 --- a/src/HOL/Hyperreal/Lim.ML	Thu Jan 04 10:22:33 2001 +0100
    12.2 +++ b/src/HOL/Hyperreal/Lim.ML	Thu Jan 04 10:23:01 2001 +0100
    12.3 @@ -5,7 +5,6 @@
    12.4                    differentiation of real=>real functions
    12.5  *)
    12.6  
    12.7 -
    12.8  fun ARITH_PROVE str = prove_goal thy str 
    12.9                        (fn prems => [cut_facts_tac prems 1,arith_tac 1]);
   12.10  
   12.11 @@ -28,12 +27,9 @@
   12.12      LIM_add    
   12.13   ---------------*)
   12.14  Goalw [LIM_def] 
   12.15 -     "[| f -- x --> l; g -- x --> m |] \
   12.16 -\     ==> (%x. f(x) + g(x)) -- x --> (l + m)";
   12.17 -by (Step_tac 1);
   12.18 +     "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)";
   12.19 +by (Clarify_tac 1);
   12.20  by (REPEAT(dres_inst_tac [("x","r/#2")] spec 1));
   12.21 -by (dtac (rename_numerals (real_zero_less_two RS real_inverse_gt_zero 
   12.22 -          RSN (2,real_mult_less_mono2))) 1);
   12.23  by (Asm_full_simp_tac 1);
   12.24  by (Clarify_tac 1);
   12.25  by (res_inst_tac [("R1.0","s"),("R2.0","sa")] 
   12.26 @@ -189,26 +185,26 @@
   12.27  Goal "ALL s. #0 < s --> (EX xa.  xa ~= x & \
   12.28  \        abs (xa + - x) < s  & r <= abs (f xa + -L)) \
   12.29  \     ==> ALL n::nat. EX xa.  xa ~= x & \
   12.30 -\             abs(xa + -x) < inverse(real_of_posnat n) & r <= abs(f xa + -L)";
   12.31 -by (Step_tac 1);
   12.32 +\             abs(xa + -x) < inverse(real_of_nat(Suc n)) & r <= abs(f xa + -L)";
   12.33 +by (Clarify_tac 1); 
   12.34  by (cut_inst_tac [("n1","n")]
   12.35 -    (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1);
   12.36 +    (real_of_nat_Suc_gt_zero RS rename_numerals real_inverse_gt_zero) 1);
   12.37  by Auto_tac;
   12.38  val lemma_LIM = result();
   12.39  
   12.40  Goal "ALL s. #0 < s --> (EX xa.  xa ~= x & \
   12.41  \        abs (xa + - x) < s  & r <= abs (f xa + -L)) \
   12.42  \     ==> EX X. ALL n::nat. X n ~= x & \
   12.43 -\               abs(X n + -x) < inverse(real_of_posnat n) & r <= abs(f (X n) + -L)";
   12.44 +\               abs(X n + -x) < inverse(real_of_nat(Suc n)) & r <= abs(f (X n) + -L)";
   12.45  by (dtac lemma_LIM 1);
   12.46  by (dtac choice 1);
   12.47  by (Blast_tac 1);
   12.48  val lemma_skolemize_LIM2 = result();
   12.49  
   12.50  Goal "ALL n. X n ~= x & \
   12.51 -\         abs (X n + - x) < inverse (real_of_posnat  n) & \
   12.52 +\         abs (X n + - x) < inverse (real_of_nat(Suc n)) & \
   12.53  \         r <= abs (f (X n) + - L) ==> \
   12.54 -\         ALL n. abs (X n + - x) < inverse (real_of_posnat  n)";
   12.55 +\         ALL n. abs (X n + - x) < inverse (real_of_nat(Suc n))";
   12.56  by (Auto_tac );
   12.57  val lemma_simp = result();
   12.58   
   12.59 @@ -217,7 +213,7 @@
   12.60   -------------------*)
   12.61  
   12.62  Goalw [LIM_def,NSLIM_def,inf_close_def] 
   12.63 -      "f -- x --NS> L ==> f -- x --> L";
   12.64 +     "f -- x --NS> L ==> f -- x --> L";
   12.65  by (asm_full_simp_tac
   12.66      (simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff]) 1);
   12.67  by (EVERY1[Step_tac, rtac ccontr, Asm_full_simp_tac]);
   12.68 @@ -697,16 +693,17 @@
   12.69  
   12.70  Goal "ALL s. #0 < s --> (EX z y. abs (z + - y) < s & r <= abs (f z + -f y)) \
   12.71  \     ==> ALL n::nat. EX z y.  \
   12.72 -\              abs(z + -y) < inverse(real_of_posnat n) & \
   12.73 +\              abs(z + -y) < inverse(real_of_nat(Suc n)) & \
   12.74  \              r <= abs(f z + -f y)";
   12.75 -by (Step_tac 1);
   12.76 -by (cut_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1);
   12.77 +by (Clarify_tac 1); 
   12.78 +by (cut_inst_tac [("n1","n")]
   12.79 +    (real_of_nat_Suc_gt_zero RS rename_numerals real_inverse_gt_zero) 1);
   12.80  by Auto_tac;
   12.81  val lemma_LIMu = result();
   12.82  
   12.83  Goal "ALL s. #0 < s --> (EX z y. abs (z + - y) < s  & r <= abs (f z + -f y)) \
   12.84  \     ==> EX X Y. ALL n::nat. \
   12.85 -\              abs(X n + -(Y n)) < inverse(real_of_posnat n) & \
   12.86 +\              abs(X n + -(Y n)) < inverse(real_of_nat(Suc n)) & \
   12.87  \              r <= abs(f (X n) + -f (Y n))";
   12.88  by (dtac lemma_LIMu 1);
   12.89  by (dtac choice 1);
   12.90 @@ -715,9 +712,9 @@
   12.91  by (Blast_tac 1);
   12.92  val lemma_skolemize_LIM2u = result();
   12.93  
   12.94 -Goal "ALL n. abs (X n + -Y n) < inverse (real_of_posnat  n) & \
   12.95 +Goal "ALL n. abs (X n + -Y n) < inverse (real_of_nat(Suc n)) & \
   12.96  \         r <= abs (f (X n) + - f(Y n)) ==> \
   12.97 -\         ALL n. abs (X n + - Y n) < inverse (real_of_posnat  n)";
   12.98 +\         ALL n. abs (X n + - Y n) < inverse (real_of_nat(Suc n))";
   12.99  by (Auto_tac );
  12.100  val lemma_simpu = result();
  12.101  
  12.102 @@ -1301,17 +1298,17 @@
  12.103  Goal "DERIV (%x. x ^ n) x :> real_of_nat n * (x ^ (n - 1))";
  12.104  by (induct_tac "n" 1);
  12.105  by (dtac (DERIV_Id RS DERIV_mult) 2);
  12.106 -by (auto_tac (claset(),simpset() addsimps 
  12.107 -    [real_add_mult_distrib]));
  12.108 +by (auto_tac (claset(), 
  12.109 +              simpset() addsimps [real_of_nat_Suc, real_add_mult_distrib]));
  12.110  by (case_tac "0 < n" 1);
  12.111  by (dres_inst_tac [("x","x")] realpow_minus_mult 1);
  12.112 -by (auto_tac (claset(),simpset() addsimps 
  12.113 -    [real_mult_assoc,real_add_commute]));
  12.114 +by (auto_tac (claset(), 
  12.115 +              simpset() addsimps [real_mult_assoc, real_add_commute]));
  12.116  qed "DERIV_pow";
  12.117  
  12.118  (* NS version *)
  12.119  Goal "NSDERIV (%x. x ^ n) x :> real_of_nat n * (x ^ (n - 1))";
  12.120 -by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,DERIV_pow]) 1);
  12.121 +by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, DERIV_pow]) 1);
  12.122  qed "NSDERIV_pow";
  12.123  
  12.124  (*---------------------------------------------------------------
    13.1 --- a/src/HOL/Hyperreal/NSA.ML	Thu Jan 04 10:22:33 2001 +0100
    13.2 +++ b/src/HOL/Hyperreal/NSA.ML	Thu Jan 04 10:23:01 2001 +0100
    13.3 @@ -228,13 +228,10 @@
    13.4  by Auto_tac;
    13.5  qed "HFiniteD";
    13.6  
    13.7 -Goalw [HFinite_def] "x : HFinite ==> abs x : HFinite";
    13.8 +Goalw [HFinite_def] "(abs x : HFinite) = (x : HFinite)";
    13.9  by (auto_tac (claset(), simpset() addsimps [hrabs_idempotent]));
   13.10 -qed "HFinite_hrabs";
   13.11 -
   13.12 -Goalw [HFinite_def,Bex_def] "x ~: HFinite ==> abs x ~: HFinite";
   13.13 -by (auto_tac (claset(), simpset() addsimps [hrabs_idempotent]));
   13.14 -qed "not_HFinite_hrabs";
   13.15 +qed "HFinite_hrabs_iff";
   13.16 +AddIffs [HFinite_hrabs_iff];
   13.17  
   13.18  Goal "number_of w : HFinite";
   13.19  by (rtac (SReal_number_of RS (SReal_subset_HFinite RS subsetD)) 1);
   13.20 @@ -389,23 +386,13 @@
   13.21  by Auto_tac;
   13.22  qed "not_Infinitesimal_not_zero2";
   13.23  
   13.24 -Goal "x : Infinitesimal ==> abs x : Infinitesimal";
   13.25 -by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1);
   13.26 -by Auto_tac;
   13.27 -qed "Infinitesimal_hrabs";
   13.28 -
   13.29 -Goal "x ~: Infinitesimal ==> abs x ~: Infinitesimal";
   13.30 -by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1);
   13.31 -by Auto_tac;
   13.32 -qed "not_Infinitesimal_hrabs";
   13.33 -
   13.34 -Goal "abs x : Infinitesimal ==> x : Infinitesimal";
   13.35 -by (rtac ccontr 1);
   13.36 -by (blast_tac (claset() addDs [not_Infinitesimal_hrabs]) 1);
   13.37 -qed "hrabs_Infinitesimal_Infinitesimal";
   13.38 +Goal "(abs x : Infinitesimal) = (x : Infinitesimal)";
   13.39 +by (auto_tac (claset(), simpset() addsimps [hrabs_def]));
   13.40 +qed "Infinitesimal_hrabs_iff";
   13.41 +AddIffs [Infinitesimal_hrabs_iff];
   13.42  
   13.43  Goal "x : HFinite - Infinitesimal ==> abs x : HFinite - Infinitesimal";
   13.44 -by (fast_tac (set_cs addSEs [HFinite_hrabs,not_Infinitesimal_hrabs]) 1);
   13.45 +by (Blast_tac 1);
   13.46  qed "HFinite_diff_Infinitesimal_hrabs";
   13.47  
   13.48  Goalw [Infinitesimal_def] 
   13.49 @@ -417,8 +404,7 @@
   13.50  
   13.51  Goal "[| e : Infinitesimal; abs x <= e |] ==> x : Infinitesimal";
   13.52  by (blast_tac (claset() addDs [order_le_imp_less_or_eq] 
   13.53 -                        addIs [hrabs_Infinitesimal_Infinitesimal,
   13.54 -                               hrabs_less_Infinitesimal]) 1);
   13.55 +                        addIs [hrabs_less_Infinitesimal]) 1);
   13.56  qed "hrabs_le_Infinitesimal";
   13.57  
   13.58  Goalw [Infinitesimal_def] 
   13.59 @@ -1091,8 +1077,7 @@
   13.60   ------------------------------------------------------------------*)
   13.61  
   13.62  Goalw [HFinite_def,HInfinite_def] "HFinite Int HInfinite = {}";
   13.63 -by (auto_tac (claset() addIs [hypreal_less_irrefl] 
   13.64 -              addDs [order_less_trans,bspec],
   13.65 +by (auto_tac (claset() addIs [hypreal_less_irrefl] addDs [order_less_trans],
   13.66                simpset()));
   13.67  qed "HFinite_Int_HInfinite_empty";
   13.68  Addsimps [HFinite_Int_HInfinite_empty];
   13.69 @@ -1102,15 +1087,10 @@
   13.70  by Auto_tac;
   13.71  qed "HFinite_not_HInfinite";
   13.72  
   13.73 -val [prem] = goalw thy [HInfinite_def] "x~: HFinite ==> x: HInfinite";
   13.74 -by (cut_facts_tac [prem] 1);
   13.75 -by (Clarify_tac 1);
   13.76 -by (auto_tac (claset() addSDs [spec],
   13.77 -              simpset() addsimps [HFinite_def,Bex_def]));
   13.78 -by (dtac hypreal_leI 1);
   13.79 -by (dtac order_le_imp_less_or_eq 1);
   13.80 -by (auto_tac (claset() addSDs [SReal_subset_HFinite RS subsetD],
   13.81 -    simpset() addsimps [prem,hrabs_idempotent,prem RS not_HFinite_hrabs]));
   13.82 +Goalw [HInfinite_def, HFinite_def] "x~: HFinite ==> x: HInfinite";
   13.83 +by Auto_tac;  
   13.84 +by (dres_inst_tac [("x","r + #1")] bspec 1);
   13.85 +by (auto_tac (claset(), simpset() addsimps [SReal_add]));   
   13.86  qed "not_HFinite_HInfinite";
   13.87  
   13.88  Goal "x : HInfinite | x : HFinite";
   13.89 @@ -1325,22 +1305,19 @@
   13.90                simpset()));
   13.91  qed "less_Infinitesimal_less";
   13.92  
   13.93 -Goal "[| #0 < x;  x ~: Infinitesimal|] ==> ALL u: monad x. #0 < u";
   13.94 -by (Step_tac 1);
   13.95 +Goal "[| #0 < x;  x ~: Infinitesimal; u: monad x |] ==> #0 < u";
   13.96  by (dtac (mem_monad_inf_close RS inf_close_sym) 1);
   13.97  by (etac (bex_Infinitesimal_iff2 RS iffD2 RS bexE) 1);
   13.98  by (dres_inst_tac [("e","-xa")] less_Infinitesimal_less 1);
   13.99  by Auto_tac;  
  13.100  qed "Ball_mem_monad_gt_zero";
  13.101  
  13.102 -Goal "[| x < #0; x ~: Infinitesimal|] ==> ALL u: monad x. u < #0";
  13.103 -by (Step_tac 1);
  13.104 +Goal "[| x < #0; x ~: Infinitesimal; u: monad x |] ==> u < #0";
  13.105  by (dtac (mem_monad_inf_close RS inf_close_sym) 1);
  13.106  by (etac (bex_Infinitesimal_iff RS iffD2 RS bexE) 1);
  13.107  by (cut_inst_tac [("x","-x"),("e","xa")] less_Infinitesimal_less 1);
  13.108  by Auto_tac;  
  13.109  qed "Ball_mem_monad_less_zero";
  13.110 -(*??GET RID OF QUANTIFIERS ABOVE??*)
  13.111  
  13.112  Goal "[|#0 < x; x ~: Infinitesimal; x @= y|] ==> #0 < y";
  13.113  by (blast_tac (claset() addDs [Ball_mem_monad_gt_zero,
  13.114 @@ -1352,16 +1329,14 @@
  13.115      inf_close_subset_monad]) 1);
  13.116  qed "lemma_inf_close_less_zero";
  13.117  
  13.118 -Goal "[| x @= y; x < #0; x ~: Infinitesimal |] \
  13.119 -\     ==> abs x @= abs y";
  13.120 +Goal "[| x @= y; x < #0; x ~: Infinitesimal |] ==> abs x @= abs y";
  13.121  by (forward_tac [lemma_inf_close_less_zero] 1);
  13.122  by (REPEAT(assume_tac 1));
  13.123  by (REPEAT(dtac hrabs_minus_eqI2 1));
  13.124  by Auto_tac;
  13.125  qed "inf_close_hrabs1";
  13.126  
  13.127 -Goal "[| x @= y; #0 < x; x ~: Infinitesimal |] \
  13.128 -\     ==> abs x @= abs y";
  13.129 +Goal "[| x @= y; #0 < x; x ~: Infinitesimal |] ==> abs x @= abs y";
  13.130  by (forward_tac [lemma_inf_close_gt_zero] 1);
  13.131  by (REPEAT(assume_tac 1));
  13.132  by (REPEAT(dtac hrabs_eqI2 1));
  13.133 @@ -1975,42 +1950,42 @@
  13.134  (*------------------------------------------------------------------------
  13.135           Infinitesimals as smaller than 1/n for all n::nat (> 0)
  13.136   ------------------------------------------------------------------------*)
  13.137 -Goal "(ALL r. #0 < r --> x < r) = (ALL n. x < inverse(real_of_posnat n))";
  13.138 -by (auto_tac (claset(),
  13.139 -        simpset() addsimps [rename_numerals real_of_posnat_gt_zero]));
  13.140 -by (blast_tac (claset() addSDs [rename_numerals reals_Archimedean] 
  13.141 +
  13.142 +Goal "(ALL r. #0 < r --> x < r) = (ALL n. x < inverse(real_of_nat (Suc n)))";
  13.143 +by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc_gt_zero]));
  13.144 +by (blast_tac (claset() addSDs [reals_Archimedean] 
  13.145                          addIs [order_less_trans]) 1);
  13.146  qed "lemma_Infinitesimal";
  13.147  
  13.148  Goal "(ALL r: SReal. #0 < r --> x < r) = \
  13.149 -\     (ALL n. x < inverse(hypreal_of_posnat n))";
  13.150 +\     (ALL n. x < inverse(hypreal_of_nat (Suc n)))";
  13.151  by (Step_tac 1);
  13.152 -by (dres_inst_tac [("x","inverse (hypreal_of_real(real_of_posnat n))")] 
  13.153 +by (dres_inst_tac [("x","inverse (hypreal_of_real(real_of_nat (Suc n)))")] 
  13.154      bspec 1);
  13.155  by (full_simp_tac (simpset() addsimps [SReal_inverse]) 1); 
  13.156 -by (rtac (real_of_posnat_gt_zero RS real_inverse_gt_zero RS 
  13.157 +by (rtac (real_of_nat_Suc_gt_zero RS rename_numerals real_inverse_gt_zero RS 
  13.158            (hypreal_of_real_less_iff RS iffD2) RSN(2,impE)) 1);
  13.159  by (assume_tac 2);
  13.160  by (asm_full_simp_tac (simpset() addsimps 
  13.161 -       [rename_numerals real_of_posnat_gt_zero, hypreal_of_real_zero,
  13.162 -        hypreal_of_real_of_posnat]) 1);
  13.163 +       [real_of_nat_Suc_gt_zero, hypreal_of_real_zero, hypreal_of_nat_def]) 1);
  13.164  by (auto_tac (claset() addSDs [reals_Archimedean],
  13.165                simpset() addsimps [SReal_iff,hypreal_of_real_zero RS sym]));
  13.166  by (dtac (hypreal_of_real_less_iff RS iffD2) 1);
  13.167  by (asm_full_simp_tac (simpset() addsimps 
  13.168 -       [rename_numerals real_of_posnat_gt_zero,hypreal_of_real_of_posnat])1);
  13.169 +         [real_of_nat_Suc_gt_zero, hypreal_of_nat_def])1);
  13.170  by (blast_tac (claset() addIs [order_less_trans]) 1);
  13.171  qed "lemma_Infinitesimal2";
  13.172  
  13.173  Goalw [Infinitesimal_def] 
  13.174 -     "Infinitesimal = {x. ALL n. abs x < inverse (hypreal_of_posnat n)}";
  13.175 +     "Infinitesimal = {x. ALL n. abs x < inverse (hypreal_of_nat (Suc n))}";
  13.176  by (auto_tac (claset(), simpset() addsimps [lemma_Infinitesimal2]));
  13.177 -qed "Infinitesimal_hypreal_of_posnat_iff";
  13.178 +qed "Infinitesimal_hypreal_of_nat_iff";
  13.179 +
  13.180  
  13.181 -(*-----------------------------------------------------------------------------
  13.182 -       Actual proof that omega (whr) is an infinite number and 
  13.183 +(*---------------------------------------------------------------------------
  13.184 +       Proof that omega (whr) is an infinite number and 
  13.185         hence that epsilon (ehr) is an infinitesimal number.
  13.186 - -----------------------------------------------------------------------------*)
  13.187 + ---------------------------------------------------------------------------*)
  13.188  Goal "{n. n < Suc m} = {n. n < m} Un {n. n = m}";
  13.189  by (auto_tac (claset(), simpset() addsimps [less_Suc_eq]));
  13.190  qed "Suc_Un_eq";
  13.191 @@ -2024,72 +1999,85 @@
  13.192  by (auto_tac (claset(), simpset() addsimps [Suc_Un_eq]));
  13.193  qed "finite_nat_segment";
  13.194  
  13.195 -Goal "finite {n::nat. real_of_posnat n < real_of_posnat m}";
  13.196 +Goal "finite {n::nat. real_of_nat n < real_of_nat m}";
  13.197  by (auto_tac (claset() addIs [finite_nat_segment], simpset()));
  13.198 -qed "finite_real_of_posnat_segment";
  13.199 +qed "finite_real_of_nat_segment";
  13.200  
  13.201 -Goal "finite {n. real_of_posnat n < u}";
  13.202 +Goal "finite {n. real_of_nat n < u}";
  13.203  by (cut_inst_tac [("x","u")] reals_Archimedean2 1);
  13.204  by (Step_tac 1);
  13.205 -by (rtac (finite_real_of_posnat_segment RSN (2,finite_subset)) 1);
  13.206 +by (rtac (finite_real_of_nat_segment RSN (2,finite_subset)) 1);
  13.207  by (auto_tac (claset() addDs [order_less_trans], simpset()));
  13.208 -qed "finite_real_of_posnat_less_real";
  13.209 +qed "finite_real_of_nat_less_real";
  13.210  
  13.211 -Goal "{n. real_of_posnat n <= u} = \
  13.212 -\     {n. real_of_posnat n < u} Un {n. u = real_of_posnat n}";
  13.213 +Goal "{n. f n <= u} = {n. f n < u} Un {n. u = (f n :: real)}";
  13.214  by (auto_tac (claset() addDs [order_le_imp_less_or_eq],
  13.215                simpset() addsimps [order_less_imp_le]));
  13.216  qed "lemma_real_le_Un_eq";
  13.217  
  13.218 -Goal "finite {n. real_of_posnat n <= u}";
  13.219 -by (auto_tac (claset(), simpset() addsimps 
  13.220 -    [lemma_real_le_Un_eq,lemma_finite_omega_set,
  13.221 -     finite_real_of_posnat_less_real]));
  13.222 -qed "finite_real_of_posnat_le_real";
  13.223 +Goal "finite {n. real_of_nat n <= u}";
  13.224 +by (auto_tac (claset(), 
  13.225 +              simpset() addsimps [lemma_real_le_Un_eq,lemma_finite_omega_set, 
  13.226 +                                  finite_real_of_nat_less_real]));
  13.227 +qed "finite_real_of_nat_le_real";
  13.228  
  13.229 -Goal "finite {n. abs(real_of_posnat n) <= u}";
  13.230 -by (full_simp_tac (simpset() addsimps [rename_numerals 
  13.231 -    real_of_posnat_gt_zero,abs_eqI2,
  13.232 -    finite_real_of_posnat_le_real]) 1);
  13.233 -qed "finite_rabs_real_of_posnat_le_real";
  13.234 +Goal "finite {n. abs(real_of_nat n) <= u}";
  13.235 +by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero,
  13.236 +                                  finite_real_of_nat_le_real]) 1);
  13.237 +qed "finite_rabs_real_of_nat_le_real";
  13.238  
  13.239 -Goal "{n. abs(real_of_posnat n) <= u} ~: FreeUltrafilterNat";
  13.240 +Goal "{n. abs(real_of_nat n) <= u} ~: FreeUltrafilterNat";
  13.241  by (blast_tac (claset() addSIs [FreeUltrafilterNat_finite,
  13.242 -    finite_rabs_real_of_posnat_le_real]) 1);
  13.243 -qed "rabs_real_of_posnat_le_real_FreeUltrafilterNat";
  13.244 +                                finite_rabs_real_of_nat_le_real]) 1);
  13.245 +qed "rabs_real_of_nat_le_real_FreeUltrafilterNat";
  13.246  
  13.247 -Goal "{n. u < real_of_posnat n} : FreeUltrafilterNat";
  13.248 +Goal "{n. u < real_of_nat n} : FreeUltrafilterNat";
  13.249  by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1);
  13.250 -by (auto_tac (claset(), simpset() addsimps 
  13.251 -    [CLAIM_SIMP "- {n. u < real_of_posnat  n} = \
  13.252 -\                {n. real_of_posnat n <= u}" 
  13.253 -     [real_le_def],finite_real_of_posnat_le_real 
  13.254 -                   RS FreeUltrafilterNat_finite]));
  13.255 +by (subgoal_tac "- {n. u < real_of_nat n} = {n. real_of_nat n <= u}" 1);
  13.256 +by (Force_tac 2); 
  13.257 +by (asm_full_simp_tac (simpset() addsimps
  13.258 +        [finite_real_of_nat_le_real RS FreeUltrafilterNat_finite]) 1); 
  13.259  qed "FreeUltrafilterNat_nat_gt_real";
  13.260  
  13.261  (*--------------------------------------------------------------
  13.262 - The complement of {n. abs(real_of_posnat n) <= u} = 
  13.263 - {n. u < abs (real_of_posnat n)} is in FreeUltrafilterNat 
  13.264 + The complement of {n. abs(real_of_nat n) <= u} = 
  13.265 + {n. u < abs (real_of_nat n)} is in FreeUltrafilterNat 
  13.266   by property of (free) ultrafilters
  13.267   --------------------------------------------------------------*)
  13.268 -Goal "- {n. abs (real_of_posnat  n) <= u} = \
  13.269 -\     {n. u < abs (real_of_posnat  n)}";
  13.270 +Goal "- {n. real_of_nat n <= u} = {n. u < real_of_nat n}";
  13.271  by (auto_tac (claset() addSDs [order_le_less_trans],
  13.272                simpset() addsimps [not_real_leE]));
  13.273  val lemma = result();
  13.274  
  13.275 -Goal "{n. u < abs (real_of_posnat n)} : FreeUltrafilterNat";
  13.276 -by (cut_inst_tac [("u","u")] rabs_real_of_posnat_le_real_FreeUltrafilterNat 1);
  13.277 +Goal "{n. u < abs (real_of_nat n)} : FreeUltrafilterNat";
  13.278 +by (cut_inst_tac [("u","u")] rabs_real_of_nat_le_real_FreeUltrafilterNat 1);
  13.279  by (auto_tac (claset() addDs [FreeUltrafilterNat_Compl_mem],
  13.280 -    simpset() addsimps [lemma]));
  13.281 +              simpset() addsimps [lemma]));
  13.282  qed "FreeUltrafilterNat_omega";
  13.283  
  13.284  (*-----------------------------------------------
  13.285         Omega is a member of HInfinite
  13.286   -----------------------------------------------*)
  13.287 +
  13.288 +Goal "hyprel^^{%n::nat. real_of_nat (Suc n)} : hypreal";
  13.289 +by Auto_tac;
  13.290 +qed "hypreal_omega";
  13.291 +
  13.292 +
  13.293 +Goal "{n. u < real_of_nat n} : FreeUltrafilterNat";
  13.294 +by (cut_inst_tac [("u","u")] rabs_real_of_nat_le_real_FreeUltrafilterNat 1);
  13.295 +by (auto_tac (claset() addDs [FreeUltrafilterNat_Compl_mem],
  13.296 +              simpset() addsimps [lemma]));
  13.297 +qed "FreeUltrafilterNat_omega";
  13.298 +
  13.299  Goalw [omega_def] "whr: HInfinite";
  13.300 -by (auto_tac (claset() addSIs [FreeUltrafilterNat_HInfinite,
  13.301 -    lemma_hyprel_refl,FreeUltrafilterNat_omega], simpset()));
  13.302 +by (auto_tac (claset() addSIs [FreeUltrafilterNat_HInfinite], 
  13.303 +              simpset()));
  13.304 +by (rtac bexI 1); 
  13.305 +by (rtac lemma_hyprel_refl 2); 
  13.306 +by Auto_tac;  
  13.307 +by (simp_tac (simpset() addsimps [real_of_nat_Suc, real_diff_less_eq RS sym, 
  13.308 +                                  FreeUltrafilterNat_omega]) 1); 
  13.309  qed "HInfinite_omega";
  13.310  
  13.311  (*-----------------------------------------------
  13.312 @@ -2118,48 +2106,75 @@
  13.313    that ALL n. |X n - a| < 1/n. Used in proof of NSLIM => LIM.
  13.314   -----------------------------------------------------------------------*)
  13.315  
  13.316 -Goal "#0 < u ==> finite {n. u < inverse(real_of_posnat n)}";
  13.317 -by (asm_simp_tac (simpset() addsimps [real_of_posnat_less_inverse_iff]) 1);
  13.318 -by (rtac finite_real_of_posnat_less_real 1);
  13.319 +Goal "0 < u  ==> \
  13.320 +\     (u < inverse (real_of_nat(Suc n))) = (real_of_nat(Suc n) < inverse u)";
  13.321 +by (asm_full_simp_tac (simpset() addsimps [real_inverse_eq_divide]) 1);
  13.322 +by (stac pos_real_less_divide_eq 1); 
  13.323 +by (assume_tac 1); 
  13.324 +by (stac pos_real_less_divide_eq 1); 
  13.325 +by (simp_tac (simpset() addsimps [real_mult_commute]) 2); 
  13.326 +by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero]) 1); 
  13.327 +qed "real_of_nat_less_inverse_iff";
  13.328 +
  13.329 +Goal "#0 < u ==> finite {n. u < inverse(real_of_nat(Suc n))}";
  13.330 +by (asm_simp_tac (simpset() addsimps [real_of_nat_less_inverse_iff]) 1);
  13.331 +by (asm_simp_tac (simpset() addsimps [real_of_nat_Suc, 
  13.332 +                         real_less_diff_eq RS sym]) 1); 
  13.333 +by (rtac finite_real_of_nat_less_real 1);
  13.334  qed "finite_inverse_real_of_posnat_gt_real";
  13.335  
  13.336 -Goal "{n. u <= inverse(real_of_posnat n)} = \
  13.337 -\    {n. u < inverse(real_of_posnat n)} Un {n. u = inverse(real_of_posnat n)}";
  13.338 +Goal "{n. u <= inverse(real_of_nat(Suc n))} = \
  13.339 +\    {n. u < inverse(real_of_nat(Suc n))} Un {n. u = inverse(real_of_nat(Suc n))}";
  13.340  by (auto_tac (claset() addDs [order_le_imp_less_or_eq],
  13.341                simpset() addsimps [order_less_imp_le]));
  13.342  qed "lemma_real_le_Un_eq2";
  13.343  
  13.344 -Goal "#0 < u ==> finite {n::nat. u = inverse(real_of_posnat  n)}";
  13.345 -by (asm_simp_tac (simpset() addsimps [real_of_posnat_inverse_eq_iff]) 1);
  13.346 -by (auto_tac (claset() addIs [lemma_finite_omega_set RSN 
  13.347 -    (2,finite_subset)], simpset()));
  13.348 +Goal "(inverse (real_of_nat(Suc n)) <= r) = (#1 <= r * real_of_nat(Suc n))";
  13.349 +by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 
  13.350 +by (simp_tac (simpset() addsimps [real_inverse_eq_divide]) 1);
  13.351 +by (stac pos_real_less_divide_eq 1); 
  13.352 +by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero]) 1); 
  13.353 +by (simp_tac (simpset() addsimps [real_mult_commute]) 1); 
  13.354 +qed "real_of_nat_inverse_le_iff";
  13.355 +
  13.356 +Goal "(u = inverse (real_of_nat(Suc n))) = (real_of_nat(Suc n) = inverse u)";
  13.357 +by (auto_tac (claset(),
  13.358 +      simpset() addsimps [real_inverse_inverse, real_of_nat_Suc_gt_zero, 
  13.359 +			  real_not_refl2 RS not_sym]));
  13.360 +qed "real_of_nat_inverse_eq_iff";
  13.361 +
  13.362 +Goal "finite {n::nat. u = inverse(real_of_nat(Suc n))}";
  13.363 +by (asm_simp_tac (simpset() addsimps [real_of_nat_inverse_eq_iff]) 1);
  13.364 +by (cut_inst_tac [("x","inverse u - #1")] lemma_finite_omega_set 1);
  13.365 +by (asm_full_simp_tac (simpset() addsimps [real_of_nat_Suc, 
  13.366 +                         real_diff_eq_eq RS sym, eq_commute]) 1); 
  13.367  qed "lemma_finite_omega_set2";
  13.368  
  13.369 -Goal "#0 < u ==> finite {n. u <= inverse(real_of_posnat n)}";
  13.370 +Goal "#0 < u ==> finite {n. u <= inverse(real_of_nat(Suc n))}";
  13.371  by (auto_tac (claset(), 
  13.372        simpset() addsimps [lemma_real_le_Un_eq2,lemma_finite_omega_set2,
  13.373                            finite_inverse_real_of_posnat_gt_real]));
  13.374  qed "finite_inverse_real_of_posnat_ge_real";
  13.375  
  13.376  Goal "#0 < u ==> \
  13.377 -\    {n. u <= inverse(real_of_posnat n)} ~: FreeUltrafilterNat";
  13.378 +\      {n. u <= inverse(real_of_nat(Suc n))} ~: FreeUltrafilterNat";
  13.379  by (blast_tac (claset() addSIs [FreeUltrafilterNat_finite,
  13.380                                  finite_inverse_real_of_posnat_ge_real]) 1);
  13.381  qed "inverse_real_of_posnat_ge_real_FreeUltrafilterNat";
  13.382  
  13.383  (*--------------------------------------------------------------
  13.384 -    The complement of  {n. u <= inverse(real_of_posnat n)} =
  13.385 -    {n. inverse(real_of_posnat n) < u} is in FreeUltrafilterNat 
  13.386 +    The complement of  {n. u <= inverse(real_of_nat(Suc n))} =
  13.387 +    {n. inverse(real_of_nat(Suc n)) < u} is in FreeUltrafilterNat 
  13.388      by property of (free) ultrafilters
  13.389   --------------------------------------------------------------*)
  13.390 -Goal "- {n. u <= inverse(real_of_posnat n)} = \
  13.391 -\     {n. inverse(real_of_posnat n) < u}";
  13.392 +Goal "- {n. u <= inverse(real_of_nat(Suc n))} = \
  13.393 +\     {n. inverse(real_of_nat(Suc n)) < u}";
  13.394  by (auto_tac (claset() addSDs [order_le_less_trans],
  13.395                simpset() addsimps [not_real_leE]));
  13.396  val lemma = result();
  13.397  
  13.398  Goal "#0 < u ==> \
  13.399 -\     {n. inverse(real_of_posnat n) < u} : FreeUltrafilterNat";
  13.400 +\     {n. inverse(real_of_nat(Suc n)) < u} : FreeUltrafilterNat";
  13.401  by (cut_inst_tac [("u","u")]  inverse_real_of_posnat_ge_real_FreeUltrafilterNat 1);
  13.402  by (auto_tac (claset() addDs [FreeUltrafilterNat_Compl_mem],
  13.403      simpset() addsimps [lemma]));
  13.404 @@ -2176,7 +2191,7 @@
  13.405  (*-----------------------------------------------------
  13.406      |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x|: Infinitesimal 
  13.407   -----------------------------------------------------*)
  13.408 -Goal "ALL n. abs(X n + -x) < inverse(real_of_posnat n) \ 
  13.409 +Goal "ALL n. abs(X n + -x) < inverse(real_of_nat(Suc n)) \ 
  13.410  \    ==> Abs_hypreal(hyprel^^{X}) + -hypreal_of_real x : Infinitesimal";
  13.411  by (auto_tac (claset() addSIs [bexI] 
  13.412             addDs [rename_numerals FreeUltrafilterNat_inverse_real_of_posnat,
  13.413 @@ -2184,24 +2199,23 @@
  13.414             addIs [order_less_trans, FreeUltrafilterNat_subset],
  13.415        simpset() addsimps [hypreal_minus, 
  13.416                            hypreal_of_real_def,hypreal_add,
  13.417 -                          Infinitesimal_FreeUltrafilterNat_iff,hypreal_inverse,
  13.418 -                          hypreal_of_real_of_posnat]));
  13.419 +                      Infinitesimal_FreeUltrafilterNat_iff,hypreal_inverse]));
  13.420  qed "real_seq_to_hypreal_Infinitesimal";
  13.421  
  13.422 -Goal "ALL n. abs(X n + -x) < inverse(real_of_posnat n) \ 
  13.423 +Goal "ALL n. abs(X n + -x) < inverse(real_of_nat(Suc n)) \ 
  13.424  \     ==> Abs_hypreal(hyprel^^{X}) @= hypreal_of_real x";
  13.425  by (rtac (inf_close_minus_iff RS ssubst) 1);
  13.426  by (rtac (mem_infmal_iff RS subst) 1);
  13.427  by (etac real_seq_to_hypreal_Infinitesimal 1);
  13.428  qed "real_seq_to_hypreal_inf_close";
  13.429  
  13.430 -Goal "ALL n. abs(x + -X n) < inverse(real_of_posnat n) \ 
  13.431 +Goal "ALL n. abs(x + -X n) < inverse(real_of_nat(Suc n)) \ 
  13.432  \              ==> Abs_hypreal(hyprel^^{X}) @= hypreal_of_real x";
  13.433  by (asm_full_simp_tac (simpset() addsimps [abs_minus_add_cancel,
  13.434          real_seq_to_hypreal_inf_close]) 1);
  13.435  qed "real_seq_to_hypreal_inf_close2";
  13.436  
  13.437 -Goal "ALL n. abs(X n + -Y n) < inverse(real_of_posnat n) \ 
  13.438 +Goal "ALL n. abs(X n + -Y n) < inverse(real_of_nat(Suc n)) \ 
  13.439  \     ==> Abs_hypreal(hyprel^^{X}) + \
  13.440  \         -Abs_hypreal(hyprel^^{Y}) : Infinitesimal";
  13.441  by (auto_tac (claset() addSIs [bexI] 
  13.442 @@ -2211,5 +2225,5 @@
  13.443          addIs [order_less_trans, FreeUltrafilterNat_subset],
  13.444       simpset() addsimps 
  13.445              [Infinitesimal_FreeUltrafilterNat_iff,hypreal_minus,hypreal_add, 
  13.446 -             hypreal_inverse,hypreal_of_real_of_posnat]));
  13.447 +             hypreal_inverse]));
  13.448  qed "real_seq_to_hypreal_Infinitesimal2";
    14.1 --- a/src/HOL/Hyperreal/NatStar.ML	Thu Jan 04 10:22:33 2001 +0100
    14.2 +++ b/src/HOL/Hyperreal/NatStar.ML	Thu Jan 04 10:23:01 2001 +0100
    14.3 @@ -122,13 +122,13 @@
    14.4  by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
    14.5  qed "NatStar_hypreal_of_real_image_subset";
    14.6  
    14.7 -Goal "SHNat <= *sNat* (UNIV:: nat set)";
    14.8 +Goal "SNat <= *sNat* (UNIV:: nat set)";
    14.9  by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_iff,
   14.10 -    NatStar_hypreal_of_real_image_subset]) 1);
   14.11 +                          NatStar_hypreal_of_real_image_subset]) 1);
   14.12  qed "NatStar_SHNat_subset";
   14.13  
   14.14  Goalw [starsetNat_def] 
   14.15 -      "*sNat* X Int SHNat = hypnat_of_nat `` X";
   14.16 +     "*sNat* X Int SNat = hypnat_of_nat `` X";
   14.17  by (auto_tac (claset(),
   14.18           simpset() addsimps 
   14.19             [hypnat_of_nat_def,SHNat_def]));
    15.1 --- a/src/HOL/Hyperreal/NatStar.thy	Thu Jan 04 10:22:33 2001 +0100
    15.2 +++ b/src/HOL/Hyperreal/NatStar.thy	Thu Jan 04 10:23:01 2001 +0100
    15.3 @@ -5,7 +5,7 @@
    15.4                    sets of reals, and nat=>real, nat=>nat functions
    15.5  *) 
    15.6  
    15.7 -NatStar = HyperNat + RealPow + HyperPow + 
    15.8 +NatStar = RealPow + HyperPow + 
    15.9  
   15.10  constdefs
   15.11  
    16.1 --- a/src/HOL/Hyperreal/SEQ.ML	Thu Jan 04 10:22:33 2001 +0100
    16.2 +++ b/src/HOL/Hyperreal/SEQ.ML	Thu Jan 04 10:23:01 2001 +0100
    16.3 @@ -11,14 +11,13 @@
    16.4   -------------------------------------------------------------------------- *)
    16.5  
    16.6  Goalw [hypnat_omega_def] 
    16.7 -      "(*fNat* (%n::nat. inverse(real_of_posnat n))) whn : Infinitesimal";
    16.8 +      "(*fNat* (%n::nat. inverse(real_of_nat(Suc n)))) whn : Infinitesimal";
    16.9  by (auto_tac (claset(),
   16.10        simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff,starfunNat]));
   16.11  by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
   16.12  by (auto_tac (claset(),
   16.13 -       simpset() addsimps (map rename_numerals) 
   16.14 -         [real_of_posnat_gt_zero,real_inverse_gt_zero,abs_eqI2,
   16.15 -          FreeUltrafilterNat_inverse_real_of_posnat]));
   16.16 +              simpset() addsimps [real_of_nat_Suc_gt_zero, abs_eqI2,
   16.17 +                            FreeUltrafilterNat_inverse_real_of_posnat]));
   16.18  qed "SEQ_Infinitesimal";
   16.19  
   16.20  (*--------------------------------------------------------------------------
   16.21 @@ -423,45 +422,46 @@
   16.22  qed "BseqI";
   16.23  
   16.24  Goal "(EX K. #0 < K & (ALL n. abs(X n) <= K)) = \
   16.25 -\         (EX N. ALL n. abs(X n) <= real_of_posnat N)";
   16.26 -by (auto_tac (claset(),simpset() addsimps 
   16.27 -    (map rename_numerals) [real_gt_zero_preal_Ex,real_of_posnat_gt_zero]));
   16.28 -by (cut_inst_tac [("x","real_of_preal y")] reals_Archimedean2 1);
   16.29 -by (blast_tac (claset() addIs [order_le_less_trans, order_less_imp_le]) 1);
   16.30 -by (auto_tac (claset(),simpset() addsimps [real_of_posnat_def]));
   16.31 +\     (EX N. ALL n. abs(X n) <= real_of_nat(Suc N))";
   16.32 +by Auto_tac;
   16.33 +by (Force_tac 2); 
   16.34 +by (cut_inst_tac [("x","K")] reals_Archimedean2 1);
   16.35 +by (Clarify_tac 1); 
   16.36 +by (res_inst_tac [("x","n")] exI 1); 
   16.37 +by (Clarify_tac 1); 
   16.38 +by (dres_inst_tac [("x","na")] spec 1); 
   16.39 +by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));  
   16.40  qed "lemma_NBseq_def";
   16.41  
   16.42  (* alternative definition for Bseq *)
   16.43 -Goalw [Bseq_def] 
   16.44 -      "Bseq X = (EX N. ALL n. abs(X n) <= real_of_posnat N)";
   16.45 +Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) <= real_of_nat(Suc N))";
   16.46  by (simp_tac (simpset() addsimps [lemma_NBseq_def]) 1);
   16.47  qed "Bseq_iff";
   16.48  
   16.49  Goal "(EX K. #0 < K & (ALL n. abs(X n) <= K)) = \
   16.50 -\     (EX N. ALL n. abs(X n) < real_of_posnat N)";
   16.51 -by (auto_tac (claset(),simpset() addsimps 
   16.52 -    (map rename_numerals) [real_gt_zero_preal_Ex,real_of_posnat_gt_zero]));
   16.53 -by (cut_inst_tac [("x","real_of_preal y")] reals_Archimedean2 1);
   16.54 -by (blast_tac (claset() addIs [order_less_trans, order_le_less_trans]) 1);
   16.55 -by (auto_tac (claset() addIs [order_less_imp_le],
   16.56 -              simpset() addsimps [real_of_posnat_def]));
   16.57 +\     (EX N. ALL n. abs(X n) < real_of_nat(Suc N))";
   16.58 +by (stac lemma_NBseq_def 1); 
   16.59 +by Auto_tac;
   16.60 +by (res_inst_tac [("x","Suc N")] exI 1); 
   16.61 +by (res_inst_tac [("x","N")] exI 2); 
   16.62 +by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));  
   16.63 +by (blast_tac (claset() addIs [order_less_imp_le]) 2);
   16.64 +by (dres_inst_tac [("x","n")] spec 1); 
   16.65 +by (Asm_simp_tac 1); 
   16.66  qed "lemma_NBseq_def2";
   16.67  
   16.68  (* yet another definition for Bseq *)
   16.69 -Goalw [Bseq_def] 
   16.70 -      "Bseq X = (EX N. ALL n. abs(X n) < real_of_posnat N)";
   16.71 +Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) < real_of_nat(Suc N))";
   16.72  by (simp_tac (simpset() addsimps [lemma_NBseq_def2]) 1);
   16.73  qed "Bseq_iff1a";
   16.74  
   16.75  Goalw [NSBseq_def]
   16.76 -      "[| NSBseq X; N: HNatInfinite |] \
   16.77 -\           ==> (*fNat* X) N : HFinite";
   16.78 +     "[| NSBseq X;  N: HNatInfinite |] ==> (*fNat* X) N : HFinite";
   16.79  by (Blast_tac 1);
   16.80  qed "NSBseqD";
   16.81  
   16.82  Goalw [NSBseq_def]
   16.83 -      "ALL N: HNatInfinite. (*fNat* X) N : HFinite \
   16.84 -\           ==> NSBseq X";
   16.85 +     "ALL N: HNatInfinite. (*fNat* X) N : HFinite ==> NSBseq X";
   16.86  by (assume_tac 1);
   16.87  qed "NSBseqI";
   16.88  
   16.89 @@ -469,17 +469,16 @@
   16.90         Standard definition ==> NS definition
   16.91   ----------------------------------------------------------*)
   16.92  (* a few lemmas *)
   16.93 -Goal "ALL n. abs(X n) <= K ==> \
   16.94 -\     ALL n. abs(X((f::nat=>nat) n)) <= K";
   16.95 +Goal "ALL n. abs(X n) <= K ==> ALL n. abs(X((f::nat=>nat) n)) <= K";
   16.96  by (Auto_tac);
   16.97  val lemma_Bseq = result();
   16.98  
   16.99  Goalw [Bseq_def,NSBseq_def] "Bseq X ==> NSBseq X";
  16.100  by (Step_tac 1);
  16.101  by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
  16.102 -by (auto_tac (claset(),simpset() addsimps [starfunNat,    
  16.103 -    HFinite_FreeUltrafilterNat_iff,
  16.104 -    HNatInfinite_FreeUltrafilterNat_iff]));
  16.105 +by (auto_tac (claset(),
  16.106 +              simpset() addsimps [starfunNat, HFinite_FreeUltrafilterNat_iff,
  16.107 +                                  HNatInfinite_FreeUltrafilterNat_iff]));
  16.108  by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2]);
  16.109  by (dres_inst_tac [("f","Xa")] lemma_Bseq 1); 
  16.110  by (res_inst_tac [("x","K+#1")] exI 1);
  16.111 @@ -500,79 +499,77 @@
  16.112   -------------------------------------------------------------------*)
  16.113   
  16.114  Goal "ALL K. #0 < K --> (EX n. K < abs (X n)) \
  16.115 -\          ==> ALL N. EX n. real_of_posnat  N < abs (X n)";
  16.116 +\          ==> ALL N. EX n. real_of_nat(Suc N) < abs (X n)";
  16.117  by (Step_tac 1);
  16.118 -by (cut_inst_tac [("n","N")] (rename_numerals real_of_posnat_gt_zero) 1);
  16.119 +by (cut_inst_tac [("n","N")] real_of_nat_Suc_gt_zero 1);
  16.120  by (Blast_tac 1);
  16.121  val lemmaNSBseq = result();
  16.122  
  16.123  Goal "ALL K. #0 < K --> (EX n. K < abs (X n)) \
  16.124 -\         ==> EX f. ALL N. real_of_posnat  N < abs (X (f N))";
  16.125 +\         ==> EX f. ALL N. real_of_nat(Suc N) < abs (X (f N))";
  16.126  by (dtac lemmaNSBseq 1);
  16.127  by (dtac choice 1);
  16.128  by (Blast_tac 1);
  16.129  val lemmaNSBseq2 = result();
  16.130  
  16.131 -Goal "ALL N. real_of_posnat  N < abs (X (f N)) \
  16.132 +Goal "ALL N. real_of_nat(Suc N) < abs (X (f N)) \
  16.133  \         ==>  Abs_hypreal(hyprel^^{X o f}) : HInfinite";
  16.134 -by (auto_tac (claset(),simpset() addsimps 
  16.135 -    [HInfinite_FreeUltrafilterNat_iff,o_def]));
  16.136 -by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, 
  16.137 -    Step_tac 1]);
  16.138 +by (auto_tac (claset(),
  16.139 +              simpset() addsimps [HInfinite_FreeUltrafilterNat_iff,o_def]));
  16.140 +by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]);
  16.141  by (cut_inst_tac [("u","u")] FreeUltrafilterNat_nat_gt_real 1);
  16.142 -by (blast_tac (claset() addDs [FreeUltrafilterNat_all, FreeUltrafilterNat_Int] 
  16.143 -                        addIs [order_less_trans, FreeUltrafilterNat_subset]) 1);
  16.144 +by (dtac FreeUltrafilterNat_all 1);
  16.145 +by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1); 
  16.146 +by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));  
  16.147  qed "real_seq_to_hypreal_HInfinite";
  16.148  
  16.149 -(*--------------------------------------------------------------------------------
  16.150 +(*-----------------------------------------------------------------------------
  16.151       Now prove that we can get out an infinite hypernatural as well 
  16.152       defined using the skolem function f::nat=>nat above
  16.153 - --------------------------------------------------------------------------------*)
  16.154 + ----------------------------------------------------------------------------*)
  16.155  
  16.156 -Goal "{n. f n <= Suc u & real_of_posnat  n < abs (X (f n))} <= \
  16.157 -\         {n. f n <= u & real_of_posnat  n < abs (X (f n))} \
  16.158 -\         Un {n. real_of_posnat n < abs (X (Suc u))}";
  16.159 -by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_imp_le],
  16.160 -    simpset() addsimps [less_Suc_eq]));
  16.161 +Goal "{n. f n <= Suc u & real_of_nat(Suc n) < abs (X (f n))} <= \
  16.162 +\         {n. f n <= u & real_of_nat(Suc n) < abs (X (f n))} \
  16.163 +\         Un {n. real_of_nat(Suc n) < abs (X (Suc u))}";
  16.164 +by (auto_tac (claset() addSDs [le_imp_less_or_eq], simpset()));
  16.165  val lemma_finite_NSBseq = result();
  16.166  
  16.167 -Goal "finite {n. f n <= (u::nat) &  real_of_posnat n < abs(X(f n))}";
  16.168 +Goal "finite {n. f n <= (u::nat) &  real_of_nat(Suc n) < abs(X(f n))}";
  16.169  by (induct_tac "u" 1);
  16.170 -by (rtac (CLAIM "{n. f n <= (0::nat) & real_of_posnat n < abs (X (f n))} <= \
  16.171 -\         {n. real_of_posnat n < abs (X 0)}"
  16.172 -          RS finite_subset) 1);
  16.173 -by (rtac finite_real_of_posnat_less_real 1);
  16.174 -by (rtac (lemma_finite_NSBseq RS finite_subset) 1);
  16.175 -by (auto_tac (claset() addIs [finite_real_of_posnat_less_real], simpset()));
  16.176 +by (res_inst_tac [("B","{n. real_of_nat(Suc n) < abs(X 0)}")] finite_subset 1);
  16.177 +by (Force_tac 1); 
  16.178 +by (rtac (lemma_finite_NSBseq RS finite_subset) 2);
  16.179 +by (auto_tac (claset() addIs [finite_real_of_nat_less_real], 
  16.180 +              simpset() addsimps [real_of_nat_Suc, real_less_diff_eq RS sym]));
  16.181  val lemma_finite_NSBseq2 = result();
  16.182  
  16.183 -Goal "ALL N. real_of_posnat  N < abs (X (f N)) \
  16.184 +Goal "ALL N. real_of_nat(Suc N) < abs (X (f N)) \
  16.185  \     ==> Abs_hypnat(hypnatrel^^{f}) : HNatInfinite";
  16.186 -by (auto_tac (claset(),simpset() addsimps 
  16.187 -    [HNatInfinite_FreeUltrafilterNat_iff]));
  16.188 -by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, 
  16.189 -    Step_tac 1]);
  16.190 +by (auto_tac (claset(),
  16.191 +              simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
  16.192 +by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]);
  16.193  by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1);
  16.194  by (asm_full_simp_tac (simpset() addsimps 
  16.195     [CLAIM_SIMP "- {n. u < (f::nat=>nat) n} \
  16.196  \   = {n. f n <= u}" [le_def]]) 1);
  16.197  by (dtac FreeUltrafilterNat_all 1);
  16.198  by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
  16.199 -by (auto_tac (claset(),simpset() addsimps 
  16.200 -    [CLAIM "({n. f n <= u} Int {n. real_of_posnat n < abs(X(f n))}) = \
  16.201 -\          {n. f n <= (u::nat) &  real_of_posnat n < abs(X(f n))}",
  16.202 +by (auto_tac (claset(), 
  16.203 +     simpset() addsimps 
  16.204 +    [CLAIM "({n. f n <= u} Int {n. real_of_nat(Suc n) < abs(X(f n))}) = \
  16.205 +\          {n. f n <= (u::nat) &  real_of_nat(Suc n) < abs(X(f n))}",
  16.206       lemma_finite_NSBseq2 RS FreeUltrafilterNat_finite]));
  16.207  qed "HNatInfinite_skolem_f";
  16.208  
  16.209  Goalw [Bseq_def,NSBseq_def] 
  16.210        "NSBseq X ==> Bseq X";
  16.211  by (rtac ccontr 1);
  16.212 -by (auto_tac (claset(),simpset() addsimps [real_le_def]));
  16.213 +by (auto_tac (claset(), simpset() addsimps [real_le_def]));
  16.214  by (dtac lemmaNSBseq2 1 THEN Step_tac 1);
  16.215  by (forw_inst_tac [("X","X"),("f","f")] real_seq_to_hypreal_HInfinite 1);
  16.216  by (dtac (HNatInfinite_skolem_f RSN (2,bspec)) 1 THEN assume_tac 1);
  16.217 -by (auto_tac (claset(),simpset() addsimps [starfunNat,
  16.218 -    o_def,HFinite_HInfinite_iff]));
  16.219 +by (auto_tac (claset(), 
  16.220 +              simpset() addsimps [starfunNat, o_def,HFinite_HInfinite_iff]));
  16.221  qed "NSBseq_Bseq";
  16.222  
  16.223  (*----------------------------------------------------------------------
  16.224 @@ -805,7 +802,7 @@
  16.225  by (auto_tac (claset(),
  16.226                simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
  16.227  by (dres_inst_tac [("x","M")] spec 1);
  16.228 -by (ultra_tac (claset(),simpset() addsimps [less_imp_le]) 1);
  16.229 +by (ultra_tac (claset(), simpset() addsimps [less_imp_le]) 1);
  16.230  val lemmaCauchy1 = result();
  16.231  
  16.232  Goal "{n. ALL m n. M <= m & M <= (n::nat) --> abs (X m + - X n) < u} Int \
  16.233 @@ -821,8 +818,9 @@
  16.234  by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
  16.235  by (rtac (inf_close_minus_iff RS iffD2) 1);
  16.236  by (rtac (mem_infmal_iff RS iffD1) 1);
  16.237 -by (auto_tac (claset(),simpset() addsimps [starfunNat,
  16.238 -    hypreal_minus,hypreal_add,Infinitesimal_FreeUltrafilterNat_iff]));
  16.239 +by (auto_tac (claset(),
  16.240 +              simpset() addsimps [starfunNat, hypreal_minus,hypreal_add,
  16.241 +                                  Infinitesimal_FreeUltrafilterNat_iff]));
  16.242  by (EVERY[rtac bexI 1, Auto_tac]);
  16.243  by (dtac spec 1 THEN Auto_tac);
  16.244  by (dres_inst_tac [("M","M")] lemmaCauchy1 1);
  16.245 @@ -841,17 +839,17 @@
  16.246  Goalw [Cauchy_def,NSCauchy_def] 
  16.247        "NSCauchy X ==> Cauchy X";
  16.248  by (EVERY1[Step_tac, rtac ccontr,Asm_full_simp_tac]);
  16.249 -by (dtac choice 1 THEN auto_tac (claset(),simpset() 
  16.250 -         addsimps [all_conj_distrib]));
  16.251 -by (dtac choice 1 THEN step_tac (claset() addSDs 
  16.252 -         [all_conj_distrib RS iffD1]) 1);
  16.253 +by (dtac choice 1 THEN 
  16.254 +    auto_tac (claset(), simpset() addsimps [all_conj_distrib]));
  16.255 +by (dtac choice 1 THEN 
  16.256 +    step_tac (claset() addSDs [all_conj_distrib RS iffD1]) 1);
  16.257  by (REPEAT(dtac HNatInfinite_NSLIMSEQ 1));
  16.258  by (dtac bspec 1 THEN assume_tac 1);
  16.259  by (dres_inst_tac [("x","Abs_hypnat (hypnatrel ^^ {fa})")] bspec 1 
  16.260 -    THEN auto_tac (claset(),simpset() addsimps [starfunNat]));
  16.261 +    THEN auto_tac (claset(), simpset() addsimps [starfunNat]));
  16.262  by (dtac (inf_close_minus_iff RS iffD1) 1);
  16.263  by (dtac (mem_infmal_iff RS iffD2) 1);
  16.264 -by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
  16.265 +by (auto_tac (claset(), simpset() addsimps [hypreal_minus,
  16.266      hypreal_add,Infinitesimal_FreeUltrafilterNat_iff]));
  16.267  by (dres_inst_tac [("x","e")] spec 1 THEN Auto_tac);
  16.268  by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
  16.269 @@ -1076,8 +1074,8 @@
  16.270  Goal "f ----NS> l ==> (%n. f(Suc n)) ----NS> l";
  16.271  by (forward_tac [NSconvergentI RS 
  16.272      (NSCauchy_NSconvergent_iff RS iffD2)] 1);
  16.273 -by (auto_tac (claset(),simpset() addsimps [NSCauchy_def,
  16.274 -    NSLIMSEQ_def,starfunNat_shift_one]));
  16.275 +by (auto_tac (claset(), 
  16.276 +     simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one]));
  16.277  by (dtac bspec 1 THEN assume_tac 1);
  16.278  by (dtac bspec 1 THEN assume_tac 1);
  16.279  by (dtac (SHNat_one RSN (2,HNatInfinite_SHNat_add)) 1);
  16.280 @@ -1093,8 +1091,8 @@
  16.281  Goal "(%n. f(Suc n)) ----NS> l ==> f ----NS> l";
  16.282  by (forward_tac [NSconvergentI RS 
  16.283      (NSCauchy_NSconvergent_iff RS iffD2)] 1);
  16.284 -by (auto_tac (claset(),simpset() addsimps [NSCauchy_def,
  16.285 -    NSLIMSEQ_def,starfunNat_shift_one]));
  16.286 +by (auto_tac (claset(),
  16.287 +      simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one]));
  16.288  by (dtac bspec 1 THEN assume_tac 1);
  16.289  by (dtac bspec 1 THEN assume_tac 1);
  16.290  by (ftac (SHNat_one RSN (2,HNatInfinite_SHNat_diff)) 1);
  16.291 @@ -1181,31 +1179,33 @@
  16.292  (*--------------------------------------------------------------
  16.293               Sequence  1/n --> 0 as n --> infinity 
  16.294   -------------------------------------------------------------*)
  16.295 -Goal "(%n. inverse(real_of_posnat n)) ----> #0";
  16.296 +
  16.297 +Goal "(%n. inverse(real_of_nat(Suc n))) ----> #0";
  16.298  by (rtac LIMSEQ_inverse_zero 1 THEN Step_tac 1);
  16.299  by (cut_inst_tac [("x","y")] reals_Archimedean2 1);
  16.300  by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
  16.301 -by (Step_tac 1 THEN etac (le_imp_less_or_eq RS disjE) 1);
  16.302 -by (dtac (real_of_posnat_less_iff RS iffD2) 1);
  16.303 -by (auto_tac (claset() addEs [order_less_trans], simpset()));
  16.304 -qed "LIMSEQ_inverse_real_of_posnat";
  16.305 +by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));  
  16.306 +by (subgoal_tac "y < real_of_nat na" 1);
  16.307 +by (Asm_simp_tac 1);
  16.308 +by (blast_tac (claset() addIs [order_less_le_trans]) 1);  
  16.309 +qed "LIMSEQ_inverse_real_of_nat";
  16.310  
  16.311 -Goal "(%n. inverse(real_of_posnat n)) ----NS> #0";
  16.312 +Goal "(%n. inverse(real_of_nat(Suc n))) ----NS> #0";
  16.313  by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
  16.314 -    LIMSEQ_inverse_real_of_posnat]) 1);
  16.315 -qed "NSLIMSEQ_inverse_real_of_posnat";
  16.316 +    LIMSEQ_inverse_real_of_nat]) 1);
  16.317 +qed "NSLIMSEQ_inverse_real_of_nat";
  16.318  
  16.319  (*--------------------------------------------
  16.320      Sequence  r + 1/n --> r as n --> infinity 
  16.321      now easily proved
  16.322   --------------------------------------------*)
  16.323 -Goal "(%n. r + inverse(real_of_posnat n)) ----> r";
  16.324 -by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_posnat]
  16.325 -    MRS LIMSEQ_add] 1);
  16.326 -by (Auto_tac);
  16.327 +Goal "(%n. r + inverse(real_of_nat(Suc n))) ----> r";
  16.328 +by (cut_facts_tac
  16.329 +    [ [LIMSEQ_const,LIMSEQ_inverse_real_of_nat] MRS LIMSEQ_add ] 1);
  16.330 +by Auto_tac;
  16.331  qed "LIMSEQ_inverse_real_of_posnat_add";
  16.332  
  16.333 -Goal "(%n. r + inverse(real_of_posnat n)) ----NS> r";
  16.334 +Goal "(%n. r + inverse(real_of_nat(Suc n))) ----NS> r";
  16.335  by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
  16.336      LIMSEQ_inverse_real_of_posnat_add]) 1);
  16.337  qed "NSLIMSEQ_inverse_real_of_posnat_add";
  16.338 @@ -1214,24 +1214,24 @@
  16.339      Also...
  16.340   --------------*)
  16.341  
  16.342 -Goal "(%n. r + -inverse(real_of_posnat n)) ----> r";
  16.343 -by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_posnat]
  16.344 -    MRS LIMSEQ_add_minus] 1);
  16.345 +Goal "(%n. r + -inverse(real_of_nat(Suc n))) ----> r";
  16.346 +by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_nat]
  16.347 +                   MRS LIMSEQ_add_minus] 1);
  16.348  by (Auto_tac);
  16.349  qed "LIMSEQ_inverse_real_of_posnat_add_minus";
  16.350  
  16.351 -Goal "(%n. r + -inverse(real_of_posnat n)) ----NS> r";
  16.352 +Goal "(%n. r + -inverse(real_of_nat(Suc n))) ----NS> r";
  16.353  by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
  16.354      LIMSEQ_inverse_real_of_posnat_add_minus]) 1);
  16.355  qed "NSLIMSEQ_inverse_real_of_posnat_add_minus";
  16.356  
  16.357 -Goal "(%n. r*( #1 + -inverse(real_of_posnat n))) ----> r";
  16.358 +Goal "(%n. r*( #1 + -inverse(real_of_nat(Suc n)))) ----> r";
  16.359  by (cut_inst_tac [("b","#1")] ([LIMSEQ_const,
  16.360      LIMSEQ_inverse_real_of_posnat_add_minus] MRS LIMSEQ_mult) 1);
  16.361  by (Auto_tac);
  16.362  qed "LIMSEQ_inverse_real_of_posnat_add_minus_mult";
  16.363  
  16.364 -Goal "(%n. r*( #1 + -inverse(real_of_posnat n))) ----NS> r";
  16.365 +Goal "(%n. r*( #1 + -inverse(real_of_nat(Suc n)))) ----NS> r";
  16.366  by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
  16.367      LIMSEQ_inverse_real_of_posnat_add_minus_mult]) 1);
  16.368  qed "NSLIMSEQ_inverse_real_of_posnat_add_minus_mult";
  16.369 @@ -1349,8 +1349,9 @@
  16.370        "X ----NS> #0 ==> Abs_hypreal(hyprel^^{X}) : Infinitesimal";
  16.371  by (dres_inst_tac [("x","whn")] bspec 1);
  16.372  by (simp_tac (simpset() addsimps [HNatInfinite_whn]) 1);
  16.373 -by (auto_tac (claset(),simpset() addsimps [hypnat_omega_def,
  16.374 -    mem_infmal_iff RS sym,starfunNat,hypreal_of_real_zero]));
  16.375 +by (auto_tac (claset(),
  16.376 +              simpset() addsimps [hypnat_omega_def, mem_infmal_iff RS sym,
  16.377 +                                  starfunNat,hypreal_of_real_zero]));
  16.378  qed "NSLIMSEQ_zero_Infinitesimal_hypreal";
  16.379  
  16.380  (***---------------------------------------------------------------
  16.381 @@ -1366,3 +1367,5 @@
  16.382  Goal "subseq f ==> n <= f(n)";
  16.383  Goal "subseq f ==> EX n. N1 <= n & N2 <= f(n)";
  16.384   ---------------------------------------------------------------***)
  16.385 +
  16.386 +
    17.1 --- a/src/HOL/Hyperreal/Series.ML	Thu Jan 04 10:22:33 2001 +0100
    17.2 +++ b/src/HOL/Hyperreal/Series.ML	Thu Jan 04 10:23:01 2001 +0100
    17.3 @@ -67,8 +67,9 @@
    17.4  
    17.5  Goal "sumr 0 n (%i. r) = real_of_nat n*r";
    17.6  by (induct_tac "n" 1);
    17.7 -by (auto_tac (claset(),simpset() addsimps 
    17.8 -    [real_add_mult_distrib,real_of_nat_zero]));
    17.9 +by (auto_tac (claset(),
   17.10 +              simpset() addsimps [real_add_mult_distrib,real_of_nat_zero,
   17.11 +                                  real_of_nat_Suc]));
   17.12  qed "sumr_const";
   17.13  Addsimps [sumr_const];
   17.14  
   17.15 @@ -118,10 +119,9 @@
   17.16  by (asm_full_simp_tac (simpset() addsimps [le_Suc_eq])  2);
   17.17  by (Step_tac 1);
   17.18  by (dres_inst_tac [("x","n")] spec 3);
   17.19 -by (auto_tac (claset() addSDs [le_imp_less_or_eq],
   17.20 -    simpset()));
   17.21 -by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib,
   17.22 -    Suc_diff_n]) 1);
   17.23 +by (auto_tac (claset() addSDs [le_imp_less_or_eq], simpset()));
   17.24 +by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib, Suc_diff_n,
   17.25 +                                      real_of_nat_Suc]) 1);
   17.26  qed_spec_mp "sumr_interval_const";
   17.27  
   17.28  Goal "(ALL n. m <= n --> f n = r) & m <= na \
   17.29 @@ -133,20 +133,14 @@
   17.30  by (dres_inst_tac [("x","n")] spec 3);
   17.31  by (auto_tac (claset() addSDs [le_imp_less_or_eq],
   17.32      simpset()));
   17.33 -by (asm_simp_tac (simpset() addsimps [Suc_diff_n,
   17.34 -    real_add_mult_distrib]) 1);
   17.35 +by (asm_simp_tac (simpset() addsimps [Suc_diff_n, real_add_mult_distrib,
   17.36 +                                      real_of_nat_Suc]) 1);
   17.37  qed_spec_mp "sumr_interval_const2";
   17.38  
   17.39 -Goal "(m <= n)= (m < Suc n)";
   17.40 -by (Auto_tac);
   17.41 -qed "le_eq_less_Suc";
   17.42 -
   17.43 -Goal "(ALL n. m <= n --> #0 <= f n) & m < na \
   17.44 -\                --> sumr 0 m f <= sumr 0 na f";
   17.45 -by (induct_tac "na" 1);
   17.46 +Goal "(ALL n. m <= n --> #0 <= f n) & m < k --> sumr 0 m f <= sumr 0 k f";
   17.47 +by (induct_tac "k" 1);
   17.48  by (Step_tac 1);
   17.49 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps 
   17.50 -    [le_eq_less_Suc RS sym])));
   17.51 +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [less_Suc_eq_le])));
   17.52  by (ALLGOALS(dres_inst_tac [("x","n")] spec));
   17.53  by (Step_tac 1);
   17.54  by (dtac le_imp_less_or_eq 1 THEN Step_tac 1);
   17.55 @@ -235,14 +229,14 @@
   17.56  \     --> (sumr m (m + n) f <= (real_of_nat n * K))";
   17.57  by (induct_tac "n" 1);
   17.58  by (auto_tac (claset() addIs [real_add_le_mono],
   17.59 -    simpset() addsimps [real_add_mult_distrib]));
   17.60 +              simpset() addsimps [real_add_mult_distrib, real_of_nat_Suc]));
   17.61  qed_spec_mp "sumr_bound";
   17.62  
   17.63  Goal "(ALL p. 0 <= p & p < n --> (f(p) <= K)) \
   17.64  \     --> (sumr 0 n f <= (real_of_nat n * K))";
   17.65  by (induct_tac "n" 1);
   17.66  by (auto_tac (claset() addIs [real_add_le_mono],
   17.67 -    simpset() addsimps [real_add_mult_distrib]));
   17.68 +        simpset() addsimps [real_add_mult_distrib, real_of_nat_Suc]));
   17.69  qed_spec_mp "sumr_bound2";
   17.70  
   17.71  Goal "sumr 0 n (%m. sumr (m * k) (m*k + k) f) = sumr 0 (n * k) f";
   17.72 @@ -543,14 +537,13 @@
   17.73  (*-------------------------------------------------------------------
   17.74                          The ratio test
   17.75   -------------------------------------------------------------------*)
   17.76 +
   17.77  Goal "[| c <= #0; abs x <= c * abs y |] ==> x = (#0::real)";
   17.78  by (dtac order_le_imp_less_or_eq 1);
   17.79 -by Auto_tac;
   17.80 -by (dres_inst_tac [("x1","y")] 
   17.81 -    (abs_ge_zero RS rename_numerals real_mult_le_zero) 1);
   17.82 -by (asm_full_simp_tac (simpset() addsimps [real_mult_commute]) 1);
   17.83 -by (dtac order_trans 1 THEN assume_tac 1);
   17.84 -by (TRYALL(arith_tac));
   17.85 +by Auto_tac;  
   17.86 +by (subgoal_tac "#0 <= c * abs y" 1);
   17.87 +by (arith_tac 2);
   17.88 +by (asm_full_simp_tac (simpset() addsimps [real_0_le_mult_iff]) 1); 
   17.89  qed "rabs_ratiotest_lemma";
   17.90  
   17.91  (* lemmas *)
   17.92 @@ -599,9 +592,9 @@
   17.93  qed "ratio_test";
   17.94  
   17.95  
   17.96 -(*----------------------------------------------------------------------------*)
   17.97 -(* Differentiation of finite sum                                              *)
   17.98 -(*----------------------------------------------------------------------------*)
   17.99 +(*--------------------------------------------------------------------------*)
  17.100 +(* Differentiation of finite sum                                            *)
  17.101 +(*--------------------------------------------------------------------------*)
  17.102  
  17.103  Goal "(ALL r. m <= r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) \
  17.104  \     --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)";
    18.1 --- a/src/HOL/Hyperreal/Star.ML	Thu Jan 04 10:22:33 2001 +0100
    18.2 +++ b/src/HOL/Hyperreal/Star.ML	Thu Jan 04 10:23:01 2001 +0100
    18.3 @@ -451,25 +451,28 @@
    18.4  qed "STAR_starfun_rabs_add_minus";
    18.5  
    18.6  (*-------------------------------------------------------------------
    18.7 -   Another charaterization of Infinitesimal and one of @= relation. 
    18.8 +   Another characterization of Infinitesimal and one of @= relation. 
    18.9     In this theory since hypreal_hrabs proved here. (To Check:) Maybe 
   18.10     move both if possible? 
   18.11   -------------------------------------------------------------------*)
   18.12  Goal "(x:Infinitesimal) = \
   18.13  \     (EX X:Rep_hypreal(x). \
   18.14 -\       ALL m. {n. abs(X n) < inverse(real_of_posnat m)}:FreeUltrafilterNat)";
   18.15 +\       ALL m. {n. abs(X n) < inverse(real_of_nat(Suc m))} \
   18.16 +\              : FreeUltrafilterNat)";
   18.17  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   18.18  by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl],
   18.19 -	simpset() addsimps [Infinitesimal_hypreal_of_posnat_iff,
   18.20 -	    hypreal_of_real_of_posnat,hypreal_of_real_def,hypreal_inverse,
   18.21 -	    hypreal_hrabs,hypreal_less])); 
   18.22 +	simpset() addsimps [Infinitesimal_hypreal_of_nat_iff,
   18.23 +	    hypreal_of_real_def,hypreal_inverse,
   18.24 +	    hypreal_hrabs,hypreal_less, hypreal_of_nat_def])); 
   18.25 +by (asm_full_simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero, 
   18.26 +			  real_not_refl2 RS not_sym]) 1) ;
   18.27  by (dres_inst_tac [("x","n")] spec 1);
   18.28  by (Fuf_tac 1);
   18.29  qed  "Infinitesimal_FreeUltrafilterNat_iff2";
   18.30  
   18.31  Goal "(Abs_hypreal(hyprel^^{X}) @= Abs_hypreal(hyprel^^{Y})) = \
   18.32  \     (ALL m. {n. abs (X n + - Y n) < \
   18.33 -\                 inverse(real_of_posnat m)} : FreeUltrafilterNat)";
   18.34 +\                 inverse(real_of_nat(Suc m))} : FreeUltrafilterNat)";
   18.35  by (rtac (inf_close_minus_iff RS ssubst) 1);
   18.36  by (rtac (mem_infmal_iff RS subst) 1);
   18.37  by (auto_tac (claset(), 
   18.38 @@ -485,8 +488,3 @@
   18.39  by (dres_inst_tac [("x","Abs_hypreal(hyprel ^^{%n. xa})")] fun_cong 1);
   18.40  by (auto_tac (claset(),simpset() addsimps [starfun]));
   18.41  qed "inj_starfun";
   18.42 -
   18.43 -
   18.44 -
   18.45 -
   18.46 -
    19.1 --- a/src/HOL/Real/RComplete.ML	Thu Jan 04 10:22:33 2001 +0100
    19.2 +++ b/src/HOL/Real/RComplete.ML	Thu Jan 04 10:23:01 2001 +0100
    19.3 @@ -194,51 +194,61 @@
    19.4          Related: Archimedean property of reals
    19.5   ----------------------------------------------------------------*)
    19.6  
    19.7 -Goal "#0 < x ==> EX n. inverse (real_of_posnat n) < x";
    19.8 -by (stac real_of_posnat_inverse_Ex_iff 1);
    19.9 -by (EVERY1[rtac ccontr, Asm_full_simp_tac]);
   19.10 -by (fold_tac [real_le_def]);
   19.11 +Goal "#0 < real_of_nat (Suc n)";
   19.12 +by (res_inst_tac [("y","real_of_nat n")] order_le_less_trans 1); 
   19.13 +by (rtac (rename_numerals real_of_nat_ge_zero) 1);
   19.14 +by (simp_tac (simpset() addsimps [real_of_nat_Suc]) 1); 
   19.15 +qed "real_of_nat_Suc_gt_zero";
   19.16 +
   19.17 +Goal "#0 < x ==> EX n. inverse (real_of_nat(Suc n)) < x";
   19.18 +by (rtac ccontr 1);
   19.19 +by (subgoal_tac "ALL n. x * real_of_nat (Suc n) <= #1" 1);
   19.20 +by (asm_full_simp_tac
   19.21 +    (simpset() addsimps [linorder_not_less, real_inverse_eq_divide]) 2); 
   19.22 +by (Clarify_tac 2);
   19.23 +by (dres_inst_tac [("x","n")] spec 2); 
   19.24 +by (dres_inst_tac [("z","real_of_nat (Suc n)")] 
   19.25 +    (rotate_prems 1 real_mult_le_le_mono1) 2); 
   19.26 +by (rtac real_of_nat_ge_zero 2);
   19.27 +by (asm_full_simp_tac (simpset()  
   19.28 +	 addsimps [real_of_nat_Suc_gt_zero RS real_not_refl2 RS not_sym, 
   19.29 +                   real_mult_commute]) 2); 
   19.30  by (subgoal_tac "isUb (UNIV::real set) \
   19.31 -\   {z. EX n. z = x*(real_of_posnat n)} #1" 1);
   19.32 -by (subgoal_tac "EX X. X : {z. EX n. z = x*(real_of_posnat n)}" 1);
   19.33 +\                     {z. EX n. z = x*(real_of_nat (Suc n))} #1" 1);
   19.34 +by (subgoal_tac "EX X. X : {z. EX n. z = x*(real_of_nat (Suc n))}" 1);
   19.35  by (dtac reals_complete 1);
   19.36  by (auto_tac (claset() addIs [isUbI,setleI],simpset()));
   19.37 -by (subgoal_tac "ALL m. x*(real_of_posnat(Suc m)) <= t" 1);
   19.38 +by (subgoal_tac "ALL m. x*(real_of_nat(Suc m)) <= t" 1);
   19.39  by (asm_full_simp_tac (simpset() addsimps 
   19.40 -   [real_of_posnat_Suc,real_add_mult_distrib2]) 1);
   19.41 +                       [real_of_nat_Suc, real_add_mult_distrib2]) 1);
   19.42  by (blast_tac (claset() addIs [isLubD2]) 2);
   19.43  by (asm_full_simp_tac
   19.44      (simpset() addsimps [real_le_diff_eq RS sym, real_diff_def]) 1);
   19.45  by (subgoal_tac "isUb (UNIV::real set) \
   19.46 -\   {z. EX n. z = x*(real_of_posnat n)} (t + (-x))" 1);
   19.47 +\                  {z. EX n. z = x*(real_of_nat (Suc n))} (t + (-x))" 1);
   19.48  by (blast_tac (claset() addSIs [isUbI,setleI]) 2);
   19.49  by (dres_inst_tac [("y","t+(-x)")] isLub_le_isUb 1);
   19.50 -by (dres_inst_tac [("x","-t")] real_add_left_le_mono1 2);
   19.51 -by (auto_tac (claset() addDs [order_le_less_trans,
   19.52 -			      real_minus_zero_less_iff2 RS iffD2], 
   19.53 -	      simpset() addsimps [real_add_assoc RS sym]));
   19.54 +by (auto_tac (claset(), 
   19.55 +	      simpset() addsimps [real_of_nat_Suc,real_add_mult_distrib2]));
   19.56  qed "reals_Archimedean";
   19.57  
   19.58 -Goal "EX n. (x::real) < real_of_posnat n";
   19.59 +(*There must be other proofs, e.g. Suc of the largest integer in the
   19.60 +  cut representing x*)
   19.61 +Goal "EX n. (x::real) < real_of_nat n";
   19.62  by (res_inst_tac [("R1.0","x"),("R2.0","#0")] real_linear_less2 1);
   19.63  by (res_inst_tac [("x","0")] exI 1);
   19.64 -by (res_inst_tac [("x","0")] exI 2);
   19.65 +by (res_inst_tac [("x","1")] exI 2);
   19.66  by (auto_tac (claset() addEs [order_less_trans],
   19.67 -	      simpset() addsimps [real_of_posnat_one,real_zero_less_one]));
   19.68 +	      simpset() addsimps [real_of_nat_one]));
   19.69  by (ftac ((rename_numerals real_inverse_gt_zero) RS reals_Archimedean) 1);
   19.70 -by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
   19.71 +by (Step_tac 1 THEN res_inst_tac [("x","Suc n")] exI 1);
   19.72  by (forw_inst_tac [("y","inverse x")]
   19.73      (rename_numerals real_mult_less_mono1) 1);
   19.74 -by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym]));
   19.75 -by (dres_inst_tac [("n1","n"),("y","#1")] 
   19.76 -     (real_of_posnat_gt_zero RS real_mult_less_mono2)  1);
   19.77 +by Auto_tac;  
   19.78 +by (dres_inst_tac [("y","#1"),("z","real_of_nat (Suc n)")]
   19.79 +    (rotate_prems 1 real_mult_less_mono2) 1);
   19.80  by (auto_tac (claset(),
   19.81 -	      simpset() addsimps [rename_numerals real_of_posnat_gt_zero,
   19.82 +	      simpset() addsimps [real_of_nat_Suc_gt_zero,
   19.83  				  real_not_refl2 RS not_sym,
   19.84  				  real_mult_assoc RS sym]));
   19.85  qed "reals_Archimedean2";
   19.86 -
   19.87 -
   19.88 -
   19.89 -
   19.90 -
    20.1 --- a/src/HOL/Real/RealArith0.ML	Thu Jan 04 10:22:33 2001 +0100
    20.2 +++ b/src/HOL/Real/RealArith0.ML	Thu Jan 04 10:23:01 2001 +0100
    20.3 @@ -86,6 +86,11 @@
    20.4  qed "real_divide_eq_0_iff";
    20.5  Addsimps [real_divide_eq_0_iff];
    20.6  
    20.7 +Goal "h ~= (#0::real) ==> h/h = #1";
    20.8 +by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_inv_left]) 1);
    20.9 +qed "real_divide_self_eq"; 
   20.10 +Addsimps [real_divide_self_eq];
   20.11 +
   20.12  
   20.13  (**** Factor cancellation theorems for "real" ****)
   20.14  
   20.15 @@ -524,6 +529,25 @@
   20.16  by (asm_simp_tac (simpset() addsimps [min_def]) 1); 
   20.17  qed "real_lbound_gt_zero";
   20.18  
   20.19 +Goal "(inverse x = inverse y) = (x = (y::real))";
   20.20 +by (case_tac "x=#0 | y=#0" 1);
   20.21 +by (auto_tac (claset(), 
   20.22 +              simpset() addsimps [real_inverse_eq_divide, 
   20.23 +                                  rename_numerals DIVISION_BY_ZERO])); 
   20.24 +by (dres_inst_tac [("f","%u. x*y*u")] arg_cong 1); 
   20.25 +by (Asm_full_simp_tac 1); 
   20.26 +qed "real_inverse_eq_iff";
   20.27 +Addsimps [real_inverse_eq_iff];
   20.28 +
   20.29 +Goal "(z/x = z/y) = (z = #0 | x = (y::real))";
   20.30 +by (case_tac "x=#0 | y=#0" 1);
   20.31 +by (auto_tac (claset(), 
   20.32 +              simpset() addsimps [rename_numerals DIVISION_BY_ZERO])); 
   20.33 +by (dres_inst_tac [("f","%u. x*y*u")] arg_cong 1);
   20.34 +by Auto_tac;   
   20.35 +qed "real_divide_eq_iff";
   20.36 +Addsimps [real_divide_eq_iff];
   20.37 +
   20.38  
   20.39  (*** General rewrites to improve automation, like those for type "int" ***)
   20.40  
    21.1 --- a/src/HOL/Real/RealDef.thy	Thu Jan 04 10:22:33 2001 +0100
    21.2 +++ b/src/HOL/Real/RealDef.thy	Thu Jan 04 10:23:01 2001 +0100
    21.3 @@ -23,9 +23,10 @@
    21.4  consts 
    21.5    "1r"   :: real               ("1r")  
    21.6  
    21.7 -   (*Overloaded constant: denotes the Real subset of enclosing types such as
    21.8 -     hypreal and complex*)
    21.9 -   SReal :: "'a set"
   21.10 +   (*Overloaded constants denoting the Nat and Real subsets of enclosing
   21.11 +     types such as hypreal and complex*)
   21.12 +   SNat, SReal :: "'a set"
   21.13 +  
   21.14  
   21.15  defs
   21.16  
   21.17 @@ -80,5 +81,6 @@
   21.18  
   21.19  syntax (symbols)
   21.20    SReal     :: "'a set"                   ("\\<real>")
   21.21 +  SNat      :: "'a set"                   ("\\<nat>")
   21.22  
   21.23  end
    22.1 --- a/src/HOL/Real/RealOrd.ML	Thu Jan 04 10:22:33 2001 +0100
    22.2 +++ b/src/HOL/Real/RealOrd.ML	Thu Jan 04 10:23:01 2001 +0100
    22.3 @@ -142,24 +142,6 @@
    22.4                simpset()));
    22.5  qed "real_less_le_mult_order";
    22.6  
    22.7 -Goal "[| x <= 0; y <= 0 |] ==> (0::real) <= x * y";
    22.8 -by (rtac real_less_or_eq_imp_le 1);
    22.9 -by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1);
   22.10 -by Auto_tac;
   22.11 -by (dtac order_le_imp_less_or_eq 1);
   22.12 -by (auto_tac (claset() addDs [real_mult_less_zero1],simpset()));
   22.13 -qed "real_mult_le_zero1";
   22.14 -
   22.15 -Goal "[| 0 <= x; y < 0 |] ==> x * y <= (0::real)";
   22.16 -by (rtac real_less_or_eq_imp_le 1);
   22.17 -by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1);
   22.18 -by Auto_tac;
   22.19 -by (dtac (real_minus_zero_less_iff RS iffD2) 1);
   22.20 -by (rtac (real_minus_zero_less_iff RS subst) 1);
   22.21 -by (blast_tac (claset() addDs [real_mult_order] 
   22.22 -	                addIs [real_minus_mult_eq2 RS ssubst]) 1);
   22.23 -qed "real_mult_le_zero";
   22.24 -
   22.25  Goal "[| 0 < x; y < 0 |] ==> x*y < (0::real)";
   22.26  by (dtac (real_minus_zero_less_iff RS iffD2) 1);
   22.27  by (dtac real_mult_order 1 THEN assume_tac 1);
   22.28 @@ -281,11 +263,6 @@
   22.29  by (auto_tac (claset(), simpset() addsimps [real_add_assoc]));
   22.30  qed "real_le_minus_iff";
   22.31  Addsimps [real_le_minus_iff];
   22.32 -          
   22.33 -Goal "0 <= 1r";
   22.34 -by (rtac (real_zero_less_one RS order_less_imp_le) 1);
   22.35 -qed "real_zero_le_one";
   22.36 -Addsimps [real_zero_le_one];
   22.37  
   22.38  Goal "(0::real) <= x*x";
   22.39  by (res_inst_tac [("R2.0","0"),("R1.0","x")] real_linear_less2 1);
   22.40 @@ -300,19 +277,18 @@
   22.41   ----------------------------------------------------------------------------*)
   22.42  
   22.43  Goalw [real_of_posnat_def] "real_of_posnat 0 = 1r";
   22.44 -by (full_simp_tac (simpset() addsimps [pnat_one_iff RS sym,real_of_preal_def]) 1);
   22.45 -by (fold_tac [real_one_def]);
   22.46 -by (rtac refl 1);
   22.47 +by (simp_tac (simpset() addsimps [pnat_one_iff RS sym,real_of_preal_def,
   22.48 +                       symmetric real_one_def]) 1);
   22.49  qed "real_of_posnat_one";
   22.50  
   22.51  Goalw [real_of_posnat_def] "real_of_posnat 1 = 1r + 1r";
   22.52 -by (full_simp_tac (simpset() addsimps [real_of_preal_def,real_one_def,
   22.53 -    pnat_two_eq,real_add,prat_of_pnat_add RS sym,preal_of_prat_add RS sym
   22.54 -    ] @ pnat_add_ac) 1);
   22.55 +by (simp_tac (simpset() addsimps [real_of_preal_def,real_one_def,
   22.56 +                               pnat_two_eq,real_add,prat_of_pnat_add RS sym,
   22.57 +                               preal_of_prat_add RS sym] @ pnat_add_ac) 1);
   22.58  qed "real_of_posnat_two";
   22.59  
   22.60  Goalw [real_of_posnat_def]
   22.61 -    "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + 1r";
   22.62 +     "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + 1r";
   22.63  by (full_simp_tac (simpset() addsimps [real_of_posnat_one RS sym,
   22.64      real_of_posnat_def,real_of_preal_add RS sym,preal_of_prat_add RS sym,
   22.65      prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
   22.66 @@ -338,40 +314,96 @@
   22.67  by (etac (inj_pnat_of_nat RS injD) 1);
   22.68  qed "inj_real_of_posnat";
   22.69  
   22.70 -Goalw [real_of_posnat_def] "0 < real_of_posnat n";
   22.71 -by (rtac (real_gt_zero_preal_Ex RS iffD2) 1);
   22.72 -by (Blast_tac 1);
   22.73 -qed "real_of_posnat_gt_zero";
   22.74 +Goalw [real_of_nat_def] "real_of_nat 0 = 0";
   22.75 +by (simp_tac (simpset() addsimps [real_of_posnat_one]) 1);
   22.76 +qed "real_of_nat_zero";
   22.77 +
   22.78 +Goalw [real_of_nat_def] "real_of_nat 1 = 1r";
   22.79 +by (simp_tac (simpset() addsimps [real_of_posnat_two, real_add_assoc]) 1);
   22.80 +qed "real_of_nat_one";
   22.81 +Addsimps [real_of_nat_zero, real_of_nat_one];
   22.82 +
   22.83 +Goalw [real_of_nat_def]
   22.84 +     "real_of_nat (m + n) = real_of_nat m + real_of_nat n";
   22.85 +by (simp_tac (simpset() addsimps 
   22.86 +              [real_of_posnat_add,real_add_assoc RS sym]) 1);
   22.87 +qed "real_of_nat_add";
   22.88  
   22.89 -Goal "real_of_posnat n ~= 0";
   22.90 -by (rtac (real_of_posnat_gt_zero RS real_not_refl2 RS not_sym) 1);
   22.91 -qed "real_of_posnat_not_eq_zero";
   22.92 -Addsimps[real_of_posnat_not_eq_zero];
   22.93 +(*Not for addsimps: often the LHS is used to represent a positive natural*)
   22.94 +Goalw [real_of_nat_def] "real_of_nat (Suc n) = real_of_nat n + 1r";
   22.95 +by (simp_tac (simpset() addsimps [real_of_posnat_Suc] @ real_add_ac) 1);
   22.96 +qed "real_of_nat_Suc";
   22.97 +
   22.98 +Goalw [real_of_nat_def, real_of_posnat_def]
   22.99 +     "(real_of_nat n < real_of_nat m) = (n < m)";
  22.100 +by Auto_tac;
  22.101 +qed "real_of_nat_less_iff";
  22.102 +AddIffs [real_of_nat_less_iff];
  22.103  
  22.104 -Goal "1r <= real_of_posnat n";
  22.105 -by (simp_tac (simpset() addsimps [real_of_posnat_one RS sym]) 1);
  22.106 +Goal "(real_of_nat n <= real_of_nat m) = (n <= m)";
  22.107 +by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 
  22.108 +qed "real_of_nat_le_iff";
  22.109 +AddIffs [real_of_nat_le_iff];
  22.110 +
  22.111 +Goal "inj real_of_nat";
  22.112 +by (rtac injI 1);
  22.113 +by (auto_tac (claset() addSIs [inj_real_of_posnat RS injD],
  22.114 +	      simpset() addsimps [real_of_nat_def,real_add_right_cancel]));
  22.115 +qed "inj_real_of_nat";
  22.116 +
  22.117 +Goal "0 <= real_of_nat n";
  22.118  by (induct_tac "n" 1);
  22.119  by (auto_tac (claset(),
  22.120 -	      simpset () addsimps [real_of_posnat_Suc,real_of_posnat_one,
  22.121 -			   real_of_posnat_gt_zero, order_less_imp_le]));
  22.122 -qed "real_of_posnat_less_one";
  22.123 -Addsimps [real_of_posnat_less_one];
  22.124 +              simpset () addsimps [real_of_nat_Suc]));
  22.125 +by (dtac real_add_le_less_mono 1); 
  22.126 +by (rtac real_zero_less_one 1); 
  22.127 +by (asm_full_simp_tac (simpset() addsimps [order_less_imp_le]) 1); 
  22.128 +qed "real_of_nat_ge_zero";
  22.129 +AddIffs [real_of_nat_ge_zero];
  22.130 +
  22.131 +Goal "real_of_nat (m * n) = real_of_nat m * real_of_nat n";
  22.132 +by (induct_tac "m" 1);
  22.133 +by (auto_tac (claset(),
  22.134 +	      simpset() addsimps [real_of_nat_add, real_of_nat_Suc,
  22.135 +				  real_add_mult_distrib, real_add_commute]));
  22.136 +qed "real_of_nat_mult";
  22.137 +
  22.138 +Goal "(real_of_nat n = real_of_nat m) = (n = m)";
  22.139 +by (auto_tac (claset() addDs [inj_real_of_nat RS injD], simpset()));
  22.140 +qed "real_of_nat_eq_cancel";
  22.141 +Addsimps [real_of_nat_eq_cancel];
  22.142  
  22.143 -Goal "inverse (real_of_posnat n) ~= 0";
  22.144 -by (rtac ((real_of_posnat_gt_zero RS 
  22.145 -    real_not_refl2 RS not_sym) RS real_inverse_not_zero) 1);
  22.146 -qed "real_of_posnat_inverse_not_zero";
  22.147 -Addsimps [real_of_posnat_inverse_not_zero];
  22.148 +Goal "n <= m --> real_of_nat (m - n) = real_of_nat m + (-real_of_nat n)";
  22.149 +by (induct_tac "m" 1);
  22.150 +by (auto_tac (claset(),
  22.151 +	      simpset() addsimps [Suc_diff_le, le_Suc_eq, real_of_nat_Suc, 
  22.152 +				  real_of_nat_zero] @ real_add_ac));
  22.153 +qed_spec_mp "real_of_nat_minus";
  22.154 +
  22.155 +Goalw [real_diff_def]
  22.156 +     "n < m ==> real_of_nat (m - n) = real_of_nat m - real_of_nat n";
  22.157 +by (auto_tac (claset() addIs [real_of_nat_minus], simpset()));
  22.158 +qed "real_of_nat_diff";
  22.159  
  22.160 -Goal "inverse (real_of_posnat x) = inverse (real_of_posnat y) ==> x = y";
  22.161 -by (rtac (inj_real_of_posnat RS injD) 1);
  22.162 -by (res_inst_tac [("n2","x")] 
  22.163 -    (real_of_posnat_inverse_not_zero RS real_mult_left_cancel RS iffD1) 1);
  22.164 -by (full_simp_tac (simpset() addsimps [(real_of_posnat_gt_zero RS 
  22.165 -    real_not_refl2 RS not_sym) RS real_mult_inv_left]) 1);
  22.166 -by (asm_full_simp_tac (simpset() addsimps [(real_of_posnat_gt_zero RS 
  22.167 -    real_not_refl2 RS not_sym)]) 1);
  22.168 -qed "real_of_posnat_inverse_inj";
  22.169 +Goalw [real_diff_def]
  22.170 +     "n <= m ==> real_of_nat (m - n) = real_of_nat m - real_of_nat n";
  22.171 +by (etac real_of_nat_minus 1);
  22.172 +qed "real_of_nat_diff2";
  22.173 +
  22.174 +Goal "(real_of_nat n = 0) = (n = 0)";
  22.175 +by (auto_tac (claset() addIs [inj_real_of_nat RS injD], simpset()));
  22.176 +qed "real_of_nat_zero_iff";
  22.177 +Addsimps [real_of_nat_zero_iff];
  22.178 +
  22.179 +Goal "neg z ==> real_of_nat (nat z) = 0";
  22.180 +by (asm_simp_tac (simpset() addsimps [neg_nat, real_of_nat_zero]) 1);
  22.181 +qed "real_of_nat_neg_int";
  22.182 +Addsimps [real_of_nat_neg_int];
  22.183 +
  22.184 +
  22.185 +(*----------------------------------------------------------------------------
  22.186 +     inverse, etc.
  22.187 + ----------------------------------------------------------------------------*)
  22.188  
  22.189  Goal "0 < x ==> 0 < inverse (x::real)";
  22.190  by (EVERY1[rtac ccontr, dtac real_leI]);
  22.191 @@ -392,40 +424,6 @@
  22.192  by (auto_tac (claset() addIs [real_inverse_gt_zero], simpset()));
  22.193  qed "real_inverse_less_zero";
  22.194  
  22.195 -Goal "0 < inverse (real_of_posnat n)";
  22.196 -by (rtac (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1);
  22.197 -qed "real_of_posnat_inverse_gt_zero";
  22.198 -Addsimps [real_of_posnat_inverse_gt_zero];
  22.199 -
  22.200 -Goal "real_of_preal (preal_of_prat (prat_of_pnat (pnat_of_nat N))) = \
  22.201 -\     real_of_nat (Suc N)";
  22.202 -by (simp_tac (simpset() addsimps [real_of_nat_def,real_of_posnat_Suc,
  22.203 -    real_add_assoc,(real_of_posnat_def RS meta_eq_to_obj_eq) RS sym]) 1);
  22.204 -qed "real_of_preal_real_of_nat_Suc";
  22.205 -
  22.206 -Goal "x+x = x*(1r+1r)";
  22.207 -by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
  22.208 -qed "real_add_self";
  22.209 -
  22.210 -Goal "x < x + 1r";
  22.211 -by (rtac (real_less_sum_gt_0_iff RS iffD1) 1);
  22.212 -by (full_simp_tac (simpset() addsimps [real_zero_less_one,
  22.213 -				real_add_assoc, real_add_left_commute]) 1);
  22.214 -qed "real_self_less_add_one";
  22.215 -
  22.216 -Goal "1r < 1r + 1r";
  22.217 -by (rtac real_self_less_add_one 1);
  22.218 -qed "real_one_less_two";
  22.219 -
  22.220 -Goal "0 < 1r + 1r";
  22.221 -by (rtac ([real_zero_less_one, real_one_less_two] MRS order_less_trans) 1);
  22.222 -qed "real_zero_less_two";
  22.223 -
  22.224 -Goal "1r + 1r ~= 0";
  22.225 -by (rtac (real_zero_less_two RS real_not_refl2 RS not_sym) 1);
  22.226 -qed "real_two_not_zero";
  22.227 -Addsimps [real_two_not_zero];
  22.228 -
  22.229  Goal "[| (0::real) < z; x < y |] ==> x*z < y*z";       
  22.230  by (rotate_tac 1 1);
  22.231  by (dtac real_less_sum_gt_zero 1);
  22.232 @@ -550,66 +548,6 @@
  22.233  by (auto_tac (claset() addIs [real_mult_self_le], simpset()));
  22.234  qed "real_mult_self_le2";
  22.235  
  22.236 -Goal "(EX n. inverse (real_of_posnat n) < r) = (EX n. 1r < r * real_of_posnat n)";
  22.237 -by (Step_tac 1);
  22.238 -by (dres_inst_tac [("n1","n")] (real_of_posnat_gt_zero 
  22.239 -				RS real_mult_less_mono1) 1);
  22.240 -by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS 
  22.241 -				real_inverse_gt_zero RS real_mult_less_mono1) 2);
  22.242 -by (auto_tac (claset(),
  22.243 -	      simpset() addsimps [(real_of_posnat_gt_zero RS 
  22.244 -				   real_not_refl2 RS not_sym),
  22.245 -				  real_mult_assoc]));
  22.246 -qed "real_of_posnat_inverse_Ex_iff";
  22.247 -
  22.248 -Goal "(inverse(real_of_posnat n) < r) = (1r < r * real_of_posnat n)";
  22.249 -by (Step_tac 1);
  22.250 -by (dres_inst_tac [("n1","n")] (real_of_posnat_gt_zero 
  22.251 -                       RS real_mult_less_mono1) 1);
  22.252 -by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS 
  22.253 -				real_inverse_gt_zero RS real_mult_less_mono1) 2);
  22.254 -by (auto_tac (claset(), simpset() addsimps [real_mult_assoc]));
  22.255 -qed "real_of_posnat_inverse_iff";
  22.256 -
  22.257 -Goal "(inverse (real_of_posnat n) <= r) = (1r <= r * real_of_posnat n)";
  22.258 -by (Step_tac 1);
  22.259 -by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS 
  22.260 -    order_less_imp_le RS real_mult_le_le_mono1) 1);
  22.261 -by (dres_inst_tac [("n3","n")] (real_of_posnat_gt_zero RS 
  22.262 -        real_inverse_gt_zero RS order_less_imp_le RS 
  22.263 -        real_mult_le_le_mono1) 2);
  22.264 -by (auto_tac (claset(), simpset() addsimps real_mult_ac));
  22.265 -qed "real_of_posnat_inverse_le_iff";
  22.266 -
  22.267 -Goalw [real_of_posnat_def] "(real_of_posnat n < real_of_posnat m) = (n < m)";
  22.268 -by Auto_tac;
  22.269 -qed "real_of_posnat_less_iff";
  22.270 -
  22.271 -Addsimps [real_of_posnat_less_iff];
  22.272 -
  22.273 -Goal "0 < u  ==> (u < inverse (real_of_posnat n)) = (real_of_posnat n < inverse u)";
  22.274 -by (Step_tac 1);
  22.275 -by (res_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS 
  22.276 -    real_inverse_gt_zero RS real_mult_less_cancel1) 1);
  22.277 -by (res_inst_tac [("x1","u")] ( real_inverse_gt_zero
  22.278 -   RS real_mult_less_cancel1) 2);
  22.279 -by (auto_tac (claset(),
  22.280 -	      simpset() addsimps [real_of_posnat_gt_zero, 
  22.281 -    real_not_refl2 RS not_sym]));
  22.282 -by (res_inst_tac [("z","u")] real_mult_less_cancel2 1);
  22.283 -by (res_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS 
  22.284 -    real_mult_less_cancel2) 3);
  22.285 -by (auto_tac (claset(),
  22.286 -	      simpset() addsimps [real_of_posnat_gt_zero, 
  22.287 -    real_not_refl2 RS not_sym,real_mult_assoc RS sym]));
  22.288 -qed "real_of_posnat_less_inverse_iff";
  22.289 -
  22.290 -Goal "0 < u ==> (u = inverse (real_of_posnat n)) = (real_of_posnat n = inverse u)";
  22.291 -by (auto_tac (claset(),
  22.292 -	      simpset() addsimps [real_inverse_inverse, real_of_posnat_gt_zero, 
  22.293 -				  real_not_refl2 RS not_sym]));
  22.294 -qed "real_of_posnat_inverse_eq_iff";
  22.295 -
  22.296  Goal "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)";
  22.297  by (ftac order_less_trans 1 THEN assume_tac 1);
  22.298  by (ftac real_inverse_gt_zero 1);
  22.299 @@ -625,65 +563,14 @@
  22.300           not_sym RS real_mult_inv_left,real_mult_assoc RS sym]) 1);
  22.301  qed "real_inverse_less_swap";
  22.302  
  22.303 -Goal "r < r + inverse (real_of_posnat n)";
  22.304 -by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
  22.305 -by (full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
  22.306 -qed "real_add_inverse_real_of_posnat_less";
  22.307 -Addsimps [real_add_inverse_real_of_posnat_less];
  22.308 -
  22.309 -Goal "r <= r + inverse (real_of_posnat n)";
  22.310 -by (rtac order_less_imp_le 1);
  22.311 -by (Simp_tac 1);
  22.312 -qed "real_add_inverse_real_of_posnat_le";
  22.313 -Addsimps [real_add_inverse_real_of_posnat_le];
  22.314 -
  22.315 -Goal "r + (-inverse (real_of_posnat n)) < r";
  22.316 -by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
  22.317 -by (full_simp_tac (simpset() addsimps [real_add_assoc RS sym,
  22.318 -				       real_minus_zero_less_iff2]) 1);
  22.319 -qed "real_add_minus_inverse_real_of_posnat_less";
  22.320 -Addsimps [real_add_minus_inverse_real_of_posnat_less];
  22.321 -
  22.322 -Goal "r + (-inverse (real_of_posnat n)) <= r";
  22.323 -by (rtac order_less_imp_le 1);
  22.324 -by (Simp_tac 1);
  22.325 -qed "real_add_minus_inverse_real_of_posnat_le";
  22.326 -Addsimps [real_add_minus_inverse_real_of_posnat_le];
  22.327 -
  22.328 -Goal "0 < r ==> r*(1r + (-inverse (real_of_posnat n))) < r";
  22.329 -by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
  22.330 -by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
  22.331 -by (auto_tac (claset() addIs [real_mult_order],
  22.332 -	      simpset() addsimps [real_add_assoc RS sym,
  22.333 -				  real_minus_zero_less_iff2]));
  22.334 -qed "real_mult_less_self";
  22.335 -
  22.336 -Goal "0 <= 1r + (-inverse (real_of_posnat n))";
  22.337 -by (res_inst_tac [("C","inverse (real_of_posnat n)")] real_le_add_right_cancel 1);
  22.338 -by (simp_tac (simpset() addsimps [real_add_assoc,
  22.339 -				  real_of_posnat_inverse_le_iff]) 1);
  22.340 -qed "real_add_one_minus_inverse_ge_zero";
  22.341 -
  22.342 -Goal "0 < r ==> 0 <= r*(1r + (-inverse (real_of_posnat n)))";
  22.343 -by (dtac (real_add_one_minus_inverse_ge_zero RS real_mult_le_less_mono1) 1);
  22.344 -by Auto_tac;
  22.345 -qed "real_mult_add_one_minus_ge_zero";
  22.346 -
  22.347  Goal "(x*y = 0) = (x = 0 | y = (0::real))";
  22.348  by Auto_tac;
  22.349  by (blast_tac (claset() addIs [ccontr] addDs [real_mult_not_zero]) 1);
  22.350  qed "real_mult_is_0";
  22.351  AddIffs [real_mult_is_0];
  22.352  
  22.353 -Goal "[| 0 <= x * y; 0 < x |] ==> (0::real) <= y";
  22.354 -by (ftac real_inverse_gt_zero 1);
  22.355 -by (dres_inst_tac [("x","inverse x")] real_less_le_mult_order 1);
  22.356 -by (dtac (real_not_refl2 RS not_sym RS real_mult_inv_left) 2);
  22.357 -by (auto_tac (claset(),
  22.358 -	      simpset() addsimps [real_mult_assoc RS sym]));
  22.359 -qed "real_mult_ge_zero_cancel";
  22.360 -
  22.361 -Goal "[|x ~= 0; y ~= 0 |] ==> inverse x + inverse y = (x + y) * inverse (x * (y::real))";
  22.362 +Goal "[| x ~= 0; y ~= 0 |] \
  22.363 +\     ==> inverse x + inverse y = (x + y) * inverse (x * (y::real))";
  22.364  by (asm_full_simp_tac (simpset() addsimps 
  22.365  		       [real_inverse_distrib,real_add_mult_distrib,
  22.366  			real_mult_assoc RS sym]) 1);
  22.367 @@ -753,90 +640,3 @@
  22.368                                    linorder_not_less RS sym]));
  22.369  qed "real_mult_le_zero_iff";
  22.370  
  22.371 -
  22.372 -(*----------------------------------------------------------------------------
  22.373 -     Another embedding of the naturals in the reals (see real_of_posnat)
  22.374 - ----------------------------------------------------------------------------*)
  22.375 -Goalw [real_of_nat_def] "real_of_nat 0 = 0";
  22.376 -by (simp_tac (simpset() addsimps [real_of_posnat_one]) 1);
  22.377 -qed "real_of_nat_zero";
  22.378 -
  22.379 -Goalw [real_of_nat_def] "real_of_nat 1 = 1r";
  22.380 -by (simp_tac (simpset() addsimps [real_of_posnat_two, real_add_assoc]) 1);
  22.381 -qed "real_of_nat_one";
  22.382 -Addsimps [real_of_nat_zero, real_of_nat_one];
  22.383 -
  22.384 -Goalw [real_of_nat_def]
  22.385 -     "real_of_nat (m + n) = real_of_nat m + real_of_nat n";
  22.386 -by (simp_tac (simpset() addsimps 
  22.387 -              [real_of_posnat_add,real_add_assoc RS sym]) 1);
  22.388 -qed "real_of_nat_add";
  22.389 -
  22.390 -Goalw [real_of_nat_def] "real_of_nat (Suc n) = real_of_nat n + 1r";
  22.391 -by (simp_tac (simpset() addsimps [real_of_posnat_Suc] @ real_add_ac) 1);
  22.392 -qed "real_of_nat_Suc";
  22.393 -Addsimps [real_of_nat_Suc];
  22.394 -    
  22.395 -Goalw [real_of_nat_def] "(real_of_nat n < real_of_nat m) = (n < m)";
  22.396 -by Auto_tac;
  22.397 -qed "real_of_nat_less_iff";
  22.398 -
  22.399 -AddIffs [real_of_nat_less_iff];
  22.400 -
  22.401 -Goal "inj real_of_nat";
  22.402 -by (rtac injI 1);
  22.403 -by (auto_tac (claset() addSIs [inj_real_of_posnat RS injD],
  22.404 -	      simpset() addsimps [real_of_nat_def,real_add_right_cancel]));
  22.405 -qed "inj_real_of_nat";
  22.406 -
  22.407 -Goalw [real_of_nat_def] "0 <= real_of_nat n";
  22.408 -by (res_inst_tac [("C","1r")] real_le_add_right_cancel 1);
  22.409 -by (asm_full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
  22.410 -qed "real_of_nat_ge_zero";
  22.411 -AddIffs [real_of_nat_ge_zero];
  22.412 -
  22.413 -Goal "real_of_nat (m * n) = real_of_nat m * real_of_nat n";
  22.414 -by (induct_tac "m" 1);
  22.415 -by (auto_tac (claset(),
  22.416 -	      simpset() addsimps [real_of_nat_add,
  22.417 -				  real_add_mult_distrib, real_add_commute]));
  22.418 -qed "real_of_nat_mult";
  22.419 -
  22.420 -Goal "(real_of_nat n = real_of_nat m) = (n = m)";
  22.421 -by (auto_tac (claset() addDs [inj_real_of_nat RS injD],
  22.422 -              simpset()));
  22.423 -qed "real_of_nat_eq_cancel";
  22.424 -
  22.425 -Goal "n <= m --> real_of_nat (m - n) = real_of_nat m + (-real_of_nat n)";
  22.426 -by (induct_tac "m" 1);
  22.427 -by (auto_tac (claset(),
  22.428 -	      simpset() addsimps [Suc_diff_le, le_Suc_eq, real_of_nat_Suc, 
  22.429 -				  real_of_nat_zero] @ real_add_ac));
  22.430 -qed_spec_mp "real_of_nat_minus";
  22.431 -
  22.432 -(* 05/00 *)
  22.433 -Goal "n < m ==> real_of_nat (m - n) = \
  22.434 -\     real_of_nat m + -real_of_nat n";
  22.435 -by (auto_tac (claset() addIs [real_of_nat_minus],simpset()));
  22.436 -qed "real_of_nat_minus2";
  22.437 -
  22.438 -Goalw [real_diff_def]
  22.439 -     "n < m ==> real_of_nat (m - n) = real_of_nat m - real_of_nat n";
  22.440 -by (etac real_of_nat_minus2 1);
  22.441 -qed "real_of_nat_diff";
  22.442 -
  22.443 -Goalw [real_diff_def]
  22.444 -     "n <= m ==> real_of_nat (m - n) = real_of_nat m - real_of_nat n";
  22.445 -by (etac real_of_nat_minus 1);
  22.446 -qed "real_of_nat_diff2";
  22.447 -
  22.448 -Goal "(real_of_nat n = 0) = (n = 0)";
  22.449 -by (auto_tac (claset() addIs [inj_real_of_nat RS injD], simpset()));
  22.450 -qed "real_of_nat_zero_iff";
  22.451 -AddIffs [real_of_nat_zero_iff];
  22.452 -
  22.453 -Goal "neg z ==> real_of_nat (nat z) = 0";
  22.454 -by (asm_simp_tac (simpset() addsimps [neg_nat, real_of_nat_zero]) 1);
  22.455 -qed "real_of_nat_neg_int";
  22.456 -Addsimps [real_of_nat_neg_int];
  22.457 -
    23.1 --- a/src/HOL/Real/RealPow.ML	Thu Jan 04 10:22:33 2001 +0100
    23.2 +++ b/src/HOL/Real/RealPow.ML	Thu Jan 04 10:23:01 2001 +0100
    23.3 @@ -146,16 +146,15 @@
    23.4  Goal "(#1::real) <= #2 ^ n";
    23.5  by (res_inst_tac [("y","#1 ^ n")] order_trans 1);
    23.6  by (rtac realpow_le 2);
    23.7 -by (auto_tac (claset() addIs [order_less_imp_le],simpset()));
    23.8 +by (auto_tac (claset() addIs [order_less_imp_le], simpset()));
    23.9  qed "two_realpow_ge_one";
   23.10  
   23.11  Goal "real_of_nat n < #2 ^ n";
   23.12  by (induct_tac "n" 1);
   23.13 -by Auto_tac;
   23.14 +by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));
   23.15  by (stac real_mult_2 1);
   23.16  by (rtac real_add_less_le_mono 1);
   23.17 -by (auto_tac (claset(),
   23.18 -	      simpset() addsimps [two_realpow_ge_one]));
   23.19 +by (auto_tac (claset(), simpset() addsimps [two_realpow_ge_one]));
   23.20  qed "two_realpow_gt";
   23.21  Addsimps [two_realpow_gt,two_realpow_ge_one];
   23.22