# HG changeset patch
# User paulson
# Date 1079344709 -3600
# Node ID c7674b7034f5c13b9a32869afc3ce21bf37d26dd
# Parent  6be497cacab58a2af85c0a45f68ecc0bdc0a3799
heavy tidying

diff -r 6be497cacab5 -r c7674b7034f5 src/HOL/Complex/CLim.thy
--- a/src/HOL/Complex/CLim.thy	Mon Mar 15 10:46:19 2004 +0100
+++ b/src/HOL/Complex/CLim.thy	Mon Mar 15 10:58:29 2004 +0100
@@ -1,10 +1,11 @@
 (*  Title       : CLim.thy
     Author      : Jacques D. Fleuriot
     Copyright   : 2001 University of Edinburgh
-    Description : A first theory of limits, continuity and
-                  differentiation for complex functions
+    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
 *)
 
+header{*Limits, Continuity and Differentiation for Complex Functions*}
+
 theory CLim = CSeries:
 
 (*not in simpset?*)
@@ -13,7 +14,7 @@
 (*??generalize*)
 lemma lemma_complex_mult_inverse_squared [simp]:
      "x \<noteq> (0::complex) \<Longrightarrow> (x * inverse(x) ^ 2) = inverse x"
-by (auto simp add: numeral_2_eq_2)
+by (simp add: numeral_2_eq_2)
 
 text{*Changing the quantified variable. Install earlier?*}
 lemma all_shift: "(\<forall>x::'a::ring. P x) = (\<forall>x. P (x-a))";
@@ -109,21 +110,17 @@
 subsection{*Limit of Complex to Complex Function*}
 
 lemma NSCLIM_NSCRLIM_Re: "f -- a --NSC> L ==> (%x. Re(f x)) -- a --NSCR> Re(L)"
-apply (unfold NSCLIM_def NSCRLIM_def)
-apply (rule eq_Abs_hcomplex [of x])
-apply (auto simp add: starfunC_approx_Re_Im_iff hRe_hcomplex_of_complex)
-done
+by (simp add: NSCLIM_def NSCRLIM_def starfunC_approx_Re_Im_iff 
+              hRe_hcomplex_of_complex)
+
 
-lemma NSCLIM_NSCRLIM_Im:
-   "f -- a --NSC> L ==> (%x. Im(f x)) -- a --NSCR> Im(L)"
-apply (unfold NSCLIM_def NSCRLIM_def)
-apply (rule eq_Abs_hcomplex [of x])
-apply (auto simp add: starfunC_approx_Re_Im_iff hIm_hcomplex_of_complex)
-done
+lemma NSCLIM_NSCRLIM_Im: "f -- a --NSC> L ==> (%x. Im(f x)) -- a --NSCR> Im(L)"
+by (simp add: NSCLIM_def NSCRLIM_def starfunC_approx_Re_Im_iff 
+              hIm_hcomplex_of_complex)
 
 lemma CLIM_NSCLIM:
       "f -- x --C> L ==> f -- x --NSC> L"
-apply (unfold CLIM_def NSCLIM_def capprox_def, auto)
+apply (simp add: CLIM_def NSCLIM_def capprox_def, auto)
 apply (rule_tac z = xa in eq_Abs_hcomplex)
 apply (auto simp add: hcomplex_of_complex_def starfunC hcomplex_diff 
          CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff)
@@ -167,14 +164,18 @@
 
 lemma NSCLIM_CLIM:
      "f -- x --NSC> L ==> f -- x --C> L"
-apply (unfold CLIM_def NSCLIM_def)
+apply (simp add: CLIM_def NSCLIM_def)
 apply (rule ccontr) 
-apply (auto simp add: eq_Abs_hcomplex_ALL starfunC CInfinitesimal_capprox_minus [symmetric] hcomplex_diff CInfinitesimal_hcmod_iff hcomplex_of_complex_def Infinitesimal_FreeUltrafilterNat_iff hcmod)
+apply (auto simp add: eq_Abs_hcomplex_ALL starfunC 
+            CInfinitesimal_capprox_minus [symmetric] hcomplex_diff
+            CInfinitesimal_hcmod_iff hcomplex_of_complex_def 
+            Infinitesimal_FreeUltrafilterNat_iff hcmod)
 apply (simp add: linorder_not_less)
 apply (drule lemma_skolemize_CLIM2, safe)
 apply (drule_tac x = X in spec, auto)
 apply (drule lemma_csimp [THEN complex_seq_to_hcomplex_CInfinitesimal])
-apply (simp add: CInfinitesimal_hcmod_iff hcomplex_of_complex_def Infinitesimal_FreeUltrafilterNat_iff hcomplex_diff hcmod, blast)
+apply (simp add: CInfinitesimal_hcmod_iff hcomplex_of_complex_def 
+            Infinitesimal_FreeUltrafilterNat_iff hcomplex_diff hcmod,  blast)
 apply (drule_tac x = r in spec, clarify)
 apply (drule FreeUltrafilterNat_all, ultra, arith)
 done
@@ -188,9 +189,12 @@
 subsection{*Limit of Complex to Real Function*}
 
 lemma CRLIM_NSCRLIM: "f -- x --CR> L ==> f -- x --NSCR> L"
-apply (unfold CRLIM_def NSCRLIM_def capprox_def, auto)
+apply (simp add: CRLIM_def NSCRLIM_def capprox_def, auto)
 apply (rule_tac z = xa in eq_Abs_hcomplex)
-apply (auto simp add: hcomplex_of_complex_def starfunCR hcomplex_diff CInfinitesimal_hcmod_iff hcmod hypreal_diff Infinitesimal_FreeUltrafilterNat_iff Infinitesimal_approx_minus [symmetric] hypreal_of_real_def)
+apply (auto simp add: hcomplex_of_complex_def starfunCR hcomplex_diff
+              CInfinitesimal_hcmod_iff hcmod hypreal_diff
+              Infinitesimal_FreeUltrafilterNat_iff
+              Infinitesimal_approx_minus [symmetric] hypreal_of_real_def)
 apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe)
 apply (drule_tac x = u in spec, auto)
 apply (drule_tac x = s in spec, auto, ultra)
@@ -223,7 +227,7 @@
 by auto
 
 lemma NSCRLIM_CRLIM: "f -- x --NSCR> L ==> f -- x --CR> L"
