src/HOL/Complex/NSCA.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15229 1eb23f805c06
permissions -rw-r--r--
import -> imports
paulson@13957
     1
(*  Title       : NSCA.thy
paulson@13957
     2
    Author      : Jacques D. Fleuriot
paulson@13957
     3
    Copyright   : 2001,2002 University of Edinburgh
paulson@13957
     4
*)
paulson@13957
     5
paulson@14408
     6
header{*Non-Standard Complex Analysis*}
paulson@13957
     7
nipkow@15131
     8
theory NSCA
nipkow@15140
     9
imports NSComplex
nipkow@15131
    10
begin
paulson@13957
    11
paulson@14408
    12
constdefs
paulson@13957
    13
wenzelm@14653
    14
   CInfinitesimal  :: "hcomplex set"
wenzelm@14653
    15
   "CInfinitesimal == {x. \<forall>r \<in> Reals. 0 < r --> hcmod x < r}"
wenzelm@14653
    16
paulson@14408
    17
    capprox    :: "[hcomplex,hcomplex] => bool"  (infixl "@c=" 50)  
paulson@14408
    18
      --{*the ``infinitely close'' relation*}
paulson@14408
    19
      "x @c= y == (x - y) \<in> CInfinitesimal"     
paulson@13957
    20
  
paulson@13957
    21
   (* standard complex numbers reagarded as an embedded subset of NS complex *)
paulson@13957
    22
   SComplex  :: "hcomplex set"
paulson@14408
    23
   "SComplex == {x. \<exists>r. x = hcomplex_of_complex r}"
paulson@13957
    24
paulson@13957
    25
   CFinite :: "hcomplex set"
paulson@14408
    26
   "CFinite == {x. \<exists>r \<in> Reals. hcmod x < r}"
paulson@13957
    27
paulson@13957
    28
   CInfinite :: "hcomplex set"
paulson@14408
    29
   "CInfinite == {x. \<forall>r \<in> Reals. r < hcmod x}"
paulson@13957
    30
paulson@14408
    31
   stc :: "hcomplex => hcomplex"
paulson@14408
    32
    --{* standard part map*}
paulson@14408
    33
   "stc x == (@r. x \<in> CFinite & r:SComplex & r @c= x)"
paulson@13957
    34
paulson@14408
    35
   cmonad    :: "hcomplex => hcomplex set"
paulson@13957
    36
   "cmonad x  == {y. x @c= y}"
paulson@13957
    37
paulson@14408
    38
   cgalaxy   :: "hcomplex => hcomplex set"
paulson@14408
    39
   "cgalaxy x == {y. (x - y) \<in> CFinite}"
paulson@14408
    40
paulson@14408
    41
paulson@14408
    42
paulson@14408
    43
subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}
paulson@14408
    44
paulson@14408
    45
lemma SComplex_add: "[| x \<in> SComplex; y \<in> SComplex |] ==> x + y \<in> SComplex"
paulson@14408
    46
apply (simp add: SComplex_def, safe)
paulson@14408
    47
apply (rule_tac x = "r + ra" in exI, simp)
paulson@14408
    48
done
paulson@14408
    49
paulson@14408
    50
lemma SComplex_mult: "[| x \<in> SComplex; y \<in> SComplex |] ==> x * y \<in> SComplex"
paulson@14408
    51
apply (simp add: SComplex_def, safe)
paulson@14408
    52
apply (rule_tac x = "r * ra" in exI, simp)
paulson@14408
    53
done
paulson@14408
    54
paulson@14408
    55
lemma SComplex_inverse: "x \<in> SComplex ==> inverse x \<in> SComplex"
paulson@14408
    56
apply (simp add: SComplex_def)
paulson@14408
    57
apply (blast intro: hcomplex_of_complex_inverse [symmetric])
paulson@14408
    58
done
paulson@14408
    59
paulson@14408
    60
lemma SComplex_divide: "[| x \<in> SComplex;  y \<in> SComplex |] ==> x/y \<in> SComplex"
paulson@14430
    61
by (simp add: SComplex_mult SComplex_inverse divide_inverse)
paulson@14408
    62
paulson@14408
    63
lemma SComplex_minus: "x \<in> SComplex ==> -x \<in> SComplex"
paulson@14408
    64
apply (simp add: SComplex_def)
paulson@14408
    65
apply (blast intro: hcomplex_of_complex_minus [symmetric])
paulson@14408
    66
done
paulson@14408
    67
paulson@14408
    68
lemma SComplex_minus_iff [simp]: "(-x \<in> SComplex) = (x \<in> SComplex)"
paulson@14408
    69
apply auto
paulson@14408
    70
apply (erule_tac [2] SComplex_minus)
paulson@14408
    71
apply (drule SComplex_minus, auto)
paulson@14408
    72
done
paulson@14408
    73
paulson@14408
    74
lemma SComplex_diff: "[| x \<in> SComplex; y \<in> SComplex |] ==> x - y \<in> SComplex"
paulson@14408
    75
by (simp add: diff_minus SComplex_add) 
paulson@14408
    76
paulson@14408
    77
lemma SComplex_add_cancel:
paulson@14408
    78
     "[| x + y \<in> SComplex; y \<in> SComplex |] ==> x \<in> SComplex"
paulson@14408
    79
by (drule SComplex_diff, assumption, simp)
paulson@14408
    80
paulson@14408
    81
lemma SReal_hcmod_hcomplex_of_complex [simp]:
paulson@14408
    82
     "hcmod (hcomplex_of_complex r) \<in> Reals"
paulson@14408
    83
by (simp add: hcomplex_of_complex_def hcmod SReal_def hypreal_of_real_def)
paulson@14408
    84
paulson@14408
    85
lemma SReal_hcmod_number_of [simp]: "hcmod (number_of w ::hcomplex) \<in> Reals"
paulson@14408
    86
apply (subst hcomplex_number_of [symmetric])
paulson@14408
    87
apply (rule SReal_hcmod_hcomplex_of_complex)
paulson@14408
    88
done
paulson@14408
    89
paulson@14408
    90
lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> Reals"
paulson@14408
    91
by (auto simp add: SComplex_def)
paulson@14408
    92
paulson@14408
    93
lemma SComplex_hcomplex_of_complex [simp]: "hcomplex_of_complex x \<in> SComplex"
paulson@14408
    94
by (simp add: SComplex_def)
paulson@14408
    95
paulson@14408
    96
lemma SComplex_number_of [simp]: "(number_of w ::hcomplex) \<in> SComplex"
paulson@14408
    97
apply (subst hcomplex_number_of [symmetric])
paulson@14408
    98
apply (rule SComplex_hcomplex_of_complex)
paulson@14408
    99
done
paulson@14408
   100
paulson@14408
   101
lemma SComplex_divide_number_of:
paulson@14408
   102
     "r \<in> SComplex ==> r/(number_of w::hcomplex) \<in> SComplex"
paulson@14430
   103
apply (simp only: divide_inverse)
paulson@14408
   104
apply (blast intro!: SComplex_number_of SComplex_mult SComplex_inverse)
paulson@14408
   105
done
paulson@14408
   106
paulson@14408
   107
lemma SComplex_UNIV_complex:
paulson@14408
   108
     "{x. hcomplex_of_complex x \<in> SComplex} = (UNIV::complex set)"
paulson@14408
   109
by (simp add: SComplex_def)
paulson@14408
   110
paulson@14408
   111
lemma SComplex_iff: "(x \<in> SComplex) = (\<exists>y. x = hcomplex_of_complex y)"
paulson@14408
   112
by (simp add: SComplex_def)
paulson@14408
   113
paulson@14408
   114
lemma hcomplex_of_complex_image:
paulson@14408
   115
     "hcomplex_of_complex `(UNIV::complex set) = SComplex"
paulson@14408
   116
by (auto simp add: SComplex_def)
paulson@14408
   117
paulson@14408
   118
lemma inv_hcomplex_of_complex_image: "inv hcomplex_of_complex `SComplex = UNIV"
paulson@14408
   119
apply (auto simp add: SComplex_def)
paulson@14408
   120
apply (rule inj_hcomplex_of_complex [THEN inv_f_f, THEN subst], blast)
paulson@14408
   121
done
paulson@14408
   122
paulson@14408
   123
lemma SComplex_hcomplex_of_complex_image: 
paulson@14408
   124
      "[| \<exists>x. x: P; P \<le> SComplex |] ==> \<exists>Q. P = hcomplex_of_complex ` Q"
paulson@14408
   125
apply (simp add: SComplex_def, blast)
paulson@14408
   126
done
paulson@14408
   127
paulson@14408
   128
lemma SComplex_SReal_dense:
paulson@14408
   129
     "[| x \<in> SComplex; y \<in> SComplex; hcmod x < hcmod y  
paulson@14408
   130
      |] ==> \<exists>r \<in> Reals. hcmod x< r & r < hcmod y"
paulson@14408
   131
apply (auto intro: SReal_dense simp add: SReal_hcmod_SComplex)
paulson@14408
   132
done
paulson@14408
   133
paulson@14408
   134
lemma SComplex_hcmod_SReal: 
paulson@14408
   135
      "z \<in> SComplex ==> hcmod z \<in> Reals"
paulson@14408
   136
apply (simp add: SComplex_def SReal_def)
paulson@14408
   137
apply (rule_tac z = z in eq_Abs_hcomplex)
paulson@14408
   138
apply (auto simp add: hcmod hypreal_of_real_def hcomplex_of_complex_def cmod_def)
paulson@14408
   139
apply (rule_tac x = "cmod r" in exI)
paulson@14408
   140
apply (simp add: cmod_def, ultra)
paulson@14408
   141
done
paulson@14408
   142
paulson@14408
   143
lemma SComplex_zero [simp]: "0 \<in> SComplex"
paulson@14408
   144
by (simp add: SComplex_def hcomplex_of_complex_zero_iff)
paulson@14408
   145
paulson@14408
   146
lemma SComplex_one [simp]: "1 \<in> SComplex"
paulson@14408
   147
by (simp add: SComplex_def hcomplex_of_complex_def hcomplex_one_def)
paulson@14408
   148
paulson@14408
   149
(*
paulson@14408
   150
Goalw [SComplex_def,SReal_def] "hcmod z \<in> Reals ==> z \<in> SComplex"
paulson@14408
   151
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
paulson@14408
   152
by (auto_tac (claset(),simpset() addsimps [hcmod,hypreal_of_real_def,
paulson@14408
   153
    hcomplex_of_complex_def,cmod_def]));
paulson@14408
   154
*)
paulson@14408
   155
paulson@14408
   156
paulson@14408
   157
subsection{*The Finite Elements form a Subring*}
paulson@14408
   158
paulson@14408
   159
lemma CFinite_add: "[|x \<in> CFinite; y \<in> CFinite|] ==> (x+y) \<in> CFinite"
paulson@14408
   160
apply (simp add: CFinite_def)
paulson@14408
   161
apply (blast intro!: SReal_add hcmod_add_less)
paulson@14408
   162
done
paulson@14408
   163
paulson@14408
   164
lemma CFinite_mult: "[|x \<in> CFinite; y \<in> CFinite|] ==> x*y \<in> CFinite"
paulson@14408
   165
apply (simp add: CFinite_def)
paulson@14408
   166
apply (blast intro!: SReal_mult hcmod_mult_less)
paulson@14408
   167
done
paulson@14408
   168
paulson@14408
   169
lemma CFinite_minus_iff [simp]: "(-x \<in> CFinite) = (x \<in> CFinite)"
paulson@14408
   170
by (simp add: CFinite_def)
paulson@14408
   171
paulson@14408
   172
lemma SComplex_subset_CFinite [simp]: "SComplex \<le> CFinite"
paulson@14408
   173
apply (auto simp add: SComplex_def CFinite_def)
paulson@14408
   174
apply (rule_tac x = "1 + hcmod (hcomplex_of_complex r) " in bexI)
paulson@14408
   175
apply (auto intro: SReal_add)
paulson@14408
   176
done
paulson@14408
   177
paulson@14408
   178
lemma HFinite_hcmod_hcomplex_of_complex [simp]:
paulson@14408
   179
     "hcmod (hcomplex_of_complex r) \<in> HFinite"
paulson@14408
   180
by (auto intro!: SReal_subset_HFinite [THEN subsetD])
paulson@14408
   181
paulson@14408
   182
lemma CFinite_hcomplex_of_complex [simp]: "hcomplex_of_complex x \<in> CFinite"
paulson@14408
   183
by (auto intro!: SComplex_subset_CFinite [THEN subsetD])
paulson@14408
   184
paulson@14408
   185
lemma CFiniteD: "x \<in> CFinite ==> \<exists>t \<in> Reals. hcmod x < t"
paulson@14408
   186
by (simp add: CFinite_def)
paulson@14408
   187
paulson@14408
   188
lemma CFinite_hcmod_iff: "(x \<in> CFinite) = (hcmod x \<in> HFinite)"
paulson@14408
   189
by (simp add: CFinite_def HFinite_def)
paulson@14408
   190
paulson@14408
   191
lemma CFinite_number_of [simp]: "number_of w \<in> CFinite"
paulson@14408
   192
by (rule SComplex_number_of [THEN SComplex_subset_CFinite [THEN subsetD]])
paulson@14408
   193
paulson@14408
   194
lemma CFinite_bounded: "[|x \<in> CFinite; y \<le> hcmod x; 0 \<le> y |] ==> y: HFinite"
paulson@14408
   195
by (auto intro: HFinite_bounded simp add: CFinite_hcmod_iff)
paulson@14408
   196
paulson@14408
   197
paulson@14408
   198
subsection{*The Complex Infinitesimals form a Subring*}
paulson@14408
   199
	 
paulson@14408
   200
lemma CInfinitesimal_zero [iff]: "0 \<in> CInfinitesimal"
paulson@14408
   201
by (simp add: CInfinitesimal_def)
paulson@14408
   202
paulson@14408
   203
lemma hcomplex_sum_of_halves: "x/(2::hcomplex) + x/(2::hcomplex) = x"
paulson@14408
   204
by auto
paulson@14408
   205
paulson@14408
   206
