# HG changeset patch
# User huffman
# Date 1159327164 -7200
# Node ID 3ca92a58ebd7d8c3868cbb45d3f3c8a00a12f96a
# Parent  f43214ff6baf159e673b4ea2e5a0794ef47548e4
convert more proofs to transfer principle

diff -r f43214ff6baf -r 3ca92a58ebd7 src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Wed Sep 27 04:19:21 2006 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Wed Sep 27 05:19:24 2006 +0200
@@ -91,39 +91,40 @@
 
 lemma hcomplex_hRe_hIm_cancel_iff:
      "!!w z. (w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
-by (transfer, rule complex_Re_Im_cancel_iff)
+by transfer (rule complex_Re_Im_cancel_iff)
 
-lemma hcomplex_equality [intro?]: "hRe z = hRe w ==> hIm z = hIm w ==> z = w"
-by (simp add: hcomplex_hRe_hIm_cancel_iff)
+lemma hcomplex_equality [intro?]:
+  "!!z w. hRe z = hRe w ==> hIm z = hIm w ==> z = w"
+by transfer (rule complex_equality)
 
 lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0"
-by (simp add: hRe star_n_zero_num)
+by transfer (rule complex_Re_zero)
 
 lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0"
-by (simp add: hIm star_n_zero_num)
+by transfer (rule complex_Im_zero)
 
 lemma hcomplex_hRe_one [simp]: "hRe 1 = 1"
-by (simp add: hRe star_n_one_num)
+by transfer (rule complex_Re_one)
 
 lemma hcomplex_hIm_one [simp]: "hIm 1 = 0"
-by (simp add: hIm star_n_one_num star_n_zero_num)
+by transfer (rule complex_Im_one)
 
 
 subsection{*Addition for Nonstandard Complex Numbers*}
 
 lemma hRe_add: "!!x y. hRe(x + y) = hRe(x) + hRe(y)"
-by (transfer, rule complex_Re_add)
+by transfer (rule complex_Re_add)
 
 lemma hIm_add: "!!x y. hIm(x + y) = hIm(x) + hIm(y)"
-by (transfer, rule complex_Im_add)
+by transfer (rule complex_Im_add)
 
 subsection{*More Minus Laws*}
 
 lemma hRe_minus: "!!z. hRe(-z) = - hRe(z)"
-by (transfer, rule complex_Re_minus)
+by transfer (rule complex_Re_minus)
 
 lemma hIm_minus: "!!z. hIm(-z) = - hIm(z)"
-by (transfer, rule complex_Im_minus)
+by transfer (rule complex_Im_minus)
 
 lemma hcomplex_add_minus_eq_minus:
       "x + y = (0::hcomplex) ==> x = -y"
@@ -132,30 +133,30 @@
 done
 
 lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1"
-by (simp add: iii_def star_of_def star_n_mult star_n_one_num star_n_minus)
+by transfer (rule i_mult_eq2)
 
-lemma hcomplex_i_mult_left [simp]: "iii * (iii * z) = -z"
-by (simp add: mult_assoc [symmetric])
+lemma hcomplex_i_mult_left [simp]: "!!z. iii * (iii * z) = -z"
+by transfer (rule complex_i_mult_minus)
 
 lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0"
-by (simp add: iii_def star_of_def star_n_zero_num star_n_eq_iff)
+by transfer (rule complex_i_not_zero)
 
 
 subsection{*More Multiplication Laws*}
 
-lemma hcomplex_mult_minus_one [simp]: "- 1 * (z::hcomplex) = -z"
+lemma hcomplex_mult_minus_one: "- 1 * (z::hcomplex) = -z"
 by simp
 
-lemma hcomplex_mult_minus_one_right [simp]: "(z::hcomplex) * - 1 = -z"
+lemma hcomplex_mult_minus_one_right: "(z::hcomplex) * - 1 = -z"
 by simp
 
 lemma hcomplex_mult_left_cancel:
      "(c::hcomplex) \<noteq> (0::hcomplex) ==> (c*a=c*b) = (a=b)"
-by (simp add: field_mult_cancel_left)
+by simp
 
 lemma hcomplex_mult_right_cancel:
      "(c::hcomplex) \<noteq> (0::hcomplex) ==> (a*c=b*c) = (a=b)"
-by (simp add: Ring_and_Field.field_mult_cancel_right)
+by simp
 
 
 subsection{*Subraction and Division*}
@@ -175,47 +176,47 @@
 
 lemma hcomplex_of_hypreal_cancel_iff [iff]:
      "!!x y. (hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
-by (transfer, simp)
+by transfer (rule of_real_eq_iff)
 
 lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1"