-apply (unfold CRLIM_def NSCRLIM_def capprox_def)
+apply (simp add: CRLIM_def NSCRLIM_def capprox_def)
 apply (rule ccontr) 
 apply (auto simp add: eq_Abs_hcomplex_ALL starfunCR hcomplex_diff 
              hcomplex_of_complex_def hypreal_diff CInfinitesimal_hcmod_iff 
@@ -252,10 +256,10 @@
 by (auto dest: NSCLIM_NSCRLIM_Im simp add: CLIM_NSCLIM_iff CRLIM_NSCRLIM_iff [symmetric])
 
 lemma CLIM_cnj: "f -- a --C> L ==> (%x. cnj (f x)) -- a --C> cnj L"
-by (auto simp add: CLIM_def complex_cnj_diff [symmetric])
+by (simp add: CLIM_def complex_cnj_diff [symmetric])
 
 lemma CLIM_cnj_iff: "((%x. cnj (f x)) -- a --C> cnj L) = (f -- a --C> L)"
-by (auto simp add: CLIM_def complex_cnj_diff [symmetric])
+by (simp add: CLIM_def complex_cnj_diff [symmetric])
 
 (*** NSLIM_add hence CLIM_add *)
 
@@ -302,7 +306,7 @@
 lemma NSCLIM_diff:
      "[| f -- x --NSC> l; g -- x --NSC> m |]
       ==> (%x. f(x) - g(x)) -- x --NSC> (l - m)"
-by (simp add: complex_diff_def NSCLIM_add NSCLIM_minus)
+by (simp add: diff_minus NSCLIM_add NSCLIM_minus)
 
 lemma CLIM_diff:
      "[| f -- x --C> l; g -- x --C> m |]
@@ -314,9 +318,9 @@
 lemma NSCLIM_inverse:
      "[| f -- a --NSC> L;  L \<noteq> 0 |]
       ==> (%x. inverse(f(x))) -- a --NSC> (inverse L)"
-apply (unfold NSCLIM_def, clarify)
+apply (simp add: NSCLIM_def, clarify)
 apply (drule spec)
-apply (auto simp add: hcomplex_of_complex_capprox_inverse)
+apply (force simp add: hcomplex_of_complex_capprox_inverse)
 done
 
 lemma CLIM_inverse:
@@ -327,9 +331,9 @@
 (*** NSCLIM_zero, CLIM_zero, etc. ***)
 
 lemma NSCLIM_zero: "f -- a --NSC> l ==> (%x. f(x) - l) -- a --NSC> 0"
+apply (simp add: diff_minus)
 apply (rule_tac a1 = l in right_minus [THEN subst])
-apply (unfold complex_diff_def)
-apply (rule NSCLIM_add, auto)
+apply (rule NSCLIM_add, auto) 
 done
 
 lemma CLIM_zero: "f -- a --C> l ==> (%x. f(x) - l) -- a --C> 0"
@@ -412,7 +416,7 @@
 (* so this is nicer nonstandard proof *)
 lemma NSCLIM_NSCRLIM_iff2:
      "(f -- x --NSC> L) = ((%y. cmod(f y - L)) -- x --NSCR> 0)"
-by (auto simp add: CRLIM_NSCRLIM_iff [symmetric] CLIM_CRLIM_iff CLIM_NSCLIM_iff [symmetric])
+by (simp add: CRLIM_NSCRLIM_iff [symmetric] CLIM_CRLIM_iff CLIM_NSCLIM_iff [symmetric])
 
 lemma NSCLIM_NSCRLIM_Re_Im_iff:
      "(f -- a --NSC> L) = ((%x. Re(f x)) -- a --NSCR> Re(L) &
@@ -421,7 +425,7 @@
 apply (auto simp add: NSCLIM_def NSCRLIM_def)
 apply (auto dest!: spec) 
 apply (rule_tac z = x in eq_Abs_hcomplex)
-apply (auto simp add: capprox_approx_iff starfunC hcomplex_of_complex_def starfunCR hypreal_of_real_def)
+apply (simp add: capprox_approx_iff starfunC hcomplex_of_complex_def starfunCR hypreal_of_real_def)
 done
 
 lemma CLIM_CRLIM_Re_Im_iff:
@@ -501,7 +505,7 @@
 
 
 lemma isContc_o: "[| isContc f a; isContc g (f a) |] ==> isContc (g o f) a"
-by (auto simp add: isNSContc_isContc_iff [symmetric] isNSContc_def starfunC_o [symmetric])
+by (simp add: isNSContc_isContc_iff [symmetric] isNSContc_def starfunC_o [symmetric])
 
 lemma isContc_o2:
      "[| isContc f a; isContc g (f a) |] ==> isContc (%x. g (f x)) a"
@@ -523,7 +527,7 @@
 
 lemma isContc_diff:
       "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) - g(x)) a"
-apply (simp add: complex_diff_def)
+apply (simp add: diff_minus)
 apply (auto intro: isContc_add isContc_minus)
 done
 
@@ -571,7 +575,7 @@
                     isNSContCR_def) 
 
 lemma isContCR_cmod [simp]: "isContCR cmod (a)"
-by (auto simp add: isNSContCR_isContCR_iff [symmetric])
+by (simp add: isNSContCR_isContCR_iff [symmetric])
 
 lemma isContc_isContCR_Re: "isContc f a ==> isContCR (%x. Re (f x)) a"
 by (simp add: isContc_def isContCR_def CLIM_CRLIM_Re)
@@ -746,7 +750,7 @@
 
 lemma NSCDERIV_cmult: "NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c*D"
 apply (simp add: times_divide_eq_right [symmetric] NSCDERIV_NSCLIM_iff 
-                 minus_mult_right right_distrib [symmetric] complex_diff_def
+                 minus_mult_right right_distrib [symmetric] diff_minus
             del: times_divide_eq_right minus_mult_right [symmetric])
 apply (erule NSCLIM_const [THEN NSCLIM_mult])
 done
@@ -755,7 +759,7 @@
 by (simp add: NSCDERIV_cmult NSCDERIV_CDERIV_iff [symmetric])
 
 lemma NSCDERIV_minus: "NSCDERIV f x :> D ==> NSCDERIV (%x. -(f x)) x :> -D"
-apply (simp add: NSCDERIV_NSCLIM_iff complex_diff_def)
+apply (simp add: NSCDERIV_NSCLIM_iff diff_minus)
 apply (rule_tac t = "f x" in minus_minus [THEN subst])
 apply (simp (no_asm_simp) add: minus_add_distrib [symmetric]
             del: minus_add_distrib minus_minus)
@@ -778,12 +782,12 @@
 lemma NSCDERIV_diff:
      "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |]
       ==> NSCDERIV (%x. f x - g x) x :> Da - Db"