lemma CInfinitesimal_hcmod_iff: 
paulson@14408
   207
   "(z \<in> CInfinitesimal) = (hcmod z \<in> Infinitesimal)"
paulson@14408
   208
by (simp add: CInfinitesimal_def Infinitesimal_def)
paulson@14408
   209
paulson@14408
   210
lemma one_not_CInfinitesimal [simp]: "1 \<notin> CInfinitesimal"
paulson@14408
   211
by (simp add: CInfinitesimal_hcmod_iff)
paulson@14408
   212
paulson@14408
   213
lemma CInfinitesimal_add:
paulson@14408
   214
     "[| x \<in> CInfinitesimal; y \<in> CInfinitesimal |] ==> (x+y) \<in> CInfinitesimal"
paulson@14408
   215
apply (auto simp add: CInfinitesimal_hcmod_iff)
paulson@14408
   216
apply (rule hrabs_le_Infinitesimal)
paulson@14408
   217
apply (rule_tac y = "hcmod y" in Infinitesimal_add, auto)
paulson@14408
   218
done
paulson@14408
   219
paulson@14408
   220
lemma CInfinitesimal_minus_iff [simp]:
paulson@14408
   221
     "(-x:CInfinitesimal) = (x:CInfinitesimal)"
paulson@14408
   222
by (simp add: CInfinitesimal_def)
paulson@14408
   223
paulson@14408
   224
lemma CInfinitesimal_diff:
paulson@14408
   225
     "[| x \<in> CInfinitesimal;  y \<in> CInfinitesimal |] ==> x-y \<in> CInfinitesimal"
paulson@14408
   226
by (simp add: diff_minus CInfinitesimal_add)
paulson@14408
   227
paulson@14408
   228
lemma CInfinitesimal_mult:
paulson@14408
   229
     "[| x \<in> CInfinitesimal; y \<in> CInfinitesimal |] ==> x * y \<in> CInfinitesimal"
paulson@14408
   230
by (auto intro: Infinitesimal_mult simp add: CInfinitesimal_hcmod_iff hcmod_mult)
paulson@14408
   231
paulson@14408
   232
lemma CInfinitesimal_CFinite_mult:
paulson@14408
   233
     "[| x \<in> CInfinitesimal; y \<in> CFinite |] ==> (x * y) \<in> CInfinitesimal"
paulson@14408
   234
by (auto intro: Infinitesimal_HFinite_mult simp add: CInfinitesimal_hcmod_iff CFinite_hcmod_iff hcmod_mult)
paulson@14408
   235
paulson@14408
   236
lemma CInfinitesimal_CFinite_mult2:
paulson@14408
   237
     "[| x \<in> CInfinitesimal; y \<in> CFinite |] ==> (y * x) \<in> CInfinitesimal"
paulson@14408
   238
by (auto dest: CInfinitesimal_CFinite_mult simp add: hcomplex_mult_commute)
paulson@14408
   239
paulson@14408
   240
lemma CInfinite_hcmod_iff: "(z \<in> CInfinite) = (hcmod z \<in> HInfinite)"
paulson@14408
   241
by (simp add: CInfinite_def HInfinite_def)
paulson@14408
   242
paulson@14408
   243
lemma CInfinite_inverse_CInfinitesimal:
paulson@14408
   244
     "x \<in> CInfinite ==> inverse x \<in> CInfinitesimal"
paulson@14408
   245
by (auto intro: HInfinite_inverse_Infinitesimal simp add: CInfinitesimal_hcmod_iff CInfinite_hcmod_iff hcmod_hcomplex_inverse)
paulson@14408
   246
paulson@14408
   247
lemma CInfinite_mult: "[|x \<in> CInfinite; y \<in> CInfinite|] ==> (x*y): CInfinite"
paulson@14408
   248
by (auto intro: HInfinite_mult simp add: CInfinite_hcmod_iff hcmod_mult)
paulson@14408
   249
paulson@14408
   250
lemma CInfinite_minus_iff [simp]: "(-x \<in> CInfinite) = (x \<in> CInfinite)"
paulson@14408
   251
by (simp add: CInfinite_def)
paulson@14408
   252
paulson@14408
   253
lemma CFinite_sum_squares:
paulson@14408
   254
     "[|a \<in> CFinite; b \<in> CFinite; c \<in> CFinite|]   
paulson@14408
   255
      ==> a*a + b*b + c*c \<in> CFinite"
paulson@14408
   256
by (auto intro: CFinite_mult CFinite_add)
paulson@14408
   257
paulson@14408
   258
lemma not_CInfinitesimal_not_zero: "x \<notin> CInfinitesimal ==> x \<noteq> 0"
paulson@14408
   259
by auto
paulson@14408
   260
paulson@14408
   261
lemma not_CInfinitesimal_not_zero2: "x \<in> CFinite - CInfinitesimal ==> x \<noteq> 0"
paulson@14408
   262
by auto
paulson@14408
   263
paulson@14408
   264
lemma CFinite_diff_CInfinitesimal_hcmod:
paulson@14408
   265
     "x \<in> CFinite - CInfinitesimal ==> hcmod x \<in> HFinite - Infinitesimal"
paulson@14408
   266
by (simp add: CFinite_hcmod_iff CInfinitesimal_hcmod_iff)
paulson@14408
   267
paulson@14408
   268
lemma hcmod_less_CInfinitesimal:
paulson@14408
   269
     "[| e \<in> CInfinitesimal; hcmod x < hcmod e |] ==> x \<in> CInfinitesimal"
paulson@14408
   270
by (auto intro: hrabs_less_Infinitesimal simp add: CInfinitesimal_hcmod_iff)
paulson@14408
   271
paulson@14408
   272
lemma hcmod_le_CInfinitesimal:
paulson@14408
   273
     "[| e \<in> CInfinitesimal; hcmod x \<le> hcmod e |] ==> x \<in> CInfinitesimal"
paulson@14408
   274
by (auto intro: hrabs_le_Infinitesimal simp add: CInfinitesimal_hcmod_iff)
paulson@14408
   275
paulson@14408
   276
lemma CInfinitesimal_interval:
paulson@14408
   277
     "[| e \<in> CInfinitesimal;  
paulson@14408
   278
          e' \<in> CInfinitesimal;  
paulson@14408
   279
          hcmod e' < hcmod x ; hcmod x < hcmod e  
paulson@14408
   280
       |] ==> x \<in> CInfinitesimal"
paulson@14408
   281
by (auto intro: Infinitesimal_interval simp add: CInfinitesimal_hcmod_iff)
paulson@14408
   282
paulson@14408
   283
lemma CInfinitesimal_interval2:
paulson@14408
   284
     "[| e \<in> CInfinitesimal;  
paulson@14408
   285
         e' \<in> CInfinitesimal;  
paulson@14408
   286
         hcmod e' \<le> hcmod x ; hcmod x \<le> hcmod e  
paulson@14408
   287
      |] ==> x \<in> CInfinitesimal"
paulson@14408
   288
by (auto intro: Infinitesimal_interval2 simp add: CInfinitesimal_hcmod_iff)
paulson@14408
   289
paulson@14408
   290
lemma not_CInfinitesimal_mult:
paulson@14408
   291
     "[| x \<notin> CInfinitesimal;  y \<notin> CInfinitesimal|] ==> (x*y) \<notin> CInfinitesimal"
paulson@14408
   292
apply (auto simp add: CInfinitesimal_hcmod_iff hcmod_mult)
paulson@14408
   293
apply (drule not_Infinitesimal_mult, auto)
paulson@14408
   294
done
paulson@14408
   295
paulson@14408
   296
lemma CInfinitesimal_mult_disj:
paulson@14408
   297
     "x*y \<in> CInfinitesimal ==> x \<in> CInfinitesimal | y \<in> CInfinitesimal"
paulson@14408
   298
by (auto dest: Infinitesimal_mult_disj simp add: CInfinitesimal_hcmod_iff hcmod_mult)
paulson@14408
   299
paulson@14408
   300
lemma CFinite_CInfinitesimal_diff_mult:
paulson@14408
   301
     "[| x \<in> CFinite - CInfinitesimal; y \<in> CFinite - CInfinitesimal |] 
paulson@14408
   302
      ==> x*y \<in> CFinite - CInfinitesimal"
paulson@14408
   303
by (blast dest: CFinite_mult not_CInfinitesimal_mult)
paulson@14408
   304
paulson@14408
   305
lemma CInfinitesimal_subset_CFinite: "CInfinitesimal \<le> CFinite"
paulson@14408
   306
by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
paulson@14408
   307
         simp add: CInfinitesimal_hcmod_iff CFinite_hcmod_iff)
paulson@14408
   308
paulson@14408
   309
lemma CInfinitesimal_hcomplex_of_complex_mult:
paulson@14408
   310
     "x \<in> CInfinitesimal ==> x * hcomplex_of_complex r \<in> CInfinitesimal"
paulson@14408
   311
by (auto intro!: Infinitesimal_HFinite_mult simp add: CInfinitesimal_hcmod_iff hcmod_mult)
paulson@14408
   312
paulson@14408
   313
lemma CInfinitesimal_hcomplex_of_complex_mult2:
paulson@14408
   314
     "x \<in> CInfinitesimal ==> hcomplex_of_complex r * x \<in> CInfinitesimal"
paulson@14408
   315
by (auto intro!: Infinitesimal_HFinite_mult2 simp add: CInfinitesimal_hcmod_iff hcmod_mult)
paulson@14408
   316
paulson@14408
   317
paulson@14408
   318
subsection{*The ``Infinitely Close'' Relation*}
paulson@14408
   319
paulson@14408
   320
(*
paulson@14408
   321
Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z @= hcmod w)"
paulson@14408
   322
by (auto_tac (claset(),simpset() addsimps [CInfinitesimal_hcmod_iff]));
paulson@14408
   323
*)
paulson@14408
   324
paulson@14408
   325
lemma mem_cinfmal_iff: "x:CInfinitesimal = (x @c= 0)"
paulson@14408
   326
by (simp add: CInfinitesimal_hcmod_iff capprox_def)
paulson@14408
   327
paulson@14408
   328
lemma capprox_minus_iff: "(x @c= y) = (x + -y @c= 0)"
paulson@14408
   329
by (simp add: capprox_def diff_minus)
paulson@14408
   330
paulson@14408
   331
lemma capprox_minus_iff2: "(x @c= y) = (-y + x @c= 0)"
paulson@14408
   332
by (simp add: capprox_def diff_minus add_commute)
paulson@14408
   333
paulson@14408
   334
lemma capprox_refl [simp]: "x @c= x"
paulson@14408
   335
by (simp add: capprox_def)
paulson@14408
   336
paulson@14408
   337
lemma capprox_sym: "x @c= y ==> y @c= x"
paulson@14408
   338
by (simp add: capprox_def CInfinitesimal_def hcmod_diff_commute)
paulson@14408
   339
paulson@14408
   340
lemma capprox_trans: "[| x @c= y; y @c= z |] ==> x @c= z"
paulson@14408
   341
apply (simp add: capprox_def)
paulson@14408
   342
apply (drule CInfinitesimal_add, assumption)
paulson@14408
   343
apply (simp add: diff_minus)
paulson@14408
   344
done
paulson@14408
   345
paulson@14408
   346
lemma capprox_trans2: "[| r @c= x; s @c= x |] ==> r @c= s"
paulson@14408
   347
by (blast intro: capprox_sym capprox_trans)
paulson@14408
   348
paulson@14408
   349
lemma capprox_trans3: "[| x @c= r; x @c= s|] ==> r @c= s"
paulson@14408
   350
by (blast intro: capprox_sym capprox_trans)
paulson@14408
   351
paulson@14408
   352
lemma number_of_capprox_reorient [simp]:
paulson@14408
   353
     "(number_of w @c= x) = (x @c= number_of w)"
paulson@14408
   354
by (blast intro: capprox_sym)
paulson@14408
   355
paulson@14408
   356
lemma CInfinitesimal_capprox_minus: "(x-y \<in> CInfinitesimal) = (x @c= y)"
paulson@14408
   357
by (simp add: diff_minus capprox_minus_iff [symmetric] mem_cinfmal_iff)
paulson@14408
   358
paulson@14408
   359
lemma capprox_monad_iff: "(x @c= y) = (cmonad(x)=cmonad(y))"
paulson@14408
   360
by (auto simp add: cmonad_def dest: capprox_sym elim!: capprox_trans equalityCE)
paulson@14408
   361
paulson@14408
   362
lemma Infinitesimal_capprox:
paulson@14408
   363
     "[| x \<in> CInfinitesimal; y \<in> CInfinitesimal |] ==> x @c= y"
paulson@14408
   364
apply (simp add: mem_cinfmal_iff)
paulson@14408
   365
apply (blast intro: capprox_trans capprox_sym)
paulson@14408
   366
done
paulson@14408
   367
paulson@14408
   368
lemma capprox_add: "[| a @c= b; c @c= d |] ==> a+c @c= b+d"
paulson@14408
   369
apply (simp add: capprox_def diff_minus) 
paulson@14408
   370
apply (rule minus_add_distrib [THEN ssubst])
paulson@14408
   371
apply (rule add_assoc [THEN ssubst])
paulson@14408
   372
apply (rule_tac b1 = c in add_left_commute [THEN subst])
paulson@14408
   373
apply (rule add_assoc [THEN subst])
paulson@14408
   374
apply (blast intro: CInfinitesimal_add)
paulson@14408
   375
done
paulson@14408
   376
paulson@14408
   377
lemma capprox_minus: "a @c= b ==> -a @c= -b"
paulson@14408
   378
apply (rule capprox_minus_iff [THEN iffD2, THEN capprox_sym])
paulson@14408
   379
apply (drule capprox_minus_iff [THEN iffD1])
paulson@14408
   380
apply (simp add: add_commute)
paulson@14408
   381
done
paulson@14408
   382
paulson@14408
   383
lemma capprox_minus2: "-a @c= -b ==> a @c= b"
paulson@14408
   384
by (auto dest: capprox_minus)
paulson@14408
   385
paulson@14408
   386
lemma capprox_minus_cancel [simp]: "(-a @c= -b) = (a @c= b)"
paulson@14408
   387
by (blast intro: capprox_minus capprox_minus2)
paulson@14408
   388
