src/HOL/Hyperreal/Star.thy
author nipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131 c69542757a4d
parent 15003 6145dd7538d7
child 15140 322485b816ac
permissions -rw-r--r--
New theory header syntax.
paulson@10751
     1
(*  Title       : Star.thy
paulson@10751
     2
    Author      : Jacques D. Fleuriot
paulson@10751
     3
    Copyright   : 1998  University of Cambridge
paulson@14468
     4
    Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
paulson@14370
     5
*)
paulson@10751
     6
paulson@14370
     7
header{*Star-Transforms in Non-Standard Analysis*}
paulson@14370
     8
nipkow@15131
     9
theory Star
nipkow@15131
    10
import NSA
nipkow@15131
    11
begin
paulson@10751
    12
paulson@10751
    13
constdefs
paulson@10751
    14
    (* nonstandard extension of sets *)
paulson@14370
    15
    starset :: "real set => hypreal set"          ("*s* _" [80] 80)
paulson@14468
    16
    "*s* A  == {x. \<forall>X \<in> Rep_hypreal(x). {n::nat. X n  \<in> A}: FreeUltrafilterNat}"
paulson@10751
    17
paulson@10751
    18
    (* internal sets *)
paulson@14370
    19
    starset_n :: "(nat => real set) => hypreal set"        ("*sn* _" [80] 80)
paulson@14468
    20
    "*sn* As  == {x. \<forall>X \<in> Rep_hypreal(x). {n::nat. X n : (As n)}: FreeUltrafilterNat}"
paulson@14370
    21
paulson@10751
    22
    InternalSets :: "hypreal set set"
paulson@14468
    23
    "InternalSets == {X. \<exists>As. X = *sn* As}"
paulson@10751
    24
paulson@10751
    25
    (* nonstandard extension of function *)
paulson@14370
    26
    is_starext  :: "[hypreal => hypreal, real => real] => bool"
paulson@14468
    27
    "is_starext F f == (\<forall>x y. \<exists>X \<in> Rep_hypreal(x). \<exists>Y \<in> Rep_hypreal(y).
paulson@10751
    28
                        ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
paulson@14370
    29
paulson@14370
    30
    starfun :: "(real => real) => hypreal => hypreal"       ("*f* _" [80] 80)
paulson@14468
    31
    "*f* f  == (%x. Abs_hypreal(\<Union>X \<in> Rep_hypreal(x). hyprel``{%n. f(X n)}))"
paulson@10751
    32
paulson@10751
    33
    (* internal functions *)
paulson@14370
    34
    starfun_n :: "(nat => (real => real)) => hypreal => hypreal"
paulson@14370
    35
                 ("*fn* _" [80] 80)
paulson@14468
    36
    "*fn* F  == (%x. Abs_hypreal(\<Union>X \<in> Rep_hypreal(x). hyprel``{%n. (F n)(X n)}))"
paulson@10751
    37
paulson@14370
    38
    InternalFuns :: "(hypreal => hypreal) set"
paulson@14468
    39
    "InternalFuns == {X. \<exists>F. X = *fn* F}"
paulson@10751
    40
paulson@10751
    41
paulson@10751
    42
paulson@14370
    43
(*--------------------------------------------------------
paulson@14370
    44
   Preamble - Pulling "EX" over "ALL"
paulson@14370
    45
 ---------------------------------------------------------*)
paulson@14370
    46
paulson@14370
    47
(* This proof does not need AC and was suggested by the
paulson@14370
    48
   referee for the JCM Paper: let f(x) be least y such
paulson@14370
    49
   that  Q(x,y)
paulson@14370
    50
*)
paulson@14468
    51
lemma no_choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>(f :: nat => nat). \<forall>x. Q x (f x)"
paulson@14370
    52
apply (rule_tac x = "%x. LEAST y. Q x y" in exI)
paulson@14370
    53
apply (blast intro: LeastI)
paulson@14370
    54
done
paulson@14370
    55
paulson@14370
    56
(*------------------------------------------------------------
paulson@14370
    57
    Properties of the *-transform applied to sets of reals
paulson@14370
    58
 ------------------------------------------------------------*)
paulson@14370
    59
paulson@14370
    60
lemma STAR_real_set: "*s*(UNIV::real set) = (UNIV::hypreal set)"
paulson@14468
    61
by (simp add: starset_def)
paulson@14370
    62
declare STAR_real_set [simp]
paulson@14370
    63
paulson@14370
    64
lemma STAR_empty_set: "*s* {} = {}"
paulson@14468
    65
by (simp add: starset_def)
paulson@14370
    66
declare STAR_empty_set [simp]
paulson@14370
    67
paulson@14370
    68
