# HG changeset patch
# User huffman
# Date 1158849953 -7200
# Node ID 66b8455090b8f0ff297b2aeb64531d43ae171c16
# Parent  2586df9fb95ad17c81aa923dc024731d053c4e30
changed constants into abbreviations; shortened proofs

diff -r 2586df9fb95a -r 66b8455090b8 src/HOL/Complex/CLim.thy
--- a/src/HOL/Complex/CLim.thy	Thu Sep 21 15:41:18 2006 +0200
+++ b/src/HOL/Complex/CLim.thy	Thu Sep 21 16:45:53 2006 +0200
@@ -33,51 +33,86 @@
 apply (drule sym [THEN diff_eq_eq [THEN iffD2]], auto)
 done
 
-definition
+abbreviation
 
   CLIM :: "[complex=>complex,complex,complex] => bool"
 				("((_)/ -- (_)/ --C> (_))" [60, 0, 60] 60)
+  "CLIM == LIM"
+
+  NSCLIM :: "[complex=>complex,complex,complex] => bool"
+			      ("((_)/ -- (_)/ --NSC> (_))" [60, 0, 60] 60)
+  "NSCLIM == NSLIM"
+
+  (* f: C --> R *)
+  CRLIM :: "[complex=>real,complex,real] => bool"
+				("((_)/ -- (_)/ --CR> (_))" [60, 0, 60] 60)
+  "CRLIM == LIM"
+
+  NSCRLIM :: "[complex=>real,complex,real] => bool"
+			      ("((_)/ -- (_)/ --NSCR> (_))" [60, 0, 60] 60)
+  "NSCRLIM == NSLIM"
+
+
+  isContc :: "[complex=>complex,complex] => bool"
+  "isContc == isCont"
+
+  (* NS definition dispenses with limit notions *)
+  isNSContc :: "[complex=>complex,complex] => bool"
+  "isNSContc == isNSCont"
+
+  isContCR :: "[complex=>real,complex] => bool"
+  "isContCR == isCont"
+
+  (* NS definition dispenses with limit notions *)
+  isNSContCR :: "[complex=>real,complex] => bool"
+  "isNSContCR == isNSCont"
+
+
+lemma CLIM_def:
   "f -- a --C> L =
      (\<forall>r. 0 < r -->
 	     (\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (cmod(x - a) < s)
 			  --> cmod(f x - L) < r))))"
+by (rule LIM_def)
 
-  NSCLIM :: "[complex=>complex,complex,complex] => bool"
-			      ("((_)/ -- (_)/ --NSC> (_))" [60, 0, 60] 60)
+lemma NSCLIM_def:
   "f -- a --NSC> L = (\<forall>x. (x \<noteq> hcomplex_of_complex a &
            		         x @= hcomplex_of_complex a
                                    --> ( *f* f) x @= hcomplex_of_complex L))"
+by (rule NSLIM_def)
 
-  (* f: C --> R *)
-  CRLIM :: "[complex=>real,complex,real] => bool"
-				("((_)/ -- (_)/ --CR> (_))" [60, 0, 60] 60)
+lemma CRLIM_def:
   "f -- a --CR> L =
      (\<forall>r. 0 < r -->
 	     (\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (cmod(x - a) < s)
 			  --> abs(f x - L) < r))))"
+by (simp add: LIM_def)
 
-  NSCRLIM :: "[complex=>real,complex,real] => bool"
-			      ("((_)/ -- (_)/ --NSCR> (_))" [60, 0, 60] 60)
+lemma NSCRLIM_def:
   "f -- a --NSCR> L = (\<forall>x. (x \<noteq> hcomplex_of_complex a &
            		         x @= hcomplex_of_complex a
                                    --> ( *f* f) x @= hypreal_of_real L))"
-
+by (rule NSLIM_def)
 
-  isContc :: "[complex=>complex,complex] => bool"
+lemma isContc_def:
   "isContc f a = (f -- a --C> (f a))"
+by (rule isCont_def)
 
