--- a/Admin/components/components.sha1 Sat Jan 22 14:33:35 2022 +0100
+++ b/Admin/components/components.sha1 Tue Jan 25 09:57:44 2022 +0100
@@ -161,6 +161,7 @@
e8ae300e61b0b121018456d50010b555bc96ce10 jdk-15.0.2+7.tar.gz
a426a32ad34014953c0f7d4cc6f44199572e1c38 jdk-17+35.tar.gz
85707cfe369d0d32accbe3d96a0730c87e8639b5 jdk-17.0.1+12.tar.gz
+699ab2d723b2f1df151a7dbcbdf33ddad36c7978 jdk-17.0.2+8.tar.gz
8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz
38d2d2a91c66714c18430e136e7e5191af3996e6 jdk-7u11.tar.gz
d765bc4ad2f34d494429b2a8c1563c49db224944 jdk-7u13.tar.gz
@@ -341,6 +342,7 @@
49f1adfacdd6d29fa9f72035d94a31eaac411a97 polyml-test-0a6ebca445fc.tar.gz
2a8c4421e0a03c0d6ad556b3c36c34eb11568adb polyml-test-1236652ebd55.tar.gz
8e83fb5088cf265902b8da753a8eac5fe3f6a14b polyml-test-159dc81efc3b.tar.gz
+b80c17398293d0c8f8d9923427176efb33cf2d89 polyml-test-15c840d48c9a.tar.gz
a0064c157a59e2706e18512a49a6dca914fa17fc polyml-test-1b2dcf8f5202.tar.gz
4e6543dbbb2b2aa402fd61428e1c045c48f18b47 polyml-test-79534495ee94.tar.gz
853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e polyml-test-7a7b742897e9.tar.gz
--- a/Admin/components/main Sat Jan 22 14:33:35 2022 +0100
+++ b/Admin/components/main Tue Jan 25 09:57:44 2022 +0100
@@ -10,7 +10,7 @@
idea-icons-20210508
isabelle_fonts-20211004
isabelle_setup-20211109
-jdk-17.0.1+12
+jdk-17.0.2+8
jedit-20211103
jfreechart-1.5.3
jortho-1.0-2
@@ -18,7 +18,7 @@
minisat-2.2.1-1
nunchaku-0.5
opam-2.0.7
-polyml-5.9
+polyml-test-15c840d48c9a
postgresql-42.2.24
scala-2.13.5
smbc-0.4.1
--- a/Admin/polyml/settings Sat Jan 22 14:33:35 2022 +0100
+++ b/Admin/polyml/settings Tue Jan 25 09:57:44 2022 +0100
@@ -2,7 +2,7 @@
POLYML_HOME="$COMPONENT"
-ML_PLATFORM="${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_PLATFORM64}}"
+ML_PLATFORM="${ISABELLE_APPLE_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_PLATFORM64}}}"
if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
then
--- a/src/Doc/Implementation/Proof.thy Sat Jan 22 14:33:35 2022 +0100
+++ b/src/Doc/Implementation/Proof.thy Tue Jan 25 09:57:44 2022 +0100
@@ -271,11 +271,12 @@
@{define_ML Assumption.add_assumes: "
cterm list -> Proof.context -> thm list * Proof.context"} \\
@{define_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\
+ @{define_ML Assumption.export_term: "Proof.context -> Proof.context -> term -> term"} \\
\end{mldecls}
- \<^descr> Type \<^ML_type>\<open>Assumption.export\<close> represents arbitrary export rules, which
- is any function of type \<^ML_type>\<open>bool -> cterm list -> thm -> thm\<close>, where
- the \<^ML_type>\<open>bool\<close> indicates goal mode, and the \<^ML_type>\<open>cterm list\<close>
+ \<^descr> Type \<^ML_type>\<open>Assumption.export\<close> represents export rules, as a pair of
+ functions \<^ML_type>\<open>bool -> cterm list -> (thm -> thm) * (term -> term)\<close>.
+ The \<^ML_type>\<open>bool\<close> argument indicates goal mode, and the \<^ML_type>\<open>cterm list\<close>
the collection of assumptions to be discharged simultaneously.
\<^descr> \<^ML>\<open>Assumption.assume\<close>~\<open>ctxt A\<close> turns proposition \<open>A\<close> into a primitive
@@ -285,13 +286,21 @@
with export rule \<open>r\<close>. The resulting facts are hypothetical theorems as
produced by the raw \<^ML>\<open>Assumption.assume\<close>.
- \<^descr> \<^ML>\<open>Assumption.add_assumes\<close>~\<open>As\<close> is a special case of \<^ML>\<open>Assumption.add_assms\<close> where the export rule performs \<open>\<Longrightarrow>\<hyphen>intro\<close> or
+ \<^descr> \<^ML>\<open>Assumption.add_assumes\<close>~\<open>As\<close> is a special case of
+ \<^ML>\<open>Assumption.add_assms\<close> where the export rule performs \<open>\<Longrightarrow>\<hyphen>intro\<close> or
\<open>#\<Longrightarrow>\<hyphen>intro\<close>, depending on goal mode.
\<^descr> \<^ML>\<open>Assumption.export\<close>~\<open>is_goal inner outer thm\<close> exports result \<open>thm\<close>
- from the the \<open>inner\<close> context back into the \<open>outer\<close> one; \<open>is_goal = true\<close>
- means this is a goal context. The result is in HHF normal form. Note that
- \<^ML>\<open>Proof_Context.export\<close> combines \<^ML>\<open>Variable.export\<close> and \<^ML>\<open>Assumption.export\<close> in the canonical way.
+ from the \<open>inner\<close> context back into the \<open>outer\<close> one; \<open>is_goal = true\<close> means
+ this is a goal context. The result is in HHF normal form. Note that
+ \<^ML>\<open>Proof_Context.export\<close> combines \<^ML>\<open>Variable.export\<close> and
+ \<^ML>\<open>Assumption.export\<close> in the canonical way.
+
+ \<^descr> \<^ML>\<open>Assumption.export_term\<close>~\<open>inner outer t\<close> exports term \<open>t\<close> from the
+ \<open>inner\<close> context back into the \<open>outer\<close> one. This is analogous to
+ \<^ML>\<open>Assumption.export\<close>, but only takes syntactical aspects of the
+ context into account (such as locally specified variables as seen in
+ @{command define} or @{command obtain}).
\<close>
text %mlex \<open>
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sat Jan 22 14:33:35 2022 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Jan 25 09:57:44 2022 +0100
@@ -5472,45 +5472,57 @@
shows "f integrable_on C"
using integrable_Un[of A B f] assms by simp
-lemma has_integral_Union:
+lemma has_integral_UN:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes \<T>: "finite \<T>"
- and int: "\<And>S. S \<in> \<T> \<Longrightarrow> (f has_integral (i S)) S"
- and neg: "pairwise (\<lambda>S S'. negligible (S \<inter> S')) \<T>"
- shows "(f has_integral (sum i \<T>)) (\<Union>\<T>)"
+ assumes "finite I"
+ and int: "\<And>i. i \<in> I \<Longrightarrow> (f has_integral (g i)) (\<T> i)"
+ and neg: "pairwise (\<lambda>i i'. negligible (\<T> i \<inter> \<T> i')) I"
+ shows "(f has_integral (sum g I)) (\<Union>i\<in>I. \<T> i)"
proof -
- let ?\<U> = "((\<lambda>(a,b). a \<inter> b) ` {(a,b). a \<in> \<T> \<and> b \<in> {y. y \<in> \<T> \<and> a \<noteq> y}})"
- have "((\<lambda>x. if x \<in> \<Union>\<T> then f x else 0) has_integral sum i \<T>) UNIV"
+ let ?\<U> = "((\<lambda>(a,b). \<T> a \<inter> \<T> b) ` {(a,b). a \<in> I \<and> b \<in> I-{a}})"
+ have "((\<lambda>x. if x \<in> (\<Union>i\<in>I. \<T> i) then f x else 0) has_integral sum g I) UNIV"
proof (rule has_integral_spike)
show "negligible (\<Union>?\<U>)"
proof (rule negligible_Union)
- have "finite (\<T> \<times> \<T>)"
- by (simp add: \<T>)
- moreover have "{(a, b). a \<in> \<T> \<and> b \<in> {y \<in> \<T>. a \<noteq> y}} \<subseteq> \<T> \<times> \<T>"
+ have "finite (I \<times> I)"
+ by (simp add: \<open>finite I\<close>)
+ moreover have "{(a,b). a \<in> I \<and> b \<in> I-{a}} \<subseteq> I \<times> I"
by auto
ultimately show "finite ?\<U>"
- by (blast intro: finite_subset[of _ "\<T> \<times> \<T>"])
+ by (simp add: finite_subset)
show "\<And>t. t \<in> ?\<U> \<Longrightarrow> negligible t"
using neg unfolding pairwise_def by auto
qed
next
- show "(if x \<in> \<Union>\<T> then f x else 0) = (\<Sum>A\<in>\<T>. if x \<in> A then f x else 0)"
+ show "(if x \<in> (\<Union>i\<in>I. \<T> i) then f x else 0) = (\<Sum>i\<in>I. if x \<in> \<T> i then f x else 0)"
if "x \<in> UNIV - (\<Union>?\<U>)" for x
proof clarsimp
- fix S assume "S \<in> \<T>" "x \<in> S"
- moreover then have "\<forall>b\<in>\<T>. x \<in> b \<longleftrightarrow> b = S"
+ fix i assume i: "i \<in> I" "x \<in> \<T> i"
+ then have "\<forall>j\<in>I. x \<in> \<T> j \<longleftrightarrow> j = i"
using that by blast
- ultimately show "f x = (\<Sum>A\<in>\<T>. if x \<in> A then f x else 0)"
- by (simp add: sum.delta[OF \<T>])
+ with i show "f x = (\<Sum>i\<in>I. if x \<in> \<T> i then f x else 0)"
+ by (simp add: sum.delta[OF \<open>finite I\<close>])
qed
next
- show "((\<lambda>x. \<Sum>A\<in>\<T>. if x \<in> A then f x else 0) has_integral (\<Sum>A\<in>\<T>. i A)) UNIV"
- using int by (simp add: has_integral_restrict_UNIV has_integral_sum [OF \<T>])
+ show "((\<lambda>x. (\<Sum>i\<in>I. if x \<in> \<T> i then f x else 0)) has_integral sum g I) UNIV"
+ using int by (simp add: has_integral_restrict_UNIV has_integral_sum [OF \<open>finite I\<close>])
qed
then show ?thesis
using has_integral_restrict_UNIV by blast
qed
+lemma has_integral_Union:
+ fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
+ assumes "finite \<T>"
+ and "\<And>S. S \<in> \<T> \<Longrightarrow> (f has_integral (i S)) S"
+ and "pairwise (\<lambda>S S'. negligible (S \<inter> S')) \<T>"
+ shows "(f has_integral (sum i \<T>)) (\<Union>\<T>)"
+proof -
+ have "(f has_integral (sum i \<T>)) (\<Union>S\<in>\<T>. S)"
+ by (intro has_integral_UN assms)
+ then show ?thesis
+ by force
+qed
text \<open>In particular adding integrals over a division, maybe not of an interval.\<close>