-by (simp add: hcomplex_of_hypreal star_n_one_num)
+by transfer (rule of_real_1)
 
 lemma hcomplex_of_hypreal_zero [simp]: "hcomplex_of_hypreal 0 = 0"
-by (simp add: star_n_zero_num hcomplex_of_hypreal)
+by transfer (rule of_real_0)
 
 lemma hcomplex_of_hypreal_minus [simp]:
      "!!x. hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
-by (transfer, simp)
+by transfer (rule of_real_minus)
 
 lemma hcomplex_of_hypreal_inverse [simp]:
      "!!x. hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
-by (transfer, simp)
+by transfer (rule of_real_inverse)
 
 lemma hcomplex_of_hypreal_add [simp]:
      "!!x y. hcomplex_of_hypreal (x + y) =
       hcomplex_of_hypreal x + hcomplex_of_hypreal y"
-by (transfer, simp)
+by transfer (rule of_real_add)
 
 lemma hcomplex_of_hypreal_diff [simp]:
      "!!x y. hcomplex_of_hypreal (x - y) =
       hcomplex_of_hypreal x - hcomplex_of_hypreal y "
-by (transfer, simp)
+by transfer (rule of_real_diff)
 
 lemma hcomplex_of_hypreal_mult [simp]:
      "!!x y. hcomplex_of_hypreal (x * y) =
       hcomplex_of_hypreal x * hcomplex_of_hypreal y"
-by (transfer, simp)
+by transfer (rule of_real_mult)
 
 lemma hcomplex_of_hypreal_divide [simp]:
      "!!x y. hcomplex_of_hypreal(x/y) =
       hcomplex_of_hypreal x / hcomplex_of_hypreal y"
-by (transfer, simp)
+by transfer (rule of_real_divide)
 
 lemma hRe_hcomplex_of_hypreal [simp]: "!!z. hRe(hcomplex_of_hypreal z) = z"
-by (transfer, simp)
+by transfer (rule Re_complex_of_real)
 
 lemma hIm_hcomplex_of_hypreal [simp]: "!!z. hIm(hcomplex_of_hypreal z) = 0"
-by (transfer, simp)
+by transfer (rule Im_complex_of_real)
 
 lemma hcomplex_of_hypreal_epsilon_not_zero [simp]:
      "hcomplex_of_hypreal epsilon \<noteq> 0"
@@ -225,10 +226,10 @@
 subsection{*HComplex theorems*}
 
 lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x"
-by (transfer, simp)
+by transfer (rule Re)
 
 lemma hIm_HComplex [simp]: "!!x y. hIm (HComplex x y) = y"
-by (transfer, simp)
+by transfer (rule Im)
 
 text{*Relates the two nonstandard constructions*}
 lemma HComplex_eq_Abs_star_Complex:
@@ -236,8 +237,8 @@
       star_n (%n::nat. Complex (X n) (Y n))"
 by (simp add: hcomplex_hRe_hIm_cancel_iff hRe hIm)
 
-lemma hcomplex_surj [simp]: "HComplex (hRe z) (hIm z) = z"
-by (simp add: hcomplex_equality)
+lemma hcomplex_surj [simp]: "!!z. HComplex (hRe z) (hIm z) = z"
+by transfer (rule complex_surj)
 
 lemma hcomplex_induct [case_names rect(*, induct type: hcomplex*)]:
      "(\<And>x y. P (HComplex x y)) ==> P z"
@@ -250,14 +251,14 @@
 by (simp add: hcmod_def starfun)
 
 lemma hcmod_zero [simp]: "hcmod(0) = 0"
-by (simp add: star_n_zero_num hcmod)
+by (rule hnorm_zero)
 
 lemma hcmod_one [simp]: "hcmod(1) = 1"
-by (simp add: hcmod star_n_one_num)
+by (rule hnorm_one)
 
 lemma hcmod_hcomplex_of_hypreal [simp]:
   "!!x. hcmod(hcomplex_of_hypreal x) = abs x"
-by (transfer, simp)
+by transfer (rule norm_of_real)
 
 lemma hcomplex_of_hypreal_abs:
      "hcomplex_of_hypreal (abs x) =
@@ -266,54 +267,52 @@
 
 lemma HComplex_inject [simp]:
   "!!x y x' y'. HComplex x y = HComplex x' y' = (x=x' & y=y')"
-by (transfer, simp)
+by transfer (rule complex.inject)
 
 lemma HComplex_add [simp]:
   "!!x1 y1 x2 y2. HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)"
