src/HOL/NSA/NSCA.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 47108 2a1953f0d20d
child 53015 a1119cf551e8
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
haftmann@28952
     1
(*  Title       : NSA/NSCA.thy
huffman@27468
     2
    Author      : Jacques D. Fleuriot
huffman@27468
     3
    Copyright   : 2001,2002 University of Edinburgh
huffman@27468
     4
*)
huffman@27468
     5
huffman@27468
     6
header{*Non-Standard Complex Analysis*}
huffman@27468
     7
huffman@27468
     8
theory NSCA
haftmann@28952
     9
imports NSComplex HTranscendental
huffman@27468
    10
begin
huffman@27468
    11
huffman@27468
    12
abbreviation
huffman@27468
    13
   (* standard complex numbers reagarded as an embedded subset of NS complex *)
huffman@27468
    14
   SComplex  :: "hcomplex set" where
huffman@27468
    15
   "SComplex \<equiv> Standard"
huffman@27468
    16
huffman@27468
    17
definition --{* standard part map*}
huffman@27468
    18
  stc :: "hcomplex => hcomplex" where 
haftmann@37765
    19
  "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
huffman@27468
    20
huffman@27468
    21
huffman@27468
    22
subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}
huffman@27468
    23
huffman@27468
    24
lemma SComplex_minus_iff [simp]: "(-x \<in> SComplex) = (x \<in> SComplex)"
huffman@27468
    25
by (auto, drule Standard_minus, auto)
huffman@27468
    26
huffman@27468
    27
lemma SComplex_add_cancel:
huffman@27468
    28
     "[| x + y \<in> SComplex; y \<in> SComplex |] ==> x \<in> SComplex"
huffman@27468
    29
by (drule (1) Standard_diff, simp)
huffman@27468
    30
huffman@27468
    31
lemma SReal_hcmod_hcomplex_of_complex [simp]:
huffman@27468
    32
     "hcmod (hcomplex_of_complex r) \<in> Reals"
huffman@27468
    33
by (simp add: Reals_eq_Standard)
huffman@27468
    34
huffman@47108
    35
lemma SReal_hcmod_numeral [simp]: "hcmod (numeral w ::hcomplex) \<in> Reals"
huffman@27468
    36
by (simp add: Reals_eq_Standard)
huffman@27468
    37
huffman@27468
    38
lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> Reals"
huffman@27468
    39
by (simp add: Reals_eq_Standard)
huffman@27468
    40
huffman@47108
    41
lemma SComplex_divide_numeral:
huffman@47108
    42
     "r \<in> SComplex ==> r/(numeral w::hcomplex) \<in> SComplex"
huffman@27468
    43
by simp
huffman@27468
    44
huffman@27468
    45
lemma SComplex_UNIV_complex:
huffman@27468
    46
     "{x. hcomplex_of_complex x \<in> SComplex} = (UNIV::complex set)"
huffman@27468
    47
by simp
huffman@27468
    48
huffman@27468
    49
lemma SComplex_iff: "(x \<in> SComplex) = (\<exists>y. x = hcomplex_of_complex y)"
huffman@27468
    50
by (simp add: Standard_def image_def)
huffman@27468
    51
huffman@27468
    52
lemma hcomplex_of_complex_image:
huffman@27468
    53
     "hcomplex_of_complex `(UNIV::complex set) = SComplex"
huffman@27468
    54
by (simp add: Standard_def)
huffman@27468
    55
huffman@27468
    56
lemma inv_hcomplex_of_complex_image: "inv hcomplex_of_complex `SComplex = UNIV"
huffman@27468
    57
apply (auto simp add: Standard_def image_def)
huffman@27468
    58
apply (rule inj_hcomplex_of_complex [THEN inv_f_f, THEN subst], blast)
huffman@27468
    59
done
huffman@27468
    60
huffman@27468
    61
lemma SComplex_hcomplex_of_complex_image: 
huffman@27468
    62
      "[| \<exists>x. x: P; P \<le> SComplex |] ==> \<exists>Q. P = hcomplex_of_complex ` Q"
huffman@27468
    63
apply (simp add: Standard_def, blast)
huffman@27468
    64
done
huffman@27468
    65
huffman@27468
    66
lemma SComplex_SReal_dense:
huffman@27468
    67
     "[| x \<in> SComplex; y \<in> SComplex; hcmod x < hcmod y  
huffman@27468
    68
      |] ==> \<exists>r \<in> Reals. hcmod x< r & r < hcmod y"
huffman@27468
    69
apply (auto intro: SReal_dense simp add: SReal_hcmod_SComplex)
huffman@27468
    70
done
huffman@27468
    71
huffman@27468
    72
