# 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>\Assumption.export\ represents arbitrary export rules, which - is any function of type \<^ML_type>\bool -> cterm list -> thm -> thm\, where - the \<^ML_type>\bool\ indicates goal mode, and the \<^ML_type>\cterm list\ + \<^descr> Type \<^ML_type>\Assumption.export\ represents export rules, as a pair of + functions \<^ML_type>\bool -> cterm list -> (thm -> thm) * (term -> term)\. + The \<^ML_type>\bool\ argument indicates goal mode, and the \<^ML_type>\cterm list\ the collection of assumptions to be discharged simultaneously. \<^descr> \<^ML>\Assumption.assume\~\ctxt A\ turns proposition \A\ into a primitive @@ -285,13 +286,21 @@ with export rule \r\. The resulting facts are hypothetical theorems as produced by the raw \<^ML>\Assumption.assume\. - \<^descr> \<^ML>\Assumption.add_assumes\~\As\ is a special case of \<^ML>\Assumption.add_assms\ where the export rule performs \\\intro\ or + \<^descr> \<^ML>\Assumption.add_assumes\~\As\ is a special case of + \<^ML>\Assumption.add_assms\ where the export rule performs \\\intro\ or \#\\intro\, depending on goal mode. \<^descr> \<^ML>\Assumption.export\~\is_goal inner outer thm\ exports result \thm\ - from the the \inner\ context back into the \outer\ one; \is_goal = true\ - means this is a goal context. The result is in HHF normal form. Note that - \<^ML>\Proof_Context.export\ combines \<^ML>\Variable.export\ and \<^ML>\Assumption.export\ in the canonical way. + from the \inner\ context back into the \outer\ one; \is_goal = true\ means + this is a goal context. The result is in HHF normal form. Note that + \<^ML>\Proof_Context.export\ combines \<^ML>\Variable.export\ and + \<^ML>\Assumption.export\ in the canonical way. + + \<^descr> \<^ML>\Assumption.export_term\~\inner outer t\ exports term \t\ from the + \inner\ context back into the \outer\ one. This is analogous to + \<^ML>\Assumption.export\, but only takes syntactical aspects of the + context into account (such as locally specified variables as seen in + @{command define} or @{command obtain}). \ text %mlex \ 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 \ 'a::banach" - assumes \: "finite \" - and int: "\S. S \ \ \ (f has_integral (i S)) S" - and neg: "pairwise (\S S'. negligible (S \ S')) \" - shows "(f has_integral (sum i \)) (\\)" + assumes "finite I" + and int: "\i. i \ I \ (f has_integral (g i)) (\ i)" + and neg: "pairwise (\i i'. negligible (\ i \ \ i')) I" + shows "(f has_integral (sum g I)) (\i\I. \ i)" proof - - let ?\ = "((\(a,b). a \ b) ` {(a,b). a \ \ \ b \ {y. y \ \ \ a \ y}})" - have "((\x. if x \ \\ then f x else 0) has_integral sum i \) UNIV" + let ?\ = "((\(a,b). \ a \ \ b) ` {(a,b). a \ I \ b \ I-{a}})" + have "((\x. if x \ (\i\I. \ i) then f x else 0) has_integral sum g I) UNIV" proof (rule has_integral_spike) show "negligible (\?\)" proof (rule negligible_Union) - have "finite (\ \ \)" - by (simp add: \) - moreover have "{(a, b). a \ \ \ b \ {y \ \. a \ y}} \ \ \ \" + have "finite (I \ I)" + by (simp add: \finite I\) + moreover have "{(a,b). a \ I \ b \ I-{a}} \ I \ I" by auto ultimately show "finite ?\" - by (blast intro: finite_subset[of _ "\ \ \"]) + by (simp add: finite_subset) show "\t. t \ ?\ \ negligible t" using neg unfolding pairwise_def by auto qed next - show "(if x \ \\ then f x else 0) = (\A\\. if x \ A then f x else 0)" + show "(if x \ (\i\I. \ i) then f x else 0) = (\i\I. if x \ \ i then f x else 0)" if "x \ UNIV - (\?\)" for x proof clarsimp - fix S assume "S \ \" "x \ S" - moreover then have "\b\\. x \ b \ b = S" + fix i assume i: "i \ I" "x \ \ i" + then have "\j\I. x \ \ j \ j = i" using that by blast - ultimately show "f x = (\A\\. if x \ A then f x else 0)" - by (simp add: sum.delta[OF \]) + with i show "f x = (\i\I. if x \ \ i then f x else 0)" + by (simp add: sum.delta[OF \finite I\]) qed next - show "((\x. \A\\. if x \ A then f x else 0) has_integral (\A\\. i A)) UNIV" - using int by (simp add: has_integral_restrict_UNIV has_integral_sum [OF \]) + show "((\x. (\i\I. if x \ \ 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 \finite I\]) qed then show ?thesis using has_integral_restrict_UNIV by blast qed +lemma has_integral_Union: + fixes f :: "'n::euclidean_space \ 'a::banach" + assumes "finite \" + and "\S. S \ \ \ (f has_integral (i S)) S" + and "pairwise (\S S'. negligible (S \ S')) \" + shows "(f has_integral (sum i \)) (\\)" +proof - + have "(f has_integral (sum i \)) (\S\\. S)" + by (intro has_integral_UN assms) + then show ?thesis + by force +qed text \In particular adding integrals over a division, maybe not of an interval.\