--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Fri Oct 15 12:42:51 2021 +0100
@@ -144,6 +144,25 @@
"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_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]
--- a/src/HOL/Analysis/Complex_Transcendental.thy Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Fri Oct 15 12:42:51 2021 +0100
@@ -2258,8 +2258,8 @@
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"
--- a/src/HOL/Analysis/Elementary_Topology.thy Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Analysis/Elementary_Topology.thy Fri Oct 15 12:42:51 2021 +0100
@@ -1597,11 +1597,20 @@
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>
--- a/src/HOL/Analysis/Polytope.thy Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Analysis/Polytope.thy Fri Oct 15 12:42:51 2021 +0100
@@ -434,11 +434,10 @@
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
--- a/src/HOL/Limits.thy Thu Oct 14 15:24:28 2021 +0200
+++ b/src/HOL/Limits.thy Fri Oct 15 12:42:51 2021 +0100
@@ -2849,9 +2849,8 @@
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)