src/HOL/Analysis/Complex_Analysis_Basics.thy

 subsection\<open>Analyticity on a set\<close>
 
 definition analytic_on (infixl "(analytic'_on)" 50)
   where
    "f analytic_on s \<equiv> \<forall>x \<in> s. \<exists>e. 0 < e \<and> f holomorphic_on (ball x e)"
+
+named_theorems analytic_intros "introduction rules for proving analyticity"
 
 lemma analytic_imp_holomorphic: "f analytic_on s \<Longrightarrow> f holomorphic_on s"
   by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def)
      (metis centre_in_ball field_differentiable_at_within)
 

   also have "... \<longleftrightarrow> ?rhs"
     by (auto simp: analytic_on_open)
   finally show ?thesis .
 qed
 
-lemma analytic_on_linear: "(op * c) analytic_on s"
-  by (auto simp add: analytic_on_holomorphic holomorphic_on_linear)
-
-lemma analytic_on_const: "(\<lambda>z. c) analytic_on s"
+lemma analytic_on_linear [analytic_intros,simp]: "(op * c) analytic_on s"
+  by (auto simp add: analytic_on_holomorphic)
+
+lemma analytic_on_const [analytic_intros,simp]: "(\<lambda>z. c) analytic_on s"
   by (metis analytic_on_def holomorphic_on_const zero_less_one)
 
-lemma analytic_on_ident: "(\<lambda>x. x) analytic_on s"
-  by (simp add: analytic_on_def holomorphic_on_ident gt_ex)
-
-lemma analytic_on_id: "id analytic_on s"
+lemma analytic_on_ident [analytic_intros,simp]: "(\<lambda>x. x) analytic_on s"
+  by (simp add: analytic_on_def gt_ex)
+
+lemma analytic_on_id [analytic_intros]: "id analytic_on s"
   unfolding id_def by (rule analytic_on_ident)
 
 lemma analytic_on_compose:
   assumes f: "f analytic_on s"
       and g: "g analytic_on (f ` s)"

 lemma analytic_on_compose_gen:
   "f analytic_on s \<Longrightarrow> g analytic_on t \<Longrightarrow> (\<And>z. z \<in> s \<Longrightarrow> f z \<in> t)
              \<Longrightarrow> g o f analytic_on s"
 by (metis analytic_on_compose analytic_on_subset image_subset_iff)
 
-lemma analytic_on_neg:
+lemma analytic_on_neg [analytic_intros]:
   "f analytic_on s \<Longrightarrow> (\<lambda>z. -(f z)) analytic_on s"
 by (metis analytic_on_holomorphic holomorphic_on_minus)
 
-lemma analytic_on_add:
+lemma analytic_on_add [analytic_intros]:
   assumes f: "f analytic_on s"
       and g: "g analytic_on s"
     shows "(\<lambda>z. f z + g z) analytic_on s"
 unfolding analytic_on_def
 proof (intro ballI)

     by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
   then show "\<exists>e>0. (\<lambda>z. f z + g z) holomorphic_on ball z e"
     by (metis e e' min_less_iff_conj)
 qed
 
-lemma analytic_on_diff:
+lemma analytic_on_diff [analytic_intros]:
   assumes f: "f analytic_on s"
       and g: "g analytic_on s"
     shows "(\<lambda>z. f z - g z) analytic_on s"
 unfolding analytic_on_def
 proof (intro ballI)

     by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
   then show "\<exists>e>0. (\<lambda>z. f z - g z) holomorphic_on ball z e"
     by (metis e e' min_less_iff_conj)
 qed
 
-lemma analytic_on_mult:
+lemma analytic_on_mult [analytic_intros]:
   assumes f: "f analytic_on s"
       and g: "g analytic_on s"
     shows "(\<lambda>z. f z * g z) analytic_on s"
 unfolding analytic_on_def
 proof (intro ballI)

     by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
   then show "\<exists>e>0. (\<lambda>z. f z * g z) holomorphic_on ball z e"
     by (metis e e' min_less_iff_conj)
 qed
 
-lemma analytic_on_inverse:
+lemma analytic_on_inverse [analytic_intros]:
   assumes f: "f analytic_on s"
       and nz: "(\<And>z. z \<in> s \<Longrightarrow> f z \<noteq> 0)"
     shows "(\<lambda>z. inverse (f z)) analytic_on s"
 unfolding analytic_on_def
 proof (intro ballI)

     by (metis nz' mem_ball min_less_iff_conj)
   then show "\<exists>e>0. (\<lambda>z. inverse (f z)) holomorphic_on ball z e"
     by (metis e e' min_less_iff_conj)
 qed
 
-lemma analytic_on_divide:
+lemma analytic_on_divide [analytic_intros]:
   assumes f: "f analytic_on s"
       and g: "g analytic_on s"
       and nz: "(\<And>z. z \<in> s \<Longrightarrow> g z \<noteq> 0)"
     shows "(\<lambda>z. f z / g z) analytic_on s"
 unfolding divide_inverse
 by (metis analytic_on_inverse analytic_on_mult f g nz)
 
-lemma analytic_on_power:
+lemma analytic_on_power [analytic_intros]:
   "f analytic_on s \<Longrightarrow> (\<lambda>z. (f z) ^ n) analytic_on s"
-by (induct n) (auto simp: analytic_on_const analytic_on_mult)
-
-lemma analytic_on_sum:
+by (induct n) (auto simp: analytic_on_mult)
+
+lemma analytic_on_sum [analytic_intros]:
   "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on s) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) analytic_on s"
   by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_const analytic_on_add)
 
 lemma deriv_left_inverse:
   assumes "f holomorphic_on S" and "g holomorphic_on T"