-by (simp add: complex_diff_def NSCDERIV_add_minus)
+by (simp add: diff_minus NSCDERIV_add_minus)
 
 lemma CDERIV_diff:
      "[| CDERIV f x :> Da; CDERIV g x :> Db |]
        ==> CDERIV (%x. f x - g x) x :> Da - Db"
-by (simp add: complex_diff_def CDERIV_add_minus)
+by (simp add: diff_minus CDERIV_add_minus)
 
 
 subsection{*Chain Rule*}
@@ -823,7 +827,7 @@
 	 - hcomplex_of_complex (f (g x))) /
 	(( *fc* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex (g x))
 	   @c= hcomplex_of_complex (Da)"
-by (auto simp add: NSCDERIV_NSCLIM_iff2 NSCLIM_def)
+by (simp add: NSCDERIV_NSCLIM_iff2 NSCLIM_def)
 
 (*--------------------------------------------------*)
 (* from other version of differentiability          *)
@@ -837,7 +841,7 @@
   "[| NSCDERIV g x :> Db; xa: CInfinitesimal; xa \<noteq> 0 |]
    ==> (( *fc* g) (hcomplex_of_complex x + xa) - hcomplex_of_complex(g x)) / xa
        @c= hcomplex_of_complex (Db)"
-by (auto simp add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_cinfmal_iff starfunC_lambda_cancel)
+by (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_cinfmal_iff starfunC_lambda_cancel)
 
 lemma lemma_complex_chain: "(z::hcomplex) \<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)"
 by auto
@@ -921,7 +925,7 @@
      "x \<noteq> 0 ==> NSCDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))"
 apply (simp add: nscderiv_def Ball_def, clarify) 
 apply (frule CInfinitesimal_add_not_zero [where x=x])
-apply (auto simp add: starfunC_inverse_inverse hcomplex_diff_def 
+apply (auto simp add: starfunC_inverse_inverse diff_minus 
            simp del: minus_mult_left [symmetric] minus_mult_right [symmetric])
 apply (simp add: hcomplex_add_commute numeral_2_eq_2 inverse_add
                  inverse_mult_distrib [symmetric] inverse_minus_eq [symmetric]
@@ -964,7 +968,7 @@
 lemma CDERIV_quotient:
      "[| CDERIV f x :> d; CDERIV g x :> e; g(x) \<noteq> 0 |]
        ==> CDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
-apply (simp add: complex_diff_def)
+apply (simp add: diff_minus)
 apply (drule_tac f = g in CDERIV_inverse_fun)
 apply (drule_tac [2] CDERIV_mult, assumption+)
 apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left 
@@ -1004,7 +1008,7 @@
 lemma CARAT_NSCDERIV:
      "NSCDERIV f x :> l ==>
       \<exists>g. (\<forall>z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l"
-by (auto simp add: NSCDERIV_CDERIV_iff isNSContc_isContc_iff CARAT_CDERIV)
+by (simp add: NSCDERIV_CDERIV_iff isNSContc_isContc_iff CARAT_CDERIV)
 
 (* FIXME tidy! How about a NS proof? *)
 lemma CARAT_CDERIVD:
diff -r 6be497cacab5 -r c7674b7034f5 src/HOL/Complex/CStar.thy
--- a/src/HOL/Complex/CStar.thy	Mon Mar 15 10:46:19 2004 +0100
+++ b/src/HOL/Complex/CStar.thy	Mon Mar 15 10:58:29 2004 +0100
@@ -242,7 +242,7 @@
 
 lemma starfunRC_mult:
     "( *fRc* f) z * ( *fRc* g) z = ( *fRc* (%x. f x * g x)) z"
-apply (rule eq_Abs_hypreal [of z])
+apply (cases z)
 apply (simp add: starfunRC hcomplex_mult)
 done
 declare starfunRC_mult [symmetric, simp]
@@ -263,7 +263,7 @@
 declare starfunC_add [symmetric, simp]
 
 lemma starfunRC_add: "( *fRc* f) z + ( *fRc* g) z = ( *fRc* (%x. f x + g x)) z"
-apply (rule eq_Abs_hypreal [of z])
+apply (cases z)
 apply (simp add: starfunRC hcomplex_add)
 done
 declare starfunRC_add [symmetric, simp]
@@ -281,7 +281,7 @@
 done
 
 lemma starfunRC_minus [simp]: "( *fRc* (%x. - f x)) x = - ( *fRc* f) x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: starfunRC hcomplex_minus)
 done
 
@@ -338,36 +338,36 @@
 by (simp add: o_def starfun_starfunCR_o2)
 
 lemma starfunC_const_fun [simp]: "( *fc* (%x. k)) z = hcomplex_of_complex k"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: starfunC hcomplex_of_complex_def)
 done
 
 lemma starfunRC_const_fun [simp]: "( *fRc* (%x. k)) z = hcomplex_of_complex k"
-apply (rule eq_Abs_hypreal [of z])
+apply (cases z)
 apply (simp add: starfunRC hcomplex_of_complex_def)
 done
 
 lemma starfunCR_const_fun [simp]: "( *fcR* (%x. k)) z = hypreal_of_real k"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: starfunCR hypreal_of_real_def)
 done
 
 lemma starfunC_inverse: "inverse (( *fc* f) x) = ( *fc* (%x. inverse (f x))) x"
-apply (rule eq_Abs_hcomplex [of x])
+apply (cases x)
 apply (simp add: starfunC hcomplex_inverse)
 done
 declare starfunC_inverse [symmetric, simp]
 
 lemma starfunRC_inverse:
     "inverse (( *fRc* f) x) = ( *fRc* (%x. inverse (f x))) x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: starfunRC hcomplex_inverse)
 done
 declare starfunRC_inverse [symmetric, simp]
 
 lemma starfunCR_inverse:
     "inverse (( *fcR* f) x) = ( *fcR* (%x. inverse (f x))) x"
-apply (rule eq_Abs_hcomplex [of x])
+apply (cases x)
 apply (simp add: starfunCR hypreal_inverse)
 done
 declare starfunCR_inverse [symmetric, simp]
@@ -401,43 +401,43 @@
 *)
 
 lemma starfunC_hcpow: "( *fc* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n"
-apply (rule eq_Abs_hcomplex [of Z])
+apply (cases Z)
 apply (simp add: hcpow starfunC hypnat_of_nat_eq)
 done
 
 lemma starfunC_lambda_cancel:
     "( *fc* (%h. f (x + h))) y  = ( *fc* f) (hcomplex_of_complex  x + y)"
-apply (rule eq_Abs_hcomplex [of y])
+apply (cases y)
 apply (simp add: starfunC hcomplex_of_complex_def hcomplex_add)
 done
 
 lemma starfunCR_lambda_cancel:
     "( *fcR* (%h. f (x + h))) y  = ( *fcR* f) (hcomplex_of_complex  x + y)"
-apply (rule eq_Abs_hcomplex [of y])
+apply (cases y)
 apply (simp add: starfunCR hcomplex_of_complex_def hcomplex_add)
 done
 
 lemma starfunRC_lambda_cancel:
     "( *fRc* (%h. f (x + h))) y  = ( *fRc* f) (hypreal_of_real x + y)"
-apply (rule eq_Abs_hypreal [of y])
+apply (cases y)
 apply (simp add: starfunRC hypreal_of_real_def hypreal_add)
 done
 
 lemma starfunC_lambda_cancel2:
     "( *fc* (%h. f(g(x + h)))) y = ( *fc* (f o g)) (hcomplex_of_complex x + y)"
-apply (rule eq_Abs_hcomplex [of y])
+apply (cases y)
 apply (simp add: starfunC hcomplex_of_complex_def hcomplex_add)
 done
 
 lemma starfunCR_lambda_cancel2:
     "( *fcR* (%h. f(g(x + h)))) y = ( *fcR* (f o g)) (hcomplex_of_complex x + y)"
-apply (rule eq_Abs_hcomplex [of y])
+apply (cases y)
 apply (simp add: starfunCR hcomplex_of_complex_def hcomplex_add)
 done
 
 lemma starfunRC_lambda_cancel2:
     "( *fRc* (%h. f(g(x + h)))) y = ( *fRc* (f o g)) (hypreal_of_real x + y)"
-apply (rule eq_Abs_hypreal [of y])
+apply (cases y)
 apply (simp add: starfunRC hypreal_of_real_def hypreal_add)
 done
 
@@ -484,7 +484,7 @@
 done
 
 lemma starfunC_inverse_inverse: "( *fc* inverse) x = inverse(x)"
-apply (rule eq_Abs_hcomplex [of x])
+apply (cases x)
 apply (simp add: starfunC hcomplex_inverse)
 done
 
@@ -521,7 +521,7 @@
 
 lemma starfunC_n_mult:
     "( *fcn* f) z * ( *fcn* g) z = ( *fcn* (% i x. f i x * g i x)) z"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: starfunC_n hcomplex_mult)
 done
 