lemma SComplex_hcmod_SReal: 
huffman@27468
    73
      "z \<in> SComplex ==> hcmod z \<in> Reals"
huffman@27468
    74
by (simp add: Reals_eq_Standard)
huffman@27468
    75
huffman@27468
    76
huffman@27468
    77
subsection{*The Finite Elements form a Subring*}
huffman@27468
    78
huffman@27468
    79
lemma HFinite_hcmod_hcomplex_of_complex [simp]:
huffman@27468
    80
     "hcmod (hcomplex_of_complex r) \<in> HFinite"
huffman@27468
    81
by (auto intro!: SReal_subset_HFinite [THEN subsetD])
huffman@27468
    82
huffman@27468
    83
lemma HFinite_hcmod_iff: "(x \<in> HFinite) = (hcmod x \<in> HFinite)"
huffman@27468
    84
by (simp add: HFinite_def)
huffman@27468
    85
huffman@27468
    86
lemma HFinite_bounded_hcmod:
huffman@27468
    87
  "[|x \<in> HFinite; y \<le> hcmod x; 0 \<le> y |] ==> y: HFinite"
huffman@27468
    88
by (auto intro: HFinite_bounded simp add: HFinite_hcmod_iff)
huffman@27468
    89
huffman@27468
    90
huffman@27468
    91
subsection{*The Complex Infinitesimals form a Subring*}
huffman@27468
    92
huffman@27468
    93
lemma hcomplex_sum_of_halves: "x/(2::hcomplex) + x/(2::hcomplex) = x"
huffman@27468
    94
by auto
huffman@27468
    95
huffman@27468
    96
lemma Infinitesimal_hcmod_iff: 
huffman@27468
    97
   "(z \<in> Infinitesimal) = (hcmod z \<in> Infinitesimal)"
huffman@27468
    98
by (simp add: Infinitesimal_def)
huffman@27468
    99
huffman@27468
   100
lemma HInfinite_hcmod_iff: "(z \<in> HInfinite) = (hcmod z \<in> HInfinite)"
huffman@27468
   101
by (simp add: HInfinite_def)
huffman@27468
   102
huffman@27468
   103
lemma HFinite_diff_Infinitesimal_hcmod:
huffman@27468
   104
     "x \<in> HFinite - Infinitesimal ==> hcmod x \<in> HFinite - Infinitesimal"
huffman@27468
   105
by (simp add: HFinite_hcmod_iff Infinitesimal_hcmod_iff)
huffman@27468
   106
huffman@27468
   107
lemma hcmod_less_Infinitesimal:
huffman@27468
   108
     "[| e \<in> Infinitesimal; hcmod x < hcmod e |] ==> x \<in> Infinitesimal"
huffman@27468
   109
by (auto elim: hrabs_less_Infinitesimal simp add: Infinitesimal_hcmod_iff)
huffman@27468
   110
huffman@27468
   111
lemma hcmod_le_Infinitesimal:
huffman@27468
   112
     "[| e \<in> Infinitesimal; hcmod x \<le> hcmod e |] ==> x \<in> Infinitesimal"
huffman@27468
   113
by (auto elim: hrabs_le_Infinitesimal simp add: Infinitesimal_hcmod_iff)
huffman@27468
   114
huffman@27468
   115
lemma Infinitesimal_interval_hcmod:
huffman@27468
   116
     "[| e \<in> Infinitesimal;  
huffman@27468
   117
          e' \<in> Infinitesimal;  
huffman@27468
   118
          hcmod e' < hcmod x ; hcmod x < hcmod e  
huffman@27468
   119
       |] ==> x \<in> Infinitesimal"
huffman@27468
   120
by (auto intro: Infinitesimal_interval simp add: Infinitesimal_hcmod_iff)
huffman@27468
   121
huffman@27468
   122
lemma Infinitesimal_interval2_hcmod:
huffman@27468
   123
     "[| e \<in> Infinitesimal;  
huffman@27468
   124
         e' \<in> Infinitesimal;  
huffman@27468
   125
         hcmod e' \<le> hcmod x ; hcmod x \<le> hcmod e  
huffman@27468
   126
      |] ==> x \<in> Infinitesimal"
huffman@27468
   127
by (auto intro: Infinitesimal_interval2 simp add: Infinitesimal_hcmod_iff)
huffman@27468
   128
huffman@27468
   129
huffman@27468
   130
subsection{*The ``Infinitely Close'' Relation*}
huffman@27468
   131
huffman@27468
   132
(*
huffman@27468
   133
Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z @= hcmod w)"
huffman@27468
   134
by (auto_tac (claset(),simpset() addsimps [Infinitesimal_hcmod_iff]));
huffman@27468
   135
*)
huffman@27468
   136
