new theory Real/Hyperreal/HyperDef and file fuf.ML
authorpaulson
Mon Aug 16 18:41:06 1999 +0200 (1999-08-16)
changeset 7218bfa767b4dc51
parent 7217 3af1e69b25b8
child 7219 4e3f386c2e37
new theory Real/Hyperreal/HyperDef and file fuf.ML
src/HOL/IsaMakefile
src/HOL/Real/Hyperreal/HyperDef.ML
src/HOL/Real/Hyperreal/HyperDef.thy
src/HOL/Real/Hyperreal/fuf.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Aug 16 17:44:14 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Aug 16 18:41:06 1999 +0200
     1.3 @@ -82,6 +82,8 @@
     1.4    Real/RealDef.ML Real/RealDef.thy Real/simproc.ML \
     1.5    Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
     1.6    Real/Hyperreal/Filter.ML Real/Hyperreal/Filter.thy \
     1.7 +  Real/Hyperreal/fuf.ML \
     1.8 +  Real/Hyperreal/HyperDef.ML Real/Hyperreal/HyperDef.thy \
     1.9    Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy
    1.10  	@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real
    1.11  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Mon Aug 16 18:41:06 1999 +0200
     2.3 @@ -0,0 +1,2227 @@
     2.4 +(*  Title       : HOL/Real/Hyperreal/Hyper.ML
     2.5 +    ID          : $Id$
     2.6 +    Author      : Jacques D. Fleuriot
     2.7 +    Copyright   : 1998  University of Cambridge
     2.8 +    Description : Ultrapower construction of hyperreals
     2.9 +*) 
    2.10 +
    2.11 +(*------------------------------------------------------------------------
    2.12 +             Proof that the set of naturals is not finite
    2.13 + ------------------------------------------------------------------------*)
    2.14 +
    2.15 +(*** based on James' proof that the set of naturals is not finite ***)
    2.16 +Goal "finite (A::nat set) --> (? n. !m. Suc (n + m) ~: A)";
    2.17 +by (rtac impI 1);
    2.18 +by (eres_inst_tac [("F","A")] finite_induct 1);
    2.19 +by (Blast_tac 1 THEN etac exE 1);
    2.20 +by (res_inst_tac [("x","n + x")] exI 1);
    2.21 +by (rtac allI 1 THEN eres_inst_tac [("x","x + m")] allE 1);
    2.22 +by (auto_tac (claset(), simpset() addsimps add_ac));
    2.23 +by (auto_tac (claset(),
    2.24 +	      simpset() addsimps [add_assoc RS sym,
    2.25 +				  less_add_Suc2 RS less_not_refl2]));
    2.26 +qed_spec_mp "finite_exhausts";
    2.27 +
    2.28 +Goal "finite (A :: nat set) --> (? n. n ~:A)";
    2.29 +by (rtac impI 1 THEN dtac finite_exhausts 1);
    2.30 +by (Blast_tac 1);
    2.31 +qed_spec_mp "finite_not_covers";
    2.32 +
    2.33 +Goal "~ finite(UNIV:: nat set)";
    2.34 +by (fast_tac (claset() addSDs [finite_exhausts]) 1);
    2.35 +qed "not_finite_nat";
    2.36 +
    2.37 +(*------------------------------------------------------------------------
    2.38 +   Existence of free ultrafilter over the naturals and proof of various 
    2.39 +   properties of the FreeUltrafilterNat- an arbitrary free ultrafilter
    2.40 + ------------------------------------------------------------------------*)
    2.41 +
    2.42 +Goal "EX U. U: FreeUltrafilter (UNIV::nat set)";
    2.43 +by (rtac (not_finite_nat RS FreeUltrafilter_Ex) 1);
    2.44 +qed "FreeUltrafilterNat_Ex";
    2.45 +
    2.46 +Goalw [FreeUltrafilterNat_def] 
    2.47 +     "FreeUltrafilterNat: FreeUltrafilter(UNIV:: nat set)";
    2.48 +by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
    2.49 +by (rtac selectI2 1 THEN ALLGOALS(assume_tac));
    2.50 +qed "FreeUltrafilterNat_mem";
    2.51 +Addsimps [FreeUltrafilterNat_mem];
    2.52 +
    2.53 +Goalw [FreeUltrafilterNat_def] "finite x ==> x ~: FreeUltrafilterNat";
    2.54 +by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
    2.55 +by (rtac selectI2 1 THEN assume_tac 1);
    2.56 +by (blast_tac (claset() addDs [mem_FreeUltrafiltersetD1]) 1);
    2.57 +qed "FreeUltrafilterNat_finite";
    2.58 +
    2.59 +Goal "x: FreeUltrafilterNat ==> ~ finite x";
    2.60 +by (blast_tac (claset() addDs [FreeUltrafilterNat_finite]) 1);
    2.61 +qed "FreeUltrafilterNat_not_finite";
    2.62 +
    2.63 +Goalw [FreeUltrafilterNat_def] "{} ~: FreeUltrafilterNat";
    2.64 +by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
    2.65 +by (rtac selectI2 1 THEN assume_tac 1);
    2.66 +by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter,
    2.67 +			       Ultrafilter_Filter,Filter_empty_not_mem]) 1);
    2.68 +qed "FreeUltrafilterNat_empty";
    2.69 +Addsimps [FreeUltrafilterNat_empty];
    2.70 +
    2.71 +Goal "[| X: FreeUltrafilterNat;  Y: FreeUltrafilterNat |]  \
    2.72 +\     ==> X Int Y : FreeUltrafilterNat";
    2.73 +by (cut_facts_tac [FreeUltrafilterNat_mem] 1);
    2.74 +by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter,
    2.75 +			       Ultrafilter_Filter,mem_FiltersetD1]) 1);
    2.76 +qed "FreeUltrafilterNat_Int";
    2.77 +
    2.78 +Goal "[| X: FreeUltrafilterNat;  X <= Y |] \
    2.79 +\     ==> Y : FreeUltrafilterNat";
    2.80 +by (cut_facts_tac [FreeUltrafilterNat_mem] 1);
    2.81 +by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter,
    2.82 +			       Ultrafilter_Filter,mem_FiltersetD2]) 1);
    2.83 +qed "FreeUltrafilterNat_subset";
    2.84 +
    2.85 +Goal "X: FreeUltrafilterNat ==> -X ~: FreeUltrafilterNat";
    2.86 +by (Step_tac 1);
    2.87 +by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
    2.88 +by Auto_tac;
    2.89 +qed "FreeUltrafilterNat_Compl";
    2.90 +
    2.91 +Goal "X~: FreeUltrafilterNat ==> -X : FreeUltrafilterNat";
    2.92 +by (cut_facts_tac [FreeUltrafilterNat_mem RS (FreeUltrafilter_iff RS iffD1)] 1);
    2.93 +by (Step_tac 1 THEN dres_inst_tac [("x","X")] bspec 1);
    2.94 +by (auto_tac (claset(),simpset() addsimps [UNIV_diff_Compl]));
    2.95 +qed "FreeUltrafilterNat_Compl_mem";
    2.96 +
    2.97 +Goal "(X ~: FreeUltrafilterNat) = (-X: FreeUltrafilterNat)";
    2.98 +by (blast_tac (claset() addDs [FreeUltrafilterNat_Compl,
    2.99 +			       FreeUltrafilterNat_Compl_mem]) 1);
   2.100 +qed "FreeUltrafilterNat_Compl_iff1";
   2.101 +
   2.102 +Goal "(X: FreeUltrafilterNat) = (-X ~: FreeUltrafilterNat)";
   2.103 +by (auto_tac (claset(),
   2.104 +	      simpset() addsimps [FreeUltrafilterNat_Compl_iff1 RS sym]));
   2.105 +qed "FreeUltrafilterNat_Compl_iff2";
   2.106 +
   2.107 +Goal "(UNIV::nat set) : FreeUltrafilterNat";
   2.108 +by (rtac (FreeUltrafilterNat_mem RS FreeUltrafilter_Ultrafilter RS 
   2.109 +          Ultrafilter_Filter RS mem_FiltersetD4) 1);
   2.110 +qed "FreeUltrafilterNat_UNIV";
   2.111 +Addsimps [FreeUltrafilterNat_UNIV];
   2.112 +
   2.113 +Goal "{n::nat. True}: FreeUltrafilterNat";
   2.114 +by (subgoal_tac "{n::nat. True} = (UNIV::nat set)" 1);
   2.115 +by Auto_tac;
   2.116 +qed "FreeUltrafilterNat_Nat_set";
   2.117 +Addsimps [FreeUltrafilterNat_Nat_set];
   2.118 +
   2.119 +Goal "{n. P(n) = P(n)} : FreeUltrafilterNat";
   2.120 +by (Simp_tac 1);
   2.121 +qed "FreeUltrafilterNat_Nat_set_refl";
   2.122 +AddIs [FreeUltrafilterNat_Nat_set_refl];
   2.123 +
   2.124 +Goal "{n::nat. P} : FreeUltrafilterNat ==> P";
   2.125 +by (rtac ccontr 1);
   2.126 +by (rotate_tac 1 1);
   2.127 +by (Asm_full_simp_tac 1);
   2.128 +qed "FreeUltrafilterNat_P";
   2.129 +
   2.130 +Goal "{n. P(n)} : FreeUltrafilterNat ==> EX n. P(n)";
   2.131 +by (rtac ccontr 1 THEN rotate_tac 1 1);
   2.132 +by (Asm_full_simp_tac 1);
   2.133 +qed "FreeUltrafilterNat_Ex_P";
   2.134 +
   2.135 +Goal "ALL n. P(n) ==> {n. P(n)} : FreeUltrafilterNat";
   2.136 +by (auto_tac (claset() addIs [FreeUltrafilterNat_Nat_set],simpset()));
   2.137 +qed "FreeUltrafilterNat_all";
   2.138 +
   2.139 +(*-----------------------------------------
   2.140 +     Define and use Ultrafilter tactics
   2.141 + -----------------------------------------*)
   2.142 +use "fuf.ML";
   2.143 +
   2.144 +
   2.145 +
   2.146 +(*------------------------------------------------------
   2.147 +   Now prove one further property of our free ultrafilter
   2.148 + -------------------------------------------------------*)
   2.149 +Goal "X Un Y: FreeUltrafilterNat \
   2.150 +\     ==> X: FreeUltrafilterNat | Y: FreeUltrafilterNat";
   2.151 +by Auto_tac;
   2.152 +by (Ultra_tac 1);
   2.153 +qed "FreeUltrafilterNat_Un";
   2.154 +
   2.155 +(*------------------------------------------------------------------------
   2.156 +                       Properties of hyprel
   2.157 + ------------------------------------------------------------------------*)
   2.158 +
   2.159 +(** Proving that hyprel is an equivalence relation **)
   2.160 +(** Natural deduction for hyprel **)
   2.161 +
   2.162 +Goalw [hyprel_def]
   2.163 +   "((X,Y): hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)";
   2.164 +by (Fast_tac 1);
   2.165 +qed "hyprel_iff";
   2.166 +
   2.167 +Goalw [hyprel_def] 
   2.168 +     "{n. X n = Y n}: FreeUltrafilterNat  ==> (X,Y): hyprel";
   2.169 +by (Fast_tac 1);
   2.170 +qed "hyprelI";
   2.171 +
   2.172 +Goalw [hyprel_def]
   2.173 +  "p: hyprel --> (EX X Y. \
   2.174 +\                 p = (X,Y) & {n. X n = Y n} : FreeUltrafilterNat)";
   2.175 +by (Fast_tac 1);
   2.176 +qed "hyprelE_lemma";
   2.177 +
   2.178 +val [major,minor] = goal thy
   2.179 +  "[| p: hyprel;  \
   2.180 +\     !!X Y. [| p = (X,Y); {n. X n = Y n}: FreeUltrafilterNat\
   2.181 +\                    |] ==> Q |] ==> Q";
   2.182 +by (cut_facts_tac [major RS (hyprelE_lemma RS mp)] 1);
   2.183 +by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
   2.184 +qed "hyprelE";
   2.185 +
   2.186 +AddSIs [hyprelI];
   2.187 +AddSEs [hyprelE];
   2.188 +
   2.189 +Goalw [hyprel_def] "(x,x): hyprel";
   2.190 +by (auto_tac (claset(),simpset() addsimps 
   2.191 +         [FreeUltrafilterNat_Nat_set]));
   2.192 +qed "hyprel_refl";
   2.193 +
   2.194 +Goal "{n. X n = Y n} = {n. Y n = X n}";
   2.195 +by Auto_tac;
   2.196 +qed "lemma_perm";
   2.197 +
   2.198 +Goalw [hyprel_def] "(x,y): hyprel --> (y,x):hyprel";
   2.199 +by (auto_tac (claset() addIs [lemma_perm RS subst],simpset()));
   2.200 +qed_spec_mp "hyprel_sym";
   2.201 +
   2.202 +Goalw [hyprel_def]
   2.203 +      "(x,y): hyprel --> (y,z):hyprel --> (x,z):hyprel";
   2.204 +by Auto_tac;
   2.205 +by (Ultra_tac 1);
   2.206 +qed_spec_mp "hyprel_trans";
   2.207 +
   2.208 +Goalw [equiv_def, refl_def, sym_def, trans_def]
   2.209 +    "equiv {x::nat=>real. True} hyprel";
   2.210 +by (auto_tac (claset() addSIs [hyprel_refl] 
   2.211 +                       addSEs [hyprel_sym,hyprel_trans] 
   2.212 +                       delrules [hyprelI,hyprelE],
   2.213 +	      simpset() addsimps [FreeUltrafilterNat_Nat_set]));
   2.214 +qed "equiv_hyprel";
   2.215 +
   2.216 +val equiv_hyprel_iff =
   2.217 +    [TrueI, TrueI] MRS 
   2.218 +    ([CollectI, CollectI] MRS 
   2.219 +    (equiv_hyprel RS eq_equiv_class_iff));
   2.220 +
   2.221 +Goalw  [hypreal_def,hyprel_def,quotient_def] "hyprel^^{x}:hypreal";
   2.222 +by (Blast_tac 1);
   2.223 +qed "hyprel_in_hypreal";
   2.224 +
   2.225 +Goal "inj_on Abs_hypreal hypreal";
   2.226 +by (rtac inj_on_inverseI 1);
   2.227 +by (etac Abs_hypreal_inverse 1);
   2.228 +qed "inj_on_Abs_hypreal";
   2.229 +
   2.230 +Addsimps [equiv_hyprel_iff,inj_on_Abs_hypreal RS inj_on_iff,
   2.231 +          hyprel_iff, hyprel_in_hypreal, Abs_hypreal_inverse];
   2.232 +
   2.233 +Addsimps [equiv_hyprel RS eq_equiv_class_iff];
   2.234 +val eq_hyprelD = equiv_hyprel RSN (2,eq_equiv_class);
   2.235 +
   2.236 +Goal "inj(Rep_hypreal)";
   2.237 +by (rtac inj_inverseI 1);
   2.238 +by (rtac Rep_hypreal_inverse 1);
   2.239 +qed "inj_Rep_hypreal";
   2.240 +
   2.241 +Goalw [hyprel_def] "x: hyprel ^^ {x}";
   2.242 +by (Step_tac 1);
   2.243 +by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset()));
   2.244 +qed "lemma_hyprel_refl";
   2.245 +
   2.246 +Addsimps [lemma_hyprel_refl];
   2.247 +
   2.248 +Goalw [hypreal_def] "{} ~: hypreal";
   2.249 +by (auto_tac (claset() addSEs [quotientE], simpset()));
   2.250 +qed "hypreal_empty_not_mem";
   2.251 +
   2.252 +Addsimps [hypreal_empty_not_mem];
   2.253 +
   2.254 +Goal "Rep_hypreal x ~= {}";
   2.255 +by (cut_inst_tac [("x","x")] Rep_hypreal 1);
   2.256 +by Auto_tac;
   2.257 +qed "Rep_hypreal_nonempty";
   2.258 +
   2.259 +Addsimps [Rep_hypreal_nonempty];
   2.260 +
   2.261 +(*------------------------------------------------------------------------
   2.262 +   hypreal_of_real: the injection from real to hypreal
   2.263 + ------------------------------------------------------------------------*)
   2.264 +
   2.265 +Goal "inj(hypreal_of_real)";
   2.266 +by (rtac injI 1);
   2.267 +by (rewtac hypreal_of_real_def);
   2.268 +by (dtac (inj_on_Abs_hypreal RS inj_onD) 1);
   2.269 +by (REPEAT (rtac hyprel_in_hypreal 1));
   2.270 +by (dtac eq_equiv_class 1);
   2.271 +by (rtac equiv_hyprel 1);
   2.272 +by (Fast_tac 1);
   2.273 +by (rtac ccontr 1 THEN rotate_tac 1 1);
   2.274 +by Auto_tac;
   2.275 +qed "inj_hypreal_of_real";
   2.276 +
   2.277 +val [prem] = goal thy
   2.278 +    "(!!x y. z = Abs_hypreal(hyprel^^{x}) ==> P) ==> P";
   2.279 +by (res_inst_tac [("x1","z")] 
   2.280 +    (rewrite_rule [hypreal_def] Rep_hypreal RS quotientE) 1);
   2.281 +by (dres_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   2.282 +by (res_inst_tac [("x","x")] prem 1);
   2.283 +by (asm_full_simp_tac (simpset() addsimps [Rep_hypreal_inverse]) 1);
   2.284 +qed "eq_Abs_hypreal";
   2.285 +
   2.286 +(**** hypreal_minus: additive inverse on hypreal ****)
   2.287 +
   2.288 +Goalw [congruent_def]
   2.289 +  "congruent hyprel (%X. hyprel^^{%n. - (X n)})";
   2.290 +by Safe_tac;
   2.291 +by (ALLGOALS Ultra_tac);
   2.292 +qed "hypreal_minus_congruent";
   2.293 +
   2.294 +(*Resolve th against the corresponding facts for hypreal_minus*)
   2.295 +val hypreal_minus_ize = RSLIST [equiv_hyprel, hypreal_minus_congruent];
   2.296 +
   2.297 +Goalw [hypreal_minus_def]
   2.298 +      "- (Abs_hypreal(hyprel^^{%n. X n})) = Abs_hypreal(hyprel ^^ {%n. -(X n)})";
   2.299 +by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   2.300 +by (simp_tac (simpset() addsimps 
   2.301 +   [hyprel_in_hypreal RS Abs_hypreal_inverse,hypreal_minus_ize UN_equiv_class]) 1);
   2.302 +qed "hypreal_minus";
   2.303 +
   2.304 +Goal "- (- z) = (z::hypreal)";
   2.305 +by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   2.306 +by (asm_simp_tac (simpset() addsimps [hypreal_minus]) 1);
   2.307 +qed "hypreal_minus_minus";
   2.308 +
   2.309 +Addsimps [hypreal_minus_minus];
   2.310 +
   2.311 +Goal "inj(%r::hypreal. -r)";
   2.312 +by (rtac injI 1);
   2.313 +by (dres_inst_tac [("f","uminus")] arg_cong 1);
   2.314 +by (asm_full_simp_tac (simpset() addsimps [hypreal_minus_minus]) 1);
   2.315 +qed "inj_hypreal_minus";
   2.316 +
   2.317 +Goalw [hypreal_zero_def] "-0hr = 0hr";
   2.318 +by (simp_tac (simpset() addsimps [hypreal_minus]) 1);
   2.319 +qed "hypreal_minus_zero";
   2.320 +
   2.321 +Addsimps [hypreal_minus_zero];
   2.322 +
   2.323 +Goal "(-x = 0hr) = (x = 0hr)"; 
   2.324 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   2.325 +by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def,
   2.326 +    hypreal_minus] @ real_add_ac));
   2.327 +qed "hypreal_minus_zero_iff";
   2.328 +
   2.329 +Addsimps [hypreal_minus_zero_iff];
   2.330 +(**** hrinv: multiplicative inverse on hypreal ****)
   2.331 +
   2.332 +Goalw [congruent_def]
   2.333 +  "congruent hyprel (%X. hyprel^^{%n. if X n = 0r then 0r else rinv(X n)})";
   2.334 +by (Auto_tac THEN Ultra_tac 1);
   2.335 +qed "hypreal_hrinv_congruent";
   2.336 +
   2.337 +(* Resolve th against the corresponding facts for hrinv *)
   2.338 +val hypreal_hrinv_ize = RSLIST [equiv_hyprel, hypreal_hrinv_congruent];
   2.339 +
   2.340 +Goalw [hrinv_def]
   2.341 +      "hrinv (Abs_hypreal(hyprel^^{%n. X n})) = \
   2.342 +\      Abs_hypreal(hyprel ^^ {%n. if X n = 0r then 0r else rinv(X n)})";
   2.343 +by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   2.344 +by (simp_tac (simpset() addsimps 
   2.345 +   [hyprel_in_hypreal RS Abs_hypreal_inverse,hypreal_hrinv_ize UN_equiv_class]) 1);
   2.346 +qed "hypreal_hrinv";
   2.347 +
   2.348 +Goal "z ~= 0hr ==> hrinv (hrinv z) = z";
   2.349 +by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   2.350 +by (rotate_tac 1 1);
   2.351 +by (asm_full_simp_tac (simpset() addsimps 
   2.352 +    [hypreal_hrinv,hypreal_zero_def] setloop (split_tac [expand_if])) 1);
   2.353 +by (ultra_tac (claset() addDs [rinv_not_zero,real_rinv_rinv],simpset()) 1);
   2.354 +qed "hypreal_hrinv_hrinv";
   2.355 +
   2.356 +Addsimps [hypreal_hrinv_hrinv];
   2.357 +
   2.358 +Goalw [hypreal_one_def] "hrinv(1hr) = 1hr";
   2.359 +by (full_simp_tac (simpset() addsimps [hypreal_hrinv,
   2.360 +       real_zero_not_eq_one RS not_sym] 
   2.361 +                   setloop (split_tac [expand_if])) 1);
   2.362 +qed "hypreal_hrinv_1";
   2.363 +Addsimps [hypreal_hrinv_1];
   2.364 +
   2.365 +(**** hyperreal addition: hypreal_add  ****)
   2.366 +
   2.367 +Goalw [congruent2_def]
   2.368 +    "congruent2 hyprel (%X Y. hyprel^^{%n. X n + Y n})";
   2.369 +by Safe_tac;
   2.370 +by (ALLGOALS(Ultra_tac));
   2.371 +qed "hypreal_add_congruent2";
   2.372 +
   2.373 +(*Resolve th against the corresponding facts for hyppreal_add*)
   2.374 +val hypreal_add_ize = RSLIST [equiv_hyprel, hypreal_add_congruent2];
   2.375 +
   2.376 +Goalw [hypreal_add_def]
   2.377 +  "Abs_hypreal(hyprel^^{%n. X n}) + Abs_hypreal(hyprel^^{%n. Y n}) = \
   2.378 +\  Abs_hypreal(hyprel^^{%n. X n + Y n})";
   2.379 +by (asm_simp_tac
   2.380 +    (simpset() addsimps [hypreal_add_ize UN_equiv_class2]) 1);
   2.381 +qed "hypreal_add";
   2.382 +
   2.383 +Goal "(z::hypreal) + w = w + z";
   2.384 +by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   2.385 +by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
   2.386 +by (asm_simp_tac (simpset() addsimps (real_add_ac @ [hypreal_add])) 1);
   2.387 +qed "hypreal_add_commute";
   2.388 +
   2.389 +Goal "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)";
   2.390 +by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
   2.391 +by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
   2.392 +by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
   2.393 +by (asm_simp_tac (simpset() addsimps [hypreal_add, real_add_assoc]) 1);
   2.394 +qed "hypreal_add_assoc";
   2.395 +
   2.396 +(*For AC rewriting*)
   2.397 +Goal "(x::hypreal)+(y+z)=y+(x+z)";
   2.398 +by (rtac (hypreal_add_commute RS trans) 1);
   2.399 +by (rtac (hypreal_add_assoc RS trans) 1);
   2.400 +by (rtac (hypreal_add_commute RS arg_cong) 1);
   2.401 +qed "hypreal_add_left_commute";
   2.402 +
   2.403 +(* hypreal addition is an AC operator *)
   2.404 +val hypreal_add_ac = [hypreal_add_assoc,hypreal_add_commute,
   2.405 +                      hypreal_add_left_commute];
   2.406 +
   2.407 +Goalw [hypreal_zero_def] "0hr + z = z";
   2.408 +by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   2.409 +by (asm_full_simp_tac (simpset() addsimps 
   2.410 +    [hypreal_add]) 1);
   2.411 +qed "hypreal_add_zero_left";
   2.412 +
   2.413 +Goal "z + 0hr = z";
   2.414 +by (simp_tac (simpset() addsimps 
   2.415 +    [hypreal_add_zero_left,hypreal_add_commute]) 1);
   2.416 +qed "hypreal_add_zero_right";
   2.417 +
   2.418 +Goalw [hypreal_zero_def] "z + -z = 0hr";
   2.419 +by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   2.420 +by (asm_full_simp_tac (simpset() addsimps [hypreal_minus,
   2.421 +        hypreal_add]) 1);
   2.422 +qed "hypreal_add_minus";
   2.423 +
   2.424 +Goal "-z + z = 0hr";
   2.425 +by (simp_tac (simpset() addsimps 
   2.426 +    [hypreal_add_commute,hypreal_add_minus]) 1);
   2.427 +qed "hypreal_add_minus_left";
   2.428 +
   2.429 +Addsimps [hypreal_add_minus,hypreal_add_minus_left,
   2.430 +          hypreal_add_zero_left,hypreal_add_zero_right];
   2.431 +
   2.432 +Goal "? y. (x::hypreal) + y = 0hr";
   2.433 +by (fast_tac (claset() addIs [hypreal_add_minus]) 1);
   2.434 +qed "hypreal_minus_ex";
   2.435 +
   2.436 +Goal "?! y. (x::hypreal) + y = 0hr";
   2.437 +by (auto_tac (claset() addIs [hypreal_add_minus],simpset()));
   2.438 +by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
   2.439 +by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   2.440 +by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   2.441 +qed "hypreal_minus_ex1";
   2.442 +
   2.443 +Goal "?! y. y + (x::hypreal) = 0hr";
   2.444 +by (auto_tac (claset() addIs [hypreal_add_minus_left],simpset()));
   2.445 +by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
   2.446 +by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
   2.447 +by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   2.448 +qed "hypreal_minus_left_ex1";
   2.449 +
   2.450 +Goal "x + y = 0hr ==> x = -y";
   2.451 +by (cut_inst_tac [("z","y")] hypreal_add_minus_left 1);
   2.452 +by (res_inst_tac [("x1","y")] (hypreal_minus_left_ex1 RS ex1E) 1);
   2.453 +by (Blast_tac 1);
   2.454 +qed "hypreal_add_minus_eq_minus";
   2.455 +
   2.456 +Goal "? y::hypreal. x = -y";
   2.457 +by (cut_inst_tac [("x","x")] hypreal_minus_ex 1);
   2.458 +by (etac exE 1 THEN dtac hypreal_add_minus_eq_minus 1);
   2.459 +by (Fast_tac 1);
   2.460 +qed "hypreal_as_add_inverse_ex";
   2.461 +
   2.462 +Goal "-(x + (y::hypreal)) = -x + -y";
   2.463 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   2.464 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   2.465 +by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
   2.466 +    hypreal_add,real_minus_add_distrib]));
   2.467 +qed "hypreal_minus_add_distrib";
   2.468 +
   2.469 +Goal "-(y + -(x::hypreal)) = x + -y";
   2.470 +by (simp_tac (simpset() addsimps [hypreal_minus_add_distrib,
   2.471 +    hypreal_add_commute]) 1);
   2.472 +qed "hypreal_minus_distrib1";
   2.473 +
   2.474 +Goal "(x + - (y::hypreal)) + (y + - z) = x + -z";
   2.475 +by (res_inst_tac [("w1","y")] (hypreal_add_commute RS subst) 1);
   2.476 +by (simp_tac (simpset() addsimps [hypreal_add_left_commute,
   2.477 +    hypreal_add_assoc]) 1);
   2.478 +by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   2.479 +qed "hypreal_add_minus_cancel1";
   2.480 +
   2.481 +Goal "((x::hypreal) + y = x + z) = (y = z)";
   2.482 +by (Step_tac 1);
   2.483 +by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1);
   2.484 +by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   2.485 +qed "hypreal_add_left_cancel";
   2.486 +
   2.487 +Goal "z + (x + (y + -z)) = x + (y::hypreal)";
   2.488 +by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
   2.489 +qed "hypreal_add_minus_cancel2";
   2.490 +Addsimps [hypreal_add_minus_cancel2];
   2.491 +
   2.492 +Goal "y + -(x + y) = -(x::hypreal)";
   2.493 +by (full_simp_tac (simpset() addsimps [hypreal_minus_add_distrib]) 1);
   2.494 +by (rtac (hypreal_add_left_commute RS subst) 1);
   2.495 +by (Full_simp_tac 1);
   2.496 +qed "hypreal_add_minus_cancel";
   2.497 +Addsimps [hypreal_add_minus_cancel];
   2.498 +
   2.499 +Goal "y + -(y + x) = -(x::hypreal)";
   2.500 +by (simp_tac (simpset() addsimps [hypreal_minus_add_distrib,
   2.501 +              hypreal_add_assoc RS sym]) 1);
   2.502 +qed "hypreal_add_minus_cancelc";
   2.503 +Addsimps [hypreal_add_minus_cancelc];
   2.504 +
   2.505 +Goal "(z + -x) + (y + -z) = (y + -(x::hypreal))";
   2.506 +by (full_simp_tac (simpset() addsimps [hypreal_minus_add_distrib
   2.507 +    RS sym, hypreal_add_left_cancel] @ hypreal_add_ac) 1); 
   2.508 +qed "hypreal_add_minus_cancel3";
   2.509 +Addsimps [hypreal_add_minus_cancel3];
   2.510 +
   2.511 +Goal "(y + (x::hypreal)= z + x) = (y = z)";
   2.512 +by (simp_tac (simpset() addsimps [hypreal_add_commute,
   2.513 +    hypreal_add_left_cancel]) 1);
   2.514 +qed "hypreal_add_right_cancel";
   2.515 +
   2.516 +Goal "z + (y + -z) = (y::hypreal)";
   2.517 +by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
   2.518 +qed "hypreal_add_minus_cancel4";
   2.519 +Addsimps [hypreal_add_minus_cancel4];
   2.520 +
   2.521 +Goal "z + (w + (x + (-z + y))) = w + x + (y::hypreal)";
   2.522 +by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
   2.523 +qed "hypreal_add_minus_cancel5";
   2.524 +Addsimps [hypreal_add_minus_cancel5];
   2.525 +
   2.526 +
   2.527 +(**** hyperreal multiplication: hypreal_mult  ****)
   2.528 +
   2.529 +Goalw [congruent2_def]
   2.530 +    "congruent2 hyprel (%X Y. hyprel^^{%n. X n * Y n})";
   2.531 +by Safe_tac;
   2.532 +by (ALLGOALS(Ultra_tac));
   2.533 +qed "hypreal_mult_congruent2";
   2.534 +
   2.535 +(*Resolve th against the corresponding facts for hypreal_mult*)
   2.536 +val hypreal_mult_ize = RSLIST [equiv_hyprel, hypreal_mult_congruent2];
   2.537 +
   2.538 +Goalw [hypreal_mult_def]
   2.539 +  "Abs_hypreal(hyprel^^{%n. X n}) * Abs_hypreal(hyprel^^{%n. Y n}) = \
   2.540 +\  Abs_hypreal(hyprel^^{%n. X n * Y n})";
   2.541 +by (asm_simp_tac
   2.542 +    (simpset() addsimps [hypreal_mult_ize UN_equiv_class2]) 1);
   2.543 +qed "hypreal_mult";
   2.544 +
   2.545 +Goal "(z::hypreal) * w = w * z";
   2.546 +by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   2.547 +by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
   2.548 +by (asm_simp_tac (simpset() addsimps ([hypreal_mult] @ real_mult_ac)) 1);
   2.549 +qed "hypreal_mult_commute";
   2.550 +
   2.551 +Goal "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)";
   2.552 +by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
   2.553 +by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
   2.554 +by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
   2.555 +by (asm_simp_tac (simpset() addsimps [hypreal_mult,real_mult_assoc]) 1);
   2.556 +qed "hypreal_mult_assoc";
   2.557 +
   2.558 +qed_goal "hypreal_mult_left_commute" thy
   2.559 +    "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)"
   2.560 + (fn _ => [rtac (hypreal_mult_commute RS trans) 1, rtac (hypreal_mult_assoc RS trans) 1,
   2.561 +           rtac (hypreal_mult_commute RS arg_cong) 1]);
   2.562 +
   2.563 +(* hypreal multiplication is an AC operator *)
   2.564 +val hypreal_mult_ac = [hypreal_mult_assoc, hypreal_mult_commute, 
   2.565 +                       hypreal_mult_left_commute];
   2.566 +
   2.567 +Goalw [hypreal_one_def] "1hr * z = z";
   2.568 +by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   2.569 +by (asm_full_simp_tac (simpset() addsimps [hypreal_mult]) 1);
   2.570 +qed "hypreal_mult_1";
   2.571 +
   2.572 +Goal "z * 1hr = z";
   2.573 +by (simp_tac (simpset() addsimps [hypreal_mult_commute,
   2.574 +    hypreal_mult_1]) 1);
   2.575 +qed "hypreal_mult_1_right";
   2.576 +
   2.577 +Goalw [hypreal_zero_def] "0hr * z = 0hr";
   2.578 +by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   2.579 +by (asm_full_simp_tac (simpset() addsimps [hypreal_mult,real_mult_0]) 1);
   2.580 +qed "hypreal_mult_0";
   2.581 +
   2.582 +Goal "z * 0hr = 0hr";
   2.583 +by (simp_tac (simpset() addsimps [hypreal_mult_commute,
   2.584 +    hypreal_mult_0]) 1);
   2.585 +qed "hypreal_mult_0_right";
   2.586 +
   2.587 +Addsimps [hypreal_mult_0,hypreal_mult_0_right];
   2.588 +
   2.589 +Goal "-(x * y) = -x * (y::hypreal)";
   2.590 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   2.591 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   2.592 +by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
   2.593 +    hypreal_mult,real_minus_mult_eq1] 
   2.594 +      @ real_mult_ac @ real_add_ac));
   2.595 +qed "hypreal_minus_mult_eq1";
   2.596 +
   2.597 +Goal "-(x * y) = (x::hypreal) * -y";
   2.598 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   2.599 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   2.600 +by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
   2.601 +   hypreal_mult,real_minus_mult_eq2] 
   2.602 +    @ real_mult_ac @ real_add_ac));
   2.603 +qed "hypreal_minus_mult_eq2";
   2.604 +
   2.605 +Goal "-x*-y = x*(y::hypreal)";
   2.606 +by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym,
   2.607 +    hypreal_minus_mult_eq1 RS sym]) 1);
   2.608 +qed "hypreal_minus_mult_cancel";
   2.609 +
   2.610 +Addsimps [hypreal_minus_mult_cancel];
   2.611 +
   2.612 +Goal "-x*y = (x::hypreal)*-y";
   2.613 +by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym,
   2.614 +    hypreal_minus_mult_eq1 RS sym]) 1);
   2.615 +qed "hypreal_minus_mult_commute";
   2.616 +
   2.617 +
   2.618 +(*-----------------------------------------------------------------------------
   2.619 +    A few more theorems
   2.620 + ----------------------------------------------------------------------------*)
   2.621 +Goal "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
   2.622 +by (asm_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   2.623 +qed "hypreal_add_assoc_cong";
   2.624 +
   2.625 +Goal "(z::hypreal) + (v + w) = v + (z + w)";
   2.626 +by (REPEAT (ares_tac [hypreal_add_commute RS hypreal_add_assoc_cong] 1));
   2.627 +qed "hypreal_add_assoc_swap";
   2.628 +
   2.629 +Goal "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)";
   2.630 +by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
   2.631 +by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
   2.632 +by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
   2.633 +by (asm_simp_tac (simpset() addsimps [hypreal_mult,hypreal_add,
   2.634 +     real_add_mult_distrib]) 1);
   2.635 +qed "hypreal_add_mult_distrib";
   2.636 +
   2.637 +val hypreal_mult_commute'= read_instantiate [("z","w")] hypreal_mult_commute;
   2.638 +
   2.639 +Goal "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)";
   2.640 +by (simp_tac (simpset() addsimps [hypreal_mult_commute',hypreal_add_mult_distrib]) 1);
   2.641 +qed "hypreal_add_mult_distrib2";
   2.642 +
   2.643 +val hypreal_mult_simps = [hypreal_mult_1, hypreal_mult_1_right];
   2.644 +Addsimps hypreal_mult_simps;
   2.645 +
   2.646 +(*** one and zero are distinct ***)
   2.647 +Goalw [hypreal_zero_def,hypreal_one_def] "0hr ~= 1hr";
   2.648 +by (auto_tac (claset(),simpset() addsimps [real_zero_not_eq_one]));
   2.649 +qed "hypreal_zero_not_eq_one";
   2.650 +
   2.651 +(*** existence of inverse ***)
   2.652 +Goalw [hypreal_one_def,hypreal_zero_def] 
   2.653 +          "x ~= 0hr ==> x*hrinv(x) = 1hr";
   2.654 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   2.655 +by (rotate_tac 1 1);
   2.656 +by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
   2.657 +    hypreal_mult] setloop (split_tac [expand_if])) 1);
   2.658 +by (dtac FreeUltrafilterNat_Compl_mem 1);
   2.659 +by (blast_tac (claset() addSIs [real_mult_inv_right,
   2.660 +    FreeUltrafilterNat_subset]) 1);
   2.661 +qed "hypreal_mult_hrinv";
   2.662 +
   2.663 +Goal "x ~= 0hr ==> hrinv(x)*x = 1hr";
   2.664 +by (asm_simp_tac (simpset() addsimps [hypreal_mult_hrinv,
   2.665 +    hypreal_mult_commute]) 1);
   2.666 +qed "hypreal_mult_hrinv_left";
   2.667 +
   2.668 +Goal "x ~= 0hr ==> ? y. (x::hypreal) * y = 1hr";
   2.669 +by (fast_tac (claset() addDs [hypreal_mult_hrinv]) 1);
   2.670 +qed "hypreal_hrinv_ex";
   2.671 +
   2.672 +Goal "x ~= 0hr ==> ? y. y * (x::hypreal) = 1hr";
   2.673 +by (fast_tac (claset() addDs [hypreal_mult_hrinv_left]) 1);
   2.674 +qed "hypreal_hrinv_left_ex";
   2.675 +
   2.676 +Goal "x ~= 0hr ==> ?! y. (x::hypreal) * y = 1hr";
   2.677 +by (auto_tac (claset() addIs [hypreal_mult_hrinv],simpset()));
   2.678 +by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
   2.679 +by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
   2.680 +by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
   2.681 +qed "hypreal_hrinv_ex1";
   2.682 +
   2.683 +Goal "x ~= 0hr ==> ?! y. y * (x::hypreal) = 1hr";
   2.684 +by (auto_tac (claset() addIs [hypreal_mult_hrinv_left],simpset()));
   2.685 +by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
   2.686 +by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
   2.687 +by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
   2.688 +qed "hypreal_hrinv_left_ex1";
   2.689 +
   2.690 +Goal "[| y~= 0hr; x * y = 1hr |]  ==> x = hrinv y";
   2.691 +by (forw_inst_tac [("x","y")] hypreal_mult_hrinv_left 1);
   2.692 +by (res_inst_tac [("x1","y")] (hypreal_hrinv_left_ex1 RS ex1E) 1);
   2.693 +by (assume_tac 1);
   2.694 +by (Blast_tac 1);
   2.695 +qed "hypreal_mult_inv_hrinv";
   2.696 +
   2.697 +Goal "x ~= 0hr ==> ? y. x = hrinv y";
   2.698 +by (forw_inst_tac [("x","x")] hypreal_hrinv_left_ex 1);
   2.699 +by (etac exE 1 THEN 
   2.700 +    forw_inst_tac [("x","y")] hypreal_mult_inv_hrinv 1);
   2.701 +by (res_inst_tac [("x","y")] exI 2);
   2.702 +by Auto_tac;
   2.703 +qed "hypreal_as_inverse_ex";
   2.704 +
   2.705 +Goal "(c::hypreal) ~= 0hr ==> (c*a=c*b) = (a=b)";
   2.706 +by Auto_tac;
   2.707 +by (dres_inst_tac [("f","%x. x*hrinv c")] arg_cong 1);
   2.708 +by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_hrinv] @ hypreal_mult_ac)  1);
   2.709 +qed "hypreal_mult_left_cancel";
   2.710 +    
   2.711 +Goal "(c::hypreal) ~= 0hr ==> (a*c=b*c) = (a=b)";
   2.712 +by (Step_tac 1);
   2.713 +by (dres_inst_tac [("f","%x. x*hrinv c")] arg_cong 1);
   2.714 +by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_hrinv] @ hypreal_mult_ac)  1);
   2.715 +qed "hypreal_mult_right_cancel";
   2.716 +
   2.717 +Goalw [hypreal_zero_def] "x ~= 0hr ==> hrinv(x) ~= 0hr";
   2.718 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   2.719 +by (rotate_tac 1 1);
   2.720 +by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
   2.721 +    hypreal_mult] setloop (split_tac [expand_if])) 1);
   2.722 +by (dtac FreeUltrafilterNat_Compl_mem 1 THEN Clarify_tac 1);
   2.723 +by (ultra_tac (claset() addIs [ccontr] addDs 
   2.724 +    [rinv_not_zero],simpset()) 1);
   2.725 +qed "hrinv_not_zero";
   2.726 +
   2.727 +Addsimps [hypreal_mult_hrinv,hypreal_mult_hrinv_left];
   2.728 +
   2.729 +Goal "[| x ~= 0hr; y ~= 0hr |] ==> x * y ~= 0hr";
   2.730 +by (Step_tac 1);
   2.731 +by (dres_inst_tac [("f","%z. hrinv x*z")] arg_cong 1);
   2.732 +by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
   2.733 +qed "hypreal_mult_not_0";
   2.734 +
   2.735 +bind_thm ("hypreal_mult_not_0E",hypreal_mult_not_0 RS notE);
   2.736 +
   2.737 +Goal "x ~= 0hr ==> x * x ~= 0hr";
   2.738 +by (blast_tac (claset() addDs [hypreal_mult_not_0]) 1);
   2.739 +qed "hypreal_mult_self_not_zero";
   2.740 +
   2.741 +Goal "[| x ~= 0hr; y ~= 0hr |] ==> hrinv(x*y) = hrinv(x)*hrinv(y)";
   2.742 +by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
   2.743 +by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,
   2.744 +    hypreal_mult_not_0]));
   2.745 +by (res_inst_tac [("c1","y")] (hypreal_mult_right_cancel RS iffD1) 1);
   2.746 +by (auto_tac (claset(),simpset() addsimps [hypreal_mult_not_0] @ hypreal_mult_ac));
   2.747 +by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,hypreal_mult_not_0]));
   2.748 +qed "hrinv_mult_eq";
   2.749 +
   2.750 +Goal "x ~= 0hr ==> hrinv(-x) = -hrinv(x)";
   2.751 +by (res_inst_tac [("c1","-x")] (hypreal_mult_right_cancel RS iffD1) 1);
   2.752 +by Auto_tac;
   2.753 +qed "hypreal_minus_hrinv";
   2.754 +
   2.755 +Goal "[| x ~= 0hr; y ~= 0hr |] \
   2.756 +\     ==> hrinv(x*y) = hrinv(x)*hrinv(y)";
   2.757 +by (forw_inst_tac [("y","y")] hypreal_mult_not_0 1 THEN assume_tac 1);
   2.758 +by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
   2.759 +by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym]));
   2.760 +by (res_inst_tac [("c1","y")] (hypreal_mult_left_cancel RS iffD1) 1);
   2.761 +by (auto_tac (claset(),simpset() addsimps [hypreal_mult_left_commute]));
   2.762 +by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
   2.763 +qed "hypreal_hrinv_distrib";
   2.764 +
   2.765 +(*------------------------------------------------------------------
   2.766 +                   Theorems for ordering 
   2.767 + ------------------------------------------------------------------*)
   2.768 +
   2.769 +(* prove introduction and elimination rules for hypreal_less *)
   2.770 +
   2.771 +Goalw [hypreal_less_def]
   2.772 + "P < (Q::hypreal) = (EX X Y. X : Rep_hypreal(P) & \
   2.773 +\                             Y : Rep_hypreal(Q) & \
   2.774 +\                             {n. X n < Y n} : FreeUltrafilterNat)";
   2.775 +by (Fast_tac 1);
   2.776 +qed "hypreal_less_iff";
   2.777 +
   2.778 +Goalw [hypreal_less_def]
   2.779 + "[| {n. X n < Y n} : FreeUltrafilterNat; \
   2.780 +\         X : Rep_hypreal(P); \
   2.781 +\         Y : Rep_hypreal(Q) |] ==> P < (Q::hypreal)";
   2.782 +by (Fast_tac 1);
   2.783 +qed "hypreal_lessI";
   2.784 +
   2.785 +
   2.786 +Goalw [hypreal_less_def]
   2.787 +     "!! R1. [| R1 < (R2::hypreal); \
   2.788 +\         !!X Y. {n. X n < Y n} : FreeUltrafilterNat ==> P; \
   2.789 +\         !!X. X : Rep_hypreal(R1) ==> P; \ 
   2.790 +\         !!Y. Y : Rep_hypreal(R2) ==> P |] \
   2.791 +\     ==> P";
   2.792 +by Auto_tac;
   2.793 +qed "hypreal_lessE";
   2.794 +
   2.795 +Goalw [hypreal_less_def]
   2.796 + "R1 < (R2::hypreal) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \
   2.797 +\                                  X : Rep_hypreal(R1) & \
   2.798 +\                                  Y : Rep_hypreal(R2))";
   2.799 +by (Fast_tac 1);
   2.800 +qed "hypreal_lessD";
   2.801 +
   2.802 +Goal "~ (R::hypreal) < R";
   2.803 +by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
   2.804 +by (auto_tac (claset(),simpset() addsimps [hypreal_less_def]));
   2.805 +by (Ultra_tac 1);
   2.806 +qed "hypreal_less_not_refl";
   2.807 +
   2.808 +(*** y < y ==> P ***)
   2.809 +bind_thm("hypreal_less_irrefl",hypreal_less_not_refl RS notE);
   2.810 +
   2.811 +Goal "!!(x::hypreal). x < y ==> x ~= y";
   2.812 +by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
   2.813 +qed "hypreal_not_refl2";
   2.814 +
   2.815 +Goal "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
   2.816 +by (res_inst_tac [("z","R1")] eq_Abs_hypreal 1);
   2.817 +by (res_inst_tac [("z","R2")] eq_Abs_hypreal 1);
   2.818 +by (res_inst_tac [("z","R3")] eq_Abs_hypreal 1);
   2.819 +by (auto_tac (claset() addSIs [exI],simpset() 
   2.820 +     addsimps [hypreal_less_def]));
   2.821 +by (ultra_tac (claset() addIs [real_less_trans],simpset()) 1);
   2.822 +qed "hypreal_less_trans";
   2.823 +
   2.824 +Goal "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P";
   2.825 +by (dtac hypreal_less_trans 1 THEN assume_tac 1);
   2.826 +by (asm_full_simp_tac (simpset() addsimps 
   2.827 +    [hypreal_less_not_refl]) 1);
   2.828 +qed "hypreal_less_asym";
   2.829 +
   2.830 +(*--------------------------------------------------------
   2.831 +  TODO: The following theorem should have been proved 
   2.832 +  first and then used througout the proofs as it probably 
   2.833 +  makes many of them more straightforward. 
   2.834 + -------------------------------------------------------*)
   2.835 +Goalw [hypreal_less_def]
   2.836 +      "(Abs_hypreal(hyprel^^{%n. X n}) < \
   2.837 +\           Abs_hypreal(hyprel^^{%n. Y n})) = \
   2.838 +\      ({n. X n < Y n} : FreeUltrafilterNat)";
   2.839 +by (auto_tac (claset() addSIs [lemma_hyprel_refl],simpset()));
   2.840 +by (Ultra_tac 1);
   2.841 +qed "hypreal_less";
   2.842 +
   2.843 +(*---------------------------------------------------------------------------------
   2.844 +             Hyperreals as a linearly ordered field
   2.845 + ---------------------------------------------------------------------------------*)
   2.846 +(*** sum order ***)
   2.847 +
   2.848 +Goalw [hypreal_zero_def] 
   2.849 +      "[| 0hr < x; 0hr < y |] ==> 0hr < x + y";
   2.850 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   2.851 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   2.852 +by (auto_tac (claset(),simpset() addsimps
   2.853 +    [hypreal_less_def,hypreal_add]));
   2.854 +by (auto_tac (claset() addSIs [exI],simpset() addsimps
   2.855 +    [hypreal_less_def,hypreal_add]));
   2.856 +by (ultra_tac (claset() addIs [real_add_order],simpset()) 1);
   2.857 +qed "hypreal_add_order";
   2.858 +
   2.859 +(*** mult order ***)
   2.860 +
   2.861 +Goalw [hypreal_zero_def] 
   2.862 +          "[| 0hr < x; 0hr < y |] ==> 0hr < x * y";
   2.863 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   2.864 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   2.865 +by (auto_tac (claset() addSIs [exI],simpset() addsimps
   2.866 +    [hypreal_less_def,hypreal_mult]));
   2.867 +by (ultra_tac (claset() addIs [real_mult_order],simpset()) 1);
   2.868 +qed "hypreal_mult_order";
   2.869 +
   2.870 +(*---------------------------------------------------------------------------------
   2.871 +                         Trichotomy of the hyperreals
   2.872 +  --------------------------------------------------------------------------------*)
   2.873 +
   2.874 +Goalw [hyprel_def] "? x. x: hyprel ^^ {%n. 0r}";
   2.875 +by (res_inst_tac [("x","%n. 0r")] exI 1);
   2.876 +by (Step_tac 1);
   2.877 +by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset()));
   2.878 +qed "lemma_hyprel_0r_mem";
   2.879 +
   2.880 +Goalw [hypreal_zero_def]"0hr <  x | x = 0hr | x < 0hr";
   2.881 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   2.882 +by (auto_tac (claset(),simpset() addsimps [hypreal_less_def]));
   2.883 +by (cut_facts_tac [lemma_hyprel_0r_mem] 1 THEN etac exE 1);
   2.884 +by (dres_inst_tac [("x","xa")] spec 1);
   2.885 +by (dres_inst_tac [("x","x")] spec 1);
   2.886 +by (cut_inst_tac [("x","x")] lemma_hyprel_refl 1);
   2.887 +by Auto_tac;
   2.888 +by (dres_inst_tac [("x","x")] spec 1);
   2.889 +by (dres_inst_tac [("x","xa")] spec 1);
   2.890 +by Auto_tac;
   2.891 +by (Ultra_tac 1);
   2.892 +by (auto_tac (claset() addIs [real_linear_less2],simpset()));
   2.893 +qed "hypreal_trichotomy";
   2.894 +
   2.895 +val prems = Goal "[| 0hr < x ==> P; \
   2.896 +\                 x = 0hr ==> P; \
   2.897 +\                 x < 0hr ==> P |] ==> P";
   2.898 +by (cut_inst_tac [("x","x")] hypreal_trichotomy 1);
   2.899 +by (REPEAT (eresolve_tac (disjE::prems) 1));
   2.900 +qed "hypreal_trichotomyE";
   2.901 +
   2.902 +(*----------------------------------------------------------------------------
   2.903 +            More properties of <
   2.904 + ----------------------------------------------------------------------------*)
   2.905 +Goal "!!(A::hypreal). A < B ==> A + C < B + C";
   2.906 +by (res_inst_tac [("z","A")] eq_Abs_hypreal 1);
   2.907 +by (res_inst_tac [("z","B")] eq_Abs_hypreal 1);
   2.908 +by (res_inst_tac [("z","C")] eq_Abs_hypreal 1);
   2.909 +by (auto_tac (claset() addSIs [exI],simpset() addsimps
   2.910 +    [hypreal_less_def,hypreal_add]));
   2.911 +by (Ultra_tac 1);
   2.912 +qed "hypreal_add_less_mono1";
   2.913 +
   2.914 +Goal "!!(A::hypreal). A < B ==> C + A < C + B";
   2.915 +by (auto_tac (claset() addIs [hypreal_add_less_mono1],
   2.916 +    simpset() addsimps [hypreal_add_commute]));
   2.917 +qed "hypreal_add_less_mono2";
   2.918 +
   2.919 +Goal "((x::hypreal) < y) = (0hr < y + -x)";
   2.920 +by (Step_tac 1);
   2.921 +by (dres_inst_tac [("C","-x")] hypreal_add_less_mono1 1);
   2.922 +by (dres_inst_tac [("C","x")] hypreal_add_less_mono1 2);
   2.923 +by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   2.924 +qed "hypreal_less_minus_iff"; 
   2.925 +
   2.926 +Goal "((x::hypreal) < y) = (x + -y< 0hr)";
   2.927 +by (Step_tac 1);
   2.928 +by (dres_inst_tac [("C","-y")] hypreal_add_less_mono1 1);
   2.929 +by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 2);
   2.930 +by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   2.931 +qed "hypreal_less_minus_iff2";
   2.932 +
   2.933 +Goal  "!!(y1 :: hypreal). [| z1 < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2";
   2.934 +by (dtac (hypreal_less_minus_iff RS iffD1) 1);
   2.935 +by (dtac (hypreal_less_minus_iff RS iffD1) 1);
   2.936 +by (dtac hypreal_add_order 1 THEN assume_tac 1);
   2.937 +by (thin_tac "0hr < y2 + - z2" 1);
   2.938 +by (dres_inst_tac [("C","z1 + z2")] hypreal_add_less_mono1 1);
   2.939 +by (auto_tac (claset(),simpset() addsimps 
   2.940 +    [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac));
   2.941 +qed "hypreal_add_less_mono";
   2.942 +
   2.943 +Goal "((x::hypreal) = y) = (0hr = x + - y)";
   2.944 +by Auto_tac;
   2.945 +by (res_inst_tac [("x1","-y")] (hypreal_add_right_cancel RS iffD1) 1);
   2.946 +by Auto_tac;
   2.947 +qed "hypreal_eq_minus_iff"; 
   2.948 +
   2.949 +Goal "((x::hypreal) = y) = (0hr = y + - x)";
   2.950 +by Auto_tac;
   2.951 +by (res_inst_tac [("x1","-x")] (hypreal_add_right_cancel RS iffD1) 1);
   2.952 +by Auto_tac;
   2.953 +qed "hypreal_eq_minus_iff2"; 
   2.954 +
   2.955 +Goal "(x = y + z) = (x + -z = (y::hypreal))";
   2.956 +by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   2.957 +qed "hypreal_eq_minus_iff3";
   2.958 +
   2.959 +Goal "(x = z + y) = (x + -z = (y::hypreal))";
   2.960 +by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
   2.961 +qed "hypreal_eq_minus_iff4";
   2.962 +
   2.963 +Goal "(x ~= a) = (x + -a ~= 0hr)";
   2.964 +by (auto_tac (claset() addDs [sym RS 
   2.965 +    (hypreal_eq_minus_iff RS iffD2)],simpset())); 
   2.966 +qed "hypreal_not_eq_minus_iff";
   2.967 +
   2.968 +(*** linearity ***)
   2.969 +Goal "(x::hypreal) < y | x = y | y < x";
   2.970 +by (rtac (hypreal_eq_minus_iff2 RS ssubst) 1);
   2.971 +by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1);
   2.972 +by (res_inst_tac [("x1","y")] (hypreal_less_minus_iff2 RS ssubst) 1);
   2.973 +by (rtac hypreal_trichotomyE 1);
   2.974 +by Auto_tac;
   2.975 +qed "hypreal_linear";
   2.976 +
   2.977 +Goal "!!(x::hypreal). [| x < y ==> P;  x = y ==> P; \
   2.978 +\          y < x ==> P |] ==> P";
   2.979 +by (cut_inst_tac [("x","x"),("y","y")] hypreal_linear 1);
   2.980 +by Auto_tac;
   2.981 +qed "hypreal_linear_less2";
   2.982 +
   2.983 +(*------------------------------------------------------------------------------
   2.984 +                            Properties of <=
   2.985 + ------------------------------------------------------------------------------*)
   2.986 +(*------ hypreal le iff reals le a.e ------*)
   2.987 +
   2.988 +Goalw [hypreal_le_def,real_le_def]
   2.989 +      "(Abs_hypreal(hyprel^^{%n. X n}) <= \
   2.990 +\           Abs_hypreal(hyprel^^{%n. Y n})) = \
   2.991 +\      ({n. X n <= Y n} : FreeUltrafilterNat)";
   2.992 +by (auto_tac (claset(),simpset() addsimps [hypreal_less]));
   2.993 +by (ALLGOALS(Ultra_tac));
   2.994 +qed "hypreal_le";
   2.995 +
   2.996 +(*---------------------------------------------------------*)
   2.997 +(*---------------------------------------------------------*)
   2.998 +Goalw [hypreal_le_def] 
   2.999 +     "~(w < z) ==> z <= (w::hypreal)";
  2.1000 +by (assume_tac 1);
  2.1001 +qed "hypreal_leI";
  2.1002 +
  2.1003 +Goalw [hypreal_le_def] 
  2.1004 +      "z<=w ==> ~(w<(z::hypreal))";
  2.1005 +by (assume_tac 1);
  2.1006 +qed "hypreal_leD";
  2.1007 +
  2.1008 +val hypreal_leE = make_elim hypreal_leD;
  2.1009 +
  2.1010 +Goal "(~(w < z)) = (z <= (w::hypreal))";
  2.1011 +by (fast_tac (claset() addSIs [hypreal_leI,hypreal_leD]) 1);
  2.1012 +qed "hypreal_less_le_iff";
  2.1013 +
  2.1014 +Goalw [hypreal_le_def] "~ z <= w ==> w<(z::hypreal)";
  2.1015 +by (Fast_tac 1);
  2.1016 +qed "not_hypreal_leE";
  2.1017 +
  2.1018 +Goalw [hypreal_le_def] "z < w ==> z <= (w::hypreal)";
  2.1019 +by (fast_tac (claset() addEs [hypreal_less_asym]) 1);
  2.1020 +qed "hypreal_less_imp_le";
  2.1021 +
  2.1022 +Goalw [hypreal_le_def] "!!(x::hypreal). x <= y ==> x < y | x = y";
  2.1023 +by (cut_facts_tac [hypreal_linear] 1);
  2.1024 +by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1);
  2.1025 +qed "hypreal_le_imp_less_or_eq";
  2.1026 +
  2.1027 +Goalw [hypreal_le_def] "z<w | z=w ==> z <=(w::hypreal)";
  2.1028 +by (cut_facts_tac [hypreal_linear] 1);
  2.1029 +by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1);
  2.1030 +qed "hypreal_less_or_eq_imp_le";
  2.1031 +
  2.1032 +Goal "(x <= (y::hypreal)) = (x < y | x=y)";
  2.1033 +by (REPEAT(ares_tac [iffI, hypreal_less_or_eq_imp_le, hypreal_le_imp_less_or_eq] 1));
  2.1034 +qed "hypreal_le_eq_less_or_eq";
  2.1035 +
  2.1036 +Goal "w <= (w::hypreal)";
  2.1037 +by (simp_tac (simpset() addsimps [hypreal_le_eq_less_or_eq]) 1);
  2.1038 +qed "hypreal_le_refl";
  2.1039 +Addsimps [hypreal_le_refl];
  2.1040 +
  2.1041 +Goal "[| i <= j; j < k |] ==> i < (k::hypreal)";
  2.1042 +by (dtac hypreal_le_imp_less_or_eq 1);
  2.1043 +by (fast_tac (claset() addIs [hypreal_less_trans]) 1);
  2.1044 +qed "hypreal_le_less_trans";
  2.1045 +
  2.1046 +Goal "!! (i::hypreal). [| i < j; j <= k |] ==> i < k";
  2.1047 +by (dtac hypreal_le_imp_less_or_eq 1);
  2.1048 +by (fast_tac (claset() addIs [hypreal_less_trans]) 1);
  2.1049 +qed "hypreal_less_le_trans";
  2.1050 +
  2.1051 +Goal "[| i <= j; j <= k |] ==> i <= (k::hypreal)";
  2.1052 +by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq,
  2.1053 +            rtac hypreal_less_or_eq_imp_le, fast_tac (claset() addIs [hypreal_less_trans])]);
  2.1054 +qed "hypreal_le_trans";
  2.1055 +
  2.1056 +Goal "[| z <= w; w <= z |] ==> z = (w::hypreal)";
  2.1057 +by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq,
  2.1058 +            fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym])]);
  2.1059 +qed "hypreal_le_anti_sym";
  2.1060 +
  2.1061 +Goal "[| 0hr < x; 0hr <= y |] ==> 0hr < x + y";
  2.1062 +by (auto_tac (claset() addDs [sym,hypreal_le_imp_less_or_eq]
  2.1063 +              addIs [hypreal_add_order],simpset()));
  2.1064 +qed "hypreal_add_order_le";            
  2.1065 +
  2.1066 +(*------------------------------------------------------------------------
  2.1067 + ------------------------------------------------------------------------*)
  2.1068 +
  2.1069 +Goal "[| ~ y < x; y ~= x |] ==> x < (y::hypreal)";
  2.1070 +by (rtac not_hypreal_leE 1);
  2.1071 +by (fast_tac (claset() addDs [hypreal_le_imp_less_or_eq]) 1);
  2.1072 +qed "not_less_not_eq_hypreal_less";
  2.1073 +
  2.1074 +Goal "(0hr < -R) = (R < 0hr)";
  2.1075 +by (Step_tac 1);
  2.1076 +by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1);
  2.1077 +by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2);
  2.1078 +by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
  2.1079 +qed "hypreal_minus_zero_less_iff";
  2.1080 +
  2.1081 +Goal "(-R < 0hr) = (0hr < R)";
  2.1082 +by (Step_tac 1);
  2.1083 +by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1);
  2.1084 +by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2);
  2.1085 +by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
  2.1086 +qed "hypreal_minus_zero_less_iff2";
  2.1087 +
  2.1088 +Goal "((x::hypreal) < y) = (-y < -x)";
  2.1089 +by (rtac (hypreal_less_minus_iff RS ssubst) 1);
  2.1090 +by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1);
  2.1091 +by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
  2.1092 +qed "hypreal_less_swap_iff";
  2.1093 +
  2.1094 +Goal "(0hr < x) = (-x < x)";
  2.1095 +by (Step_tac 1);
  2.1096 +by (rtac ccontr 2 THEN forward_tac 
  2.1097 +    [hypreal_leI RS hypreal_le_imp_less_or_eq] 2);
  2.1098 +by (Step_tac 2);
  2.1099 +by (dtac (hypreal_minus_zero_less_iff RS iffD2) 2);
  2.1100 +by (dres_inst_tac [("R2.0","-x")] hypreal_less_trans 2);
  2.1101 +by (Auto_tac );
  2.1102 +by (forward_tac [hypreal_add_order] 1 THEN assume_tac 1);
  2.1103 +by (dres_inst_tac [("C","-x"),("B","x + x")] hypreal_add_less_mono1 1);
  2.1104 +by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
  2.1105 +qed "hypreal_gt_zero_iff";
  2.1106 +
  2.1107 +Goal "(x < 0hr) = (x < -x)";
  2.1108 +by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
  2.1109 +by (rtac (hypreal_gt_zero_iff RS ssubst) 1);
  2.1110 +by (Full_simp_tac 1);
  2.1111 +qed "hypreal_lt_zero_iff";
  2.1112 +
  2.1113 +Goalw [hypreal_le_def] "(0hr <= x) = (-x <= x)";
  2.1114 +by (auto_tac (claset(),simpset() addsimps [hypreal_lt_zero_iff RS sym]));
  2.1115 +qed "hypreal_ge_zero_iff";
  2.1116 +
  2.1117 +Goalw [hypreal_le_def] "(x <= 0hr) = (x <= -x)";
  2.1118 +by (auto_tac (claset(),simpset() addsimps [hypreal_gt_zero_iff RS sym]));
  2.1119 +qed "hypreal_le_zero_iff";
  2.1120 +
  2.1121 +Goal "[| x < 0hr; y < 0hr |] ==> 0hr < x * y";
  2.1122 +by (REPEAT(dtac (hypreal_minus_zero_less_iff RS iffD2) 1));
  2.1123 +by (dtac hypreal_mult_order 1 THEN assume_tac 1);
  2.1124 +by (Asm_full_simp_tac 1);
  2.1125 +qed "hypreal_mult_less_zero1";
  2.1126 +
  2.1127 +Goal "[| 0hr <= x; 0hr <= y |] ==> 0hr <= x * y";
  2.1128 +by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
  2.1129 +by (auto_tac (claset() addIs [hypreal_mult_order,
  2.1130 +    hypreal_less_imp_le],simpset()));
  2.1131 +qed "hypreal_le_mult_order";
  2.1132 +
  2.1133 +Goal "[| x <= 0hr; y <= 0hr |] ==> 0hr <= x * y";
  2.1134 +by (rtac hypreal_less_or_eq_imp_le 1);
  2.1135 +by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1);
  2.1136 +by Auto_tac;
  2.1137 +by (dtac hypreal_le_imp_less_or_eq 1);
  2.1138 +by (auto_tac (claset() addDs [hypreal_mult_less_zero1],simpset()));
  2.1139 +qed "real_mult_le_zero1";
  2.1140 +
  2.1141 +Goal "[| 0hr <= x; y < 0hr |] ==> x * y <= 0hr";
  2.1142 +by (rtac hypreal_less_or_eq_imp_le 1);
  2.1143 +by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1);
  2.1144 +by Auto_tac;
  2.1145 +by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
  2.1146 +by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
  2.1147 +by (blast_tac (claset() addDs [hypreal_mult_order] 
  2.1148 +    addIs [hypreal_minus_mult_eq2 RS ssubst]) 1);
  2.1149 +qed "hypreal_mult_le_zero";
  2.1150 +
  2.1151 +Goal "[| 0hr < x; y < 0hr |] ==> x*y < 0hr";
  2.1152 +by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
  2.1153 +by (dtac hypreal_mult_order 1 THEN assume_tac 1);
  2.1154 +by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
  2.1155 +by (asm_full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2]) 1);
  2.1156 +qed "hypreal_mult_less_zero";
  2.1157 +
  2.1158 +Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0hr < 1hr";
  2.1159 +by (res_inst_tac [("x","%n. 0r")] exI 1);
  2.1160 +by (res_inst_tac [("x","%n. 1r")] exI 1);
  2.1161 +by (auto_tac (claset(),simpset() addsimps [real_zero_less_one,
  2.1162 +    FreeUltrafilterNat_Nat_set]));
  2.1163 +qed "hypreal_zero_less_one";
  2.1164 +
  2.1165 +Goal "[| 0hr <= x; 0hr <= y |] ==> 0hr <= x + y";
  2.1166 +by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
  2.1167 +by (auto_tac (claset() addIs [hypreal_add_order,
  2.1168 +    hypreal_less_imp_le],simpset()));
  2.1169 +qed "hypreal_le_add_order";
  2.1170 +
  2.1171 +Goal "!!(q1::hypreal). q1 <= q2  ==> x + q1 <= x + q2";
  2.1172 +by (dtac hypreal_le_imp_less_or_eq 1);
  2.1173 +by (Step_tac 1);
  2.1174 +by (auto_tac (claset() addSIs [hypreal_le_refl,
  2.1175 +    hypreal_less_imp_le,hypreal_add_less_mono1],
  2.1176 +    simpset() addsimps [hypreal_add_commute]));
  2.1177 +qed "hypreal_add_left_le_mono1";
  2.1178 +
  2.1179 +Goal "!!(q1::hypreal). q1 <= q2  ==> q1 + x <= q2 + x";
  2.1180 +by (auto_tac (claset() addDs [hypreal_add_left_le_mono1],
  2.1181 +    simpset() addsimps [hypreal_add_commute]));
  2.1182 +qed "hypreal_add_le_mono1";
  2.1183 +
  2.1184 +Goal "!!k l::hypreal. [|i<=j;  k<=l |] ==> i + k <= j + l";
  2.1185 +by (etac (hypreal_add_le_mono1 RS hypreal_le_trans) 1);
  2.1186 +by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
  2.1187 +(*j moves to the end because it is free while k, l are bound*)
  2.1188 +by (etac hypreal_add_le_mono1 1);
  2.1189 +qed "hypreal_add_le_mono";
  2.1190 +
  2.1191 +Goal "!!k l::hypreal. [|i<j;  k<=l |] ==> i + k < j + l";
  2.1192 +by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] 
  2.1193 +    addIs [hypreal_add_less_mono1,hypreal_add_less_mono],simpset()));
  2.1194 +qed "hypreal_add_less_le_mono";
  2.1195 +
  2.1196 +Goal "!!k l::hypreal. [|i<=j;  k<l |] ==> i + k < j + l";
  2.1197 +by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] 
  2.1198 +    addIs [hypreal_add_less_mono2,hypreal_add_less_mono],simpset()));
  2.1199 +qed "hypreal_add_le_less_mono";
  2.1200 +
  2.1201 +Goal "(0hr*x<r)=(0hr<r)";
  2.1202 +by (Simp_tac 1);
  2.1203 +qed "hypreal_mult_0_less";
  2.1204 +
  2.1205 +Goal "[| 0hr < z; x < y |] ==> x*z < y*z";       
  2.1206 +by (rotate_tac 1 1);
  2.1207 +by (dtac (hypreal_less_minus_iff RS iffD1) 1);
  2.1208 +by (rtac (hypreal_less_minus_iff RS iffD2) 1);
  2.1209 +by (dtac hypreal_mult_order 1 THEN assume_tac 1);
  2.1210 +by (asm_full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2,
  2.1211 +    hypreal_minus_mult_eq2 RS sym, hypreal_mult_commute ]) 1);
  2.1212 +qed "hypreal_mult_less_mono1";
  2.1213 +
  2.1214 +Goal "[| 0hr<z; x<y |] ==> z*x<z*y";       
  2.1215 +by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,hypreal_mult_less_mono1]) 1);
  2.1216 +qed "hypreal_mult_less_mono2";
  2.1217 +
  2.1218 +Goal "[| 0hr<=z; x<y |] ==> x*z<=y*z";
  2.1219 +by (EVERY1 [rtac hypreal_less_or_eq_imp_le, dtac hypreal_le_imp_less_or_eq]);
  2.1220 +by (auto_tac (claset() addIs [hypreal_mult_less_mono1],simpset()));
  2.1221 +qed "hypreal_mult_le_less_mono1";
  2.1222 +
  2.1223 +Goal "[| 0hr<=z; x<y |] ==> z*x<=z*y";
  2.1224 +by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,
  2.1225 +				      hypreal_mult_le_less_mono1]) 1);
  2.1226 +qed "hypreal_mult_le_less_mono2";
  2.1227 +
  2.1228 +Goal "[| 0hr<=z; x<=y |] ==> z*x<=z*y";
  2.1229 +by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1);
  2.1230 +by (auto_tac (claset() addIs [hypreal_mult_le_less_mono2,hypreal_le_refl],simpset()));
  2.1231 +qed "hypreal_mult_le_le_mono1";
  2.1232 +
  2.1233 +val prem1::prem2::prem3::rest = goal thy
  2.1234 +     "[| 0hr<y; x<r; y*r<t*s |] ==> y*x<t*s";
  2.1235 +by (rtac ([([prem1,prem2] MRS hypreal_mult_less_mono2),prem3] MRS hypreal_less_trans) 1);
  2.1236 +qed "hypreal_mult_less_trans";
  2.1237 +
  2.1238 +Goal "[| 0hr<=y; x<r; y*r<t*s; 0hr<t*s|] ==> y*x<t*s";
  2.1239 +by (dtac hypreal_le_imp_less_or_eq 1);
  2.1240 +by (fast_tac (HOL_cs addEs [(hypreal_mult_0_less RS iffD2),hypreal_mult_less_trans]) 1);
  2.1241 +qed "hypreal_mult_le_less_trans";
  2.1242 +
  2.1243 +Goal "[| 0hr <= y; x <= r; y*r < t*s; 0hr < t*s|] ==> y*x < t*s";
  2.1244 +by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1);
  2.1245 +by (fast_tac (claset() addIs [hypreal_mult_le_less_trans]) 1);
  2.1246 +qed "hypreal_mult_le_le_trans";
  2.1247 +
  2.1248 +Goal "[| 0hr < r1; r1 <r2; 0hr < x; x < y|] \
  2.1249 +\                     ==> r1 * x < r2 * y";
  2.1250 +by (dres_inst_tac [("x","x")] hypreal_mult_less_mono2 1);
  2.1251 +by (dres_inst_tac [("R1.0","0hr")] hypreal_less_trans 2);
  2.1252 +by (dres_inst_tac [("x","r1")] hypreal_mult_less_mono1 3);
  2.1253 +by Auto_tac;
  2.1254 +by (blast_tac (claset() addIs [hypreal_less_trans]) 1);
  2.1255 +qed "hypreal_mult_less_mono";
  2.1256 +
  2.1257 +Goal "[| 0hr < r1; r1 <r2; 0hr < y|] \
  2.1258 +\                           ==> 0hr < r2 * y";
  2.1259 +by (dres_inst_tac [("R1.0","0hr")] hypreal_less_trans 1);
  2.1260 +by (assume_tac 1);
  2.1261 +by (blast_tac (claset() addIs [hypreal_mult_order]) 1);
  2.1262 +qed "hypreal_mult_order_trans";
  2.1263 +
  2.1264 +Goal "[| 0hr < r1; r1 <= r2; 0hr <= x; x <= y |] \
  2.1265 +\                  ==> r1 * x <= r2 * y";
  2.1266 +by (rtac hypreal_less_or_eq_imp_le 1);
  2.1267 +by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
  2.1268 +by (auto_tac (claset() addIs [hypreal_mult_less_mono,
  2.1269 +    hypreal_mult_less_mono1,hypreal_mult_less_mono2,
  2.1270 +    hypreal_mult_order_trans,hypreal_mult_order],simpset()));
  2.1271 +qed "hypreal_mult_le_mono";
  2.1272 +
  2.1273 +(*----------------------------------------------------------
  2.1274 +  hypreal_of_real preserves field and order properties
  2.1275 + -----------------------------------------------------------*)
  2.1276 +Goalw [hypreal_of_real_def] 
  2.1277 +      "hypreal_of_real ((z1::real) + z2) = \
  2.1278 +\      hypreal_of_real z1 + hypreal_of_real z2";
  2.1279 +by (asm_simp_tac (simpset() addsimps [hypreal_add,
  2.1280 +       hypreal_add_mult_distrib]) 1);
  2.1281 +qed "hypreal_of_real_add";
  2.1282 +
  2.1283 +Goalw [hypreal_of_real_def] 
  2.1284 +            "hypreal_of_real ((z1::real) * z2) = hypreal_of_real z1 * hypreal_of_real z2";
  2.1285 +by (full_simp_tac (simpset() addsimps [hypreal_mult,
  2.1286 +        hypreal_add_mult_distrib2]) 1);
  2.1287 +qed "hypreal_of_real_mult";
  2.1288 +
  2.1289 +Goalw [hypreal_less_def,hypreal_of_real_def] 
  2.1290 +            "(z1 < z2) = (hypreal_of_real z1 <  hypreal_of_real z2)";
  2.1291 +by Auto_tac;
  2.1292 +by (res_inst_tac [("x","%n. z1")] exI 1);
  2.1293 +by (Step_tac 1); 
  2.1294 +by (res_inst_tac [("x","%n. z2")] exI 2);
  2.1295 +by Auto_tac;
  2.1296 +by (rtac FreeUltrafilterNat_P 1);
  2.1297 +by (Ultra_tac 1);
  2.1298 +qed "hypreal_of_real_less_iff";
  2.1299 +
  2.1300 +Addsimps [hypreal_of_real_less_iff RS sym];
  2.1301 +
  2.1302 +Goalw [hypreal_le_def,real_le_def] 
  2.1303 +            "(z1 <= z2) = (hypreal_of_real z1 <=  hypreal_of_real z2)";
  2.1304 +by Auto_tac;
  2.1305 +qed "hypreal_of_real_le_iff";
  2.1306 +
  2.1307 +Goalw [hypreal_of_real_def] "hypreal_of_real (-r) = - hypreal_of_real  r";
  2.1308 +by (auto_tac (claset(),simpset() addsimps [hypreal_minus]));
  2.1309 +qed "hypreal_of_real_minus";
  2.1310 +
  2.1311 +Goal "0hr < x ==> 0hr < hrinv x";
  2.1312 +by (EVERY1[rtac ccontr, dtac hypreal_leI]);
  2.1313 +by (forward_tac [hypreal_minus_zero_less_iff2 RS iffD2] 1);
  2.1314 +by (forward_tac [hypreal_not_refl2 RS not_sym] 1);
  2.1315 +by (dtac (hypreal_not_refl2 RS not_sym RS hrinv_not_zero) 1);
  2.1316 +by (EVERY1[dtac hypreal_le_imp_less_or_eq, Step_tac]); 
  2.1317 +by (dtac hypreal_mult_less_zero1 1 THEN assume_tac 1);
  2.1318 +by (auto_tac (claset() addIs [hypreal_zero_less_one RS hypreal_less_asym],
  2.1319 +    simpset() addsimps [hypreal_minus_mult_eq1 RS sym,
  2.1320 +     hypreal_minus_zero_less_iff]));
  2.1321 +qed "hypreal_hrinv_gt_zero";
  2.1322 +
  2.1323 +Goal "x < 0hr ==> hrinv x < 0hr";
  2.1324 +by (forward_tac [hypreal_not_refl2] 1);
  2.1325 +by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
  2.1326 +by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
  2.1327 +by (dtac (hypreal_minus_hrinv RS sym) 1);
  2.1328 +by (auto_tac (claset() addIs [hypreal_hrinv_gt_zero],
  2.1329 +    simpset()));
  2.1330 +qed "hypreal_hrinv_less_zero";
  2.1331 +
  2.1332 +Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real  1r = 1hr";
  2.1333 +by (Step_tac 1);
  2.1334 +qed "hypreal_of_real_one";
  2.1335 +
  2.1336 +Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real  0r = 0hr";
  2.1337 +by (Step_tac 1);
  2.1338 +qed "hypreal_of_real_zero";
  2.1339 +
  2.1340 +Goal "(hypreal_of_real  r = 0hr) = (r = 0r)";
  2.1341 +by (auto_tac (claset() addIs [FreeUltrafilterNat_P],
  2.1342 +    simpset() addsimps [hypreal_of_real_def,
  2.1343 +    hypreal_zero_def,FreeUltrafilterNat_Nat_set]));
  2.1344 +qed "hypreal_of_real_zero_iff";
  2.1345 +
  2.1346 +Goal "(hypreal_of_real  r ~= 0hr) = (r ~= 0r)";
  2.1347 +by (full_simp_tac (simpset() addsimps [hypreal_of_real_zero_iff]) 1);
  2.1348 +qed "hypreal_of_real_not_zero_iff";
  2.1349 +
  2.1350 +Goal "r ~= 0r ==> hrinv (hypreal_of_real r) = \
  2.1351 +\          hypreal_of_real (rinv r)";
  2.1352 +by (res_inst_tac [("c1","hypreal_of_real r")] (hypreal_mult_left_cancel RS iffD1) 1);
  2.1353 +by (etac (hypreal_of_real_not_zero_iff RS iffD2) 1);
  2.1354 +by (forward_tac [hypreal_of_real_not_zero_iff RS iffD2] 1);
  2.1355 +by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_mult RS sym,hypreal_of_real_one]));
  2.1356 +qed "hypreal_of_real_hrinv";
  2.1357 +
  2.1358 +Goal "hypreal_of_real r ~= 0hr ==> hrinv (hypreal_of_real r) = \
  2.1359 +\          hypreal_of_real (rinv r)";
  2.1360 +by (etac (hypreal_of_real_not_zero_iff RS iffD1 RS hypreal_of_real_hrinv) 1);
  2.1361 +qed "hypreal_of_real_hrinv2";
  2.1362 +
  2.1363 +Goal "x+x=x*(1hr+1hr)";
  2.1364 +by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1);
  2.1365 +qed "hypreal_add_self";
  2.1366 +
  2.1367 +Goal "1hr < 1hr + 1hr";
  2.1368 +by (rtac (hypreal_less_minus_iff RS iffD2) 1);
  2.1369 +by (full_simp_tac (simpset() addsimps [hypreal_zero_less_one,
  2.1370 +    hypreal_add_assoc]) 1);
  2.1371 +qed "hypreal_one_less_two";
  2.1372 +
  2.1373 +Goal "0hr < 1hr + 1hr";
  2.1374 +by (rtac ([hypreal_zero_less_one,
  2.1375 +          hypreal_one_less_two] MRS hypreal_less_trans) 1);
  2.1376 +qed "hypreal_zero_less_two";
  2.1377 +
  2.1378 +Goal "1hr + 1hr ~= 0hr";
  2.1379 +by (rtac (hypreal_zero_less_two RS hypreal_not_refl2 RS not_sym) 1);
  2.1380 +qed "hypreal_two_not_zero";
  2.1381 +Addsimps [hypreal_two_not_zero];
  2.1382 +
  2.1383 +Goal "x*hrinv(1hr + 1hr) + x*hrinv(1hr + 1hr) = x";
  2.1384 +by (rtac (hypreal_add_self RS ssubst) 1);
  2.1385 +by (full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
  2.1386 +qed "hypreal_sum_of_halves";
  2.1387 +
  2.1388 +Goal "z ~= 0hr ==> x*y = (x*hrinv(z))*(z*y)";
  2.1389 +by (asm_simp_tac (simpset() addsimps hypreal_mult_ac)  1);
  2.1390 +qed "lemma_chain";
  2.1391 +
  2.1392 +Goal "0hr < r ==> 0hr < r*hrinv(1hr+1hr)";
  2.1393 +by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero 
  2.1394 +          RS hypreal_mult_less_mono1) 1);
  2.1395 +by Auto_tac;
  2.1396 +qed "hypreal_half_gt_zero";
  2.1397 +
  2.1398 +(* TODO: remove redundant  0hr < x *)
  2.1399 +Goal "[| 0hr < r; 0hr < x; r < x |] ==> hrinv x < hrinv r";
  2.1400 +by (forward_tac [hypreal_hrinv_gt_zero] 1);
  2.1401 +by (forw_inst_tac [("x","x")] hypreal_hrinv_gt_zero 1);
  2.1402 +by (forw_inst_tac [("x","r"),("z","hrinv r")] hypreal_mult_less_mono1 1);
  2.1403 +by (assume_tac 1);
  2.1404 +by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS 
  2.1405 +         not_sym RS hypreal_mult_hrinv]) 1);
  2.1406 +by (forward_tac [hypreal_hrinv_gt_zero] 1);
  2.1407 +by (forw_inst_tac [("x","1hr"),("z","hrinv x")] hypreal_mult_less_mono2 1);
  2.1408 +by (assume_tac 1);
  2.1409 +by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS 
  2.1410 +         not_sym RS hypreal_mult_hrinv_left,hypreal_mult_assoc RS sym]) 1);
  2.1411 +qed "hypreal_hrinv_less_swap";
  2.1412 +
  2.1413 +Goal "[| 0hr < r; 0hr < x|] ==> (r < x) = (hrinv x < hrinv r)";
  2.1414 +by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],simpset()));
  2.1415 +by (res_inst_tac [("t","r")] (hypreal_hrinv_hrinv RS subst) 1);
  2.1416 +by (etac (hypreal_not_refl2 RS not_sym) 1);
  2.1417 +by (res_inst_tac [("t","x")] (hypreal_hrinv_hrinv RS subst) 1);
  2.1418 +by (etac (hypreal_not_refl2 RS not_sym) 1);
  2.1419 +by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],
  2.1420 +    simpset() addsimps [hypreal_hrinv_gt_zero]));
  2.1421 +qed "hypreal_hrinv_less_iff";
  2.1422 +
  2.1423 +Goal "[| 0hr < z; x < y |] ==> x*hrinv(z) < y*hrinv(z)";
  2.1424 +by (blast_tac (claset() addSIs [hypreal_mult_less_mono1,
  2.1425 +    hypreal_hrinv_gt_zero]) 1);
  2.1426 +qed "hypreal_mult_hrinv_less_mono1";
  2.1427 +
  2.1428 +Goal "[| 0hr < z; x < y |] ==> hrinv(z)*x < hrinv(z)*y";
  2.1429 +by (blast_tac (claset() addSIs [hypreal_mult_less_mono2,
  2.1430 +    hypreal_hrinv_gt_zero]) 1);
  2.1431 +qed "hypreal_mult_hrinv_less_mono2";
  2.1432 +
  2.1433 +Goal "[| 0hr < z; x*z < y*z |] ==> x < y";
  2.1434 +by (forw_inst_tac [("x","x*z")] hypreal_mult_hrinv_less_mono1 1);
  2.1435 +by (dtac (hypreal_not_refl2 RS not_sym) 2);
  2.1436 +by (auto_tac (claset() addSDs [hypreal_mult_hrinv],
  2.1437 +              simpset() addsimps hypreal_mult_ac));
  2.1438 +qed "hypreal_less_mult_right_cancel";
  2.1439 +
  2.1440 +Goal "[| 0hr < z; z*x < z*y |] ==> x < y";
  2.1441 +by (auto_tac (claset() addIs [hypreal_less_mult_right_cancel],
  2.1442 +    simpset() addsimps [hypreal_mult_commute]));
  2.1443 +qed "hypreal_less_mult_left_cancel";
  2.1444 +
  2.1445 +Goal "[| 0hr < r; 0hr < ra; \
  2.1446 +\                 r < x; ra < y |] \
  2.1447 +\              ==> r*ra < x*y";
  2.1448 +by (forw_inst_tac [("R2.0","r")] hypreal_less_trans 1);
  2.1449 +by (dres_inst_tac [("z","ra"),("x","r")] hypreal_mult_less_mono1 2);
  2.1450 +by (dres_inst_tac [("z","x"),("x","ra")] hypreal_mult_less_mono2 3);
  2.1451 +by (auto_tac (claset() addIs [hypreal_less_trans],simpset()));
  2.1452 +qed "hypreal_mult_less_gt_zero"; 
  2.1453 +
  2.1454 +Goal "[| 0hr < r; 0hr < ra; \
  2.1455 +\                 r <= x; ra <= y |] \
  2.1456 +\              ==> r*ra <= x*y";
  2.1457 +by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
  2.1458 +by (rtac hypreal_less_or_eq_imp_le 1);
  2.1459 +by (auto_tac (claset() addIs [hypreal_mult_less_mono1,
  2.1460 +    hypreal_mult_less_mono2,hypreal_mult_less_gt_zero],
  2.1461 +    simpset()));
  2.1462 +qed "hypreal_mult_le_ge_zero"; 
  2.1463 +
  2.1464 +Goal "? (x::hypreal). x < y";
  2.1465 +by (rtac (hypreal_add_zero_right RS subst) 1);
  2.1466 +by (res_inst_tac [("x","y + -1hr")] exI 1);
  2.1467 +by (auto_tac (claset() addSIs [hypreal_add_less_mono2],
  2.1468 +    simpset() addsimps [hypreal_minus_zero_less_iff2,
  2.1469 +    hypreal_zero_less_one] delsimps [hypreal_add_zero_right]));
  2.1470 +qed "hypreal_less_Ex";
  2.1471 +
  2.1472 +Goal "!!(A::hypreal). A + C < B + C ==> A < B";
  2.1473 +by (dres_inst_tac [("C","-C")] hypreal_add_less_mono1 1);
  2.1474 +by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
  2.1475 +qed "hypreal_less_add_right_cancel";
  2.1476 +
  2.1477 +Goal "!!(A::hypreal). C + A < C + B ==> A < B";
  2.1478 +by (dres_inst_tac [("C","-C")] hypreal_add_less_mono2 1);
  2.1479 +by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
  2.1480 +qed "hypreal_less_add_left_cancel";
  2.1481 +
  2.1482 +Goal "0hr <= x*x";
  2.1483 +by (res_inst_tac [("x","0hr"),("y","x")] hypreal_linear_less2 1);
  2.1484 +by (auto_tac (claset() addIs [hypreal_mult_order,
  2.1485 +    hypreal_mult_less_zero1,hypreal_less_imp_le],
  2.1486 +    simpset()));
  2.1487 +qed "hypreal_le_square";
  2.1488 +Addsimps [hypreal_le_square];
  2.1489 +
  2.1490 +Goalw [hypreal_le_def] "- (x*x) <= 0hr";
  2.1491 +by (auto_tac (claset() addSDs [(hypreal_le_square RS 
  2.1492 +    hypreal_le_less_trans)],simpset() addsimps 
  2.1493 +    [hypreal_minus_zero_less_iff,hypreal_less_not_refl]));
  2.1494 +qed "hypreal_less_minus_square";
  2.1495 +Addsimps [hypreal_less_minus_square];
  2.1496 +
  2.1497 +Goal "[|x ~= 0hr; y ~= 0hr |] ==> \
  2.1498 +\                   hrinv(x) + hrinv(y) = (x + y)*hrinv(x*y)";
  2.1499 +by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv_distrib,
  2.1500 +             hypreal_add_mult_distrib,hypreal_mult_assoc RS sym]) 1);
  2.1501 +by (rtac (hypreal_mult_assoc RS ssubst) 1);
  2.1502 +by (rtac (hypreal_mult_left_commute RS subst) 1);
  2.1503 +by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
  2.1504 +qed "hypreal_hrinv_add";
  2.1505 +
  2.1506 +Goal "x = -x ==> x = 0hr";
  2.1507 +by (dtac (hypreal_eq_minus_iff RS iffD1 RS sym) 1);
  2.1508 +by (Asm_full_simp_tac 1);
  2.1509 +by (dtac (hypreal_add_self RS subst) 1);
  2.1510 +by (rtac ccontr 1);
  2.1511 +by (blast_tac (claset() addDs [hypreal_two_not_zero RSN
  2.1512 +               (2,hypreal_mult_not_0)]) 1);
  2.1513 +qed "hypreal_self_eq_minus_self_zero";
  2.1514 +
  2.1515 +Goal "(x + x = 0hr) = (x = 0hr)";
  2.1516 +by Auto_tac;
  2.1517 +by (dtac (hypreal_add_self RS subst) 1);
  2.1518 +by (rtac ccontr 1 THEN rtac hypreal_mult_not_0E 1);
  2.1519 +by Auto_tac;
  2.1520 +qed "hypreal_add_self_zero_cancel";
  2.1521 +Addsimps [hypreal_add_self_zero_cancel];
  2.1522 +
  2.1523 +Goal "(x + x + y = y) = (x = 0hr)";
  2.1524 +by Auto_tac;
  2.1525 +by (dtac (hypreal_eq_minus_iff RS iffD1) 1 THEN dtac sym 1);
  2.1526 +by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
  2.1527 +qed "hypreal_add_self_zero_cancel2";
  2.1528 +Addsimps [hypreal_add_self_zero_cancel2];
  2.1529 +
  2.1530 +Goal "(x + (x + y) = y) = (x = 0hr)";
  2.1531 +by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
  2.1532 +qed "hypreal_add_self_zero_cancel2a";
  2.1533 +Addsimps [hypreal_add_self_zero_cancel2a];
  2.1534 +
  2.1535 +Goal "(b = -a) = (-b = (a::hypreal))";
  2.1536 +by Auto_tac;
  2.1537 +qed "hypreal_minus_eq_swap";
  2.1538 +
  2.1539 +Goal "(-b = -a) = (b = (a::hypreal))";
  2.1540 +by (asm_full_simp_tac (simpset() addsimps 
  2.1541 +    [hypreal_minus_eq_swap]) 1);
  2.1542 +qed "hypreal_minus_eq_cancel";
  2.1543 +Addsimps [hypreal_minus_eq_cancel];
  2.1544 +
  2.1545 +Goal "x < x + 1hr";
  2.1546 +by (cut_inst_tac [("C","x")] 
  2.1547 +    (hypreal_zero_less_one RS hypreal_add_less_mono2) 1);
  2.1548 +by (Asm_full_simp_tac 1);
  2.1549 +qed "hypreal_less_self_add_one";
  2.1550 +Addsimps [hypreal_less_self_add_one];
  2.1551 +
  2.1552 +Goal "((x::hypreal) + x = y + y) = (x = y)";
  2.1553 +by (auto_tac (claset() addIs [hypreal_two_not_zero RS 
  2.1554 +     hypreal_mult_left_cancel RS iffD1],simpset() addsimps 
  2.1555 +     [hypreal_add_mult_distrib]));
  2.1556 +qed "hypreal_add_self_cancel";
  2.1557 +Addsimps [hypreal_add_self_cancel];
  2.1558 +
  2.1559 +Goal "(y = x + - y + x) = (y = (x::hypreal))";
  2.1560 +by Auto_tac;
  2.1561 +by (dres_inst_tac [("x1","y")] 
  2.1562 +    (hypreal_add_right_cancel RS iffD2) 1);
  2.1563 +by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
  2.1564 +qed "hypreal_add_self_minus_cancel";
  2.1565 +Addsimps [hypreal_add_self_minus_cancel];
  2.1566 +
  2.1567 +Goal "(y = x + (- y + x)) = (y = (x::hypreal))";
  2.1568 +by (asm_full_simp_tac (simpset() addsimps 
  2.1569 +         [hypreal_add_assoc RS sym])1);
  2.1570 +qed "hypreal_add_self_minus_cancel2";
  2.1571 +Addsimps [hypreal_add_self_minus_cancel2];
  2.1572 +
  2.1573 +Goal "z + -x = y + (y + (-x + -z)) = (y = (z::hypreal))";
  2.1574 +by Auto_tac;
  2.1575 +by (dres_inst_tac [("x1","z")] 
  2.1576 +    (hypreal_add_right_cancel RS iffD2) 1);
  2.1577 +by (asm_full_simp_tac (simpset() addsimps 
  2.1578 +    [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac) 1);
  2.1579 +by (asm_full_simp_tac (simpset() addsimps 
  2.1580 +     [hypreal_add_assoc RS sym,hypreal_add_right_cancel]) 1);
  2.1581 +qed "hypreal_add_self_minus_cancel3";
  2.1582 +Addsimps [hypreal_add_self_minus_cancel3];
  2.1583 +
  2.1584 +(* check why this does not work without 2nd substiution anymore! *)
  2.1585 +Goal "x < y ==> x < (x + y)*hrinv(1hr + 1hr)";
  2.1586 +by (dres_inst_tac [("C","x")] hypreal_add_less_mono2 1);
  2.1587 +by (dtac (hypreal_add_self RS subst) 1);
  2.1588 +by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS 
  2.1589 +          hypreal_mult_less_mono1) 1);
  2.1590 +by (auto_tac (claset() addDs [hypreal_two_not_zero RS 
  2.1591 +          (hypreal_mult_hrinv RS subst)],simpset() 
  2.1592 +          addsimps [hypreal_mult_assoc]));
  2.1593 +qed "hypreal_less_half_sum";
  2.1594 +
  2.1595 +(* check why this does not work without 2nd substiution anymore! *)
  2.1596 +Goal "x < y ==> (x + y)*hrinv(1hr + 1hr) < y";
  2.1597 +by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 1);
  2.1598 +by (dtac (hypreal_add_self RS subst) 1);
  2.1599 +by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS 
  2.1600 +          hypreal_mult_less_mono1) 1);
  2.1601 +by (auto_tac (claset() addDs [hypreal_two_not_zero RS 
  2.1602 +          (hypreal_mult_hrinv RS subst)],simpset() 
  2.1603 +          addsimps [hypreal_mult_assoc]));
  2.1604 +qed "hypreal_gt_half_sum";
  2.1605 +
  2.1606 +Goal "!!(x::hypreal). x < y ==> EX r. x < r & r < y";
  2.1607 +by (blast_tac (claset() addSIs [hypreal_less_half_sum,
  2.1608 +    hypreal_gt_half_sum]) 1);
  2.1609 +qed "hypreal_dense";
  2.1610 +
  2.1611 +Goal "(x * x = 0hr) = (x = 0hr)";
  2.1612 +by Auto_tac;
  2.1613 +by (blast_tac (claset() addIs [hypreal_mult_not_0E]) 1);
  2.1614 +qed "hypreal_mult_self_eq_zero_iff";
  2.1615 +Addsimps [hypreal_mult_self_eq_zero_iff];
  2.1616 +
  2.1617 +Goal "(0hr = x * x) = (x = 0hr)";
  2.1618 +by (auto_tac (claset() addDs [sym],simpset()));
  2.1619 +qed "hypreal_mult_self_eq_zero_iff2";
  2.1620 +Addsimps [hypreal_mult_self_eq_zero_iff2];
  2.1621 +
  2.1622 +Goal "(x*x + y*y = 0hr) = (x = 0hr & y = 0hr)";
  2.1623 +by Auto_tac;
  2.1624 +by (dtac (sym RS (hypreal_eq_minus_iff3 RS iffD1))  1);
  2.1625 +by (dtac (sym RS (hypreal_eq_minus_iff4 RS iffD1))  2);
  2.1626 +by (ALLGOALS(rtac ccontr));
  2.1627 +by (ALLGOALS(dtac hypreal_mult_self_not_zero));
  2.1628 +by (cut_inst_tac [("x1","x")] (hypreal_le_square 
  2.1629 +        RS hypreal_le_imp_less_or_eq) 1);
  2.1630 +by (cut_inst_tac [("x1","y")] (hypreal_le_square 
  2.1631 +        RS hypreal_le_imp_less_or_eq) 2);
  2.1632 +by (auto_tac (claset() addDs [sym],simpset()));
  2.1633 +by (dres_inst_tac [("x1","y")] (hypreal_less_minus_square 
  2.1634 +    RS hypreal_le_less_trans) 1);
  2.1635 +by (dres_inst_tac [("x1","x")] (hypreal_less_minus_square 
  2.1636 +    RS hypreal_le_less_trans) 2);
  2.1637 +by (auto_tac (claset(),simpset() addsimps 
  2.1638 +       [hypreal_less_not_refl]));
  2.1639 +qed "hypreal_squares_add_zero_iff";
  2.1640 +Addsimps [hypreal_squares_add_zero_iff];
  2.1641 +
  2.1642 +Goal "x * x ~= 0hr ==> 0hr < x* x + y*y + z*z";
  2.1643 +by (cut_inst_tac [("x1","x")] (hypreal_le_square 
  2.1644 +        RS hypreal_le_imp_less_or_eq) 1);
  2.1645 +by (auto_tac (claset() addSIs 
  2.1646 +              [hypreal_add_order_le],simpset()));
  2.1647 +qed "hypreal_sum_squares3_gt_zero";
  2.1648 +
  2.1649 +Goal "x * x ~= 0hr ==> 0hr < y*y + x*x + z*z";
  2.1650 +by (dtac hypreal_sum_squares3_gt_zero 1);
  2.1651 +by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
  2.1652 +qed "hypreal_sum_squares3_gt_zero2";
  2.1653 +
  2.1654 +Goal "x * x ~= 0hr ==> 0hr < y*y + z*z + x*x";
  2.1655 +by (dtac hypreal_sum_squares3_gt_zero 1);
  2.1656 +by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
  2.1657 +qed "hypreal_sum_squares3_gt_zero3";
  2.1658 +
  2.1659 +Goal "(x*x + y*y + z*z = 0hr) = \ 
  2.1660 +\               (x = 0hr & y = 0hr & z = 0hr)";
  2.1661 +by Auto_tac;
  2.1662 +by (ALLGOALS(rtac ccontr));
  2.1663 +by (ALLGOALS(dtac hypreal_mult_self_not_zero));
  2.1664 +by (auto_tac (claset() addDs [hypreal_not_refl2 RS not_sym,
  2.1665 +   hypreal_sum_squares3_gt_zero3,hypreal_sum_squares3_gt_zero,
  2.1666 +   hypreal_sum_squares3_gt_zero2],simpset() delsimps
  2.1667 +   [hypreal_mult_self_eq_zero_iff]));
  2.1668 +qed "hypreal_three_squares_add_zero_iff";
  2.1669 +Addsimps [hypreal_three_squares_add_zero_iff];
  2.1670 +
  2.1671 +Goal "(x::hypreal)*x <= x*x + y*y";
  2.1672 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  2.1673 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
  2.1674 +by (auto_tac (claset(),simpset() addsimps 
  2.1675 +    [hypreal_mult,hypreal_add,hypreal_le]));
  2.1676 +qed "hypreal_self_le_add_pos";
  2.1677 +Addsimps [hypreal_self_le_add_pos];
  2.1678 +
  2.1679 +Goal "(x::hypreal)*x <= x*x + y*y + z*z";
  2.1680 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  2.1681 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
  2.1682 +by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
  2.1683 +by (auto_tac (claset(),simpset() addsimps 
  2.1684 +    [hypreal_mult,hypreal_add,hypreal_le,
  2.1685 +    real_le_add_order]));
  2.1686 +qed "hypreal_self_le_add_pos2";
  2.1687 +Addsimps [hypreal_self_le_add_pos2];
  2.1688 +
  2.1689 +(*---------------------------------------------------------------------------------
  2.1690 +             Embedding of the naturals in the hyperreals
  2.1691 + ---------------------------------------------------------------------------------*)
  2.1692 +Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 0 = 1hr";
  2.1693 +by (full_simp_tac (simpset() addsimps 
  2.1694 +    [pnat_one_iff RS sym,real_of_preal_def]) 1);
  2.1695 +by (fold_tac [real_one_def]);
  2.1696 +by (rtac hypreal_of_real_one 1);
  2.1697 +qed "hypreal_of_posnat_one";
  2.1698 +
  2.1699 +Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr";
  2.1700 +by (full_simp_tac (simpset() addsimps [real_of_preal_def,real_one_def,
  2.1701 +    hypreal_one_def,hypreal_add,hypreal_of_real_def,pnat_two_eq,
  2.1702 +    real_add,prat_of_pnat_add RS sym,preal_of_prat_add RS sym] @ pnat_add_ac) 1);
  2.1703 +qed "hypreal_of_posnat_two";
  2.1704 +
  2.1705 +Goalw [hypreal_of_posnat_def]
  2.1706 +          "hypreal_of_posnat n1 + hypreal_of_posnat n2 = \
  2.1707 +\          hypreal_of_posnat (n1 + n2) + 1hr";
  2.1708 +by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one RS sym,
  2.1709 +    hypreal_of_real_add RS sym,hypreal_of_posnat_def,real_of_preal_add RS sym,
  2.1710 +    preal_of_prat_add RS sym,prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
  2.1711 +qed "hypreal_of_posnat_add";
  2.1712 +
  2.1713 +Goal "hypreal_of_posnat (n + 1) = hypreal_of_posnat n + 1hr";
  2.1714 +by (res_inst_tac [("x1","1hr")] (hypreal_add_right_cancel RS iffD1) 1);
  2.1715 +by (rtac (hypreal_of_posnat_add RS subst) 1);
  2.1716 +by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,hypreal_add_assoc]) 1);
  2.1717 +qed "hypreal_of_posnat_add_one";
  2.1718 +
  2.1719 +Goalw [real_of_posnat_def,hypreal_of_posnat_def] 
  2.1720 +      "hypreal_of_posnat n = hypreal_of_real (real_of_posnat n)";
  2.1721 +by (rtac refl 1);
  2.1722 +qed "hypreal_of_real_of_posnat";
  2.1723 +
  2.1724 +Goalw [hypreal_of_posnat_def] 
  2.1725 +      "(n < m) = (hypreal_of_posnat n < hypreal_of_posnat m)";
  2.1726 +by Auto_tac;
  2.1727 +qed "hypreal_of_posnat_less_iff";
  2.1728 +
  2.1729 +Addsimps [hypreal_of_posnat_less_iff RS sym];
  2.1730 +(*---------------------------------------------------------------------------------
  2.1731 +               Existence of infinite hyperreal number
  2.1732 + ---------------------------------------------------------------------------------*)
  2.1733 +
  2.1734 +Goal "hyprel^^{%n::nat. real_of_posnat n} : hypreal";
  2.1735 +by Auto_tac;
  2.1736 +qed "hypreal_omega";
  2.1737 +
  2.1738 +Goalw [omega_def] "Rep_hypreal(whr) : hypreal";
  2.1739 +by (rtac Rep_hypreal 1);
  2.1740 +qed "Rep_hypreal_omega";
  2.1741 +
  2.1742 +(* existence of infinite number not corresponding to any real number *)
  2.1743 +(* use assumption that member FreeUltrafilterNat is not finite       *)
  2.1744 +(* a few lemmas first *)
  2.1745 +
  2.1746 +Goal "{n::nat. x = real_of_posnat n} = {} | \
  2.1747 +\     (? y. {n::nat. x = real_of_posnat n} = {y})";
  2.1748 +by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],simpset()));
  2.1749 +qed "lemma_omega_empty_singleton_disj";
  2.1750 +
  2.1751 +Goal "finite {n::nat. x = real_of_posnat n}";
  2.1752 +by (cut_inst_tac [("x","x")] lemma_omega_empty_singleton_disj 1);
  2.1753 +by Auto_tac;
  2.1754 +qed "lemma_finite_omega_set";
  2.1755 +
  2.1756 +Goalw [omega_def,hypreal_of_real_def] 
  2.1757 +      "~ (? x. hypreal_of_real x = whr)";
  2.1758 +by (auto_tac (claset(),simpset() addsimps [lemma_finite_omega_set 
  2.1759 +    RS FreeUltrafilterNat_finite]));
  2.1760 +qed "not_ex_hypreal_of_real_eq_omega";
  2.1761 +
  2.1762 +Goal "hypreal_of_real x ~= whr";
  2.1763 +by (cut_facts_tac [not_ex_hypreal_of_real_eq_omega] 1);
  2.1764 +by Auto_tac;
  2.1765 +qed "hypreal_of_real_not_eq_omega";
  2.1766 +
  2.1767 +(* existence of infinitesimal number also not *)
  2.1768 +(* corresponding to any real number *)
  2.1769 +
  2.1770 +Goal "{n::nat. x = rinv(real_of_posnat n)} = {} | \
  2.1771 +\     (? y. {n::nat. x = rinv(real_of_posnat n)} = {y})";
  2.1772 +by (Step_tac 1 THEN Step_tac 1);
  2.1773 +by (auto_tac (claset() addIs [real_of_posnat_rinv_inj],simpset()));
  2.1774 +qed "lemma_epsilon_empty_singleton_disj";
  2.1775 +
  2.1776 +Goal "finite {n::nat. x = rinv(real_of_posnat n)}";
  2.1777 +by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1);
  2.1778 +by Auto_tac;
  2.1779 +qed "lemma_finite_epsilon_set";
  2.1780 +
  2.1781 +Goalw [epsilon_def,hypreal_of_real_def] 
  2.1782 +      "~ (? x. hypreal_of_real x = ehr)";
  2.1783 +by (auto_tac (claset(),simpset() addsimps [lemma_finite_epsilon_set 
  2.1784 +    RS FreeUltrafilterNat_finite]));
  2.1785 +qed "not_ex_hypreal_of_real_eq_epsilon";
  2.1786 +
  2.1787 +Goal "hypreal_of_real x ~= ehr";
  2.1788 +by (cut_facts_tac [not_ex_hypreal_of_real_eq_epsilon] 1);
  2.1789 +by Auto_tac;
  2.1790 +qed "hypreal_of_real_not_eq_epsilon";
  2.1791 +
  2.1792 +Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0hr";
  2.1793 +by (auto_tac (claset(),simpset() addsimps 
  2.1794 +    [real_of_posnat_rinv_not_zero]));
  2.1795 +qed "hypreal_epsilon_not_zero";
  2.1796 +
  2.1797 +Goalw [omega_def,hypreal_zero_def] "whr ~= 0hr";
  2.1798 +by (Simp_tac 1);
  2.1799 +qed "hypreal_omega_not_zero";
  2.1800 +
  2.1801 +Goal "ehr = hrinv(whr)";
  2.1802 +by (asm_full_simp_tac (simpset() addsimps 
  2.1803 +    [hypreal_hrinv,omega_def,epsilon_def]
  2.1804 +    setloop (split_tac [expand_if])) 1);
  2.1805 +qed "hypreal_epsilon_hrinv_omega";
  2.1806 +
  2.1807 +(*----------------------------------------------------------------
  2.1808 +     Another embedding of the naturals in the 
  2.1809 +    hyperreals (see hypreal_of_posnat)
  2.1810 + ----------------------------------------------------------------*)
  2.1811 +Goalw [hypreal_of_nat_def] "hypreal_of_nat 0 = 0hr";
  2.1812 +by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one]) 1);
  2.1813 +qed "hypreal_of_nat_zero";
  2.1814 +
  2.1815 +Goalw [hypreal_of_nat_def] "hypreal_of_nat 1 = 1hr";
  2.1816 +by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,
  2.1817 +    hypreal_add_assoc]) 1);
  2.1818 +qed "hypreal_of_nat_one";
  2.1819 +
  2.1820 +Goalw [hypreal_of_nat_def]
  2.1821 +      "hypreal_of_nat n1 + hypreal_of_nat n2 = \
  2.1822 +\      hypreal_of_nat (n1 + n2)";
  2.1823 +by (full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
  2.1824 +by (simp_tac (simpset() addsimps [hypreal_of_posnat_add,
  2.1825 +    hypreal_add_assoc RS sym]) 1);
  2.1826 +by (rtac (hypreal_add_commute RS subst) 1);
  2.1827 +by (simp_tac (simpset() addsimps [hypreal_add_left_cancel,
  2.1828 +    hypreal_add_assoc]) 1);
  2.1829 +qed "hypreal_of_nat_add";
  2.1830 +
  2.1831 +Goal "hypreal_of_nat 2 = 1hr + 1hr";
  2.1832 +by (simp_tac (simpset() addsimps [hypreal_of_nat_one 
  2.1833 +    RS sym,hypreal_of_nat_add]) 1);
  2.1834 +qed "hypreal_of_nat_two";
  2.1835 +
  2.1836 +Goalw [hypreal_of_nat_def] 
  2.1837 +      "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)";
  2.1838 +by (auto_tac (claset() addIs [hypreal_add_less_mono1],simpset()));
  2.1839 +by (dres_inst_tac [("C","1hr")] hypreal_add_less_mono1 1);
  2.1840 +by (full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
  2.1841 +qed "hypreal_of_nat_less_iff";
  2.1842 +Addsimps [hypreal_of_nat_less_iff RS sym];
  2.1843 +
  2.1844 +(* naturals embedded in hyperreals is an hyperreal *)
  2.1845 +Goalw [hypreal_of_nat_def,real_of_nat_def] 
  2.1846 +      "hypreal_of_nat  m = Abs_hypreal(hyprel^^{%n. real_of_nat m})";
  2.1847 +by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def,
  2.1848 +    hypreal_of_real_of_posnat,hypreal_minus,hypreal_one_def,hypreal_add]));
  2.1849 +qed "hypreal_of_nat_iff";
  2.1850 +
  2.1851 +Goal "inj hypreal_of_nat";
  2.1852 +by (rtac injI 1);
  2.1853 +by (auto_tac (claset() addSDs [FreeUltrafilterNat_P],
  2.1854 +        simpset() addsimps [hypreal_of_nat_iff,
  2.1855 +        real_add_right_cancel,inj_real_of_nat RS injD]));
  2.1856 +qed "inj_hypreal_of_nat";
  2.1857 +
  2.1858 +Goalw [hypreal_of_nat_def,hypreal_of_real_def,hypreal_of_posnat_def,
  2.1859 +       real_of_posnat_def,hypreal_one_def,real_of_nat_def] 
  2.1860 +       "hypreal_of_nat n = hypreal_of_real (real_of_nat n)";
  2.1861 +by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1);
  2.1862 +qed "hypreal_of_nat_real_of_nat";
  2.1863 +
  2.1864 +
  2.1865 +
  2.1866 +
  2.1867 +
  2.1868 +
  2.1869 +
  2.1870 +
  2.1871 +
  2.1872 +
  2.1873 +
  2.1874 +
  2.1875 +
  2.1876 +
  2.1877 +
  2.1878 +
  2.1879 +
  2.1880 +
  2.1881 +
  2.1882 +
  2.1883 +
  2.1884 +
  2.1885 +
  2.1886 +
  2.1887 +
  2.1888 +
  2.1889 +
  2.1890 +
  2.1891 +
  2.1892 +
  2.1893 +
  2.1894 +
  2.1895 +
  2.1896 +
  2.1897 +
  2.1898 +
  2.1899 +
  2.1900 +
  2.1901 +
  2.1902 +
  2.1903 +
  2.1904 +
  2.1905 +
  2.1906 +
  2.1907 +
  2.1908 +
  2.1909 +
  2.1910 +
  2.1911 +
  2.1912 +
  2.1913 +
  2.1914 +
  2.1915 +
  2.1916 +
  2.1917 +
  2.1918 +
  2.1919 +
  2.1920 +
  2.1921 +
  2.1922 +
  2.1923 +
  2.1924 +
  2.1925 +
  2.1926 +
  2.1927 +
  2.1928 +
  2.1929 +
  2.1930 +
  2.1931 +
  2.1932 +
  2.1933 +
  2.1934 +
  2.1935 +
  2.1936 +
  2.1937 +
  2.1938 +
  2.1939 +
  2.1940 +
  2.1941 +
  2.1942 +
  2.1943 +
  2.1944 +
  2.1945 +
  2.1946 +
  2.1947 +
  2.1948 +
  2.1949 +
  2.1950 +
  2.1951 +
  2.1952 +
  2.1953 +
  2.1954 +
  2.1955 +
  2.1956 +
  2.1957 +
  2.1958 +
  2.1959 +
  2.1960 +
  2.1961 +
  2.1962 +
  2.1963 +
  2.1964 +
  2.1965 +
  2.1966 +
  2.1967 +
  2.1968 +
  2.1969 +
  2.1970 +
  2.1971 +
  2.1972 +
  2.1973 +
  2.1974 +
  2.1975 +
  2.1976 +
  2.1977 +
  2.1978 +
  2.1979 +
  2.1980 +
  2.1981 +
  2.1982 +
  2.1983 +
  2.1984 +
  2.1985 +
  2.1986 +
  2.1987 +
  2.1988 +
  2.1989 +
  2.1990 +
  2.1991 +
  2.1992 +
  2.1993 +
  2.1994 +
  2.1995 +
  2.1996 +
  2.1997 +
  2.1998 +
  2.1999 +
  2.2000 +
  2.2001 +
  2.2002 +
  2.2003 +
  2.2004 +
  2.2005 +
  2.2006 +
  2.2007 +
  2.2008 +
  2.2009 +
  2.2010 +
  2.2011 +
  2.2012 +
  2.2013 +
  2.2014 +
  2.2015 +
  2.2016 +
  2.2017 +
  2.2018 +
  2.2019 +
  2.2020 +
  2.2021 +
  2.2022 +
  2.2023 +
  2.2024 +
  2.2025 +
  2.2026 +
  2.2027 +
  2.2028 +
  2.2029 +
  2.2030 +
  2.2031 +
  2.2032 +
  2.2033 +
  2.2034 +
  2.2035 +
  2.2036 +
  2.2037 +
  2.2038 +
  2.2039 +
  2.2040 +
  2.2041 +
  2.2042 +
  2.2043 +
  2.2044 +
  2.2045 +
  2.2046 +
  2.2047 +
  2.2048 +
  2.2049 +
  2.2050 +
  2.2051 +
  2.2052 +
  2.2053 +
  2.2054 +
  2.2055 +
  2.2056 +
  2.2057 +
  2.2058 +
  2.2059 +
  2.2060 +
  2.2061 +
  2.2062 +
  2.2063 +
  2.2064 +
  2.2065 +
  2.2066 +
  2.2067 +
  2.2068 +
  2.2069 +
  2.2070 +
  2.2071 +
  2.2072 +
  2.2073 +
  2.2074 +
  2.2075 +
  2.2076 +
  2.2077 +
  2.2078 +
  2.2079 +
  2.2080 +
  2.2081 +
  2.2082 +
  2.2083 +
  2.2084 +
  2.2085 +
  2.2086 +
  2.2087 +
  2.2088 +
  2.2089 +
  2.2090 +
  2.2091 +
  2.2092 +
  2.2093 +
  2.2094 +
  2.2095 +
  2.2096 +
  2.2097 +
  2.2098 +
  2.2099 +
  2.2100 +
  2.2101 +
  2.2102 +
  2.2103 +
  2.2104 +
  2.2105 +
  2.2106 +
  2.2107 +
  2.2108 +
  2.2109 +
  2.2110 +
  2.2111 +
  2.2112 +
  2.2113 +
  2.2114 +
  2.2115 +
  2.2116 +
  2.2117 +
  2.2118 +
  2.2119 +
  2.2120 +
  2.2121 +
  2.2122 +
  2.2123 +
  2.2124 +
  2.2125 +
  2.2126 +
  2.2127 +
  2.2128 +
  2.2129 +
  2.2130 +
  2.2131 +
  2.2132 +
  2.2133 +
  2.2134 +
  2.2135 +
  2.2136 +
  2.2137 +
  2.2138 +
  2.2139 +
  2.2140 +
  2.2141 +
  2.2142 +
  2.2143 +
  2.2144 +
  2.2145 +
  2.2146 +
  2.2147 +
  2.2148 +
  2.2149 +
  2.2150 +
  2.2151 +
  2.2152 +
  2.2153 +
  2.2154 +
  2.2155 +
  2.2156 +
  2.2157 +
  2.2158 +
  2.2159 +
  2.2160 +
  2.2161 +
  2.2162 +
  2.2163 +
  2.2164 +
  2.2165 +
  2.2166 +
  2.2167 +
  2.2168 +
  2.2169 +
  2.2170 +
  2.2171 +
  2.2172 +
  2.2173 +
  2.2174 +
  2.2175 +
  2.2176 +
  2.2177 +
  2.2178 +
  2.2179 +
  2.2180 +
  2.2181 +
  2.2182 +
  2.2183 +
  2.2184 +
  2.2185 +
  2.2186 +
  2.2187 +
  2.2188 +
  2.2189 +
  2.2190 +
  2.2191 +
  2.2192 +
  2.2193 +
  2.2194 +
  2.2195 +
  2.2196 +
  2.2197 +
  2.2198 +
  2.2199 +
  2.2200 +
  2.2201 +
  2.2202 +
  2.2203 +
  2.2204 +
  2.2205 +
  2.2206 +
  2.2207 +
  2.2208 +
  2.2209 +
  2.2210 +
  2.2211 +
  2.2212 +
  2.2213 +
  2.2214 +
  2.2215 +
  2.2216 +
  2.2217 +
  2.2218 +
  2.2219 +
  2.2220 +
  2.2221 +
  2.2222 +
  2.2223 +
  2.2224 +
  2.2225 +
  2.2226 +
  2.2227 +
  2.2228 +
  2.2229 +
  2.2230 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.thy	Mon Aug 16 18:41:06 1999 +0200
     3.3 @@ -0,0 +1,91 @@
     3.4 +(*  Title       : HOL/Real/Hyperreal/HyperDef.thy
     3.5 +    ID          : $Id$
     3.6 +    Author      : Jacques D. Fleuriot
     3.7 +    Copyright   : 1998  University of Cambridge
     3.8 +    Description : Construction of hyperreals using ultrafilters
     3.9 +*) 
    3.10 +
    3.11 +HyperDef = Filter + Real +
    3.12 +
    3.13 +consts 
    3.14 + 
    3.15 +    FreeUltrafilterNat   :: nat set set
    3.16 +
    3.17 +defs
    3.18 +
    3.19 +    FreeUltrafilterNat_def
    3.20 +    "FreeUltrafilterNat    ==   (@U. U : FreeUltrafilter (UNIV:: nat set))"
    3.21 +
    3.22 +
    3.23 +constdefs
    3.24 +    hyprel :: "((nat=>real)*(nat=>real)) set"
    3.25 +    "hyprel == {p. ? X Y. p = ((X::nat=>real),Y) & 
    3.26 +                   {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
    3.27 +
    3.28 +typedef hypreal = "{x::nat=>real. True}/hyprel"              (Equiv.quotient_def)
    3.29 +
    3.30 +instance
    3.31 +   hypreal  :: {ord,plus,times,minus}
    3.32 +
    3.33 +consts 
    3.34 +
    3.35 +  "0hr"       :: hypreal               ("0hr")   
    3.36 +  "1hr"       :: hypreal               ("1hr")  
    3.37 +  "whr"       :: hypreal               ("whr")  
    3.38 +  "ehr"       :: hypreal               ("ehr")  
    3.39 +
    3.40 +
    3.41 +defs
    3.42 +
    3.43 +  hypreal_zero_def     "0hr == Abs_hypreal(hyprel^^{%n::nat. 0r})"
    3.44 +  hypreal_one_def      "1hr == Abs_hypreal(hyprel^^{%n::nat. 1r})"
    3.45 +
    3.46 +  (* an infinite number = [<1,2,3,...>] *)
    3.47 +  omega_def   "whr == Abs_hypreal(hyprel^^{%n::nat. real_of_posnat n})"
    3.48 +    
    3.49 +  (* an infinitesimal number = [<1,1/2,1/3,...>] *)
    3.50 +  epsilon_def "ehr == Abs_hypreal(hyprel^^{%n::nat. rinv(real_of_posnat n)})"
    3.51 +
    3.52 +  hypreal_minus_def
    3.53 +  "- P         == Abs_hypreal(UN X: Rep_hypreal(P). hyprel^^{%n::nat. - (X n)})"
    3.54 +
    3.55 +  hypreal_diff_def 
    3.56 +  "x - y == x + -(y::hypreal)"
    3.57 +
    3.58 +constdefs
    3.59 +
    3.60 +  hypreal_of_real  :: real => hypreal                 ("&# _" [80] 80)
    3.61 +  "hypreal_of_real r         == Abs_hypreal(hyprel^^{%n::nat. r})"
    3.62 +  
    3.63 +  hrinv       :: hypreal => hypreal
    3.64 +  "hrinv(P)   == Abs_hypreal(UN X: Rep_hypreal(P). 
    3.65 +                    hyprel^^{%n. if X n = 0r then 0r else rinv(X n)})"
    3.66 +
    3.67 +  (* n::nat --> (n+1)::hypreal *)
    3.68 +  hypreal_of_posnat :: nat => hypreal                ("&&# _" [80] 80)
    3.69 +  "hypreal_of_posnat n  == (hypreal_of_real(real_of_preal
    3.70 +                            (preal_of_prat(prat_of_pnat(pnat_of_nat n)))))"
    3.71 +
    3.72 +  hypreal_of_nat :: nat => hypreal                   ("&&## _" [80] 80)
    3.73 +  "hypreal_of_nat n      == hypreal_of_posnat n + -1hr"
    3.74 +
    3.75 +defs 
    3.76 +
    3.77 +  hypreal_add_def  
    3.78 +  "P + Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
    3.79 +                hyprel^^{%n::nat. X n + Y n})"
    3.80 +
    3.81 +  hypreal_mult_def  
    3.82 +  "P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
    3.83 +                hyprel^^{%n::nat. X n * Y n})"
    3.84 +
    3.85 +  hypreal_less_def
    3.86 +  "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) & 
    3.87 +                               Y: Rep_hypreal(Q) & 
    3.88 +                               {n::nat. X n < Y n} : FreeUltrafilterNat"
    3.89 +  hypreal_le_def
    3.90 +  "P <= (Q::hypreal) == ~(Q < P)" 
    3.91 +
    3.92 +end
    3.93 + 
    3.94 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Real/Hyperreal/fuf.ML	Mon Aug 16 18:41:06 1999 +0200
     4.3 @@ -0,0 +1,82 @@
     4.4 +(*  Title       : HOL/Real/Hyperreal/fuf.ml
     4.5 +    ID          : $Id$
     4.6 +    Author      : Jacques D. Fleuriot
     4.7 +    Copyright   : 1998  University of Cambridge
     4.8 +                  1999  University of Edinburgh
     4.9 +    Description : Simple tactics to help proofs involving our 
    4.10 +                  free ultrafilter (FreeUltrafilterNat). We rely
    4.11 +                  on the fact that filters satisfy the  finite 
    4.12 +                  intersection property.
    4.13 +*)
    4.14 +
    4.15 +exception FUFempty;
    4.16 +
    4.17 +fun get_fuf_hyps [] zs = zs
    4.18 +|   get_fuf_hyps (x::xs) zs = 
    4.19 +        case (concl_of x) of 
    4.20 +        (_ $ (Const ("Not",_) $ (Const ("op :",_) $ _ $
    4.21 +             Const ("HyperDef.FreeUltrafilterNat",_)))) =>  get_fuf_hyps xs 
    4.22 +                                              ((x RS FreeUltrafilterNat_Compl_mem)::zs)
    4.23 +       |(_ $ (Const ("op :",_) $ _ $
    4.24 +             Const ("HyperDef.FreeUltrafilterNat",_)))  =>  get_fuf_hyps xs (x::zs)
    4.25 +       | _ => get_fuf_hyps xs zs;
    4.26 +
    4.27 +fun Intprems [] = raise FUFempty
    4.28 +|   Intprems [x] = x
    4.29 +|   Intprems (x::y::ys) = 
    4.30 +      Intprems (([x,y] MRS FreeUltrafilterNat_Int) :: ys);
    4.31 +
    4.32 +(*---------------------------------------------------------------  
    4.33 +   solves goals of the form 
    4.34 +    [| A1: FUF; A2: FUF; ...; An: FUF |] ==> B : FUF   
    4.35 +   where A1 Int A2 Int ... Int An <= B 
    4.36 + ---------------------------------------------------------------*)
    4.37 +
    4.38 +val Fuf_tac = METAHYPS(fn prems =>
    4.39 +                    (rtac ((Intprems (get_fuf_hyps prems [])) RS
    4.40 +                           FreeUltrafilterNat_subset) 1) THEN 
    4.41 +                    Auto_tac);
    4.42 +
    4.43 +fun fuf_tac (fclaset,fsimpset) i = METAHYPS(fn prems =>
    4.44 +                    (rtac ((Intprems (get_fuf_hyps prems [])) RS
    4.45 +                           FreeUltrafilterNat_subset) 1) THEN 
    4.46 +                    auto_tac (fclaset,fsimpset)) i;
    4.47 +
    4.48 +(*---------------------------------------------------------------  
    4.49 +   solves goals of the form 
    4.50 +    [| A1: FUF; A2: FUF; ...; An: FUF |] ==> P
    4.51 +   where A1 Int A2 Int ... Int An <= {} since {} ~: FUF
    4.52 +   (i.e. uses fact that FUF is a proper filter)
    4.53 + ---------------------------------------------------------------*)
    4.54 +
    4.55 +val Fuf_empty_tac = METAHYPS(fn prems => 
    4.56 +                    (rtac ((Intprems (get_fuf_hyps prems [])) RS
    4.57 +                           (FreeUltrafilterNat_subset RS 
    4.58 +                           (FreeUltrafilterNat_empty RS notE))) 1) 
    4.59 +                     THEN Auto_tac);
    4.60 +
    4.61 +fun fuf_empty_tac (fclaset,fsimpset) i = METAHYPS(fn prems => 
    4.62 +                    (rtac ((Intprems (get_fuf_hyps prems [])) RS
    4.63 +                           (FreeUltrafilterNat_subset RS 
    4.64 +                          (FreeUltrafilterNat_empty RS notE))) 1) 
    4.65 +                     THEN auto_tac (fclaset,fsimpset)) i;
    4.66 +
    4.67 +(*---------------------------------------------------------------  
    4.68 +  All in one -- not really needed.
    4.69 + ---------------------------------------------------------------*)
    4.70 +
    4.71 +fun Fuf_auto_tac i = SOLVE (Fuf_empty_tac i) ORELSE TRY(Fuf_tac i);
    4.72 +
    4.73 +fun fuf_auto_tac (fclaset,fsimpset) i = 
    4.74 +     SOLVE (fuf_empty_tac (fclaset,fsimpset) i) 
    4.75 +     ORELSE TRY(fuf_tac (fclaset,fsimpset) i);
    4.76 +
    4.77 +(*---------------------------------------------------------------  
    4.78 +   In fact could make this the only tactic: just need to
    4.79 +   use contraposition and then look for empty set.
    4.80 + ---------------------------------------------------------------*)
    4.81 +
    4.82 +fun Ultra_tac i = rtac ccontr i THEN Fuf_empty_tac i;
    4.83 +fun ultra_tac (fclaset,fsimpset) i = rtac ccontr i THEN 
    4.84 +              fuf_empty_tac (fclaset,fsimpset) i;
    4.85 +