src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 65587 16a8991ab398
parent 64394 141e1ed8d5a0
child 66089 def95e0bc529
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Apr 27 11:06:47 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Apr 27 15:59:00 2017 +0100
     1.3 @@ -482,6 +482,8 @@
     1.4    where
     1.5     "f analytic_on s \<equiv> \<forall>x \<in> s. \<exists>e. 0 < e \<and> f holomorphic_on (ball x e)"
     1.6  
     1.7 +named_theorems analytic_intros "introduction rules for proving analyticity"
     1.8 +
     1.9  lemma analytic_imp_holomorphic: "f analytic_on s \<Longrightarrow> f holomorphic_on s"
    1.10    by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def)
    1.11       (metis centre_in_ball field_differentiable_at_within)
    1.12 @@ -531,16 +533,16 @@
    1.13    finally show ?thesis .
    1.14  qed
    1.15  
    1.16 -lemma analytic_on_linear: "(op * c) analytic_on s"
    1.17 -  by (auto simp add: analytic_on_holomorphic holomorphic_on_linear)
    1.18 +lemma analytic_on_linear [analytic_intros,simp]: "(op * c) analytic_on s"
    1.19 +  by (auto simp add: analytic_on_holomorphic)
    1.20  
    1.21 -lemma analytic_on_const: "(\<lambda>z. c) analytic_on s"
    1.22 +lemma analytic_on_const [analytic_intros,simp]: "(\<lambda>z. c) analytic_on s"
    1.23    by (metis analytic_on_def holomorphic_on_const zero_less_one)
    1.24  
    1.25 -lemma analytic_on_ident: "(\<lambda>x. x) analytic_on s"
    1.26 -  by (simp add: analytic_on_def holomorphic_on_ident gt_ex)
    1.27 +lemma analytic_on_ident [analytic_intros,simp]: "(\<lambda>x. x) analytic_on s"
    1.28 +  by (simp add: analytic_on_def gt_ex)
    1.29  
    1.30 -lemma analytic_on_id: "id analytic_on s"
    1.31 +lemma analytic_on_id [analytic_intros]: "id analytic_on s"
    1.32    unfolding id_def by (rule analytic_on_ident)
    1.33  
    1.34  lemma analytic_on_compose:
    1.35 @@ -572,11 +574,11 @@
    1.36               \<Longrightarrow> g o f analytic_on s"
    1.37  by (metis analytic_on_compose analytic_on_subset image_subset_iff)
    1.38  
    1.39 -lemma analytic_on_neg:
    1.40 +lemma analytic_on_neg [analytic_intros]:
    1.41    "f analytic_on s \<Longrightarrow> (\<lambda>z. -(f z)) analytic_on s"
    1.42  by (metis analytic_on_holomorphic holomorphic_on_minus)
    1.43  
    1.44 -lemma analytic_on_add:
    1.45 +lemma analytic_on_add [analytic_intros]:
    1.46    assumes f: "f analytic_on s"
    1.47        and g: "g analytic_on s"
    1.48      shows "(\<lambda>z. f z + g z) analytic_on s"
    1.49 @@ -596,7 +598,7 @@
    1.50      by (metis e e' min_less_iff_conj)
    1.51  qed
    1.52  
    1.53 -lemma analytic_on_diff:
    1.54 +lemma analytic_on_diff [analytic_intros]:
    1.55    assumes f: "f analytic_on s"
    1.56        and g: "g analytic_on s"
    1.57      shows "(\<lambda>z. f z - g z) analytic_on s"
    1.58 @@ -616,7 +618,7 @@
    1.59      by (metis e e' min_less_iff_conj)
    1.60  qed
    1.61  
    1.62 -lemma analytic_on_mult:
    1.63 +lemma analytic_on_mult [analytic_intros]:
    1.64    assumes f: "f analytic_on s"
    1.65        and g: "g analytic_on s"
    1.66      shows "(\<lambda>z. f z * g z) analytic_on s"
    1.67 @@ -636,7 +638,7 @@
    1.68      by (metis e e' min_less_iff_conj)
    1.69  qed
    1.70  
    1.71 -lemma analytic_on_inverse:
    1.72 +lemma analytic_on_inverse [analytic_intros]:
    1.73    assumes f: "f analytic_on s"
    1.74        and nz: "(\<And>z. z \<in> s \<Longrightarrow> f z \<noteq> 0)"
    1.75      shows "(\<lambda>z. inverse (f z)) analytic_on s"
    1.76 @@ -658,7 +660,7 @@
    1.77      by (metis e e' min_less_iff_conj)
    1.78  qed
    1.79  
    1.80 -lemma analytic_on_divide:
    1.81 +lemma analytic_on_divide [analytic_intros]:
    1.82    assumes f: "f analytic_on s"
    1.83        and g: "g analytic_on s"
    1.84        and nz: "(\<And>z. z \<in> s \<Longrightarrow> g z \<noteq> 0)"
    1.85 @@ -666,11 +668,11 @@
    1.86  unfolding divide_inverse
    1.87  by (metis analytic_on_inverse analytic_on_mult f g nz)
    1.88  
    1.89 -lemma analytic_on_power:
    1.90 +lemma analytic_on_power [analytic_intros]:
    1.91    "f analytic_on s \<Longrightarrow> (\<lambda>z. (f z) ^ n) analytic_on s"
    1.92 -by (induct n) (auto simp: analytic_on_const analytic_on_mult)
    1.93 +by (induct n) (auto simp: analytic_on_mult)
    1.94  
    1.95 -lemma analytic_on_sum:
    1.96 +lemma analytic_on_sum [analytic_intros]:
    1.97    "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on s) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) analytic_on s"
    1.98    by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_const analytic_on_add)
    1.99