-  (* NS definition dispenses with limit notions *)
-  isNSContc :: "[complex=>complex,complex] => bool"
+lemma isNSContc_def:
   "isNSContc f a = (\<forall>y. y @= hcomplex_of_complex a -->
 			   ( *f* f) y @= hcomplex_of_complex (f a))"
+by (rule isNSCont_def)
 
-  isContCR :: "[complex=>real,complex] => bool"
+lemma isContCR_def:
   "isContCR f a = (f -- a --CR> (f a))"
+by (rule isCont_def)
 
-  (* NS definition dispenses with limit notions *)
-  isNSContCR :: "[complex=>real,complex] => bool"
+lemma isNSContCR_def:
   "isNSContCR f a = (\<forall>y. y @= hcomplex_of_complex a -->
 			   ( *f* f) y @= hypreal_of_real (f a))"
+by (rule isNSCont_def)
+
+definition
 
   (* differentiation: D is derivative of function f at x *)
   cderiv:: "[complex=>complex,complex,complex] => bool"
@@ -112,25 +147,17 @@
 subsection{*Limit of Complex to Complex Function*}
 
 lemma NSCLIM_NSCRLIM_Re: "f -- a --NSC> L ==> (%x. Re(f x)) -- a --NSCR> Re(L)"
-by (simp add: NSCLIM_def NSCRLIM_def starfunC_approx_Re_Im_iff 
+by (simp add: NSLIM_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)"
-by (simp add: NSCLIM_def NSCRLIM_def starfunC_approx_Re_Im_iff 
+by (simp add: NSLIM_def starfunC_approx_Re_Im_iff 
               hIm_hcomplex_of_complex)
 
 lemma CLIM_NSCLIM:
       "f -- x --C> L ==> f -- x --NSC> L"
-apply (simp add: CLIM_def NSCLIM_def approx_def, auto)
-apply (rule_tac x = xa in star_cases)
-apply (auto simp add: starfun star_n_diff star_of_def star_n_eq_iff
-         Infinitesimal_hcmod_iff hcmod diff_def [symmetric])
-apply (auto simp add: Infinitesimal_FreeUltrafilterNat_iff)
-apply (drule_tac x = u in spec, auto)
-apply (drule_tac x = s in spec, auto, ultra)
-apply (auto)
-done
+by (rule LIM_NSLIM)
 
 lemma eq_Abs_star_ALL: "(\<forall>t. P t) = (\<forall>X. P (star_n X))"
 apply auto
@@ -165,43 +192,18 @@
 
 lemma NSCLIM_CLIM:
      "f -- x --NSC> L ==> f -- x --C> L"
-apply (simp add: CLIM_def NSCLIM_def)
-apply (rule ccontr) 
-apply (auto simp add: eq_Abs_star_ALL starfun
-            Infinitesimal_approx_minus [symmetric] star_n_diff
-            Infinitesimal_hcmod_iff star_of_def star_n_eq_iff
-            hcmod)
-apply (auto simp add: Infinitesimal_FreeUltrafilterNat_iff)
-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_Infinitesimal])
-apply (simp add: Infinitesimal_hcmod_iff star_of_def
-            Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod)
-apply (drule_tac x = r in spec, clarify)
-apply (drule FreeUltrafilterNat_all, ultra)
-done
+by (rule NSLIM_LIM)
 
 
 text{*First key result*}
 theorem CLIM_NSCLIM_iff: "(f -- x --C> L) = (f -- x --NSC> L)"
-by (blast intro: CLIM_NSCLIM NSCLIM_CLIM)
+by (rule LIM_NSLIM_iff)
 
 
 subsection{*Limit of Complex to Real Function*}
 
 lemma CRLIM_NSCRLIM: "f -- x --CR> L ==> f -- x --NSCR> L"