@@ -529,14 +529,14 @@
 
 lemma starfunC_n_add:
     "( *fcn* f) z + ( *fcn* g) z = ( *fcn* (%i x. f i x + g i x)) z"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: starfunC_n hcomplex_add)
 done
 
 (** uminus **)
 
 lemma starfunC_n_minus: "- ( *fcn* g) z = ( *fcn* (%i x. - g i x)) z"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: starfunC_n hcomplex_minus)
 done
 
@@ -550,7 +550,7 @@
 
 lemma starfunC_n_const_fun [simp]:
      "( *fcn* (%i x. k)) z = hcomplex_of_complex  k"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: starfunC_n hcomplex_of_complex_def)
 done
 
@@ -582,27 +582,25 @@
 lemma starfunC_eq_Re_Im_iff:
     "(( *fc* f) x = z) = ((( *fcR* (%x. Re(f x))) x = hRe (z)) &
                           (( *fcR* (%x. Im(f x))) x = hIm (z)))"
-apply (rule eq_Abs_hcomplex [of x])
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases x, cases z)
 apply (auto simp add: starfunCR starfunC hIm hRe complex_Re_Im_cancel_iff, ultra+)
 done
 
 lemma starfunC_approx_Re_Im_iff:
     "(( *fc* f) x @c= z) = ((( *fcR* (%x. Re(f x))) x @= hRe (z)) &
                             (( *fcR* (%x. Im(f x))) x @= hIm (z)))"
-apply (rule eq_Abs_hcomplex [of x])
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases x, cases z)
 apply (simp add: starfunCR starfunC hIm hRe capprox_approx_iff)
 done
 
 lemma starfunC_Idfun_capprox:
     "x @c= hcomplex_of_complex a ==> ( *fc* (%x. x)) x @c= hcomplex_of_complex  a"
-apply (rule eq_Abs_hcomplex [of x])
+apply (cases x)
 apply (simp add: starfunC)
 done
 
 lemma starfunC_Id [simp]: "( *fc* (%x. x)) x = x"
-apply (rule eq_Abs_hcomplex [of x])
+apply (cases x)
 apply (simp add: starfunC)
 done
 
diff -r 6be497cacab5 -r c7674b7034f5 src/HOL/Complex/NSCA.thy
--- a/src/HOL/Complex/NSCA.thy	Mon Mar 15 10:46:19 2004 +0100
+++ b/src/HOL/Complex/NSCA.thy	Mon Mar 15 10:58:29 2004 +0100
@@ -724,8 +724,7 @@
 
 lemma hcomplex_of_hypreal_capprox_iff [simp]:
      "(hcomplex_of_hypreal x @c= hcomplex_of_hypreal z) = (x @= z)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of z])
+apply (cases x, cases z)
 apply (simp add: hcomplex_of_hypreal capprox_approx_iff)
 done
 
@@ -1133,13 +1132,13 @@
 
 lemma CFinite_HFinite_hcomplex_of_hypreal:
      "z \<in> HFinite ==> hcomplex_of_hypreal z \<in> CFinite"
-apply (rule eq_Abs_hypreal [of z])
+apply (cases z)
 apply (simp add: hcomplex_of_hypreal CFinite_HFinite_iff hypreal_zero_def [symmetric])
 done
 
 lemma SComplex_SReal_hcomplex_of_hypreal:
      "x \<in> Reals ==>  hcomplex_of_hypreal x \<in> SComplex"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: hcomplex_of_hypreal SComplex_SReal_iff hypreal_zero_def [symmetric])
 done
 
@@ -1178,32 +1177,28 @@
 lemma hcomplex_split_CInfinitesimal_iff:
      "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CInfinitesimal) =  
       (x \<in> Infinitesimal & y \<in> Infinitesimal)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases x, cases y)
 apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CInfinitesimal_Infinitesimal_iff)
 done
 
 lemma hcomplex_split_CFinite_iff:
      "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CFinite) =  
       (x \<in> HFinite & y \<in> HFinite)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases x, cases y)
 apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CFinite_HFinite_iff)
 done
 
 lemma hcomplex_split_SComplex_iff:
      "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> SComplex) =  
       (x \<in> Reals & y \<in> Reals)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases x, cases y)
 apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal SComplex_SReal_iff)
 done
 
 lemma hcomplex_split_CInfinite_iff:
      "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CInfinite) =  
       (x \<in> HInfinite | y \<in> HInfinite)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases x, cases y)
 apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CInfinite_HInfinite_iff)
 done
 