paulson@14408
   389
lemma capprox_add_minus: "[| a @c= b; c @c= d |] ==> a + -c @c= b + -d"
paulson@14408
   390
by (blast intro!: capprox_add capprox_minus)
paulson@14408
   391
paulson@14408
   392
lemma capprox_mult1: 
paulson@14408
   393
      "[| a @c= b; c \<in> CFinite|] ==> a*c @c= b*c"
paulson@14408
   394
apply (simp add: capprox_def diff_minus)
paulson@14408
   395
apply (simp only: CInfinitesimal_CFinite_mult minus_mult_left hcomplex_add_mult_distrib [symmetric])
paulson@14408
   396
done
paulson@14408
   397
paulson@14408
   398
lemma capprox_mult2: "[|a @c= b; c \<in> CFinite|] ==> c*a @c= c*b"
paulson@14408
   399
by (simp add: capprox_mult1 hcomplex_mult_commute)
paulson@14408
   400
paulson@14408
   401
lemma capprox_mult_subst:
paulson@14408
   402
     "[|u @c= v*x; x @c= y; v \<in> CFinite|] ==> u @c= v*y"
paulson@14408
   403
by (blast intro: capprox_mult2 capprox_trans)
paulson@14408
   404
paulson@14408
   405
lemma capprox_mult_subst2:
paulson@14408
   406
     "[| u @c= x*v; x @c= y; v \<in> CFinite |] ==> u @c= y*v"
paulson@14408
   407
by (blast intro: capprox_mult1 capprox_trans)
paulson@14408
   408
paulson@14408
   409
lemma capprox_mult_subst_SComplex:
paulson@14408
   410
     "[| u @c= x*hcomplex_of_complex v; x @c= y |] 
paulson@14408
   411
      ==> u @c= y*hcomplex_of_complex v"
paulson@14408
   412
by (auto intro: capprox_mult_subst2)
paulson@14408
   413
paulson@14408
   414
lemma capprox_eq_imp: "a = b ==> a @c= b"
paulson@14408
   415
by (simp add: capprox_def)
paulson@14408
   416
paulson@14408
   417
lemma CInfinitesimal_minus_capprox: "x \<in> CInfinitesimal ==> -x @c= x"
paulson@14408
   418
by (blast intro: CInfinitesimal_minus_iff [THEN iffD2] mem_cinfmal_iff [THEN iffD1] capprox_trans2)
paulson@14408
   419
paulson@14408
   420
lemma bex_CInfinitesimal_iff: "(\<exists>y \<in> CInfinitesimal. x - z = y) = (x @c= z)"
paulson@14408
   421
by (unfold capprox_def, blast)
paulson@14408
   422
paulson@14408
   423
lemma bex_CInfinitesimal_iff2: "(\<exists>y \<in> CInfinitesimal. x = z + y) = (x @c= z)"
paulson@14408
   424
by (simp add: bex_CInfinitesimal_iff [symmetric], force)
paulson@14408
   425
paulson@14408
   426
lemma CInfinitesimal_add_capprox:
paulson@14408
   427
     "[| y \<in> CInfinitesimal; x + y = z |] ==> x @c= z"
paulson@14408
   428
apply (rule bex_CInfinitesimal_iff [THEN iffD1])
paulson@14408
   429
apply (drule CInfinitesimal_minus_iff [THEN iffD2])
paulson@14408
   430
apply (simp add: eq_commute compare_rls)
paulson@14408
   431
done
paulson@14408
   432
paulson@14408
   433
lemma CInfinitesimal_add_capprox_self: "y \<in> CInfinitesimal ==> x @c= x + y"
paulson@14408
   434
apply (rule bex_CInfinitesimal_iff [THEN iffD1])
paulson@14408
   435
apply (drule CInfinitesimal_minus_iff [THEN iffD2])
paulson@14408
   436
apply (simp add: eq_commute compare_rls)
paulson@14408
   437
done
paulson@14408
   438
paulson@14408
   439
lemma CInfinitesimal_add_capprox_self2: "y \<in> CInfinitesimal ==> x @c= y + x"
paulson@14408
   440
by (auto dest: CInfinitesimal_add_capprox_self simp add: add_commute)
paulson@14408
   441
paulson@14408
   442
lemma CInfinitesimal_add_minus_capprox_self:
paulson@14408
   443
     "y \<in> CInfinitesimal ==> x @c= x + -y"
paulson@14408
   444
by (blast intro!: CInfinitesimal_add_capprox_self CInfinitesimal_minus_iff [THEN iffD2])
paulson@14408
   445
paulson@14408
   446
lemma CInfinitesimal_add_cancel:
paulson@14408
   447
     "[| y \<in> CInfinitesimal; x+y @c= z|] ==> x @c= z"
paulson@14408
   448
apply (drule_tac x = x in CInfinitesimal_add_capprox_self [THEN capprox_sym])
paulson@14408
   449
apply (erule capprox_trans3 [THEN capprox_sym], assumption)
paulson@14408
   450
done
paulson@14408
   451
paulson@14408
   452
lemma CInfinitesimal_add_right_cancel:
paulson@14408
   453
     "[| y \<in> CInfinitesimal; x @c= z + y|] ==> x @c= z"
paulson@14408
   454
apply (drule_tac x = z in CInfinitesimal_add_capprox_self2 [THEN capprox_sym])
paulson@14408
   455
apply (erule capprox_trans3 [THEN capprox_sym])
paulson@14408
   456
apply (simp add: add_commute)
paulson@14408
   457
apply (erule capprox_sym)
paulson@14408
   458
done
paulson@14408
   459
paulson@14408
   460
lemma capprox_add_left_cancel: "d + b  @c= d + c ==> b @c= c"
paulson@14408
   461
apply (drule capprox_minus_iff [THEN iffD1])
paulson@14408
   462
apply (simp add: minus_add_distrib capprox_minus_iff [symmetric] add_ac)
paulson@14408
   463
done
paulson@14408
   464
paulson@14408
   465
lemma capprox_add_right_cancel: "b + d @c= c + d ==> b @c= c"
paulson@14408
   466
apply (rule capprox_add_left_cancel)
paulson@14408
   467
apply (simp add: add_commute)
paulson@14408
   468
done
paulson@14408
   469
paulson@14408
   470
lemma capprox_add_mono1: "b @c= c ==> d + b @c= d + c"
paulson@14408
   471
apply (rule capprox_minus_iff [THEN iffD2])
paulson@14408
   472
apply (simp add: capprox_minus_iff [symmetric] add_ac)
paulson@14408
   473
done
paulson@14408
   474
paulson@14408
   475
lemma capprox_add_mono2: "b @c= c ==> b + a @c= c + a"
paulson@14408
   476
apply (simp (no_asm_simp) add: add_commute capprox_add_mono1)
paulson@14408
   477
done
paulson@14408
   478
paulson@14408
   479
lemma capprox_add_left_iff [iff]: "(a + b @c= a + c) = (b @c= c)"
paulson@14408
   480
by (fast elim: capprox_add_left_cancel capprox_add_mono1)
paulson@14408
   481
paulson@14408
   482
lemma capprox_add_right_iff [iff]: "(b + a @c= c + a) = (b @c= c)"
paulson@14408
   483
by (simp add: add_commute)
paulson@14408
   484
paulson@14408
   485
lemma capprox_CFinite: "[| x \<in> CFinite; x @c= y |] ==> y \<in> CFinite"
paulson@14408
   486
apply (drule bex_CInfinitesimal_iff2 [THEN iffD2], safe)
paulson@14408
   487
apply (drule CInfinitesimal_subset_CFinite [THEN subsetD, THEN CFinite_minus_iff [THEN iffD2]])
paulson@14408
   488
apply (drule CFinite_add)
paulson@14408
   489
apply (assumption, auto)
paulson@14408
   490
done
paulson@14408
   491
paulson@14408
   492
lemma capprox_hcomplex_of_complex_CFinite:
paulson@14408
   493
     "x @c= hcomplex_of_complex D ==> x \<in> CFinite"
paulson@14408
   494
by (rule capprox_sym [THEN [2] capprox_CFinite], auto)
paulson@14408
   495
paulson@14408
   496
lemma capprox_mult_CFinite:
paulson@14408
   497
     "[|a @c= b; c @c= d; b \<in> CFinite; d \<in> CFinite|] ==> a*c @c= b*d"
paulson@14408
   498
apply (rule capprox_trans)
paulson@14408
   499
apply (rule_tac [2] capprox_mult2)
paulson@14408
   500
apply (rule capprox_mult1)
paulson@14408
   501
prefer 2 apply (blast intro: capprox_CFinite capprox_sym, auto)
paulson@14408
   502
done
paulson@14408
   503
paulson@14408
   504
lemma capprox_mult_hcomplex_of_complex:
paulson@14408
   505
     "[|a @c= hcomplex_of_complex b; c @c= hcomplex_of_complex d |]  
paulson@14408
   506
      ==> a*c @c= hcomplex_of_complex b * hcomplex_of_complex d"
paulson@14408
   507
apply (blast intro!: capprox_mult_CFinite capprox_hcomplex_of_complex_CFinite CFinite_hcomplex_of_complex)
paulson@14408
   508
done
paulson@14408
   509
paulson@14408
   510
lemma capprox_SComplex_mult_cancel_zero:
paulson@14408
   511
     "[| a \<in> SComplex; a \<noteq> 0; a*x @c= 0 |] ==> x @c= 0"
paulson@14408
   512
apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]])
paulson@15013
   513
apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
paulson@14408
   514
done
paulson@14408
   515
paulson@14408
   516
lemma capprox_mult_SComplex1: "[| a \<in> SComplex; x @c= 0 |] ==> x*a @c= 0"
paulson@14408
   517
by (auto dest: SComplex_subset_CFinite [THEN subsetD] capprox_mult1)
paulson@14408
   518
paulson@14408
   519
lemma capprox_mult_SComplex2: "[| a \<in> SComplex; x @c= 0 |] ==> a*x @c= 0"
paulson@14408
   520
by (auto dest: SComplex_subset_CFinite [THEN subsetD] capprox_mult2)
paulson@14408
   521
paulson@14408
   522
lemma capprox_mult_SComplex_zero_cancel_iff [simp]:
paulson@14408
   523
     "[|a \<in> SComplex; a \<noteq> 0 |] ==> (a*x @c= 0) = (x @c= 0)"
paulson@14408
   524
by (blast intro: capprox_SComplex_mult_cancel_zero capprox_mult_SComplex2)
paulson@14408
   525
paulson@14408
   526
lemma capprox_SComplex_mult_cancel:
paulson@14408
   527
     "[| a \<in> SComplex; a \<noteq> 0; a* w @c= a*z |] ==> w @c= z"
paulson@14408
   528
apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]])
paulson@15013
   529
apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
paulson@14408
   530
done
paulson@14408
   531
paulson@14408
   532
lemma capprox_SComplex_mult_cancel_iff1 [simp]:
paulson@14408
   533
     "[| a \<in> SComplex; a \<noteq> 0|] ==> (a* w @c= a*z) = (w @c= z)"
paulson@14408
   534
by (auto intro!: capprox_mult2 SComplex_subset_CFinite [THEN subsetD]
paulson@14408
   535
            intro: capprox_SComplex_mult_cancel)
paulson@14408
   536
paulson@14408
   537
lemma capprox_hcmod_approx_zero: "(x @c= y) = (hcmod (y - x) @= 0)"
paulson@14408
   538
apply (rule capprox_minus_iff [THEN ssubst])
paulson@14408
   539
apply (simp add: capprox_def CInfinitesimal_hcmod_iff mem_infmal_iff diff_minus [symmetric] hcmod_diff_commute)
paulson@14408
   540
done
paulson@14408
   541
paulson@14408
   542
lemma capprox_approx_zero_iff: "(x @c= 0) = (hcmod x @= 0)"
paulson@14408
   543
by (simp add: capprox_hcmod_approx_zero)
paulson@14408
   544
paulson@14408
   545
lemma capprox_minus_zero_cancel_iff [simp]: "(-x @c= 0) = (x @c= 0)"
paulson@14408
   546
by (simp add: capprox_hcmod_approx_zero)
paulson@14408
   547
paulson@14408
   548
lemma Infinitesimal_hcmod_add_diff:
paulson@14408
   549
     "u @c= 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal"
paulson@14408
   550
apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2)
paulson@14408
   551
apply (auto dest: capprox_approx_zero_iff [THEN iffD1]
paulson@14408
   552
             simp add: mem_infmal_iff [symmetric] hypreal_diff_def)
paulson@14408
   553
apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1])
paulson@14408
   554
apply (auto simp add: diff_minus [symmetric])
paulson@14408
   555
done
paulson@14408
   556
paulson@14408
   557
lemma approx_hcmod_add_hcmod: "u @c= 0 ==> hcmod(x + u) @= hcmod x"
paulson@14408
   558
apply (rule approx_minus_iff [THEN iffD2])
paulson@14408
   559
apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric] diff_minus [symmetric])
paulson@14408
   560
done
paulson@14408
   561
paulson@14408
   562
lemma capprox_hcmod_approx: "x @c= y ==> hcmod x @= hcmod y"
paulson@14408
   563
by (auto intro: approx_hcmod_add_hcmod 
paulson@14408
   564
         dest!: bex_CInfinitesimal_iff2 [THEN iffD2]
paulson@14408
   565
         simp add: mem_cinfmal_iff)
paulson@13957
   566
paulson@13957
   567
paulson@14408
   568
subsection{*Zero is the Only Infinitesimal Complex Number*}
paulson@14408
   569
paulson@14408
   570
lemma CInfinitesimal_less_SComplex:
paulson@14408
   571
   "[| x \<in> SComplex; y \<in> CInfinitesimal; 0 < hcmod x |] ==> hcmod y < hcmod x"
paulson@14408
   572
by (auto intro!: Infinitesimal_less_SReal SComplex_hcmod_SReal simp add: CInfinitesimal_hcmod_iff)
paulson@14408
   573
paulson@14408
   574
lemma SComplex_Int_CInfinitesimal_zero: "SComplex Int CInfinitesimal = {0}"
paulson@14408
   575