lemma STAR_Un: "*s* (A Un B) = *s* A Un *s* B"
paulson@14468
    69
apply (auto simp add: starset_def)
paulson@14370
    70
  prefer 3 apply (blast intro: FreeUltrafilterNat_subset)
paulson@14370
    71
 prefer 2 apply (blast intro: FreeUltrafilterNat_subset)
paulson@14370
    72
apply (drule FreeUltrafilterNat_Compl_mem)
paulson@14371
    73
apply (drule bspec, assumption)
paulson@14371
    74
apply (rule_tac z = x in eq_Abs_hypreal, auto, ultra)
paulson@14370
    75
done
paulson@14370
    76
paulson@14370
    77
lemma STAR_Int: "*s* (A Int B) = *s* A Int *s* B"
paulson@14468
    78
apply (simp add: starset_def, auto)
paulson@14370
    79
prefer 3 apply (blast intro: FreeUltrafilterNat_Int FreeUltrafilterNat_subset)
paulson@14370
    80
apply (blast intro: FreeUltrafilterNat_subset)+
paulson@14370
    81
done
paulson@14370
    82
paulson@14370
    83
lemma STAR_Compl: "*s* -A = -( *s* A)"
paulson@14370
    84
apply (auto simp add: starset_def)
paulson@14371
    85
apply (rule_tac [!] z = x in eq_Abs_hypreal)
paulson@14371
    86
apply (auto dest!: bspec, ultra)
paulson@14371
    87
apply (drule FreeUltrafilterNat_Compl_mem, ultra)
paulson@14370
    88
done
paulson@14370
    89
paulson@14370
    90
lemma STAR_mem_Compl: "x \<notin> *s* F ==> x : *s* (- F)"
paulson@14371
    91
by (auto simp add: STAR_Compl)
paulson@14370
    92
paulson@14370
    93
lemma STAR_diff: "*s* (A - B) = *s* A - *s* B"
paulson@14371
    94
by (auto simp add: Diff_eq STAR_Int STAR_Compl)
paulson@14370
    95
paulson@14370
    96
lemma STAR_subset: "A <= B ==> *s* A <= *s* B"
paulson@14468
    97
apply (simp add: starset_def)
paulson@14370
    98
apply (blast intro: FreeUltrafilterNat_subset)+
paulson@14370
    99
done
paulson@14370
   100
paulson@14468
   101
lemma STAR_mem: "a  \<in> A ==> hypreal_of_real a : *s* A"
paulson@14468
   102
apply (simp add: starset_def hypreal_of_real_def)
paulson@14370
   103
apply (auto intro: FreeUltrafilterNat_subset)
paulson@14370
   104
done
paulson@14370
   105
paulson@14370
   106
lemma STAR_hypreal_of_real_image_subset: "hypreal_of_real ` A <= *s* A"
paulson@14468
   107
apply (simp add: starset_def)
paulson@14370
   108
apply (auto simp add: hypreal_of_real_def)
paulson@14370
   109
apply (blast intro: FreeUltrafilterNat_subset)
paulson@14370
   110
done
paulson@14370
   111
paulson@14370
   112
lemma STAR_hypreal_of_real_Int: "*s* X Int Reals = hypreal_of_real ` X"
paulson@14468
   113
apply (simp add: starset_def)
paulson@14370
   114
apply (auto simp add: hypreal_of_real_def SReal_def)
paulson@14370
   115
apply (simp add: hypreal_of_real_def [symmetric])
paulson@14371
   116
apply (rule imageI, rule ccontr)
paulson@14370
   117
apply (drule bspec)
paulson@14370
   118
apply (rule lemma_hyprel_refl)
paulson@14371
   119
prefer 2 apply (blast intro: FreeUltrafilterNat_subset, auto)
paulson@14370
   120
done
paulson@14370
   121
paulson@14468
   122
lemma lemma_not_hyprealA: "x \<notin> hypreal_of_real ` A ==> \<forall>y \<in> A. x \<noteq> hypreal_of_real y"
paulson@14371
   123
by auto
paulson@14370
   124
paulson@14370
   125
lemma lemma_Compl_eq: "- {n. X n = xa} = {n. X n \<noteq> xa}"
paulson@14371
   126
by auto
paulson@14370
   127
paulson@14370
   128
lemma STAR_real_seq_to_hypreal:
paulson@14468
   129
    "\<forall>n. (X n) \<notin> M
paulson@14370
   130
          ==> Abs_hypreal(hyprel``{X}) \<notin> *s* M"
paulson@14468
   131
apply (simp add: starset_def)
paulson@14468
   132
apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
paulson@14370
   133
done
paulson@14370
   134
