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