apply (auto simp add: SComplex_def CInfinitesimal_hcmod_iff)
paulson@14408
   576
apply (cut_tac r = r in SReal_hcmod_hcomplex_of_complex)
paulson@14408
   577
apply (drule_tac A = Reals in IntI, assumption)
paulson@14408
   578
apply (subgoal_tac "hcmod (hcomplex_of_complex r) = 0")
paulson@14408
   579
apply simp
paulson@14408
   580
apply (simp add: SReal_Int_Infinitesimal_zero) 
paulson@14408
   581
done
paulson@14408
   582
paulson@14408
   583
lemma SComplex_CInfinitesimal_zero:
paulson@14408
   584
     "[| x \<in> SComplex; x \<in> CInfinitesimal|] ==> x = 0"
paulson@14408
   585
by (cut_tac SComplex_Int_CInfinitesimal_zero, blast)
paulson@14408
   586
paulson@14408
   587
lemma SComplex_CFinite_diff_CInfinitesimal:
paulson@14408
   588
     "[| x \<in> SComplex; x \<noteq> 0 |] ==> x \<in> CFinite - CInfinitesimal"
paulson@14408
   589
by (auto dest: SComplex_CInfinitesimal_zero SComplex_subset_CFinite [THEN subsetD])
paulson@14408
   590
paulson@14408
   591
lemma hcomplex_of_complex_CFinite_diff_CInfinitesimal:
paulson@14408
   592
     "hcomplex_of_complex x \<noteq> 0 
paulson@14408
   593
      ==> hcomplex_of_complex x \<in> CFinite - CInfinitesimal"
paulson@14408
   594
by (rule SComplex_CFinite_diff_CInfinitesimal, auto)
paulson@14408
   595
paulson@14408
   596
lemma hcomplex_of_complex_CInfinitesimal_iff_0 [iff]:
paulson@14408
   597
     "(hcomplex_of_complex x \<in> CInfinitesimal) = (x=0)"
paulson@14408
   598
apply (auto simp add: hcomplex_of_complex_zero)
paulson@14408
   599
apply (rule ccontr)
paulson@14408
   600
apply (rule hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN DiffD2], auto)
paulson@14408
   601
done
paulson@14408
   602
paulson@14408
   603
lemma number_of_not_CInfinitesimal [simp]:
paulson@14408
   604
     "number_of w \<noteq> (0::hcomplex) ==> number_of w \<notin> CInfinitesimal"
paulson@14408
   605
by (fast dest: SComplex_number_of [THEN SComplex_CInfinitesimal_zero])
paulson@14408
   606
paulson@14408
   607
lemma capprox_SComplex_not_zero:
paulson@14408
   608
     "[| y \<in> SComplex; x @c= y; y\<noteq> 0 |] ==> x \<noteq> 0"
paulson@14408
   609
by (auto dest: SComplex_CInfinitesimal_zero capprox_sym [THEN mem_cinfmal_iff [THEN iffD2]])
paulson@14408
   610
paulson@14408
   611
lemma CFinite_diff_CInfinitesimal_capprox:
paulson@14408
   612
     "[| x @c= y; y \<in> CFinite - CInfinitesimal |]  
paulson@14408
   613
      ==> x \<in> CFinite - CInfinitesimal"
paulson@14408
   614
apply (auto intro: capprox_sym [THEN [2] capprox_CFinite] 
paulson@14408
   615
            simp add: mem_cinfmal_iff)
paulson@14408
   616
apply (drule capprox_trans3, assumption)
paulson@14408
   617
apply (blast dest: capprox_sym)
paulson@14408
   618
done
paulson@14408
   619
paulson@14408
   620
lemma CInfinitesimal_ratio:
paulson@14408
   621
     "[| y \<noteq> 0;  y \<in> CInfinitesimal;  x/y \<in> CFinite |] ==> x \<in> CInfinitesimal"
paulson@14408
   622
apply (drule CInfinitesimal_CFinite_mult2, assumption)
paulson@15013
   623
apply (simp add: divide_inverse mult_assoc)
paulson@14408
   624
done
paulson@14408
   625
paulson@14408
   626
lemma SComplex_capprox_iff:
paulson@14408
   627
     "[|x \<in> SComplex; y \<in> SComplex|] ==> (x @c= y) = (x = y)"
paulson@14408
   628
apply auto
paulson@14408
   629
apply (simp add: capprox_def)
paulson@14408
   630
apply (subgoal_tac "x-y = 0", simp) 
paulson@14408
   631
apply (rule SComplex_CInfinitesimal_zero)
paulson@14408
   632
apply (simp add: SComplex_diff, assumption)
paulson@14408
   633
done
paulson@14408
   634
paulson@14408
   635
lemma number_of_capprox_iff [simp]:
paulson@14408
   636
    "(number_of v @c= number_of w) = (number_of v = (number_of w :: hcomplex))"
paulson@14408
   637
by (rule SComplex_capprox_iff, auto)
paulson@14408
   638
paulson@14408
   639
lemma number_of_CInfinitesimal_iff [simp]:
paulson@14408
   640
     "(number_of w \<in> CInfinitesimal) = (number_of w = (0::hcomplex))"
paulson@14408
   641
apply (rule iffI)
paulson@14408
   642
apply (fast dest: SComplex_number_of [THEN SComplex_CInfinitesimal_zero])
paulson@14408
   643
apply (simp (no_asm_simp))
paulson@14408
   644
done
paulson@14408
   645
paulson@14408
   646
lemma hcomplex_of_complex_approx_iff [simp]:
paulson@14408
   647
     "(hcomplex_of_complex k @c= hcomplex_of_complex m) = (k = m)"
paulson@14408
   648
apply auto
paulson@14408
   649
apply (rule inj_hcomplex_of_complex [THEN injD])
paulson@14408
   650
apply (rule SComplex_capprox_iff [THEN iffD1], auto)
paulson@14408
   651
done
paulson@14408
   652
paulson@14408
   653
lemma hcomplex_of_complex_capprox_number_of_iff [simp]:
paulson@14408
   654
     "(hcomplex_of_complex k @c= number_of w) = (k = number_of w)"
paulson@14408
   655
by (subst hcomplex_of_complex_approx_iff [symmetric], auto)
paulson@14408
   656
paulson@14408
   657
lemma capprox_unique_complex:
paulson@14408
   658
     "[| r \<in> SComplex; s \<in> SComplex; r @c= x; s @c= x|] ==> r = s"
paulson@14408
   659
by (blast intro: SComplex_capprox_iff [THEN iffD1] capprox_trans2)
paulson@14408
   660
paulson@14408
   661
lemma hcomplex_capproxD1:
paulson@14408
   662
     "Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})  
paulson@14408
   663
      ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) @=  
paulson@14408
   664
          Abs_hypreal(hyprel `` {%n. Re(Y n)})"
paulson@14408
   665
apply (auto simp add: approx_FreeUltrafilterNat_iff)
paulson@14408
   666
apply (drule capprox_minus_iff [THEN iffD1])
paulson@14408
   667
apply (auto simp add: hcomplex_minus hcomplex_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
paulson@14408
   668
apply (drule_tac x = m in spec, ultra)
paulson@14408
   669
apply (rename_tac Z x)
paulson@14408
   670
apply (case_tac "X x")
paulson@14408
   671
apply (case_tac "Y x")
paulson@14408
   672
apply (auto simp add: complex_minus complex_add complex_mod
paulson@14408
   673
           simp del: realpow_Suc)
paulson@14408
   674
apply (rule_tac y="abs(Z x)" in order_le_less_trans)
paulson@14408
   675
apply (drule_tac t = "Z x" in sym)
paulson@14408
   676
apply (auto simp add: abs_eqI1 simp del: realpow_Suc)
paulson@14408
   677
done
paulson@14408
   678
paulson@14408
   679
(* same proof *)
paulson@14408
   680
lemma hcomplex_capproxD2:
paulson@14408
   681
     "Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})  
paulson@14408
   682
      ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) @=  
paulson@14408
   683
          Abs_hypreal(hyprel `` {%n. Im(Y n)})"
paulson@14408
   684
apply (auto simp add: approx_FreeUltrafilterNat_iff)
paulson@14408
   685
apply (drule capprox_minus_iff [THEN iffD1])
paulson@14408
   686
apply (auto simp add: hcomplex_minus hcomplex_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
paulson@14408
   687
apply (drule_tac x = m in spec, ultra)
paulson@14408
   688
apply (rename_tac Z x)
paulson@14408
   689
apply (case_tac "X x")
paulson@14408
   690
apply (case_tac "Y x")
paulson@14408
   691
apply (auto simp add: complex_minus complex_add complex_mod simp del: realpow_Suc)
paulson@14408
   692
apply (rule_tac y="abs(Z x)" in order_le_less_trans)
paulson@14408
   693
apply (drule_tac t = "Z x" in sym)
paulson@14408
   694
apply (auto simp add: abs_eqI1 simp del: realpow_Suc)
paulson@14408
   695
done
paulson@14408
   696
paulson@14408
   697
lemma hcomplex_capproxI:
paulson@14408
   698
     "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) @=  
paulson@14408
   699
         Abs_hypreal(hyprel `` {%n. Re(Y n)});  
paulson@14408
   700
         Abs_hypreal(hyprel `` {%n. Im(X n)}) @=  
paulson@14408
   701
         Abs_hypreal(hyprel `` {%n. Im(Y n)})  
paulson@14408
   702
      |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})"
paulson@14408
   703
apply (drule approx_minus_iff [THEN iffD1])
paulson@14408
   704
apply (drule approx_minus_iff [THEN iffD1])
paulson@14408
   705
apply (rule capprox_minus_iff [THEN iffD2])
paulson@14408
   706
apply (auto simp add: mem_cinfmal_iff [symmetric] mem_infmal_iff [symmetric] hypreal_minus hypreal_add hcomplex_minus hcomplex_add CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff)
paulson@14408
   707
apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
paulson@14408
   708
apply (drule_tac x = "u/2" in spec)
paulson@14408
   709
apply (drule_tac x = "u/2" in spec, auto, ultra)
paulson@14408
   710
apply (drule sym, drule sym)
paulson@14408
   711
apply (case_tac "X x")
paulson@14408
   712
apply (case_tac "Y x")
paulson@14408
   713
apply (auto simp add: complex_minus complex_add complex_mod snd_conv fst_conv numeral_2_eq_2)
paulson@14408
   714
apply (rename_tac a b c d)
paulson@14408
   715
apply (subgoal_tac "sqrt (abs (a + - c) ^ 2 + abs (b + - d) ^ 2) < u")
paulson@14408
   716
apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto)
paulson@14408
   717
apply (simp add: power2_eq_square)
paulson@14408
   718
done
paulson@14408
   719
paulson@14408
   720
lemma capprox_approx_iff:
paulson@14408
   721
     "(Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})) = 
paulson@14408
   722
       (Abs_hypreal(hyprel `` {%n. Re(X n)}) @= Abs_hypreal(hyprel `` {%n. Re(Y n)}) &  
paulson@14408
   723
        Abs_hypreal(hyprel `` {%n. Im(X n)}) @= Abs_hypreal(hyprel `` {%n. Im(Y n)}))"
paulson@14408
   724
apply (blast intro: hcomplex_capproxI hcomplex_capproxD1 hcomplex_capproxD2)
paulson@14408
   725
done
paulson@14408
   726
paulson@14408
   727
lemma hcomplex_of_hypreal_capprox_iff [simp]:
paulson@14408
   728
     "(hcomplex_of_hypreal x @c= hcomplex_of_hypreal z) = (x @= z)"
paulson@14469
   729
apply (cases x, cases z)
paulson@14408
   730
apply (simp add: hcomplex_of_hypreal capprox_approx_iff)
paulson@14408
   731
done
paulson@14408
   732
paulson@14408
   733
lemma CFinite_HFinite_Re:
paulson@14408
   734
     "Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite  
paulson@14408
   735
      ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HFinite"
paulson@14408
   736
apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
paulson@14408
   737
apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
paulson@14408
   738
apply (rule_tac x = u in exI, ultra)
paulson@14408
   739
apply (drule sym, case_tac "X x")
paulson@14408
   740
apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc)
paulson@14408
   741
apply (rule ccontr, drule linorder_not_less [THEN iffD1])
paulson@14408
   742
apply (drule order_less_le_trans, assumption)
paulson@14408
   743
apply (drule real_sqrt_ge_abs1 [THEN [2] order_less_le_trans]) 
paulson@14408
   744
apply (auto simp add: numeral_2_eq_2 [symmetric]) 
paulson@14408
   745
done
paulson@14408
   746
paulson@14408
   747
lemma CFinite_HFinite_Im:
paulson@14408
   748
     "Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite  
paulson@14408
   749
      ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HFinite"
paulson@14408
   750
apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
paulson@14408
   751
apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
paulson@14408
   752
apply (rule_tac x = u in exI, ultra)
paulson@14408
   753
apply (drule sym, case_tac "X x")
paulson@14408
   754
apply (auto simp add: complex_mod simp del: realpow_Suc)
paulson@14408
   755
apply (rule ccontr, drule linorder_not_less [THEN iffD1])
paulson@14408
   756
apply (drule order_less_le_trans, assumption)
paulson@14408
   757
apply (drule real_sqrt_ge_abs2 [THEN [2] order_less_le_trans], auto) 
paulson@14408
   758
done
paulson@14408
   759
paulson@14408
   760
lemma HFinite_Re_Im_CFinite:
paulson@14408
   761
     "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HFinite;  
paulson@14408
   762
         Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HFinite  
paulson@14408
   763
      |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite"
paulson@14408
   764
apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
paulson@14408
   765
apply (rename_tac Y Z u v)
paulson@14408
   766
apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
paulson@14408
   767
apply (rule_tac x = "2* (u + v) " in exI)
paulson@14408
   768
apply ultra
paulson@14408
   769
apply (drule sym, case_tac "X x")
paulson@14408
   770
apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc)
paulson@14408
   771
apply (subgoal_tac "0 < u")
paulson@14408
   772
 prefer 2 apply arith
paulson@14408
   773
apply (subgoal_tac "0 < v")
paulson@14408
   774
 prefer 2 apply arith