paulson@14370
   135
lemma STAR_singleton: "*s* {x} = {hypreal_of_real x}"
paulson@14468
   136
apply (simp add: starset_def)
paulson@14370
   137
apply (auto simp add: hypreal_of_real_def)
paulson@14371
   138
apply (rule_tac z = xa in eq_Abs_hypreal)
paulson@14370
   139
apply (auto intro: FreeUltrafilterNat_subset)
paulson@14370
   140
done
paulson@14370
   141
declare STAR_singleton [simp]
paulson@14370
   142
paulson@14370
   143
lemma STAR_not_mem: "x \<notin> F ==> hypreal_of_real x \<notin> *s* F"
paulson@14370
   144
apply (auto simp add: starset_def hypreal_of_real_def)
paulson@14371
   145
apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
paulson@14370
   146
done
paulson@14370
   147
paulson@14370
   148
lemma STAR_subset_closed: "[| x : *s* A; A <= B |] ==> x : *s* B"
paulson@14371
   149
by (blast dest: STAR_subset)
paulson@14370
   150
paulson@14370
   151
(*------------------------------------------------------------------
paulson@14370
   152
   Nonstandard extension of a set (defined using a constant
paulson@14370
   153
   sequence) as a special case of an internal set
paulson@14370
   154
 -----------------------------------------------------------------*)
paulson@14370
   155
paulson@14468
   156
lemma starset_n_starset: "\<forall>n. (As n = A) ==> *sn* As = *s* A"
paulson@14468
   157
by (simp add: starset_n_def starset_def)
paulson@14370
   158
paulson@14370
   159
paulson@14370
   160
(*----------------------------------------------------------------*)
paulson@14370
   161
(* Theorems about nonstandard extensions of functions             *)
paulson@14370
   162
(*----------------------------------------------------------------*)
paulson@14370
   163
paulson@14370
   164
(*----------------------------------------------------------------*)
paulson@14370
   165
(* Nonstandard extension of a function (defined using a           *)
paulson@14370
   166
(* constant sequence) as a special case of an internal function   *)
paulson@14370
   167
(*----------------------------------------------------------------*)
paulson@14370
   168
paulson@14468
   169
lemma starfun_n_starfun: "\<forall>n. (F n = f) ==> *fn* F = *f* f"
paulson@14468
   170
by (simp add: starfun_n_def starfun_def)
paulson@14370
   171
paulson@14370
   172
paulson@14370
   173
(*
paulson@15003
   174
   Prove that abs for hypreal is a nonstandard extension of abs for real w/o
paulson@14370
   175
   use of congruence property (proved after this for general
paulson@15003
   176
   nonstandard extensions of real valued functions). 
paulson@14370
   177
paulson@15003
   178
   Proof now Uses the ultrafilter tactic!
paulson@14370
   179
*)
paulson@14370
   180
paulson@14370
   181
lemma hrabs_is_starext_rabs: "is_starext abs abs"
paulson@14468
   182
apply (simp add: is_starext_def, safe)
paulson@14371
   183
apply (rule_tac z = x in eq_Abs_hypreal)
paulson@14371
   184
apply (rule_tac z = y in eq_Abs_hypreal, auto)
paulson@14371
   185
apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
paulson@14371
   186
apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
paulson@15003
   187
apply (auto dest!: spec 
paulson@15003
   188
            simp add: hypreal_minus abs_if hypreal_zero_def
paulson@15003
   189
                  hypreal_le hypreal_less)
paulson@14370
   190
apply (arith | ultra)+
paulson@14370
   191
done
paulson@14370
   192
paulson@14477
   193
lemma Rep_hypreal_FreeUltrafilterNat:
paulson@14477
   194
     "[| X \<in> Rep_hypreal z; Y \<in> Rep_hypreal z |]
paulson@14370
   195
      ==> {n. X n = Y n} : FreeUltrafilterNat"
paulson@14477
   196
apply (cases z)
paulson@14371
   197
apply (auto, ultra)
paulson@14370
   198
done
paulson@14370
   199
paulson@14370
   200
(*-----------------------------------------------------------------------
paulson@14370
   201
    Nonstandard extension of functions- congruence
paulson@14370
   202
 -----------------------------------------------------------------------*)
paulson@14370
   203
paulson@14370
   204
lemma starfun_congruent: "congruent hyprel (%X. hyprel``{%n. f (X n)})"
paulson@14468
   205
by (simp add: congruent_def, auto, ultra)
paulson@14370
   206
paulson@14370
   207
lemma starfun:
paulson@14370
   208
      "( *f* f) (Abs_hypreal(hyprel``{%n. X n})) =