-apply (simp add: CRLIM_def NSCRLIM_def approx_def, auto)
-apply (rule_tac x = xa in star_cases)
-apply (auto simp add: starfun star_n_diff
-              Infinitesimal_hcmod_iff hcmod
-              star_of_def star_n_eq_iff
-              diff_def [symmetric])
-apply (auto simp add: Infinitesimal_FreeUltrafilterNat_iff)
-apply (drule_tac x = u in spec, auto)
-apply (drule_tac x = s in spec, auto, ultra)
-apply (auto)
-done
+by (rule LIM_NSLIM)
 
 lemma lemma_CRLIM:
      "\<forall>s. 0 < s --> (\<exists>xa.  xa \<noteq> x &
@@ -229,27 +231,11 @@
 by auto
 
 lemma NSCRLIM_CRLIM: "f -- x --NSCR> L ==> f -- x --CR> L"
-apply (simp add: CRLIM_def NSCRLIM_def approx_def)
-apply (rule ccontr) 
-apply (auto simp add: eq_Abs_star_ALL starfun star_n_diff 
-             Infinitesimal_hcmod_iff 
-             hcmod Infinitesimal_approx_minus [symmetric]
-             star_of_def star_n_eq_iff
-             diff_def [symmetric])
-apply (auto simp add: Infinitesimal_FreeUltrafilterNat_iff)
-apply (simp add: linorder_not_less)
-apply (drule lemma_skolemize_CRLIM2, safe)
-apply (drule_tac x = X in spec, auto)
-apply (drule lemma_crsimp [THEN complex_seq_to_hcomplex_Infinitesimal])
-apply (simp add: Infinitesimal_hcmod_iff star_of_def
-             Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod)
-apply (drule_tac x = r in spec, clarify)
-apply (drule FreeUltrafilterNat_all, ultra)
-done
+by (rule NSLIM_LIM)
 
 text{*Second key result*}
 theorem CRLIM_NSCRLIM_iff: "(f -- x --CR> L) = (f -- x --NSCR> L)"
-by (blast intro: CRLIM_NSCRLIM NSCRLIM_CRLIM)
+by (rule LIM_NSLIM_iff)
 
 (** get this result easily now **)
 lemma CLIM_CRLIM_Re: "f -- a --C> L ==> (%x. Re(f x)) -- a --CR> Re(L)"
@@ -269,40 +255,40 @@
 lemma NSCLIM_add:
      "[| f -- x --NSC> l; g -- x --NSC> m |]
       ==> (%x. f(x) + g(x)) -- x --NSC> (l + m)"
-by (auto simp: NSCLIM_def intro!: approx_add)
+by (rule NSLIM_add)
 
 lemma CLIM_add:
      "[| f -- x --C> l; g -- x --C> m |]
       ==> (%x. f(x) + g(x)) -- x --C> (l + m)"
-by (simp add: CLIM_NSCLIM_iff NSCLIM_add)
+by (rule LIM_add)
 
 (*** NSLIM_mult hence CLIM_mult *)
 
 lemma NSCLIM_mult:
      "[| f -- x --NSC> l; g -- x --NSC> m |]
       ==> (%x. f(x) * g(x)) -- x --NSC> (l * m)"
-by (auto simp add: NSCLIM_def intro!: approx_mult_HFinite)
+by (rule NSLIM_mult)
 
 lemma CLIM_mult:
      "[| f -- x --C> l; g -- x --C> m |]
       ==> (%x. f(x) * g(x)) -- x --C> (l * m)"
-by (simp add: CLIM_NSCLIM_iff NSCLIM_mult)
+by (rule LIM_mult2)
 
 (*** NSCLIM_const and CLIM_const ***)
 
 lemma NSCLIM_const [simp]: "(%x. k) -- x --NSC> k"
-by (simp add: NSCLIM_def)
+by (rule NSLIM_const)
 
 lemma CLIM_const [simp]: "(%x. k) -- x --C> k"
-by (simp add: CLIM_def)
+by (rule LIM_const)
 
 (*** NSCLIM_minus and CLIM_minus ***)
 
 lemma NSCLIM_minus: "f -- a --NSC> L ==> (%x. -f(x)) -- a --NSC> -L"