-by (transfer, simp)
+by transfer (rule complex_add)
 
 lemma HComplex_minus [simp]: "!!x y. - HComplex x y = HComplex (-x) (-y)"
-by (transfer, simp)
+by transfer (rule complex_minus)
 
 lemma HComplex_diff [simp]:
   "!!x1 y1 x2 y2. HComplex x1 y1 - HComplex x2 y2 = HComplex (x1-x2) (y1-y2)"
-by (transfer, rule complex_diff)
+by transfer (rule complex_diff)
 
 lemma HComplex_mult [simp]:
   "!!x1 y1 x2 y2. HComplex x1 y1 * HComplex x2 y2 =
    HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
-by (transfer, rule complex_mult)
+by transfer (rule complex_mult)
 
 (*HComplex_inverse is proved below*)
 
 lemma hcomplex_of_hypreal_eq: "!!r. hcomplex_of_hypreal r = HComplex r 0"
-apply (transfer)
-apply (simp add: complex_of_real_def)
-done
+by transfer (rule complex_of_real_def)
 
 lemma HComplex_add_hcomplex_of_hypreal [simp]:
-     "HComplex x y + hcomplex_of_hypreal r = HComplex (x+r) y"
-by (simp add: hcomplex_of_hypreal_eq)
+     "!!x y r. HComplex x y + hcomplex_of_hypreal r = HComplex (x+r) y"
+by transfer (rule Complex_add_complex_of_real)
 
 lemma hcomplex_of_hypreal_add_HComplex [simp]:
-     "hcomplex_of_hypreal r + HComplex x y = HComplex (r+x) y"
-by (simp add: i_def hcomplex_of_hypreal_eq)
+     "!!r x y. hcomplex_of_hypreal r + HComplex x y = HComplex (r+x) y"
+by transfer (rule complex_of_real_add_Complex)
 
 lemma HComplex_mult_hcomplex_of_hypreal:
-     "HComplex x y * hcomplex_of_hypreal r = HComplex (x*r) (y*r)"
-by (simp add: hcomplex_of_hypreal_eq)
+     "!!x y r. HComplex x y * hcomplex_of_hypreal r = HComplex (x*r) (y*r)"
+by transfer (rule Complex_mult_complex_of_real)
 
 lemma hcomplex_of_hypreal_mult_HComplex:
-     "hcomplex_of_hypreal r * HComplex x y = HComplex (r*x) (r*y)"
-by (simp add: i_def hcomplex_of_hypreal_eq)
+     "!!r x y. hcomplex_of_hypreal r * HComplex x y = HComplex (r*x) (r*y)"
+by transfer (rule complex_of_real_mult_Complex)
 
 lemma i_hcomplex_of_hypreal [simp]:
      "!!r. iii * hcomplex_of_hypreal r = HComplex 0 r"
-by (transfer, rule i_complex_of_real)
+by transfer (rule i_complex_of_real)
 
 lemma hcomplex_of_hypreal_i [simp]:
      "!!r. hcomplex_of_hypreal r * iii = HComplex 0 r"
-by (transfer, rule complex_of_real_i)
+by transfer (rule complex_of_real_i)
 
 
 subsection{*Conjugation*}
@@ -322,115 +321,115 @@
 by (simp add: hcnj_def starfun)
 
 lemma hcomplex_hcnj_cancel_iff [iff]: "!!x y. (hcnj x = hcnj y) = (x = y)"
-by (transfer, rule complex_cnj_cancel_iff)
+by transfer (rule complex_cnj_cancel_iff)
 
 lemma hcomplex_hcnj_hcnj [simp]: "!!z. hcnj (hcnj z) = z"
-by (transfer, rule complex_cnj_cnj)
+by transfer (rule complex_cnj_cnj)
 
 lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]:
      "!!x. hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
-by (transfer, rule complex_cnj_complex_of_real)
+by transfer (rule complex_cnj_complex_of_real)
 
 lemma hcomplex_hmod_hcnj [simp]: "!!z. hcmod (hcnj z) = hcmod z"
-by (transfer, rule complex_mod_cnj)
+by transfer (rule complex_mod_cnj)
 
 lemma hcomplex_hcnj_minus: "!!z. hcnj (-z) = - hcnj z"
-by (transfer, rule complex_cnj_minus)
+by transfer (rule complex_cnj_minus)
 
 lemma hcomplex_hcnj_inverse: "!!z. hcnj(inverse z) = inverse(hcnj z)"
-by (transfer, rule complex_cnj_inverse)
+by transfer (rule complex_cnj_inverse)
 
 lemma hcomplex_hcnj_add: "!!w z. hcnj(w + z) = hcnj(w) + hcnj(z)"