paulson@14370
   209
       Abs_hypreal(hyprel `` {%n. f (X n)})"
paulson@14468
   210
apply (simp add: starfun_def)
paulson@14371
   211
apply (rule_tac f = Abs_hypreal in arg_cong)
paulson@14370
   212
apply (simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
paulson@14370
   213
                 UN_equiv_class [OF equiv_hyprel starfun_congruent])
paulson@14370
   214
done
paulson@14370
   215
paulson@14477
   216
lemma starfun_if_eq:
paulson@14477
   217
     "w \<noteq> hypreal_of_real x
paulson@14477
   218
       ==> ( *f* (\<lambda>z. if z = x then a else g z)) w = ( *f* g) w" 
paulson@14477
   219
apply (cases w) 
paulson@14477
   220
apply (simp add: hypreal_of_real_def starfun, ultra)
paulson@14477
   221
done
paulson@14477
   222
paulson@14370
   223
(*-------------------------------------------
paulson@14371
   224
  multiplication: ( *f) x ( *g) = *(f x g)
paulson@14370
   225
 ------------------------------------------*)
paulson@14370
   226
lemma starfun_mult: "( *f* f) xa * ( *f* g) xa = ( *f* (%x. f x * g x)) xa"
paulson@14477
   227
by (cases xa, simp add: starfun hypreal_mult)
paulson@15003
   228
paulson@14370
   229
declare starfun_mult [symmetric, simp]
paulson@14370
   230
paulson@14370
   231
(*---------------------------------------
paulson@14371
   232
  addition: ( *f) + ( *g) = *(f + g)
paulson@14370
   233
 ---------------------------------------*)
paulson@14370
   234
lemma starfun_add: "( *f* f) xa + ( *f* g) xa = ( *f* (%x. f x + g x)) xa"
paulson@14477
   235
by (cases xa, simp add: starfun hypreal_add)
paulson@14370
   236
declare starfun_add [symmetric, simp]
paulson@14370
   237
paulson@14370
   238
(*--------------------------------------------
paulson@14371
   239
  subtraction: ( *f) + -( *g) = *(f + -g)
paulson@14370
   240
 -------------------------------------------*)
paulson@14370
   241
paulson@14370
   242
lemma starfun_minus: "- ( *f* f) x = ( *f* (%x. - f x)) x"
paulson@14477
   243
apply (cases x)
paulson@14370
   244
apply (auto simp add: starfun hypreal_minus)
paulson@14370
   245
done
paulson@14370
   246
declare starfun_minus [symmetric, simp]
paulson@14370
   247
paulson@14370
   248
(*FIXME: delete*)
paulson@14370
   249
lemma starfun_add_minus: "( *f* f) xa + -( *f* g) xa = ( *f* (%x. f x + -g x)) xa"
paulson@14370
   250
apply (simp (no_asm))
paulson@14370
   251
done
paulson@14370
   252
declare starfun_add_minus [symmetric, simp]
paulson@14370
   253
paulson@14370
   254
lemma starfun_diff:
paulson@14370
   255
  "( *f* f) xa  - ( *f* g) xa = ( *f* (%x. f x - g x)) xa"
paulson@14468
   256
apply (simp add: diff_minus)
paulson@14370
   257
done
paulson@14370
   258
declare starfun_diff [symmetric, simp]
paulson@14370
   259
paulson@14370
   260
(*--------------------------------------
paulson@14371
   261
  composition: ( *f) o ( *g) = *(f o g)
paulson@14370
   262
 ---------------------------------------*)
paulson@14370
   263
paulson@14370
   264
lemma starfun_o2: "(%x. ( *f* f) (( *f* g) x)) = *f* (%x. f (g x))"
paulson@14370
   265
apply (rule ext)
paulson@14371
   266
apply (rule_tac z = x in eq_Abs_hypreal)
paulson@14370
   267
apply (auto simp add: starfun)
paulson@14370
   268
done
paulson@14370
   269
paulson@14370
   270
lemma starfun_o: "( *f* f) o ( *f* g) = ( *f* (f o g))"
paulson@14468
   271
apply (simp add: o_def)
paulson@14370
   272
apply (simp (no_asm) add: starfun_o2)
paulson@14370
   273
done
paulson@14370
   274
paulson@14370
   275
(*--------------------------------------
paulson@14370
   276
  NS extension of constant function
paulson@14370
   277
 --------------------------------------*)
paulson@14370
   278
lemma starfun_const_fun: "( *f* (%x. k)) xa = hypreal_of_real  k"
paulson@14477
   279
apply (cases xa)
paulson@14370
   280
apply (auto simp add: starfun hypreal_of_real_def)
paulson@14370
   281
