(* -*- holl -*- *)

(* ========================================================================= *)
(*  Generalities.                                                            *)
(* ========================================================================= *)

needs "Examples/binomial.ml";;
prioritize_num ();;
prioritize_complex ();;

let SING_SUBSET = prove
  (`!s x. {x} SUBSET s <=> x IN s`,
   REWRITE_TAC [SUBSET; IN_SING] THEN MESON_TAC[]);;

let BINOM_PENULT = prove
  (`!n. binom(SUC n,n) = SUC n`,
   INDUCT_TAC THEN ASM_REWRITE_TAC [binom; ONE; BINOM_REFL] THEN
   SUBGOAL_THEN `binom(n,SUC n)=0` SUBST1_TAC THENL
   [REWRITE_TAC [BINOM_EQ_0; LT]; REWRITE_TAC [ADD; ADD_0; ADD_SUC; SUC_INJ]]);;

let SERIES_VSUM = prove
  (`!f l k s. FINITE s /\ s SUBSET k /\ (!x. ~(x IN s) ==> f x = vec 0) /\
	      vsum s f = l ==> (f sums l) k`,
   REPEAT STRIP_TAC THEN EXPAND_TAC "l" THEN
   SUBGOAL_THEN `s INTER k = s:num->bool` ASSUME_TAC THENL
   [SET_TAC []; ASM_MESON_TAC [SERIES_FINITE_SUPPORT]]);;

let VSUM_SUC = prove
  (`!f m n. vsum (SUC n..SUC m) f = vsum (n..m) (f o SUC)`,
   REPEAT GEN_TAC THEN
   SUBGOAL_THEN `SUC n..SUC m = IMAGE SUC (n..m)` SUBST1_TAC THENL
   [REWRITE_TAC [ADD1; NUMSEG_OFFSET_IMAGE] THEN
    REWRITE_TAC [ONE; ADD_SUC; ADD_0; ETA_AX];
    SIMP_TAC [VSUM_IMAGE; FINITE_NUMSEG; SUC_INJ]]);;

let CONTINUOUS_OPEN_PREIMAGE = prove
  (`!f:real^M->real^N s t.
      f continuous_on s /\ open s /\ open t
      ==> open {x | x IN s /\ f(x) IN t}`,
   REPEAT STRIP_TAC THEN
   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [CONTINUOUS_ON_OPEN]) THEN
   REWRITE_TAC [OPEN_IN_OPEN] THEN
   DISCH_THEN(MP_TAC o SPEC `IMAGE (f:real^M->real^N) s INTER t`) THEN
   ANTS_TAC THENL
   [EXISTS_TAC `t:real^N->bool` THEN ASM_REWRITE_TAC [];
    STRIP_TAC THEN
    SUBGOAL_THEN `{x | x IN s /\ (f:real^M->real^N) x IN t} =
                 s INTER t'` SUBST1_TAC THENL
    [SET_TAC []; ASM_MESON_TAC [OPEN_INTER]]]);;

let CONTINUOUS_CLOSED_PREIMAGE = prove
  (`!f:real^M->real^N s t.
      f continuous_on s /\ closed s /\ closed t
      ==> closed {x | x IN s /\ f(x) IN t}`,
   REPEAT STRIP_TAC THEN
   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [CONTINUOUS_ON_CLOSED]) THEN
   REWRITE_TAC [CLOSED_IN_CLOSED] THEN
   DISCH_THEN(MP_TAC o SPEC `IMAGE (f:real^M->real^N) s INTER t`) THEN
   ANTS_TAC THENL
   [EXISTS_TAC `t:real^N->bool` THEN ASM_REWRITE_TAC [];
    STRIP_TAC THEN
    SUBGOAL_THEN `{x | x IN s /\ (f:real^M->real^N) x IN t} =
                 s INTER t'` SUBST1_TAC THENL
    [SET_TAC []; ASM_MESON_TAC [CLOSED_INTER]]]);;

let IMAGE_CLOSURE_SUBSET = prove
  (`!f (s:real^N->bool) (t:real^M->bool).
       f continuous_on closure s /\ closed t /\ IMAGE f s SUBSET t
       ==> IMAGE f (closure s) SUBSET t`,
   REPEAT STRIP_TAC THEN
   SUBGOAL_THEN `closure s SUBSET {x | (f:real^N->real^M) x IN t}` MP_TAC
   THENL [MATCH_MP_TAC SUBSET_TRANS; SET_TAC []]  THEN
   EXISTS_TAC `{x | x IN closure s /\ (f:real^N->real^M) x IN t}` THEN
   CONJ_TAC THENL
   [MATCH_MP_TAC CLOSURE_MINIMAL; SET_TAC[]] THEN
   ASM_SIMP_TAC[CONTINUOUS_CLOSED_PREIMAGE; CLOSED_CLOSURE] THEN
   MP_TAC (ISPEC `s:real^N->bool` CLOSURE_SUBSET) THEN SET_TAC[]);;