paulson@14408
   775
apply (subgoal_tac "sqrt (abs (Y x) ^ 2 + abs (Z x) ^ 2) < 2*u + 2*v")
paulson@14408
   776
apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto)
paulson@14408
   777
apply (simp add: power2_eq_square)
paulson@14408
   778
done
paulson@14408
   779
paulson@14408
   780
lemma CFinite_HFinite_iff:
paulson@14408
   781
     "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite) =  
paulson@14408
   782
      (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HFinite &  
paulson@14408
   783
       Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HFinite)"
paulson@14408
   784
by (blast intro: HFinite_Re_Im_CFinite CFinite_HFinite_Im CFinite_HFinite_Re)
paulson@14408
   785
paulson@14408
   786
lemma SComplex_Re_SReal:
paulson@14408
   787
     "Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex  
paulson@14408
   788
      ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Reals"
paulson@14408
   789
apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def)
paulson@14408
   790
apply (rule_tac x = "Re r" in exI, ultra)
paulson@14408
   791
done
paulson@14408
   792
paulson@14408
   793
lemma SComplex_Im_SReal:
paulson@14408
   794
     "Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex  
paulson@14408
   795
      ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Reals"
paulson@14408
   796
apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def)
paulson@14408
   797
apply (rule_tac x = "Im r" in exI, ultra)
paulson@14408
   798
done
paulson@14408
   799
paulson@14408
   800
lemma Reals_Re_Im_SComplex:
paulson@14408
   801
     "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Reals;  
paulson@14408
   802
         Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Reals  
paulson@14408
   803
      |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex"
paulson@14408
   804
apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def)
paulson@14408
   805
apply (rule_tac x = "Complex r ra" in exI, ultra)
paulson@14408
   806
done
paulson@14408
   807
paulson@14408
   808
lemma SComplex_SReal_iff:
paulson@14408
   809
     "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex) =  
paulson@14408
   810
      (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Reals &  
paulson@14408
   811
       Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Reals)"
paulson@14408
   812
by (blast intro: SComplex_Re_SReal SComplex_Im_SReal Reals_Re_Im_SComplex)
paulson@14408
   813
paulson@14408
   814
lemma CInfinitesimal_Infinitesimal_iff:
paulson@14408
   815
     "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CInfinitesimal) =  
paulson@14408
   816
      (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Infinitesimal &  
paulson@14408
   817
       Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Infinitesimal)"
paulson@14408
   818
by (simp add: mem_cinfmal_iff mem_infmal_iff hcomplex_zero_num hypreal_zero_num capprox_approx_iff)
paulson@14408
   819
paulson@14408
   820
lemma eq_Abs_hcomplex_EX:
paulson@14408
   821
     "(\<exists>t. P t) = (\<exists>X. P (Abs_hcomplex(hcomplexrel `` {X})))"
paulson@14408
   822
apply auto
paulson@14408
   823
apply (rule_tac z = t in eq_Abs_hcomplex, auto)
paulson@14408
   824
done
paulson@14408
   825
paulson@14408
   826
lemma eq_Abs_hcomplex_Bex:
paulson@14408
   827
     "(\<exists>t \<in> A. P t) = (\<exists>X. (Abs_hcomplex(hcomplexrel `` {X})) \<in> A &  
paulson@14408
   828
                         P (Abs_hcomplex(hcomplexrel `` {X})))"
paulson@14408
   829
apply auto
paulson@14408
   830
apply (rule_tac z = t in eq_Abs_hcomplex, auto)
paulson@14408
   831
done
paulson@14408
   832
paulson@14408
   833
(* Here we go - easy proof now!! *)
paulson@14408
   834
lemma stc_part_Ex: "x:CFinite ==> \<exists>t \<in> SComplex. x @c= t"
paulson@14408
   835
apply (rule_tac z = x in eq_Abs_hcomplex)
paulson@14408
   836
apply (auto simp add: CFinite_HFinite_iff eq_Abs_hcomplex_Bex SComplex_SReal_iff capprox_approx_iff)
paulson@14408
   837
apply (drule st_part_Ex, safe)+
paulson@14408
   838
apply (rule_tac z = t in eq_Abs_hypreal)
paulson@14408
   839
apply (rule_tac z = ta in eq_Abs_hypreal, auto)
paulson@14408
   840
apply (rule_tac x = "%n. Complex (xa n) (xb n) " in exI)
paulson@14408
   841
apply auto
paulson@14408
   842
done
paulson@14408
   843
paulson@14408
   844
lemma stc_part_Ex1: "x:CFinite ==> EX! t. t \<in> SComplex &  x @c= t"
paulson@14408
   845
apply (drule stc_part_Ex, safe)
paulson@14408
   846
apply (drule_tac [2] capprox_sym, drule_tac [2] capprox_sym, drule_tac [2] capprox_sym)
paulson@14408
   847
apply (auto intro!: capprox_unique_complex)
paulson@14408
   848
done
paulson@14408
   849
paulson@14408
   850
lemma CFinite_Int_CInfinite_empty: "CFinite Int CInfinite = {}"
paulson@14408
   851
by (simp add: CFinite_def CInfinite_def, auto)
paulson@14408
   852
paulson@14408
   853
lemma CFinite_not_CInfinite: "x \<in> CFinite ==> x \<notin> CInfinite"
paulson@14408
   854
by (insert CFinite_Int_CInfinite_empty, blast)
paulson@14408
   855
paulson@14408
   856
text{*Not sure this is a good idea!*}
paulson@14408
   857
declare CFinite_Int_CInfinite_empty [simp]
paulson@14408
   858
paulson@14408
   859
lemma not_CFinite_CInfinite: "x\<notin> CFinite ==> x \<in> CInfinite"
paulson@14408
   860
by (auto intro: not_HFinite_HInfinite simp add: CFinite_hcmod_iff CInfinite_hcmod_iff)
paulson@14408
   861
paulson@14408
   862
lemma CInfinite_CFinite_disj: "x \<in> CInfinite | x \<in> CFinite"
paulson@14408
   863
by (blast intro: not_CFinite_CInfinite)
paulson@14408
   864
paulson@14408
   865
lemma CInfinite_CFinite_iff: "(x \<in> CInfinite) = (x \<notin> CFinite)"
paulson@14408
   866
by (blast dest: CFinite_not_CInfinite not_CFinite_CInfinite)
paulson@14408
   867
paulson@14408
   868
lemma CFinite_CInfinite_iff: "(x \<in> CFinite) = (x \<notin> CInfinite)"
paulson@14408
   869
by (simp add: CInfinite_CFinite_iff)
paulson@14408
   870
paulson@14408
   871
lemma CInfinite_diff_CFinite_CInfinitesimal_disj:
paulson@14408
   872
     "x \<notin> CInfinitesimal ==> x \<in> CInfinite | x \<in> CFinite - CInfinitesimal"
paulson@14408
   873
by (fast intro: not_CFinite_CInfinite)
paulson@14408
   874
paulson@14408
   875
lemma CFinite_inverse:
paulson@14408
   876
     "[| x \<in> CFinite; x \<notin> CInfinitesimal |] ==> inverse x \<in> CFinite"
paulson@14408
   877
apply (cut_tac x = "inverse x" in CInfinite_CFinite_disj)
paulson@14408
   878
apply (auto dest!: CInfinite_inverse_CInfinitesimal)
paulson@14408
   879
done
paulson@14408
   880
paulson@14408
   881
lemma CFinite_inverse2: "x \<in> CFinite - CInfinitesimal ==> inverse x \<in> CFinite"
paulson@14408
   882
by (blast intro: CFinite_inverse)
paulson@14408
   883
paulson@14408
   884
lemma CInfinitesimal_inverse_CFinite:
paulson@14408
   885
     "x \<notin> CInfinitesimal ==> inverse(x) \<in> CFinite"
paulson@14408
   886
apply (drule CInfinite_diff_CFinite_CInfinitesimal_disj)
paulson@14408
   887
apply (blast intro: CFinite_inverse CInfinite_inverse_CInfinitesimal CInfinitesimal_subset_CFinite [THEN subsetD])
paulson@14408
   888
done
paulson@14408
   889
paulson@14408
   890
paulson@14408
   891
lemma CFinite_not_CInfinitesimal_inverse:
paulson@14408
   892
     "x \<in> CFinite - CInfinitesimal ==> inverse x \<in> CFinite - CInfinitesimal"
paulson@14408
   893
apply (auto intro: CInfinitesimal_inverse_CFinite)
paulson@14408
   894
apply (drule CInfinitesimal_CFinite_mult2, assumption)
paulson@14408
   895
apply (simp add: not_CInfinitesimal_not_zero)
paulson@14408
   896
done
paulson@14408
   897
paulson@14408
   898
lemma capprox_inverse:
paulson@14408
   899
     "[| x @c= y; y \<in>  CFinite - CInfinitesimal |] ==> inverse x @c= inverse y"
paulson@14408
   900
apply (frule CFinite_diff_CInfinitesimal_capprox, assumption)
paulson@14408
   901
apply (frule not_CInfinitesimal_not_zero2)
paulson@14408
   902
apply (frule_tac x = x in not_CInfinitesimal_not_zero2)
paulson@14408
   903
apply (drule CFinite_inverse2)+
paulson@14408
   904
apply (drule capprox_mult2, assumption, auto)
paulson@14408
   905
apply (drule_tac c = "inverse x" in capprox_mult1, assumption)
paulson@15013
   906
apply (auto intro: capprox_sym simp add: mult_assoc)
paulson@14408
   907
done
paulson@14408
   908
paulson@15013
   909
lemmas hcomplex_of_complex_capprox_inverse =
paulson@15013
   910
  hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN [2] capprox_inverse]
paulson@14408
   911
paulson@14408
   912
lemma inverse_add_CInfinitesimal_capprox:
paulson@14408
   913
     "[| x \<in> CFinite - CInfinitesimal;  
paulson@14408
   914
         h \<in> CInfinitesimal |] ==> inverse(x + h) @c= inverse x"
paulson@14408
   915
by (auto intro: capprox_inverse capprox_sym CInfinitesimal_add_capprox_self)
paulson@14408
   916
paulson@14408
   917
lemma inverse_add_CInfinitesimal_capprox2:
paulson@14408
   918
     "[| x \<in> CFinite - CInfinitesimal;  
paulson@14408
   919
         h \<in> CInfinitesimal |] ==> inverse(h + x) @c= inverse x"
paulson@14408
   920
apply (rule add_commute [THEN subst])
paulson@14408
   921
apply (blast intro: inverse_add_CInfinitesimal_capprox)
paulson@14408
   922
done
paulson@14408
   923
paulson@14408
   924
lemma inverse_add_CInfinitesimal_approx_CInfinitesimal:
paulson@14408
   925
     "[| x \<in> CFinite - CInfinitesimal;  
paulson@14408
   926
         h \<in> CInfinitesimal |] ==> inverse(x + h) - inverse x @c= h"
paulson@14408
   927
apply (rule capprox_trans2)
paulson@14408
   928
apply (auto intro: inverse_add_CInfinitesimal_capprox 
paulson@14408
   929
       simp add: mem_cinfmal_iff diff_minus capprox_minus_iff [symmetric])
paulson@14408
   930
done
paulson@14408
   931
paulson@14408
   932
lemma CInfinitesimal_square_iff [iff]:
paulson@14408
   933
     "(x*x \<in> CInfinitesimal) = (x \<in> CInfinitesimal)"
paulson@14408
   934
by (simp add: CInfinitesimal_hcmod_iff hcmod_mult)
paulson@14408
   935
paulson@14408
   936
lemma capprox_CFinite_mult_cancel:
paulson@14408
   937
     "[| a \<in> CFinite-CInfinitesimal; a*w @c= a*z |] ==> w @c= z"
paulson@14408
   938
apply safe
paulson@14408
   939
apply (frule CFinite_inverse, assumption)
paulson@14408
   940
apply (drule not_CInfinitesimal_not_zero)
paulson@15013
   941
apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
paulson@14408
   942
done
paulson@14408
   943
paulson@14408
   944
lemma capprox_CFinite_mult_cancel_iff1:
paulson@14408
   945
     "a \<in> CFinite-CInfinitesimal ==> (a * w @c= a * z) = (w @c= z)"
paulson@14408
   946
by (auto intro: capprox_mult2 capprox_CFinite_mult_cancel)
paulson@14408
   947
paulson@14408
   948
paulson@14408
   949
subsection{*Theorems About Monads*}
paulson@14408
   950
paulson@14408
   951
lemma capprox_cmonad_iff: "(x @c= y) = (cmonad(x)=cmonad(y))"
paulson@14408
   952
apply (simp add: cmonad_def)
paulson@14408
   953
apply (auto dest: capprox_sym elim!: capprox_trans equalityCE)
paulson@14408
   954
done
paulson@14408
   955
paulson@14408
   956
lemma CInfinitesimal_cmonad_eq:
paulson@14408
   957
     "e \<in> CInfinitesimal ==> cmonad (x+e) = cmonad x"
paulson@14408
   958
by (fast intro!: CInfinitesimal_add_capprox_self [THEN capprox_sym] capprox_cmonad_iff [THEN iffD1])
paulson@14408
   959
paulson@14408
   960
lemma mem_cmonad_iff: "(u \<in> cmonad x) = (-u \<in> cmonad (-x))"
paulson@14408
   961
by (simp add: cmonad_def)
paulson@14408
   962
paulson@14408
   963
lemma CInfinitesimal_cmonad_zero_iff: "(x:CInfinitesimal) = (x \<in> cmonad 0)"
paulson@14408
   964
by (auto intro: capprox_sym simp add: mem_cinfmal_iff cmonad_def)
paulson@14408
   965
paulson@14408
   966
lemma cmonad_zero_minus_iff: "(x \<in> cmonad 0) = (-x \<in> cmonad 0)"
paulson@14408
   967
by (simp add: CInfinitesimal_cmonad_zero_iff [symmetric])
paulson@14408
   968
paulson@14408
   969
lemma cmonad_zero_hcmod_iff: "(x \<in> cmonad 0) = (hcmod x:monad 0)"
paulson@14408
   970