done
paulson@14370
   282
paulson@14370
   283
declare starfun_const_fun [simp]
paulson@14370
   284
paulson@14370
   285
(*----------------------------------------------------
paulson@14370
   286
   the NS extension of the identity function
paulson@14370
   287
 ----------------------------------------------------*)
paulson@14370
   288
paulson@14370
   289
lemma starfun_Idfun_approx: "x @= hypreal_of_real a ==> ( *f* (%x. x)) x @= hypreal_of_real  a"
paulson@14477
   290
apply (cases x)
paulson@14370
   291
apply (auto simp add: starfun)
paulson@14370
   292
done
paulson@14370
   293
paulson@14370
   294
lemma starfun_Id: "( *f* (%x. x)) x = x"
paulson@14477
   295
apply (cases x)
paulson@14370
   296
apply (auto simp add: starfun)
paulson@14370
   297
done
paulson@14370
   298
declare starfun_Id [simp]
paulson@14370
   299
paulson@14370
   300
(*----------------------------------------------------------------------
paulson@14370
   301
      the *-function is a (nonstandard) extension of the function
paulson@14370
   302
 ----------------------------------------------------------------------*)
paulson@14370
   303
paulson@14370
   304
lemma is_starext_starfun: "is_starext ( *f* f) f"
paulson@14468
   305
apply (simp add: is_starext_def, auto)
paulson@14371
   306
apply (rule_tac z = x in eq_Abs_hypreal)
paulson@14371
   307
apply (rule_tac z = y in eq_Abs_hypreal)
paulson@14370
   308
apply (auto intro!: bexI simp add: starfun)
paulson@14370
   309
done
paulson@14370
   310
paulson@14370
   311
(*----------------------------------------------------------------------
paulson@14370
   312
     Any nonstandard extension is in fact the *-function
paulson@14370
   313
 ----------------------------------------------------------------------*)
paulson@14370
   314
paulson@14370
   315
lemma is_starfun_starext: "is_starext F f ==> F = *f* f"
paulson@14468
   316
apply (simp add: is_starext_def)
paulson@14370
   317
apply (rule ext)
paulson@14371
   318
apply (rule_tac z = x in eq_Abs_hypreal)
paulson@14371
   319
apply (drule_tac x = x in spec)
paulson@14370
   320
apply (drule_tac x = "( *f* f) x" in spec)
paulson@14371
   321
apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: starfun, ultra)
paulson@14370
   322
done
paulson@14370
   323
paulson@14370
   324
lemma is_starext_starfun_iff: "(is_starext F f) = (F = *f* f)"
paulson@14371
   325
by (blast intro: is_starfun_starext is_starext_starfun)
paulson@14370
   326
paulson@14370
   327
(*--------------------------------------------------------
paulson@14370
   328
   extented function has same solution as its standard
paulson@14370
   329
   version for real arguments. i.e they are the same
paulson@14370
   330
   for all real arguments
paulson@14370
   331
 -------------------------------------------------------*)
paulson@14370
   332
lemma starfun_eq: "( *f* f) (hypreal_of_real a) = hypreal_of_real (f a)"
paulson@14371
   333
by (auto simp add: starfun hypreal_of_real_def)
paulson@14370
   334
paulson@14370
   335
declare starfun_eq [simp]
paulson@14370
   336
paulson@14370
   337
lemma starfun_approx: "( *f* f) (hypreal_of_real a) @= hypreal_of_real (f a)"
paulson@14371
   338
by auto
paulson@14370
   339
paulson@14370
   340
(* useful for NS definition of derivatives *)
paulson@14370
   341
lemma starfun_lambda_cancel: "( *f* (%h. f (x + h))) xa  = ( *f* f) (hypreal_of_real  x + xa)"
paulson@14477
   342
apply (cases xa)
paulson@14370
   343
apply (auto simp add: starfun hypreal_of_real_def hypreal_add)
paulson@14370
   344
done
paulson@14370
   345
paulson@14370
   346
lemma starfun_lambda_cancel2: "( *f* (%h. f(g(x + h)))) xa = ( *f* (f o g)) (hypreal_of_real x + xa)"
paulson@14477
   347
apply (cases xa)
paulson@14370
   348
apply (auto simp add: starfun hypreal_of_real_def hypreal_add)
paulson@14370
   349
done
paulson@14370
   350
paulson@14370
   351
lemma starfun_mult_HFinite_approx: "[| ( *f* f) xa @= l; ( *f* g) xa @= m;
paulson@14370
   352
                  l: HFinite; m: HFinite
paulson@14370
   353
               |] ==>  ( *f* (%x. f x * g x)) xa @= l * m"