(* TODO: immergere(?) *)
let CONTINUOUS_ON_CLOSURE_LE = prove
  (`!f:real^N->real^M s x b.
       f continuous_on (closure s) /\
       (!y. y IN s ==> norm (f y) <= b) /\
       x IN (closure s)
       ==> norm (f x) <= b`,
   REWRITE_TAC [GSYM IN_CBALL_0] THEN REPEAT STRIP_TAC THEN
   SUBGOAL_THEN `IMAGE (f:real^N->real^M) (closure s) SUBSET cball(vec 0,b)`
     MP_TAC THENL
   [MATCH_MP_TAC IMAGE_CLOSURE_SUBSET; SET_TAC []] THEN
   ASM_REWRITE_TAC [CLOSED_CBALL] THEN SET_TAC []);;

(* TODO: immergere (?) *)
let REAL_ARCH_RDIV_EQ_0 = prove
  (`!x c. &0 <= x /\ &0 <= c /\ (!m. 0 < m ==> &m * x <= c) ==> x = &0`,
   SIMP_TAC [GSYM REAL_LE_ANTISYM; GSYM REAL_NOT_LT] THEN REPEAT STRIP_TAC THEN
   POP_ASSUM (STRIP_ASSUME_TAC o SPEC `c:real` o MATCH_MP REAL_ARCH) THEN
   ASM_CASES_TAC `n=0` THENL
   [POP_ASSUM SUBST_ALL_TAC THEN
    RULE_ASSUM_TAC (REWRITE_RULE [REAL_MUL_LZERO]) THEN
    ASM_MESON_TAC [REAL_LET_ANTISYM];
    ASM_MESON_TAC [REAL_LET_ANTISYM; REAL_MUL_SYM; LT_NZ]]);;

(* ------------------------------------------------------------------------- *)
(*  Iterates of a function.                                                  *)
(* ------------------------------------------------------------------------- *)

let ITER = define
  `(!f. ITER 0 f x = x) /\
   (!f n. ITER (SUC n) f x = f (ITER n f x))`;;

let ITER_POINTLESS = prove
  (`(!f. ITER 0 f = I) /\
   (!f n. ITER (SUC n) f = f o ITER n f)`,
   REWRITE_TAC [FUN_EQ_THM; I_THM; o_THM; ITER]);;

let ITER_ALT = prove
  (`(!f x. ITER 0 f x = x) /\
    (!f n x. ITER (SUC n) f x = ITER n f (f x))`,
   REWRITE_TAC [ITER] THEN GEN_TAC THEN INDUCT_TAC THEN
   ASM_REWRITE_TAC [ITER]);;

let ITER_ALT_POINTLESS = prove
  (`(!f x. ITER 0 f = I) /\
    (!f n x. ITER (SUC n) f = ITER n f o f)`,
   REWRITE_TAC [FUN_EQ_THM; I_THM; o_THM; ITER_ALT]);;

let ITER_ADD = prove
  (`!f n m x. ITER n f (ITER m f x) = ITER (n + m) f x`,
   GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ITER; ADD]);;

let ITER_MUL = prove
  (`!f n m x. ITER n (ITER m f) x = ITER (n * m) f x`,
   GEN_TAC THEN INDUCT_TAC THEN
   ASM_REWRITE_TAC[ITER; MULT; ITER_ADD; ADD_AC]);;

let ITER_FIXPOINT = prove
  (`!f n x. f x = x ==> ITER n f x = x`,
   GEN_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC [ITER_ALT]);;

(* ========================================================================= *)
(*  Generalities on analytic functions.                                      *)
(* ========================================================================= *)

let ANALYTIC_ON_UNION = prove
  (`!f s t. f analytic_on (s UNION t) <=> f analytic_on s /\ f analytic_on t`,
   REWRITE_TAC [analytic_on; IN_UNION] THEN MESON_TAC[]);;

let ANALYTIC_ON_UNIONS = prove
  (`!f s. f analytic_on (UNIONS s) <=> (!t. t IN s ==> f analytic_on t)`,
   REWRITE_TAC [analytic_on; IN_UNIONS] THEN MESON_TAC[]);;

