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