huffman@27468
   137
lemma approx_SComplex_mult_cancel_zero:
huffman@27468
   138
     "[| a \<in> SComplex; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
huffman@27468
   139
apply (drule Standard_inverse [THEN Standard_subset_HFinite [THEN subsetD]])
huffman@27468
   140
apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric])
huffman@27468
   141
done
huffman@27468
   142
huffman@27468
   143
lemma approx_mult_SComplex1: "[| a \<in> SComplex; x @= 0 |] ==> x*a @= 0"
huffman@27468
   144
by (auto dest: Standard_subset_HFinite [THEN subsetD] approx_mult1)
huffman@27468
   145
huffman@27468
   146
lemma approx_mult_SComplex2: "[| a \<in> SComplex; x @= 0 |] ==> a*x @= 0"
huffman@27468
   147
by (auto dest: Standard_subset_HFinite [THEN subsetD] approx_mult2)
huffman@27468
   148
huffman@27468
   149
lemma approx_mult_SComplex_zero_cancel_iff [simp]:
huffman@27468
   150
     "[|a \<in> SComplex; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
huffman@27468
   151
by (blast intro: approx_SComplex_mult_cancel_zero approx_mult_SComplex2)
huffman@27468
   152
huffman@27468
   153
lemma approx_SComplex_mult_cancel:
huffman@27468
   154
     "[| a \<in> SComplex; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
huffman@27468
   155
apply (drule Standard_inverse [THEN Standard_subset_HFinite [THEN subsetD]])
huffman@27468
   156
apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric])
huffman@27468
   157
done
huffman@27468
   158
huffman@27468
   159
lemma approx_SComplex_mult_cancel_iff1 [simp]:
huffman@27468
   160
     "[| a \<in> SComplex; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
huffman@27468
   161
by (auto intro!: approx_mult2 Standard_subset_HFinite [THEN subsetD]
huffman@27468
   162
            intro: approx_SComplex_mult_cancel)
huffman@27468
   163
huffman@27468
   164
(* TODO: generalize following theorems: hcmod -> hnorm *)
huffman@27468
   165
huffman@27468
   166
lemma approx_hcmod_approx_zero: "(x @= y) = (hcmod (y - x) @= 0)"
huffman@27468
   167
apply (subst hnorm_minus_commute)
huffman@27468
   168
apply (simp add: approx_def Infinitesimal_hcmod_iff diff_minus)
huffman@27468
   169
done
huffman@27468
   170
huffman@27468
   171
lemma approx_approx_zero_iff: "(x @= 0) = (hcmod x @= 0)"
huffman@27468
   172
by (simp add: approx_hcmod_approx_zero)
huffman@27468
   173
huffman@27468
   174
lemma approx_minus_zero_cancel_iff [simp]: "(-x @= 0) = (x @= 0)"
huffman@27468
   175
by (simp add: approx_def)
huffman@27468
   176
huffman@27468
   177
lemma Infinitesimal_hcmod_add_diff:
huffman@27468
   178
     "u @= 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal"
huffman@27468
   179
apply (drule approx_approx_zero_iff [THEN iffD1])
huffman@27468
   180
apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2)
haftmann@37887
   181
apply (auto simp add: mem_infmal_iff [symmetric] diff_minus)
huffman@27468
   182
apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1])
huffman@27468
   183
apply (auto simp add: diff_minus [symmetric])
huffman@27468
   184
done
huffman@27468
   185
huffman@27468
   186
lemma approx_hcmod_add_hcmod: "u @= 0 ==> hcmod(x + u) @= hcmod x"
huffman@27468
   187
apply (rule approx_minus_iff [THEN iffD2])
huffman@27468
   188
apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric] diff_minus [symmetric])
huffman@27468
   189
done
huffman@27468
   190
huffman@27468
   191
huffman@27468
   192
subsection{*Zero is the Only Infinitesimal Complex Number*}
huffman@27468
   193
huffman@27468
   194
lemma Infinitesimal_less_SComplex:
huffman@27468
   195
   "[| x \<in> SComplex; y \<in> Infinitesimal; 0 < hcmod x |] ==> hcmod y < hcmod x"
huffman@27468
   196
by (auto intro: Infinitesimal_less_SReal SComplex_hcmod_SReal simp add: Infinitesimal_hcmod_iff)
huffman@27468
   197
huffman@27468
   198
lemma SComplex_Int_Infinitesimal_zero: "SComplex Int Infinitesimal = {0}"
huffman@27468
   199
by (auto simp add: Standard_def Infinitesimal_hcmod_iff)
huffman@27468
   200
huffman@27468
   201