let ANALYTIC_ON_HOLOMORPHIC = prove
  (`!f s. f analytic_on s <=> ?t. open t /\ s SUBSET t /\ f holomorphic_on t`,
   REPEAT GEN_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
   EXISTS_TAC `?t. open t /\ s SUBSET t /\ f analytic_on t` THEN CONJ_TAC THENL
   [EQ_TAC THENL
    [DISCH_TAC THEN EXISTS_TAC `UNIONS {u | open u /\ f analytic_on u}` THEN
     SIMP_TAC [IN_ELIM_THM; OPEN_UNIONS; ANALYTIC_ON_UNIONS] THEN
     REWRITE_TAC [SUBSET; IN_UNIONS; IN_ELIM_THM] THEN
     ASM_MESON_TAC [analytic_on; ANALYTIC_ON_OPEN; OPEN_BALL; CENTRE_IN_BALL];
     MESON_TAC [ANALYTIC_ON_SUBSET]];
    MESON_TAC [ANALYTIC_ON_OPEN]]);;

let HAS_COMPLEX_DERIVATIVE_TRANSFORM_WITHIN_OPEN = prove
  (`!f g f' s z. open s /\ z IN s /\ (!w. w IN s ==> f w = g w) /\
                 (f has_complex_derivative f') (at z)
                 ==> (g has_complex_derivative f') (at z)`,
   REWRITE_TAC [has_complex_derivative] THEN
   ASM_MESON_TAC [HAS_DERIVATIVE_TRANSFORM_WITHIN_OPEN]);;