paulson@14371
   354
apply (drule approx_mult_HFinite, assumption+)
paulson@14370
   355
apply (auto intro: approx_HFinite [OF _ approx_sym])
paulson@14370
   356
done
paulson@14370
   357
paulson@14370
   358
lemma starfun_add_approx: "[| ( *f* f) xa @= l; ( *f* g) xa @= m
paulson@14370
   359
               |] ==>  ( *f* (%x. f x + g x)) xa @= l + m"
paulson@14370
   360
apply (auto intro: approx_add)
paulson@14370
   361
done
paulson@14370
   362
paulson@14370
   363
(*----------------------------------------------------
paulson@14370
   364
    Examples: hrabs is nonstandard extension of rabs
paulson@14370
   365
              inverse is nonstandard extension of inverse
paulson@14370
   366
 ---------------------------------------------------*)
paulson@14370
   367
paulson@14370
   368
(* can be proved easily using theorem "starfun" and *)
paulson@14370
   369
(* properties of ultrafilter as for inverse below we  *)
paulson@14370
   370
(* use the theorem we proved above instead          *)
paulson@14370
   371
paulson@14370
   372
lemma starfun_rabs_hrabs: "*f* abs = abs"
paulson@14371
   373
by (rule hrabs_is_starext_rabs [THEN is_starext_starfun_iff [THEN iffD1], symmetric])
paulson@14370
   374
paulson@14370
   375
lemma starfun_inverse_inverse: "( *f* inverse) x = inverse(x)"
paulson@14477
   376
apply (cases x)
paulson@14370
   377
apply (auto simp add: starfun hypreal_inverse hypreal_zero_def)
paulson@14370
   378
done
paulson@14370
   379
declare starfun_inverse_inverse [simp]
paulson@14370
   380
paulson@14370
   381
lemma starfun_inverse: "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
paulson@14477
   382
apply (cases x)
paulson@14370
   383
apply (auto simp add: starfun hypreal_inverse)
paulson@14370
   384
done
paulson@14370
   385
declare starfun_inverse [symmetric, simp]
paulson@14370
   386
paulson@14468
   387
lemma starfun_divide: "( *f* f) xa  / ( *f* g) xa = ( *f* (%x. f x / g x)) xa"
paulson@14468
   388
by (simp add: divide_inverse)
paulson@14370
   389
declare starfun_divide [symmetric, simp]
paulson@14370
   390
paulson@14370
   391
lemma starfun_inverse2: "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
paulson@14477
   392
apply (cases x)
paulson@14370
   393
apply (auto intro: FreeUltrafilterNat_subset dest!: FreeUltrafilterNat_Compl_mem simp add: starfun hypreal_inverse hypreal_zero_def)
paulson@14370
   394
done
paulson@14370
   395
paulson@14370
   396
(*-------------------------------------------------------------
paulson@14370
   397
    General lemma/theorem needed for proofs in elementary
paulson@14370
   398
    topology of the reals
paulson@14370
   399
 ------------------------------------------------------------*)
paulson@14370
   400
lemma starfun_mem_starset:
paulson@14468
   401
      "( *f* f) x : *s* A ==> x : *s* {x. f x  \<in> A}"
paulson@14468
   402
apply (simp add: starset_def)
paulson@14477
   403
apply (cases x)
paulson@14370
   404
apply (auto simp add: starfun)
paulson@14370
   405
apply (rename_tac "X")
paulson@14370
   406
apply (drule_tac x = "%n. f (X n) " in bspec)
paulson@14371
   407
apply (auto, ultra)
paulson@14370
   408
done
paulson@14370
   409
paulson@14370
   410
(*------------------------------------------------------------
paulson@14370
   411
   Alternative definition for hrabs with rabs function
paulson@14370
   412
   applied entrywise to equivalence class representative.
paulson@14370
   413
   This is easily proved using starfun and ns extension thm
paulson@14370
   414
 ------------------------------------------------------------*)
paulson@14370
   415
lemma hypreal_hrabs: "abs (Abs_hypreal (hyprel `` {X})) =
paulson@14370
   416
                  Abs_hypreal(hyprel `` {%n. abs (X n)})"
paulson@14370
   417
apply (simp (no_asm) add: starfun_rabs_hrabs [symmetric] starfun)
paulson@14370
   418
done
paulson@14370
   419
paulson@14370
   420
(*----------------------------------------------------------------
paulson@14370
   421
   nonstandard extension of set through nonstandard extension
paulson@14370
   422
   of rabs function i.e hrabs. A more general result should be
paulson@14370
   423
   where we replace rabs by some arbitrary function f and hrabs
paulson@14370
   424
   by its NS extenson ( *f* f). See second NS set extension below.
paulson@14370
   425
 ----------------------------------------------------------------*)