@@ -1211,10 +1206,7 @@
      "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @c=  
        hcomplex_of_hypreal x' + iii * hcomplex_of_hypreal y') =  
       (x @= x' & y @= y')"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (rule eq_Abs_hypreal [of x'])
-apply (rule eq_Abs_hypreal [of y'])
+apply (cases x, cases y, cases x', cases y')
 apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal capprox_approx_iff)
 done
 
diff -r 6be497cacab5 -r c7674b7034f5 src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Mon Mar 15 10:46:19 2004 +0100
+++ b/src/HOL/Complex/NSComplex.thy	Mon Mar 15 10:58:29 2004 +0100
@@ -190,6 +190,10 @@
 apply (force simp add: Rep_hcomplex_inverse hcomplexrel_def)
 done
 
+theorem hcomplex_cases [case_names Abs_hcomplex, cases type: hcomplex]:
+    "(!!x. z = Abs_hcomplex(hcomplexrel``{x}) ==> P) ==> P"
+by (rule eq_Abs_hcomplex [of z], blast)
+
 lemma hcomplexrel_iff [simp]:
    "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
 by (simp add: hcomplexrel_def)
@@ -215,8 +219,7 @@
 
 lemma hcomplex_hRe_hIm_cancel_iff:
      "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
-apply (rule eq_Abs_hcomplex [of z])
-apply (rule eq_Abs_hcomplex [of w])
+apply (cases z, cases w)
 apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff iff: hcomplexrel_iff)
 apply (ultra+)
 done
@@ -253,20 +256,17 @@
 done
 
 lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z"
-apply (rule eq_Abs_hcomplex [of z])
-apply (rule eq_Abs_hcomplex [of w])
+apply (cases z, cases w)
 apply (simp add: complex_add_commute hcomplex_add)
 done
 
 lemma hcomplex_add_assoc: "((z1::hcomplex) + z2) + z3 = z1 + (z2 + z3)"
-apply (rule eq_Abs_hcomplex [of z1])
-apply (rule eq_Abs_hcomplex [of z2])
-apply (rule eq_Abs_hcomplex [of z3])
+apply (cases z1, cases z2, cases z3)
 apply (simp add: hcomplex_add complex_add_assoc)
 done
 
 lemma hcomplex_add_zero_left: "(0::hcomplex) + z = z"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hcomplex_zero_def hcomplex_add)
 done
 
@@ -274,14 +274,12 @@
 by (simp add: hcomplex_add_zero_left hcomplex_add_commute)
 
 lemma hRe_add: "hRe(x + y) = hRe(x) + hRe(y)"
-apply (rule eq_Abs_hcomplex [of x])
-apply (rule eq_Abs_hcomplex [of y])
+apply (cases x, cases y)
 apply (simp add: hRe hcomplex_add hypreal_add complex_Re_add)
 done
 
 lemma hIm_add: "hIm(x + y) = hIm(x) + hIm(y)"
-apply (rule eq_Abs_hcomplex [of x])
-apply (rule eq_Abs_hcomplex [of y])
+apply (cases x, cases y)
 apply (simp add: hIm hcomplex_add hypreal_add complex_Im_add)
 done
 
@@ -301,7 +299,7 @@
 done
 
 lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hcomplex_add hcomplex_minus hcomplex_zero_def)
 done
 
@@ -318,33 +316,28 @@
 done
 
 lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w"
-apply (rule eq_Abs_hcomplex [of w])
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases w, cases z)
 apply (simp add: hcomplex_mult complex_mult_commute)
 done
 
 lemma hcomplex_mult_assoc: "((u::hcomplex) * v) * w = u * (v * w)"
-apply (rule eq_Abs_hcomplex [of u])
-apply (rule eq_Abs_hcomplex [of v])
-apply (rule eq_Abs_hcomplex [of w])
+apply (cases u, cases v, cases w)
 apply (simp add: hcomplex_mult complex_mult_assoc)
 done
 
 lemma hcomplex_mult_one_left: "(1::hcomplex) * z = z"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hcomplex_one_def hcomplex_mult)
 done
 
 lemma hcomplex_mult_zero_left: "(0::hcomplex) * z = 0"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hcomplex_zero_def hcomplex_mult)
 done
 
 lemma hcomplex_add_mult_distrib:
      "((z1::hcomplex) + z2) * w = (z1 * w) + (z2 * w)"
-apply (rule eq_Abs_hcomplex [of z1])
-apply (rule eq_Abs_hcomplex [of z2])
-apply (rule eq_Abs_hcomplex [of w])
+apply (cases z1, cases z2, cases w)
 apply (simp add: hcomplex_mult hcomplex_add left_distrib)
 done
 
@@ -366,7 +359,7 @@
 
 lemma hcomplex_mult_inv_left:
       "z \<noteq> (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hcomplex_zero_def hcomplex_one_def hcomplex_inverse hcomplex_mult, ultra)
 apply (rule ccontr)
 apply (drule left_inverse, auto)
@@ -414,12 +407,12 @@
 subsection{*More Minus Laws*}
 
 lemma hRe_minus: "hRe(-z) = - hRe(z)"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hRe hcomplex_minus hypreal_minus complex_Re_minus)
 done
 
 lemma hIm_minus: "hIm(-z) = - hIm(z)"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hIm hcomplex_minus hypreal_minus complex_Im_minus)
 done
 
@@ -484,28 +477,26 @@
 
 lemma hcomplex_of_hypreal_cancel_iff [iff]:
      "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases x, cases y)
 apply (simp add: hcomplex_of_hypreal)
 done
 
 lemma hcomplex_of_hypreal_minus:
      "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus)
 done
 
 lemma hcomplex_of_hypreal_inverse:
      "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse)
 done
 
 lemma hcomplex_of_hypreal_add:
      "hcomplex_of_hypreal x + hcomplex_of_hypreal y =
       hcomplex_of_hypreal (x + y)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases x, cases y)
 apply (simp add: hcomplex_of_hypreal hypreal_add hcomplex_add complex_of_real_add)
 done
 
@@ -517,8 +508,7 @@
 lemma hcomplex_of_hypreal_mult:
      "hcomplex_of_hypreal x * hcomplex_of_hypreal y =
       hcomplex_of_hypreal (x * y)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases x, cases y)
 apply (simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult complex_of_real_mult)
 done
 
@@ -537,12 +527,12 @@
 by (simp add: hcomplex_zero_def hypreal_zero_def hcomplex_of_hypreal)
 
 lemma hRe_hcomplex_of_hypreal [simp]: "hRe(hcomplex_of_hypreal z) = z"