lemma SComplex_Infinitesimal_zero:
huffman@27468
   202
     "[| x \<in> SComplex; x \<in> Infinitesimal|] ==> x = 0"
huffman@27468
   203
by (cut_tac SComplex_Int_Infinitesimal_zero, blast)
huffman@27468
   204
huffman@27468
   205
lemma SComplex_HFinite_diff_Infinitesimal:
huffman@27468
   206
     "[| x \<in> SComplex; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"
huffman@27468
   207
by (auto dest: SComplex_Infinitesimal_zero Standard_subset_HFinite [THEN subsetD])
huffman@27468
   208
huffman@27468
   209
lemma hcomplex_of_complex_HFinite_diff_Infinitesimal:
huffman@27468
   210
     "hcomplex_of_complex x \<noteq> 0 
huffman@27468
   211
      ==> hcomplex_of_complex x \<in> HFinite - Infinitesimal"
huffman@27468
   212
by (rule SComplex_HFinite_diff_Infinitesimal, auto)
huffman@27468
   213
huffman@47108
   214
lemma numeral_not_Infinitesimal [simp]:
huffman@47108
   215
     "numeral w \<noteq> (0::hcomplex) ==> (numeral w::hcomplex) \<notin> Infinitesimal"
huffman@47108
   216
by (fast dest: Standard_numeral [THEN SComplex_Infinitesimal_zero])
huffman@27468
   217
huffman@27468
   218
lemma approx_SComplex_not_zero:
huffman@27468
   219
     "[| y \<in> SComplex; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
huffman@27468
   220
by (auto dest: SComplex_Infinitesimal_zero approx_sym [THEN mem_infmal_iff [THEN iffD2]])
huffman@27468
   221
huffman@27468
   222
lemma SComplex_approx_iff:
huffman@27468
   223
     "[|x \<in> SComplex; y \<in> SComplex|] ==> (x @= y) = (x = y)"
huffman@27468
   224
by (auto simp add: Standard_def)
huffman@27468
   225
huffman@47108
   226
lemma numeral_Infinitesimal_iff [simp]:
huffman@47108
   227
     "((numeral w :: hcomplex) \<in> Infinitesimal) =
huffman@47108
   228
      (numeral w = (0::hcomplex))"
huffman@27468
   229
apply (rule iffI)
huffman@47108
   230
apply (fast dest: Standard_numeral [THEN SComplex_Infinitesimal_zero])
huffman@27468
   231
apply (simp (no_asm_simp))
huffman@27468
   232
done
huffman@27468
   233
huffman@27468
   234
lemma approx_unique_complex:
huffman@27468
   235
     "[| r \<in> SComplex; s \<in> SComplex; r @= x; s @= x|] ==> r = s"
huffman@27468
   236
by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2)
huffman@27468
   237
huffman@27468
   238
subsection {* Properties of @{term hRe}, @{term hIm} and @{term HComplex} *}
huffman@27468
   239
huffman@27468
   240
huffman@27468
   241
lemma abs_hRe_le_hcmod: "\<And>x. \<bar>hRe x\<bar> \<le> hcmod x"
huffman@27468
   242
by transfer (rule abs_Re_le_cmod)
huffman@27468
   243
huffman@27468
   244
lemma abs_hIm_le_hcmod: "\<And>x. \<bar>hIm x\<bar> \<le> hcmod x"
huffman@27468
   245
by transfer (rule abs_Im_le_cmod)
huffman@27468
   246
huffman@27468
   247
lemma Infinitesimal_hRe: "x \<in> Infinitesimal \<Longrightarrow> hRe x \<in> Infinitesimal"
huffman@27468
   248
apply (rule InfinitesimalI2, simp)
huffman@27468
   249
apply (rule order_le_less_trans [OF abs_hRe_le_hcmod])
huffman@27468
   250
apply (erule (1) InfinitesimalD2)
huffman@27468
   251
done
huffman@27468
   252
huffman@27468
   253
lemma Infinitesimal_hIm: "x \<in> Infinitesimal \<Longrightarrow> hIm x \<in> Infinitesimal"
huffman@27468
   254
apply (rule InfinitesimalI2, simp)
huffman@27468
   255
apply (rule order_le_less_trans [OF abs_hIm_le_hcmod])
huffman@27468
   256
apply (erule (1) InfinitesimalD2)
huffman@27468
   257
done
huffman@27468
   258
huffman@27468
   259
lemma real_sqrt_lessI: "\<lbrakk>0 < u; x < u\<twosuperior>\<rbrakk> \<Longrightarrow> sqrt x < u"
huffman@27468
   260
(* TODO: this belongs somewhere else *)
huffman@27468
   261
by (frule real_sqrt_less_mono) simp
huffman@27468
   262