-by (simp add: NSCLIM_def)
+by (rule NSLIM_minus)
 
 lemma CLIM_minus: "f -- a --C> L ==> (%x. -f(x)) -- a --C> -L"
-by (simp add: CLIM_NSCLIM_iff NSCLIM_minus)
+by (rule LIM_minus)
 
 (*** NSCLIM_diff hence CLIM_diff ***)
 
@@ -314,22 +300,19 @@
 lemma CLIM_diff:
      "[| f -- x --C> l; g -- x --C> m |]
       ==> (%x. f(x) - g(x)) -- x --C> (l - m)"
-by (simp add: CLIM_NSCLIM_iff NSCLIM_diff)
+by (rule LIM_diff)
 
 (*** NSCLIM_inverse and hence CLIM_inverse *)
 
 lemma NSCLIM_inverse:
      "[| f -- a --NSC> L;  L \<noteq> 0 |]
       ==> (%x. inverse(f(x))) -- a --NSC> (inverse L)"
-apply (simp add: NSCLIM_def, clarify)
-apply (drule spec)
-apply (force simp add: hcomplex_of_complex_approx_inverse)
-done
+by (rule NSLIM_inverse)
 
 lemma CLIM_inverse:
      "[| f -- a --C> L;  L \<noteq> 0 |]
       ==> (%x. inverse(f(x))) -- a --C> (inverse L)"
-by (simp add: CLIM_NSCLIM_iff NSCLIM_inverse)
+by (rule LIM_inverse)
 
 (*** NSCLIM_zero, CLIM_zero, etc. ***)
 
@@ -343,10 +326,10 @@
 by (simp add: CLIM_NSCLIM_iff NSCLIM_zero)
 
 lemma NSCLIM_zero_cancel: "(%x. f(x) - l) -- x --NSC> 0 ==> f -- x --NSC> l"
-by (drule_tac g = "%x. l" and m = l in NSCLIM_add, auto)
+by (rule NSLIM_zero_cancel)
 
 lemma CLIM_zero_cancel: "(%x. f(x) - l) -- x --C> 0 ==> f -- x --C> l"
-by (drule_tac g = "%x. l" and m = l in CLIM_add, auto)
+by (rule LIM_zero_cancel)
 
 (*** NSCLIM_not zero and hence CLIM_not_zero ***)
 
@@ -372,7 +355,7 @@
 done
 
 lemma CLIM_const_eq: "(%x. k) -- x --C> L ==> k = L"
-by (simp add: CLIM_NSCLIM_iff NSCLIM_const_eq)
+by (rule LIM_const_eq)
 
 (*** NSCLIM and hence CLIM are unique ***)
 
@@ -383,25 +366,25 @@
 done
 
 lemma CLIM_unique: "[| f -- x --C> L; f -- x --C> M |] ==> L = M"
-by (simp add: CLIM_NSCLIM_iff NSCLIM_unique)
+by (rule LIM_unique)
 
 (***  NSCLIM_mult_zero and CLIM_mult_zero ***)
 
 lemma NSCLIM_mult_zero:
      "[| f -- x --NSC> 0; g -- x --NSC> 0 |] ==> (%x. f(x)*g(x)) -- x --NSC> 0"
-by (drule NSCLIM_mult, auto)
+by (rule NSLIM_mult_zero)
 
 lemma CLIM_mult_zero:
      "[| f -- x --C> 0; g -- x --C> 0 |] ==> (%x. f(x)*g(x)) -- x --C> 0"
-by (drule CLIM_mult, auto)
+by (rule LIM_mult_zero)
 
 (*** NSCLIM_self hence CLIM_self ***)
 
 lemma NSCLIM_self: "(%x. x) -- a --NSC> a"
-by (auto simp add: NSCLIM_def intro: starfunC_Idfun_approx)
+by (rule NSLIM_self)
 
 lemma CLIM_self: "(%x. x) -- a --C> a"
-by (simp add: CLIM_NSCLIM_iff NSCLIM_self)
+by (rule LIM_self)
 
 (** another equivalence result **)
 lemma NSCLIM_NSCRLIM_iff:
