src/HOL/Real/Hyperreal/HyperDef.ML
author fleuriot
Thu Jun 01 11:22:27 2000 +0200 (2000-06-01)
changeset 9013 9dd0274f76af
parent 8856 435187ffc64e
child 9043 ca761fe227d8
permissions -rw-r--r--
Updated files to remove 0r and 1r from theorems in descendant theories
of RealBin. Some new theorems added.
     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 = #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 ~= 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 (map (full_rename_numerals thy)
   351     [rinv_not_zero,real_rinv_rinv]),simpset()) 1);
   352 qed "hypreal_hrinv_hrinv";
   353 
   354 Addsimps [hypreal_hrinv_hrinv];
   355 
   356 Goalw [hypreal_one_def] "hrinv(1hr) = 1hr";
   357 by (full_simp_tac (simpset() addsimps [hypreal_hrinv,
   358        real_zero_not_eq_one RS not_sym] 
   359                    setloop (split_tac [expand_if])) 1);
   360 qed "hypreal_hrinv_1";
   361 Addsimps [hypreal_hrinv_1];
   362 
   363 (**** hyperreal addition: hypreal_add  ****)
   364 
   365 Goalw [congruent2_def]
   366     "congruent2 hyprel (%X Y. hyprel^^{%n. X n + Y n})";
   367 by Safe_tac;
   368 by (ALLGOALS(Ultra_tac));
   369 qed "hypreal_add_congruent2";
   370 
   371 (*Resolve th against the corresponding facts for hyppreal_add*)
   372 val hypreal_add_ize = RSLIST [equiv_hyprel, hypreal_add_congruent2];
   373 
   374 Goalw [hypreal_add_def]
   375   "Abs_hypreal(hyprel^^{%n. X n}) + Abs_hypreal(hyprel^^{%n. Y n}) = \
   376 \  Abs_hypreal(hyprel^^{%n. X n + Y n})";
   377 by (asm_simp_tac
   378     (simpset() addsimps [hypreal_add_ize UN_equiv_class2]) 1);
   379 qed "hypreal_add";
   380 
   381 Goal "(z::hypreal) + w = w + z";
   382 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   383 by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
   384 by (asm_simp_tac (simpset() addsimps (real_add_ac @ [hypreal_add])) 1);
   385 qed "hypreal_add_commute";
   386 
   387 Goal "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)";
   388 by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
   389 by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
   390 by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
   391 by (asm_simp_tac (simpset() addsimps [hypreal_add, real_add_assoc]) 1);
   392 qed "hypreal_add_assoc";
   393 
   394 (*For AC rewriting*)
   395 Goal "(x::hypreal)+(y+z)=y+(x+z)";
   396 by (rtac (hypreal_add_commute RS trans) 1);
   397 by (rtac (hypreal_add_assoc RS trans) 1);
   398 by (rtac (hypreal_add_commute RS arg_cong) 1);
   399 qed "hypreal_add_left_commute";
   400 
   401 (* hypreal addition is an AC operator *)
   402 val hypreal_add_ac = [hypreal_add_assoc,hypreal_add_commute,
   403                       hypreal_add_left_commute];
   404 
   405 Goalw [hypreal_zero_def] "0hr + z = z";
   406 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   407 by (asm_full_simp_tac (simpset() addsimps 
   408     [hypreal_add]) 1);
   409 qed "hypreal_add_zero_left";
   410 
   411 Goal "z + 0hr = z";
   412 by (simp_tac (simpset() addsimps 
   413     [hypreal_add_zero_left,hypreal_add_commute]) 1);
   414 qed "hypreal_add_zero_right";
   415 
   416 Goalw [hypreal_zero_def] "z + -z = 0hr";
   417 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   418 by (asm_full_simp_tac (simpset() addsimps [hypreal_minus,
   419         hypreal_add]) 1);
   420 qed "hypreal_add_minus";
   421 
   422 Goal "-z + z = 0hr";
   423 by (simp_tac (simpset() addsimps 
   424     [hypreal_add_commute,hypreal_add_minus]) 1);
   425 qed "hypreal_add_minus_left";
   426 
   427 Addsimps [hypreal_add_minus,hypreal_add_minus_left,
   428           hypreal_add_zero_left,hypreal_add_zero_right];
   429 
   430 Goal "? y. (x::hypreal) + y = 0hr";
   431 by (fast_tac (claset() addIs [hypreal_add_minus]) 1);
   432 qed "hypreal_minus_ex";
   433 
   434 Goal "?! y. (x::hypreal) + y = 0hr";
   435 by (auto_tac (claset() addIs [hypreal_add_minus],simpset()));
   436 by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
   437 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   438 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   439 qed "hypreal_minus_ex1";
   440 
   441 Goal "?! y. y + (x::hypreal) = 0hr";
   442 by (auto_tac (claset() addIs [hypreal_add_minus_left],simpset()));
   443 by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
   444 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
   445 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   446 qed "hypreal_minus_left_ex1";
   447 
   448 Goal "x + y = 0hr ==> x = -y";
   449 by (cut_inst_tac [("z","y")] hypreal_add_minus_left 1);
   450 by (res_inst_tac [("x1","y")] (hypreal_minus_left_ex1 RS ex1E) 1);
   451 by (Blast_tac 1);
   452 qed "hypreal_add_minus_eq_minus";
   453 
   454 Goal "? y::hypreal. x = -y";
   455 by (cut_inst_tac [("x","x")] hypreal_minus_ex 1);
   456 by (etac exE 1 THEN dtac hypreal_add_minus_eq_minus 1);
   457 by (Fast_tac 1);
   458 qed "hypreal_as_add_inverse_ex";
   459 
   460 Goal "-(x + (y::hypreal)) = -x + -y";
   461 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   462 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   463 by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
   464     hypreal_add,real_minus_add_distrib]));
   465 qed "hypreal_minus_add_distrib";
   466 
   467 Goal "-(y + -(x::hypreal)) = x + -y";
   468 by (simp_tac (simpset() addsimps [hypreal_minus_add_distrib,
   469     hypreal_add_commute]) 1);
   470 qed "hypreal_minus_distrib1";
   471 
   472 Goal "(x + - (y::hypreal)) + (y + - z) = x + -z";
   473 by (res_inst_tac [("w1","y")] (hypreal_add_commute RS subst) 1);
   474 by (simp_tac (simpset() addsimps [hypreal_add_left_commute,
   475     hypreal_add_assoc]) 1);
   476 by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   477 qed "hypreal_add_minus_cancel1";
   478 
   479 Goal "((x::hypreal) + y = x + z) = (y = z)";
   480 by (Step_tac 1);
   481 by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1);
   482 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   483 qed "hypreal_add_left_cancel";
   484 
   485 Goal "z + (x + (y + -z)) = x + (y::hypreal)";
   486 by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
   487 qed "hypreal_add_minus_cancel2";
   488 Addsimps [hypreal_add_minus_cancel2];
   489 
   490 Goal "y + -(x + y) = -(x::hypreal)";
   491 by (full_simp_tac (simpset() addsimps [hypreal_minus_add_distrib]) 1);
   492 by (rtac (hypreal_add_left_commute RS subst) 1);
   493 by (Full_simp_tac 1);
   494 qed "hypreal_add_minus_cancel";
   495 Addsimps [hypreal_add_minus_cancel];
   496 
   497 Goal "y + -(y + x) = -(x::hypreal)";
   498 by (simp_tac (simpset() addsimps [hypreal_minus_add_distrib,
   499               hypreal_add_assoc RS sym]) 1);
   500 qed "hypreal_add_minus_cancelc";
   501 Addsimps [hypreal_add_minus_cancelc];
   502 
   503 Goal "(z + -x) + (y + -z) = (y + -(x::hypreal))";
   504 by (full_simp_tac (simpset() addsimps [hypreal_minus_add_distrib
   505     RS sym, hypreal_add_left_cancel] @ hypreal_add_ac) 1); 
   506 qed "hypreal_add_minus_cancel3";
   507 Addsimps [hypreal_add_minus_cancel3];
   508 
   509 Goal "(y + (x::hypreal)= z + x) = (y = z)";
   510 by (simp_tac (simpset() addsimps [hypreal_add_commute,
   511     hypreal_add_left_cancel]) 1);
   512 qed "hypreal_add_right_cancel";
   513 
   514 Goal "z + (y + -z) = (y::hypreal)";
   515 by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
   516 qed "hypreal_add_minus_cancel4";
   517 Addsimps [hypreal_add_minus_cancel4];
   518 
   519 Goal "z + (w + (x + (-z + y))) = w + x + (y::hypreal)";
   520 by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
   521 qed "hypreal_add_minus_cancel5";
   522 Addsimps [hypreal_add_minus_cancel5];
   523 
   524 
   525 (**** hyperreal multiplication: hypreal_mult  ****)
   526 
   527 Goalw [congruent2_def]
   528     "congruent2 hyprel (%X Y. hyprel^^{%n. X n * Y n})";
   529 by Safe_tac;
   530 by (ALLGOALS(Ultra_tac));
   531 qed "hypreal_mult_congruent2";
   532 
   533 (*Resolve th against the corresponding facts for hypreal_mult*)
   534 val hypreal_mult_ize = RSLIST [equiv_hyprel, hypreal_mult_congruent2];
   535 
   536 Goalw [hypreal_mult_def]
   537   "Abs_hypreal(hyprel^^{%n. X n}) * Abs_hypreal(hyprel^^{%n. Y n}) = \
   538 \  Abs_hypreal(hyprel^^{%n. X n * Y n})";
   539 by (asm_simp_tac
   540     (simpset() addsimps [hypreal_mult_ize UN_equiv_class2]) 1);
   541 qed "hypreal_mult";
   542 
   543 Goal "(z::hypreal) * w = w * z";
   544 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   545 by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
   546 by (asm_simp_tac (simpset() addsimps ([hypreal_mult] @ real_mult_ac)) 1);
   547 qed "hypreal_mult_commute";
   548 
   549 Goal "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)";
   550 by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
   551 by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
   552 by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
   553 by (asm_simp_tac (simpset() addsimps [hypreal_mult,real_mult_assoc]) 1);
   554 qed "hypreal_mult_assoc";
   555 
   556 qed_goal "hypreal_mult_left_commute" thy
   557     "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)"
   558  (fn _ => [rtac (hypreal_mult_commute RS trans) 1, rtac (hypreal_mult_assoc RS trans) 1,
   559            rtac (hypreal_mult_commute RS arg_cong) 1]);
   560 
   561 (* hypreal multiplication is an AC operator *)
   562 val hypreal_mult_ac = [hypreal_mult_assoc, hypreal_mult_commute, 
   563                        hypreal_mult_left_commute];
   564 
   565 Goalw [hypreal_one_def] "1hr * z = z";
   566 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   567 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult]) 1);
   568 qed "hypreal_mult_1";
   569 
   570 Goal "z * 1hr = z";
   571 by (simp_tac (simpset() addsimps [hypreal_mult_commute,
   572     hypreal_mult_1]) 1);
   573 qed "hypreal_mult_1_right";
   574 
   575 Goalw [hypreal_zero_def] "0hr * z = 0hr";
   576 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   577 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult,real_mult_0]) 1);
   578 qed "hypreal_mult_0";
   579 
   580 Goal "z * 0hr = 0hr";
   581 by (simp_tac (simpset() addsimps [hypreal_mult_commute,
   582     hypreal_mult_0]) 1);
   583 qed "hypreal_mult_0_right";
   584 
   585 Addsimps [hypreal_mult_0,hypreal_mult_0_right];
   586 
   587 Goal "-(x * y) = -x * (y::hypreal)";
   588 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   589 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   590 by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
   591     hypreal_mult,real_minus_mult_eq1] 
   592       @ real_mult_ac @ real_add_ac));
   593 qed "hypreal_minus_mult_eq1";
   594 
   595 Goal "-(x * y) = (x::hypreal) * -y";
   596 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   597 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   598 by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
   599    hypreal_mult,real_minus_mult_eq2] 
   600     @ real_mult_ac @ real_add_ac));
   601 qed "hypreal_minus_mult_eq2";
   602 
   603 Goal "-x*-y = x*(y::hypreal)";
   604 by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym,
   605     hypreal_minus_mult_eq1 RS sym]) 1);
   606 qed "hypreal_minus_mult_cancel";
   607 
   608 Addsimps [hypreal_minus_mult_cancel];
   609 
   610 Goal "-x*y = (x::hypreal)*-y";
   611 by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym,
   612     hypreal_minus_mult_eq1 RS sym]) 1);
   613 qed "hypreal_minus_mult_commute";
   614 
   615 
   616 (*-----------------------------------------------------------------------------
   617     A few more theorems
   618  ----------------------------------------------------------------------------*)
   619 Goal "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
   620 by (asm_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   621 qed "hypreal_add_assoc_cong";
   622 
   623 Goal "(z::hypreal) + (v + w) = v + (z + w)";
   624 by (REPEAT (ares_tac [hypreal_add_commute RS hypreal_add_assoc_cong] 1));
   625 qed "hypreal_add_assoc_swap";
   626 
   627 Goal "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)";
   628 by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
   629 by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
   630 by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
   631 by (asm_simp_tac (simpset() addsimps [hypreal_mult,hypreal_add,
   632      real_add_mult_distrib]) 1);
   633 qed "hypreal_add_mult_distrib";
   634 
   635 val hypreal_mult_commute'= read_instantiate [("z","w")] hypreal_mult_commute;
   636 
   637 Goal "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)";
   638 by (simp_tac (simpset() addsimps [hypreal_mult_commute',hypreal_add_mult_distrib]) 1);
   639 qed "hypreal_add_mult_distrib2";
   640 
   641 val hypreal_mult_simps = [hypreal_mult_1, hypreal_mult_1_right];
   642 Addsimps hypreal_mult_simps;
   643 
   644 (*** one and zero are distinct ***)
   645 Goalw [hypreal_zero_def,hypreal_one_def] "0hr ~= 1hr";
   646 by (auto_tac (claset(),simpset() addsimps [real_zero_not_eq_one]));
   647 qed "hypreal_zero_not_eq_one";
   648 
   649 (*** existence of inverse ***)
   650 Goalw [hypreal_one_def,hypreal_zero_def] 
   651           "x ~= 0hr ==> x*hrinv(x) = 1hr";
   652 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   653 by (rotate_tac 1 1);
   654 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
   655     hypreal_mult] setloop (split_tac [expand_if])) 1);
   656 by (dtac FreeUltrafilterNat_Compl_mem 1);
   657 by (blast_tac (claset() addSIs [real_mult_inv_right,
   658     FreeUltrafilterNat_subset]) 1);
   659 qed "hypreal_mult_hrinv";
   660 
   661 Goal "x ~= 0hr ==> hrinv(x)*x = 1hr";
   662 by (asm_simp_tac (simpset() addsimps [hypreal_mult_hrinv,
   663     hypreal_mult_commute]) 1);
   664 qed "hypreal_mult_hrinv_left";
   665 
   666 Goal "x ~= 0hr ==> ? y. (x::hypreal) * y = 1hr";
   667 by (fast_tac (claset() addDs [hypreal_mult_hrinv]) 1);
   668 qed "hypreal_hrinv_ex";
   669 
   670 Goal "x ~= 0hr ==> ? y. y * (x::hypreal) = 1hr";
   671 by (fast_tac (claset() addDs [hypreal_mult_hrinv_left]) 1);
   672 qed "hypreal_hrinv_left_ex";
   673 
   674 Goal "x ~= 0hr ==> ?! y. (x::hypreal) * y = 1hr";
   675 by (auto_tac (claset() addIs [hypreal_mult_hrinv],simpset()));
   676 by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
   677 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
   678 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
   679 qed "hypreal_hrinv_ex1";
   680 
   681 Goal "x ~= 0hr ==> ?! y. y * (x::hypreal) = 1hr";
   682 by (auto_tac (claset() addIs [hypreal_mult_hrinv_left],simpset()));
   683 by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
   684 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
   685 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
   686 qed "hypreal_hrinv_left_ex1";
   687 
   688 Goal "[| y~= 0hr; x * y = 1hr |]  ==> x = hrinv y";
   689 by (forw_inst_tac [("x","y")] hypreal_mult_hrinv_left 1);
   690 by (res_inst_tac [("x1","y")] (hypreal_hrinv_left_ex1 RS ex1E) 1);
   691 by (assume_tac 1);
   692 by (Blast_tac 1);
   693 qed "hypreal_mult_inv_hrinv";
   694 
   695 Goal "x ~= 0hr ==> ? y. x = hrinv y";
   696 by (forw_inst_tac [("x","x")] hypreal_hrinv_left_ex 1);
   697 by (etac exE 1 THEN 
   698     forw_inst_tac [("x","y")] hypreal_mult_inv_hrinv 1);
   699 by (res_inst_tac [("x","y")] exI 2);
   700 by Auto_tac;
   701 qed "hypreal_as_inverse_ex";
   702 
   703 Goal "(c::hypreal) ~= 0hr ==> (c*a=c*b) = (a=b)";
   704 by Auto_tac;
   705 by (dres_inst_tac [("f","%x. x*hrinv c")] arg_cong 1);
   706 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_hrinv] @ hypreal_mult_ac)  1);
   707 qed "hypreal_mult_left_cancel";
   708     
   709 Goal "(c::hypreal) ~= 0hr ==> (a*c=b*c) = (a=b)";
   710 by (Step_tac 1);
   711 by (dres_inst_tac [("f","%x. x*hrinv c")] arg_cong 1);
   712 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_hrinv] @ hypreal_mult_ac)  1);
   713 qed "hypreal_mult_right_cancel";
   714 
   715 Goalw [hypreal_zero_def] "x ~= 0hr ==> hrinv(x) ~= 0hr";
   716 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   717 by (rotate_tac 1 1);
   718 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
   719     hypreal_mult] setloop (split_tac [expand_if])) 1);
   720 by (dtac FreeUltrafilterNat_Compl_mem 1 THEN Clarify_tac 1);
   721 by (ultra_tac (claset() addIs [ccontr] addDs 
   722     [full_rename_numerals thy rinv_not_zero],simpset()) 1);
   723 qed "hrinv_not_zero";
   724 
   725 Addsimps [hypreal_mult_hrinv,hypreal_mult_hrinv_left];
   726 
   727 Goal "[| x ~= 0hr; y ~= 0hr |] ==> x * y ~= 0hr";
   728 by (Step_tac 1);
   729 by (dres_inst_tac [("f","%z. hrinv x*z")] arg_cong 1);
   730 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
   731 qed "hypreal_mult_not_0";
   732 
   733 bind_thm ("hypreal_mult_not_0E",hypreal_mult_not_0 RS notE);
   734 
   735 Goal "x ~= 0hr ==> x * x ~= 0hr";
   736 by (blast_tac (claset() addDs [hypreal_mult_not_0]) 1);
   737 qed "hypreal_mult_self_not_zero";
   738 
   739 Goal "[| x ~= 0hr; y ~= 0hr |] ==> hrinv(x*y) = hrinv(x)*hrinv(y)";
   740 by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
   741 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,
   742     hypreal_mult_not_0]));
   743 by (res_inst_tac [("c1","y")] (hypreal_mult_right_cancel RS iffD1) 1);
   744 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_not_0] @ hypreal_mult_ac));
   745 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,hypreal_mult_not_0]));
   746 qed "hrinv_mult_eq";
   747 
   748 Goal "x ~= 0hr ==> hrinv(-x) = -hrinv(x)";
   749 by (res_inst_tac [("c1","-x")] (hypreal_mult_right_cancel RS iffD1) 1);
   750 by Auto_tac;
   751 qed "hypreal_minus_hrinv";
   752 
   753 Goal "[| x ~= 0hr; y ~= 0hr |] \
   754 \     ==> hrinv(x*y) = hrinv(x)*hrinv(y)";
   755 by (forw_inst_tac [("y","y")] hypreal_mult_not_0 1 THEN assume_tac 1);
   756 by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
   757 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym]));
   758 by (res_inst_tac [("c1","y")] (hypreal_mult_left_cancel RS iffD1) 1);
   759 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_left_commute]));
   760 by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
   761 qed "hypreal_hrinv_distrib";
   762 
   763 (*------------------------------------------------------------------
   764                    Theorems for ordering 
   765  ------------------------------------------------------------------*)
   766 
   767 (* prove introduction and elimination rules for hypreal_less *)
   768 
   769 Goalw [hypreal_less_def]
   770  "P < (Q::hypreal) = (EX X Y. X : Rep_hypreal(P) & \
   771 \                             Y : Rep_hypreal(Q) & \
   772 \                             {n. X n < Y n} : FreeUltrafilterNat)";
   773 by (Fast_tac 1);
   774 qed "hypreal_less_iff";
   775 
   776 Goalw [hypreal_less_def]
   777  "[| {n. X n < Y n} : FreeUltrafilterNat; \
   778 \         X : Rep_hypreal(P); \
   779 \         Y : Rep_hypreal(Q) |] ==> P < (Q::hypreal)";
   780 by (Fast_tac 1);
   781 qed "hypreal_lessI";
   782 
   783 
   784 Goalw [hypreal_less_def]
   785      "!! R1. [| R1 < (R2::hypreal); \
   786 \         !!X Y. {n. X n < Y n} : FreeUltrafilterNat ==> P; \
   787 \         !!X. X : Rep_hypreal(R1) ==> P; \ 
   788 \         !!Y. Y : Rep_hypreal(R2) ==> P |] \
   789 \     ==> P";
   790 by Auto_tac;
   791 qed "hypreal_lessE";
   792 
   793 Goalw [hypreal_less_def]
   794  "R1 < (R2::hypreal) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \
   795 \                                  X : Rep_hypreal(R1) & \
   796 \                                  Y : Rep_hypreal(R2))";
   797 by (Fast_tac 1);
   798 qed "hypreal_lessD";
   799 
   800 Goal "~ (R::hypreal) < R";
   801 by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
   802 by (auto_tac (claset(),simpset() addsimps [hypreal_less_def]));
   803 by (Ultra_tac 1);
   804 qed "hypreal_less_not_refl";
   805 
   806 (*** y < y ==> P ***)
   807 bind_thm("hypreal_less_irrefl",hypreal_less_not_refl RS notE);
   808 
   809 Goal "!!(x::hypreal). x < y ==> x ~= y";
   810 by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
   811 qed "hypreal_not_refl2";
   812 
   813 Goal "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
   814 by (res_inst_tac [("z","R1")] eq_Abs_hypreal 1);
   815 by (res_inst_tac [("z","R2")] eq_Abs_hypreal 1);
   816 by (res_inst_tac [("z","R3")] eq_Abs_hypreal 1);
   817 by (auto_tac (claset() addSIs [exI],simpset() 
   818      addsimps [hypreal_less_def]));
   819 by (ultra_tac (claset() addIs [real_less_trans],simpset()) 1);
   820 qed "hypreal_less_trans";
   821 
   822 Goal "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P";
   823 by (dtac hypreal_less_trans 1 THEN assume_tac 1);
   824 by (asm_full_simp_tac (simpset() addsimps 
   825     [hypreal_less_not_refl]) 1);
   826 qed "hypreal_less_asym";
   827 
   828 (*--------------------------------------------------------
   829   TODO: The following theorem should have been proved 
   830   first and then used througout the proofs as it probably 
   831   makes many of them more straightforward. 
   832  -------------------------------------------------------*)
   833 Goalw [hypreal_less_def]
   834       "(Abs_hypreal(hyprel^^{%n. X n}) < \
   835 \           Abs_hypreal(hyprel^^{%n. Y n})) = \
   836 \      ({n. X n < Y n} : FreeUltrafilterNat)";
   837 by (auto_tac (claset() addSIs [lemma_hyprel_refl],simpset()));
   838 by (Ultra_tac 1);
   839 qed "hypreal_less";
   840 
   841 (*---------------------------------------------------------------------------------
   842              Hyperreals as a linearly ordered field
   843  ---------------------------------------------------------------------------------*)
   844 (*** sum order ***)
   845 
   846 Goalw [hypreal_zero_def] 
   847       "[| 0hr < x; 0hr < y |] ==> 0hr < x + y";
   848 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   849 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   850 by (auto_tac (claset(),simpset() addsimps
   851     [hypreal_less_def,hypreal_add]));
   852 by (auto_tac (claset() addSIs [exI],simpset() addsimps
   853     [hypreal_less_def,hypreal_add]));
   854 by (ultra_tac (claset() addIs [real_add_order],simpset()) 1);
   855 qed "hypreal_add_order";
   856 
   857 (*** mult order ***)
   858 
   859 Goalw [hypreal_zero_def] 
   860           "[| 0hr < x; 0hr < y |] ==> 0hr < x * y";
   861 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   862 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   863 by (auto_tac (claset() addSIs [exI],simpset() addsimps
   864     [hypreal_less_def,hypreal_mult]));
   865 by (ultra_tac (claset() addIs [rename_numerals thy 
   866     real_mult_order],simpset()) 1);
   867 qed "hypreal_mult_order";
   868 
   869 (*---------------------------------------------------------------------------------
   870                          Trichotomy of the hyperreals
   871   --------------------------------------------------------------------------------*)
   872 
   873 Goalw [hyprel_def] "? x. x: hyprel ^^ {%n. #0}";
   874 by (res_inst_tac [("x","%n. #0")] exI 1);
   875 by (Step_tac 1);
   876 by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset()));
   877 qed "lemma_hyprel_0r_mem";
   878 
   879 Goalw [hypreal_zero_def]"0hr <  x | x = 0hr | x < 0hr";
   880 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   881 by (auto_tac (claset(),simpset() addsimps [hypreal_less_def]));
   882 by (cut_facts_tac [lemma_hyprel_0r_mem] 1 THEN etac exE 1);
   883 by (dres_inst_tac [("x","xa")] spec 1);
   884 by (dres_inst_tac [("x","x")] spec 1);
   885 by (cut_inst_tac [("x","x")] lemma_hyprel_refl 1);
   886 by Auto_tac;
   887 by (dres_inst_tac [("x","x")] spec 1);
   888 by (dres_inst_tac [("x","xa")] spec 1);
   889 by Auto_tac;
   890 by (Ultra_tac 1);
   891 by (auto_tac (claset() addIs [real_linear_less2],simpset()));
   892 qed "hypreal_trichotomy";
   893 
   894 val prems = Goal "[| 0hr < x ==> P; \
   895 \                 x = 0hr ==> P; \
   896 \                 x < 0hr ==> P |] ==> P";
   897 by (cut_inst_tac [("x","x")] hypreal_trichotomy 1);
   898 by (REPEAT (eresolve_tac (disjE::prems) 1));
   899 qed "hypreal_trichotomyE";
   900 
   901 (*----------------------------------------------------------------------------
   902             More properties of <
   903  ----------------------------------------------------------------------------*)
   904 Goal "!!(A::hypreal). A < B ==> A + C < B + C";
   905 by (res_inst_tac [("z","A")] eq_Abs_hypreal 1);
   906 by (res_inst_tac [("z","B")] eq_Abs_hypreal 1);
   907 by (res_inst_tac [("z","C")] eq_Abs_hypreal 1);
   908 by (auto_tac (claset() addSIs [exI],simpset() addsimps
   909     [hypreal_less_def,hypreal_add]));
   910 by (Ultra_tac 1);
   911 qed "hypreal_add_less_mono1";
   912 
   913 Goal "!!(A::hypreal). A < B ==> C + A < C + B";
   914 by (auto_tac (claset() addIs [hypreal_add_less_mono1],
   915     simpset() addsimps [hypreal_add_commute]));
   916 qed "hypreal_add_less_mono2";
   917 
   918 Goal "((x::hypreal) < y) = (0hr < y + -x)";
   919 by (Step_tac 1);
   920 by (dres_inst_tac [("C","-x")] hypreal_add_less_mono1 1);
   921 by (dres_inst_tac [("C","x")] hypreal_add_less_mono1 2);
   922 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   923 qed "hypreal_less_minus_iff"; 
   924 
   925 Goal "((x::hypreal) < y) = (x + -y< 0hr)";
   926 by (Step_tac 1);
   927 by (dres_inst_tac [("C","-y")] hypreal_add_less_mono1 1);
   928 by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 2);
   929 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   930 qed "hypreal_less_minus_iff2";
   931 
   932 Goal  "!!(y1 :: hypreal). [| z1 < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2";
   933 by (dtac (hypreal_less_minus_iff RS iffD1) 1);
   934 by (dtac (hypreal_less_minus_iff RS iffD1) 1);
   935 by (dtac hypreal_add_order 1 THEN assume_tac 1);
   936 by (thin_tac "0hr < y2 + - z2" 1);
   937 by (dres_inst_tac [("C","z1 + z2")] hypreal_add_less_mono1 1);
   938 by (auto_tac (claset(),simpset() addsimps 
   939     [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac));
   940 qed "hypreal_add_less_mono";
   941 
   942 Goal "((x::hypreal) = y) = (0hr = x + - y)";
   943 by Auto_tac;
   944 by (res_inst_tac [("x1","-y")] (hypreal_add_right_cancel RS iffD1) 1);
   945 by Auto_tac;
   946 qed "hypreal_eq_minus_iff"; 
   947 
   948 Goal "((x::hypreal) = y) = (0hr = y + - x)";
   949 by Auto_tac;
   950 by (res_inst_tac [("x1","-x")] (hypreal_add_right_cancel RS iffD1) 1);
   951 by Auto_tac;
   952 qed "hypreal_eq_minus_iff2"; 
   953 
   954 Goal "(x = y + z) = (x + -z = (y::hypreal))";
   955 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   956 qed "hypreal_eq_minus_iff3";
   957 
   958 Goal "(x = z + y) = (x + -z = (y::hypreal))";
   959 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
   960 qed "hypreal_eq_minus_iff4";
   961 
   962 Goal "(x ~= a) = (x + -a ~= 0hr)";
   963 by (auto_tac (claset() addDs [sym RS 
   964     (hypreal_eq_minus_iff RS iffD2)],simpset())); 
   965 qed "hypreal_not_eq_minus_iff";
   966 
   967 (*** linearity ***)
   968 Goal "(x::hypreal) < y | x = y | y < x";
   969 by (stac hypreal_eq_minus_iff2 1);
   970 by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1);
   971 by (res_inst_tac [("x1","y")] (hypreal_less_minus_iff2 RS ssubst) 1);
   972 by (rtac hypreal_trichotomyE 1);
   973 by Auto_tac;
   974 qed "hypreal_linear";
   975 
   976 Goal "!!(x::hypreal). [| x < y ==> P;  x = y ==> P; \
   977 \          y < x ==> P |] ==> P";
   978 by (cut_inst_tac [("x","x"),("y","y")] hypreal_linear 1);
   979 by Auto_tac;
   980 qed "hypreal_linear_less2";
   981 
   982 (*------------------------------------------------------------------------------
   983                             Properties of <=
   984  ------------------------------------------------------------------------------*)
   985 (*------ hypreal le iff reals le a.e ------*)
   986 
   987 Goalw [hypreal_le_def,real_le_def]
   988       "(Abs_hypreal(hyprel^^{%n. X n}) <= \
   989 \           Abs_hypreal(hyprel^^{%n. Y n})) = \
   990 \      ({n. X n <= Y n} : FreeUltrafilterNat)";
   991 by (auto_tac (claset(),simpset() addsimps [hypreal_less]));
   992 by (ALLGOALS(Ultra_tac));
   993 qed "hypreal_le";
   994 
   995 (*---------------------------------------------------------*)
   996 (*---------------------------------------------------------*)
   997 Goalw [hypreal_le_def] 
   998      "~(w < z) ==> z <= (w::hypreal)";
   999 by (assume_tac 1);
  1000 qed "hypreal_leI";
  1001 
  1002 Goalw [hypreal_le_def] 
  1003       "z<=w ==> ~(w<(z::hypreal))";
  1004 by (assume_tac 1);
  1005 qed "hypreal_leD";
  1006 
  1007 val hypreal_leE = make_elim hypreal_leD;
  1008 
  1009 Goal "(~(w < z)) = (z <= (w::hypreal))";
  1010 by (fast_tac (claset() addSIs [hypreal_leI,hypreal_leD]) 1);
  1011 qed "hypreal_less_le_iff";
  1012 
  1013 Goalw [hypreal_le_def] "~ z <= w ==> w<(z::hypreal)";
  1014 by (Fast_tac 1);
  1015 qed "not_hypreal_leE";
  1016 
  1017 Goalw [hypreal_le_def] "z < w ==> z <= (w::hypreal)";
  1018 by (fast_tac (claset() addEs [hypreal_less_asym]) 1);
  1019 qed "hypreal_less_imp_le";
  1020 
  1021 Goalw [hypreal_le_def] "!!(x::hypreal). x <= y ==> x < y | x = y";
  1022 by (cut_facts_tac [hypreal_linear] 1);
  1023 by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1);
  1024 qed "hypreal_le_imp_less_or_eq";
  1025 
  1026 Goalw [hypreal_le_def] "z<w | z=w ==> z <=(w::hypreal)";
  1027 by (cut_facts_tac [hypreal_linear] 1);
  1028 by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1);
  1029 qed "hypreal_less_or_eq_imp_le";
  1030 
  1031 Goal "(x <= (y::hypreal)) = (x < y | x=y)";
  1032 by (REPEAT(ares_tac [iffI, hypreal_less_or_eq_imp_le, hypreal_le_imp_less_or_eq] 1));
  1033 qed "hypreal_le_eq_less_or_eq";
  1034 
  1035 Goal "w <= (w::hypreal)";
  1036 by (simp_tac (simpset() addsimps [hypreal_le_eq_less_or_eq]) 1);
  1037 qed "hypreal_le_refl";
  1038 Addsimps [hypreal_le_refl];
  1039 
  1040 Goal "[| i <= j; j < k |] ==> i < (k::hypreal)";
  1041 by (dtac hypreal_le_imp_less_or_eq 1);
  1042 by (fast_tac (claset() addIs [hypreal_less_trans]) 1);
  1043 qed "hypreal_le_less_trans";
  1044 
  1045 Goal "!! (i::hypreal). [| i < j; j <= k |] ==> i < k";
  1046 by (dtac hypreal_le_imp_less_or_eq 1);
  1047 by (fast_tac (claset() addIs [hypreal_less_trans]) 1);
  1048 qed "hypreal_less_le_trans";
  1049 
  1050 Goal "[| i <= j; j <= k |] ==> i <= (k::hypreal)";
  1051 by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq,
  1052             rtac hypreal_less_or_eq_imp_le, fast_tac (claset() addIs [hypreal_less_trans])]);
  1053 qed "hypreal_le_trans";
  1054 
  1055 Goal "[| z <= w; w <= z |] ==> z = (w::hypreal)";
  1056 by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq,
  1057             fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym])]);
  1058 qed "hypreal_le_anti_sym";
  1059 
  1060 Goal "[| 0hr < x; 0hr <= y |] ==> 0hr < x + y";
  1061 by (auto_tac (claset() addDs [sym,hypreal_le_imp_less_or_eq]
  1062               addIs [hypreal_add_order],simpset()));
  1063 qed "hypreal_add_order_le";            
  1064 
  1065 (*------------------------------------------------------------------------
  1066  ------------------------------------------------------------------------*)
  1067 
  1068 Goal "[| ~ y < x; y ~= x |] ==> x < (y::hypreal)";
  1069 by (rtac not_hypreal_leE 1);
  1070 by (fast_tac (claset() addDs [hypreal_le_imp_less_or_eq]) 1);
  1071 qed "not_less_not_eq_hypreal_less";
  1072 
  1073 Goal "(0hr < -R) = (R < 0hr)";
  1074 by (Step_tac 1);
  1075 by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1);
  1076 by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2);
  1077 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
  1078 qed "hypreal_minus_zero_less_iff";
  1079 
  1080 Goal "(-R < 0hr) = (0hr < R)";
  1081 by (Step_tac 1);
  1082 by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1);
  1083 by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2);
  1084 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
  1085 qed "hypreal_minus_zero_less_iff2";
  1086 
  1087 Goal "((x::hypreal) < y) = (-y < -x)";
  1088 by (stac hypreal_less_minus_iff 1);
  1089 by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1);
  1090 by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
  1091 qed "hypreal_less_swap_iff";
  1092 
  1093 Goal "(0hr < x) = (-x < x)";
  1094 by (Step_tac 1);
  1095 by (rtac ccontr 2 THEN forward_tac 
  1096     [hypreal_leI RS hypreal_le_imp_less_or_eq] 2);
  1097 by (Step_tac 2);
  1098 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 2);
  1099 by (dres_inst_tac [("R2.0","-x")] hypreal_less_trans 2);
  1100 by (Auto_tac );
  1101 by (ftac hypreal_add_order 1 THEN assume_tac 1);
  1102 by (dres_inst_tac [("C","-x"),("B","x + x")] hypreal_add_less_mono1 1);
  1103 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
  1104 qed "hypreal_gt_zero_iff";
  1105 
  1106 Goal "(x < 0hr) = (x < -x)";
  1107 by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
  1108 by (stac hypreal_gt_zero_iff 1);
  1109 by (Full_simp_tac 1);
  1110 qed "hypreal_lt_zero_iff";
  1111 
  1112 Goalw [hypreal_le_def] "(0hr <= x) = (-x <= x)";
  1113 by (auto_tac (claset(),simpset() addsimps [hypreal_lt_zero_iff RS sym]));
  1114 qed "hypreal_ge_zero_iff";
  1115 
  1116 Goalw [hypreal_le_def] "(x <= 0hr) = (x <= -x)";
  1117 by (auto_tac (claset(),simpset() addsimps [hypreal_gt_zero_iff RS sym]));
  1118 qed "hypreal_le_zero_iff";
  1119 
  1120 Goal "[| x < 0hr; y < 0hr |] ==> 0hr < x * y";
  1121 by (REPEAT(dtac (hypreal_minus_zero_less_iff RS iffD2) 1));
  1122 by (dtac hypreal_mult_order 1 THEN assume_tac 1);
  1123 by (Asm_full_simp_tac 1);
  1124 qed "hypreal_mult_less_zero1";
  1125 
  1126 Goal "[| 0hr <= x; 0hr <= y |] ==> 0hr <= x * y";
  1127 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
  1128 by (auto_tac (claset() addIs [hypreal_mult_order,
  1129     hypreal_less_imp_le],simpset()));
  1130 qed "hypreal_le_mult_order";
  1131 
  1132 Goal "[| x <= 0hr; y <= 0hr |] ==> 0hr <= x * y";
  1133 by (rtac hypreal_less_or_eq_imp_le 1);
  1134 by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1);
  1135 by Auto_tac;
  1136 by (dtac hypreal_le_imp_less_or_eq 1);
  1137 by (auto_tac (claset() addDs [hypreal_mult_less_zero1],simpset()));
  1138 qed "real_mult_le_zero1";
  1139 
  1140 Goal "[| 0hr <= x; y < 0hr |] ==> x * y <= 0hr";
  1141 by (rtac hypreal_less_or_eq_imp_le 1);
  1142 by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1);
  1143 by Auto_tac;
  1144 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
  1145 by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
  1146 by (blast_tac (claset() addDs [hypreal_mult_order] 
  1147     addIs [hypreal_minus_mult_eq2 RS ssubst]) 1);
  1148 qed "hypreal_mult_le_zero";
  1149 
  1150 Goal "[| 0hr < x; y < 0hr |] ==> x*y < 0hr";
  1151 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
  1152 by (dtac hypreal_mult_order 1 THEN assume_tac 1);
  1153 by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
  1154 by (asm_full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2]) 1);
  1155 qed "hypreal_mult_less_zero";
  1156 
  1157 Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0hr < 1hr";
  1158 by (res_inst_tac [("x","%n. #0")] exI 1);
  1159 by (res_inst_tac [("x","%n. #1")] exI 1);
  1160 by (auto_tac (claset(),simpset() addsimps [real_zero_less_one,
  1161     FreeUltrafilterNat_Nat_set]));
  1162 qed "hypreal_zero_less_one";
  1163 
  1164 Goal "[| 0hr <= x; 0hr <= y |] ==> 0hr <= x + y";
  1165 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
  1166 by (auto_tac (claset() addIs [hypreal_add_order,
  1167     hypreal_less_imp_le],simpset()));
  1168 qed "hypreal_le_add_order";
  1169 
  1170 Goal "!!(q1::hypreal). q1 <= q2  ==> x + q1 <= x + q2";
  1171 by (dtac hypreal_le_imp_less_or_eq 1);
  1172 by (Step_tac 1);
  1173 by (auto_tac (claset() addSIs [hypreal_le_refl,
  1174     hypreal_less_imp_le,hypreal_add_less_mono1],
  1175     simpset() addsimps [hypreal_add_commute]));
  1176 qed "hypreal_add_left_le_mono1";
  1177 
  1178 Goal "!!(q1::hypreal). q1 <= q2  ==> q1 + x <= q2 + x";
  1179 by (auto_tac (claset() addDs [hypreal_add_left_le_mono1],
  1180     simpset() addsimps [hypreal_add_commute]));
  1181 qed "hypreal_add_le_mono1";
  1182 
  1183 Goal "!!k l::hypreal. [|i<=j;  k<=l |] ==> i + k <= j + l";
  1184 by (etac (hypreal_add_le_mono1 RS hypreal_le_trans) 1);
  1185 by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
  1186 (*j moves to the end because it is free while k, l are bound*)
  1187 by (etac hypreal_add_le_mono1 1);
  1188 qed "hypreal_add_le_mono";
  1189 
  1190 Goal "!!k l::hypreal. [|i<j;  k<=l |] ==> i + k < j + l";
  1191 by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] 
  1192     addIs [hypreal_add_less_mono1,hypreal_add_less_mono],simpset()));
  1193 qed "hypreal_add_less_le_mono";
  1194 
  1195 Goal "!!k l::hypreal. [|i<=j;  k<l |] ==> i + k < j + l";
  1196 by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] 
  1197     addIs [hypreal_add_less_mono2,hypreal_add_less_mono],simpset()));
  1198 qed "hypreal_add_le_less_mono";
  1199 
  1200 Goal "(0hr*x<r)=(0hr<r)";
  1201 by (Simp_tac 1);
  1202 qed "hypreal_mult_0_less";
  1203 
  1204 Goal "[| 0hr < z; x < y |] ==> x*z < y*z";       
  1205 by (rotate_tac 1 1);
  1206 by (dtac (hypreal_less_minus_iff RS iffD1) 1);
  1207 by (rtac (hypreal_less_minus_iff RS iffD2) 1);
  1208 by (dtac hypreal_mult_order 1 THEN assume_tac 1);
  1209 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2,
  1210     hypreal_minus_mult_eq2 RS sym, hypreal_mult_commute ]) 1);
  1211 qed "hypreal_mult_less_mono1";
  1212 
  1213 Goal "[| 0hr<z; x<y |] ==> z*x<z*y";       
  1214 by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,hypreal_mult_less_mono1]) 1);
  1215 qed "hypreal_mult_less_mono2";
  1216 
  1217 Goal "[| 0hr<=z; x<y |] ==> x*z<=y*z";
  1218 by (EVERY1 [rtac hypreal_less_or_eq_imp_le, dtac hypreal_le_imp_less_or_eq]);
  1219 by (auto_tac (claset() addIs [hypreal_mult_less_mono1],simpset()));
  1220 qed "hypreal_mult_le_less_mono1";
  1221 
  1222 Goal "[| 0hr<=z; x<y |] ==> z*x<=z*y";
  1223 by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,
  1224 				      hypreal_mult_le_less_mono1]) 1);
  1225 qed "hypreal_mult_le_less_mono2";
  1226 
  1227 Goal "[| 0hr<=z; x<=y |] ==> z*x<=z*y";
  1228 by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1);
  1229 by (auto_tac (claset() addIs [hypreal_mult_le_less_mono2,hypreal_le_refl],simpset()));
  1230 qed "hypreal_mult_le_le_mono1";
  1231 
  1232 val prem1::prem2::prem3::rest = goal thy
  1233      "[| 0hr<y; x<r; y*r<t*s |] ==> y*x<t*s";
  1234 by (rtac ([([prem1,prem2] MRS hypreal_mult_less_mono2),prem3] MRS hypreal_less_trans) 1);
  1235 qed "hypreal_mult_less_trans";
  1236 
  1237 Goal "[| 0hr<=y; x<r; y*r<t*s; 0hr<t*s|] ==> y*x<t*s";
  1238 by (dtac hypreal_le_imp_less_or_eq 1);
  1239 by (fast_tac (HOL_cs addEs [(hypreal_mult_0_less RS iffD2),hypreal_mult_less_trans]) 1);
  1240 qed "hypreal_mult_le_less_trans";
  1241 
  1242 Goal "[| 0hr <= y; x <= r; y*r < t*s; 0hr < t*s|] ==> y*x < t*s";
  1243 by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1);
  1244 by (fast_tac (claset() addIs [hypreal_mult_le_less_trans]) 1);
  1245 qed "hypreal_mult_le_le_trans";
  1246 
  1247 Goal "[| 0hr < r1; r1 <r2; 0hr < x; x < y|] \
  1248 \                     ==> r1 * x < r2 * y";
  1249 by (dres_inst_tac [("x","x")] hypreal_mult_less_mono2 1);
  1250 by (dres_inst_tac [("R1.0","0hr")] hypreal_less_trans 2);
  1251 by (dres_inst_tac [("x","r1")] hypreal_mult_less_mono1 3);
  1252 by Auto_tac;
  1253 by (blast_tac (claset() addIs [hypreal_less_trans]) 1);
  1254 qed "hypreal_mult_less_mono";
  1255 
  1256 Goal "[| 0hr < r1; r1 <r2; 0hr < y|] \
  1257 \                           ==> 0hr < r2 * y";
  1258 by (dres_inst_tac [("R1.0","0hr")] hypreal_less_trans 1);
  1259 by (assume_tac 1);
  1260 by (blast_tac (claset() addIs [hypreal_mult_order]) 1);
  1261 qed "hypreal_mult_order_trans";
  1262 
  1263 Goal "[| 0hr < r1; r1 <= r2; 0hr <= x; x <= y |] \
  1264 \                  ==> r1 * x <= r2 * y";
  1265 by (rtac hypreal_less_or_eq_imp_le 1);
  1266 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
  1267 by (auto_tac (claset() addIs [hypreal_mult_less_mono,
  1268     hypreal_mult_less_mono1,hypreal_mult_less_mono2,
  1269     hypreal_mult_order_trans,hypreal_mult_order],simpset()));
  1270 qed "hypreal_mult_le_mono";
  1271 
  1272 (*----------------------------------------------------------
  1273   hypreal_of_real preserves field and order properties
  1274  -----------------------------------------------------------*)
  1275 Goalw [hypreal_of_real_def] 
  1276       "hypreal_of_real ((z1::real) + z2) = \
  1277 \      hypreal_of_real z1 + hypreal_of_real z2";
  1278 by (asm_simp_tac (simpset() addsimps [hypreal_add,
  1279        hypreal_add_mult_distrib]) 1);
  1280 qed "hypreal_of_real_add";
  1281 
  1282 Goalw [hypreal_of_real_def] 
  1283             "hypreal_of_real ((z1::real) * z2) = hypreal_of_real z1 * hypreal_of_real z2";
  1284 by (full_simp_tac (simpset() addsimps [hypreal_mult,
  1285         hypreal_add_mult_distrib2]) 1);
  1286 qed "hypreal_of_real_mult";
  1287 
  1288 Goalw [hypreal_less_def,hypreal_of_real_def] 
  1289             "(z1 < z2) = (hypreal_of_real z1 <  hypreal_of_real z2)";
  1290 by Auto_tac;
  1291 by (res_inst_tac [("x","%n. z1")] exI 1);
  1292 by (Step_tac 1); 
  1293 by (res_inst_tac [("x","%n. z2")] exI 2);
  1294 by Auto_tac;
  1295 by (rtac FreeUltrafilterNat_P 1);
  1296 by (Ultra_tac 1);
  1297 qed "hypreal_of_real_less_iff";
  1298 
  1299 Addsimps [hypreal_of_real_less_iff RS sym];
  1300 
  1301 Goalw [hypreal_le_def,real_le_def] 
  1302             "(z1 <= z2) = (hypreal_of_real z1 <=  hypreal_of_real z2)";
  1303 by Auto_tac;
  1304 qed "hypreal_of_real_le_iff";
  1305 
  1306 Goalw [hypreal_of_real_def] "hypreal_of_real (-r) = - hypreal_of_real  r";
  1307 by (auto_tac (claset(),simpset() addsimps [hypreal_minus]));
  1308 qed "hypreal_of_real_minus";
  1309 
  1310 Goal "0hr < x ==> 0hr < hrinv x";
  1311 by (EVERY1[rtac ccontr, dtac hypreal_leI]);
  1312 by (forward_tac [hypreal_minus_zero_less_iff2 RS iffD2] 1);
  1313 by (forward_tac [hypreal_not_refl2 RS not_sym] 1);
  1314 by (dtac (hypreal_not_refl2 RS not_sym RS hrinv_not_zero) 1);
  1315 by (EVERY1[dtac hypreal_le_imp_less_or_eq, Step_tac]); 
  1316 by (dtac hypreal_mult_less_zero1 1 THEN assume_tac 1);
  1317 by (auto_tac (claset() addIs [hypreal_zero_less_one RS hypreal_less_asym],
  1318     simpset() addsimps [hypreal_minus_mult_eq1 RS sym,
  1319      hypreal_minus_zero_less_iff]));
  1320 qed "hypreal_hrinv_gt_zero";
  1321 
  1322 Goal "x < 0hr ==> hrinv x < 0hr";
  1323 by (ftac hypreal_not_refl2 1);
  1324 by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
  1325 by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
  1326 by (dtac (hypreal_minus_hrinv RS sym) 1);
  1327 by (auto_tac (claset() addIs [hypreal_hrinv_gt_zero],
  1328     simpset()));
  1329 qed "hypreal_hrinv_less_zero";
  1330 
  1331 Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real  #1 = 1hr";
  1332 by (Step_tac 1);
  1333 qed "hypreal_of_real_one";
  1334 
  1335 Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real  #0 = 0hr";
  1336 by (Step_tac 1);
  1337 qed "hypreal_of_real_zero";
  1338 
  1339 Goal "(hypreal_of_real  r = 0hr) = (r = #0)";
  1340 by (auto_tac (claset() addIs [FreeUltrafilterNat_P],
  1341     simpset() addsimps [hypreal_of_real_def,
  1342     hypreal_zero_def,FreeUltrafilterNat_Nat_set]));
  1343 qed "hypreal_of_real_zero_iff";
  1344 
  1345 Goal "(hypreal_of_real  r ~= 0hr) = (r ~= #0)";
  1346 by (full_simp_tac (simpset() addsimps [hypreal_of_real_zero_iff]) 1);
  1347 qed "hypreal_of_real_not_zero_iff";
  1348 
  1349 Goal "r ~= #0 ==> hrinv (hypreal_of_real r) = \
  1350 \          hypreal_of_real (rinv r)";
  1351 by (res_inst_tac [("c1","hypreal_of_real r")] (hypreal_mult_left_cancel RS iffD1) 1);
  1352 by (etac (hypreal_of_real_not_zero_iff RS iffD2) 1);
  1353 by (forward_tac [hypreal_of_real_not_zero_iff RS iffD2] 1);
  1354 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_mult RS sym,hypreal_of_real_one]));
  1355 qed "hypreal_of_real_hrinv";
  1356 
  1357 Goal "hypreal_of_real r ~= 0hr ==> hrinv (hypreal_of_real r) = \
  1358 \          hypreal_of_real (rinv r)";
  1359 by (etac (hypreal_of_real_not_zero_iff RS iffD1 RS hypreal_of_real_hrinv) 1);
  1360 qed "hypreal_of_real_hrinv2";
  1361 
  1362 Goal "x+x=x*(1hr+1hr)";
  1363 by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1);
  1364 qed "hypreal_add_self";
  1365 
  1366 Goal "1hr < 1hr + 1hr";
  1367 by (rtac (hypreal_less_minus_iff RS iffD2) 1);
  1368 by (full_simp_tac (simpset() addsimps [hypreal_zero_less_one,
  1369     hypreal_add_assoc]) 1);
  1370 qed "hypreal_one_less_two";
  1371 
  1372 Goal "0hr < 1hr + 1hr";
  1373 by (rtac ([hypreal_zero_less_one,
  1374           hypreal_one_less_two] MRS hypreal_less_trans) 1);
  1375 qed "hypreal_zero_less_two";
  1376 
  1377 Goal "1hr + 1hr ~= 0hr";
  1378 by (rtac (hypreal_zero_less_two RS hypreal_not_refl2 RS not_sym) 1);
  1379 qed "hypreal_two_not_zero";
  1380 Addsimps [hypreal_two_not_zero];
  1381 
  1382 Goal "x*hrinv(1hr + 1hr) + x*hrinv(1hr + 1hr) = x";
  1383 by (stac hypreal_add_self 1);
  1384 by (full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
  1385 qed "hypreal_sum_of_halves";
  1386 
  1387 Goal "z ~= 0hr ==> x*y = (x*hrinv(z))*(z*y)";
  1388 by (asm_simp_tac (simpset() addsimps hypreal_mult_ac)  1);
  1389 qed "lemma_chain";
  1390 
  1391 Goal "0hr < r ==> 0hr < r*hrinv(1hr+1hr)";
  1392 by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero 
  1393           RS hypreal_mult_less_mono1) 1);
  1394 by Auto_tac;
  1395 qed "hypreal_half_gt_zero";
  1396 
  1397 (* TODO: remove redundant  0hr < x *)
  1398 Goal "[| 0hr < r; 0hr < x; r < x |] ==> hrinv x < hrinv r";
  1399 by (ftac hypreal_hrinv_gt_zero 1);
  1400 by (forw_inst_tac [("x","x")] hypreal_hrinv_gt_zero 1);
  1401 by (forw_inst_tac [("x","r"),("z","hrinv r")] hypreal_mult_less_mono1 1);
  1402 by (assume_tac 1);
  1403 by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS 
  1404          not_sym RS hypreal_mult_hrinv]) 1);
  1405 by (ftac hypreal_hrinv_gt_zero 1);
  1406 by (forw_inst_tac [("x","1hr"),("z","hrinv x")] hypreal_mult_less_mono2 1);
  1407 by (assume_tac 1);
  1408 by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS 
  1409          not_sym RS hypreal_mult_hrinv_left,hypreal_mult_assoc RS sym]) 1);
  1410 qed "hypreal_hrinv_less_swap";
  1411 
  1412 Goal "[| 0hr < r; 0hr < x|] ==> (r < x) = (hrinv x < hrinv r)";
  1413 by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],simpset()));
  1414 by (res_inst_tac [("t","r")] (hypreal_hrinv_hrinv RS subst) 1);
  1415 by (etac (hypreal_not_refl2 RS not_sym) 1);
  1416 by (res_inst_tac [("t","x")] (hypreal_hrinv_hrinv RS subst) 1);
  1417 by (etac (hypreal_not_refl2 RS not_sym) 1);
  1418 by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],
  1419     simpset() addsimps [hypreal_hrinv_gt_zero]));
  1420 qed "hypreal_hrinv_less_iff";
  1421 
  1422 Goal "[| 0hr < z; x < y |] ==> x*hrinv(z) < y*hrinv(z)";
  1423 by (blast_tac (claset() addSIs [hypreal_mult_less_mono1,
  1424     hypreal_hrinv_gt_zero]) 1);
  1425 qed "hypreal_mult_hrinv_less_mono1";
  1426 
  1427 Goal "[| 0hr < z; x < y |] ==> hrinv(z)*x < hrinv(z)*y";
  1428 by (blast_tac (claset() addSIs [hypreal_mult_less_mono2,
  1429     hypreal_hrinv_gt_zero]) 1);
  1430 qed "hypreal_mult_hrinv_less_mono2";
  1431 
  1432 Goal "[| 0hr < z; x*z < y*z |] ==> x < y";
  1433 by (forw_inst_tac [("x","x*z")] hypreal_mult_hrinv_less_mono1 1);
  1434 by (dtac (hypreal_not_refl2 RS not_sym) 2);
  1435 by (auto_tac (claset() addSDs [hypreal_mult_hrinv],
  1436               simpset() addsimps hypreal_mult_ac));
  1437 qed "hypreal_less_mult_right_cancel";
  1438 
  1439 Goal "[| 0hr < z; z*x < z*y |] ==> x < y";
  1440 by (auto_tac (claset() addIs [hypreal_less_mult_right_cancel],
  1441     simpset() addsimps [hypreal_mult_commute]));
  1442 qed "hypreal_less_mult_left_cancel";
  1443 
  1444 Goal "[| 0hr < r; 0hr < ra; \
  1445 \                 r < x; ra < y |] \
  1446 \              ==> r*ra < x*y";
  1447 by (forw_inst_tac [("R2.0","r")] hypreal_less_trans 1);
  1448 by (dres_inst_tac [("z","ra"),("x","r")] hypreal_mult_less_mono1 2);
  1449 by (dres_inst_tac [("z","x"),("x","ra")] hypreal_mult_less_mono2 3);
  1450 by (auto_tac (claset() addIs [hypreal_less_trans],simpset()));
  1451 qed "hypreal_mult_less_gt_zero"; 
  1452 
  1453 Goal "[| 0hr < r; 0hr < ra; \
  1454 \                 r <= x; ra <= y |] \
  1455 \              ==> r*ra <= x*y";
  1456 by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
  1457 by (rtac hypreal_less_or_eq_imp_le 1);
  1458 by (auto_tac (claset() addIs [hypreal_mult_less_mono1,
  1459     hypreal_mult_less_mono2,hypreal_mult_less_gt_zero],
  1460     simpset()));
  1461 qed "hypreal_mult_le_ge_zero"; 
  1462 
  1463 Goal "? (x::hypreal). x < y";
  1464 by (rtac (hypreal_add_zero_right RS subst) 1);
  1465 by (res_inst_tac [("x","y + -1hr")] exI 1);
  1466 by (auto_tac (claset() addSIs [hypreal_add_less_mono2],
  1467     simpset() addsimps [hypreal_minus_zero_less_iff2,
  1468     hypreal_zero_less_one] delsimps [hypreal_add_zero_right]));
  1469 qed "hypreal_less_Ex";
  1470 
  1471 Goal "!!(A::hypreal). A + C < B + C ==> A < B";
  1472 by (dres_inst_tac [("C","-C")] hypreal_add_less_mono1 1);
  1473 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
  1474 qed "hypreal_less_add_right_cancel";
  1475 
  1476 Goal "!!(A::hypreal). C + A < C + B ==> A < B";
  1477 by (dres_inst_tac [("C","-C")] hypreal_add_less_mono2 1);
  1478 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
  1479 qed "hypreal_less_add_left_cancel";
  1480 
  1481 Goal "0hr <= x*x";
  1482 by (res_inst_tac [("x","0hr"),("y","x")] hypreal_linear_less2 1);
  1483 by (auto_tac (claset() addIs [hypreal_mult_order,
  1484     hypreal_mult_less_zero1,hypreal_less_imp_le],
  1485     simpset()));
  1486 qed "hypreal_le_square";
  1487 Addsimps [hypreal_le_square];
  1488 
  1489 Goalw [hypreal_le_def] "- (x*x) <= 0hr";
  1490 by (auto_tac (claset() addSDs [(hypreal_le_square RS 
  1491     hypreal_le_less_trans)],simpset() addsimps 
  1492     [hypreal_minus_zero_less_iff,hypreal_less_not_refl]));
  1493 qed "hypreal_less_minus_square";
  1494 Addsimps [hypreal_less_minus_square];
  1495 
  1496 Goal "[|x ~= 0hr; y ~= 0hr |] ==> \
  1497 \                   hrinv(x) + hrinv(y) = (x + y)*hrinv(x*y)";
  1498 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv_distrib,
  1499              hypreal_add_mult_distrib,hypreal_mult_assoc RS sym]) 1);
  1500 by (stac hypreal_mult_assoc 1);
  1501 by (rtac (hypreal_mult_left_commute RS subst) 1);
  1502 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
  1503 qed "hypreal_hrinv_add";
  1504 
  1505 Goal "x = -x ==> x = 0hr";
  1506 by (dtac (hypreal_eq_minus_iff RS iffD1 RS sym) 1);
  1507 by (Asm_full_simp_tac 1);
  1508 by (dtac (hypreal_add_self RS subst) 1);
  1509 by (rtac ccontr 1);
  1510 by (blast_tac (claset() addDs [hypreal_two_not_zero RSN
  1511                (2,hypreal_mult_not_0)]) 1);
  1512 qed "hypreal_self_eq_minus_self_zero";
  1513 
  1514 Goal "(x + x = 0hr) = (x = 0hr)";
  1515 by Auto_tac;
  1516 by (dtac (hypreal_add_self RS subst) 1);
  1517 by (rtac ccontr 1 THEN rtac hypreal_mult_not_0E 1);
  1518 by Auto_tac;
  1519 qed "hypreal_add_self_zero_cancel";
  1520 Addsimps [hypreal_add_self_zero_cancel];
  1521 
  1522 Goal "(x + x + y = y) = (x = 0hr)";
  1523 by Auto_tac;
  1524 by (dtac (hypreal_eq_minus_iff RS iffD1) 1 THEN dtac sym 1);
  1525 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
  1526 qed "hypreal_add_self_zero_cancel2";
  1527 Addsimps [hypreal_add_self_zero_cancel2];
  1528 
  1529 Goal "(x + (x + y) = y) = (x = 0hr)";
  1530 by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
  1531 qed "hypreal_add_self_zero_cancel2a";
  1532 Addsimps [hypreal_add_self_zero_cancel2a];
  1533 
  1534 Goal "(b = -a) = (-b = (a::hypreal))";
  1535 by Auto_tac;
  1536 qed "hypreal_minus_eq_swap";
  1537 
  1538 Goal "(-b = -a) = (b = (a::hypreal))";
  1539 by (asm_full_simp_tac (simpset() addsimps 
  1540     [hypreal_minus_eq_swap]) 1);
  1541 qed "hypreal_minus_eq_cancel";
  1542 Addsimps [hypreal_minus_eq_cancel];
  1543 
  1544 Goal "x < x + 1hr";
  1545 by (cut_inst_tac [("C","x")] 
  1546     (hypreal_zero_less_one RS hypreal_add_less_mono2) 1);
  1547 by (Asm_full_simp_tac 1);
  1548 qed "hypreal_less_self_add_one";
  1549 Addsimps [hypreal_less_self_add_one];
  1550 
  1551 Goal "((x::hypreal) + x = y + y) = (x = y)";
  1552 by (auto_tac (claset() addIs [hypreal_two_not_zero RS 
  1553      hypreal_mult_left_cancel RS iffD1],simpset() addsimps 
  1554      [hypreal_add_mult_distrib]));
  1555 qed "hypreal_add_self_cancel";
  1556 Addsimps [hypreal_add_self_cancel];
  1557 
  1558 Goal "(y = x + - y + x) = (y = (x::hypreal))";
  1559 by Auto_tac;
  1560 by (dres_inst_tac [("x1","y")] 
  1561     (hypreal_add_right_cancel RS iffD2) 1);
  1562 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
  1563 qed "hypreal_add_self_minus_cancel";
  1564 Addsimps [hypreal_add_self_minus_cancel];
  1565 
  1566 Goal "(y = x + (- y + x)) = (y = (x::hypreal))";
  1567 by (asm_full_simp_tac (simpset() addsimps 
  1568          [hypreal_add_assoc RS sym])1);
  1569 qed "hypreal_add_self_minus_cancel2";
  1570 Addsimps [hypreal_add_self_minus_cancel2];
  1571 
  1572 Goal "z + -x = y + (y + (-x + -z)) = (y = (z::hypreal))";
  1573 by Auto_tac;
  1574 by (dres_inst_tac [("x1","z")] 
  1575     (hypreal_add_right_cancel RS iffD2) 1);
  1576 by (asm_full_simp_tac (simpset() addsimps 
  1577     [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac) 1);
  1578 by (asm_full_simp_tac (simpset() addsimps 
  1579      [hypreal_add_assoc RS sym,hypreal_add_right_cancel]) 1);
  1580 qed "hypreal_add_self_minus_cancel3";
  1581 Addsimps [hypreal_add_self_minus_cancel3];
  1582 
  1583 (* check why this does not work without 2nd substiution anymore! *)
  1584 Goal "x < y ==> x < (x + y)*hrinv(1hr + 1hr)";
  1585 by (dres_inst_tac [("C","x")] hypreal_add_less_mono2 1);
  1586 by (dtac (hypreal_add_self RS subst) 1);
  1587 by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS 
  1588           hypreal_mult_less_mono1) 1);
  1589 by (auto_tac (claset() addDs [hypreal_two_not_zero RS 
  1590           (hypreal_mult_hrinv RS subst)],simpset() 
  1591           addsimps [hypreal_mult_assoc]));
  1592 qed "hypreal_less_half_sum";
  1593 
  1594 (* check why this does not work without 2nd substiution anymore! *)
  1595 Goal "x < y ==> (x + y)*hrinv(1hr + 1hr) < y";
  1596 by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 1);
  1597 by (dtac (hypreal_add_self RS subst) 1);
  1598 by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS 
  1599           hypreal_mult_less_mono1) 1);
  1600 by (auto_tac (claset() addDs [hypreal_two_not_zero RS 
  1601           (hypreal_mult_hrinv RS subst)],simpset() 
  1602           addsimps [hypreal_mult_assoc]));
  1603 qed "hypreal_gt_half_sum";
  1604 
  1605 Goal "!!(x::hypreal). x < y ==> EX r. x < r & r < y";
  1606 by (blast_tac (claset() addSIs [hypreal_less_half_sum,
  1607     hypreal_gt_half_sum]) 1);
  1608 qed "hypreal_dense";
  1609 
  1610 Goal "(x * x = 0hr) = (x = 0hr)";
  1611 by Auto_tac;
  1612 by (blast_tac (claset() addIs [hypreal_mult_not_0E]) 1);
  1613 qed "hypreal_mult_self_eq_zero_iff";
  1614 Addsimps [hypreal_mult_self_eq_zero_iff];
  1615 
  1616 Goal "(0hr = x * x) = (x = 0hr)";
  1617 by (auto_tac (claset() addDs [sym],simpset()));
  1618 qed "hypreal_mult_self_eq_zero_iff2";
  1619 Addsimps [hypreal_mult_self_eq_zero_iff2];
  1620 
  1621 Goal "(x*x + y*y = 0hr) = (x = 0hr & y = 0hr)";
  1622 by Auto_tac;
  1623 by (dtac (sym RS (hypreal_eq_minus_iff3 RS iffD1))  1);
  1624 by (dtac (sym RS (hypreal_eq_minus_iff4 RS iffD1))  2);
  1625 by (ALLGOALS(rtac ccontr));
  1626 by (ALLGOALS(dtac hypreal_mult_self_not_zero));
  1627 by (cut_inst_tac [("x1","x")] (hypreal_le_square 
  1628         RS hypreal_le_imp_less_or_eq) 1);
  1629 by (cut_inst_tac [("x1","y")] (hypreal_le_square 
  1630         RS hypreal_le_imp_less_or_eq) 2);
  1631 by (auto_tac (claset() addDs [sym],simpset()));
  1632 by (dres_inst_tac [("x1","y")] (hypreal_less_minus_square 
  1633     RS hypreal_le_less_trans) 1);
  1634 by (dres_inst_tac [("x1","x")] (hypreal_less_minus_square 
  1635     RS hypreal_le_less_trans) 2);
  1636 by (auto_tac (claset(),simpset() addsimps 
  1637        [hypreal_less_not_refl]));
  1638 qed "hypreal_squares_add_zero_iff";
  1639 Addsimps [hypreal_squares_add_zero_iff];
  1640 
  1641 Goal "x * x ~= 0hr ==> 0hr < x* x + y*y + z*z";
  1642 by (cut_inst_tac [("x1","x")] (hypreal_le_square 
  1643         RS hypreal_le_imp_less_or_eq) 1);
  1644 by (auto_tac (claset() addSIs 
  1645               [hypreal_add_order_le],simpset()));
  1646 qed "hypreal_sum_squares3_gt_zero";
  1647 
  1648 Goal "x * x ~= 0hr ==> 0hr < y*y + x*x + z*z";
  1649 by (dtac hypreal_sum_squares3_gt_zero 1);
  1650 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
  1651 qed "hypreal_sum_squares3_gt_zero2";
  1652 
  1653 Goal "x * x ~= 0hr ==> 0hr < y*y + z*z + x*x";
  1654 by (dtac hypreal_sum_squares3_gt_zero 1);
  1655 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
  1656 qed "hypreal_sum_squares3_gt_zero3";
  1657 
  1658 Goal "(x*x + y*y + z*z = 0hr) = \ 
  1659 \               (x = 0hr & y = 0hr & z = 0hr)";
  1660 by Auto_tac;
  1661 by (ALLGOALS(rtac ccontr));
  1662 by (ALLGOALS(dtac hypreal_mult_self_not_zero));
  1663 by (auto_tac (claset() addDs [hypreal_not_refl2 RS not_sym,
  1664    hypreal_sum_squares3_gt_zero3,hypreal_sum_squares3_gt_zero,
  1665    hypreal_sum_squares3_gt_zero2],simpset() delsimps
  1666    [hypreal_mult_self_eq_zero_iff]));
  1667 qed "hypreal_three_squares_add_zero_iff";
  1668 Addsimps [hypreal_three_squares_add_zero_iff];
  1669 
  1670 Addsimps [rename_numerals thy real_le_square];
  1671 Goal "(x::hypreal)*x <= x*x + y*y";
  1672 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  1673 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
  1674 by (auto_tac (claset(),simpset() addsimps 
  1675     [hypreal_mult,hypreal_add,hypreal_le]));
  1676 qed "hypreal_self_le_add_pos";
  1677 Addsimps [hypreal_self_le_add_pos];
  1678 
  1679 Goal "(x::hypreal)*x <= x*x + y*y + z*z";
  1680 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  1681 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
  1682 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
  1683 by (auto_tac (claset(),simpset() addsimps 
  1684     [hypreal_mult,hypreal_add,hypreal_le,
  1685     rename_numerals thy real_le_add_order]));
  1686 qed "hypreal_self_le_add_pos2";
  1687 Addsimps [hypreal_self_le_add_pos2];
  1688 
  1689 (*---------------------------------------------------------------------------------
  1690              Embedding of the naturals in the hyperreals
  1691  ---------------------------------------------------------------------------------*)
  1692 Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 0 = 1hr";
  1693 by (full_simp_tac (simpset() addsimps 
  1694     [pnat_one_iff RS sym,real_of_preal_def]) 1);
  1695 by (fold_tac [real_one_def]);
  1696 by (simp_tac (simpset() addsimps [hypreal_of_real_one]) 1);
  1697 qed "hypreal_of_posnat_one";
  1698 
  1699 Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr";
  1700 by (full_simp_tac (simpset() addsimps [real_of_preal_def,
  1701     rename_numerals thy (real_one_def RS meta_eq_to_obj_eq),
  1702      hypreal_add,hypreal_of_real_def,pnat_two_eq,hypreal_one_def,
  1703     real_add,prat_of_pnat_add RS sym,preal_of_prat_add RS sym] @ 
  1704     pnat_add_ac) 1);
  1705 qed "hypreal_of_posnat_two";
  1706 
  1707 Goalw [hypreal_of_posnat_def]
  1708           "hypreal_of_posnat n1 + hypreal_of_posnat n2 = \
  1709 \          hypreal_of_posnat (n1 + n2) + 1hr";
  1710 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one RS sym,
  1711     hypreal_of_real_add RS sym,hypreal_of_posnat_def,real_of_preal_add RS sym,
  1712     preal_of_prat_add RS sym,prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
  1713 qed "hypreal_of_posnat_add";
  1714 
  1715 Goal "hypreal_of_posnat (n + 1) = hypreal_of_posnat n + 1hr";
  1716 by (res_inst_tac [("x1","1hr")] (hypreal_add_right_cancel RS iffD1) 1);
  1717 by (rtac (hypreal_of_posnat_add RS subst) 1);
  1718 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,hypreal_add_assoc]) 1);
  1719 qed "hypreal_of_posnat_add_one";
  1720 
  1721 Goalw [real_of_posnat_def,hypreal_of_posnat_def] 
  1722       "hypreal_of_posnat n = hypreal_of_real (real_of_posnat n)";
  1723 by (rtac refl 1);
  1724 qed "hypreal_of_real_of_posnat";
  1725 
  1726 Goalw [hypreal_of_posnat_def] 
  1727       "(n < m) = (hypreal_of_posnat n < hypreal_of_posnat m)";
  1728 by Auto_tac;
  1729 qed "hypreal_of_posnat_less_iff";
  1730 
  1731 Addsimps [hypreal_of_posnat_less_iff RS sym];
  1732 (*---------------------------------------------------------------------------------
  1733                Existence of infinite hyperreal number
  1734  ---------------------------------------------------------------------------------*)
  1735 
  1736 Goal "hyprel^^{%n::nat. real_of_posnat n} : hypreal";
  1737 by Auto_tac;
  1738 qed "hypreal_omega";
  1739 
  1740 Goalw [omega_def] "Rep_hypreal(whr) : hypreal";
  1741 by (rtac Rep_hypreal 1);
  1742 qed "Rep_hypreal_omega";
  1743 
  1744 (* existence of infinite number not corresponding to any real number *)
  1745 (* use assumption that member FreeUltrafilterNat is not finite       *)
  1746 (* a few lemmas first *)
  1747 
  1748 Goal "{n::nat. x = real_of_posnat n} = {} | \
  1749 \     (? y. {n::nat. x = real_of_posnat n} = {y})";
  1750 by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],simpset()));
  1751 qed "lemma_omega_empty_singleton_disj";
  1752 
  1753 Goal "finite {n::nat. x = real_of_posnat n}";
  1754 by (cut_inst_tac [("x","x")] lemma_omega_empty_singleton_disj 1);
  1755 by Auto_tac;
  1756 qed "lemma_finite_omega_set";
  1757 
  1758 Goalw [omega_def,hypreal_of_real_def] 
  1759       "~ (? x. hypreal_of_real x = whr)";
  1760 by (auto_tac (claset(),simpset() addsimps [lemma_finite_omega_set 
  1761     RS FreeUltrafilterNat_finite]));
  1762 qed "not_ex_hypreal_of_real_eq_omega";
  1763 
  1764 Goal "hypreal_of_real x ~= whr";
  1765 by (cut_facts_tac [not_ex_hypreal_of_real_eq_omega] 1);
  1766 by Auto_tac;
  1767 qed "hypreal_of_real_not_eq_omega";
  1768 
  1769 (* existence of infinitesimal number also not *)
  1770 (* corresponding to any real number *)
  1771 
  1772 Goal "{n::nat. x = rinv(real_of_posnat n)} = {} | \
  1773 \     (? y. {n::nat. x = rinv(real_of_posnat n)} = {y})";
  1774 by (Step_tac 1 THEN Step_tac 1);
  1775 by (auto_tac (claset() addIs [real_of_posnat_rinv_inj],simpset()));
  1776 qed "lemma_epsilon_empty_singleton_disj";
  1777 
  1778 Goal "finite {n::nat. x = rinv(real_of_posnat n)}";
  1779 by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1);
  1780 by Auto_tac;
  1781 qed "lemma_finite_epsilon_set";
  1782 
  1783 Goalw [epsilon_def,hypreal_of_real_def] 
  1784       "~ (? x. hypreal_of_real x = ehr)";
  1785 by (auto_tac (claset(),simpset() addsimps [lemma_finite_epsilon_set 
  1786     RS FreeUltrafilterNat_finite]));
  1787 qed "not_ex_hypreal_of_real_eq_epsilon";
  1788 
  1789 Goal "hypreal_of_real x ~= ehr";
  1790 by (cut_facts_tac [not_ex_hypreal_of_real_eq_epsilon] 1);
  1791 by Auto_tac;
  1792 qed "hypreal_of_real_not_eq_epsilon";
  1793 
  1794 Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0hr";
  1795 by (auto_tac (claset(),simpset() addsimps 
  1796     [rename_numerals thy real_of_posnat_rinv_not_zero]));
  1797 qed "hypreal_epsilon_not_zero";
  1798 
  1799 Addsimps [rename_numerals thy real_of_posnat_not_eq_zero];
  1800 Goalw [omega_def,hypreal_zero_def] "whr ~= 0hr";
  1801 by (Simp_tac 1);
  1802 qed "hypreal_omega_not_zero";
  1803 
  1804 Goal "ehr = hrinv(whr)";
  1805 by (asm_full_simp_tac (simpset() addsimps 
  1806     [hypreal_hrinv,omega_def,epsilon_def]
  1807     setloop (split_tac [expand_if])) 1);
  1808 qed "hypreal_epsilon_hrinv_omega";
  1809 
  1810 (*----------------------------------------------------------------
  1811      Another embedding of the naturals in the 
  1812     hyperreals (see hypreal_of_posnat)
  1813  ----------------------------------------------------------------*)
  1814 Goalw [hypreal_of_nat_def] "hypreal_of_nat 0 = 0hr";
  1815 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one]) 1);
  1816 qed "hypreal_of_nat_zero";
  1817 
  1818 Goalw [hypreal_of_nat_def] "hypreal_of_nat 1 = 1hr";
  1819 by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,
  1820     hypreal_add_assoc]) 1);
  1821 qed "hypreal_of_nat_one";
  1822 
  1823 Goalw [hypreal_of_nat_def]
  1824       "hypreal_of_nat n1 + hypreal_of_nat n2 = \
  1825 \      hypreal_of_nat (n1 + n2)";
  1826 by (full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
  1827 by (simp_tac (simpset() addsimps [hypreal_of_posnat_add,
  1828     hypreal_add_assoc RS sym]) 1);
  1829 by (rtac (hypreal_add_commute RS subst) 1);
  1830 by (simp_tac (simpset() addsimps [hypreal_add_left_cancel,
  1831     hypreal_add_assoc]) 1);
  1832 qed "hypreal_of_nat_add";
  1833 
  1834 Goal "hypreal_of_nat 2 = 1hr + 1hr";
  1835 by (simp_tac (simpset() addsimps [hypreal_of_nat_one 
  1836     RS sym,hypreal_of_nat_add]) 1);
  1837 qed "hypreal_of_nat_two";
  1838 
  1839 Goalw [hypreal_of_nat_def] 
  1840       "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)";
  1841 by (auto_tac (claset() addIs [hypreal_add_less_mono1],simpset()));
  1842 by (dres_inst_tac [("C","1hr")] hypreal_add_less_mono1 1);
  1843 by (full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
  1844 qed "hypreal_of_nat_less_iff";
  1845 Addsimps [hypreal_of_nat_less_iff RS sym];
  1846 
  1847 (* naturals embedded in hyperreals is an hyperreal *)
  1848 Goalw [hypreal_of_nat_def,real_of_nat_def] 
  1849       "hypreal_of_nat  m = Abs_hypreal(hyprel^^{%n. real_of_nat m})";
  1850 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def,
  1851     hypreal_of_real_of_posnat,hypreal_minus,hypreal_one_def,hypreal_add]));
  1852 qed "hypreal_of_nat_iff";
  1853 
  1854 Goal "inj hypreal_of_nat";
  1855 by (rtac injI 1);
  1856 by (auto_tac (claset() addSDs [FreeUltrafilterNat_P],
  1857         simpset() addsimps [split_if_mem1, hypreal_of_nat_iff,
  1858         real_add_right_cancel,inj_real_of_nat RS injD]));
  1859 qed "inj_hypreal_of_nat";
  1860 
  1861 Goalw [hypreal_of_nat_def,hypreal_of_real_def,hypreal_of_posnat_def,
  1862        real_of_posnat_def,hypreal_one_def,real_of_nat_def] 
  1863        "hypreal_of_nat n = hypreal_of_real (real_of_nat n)";
  1864 by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1);
  1865 qed "hypreal_of_nat_real_of_nat";