huffman@27468
   263
lemma hypreal_sqrt_lessI:
huffman@27468
   264
  "\<And>x u. \<lbrakk>0 < u; x < u\<twosuperior>\<rbrakk> \<Longrightarrow> ( *f* sqrt) x < u"
huffman@27468
   265
by transfer (rule real_sqrt_lessI)
huffman@27468
   266
 
huffman@27468
   267
lemma hypreal_sqrt_ge_zero: "\<And>x. 0 \<le> x \<Longrightarrow> 0 \<le> ( *f* sqrt) x"
huffman@27468
   268
by transfer (rule real_sqrt_ge_zero)
huffman@27468
   269
huffman@27468
   270
lemma Infinitesimal_sqrt:
huffman@27468
   271
  "\<lbrakk>x \<in> Infinitesimal; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> Infinitesimal"
huffman@27468
   272
apply (rule InfinitesimalI2)
huffman@27468
   273
apply (drule_tac r="r\<twosuperior>" in InfinitesimalD2, simp)
huffman@27468
   274
apply (simp add: hypreal_sqrt_ge_zero)
huffman@27468
   275
apply (rule hypreal_sqrt_lessI, simp_all)
huffman@27468
   276
done
huffman@27468
   277
huffman@27468
   278
lemma Infinitesimal_HComplex:
huffman@27468
   279
  "\<lbrakk>x \<in> Infinitesimal; y \<in> Infinitesimal\<rbrakk> \<Longrightarrow> HComplex x y \<in> Infinitesimal"
huffman@27468
   280
apply (rule Infinitesimal_hcmod_iff [THEN iffD2])
huffman@27468
   281
apply (simp add: hcmod_i)
huffman@27468
   282
apply (rule Infinitesimal_add)
huffman@27468
   283
apply (erule Infinitesimal_hrealpow, simp)
huffman@27468
   284
apply (erule Infinitesimal_hrealpow, simp)
huffman@27468
   285
done
huffman@27468
   286
huffman@27468
   287
lemma hcomplex_Infinitesimal_iff:
huffman@27468
   288
  "(x \<in> Infinitesimal) = (hRe x \<in> Infinitesimal \<and> hIm x \<in> Infinitesimal)"
huffman@27468
   289
apply (safe intro!: Infinitesimal_hRe Infinitesimal_hIm)
huffman@27468
   290
apply (drule (1) Infinitesimal_HComplex, simp)
huffman@27468
   291
done
huffman@27468
   292
huffman@27468
   293
lemma hRe_diff [simp]: "\<And>x y. hRe (x - y) = hRe x - hRe y"
huffman@27468
   294
by transfer (rule complex_Re_diff)
huffman@27468
   295
huffman@27468
   296
lemma hIm_diff [simp]: "\<And>x y. hIm (x - y) = hIm x - hIm y"
huffman@27468
   297
by transfer (rule complex_Im_diff)
huffman@27468
   298
huffman@27468
   299
lemma approx_hRe: "x \<approx> y \<Longrightarrow> hRe x \<approx> hRe y"
huffman@27468
   300
unfolding approx_def by (drule Infinitesimal_hRe) simp
huffman@27468
   301
huffman@27468
   302
lemma approx_hIm: "x \<approx> y \<Longrightarrow> hIm x \<approx> hIm y"
huffman@27468
   303
unfolding approx_def by (drule Infinitesimal_hIm) simp
huffman@27468
   304
huffman@27468
   305
lemma approx_HComplex:
huffman@27468
   306
  "\<lbrakk>a \<approx> b; c \<approx> d\<rbrakk> \<Longrightarrow> HComplex a c \<approx> HComplex b d"
huffman@27468
   307
unfolding approx_def by (simp add: Infinitesimal_HComplex)
huffman@27468
   308
huffman@27468
   309
lemma hcomplex_approx_iff:
huffman@27468
   310
  "(x \<approx> y) = (hRe x \<approx> hRe y \<and> hIm x \<approx> hIm y)"
huffman@27468
   311
unfolding approx_def by (simp add: hcomplex_Infinitesimal_iff)
huffman@27468
   312
huffman@27468
   313
lemma HFinite_hRe: "x \<in> HFinite \<Longrightarrow> hRe x \<in> HFinite"
huffman@27468
   314
apply (auto simp add: HFinite_def SReal_def)
huffman@27468
   315
apply (rule_tac x="star_of r" in exI, simp)
huffman@27468
   316
apply (erule order_le_less_trans [OF abs_hRe_le_hcmod])
huffman@27468
   317
done
huffman@27468
   318
huffman@27468
   319
lemma HFinite_hIm: "x \<in> HFinite \<Longrightarrow> hIm x \<in> HFinite"
huffman@27468
   320