@@ -445,100 +428,85 @@
 by (simp add: isNSContc_def)
 
 lemma isNSContc_NSCLIM: "isNSContc f a ==> f -- a --NSC> (f a) "
-by (simp add: isNSContc_def NSCLIM_def)
+by (rule isNSCont_NSLIM)
 
 lemma NSCLIM_isNSContc:
       "f -- a --NSC> (f a) ==> isNSContc f a"
-apply (simp add: isNSContc_def NSCLIM_def, auto)
-apply (case_tac "y = hcomplex_of_complex a", auto)
-done
+by (rule NSLIM_isNSCont)
 
 text{*Nonstandard continuity can be defined using NS Limit in 
 similar fashion to standard definition of continuity*}
 
 lemma isNSContc_NSCLIM_iff: "(isNSContc f a) = (f -- a --NSC> (f a))"
-by (blast intro: isNSContc_NSCLIM NSCLIM_isNSContc)
+by (rule isNSCont_NSLIM_iff)
 
 lemma isNSContc_CLIM_iff: "(isNSContc f a) = (f -- a --C> (f a))"
-by (simp add: CLIM_NSCLIM_iff isNSContc_NSCLIM_iff)
+by (rule isNSCont_LIM_iff)
 
 (*** key result for continuity ***)
 lemma isNSContc_isContc_iff: "(isNSContc f a) = (isContc f a)"
-by (simp add: isContc_def isNSContc_CLIM_iff)
+by (rule isNSCont_isCont_iff)
 
 lemma isContc_isNSContc: "isContc f a ==> isNSContc f a"
-by (erule isNSContc_isContc_iff [THEN iffD2])
+by (rule isCont_isNSCont)
 
 lemma isNSContc_isContc: "isNSContc f a ==> isContc f a"
-by (erule isNSContc_isContc_iff [THEN iffD1])
+by (rule isNSCont_isCont)
 
 
 text{*Alternative definition of continuity*}
 lemma NSCLIM_h_iff: "(f -- a --NSC> L) = ((%h. f(a + h)) -- 0 --NSC> L)"
