# HG changeset patch
# User desharna
# Date 1643101064 -3600
# Node ID 2e16798b6f2bda7e4884086cabf0c3dc2e4c92c1
# Parent  01bb90de56bb88d04c950ac91a480a005ec8c653# Parent  68ffcf5cc94bd7be344a49bfff0060114ef92987
merged

diff -r 01bb90de56bb -r 2e16798b6f2b Admin/components/components.sha1
--- 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
diff -r 01bb90de56bb -r 2e16798b6f2b Admin/components/main
--- 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
diff -r 01bb90de56bb -r 2e16798b6f2b Admin/polyml/settings
--- 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
diff -r 01bb90de56bb -r 2e16798b6f2b src/Doc/Implementation/Proof.thy
--- 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>
diff -r 01bb90de56bb -r 2e16798b6f2b src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- 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>