apply (auto simp add: HFinite_def SReal_def)
huffman@27468
   321
apply (rule_tac x="star_of r" in exI, simp)
huffman@27468
   322
apply (erule order_le_less_trans [OF abs_hIm_le_hcmod])
huffman@27468
   323
done
huffman@27468
   324
huffman@27468
   325
lemma HFinite_HComplex:
huffman@27468
   326
  "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> HComplex x y \<in> HFinite"
huffman@27468
   327
apply (subgoal_tac "HComplex x 0 + HComplex 0 y \<in> HFinite", simp)
huffman@27468
   328
apply (rule HFinite_add)
huffman@27468
   329
apply (simp add: HFinite_hcmod_iff hcmod_i)
huffman@27468
   330
apply (simp add: HFinite_hcmod_iff hcmod_i)
huffman@27468
   331
done
huffman@27468
   332
huffman@27468
   333
lemma hcomplex_HFinite_iff:
huffman@27468
   334
  "(x \<in> HFinite) = (hRe x \<in> HFinite \<and> hIm x \<in> HFinite)"
huffman@27468
   335
apply (safe intro!: HFinite_hRe HFinite_hIm)
huffman@27468
   336
apply (drule (1) HFinite_HComplex, simp)
huffman@27468
   337
done
huffman@27468
   338
huffman@27468
   339
lemma hcomplex_HInfinite_iff:
huffman@27468
   340
  "(x \<in> HInfinite) = (hRe x \<in> HInfinite \<or> hIm x \<in> HInfinite)"
huffman@27468
   341
by (simp add: HInfinite_HFinite_iff hcomplex_HFinite_iff)
huffman@27468
   342
huffman@27468
   343
lemma hcomplex_of_hypreal_approx_iff [simp]:
huffman@27468
   344
     "(hcomplex_of_hypreal x @= hcomplex_of_hypreal z) = (x @= z)"
huffman@27468
   345
by (simp add: hcomplex_approx_iff)
huffman@27468
   346
huffman@27468
   347
lemma Standard_HComplex:
huffman@27468
   348
  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> HComplex x y \<in> Standard"
huffman@27468
   349
by (simp add: HComplex_def)
huffman@27468
   350
huffman@27468
   351
(* Here we go - easy proof now!! *)
huffman@27468
   352
lemma stc_part_Ex: "x:HFinite ==> \<exists>t \<in> SComplex. x @= t"
huffman@27468
   353
apply (simp add: hcomplex_HFinite_iff hcomplex_approx_iff)
huffman@27468
   354
apply (rule_tac x="HComplex (st (hRe x)) (st (hIm x))" in bexI)
huffman@27468
   355
apply (simp add: st_approx_self [THEN approx_sym])
huffman@27468
   356
apply (simp add: Standard_HComplex st_SReal [unfolded Reals_eq_Standard])
huffman@27468
   357
done
huffman@27468
   358
huffman@27468
   359
lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \<in> SComplex &  x @= t"
huffman@27468
   360
apply (drule stc_part_Ex, safe)
huffman@27468
   361
apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
huffman@27468
   362
apply (auto intro!: approx_unique_complex)
huffman@27468
   363
done
huffman@27468
   364
huffman@27468
   365
lemmas hcomplex_of_complex_approx_inverse =
huffman@27468
   366
  hcomplex_of_complex_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
huffman@27468
   367
huffman@27468
   368
huffman@27468
   369
subsection{*Theorems About Monads*}
huffman@27468
   370
huffman@27468
   371
lemma monad_zero_hcmod_iff: "(x \<in> monad 0) = (hcmod x:monad 0)"
huffman@27468
   372
by (simp add: Infinitesimal_monad_zero_iff [symmetric] Infinitesimal_hcmod_iff)
huffman@27468
   373
huffman@27468
   374
huffman@27468
   375
subsection{*Theorems About Standard Part*}
huffman@27468
   376
huffman@27468
   377
lemma stc_approx_self: "x \<in> HFinite ==> stc x @= x"
huffman@27468
   378
apply (simp add: stc_def)
huffman@27468
   379
apply (frule stc_part_Ex, safe)
huffman@27468
   380
apply (rule someI2)
huffman@27468
   381
apply (auto intro: approx_sym)
huffman@27468
   382
done
huffman@27468
   383
huffman@27468
   384
lemma stc_SComplex: "x \<in> HFinite ==> stc x \<in> SComplex"
huffman@27468
   385
apply (simp add: stc_def)
huffman@27468
   386
apply (frule stc_part_Ex, safe)
huffman@27468
   387
apply (rule someI2)
huffman@27468
   388
apply (auto intro: approx_sym)
huffman@27468
   389
