--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Sun Feb 12 21:11:57 2023 +0100
@@ -417,14 +417,24 @@
(metis centre_in_ball field_differentiable_at_within)
lemma analytic_on_open: "open S \<Longrightarrow> f analytic_on S \<longleftrightarrow> f holomorphic_on S"
-apply (auto simp: analytic_imp_holomorphic)
-apply (auto simp: analytic_on_def holomorphic_on_def)
-by (metis holomorphic_on_def holomorphic_on_subset open_contains_ball)
+ by (meson analytic_imp_holomorphic analytic_on_def holomorphic_on_subset openE)
lemma analytic_on_imp_differentiable_at:
"f analytic_on S \<Longrightarrow> x \<in> S \<Longrightarrow> f field_differentiable (at x)"
- apply (auto simp: analytic_on_def holomorphic_on_def)
-by (metis open_ball centre_in_ball field_differentiable_within_open)
+ using analytic_on_def holomorphic_on_imp_differentiable_at by auto
+
+lemma analytic_at_imp_isCont:
+ assumes "f analytic_on {z}"
+ shows "isCont f z"
+ using assms by (meson analytic_on_imp_differentiable_at field_differentiable_imp_continuous_at insertI1)
+
+lemma analytic_at_neq_imp_eventually_neq:
+ assumes "f analytic_on {x}" "f x \<noteq> c"
+ shows "eventually (\<lambda>y. f y \<noteq> c) (at x)"
+proof (intro tendsto_imp_eventually_ne)
+ show "f \<midarrow>x\<rightarrow> f x"
+ using assms by (simp add: analytic_at_imp_isCont isContD)
+qed (use assms in auto)
lemma analytic_on_subset: "f analytic_on S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> f analytic_on T"
by (auto simp: analytic_on_def)
@@ -652,15 +662,20 @@
lemma analytic_at_ball:
"f analytic_on {z} \<longleftrightarrow> (\<exists>e. 0<e \<and> f holomorphic_on ball z e)"
-by (metis analytic_on_def singleton_iff)
+ by (metis analytic_on_def singleton_iff)
lemma analytic_at:
- "f analytic_on {z} \<longleftrightarrow> (\<exists>s. open s \<and> z \<in> s \<and> f holomorphic_on s)"
-by (metis analytic_on_holomorphic empty_subsetI insert_subset)
+ "f analytic_on {z} \<longleftrightarrow> (\<exists>s. open s \<and> z \<in> s \<and> f holomorphic_on s)"
+ by (metis analytic_on_holomorphic empty_subsetI insert_subset)
+
+lemma holomorphic_on_imp_analytic_at:
+ assumes "f holomorphic_on A" "open A" "z \<in> A"
+ shows "f analytic_on {z}"
+ using assms by (meson analytic_at)
lemma analytic_on_analytic_at:
- "f analytic_on s \<longleftrightarrow> (\<forall>z \<in> s. f analytic_on {z})"
-by (metis analytic_at_ball analytic_on_def)
+ "f analytic_on s \<longleftrightarrow> (\<forall>z \<in> s. f analytic_on {z})"
+ by (metis analytic_at_ball analytic_on_def)
lemma analytic_at_two:
"f analytic_on {z} \<and> g analytic_on {z} \<longleftrightarrow>
--- a/src/HOL/Analysis/Complex_Transcendental.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Sun Feb 12 21:11:57 2023 +0100
@@ -2649,7 +2649,7 @@
lemma powr_nat': "(z :: complex) \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> z powr of_nat n = z ^ n"
by (cases "z = 0") (auto simp: powr_nat)
-
+
lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
using Ln_Reals_eq norm_exp_eq_Re by (auto simp: Im_Ln_eq_0 powr_def norm_complex_def)
@@ -2694,12 +2694,15 @@
shows "z powr of_int n = (if n\<ge>0 then z^nat n else inverse (z^nat (-n)))"
by (metis assms not_le of_int_of_nat powr_complexpow powr_minus)
+lemma complex_powr_of_int: "z \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> z powr of_int n = (z :: complex) powi n"
+ by (cases "z = 0 \<or> n = 0")
+ (auto simp: power_int_def powr_minus powr_nat powr_of_int power_0_left power_inverse)
+
lemma powr_Reals_eq: "\<lbrakk>x \<in> \<real>; y \<in> \<real>; Re x \<ge> 0\<rbrakk> \<Longrightarrow> x powr y = of_real (Re x powr Re y)"
by (metis of_real_Re powr_of_real)
lemma norm_powr_real_mono:
- "\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk>
- \<Longrightarrow> cmod(w powr z1) \<le> cmod(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
+ "\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk> \<Longrightarrow> cmod(w powr z1) \<le> cmod(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
by (auto simp: powr_def algebra_simps Reals_def Ln_of_real)
lemma powr_times_real:
@@ -4035,6 +4038,36 @@
lemma holomorphic_on_Arccos: "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos holomorphic_on s"
by (simp add: field_differentiable_within_Arccos holomorphic_on_def)
+text \<open>This theorem is about REAL cos/arccos but relies on theorems about @{term Arg}\<close>
+lemma cos_eq_arccos_Ex:
+ "cos x = y \<longleftrightarrow> -1\<le>y \<and> y\<le>1 \<and> (\<exists>k::int. x = arccos y + 2*k*pi \<or> x = - arccos y + 2*k*pi)" (is "?L=?R")
+proof
+ assume R: ?R
+ then obtain k::int where "x = arccos y + 2*k*pi \<or> x = - arccos y + 2*k*pi" by auto
+ moreover have "cos x = y" when "x = arccos y + 2*k*pi"
+ by (metis (no_types) R cos_arccos cos_eq_periodic_intro cos_minus minus_add_cancel)
+ moreover have "cos x = y" when "x = -arccos y + 2*k*pi"
+ by (metis add_minus_cancel R cos_arccos cos_eq_periodic_intro uminus_add_conv_diff)
+ ultimately show "cos x = y" by auto
+next
+ assume L: ?L
+ let ?goal = "(\<exists>k::int. x = arccos y + 2*k*pi \<or> x = - arccos y + 2*k*pi)"
+ obtain k::int where k: "-pi < x-k*2*pi" "x-k*2*pi \<le> pi"
+ by (metis Arg_bounded Arg_exp_diff_2pi complex.sel(2) mult.assoc of_int_mult of_int_numeral)
+ have *: "cos (x - k * 2*pi) = y"
+ using cos.periodic_simps(3)[of x "-k"] L by (auto simp add:field_simps)
+ then have \<section>: ?goal when "x-k*2*pi \<ge> 0"
+ using arccos_cos k that by force
+ moreover have ?goal when "\<not> x-k*2*pi \<ge>0"
+ proof -
+ have "cos (k * 2*pi - x) = y"
+ by (metis * cos_minus minus_diff_eq)
+ then show ?goal
+ using arccos_cos \<section> k by fastforce
+ qed
+ ultimately show "-1\<le>y \<and> y\<le>1 \<and> ?goal"
+ using L by auto
+qed
subsection\<^marker>\<open>tag unimportant\<close>\<open>Upper and Lower Bounds for Inverse Sine and Cosine\<close>
@@ -4276,8 +4309,8 @@
qed
lemma finite_complex_roots_unity_explicit:
- "finite {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n}"
-by simp
+ "finite {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n}"
+ by simp
lemma card_complex_roots_unity_explicit:
"card {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n} = n"
--- a/src/HOL/Analysis/Connected.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Analysis/Connected.thy Sun Feb 12 21:11:57 2023 +0100
@@ -238,10 +238,7 @@
connected_component_set S x \<inter> T \<noteq> {};
connected_component_set S y \<inter> T \<noteq> {}\<rbrakk>
\<Longrightarrow> connected_component_set S x = connected_component_set S y"
-apply (simp add: ex_in_conv [symmetric])
-apply (rule connected_component_eq)
-by (metis (no_types, opaque_lifting) connected_component_eq_eq connected_component_in connected_component_maximal subsetD mem_Collect_eq)
-
+ by (metis (full_types) subsetD connected_component_eq connected_component_maximal disjoint_iff_not_equal)
lemma Union_connected_component: "\<Union>(connected_component_set S ` S) = S"
apply (rule subset_antisym)
@@ -260,10 +257,36 @@
lemma connected_component_intermediate_subset:
"\<lbrakk>connected_component_set U a \<subseteq> T; T \<subseteq> U\<rbrakk>
\<Longrightarrow> connected_component_set T a = connected_component_set U a"
- apply (case_tac "a \<in> U")
- apply (simp add: connected_component_maximal connected_component_mono subset_antisym)
- using connected_component_eq_empty by blast
+ by (metis connected_component_idemp connected_component_mono subset_antisym)
+
+lemma connected_component_homeomorphismI:
+ assumes "homeomorphism A B f g" "connected_component A x y"
+ shows "connected_component B (f x) (f y)"
+proof -
+ from assms obtain T where T: "connected T" "T \<subseteq> A" "x \<in> T" "y \<in> T"
+ unfolding connected_component_def by blast
+ have "connected (f ` T)" "f ` T \<subseteq> B" "f x \<in> f ` T" "f y \<in> f ` T"
+ using assms T continuous_on_subset[of A f T]
+ by (auto intro!: connected_continuous_image simp: homeomorphism_def)
+ thus ?thesis
+ unfolding connected_component_def by blast
+qed
+
+lemma connected_component_homeomorphism_iff:
+ assumes "homeomorphism A B f g"
+ shows "connected_component A x y \<longleftrightarrow> x \<in> A \<and> y \<in> A \<and> connected_component B (f x) (f y)"
+ by (metis assms connected_component_homeomorphismI connected_component_in homeomorphism_apply1 homeomorphism_sym)
+
+lemma connected_component_set_homeomorphism:
+ assumes "homeomorphism A B f g" "x \<in> A"
+ shows "connected_component_set B (f x) = f ` connected_component_set A x" (is "?lhs = ?rhs")
+proof -
+ have "y \<in> ?lhs \<longleftrightarrow> y \<in> ?rhs" for y
+ by (smt (verit, best) assms connected_component_homeomorphism_iff homeomorphism_def image_iff mem_Collect_eq)
+ thus ?thesis
+ by blast
+qed
subsection \<open>The set of connected components of a set\<close>
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Sun Feb 12 21:11:57 2023 +0100
@@ -274,6 +274,48 @@
ultimately show ?thesis by blast
qed
+lemma frequently_atE:
+ fixes x :: "'a :: metric_space"
+ assumes "frequently P (at x within s)"
+ shows "\<exists>f. filterlim f (at x within s) sequentially \<and> (\<forall>n. P (f n))"
+proof -
+ have "\<exists>y. y \<in> s \<inter> (ball x (1 / real (Suc n)) - {x}) \<and> P y" for n
+ proof -
+ have "\<exists>z\<in>s. z \<noteq> x \<and> dist z x < (1 / real (Suc n)) \<and> P z"
+ by (metis assms divide_pos_pos frequently_at of_nat_0_less_iff zero_less_Suc zero_less_one)
+ then show ?thesis
+ by (auto simp: dist_commute conj_commute)
+ qed
+ then obtain f where f: "\<And>n. f n \<in> s \<inter> (ball x (1 / real (Suc n)) - {x}) \<and> P (f n)"
+ by metis
+ have "filterlim f (nhds x) sequentially"
+ unfolding tendsto_iff
+ proof clarify
+ fix e :: real
+ assume e: "e > 0"
+ then obtain n where n: "Suc n > 1 / e"
+ by (meson le_nat_floor lessI not_le)
+ have "dist (f k) x < e" if "k \<ge> n" for k
+ proof -
+ have "dist (f k) x < 1 / real (Suc k)"
+ using f[of k] by (auto simp: dist_commute)
+ also have "\<dots> \<le> 1 / real (Suc n)"
+ using that by (intro divide_left_mono) auto
+ also have "\<dots> < e"
+ using n e by (simp add: field_simps)
+ finally show ?thesis .
+ qed
+ thus "\<forall>\<^sub>F k in sequentially. dist (f k) x < e"
+ unfolding eventually_at_top_linorder by blast
+ qed
+ moreover have "f n \<noteq> x" for n
+ using f[of n] by auto
+ ultimately have "filterlim f (at x within s) sequentially"
+ using f by (auto simp: filterlim_at)
+ with f show ?thesis
+ by blast
+qed
+
subsection \<open>Limit Points\<close>
lemma islimpt_approachable:
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Sun Feb 12 21:11:57 2023 +0100
@@ -659,6 +659,16 @@
lemma bounded_pos_less: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x < b)"
by (metis bounded_pos le_less_trans less_imp_le linordered_field_no_ub)
+lemma bounded_normE:
+ assumes "bounded A"
+ obtains B where "B > 0" "\<And>z. z \<in> A \<Longrightarrow> norm z \<le> B"
+ by (meson assms bounded_pos)
+
+lemma bounded_normE_less:
+ assumes "bounded A"
+ obtains B where "B > 0" "\<And>z. z \<in> A \<Longrightarrow> norm z < B"
+ by (meson assms bounded_pos_less)
+
lemma Bseq_eq_bounded:
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
shows "Bseq f \<longleftrightarrow> bounded (range f)"
--- a/src/HOL/Analysis/Elementary_Topology.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy Sun Feb 12 21:11:57 2023 +0100
@@ -758,6 +758,87 @@
by simp
qed
+(*could prove directly from islimpt_sequential_inj, but only for metric spaces*)
+lemma islimpt_sequential:
+ fixes x :: "'a::first_countable_topology"
+ shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> (f \<longlongrightarrow> x) sequentially)"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ from countable_basis_at_decseq[of x] obtain A where A:
+ "\<And>i. open (A i)"
+ "\<And>i. x \<in> A i"
+ "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
+ by blast
+ define f where "f n = (SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y)" for n
+ {
+ fix n
+ from \<open>?lhs\<close> have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
+ unfolding islimpt_def using A(1,2)[of n] by auto
+ then have "f n \<in> S \<and> f n \<in> A n \<and> x \<noteq> f n"
+ unfolding f_def by (rule someI_ex)
+ then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto
+ }
+ then have "\<forall>n. f n \<in> S - {x}" by auto
+ moreover have "(\<lambda>n. f n) \<longlonglongrightarrow> x"
+ proof (rule topological_tendstoI)
+ fix S
+ assume "open S" "x \<in> S"
+ from A(3)[OF this] \<open>\<And>n. f n \<in> A n\<close>
+ show "eventually (\<lambda>x. f x \<in> S) sequentially"
+ by (auto elim!: eventually_mono)
+ qed
+ ultimately show ?rhs by fast
+next
+ assume ?rhs
+ then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f \<longlonglongrightarrow> x"
+ by auto
+ show ?lhs
+ unfolding islimpt_def
+ proof safe
+ fix T
+ assume "open T" "x \<in> T"
+ from lim[THEN topological_tendstoD, OF this] f
+ show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
+ unfolding eventually_sequentially by auto
+ qed
+qed
+
+lemma islimpt_isCont_image:
+ fixes f :: "'a :: {first_countable_topology, t2_space} \<Rightarrow> 'b :: {first_countable_topology, t2_space}"
+ assumes "x islimpt A" and "isCont f x" and ev: "eventually (\<lambda>y. f y \<noteq> f x) (at x)"
+ shows "f x islimpt f ` A"
+proof -
+ from assms(1) obtain g where g: "g \<longlonglongrightarrow> x" "range g \<subseteq> A - {x}"
+ unfolding islimpt_sequential by blast
+ have "filterlim g (at x) sequentially"
+ using g by (auto simp: filterlim_at intro!: always_eventually)
+ then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> f (g n) \<noteq> f x"
+ by (metis (mono_tags, lifting) ev eventually_at_top_linorder filterlim_iff)
+ have "(\<lambda>x. g (x + N)) \<longlonglongrightarrow> x"
+ using g(1) by (rule LIMSEQ_ignore_initial_segment)
+ hence "(\<lambda>x. f (g (x + N))) \<longlonglongrightarrow> f x"
+ using assms(2) isCont_tendsto_compose by blast
+ moreover have "range (\<lambda>x. f (g (x + N))) \<subseteq> f ` A - {f x}"
+ using g(2) N by auto
+ ultimately show ?thesis
+ unfolding islimpt_sequential by (intro exI[of _ "\<lambda>x. f (g (x + N))"]) auto
+qed
+
+lemma islimpt_image:
+ assumes "z islimpt g -` A \<inter> B" "g z \<notin> A" "z \<in> B" "open B" "continuous_on B g"
+ shows "g z islimpt A"
+ unfolding islimpt_def
+proof clarify
+ fix T assume T: "g z \<in> T" "open T"
+ have "z \<in> g -` T \<inter> B"
+ using T assms by auto
+ moreover have "open (g -` T \<inter> B)"
+ using T continuous_on_open_vimage assms by blast
+ ultimately show "\<exists>y\<in>A. y \<in> T \<and> y \<noteq> g z"
+ using assms by (metis (mono_tags, lifting) IntD1 islimptE vimageE)
+qed
+
subsection \<open>Interior of a Set\<close>
@@ -845,7 +926,12 @@
lemma islimpt_conv_frequently_at:
"x islimpt A \<longleftrightarrow> frequently (\<lambda>y. y \<in> A) (at x)"
- unfolding islimpt_def eventually_at_filter frequently_def eventually_nhds by blast
+ by (simp add: frequently_def islimpt_iff_eventually)
+
+lemma frequently_at_imp_islimpt:
+ assumes "frequently (\<lambda>y. y \<in> A) (at x)"
+ shows "x islimpt A"
+ by (simp add: assms islimpt_conv_frequently_at)
lemma interior_closed_Un_empty_interior:
assumes cS: "closed S"
@@ -1350,52 +1436,6 @@
qed
qed
-(*could prove directly from islimpt_sequential_inj, but only for metric spaces*)
-lemma islimpt_sequential:
- fixes x :: "'a::first_countable_topology"
- shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> (f \<longlongrightarrow> x) sequentially)"
- (is "?lhs = ?rhs")
-proof
- assume ?lhs
- from countable_basis_at_decseq[of x] obtain A where A:
- "\<And>i. open (A i)"
- "\<And>i. x \<in> A i"
- "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
- by blast
- define f where "f n = (SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y)" for n
- {
- fix n
- from \<open>?lhs\<close> have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
- unfolding islimpt_def using A(1,2)[of n] by auto
- then have "f n \<in> S \<and> f n \<in> A n \<and> x \<noteq> f n"
- unfolding f_def by (rule someI_ex)
- then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto
- }
- then have "\<forall>n. f n \<in> S - {x}" by auto
- moreover have "(\<lambda>n. f n) \<longlonglongrightarrow> x"
- proof (rule topological_tendstoI)
- fix S
- assume "open S" "x \<in> S"
- from A(3)[OF this] \<open>\<And>n. f n \<in> A n\<close>
- show "eventually (\<lambda>x. f x \<in> S) sequentially"
- by (auto elim!: eventually_mono)
- qed
- ultimately show ?rhs by fast
-next
- assume ?rhs
- then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f \<longlonglongrightarrow> x"
- by auto
- show ?lhs
- unfolding islimpt_def
- proof safe
- fix T
- assume "open T" "x \<in> T"
- from lim[THEN topological_tendstoD, OF this] f
- show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
- unfolding eventually_sequentially by auto
- qed
-qed
-
text\<open>These are special for limits out of the same topological space.\<close>
lemma Lim_within_id: "(id \<longlongrightarrow> a) (at a within s)"
--- a/src/HOL/Analysis/Isolated.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Analysis/Isolated.thy Sun Feb 12 21:11:57 2023 +0100
@@ -14,6 +14,12 @@
definition (in metric_space) uniform_discrete :: "'a set \<Rightarrow> bool" where
"uniform_discrete S \<longleftrightarrow> (\<exists>e>0. \<forall>x\<in>S. \<forall>y\<in>S. dist x y < e \<longrightarrow> x = y)"
+lemma discreteI: "(\<And>x. x \<in> X \<Longrightarrow> x isolated_in X ) \<Longrightarrow> discrete X"
+ unfolding discrete_def by auto
+
+lemma discreteD: "discrete X \<Longrightarrow> x \<in> X \<Longrightarrow> x isolated_in X "
+ unfolding discrete_def by auto
+
lemma uniformI1:
assumes "e>0" "\<And>x y. \<lbrakk>x\<in>S;y\<in>S;dist x y<e\<rbrakk> \<Longrightarrow> x =y "
shows "uniform_discrete S"
@@ -43,6 +49,54 @@
shows "x isolated_in (insert a S) \<longleftrightarrow> x isolated_in S \<or> (x=a \<and> \<not> (x islimpt S))"
by (meson insert_iff islimpt_insert isolated_in_islimpt_iff)
+lemma isolated_inI:
+ assumes "x\<in>S" "open T" "T \<inter> S = {x}"
+ shows "x isolated_in S"
+ using assms unfolding isolated_in_def by auto
+
+lemma isolated_inE:
+ assumes "x isolated_in S"
+ obtains T where "x \<in> S" "open T" "T \<inter> S = {x}"
+ using assms that unfolding isolated_in_def by force
+
+lemma isolated_inE_dist:
+ assumes "x isolated_in S"
+ obtains d where "d > 0" "\<And>y. y \<in> S \<Longrightarrow> dist x y < d \<Longrightarrow> y = x"
+ by (meson assms isolated_in_dist_Ex_iff)
+
+lemma isolated_in_altdef:
+ "x isolated_in S \<longleftrightarrow> (x\<in>S \<and> eventually (\<lambda>y. y \<notin> S) (at x))"
+proof
+ assume "x isolated_in S"
+ from isolated_inE[OF this]
+ obtain T where "x \<in> S" and T:"open T" "T \<inter> S = {x}"
+ by metis
+ have "\<forall>\<^sub>F y in nhds x. y \<in> T"
+ apply (rule eventually_nhds_in_open)
+ using T by auto
+ then have "eventually (\<lambda>y. y \<in> T - {x}) (at x)"
+ unfolding eventually_at_filter by eventually_elim auto
+ then have "eventually (\<lambda>y. y \<notin> S) (at x)"
+ by eventually_elim (use T in auto)
+ then show " x \<in> S \<and> (\<forall>\<^sub>F y in at x. y \<notin> S)" using \<open>x \<in> S\<close> by auto
+next
+ assume "x \<in> S \<and> (\<forall>\<^sub>F y in at x. y \<notin> S)"
+ then have "\<forall>\<^sub>F y in at x. y \<notin> S" "x\<in>S" by auto
+ from this(1) have "eventually (\<lambda>y. y \<notin> S \<or> y = x) (nhds x)"
+ unfolding eventually_at_filter by eventually_elim auto
+ then obtain T where T:"open T" "x \<in> T" "(\<forall>y\<in>T. y \<notin> S \<or> y = x)"
+ unfolding eventually_nhds by auto
+ with \<open>x \<in> S\<close> have "T \<inter> S = {x}"
+ by fastforce
+ with \<open>x\<in>S\<close> \<open>open T\<close>
+ show "x isolated_in S"
+ unfolding isolated_in_def by auto
+qed
+
+lemma discrete_altdef:
+ "discrete S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>\<^sub>F y in at x. y \<notin> S)"
+ unfolding discrete_def isolated_in_altdef by auto
+
(*
TODO.
Other than
@@ -194,4 +248,80 @@
ultimately show ?thesis by fastforce
qed
+definition sparse :: "real \<Rightarrow> 'a :: metric_space set \<Rightarrow> bool"
+ where "sparse \<epsilon> X \<longleftrightarrow> (\<forall>x\<in>X. \<forall>y\<in>X-{x}. dist x y > \<epsilon>)"
+
+lemma sparse_empty [simp, intro]: "sparse \<epsilon> {}"
+ by (auto simp: sparse_def)
+
+lemma sparseI [intro?]:
+ "(\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> x \<noteq> y \<Longrightarrow> dist x y > \<epsilon>) \<Longrightarrow> sparse \<epsilon> X"
+ unfolding sparse_def by auto
+
+lemma sparseD:
+ "sparse \<epsilon> X \<Longrightarrow> x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> x \<noteq> y \<Longrightarrow> dist x y > \<epsilon>"
+ unfolding sparse_def by auto
+
+lemma sparseD':
+ "sparse \<epsilon> X \<Longrightarrow> x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist x y \<le> \<epsilon> \<Longrightarrow> x = y"
+ unfolding sparse_def by force
+
+lemma sparse_singleton [simp, intro]: "sparse \<epsilon> {x}"
+ by (auto simp: sparse_def)
+
+definition setdist_gt where "setdist_gt \<epsilon> X Y \<longleftrightarrow> (\<forall>x\<in>X. \<forall>y\<in>Y. dist x y > \<epsilon>)"
+
+lemma setdist_gt_empty [simp]: "setdist_gt \<epsilon> {} Y" "setdist_gt \<epsilon> X {}"
+ by (auto simp: setdist_gt_def)
+
+lemma setdist_gtI: "(\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> dist x y > \<epsilon>) \<Longrightarrow> setdist_gt \<epsilon> X Y"
+ unfolding setdist_gt_def by auto
+
+lemma setdist_gtD: "setdist_gt \<epsilon> X Y \<Longrightarrow> x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> dist x y > \<epsilon>"
+ unfolding setdist_gt_def by auto
+
+lemma setdist_gt_setdist: "\<epsilon> < setdist A B \<Longrightarrow> setdist_gt \<epsilon> A B"
+ unfolding setdist_gt_def using setdist_le_dist by fastforce
+
+lemma setdist_gt_mono: "setdist_gt \<epsilon>' A B \<Longrightarrow> \<epsilon> \<le> \<epsilon>' \<Longrightarrow> A' \<subseteq> A \<Longrightarrow> B' \<subseteq> B \<Longrightarrow> setdist_gt \<epsilon> A' B'"
+ by (force simp: setdist_gt_def)
+
+lemma setdist_gt_Un_left: "setdist_gt \<epsilon> (A \<union> B) C \<longleftrightarrow> setdist_gt \<epsilon> A C \<and> setdist_gt \<epsilon> B C"
+ by (auto simp: setdist_gt_def)
+
+lemma setdist_gt_Un_right: "setdist_gt \<epsilon> C (A \<union> B) \<longleftrightarrow> setdist_gt \<epsilon> C A \<and> setdist_gt \<epsilon> C B"
+ by (auto simp: setdist_gt_def)
+
+lemma compact_closed_imp_eventually_setdist_gt_at_right_0:
+ assumes "compact A" "closed B" "A \<inter> B = {}"
+ shows "eventually (\<lambda>\<epsilon>. setdist_gt \<epsilon> A B) (at_right 0)"
+proof (cases "A = {} \<or> B = {}")
+ case False
+ hence "setdist A B > 0"
+ by (metis IntI assms empty_iff in_closed_iff_infdist_zero order_less_le setdist_attains_inf setdist_pos_le setdist_sym)
+ hence "eventually (\<lambda>\<epsilon>. \<epsilon> < setdist A B) (at_right 0)"
+ using eventually_at_right_field by blast
+ thus ?thesis
+ by eventually_elim (auto intro: setdist_gt_setdist)
+qed auto
+
+lemma setdist_gt_symI: "setdist_gt \<epsilon> A B \<Longrightarrow> setdist_gt \<epsilon> B A"
+ by (force simp: setdist_gt_def dist_commute)
+
+lemma setdist_gt_sym: "setdist_gt \<epsilon> A B \<longleftrightarrow> setdist_gt \<epsilon> B A"
+ by (force simp: setdist_gt_def dist_commute)
+
+lemma eventually_setdist_gt_at_right_0_mult_iff:
+ assumes "c > 0"
+ shows "eventually (\<lambda>\<epsilon>. setdist_gt (c * \<epsilon>) A B) (at_right 0) \<longleftrightarrow>
+ eventually (\<lambda>\<epsilon>. setdist_gt \<epsilon> A B) (at_right 0)"
+proof -
+ have "eventually (\<lambda>\<epsilon>. setdist_gt (c * \<epsilon>) A B) (at_right 0) \<longleftrightarrow>
+ eventually (\<lambda>\<epsilon>. setdist_gt \<epsilon> A B) (filtermap ((*) c) (at_right 0))"
+ by (simp add: eventually_filtermap)
+ also have "filtermap ((*) c) (at_right 0) = at_right 0"
+ by (subst filtermap_times_pos_at_right) (use assms in auto)
+ finally show ?thesis .
+qed
+
end
--- a/src/HOL/Analysis/Product_Vector.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Analysis/Product_Vector.thy Sun Feb 12 21:11:57 2023 +0100
@@ -131,7 +131,10 @@
instance..
end
-instantiation\<^marker>\<open>tag unimportant\<close> prod :: (uniform_space, uniform_space) uniform_space begin
+subsubsection \<open>Uniform spaces\<close>
+
+instantiation\<^marker>\<open>tag unimportant\<close> prod :: (uniform_space, uniform_space) uniform_space
+begin
instance
proof standard
fix U :: \<open>('a \<times> 'b) set\<close>
@@ -216,6 +219,133 @@
qed
end
+
+lemma (in uniform_space) nhds_eq_comap_uniformity: "nhds x = filtercomap (\<lambda>y. (x, y)) uniformity"
+proof -
+ have *: "eventually P (filtercomap (\<lambda>y. (x, y)) F) \<longleftrightarrow>
+ eventually (\<lambda>z. fst z = x \<longrightarrow> P (snd z)) F" for P :: "'a \<Rightarrow> bool" and F
+ unfolding eventually_filtercomap
+ by (smt (verit) eventually_elim2 fst_conv prod.collapse snd_conv)
+ thus ?thesis
+ unfolding filter_eq_iff
+ by (subst *) (auto simp: eventually_nhds_uniformity case_prod_unfold)
+qed
+
+lemma uniformity_of_uniform_continuous_invariant:
+ fixes f :: "'a :: uniform_space \<Rightarrow> 'a \<Rightarrow> 'a"
+ assumes "filterlim (\<lambda>((a,b),(c,d)). (f a c, f b d)) uniformity (uniformity \<times>\<^sub>F uniformity)"
+ assumes "eventually P uniformity"
+ obtains Q where "eventually Q uniformity" "\<And>a b c. Q (a, b) \<Longrightarrow> P (f a c, f b c)"
+ using eventually_compose_filterlim[OF assms(2,1)] uniformity_refl
+ by (fastforce simp: case_prod_unfold eventually_filtercomap eventually_prod_same)
+
+class uniform_topological_monoid_add = topological_monoid_add + uniform_space +
+ assumes uniformly_continuous_add':
+ "filterlim (\<lambda>((a,b), (c,d)). (a + c, b + d)) uniformity (uniformity \<times>\<^sub>F uniformity)"
+
+lemma uniformly_continuous_add:
+ "uniformly_continuous_on UNIV (\<lambda>(x :: 'a :: uniform_topological_monoid_add,y). x + y)"
+ using uniformly_continuous_add'[where ?'a = 'a]
+ by (simp add: uniformly_continuous_on_uniformity case_prod_unfold uniformity_prod_def filterlim_filtermap)
+
+lemma filterlim_fst: "filterlim fst F (F \<times>\<^sub>F G)"
+ by (simp add: filterlim_def filtermap_fst_prod_filter)
+
+lemma filterlim_snd: "filterlim snd G (F \<times>\<^sub>F G)"
+ by (simp add: filterlim_def filtermap_snd_prod_filter)
+
+class uniform_topological_group_add = topological_group_add + uniform_topological_monoid_add +
+ assumes uniformly_continuous_uminus': "filterlim (\<lambda>(a, b). (-a, -b)) uniformity uniformity"
+begin
+
+lemma uniformly_continuous_minus':
+ "filterlim (\<lambda>((a,b), (c,d)). (a - c, b - d)) uniformity (uniformity \<times>\<^sub>F uniformity)"
+proof -
+ have "filterlim ((\<lambda>((a,b), (c,d)). (a + c, b + d)) \<circ> (\<lambda>((a,b), (c,d)). ((a, b), (-c, -d))))
+ uniformity (uniformity \<times>\<^sub>F uniformity)"
+ unfolding o_def using uniformly_continuous_uminus'
+ by (intro filterlim_compose[OF uniformly_continuous_add'])
+ (auto simp: case_prod_unfold intro!: filterlim_Pair
+ filterlim_fst filterlim_compose[OF _ filterlim_snd])
+ thus ?thesis
+ by (simp add: o_def case_prod_unfold)
+qed
+
+end
+
+lemma uniformly_continuous_uminus:
+ "uniformly_continuous_on UNIV (\<lambda>x :: 'a :: uniform_topological_group_add. -x)"
+ using uniformly_continuous_uminus'[where ?'a = 'a]
+ by (simp add: uniformly_continuous_on_uniformity)
+
+lemma uniformly_continuous_minus:
+ "uniformly_continuous_on UNIV (\<lambda>(x :: 'a :: uniform_topological_group_add,y). x - y)"
+ using uniformly_continuous_minus'[where ?'a = 'a]
+ by (simp add: uniformly_continuous_on_uniformity case_prod_unfold uniformity_prod_def filterlim_filtermap)
+
+
+
+lemma real_normed_vector_is_uniform_topological_group_add [Pure.intro]:
+ "OFCLASS('a :: real_normed_vector, uniform_topological_group_add_class)"
+proof
+ show "filterlim (\<lambda>((a::'a,b), (c,d)). (a + c, b + d)) uniformity (uniformity \<times>\<^sub>F uniformity)"
+ unfolding filterlim_def le_filter_def eventually_filtermap case_prod_unfold
+ proof safe
+ fix P :: "'a \<times> 'a \<Rightarrow> bool"
+ assume "eventually P uniformity"
+ then obtain \<epsilon> where \<epsilon>: "\<epsilon> > 0" "\<And>x y. dist x y < \<epsilon> \<Longrightarrow> P (x, y)"
+ by (auto simp: eventually_uniformity_metric)
+ define Q where "Q = (\<lambda>(x::'a,y). dist x y < \<epsilon> / 2)"
+ have Q: "eventually Q uniformity"
+ unfolding eventually_uniformity_metric Q_def using \<open>\<epsilon> > 0\<close>
+ by (meson case_prodI divide_pos_pos zero_less_numeral)
+ have "P (a + c, b + d)" if "Q (a, b)" "Q (c, d)" for a b c d
+ proof -
+ have "dist (a + c) (b + d) \<le> dist a b + dist c d"
+ by (simp add: dist_norm norm_diff_triangle_ineq)
+ also have "\<dots> < \<epsilon>"
+ using that by (auto simp: Q_def)
+ finally show ?thesis
+ by (intro \<epsilon>)
+ qed
+ thus "\<forall>\<^sub>F x in uniformity \<times>\<^sub>F uniformity. P (fst (fst x) + fst (snd x), snd (fst x) + snd (snd x))"
+ unfolding eventually_prod_filter by (intro exI[of _ Q] conjI Q) auto
+ qed
+next
+ show "filterlim (\<lambda>((a::'a), b). (-a, -b)) uniformity uniformity"
+ unfolding filterlim_def le_filter_def eventually_filtermap
+ proof safe
+ fix P :: "'a \<times> 'a \<Rightarrow> bool"
+ assume "eventually P uniformity"
+ then obtain \<epsilon> where \<epsilon>: "\<epsilon> > 0" "\<And>x y. dist x y < \<epsilon> \<Longrightarrow> P (x, y)"
+ by (auto simp: eventually_uniformity_metric)
+ show "\<forall>\<^sub>F x in uniformity. P (case x of (a, b) \<Rightarrow> (- a, - b))"
+ unfolding eventually_uniformity_metric
+ by (intro exI[of _ \<epsilon>]) (auto intro!: \<epsilon> simp: dist_norm norm_minus_commute)
+ qed
+qed
+
+instance real :: uniform_topological_group_add ..
+instance complex :: uniform_topological_group_add ..
+
+lemma cauchy_seq_finset_iff_vanishing:
+ "uniformity = filtercomap (\<lambda>(x,y). y - x :: 'a :: uniform_topological_group_add) (nhds 0)"
+proof -
+ have "filtercomap (\<lambda>x. (0, case x of (x, y) \<Rightarrow> y - (x :: 'a))) uniformity \<le> uniformity"
+ apply (simp add: le_filter_def eventually_filtercomap)
+ using uniformity_of_uniform_continuous_invariant[OF uniformly_continuous_add']
+ by (metis diff_self eq_diff_eq)
+ moreover
+ have "uniformity \<le> filtercomap (\<lambda>x. (0, case x of (x, y) \<Rightarrow> y - (x :: 'a))) uniformity"
+ apply (simp add: le_filter_def eventually_filtercomap)
+ using uniformity_of_uniform_continuous_invariant[OF uniformly_continuous_minus']
+ by (metis (mono_tags) diff_self eventually_mono surjective_pairing)
+ ultimately show ?thesis
+ by (simp add: nhds_eq_comap_uniformity filtercomap_filtercomap)
+qed
+
+subsubsection \<open>Metric spaces\<close>
+
instantiation\<^marker>\<open>tag unimportant\<close> prod :: (metric_space, metric_space) uniformity_dist begin
instance
proof
@@ -422,7 +552,7 @@
using uniformly_continuous_on_prod_metric[of UNIV UNIV]
by auto
-text \<open>This logically belong with the real vector spaces by we only have the necessary lemmas now.\<close>
+text \<open>This logically belong with the real vector spaces but we only have the necessary lemmas now.\<close>
lemma isUCont_plus[simp]:
shows \<open>isUCont (\<lambda>(x::'a::real_normed_vector,y). x+y)\<close>
proof (rule isUCont_prod_metric[THEN iffD2], intro allI impI, simp)
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Sun Feb 12 21:11:57 2023 +0100
@@ -2567,6 +2567,11 @@
definition\<^marker>\<open>tag important\<close> fps_expansion :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex fps" where
"fps_expansion f z0 = Abs_fps (\<lambda>n. (deriv ^^ n) f z0 / fact n)"
+lemma fps_expansion_cong:
+ assumes "\<forall>\<^sub>F w in nhds x. f w =g w"
+ shows "fps_expansion f x = fps_expansion g x"
+ unfolding fps_expansion_def using assms higher_deriv_cong_ev by fastforce
+
lemma
fixes r :: ereal
assumes "f holomorphic_on eball z0 r"
--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy Sun Feb 12 21:11:57 2023 +0100
@@ -26,8 +26,23 @@
lemma is_pole_tendsto:
fixes f::"('a::topological_space \<Rightarrow> 'b::real_normed_div_algebra)"
shows "is_pole f x \<Longrightarrow> ((inverse o f) \<longlongrightarrow> 0) (at x)"
-unfolding is_pole_def
-by (auto simp add:filterlim_inverse_at_iff[symmetric] comp_def filterlim_at)
+ unfolding is_pole_def
+ by (auto simp add:filterlim_inverse_at_iff[symmetric] comp_def filterlim_at)
+
+lemma is_pole_shift_0:
+ fixes f :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector)"
+ shows "is_pole f z \<longleftrightarrow> is_pole (\<lambda>x. f (z + x)) 0"
+ unfolding is_pole_def by (subst at_to_0) (auto simp: filterlim_filtermap add_ac)
+
+lemma is_pole_shift_0':
+ fixes f :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector)"
+ shows "NO_MATCH 0 z \<Longrightarrow> is_pole f z \<longleftrightarrow> is_pole (\<lambda>x. f (z + x)) 0"
+ by (metis is_pole_shift_0)
+
+lemma is_pole_compose_iff:
+ assumes "filtermap g (at x) = (at y)"
+ shows "is_pole (f \<circ> g) x \<longleftrightarrow> is_pole f y"
+ unfolding is_pole_def filterlim_def filtermap_compose assms ..
lemma is_pole_inverse_holomorphic:
assumes "open s"
@@ -71,6 +86,23 @@
by (intro filterlim_compose[OF filterlim_inverse_at_infinity] tendsto_intros)
(auto simp: filterlim_at eventually_at intro!: exI[of _ 1] tendsto_eq_intros)
+lemma is_pole_cmult_iff [simp]:
+ "c \<noteq> 0 \<Longrightarrow> is_pole (\<lambda>z. c * f z :: 'a :: real_normed_field) z \<longleftrightarrow> is_pole f z"
+proof
+ assume *: "c \<noteq> 0" "is_pole (\<lambda>z. c * f z) z"
+ have "is_pole (\<lambda>z. inverse c * (c * f z)) z" unfolding is_pole_def
+ by (rule tendsto_mult_filterlim_at_infinity tendsto_const)+ (use * in \<open>auto simp: is_pole_def\<close>)
+ thus "is_pole f z"
+ using *(1) by (simp add: field_simps)
+next
+ assume *: "c \<noteq> 0" "is_pole f z"
+ show "is_pole (\<lambda>z. c * f z) z" unfolding is_pole_def
+ by (rule tendsto_mult_filterlim_at_infinity tendsto_const)+ (use * in \<open>auto simp: is_pole_def\<close>)
+qed
+
+lemma is_pole_uminus_iff [simp]: "is_pole (\<lambda>z. -f z :: 'a :: real_normed_field) z \<longleftrightarrow> is_pole f z"
+ using is_pole_cmult_iff[of "-1" f] by (simp del: is_pole_cmult_iff)
+
lemma is_pole_inverse: "is_pole (\<lambda>z::complex. 1 / (z - a)) a"
using is_pole_inverse_power[of 1 a] by simp
@@ -80,7 +112,7 @@
shows "is_pole (\<lambda>z. f z / g z) z"
proof -
have "filterlim (\<lambda>z. f z * inverse (g z)) at_infinity (at z)"
- using assms filterlim_compose filterlim_inverse_at_infinity isCont_def
+ using assms filterlim_compose filterlim_inverse_at_infinity isCont_def
tendsto_mult_filterlim_at_infinity by blast
thus ?thesis by (simp add: field_split_simps is_pole_def)
qed
@@ -103,7 +135,106 @@
shows "is_pole (\<lambda>w. f w / w ^ n) 0"
using is_pole_basic[of f A 0] assms by simp
-text \<open>The proposition
+lemma is_pole_compose:
+ assumes "is_pole f w" "g \<midarrow>z\<rightarrow> w" "eventually (\<lambda>z. g z \<noteq> w) (at z)"
+ shows "is_pole (\<lambda>x. f (g x)) z"
+ using assms(1) unfolding is_pole_def
+ by (rule filterlim_compose) (use assms in \<open>auto simp: filterlim_at\<close>)
+
+lemma is_pole_plus_const_iff:
+ "is_pole f z \<longleftrightarrow> is_pole (\<lambda>x. f x + c) z"
+proof
+ assume "is_pole f z"
+ then have "filterlim f at_infinity (at z)" unfolding is_pole_def .
+ moreover have "((\<lambda>_. c) \<longlongrightarrow> c) (at z)" by auto
+ ultimately have " LIM x (at z). f x + c :> at_infinity"
+ using tendsto_add_filterlim_at_infinity'[of f "at z"] by auto
+ then show "is_pole (\<lambda>x. f x + c) z" unfolding is_pole_def .
+next
+ assume "is_pole (\<lambda>x. f x + c) z"
+ then have "filterlim (\<lambda>x. f x + c) at_infinity (at z)"
+ unfolding is_pole_def .
+ moreover have "((\<lambda>_. -c) \<longlongrightarrow> -c) (at z)" by auto
+ ultimately have " LIM x (at z). f x :> at_infinity"
+ using tendsto_add_filterlim_at_infinity'[of "(\<lambda>x. f x + c)"
+ "at z" "(\<lambda>_. - c)" "-c"]
+ by auto
+ then show "is_pole f z" unfolding is_pole_def .
+qed
+
+lemma is_pole_minus_const_iff:
+ "is_pole (\<lambda>x. f x - c) z \<longleftrightarrow> is_pole f z"
+ using is_pole_plus_const_iff [of f z "-c"] by simp
+
+lemma is_pole_alt:
+ "is_pole f x = (\<forall>B>0. \<exists>U. open U \<and> x\<in>U \<and> (\<forall>y\<in>U. y\<noteq>x \<longrightarrow> norm (f y)\<ge>B))"
+ unfolding is_pole_def
+ unfolding filterlim_at_infinity[of 0,simplified] eventually_at_topological
+ by auto
+
+lemma is_pole_mult_analytic_nonzero1:
+ assumes "is_pole g x" "f analytic_on {x}" "f x \<noteq> 0"
+ shows "is_pole (\<lambda>x. f x * g x) x"
+ unfolding is_pole_def
+proof (rule tendsto_mult_filterlim_at_infinity)
+ show "f \<midarrow>x\<rightarrow> f x"
+ using assms by (simp add: analytic_at_imp_isCont isContD)
+qed (use assms in \<open>auto simp: is_pole_def\<close>)
+
+lemma is_pole_mult_analytic_nonzero2:
+ assumes "is_pole f x" "g analytic_on {x}" "g x \<noteq> 0"
+ shows "is_pole (\<lambda>x. f x * g x) x"
+ by (subst mult.commute, rule is_pole_mult_analytic_nonzero1) (use assms in auto)
+
+lemma is_pole_mult_analytic_nonzero1_iff:
+ assumes "f analytic_on {x}" "f x \<noteq> 0"
+ shows "is_pole (\<lambda>x. f x * g x) x \<longleftrightarrow> is_pole g x"
+proof
+ assume "is_pole g x"
+ thus "is_pole (\<lambda>x. f x * g x) x"
+ by (intro is_pole_mult_analytic_nonzero1 assms)
+next
+ assume "is_pole (\<lambda>x. f x * g x) x"
+ hence "is_pole (\<lambda>x. inverse (f x) * (f x * g x)) x"
+ by (rule is_pole_mult_analytic_nonzero1)
+ (use assms in \<open>auto intro!: analytic_intros\<close>)
+ also have "?this \<longleftrightarrow> is_pole g x"
+ proof (rule is_pole_cong)
+ have "eventually (\<lambda>x. f x \<noteq> 0) (at x)"
+ using assms by (simp add: analytic_at_neq_imp_eventually_neq)
+ thus "eventually (\<lambda>x. inverse (f x) * (f x * g x) = g x) (at x)"
+ by eventually_elim auto
+ qed auto
+ finally show "is_pole g x" .
+qed
+
+lemma is_pole_mult_analytic_nonzero2_iff:
+ assumes "g analytic_on {x}" "g x \<noteq> 0"
+ shows "is_pole (\<lambda>x. f x * g x) x \<longleftrightarrow> is_pole f x"
+ by (subst mult.commute, rule is_pole_mult_analytic_nonzero1_iff) (fact assms)+
+
+lemma frequently_const_imp_not_is_pole:
+ fixes z :: "'a::first_countable_topology"
+ assumes "frequently (\<lambda>w. f w = c) (at z)"
+ shows "\<not> is_pole f z"
+proof
+ assume "is_pole f z"
+ from assms have "z islimpt {w. f w = c}"
+ by (simp add: islimpt_conv_frequently_at)
+ then obtain g where g: "\<And>n. g n \<in> {w. f w = c} - {z}" "g \<longlonglongrightarrow> z"
+ unfolding islimpt_sequential by blast
+ then have "(f \<circ> g) \<longlonglongrightarrow> c"
+ by (simp add: tendsto_eventually)
+ moreover have *: "filterlim g (at z) sequentially"
+ using g by (auto simp: filterlim_at)
+ have "filterlim (f \<circ> g) at_infinity sequentially"
+ unfolding o_def by (rule filterlim_compose [OF _ *])
+ (use \<open>is_pole f z\<close> in \<open>simp add: is_pole_def\<close>)
+ ultimately show False
+ using not_tendsto_and_filterlim_at_infinity trivial_limit_sequentially by blast
+qed
+
+ text \<open>The proposition
\<^term>\<open>\<exists>x. ((f::complex\<Rightarrow>complex) \<longlongrightarrow> x) (at z) \<or> is_pole f z\<close>
can be interpreted as the complex function \<^term>\<open>f\<close> has a non-essential singularity at \<^term>\<open>z\<close>
(i.e. the singularity is either removable or a pole).\<close>
@@ -113,6 +244,95 @@
definition isolated_singularity_at::"[complex \<Rightarrow> complex, complex] \<Rightarrow> bool" where
"isolated_singularity_at f z = (\<exists>r>0. f analytic_on ball z r-{z})"
+lemma not_essential_cong:
+ assumes "eventually (\<lambda>x. f x = g x) (at z)" "z = z'"
+ shows "not_essential f z \<longleftrightarrow> not_essential g z'"
+ unfolding not_essential_def using assms filterlim_cong is_pole_cong by fastforce
+
+lemma isolated_singularity_at_cong:
+ assumes "eventually (\<lambda>x. f x = g x) (at z)" "z = z'"
+ shows "isolated_singularity_at f z \<longleftrightarrow> isolated_singularity_at g z'"
+proof -
+ have "isolated_singularity_at g z"
+ if "isolated_singularity_at f z" "eventually (\<lambda>x. f x = g x) (at z)" for f g
+ proof -
+ from that(1) obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
+ by (auto simp: isolated_singularity_at_def)
+ from that(2) obtain r' where r': "r' > 0" "\<forall>x\<in>ball z r'-{z}. f x = g x"
+ unfolding eventually_at_filter eventually_nhds_metric by (auto simp: dist_commute)
+
+ have "f holomorphic_on ball z r - {z}"
+ using r(2) by (subst (asm) analytic_on_open) auto
+ hence "f holomorphic_on ball z (min r r') - {z}"
+ by (rule holomorphic_on_subset) auto
+ also have "?this \<longleftrightarrow> g holomorphic_on ball z (min r r') - {z}"
+ using r' by (intro holomorphic_cong) auto
+ also have "\<dots> \<longleftrightarrow> g analytic_on ball z (min r r') - {z}"
+ by (subst analytic_on_open) auto
+ finally show ?thesis
+ unfolding isolated_singularity_at_def
+ by (intro exI[of _ "min r r'"]) (use \<open>r > 0\<close> \<open>r' > 0\<close> in auto)
+ qed
+ from this[of f g] this[of g f] assms show ?thesis
+ by (auto simp: eq_commute)
+qed
+
+lemma removable_singularity:
+ assumes "f holomorphic_on A - {x}" "open A"
+ assumes "f \<midarrow>x\<rightarrow> c"
+ shows "(\<lambda>y. if y = x then c else f y) holomorphic_on A" (is "?g holomorphic_on _")
+proof -
+ have "continuous_on A ?g"
+ unfolding continuous_on_def
+ proof
+ fix y assume y: "y \<in> A"
+ show "(?g \<longlongrightarrow> ?g y) (at y within A)"
+ proof (cases "y = x")
+ case False
+ have "continuous_on (A - {x}) f"
+ using assms(1) by (meson holomorphic_on_imp_continuous_on)
+ hence "(f \<longlongrightarrow> ?g y) (at y within A - {x})"
+ using False y by (auto simp: continuous_on_def)
+ also have "?this \<longleftrightarrow> (?g \<longlongrightarrow> ?g y) (at y within A - {x})"
+ by (intro filterlim_cong refl) (auto simp: eventually_at_filter)
+ also have "at y within A - {x} = at y within A"
+ using y assms False
+ by (intro at_within_nhd[of _ "A - {x}"]) auto
+ finally show ?thesis .
+ next
+ case [simp]: True
+ have "f \<midarrow>x\<rightarrow> c"
+ by fact
+ also have "?this \<longleftrightarrow> (?g \<longlongrightarrow> ?g y) (at y)"
+ by (intro filterlim_cong) (auto simp: eventually_at_filter)
+ finally show ?thesis
+ by (meson Lim_at_imp_Lim_at_within)
+ qed
+ qed
+ moreover {
+ have "?g holomorphic_on A - {x}"
+ using assms(1) holomorphic_transform by fastforce
+ }
+ ultimately show ?thesis
+ by (rule no_isolated_singularity) (use assms in auto)
+qed
+
+lemma removable_singularity':
+ assumes "isolated_singularity_at f z"
+ assumes "f \<midarrow>z\<rightarrow> c"
+ shows "(\<lambda>y. if y = z then c else f y) analytic_on {z}"
+proof -
+ from assms obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
+ by (auto simp: isolated_singularity_at_def)
+ have "(\<lambda>y. if y = z then c else f y) holomorphic_on ball z r"
+ proof (rule removable_singularity)
+ show "f holomorphic_on ball z r - {z}"
+ using r(2) by (subst (asm) analytic_on_open) auto
+ qed (use assms in auto)
+ thus ?thesis
+ using r(1) unfolding analytic_at by (intro exI[of _ "ball z r"]) auto
+qed
+
named_theorems singularity_intros "introduction rules for singularities"
lemma holomorphic_factor_unique:
@@ -137,7 +357,7 @@
define f' where "f' \<equiv> \<lambda>x. (x - z) powr (n-m)"
have "f' z=0" using \<open>n>m\<close> unfolding f'_def by auto
moreover have "continuous F f'" unfolding f'_def F_def continuous_def
- using \<open>n>m\<close>
+ using \<open>n>m\<close>
by (auto simp add: Lim_ident_at intro!:tendsto_powr_complex_0 tendsto_eq_intros)
ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
by (simp add: continuous_within)
@@ -165,7 +385,7 @@
define f' where "f' \<equiv>\<lambda>x. (x - z) powr (m-n)"
have "f' z=0" using \<open>m>n\<close> unfolding f'_def by auto
moreover have "continuous F f'" unfolding f'_def F_def continuous_def
- using \<open>m>n\<close>
+ using \<open>m>n\<close>
by (auto simp: Lim_ident_at intro!:tendsto_powr_complex_0 tendsto_eq_intros)
ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
by (simp add: continuous_within)
@@ -272,7 +492,7 @@
ultimately show ?thesis by auto
qed
- have ?thesis when "\<exists>x. (f \<longlongrightarrow> x) (at z)"
+ have ?thesis when "\<exists>x. (f \<longlongrightarrow> x) (at z)"
apply (rule_tac imp_unique[unfolded P_def])
using P_exist[OF that(1) f_iso non_zero] unfolding P_def .
moreover have ?thesis when "is_pole f z"
@@ -312,7 +532,7 @@
have "P f (-n) (inverse o g) r"
proof -
have "f w = inverse (g w) * (w - z) powr of_int (- n)" when "w\<in>cball z r - {z}" for w
- by (metis g_fac h_def inverse_inverse_eq inverse_mult_distrib of_int_minus
+ by (metis g_fac h_def inverse_inverse_eq inverse_mult_distrib of_int_minus
powr_minus that)
then show ?thesis
unfolding P_def comp_def
@@ -398,7 +618,7 @@
have "(\<lambda>w. inverse ((f w) ^ (nat (-n)))) \<midarrow>z\<rightarrow>?xx"
using assms False unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
then have "fp \<midarrow>z\<rightarrow> ?xx"
- by (smt (verit) LIM_cong fp_def inverse_nonzero_iff_nonzero power_eq_0_iff powr_eq_0_iff
+ by (smt (verit) LIM_cong fp_def inverse_nonzero_iff_nonzero power_eq_0_iff powr_eq_0_iff
powr_of_int that zero_less_nat_eq)
then show ?thesis unfolding fp_def not_essential_def by auto
qed
@@ -520,7 +740,7 @@
using that by (auto intro!:tendsto_eq_intros)
then have "fg \<midarrow>z\<rightarrow> 0"
using Lim_transform_within[OF _ \<open>r1>0\<close>]
- by (smt (verit, ccfv_SIG) DiffI dist_commute dist_nz fg_times mem_ball powr_of_int right_minus_eq
+ by (smt (verit, ccfv_SIG) DiffI dist_commute dist_nz fg_times mem_ball powr_of_int right_minus_eq
singletonD that)
then show ?thesis unfolding not_essential_def fg_def by auto
qed
@@ -629,7 +849,7 @@
using f_iso unfolding isolated_singularity_at_def by auto
define d3 where "d3=min d1 d2"
have "d3>0" unfolding d3_def using \<open>d1>0\<close> \<open>d2>0\<close> by auto
- moreover
+ moreover
have "f analytic_on ball z d3 - {z}"
by (smt (verit, best) Diff_iff analytic_on_analytic_at d2 d3_def mem_ball)
then have "vf analytic_on ball z d3 - {z}"
@@ -712,8 +932,156 @@
using assms unfolding isolated_singularity_at_def
by (metis analytic_on_holomorphic centre_in_ball insert_Diff openE open_delete subset_insert_iff)
-subsubsection \<open>The order of non-essential singularities (i.e. removable singularities or poles)\<close>
+lemma isolated_singularity_at_altdef:
+ "isolated_singularity_at f z \<longleftrightarrow> eventually (\<lambda>z. f analytic_on {z}) (at z)"
+proof
+ assume "isolated_singularity_at f z"
+ then obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
+ unfolding isolated_singularity_at_def by blast
+ have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
+ using r(1) by (intro eventually_at_in_open) auto
+ thus "eventually (\<lambda>z. f analytic_on {z}) (at z)"
+ by eventually_elim (use r analytic_on_subset in auto)
+next
+ assume "eventually (\<lambda>z. f analytic_on {z}) (at z)"
+ then obtain A where A: "open A" "z \<in> A" "\<And>w. w \<in> A - {z} \<Longrightarrow> f analytic_on {w}"
+ unfolding eventually_at_topological by blast
+ then show "isolated_singularity_at f z"
+ by (meson analytic_imp_holomorphic analytic_on_analytic_at isolated_singularity_at_holomorphic)
+qed
+
+lemma isolated_singularity_at_shift:
+ assumes "isolated_singularity_at (\<lambda>x. f (x + w)) z"
+ shows "isolated_singularity_at f (z + w)"
+proof -
+ from assms obtain r where r: "r > 0" and ana: "(\<lambda>x. f (x + w)) analytic_on ball z r - {z}"
+ unfolding isolated_singularity_at_def by blast
+ have "((\<lambda>x. f (x + w)) \<circ> (\<lambda>x. x - w)) analytic_on (ball (z + w) r - {z + w})"
+ by (rule analytic_on_compose_gen[OF _ ana])
+ (auto simp: dist_norm algebra_simps intro!: analytic_intros)
+ hence "f analytic_on (ball (z + w) r - {z + w})"
+ by (simp add: o_def)
+ thus ?thesis using r
+ unfolding isolated_singularity_at_def by blast
+qed
+
+lemma isolated_singularity_at_shift_iff:
+ "isolated_singularity_at f (z + w) \<longleftrightarrow> isolated_singularity_at (\<lambda>x. f (x + w)) z"
+ using isolated_singularity_at_shift[of f w z]
+ isolated_singularity_at_shift[of "\<lambda>x. f (x + w)" "-w" "w + z"]
+ by (auto simp: algebra_simps)
+
+lemma isolated_singularity_at_shift_0:
+ "NO_MATCH 0 z \<Longrightarrow> isolated_singularity_at f z \<longleftrightarrow> isolated_singularity_at (\<lambda>x. f (z + x)) 0"
+ using isolated_singularity_at_shift_iff[of f 0 z] by (simp add: add_ac)
+
+lemma not_essential_shift:
+ assumes "not_essential (\<lambda>x. f (x + w)) z"
+ shows "not_essential f (z + w)"
+proof -
+ from assms consider c where "(\<lambda>x. f (x + w)) \<midarrow>z\<rightarrow> c" | "is_pole (\<lambda>x. f (x + w)) z"
+ unfolding not_essential_def by blast
+ thus ?thesis
+ proof cases
+ case (1 c)
+ hence "f \<midarrow>z + w\<rightarrow> c"
+ by (smt (verit, ccfv_SIG) LIM_cong add.assoc filterlim_at_to_0)
+ thus ?thesis
+ by (auto simp: not_essential_def)
+ next
+ case 2
+ hence "is_pole f (z + w)"
+ by (subst is_pole_shift_iff [symmetric]) (auto simp: o_def add_ac)
+ thus ?thesis
+ by (auto simp: not_essential_def)
+ qed
+qed
+
+lemma not_essential_shift_iff: "not_essential f (z + w) \<longleftrightarrow> not_essential (\<lambda>x. f (x + w)) z"
+ using not_essential_shift[of f w z]
+ not_essential_shift[of "\<lambda>x. f (x + w)" "-w" "w + z"]
+ by (auto simp: algebra_simps)
+
+lemma not_essential_shift_0:
+ "NO_MATCH 0 z \<Longrightarrow> not_essential f z \<longleftrightarrow> not_essential (\<lambda>x. f (z + x)) 0"
+ using not_essential_shift_iff[of f 0 z] by (simp add: add_ac)
+lemma not_essential_holomorphic:
+ assumes "f holomorphic_on A" "x \<in> A" "open A"
+ shows "not_essential f x"
+proof -
+ have "continuous_on A f"
+ using assms holomorphic_on_imp_continuous_on by blast
+ hence "f \<midarrow>x\<rightarrow> f x"
+ using assms continuous_on_eq_continuous_at isContD by blast
+ thus ?thesis
+ by (auto simp: not_essential_def)
+qed
+
+lemma not_essential_analytic:
+ assumes "f analytic_on {z}"
+ shows "not_essential f z"
+ using analytic_at assms not_essential_holomorphic by blast
+
+lemma not_essential_id [singularity_intros]: "not_essential (\<lambda>w. w) z"
+ by (simp add: not_essential_analytic)
+
+lemma is_pole_imp_not_essential [intro]: "is_pole f z \<Longrightarrow> not_essential f z"
+ by (auto simp: not_essential_def)
+
+lemma tendsto_imp_not_essential [intro]: "f \<midarrow>z\<rightarrow> c \<Longrightarrow> not_essential f z"
+ by (auto simp: not_essential_def)
+
+lemma eventually_not_pole:
+ assumes "isolated_singularity_at f z"
+ shows "eventually (\<lambda>w. \<not>is_pole f w) (at z)"
+proof -
+ from assms obtain r where "r > 0" and r: "f analytic_on ball z r - {z}"
+ by (auto simp: isolated_singularity_at_def)
+ then have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
+ by (intro eventually_at_in_open) auto
+ thus "eventually (\<lambda>w. \<not>is_pole f w) (at z)"
+ proof eventually_elim
+ case (elim w)
+ with r show ?case
+ using analytic_imp_holomorphic not_is_pole_holomorphic open_delete by blast
+ qed
+qed
+
+lemma not_islimpt_poles:
+ assumes "isolated_singularity_at f z"
+ shows "\<not>z islimpt {w. is_pole f w}"
+ using eventually_not_pole [OF assms]
+ by (auto simp: islimpt_conv_frequently_at frequently_def)
+
+lemma analytic_at_imp_no_pole: "f analytic_on {z} \<Longrightarrow> \<not>is_pole f z"
+ using analytic_at not_is_pole_holomorphic by blast
+
+lemma not_essential_const [singularity_intros]: "not_essential (\<lambda>_. c) z"
+ unfolding not_essential_def by (rule exI[of _ c]) auto
+
+lemma not_essential_uminus [singularity_intros]:
+ assumes f_ness: "not_essential f z"
+ assumes f_iso:"isolated_singularity_at f z"
+ shows "not_essential (\<lambda>w. -f w) z"
+proof -
+ have "not_essential (\<lambda>w. -1 * f w) z"
+ by (intro assms singularity_intros)
+ thus ?thesis by simp
+qed
+
+lemma isolated_singularity_at_analytic:
+ assumes "f analytic_on {z}"
+ shows "isolated_singularity_at f z"
+proof -
+ from assms obtain r where r: "r > 0" "f holomorphic_on ball z r"
+ by (auto simp: analytic_on_def)
+ show ?thesis
+ by (rule isolated_singularity_at_holomorphic[of f "ball z r"])
+ (use \<open>r > 0\<close> in \<open>auto intro!: holomorphic_on_subset[OF r(2)]\<close>)
+qed
+
+subsection \<open>The order of non-essential singularities (i.e. removable singularities or poles)\<close>
definition\<^marker>\<open>tag important\<close> zorder :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> int" where
"zorder f z = (THE n. (\<exists>h r. r>0 \<and> h holomorphic_on cball z r \<and> h z\<noteq>0
@@ -749,6 +1117,29 @@
then show ?thesis unfolding P_def by auto
qed
+lemma zorder_shift:
+ shows "zorder f z = zorder (\<lambda>u. f (u + z)) 0"
+ unfolding zorder_def
+ apply (rule arg_cong [of concl: The])
+ apply (auto simp: fun_eq_iff Ball_def dist_norm)
+ subgoal for x h r
+ apply (rule_tac x="h o (+)z" in exI)
+ apply (rule_tac x="r" in exI)
+ apply (intro conjI holomorphic_on_compose holomorphic_intros)
+ apply (simp_all flip: cball_translation)
+ apply (simp add: add.commute)
+ done
+ subgoal for x h r
+ apply (rule_tac x="h o (\<lambda>u. u-z)" in exI)
+ apply (rule_tac x="r" in exI)
+ apply (intro conjI holomorphic_on_compose holomorphic_intros)
+ apply (simp_all add: flip: cball_translation_subtract)
+ by (metis diff_add_cancel eq_iff_diff_eq_0 norm_minus_commute)
+ done
+
+lemma zorder_shift': "NO_MATCH 0 z \<Longrightarrow> zorder f z = zorder (\<lambda>u. f (u + z)) 0"
+ by (rule zorder_shift)
+
lemma
fixes f::"complex \<Rightarrow> complex" and z::complex
assumes f_iso:"isolated_singularity_at f z"
@@ -819,6 +1210,99 @@
by (metis DiffI dist_commute mem_ball singletonD)
qed
+lemma zor_poly_shift:
+ assumes iso1: "isolated_singularity_at f z"
+ and ness1: "not_essential f z"
+ and nzero1: "\<exists>\<^sub>F w in at z. f w \<noteq> 0"
+ shows "\<forall>\<^sub>F w in nhds z. zor_poly f z w = zor_poly (\<lambda>u. f (z + u)) 0 (w-z)"
+proof -
+ obtain r1 where "r1>0" "zor_poly f z z \<noteq> 0" and
+ holo1:"zor_poly f z holomorphic_on cball z r1" and
+ rball1:"\<forall>w\<in>cball z r1 - {z}.
+ f w = zor_poly f z w * (w - z) powr of_int (zorder f z) \<and>
+ zor_poly f z w \<noteq> 0"
+ using zorder_exist[OF iso1 ness1 nzero1] by blast
+
+ define ff where "ff=(\<lambda>u. f (z + u))"
+ have "isolated_singularity_at ff 0"
+ unfolding ff_def
+ using iso1 isolated_singularity_at_shift_iff[of f 0 z]
+ by (simp add:algebra_simps)
+ moreover have "not_essential ff 0"
+ unfolding ff_def
+ using ness1 not_essential_shift_iff[of f 0 z]
+ by (simp add:algebra_simps)
+ moreover have "\<exists>\<^sub>F w in at 0. ff w \<noteq> 0"
+ unfolding ff_def using nzero1
+ by (smt (verit, ccfv_SIG) add.commute eventually_at_to_0
+ eventually_mono not_frequently)
+ ultimately obtain r2 where "r2>0" "zor_poly ff 0 0 \<noteq> 0" and
+ holo2:"zor_poly ff 0 holomorphic_on cball 0 r2" and
+ rball2:"\<forall>w\<in>cball 0 r2 - {0}.
+ ff w = zor_poly ff 0 w * w powr of_int (zorder ff 0) \<and>
+ zor_poly ff 0 w \<noteq> 0"
+ using zorder_exist[of ff 0] by auto
+
+ define r where "r=min r1 r2"
+ have "r>0" using \<open>r1>0\<close> \<open>r2>0\<close> unfolding r_def by auto
+
+ have "zor_poly f z w = zor_poly ff 0 (w - z)"
+ if "w\<in>ball z r - {z}" for w
+ proof -
+ define n::complex where "n= of_int (zorder f z)"
+
+ have "f w = zor_poly f z w * (w - z) powr n"
+ proof -
+ have "w\<in>cball z r1 - {z}"
+ using r_def that by auto
+ from rball1[rule_format, OF this]
+ show ?thesis unfolding n_def by auto
+ qed
+
+ moreover have "f w = zor_poly ff 0 (w - z) * (w - z) powr n"
+ proof -
+ have "w-z\<in>cball 0 r2 - {0}"
+ using r_def that by (auto simp:dist_complex_def)
+ from rball2[rule_format, OF this]
+ have "ff (w - z) = zor_poly ff 0 (w - z) * (w - z)
+ powr of_int (zorder ff 0)"
+ by simp
+ moreover have "of_int (zorder ff 0) = n"
+ unfolding n_def ff_def by (simp add:zorder_shift' add.commute)
+ ultimately show ?thesis unfolding ff_def by auto
+ qed
+ ultimately have "zor_poly f z w * (w - z) powr n
+ = zor_poly ff 0 (w - z) * (w - z) powr n"
+ by auto
+ moreover have "(w - z) powr n \<noteq>0"
+ using that by auto
+ ultimately show ?thesis
+ apply (subst (asm) mult_cancel_right)
+ by (simp add:ff_def)
+ qed
+ then have "\<forall>\<^sub>F w in at z. zor_poly f z w
+ = zor_poly ff 0 (w - z)"
+ unfolding eventually_at
+ apply (rule_tac x=r in exI)
+ using \<open>r>0\<close> by (auto simp:dist_commute)
+ moreover have "isCont (zor_poly f z) z"
+ using holo1[THEN holomorphic_on_imp_continuous_on]
+ apply (elim continuous_on_interior)
+ using \<open>r1>0\<close> by auto
+ moreover have "isCont (\<lambda>w. zor_poly ff 0 (w - z)) z"
+ proof -
+ have "isCont (zor_poly ff 0) 0"
+ using holo2[THEN holomorphic_on_imp_continuous_on]
+ apply (elim continuous_on_interior)
+ using \<open>r2>0\<close> by auto
+ then show ?thesis
+ unfolding isCont_iff by simp
+ qed
+ ultimately show "\<forall>\<^sub>F w in nhds z. zor_poly f z w
+ = zor_poly ff 0 (w - z)"
+ by (elim at_within_isCont_imp_nhds;auto)
+qed
+
lemma
fixes f g::"complex \<Rightarrow> complex" and z::complex
assumes f_iso:"isolated_singularity_at f z" and g_iso:"isolated_singularity_at g z"
@@ -979,7 +1463,7 @@
have fz_lim: "f\<midarrow> z \<rightarrow> f z"
by (metis assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on)
have gz_lim: "g \<midarrow>z\<rightarrow>g z"
- by (metis r open_ball at_within_open ball_subset_cball centre_in_ball
+ by (metis r open_ball at_within_open ball_subset_cball centre_in_ball
continuous_on_def continuous_on_subset holomorphic_on_imp_continuous_on)
have if_0:"if f z=0 then n > 0 else n=0"
proof -
@@ -1185,7 +1669,7 @@
unfolding z'_def using \<open>d>0\<close> \<open>r>0\<close> by (auto simp add:dist_norm)
moreover have "f z' \<noteq> 0"
proof (subst fg_eq[OF _ \<open>z'\<noteq>z\<close>])
- have "z' \<in> cball z r"
+ have "z' \<in> cball z r"
unfolding z'_def using \<open>r>0\<close> \<open>d>0\<close> by (auto simp add:dist_norm)
then show " z' \<in> s" using r(2) by blast
show "g z' * (z' - z) powr of_int n \<noteq> 0"
@@ -1354,6 +1838,33 @@
using \<open>z=z'\<close> unfolding P_def zorder_def zor_poly_def by auto
qed
+lemma zorder_times_analytic':
+ assumes "isolated_singularity_at f z" "not_essential f z"
+ assumes "g analytic_on {z}" "frequently (\<lambda>z. f z * g z \<noteq> 0) (at z)"
+ shows "zorder (\<lambda>x. f x * g x) z = zorder f z + zorder g z"
+proof (rule zorder_times)
+ show "isolated_singularity_at g z" "not_essential g z"
+ by (intro isolated_singularity_at_analytic not_essential_analytic assms)+
+qed (use assms in auto)
+
+lemma zorder_cmult:
+ assumes "c \<noteq> 0"
+ shows "zorder (\<lambda>z. c * f z) z = zorder f z"
+proof -
+ define P where
+ "P = (\<lambda>f n h r. 0 < r \<and> h holomorphic_on cball z r \<and>
+ h z \<noteq> 0 \<and> (\<forall>w\<in>cball z r - {z}. f w = h w * (w - z) powr of_int n \<and> h w \<noteq> 0))"
+ have *: "P (\<lambda>x. c * f x) n (\<lambda>x. c * h x) r" if "P f n h r" "c \<noteq> 0" for f n h r c
+ using that unfolding P_def by (auto intro!: holomorphic_intros)
+ have "(\<exists>h r. P (\<lambda>x. c * f x) n h r) \<longleftrightarrow> (\<exists>h r. P f n h r)" for n
+ using *[of f n _ _ c] *[of "\<lambda>x. c * f x" n _ _ "inverse c"] \<open>c \<noteq> 0\<close>
+ by (fastforce simp: field_simps)
+ hence "(THE n. \<exists>h r. P (\<lambda>x. c * f x) n h r) = (THE n. \<exists>h r. P f n h r)"
+ by simp
+ thus ?thesis
+ by (simp add: zorder_def P_def)
+qed
+
lemma zorder_nonzero_div_power:
assumes sz: "open s" "z \<in> s" "f holomorphic_on s" "f z \<noteq> 0" and "n > 0"
shows "zorder (\<lambda>w. f w / (w - z) ^ n) z = - n"
@@ -1493,4 +2004,735 @@
from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis .
qed
-end
\ No newline at end of file
+lemma
+ assumes "is_pole f (x :: complex)" "open A" "x \<in> A"
+ assumes "\<And>y. y \<in> A - {x} \<Longrightarrow> (f has_field_derivative f' y) (at y)"
+ shows is_pole_deriv': "is_pole f' x"
+ and zorder_deriv': "zorder f' x = zorder f x - 1"
+proof -
+ have holo: "f holomorphic_on A - {x}"
+ using assms by (subst holomorphic_on_open) auto
+ obtain r where r: "r > 0" "ball x r \<subseteq> A"
+ using assms(2,3) openE by blast
+ moreover have "open (ball x r - {x})"
+ by auto
+ ultimately have "isolated_singularity_at f x"
+ by (auto simp: isolated_singularity_at_def analytic_on_open
+ intro!: exI[of _ r] holomorphic_on_subset[OF holo])
+ hence ev: "\<forall>\<^sub>F w in at x. zor_poly f x w = f w * (w - x) ^ nat (- zorder f x)"
+ using \<open>is_pole f x\<close> zor_poly_pole_eq by blast
+
+ define P where "P = zor_poly f x"
+ define n where "n = nat (-zorder f x)"
+
+ obtain r where r: "r > 0" "cball x r \<subseteq> A" "P holomorphic_on cball x r" "zorder f x < 0" "P x \<noteq> 0"
+ "\<forall>w\<in>cball x r - {x}. f w = P w / (w - x) ^ n \<and> P w \<noteq> 0"
+ unfolding P_def n_def using zorder_exist_pole[OF holo assms(2,3,1)] by blast
+ have n: "n > 0"
+ using r(4) by (auto simp: n_def)
+
+ have [derivative_intros]: "(P has_field_derivative deriv P w) (at w)"
+ if "w \<in> ball x r" for w
+ using that by (intro holomorphic_derivI[OF holomorphic_on_subset[OF r(3), of "ball x r"]]) auto
+
+ define D where "D = (\<lambda>w. (deriv P w * (w - x) - of_nat n * P w) / (w - x) ^ (n + 1))"
+ define n' where "n' = n - 1"
+ have n': "n = Suc n'"
+ using n by (simp add: n'_def)
+
+ have "eventually (\<lambda>w. w \<in> ball x r) (nhds x)"
+ using \<open>r > 0\<close> by (intro eventually_nhds_in_open) auto
+ hence ev'': "eventually (\<lambda>w. w \<in> ball x r - {x}) (at x)"
+ by (auto simp: eventually_at_filter elim: eventually_mono)
+
+ {
+ fix w assume w: "w \<in> ball x r - {x}"
+ have ev': "eventually (\<lambda>w. w \<in> ball x r - {x}) (nhds w)"
+ using w by (intro eventually_nhds_in_open) auto
+
+ have "((\<lambda>w. P w / (w - x) ^ n) has_field_derivative D w) (at w)"
+ apply (rule derivative_eq_intros refl | use w in force)+
+ using w
+ apply (simp add: divide_simps D_def)
+ apply (simp add: n' algebra_simps)
+ done
+ also have "?this \<longleftrightarrow> (f has_field_derivative D w) (at w)"
+ using r by (intro has_field_derivative_cong_ev refl eventually_mono[OF ev']) auto
+ finally have "(f has_field_derivative D w) (at w)" .
+ moreover have "(f has_field_derivative f' w) (at w)"
+ using w r by (intro assms) auto
+ ultimately have "D w = f' w"
+ using DERIV_unique by blast
+ } note D_eq = this
+
+ have "is_pole D x"
+ unfolding D_def using n \<open>r > 0\<close> \<open>P x \<noteq> 0\<close>
+ by (intro is_pole_basic[where A = "ball x r"] holomorphic_intros holomorphic_on_subset[OF r(3)]) auto
+ also have "?this \<longleftrightarrow> is_pole f' x"
+ by (intro is_pole_cong eventually_mono[OF ev''] D_eq) auto
+ finally show "is_pole f' x" .
+
+ have "zorder f' x = -int (Suc n)"
+ proof (rule zorder_eqI)
+ show "open (ball x r)" "x \<in> ball x r"
+ using \<open>r > 0\<close> by auto
+ show "f' w = (deriv P w * (w - x) - of_nat n * P w) * (w - x) powr of_int (- int (Suc n))"
+ if "w \<in> ball x r" "w \<noteq> x" for w
+ using that D_eq[of w] n by (auto simp: D_def powr_diff powr_minus powr_nat' divide_simps)
+ qed (use r n in \<open>auto intro!: holomorphic_intros\<close>)
+ thus "zorder f' x = zorder f x - 1"
+ using n by (simp add: n_def)
+qed
+
+lemma
+ assumes "is_pole f (x :: complex)" "isolated_singularity_at f x"
+ shows is_pole_deriv: "is_pole (deriv f) x"
+ and zorder_deriv: "zorder (deriv f) x = zorder f x - 1"
+proof -
+ from assms(2) obtain r where r: "r > 0" "f analytic_on ball x r - {x}"
+ by (auto simp: isolated_singularity_at_def)
+ hence holo: "f holomorphic_on ball x r - {x}"
+ by (subst (asm) analytic_on_open) auto
+ have *: "x \<in> ball x r" "open (ball x r)" "open (ball x r - {x})"
+ using \<open>r > 0\<close> by auto
+ show "is_pole (deriv f) x" "zorder (deriv f) x = zorder f x - 1"
+ by (rule is_pole_deriv' zorder_deriv', (rule assms * holomorphic_derivI holo | assumption)+)+
+qed
+
+lemma removable_singularity_deriv':
+ assumes "f \<midarrow>x\<rightarrow> c" "x \<in> A" "open (A :: complex set)"
+ assumes "\<And>y. y \<in> A - {x} \<Longrightarrow> (f has_field_derivative f' y) (at y)"
+ shows "\<exists>c. f' \<midarrow>x\<rightarrow> c"
+proof -
+ have holo: "f holomorphic_on A - {x}"
+ using assms by (subst holomorphic_on_open) auto
+
+ define g where "g = (\<lambda>y. if y = x then c else f y)"
+ have deriv_g_eq: "deriv g y = f' y" if "y \<in> A - {x}" for y
+ proof -
+ have ev: "eventually (\<lambda>y. y \<in> A - {x}) (nhds y)"
+ using that assms by (intro eventually_nhds_in_open) auto
+ have "(f has_field_derivative f' y) (at y)"
+ using assms that by auto
+ also have "?this \<longleftrightarrow> (g has_field_derivative f' y) (at y)"
+ by (intro has_field_derivative_cong_ev refl eventually_mono[OF ev]) (auto simp: g_def)
+ finally show ?thesis
+ by (intro DERIV_imp_deriv assms)
+ qed
+
+ have "g holomorphic_on A"
+ unfolding g_def using assms assms(1) holo by (intro removable_singularity) auto
+ hence "deriv g holomorphic_on A"
+ by (intro holomorphic_deriv assms)
+ hence "continuous_on A (deriv g)"
+ by (meson holomorphic_on_imp_continuous_on)
+ hence "(deriv g \<longlongrightarrow> deriv g x) (at x within A)"
+ using assms by (auto simp: continuous_on_def)
+ also have "?this \<longleftrightarrow> (f' \<longlongrightarrow> deriv g x) (at x within A)"
+ by (intro filterlim_cong refl) (auto simp: eventually_at_filter deriv_g_eq)
+ finally have "f' \<midarrow>x\<rightarrow> deriv g x"
+ using \<open>open A\<close> \<open>x \<in> A\<close> by (meson tendsto_within_open)
+ thus ?thesis
+ by blast
+qed
+
+lemma removable_singularity_deriv:
+ assumes "f \<midarrow>x\<rightarrow> c" "isolated_singularity_at f x"
+ shows "\<exists>c. deriv f \<midarrow>x\<rightarrow> c"
+proof -
+ from assms(2) obtain r where r: "r > 0" "f analytic_on ball x r - {x}"
+ by (auto simp: isolated_singularity_at_def)
+ hence holo: "f holomorphic_on ball x r - {x}"
+ using analytic_imp_holomorphic by blast
+ show ?thesis
+ using assms(1)
+ proof (rule removable_singularity_deriv')
+ show "x \<in> ball x r" "open (ball x r)"
+ using \<open>r > 0\<close> by auto
+ qed (auto intro!: holomorphic_derivI[OF holo])
+qed
+
+lemma not_essential_deriv':
+ assumes "not_essential f x" "x \<in> A" "open A"
+ assumes "\<And>y. y \<in> A - {x} \<Longrightarrow> (f has_field_derivative f' y) (at y)"
+ shows "not_essential f' x"
+proof -
+ have holo: "f holomorphic_on A - {x}"
+ using assms by (subst holomorphic_on_open) auto
+ from assms consider "is_pole f x" | c where "f \<midarrow>x\<rightarrow> c"
+ by (auto simp: not_essential_def)
+ thus ?thesis
+ proof cases
+ case 1
+ hence "is_pole f' x"
+ using is_pole_deriv' assms by blast
+ thus ?thesis by (auto simp: not_essential_def)
+ next
+ case (2 c)
+ from 2 have "\<exists>c. f' \<midarrow>x\<rightarrow> c"
+ by (rule removable_singularity_deriv'[OF _ assms(2-4)])
+ thus ?thesis
+ by (auto simp: not_essential_def)
+ qed
+qed
+
+lemma not_essential_deriv[singularity_intros]:
+ assumes "not_essential f x" "isolated_singularity_at f x"
+ shows "not_essential (deriv f) x"
+proof -
+ from assms(2) obtain r where r: "r > 0" "f analytic_on ball x r - {x}"
+ by (auto simp: isolated_singularity_at_def)
+ hence holo: "f holomorphic_on ball x r - {x}"
+ by (subst (asm) analytic_on_open) auto
+ show ?thesis
+ using assms(1)
+ proof (rule not_essential_deriv')
+ show "x \<in> ball x r" "open (ball x r)"
+ using \<open>r > 0\<close> by auto
+ qed (auto intro!: holomorphic_derivI[OF holo])
+qed
+
+lemma not_essential_frequently_0_imp_tendsto_0:
+ fixes f :: "complex \<Rightarrow> complex"
+ assumes sing: "isolated_singularity_at f z" "not_essential f z"
+ assumes freq: "frequently (\<lambda>z. f z = 0) (at z)"
+ shows "f \<midarrow>z\<rightarrow> 0"
+proof -
+ from freq obtain g :: "nat \<Rightarrow> complex" where g: "filterlim g (at z) at_top" "\<And>n. f (g n) = 0"
+ using frequently_atE by blast
+ have "eventually (\<lambda>x. f (g x) = 0) sequentially"
+ using g by auto
+ hence fg: "(\<lambda>x. f (g x)) \<longlonglongrightarrow> 0"
+ by (simp add: tendsto_eventually)
+
+ from assms(2) consider c where "f \<midarrow>z\<rightarrow> c" | "is_pole f z"
+ unfolding not_essential_def by blast
+ thus ?thesis
+ proof cases
+ case (1 c)
+ have "(\<lambda>x. f (g x)) \<longlonglongrightarrow> c"
+ by (rule filterlim_compose[OF 1 g(1)])
+ with fg have "c = 0"
+ using LIMSEQ_unique by blast
+ with 1 show ?thesis by simp
+ next
+ case 2
+ have "filterlim (\<lambda>x. f (g x)) at_infinity sequentially"
+ by (rule filterlim_compose[OF _ g(1)]) (use 2 in \<open>auto simp: is_pole_def\<close>)
+ with fg have False
+ by (meson not_tendsto_and_filterlim_at_infinity sequentially_bot)
+ thus ?thesis ..
+ qed
+qed
+
+lemma not_essential_frequently_0_imp_eventually_0:
+ fixes f :: "complex \<Rightarrow> complex"
+ assumes sing: "isolated_singularity_at f z" "not_essential f z"
+ assumes freq: "frequently (\<lambda>z. f z = 0) (at z)"
+ shows "eventually (\<lambda>z. f z = 0) (at z)"
+proof -
+ from sing obtain r where r: "r > 0" and "f analytic_on ball z r - {z}"
+ by (auto simp: isolated_singularity_at_def)
+ hence holo: "f holomorphic_on ball z r - {z}"
+ by (subst (asm) analytic_on_open) auto
+ have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
+ using r by (intro eventually_at_in_open) auto
+ from freq and this have "frequently (\<lambda>w. f w = 0 \<and> w \<in> ball z r - {z}) (at z)"
+ using frequently_eventually_frequently by blast
+ hence "frequently (\<lambda>w. w \<in> {w\<in>ball z r - {z}. f w = 0}) (at z)"
+ by (simp add: conj_commute)
+ hence limpt: "z islimpt {w\<in>ball z r - {z}. f w = 0}"
+ using islimpt_conv_frequently_at by blast
+
+ define g where "g = (\<lambda>w. if w = z then 0 else f w)"
+ have "f \<midarrow>z\<rightarrow> 0"
+ by (intro not_essential_frequently_0_imp_tendsto_0 assms)
+ hence g_holo: "g holomorphic_on ball z r"
+ unfolding g_def by (intro removable_singularity holo) auto
+
+ have g_eq_0: "g w = 0" if "w \<in> ball z r" for w
+ proof (rule analytic_continuation[where f = g])
+ show "open (ball z r)" "connected (ball z r)"
+ using r by auto
+ show "z islimpt {w\<in>ball z r - {z}. f w = 0}"
+ by fact
+ show "g w = 0" if "w \<in> {w \<in> ball z r - {z}. f w = 0}" for w
+ using that by (auto simp: g_def)
+ qed (use r that g_holo in auto)
+
+ have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
+ using r by (intro eventually_at_in_open) auto
+ thus "eventually (\<lambda>w. f w = 0) (at z)"
+ proof eventually_elim
+ case (elim w)
+ thus ?case using g_eq_0[of w]
+ by (auto simp: g_def)
+ qed
+qed
+
+lemma pole_imp_not_constant:
+ fixes f :: "'a :: {perfect_space} \<Rightarrow> _"
+ assumes "is_pole f x" "open A" "x \<in> A" "A \<subseteq> insert x B"
+ shows "\<not>f constant_on B"
+proof
+ assume *: "f constant_on B"
+ then obtain c where c: "\<forall>x\<in>B. f x = c"
+ by (auto simp: constant_on_def)
+ have "eventually (\<lambda>y. y \<in> A - {x}) (at x)"
+ using assms by (intro eventually_at_in_open) auto
+ hence "eventually (\<lambda>y. f y = c) (at x)"
+ by eventually_elim (use c assms in auto)
+ hence **: "f \<midarrow>x\<rightarrow> c"
+ by (simp add: tendsto_eventually)
+ show False
+ using not_tendsto_and_filterlim_at_infinity[OF _ ** assms(1)[unfolded is_pole_def]] by simp
+qed
+
+
+lemma neg_zorder_imp_is_pole:
+ assumes iso:"isolated_singularity_at f z" and f_ness:"not_essential f z"
+ and "zorder f z < 0" and fre_nz:"\<exists>\<^sub>F w in at z. f w \<noteq> 0 "
+ shows "is_pole f z"
+proof -
+ define P where "P = zor_poly f z"
+ define n where "n = zorder f z"
+ have "n<0" unfolding n_def by (simp add: assms(3))
+ define nn where "nn = nat (-n)"
+
+ obtain r where "P z \<noteq> 0" "r>0" and r_holo:"P holomorphic_on cball z r" and
+ w_Pn:"(\<forall>w\<in>cball z r - {z}. f w = P w * (w - z) powr of_int n \<and> P w \<noteq> 0)"
+ using zorder_exist[OF iso f_ness fre_nz,folded P_def n_def] by auto
+
+ have "is_pole (\<lambda>w. P w * (w - z) powr of_int n) z"
+ unfolding is_pole_def
+ proof (rule tendsto_mult_filterlim_at_infinity)
+ show "P \<midarrow>z\<rightarrow> P z"
+ by (meson open_ball \<open>0 < r\<close> ball_subset_cball centre_in_ball
+ continuous_on_eq_continuous_at continuous_on_subset
+ holomorphic_on_imp_continuous_on isContD r_holo)
+ show "P z\<noteq>0" by (simp add: \<open>P z \<noteq> 0\<close>)
+
+ have "LIM x at z. inverse ((x - z) ^ nat (-n)) :> at_infinity"
+ apply (subst filterlim_inverse_at_iff[symmetric])
+ using \<open>n<0\<close>
+ by (auto intro!:tendsto_eq_intros filterlim_atI
+ simp add:eventually_at_filter)
+ then show "LIM x at z. (x - z) powr of_int n :> at_infinity"
+ proof (elim filterlim_mono_eventually)
+ have "inverse ((x - z) ^ nat (-n)) = (x - z) powr of_int n"
+ if "x\<noteq>z" for x
+ apply (subst powr_of_int)
+ using \<open>n<0\<close> using that by auto
+ then show "\<forall>\<^sub>F x in at z. inverse ((x - z) ^ nat (-n))
+ = (x - z) powr of_int n"
+ by (simp add: eventually_at_filter)
+ qed auto
+ qed
+ moreover have "\<forall>\<^sub>F w in at z. f w = P w * (w - z) powr of_int n"
+ unfolding eventually_at_le
+ apply (rule exI[where x=r])
+ using w_Pn \<open>r>0\<close> by (simp add: dist_commute)
+ ultimately show ?thesis using is_pole_cong by fast
+qed
+
+lemma is_pole_divide_zorder:
+ fixes f g::"complex \<Rightarrow> complex" and z::complex
+ assumes f_iso:"isolated_singularity_at f z" and g_iso:"isolated_singularity_at g z"
+ and f_ness:"not_essential f z" and g_ness:"not_essential g z"
+ and fg_nconst: "\<exists>\<^sub>Fw in (at z). f w * g w\<noteq> 0"
+ and z_less:"zorder f z < zorder g z"
+ shows "is_pole (\<lambda>z. f z / g z) z"
+proof -
+ define fn gn fg where "fn=zorder f z" and "gn=zorder g z"
+ and "fg=(\<lambda>w. f w / g w)"
+
+ have "isolated_singularity_at fg z"
+ unfolding fg_def using f_iso g_iso g_ness
+ by (auto intro:singularity_intros)
+ moreover have "not_essential fg z"
+ unfolding fg_def using f_iso g_iso g_ness f_ness
+ by (auto intro:singularity_intros)
+ moreover have "zorder fg z < 0"
+ proof -
+ have "zorder fg z = fn - gn"
+ using zorder_divide[OF f_iso g_iso f_ness g_ness
+ fg_nconst,folded fn_def gn_def fg_def] .
+ then show ?thesis
+ using z_less by (simp add: fn_def gn_def)
+ qed
+ moreover have "\<exists>\<^sub>F w in at z. fg w \<noteq> 0"
+ using fg_nconst unfolding fg_def by force
+ ultimately show "is_pole fg z"
+ using neg_zorder_imp_is_pole by auto
+qed
+
+lemma isolated_pole_imp_nzero_times:
+ assumes f_iso:"isolated_singularity_at f z"
+ and "is_pole f z"
+ shows "\<exists>\<^sub>Fw in (at z). deriv f w * f w \<noteq> 0"
+proof (rule ccontr)
+ assume "\<not> (\<exists>\<^sub>F w in at z. deriv f w * f w \<noteq> 0)"
+ then have "\<forall>\<^sub>F x in at z. deriv f x * f x = 0"
+ unfolding not_frequently by simp
+ moreover have "\<forall>\<^sub>F w in at z. f w \<noteq> 0"
+ using non_zero_neighbour_pole[OF \<open>is_pole f z\<close>] .
+ moreover have "\<forall>\<^sub>F w in at z. deriv f w \<noteq> 0"
+ using is_pole_deriv[OF \<open>is_pole f z\<close> f_iso,THEN non_zero_neighbour_pole]
+ .
+ ultimately have "\<forall>\<^sub>F w in at z. False"
+ apply eventually_elim
+ by auto
+ then show False by auto
+qed
+
+lemma isolated_pole_imp_neg_zorder:
+ assumes f_iso:"isolated_singularity_at f z"
+ and "is_pole f z"
+ shows "zorder f z<0"
+proof -
+ obtain e where [simp]:"e>0" and f_holo:"f holomorphic_on ball z e - {z}"
+ using f_iso analytic_imp_holomorphic unfolding isolated_singularity_at_def by blast
+ show ?thesis
+ using zorder_exist_pole[OF f_holo,simplified,OF \<open>is_pole f z\<close>]
+ by auto
+qed
+
+lemma isolated_singularity_at_deriv[singularity_intros]:
+ assumes "isolated_singularity_at f x"
+ shows "isolated_singularity_at (deriv f) x"
+proof -
+ obtain r where "r>0" "f analytic_on ball x r - {x}"
+ using assms unfolding isolated_singularity_at_def by auto
+ from analytic_deriv[OF this(2)]
+ have "deriv f analytic_on ball x r - {x}" .
+ with \<open>r>0\<close> show ?thesis
+ unfolding isolated_singularity_at_def by auto
+qed
+
+lemma zorder_deriv_minus_1:
+ fixes f g::"complex \<Rightarrow> complex" and z::complex
+ assumes f_iso:"isolated_singularity_at f z"
+ and f_ness:"not_essential f z"
+ and f_nconst:"\<exists>\<^sub>F w in at z. f w \<noteq> 0"
+ and f_ord:"zorder f z \<noteq>0"
+ shows "zorder (deriv f) z = zorder f z - 1"
+proof -
+ define P where "P = zor_poly f z"
+ define n where "n = zorder f z"
+ have "n\<noteq>0" unfolding n_def using f_ord by auto
+
+ obtain r where "P z \<noteq> 0" "r>0" and P_holo:"P holomorphic_on cball z r"
+ and "(\<forall>w\<in>cball z r - {z}. f w
+ = P w * (w - z) powr of_int n \<and> P w \<noteq> 0)"
+ using zorder_exist[OF f_iso f_ness f_nconst,folded P_def n_def] by auto
+ from this(4)
+ have f_eq:"(\<forall>w\<in>cball z r - {z}. f w
+ = P w * (w - z) powi n \<and> P w \<noteq> 0)"
+ using complex_powr_of_int f_ord n_def by presburger
+
+ define D where "D = (\<lambda>w. (deriv P w * (w - z) + of_int n * P w)
+ * (w - z) powi (n - 1))"
+
+ have deriv_f_eq:"deriv f w = D w" if "w \<in> ball z r - {z}" for w
+ proof -
+ have ev': "eventually (\<lambda>w. w \<in> ball z r - {z}) (nhds w)"
+ using that by (intro eventually_nhds_in_open) auto
+
+ define wz where "wz = w - z"
+
+ have "wz \<noteq>0" unfolding wz_def using that by auto
+ moreover have "(P has_field_derivative deriv P w) (at w)"
+ by (meson DiffD1 Elementary_Metric_Spaces.open_ball P_holo
+ ball_subset_cball holomorphic_derivI holomorphic_on_subset that)
+ ultimately have "((\<lambda>w. P w * (w - z) powi n) has_field_derivative D w) (at w)"
+ unfolding D_def using that
+ apply (auto intro!: derivative_eq_intros)
+ apply (fold wz_def)
+ by (auto simp:algebra_simps simp flip:power_int_add_1')
+ also have "?this \<longleftrightarrow> (f has_field_derivative D w) (at w)"
+ using f_eq
+ by (intro has_field_derivative_cong_ev refl eventually_mono[OF ev']) auto
+ ultimately have "(f has_field_derivative D w) (at w)" by simp
+ moreover have "(f has_field_derivative deriv f w) (at w)"
+ by (metis DERIV_imp_deriv calculation)
+ ultimately show ?thesis using DERIV_imp_deriv by blast
+ qed
+
+ show "zorder (deriv f) z = n - 1"
+ proof (rule zorder_eqI)
+ show "open (ball z r)" "z \<in> ball z r"
+ using \<open>r > 0\<close> by auto
+ define g where "g=(\<lambda>w. (deriv P w * (w - z) + of_int n * P w))"
+ show "g holomorphic_on ball z r"
+ unfolding g_def using P_holo
+ by (auto intro!:holomorphic_intros)
+ show "g z \<noteq> 0"
+ unfolding g_def using \<open>P z \<noteq> 0\<close> \<open>n\<noteq>0\<close> by auto
+ show "deriv f w =
+ (deriv P w * (w - z) + of_int n * P w) * (w - z) powr of_int (n - 1)"
+ if "w \<in> ball z r" "w \<noteq> z" for w
+ apply (subst complex_powr_of_int)
+ using deriv_f_eq that unfolding D_def by auto
+ qed
+qed
+
+
+lemma deriv_divide_is_pole: \<comment>\<open>Generalises @{thm zorder_deriv}\<close>
+ fixes f g::"complex \<Rightarrow> complex" and z::complex
+ assumes f_iso:"isolated_singularity_at f z"
+ and f_ness:"not_essential f z"
+ and fg_nconst: "\<exists>\<^sub>Fw in (at z). deriv f w * f w \<noteq> 0"
+ and f_ord:"zorder f z \<noteq>0"
+ shows "is_pole (\<lambda>z. deriv f z / f z) z"
+proof (rule neg_zorder_imp_is_pole)
+ define ff where "ff=(\<lambda>w. deriv f w / f w)"
+ show "isolated_singularity_at ff z"
+ using f_iso f_ness unfolding ff_def
+ by (auto intro:singularity_intros)
+ show "not_essential ff z"
+ unfolding ff_def using f_ness f_iso
+ by (auto intro:singularity_intros)
+
+ have "zorder ff z = zorder (deriv f) z - zorder f z"
+ unfolding ff_def using f_iso f_ness fg_nconst
+ apply (rule_tac zorder_divide)
+ by (auto intro:singularity_intros)
+ moreover have "zorder (deriv f) z = zorder f z - 1"
+ proof (rule zorder_deriv_minus_1)
+ show " \<exists>\<^sub>F w in at z. f w \<noteq> 0"
+ using fg_nconst frequently_elim1 by fastforce
+ qed (use f_iso f_ness f_ord in auto)
+ ultimately show "zorder ff z < 0" by auto
+
+ show "\<exists>\<^sub>F w in at z. ff w \<noteq> 0"
+ unfolding ff_def using fg_nconst by auto
+qed
+
+lemma is_pole_deriv_divide_is_pole:
+ fixes f g::"complex \<Rightarrow> complex" and z::complex
+ assumes f_iso:"isolated_singularity_at f z"
+ and "is_pole f z"
+ shows "is_pole (\<lambda>z. deriv f z / f z) z"
+proof (rule deriv_divide_is_pole[OF f_iso])
+ show "not_essential f z"
+ using \<open>is_pole f z\<close> unfolding not_essential_def by auto
+ show "\<exists>\<^sub>F w in at z. deriv f w * f w \<noteq> 0"
+ apply (rule isolated_pole_imp_nzero_times)
+ using assms by auto
+ show "zorder f z \<noteq> 0"
+ using isolated_pole_imp_neg_zorder assms by fastforce
+qed
+
+subsection \<open>Isolated zeroes\<close>
+
+definition isolated_zero :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> bool" where
+ "isolated_zero f z \<longleftrightarrow> f z = 0 \<and> eventually (\<lambda>z. f z \<noteq> 0) (at z)"
+
+lemma isolated_zero_altdef: "isolated_zero f z \<longleftrightarrow> f z = 0 \<and> \<not>z islimpt {z. f z = 0}"
+ unfolding isolated_zero_def eventually_at_filter eventually_nhds islimpt_def by blast
+
+lemma isolated_zero_mult1:
+ assumes "isolated_zero f x" "isolated_zero g x"
+ shows "isolated_zero (\<lambda>x. f x * g x) x"
+proof -
+ have "eventually (\<lambda>x. f x \<noteq> 0) (at x)" "eventually (\<lambda>x. g x \<noteq> 0) (at x)"
+ using assms unfolding isolated_zero_def by auto
+ hence "eventually (\<lambda>x. f x * g x \<noteq> 0) (at x)"
+ by eventually_elim auto
+ with assms show ?thesis
+ by (auto simp: isolated_zero_def)
+qed
+
+lemma isolated_zero_mult2:
+ assumes "isolated_zero f x" "g x \<noteq> 0" "g analytic_on {x}"
+ shows "isolated_zero (\<lambda>x. f x * g x) x"
+proof -
+ have "eventually (\<lambda>x. f x \<noteq> 0) (at x)"
+ using assms unfolding isolated_zero_def by auto
+ moreover have "eventually (\<lambda>x. g x \<noteq> 0) (at x)"
+ using analytic_at_neq_imp_eventually_neq[of g x 0] assms by auto
+ ultimately have "eventually (\<lambda>x. f x * g x \<noteq> 0) (at x)"
+ by eventually_elim auto
+ thus ?thesis
+ using assms(1) by (auto simp: isolated_zero_def)
+qed
+
+lemma isolated_zero_mult3:
+ assumes "isolated_zero f x" "g x \<noteq> 0" "g analytic_on {x}"
+ shows "isolated_zero (\<lambda>x. g x * f x) x"
+ using isolated_zero_mult2[OF assms] by (simp add: mult_ac)
+
+lemma isolated_zero_prod:
+ assumes "\<And>x. x \<in> I \<Longrightarrow> isolated_zero (f x) z" "I \<noteq> {}" "finite I"
+ shows "isolated_zero (\<lambda>y. \<Prod>x\<in>I. f x y) z"
+ using assms(3,2,1) by (induction rule: finite_ne_induct) (auto intro: isolated_zero_mult1)
+
+lemma non_isolated_zero':
+ assumes "isolated_singularity_at f z" "not_essential f z" "f z = 0" "\<not>isolated_zero f z"
+ shows "eventually (\<lambda>z. f z = 0) (at z)"
+proof (rule not_essential_frequently_0_imp_eventually_0)
+ from assms show "frequently (\<lambda>z. f z = 0) (at z)"
+ by (auto simp: frequently_def isolated_zero_def)
+qed fact+
+
+lemma non_isolated_zero:
+ assumes "\<not>isolated_zero f z" "f analytic_on {z}" "f z = 0"
+ shows "eventually (\<lambda>z. f z = 0) (nhds z)"
+proof -
+ have "eventually (\<lambda>z. f z = 0) (at z)"
+ by (rule non_isolated_zero')
+ (use assms in \<open>auto intro: not_essential_analytic isolated_singularity_at_analytic\<close>)
+ with \<open>f z = 0\<close> show ?thesis
+ unfolding eventually_at_filter by (auto elim!: eventually_mono)
+qed
+
+lemma not_essential_compose:
+ assumes "not_essential f (g z)" "g analytic_on {z}"
+ shows "not_essential (\<lambda>x. f (g x)) z"
+proof (cases "isolated_zero (\<lambda>w. g w - g z) z")
+ case False
+ hence "eventually (\<lambda>w. g w - g z = 0) (nhds z)"
+ by (rule non_isolated_zero) (use assms in \<open>auto intro!: analytic_intros\<close>)
+ hence "not_essential (\<lambda>x. f (g x)) z \<longleftrightarrow> not_essential (\<lambda>_. f (g z)) z"
+ by (intro not_essential_cong refl)
+ (auto elim!: eventually_mono simp: eventually_at_filter)
+ thus ?thesis
+ by (simp add: not_essential_const)
+next
+ case True
+ hence ev: "eventually (\<lambda>w. g w \<noteq> g z) (at z)"
+ by (auto simp: isolated_zero_def)
+ from assms consider c where "f \<midarrow>g z\<rightarrow> c" | "is_pole f (g z)"
+ by (auto simp: not_essential_def)
+ have "isCont g z"
+ by (rule analytic_at_imp_isCont) fact
+ hence lim: "g \<midarrow>z\<rightarrow> g z"
+ using isContD by blast
+
+ from assms(1) consider c where "f \<midarrow>g z\<rightarrow> c" | "is_pole f (g z)"
+ unfolding not_essential_def by blast
+ thus ?thesis
+ proof cases
+ fix c assume "f \<midarrow>g z\<rightarrow> c"
+ hence "(\<lambda>x. f (g x)) \<midarrow>z\<rightarrow> c"
+ by (rule filterlim_compose) (use lim ev in \<open>auto simp: filterlim_at\<close>)
+ thus ?thesis
+ by (auto simp: not_essential_def)
+ next
+ assume "is_pole f (g z)"
+ hence "is_pole (\<lambda>x. f (g x)) z"
+ by (rule is_pole_compose) fact+
+ thus ?thesis
+ by (auto simp: not_essential_def)
+ qed
+qed
+
+subsection \<open>Isolated points\<close>
+
+definition isolated_points_of :: "complex set \<Rightarrow> complex set" where
+ "isolated_points_of A = {z\<in>A. eventually (\<lambda>w. w \<notin> A) (at z)}"
+
+lemma isolated_points_of_altdef: "isolated_points_of A = {z\<in>A. \<not>z islimpt A}"
+ unfolding isolated_points_of_def islimpt_def eventually_at_filter eventually_nhds by blast
+
+lemma isolated_points_of_empty [simp]: "isolated_points_of {} = {}"
+ and isolated_points_of_UNIV [simp]: "isolated_points_of UNIV = {}"
+ by (auto simp: isolated_points_of_def)
+
+lemma isolated_points_of_open_is_empty [simp]: "open A \<Longrightarrow> isolated_points_of A = {}"
+ unfolding isolated_points_of_altdef
+ by (simp add: interior_limit_point interior_open)
+
+lemma isolated_points_of_subset: "isolated_points_of A \<subseteq> A"
+ by (auto simp: isolated_points_of_def)
+
+lemma isolated_points_of_discrete:
+ assumes "discrete A"
+ shows "isolated_points_of A = A"
+ using assms by (auto simp: isolated_points_of_def discrete_altdef)
+
+lemmas uniform_discreteI1 = uniformI1
+lemmas uniform_discreteI2 = uniformI2
+
+lemma isolated_singularity_at_compose:
+ assumes "isolated_singularity_at f (g z)" "g analytic_on {z}"
+ shows "isolated_singularity_at (\<lambda>x. f (g x)) z"
+proof (cases "isolated_zero (\<lambda>w. g w - g z) z")
+ case False
+ hence "eventually (\<lambda>w. g w - g z = 0) (nhds z)"
+ by (rule non_isolated_zero) (use assms in \<open>auto intro!: analytic_intros\<close>)
+ hence "isolated_singularity_at (\<lambda>x. f (g x)) z \<longleftrightarrow> isolated_singularity_at (\<lambda>_. f (g z)) z"
+ by (intro isolated_singularity_at_cong refl)
+ (auto elim!: eventually_mono simp: eventually_at_filter)
+ thus ?thesis
+ by (simp add: isolated_singularity_at_const)
+next
+ case True
+ from assms(1) obtain r where r: "r > 0" "f analytic_on ball (g z) r - {g z}"
+ by (auto simp: isolated_singularity_at_def)
+ hence holo_f: "f holomorphic_on ball (g z) r - {g z}"
+ by (subst (asm) analytic_on_open) auto
+ from assms(2) obtain r' where r': "r' > 0" "g holomorphic_on ball z r'"
+ by (auto simp: analytic_on_def)
+
+ have "continuous_on (ball z r') g"
+ using holomorphic_on_imp_continuous_on r' by blast
+ hence "isCont g z"
+ using r' by (subst (asm) continuous_on_eq_continuous_at) auto
+ hence "g \<midarrow>z\<rightarrow> g z"
+ using isContD by blast
+ hence "eventually (\<lambda>w. g w \<in> ball (g z) r) (at z)"
+ using \<open>r > 0\<close> unfolding tendsto_def by force
+ moreover have "eventually (\<lambda>w. g w \<noteq> g z) (at z)" using True
+ by (auto simp: isolated_zero_def elim!: eventually_mono)
+ ultimately have "eventually (\<lambda>w. g w \<in> ball (g z) r - {g z}) (at z)"
+ by eventually_elim auto
+ then obtain r'' where r'': "r'' > 0" "\<forall>w\<in>ball z r''-{z}. g w \<in> ball (g z) r - {g z}"
+ unfolding eventually_at_filter eventually_nhds_metric ball_def
+ by (auto simp: dist_commute)
+ have "f \<circ> g holomorphic_on ball z (min r' r'') - {z}"
+ proof (rule holomorphic_on_compose_gen)
+ show "g holomorphic_on ball z (min r' r'') - {z}"
+ by (rule holomorphic_on_subset[OF r'(2)]) auto
+ show "f holomorphic_on ball (g z) r - {g z}"
+ by fact
+ show "g ` (ball z (min r' r'') - {z}) \<subseteq> ball (g z) r - {g z}"
+ using r'' by force
+ qed
+ hence "f \<circ> g analytic_on ball z (min r' r'') - {z}"
+ by (subst analytic_on_open) auto
+ thus ?thesis using \<open>r' > 0\<close> \<open>r'' > 0\<close>
+ by (auto simp: isolated_singularity_at_def o_def intro!: exI[of _ "min r' r''"])
+qed
+
+lemma is_pole_power_int_0:
+ assumes "f analytic_on {x}" "isolated_zero f x" "n < 0"
+ shows "is_pole (\<lambda>x. f x powi n) x"
+proof -
+ have "f \<midarrow>x\<rightarrow> f x"
+ using assms(1) by (simp add: analytic_at_imp_isCont isContD)
+ with assms show ?thesis
+ unfolding is_pole_def
+ by (intro filterlim_power_int_neg_at_infinity) (auto simp: isolated_zero_def)
+qed
+
+lemma isolated_zero_imp_not_constant_on:
+ assumes "isolated_zero f x" "x \<in> A" "open A"
+ shows "\<not>f constant_on A"
+proof
+ assume "f constant_on A"
+ then obtain c where c: "\<And>x. x \<in> A \<Longrightarrow> f x = c"
+ by (auto simp: constant_on_def)
+ from assms and c[of x] have [simp]: "c = 0"
+ by (auto simp: isolated_zero_def)
+ have "eventually (\<lambda>x. f x \<noteq> 0) (at x)"
+ using assms by (auto simp: isolated_zero_def)
+ moreover have "eventually (\<lambda>x. x \<in> A) (at x)"
+ using assms by (intro eventually_at_in_open') auto
+ ultimately have "eventually (\<lambda>x. False) (at x)"
+ by eventually_elim (use c in auto)
+ thus False
+ by simp
+qed
+
+end
--- a/src/HOL/Complex_Analysis/Conformal_Mappings.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Complex_Analysis/Conformal_Mappings.thy Sun Feb 12 21:11:57 2023 +0100
@@ -1079,7 +1079,7 @@
qed
qed
-text\<open>Hence a nice clean inverse function theorem\<close>
+subsubsection \<open>Hence a nice clean inverse function theorem\<close>
lemma has_field_derivative_inverse_strong:
fixes f :: "'a::{euclidean_space,real_normed_field} \<Rightarrow> 'a"
@@ -1140,6 +1140,78 @@
qed
qed
+subsubsection \<open> Holomorphism of covering maps and lifts.\<close>
+
+lemma covering_space_lift_is_holomorphic:
+ assumes cov: "covering_space C p S"
+ and C: "open C" "p holomorphic_on C"
+ and holf: "f holomorphic_on U" and fim: "f ` U \<subseteq> S" and gim: "g ` U \<subseteq> C"
+ and contg: "continuous_on U g" and pg_f: "\<And>x. x \<in> U \<Longrightarrow> p(g x) = f x"
+ shows "g holomorphic_on U"
+ unfolding holomorphic_on_def
+proof (intro strip)
+ fix z
+ assume "z \<in> U"
+ with fim have "f z \<in> S" by blast
+ then obtain T \<V> where "f z \<in> T" and opeT: "openin (top_of_set S) T"
+ and UV: "\<Union>\<V> = C \<inter> p -` T"
+ and "\<And>W. W \<in> \<V> \<Longrightarrow> openin (top_of_set C) W"
+ and disV: "pairwise disjnt \<V>" and homeV: "\<And>W. W \<in> \<V> \<Longrightarrow> \<exists>q. homeomorphism W T p q"
+ using cov fim unfolding covering_space_def by meson
+ then have "\<And>W. W \<in> \<V> \<Longrightarrow> open W \<and> W \<subseteq> C"
+ by (metis \<open>open C\<close> inf_le1 open_Int openin_open)
+ then obtain V where "V \<in> \<V>" "g z \<in> V" "open V" "V \<subseteq> C"
+ by (metis IntI UnionE image_subset_iff vimageI UV \<open>f z \<in> T\<close> \<open>z \<in> U\<close> gim pg_f)
+ have holp: "p holomorphic_on V"
+ using \<open>V \<subseteq> C\<close> \<open>p holomorphic_on C\<close> holomorphic_on_subset by blast
+ moreover have injp: "inj_on p V"
+ by (metis \<open>V \<in> \<V>\<close> homeV homeomorphism_def inj_on_inverseI)
+ ultimately
+ obtain p' where holp': "p' holomorphic_on (p ` V)" and pp': "\<And>z. z \<in> V \<Longrightarrow> p'(p z) = z"
+ using \<open>open V\<close> holomorphic_has_inverse by metis
+ have "z \<in> U \<inter> g -` V"
+ using \<open>g z \<in> V\<close> \<open>z \<in> U\<close> by blast
+ moreover have "openin (top_of_set U) (U \<inter> g -` V)"
+ using continuous_openin_preimage [OF contg gim]
+ by (meson \<open>open V\<close> contg continuous_openin_preimage_eq)
+ ultimately obtain \<epsilon> where "\<epsilon>>0" and e: "ball z \<epsilon> \<inter> U \<subseteq> g -` V"
+ by (force simp add: openin_contains_ball)
+ show "g field_differentiable at z within U"
+ proof (rule field_differentiable_transform_within)
+ show "(0::real) < \<epsilon>"
+ by (simp add: \<open>0 < \<epsilon>\<close>)
+ show "z \<in> U"
+ by (simp add: \<open>z \<in> U\<close>)
+ show "(p' o f) x' = g x'" if "x' \<in> U" "dist x' z < \<epsilon>" for x'
+ using that
+ by (metis Int_iff comp_apply dist_commute e mem_ball pg_f pp' subsetD vimage_eq)
+ have "open (p ` V)"
+ using \<open>open V\<close> holp injp open_mapping_thm3 by force
+ moreover have "f z \<in> p ` V"
+ by (metis \<open>z \<in> U\<close> image_iff pg_f \<open>g z \<in> V\<close>)
+ ultimately have "p' field_differentiable at (f z)"
+ using holomorphic_on_imp_differentiable_at holp' by blast
+ moreover have "f field_differentiable at z within U"
+ by (metis (no_types) \<open>z \<in> U\<close> holf holomorphic_on_def)
+ ultimately show "(p' o f) field_differentiable at z within U"
+ by (metis (no_types) field_differentiable_at_within field_differentiable_compose_within)
+ qed
+qed
+
+lemma covering_space_lift_holomorphic:
+ assumes cov: "covering_space C p S"
+ and C: "open C" "p holomorphic_on C"
+ and f: "f holomorphic_on U" "f ` U \<subseteq> S"
+ and U: "simply_connected U" "locally path_connected U"
+ obtains g where "g holomorphic_on U" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
+proof -
+ obtain g where "continuous_on U g" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
+ using covering_space_lift [OF cov U]
+ using f holomorphic_on_imp_continuous_on by blast
+ then show ?thesis
+ by (metis C cov covering_space_lift_is_holomorphic f that)
+qed
+
subsection\<open>The Schwarz Lemma\<close>
lemma Schwarz1:
@@ -1923,8 +1995,7 @@
qed
show ?thesis
apply (rule Bloch_unit [OF 1 2])
- apply (rule_tac b="(C * of_real r) * b" in that)
- using image_mono sb1 sb2 by fastforce
+ using image_mono sb1 sb2 that by fastforce
qed
corollary Bloch_general:
@@ -1954,10 +2025,7 @@
then have 1: "f holomorphic_on ball a t"
using holf using holomorphic_on_subset by blast
show ?thesis
- apply (rule Bloch [OF 1 \<open>t > 0\<close> rle])
- apply (rule_tac b=b in that)
- using * apply force
- done
+ using Bloch [OF 1 \<open>t > 0\<close> rle] * by (metis image_mono order_trans that)
qed
qed
qed
--- a/src/HOL/Complex_Analysis/Contour_Integration.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Complex_Analysis/Contour_Integration.thy Sun Feb 12 21:11:57 2023 +0100
@@ -94,8 +94,6 @@
subsection\<^marker>\<open>tag unimportant\<close> \<open>Reversing a path\<close>
-
-
lemma has_contour_integral_reversepath:
assumes "valid_path g" and f: "(f has_contour_integral i) g"
shows "(f has_contour_integral (-i)) (reversepath g)"
@@ -807,9 +805,8 @@
lemma contour_integral_const_linepath [simp]: "contour_integral (linepath a b) (\<lambda>x. c) = c*(b - a)"
by (rule contour_integral_unique [OF has_contour_integral_const_linepath])
-lemma contour_integral_neg:
- "f contour_integrable_on g \<Longrightarrow> contour_integral g (\<lambda>x. -(f x)) = -(contour_integral g f)"
- by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_neg)
+lemma contour_integral_neg: "contour_integral g (\<lambda>z. -f z) = -contour_integral g f"
+ by (simp add: contour_integral_integral)
lemma contour_integral_add:
"f1 contour_integrable_on g \<Longrightarrow> f2 contour_integrable_on g \<Longrightarrow> contour_integral g (\<lambda>x. f1 x + f2 x) =
@@ -903,6 +900,19 @@
unfolding contour_integrable_on_def
by (metis has_contour_integral_sum)
+lemma contour_integrable_lmul_iff:
+ "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c * f x) contour_integrable_on g \<longleftrightarrow> f contour_integrable_on g"
+ using contour_integrable_lmul[of f g c] contour_integrable_lmul[of "\<lambda>x. c * f x" g "inverse c"]
+ by (auto simp: field_simps)
+
+lemma contour_integrable_rmul_iff:
+ "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x * c) contour_integrable_on g \<longleftrightarrow> f contour_integrable_on g"
+ using contour_integrable_rmul[of f g c] contour_integrable_rmul[of "\<lambda>x. c * f x" g "inverse c"]
+ by (auto simp: field_simps)
+
+lemma contour_integrable_div_iff:
+ "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / c) contour_integrable_on g \<longleftrightarrow> f contour_integrable_on g"
+ using contour_integrable_rmul_iff[of "inverse c"] by (simp add: field_simps)
subsection\<^marker>\<open>tag unimportant\<close> \<open>Reversing a path integral\<close>
@@ -912,9 +922,9 @@
using has_contour_integral_reversepath valid_path_linepath by fastforce
lemma contour_integral_reverse_linepath:
- "continuous_on (closed_segment a b) f
- \<Longrightarrow> contour_integral (linepath a b) f = - (contour_integral(linepath b a) f)"
- by (metis contour_integrable_continuous_linepath contour_integral_unique has_contour_integral_integral has_contour_integral_reverse_linepath)
+ "continuous_on (closed_segment a b) f \<Longrightarrow> contour_integral (linepath a b) f = - (contour_integral(linepath b a) f)"
+ using contour_integral_reversepath by fastforce
+
text \<open>Splitting a path integral in a flat way.*)\<close>
--- a/src/HOL/Complex_Analysis/Residue_Theorem.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Complex_Analysis/Residue_Theorem.thy Sun Feb 12 21:11:57 2023 +0100
@@ -454,9 +454,8 @@
theorem argument_principle:
fixes f::"complex \<Rightarrow> complex" and poles s:: "complex set"
- defines "pz \<equiv> {w. f w = 0 \<or> w \<in> poles}" \<comment> \<open>\<^term>\<open>pz\<close> is the set of poles and zeros\<close>
- assumes "open s" and
- "connected s" and
+ defines "pz \<equiv> {w\<in>s. f w = 0 \<or> w \<in> poles}" \<comment> \<open>\<^term>\<open>pz\<close> is the set of poles and zeros\<close>
+ assumes "open s" "connected s" and
f_holo:"f holomorphic_on s-poles" and
h_holo:"h holomorphic_on s" and
"valid_path g" and
@@ -464,7 +463,7 @@
path_img:"path_image g \<subseteq> s - pz" and
homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number g z = 0" and
finite:"finite pz" and
- poles:"\<forall>p\<in>poles. is_pole f p"
+ poles:"\<forall>p\<in>s\<inter>poles. is_pole f p"
shows "contour_integral g (\<lambda>x. deriv f x * h x / f x) = 2 * pi * \<i> *
(\<Sum>p\<in>pz. winding_number g p * h p * zorder f p)"
(is "?L=?R")
@@ -505,10 +504,12 @@
case False
then have "p\<in>s-poles" using \<open>p\<in>s\<close> poles unfolding pz_def by auto
moreover have "open (s-poles)"
- using \<open>open s\<close>
- apply (elim open_Diff)
- apply (rule finite_imp_closed)
- using finite unfolding pz_def by simp
+ proof -
+ have "closed (s \<inter> poles)"
+ using finite by (simp add: pz_def finite_imp_closed rev_finite_subset subset_eq)
+ then show ?thesis
+ by (metis Diff_Compl Diff_Diff_Int Diff_eq \<open>open s\<close> open_Diff)
+ qed
ultimately have "isCont f p"
using holomorphic_on_imp_continuous_on[OF f_holo] continuous_on_eq_continuous_at
by auto
@@ -518,13 +519,21 @@
proof (rule ccontr)
assume "\<not> (\<exists>\<^sub>F w in at p. f w \<noteq> 0)"
then have "\<forall>\<^sub>F w in at p. f w= 0" unfolding frequently_def by auto
- then obtain rr where "rr>0" "\<forall>w\<in>ball p rr - {p}. f w =0"
+ then obtain r1 where "r1>0" and r1:"\<forall>w\<in>ball p r1 - {p}. f w =0"
unfolding eventually_at by (auto simp add:dist_commute)
- then have "ball p rr - {p} \<subseteq> {w\<in>ball p rr-{p}. f w=0}" by blast
- moreover have "infinite (ball p rr - {p})" using \<open>rr>0\<close> using finite_imp_not_open by fastforce
- ultimately have "infinite {w\<in>ball p rr-{p}. f w=0}" using infinite_super by blast
+ obtain r2 where "r2>0" and r2: "ball p r2 \<subseteq> s"
+ using \<open>p\<in>s\<close> \<open>open s\<close> openE by blast
+ define rr where "rr=min r1 r2"
+
+ from r1 r2
+ have "ball p rr - {p} \<subseteq> {w\<in> s \<inter> ball p rr-{p}. f w=0}"
+ unfolding rr_def by auto
+ moreover have "infinite (ball p rr - {p})"
+ using \<open>r1>0\<close> \<open>r2>0\<close> finite_imp_not_open
+ unfolding rr_def by fastforce
+ ultimately have "infinite {w\<in>s \<inter> ball p rr-{p}. f w=0}" using infinite_super by blast
then have "infinite pz"
- unfolding pz_def infinite_super by auto
+ unfolding pz_def by (smt (verit) infinite_super Collect_mono_iff DiffE Int_iff)
then show False using \<open>finite pz\<close> by auto
qed
ultimately obtain r where "pp p \<noteq> 0" and r:"r>0" "pp holomorphic_on cball p r"
@@ -795,7 +804,7 @@
theorem Rouche_theorem:
fixes f g::"complex \<Rightarrow> complex" and s:: "complex set"
defines "fg\<equiv>(\<lambda>p. f p + g p)"
- defines "zeros_fg\<equiv>{p. fg p = 0}" and "zeros_f\<equiv>{p. f p = 0}"
+ defines "zeros_fg\<equiv>{p\<in>s. fg p = 0}" and "zeros_f\<equiv>{p\<in>s. f p = 0}"
assumes
"open s" and "connected s" and
"finite zeros_fg" and
@@ -844,9 +853,8 @@
proof -
have "h p \<in> ball 1 1" when "p\<in>path_image \<gamma>" for p
proof -
- have "cmod (g p/f p) <1" using path_less[rule_format,OF that]
- apply (cases "cmod (f p) = 0")
- by (auto simp add: norm_divide)
+ have "cmod (g p/f p) <1"
+ by (smt (verit) divide_less_eq_1_pos norm_divide norm_ge_zero path_less that)
then show ?thesis unfolding h_def by (auto simp add:dist_complex_def)
qed
then have "path_image (h o \<gamma>) \<subseteq> ball 1 1"
@@ -935,9 +943,8 @@
assume "\<not> h p \<noteq> 0"
then have "g p / f p= -1" unfolding h_def by (simp add: add_eq_0_iff2)
then have "cmod (g p/f p) = 1" by auto
- moreover have "cmod (g p/f p) <1" using path_less[rule_format,OF that]
- apply (cases "cmod (f p) = 0")
- by (auto simp add: norm_divide)
+ moreover have "cmod (g p/f p) <1"
+ by (simp add: \<open>f p \<noteq> 0\<close> norm_divide path_less that)
ultimately show False by auto
qed
have der_fg:"deriv fg p = deriv f p + deriv g p" unfolding fg_def
@@ -963,20 +970,24 @@
ultimately show ?thesis by auto
qed
moreover have "contour_integral \<gamma> (\<lambda>x. deriv fg x / fg x) = c * (\<Sum>p\<in>zeros_fg. w p * zorder fg p)"
- unfolding c_def zeros_fg_def w_def
- proof (rule argument_principle[OF \<open>open s\<close> \<open>connected s\<close> _ _ \<open>valid_path \<gamma>\<close> loop _ homo
- , of _ "{}" "\<lambda>_. 1",simplified])
- show "fg holomorphic_on s" unfolding fg_def using f_holo g_holo holomorphic_on_add by auto
- show "path_image \<gamma> \<subseteq> s - {p. fg p = 0}" using path_fg unfolding zeros_fg_def .
- show " finite {p. fg p = 0}" using \<open>finite zeros_fg\<close> unfolding zeros_fg_def .
+ proof -
+ have "fg holomorphic_on s" unfolding fg_def using f_holo g_holo holomorphic_on_add by auto
+ moreover
+ have "path_image \<gamma> \<subseteq> s - {p\<in>s. fg p = 0}" using path_fg unfolding zeros_fg_def .
+ moreover
+ have " finite {p\<in>s. fg p = 0}" using \<open>finite zeros_fg\<close> unfolding zeros_fg_def .
+ ultimately show ?thesis
+ unfolding c_def zeros_fg_def w_def
+ using argument_principle[OF \<open>open s\<close> \<open>connected s\<close> _ _ \<open>valid_path \<gamma>\<close> loop _ homo, of _ "{}" "\<lambda>_. 1"]
+ by simp
qed
moreover have "contour_integral \<gamma> (\<lambda>x. deriv f x / f x) = c * (\<Sum>p\<in>zeros_f. w p * zorder f p)"
unfolding c_def zeros_f_def w_def
proof (rule argument_principle[OF \<open>open s\<close> \<open>connected s\<close> _ _ \<open>valid_path \<gamma>\<close> loop _ homo
, of _ "{}" "\<lambda>_. 1",simplified])
show "f holomorphic_on s" using f_holo g_holo holomorphic_on_add by auto
- show "path_image \<gamma> \<subseteq> s - {p. f p = 0}" using path_f unfolding zeros_f_def .
- show " finite {p. f p = 0}" using \<open>finite zeros_f\<close> unfolding zeros_f_def .
+ show "path_image \<gamma> \<subseteq> s - {p\<in>s. f p = 0}" using path_f unfolding zeros_f_def .
+ show " finite {p\<in>s. f p = 0}" using \<open>finite zeros_f\<close> unfolding zeros_f_def .
qed
ultimately have " c* (\<Sum>p\<in>zeros_fg. w p * (zorder fg p)) = c* (\<Sum>p\<in>zeros_f. w p * (zorder f p))"
by auto
--- a/src/HOL/Data_Structures/Map_Specs.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Data_Structures/Map_Specs.thy Sun Feb 12 21:11:57 2023 +0100
@@ -6,7 +6,7 @@
imports AList_Upd_Del
begin
-text \<open>The basic map interface with traditional \<open>set\<close>-based specification:\<close>
+text \<open>The basic map interface with @{typ "'a \<Rightarrow> 'b option"} based specification:\<close>
locale Map =
fixes empty :: "'m"
--- a/src/HOL/Filter.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Filter.thy Sun Feb 12 21:11:57 2023 +0100
@@ -223,6 +223,16 @@
shows "\<exists>\<^sub>Fx in F. Q x \<and> P x"
using assms eventually_elim2 by (force simp add: frequently_def)
+lemma frequently_cong:
+ assumes ev: "eventually P F" and QR: "\<And>x. P x \<Longrightarrow> Q x \<longleftrightarrow> R x"
+ shows "frequently Q F \<longleftrightarrow> frequently R F"
+ unfolding frequently_def
+ using QR by (auto intro!: eventually_cong [OF ev])
+
+lemma frequently_eventually_frequently:
+ "frequently P F \<Longrightarrow> eventually Q F \<Longrightarrow> frequently (\<lambda>x. P x \<and> Q x) F"
+ using frequently_cong [of Q F P "\<lambda>x. P x \<and> Q x"] by meson
+
lemma eventually_frequently_const_simps:
"(\<exists>\<^sub>Fx in F. P x \<and> C) \<longleftrightarrow> (\<exists>\<^sub>Fx in F. P x) \<and> C"
"(\<exists>\<^sub>Fx in F. C \<and> P x) \<longleftrightarrow> C \<and> (\<exists>\<^sub>Fx in F. P x)"
@@ -606,12 +616,6 @@
lemma filtermap_INF: "filtermap f (\<Sqinter>b\<in>B. F b) \<le> (\<Sqinter>b\<in>B. filtermap f (F b))"
by (rule INF_greatest, rule filtermap_mono, erule INF_lower)
-lemma frequently_cong:
- assumes ev: "eventually P F" and QR: "\<And>x. P x \<Longrightarrow> Q x \<longleftrightarrow> R x"
- shows "frequently Q F \<longleftrightarrow> frequently R F"
- unfolding frequently_def
- using QR by (auto intro!: eventually_cong [OF ev])
-
lemma frequently_filtermap:
"frequently P (filtermap f F) = frequently (\<lambda>x. P (f x)) F"
by (simp add: frequently_def eventually_filtermap)
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Sun Feb 12 21:11:57 2023 +0100
@@ -646,8 +646,8 @@
val unitT = \<^type_name>\<open>unit\<close> `%% [];
val unitt =
IConst { sym = Code_Symbol.Constant \<^const_name>\<open>Unity\<close>, typargs = [], dicts = [], dom = [],
- annotation = NONE };
- fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
+ annotation = NONE, range = unitT };
+ fun dest_abs ((v, ty) `|=> (t, _), _) = ((v, ty), t)
| dest_abs (t, ty) =
let
val vs = fold_varnames cons t [];
@@ -667,18 +667,18 @@
else force t
| _ => force t;
fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=>
- ICase { term = IVar (SOME dummy_name), typ = unitT, clauses = [(unitt, tr_bind'' ts)], primitive = dummy_case_term }
+ (ICase { term = IVar (SOME dummy_name), typ = unitT, clauses = [(unitt, tr_bind'' ts)], primitive = dummy_case_term }, unitT)
fun imp_monad_bind' (const as { sym = Code_Symbol.Constant c, dom = dom, ... }) ts = if is_bind c then case (ts, dom)
of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
| ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
- | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
+ | (ts, _) => imp_monad_bind (satisfied_application 2 (const, ts))
else IConst const `$$ map imp_monad_bind ts
and imp_monad_bind (IConst const) = imp_monad_bind' const []
| imp_monad_bind (t as IVar _) = t
| imp_monad_bind (t as _ `$ _) = (case unfold_app t
of (IConst const, ts) => imp_monad_bind' const ts
| (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
- | imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t
+ | imp_monad_bind (v_ty `|=> t) = v_ty `|=> apfst imp_monad_bind t
| imp_monad_bind (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) =
ICase { term = imp_monad_bind t, typ = ty,
clauses = (map o apply2) imp_monad_bind clauses, primitive = imp_monad_bind t0 };
--- a/src/HOL/Library/Word.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Library/Word.thy Sun Feb 12 21:11:57 2023 +0100
@@ -605,20 +605,21 @@
where \<open>enum_word = map word_of_nat [0..<2 ^ LENGTH('a)]\<close>
definition enum_all_word :: \<open>('a word \<Rightarrow> bool) \<Rightarrow> bool\<close>
- where \<open>enum_all_word = Ball UNIV\<close>
+ where \<open>enum_all_word = All\<close>
definition enum_ex_word :: \<open>('a word \<Rightarrow> bool) \<Rightarrow> bool\<close>
- where \<open>enum_ex_word = Bex UNIV\<close>
+ where \<open>enum_ex_word = Ex\<close>
+
+instance
+ by standard
+ (simp_all add: enum_all_word_def enum_ex_word_def enum_word_def distinct_map inj_on_word_of_nat flip: UNIV_word_eq_word_of_nat)
+
+end
lemma [code]:
- \<open>Enum.enum_all P \<longleftrightarrow> Ball UNIV P\<close>
- \<open>Enum.enum_ex P \<longleftrightarrow> Bex UNIV P\<close> for P :: \<open>'a word \<Rightarrow> bool\<close>
- by (simp_all add: enum_all_word_def enum_ex_word_def)
-
-instance
- by standard (simp_all add: UNIV_word_eq_word_of_nat inj_on_word_of_nat enum_word_def enum_all_word_def enum_ex_word_def distinct_map)
-
-end
+ \<open>Enum.enum_all P \<longleftrightarrow> list_all P Enum.enum\<close>
+ \<open>Enum.enum_ex P \<longleftrightarrow> list_ex P Enum.enum\<close> for P :: \<open>'a::len word \<Rightarrow> bool\<close>
+ by (simp_all add: enum_all_word_def enum_ex_word_def enum_UNIV list_all_iff list_ex_iff)
subsection \<open>Bit-wise operations\<close>
--- a/src/HOL/Topological_Spaces.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Topological_Spaces.thy Sun Feb 12 21:11:57 2023 +0100
@@ -1078,6 +1078,37 @@
lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
+lemma Lim_cong:
+ assumes "eventually (\<lambda>x. f x = g x) F" "F = G"
+ shows "Lim F f = Lim G g"
+proof (cases "(\<exists>c. (f \<longlongrightarrow> c) F) \<and> F \<noteq> bot")
+ case True
+ then obtain c where c: "(f \<longlongrightarrow> c) F"
+ by blast
+ hence "Lim F f = c"
+ using True by (intro tendsto_Lim) auto
+ moreover have "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) G"
+ using assms by (intro filterlim_cong) auto
+ with True c assms have "Lim G g = c"
+ by (intro tendsto_Lim) auto
+ ultimately show ?thesis
+ by simp
+next
+ case False
+ show ?thesis
+ proof (cases "F = bot")
+ case True
+ thus ?thesis using assms
+ by (auto simp: Topological_Spaces.Lim_def)
+ next
+ case False
+ have "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) G" for c
+ using assms by (intro filterlim_cong) auto
+ thus ?thesis
+ by (auto simp: Topological_Spaces.Lim_def)
+ qed
+qed
+
lemma eventually_Lim_ident_at:
"(\<forall>\<^sub>F y in at x within X. P (Lim (at x within X) (\<lambda>x. x)) y) \<longleftrightarrow>
(\<forall>\<^sub>F y in at x within X. P x y)" for x::"'a::t2_space"
@@ -2217,6 +2248,18 @@
"continuous_on A (f :: 'a :: discrete_topology \<Rightarrow> _)"
by (auto simp: continuous_on_def at_discrete)
+lemma continuous_on_of_nat [continuous_intros]:
+ assumes "continuous_on A f"
+ shows "continuous_on A (\<lambda>n. of_nat (f n))"
+ using continuous_on_compose[OF assms continuous_on_discrete[of _ of_nat]]
+ by (simp add: o_def)
+
+lemma continuous_on_of_int [continuous_intros]:
+ assumes "continuous_on A f"
+ shows "continuous_on A (\<lambda>n. of_int (f n))"
+ using continuous_on_compose[OF assms continuous_on_discrete[of _ of_int]]
+ by (simp add: o_def)
+
subsubsection \<open>Continuity at a point\<close>
definition continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool"
@@ -2330,6 +2373,21 @@
"isCont g (f x) \<Longrightarrow> continuous (at x within s) f \<Longrightarrow> continuous (at x within s) (\<lambda>x. g (f x))"
using continuous_at_imp_continuous_at_within continuous_within_compose2 by blast
+lemma at_within_isCont_imp_nhds:
+ fixes f:: "'a:: {t2_space,perfect_space} \<Rightarrow> 'b:: t2_space"
+ assumes "\<forall>\<^sub>F w in at z. f w = g w" "isCont f z" "isCont g z"
+ shows "\<forall>\<^sub>F w in nhds z. f w = g w"
+proof -
+ have "g \<midarrow>z\<rightarrow> f z"
+ using assms isContD tendsto_cong by blast
+ moreover have "g \<midarrow>z\<rightarrow> g z" using \<open>isCont g z\<close> using isCont_def by blast
+ ultimately have "f z=g z" using LIM_unique by auto
+ moreover have "\<forall>\<^sub>F x in nhds z. x \<noteq> z \<longrightarrow> f x = g x"
+ using assms unfolding eventually_at_filter by auto
+ ultimately show ?thesis
+ by (auto elim:eventually_mono)
+qed
+
lemma filtermap_nhds_open_map':
assumes cont: "isCont f a"
and "open A" "a \<in> A"
@@ -2933,6 +2991,30 @@
by auto
qed
+lemma connected_Un_UN:
+ assumes "connected A" "\<And>X. X \<in> B \<Longrightarrow> connected X" "\<And>X. X \<in> B \<Longrightarrow> A \<inter> X \<noteq> {}"
+ shows "connected (A \<union> \<Union>B)"
+proof (rule connectedI_const)
+ fix f :: "'a \<Rightarrow> bool"
+ assume f: "continuous_on (A \<union> \<Union>B) f"
+ have "connected A" "continuous_on A f"
+ by (auto intro: assms continuous_on_subset[OF f(1)])
+ from connectedD_const[OF this] obtain c where c: "\<And>x. x \<in> A \<Longrightarrow> f x = c"
+ by metis
+ have "f x = c" if "x \<in> X" "X \<in> B" for x X
+ proof -
+ have "connected X" "continuous_on X f"
+ using that by (auto intro: assms continuous_on_subset[OF f])
+ from connectedD_const[OF this] obtain c' where c': "\<And>x. x \<in> X \<Longrightarrow> f x = c'"
+ by metis
+ from assms(3) and that obtain y where "y \<in> A \<inter> X"
+ by auto
+ with c[of y] c'[of y] c'[of x] that show ?thesis
+ by auto
+ qed
+ with c show "\<exists>c. \<forall>x\<in>A \<union> \<Union> B. f x = c"
+ by (intro exI[of _ c]) auto
+qed
section \<open>Linear Continuum Topologies\<close>
@@ -3885,5 +3967,4 @@
then show ?thesis using open_subdiagonal closed_Diff by auto
qed
-
end
--- a/src/HOL/Transcendental.thy Sun Feb 12 21:09:12 2023 +0100
+++ b/src/HOL/Transcendental.thy Sun Feb 12 21:11:57 2023 +0100
@@ -4204,6 +4204,12 @@
finally show ?thesis .
qed
+lemma cos_zero_iff_int2:
+ fixes x::real
+ shows "cos x = 0 \<longleftrightarrow> (\<exists>n::int. x = n * pi + pi/2)"
+ using sin_zero_iff_int2[of "x-pi/2"] unfolding sin_cos_eq
+ by (auto simp add: algebra_simps)
+
lemma sin_npi_int [simp]: "sin (pi * of_int n) = 0"
by (simp add: sin_zero_iff_int2)
@@ -4548,6 +4554,9 @@
for n :: nat
by (simp add: tan_def)
+lemma tan_pi_half [simp]: "tan (pi / 2) = 0"
+ by (simp add: tan_def)
+
lemma tan_minus [simp]: "tan (- x) = - tan x"
by (simp add: tan_def)
@@ -4561,6 +4570,16 @@
for x :: "'a::{real_normed_field,banach}"
by (simp add: tan_def sin_add field_simps)
+lemma tan_eq_0_cos_sin: "tan x = 0 \<longleftrightarrow> cos x = 0 \<or> sin x = 0"
+ by (auto simp: tan_def)
+
+text \<open>Note: half of these zeros would normally be regarded as undefined cases.\<close>
+lemma tan_eq_0_Ex:
+ assumes "tan x = 0"
+ obtains k::int where "x = (k/2) * pi"
+ using assms
+ by (metis cos_zero_iff_int mult.commute sin_zero_iff_int tan_eq_0_cos_sin times_divide_eq_left)
+
lemma tan_add:
"cos x \<noteq> 0 \<Longrightarrow> cos y \<noteq> 0 \<Longrightarrow> cos (x + y) \<noteq> 0 \<Longrightarrow> tan (x + y) = (tan x + tan y)/(1 - tan x * tan y)"
for x :: "'a::{real_normed_field,banach}"
@@ -4803,7 +4822,6 @@
by (simp add: tan_def)
lemma tan_periodic_nat[simp]: "tan (x + real n * pi) = tan x"
- for n :: nat
proof (induct n arbitrary: x)
case 0
then show ?case by simp
@@ -4817,25 +4835,16 @@
lemma tan_periodic_int[simp]: "tan (x + of_int i * pi) = tan x"
proof (cases "0 \<le> i")
- case True
- then have i_nat: "of_int i = of_int (nat i)" by auto
- show ?thesis unfolding i_nat
- by (metis of_int_of_nat_eq tan_periodic_nat)
-next
case False
then have i_nat: "of_int i = - of_int (nat (- i))" by auto
- have "tan x = tan (x + of_int i * pi - of_int i * pi)"
- by auto
- also have "\<dots> = tan (x + of_int i * pi)"
- unfolding i_nat mult_minus_left diff_minus_eq_add
- by (metis of_int_of_nat_eq tan_periodic_nat)
- finally show ?thesis by auto
-qed
+ then show ?thesis
+ by (smt (verit, best) mult_minus_left of_int_of_nat_eq tan_periodic_nat)
+qed (use zero_le_imp_eq_int in fastforce)
lemma tan_periodic_n[simp]: "tan (x + numeral n * pi) = tan x"
using tan_periodic_int[of _ "numeral n" ] by simp
-lemma tan_minus_45: "tan (-(pi/4)) = -1"
+lemma tan_minus_45 [simp]: "tan (-(pi/4)) = -1"
unfolding tan_def by (simp add: sin_45 cos_45)
lemma tan_diff:
@@ -4923,11 +4932,7 @@
lemma cot_less_zero:
assumes lb: "- pi/2 < x" and "x < 0"
shows "cot x < 0"
-proof -
- have "0 < cot (- x)"
- using assms by (simp only: cot_gt_zero)
- then show ?thesis by simp
-qed
+ by (smt (verit) assms cot_gt_zero cot_minus divide_minus_left)
lemma DERIV_cot [simp]: "sin x \<noteq> 0 \<Longrightarrow> DERIV cot x :> -inverse ((sin x)\<^sup>2)"
for x :: "'a::{real_normed_field,banach}"
@@ -5160,6 +5165,48 @@
lemma cos_arctan_not_zero [simp]: "cos (arctan x) \<noteq> 0"
by (intro less_imp_neq [symmetric] cos_gt_zero_pi arctan_lbound arctan_ubound)
+lemma tan_eq_arctan_Ex:
+ shows "tan x = y \<longleftrightarrow> (\<exists>k::int. x = arctan y + k*pi \<or> (x = pi/2 + k*pi \<and> y=0))"
+proof
+ assume lhs: "tan x = y"
+ obtain k::int where k:"-pi/2 < x-k*pi" "x-k*pi \<le> pi/2"
+ proof
+ define k where "k \<equiv> ceiling (x/pi - 1/2)"
+ show "- pi / 2 < x - real_of_int k * pi"
+ using ceiling_divide_lower [of "pi*2" "(x * 2 - pi)"] by (auto simp: k_def field_simps)
+ show "x-k*pi \<le> pi/2"
+ using ceiling_divide_upper [of "pi*2" "(x * 2 - pi)"] by (auto simp: k_def field_simps)
+ qed
+ have "x = arctan y + of_int k * pi" when "x \<noteq> pi/2 + k*pi"
+ proof -
+ have "tan (x - k * pi) = y" using lhs tan_periodic_int[of _ "-k"] by auto
+ then have "arctan y = x - real_of_int k * pi"
+ by (smt (verit) arctan_tan lhs divide_minus_left k mult_minus_left of_int_minus tan_periodic_int that)
+ then show ?thesis by auto
+ qed
+ then show "\<exists>k. x = arctan y + of_int k * pi \<or> (x = pi/2 + k*pi \<and> y=0)"
+ using lhs k by force
+qed (auto simp: arctan)
+
+lemma arctan_tan_eq_abs_pi:
+ assumes "cos \<theta> \<noteq> 0"
+ obtains k where "arctan (tan \<theta>) = \<theta> - of_int k * pi"
+ by (metis add.commute assms cos_zero_iff_int2 eq_diff_eq tan_eq_arctan_Ex)
+
+lemma tan_eq:
+ assumes "tan x = tan y" "tan x \<noteq> 0"
+ obtains k::int where "x = y + k * pi"
+proof -
+ obtain k0 where k0: "x = arctan (tan y) + real_of_int k0 * pi"
+ using assms tan_eq_arctan_Ex[of x "tan y"] by auto
+ obtain k1 where k1: "arctan (tan y) = y - of_int k1 * pi"
+ using arctan_tan_eq_abs_pi assms tan_eq_0_cos_sin by auto
+ have "x = y + (k0-k1)*pi"
+ using k0 k1 by (auto simp: algebra_simps)
+ with that show ?thesis
+ by blast
+qed
+
lemma cos_arctan: "cos (arctan x) = 1 / sqrt (1 + x\<^sup>2)"
proof (rule power2_eq_imp_eq)
have "0 < 1 + x\<^sup>2" by (simp add: add_pos_nonneg)
--- a/src/Tools/Code/code_haskell.ML Sun Feb 12 21:09:12 2023 +0100
+++ b/src/Tools/Code/code_haskell.ML Sun Feb 12 21:11:57 2023 +0100
@@ -241,18 +241,18 @@
str "=",
print_app tyvars (SOME thm) reserved NOBR (const, [])
]
- | SOME (k, Code_Printer.Complex_printer _) =>
+ | SOME (wanted, Code_Printer.Complex_printer _) =>
let
- val { sym = Constant c, dom, ... } = const;
+ val { sym = Constant c, dom, range, ... } = const;
val (vs, rhs) = (apfst o map) fst
- (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
+ (Code_Thingol.unfold_abs (Code_Thingol.satisfied_application wanted (const, [])));
val s = if (is_some o const_syntax) c
then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
val vars = reserved
|> intro_vars (map_filter I (s :: vs));
val lhs = IConst { sym = Constant classparam, typargs = [],
- dicts = [], dom = dom, annotation = NONE } `$$ map IVar vs;
- (*dictionaries are not relevant at this late stage,
+ dicts = [], dom = dom, range = range, annotation = NONE } `$$ map IVar vs;
+ (*dictionaries are not relevant in Haskell,
and these consts never need type annotations for disambiguation *)
in
semicolon [
--- a/src/Tools/Code/code_ml.ML Sun Feb 12 21:09:12 2023 +0100
+++ b/src/Tools/Code/code_ml.ML Sun Feb 12 21:11:57 2023 +0100
@@ -123,17 +123,17 @@
then print_case is_pseudo_fun some_thm vars fxy case_expr
else print_app is_pseudo_fun some_thm vars fxy app
| NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
- and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
+ and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts, dom, ... }, ts)) =
if is_constr sym then
- let val k = length dom in
- if k < 2 orelse length ts = k
+ let val wanted = length dom in
+ if wanted < 2 orelse length ts = wanted
then (str o deresolve) sym
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
- else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
+ else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.satisfied_application wanted app)]
end
else if is_pseudo_fun sym
then (str o deresolve) sym @@ str "()"
- else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
+ else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
@ map (print_term is_pseudo_fun some_thm vars BR) ts
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
(print_term is_pseudo_fun) const_syntax some_thm vars
@@ -446,17 +446,17 @@
then print_case is_pseudo_fun some_thm vars fxy case_expr
else print_app is_pseudo_fun some_thm vars fxy app
| NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
- and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
+ and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts, dom, ... }, ts)) =
if is_constr sym then
- let val k = length dom in
- if length ts = k
+ let val wanted = length dom in
+ if length ts = wanted
then (str o deresolve) sym
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
- else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
+ else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.satisfied_application wanted app)]
end
else if is_pseudo_fun sym
then (str o deresolve) sym @@ str "()"
- else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
+ else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
@ map (print_term is_pseudo_fun some_thm vars BR) ts
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
(print_term is_pseudo_fun) const_syntax some_thm vars
--- a/src/Tools/Code/code_printer.ML Sun Feb 12 21:09:12 2023 +0100
+++ b/src/Tools/Code/code_printer.ML Sun Feb 12 21:11:57 2023 +0100
@@ -325,17 +325,17 @@
NONE => brackify fxy (print_app_expr some_thm vars app)
| SOME (_, Plain_printer s) =>
brackify fxy (str s :: map (print_term some_thm vars BR) ts)
- | SOME (k, Complex_printer print) =>
+ | SOME (wanted, Complex_printer print) =>
let
fun print' fxy ts =
- print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
+ print (print_term some_thm) some_thm vars fxy (ts ~~ take wanted dom);
in
- if k = length ts
+ if wanted = length ts
then print' fxy ts
- else if k < length ts
- then case chop k ts of (ts1, ts2) =>
+ else if wanted < length ts
+ then case chop wanted ts of (ts1, ts2) =>
brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
- else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
+ else print_term some_thm vars fxy (Code_Thingol.satisfied_application wanted app)
end)
| _ => brackify fxy (print_app_expr some_thm vars app);
--- a/src/Tools/Code/code_scala.ML Sun Feb 12 21:09:12 2023 +0100
+++ b/src/Tools/Code/code_scala.ML Sun Feb 12 21:11:57 2023 +0100
@@ -117,7 +117,6 @@
and print_app tyvars is_pat some_thm vars fxy
(app as ({ sym, typargs, dom, dicts, ... }, ts)) =
let
- val k = length ts;
val typargs' = if is_pat then [] else typargs;
val syntax = case sym of
Constant const => const_syntax const
@@ -127,7 +126,7 @@
orelse Code_Thingol.unambiguous_dictss dicts
then fn p => K p
else applify_dictss tyvars;
- val (l, print') = case syntax of
+ val (wanted, print') = case syntax of
NONE => (args_num sym, fn fxy => fn ts => applify_dicts
(gen_applify (is_constr sym) "(" ")"
(print_term tyvars is_pat some_thm vars NOBR) fxy
@@ -141,11 +140,11 @@
| SOME (k, Complex_printer print) =>
(k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
(ts ~~ take k dom))
- in if k = l then print' fxy ts
- else if k < l then
- print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
+ in if length ts = wanted then print' fxy ts
+ else if length ts < wanted then
+ print_term tyvars is_pat some_thm vars fxy (Code_Thingol.satisfied_application wanted app)
else let
- val (ts1, ts23) = chop l ts;
+ val (ts1, ts23) = chop wanted ts;
in
Pretty.block (print' BR ts1 :: map (fn t => Pretty.block
[str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23)
--- a/src/Tools/Code/code_thingol.ML Sun Feb 12 21:09:12 2023 +0100
+++ b/src/Tools/Code/code_thingol.ML Sun Feb 12 21:11:57 2023 +0100
@@ -9,6 +9,7 @@
infix 4 `$;
infix 4 `$$;
infixr 3 `->;
+infixr 3 `-->;
infixr 3 `|=>;
infixr 3 `|==>;
@@ -24,16 +25,17 @@
`%% of string * itype list
| ITyVar of vname;
type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
- dom: itype list, annotation: itype option };
+ dom: itype list, range: itype, annotation: itype option };
datatype iterm =
IConst of const
| IVar of vname option
| `$ of iterm * iterm
- | `|=> of (vname option * itype) * iterm
+ | `|=> of (vname option * itype) * (iterm * itype)
| ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
val `-> : itype * itype -> itype;
+ val `--> : itype list * itype -> itype;
val `$$ : iterm * iterm list -> iterm;
- val `|==> : (vname option * itype) list * iterm -> iterm;
+ val `|==> : (vname option * itype) list * (iterm * itype) -> iterm;
type typscheme = (vname * sort) list * itype;
end;
@@ -46,6 +48,7 @@
val unfold_fun_n: int -> itype -> itype list * itype
val unfold_app: iterm -> iterm * iterm list
val unfold_abs: iterm -> (vname option * itype) list * iterm
+ val unfold_abs_typed: iterm -> ((vname option * itype) list * (iterm * itype)) option
val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
val split_let_no_pat: iterm -> (((string option * itype) * iterm) * iterm) option
val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
@@ -53,10 +56,9 @@
val split_pat_abs: iterm -> ((iterm * itype) * iterm) option
val unfold_pat_abs: iterm -> (iterm * itype) list * iterm
val unfold_const_app: iterm -> (const * iterm list) option
- val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
val is_IVar: iterm -> bool
val is_IAbs: iterm -> bool
- val eta_expand: int -> const * iterm list -> iterm
+ val satisfied_application: int -> const * iterm list -> iterm
val contains_dict_var: iterm -> bool
val unambiguous_dictss: dict list list -> bool
val add_constsyms: iterm -> Code_Symbol.T list -> Code_Symbol.T list
@@ -144,6 +146,8 @@
fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];
+val op `--> = Library.foldr (op `->);
+
val unfold_fun = unfoldr
(fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2)
| _ => NONE);
@@ -152,17 +156,16 @@
let
val (tys1, ty1) = unfold_fun ty;
val (tys3, tys2) = chop n tys1;
- val ty3 = Library.foldr (op `->) (tys2, ty1);
- in (tys3, ty3) end;
+ in (tys3, tys2 `--> ty1) end;
type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
- dom: itype list, annotation: itype option };
+ dom: itype list, range: itype, annotation: itype option };
datatype iterm =
IConst of const
| IVar of vname option
| `$ of iterm * iterm
- | `|=> of (vname option * itype) * iterm
+ | `|=> of (vname option * itype) * (iterm * itype)
| ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
(*see also signature*)
@@ -173,23 +176,33 @@
| is_IAbs _ = false;
val op `$$ = Library.foldl (op `$);
-val op `|==> = Library.foldr (op `|=>);
+fun vs_tys `|==> body = Library.foldr
+ (fn (v_ty as (_, ty), body as (_, rty)) => (v_ty `|=> body, ty `-> rty)) (vs_tys, body)
+ |> fst;
val unfold_app = unfoldl
- (fn op `$ t => SOME t
+ (fn op `$ t_t => SOME t_t
| _ => NONE);
val unfold_abs = unfoldr
- (fn op `|=> t => SOME t
+ (fn (v `|=> (t, _)) => SOME (v, t)
| _ => NONE);
-val split_let =
- (fn ICase { term = t, typ = ty, clauses = [(p, body)], ... } => SOME (((p, ty), t), body)
- | _ => NONE);
+fun unfold_abs_typed (v_ty `|=> body) =
+ unfoldr
+ (fn (v_ty `|=> body, _) => SOME (v_ty, body)
+ | _ => NONE) body
+ |> apfst (cons v_ty)
+ |> SOME
+ | unfold_abs_typed _ = NONE
-val split_let_no_pat =
- (fn ICase { term = t, typ = ty, clauses = [(IVar v, body)], ... } => SOME (((v, ty), t), body)
- | _ => NONE);
+fun split_let (ICase { term = t, typ = ty, clauses = [(p, body)], ... }) =
+ SOME (((p, ty), t), body)
+ | split_let _ = NONE;
+
+fun split_let_no_pat (ICase { term = t, typ = ty, clauses = [(IVar v, body)], ... }) =
+ SOME (((v, ty), t), body)
+ | split_let_no_pat _ = NONE;
val unfold_let = unfoldr split_let;
@@ -205,9 +218,9 @@
fun fold' (IConst c) = f c
| fold' (IVar _) = I
| fold' (t1 `$ t2) = fold' t1 #> fold' t2
- | fold' (_ `|=> t) = fold' t
- | fold' (ICase { term = t, clauses = clauses, ... }) = fold' t
- #> fold (fn (p, body) => fold' p #> fold' body) clauses
+ | fold' (_ `|=> (t, _)) = fold' t
+ | fold' (ICase { term = t, clauses = clauses, ... }) =
+ fold' t #> fold (fn (p, body) => fold' p #> fold' body) clauses
in fold' end;
val add_constsyms = fold_constexprs (fn { sym, ... } => insert (op =) sym);
@@ -225,8 +238,8 @@
| fold_term vs (IVar (SOME v)) = if member (op =) vs v then I else f v
| fold_term _ (IVar NONE) = I
| fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2
- | fold_term vs ((SOME v, _) `|=> t) = fold_term (insert (op =) v vs) t
- | fold_term vs ((NONE, _) `|=> t) = fold_term vs t
+ | fold_term vs ((SOME v, _) `|=> (t, _)) = fold_term (insert (op =) v vs) t
+ | fold_term vs ((NONE, _) `|=> (t, _)) = fold_term vs t
| fold_term vs (ICase { term = t, clauses = clauses, ... }) =
fold_term vs t #> fold (fold_clause vs) clauses
and fold_clause vs (p, t) = fold_term (add_vars p vs) t;
@@ -240,8 +253,11 @@
fun exists_var t v = fold_varnames (fn w => fn b => v = w orelse b) t false;
-fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t)
- | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t
+fun invent_params used tys =
+ (map o apfst) SOME (Name.invent_names (Name.build_context used) "a" tys);
+
+fun split_pat_abs ((NONE, ty) `|=> (t, _)) = SOME ((IVar NONE, ty), t)
+ | split_pat_abs ((SOME v, ty) `|=> (t, _)) = SOME (case t
of ICase { term = IVar (SOME w), clauses = [(p, body)], ... } =>
if v = w andalso (exists_var p v orelse not (exists_var body v))
then ((p, ty), body)
@@ -252,33 +268,30 @@
val unfold_pat_abs = unfoldr split_pat_abs;
fun unfold_abs_eta [] t = ([], t)
- | unfold_abs_eta (_ :: tys) (v_ty `|=> t) =
+ | unfold_abs_eta (_ :: tys) ((v, _) `|=> (t, _)) =
let
- val (vs_tys, t') = unfold_abs_eta tys t;
- in (v_ty :: vs_tys, t') end
+ val (vs, t') = unfold_abs_eta tys t;
+ in (v :: vs, t') end
| unfold_abs_eta tys t =
let
- val ctxt = Name.build_context (declare_varnames t);
- val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
- in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
+ val vs = map fst (invent_params (declare_varnames t) tys);
+ in (vs, t `$$ map IVar vs) end;
-fun eta_expand k (const as { dom = tys, ... }, ts) =
+fun satisfied_application wanted (const as { dom, range, ... }, ts) =
let
- val j = length ts;
- val l = k - j;
- val _ = if l > length tys
- then error "Impossible eta-expansion" else ();
- val vars = Name.build_context (fold declare_varnames ts);
- val vs_tys = (map o apfst) SOME
- (Name.invent_names vars "a" ((take l o drop j) tys));
- in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end;
+ val given = length ts;
+ val delta = wanted - given;
+ val vs_tys = invent_params (fold declare_varnames ts)
+ (((take delta o drop given) dom));
+ val (_, rty) = unfold_fun_n wanted range;
+ in vs_tys `|==> (IConst const `$$ ts @ map (IVar o fst) vs_tys, rty) end;
fun map_terms_bottom_up f (t as IConst _) = f t
| map_terms_bottom_up f (t as IVar _) = f t
| map_terms_bottom_up f (t1 `$ t2) = f
(map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2)
- | map_terms_bottom_up f ((v, ty) `|=> t) = f
- ((v, ty) `|=> map_terms_bottom_up f t)
+ | map_terms_bottom_up f ((v, ty) `|=> (t, rty)) = f
+ ((v, ty) `|=> (map_terms_bottom_up f t, rty))
| map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f
(ICase { term = map_terms_bottom_up f t, typ = ty,
clauses = (map o apply2) (map_terms_bottom_up f) clauses,
@@ -316,8 +329,7 @@
|> the_default [(pat_args, body)]
| NONE => [(pat_args, body)])
| distill vs_map pat_args body = [(pat_args, body)];
- val (vTs, body) = unfold_abs_eta tys t;
- val vs = map fst vTs;
+ val (vs, body) = unfold_abs_eta tys t;
val vs_map =
build (fold_index (fn (i, SOME v) => cons (v, i) | _ => I) vs);
in distill vs_map (map IVar vs) body end;
@@ -330,7 +342,7 @@
fun contains_dict_var (IConst { dicts = dss, ... }) = exists_dictss_var (K true) dss
| contains_dict_var (IVar _) = false
| contains_dict_var (t1 `$ t2) = contains_dict_var t1 orelse contains_dict_var t2
- | contains_dict_var (_ `|=> t) = contains_dict_var t
+ | contains_dict_var (_ `|=> (t, _)) = contains_dict_var t
| contains_dict_var (ICase { primitive = t, ... }) = contains_dict_var t;
val unambiguous_dictss = not o exists_dictss_var (fn { unique, ... } => not unique);
@@ -639,7 +651,7 @@
fun translate_classparam_instance (c, ty) =
let
val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
- val dom_length = length (fst (strip_type ty))
+ val dom_length = length (binder_types ty);
val thm = Axclass.unoverload_conv ctxt (Thm.cterm_of ctxt raw_const);
val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
o Logic.dest_equals o Thm.prop_of) thm;
@@ -673,10 +685,12 @@
let
val ((v', _), t') = Term.dest_abs_global (Abs (Name.desymbolize (SOME false) v, ty, t));
val v'' = if Term.used_free v' t' then SOME v' else NONE
+ val rty = fastype_of_tagged_term t'
in
translate_typ ctxt algbr eqngr permissive ty
+ ##>> translate_typ ctxt algbr eqngr permissive rty
##>> translate_term ctxt algbr eqngr permissive some_thm (t', some_abs)
- #>> (fn (ty, t) => (v'', ty) `|=> t)
+ #>> (fn ((ty, rty), t) => (v'', ty) `|=> (t, rty))
end
| translate_term ctxt algbr eqngr permissive some_thm (t as _ $ _, some_abs) =
case strip_comb t
@@ -712,11 +726,11 @@
ensure_const ctxt algbr eqngr permissive c
##>> fold_map (translate_typ ctxt algbr eqngr permissive) typargs
##>> fold_map (translate_dicts ctxt algbr eqngr permissive some_thm) (typargs ~~ sorts)
- ##>> fold_map (translate_typ ctxt algbr eqngr permissive) (ty' :: dom)
- #>> (fn (((c, typargs), dss), annotation :: dom) =>
+ ##>> fold_map (translate_typ ctxt algbr eqngr permissive) (range :: dom)
+ #>> (fn (((c, typargs), dss), range :: dom) =>
IConst { sym = Constant c, typargs = typargs, dicts = dss,
- dom = dom, annotation =
- if annotate then SOME annotation else NONE })
+ dom = dom, range = range, annotation =
+ if annotate then SOME (dom `--> range) else NONE })
end
and translate_app_const ctxt algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
translate_const ctxt algbr eqngr permissive some_thm (c_ty, some_abs)
@@ -766,21 +780,24 @@
clauses = (filter_out (is_undefined_clause ctxt) o distill_clauses constrs o project_cases) ts,
primitive = t_app `$$ ts })
end
-and translate_app_case ctxt algbr eqngr permissive some_thm (num_args, pattern_schema) ((c, ty), ts) =
- if length ts < num_args then
+and translate_app_case ctxt algbr eqngr permissive some_thm (wanted, pattern_schema) ((c, ty), ts) =
+ if length ts < wanted then
let
- val k = length ts;
- val tys = (take (num_args - k) o drop k o fst o strip_type) ty;
- val names = Name.build_context (ts |> (fold o fold_aterms) Term.declare_term_frees);
- val vs = Name.invent_names names "a" tys;
+ val given = length ts;
+ val delta = wanted - given;
+ val tys = (take delta o drop given o binder_types) ty;
+ val used = Name.build_context ((fold o fold_aterms) Term.declare_term_frees ts);
+ val vs_tys = Name.invent_names used "a" tys;
+ val rty = (drop delta o binder_types) ty ---> body_type ty;
in
fold_map (translate_typ ctxt algbr eqngr permissive) tys
- ##>> translate_case ctxt algbr eqngr permissive some_thm pattern_schema ((c, ty), ts @ map Free vs)
- #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
+ ##>> translate_case ctxt algbr eqngr permissive some_thm pattern_schema ((c, ty), ts @ map Free vs_tys)
+ ##>> translate_typ ctxt algbr eqngr permissive rty
+ #>> (fn ((tys, t), rty) => map2 (fn (v, _) => pair (SOME v)) vs_tys tys `|==> (t, rty))
end
- else if length ts > num_args then
- translate_case ctxt algbr eqngr permissive some_thm pattern_schema ((c, ty), take num_args ts)
- ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) (drop num_args ts)
+ else if length ts > wanted then
+ translate_case ctxt algbr eqngr permissive some_thm pattern_schema ((c, ty), take wanted ts)
+ ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) (drop wanted ts)
#>> (fn (t, ts) => t `$$ ts)
else
translate_case ctxt algbr eqngr permissive some_thm pattern_schema ((c, ty), ts)
--- a/src/Tools/nbe.ML Sun Feb 12 21:09:12 2023 +0100
+++ b/src/Tools/nbe.ML Sun Feb 12 21:11:57 2023 +0100
@@ -326,7 +326,7 @@
in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
and of_iapp match_cont (IConst { sym, dicts = dss, ... }) ts = constapp sym dss ts
| of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
- | of_iapp match_cont ((v, _) `|=> t) ts =
+ | of_iapp match_cont ((v, _) `|=> (t, _)) ts =
nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
| of_iapp match_cont (ICase { term = t, clauses = clauses, primitive = t0, ... }) ts =
nbe_apps (ml_cases (of_iterm NONE t)
@@ -421,7 +421,7 @@
fun dummy_const sym dss =
IConst { sym = sym, typargs = [], dicts = dss,
- dom = [], annotation = NONE };
+ dom = [], annotation = NONE, range = ITyVar "" };
fun eqns_of_stmt (_, Code_Thingol.NoStmt) =
[]