-apply (rule eq_Abs_hypreal [of z])
+apply (cases z)
 apply (auto simp add: hcomplex_of_hypreal hRe)
 done
 
 lemma hIm_hcomplex_of_hypreal [simp]: "hIm(hcomplex_of_hypreal z) = 0"
-apply (rule eq_Abs_hypreal [of z])
+apply (cases z)
 apply (auto simp add: hcomplex_of_hypreal hIm hypreal_zero_num)
 done
 
@@ -554,14 +544,12 @@
 subsection{*HComplex theorems*}
 
 lemma hRe_HComplex [simp]: "hRe (HComplex x y) = x"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases x, cases y)
 apply (simp add: HComplex_def hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
 done
 
 lemma hIm_HComplex [simp]: "hIm (HComplex x y) = y"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases x, cases y)
 apply (simp add: HComplex_def hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
 done
 
@@ -597,7 +585,7 @@
 by (simp add: hcomplex_one_def hcmod hypreal_one_num)
 
 lemma hcmod_hcomplex_of_hypreal [simp]: "hcmod(hcomplex_of_hypreal x) = abs x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (auto simp add: hcmod hcomplex_of_hypreal hypreal_hrabs)
 done
 
@@ -610,10 +598,7 @@
 apply (rule iffI) 
  prefer 2 apply simp 
 apply (simp add: HComplex_def iii_def) 
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (rule eq_Abs_hypreal [of x'])
-apply (rule eq_Abs_hypreal [of y'])
+apply (cases x, cases y, cases x', cases y')
 apply (auto simp add: iii_def hcomplex_mult hcomplex_add hcomplex_of_hypreal)
 apply (ultra+) 
 done
@@ -676,52 +661,48 @@
 done
 
 lemma hcomplex_hcnj_cancel_iff [iff]: "(hcnj x = hcnj y) = (x = y)"
-apply (rule eq_Abs_hcomplex [of x])
-apply (rule eq_Abs_hcomplex [of y])
+apply (cases x, cases y)
 apply (simp add: hcnj)
 done
 
 lemma hcomplex_hcnj_hcnj [simp]: "hcnj (hcnj z) = z"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hcnj)
 done
 
 lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]:
      "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
 apply (simp add: hcnj hcomplex_of_hypreal)
 done
 
 lemma hcomplex_hmod_hcnj [simp]: "hcmod (hcnj z) = hcmod z"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hcnj hcmod)
 done
 
 lemma hcomplex_hcnj_minus: "hcnj (-z) = - hcnj z"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hcnj hcomplex_minus complex_cnj_minus)
 done
 
 lemma hcomplex_hcnj_inverse: "hcnj(inverse z) = inverse(hcnj z)"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hcnj hcomplex_inverse complex_cnj_inverse)
 done
 
 lemma hcomplex_hcnj_add: "hcnj(w + z) = hcnj(w) + hcnj(z)"
-apply (rule eq_Abs_hcomplex [of z])
-apply (rule eq_Abs_hcomplex [of w])
+apply (cases z, cases w)
 apply (simp add: hcnj hcomplex_add complex_cnj_add)
 done
 
 lemma hcomplex_hcnj_diff: "hcnj(w - z) = hcnj(w) - hcnj(z)"
-apply (rule eq_Abs_hcomplex [of z])
-apply (rule eq_Abs_hcomplex [of w])
+apply (cases z, cases w)
 apply (simp add: hcnj hcomplex_diff complex_cnj_diff)
 done
 
 lemma hcomplex_hcnj_mult: "hcnj(w * z) = hcnj(w) * hcnj(z)"
-apply (rule eq_Abs_hcomplex [of z])
-apply (rule eq_Abs_hcomplex [of w])
+apply (cases z, cases w)
 apply (simp add: hcnj hcomplex_mult complex_cnj_mult)
 done
 
@@ -735,13 +716,13 @@
 by (simp add: hcomplex_zero_def hcnj)
 
 lemma hcomplex_hcnj_zero_iff [iff]: "(hcnj z = 0) = (z = 0)"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hcomplex_zero_def hcnj)
 done
 
 lemma hcomplex_mult_hcnj:
      "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add
                       hypreal_mult complex_mult_cnj numeral_2_eq_2)
 done
@@ -750,7 +731,7 @@
 subsection{*More Theorems about the Function @{term hcmod}*}
 
 lemma hcomplex_hcmod_eq_zero_cancel [simp]: "(hcmod x = 0) = (x = 0)"
-apply (rule eq_Abs_hcomplex [of x])
+apply (cases x)
 apply (simp add: hcmod hcomplex_zero_def hypreal_zero_num)
 done
 
@@ -765,17 +746,17 @@
 done
 
 lemma hcmod_minus [simp]: "hcmod (-x) = hcmod(x)"
-apply (rule eq_Abs_hcomplex [of x])
+apply (cases x)
 apply (simp add: hcmod hcomplex_minus)
 done
 
 lemma hcmod_mult_hcnj: "hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj numeral_2_eq_2)
 done
 
 lemma hcmod_ge_zero [simp]: "(0::hypreal) \<le> hcmod x"
-apply (rule eq_Abs_hcomplex [of x])
+apply (cases x)
 apply (simp add: hcmod hypreal_zero_num hypreal_le)
 done
 
@@ -783,15 +764,13 @@
 by (simp add: abs_if linorder_not_less)
 
 lemma hcmod_mult: "hcmod(x*y) = hcmod(x) * hcmod(y)"
-apply (rule eq_Abs_hcomplex [of x])
-apply (rule eq_Abs_hcomplex [of y])
+apply (cases x, cases y)
 apply (simp add: hcmod hcomplex_mult hypreal_mult complex_mod_mult)
 done
 
 lemma hcmod_add_squared_eq:
      "hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)"
-apply (rule eq_Abs_hcomplex [of x])
-apply (rule eq_Abs_hcomplex [of y])
+apply (cases x, cases y)
 apply (simp add: hcmod hcomplex_add hypreal_mult hRe hcnj hcomplex_mult
                       numeral_2_eq_2 realpow_two [symmetric]
                   del: realpow_Suc)
@@ -801,8 +780,7 @@
 done
 
 lemma hcomplex_hRe_mult_hcnj_le_hcmod [simp]: "hRe(x * hcnj y) \<le> hcmod(x * hcnj y)"
-apply (rule eq_Abs_hcomplex [of x])
-apply (rule eq_Abs_hcomplex [of y])
+apply (cases x, cases y)
 apply (simp add: hcmod hcnj hcomplex_mult hRe hypreal_le)
 done
 