done
huffman@27468
   390
huffman@27468
   391
lemma stc_HFinite: "x \<in> HFinite ==> stc x \<in> HFinite"
huffman@27468
   392
by (erule stc_SComplex [THEN Standard_subset_HFinite [THEN subsetD]])
huffman@27468
   393
huffman@27468
   394
lemma stc_unique: "\<lbrakk>y \<in> SComplex; y \<approx> x\<rbrakk> \<Longrightarrow> stc x = y"
huffman@27468
   395
apply (frule Standard_subset_HFinite [THEN subsetD])
huffman@27468
   396
apply (drule (1) approx_HFinite)
huffman@27468
   397
apply (unfold stc_def)
huffman@27468
   398
apply (rule some_equality)
huffman@27468
   399
apply (auto intro: approx_unique_complex)
huffman@27468
   400
done
huffman@27468
   401
huffman@27468
   402
lemma stc_SComplex_eq [simp]: "x \<in> SComplex ==> stc x = x"
huffman@27468
   403
apply (erule stc_unique)
huffman@27468
   404
apply (rule approx_refl)
huffman@27468
   405
done
huffman@27468
   406
huffman@27468
   407
lemma stc_hcomplex_of_complex:
huffman@27468
   408
     "stc (hcomplex_of_complex x) = hcomplex_of_complex x"
huffman@27468
   409
by auto
huffman@27468
   410
huffman@27468
   411
lemma stc_eq_approx:
huffman@27468
   412
     "[| x \<in> HFinite; y \<in> HFinite; stc x = stc y |] ==> x @= y"
huffman@27468
   413
by (auto dest!: stc_approx_self elim!: approx_trans3)
huffman@27468
   414
huffman@27468
   415
lemma approx_stc_eq:
huffman@27468
   416
     "[| x \<in> HFinite; y \<in> HFinite; x @= y |] ==> stc x = stc y"
huffman@27468
   417
by (blast intro: approx_trans approx_trans2 SComplex_approx_iff [THEN iffD1]
huffman@27468
   418
          dest: stc_approx_self stc_SComplex)
huffman@27468
   419
huffman@27468
   420
lemma stc_eq_approx_iff:
huffman@27468
   421
     "[| x \<in> HFinite; y \<in> HFinite|] ==> (x @= y) = (stc x = stc y)"
huffman@27468
   422
by (blast intro: approx_stc_eq stc_eq_approx)
huffman@27468
   423
huffman@27468
   424
lemma stc_Infinitesimal_add_SComplex:
huffman@27468
   425
     "[| x \<in> SComplex; e \<in> Infinitesimal |] ==> stc(x + e) = x"
huffman@27468
   426
apply (erule stc_unique)
huffman@27468
   427
apply (erule Infinitesimal_add_approx_self)
huffman@27468
   428
done
huffman@27468
   429
huffman@27468
   430
lemma stc_Infinitesimal_add_SComplex2:
huffman@27468
   431
     "[| x \<in> SComplex; e \<in> Infinitesimal |] ==> stc(e + x) = x"
huffman@27468
   432
apply (erule stc_unique)
huffman@27468
   433
apply (erule Infinitesimal_add_approx_self2)
huffman@27468
   434
done
huffman@27468
   435
huffman@27468
   436
lemma HFinite_stc_Infinitesimal_add:
huffman@27468
   437
     "x \<in> HFinite ==> \<exists>e \<in> Infinitesimal. x = stc(x) + e"
huffman@27468
   438
by (blast dest!: stc_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2])
huffman@27468
   439
huffman@27468
   440
lemma stc_add:
huffman@27468
   441
     "[| x \<in> HFinite; y \<in> HFinite |] ==> stc (x + y) = stc(x) + stc(y)"
huffman@27468
   442
by (simp add: stc_unique stc_SComplex stc_approx_self approx_add)
huffman@27468
   443
huffman@47108
   444
lemma stc_numeral [simp]: "stc (numeral w) = numeral w"
huffman@47108
   445
by (rule Standard_numeral [THEN stc_SComplex_eq])
huffman@27468
   446
huffman@27468
   447
lemma stc_zero [simp]: "stc 0 = 0"
huffman@27468
   448
by simp
huffman@27468
   449
huffman@27468
   450
lemma stc_one [simp]: "stc 1 = 1"
huffman@27468
   451
by simp
huffman@27468
   452
huffman@27468
   453
lemma stc_minus: "y \<in> HFinite ==> stc(-y) = -stc(y)"
huffman@27468
   454
by (simp add: stc_unique stc_SComplex stc_approx_self approx_minus)
huffman@27468
   455
huffman@27468
   456
