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