@@ -812,8 +790,7 @@
 done
 
 lemma hcmod_triangle_squared [simp]: "hcmod (x + y) ^ 2 \<le> (hcmod(x) + hcmod(y)) ^ 2"
-apply (rule eq_Abs_hcomplex [of x])
-apply (rule eq_Abs_hcomplex [of y])
+apply (cases x, cases y)
 apply (simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add
                       hypreal_le realpow_two [symmetric] numeral_2_eq_2
             del: realpow_Suc)
@@ -821,8 +798,7 @@
 done
 
 lemma hcmod_triangle_ineq [simp]: "hcmod (x + y) \<le> hcmod(x) + hcmod(y)"
-apply (rule eq_Abs_hcomplex [of x])
-apply (rule eq_Abs_hcomplex [of y])
+apply (cases x, cases y)
 apply (simp add: hcmod hcomplex_add hypreal_add hypreal_le)
 done
 
@@ -832,34 +808,26 @@
 done
 
 lemma hcmod_diff_commute: "hcmod (x - y) = hcmod (y - x)"
-apply (rule eq_Abs_hcomplex [of x])
-apply (rule eq_Abs_hcomplex [of y])
+apply (cases x, cases y)
 apply (simp add: hcmod hcomplex_diff complex_mod_diff_commute)
 done
 
 lemma hcmod_add_less:
      "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s"
-apply (rule eq_Abs_hcomplex [of x])
-apply (rule eq_Abs_hcomplex [of y])
-apply (rule eq_Abs_hypreal [of r])
-apply (rule eq_Abs_hypreal [of s])
+apply (cases x, cases y, cases r, cases s)
 apply (simp add: hcmod hcomplex_add hypreal_add hypreal_less, ultra)
 apply (auto intro: complex_mod_add_less)
 done
 
 lemma hcmod_mult_less:
      "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s"
-apply (rule eq_Abs_hcomplex [of x])
-apply (rule eq_Abs_hcomplex [of y])
-apply (rule eq_Abs_hypreal [of r])
-apply (rule eq_Abs_hypreal [of s])
+apply (cases x, cases y, cases r, cases s)
 apply (simp add: hcmod hypreal_mult hypreal_less hcomplex_mult, ultra)
 apply (auto intro: complex_mod_mult_less)
 done
 
 lemma hcmod_diff_ineq [simp]: "hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
-apply (rule eq_Abs_hcomplex [of a])
-apply (rule eq_Abs_hcomplex [of b])
+apply (cases a, cases b)
 apply (simp add: hcmod hcomplex_add hypreal_diff hypreal_le)
 done
 
@@ -877,14 +845,12 @@
 
 lemma hcomplex_of_hypreal_hyperpow:
      "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases x, cases n)
 apply (simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow)
 done
 
 lemma hcmod_hcpow: "hcmod(x hcpow n) = hcmod(x) pow n"
-apply (rule eq_Abs_hcomplex [of x])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases x, cases n)
 apply (simp add: hcpow hyperpow hcmod complex_mod_complexpow)
 done
 
@@ -935,22 +901,18 @@
 lemma hcpow_minus:
      "(-x::hcomplex) hcpow n =
       (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"
-apply (rule eq_Abs_hcomplex [of x])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases x, cases n)
 apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus, ultra)
 apply (auto simp add: neg_power_if, ultra)
 done
 
 lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
-apply (rule eq_Abs_hcomplex [of r])
-apply (rule eq_Abs_hcomplex [of s])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases r, cases s, cases n)
 apply (simp add: hcpow hypreal_mult hcomplex_mult power_mult_distrib)
 done
 
 lemma hcpow_zero [simp]: "0 hcpow (n + 1) = 0"
-apply (simp add: hcomplex_zero_def hypnat_one_def)
-apply (rule eq_Abs_hypnat [of n])
+apply (simp add: hcomplex_zero_def hypnat_one_def, cases n)
 apply (simp add: hcpow hypnat_add)
 done
 
@@ -958,8 +920,7 @@
 by (simp add: hSuc_def)
 
 lemma hcpow_not_zero [simp,intro]: "r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)"
-apply (rule eq_Abs_hcomplex [of r])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases r, cases n)
 apply (auto simp add: hcpow hcomplex_zero_def, ultra)
 done
 
@@ -991,19 +952,18 @@
 by (simp add: hcomplex_one_def hsgn)
 
 lemma hsgn_minus: "hsgn (-z) = - hsgn(z)"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hsgn hcomplex_minus sgn_minus)
 done
 
 lemma hsgn_eq: "hsgn z = z / hcomplex_of_hypreal (hcmod z)"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq)
 done
 
 
 lemma hcmod_i: "hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y]) 
+apply (cases x, cases y) 
 apply (simp add: HComplex_eq_Abs_hcomplex_Complex starfun 
                  hypreal_mult hypreal_add hcmod numeral_2_eq_2)
 done
@@ -1029,12 +989,12 @@
 by (simp add: i_eq_HComplex_0_1) 
 
 lemma hRe_hsgn [simp]: "hRe(hsgn z) = hRe(z)/hcmod z"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hsgn hcmod hRe hypreal_divide)
 done
 
 lemma hIm_hsgn [simp]: "hIm(hsgn z) = hIm(z)/hcmod z"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: hsgn hcmod hIm hypreal_divide)
 done
 
@@ -1045,8 +1005,7 @@
      "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))"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases x, cases y)
 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)
 apply (simp add: diff_minus) 
 done
@@ -1060,20 +1019,18 @@
 
 lemma hRe_mult_i_eq[simp]:
     "hRe (iii * hcomplex_of_hypreal y) = 0"
-apply (simp add: iii_def)
-apply (rule eq_Abs_hypreal [of y])
+apply (simp add: iii_def, cases y)
 apply (simp add: hcomplex_of_hypreal hcomplex_mult hRe hypreal_zero_num)
 done
 
 lemma hIm_mult_i_eq [simp]:
     "hIm (iii * hcomplex_of_hypreal y) = y"
-apply (simp add: iii_def)
-apply (rule eq_Abs_hypreal [of y])
+apply (simp add: iii_def, cases y)
 apply (simp add: hcomplex_of_hypreal hcomplex_mult hIm hypreal_zero_num)
 done
 
 lemma hcmod_mult_i [simp]: "hcmod (iii * hcomplex_of_hypreal y) = abs y"
-apply (rule eq_Abs_hypreal [of y])
+apply (cases y)
 apply (simp add: hcomplex_of_hypreal hcmod hypreal_hrabs iii_def hcomplex_mult)
 done
 