lemma stc_diff: 
huffman@27468
   457
     "[| x \<in> HFinite; y \<in> HFinite |] ==> stc (x-y) = stc(x) - stc(y)"
huffman@27468
   458
by (simp add: stc_unique stc_SComplex stc_approx_self approx_diff)
huffman@27468
   459
huffman@27468
   460
lemma stc_mult:
huffman@27468
   461
     "[| x \<in> HFinite; y \<in> HFinite |]  
huffman@27468
   462
               ==> stc (x * y) = stc(x) * stc(y)"
huffman@27468
   463
by (simp add: stc_unique stc_SComplex stc_approx_self approx_mult_HFinite)
huffman@27468
   464
huffman@27468
   465
lemma stc_Infinitesimal: "x \<in> Infinitesimal ==> stc x = 0"
huffman@27468
   466
by (simp add: stc_unique mem_infmal_iff)
huffman@27468
   467
huffman@27468
   468
lemma stc_not_Infinitesimal: "stc(x) \<noteq> 0 ==> x \<notin> Infinitesimal"
huffman@27468
   469
by (fast intro: stc_Infinitesimal)
huffman@27468
   470
huffman@27468
   471
lemma stc_inverse:
huffman@27468
   472
     "[| x \<in> HFinite; stc x \<noteq> 0 |]  
huffman@27468
   473
      ==> stc(inverse x) = inverse (stc x)"
huffman@27468
   474
apply (drule stc_not_Infinitesimal)
huffman@27468
   475
apply (simp add: stc_unique stc_SComplex stc_approx_self approx_inverse)
huffman@27468
   476
done
huffman@27468
   477
huffman@27468
   478
lemma stc_divide [simp]:
huffman@27468
   479
     "[| x \<in> HFinite; y \<in> HFinite; stc y \<noteq> 0 |]  
huffman@27468
   480
      ==> stc(x/y) = (stc x) / (stc y)"
huffman@27468
   481
by (simp add: divide_inverse stc_mult stc_not_Infinitesimal HFinite_inverse stc_inverse)
huffman@27468
   482
huffman@27468
   483
lemma stc_idempotent [simp]: "x \<in> HFinite ==> stc(stc(x)) = stc(x)"
huffman@27468
   484
by (blast intro: stc_HFinite stc_approx_self approx_stc_eq)
huffman@27468
   485
huffman@27468
   486
lemma HFinite_HFinite_hcomplex_of_hypreal:
huffman@27468
   487
     "z \<in> HFinite ==> hcomplex_of_hypreal z \<in> HFinite"
huffman@27468
   488
by (simp add: hcomplex_HFinite_iff)
huffman@27468
   489
huffman@27468
   490
lemma SComplex_SReal_hcomplex_of_hypreal:
huffman@27468
   491
     "x \<in> Reals ==>  hcomplex_of_hypreal x \<in> SComplex"
huffman@27468
   492
apply (rule Standard_of_hypreal)
huffman@27468
   493
apply (simp add: Reals_eq_Standard)
huffman@27468
   494
done
huffman@27468
   495
huffman@27468
   496
lemma stc_hcomplex_of_hypreal: 
huffman@27468
   497
 "z \<in> HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)"
huffman@27468
   498
apply (rule stc_unique)
huffman@27468
   499
apply (rule SComplex_SReal_hcomplex_of_hypreal)
huffman@27468
   500
apply (erule st_SReal)
huffman@27468
   501
apply (simp add: hcomplex_of_hypreal_approx_iff st_approx_self)
huffman@27468
   502
done
huffman@27468
   503
huffman@27468
   504
(*
huffman@27468
   505
Goal "x \<in> HFinite ==> hcmod(stc x) = st(hcmod x)"
huffman@27468
   506
by (dtac stc_approx_self 1)
huffman@27468
   507
by (auto_tac (claset(),simpset() addsimps [bex_Infinitesimal_iff2 RS sym]));
huffman@27468
   508
huffman@27468
   509
huffman@27468
   510
approx_hcmod_add_hcmod
huffman@27468
   511
*)
huffman@27468
   512
huffman@27468
   513
lemma Infinitesimal_hcnj_iff [simp]:
huffman@27468
   514
     "(hcnj z \<in> Infinitesimal) = (z \<in> Infinitesimal)"
huffman@27468
   515
by (simp add: Infinitesimal_hcmod_iff)
huffman@27468
   516
huffman@27468
   517
lemma Infinitesimal_hcomplex_of_hypreal_epsilon [simp]:
huffman@27468
   518
     "hcomplex_of_hypreal epsilon \<in> Infinitesimal"
huffman@27468
   519
by (simp add: Infinitesimal_hcmod_iff)
huffman@27468
   520
huffman@27468
   521
end