let HIGHER_COMPLEX_DERIVATIVE_MUL = prove
  (`!f g s n z.
      open s /\ f holomorphic_on s /\ g holomorphic_on s /\ z IN s
      ==> higher_complex_derivative n (\w. f w * g w) z =
          vsum (0..n) (\i. Cx(&(binom(n,i))) *
                           higher_complex_derivative i f z *
 	 		   higher_complex_derivative (n-i) g z)`,
   REWRITE_TAC [IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN
   REPEAT DISCH_TAC THEN INDUCT_TAC THEN
   REPEAT STRIP_TAC THEN REWRITE_TAC [NUMSEG_SING; VSUM_SING; SUB] THEN
   REWRITE_TAC [higher_complex_derivative; binom; COMPLEX_MUL_LID] THEN
   MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_DERIVATIVE THEN
   MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_TRANSFORM_WITHIN_OPEN THEN
   EXISTS_TAC `\w. vsum (0..n)
                     (\i. Cx (&(binom (n,i))) *
                          higher_complex_derivative i f w *
                   	  higher_complex_derivative (n-i) g w)` THEN
   EXISTS_TAC `s:complex->bool` THEN ASM_SIMP_TAC [] THEN
   SUBGOAL_THEN `vsum (0..SUC n) (\i. Cx (&(binom (SUC n,i))) *
       		                      higher_complex_derivative i f z *
       		   	              higher_complex_derivative (SUC n-i) g z) =
                 vsum (0..n) (\i. Cx (&(binom (n,i))) *
                                  (higher_complex_derivative i f z *
            	                   higher_complex_derivative (SUC n-i) g z +
                          	   higher_complex_derivative (SUC i) f z *
            	          	   higher_complex_derivative (n-i) g z))`
     SUBST1_TAC THENL
   [SUBGOAL_THEN
        `!i. binom(SUC n,i) = binom(n,i) + if i=0 then 0 else binom(n,PRE i)`
      (fun th -> REWRITE_TAC[th; GSYM REAL_OF_NUM_ADD; CX_ADD]) THENL
    [INDUCT_TAC THEN REWRITE_TAC[binom; NOT_SUC; PRE; ADD_SYM; ADD_0];
     REWRITE_TAC [COMPLEX_ADD_LDISTRIB; COMPLEX_ADD_RDISTRIB]] THEN
    SIMP_TAC [VSUM_ADD; FINITE_NUMSEG] THEN BINOP_TAC THENL
    [REWRITE_TAC [VSUM_CLAUSES_NUMSEG; LE_0] THEN
     SUBGOAL_THEN `binom(n,SUC n)=0` SUBST1_TAC THENL
     [REWRITE_TAC [BINOM_EQ_0] THEN ARITH_TAC; CONV_TAC COMPLEX_RING];
     SIMP_TAC [VSUM_CLAUSES_LEFT; SPEC `SUC n` LE_0] THEN
     REWRITE_TAC [COMPLEX_MUL_LZERO; COMPLEX_ADD_LID; GSYM ADD1;
                  VSUM_SUC; o_DEF; SUB_SUC; NOT_SUC; PRE]];
    MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_VSUM THEN
    REWRITE_TAC [FINITE_NUMSEG; IN_NUMSEG] THEN REPEAT STRIP_TAC THEN
    MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_LMUL_AT THEN
    MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_MUL_AT THEN
    ASM_SIMP_TAC [ETA_AX; ARITH_RULE `i <= n ==> SUC n - i = SUC (n-i)`] THEN
    ASM_MESON_TAC [HAS_COMPLEX_DERIVATIVE_HIGHER_COMPLEX_DERIVATIVE]]);;

let HOLOMORPHIC_ON_COMPOSE = prove
  (`!f g s t. f holomorphic_on s /\ g holomorphic_on t /\
              (!z. z IN s ==> f z IN t)
              ==>  g o f holomorphic_on s`,
   REWRITE_TAC [holomorphic_on] THEN REPEAT STRIP_TAC THEN
   SUBGOAL_THEN `IMAGE (f:complex->complex) s SUBSET t` MP_TAC THENL
   [SET_TAC []; ASM_MESON_TAC [HAS_COMPLEX_DERIVATIVE_WITHIN_SUBSET;
                               COMPLEX_DIFF_CHAIN_WITHIN]]);;

(* ------------------------------------------------------------------------- *)
(*  HAS_COMPLEX_DERIVATIVE_TRANSFORM                                         *)
(* ------------------------------------------------------------------------- *)

let COMPLEX_DERIVATIVE_TRANSFORM_WITHIN_OPEN = prove
  (`!f g s. open s /\ f holomorphic_on s /\ g holomorphic_on s /\ z IN s /\
            (!w. w IN s ==> f w = g w)
 	    ==> complex_derivative f z = complex_derivative g z`,
   REPEAT STRIP_TAC THEN MATCH_MP_TAC COMPLEX_DERIVATIVE_UNIQUE_AT THEN
   ASM_MESON_TAC[HAS_COMPLEX_DERIVATIVE_TRANSFORM_WITHIN_OPEN;
                 HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT;
 		 HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE]);;

let HIGHER_COMPLEX_DERIVATIVE_TRANSFORM_WITHIN_OPEN = prove
  (`!f g s i z.
      open s /\ f holomorphic_on s /\ g holomorphic_on s /\
      (!w. w IN s ==> f w = g w) /\ z IN s
      ==> higher_complex_derivative i f z = higher_complex_derivative i g z`,
   REWRITE_TAC [IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN
   REPEAT DISCH_TAC THEN INDUCT_TAC THEN REPEAT STRIP_TAC THEN
   ASM_SIMP_TAC [higher_complex_derivative] THEN
   MATCH_MP_TAC COMPLEX_DERIVATIVE_TRANSFORM_WITHIN_OPEN THEN
   ASM_MESON_TAC [HOLOMORPHIC_HIGHER_COMPLEX_DERIVATIVE]);;

(* ------------------------------------------------------------------------- *)
(*  complex_differentiable                                                   *)
(* ------------------------------------------------------------------------- *)

let COMPLEX_DIFFERENTIABLE_COMPOSE = prove
  (`!f g z. f complex_differentiable at z /\ g complex_differentiable at (f z)
           ==> (g o f) complex_differentiable at z`,
   REWRITE_TAC [complex_differentiable] THEN
   MESON_TAC [COMPLEX_DIFF_CHAIN_AT]);;

let COMPLEX_DERIVATIVE_CHAIN = prove
  (`!f g z. f complex_differentiable at z /\ g complex_differentiable at (f z)
            ==> complex_derivative (g o f) z =
                complex_derivative g (f z) * complex_derivative f z`,
   MESON_TAC [HAS_COMPLEX_DERIVATIVE_DERIVATIVE; COMPLEX_DIFF_CHAIN_AT;
              HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE]);;

(* ------------------------------------------------------------------------- *)
(*  complex_derivative                                                       *)
(* ------------------------------------------------------------------------- *)

let COMPLEX_DERIVATIVE_ID = prove
  (`complex_derivative (\w.w) = \z. Cx(&1)`,
   REWRITE_TAC [FUN_EQ_THM] THEN
   MESON_TAC [HAS_COMPLEX_DERIVATIVE_DERIVATIVE; HAS_COMPLEX_DERIVATIVE_ID]);;

let COMPLEX_DERIVATIVE_CONST = prove
  (`!c. complex_derivative (\w.c) = \z. Cx(&0)`,
   REWRITE_TAC [FUN_EQ_THM] THEN
   MESON_TAC [HAS_COMPLEX_DERIVATIVE_DERIVATIVE;
              HAS_COMPLEX_DERIVATIVE_CONST]);;

let COMPLEX_DERIVATIVE_ADD = prove
  (`!f g z. f complex_differentiable at z /\ g complex_differentiable at z
            ==> complex_derivative (\w. f w + g w) z =
                complex_derivative f z + complex_derivative g z`,
   REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_DERIVATIVE THEN
   ASM_SIMP_TAC [HAS_COMPLEX_DERIVATIVE_ADD;
                 HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE]);;

let COMPLEX_DERIVATIVE_SUB = prove
  (`!f g z. f complex_differentiable at z /\ g complex_differentiable at z
            ==> complex_derivative (\w. f w - g w) z =
                complex_derivative f z - complex_derivative g z`,
   REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_DERIVATIVE THEN
   ASM_SIMP_TAC [HAS_COMPLEX_DERIVATIVE_SUB;
                 HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE]);;

let COMPLEX_DERIVATIVE_MUL = prove
  (`!f g z. f complex_differentiable at z /\ g complex_differentiable at z
            ==> complex_derivative (\w. f w * g w) z =
                f z * complex_derivative g z + complex_derivative f z * g z`,
   REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_DERIVATIVE THEN
   ASM_SIMP_TAC [HAS_COMPLEX_DERIVATIVE_MUL_AT;
                 HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE]);;

let COMPLEX_DERIVATIVE_LMUL = prove
  (`!f c z. f complex_differentiable at z
              ==> complex_derivative (\w. c * f w) z =
                  c * complex_derivative f z`,
   REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_DERIVATIVE THEN
   ASM_SIMP_TAC [HAS_COMPLEX_DERIVATIVE_LMUL_AT;
                 HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE]);;

let COMPLEX_DERIVATIVE_RMUL = prove
  (`!f c z. f complex_differentiable at z
            ==> complex_derivative (\w. f w * c) z =
                complex_derivative f z * c`,
   REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_DERIVATIVE THEN
   ASM_SIMP_TAC [HAS_COMPLEX_DERIVATIVE_RMUL_AT;
                 HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE]);;

(* ------------------------------------------------------------------------- *)
(*  higher_complex_derivative                                                *)
(* ------------------------------------------------------------------------- *)

let HIGHER_COMPLEX_DERIVATIVE_HOLOMORPHIC_ON = prove
  (`!f s n. open s /\ f holomorphic_on s
            ==> higher_complex_derivative n f holomorphic_on s`,
   REWRITE_TAC [RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
   INDUCT_TAC THEN
   ASM_SIMP_TAC [higher_complex_derivative; HOLOMORPHIC_COMPLEX_DERIVATIVE]);;

let HIGHER_COMPLEX_DERIVATIVE_EQ_ITER = prove
  (`!n. higher_complex_derivative n = ITER n complex_derivative`,
   INDUCT_TAC THEN
   ASM_REWRITE_TAC [FUN_EQ_THM; ITER; higher_complex_derivative]);;

let higher_complex_derivative_alt = prove
  (`(!f z. higher_complex_derivative 0 f = f) /\
    (!f z n. higher_complex_derivative (SUC n) f =
             higher_complex_derivative n (complex_derivative f))`,
   REWRITE_TAC [HIGHER_COMPLEX_DERIVATIVE_EQ_ITER; ITER_ALT]);;

let HIGHER_COMPLEX_DERIVATIVE_CONST = prove
  (`!i c. higher_complex_derivative i (\w.c) = \w. if i=0 then c else Cx(&0)`,
   INDUCT_TAC THEN ASM_REWRITE_TAC [higher_complex_derivative_alt; NOT_SUC;
                                    COMPLEX_DERIVATIVE_CONST; FUN_EQ_THM] THEN
   MESON_TAC[]);;

let HIGHER_COMPLEX_DERIVATIVE_ID = prove
  (`!z i. higher_complex_derivative i (\w.w) z = if i=0 then z else
                                               if i=1 then Cx(&1) else Cx(&0)`,
   GEN_TAC THEN INDUCT_TAC THEN
   ASM_REWRITE_TAC [higher_complex_derivative_alt; NOT_SUC; ONE; SUC_INJ] THEN
   REWRITE_TAC[COMPLEX_DERIVATIVE_ID; HIGHER_COMPLEX_DERIVATIVE_CONST; ONE]);;

let HAS_COMPLEX_DERIVATIVE_ITER_1 = prove
  (`!f n z. f z = z /\ (f has_complex_derivative Cx(&1)) (at z)
            ==> (ITER n f has_complex_derivative Cx(&1)) (at z)`,
   GEN_TAC THEN INDUCT_TAC THEN REPEAT STRIP_TAC THEN
   REWRITE_TAC [ITER_POINTLESS; I_DEF; HAS_COMPLEX_DERIVATIVE_ID] THEN
   SUBGOAL_THEN `Cx(&1) = Cx(&1) * Cx(&1)` SUBST1_TAC THENL
   [REWRITE_TAC [COMPLEX_MUL_LID];
    ASM_SIMP_TAC [ITER_FIXPOINT; COMPLEX_DIFF_CHAIN_AT]]);;

let HIGHER_COMPLEX_DERIVATIVE_ADD = prove
  (`!f g s n z.
      open s /\ f holomorphic_on s /\ g holomorphic_on s /\ z IN s ==>
      higher_complex_derivative n (\w. f w + g w) z  =
      higher_complex_derivative n f z + higher_complex_derivative n g z`,
   REWRITE_TAC [IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN
   REPEAT DISCH_TAC THEN INDUCT_TAC THEN
   REWRITE_TAC [higher_complex_derivative] THEN REPEAT STRIP_TAC THEN
   MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_DERIVATIVE THEN
   MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_TRANSFORM_WITHIN_OPEN THEN
   EXISTS_TAC `(\w. higher_complex_derivative n f w +
                    higher_complex_derivative n g w)` THEN
   EXISTS_TAC `s:complex->bool` THEN ASM_SIMP_TAC [] THEN
   MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_ADD THEN
   REWRITE_TAC [ETA_AX; GSYM higher_complex_derivative] THEN
   ASM_MESON_TAC [HAS_COMPLEX_DERIVATIVE_HIGHER_COMPLEX_DERIVATIVE]);;

let HIGHER_COMPLEX_DERIVATIVE_SUB = prove
  (`!f g s n z.
      open s /\ f holomorphic_on s /\ g holomorphic_on s /\ z IN s ==>
      higher_complex_derivative n (\w. f w - g w) z  =
      higher_complex_derivative n f z - higher_complex_derivative n g z`,
   REWRITE_TAC [IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN
   REPEAT DISCH_TAC THEN INDUCT_TAC THEN
   REWRITE_TAC [higher_complex_derivative] THEN REPEAT STRIP_TAC THEN
   MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_DERIVATIVE THEN
   MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_TRANSFORM_WITHIN_OPEN THEN
   EXISTS_TAC `(\w. higher_complex_derivative n f w -
                    higher_complex_derivative n g w)` THEN
   EXISTS_TAC `s:complex->bool` THEN ASM_SIMP_TAC [] THEN
   MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_SUB THEN
   REWRITE_TAC [ETA_AX; GSYM higher_complex_derivative] THEN
   ASM_MESON_TAC [HAS_COMPLEX_DERIVATIVE_HIGHER_COMPLEX_DERIVATIVE]);;

(* ------------------------------------------------------------------------- *)
(* analytic_at                                                               *)
(* ------------------------------------------------------------------------- *)

let ANALYTIC_AT_BALL = prove
  (`!f z. f analytic_on {z} <=> ?e. &0<e /\ f holomorphic_on ball (z,e)`,
   REWRITE_TAC [analytic_on; IN_SING] THEN MESON_TAC []);;

let ANALYTIC_AT = prove
  (`!f z. f analytic_on {z} <=> ?s. open s /\ z IN s /\ f holomorphic_on s`,
   REWRITE_TAC [ANALYTIC_ON_HOLOMORPHIC; SING_SUBSET]);;

let ANALYTIC_ON_ANALYTIC_AT = prove
  (`!f s. f analytic_on s <=> !z. z IN s ==> f analytic_on {z}`,
   REWRITE_TAC [ANALYTIC_AT_BALL; analytic_on]);;

let ANALYTIC_AT_TWO = prove
  (`!f g z. f analytic_on {z} /\ g analytic_on {z} <=>
     ?s. open s /\ z IN s /\ f holomorphic_on s /\ g holomorphic_on s`,
   REWRITE_TAC [ANALYTIC_AT] THEN
   MESON_TAC [HOLOMORPHIC_ON_SUBSET; OPEN_INTER; INTER_SUBSET; IN_INTER]);;

let ANALYTIC_AT_ADD = prove
  (`!f g z. f analytic_on {z} /\ g analytic_on {z}
      ==> (\w. f w + g w) analytic_on {z}`,
   REWRITE_TAC [ANALYTIC_AT_TWO] THEN REWRITE_TAC [ANALYTIC_AT] THEN
   MESON_TAC [HOLOMORPHIC_ON_ADD]);;

let ANALYTIC_AT_SUB = prove
  (`!f g z. f analytic_on {z} /\ g analytic_on {z}
      ==> (\w. f w - g w) analytic_on {z}`,
   REWRITE_TAC [ANALYTIC_AT_TWO] THEN REWRITE_TAC [ANALYTIC_AT] THEN
   MESON_TAC [HOLOMORPHIC_ON_SUB]);;

let ANALYTIC_AT_MUL = prove
  (`!f g z. f analytic_on {z} /\ g analytic_on {z}
      ==> (\w. f w * g w) analytic_on {z}`,
   REWRITE_TAC [ANALYTIC_AT_TWO] THEN REWRITE_TAC [ANALYTIC_AT] THEN
   MESON_TAC [HOLOMORPHIC_ON_MUL]);;

let ANALYTIC_AT_POW = prove
  (`!f n z. f analytic_on {z}
      ==> (\w. f w pow n) analytic_on {z}`,
   REWRITE_TAC [ANALYTIC_AT] THEN MESON_TAC [HOLOMORPHIC_ON_POW]);;

let ANALYTIC_AT_COMPOSE = prove
 (`!f g z. f analytic_on {z} /\ g analytic_on {f z} ==> g o f analytic_on {z}`,
   REWRITE_TAC [ANALYTIC_AT] THEN REPEAT STRIP_TAC THEN
   EXISTS_TAC `{w:complex | w IN s /\ (f w:complex) IN s'}` THEN
   ASM_SIMP_TAC[CONTINUOUS_OPEN_PREIMAGE;HOLOMORPHIC_ON_IMP_CONTINUOUS_ON] THEN
   CONJ_TAC THENL [SET_TAC[]; MATCH_MP_TAC HOLOMORPHIC_ON_COMPOSE] THEN
   EXISTS_TAC `s':complex->bool` THEN ASM_REWRITE_TAC [] THEN CONJ_TAC THENL
   [MATCH_MP_TAC HOLOMORPHIC_ON_SUBSET THEN SET_TAC []; SET_TAC []]);;

let ANALYTIC_AT_ITER = prove
  (`!f z m. f analytic_on {z} /\ f z = z ==> ITER m f analytic_on {z}`,
   REWRITE_TAC [RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
   SUBGOAL_THEN `!m. ITER m f z = z:complex` ASSUME_TAC THENL
   [INDUCT_TAC THEN ASM_REWRITE_TAC [ITER];
    INDUCT_TAC THEN ASM_SIMP_TAC [ITER_POINTLESS; I_DEF;
                                  ANALYTIC_ON_ID; ANALYTIC_AT_COMPOSE]]);;

(* ------------------------------------------------------------------------- *)
(* COMPLEX_DERIVATIVE_AT                                                     *)
(* ------------------------------------------------------------------------- *)

let COMPLEX_DERIVATIVE_ADD_AT = prove
  (`!f g z. f analytic_on {z} /\ g analytic_on {z}
      ==> complex_derivative (\w. f w + g w) z =
            complex_derivative f z + complex_derivative g z`,
   REWRITE_TAC [ANALYTIC_AT_TWO] THEN REPEAT STRIP_TAC THEN
   MATCH_MP_TAC COMPLEX_DERIVATIVE_ADD THEN
   ASM_MESON_TAC [HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT]);;

let COMPLEX_DERIVATIVE_SUB_AT = prove
  (`!f g z. f analytic_on {z} /\ g analytic_on {z}
      ==> complex_derivative (\w. f w - g w) z =
            complex_derivative f z - complex_derivative g z`,
   REWRITE_TAC [ANALYTIC_AT_TWO] THEN REPEAT STRIP_TAC THEN
   MATCH_MP_TAC COMPLEX_DERIVATIVE_SUB THEN
   ASM_MESON_TAC [HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT]);;

let COMPLEX_DERIVATIVE_MUL_AT = prove
  (`!f g z. f analytic_on {z} /\ g analytic_on {z}
      ==> complex_derivative (\w. f w * g w) z =
            f z * complex_derivative g z + complex_derivative f z * g z`,
   REWRITE_TAC [ANALYTIC_AT_TWO] THEN REPEAT STRIP_TAC THEN
   MATCH_MP_TAC COMPLEX_DERIVATIVE_MUL THEN
   ASM_MESON_TAC [HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT]);;

let COMPLEX_DERIVATIVE_LMUL_AT = prove
  (`!f c z. f analytic_on {z}
     ==> complex_derivative (\w. c * f w) z = c * complex_derivative f z`,
   REWRITE_TAC [ANALYTIC_AT] THEN
   MESON_TAC [HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT; COMPLEX_DERIVATIVE_LMUL]);;

let COMPLEX_DERIVATIVE_RMUL_AT = prove
  (`!f c z. f analytic_on {z}
     ==> complex_derivative (\w. f w * c) z = complex_derivative f z * c`,
   REWRITE_TAC [ANALYTIC_AT] THEN
   MESON_TAC [HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT; COMPLEX_DERIVATIVE_RMUL]);;

let COMPLEX_DERIVATIVE_CHAIN_AT = prove
  (`!f g. f analytic_on {z} /\  g analytic_on {f z}
      ==> complex_derivative (g o f) z =
          complex_derivative g (f z) * complex_derivative f z`,
   REWRITE_TAC [ANALYTIC_AT] THEN
   MESON_TAC [COMPLEX_DERIVATIVE_CHAIN;
              HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT]);;

(* ------------------------------------------------------------------------- *)
(* HIGHER_COMPLEX_DERIVATIVE_AT                                              *)
(* ------------------------------------------------------------------------- *)

let HIGHER_COMPLEX_DERIVATIVE_ADD_AT = prove
  (`!f g n z.
      f analytic_on {z} /\ g analytic_on {z}
      ==> higher_complex_derivative n (\w. f w + g w) z =
          higher_complex_derivative n f z +
          higher_complex_derivative n g z`,
   REWRITE_TAC [ANALYTIC_AT_TWO] THEN
   MESON_TAC [HIGHER_COMPLEX_DERIVATIVE_ADD]);;

let HIGHER_COMPLEX_DERIVATIVE_SUB_AT = prove
  (`!f g n z.
      f analytic_on {z} /\ g analytic_on {z}
      ==> higher_complex_derivative n (\w. f w - g w) z =
          higher_complex_derivative n f z -
          higher_complex_derivative n g z`,
   REWRITE_TAC [ANALYTIC_AT_TWO] THEN
   MESON_TAC [HIGHER_COMPLEX_DERIVATIVE_SUB]);;

let HIGHER_COMPLEX_DERIVATIVE_NEG_AT = prove
  (`!f g n z.
      f analytic_on {z} /\ g analytic_on {z}
      ==> higher_complex_derivative n (\w. f w - g w) z =
          higher_complex_derivative n f z -
          higher_complex_derivative n g z`,
   REWRITE_TAC [ANALYTIC_AT_TWO] THEN
   MESON_TAC [HIGHER_COMPLEX_DERIVATIVE_SUB]);;

let HIGHER_COMPLEX_DERIVATIVE_MUL_AT = prove
  (`!f g n z.
      f analytic_on {z} /\ g analytic_on {z}
      ==> higher_complex_derivative n (\w. f w * g w) z =
          vsum (0..n) (\i. Cx(&(binom(n,i))) *
                           higher_complex_derivative i f z *
 	 		   higher_complex_derivative (n-i) g z)`,
   REWRITE_TAC [ANALYTIC_AT_TWO] THEN
   MESON_TAC [HIGHER_COMPLEX_DERIVATIVE_MUL]);;

(* ------------------------------------------------------------------------- *)
(* Equality between holomorphic functions.                                   *)
(* (Should be generalized for open connected domains.)                       *)
(* ------------------------------------------------------------------------- *)

let HOLOMORPHIC_FUN_EQ_ON_BALL = prove
  (`!f g z r w.
      f holomorphic_on ball(z,r) /\ g holomorphic_on ball(z,r) /\
      w IN ball(z,r) /\ 
      (!n. higher_complex_derivative n f z = higher_complex_derivative n g z)
      ==> f w = g w`,
   REPEAT STRIP_TAC THEN MATCH_MP_TAC SERIES_UNIQUE THEN
   EXISTS_TAC `(\n. higher_complex_derivative n f z /
                    Cx (&(FACT n)) * (w - z) pow n)` THEN
   EXISTS_TAC `(from 0)` THEN CONJ_TAC THENL [ALL_TAC; ASM_REWRITE_TAC []] THEN
   ASM_MESON_TAC [HOLOMORPHIC_POWER_SERIES]);;

let HOLOMORPHIC_FUN_EQ_0_ON_BALL = prove
  (`!f z r w.
      w IN ball(z,r) /\ f holomorphic_on ball(z,r) /\
      (!n. higher_complex_derivative n f z = Cx(&0))
      ==> f w = Cx(&0)`,
   REPEAT STRIP_TAC THEN
   SUBST1_TAC (GSYM (BETA_CONV `(\z:complex. Cx(&0)) w`)) THEN
   MATCH_MP_TAC HOLOMORPHIC_FUN_EQ_ON_BALL THEN
   REWRITE_TAC [HOLOMORPHIC_ON_CONST; HIGHER_COMPLEX_DERIVATIVE_CONST] THEN
   ASM_MESON_TAC []);;