paulson@14370
   426
lemma STAR_rabs_add_minus:
paulson@14370
   427
   "*s* {x. abs (x + - y) < r} =
paulson@14370
   428
     {x. abs(x + -hypreal_of_real y) < hypreal_of_real r}"
paulson@14468
   429
apply (simp add: starset_def, safe)
paulson@14371
   430
apply (rule_tac [!] z = x in eq_Abs_hypreal)
paulson@14371
   431
apply (auto intro!: exI dest!: bspec simp add: hypreal_minus hypreal_of_real_def hypreal_add hypreal_hrabs hypreal_less, ultra)
paulson@14370
   432
done
paulson@14370
   433
paulson@14370
   434
lemma STAR_starfun_rabs_add_minus:
paulson@14370
   435
  "*s* {x. abs (f x + - y) < r} =
paulson@14370
   436
       {x. abs(( *f* f) x + -hypreal_of_real y) < hypreal_of_real r}"
paulson@14468
   437
apply (simp add: starset_def, safe)
paulson@14371
   438
apply (rule_tac [!] z = x in eq_Abs_hypreal)
paulson@14371
   439
apply (auto intro!: exI dest!: bspec simp add: hypreal_minus hypreal_of_real_def hypreal_add hypreal_hrabs hypreal_less starfun, ultra)
paulson@14370
   440
done
paulson@14370
   441
paulson@14370
   442
(*-------------------------------------------------------------------
paulson@14370
   443
   Another characterization of Infinitesimal and one of @= relation.
paulson@14370
   444
   In this theory since hypreal_hrabs proved here. (To Check:) Maybe
paulson@14370
   445
   move both if possible?
paulson@14370
   446
 -------------------------------------------------------------------*)
paulson@14378
   447
lemma Infinitesimal_FreeUltrafilterNat_iff2:
paulson@14468
   448
     "(x \<in> Infinitesimal) =
paulson@14468
   449
      (\<exists>X \<in> Rep_hypreal(x).
paulson@14468
   450
        \<forall>m. {n. abs(X n) < inverse(real(Suc m))}
paulson@14468
   451
                \<in>  FreeUltrafilterNat)"
paulson@14477
   452
apply (cases x)
paulson@14370
   453
apply (auto intro!: bexI lemma_hyprel_refl 
paulson@14378
   454
            simp add: Infinitesimal_hypreal_of_nat_iff hypreal_of_real_def
paulson@14378
   455
     hypreal_inverse hypreal_hrabs hypreal_less hypreal_of_nat_eq)
paulson@14371
   456
apply (drule_tac x = n in spec, ultra)
paulson@14370
   457
done
paulson@14370
   458
paulson@14370
   459
lemma approx_FreeUltrafilterNat_iff: "(Abs_hypreal(hyprel``{X}) @= Abs_hypreal(hyprel``{Y})) =
paulson@14468
   460
      (\<forall>m. {n. abs (X n + - Y n) <
paulson@14370
   461
                  inverse(real(Suc m))} : FreeUltrafilterNat)"
paulson@14370
   462
apply (subst approx_minus_iff)
paulson@14370
   463
apply (rule mem_infmal_iff [THEN subst])
paulson@14370
   464
apply (auto simp add: hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff2)
paulson@14371
   465
apply (drule_tac x = m in spec, ultra)
paulson@14370
   466
done
paulson@14370
   467
paulson@14370
   468
lemma inj_starfun: "inj starfun"
paulson@14370
   469
apply (rule inj_onI)
paulson@14371
   470
apply (rule ext, rule ccontr)
paulson@14370
   471
apply (drule_tac x = "Abs_hypreal (hyprel ``{%n. xa}) " in fun_cong)
paulson@14370
   472
apply (auto simp add: starfun)
paulson@14370
   473
done
paulson@14370
   474
paulson@14370
   475
