src/HOL/Complex/NSComplex.thy
changeset 14374 61de62096768
parent 14373 67a628beb981
child 14377 f454b3004f8f
     1.1 --- a/src/HOL/Complex/NSComplex.thy	Tue Feb 03 11:06:36 2004 +0100
     1.2 +++ b/src/HOL/Complex/NSComplex.thy	Tue Feb 03 15:58:31 2004 +0100
     1.3 @@ -127,38 +127,26 @@
     1.4               hcomplexrel `` {%n. (X n) ^ (Y n)})"
     1.5  
     1.6  
     1.7 -lemma hcomplexrel_iff:
     1.8 -   "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
     1.9 -apply (unfold hcomplexrel_def)
    1.10 -apply fast
    1.11 -done
    1.12 -
    1.13  lemma hcomplexrel_refl: "(x,x): hcomplexrel"
    1.14 -apply (simp add: hcomplexrel_iff) 
    1.15 -done
    1.16 +by (simp add: hcomplexrel_def)
    1.17  
    1.18  lemma hcomplexrel_sym: "(x,y): hcomplexrel ==> (y,x):hcomplexrel"
    1.19 -apply (auto simp add: hcomplexrel_iff eq_commute)
    1.20 -done
    1.21 +by (auto simp add: hcomplexrel_def eq_commute)
    1.22  
    1.23  lemma hcomplexrel_trans:
    1.24        "[|(x,y): hcomplexrel; (y,z):hcomplexrel|] ==> (x,z):hcomplexrel"
    1.25 -apply (simp add: hcomplexrel_iff) 
    1.26 -apply ultra
    1.27 -done
    1.28 +by (simp add: hcomplexrel_def, ultra)
    1.29  
    1.30  lemma equiv_hcomplexrel: "equiv UNIV hcomplexrel"
    1.31 -apply (simp add: equiv_def refl_def sym_def trans_def hcomplexrel_refl) 
    1.32 -apply (blast intro: hcomplexrel_sym hcomplexrel_trans) 
    1.33 +apply (simp add: equiv_def refl_def sym_def trans_def hcomplexrel_refl)
    1.34 +apply (blast intro: hcomplexrel_sym hcomplexrel_trans)
    1.35  done
    1.36  
    1.37  lemmas equiv_hcomplexrel_iff =
    1.38      eq_equiv_class_iff [OF equiv_hcomplexrel UNIV_I UNIV_I, simp]
    1.39  
    1.40  lemma hcomplexrel_in_hcomplex [simp]: "hcomplexrel``{x} : hcomplex"
    1.41 -apply (unfold hcomplex_def hcomplexrel_def quotient_def)
    1.42 -apply blast
    1.43 -done
    1.44 +by (simp add: hcomplex_def hcomplexrel_def quotient_def, blast)
    1.45  
    1.46  lemma inj_on_Abs_hcomplex: "inj_on Abs_hcomplex hcomplex"
    1.47  apply (rule inj_on_inverseI)
    1.48 @@ -170,216 +158,188 @@
    1.49  
    1.50  declare equiv_hcomplexrel [THEN eq_equiv_class_iff, simp]
    1.51  
    1.52 -declare hcomplexrel_iff [iff]
    1.53  
    1.54  lemma inj_Rep_hcomplex: "inj(Rep_hcomplex)"
    1.55  apply (rule inj_on_inverseI)
    1.56  apply (rule Rep_hcomplex_inverse)
    1.57  done
    1.58  
    1.59 -lemma lemma_hcomplexrel_refl: "x: hcomplexrel `` {x}"
    1.60 -apply (unfold hcomplexrel_def)
    1.61 -apply (safe)
    1.62 -apply auto
    1.63 -done
    1.64 -declare lemma_hcomplexrel_refl [simp]
    1.65 +lemma lemma_hcomplexrel_refl [simp]: "x: hcomplexrel `` {x}"
    1.66 +by (simp add: hcomplexrel_def)
    1.67  
    1.68 -lemma hcomplex_empty_not_mem: "{} \<notin> hcomplex"
    1.69 -apply (unfold hcomplex_def)
    1.70 +lemma hcomplex_empty_not_mem [simp]: "{} \<notin> hcomplex"
    1.71 +apply (simp add: hcomplex_def hcomplexrel_def)
    1.72  apply (auto elim!: quotientE)
    1.73  done
    1.74 -declare hcomplex_empty_not_mem [simp]
    1.75  
    1.76 -lemma Rep_hcomplex_nonempty: "Rep_hcomplex x \<noteq> {}"
    1.77 -apply (cut_tac x = "x" in Rep_hcomplex)
    1.78 -apply auto
    1.79 -done
    1.80 -declare Rep_hcomplex_nonempty [simp]
    1.81 +lemma Rep_hcomplex_nonempty [simp]: "Rep_hcomplex x \<noteq> {}"
    1.82 +by (cut_tac x = x in Rep_hcomplex, auto)
    1.83  
    1.84  lemma eq_Abs_hcomplex:
    1.85      "(!!x. z = Abs_hcomplex(hcomplexrel `` {x}) ==> P) ==> P"
    1.86  apply (rule_tac x1=z in Rep_hcomplex [unfolded hcomplex_def, THEN quotientE])
    1.87  apply (drule_tac f = Abs_hcomplex in arg_cong)
    1.88 -apply (force simp add: Rep_hcomplex_inverse)
    1.89 +apply (force simp add: Rep_hcomplex_inverse hcomplexrel_def)
    1.90  done
    1.91  
    1.92 +(*??delete*)
    1.93 +lemma hcomplexrel_iff [iff]:
    1.94 +   "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
    1.95 +by (simp add: hcomplexrel_def)
    1.96 +
    1.97  
    1.98  subsection{*Properties of Nonstandard Real and Imaginary Parts*}
    1.99  
   1.100  lemma hRe:
   1.101       "hRe(Abs_hcomplex (hcomplexrel `` {X})) =
   1.102        Abs_hypreal(hyprel `` {%n. Re(X n)})"
   1.103 -apply (unfold hRe_def)
   1.104 -apply (rule_tac f = "Abs_hypreal" in arg_cong)
   1.105 -apply (auto , ultra)
   1.106 +apply (simp add: hRe_def)
   1.107 +apply (rule_tac f = Abs_hypreal in arg_cong)
   1.108 +apply (auto, ultra)
   1.109  done
   1.110  
   1.111  lemma hIm:
   1.112       "hIm(Abs_hcomplex (hcomplexrel `` {X})) =
   1.113        Abs_hypreal(hyprel `` {%n. Im(X n)})"
   1.114 -apply (unfold hIm_def)
   1.115 -apply (rule_tac f = "Abs_hypreal" in arg_cong)
   1.116 -apply (auto , ultra)
   1.117 +apply (simp add: hIm_def)
   1.118 +apply (rule_tac f = Abs_hypreal in arg_cong)
   1.119 +apply (auto, ultra)
   1.120  done
   1.121  
   1.122  lemma hcomplex_hRe_hIm_cancel_iff:
   1.123       "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
   1.124 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.125 -apply (rule_tac z = "w" in eq_Abs_hcomplex)
   1.126 +apply (rule eq_Abs_hcomplex [of z])
   1.127 +apply (rule eq_Abs_hcomplex [of w])
   1.128  apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff)
   1.129  apply (ultra+)
   1.130  done
   1.131  
   1.132 -lemma hcomplex_hRe_zero: "hRe 0 = 0"
   1.133 -apply (unfold hcomplex_zero_def)
   1.134 -apply (simp (no_asm) add: hRe hypreal_zero_num)
   1.135 -done
   1.136 -declare hcomplex_hRe_zero [simp]
   1.137 +lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0"
   1.138 +by (simp add: hcomplex_zero_def hRe hypreal_zero_num)
   1.139  
   1.140 -lemma hcomplex_hIm_zero: "hIm 0 = 0"
   1.141 -apply (unfold hcomplex_zero_def)
   1.142 -apply (simp (no_asm) add: hIm hypreal_zero_num)
   1.143 -done
   1.144 -declare hcomplex_hIm_zero [simp]
   1.145 +lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0"
   1.146 +by (simp add: hcomplex_zero_def hIm hypreal_zero_num)
   1.147  
   1.148 -lemma hcomplex_hRe_one: "hRe 1 = 1"
   1.149 -apply (unfold hcomplex_one_def)
   1.150 -apply (simp (no_asm) add: hRe hypreal_one_num)
   1.151 -done
   1.152 -declare hcomplex_hRe_one [simp]
   1.153 +lemma hcomplex_hRe_one [simp]: "hRe 1 = 1"
   1.154 +by (simp add: hcomplex_one_def hRe hypreal_one_num)
   1.155  
   1.156 -lemma hcomplex_hIm_one: "hIm 1 = 0"
   1.157 -apply (unfold hcomplex_one_def)
   1.158 -apply (simp (no_asm) add: hIm hypreal_one_def hypreal_zero_num)
   1.159 -done
   1.160 -declare hcomplex_hIm_one [simp]
   1.161 +lemma hcomplex_hIm_one [simp]: "hIm 1 = 0"
   1.162 +by (simp add: hcomplex_one_def hIm hypreal_one_def hypreal_zero_num)
   1.163  
   1.164  
   1.165  subsection{*Addition for Nonstandard Complex Numbers*}
   1.166  
   1.167  lemma hcomplex_add_congruent2:
   1.168      "congruent2 hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})"
   1.169 -apply (unfold congruent2_def)
   1.170 -apply safe
   1.171 -apply (ultra+)
   1.172 -done
   1.173 +by (auto simp add: congruent2_def, ultra)
   1.174  
   1.175  lemma hcomplex_add:
   1.176    "Abs_hcomplex(hcomplexrel``{%n. X n}) + Abs_hcomplex(hcomplexrel``{%n. Y n}) =
   1.177     Abs_hcomplex(hcomplexrel``{%n. X n + Y n})"
   1.178 -apply (unfold hcomplex_add_def)
   1.179 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   1.180 +apply (simp add: hcomplex_add_def)
   1.181 +apply (rule_tac f = Abs_hcomplex in arg_cong)
   1.182  apply (auto, ultra)
   1.183  done
   1.184  
   1.185  lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z"
   1.186 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.187 -apply (rule_tac z = "w" in eq_Abs_hcomplex)
   1.188 +apply (rule eq_Abs_hcomplex [of z])
   1.189 +apply (rule eq_Abs_hcomplex [of w])
   1.190  apply (simp add: complex_add_commute hcomplex_add)
   1.191  done
   1.192  
   1.193  lemma hcomplex_add_assoc: "((z1::hcomplex) + z2) + z3 = z1 + (z2 + z3)"
   1.194 -apply (rule_tac z = "z1" in eq_Abs_hcomplex)
   1.195 -apply (rule_tac z = "z2" in eq_Abs_hcomplex)
   1.196 -apply (rule_tac z = "z3" in eq_Abs_hcomplex)
   1.197 +apply (rule eq_Abs_hcomplex [of z1])
   1.198 +apply (rule eq_Abs_hcomplex [of z2])
   1.199 +apply (rule eq_Abs_hcomplex [of z3])
   1.200  apply (simp add: hcomplex_add complex_add_assoc)
   1.201  done
   1.202  
   1.203  lemma hcomplex_add_zero_left: "(0::hcomplex) + z = z"
   1.204 -apply (unfold hcomplex_zero_def)
   1.205 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.206 -apply (simp add: hcomplex_add)
   1.207 +apply (rule eq_Abs_hcomplex [of z])
   1.208 +apply (simp add: hcomplex_zero_def hcomplex_add)
   1.209  done
   1.210  
   1.211  lemma hcomplex_add_zero_right: "z + (0::hcomplex) = z"
   1.212 -apply (simp add: hcomplex_add_zero_left hcomplex_add_commute)
   1.213 -done
   1.214 +by (simp add: hcomplex_add_zero_left hcomplex_add_commute)
   1.215  
   1.216  lemma hRe_add: "hRe(x + y) = hRe(x) + hRe(y)"
   1.217 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
   1.218 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
   1.219 -apply (auto simp add: hRe hcomplex_add hypreal_add complex_Re_add)
   1.220 +apply (rule eq_Abs_hcomplex [of x])
   1.221 +apply (rule eq_Abs_hcomplex [of y])
   1.222 +apply (simp add: hRe hcomplex_add hypreal_add complex_Re_add)
   1.223  done
   1.224  
   1.225  lemma hIm_add: "hIm(x + y) = hIm(x) + hIm(y)"
   1.226 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
   1.227 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
   1.228 -apply (auto simp add: hIm hcomplex_add hypreal_add complex_Im_add)
   1.229 +apply (rule eq_Abs_hcomplex [of x])
   1.230 +apply (rule eq_Abs_hcomplex [of y])
   1.231 +apply (simp add: hIm hcomplex_add hypreal_add complex_Im_add)
   1.232  done
   1.233  
   1.234  
   1.235  subsection{*Additive Inverse on Nonstandard Complex Numbers*}
   1.236  
   1.237  lemma hcomplex_minus_congruent:
   1.238 -  "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})"
   1.239 -apply (unfold congruent_def)
   1.240 -apply safe
   1.241 -apply (ultra+)
   1.242 -done
   1.243 +     "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})"
   1.244 +by (simp add: congruent_def)
   1.245  
   1.246  lemma hcomplex_minus:
   1.247    "- (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
   1.248        Abs_hcomplex(hcomplexrel `` {%n. -(X n)})"
   1.249 -apply (unfold hcomplex_minus_def)
   1.250 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   1.251 +apply (simp add: hcomplex_minus_def)
   1.252 +apply (rule_tac f = Abs_hcomplex in arg_cong)
   1.253  apply (auto, ultra)
   1.254  done
   1.255  
   1.256  lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)"
   1.257 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.258 -apply (auto simp add: hcomplex_add hcomplex_minus hcomplex_zero_def)
   1.259 +apply (rule eq_Abs_hcomplex [of z])
   1.260 +apply (simp add: hcomplex_add hcomplex_minus hcomplex_zero_def)
   1.261  done
   1.262  
   1.263  
   1.264  subsection{*Multiplication for Nonstandard Complex Numbers*}
   1.265  
   1.266  lemma hcomplex_mult:
   1.267 -  "Abs_hcomplex(hcomplexrel``{%n. X n}) * 
   1.268 +  "Abs_hcomplex(hcomplexrel``{%n. X n}) *
   1.269       Abs_hcomplex(hcomplexrel``{%n. Y n}) =
   1.270 -   Abs_hcomplex(hcomplexrel``{%n. X n * Y n})"
   1.271 -apply (unfold hcomplex_mult_def)
   1.272 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   1.273 +     Abs_hcomplex(hcomplexrel``{%n. X n * Y n})"
   1.274 +apply (simp add: hcomplex_mult_def)
   1.275 +apply (rule_tac f = Abs_hcomplex in arg_cong)
   1.276  apply (auto, ultra)
   1.277  done
   1.278  
   1.279  lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w"
   1.280 -apply (rule_tac z = "w" in eq_Abs_hcomplex)
   1.281 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.282 -apply (auto simp add: hcomplex_mult complex_mult_commute)
   1.283 +apply (rule eq_Abs_hcomplex [of w])
   1.284 +apply (rule eq_Abs_hcomplex [of z])
   1.285 +apply (simp add: hcomplex_mult complex_mult_commute)
   1.286  done
   1.287  
   1.288  lemma hcomplex_mult_assoc: "((u::hcomplex) * v) * w = u * (v * w)"
   1.289 -apply (rule_tac z = "u" in eq_Abs_hcomplex)
   1.290 -apply (rule_tac z = "v" in eq_Abs_hcomplex)
   1.291 -apply (rule_tac z = "w" in eq_Abs_hcomplex)
   1.292 -apply (auto simp add: hcomplex_mult complex_mult_assoc)
   1.293 +apply (rule eq_Abs_hcomplex [of u])
   1.294 +apply (rule eq_Abs_hcomplex [of v])
   1.295 +apply (rule eq_Abs_hcomplex [of w])
   1.296 +apply (simp add: hcomplex_mult complex_mult_assoc)
   1.297  done
   1.298  
   1.299  lemma hcomplex_mult_one_left: "(1::hcomplex) * z = z"
   1.300 -apply (unfold hcomplex_one_def)
   1.301 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.302 -apply (auto simp add: hcomplex_mult)
   1.303 +apply (rule eq_Abs_hcomplex [of z])
   1.304 +apply (simp add: hcomplex_one_def hcomplex_mult)
   1.305  done
   1.306  
   1.307  lemma hcomplex_mult_zero_left: "(0::hcomplex) * z = 0"
   1.308 -apply (unfold hcomplex_zero_def)
   1.309 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.310 -apply (auto simp add: hcomplex_mult)
   1.311 +apply (rule eq_Abs_hcomplex [of z])
   1.312 +apply (simp add: hcomplex_zero_def hcomplex_mult)
   1.313  done
   1.314  
   1.315  lemma hcomplex_add_mult_distrib:
   1.316       "((z1::hcomplex) + z2) * w = (z1 * w) + (z2 * w)"
   1.317 -apply (rule_tac z = "z1" in eq_Abs_hcomplex)
   1.318 -apply (rule_tac z = "z2" in eq_Abs_hcomplex)
   1.319 -apply (rule_tac z = "w" in eq_Abs_hcomplex)
   1.320 -apply (auto simp add: hcomplex_mult hcomplex_add left_distrib)
   1.321 +apply (rule eq_Abs_hcomplex [of z1])
   1.322 +apply (rule eq_Abs_hcomplex [of z2])
   1.323 +apply (rule eq_Abs_hcomplex [of w])
   1.324 +apply (simp add: hcomplex_mult hcomplex_add left_distrib)
   1.325  done
   1.326  
   1.327  lemma hcomplex_zero_not_eq_one: "(0::hcomplex) \<noteq> (1::hcomplex)"
   1.328 -apply (unfold hcomplex_zero_def hcomplex_one_def)
   1.329 -apply auto
   1.330 -done
   1.331 -declare hcomplex_zero_not_eq_one [simp]
   1.332 +by (simp add: hcomplex_zero_def hcomplex_one_def)
   1.333 +
   1.334  declare hcomplex_zero_not_eq_one [THEN not_sym, simp]
   1.335  
   1.336  
   1.337 @@ -388,20 +348,17 @@
   1.338  lemma hcomplex_inverse:
   1.339    "inverse (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
   1.340        Abs_hcomplex(hcomplexrel `` {%n. inverse (X n)})"
   1.341 -apply (unfold hcinv_def)
   1.342 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   1.343 +apply (simp add: hcinv_def)
   1.344 +apply (rule_tac f = Abs_hcomplex in arg_cong)
   1.345  apply (auto, ultra)
   1.346  done
   1.347  
   1.348  lemma hcomplex_mult_inv_left:
   1.349        "z \<noteq> (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)"
   1.350 -apply (unfold hcomplex_zero_def hcomplex_one_def)
   1.351 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.352 -apply (auto simp add: hcomplex_inverse hcomplex_mult)
   1.353 -apply (ultra)
   1.354 +apply (rule eq_Abs_hcomplex [of z])
   1.355 +apply (simp add: hcomplex_zero_def hcomplex_one_def hcomplex_inverse hcomplex_mult, ultra)
   1.356  apply (rule ccontr)
   1.357 -apply (drule left_inverse)
   1.358 -apply auto
   1.359 +apply (drule left_inverse, auto)
   1.360  done
   1.361  
   1.362  subsection {* The Field of Nonstandard Complex Numbers *}
   1.363 @@ -431,9 +388,9 @@
   1.364      by (simp add: hcomplex_add_mult_distrib)
   1.365    show "z+u = z+v ==> u=v"
   1.366      proof -
   1.367 -      assume eq: "z+u = z+v" 
   1.368 +      assume eq: "z+u = z+v"
   1.369        hence "(-z + z) + u = (-z + z) + v" by (simp only: eq hcomplex_add_assoc)
   1.370 -      thus "u = v" 
   1.371 +      thus "u = v"
   1.372          by (simp only: hcomplex_add_minus_left hcomplex_add_zero_left)
   1.373      qed
   1.374    assume neq: "w \<noteq> 0"
   1.375 @@ -443,71 +400,53 @@
   1.376      by (rule hcomplex_mult_inv_left)
   1.377  qed
   1.378  
   1.379 -lemma HCOMPLEX_INVERSE_ZERO: "inverse (0::hcomplex) = 0"
   1.380 -apply (simp add:  hcomplex_zero_def hcomplex_inverse)
   1.381 -done
   1.382 -
   1.383 -lemma HCOMPLEX_DIVISION_BY_ZERO: "a / (0::hcomplex) = 0"
   1.384 -apply (simp add: hcomplex_divide_def HCOMPLEX_INVERSE_ZERO)
   1.385 -done
   1.386 -
   1.387  instance hcomplex :: division_by_zero
   1.388  proof
   1.389 +  show inv: "inverse 0 = (0::hcomplex)"
   1.390 +    by (simp add: hcomplex_inverse hcomplex_zero_def)
   1.391    fix x :: hcomplex
   1.392 -  show "inverse 0 = (0::hcomplex)" by (rule HCOMPLEX_INVERSE_ZERO)
   1.393 -  show "x/0 = 0" by (rule HCOMPLEX_DIVISION_BY_ZERO) 
   1.394 +  show "x/0 = 0"
   1.395 +    by (simp add: hcomplex_divide_def inv)
   1.396  qed
   1.397  
   1.398 +
   1.399  subsection{*More Minus Laws*}
   1.400  
   1.401 -lemma inj_hcomplex_minus: "inj(%z::hcomplex. -z)"
   1.402 -apply (rule inj_onI)
   1.403 -apply (drule_tac f = "uminus" in arg_cong)
   1.404 -apply simp
   1.405 -done
   1.406 -
   1.407  lemma hRe_minus: "hRe(-z) = - hRe(z)"
   1.408 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.409 -apply (auto simp add: hRe hcomplex_minus hypreal_minus complex_Re_minus)
   1.410 +apply (rule eq_Abs_hcomplex [of z])
   1.411 +apply (simp add: hRe hcomplex_minus hypreal_minus complex_Re_minus)
   1.412  done
   1.413  
   1.414  lemma hIm_minus: "hIm(-z) = - hIm(z)"
   1.415 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.416 -apply (auto simp add: hIm hcomplex_minus hypreal_minus complex_Im_minus)
   1.417 +apply (rule eq_Abs_hcomplex [of z])
   1.418 +apply (simp add: hIm hcomplex_minus hypreal_minus complex_Im_minus)
   1.419  done
   1.420  
   1.421  lemma hcomplex_add_minus_eq_minus:
   1.422        "x + y = (0::hcomplex) ==> x = -y"
   1.423 -apply (drule Ring_and_Field.equals_zero_I) 
   1.424 -apply (simp add: minus_equation_iff [of x y]) 
   1.425 +apply (drule Ring_and_Field.equals_zero_I)
   1.426 +apply (simp add: minus_equation_iff [of x y])
   1.427  done
   1.428  
   1.429  
   1.430  subsection{*More Multiplication Laws*}
   1.431  
   1.432  lemma hcomplex_mult_one_right: "z * (1::hcomplex) = z"
   1.433 -apply (rule Ring_and_Field.mult_1_right)
   1.434 -done
   1.435 +by (rule Ring_and_Field.mult_1_right)
   1.436  
   1.437 -lemma hcomplex_mult_minus_one: "- 1 * (z::hcomplex) = -z"
   1.438 -apply (simp (no_asm))
   1.439 -done
   1.440 -declare hcomplex_mult_minus_one [simp]
   1.441 +lemma hcomplex_mult_minus_one [simp]: "- 1 * (z::hcomplex) = -z"
   1.442 +by simp
   1.443  
   1.444 -lemma hcomplex_mult_minus_one_right: "(z::hcomplex) * - 1 = -z"
   1.445 -apply (subst hcomplex_mult_commute)
   1.446 -apply (simp (no_asm))
   1.447 -done
   1.448 -declare hcomplex_mult_minus_one_right [simp]
   1.449 +lemma hcomplex_mult_minus_one_right [simp]: "(z::hcomplex) * - 1 = -z"
   1.450 +by (subst hcomplex_mult_commute, simp)
   1.451  
   1.452  lemma hcomplex_mult_left_cancel:
   1.453       "(c::hcomplex) \<noteq> (0::hcomplex) ==> (c*a=c*b) = (a=b)"
   1.454 -by (simp add: field_mult_cancel_left) 
   1.455 +by (simp add: field_mult_cancel_left)
   1.456  
   1.457  lemma hcomplex_mult_right_cancel:
   1.458       "(c::hcomplex) \<noteq> (0::hcomplex) ==> (a*c=b*c) = (a=b)"
   1.459 -apply (simp add: Ring_and_Field.field_mult_cancel_right); 
   1.460 -done
   1.461 +by (simp add: Ring_and_Field.field_mult_cancel_right)
   1.462  
   1.463  
   1.464  subsection{*Subraction and Division*}
   1.465 @@ -515,17 +454,13 @@
   1.466  lemma hcomplex_diff:
   1.467   "Abs_hcomplex(hcomplexrel``{%n. X n}) - Abs_hcomplex(hcomplexrel``{%n. Y n}) =
   1.468    Abs_hcomplex(hcomplexrel``{%n. X n - Y n})"
   1.469 -apply (unfold hcomplex_diff_def)
   1.470 -apply (auto simp add: hcomplex_minus hcomplex_add complex_diff_def)
   1.471 -done
   1.472 +by (simp add: hcomplex_diff_def hcomplex_minus hcomplex_add complex_diff_def)
   1.473  
   1.474 -lemma hcomplex_diff_eq_eq: "((x::hcomplex) - y = z) = (x = z + y)"
   1.475 -apply (rule Ring_and_Field.diff_eq_eq) 
   1.476 -done
   1.477 +lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)"
   1.478 +by (rule Ring_and_Field.diff_eq_eq)
   1.479  
   1.480  lemma hcomplex_add_divide_distrib: "(x+y)/(z::hcomplex) = x/z + y/z"
   1.481 -apply (rule Ring_and_Field.add_divide_distrib) 
   1.482 -done
   1.483 +by (rule Ring_and_Field.add_divide_distrib)
   1.484  
   1.485  
   1.486  subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*}
   1.487 @@ -533,98 +468,77 @@
   1.488  lemma hcomplex_of_hypreal:
   1.489    "hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) =
   1.490        Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})"
   1.491 -apply (unfold hcomplex_of_hypreal_def)
   1.492 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   1.493 -apply auto
   1.494 -apply (ultra)
   1.495 +apply (simp add: hcomplex_of_hypreal_def)
   1.496 +apply (rule_tac f = Abs_hcomplex in arg_cong, auto, ultra)
   1.497  done
   1.498  
   1.499 -lemma inj_hcomplex_of_hypreal: "inj hcomplex_of_hypreal"
   1.500 -apply (rule inj_onI)
   1.501 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   1.502 -apply (rule_tac z = "y" in eq_Abs_hypreal)
   1.503 -apply (auto simp add: hcomplex_of_hypreal)
   1.504 +lemma hcomplex_of_hypreal_cancel_iff [iff]:
   1.505 +     "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
   1.506 +apply (rule eq_Abs_hypreal [of x])
   1.507 +apply (rule eq_Abs_hypreal [of y])
   1.508 +apply (simp add: hcomplex_of_hypreal)
   1.509  done
   1.510  
   1.511 -lemma hcomplex_of_hypreal_cancel_iff:
   1.512 -     "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
   1.513 -apply (auto dest: inj_hcomplex_of_hypreal [THEN injD])
   1.514 -done
   1.515 -declare hcomplex_of_hypreal_cancel_iff [iff]
   1.516 -
   1.517  lemma hcomplex_of_hypreal_minus:
   1.518       "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
   1.519 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   1.520 -apply (auto simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus)
   1.521 +apply (rule eq_Abs_hypreal [of x])
   1.522 +apply (simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus)
   1.523  done
   1.524  
   1.525  lemma hcomplex_of_hypreal_inverse:
   1.526       "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
   1.527 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   1.528 -apply (auto simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse)
   1.529 +apply (rule eq_Abs_hypreal [of x])
   1.530 +apply (simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse)
   1.531  done
   1.532  
   1.533  lemma hcomplex_of_hypreal_add:
   1.534       "hcomplex_of_hypreal x + hcomplex_of_hypreal y =
   1.535        hcomplex_of_hypreal (x + y)"
   1.536 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   1.537 -apply (rule_tac z = "y" in eq_Abs_hypreal)
   1.538 -apply (auto simp add: hcomplex_of_hypreal hypreal_add hcomplex_add complex_of_real_add)
   1.539 +apply (rule eq_Abs_hypreal [of x])
   1.540 +apply (rule eq_Abs_hypreal [of y])
   1.541 +apply (simp add: hcomplex_of_hypreal hypreal_add hcomplex_add complex_of_real_add)
   1.542  done
   1.543  
   1.544  lemma hcomplex_of_hypreal_diff:
   1.545       "hcomplex_of_hypreal x - hcomplex_of_hypreal y =
   1.546        hcomplex_of_hypreal (x - y)"
   1.547 -apply (unfold hcomplex_diff_def)
   1.548 -apply (auto simp add: hcomplex_of_hypreal_minus [symmetric] hcomplex_of_hypreal_add hypreal_diff_def)
   1.549 -done
   1.550 +by (simp add: hcomplex_diff_def hcomplex_of_hypreal_minus [symmetric] hcomplex_of_hypreal_add hypreal_diff_def)
   1.551  
   1.552  lemma hcomplex_of_hypreal_mult:
   1.553       "hcomplex_of_hypreal x * hcomplex_of_hypreal y =
   1.554        hcomplex_of_hypreal (x * y)"
   1.555 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   1.556 -apply (rule_tac z = "y" in eq_Abs_hypreal)
   1.557 -apply (auto simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult 
   1.558 -                      complex_of_real_mult)
   1.559 +apply (rule eq_Abs_hypreal [of x])
   1.560 +apply (rule eq_Abs_hypreal [of y])
   1.561 +apply (simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult complex_of_real_mult)
   1.562  done
   1.563  
   1.564  lemma hcomplex_of_hypreal_divide:
   1.565    "hcomplex_of_hypreal x / hcomplex_of_hypreal y = hcomplex_of_hypreal(x/y)"
   1.566 -apply (unfold hcomplex_divide_def)
   1.567 -apply (case_tac "y=0")
   1.568 -apply (simp)
   1.569 +apply (simp add: hcomplex_divide_def)
   1.570 +apply (case_tac "y=0", simp)
   1.571  apply (auto simp add: hcomplex_of_hypreal_mult hcomplex_of_hypreal_inverse [symmetric])
   1.572 -apply (simp (no_asm) add: hypreal_divide_def)
   1.573 -done
   1.574 -
   1.575 -lemma hcomplex_of_hypreal_one [simp]:
   1.576 -      "hcomplex_of_hypreal 1 = 1"
   1.577 -apply (unfold hcomplex_one_def)
   1.578 -apply (auto simp add: hcomplex_of_hypreal hypreal_one_num)
   1.579 +apply (simp add: hypreal_divide_def)
   1.580  done
   1.581  
   1.582 -lemma hcomplex_of_hypreal_zero [simp]:
   1.583 -      "hcomplex_of_hypreal 0 = 0"
   1.584 -apply (unfold hcomplex_zero_def hypreal_zero_def)
   1.585 -apply (auto simp add: hcomplex_of_hypreal)
   1.586 -done
   1.587 +lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1"
   1.588 +by (simp add: hcomplex_one_def hcomplex_of_hypreal hypreal_one_num)
   1.589  
   1.590 -lemma hRe_hcomplex_of_hypreal: "hRe(hcomplex_of_hypreal z) = z"
   1.591 -apply (rule_tac z = "z" in eq_Abs_hypreal)
   1.592 +lemma hcomplex_of_hypreal_zero [simp]: "hcomplex_of_hypreal 0 = 0"
   1.593 +by (simp add: hcomplex_zero_def hypreal_zero_def hcomplex_of_hypreal)
   1.594 +
   1.595 +lemma hRe_hcomplex_of_hypreal [simp]: "hRe(hcomplex_of_hypreal z) = z"
   1.596 +apply (rule eq_Abs_hypreal [of z])
   1.597  apply (auto simp add: hcomplex_of_hypreal hRe)
   1.598  done
   1.599 -declare hRe_hcomplex_of_hypreal [simp]
   1.600  
   1.601 -lemma hIm_hcomplex_of_hypreal: "hIm(hcomplex_of_hypreal z) = 0"
   1.602 -apply (rule_tac z = "z" in eq_Abs_hypreal)
   1.603 +lemma hIm_hcomplex_of_hypreal [simp]: "hIm(hcomplex_of_hypreal z) = 0"
   1.604 +apply (rule eq_Abs_hypreal [of z])
   1.605  apply (auto simp add: hcomplex_of_hypreal hIm hypreal_zero_num)
   1.606  done
   1.607 -declare hIm_hcomplex_of_hypreal [simp]
   1.608  
   1.609 -lemma hcomplex_of_hypreal_epsilon_not_zero: "hcomplex_of_hypreal epsilon \<noteq> 0"
   1.610 -apply (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def)
   1.611 -done
   1.612 -declare hcomplex_of_hypreal_epsilon_not_zero [simp]
   1.613 +lemma hcomplex_of_hypreal_epsilon_not_zero [simp]:
   1.614 +     "hcomplex_of_hypreal epsilon \<noteq> 0"
   1.615 +by (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def)
   1.616  
   1.617  
   1.618  subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*}
   1.619 @@ -633,35 +547,27 @@
   1.620    "hcmod (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
   1.621        Abs_hypreal(hyprel `` {%n. cmod (X n)})"
   1.622  
   1.623 -apply (unfold hcmod_def)
   1.624 -apply (rule_tac f = "Abs_hypreal" in arg_cong)
   1.625 +apply (simp add: hcmod_def)
   1.626 +apply (rule_tac f = Abs_hypreal in arg_cong)
   1.627  apply (auto, ultra)
   1.628  done
   1.629  
   1.630 -lemma hcmod_zero [simp]:
   1.631 -      "hcmod(0) = 0"
   1.632 -apply (unfold hcomplex_zero_def hypreal_zero_def)
   1.633 -apply (auto simp add: hcmod)
   1.634 +lemma hcmod_zero [simp]: "hcmod(0) = 0"
   1.635 +apply (simp add: hcomplex_zero_def hypreal_zero_def hcmod)
   1.636  done
   1.637  
   1.638 -lemma hcmod_one:
   1.639 -      "hcmod(1) = 1"
   1.640 -apply (unfold hcomplex_one_def)
   1.641 -apply (auto simp add: hcmod hypreal_one_num)
   1.642 -done
   1.643 -declare hcmod_one [simp]
   1.644 +lemma hcmod_one [simp]: "hcmod(1) = 1"
   1.645 +by (simp add: hcomplex_one_def hcmod hypreal_one_num)
   1.646  
   1.647 -lemma hcmod_hcomplex_of_hypreal: "hcmod(hcomplex_of_hypreal x) = abs x"
   1.648 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   1.649 +lemma hcmod_hcomplex_of_hypreal [simp]: "hcmod(hcomplex_of_hypreal x) = abs x"
   1.650 +apply (rule eq_Abs_hypreal [of x])
   1.651  apply (auto simp add: hcmod hcomplex_of_hypreal hypreal_hrabs)
   1.652  done
   1.653 -declare hcmod_hcomplex_of_hypreal [simp]
   1.654  
   1.655  lemma hcomplex_of_hypreal_abs:
   1.656       "hcomplex_of_hypreal (abs x) =
   1.657        hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))"
   1.658 -apply (simp (no_asm))
   1.659 -done
   1.660 +by simp
   1.661  
   1.662  
   1.663  subsection{*Conjugation*}
   1.664 @@ -669,232 +575,198 @@
   1.665  lemma hcnj:
   1.666    "hcnj (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
   1.667     Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})"
   1.668 -apply (unfold hcnj_def)
   1.669 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   1.670 +apply (simp add: hcnj_def)
   1.671 +apply (rule_tac f = Abs_hcomplex in arg_cong)
   1.672  apply (auto, ultra)
   1.673  done
   1.674  
   1.675 -lemma inj_hcnj: "inj hcnj"
   1.676 -apply (rule inj_onI)
   1.677 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
   1.678 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
   1.679 -apply (auto simp add: hcnj)
   1.680 +lemma hcomplex_hcnj_cancel_iff [iff]: "(hcnj x = hcnj y) = (x = y)"
   1.681 +apply (rule eq_Abs_hcomplex [of x])
   1.682 +apply (rule eq_Abs_hcomplex [of y])
   1.683 +apply (simp add: hcnj)
   1.684 +done
   1.685 +
   1.686 +lemma hcomplex_hcnj_hcnj [simp]: "hcnj (hcnj z) = z"
   1.687 +apply (rule eq_Abs_hcomplex [of z])
   1.688 +apply (simp add: hcnj)
   1.689  done
   1.690  
   1.691 -lemma hcomplex_hcnj_cancel_iff: "(hcnj x = hcnj y) = (x = y)"
   1.692 -apply (auto dest: inj_hcnj [THEN injD])
   1.693 +lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]:
   1.694 +     "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
   1.695 +apply (rule eq_Abs_hypreal [of x])
   1.696 +apply (simp add: hcnj hcomplex_of_hypreal)
   1.697  done
   1.698 -declare hcomplex_hcnj_cancel_iff [simp]
   1.699 -
   1.700 -lemma hcomplex_hcnj_hcnj: "hcnj (hcnj z) = z"
   1.701 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.702 -apply (auto simp add: hcnj)
   1.703 -done
   1.704 -declare hcomplex_hcnj_hcnj [simp]
   1.705  
   1.706 -lemma hcomplex_hcnj_hcomplex_of_hypreal:
   1.707 -     "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
   1.708 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   1.709 -apply (auto simp add: hcnj hcomplex_of_hypreal)
   1.710 +lemma hcomplex_hmod_hcnj [simp]: "hcmod (hcnj z) = hcmod z"
   1.711 +apply (rule eq_Abs_hcomplex [of z])
   1.712 +apply (simp add: hcnj hcmod)
   1.713  done
   1.714 -declare hcomplex_hcnj_hcomplex_of_hypreal [simp]
   1.715 -
   1.716 -lemma hcomplex_hmod_hcnj: "hcmod (hcnj z) = hcmod z"
   1.717 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.718 -apply (auto simp add: hcnj hcmod)
   1.719 -done
   1.720 -declare hcomplex_hmod_hcnj [simp]
   1.721  
   1.722  lemma hcomplex_hcnj_minus: "hcnj (-z) = - hcnj z"
   1.723 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.724 -apply (auto simp add: hcnj hcomplex_minus complex_cnj_minus)
   1.725 +apply (rule eq_Abs_hcomplex [of z])
   1.726 +apply (simp add: hcnj hcomplex_minus complex_cnj_minus)
   1.727  done
   1.728  
   1.729  lemma hcomplex_hcnj_inverse: "hcnj(inverse z) = inverse(hcnj z)"
   1.730 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.731 -apply (auto simp add: hcnj hcomplex_inverse complex_cnj_inverse)
   1.732 +apply (rule eq_Abs_hcomplex [of z])
   1.733 +apply (simp add: hcnj hcomplex_inverse complex_cnj_inverse)
   1.734  done
   1.735  
   1.736  lemma hcomplex_hcnj_add: "hcnj(w + z) = hcnj(w) + hcnj(z)"
   1.737 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.738 -apply (rule_tac z = "w" in eq_Abs_hcomplex)
   1.739 -apply (auto simp add: hcnj hcomplex_add complex_cnj_add)
   1.740 +apply (rule eq_Abs_hcomplex [of z])
   1.741 +apply (rule eq_Abs_hcomplex [of w])
   1.742 +apply (simp add: hcnj hcomplex_add complex_cnj_add)
   1.743  done
   1.744  
   1.745  lemma hcomplex_hcnj_diff: "hcnj(w - z) = hcnj(w) - hcnj(z)"
   1.746 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.747 -apply (rule_tac z = "w" in eq_Abs_hcomplex)
   1.748 -apply (auto simp add: hcnj hcomplex_diff complex_cnj_diff)
   1.749 +apply (rule eq_Abs_hcomplex [of z])
   1.750 +apply (rule eq_Abs_hcomplex [of w])
   1.751 +apply (simp add: hcnj hcomplex_diff complex_cnj_diff)
   1.752  done
   1.753  
   1.754  lemma hcomplex_hcnj_mult: "hcnj(w * z) = hcnj(w) * hcnj(z)"
   1.755 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.756 -apply (rule_tac z = "w" in eq_Abs_hcomplex)
   1.757 -apply (auto simp add: hcnj hcomplex_mult complex_cnj_mult)
   1.758 +apply (rule eq_Abs_hcomplex [of z])
   1.759 +apply (rule eq_Abs_hcomplex [of w])
   1.760 +apply (simp add: hcnj hcomplex_mult complex_cnj_mult)
   1.761  done
   1.762  
   1.763  lemma hcomplex_hcnj_divide: "hcnj(w / z) = (hcnj w)/(hcnj z)"
   1.764 -apply (unfold hcomplex_divide_def)
   1.765 -apply (simp (no_asm) add: hcomplex_hcnj_mult hcomplex_hcnj_inverse)
   1.766 -done
   1.767 +by (simp add: hcomplex_divide_def hcomplex_hcnj_mult hcomplex_hcnj_inverse)
   1.768  
   1.769 -lemma hcnj_one: "hcnj 1 = 1"
   1.770 -apply (unfold hcomplex_one_def)
   1.771 -apply (simp (no_asm) add: hcnj)
   1.772 -done
   1.773 -declare hcnj_one [simp]
   1.774 +lemma hcnj_one [simp]: "hcnj 1 = 1"
   1.775 +by (simp add: hcomplex_one_def hcnj)
   1.776  
   1.777 -lemma hcomplex_hcnj_zero:
   1.778 -      "hcnj 0 = 0"
   1.779 -apply (unfold hcomplex_zero_def)
   1.780 -apply (auto simp add: hcnj)
   1.781 +lemma hcomplex_hcnj_zero [simp]: "hcnj 0 = 0"
   1.782 +by (simp add: hcomplex_zero_def hcnj)
   1.783 +
   1.784 +lemma hcomplex_hcnj_zero_iff [iff]: "(hcnj z = 0) = (z = 0)"
   1.785 +apply (rule eq_Abs_hcomplex [of z])
   1.786 +apply (simp add: hcomplex_zero_def hcnj)
   1.787  done
   1.788 -declare hcomplex_hcnj_zero [simp]
   1.789 -
   1.790 -lemma hcomplex_hcnj_zero_iff: "(hcnj z = 0) = (z = 0)"
   1.791 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.792 -apply (auto simp add: hcomplex_zero_def hcnj)
   1.793 -done
   1.794 -declare hcomplex_hcnj_zero_iff [iff]
   1.795  
   1.796  lemma hcomplex_mult_hcnj:
   1.797       "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
   1.798 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.799 -apply (auto simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add hypreal_mult complex_mult_cnj numeral_2_eq_2)
   1.800 +apply (rule eq_Abs_hcomplex [of z])
   1.801 +apply (simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add
   1.802 +                      hypreal_mult complex_mult_cnj numeral_2_eq_2)
   1.803  done
   1.804  
   1.805  
   1.806  subsection{*More Theorems about the Function @{term hcmod}*}
   1.807  
   1.808 -lemma hcomplex_hcmod_eq_zero_cancel: "(hcmod x = 0) = (x = 0)"
   1.809 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
   1.810 -apply (auto simp add: hcmod hcomplex_zero_def hypreal_zero_num)
   1.811 +lemma hcomplex_hcmod_eq_zero_cancel [simp]: "(hcmod x = 0) = (x = 0)"
   1.812 +apply (rule eq_Abs_hcomplex [of x])
   1.813 +apply (simp add: hcmod hcomplex_zero_def hypreal_zero_num)
   1.814  done
   1.815 -declare hcomplex_hcmod_eq_zero_cancel [simp]
   1.816  
   1.817 -lemma hcmod_hcomplex_of_hypreal_of_nat:
   1.818 +lemma hcmod_hcomplex_of_hypreal_of_nat [simp]:
   1.819       "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
   1.820 -apply (simp add: abs_if linorder_not_less) 
   1.821 +apply (simp add: abs_if linorder_not_less)
   1.822  done
   1.823 -declare hcmod_hcomplex_of_hypreal_of_nat [simp]
   1.824  
   1.825 -lemma hcmod_hcomplex_of_hypreal_of_hypnat:
   1.826 +lemma hcmod_hcomplex_of_hypreal_of_hypnat [simp]:
   1.827       "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"
   1.828 -apply (simp add: abs_if linorder_not_less) 
   1.829 +apply (simp add: abs_if linorder_not_less)
   1.830  done
   1.831 -declare hcmod_hcomplex_of_hypreal_of_hypnat [simp]
   1.832  
   1.833 -lemma hcmod_minus: "hcmod (-x) = hcmod(x)"
   1.834 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
   1.835 -apply (auto simp add: hcmod hcomplex_minus)
   1.836 +lemma hcmod_minus [simp]: "hcmod (-x) = hcmod(x)"
   1.837 +apply (rule eq_Abs_hcomplex [of x])
   1.838 +apply (simp add: hcmod hcomplex_minus)
   1.839  done
   1.840 -declare hcmod_minus [simp]
   1.841  
   1.842  lemma hcmod_mult_hcnj: "hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
   1.843 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
   1.844 -apply (auto simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj numeral_2_eq_2)
   1.845 +apply (rule eq_Abs_hcomplex [of z])
   1.846 +apply (simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj numeral_2_eq_2)
   1.847  done
   1.848  
   1.849 -lemma hcmod_ge_zero: "(0::hypreal) \<le> hcmod x"
   1.850 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
   1.851 -apply (auto simp add: hcmod hypreal_zero_num hypreal_le)
   1.852 +lemma hcmod_ge_zero [simp]: "(0::hypreal) \<le> hcmod x"
   1.853 +apply (rule eq_Abs_hcomplex [of x])
   1.854 +apply (simp add: hcmod hypreal_zero_num hypreal_le)
   1.855  done
   1.856 -declare hcmod_ge_zero [simp]
   1.857  
   1.858 -lemma hrabs_hcmod_cancel: "abs(hcmod x) = hcmod x" 
   1.859 -apply (simp add: abs_if linorder_not_less) 
   1.860 -done
   1.861 -declare hrabs_hcmod_cancel [simp]
   1.862 +lemma hrabs_hcmod_cancel [simp]: "abs(hcmod x) = hcmod x"
   1.863 +by (simp add: abs_if linorder_not_less)
   1.864  
   1.865  lemma hcmod_mult: "hcmod(x*y) = hcmod(x) * hcmod(y)"
   1.866 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
   1.867 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
   1.868 -apply (auto simp add: hcmod hcomplex_mult hypreal_mult complex_mod_mult)
   1.869 +apply (rule eq_Abs_hcomplex [of x])
   1.870 +apply (rule eq_Abs_hcomplex [of y])
   1.871 +apply (simp add: hcmod hcomplex_mult hypreal_mult complex_mod_mult)
   1.872  done
   1.873  
   1.874  lemma hcmod_add_squared_eq:
   1.875       "hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)"
   1.876 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
   1.877 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
   1.878 -apply (auto simp add: hcmod hcomplex_add hypreal_mult hRe hcnj hcomplex_mult
   1.879 -                      numeral_2_eq_2 realpow_two [symmetric] 
   1.880 -                 simp del: realpow_Suc)
   1.881 -apply (auto simp add: numeral_2_eq_2 [symmetric] complex_mod_add_squared_eq
   1.882 -                 hypreal_add [symmetric] hypreal_mult [symmetric] 
   1.883 +apply (rule eq_Abs_hcomplex [of x])
   1.884 +apply (rule eq_Abs_hcomplex [of y])
   1.885 +apply (simp add: hcmod hcomplex_add hypreal_mult hRe hcnj hcomplex_mult
   1.886 +                      numeral_2_eq_2 realpow_two [symmetric]
   1.887 +                  del: realpow_Suc)
   1.888 +apply (simp add: numeral_2_eq_2 [symmetric] complex_mod_add_squared_eq
   1.889 +                 hypreal_add [symmetric] hypreal_mult [symmetric]
   1.890                   hypreal_of_real_def [symmetric])
   1.891  done
   1.892  
   1.893 -lemma hcomplex_hRe_mult_hcnj_le_hcmod: "hRe(x * hcnj y) \<le> hcmod(x * hcnj y)"
   1.894 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
   1.895 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
   1.896 -apply (auto simp add: hcmod hcnj hcomplex_mult hRe hypreal_le)
   1.897 +lemma hcomplex_hRe_mult_hcnj_le_hcmod [simp]: "hRe(x * hcnj y) \<le> hcmod(x * hcnj y)"
   1.898 +apply (rule eq_Abs_hcomplex [of x])
   1.899 +apply (rule eq_Abs_hcomplex [of y])
   1.900 +apply (simp add: hcmod hcnj hcomplex_mult hRe hypreal_le)
   1.901  done
   1.902 -declare hcomplex_hRe_mult_hcnj_le_hcmod [simp]
   1.903  
   1.904 -lemma hcomplex_hRe_mult_hcnj_le_hcmod2: "hRe(x * hcnj y) \<le> hcmod(x * y)"
   1.905 -apply (cut_tac x = "x" and y = "y" in hcomplex_hRe_mult_hcnj_le_hcmod)
   1.906 +lemma hcomplex_hRe_mult_hcnj_le_hcmod2 [simp]: "hRe(x * hcnj y) \<le> hcmod(x * y)"
   1.907 +apply (cut_tac x = x and y = y in hcomplex_hRe_mult_hcnj_le_hcmod)
   1.908  apply (simp add: hcmod_mult)
   1.909  done
   1.910 -declare hcomplex_hRe_mult_hcnj_le_hcmod2 [simp]
   1.911  
   1.912 -lemma hcmod_triangle_squared: "hcmod (x + y) ^ 2 \<le> (hcmod(x) + hcmod(y)) ^ 2"
   1.913 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
   1.914 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
   1.915 -apply (auto simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add
   1.916 +lemma hcmod_triangle_squared [simp]: "hcmod (x + y) ^ 2 \<le> (hcmod(x) + hcmod(y)) ^ 2"
   1.917 +apply (rule eq_Abs_hcomplex [of x])
   1.918 +apply (rule eq_Abs_hcomplex [of y])
   1.919 +apply (simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add
   1.920                        hypreal_le realpow_two [symmetric] numeral_2_eq_2
   1.921 -            simp del: realpow_Suc)
   1.922 -apply (simp (no_asm) add: numeral_2_eq_2 [symmetric])
   1.923 +            del: realpow_Suc)
   1.924 +apply (simp add: numeral_2_eq_2 [symmetric])
   1.925  done
   1.926 -declare hcmod_triangle_squared [simp]
   1.927  
   1.928 -lemma hcmod_triangle_ineq: "hcmod (x + y) \<le> hcmod(x) + hcmod(y)"
   1.929 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
   1.930 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
   1.931 -apply (auto simp add: hcmod hcomplex_add hypreal_add hypreal_le)
   1.932 +lemma hcmod_triangle_ineq [simp]: "hcmod (x + y) \<le> hcmod(x) + hcmod(y)"
   1.933 +apply (rule eq_Abs_hcomplex [of x])
   1.934 +apply (rule eq_Abs_hcomplex [of y])
   1.935 +apply (simp add: hcmod hcomplex_add hypreal_add hypreal_le)
   1.936  done
   1.937 -declare hcmod_triangle_ineq [simp]
   1.938  
   1.939 -lemma hcmod_triangle_ineq2: "hcmod(b + a) - hcmod b \<le> hcmod a"
   1.940 -apply (cut_tac x1 = "b" and y1 = "a" and c = "-hcmod b" in hcmod_triangle_ineq [THEN add_right_mono])
   1.941 +lemma hcmod_triangle_ineq2 [simp]: "hcmod(b + a) - hcmod b \<le> hcmod a"
   1.942 +apply (cut_tac x1 = b and y1 = a and c = "-hcmod b" in hcmod_triangle_ineq [THEN add_right_mono])
   1.943  apply (simp add: add_ac)
   1.944  done
   1.945 -declare hcmod_triangle_ineq2 [simp]
   1.946  
   1.947  lemma hcmod_diff_commute: "hcmod (x - y) = hcmod (y - x)"
   1.948 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
   1.949 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
   1.950 -apply (auto simp add: hcmod hcomplex_diff complex_mod_diff_commute)
   1.951 +apply (rule eq_Abs_hcomplex [of x])
   1.952 +apply (rule eq_Abs_hcomplex [of y])
   1.953 +apply (simp add: hcmod hcomplex_diff complex_mod_diff_commute)
   1.954  done
   1.955  
   1.956  lemma hcmod_add_less:
   1.957       "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s"
   1.958 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
   1.959 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
   1.960 -apply (rule_tac z = "r" in eq_Abs_hypreal)
   1.961 -apply (rule_tac z = "s" in eq_Abs_hypreal)
   1.962 -apply (auto simp add: hcmod hcomplex_add hypreal_add hypreal_less)
   1.963 -apply ultra
   1.964 +apply (rule eq_Abs_hcomplex [of x])
   1.965 +apply (rule eq_Abs_hcomplex [of y])
   1.966 +apply (rule eq_Abs_hypreal [of r])
   1.967 +apply (rule eq_Abs_hypreal [of s])
   1.968 +apply (simp add: hcmod hcomplex_add hypreal_add hypreal_less, ultra)
   1.969  apply (auto intro: complex_mod_add_less)
   1.970  done
   1.971  
   1.972  lemma hcmod_mult_less:
   1.973       "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s"
   1.974 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
   1.975 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
   1.976 -apply (rule_tac z = "r" in eq_Abs_hypreal)
   1.977 -apply (rule_tac z = "s" in eq_Abs_hypreal)
   1.978 -apply (auto simp add: hcmod hypreal_mult hypreal_less hcomplex_mult)
   1.979 -apply ultra
   1.980 +apply (rule eq_Abs_hcomplex [of x])
   1.981 +apply (rule eq_Abs_hcomplex [of y])
   1.982 +apply (rule eq_Abs_hypreal [of r])
   1.983 +apply (rule eq_Abs_hypreal [of s])
   1.984 +apply (simp add: hcmod hypreal_mult hypreal_less hcomplex_mult, ultra)
   1.985  apply (auto intro: complex_mod_mult_less)
   1.986  done
   1.987  
   1.988 -lemma hcmod_diff_ineq: "hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
   1.989 -apply (rule_tac z = "a" in eq_Abs_hcomplex)
   1.990 -apply (rule_tac z = "b" in eq_Abs_hcomplex)
   1.991 -apply (auto simp add: hcmod hcomplex_add hypreal_diff hypreal_le)
   1.992 +lemma hcmod_diff_ineq [simp]: "hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
   1.993 +apply (rule eq_Abs_hcomplex [of a])
   1.994 +apply (rule eq_Abs_hcomplex [of b])
   1.995 +apply (simp add: hcmod hcomplex_add hypreal_diff hypreal_le)
   1.996  done
   1.997 -declare hcmod_diff_ineq [simp]
   1.998 -
   1.999  
  1.1000  
  1.1001  subsection{*A Few Nonlinear Theorems*}
  1.1002 @@ -903,42 +775,32 @@
  1.1003    "Abs_hcomplex(hcomplexrel``{%n. X n}) hcpow
  1.1004     Abs_hypnat(hypnatrel``{%n. Y n}) =
  1.1005     Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})"
  1.1006 -apply (unfold hcpow_def)
  1.1007 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
  1.1008 +apply (simp add: hcpow_def)
  1.1009 +apply (rule_tac f = Abs_hcomplex in arg_cong)
  1.1010  apply (auto, ultra)
  1.1011  done
  1.1012  
  1.1013  lemma hcomplex_of_hypreal_hyperpow:
  1.1014       "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
  1.1015 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  1.1016 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  1.1017 -apply (auto simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow)
  1.1018 +apply (rule eq_Abs_hypreal [of x])
  1.1019 +apply (rule eq_Abs_hypnat [of n])
  1.1020 +apply (simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow)
  1.1021  done
  1.1022  
  1.1023  lemma hcmod_hcpow: "hcmod(x hcpow n) = hcmod(x) pow n"
  1.1024 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
  1.1025 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  1.1026 -apply (auto simp add: hcpow hyperpow hcmod complex_mod_complexpow)
  1.1027 +apply (rule eq_Abs_hcomplex [of x])
  1.1028 +apply (rule eq_Abs_hypnat [of n])
  1.1029 +apply (simp add: hcpow hyperpow hcmod complex_mod_complexpow)
  1.1030  done
  1.1031  
  1.1032  lemma hcmod_hcomplex_inverse: "hcmod(inverse x) = inverse(hcmod x)"
  1.1033 -apply (case_tac "x = 0", simp add: HCOMPLEX_INVERSE_ZERO)
  1.1034 +apply (case_tac "x = 0", simp)
  1.1035  apply (rule_tac c1 = "hcmod x" in hypreal_mult_left_cancel [THEN iffD1])
  1.1036  apply (auto simp add: hcmod_mult [symmetric])
  1.1037  done
  1.1038  
  1.1039 -lemma hcmod_divide:
  1.1040 -      "hcmod(x/y) = hcmod(x)/(hcmod y)"
  1.1041 -apply (unfold hcomplex_divide_def hypreal_divide_def)
  1.1042 -apply (auto simp add: hcmod_mult hcmod_hcomplex_inverse)
  1.1043 -done
  1.1044 -
  1.1045 -lemma hcomplex_inverse_divide:
  1.1046 -      "inverse(x/y) = y/(x::hcomplex)"
  1.1047 -apply (unfold hcomplex_divide_def)
  1.1048 -apply (auto simp add: inverse_mult_distrib hcomplex_mult_commute)
  1.1049 -done
  1.1050 -declare hcomplex_inverse_divide [simp]
  1.1051 +lemma hcmod_divide: "hcmod(x/y) = hcmod(x)/(hcmod y)"
  1.1052 +by (simp add: hcomplex_divide_def hypreal_divide_def hcmod_mult hcmod_hcomplex_inverse)
  1.1053  
  1.1054  
  1.1055  subsection{*Exponentiation*}
  1.1056 @@ -974,73 +836,56 @@
  1.1057  
  1.1058  lemma hcomplexpow_minus:
  1.1059       "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
  1.1060 -apply (induct_tac "n")
  1.1061 -apply auto
  1.1062 -done
  1.1063 +by (induct_tac "n", auto)
  1.1064  
  1.1065  lemma hcpow_minus:
  1.1066       "(-x::hcomplex) hcpow n =
  1.1067        (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"
  1.1068 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
  1.1069 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  1.1070 -apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus)
  1.1071 -apply ultra
  1.1072 -apply (auto simp add: complexpow_minus) 
  1.1073 -apply ultra
  1.1074 +apply (rule eq_Abs_hcomplex [of x])
  1.1075 +apply (rule eq_Abs_hypnat [of n])
  1.1076 +apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus, ultra)
  1.1077 +apply (auto simp add: complexpow_minus, ultra)
  1.1078  done
  1.1079  
  1.1080  lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
  1.1081 -apply (rule_tac z = "r" in eq_Abs_hcomplex)
  1.1082 -apply (rule_tac z = "s" in eq_Abs_hcomplex)
  1.1083 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  1.1084 -apply (auto simp add: hcpow hypreal_mult hcomplex_mult power_mult_distrib)
  1.1085 +apply (rule eq_Abs_hcomplex [of r])
  1.1086 +apply (rule eq_Abs_hcomplex [of s])
  1.1087 +apply (rule eq_Abs_hypnat [of n])
  1.1088 +apply (simp add: hcpow hypreal_mult hcomplex_mult power_mult_distrib)
  1.1089  done
  1.1090  
  1.1091  lemma hcpow_zero [simp]: "0 hcpow (n + 1) = 0"
  1.1092 -apply (unfold hcomplex_zero_def hypnat_one_def)
  1.1093 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  1.1094 -apply (auto simp add: hcpow hypnat_add)
  1.1095 +apply (simp add: hcomplex_zero_def hypnat_one_def)
  1.1096 +apply (rule eq_Abs_hypnat [of n])
  1.1097 +apply (simp add: hcpow hypnat_add)
  1.1098  done
  1.1099  
  1.1100  lemma hcpow_zero2 [simp]: "0 hcpow (hSuc n) = 0"
  1.1101 -apply (unfold hSuc_def)
  1.1102 -apply (simp (no_asm))
  1.1103 -done
  1.1104 +by (simp add: hSuc_def)
  1.1105  
  1.1106  lemma hcpow_not_zero [simp,intro]: "r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)"
  1.1107 -apply (rule_tac z = "r" in eq_Abs_hcomplex)
  1.1108 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  1.1109 -apply (auto simp add: hcpow hcomplex_zero_def)
  1.1110 -apply ultra
  1.1111 +apply (rule eq_Abs_hcomplex [of r])
  1.1112 +apply (rule eq_Abs_hypnat [of n])
  1.1113 +apply (auto simp add: hcpow hcomplex_zero_def, ultra)
  1.1114  done
  1.1115  
  1.1116  lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0"
  1.1117 -apply (blast intro: ccontr dest: hcpow_not_zero)
  1.1118 -done
  1.1119 +by (blast intro: ccontr dest: hcpow_not_zero)
  1.1120  
  1.1121 -lemma hcomplex_i_mult_eq: "iii * iii = - 1"
  1.1122 -apply (unfold iii_def)
  1.1123 -apply (auto simp add: hcomplex_mult hcomplex_one_def hcomplex_minus)
  1.1124 -done
  1.1125 -declare hcomplex_i_mult_eq [simp]
  1.1126 +lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1"
  1.1127 +by (simp add: iii_def hcomplex_mult hcomplex_one_def hcomplex_minus)
  1.1128  
  1.1129 -lemma hcomplexpow_i_squared: "iii ^ 2 = - 1"
  1.1130 -apply (simp (no_asm) add: numeral_2_eq_2)
  1.1131 -done
  1.1132 -declare hcomplexpow_i_squared [simp]
  1.1133 +lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = - 1"
  1.1134 +by (simp add: numeral_2_eq_2)
  1.1135  
  1.1136 -lemma hcomplex_i_not_zero: "iii \<noteq> 0"
  1.1137 -apply (unfold iii_def hcomplex_zero_def)
  1.1138 -apply auto
  1.1139 -done
  1.1140 -declare hcomplex_i_not_zero [simp]
  1.1141 +lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0"
  1.1142 +by (simp add: iii_def hcomplex_zero_def)
  1.1143  
  1.1144  lemma hcomplex_divide:
  1.1145    "Abs_hcomplex(hcomplexrel``{%n. X n}) / Abs_hcomplex(hcomplexrel``{%n. Y n}) =
  1.1146     Abs_hcomplex(hcomplexrel``{%n. X n / Y n})"
  1.1147 -apply (unfold hcomplex_divide_def complex_divide_def)
  1.1148 -apply (auto simp add: hcomplex_inverse hcomplex_mult)
  1.1149 -done
  1.1150 +by (simp add: hcomplex_divide_def complex_divide_def hcomplex_inverse hcomplex_mult)
  1.1151 +
  1.1152  
  1.1153  
  1.1154  subsection{*The Function @{term hsgn}*}
  1.1155 @@ -1048,244 +893,210 @@
  1.1156  lemma hsgn:
  1.1157    "hsgn (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
  1.1158        Abs_hcomplex(hcomplexrel `` {%n. sgn (X n)})"
  1.1159 -apply (unfold hsgn_def)
  1.1160 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
  1.1161 +apply (simp add: hsgn_def)
  1.1162 +apply (rule_tac f = Abs_hcomplex in arg_cong)
  1.1163  apply (auto, ultra)
  1.1164  done
  1.1165  
  1.1166 -lemma hsgn_zero: "hsgn 0 = 0"
  1.1167 -apply (unfold hcomplex_zero_def)
  1.1168 -apply (simp (no_asm) add: hsgn)
  1.1169 -done
  1.1170 -declare hsgn_zero [simp]
  1.1171 +lemma hsgn_zero [simp]: "hsgn 0 = 0"
  1.1172 +by (simp add: hcomplex_zero_def hsgn)
  1.1173  
  1.1174 -
  1.1175 -lemma hsgn_one: "hsgn 1 = 1"
  1.1176 -apply (unfold hcomplex_one_def)
  1.1177 -apply (simp (no_asm) add: hsgn)
  1.1178 -done
  1.1179 -declare hsgn_one [simp]
  1.1180 +lemma hsgn_one [simp]: "hsgn 1 = 1"
  1.1181 +by (simp add: hcomplex_one_def hsgn)
  1.1182  
  1.1183  lemma hsgn_minus: "hsgn (-z) = - hsgn(z)"
  1.1184 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
  1.1185 -apply (auto simp add: hsgn hcomplex_minus sgn_minus)
  1.1186 +apply (rule eq_Abs_hcomplex [of z])
  1.1187 +apply (simp add: hsgn hcomplex_minus sgn_minus)
  1.1188  done
  1.1189  
  1.1190  lemma hsgn_eq: "hsgn z = z / hcomplex_of_hypreal (hcmod z)"
  1.1191 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
  1.1192 -apply (auto simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq)
  1.1193 +apply (rule eq_Abs_hcomplex [of z])
  1.1194 +apply (simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq)
  1.1195  done
  1.1196  
  1.1197  lemma lemma_hypreal_P_EX2:
  1.1198       "(\<exists>(x::hypreal) y. P x y) =
  1.1199        (\<exists>f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"
  1.1200  apply auto
  1.1201 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  1.1202 -apply (rule_tac z = "y" in eq_Abs_hypreal)
  1.1203 -apply auto
  1.1204 +apply (rule_tac z = x in eq_Abs_hypreal)
  1.1205 +apply (rule_tac z = y in eq_Abs_hypreal, auto)
  1.1206  done
  1.1207  
  1.1208  lemma complex_split2:
  1.1209       "\<forall>(n::nat). \<exists>x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)"
  1.1210 -apply (blast intro: complex_split)
  1.1211 -done
  1.1212 +by (blast intro: complex_split)
  1.1213  
  1.1214  (* Interesting proof! *)
  1.1215  lemma hcomplex_split:
  1.1216       "\<exists>x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)"
  1.1217 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
  1.1218 +apply (rule eq_Abs_hcomplex [of z])
  1.1219  apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult)
  1.1220 -apply (cut_tac z = "x" in complex_split2)
  1.1221 +apply (cut_tac z = x in complex_split2)
  1.1222  apply (drule choice, safe)+
  1.1223 -apply (rule_tac x = "f" in exI)
  1.1224 -apply (rule_tac x = "fa" in exI)
  1.1225 -apply auto
  1.1226 +apply (rule_tac x = f in exI)
  1.1227 +apply (rule_tac x = fa in exI, auto)
  1.1228  done
  1.1229  
  1.1230 -lemma hRe_hcomplex_i:
  1.1231 +lemma hRe_hcomplex_i [simp]:
  1.1232       "hRe(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = x"
  1.1233 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  1.1234 -apply (rule_tac z = "y" in eq_Abs_hypreal)
  1.1235 +apply (rule eq_Abs_hypreal [of x])
  1.1236 +apply (rule eq_Abs_hypreal [of y])
  1.1237  apply (auto simp add: hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
  1.1238  done
  1.1239 -declare hRe_hcomplex_i [simp]
  1.1240  
  1.1241 -lemma hIm_hcomplex_i:
  1.1242 +lemma hIm_hcomplex_i [simp]:
  1.1243       "hIm(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = y"
  1.1244 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  1.1245 -apply (rule_tac z = "y" in eq_Abs_hypreal)
  1.1246 -apply (auto simp add: hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
  1.1247 +apply (rule eq_Abs_hypreal [of x])
  1.1248 +apply (rule eq_Abs_hypreal [of y])
  1.1249 +apply (simp add: hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
  1.1250  done
  1.1251 -declare hIm_hcomplex_i [simp]
  1.1252  
  1.1253  lemma hcmod_i:
  1.1254       "hcmod (hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) =
  1.1255        ( *f* sqrt) (x ^ 2 + y ^ 2)"
  1.1256 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  1.1257 -apply (rule_tac z = "y" in eq_Abs_hypreal)
  1.1258 -apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult starfun hypreal_mult hypreal_add hcmod cmod_i numeral_2_eq_2)
  1.1259 +apply (rule eq_Abs_hypreal [of x])
  1.1260 +apply (rule eq_Abs_hypreal [of y])
  1.1261 +apply (simp add: hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult starfun hypreal_mult hypreal_add hcmod cmod_i numeral_2_eq_2)
  1.1262  done
  1.1263  
  1.1264  lemma hcomplex_eq_hRe_eq:
  1.1265       "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
  1.1266        hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb
  1.1267         ==> xa = xb"
  1.1268 -apply (unfold iii_def)
  1.1269 -apply (rule_tac z = "xa" in eq_Abs_hypreal)
  1.1270 -apply (rule_tac z = "ya" in eq_Abs_hypreal)
  1.1271 -apply (rule_tac z = "xb" in eq_Abs_hypreal)
  1.1272 -apply (rule_tac z = "yb" in eq_Abs_hypreal)
  1.1273 -apply (auto simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal)
  1.1274 -apply (ultra)
  1.1275 +apply (simp add: iii_def)
  1.1276 +apply (rule eq_Abs_hypreal [of xa])
  1.1277 +apply (rule eq_Abs_hypreal [of ya])
  1.1278 +apply (rule eq_Abs_hypreal [of xb])
  1.1279 +apply (rule eq_Abs_hypreal [of yb])
  1.1280 +apply (simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal, ultra)
  1.1281  done
  1.1282  
  1.1283  lemma hcomplex_eq_hIm_eq:
  1.1284       "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
  1.1285        hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb
  1.1286         ==> ya = yb"
  1.1287 -apply (unfold iii_def)
  1.1288 -apply (rule_tac z = "xa" in eq_Abs_hypreal)
  1.1289 -apply (rule_tac z = "ya" in eq_Abs_hypreal)
  1.1290 -apply (rule_tac z = "xb" in eq_Abs_hypreal)
  1.1291 -apply (rule_tac z = "yb" in eq_Abs_hypreal)
  1.1292 -apply (auto simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal)
  1.1293 -apply (ultra)
  1.1294 +apply (simp add: iii_def)
  1.1295 +apply (rule eq_Abs_hypreal [of xa])
  1.1296 +apply (rule eq_Abs_hypreal [of ya])
  1.1297 +apply (rule eq_Abs_hypreal [of xb])
  1.1298 +apply (rule eq_Abs_hypreal [of yb])
  1.1299 +apply (simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal, ultra)
  1.1300  done
  1.1301  
  1.1302 -lemma hcomplex_eq_cancel_iff:
  1.1303 +lemma hcomplex_eq_cancel_iff [simp]:
  1.1304       "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
  1.1305         hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) =
  1.1306        ((xa = xb) & (ya = yb))"
  1.1307 -apply (auto intro: hcomplex_eq_hIm_eq hcomplex_eq_hRe_eq)
  1.1308 -done
  1.1309 -declare hcomplex_eq_cancel_iff [simp]
  1.1310 +by (auto intro: hcomplex_eq_hIm_eq hcomplex_eq_hRe_eq)
  1.1311  
  1.1312 -lemma hcomplex_eq_cancel_iffA:
  1.1313 +lemma hcomplex_eq_cancel_iffA [iff]:
  1.1314       "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
  1.1315 -       hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii ) = ((xa = xb) & (ya = yb))"
  1.1316 -apply (auto simp add: hcomplex_mult_commute)
  1.1317 +       hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))"
  1.1318 +apply (simp add: hcomplex_mult_commute)
  1.1319  done
  1.1320 -declare hcomplex_eq_cancel_iffA [iff]
  1.1321  
  1.1322 -lemma hcomplex_eq_cancel_iffB:
  1.1323 +lemma hcomplex_eq_cancel_iffB [iff]:
  1.1324       "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
  1.1325         hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = ((xa = xb) & (ya = yb))"
  1.1326 -apply (auto simp add: hcomplex_mult_commute)
  1.1327 +apply (simp add: hcomplex_mult_commute)
  1.1328  done
  1.1329 -declare hcomplex_eq_cancel_iffB [iff]
  1.1330  
  1.1331 -lemma hcomplex_eq_cancel_iffC:
  1.1332 +lemma hcomplex_eq_cancel_iffC [iff]:
  1.1333       "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya  =
  1.1334         hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))"
  1.1335 -apply (auto simp add: hcomplex_mult_commute)
  1.1336 +apply (simp add: hcomplex_mult_commute)
  1.1337  done
  1.1338 -declare hcomplex_eq_cancel_iffC [iff]
  1.1339  
  1.1340 -lemma hcomplex_eq_cancel_iff2:
  1.1341 +lemma hcomplex_eq_cancel_iff2 [simp]:
  1.1342       "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
  1.1343        hcomplex_of_hypreal xa) = (x = xa & y = 0)"
  1.1344 -apply (cut_tac xa = "x" and ya = "y" and xb = "xa" and yb = "0" in hcomplex_eq_cancel_iff)
  1.1345 +apply (cut_tac xa = x and ya = y and xb = xa and yb = 0 in hcomplex_eq_cancel_iff)
  1.1346  apply (simp del: hcomplex_eq_cancel_iff)
  1.1347  done
  1.1348 -declare hcomplex_eq_cancel_iff2 [simp]
  1.1349  
  1.1350 -lemma hcomplex_eq_cancel_iff2a:
  1.1351 +lemma hcomplex_eq_cancel_iff2a [simp]:
  1.1352       "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
  1.1353        hcomplex_of_hypreal xa) = (x = xa & y = 0)"
  1.1354 -apply (auto simp add: hcomplex_mult_commute)
  1.1355 +apply (simp add: hcomplex_mult_commute)
  1.1356  done
  1.1357 -declare hcomplex_eq_cancel_iff2a [simp]
  1.1358  
  1.1359 -lemma hcomplex_eq_cancel_iff3:
  1.1360 +lemma hcomplex_eq_cancel_iff3 [simp]:
  1.1361       "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
  1.1362        iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"
  1.1363 -apply (cut_tac xa = "x" and ya = "y" and xb = "0" and yb = "ya" in hcomplex_eq_cancel_iff)
  1.1364 +apply (cut_tac xa = x and ya = y and xb = 0 and yb = ya in hcomplex_eq_cancel_iff)
  1.1365  apply (simp del: hcomplex_eq_cancel_iff)
  1.1366  done
  1.1367 -declare hcomplex_eq_cancel_iff3 [simp]
  1.1368  
  1.1369 -lemma hcomplex_eq_cancel_iff3a:
  1.1370 +lemma hcomplex_eq_cancel_iff3a [simp]:
  1.1371       "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
  1.1372        iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"
  1.1373 -apply (auto simp add: hcomplex_mult_commute)
  1.1374 +apply (simp add: hcomplex_mult_commute)
  1.1375  done
  1.1376 -declare hcomplex_eq_cancel_iff3a [simp]
  1.1377  
  1.1378  lemma hcomplex_split_hRe_zero:
  1.1379       "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0
  1.1380        ==> x = 0"
  1.1381 -apply (unfold iii_def)
  1.1382 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  1.1383 -apply (rule_tac z = "y" in eq_Abs_hypreal)
  1.1384 -apply (auto simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num)
  1.1385 -apply ultra
  1.1386 -apply (auto simp add: complex_split_Re_zero)
  1.1387 +apply (simp add: iii_def)
  1.1388 +apply (rule eq_Abs_hypreal [of x])
  1.1389 +apply (rule eq_Abs_hypreal [of y])
  1.1390 +apply (simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num, ultra)
  1.1391 +apply (simp add: complex_split_Re_zero)
  1.1392  done
  1.1393  
  1.1394  lemma hcomplex_split_hIm_zero:
  1.1395       "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0
  1.1396        ==> y = 0"
  1.1397 -apply (unfold iii_def)
  1.1398 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  1.1399 -apply (rule_tac z = "y" in eq_Abs_hypreal)
  1.1400 -apply (auto simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num)
  1.1401 -apply ultra
  1.1402 -apply (auto simp add: complex_split_Im_zero)
  1.1403 +apply (simp add: iii_def)
  1.1404 +apply (rule eq_Abs_hypreal [of x])
  1.1405 +apply (rule eq_Abs_hypreal [of y])
  1.1406 +apply (simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num, ultra)
  1.1407 +apply (simp add: complex_split_Im_zero)
  1.1408  done
  1.1409  
  1.1410 -lemma hRe_hsgn: "hRe(hsgn z) = hRe(z)/hcmod z"
  1.1411 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
  1.1412 -apply (auto simp add: hsgn hcmod hRe hypreal_divide)
  1.1413 +lemma hRe_hsgn [simp]: "hRe(hsgn z) = hRe(z)/hcmod z"
  1.1414 +apply (rule eq_Abs_hcomplex [of z])
  1.1415 +apply (simp add: hsgn hcmod hRe hypreal_divide)
  1.1416  done
  1.1417 -declare hRe_hsgn [simp]
  1.1418  
  1.1419 -lemma hIm_hsgn: "hIm(hsgn z) = hIm(z)/hcmod z"
  1.1420 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
  1.1421 -apply (auto simp add: hsgn hcmod hIm hypreal_divide)
  1.1422 +lemma hIm_hsgn [simp]: "hIm(hsgn z) = hIm(z)/hcmod z"
  1.1423 +apply (rule eq_Abs_hcomplex [of z])
  1.1424 +apply (simp add: hsgn hcmod hIm hypreal_divide)
  1.1425  done
  1.1426 -declare hIm_hsgn [simp]
  1.1427  
  1.1428 -lemma real_two_squares_add_zero_iff:
  1.1429 -     "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"
  1.1430 +lemma real_two_squares_add_zero_iff [simp]: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"
  1.1431  apply (auto intro: real_sum_squares_cancel)
  1.1432  done
  1.1433 -declare real_two_squares_add_zero_iff [simp]
  1.1434  
  1.1435  lemma hcomplex_inverse_complex_split:
  1.1436       "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
  1.1437        hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
  1.1438        iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
  1.1439 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  1.1440 -apply (rule_tac z = "y" in eq_Abs_hypreal)
  1.1441 -apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide hcomplex_diff complex_inverse_complex_split numeral_2_eq_2)
  1.1442 +apply (rule eq_Abs_hypreal [of x])
  1.1443 +apply (rule eq_Abs_hypreal [of y])
  1.1444 +apply (simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide hcomplex_diff complex_inverse_complex_split numeral_2_eq_2)
  1.1445 +done
  1.1446 +
  1.1447 +lemma hRe_mult_i_eq[simp]:
  1.1448 +    "hRe (iii * hcomplex_of_hypreal y) = 0"
  1.1449 +apply (simp add: iii_def)
  1.1450 +apply (rule eq_Abs_hypreal [of y])
  1.1451 +apply (simp add: hcomplex_of_hypreal hcomplex_mult hRe hypreal_zero_num)
  1.1452  done
  1.1453  
  1.1454 -lemma hRe_mult_i_eq:
  1.1455 -    "hRe (iii * hcomplex_of_hypreal y) = 0"
  1.1456 -apply (unfold iii_def)
  1.1457 -apply (rule_tac z = "y" in eq_Abs_hypreal)
  1.1458 -apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hRe hypreal_zero_num)
  1.1459 -done
  1.1460 -declare hRe_mult_i_eq [simp]
  1.1461 -
  1.1462 -lemma hIm_mult_i_eq:
  1.1463 +lemma hIm_mult_i_eq [simp]:
  1.1464      "hIm (iii * hcomplex_of_hypreal y) = y"
  1.1465 -apply (unfold iii_def)
  1.1466 -apply (rule_tac z = "y" in eq_Abs_hypreal)
  1.1467 -apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hIm hypreal_zero_num)
  1.1468 +apply (simp add: iii_def)
  1.1469 +apply (rule eq_Abs_hypreal [of y])
  1.1470 +apply (simp add: hcomplex_of_hypreal hcomplex_mult hIm hypreal_zero_num)
  1.1471  done
  1.1472 -declare hIm_mult_i_eq [simp]
  1.1473  
  1.1474 -lemma hcmod_mult_i: "hcmod (iii * hcomplex_of_hypreal y) = abs y"
  1.1475 -apply (rule_tac z = "y" in eq_Abs_hypreal)
  1.1476 -apply (auto simp add: hcomplex_of_hypreal hcmod hypreal_hrabs iii_def hcomplex_mult)
  1.1477 +lemma hcmod_mult_i [simp]: "hcmod (iii * hcomplex_of_hypreal y) = abs y"
  1.1478 +apply (rule eq_Abs_hypreal [of y])
  1.1479 +apply (simp add: hcomplex_of_hypreal hcmod hypreal_hrabs iii_def hcomplex_mult)
  1.1480  done
  1.1481 -declare hcmod_mult_i [simp]
  1.1482  
  1.1483 -lemma hcmod_mult_i2: "hcmod (hcomplex_of_hypreal y * iii) = abs y"
  1.1484 -apply (auto simp add: hcomplex_mult_commute)
  1.1485 -done
  1.1486 -declare hcmod_mult_i2 [simp]
  1.1487 +lemma hcmod_mult_i2 [simp]: "hcmod (hcomplex_of_hypreal y * iii) = abs y"
  1.1488 +by (simp add: hcomplex_mult_commute)
  1.1489  
  1.1490  (*---------------------------------------------------------------------------*)
  1.1491  (*  harg                                                                     *)
  1.1492 @@ -1295,37 +1106,35 @@
  1.1493    "harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
  1.1494        Abs_hypreal(hyprel `` {%n. arg (X n)})"
  1.1495  
  1.1496 -apply (unfold harg_def)
  1.1497 -apply (rule_tac f = "Abs_hypreal" in arg_cong)
  1.1498 +apply (simp add: harg_def)
  1.1499 +apply (rule_tac f = Abs_hypreal in arg_cong)
  1.1500  apply (auto, ultra)
  1.1501  done
  1.1502  
  1.1503  lemma cos_harg_i_mult_zero_pos:
  1.1504       "0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
  1.1505 -apply (rule_tac z = "y" in eq_Abs_hypreal)
  1.1506 -apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult 
  1.1507 -                hypreal_zero_num hypreal_less starfun harg)
  1.1508 -apply (ultra)
  1.1509 +apply (rule eq_Abs_hypreal [of y])
  1.1510 +apply (simp add: hcomplex_of_hypreal iii_def hcomplex_mult
  1.1511 +                hypreal_zero_num hypreal_less starfun harg, ultra)
  1.1512  done
  1.1513  
  1.1514  lemma cos_harg_i_mult_zero_neg:
  1.1515       "y < 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
  1.1516 -apply (rule_tac z = "y" in eq_Abs_hypreal)
  1.1517 -apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult
  1.1518 -                      hypreal_zero_num hypreal_less starfun harg)
  1.1519 -apply (ultra)
  1.1520 +apply (rule eq_Abs_hypreal [of y])
  1.1521 +apply (simp add: hcomplex_of_hypreal iii_def hcomplex_mult
  1.1522 +                      hypreal_zero_num hypreal_less starfun harg, ultra)
  1.1523  done
  1.1524  
  1.1525  lemma cos_harg_i_mult_zero [simp]:
  1.1526       "y \<noteq> 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
  1.1527 -apply (cut_tac x = "y" and y = "0" in linorder_less_linear)
  1.1528 +apply (cut_tac x = y and y = 0 in linorder_less_linear)
  1.1529  apply (auto simp add: cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg)
  1.1530  done
  1.1531  
  1.1532  lemma hcomplex_of_hypreal_zero_iff [simp]:
  1.1533       "(hcomplex_of_hypreal y = 0) = (y = 0)"
  1.1534 -apply (rule_tac z = "y" in eq_Abs_hypreal)
  1.1535 -apply (auto simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
  1.1536 +apply (rule eq_Abs_hypreal [of y])
  1.1537 +apply (simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
  1.1538  done
  1.1539  
  1.1540  
  1.1541 @@ -1340,331 +1149,259 @@
  1.1542  lemma hcomplex_split_polar:
  1.1543    "\<exists>r a. z = hcomplex_of_hypreal r *
  1.1544     (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))"
  1.1545 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
  1.1546 -apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult)
  1.1547 -apply (cut_tac z = "x" in complex_split_polar2)
  1.1548 +apply (rule eq_Abs_hcomplex [of z])
  1.1549 +apply (simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult)
  1.1550 +apply (cut_tac z = x in complex_split_polar2)
  1.1551  apply (drule choice, safe)+
  1.1552 -apply (rule_tac x = "f" in exI)
  1.1553 -apply (rule_tac x = "fa" in exI)
  1.1554 -apply auto
  1.1555 +apply (rule_tac x = f in exI)
  1.1556 +apply (rule_tac x = fa in exI, auto)
  1.1557  done
  1.1558  
  1.1559  lemma hcis:
  1.1560    "hcis (Abs_hypreal(hyprel `` {%n. X n})) =
  1.1561        Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})"
  1.1562 -apply (unfold hcis_def)
  1.1563 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
  1.1564 -apply auto
  1.1565 -apply (ultra)
  1.1566 +apply (simp add: hcis_def)
  1.1567 +apply (rule_tac f = Abs_hcomplex in arg_cong, auto, ultra)
  1.1568  done
  1.1569  
  1.1570  lemma hcis_eq:
  1.1571     "hcis a =
  1.1572      (hcomplex_of_hypreal(( *f* cos) a) +
  1.1573      iii * hcomplex_of_hypreal(( *f* sin) a))"
  1.1574 -apply (rule_tac z = "a" in eq_Abs_hypreal)
  1.1575 -apply (auto simp add: starfun hcis hcomplex_of_hypreal iii_def hcomplex_mult hcomplex_add cis_def)
  1.1576 +apply (rule eq_Abs_hypreal [of a])
  1.1577 +apply (simp add: starfun hcis hcomplex_of_hypreal iii_def hcomplex_mult hcomplex_add cis_def)
  1.1578  done
  1.1579  
  1.1580  lemma hrcis:
  1.1581    "hrcis (Abs_hypreal(hyprel `` {%n. X n})) (Abs_hypreal(hyprel `` {%n. Y n})) =
  1.1582        Abs_hcomplex(hcomplexrel `` {%n. rcis (X n) (Y n)})"
  1.1583 -apply (unfold hrcis_def)
  1.1584 -apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hcis rcis_def)
  1.1585 -done
  1.1586 +by (simp add: hrcis_def hcomplex_of_hypreal hcomplex_mult hcis rcis_def)
  1.1587  
  1.1588  lemma hrcis_Ex: "\<exists>r a. z = hrcis r a"
  1.1589 -apply (simp (no_asm) add: hrcis_def hcis_eq)
  1.1590 +apply (simp add: hrcis_def hcis_eq)
  1.1591  apply (rule hcomplex_split_polar)
  1.1592  done
  1.1593  
  1.1594 -lemma hRe_hcomplex_polar:
  1.1595 +lemma hRe_hcomplex_polar [simp]:
  1.1596       "hRe(hcomplex_of_hypreal r *
  1.1597        (hcomplex_of_hypreal(( *f* cos) a) +
  1.1598         iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* cos) a"
  1.1599 -apply (auto simp add: right_distrib hcomplex_of_hypreal_mult mult_ac)
  1.1600 -done
  1.1601 -declare hRe_hcomplex_polar [simp]
  1.1602 +by (simp add: right_distrib hcomplex_of_hypreal_mult mult_ac)
  1.1603  
  1.1604 -lemma hRe_hrcis: "hRe(hrcis r a) = r * ( *f* cos) a"
  1.1605 -apply (unfold hrcis_def)
  1.1606 -apply (auto simp add: hcis_eq)
  1.1607 -done
  1.1608 -declare hRe_hrcis [simp]
  1.1609 +lemma hRe_hrcis [simp]: "hRe(hrcis r a) = r * ( *f* cos) a"
  1.1610 +by (simp add: hrcis_def hcis_eq)
  1.1611  
  1.1612 -lemma hIm_hcomplex_polar:
  1.1613 +lemma hIm_hcomplex_polar [simp]:
  1.1614       "hIm(hcomplex_of_hypreal r *
  1.1615        (hcomplex_of_hypreal(( *f* cos) a) +
  1.1616         iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* sin) a"
  1.1617 -apply (auto simp add: right_distrib hcomplex_of_hypreal_mult mult_ac)
  1.1618 -done
  1.1619 -declare hIm_hcomplex_polar [simp]
  1.1620 +by (simp add: right_distrib hcomplex_of_hypreal_mult mult_ac)
  1.1621  
  1.1622 -lemma hIm_hrcis: "hIm(hrcis r a) = r * ( *f* sin) a"
  1.1623 -apply (unfold hrcis_def)
  1.1624 -apply (auto simp add: hcis_eq)
  1.1625 -done
  1.1626 -declare hIm_hrcis [simp]
  1.1627 +lemma hIm_hrcis [simp]: "hIm(hrcis r a) = r * ( *f* sin) a"
  1.1628 +by (simp add: hrcis_def hcis_eq)
  1.1629  
  1.1630 -lemma hcmod_complex_polar:
  1.1631 +lemma hcmod_complex_polar [simp]:
  1.1632       "hcmod (hcomplex_of_hypreal r *
  1.1633        (hcomplex_of_hypreal(( *f* cos) a) +
  1.1634         iii * hcomplex_of_hypreal(( *f* sin) a))) = abs r"
  1.1635 -apply (rule_tac z = "r" in eq_Abs_hypreal)
  1.1636 -apply (rule_tac z = "a" in eq_Abs_hypreal)
  1.1637 -apply (auto simp add: iii_def starfun hcomplex_of_hypreal hcomplex_mult hcmod hcomplex_add hypreal_hrabs)
  1.1638 +apply (rule eq_Abs_hypreal [of r])
  1.1639 +apply (rule eq_Abs_hypreal [of a])
  1.1640 +apply (simp add: iii_def starfun hcomplex_of_hypreal hcomplex_mult hcmod hcomplex_add hypreal_hrabs)
  1.1641  done
  1.1642 -declare hcmod_complex_polar [simp]
  1.1643  
  1.1644 -lemma hcmod_hrcis: "hcmod(hrcis r a) = abs r"
  1.1645 -apply (unfold hrcis_def)
  1.1646 -apply (auto simp add: hcis_eq)
  1.1647 -done
  1.1648 -declare hcmod_hrcis [simp]
  1.1649 +lemma hcmod_hrcis [simp]: "hcmod(hrcis r a) = abs r"
  1.1650 +by (simp add: hrcis_def hcis_eq)
  1.1651  
  1.1652  (*---------------------------------------------------------------------------*)
  1.1653  (*  (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b)                *)
  1.1654  (*---------------------------------------------------------------------------*)
  1.1655  
  1.1656  lemma hcis_hrcis_eq: "hcis a = hrcis 1 a"
  1.1657 -apply (unfold hrcis_def)
  1.1658 -apply (simp (no_asm))
  1.1659 -done
  1.1660 +by (simp add: hrcis_def)
  1.1661  declare hcis_hrcis_eq [symmetric, simp]
  1.1662  
  1.1663  lemma hrcis_mult:
  1.1664    "hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
  1.1665 -apply (unfold hrcis_def)
  1.1666 -apply (rule_tac z = "r1" in eq_Abs_hypreal)
  1.1667 -apply (rule_tac z = "r2" in eq_Abs_hypreal)
  1.1668 -apply (rule_tac z = "a" in eq_Abs_hypreal)
  1.1669 -apply (rule_tac z = "b" in eq_Abs_hypreal)
  1.1670 -apply (auto simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal
  1.1671 -                      hcomplex_mult cis_mult [symmetric] 
  1.1672 +apply (simp add: hrcis_def)
  1.1673 +apply (rule eq_Abs_hypreal [of r1])
  1.1674 +apply (rule eq_Abs_hypreal [of r2])
  1.1675 +apply (rule eq_Abs_hypreal [of a])
  1.1676 +apply (rule eq_Abs_hypreal [of b])
  1.1677 +apply (simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal
  1.1678 +                      hcomplex_mult cis_mult [symmetric]
  1.1679                        complex_of_real_mult [symmetric])
  1.1680  done
  1.1681  
  1.1682  lemma hcis_mult: "hcis a * hcis b = hcis (a + b)"
  1.1683 -apply (rule_tac z = "a" in eq_Abs_hypreal)
  1.1684 -apply (rule_tac z = "b" in eq_Abs_hypreal)
  1.1685 -apply (auto simp add: hcis hcomplex_mult hypreal_add cis_mult)
  1.1686 +apply (rule eq_Abs_hypreal [of a])
  1.1687 +apply (rule eq_Abs_hypreal [of b])
  1.1688 +apply (simp add: hcis hcomplex_mult hypreal_add cis_mult)
  1.1689  done
  1.1690  
  1.1691 -lemma hcis_zero:
  1.1692 -  "hcis 0 = 1"
  1.1693 -apply (unfold hcomplex_one_def)
  1.1694 -apply (auto simp add: hcis hypreal_zero_num)
  1.1695 -done
  1.1696 -declare hcis_zero [simp]
  1.1697 +lemma hcis_zero [simp]: "hcis 0 = 1"
  1.1698 +by (simp add: hcomplex_one_def hcis hypreal_zero_num)
  1.1699  
  1.1700 -lemma hrcis_zero_mod:
  1.1701 -  "hrcis 0 a = 0"
  1.1702 -apply (unfold hcomplex_zero_def)
  1.1703 -apply (rule_tac z = "a" in eq_Abs_hypreal)
  1.1704 -apply (auto simp add: hrcis hypreal_zero_num)
  1.1705 +lemma hrcis_zero_mod [simp]: "hrcis 0 a = 0"
  1.1706 +apply (simp add: hcomplex_zero_def)
  1.1707 +apply (rule eq_Abs_hypreal [of a])
  1.1708 +apply (simp add: hrcis hypreal_zero_num)
  1.1709  done
  1.1710 -declare hrcis_zero_mod [simp]
  1.1711  
  1.1712 -lemma hrcis_zero_arg: "hrcis r 0 = hcomplex_of_hypreal r"
  1.1713 -apply (rule_tac z = "r" in eq_Abs_hypreal)
  1.1714 -apply (auto simp add: hrcis hypreal_zero_num hcomplex_of_hypreal)
  1.1715 +lemma hrcis_zero_arg [simp]: "hrcis r 0 = hcomplex_of_hypreal r"
  1.1716 +apply (rule eq_Abs_hypreal [of r])
  1.1717 +apply (simp add: hrcis hypreal_zero_num hcomplex_of_hypreal)
  1.1718  done
  1.1719 -declare hrcis_zero_arg [simp]
  1.1720  
  1.1721 -lemma hcomplex_i_mult_minus: "iii * (iii * x) = - x"
  1.1722 -apply (simp (no_asm) add: hcomplex_mult_assoc [symmetric])
  1.1723 -done
  1.1724 -declare hcomplex_i_mult_minus [simp]
  1.1725 +lemma hcomplex_i_mult_minus [simp]: "iii * (iii * x) = - x"
  1.1726 +by (simp add: hcomplex_mult_assoc [symmetric])
  1.1727  
  1.1728 -lemma hcomplex_i_mult_minus2: "iii * iii * x = - x"
  1.1729 -apply (simp (no_asm))
  1.1730 -done
  1.1731 -declare hcomplex_i_mult_minus2 [simp]
  1.1732 +lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x"
  1.1733 +by simp
  1.1734  
  1.1735  lemma hcis_hypreal_of_nat_Suc_mult:
  1.1736     "hcis (hypreal_of_nat (Suc n) * a) = hcis a * hcis (hypreal_of_nat n * a)"
  1.1737 -apply (rule_tac z = "a" in eq_Abs_hypreal)
  1.1738 -apply (auto simp add: hypreal_of_nat hcis hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
  1.1739 +apply (rule eq_Abs_hypreal [of a])
  1.1740 +apply (simp add: hypreal_of_nat hcis hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
  1.1741  done
  1.1742  
  1.1743  lemma NSDeMoivre: "(hcis a) ^ n = hcis (hypreal_of_nat n * a)"
  1.1744  apply (induct_tac "n")
  1.1745 -apply (auto simp add: hcis_hypreal_of_nat_Suc_mult)
  1.1746 +apply (simp_all add: hcis_hypreal_of_nat_Suc_mult)
  1.1747  done
  1.1748  
  1.1749  lemma hcis_hypreal_of_hypnat_Suc_mult:
  1.1750       "hcis (hypreal_of_hypnat (n + 1) * a) =
  1.1751        hcis a * hcis (hypreal_of_hypnat n * a)"
  1.1752 -apply (rule_tac z = "a" in eq_Abs_hypreal)
  1.1753 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  1.1754 -apply (auto simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
  1.1755 +apply (rule eq_Abs_hypreal [of a])
  1.1756 +apply (rule eq_Abs_hypnat [of n])
  1.1757 +apply (simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
  1.1758  done
  1.1759  
  1.1760  lemma NSDeMoivre_ext: "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)"
  1.1761 -apply (rule_tac z = "a" in eq_Abs_hypreal)
  1.1762 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  1.1763 -apply (auto simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre)
  1.1764 +apply (rule eq_Abs_hypreal [of a])
  1.1765 +apply (rule eq_Abs_hypnat [of n])
  1.1766 +apply (simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre)
  1.1767  done
  1.1768  
  1.1769  lemma DeMoivre2:
  1.1770    "(hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"
  1.1771 -apply (unfold hrcis_def)
  1.1772 -apply (auto simp add: power_mult_distrib NSDeMoivre hcomplex_of_hypreal_pow)
  1.1773 +apply (simp add: hrcis_def power_mult_distrib NSDeMoivre hcomplex_of_hypreal_pow)
  1.1774  done
  1.1775  
  1.1776  lemma DeMoivre2_ext:
  1.1777    "(hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)"
  1.1778 -apply (unfold hrcis_def)
  1.1779 -apply (auto simp add: hcpow_mult NSDeMoivre_ext hcomplex_of_hypreal_hyperpow)
  1.1780 +apply (simp add: hrcis_def hcpow_mult NSDeMoivre_ext hcomplex_of_hypreal_hyperpow)
  1.1781 +done
  1.1782 +
  1.1783 +lemma hcis_inverse [simp]: "inverse(hcis a) = hcis (-a)"
  1.1784 +apply (rule eq_Abs_hypreal [of a])
  1.1785 +apply (simp add: hcomplex_inverse hcis hypreal_minus)
  1.1786  done
  1.1787  
  1.1788 -lemma hcis_inverse: "inverse(hcis a) = hcis (-a)"
  1.1789 -apply (rule_tac z = "a" in eq_Abs_hypreal)
  1.1790 -apply (auto simp add: hcomplex_inverse hcis hypreal_minus)
  1.1791 +lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)"
  1.1792 +apply (rule eq_Abs_hypreal [of a])
  1.1793 +apply (rule eq_Abs_hypreal [of r])
  1.1794 +apply (simp add: hcomplex_inverse hrcis hypreal_minus hypreal_inverse rcis_inverse, ultra)
  1.1795 +apply (simp add: real_divide_def)
  1.1796  done
  1.1797 -declare hcis_inverse [simp]
  1.1798  
  1.1799 -lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)"
  1.1800 -apply (rule_tac z = "a" in eq_Abs_hypreal)
  1.1801 -apply (rule_tac z = "r" in eq_Abs_hypreal)
  1.1802 -apply (auto simp add: hcomplex_inverse hrcis hypreal_minus hypreal_inverse rcis_inverse)
  1.1803 -apply (ultra)
  1.1804 -apply (unfold real_divide_def)
  1.1805 -apply (auto simp add: INVERSE_ZERO)
  1.1806 +lemma hRe_hcis [simp]: "hRe(hcis a) = ( *f* cos) a"
  1.1807 +apply (rule eq_Abs_hypreal [of a])
  1.1808 +apply (simp add: hcis starfun hRe)
  1.1809  done
  1.1810  
  1.1811 -lemma hRe_hcis: "hRe(hcis a) = ( *f* cos) a"
  1.1812 -apply (rule_tac z = "a" in eq_Abs_hypreal)
  1.1813 -apply (auto simp add: hcis starfun hRe)
  1.1814 +lemma hIm_hcis [simp]: "hIm(hcis a) = ( *f* sin) a"
  1.1815 +apply (rule eq_Abs_hypreal [of a])
  1.1816 +apply (simp add: hcis starfun hIm)
  1.1817  done
  1.1818 -declare hRe_hcis [simp]
  1.1819  
  1.1820 -lemma hIm_hcis: "hIm(hcis a) = ( *f* sin) a"
  1.1821 -apply (rule_tac z = "a" in eq_Abs_hypreal)
  1.1822 -apply (auto simp add: hcis starfun hIm)
  1.1823 -done
  1.1824 -declare hIm_hcis [simp]
  1.1825 -
  1.1826 -lemma cos_n_hRe_hcis_pow_n:
  1.1827 -     "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
  1.1828 -apply (auto simp add: NSDeMoivre)
  1.1829 +lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
  1.1830 +apply (simp add: NSDeMoivre)
  1.1831  done
  1.1832  
  1.1833 -lemma sin_n_hIm_hcis_pow_n:
  1.1834 -     "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
  1.1835 -apply (auto simp add: NSDeMoivre)
  1.1836 +lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
  1.1837 +apply (simp add: NSDeMoivre)
  1.1838  done
  1.1839  
  1.1840 -lemma cos_n_hRe_hcis_hcpow_n:
  1.1841 -     "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)"
  1.1842 -apply (auto simp add: NSDeMoivre_ext)
  1.1843 +lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)"
  1.1844 +apply (simp add: NSDeMoivre_ext)
  1.1845  done
  1.1846  
  1.1847 -lemma sin_n_hIm_hcis_hcpow_n:
  1.1848 -     "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)"
  1.1849 -apply (auto simp add: NSDeMoivre_ext)
  1.1850 +lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)"
  1.1851 +apply (simp add: NSDeMoivre_ext)
  1.1852  done
  1.1853  
  1.1854  lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)"
  1.1855 -apply (unfold hexpi_def)
  1.1856 -apply (rule_tac z = "a" in eq_Abs_hcomplex)
  1.1857 -apply (rule_tac z = "b" in eq_Abs_hcomplex)
  1.1858 -apply (auto simp add: hcis hRe hIm hcomplex_add hcomplex_mult hypreal_mult starfun hcomplex_of_hypreal cis_mult [symmetric] complex_Im_add complex_Re_add exp_add complex_of_real_mult)
  1.1859 +apply (simp add: hexpi_def)
  1.1860 +apply (rule eq_Abs_hcomplex [of a])
  1.1861 +apply (rule eq_Abs_hcomplex [of b])
  1.1862 +apply (simp add: hcis hRe hIm hcomplex_add hcomplex_mult hypreal_mult starfun hcomplex_of_hypreal cis_mult [symmetric] complex_Im_add complex_Re_add exp_add complex_of_real_mult)
  1.1863  done
  1.1864  
  1.1865  
  1.1866 -subsection{*@{term hcomplex_of_complex}: the Injection from 
  1.1867 +subsection{*@{term hcomplex_of_complex}: the Injection from
  1.1868    type @{typ complex} to to @{typ hcomplex}*}
  1.1869  
  1.1870  lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)"
  1.1871 -apply (rule inj_onI , rule ccontr)
  1.1872 -apply (auto simp add: hcomplex_of_complex_def)
  1.1873 +apply (rule inj_onI, rule ccontr)
  1.1874 +apply (simp add: hcomplex_of_complex_def)
  1.1875  done
  1.1876  
  1.1877  lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
  1.1878 -apply (unfold iii_def hcomplex_of_complex_def)
  1.1879 -apply (simp (no_asm))
  1.1880 -done
  1.1881 +by (simp add: iii_def hcomplex_of_complex_def)
  1.1882  
  1.1883 -lemma hcomplex_of_complex_add:
  1.1884 +lemma hcomplex_of_complex_add [simp]:
  1.1885       "hcomplex_of_complex (z1 + z2) = hcomplex_of_complex z1 + hcomplex_of_complex z2"
  1.1886 -apply (unfold hcomplex_of_complex_def)
  1.1887 -apply (simp (no_asm) add: hcomplex_add)
  1.1888 -done
  1.1889 -declare hcomplex_of_complex_add [simp]
  1.1890 +by (simp add: hcomplex_of_complex_def hcomplex_add)
  1.1891  
  1.1892 -lemma hcomplex_of_complex_mult:
  1.1893 +lemma hcomplex_of_complex_mult [simp]:
  1.1894       "hcomplex_of_complex (z1 * z2) = hcomplex_of_complex z1 * hcomplex_of_complex z2"
  1.1895 -apply (unfold hcomplex_of_complex_def)
  1.1896 -apply (simp (no_asm) add: hcomplex_mult)
  1.1897 -done
  1.1898 -declare hcomplex_of_complex_mult [simp]
  1.1899 +by (simp add: hcomplex_of_complex_def hcomplex_mult)
  1.1900  
  1.1901 -lemma hcomplex_of_complex_eq_iff:
  1.1902 - "(hcomplex_of_complex z1 = hcomplex_of_complex z2) = (z1 = z2)"
  1.1903 -apply (unfold hcomplex_of_complex_def)
  1.1904 -apply auto
  1.1905 -done
  1.1906 -declare hcomplex_of_complex_eq_iff [simp]
  1.1907 +lemma hcomplex_of_complex_eq_iff [simp]:
  1.1908 +     "(hcomplex_of_complex z1 = hcomplex_of_complex z2) = (z1 = z2)"
  1.1909 +by (simp add: hcomplex_of_complex_def)
  1.1910  
  1.1911 -lemma hcomplex_of_complex_minus:
  1.1912 +
  1.1913 +lemma hcomplex_of_complex_minus [simp]:
  1.1914       "hcomplex_of_complex (-r) = - hcomplex_of_complex  r"
  1.1915 -apply (unfold hcomplex_of_complex_def)
  1.1916 -apply (auto simp add: hcomplex_minus)
  1.1917 -done
  1.1918 -declare hcomplex_of_complex_minus [simp]
  1.1919 +by (simp add: hcomplex_of_complex_def hcomplex_minus)
  1.1920  
  1.1921 -lemma hcomplex_of_complex_one [simp]:
  1.1922 -      "hcomplex_of_complex 1 = 1"
  1.1923 -apply (unfold hcomplex_of_complex_def hcomplex_one_def)
  1.1924 -apply auto
  1.1925 -done
  1.1926 +lemma hcomplex_of_complex_one [simp]: "hcomplex_of_complex 1 = 1"
  1.1927 +by (simp add: hcomplex_of_complex_def hcomplex_one_def)
  1.1928  
  1.1929 -lemma hcomplex_of_complex_zero [simp]:
  1.1930 -      "hcomplex_of_complex 0 = 0"
  1.1931 -apply (unfold hcomplex_of_complex_def hcomplex_zero_def)
  1.1932 -apply (simp (no_asm))
  1.1933 -done
  1.1934 +lemma hcomplex_of_complex_zero [simp]: "hcomplex_of_complex 0 = 0"
  1.1935 +by (simp add: hcomplex_of_complex_def hcomplex_zero_def)
  1.1936  
  1.1937  lemma hcomplex_of_complex_zero_iff: "(hcomplex_of_complex r = 0) = (r = 0)"
  1.1938 -apply (auto intro: FreeUltrafilterNat_P simp add: hcomplex_of_complex_def hcomplex_zero_def)
  1.1939 -done
  1.1940 +by (auto intro: FreeUltrafilterNat_P simp add: hcomplex_of_complex_def hcomplex_zero_def)
  1.1941  
  1.1942 -lemma hcomplex_of_complex_inverse:
  1.1943 +lemma hcomplex_of_complex_inverse [simp]:
  1.1944       "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)"
  1.1945  apply (case_tac "r=0")
  1.1946  apply (simp add: hcomplex_of_complex_zero)
  1.1947 -apply (rule_tac c1 = "hcomplex_of_complex r" 
  1.1948 +apply (rule_tac c1 = "hcomplex_of_complex r"
  1.1949         in hcomplex_mult_left_cancel [THEN iffD1])
  1.1950  apply (force simp add: hcomplex_of_complex_zero_iff)
  1.1951  apply (subst hcomplex_of_complex_mult [symmetric])
  1.1952 -apply (auto simp add: hcomplex_of_complex_one hcomplex_of_complex_zero_iff)
  1.1953 +apply (simp add: hcomplex_of_complex_one hcomplex_of_complex_zero_iff)
  1.1954  done
  1.1955 -declare hcomplex_of_complex_inverse [simp]
  1.1956  
  1.1957 -lemma hcomplex_of_complex_divide:
  1.1958 +lemma hcomplex_of_complex_divide [simp]:
  1.1959       "hcomplex_of_complex (z1 / z2) = hcomplex_of_complex z1 / hcomplex_of_complex z2"
  1.1960 -apply (simp (no_asm) add: hcomplex_divide_def complex_divide_def)
  1.1961 -done
  1.1962 -declare hcomplex_of_complex_divide [simp]
  1.1963 +by (simp add: hcomplex_divide_def complex_divide_def)
  1.1964  
  1.1965  lemma hRe_hcomplex_of_complex:
  1.1966     "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)"
  1.1967 -apply (unfold hcomplex_of_complex_def hypreal_of_real_def)
  1.1968 -apply (auto simp add: hRe)
  1.1969 -done
  1.1970 +by (simp add: hcomplex_of_complex_def hypreal_of_real_def hRe)
  1.1971  
  1.1972  lemma hIm_hcomplex_of_complex:
  1.1973     "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)"
  1.1974 -apply (unfold hcomplex_of_complex_def hypreal_of_real_def)
  1.1975 -apply (auto simp add: hIm)
  1.1976 -done
  1.1977 +by (simp add: hcomplex_of_complex_def hypreal_of_real_def hIm)
  1.1978  
  1.1979  lemma hcmod_hcomplex_of_complex:
  1.1980       "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)"
  1.1981 -apply (unfold hypreal_of_real_def hcomplex_of_complex_def)
  1.1982 -apply (auto simp add: hcmod)
  1.1983 -done
  1.1984 +by (simp add: hypreal_of_real_def hcomplex_of_complex_def hcmod)
  1.1985  
  1.1986  ML
  1.1987  {*
  1.1988 @@ -1710,7 +1447,6 @@
  1.1989  val hIm_add = thm"hIm_add";
  1.1990  val hcomplex_minus_congruent = thm"hcomplex_minus_congruent";
  1.1991  val hcomplex_minus = thm"hcomplex_minus";
  1.1992 -val inj_hcomplex_minus = thm"inj_hcomplex_minus";
  1.1993  val hcomplex_add_minus_left = thm"hcomplex_add_minus_left";
  1.1994  val hRe_minus = thm"hRe_minus";
  1.1995  val hIm_minus = thm"hIm_minus";
  1.1996 @@ -1728,14 +1464,11 @@
  1.1997  val hcomplex_add_mult_distrib = thm"hcomplex_add_mult_distrib";
  1.1998  val hcomplex_zero_not_eq_one = thm"hcomplex_zero_not_eq_one";
  1.1999  val hcomplex_inverse = thm"hcomplex_inverse";
  1.2000 -val HCOMPLEX_INVERSE_ZERO = thm"HCOMPLEX_INVERSE_ZERO";
  1.2001 -val HCOMPLEX_DIVISION_BY_ZERO = thm"HCOMPLEX_DIVISION_BY_ZERO";
  1.2002  val hcomplex_mult_inv_left = thm"hcomplex_mult_inv_left";
  1.2003  val hcomplex_mult_left_cancel = thm"hcomplex_mult_left_cancel";
  1.2004  val hcomplex_mult_right_cancel = thm"hcomplex_mult_right_cancel";
  1.2005  val hcomplex_add_divide_distrib = thm"hcomplex_add_divide_distrib";
  1.2006  val hcomplex_of_hypreal = thm"hcomplex_of_hypreal";
  1.2007 -val inj_hcomplex_of_hypreal = thm"inj_hcomplex_of_hypreal";
  1.2008  val hcomplex_of_hypreal_cancel_iff = thm"hcomplex_of_hypreal_cancel_iff";
  1.2009  val hcomplex_of_hypreal_minus = thm"hcomplex_of_hypreal_minus";
  1.2010  val hcomplex_of_hypreal_inverse = thm"hcomplex_of_hypreal_inverse";
  1.2011 @@ -1755,7 +1488,6 @@
  1.2012  val hcmod_hcomplex_of_hypreal = thm"hcmod_hcomplex_of_hypreal";
  1.2013  val hcomplex_of_hypreal_abs = thm"hcomplex_of_hypreal_abs";
  1.2014  val hcnj = thm"hcnj";
  1.2015 -val inj_hcnj = thm"inj_hcnj";
  1.2016  val hcomplex_hcnj_cancel_iff = thm"hcomplex_hcnj_cancel_iff";
  1.2017  val hcomplex_hcnj_hcnj = thm"hcomplex_hcnj_hcnj";
  1.2018  val hcomplex_hcnj_hcomplex_of_hypreal = thm"hcomplex_hcnj_hcomplex_of_hypreal";
  1.2019 @@ -1798,7 +1530,6 @@
  1.2020  val hcpow_minus = thm"hcpow_minus";
  1.2021  val hcmod_hcomplex_inverse = thm"hcmod_hcomplex_inverse";
  1.2022  val hcmod_divide = thm"hcmod_divide";
  1.2023 -val hcomplex_inverse_divide = thm"hcomplex_inverse_divide";
  1.2024  val hcpow_mult = thm"hcpow_mult";
  1.2025  val hcpow_zero = thm"hcpow_zero";
  1.2026  val hcpow_zero2 = thm"hcpow_zero2";