by (simp add: CInfinitesimal_cmonad_zero_iff [symmetric] CInfinitesimal_hcmod_iff Infinitesimal_monad_zero_iff [symmetric])
paulson@14408
   971
paulson@14408
   972
lemma mem_cmonad_self [simp]: "x \<in> cmonad x"
paulson@14408
   973
by (simp add: cmonad_def)
paulson@14408
   974
paulson@14408
   975
paulson@14408
   976
subsection{*Theorems About Standard Part*}
paulson@14408
   977
paulson@14408
   978
lemma stc_capprox_self: "x \<in> CFinite ==> stc x @c= x"
paulson@14408
   979
apply (simp add: stc_def)
paulson@14408
   980
apply (frule stc_part_Ex, safe)
paulson@14408
   981
apply (rule someI2)
paulson@14408
   982
apply (auto intro: capprox_sym)
paulson@14408
   983
done
paulson@14408
   984
paulson@14408
   985
lemma stc_SComplex: "x \<in> CFinite ==> stc x \<in> SComplex"
paulson@14408
   986
apply (simp add: stc_def)
paulson@14408
   987
apply (frule stc_part_Ex, safe)
paulson@14408
   988
apply (rule someI2)
paulson@14408
   989
apply (auto intro: capprox_sym)
paulson@14408
   990
done
paulson@14408
   991
paulson@14408
   992
lemma stc_CFinite: "x \<in> CFinite ==> stc x \<in> CFinite"
paulson@14408
   993
by (erule stc_SComplex [THEN SComplex_subset_CFinite [THEN subsetD]])
paulson@14408
   994
paulson@14408
   995
lemma stc_SComplex_eq [simp]: "x \<in> SComplex ==> stc x = x"
paulson@14408
   996
apply (simp add: stc_def)
paulson@14408
   997
apply (rule some_equality)
paulson@14408
   998
apply (auto intro: SComplex_subset_CFinite [THEN subsetD])
paulson@14408
   999
apply (blast dest: SComplex_capprox_iff [THEN iffD1])
paulson@14408
  1000
done
paulson@14408
  1001
paulson@14408
  1002
lemma stc_hcomplex_of_complex:
paulson@14408
  1003
     "stc (hcomplex_of_complex x) = hcomplex_of_complex x"
paulson@14408
  1004
by auto
paulson@14408
  1005
paulson@14408
  1006
lemma stc_eq_capprox:
paulson@14408
  1007
     "[| x \<in> CFinite; y \<in> CFinite; stc x = stc y |] ==> x @c= y"
paulson@14408
  1008
by (auto dest!: stc_capprox_self elim!: capprox_trans3)
paulson@14408
  1009
paulson@14408
  1010
lemma capprox_stc_eq:
paulson@14408
  1011
     "[| x \<in> CFinite; y \<in> CFinite; x @c= y |] ==> stc x = stc y"
paulson@14408
  1012
by (blast intro: capprox_trans capprox_trans2 SComplex_capprox_iff [THEN iffD1]
paulson@14408
  1013
          dest: stc_capprox_self stc_SComplex)
paulson@13957
  1014
paulson@14408
  1015
lemma stc_eq_capprox_iff:
paulson@14408
  1016
     "[| x \<in> CFinite; y \<in> CFinite|] ==> (x @c= y) = (stc x = stc y)"
paulson@14408
  1017
by (blast intro: capprox_stc_eq stc_eq_capprox)
paulson@14408
  1018
paulson@14408
  1019
lemma stc_CInfinitesimal_add_SComplex:
paulson@14408
  1020
     "[| x \<in> SComplex; e \<in> CInfinitesimal |] ==> stc(x + e) = x"
paulson@14408
  1021
apply (frule stc_SComplex_eq [THEN subst])
paulson@14408
  1022
prefer 2 apply assumption
paulson@14408
  1023
apply (frule SComplex_subset_CFinite [THEN subsetD])
paulson@14408
  1024
apply (frule CInfinitesimal_subset_CFinite [THEN subsetD])
paulson@14408
  1025
apply (drule stc_SComplex_eq)
paulson@14408
  1026
apply (rule capprox_stc_eq)
paulson@14408
  1027
apply (auto intro: CFinite_add simp add: CInfinitesimal_add_capprox_self [THEN capprox_sym])
paulson@14408
  1028
done
paulson@14408
  1029
paulson@14408
  1030
lemma stc_CInfinitesimal_add_SComplex2:
paulson@14408
  1031
     "[| x \<in> SComplex; e \<in> CInfinitesimal |] ==> stc(e + x) = x"
paulson@14408
  1032
apply (rule add_commute [THEN subst])
paulson@14408
  1033
apply (blast intro!: stc_CInfinitesimal_add_SComplex)
paulson@14408
  1034
done
paulson@14408
  1035
paulson@14408
  1036
lemma CFinite_stc_CInfinitesimal_add:
paulson@14408
  1037
     "x \<in> CFinite ==> \<exists>e \<in> CInfinitesimal. x = stc(x) + e"
paulson@14408
  1038
by (blast dest!: stc_capprox_self [THEN capprox_sym] bex_CInfinitesimal_iff2 [THEN iffD2])
paulson@14408
  1039
paulson@14408
  1040
lemma stc_add:
paulson@14408
  1041
     "[| x \<in> CFinite; y \<in> CFinite |] ==> stc (x + y) = stc(x) + stc(y)"
paulson@14408
  1042
apply (frule CFinite_stc_CInfinitesimal_add)
paulson@14408
  1043
apply (frule_tac x = y in CFinite_stc_CInfinitesimal_add, safe)
paulson@14408
  1044
apply (subgoal_tac "stc (x + y) = stc ((stc x + e) + (stc y + ea))")
paulson@14408
  1045
apply (drule_tac [2] sym, drule_tac [2] sym)
paulson@14408
  1046
 prefer 2 apply simp 
paulson@14408
  1047
apply (simp (no_asm_simp) add: add_ac)
paulson@14408
  1048
apply (drule stc_SComplex)+
paulson@14408
  1049
apply (drule SComplex_add, assumption)
paulson@14408
  1050
apply (drule CInfinitesimal_add, assumption)
paulson@14408
  1051
apply (rule add_assoc [THEN subst])
paulson@14408
  1052
apply (blast intro!: stc_CInfinitesimal_add_SComplex2)
paulson@14408
  1053
done
paulson@14408
  1054
paulson@14408
  1055
lemma stc_number_of [simp]: "stc (number_of w) = number_of w"
paulson@14408
  1056
by (rule SComplex_number_of [THEN stc_SComplex_eq])
paulson@14408
  1057
paulson@14408
  1058
lemma stc_zero [simp]: "stc 0 = 0"
paulson@14408
  1059
by simp
paulson@14408
  1060
paulson@14408
  1061
lemma stc_one [simp]: "stc 1 = 1"
paulson@14408
  1062
by simp
paulson@14408
  1063
paulson@14408
  1064
lemma stc_minus: "y \<in> CFinite ==> stc(-y) = -stc(y)"
paulson@14408
  1065
apply (frule CFinite_minus_iff [THEN iffD2])
paulson@14408
  1066
apply (rule hcomplex_add_minus_eq_minus)
paulson@14408
  1067
apply (drule stc_add [symmetric], assumption)
paulson@14408
  1068
apply (simp add: add_commute)
paulson@14408
  1069
done
paulson@14408
  1070
paulson@14408
  1071
lemma stc_diff: 
paulson@14408
  1072
     "[| x \<in> CFinite; y \<in> CFinite |] ==> stc (x-y) = stc(x) - stc(y)"
paulson@14408
  1073
apply (simp add: diff_minus)
paulson@14408
  1074
apply (frule_tac y1 = y in stc_minus [symmetric])
paulson@14408
  1075
apply (drule_tac x1 = y in CFinite_minus_iff [THEN iffD2])
paulson@14408
  1076
apply (auto intro: stc_add)
paulson@14408
  1077
done
paulson@14408
  1078
paulson@14408
  1079
lemma lemma_stc_mult:
paulson@14408
  1080
     "[| x \<in> CFinite; y \<in> CFinite;  
paulson@14408
  1081
         e \<in> CInfinitesimal;        
paulson@14408
  1082
         ea: CInfinitesimal |]    
paulson@14408
  1083
       ==> e*y + x*ea + e*ea: CInfinitesimal"
paulson@14408
  1084
apply (frule_tac x = e and y = y in CInfinitesimal_CFinite_mult)
paulson@14408
  1085
apply (frule_tac [2] x = ea and y = x in CInfinitesimal_CFinite_mult)
paulson@14408
  1086
apply (drule_tac [3] CInfinitesimal_mult)
paulson@14408
  1087
apply (auto intro: CInfinitesimal_add simp add: add_ac mult_ac)
paulson@14408
  1088
done
paulson@14408
  1089
paulson@14408
  1090
lemma stc_mult:
paulson@14408
  1091
     "[| x \<in> CFinite; y \<in> CFinite |]  
paulson@14408
  1092
               ==> stc (x * y) = stc(x) * stc(y)"
paulson@14408
  1093
apply (frule CFinite_stc_CInfinitesimal_add)
paulson@14408
  1094
apply (frule_tac x = y in CFinite_stc_CInfinitesimal_add, safe)
paulson@14408
  1095
apply (subgoal_tac "stc (x * y) = stc ((stc x + e) * (stc y + ea))")
paulson@14408
  1096
apply (drule_tac [2] sym, drule_tac [2] sym)
paulson@14408
  1097
 prefer 2 apply simp 
paulson@14408
  1098
apply (erule_tac V = "x = stc x + e" in thin_rl)
paulson@14408
  1099
apply (erule_tac V = "y = stc y + ea" in thin_rl)
paulson@14408
  1100
apply (simp add: hcomplex_add_mult_distrib right_distrib)
paulson@14408
  1101
apply (drule stc_SComplex)+
paulson@14408
  1102
apply (simp (no_asm_use) add: add_assoc)
paulson@14408
  1103
apply (rule stc_CInfinitesimal_add_SComplex)
paulson@14408
  1104
apply (blast intro!: SComplex_mult)
paulson@14408
  1105
apply (drule SComplex_subset_CFinite [THEN subsetD])+
paulson@14408
  1106
apply (rule add_assoc [THEN subst])
paulson@14408
  1107
apply (blast intro!: lemma_stc_mult)
paulson@14408
  1108
done
paulson@14408
  1109
paulson@14408
  1110
lemma stc_CInfinitesimal: "x \<in> CInfinitesimal ==> stc x = 0"
paulson@14408
  1111
apply (rule stc_zero [THEN subst])
paulson@14408
  1112
apply (rule capprox_stc_eq)
paulson@14408
  1113
apply (auto intro: CInfinitesimal_subset_CFinite [THEN subsetD]
paulson@14408
  1114
                 simp add: mem_cinfmal_iff [symmetric])
paulson@14408
  1115
done
paulson@14408
  1116
paulson@14408
  1117
lemma stc_not_CInfinitesimal: "stc(x) \<noteq> 0 ==> x \<notin> CInfinitesimal"
paulson@14408
  1118
by (fast intro: stc_CInfinitesimal)
paulson@14408
  1119
paulson@14408
  1120
lemma stc_inverse:
paulson@14408
  1121
     "[| x \<in> CFinite; stc x \<noteq> 0 |]  
paulson@14408
  1122
      ==> stc(inverse x) = inverse (stc x)"
paulson@14408
  1123
apply (rule_tac c1 = "stc x" in hcomplex_mult_left_cancel [THEN iffD1])
paulson@14408
  1124
apply (auto simp add: stc_mult [symmetric] stc_not_CInfinitesimal CFinite_inverse)
paulson@14408
  1125
apply (subst right_inverse, auto)
paulson@14408
  1126
done
paulson@14408
  1127
paulson@14408
  1128
lemma stc_divide [simp]:
paulson@14408
  1129
     "[| x \<in> CFinite; y \<in> CFinite; stc y \<noteq> 0 |]  
paulson@14408
  1130
      ==> stc(x/y) = (stc x) / (stc y)"
paulson@14430
  1131
by (simp add: divide_inverse stc_mult stc_not_CInfinitesimal CFinite_inverse stc_inverse)
paulson@14408
  1132
paulson@14408
  1133
lemma stc_idempotent [simp]: "x \<in> CFinite ==> stc(stc(x)) = stc(x)"
paulson@14408
  1134
by (blast intro: stc_CFinite stc_capprox_self capprox_stc_eq)
paulson@14408
  1135
paulson@14408
  1136
lemma CFinite_HFinite_hcomplex_of_hypreal:
paulson@14408
  1137
     "z \<in> HFinite ==> hcomplex_of_hypreal z \<in> CFinite"
paulson@14469
  1138
apply (cases z)
paulson@14408
  1139
apply (simp add: hcomplex_of_hypreal CFinite_HFinite_iff hypreal_zero_def [symmetric])
paulson@14408
  1140
done
paulson@14408
  1141
paulson@14408
  1142
lemma SComplex_SReal_hcomplex_of_hypreal:
paulson@14408
  1143
     "x \<in> Reals ==>  hcomplex_of_hypreal x \<in> SComplex"
paulson@14469
  1144
apply (cases x)
paulson@14408
  1145
apply (simp add: hcomplex_of_hypreal SComplex_SReal_iff hypreal_zero_def [symmetric])
paulson@14408
  1146
done
paulson@14408
  1147
paulson@14408
  1148
lemma stc_hcomplex_of_hypreal: 
paulson@14408
  1149
 "z \<in> HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)"
paulson@14408
  1150
apply (simp add: st_def stc_def)
paulson@14408
  1151
apply (frule st_part_Ex, safe)
paulson@14408
  1152
apply (rule someI2)
paulson@14408
  1153
apply (auto intro: approx_sym)
paulson@14408
  1154
apply (drule CFinite_HFinite_hcomplex_of_hypreal)
paulson@14408
  1155
apply (frule stc_part_Ex, safe)
paulson@14408
  1156
apply (rule someI2)
paulson@14408
  1157
apply (auto intro: capprox_sym intro!: capprox_unique_complex dest: SComplex_SReal_hcomplex_of_hypreal)
paulson@14408
  1158