-by (transfer, rule complex_cnj_add)
+by transfer (rule complex_cnj_add)
 
 lemma hcomplex_hcnj_diff: "!!w z. hcnj(w - z) = hcnj(w) - hcnj(z)"
-by (transfer, rule complex_cnj_diff)
+by transfer (rule complex_cnj_diff)
 
 lemma hcomplex_hcnj_mult: "!!w z. hcnj(w * z) = hcnj(w) * hcnj(z)"
-by (transfer, rule complex_cnj_mult)
+by transfer (rule complex_cnj_mult)
 
 lemma hcomplex_hcnj_divide: "!!w z. hcnj(w / z) = (hcnj w)/(hcnj z)"
-by (transfer, rule complex_cnj_divide)
+by transfer (rule complex_cnj_divide)
 
 lemma hcnj_one [simp]: "hcnj 1 = 1"
-by (transfer, rule complex_cnj_one)
+by transfer (rule complex_cnj_one)
 
 lemma hcomplex_hcnj_zero [simp]: "hcnj 0 = 0"
-by (transfer, rule complex_cnj_zero)
+by transfer (rule complex_cnj_zero)
 
 lemma hcomplex_hcnj_zero_iff [iff]: "!!z. (hcnj z = 0) = (z = 0)"
-by (transfer, rule complex_cnj_zero_iff)
+by transfer (rule complex_cnj_zero_iff)
 
 lemma hcomplex_mult_hcnj:
      "!!z. z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
-by (transfer, rule complex_mult_cnj)
+by transfer (rule complex_mult_cnj)
 
 
 subsection{*More Theorems about the Function @{term hcmod}*}
 
 lemma hcomplex_hcmod_eq_zero_cancel [simp]: "!!x. (hcmod x = 0) = (x = 0)"
-by (transfer, rule complex_mod_eq_zero_cancel)
+by transfer (rule complex_mod_eq_zero_cancel)
 
 lemma hcmod_hcomplex_of_hypreal_of_nat [simp]:
      "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
-by (simp add: abs_if linorder_not_less)
+by simp
 
 lemma hcmod_hcomplex_of_hypreal_of_hypnat [simp]:
      "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"
-by (simp add: abs_if linorder_not_less)
+by simp
 
 lemma hcmod_minus [simp]: "!!x. hcmod (-x) = hcmod(x)"
-by (transfer, rule complex_mod_minus)
+by transfer (rule complex_mod_minus)
 
 lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
-by (transfer, rule complex_mod_mult_cnj)
+by transfer (rule complex_mod_mult_cnj)
 
 lemma hcmod_ge_zero [simp]: "!!x. (0::hypreal) \<le> hcmod x"
-by (transfer, rule complex_mod_ge_zero)
+by transfer (rule complex_mod_ge_zero)
 
 lemma hrabs_hcmod_cancel [simp]: "abs(hcmod x) = hcmod x"
 by (simp add: abs_if linorder_not_less)
 
 lemma hcmod_mult: "!!x y. hcmod(x*y) = hcmod(x) * hcmod(y)"
-by (transfer, rule complex_mod_mult)
+by transfer (rule complex_mod_mult)
 
 lemma hcmod_add_squared_eq:
   "!!x y. hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)"
-by (transfer, rule complex_mod_add_squared_eq)
+by transfer (rule complex_mod_add_squared_eq)
 
 lemma hcomplex_hRe_mult_hcnj_le_hcmod [simp]:
   "!!x y. hRe(x * hcnj y) \<le> hcmod(x * hcnj y)"
-by (transfer, simp)
+by transfer (rule complex_Re_mult_cnj_le_cmod)
 
 lemma hcomplex_hRe_mult_hcnj_le_hcmod2 [simp]:
   "!!x y. hRe(x * hcnj y) \<le> hcmod(x * y)"
-by (transfer, simp)
+by transfer (rule complex_Re_mult_cnj_le_cmod2)
 
 lemma hcmod_triangle_squared [simp]:
   "!!x y. hcmod (x + y) ^ 2 \<le> (hcmod(x) + hcmod(y)) ^ 2"
-by (transfer, simp)
+by transfer (rule complex_mod_triangle_squared)
 
 lemma hcmod_triangle_ineq [simp]:
   "!!x y. hcmod (x + y) \<le> hcmod(x) + hcmod(y)"
-by (transfer, simp)
+by transfer (rule complex_mod_triangle_ineq)
 
 lemma hcmod_triangle_ineq2 [simp]:
   "!!a b. hcmod(b + a) - hcmod b \<le> hcmod a"