-apply (simp add: NSCLIM_def, auto)
-apply (drule_tac x = "hcomplex_of_complex a + x" in spec)
-apply (drule_tac [2] x = "- hcomplex_of_complex a + x" in spec, safe, simp)
-apply (rule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
-apply (rule_tac [4] approx_minus_iff2 [THEN iffD1])
- prefer 3 apply (simp add: compare_rls add_commute)
-apply (rule_tac [2] x = x in star_cases)
-apply (rule_tac [4] x = x in star_cases)
-apply (auto simp add: starfun star_n_minus star_n_add star_of_def)
-done
+by (rule NSLIM_h_iff)
 
 lemma NSCLIM_isContc_iff:
      "(f -- a --NSC> f a) = ((%h. f(a + h)) -- 0 --NSC> f a)"
 by (rule NSCLIM_h_iff)
 
 lemma CLIM_isContc_iff: "(f -- a --C> f a) = ((%h. f(a + h)) -- 0 --C> f(a))"
-by (simp add: CLIM_NSCLIM_iff NSCLIM_isContc_iff)
+by (rule LIM_isCont_iff)
 
 lemma isContc_iff: "(isContc f x) = ((%h. f(x + h)) -- 0 --C> f(x))"
-by (simp add: isContc_def CLIM_isContc_iff)
+by (rule isCont_iff)
 
 lemma isContc_add:
      "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) + g(x)) a"
-by (auto intro: approx_add simp add: isNSContc_isContc_iff [symmetric] isNSContc_def)
+by (rule isCont_add)
 
 lemma isContc_mult:
      "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) * g(x)) a"
-by (auto intro!: starfun_mult_HFinite_approx
-            [simplified starfun_mult [symmetric]]
-            simp add: isNSContc_isContc_iff [symmetric] isNSContc_def)
+by (rule isCont_mult)
 
 
 lemma isContc_o: "[| isContc f a; isContc g (f a) |] ==> isContc (g o f) a"
-by (simp add: isNSContc_isContc_iff [symmetric] isNSContc_def starfun_o [symmetric])
+by (rule isCont_o)
 
 lemma isContc_o2:
      "[| isContc f a; isContc g (f a) |] ==> isContc (%x. g (f x)) a"
-by (auto dest: isContc_o simp add: o_def)
+by (rule isCont_o2)
 
 lemma isNSContc_minus: "isNSContc f a ==> isNSContc (%x. - f x) a"
-by (simp add: isNSContc_def)
+by (rule isNSCont_minus)
 
 lemma isContc_minus: "isContc f a ==> isContc (%x. - f x) a"
-by (simp add: isNSContc_isContc_iff [symmetric] isNSContc_minus)
+by (rule isCont_minus)
 
 lemma isContc_inverse:
       "[| isContc f x; f x \<noteq> 0 |] ==> isContc (%x. inverse (f x)) x"
-by (simp add: isContc_def CLIM_inverse)
+by (rule isCont_inverse)
 
 lemma isNSContc_inverse:
      "[| isNSContc f x; f x \<noteq> 0 |] ==> isNSContc (%x. inverse (f x)) x"
-by (auto intro: isContc_inverse simp add: isNSContc_isContc_iff)
+by (rule isNSCont_inverse)
 
 lemma isContc_diff:
       "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) - g(x)) a"
-apply (simp add: diff_minus)
-apply (auto intro: isContc_add isContc_minus)
-done
+by (rule isCont_diff)
 
 lemma isContc_const [simp]: "isContc (%x. k) a"
-by (simp add: isContc_def)
+by (rule isCont_const)
 
 lemma isNSContc_const [simp]: "isNSContc (%x. k) a"
-by (simp add: isNSContc_def)
+by (rule isNSCont_const)
 
 
 subsection{*Functions from Complex to Reals*}
@@ -549,28 +517,26 @@
 by (simp add: isNSContCR_def)
 
 lemma isNSContCR_NSCRLIM: "isNSContCR f a ==> f -- a --NSCR> (f a) "
-by (simp add: isNSContCR_def NSCRLIM_def)
+by (rule isNSCont_NSLIM)
 
 lemma NSCRLIM_isNSContCR: "f -- a --NSCR> (f a) ==> isNSContCR f a"
-apply (auto simp add: isNSContCR_def NSCRLIM_def)
-apply (case_tac "y = hcomplex_of_complex a", auto)
-done
+by (rule NSLIM_isNSCont)
 
 lemma isNSContCR_NSCRLIM_iff: "(isNSContCR f a) = (f -- a --NSCR> (f a))"
-by (blast intro: isNSContCR_NSCRLIM NSCRLIM_isNSContCR)
+by (rule isNSCont_NSLIM_iff)
 
 lemma isNSContCR_CRLIM_iff: "(isNSContCR f a) = (f -- a --CR> (f a))"
-by (simp add: CRLIM_NSCRLIM_iff isNSContCR_NSCRLIM_iff)
+by (rule isNSCont_LIM_iff)
 
 (*** another key result for continuity ***)
 lemma isNSContCR_isContCR_iff: "(isNSContCR f a) = (isContCR f a)"
-by (simp add: isContCR_def isNSContCR_CRLIM_iff)
+by (rule isNSCont_isCont_iff)
 
 lemma isContCR_isNSContCR: "isContCR f a ==> isNSContCR f a"
-by (erule isNSContCR_isContCR_iff [THEN iffD2])
+by (rule isCont_isNSCont)
 
 lemma isNSContCR_isContCR: "isNSContCR f a ==> isContCR f a"
-by (erule isNSContCR_isContCR_iff [THEN iffD1])
+by (rule isNSCont_isCont)
 
 lemma isNSContCR_cmod [simp]: "isNSContCR cmod (a)"
 by (auto intro: approx_hcmod_approx