--- a/NEWS Tue Dec 20 09:34:37 2022 +0100
+++ b/NEWS Thu Dec 22 21:55:51 2022 +0100
@@ -18,6 +18,9 @@
- Dagstuhl LIPIcs style as session "Demo_LIPIcs" / doc "demo_lipics"
- Springer LaTeX LNCS style as session "Demo_LLNCS" / doc "demo_llncs"
+* Support for interactive document preparation in PIDE, notably via the
+Isabelle/jEdit Document panel.
+
*** HOL ***
@@ -84,11 +87,13 @@
irrefl_onD
irrefl_onI
irrefl_on_converse[simp]
+ irrefl_on_if_asym_on[simp]
irrefl_on_subset
irreflpD
irreflp_onD
irreflp_onI
irreflp_on_converse[simp]
+ irreflp_on_if_asymp_on[simp]
irreflp_on_irrefl_on_eq[pred_set_conv]
irreflp_on_subset
linorder.totalp_on_ge[simp]
--- a/src/HOL/Analysis/Complex_Transcendental.thy Tue Dec 20 09:34:37 2022 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Thu Dec 22 21:55:51 2022 +0100
@@ -1526,6 +1526,47 @@
qed
+lemma norm_Ln_le:
+ fixes z :: complex
+ assumes "norm z < 1/2"
+ shows "norm (Ln(1+z)) \<le> 2 * norm z"
+proof -
+ have sums: "(\<lambda>n. - ((- z) ^ n) / of_nat n) sums ln (1 + z)"
+ by (intro Ln_series') (use assms in auto)
+ have summable: "summable (\<lambda>n. norm (- ((- z) ^ n / of_nat n)))"
+ using ln_series'[of "-norm z"] assms
+ by (simp add: sums_iff summable_minus_iff norm_power norm_divide)
+
+ have "norm (ln (1 + z)) = norm (\<Sum>n. -((-z) ^ n / of_nat n))"
+ using sums by (simp add: sums_iff)
+ also have "\<dots> \<le> (\<Sum>n. norm (-((-z) ^ n / of_nat n)))"
+ using summable by (rule summable_norm)
+ also have "\<dots> = (\<Sum>n. norm (-((-z) ^ Suc n / of_nat (Suc n))))"
+ using summable by (subst suminf_split_head) auto
+ also have "\<dots> \<le> (\<Sum>n. norm z * (1 / 2) ^ n)"
+ proof (rule suminf_le)
+ show "summable (\<lambda>n. norm z * (1 / 2) ^ n)"
+ by (intro summable_mult summable_geometric) auto
+ next
+ show "summable (\<lambda>n. norm (- ((- z) ^ Suc n / of_nat (Suc n))))"
+ using summable by (subst summable_Suc_iff)
+ next
+ fix n
+ have "norm (-((-z) ^ Suc n / of_nat (Suc n))) = norm z * (norm z ^ n / real (Suc n))"
+ by (simp add: norm_power norm_divide norm_mult del: of_nat_Suc)
+ also have "\<dots> \<le> norm z * ((1 / 2) ^ n / 1)"
+ using assms by (intro mult_left_mono frac_le power_mono) auto
+ finally show "norm (- ((- z) ^ Suc n / of_nat (Suc n))) \<le> norm z * (1 / 2) ^ n"
+ by simp
+ qed
+ also have "\<dots> = norm z * (\<Sum>n. (1 / 2) ^ n)"
+ by (subst suminf_mult) (auto intro: summable_geometric)
+ also have "(\<Sum>n. (1 / 2 :: real) ^ n) = 2"
+ using geometric_sums[of "1 / 2 :: real"] by (simp add: sums_iff)
+ finally show ?thesis
+ by (simp add: mult_ac)
+qed
+
subsection\<^marker>\<open>tag unimportant\<close>\<open>Quadrant-type results for Ln\<close>
lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
@@ -1796,6 +1837,260 @@
finally show ?thesis .
qed
+lemma norm_Ln_times_le:
+ assumes "w \<noteq> 0" "z \<noteq> 0"
+ shows "cmod (Ln(w * z)) \<le> cmod (Ln(w) + Ln(z))"
+proof (cases "- pi < Im(Ln w + Ln z) \<and> Im(Ln w + Ln z) \<le> pi")
+ case True
+ then show ?thesis
+ by (simp add: Ln_times_simple assms)
+next
+ case False
+ then show ?thesis
+ by (smt (verit) Im_Ln_le_pi assms cmod_Im_le_iff exp_Ln exp_add ln_unique mpi_less_Im_Ln mult_eq_0_iff norm_exp_eq_Re)
+qed
+
+corollary norm_Ln_prod_le:
+ fixes f :: "'a \<Rightarrow> complex"
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
+ shows "cmod (Ln (prod f A)) \<le> (\<Sum>x \<in> A. cmod (Ln (f x)))"
+ using assms
+proof (induction A rule: infinite_finite_induct)
+ case (insert x A)
+ then show ?case
+ by simp (smt (verit) norm_Ln_times_le norm_triangle_ineq prod_zero_iff)
+qed auto
+
+lemma norm_Ln_exp_le: "norm (Ln (exp z)) \<le> norm z"
+ by (smt (verit) Im_Ln_le_pi Ln_exp Re_Ln cmod_Im_le_iff exp_not_eq_zero ln_exp mpi_less_Im_Ln norm_exp_eq_Re)
+
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Uniform convergence and products\<close>
+
+(* TODO: could be generalised perhaps, but then one would have to do without the ln *)
+lemma uniformly_convergent_on_prod_aux:
+ fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+ assumes norm_f: "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) < 1"
+ assumes cont: "\<And>n. continuous_on A (f n)"
+ assumes conv: "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. ln (1 + f n x))"
+ assumes A: "compact A"
+ shows "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. 1 + f n x)"
+proof -
+ from conv obtain S where S: "uniform_limit A (\<lambda>N x. \<Sum>n<N. ln (1 + f n x)) S sequentially"
+ by (auto simp: uniformly_convergent_on_def)
+ have cont': "continuous_on A S"
+ proof (rule uniform_limit_theorem[OF _ S])
+ have "f n x + 1 \<notin> \<real>\<^sub>\<le>\<^sub>0" if "x \<in> A" for n x
+ proof
+ assume "f n x + 1 \<in> \<real>\<^sub>\<le>\<^sub>0"
+ then obtain t where t: "t \<le> 0" "f n x + 1 = of_real t"
+ by (auto elim!: nonpos_Reals_cases)
+ hence "f n x = of_real (t - 1)"
+ by (simp add: algebra_simps)
+ also have "norm \<dots> \<ge> 1"
+ using t by (subst norm_of_real) auto
+ finally show False
+ using norm_f[of x n] that by auto
+ qed
+ thus "\<forall>\<^sub>F n in sequentially. continuous_on A (\<lambda>x. \<Sum>n<n. Ln (1 + f n x))"
+ by (auto intro!: always_eventually continuous_intros cont simp: add_ac)
+ qed auto
+
+ define B where "B = {x + y |x y. x \<in> S ` A \<and> y \<in> cball 0 1}"
+ have "compact B"
+ unfolding B_def by (intro compact_sums compact_continuous_image cont' A) auto
+
+ have "uniformly_convergent_on A (\<lambda>N x. exp ((\<Sum>n<N. ln (1 + f n x))))"
+ using conv
+ proof (rule uniformly_convergent_on_compose_uniformly_continuous_on)
+ show "closed B"
+ using \<open>compact B\<close> by (auto dest: compact_imp_closed)
+ show "uniformly_continuous_on B exp"
+ by (intro compact_uniformly_continuous continuous_intros \<open>compact B\<close>)
+
+ have "eventually (\<lambda>N. \<forall>x\<in>A. dist (\<Sum>n<N. Ln (1 + f n x)) (S x) < 1) sequentially"
+ using S unfolding uniform_limit_iff by simp
+ thus "eventually (\<lambda>N. \<forall>x\<in>A. (\<Sum>n<N. Ln (1 + f n x)) \<in> B) sequentially"
+ proof eventually_elim
+ case (elim N)
+ show "\<forall>x\<in>A. (\<Sum>n<N. Ln (1 + f n x)) \<in> B"
+ proof safe
+ fix x assume x: "x \<in> A"
+ have "(\<Sum>n<N. Ln (1 + f n x)) = S x + ((\<Sum>n<N. Ln (1 + f n x)) - S x)"
+ by auto
+ moreover have "((\<Sum>n<N. Ln (1 + f n x)) - S x) \<in> ball 0 1"
+ using elim x by (auto simp: dist_norm norm_minus_commute)
+ ultimately show "(\<Sum>n<N. Ln (1 + f n x)) \<in> B"
+ unfolding B_def using x by fastforce
+ qed
+ qed
+ qed
+ also have "?this \<longleftrightarrow> uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. 1 + f n x)"
+ proof (intro uniformly_convergent_cong refl always_eventually allI ballI)
+ fix N :: nat and x assume x: "x \<in> A"
+ have "exp (\<Sum>n<N. ln (1 + f n x)) = (\<Prod>n<N. exp (ln (1 + f n x)))"
+ by (simp add: exp_sum)
+ also have "\<dots> = (\<Prod>n<N. 1 + f n x)"
+ proof (rule prod.cong)
+ fix n assume "n \<in> {..<N}"
+ have "f n x \<noteq> -1"
+ using norm_f[of x n] x by auto
+ thus "exp (ln (1 + f n x)) = 1 + f n x"
+ by (simp add: add_eq_0_iff)
+ qed auto
+ finally show "exp (\<Sum>n<N. ln (1 + f n x)) = (\<Prod>n<N. 1 + f n x)" .
+ qed
+ finally show ?thesis .
+qed
+
+(* Theorem 17.6 by Bak & Newman, roughly *)
+lemma uniformly_convergent_on_prod:
+ fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+ assumes cont: "\<And>n. continuous_on A (f n)"
+ assumes A: "compact A"
+ assumes conv_sum: "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. norm (f n x))"
+ shows "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. 1 + f n x)"
+proof -
+ obtain M where M: "\<And>n x. n \<ge> M \<Longrightarrow> x \<in> A \<Longrightarrow> norm (f n x) < 1 / 2"
+ proof -
+ from conv_sum have "uniformly_Cauchy_on A (\<lambda>N x. \<Sum>n<N. norm (f n x))"
+ using uniformly_convergent_Cauchy by blast
+ moreover have "(1 / 2 :: real) > 0"
+ by simp
+ ultimately obtain M where M:
+ "\<And>x m n. x \<in> A \<Longrightarrow> m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> dist (\<Sum>k<m. norm (f k x)) (\<Sum>k<n. norm (f k x)) < 1 / 2"
+ unfolding uniformly_Cauchy_on_def by fast
+ show ?thesis
+ proof (rule that[of M])
+ fix n x assume nx: "n \<ge> M" "x \<in> A"
+ have "dist (\<Sum>k<Suc n. norm (f k x)) (\<Sum>k<n. norm (f k x)) < 1 / 2"
+ by (rule M) (use nx in auto)
+ also have "dist (\<Sum>k<Suc n. norm (f k x)) (\<Sum>k<n. norm (f k x)) = norm (f n x)"
+ by (simp add: dist_norm)
+ finally show "norm (f n x) < 1 / 2" .
+ qed
+ qed
+
+ have conv: "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. ln (1 + f (n + M) x))"
+ proof (rule uniformly_summable_comparison_test)
+ show "norm (ln (1 + f (n + M) x)) \<le> 2 * norm (f (n + M) x)" if "x \<in> A" for n x
+ by (rule norm_Ln_le) (use M[of "n + M" x] that in auto)
+ have *: "filterlim (\<lambda>n. n + M) at_top at_top"
+ by (rule filterlim_add_const_nat_at_top)
+ have "uniformly_convergent_on A (\<lambda>N x. 2 * ((\<Sum>n<N+M. norm (f n x)) - (\<Sum>n<M. norm (f n x))))"
+ by (intro uniformly_convergent_mult uniformly_convergent_minus
+ uniformly_convergent_on_compose[OF conv_sum *] uniformly_convergent_on_const)
+ also have "(\<lambda>N x. 2 * ((\<Sum>n<N+M. norm (f n x)) - (\<Sum>n<M. norm (f n x)))) =
+ (\<lambda>N x. \<Sum>n<N. 2 * norm (f (n + M) x))" (is "?lhs = ?rhs")
+ proof (intro ext)
+ fix N x
+ have "(\<Sum>n<N+M. norm (f n x)) - (\<Sum>n<M. norm (f n x)) = (\<Sum>n\<in>{..<N+M}-{..<M}. norm (f n x))"
+ by (subst sum_diff) auto
+ also have "\<dots> = (\<Sum>n<N. norm (f (n + M) x))"
+ by (intro sum.reindex_bij_witness[of _ "\<lambda>n. n + M" "\<lambda>n. n - M"]) auto
+ finally show "?lhs N x = ?rhs N x"
+ by (simp add: sum_distrib_left)
+ qed
+ finally show "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. 2 * cmod (f (n + M) x))" .
+ qed
+
+ have conv': "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. 1 + f (n + M) x)"
+ proof (rule uniformly_convergent_on_prod_aux)
+ show "norm (f (n + M) x) < 1" if "x \<in> A" for n x
+ using M[of "n + M" x] that by simp
+ qed (use M assms conv in auto)
+
+ then obtain S where S: "uniform_limit A (\<lambda>N x. \<Prod>n<N. 1 + f (n + M) x) S sequentially"
+ by (auto simp: uniformly_convergent_on_def)
+ have cont': "continuous_on A S"
+ by (intro uniform_limit_theorem[OF _ S] always_eventually ballI allI continuous_intros cont) auto
+
+ have "uniform_limit A (\<lambda>N x. (\<Prod>n<M. 1 + f n x) * (\<Prod>n<N. 1 + f (n + M) x)) (\<lambda>x. (\<Prod>n<M. 1 + f n x) * S x) sequentially"
+ proof (rule uniform_lim_mult[OF uniform_limit_const S])
+ show "bounded (S ` A)"
+ by (intro compact_imp_bounded compact_continuous_image A cont')
+ show "bounded ((\<lambda>x. \<Prod>n<M. 1 + f n x) ` A)"
+ by (intro compact_imp_bounded compact_continuous_image A continuous_intros cont)
+ qed
+ hence "uniformly_convergent_on A (\<lambda>N x. (\<Prod>n<M. 1 + f n x) * (\<Prod>n<N. 1 + f (n + M) x))"
+ by (auto simp: uniformly_convergent_on_def)
+ also have "(\<lambda>N x. (\<Prod>n<M. 1 + f n x) * (\<Prod>n<N. 1 + f (n + M) x)) = (\<lambda>N x. (\<Prod>n<M+N. 1 + f n x))"
+ proof (intro ext)
+ fix N :: nat and x :: complex
+ have "(\<Prod>n<N. 1 + f (n + M) x) = (\<Prod>n\<in>{M..<M+N}. 1 + f n x)"
+ by (intro prod.reindex_bij_witness[of _ "\<lambda>n. n - M" "\<lambda>n. n + M"]) auto
+ also have "(\<Prod>n<M. 1 + f n x) * \<dots> = (\<Prod>n\<in>{..<M}\<union>{M..<M+N}. 1 + f n x)"
+ by (subst prod.union_disjoint) auto
+ also have "{..<M} \<union> {M..<M+N} = {..<M+N}"
+ by auto
+ finally show "(\<Prod>n<M. 1 + f n x) * (\<Prod>n<N. 1 + f (n + M) x) = (\<Prod>n<M+N. 1 + f n x)" .
+ qed
+ finally have "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<M + N. 1 + f n x)"
+ by simp
+ hence "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<M + (N - M). 1 + f n x)"
+ by (rule uniformly_convergent_on_compose) (rule filterlim_minus_const_nat_at_top)
+ also have "?this \<longleftrightarrow> ?thesis"
+ proof (rule uniformly_convergent_cong)
+ show "eventually (\<lambda>x. \<forall>y\<in>A. (\<Prod>n<M + (x - M). 1 + f n y) = (\<Prod>n<x. 1 + f n y)) at_top"
+ using eventually_ge_at_top[of M] by eventually_elim auto
+ qed auto
+ finally show ?thesis .
+qed
+
+lemma uniformly_convergent_on_prod':
+ fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+ assumes cont: "\<And>n. continuous_on A (f n)"
+ assumes A: "compact A"
+ assumes conv_sum: "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. norm (f n x - 1))"
+ shows "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. f n x)"
+proof -
+ have "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. 1 + (f n x - 1))"
+ by (rule uniformly_convergent_on_prod) (use assms in \<open>auto intro!: continuous_intros\<close>)
+ thus ?thesis
+ by simp
+qed
+
+text\<open>Prop 17.6 of Bak and Newman, Complex Analysis, p. 243.
+ Only this version is for the reals. Can the two proofs be consolidated?\<close>
+lemma uniformly_convergent_on_prod_real:
+ fixes u :: "nat \<Rightarrow> real \<Rightarrow> real"
+ assumes contu: "\<And>k. continuous_on K (u k)"
+ and uconv: "uniformly_convergent_on K (\<lambda>n x. \<Sum>k<n. \<bar>u k x\<bar>)"
+ and K: "compact K"
+ shows "uniformly_convergent_on K (\<lambda>n x. \<Prod>k<n. 1 + u k x)"
+proof -
+ define f where "f \<equiv> \<lambda>k. complex_of_real \<circ> u k \<circ> Re"
+ define L where "L \<equiv> complex_of_real ` K"
+ have "compact L"
+ by (simp add: \<open>compact K\<close> L_def compact_continuous_image)
+ have "Re ` complex_of_real ` X = X" for X
+ by (auto simp: image_iff)
+ with contu have contf: "\<And>k. continuous_on L (f k)"
+ unfolding f_def L_def by (intro continuous_intros) auto
+ obtain S where S: "\<And>\<epsilon>. \<epsilon>>0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<Sum>k<n. \<bar>u k x\<bar>) (S x) < \<epsilon>"
+ using uconv unfolding uniformly_convergent_on_def uniform_limit_iff by presburger
+ have "\<forall>\<^sub>F n in sequentially. \<forall>z\<in>L. dist (\<Sum>k<n. cmod (f k z)) ((of_real \<circ> S \<circ> Re) z) < \<epsilon>"
+ if "\<epsilon>>0" for \<epsilon>
+ using S [OF that] by eventually_elim (simp add: L_def f_def)
+ then have uconvf: "uniformly_convergent_on L (\<lambda>n z. \<Sum>k<n. norm (f k z))"
+ unfolding uniformly_convergent_on_def uniform_limit_iff by blast
+ obtain P where P: "\<And>\<epsilon>. \<epsilon>>0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>z\<in>L. dist (\<Prod>k<n. 1 + f k z) (P z) < \<epsilon>"
+ using uniformly_convergent_on_prod [OF contf \<open>compact L\<close> uconvf]
+ unfolding uniformly_convergent_on_def uniform_limit_iff by blast
+ have \<section>: "\<bar>(\<Prod>k<n. 1 + u k x) - Re (P x)\<bar> \<le> cmod ((\<Prod>k<n. 1 + of_real (u k x)) - P x)" for n x
+ proof -
+ have "(\<Prod>k\<in>N. of_real (1 + u k x)) = (\<Prod>k\<in>N. 1 + of_real (u k x))" for N
+ by force
+ then show ?thesis
+ by (metis Re_complex_of_real abs_Re_le_cmod minus_complex.sel(1) of_real_prod)
+ qed
+ have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<Prod>k<n. 1 + u k x) ((Re \<circ> P \<circ> of_real) x) < \<epsilon>"
+ if "\<epsilon>>0" for \<epsilon>
+ using P [OF that] by eventually_elim (simp add: L_def f_def dist_norm le_less_trans [OF \<section>])
+ then show ?thesis
+ unfolding uniformly_convergent_on_def uniform_limit_iff by blast
+qed
+
+
subsection\<open>The Argument of a Complex Number\<close>
text\<open>Unlike in HOL Light, it's defined for the same interval as the complex logarithm: \<open>(-\<pi>,\<pi>]\<close>.\<close>
@@ -2623,7 +2918,6 @@
qed
qed
-
subsection\<^marker>\<open>tag unimportant\<close>\<open>Some Limits involving Logarithms\<close>
lemma lim_Ln_over_power:
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Tue Dec 20 09:34:37 2022 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Thu Dec 22 21:55:51 2022 +0100
@@ -1130,6 +1130,12 @@
using assms uniformly_continuous_on_add [of s f "- g"]
by (simp add: fun_Compl_def uniformly_continuous_on_minus)
+lemma uniformly_continuous_on_sum [continuous_intros]:
+ fixes f :: "'a \<Rightarrow> 'b::metric_space \<Rightarrow> 'c::real_normed_vector"
+ shows "(\<And>i. i \<in> I \<Longrightarrow> uniformly_continuous_on S (f i)) \<Longrightarrow> uniformly_continuous_on S (\<lambda>x. \<Sum>i\<in>I. f i x)"
+ by (induction I rule: infinite_finite_induct)
+ (auto simp: uniformly_continuous_on_add uniformly_continuous_on_const)
+
subsection\<^marker>\<open>tag unimportant\<close> \<open>Arithmetic Preserves Topological Properties\<close>
--- a/src/HOL/Analysis/Infinite_Products.thy Tue Dec 20 09:34:37 2022 +0100
+++ b/src/HOL/Analysis/Infinite_Products.thy Thu Dec 22 21:55:51 2022 +0100
@@ -118,6 +118,48 @@
shows "f has_prod s \<Longrightarrow> s = prodinf f"
by (simp add: has_prod_unique2 prodinf_def the_equality)
+lemma has_prod_eq_0_iff:
+ fixes f :: "nat \<Rightarrow> 'a :: {semidom, comm_semiring_1, t2_space}"
+ assumes "f has_prod P"
+ shows "P = 0 \<longleftrightarrow> 0 \<in> range f"
+proof
+ assume "0 \<in> range f"
+ then obtain N where N: "f N = 0"
+ by auto
+ have "eventually (\<lambda>n. n > N) at_top"
+ by (rule eventually_gt_at_top)
+ hence "eventually (\<lambda>n. (\<Prod>k<n. f k) = 0) at_top"
+ by eventually_elim (use N in auto)
+ hence "(\<lambda>n. \<Prod>k<n. f k) \<longlonglongrightarrow> 0"
+ by (simp add: tendsto_eventually)
+ moreover have "(\<lambda>n. \<Prod>k<n. f k) \<longlonglongrightarrow> P"
+ using assms by (metis N calculation prod_defs(2) raw_has_prod_eq_0 zero_le)
+ ultimately show "P = 0"
+ using tendsto_unique by force
+qed (use assms in \<open>auto simp: has_prod_def\<close>)
+
+lemma has_prod_0D:
+ fixes f :: "nat \<Rightarrow> 'a :: {semidom, comm_semiring_1, t2_space}"
+ shows "f has_prod 0 \<Longrightarrow> 0 \<in> range f"
+ using has_prod_eq_0_iff[of f 0] by auto
+
+lemma has_prod_zeroI:
+ fixes f :: "nat \<Rightarrow> 'a :: {semidom, comm_semiring_1, t2_space}"
+ assumes "f has_prod P" "f n = 0"
+ shows "P = 0"
+ using assms by (auto simp: has_prod_eq_0_iff)
+
+lemma raw_has_prod_in_Reals:
+ assumes "raw_has_prod (complex_of_real \<circ> z) M p"
+ shows "p \<in> \<real>"
+ using assms by (auto simp: raw_has_prod_def real_lim_sequentially)
+
+lemma raw_has_prod_of_real_iff: "raw_has_prod (complex_of_real \<circ> z) M (of_real p) \<longleftrightarrow> raw_has_prod z M p"
+ by (auto simp: raw_has_prod_def tendsto_of_real_iff simp flip: of_real_prod)
+
+lemma convergent_prod_of_real_iff: "convergent_prod (complex_of_real \<circ> z) \<longleftrightarrow> convergent_prod z"
+ by (smt (verit, best) Reals_cases convergent_prod_def raw_has_prod_in_Reals raw_has_prod_of_real_iff)
+
lemma convergent_prod_altdef:
fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}"
shows "convergent_prod f \<longleftrightarrow> (\<exists>M L. (\<forall>n\<ge>M. f n \<noteq> 0) \<and> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L \<and> L \<noteq> 0)"
@@ -668,6 +710,24 @@
using assms convergent_prod_offset_0 [OF assms]
by (simp add: prod_defs lim_def) (metis (no_types) assms(1) convergent_prod_to_zero_iff)
+lemma prodinf_eq_lim':
+ fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
+ assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
+ shows "prodinf f = lim (\<lambda>n. \<Prod>i<n. f i)"
+ by (metis assms prodinf_eq_lim LIMSEQ_lessThan_iff_atMost convergent_prod_iff_nz_lim limI)
+
+lemma prodinf_eq_prod_lim:
+ fixes a:: "'a :: {topological_semigroup_mult,t2_space,idom}"
+ assumes "(\<lambda>n. \<Prod>k\<le>n. f k) \<longlonglongrightarrow> a" "a \<noteq> 0"
+ shows"(\<Prod>k. f k) = a"
+ by (metis LIMSEQ_prod_0 LIMSEQ_unique assms convergent_prod_iff_nz_lim limI prodinf_eq_lim)
+
+lemma prodinf_eq_prod_lim':
+ fixes a:: "'a :: {topological_semigroup_mult,t2_space,idom}"
+ assumes "(\<lambda>n. \<Prod>k<n. f k) \<longlonglongrightarrow> a" "a \<noteq> 0"
+ shows"(\<Prod>k. f k) = a"
+ using LIMSEQ_lessThan_iff_atMost assms prodinf_eq_prod_lim by blast
+
lemma has_prod_one[simp, intro]: "(\<lambda>n. 1) has_prod 1"
unfolding prod_defs by auto
@@ -833,6 +893,34 @@
shows "(\<lambda>r. if r = i then f r else 1) has_prod f i"
using has_prod_If_finite[of "\<lambda>r. r = i"] by simp
+text \<open>The ge1 assumption can probably be weakened, at the expense of extra work\<close>
+lemma uniform_limit_prodinf:
+ fixes f:: "nat \<Rightarrow> real \<Rightarrow> real"
+ assumes "uniformly_convergent_on X (\<lambda>n x. \<Prod>k<n. f k x)"
+ and ge1: "\<And>x k . x \<in> X \<Longrightarrow> f k x \<ge> 1"
+ shows "uniform_limit X (\<lambda>n x. \<Prod>k<n. f k x) (\<lambda>x. \<Prod>k. f k x) sequentially"
+proof -
+ have ul: "uniform_limit X (\<lambda>n x. \<Prod>k<n. f k x) (\<lambda>x. lim (\<lambda>n. \<Prod>k<n. f k x)) sequentially"
+ using assms uniformly_convergent_uniform_limit_iff by blast
+ moreover have "(\<Prod>k. f k x) = lim (\<lambda>n. \<Prod>k<n. f k x)" if "x \<in> X" for x
+ proof (intro prodinf_eq_lim')
+ have tends: "(\<lambda>n. \<Prod>k<n. f k x) \<longlonglongrightarrow> lim (\<lambda>n. \<Prod>k<n. f k x)"
+ using tendsto_uniform_limitI [OF ul] that by metis
+ moreover have "(\<Prod>k<n. f k x) \<ge> 1" for n
+ using ge1 by (simp add: prod_ge_1 that)
+ ultimately have "lim (\<lambda>n. \<Prod>k<n. f k x) \<ge> 1"
+ by (meson LIMSEQ_le_const)
+ then have "raw_has_prod (\<lambda>k. f k x) 0 (lim (\<lambda>n. \<Prod>k<n. f k x))"
+ using LIMSEQ_lessThan_iff_atMost tends by (auto simp: raw_has_prod_def)
+ then show "convergent_prod (\<lambda>k. f k x)"
+ unfolding convergent_prod_def by blast
+ show "\<And>k. f k x \<noteq> 0"
+ by (smt (verit) ge1 that)
+ qed
+ ultimately show ?thesis
+ by (metis (mono_tags, lifting) uniform_limit_cong')
+qed
+
context
fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
begin
@@ -902,29 +990,15 @@
subsection\<^marker>\<open>tag unimportant\<close> \<open>Infinite products on ordered topological monoids\<close>
-lemma LIMSEQ_prod_0:
- fixes f :: "nat \<Rightarrow> 'a::{semidom,topological_space}"
- assumes "f i = 0"
- shows "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> 0"
-proof (subst tendsto_cong)
- show "\<forall>\<^sub>F n in sequentially. prod f {..n} = 0"
- proof
- show "prod f {..n} = 0" if "n \<ge> i" for n
- using that assms by auto
- qed
-qed auto
-
-lemma LIMSEQ_prod_nonneg:
- fixes f :: "nat \<Rightarrow> 'a::{linordered_semidom,linorder_topology}"
- assumes 0: "\<And>n. 0 \<le> f n" and a: "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> a"
- shows "a \<ge> 0"
- by (simp add: "0" prod_nonneg LIMSEQ_le_const [OF a])
-
-
context
fixes f :: "nat \<Rightarrow> 'a::{linordered_semidom,linorder_topology}"
begin
+lemma has_prod_nonzero:
+ assumes "f has_prod a" "a \<noteq> 0"
+ shows "f k \<noteq> 0"
+ using assms by (auto simp: has_prod_def raw_has_prod_def LIMSEQ_prod_0 LIMSEQ_unique)
+
lemma has_prod_le:
assumes f: "f has_prod a" and g: "g has_prod b" and le: "\<And>n. 0 \<le> f n \<and> f n \<le> g n"
shows "a \<le> b"
@@ -982,9 +1056,9 @@
lemma prodinf_le_const:
fixes f :: "nat \<Rightarrow> real"
- assumes "convergent_prod f" "\<And>n. prod f {..<n} \<le> x"
+ assumes "convergent_prod f" "\<And>n. n \<ge> N \<Longrightarrow> prod f {..<n} \<le> x"
shows "prodinf f \<le> x"
- by (metis lessThan_Suc_atMost assms convergent_prod_LIMSEQ LIMSEQ_le_const2)
+ by (metis lessThan_Suc_atMost assms convergent_prod_LIMSEQ LIMSEQ_le_const2 atMost_iff lessThan_iff less_le)
lemma prodinf_eq_one_iff [simp]:
fixes f :: "nat \<Rightarrow> real"
@@ -1394,6 +1468,25 @@
shows "(\<Prod>n. f (Suc n)) = prodinf f / f 0"
using prodinf_split_initial_segment[of 1] assms by simp
+lemma has_prod_ignore_initial_segment':
+ assumes "convergent_prod f"
+ shows "f has_prod ((\<Prod>k<n. f k) * (\<Prod>k. f (k + n)))"
+proof (cases "\<exists>k<n. f k = 0")
+ case True
+ hence [simp]: "(\<Prod>k<n. f k) = 0"
+ by (meson finite_lessThan lessThan_iff prod_zero)
+ thus ?thesis using True assms
+ by (metis convergent_prod_has_prod_iff has_prod_zeroI mult_not_zero)
+next
+ case False
+ hence "(\<lambda>i. f (i + n)) has_prod (prodinf f / prod f {..<n})"
+ using assms by (intro has_prod_split_initial_segment) (auto simp: convergent_prod_has_prod_iff)
+ hence "prodinf f = prod f {..<n} * (\<Prod>k. f (k + n))"
+ using False by (simp add: has_prod_iff divide_simps mult_ac)
+ thus ?thesis
+ using assms by (simp add: convergent_prod_has_prod_iff)
+qed
+
end
context
@@ -1745,53 +1838,29 @@
assumes z: "summable (\<lambda>k. norm (z k))" and non0: "\<And>k. z k \<noteq> -1"
shows "convergent_prod (\<lambda>k. 1 + z k)"
proof -
- note if_cong [cong] power_Suc [simp del]
- obtain N where N: "\<And>k. k\<ge>N \<Longrightarrow> norm (z k) < 1/2"
+ obtain N where "\<And>k. k\<ge>N \<Longrightarrow> norm (z k) < 1/2"
using summable_LIMSEQ_zero [OF z]
by (metis diff_zero dist_norm half_gt_zero_iff less_numeral_extra(1) lim_sequentially tendsto_norm_zero_iff)
- have "norm (Ln (1 + z k)) \<le> 2 * norm (z k)" if "k \<ge> N" for k
- proof (cases "z k = 0")
- case False
- let ?f = "\<lambda>i. cmod ((- 1) ^ i * z k ^ i / of_nat (Suc i))"
- have normf: "norm (?f n) \<le> (1 / 2) ^ n" for n
- proof -
- have "norm (?f n) = cmod (z k) ^ n / cmod (1 + of_nat n)"
- by (auto simp: norm_divide norm_mult norm_power)
- also have "\<dots> \<le> cmod (z k) ^ n"
- by (auto simp: field_split_simps mult_le_cancel_left1 in_Reals_norm)
- also have "\<dots> \<le> (1 / 2) ^ n"
- using N [OF that] by (simp add: power_mono)
- finally show "norm (?f n) \<le> (1 / 2) ^ n" .
- qed
- have summablef: "summable ?f"
- by (intro normf summable_comparison_test' [OF summable_geometric [of "1/2"]]) auto
- have "(\<lambda>n. (- 1) ^ Suc n / of_nat n * z k ^ n) sums Ln (1 + z k)"
- using Ln_series [of "z k"] N that by fastforce
- then have *: "(\<lambda>i. z k * (((- 1) ^ i * z k ^ i) / (Suc i))) sums Ln (1 + z k)"
- using sums_split_initial_segment [where n= 1] by (force simp: power_Suc mult_ac)
- then have "norm (Ln (1 + z k)) = norm (suminf (\<lambda>i. z k * (((- 1) ^ i * z k ^ i) / (Suc i))))"
- using sums_unique by force
- also have "\<dots> = norm (z k * suminf (\<lambda>i. ((- 1) ^ i * z k ^ i) / (Suc i)))"
- apply (subst suminf_mult)
- using * False
- by (auto simp: sums_summable intro: summable_mult_D [of "z k"])
- also have "\<dots> = norm (z k) * norm (suminf (\<lambda>i. ((- 1) ^ i * z k ^ i) / (Suc i)))"
- by (simp add: norm_mult)
- also have "\<dots> \<le> norm (z k) * suminf (\<lambda>i. norm (((- 1) ^ i * z k ^ i) / (Suc i)))"
- by (intro mult_left_mono summable_norm summablef) auto
- also have "\<dots> \<le> norm (z k) * suminf (\<lambda>i. (1/2) ^ i)"
- by (intro mult_left_mono suminf_le) (use summable_geometric [of "1/2"] summablef normf in auto)
- also have "\<dots> \<le> norm (z k) * 2"
- using suminf_geometric [of "1/2::real"] by simp
- finally show ?thesis
- by (simp add: mult_ac)
- qed simp
then have "summable (\<lambda>k. Ln (1 + z k))"
- by (metis summable_comparison_test summable_mult z)
+ by (metis norm_Ln_le summable_comparison_test summable_mult z)
with non0 show ?thesis
by (simp add: add_eq_0_iff convergent_prod_iff_summable_complex)
qed
+corollary summable_imp_convergent_prod_real:
+ fixes z :: "nat \<Rightarrow> real"
+ assumes z: "summable (\<lambda>k. \<bar>z k\<bar>)" and non0: "\<And>k. z k \<noteq> -1"
+ shows "convergent_prod (\<lambda>k. 1 + z k)"
+proof -
+ have "\<And>k. (complex_of_real \<circ> z) k \<noteq> - 1"
+ by (metis non0 o_apply of_real_1 of_real_eq_iff of_real_minus)
+ with z
+ have "convergent_prod (\<lambda>k. 1 + (complex_of_real \<circ> z) k)"
+ by (auto intro: summable_imp_convergent_prod_complex)
+ then show ?thesis
+ using convergent_prod_of_real_iff [of "\<lambda>k. 1 + z k"] by (simp add: o_def)
+qed
+
lemma summable_Ln_complex:
fixes z :: "nat \<Rightarrow> complex"
assumes "convergent_prod z" "\<And>k. z k \<noteq> 0"
--- a/src/HOL/Analysis/Uniform_Limit.thy Tue Dec 20 09:34:37 2022 +0100
+++ b/src/HOL/Analysis/Uniform_Limit.thy Thu Dec 22 21:55:51 2022 +0100
@@ -198,6 +198,19 @@
unfolding uniformly_convergent_on_def assms(2) [symmetric]
by (intro iff_exI uniform_limit_cong eventually_mono [OF assms(1)]) auto
+lemma uniformly_convergent_on_compose:
+ assumes "uniformly_convergent_on A f"
+ assumes "filterlim g sequentially sequentially"
+ shows "uniformly_convergent_on A (\<lambda>n. f (g n))"
+proof -
+ from assms(1) obtain f' where "uniform_limit A f f' sequentially"
+ by (auto simp: uniformly_convergent_on_def)
+ hence "uniform_limit A (\<lambda>n. f (g n)) f' sequentially"
+ by (rule filterlim_compose) fact
+ thus ?thesis
+ by (auto simp: uniformly_convergent_on_def)
+qed
+
lemma uniformly_convergent_uniform_limit_iff:
"uniformly_convergent_on X f \<longleftrightarrow> uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially"
proof
@@ -308,6 +321,59 @@
ultimately show ?thesis by auto
qed
+lemma uniformly_convergent_on_sum_E:
+ fixes \<epsilon>::real and f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_space,real_normed_vector}"
+ assumes uconv: "uniformly_convergent_on K (\<lambda>n z. \<Sum>k<n. f k z)" and "\<epsilon>>0"
+ obtains N where "\<And>m n z. \<lbrakk>N \<le> m; m \<le> n; z\<in>K\<rbrakk> \<Longrightarrow> norm(\<Sum>k=m..<n. f k z) < \<epsilon>"
+proof -
+ obtain N where N: "\<And>m n z. \<lbrakk>N \<le> m; N \<le> n; z\<in>K\<rbrakk> \<Longrightarrow> dist (\<Sum>k<m. f k z) (\<Sum>k<n. f k z) < \<epsilon>"
+ using uconv \<open>\<epsilon>>0\<close> unfolding uniformly_Cauchy_on_def uniformly_convergent_eq_Cauchy by meson
+ show thesis
+ proof
+ fix m n z
+ assume "N \<le> m" "m \<le> n" "z \<in> K"
+ moreover have "(\<Sum>k = m..<n. f k z) = (\<Sum>k<n. f k z) - (\<Sum>k<m. f k z)"
+ by (metis atLeast0LessThan le0 sum_diff_nat_ivl \<open>m \<le> n\<close>)
+ ultimately show "norm(\<Sum>k = m..<n. f k z) < \<epsilon>"
+ using N by (simp add: dist_norm)
+ qed
+qed
+
+lemma uniformly_convergent_on_sum_iff:
+ fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_space,real_normed_vector}"
+ shows "uniformly_convergent_on K (\<lambda>n z. \<Sum>k<n. f k z)
+ \<longleftrightarrow> (\<forall>\<epsilon>>0. \<exists>N. \<forall>m n z. N\<le>m \<longrightarrow> m\<le>n \<longrightarrow> z\<in>K \<longrightarrow> norm (\<Sum>k=m..<n. f k z) < \<epsilon>)" (is "?lhs=?rhs")
+proof
+ assume R: ?rhs
+ show ?lhs
+ unfolding uniformly_Cauchy_on_def uniformly_convergent_eq_Cauchy
+ proof (intro strip)
+ fix \<epsilon>::real
+ assume "\<epsilon>>0"
+ then obtain N where "\<And>m n z. \<lbrakk>N \<le> m; m \<le> n; z\<in>K\<rbrakk> \<Longrightarrow> norm(\<Sum>k = m..<n. f k z) < \<epsilon>"
+ using R by blast
+ then have "\<forall>x\<in>K. \<forall>m\<ge>N. \<forall>n\<ge>m. norm ((\<Sum>k<m. f k x) - (\<Sum>k<n. f k x)) < \<epsilon>"
+ by (metis atLeast0LessThan le0 sum_diff_nat_ivl norm_minus_commute)
+ then have "\<forall>x\<in>K. \<forall>m\<ge>N. \<forall>n\<ge>N. norm ((\<Sum>k<m. f k x) - (\<Sum>k<n. f k x)) < \<epsilon>"
+ by (metis linorder_le_cases norm_minus_commute)
+ then show "\<exists>M. \<forall>x\<in>K. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (\<Sum>k<m. f k x) (\<Sum>k<n. f k x) < \<epsilon>"
+ by (metis dist_norm)
+ qed
+qed (metis uniformly_convergent_on_sum_E)
+
+lemma uniform_limit_suminf:
+ fixes f:: "nat \<Rightarrow> 'a::{metric_space, comm_monoid_add} \<Rightarrow> 'a"
+ assumes "uniformly_convergent_on X (\<lambda>n x. \<Sum>k<n. f k x)"
+ shows "uniform_limit X (\<lambda>n x. \<Sum>k<n. f k x) (\<lambda>x. \<Sum>k. f k x) sequentially"
+proof -
+ obtain S where S: "uniform_limit X (\<lambda>n x. \<Sum>k<n. f k x) S sequentially"
+ using assms uniformly_convergent_on_def by blast
+ then have "(\<Sum>k. f k x) = S x" if "x \<in> X" for x
+ using that sums_iff sums_def by (blast intro: tendsto_uniform_limitI [OF S])
+ with S show ?thesis
+ by (simp cong: uniform_limit_cong')
+qed
+
text \<open>TODO: remove explicit formulations
@{thm uniformly_convergent_eq_cauchy uniformly_cauchy_imp_uniformly_convergent}?!\<close>
@@ -316,6 +382,102 @@
unfolding uniformly_convergent_on_def convergent_def
by (auto dest: tendsto_uniform_limitI)
+subsection \<open>Comparison Test\<close>
+
+lemma uniformly_summable_comparison_test:
+ fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: banach"
+ assumes "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. g n x)"
+ assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> g n x"
+ shows "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. f n x)"
+proof -
+ have "uniformly_Cauchy_on A (\<lambda>N x. \<Sum>n<N. f n x)"
+ proof (rule uniformly_Cauchy_onI')
+ fix e :: real assume e: "e > 0"
+ obtain M where M: "\<And>x m n. x \<in> A \<Longrightarrow> m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> dist (\<Sum>k<m. g k x) (\<Sum>k<n. g k x) < e"
+ using assms(1) e unfolding uniformly_convergent_eq_Cauchy uniformly_Cauchy_on_def by metis
+ show "\<exists>M. \<forall>x\<in>A. \<forall>m\<ge>M. \<forall>n>m. dist (\<Sum>k<m. f k x) (\<Sum>k<n. f k x) < e"
+ proof (rule exI[of _ M], safe)
+ fix x m n assume xmn: "x \<in> A" "m \<ge> M" "m < n"
+ have nonneg: "g k x \<ge> 0" for k
+ by (rule order.trans[OF _ assms(2)]) (use xmn in auto)
+ have "dist (\<Sum>k<m. f k x) (\<Sum>k<n. f k x) = norm (\<Sum>k\<in>{..<n}-{..<m}. f k x)"
+ using xmn by (subst sum_diff) (auto simp: dist_norm norm_minus_commute)
+ also have "{..<n}-{..<m} = {m..<n}"
+ by auto
+ also have "norm (\<Sum>k\<in>{m..<n}. f k x) \<le> (\<Sum>k\<in>{m..<n}. norm (f k x))"
+ using norm_sum by blast
+ also have "\<dots> \<le> (\<Sum>k\<in>{m..<n}. g k x)"
+ by (intro sum_mono assms xmn)
+ also have "\<dots> = \<bar>\<Sum>k\<in>{m..<n}. g k x\<bar>"
+ by (subst abs_of_nonneg) (auto simp: nonneg intro!: sum_nonneg)
+ also have "{m..<n} = {..<n} - {..<m}"
+ by auto
+ also have "\<bar>\<Sum>k\<in>\<dots>. g k x\<bar> = dist (\<Sum>k<m. g k x) (\<Sum>k<n. g k x)"
+ using xmn by (subst sum_diff) (auto simp: abs_minus_commute dist_norm)
+ also have "\<dots> < e"
+ by (rule M) (use xmn in auto)
+ finally show "dist (\<Sum>k<m. f k x) (\<Sum>k<n. f k x) < e" .
+ qed
+ qed
+ thus ?thesis
+ unfolding uniformly_convergent_eq_Cauchy .
+qed
+
+lemma uniform_limit_compose_uniformly_continuous_on:
+ fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
+ assumes lim: "uniform_limit A g g' F"
+ assumes cont: "uniformly_continuous_on B f"
+ assumes ev: "eventually (\<lambda>x. \<forall>y\<in>A. g x y \<in> B) F" and "closed B"
+ shows "uniform_limit A (\<lambda>x y. f (g x y)) (\<lambda>y. f (g' y)) F"
+proof (cases "F = bot")
+ case [simp]: False
+ show ?thesis
+ unfolding uniform_limit_iff
+ proof safe
+ fix e :: real assume e: "e > 0"
+
+ have g'_in_B: "g' y \<in> B" if "y \<in> A" for y
+ proof (rule Lim_in_closed_set)
+ show "eventually (\<lambda>x. g x y \<in> B) F"
+ using ev by eventually_elim (use that in auto)
+ show "((\<lambda>x. g x y) \<longlongrightarrow> g' y) F"
+ using lim that by (metis tendsto_uniform_limitI)
+ qed (use \<open>closed B\<close> in auto)
+
+ obtain d where d: "d > 0" "\<And>x y. x \<in> B \<Longrightarrow> y \<in> B \<Longrightarrow> dist x y < d \<Longrightarrow> dist (f x) (f y) < e"
+ using e cont unfolding uniformly_continuous_on_def by metis
+ from lim have "eventually (\<lambda>x. \<forall>y\<in>A. dist (g x y) (g' y) < d) F"
+ unfolding uniform_limit_iff using \<open>d > 0\<close> by meson
+ thus "eventually (\<lambda>x. \<forall>y\<in>A. dist (f (g x y)) (f (g' y)) < e) F"
+ using assms(3)
+ proof eventually_elim
+ case (elim x)
+ show "\<forall>y\<in>A. dist (f (g x y)) (f (g' y)) < e"
+ proof safe
+ fix y assume y: "y \<in> A"
+ show "dist (f (g x y)) (f (g' y)) < e"
+ proof (rule d)
+ show "dist (g x y) (g' y) < d"
+ using elim y by blast
+ qed (use y elim g'_in_B in auto)
+ qed
+ qed
+ qed
+qed (auto simp: filterlim_def)
+
+lemma uniformly_convergent_on_compose_uniformly_continuous_on:
+ fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
+ assumes lim: "uniformly_convergent_on A g"
+ assumes cont: "uniformly_continuous_on B f"
+ assumes ev: "eventually (\<lambda>x. \<forall>y\<in>A. g x y \<in> B) sequentially" and "closed B"
+ shows "uniformly_convergent_on A (\<lambda>x y. f (g x y))"
+proof -
+ from lim obtain g' where g': "uniform_limit A g g' sequentially"
+ by (auto simp: uniformly_convergent_on_def)
+ thus ?thesis
+ using uniform_limit_compose_uniformly_continuous_on[OF g' cont ev \<open>closed B\<close>]
+ by (auto simp: uniformly_convergent_on_def)
+qed
subsection \<open>Weierstrass M-Test\<close>
--- a/src/HOL/Complex.thy Tue Dec 20 09:34:37 2022 +0100
+++ b/src/HOL/Complex.thy Thu Dec 22 21:55:51 2022 +0100
@@ -6,7 +6,7 @@
section \<open>Complex Numbers: Rectangular and Polar Representations\<close>
theory Complex
-imports Transcendental
+imports Transcendental Real_Vector_Spaces
begin
text \<open>
@@ -196,6 +196,12 @@
lemma Im_divide_of_nat [simp]: "Im (z / of_nat n) = Im z / of_nat n"
by (cases n) (simp_all add: Im_divide field_split_simps power2_eq_square del: of_nat_Suc)
+lemma Re_inverse [simp]: "r \<in> \<real> \<Longrightarrow> Re (inverse r) = inverse (Re r)"
+ by (metis Re_complex_of_real Reals_cases of_real_inverse)
+
+lemma Im_inverse [simp]: "r \<in> \<real> \<Longrightarrow> Im (inverse r) = 0"
+ by (metis Im_complex_of_real Reals_cases of_real_inverse)
+
lemma of_real_Re [simp]: "z \<in> \<real> \<Longrightarrow> of_real (Re z) = z"
by (auto simp: Reals_def)
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy Tue Dec 20 09:34:37 2022 +0100
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Thu Dec 22 21:55:51 2022 +0100
@@ -11,6 +11,8 @@
"HOL-Library.Multiset"
begin
+unbundle multiset.lifting
+
subsection \<open>Irreducible and prime elements\<close>
context comm_semiring_1
@@ -2257,4 +2259,7 @@
end
+lifting_update multiset.lifting
+lifting_forget multiset.lifting
+
end
--- a/src/HOL/Filter.thy Tue Dec 20 09:34:37 2022 +0100
+++ b/src/HOL/Filter.thy Thu Dec 22 21:55:51 2022 +0100
@@ -1519,6 +1519,24 @@
by eventually_elim (insert n, auto)
qed
+lemma filterlim_minus_const_nat_at_top:
+ "filterlim (\<lambda>n. n - c) sequentially sequentially"
+ unfolding filterlim_at_top
+proof
+ fix a :: nat
+ show "eventually (\<lambda>n. n - c \<ge> a) at_top"
+ using eventually_ge_at_top[of "a + c"] by eventually_elim auto
+qed
+
+lemma filterlim_add_const_nat_at_top:
+ "filterlim (\<lambda>n. n + c) sequentially sequentially"
+ unfolding filterlim_at_top
+proof
+ fix a :: nat
+ show "eventually (\<lambda>n. n + c \<ge> a) at_top"
+ using eventually_ge_at_top[of a] by eventually_elim auto
+qed
+
subsection \<open>Setup \<^typ>\<open>'a filter\<close> for lifting and transfer\<close>
lemma filtermap_id [simp, id_simps]: "filtermap id = id"
--- a/src/HOL/Fun.thy Tue Dec 20 09:34:37 2022 +0100
+++ b/src/HOL/Fun.thy Thu Dec 22 21:55:51 2022 +0100
@@ -300,11 +300,17 @@
using lin [of x y] ne by (force simp: dual_order.order_iff_strict)
qed
+lemma linorder_inj_onI':
+ fixes A :: "'a :: linorder set"
+ assumes "\<And>i j. i \<in> A \<Longrightarrow> j \<in> A \<Longrightarrow> i < j \<Longrightarrow> f i \<noteq> f j"
+ shows "inj_on f A"
+ by (intro linorder_inj_onI) (auto simp add: assms)
+
lemma linorder_injI:
assumes "\<And>x y::'a::linorder. x < y \<Longrightarrow> f x \<noteq> f y"
shows "inj f"
\<comment> \<open>Courtesy of Stephan Merz\<close>
-using assms by (auto intro: linorder_inj_onI linear)
+using assms by (simp add: linorder_inj_onI')
lemma inj_on_image_Pow: "inj_on f A \<Longrightarrow>inj_on (image f) (Pow A)"
unfolding Pow_def inj_on_def by blast
--- a/src/HOL/Library/Multiset.thy Tue Dec 20 09:34:37 2022 +0100
+++ b/src/HOL/Library/Multiset.thy Thu Dec 22 21:55:51 2022 +0100
@@ -4410,6 +4410,9 @@
lemma size_psubset: "M \<subseteq># M' \<Longrightarrow> size M < size M' \<Longrightarrow> M \<subset># M'"
using less_irrefl subset_mset_def by blast
+lifting_update multiset.lifting
+lifting_forget multiset.lifting
+
hide_const (open) wcount
end
--- a/src/HOL/Limits.thy Tue Dec 20 09:34:37 2022 +0100
+++ b/src/HOL/Limits.thy Thu Dec 22 21:55:51 2022 +0100
@@ -14,7 +14,7 @@
text \<open>Lemmas related to shifting/scaling\<close>
lemma range_add [simp]:
fixes a::"'a::group_add" shows "range ((+) a) = UNIV"
- by (metis add_minus_cancel surjI)
+ by simp
lemma range_diff [simp]:
fixes a::"'a::group_add" shows "range ((-) a) = UNIV"
@@ -1060,6 +1060,21 @@
shows "((\<lambda>i. prod (f i) I) \<longlongrightarrow> 1) F"
using tendsto_prod' [of I "\<lambda>x y. f y x" "\<lambda>x. 1"] assms by simp
+lemma LIMSEQ_prod_0:
+ fixes f :: "nat \<Rightarrow> 'a::{semidom,topological_space}"
+ assumes "f i = 0"
+ shows "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> 0"
+proof (subst tendsto_cong)
+ show "\<forall>\<^sub>F n in sequentially. prod f {..n} = 0"
+ using assms eventually_at_top_linorder by auto
+qed auto
+
+lemma LIMSEQ_prod_nonneg:
+ fixes f :: "nat \<Rightarrow> 'a::{linordered_semidom,linorder_topology}"
+ assumes 0: "\<And>n. 0 \<le> f n" and a: "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> a"
+ shows "a \<ge> 0"
+ by (simp add: "0" prod_nonneg LIMSEQ_le_const [OF a])
+
lemma continuous_prod' [continuous_intros]:
fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_mult"
shows "(\<And>i. i \<in> I \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Prod>i\<in>I. f i x)"
--- a/src/HOL/Relation.thy Tue Dec 20 09:34:37 2022 +0100
+++ b/src/HOL/Relation.thy Thu Dec 22 21:55:51 2022 +0100
@@ -393,6 +393,12 @@
lemma asymp_on_subset: "asymp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> asymp_on B R"
by (auto simp: asymp_on_def)
+lemma irrefl_on_if_asym_on[simp]: "asym_on A r \<Longrightarrow> irrefl_on A r"
+ by (auto intro: irrefl_onI dest: asym_onD)
+
+lemma irreflp_on_if_asymp_on[simp]: "asymp_on A r \<Longrightarrow> irreflp_on A r"
+ by (rule irrefl_on_if_asym_on[to_pred])
+
lemma (in preorder) asymp_on_less[simp]: "asymp_on A (<)"
by (auto intro: dual_order.asym)
--- a/src/HOL/Topological_Spaces.thy Tue Dec 20 09:34:37 2022 +0100
+++ b/src/HOL/Topological_Spaces.thy Thu Dec 22 21:55:51 2022 +0100
@@ -3440,7 +3440,7 @@
lemma uniformly_continuous_on_id[continuous_intros]: "uniformly_continuous_on s (\<lambda>x. x)"
by (auto simp: uniformly_continuous_on_uniformity filterlim_def)
-lemma uniformly_continuous_on_compose[continuous_intros]:
+lemma uniformly_continuous_on_compose:
"uniformly_continuous_on s g \<Longrightarrow> uniformly_continuous_on (g`s) f \<Longrightarrow>
uniformly_continuous_on s (\<lambda>x. f (g x))"
using filterlim_compose[of "\<lambda>(x, y). (f x, f y)" uniformity
--- a/src/Pure/GUI/gui_thread.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Pure/GUI/gui_thread.scala Thu Dec 22 21:55:51 2022 +0100
@@ -13,13 +13,15 @@
object GUI_Thread {
/* context check */
+ def check(): Boolean = SwingUtilities.isEventDispatchThread()
+
def assert[A](body: => A): A = {
- Predef.assert(SwingUtilities.isEventDispatchThread)
+ Predef.assert(check())
body
}
def require[A](body: => A): A = {
- Predef.require(SwingUtilities.isEventDispatchThread, "GUI thread expected")
+ Predef.require(check(), "GUI thread expected")
body
}
@@ -27,7 +29,7 @@
/* event dispatch queue */
def now[A](body: => A): A = {
- if (SwingUtilities.isEventDispatchThread) body
+ if (check()) body
else {
lazy val result = assert { Exn.capture(body) }
SwingUtilities.invokeAndWait(() => result)
@@ -36,12 +38,12 @@
}
def later(body: => Unit): Unit = {
- if (SwingUtilities.isEventDispatchThread) body
+ if (check()) body
else SwingUtilities.invokeLater(() => body)
}
def future[A](body: => A): Future[A] = {
- if (SwingUtilities.isEventDispatchThread) Future.value(body)
+ if (check()) Future.value(body)
else {
val promise = Future.promise[A]
later { promise.fulfill_result(Exn.capture(body)) }
--- a/src/Pure/ML/ml_console.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Pure/ML/ml_console.scala Thu Dec 22 21:55:51 2022 +0100
@@ -60,7 +60,7 @@
if (rc != Process_Result.RC.ok) sys.exit(rc)
}
- val background =
+ val session_background =
if (raw_ml_system) {
Sessions.Background(
base = Sessions.Base.bootstrap,
@@ -73,7 +73,7 @@
// process loop
val process =
- ML_Process(options, background, store,
+ ML_Process(store, options, session_background,
logic = logic, args = List("-i"), redirect = true,
modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
raw_ml_system = raw_ml_system)
--- a/src/Pure/ML/ml_process.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Pure/ML/ml_process.scala Thu Dec 22 21:55:51 2022 +0100
@@ -12,9 +12,10 @@
object ML_Process {
- def apply(options: Options,
+ def apply(
+ store: Sessions.Store,
+ options: Options,
session_background: Sessions.Background,
- store: Sessions.Store,
logic: String = "",
raw_ml_system: Boolean = false,
use_prelude: List[String] = Nil,
@@ -168,10 +169,10 @@
val more_args = getopts(args)
if (args.isEmpty || more_args.nonEmpty) getopts.usage()
+ val store = Sessions.store(options)
val session_background = Sessions.background(options, logic, dirs = dirs).check_errors
- val store = Sessions.store(options)
val result =
- ML_Process(options, session_background, store,
+ ML_Process(store, options, session_background,
logic = logic, args = eval_args, modes = modes).result(
progress_stdout = Output.writeln(_, stdout = true),
progress_stderr = Output.writeln(_))
--- a/src/Pure/PIDE/document.ML Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Pure/PIDE/document.ML Thu Dec 22 21:55:51 2022 +0100
@@ -85,12 +85,13 @@
val no_header: node_header =
{master = "", header = Thy_Header.make ("", Position.none) [] [], errors = []};
-val no_perspective = make_perspective (false, [], []);
+
+val empty_perspective = make_perspective (false, [], []);
val empty_node =
- make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Lazy.value ());
+ make_node (no_header, NONE, empty_perspective, Entries.empty, NONE, Lazy.value ());
-fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) =
+fun is_empty_perspective ({required, visible, visible_last, overlays}: perspective) =
not required andalso
Inttab.is_empty visible andalso
is_none visible_last andalso
@@ -99,7 +100,7 @@
fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidated}) =
header = no_header andalso
is_none keywords andalso
- is_no_perspective perspective andalso
+ is_empty_perspective perspective andalso
Entries.is_empty entries andalso
is_none result andalso
Lazy.is_finished consolidated;
--- a/src/Pure/PIDE/document.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Pure/PIDE/document.scala Thu Dec 22 21:55:51 2022 +0100
@@ -181,24 +181,23 @@
/* perspective */
- type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
- type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
-
- val no_perspective_text: Perspective_Text =
- Perspective(false, Text.Perspective.empty, Overlays.empty)
-
- val no_perspective_command: Perspective_Command =
- Perspective(false, Command.Perspective.empty, Overlays.empty)
+ object Perspective_Text {
+ type T = Perspective[Text.Edit, Text.Perspective]
+ val empty: T = Perspective(false, Text.Perspective.empty, Overlays.empty)
+ def is_empty(perspective: T): Boolean =
+ !perspective.required &&
+ perspective.visible.is_empty &&
+ perspective.overlays.is_empty
+ }
- def is_no_perspective_text(perspective: Perspective_Text): Boolean =
- !perspective.required &&
- perspective.visible.is_empty &&
- perspective.overlays.is_empty
-
- def is_no_perspective_command(perspective: Perspective_Command): Boolean =
- !perspective.required &&
- perspective.visible.is_empty &&
- perspective.overlays.is_empty
+ object Perspective_Command {
+ type T = Perspective[Command.Edit, Command.Perspective]
+ val empty: T = Perspective(false, Command.Perspective.empty, Overlays.empty)
+ def is_empty(perspective: T): Boolean =
+ !perspective.required &&
+ perspective.visible.is_empty &&
+ perspective.overlays.is_empty
+ }
/* commands */
@@ -272,14 +271,14 @@
val header: Node.Header = Node.no_header,
val syntax: Option[Outer_Syntax] = None,
val text_perspective: Text.Perspective = Text.Perspective.empty,
- val perspective: Node.Perspective_Command = Node.no_perspective_command,
+ val perspective: Node.Perspective_Command.T = Node.Perspective_Command.empty,
_commands: Node.Commands = Node.Commands.empty
) {
def is_empty: Boolean =
get_blob.isEmpty &&
header == Node.no_header &&
text_perspective.is_empty &&
- Node.is_no_perspective_command(perspective) &&
+ Node.Perspective_Command.is_empty(perspective) &&
commands.isEmpty
def has_header: Boolean = header != Node.no_header
@@ -304,7 +303,7 @@
def update_perspective(
new_text_perspective: Text.Perspective,
- new_perspective: Node.Perspective_Command): Node =
+ new_perspective: Node.Perspective_Command.T): Node =
new Node(get_blob, header, syntax, new_text_perspective, new_perspective, _commands)
def edit_perspective: Node.Edit[Text.Edit, Text.Perspective] =
@@ -312,7 +311,7 @@
def same_perspective(
other_text_perspective: Text.Perspective,
- other_perspective: Node.Perspective_Command): Boolean =
+ other_perspective: Node.Perspective_Command.T): Boolean =
text_perspective == other_text_perspective &&
perspective.required == other_perspective.required &&
perspective.visible.same(other_perspective.visible) &&
@@ -761,8 +760,7 @@
def get_text(range: Text.Range): Option[String]
- def get_required(document: Boolean): Boolean
- def node_required: Boolean = get_required(false) || get_required(true)
+ def node_required: Boolean
def get_blob: Option[Blob]
def bibtex_entries: List[Text.Info[String]]
@@ -770,7 +768,7 @@
def node_edits(
node_header: Node.Header,
text_edits: List[Text.Edit],
- perspective: Node.Perspective_Text
+ perspective: Node.Perspective_Text.T
): List[Edit_Text] = {
val edits: List[Node.Edit[Text.Edit, Text.Perspective]] =
get_blob match {
--- a/src/Pure/PIDE/document_editor.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Pure/PIDE/document_editor.scala Thu Dec 22 21:55:51 2022 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/PIDE/document_editor.scala
Author: Makarius
-Central resources for interactive document preparation.
+Central resources and configuration for interactive document preparation.
*/
package isabelle
@@ -32,24 +32,52 @@
override def echo(msg: String): Unit = { syslog += msg; delay.invoke() }
- def load(): Unit = GUI_Thread.require {
- val path = document_output().log
- val text = if (path.is_file) File.read(path) else ""
- GUI_Thread.later { delay.revoke(); update(text) }
+ def finish(text: String): Unit = GUI_Thread.require {
+ delay.revoke()
+ update(text)
}
GUI_Thread.later { update() }
}
- /* global state */
+ /* configuration state */
sealed case class State(
session_background: Option[Sessions.Background] = None,
+ selection: Set[Document.Node.Name] = Set.empty,
views: Set[AnyRef] = Set.empty,
) {
def is_active: Boolean = session_background.isDefined && views.nonEmpty
+ def is_required(name: Document.Node.Name): Boolean =
+ is_active && selection.contains(name) && all_document_theories.contains(name)
+
+ def required: List[Document.Node.Name] =
+ if (is_active) all_document_theories.filter(selection) else Nil
+
+ def all_document_theories: List[Document.Node.Name] =
+ session_background match {
+ case Some(background) => background.base.all_document_theories
+ case None => Nil
+ }
+
+ def active_document_theories: List[Document.Node.Name] =
+ if (is_active) all_document_theories else Nil
+
+ def select(
+ names: Iterable[Document.Node.Name],
+ set: Boolean = false,
+ toggle: Boolean = false
+ ): State = {
+ copy(selection =
+ names.foldLeft(selection) {
+ case (sel, name) =>
+ val b = if (toggle) !selection(name) else set
+ if (b) sel + name else sel - name
+ })
+ }
+
def register_view(id: AnyRef): State = copy(views = views + id)
def unregister_view(id: AnyRef): State = copy(views = views - id)
}
--- a/src/Pure/PIDE/document_status.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Pure/PIDE/document_status.scala Thu Dec 22 21:55:51 2022 +0100
@@ -97,10 +97,25 @@
/* node status */
object Node_Status {
+ val empty: Node_Status =
+ Node_Status(
+ is_suppressed = false,
+ unprocessed = 0,
+ running = 0,
+ warned = 0,
+ failed = 0,
+ finished = 0,
+ canceled = false,
+ terminated = false,
+ initialized = false,
+ finalized = false,
+ consolidated = false)
+
def make(
state: Document.State,
version: Document.Version,
- name: Document.Node.Name): Node_Status = {
+ name: Document.Node.Name
+ ): Node_Status = {
val node = version.nodes(name)
var unprocessed = 0
@@ -156,6 +171,8 @@
finalized: Boolean,
consolidated: Boolean
) {
+ def is_empty: Boolean = this == Node_Status.empty
+
def ok: Boolean = failed == 0
def total: Int = unprocessed + running + warned + failed + finished
@@ -229,11 +246,12 @@
def apply(name: Document.Node.Name): Node_Status = rep(name)
def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
- def present: List[(Document.Node.Name, Node_Status)] =
- (for {
- name <- nodes.topological_order.iterator
- node_status <- get(name)
- } yield (name, node_status)).toList
+ def present(
+ domain: Option[List[Document.Node.Name]] = None
+ ): List[(Document.Node.Name, Node_Status)] = {
+ for (name <- domain.getOrElse(nodes.topological_order))
+ yield name -> get(name).getOrElse(Node_Status.empty)
+ }
def quasi_consolidated(name: Document.Node.Name): Boolean =
rep.get(name) match {
--- a/src/Pure/PIDE/editor.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Pure/PIDE/editor.scala Thu Dec 22 21:55:51 2022 +0100
@@ -20,16 +20,42 @@
protected val document_editor: Synchronized[Document_Editor.State] =
Synchronized(Document_Editor.State())
- def document_editor_session: Option[Sessions.Background] =
- document_editor.value.session_background
- def document_editor_active: Boolean =
- document_editor.value.is_active
- def document_editor_setup(background: Option[Sessions.Background]): Unit =
- document_editor.change(_.copy(session_background = background))
- def document_editor_init(id: AnyRef): Unit =
- document_editor.change(_.register_view(id))
- def document_editor_exit(id: AnyRef): Unit =
- document_editor.change(_.unregister_view(id))
+ protected def document_state(): Document_Editor.State = document_editor.value
+
+ protected def document_state_changed(): Unit = {}
+ private def document_state_change(f: Document_Editor.State => Document_Editor.State): Unit = {
+ val changed =
+ document_editor.change_result { st =>
+ val st1 = f(st)
+ val changed =
+ st.active_document_theories != st1.active_document_theories ||
+ st.required != st1.required
+ (changed, st1)
+ }
+ if (changed) document_state_changed()
+ }
+
+ def document_session(): Option[Sessions.Background] = document_state().session_background
+ def document_required(): List[Document.Node.Name] = document_state().required
+ def document_node_required(name: Document.Node.Name): Boolean = document_state().is_required(name)
+
+ def document_theories(): List[Document.Node.Name] = document_state().active_document_theories
+ def document_selection(): Set[Document.Node.Name] = document_state().selection
+
+ def document_setup(background: Option[Sessions.Background]): Unit =
+ document_state_change(_.copy(session_background = background))
+
+ def document_select(
+ names: Iterable[Document.Node.Name],
+ set: Boolean = false,
+ toggle: Boolean = false
+ ): Unit = document_state_change(_.select(names, set = set, toggle = toggle))
+
+ def document_select_all(set: Boolean = false): Unit =
+ document_state_change(st => st.select(st.active_document_theories, set = set))
+
+ def document_init(id: AnyRef): Unit = document_state_change(_.register_view(id))
+ def document_exit(id: AnyRef): Unit = document_state_change(_.unregister_view(id))
/* current situation */
--- a/src/Pure/PIDE/headless.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Pure/PIDE/headless.scala Thu Dec 22 21:55:51 2022 +0100
@@ -390,8 +390,9 @@
val theory_progress =
(for {
- (name, node_status) <- st1.nodes_status.present.iterator
- if changed_st.changed_nodes(name) && !st.already_committed.isDefinedAt(name)
+ (name, node_status) <- st1.nodes_status.present().iterator
+ if !node_status.is_empty && changed_st.changed_nodes(name) &&
+ !st.already_committed.isDefinedAt(name)
p1 = node_status.percentage
if p1 > 0 && !st.nodes_status.get(name).map(_.percentage).contains(p1)
} yield Progress.Theory(name.theory, percentage = Some(p1))).toList
@@ -471,7 +472,7 @@
) {
override def toString: String = node_name.toString
- def node_perspective: Document.Node.Perspective_Text =
+ def node_perspective: Document.Node.Perspective_Text.T =
Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
@@ -621,7 +622,7 @@
val session = new Session(session_name, options, resources)
progress.echo("Starting session " + session_name + " ...")
- Isabelle_Process.start(session, options, session_background, store,
+ Isabelle_Process.start(store, options, session, session_background,
logic = session_name, modes = print_mode).await_startup()
session
--- a/src/Pure/System/isabelle_process.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Pure/System/isabelle_process.scala Thu Dec 22 21:55:51 2022 +0100
@@ -13,10 +13,10 @@
object Isabelle_Process {
def start(
- session: Session,
+ store: Sessions.Store,
options: Options,
+ session: Session,
session_background: Sessions.Background,
- store: Sessions.Store,
logic: String = "",
raw_ml_system: Boolean = false,
use_prelude: List[String] = Nil,
@@ -28,10 +28,11 @@
val channel = System_Channel()
val process =
try {
- val channel_options =
- options.string.update("system_channel_address", channel.address).
+ val ml_options =
+ options.
+ string.update("system_channel_address", channel.address).
string.update("system_channel_password", channel.password)
- ML_Process(channel_options, session_background, store,
+ ML_Process(store, ml_options, session_background,
logic = logic, raw_ml_system = raw_ml_system,
use_prelude = use_prelude, eval_main = eval_main,
modes = modes, cwd = cwd, env = env)
--- a/src/Pure/Thy/document_build.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Pure/Thy/document_build.scala Thu Dec 22 21:55:51 2022 +0100
@@ -115,10 +115,11 @@
options: Options,
session: String,
dirs: List[Path] = Nil,
- progress: Progress = new Progress
+ progress: Progress = new Progress,
+ verbose: Boolean = false
): Sessions.Background = {
Sessions.load_structure(options + "document=pdf", dirs = dirs).
- selection_deps(Sessions.Selection.session(session), progress = progress).
+ selection_deps(Sessions.Selection.session(session), progress = progress, verbose = verbose).
background(session)
}
@@ -134,13 +135,15 @@
def context(
session_context: Export.Session_Context,
document_session: Option[Sessions.Base] = None,
+ document_selection: Document.Node.Name => Boolean = _ => true,
progress: Progress = new Progress
- ): Context = new Context(session_context, document_session, progress)
+ ): Context = new Context(session_context, document_session, document_selection, progress)
final class Context private[Document_Build](
val session_context: Export.Session_Context,
document_session: Option[Sessions.Base],
- val progress: Progress = new Progress
+ document_selection: Document.Node.Name => Boolean,
+ val progress: Progress
) {
context =>
@@ -186,8 +189,12 @@
for (name <- all_document_theories)
yield {
val path = Path.basic(tex_name(name))
- val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
- val content = YXML.parse_body(entry.text)
+ val content =
+ if (document_selection(name)) {
+ val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
+ YXML.parse_body(entry.text)
+ }
+ else Nil
File.content(path, content)
}
@@ -312,12 +319,12 @@
val result_pdf = doc_dir + root_pdf
if (errors.nonEmpty) {
- val errors1 = errors ::: List("Failed to build document " + quote(doc.name))
- throw new Build_Error(log, Exn.cat_message(errors1: _*))
+ val message = "Failed to build document " + quote(doc.name)
+ throw new Build_Error(log, errors ::: List(message))
}
else if (!result_pdf.is_file) {
val message = "Bad document result: expected to find " + root_pdf
- throw new Build_Error(log, message)
+ throw new Build_Error(log, List(message))
}
else {
val log_xz = Bytes(cat_lines(log)).compress()
@@ -389,8 +396,15 @@
watchdog = Time.seconds(0.5))
val log = result.out_lines ::: result.err_lines
- val errors = (if (result.ok) Nil else List(result.err)) ::: directory.log_errors()
- directory.make_document(log, errors)
+ val err = result.err
+
+ val errors1 = directory.log_errors()
+ val errors2 =
+ if (result.ok) errors1
+ else if (err.nonEmpty) err :: errors1
+ else if (errors1.nonEmpty) errors1
+ else List("Error")
+ directory.make_document(log, errors2)
}
}
@@ -422,8 +436,8 @@
def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex"
- class Build_Error(val log_lines: List[String], val message: String)
- extends Exn.User_Error(message)
+ class Build_Error(val log_lines: List[String], val log_errors: List[String])
+ extends Exn.User_Error(Exn.cat_message(log_errors: _*))
def build_documents(
context: Context,
@@ -525,8 +539,8 @@
progress.echo_warning("No output directory")
}
- val background = session_background(options, session, dirs = dirs)
- using(Export.open_session_context(build_results.store, background)) {
+ val session_background = Document_Build.session_background(options, session, dirs = dirs)
+ using(Export.open_session_context(build_results.store, session_background)) {
session_context =>
build_documents(
context(session_context, progress = progress),
--- a/src/Pure/Thy/sessions.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Pure/Thy/sessions.scala Thu Dec 22 21:55:51 2022 +0100
@@ -112,6 +112,7 @@
infos: List[Info] = Nil
) {
def session_name: String = base.session_name
+ def info: Info = sessions_structure(session_name)
def check_errors: Background =
if (errors.isEmpty) this
--- a/src/Pure/Thy/thy_syntax.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Thu Dec 22 21:55:51 2022 +0100
@@ -258,7 +258,7 @@
case (name, Document.Node.Perspective(required, text_perspective, overlays)) =>
val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays)
- val perspective: Document.Node.Perspective_Command =
+ val perspective: Document.Node.Perspective_Command.T =
Document.Node.Perspective(required, visible_overlay, overlays)
if (node.same_perspective(text_perspective, perspective)) node
else {
--- a/src/Pure/Tools/build_job.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Pure/Tools/build_job.scala Thu Dec 22 21:55:51 2022 +0100
@@ -447,7 +447,7 @@
val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
val process =
- Isabelle_Process.start(session, options, session_background, store,
+ Isabelle_Process.start(store, options, session, session_background,
logic = parent, raw_ml_system = is_pure,
use_prelude = use_prelude, eval_main = eval_main,
cwd = info.dir.file, env = env)
@@ -500,7 +500,7 @@
else (Nil, Nil)
}
catch {
- case exn: Document_Build.Build_Error => (exn.log_lines, List(exn.message))
+ case exn: Document_Build.Build_Error => (exn.log_lines, exn.log_errors)
case Exn.Interrupt.ERROR(msg) => (Nil, List(msg))
}
--- a/src/Pure/Tools/server.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Pure/Tools/server.scala Thu Dec 22 21:55:51 2022 +0100
@@ -269,7 +269,7 @@
override def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {
val json =
- for ((name, node_status) <- nodes_status.present)
+ for ((name, node_status) <- nodes_status.present() if !node_status.is_empty)
yield name.json + ("status" -> node_status.json)
context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
}
--- a/src/Tools/VSCode/src/language_server.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Tools/VSCode/src/language_server.scala Thu Dec 22 21:55:51 2022 +0100
@@ -307,7 +307,7 @@
dynamic_output.init()
try {
- Isabelle_Process.start(session, options, session_background, store,
+ Isabelle_Process.start(store, options, session, session_background,
modes = modes, logic = session_background.session_name).await_startup()
reply_ok(
"Welcome to Isabelle/" + session_background.session_name +
--- a/src/Tools/VSCode/src/vscode_model.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala Thu Dec 22 21:55:51 2022 +0100
@@ -59,7 +59,7 @@
node_name: Document.Node.Name
): VSCode_Model = {
VSCode_Model(session, editor, node_name, Content.empty,
- theory_required = File_Format.registry.is_theory(node_name))
+ node_required = File_Format.registry.is_theory(node_name))
}
}
@@ -70,21 +70,14 @@
content: VSCode_Model.Content,
version: Option[Long] = None,
external_file: Boolean = false,
- theory_required: Boolean = false,
- document_required: Boolean = false,
- last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
+ node_required: Boolean = false,
+ last_perspective: Document.Node.Perspective_Text.T = Document.Node.Perspective_Text.empty,
pending_edits: List[Text.Edit] = Nil,
published_diagnostics: List[Text.Info[Command.Results]] = Nil,
published_decorations: List[VSCode_Model.Decoration] = Nil
) extends Document.Model {
model =>
- /* required */
-
- def get_required(document: Boolean): Boolean =
- if (document) document_required else theory_required
-
-
/* content */
def get_text(range: Text.Range): Option[String] = content.doc.get_text(range)
@@ -111,10 +104,12 @@
def node_perspective(
doc_blobs: Document.Blobs,
caret: Option[Line.Position]
- ): (Boolean, Document.Node.Perspective_Text) = {
+ ): (Boolean, Document.Node.Perspective_Text.T) = {
if (is_theory) {
val snapshot = model.snapshot()
+ val required = node_required || editor.document_node_required(node_name)
+
val caret_perspective = resources.options.int("vscode_caret_perspective") max 0
val caret_range =
if (caret_perspective != 0) {
@@ -142,9 +137,9 @@
val overlays = editor.node_overlays(node_name)
(snapshot.node.load_commands_changed(doc_blobs),
- Document.Node.Perspective(node_required, text_perspective, overlays))
+ Document.Node.Perspective(required, text_perspective, overlays))
}
- else (false, Document.Node.no_perspective_text)
+ else (false, Document.Node.Perspective_Text.empty)
}
--- a/src/Tools/VSCode/src/vscode_resources.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Thu Dec 22 21:55:51 2022 +0100
@@ -206,7 +206,10 @@
state.change_result { st =>
val stable_tip_version = session.stable_tip_version(st.models)
- val thy_files = resources.resolve_dependencies(st.models, Nil)
+ val thy_files =
+ resources.resolve_dependencies(st.models,
+ editor.document_required().map((_, Position.none)))
+
val aux_files = stable_tip_version.toList.flatMap(undefined_blobs)
val loaded_models =
--- a/src/Tools/jEdit/src/document_dockable.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala Thu Dec 22 21:55:51 2022 +0100
@@ -27,10 +27,6 @@
val FINISHED = Value("finished")
}
- sealed case class Result(output: List[XML.Tree] = Nil) {
- def failed: Boolean = output.exists(Protocol.is_error)
- }
-
object State {
def init(): State = State()
}
@@ -44,8 +40,10 @@
def run(progress: Progress, process: Future[Unit]): State =
copy(progress = progress, process = process, status = Status.RUNNING)
- def finish(result: Result): State = State(output = result.output)
- def finish(msg: XML.Tree): State = finish(Result(output = List(msg)))
+ def finish(output: List[XML.Tree]): State =
+ copy(process = Future.value(()), status = Status.FINISHED, output = output)
+
+ def ok: Boolean = !output.exists(Protocol.is_error)
}
}
@@ -121,73 +119,119 @@
/* document build process */
- private def cancel(): Unit =
- current_state.change { st => st.process.cancel(); st }
-
private def init_state(): Unit =
current_state.change { _ => Document_Dockable.State(progress = log_progress()) }
+ private def cancel_process(): Unit =
+ current_state.change { st => st.process.cancel(); st }
+
+ private def await_process(): Unit =
+ current_state.guarded_access(st => if (st.process.is_finished) None else Some((), st))
+
+ private def finish_process(output: List[XML.Tree]): Unit =
+ current_state.change(_.finish(output))
+
+ private def run_process(body: Document_Editor.Log_Progress => Unit): Boolean = {
+ val started =
+ current_state.change_result { st =>
+ if (st.process.is_finished) {
+ val progress = log_progress()
+ val process =
+ Future.thread[Unit](name = "Document_Dockable.process") {
+ await_process()
+ body(progress)
+ }
+ (true, st.run(progress, process))
+ }
+ else (false, st)
+ }
+ show_state()
+ started
+ }
+
private def load_document(session: String): Boolean = {
- current_state.change_result { st =>
- if (st.process.is_finished) {
- val options = PIDE.options.value
- val progress = log_progress()
- val process =
- Future.thread[Unit](name = "Document_Dockable.load_document") {
- try {
- val session_background =
- Document_Build.session_background(
- options, session, dirs = JEdit_Sessions.session_dirs)
- PIDE.editor.document_editor_setup(Some(session_background))
- GUI_Thread.later { show_state(); show_page(theories_page) }
- }
- catch {
- case exn: Throwable if !Exn.is_interrupt(exn) =>
- current_state.change(_.finish(Protocol.error_message(Exn.message(exn))))
- GUI_Thread.later { show_state(); show_page(output_page) }
- }
+ val options = PIDE.options.value
+ run_process { _ =>
+ try {
+ val session_background =
+ Document_Build.session_background(
+ options, session, dirs = JEdit_Sessions.session_dirs)
+ PIDE.editor.document_setup(Some(session_background))
+
+ finish_process(Nil)
+ GUI_Thread.later {
+ refresh_theories()
+ show_state()
+ show_page(theories_page)
+ }
+ }
+ catch {
+ case exn: Throwable if !Exn.is_interrupt(exn) =>
+ finish_process(List(Protocol.error_message(Exn.print(exn))))
+ GUI_Thread.later {
+ show_state()
+ show_page(output_page)
}
- (true, st.run(progress, process))
}
- else (false, st)
}
}
+ private def document_build(
+ session_background: Sessions.Background,
+ progress: Document_Editor.Log_Progress
+ ): Unit = {
+ val store = JEdit_Sessions.sessions_store(PIDE.options.value)
+ val document_selection = PIDE.editor.document_selection()
+
+ val snapshot = PIDE.session.await_stable_snapshot()
+ val session_context =
+ Export.open_session_context(store, PIDE.resources.session_background,
+ document_snapshot = Some(snapshot))
+ try {
+ val context =
+ Document_Build.context(session_context,
+ document_session = Some(session_background.base),
+ document_selection = document_selection,
+ progress = progress)
+ val variant = session_background.info.documents.head
+
+ Isabelle_System.make_directory(Document_Editor.document_output_dir())
+ val doc = context.build_document(variant, verbose = true)
+
+ // log
+ File.write(Document_Editor.document_output().log, doc.log)
+ GUI_Thread.later { progress.finish(doc.log) }
+
+ // pdf
+ Bytes.write(Document_Editor.document_output().pdf, doc.pdf)
+ Document_Editor.view_document()
+ }
+ finally { session_context.close() }
+ }
+
private def build_document(): Unit = {
- current_state.change { st =>
- if (st.process.is_finished) {
- val progress = log_progress()
- val process =
- Future.thread[Unit](name = "Document_Dockable.build_document") {
- show_page(theories_page)
- Time.seconds(2.0).sleep()
+ PIDE.editor.document_session() match {
+ case Some(session_background) if session_background.info.documents.nonEmpty =>
+ run_process { progress =>
+ show_page(log_page)
+ val result = Exn.capture { document_build(session_background, progress) }
+ val msgs =
+ result match {
+ case Exn.Res(_) =>
+ List(Protocol.writeln_message("OK"))
+ case Exn.Exn(exn: Document_Build.Build_Error) =>
+ exn.log_errors.map(s => Protocol.error_message(YXML.parse_body(s)))
+ case Exn.Exn(exn) =>
+ List(Protocol.error_message(YXML.parse_body(Exn.print(exn))))
+ }
- show_page(log_page)
- val res =
- Exn.capture {
- progress.echo("Start " + Date.now())
- for (i <- 1 to 200) {
- progress.echo("message " + i)
- Time.seconds(0.1).sleep()
- }
- progress.echo("Stop " + Date.now())
- }
- val msg =
- res match {
- case Exn.Res(_) => Protocol.writeln_message("OK")
- case Exn.Exn(exn) => Protocol.error_message(Exn.message(exn))
- }
- current_state.change(_.finish(msg))
- show_state()
+ finish_process(Pretty.separate(msgs))
- show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page)
- GUI_Thread.later { progress.load() }
- }
- st.run(progress, process)
- }
- else st
+ show_state()
+ show_page(if (Exn.is_interrupt_exn(result)) theories_page else output_page)
+ }
+ case _ =>
}
- show_state()
}
@@ -205,6 +249,12 @@
document_session.reactions += { case SelectionChanged(_) => delay_load.invoke() }
+ private val load_button =
+ new GUI.Button("Load") {
+ tooltip = "Load document theories"
+ override def clicked(): Unit = PIDE.editor.document_select_all(set = true)
+ }
+
private val build_button =
new GUI.Button("<html><b>Build</b></html>") {
tooltip = "Build document"
@@ -214,7 +264,7 @@
private val cancel_button =
new GUI.Button("Cancel") {
tooltip = "Cancel build process"
- override def clicked(): Unit = cancel()
+ override def clicked(): Unit = cancel_process()
}
private val view_button =
@@ -224,8 +274,8 @@
}
private val controls =
- Wrap_Panel(List(document_session, process_indicator.component, build_button,
- view_button, cancel_button))
+ Wrap_Panel(List(document_session, process_indicator.component, load_button,
+ build_button, view_button, cancel_button))
add(controls.peer, BorderLayout.NORTH)
@@ -234,10 +284,31 @@
/* message pane with pages */
+ private val reset_button =
+ new GUI.Button("Reset") {
+ tooltip = "Deselect document theories"
+ override def clicked(): Unit = PIDE.editor.document_select_all(set = false)
+ }
+
+ private val purge_button = new GUI.Button("Purge") {
+ tooltip = "Remove theories that are no longer required"
+ override def clicked(): Unit = PIDE.editor.purge()
+ }
+
+ private val theories_controls =
+ Wrap_Panel(List(reset_button, purge_button))
+
private val theories = new Theories_Status(view, document = true)
+ private def refresh_theories(): Unit = {
+ val domain = PIDE.editor.document_theories().toSet
+ theories.update(domain = Some(domain), trim = true, force = true)
+ theories.refresh()
+ }
+
private val theories_page =
new TabbedPane.Page("Theories", new BorderPanel {
+ layout(theories_controls) = BorderPanel.Position.North
layout(theories.gui) = BorderPanel.Position.Center
}, "Selection and status of document theories")
@@ -268,20 +339,20 @@
GUI_Thread.later {
document_session.load()
handle_resize()
- theories.reinit()
+ refresh_theories()
}
case changed: Session.Commands_Changed =>
GUI_Thread.later {
- theories.update(domain = Some(changed.nodes), trim = changed.assignment)
+ val domain = PIDE.editor.document_theories().filter(changed.nodes).toSet
+ if (domain.nonEmpty) theories.update(domain = Some(domain))
}
}
override def init(): Unit = {
- PIDE.editor.document_editor_init(dockable)
+ PIDE.editor.document_init(dockable)
init_state()
PIDE.session.global_options += main
PIDE.session.commands_changed += main
- theories.update()
handle_resize()
delay_load.invoke()
}
@@ -290,6 +361,6 @@
PIDE.session.global_options -= main
PIDE.session.commands_changed -= main
delay_resize.revoke()
- PIDE.editor.document_editor_exit(dockable)
+ PIDE.editor.document_exit(dockable)
}
}
--- a/src/Tools/jEdit/src/document_model.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Thu Dec 22 21:55:51 2022 +0100
@@ -182,15 +182,14 @@
/* required nodes */
- def required_nodes(document: Boolean): Set[Document.Node.Name] =
+ def nodes_required(): Set[Document.Node.Name] =
(for {
(node_name, model) <- state.value.models.iterator
- if model.get_required(document)
+ if model.node_required
} yield node_name).toSet
def node_required(
name: Document.Node.Name,
- document: Boolean = false,
toggle: Boolean = false,
set: Boolean = false
) : Unit = {
@@ -201,30 +200,26 @@
st.models.get(name) match {
case None => (false, st)
case Some(model) =>
- val a = model.get_required(document)
+ val a = model.node_required
val b = if (toggle) !a else set
model match {
case m: File_Model if a != b =>
- (true, st.copy(models = st.models + (name -> m.set_required(document, b))))
+ (true, st.copy(models = st.models + (name -> m.set_node_required(b))))
case m: Buffer_Model if a != b =>
- m.set_required(document, b); (true, st)
+ m.set_node_required(b); (true, st)
case _ => (false, st)
}
})
- if (changed) {
- PIDE.plugin.options_changed()
- PIDE.editor.flush()
- }
+ if (changed) PIDE.editor.state_changed()
}
def view_node_required(
view: View,
- document: Boolean = false,
toggle: Boolean = false,
set: Boolean = false
): Unit =
Document_Model.get(view.getBuffer).foreach(model =>
- node_required(model.node_name, document = document, toggle = toggle, set = set))
+ node_required(model.node_name, toggle = toggle, set = set))
/* flushed edits */
@@ -340,12 +335,14 @@
def node_perspective(
doc_blobs: Document.Blobs,
hidden: Boolean
- ): (Boolean, Document.Node.Perspective_Text) = {
+ ): (Boolean, Document.Node.Perspective_Text.T) = {
GUI_Thread.require {}
if (JEdit_Options.continuous_checking() && is_theory) {
val snapshot = this.snapshot()
+ val required = node_required || PIDE.editor.document_node_required(node_name)
+
val reparse = snapshot.node.load_commands_changed(doc_blobs)
val perspective =
if (hidden) Text.Perspective.empty
@@ -356,9 +353,9 @@
}
val overlays = PIDE.editor.node_overlays(node_name)
- (reparse, Document.Node.Perspective(node_required, perspective, overlays))
+ (reparse, Document.Node.Perspective(required, perspective, overlays))
}
- else (false, Document.Node.no_perspective_text)
+ else (false, Document.Node.Perspective_Text.empty)
}
@@ -377,23 +374,21 @@
object File_Model {
def empty(session: Session): File_Model =
File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
- false, false, Document.Node.no_perspective_text, Nil)
+ false, Document.Node.Perspective_Text.empty, Nil)
def init(session: Session,
node_name: Document.Node.Name,
text: String,
- theory_required: Boolean = false,
- document_required: Boolean = false,
- last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
+ node_required: Boolean = false,
+ last_perspective: Document.Node.Perspective_Text.T = Document.Node.Perspective_Text.empty,
pending_edits: List[Text.Edit] = Nil
): File_Model = {
val file = JEdit_Lib.check_file(node_name.node)
file.foreach(PIDE.plugin.file_watcher.register_parent(_))
val content = Document_Model.File_Content(text)
- val theory_required1 = theory_required || File_Format.registry.is_theory(node_name)
- File_Model(session, node_name, file, content, theory_required1, document_required,
- last_perspective, pending_edits)
+ val node_required1 = node_required || File_Format.registry.is_theory(node_name)
+ File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits)
}
}
@@ -402,18 +397,13 @@
node_name: Document.Node.Name,
file: Option[JFile],
content: Document_Model.File_Content,
- theory_required: Boolean,
- document_required: Boolean,
- last_perspective: Document.Node.Perspective_Text,
+ node_required: Boolean,
+ last_perspective: Document.Node.Perspective_Text.T,
pending_edits: List[Text.Edit]
) extends Document_Model {
/* required */
- def get_required(document: Boolean): Boolean =
- if (document) document_required else theory_required
-
- def set_required(document: Boolean, b: Boolean): File_Model =
- if (document) copy(document_required = b) else copy(theory_required = b)
+ def set_node_required(b: Boolean): File_Model = copy(node_required = b)
/* text */
@@ -469,10 +459,10 @@
def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] =
if (pending_edits.nonEmpty ||
!File_Format.registry.is_theory(node_name) &&
- (node_required || !Document.Node.is_no_perspective_text(last_perspective))) None
+ (node_required || !Document.Node.Perspective_Text.is_empty(last_perspective))) None
else {
val text_edits = List(Text.Edit.remove(0, content.text))
- Some(node_edits(Document.Node.no_header, text_edits, Document.Node.no_perspective_text))
+ Some(node_edits(Document.Node.no_header, text_edits, Document.Node.Perspective_Text.empty))
}
@@ -505,13 +495,9 @@
/* perspective */
// owned by GUI thread
- private var _theory_required = false
- private var _document_required = false
-
- def get_required(document: Boolean): Boolean =
- if (document) _document_required else _theory_required
- def set_required(document: Boolean, b: Boolean): Unit =
- GUI_Thread.require { if (document) _document_required = b else _theory_required = b }
+ private var _node_required = false
+ def node_required: Boolean = _node_required
+ def set_node_required(b: Boolean): Unit = GUI_Thread.require { _node_required = b }
def document_view_iterator: Iterator[Document_View] =
for {
@@ -586,12 +572,12 @@
private object pending_edits {
private val pending = new mutable.ListBuffer[Text.Edit]
- private var last_perspective = Document.Node.no_perspective_text
+ private var last_perspective = Document.Node.Perspective_Text.empty
def nonEmpty: Boolean = synchronized { pending.nonEmpty }
def get_edits: List[Text.Edit] = synchronized { pending.toList }
- def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective }
- def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit =
+ def get_last_perspective: Document.Node.Perspective_Text.T = synchronized { last_perspective }
+ def set_last_perspective(perspective: Document.Node.Perspective_Text.T): Unit =
synchronized { last_perspective = perspective }
def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
@@ -683,8 +669,7 @@
case None =>
pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
case Some(file_model) =>
- set_required(false, file_model.theory_required)
- set_required(true, file_model.document_required)
+ set_node_required(file_model.node_required)
pending_edits.set_last_perspective(file_model.last_perspective)
pending_edits.edit(
file_model.pending_edits :::
@@ -707,8 +692,7 @@
init_token_marker()
File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer),
- theory_required = _theory_required,
- document_required = _document_required,
+ node_required = _node_required,
last_perspective = pending_edits.get_last_perspective,
pending_edits = pending_edits.get_edits)
}
--- a/src/Tools/jEdit/src/jedit_editor.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Thu Dec 22 21:55:51 2022 +0100
@@ -53,6 +53,17 @@
} yield doc_view.model.node_name).contains(name)
+ /* global changes */
+
+ def state_changed(): Unit = {
+ GUI_Thread.later { flush() }
+ PIDE.plugin.deps_changed()
+ session.global_options.post(Session.Global_Options(PIDE.options.value))
+ }
+
+ override def document_state_changed(): Unit = state_changed()
+
+
/* current situation */
override def current_node(view: View): Option[Document.Node.Name] =
--- a/src/Tools/jEdit/src/jedit_sessions.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Thu Dec 22 21:55:51 2022 +0100
@@ -43,6 +43,9 @@
Sessions.load_structure(session_options(options), dirs = dirs)
}
+ def sessions_store(options: Options): Sessions.Store =
+ Sessions.store(session_options(options))
+
/* raw logic info */
@@ -141,18 +144,17 @@
infos = PIDE.resources.session_background.infos).rc
}
- def session_start(options0: Options): Unit = {
+ def session_start(options: Options): Unit = {
val session = PIDE.session
- val options = session_options(options0)
val session_background = PIDE.resources.session_background
- val store = Sessions.store(options)
+ val store = sessions_store(options)
session.phase_changed += PIDE.plugin.session_phase_changed
- Isabelle_Process.start(session, options, session_background, store,
- logic = PIDE.resources.session_base.session_name,
+ Isabelle_Process.start(store, store.options, session, session_background,
+ logic = session_background.session_name,
modes =
- (space_explode(',', options.string("jedit_print_mode")) :::
+ (space_explode(',', store.options.string("jedit_print_mode")) :::
space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse)
}
}
--- a/src/Tools/jEdit/src/main_plugin.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala Thu Dec 22 21:55:51 2022 +0100
@@ -86,23 +86,23 @@
val spell_checker = new Spell_Checker_Variable
- /* global changes */
-
- def options_changed(): Unit = {
- session.global_options.post(Session.Global_Options(options.value))
- delay_load.invoke()
- }
-
- def deps_changed(): Unit = {
- delay_load.invoke()
- }
-
-
/* theory files */
- lazy val delay_init: Delay =
+ private lazy val delay_init: Delay =
Delay.last(PIDE.session.load_delay, gui = true) { init_models() }
+ private lazy val delay_load: Delay =
+ Delay.last(session.load_delay, gui = true) {
+ if (JEdit_Options.continuous_checking()) {
+ if (!PerspectiveManager.isPerspectiveEnabled ||
+ JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
+ else if (delay_load_activated()) delay_load_body()
+ else delay_load.invoke()
+ }
+ }
+
+ def deps_changed(): Unit = delay_load.invoke()
+
private val delay_load_active = Synchronized(false)
private def delay_load_finished(): Unit = delay_load_active.change(_ => false)
private def delay_load_activated(): Boolean =
@@ -112,7 +112,9 @@
val required_files = {
val models = Document_Model.get_models()
- val thy_files = resources.resolve_dependencies(models, Nil)
+ val thy_files =
+ resources.resolve_dependencies(models,
+ PIDE.editor.document_required().map((_, Position.none)))
val aux_files =
if (resources.auto_resolve) {
@@ -148,16 +150,6 @@
else delay_load_finished()
}
- private lazy val delay_load: Delay =
- Delay.last(session.load_delay, gui = true) {
- if (JEdit_Options.continuous_checking()) {
- if (!PerspectiveManager.isPerspectiveEnabled ||
- JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
- else if (delay_load_activated()) delay_load_body()
- else delay_load.invoke()
- }
- }
-
private def file_watcher_action(changed: Set[JFile]): Unit =
if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
--- a/src/Tools/jEdit/src/theories_dockable.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Thu Dec 22 21:55:51 2022 +0100
@@ -31,7 +31,7 @@
}
private val purge = new GUI.Button("Purge") {
- tooltip = "Restrict document model to theories required for open editor buffers"
+ tooltip = "Remove theories that are no longer required"
override def clicked(): Unit = PIDE.editor.purge()
}
@@ -48,8 +48,8 @@
/* main */
- val status = new Theories_Status(view)
- set_content(new ScrollPane(status.gui))
+ private val theories = new Theories_Status(view)
+ set_content(new ScrollPane(theories.gui))
private val main =
Session.Consumer[Any](getClass.getName) {
@@ -60,11 +60,11 @@
GUI_Thread.later {
continuous_checking.load()
logic.load()
- status.reinit()
+ theories.refresh()
}
case changed: Session.Commands_Changed =>
- GUI_Thread.later { status.update(domain = Some(changed.nodes), trim = changed.assignment) }
+ GUI_Thread.later { theories.update(domain = Some(changed.nodes), trim = changed.assignment) }
}
override def init(): Unit = {
@@ -73,7 +73,7 @@
PIDE.session.commands_changed += main
handle_phase(PIDE.session.phase)
- status.update()
+ theories.update()
}
override def exit(): Unit = {
--- a/src/Tools/jEdit/src/theories_status.scala Tue Dec 20 09:34:37 2022 +0100
+++ b/src/Tools/jEdit/src/theories_status.scala Thu Dec 22 21:55:51 2022 +0100
@@ -24,8 +24,18 @@
/* component state -- owned by GUI thread */
private var nodes_status = Document_Status.Nodes_Status.empty
- private var theory_required: Set[Document.Node.Name] = Document_Model.required_nodes(false)
- private var document_required: Set[Document.Node.Name] = Document_Model.required_nodes(true)
+ private var nodes_required = Set.empty[Document.Node.Name]
+ private var document_required = Set.empty[Document.Node.Name]
+
+ private def init_state(): Unit = GUI_Thread.require {
+ if (document) {
+ nodes_required = PIDE.editor.document_required().toSet
+ }
+ else {
+ nodes_required = Document_Model.nodes_required()
+ document_required = PIDE.editor.document_required().toSet
+ }
+ }
/* node renderer */
@@ -51,6 +61,9 @@
}
private class Node_Renderer extends ListView.Renderer[Document.Node.Name] {
+ private val document_marker = Symbol.decode(" \\<^file>")
+ private val no_document_marker = " "
+
private object component extends BorderPanel {
opaque = true
border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
@@ -143,10 +156,11 @@
index: Int
): Component = {
component.node_name = name
- component.required.selected =
- (if (document) document_required else theory_required).contains(name)
+ component.required.selected = nodes_required.contains(name)
component.label_border(name)
- component.label.text = name.theory_base_name
+ component.label.text =
+ name.theory_base_name +
+ (if (document_required.contains(name)) document_marker else no_document_marker)
component
}
}
@@ -172,7 +186,9 @@
val index_location = peer.indexToLocation(index)
if (node_renderer.in_required(index_location, point)) {
if (clicks == 1) {
- Document_Model.node_required(listData(index), toggle = true, document = document)
+ val name = listData(index)
+ if (document) PIDE.editor.document_select(Set(name), toggle = true)
+ else Document_Model.node_required(name, toggle = true)
}
}
else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node)
@@ -203,7 +219,11 @@
/* update */
- def update(domain: Option[Set[Document.Node.Name]] = None, trim: Boolean = false): Unit = {
+ def update(
+ domain: Option[Set[Document.Node.Name]] = None,
+ trim: Boolean = false,
+ force: Boolean = false
+ ): Unit = {
GUI_Thread.require {}
val snapshot = PIDE.session.snapshot()
@@ -213,23 +233,27 @@
PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim)
nodes_status = nodes_status1
- if (nodes_status_changed) {
+ if (nodes_status_changed || force) {
gui.listData =
- (for {
- (name, node_status) <- nodes_status1.present.iterator
- if !node_status.is_suppressed && node_status.total > 0
- } yield name).toList
+ if (document) {
+ nodes_status1.present(domain = Some(PIDE.editor.document_theories())).map(_._1)
+ }
+ else {
+ (for {
+ (name, node_status) <- nodes_status1.present().iterator
+ if !node_status.is_empty && !node_status.is_suppressed && node_status.total > 0
+ } yield name).toList
+ }
}
}
- /* reinit */
+ /* refresh */
- def reinit(): Unit = {
- GUI_Thread.require {}
-
- theory_required = Document_Model.required_nodes(false)
- document_required = Document_Model.required_nodes(true)
+ def refresh(): Unit = GUI_Thread.require {
+ init_state()
gui.repaint()
}
+
+ init_state()
}