-by (transfer, simp)
+by transfer (rule complex_mod_triangle_ineq2)
 
 lemma hcmod_diff_commute: "!!x y. hcmod (x - y) = hcmod (y - x)"
-by (transfer, rule complex_mod_diff_commute)
+by transfer (rule complex_mod_diff_commute)
 
 lemma hcmod_add_less:
   "!!x y r s. [| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s"
-by (transfer, rule complex_mod_add_less)
+by transfer (rule complex_mod_add_less)
 
 lemma hcmod_mult_less:
   "!!x y r s. [| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s"
-by (transfer, rule complex_mod_mult_less)
+by transfer (rule complex_mod_mult_less)
 
 lemma hcmod_diff_ineq [simp]: "!!a b. hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
-by (transfer, simp)
+by transfer (rule complex_mod_diff_ineq)
 
 
 subsection{*A Few Nonlinear Theorems*}
@@ -440,16 +439,16 @@
 
 lemma hcomplex_of_hypreal_hyperpow:
      "!!x n. hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
-by (transfer, rule complex_of_real_pow)
+by transfer (rule complex_of_real_pow)
 
 lemma hcmod_hcpow: "!!x n. hcmod(x hcpow n) = hcmod(x) pow n"
-by (transfer, rule complex_mod_complexpow)
+by transfer (rule complex_mod_complexpow)
 
 lemma hcmod_hcomplex_inverse: "!!x. hcmod(inverse x) = inverse(hcmod x)"
-by (transfer, rule complex_mod_inverse)
+by transfer (rule complex_mod_inverse)
 
-lemma hcmod_divide: "hcmod(x/y) = hcmod(x)/(hcmod y)"
-by (simp add: divide_inverse hcmod_mult hcmod_hcomplex_inverse)
+lemma hcmod_divide: "!!x y. hcmod(x/y) = hcmod(x)/(hcmod y)"
+by transfer (rule norm_divide)
 
 
 subsection{*Exponentiation*}
@@ -461,43 +460,36 @@
 by (rule power_Suc)
 
 lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = - 1"
-by (simp add: power2_eq_square)
-
+by transfer (rule complexpow_i_squared)
 
 lemma hcomplex_of_hypreal_pow:
-     "hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"
-apply (induct_tac "n")
-apply (auto simp add: hcomplex_of_hypreal_mult [symmetric])
-done
+     "!!x. hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"
+by transfer (rule of_real_power)
 
-lemma hcomplex_hcnj_pow: "hcnj(z ^ n) = hcnj(z) ^ n"
-apply (induct_tac "n")
-apply (auto simp add: hcomplex_hcnj_mult)
-done
+lemma hcomplex_hcnj_pow: "!!z. hcnj(z ^ n) = hcnj(z) ^ n"
+by transfer (rule complex_cnj_pow)
 
-lemma hcmod_hcomplexpow: "hcmod(x ^ n) = hcmod(x) ^ n"
-apply (induct_tac "n")
-apply (auto simp add: hcmod_mult)
-done
+lemma hcmod_hcomplexpow: "!!x. hcmod(x ^ n) = hcmod(x) ^ n"
+by transfer (rule norm_power)
 
 lemma hcpow_minus:
      "!!x n. (-x::hcomplex) hcpow n =
       (if ( *p* even) n then (x hcpow n) else -(x hcpow n))"
-by (transfer, rule neg_power_if)
+by transfer (rule neg_power_if)
 
 lemma hcpow_mult:
   "!!r s n. ((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
-by (transfer, rule power_mult_distrib)
+by transfer (rule power_mult_distrib)
 
 lemma hcpow_zero [simp]: "!!n. 0 hcpow (n + 1) = 0"
-by (transfer, simp)
+by transfer simp
 
-lemma hcpow_zero2 [simp]: "0 hcpow (hSuc n) = 0"
+lemma hcpow_zero2 [simp]: "!!n. 0 hcpow (hSuc n) = 0"
 by (simp add: hSuc_def)
 
 lemma hcpow_not_zero [simp,intro]:
   "!!r n. r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)"
-by (transfer, simp)
+by transfer (rule field_power_not_zero)
 
 lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0"
 by (blast intro: ccontr dest: hcpow_not_zero)
@@ -511,19 +503,19 @@
 by (simp add: hsgn_def starfun)
 
 lemma hsgn_zero [simp]: "hsgn 0 = 0"
-by (simp add: star_n_zero_num hsgn)
+by transfer (rule sgn_zero)
 
 lemma hsgn_one [simp]: "hsgn 1 = 1"
