src/HOL/Hyperreal/ExtraThms2.ML
author nipkow
Fri Feb 07 16:40:23 2003 +0100 (2003-02-07)
changeset 13810 c3fbfd472365
parent 13153 4b052946b41c
permissions -rw-r--r--
(*f -> ( *f because of new comments
     1 (*lcp: needed for binary 2 MOVE UP???*)
     2 
     3 Goal "(0::real) <= x^2";
     4 by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2]) 1); 
     5 qed "zero_le_x_squared";
     6 Addsimps [zero_le_x_squared];
     7 
     8 fun multl_by_tac x i = 
     9        let val cancel_thm = 
    10            CLAIM "[| (0::real)<z; z*x<z*y |] ==> x<y" 
    11        in
    12            res_inst_tac [("z",x)] cancel_thm i 
    13        end;
    14 
    15 fun multr_by_tac x i = 
    16        let val cancel_thm = 
    17            CLAIM "[| (0::real)<z; x*z<y*z |] ==> x<y" 
    18        in
    19            res_inst_tac [("z",x)] cancel_thm i 
    20        end;
    21 
    22 (* unused? *)
    23 Goal "ALL x y. x < y --> (f::real=>real) x < f y ==> inj f";
    24 by (rtac injI 1 THEN rtac ccontr 1);
    25 by (dtac (ARITH_PROVE "x ~= y ==> x < y | y < (x::real)") 1);
    26 by (Step_tac 1);
    27 by (auto_tac (claset() addSDs [spec],simpset()));
    28 qed "real_monofun_inj";
    29 
    30 (* HyperDef *)
    31 
    32 Goal "0 = Abs_hypreal (hyprel `` {%n. 0})";
    33 by (simp_tac (simpset() addsimps [hypreal_zero_def RS meta_eq_to_obj_eq RS sym]) 1);
    34 qed "hypreal_zero_num";
    35 
    36 Goal "1 = Abs_hypreal (hyprel `` {%n. 1})";
    37 by (simp_tac (simpset() addsimps [hypreal_one_def RS meta_eq_to_obj_eq RS sym]) 1);
    38 qed "hypreal_one_num";
    39 
    40 (* RealOrd *)
    41 
    42 Goalw [real_of_posnat_def] "0 < real_of_posnat n";
    43 by (rtac (real_gt_zero_preal_Ex RS iffD2) 1);
    44 by (Blast_tac 1);
    45 qed "real_of_posnat_gt_zero";
    46 
    47 Addsimps [real_of_posnat_gt_zero];
    48 
    49 bind_thm ("real_inv_real_of_posnat_gt_zero",
    50           real_of_posnat_gt_zero RS real_inverse_gt_0);
    51 Addsimps [real_inv_real_of_posnat_gt_zero];
    52 
    53 bind_thm ("real_of_posnat_ge_zero",real_of_posnat_gt_zero RS order_less_imp_le);
    54 Addsimps [real_of_posnat_ge_zero];
    55 
    56 Goal "real_of_posnat n ~= 0";
    57 by (rtac (real_of_posnat_gt_zero RS real_not_refl2 RS not_sym) 1);
    58 qed "real_of_posnat_not_eq_zero";
    59 Addsimps[real_of_posnat_not_eq_zero];
    60 
    61 Addsimps [real_of_posnat_not_eq_zero RS real_mult_inv_left];
    62 Addsimps [real_of_posnat_not_eq_zero RS real_mult_inv_right];
    63 
    64 Goal "1 <= real_of_posnat n";
    65 by (simp_tac (simpset() addsimps [real_of_posnat_one RS sym]) 1);
    66 by (induct_tac "n" 1);
    67 by (auto_tac (claset(),
    68 	      simpset () addsimps [real_of_posnat_Suc,real_of_posnat_one,
    69 				   order_less_imp_le]));
    70 qed "real_of_posnat_ge_one";
    71 Addsimps [real_of_posnat_ge_one];
    72 
    73 Goal "inverse(real_of_posnat n) ~= 0";
    74 by (rtac ((real_of_posnat_gt_zero RS 
    75     real_not_refl2 RS not_sym) RS real_inverse_not_zero) 1);
    76 qed "real_of_posnat_real_inv_not_zero";
    77 Addsimps [real_of_posnat_real_inv_not_zero];
    78 
    79 Goal "inverse(real_of_posnat x) = inverse(real_of_posnat y) ==> x = y";
    80 by (rtac (inj_real_of_posnat RS injD) 1);
    81 by (res_inst_tac [("n2","x")] 
    82     (real_of_posnat_real_inv_not_zero RS real_mult_left_cancel RS iffD1) 1);
    83 by (asm_full_simp_tac (simpset() addsimps [(real_of_posnat_gt_zero RS 
    84     real_not_refl2 RS not_sym) RS real_mult_inv_left]) 1);
    85 qed "real_of_posnat_real_inv_inj";
    86 
    87 Goal "r < r + inverse(real_of_posnat n)";
    88 by Auto_tac;
    89 qed "real_add_inv_real_of_posnat_less";
    90 Addsimps [real_add_inv_real_of_posnat_less];
    91 
    92 Goal "r <= r + inverse(real_of_posnat n)";
    93 by Auto_tac;
    94 qed "real_add_inv_real_of_posnat_le";
    95 Addsimps [real_add_inv_real_of_posnat_le];
    96 
    97 Goal "0 < r ==> r*(1 + -inverse(real_of_posnat n)) < r";
    98 by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
    99 by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
   100 by (auto_tac (claset() addIs [real_mult_order],simpset() 
   101     addsimps [real_add_assoc RS sym,real_minus_zero_less_iff2]));
   102 qed "real_mult_less_self";
   103 
   104 Goal "(EX n. inverse(real_of_posnat n) < r) = (EX n. 1 < r * real_of_posnat n)";
   105 by (Step_tac 1);
   106 by (dres_inst_tac [("n1","n")] (real_of_posnat_gt_zero 
   107                        RS real_mult_less_mono1) 1);
   108 by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS 
   109         real_inverse_gt_0 RS real_mult_less_mono1) 2);
   110 by (auto_tac (claset(),
   111 	      simpset() addsimps [(real_of_posnat_gt_zero RS 
   112     real_not_refl2 RS not_sym),real_mult_assoc]));
   113 qed "real_of_posnat_inv_Ex_iff";
   114 
   115 Goal "(inverse(real_of_posnat n) < r) = (1 < r * real_of_posnat n)";
   116 by (Step_tac 1);
   117 by (dres_inst_tac [("n1","n")] (real_of_posnat_gt_zero 
   118                        RS real_mult_less_mono1) 1);
   119 by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS 
   120         real_inverse_gt_0 RS real_mult_less_mono1) 2);
   121 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc]));
   122 qed "real_of_posnat_inv_iff";
   123 
   124 Goal "[| (0::real) <=z; x<y |] ==> z*x<=z*y";
   125 by (asm_simp_tac (simpset() addsimps [real_mult_commute,real_mult_le_less_mono1]) 1);
   126 qed "real_mult_le_less_mono2";
   127 
   128 Goal "[| (0::real) <=z; x<=y |] ==> z*x<=z*y";
   129 by (dres_inst_tac [("x","x")] real_le_imp_less_or_eq 1);
   130 by (auto_tac (claset() addIs [real_mult_le_less_mono2], simpset()));
   131 qed "real_mult_le_le_mono1";
   132 
   133 Goal "[| (0::real)<=z; x<=y |] ==> x*z<=y*z";
   134 by (dtac (real_mult_le_le_mono1) 1);
   135 by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
   136 qed "real_mult_le_le_mono2";
   137 
   138 Goal "(inverse(real_of_posnat n) <= r) = (1 <= r * real_of_posnat n)";
   139 by (Step_tac 1);
   140 by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS 
   141     order_less_imp_le RS real_mult_le_le_mono1) 1);
   142 by (dres_inst_tac [("n3","n")] (real_of_posnat_gt_zero RS 
   143         real_inverse_gt_0 RS order_less_imp_le RS 
   144         real_mult_le_le_mono1) 2);
   145 by (auto_tac (claset(),simpset() addsimps real_mult_ac));
   146 qed "real_of_posnat_inv_le_iff";
   147 
   148 Goalw [real_of_posnat_def] 
   149       "(real_of_posnat n < real_of_posnat m) = (n < m)";
   150 by Auto_tac;
   151 qed "real_of_posnat_less_iff";
   152 Addsimps [real_of_posnat_less_iff];
   153 
   154 Goal "(real_of_posnat n <= real_of_posnat m) = (n <= m)";
   155 by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],
   156     simpset() addsimps [real_le_less,le_eq_less_or_eq]));
   157 qed "real_of_posnat_le_iff";
   158 Addsimps [real_of_posnat_le_iff];
   159 
   160 Goal "[| (0::real)<z; x*z<y*z |] ==> x<y";
   161 by Auto_tac;
   162 qed "real_mult_less_cancel3";
   163 
   164 Goal "[| (0::real)<z; z*x<z*y |] ==> x<y";
   165 by Auto_tac;
   166 qed "real_mult_less_cancel4";
   167 
   168 Goal "0 < u  ==> (u < inverse (real_of_posnat n)) = (real_of_posnat n < inverse(u))";
   169 by (Step_tac 1);
   170 by (res_inst_tac [("n2","n")] ((real_of_posnat_gt_zero RS 
   171     real_inverse_gt_0) RS real_mult_less_cancel3) 1);
   172 by (res_inst_tac [("x1","u")] ( real_inverse_gt_0
   173    RS real_mult_less_cancel3) 2);
   174 by (auto_tac (claset(),
   175 	      simpset() addsimps [real_not_refl2 RS not_sym]));
   176 by (res_inst_tac [("z","u")] real_mult_less_cancel4 1);
   177 by (res_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS 
   178     real_mult_less_cancel4) 3);
   179 by (auto_tac (claset(),
   180 	      simpset() addsimps [real_not_refl2 RS not_sym,
   181               real_mult_assoc RS sym]));
   182 qed "real_of_posnat_less_inv_iff";
   183 
   184 Goal "0 < u ==> (u = inverse(real_of_posnat n)) = (real_of_posnat n = inverse u)";
   185 by Auto_tac;
   186 qed "real_of_posnat_inv_eq_iff";
   187 
   188 Goal "0 <= 1 + -inverse(real_of_posnat n)";
   189 by (res_inst_tac [("C","inverse(real_of_posnat n)")] real_le_add_right_cancel 1);
   190 by (simp_tac (simpset() addsimps [real_add_assoc,
   191     real_of_posnat_inv_le_iff]) 1);
   192 qed "real_add_one_minus_inv_ge_zero";
   193 
   194 Goal "0 < r ==> 0 <= r*(1 + -inverse(real_of_posnat n))";
   195 by (dtac (real_add_one_minus_inv_ge_zero RS real_mult_le_less_mono1) 1);
   196 by (Auto_tac);
   197 qed "real_mult_add_one_minus_ge_zero";
   198 
   199 Goal "x*y = (1::real) ==> y = inverse x";
   200 by (case_tac "x ~= 0" 1);
   201 by (res_inst_tac [("c1","x")] (real_mult_left_cancel RS iffD1) 1);
   202 by Auto_tac;
   203 qed "real_inverse_unique";
   204 
   205 Goal "[| (0::real) < x; x < 1 |] ==> 1 < inverse x";
   206 by (auto_tac (claset() addDs [real_inverse_less_swap],simpset()));
   207 qed "real_inverse_gt_one";
   208 
   209 Goal "(0 < real (n::nat)) = (0 < n)";
   210 by (rtac (real_of_nat_less_iff RS subst) 1);
   211 by Auto_tac;
   212 qed "real_of_nat_gt_zero_cancel_iff";
   213 Addsimps [real_of_nat_gt_zero_cancel_iff];
   214 
   215 Goal "(real (n::nat) <= 0) = (n = 0)";
   216 by (rtac ((real_of_nat_zero) RS subst) 1);
   217 by (stac real_of_nat_le_iff 1);
   218 by Auto_tac;
   219 qed "real_of_nat_le_zero_cancel_iff";
   220 Addsimps [real_of_nat_le_zero_cancel_iff];
   221 
   222 Goal "~ real (n::nat) < 0";
   223 by (simp_tac (simpset() addsimps [symmetric real_le_def,
   224     real_of_nat_ge_zero]) 1);
   225 qed "not_real_of_nat_less_zero";
   226 Addsimps [not_real_of_nat_less_zero];
   227 
   228 Goalw [real_le_def,le_def] 
   229       "(0 <= real (n::nat)) = (0 <= n)";
   230 by (Simp_tac 1);
   231 qed "real_of_nat_ge_zero_cancel_iff";
   232 Addsimps [real_of_nat_ge_zero_cancel_iff];
   233 
   234 Goal "real n = (if n=0 then 0 else 1 + real ((n::nat) - 1))";
   235 by (case_tac "n" 1);
   236 by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc]));
   237 qed "real_of_nat_num_if";
   238 
   239 Goal "4 * real n = real (4 * (n::nat))";
   240 by Auto_tac;
   241 qed "real_of_nat_mult_num_4_eq";
   242 
   243 (*REDUNDANT
   244     Goal "x * x = -(y * y) ==> x = (0::real)";
   245     by (auto_tac (claset() addIs [
   246 	real_sum_squares_cancel],simpset()));
   247     qed "real_sum_squares_cancel1a";
   248 
   249     Goal "x * x = -(y * y) ==> y = (0::real)";
   250     by (auto_tac (claset() addIs [
   251 	real_sum_squares_cancel],simpset()));
   252     qed "real_sum_squares_cancel2a";
   253 *)
   254 
   255 Goal "x * x = -(y * y) ==> x = (0::real) & y=0";
   256 by (auto_tac (claset() addIs [real_sum_squares_cancel],simpset()));
   257 qed "real_sum_squares_cancel_a";
   258 
   259 Goal "x*x - (1::real) = (x + 1)*(x - 1)";
   260 by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib,
   261     real_add_mult_distrib2,real_diff_def]));
   262 qed "real_squared_diff_one_factored";
   263 
   264 Goal "(x*x = (1::real)) = (x = 1 | x = - 1)";
   265 by Auto_tac;
   266 by (dtac (CLAIM "x = (y::real) ==> x - y = 0") 1);
   267 by (auto_tac (claset(),simpset() addsimps [real_squared_diff_one_factored]));
   268 qed "real_mult_is_one";
   269 AddIffs [real_mult_is_one];
   270 
   271 Goal "(x + y/2 <= (y::real)) = (x <= y /2)";
   272 by Auto_tac;
   273 qed "real_le_add_half_cancel";
   274 Addsimps [real_le_add_half_cancel];
   275 
   276 Goal "(x::real) - x/2 = x/2";
   277 by Auto_tac;
   278 qed "real_minus_half_eq";
   279 Addsimps [real_minus_half_eq];
   280 
   281 Goal "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> inverse x * y < inverse x1 * u";
   282 by (multl_by_tac "x" 1);
   283 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym]));
   284 by (simp_tac (simpset() addsimps real_mult_ac) 1);
   285 by (multr_by_tac "x1" 1);
   286 by (auto_tac (claset(),simpset() addsimps real_mult_ac));
   287 qed "real_mult_inverse_cancel";
   288 
   289 Goal "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1";
   290 by (auto_tac (claset() addDs [real_mult_inverse_cancel],simpset() addsimps real_mult_ac));
   291 qed "real_mult_inverse_cancel2";
   292 
   293 Goal "0 < inverse (real (Suc n))";
   294 by Auto_tac;
   295 qed "inverse_real_of_nat_gt_zero";
   296 Addsimps [ inverse_real_of_nat_gt_zero];
   297 
   298 Goal "0 <= inverse (real (Suc n))";
   299 by Auto_tac;
   300 qed "inverse_real_of_nat_ge_zero";
   301 Addsimps [ inverse_real_of_nat_ge_zero];
   302 
   303 Goal "x ~= 0 ==> x * x + y * y ~= (0::real)";
   304 by (rtac (CLAIM "!!x. ((x = y ==> False)) ==> x ~= y") 1);
   305 by (dtac (real_sum_squares_cancel) 1);
   306 by (Asm_full_simp_tac 1);
   307 qed "real_sum_squares_not_zero";
   308 
   309 Goal "y ~= 0 ==> x * x + y * y ~= (0::real)";
   310 by (rtac (CLAIM "!!x. ((x = y ==> False)) ==> x ~= y") 1);
   311 by (dtac (real_sum_squares_cancel2) 1);
   312 by (Asm_full_simp_tac 1);
   313 qed "real_sum_squares_not_zero2";
   314 
   315 (* RealAbs *)
   316 
   317 (* nice theorem *)
   318 Goal "abs x * abs x = x * (x::real)";
   319 by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
   320 by (auto_tac (claset(),simpset() addsimps [abs_eqI2,abs_minus_eqI2]));
   321 qed "abs_mult_abs";
   322 Addsimps [abs_mult_abs];
   323 
   324 (* RealPow *)
   325 Goalw [real_divide_def]
   326     "(x/y) ^ n = ((x::real) ^ n/ y ^ n)";
   327 by (auto_tac (claset(),simpset() addsimps [realpow_mult,
   328     realpow_inverse]));
   329 qed "realpow_divide";
   330 
   331 Goal "isCont (%x. x ^ n) x";
   332 by (rtac (DERIV_pow RS DERIV_isCont) 1);
   333 qed "isCont_realpow";
   334 Addsimps [isCont_realpow];
   335 
   336 Goal "(0::real) <= r --> 0 <= r ^ n";
   337 by (induct_tac "n" 1);
   338 by (auto_tac (claset(),simpset() addsimps [real_0_le_mult_iff]));
   339 qed_spec_mp "realpow_ge_zero2";
   340 
   341 Goal "(0::real) <= x & x <= y --> x ^ n <= y ^ n";
   342 by (induct_tac "n" 1);
   343 by (auto_tac (claset() addSIs [real_mult_le_mono],
   344     simpset() addsimps [realpow_ge_zero2]));
   345 qed_spec_mp "realpow_le2";
   346 
   347 Goal "(1::real) < r ==> 1 < r ^ (Suc n)";
   348 by (forw_inst_tac [("n","n")] realpow_ge_one 1);
   349 by (dtac real_le_imp_less_or_eq 1 THEN Step_tac 1);
   350 by (forward_tac [(real_zero_less_one RS real_less_trans)] 1);
   351 by (dres_inst_tac [("y","r ^ n")] (real_mult_less_mono2) 1);
   352 by (assume_tac 1);
   353 by (auto_tac (claset() addDs [real_less_trans],simpset()));
   354 qed "realpow_Suc_gt_one";
   355 
   356 Goal "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)";
   357 by (auto_tac (claset() addIs [real_sum_squares_cancel, real_sum_squares_cancel2], 
   358               simpset() addsimps [numeral_2_eq_2]));
   359 qed "realpow_two_sum_zero_iff";
   360 Addsimps [realpow_two_sum_zero_iff];
   361 
   362 Goal "(0::real) <= u ^ 2 + v ^ 2";
   363 by (rtac (real_le_add_order) 1);
   364 by (auto_tac (claset(), simpset() addsimps [numeral_2_eq_2])); 
   365 qed "realpow_two_le_add_order";
   366 Addsimps [realpow_two_le_add_order];
   367 
   368 Goal "(0::real) <= u ^ 2 + v ^ 2 + w ^ 2";
   369 by (REPEAT(rtac (real_le_add_order) 1));
   370 by (auto_tac (claset(), simpset() addsimps [numeral_2_eq_2])); 
   371 qed "realpow_two_le_add_order2";
   372 Addsimps [realpow_two_le_add_order2];
   373 
   374 Goal "(0::real) <= x*x + y*y";
   375 by (cut_inst_tac [("u","x"),("v","y")] realpow_two_le_add_order 1);
   376 by (auto_tac (claset(), simpset() addsimps [numeral_2_eq_2])); 
   377 qed "real_mult_self_sum_ge_zero";
   378 Addsimps [real_mult_self_sum_ge_zero];
   379 Addsimps [real_mult_self_sum_ge_zero RS abs_eqI1];
   380 
   381 Goal "x ~= 0 ==> (0::real) < x * x + y * y";
   382 by (cut_inst_tac [("x","x"),("y","y")] real_mult_self_sum_ge_zero 1);
   383 by (dtac real_le_imp_less_or_eq 1);
   384 by (dres_inst_tac [("y","y")] real_sum_squares_not_zero 1);
   385 by Auto_tac;
   386 qed "real_sum_square_gt_zero";
   387 
   388 Goal "y ~= 0 ==> (0::real) < x * x + y * y";
   389 by (rtac (real_add_commute RS subst) 1);
   390 by (etac real_sum_square_gt_zero 1);
   391 qed "real_sum_square_gt_zero2";
   392 
   393 Goal "-(u * u) <= (x * (x::real))";
   394 by (res_inst_tac [("j","0")] real_le_trans 1);
   395 by Auto_tac;
   396 qed "real_minus_mult_self_le";
   397 Addsimps [real_minus_mult_self_le];
   398 
   399 Goal "-(u ^ 2) <= (x::real) ^ 2";
   400 by (auto_tac (claset(), simpset() addsimps [numeral_2_eq_2])); 
   401 qed "realpow_square_minus_le";
   402 Addsimps [realpow_square_minus_le];
   403 
   404 Goal "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))";
   405 by (case_tac "n" 1);
   406 by Auto_tac;
   407 qed "realpow_num_eq_if";
   408 
   409 Goal "0 < (2::real) ^ (4*d)";
   410 by (induct_tac "d" 1);
   411 by (auto_tac (claset(),simpset() addsimps [realpow_num_eq_if]));
   412 qed "real_num_zero_less_two_pow";
   413 Addsimps [real_num_zero_less_two_pow];
   414 
   415 Goal "x * (4::real)   < y ==> x * (2 ^ 8) < y * (2 ^ 6)";
   416 by (subgoal_tac "(2::real) ^ 8 = 4 * (2 ^ 6)" 1);
   417 by (asm_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
   418 by (auto_tac (claset(),simpset() addsimps [realpow_num_eq_if]));
   419 qed "lemma_realpow_num_two_mono";
   420 
   421 Goal "2 ^ 2 = (4::real)";
   422 by (simp_tac (simpset() addsimps [realpow_num_eq_if]) 1);
   423 val lemma_realpow_4 = result();
   424 Addsimps [lemma_realpow_4];
   425 
   426 Goal "2 ^ 4 = (16::real)";
   427 by (simp_tac (simpset() addsimps [realpow_num_eq_if]) 1);
   428 val lemma_realpow_16 = result();
   429 Addsimps [lemma_realpow_16];
   430 
   431 (* HyperOrd *)
   432 
   433 Goal "[| (0::hypreal) < x; y < 0 |] ==> y*x < 0";
   434 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_commute,
   435     hypreal_mult_less_zero]));
   436 qed "hypreal_mult_less_zero2";
   437 
   438 (* HyperPow *)
   439 Goal "(0::hypreal) <= x * x";
   440 by (auto_tac (claset(),simpset() addsimps 
   441     [hypreal_0_le_mult_iff]));
   442 qed "hypreal_mult_self_ge_zero";
   443 Addsimps [hypreal_mult_self_ge_zero];
   444 
   445 (* deleted from distribution but I prefer to have it *)
   446 Goal "[|(0::hypreal) <= x; 0 <= y; x ^ Suc n = y ^ Suc n |] ==> x = y";
   447 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   448 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   449 by (auto_tac (claset(),simpset() addsimps 
   450     [hrealpow,hypreal_mult,hypreal_le,hypreal_zero_num]));
   451 by (ultra_tac (claset() addIs [realpow_Suc_cancel_eq],
   452     simpset()) 1);
   453 qed "hrealpow_Suc_cancel_eq";
   454 
   455 (* NSA.ML: next two were there before? Not in distrib though *)
   456 
   457 Goal "[| x + y : HInfinite; y: HFinite |] ==> x : HInfinite";
   458 by (rtac ccontr 1);
   459 by (dtac (HFinite_HInfinite_iff RS iffD2) 1);
   460 by (auto_tac (claset() addDs [HFinite_add],simpset() 
   461     addsimps [HInfinite_HFinite_iff]));
   462 qed "HInfinite_HFinite_add_cancel";
   463 
   464 Goal "[| x : HInfinite; y : HFinite |] ==> x + y : HInfinite";
   465 by (res_inst_tac [("y","-y")] HInfinite_HFinite_add_cancel 1);
   466 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc,
   467     HFinite_minus_iff]));
   468 qed "HInfinite_HFinite_add";
   469 
   470 Goal "[| x : HInfinite; x <= y; 0 <= x |] ==> y : HInfinite";
   471 by (auto_tac (claset() addIs [HFinite_bounded],simpset() 
   472     addsimps [HInfinite_HFinite_iff]));
   473 qed "HInfinite_ge_HInfinite";
   474 
   475 Goal "[| x : Infinitesimal; x ~= 0 |] ==> inverse x : HInfinite";
   476 by (rtac ccontr 1 THEN dtac (HFinite_HInfinite_iff RS iffD2) 1);
   477 by (auto_tac (claset() addDs [Infinitesimal_HFinite_mult2],simpset()));
   478 qed "Infinitesimal_inverse_HInfinite";
   479 
   480 Goal "n : HNatInfinite ==> inverse (hypreal_of_hypnat n) : Infinitesimal";
   481 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   482 by (auto_tac (claset(),simpset() addsimps [hypreal_of_hypnat,hypreal_inverse,
   483     HNatInfinite_FreeUltrafilterNat_iff,Infinitesimal_FreeUltrafilterNat_iff2]));
   484 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
   485 by Auto_tac;
   486 by (dres_inst_tac [("x","m + 1")] spec 1);
   487 by (Ultra_tac 1);
   488 by (subgoal_tac "abs(inverse (real (Y x))) = inverse(real (Y x))" 1);
   489 by (auto_tac (claset() addSIs [abs_eqI2],simpset()));
   490 by (rtac real_inverse_less_swap 1);
   491 by Auto_tac;
   492 qed "HNatInfinite_inverse_Infinitesimal";
   493 Addsimps [HNatInfinite_inverse_Infinitesimal];
   494 
   495 Goal "n : HNatInfinite ==> inverse (hypreal_of_hypnat n) ~= 0";
   496 by (auto_tac (claset() addSIs [hypreal_inverse_not_zero],simpset()));
   497 qed "HNatInfinite_inverse_not_zero";
   498 Addsimps [HNatInfinite_inverse_not_zero];
   499 
   500 Goal "N : HNatInfinite \
   501 \     ==> ( *fNat* (%x. inverse (real x))) N : Infinitesimal";
   502 by (res_inst_tac [("f1","inverse")]  (starfun_stafunNat_o2 RS subst) 1);
   503 by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
   504 by (auto_tac (claset(),simpset() addsimps [starfunNat_real_of_nat]));
   505 qed "starfunNat_inverse_real_of_nat_Infinitesimal";
   506 Addsimps [starfunNat_inverse_real_of_nat_Infinitesimal];
   507 
   508 Goal "[| x : HInfinite; y : HFinite - Infinitesimal |] \
   509 \     ==> x * y : HInfinite";
   510 by (rtac ccontr 1 THEN dtac (HFinite_HInfinite_iff RS iffD2) 1); 
   511 by (ftac HFinite_Infinitesimal_not_zero 1);
   512 by (dtac HFinite_not_Infinitesimal_inverse 1);
   513 by (Step_tac 1 THEN dtac HFinite_mult 1);
   514 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc,
   515     HFinite_HInfinite_iff]));
   516 qed "HInfinite_HFinite_not_Infinitesimal_mult";
   517 
   518 Goal "[| x : HInfinite; y : HFinite - Infinitesimal |] \
   519 \     ==> y * x : HInfinite";
   520 by (auto_tac (claset(),simpset() addsimps [hypreal_mult_commute,
   521     HInfinite_HFinite_not_Infinitesimal_mult]));
   522 qed "HInfinite_HFinite_not_Infinitesimal_mult2";
   523 
   524 Goal "[| x : HInfinite; 0 < x; y : Reals |] ==> y < x";
   525 by (auto_tac (claset() addSDs [bspec],simpset() addsimps 
   526     [HInfinite_def,hrabs_def,order_less_imp_le]));
   527 qed "HInfinite_gt_SReal";
   528 
   529 Goal "[| x : HInfinite; 0 < x |] ==> 1 < x";
   530 by (auto_tac (claset() addIs [HInfinite_gt_SReal],simpset()));
   531 qed "HInfinite_gt_zero_gt_one";
   532 
   533 (* not added at proof?? *)
   534 Addsimps [HInfinite_omega];
   535 
   536 (* Add in HyperDef.ML? *)
   537 Goalw [omega_def] "0 < omega";
   538 by (auto_tac (claset(),simpset() addsimps [hypreal_less,hypreal_zero_num]));
   539 qed "hypreal_omega_gt_zero";
   540 Addsimps [hypreal_omega_gt_zero];
   541 
   542 Goal "1 ~: HInfinite";
   543 by (simp_tac (simpset() addsimps [HInfinite_HFinite_iff]) 1);
   544 qed "not_HInfinite_one";
   545 Addsimps [not_HInfinite_one];
   546 
   547 
   548 (* RComplete.ML *)
   549 
   550 Goal "0 < x ==> ALL y. EX (n::nat). y < real n * x";
   551 by (Step_tac 1);
   552 by (cut_inst_tac [("x","y*inverse(x)")] reals_Archimedean2 1);
   553 by (Step_tac 1);
   554 by (forw_inst_tac [("x","y * inverse x")] (real_mult_less_mono1) 1);
   555 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,real_of_nat_def]));
   556 qed "reals_Archimedean3";
   557