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