A few new lemmas plus some refinements

src/HOL/Analysis/Complex_Analysis_Basics.thy

@@ -144,6 +144,25 @@ lemma holomorphic_on_open:
     "open s \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> (\<forall>x \<in> s. \<exists>f'. DERIV f x :> f')"
   by (auto simp: holomorphic_on_def field_differentiable_def has_field_derivative_def at_within_open [of _ s])
 
+lemma holomorphic_on_UN_open:
+  assumes "\<And>n. n \<in> I \<Longrightarrow> f holomorphic_on A n" "\<And>n. n \<in> I \<Longrightarrow> open (A n)"
+  shows   "f holomorphic_on (\<Union>n\<in>I. A n)"
+proof -
+  have "f field_differentiable at z within (\<Union>n\<in>I. A n)" if "z \<in> (\<Union>n\<in>I. A n)" for z
+  proof -
+    from that obtain n where "n \<in> I" "z \<in> A n"
+      by blast
+    hence "f holomorphic_on A n" "open (A n)"
+      by (simp add: assms)+
+    with \<open>z \<in> A n\<close> have "f field_differentiable at z"
+      by (auto simp: holomorphic_on_open field_differentiable_def)
+    thus ?thesis
+      by (meson field_differentiable_at_within)
+  qed
+  thus ?thesis
+    by (auto simp: holomorphic_on_def)
+qed
+
 lemma holomorphic_on_imp_continuous_on:
     "f holomorphic_on s \<Longrightarrow> continuous_on s f"
   by (metis field_differentiable_imp_continuous_at continuous_on_eq_continuous_within holomorphic_on_def)
@@ -181,6 +200,18 @@ lemma holomorphic_on_ident [simp, holomorphic_intros]: "(\<lambda>x. x) holomorp
 lemma holomorphic_on_id [simp, holomorphic_intros]: "id holomorphic_on s"
   unfolding id_def by (rule holomorphic_on_ident)
 
+lemma constant_on_imp_holomorphic_on:
+  assumes "f constant_on A"
+  shows   "f holomorphic_on A"
+proof -
+  from assms obtain c where c: "\<forall>x\<in>A. f x = c"
+    unfolding constant_on_def by blast
+  have "f holomorphic_on A \<longleftrightarrow> (\<lambda>_. c) holomorphic_on A"
+    by (intro holomorphic_cong) (use c in auto)
+  thus ?thesis
+    by simp
+qed
+
 lemma holomorphic_on_compose:
   "f holomorphic_on s \<Longrightarrow> g holomorphic_on (f ` s) \<Longrightarrow> (g o f) holomorphic_on s"
   using field_differentiable_compose_within[of f _ s g]

src/HOL/Analysis/Complex_Transcendental.thy

@@ -2258,8 +2258,8 @@ lemma powr_complexpow [simp]:
   by (induct n) (auto simp: ac_simps powr_add)
 
 lemma powr_complexnumeral [simp]:
-  fixes x::complex shows "x \<noteq> 0 \<Longrightarrow> x powr (numeral n) = x ^ (numeral n)"
-  by (metis of_nat_numeral powr_complexpow)
+  fixes x::complex shows "x powr (numeral n) = x ^ (numeral n)"
+  by (metis of_nat_numeral power_zero_numeral powr_nat)
 
 lemma cnj_powr:
   assumes "Im a = 0 \<Longrightarrow> Re a \<ge> 0"

src/HOL/Analysis/Elementary_Topology.thy

@@ -1597,11 +1597,20 @@ qed
 lemma closure_insert:
   fixes x :: "'a::t1_space"
   shows "closure (insert x s) = insert x (closure s)"
-  apply (rule closure_unique)
-  apply (rule insert_mono [OF closure_subset])
-  apply (rule closed_insert [OF closed_closure])
-  apply (simp add: closure_minimal)
-  done
+  by (meson closed_closure closed_insert closure_minimal closure_subset dual_order.antisym insert_mono insert_subset)
+
+lemma finite_not_islimpt_in_compact:
+  assumes "compact A" "\<And>z. z \<in> A \<Longrightarrow> \<not>z islimpt B"
+  shows   "finite (A \<inter> B)"
+proof (rule ccontr)
+  assume "infinite (A \<inter> B)"
+  have "\<exists>z\<in>A. z islimpt A \<inter> B"
+    by (rule Heine_Borel_imp_Bolzano_Weierstrass) (use assms \<open>infinite _\<close> in auto)
+  hence "\<exists>z\<in>A. z islimpt B"
+    using islimpt_subset by blast
+  thus False using assms(2)
+    by simp
+qed
 
 
 text\<open>In particular, some common special cases.\<close>

src/HOL/Analysis/Polytope.thy

@@ -434,11 +434,10 @@ proof (cases "\<forall>F'. finite F' \<and> F' \<subseteq> T \<and> card F' \<le
   then obtain c where c:
        "\<And>F'. \<lbrakk>finite F'; F' \<subseteq> T; card F' \<le> DIM('a) + 2\<rbrakk> \<Longrightarrow> c F' \<in> T \<and> c F' \<inter> (\<Inter>F') \<subset> (\<Inter>F')"
     by metis
-  define d where "d = rec_nat {c{}} (\<lambda>n r. insert (c r) r)"
-  have [simp]: "d 0 = {c {}}"
-    by (simp add: d_def)
-  have dSuc [simp]: "\<And>n. d (Suc n) = insert (c (d n)) (d n)"
-    by (simp add: d_def)
+  define d where "d \<equiv> \<lambda>n. ((\<lambda>r. insert (c r) r)^^n) {c{}}"
+  note d_def [simp]
+  have dSuc: "\<And>n. d (Suc n) = insert (c (d n)) (d n)"
+    by simp
   have dn_notempty: "d n \<noteq> {}" for n
     by (induction n) auto
   have dn_le_Suc: "d n \<subseteq> T \<and> finite(d n) \<and> card(d n) \<le> Suc n" if "n \<le> DIM('a) + 2" for n

src/HOL/Limits.thy

@@ -2849,9 +2849,8 @@ lemma Bolzano[consumes 1, case_names trans local]:
     and local: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> \<exists>d>0. \<forall>a b. a \<le> x \<and> x \<le> b \<and> b - a < d \<longrightarrow> P a b"
   shows "P a b"
 proof -
-  define bisect where "bisect =
-    rec_nat (a, b) (\<lambda>n (x, y). if P x ((x+y) / 2) then ((x+y)/2, y) else (x, (x+y)/2))"
-  define l u where "l n = fst (bisect n)" and "u n = snd (bisect n)" for n
+  define bisect where "bisect \<equiv> \<lambda>(x,y). if P x ((x+y) / 2) then ((x+y)/2, y) else (x, (x+y)/2)"
+  define l u where "l n \<equiv> fst ((bisect^^n)(a,b))" and "u n \<equiv> snd ((bisect^^n)(a,b))" for n
   have l[simp]: "l 0 = a" "\<And>n. l (Suc n) = (if P (l n) ((l n + u n) / 2) then (l n + u n) / 2 else l n)"
     and u[simp]: "u 0 = b" "\<And>n. u (Suc n) = (if P (l n) ((l n + u n) / 2) then u n else (l n + u n) / 2)"
     by (simp_all add: l_def u_def bisect_def split: prod.split)