ML
paulson@14370
   476
{*
paulson@14370
   477
val starset_def = thm"starset_def";
paulson@14370
   478
val starset_n_def = thm"starset_n_def";
paulson@14370
   479
val InternalSets_def = thm"InternalSets_def";
paulson@14370
   480
val is_starext_def = thm"is_starext_def";
paulson@14370
   481
val starfun_def = thm"starfun_def";
paulson@14370
   482
val starfun_n_def = thm"starfun_n_def";
paulson@14370
   483
val InternalFuns_def = thm"InternalFuns_def";
paulson@14370
   484
paulson@14370
   485
val no_choice = thm "no_choice";
paulson@14370
   486
val STAR_real_set = thm "STAR_real_set";
paulson@14370
   487
val STAR_empty_set = thm "STAR_empty_set";
paulson@14370
   488
val STAR_Un = thm "STAR_Un";
paulson@14370
   489
val STAR_Int = thm "STAR_Int";
paulson@14370
   490
val STAR_Compl = thm "STAR_Compl";
paulson@14370
   491
val STAR_mem_Compl = thm "STAR_mem_Compl";
paulson@14370
   492
val STAR_diff = thm "STAR_diff";
paulson@14370
   493
val STAR_subset = thm "STAR_subset";
paulson@14370
   494
val STAR_mem = thm "STAR_mem";
paulson@14370
   495
val STAR_hypreal_of_real_image_subset = thm "STAR_hypreal_of_real_image_subset";
paulson@14370
   496
val STAR_hypreal_of_real_Int = thm "STAR_hypreal_of_real_Int";
paulson@14370
   497
val STAR_real_seq_to_hypreal = thm "STAR_real_seq_to_hypreal";
paulson@14370
   498
val STAR_singleton = thm "STAR_singleton";
paulson@14370
   499
val STAR_not_mem = thm "STAR_not_mem";
paulson@14370
   500
val STAR_subset_closed = thm "STAR_subset_closed";
paulson@14370
   501
val starset_n_starset = thm "starset_n_starset";
paulson@14370
   502
val starfun_n_starfun = thm "starfun_n_starfun";
paulson@14370
   503
val hrabs_is_starext_rabs = thm "hrabs_is_starext_rabs";
paulson@14370
   504
val Rep_hypreal_FreeUltrafilterNat = thm "Rep_hypreal_FreeUltrafilterNat";
paulson@14370
   505
val starfun_congruent = thm "starfun_congruent";
paulson@14370
   506
val starfun = thm "starfun";
paulson@14370
   507
val starfun_mult = thm "starfun_mult";
paulson@14370
   508
val starfun_add = thm "starfun_add";
paulson@14370
   509
val starfun_minus = thm "starfun_minus";
paulson@14370
   510
val starfun_add_minus = thm "starfun_add_minus";
paulson@14370
   511
val starfun_diff = thm "starfun_diff";
paulson@14370
   512
val starfun_o2 = thm "starfun_o2";
paulson@14370
   513
val starfun_o = thm "starfun_o";
paulson@14370
   514
val starfun_const_fun = thm "starfun_const_fun";
paulson@14370
   515
val starfun_Idfun_approx = thm "starfun_Idfun_approx";
paulson@14370
   516
val starfun_Id = thm "starfun_Id";
paulson@14370
   517
val is_starext_starfun = thm "is_starext_starfun";
paulson@14370
   518
val is_starfun_starext = thm "is_starfun_starext";
paulson@14370
   519
val is_starext_starfun_iff = thm "is_starext_starfun_iff";
paulson@14370
   520
val starfun_eq = thm "starfun_eq";
paulson@14370
   521
val starfun_approx = thm "starfun_approx";
paulson@14370
   522
val starfun_lambda_cancel = thm "starfun_lambda_cancel";
paulson@14370
   523
val starfun_lambda_cancel2 = thm "starfun_lambda_cancel2";
paulson@14370
   524
val starfun_mult_HFinite_approx = thm "starfun_mult_HFinite_approx";
paulson@14370
   525
val starfun_add_approx = thm "starfun_add_approx";
paulson@14370
   526
val starfun_rabs_hrabs = thm "starfun_rabs_hrabs";
paulson@14370
   527
val starfun_inverse_inverse = thm "starfun_inverse_inverse";
paulson@14370
   528
val starfun_inverse = thm "starfun_inverse";
paulson@14370
   529
val starfun_divide = thm "starfun_divide";
paulson@14370
   530
val starfun_inverse2 = thm "starfun_inverse2";
paulson@14370
   531
val starfun_mem_starset = thm "starfun_mem_starset";
paulson@14370
   532
val hypreal_hrabs = thm "hypreal_hrabs";
paulson@14370
   533
val STAR_rabs_add_minus = thm "STAR_rabs_add_minus";
paulson@14370
   534
val STAR_starfun_rabs_add_minus = thm "STAR_starfun_rabs_add_minus";
paulson@14370
   535
val Infinitesimal_FreeUltrafilterNat_iff2 = thm "Infinitesimal_FreeUltrafilterNat_iff2";
paulson@14370
   536
val approx_FreeUltrafilterNat_iff = thm "approx_FreeUltrafilterNat_iff";
paulson@14370
   537
val inj_starfun = thm "inj_starfun";
paulson@14370
   538
*}
paulson@14370
   539
paulson@14370
   540
end