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 -lemma NSCLIM_NSCRLIM_Im:
1.38 - "f -- a --NSC> L ==> (%x. Im(f x)) -- a --NSCR> Im(L)"
1.39 -apply (unfold NSCLIM_def NSCRLIM_def)
1.40 -apply (rule eq_Abs_hcomplex [of x])
1.41 -apply (auto simp add: starfunC_approx_Re_Im_iff hIm_hcomplex_of_complex)
1.42 -done
1.43 +
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)