-by (simp add: star_n_one_num hsgn)
+by transfer (rule sgn_one)
 
 lemma hsgn_minus: "!!z. hsgn (-z) = - hsgn(z)"
-by (transfer, rule sgn_minus)
+by transfer (rule sgn_minus)
 
 lemma hsgn_eq: "!!z. hsgn z = z / hcomplex_of_hypreal (hcmod z)"
-by (transfer, rule sgn_eq)
+by transfer (rule sgn_eq)
 
 lemma hcmod_i: "!!x y. hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)"
-by (transfer, rule complex_mod)
+by transfer (rule complex_mod)
 
 lemma hcomplex_eq_cancel_iff1 [simp]:
      "(hcomplex_of_hypreal xa = HComplex x y) = (xa = x & y = 0)"
@@ -533,23 +525,23 @@
      "(HComplex x y = hcomplex_of_hypreal xa) = (x = xa & y = 0)"
 by (simp add: hcomplex_of_hypreal_eq)
 
-lemma HComplex_eq_0 [simp]: "(HComplex x y = 0) = (x = 0 & y = 0)"
-by (insert hcomplex_eq_cancel_iff2 [of _ _ 0], simp)
+lemma HComplex_eq_0 [simp]: "!!x y. (HComplex x y = 0) = (x = 0 & y = 0)"
+by transfer (rule Complex_eq_0)
 
-lemma HComplex_eq_1 [simp]: "(HComplex x y = 1) = (x = 1 & y = 0)"
-by (insert hcomplex_eq_cancel_iff2 [of _ _ 1], simp)
+lemma HComplex_eq_1 [simp]: "!!x y. (HComplex x y = 1) = (x = 1 & y = 0)"
+by transfer (rule Complex_eq_1)
 
 lemma i_eq_HComplex_0_1: "iii = HComplex 0 1"
-by (insert hcomplex_of_hypreal_i [of 1], simp)
+by transfer (rule i_def [THEN meta_eq_to_obj_eq])
 
-lemma HComplex_eq_i [simp]: "(HComplex x y = iii) = (x = 0 & y = 1)"
-by (simp add: i_eq_HComplex_0_1) 
+lemma HComplex_eq_i [simp]: "!!x y. (HComplex x y = iii) = (x = 0 & y = 1)"
+by transfer (rule Complex_eq_i)
 
 lemma hRe_hsgn [simp]: "!!z. hRe(hsgn z) = hRe(z)/hcmod z"
-by (transfer, simp)
+by transfer (rule Re_sgn)
 
 lemma hIm_hsgn [simp]: "!!z. hIm(hsgn z) = hIm(z)/hcmod z"
-by (transfer, simp)
+by transfer (rule Im_sgn)
 
 (*????move to RealDef????*)
 lemma real_two_squares_add_zero_iff [simp]: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"
@@ -559,26 +551,26 @@
      "!!x y. inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
       hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
       iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
-by (transfer, rule complex_inverse_complex_split)
+by transfer (rule complex_inverse_complex_split)
 
 lemma HComplex_inverse:
      "!!x y. inverse (HComplex x y) =
       HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
-by (transfer, rule complex_inverse)
+by transfer (rule complex_inverse)
 
 lemma hRe_mult_i_eq[simp]:
     "!!y. hRe (iii * hcomplex_of_hypreal y) = 0"
-by (transfer, simp)
+by transfer simp
 
 lemma hIm_mult_i_eq [simp]:
     "!!y. hIm (iii * hcomplex_of_hypreal y) = y"
-by (transfer, simp)
+by transfer simp
 
 lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = abs y"
-by (transfer, simp)
+by transfer simp
 
-lemma hcmod_mult_i2 [simp]: "hcmod (hcomplex_of_hypreal y * iii) = abs y"
-by (simp only: hcmod_mult_i mult_commute)
+lemma hcmod_mult_i2 [simp]: "!!y. hcmod (hcomplex_of_hypreal y * iii) = abs y"
+by transfer simp
 
 (*---------------------------------------------------------------------------*)
 (*  harg                                                                     *)
@@ -589,20 +581,19 @@
 
 lemma cos_harg_i_mult_zero_pos:
      "!!y. 0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
-by (transfer, rule cos_arg_i_mult_zero_pos)
+by transfer (rule cos_arg_i_mult_zero_pos)
 
 lemma cos_harg_i_mult_zero_neg:
      "!!y. y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
-by (transfer, rule cos_arg_i_mult_zero_neg)
+by transfer (rule cos_arg_i_mult_zero_neg)
 
 lemma cos_harg_i_mult_zero [simp]:
