--- a/Admin/components/components.sha1 Thu Jul 08 08:42:36 2021 +0200
+++ b/Admin/components/components.sha1 Thu Jul 08 08:44:18 2021 +0200
@@ -90,6 +90,7 @@
dac46ce81cee10fb36a9d39b414dec7b7b671545 flatlaf-1.0-rc2.tar.gz
d94e6da7299004890c04a7b395a3f2d381a3281e flatlaf-1.0-rc3.tar.gz
7ca3e6a8c9bd837990e64d89e7fa07a7e7cf78ff flatlaf-1.0.tar.gz
+9908e5ab721f1c0035c0ab04dc7ad0bd00a8db27 flatlaf-1.2.tar.gz
f339234ec18369679be0095264e0c0af7762f351 gnu-utils-20210414.tar.gz
683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz
989234b3799fe8750f3c24825d1f717c24fb0214 idea-icons-20210508.tar.gz
@@ -120,6 +121,8 @@
b166b4bd583b6442a5d75eab06f7adbb66919d6d isabelle_fonts-20210319.tar.gz
9467ad54a9ac10a6e7e8db5458d8d2a5516eba96 isabelle_fonts-20210321.tar.gz
1f7a0b9829ecac6552b21e995ad0f0ac168634f3 isabelle_fonts-20210322.tar.gz
+916adccd2f40c55116b68b92ce1eccb24d4dd9a2 isabelle_setup-20210630.tar.gz
+c611e363287fcc9bdd93c33bef85fa4e66cd3f37 isabelle_setup-20210701.tar.gz
0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
@@ -345,6 +348,7 @@
a0622fe75c3482ba7dc3ce74d58583b648a1ff0d scala-2.13.4-1.tar.gz
ec53cce3c5edda1145ec5d13924a5f9418995c15 scala-2.13.4.tar.gz
f51981baf34c020ad103b262f81796c37abcaa4a scala-2.13.5.tar.gz
+0a7cab09dec357dab7819273f2542ff1c3ea0968 scala-2.13.6.tar.gz
b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz
5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz
abe7a3b50da529d557a478e9f631a22429418a67 smbc-0.4.1.tar.gz
--- a/Admin/components/main Thu Jul 08 08:42:36 2021 +0200
+++ b/Admin/components/main Thu Jul 08 08:44:18 2021 +0200
@@ -5,9 +5,10 @@
csdp-6.1.1
cvc4-1.8
e-2.5-1
-flatlaf-1.0
+flatlaf-1.2
idea-icons-20210508
isabelle_fonts-20210322
+isabelle_setup-20210701
jdk-15.0.2+7
jedit_build-20210510-1
jfreechart-1.5.1
--- a/Admin/etc/options Thu Jul 08 08:42:36 2021 +0200
+++ b/Admin/etc/options Thu Jul 08 08:44:18 2021 +0200
@@ -5,10 +5,10 @@
option isabelle_components_server : string = "lxbroy10.informatik.tu-muenchen.de"
-- "user@host for SSH connection"
-option isabelle_components_dir : string = "/home/isabelle/components"
+option isabelle_components_dir : string = "/p/home/isabelle/components"
-- "webspace for ISABELLE_COMPONENT_REPOSITORY"
-option isabelle_components_contrib_dir : string = "/home/isabelle/contrib"
+option isabelle_components_contrib_dir : string = "/p/home/isabelle/contrib"
-- "unpacked components for remote build services"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/lib/Tools/build_setup Thu Jul 08 08:44:18 2021 +0200
@@ -0,0 +1,84 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: build component for Isabelle/Java setup tool
+
+## sources
+
+declare -a SOURCES=(
+ "Build_Scala.java"
+ "Environment.java"
+ "Setup.java"
+)
+
+
+## usage
+
+PRG=$(basename "$0")
+
+function usage()
+{
+ echo
+ echo "Usage: isabelle $PRG [OPTIONS] COMPONENT_DIR"
+ echo
+ echo " Build component for Isabelle/Java setup tool."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## process command line
+
+[ "$#" -ge 1 ] && { COMPONENT_DIR="$1"; shift; }
+[ "$#" -ne 0 -o -z "$COMPONENT_DIR" ] && usage
+
+
+
+## main
+
+[ -d "$COMPONENT_DIR" ] && fail "Directory already exists: \"$COMPONENT_DIR\""
+
+
+# build jar
+
+TARGET_DIR="$COMPONENT_DIR/lib"
+mkdir -p "$TARGET_DIR/isabelle/setup"
+
+declare -a ARGS=("-Xlint:unchecked")
+for SRC in "${SOURCES[@]}"
+do
+ ARGS["${#ARGS[@]}"]="$(platform_path "$ISABELLE_HOME/src/Tools/Setup/isabelle/setup/$SRC")"
+done
+
+isabelle_jdk javac -d "$TARGET_DIR" -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "${ARGS[@]}" || \
+ fail "Failed to compile sources"
+
+isabelle_jdk jar -c -f "$(platform_path "$TARGET_DIR/isabelle_setup.jar")" \
+ -e "isabelle.setup.Setup" -C "$TARGET_DIR" isabelle || fail "Failed to produce jar"
+
+rm -rf "$TARGET_DIR/isabelle"
+
+
+# etc/settings
+
+mkdir -p "$COMPONENT_DIR/etc"
+cat > "$COMPONENT_DIR/etc/settings" <<EOF
+# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_SETUP_JAR="\$COMPONENT/lib/isabelle_setup.jar"
+classpath "\$ISABELLE_SETUP_JAR"
+EOF
+
+
+# README
+
+cat > "$COMPONENT_DIR/README" <<EOF
+Isabelle setup in pure Java, see also \$ISABELLE_HOME/src/Tools/Setup/.
+EOF
--- a/NEWS Thu Jul 08 08:42:36 2021 +0200
+++ b/NEWS Thu Jul 08 08:44:18 2021 +0200
@@ -31,6 +31,8 @@
* More robust 'proof' outline for method "induct": support nested cases.
+* Support for built-in font substitution of jEdit text area.
+
*** Document preparation ***
@@ -131,12 +133,23 @@
operations has been adjusted to match the corresponding precendences on
sets. Rare INCOMPATIBILITY.
+* Theory "HOL-Library.Cardinality": code generator setup based on the
+type classes finite_UNIV and card_UNIV has been moved to
+"HOL-Library.Code_Cardinality", to avoid incompatibilities with
+other code setups for sets in AFP/Containers. Applications relying on
+this code setup should import "HOL-Library.Code_Cardinality". Minor
+INCOMPATIBILITY.
+
* Session "HOL-Analysis" and "HOL-Probability": indexed products of
discrete distributions, negative binomial distribution, Hoeffding's
inequality, Chernoff bounds, Cauchy–Schwarz inequality for nn_integral,
and some more small lemmas. Some theorems that were stated awkwardly
before were corrected. Minor INCOMPATIBILITY.
+* Session "HOL-Analysis": the complex Arg function has been identified
+with the function "arg" of Complex_Main, renaming arg->Arg also in the
+names of arg_bounded. Minor INCOMPATIBILITY.
+
* Theorems "antisym" and "eq_iff" in class "order" have been renamed to
"order.antisym" and "order.eq_iff", to coexist locally with "antisym"
and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant
@@ -175,6 +188,10 @@
"setBit", "clearBit". See there further the changelog in theory Guide.
INCOMPATIBILITY.
+* New simp rules: less_exp, min.absorb1, min.absorb2, min.absorb3,
+min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4. Minor
+INCOMPATIBILITY.
+
*** ML ***
--- a/src/HOL/Analysis/Bochner_Integration.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Thu Jul 08 08:44:18 2021 +0200
@@ -1657,7 +1657,8 @@
have U_le: "x \<in> space M \<Longrightarrow> U i x \<le> max 0 (f x)" for x i
using seq by (intro incseq_le) (auto simp: incseq_def le_fun_def)
with seq nonneg show "(\<lambda>i. integral\<^sup>L M (U i)) \<longlonglongrightarrow> LINT x|M. max 0 (f x)"
- by (intro integral_dominated_convergence) auto
+ by (intro integral_dominated_convergence)
+ (simp_all, fastforce)
have "integrable M (U i)" for i
using seq.prems by (rule integrable_bound) (insert U_le seq, auto)
with seq show "\<exists>N. \<forall>n\<ge>N. 0 \<le> integral\<^sup>L M (U n)"
--- a/src/HOL/Analysis/Change_Of_Vars.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Thu Jul 08 08:44:18 2021 +0200
@@ -3374,6 +3374,26 @@
(\<lambda>x. \<bar>g' x\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S)"
using has_absolute_integral_change_of_variables_1 [OF assms] by auto
+text \<open>when @{term "n=1"}\<close>
+lemma has_absolute_integral_change_of_variables_1':
+ fixes f :: "real \<Rightarrow> real" and g :: "real \<Rightarrow> real"
+ assumes S: "S \<in> sets lebesgue"
+ and der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)"
+ and inj: "inj_on g S"
+ shows "(\<lambda>x. \<bar>g' x\<bar> *\<^sub>R f(g x)) absolutely_integrable_on S \<and>
+ integral S (\<lambda>x. \<bar>g' x\<bar> *\<^sub>R f(g x)) = b
+ \<longleftrightarrow> f absolutely_integrable_on (g ` S) \<and> integral (g ` S) f = b"
+proof -
+ have "(\<lambda>x. \<bar>g' x\<bar> *\<^sub>R vec (f(g x)) :: real ^ 1) absolutely_integrable_on S \<and>
+ integral S (\<lambda>x. \<bar>g' x\<bar> *\<^sub>R vec (f(g x))) = (vec b :: real ^ 1)
+ \<longleftrightarrow> (\<lambda>x. vec (f x) :: real ^ 1) absolutely_integrable_on (g ` S) \<and>
+ integral (g ` S) (\<lambda>x. vec (f x)) = (vec b :: real ^ 1)"
+ using assms unfolding has_field_derivative_iff_has_vector_derivative
+ by (intro has_absolute_integral_change_of_variables_1 assms) auto
+ thus ?thesis
+ by (simp add: absolutely_integrable_on_1_iff integral_on_1_eq)
+qed
+
subsection\<open>Change of variables for integrals: special case of linear function\<close>
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Thu Jul 08 08:44:18 2021 +0200
@@ -148,6 +148,16 @@
"f holomorphic_on s \<Longrightarrow> continuous_on s f"
by (metis field_differentiable_imp_continuous_at continuous_on_eq_continuous_within holomorphic_on_def)
+lemma holomorphic_closedin_preimage_constant:
+ assumes "f holomorphic_on D"
+ shows "closedin (top_of_set D) {z\<in>D. f z = a}"
+ by (simp add: assms continuous_closedin_preimage_constant holomorphic_on_imp_continuous_on)
+
+lemma holomorphic_closed_preimage_constant:
+ assumes "f holomorphic_on UNIV"
+ shows "closed {z. f z = a}"
+ using holomorphic_closedin_preimage_constant [OF assms] by simp
+
lemma holomorphic_on_subset [elim]:
"f holomorphic_on s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f holomorphic_on t"
unfolding holomorphic_on_def
--- a/src/HOL/Analysis/Complex_Transcendental.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Thu Jul 08 08:44:18 2021 +0200
@@ -1367,8 +1367,8 @@
"continuous_on S f \<Longrightarrow> (\<And>z. z \<in> S \<Longrightarrow> f z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on S (\<lambda>x. Ln (f x))"
by (rule continuous_on_compose2[OF continuous_on_Ln, of "UNIV - nonpos_Reals" S f]) auto
-lemma holomorphic_on_Ln [holomorphic_intros]: "(\<And>z. z \<in> S \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on S"
- by (simp add: field_differentiable_within_Ln holomorphic_on_def)
+lemma holomorphic_on_Ln [holomorphic_intros]: "S \<inter> \<real>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Ln holomorphic_on S"
+ by (simp add: disjoint_iff field_differentiable_within_Ln holomorphic_on_def)
lemma holomorphic_on_Ln' [holomorphic_intros]:
"(\<And>z. z \<in> A \<Longrightarrow> f z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> f holomorphic_on A \<Longrightarrow> (\<lambda>z. Ln (f z)) holomorphic_on A"
@@ -1695,6 +1695,10 @@
using mpi_less_Im_Ln Im_Ln_le_pi
by (force simp: Ln_times)
+corollary\<^marker>\<open>tag unimportant\<close> Ln_times_of_nat:
+ "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(of_nat r * z :: complex) = ln (of_nat r) + Ln(z)"
+ using Ln_times_of_real[of "of_nat r" z] by simp
+
corollary\<^marker>\<open>tag unimportant\<close> Ln_times_Reals:
"\<lbrakk>r \<in> Reals; Re r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(r * z) = ln (Re r) + Ln(z)"
using Ln_Reals_eq Ln_times_of_real by fastforce
@@ -1778,11 +1782,26 @@
subsection\<open>The Argument of a Complex Number\<close>
-text\<open>Finally: it's is defined for the same interval as the complex logarithm: \<open>(-\<pi>,\<pi>]\<close>.\<close>
-
-definition\<^marker>\<open>tag important\<close> Arg :: "complex \<Rightarrow> real" where "Arg z \<equiv> (if z = 0 then 0 else Im (Ln z))"
-
-lemma Arg_of_real: "Arg (of_real r) = (if r<0 then pi else 0)"
+text\<open>Unlike in HOL Light, it's defined for the same interval as the complex logarithm: \<open>(-\<pi>,\<pi>]\<close>.\<close>
+
+lemma Arg_eq_Im_Ln:
+ assumes "z \<noteq> 0" shows "Arg z = Im (Ln z)"
+proof (rule cis_Arg_unique)
+ show "sgn z = cis (Im (Ln z))"
+ by (metis assms exp_Ln exp_eq_polar nonzero_mult_div_cancel_left norm_eq_zero
+ norm_exp_eq_Re of_real_eq_0_iff sgn_eq)
+ show "- pi < Im (Ln z)"
+ by (simp add: assms mpi_less_Im_Ln)
+ show "Im (Ln z) \<le> pi"
+ by (simp add: Im_Ln_le_pi assms)
+qed
+
+text \<open>The 1990s definition of argument coincides with the more recent one\<close>
+lemma\<^marker>\<open>tag important\<close> Arg_def:
+ shows "Arg z = (if z = 0 then 0 else Im (Ln z))"
+ by (simp add: Arg_eq_Im_Ln Arg_zero)
+
+lemma Arg_of_real [simp]: "Arg (of_real r) = (if r<0 then pi else 0)"
by (simp add: Im_Ln_eq_pi Arg_def)
lemma mpi_less_Arg: "-pi < Arg z"
@@ -2032,6 +2051,41 @@
using unwinding_2pi by (simp add: exp_add)
+lemma arg_conv_arctan:
+ assumes "Re z > 0"
+ shows "Arg z = arctan (Im z / Re z)"
+proof (rule cis_Arg_unique)
+ show "sgn z = cis (arctan (Im z / Re z))"
+ proof (rule complex_eqI)
+ have "Re (cis (arctan (Im z / Re z))) = 1 / sqrt (1 + (Im z)\<^sup>2 / (Re z)\<^sup>2)"
+ by (simp add: cos_arctan power_divide)
+ also have "1 + Im z ^ 2 / Re z ^ 2 = norm z ^ 2 / Re z ^ 2"
+ using assms by (simp add: cmod_def field_simps)
+ also have "1 / sqrt \<dots> = Re z / norm z"
+ using assms by (simp add: real_sqrt_divide)
+ finally show "Re (sgn z) = Re (cis (arctan (Im z / Re z)))"
+ by simp
+ next
+ have "Im (cis (arctan (Im z / Re z))) = Im z / (Re z * sqrt (1 + (Im z)\<^sup>2 / (Re z)\<^sup>2))"
+ by (simp add: sin_arctan field_simps)
+ also have "1 + Im z ^ 2 / Re z ^ 2 = norm z ^ 2 / Re z ^ 2"
+ using assms by (simp add: cmod_def field_simps)
+ also have "Im z / (Re z * sqrt \<dots>) = Im z / norm z"
+ using assms by (simp add: real_sqrt_divide)
+ finally show "Im (sgn z) = Im (cis (arctan (Im z / Re z)))"
+ by simp
+ qed
+next
+ show "arctan (Im z / Re z) > -pi"
+ by (rule le_less_trans[OF _ arctan_lbound]) auto
+next
+ have "arctan (Im z / Re z) < pi / 2"
+ by (rule arctan_ubound)
+ also have "\<dots> \<le> pi" by simp
+ finally show "arctan (Im z / Re z) \<le> pi"
+ by simp
+qed
+
subsection\<^marker>\<open>tag unimportant\<close>\<open>Relation between Ln and Arg2pi, and hence continuity of Arg2pi\<close>
lemma Arg2pi_Ln:
--- a/src/HOL/Analysis/Derivative.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Analysis/Derivative.thy Thu Jul 08 08:44:18 2021 +0200
@@ -1792,6 +1792,10 @@
by (intro vector_derivative_unique_within[OF not_bot vector_derivative_works[THEN iffD1] y])
(auto simp: differentiable_def has_vector_derivative_def)
+lemma deriv_of_real [simp]:
+ "at x within A \<noteq> bot \<Longrightarrow> vector_derivative of_real (at x within A) = 1"
+ by (auto intro!: vector_derivative_within derivative_eq_intros)
+
lemma frechet_derivative_eq_vector_derivative:
assumes "f differentiable (at x)"
shows "(frechet_derivative f (at x)) = (\<lambda>r. r *\<^sub>R vector_derivative f (at x))"
@@ -1825,6 +1829,18 @@
apply (auto simp: Lim_ident_at eventually_at_filter elim: eventually_mono)
done
+lemma vector_derivative_cong_eq:
+ assumes "eventually (\<lambda>x. x \<in> A \<longrightarrow> f x = g x) (nhds x)" "x = y" "A = B" "x \<in> A"
+ shows "vector_derivative f (at x within A) = vector_derivative g (at y within B)"
+proof -
+ have "f x = g x"
+ using assms eventually_nhds_x_imp_x by blast
+ hence "(\<lambda>D. (f has_vector_derivative D) (at x within A)) =
+ (\<lambda>D. (g has_vector_derivative D) (at x within A))" using assms
+ by (intro ext has_vector_derivative_cong_ev refl assms) simp_all
+ thus ?thesis by (simp add: vector_derivative_def assms)
+qed
+
lemma islimpt_closure_open:
fixes s :: "'a::perfect_space set"
assumes "open s" and t: "t = closure s" "x \<in> t"
@@ -1870,7 +1886,7 @@
\<Longrightarrow> vector_derivative (\<lambda>x. f x + g x) (at a) = vector_derivative f (at a) + vector_derivative g (at a)"
by (simp add: vector_derivative_at has_vector_derivative_add vector_derivative_works [symmetric])
-lemma vector_derivative_diff_at [simp]:
+lemma vector_derivative_diff_at [simp,derivative_intros]:
"\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
\<Longrightarrow> vector_derivative (\<lambda>x. f x - g x) (at a) = vector_derivative f (at a) - vector_derivative g (at a)"
by (simp add: vector_derivative_at has_vector_derivative_diff vector_derivative_works [symmetric])
@@ -2254,6 +2270,20 @@
shows "DERIV f x :> deriv f x \<longleftrightarrow> f differentiable at x"
unfolding differentiable_def by (metis DERIV_imp_deriv has_real_derivative_iff)
+lemma DERIV_deriv_iff_field_differentiable:
+ "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
+ unfolding field_differentiable_def by (metis DERIV_imp_deriv)
+
+lemma vector_derivative_of_real_left:
+ assumes "f differentiable at x"
+ shows "vector_derivative (\<lambda>x. of_real (f x)) (at x) = of_real (deriv f x)"
+ by (metis DERIV_deriv_iff_real_differentiable assms has_vector_derivative_of_real vector_derivative_at)
+
+lemma vector_derivative_of_real_right:
+ assumes "f field_differentiable at (of_real x)"
+ shows "vector_derivative (\<lambda>x. f (of_real x)) (at x) = deriv f (of_real x)"
+ by (metis DERIV_deriv_iff_field_differentiable assms has_vector_derivative_real_field vector_derivative_at)
+
lemma deriv_cong_ev:
assumes "eventually (\<lambda>x. f x = g x) (nhds x)" "x = y"
shows "deriv f x = deriv g y"
@@ -2276,7 +2306,7 @@
by eventually_elim (rule deriv_cong_ev, simp_all)
thus ?case by (auto intro!: deriv_cong_ev Suc simp: funpow_Suc_right simp del: funpow.simps)
qed auto
- from eventually_nhds_x_imp_x[OF this] assms(2) show ?thesis by simp
+ with \<open>x = y\<close> eventually_nhds_x_imp_x show ?thesis by blast
qed
lemma real_derivative_chain:
@@ -2298,10 +2328,6 @@
apply (rule vector_derivative_at [OF field_vector_diff_chain_at])
using assms vector_derivative_works by (auto simp: field_differentiable_derivI)
-lemma DERIV_deriv_iff_field_differentiable:
- "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
- unfolding field_differentiable_def by (metis DERIV_imp_deriv)
-
lemma deriv_chain:
"f field_differentiable at x \<Longrightarrow> g field_differentiable at (f x)
\<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Thu Jul 08 08:44:18 2021 +0200
@@ -1465,6 +1465,12 @@
using bounded_closed_imp_seq_compact compact_eq_seq_compact_metric compact_imp_bounded compact_imp_closed
by auto
+lemma bounded_infinite_imp_islimpt:
+ fixes S :: "'a::heine_borel set"
+ assumes "T \<subseteq> S" "bounded S" "infinite T"
+ obtains x where "x islimpt S"
+ by (meson assms closed_limpt compact_eq_Bolzano_Weierstrass compact_eq_bounded_closed islimpt_subset)
+
lemma compact_Inter:
fixes \<F> :: "'a :: heine_borel set set"
assumes com: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" and "\<F> \<noteq> {}"
--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Thu Jul 08 08:44:18 2021 +0200
@@ -765,13 +765,7 @@
using LIMSEQ_ignore_initial_segment [where k=2, OF b] by simp
qed
also have "(\<Sum>i\<in>Basis. max (a \<bullet> i) (min (f x \<bullet> i) (b \<bullet> i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (f x \<bullet> i) *\<^sub>R i)"
- apply (rule sum.cong)
- using fab
- apply auto
- apply (intro order_antisym)
- apply (auto simp: mem_box)
- using less_imp_le apply blast
- by (metis (full_types) linear max_less_iff_conj min.bounded_iff not_le)
+ using fab by (auto simp add: mem_box intro: sum.cong)
also have "\<dots> = f x"
using euclidean_representation by blast
finally show "(\<lambda>n. \<theta> n x) \<longlonglongrightarrow> f x" .
--- a/src/HOL/Analysis/Gamma_Function.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy Thu Jul 08 08:44:18 2021 +0200
@@ -1015,6 +1015,21 @@
by (intro DERIV_imp_deriv has_field_derivative_ln_Gamma_complex assms)
+lemma higher_deriv_ln_Gamma_complex:
+ assumes "(x::complex) \<notin> \<real>\<^sub>\<le>\<^sub>0"
+ shows "(deriv ^^ j) ln_Gamma x = (if j = 0 then ln_Gamma x else Polygamma (j - 1) x)"
+proof (cases j)
+ case (Suc j')
+ have "(deriv ^^ j') (deriv ln_Gamma) x = (deriv ^^ j') Digamma x"
+ using eventually_nhds_in_open[of "UNIV - \<real>\<^sub>\<le>\<^sub>0" x] assms
+ by (intro higher_deriv_cong_ev refl)
+ (auto elim!: eventually_mono simp: open_Diff deriv_ln_Gamma_complex)
+ also have "\<dots> = Polygamma j' x" using assms
+ by (subst higher_deriv_Polygamma)
+ (auto elim!: nonpos_Ints_cases simp: complex_nonpos_Reals_iff)
+ finally show ?thesis using Suc by (simp del: funpow.simps add: funpow_Suc_right)
+qed simp_all
+
text \<open>
We define a type class that captures all the fundamental properties of the inverse of the Gamma function
@@ -1695,6 +1710,27 @@
shows "deriv ln_Gamma z = Digamma (z :: real)"
by (intro DERIV_imp_deriv has_field_derivative_ln_Gamma_real assms)
+lemma higher_deriv_ln_Gamma_real:
+ assumes "(x::real) > 0"
+ shows "(deriv ^^ j) ln_Gamma x = (if j = 0 then ln_Gamma x else Polygamma (j - 1) x)"
+proof (cases j)
+ case (Suc j')
+ have "(deriv ^^ j') (deriv ln_Gamma) x = (deriv ^^ j') Digamma x"
+ using eventually_nhds_in_open[of "{0<..}" x] assms
+ by (intro higher_deriv_cong_ev refl)
+ (auto elim!: eventually_mono simp: open_Diff deriv_ln_Gamma_real)
+ also have "\<dots> = Polygamma j' x" using assms
+ by (subst higher_deriv_Polygamma)
+ (auto elim!: nonpos_Ints_cases simp: complex_nonpos_Reals_iff)
+ finally show ?thesis using Suc by (simp del: funpow.simps add: funpow_Suc_right)
+qed simp_all
+
+lemma higher_deriv_ln_Gamma_complex_of_real:
+ assumes "(x :: real) > 0"
+ shows "(deriv ^^ j) ln_Gamma (complex_of_real x) = of_real ((deriv ^^ j) ln_Gamma x)"
+ using assms
+ by (auto simp: higher_deriv_ln_Gamma_real higher_deriv_ln_Gamma_complex
+ ln_Gamma_complex_of_real Polygamma_of_real)
lemma has_field_derivative_rGamma_real' [derivative_intros]:
"(rGamma has_field_derivative (if x \<in> \<int>\<^sub>\<le>\<^sub>0 then (-1)^(nat \<lfloor>-x\<rfloor>) * fact (nat \<lfloor>-x\<rfloor>) else
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Jul 08 08:44:18 2021 +0200
@@ -4922,6 +4922,9 @@
shows "negligible S"
by (metis negligible_translation [OF assms, of "-c"] translation_galois)
+lemma negligible_atLeastAtMostI: "b \<le> a \<Longrightarrow> negligible {a..(b::real)}"
+ using negligible_insert by fastforce
+
lemma has_integral_spike_set_eq:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
assumes "negligible {x \<in> S - T. f x \<noteq> 0}" "negligible {x \<in> T - S. f x \<noteq> 0}"
--- a/src/HOL/Analysis/Linear_Algebra.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Thu Jul 08 08:44:18 2021 +0200
@@ -1240,6 +1240,22 @@
qed
qed
+lemma collinear_iff_Reals: "collinear {0::complex,w,z} \<longleftrightarrow> z/w \<in> \<real>"
+proof
+ show "z/w \<in> \<real> \<Longrightarrow> collinear {0,w,z}"
+ by (metis Reals_cases collinear_lemma nonzero_divide_eq_eq scaleR_conv_of_real)
+qed (auto simp: collinear_lemma scaleR_conv_of_real)
+
+lemma collinear_scaleR_iff: "collinear {0, \<alpha> *\<^sub>R w, \<beta> *\<^sub>R z} \<longleftrightarrow> collinear {0,w,z} \<or> \<alpha>=0 \<or> \<beta>=0"
+ (is "?lhs = ?rhs")
+proof (cases "\<alpha>=0 \<or> \<beta>=0")
+ case False
+ then have "(\<exists>c. \<beta> *\<^sub>R z = (c * \<alpha>) *\<^sub>R w) = (\<exists>c. z = c *\<^sub>R w)"
+ by (metis mult.commute scaleR_scaleR vector_fraction_eq_iff)
+ then show ?thesis
+ by (auto simp add: collinear_lemma)
+qed (auto simp: collinear_lemma)
+
lemma norm_cauchy_schwarz_equal: "\<bar>x \<bullet> y\<bar> = norm x * norm y \<longleftrightarrow> collinear {0, x, y}"
proof (cases "x=0")
case True
@@ -1262,6 +1278,16 @@
qed
qed
+lemma norm_triangle_eq_imp_collinear:
+ fixes x y :: "'a::real_inner"
+ assumes "norm (x + y) = norm x + norm y"
+ shows "collinear{0,x,y}"
+proof (cases "x = 0 \<or> y = 0")
+ case False
+ with assms show ?thesis
+ by (meson norm_cauchy_schwarz_abs_eq norm_cauchy_schwarz_equal norm_triangle_eq)
+qed (use collinear_lemma in blast)
+
subsection\<open>Properties of special hyperplanes\<close>
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Thu Jul 08 08:44:18 2021 +0200
@@ -21,10 +21,10 @@
"Sup :: _ Predicate.pred set \<Rightarrow> _"
pred_of_set
Wellfounded.acc
- Cardinality.card'
- Cardinality.finite'
- Cardinality.subset'
- Cardinality.eq_set
+ Code_Cardinality.card'
+ Code_Cardinality.finite'
+ Code_Cardinality.subset'
+ Code_Cardinality.eq_set
Euclidean_Algorithm.Gcd
Euclidean_Algorithm.Lcm
"Gcd :: _ poly set \<Rightarrow> _"
--- a/src/HOL/Complex.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Complex.thy Thu Jul 08 08:44:18 2021 +0200
@@ -888,7 +888,6 @@
lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1 / r2) (a - b)"
by (simp add: rcis_def cis_divide [symmetric])
-
subsubsection \<open>Complex exponential\<close>
lemma exp_Reals_eq:
@@ -957,15 +956,15 @@
subsubsection \<open>Complex argument\<close>
-definition arg :: "complex \<Rightarrow> real"
- where "arg z = (if z = 0 then 0 else (SOME a. sgn z = cis a \<and> - pi < a \<and> a \<le> pi))"
+definition Arg :: "complex \<Rightarrow> real"
+ where "Arg z = (if z = 0 then 0 else (SOME a. sgn z = cis a \<and> - pi < a \<and> a \<le> pi))"
-lemma arg_zero: "arg 0 = 0"
- by (simp add: arg_def)
+lemma Arg_zero: "Arg 0 = 0"
+ by (simp add: Arg_def)
-lemma arg_unique:
+lemma cis_Arg_unique:
assumes "sgn z = cis x" and "-pi < x" and "x \<le> pi"
- shows "arg z = x"
+ shows "Arg z = x"
proof -
from assms have "z \<noteq> 0" by auto
have "(SOME a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi) = x"
@@ -987,14 +986,14 @@
then show "a = x"
by (simp add: d_def)
qed (simp add: assms del: Re_sgn Im_sgn)
- with \<open>z \<noteq> 0\<close> show "arg z = x"
- by (simp add: arg_def)
+ with \<open>z \<noteq> 0\<close> show "Arg z = x"
+ by (simp add: Arg_def)
qed
-lemma arg_correct:
+lemma Arg_correct:
assumes "z \<noteq> 0"
- shows "sgn z = cis (arg z) \<and> -pi < arg z \<and> arg z \<le> pi"
-proof (simp add: arg_def assms, rule someI_ex)
+ shows "sgn z = cis (Arg z) \<and> -pi < Arg z \<and> Arg z \<le> pi"
+proof (simp add: Arg_def assms, rule someI_ex)
obtain r a where z: "z = rcis r a"
using rcis_Ex by fast
with assms have "r \<noteq> 0" by auto
@@ -1016,23 +1015,27 @@
by fast
qed
-lemma arg_bounded: "- pi < arg z \<and> arg z \<le> pi"
- by (cases "z = 0") (simp_all add: arg_zero arg_correct)
+lemma Arg_bounded: "- pi < Arg z \<and> Arg z \<le> pi"
+ by (cases "z = 0") (simp_all add: Arg_zero Arg_correct)
-lemma cis_arg: "z \<noteq> 0 \<Longrightarrow> cis (arg z) = sgn z"
- by (simp add: arg_correct)
+lemma cis_Arg: "z \<noteq> 0 \<Longrightarrow> cis (Arg z) = sgn z"
+ by (simp add: Arg_correct)
-lemma rcis_cmod_arg: "rcis (cmod z) (arg z) = z"
- by (cases "z = 0") (simp_all add: rcis_def cis_arg sgn_div_norm of_real_def)
+lemma rcis_cmod_Arg: "rcis (cmod z) (Arg z) = z"
+ by (cases "z = 0") (simp_all add: rcis_def cis_Arg sgn_div_norm of_real_def)
-lemma cos_arg_i_mult_zero [simp]: "y \<noteq> 0 \<Longrightarrow> Re y = 0 \<Longrightarrow> cos (arg y) = 0"
- using cis_arg [of y] by (simp add: complex_eq_iff)
+lemma rcis_cnj:
+ shows "cnj a = rcis (cmod a) (- Arg a)"
+ by (metis cis_cnj complex_cnj_complex_of_real complex_cnj_mult rcis_cmod_Arg rcis_def)
-lemma arg_ii [simp]: "arg \<i> = pi/2"
- by (rule arg_unique; simp add: sgn_eq)
+lemma cos_Arg_i_mult_zero [simp]: "y \<noteq> 0 \<Longrightarrow> Re y = 0 \<Longrightarrow> cos (Arg y) = 0"
+ using cis_Arg [of y] by (simp add: complex_eq_iff)
-lemma arg_minus_ii [simp]: "arg (-\<i>) = -pi/2"
-proof (rule arg_unique)
+lemma Arg_ii [simp]: "Arg \<i> = pi/2"
+ by (rule cis_Arg_unique; simp add: sgn_eq)
+
+lemma Arg_minus_ii [simp]: "Arg (-\<i>) = -pi/2"
+proof (rule cis_Arg_unique)
show "sgn (- \<i>) = cis (- pi / 2)"
by (simp add: sgn_eq)
show "- pi / 2 \<le> pi"
@@ -1097,23 +1100,23 @@
lemma bij_betw_nth_root_unity:
fixes c :: complex and n :: nat
assumes c: "c \<noteq> 0" and n: "n > 0"
- defines "c' \<equiv> root n (norm c) * cis (arg c / n)"
+ defines "c' \<equiv> root n (norm c) * cis (Arg c / n)"
shows "bij_betw (\<lambda>z. c' * z) {z. z ^ n = 1} {z. z ^ n = c}"
proof -
- have "c' ^ n = of_real (root n (norm c) ^ n) * cis (arg c)"
+ have "c' ^ n = of_real (root n (norm c) ^ n) * cis (Arg c)"
unfolding of_real_power using n by (simp add: c'_def power_mult_distrib DeMoivre)
also from n have "root n (norm c) ^ n = norm c" by simp
- also from c have "of_real \<dots> * cis (arg c) = c" by (simp add: cis_arg Complex.sgn_eq)
+ also from c have "of_real \<dots> * cis (Arg c) = c" by (simp add: cis_Arg Complex.sgn_eq)
finally have [simp]: "c' ^ n = c" .
show ?thesis unfolding bij_betw_def inj_on_def
proof safe
fix z :: complex assume "z ^ n = 1"
hence "(c' * z) ^ n = c' ^ n" by (simp add: power_mult_distrib)
- also have "c' ^ n = of_real (root n (norm c) ^ n) * cis (arg c)"
+ also have "c' ^ n = of_real (root n (norm c) ^ n) * cis (Arg c)"
unfolding of_real_power using n by (simp add: c'_def power_mult_distrib DeMoivre)
also from n have "root n (norm c) ^ n = norm c" by simp
- also from c have "\<dots> * cis (arg c) = c" by (simp add: cis_arg Complex.sgn_eq)
+ also from c have "\<dots> * cis (Arg c) = c" by (simp add: cis_Arg Complex.sgn_eq)
finally show "(c' * z) ^ n = c" .
next
fix z assume z: "c = z ^ n"
@@ -1188,7 +1191,7 @@
finally show ?thesis .
next
case False
- define c' where "c' = root n (norm c) * cis (arg c / n)"
+ define c' where "c' = root n (norm c) * cis (Arg c / n)"
from False and assms have "(\<Sum>{z. z ^ n = c}) = (\<Sum>z | z ^ n = 1. c' * z)"
by (subst sum.reindex_bij_betw [OF bij_betw_nth_root_unity, symmetric])
(auto simp: sum_distrib_left finite_roots_unity c'_def)
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Thu Jul 08 08:44:18 2021 +0200
@@ -400,6 +400,20 @@
\<Longrightarrow> ((deriv ^^ n) f has_field_derivative (deriv ^^ (Suc n)) f x) (at x)"
by (metis (no_types, opaque_lifting) DERIV_deriv_iff_field_differentiable at_within_open comp_apply
funpow.simps(2) holomorphic_higher_deriv holomorphic_on_def)
+
+lemma higher_deriv_cmult:
+ assumes "f holomorphic_on A" "x \<in> A" "open A"
+ shows "(deriv ^^ j) (\<lambda>x. c * f x) x = c * (deriv ^^ j) f x"
+ using assms
+proof (induction j arbitrary: f x)
+ case (Suc j f x)
+ have "deriv ((deriv ^^ j) (\<lambda>x. c * f x)) x = deriv (\<lambda>x. c * (deriv ^^ j) f x) x"
+ using eventually_nhds_in_open[of A x] assms(2,3) Suc.prems
+ by (intro deriv_cong_ev refl) (auto elim!: eventually_mono simp: Suc.IH)
+ also have "\<dots> = c * deriv ((deriv ^^ j) f) x" using Suc.prems assms(2,3)
+ by (intro deriv_cmult holomorphic_on_imp_differentiable_at holomorphic_higher_deriv) auto
+ finally show ?case by simp
+qed simp_all
lemma valid_path_compose_holomorphic:
assumes "valid_path g" and holo:"f holomorphic_on S" and "open S" "path_image g \<subseteq> S"
--- a/src/HOL/Complex_Analysis/Complex_Residues.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Complex_Analysis/Complex_Residues.thy Thu Jul 08 08:44:18 2021 +0200
@@ -11,11 +11,6 @@
"residue f z = (SOME int. \<exists>e>0. \<forall>\<epsilon>>0. \<epsilon><e
\<longrightarrow> (f has_contour_integral 2*pi* \<i> *int) (circlepath z \<epsilon>))"
-lemma Eps_cong:
- assumes "\<And>x. P x = Q x"
- shows "Eps P = Eps Q"
- using ext[of P Q, OF assms] by simp
-
lemma residue_cong:
assumes eq: "eventually (\<lambda>z. f z = g z) (at z)" and "z = z'"
shows "residue f z = residue g z'"
@@ -542,4 +537,4 @@
using Gamma_residues[of n] by simp
qed auto
-end
\ No newline at end of file
+end
--- a/src/HOL/Decision_Procs/Ferrack.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Thu Jul 08 08:44:18 2021 +0200
@@ -751,17 +751,7 @@
by (induct t) (simp_all add: numadd_nz numneg_nz numsub_nz nummul_nz)
lemma maxcoeff_nz: "nozerocoeff t \<Longrightarrow> maxcoeff t = 0 \<Longrightarrow> t = C 0"
-proof (induct t rule: maxcoeff.induct)
- case (2 n c t)
- then have cnz: "c \<noteq> 0" and mx: "max \<bar>c\<bar> (maxcoeff t) = 0"
- by simp_all
- have "max \<bar>c\<bar> (maxcoeff t) \<ge> \<bar>c\<bar>"
- by simp
- with cnz have "max \<bar>c\<bar> (maxcoeff t) > 0"
- by arith
- with 2 show ?case
- by simp
-qed auto
+ by (induction t rule: maxcoeff.induct) auto
lemma numgcd_nz:
assumes nz: "nozerocoeff t"
--- a/src/HOL/Deriv.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Deriv.thy Thu Jul 08 08:44:18 2021 +0200
@@ -813,6 +813,38 @@
lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff ..
+lemma field_derivative_lim_unique:
+ assumes f: "(f has_field_derivative df) (at z)"
+ and s: "s \<longlonglongrightarrow> 0" "\<And>n. s n \<noteq> 0"
+ and a: "(\<lambda>n. (f (z + s n) - f z) / s n) \<longlonglongrightarrow> a"
+ shows "df = a"
+proof (rule ccontr)
+ assume "df \<noteq> a"
+ obtain q where qpos: "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> q \<epsilon> > 0"
+ and q: "\<And>\<epsilon> y. \<lbrakk>\<epsilon> > 0; y \<noteq> z; dist y z < q \<epsilon>\<rbrakk> \<Longrightarrow> dist ((f y - f z) / (y - z)) df < \<epsilon>"
+ using f unfolding LIM_def has_field_derivative_iff by metis
+ obtain NA where NA: "\<And>\<epsilon> n. \<lbrakk>\<epsilon> > 0; n \<ge> NA \<epsilon>\<rbrakk> \<Longrightarrow> dist ((f (z + s n) - f z) / s n) a < \<epsilon>"
+ using a unfolding LIMSEQ_def by metis
+ obtain NB where NB: "\<And>\<epsilon> n. \<lbrakk>\<epsilon> > 0; n \<ge> NB \<epsilon>\<rbrakk> \<Longrightarrow> norm (s n) < \<epsilon>"
+ using s unfolding LIMSEQ_def by (metis norm_conv_dist)
+ have df: "\<And>\<epsilon> n. \<epsilon> > 0 \<Longrightarrow> \<lbrakk>0 < \<epsilon>; norm (s n) < q \<epsilon>\<rbrakk> \<Longrightarrow> dist ((f (z + s n) - f z) / s n) df < \<epsilon>"
+ using add_cancel_left_right add_diff_cancel_left' q s
+ by (metis add_diff_cancel_right' dist_diff(1))
+ define \<delta> where "\<delta> \<equiv> dist df a / 2"
+ with \<open>df \<noteq> a\<close> have "\<delta> > 0" and \<delta>: "\<delta>+\<delta> \<le> dist df a"
+ by auto
+ define N where "N \<equiv> max (NA \<delta>) (NB (q \<delta>))"
+ then have "norm (s N) < q \<delta>"
+ by (simp add: NB \<open>\<delta> > 0\<close> qpos)
+ then have "dist ((f (z + s N) - f z) / s N) df < \<delta>"
+ by (simp add: \<open>0 < \<delta>\<close> df)
+ moreover have "dist ((f (z + s N) - f z) / s N) a < \<delta>"
+ using NA N_def \<open>0 < \<delta>\<close> by force
+ ultimately have "dist df a < dist df a"
+ by (smt (verit, ccfv_SIG) \<delta> dist_commute dist_triangle)
+ then show False ..
+qed
+
lemma mult_commute_abs: "(\<lambda>x. x * c) = (*) c"
for c :: "'a::ab_semigroup_mult"
by (simp add: fun_eq_iff mult.commute)
@@ -1194,14 +1226,40 @@
DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
by (rule has_field_derivative_cong_ev) simp_all
+lemma DERIV_mirror: "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x)) x :> - y)"
+ for f :: "real \<Rightarrow> real" and x y :: real
+ by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right
+ tendsto_minus_cancel_left field_simps conj_commute)
+
lemma DERIV_shift:
"(f has_field_derivative y) (at (x + z)) = ((\<lambda>x. f (x + z)) has_field_derivative y) (at x)"
by (simp add: DERIV_def field_simps)
-lemma DERIV_mirror: "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x)) x :> - y)"
- for f :: "real \<Rightarrow> real" and x y :: real
- by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right
- tendsto_minus_cancel_left field_simps conj_commute)
+lemma DERIV_at_within_shift_lemma:
+ assumes "(f has_field_derivative y) (at (z+x) within (+) z ` S)"
+ shows "(f \<circ> (+)z has_field_derivative y) (at x within S)"
+proof -
+ have "((+)z has_field_derivative 1) (at x within S)"
+ by (rule derivative_eq_intros | simp)+
+ with assms DERIV_image_chain show ?thesis
+ by (metis mult.right_neutral)
+qed
+
+lemma DERIV_at_within_shift:
+ "(f has_field_derivative y) (at (z+x) within (+) z ` S) \<longleftrightarrow>
+ ((\<lambda>x. f (z+x)) has_field_derivative y) (at x within S)" (is "?lhs = ?rhs")
+proof
+ assume ?lhs then show ?rhs
+ using DERIV_at_within_shift_lemma unfolding o_def by blast
+next
+ have [simp]: "(\<lambda>x. x - z) ` (+) z ` S = S"
+ by force
+ assume R: ?rhs
+ have "(f \<circ> (+) z \<circ> (+) (- z) has_field_derivative y) (at (z + x) within (+) z ` S)"
+ by (rule DERIV_at_within_shift_lemma) (use R in \<open>simp add: o_def\<close>)
+ then show ?lhs
+ by (simp add: o_def)
+qed
lemma floor_has_real_derivative:
fixes f :: "real \<Rightarrow> 'a::{floor_ceiling,order_topology}"
--- a/src/HOL/HOLCF/Universal.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/HOLCF/Universal.thy Thu Jul 08 08:44:18 2021 +0200
@@ -41,7 +41,7 @@
by (rule order_trans [OF le_prod_encode_1 le_prod_encode_2])
lemma nat_less_power2: "n < 2^n"
-by (induct n) simp_all
+ by (fact less_exp)
lemma node_gt2: "\<lbrakk>finite S; b \<in> S\<rbrakk> \<Longrightarrow> b < node i a S"
unfolding node_def less_Suc_eq_le set_encode_def
--- a/src/HOL/Homology/Simplices.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Homology/Simplices.thy Thu Jul 08 08:44:18 2021 +0200
@@ -3241,9 +3241,12 @@
apply (subst pr_def)
apply (simp add: chain_boundary_sum chain_boundary_cmul)
apply (subst chain_boundary_def)
+ apply simp
apply (simp add: frag_cmul_sum sum.cartesian_product eq sum.union_disjoint disjoint_iff_not_equal
- sum.atLeast_Suc_atMost_Suc_shift del: sum.cl_ivl_Suc flip: comm_monoid_add_class.sum.Sigma)
- apply (simp add: comm_monoid_add_class.sum.Sigma eq2 [of _ "\<lambda>i. {_ i.._ i}"])
+ sum.atLeast_Suc_atMost_Suc_shift del: sum.cl_ivl_Suc min.absorb2 min.absorb4
+ flip: comm_monoid_add_class.sum.Sigma)
+ apply (simp add: sum.Sigma eq2 [of _ "\<lambda>i. {_ i.._ i}"]
+ del: min.absorb2 min.absorb4)
apply (simp add: sum.union_disjoint disjoint_iff_not_equal * [OF 1 2])
done
next
--- a/src/HOL/Import/HOL_Light_Maps.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Import/HOL_Light_Maps.thy Thu Jul 08 08:44:18 2021 +0200
@@ -175,11 +175,11 @@
lemma DEF_MAX[import_const "MAX"]:
"max = (\<lambda>x y :: nat. if x \<le> y then y else x)"
- by (auto simp add: max.absorb_iff2 fun_eq_iff)
+ by (simp add: fun_eq_iff)
lemma DEF_MIN[import_const "MIN"]:
"min = (\<lambda>x y :: nat. if x \<le> y then x else y)"
- by (auto simp add: min.absorb_iff1 fun_eq_iff)
+ by (simp add: fun_eq_iff)
definition even
where
--- a/src/HOL/Lattices.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Lattices.thy Thu Jul 08 08:44:18 2021 +0200
@@ -123,6 +123,12 @@
lemma absorb2: "b \<^bold>\<le> a \<Longrightarrow> a \<^bold>* b = b"
by (rule antisym) (auto simp: refl)
+lemma absorb3: "a \<^bold>< b \<Longrightarrow> a \<^bold>* b = a"
+ by (rule absorb1) (rule strict_implies_order)
+
+lemma absorb4: "b \<^bold>< a \<Longrightarrow> a \<^bold>* b = b"
+ by (rule absorb2) (rule strict_implies_order)
+
lemma absorb_iff1: "a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>* b = a"
using order_iff by auto
@@ -650,7 +656,7 @@
then show ?thesis by simp
qed
-lemma compl_less_compl_iff: "- x < - y \<longleftrightarrow> y < x" (* TODO: declare [simp] ? *)
+lemma compl_less_compl_iff [simp]: "- x < - y \<longleftrightarrow> y < x"
by (auto simp add: less_le)
lemma compl_less_swap1:
@@ -671,16 +677,16 @@
qed
lemma sup_cancel_left1: "sup (sup x a) (sup (- x) b) = top"
- by (simp add: inf_sup_aci sup_compl_top)
+ by (simp add: ac_simps sup_compl_top)
lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top"
- by (simp add: inf_sup_aci sup_compl_top)
+ by (simp add: ac_simps sup_compl_top)
lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot"
- by (simp add: inf_sup_aci inf_compl_bot)
+ by (simp add: ac_simps inf_compl_bot)
lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot"
- by (simp add: inf_sup_aci inf_compl_bot)
+ by (simp add: ac_simps inf_compl_bot)
declare inf_compl_bot [simp]
and sup_compl_top [simp]
@@ -743,6 +749,11 @@
+ max: semilattice_order max greater_eq greater
by standard (auto simp add: min_def max_def)
+declare min.absorb1 [simp] min.absorb2 [simp]
+ min.absorb3 [simp] min.absorb4 [simp]
+ max.absorb1 [simp] max.absorb2 [simp]
+ max.absorb3 [simp] max.absorb4 [simp]
+
lemma min_le_iff_disj: "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
unfolding min_def using linear by (auto intro: order_trans)
@@ -783,11 +794,11 @@
lemma split_min_lin [no_atp]:
\<open>P (min a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a < b \<longrightarrow> P a) \<and> (b < a \<longrightarrow> P b)\<close>
- by (cases a b rule: linorder_cases) (auto simp add: min.absorb1 min.absorb2)
+ by (cases a b rule: linorder_cases) auto
lemma split_max_lin [no_atp]:
\<open>P (max a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a < b \<longrightarrow> P b) \<and> (b < a \<longrightarrow> P a)\<close>
- by (cases a b rule: linorder_cases) (auto simp add: max.absorb1 max.absorb2)
+ by (cases a b rule: linorder_cases) auto
lemma min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)" for f :: "'a \<Rightarrow> 'b::linorder"
by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
--- a/src/HOL/Library/Bit_Operations.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Library/Bit_Operations.thy Thu Jul 08 08:44:18 2021 +0200
@@ -9,11 +9,6 @@
"HOL-Library.Boolean_Algebra"
begin
-lemma bit_numeral_int_iff [bit_simps]: \<comment> \<open>TODO: move\<close>
- \<open>bit (numeral m :: int) n \<longleftrightarrow> bit (numeral m :: nat) n\<close>
- using bit_of_nat_iff_bit [of \<open>numeral m\<close> n] by simp
-
-
subsection \<open>Bit operations\<close>
class semiring_bit_operations = semiring_bit_shifts +
@@ -533,7 +528,10 @@
proof (cases \<open>k \<ge> 0\<close>)
case True
moreover from power_gt_expt [of 2 \<open>nat k\<close>]
- have \<open>k < 2 ^ nat k\<close> by simp
+ have \<open>nat k < 2 ^ nat k\<close>
+ by simp
+ then have \<open>int (nat k) < int (2 ^ nat k)\<close>
+ by (simp only: of_nat_less_iff)
ultimately have *: \<open>k div 2 ^ nat k = 0\<close>
by simp
show thesis
@@ -546,8 +544,10 @@
next
case False
moreover from power_gt_expt [of 2 \<open>nat (- k)\<close>]
- have \<open>- k \<le> 2 ^ nat (- k)\<close>
+ have \<open>nat (- k) < 2 ^ nat (- k)\<close>
by simp
+ then have \<open>int (nat (- k)) < int (2 ^ nat (- k))\<close>
+ by (simp only: of_nat_less_iff)
ultimately have \<open>- k div - (2 ^ nat (- k)) = - 1\<close>
by (subst div_pos_neg_trivial) simp_all
then have *: \<open>k div 2 ^ nat (- k) = - 1\<close>
@@ -1520,6 +1520,17 @@
for k :: int
by (simp add: signed_take_bit_def not_less concat_bit_def)
+lemma signed_take_bit_int_greater_eq_minus_exp [simp]:
+ \<open>- (2 ^ n) \<le> signed_take_bit n k\<close>
+ for k :: int
+ by (simp add: signed_take_bit_eq_take_bit_shift)
+
+lemma signed_take_bit_int_less_exp [simp]:
+ \<open>signed_take_bit n k < 2 ^ n\<close>
+ for k :: int
+ using take_bit_int_less_exp [of \<open>Suc n\<close>]
+ by (simp add: signed_take_bit_eq_take_bit_shift)
+
lemma signed_take_bit_int_eq_self_iff:
\<open>signed_take_bit n k = k \<longleftrightarrow> - (2 ^ n) \<le> k \<and> k < 2 ^ n\<close>
for k :: int
--- a/src/HOL/Library/Cardinality.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Library/Cardinality.thy Thu Jul 08 08:44:18 2021 +0200
@@ -387,147 +387,4 @@
by intro_classes (simp_all add: UNIV_finite_5 card_UNIV_finite_5_def finite_UNIV_finite_5_def)
end
-subsection \<open>Code setup for sets\<close>
-
-text \<open>
- Implement \<^term>\<open>CARD('a)\<close> via \<^term>\<open>card_UNIV\<close> and provide
- implementations for \<^term>\<open>finite\<close>, \<^term>\<open>card\<close>, \<^term>\<open>(\<subseteq>)\<close>,
- and \<^term>\<open>(=)\<close>if the calling context already provides \<^class>\<open>finite_UNIV\<close>
- and \<^class>\<open>card_UNIV\<close> instances. If we implemented the latter
- always via \<^term>\<open>card_UNIV\<close>, we would require instances of essentially all
- element types, i.e., a lot of instantiation proofs and -- at run time --
- possibly slow dictionary constructions.
-\<close>
-
-context
-begin
-
-qualified definition card_UNIV' :: "'a card_UNIV"
-where [code del]: "card_UNIV' = Phantom('a) CARD('a)"
-
-lemma CARD_code [code_unfold]:
- "CARD('a) = of_phantom (card_UNIV' :: 'a card_UNIV)"
-by(simp add: card_UNIV'_def)
-
-lemma card_UNIV'_code [code]:
- "card_UNIV' = card_UNIV"
-by(simp add: card_UNIV card_UNIV'_def)
-
end
-
-lemma card_Compl:
- "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
-by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest)
-
-context fixes xs :: "'a :: finite_UNIV list"
-begin
-
-qualified definition finite' :: "'a set \<Rightarrow> bool"
-where [simp, code del, code_abbrev]: "finite' = finite"
-
-lemma finite'_code [code]:
- "finite' (set xs) \<longleftrightarrow> True"
- "finite' (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
-by(simp_all add: card_gt_0_iff finite_UNIV)
-
-end
-
-context fixes xs :: "'a :: card_UNIV list"
-begin
-
-qualified definition card' :: "'a set \<Rightarrow> nat"
-where [simp, code del, code_abbrev]: "card' = card"
-
-lemma card'_code [code]:
- "card' (set xs) = length (remdups xs)"
- "card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)"
-by(simp_all add: List.card_set card_Compl card_UNIV)
-
-
-qualified definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
-where [simp, code del, code_abbrev]: "subset' = (\<subseteq>)"
-
-lemma subset'_code [code]:
- "subset' A (List.coset ys) \<longleftrightarrow> (\<forall>y \<in> set ys. y \<notin> A)"
- "subset' (set ys) B \<longleftrightarrow> (\<forall>y \<in> set ys. y \<in> B)"
- "subset' (List.coset xs) (set ys) \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card(set (xs @ ys)) = n)"
-by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card])
- (metis finite_compl finite_set rev_finite_subset)
-
-qualified definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
-where [simp, code del, code_abbrev]: "eq_set = (=)"
-
-lemma eq_set_code [code]:
- fixes ys
- defines "rhs \<equiv>
- let n = CARD('a)
- in if n = 0 then False else
- let xs' = remdups xs; ys' = remdups ys
- in length xs' + length ys' = n \<and> (\<forall>x \<in> set xs'. x \<notin> set ys') \<and> (\<forall>y \<in> set ys'. y \<notin> set xs')"
- shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs"
- and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs"
- and "eq_set (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)"
- and "eq_set (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)"
-proof goal_cases
- {
- case 1
- show ?case (is "?lhs \<longleftrightarrow> ?rhs")
- proof
- show ?rhs if ?lhs
- using that
- by (auto simp add: rhs_def Let_def List.card_set[symmetric]
- card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV
- Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
- show ?lhs if ?rhs
- proof -
- have "\<lbrakk> \<forall>y\<in>set xs. y \<notin> set ys; \<forall>x\<in>set ys. x \<notin> set xs \<rbrakk> \<Longrightarrow> set xs \<inter> set ys = {}" by blast
- with that show ?thesis
- by (auto simp add: rhs_def Let_def List.card_set[symmetric]
- card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"]
- dest: card_eq_UNIV_imp_eq_UNIV split: if_split_asm)
- qed
- qed
- }
- moreover
- case 2
- ultimately show ?case unfolding eq_set_def by blast
-next
- case 3
- show ?case unfolding eq_set_def List.coset_def by blast
-next
- case 4
- show ?case unfolding eq_set_def List.coset_def by blast
-qed
-
-end
-
-text \<open>
- Provide more informative exceptions than Match for non-rewritten cases.
- If generated code raises one these exceptions, then a code equation calls
- the mentioned operator for an element type that is not an instance of
- \<^class>\<open>card_UNIV\<close> and is therefore not implemented via \<^term>\<open>card_UNIV\<close>.
- Constrain the element type with sort \<^class>\<open>card_UNIV\<close> to change this.
-\<close>
-
-lemma card_coset_error [code]:
- "card (List.coset xs) =
- Code.abort (STR ''card (List.coset _) requires type class instance card_UNIV'')
- (\<lambda>_. card (List.coset xs))"
-by(simp)
-
-lemma coset_subseteq_set_code [code]:
- "List.coset xs \<subseteq> set ys \<longleftrightarrow>
- (if xs = [] \<and> ys = [] then False
- else Code.abort
- (STR ''subset_eq (List.coset _) (List.set _) requires type class instance card_UNIV'')
- (\<lambda>_. List.coset xs \<subseteq> set ys))"
-by simp
-
-notepad begin \<comment> \<open>test code setup\<close>
-have "List.coset [True] = set [False] \<and>
- List.coset [] \<subseteq> List.set [True, False] \<and>
- finite (List.coset [True])"
- by eval
-end
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Cardinality.thy Thu Jul 08 08:44:18 2021 +0200
@@ -0,0 +1,147 @@
+subsection \<open>Code setup for sets with cardinality type information\<close>
+
+theory Code_Cardinality imports Cardinality begin
+
+text \<open>
+ Implement \<^term>\<open>CARD('a)\<close> via \<^term>\<open>card_UNIV\<close> and provide
+ implementations for \<^term>\<open>finite\<close>, \<^term>\<open>card\<close>, \<^term>\<open>(\<subseteq>)\<close>,
+ and \<^term>\<open>(=)\<close>if the calling context already provides \<^class>\<open>finite_UNIV\<close>
+ and \<^class>\<open>card_UNIV\<close> instances. If we implemented the latter
+ always via \<^term>\<open>card_UNIV\<close>, we would require instances of essentially all
+ element types, i.e., a lot of instantiation proofs and -- at run time --
+ possibly slow dictionary constructions.
+\<close>
+
+context
+begin
+
+qualified definition card_UNIV' :: "'a card_UNIV"
+where [code del]: "card_UNIV' = Phantom('a) CARD('a)"
+
+lemma CARD_code [code_unfold]:
+ "CARD('a) = of_phantom (card_UNIV' :: 'a card_UNIV)"
+by(simp add: card_UNIV'_def)
+
+lemma card_UNIV'_code [code]:
+ "card_UNIV' = card_UNIV"
+by(simp add: card_UNIV card_UNIV'_def)
+
+end
+
+lemma card_Compl:
+ "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
+by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest)
+
+context fixes xs :: "'a :: finite_UNIV list"
+begin
+
+qualified definition finite' :: "'a set \<Rightarrow> bool"
+where [simp, code del, code_abbrev]: "finite' = finite"
+
+lemma finite'_code [code]:
+ "finite' (set xs) \<longleftrightarrow> True"
+ "finite' (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
+by(simp_all add: card_gt_0_iff finite_UNIV)
+
+end
+
+context fixes xs :: "'a :: card_UNIV list"
+begin
+
+qualified definition card' :: "'a set \<Rightarrow> nat"
+where [simp, code del, code_abbrev]: "card' = card"
+
+lemma card'_code [code]:
+ "card' (set xs) = length (remdups xs)"
+ "card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)"
+by(simp_all add: List.card_set card_Compl card_UNIV)
+
+
+qualified definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+where [simp, code del, code_abbrev]: "subset' = (\<subseteq>)"
+
+lemma subset'_code [code]:
+ "subset' A (List.coset ys) \<longleftrightarrow> (\<forall>y \<in> set ys. y \<notin> A)"
+ "subset' (set ys) B \<longleftrightarrow> (\<forall>y \<in> set ys. y \<in> B)"
+ "subset' (List.coset xs) (set ys) \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card(set (xs @ ys)) = n)"
+by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card])
+ (metis finite_compl finite_set rev_finite_subset)
+
+qualified definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+where [simp, code del, code_abbrev]: "eq_set = (=)"
+
+lemma eq_set_code [code]:
+ fixes ys
+ defines "rhs \<equiv>
+ let n = CARD('a)
+ in if n = 0 then False else
+ let xs' = remdups xs; ys' = remdups ys
+ in length xs' + length ys' = n \<and> (\<forall>x \<in> set xs'. x \<notin> set ys') \<and> (\<forall>y \<in> set ys'. y \<notin> set xs')"
+ shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs"
+ and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs"
+ and "eq_set (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)"
+ and "eq_set (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)"
+proof goal_cases
+ {
+ case 1
+ show ?case (is "?lhs \<longleftrightarrow> ?rhs")
+ proof
+ show ?rhs if ?lhs
+ using that
+ by (auto simp add: rhs_def Let_def List.card_set[symmetric]
+ card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV
+ Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
+ show ?lhs if ?rhs
+ proof -
+ have "\<lbrakk> \<forall>y\<in>set xs. y \<notin> set ys; \<forall>x\<in>set ys. x \<notin> set xs \<rbrakk> \<Longrightarrow> set xs \<inter> set ys = {}" by blast
+ with that show ?thesis
+ by (auto simp add: rhs_def Let_def List.card_set[symmetric]
+ card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"]
+ dest: card_eq_UNIV_imp_eq_UNIV split: if_split_asm)
+ qed
+ qed
+ }
+ moreover
+ case 2
+ ultimately show ?case unfolding eq_set_def by blast
+next
+ case 3
+ show ?case unfolding eq_set_def List.coset_def by blast
+next
+ case 4
+ show ?case unfolding eq_set_def List.coset_def by blast
+qed
+
+end
+
+text \<open>
+ Provide more informative exceptions than Match for non-rewritten cases.
+ If generated code raises one these exceptions, then a code equation calls
+ the mentioned operator for an element type that is not an instance of
+ \<^class>\<open>card_UNIV\<close> and is therefore not implemented via \<^term>\<open>card_UNIV\<close>.
+ Constrain the element type with sort \<^class>\<open>card_UNIV\<close> to change this.
+\<close>
+
+lemma card_coset_error [code]:
+ "card (List.coset xs) =
+ Code.abort (STR ''card (List.coset _) requires type class instance card_UNIV'')
+ (\<lambda>_. card (List.coset xs))"
+by(simp)
+
+lemma coset_subseteq_set_code [code]:
+ "List.coset xs \<subseteq> set ys \<longleftrightarrow>
+ (if xs = [] \<and> ys = [] then False
+ else Code.abort
+ (STR ''subset_eq (List.coset _) (List.set _) requires type class instance card_UNIV'')
+ (\<lambda>_. List.coset xs \<subseteq> set ys))"
+by simp
+
+notepad begin \<comment> \<open>test code setup\<close>
+have "List.coset [True] = set [False] \<and>
+ List.coset [] \<subseteq> List.set [True, False] \<and>
+ finite (List.coset [True])"
+ by eval
+
+end
+
+end
\ No newline at end of file
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Jul 08 08:44:18 2021 +0200
@@ -1305,11 +1305,24 @@
using assms(1) continuous_at_enn2ereal isCont_tendsto_compose x by fastforce
qed
-lemma tendsto_ennreal_iff[simp]:
- "\<forall>\<^sub>F x in F. 0 \<le> f x \<Longrightarrow> 0 \<le> x \<Longrightarrow> ((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal x) F \<longleftrightarrow> (f \<longlongrightarrow> x) F"
- by (auto dest: tendsto_ennrealD)
- (auto simp: ennreal_def
- intro!: continuous_on_tendsto_compose[OF continuous_on_e2ennreal[of UNIV]] tendsto_max)
+lemma tendsto_ennreal_iff [simp]:
+ \<open>((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal x) F \<longleftrightarrow> (f \<longlongrightarrow> x) F\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+ if \<open>\<forall>\<^sub>F x in F. 0 \<le> f x\<close> \<open>0 \<le> x\<close>
+proof
+ assume \<open>?P\<close>
+ then show \<open>?Q\<close>
+ using that by (rule tendsto_ennrealD)
+next
+ assume \<open>?Q\<close>
+ have \<open>continuous_on UNIV ereal\<close>
+ using continuous_on_ereal [of _ id] by simp
+ then have \<open>continuous_on UNIV (e2ennreal \<circ> ereal)\<close>
+ by (rule continuous_on_compose) (simp_all add: continuous_on_e2ennreal)
+ then have \<open>((\<lambda>x. (e2ennreal \<circ> ereal) (f x)) \<longlongrightarrow> (e2ennreal \<circ> ereal) x) F\<close>
+ using \<open>?Q\<close> by (rule continuous_on_tendsto_compose) simp_all
+ then show \<open>?P\<close>
+ by (simp flip: e2ennreal_ereal)
+qed
lemma tendsto_enn2ereal_iff[simp]: "((\<lambda>i. enn2ereal (f i)) \<longlongrightarrow> enn2ereal x) F \<longleftrightarrow> (f \<longlongrightarrow> x) F"
using continuous_on_enn2ereal[THEN continuous_on_tendsto_compose, of f x F]
--- a/src/HOL/Library/Indicator_Function.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Library/Indicator_Function.thy Thu Jul 08 08:44:18 2021 +0200
@@ -77,7 +77,12 @@
lemma indicator_vimage: "indicator (f -` A) x = indicator A (f x)"
by (auto split: split_indicator)
-lemma (* FIXME unnamed!? *)
+lemma mult_indicator_cong:
+ fixes f g :: "_ \<Rightarrow> 'a :: semiring_1"
+ shows "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> indicator A x * f x = indicator A x * g x"
+ by (auto simp: indicator_def)
+
+lemma
fixes f :: "'a \<Rightarrow> 'b::semiring_1"
assumes "finite A"
shows sum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"
--- a/src/HOL/Library/Library.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Library/Library.thy Thu Jul 08 08:44:18 2021 +0200
@@ -10,6 +10,7 @@
Boolean_Algebra
Bourbaki_Witt_Fixpoint
Char_ord
+ Code_Cardinality
Code_Lazy
Code_Test
Combine_PER
--- a/src/HOL/Limits.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Limits.thy Thu Jul 08 08:44:18 2021 +0200
@@ -1777,7 +1777,15 @@
qed
lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 0) F"
- by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
+ by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
+
+lemma filterlim_inverse_at_top_iff:
+ "eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> (LIM x F. inverse (f x) :> at_top) \<longleftrightarrow> (f \<longlongrightarrow> (0 :: real)) F"
+ by (auto dest: tendsto_inverse_0_at_top filterlim_inverse_at_top)
+
+lemma filterlim_at_top_iff_inverse_0:
+ "eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> (LIM x F. f x :> at_top) \<longleftrightarrow> ((inverse \<circ> f) \<longlongrightarrow> (0 :: real)) F"
+ using filterlim_inverse_at_top_iff [of "inverse \<circ> f"] by auto
lemma real_tendsto_divide_at_top:
fixes c::"real"
--- a/src/HOL/Nonstandard_Analysis/NSComplex.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSComplex.thy Thu Jul 08 08:44:18 2021 +0200
@@ -45,7 +45,7 @@
where "hsgn = *f* sgn"
definition harg :: "hcomplex \<Rightarrow> hypreal"
- where "harg = *f* arg"
+ where "harg = *f* Arg"
definition \<comment> \<open>abbreviation for \<open>cos a + i sin a\<close>\<close>
hcis :: "hypreal \<Rightarrow> hcomplex"
--- a/src/HOL/Parity.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Parity.thy Thu Jul 08 08:44:18 2021 +0200
@@ -1818,6 +1818,10 @@
instance int :: unique_euclidean_semiring_with_bit_shifts ..
+lemma bit_numeral_int_iff [bit_simps]:
+ \<open>bit (numeral m :: int) n \<longleftrightarrow> bit (numeral m :: nat) n\<close>
+ using bit_of_nat_iff_bit [of \<open>numeral m\<close> n] by simp
+
lemma bit_not_int_iff':
\<open>bit (- k - 1) n \<longleftrightarrow> \<not> bit k n\<close>
for k :: int
--- a/src/HOL/Power.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Power.thy Thu Jul 08 08:44:18 2021 +0200
@@ -908,7 +908,7 @@
lemma power_gt_expt: "n > Suc 0 \<Longrightarrow> n^k > k"
by (induction k) (auto simp: less_trans_Suc n_less_m_mult_n)
-lemma less_exp:
+lemma less_exp [simp]:
\<open>n < 2 ^ n\<close>
by (simp add: power_gt_expt)
--- a/src/HOL/Series.thy Thu Jul 08 08:42:36 2021 +0200
+++ b/src/HOL/Series.thy Thu Jul 08 08:44:18 2021 +0200
@@ -58,7 +58,7 @@
by simp
lemma sums_cong: "(\<And>n. f n = g n) \<Longrightarrow> f sums c \<longleftrightarrow> g sums c"
- by (drule ext) simp
+ by presburger
lemma sums_summable: "f sums l \<Longrightarrow> summable f"
by (simp add: sums_def summable_def, blast)
@@ -67,8 +67,7 @@
by (simp add: summable_def sums_def convergent_def)
lemma summable_iff_convergent': "summable f \<longleftrightarrow> convergent (\<lambda>n. sum f {..n})"
- by (simp_all only: summable_iff_convergent convergent_def
- lessThan_Suc_atMost [symmetric] filterlim_sequentially_Suc[of "\<lambda>n. sum f {..<n}"])
+ by (simp add: convergent_def summable_def sums_def_le)
lemma suminf_eq_lim: "suminf f = lim (\<lambda>n. \<Sum>i<n. f i)"
by (simp add: suminf_def sums_def lim_def)
@@ -82,11 +81,10 @@
lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. sum f {n * k ..< n * k + k}) sums s"
apply (simp only: sums_def sum.nat_group tendsto_def eventually_sequentially)
apply (erule all_forward imp_forward exE| assumption)+
- apply (rule_tac x="N" in exI)
by (metis le_square mult.commute mult.left_neutral mult_le_cancel2 mult_le_mono)
lemma suminf_cong: "(\<And>n. f n = g n) \<Longrightarrow> suminf f = suminf g"
- by (rule arg_cong[of f g], rule ext) simp
+ by presburger
lemma summable_cong:
fixes f g :: "nat \<Rightarrow> 'a::real_normed_vector"
@@ -225,16 +223,13 @@
assumes "summable f" and pos: "\<And>n. 0 \<le> f n"
shows "suminf f = 0 \<longleftrightarrow> (\<forall>n. f n = 0)"
proof
- assume "suminf f = 0"
+ assume L: "suminf f = 0"
then have f: "(\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> 0"
using summable_LIMSEQ[of f] assms by simp
then have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
- proof (rule LIMSEQ_le_const)
- show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> sum f {..<n}" for i
- using pos by (intro exI[of _ "Suc i"] allI impI sum_mono2) auto
- qed
+ by (metis L \<open>summable f\<close> order_refl pos sum.infinite sum_le_suminf)
with pos show "\<forall>n. f n = 0"
- by (auto intro!: antisym)
+ by (simp add: order.antisym)
qed (metis suminf_zero fun_eq_iff)
lemma suminf_pos_iff: "summable f \<Longrightarrow> (\<And>n. 0 \<le> f n) \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
@@ -735,11 +730,11 @@
proof (cases m n rule: linorder_class.le_cases)
assume "m \<le> n"
then show ?thesis
- by (metis Groups_Big.sum_diff N finite_lessThan lessThan_minus_lessThan lessThan_subset_iff norm_minus_commute \<open>m\<ge>N\<close>)
+ by (metis N finite_lessThan lessThan_minus_lessThan lessThan_subset_iff norm_minus_commute sum_diff \<open>m\<ge>N\<close>)
next
assume "n \<le> m"
then show ?thesis
- by (metis Groups_Big.sum_diff N finite_lessThan lessThan_minus_lessThan lessThan_subset_iff \<open>n\<ge>N\<close>)
+ by (metis N finite_lessThan lessThan_minus_lessThan lessThan_subset_iff sum_diff \<open>n\<ge>N\<close>)
qed
then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (sum f {..<m} - sum f {..<n}) < e"
by blast
@@ -748,13 +743,14 @@
lemma summable_Cauchy':
fixes f :: "nat \<Rightarrow> 'a :: banach"
- assumes "eventually (\<lambda>m. \<forall>n\<ge>m. norm (sum f {m..<n}) \<le> g m) sequentially"
- assumes "filterlim g (nhds 0) sequentially"
+ assumes ev: "eventually (\<lambda>m. \<forall>n\<ge>m. norm (sum f {m..<n}) \<le> g m) sequentially"
+ assumes g0: "g \<longlonglongrightarrow> 0"
shows "summable f"
proof (subst summable_Cauchy, intro allI impI, goal_cases)
case (1 e)
- from order_tendstoD(2)[OF assms(2) this] and assms(1)
- have "eventually (\<lambda>m. \<forall>n. norm (sum f {m..<n}) < e) at_top"
+ then have "\<forall>\<^sub>F x in sequentially. g x < e"
+ using g0 order_tendstoD(2) by blast
+ with ev have "eventually (\<lambda>m. \<forall>n. norm (sum f {m..<n}) < e) at_top"
proof eventually_elim
case (elim m)
show ?case
--- a/src/Pure/Admin/build_release.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/Admin/build_release.scala Thu Jul 08 08:44:18 2021 +0200
@@ -861,7 +861,7 @@
var rev = ""
val getopts = Getopts("""
-Usage: Admin/build_release [OPTIONS] BASE_DIR
+Usage: Admin/build_release [OPTIONS]
Options are:
-A REV corresponding AFP changeset id
--- a/src/Pure/Admin/isabelle_cronjob.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Thu Jul 08 08:44:18 2021 +0200
@@ -209,6 +209,16 @@
val remote_builds_old: List[Remote_Build] =
List(
+ Remote_Build("Linux A", "i21of4", user = "i21isatest",
+ proxy_host = "lxbroy10", proxy_user = "i21isatest",
+ self_update = true,
+ options = "-m32 -M1x4,2,4" +
+ " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
+ " -e ISABELLE_GHC_SETUP=true" +
+ " -e ISABELLE_MLTON=mlton" +
+ " -e ISABELLE_SMLNJ=sml" +
+ " -e ISABELLE_SWIPL=swipl",
+ args = "-a -d '~~/src/Benchmarks'"),
Remote_Build("Linux A", "lxbroy9",
java_heap = "2g", options = "-m32 -B -M1x2,2", args = "-N -g timing"),
Remote_Build("Linux Benchmarks", "lxbroy5", historic = true, history = 90,
@@ -303,23 +313,13 @@
val remote_builds1: List[List[Remote_Build]] =
{
List(
- List(Remote_Build("Linux A", "i21of4", user = "i21isatest",
- proxy_host = "lxbroy10", proxy_user = "i21isatest",
- self_update = true,
- options = "-m32 -M1x4,2,4" +
- " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
- " -e ISABELLE_GHC_SETUP=true" +
- " -e ISABELLE_MLTON=mlton" +
- " -e ISABELLE_SMLNJ=sml" +
- " -e ISABELLE_SWIPL=swipl",
- args = "-a -d '~~/src/Benchmarks'")),
List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90,
options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
List(Remote_Build("macOS 10.13 High Sierra", "lapbroy68",
options = "-m32 -B -M1,2,4 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
self_update = true, args = "-a -d '~~/src/Benchmarks'")),
List(
- Remote_Build("macOS 11.1 Big Sur", "mini1",
+ Remote_Build("macOS 11 Big Sur", "mini1",
options = "-m32 -B -M1x2,2,4 -p pide_session=false" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
" -e ISABELLE_GHC_SETUP=true" +
--- a/src/Pure/GUI/gui.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/GUI/gui.scala Thu Jul 08 08:44:18 2021 +0200
@@ -6,6 +6,7 @@
package isabelle
+import java.util.{Map => JMap}
import java.awt.{Component, Container, Font, Image, Insets, KeyboardFocusManager, Window, Point,
Rectangle, Dimension, GraphicsEnvironment, MouseInfo, Toolkit}
import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute}
@@ -20,7 +21,7 @@
{
/* Swing look-and-feel */
- def init_laf(): Unit = com.formdev.flatlaf.FlatLightLaf.install()
+ def init_laf(): Unit = com.formdev.flatlaf.FlatLightLaf.setup()
def current_laf: String = UIManager.getLookAndFeel.getClass.getName()
@@ -299,7 +300,7 @@
font.getLineMetrics("", new FontRenderContext(null, false, false))
def transform_font(font: Font, transform: AffineTransform): Font =
- font.deriveFont(java.util.Map.of(TextAttribute.TRANSFORM, new TransformAttribute(transform)))
+ font.deriveFont(JMap.of(TextAttribute.TRANSFORM, new TransformAttribute(transform)))
def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font =
new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
--- a/src/Pure/General/file.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/General/file.scala Thu Jul 08 08:44:18 2021 +0200
@@ -15,13 +15,11 @@
import java.nio.file.attribute.BasicFileAttributes
import java.net.{URL, MalformedURLException}
import java.util.zip.{GZIPInputStream, GZIPOutputStream}
-import java.util.regex.Pattern
import java.util.EnumSet
import org.tukaani.xz.{XZInputStream, XZOutputStream}
import scala.collection.mutable
-import scala.util.matching.Regex
object File
@@ -31,20 +29,7 @@
def standard_path(path: Path): String = path.expand.implode
def standard_path(platform_path: String): String =
- if (Platform.is_windows) {
- val Platform_Root = new Regex("(?i)" +
- Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""")
- val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
-
- platform_path.replace('/', '\\') match {
- case Platform_Root(rest) => "/" + rest.replace('\\', '/')
- case Drive(letter, rest) =>
- "/cygdrive/" + Word.lowercase(letter) +
- (if (rest == "") "" else "/" + rest.replace('\\', '/'))
- case path => path.replace('\\', '/')
- }
- }
- else platform_path
+ isabelle.setup.Environment.standard_path(platform_path)
def standard_path(file: JFile): String = standard_path(file.getPath)
@@ -60,36 +45,8 @@
/* platform path (Windows or Posix) */
- private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
- private val Named_Root = new Regex("//+([^/]*)(.*)")
-
def platform_path(standard_path: String): String =
- if (Platform.is_windows) {
- val result_path = new StringBuilder
- val rest =
- standard_path match {
- case Cygdrive(drive, rest) =>
- result_path ++= (Word.uppercase(drive) + ":" + JFile.separator)
- rest
- case Named_Root(root, rest) =>
- result_path ++= JFile.separator
- result_path ++= JFile.separator
- result_path ++= root
- rest
- case path if path.startsWith("/") =>
- result_path ++= Isabelle_System.cygwin_root()
- path
- case path => path
- }
- for (p <- space_explode('/', rest) if p != "") {
- val len = result_path.length
- if (len > 0 && result_path(len - 1) != JFile.separatorChar)
- result_path += JFile.separatorChar
- result_path ++= p
- }
- result_path.toString
- }
- else standard_path
+ isabelle.setup.Environment.platform_path(standard_path)
def platform_path(path: Path): String = platform_path(standard_path(path))
def platform_file(path: Path): JFile = new JFile(platform_path(path))
--- a/src/Pure/General/file_watcher.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/General/file_watcher.scala Thu Jul 08 08:44:18 2021 +0200
@@ -7,6 +7,7 @@
package isabelle
+import java.util.{List => JList}
import java.io.{File => JFile}
import java.nio.file.FileSystems
import java.nio.file.{WatchKey, WatchEvent, Path => JPath}
@@ -102,7 +103,7 @@
st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match {
case Some(dir) =>
val events: Iterable[WatchEvent[JPath]] =
- key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]].asScala
+ key.pollEvents.asInstanceOf[JList[WatchEvent[JPath]]].asScala
val remove = if (key.reset) None else Some(dir)
val changed =
events.iterator.foldLeft(Set.empty[JFile]) {
--- a/src/Pure/General/mailman.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/General/mailman.scala Thu Jul 08 08:44:18 2021 +0200
@@ -67,5 +67,5 @@
archive(Url("https://lists.cam.ac.uk/pipermail/cl-isabelle-users"), name = "isabelle-users")
def isabelle_dev: Archive =
- archive(Url("https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev"))
+ archive(Url("https://mailmanbroy.in.tum.de/pipermail/isabelle-dev"))
}
--- a/src/Pure/General/path.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/General/path.scala Thu Jul 08 08:44:18 2021 +0200
@@ -8,6 +8,7 @@
package isabelle
+import java.util.{Map => JMap}
import java.io.{File => JFile}
import scala.util.matching.Regex
@@ -256,7 +257,7 @@
/* expand */
- def expand_env(env: Map[String, String]): Path =
+ def expand_env(env: JMap[String, String]): Path =
{
def eval(elem: Path.Elem): List[Path.Elem] =
elem match {
--- a/src/Pure/General/ssh.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/General/ssh.scala Thu Jul 08 08:44:18 2021 +0200
@@ -7,6 +7,7 @@
package isabelle
+import java.util.{Map => JMap}
import java.io.{InputStream, OutputStream, ByteArrayOutputStream}
import scala.collection.mutable
@@ -349,10 +350,10 @@
override def close(): Unit = { sftp.disconnect; session.disconnect; on_close() }
- val settings: Map[String, String] =
+ val settings: JMap[String, String] =
{
val home = sftp.getHome
- Map("HOME" -> home, "USER_HOME" -> home)
+ JMap.of("HOME", home, "USER_HOME", home)
}
override def expand_path(path: Path): Path = path.expand_env(settings)
def remote_path(path: Path): String = expand_path(path).implode
--- a/src/Pure/ML/ml_process.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/ML/ml_process.scala Thu Jul 08 08:44:18 2021 +0200
@@ -7,6 +7,7 @@
package isabelle
+import java.util.{Map => JMap, HashMap}
import java.io.{File => JFile}
@@ -22,7 +23,7 @@
args: List[String] = Nil,
modes: List[String] = Nil,
cwd: JFile = null,
- env: Map[String, String] = Isabelle_System.settings(),
+ env: JMap[String, String] = Isabelle_System.settings(),
redirect: Boolean = false,
cleanup: () => Unit = () => (),
session_base: Option[Sessions.Base] = None): Bash.Process =
@@ -70,11 +71,11 @@
if (modes.isEmpty) Nil
else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes))
+
// options
val isabelle_process_options = Isabelle_System.tmp_file("options")
Isabelle_System.chmod("600", File.path(isabelle_process_options))
File.write(isabelle_process_options, YXML.string_of_body(options.encode))
- val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
// session base
@@ -99,11 +100,6 @@
// ISABELLE_TMP
val isabelle_tmp = Isabelle_System.tmp_dir("process")
- val env_tmp =
- Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp),
- "POLYSTATSDIR" -> isabelle_tmp.getAbsolutePath)
-
- val env_functions = Map("ISABELLE_SCALA_FUNCTIONS" -> Scala.functions.mkString(","))
val ml_runtime_options =
{
@@ -123,11 +119,17 @@
(eval_init ::: eval_modes ::: eval_options ::: eval_init_session).flatMap(List("--eval", _)) :::
use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args
+ val bash_env = new HashMap(env)
+ bash_env.put("ISABELLE_PROCESS_OPTIONS", File.standard_path(isabelle_process_options))
+ bash_env.put("ISABELLE_TMP", File.standard_path(isabelle_tmp))
+ bash_env.put("POLYSTATSDIR", isabelle_tmp.getAbsolutePath)
+ bash_env.put("ISABELLE_SCALA_FUNCTIONS", Scala.functions.mkString(","))
+
Bash.process(
options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
Bash.strings(bash_args),
cwd = cwd,
- env = env ++ env_options ++ env_tmp ++ env_functions,
+ env = bash_env,
redirect = redirect,
cleanup = () =>
{
--- a/src/Pure/System/bash.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/System/bash.scala Thu Jul 08 08:44:18 2021 +0200
@@ -7,9 +7,8 @@
package isabelle
-import java.io.{File => JFile, BufferedReader, InputStreamReader,
- BufferedWriter, OutputStreamWriter}
-
+import java.util.{LinkedList, List => JList, Map => JMap}
+import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, File => JFile}
import scala.annotation.tailrec
import scala.jdk.OptionConverters._
@@ -50,7 +49,7 @@
def process(script: String,
cwd: JFile = null,
- env: Map[String, String] = Isabelle_System.settings(),
+ env: JMap[String, String] = Isabelle_System.settings(),
redirect: Boolean = false,
cleanup: () => Unit = () => ()): Process =
new Process(script, cwd, env, redirect, cleanup)
@@ -58,7 +57,7 @@
class Process private[Bash](
script: String,
cwd: JFile,
- env: Map[String, String],
+ env: JMap[String, String],
redirect: Boolean,
cleanup: () => Unit)
{
@@ -80,10 +79,10 @@
File.write(script_file, winpid_script)
private val proc =
- Isabelle_System.process(
- List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")),
+ isabelle.setup.Environment.process_builder(
+ JList.of(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")),
File.standard_path(timing_file), "bash", File.standard_path(script_file)),
- cwd = cwd, env = env, redirect = redirect)
+ cwd, env, redirect).start()
// channels
@@ -119,8 +118,10 @@
{
count <= 0 ||
{
- Isabelle_System.process_signal(group_pid, signal = s)
- val running = root_process_alive() || Isabelle_System.process_signal(group_pid)
+ isabelle.setup.Environment.kill_process(group_pid, s)
+ val running =
+ root_process_alive() ||
+ isabelle.setup.Environment.kill_process(group_pid, "0")
if (running) {
Time.seconds(0.1).sleep()
signal(s, count - 1)
@@ -138,7 +139,7 @@
def interrupt(): Unit = Isabelle_Thread.try_uninterruptible
{
- Isabelle_System.process_signal(group_pid, "INT")
+ isabelle.setup.Environment.kill_process(group_pid, "INT")
}
--- a/src/Pure/System/cygwin.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/System/cygwin.scala Thu Jul 08 08:44:18 2021 +0200
@@ -15,54 +15,4 @@
object Cygwin
{
- /* init (e.g. after extraction via 7zip) */
-
- def init(isabelle_root: String, cygwin_root: String): Unit =
- {
- require(Platform.is_windows, "Windows platform expected")
-
- def exec(cmdline: String*): Unit =
- {
- val cwd = new JFile(isabelle_root)
- val env = sys.env + ("CYGWIN" -> "nodosfilewarning")
- val proc = Isabelle_System.process(cmdline.toList, cwd = cwd, env = env, redirect = true)
- val (output, rc) = Isabelle_System.process_output(proc)
- if (rc != 0) error(output)
- }
-
- val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
- val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
-
- if (uninitialized) {
- val symlinks =
- {
- val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath
- Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
- }
- @tailrec def recover_symlinks(list: List[String]): Unit =
- {
- list match {
- case Nil | List("") =>
- case target :: content :: rest =>
- link(content, new JFile(isabelle_root, target))
- recover_symlinks(rest)
- case _ => error("Unbalanced symlinks list")
- }
- }
- recover_symlinks(symlinks)
-
- exec(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
- exec(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
- }
- }
-
- def link(content: String, target: JFile): Unit =
- {
- val target_path = target.toPath
-
- using(Files.newBufferedWriter(target_path, UTF8.charset))(
- _.write("!<symlink>" + content + "\u0000"))
-
- Files.setAttribute(target_path, "dos:system", true)
- }
}
--- a/src/Pure/System/isabelle_charset.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/System/isabelle_charset.scala Thu Jul 08 08:44:18 2021 +0200
@@ -7,6 +7,7 @@
package isabelle
+import java.util.{List => JList}
import java.nio.Buffer
import java.nio.{ByteBuffer, CharBuffer}
import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult}
@@ -45,6 +46,6 @@
{
// FIXME inactive
// Iterator(Isabelle_Charset.charset)
- java.util.List.of[Charset]().listIterator()
+ JList.of[Charset]().listIterator()
}
}
--- a/src/Pure/System/isabelle_process.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/System/isabelle_process.scala Thu Jul 08 08:44:18 2021 +0200
@@ -7,6 +7,7 @@
package isabelle
+import java.util.{Map => JMap}
import java.io.{File => JFile}
@@ -23,7 +24,7 @@
eval_main: String = "",
modes: List[String] = Nil,
cwd: JFile = null,
- env: Map[String, String] = Isabelle_System.settings()): Isabelle_Process =
+ env: JMap[String, String] = Isabelle_System.settings()): Isabelle_Process =
{
val channel = System_Channel()
val process =
--- a/src/Pure/System/isabelle_system.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu Jul 08 08:44:18 2021 +0200
@@ -1,63 +1,39 @@
/* Title: Pure/System/isabelle_system.scala
Author: Makarius
-Fundamental Isabelle system environment: quasi-static module with
-optional init operation.
+Miscellaneous Isabelle system operations.
*/
package isabelle
+import java.util.{Map => JMap}
import java.io.{File => JFile, IOException}
import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult,
StandardCopyOption, FileSystemException}
import java.nio.file.attribute.BasicFileAttributes
-import scala.jdk.CollectionConverters._
-
object Isabelle_System
{
- /** bootstrap information **/
+ /* settings */
- def jdk_home(): String =
- {
- val java_home = System.getProperty("java.home", "")
- val home = new JFile(java_home)
- val parent = home.getParent
- if (home.getName == "jre" && parent != null &&
- (new JFile(new JFile(parent, "bin"), "javac")).exists) parent
- else java_home
- }
+ def settings(): JMap[String, String] = isabelle.setup.Environment.settings()
- def bootstrap_directory(
- preference: String, envar: String, property: String, description: String): String =
- {
- val value =
- proper_string(preference) orElse // explicit argument
- proper_string(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool
- proper_string(System.getProperty(property)) getOrElse // e.g. via JVM application boot process
- error("Unknown " + description + " directory")
+ def getenv(name: String, env: JMap[String, String] = settings()): String =
+ Option(env.get(name)).getOrElse("")
- if ((new JFile(value)).isDirectory) value
- else error("Bad " + description + " directory " + quote(value))
- }
+ def getenv_strict(name: String, env: JMap[String, String] = settings()): String =
+ proper_string(getenv(name, env)) getOrElse
+ error("Undefined Isabelle environment variable: " + quote(name))
-
- /** implicit settings environment **/
+ /* services */
abstract class Service
- @volatile private var _settings: Option[Map[String, String]] = None
@volatile private var _services: Option[List[Class[Service]]] = None
- def settings(): Map[String, String] =
- {
- if (_settings.isEmpty) init() // unsynchronized check
- _settings.get
- }
-
def services(): List[Class[Service]] =
{
if (_services.isEmpty) init() // unsynchronized check
@@ -68,110 +44,32 @@
for { c1 <- services() if Library.is_subclass(c1, c) }
yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
- def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized
- {
- if (_settings.isEmpty || _services.isEmpty) {
- val isabelle_root1 =
- bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
- val cygwin_root1 =
- if (Platform.is_windows)
- bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
- else ""
-
- if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1)
-
- def set_cygwin_root(): Unit =
- {
- if (Platform.is_windows)
- _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
- }
-
- set_cygwin_root()
-
- def default(env: Map[String, String], entry: (String, String)): Map[String, String] =
- if (env.isDefinedAt(entry._1) || entry._2 == "") env
- else env + entry
-
- val env =
- {
- val temp_windows =
- {
- val temp = if (Platform.is_windows) System.getenv("TEMP") else null
- if (temp != null && temp.contains('\\')) temp else ""
- }
- val user_home = System.getProperty("user.home", "")
- val isabelle_app = System.getProperty("isabelle.app", "")
-
- default(
- default(
- default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())),
- "TEMP_WINDOWS" -> temp_windows),
- "HOME" -> user_home),
- "ISABELLE_APP" -> "true")
- }
+ /* init settings + services */
- val settings =
- {
- val dump = JFile.createTempFile("settings", null)
- dump.deleteOnExit
- try {
- val cmd1 =
- if (Platform.is_windows)
- List(cygwin_root1 + "\\bin\\bash", "-l",
- File.standard_path(isabelle_root1 + "\\bin\\isabelle"))
- else
- List(isabelle_root1 + "/bin/isabelle")
- val cmd = cmd1 ::: List("getenv", "-d", dump.toString)
-
- val (output, rc) = process_output(process(cmd, env = env, redirect = true))
- if (rc != 0) error(output)
-
- val entries =
- space_explode('\u0000', File.read(dump)).flatMap(
- {
- case Properties.Eq(a, b) => Some(a -> b)
- case s => if (s.isEmpty || s.startsWith("=")) None else Some(s -> "")
- }).toMap
- entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
- }
- finally { dump.delete }
+ def init(isabelle_root: String = "", cygwin_root: String = ""): Unit =
+ {
+ isabelle.setup.Environment.init(isabelle_root, cygwin_root)
+ synchronized {
+ if (_services.isEmpty) {
+ val variable = "ISABELLE_SCALA_SERVICES"
+ val services =
+ for (name <- space_explode(':', getenv_strict(variable)))
+ yield {
+ def err(msg: String): Nothing =
+ error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
+ try { Class.forName(name).asInstanceOf[Class[Service]] }
+ catch {
+ case _: ClassNotFoundException => err("Class not found")
+ case exn: Throwable => err(Exn.message(exn))
+ }
+ }
+ _services = Some(services)
}
- _settings = Some(settings)
- set_cygwin_root()
-
- val variable = "ISABELLE_SCALA_SERVICES"
- val services =
- for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable))))
- yield {
- def err(msg: String): Nothing =
- error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
- try { Class.forName(name).asInstanceOf[Class[Service]] }
- catch {
- case _: ClassNotFoundException => err("Class not found")
- case exn: Throwable => err(Exn.message(exn))
- }
- }
- _services = Some(services)
}
}
- /* getenv -- dynamic process environment */
-
- private def getenv_error(name: String): Nothing =
- error("Undefined Isabelle environment variable: " + quote(name))
-
- def getenv(name: String, env: Map[String, String] = settings()): String =
- env.getOrElse(name, "")
-
- def getenv_strict(name: String, env: Map[String, String] = settings()): String =
- proper_string(getenv(name, env)) getOrElse
- error("Undefined Isabelle environment variable: " + quote(name))
-
- def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
-
-
/* getetc -- static distribution parameters */
def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] =
@@ -352,12 +250,13 @@
if (force) target.delete
+ def cygwin_link(): Unit =
+ isabelle.setup.Environment.cygwin_link(File.standard_path(src), target)
+
try { Files.createSymbolicLink(target.toPath, src_file.toPath) }
catch {
- case _: UnsupportedOperationException if Platform.is_windows =>
- Cygwin.link(File.standard_path(src), target)
- case _: FileSystemException if Platform.is_windows =>
- Cygwin.link(File.standard_path(src), target)
+ case _: UnsupportedOperationException if Platform.is_windows => cygwin_link()
+ case _: FileSystemException if Platform.is_windows => cygwin_link()
}
}
@@ -458,59 +357,11 @@
/** external processes **/
- /* raw process */
-
- def process(command_line: List[String],
- cwd: JFile = null,
- env: Map[String, String] = settings(),
- redirect: Boolean = false): Process =
- {
- val proc = new ProcessBuilder
-
- // fragile on Windows:
- // see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160
- proc.command(command_line.asJava)
-
- if (cwd != null) proc.directory(cwd)
- if (env != null) {
- proc.environment.clear()
- for ((x, y) <- env) proc.environment.put(x, y)
- }
- proc.redirectErrorStream(redirect)
- proc.start
- }
-
- def process_output(proc: Process): (String, Int) =
- {
- proc.getOutputStream.close()
-
- val output = File.read_stream(proc.getInputStream)
- val rc =
- try { proc.waitFor }
- finally {
- proc.getInputStream.close()
- proc.getErrorStream.close()
- proc.destroy()
- Exn.Interrupt.dispose()
- }
- (output, rc)
- }
-
- def process_signal(group_pid: String, signal: String = "0"): Boolean =
- {
- val bash =
- if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe")
- else List("/usr/bin/env", "bash")
- val (_, rc) = process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid)))
- rc == 0
- }
-
-
/* GNU bash */
def bash(script: String,
cwd: JFile = null,
- env: Map[String, String] = settings(),
+ env: JMap[String, String] = settings(),
redirect: Boolean = false,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
--- a/src/Pure/System/platform.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/System/platform.scala Thu Jul 08 08:44:18 2021 +0200
@@ -11,9 +11,9 @@
{
/* platform family */
+ val is_windows: Boolean = isabelle.setup.Environment.is_windows()
val is_linux: Boolean = System.getProperty("os.name", "") == "Linux"
val is_macos: Boolean = System.getProperty("os.name", "") == "Mac OS X"
- val is_windows: Boolean = System.getProperty("os.name", "").startsWith("Windows")
val is_unix: Boolean = is_linux || is_macos
def is_arm: Boolean = cpu_arch.startsWith("arm")
--- a/src/Pure/System/progress.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/System/progress.scala Thu Jul 08 08:44:18 2021 +0200
@@ -7,6 +7,7 @@
package isabelle
+import java.util.{Map => JMap}
import java.io.{File => JFile}
@@ -50,7 +51,7 @@
def bash(script: String,
cwd: JFile = null,
- env: Map[String, String] = Isabelle_System.settings(),
+ env: JMap[String, String] = Isabelle_System.settings(),
redirect: Boolean = false,
echo: Boolean = false,
watchdog: Time = Time.zero,
--- a/src/Pure/Tools/build_job.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/Tools/build_job.scala Thu Jul 08 08:44:18 2021 +0200
@@ -7,6 +7,8 @@
package isabelle
+import java.util.HashMap
+
import scala.collection.mutable
@@ -217,9 +219,8 @@
val base = deps(parent)
val result_base = deps(session_name)
- val env =
- Isabelle_System.settings() +
- ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
+ val env = new HashMap(Isabelle_System.settings())
+ env.put("ISABELLE_ML_DEBUGGER", options.bool("ML_debugger").toString)
val is_pure = Sessions.is_pure(session_name)
--- a/src/Pure/Tools/scala_project.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/Tools/scala_project.scala Thu Jul 08 08:44:18 2021 +0200
@@ -111,12 +111,15 @@
if (project_dir.is_file || project_dir.is_dir)
error("Project directory already exists: " + project_dir)
- val src_dir = project_dir + Path.explode("src/main/scala")
val java_src_dir = project_dir + Path.explode("src/main/java")
val scala_src_dir = Isabelle_System.make_directory(project_dir + Path.explode("src/main/scala"))
Isabelle_System.copy_dir(Path.explode("~~/src/Tools/jEdit/dist/jEdit"), java_src_dir)
+ val isabelle_setup_dir = Path.explode("~~/src/Tools/Setup/isabelle")
+ if (symlinks) Isabelle_System.symlink(isabelle_setup_dir, java_src_dir)
+ else Isabelle_System.copy_dir(isabelle_setup_dir, java_src_dir)
+
val files = isabelle_files
isabelle_scala_files
--- a/src/Pure/Tools/spell_checker.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/Tools/spell_checker.scala Thu Jul 08 08:44:18 2021 +0200
@@ -9,6 +9,7 @@
import java.lang.Class
+import java.util.{List => JList}
import scala.collection.mutable
import scala.annotation.tailrec
@@ -223,7 +224,7 @@
{
val res =
Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]).
- invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
+ invoke(dict, word).asInstanceOf[JList[AnyRef]].toArray.toList.map(_.toString)
if (res.isEmpty) None else Some(res)
}
--- a/src/Pure/build-jars Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Pure/build-jars Thu Jul 08 08:44:18 2021 +0200
@@ -133,7 +133,6 @@
src/Pure/System/bash.scala
src/Pure/System/command_line.scala
src/Pure/System/components.scala
- src/Pure/System/cygwin.scala
src/Pure/System/executable.scala
src/Pure/System/getopts.scala
src/Pure/System/isabelle_charset.scala
--- a/src/Tools/Graphview/metrics.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Tools/Graphview/metrics.scala Thu Jul 08 08:44:18 2021 +0200
@@ -9,6 +9,7 @@
import isabelle._
+import java.util.HashMap
import java.awt.{Font, RenderingHints}
import java.awt.font.FontRenderContext
import java.awt.geom.Rectangle2D
@@ -18,7 +19,7 @@
{
val rendering_hints: RenderingHints =
{
- val hints = new java.util.HashMap[RenderingHints.Key, AnyRef]
+ val hints = new HashMap[RenderingHints.Key, AnyRef]
hints.put(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON)
hints.put(RenderingHints.KEY_FRACTIONALMETRICS, RenderingHints.VALUE_FRACTIONALMETRICS_ON)
new RenderingHints(hints)
--- a/src/Tools/Setup/.idea/.name Thu Jul 08 08:42:36 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-isabelle-setup
\ No newline at end of file
--- a/src/Tools/Setup/.idea/artifacts/Setup_jar.xml Thu Jul 08 08:42:36 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-<component name="ArtifactManager">
- <artifact type="jar" name="Setup:jar">
- <output-path>$PROJECT_DIR$/out/artifacts/</output-path>
- <root id="archive" name="Setup.jar">
- <element id="module-output" name="Setup" />
- </root>
- </artifact>
-</component>
\ No newline at end of file
--- a/src/Tools/Setup/.idea/codeStyles/Project.xml Thu Jul 08 08:42:36 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-<component name="ProjectCodeStyleConfiguration">
- <code_scheme name="Project" version="173">
- <option name="LINE_SEPARATOR" value=" " />
- <option name="SOFT_MARGINS" value="100" />
- <codeStyleSettings language="Scala">
- <option name="ALIGN_MULTILINE_PARAMETERS" value="false" />
- </codeStyleSettings>
- </code_scheme>
-</component>
\ No newline at end of file
--- a/src/Tools/Setup/.idea/codeStyles/codeStyleConfig.xml Thu Jul 08 08:42:36 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-<component name="ProjectCodeStyleConfiguration">
- <state>
- <option name="PREFERRED_PROJECT_CODE_STYLE" value="Default" />
- </state>
-</component>
\ No newline at end of file
--- a/src/Tools/Setup/.idea/misc.xml Thu Jul 08 08:42:36 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<project version="4">
- <component name="ProjectRootManager" version="2" languageLevel="JDK_11" default="true" project-jdk-name="11" project-jdk-type="JavaSDK">
- <output url="file://$PROJECT_DIR$/out" />
- </component>
-</project>
\ No newline at end of file
--- a/src/Tools/Setup/.idea/modules.xml Thu Jul 08 08:42:36 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<project version="4">
- <component name="ProjectModuleManager">
- <modules>
- <module fileurl="file://$PROJECT_DIR$/Setup.iml" filepath="$PROJECT_DIR$/Setup.iml" />
- </modules>
- </component>
-</project>
\ No newline at end of file
--- a/src/Tools/Setup/.idea/sbt.xml Thu Jul 08 08:42:36 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<project version="4">
- <component name="ScalaSbtSettings">
- <option name="customVMPath" />
- </component>
-</project>
\ No newline at end of file
--- a/src/Tools/Setup/.idea/vcs.xml Thu Jul 08 08:42:36 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<project version="4">
- <component name="VcsDirectoryMappings">
- <mapping directory="$PROJECT_DIR$/../../.." vcs="hg4idea" />
- </component>
-</project>
\ No newline at end of file
--- a/src/Tools/Setup/.idea/workspace.xml Thu Jul 08 08:42:36 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<project version="4">
- <component name="ArtifactsWorkspaceSettings">
- <artifacts-to-build>
- <artifact name="Setup:jar" />
- </artifacts-to-build>
- </component>
- <component name="AutoImportSettings">
- <option name="autoReloadType" value="SELECTIVE" />
- </component>
- <component name="ChangeListManager">
- <list default="true" id="a00f79eb-e202-4706-95b3-a972b05b3ddb" name="Default Changelist" comment="" />
- <option name="SHOW_DIALOG" value="false" />
- <option name="HIGHLIGHT_CONFLICTS" value="true" />
- <option name="HIGHLIGHT_NON_ACTIVE_CHANGELIST" value="false" />
- <option name="LAST_RESOLUTION" value="IGNORE" />
- </component>
- <component name="CodeStyleSettingsInfer">
- <option name="done" value="true" />
- </component>
- <component name="FileTemplateManagerImpl">
- <option name="RECENT_TEMPLATES">
- <list>
- <option value="Class" />
- </list>
- </option>
- </component>
- <component name="ProjectCodeStyleSettingsMigration">
- <option name="version" value="1" />
- </component>
- <component name="ProjectId" id="1sP6lEsakYWhAQI9WzuHpAcovaN" />
- <component name="ProjectLevelVcsManager" settingsEditedManually="true" />
- <component name="ProjectViewState">
- <option name="hideEmptyMiddlePackages" value="true" />
- <option name="showLibraryContents" value="true" />
- </component>
- <component name="PropertiesComponent">
- <property name="RunOnceActivity.OpenProjectViewOnStart" value="true" />
- <property name="RunOnceActivity.ShowReadmeOnStart" value="true" />
- <property name="project.structure.last.edited" value="Artifacts" />
- <property name="project.structure.proportion" value="0.15" />
- <property name="project.structure.side.proportion" value="0.18055555" />
- </component>
- <component name="SpellCheckerSettings" RuntimeDictionaries="0" Folders="0" CustomDictionaries="0" DefaultDictionary="application-level" UseSingleDictionary="true" transferred="true" />
- <component name="TaskManager">
- <task active="true" id="Default" summary="Default task">
- <changelist id="a00f79eb-e202-4706-95b3-a972b05b3ddb" name="Default Changelist" comment="" />
- <created>1620762028428</created>
- <option name="number" value="Default" />
- <option name="presentableId" value="Default" />
- <updated>1620762028428</updated>
- </task>
- <servers />
- </component>
- <component name="hg4idea.settings">
- <option name="CHECK_INCOMING_OUTGOING" value="true" />
- <option name="RECENT_HG_ROOT_PATH" value="$PROJECT_DIR$/../../.." />
- </component>
-</project>
\ No newline at end of file
--- a/src/Tools/Setup/Setup.iml Thu Jul 08 08:42:36 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<module type="JAVA_MODULE" version="4">
- <component name="NewModuleRootManager" inherit-compiler-output="true">
- <exclude-output />
- <content url="file://$MODULE_DIR$">
- <sourceFolder url="file://$MODULE_DIR$/src" isTestSource="false" />
- </content>
- <orderEntry type="inheritedJdk" />
- <orderEntry type="sourceFolder" forTests="false" />
- </component>
-</module>
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Setup/isabelle/setup/Build_Scala.java Thu Jul 08 08:44:18 2021 +0200
@@ -0,0 +1,255 @@
+/* Title: Tools/Setup/isabelle/setup/Build_Scala.java
+ Author: Makarius
+
+Build Isabelle/Scala modules.
+*/
+
+package isabelle.setup;
+
+
+import java.io.BufferedOutputStream;
+import java.io.File;
+import java.io.IOException;
+import java.math.BigInteger;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.StandardCopyOption;
+import java.security.MessageDigest;
+import java.security.NoSuchAlgorithmException;
+import java.util.ArrayList;
+import java.util.Comparator;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Locale;
+import java.util.Properties;
+import java.util.jar.Attributes;
+import java.util.jar.JarEntry;
+import java.util.jar.JarOutputStream;
+import java.util.jar.Manifest;
+import java.util.stream.Stream;
+
+import scala.tools.nsc.MainClass;
+
+
+public class Build_Scala
+{
+ /** component directory context **/
+
+ public static class Context
+ {
+ private final Path component_dir;
+ private Properties props;
+
+ public Context(Path dir) throws IOException
+ {
+ component_dir = dir;
+ props = new Properties();
+ Path path = component_dir.resolve("etc/scala.props");
+ if (Files.exists(path)) { props.load(Files.newBufferedReader(path)); }
+ }
+
+ @Override public String toString() { return component_dir.toString(); }
+
+ public String component_name() { return component_dir.toFile().getName(); }
+ public String name() { return props.getProperty("name", component_name()); }
+ public String description() { return props.getProperty("description", name()); }
+
+ public String lib_name() { return props.getProperty("lib", "lib") + "/" + name(); }
+ public String jar_name() { return lib_name() + ".jar"; }
+ public String shasum_name() { return lib_name() + ".shasum"; }
+
+ public String main() { return props.getProperty("main", ""); }
+
+ private List<String> get_list(String name)
+ {
+ List<String> list = new LinkedList<String>();
+ for (String s : props.getProperty(name, "").split("\\s+")) {
+ if (!s.isEmpty()) { list.add(s); }
+ }
+ return List.copyOf(list);
+ }
+ public List<String> sources() { return get_list("sources"); }
+ public List<String> resources() { return get_list("resources"); }
+ public List<String> services() { return get_list("services"); }
+
+ public Path path(String file) { return component_dir.resolve(file); }
+ public boolean exists(String file) { return Files.exists(path(file)); }
+
+ public String item_name(String s)
+ {
+ int i = s.indexOf(':');
+ return i > 0 ? s.substring(0, i) : s;
+ }
+
+ public String item_target(String s)
+ {
+ int i = s.indexOf(':');
+ return i > 0 ? s.substring(i + 1) : s;
+ }
+
+ public String shasum(String file)
+ throws IOException, NoSuchAlgorithmException
+ {
+ if (exists(file)) {
+ MessageDigest sha = MessageDigest.getInstance("SHA");
+ sha.update(Files.readAllBytes(path(file)));
+ String digest = String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest()));
+ return digest + " *" + file + "\n";
+ }
+ else { return ""; }
+ }
+ }
+
+
+ /** compile sources **/
+
+ public static void compile_sources(
+ Path target_dir, List<Path> deps, String options, List<Path> sources)
+ {
+ ArrayList<String> args = new ArrayList<String>();
+ args.add("-d");
+ args.add(target_dir.toString());
+ args.add("-bootclasspath");
+ args.add(Environment.join_paths(deps));
+ for (String s : options.split("\\s+")) {
+ if (!s.isEmpty()) { args.add(s); }
+ }
+ args.add("--");
+ for (Path p : sources) { args.add(p.toString()); }
+
+ MainClass main = new MainClass();
+ boolean ok = main.process(args.toArray(String[]::new));
+ if (!ok) throw new RuntimeException("Failed to compile sources");
+ }
+
+
+ /** create jar **/
+
+ public static void create_jar(Path dir, String main, Path jar)
+ throws IOException
+ {
+ Files.deleteIfExists(jar);
+
+ Manifest manifest = new Manifest();
+ Attributes attributes = manifest.getMainAttributes();
+ attributes.put(Attributes.Name.MANIFEST_VERSION, "1.0");
+ attributes.put(new Attributes.Name("Created-By"),
+ System.getProperty("java.version") + " (" + System.getProperty("java.vendor") + ")");
+ if (!main.isEmpty()) { attributes.put(Attributes.Name.MAIN_CLASS, main); }
+
+ try (JarOutputStream out =
+ new JarOutputStream(new BufferedOutputStream(Files.newOutputStream(jar)), manifest))
+ {
+ for (Path path : Files.walk(dir).sorted().toArray(Path[]::new)) {
+ boolean is_dir = Files.isDirectory(path);
+ boolean is_file = Files.isRegularFile(path);
+ if (is_dir || is_file) {
+ String name = Environment.slashes(dir.relativize(path).toString());
+ JarEntry entry = new JarEntry(is_dir ? name + "/" : name);
+ entry.setTime(path.toFile().lastModified());
+ out.putNextEntry(entry);
+ if (is_file) { out.write(Files.readAllBytes(path)); }
+ out.closeEntry();
+ }
+ }
+ }
+ }
+
+
+
+ /** build scala **/
+
+ public static void build_scala(Context context, boolean fresh)
+ throws IOException, InterruptedException, NoSuchAlgorithmException
+ {
+ String jar_name = context.jar_name();
+ Path jar_path = context.path(jar_name);
+ String shasum_name = context.shasum_name();
+
+ List<String> sources = context.sources();
+ List<String> resources = context.resources();
+
+ if (sources.isEmpty()) {
+ Files.deleteIfExists(jar_path);
+ Files.deleteIfExists(context.path(shasum_name));
+ }
+ else {
+ String shasum_old =
+ context.exists(shasum_name) ? Files.readString(context.path(shasum_name)) : "";
+ String shasum_sources;
+ {
+ StringBuilder _shasum = new StringBuilder();
+ for (String s : resources) {
+ _shasum.append(context.shasum(context.item_name(s)));
+ }
+ for (String s : sources) { _shasum.append(context.shasum(s)); }
+ shasum_sources = _shasum.toString();
+ }
+ if (fresh || !shasum_old.equals(context.shasum(jar_name) + shasum_sources)) {
+ System.out.println(
+ "### Building " + context.description() + " (" + jar_path + ") ...");
+
+ String scalac_options = Environment.getenv("ISABELLE_SCALAC_OPTIONS");
+ String isabelle_class_path = Environment.getenv("ISABELLE_CLASSPATH");
+
+ Path build_dir = Files.createTempDirectory("isabelle");
+ try {
+ /* compile sources */
+
+ List<Path> compiler_deps = new LinkedList<Path>();
+ for (String s : isabelle_class_path.split(":", -1)) {
+ if (!s.isEmpty()) {
+ compiler_deps.add(Path.of(Environment.platform_path(s)));
+ }
+ }
+
+ List<Path> compiler_sources = new LinkedList<Path>();
+ for (String s : sources) { compiler_sources.add(context.path(s)); }
+
+ compile_sources(build_dir, compiler_deps, scalac_options, compiler_sources);
+
+
+ /* copy resources */
+
+ for (String s : context.resources()) {
+ String name = context.item_name(s);
+ String target = context.item_target(s);
+ Path file_name = Path.of(name).normalize().getFileName();
+ Path target_path = Path.of(target).normalize();
+
+ Path target_dir;
+ Path target_file;
+ {
+ if (target.endsWith("/") || target.endsWith("/.")) {
+ target_dir = build_dir.resolve(target_path);
+ target_file = target_dir.resolve(file_name);
+ }
+ else {
+ target_file = build_dir.resolve(target_path);
+ target_dir = target_file.getParent();
+ }
+ }
+ Files.createDirectories(target_dir);
+ Files.copy(context.path(name), target_file,
+ StandardCopyOption.COPY_ATTRIBUTES);
+ }
+
+
+ /* packaging */
+
+ create_jar(build_dir, context.main(), jar_path);
+
+ String shasum = context.shasum(jar_name) + shasum_sources;
+ Files.writeString(context.path(shasum_name), shasum);
+ }
+ finally {
+ try (Stream<Path> walk = Files.walk(build_dir)) {
+ walk.sorted(Comparator.reverseOrder())
+ .map(Path::toFile)
+ .forEach(File::delete);
+ }
+ }
+ }
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Setup/isabelle/setup/Environment.java Thu Jul 08 08:44:18 2021 +0200
@@ -0,0 +1,389 @@
+/* Title: Pure/System/isabelle_env.scala
+ Author: Makarius
+
+Fundamental Isabelle system environment: quasi-static module with
+optional init operation.
+*/
+
+package isabelle.setup;
+
+import java.io.File;
+import java.io.IOException;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.util.HashMap;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Locale;
+import java.util.Map;
+import java.util.function.BiFunction;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+
+
+public class Environment
+{
+ /** Support for Cygwin as POSIX emulation on Windows **/
+
+ public static Boolean is_windows()
+ {
+ return System.getProperty("os.name", "").startsWith("Windows");
+ }
+
+ public static String quote(String s)
+ {
+ return "\"" + s + "\"";
+ }
+
+
+
+ /* system path representations */
+
+ public static String slashes(String s) { return s.replace('\\', '/'); }
+
+ public static String standard_path(String cygwin_root, String platform_path)
+ {
+ if (is_windows()) {
+ String backslashes = platform_path.replace('/', '\\');
+
+ Pattern root_pattern =
+ Pattern.compile("(?i)" + Pattern.quote(cygwin_root) + "(?:\\\\+|\\z)(.*)");
+ Matcher root_matcher = root_pattern.matcher(backslashes);
+
+ Pattern drive_pattern = Pattern.compile("([a-zA-Z]):\\\\*(.*)");
+ Matcher drive_matcher = drive_pattern.matcher(backslashes);
+
+ if (root_matcher.matches()) {
+ String rest = root_matcher.group(1);
+ return "/" + slashes(rest);
+ }
+ else if (drive_matcher.matches()) {
+ String letter = drive_matcher.group(1).toLowerCase(Locale.ROOT);
+ String rest = drive_matcher.group(2);
+ return "/cygdrive/" + letter + (rest.isEmpty() ? "" : "/" + slashes(rest));
+ }
+ else { return slashes(backslashes); }
+ }
+ else { return platform_path; }
+ }
+
+ public static String platform_path(String cygwin_root, String standard_path)
+ {
+ if (is_windows()) {
+ StringBuilder result_path = new StringBuilder();
+
+ Pattern cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)");
+ Matcher cygdrive_matcher = cygdrive_pattern.matcher(standard_path);
+
+ Pattern named_root_pattern = Pattern.compile("//+([^/]*)(.*)");
+ Matcher named_root_matcher = named_root_pattern.matcher(standard_path);
+
+ String rest;
+ if (cygdrive_matcher.matches()) {
+ String drive = cygdrive_matcher.group(1).toUpperCase(Locale.ROOT);
+ rest = cygdrive_matcher.group(2);
+ result_path.append(drive);
+ result_path.append(':');
+ result_path.append(File.separatorChar);
+ }
+ else if (named_root_matcher.matches()) {
+ String root = named_root_matcher.group(1);
+ rest = named_root_matcher.group(2);
+ result_path.append(File.separatorChar);
+ result_path.append(File.separatorChar);
+ result_path.append(root);
+ }
+ else {
+ if (standard_path.startsWith("/")) { result_path.append(cygwin_root); }
+ rest = standard_path;
+ }
+
+ for (String p : rest.split("/", -1)) {
+ if (!p.isEmpty()) {
+ int len = result_path.length();
+ if (len > 0 && result_path.charAt(len - 1) != File.separatorChar) {
+ result_path.append(File.separatorChar);
+ }
+ result_path.append(p);
+ }
+ }
+
+ return result_path.toString();
+ }
+ else { return standard_path; }
+ }
+
+ public static String join_paths(List<Path> paths)
+ {
+ List<String> strs = new LinkedList<String>();
+ for (Path p : paths) { strs.add(p.toString()); }
+ return String.join(File.pathSeparator, strs);
+ }
+
+
+ /* raw process */
+
+ public static ProcessBuilder process_builder(
+ List<String> cmd, File cwd, Map<String,String> env, boolean redirect)
+ {
+ ProcessBuilder builder = new ProcessBuilder();
+
+ // fragile on Windows:
+ // see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160
+ builder.command(cmd);
+
+ if (cwd != null) builder.directory(cwd);
+ if (env != null) {
+ builder.environment().clear();
+ builder.environment().putAll(env);
+ }
+ builder.redirectErrorStream(redirect);
+
+ return builder;
+ }
+
+ public static class Exec_Result
+ {
+ private final int _rc;
+ private final String _out;
+ private final String _err;
+
+ Exec_Result(int rc, String out, String err)
+ {
+ _rc = rc;
+ _out = out;
+ _err = err;
+ }
+
+ public int rc() { return _rc; }
+ public boolean ok() { return _rc == 0; }
+ public String out() { return _out; }
+ public String err() { return _err; }
+ }
+
+ public static Exec_Result exec_process(
+ List<String> command_line,
+ File cwd,
+ Map<String,String> env,
+ boolean redirect) throws IOException, InterruptedException
+ {
+ Path out_file = Files.createTempFile(null, null);
+ Path err_file = Files.createTempFile(null, null);
+ Exec_Result res;
+ try {
+ ProcessBuilder builder = process_builder(command_line, cwd, env, redirect);
+ builder.redirectOutput(out_file.toFile());
+ builder.redirectError(err_file.toFile());
+
+ Process proc = builder.start();
+ proc.getOutputStream().close();
+ try { proc.waitFor(); }
+ finally {
+ proc.getInputStream().close();
+ proc.getErrorStream().close();
+ proc.destroy();
+ Thread.interrupted();
+ }
+
+ int rc = proc.exitValue();
+ String out = Files.readString(out_file);
+ String err = Files.readString(err_file);
+ res = new Exec_Result(rc, out, err);
+ }
+ finally {
+ Files.deleteIfExists(out_file);
+ Files.deleteIfExists(err_file);
+ }
+ return res;
+ }
+
+
+ /* init (e.g. after extraction via 7zip) */
+
+ private static String bootstrap_directory(
+ String preference, String variable, String property, String description)
+ {
+ String a = preference; // explicit argument
+ String b = System.getenv(variable); // e.g. inherited from running isabelle tool
+ String c = System.getProperty(property); // e.g. via JVM application boot process
+ String dir;
+
+ if (a != null && !a.isEmpty()) { dir = a; }
+ else if (b != null && !b.isEmpty()) { dir = b; }
+ else if (c != null && !c.isEmpty()) { dir = c; }
+ else { throw new RuntimeException("Unknown " + description + " directory"); }
+
+ if ((new File(dir)).isDirectory()) { return dir; }
+ else { throw new RuntimeException("Bad " + description + " directory " + quote(dir)); }
+ }
+
+ private static void cygwin_exec(String isabelle_root, List<String> cmd)
+ throws IOException, InterruptedException
+ {
+ File cwd = new File(isabelle_root);
+ Map<String,String> env = new HashMap<String,String>(System.getenv());
+ env.put("CYGWIN", "nodosfilewarning");
+ Exec_Result res = exec_process(cmd, cwd, env, true);
+ if (!res.ok()) throw new RuntimeException(res.out());
+ }
+
+ public static void cygwin_link(String content, File target) throws IOException
+ {
+ Path target_path = target.toPath();
+ Files.writeString(target_path, "!<symlink>" + content + "\u0000");
+ Files.setAttribute(target_path, "dos:system", true);
+ }
+
+ public static void cygwin_init(String isabelle_root, String cygwin_root)
+ throws IOException, InterruptedException
+ {
+ if (is_windows()) {
+ File uninitialized_file = new File(cygwin_root, "isabelle\\uninitialized");
+ boolean uninitialized = uninitialized_file.isFile() && uninitialized_file.delete();
+
+ if (uninitialized) {
+ Path symlinks_path = (new File(cygwin_root + "\\isabelle\\symlinks")).toPath();
+ String[] symlinks = Files.readAllLines(symlinks_path).toArray(new String[0]);
+
+ // recover symlinks
+ int i = 0;
+ int m = symlinks.length;
+ int n = (m > 0 && symlinks[m - 1].isEmpty()) ? m - 1 : m;
+ while (i < n) {
+ if (i + 1 < n) {
+ String target = symlinks[i];
+ String content = symlinks[i + 1];
+ cygwin_link(content, new File(isabelle_root, target));
+ i += 2;
+ } else { throw new RuntimeException("Unbalanced symlinks list"); }
+ }
+
+ cygwin_exec(isabelle_root,
+ List.of(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall"));
+ cygwin_exec(isabelle_root,
+ List.of(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall"));
+ }
+ }
+ }
+
+
+ /* implicit settings environment */
+
+ private static volatile Map<String,String> _settings = null;
+
+ public static Map<String,String> settings()
+ throws IOException, InterruptedException
+ {
+ if (_settings == null) { init("", ""); } // unsynchronized check
+ return _settings;
+ }
+
+ public static String getenv(String name)
+ throws IOException, InterruptedException
+ {
+ return settings().getOrDefault(name, "");
+ }
+
+ public static synchronized void init(String _isabelle_root, String _cygwin_root)
+ throws IOException, InterruptedException
+ {
+ if (_settings == null) {
+ String isabelle_root =
+ bootstrap_directory(_isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root");
+
+ String cygwin_root = "";
+ if (is_windows()) {
+ cygwin_root = bootstrap_directory(_cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root");
+ cygwin_init(isabelle_root, cygwin_root);
+ }
+
+ Map<String,String> env = new HashMap<String,String>(System.getenv());
+
+ BiFunction<String,String,Void> env_default =
+ (String a, String b) -> { if (!b.isEmpty()) env.putIfAbsent(a, b); return null; };
+
+ String temp_windows = is_windows() ? System.getenv("TEMP") : null;
+
+ env_default.apply("CYGWIN_ROOT", cygwin_root);
+ env_default.apply("TEMP_WINDOWS",
+ (temp_windows != null && temp_windows.contains("\\")) ? temp_windows : "");
+ env_default.apply("ISABELLE_JDK_HOME",
+ standard_path(cygwin_root, System.getProperty("java.home", "")));
+ env_default.apply("HOME", System.getProperty("user.home", ""));
+ env_default.apply("ISABELLE_APP", System.getProperty("isabelle.app", ""));
+
+ Map<String,String> settings = new HashMap<String,String>();
+ Path settings_file = Files.createTempFile(null, null);
+ try {
+ List<String> cmd = new LinkedList<String>();
+ if (is_windows()) {
+ cmd.add(cygwin_root + "\\bin\\bash");
+ cmd.add("-l");
+ cmd.add(standard_path(cygwin_root, isabelle_root + "\\bin\\isabelle"));
+ } else {
+ cmd.add(isabelle_root + "/bin/isabelle");
+ }
+ cmd.add("getenv");
+ cmd.add("-d");
+ cmd.add(settings_file.toString());
+
+ Exec_Result res = exec_process(cmd, null, env, true);
+ if (!res.ok()) throw new RuntimeException(res.out());
+
+ for (String s : Files.readString(settings_file).split("\u0000", -1)) {
+ int i = s.indexOf('=');
+ if (i > 0) { settings.put(s.substring(0, i), s.substring(i + 1)); }
+ else if (i < 0 && !s.isEmpty()) { settings.put(s, ""); }
+ }
+ }
+ finally { Files.delete(settings_file); }
+
+ if (is_windows()) { settings.put("CYGWIN_ROOT", cygwin_root); }
+
+ settings.put("PATH", settings.get("PATH_JVM"));
+ settings.remove("PATH_JVM");
+
+ _settings = Map.copyOf(settings);
+ }
+ }
+
+
+ /* Cygwin root (after init) */
+
+ public static String cygwin_root()
+ throws IOException, InterruptedException
+ {
+ return getenv("CYGWIN_ROOT");
+ }
+
+ public static String standard_path(String platform_path)
+ throws IOException, InterruptedException
+ {
+ return standard_path(cygwin_root(), platform_path);
+ }
+
+ public static String platform_path(String standard_path)
+ throws IOException, InterruptedException
+ {
+ return platform_path(cygwin_root(), standard_path);
+ }
+
+
+ /* kill process (via bash) */
+
+ static public boolean kill_process(String group_pid, String signal)
+ throws IOException, InterruptedException
+ {
+ List<String> cmd = new LinkedList<String>();
+ if (is_windows()) {
+ cmd.add(cygwin_root() + "\\bin\\bash.exe");
+ }
+ else {
+ cmd.add("/usr/bin/env");
+ cmd.add("bash");
+ }
+ cmd.add("-c");
+ cmd.add("kill -" + signal + " -" + group_pid);
+ return exec_process(cmd, null, null, false).ok();
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Setup/isabelle/setup/Setup.java Thu Jul 08 08:44:18 2021 +0200
@@ -0,0 +1,15 @@
+/* Title: Tools/Setup/isabelle/setup/Setup.java
+ Author: Makarius
+
+Isabelle setup tool: bootstrap from generic Java environment.
+*/
+
+package isabelle.setup;
+
+class Setup
+{
+ public static void main(String[] args)
+ {
+ System.out.println("Isabelle setup");
+ }
+}
--- a/src/Tools/Setup/src/META-INF/MANIFEST.MF Thu Jul 08 08:42:36 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-Manifest-Version: 1.0
-Main-Class: isabelle.setup.Setup
-
--- a/src/Tools/Setup/src/isabelle/setup/Setup.java Thu Jul 08 08:42:36 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-/* Title: Tools/Setup/isabelle/setup/Setup.java
- Author: Makarius
-
-Isabelle setup tool: bootstrap from generic Java environment.
-*/
-
-package isabelle.setup;
-
-class Setup
-{
- public static void main(String[] args)
- {
- System.out.println("Isabelle setup");
- }
-}
--- a/src/Tools/jEdit/etc/options Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Tools/jEdit/etc/options Thu Jul 08 08:44:18 2021 +0200
@@ -99,6 +99,8 @@
option warning_color : string = "FF8C00FF"
option legacy_color : string = "FF8C00FF"
option error_color : string = "B22222FF"
+option ok_color : string = "000000FF"
+option failed_color : string = "B22222FF"
option writeln_message_color : string = "F0F0F0FF"
option information_message_color : string = "DCEAF3FF"
option tracing_message_color : string = "F0F8FFFF"
--- a/src/Tools/jEdit/src-base/pide_docking_framework.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Tools/jEdit/src-base/pide_docking_framework.scala Thu Jul 08 08:44:18 2021 +0200
@@ -9,6 +9,7 @@
import isabelle._
+import java.util.{List => JList}
import java.awt.event.{ActionListener, ActionEvent}
import javax.swing.{JPopupMenu, JMenuItem}
@@ -42,7 +43,7 @@
}
case panel: PanelWindowContainer =>
- val entries = Untyped.get[java.util.List[AnyRef]](panel, "dockables").toArray
+ val entries = Untyped.get[JList[AnyRef]](panel, "dockables").toArray
val wins =
(for {
entry <- entries.iterator
--- a/src/Tools/jEdit/src/fold_handling.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Tools/jEdit/src/fold_handling.scala Thu Jul 08 08:44:18 2021 +0200
@@ -9,6 +9,8 @@
import isabelle._
+import java.util.{List => JList}
+
import javax.swing.text.Segment
import scala.jdk.CollectionConverters._
@@ -32,7 +34,7 @@
Token_Markup.Line_Context.after(buffer, line).structure.depth max 0
override def getPrecedingFoldLevels(
- buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] =
+ buffer: JEditBuffer, line: Int, seg: Segment, level: Int): JList[Integer] =
{
val structure = Token_Markup.Line_Context.after(buffer, line).structure
val result =
--- a/src/Tools/jEdit/src/keymap_merge.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Tools/jEdit/src/keymap_merge.scala Thu Jul 08 08:44:18 2021 +0200
@@ -9,6 +9,7 @@
import isabelle._
+import java.util.{Properties => JProperties}
import java.awt.{Color, Dimension, BorderLayout}
import javax.swing.{JPanel, JTable, JScrollPane, JOptionPane}
import javax.swing.table.AbstractTableModel
@@ -64,7 +65,7 @@
/* content wrt. keymap */
- def convert_properties(props: java.util.Properties): List[Shortcut] =
+ def convert_properties(props: JProperties): List[Shortcut] =
if (props == null) Nil
else {
var result = List.empty[Shortcut]
@@ -82,7 +83,7 @@
{
val keymap_shortcuts =
if (keymap == null) Nil
- else convert_properties(Untyped.get[java.util.Properties](keymap, "props"))
+ else convert_properties(Untyped.get[JProperties](keymap, "props"))
for (s <- convert_properties(jEdit.getProperties) if !s.is_ignored(keymap_name)) yield {
val conflicts =
--- a/src/Tools/jEdit/src/rich_text_area.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Thu Jul 08 08:44:18 2021 +0200
@@ -10,7 +10,7 @@
import isabelle._
-import java.awt.{Graphics2D, Shape, Color, Point, Cursor, MouseInfo}
+import java.awt.{Graphics2D, Shape, Color, Point, Cursor, MouseInfo, Font}
import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
FocusAdapter, FocusEvent, WindowEvent, WindowAdapter, KeyEvent}
import java.awt.font.TextAttribute
@@ -176,7 +176,7 @@
def update_rendering(r: JEdit_Rendering, range: Text.Range): Unit =
update(rendering(r)(range))
- def reset: Unit = update(None)
+ def reset(): Unit = update(None)
}
// owned by GUI thread
@@ -195,7 +195,7 @@
private val active_areas =
List((highlight_area, true), (hyperlink_area, true), (active_area, false))
- def active_reset(): Unit = active_areas.foreach(_._1.reset)
+ def active_reset(): Unit = active_areas.foreach(_._1.reset())
private def area_active(): Boolean =
active_areas.exists({ case (area, _) => area.is_active })
@@ -273,7 +273,7 @@
{
if (control == require_control && !rendering.snapshot.is_outdated)
area.update_rendering(rendering, range)
- else area.reset
+ else area.reset()
}
}
}
@@ -404,12 +404,26 @@
}
}
- private def paint_chunk_list(rendering: JEdit_Rendering,
+ private class Font_Subst
+ {
+ private var cache = Map.empty[Int, Option[Font]]
+
+ def get(codepoint: Int): Option[Font] =
+ cache.getOrElse(codepoint,
+ {
+ val field = classOf[Chunk].getDeclaredField("lastSubstFont")
+ field.setAccessible(true)
+ field.set(null, null)
+ val res = Option(Chunk.getSubstFont(codepoint))
+ cache += (codepoint -> res)
+ res
+ })
+ }
+
+ private def paint_chunk_list(rendering: JEdit_Rendering, font_subst: Font_Subst,
gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
{
val clip_rect = gfx.getClipBounds
- val painter = text_area.getPainter
- val font_context = painter.getFontRenderContext
val caret_range =
if (caret_enabled) JEdit_Lib.caret_range(text_area)
@@ -432,55 +446,39 @@
val chunk_font = chunk.style.getFont
val chunk_color = chunk.style.getForegroundColor
- def string_width(s: String): Float =
- if (s.isEmpty) 0.0f
- else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
-
- val markup =
- for {
- r1 <- rendering.text_color(chunk_range, chunk_color)
- r2 <- r1.try_restrict(chunk_range)
- } yield r2
+ val chunk_text = new AttributedString(chunk_str)
- val padded_markup_iterator =
- if (markup.isEmpty)
- Iterator(Text.Info(chunk_range, chunk_color))
- else
- Iterator(
- Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++
- markup.iterator ++
- Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color))
-
- var x1 = x + w
- gfx.setFont(chunk_font)
- for (Text.Info(range, color) <- padded_markup_iterator if !range.is_singularity) {
- val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
- gfx.setColor(color)
+ def chunk_attrib(attrib: TextAttribute, value: AnyRef, r: Text.Range): Unit =
+ chunk_text.addAttribute(attrib, value, r.start - chunk_offset, r.stop - chunk_offset)
- range.try_restrict(caret_range) match {
- case Some(r) if !r.is_singularity =>
- val i = r.start - range.start
- val j = r.stop - range.start
- val s1 = str.substring(0, i)
- val s2 = str.substring(i, j)
- val s3 = str.substring(j)
-
- if (s1.nonEmpty) gfx.drawString(Word.bidi_override(s1), x1, y)
+ // font
+ chunk_text.addAttribute(TextAttribute.RUN_DIRECTION, TextAttribute.RUN_DIRECTION_LTR)
+ chunk_text.addAttribute(TextAttribute.FONT, chunk_font)
+ if (chunk.usedFontSubstitution) {
+ for {
+ (c, i) <- Codepoint.iterator_offset(chunk_str) if !chunk_font.canDisplay(c)
+ subst_font <- font_subst.get(c)
+ } {
+ val r = Text.Range(i, i + Character.charCount(c)) + chunk_offset
+ val font = Chunk.deriveSubstFont(chunk_font, subst_font)
+ chunk_attrib(TextAttribute.FONT, font, r)
+ }
+ }
- val astr = new AttributedString(Word.bidi_override(s2))
- astr.addAttribute(TextAttribute.FONT, chunk_font)
- astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, r.start))
- astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
- gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
+ // color
+ chunk_text.addAttribute(TextAttribute.FOREGROUND, chunk_color)
+ for {
+ Text.Info(r1, color) <- rendering.text_color(chunk_range, chunk_color).iterator
+ r2 <- r1.try_restrict(chunk_range) if !r2.is_singularity
+ } chunk_attrib(TextAttribute.FOREGROUND, color, r2)
- if (s3.nonEmpty)
- gfx.drawString(Word.bidi_override(s3), x1 + string_width(str.substring(0, j)), y)
+ // caret
+ for { r <- caret_range.try_restrict(chunk_range) if !r.is_singularity } {
+ chunk_attrib(TextAttribute.FOREGROUND, caret_color(rendering, r.start), r)
+ chunk_attrib(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, r)
+ }
- case _ =>
- gfx.drawString(Word.bidi_override(str), x1, y)
- }
- x1 += string_width(str)
- }
+ gfx.drawString(chunk_text.getIterator, x + w, y)
}
w += chunk.width
chunk = chunk.next.asInstanceOf[Chunk]
@@ -507,10 +505,12 @@
{
val w = fm.charWidth(' ')
val b = (w / 2) max 1
- val c = (lm.getAscent + lm.getStrikethroughOffset).round.toInt
+ val c = (lm.getAscent + lm.getStrikethroughOffset).round
((w - b + 1) / 2, c - b / 2, w - b, line_height - b)
}
+ val font_subst = new Font_Subst
+
for (i <- physical_lines.indices) {
val line = physical_lines(i)
if (line != -1) {
@@ -524,7 +524,8 @@
val line_start = buffer.getLineStartOffset(line)
gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
val w =
- paint_chunk_list(rendering, gfx, line_start, chunks, x0.toFloat, y0.toFloat).toInt
+ paint_chunk_list(rendering, font_subst, gfx,
+ line_start, chunks, x0.toFloat, y0.toFloat)
gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
orig_text_painter.paintValidLine(gfx,
screen_line, line, start(i), end(i), y + line_height * i)
--- a/src/Tools/jEdit/src/syntax_style.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Tools/jEdit/src/syntax_style.scala Thu Jul 08 08:44:18 2021 +0200
@@ -9,6 +9,7 @@
import isabelle._
+import java.util.{Map => JMap}
import java.awt.{Font, Color}
import java.awt.font.TextAttribute
import java.awt.geom.AffineTransform
@@ -40,8 +41,7 @@
{
font_style(style, font0 =>
{
- val font1 =
- font0.deriveFont(java.util.Map.of(TextAttribute.SUPERSCRIPT, java.lang.Integer.valueOf(i)))
+ val font1 = font0.deriveFont(JMap.of(TextAttribute.SUPERSCRIPT, java.lang.Integer.valueOf(i)))
def shift(y: Float): Font =
GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))
--- a/src/Tools/jEdit/src/text_structure.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala Thu Jul 08 08:44:18 2021 +0200
@@ -9,6 +9,8 @@
import isabelle._
+import java.util.{List => JList}
+
import org.gjt.sp.jedit.indent.{IndentRule, IndentAction}
import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection}
import org.gjt.sp.jedit.buffer.JEditBuffer
@@ -45,7 +47,7 @@
private val keyword_close = Keyword.proof_close
def apply(buffer: JEditBuffer, current_line: Int, prev_line0: Int, prev_prev_line0: Int,
- actions: java.util.List[IndentAction]): Unit =
+ actions: JList[IndentAction]): Unit =
{
Isabelle.buffer_syntax(buffer) match {
case Some(syntax) =>
--- a/src/Tools/jEdit/src/theories_dockable.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Thu Jul 08 08:44:18 2021 +0200
@@ -180,11 +180,15 @@
{
val st = nodes_status.overall_node_status(name)
val color =
- if (st == Document_Status.Overall_Node_Status.failed)
- PIDE.options.color_value("error_color")
- else label.foreground
- val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 2
- val thickness2 = 3 - thickness1
+ st match {
+ case Document_Status.Overall_Node_Status.ok =>
+ PIDE.options.color_value("ok_color")
+ case Document_Status.Overall_Node_Status.failed =>
+ PIDE.options.color_value("failed_color")
+ case _ => label.foreground
+ }
+ val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 3
+ val thickness2 = 4 - thickness1
label.border =
BorderFactory.createCompoundBorder(
--- a/src/Tools/jEdit/src/token_markup.scala Thu Jul 08 08:42:36 2021 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Thu Jul 08 08:44:18 2021 +0200
@@ -9,6 +9,8 @@
import isabelle._
+import java.util.{List => JList}
+
import javax.swing.text.Segment
import org.gjt.sp.jedit.{Mode, Buffer}
@@ -312,10 +314,9 @@
override def loadMode(mode: Mode, xmh: XModeHandler): Unit =
{
super.loadMode(mode, xmh)
- Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker _)
+ Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker)
Isabelle.indent_rule(mode.getName).foreach(indent_rule =>
- Untyped.set[java.util.List[IndentRule]](
- mode, "indentRules", java.util.List.of(indent_rule)))
+ Untyped.set[JList[IndentRule]](mode, "indentRules", JList.of(indent_rule)))
}
}
}