@@ -1094,14 +1051,14 @@
 
 lemma cos_harg_i_mult_zero_pos:
      "0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
-apply (rule eq_Abs_hypreal [of y])
+apply (cases y)
 apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
                 hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
 done
 
 lemma cos_harg_i_mult_zero_neg:
      "y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
-apply (rule eq_Abs_hypreal [of y])
+apply (cases y)
 apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
                  hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
 done
@@ -1113,7 +1070,7 @@
 
 lemma hcomplex_of_hypreal_zero_iff [simp]:
      "(hcomplex_of_hypreal y = 0) = (y = 0)"
-apply (rule eq_Abs_hypreal [of y])
+apply (cases y)
 apply (simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
 done
 
@@ -1134,7 +1091,7 @@
 
 lemma hcomplex_split_polar:
   "\<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
-apply (rule eq_Abs_hcomplex [of z])
+apply (cases z)
 apply (simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult HComplex_def)
 apply (cut_tac z = x in complex_split_polar2)
 apply (drule choice, safe)+
@@ -1153,7 +1110,7 @@
    "hcis a =
     (hcomplex_of_hypreal(( *f* cos) a) +
     iii * hcomplex_of_hypreal(( *f* sin) a))"
-apply (rule eq_Abs_hypreal [of a])
+apply (cases a)
 apply (simp add: starfun hcis hcomplex_of_hypreal iii_def hcomplex_mult hcomplex_add cis_def)
 done
 
@@ -1186,7 +1143,7 @@
 
 lemma hcmod_unit_one [simp]:
      "hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
-apply (rule eq_Abs_hypreal [of a]) 
+apply (cases a) 
 apply (simp add: HComplex_def iii_def starfun hcomplex_of_hypreal 
                  hcomplex_mult hcmod hcomplex_add hypreal_one_def)
 done
@@ -1210,19 +1167,14 @@
 
 lemma hrcis_mult:
   "hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
-apply (simp add: hrcis_def)
-apply (rule eq_Abs_hypreal [of r1])
-apply (rule eq_Abs_hypreal [of r2])
-apply (rule eq_Abs_hypreal [of a])
-apply (rule eq_Abs_hypreal [of b])
+apply (simp add: hrcis_def, cases r1, cases r2, cases a, cases b)
 apply (simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal
                       hcomplex_mult cis_mult [symmetric]
                       complex_of_real_mult [symmetric])
 done
 
 lemma hcis_mult: "hcis a * hcis b = hcis (a + b)"
-apply (rule eq_Abs_hypreal [of a])
-apply (rule eq_Abs_hypreal [of b])
+apply (cases a, cases b)
 apply (simp add: hcis hcomplex_mult hypreal_add cis_mult)
 done
 
@@ -1230,13 +1182,12 @@
 by (simp add: hcomplex_one_def hcis hypreal_zero_num)
 
 lemma hrcis_zero_mod [simp]: "hrcis 0 a = 0"
-apply (simp add: hcomplex_zero_def)
-apply (rule eq_Abs_hypreal [of a])
+apply (simp add: hcomplex_zero_def, cases a)
 apply (simp add: hrcis hypreal_zero_num)
 done
 
 lemma hrcis_zero_arg [simp]: "hrcis r 0 = hcomplex_of_hypreal r"
-apply (rule eq_Abs_hypreal [of r])
+apply (cases r)
 apply (simp add: hrcis hypreal_zero_num hcomplex_of_hypreal)
 done
 
@@ -1248,7 +1199,7 @@
 
 lemma hcis_hypreal_of_nat_Suc_mult:
    "hcis (hypreal_of_nat (Suc n) * a) = hcis a * hcis (hypreal_of_nat n * a)"
-apply (rule eq_Abs_hypreal [of a])
+apply (cases a)
 apply (simp add: hypreal_of_nat hcis hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
 done
 
@@ -1260,14 +1211,12 @@
 lemma hcis_hypreal_of_hypnat_Suc_mult:
      "hcis (hypreal_of_hypnat (n + 1) * a) =
       hcis a * hcis (hypreal_of_hypnat n * a)"
-apply (rule eq_Abs_hypreal [of a])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases a, cases n)
 apply (simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
 done
 
 lemma NSDeMoivre_ext: "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)"
-apply (rule eq_Abs_hypreal [of a])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases a, cases n)
 apply (simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre)
 done
 
@@ -1282,24 +1231,23 @@
 done
 
 lemma hcis_inverse [simp]: "inverse(hcis a) = hcis (-a)"
-apply (rule eq_Abs_hypreal [of a])
+apply (cases a)
 apply (simp add: hcomplex_inverse hcis hypreal_minus)
 done
 
 lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)"
-apply (rule eq_Abs_hypreal [of a])
-apply (rule eq_Abs_hypreal [of r])
+apply (cases a, cases r)
 apply (simp add: hcomplex_inverse hrcis hypreal_minus hypreal_inverse rcis_inverse, ultra)
 apply (simp add: real_divide_def)
 done
 
 lemma hRe_hcis [simp]: "hRe(hcis a) = ( *f* cos) a"
-apply (rule eq_Abs_hypreal [of a])
+apply (cases a)
 apply (simp add: hcis starfun hRe)
 done
 
 lemma hIm_hcis [simp]: "hIm(hcis a) = ( *f* sin) a"
-apply (rule eq_Abs_hypreal [of a])
+apply (cases a)
 apply (simp add: hcis starfun hIm)
 done
 
@@ -1316,9 +1264,7 @@
 by (simp add: NSDeMoivre_ext)
 
 lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)"
-apply (simp add: hexpi_def)
-apply (rule eq_Abs_hcomplex [of a])
-apply (rule eq_Abs_hcomplex [of b])
+apply (simp add: hexpi_def, cases a, cases b)
 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)
 done
 
diff -r 6be497cacab5 -r c7674b7034f5 src/HOL/Complex/NSInduct.thy
--- a/src/HOL/Complex/NSInduct.thy	Mon Mar 15 10:46:19 2004 +0100
+++ b/src/HOL/Complex/NSInduct.thy	Mon Mar 15 10:58:29 2004 +0100
@@ -35,7 +35,7 @@
     "(( *pNat* P) 0 &
             (\<forall>n. ( *pNat* P)(n) --> ( *pNat* P)(n + 1)))
        --> ( *pNat* P)(n)"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
 apply (auto simp add: hypnat_zero_def hypnat_one_def starPNat, ultra)
 apply (erule nat_induct)
 apply (drule_tac x = "hypnat_of_nat n" in spec)