done
paulson@14408
  1159
paulson@14408
  1160
(*
paulson@14408
  1161
Goal "x \<in> CFinite ==> hcmod(stc x) = st(hcmod x)"
paulson@14408
  1162
by (dtac stc_capprox_self 1)
paulson@14408
  1163
by (auto_tac (claset(),simpset() addsimps [bex_CInfinitesimal_iff2 RS sym]));
paulson@14408
  1164
paulson@14408
  1165
paulson@14408
  1166
approx_hcmod_add_hcmod
paulson@14408
  1167
*)
paulson@14408
  1168
paulson@14408
  1169
lemma CInfinitesimal_hcnj_iff [simp]:
paulson@14408
  1170
     "(hcnj z \<in> CInfinitesimal) = (z \<in> CInfinitesimal)"
paulson@14408
  1171
by (simp add: CInfinitesimal_hcmod_iff)
paulson@14408
  1172
paulson@14408
  1173
lemma CInfinite_HInfinite_iff:
paulson@14408
  1174
     "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CInfinite) =  
paulson@14408
  1175
      (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HInfinite |  
paulson@14408
  1176
       Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HInfinite)"
paulson@14408
  1177
by (simp add: CInfinite_CFinite_iff HInfinite_HFinite_iff CFinite_HFinite_iff)
paulson@14408
  1178
paulson@14408
  1179
text{*These theorems should probably be deleted*}
paulson@14408
  1180
lemma hcomplex_split_CInfinitesimal_iff:
paulson@14408
  1181
     "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CInfinitesimal) =  
paulson@14408
  1182
      (x \<in> Infinitesimal & y \<in> Infinitesimal)"
paulson@14469
  1183
apply (cases x, cases y)
paulson@14408
  1184
apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CInfinitesimal_Infinitesimal_iff)
paulson@14408
  1185
done
paulson@14408
  1186
paulson@14408
  1187
lemma hcomplex_split_CFinite_iff:
paulson@14408
  1188
     "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CFinite) =  
paulson@14408
  1189
      (x \<in> HFinite & y \<in> HFinite)"
paulson@14469
  1190
apply (cases x, cases y)
paulson@14408
  1191
apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CFinite_HFinite_iff)
paulson@14408
  1192
done
paulson@14408
  1193
paulson@14408
  1194
lemma hcomplex_split_SComplex_iff:
paulson@14408
  1195
     "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> SComplex) =  
paulson@14408
  1196
      (x \<in> Reals & y \<in> Reals)"
paulson@14469
  1197
apply (cases x, cases y)
paulson@14408
  1198
apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal SComplex_SReal_iff)
paulson@14408
  1199
done
paulson@14408
  1200
paulson@14408
  1201
lemma hcomplex_split_CInfinite_iff:
paulson@14408
  1202
     "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CInfinite) =  
paulson@14408
  1203
      (x \<in> HInfinite | y \<in> HInfinite)"
paulson@14469
  1204
apply (cases x, cases y)
paulson@14408
  1205
apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CInfinite_HInfinite_iff)
paulson@14408
  1206
done
paulson@14408
  1207
paulson@14408
  1208
lemma hcomplex_split_capprox_iff:
paulson@14408
  1209
     "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @c=  
paulson@14408
  1210
       hcomplex_of_hypreal x' + iii * hcomplex_of_hypreal y') =  
paulson@14408
  1211
      (x @= x' & y @= y')"
paulson@14469
  1212
apply (cases x, cases y, cases x', cases y')
paulson@14408
  1213
apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal capprox_approx_iff)
paulson@14408
  1214
done
paulson@14408
  1215
paulson@14408
  1216
lemma complex_seq_to_hcomplex_CInfinitesimal:
paulson@14408
  1217
     "\<forall>n. cmod (X n - x) < inverse (real (Suc n)) ==>  
paulson@14408
  1218
      Abs_hcomplex(hcomplexrel``{X}) - hcomplex_of_complex x \<in> CInfinitesimal"
paulson@14408
  1219
apply (simp add: hcomplex_diff CInfinitesimal_hcmod_iff hcomplex_of_complex_def Infinitesimal_FreeUltrafilterNat_iff hcmod)
paulson@14408
  1220
apply (rule bexI, auto)
paulson@14408
  1221
apply (auto dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset)
paulson@14408
  1222
done
paulson@14408
  1223
paulson@14408
  1224
lemma CInfinitesimal_hcomplex_of_hypreal_epsilon [simp]:
paulson@14408
  1225
     "hcomplex_of_hypreal epsilon \<in> CInfinitesimal"
paulson@14408
  1226
by (simp add: CInfinitesimal_hcmod_iff)
paulson@14408
  1227
paulson@14408
  1228
lemma hcomplex_of_complex_approx_zero_iff [simp]:
paulson@14408
  1229
     "(hcomplex_of_complex z @c= 0) = (z = 0)"
paulson@14408
  1230
by (simp add: hcomplex_of_complex_zero [symmetric]
paulson@14408
  1231
         del: hcomplex_of_complex_zero)
paulson@14408
  1232
paulson@14408
  1233
lemma hcomplex_of_complex_approx_zero_iff2 [simp]:
paulson@14408
  1234
     "(0 @c= hcomplex_of_complex z) = (z = 0)"
paulson@14408
  1235
by (simp add: hcomplex_of_complex_zero [symmetric]
paulson@14408
  1236
         del: hcomplex_of_complex_zero)
paulson@14408
  1237
paulson@14408
  1238
paulson@14408
  1239
