src/HOL/Real/Hyperreal/HyperDef.ML
author wenzelm
Tue Sep 07 10:40:58 1999 +0200 (1999-09-07)
changeset 7499 23e090051cb8
parent 7322 d16d7ddcc842
child 7825 1be9b63e7d93
permissions -rw-r--r--
isatool expandshort;
     1 (*  Title       : HOL/Real/Hyperreal/Hyper.ML
     2     ID          : $Id$
     3     Author      : Jacques D. Fleuriot
     4     Copyright   : 1998  University of Cambridge
     5     Description : Ultrapower construction of hyperreals
     6 *) 
     7 
     8 (*------------------------------------------------------------------------
     9              Proof that the set of naturals is not finite
    10  ------------------------------------------------------------------------*)
    11 
    12 (*** based on James' proof that the set of naturals is not finite ***)
    13 Goal "finite (A::nat set) --> (? n. !m. Suc (n + m) ~: A)";
    14 by (rtac impI 1);
    15 by (eres_inst_tac [("F","A")] finite_induct 1);
    16 by (Blast_tac 1 THEN etac exE 1);
    17 by (res_inst_tac [("x","n + x")] exI 1);
    18 by (rtac allI 1 THEN eres_inst_tac [("x","x + m")] allE 1);
    19 by (auto_tac (claset(), simpset() addsimps add_ac));
    20 by (auto_tac (claset(),
    21 	      simpset() addsimps [add_assoc RS sym,
    22 				  less_add_Suc2 RS less_not_refl2]));
    23 qed_spec_mp "finite_exhausts";
    24 
    25 Goal "finite (A :: nat set) --> (? n. n ~:A)";
    26 by (rtac impI 1 THEN dtac finite_exhausts 1);
    27 by (Blast_tac 1);
    28 qed_spec_mp "finite_not_covers";
    29 
    30 Goal "~ finite(UNIV:: nat set)";
    31 by (fast_tac (claset() addSDs [finite_exhausts]) 1);
    32 qed "not_finite_nat";
    33 
    34 (*------------------------------------------------------------------------
    35    Existence of free ultrafilter over the naturals and proof of various 
    36    properties of the FreeUltrafilterNat- an arbitrary free ultrafilter
    37  ------------------------------------------------------------------------*)
    38 
    39 Goal "EX U. U: FreeUltrafilter (UNIV::nat set)";
    40 by (rtac (not_finite_nat RS FreeUltrafilter_Ex) 1);
    41 qed "FreeUltrafilterNat_Ex";
    42 
    43 Goalw [FreeUltrafilterNat_def] 
    44      "FreeUltrafilterNat: FreeUltrafilter(UNIV:: nat set)";
    45 by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
    46 by (rtac selectI2 1 THEN ALLGOALS(assume_tac));
    47 qed "FreeUltrafilterNat_mem";
    48 Addsimps [FreeUltrafilterNat_mem];
    49 
    50 Goalw [FreeUltrafilterNat_def] "finite x ==> x ~: FreeUltrafilterNat";
    51 by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
    52 by (rtac selectI2 1 THEN assume_tac 1);
    53 by (blast_tac (claset() addDs [mem_FreeUltrafiltersetD1]) 1);
    54 qed "FreeUltrafilterNat_finite";
    55 
    56 Goal "x: FreeUltrafilterNat ==> ~ finite x";
    57 by (blast_tac (claset() addDs [FreeUltrafilterNat_finite]) 1);
    58 qed "FreeUltrafilterNat_not_finite";
    59 
    60 Goalw [FreeUltrafilterNat_def] "{} ~: FreeUltrafilterNat";
    61 by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
    62 by (rtac selectI2 1 THEN assume_tac 1);
    63 by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter,
    64 			       Ultrafilter_Filter,Filter_empty_not_mem]) 1);
    65 qed "FreeUltrafilterNat_empty";
    66 Addsimps [FreeUltrafilterNat_empty];
    67 
    68 Goal "[| X: FreeUltrafilterNat;  Y: FreeUltrafilterNat |]  \
    69 \     ==> X Int Y : FreeUltrafilterNat";
    70 by (cut_facts_tac [FreeUltrafilterNat_mem] 1);
    71 by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter,
    72 			       Ultrafilter_Filter,mem_FiltersetD1]) 1);
    73 qed "FreeUltrafilterNat_Int";
    74 
    75 Goal "[| X: FreeUltrafilterNat;  X <= Y |] \
    76 \     ==> Y : FreeUltrafilterNat";
    77 by (cut_facts_tac [FreeUltrafilterNat_mem] 1);
    78 by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter,
    79 			       Ultrafilter_Filter,mem_FiltersetD2]) 1);
    80 qed "FreeUltrafilterNat_subset";
    81 
    82 Goal "X: FreeUltrafilterNat ==> -X ~: FreeUltrafilterNat";
    83 by (Step_tac 1);
    84 by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
    85 by Auto_tac;
    86 qed "FreeUltrafilterNat_Compl";
    87 
    88 Goal "X~: FreeUltrafilterNat ==> -X : FreeUltrafilterNat";
    89 by (cut_facts_tac [FreeUltrafilterNat_mem RS (FreeUltrafilter_iff RS iffD1)] 1);
    90 by (Step_tac 1 THEN dres_inst_tac [("x","X")] bspec 1);
    91 by (auto_tac (claset(),simpset() addsimps [UNIV_diff_Compl]));
    92 qed "FreeUltrafilterNat_Compl_mem";
    93 
    94 Goal "(X ~: FreeUltrafilterNat) = (-X: FreeUltrafilterNat)";
    95 by (blast_tac (claset() addDs [FreeUltrafilterNat_Compl,
    96 			       FreeUltrafilterNat_Compl_mem]) 1);
    97 qed "FreeUltrafilterNat_Compl_iff1";
    98 
    99 Goal "(X: FreeUltrafilterNat) = (-X ~: FreeUltrafilterNat)";
   100 by (auto_tac (claset(),
   101 	      simpset() addsimps [FreeUltrafilterNat_Compl_iff1 RS sym]));
   102 qed "FreeUltrafilterNat_Compl_iff2";
   103 
   104 Goal "(UNIV::nat set) : FreeUltrafilterNat";
   105 by (rtac (FreeUltrafilterNat_mem RS FreeUltrafilter_Ultrafilter RS 
   106           Ultrafilter_Filter RS mem_FiltersetD4) 1);
   107 qed "FreeUltrafilterNat_UNIV";
   108 Addsimps [FreeUltrafilterNat_UNIV];
   109 
   110 Goal "{n::nat. True}: FreeUltrafilterNat";
   111 by (subgoal_tac "{n::nat. True} = (UNIV::nat set)" 1);
   112 by Auto_tac;
   113 qed "FreeUltrafilterNat_Nat_set";
   114 Addsimps [FreeUltrafilterNat_Nat_set];
   115 
   116 Goal "{n. P(n) = P(n)} : FreeUltrafilterNat";
   117 by (Simp_tac 1);
   118 qed "FreeUltrafilterNat_Nat_set_refl";
   119 AddIs [FreeUltrafilterNat_Nat_set_refl];
   120 
   121 Goal "{n::nat. P} : FreeUltrafilterNat ==> P";
   122 by (rtac ccontr 1);
   123 by (rotate_tac 1 1);
   124 by (Asm_full_simp_tac 1);
   125 qed "FreeUltrafilterNat_P";
   126 
   127 Goal "{n. P(n)} : FreeUltrafilterNat ==> EX n. P(n)";
   128 by (rtac ccontr 1 THEN rotate_tac 1 1);
   129 by (Asm_full_simp_tac 1);
   130 qed "FreeUltrafilterNat_Ex_P";
   131 
   132 Goal "ALL n. P(n) ==> {n. P(n)} : FreeUltrafilterNat";
   133 by (auto_tac (claset() addIs [FreeUltrafilterNat_Nat_set],simpset()));
   134 qed "FreeUltrafilterNat_all";
   135 
   136 (*-----------------------------------------
   137      Define and use Ultrafilter tactics
   138  -----------------------------------------*)
   139 use "fuf.ML";
   140 
   141 
   142 
   143 (*------------------------------------------------------
   144    Now prove one further property of our free ultrafilter
   145  -------------------------------------------------------*)
   146 Goal "X Un Y: FreeUltrafilterNat \
   147 \     ==> X: FreeUltrafilterNat | Y: FreeUltrafilterNat";
   148 by Auto_tac;
   149 by (Ultra_tac 1);
   150 qed "FreeUltrafilterNat_Un";
   151 
   152 (*------------------------------------------------------------------------
   153                        Properties of hyprel
   154  ------------------------------------------------------------------------*)
   155 
   156 (** Proving that hyprel is an equivalence relation **)
   157 (** Natural deduction for hyprel **)
   158 
   159 Goalw [hyprel_def]
   160    "((X,Y): hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)";
   161 by (Fast_tac 1);
   162 qed "hyprel_iff";
   163 
   164 Goalw [hyprel_def] 
   165      "{n. X n = Y n}: FreeUltrafilterNat  ==> (X,Y): hyprel";
   166 by (Fast_tac 1);
   167 qed "hyprelI";
   168 
   169 Goalw [hyprel_def]
   170   "p: hyprel --> (EX X Y. \
   171 \                 p = (X,Y) & {n. X n = Y n} : FreeUltrafilterNat)";
   172 by (Fast_tac 1);
   173 qed "hyprelE_lemma";
   174 
   175 val [major,minor] = goal thy
   176   "[| p: hyprel;  \
   177 \     !!X Y. [| p = (X,Y); {n. X n = Y n}: FreeUltrafilterNat\
   178 \                    |] ==> Q |] ==> Q";
   179 by (cut_facts_tac [major RS (hyprelE_lemma RS mp)] 1);
   180 by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
   181 qed "hyprelE";
   182 
   183 AddSIs [hyprelI];
   184 AddSEs [hyprelE];
   185 
   186 Goalw [hyprel_def] "(x,x): hyprel";
   187 by (auto_tac (claset(),simpset() addsimps 
   188          [FreeUltrafilterNat_Nat_set]));
   189 qed "hyprel_refl";
   190 
   191 Goal "{n. X n = Y n} = {n. Y n = X n}";
   192 by Auto_tac;
   193 qed "lemma_perm";
   194 
   195 Goalw [hyprel_def] "(x,y): hyprel --> (y,x):hyprel";
   196 by (auto_tac (claset() addIs [lemma_perm RS subst],simpset()));
   197 qed_spec_mp "hyprel_sym";
   198 
   199 Goalw [hyprel_def]
   200       "(x,y): hyprel --> (y,z):hyprel --> (x,z):hyprel";
   201 by Auto_tac;
   202 by (Ultra_tac 1);
   203 qed_spec_mp "hyprel_trans";
   204 
   205 Goalw [equiv_def, refl_def, sym_def, trans_def]
   206     "equiv {x::nat=>real. True} hyprel";
   207 by (auto_tac (claset() addSIs [hyprel_refl] 
   208                        addSEs [hyprel_sym,hyprel_trans] 
   209                        delrules [hyprelI,hyprelE],
   210 	      simpset() addsimps [FreeUltrafilterNat_Nat_set]));
   211 qed "equiv_hyprel";
   212 
   213 val equiv_hyprel_iff =
   214     [TrueI, TrueI] MRS 
   215     ([CollectI, CollectI] MRS 
   216     (equiv_hyprel RS eq_equiv_class_iff));
   217 
   218 Goalw  [hypreal_def,hyprel_def,quotient_def] "hyprel^^{x}:hypreal";
   219 by (Blast_tac 1);
   220 qed "hyprel_in_hypreal";
   221 
   222 Goal "inj_on Abs_hypreal hypreal";
   223 by (rtac inj_on_inverseI 1);
   224 by (etac Abs_hypreal_inverse 1);
   225 qed "inj_on_Abs_hypreal";
   226 
   227 Addsimps [equiv_hyprel_iff,inj_on_Abs_hypreal RS inj_on_iff,
   228           hyprel_iff, hyprel_in_hypreal, Abs_hypreal_inverse];
   229 
   230 Addsimps [equiv_hyprel RS eq_equiv_class_iff];
   231 val eq_hyprelD = equiv_hyprel RSN (2,eq_equiv_class);
   232 
   233 Goal "inj(Rep_hypreal)";
   234 by (rtac inj_inverseI 1);
   235 by (rtac Rep_hypreal_inverse 1);
   236 qed "inj_Rep_hypreal";
   237 
   238 Goalw [hyprel_def] "x: hyprel ^^ {x}";
   239 by (Step_tac 1);
   240 by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset()));
   241 qed "lemma_hyprel_refl";
   242 
   243 Addsimps [lemma_hyprel_refl];
   244 
   245 Goalw [hypreal_def] "{} ~: hypreal";
   246 by (auto_tac (claset() addSEs [quotientE], simpset()));
   247 qed "hypreal_empty_not_mem";
   248 
   249 Addsimps [hypreal_empty_not_mem];
   250 
   251 Goal "Rep_hypreal x ~= {}";
   252 by (cut_inst_tac [("x","x")] Rep_hypreal 1);
   253 by Auto_tac;
   254 qed "Rep_hypreal_nonempty";
   255 
   256 Addsimps [Rep_hypreal_nonempty];
   257 
   258 (*------------------------------------------------------------------------
   259    hypreal_of_real: the injection from real to hypreal
   260  ------------------------------------------------------------------------*)
   261 
   262 Goal "inj(hypreal_of_real)";
   263 by (rtac injI 1);
   264 by (rewtac hypreal_of_real_def);
   265 by (dtac (inj_on_Abs_hypreal RS inj_onD) 1);
   266 by (REPEAT (rtac hyprel_in_hypreal 1));
   267 by (dtac eq_equiv_class 1);
   268 by (rtac equiv_hyprel 1);
   269 by (Fast_tac 1);
   270 by (rtac ccontr 1 THEN rotate_tac 1 1);
   271 by Auto_tac;
   272 qed "inj_hypreal_of_real";
   273 
   274 val [prem] = goal thy
   275     "(!!x y. z = Abs_hypreal(hyprel^^{x}) ==> P) ==> P";
   276 by (res_inst_tac [("x1","z")] 
   277     (rewrite_rule [hypreal_def] Rep_hypreal RS quotientE) 1);
   278 by (dres_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   279 by (res_inst_tac [("x","x")] prem 1);
   280 by (asm_full_simp_tac (simpset() addsimps [Rep_hypreal_inverse]) 1);
   281 qed "eq_Abs_hypreal";
   282 
   283 (**** hypreal_minus: additive inverse on hypreal ****)
   284 
   285 Goalw [congruent_def]
   286   "congruent hyprel (%X. hyprel^^{%n. - (X n)})";
   287 by Safe_tac;
   288 by (ALLGOALS Ultra_tac);
   289 qed "hypreal_minus_congruent";
   290 
   291 (*Resolve th against the corresponding facts for hypreal_minus*)
   292 val hypreal_minus_ize = RSLIST [equiv_hyprel, hypreal_minus_congruent];
   293 
   294 Goalw [hypreal_minus_def]
   295       "- (Abs_hypreal(hyprel^^{%n. X n})) = Abs_hypreal(hyprel ^^ {%n. -(X n)})";
   296 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   297 by (simp_tac (simpset() addsimps 
   298    [hyprel_in_hypreal RS Abs_hypreal_inverse,hypreal_minus_ize UN_equiv_class]) 1);
   299 qed "hypreal_minus";
   300 
   301 Goal "- (- z) = (z::hypreal)";
   302 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   303 by (asm_simp_tac (simpset() addsimps [hypreal_minus]) 1);
   304 qed "hypreal_minus_minus";
   305 
   306 Addsimps [hypreal_minus_minus];
   307 
   308 Goal "inj(%r::hypreal. -r)";
   309 by (rtac injI 1);
   310 by (dres_inst_tac [("f","uminus")] arg_cong 1);
   311 by (asm_full_simp_tac (simpset() addsimps [hypreal_minus_minus]) 1);
   312 qed "inj_hypreal_minus";
   313 
   314 Goalw [hypreal_zero_def] "-0hr = 0hr";
   315 by (simp_tac (simpset() addsimps [hypreal_minus]) 1);
   316 qed "hypreal_minus_zero";
   317 
   318 Addsimps [hypreal_minus_zero];
   319 
   320 Goal "(-x = 0hr) = (x = 0hr)"; 
   321 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   322 by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def,
   323     hypreal_minus] @ real_add_ac));
   324 qed "hypreal_minus_zero_iff";
   325 
   326 Addsimps [hypreal_minus_zero_iff];
   327 (**** hrinv: multiplicative inverse on hypreal ****)
   328 
   329 Goalw [congruent_def]
   330   "congruent hyprel (%X. hyprel^^{%n. if X n = 0r then 0r else rinv(X n)})";
   331 by (Auto_tac THEN Ultra_tac 1);
   332 qed "hypreal_hrinv_congruent";
   333 
   334 (* Resolve th against the corresponding facts for hrinv *)
   335 val hypreal_hrinv_ize = RSLIST [equiv_hyprel, hypreal_hrinv_congruent];
   336 
   337 Goalw [hrinv_def]
   338       "hrinv (Abs_hypreal(hyprel^^{%n. X n})) = \
   339 \      Abs_hypreal(hyprel ^^ {%n. if X n = 0r then 0r else rinv(X n)})";
   340 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   341 by (simp_tac (simpset() addsimps 
   342    [hyprel_in_hypreal RS Abs_hypreal_inverse,hypreal_hrinv_ize UN_equiv_class]) 1);
   343 qed "hypreal_hrinv";
   344 
   345 Goal "z ~= 0hr ==> hrinv (hrinv z) = z";
   346 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   347 by (rotate_tac 1 1);
   348 by (asm_full_simp_tac (simpset() addsimps 
   349     [hypreal_hrinv,hypreal_zero_def] setloop (split_tac [expand_if])) 1);
   350 by (ultra_tac (claset() addDs [rinv_not_zero,real_rinv_rinv],simpset()) 1);
   351 qed "hypreal_hrinv_hrinv";
   352 
   353 Addsimps [hypreal_hrinv_hrinv];
   354 
   355 Goalw [hypreal_one_def] "hrinv(1hr) = 1hr";
   356 by (full_simp_tac (simpset() addsimps [hypreal_hrinv,
   357        real_zero_not_eq_one RS not_sym] 
   358                    setloop (split_tac [expand_if])) 1);
   359 qed "hypreal_hrinv_1";
   360 Addsimps [hypreal_hrinv_1];
   361 
   362 (**** hyperreal addition: hypreal_add  ****)
   363 
   364 Goalw [congruent2_def]
   365     "congruent2 hyprel (%X Y. hyprel^^{%n. X n + Y n})";
   366 by Safe_tac;
   367 by (ALLGOALS(Ultra_tac));
   368 qed "hypreal_add_congruent2";
   369 
   370 (*Resolve th against the corresponding facts for hyppreal_add*)
   371 val hypreal_add_ize = RSLIST [equiv_hyprel, hypreal_add_congruent2];
   372 
   373 Goalw [hypreal_add_def]
   374   "Abs_hypreal(hyprel^^{%n. X n}) + Abs_hypreal(hyprel^^{%n. Y n}) = \
   375 \  Abs_hypreal(hyprel^^{%n. X n + Y n})";
   376 by (asm_simp_tac
   377     (simpset() addsimps [hypreal_add_ize UN_equiv_class2]) 1);
   378 qed "hypreal_add";
   379 
   380 Goal "(z::hypreal) + w = w + z";
   381 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   382 by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
   383 by (asm_simp_tac (simpset() addsimps (real_add_ac @ [hypreal_add])) 1);
   384 qed "hypreal_add_commute";
   385 
   386 Goal "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)";
   387 by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
   388 by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
   389 by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
   390 by (asm_simp_tac (simpset() addsimps [hypreal_add, real_add_assoc]) 1);
   391 qed "hypreal_add_assoc";
   392 
   393 (*For AC rewriting*)
   394 Goal "(x::hypreal)+(y+z)=y+(x+z)";
   395 by (rtac (hypreal_add_commute RS trans) 1);
   396 by (rtac (hypreal_add_assoc RS trans) 1);
   397 by (rtac (hypreal_add_commute RS arg_cong) 1);
   398 qed "hypreal_add_left_commute";
   399 
   400 (* hypreal addition is an AC operator *)
   401 val hypreal_add_ac = [hypreal_add_assoc,hypreal_add_commute,
   402                       hypreal_add_left_commute];
   403 
   404 Goalw [hypreal_zero_def] "0hr + z = z";
   405 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   406 by (asm_full_simp_tac (simpset() addsimps 
   407     [hypreal_add]) 1);
   408 qed "hypreal_add_zero_left";
   409 
   410 Goal "z + 0hr = z";
   411 by (simp_tac (simpset() addsimps 
   412     [hypreal_add_zero_left,hypreal_add_commute]) 1);
   413 qed "hypreal_add_zero_right";
   414 
   415 Goalw [hypreal_zero_def] "z + -z = 0hr";
   416 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   417 by (asm_full_simp_tac (simpset() addsimps [hypreal_minus,
   418         hypreal_add]) 1);
   419 qed "hypreal_add_minus";
   420 
   421 Goal "-z + z = 0hr";
   422 by (simp_tac (simpset() addsimps 
   423     [hypreal_add_commute,hypreal_add_minus]) 1);
   424 qed "hypreal_add_minus_left";
   425 
   426 Addsimps [hypreal_add_minus,hypreal_add_minus_left,
   427           hypreal_add_zero_left,hypreal_add_zero_right];
   428 
   429 Goal "? y. (x::hypreal) + y = 0hr";
   430 by (fast_tac (claset() addIs [hypreal_add_minus]) 1);
   431 qed "hypreal_minus_ex";
   432 
   433 Goal "?! y. (x::hypreal) + y = 0hr";
   434 by (auto_tac (claset() addIs [hypreal_add_minus],simpset()));
   435 by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
   436 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   437 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   438 qed "hypreal_minus_ex1";
   439 
   440 Goal "?! y. y + (x::hypreal) = 0hr";
   441 by (auto_tac (claset() addIs [hypreal_add_minus_left],simpset()));
   442 by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
   443 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
   444 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   445 qed "hypreal_minus_left_ex1";
   446 
   447 Goal "x + y = 0hr ==> x = -y";
   448 by (cut_inst_tac [("z","y")] hypreal_add_minus_left 1);
   449 by (res_inst_tac [("x1","y")] (hypreal_minus_left_ex1 RS ex1E) 1);
   450 by (Blast_tac 1);
   451 qed "hypreal_add_minus_eq_minus";
   452 
   453 Goal "? y::hypreal. x = -y";
   454 by (cut_inst_tac [("x","x")] hypreal_minus_ex 1);
   455 by (etac exE 1 THEN dtac hypreal_add_minus_eq_minus 1);
   456 by (Fast_tac 1);
   457 qed "hypreal_as_add_inverse_ex";
   458 
   459 Goal "-(x + (y::hypreal)) = -x + -y";
   460 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   461 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   462 by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
   463     hypreal_add,real_minus_add_distrib]));
   464 qed "hypreal_minus_add_distrib";
   465 
   466 Goal "-(y + -(x::hypreal)) = x + -y";
   467 by (simp_tac (simpset() addsimps [hypreal_minus_add_distrib,
   468     hypreal_add_commute]) 1);
   469 qed "hypreal_minus_distrib1";
   470 
   471 Goal "(x + - (y::hypreal)) + (y + - z) = x + -z";
   472 by (res_inst_tac [("w1","y")] (hypreal_add_commute RS subst) 1);
   473 by (simp_tac (simpset() addsimps [hypreal_add_left_commute,
   474     hypreal_add_assoc]) 1);
   475 by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   476 qed "hypreal_add_minus_cancel1";
   477 
   478 Goal "((x::hypreal) + y = x + z) = (y = z)";
   479 by (Step_tac 1);
   480 by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1);
   481 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   482 qed "hypreal_add_left_cancel";
   483 
   484 Goal "z + (x + (y + -z)) = x + (y::hypreal)";
   485 by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
   486 qed "hypreal_add_minus_cancel2";
   487 Addsimps [hypreal_add_minus_cancel2];
   488 
   489 Goal "y + -(x + y) = -(x::hypreal)";
   490 by (full_simp_tac (simpset() addsimps [hypreal_minus_add_distrib]) 1);
   491 by (rtac (hypreal_add_left_commute RS subst) 1);
   492 by (Full_simp_tac 1);
   493 qed "hypreal_add_minus_cancel";
   494 Addsimps [hypreal_add_minus_cancel];
   495 
   496 Goal "y + -(y + x) = -(x::hypreal)";
   497 by (simp_tac (simpset() addsimps [hypreal_minus_add_distrib,
   498               hypreal_add_assoc RS sym]) 1);
   499 qed "hypreal_add_minus_cancelc";
   500 Addsimps [hypreal_add_minus_cancelc];
   501 
   502 Goal "(z + -x) + (y + -z) = (y + -(x::hypreal))";
   503 by (full_simp_tac (simpset() addsimps [hypreal_minus_add_distrib
   504     RS sym, hypreal_add_left_cancel] @ hypreal_add_ac) 1); 
   505 qed "hypreal_add_minus_cancel3";
   506 Addsimps [hypreal_add_minus_cancel3];
   507 
   508 Goal "(y + (x::hypreal)= z + x) = (y = z)";
   509 by (simp_tac (simpset() addsimps [hypreal_add_commute,
   510     hypreal_add_left_cancel]) 1);
   511 qed "hypreal_add_right_cancel";
   512 
   513 Goal "z + (y + -z) = (y::hypreal)";
   514 by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
   515 qed "hypreal_add_minus_cancel4";
   516 Addsimps [hypreal_add_minus_cancel4];
   517 
   518 Goal "z + (w + (x + (-z + y))) = w + x + (y::hypreal)";
   519 by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
   520 qed "hypreal_add_minus_cancel5";
   521 Addsimps [hypreal_add_minus_cancel5];
   522 
   523 
   524 (**** hyperreal multiplication: hypreal_mult  ****)
   525 
   526 Goalw [congruent2_def]
   527     "congruent2 hyprel (%X Y. hyprel^^{%n. X n * Y n})";
   528 by Safe_tac;
   529 by (ALLGOALS(Ultra_tac));
   530 qed "hypreal_mult_congruent2";
   531 
   532 (*Resolve th against the corresponding facts for hypreal_mult*)
   533 val hypreal_mult_ize = RSLIST [equiv_hyprel, hypreal_mult_congruent2];
   534 
   535 Goalw [hypreal_mult_def]
   536   "Abs_hypreal(hyprel^^{%n. X n}) * Abs_hypreal(hyprel^^{%n. Y n}) = \
   537 \  Abs_hypreal(hyprel^^{%n. X n * Y n})";
   538 by (asm_simp_tac
   539     (simpset() addsimps [hypreal_mult_ize UN_equiv_class2]) 1);
   540 qed "hypreal_mult";
   541 
   542 Goal "(z::hypreal) * w = w * z";
   543 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   544 by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
   545 by (asm_simp_tac (simpset() addsimps ([hypreal_mult] @ real_mult_ac)) 1);
   546 qed "hypreal_mult_commute";
   547 
   548 Goal "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)";
   549 by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
   550 by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
   551 by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
   552 by (asm_simp_tac (simpset() addsimps [hypreal_mult,real_mult_assoc]) 1);
   553 qed "hypreal_mult_assoc";
   554 
   555 qed_goal "hypreal_mult_left_commute" thy
   556     "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)"
   557  (fn _ => [rtac (hypreal_mult_commute RS trans) 1, rtac (hypreal_mult_assoc RS trans) 1,
   558            rtac (hypreal_mult_commute RS arg_cong) 1]);
   559 
   560 (* hypreal multiplication is an AC operator *)
   561 val hypreal_mult_ac = [hypreal_mult_assoc, hypreal_mult_commute, 
   562                        hypreal_mult_left_commute];
   563 
   564 Goalw [hypreal_one_def] "1hr * z = z";
   565 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   566 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult]) 1);
   567 qed "hypreal_mult_1";
   568 
   569 Goal "z * 1hr = z";
   570 by (simp_tac (simpset() addsimps [hypreal_mult_commute,
   571     hypreal_mult_1]) 1);
   572 qed "hypreal_mult_1_right";
   573 
   574 Goalw [hypreal_zero_def] "0hr * z = 0hr";
   575 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   576 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult,real_mult_0]) 1);
   577 qed "hypreal_mult_0";
   578 
   579 Goal "z * 0hr = 0hr";
   580 by (simp_tac (simpset() addsimps [hypreal_mult_commute,
   581     hypreal_mult_0]) 1);
   582 qed "hypreal_mult_0_right";
   583 
   584 Addsimps [hypreal_mult_0,hypreal_mult_0_right];
   585 
   586 Goal "-(x * y) = -x * (y::hypreal)";
   587 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   588 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   589 by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
   590     hypreal_mult,real_minus_mult_eq1] 
   591       @ real_mult_ac @ real_add_ac));
   592 qed "hypreal_minus_mult_eq1";
   593 
   594 Goal "-(x * y) = (x::hypreal) * -y";
   595 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   596 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   597 by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
   598    hypreal_mult,real_minus_mult_eq2] 
   599     @ real_mult_ac @ real_add_ac));
   600 qed "hypreal_minus_mult_eq2";
   601 
   602 Goal "-x*-y = x*(y::hypreal)";
   603 by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym,
   604     hypreal_minus_mult_eq1 RS sym]) 1);
   605 qed "hypreal_minus_mult_cancel";
   606 
   607 Addsimps [hypreal_minus_mult_cancel];
   608 
   609 Goal "-x*y = (x::hypreal)*-y";
   610 by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym,
   611     hypreal_minus_mult_eq1 RS sym]) 1);
   612 qed "hypreal_minus_mult_commute";
   613 
   614 
   615 (*-----------------------------------------------------------------------------
   616     A few more theorems
   617  ----------------------------------------------------------------------------*)
   618 Goal "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
   619 by (asm_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   620 qed "hypreal_add_assoc_cong";
   621 
   622 Goal "(z::hypreal) + (v + w) = v + (z + w)";
   623 by (REPEAT (ares_tac [hypreal_add_commute RS hypreal_add_assoc_cong] 1));
   624 qed "hypreal_add_assoc_swap";
   625 
   626 Goal "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)";
   627 by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
   628 by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
   629 by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
   630 by (asm_simp_tac (simpset() addsimps [hypreal_mult,hypreal_add,
   631      real_add_mult_distrib]) 1);
   632 qed "hypreal_add_mult_distrib";
   633 
   634 val hypreal_mult_commute'= read_instantiate [("z","w")] hypreal_mult_commute;
   635 
   636 Goal "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)";
   637 by (simp_tac (simpset() addsimps [hypreal_mult_commute',hypreal_add_mult_distrib]) 1);
   638 qed "hypreal_add_mult_distrib2";
   639 
   640 val hypreal_mult_simps = [hypreal_mult_1, hypreal_mult_1_right];
   641 Addsimps hypreal_mult_simps;
   642 
   643 (*** one and zero are distinct ***)
   644 Goalw [hypreal_zero_def,hypreal_one_def] "0hr ~= 1hr";
   645 by (auto_tac (claset(),simpset() addsimps [real_zero_not_eq_one]));
   646 qed "hypreal_zero_not_eq_one";
   647 
   648 (*** existence of inverse ***)
   649 Goalw [hypreal_one_def,hypreal_zero_def] 
   650           "x ~= 0hr ==> x*hrinv(x) = 1hr";
   651 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   652 by (rotate_tac 1 1);
   653 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
   654     hypreal_mult] setloop (split_tac [expand_if])) 1);
   655 by (dtac FreeUltrafilterNat_Compl_mem 1);
   656 by (blast_tac (claset() addSIs [real_mult_inv_right,
   657     FreeUltrafilterNat_subset]) 1);
   658 qed "hypreal_mult_hrinv";
   659 
   660 Goal "x ~= 0hr ==> hrinv(x)*x = 1hr";
   661 by (asm_simp_tac (simpset() addsimps [hypreal_mult_hrinv,
   662     hypreal_mult_commute]) 1);
   663 qed "hypreal_mult_hrinv_left";
   664 
   665 Goal "x ~= 0hr ==> ? y. (x::hypreal) * y = 1hr";
   666 by (fast_tac (claset() addDs [hypreal_mult_hrinv]) 1);
   667 qed "hypreal_hrinv_ex";
   668 
   669 Goal "x ~= 0hr ==> ? y. y * (x::hypreal) = 1hr";
   670 by (fast_tac (claset() addDs [hypreal_mult_hrinv_left]) 1);
   671 qed "hypreal_hrinv_left_ex";
   672 
   673 Goal "x ~= 0hr ==> ?! y. (x::hypreal) * y = 1hr";
   674 by (auto_tac (claset() addIs [hypreal_mult_hrinv],simpset()));
   675 by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
   676 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
   677 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
   678 qed "hypreal_hrinv_ex1";
   679 
   680 Goal "x ~= 0hr ==> ?! y. y * (x::hypreal) = 1hr";
   681 by (auto_tac (claset() addIs [hypreal_mult_hrinv_left],simpset()));
   682 by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
   683 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
   684 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
   685 qed "hypreal_hrinv_left_ex1";
   686 
   687 Goal "[| y~= 0hr; x * y = 1hr |]  ==> x = hrinv y";
   688 by (forw_inst_tac [("x","y")] hypreal_mult_hrinv_left 1);
   689 by (res_inst_tac [("x1","y")] (hypreal_hrinv_left_ex1 RS ex1E) 1);
   690 by (assume_tac 1);
   691 by (Blast_tac 1);
   692 qed "hypreal_mult_inv_hrinv";
   693 
   694 Goal "x ~= 0hr ==> ? y. x = hrinv y";
   695 by (forw_inst_tac [("x","x")] hypreal_hrinv_left_ex 1);
   696 by (etac exE 1 THEN 
   697     forw_inst_tac [("x","y")] hypreal_mult_inv_hrinv 1);
   698 by (res_inst_tac [("x","y")] exI 2);
   699 by Auto_tac;
   700 qed "hypreal_as_inverse_ex";
   701 
   702 Goal "(c::hypreal) ~= 0hr ==> (c*a=c*b) = (a=b)";
   703 by Auto_tac;
   704 by (dres_inst_tac [("f","%x. x*hrinv c")] arg_cong 1);
   705 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_hrinv] @ hypreal_mult_ac)  1);
   706 qed "hypreal_mult_left_cancel";
   707     
   708 Goal "(c::hypreal) ~= 0hr ==> (a*c=b*c) = (a=b)";
   709 by (Step_tac 1);
   710 by (dres_inst_tac [("f","%x. x*hrinv c")] arg_cong 1);
   711 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_hrinv] @ hypreal_mult_ac)  1);
   712 qed "hypreal_mult_right_cancel";
   713 
   714 Goalw [hypreal_zero_def] "x ~= 0hr ==> hrinv(x) ~= 0hr";
   715 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   716 by (rotate_tac 1 1);
   717 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
   718     hypreal_mult] setloop (split_tac [expand_if])) 1);
   719 by (dtac FreeUltrafilterNat_Compl_mem 1 THEN Clarify_tac 1);
   720 by (ultra_tac (claset() addIs [ccontr] addDs 
   721     [rinv_not_zero],simpset()) 1);
   722 qed "hrinv_not_zero";
   723 
   724 Addsimps [hypreal_mult_hrinv,hypreal_mult_hrinv_left];
   725 
   726 Goal "[| x ~= 0hr; y ~= 0hr |] ==> x * y ~= 0hr";
   727 by (Step_tac 1);
   728 by (dres_inst_tac [("f","%z. hrinv x*z")] arg_cong 1);
   729 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
   730 qed "hypreal_mult_not_0";
   731 
   732 bind_thm ("hypreal_mult_not_0E",hypreal_mult_not_0 RS notE);
   733 
   734 Goal "x ~= 0hr ==> x * x ~= 0hr";
   735 by (blast_tac (claset() addDs [hypreal_mult_not_0]) 1);
   736 qed "hypreal_mult_self_not_zero";
   737 
   738 Goal "[| x ~= 0hr; y ~= 0hr |] ==> hrinv(x*y) = hrinv(x)*hrinv(y)";
   739 by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
   740 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,
   741     hypreal_mult_not_0]));
   742 by (res_inst_tac [("c1","y")] (hypreal_mult_right_cancel RS iffD1) 1);
   743 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_not_0] @ hypreal_mult_ac));
   744 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,hypreal_mult_not_0]));
   745 qed "hrinv_mult_eq";
   746 
   747 Goal "x ~= 0hr ==> hrinv(-x) = -hrinv(x)";
   748 by (res_inst_tac [("c1","-x")] (hypreal_mult_right_cancel RS iffD1) 1);
   749 by Auto_tac;
   750 qed "hypreal_minus_hrinv";
   751 
   752 Goal "[| x ~= 0hr; y ~= 0hr |] \
   753 \     ==> hrinv(x*y) = hrinv(x)*hrinv(y)";
   754 by (forw_inst_tac [("y","y")] hypreal_mult_not_0 1 THEN assume_tac 1);
   755 by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
   756 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym]));
   757 by (res_inst_tac [("c1","y")] (hypreal_mult_left_cancel RS iffD1) 1);
   758 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_left_commute]));
   759 by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
   760 qed "hypreal_hrinv_distrib";
   761 
   762 (*------------------------------------------------------------------
   763                    Theorems for ordering 
   764  ------------------------------------------------------------------*)
   765 
   766 (* prove introduction and elimination rules for hypreal_less *)
   767 
   768 Goalw [hypreal_less_def]
   769  "P < (Q::hypreal) = (EX X Y. X : Rep_hypreal(P) & \
   770 \                             Y : Rep_hypreal(Q) & \
   771 \                             {n. X n < Y n} : FreeUltrafilterNat)";
   772 by (Fast_tac 1);
   773 qed "hypreal_less_iff";
   774 
   775 Goalw [hypreal_less_def]
   776  "[| {n. X n < Y n} : FreeUltrafilterNat; \
   777 \         X : Rep_hypreal(P); \
   778 \         Y : Rep_hypreal(Q) |] ==> P < (Q::hypreal)";
   779 by (Fast_tac 1);
   780 qed "hypreal_lessI";
   781 
   782 
   783 Goalw [hypreal_less_def]
   784      "!! R1. [| R1 < (R2::hypreal); \
   785 \         !!X Y. {n. X n < Y n} : FreeUltrafilterNat ==> P; \
   786 \         !!X. X : Rep_hypreal(R1) ==> P; \ 
   787 \         !!Y. Y : Rep_hypreal(R2) ==> P |] \
   788 \     ==> P";
   789 by Auto_tac;
   790 qed "hypreal_lessE";
   791 
   792 Goalw [hypreal_less_def]
   793  "R1 < (R2::hypreal) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \
   794 \                                  X : Rep_hypreal(R1) & \
   795 \                                  Y : Rep_hypreal(R2))";
   796 by (Fast_tac 1);
   797 qed "hypreal_lessD";
   798 
   799 Goal "~ (R::hypreal) < R";
   800 by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
   801 by (auto_tac (claset(),simpset() addsimps [hypreal_less_def]));
   802 by (Ultra_tac 1);
   803 qed "hypreal_less_not_refl";
   804 
   805 (*** y < y ==> P ***)
   806 bind_thm("hypreal_less_irrefl",hypreal_less_not_refl RS notE);
   807 
   808 Goal "!!(x::hypreal). x < y ==> x ~= y";
   809 by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
   810 qed "hypreal_not_refl2";
   811 
   812 Goal "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
   813 by (res_inst_tac [("z","R1")] eq_Abs_hypreal 1);
   814 by (res_inst_tac [("z","R2")] eq_Abs_hypreal 1);
   815 by (res_inst_tac [("z","R3")] eq_Abs_hypreal 1);
   816 by (auto_tac (claset() addSIs [exI],simpset() 
   817      addsimps [hypreal_less_def]));
   818 by (ultra_tac (claset() addIs [real_less_trans],simpset()) 1);
   819 qed "hypreal_less_trans";
   820 
   821 Goal "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P";
   822 by (dtac hypreal_less_trans 1 THEN assume_tac 1);
   823 by (asm_full_simp_tac (simpset() addsimps 
   824     [hypreal_less_not_refl]) 1);
   825 qed "hypreal_less_asym";
   826 
   827 (*--------------------------------------------------------
   828   TODO: The following theorem should have been proved 
   829   first and then used througout the proofs as it probably 
   830   makes many of them more straightforward. 
   831  -------------------------------------------------------*)
   832 Goalw [hypreal_less_def]
   833       "(Abs_hypreal(hyprel^^{%n. X n}) < \
   834 \           Abs_hypreal(hyprel^^{%n. Y n})) = \
   835 \      ({n. X n < Y n} : FreeUltrafilterNat)";
   836 by (auto_tac (claset() addSIs [lemma_hyprel_refl],simpset()));
   837 by (Ultra_tac 1);
   838 qed "hypreal_less";
   839 
   840 (*---------------------------------------------------------------------------------
   841              Hyperreals as a linearly ordered field
   842  ---------------------------------------------------------------------------------*)
   843 (*** sum order ***)
   844 
   845 Goalw [hypreal_zero_def] 
   846       "[| 0hr < x; 0hr < y |] ==> 0hr < x + y";
   847 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   848 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   849 by (auto_tac (claset(),simpset() addsimps
   850     [hypreal_less_def,hypreal_add]));
   851 by (auto_tac (claset() addSIs [exI],simpset() addsimps
   852     [hypreal_less_def,hypreal_add]));
   853 by (ultra_tac (claset() addIs [real_add_order],simpset()) 1);
   854 qed "hypreal_add_order";
   855 
   856 (*** mult order ***)
   857 
   858 Goalw [hypreal_zero_def] 
   859           "[| 0hr < x; 0hr < y |] ==> 0hr < x * y";
   860 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   861 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   862 by (auto_tac (claset() addSIs [exI],simpset() addsimps
   863     [hypreal_less_def,hypreal_mult]));
   864 by (ultra_tac (claset() addIs [real_mult_order],simpset()) 1);
   865 qed "hypreal_mult_order";
   866 
   867 (*---------------------------------------------------------------------------------
   868                          Trichotomy of the hyperreals
   869   --------------------------------------------------------------------------------*)
   870 
   871 Goalw [hyprel_def] "? x. x: hyprel ^^ {%n. 0r}";
   872 by (res_inst_tac [("x","%n. 0r")] exI 1);
   873 by (Step_tac 1);
   874 by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset()));
   875 qed "lemma_hyprel_0r_mem";
   876 
   877 Goalw [hypreal_zero_def]"0hr <  x | x = 0hr | x < 0hr";
   878 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   879 by (auto_tac (claset(),simpset() addsimps [hypreal_less_def]));
   880 by (cut_facts_tac [lemma_hyprel_0r_mem] 1 THEN etac exE 1);
   881 by (dres_inst_tac [("x","xa")] spec 1);
   882 by (dres_inst_tac [("x","x")] spec 1);
   883 by (cut_inst_tac [("x","x")] lemma_hyprel_refl 1);
   884 by Auto_tac;
   885 by (dres_inst_tac [("x","x")] spec 1);
   886 by (dres_inst_tac [("x","xa")] spec 1);
   887 by Auto_tac;
   888 by (Ultra_tac 1);
   889 by (auto_tac (claset() addIs [real_linear_less2],simpset()));
   890 qed "hypreal_trichotomy";
   891 
   892 val prems = Goal "[| 0hr < x ==> P; \
   893 \                 x = 0hr ==> P; \
   894 \                 x < 0hr ==> P |] ==> P";
   895 by (cut_inst_tac [("x","x")] hypreal_trichotomy 1);
   896 by (REPEAT (eresolve_tac (disjE::prems) 1));
   897 qed "hypreal_trichotomyE";
   898 
   899 (*----------------------------------------------------------------------------
   900             More properties of <
   901  ----------------------------------------------------------------------------*)
   902 Goal "!!(A::hypreal). A < B ==> A + C < B + C";
   903 by (res_inst_tac [("z","A")] eq_Abs_hypreal 1);
   904 by (res_inst_tac [("z","B")] eq_Abs_hypreal 1);
   905 by (res_inst_tac [("z","C")] eq_Abs_hypreal 1);
   906 by (auto_tac (claset() addSIs [exI],simpset() addsimps
   907     [hypreal_less_def,hypreal_add]));
   908 by (Ultra_tac 1);
   909 qed "hypreal_add_less_mono1";
   910 
   911 Goal "!!(A::hypreal). A < B ==> C + A < C + B";
   912 by (auto_tac (claset() addIs [hypreal_add_less_mono1],
   913     simpset() addsimps [hypreal_add_commute]));
   914 qed "hypreal_add_less_mono2";
   915 
   916 Goal "((x::hypreal) < y) = (0hr < y + -x)";
   917 by (Step_tac 1);
   918 by (dres_inst_tac [("C","-x")] hypreal_add_less_mono1 1);
   919 by (dres_inst_tac [("C","x")] hypreal_add_less_mono1 2);
   920 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   921 qed "hypreal_less_minus_iff"; 
   922 
   923 Goal "((x::hypreal) < y) = (x + -y< 0hr)";
   924 by (Step_tac 1);
   925 by (dres_inst_tac [("C","-y")] hypreal_add_less_mono1 1);
   926 by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 2);
   927 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   928 qed "hypreal_less_minus_iff2";
   929 
   930 Goal  "!!(y1 :: hypreal). [| z1 < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2";
   931 by (dtac (hypreal_less_minus_iff RS iffD1) 1);
   932 by (dtac (hypreal_less_minus_iff RS iffD1) 1);
   933 by (dtac hypreal_add_order 1 THEN assume_tac 1);
   934 by (thin_tac "0hr < y2 + - z2" 1);
   935 by (dres_inst_tac [("C","z1 + z2")] hypreal_add_less_mono1 1);
   936 by (auto_tac (claset(),simpset() addsimps 
   937     [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac));
   938 qed "hypreal_add_less_mono";
   939 
   940 Goal "((x::hypreal) = y) = (0hr = x + - y)";
   941 by Auto_tac;
   942 by (res_inst_tac [("x1","-y")] (hypreal_add_right_cancel RS iffD1) 1);
   943 by Auto_tac;
   944 qed "hypreal_eq_minus_iff"; 
   945 
   946 Goal "((x::hypreal) = y) = (0hr = y + - x)";
   947 by Auto_tac;
   948 by (res_inst_tac [("x1","-x")] (hypreal_add_right_cancel RS iffD1) 1);
   949 by Auto_tac;
   950 qed "hypreal_eq_minus_iff2"; 
   951 
   952 Goal "(x = y + z) = (x + -z = (y::hypreal))";
   953 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   954 qed "hypreal_eq_minus_iff3";
   955 
   956 Goal "(x = z + y) = (x + -z = (y::hypreal))";
   957 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
   958 qed "hypreal_eq_minus_iff4";
   959 
   960 Goal "(x ~= a) = (x + -a ~= 0hr)";
   961 by (auto_tac (claset() addDs [sym RS 
   962     (hypreal_eq_minus_iff RS iffD2)],simpset())); 
   963 qed "hypreal_not_eq_minus_iff";
   964 
   965 (*** linearity ***)
   966 Goal "(x::hypreal) < y | x = y | y < x";
   967 by (stac hypreal_eq_minus_iff2 1);
   968 by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1);
   969 by (res_inst_tac [("x1","y")] (hypreal_less_minus_iff2 RS ssubst) 1);
   970 by (rtac hypreal_trichotomyE 1);
   971 by Auto_tac;
   972 qed "hypreal_linear";
   973 
   974 Goal "!!(x::hypreal). [| x < y ==> P;  x = y ==> P; \
   975 \          y < x ==> P |] ==> P";
   976 by (cut_inst_tac [("x","x"),("y","y")] hypreal_linear 1);
   977 by Auto_tac;
   978 qed "hypreal_linear_less2";
   979 
   980 (*------------------------------------------------------------------------------
   981                             Properties of <=
   982  ------------------------------------------------------------------------------*)
   983 (*------ hypreal le iff reals le a.e ------*)
   984 
   985 Goalw [hypreal_le_def,real_le_def]
   986       "(Abs_hypreal(hyprel^^{%n. X n}) <= \
   987 \           Abs_hypreal(hyprel^^{%n. Y n})) = \
   988 \      ({n. X n <= Y n} : FreeUltrafilterNat)";
   989 by (auto_tac (claset(),simpset() addsimps [hypreal_less]));
   990 by (ALLGOALS(Ultra_tac));
   991 qed "hypreal_le";
   992 
   993 (*---------------------------------------------------------*)
   994 (*---------------------------------------------------------*)
   995 Goalw [hypreal_le_def] 
   996      "~(w < z) ==> z <= (w::hypreal)";
   997 by (assume_tac 1);
   998 qed "hypreal_leI";
   999 
  1000 Goalw [hypreal_le_def] 
  1001       "z<=w ==> ~(w<(z::hypreal))";
  1002 by (assume_tac 1);
  1003 qed "hypreal_leD";
  1004 
  1005 val hypreal_leE = make_elim hypreal_leD;
  1006 
  1007 Goal "(~(w < z)) = (z <= (w::hypreal))";
  1008 by (fast_tac (claset() addSIs [hypreal_leI,hypreal_leD]) 1);
  1009 qed "hypreal_less_le_iff";
  1010 
  1011 Goalw [hypreal_le_def] "~ z <= w ==> w<(z::hypreal)";
  1012 by (Fast_tac 1);
  1013 qed "not_hypreal_leE";
  1014 
  1015 Goalw [hypreal_le_def] "z < w ==> z <= (w::hypreal)";
  1016 by (fast_tac (claset() addEs [hypreal_less_asym]) 1);
  1017 qed "hypreal_less_imp_le";
  1018 
  1019 Goalw [hypreal_le_def] "!!(x::hypreal). x <= y ==> x < y | x = y";
  1020 by (cut_facts_tac [hypreal_linear] 1);
  1021 by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1);
  1022 qed "hypreal_le_imp_less_or_eq";
  1023 
  1024 Goalw [hypreal_le_def] "z<w | z=w ==> z <=(w::hypreal)";
  1025 by (cut_facts_tac [hypreal_linear] 1);
  1026 by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1);
  1027 qed "hypreal_less_or_eq_imp_le";
  1028 
  1029 Goal "(x <= (y::hypreal)) = (x < y | x=y)";
  1030 by (REPEAT(ares_tac [iffI, hypreal_less_or_eq_imp_le, hypreal_le_imp_less_or_eq] 1));
  1031 qed "hypreal_le_eq_less_or_eq";
  1032 
  1033 Goal "w <= (w::hypreal)";
  1034 by (simp_tac (simpset() addsimps [hypreal_le_eq_less_or_eq]) 1);
  1035 qed "hypreal_le_refl";
  1036 Addsimps [hypreal_le_refl];
  1037 
  1038 Goal "[| i <= j; j < k |] ==> i < (k::hypreal)";
  1039 by (dtac hypreal_le_imp_less_or_eq 1);
  1040 by (fast_tac (claset() addIs [hypreal_less_trans]) 1);
  1041 qed "hypreal_le_less_trans";
  1042 
  1043 Goal "!! (i::hypreal). [| i < j; j <= k |] ==> i < k";
  1044 by (dtac hypreal_le_imp_less_or_eq 1);
  1045 by (fast_tac (claset() addIs [hypreal_less_trans]) 1);
  1046 qed "hypreal_less_le_trans";
  1047 
  1048 Goal "[| i <= j; j <= k |] ==> i <= (k::hypreal)";
  1049 by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq,
  1050             rtac hypreal_less_or_eq_imp_le, fast_tac (claset() addIs [hypreal_less_trans])]);
  1051 qed "hypreal_le_trans";
  1052 
  1053 Goal "[| z <= w; w <= z |] ==> z = (w::hypreal)";
  1054 by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq,
  1055             fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym])]);
  1056 qed "hypreal_le_anti_sym";
  1057 
  1058 Goal "[| 0hr < x; 0hr <= y |] ==> 0hr < x + y";
  1059 by (auto_tac (claset() addDs [sym,hypreal_le_imp_less_or_eq]
  1060               addIs [hypreal_add_order],simpset()));
  1061 qed "hypreal_add_order_le";            
  1062 
  1063 (*------------------------------------------------------------------------
  1064  ------------------------------------------------------------------------*)
  1065 
  1066 Goal "[| ~ y < x; y ~= x |] ==> x < (y::hypreal)";
  1067 by (rtac not_hypreal_leE 1);
  1068 by (fast_tac (claset() addDs [hypreal_le_imp_less_or_eq]) 1);
  1069 qed "not_less_not_eq_hypreal_less";
  1070 
  1071 Goal "(0hr < -R) = (R < 0hr)";
  1072 by (Step_tac 1);
  1073 by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1);
  1074 by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2);
  1075 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
  1076 qed "hypreal_minus_zero_less_iff";
  1077 
  1078 Goal "(-R < 0hr) = (0hr < R)";
  1079 by (Step_tac 1);
  1080 by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1);
  1081 by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2);
  1082 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
  1083 qed "hypreal_minus_zero_less_iff2";
  1084 
  1085 Goal "((x::hypreal) < y) = (-y < -x)";
  1086 by (stac hypreal_less_minus_iff 1);
  1087 by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1);
  1088 by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
  1089 qed "hypreal_less_swap_iff";
  1090 
  1091 Goal "(0hr < x) = (-x < x)";
  1092 by (Step_tac 1);
  1093 by (rtac ccontr 2 THEN forward_tac 
  1094     [hypreal_leI RS hypreal_le_imp_less_or_eq] 2);
  1095 by (Step_tac 2);
  1096 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 2);
  1097 by (dres_inst_tac [("R2.0","-x")] hypreal_less_trans 2);
  1098 by (Auto_tac );
  1099 by (ftac hypreal_add_order 1 THEN assume_tac 1);
  1100 by (dres_inst_tac [("C","-x"),("B","x + x")] hypreal_add_less_mono1 1);
  1101 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
  1102 qed "hypreal_gt_zero_iff";
  1103 
  1104 Goal "(x < 0hr) = (x < -x)";
  1105 by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
  1106 by (stac hypreal_gt_zero_iff 1);
  1107 by (Full_simp_tac 1);
  1108 qed "hypreal_lt_zero_iff";
  1109 
  1110 Goalw [hypreal_le_def] "(0hr <= x) = (-x <= x)";
  1111 by (auto_tac (claset(),simpset() addsimps [hypreal_lt_zero_iff RS sym]));
  1112 qed "hypreal_ge_zero_iff";
  1113 
  1114 Goalw [hypreal_le_def] "(x <= 0hr) = (x <= -x)";
  1115 by (auto_tac (claset(),simpset() addsimps [hypreal_gt_zero_iff RS sym]));
  1116 qed "hypreal_le_zero_iff";
  1117 
  1118 Goal "[| x < 0hr; y < 0hr |] ==> 0hr < x * y";
  1119 by (REPEAT(dtac (hypreal_minus_zero_less_iff RS iffD2) 1));
  1120 by (dtac hypreal_mult_order 1 THEN assume_tac 1);
  1121 by (Asm_full_simp_tac 1);
  1122 qed "hypreal_mult_less_zero1";
  1123 
  1124 Goal "[| 0hr <= x; 0hr <= y |] ==> 0hr <= x * y";
  1125 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
  1126 by (auto_tac (claset() addIs [hypreal_mult_order,
  1127     hypreal_less_imp_le],simpset()));
  1128 qed "hypreal_le_mult_order";
  1129 
  1130 Goal "[| x <= 0hr; y <= 0hr |] ==> 0hr <= x * y";
  1131 by (rtac hypreal_less_or_eq_imp_le 1);
  1132 by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1);
  1133 by Auto_tac;
  1134 by (dtac hypreal_le_imp_less_or_eq 1);
  1135 by (auto_tac (claset() addDs [hypreal_mult_less_zero1],simpset()));
  1136 qed "real_mult_le_zero1";
  1137 
  1138 Goal "[| 0hr <= x; y < 0hr |] ==> x * y <= 0hr";
  1139 by (rtac hypreal_less_or_eq_imp_le 1);
  1140 by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1);
  1141 by Auto_tac;
  1142 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
  1143 by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
  1144 by (blast_tac (claset() addDs [hypreal_mult_order] 
  1145     addIs [hypreal_minus_mult_eq2 RS ssubst]) 1);
  1146 qed "hypreal_mult_le_zero";
  1147 
  1148 Goal "[| 0hr < x; y < 0hr |] ==> x*y < 0hr";
  1149 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
  1150 by (dtac hypreal_mult_order 1 THEN assume_tac 1);
  1151 by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
  1152 by (asm_full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2]) 1);
  1153 qed "hypreal_mult_less_zero";
  1154 
  1155 Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0hr < 1hr";
  1156 by (res_inst_tac [("x","%n. 0r")] exI 1);
  1157 by (res_inst_tac [("x","%n. 1r")] exI 1);
  1158 by (auto_tac (claset(),simpset() addsimps [real_zero_less_one,
  1159     FreeUltrafilterNat_Nat_set]));
  1160 qed "hypreal_zero_less_one";
  1161 
  1162 Goal "[| 0hr <= x; 0hr <= y |] ==> 0hr <= x + y";
  1163 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
  1164 by (auto_tac (claset() addIs [hypreal_add_order,
  1165     hypreal_less_imp_le],simpset()));
  1166 qed "hypreal_le_add_order";
  1167 
  1168 Goal "!!(q1::hypreal). q1 <= q2  ==> x + q1 <= x + q2";
  1169 by (dtac hypreal_le_imp_less_or_eq 1);
  1170 by (Step_tac 1);
  1171 by (auto_tac (claset() addSIs [hypreal_le_refl,
  1172     hypreal_less_imp_le,hypreal_add_less_mono1],
  1173     simpset() addsimps [hypreal_add_commute]));
  1174 qed "hypreal_add_left_le_mono1";
  1175 
  1176 Goal "!!(q1::hypreal). q1 <= q2  ==> q1 + x <= q2 + x";
  1177 by (auto_tac (claset() addDs [hypreal_add_left_le_mono1],
  1178     simpset() addsimps [hypreal_add_commute]));
  1179 qed "hypreal_add_le_mono1";
  1180 
  1181 Goal "!!k l::hypreal. [|i<=j;  k<=l |] ==> i + k <= j + l";
  1182 by (etac (hypreal_add_le_mono1 RS hypreal_le_trans) 1);
  1183 by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
  1184 (*j moves to the end because it is free while k, l are bound*)
  1185 by (etac hypreal_add_le_mono1 1);
  1186 qed "hypreal_add_le_mono";
  1187 
  1188 Goal "!!k l::hypreal. [|i<j;  k<=l |] ==> i + k < j + l";
  1189 by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] 
  1190     addIs [hypreal_add_less_mono1,hypreal_add_less_mono],simpset()));
  1191 qed "hypreal_add_less_le_mono";
  1192 
  1193 Goal "!!k l::hypreal. [|i<=j;  k<l |] ==> i + k < j + l";
  1194 by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] 
  1195     addIs [hypreal_add_less_mono2,hypreal_add_less_mono],simpset()));
  1196 qed "hypreal_add_le_less_mono";
  1197 
  1198 Goal "(0hr*x<r)=(0hr<r)";
  1199 by (Simp_tac 1);
  1200 qed "hypreal_mult_0_less";
  1201 
  1202 Goal "[| 0hr < z; x < y |] ==> x*z < y*z";       
  1203 by (rotate_tac 1 1);
  1204 by (dtac (hypreal_less_minus_iff RS iffD1) 1);
  1205 by (rtac (hypreal_less_minus_iff RS iffD2) 1);
  1206 by (dtac hypreal_mult_order 1 THEN assume_tac 1);
  1207 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2,
  1208     hypreal_minus_mult_eq2 RS sym, hypreal_mult_commute ]) 1);
  1209 qed "hypreal_mult_less_mono1";
  1210 
  1211 Goal "[| 0hr<z; x<y |] ==> z*x<z*y";       
  1212 by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,hypreal_mult_less_mono1]) 1);
  1213 qed "hypreal_mult_less_mono2";
  1214 
  1215 Goal "[| 0hr<=z; x<y |] ==> x*z<=y*z";
  1216 by (EVERY1 [rtac hypreal_less_or_eq_imp_le, dtac hypreal_le_imp_less_or_eq]);
  1217 by (auto_tac (claset() addIs [hypreal_mult_less_mono1],simpset()));
  1218 qed "hypreal_mult_le_less_mono1";
  1219 
  1220 Goal "[| 0hr<=z; x<y |] ==> z*x<=z*y";
  1221 by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,
  1222 				      hypreal_mult_le_less_mono1]) 1);
  1223 qed "hypreal_mult_le_less_mono2";
  1224 
  1225 Goal "[| 0hr<=z; x<=y |] ==> z*x<=z*y";
  1226 by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1);
  1227 by (auto_tac (claset() addIs [hypreal_mult_le_less_mono2,hypreal_le_refl],simpset()));
  1228 qed "hypreal_mult_le_le_mono1";
  1229 
  1230 val prem1::prem2::prem3::rest = goal thy
  1231      "[| 0hr<y; x<r; y*r<t*s |] ==> y*x<t*s";
  1232 by (rtac ([([prem1,prem2] MRS hypreal_mult_less_mono2),prem3] MRS hypreal_less_trans) 1);
  1233 qed "hypreal_mult_less_trans";
  1234 
  1235 Goal "[| 0hr<=y; x<r; y*r<t*s; 0hr<t*s|] ==> y*x<t*s";
  1236 by (dtac hypreal_le_imp_less_or_eq 1);
  1237 by (fast_tac (HOL_cs addEs [(hypreal_mult_0_less RS iffD2),hypreal_mult_less_trans]) 1);
  1238 qed "hypreal_mult_le_less_trans";
  1239 
  1240 Goal "[| 0hr <= y; x <= r; y*r < t*s; 0hr < t*s|] ==> y*x < t*s";
  1241 by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1);
  1242 by (fast_tac (claset() addIs [hypreal_mult_le_less_trans]) 1);
  1243 qed "hypreal_mult_le_le_trans";
  1244 
  1245 Goal "[| 0hr < r1; r1 <r2; 0hr < x; x < y|] \
  1246 \                     ==> r1 * x < r2 * y";
  1247 by (dres_inst_tac [("x","x")] hypreal_mult_less_mono2 1);
  1248 by (dres_inst_tac [("R1.0","0hr")] hypreal_less_trans 2);
  1249 by (dres_inst_tac [("x","r1")] hypreal_mult_less_mono1 3);
  1250 by Auto_tac;
  1251 by (blast_tac (claset() addIs [hypreal_less_trans]) 1);
  1252 qed "hypreal_mult_less_mono";
  1253 
  1254 Goal "[| 0hr < r1; r1 <r2; 0hr < y|] \
  1255 \                           ==> 0hr < r2 * y";
  1256 by (dres_inst_tac [("R1.0","0hr")] hypreal_less_trans 1);
  1257 by (assume_tac 1);
  1258 by (blast_tac (claset() addIs [hypreal_mult_order]) 1);
  1259 qed "hypreal_mult_order_trans";
  1260 
  1261 Goal "[| 0hr < r1; r1 <= r2; 0hr <= x; x <= y |] \
  1262 \                  ==> r1 * x <= r2 * y";
  1263 by (rtac hypreal_less_or_eq_imp_le 1);
  1264 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
  1265 by (auto_tac (claset() addIs [hypreal_mult_less_mono,
  1266     hypreal_mult_less_mono1,hypreal_mult_less_mono2,
  1267     hypreal_mult_order_trans,hypreal_mult_order],simpset()));
  1268 qed "hypreal_mult_le_mono";
  1269 
  1270 (*----------------------------------------------------------
  1271   hypreal_of_real preserves field and order properties
  1272  -----------------------------------------------------------*)
  1273 Goalw [hypreal_of_real_def] 
  1274       "hypreal_of_real ((z1::real) + z2) = \
  1275 \      hypreal_of_real z1 + hypreal_of_real z2";
  1276 by (asm_simp_tac (simpset() addsimps [hypreal_add,
  1277        hypreal_add_mult_distrib]) 1);
  1278 qed "hypreal_of_real_add";
  1279 
  1280 Goalw [hypreal_of_real_def] 
  1281             "hypreal_of_real ((z1::real) * z2) = hypreal_of_real z1 * hypreal_of_real z2";
  1282 by (full_simp_tac (simpset() addsimps [hypreal_mult,
  1283         hypreal_add_mult_distrib2]) 1);
  1284 qed "hypreal_of_real_mult";
  1285 
  1286 Goalw [hypreal_less_def,hypreal_of_real_def] 
  1287             "(z1 < z2) = (hypreal_of_real z1 <  hypreal_of_real z2)";
  1288 by Auto_tac;
  1289 by (res_inst_tac [("x","%n. z1")] exI 1);
  1290 by (Step_tac 1); 
  1291 by (res_inst_tac [("x","%n. z2")] exI 2);
  1292 by Auto_tac;
  1293 by (rtac FreeUltrafilterNat_P 1);
  1294 by (Ultra_tac 1);
  1295 qed "hypreal_of_real_less_iff";
  1296 
  1297 Addsimps [hypreal_of_real_less_iff RS sym];
  1298 
  1299 Goalw [hypreal_le_def,real_le_def] 
  1300             "(z1 <= z2) = (hypreal_of_real z1 <=  hypreal_of_real z2)";
  1301 by Auto_tac;
  1302 qed "hypreal_of_real_le_iff";
  1303 
  1304 Goalw [hypreal_of_real_def] "hypreal_of_real (-r) = - hypreal_of_real  r";
  1305 by (auto_tac (claset(),simpset() addsimps [hypreal_minus]));
  1306 qed "hypreal_of_real_minus";
  1307 
  1308 Goal "0hr < x ==> 0hr < hrinv x";
  1309 by (EVERY1[rtac ccontr, dtac hypreal_leI]);
  1310 by (forward_tac [hypreal_minus_zero_less_iff2 RS iffD2] 1);
  1311 by (forward_tac [hypreal_not_refl2 RS not_sym] 1);
  1312 by (dtac (hypreal_not_refl2 RS not_sym RS hrinv_not_zero) 1);
  1313 by (EVERY1[dtac hypreal_le_imp_less_or_eq, Step_tac]); 
  1314 by (dtac hypreal_mult_less_zero1 1 THEN assume_tac 1);
  1315 by (auto_tac (claset() addIs [hypreal_zero_less_one RS hypreal_less_asym],
  1316     simpset() addsimps [hypreal_minus_mult_eq1 RS sym,
  1317      hypreal_minus_zero_less_iff]));
  1318 qed "hypreal_hrinv_gt_zero";
  1319 
  1320 Goal "x < 0hr ==> hrinv x < 0hr";
  1321 by (ftac hypreal_not_refl2 1);
  1322 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
  1323 by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
  1324 by (dtac (hypreal_minus_hrinv RS sym) 1);
  1325 by (auto_tac (claset() addIs [hypreal_hrinv_gt_zero],
  1326     simpset()));
  1327 qed "hypreal_hrinv_less_zero";
  1328 
  1329 Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real  1r = 1hr";
  1330 by (Step_tac 1);
  1331 qed "hypreal_of_real_one";
  1332 
  1333 Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real  0r = 0hr";
  1334 by (Step_tac 1);
  1335 qed "hypreal_of_real_zero";
  1336 
  1337 Goal "(hypreal_of_real  r = 0hr) = (r = 0r)";
  1338 by (auto_tac (claset() addIs [FreeUltrafilterNat_P],
  1339     simpset() addsimps [hypreal_of_real_def,
  1340     hypreal_zero_def,FreeUltrafilterNat_Nat_set]));
  1341 qed "hypreal_of_real_zero_iff";
  1342 
  1343 Goal "(hypreal_of_real  r ~= 0hr) = (r ~= 0r)";
  1344 by (full_simp_tac (simpset() addsimps [hypreal_of_real_zero_iff]) 1);
  1345 qed "hypreal_of_real_not_zero_iff";
  1346 
  1347 Goal "r ~= 0r ==> hrinv (hypreal_of_real r) = \
  1348 \          hypreal_of_real (rinv r)";
  1349 by (res_inst_tac [("c1","hypreal_of_real r")] (hypreal_mult_left_cancel RS iffD1) 1);
  1350 by (etac (hypreal_of_real_not_zero_iff RS iffD2) 1);
  1351 by (forward_tac [hypreal_of_real_not_zero_iff RS iffD2] 1);
  1352 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_mult RS sym,hypreal_of_real_one]));
  1353 qed "hypreal_of_real_hrinv";
  1354 
  1355 Goal "hypreal_of_real r ~= 0hr ==> hrinv (hypreal_of_real r) = \
  1356 \          hypreal_of_real (rinv r)";
  1357 by (etac (hypreal_of_real_not_zero_iff RS iffD1 RS hypreal_of_real_hrinv) 1);
  1358 qed "hypreal_of_real_hrinv2";
  1359 
  1360 Goal "x+x=x*(1hr+1hr)";
  1361 by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1);
  1362 qed "hypreal_add_self";
  1363 
  1364 Goal "1hr < 1hr + 1hr";
  1365 by (rtac (hypreal_less_minus_iff RS iffD2) 1);
  1366 by (full_simp_tac (simpset() addsimps [hypreal_zero_less_one,
  1367     hypreal_add_assoc]) 1);
  1368 qed "hypreal_one_less_two";
  1369 
  1370 Goal "0hr < 1hr + 1hr";
  1371 by (rtac ([hypreal_zero_less_one,
  1372           hypreal_one_less_two] MRS hypreal_less_trans) 1);
  1373 qed "hypreal_zero_less_two";
  1374 
  1375 Goal "1hr + 1hr ~= 0hr";
  1376 by (rtac (hypreal_zero_less_two RS hypreal_not_refl2 RS not_sym) 1);
  1377 qed "hypreal_two_not_zero";
  1378 Addsimps [hypreal_two_not_zero];
  1379 
  1380 Goal "x*hrinv(1hr + 1hr) + x*hrinv(1hr + 1hr) = x";
  1381 by (stac hypreal_add_self 1);
  1382 by (full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
  1383 qed "hypreal_sum_of_halves";
  1384 
  1385 Goal "z ~= 0hr ==> x*y = (x*hrinv(z))*(z*y)";
  1386 by (asm_simp_tac (simpset() addsimps hypreal_mult_ac)  1);
  1387 qed "lemma_chain";
  1388 
  1389 Goal "0hr < r ==> 0hr < r*hrinv(1hr+1hr)";
  1390 by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero 
  1391           RS hypreal_mult_less_mono1) 1);
  1392 by Auto_tac;
  1393 qed "hypreal_half_gt_zero";
  1394 
  1395 (* TODO: remove redundant  0hr < x *)
  1396 Goal "[| 0hr < r; 0hr < x; r < x |] ==> hrinv x < hrinv r";
  1397 by (ftac hypreal_hrinv_gt_zero 1);
  1398 by (forw_inst_tac [("x","x")] hypreal_hrinv_gt_zero 1);
  1399 by (forw_inst_tac [("x","r"),("z","hrinv r")] hypreal_mult_less_mono1 1);
  1400 by (assume_tac 1);
  1401 by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS 
  1402          not_sym RS hypreal_mult_hrinv]) 1);
  1403 by (ftac hypreal_hrinv_gt_zero 1);
  1404 by (forw_inst_tac [("x","1hr"),("z","hrinv x")] hypreal_mult_less_mono2 1);
  1405 by (assume_tac 1);
  1406 by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS 
  1407          not_sym RS hypreal_mult_hrinv_left,hypreal_mult_assoc RS sym]) 1);
  1408 qed "hypreal_hrinv_less_swap";
  1409 
  1410 Goal "[| 0hr < r; 0hr < x|] ==> (r < x) = (hrinv x < hrinv r)";
  1411 by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],simpset()));
  1412 by (res_inst_tac [("t","r")] (hypreal_hrinv_hrinv RS subst) 1);
  1413 by (etac (hypreal_not_refl2 RS not_sym) 1);
  1414 by (res_inst_tac [("t","x")] (hypreal_hrinv_hrinv RS subst) 1);
  1415 by (etac (hypreal_not_refl2 RS not_sym) 1);
  1416 by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],
  1417     simpset() addsimps [hypreal_hrinv_gt_zero]));
  1418 qed "hypreal_hrinv_less_iff";
  1419 
  1420 Goal "[| 0hr < z; x < y |] ==> x*hrinv(z) < y*hrinv(z)";
  1421 by (blast_tac (claset() addSIs [hypreal_mult_less_mono1,
  1422     hypreal_hrinv_gt_zero]) 1);
  1423 qed "hypreal_mult_hrinv_less_mono1";
  1424 
  1425 Goal "[| 0hr < z; x < y |] ==> hrinv(z)*x < hrinv(z)*y";
  1426 by (blast_tac (claset() addSIs [hypreal_mult_less_mono2,
  1427     hypreal_hrinv_gt_zero]) 1);
  1428 qed "hypreal_mult_hrinv_less_mono2";
  1429 
  1430 Goal "[| 0hr < z; x*z < y*z |] ==> x < y";
  1431 by (forw_inst_tac [("x","x*z")] hypreal_mult_hrinv_less_mono1 1);
  1432 by (dtac (hypreal_not_refl2 RS not_sym) 2);
  1433 by (auto_tac (claset() addSDs [hypreal_mult_hrinv],
  1434               simpset() addsimps hypreal_mult_ac));
  1435 qed "hypreal_less_mult_right_cancel";
  1436 
  1437 Goal "[| 0hr < z; z*x < z*y |] ==> x < y";
  1438 by (auto_tac (claset() addIs [hypreal_less_mult_right_cancel],
  1439     simpset() addsimps [hypreal_mult_commute]));
  1440 qed "hypreal_less_mult_left_cancel";
  1441 
  1442 Goal "[| 0hr < r; 0hr < ra; \
  1443 \                 r < x; ra < y |] \
  1444 \              ==> r*ra < x*y";
  1445 by (forw_inst_tac [("R2.0","r")] hypreal_less_trans 1);
  1446 by (dres_inst_tac [("z","ra"),("x","r")] hypreal_mult_less_mono1 2);
  1447 by (dres_inst_tac [("z","x"),("x","ra")] hypreal_mult_less_mono2 3);
  1448 by (auto_tac (claset() addIs [hypreal_less_trans],simpset()));
  1449 qed "hypreal_mult_less_gt_zero"; 
  1450 
  1451 Goal "[| 0hr < r; 0hr < ra; \
  1452 \                 r <= x; ra <= y |] \
  1453 \              ==> r*ra <= x*y";
  1454 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
  1455 by (rtac hypreal_less_or_eq_imp_le 1);
  1456 by (auto_tac (claset() addIs [hypreal_mult_less_mono1,
  1457     hypreal_mult_less_mono2,hypreal_mult_less_gt_zero],
  1458     simpset()));
  1459 qed "hypreal_mult_le_ge_zero"; 
  1460 
  1461 Goal "? (x::hypreal). x < y";
  1462 by (rtac (hypreal_add_zero_right RS subst) 1);
  1463 by (res_inst_tac [("x","y + -1hr")] exI 1);
  1464 by (auto_tac (claset() addSIs [hypreal_add_less_mono2],
  1465     simpset() addsimps [hypreal_minus_zero_less_iff2,
  1466     hypreal_zero_less_one] delsimps [hypreal_add_zero_right]));
  1467 qed "hypreal_less_Ex";
  1468 
  1469 Goal "!!(A::hypreal). A + C < B + C ==> A < B";
  1470 by (dres_inst_tac [("C","-C")] hypreal_add_less_mono1 1);
  1471 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
  1472 qed "hypreal_less_add_right_cancel";
  1473 
  1474 Goal "!!(A::hypreal). C + A < C + B ==> A < B";
  1475 by (dres_inst_tac [("C","-C")] hypreal_add_less_mono2 1);
  1476 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
  1477 qed "hypreal_less_add_left_cancel";
  1478 
  1479 Goal "0hr <= x*x";
  1480 by (res_inst_tac [("x","0hr"),("y","x")] hypreal_linear_less2 1);
  1481 by (auto_tac (claset() addIs [hypreal_mult_order,
  1482     hypreal_mult_less_zero1,hypreal_less_imp_le],
  1483     simpset()));
  1484 qed "hypreal_le_square";
  1485 Addsimps [hypreal_le_square];
  1486 
  1487 Goalw [hypreal_le_def] "- (x*x) <= 0hr";
  1488 by (auto_tac (claset() addSDs [(hypreal_le_square RS 
  1489     hypreal_le_less_trans)],simpset() addsimps 
  1490     [hypreal_minus_zero_less_iff,hypreal_less_not_refl]));
  1491 qed "hypreal_less_minus_square";
  1492 Addsimps [hypreal_less_minus_square];
  1493 
  1494 Goal "[|x ~= 0hr; y ~= 0hr |] ==> \
  1495 \                   hrinv(x) + hrinv(y) = (x + y)*hrinv(x*y)";
  1496 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv_distrib,
  1497              hypreal_add_mult_distrib,hypreal_mult_assoc RS sym]) 1);
  1498 by (stac hypreal_mult_assoc 1);
  1499 by (rtac (hypreal_mult_left_commute RS subst) 1);
  1500 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
  1501 qed "hypreal_hrinv_add";
  1502 
  1503 Goal "x = -x ==> x = 0hr";
  1504 by (dtac (hypreal_eq_minus_iff RS iffD1 RS sym) 1);
  1505 by (Asm_full_simp_tac 1);
  1506 by (dtac (hypreal_add_self RS subst) 1);
  1507 by (rtac ccontr 1);
  1508 by (blast_tac (claset() addDs [hypreal_two_not_zero RSN
  1509                (2,hypreal_mult_not_0)]) 1);
  1510 qed "hypreal_self_eq_minus_self_zero";
  1511 
  1512 Goal "(x + x = 0hr) = (x = 0hr)";
  1513 by Auto_tac;
  1514 by (dtac (hypreal_add_self RS subst) 1);
  1515 by (rtac ccontr 1 THEN rtac hypreal_mult_not_0E 1);
  1516 by Auto_tac;
  1517 qed "hypreal_add_self_zero_cancel";
  1518 Addsimps [hypreal_add_self_zero_cancel];
  1519 
  1520 Goal "(x + x + y = y) = (x = 0hr)";
  1521 by Auto_tac;
  1522 by (dtac (hypreal_eq_minus_iff RS iffD1) 1 THEN dtac sym 1);
  1523 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
  1524 qed "hypreal_add_self_zero_cancel2";
  1525 Addsimps [hypreal_add_self_zero_cancel2];
  1526 
  1527 Goal "(x + (x + y) = y) = (x = 0hr)";
  1528 by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
  1529 qed "hypreal_add_self_zero_cancel2a";
  1530 Addsimps [hypreal_add_self_zero_cancel2a];
  1531 
  1532 Goal "(b = -a) = (-b = (a::hypreal))";
  1533 by Auto_tac;
  1534 qed "hypreal_minus_eq_swap";
  1535 
  1536 Goal "(-b = -a) = (b = (a::hypreal))";
  1537 by (asm_full_simp_tac (simpset() addsimps 
  1538     [hypreal_minus_eq_swap]) 1);
  1539 qed "hypreal_minus_eq_cancel";
  1540 Addsimps [hypreal_minus_eq_cancel];
  1541 
  1542 Goal "x < x + 1hr";
  1543 by (cut_inst_tac [("C","x")] 
  1544     (hypreal_zero_less_one RS hypreal_add_less_mono2) 1);
  1545 by (Asm_full_simp_tac 1);
  1546 qed "hypreal_less_self_add_one";
  1547 Addsimps [hypreal_less_self_add_one];
  1548 
  1549 Goal "((x::hypreal) + x = y + y) = (x = y)";
  1550 by (auto_tac (claset() addIs [hypreal_two_not_zero RS 
  1551      hypreal_mult_left_cancel RS iffD1],simpset() addsimps 
  1552      [hypreal_add_mult_distrib]));
  1553 qed "hypreal_add_self_cancel";
  1554 Addsimps [hypreal_add_self_cancel];
  1555 
  1556 Goal "(y = x + - y + x) = (y = (x::hypreal))";
  1557 by Auto_tac;
  1558 by (dres_inst_tac [("x1","y")] 
  1559     (hypreal_add_right_cancel RS iffD2) 1);
  1560 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
  1561 qed "hypreal_add_self_minus_cancel";
  1562 Addsimps [hypreal_add_self_minus_cancel];
  1563 
  1564 Goal "(y = x + (- y + x)) = (y = (x::hypreal))";
  1565 by (asm_full_simp_tac (simpset() addsimps 
  1566          [hypreal_add_assoc RS sym])1);
  1567 qed "hypreal_add_self_minus_cancel2";
  1568 Addsimps [hypreal_add_self_minus_cancel2];
  1569 
  1570 Goal "z + -x = y + (y + (-x + -z)) = (y = (z::hypreal))";
  1571 by Auto_tac;
  1572 by (dres_inst_tac [("x1","z")] 
  1573     (hypreal_add_right_cancel RS iffD2) 1);
  1574 by (asm_full_simp_tac (simpset() addsimps 
  1575     [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac) 1);
  1576 by (asm_full_simp_tac (simpset() addsimps 
  1577      [hypreal_add_assoc RS sym,hypreal_add_right_cancel]) 1);
  1578 qed "hypreal_add_self_minus_cancel3";
  1579 Addsimps [hypreal_add_self_minus_cancel3];
  1580 
  1581 (* check why this does not work without 2nd substiution anymore! *)
  1582 Goal "x < y ==> x < (x + y)*hrinv(1hr + 1hr)";
  1583 by (dres_inst_tac [("C","x")] hypreal_add_less_mono2 1);
  1584 by (dtac (hypreal_add_self RS subst) 1);
  1585 by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS 
  1586           hypreal_mult_less_mono1) 1);
  1587 by (auto_tac (claset() addDs [hypreal_two_not_zero RS 
  1588           (hypreal_mult_hrinv RS subst)],simpset() 
  1589           addsimps [hypreal_mult_assoc]));
  1590 qed "hypreal_less_half_sum";
  1591 
  1592 (* check why this does not work without 2nd substiution anymore! *)
  1593 Goal "x < y ==> (x + y)*hrinv(1hr + 1hr) < y";
  1594 by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 1);
  1595 by (dtac (hypreal_add_self RS subst) 1);
  1596 by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS 
  1597           hypreal_mult_less_mono1) 1);
  1598 by (auto_tac (claset() addDs [hypreal_two_not_zero RS 
  1599           (hypreal_mult_hrinv RS subst)],simpset() 
  1600           addsimps [hypreal_mult_assoc]));
  1601 qed "hypreal_gt_half_sum";
  1602 
  1603 Goal "!!(x::hypreal). x < y ==> EX r. x < r & r < y";
  1604 by (blast_tac (claset() addSIs [hypreal_less_half_sum,
  1605     hypreal_gt_half_sum]) 1);
  1606 qed "hypreal_dense";
  1607 
  1608 Goal "(x * x = 0hr) = (x = 0hr)";
  1609 by Auto_tac;
  1610 by (blast_tac (claset() addIs [hypreal_mult_not_0E]) 1);
  1611 qed "hypreal_mult_self_eq_zero_iff";
  1612 Addsimps [hypreal_mult_self_eq_zero_iff];
  1613 
  1614 Goal "(0hr = x * x) = (x = 0hr)";
  1615 by (auto_tac (claset() addDs [sym],simpset()));
  1616 qed "hypreal_mult_self_eq_zero_iff2";
  1617 Addsimps [hypreal_mult_self_eq_zero_iff2];
  1618 
  1619 Goal "(x*x + y*y = 0hr) = (x = 0hr & y = 0hr)";
  1620 by Auto_tac;
  1621 by (dtac (sym RS (hypreal_eq_minus_iff3 RS iffD1))  1);
  1622 by (dtac (sym RS (hypreal_eq_minus_iff4 RS iffD1))  2);
  1623 by (ALLGOALS(rtac ccontr));
  1624 by (ALLGOALS(dtac hypreal_mult_self_not_zero));
  1625 by (cut_inst_tac [("x1","x")] (hypreal_le_square 
  1626         RS hypreal_le_imp_less_or_eq) 1);
  1627 by (cut_inst_tac [("x1","y")] (hypreal_le_square 
  1628         RS hypreal_le_imp_less_or_eq) 2);
  1629 by (auto_tac (claset() addDs [sym],simpset()));
  1630 by (dres_inst_tac [("x1","y")] (hypreal_less_minus_square 
  1631     RS hypreal_le_less_trans) 1);
  1632 by (dres_inst_tac [("x1","x")] (hypreal_less_minus_square 
  1633     RS hypreal_le_less_trans) 2);
  1634 by (auto_tac (claset(),simpset() addsimps 
  1635        [hypreal_less_not_refl]));
  1636 qed "hypreal_squares_add_zero_iff";
  1637 Addsimps [hypreal_squares_add_zero_iff];
  1638 
  1639 Goal "x * x ~= 0hr ==> 0hr < x* x + y*y + z*z";
  1640 by (cut_inst_tac [("x1","x")] (hypreal_le_square 
  1641         RS hypreal_le_imp_less_or_eq) 1);
  1642 by (auto_tac (claset() addSIs 
  1643               [hypreal_add_order_le],simpset()));
  1644 qed "hypreal_sum_squares3_gt_zero";
  1645 
  1646 Goal "x * x ~= 0hr ==> 0hr < y*y + x*x + z*z";
  1647 by (dtac hypreal_sum_squares3_gt_zero 1);
  1648 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
  1649 qed "hypreal_sum_squares3_gt_zero2";
  1650 
  1651 Goal "x * x ~= 0hr ==> 0hr < y*y + z*z + x*x";
  1652 by (dtac hypreal_sum_squares3_gt_zero 1);
  1653 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
  1654 qed "hypreal_sum_squares3_gt_zero3";
  1655 
  1656 Goal "(x*x + y*y + z*z = 0hr) = \ 
  1657 \               (x = 0hr & y = 0hr & z = 0hr)";
  1658 by Auto_tac;
  1659 by (ALLGOALS(rtac ccontr));
  1660 by (ALLGOALS(dtac hypreal_mult_self_not_zero));
  1661 by (auto_tac (claset() addDs [hypreal_not_refl2 RS not_sym,
  1662    hypreal_sum_squares3_gt_zero3,hypreal_sum_squares3_gt_zero,
  1663    hypreal_sum_squares3_gt_zero2],simpset() delsimps
  1664    [hypreal_mult_self_eq_zero_iff]));
  1665 qed "hypreal_three_squares_add_zero_iff";
  1666 Addsimps [hypreal_three_squares_add_zero_iff];
  1667 
  1668 Goal "(x::hypreal)*x <= x*x + y*y";
  1669 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  1670 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
  1671 by (auto_tac (claset(),simpset() addsimps 
  1672     [hypreal_mult,hypreal_add,hypreal_le]));
  1673 qed "hypreal_self_le_add_pos";
  1674 Addsimps [hypreal_self_le_add_pos];
  1675 
  1676 Goal "(x::hypreal)*x <= x*x + y*y + z*z";
  1677 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  1678 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
  1679 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
  1680 by (auto_tac (claset(),simpset() addsimps 
  1681     [hypreal_mult,hypreal_add,hypreal_le,
  1682     real_le_add_order]));
  1683 qed "hypreal_self_le_add_pos2";
  1684 Addsimps [hypreal_self_le_add_pos2];
  1685 
  1686 (*---------------------------------------------------------------------------------
  1687              Embedding of the naturals in the hyperreals
  1688  ---------------------------------------------------------------------------------*)
  1689 Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 0 = 1hr";
  1690 by (full_simp_tac (simpset() addsimps 
  1691     [pnat_one_iff RS sym,real_of_preal_def]) 1);
  1692 by (fold_tac [real_one_def]);
  1693 by (rtac hypreal_of_real_one 1);
  1694 qed "hypreal_of_posnat_one";
  1695 
  1696 Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr";
  1697 by (full_simp_tac (simpset() addsimps [real_of_preal_def,real_one_def,
  1698     hypreal_one_def,hypreal_add,hypreal_of_real_def,pnat_two_eq,
  1699     real_add,prat_of_pnat_add RS sym,preal_of_prat_add RS sym] @ pnat_add_ac) 1);
  1700 qed "hypreal_of_posnat_two";
  1701 
  1702 Goalw [hypreal_of_posnat_def]
  1703           "hypreal_of_posnat n1 + hypreal_of_posnat n2 = \
  1704 \          hypreal_of_posnat (n1 + n2) + 1hr";
  1705 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one RS sym,
  1706     hypreal_of_real_add RS sym,hypreal_of_posnat_def,real_of_preal_add RS sym,
  1707     preal_of_prat_add RS sym,prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
  1708 qed "hypreal_of_posnat_add";
  1709 
  1710 Goal "hypreal_of_posnat (n + 1) = hypreal_of_posnat n + 1hr";
  1711 by (res_inst_tac [("x1","1hr")] (hypreal_add_right_cancel RS iffD1) 1);
  1712 by (rtac (hypreal_of_posnat_add RS subst) 1);
  1713 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,hypreal_add_assoc]) 1);
  1714 qed "hypreal_of_posnat_add_one";
  1715 
  1716 Goalw [real_of_posnat_def,hypreal_of_posnat_def] 
  1717       "hypreal_of_posnat n = hypreal_of_real (real_of_posnat n)";
  1718 by (rtac refl 1);
  1719 qed "hypreal_of_real_of_posnat";
  1720 
  1721 Goalw [hypreal_of_posnat_def] 
  1722       "(n < m) = (hypreal_of_posnat n < hypreal_of_posnat m)";
  1723 by Auto_tac;
  1724 qed "hypreal_of_posnat_less_iff";
  1725 
  1726 Addsimps [hypreal_of_posnat_less_iff RS sym];
  1727 (*---------------------------------------------------------------------------------
  1728                Existence of infinite hyperreal number
  1729  ---------------------------------------------------------------------------------*)
  1730 
  1731 Goal "hyprel^^{%n::nat. real_of_posnat n} : hypreal";
  1732 by Auto_tac;
  1733 qed "hypreal_omega";
  1734 
  1735 Goalw [omega_def] "Rep_hypreal(whr) : hypreal";
  1736 by (rtac Rep_hypreal 1);
  1737 qed "Rep_hypreal_omega";
  1738 
  1739 (* existence of infinite number not corresponding to any real number *)
  1740 (* use assumption that member FreeUltrafilterNat is not finite       *)
  1741 (* a few lemmas first *)
  1742 
  1743 Goal "{n::nat. x = real_of_posnat n} = {} | \
  1744 \     (? y. {n::nat. x = real_of_posnat n} = {y})";
  1745 by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],simpset()));
  1746 qed "lemma_omega_empty_singleton_disj";
  1747 
  1748 Goal "finite {n::nat. x = real_of_posnat n}";
  1749 by (cut_inst_tac [("x","x")] lemma_omega_empty_singleton_disj 1);
  1750 by Auto_tac;
  1751 qed "lemma_finite_omega_set";
  1752 
  1753 Goalw [omega_def,hypreal_of_real_def] 
  1754       "~ (? x. hypreal_of_real x = whr)";
  1755 by (auto_tac (claset(),simpset() addsimps [lemma_finite_omega_set 
  1756     RS FreeUltrafilterNat_finite]));
  1757 qed "not_ex_hypreal_of_real_eq_omega";
  1758 
  1759 Goal "hypreal_of_real x ~= whr";
  1760 by (cut_facts_tac [not_ex_hypreal_of_real_eq_omega] 1);
  1761 by Auto_tac;
  1762 qed "hypreal_of_real_not_eq_omega";
  1763 
  1764 (* existence of infinitesimal number also not *)
  1765 (* corresponding to any real number *)
  1766 
  1767 Goal "{n::nat. x = rinv(real_of_posnat n)} = {} | \
  1768 \     (? y. {n::nat. x = rinv(real_of_posnat n)} = {y})";
  1769 by (Step_tac 1 THEN Step_tac 1);
  1770 by (auto_tac (claset() addIs [real_of_posnat_rinv_inj],simpset()));
  1771 qed "lemma_epsilon_empty_singleton_disj";
  1772 
  1773 Goal "finite {n::nat. x = rinv(real_of_posnat n)}";
  1774 by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1);
  1775 by Auto_tac;
  1776 qed "lemma_finite_epsilon_set";
  1777 
  1778 Goalw [epsilon_def,hypreal_of_real_def] 
  1779       "~ (? x. hypreal_of_real x = ehr)";
  1780 by (auto_tac (claset(),simpset() addsimps [lemma_finite_epsilon_set 
  1781     RS FreeUltrafilterNat_finite]));
  1782 qed "not_ex_hypreal_of_real_eq_epsilon";
  1783 
  1784 Goal "hypreal_of_real x ~= ehr";
  1785 by (cut_facts_tac [not_ex_hypreal_of_real_eq_epsilon] 1);
  1786 by Auto_tac;
  1787 qed "hypreal_of_real_not_eq_epsilon";
  1788 
  1789 Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0hr";
  1790 by (auto_tac (claset(),simpset() addsimps 
  1791     [real_of_posnat_rinv_not_zero]));
  1792 qed "hypreal_epsilon_not_zero";
  1793 
  1794 Goalw [omega_def,hypreal_zero_def] "whr ~= 0hr";
  1795 by (Simp_tac 1);
  1796 qed "hypreal_omega_not_zero";
  1797 
  1798 Goal "ehr = hrinv(whr)";
  1799 by (asm_full_simp_tac (simpset() addsimps 
  1800     [hypreal_hrinv,omega_def,epsilon_def]
  1801     setloop (split_tac [expand_if])) 1);
  1802 qed "hypreal_epsilon_hrinv_omega";
  1803 
  1804 (*----------------------------------------------------------------
  1805      Another embedding of the naturals in the 
  1806     hyperreals (see hypreal_of_posnat)
  1807  ----------------------------------------------------------------*)
  1808 Goalw [hypreal_of_nat_def] "hypreal_of_nat 0 = 0hr";
  1809 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one]) 1);
  1810 qed "hypreal_of_nat_zero";
  1811 
  1812 Goalw [hypreal_of_nat_def] "hypreal_of_nat 1 = 1hr";
  1813 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,
  1814     hypreal_add_assoc]) 1);
  1815 qed "hypreal_of_nat_one";
  1816 
  1817 Goalw [hypreal_of_nat_def]
  1818       "hypreal_of_nat n1 + hypreal_of_nat n2 = \
  1819 \      hypreal_of_nat (n1 + n2)";
  1820 by (full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
  1821 by (simp_tac (simpset() addsimps [hypreal_of_posnat_add,
  1822     hypreal_add_assoc RS sym]) 1);
  1823 by (rtac (hypreal_add_commute RS subst) 1);
  1824 by (simp_tac (simpset() addsimps [hypreal_add_left_cancel,
  1825     hypreal_add_assoc]) 1);
  1826 qed "hypreal_of_nat_add";
  1827 
  1828 Goal "hypreal_of_nat 2 = 1hr + 1hr";
  1829 by (simp_tac (simpset() addsimps [hypreal_of_nat_one 
  1830     RS sym,hypreal_of_nat_add]) 1);
  1831 qed "hypreal_of_nat_two";
  1832 
  1833 Goalw [hypreal_of_nat_def] 
  1834       "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)";
  1835 by (auto_tac (claset() addIs [hypreal_add_less_mono1],simpset()));
  1836 by (dres_inst_tac [("C","1hr")] hypreal_add_less_mono1 1);
  1837 by (full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
  1838 qed "hypreal_of_nat_less_iff";
  1839 Addsimps [hypreal_of_nat_less_iff RS sym];
  1840 
  1841 (* naturals embedded in hyperreals is an hyperreal *)
  1842 Goalw [hypreal_of_nat_def,real_of_nat_def] 
  1843       "hypreal_of_nat  m = Abs_hypreal(hyprel^^{%n. real_of_nat m})";
  1844 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def,
  1845     hypreal_of_real_of_posnat,hypreal_minus,hypreal_one_def,hypreal_add]));
  1846 qed "hypreal_of_nat_iff";
  1847 
  1848 Goal "inj hypreal_of_nat";
  1849 by (rtac injI 1);
  1850 by (auto_tac (claset() addSDs [FreeUltrafilterNat_P],
  1851         simpset() addsimps [hypreal_of_nat_iff,
  1852         real_add_right_cancel,inj_real_of_nat RS injD]));
  1853 qed "inj_hypreal_of_nat";
  1854 
  1855 Goalw [hypreal_of_nat_def,hypreal_of_real_def,hypreal_of_posnat_def,
  1856        real_of_posnat_def,hypreal_one_def,real_of_nat_def] 
  1857        "hypreal_of_nat n = hypreal_of_real (real_of_nat n)";
  1858 by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1);
  1859 qed "hypreal_of_nat_real_of_nat";
  1860 
  1861 
  1862 
  1863 
  1864 
  1865 
  1866 
  1867 
  1868 
  1869 
  1870 
  1871 
  1872 
  1873 
  1874 
  1875 
  1876 
  1877 
  1878 
  1879 
  1880 
  1881 
  1882 
  1883 
  1884 
  1885 
  1886 
  1887 
  1888 
  1889 
  1890 
  1891 
  1892 
  1893 
  1894 
  1895 
  1896 
  1897 
  1898 
  1899 
  1900 
  1901 
  1902 
  1903 
  1904 
  1905 
  1906 
  1907 
  1908 
  1909 
  1910 
  1911 
  1912 
  1913 
  1914 
  1915 
  1916 
  1917 
  1918 
  1919 
  1920 
  1921 
  1922 
  1923 
  1924 
  1925 
  1926 
  1927 
  1928 
  1929 
  1930 
  1931 
  1932 
  1933 
  1934 
  1935 
  1936 
  1937 
  1938 
  1939 
  1940 
  1941 
  1942 
  1943 
  1944 
  1945 
  1946 
  1947 
  1948 
  1949 
  1950 
  1951 
  1952 
  1953 
  1954 
  1955 
  1956 
  1957 
  1958 
  1959 
  1960 
  1961 
  1962 
  1963 
  1964 
  1965 
  1966 
  1967 
  1968 
  1969 
  1970 
  1971 
  1972 
  1973 
  1974 
  1975 
  1976 
  1977 
  1978 
  1979 
  1980 
  1981 
  1982 
  1983 
  1984 
  1985 
  1986 
  1987 
  1988 
  1989 
  1990 
  1991 
  1992 
  1993 
  1994 
  1995 
  1996 
  1997 
  1998 
  1999 
  2000 
  2001 
  2002 
  2003 
  2004 
  2005 
  2006 
  2007 
  2008 
  2009 
  2010 
  2011 
  2012 
  2013 
  2014 
  2015 
  2016 
  2017 
  2018 
  2019 
  2020 
  2021 
  2022 
  2023 
  2024 
  2025 
  2026 
  2027 
  2028 
  2029 
  2030 
  2031 
  2032 
  2033 
  2034 
  2035 
  2036 
  2037 
  2038 
  2039 
  2040 
  2041 
  2042 
  2043 
  2044 
  2045 
  2046 
  2047 
  2048 
  2049 
  2050 
  2051 
  2052 
  2053 
  2054 
  2055 
  2056 
  2057 
  2058 
  2059 
  2060 
  2061 
  2062 
  2063 
  2064 
  2065 
  2066 
  2067 
  2068 
  2069 
  2070 
  2071 
  2072 
  2073 
  2074 
  2075 
  2076 
  2077 
  2078 
  2079 
  2080 
  2081 
  2082 
  2083 
  2084 
  2085 
  2086 
  2087 
  2088 
  2089 
  2090 
  2091 
  2092 
  2093 
  2094 
  2095 
  2096 
  2097 
  2098 
  2099 
  2100 
  2101 
  2102 
  2103 
  2104 
  2105 
  2106 
  2107 
  2108 
  2109 
  2110 
  2111 
  2112 
  2113 
  2114 
  2115 
  2116 
  2117 
  2118 
  2119 
  2120 
  2121 
  2122 
  2123 
  2124 
  2125 
  2126 
  2127 
  2128 
  2129 
  2130 
  2131 
  2132 
  2133 
  2134 
  2135 
  2136 
  2137 
  2138 
  2139 
  2140 
  2141 
  2142 
  2143 
  2144 
  2145 
  2146 
  2147 
  2148 
  2149 
  2150 
  2151 
  2152 
  2153 
  2154 
  2155 
  2156 
  2157 
  2158 
  2159 
  2160 
  2161 
  2162 
  2163 
  2164 
  2165 
  2166 
  2167 
  2168 
  2169 
  2170 
  2171 
  2172 
  2173 
  2174 
  2175 
  2176 
  2177 
  2178 
  2179 
  2180 
  2181 
  2182 
  2183 
  2184 
  2185 
  2186 
  2187 
  2188 
  2189 
  2190 
  2191 
  2192 
  2193 
  2194 
  2195 
  2196 
  2197 
  2198 
  2199 
  2200 
  2201 
  2202 
  2203 
  2204 
  2205 
  2206 
  2207 
  2208 
  2209 
  2210 
  2211 
  2212 
  2213 
  2214 
  2215 
  2216 
  2217 
  2218 
  2219 
  2220 
  2221 
  2222 
  2223 
  2224 
  2225 
  2226 
  2227