# HG changeset patch # User paulson # Date 1506691037 -3600 # Node ID b034d2ae541c637187226316fd66bae7586a3a6e # Parent 015a95f15040db148395345f62e8a286a1113044# Parent 41bf4d324ac416542574adc4937f8447a943dc75 Merge (resolved trivial conflict) diff -r 015a95f15040 -r b034d2ae541c Admin/PLATFORMS --- a/Admin/PLATFORMS Fri Sep 29 14:12:14 2017 +0100 +++ b/Admin/PLATFORMS Fri Sep 29 14:17:17 2017 +0100 @@ -41,6 +41,7 @@ x86-windows Windows 7 x86_64-windows Windows 7 x86-cygwin Cygwin 2.8 http://isabelle.in.tum.de/cygwin_2017 (x86/release) + x86_64-cygwin Cygwin 2.8 http://isabelle.in.tum.de/cygwin_2017 (x86_64/release) All of the above platforms are 100% supported by Isabelle -- end-users should not have to care about the differences (at least in theory). @@ -67,7 +68,7 @@ help configuring platform-dependent tools: ISABELLE_PLATFORM64 (potentially empty) - ISABELLE_PLATFORM32 + ISABELLE_PLATFORM32 (potentially empty) ISABELLE_PLATFORM The ISABELLE_PLATFORM setting variable refers to the 32 bit version of diff -r 015a95f15040 -r b034d2ae541c Admin/bash_process/build --- a/Admin/bash_process/build Fri Sep 29 14:12:14 2017 +0100 +++ b/Admin/bash_process/build Fri Sep 29 14:17:17 2017 +0100 @@ -42,7 +42,7 @@ x86-linux | x86-darwin) cc -Wall -m32 bash_process.c -o "$TARGET/bash_process" ;; - x86-cygwin) + x86_64-cygwin | x86-cygwin) cc -Wall bash_process.c -o "$TARGET/bash_process.exe" ;; *) diff -r 015a95f15040 -r b034d2ae541c Admin/components/components.sha1 --- a/Admin/components/components.sha1 Fri Sep 29 14:12:14 2017 +0100 +++ b/Admin/components/components.sha1 Fri Sep 29 14:17:17 2017 +0100 @@ -1,6 +1,7 @@ fbe83b522cb37748ac1b3c943ad71704fdde2f82 bash_process-1.1.1.tar.gz bb9ef498cd594b4289221b96146d529c899da209 bash_process-1.1.tar.gz 81250148f8b89ac3587908fb20645081d7f53207 bash_process-1.2.1.tar.gz +97b2491382130a841b3bbaebdcf8720c4d4fb227 bash_process-1.2.2.tar.gz 9e21f447bfa0431ae5097301d553dd6df3c58218 bash_process-1.2.tar.gz e7ffe4238b61a3c1ee87aca4421e7a612e09b836 ci-extras-1.tar.gz 70105fd6fbfd1a868383fc510772b95234325d31 csdp-6.x.tar.gz @@ -144,6 +145,7 @@ b668e1f43a41608a8eb365c5e19db6c54c72748a polyml-5.5.3-20150911.tar.gz 1f5cd9b1390dab13861f90dfc06d4180cc107587 polyml-5.5.3-20150916.tar.gz f78896e588e8ebb4da57bf0c95210b0f0fa9e551 polyml-5.6-1.tar.gz +21fa0592b7dfd23269063f42604438165630c0f0 polyml-5.6-2.tar.gz 03ba81e595fa6d6df069532d67ad3195c37d9046 polyml-5.6-20151123.tar.gz 822f489c18e38ce5ef979ec21dccce4473e09be6 polyml-5.6-20151206.tar.gz bd6a448f0e0d5787747f4f30ca661f9c1868e4a7 polyml-5.6-20151223.tar.gz diff -r 015a95f15040 -r b034d2ae541c Admin/components/main --- a/Admin/components/main Fri Sep 29 14:12:14 2017 +0100 +++ b/Admin/components/main Fri Sep 29 14:17:17 2017 +0100 @@ -1,5 +1,5 @@ #main components for everyday use, without big impact on overall build time -bash_process-1.2.1 +bash_process-1.2.2 csdp-6.x cvc4-1.5-3 e-2.0-1 @@ -10,7 +10,7 @@ jortho-1.0-2 kodkodi-1.5.2 nunchaku-0.5 -polyml-5.6-1 +polyml-5.6-2 postgresql-42.1.4 scala-2.12.3 smbc-0.4.1 diff -r 015a95f15040 -r b034d2ae541c Admin/polyml/settings --- a/Admin/polyml/settings Fri Sep 29 14:12:14 2017 +0100 +++ b/Admin/polyml/settings Fri Sep 29 14:17:17 2017 +0100 @@ -13,10 +13,10 @@ fi case "${ISABELLE_PLATFORM}:${ML_SYSTEM_64}" in - x86-cygwin:true) + *-cygwin:true) PLATFORMS="x86_64-windows x86-windows" ;; - x86-cygwin:*) + *-cygwin:*) PLATFORMS="x86-windows x86_64-windows" ;; *:true) diff -r 015a95f15040 -r b034d2ae541c lib/scripts/isabelle-platform --- a/lib/scripts/isabelle-platform Fri Sep 29 14:12:14 2017 +0100 +++ b/lib/scripts/isabelle-platform Fri Sep 29 14:17:17 2017 +0100 @@ -40,15 +40,18 @@ ;; CYGWIN_NT*) ISABELLE_PLATFORM_FAMILY="windows" + if [ "$PROCESSOR_ARCHITECTURE" = "AMD64" -o "$PROCESSOR_ARCHITEW6432" = "AMD64" ]; then + ISABELLE_WINDOWS_PLATFORM32="x86-windows" + ISABELLE_WINDOWS_PLATFORM64="x86_64-windows" + else + ISABELLE_WINDOWS_PLATFORM32="x86-windows" + fi case $(uname -m) in - i?86 | x86_64) + x86_64) + ISABELLE_PLATFORM64=x86_64-cygwin + ;; + i?86) ISABELLE_PLATFORM32=x86-cygwin - if [ "$PROCESSOR_ARCHITECTURE" = "AMD64" -o "$PROCESSOR_ARCHITEW6432" = "AMD64" ]; then - ISABELLE_WINDOWS_PLATFORM32="x86-windows" - ISABELLE_WINDOWS_PLATFORM64="x86_64-windows" - else - ISABELLE_WINDOWS_PLATFORM32="x86-windows" - fi ;; esac ;; @@ -62,5 +65,5 @@ ;; esac -ISABELLE_PLATFORM="$ISABELLE_PLATFORM32" -ISABELLE_WINDOWS_PLATFORM="$ISABELLE_WINDOWS_PLATFORM32" +ISABELLE_PLATFORM="${ISABELLE_PLATFORM32:-$ISABELLE_PLATFORM64}" +ISABELLE_WINDOWS_PLATFORM="${ISABELLE_WINDOWS_PLATFORM32:-$ISABELLE_WINDOWS_PLATFORM64}" diff -r 015a95f15040 -r b034d2ae541c src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Sep 29 14:12:14 2017 +0100 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Sep 29 14:17:17 2017 +0100 @@ -2253,9 +2253,7 @@ have "(\x. \f x \ i\) integrable_on S" using assms integrable_component [OF fcomp, where y=i] that by simp then have "(\x. f x \ i) absolutely_integrable_on S" - apply - - apply (rule abs_absolutely_integrableI_1, auto) - by (simp add: f integrable_component) + using abs_absolutely_integrableI_1 f integrable_component by blast then show ?thesis by (rule absolutely_integrable_scaleR_right) qed diff -r 015a95f15040 -r b034d2ae541c src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Sep 29 14:12:14 2017 +0100 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Sep 29 14:17:17 2017 +0100 @@ -3060,8 +3060,8 @@ unfolding integrable_on_def by blast lemma integral_has_vector_derivative_continuous_at: - fixes f :: "real \ 'a::banach" - assumes f: "f integrable_on {a..b}" + fixes f :: "real \ 'a::banach" + assumes f: "f integrable_on {a..b}" and x: "x \ {a..b} - S" and "finite S" and fx: "continuous (at x within ({a..b} - S)) f" @@ -3091,7 +3091,7 @@ show ?thesis using False apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc) - apply (rule has_integral_bound_real [where f="(\u. f u - f x)"]) + apply (rule has_integral_bound_real[where f="(\u. f u - f x)"]) using yx False d x y \e>0\ assms by (auto simp: Idiff fux_int) next case True @@ -6062,8 +6062,7 @@ have "norm (integral S f) \ integral S ((\x. x \ k) \ g)" apply (rule integral_norm_bound_integral[OF f integrable_linear[OF g]]) apply (simp add: bounded_linear_inner_left) - unfolding o_def - apply (metis fg) + apply (metis fg o_def) done then show ?thesis unfolding o_def integral_component_eq[OF g] . @@ -6180,7 +6179,6 @@ have "closed_segment x0 x \ U" by (rule \convex U\[unfolded convex_contains_segment, rule_format, OF \x0 \ U\ \x \ U\]) from elim have [intro]: "x \ U" by auto - have "?F x - ?F x0 - ?dF (x - x0) = integral (cbox a b) (\y. f x y - f x0 y - fx x0 y (x - x0))" (is "_ = ?id") @@ -6217,7 +6215,7 @@ also have "\ < e' * norm (x - x0)" using \e' > 0\ apply (intro mult_strict_right_mono[OF _ \0 < norm (x - x0)\]) - apply (auto simp: divide_simps e_def) + apply (auto simp: divide_simps e_def) by (metis \0 < e\ e_def order.asym zero_less_divide_iff) finally have "norm (?F x - ?F x0 - ?dF (x - x0)) < e' * norm (x - x0)" . then show ?case @@ -6306,14 +6304,12 @@ by atomize_elim (auto simp: integrable_on_def intro!: choice) moreover - have gi[simp]: "g integrable_on (cbox a b)" by (auto intro!: integrable_continuous uniform_limit_theorem[OF _ u] eventuallyI c) then obtain J where J: "(g has_integral J) (cbox a b)" by blast moreover - have "(I \ J) F" proof cases assume "content (cbox a b) = 0" @@ -6461,19 +6457,17 @@ f integrable_continuous_real)+ have deriv: "(((\x. integral {c..x} f) \ g) has_vector_derivative g' x *\<^sub>R f (g x)) (at x within {a..b})" if "x \ {a..b} - s" for x - apply (rule has_vector_derivative_eq_rhs) - apply (rule vector_diff_chain_within) - apply (subst has_field_derivative_iff_has_vector_derivative [symmetric]) - apply (rule deriv that)+ - apply (rule has_vector_derivative_within_subset) - apply (rule integral_has_vector_derivative f)+ - using that le subset - apply blast+ - done + proof (rule has_vector_derivative_eq_rhs [OF vector_diff_chain_within refl]) + show "(g has_vector_derivative g' x) (at x within {a..b})" + using deriv has_field_derivative_iff_has_vector_derivative that by blast + show "((\x. integral {c..x} f) has_vector_derivative f (g x)) + (at (g x) within g ` {a..b})" + using that le subset + by (blast intro: has_vector_derivative_within_subset integral_has_vector_derivative f) + qed have deriv: "(?F has_vector_derivative g' x *\<^sub>R f (g x)) (at x)" if "x \ {a..b} - (s \ {a,b})" for x using deriv[of x] that by (simp add: at_within_closed_interval o_def) - have "((\x. g' x *\<^sub>R f (g x)) has_integral (?F b - ?F a)) {a..b}" using le cont_int s deriv cont_int by (intro fundamental_theorem_of_calculus_interior_strong[of "s \ {a,b}"]) simp_all @@ -6805,20 +6799,21 @@ \ e * content (cbox (u,w) (v,z)) / content ?CBOX" by (rule norm_xx [OF integral_Pair_const 1 2]) } note * = this - show "norm (integral ?CBOX f - integral (cbox a b) (\x. integral (cbox c d) (\y. f (x,y)))) \ e" + have "norm (integral ?CBOX f - integral (cbox a b) (\x. integral (cbox c d) (\y. f (x,y)))) \ e" + if "\x\?CBOX. \x'\?CBOX. norm (x' - x) < k \ norm (f x' - f x) < e /(2 * content (?CBOX))" "0 < k" for k + proof - + obtain p where ptag: "p tagged_division_of cbox (a, c) (b, d)" + and fine: "(\x. ball x k) fine p" + using fine_division_exists \0 < k\ by blast + show ?thesis + apply (rule op_acbd [OF division_of_tagged_division [OF ptag]]) + using that fine ptag \0 < k\ by (auto simp: *) + qed + then show "norm (integral ?CBOX f - integral (cbox a b) (\x. integral (cbox c d) (\y. f (x,y)))) \ e" using compact_uniformly_continuous [OF assms compact_cbox] apply (simp add: uniformly_continuous_on_def dist_norm) apply (drule_tac x="e/2 / content?CBOX" in spec) - using cbp \0 < e\ - apply (auto simp: zero_less_mult_iff) - apply (rename_tac k) - apply (rule_tac e1=k in fine_division_exists [OF gauge_ball, where a = "(a,c)" and b = "(b,d)"]) - apply assumption - apply (rule op_acbd) - apply (erule division_of_tagged_division) - using * - apply auto - done + using cbp \0 < e\ by (auto simp: zero_less_mult_iff) qed then show ?thesis by simp @@ -6861,7 +6856,6 @@ shows "((\x::real. exp (-a*x)) has_integral exp (-a*c)/a) {c..}" proof - define f where "f = (\k x. if x \ {c..real k} then exp (-a*x) else 0)" - { fix k :: nat assume k: "of_nat k \ c" from k a diff -r 015a95f15040 -r b034d2ae541c src/HOL/Analysis/Tagged_Division.thy --- a/src/HOL/Analysis/Tagged_Division.thy Fri Sep 29 14:12:14 2017 +0100 +++ b/src/HOL/Analysis/Tagged_Division.thy Fri Sep 29 14:17:17 2017 +0100 @@ -1919,89 +1919,71 @@ lemma interval_bisection_step: fixes type :: "'a::euclidean_space" - assumes "P {}" - and "\s t. P s \ P t \ interior(s) \ interior(t) = {} \ P (s \ t)" - and "\ P (cbox a (b::'a))" + assumes emp: "P {}" + and Un: "\S T. \P S; P T; interior(S) \ interior(T) = {}\ \ P (S \ T)" + and non: "\ P (cbox a (b::'a))" obtains c d where "\ P (cbox c d)" - and "\i\Basis. a\i \ c\i \ c\i \ d\i \ d\i \ b\i \ 2 * (d\i - c\i) \ b\i - a\i" + and "\i. i \ Basis \ a\i \ c\i \ c\i \ d\i \ d\i \ b\i \ 2 * (d\i - c\i) \ b\i - a\i" proof - have "cbox a b \ {}" - using assms(1,3) by metis + using emp non by metis then have ab: "\i. i\Basis \ a \ i \ b \ i" by (force simp: mem_box) - have UN_cases: "\finite f; - \s. s\f \ P s; - \s. s\f \ \a b. s = cbox a b; - \s t. s\f \ t\f \ s \ t \ interior s \ interior t = {}\ \ P (\f)" for f - proof (induct f rule: finite_induct) - case empty - show ?case - using assms(1) by auto + have UN_cases: "\finite \; + \S. S\\ \ P S; + \S. S\\ \ \a b. S = cbox a b; + \S T. S\\ \ T\\ \ S \ T \ interior S \ interior T = {}\ \ P (\\)" for \ + proof (induct \ rule: finite_induct) + case empty show ?case + using emp by auto next case (insert x f) - show ?case - unfolding Union_insert - apply (rule assms(2)[rule_format]) - using Int_interior_Union_intervals [of f "interior x"] - by (metis (no_types, lifting) insert insert_iff open_interior) + then show ?case + unfolding Union_insert by (metis Int_interior_Union_intervals Un insert_iff open_interior) qed - let ?A = "{cbox c d | c d::'a. \i\Basis. (c\i = a\i) \ (d\i = (a\i + b\i) / 2) \ - (c\i = (a\i + b\i) / 2) \ (d\i = b\i)}" - let ?PP = "\c d. \i\Basis. a\i \ c\i \ c\i \ d\i \ d\i \ b\i \ 2 * (d\i - c\i) \ b\i - a\i" - { - presume "\c d. ?PP c d \ P (cbox c d) \ False" - then show thesis - unfolding atomize_not not_all - by (blast intro: that) - } - assume as: "\c d. ?PP c d \ P (cbox c d)" - have "P (\?A)" + let ?ab = "\i. (a\i + b\i) / 2" + let ?A = "{cbox c d | c d::'a. \i\Basis. (c\i = a\i) \ (d\i = ?ab i) \ + (c\i = ?ab i) \ (d\i = b\i)}" + have "P (\?A)" + if "\c d. \i\Basis. a\i \ c\i \ c\i \ d\i \ d\i \ b\i \ 2 * (d\i - c\i) \ b\i - a\i \ P (cbox c d)" proof (rule UN_cases) - let ?B = "(\s. cbox (\i\Basis. (if i \ s then a\i else (a\i + b\i) / 2) *\<^sub>R i::'a) - (\i\Basis. (if i \ s then (a\i + b\i) / 2 else b\i) *\<^sub>R i)) ` {s. s \ Basis}" + let ?B = "(\S. cbox (\i\Basis. (if i \ S then a\i else ?ab i) *\<^sub>R i::'a) + (\i\Basis. (if i \ S then ?ab i else b\i) *\<^sub>R i)) ` {s. s \ Basis}" have "?A \ ?B" proof fix x assume "x \ ?A" then obtain c d where x: "x = cbox c d" - "\i. i \ Basis \ - c \ i = a \ i \ d \ i = (a \ i + b \ i) / 2 \ - c \ i = (a \ i + b \ i) / 2 \ d \ i = b \ i" by blast - show "x \ ?B" - unfolding image_iff x - apply (rule_tac x="{i. i\Basis \ c\i = a\i}" in bexI) - apply (rule arg_cong2 [where f = cbox]) - using x(2) ab - apply (auto simp add: euclidean_eq_iff[where 'a='a]) - by fastforce + "\i. i \ Basis \ + c \ i = a \ i \ d \ i = ?ab i \ c \ i = ?ab i \ d \ i = b \ i" + by blast + have "c = (\i\Basis. (if c \ i = a \ i then a \ i else ?ab i) *\<^sub>R i)" + "d = (\i\Basis. (if c \ i = a \ i then ?ab i else b \ i) *\<^sub>R i)" + using x(2) ab by (fastforce simp add: euclidean_eq_iff[where 'a='a])+ + then show "x \ ?B" + unfolding x by (rule_tac x="{i. i\Basis \ c\i = a\i}" in image_eqI) auto qed then show "finite ?A" by (rule finite_subset) auto next - fix s - assume "s \ ?A" + fix S + assume "S \ ?A" then obtain c d - where s: "s = cbox c d" - "\i. i \ Basis \ - c \ i = a \ i \ d \ i = (a \ i + b \ i) / 2 \ - c \ i = (a \ i + b \ i) / 2 \ d \ i = b \ i" + where s: "S = cbox c d" + "\i. i \ Basis \ c \ i = a \ i \ d \ i = ?ab i \ c \ i = ?ab i \ d \ i = b \ i" by blast - show "P s" - unfolding s - apply (rule as[rule_format]) - using ab s(2) by force - show "\a b. s = cbox a b" + show "P S" + unfolding s using ab s(2) by (fastforce intro!: that) + show "\a b. S = cbox a b" unfolding s by auto - fix t - assume "t \ ?A" + fix T + assume "T \ ?A" then obtain e f where t: - "t = cbox e f" - "\i. i \ Basis \ - e \ i = a \ i \ f \ i = (a \ i + b \ i) / 2 \ - e \ i = (a \ i + b \ i) / 2 \ f \ i = b \ i" + "T = cbox e f" + "\i. i \ Basis \ e \ i = a \ i \ f \ i = ?ab i \ e \ i = ?ab i \ f \ i = b \ i" by blast - assume "s \ t" + assume "S \ T" then have "\ (c = e \ d = f)" unfolding s t by auto then obtain i where "c\i \ e\i \ d\i \ f\i" and i': "i \ Basis" @@ -2011,24 +1993,15 @@ using t(2)[OF i'] \c \ i \ e \ i \ d \ i \ f \ i\ i' s(2) t(2) by fastforce have *: "\s t. (\a. a \ s \ a \ t \ False) \ s \ t = {}" by auto - show "interior s \ interior t = {}" + show "interior S \ interior T = {}" unfolding s t interior_cbox proof (rule *) fix x assume "x \ box c d" "x \ box e f" then have x: "c\i < d\i" "e\i < f\i" "c\i < f\i" "e\i < d\i" - unfolding mem_box using i' - by force+ - show False using s(2)[OF i'] - proof safe - assume as: "c \ i = a \ i" "d \ i = (a \ i + b \ i) / 2" - show False - using t(2)[OF i'] and i x unfolding as by (fastforce simp add:field_simps) - next - assume as: "c \ i = (a \ i + b \ i) / 2" "d \ i = b \ i" - show False - using t(2)[OF i'] and i x unfolding as by(fastforce simp add:field_simps) - qed + unfolding mem_box using i' by force+ + show False using s(2)[OF i'] t(2)[OF i'] and i x + by auto qed qed also have "\?A = cbox a b" @@ -2037,48 +2010,30 @@ assume "x \ \?A" then obtain c d where x: "x \ cbox c d" - "\i. i \ Basis \ - c \ i = a \ i \ d \ i = (a \ i + b \ i) / 2 \ - c \ i = (a \ i + b \ i) / 2 \ d \ i = b \ i" + "\i. i \ Basis \ c \ i = a \ i \ d \ i = ?ab i \ c \ i = ?ab i \ d \ i = b \ i" by blast - show "x\cbox a b" - unfolding mem_box - proof safe - fix i :: 'a - assume i: "i \ Basis" - then show "a \ i \ x \ i" "x \ i \ b \ i" - using x(2)[OF i] x(1)[unfolded mem_box,THEN bspec, OF i] by auto - qed + then show "x\cbox a b" + unfolding mem_box by force next fix x assume x: "x \ cbox a b" - have "\i\Basis. - \c d. (c = a\i \ d = (a\i + b\i) / 2 \ c = (a\i + b\i) / 2 \ d = b\i) \ c\x\i \ x\i \ d" + then have "\i\Basis. \c d. (c = a\i \ d = ?ab i \ c = ?ab i \ d = b\i) \ c\x\i \ x\i \ d" (is "\i\Basis. \c d. ?P i c d") - unfolding mem_box - proof - fix i :: 'a - assume i: "i \ Basis" - have "?P i (a\i) ((a \ i + b \ i) / 2) \ ?P i ((a \ i + b \ i) / 2) (b\i)" - using x[unfolded mem_box,THEN bspec, OF i] by auto - then show "\c d. ?P i c d" - by blast - qed - then obtain \ \ where - "\i\Basis. (\ \ i = a \ i \ \ \ i = (a \ i + b \ i) / 2 \ - \ \ i = (a \ i + b \ i) / 2 \ \ \ i = b \ i) \ \ \ i \ x \ i \ x \ i \ \ \ i" + unfolding mem_box by (metis linear) + then obtain \ \ where "\i\Basis. (\ \ i = a \ i \ \ \ i = ?ab i \ + \ \ i = ?ab i \ \ \ i = b \ i) \ \ \ i \ x \ i \ x \ i \ \ \ i" by (auto simp: choice_Basis_iff) then show "x\\?A" by (force simp add: mem_box) qed - finally show False - using assms by auto + finally show thesis + by (metis (no_types, lifting) assms(3) that) qed lemma interval_bisection: fixes type :: "'a::euclidean_space" assumes "P {}" - and "(\s t. P s \ P t \ interior(s) \ interior(t) = {} \ P(s \ t))" + and Un: "\S T. \P S; P T; interior(S) \ interior(T) = {}\ \ P (S \ T)" and "\ P (cbox a (b::'a))" obtains x where "x \ cbox a b" and "\e>0. \c d. x \ cbox c d \ cbox c d \ ball x e \ cbox c d \ cbox a b \ \ P (cbox c d)" @@ -2092,14 +2047,14 @@ case True then show ?thesis by auto next - case as: False + case False obtain c d where "\ P (cbox c d)" - "\i\Basis. + "\i. i \ Basis \ fst x \ i \ c \ i \ c \ i \ d \ i \ d \ i \ snd x \ i \ 2 * (d \ i - c \ i) \ snd x \ i - fst x \ i" - by (rule interval_bisection_step[of P, OF assms(1-2) as]) + by (blast intro: interval_bisection_step[of P, OF assms(1-2) False]) then show ?thesis by (rule_tac x="(c,d)" in exI) auto qed @@ -2281,33 +2236,17 @@ lemma tagged_division_finer: fixes p :: "('a::euclidean_space \ ('a::euclidean_space set)) set" - assumes "p tagged_division_of (cbox a b)" + assumes ptag: "p tagged_division_of (cbox a b)" and "gauge d" obtains q where "q tagged_division_of (cbox a b)" and "d fine q" and "\(x,k) \ p. k \ d(x) \ (x,k) \ q" proof - - let ?P = "\p. p tagged_partial_division_of (cbox a b) \ gauge d \ - (\q. q tagged_division_of (\{k. \x. (x,k) \ p}) \ d fine q \ - (\(x,k) \ p. k \ d(x) \ (x,k) \ q))" - { - have *: "finite p" "p tagged_partial_division_of (cbox a b)" - using assms(1) - unfolding tagged_division_of_def - by auto - presume "\p. finite p \ ?P p" - from this[rule_format,OF * assms(2)] - obtain q where q: "q tagged_division_of \{k. \x. (x, k) \ p}" "d fine q" "(\(x, k)\p. k \ d x \ (x, k) \ q)" - by auto - with that[of q] show ?thesis - using assms(1) by auto - } - fix p :: "('a::euclidean_space \ ('a::euclidean_space set)) set" - assume as: "finite p" - show "?P p" - apply rule - apply rule - using as + have p: "finite p" "p tagged_partial_division_of (cbox a b)" + using ptag unfolding tagged_division_of_def by auto + have "(\q. q tagged_division_of (\{k. \x. (x,k) \ p}) \ d fine q \ (\(x,k) \ p. k \ d(x) \ (x,k) \ q))" + if "finite p" "p tagged_partial_division_of (cbox a b)" "gauge d" for p + using that proof (induct p) case empty show ?case @@ -2325,7 +2264,7 @@ unfolding xk by auto note p = tagged_partial_division_ofD[OF insert(4)] obtain u v where uv: "k = cbox u v" - using p(4)[unfolded xk, OF insertI1] by blast + using p(4) xk by blast have "finite {k. \x. (x, k) \ p}" apply (rule finite_subset[of _ "snd ` p"]) using image_iff apply fastforce @@ -2363,6 +2302,9 @@ done qed qed + with p obtain q where q: "q tagged_division_of \{k. \x. (x, k) \ p}" "d fine q" "\(x, k)\p. k \ d x \ (x, k) \ q" + by (meson \gauge d\) + with ptag that show ?thesis by auto qed subsubsection \Covering lemma\ diff -r 015a95f15040 -r b034d2ae541c src/HOL/Tools/SMT/z3_replay_methods.ML --- a/src/HOL/Tools/SMT/z3_replay_methods.ML Fri Sep 29 14:12:14 2017 +0100 +++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Fri Sep 29 14:17:17 2017 +0100 @@ -426,8 +426,10 @@ abstract_eq abstract_prop (dest_prop t)) fun arith_rewrite_tac ctxt _ = - TRY o Simplifier.simp_tac ctxt - THEN_ALL_NEW (Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt) + let val backup_tac = Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt in + (TRY o Simplifier.simp_tac ctxt) THEN_ALL_NEW backup_tac + ORELSE' backup_tac + end fun prove_arith_rewrite ctxt t = prove_abstract' ctxt t arith_rewrite_tac ( diff -r 015a95f15040 -r b034d2ae541c src/Pure/General/file.scala --- a/src/Pure/General/file.scala Fri Sep 29 14:12:14 2017 +0100 +++ b/src/Pure/General/file.scala Fri Sep 29 14:17:17 2017 +0100 @@ -106,6 +106,21 @@ def pwd(): Path = path(Path.current.absolute_file) + /* relative paths */ + + def relative_path(base: Path, other: Path): Option[Path] = + { + val base_path = base.file.toPath + val other_path = other.file.toPath + if (other_path.startsWith(base_path)) + Some(path(base_path.relativize(other_path).toFile)) + else None + } + + def rebase_path(base: Path, other: Path): Option[Path] = + relative_path(base, other).map(base + _) + + /* bash path */ def bash_path(path: Path): String = Bash.string(standard_path(path)) diff -r 015a95f15040 -r b034d2ae541c src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Fri Sep 29 14:12:14 2017 +0100 +++ b/src/Pure/PIDE/resources.scala Fri Sep 29 14:17:17 2017 +0100 @@ -57,12 +57,33 @@ /* theory files */ - def loaded_files(syntax: Outer_Syntax, text: String): List[String] = - if (syntax.load_commands_in(text)) { - val spans = syntax.parse_spans(text) - spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList + def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): () => List[Path] = + { + val raw_text = with_thy_reader(name, reader => reader.source.toString) + () => { + val text = Symbol.decode(raw_text) + if (syntax.load_commands_in(text)) { + val spans = syntax.parse_spans(text) + val dir = Path.explode(name.master_dir) + spans.iterator.map(Command.span_files(syntax, _)._1).flatten. + map(a => (dir + Path.explode(a)).expand).toList + } + else Nil } - else Nil + } + + def pure_files(syntax: Outer_Syntax, dir: Path): List[Path] = + { + val roots = + for { (name, _) <- Thy_Header.ml_roots } + yield (dir + Path.explode(name)).expand + val files = + for { + (path, (_, theory)) <- roots zip Thy_Header.ml_roots + file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))() + } yield file + roots ::: files + } def theory_qualifier(name: Document.Node.Name): String = session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory)) diff -r 015a95f15040 -r b034d2ae541c src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Fri Sep 29 14:12:14 2017 +0100 +++ b/src/Pure/Thy/sessions.scala Fri Sep 29 14:17:17 2017 +0100 @@ -27,7 +27,9 @@ { val empty: Known = Known() - def make(local_dir: Path, bases: List[Base], theories: List[Document.Node.Name]): Known = + def make(local_dir: Path, bases: List[Base], + theories: List[Document.Node.Name] = Nil, + loaded_files: List[(String, List[Path])] = Nil): Known = { def bases_iterator(local: Boolean) = for { @@ -66,15 +68,21 @@ known else known + (file -> (name :: theories1)) }) + + val known_loaded_files = + (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _) + Known(known_theories, known_theories_local, - known_files.iterator.map(p => (p._1, p._2.reverse)).toMap) + known_files.iterator.map(p => (p._1, p._2.reverse)).toMap, + known_loaded_files) } } sealed case class Known( theories: Map[String, Document.Node.Name] = Map.empty, theories_local: Map[String, Document.Node.Name] = Map.empty, - files: Map[JFile, List[Document.Node.Name]] = Map.empty) + files: Map[JFile, List[Document.Node.Name]] = Map.empty, + loaded_files: Map[String, List[Path]] = Map.empty) { def platform_path: Known = copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))), @@ -106,7 +114,6 @@ sealed case class Base( pos: Position.T = Position.none, - imports: Option[Base] = None, global_theories: Map[String, String] = Map.empty, loaded_theories: Map[String, String] = Map.empty, known: Known = Known.empty, @@ -114,10 +121,9 @@ syntax: Outer_Syntax = Outer_Syntax.empty, sources: List[(Path, SHA1.Digest)] = Nil, session_graph: Graph_Display.Graph = Graph_Display.empty_graph, - errors: List[String] = Nil) + errors: List[String] = Nil, + imports: Option[Base] = None) { - def get_imports: Base = imports getOrElse Base.bootstrap(global_theories) - def platform_path: Base = copy(known = known.platform_path) def standard_path: Base = copy(known = known.standard_path) @@ -130,6 +136,8 @@ def dest_known_theories: List[(String, String)] = for ((theory, node_name) <- known.theories.toList) yield (theory, node_name.node) + + def get_imports: Base = imports getOrElse Base.bootstrap(global_theories) } sealed case class Deps(session_bases: Map[String, Base], all_known: Known) @@ -174,7 +182,7 @@ } val imports_base: Sessions.Base = parent_base.copy(known = - Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil)) + Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)))) val resources = new Resources(imports_base) @@ -200,21 +208,16 @@ val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node)) val loaded_files = if (inlined_files) { - val pure_files = - if (is_pure(info.name)) { - val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1)) - val files = - roots.flatMap(root => resources.loaded_files(syntax, File.read(root))). - map(file => info.dir + Path.explode(file)) - roots ::: files - } - else Nil - pure_files ::: thy_deps.loaded_files + if (Sessions.is_pure(info.name)) { + (Thy_Header.PURE -> resources.pure_files(syntax, info.dir)) :: + thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE) + } + else thy_deps.loaded_files } else Nil val all_files = - (theory_files ::: loaded_files ::: + (theory_files ::: loaded_files.flatMap(_._2) ::: info.files.map(file => info.dir + file) ::: info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand) @@ -257,6 +260,11 @@ ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) }) } + val known = + Known.make(info.dir, List(imports_base), + theories = thy_deps.deps.map(_.name), + loaded_files = loaded_files) + val sources = for (p <- all_files if p.is_file) yield (p, SHA1.digest(p.file)) val sources_errors = @@ -265,15 +273,15 @@ val base = Base( pos = info.pos, - imports = Some(imports_base), global_theories = global_theories, loaded_theories = thy_deps.loaded_theories, - known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)), + known = known, keywords = thy_deps.keywords, syntax = syntax, sources = sources, session_graph = session_graph, - errors = thy_deps.errors ::: sources_errors) + errors = thy_deps.errors ::: sources_errors, + imports = Some(imports_base)) session_bases + (info.name -> base) } @@ -284,13 +292,14 @@ } }) - Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2), Nil)) + Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2))) } def session_base_errors( options: Options, session: String, dirs: List[Path] = Nil, + inlined_files: Boolean = false, all_known: Boolean = false): (List[String], Base) = { val full_sessions = load(options, dirs = dirs) @@ -298,7 +307,8 @@ val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session))) val sessions: T = if (all_known) full_sessions else selected_sessions - val deps = Sessions.deps(sessions, global_theories = global_theories) + val deps = + Sessions.deps(sessions, inlined_files = inlined_files, global_theories = global_theories) val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session) (deps.errors, base) } @@ -307,9 +317,12 @@ options: Options, session: String, dirs: List[Path] = Nil, + inlined_files: Boolean = false, all_known: Boolean = false): Base = { - val (errs, base) = session_base_errors(options, session, dirs = dirs, all_known = all_known) + val (errs, base) = + session_base_errors(options, session, dirs = dirs, + inlined_files = inlined_files, all_known = all_known) if (errs.isEmpty) base else error(cat_lines(errs)) } diff -r 015a95f15040 -r b034d2ae541c src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Fri Sep 29 14:12:14 2017 +0100 +++ b/src/Pure/Thy/thy_info.scala Fri Sep 29 14:17:17 2017 +0100 @@ -88,17 +88,11 @@ (name.theory_base_name -> name.theory) // legacy } - def loaded_files: List[Path] = + def loaded_files: List[(String, List[Path])] = { - def loaded(dep: Thy_Info.Dep): List[Path] = - { - val string = resources.with_thy_reader(dep.name, - reader => Symbol.decode(reader.source.toString)) - resources.loaded_files(syntax, string). - map(a => Path.explode(dep.name.master_dir) + Path.explode(a)) - } - val dep_files = Par_List.map(loaded _, rev_deps) - ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files } + val names = deps.map(_.name) + names.map(_.theory) zip + Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _))) } override def toString: String = deps.toString