ML
paulson@14408
  1240
{*
paulson@14408
  1241
val SComplex_add = thm "SComplex_add";
paulson@14408
  1242
val SComplex_mult = thm "SComplex_mult";
paulson@14408
  1243
val SComplex_inverse = thm "SComplex_inverse";
paulson@14408
  1244
val SComplex_divide = thm "SComplex_divide";
paulson@14408
  1245
val SComplex_minus = thm "SComplex_minus";
paulson@14408
  1246
val SComplex_minus_iff = thm "SComplex_minus_iff";
paulson@14408
  1247
val SComplex_diff = thm "SComplex_diff";
paulson@14408
  1248
val SComplex_add_cancel = thm "SComplex_add_cancel";
paulson@14408
  1249
val SReal_hcmod_hcomplex_of_complex = thm "SReal_hcmod_hcomplex_of_complex";
paulson@14408
  1250
val SReal_hcmod_number_of = thm "SReal_hcmod_number_of";
paulson@14408
  1251
val SReal_hcmod_SComplex = thm "SReal_hcmod_SComplex";
paulson@14408
  1252
val SComplex_hcomplex_of_complex = thm "SComplex_hcomplex_of_complex";
paulson@14408
  1253
val SComplex_number_of = thm "SComplex_number_of";
paulson@14408
  1254
val SComplex_divide_number_of = thm "SComplex_divide_number_of";
paulson@14408
  1255
val SComplex_UNIV_complex = thm "SComplex_UNIV_complex";
paulson@14408
  1256
val SComplex_iff = thm "SComplex_iff";
paulson@14408
  1257
val hcomplex_of_complex_image = thm "hcomplex_of_complex_image";
paulson@14408
  1258
val inv_hcomplex_of_complex_image = thm "inv_hcomplex_of_complex_image";
paulson@14408
  1259
val SComplex_hcomplex_of_complex_image = thm "SComplex_hcomplex_of_complex_image";
paulson@14408
  1260
val SComplex_SReal_dense = thm "SComplex_SReal_dense";
paulson@14408
  1261
val SComplex_hcmod_SReal = thm "SComplex_hcmod_SReal";
paulson@14408
  1262
val SComplex_zero = thm "SComplex_zero";
paulson@14408
  1263
val SComplex_one = thm "SComplex_one";
paulson@14408
  1264
val CFinite_add = thm "CFinite_add";
paulson@14408
  1265
val CFinite_mult = thm "CFinite_mult";
paulson@14408
  1266
val CFinite_minus_iff = thm "CFinite_minus_iff";
paulson@14408
  1267
val SComplex_subset_CFinite = thm "SComplex_subset_CFinite";
paulson@14408
  1268
val HFinite_hcmod_hcomplex_of_complex = thm "HFinite_hcmod_hcomplex_of_complex";
paulson@14408
  1269
val CFinite_hcomplex_of_complex = thm "CFinite_hcomplex_of_complex";
paulson@14408
  1270
val CFiniteD = thm "CFiniteD";
paulson@14408
  1271
val CFinite_hcmod_iff = thm "CFinite_hcmod_iff";
paulson@14408
  1272
val CFinite_number_of = thm "CFinite_number_of";
paulson@14408
  1273
val CFinite_bounded = thm "CFinite_bounded";
paulson@14408
  1274
val CInfinitesimal_zero = thm "CInfinitesimal_zero";
paulson@14408
  1275
val hcomplex_sum_of_halves = thm "hcomplex_sum_of_halves";
paulson@14408
  1276
val CInfinitesimal_hcmod_iff = thm "CInfinitesimal_hcmod_iff";
paulson@14408
  1277
val one_not_CInfinitesimal = thm "one_not_CInfinitesimal";
paulson@14408
  1278
val CInfinitesimal_add = thm "CInfinitesimal_add";
paulson@14408
  1279
val CInfinitesimal_minus_iff = thm "CInfinitesimal_minus_iff";
paulson@14408
  1280
val CInfinitesimal_diff = thm "CInfinitesimal_diff";
paulson@14408
  1281
val CInfinitesimal_mult = thm "CInfinitesimal_mult";
paulson@14408
  1282
val CInfinitesimal_CFinite_mult = thm "CInfinitesimal_CFinite_mult";
paulson@14408
  1283
val CInfinitesimal_CFinite_mult2 = thm "CInfinitesimal_CFinite_mult2";
paulson@14408
  1284
val CInfinite_hcmod_iff = thm "CInfinite_hcmod_iff";
paulson@14408
  1285
val CInfinite_inverse_CInfinitesimal = thm "CInfinite_inverse_CInfinitesimal";
paulson@14408
  1286
val CInfinite_mult = thm "CInfinite_mult";
paulson@14408
  1287
val CInfinite_minus_iff = thm "CInfinite_minus_iff";
paulson@14408
  1288
val CFinite_sum_squares = thm "CFinite_sum_squares";
paulson@14408
  1289
val not_CInfinitesimal_not_zero = thm "not_CInfinitesimal_not_zero";
paulson@14408
  1290
val not_CInfinitesimal_not_zero2 = thm "not_CInfinitesimal_not_zero2";
paulson@14408
  1291
val CFinite_diff_CInfinitesimal_hcmod = thm "CFinite_diff_CInfinitesimal_hcmod";
paulson@14408
  1292
val hcmod_less_CInfinitesimal = thm "hcmod_less_CInfinitesimal";
paulson@14408
  1293
val hcmod_le_CInfinitesimal = thm "hcmod_le_CInfinitesimal";
paulson@14408
  1294
val CInfinitesimal_interval = thm "CInfinitesimal_interval";
paulson@14408
  1295
val CInfinitesimal_interval2 = thm "CInfinitesimal_interval2";
paulson@14408
  1296
val not_CInfinitesimal_mult = thm "not_CInfinitesimal_mult";
paulson@14408
  1297
val CInfinitesimal_mult_disj = thm "CInfinitesimal_mult_disj";
paulson@14408
  1298
val CFinite_CInfinitesimal_diff_mult = thm "CFinite_CInfinitesimal_diff_mult";
paulson@14408
  1299
val CInfinitesimal_subset_CFinite = thm "CInfinitesimal_subset_CFinite";
paulson@14408
  1300
val CInfinitesimal_hcomplex_of_complex_mult = thm "CInfinitesimal_hcomplex_of_complex_mult";
paulson@14408
  1301
val CInfinitesimal_hcomplex_of_complex_mult2 = thm "CInfinitesimal_hcomplex_of_complex_mult2";
paulson@14408
  1302
val mem_cinfmal_iff = thm "mem_cinfmal_iff";
paulson@14408
  1303
val capprox_minus_iff = thm "capprox_minus_iff";
paulson@14408
  1304
val capprox_minus_iff2 = thm "capprox_minus_iff2";
paulson@14408
  1305
val capprox_refl = thm "capprox_refl";
paulson@14408
  1306
val capprox_sym = thm "capprox_sym";
paulson@14408
  1307
val capprox_trans = thm "capprox_trans";
paulson@14408
  1308
val capprox_trans2 = thm "capprox_trans2";
paulson@14408
  1309
val capprox_trans3 = thm "capprox_trans3";
paulson@14408
  1310
val number_of_capprox_reorient = thm "number_of_capprox_reorient";
paulson@14408
  1311
val CInfinitesimal_capprox_minus = thm "CInfinitesimal_capprox_minus";
paulson@14408
  1312
val capprox_monad_iff = thm "capprox_monad_iff";
paulson@14408
  1313
val Infinitesimal_capprox = thm "Infinitesimal_capprox";
paulson@14408
  1314
val capprox_add = thm "capprox_add";
paulson@14408
  1315
val capprox_minus = thm "capprox_minus";
paulson@14408
  1316
val capprox_minus2 = thm "capprox_minus2";
paulson@14408
  1317
val capprox_minus_cancel = thm "capprox_minus_cancel";
paulson@14408
  1318
val capprox_add_minus = thm "capprox_add_minus";
paulson@14408
  1319
val capprox_mult1 = thm "capprox_mult1";
paulson@14408
  1320
val capprox_mult2 = thm "capprox_mult2";
paulson@14408
  1321
val capprox_mult_subst = thm "capprox_mult_subst";
paulson@14408
  1322
val capprox_mult_subst2 = thm "capprox_mult_subst2";
paulson@14408
  1323
val capprox_mult_subst_SComplex = thm "capprox_mult_subst_SComplex";
paulson@14408
  1324
val capprox_eq_imp = thm "capprox_eq_imp";
paulson@14408
  1325
val CInfinitesimal_minus_capprox = thm "CInfinitesimal_minus_capprox";
paulson@14408
  1326
val bex_CInfinitesimal_iff = thm "bex_CInfinitesimal_iff";
paulson@14408
  1327
val bex_CInfinitesimal_iff2 = thm "bex_CInfinitesimal_iff2";
paulson@14408
  1328
val CInfinitesimal_add_capprox = thm "CInfinitesimal_add_capprox";
paulson@14408
  1329
val CInfinitesimal_add_capprox_self = thm "CInfinitesimal_add_capprox_self";
paulson@14408
  1330
val CInfinitesimal_add_capprox_self2 = thm "CInfinitesimal_add_capprox_self2";
paulson@14408
  1331
val CInfinitesimal_add_minus_capprox_self = thm "CInfinitesimal_add_minus_capprox_self";
paulson@14408
  1332
val CInfinitesimal_add_cancel = thm "CInfinitesimal_add_cancel";
paulson@14408
  1333
val CInfinitesimal_add_right_cancel = thm "CInfinitesimal_add_right_cancel";
paulson@14408
  1334
val capprox_add_left_cancel = thm "capprox_add_left_cancel";
paulson@14408
  1335
val capprox_add_right_cancel = thm "capprox_add_right_cancel";
paulson@14408
  1336
val capprox_add_mono1 = thm "capprox_add_mono1";
paulson@14408
  1337
val capprox_add_mono2 = thm "capprox_add_mono2";
paulson@14408
  1338
val capprox_add_left_iff = thm "capprox_add_left_iff";
paulson@14408
  1339
val capprox_add_right_iff = thm "capprox_add_right_iff";
paulson@14408
  1340
val capprox_CFinite = thm "capprox_CFinite";
paulson@14408
  1341
val capprox_hcomplex_of_complex_CFinite = thm "capprox_hcomplex_of_complex_CFinite";
paulson@14408
  1342
val capprox_mult_CFinite = thm "capprox_mult_CFinite";
paulson@14408
  1343
val capprox_mult_hcomplex_of_complex = thm "capprox_mult_hcomplex_of_complex";
paulson@14408
  1344
val capprox_SComplex_mult_cancel_zero = thm "capprox_SComplex_mult_cancel_zero";
paulson@14408
  1345
val capprox_mult_SComplex1 = thm "capprox_mult_SComplex1";
paulson@14408
  1346
val capprox_mult_SComplex2 = thm "capprox_mult_SComplex2";
paulson@14408
  1347
val capprox_mult_SComplex_zero_cancel_iff = thm "capprox_mult_SComplex_zero_cancel_iff";
paulson@14408
  1348
val capprox_SComplex_mult_cancel = thm "capprox_SComplex_mult_cancel";
paulson@14408
  1349
val capprox_SComplex_mult_cancel_iff1 = thm "capprox_SComplex_mult_cancel_iff1";
paulson@14408
  1350
val capprox_hcmod_approx_zero = thm "capprox_hcmod_approx_zero";
paulson@14408
  1351
val capprox_approx_zero_iff = thm "capprox_approx_zero_iff";
paulson@14408
  1352
val capprox_minus_zero_cancel_iff = thm "capprox_minus_zero_cancel_iff";
paulson@14408
  1353
val Infinitesimal_hcmod_add_diff = thm "Infinitesimal_hcmod_add_diff";
paulson@14408
  1354
val approx_hcmod_add_hcmod = thm "approx_hcmod_add_hcmod";
paulson@14408
  1355
val capprox_hcmod_approx = thm "capprox_hcmod_approx";
paulson@14408
  1356
val CInfinitesimal_less_SComplex = thm "CInfinitesimal_less_SComplex";
paulson@14408
  1357
val SComplex_Int_CInfinitesimal_zero = thm "SComplex_Int_CInfinitesimal_zero";
paulson@14408
  1358
val SComplex_CInfinitesimal_zero = thm "SComplex_CInfinitesimal_zero";
paulson@14408
  1359
val SComplex_CFinite_diff_CInfinitesimal = thm "SComplex_CFinite_diff_CInfinitesimal";
paulson@14408
  1360
val hcomplex_of_complex_CFinite_diff_CInfinitesimal = thm "hcomplex_of_complex_CFinite_diff_CInfinitesimal";
paulson@14408
  1361
val hcomplex_of_complex_CInfinitesimal_iff_0 = thm "hcomplex_of_complex_CInfinitesimal_iff_0";
paulson@14408
  1362
val number_of_not_CInfinitesimal = thm "number_of_not_CInfinitesimal";
paulson@14408
  1363
val capprox_SComplex_not_zero = thm "capprox_SComplex_not_zero";
paulson@14408
  1364
val CFinite_diff_CInfinitesimal_capprox = thm "CFinite_diff_CInfinitesimal_capprox";
paulson@14408
  1365
val CInfinitesimal_ratio = thm "CInfinitesimal_ratio";
paulson@14408
  1366
val SComplex_capprox_iff = thm "SComplex_capprox_iff";
paulson@14408
  1367
val number_of_capprox_iff = thm "number_of_capprox_iff";
paulson@14408
  1368
val number_of_CInfinitesimal_iff = thm "number_of_CInfinitesimal_iff";
paulson@14408
  1369
val hcomplex_of_complex_approx_iff = thm "hcomplex_of_complex_approx_iff";
paulson@14408
  1370
val hcomplex_of_complex_capprox_number_of_iff = thm "hcomplex_of_complex_capprox_number_of_iff";
paulson@14408
  1371
val capprox_unique_complex = thm "capprox_unique_complex";
paulson@14408
  1372
val hcomplex_capproxD1 = thm "hcomplex_capproxD1";
paulson@14408
  1373
val hcomplex_capproxD2 = thm "hcomplex_capproxD2";
paulson@14408
  1374
val hcomplex_capproxI = thm "hcomplex_capproxI";
paulson@14408
  1375
val capprox_approx_iff = thm "capprox_approx_iff";
paulson@14408
  1376
val hcomplex_of_hypreal_capprox_iff = thm "hcomplex_of_hypreal_capprox_iff";
paulson@14408
  1377
val CFinite_HFinite_Re = thm "CFinite_HFinite_Re";
paulson@14408
  1378
val CFinite_HFinite_Im = thm "CFinite_HFinite_Im";
paulson@14408
  1379
val HFinite_Re_Im_CFinite = thm "HFinite_Re_Im_CFinite";
paulson@14408
  1380
val CFinite_HFinite_iff = thm "CFinite_HFinite_iff";
paulson@14408
  1381
val SComplex_Re_SReal = thm "SComplex_Re_SReal";
paulson@14408
  1382
val SComplex_Im_SReal = thm "SComplex_Im_SReal";
paulson@14408
  1383
val Reals_Re_Im_SComplex = thm "Reals_Re_Im_SComplex";
paulson@14408
  1384
val SComplex_SReal_iff = thm "SComplex_SReal_iff";
paulson@14408
  1385
val CInfinitesimal_Infinitesimal_iff = thm "CInfinitesimal_Infinitesimal_iff";
paulson@14408
  1386
val eq_Abs_hcomplex_Bex = thm "eq_Abs_hcomplex_Bex";
paulson@14408
  1387
val stc_part_Ex = thm "stc_part_Ex";
paulson@14408
  1388
val stc_part_Ex1 = thm "stc_part_Ex1";
paulson@14408
  1389
val CFinite_Int_CInfinite_empty = thm "CFinite_Int_CInfinite_empty";
paulson@14408
  1390
val CFinite_not_CInfinite = thm "CFinite_not_CInfinite";
paulson@14408
  1391
val not_CFinite_CInfinite = thm "not_CFinite_CInfinite";
paulson@14408
  1392
val CInfinite_CFinite_disj = thm "CInfinite_CFinite_disj";
paulson@14408
  1393
val CInfinite_CFinite_iff = thm "CInfinite_CFinite_iff";
paulson@14408
  1394
val CFinite_CInfinite_iff = thm "CFinite_CInfinite_iff";
paulson@14408
  1395
val CInfinite_diff_CFinite_CInfinitesimal_disj = thm "CInfinite_diff_CFinite_CInfinitesimal_disj";
paulson@14408
  1396
val CFinite_inverse = thm "CFinite_inverse";
paulson@14408
  1397
val CFinite_inverse2 = thm "CFinite_inverse2";
paulson@14408
  1398
val CInfinitesimal_inverse_CFinite = thm "CInfinitesimal_inverse_CFinite";
paulson@14408
  1399
val CFinite_not_CInfinitesimal_inverse = thm "CFinite_not_CInfinitesimal_inverse";
paulson@14408
  1400
val capprox_inverse = thm "capprox_inverse";
paulson@14408
  1401
val hcomplex_of_complex_capprox_inverse = thms "hcomplex_of_complex_capprox_inverse";
paulson@14408
  1402
val inverse_add_CInfinitesimal_capprox = thm "inverse_add_CInfinitesimal_capprox";
paulson@14408
  1403
val inverse_add_CInfinitesimal_capprox2 = thm "inverse_add_CInfinitesimal_capprox2";
paulson@14408
  1404
val inverse_add_CInfinitesimal_approx_CInfinitesimal = thm "inverse_add_CInfinitesimal_approx_CInfinitesimal";
paulson@14408
  1405
val CInfinitesimal_square_iff = thm "CInfinitesimal_square_iff";
paulson@14408
  1406
val capprox_CFinite_mult_cancel = thm "capprox_CFinite_mult_cancel";
paulson@14408
  1407
val capprox_CFinite_mult_cancel_iff1 = thm "capprox_CFinite_mult_cancel_iff1";
paulson@14408
  1408
val capprox_cmonad_iff = thm "capprox_cmonad_iff";
paulson@14408
  1409
val CInfinitesimal_cmonad_eq = thm "CInfinitesimal_cmonad_eq";
paulson@14408
  1410
val mem_cmonad_iff = thm "mem_cmonad_iff";
paulson@14408
  1411
val CInfinitesimal_cmonad_zero_iff = thm "CInfinitesimal_cmonad_zero_iff";
paulson@14408
  1412
val cmonad_zero_minus_iff = thm "cmonad_zero_minus_iff";
paulson@14408
  1413
val cmonad_zero_hcmod_iff = thm "cmonad_zero_hcmod_iff";
paulson@14408
  1414
val mem_cmonad_self = thm "mem_cmonad_self";
paulson@14408
  1415
val stc_capprox_self = thm "stc_capprox_self";
paulson@14408
  1416
val stc_SComplex = thm "stc_SComplex";
paulson@14408
  1417
val stc_CFinite = thm "stc_CFinite";
paulson@14408
  1418
val stc_SComplex_eq = thm "stc_SComplex_eq";
paulson@14408
  1419
val stc_hcomplex_of_complex = thm "stc_hcomplex_of_complex";
paulson@14408
  1420
val stc_eq_capprox = thm "stc_eq_capprox";
paulson@14408
  1421
val capprox_stc_eq = thm "capprox_stc_eq";
paulson@14408
  1422
val stc_eq_capprox_iff = thm "stc_eq_capprox_iff";
paulson@14408
  1423
val stc_CInfinitesimal_add_SComplex = thm "stc_CInfinitesimal_add_SComplex";
paulson@14408
  1424
val stc_CInfinitesimal_add_SComplex2 = thm "stc_CInfinitesimal_add_SComplex2";
paulson@14408
  1425
val CFinite_stc_CInfinitesimal_add = thm "CFinite_stc_CInfinitesimal_add";
paulson@14408
  1426
val stc_add = thm "stc_add";
paulson@14408
  1427
val stc_number_of = thm "stc_number_of";
paulson@14408
  1428
val stc_zero = thm "stc_zero";
paulson@14408
  1429
val stc_one = thm "stc_one";
paulson@14408
  1430
val stc_minus = thm "stc_minus";
paulson@14408
  1431
val stc_diff = thm "stc_diff";
paulson@14408
  1432
val lemma_stc_mult = thm "lemma_stc_mult";
paulson@14408
  1433
val stc_mult = thm "stc_mult";
paulson@14408
  1434
val stc_CInfinitesimal = thm "stc_CInfinitesimal";
paulson@14408
  1435
val stc_not_CInfinitesimal = thm "stc_not_CInfinitesimal";
paulson@14408
  1436
val stc_inverse = thm "stc_inverse";
paulson@14408
  1437
val stc_divide = thm "stc_divide";
paulson@14408
  1438
val stc_idempotent = thm "stc_idempotent";
paulson@14408
  1439
val CFinite_HFinite_hcomplex_of_hypreal = thm "CFinite_HFinite_hcomplex_of_hypreal";
paulson@14408
  1440
val SComplex_SReal_hcomplex_of_hypreal = thm "SComplex_SReal_hcomplex_of_hypreal";
paulson@14408
  1441
val stc_hcomplex_of_hypreal = thm "stc_hcomplex_of_hypreal";
paulson@14408
  1442
val CInfinitesimal_hcnj_iff = thm "CInfinitesimal_hcnj_iff";
paulson@14408
  1443
val CInfinite_HInfinite_iff = thm "CInfinite_HInfinite_iff";
paulson@14408
  1444
val hcomplex_split_CInfinitesimal_iff = thm "hcomplex_split_CInfinitesimal_iff";
paulson@14408
  1445
val hcomplex_split_CFinite_iff = thm "hcomplex_split_CFinite_iff";
paulson@14408
  1446
val hcomplex_split_SComplex_iff = thm "hcomplex_split_SComplex_iff";
paulson@14408
  1447
val hcomplex_split_CInfinite_iff = thm "hcomplex_split_CInfinite_iff";
paulson@14408
  1448
val hcomplex_split_capprox_iff = thm "hcomplex_split_capprox_iff";
paulson@14408
  1449
val complex_seq_to_hcomplex_CInfinitesimal = thm "complex_seq_to_hcomplex_CInfinitesimal";
paulson@14408
  1450
val CInfinitesimal_hcomplex_of_hypreal_epsilon = thm "CInfinitesimal_hcomplex_of_hypreal_epsilon";
paulson@14408
  1451
val hcomplex_of_complex_approx_zero_iff = thm "hcomplex_of_complex_approx_zero_iff";
paulson@14408
  1452
val hcomplex_of_complex_approx_zero_iff2 = thm "hcomplex_of_complex_approx_zero_iff2";
paulson@14408
  1453
*}
paulson@14408
  1454
paulson@13957
  1455
 
paulson@13957
  1456
end