src/HOL/Real/Hyperreal/HyperDef.ML
author paulson
Wed Jun 14 18:24:41 2000 +0200 (2000-06-14)
changeset 9071 6416d5a5f712
parent 9055 f020e00c6304
child 9108 9fff97d29837
permissions -rw-r--r--
tidied
     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) --> (EX n. ALL 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) --> (EX 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] "-0 = (0::hypreal)";
   315 by (simp_tac (simpset() addsimps [hypreal_minus]) 1);
   316 qed "hypreal_minus_zero";
   317 
   318 Addsimps [hypreal_minus_zero];
   319 
   320 Goal "(-x = 0) = (x = (0::hypreal))"; 
   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 = #0 then #0 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 = #0 then #0 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 ~= 0 ==> 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 (map (rename_numerals thy)
   351 			       [rinv_not_zero,real_rinv_rinv]),
   352 	       simpset()) 1);
   353 qed "hypreal_hrinv_hrinv";
   354 
   355 Addsimps [hypreal_hrinv_hrinv];
   356 
   357 Goalw [hypreal_one_def] "hrinv(1hr) = 1hr";
   358 by (full_simp_tac (simpset() addsimps [hypreal_hrinv,
   359        real_zero_not_eq_one RS not_sym] 
   360                    setloop (split_tac [expand_if])) 1);
   361 qed "hypreal_hrinv_1";
   362 Addsimps [hypreal_hrinv_1];
   363 
   364 (**** hyperreal addition: hypreal_add  ****)
   365 
   366 Goalw [congruent2_def]
   367     "congruent2 hyprel (%X Y. hyprel^^{%n. X n + Y n})";
   368 by Safe_tac;
   369 by (ALLGOALS(Ultra_tac));
   370 qed "hypreal_add_congruent2";
   371 
   372 (*Resolve th against the corresponding facts for hyppreal_add*)
   373 val hypreal_add_ize = RSLIST [equiv_hyprel, hypreal_add_congruent2];
   374 
   375 Goalw [hypreal_add_def]
   376   "Abs_hypreal(hyprel^^{%n. X n}) + Abs_hypreal(hyprel^^{%n. Y n}) = \
   377 \  Abs_hypreal(hyprel^^{%n. X n + Y n})";
   378 by (asm_simp_tac
   379     (simpset() addsimps [hypreal_add_ize UN_equiv_class2]) 1);
   380 qed "hypreal_add";
   381 
   382 Goal "(z::hypreal) + w = w + z";
   383 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   384 by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
   385 by (asm_simp_tac (simpset() addsimps (real_add_ac @ [hypreal_add])) 1);
   386 qed "hypreal_add_commute";
   387 
   388 Goal "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)";
   389 by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
   390 by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
   391 by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
   392 by (asm_simp_tac (simpset() addsimps [hypreal_add, real_add_assoc]) 1);
   393 qed "hypreal_add_assoc";
   394 
   395 (*For AC rewriting*)
   396 Goal "(x::hypreal)+(y+z)=y+(x+z)";
   397 by (rtac (hypreal_add_commute RS trans) 1);
   398 by (rtac (hypreal_add_assoc RS trans) 1);
   399 by (rtac (hypreal_add_commute RS arg_cong) 1);
   400 qed "hypreal_add_left_commute";
   401 
   402 (* hypreal addition is an AC operator *)
   403 val hypreal_add_ac = [hypreal_add_assoc,hypreal_add_commute,
   404                       hypreal_add_left_commute];
   405 
   406 Goalw [hypreal_zero_def] "(0::hypreal) + z = z";
   407 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   408 by (asm_full_simp_tac (simpset() addsimps 
   409     [hypreal_add]) 1);
   410 qed "hypreal_add_zero_left";
   411 
   412 Goal "z + (0::hypreal) = z";
   413 by (simp_tac (simpset() addsimps 
   414     [hypreal_add_zero_left,hypreal_add_commute]) 1);
   415 qed "hypreal_add_zero_right";
   416 
   417 Goalw [hypreal_zero_def] "z + -z = (0::hypreal)";
   418 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   419 by (asm_full_simp_tac (simpset() addsimps [hypreal_minus,
   420         hypreal_add]) 1);
   421 qed "hypreal_add_minus";
   422 
   423 Goal "-z + z = (0::hypreal)";
   424 by (simp_tac (simpset() addsimps 
   425     [hypreal_add_commute,hypreal_add_minus]) 1);
   426 qed "hypreal_add_minus_left";
   427 
   428 Addsimps [hypreal_add_minus,hypreal_add_minus_left,
   429           hypreal_add_zero_left,hypreal_add_zero_right];
   430 
   431 Goal "EX y. (x::hypreal) + y = 0";
   432 by (fast_tac (claset() addIs [hypreal_add_minus]) 1);
   433 qed "hypreal_minus_ex";
   434 
   435 Goal "EX! y. (x::hypreal) + y = 0";
   436 by (auto_tac (claset() addIs [hypreal_add_minus],simpset()));
   437 by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
   438 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   439 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   440 qed "hypreal_minus_ex1";
   441 
   442 Goal "EX! y. y + (x::hypreal) = 0";
   443 by (auto_tac (claset() addIs [hypreal_add_minus_left],simpset()));
   444 by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
   445 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
   446 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   447 qed "hypreal_minus_left_ex1";
   448 
   449 Goal "x + y = (0::hypreal) ==> x = -y";
   450 by (cut_inst_tac [("z","y")] hypreal_add_minus_left 1);
   451 by (res_inst_tac [("x1","y")] (hypreal_minus_left_ex1 RS ex1E) 1);
   452 by (Blast_tac 1);
   453 qed "hypreal_add_minus_eq_minus";
   454 
   455 Goal "EX y::hypreal. x = -y";
   456 by (cut_inst_tac [("x","x")] hypreal_minus_ex 1);
   457 by (etac exE 1 THEN dtac hypreal_add_minus_eq_minus 1);
   458 by (Fast_tac 1);
   459 qed "hypreal_as_add_inverse_ex";
   460 
   461 Goal "-(x + (y::hypreal)) = -x + -y";
   462 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   463 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   464 by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
   465     hypreal_add,real_minus_add_distrib]));
   466 qed "hypreal_minus_add_distrib";
   467 
   468 Goal "-(y + -(x::hypreal)) = x + -y";
   469 by (simp_tac (simpset() addsimps [hypreal_minus_add_distrib,
   470     hypreal_add_commute]) 1);
   471 qed "hypreal_minus_distrib1";
   472 
   473 Goal "(x + - (y::hypreal)) + (y + - z) = x + -z";
   474 by (res_inst_tac [("w1","y")] (hypreal_add_commute RS subst) 1);
   475 by (simp_tac (simpset() addsimps [hypreal_add_left_commute,
   476     hypreal_add_assoc]) 1);
   477 by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   478 qed "hypreal_add_minus_cancel1";
   479 
   480 Goal "((x::hypreal) + y = x + z) = (y = z)";
   481 by (Step_tac 1);
   482 by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1);
   483 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   484 qed "hypreal_add_left_cancel";
   485 
   486 Goal "z + (x + (y + -z)) = x + (y::hypreal)";
   487 by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
   488 qed "hypreal_add_minus_cancel2";
   489 Addsimps [hypreal_add_minus_cancel2];
   490 
   491 Goal "y + -(x + y) = -(x::hypreal)";
   492 by (full_simp_tac (simpset() addsimps [hypreal_minus_add_distrib]) 1);
   493 by (rtac (hypreal_add_left_commute RS subst) 1);
   494 by (Full_simp_tac 1);
   495 qed "hypreal_add_minus_cancel";
   496 Addsimps [hypreal_add_minus_cancel];
   497 
   498 Goal "y + -(y + x) = -(x::hypreal)";
   499 by (simp_tac (simpset() addsimps [hypreal_minus_add_distrib,
   500               hypreal_add_assoc RS sym]) 1);
   501 qed "hypreal_add_minus_cancelc";
   502 Addsimps [hypreal_add_minus_cancelc];
   503 
   504 Goal "(z + -x) + (y + -z) = (y + -(x::hypreal))";
   505 by (full_simp_tac (simpset() addsimps [hypreal_minus_add_distrib
   506     RS sym, hypreal_add_left_cancel] @ hypreal_add_ac) 1); 
   507 qed "hypreal_add_minus_cancel3";
   508 Addsimps [hypreal_add_minus_cancel3];
   509 
   510 Goal "(y + (x::hypreal)= z + x) = (y = z)";
   511 by (simp_tac (simpset() addsimps [hypreal_add_commute,
   512     hypreal_add_left_cancel]) 1);
   513 qed "hypreal_add_right_cancel";
   514 
   515 Goal "z + (y + -z) = (y::hypreal)";
   516 by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
   517 qed "hypreal_add_minus_cancel4";
   518 Addsimps [hypreal_add_minus_cancel4];
   519 
   520 Goal "z + (w + (x + (-z + y))) = w + x + (y::hypreal)";
   521 by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
   522 qed "hypreal_add_minus_cancel5";
   523 Addsimps [hypreal_add_minus_cancel5];
   524 
   525 
   526 (**** hyperreal multiplication: hypreal_mult  ****)
   527 
   528 Goalw [congruent2_def]
   529     "congruent2 hyprel (%X Y. hyprel^^{%n. X n * Y n})";
   530 by Safe_tac;
   531 by (ALLGOALS(Ultra_tac));
   532 qed "hypreal_mult_congruent2";
   533 
   534 (*Resolve th against the corresponding facts for hypreal_mult*)
   535 val hypreal_mult_ize = RSLIST [equiv_hyprel, hypreal_mult_congruent2];
   536 
   537 Goalw [hypreal_mult_def]
   538   "Abs_hypreal(hyprel^^{%n. X n}) * Abs_hypreal(hyprel^^{%n. Y n}) = \
   539 \  Abs_hypreal(hyprel^^{%n. X n * Y n})";
   540 by (asm_simp_tac
   541     (simpset() addsimps [hypreal_mult_ize UN_equiv_class2]) 1);
   542 qed "hypreal_mult";
   543 
   544 Goal "(z::hypreal) * w = w * z";
   545 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   546 by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
   547 by (asm_simp_tac (simpset() addsimps ([hypreal_mult] @ real_mult_ac)) 1);
   548 qed "hypreal_mult_commute";
   549 
   550 Goal "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)";
   551 by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
   552 by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
   553 by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
   554 by (asm_simp_tac (simpset() addsimps [hypreal_mult,real_mult_assoc]) 1);
   555 qed "hypreal_mult_assoc";
   556 
   557 qed_goal "hypreal_mult_left_commute" thy
   558     "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)"
   559  (fn _ => [rtac (hypreal_mult_commute RS trans) 1, rtac (hypreal_mult_assoc RS trans) 1,
   560            rtac (hypreal_mult_commute RS arg_cong) 1]);
   561 
   562 (* hypreal multiplication is an AC operator *)
   563 val hypreal_mult_ac = [hypreal_mult_assoc, hypreal_mult_commute, 
   564                        hypreal_mult_left_commute];
   565 
   566 Goalw [hypreal_one_def] "1hr * z = z";
   567 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   568 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult]) 1);
   569 qed "hypreal_mult_1";
   570 
   571 Goal "z * 1hr = z";
   572 by (simp_tac (simpset() addsimps [hypreal_mult_commute,
   573     hypreal_mult_1]) 1);
   574 qed "hypreal_mult_1_right";
   575 
   576 Goalw [hypreal_zero_def] "0 * z = (0::hypreal)";
   577 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   578 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult,real_mult_0]) 1);
   579 qed "hypreal_mult_0";
   580 
   581 Goal "z * 0 = (0::hypreal)";
   582 by (simp_tac (simpset() addsimps [hypreal_mult_commute,
   583     hypreal_mult_0]) 1);
   584 qed "hypreal_mult_0_right";
   585 
   586 Addsimps [hypreal_mult_0,hypreal_mult_0_right];
   587 
   588 Goal "-(x * y) = -x * (y::hypreal)";
   589 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   590 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   591 by (auto_tac (claset(),
   592 	      simpset() addsimps [hypreal_minus, hypreal_mult] 
   593                                  @ real_mult_ac @ real_add_ac));
   594 qed "hypreal_minus_mult_eq1";
   595 
   596 Goal "-(x * y) = (x::hypreal) * -y";
   597 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   598 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   599 by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
   600 					   hypreal_mult] 
   601                                            @ real_mult_ac @ real_add_ac));
   602 qed "hypreal_minus_mult_eq2";
   603 
   604 (*Pull negations out*)
   605 Addsimps [hypreal_minus_mult_eq2 RS sym, hypreal_minus_mult_eq1 RS sym];
   606 
   607 Goal "-x*y = (x::hypreal)*-y";
   608 by Auto_tac;
   609 qed "hypreal_minus_mult_commute";
   610 
   611 
   612 (*-----------------------------------------------------------------------------
   613     A few more theorems
   614  ----------------------------------------------------------------------------*)
   615 Goal "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
   616 by (asm_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   617 qed "hypreal_add_assoc_cong";
   618 
   619 Goal "(z::hypreal) + (v + w) = v + (z + w)";
   620 by (REPEAT (ares_tac [hypreal_add_commute RS hypreal_add_assoc_cong] 1));
   621 qed "hypreal_add_assoc_swap";
   622 
   623 Goal "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)";
   624 by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
   625 by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
   626 by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
   627 by (asm_simp_tac (simpset() addsimps [hypreal_mult,hypreal_add,
   628      real_add_mult_distrib]) 1);
   629 qed "hypreal_add_mult_distrib";
   630 
   631 val hypreal_mult_commute'= read_instantiate [("z","w")] hypreal_mult_commute;
   632 
   633 Goal "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)";
   634 by (simp_tac (simpset() addsimps [hypreal_mult_commute',hypreal_add_mult_distrib]) 1);
   635 qed "hypreal_add_mult_distrib2";
   636 
   637 val hypreal_mult_simps = [hypreal_mult_1, hypreal_mult_1_right];
   638 Addsimps hypreal_mult_simps;
   639 
   640 (*** one and zero are distinct ***)
   641 Goalw [hypreal_zero_def,hypreal_one_def] "0 ~= 1hr";
   642 by (auto_tac (claset(),simpset() addsimps [real_zero_not_eq_one]));
   643 qed "hypreal_zero_not_eq_one";
   644 
   645 (*** existence of inverse ***)
   646 Goalw [hypreal_one_def,hypreal_zero_def] 
   647           "x ~= 0 ==> x*hrinv(x) = 1hr";
   648 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   649 by (rotate_tac 1 1);
   650 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
   651     hypreal_mult] setloop (split_tac [expand_if])) 1);
   652 by (dtac FreeUltrafilterNat_Compl_mem 1);
   653 by (blast_tac (claset() addSIs [real_mult_inv_right,
   654     FreeUltrafilterNat_subset]) 1);
   655 qed "hypreal_mult_hrinv";
   656 
   657 Goal "x ~= 0 ==> hrinv(x)*x = 1hr";
   658 by (asm_simp_tac (simpset() addsimps [hypreal_mult_hrinv,
   659 				      hypreal_mult_commute]) 1);
   660 qed "hypreal_mult_hrinv_left";
   661 
   662 Goal "x ~= 0 ==> EX y. x * y = 1hr";
   663 by (fast_tac (claset() addDs [hypreal_mult_hrinv]) 1);
   664 qed "hypreal_hrinv_ex";
   665 
   666 Goal "x ~= 0 ==> EX y. y * x = 1hr";
   667 by (fast_tac (claset() addDs [hypreal_mult_hrinv_left]) 1);
   668 qed "hypreal_hrinv_left_ex";
   669 
   670 Goal "x ~= 0 ==> EX! y. x * y = 1hr";
   671 by (auto_tac (claset() addIs [hypreal_mult_hrinv],simpset()));
   672 by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
   673 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
   674 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
   675 qed "hypreal_hrinv_ex1";
   676 
   677 Goal "x ~= 0 ==> EX! y. y * x = 1hr";
   678 by (auto_tac (claset() addIs [hypreal_mult_hrinv_left],simpset()));
   679 by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
   680 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
   681 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
   682 qed "hypreal_hrinv_left_ex1";
   683 
   684 Goal "[| y~= 0; x * y = 1hr |]  ==> x = hrinv y";
   685 by (forw_inst_tac [("x","y")] hypreal_mult_hrinv_left 1);
   686 by (res_inst_tac [("x1","y")] (hypreal_hrinv_left_ex1 RS ex1E) 1);
   687 by (assume_tac 1);
   688 by (Blast_tac 1);
   689 qed "hypreal_mult_inv_hrinv";
   690 
   691 Goal "x ~= 0 ==> EX y. x = hrinv y";
   692 by (forw_inst_tac [("x","x")] hypreal_hrinv_left_ex 1);
   693 by (etac exE 1 THEN 
   694     forw_inst_tac [("x","y")] hypreal_mult_inv_hrinv 1);
   695 by (res_inst_tac [("x","y")] exI 2);
   696 by Auto_tac;
   697 qed "hypreal_as_inverse_ex";
   698 
   699 Goal "(c::hypreal) ~= 0 ==> (c*a=c*b) = (a=b)";
   700 by Auto_tac;
   701 by (dres_inst_tac [("f","%x. x*hrinv c")] arg_cong 1);
   702 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_hrinv] @ hypreal_mult_ac)  1);
   703 qed "hypreal_mult_left_cancel";
   704     
   705 Goal "(c::hypreal) ~= 0 ==> (a*c=b*c) = (a=b)";
   706 by (Step_tac 1);
   707 by (dres_inst_tac [("f","%x. x*hrinv c")] arg_cong 1);
   708 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_hrinv] @ hypreal_mult_ac)  1);
   709 qed "hypreal_mult_right_cancel";
   710 
   711 Goalw [hypreal_zero_def] "x ~= 0 ==> hrinv(x) ~= 0";
   712 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   713 by (rotate_tac 1 1);
   714 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
   715     hypreal_mult] setloop (split_tac [expand_if])) 1);
   716 by (dtac FreeUltrafilterNat_Compl_mem 1 THEN Clarify_tac 1);
   717 by (ultra_tac (claset() addIs [ccontr]
   718                         addDs [rename_numerals thy rinv_not_zero],
   719 	       simpset()) 1);
   720 qed "hrinv_not_zero";
   721 
   722 Addsimps [hypreal_mult_hrinv,hypreal_mult_hrinv_left];
   723 
   724 Goal "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::hypreal)";
   725 by (Step_tac 1);
   726 by (dres_inst_tac [("f","%z. hrinv x*z")] arg_cong 1);
   727 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
   728 qed "hypreal_mult_not_0";
   729 
   730 bind_thm ("hypreal_mult_not_0E",hypreal_mult_not_0 RS notE);
   731 
   732 Goal "x ~= 0 ==> x * x ~= (0::hypreal)";
   733 by (blast_tac (claset() addDs [hypreal_mult_not_0]) 1);
   734 qed "hypreal_mult_self_not_zero";
   735 
   736 Goal "[| x ~= 0; y ~= 0 |] ==> hrinv(x*y) = hrinv(x)*hrinv(y)";
   737 by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
   738 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,
   739     hypreal_mult_not_0]));
   740 by (res_inst_tac [("c1","y")] (hypreal_mult_right_cancel RS iffD1) 1);
   741 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_not_0] @ hypreal_mult_ac));
   742 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,hypreal_mult_not_0]));
   743 qed "hrinv_mult_eq";
   744 
   745 Goal "x ~= 0 ==> hrinv(-x) = -hrinv(x)";
   746 by (rtac (hypreal_mult_right_cancel RS iffD1) 1);
   747 by (stac hypreal_mult_hrinv_left 2);
   748 by Auto_tac;
   749 qed "hypreal_minus_hrinv";
   750 
   751 Goal "[| x ~= 0; y ~= 0 |] \
   752 \     ==> hrinv(x*y) = hrinv(x)*hrinv(y)";
   753 by (forw_inst_tac [("y","y")] hypreal_mult_not_0 1 THEN assume_tac 1);
   754 by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
   755 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym]));
   756 by (res_inst_tac [("c1","y")] (hypreal_mult_left_cancel RS iffD1) 1);
   757 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_left_commute]));
   758 by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
   759 qed "hypreal_hrinv_distrib";
   760 
   761 (*------------------------------------------------------------------
   762                    Theorems for ordering 
   763  ------------------------------------------------------------------*)
   764 
   765 (* prove introduction and elimination rules for hypreal_less *)
   766 
   767 Goalw [hypreal_less_def]
   768  "P < (Q::hypreal) = (EX X Y. X : Rep_hypreal(P) & \
   769 \                             Y : Rep_hypreal(Q) & \
   770 \                             {n. X n < Y n} : FreeUltrafilterNat)";
   771 by (Fast_tac 1);
   772 qed "hypreal_less_iff";
   773 
   774 Goalw [hypreal_less_def]
   775  "[| {n. X n < Y n} : FreeUltrafilterNat; \
   776 \         X : Rep_hypreal(P); \
   777 \         Y : Rep_hypreal(Q) |] ==> P < (Q::hypreal)";
   778 by (Fast_tac 1);
   779 qed "hypreal_lessI";
   780 
   781 
   782 Goalw [hypreal_less_def]
   783      "!! R1. [| R1 < (R2::hypreal); \
   784 \         !!X Y. {n. X n < Y n} : FreeUltrafilterNat ==> P; \
   785 \         !!X. X : Rep_hypreal(R1) ==> P; \ 
   786 \         !!Y. Y : Rep_hypreal(R2) ==> P |] \
   787 \     ==> P";
   788 by Auto_tac;
   789 qed "hypreal_lessE";
   790 
   791 Goalw [hypreal_less_def]
   792  "R1 < (R2::hypreal) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \
   793 \                                  X : Rep_hypreal(R1) & \
   794 \                                  Y : Rep_hypreal(R2))";
   795 by (Fast_tac 1);
   796 qed "hypreal_lessD";
   797 
   798 Goal "~ (R::hypreal) < R";
   799 by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
   800 by (auto_tac (claset(),simpset() addsimps [hypreal_less_def]));
   801 by (Ultra_tac 1);
   802 qed "hypreal_less_not_refl";
   803 
   804 (*** y < y ==> P ***)
   805 bind_thm("hypreal_less_irrefl",hypreal_less_not_refl RS notE);
   806 
   807 Goal "!!(x::hypreal). x < y ==> x ~= y";
   808 by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
   809 qed "hypreal_not_refl2";
   810 
   811 Goal "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
   812 by (res_inst_tac [("z","R1")] eq_Abs_hypreal 1);
   813 by (res_inst_tac [("z","R2")] eq_Abs_hypreal 1);
   814 by (res_inst_tac [("z","R3")] eq_Abs_hypreal 1);
   815 by (auto_tac (claset() addSIs [exI],simpset() 
   816      addsimps [hypreal_less_def]));
   817 by (ultra_tac (claset() addIs [real_less_trans],simpset()) 1);
   818 qed "hypreal_less_trans";
   819 
   820 Goal "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P";
   821 by (dtac hypreal_less_trans 1 THEN assume_tac 1);
   822 by (asm_full_simp_tac (simpset() addsimps 
   823     [hypreal_less_not_refl]) 1);
   824 qed "hypreal_less_asym";
   825 
   826 (*--------------------------------------------------------
   827   TODO: The following theorem should have been proved 
   828   first and then used througout the proofs as it probably 
   829   makes many of them more straightforward. 
   830  -------------------------------------------------------*)
   831 Goalw [hypreal_less_def]
   832       "(Abs_hypreal(hyprel^^{%n. X n}) < \
   833 \           Abs_hypreal(hyprel^^{%n. Y n})) = \
   834 \      ({n. X n < Y n} : FreeUltrafilterNat)";
   835 by (auto_tac (claset() addSIs [lemma_hyprel_refl],simpset()));
   836 by (Ultra_tac 1);
   837 qed "hypreal_less";
   838 
   839 (*---------------------------------------------------------------------------------
   840              Hyperreals as a linearly ordered field
   841  ---------------------------------------------------------------------------------*)
   842 (*** sum order ***)
   843 
   844 Goalw [hypreal_zero_def] 
   845       "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y";
   846 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   847 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   848 by (auto_tac (claset(),simpset() addsimps
   849     [hypreal_less_def,hypreal_add]));
   850 by (auto_tac (claset() addSIs [exI],simpset() addsimps
   851     [hypreal_less_def,hypreal_add]));
   852 by (ultra_tac (claset() addIs [real_add_order],simpset()) 1);
   853 qed "hypreal_add_order";
   854 
   855 (*** mult order ***)
   856 
   857 Goalw [hypreal_zero_def] 
   858           "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y";
   859 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   860 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   861 by (auto_tac (claset() addSIs [exI],simpset() addsimps
   862     [hypreal_less_def,hypreal_mult]));
   863 by (ultra_tac (claset() addIs [rename_numerals thy real_mult_order],
   864 	       simpset()) 1);
   865 qed "hypreal_mult_order";
   866 
   867 (*---------------------------------------------------------------------------------
   868                          Trichotomy of the hyperreals
   869   --------------------------------------------------------------------------------*)
   870 
   871 Goalw [hyprel_def] "EX x. x: hyprel ^^ {%n. #0}";
   872 by (res_inst_tac [("x","%n. #0")] 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]"0 <  x | x = 0 | x < (0::hypreal)";
   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 "[| (0::hypreal) < x ==> P; \
   893 \                 x = 0 ==> P; \
   894 \                 x < 0 ==> 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) = (0 < 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< 0)";
   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 "0 < 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) = (0 = 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) = (0 = 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 ~= (0::hypreal))";
   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 "[| 0 < x; 0 <= y |] ==> (0::hypreal) < 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 "(0 < -R) = (R < (0::hypreal))";
  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 < 0) = ((0::hypreal) < 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 "((0::hypreal) < 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 < (0::hypreal)) = (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] "((0::hypreal) <= 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 <= (0::hypreal)) = (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 < 0; y < 0 |] ==> (0::hypreal) < 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 "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= 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 <= 0; y <= 0 |] ==> (0::hypreal) <= 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 "[| 0 <= x; y < 0 |] ==> x * y <= (0::hypreal)";
  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 "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)";
  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 1);
  1153 qed "hypreal_mult_less_zero";
  1154 
  1155 Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0 < 1hr";
  1156 by (res_inst_tac [("x","%n. #0")] exI 1);
  1157 by (res_inst_tac [("x","%n. #1")] 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 "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= 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 "(0*x<r)=((0::hypreal)<r)";
  1199 by (Simp_tac 1);
  1200 qed "hypreal_mult_0_less";
  1201 
  1202 Goal "[| (0::hypreal) < 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_mult_commute ]) 1);
  1209 qed "hypreal_mult_less_mono1";
  1210 
  1211 Goal "[| (0::hypreal)<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 "[| (0::hypreal)<=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 "[| (0::hypreal)<=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 "[| (0::hypreal)<=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      "[| (0::hypreal)<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 "[| 0<=y; x<r; y*r<t*s; (0::hypreal)<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 "[| 0 <= y; x <= r; y*r < t*s; (0::hypreal) < 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 "[| 0 < r1; r1 <r2; (0::hypreal) < 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","0")] 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 "[| 0 < r1; r1 <r2; 0 < y|] \
  1255 \                           ==> (0::hypreal) < r2 * y";
  1256 by (dres_inst_tac [("R1.0","0")] 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 "[| 0 < r1; r1 <= r2; (0::hypreal) <= 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 + 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 * 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 "0 < x ==> 0 < 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_zero_less_iff]));
  1317 qed "hypreal_hrinv_gt_zero";
  1318 
  1319 Goal "x < 0 ==> hrinv x < 0";
  1320 by (ftac hypreal_not_refl2 1);
  1321 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
  1322 by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
  1323 by (dtac (hypreal_minus_hrinv RS sym) 1);
  1324 by (auto_tac (claset() addIs [hypreal_hrinv_gt_zero],
  1325     simpset()));
  1326 qed "hypreal_hrinv_less_zero";
  1327 
  1328 Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real  #1 = 1hr";
  1329 by (Step_tac 1);
  1330 qed "hypreal_of_real_one";
  1331 
  1332 Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real  #0 = 0";
  1333 by (Step_tac 1);
  1334 qed "hypreal_of_real_zero";
  1335 
  1336 Goal "(hypreal_of_real  r = 0) = (r = #0)";
  1337 by (auto_tac (claset() addIs [FreeUltrafilterNat_P],
  1338     simpset() addsimps [hypreal_of_real_def,
  1339     hypreal_zero_def,FreeUltrafilterNat_Nat_set]));
  1340 qed "hypreal_of_real_zero_iff";
  1341 
  1342 Goal "(hypreal_of_real  r ~= 0) = (r ~= #0)";
  1343 by (full_simp_tac (simpset() addsimps [hypreal_of_real_zero_iff]) 1);
  1344 qed "hypreal_of_real_not_zero_iff";
  1345 
  1346 Goal "r ~= #0 ==> hrinv (hypreal_of_real r) = \
  1347 \          hypreal_of_real (rinv r)";
  1348 by (res_inst_tac [("c1","hypreal_of_real r")] (hypreal_mult_left_cancel RS iffD1) 1);
  1349 by (etac (hypreal_of_real_not_zero_iff RS iffD2) 1);
  1350 by (forward_tac [hypreal_of_real_not_zero_iff RS iffD2] 1);
  1351 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_mult RS sym,hypreal_of_real_one]));
  1352 qed "hypreal_of_real_hrinv";
  1353 
  1354 Goal "hypreal_of_real r ~= 0 ==> hrinv (hypreal_of_real r) = \
  1355 \          hypreal_of_real (rinv r)";
  1356 by (etac (hypreal_of_real_not_zero_iff RS iffD1 RS hypreal_of_real_hrinv) 1);
  1357 qed "hypreal_of_real_hrinv2";
  1358 
  1359 Goal "x+x=x*(1hr+1hr)";
  1360 by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1);
  1361 qed "hypreal_add_self";
  1362 
  1363 Goal "1hr < 1hr + 1hr";
  1364 by (rtac (hypreal_less_minus_iff RS iffD2) 1);
  1365 by (full_simp_tac (simpset() addsimps [hypreal_zero_less_one,
  1366     hypreal_add_assoc]) 1);
  1367 qed "hypreal_one_less_two";
  1368 
  1369 Goal "0 < 1hr + 1hr";
  1370 by (rtac ([hypreal_zero_less_one,
  1371           hypreal_one_less_two] MRS hypreal_less_trans) 1);
  1372 qed "hypreal_zero_less_two";
  1373 
  1374 Goal "1hr + 1hr ~= 0";
  1375 by (rtac (hypreal_zero_less_two RS hypreal_not_refl2 RS not_sym) 1);
  1376 qed "hypreal_two_not_zero";
  1377 Addsimps [hypreal_two_not_zero];
  1378 
  1379 Goal "x*hrinv(1hr + 1hr) + x*hrinv(1hr + 1hr) = x";
  1380 by (stac hypreal_add_self 1);
  1381 by (full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
  1382 qed "hypreal_sum_of_halves";
  1383 
  1384 Goal "z ~= 0 ==> x*y = (x*hrinv(z))*(z*y)";
  1385 by (asm_simp_tac (simpset() addsimps hypreal_mult_ac)  1);
  1386 qed "lemma_chain";
  1387 
  1388 Goal "0 < r ==> 0 < r*hrinv(1hr+1hr)";
  1389 by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero 
  1390           RS hypreal_mult_less_mono1) 1);
  1391 by Auto_tac;
  1392 qed "hypreal_half_gt_zero";
  1393 
  1394 (* TODO: remove redundant  0 < x *)
  1395 Goal "[| 0 < r; 0 < x; r < x |] ==> hrinv x < hrinv r";
  1396 by (ftac hypreal_hrinv_gt_zero 1);
  1397 by (forw_inst_tac [("x","x")] hypreal_hrinv_gt_zero 1);
  1398 by (forw_inst_tac [("x","r"),("z","hrinv r")] hypreal_mult_less_mono1 1);
  1399 by (assume_tac 1);
  1400 by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS 
  1401          not_sym RS hypreal_mult_hrinv]) 1);
  1402 by (ftac hypreal_hrinv_gt_zero 1);
  1403 by (forw_inst_tac [("x","1hr"),("z","hrinv x")] hypreal_mult_less_mono2 1);
  1404 by (assume_tac 1);
  1405 by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS 
  1406          not_sym RS hypreal_mult_hrinv_left,hypreal_mult_assoc RS sym]) 1);
  1407 qed "hypreal_hrinv_less_swap";
  1408 
  1409 Goal "[| 0 < r; 0 < x|] ==> (r < x) = (hrinv x < hrinv r)";
  1410 by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],simpset()));
  1411 by (res_inst_tac [("t","r")] (hypreal_hrinv_hrinv RS subst) 1);
  1412 by (etac (hypreal_not_refl2 RS not_sym) 1);
  1413 by (res_inst_tac [("t","x")] (hypreal_hrinv_hrinv RS subst) 1);
  1414 by (etac (hypreal_not_refl2 RS not_sym) 1);
  1415 by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],
  1416     simpset() addsimps [hypreal_hrinv_gt_zero]));
  1417 qed "hypreal_hrinv_less_iff";
  1418 
  1419 Goal "[| 0 < z; x < y |] ==> x*hrinv(z) < y*hrinv(z)";
  1420 by (blast_tac (claset() addSIs [hypreal_mult_less_mono1,
  1421     hypreal_hrinv_gt_zero]) 1);
  1422 qed "hypreal_mult_hrinv_less_mono1";
  1423 
  1424 Goal "[| 0 < z; x < y |] ==> hrinv(z)*x < hrinv(z)*y";
  1425 by (blast_tac (claset() addSIs [hypreal_mult_less_mono2,
  1426     hypreal_hrinv_gt_zero]) 1);
  1427 qed "hypreal_mult_hrinv_less_mono2";
  1428 
  1429 Goal "[| (0::hypreal) < z; x*z < y*z |] ==> x < y";
  1430 by (forw_inst_tac [("x","x*z")] hypreal_mult_hrinv_less_mono1 1);
  1431 by (dtac (hypreal_not_refl2 RS not_sym) 2);
  1432 by (auto_tac (claset() addSDs [hypreal_mult_hrinv],
  1433               simpset() addsimps hypreal_mult_ac));
  1434 qed "hypreal_less_mult_right_cancel";
  1435 
  1436 Goal "[| (0::hypreal) < z; z*x < z*y |] ==> x < y";
  1437 by (auto_tac (claset() addIs [hypreal_less_mult_right_cancel],
  1438     simpset() addsimps [hypreal_mult_commute]));
  1439 qed "hypreal_less_mult_left_cancel";
  1440 
  1441 Goal "[| 0 < r; (0::hypreal) < ra; \
  1442 \                 r < x; ra < y |] \
  1443 \              ==> r*ra < x*y";
  1444 by (forw_inst_tac [("R2.0","r")] hypreal_less_trans 1);
  1445 by (dres_inst_tac [("z","ra"),("x","r")] hypreal_mult_less_mono1 2);
  1446 by (dres_inst_tac [("z","x"),("x","ra")] hypreal_mult_less_mono2 3);
  1447 by (auto_tac (claset() addIs [hypreal_less_trans],simpset()));
  1448 qed "hypreal_mult_less_gt_zero"; 
  1449 
  1450 Goal "[| 0 < r; (0::hypreal) < ra; \
  1451 \                 r <= x; ra <= y |] \
  1452 \              ==> r*ra <= x*y";
  1453 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
  1454 by (rtac hypreal_less_or_eq_imp_le 1);
  1455 by (auto_tac (claset() addIs [hypreal_mult_less_mono1,
  1456     hypreal_mult_less_mono2,hypreal_mult_less_gt_zero],
  1457     simpset()));
  1458 qed "hypreal_mult_le_ge_zero"; 
  1459 
  1460 Goal "EX (x::hypreal). x < y";
  1461 by (rtac (hypreal_add_zero_right RS subst) 1);
  1462 by (res_inst_tac [("x","y + -1hr")] exI 1);
  1463 by (auto_tac (claset() addSIs [hypreal_add_less_mono2],
  1464     simpset() addsimps [hypreal_minus_zero_less_iff2,
  1465     hypreal_zero_less_one] delsimps [hypreal_add_zero_right]));
  1466 qed "hypreal_less_Ex";
  1467 
  1468 Goal "!!(A::hypreal). A + C < B + C ==> A < B";
  1469 by (dres_inst_tac [("C","-C")] hypreal_add_less_mono1 1);
  1470 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
  1471 qed "hypreal_less_add_right_cancel";
  1472 
  1473 Goal "!!(A::hypreal). C + A < C + B ==> A < B";
  1474 by (dres_inst_tac [("C","-C")] hypreal_add_less_mono2 1);
  1475 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
  1476 qed "hypreal_less_add_left_cancel";
  1477 
  1478 Goal "(0::hypreal) <= x*x";
  1479 by (res_inst_tac [("x","0"),("y","x")] hypreal_linear_less2 1);
  1480 by (auto_tac (claset() addIs [hypreal_mult_order,
  1481     hypreal_mult_less_zero1,hypreal_less_imp_le],
  1482     simpset()));
  1483 qed "hypreal_le_square";
  1484 Addsimps [hypreal_le_square];
  1485 
  1486 Goalw [hypreal_le_def] "- (x*x) <= (0::hypreal)";
  1487 by (auto_tac (claset() addSDs [(hypreal_le_square RS 
  1488     hypreal_le_less_trans)],simpset() addsimps 
  1489     [hypreal_minus_zero_less_iff,hypreal_less_not_refl]));
  1490 qed "hypreal_less_minus_square";
  1491 Addsimps [hypreal_less_minus_square];
  1492 
  1493 Goal "[|x ~= 0; y ~= 0 |] ==> \
  1494 \                   hrinv(x) + hrinv(y) = (x + y)*hrinv(x*y)";
  1495 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv_distrib,
  1496              hypreal_add_mult_distrib,hypreal_mult_assoc RS sym]) 1);
  1497 by (stac hypreal_mult_assoc 1);
  1498 by (rtac (hypreal_mult_left_commute RS subst) 1);
  1499 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
  1500 qed "hypreal_hrinv_add";
  1501 
  1502 Goal "x = -x ==> x = (0::hypreal)";
  1503 by (dtac (hypreal_eq_minus_iff RS iffD1 RS sym) 1);
  1504 by (Asm_full_simp_tac 1);
  1505 by (dtac (hypreal_add_self RS subst) 1);
  1506 by (rtac ccontr 1);
  1507 by (blast_tac (claset() addDs [hypreal_two_not_zero RSN
  1508                (2,hypreal_mult_not_0)]) 1);
  1509 qed "hypreal_self_eq_minus_self_zero";
  1510 
  1511 Goal "(x + x = 0) = (x = (0::hypreal))";
  1512 by Auto_tac;
  1513 by (dtac (hypreal_add_self RS subst) 1);
  1514 by (rtac ccontr 1 THEN rtac hypreal_mult_not_0E 1);
  1515 by Auto_tac;
  1516 qed "hypreal_add_self_zero_cancel";
  1517 Addsimps [hypreal_add_self_zero_cancel];
  1518 
  1519 Goal "(x + x + y = y) = (x = (0::hypreal))";
  1520 by Auto_tac;
  1521 by (dtac (hypreal_eq_minus_iff RS iffD1) 1 THEN dtac sym 1);
  1522 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
  1523 qed "hypreal_add_self_zero_cancel2";
  1524 Addsimps [hypreal_add_self_zero_cancel2];
  1525 
  1526 Goal "(x + (x + y) = y) = (x = (0::hypreal))";
  1527 by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
  1528 qed "hypreal_add_self_zero_cancel2a";
  1529 Addsimps [hypreal_add_self_zero_cancel2a];
  1530 
  1531 Goal "(b = -a) = (-b = (a::hypreal))";
  1532 by Auto_tac;
  1533 qed "hypreal_minus_eq_swap";
  1534 
  1535 Goal "(-b = -a) = (b = (a::hypreal))";
  1536 by (asm_full_simp_tac (simpset() addsimps 
  1537     [hypreal_minus_eq_swap]) 1);
  1538 qed "hypreal_minus_eq_cancel";
  1539 Addsimps [hypreal_minus_eq_cancel];
  1540 
  1541 Goal "x < x + 1hr";
  1542 by (cut_inst_tac [("C","x")] 
  1543     (hypreal_zero_less_one RS hypreal_add_less_mono2) 1);
  1544 by (Asm_full_simp_tac 1);
  1545 qed "hypreal_less_self_add_one";
  1546 Addsimps [hypreal_less_self_add_one];
  1547 
  1548 Goal "((x::hypreal) + x = y + y) = (x = y)";
  1549 by (auto_tac (claset() addIs [hypreal_two_not_zero RS 
  1550      hypreal_mult_left_cancel RS iffD1],simpset() addsimps 
  1551      [hypreal_add_mult_distrib]));
  1552 qed "hypreal_add_self_cancel";
  1553 Addsimps [hypreal_add_self_cancel];
  1554 
  1555 Goal "(y = x + - y + x) = (y = (x::hypreal))";
  1556 by Auto_tac;
  1557 by (dres_inst_tac [("x1","y")] 
  1558     (hypreal_add_right_cancel RS iffD2) 1);
  1559 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
  1560 qed "hypreal_add_self_minus_cancel";
  1561 Addsimps [hypreal_add_self_minus_cancel];
  1562 
  1563 Goal "(y = x + (- y + x)) = (y = (x::hypreal))";
  1564 by (asm_full_simp_tac (simpset() addsimps 
  1565          [hypreal_add_assoc RS sym])1);
  1566 qed "hypreal_add_self_minus_cancel2";
  1567 Addsimps [hypreal_add_self_minus_cancel2];
  1568 
  1569 Goal "z + -x = y + (y + (-x + -z)) = (y = (z::hypreal))";
  1570 by Auto_tac;
  1571 by (dres_inst_tac [("x1","z")] 
  1572     (hypreal_add_right_cancel RS iffD2) 1);
  1573 by (asm_full_simp_tac (simpset() addsimps 
  1574     [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac) 1);
  1575 by (asm_full_simp_tac (simpset() addsimps 
  1576      [hypreal_add_assoc RS sym,hypreal_add_right_cancel]) 1);
  1577 qed "hypreal_add_self_minus_cancel3";
  1578 Addsimps [hypreal_add_self_minus_cancel3];
  1579 
  1580 (* check why this does not work without 2nd substiution anymore! *)
  1581 Goal "x < y ==> x < (x + y)*hrinv(1hr + 1hr)";
  1582 by (dres_inst_tac [("C","x")] hypreal_add_less_mono2 1);
  1583 by (dtac (hypreal_add_self RS subst) 1);
  1584 by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS 
  1585           hypreal_mult_less_mono1) 1);
  1586 by (auto_tac (claset() addDs [hypreal_two_not_zero RS 
  1587           (hypreal_mult_hrinv RS subst)],simpset() 
  1588           addsimps [hypreal_mult_assoc]));
  1589 qed "hypreal_less_half_sum";
  1590 
  1591 (* check why this does not work without 2nd substiution anymore! *)
  1592 Goal "x < y ==> (x + y)*hrinv(1hr + 1hr) < y";
  1593 by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 1);
  1594 by (dtac (hypreal_add_self RS subst) 1);
  1595 by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS 
  1596           hypreal_mult_less_mono1) 1);
  1597 by (auto_tac (claset() addDs [hypreal_two_not_zero RS 
  1598           (hypreal_mult_hrinv RS subst)],simpset() 
  1599           addsimps [hypreal_mult_assoc]));
  1600 qed "hypreal_gt_half_sum";
  1601 
  1602 Goal "!!(x::hypreal). x < y ==> EX r. x < r & r < y";
  1603 by (blast_tac (claset() addSIs [hypreal_less_half_sum,
  1604     hypreal_gt_half_sum]) 1);
  1605 qed "hypreal_dense";
  1606 
  1607 Goal "(x * x = 0) = (x = (0::hypreal))";
  1608 by Auto_tac;
  1609 by (blast_tac (claset() addIs [hypreal_mult_not_0E]) 1);
  1610 qed "hypreal_mult_self_eq_zero_iff";
  1611 Addsimps [hypreal_mult_self_eq_zero_iff];
  1612 
  1613 Goal "(0 = x * x) = (x = (0::hypreal))";
  1614 by (auto_tac (claset() addDs [sym],simpset()));
  1615 qed "hypreal_mult_self_eq_zero_iff2";
  1616 Addsimps [hypreal_mult_self_eq_zero_iff2];
  1617 
  1618 Goal "(x*x + y*y = 0) = (x = 0 & y = (0::hypreal))";
  1619 by Auto_tac;
  1620 by (dtac (sym RS (hypreal_eq_minus_iff3 RS iffD1))  1);
  1621 by (dtac (sym RS (hypreal_eq_minus_iff4 RS iffD1))  2);
  1622 by (ALLGOALS(rtac ccontr));
  1623 by (ALLGOALS(dtac hypreal_mult_self_not_zero));
  1624 by (cut_inst_tac [("x1","x")] (hypreal_le_square 
  1625         RS hypreal_le_imp_less_or_eq) 1);
  1626 by (cut_inst_tac [("x1","y")] (hypreal_le_square 
  1627         RS hypreal_le_imp_less_or_eq) 2);
  1628 by (auto_tac (claset() addDs [sym],simpset()));
  1629 by (dres_inst_tac [("x1","y")] (hypreal_less_minus_square 
  1630     RS hypreal_le_less_trans) 1);
  1631 by (dres_inst_tac [("x1","x")] (hypreal_less_minus_square 
  1632     RS hypreal_le_less_trans) 2);
  1633 by (auto_tac (claset(),simpset() addsimps 
  1634        [hypreal_less_not_refl]));
  1635 qed "hypreal_squares_add_zero_iff";
  1636 Addsimps [hypreal_squares_add_zero_iff];
  1637 
  1638 Goal "x * x ~= 0 ==> (0::hypreal) < x* x + y*y + z*z";
  1639 by (cut_inst_tac [("x1","x")] (hypreal_le_square 
  1640         RS hypreal_le_imp_less_or_eq) 1);
  1641 by (auto_tac (claset() addSIs 
  1642               [hypreal_add_order_le],simpset()));
  1643 qed "hypreal_sum_squares3_gt_zero";
  1644 
  1645 Goal "x * x ~= 0 ==> (0::hypreal) < y*y + x*x + z*z";
  1646 by (dtac hypreal_sum_squares3_gt_zero 1);
  1647 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
  1648 qed "hypreal_sum_squares3_gt_zero2";
  1649 
  1650 Goal "x * x ~= 0 ==> (0::hypreal) < y*y + z*z + x*x";
  1651 by (dtac hypreal_sum_squares3_gt_zero 1);
  1652 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
  1653 qed "hypreal_sum_squares3_gt_zero3";
  1654 
  1655 Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))";
  1656 by Auto_tac;
  1657 by (ALLGOALS(rtac ccontr));
  1658 by (ALLGOALS(dtac hypreal_mult_self_not_zero));
  1659 by (auto_tac (claset() addDs [hypreal_not_refl2 RS not_sym,
  1660    hypreal_sum_squares3_gt_zero3,hypreal_sum_squares3_gt_zero,
  1661    hypreal_sum_squares3_gt_zero2],simpset() delsimps
  1662    [hypreal_mult_self_eq_zero_iff]));
  1663 qed "hypreal_three_squares_add_zero_iff";
  1664 Addsimps [hypreal_three_squares_add_zero_iff];
  1665 
  1666 Addsimps [rename_numerals thy real_le_square];
  1667 Goal "(x::hypreal)*x <= x*x + y*y";
  1668 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  1669 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
  1670 by (auto_tac (claset(),simpset() addsimps 
  1671     [hypreal_mult,hypreal_add,hypreal_le]));
  1672 qed "hypreal_self_le_add_pos";
  1673 Addsimps [hypreal_self_le_add_pos];
  1674 
  1675 Goal "(x::hypreal)*x <= x*x + y*y + z*z";
  1676 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  1677 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
  1678 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
  1679 by (auto_tac (claset(),
  1680 	      simpset() addsimps [hypreal_mult, hypreal_add, hypreal_le,
  1681 				  rename_numerals thy real_le_add_order]));
  1682 qed "hypreal_self_le_add_pos2";
  1683 Addsimps [hypreal_self_le_add_pos2];
  1684 
  1685 (*---------------------------------------------------------------------------------
  1686              Embedding of the naturals in the hyperreals
  1687  ---------------------------------------------------------------------------------*)
  1688 Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 0 = 1hr";
  1689 by (full_simp_tac (simpset() addsimps 
  1690     [pnat_one_iff RS sym,real_of_preal_def]) 1);
  1691 by (fold_tac [real_one_def]);
  1692 by (simp_tac (simpset() addsimps [hypreal_of_real_one]) 1);
  1693 qed "hypreal_of_posnat_one";
  1694 
  1695 Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr";
  1696 by (full_simp_tac (simpset() addsimps 
  1697 		   [real_of_preal_def,
  1698 		    rename_numerals thy (real_one_def RS meta_eq_to_obj_eq),
  1699 		    hypreal_add,hypreal_of_real_def,pnat_two_eq,
  1700 		    hypreal_one_def, real_add,
  1701 		    prat_of_pnat_add RS sym, preal_of_prat_add RS sym] @ 
  1702 		    pnat_add_ac) 1);
  1703 qed "hypreal_of_posnat_two";
  1704 
  1705 Goalw [hypreal_of_posnat_def]
  1706           "hypreal_of_posnat n1 + hypreal_of_posnat n2 = \
  1707 \          hypreal_of_posnat (n1 + n2) + 1hr";
  1708 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one RS sym,
  1709     hypreal_of_real_add RS sym,hypreal_of_posnat_def,real_of_preal_add RS sym,
  1710     preal_of_prat_add RS sym,prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
  1711 qed "hypreal_of_posnat_add";
  1712 
  1713 Goal "hypreal_of_posnat (n + 1) = hypreal_of_posnat n + 1hr";
  1714 by (res_inst_tac [("x1","1hr")] (hypreal_add_right_cancel RS iffD1) 1);
  1715 by (rtac (hypreal_of_posnat_add RS subst) 1);
  1716 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,hypreal_add_assoc]) 1);
  1717 qed "hypreal_of_posnat_add_one";
  1718 
  1719 Goalw [real_of_posnat_def,hypreal_of_posnat_def] 
  1720       "hypreal_of_posnat n = hypreal_of_real (real_of_posnat n)";
  1721 by (rtac refl 1);
  1722 qed "hypreal_of_real_of_posnat";
  1723 
  1724 Goalw [hypreal_of_posnat_def] 
  1725       "(n < m) = (hypreal_of_posnat n < hypreal_of_posnat m)";
  1726 by Auto_tac;
  1727 qed "hypreal_of_posnat_less_iff";
  1728 
  1729 Addsimps [hypreal_of_posnat_less_iff RS sym];
  1730 (*---------------------------------------------------------------------------------
  1731                Existence of infinite hyperreal number
  1732  ---------------------------------------------------------------------------------*)
  1733 
  1734 Goal "hyprel^^{%n::nat. real_of_posnat n} : hypreal";
  1735 by Auto_tac;
  1736 qed "hypreal_omega";
  1737 
  1738 Goalw [omega_def] "Rep_hypreal(whr) : hypreal";
  1739 by (rtac Rep_hypreal 1);
  1740 qed "Rep_hypreal_omega";
  1741 
  1742 (* existence of infinite number not corresponding to any real number *)
  1743 (* use assumption that member FreeUltrafilterNat is not finite       *)
  1744 (* a few lemmas first *)
  1745 
  1746 Goal "{n::nat. x = real_of_posnat n} = {} | \
  1747 \     (EX y. {n::nat. x = real_of_posnat n} = {y})";
  1748 by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],simpset()));
  1749 qed "lemma_omega_empty_singleton_disj";
  1750 
  1751 Goal "finite {n::nat. x = real_of_posnat n}";
  1752 by (cut_inst_tac [("x","x")] lemma_omega_empty_singleton_disj 1);
  1753 by Auto_tac;
  1754 qed "lemma_finite_omega_set";
  1755 
  1756 Goalw [omega_def,hypreal_of_real_def] 
  1757       "~ (EX x. hypreal_of_real x = whr)";
  1758 by (auto_tac (claset(),simpset() addsimps [lemma_finite_omega_set 
  1759     RS FreeUltrafilterNat_finite]));
  1760 qed "not_ex_hypreal_of_real_eq_omega";
  1761 
  1762 Goal "hypreal_of_real x ~= whr";
  1763 by (cut_facts_tac [not_ex_hypreal_of_real_eq_omega] 1);
  1764 by Auto_tac;
  1765 qed "hypreal_of_real_not_eq_omega";
  1766 
  1767 (* existence of infinitesimal number also not *)
  1768 (* corresponding to any real number *)
  1769 
  1770 Goal "{n::nat. x = rinv(real_of_posnat n)} = {} | \
  1771 \     (EX y. {n::nat. x = rinv(real_of_posnat n)} = {y})";
  1772 by (Step_tac 1 THEN Step_tac 1);
  1773 by (auto_tac (claset() addIs [real_of_posnat_rinv_inj],simpset()));
  1774 qed "lemma_epsilon_empty_singleton_disj";
  1775 
  1776 Goal "finite {n::nat. x = rinv(real_of_posnat n)}";
  1777 by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1);
  1778 by Auto_tac;
  1779 qed "lemma_finite_epsilon_set";
  1780 
  1781 Goalw [epsilon_def,hypreal_of_real_def] 
  1782       "~ (EX x. hypreal_of_real x = ehr)";
  1783 by (auto_tac (claset(),simpset() addsimps [lemma_finite_epsilon_set 
  1784     RS FreeUltrafilterNat_finite]));
  1785 qed "not_ex_hypreal_of_real_eq_epsilon";
  1786 
  1787 Goal "hypreal_of_real x ~= ehr";
  1788 by (cut_facts_tac [not_ex_hypreal_of_real_eq_epsilon] 1);
  1789 by Auto_tac;
  1790 qed "hypreal_of_real_not_eq_epsilon";
  1791 
  1792 Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0";
  1793 by (auto_tac (claset(),
  1794      simpset() addsimps [rename_numerals thy real_of_posnat_rinv_not_zero]));
  1795 qed "hypreal_epsilon_not_zero";
  1796 
  1797 Addsimps [rename_numerals thy real_of_posnat_not_eq_zero];
  1798 Goalw [omega_def,hypreal_zero_def] "whr ~= 0";
  1799 by (Simp_tac 1);
  1800 qed "hypreal_omega_not_zero";
  1801 
  1802 Goal "ehr = hrinv(whr)";
  1803 by (asm_full_simp_tac (simpset() addsimps 
  1804     [hypreal_hrinv,omega_def,epsilon_def]
  1805     setloop (split_tac [expand_if])) 1);
  1806 qed "hypreal_epsilon_hrinv_omega";
  1807 
  1808 (*----------------------------------------------------------------
  1809      Another embedding of the naturals in the 
  1810     hyperreals (see hypreal_of_posnat)
  1811  ----------------------------------------------------------------*)
  1812 Goalw [hypreal_of_nat_def] "hypreal_of_nat 0 = 0";
  1813 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one]) 1);
  1814 qed "hypreal_of_nat_zero";
  1815 
  1816 Goalw [hypreal_of_nat_def] "hypreal_of_nat 1 = 1hr";
  1817 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,
  1818     hypreal_add_assoc]) 1);
  1819 qed "hypreal_of_nat_one";
  1820 
  1821 Goalw [hypreal_of_nat_def]
  1822       "hypreal_of_nat n1 + hypreal_of_nat n2 = \
  1823 \      hypreal_of_nat (n1 + n2)";
  1824 by (full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
  1825 by (simp_tac (simpset() addsimps [hypreal_of_posnat_add,
  1826     hypreal_add_assoc RS sym]) 1);
  1827 by (rtac (hypreal_add_commute RS subst) 1);
  1828 by (simp_tac (simpset() addsimps [hypreal_add_left_cancel,
  1829     hypreal_add_assoc]) 1);
  1830 qed "hypreal_of_nat_add";
  1831 
  1832 Goal "hypreal_of_nat 2 = 1hr + 1hr";
  1833 by (simp_tac (simpset() addsimps [hypreal_of_nat_one 
  1834     RS sym,hypreal_of_nat_add]) 1);
  1835 qed "hypreal_of_nat_two";
  1836 
  1837 Goalw [hypreal_of_nat_def] 
  1838       "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)";
  1839 by (auto_tac (claset() addIs [hypreal_add_less_mono1],simpset()));
  1840 by (dres_inst_tac [("C","1hr")] hypreal_add_less_mono1 1);
  1841 by (full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
  1842 qed "hypreal_of_nat_less_iff";
  1843 Addsimps [hypreal_of_nat_less_iff RS sym];
  1844 
  1845 (* naturals embedded in hyperreals is an hyperreal *)
  1846 Goalw [hypreal_of_nat_def,real_of_nat_def] 
  1847       "hypreal_of_nat  m = Abs_hypreal(hyprel^^{%n. real_of_nat m})";
  1848 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def,
  1849     hypreal_of_real_of_posnat,hypreal_minus,hypreal_one_def,hypreal_add]));
  1850 qed "hypreal_of_nat_iff";
  1851 
  1852 Goal "inj hypreal_of_nat";
  1853 by (rtac injI 1);
  1854 by (auto_tac (claset() addSDs [FreeUltrafilterNat_P],
  1855         simpset() addsimps [split_if_mem1, hypreal_of_nat_iff,
  1856         real_add_right_cancel,inj_real_of_nat RS injD]));
  1857 qed "inj_hypreal_of_nat";
  1858 
  1859 Goalw [hypreal_of_nat_def,hypreal_of_real_def,hypreal_of_posnat_def,
  1860        real_of_posnat_def,hypreal_one_def,real_of_nat_def] 
  1861        "hypreal_of_nat n = hypreal_of_real (real_of_nat n)";
  1862 by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1);
  1863 qed "hypreal_of_nat_real_of_nat";