-     "y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
-by (auto simp add: linorder_neq_iff
-                   cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg)
+     "!!y. y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
+by transfer (rule cos_arg_i_mult_zero)
 
 lemma hcomplex_of_hypreal_zero_iff [simp]:
      "!!y. (hcomplex_of_hypreal y = 0) = (y = 0)"
-by (transfer, simp)
+by transfer (rule of_real_eq_0_iff)
 
 
 subsection{*Polar Form for Nonstandard Complex Numbers*}
@@ -621,7 +612,7 @@
 
 lemma hcomplex_split_polar:
   "!!z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
-by (transfer, rule complex_split_polar)
+by transfer (rule complex_split_polar)
 
 lemma hcis: "hcis (star_n X) = star_n (%n. cis (X n))"
 by (simp add: hcis_def starfun)
@@ -630,69 +621,68 @@
    "!!a. hcis a =
     (hcomplex_of_hypreal(( *f* cos) a) +
     iii * hcomplex_of_hypreal(( *f* sin) a))"
-by (transfer, simp add: cis_def)
+by transfer (simp add: cis_def)
 
 lemma hrcis: "hrcis (star_n X) (star_n Y) = star_n (%n. rcis (X n) (Y n))"
 by (simp add: hrcis_def starfun2_star_n)
 
 lemma hrcis_Ex: "!!z. \<exists>r a. z = hrcis r a"
-by (transfer, rule rcis_Ex)
+by transfer (rule rcis_Ex)
 
 lemma hRe_hcomplex_polar [simp]:
-     "hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
+  "!!r a. hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
       r * ( *f* cos) a"
-by (simp add: hcomplex_of_hypreal_mult_HComplex)
+by transfer simp
 
 lemma hRe_hrcis [simp]: "!!r a. hRe(hrcis r a) = r * ( *f* cos) a"
-by (transfer, rule Re_rcis)
+by transfer (rule Re_rcis)
 
 lemma hIm_hcomplex_polar [simp]:
-     "hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
+  "!!r a. hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
       r * ( *f* sin) a"
-by (simp add: hcomplex_of_hypreal_mult_HComplex)
+by transfer simp
 
 lemma hIm_hrcis [simp]: "!!r a. hIm(hrcis r a) = r * ( *f* sin) a"
-by (transfer, rule Im_rcis)
-
+by transfer (rule Im_rcis)
 
 lemma hcmod_unit_one [simp]:
      "!!a. hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
-by (transfer, simp)
+by transfer (rule cmod_unit_one)
 
 lemma hcmod_complex_polar [simp]:
-     "hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
+  "!!r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
       abs r"
-by (simp only: hcmod_mult hcmod_unit_one, simp)
+by transfer (rule cmod_complex_polar)
 
 lemma hcmod_hrcis [simp]: "!!r a. hcmod(hrcis r a) = abs r"
-by (transfer, rule complex_mod_rcis)
+by transfer (rule complex_mod_rcis)
 
 (*---------------------------------------------------------------------------*)
 (*  (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b)                *)
 (*---------------------------------------------------------------------------*)
 
 lemma hcis_hrcis_eq: "!!a. hcis a = hrcis 1 a"
-by (transfer, rule cis_rcis_eq)
+by transfer (rule cis_rcis_eq)
 declare hcis_hrcis_eq [symmetric, simp]
 
 lemma hrcis_mult:
   "!!a b r1 r2. hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
-by (transfer, rule rcis_mult)
+by transfer (rule rcis_mult)
 
 lemma hcis_mult: "!!a b. hcis a * hcis b = hcis (a + b)"
-by (transfer, rule cis_mult)
+by transfer (rule cis_mult)
 
 lemma hcis_zero [simp]: "hcis 0 = 1"
-by (transfer, rule cis_zero)
+by transfer (rule cis_zero)
 
 lemma hrcis_zero_mod [simp]: "!!a. hrcis 0 a = 0"
-by (transfer, rule rcis_zero_mod)
+by transfer (rule rcis_zero_mod)
 
 lemma hrcis_zero_arg [simp]: "!!r. hrcis r 0 = hcomplex_of_hypreal r"
-by (transfer, rule rcis_zero_arg)
+by transfer (rule rcis_zero_arg)
 
-lemma hcomplex_i_mult_minus [simp]: "iii * (iii * x) = - x"
-by (simp add: mult_assoc [symmetric])
+lemma hcomplex_i_mult_minus [simp]: "!!x. iii * (iii * x) = - x"
+by transfer (rule complex_i_mult_minus)
 
 lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x"
 by simp
@@ -706,19 +696,21 @@
 apply (rule cis_real_of_nat_Suc_mult)
 done
 
