heavy tidying
authorpaulson
Mon Mar 15 10:58:29 2004 +0100 (2004-03-15)
changeset 14469c7674b7034f5
parent 14468 6be497cacab5
child 14470 1ffe42cfaefe
heavy tidying
src/HOL/Complex/CLim.thy
src/HOL/Complex/CStar.thy
src/HOL/Complex/NSCA.thy
src/HOL/Complex/NSComplex.thy
src/HOL/Complex/NSInduct.thy
     1.1 --- a/src/HOL/Complex/CLim.thy	Mon Mar 15 10:46:19 2004 +0100
     1.2 +++ b/src/HOL/Complex/CLim.thy	Mon Mar 15 10:58:29 2004 +0100
     1.3 @@ -1,10 +1,11 @@
     1.4  (*  Title       : CLim.thy
     1.5      Author      : Jacques D. Fleuriot
     1.6      Copyright   : 2001 University of Edinburgh
     1.7 -    Description : A first theory of limits, continuity and
     1.8 -                  differentiation for complex functions
     1.9 +    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
    1.10  *)
    1.11  
    1.12 +header{*Limits, Continuity and Differentiation for Complex Functions*}
    1.13 +
    1.14  theory CLim = CSeries:
    1.15  
    1.16  (*not in simpset?*)
    1.17 @@ -13,7 +14,7 @@
    1.18  (*??generalize*)
    1.19  lemma lemma_complex_mult_inverse_squared [simp]:
    1.20       "x \<noteq> (0::complex) \<Longrightarrow> (x * inverse(x) ^ 2) = inverse x"
    1.21 -by (auto simp add: numeral_2_eq_2)
    1.22 +by (simp add: numeral_2_eq_2)
    1.23  
    1.24  text{*Changing the quantified variable. Install earlier?*}
    1.25  lemma all_shift: "(\<forall>x::'a::ring. P x) = (\<forall>x. P (x-a))";
    1.26 @@ -109,21 +110,17 @@
    1.27  subsection{*Limit of Complex to Complex Function*}
    1.28  
    1.29  lemma NSCLIM_NSCRLIM_Re: "f -- a --NSC> L ==> (%x. Re(f x)) -- a --NSCR> Re(L)"
    1.30 -apply (unfold NSCLIM_def NSCRLIM_def)
    1.31 -apply (rule eq_Abs_hcomplex [of x])
    1.32 -apply (auto simp add: starfunC_approx_Re_Im_iff hRe_hcomplex_of_complex)
    1.33 -done
    1.34 +by (simp add: NSCLIM_def NSCRLIM_def starfunC_approx_Re_Im_iff 
    1.35 +              hRe_hcomplex_of_complex)
    1.36 +
    1.37  
    1.38 -lemma NSCLIM_NSCRLIM_Im:
    1.39 -   "f -- a --NSC> L ==> (%x. Im(f x)) -- a --NSCR> Im(L)"
    1.40 -apply (unfold NSCLIM_def NSCRLIM_def)
    1.41 -apply (rule eq_Abs_hcomplex [of x])
    1.42 -apply (auto simp add: starfunC_approx_Re_Im_iff hIm_hcomplex_of_complex)
    1.43 -done
    1.44 +lemma NSCLIM_NSCRLIM_Im: "f -- a --NSC> L ==> (%x. Im(f x)) -- a --NSCR> Im(L)"
    1.45 +by (simp add: NSCLIM_def NSCRLIM_def starfunC_approx_Re_Im_iff 
    1.46 +              hIm_hcomplex_of_complex)
    1.47  
    1.48  lemma CLIM_NSCLIM:
    1.49        "f -- x --C> L ==> f -- x --NSC> L"
    1.50 -apply (unfold CLIM_def NSCLIM_def capprox_def, auto)
    1.51 +apply (simp add: CLIM_def NSCLIM_def capprox_def, auto)
    1.52  apply (rule_tac z = xa in eq_Abs_hcomplex)
    1.53  apply (auto simp add: hcomplex_of_complex_def starfunC hcomplex_diff 
    1.54           CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff)
    1.55 @@ -167,14 +164,18 @@
    1.56  
    1.57  lemma NSCLIM_CLIM:
    1.58       "f -- x --NSC> L ==> f -- x --C> L"
    1.59 -apply (unfold CLIM_def NSCLIM_def)
    1.60 +apply (simp add: CLIM_def NSCLIM_def)
    1.61  apply (rule ccontr) 
    1.62 -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)
    1.63 +apply (auto simp add: eq_Abs_hcomplex_ALL starfunC 
    1.64 +            CInfinitesimal_capprox_minus [symmetric] hcomplex_diff
    1.65 +            CInfinitesimal_hcmod_iff hcomplex_of_complex_def 
    1.66 +            Infinitesimal_FreeUltrafilterNat_iff hcmod)
    1.67  apply (simp add: linorder_not_less)
    1.68  apply (drule lemma_skolemize_CLIM2, safe)
    1.69  apply (drule_tac x = X in spec, auto)
    1.70  apply (drule lemma_csimp [THEN complex_seq_to_hcomplex_CInfinitesimal])
    1.71 -apply (simp add: CInfinitesimal_hcmod_iff hcomplex_of_complex_def Infinitesimal_FreeUltrafilterNat_iff hcomplex_diff hcmod, blast)
    1.72 +apply (simp add: CInfinitesimal_hcmod_iff hcomplex_of_complex_def 
    1.73 +            Infinitesimal_FreeUltrafilterNat_iff hcomplex_diff hcmod,  blast)
    1.74  apply (drule_tac x = r in spec, clarify)
    1.75  apply (drule FreeUltrafilterNat_all, ultra, arith)
    1.76  done
    1.77 @@ -188,9 +189,12 @@
    1.78  subsection{*Limit of Complex to Real Function*}
    1.79  
    1.80  lemma CRLIM_NSCRLIM: "f -- x --CR> L ==> f -- x --NSCR> L"
    1.81 -apply (unfold CRLIM_def NSCRLIM_def capprox_def, auto)
    1.82 +apply (simp add: CRLIM_def NSCRLIM_def capprox_def, auto)
    1.83  apply (rule_tac z = xa in eq_Abs_hcomplex)
    1.84 -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)
    1.85 +apply (auto simp add: hcomplex_of_complex_def starfunCR hcomplex_diff
    1.86 +              CInfinitesimal_hcmod_iff hcmod hypreal_diff
    1.87 +              Infinitesimal_FreeUltrafilterNat_iff
    1.88 +              Infinitesimal_approx_minus [symmetric] hypreal_of_real_def)
    1.89  apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe)
    1.90  apply (drule_tac x = u in spec, auto)
    1.91  apply (drule_tac x = s in spec, auto, ultra)
    1.92 @@ -223,7 +227,7 @@
    1.93  by auto
    1.94  
    1.95  lemma NSCRLIM_CRLIM: "f -- x --NSCR> L ==> f -- x --CR> L"
    1.96 -apply (unfold CRLIM_def NSCRLIM_def capprox_def)
    1.97 +apply (simp add: CRLIM_def NSCRLIM_def capprox_def)
    1.98  apply (rule ccontr) 
    1.99  apply (auto simp add: eq_Abs_hcomplex_ALL starfunCR hcomplex_diff 
   1.100               hcomplex_of_complex_def hypreal_diff CInfinitesimal_hcmod_iff 
   1.101 @@ -252,10 +256,10 @@
   1.102  by (auto dest: NSCLIM_NSCRLIM_Im simp add: CLIM_NSCLIM_iff CRLIM_NSCRLIM_iff [symmetric])
   1.103  
   1.104  lemma CLIM_cnj: "f -- a --C> L ==> (%x. cnj (f x)) -- a --C> cnj L"
   1.105 -by (auto simp add: CLIM_def complex_cnj_diff [symmetric])
   1.106 +by (simp add: CLIM_def complex_cnj_diff [symmetric])
   1.107  
   1.108  lemma CLIM_cnj_iff: "((%x. cnj (f x)) -- a --C> cnj L) = (f -- a --C> L)"
   1.109 -by (auto simp add: CLIM_def complex_cnj_diff [symmetric])
   1.110 +by (simp add: CLIM_def complex_cnj_diff [symmetric])
   1.111  
   1.112  (*** NSLIM_add hence CLIM_add *)
   1.113  
   1.114 @@ -302,7 +306,7 @@
   1.115  lemma NSCLIM_diff:
   1.116       "[| f -- x --NSC> l; g -- x --NSC> m |]
   1.117        ==> (%x. f(x) - g(x)) -- x --NSC> (l - m)"
   1.118 -by (simp add: complex_diff_def NSCLIM_add NSCLIM_minus)
   1.119 +by (simp add: diff_minus NSCLIM_add NSCLIM_minus)
   1.120  
   1.121  lemma CLIM_diff:
   1.122       "[| f -- x --C> l; g -- x --C> m |]
   1.123 @@ -314,9 +318,9 @@
   1.124  lemma NSCLIM_inverse:
   1.125       "[| f -- a --NSC> L;  L \<noteq> 0 |]
   1.126        ==> (%x. inverse(f(x))) -- a --NSC> (inverse L)"
   1.127 -apply (unfold NSCLIM_def, clarify)
   1.128 +apply (simp add: NSCLIM_def, clarify)
   1.129  apply (drule spec)
   1.130 -apply (auto simp add: hcomplex_of_complex_capprox_inverse)
   1.131 +apply (force simp add: hcomplex_of_complex_capprox_inverse)
   1.132  done
   1.133  
   1.134  lemma CLIM_inverse:
   1.135 @@ -327,9 +331,9 @@
   1.136  (*** NSCLIM_zero, CLIM_zero, etc. ***)
   1.137  
   1.138  lemma NSCLIM_zero: "f -- a --NSC> l ==> (%x. f(x) - l) -- a --NSC> 0"
   1.139 +apply (simp add: diff_minus)
   1.140  apply (rule_tac a1 = l in right_minus [THEN subst])
   1.141 -apply (unfold complex_diff_def)
   1.142 -apply (rule NSCLIM_add, auto)
   1.143 +apply (rule NSCLIM_add, auto) 
   1.144  done
   1.145  
   1.146  lemma CLIM_zero: "f -- a --C> l ==> (%x. f(x) - l) -- a --C> 0"
   1.147 @@ -412,7 +416,7 @@
   1.148  (* so this is nicer nonstandard proof *)
   1.149  lemma NSCLIM_NSCRLIM_iff2:
   1.150       "(f -- x --NSC> L) = ((%y. cmod(f y - L)) -- x --NSCR> 0)"
   1.151 -by (auto simp add: CRLIM_NSCRLIM_iff [symmetric] CLIM_CRLIM_iff CLIM_NSCLIM_iff [symmetric])
   1.152 +by (simp add: CRLIM_NSCRLIM_iff [symmetric] CLIM_CRLIM_iff CLIM_NSCLIM_iff [symmetric])
   1.153  
   1.154  lemma NSCLIM_NSCRLIM_Re_Im_iff:
   1.155       "(f -- a --NSC> L) = ((%x. Re(f x)) -- a --NSCR> Re(L) &
   1.156 @@ -421,7 +425,7 @@
   1.157  apply (auto simp add: NSCLIM_def NSCRLIM_def)
   1.158  apply (auto dest!: spec) 
   1.159  apply (rule_tac z = x in eq_Abs_hcomplex)
   1.160 -apply (auto simp add: capprox_approx_iff starfunC hcomplex_of_complex_def starfunCR hypreal_of_real_def)
   1.161 +apply (simp add: capprox_approx_iff starfunC hcomplex_of_complex_def starfunCR hypreal_of_real_def)
   1.162  done
   1.163  
   1.164  lemma CLIM_CRLIM_Re_Im_iff:
   1.165 @@ -501,7 +505,7 @@
   1.166  
   1.167  
   1.168  lemma isContc_o: "[| isContc f a; isContc g (f a) |] ==> isContc (g o f) a"
   1.169 -by (auto simp add: isNSContc_isContc_iff [symmetric] isNSContc_def starfunC_o [symmetric])
   1.170 +by (simp add: isNSContc_isContc_iff [symmetric] isNSContc_def starfunC_o [symmetric])
   1.171  
   1.172  lemma isContc_o2:
   1.173       "[| isContc f a; isContc g (f a) |] ==> isContc (%x. g (f x)) a"
   1.174 @@ -523,7 +527,7 @@
   1.175  
   1.176  lemma isContc_diff:
   1.177        "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) - g(x)) a"
   1.178 -apply (simp add: complex_diff_def)
   1.179 +apply (simp add: diff_minus)
   1.180  apply (auto intro: isContc_add isContc_minus)
   1.181  done
   1.182  
   1.183 @@ -571,7 +575,7 @@
   1.184                      isNSContCR_def) 
   1.185  
   1.186  lemma isContCR_cmod [simp]: "isContCR cmod (a)"
   1.187 -by (auto simp add: isNSContCR_isContCR_iff [symmetric])
   1.188 +by (simp add: isNSContCR_isContCR_iff [symmetric])
   1.189  
   1.190  lemma isContc_isContCR_Re: "isContc f a ==> isContCR (%x. Re (f x)) a"
   1.191  by (simp add: isContc_def isContCR_def CLIM_CRLIM_Re)
   1.192 @@ -746,7 +750,7 @@
   1.193  
   1.194  lemma NSCDERIV_cmult: "NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c*D"
   1.195  apply (simp add: times_divide_eq_right [symmetric] NSCDERIV_NSCLIM_iff 
   1.196 -                 minus_mult_right right_distrib [symmetric] complex_diff_def
   1.197 +                 minus_mult_right right_distrib [symmetric] diff_minus
   1.198              del: times_divide_eq_right minus_mult_right [symmetric])
   1.199  apply (erule NSCLIM_const [THEN NSCLIM_mult])
   1.200  done
   1.201 @@ -755,7 +759,7 @@
   1.202  by (simp add: NSCDERIV_cmult NSCDERIV_CDERIV_iff [symmetric])
   1.203  
   1.204  lemma NSCDERIV_minus: "NSCDERIV f x :> D ==> NSCDERIV (%x. -(f x)) x :> -D"
   1.205 -apply (simp add: NSCDERIV_NSCLIM_iff complex_diff_def)
   1.206 +apply (simp add: NSCDERIV_NSCLIM_iff diff_minus)
   1.207  apply (rule_tac t = "f x" in minus_minus [THEN subst])
   1.208  apply (simp (no_asm_simp) add: minus_add_distrib [symmetric]
   1.209              del: minus_add_distrib minus_minus)
   1.210 @@ -778,12 +782,12 @@
   1.211  lemma NSCDERIV_diff:
   1.212       "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |]
   1.213        ==> NSCDERIV (%x. f x - g x) x :> Da - Db"
   1.214 -by (simp add: complex_diff_def NSCDERIV_add_minus)
   1.215 +by (simp add: diff_minus NSCDERIV_add_minus)
   1.216  
   1.217  lemma CDERIV_diff:
   1.218       "[| CDERIV f x :> Da; CDERIV g x :> Db |]
   1.219         ==> CDERIV (%x. f x - g x) x :> Da - Db"
   1.220 -by (simp add: complex_diff_def CDERIV_add_minus)
   1.221 +by (simp add: diff_minus CDERIV_add_minus)
   1.222  
   1.223  
   1.224  subsection{*Chain Rule*}
   1.225 @@ -823,7 +827,7 @@
   1.226  	 - hcomplex_of_complex (f (g x))) /
   1.227  	(( *fc* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex (g x))
   1.228  	   @c= hcomplex_of_complex (Da)"
   1.229 -by (auto simp add: NSCDERIV_NSCLIM_iff2 NSCLIM_def)
   1.230 +by (simp add: NSCDERIV_NSCLIM_iff2 NSCLIM_def)
   1.231  
   1.232  (*--------------------------------------------------*)
   1.233  (* from other version of differentiability          *)
   1.234 @@ -837,7 +841,7 @@
   1.235    "[| NSCDERIV g x :> Db; xa: CInfinitesimal; xa \<noteq> 0 |]
   1.236     ==> (( *fc* g) (hcomplex_of_complex x + xa) - hcomplex_of_complex(g x)) / xa
   1.237         @c= hcomplex_of_complex (Db)"
   1.238 -by (auto simp add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_cinfmal_iff starfunC_lambda_cancel)
   1.239 +by (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_cinfmal_iff starfunC_lambda_cancel)
   1.240  
   1.241  lemma lemma_complex_chain: "(z::hcomplex) \<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)"
   1.242  by auto
   1.243 @@ -921,7 +925,7 @@
   1.244       "x \<noteq> 0 ==> NSCDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))"
   1.245  apply (simp add: nscderiv_def Ball_def, clarify) 
   1.246  apply (frule CInfinitesimal_add_not_zero [where x=x])
   1.247 -apply (auto simp add: starfunC_inverse_inverse hcomplex_diff_def 
   1.248 +apply (auto simp add: starfunC_inverse_inverse diff_minus 
   1.249             simp del: minus_mult_left [symmetric] minus_mult_right [symmetric])
   1.250  apply (simp add: hcomplex_add_commute numeral_2_eq_2 inverse_add
   1.251                   inverse_mult_distrib [symmetric] inverse_minus_eq [symmetric]
   1.252 @@ -964,7 +968,7 @@
   1.253  lemma CDERIV_quotient:
   1.254       "[| CDERIV f x :> d; CDERIV g x :> e; g(x) \<noteq> 0 |]
   1.255         ==> CDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
   1.256 -apply (simp add: complex_diff_def)
   1.257 +apply (simp add: diff_minus)
   1.258  apply (drule_tac f = g in CDERIV_inverse_fun)
   1.259  apply (drule_tac [2] CDERIV_mult, assumption+)
   1.260  apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left 
   1.261 @@ -1004,7 +1008,7 @@
   1.262  lemma CARAT_NSCDERIV:
   1.263       "NSCDERIV f x :> l ==>
   1.264        \<exists>g. (\<forall>z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l"
   1.265 -by (auto simp add: NSCDERIV_CDERIV_iff isNSContc_isContc_iff CARAT_CDERIV)
   1.266 +by (simp add: NSCDERIV_CDERIV_iff isNSContc_isContc_iff CARAT_CDERIV)
   1.267  
   1.268  (* FIXME tidy! How about a NS proof? *)
   1.269  lemma CARAT_CDERIVD:
     2.1 --- a/src/HOL/Complex/CStar.thy	Mon Mar 15 10:46:19 2004 +0100
     2.2 +++ b/src/HOL/Complex/CStar.thy	Mon Mar 15 10:58:29 2004 +0100
     2.3 @@ -242,7 +242,7 @@
     2.4  
     2.5  lemma starfunRC_mult:
     2.6      "( *fRc* f) z * ( *fRc* g) z = ( *fRc* (%x. f x * g x)) z"
     2.7 -apply (rule eq_Abs_hypreal [of z])
     2.8 +apply (cases z)
     2.9  apply (simp add: starfunRC hcomplex_mult)
    2.10  done
    2.11  declare starfunRC_mult [symmetric, simp]
    2.12 @@ -263,7 +263,7 @@
    2.13  declare starfunC_add [symmetric, simp]
    2.14  
    2.15  lemma starfunRC_add: "( *fRc* f) z + ( *fRc* g) z = ( *fRc* (%x. f x + g x)) z"
    2.16 -apply (rule eq_Abs_hypreal [of z])
    2.17 +apply (cases z)
    2.18  apply (simp add: starfunRC hcomplex_add)
    2.19  done
    2.20  declare starfunRC_add [symmetric, simp]
    2.21 @@ -281,7 +281,7 @@
    2.22  done
    2.23  
    2.24  lemma starfunRC_minus [simp]: "( *fRc* (%x. - f x)) x = - ( *fRc* f) x"
    2.25 -apply (rule eq_Abs_hypreal [of x])
    2.26 +apply (cases x)
    2.27  apply (simp add: starfunRC hcomplex_minus)
    2.28  done
    2.29  
    2.30 @@ -338,36 +338,36 @@
    2.31  by (simp add: o_def starfun_starfunCR_o2)
    2.32  
    2.33  lemma starfunC_const_fun [simp]: "( *fc* (%x. k)) z = hcomplex_of_complex k"
    2.34 -apply (rule eq_Abs_hcomplex [of z])
    2.35 +apply (cases z)
    2.36  apply (simp add: starfunC hcomplex_of_complex_def)
    2.37  done
    2.38  
    2.39  lemma starfunRC_const_fun [simp]: "( *fRc* (%x. k)) z = hcomplex_of_complex k"
    2.40 -apply (rule eq_Abs_hypreal [of z])
    2.41 +apply (cases z)
    2.42  apply (simp add: starfunRC hcomplex_of_complex_def)
    2.43  done
    2.44  
    2.45  lemma starfunCR_const_fun [simp]: "( *fcR* (%x. k)) z = hypreal_of_real k"
    2.46 -apply (rule eq_Abs_hcomplex [of z])
    2.47 +apply (cases z)
    2.48  apply (simp add: starfunCR hypreal_of_real_def)
    2.49  done
    2.50  
    2.51  lemma starfunC_inverse: "inverse (( *fc* f) x) = ( *fc* (%x. inverse (f x))) x"
    2.52 -apply (rule eq_Abs_hcomplex [of x])
    2.53 +apply (cases x)
    2.54  apply (simp add: starfunC hcomplex_inverse)
    2.55  done
    2.56  declare starfunC_inverse [symmetric, simp]
    2.57  
    2.58  lemma starfunRC_inverse:
    2.59      "inverse (( *fRc* f) x) = ( *fRc* (%x. inverse (f x))) x"
    2.60 -apply (rule eq_Abs_hypreal [of x])
    2.61 +apply (cases x)
    2.62  apply (simp add: starfunRC hcomplex_inverse)
    2.63  done
    2.64  declare starfunRC_inverse [symmetric, simp]
    2.65  
    2.66  lemma starfunCR_inverse:
    2.67      "inverse (( *fcR* f) x) = ( *fcR* (%x. inverse (f x))) x"
    2.68 -apply (rule eq_Abs_hcomplex [of x])
    2.69 +apply (cases x)
    2.70  apply (simp add: starfunCR hypreal_inverse)
    2.71  done
    2.72  declare starfunCR_inverse [symmetric, simp]
    2.73 @@ -401,43 +401,43 @@
    2.74  *)
    2.75  
    2.76  lemma starfunC_hcpow: "( *fc* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n"
    2.77 -apply (rule eq_Abs_hcomplex [of Z])
    2.78 +apply (cases Z)
    2.79  apply (simp add: hcpow starfunC hypnat_of_nat_eq)
    2.80  done
    2.81  
    2.82  lemma starfunC_lambda_cancel:
    2.83      "( *fc* (%h. f (x + h))) y  = ( *fc* f) (hcomplex_of_complex  x + y)"
    2.84 -apply (rule eq_Abs_hcomplex [of y])
    2.85 +apply (cases y)
    2.86  apply (simp add: starfunC hcomplex_of_complex_def hcomplex_add)
    2.87  done
    2.88  
    2.89  lemma starfunCR_lambda_cancel:
    2.90      "( *fcR* (%h. f (x + h))) y  = ( *fcR* f) (hcomplex_of_complex  x + y)"
    2.91 -apply (rule eq_Abs_hcomplex [of y])
    2.92 +apply (cases y)
    2.93  apply (simp add: starfunCR hcomplex_of_complex_def hcomplex_add)
    2.94  done
    2.95  
    2.96  lemma starfunRC_lambda_cancel:
    2.97      "( *fRc* (%h. f (x + h))) y  = ( *fRc* f) (hypreal_of_real x + y)"
    2.98 -apply (rule eq_Abs_hypreal [of y])
    2.99 +apply (cases y)
   2.100  apply (simp add: starfunRC hypreal_of_real_def hypreal_add)
   2.101  done
   2.102  
   2.103  lemma starfunC_lambda_cancel2:
   2.104      "( *fc* (%h. f(g(x + h)))) y = ( *fc* (f o g)) (hcomplex_of_complex x + y)"
   2.105 -apply (rule eq_Abs_hcomplex [of y])
   2.106 +apply (cases y)
   2.107  apply (simp add: starfunC hcomplex_of_complex_def hcomplex_add)
   2.108  done
   2.109  
   2.110  lemma starfunCR_lambda_cancel2:
   2.111      "( *fcR* (%h. f(g(x + h)))) y = ( *fcR* (f o g)) (hcomplex_of_complex x + y)"
   2.112 -apply (rule eq_Abs_hcomplex [of y])
   2.113 +apply (cases y)
   2.114  apply (simp add: starfunCR hcomplex_of_complex_def hcomplex_add)
   2.115  done
   2.116  
   2.117  lemma starfunRC_lambda_cancel2:
   2.118      "( *fRc* (%h. f(g(x + h)))) y = ( *fRc* (f o g)) (hypreal_of_real x + y)"
   2.119 -apply (rule eq_Abs_hypreal [of y])
   2.120 +apply (cases y)
   2.121  apply (simp add: starfunRC hypreal_of_real_def hypreal_add)
   2.122  done
   2.123  
   2.124 @@ -484,7 +484,7 @@
   2.125  done
   2.126  
   2.127  lemma starfunC_inverse_inverse: "( *fc* inverse) x = inverse(x)"
   2.128 -apply (rule eq_Abs_hcomplex [of x])
   2.129 +apply (cases x)
   2.130  apply (simp add: starfunC hcomplex_inverse)
   2.131  done
   2.132  
   2.133 @@ -521,7 +521,7 @@
   2.134  
   2.135  lemma starfunC_n_mult:
   2.136      "( *fcn* f) z * ( *fcn* g) z = ( *fcn* (% i x. f i x * g i x)) z"
   2.137 -apply (rule eq_Abs_hcomplex [of z])
   2.138 +apply (cases z)
   2.139  apply (simp add: starfunC_n hcomplex_mult)
   2.140  done
   2.141  
   2.142 @@ -529,14 +529,14 @@
   2.143  
   2.144  lemma starfunC_n_add:
   2.145      "( *fcn* f) z + ( *fcn* g) z = ( *fcn* (%i x. f i x + g i x)) z"
   2.146 -apply (rule eq_Abs_hcomplex [of z])
   2.147 +apply (cases z)
   2.148  apply (simp add: starfunC_n hcomplex_add)
   2.149  done
   2.150  
   2.151  (** uminus **)
   2.152  
   2.153  lemma starfunC_n_minus: "- ( *fcn* g) z = ( *fcn* (%i x. - g i x)) z"
   2.154 -apply (rule eq_Abs_hcomplex [of z])
   2.155 +apply (cases z)
   2.156  apply (simp add: starfunC_n hcomplex_minus)
   2.157  done
   2.158  
   2.159 @@ -550,7 +550,7 @@
   2.160  
   2.161  lemma starfunC_n_const_fun [simp]:
   2.162       "( *fcn* (%i x. k)) z = hcomplex_of_complex  k"
   2.163 -apply (rule eq_Abs_hcomplex [of z])
   2.164 +apply (cases z)
   2.165  apply (simp add: starfunC_n hcomplex_of_complex_def)
   2.166  done
   2.167  
   2.168 @@ -582,27 +582,25 @@
   2.169  lemma starfunC_eq_Re_Im_iff:
   2.170      "(( *fc* f) x = z) = ((( *fcR* (%x. Re(f x))) x = hRe (z)) &
   2.171                            (( *fcR* (%x. Im(f x))) x = hIm (z)))"
   2.172 -apply (rule eq_Abs_hcomplex [of x])
   2.173 -apply (rule eq_Abs_hcomplex [of z])
   2.174 +apply (cases x, cases z)
   2.175  apply (auto simp add: starfunCR starfunC hIm hRe complex_Re_Im_cancel_iff, ultra+)
   2.176  done
   2.177  
   2.178  lemma starfunC_approx_Re_Im_iff:
   2.179      "(( *fc* f) x @c= z) = ((( *fcR* (%x. Re(f x))) x @= hRe (z)) &
   2.180                              (( *fcR* (%x. Im(f x))) x @= hIm (z)))"
   2.181 -apply (rule eq_Abs_hcomplex [of x])
   2.182 -apply (rule eq_Abs_hcomplex [of z])
   2.183 +apply (cases x, cases z)
   2.184  apply (simp add: starfunCR starfunC hIm hRe capprox_approx_iff)
   2.185  done
   2.186  
   2.187  lemma starfunC_Idfun_capprox:
   2.188      "x @c= hcomplex_of_complex a ==> ( *fc* (%x. x)) x @c= hcomplex_of_complex  a"
   2.189 -apply (rule eq_Abs_hcomplex [of x])
   2.190 +apply (cases x)
   2.191  apply (simp add: starfunC)
   2.192  done
   2.193  
   2.194  lemma starfunC_Id [simp]: "( *fc* (%x. x)) x = x"
   2.195 -apply (rule eq_Abs_hcomplex [of x])
   2.196 +apply (cases x)
   2.197  apply (simp add: starfunC)
   2.198  done
   2.199  
     3.1 --- a/src/HOL/Complex/NSCA.thy	Mon Mar 15 10:46:19 2004 +0100
     3.2 +++ b/src/HOL/Complex/NSCA.thy	Mon Mar 15 10:58:29 2004 +0100
     3.3 @@ -724,8 +724,7 @@
     3.4  
     3.5  lemma hcomplex_of_hypreal_capprox_iff [simp]:
     3.6       "(hcomplex_of_hypreal x @c= hcomplex_of_hypreal z) = (x @= z)"
     3.7 -apply (rule eq_Abs_hypreal [of x])
     3.8 -apply (rule eq_Abs_hypreal [of z])
     3.9 +apply (cases x, cases z)
    3.10  apply (simp add: hcomplex_of_hypreal capprox_approx_iff)
    3.11  done
    3.12  
    3.13 @@ -1133,13 +1132,13 @@
    3.14  
    3.15  lemma CFinite_HFinite_hcomplex_of_hypreal:
    3.16       "z \<in> HFinite ==> hcomplex_of_hypreal z \<in> CFinite"
    3.17 -apply (rule eq_Abs_hypreal [of z])
    3.18 +apply (cases z)
    3.19  apply (simp add: hcomplex_of_hypreal CFinite_HFinite_iff hypreal_zero_def [symmetric])
    3.20  done
    3.21  
    3.22  lemma SComplex_SReal_hcomplex_of_hypreal:
    3.23       "x \<in> Reals ==>  hcomplex_of_hypreal x \<in> SComplex"
    3.24 -apply (rule eq_Abs_hypreal [of x])
    3.25 +apply (cases x)
    3.26  apply (simp add: hcomplex_of_hypreal SComplex_SReal_iff hypreal_zero_def [symmetric])
    3.27  done
    3.28  
    3.29 @@ -1178,32 +1177,28 @@
    3.30  lemma hcomplex_split_CInfinitesimal_iff:
    3.31       "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CInfinitesimal) =  
    3.32        (x \<in> Infinitesimal & y \<in> Infinitesimal)"
    3.33 -apply (rule eq_Abs_hypreal [of x])
    3.34 -apply (rule eq_Abs_hypreal [of y])
    3.35 +apply (cases x, cases y)
    3.36  apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CInfinitesimal_Infinitesimal_iff)
    3.37  done
    3.38  
    3.39  lemma hcomplex_split_CFinite_iff:
    3.40       "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CFinite) =  
    3.41        (x \<in> HFinite & y \<in> HFinite)"
    3.42 -apply (rule eq_Abs_hypreal [of x])
    3.43 -apply (rule eq_Abs_hypreal [of y])
    3.44 +apply (cases x, cases y)
    3.45  apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CFinite_HFinite_iff)
    3.46  done
    3.47  
    3.48  lemma hcomplex_split_SComplex_iff:
    3.49       "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> SComplex) =  
    3.50        (x \<in> Reals & y \<in> Reals)"
    3.51 -apply (rule eq_Abs_hypreal [of x])
    3.52 -apply (rule eq_Abs_hypreal [of y])
    3.53 +apply (cases x, cases y)
    3.54  apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal SComplex_SReal_iff)
    3.55  done
    3.56  
    3.57  lemma hcomplex_split_CInfinite_iff:
    3.58       "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CInfinite) =  
    3.59        (x \<in> HInfinite | y \<in> HInfinite)"
    3.60 -apply (rule eq_Abs_hypreal [of x])
    3.61 -apply (rule eq_Abs_hypreal [of y])
    3.62 +apply (cases x, cases y)
    3.63  apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CInfinite_HInfinite_iff)
    3.64  done
    3.65  
    3.66 @@ -1211,10 +1206,7 @@
    3.67       "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @c=  
    3.68         hcomplex_of_hypreal x' + iii * hcomplex_of_hypreal y') =  
    3.69        (x @= x' & y @= y')"
    3.70 -apply (rule eq_Abs_hypreal [of x])
    3.71 -apply (rule eq_Abs_hypreal [of y])
    3.72 -apply (rule eq_Abs_hypreal [of x'])
    3.73 -apply (rule eq_Abs_hypreal [of y'])
    3.74 +apply (cases x, cases y, cases x', cases y')
    3.75  apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal capprox_approx_iff)
    3.76  done
    3.77  
     4.1 --- a/src/HOL/Complex/NSComplex.thy	Mon Mar 15 10:46:19 2004 +0100
     4.2 +++ b/src/HOL/Complex/NSComplex.thy	Mon Mar 15 10:58:29 2004 +0100
     4.3 @@ -190,6 +190,10 @@
     4.4  apply (force simp add: Rep_hcomplex_inverse hcomplexrel_def)
     4.5  done
     4.6  
     4.7 +theorem hcomplex_cases [case_names Abs_hcomplex, cases type: hcomplex]:
     4.8 +    "(!!x. z = Abs_hcomplex(hcomplexrel``{x}) ==> P) ==> P"
     4.9 +by (rule eq_Abs_hcomplex [of z], blast)
    4.10 +
    4.11  lemma hcomplexrel_iff [simp]:
    4.12     "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
    4.13  by (simp add: hcomplexrel_def)
    4.14 @@ -215,8 +219,7 @@
    4.15  
    4.16  lemma hcomplex_hRe_hIm_cancel_iff:
    4.17       "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
    4.18 -apply (rule eq_Abs_hcomplex [of z])
    4.19 -apply (rule eq_Abs_hcomplex [of w])
    4.20 +apply (cases z, cases w)
    4.21  apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff iff: hcomplexrel_iff)
    4.22  apply (ultra+)
    4.23  done
    4.24 @@ -253,20 +256,17 @@
    4.25  done
    4.26  
    4.27  lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z"
    4.28 -apply (rule eq_Abs_hcomplex [of z])
    4.29 -apply (rule eq_Abs_hcomplex [of w])
    4.30 +apply (cases z, cases w)
    4.31  apply (simp add: complex_add_commute hcomplex_add)
    4.32  done
    4.33  
    4.34  lemma hcomplex_add_assoc: "((z1::hcomplex) + z2) + z3 = z1 + (z2 + z3)"
    4.35 -apply (rule eq_Abs_hcomplex [of z1])
    4.36 -apply (rule eq_Abs_hcomplex [of z2])
    4.37 -apply (rule eq_Abs_hcomplex [of z3])
    4.38 +apply (cases z1, cases z2, cases z3)
    4.39  apply (simp add: hcomplex_add complex_add_assoc)
    4.40  done
    4.41  
    4.42  lemma hcomplex_add_zero_left: "(0::hcomplex) + z = z"
    4.43 -apply (rule eq_Abs_hcomplex [of z])
    4.44 +apply (cases z)
    4.45  apply (simp add: hcomplex_zero_def hcomplex_add)
    4.46  done
    4.47  
    4.48 @@ -274,14 +274,12 @@
    4.49  by (simp add: hcomplex_add_zero_left hcomplex_add_commute)
    4.50  
    4.51  lemma hRe_add: "hRe(x + y) = hRe(x) + hRe(y)"
    4.52 -apply (rule eq_Abs_hcomplex [of x])
    4.53 -apply (rule eq_Abs_hcomplex [of y])
    4.54 +apply (cases x, cases y)
    4.55  apply (simp add: hRe hcomplex_add hypreal_add complex_Re_add)
    4.56  done
    4.57  
    4.58  lemma hIm_add: "hIm(x + y) = hIm(x) + hIm(y)"
    4.59 -apply (rule eq_Abs_hcomplex [of x])
    4.60 -apply (rule eq_Abs_hcomplex [of y])
    4.61 +apply (cases x, cases y)
    4.62  apply (simp add: hIm hcomplex_add hypreal_add complex_Im_add)
    4.63  done
    4.64  
    4.65 @@ -301,7 +299,7 @@
    4.66  done
    4.67  
    4.68  lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)"
    4.69 -apply (rule eq_Abs_hcomplex [of z])
    4.70 +apply (cases z)
    4.71  apply (simp add: hcomplex_add hcomplex_minus hcomplex_zero_def)
    4.72  done
    4.73  
    4.74 @@ -318,33 +316,28 @@
    4.75  done
    4.76  
    4.77  lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w"
    4.78 -apply (rule eq_Abs_hcomplex [of w])
    4.79 -apply (rule eq_Abs_hcomplex [of z])
    4.80 +apply (cases w, cases z)
    4.81  apply (simp add: hcomplex_mult complex_mult_commute)
    4.82  done
    4.83  
    4.84  lemma hcomplex_mult_assoc: "((u::hcomplex) * v) * w = u * (v * w)"
    4.85 -apply (rule eq_Abs_hcomplex [of u])
    4.86 -apply (rule eq_Abs_hcomplex [of v])
    4.87 -apply (rule eq_Abs_hcomplex [of w])
    4.88 +apply (cases u, cases v, cases w)
    4.89  apply (simp add: hcomplex_mult complex_mult_assoc)
    4.90  done
    4.91  
    4.92  lemma hcomplex_mult_one_left: "(1::hcomplex) * z = z"
    4.93 -apply (rule eq_Abs_hcomplex [of z])
    4.94 +apply (cases z)
    4.95  apply (simp add: hcomplex_one_def hcomplex_mult)
    4.96  done
    4.97  
    4.98  lemma hcomplex_mult_zero_left: "(0::hcomplex) * z = 0"
    4.99 -apply (rule eq_Abs_hcomplex [of z])
   4.100 +apply (cases z)
   4.101  apply (simp add: hcomplex_zero_def hcomplex_mult)
   4.102  done
   4.103  
   4.104  lemma hcomplex_add_mult_distrib:
   4.105       "((z1::hcomplex) + z2) * w = (z1 * w) + (z2 * w)"
   4.106 -apply (rule eq_Abs_hcomplex [of z1])
   4.107 -apply (rule eq_Abs_hcomplex [of z2])
   4.108 -apply (rule eq_Abs_hcomplex [of w])
   4.109 +apply (cases z1, cases z2, cases w)
   4.110  apply (simp add: hcomplex_mult hcomplex_add left_distrib)
   4.111  done
   4.112  
   4.113 @@ -366,7 +359,7 @@
   4.114  
   4.115  lemma hcomplex_mult_inv_left:
   4.116        "z \<noteq> (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)"
   4.117 -apply (rule eq_Abs_hcomplex [of z])
   4.118 +apply (cases z)
   4.119  apply (simp add: hcomplex_zero_def hcomplex_one_def hcomplex_inverse hcomplex_mult, ultra)
   4.120  apply (rule ccontr)
   4.121  apply (drule left_inverse, auto)
   4.122 @@ -414,12 +407,12 @@
   4.123  subsection{*More Minus Laws*}
   4.124  
   4.125  lemma hRe_minus: "hRe(-z) = - hRe(z)"
   4.126 -apply (rule eq_Abs_hcomplex [of z])
   4.127 +apply (cases z)
   4.128  apply (simp add: hRe hcomplex_minus hypreal_minus complex_Re_minus)
   4.129  done
   4.130  
   4.131  lemma hIm_minus: "hIm(-z) = - hIm(z)"
   4.132 -apply (rule eq_Abs_hcomplex [of z])
   4.133 +apply (cases z)
   4.134  apply (simp add: hIm hcomplex_minus hypreal_minus complex_Im_minus)
   4.135  done
   4.136  
   4.137 @@ -484,28 +477,26 @@
   4.138  
   4.139  lemma hcomplex_of_hypreal_cancel_iff [iff]:
   4.140       "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
   4.141 -apply (rule eq_Abs_hypreal [of x])
   4.142 -apply (rule eq_Abs_hypreal [of y])
   4.143 +apply (cases x, cases y)
   4.144  apply (simp add: hcomplex_of_hypreal)
   4.145  done
   4.146  
   4.147  lemma hcomplex_of_hypreal_minus:
   4.148       "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
   4.149 -apply (rule eq_Abs_hypreal [of x])
   4.150 +apply (cases x)
   4.151  apply (simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus)
   4.152  done
   4.153  
   4.154  lemma hcomplex_of_hypreal_inverse:
   4.155       "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
   4.156 -apply (rule eq_Abs_hypreal [of x])
   4.157 +apply (cases x)
   4.158  apply (simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse)
   4.159  done
   4.160  
   4.161  lemma hcomplex_of_hypreal_add:
   4.162       "hcomplex_of_hypreal x + hcomplex_of_hypreal y =
   4.163        hcomplex_of_hypreal (x + y)"
   4.164 -apply (rule eq_Abs_hypreal [of x])
   4.165 -apply (rule eq_Abs_hypreal [of y])
   4.166 +apply (cases x, cases y)
   4.167  apply (simp add: hcomplex_of_hypreal hypreal_add hcomplex_add complex_of_real_add)
   4.168  done
   4.169  
   4.170 @@ -517,8 +508,7 @@
   4.171  lemma hcomplex_of_hypreal_mult:
   4.172       "hcomplex_of_hypreal x * hcomplex_of_hypreal y =
   4.173        hcomplex_of_hypreal (x * y)"
   4.174 -apply (rule eq_Abs_hypreal [of x])
   4.175 -apply (rule eq_Abs_hypreal [of y])
   4.176 +apply (cases x, cases y)
   4.177  apply (simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult complex_of_real_mult)
   4.178  done
   4.179  
   4.180 @@ -537,12 +527,12 @@
   4.181  by (simp add: hcomplex_zero_def hypreal_zero_def hcomplex_of_hypreal)
   4.182  
   4.183  lemma hRe_hcomplex_of_hypreal [simp]: "hRe(hcomplex_of_hypreal z) = z"
   4.184 -apply (rule eq_Abs_hypreal [of z])
   4.185 +apply (cases z)
   4.186  apply (auto simp add: hcomplex_of_hypreal hRe)
   4.187  done
   4.188  
   4.189  lemma hIm_hcomplex_of_hypreal [simp]: "hIm(hcomplex_of_hypreal z) = 0"
   4.190 -apply (rule eq_Abs_hypreal [of z])
   4.191 +apply (cases z)
   4.192  apply (auto simp add: hcomplex_of_hypreal hIm hypreal_zero_num)
   4.193  done
   4.194  
   4.195 @@ -554,14 +544,12 @@
   4.196  subsection{*HComplex theorems*}
   4.197  
   4.198  lemma hRe_HComplex [simp]: "hRe (HComplex x y) = x"
   4.199 -apply (rule eq_Abs_hypreal [of x])
   4.200 -apply (rule eq_Abs_hypreal [of y])
   4.201 +apply (cases x, cases y)
   4.202  apply (simp add: HComplex_def hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
   4.203  done
   4.204  
   4.205  lemma hIm_HComplex [simp]: "hIm (HComplex x y) = y"
   4.206 -apply (rule eq_Abs_hypreal [of x])
   4.207 -apply (rule eq_Abs_hypreal [of y])
   4.208 +apply (cases x, cases y)
   4.209  apply (simp add: HComplex_def hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
   4.210  done
   4.211  
   4.212 @@ -597,7 +585,7 @@
   4.213  by (simp add: hcomplex_one_def hcmod hypreal_one_num)
   4.214  
   4.215  lemma hcmod_hcomplex_of_hypreal [simp]: "hcmod(hcomplex_of_hypreal x) = abs x"
   4.216 -apply (rule eq_Abs_hypreal [of x])
   4.217 +apply (cases x)
   4.218  apply (auto simp add: hcmod hcomplex_of_hypreal hypreal_hrabs)
   4.219  done
   4.220  
   4.221 @@ -610,10 +598,7 @@
   4.222  apply (rule iffI) 
   4.223   prefer 2 apply simp 
   4.224  apply (simp add: HComplex_def iii_def) 
   4.225 -apply (rule eq_Abs_hypreal [of x])
   4.226 -apply (rule eq_Abs_hypreal [of y])
   4.227 -apply (rule eq_Abs_hypreal [of x'])
   4.228 -apply (rule eq_Abs_hypreal [of y'])
   4.229 +apply (cases x, cases y, cases x', cases y')
   4.230  apply (auto simp add: iii_def hcomplex_mult hcomplex_add hcomplex_of_hypreal)
   4.231  apply (ultra+) 
   4.232  done
   4.233 @@ -676,52 +661,48 @@
   4.234  done
   4.235  
   4.236  lemma hcomplex_hcnj_cancel_iff [iff]: "(hcnj x = hcnj y) = (x = y)"
   4.237 -apply (rule eq_Abs_hcomplex [of x])
   4.238 -apply (rule eq_Abs_hcomplex [of y])
   4.239 +apply (cases x, cases y)
   4.240  apply (simp add: hcnj)
   4.241  done
   4.242  
   4.243  lemma hcomplex_hcnj_hcnj [simp]: "hcnj (hcnj z) = z"
   4.244 -apply (rule eq_Abs_hcomplex [of z])
   4.245 +apply (cases z)
   4.246  apply (simp add: hcnj)
   4.247  done
   4.248  
   4.249  lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]:
   4.250       "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
   4.251 -apply (rule eq_Abs_hypreal [of x])
   4.252 +apply (cases x)
   4.253  apply (simp add: hcnj hcomplex_of_hypreal)
   4.254  done
   4.255  
   4.256  lemma hcomplex_hmod_hcnj [simp]: "hcmod (hcnj z) = hcmod z"
   4.257 -apply (rule eq_Abs_hcomplex [of z])
   4.258 +apply (cases z)
   4.259  apply (simp add: hcnj hcmod)
   4.260  done
   4.261  
   4.262  lemma hcomplex_hcnj_minus: "hcnj (-z) = - hcnj z"
   4.263 -apply (rule eq_Abs_hcomplex [of z])
   4.264 +apply (cases z)
   4.265  apply (simp add: hcnj hcomplex_minus complex_cnj_minus)
   4.266  done
   4.267  
   4.268  lemma hcomplex_hcnj_inverse: "hcnj(inverse z) = inverse(hcnj z)"
   4.269 -apply (rule eq_Abs_hcomplex [of z])
   4.270 +apply (cases z)
   4.271  apply (simp add: hcnj hcomplex_inverse complex_cnj_inverse)
   4.272  done
   4.273  
   4.274  lemma hcomplex_hcnj_add: "hcnj(w + z) = hcnj(w) + hcnj(z)"
   4.275 -apply (rule eq_Abs_hcomplex [of z])
   4.276 -apply (rule eq_Abs_hcomplex [of w])
   4.277 +apply (cases z, cases w)
   4.278  apply (simp add: hcnj hcomplex_add complex_cnj_add)
   4.279  done
   4.280  
   4.281  lemma hcomplex_hcnj_diff: "hcnj(w - z) = hcnj(w) - hcnj(z)"
   4.282 -apply (rule eq_Abs_hcomplex [of z])
   4.283 -apply (rule eq_Abs_hcomplex [of w])
   4.284 +apply (cases z, cases w)
   4.285  apply (simp add: hcnj hcomplex_diff complex_cnj_diff)
   4.286  done
   4.287  
   4.288  lemma hcomplex_hcnj_mult: "hcnj(w * z) = hcnj(w) * hcnj(z)"
   4.289 -apply (rule eq_Abs_hcomplex [of z])
   4.290 -apply (rule eq_Abs_hcomplex [of w])
   4.291 +apply (cases z, cases w)
   4.292  apply (simp add: hcnj hcomplex_mult complex_cnj_mult)
   4.293  done
   4.294  
   4.295 @@ -735,13 +716,13 @@
   4.296  by (simp add: hcomplex_zero_def hcnj)
   4.297  
   4.298  lemma hcomplex_hcnj_zero_iff [iff]: "(hcnj z = 0) = (z = 0)"
   4.299 -apply (rule eq_Abs_hcomplex [of z])
   4.300 +apply (cases z)
   4.301  apply (simp add: hcomplex_zero_def hcnj)
   4.302  done
   4.303  
   4.304  lemma hcomplex_mult_hcnj:
   4.305       "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
   4.306 -apply (rule eq_Abs_hcomplex [of z])
   4.307 +apply (cases z)
   4.308  apply (simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add
   4.309                        hypreal_mult complex_mult_cnj numeral_2_eq_2)
   4.310  done
   4.311 @@ -750,7 +731,7 @@
   4.312  subsection{*More Theorems about the Function @{term hcmod}*}
   4.313  
   4.314  lemma hcomplex_hcmod_eq_zero_cancel [simp]: "(hcmod x = 0) = (x = 0)"
   4.315 -apply (rule eq_Abs_hcomplex [of x])
   4.316 +apply (cases x)
   4.317  apply (simp add: hcmod hcomplex_zero_def hypreal_zero_num)
   4.318  done
   4.319  
   4.320 @@ -765,17 +746,17 @@
   4.321  done
   4.322  
   4.323  lemma hcmod_minus [simp]: "hcmod (-x) = hcmod(x)"
   4.324 -apply (rule eq_Abs_hcomplex [of x])
   4.325 +apply (cases x)
   4.326  apply (simp add: hcmod hcomplex_minus)
   4.327  done
   4.328  
   4.329  lemma hcmod_mult_hcnj: "hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
   4.330 -apply (rule eq_Abs_hcomplex [of z])
   4.331 +apply (cases z)
   4.332  apply (simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj numeral_2_eq_2)
   4.333  done
   4.334  
   4.335  lemma hcmod_ge_zero [simp]: "(0::hypreal) \<le> hcmod x"
   4.336 -apply (rule eq_Abs_hcomplex [of x])
   4.337 +apply (cases x)
   4.338  apply (simp add: hcmod hypreal_zero_num hypreal_le)
   4.339  done
   4.340  
   4.341 @@ -783,15 +764,13 @@
   4.342  by (simp add: abs_if linorder_not_less)
   4.343  
   4.344  lemma hcmod_mult: "hcmod(x*y) = hcmod(x) * hcmod(y)"
   4.345 -apply (rule eq_Abs_hcomplex [of x])
   4.346 -apply (rule eq_Abs_hcomplex [of y])
   4.347 +apply (cases x, cases y)
   4.348  apply (simp add: hcmod hcomplex_mult hypreal_mult complex_mod_mult)
   4.349  done
   4.350  
   4.351  lemma hcmod_add_squared_eq:
   4.352       "hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)"
   4.353 -apply (rule eq_Abs_hcomplex [of x])
   4.354 -apply (rule eq_Abs_hcomplex [of y])
   4.355 +apply (cases x, cases y)
   4.356  apply (simp add: hcmod hcomplex_add hypreal_mult hRe hcnj hcomplex_mult
   4.357                        numeral_2_eq_2 realpow_two [symmetric]
   4.358                    del: realpow_Suc)
   4.359 @@ -801,8 +780,7 @@
   4.360  done
   4.361  
   4.362  lemma hcomplex_hRe_mult_hcnj_le_hcmod [simp]: "hRe(x * hcnj y) \<le> hcmod(x * hcnj y)"
   4.363 -apply (rule eq_Abs_hcomplex [of x])
   4.364 -apply (rule eq_Abs_hcomplex [of y])
   4.365 +apply (cases x, cases y)
   4.366  apply (simp add: hcmod hcnj hcomplex_mult hRe hypreal_le)
   4.367  done
   4.368  
   4.369 @@ -812,8 +790,7 @@
   4.370  done
   4.371  
   4.372  lemma hcmod_triangle_squared [simp]: "hcmod (x + y) ^ 2 \<le> (hcmod(x) + hcmod(y)) ^ 2"
   4.373 -apply (rule eq_Abs_hcomplex [of x])
   4.374 -apply (rule eq_Abs_hcomplex [of y])
   4.375 +apply (cases x, cases y)
   4.376  apply (simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add
   4.377                        hypreal_le realpow_two [symmetric] numeral_2_eq_2
   4.378              del: realpow_Suc)
   4.379 @@ -821,8 +798,7 @@
   4.380  done
   4.381  
   4.382  lemma hcmod_triangle_ineq [simp]: "hcmod (x + y) \<le> hcmod(x) + hcmod(y)"
   4.383 -apply (rule eq_Abs_hcomplex [of x])
   4.384 -apply (rule eq_Abs_hcomplex [of y])
   4.385 +apply (cases x, cases y)
   4.386  apply (simp add: hcmod hcomplex_add hypreal_add hypreal_le)
   4.387  done
   4.388  
   4.389 @@ -832,34 +808,26 @@
   4.390  done
   4.391  
   4.392  lemma hcmod_diff_commute: "hcmod (x - y) = hcmod (y - x)"
   4.393 -apply (rule eq_Abs_hcomplex [of x])
   4.394 -apply (rule eq_Abs_hcomplex [of y])
   4.395 +apply (cases x, cases y)
   4.396  apply (simp add: hcmod hcomplex_diff complex_mod_diff_commute)
   4.397  done
   4.398  
   4.399  lemma hcmod_add_less:
   4.400       "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s"
   4.401 -apply (rule eq_Abs_hcomplex [of x])
   4.402 -apply (rule eq_Abs_hcomplex [of y])
   4.403 -apply (rule eq_Abs_hypreal [of r])
   4.404 -apply (rule eq_Abs_hypreal [of s])
   4.405 +apply (cases x, cases y, cases r, cases s)
   4.406  apply (simp add: hcmod hcomplex_add hypreal_add hypreal_less, ultra)
   4.407  apply (auto intro: complex_mod_add_less)
   4.408  done
   4.409  
   4.410  lemma hcmod_mult_less:
   4.411       "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s"
   4.412 -apply (rule eq_Abs_hcomplex [of x])
   4.413 -apply (rule eq_Abs_hcomplex [of y])
   4.414 -apply (rule eq_Abs_hypreal [of r])
   4.415 -apply (rule eq_Abs_hypreal [of s])
   4.416 +apply (cases x, cases y, cases r, cases s)
   4.417  apply (simp add: hcmod hypreal_mult hypreal_less hcomplex_mult, ultra)
   4.418  apply (auto intro: complex_mod_mult_less)
   4.419  done
   4.420  
   4.421  lemma hcmod_diff_ineq [simp]: "hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
   4.422 -apply (rule eq_Abs_hcomplex [of a])
   4.423 -apply (rule eq_Abs_hcomplex [of b])
   4.424 +apply (cases a, cases b)
   4.425  apply (simp add: hcmod hcomplex_add hypreal_diff hypreal_le)
   4.426  done
   4.427  
   4.428 @@ -877,14 +845,12 @@
   4.429  
   4.430  lemma hcomplex_of_hypreal_hyperpow:
   4.431       "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
   4.432 -apply (rule eq_Abs_hypreal [of x])
   4.433 -apply (rule eq_Abs_hypnat [of n])
   4.434 +apply (cases x, cases n)
   4.435  apply (simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow)
   4.436  done
   4.437  
   4.438  lemma hcmod_hcpow: "hcmod(x hcpow n) = hcmod(x) pow n"
   4.439 -apply (rule eq_Abs_hcomplex [of x])
   4.440 -apply (rule eq_Abs_hypnat [of n])
   4.441 +apply (cases x, cases n)
   4.442  apply (simp add: hcpow hyperpow hcmod complex_mod_complexpow)
   4.443  done
   4.444  
   4.445 @@ -935,22 +901,18 @@
   4.446  lemma hcpow_minus:
   4.447       "(-x::hcomplex) hcpow n =
   4.448        (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"
   4.449 -apply (rule eq_Abs_hcomplex [of x])
   4.450 -apply (rule eq_Abs_hypnat [of n])
   4.451 +apply (cases x, cases n)
   4.452  apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus, ultra)
   4.453  apply (auto simp add: neg_power_if, ultra)
   4.454  done
   4.455  
   4.456  lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
   4.457 -apply (rule eq_Abs_hcomplex [of r])
   4.458 -apply (rule eq_Abs_hcomplex [of s])
   4.459 -apply (rule eq_Abs_hypnat [of n])
   4.460 +apply (cases r, cases s, cases n)
   4.461  apply (simp add: hcpow hypreal_mult hcomplex_mult power_mult_distrib)
   4.462  done
   4.463  
   4.464  lemma hcpow_zero [simp]: "0 hcpow (n + 1) = 0"
   4.465 -apply (simp add: hcomplex_zero_def hypnat_one_def)
   4.466 -apply (rule eq_Abs_hypnat [of n])
   4.467 +apply (simp add: hcomplex_zero_def hypnat_one_def, cases n)
   4.468  apply (simp add: hcpow hypnat_add)
   4.469  done
   4.470  
   4.471 @@ -958,8 +920,7 @@
   4.472  by (simp add: hSuc_def)
   4.473  
   4.474  lemma hcpow_not_zero [simp,intro]: "r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)"
   4.475 -apply (rule eq_Abs_hcomplex [of r])
   4.476 -apply (rule eq_Abs_hypnat [of n])
   4.477 +apply (cases r, cases n)
   4.478  apply (auto simp add: hcpow hcomplex_zero_def, ultra)
   4.479  done
   4.480  
   4.481 @@ -991,19 +952,18 @@
   4.482  by (simp add: hcomplex_one_def hsgn)
   4.483  
   4.484  lemma hsgn_minus: "hsgn (-z) = - hsgn(z)"
   4.485 -apply (rule eq_Abs_hcomplex [of z])
   4.486 +apply (cases z)
   4.487  apply (simp add: hsgn hcomplex_minus sgn_minus)
   4.488  done
   4.489  
   4.490  lemma hsgn_eq: "hsgn z = z / hcomplex_of_hypreal (hcmod z)"
   4.491 -apply (rule eq_Abs_hcomplex [of z])
   4.492 +apply (cases z)
   4.493  apply (simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq)
   4.494  done
   4.495  
   4.496  
   4.497  lemma hcmod_i: "hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)"
   4.498 -apply (rule eq_Abs_hypreal [of x])
   4.499 -apply (rule eq_Abs_hypreal [of y]) 
   4.500 +apply (cases x, cases y) 
   4.501  apply (simp add: HComplex_eq_Abs_hcomplex_Complex starfun 
   4.502                   hypreal_mult hypreal_add hcmod numeral_2_eq_2)
   4.503  done
   4.504 @@ -1029,12 +989,12 @@
   4.505  by (simp add: i_eq_HComplex_0_1) 
   4.506  
   4.507  lemma hRe_hsgn [simp]: "hRe(hsgn z) = hRe(z)/hcmod z"
   4.508 -apply (rule eq_Abs_hcomplex [of z])
   4.509 +apply (cases z)
   4.510  apply (simp add: hsgn hcmod hRe hypreal_divide)
   4.511  done
   4.512  
   4.513  lemma hIm_hsgn [simp]: "hIm(hsgn z) = hIm(z)/hcmod z"
   4.514 -apply (rule eq_Abs_hcomplex [of z])
   4.515 +apply (cases z)
   4.516  apply (simp add: hsgn hcmod hIm hypreal_divide)
   4.517  done
   4.518  
   4.519 @@ -1045,8 +1005,7 @@
   4.520       "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
   4.521        hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
   4.522        iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
   4.523 -apply (rule eq_Abs_hypreal [of x])
   4.524 -apply (rule eq_Abs_hypreal [of y])
   4.525 +apply (cases x, cases y)
   4.526  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)
   4.527  apply (simp add: diff_minus) 
   4.528  done
   4.529 @@ -1060,20 +1019,18 @@
   4.530  
   4.531  lemma hRe_mult_i_eq[simp]:
   4.532      "hRe (iii * hcomplex_of_hypreal y) = 0"
   4.533 -apply (simp add: iii_def)
   4.534 -apply (rule eq_Abs_hypreal [of y])
   4.535 +apply (simp add: iii_def, cases y)
   4.536  apply (simp add: hcomplex_of_hypreal hcomplex_mult hRe hypreal_zero_num)
   4.537  done
   4.538  
   4.539  lemma hIm_mult_i_eq [simp]:
   4.540      "hIm (iii * hcomplex_of_hypreal y) = y"
   4.541 -apply (simp add: iii_def)
   4.542 -apply (rule eq_Abs_hypreal [of y])
   4.543 +apply (simp add: iii_def, cases y)
   4.544  apply (simp add: hcomplex_of_hypreal hcomplex_mult hIm hypreal_zero_num)
   4.545  done
   4.546  
   4.547  lemma hcmod_mult_i [simp]: "hcmod (iii * hcomplex_of_hypreal y) = abs y"
   4.548 -apply (rule eq_Abs_hypreal [of y])
   4.549 +apply (cases y)
   4.550  apply (simp add: hcomplex_of_hypreal hcmod hypreal_hrabs iii_def hcomplex_mult)
   4.551  done
   4.552  
   4.553 @@ -1094,14 +1051,14 @@
   4.554  
   4.555  lemma cos_harg_i_mult_zero_pos:
   4.556       "0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
   4.557 -apply (rule eq_Abs_hypreal [of y])
   4.558 +apply (cases y)
   4.559  apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
   4.560                  hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
   4.561  done
   4.562  
   4.563  lemma cos_harg_i_mult_zero_neg:
   4.564       "y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
   4.565 -apply (rule eq_Abs_hypreal [of y])
   4.566 +apply (cases y)
   4.567  apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
   4.568                   hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
   4.569  done
   4.570 @@ -1113,7 +1070,7 @@
   4.571  
   4.572  lemma hcomplex_of_hypreal_zero_iff [simp]:
   4.573       "(hcomplex_of_hypreal y = 0) = (y = 0)"
   4.574 -apply (rule eq_Abs_hypreal [of y])
   4.575 +apply (cases y)
   4.576  apply (simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
   4.577  done
   4.578  
   4.579 @@ -1134,7 +1091,7 @@
   4.580  
   4.581  lemma hcomplex_split_polar:
   4.582    "\<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
   4.583 -apply (rule eq_Abs_hcomplex [of z])
   4.584 +apply (cases z)
   4.585  apply (simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult HComplex_def)
   4.586  apply (cut_tac z = x in complex_split_polar2)
   4.587  apply (drule choice, safe)+
   4.588 @@ -1153,7 +1110,7 @@
   4.589     "hcis a =
   4.590      (hcomplex_of_hypreal(( *f* cos) a) +
   4.591      iii * hcomplex_of_hypreal(( *f* sin) a))"
   4.592 -apply (rule eq_Abs_hypreal [of a])
   4.593 +apply (cases a)
   4.594  apply (simp add: starfun hcis hcomplex_of_hypreal iii_def hcomplex_mult hcomplex_add cis_def)
   4.595  done
   4.596  
   4.597 @@ -1186,7 +1143,7 @@
   4.598  
   4.599  lemma hcmod_unit_one [simp]:
   4.600       "hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
   4.601 -apply (rule eq_Abs_hypreal [of a]) 
   4.602 +apply (cases a) 
   4.603  apply (simp add: HComplex_def iii_def starfun hcomplex_of_hypreal 
   4.604                   hcomplex_mult hcmod hcomplex_add hypreal_one_def)
   4.605  done
   4.606 @@ -1210,19 +1167,14 @@
   4.607  
   4.608  lemma hrcis_mult:
   4.609    "hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
   4.610 -apply (simp add: hrcis_def)
   4.611 -apply (rule eq_Abs_hypreal [of r1])
   4.612 -apply (rule eq_Abs_hypreal [of r2])
   4.613 -apply (rule eq_Abs_hypreal [of a])
   4.614 -apply (rule eq_Abs_hypreal [of b])
   4.615 +apply (simp add: hrcis_def, cases r1, cases r2, cases a, cases b)
   4.616  apply (simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal
   4.617                        hcomplex_mult cis_mult [symmetric]
   4.618                        complex_of_real_mult [symmetric])
   4.619  done
   4.620  
   4.621  lemma hcis_mult: "hcis a * hcis b = hcis (a + b)"
   4.622 -apply (rule eq_Abs_hypreal [of a])
   4.623 -apply (rule eq_Abs_hypreal [of b])
   4.624 +apply (cases a, cases b)
   4.625  apply (simp add: hcis hcomplex_mult hypreal_add cis_mult)
   4.626  done
   4.627  
   4.628 @@ -1230,13 +1182,12 @@
   4.629  by (simp add: hcomplex_one_def hcis hypreal_zero_num)
   4.630  
   4.631  lemma hrcis_zero_mod [simp]: "hrcis 0 a = 0"
   4.632 -apply (simp add: hcomplex_zero_def)
   4.633 -apply (rule eq_Abs_hypreal [of a])
   4.634 +apply (simp add: hcomplex_zero_def, cases a)
   4.635  apply (simp add: hrcis hypreal_zero_num)
   4.636  done
   4.637  
   4.638  lemma hrcis_zero_arg [simp]: "hrcis r 0 = hcomplex_of_hypreal r"
   4.639 -apply (rule eq_Abs_hypreal [of r])
   4.640 +apply (cases r)
   4.641  apply (simp add: hrcis hypreal_zero_num hcomplex_of_hypreal)
   4.642  done
   4.643  
   4.644 @@ -1248,7 +1199,7 @@
   4.645  
   4.646  lemma hcis_hypreal_of_nat_Suc_mult:
   4.647     "hcis (hypreal_of_nat (Suc n) * a) = hcis a * hcis (hypreal_of_nat n * a)"
   4.648 -apply (rule eq_Abs_hypreal [of a])
   4.649 +apply (cases a)
   4.650  apply (simp add: hypreal_of_nat hcis hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
   4.651  done
   4.652  
   4.653 @@ -1260,14 +1211,12 @@
   4.654  lemma hcis_hypreal_of_hypnat_Suc_mult:
   4.655       "hcis (hypreal_of_hypnat (n + 1) * a) =
   4.656        hcis a * hcis (hypreal_of_hypnat n * a)"
   4.657 -apply (rule eq_Abs_hypreal [of a])
   4.658 -apply (rule eq_Abs_hypnat [of n])
   4.659 +apply (cases a, cases n)
   4.660  apply (simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
   4.661  done
   4.662  
   4.663  lemma NSDeMoivre_ext: "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)"
   4.664 -apply (rule eq_Abs_hypreal [of a])
   4.665 -apply (rule eq_Abs_hypnat [of n])
   4.666 +apply (cases a, cases n)
   4.667  apply (simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre)
   4.668  done
   4.669  
   4.670 @@ -1282,24 +1231,23 @@
   4.671  done
   4.672  
   4.673  lemma hcis_inverse [simp]: "inverse(hcis a) = hcis (-a)"
   4.674 -apply (rule eq_Abs_hypreal [of a])
   4.675 +apply (cases a)
   4.676  apply (simp add: hcomplex_inverse hcis hypreal_minus)
   4.677  done
   4.678  
   4.679  lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)"
   4.680 -apply (rule eq_Abs_hypreal [of a])
   4.681 -apply (rule eq_Abs_hypreal [of r])
   4.682 +apply (cases a, cases r)
   4.683  apply (simp add: hcomplex_inverse hrcis hypreal_minus hypreal_inverse rcis_inverse, ultra)
   4.684  apply (simp add: real_divide_def)
   4.685  done
   4.686  
   4.687  lemma hRe_hcis [simp]: "hRe(hcis a) = ( *f* cos) a"
   4.688 -apply (rule eq_Abs_hypreal [of a])
   4.689 +apply (cases a)
   4.690  apply (simp add: hcis starfun hRe)
   4.691  done
   4.692  
   4.693  lemma hIm_hcis [simp]: "hIm(hcis a) = ( *f* sin) a"
   4.694 -apply (rule eq_Abs_hypreal [of a])
   4.695 +apply (cases a)
   4.696  apply (simp add: hcis starfun hIm)
   4.697  done
   4.698  
   4.699 @@ -1316,9 +1264,7 @@
   4.700  by (simp add: NSDeMoivre_ext)
   4.701  
   4.702  lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)"
   4.703 -apply (simp add: hexpi_def)
   4.704 -apply (rule eq_Abs_hcomplex [of a])
   4.705 -apply (rule eq_Abs_hcomplex [of b])
   4.706 +apply (simp add: hexpi_def, cases a, cases b)
   4.707  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)
   4.708  done
   4.709  
     5.1 --- a/src/HOL/Complex/NSInduct.thy	Mon Mar 15 10:46:19 2004 +0100
     5.2 +++ b/src/HOL/Complex/NSInduct.thy	Mon Mar 15 10:58:29 2004 +0100
     5.3 @@ -35,7 +35,7 @@
     5.4      "(( *pNat* P) 0 &
     5.5              (\<forall>n. ( *pNat* P)(n) --> ( *pNat* P)(n + 1)))
     5.6         --> ( *pNat* P)(n)"
     5.7 -apply (rule eq_Abs_hypnat [of n])
     5.8 +apply (cases n)
     5.9  apply (auto simp add: hypnat_zero_def hypnat_one_def starPNat, ultra)
    5.10  apply (erule nat_induct)
    5.11  apply (drule_tac x = "hypnat_of_nat n" in spec)