-lemma NSDeMoivre: "(hcis a) ^ n = hcis (hypreal_of_nat n * a)"
-apply (induct_tac "n")
-apply (simp_all add: hcis_hypreal_of_nat_Suc_mult)
+lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)"
+apply (unfold hypreal_of_nat_def)
+apply transfer
+apply (fold real_of_nat_def)
+apply (rule DeMoivre)
 done
 
 lemma hcis_hypreal_of_hypnat_Suc_mult:
      "!! a n. hcis (hypreal_of_hypnat (n + 1) * a) =
       hcis a * hcis (hypreal_of_hypnat n * a)"
-by (transfer, simp add: cis_real_of_nat_Suc_mult)
+by transfer (simp add: cis_real_of_nat_Suc_mult)
 
 lemma NSDeMoivre_ext:
   "!!a n. (hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)"
-by (transfer, rule DeMoivre)
+by transfer (rule DeMoivre)
 
 lemma NSDeMoivre2:
   "!!a r. (hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"
@@ -730,19 +722,19 @@
 
 lemma DeMoivre2_ext:
   "!! a r n. (hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)"
-by (transfer, rule DeMoivre2)
+by transfer (rule DeMoivre2)
 
 lemma hcis_inverse [simp]: "!!a. inverse(hcis a) = hcis (-a)"
-by (transfer, simp)
+by transfer (rule cis_inverse)
 
 lemma hrcis_inverse: "!!a r. inverse(hrcis r a) = hrcis (inverse r) (-a)"
-by (transfer, simp add: rcis_inverse inverse_eq_divide [symmetric])
+by transfer (simp add: rcis_inverse inverse_eq_divide [symmetric])
 
 lemma hRe_hcis [simp]: "!!a. hRe(hcis a) = ( *f* cos) a"
-by (transfer, rule Re_cis)
+by transfer (rule Re_cis)
 
 lemma hIm_hcis [simp]: "!!a. hIm(hcis a) = ( *f* sin) a"
-by (transfer, rule Im_cis)
+by transfer (rule Im_cis)
 
 lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
 by (simp add: NSDeMoivre)
@@ -757,7 +749,7 @@
 by (simp add: NSDeMoivre_ext)
 
 lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)"
-by (transfer, rule expi_add)
+by transfer (rule expi_add)
 
 
 subsection{*@{term hcomplex_of_complex}: the Injection from
@@ -767,34 +759,34 @@
 by (rule inj_onI, simp)
 
 lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
-by (simp add: iii_def)
+by (rule iii_def)
 
 lemma hRe_hcomplex_of_complex:
    "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)"
-by (transfer, rule refl)
+by transfer (rule refl)
 
 lemma hIm_hcomplex_of_complex:
    "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)"
-by (transfer, rule refl)
+by transfer (rule refl)
 
 lemma hcmod_hcomplex_of_complex:
      "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)"
-by (transfer, rule refl)
+by transfer (rule refl)
 
 
 subsection{*Numerals and Arithmetic*}
 
 lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int w"
-by (transfer, rule number_of_eq [THEN eq_reflection])
+by transfer (rule number_of_eq [THEN eq_reflection])
 
 lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: 
      "hcomplex_of_hypreal (hypreal_of_real x) =  
       hcomplex_of_complex (complex_of_real x)"
-by (transfer, rule refl)
+by transfer (rule refl)
 
 lemma hcomplex_hypreal_number_of: 
   "hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)"
-by (transfer, rule complex_number_of [symmetric])
+by transfer (rule complex_number_of [symmetric])
 
 text{*This theorem is necessary because theorems such as
    @{text iszero_number_of_0} only hold for ordered rings. They cannot
@@ -909,18 +901,18 @@
 
 lemma hcomplex_number_of_hcnj [simp]:
      "hcnj (number_of v :: hcomplex) = number_of v"
-by (transfer, rule complex_number_of_cnj)
+by transfer (rule complex_number_of_cnj)
 
 lemma hcomplex_number_of_hcmod [simp]: 
       "hcmod(number_of v :: hcomplex) = abs (number_of v :: hypreal)"
-by (transfer, rule complex_number_of_cmod)
+by transfer (rule complex_number_of_cmod)
 
 lemma hcomplex_number_of_hRe [simp]: 
       "hRe(number_of v :: hcomplex) = number_of v"
-by (transfer, simp)
+by transfer (rule complex_number_of_Re)
 
 lemma hcomplex_number_of_hIm [simp]: 
       "hIm(number_of v :: hcomplex) = 0"
-by (transfer, simp)
+by transfer (rule complex_number_of_Im)
 
 end