--- 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
--- 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"
;;
*)
--- 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
--- 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
--- 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)
--- 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}"
--- 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 "(\<lambda>x. \<bar>f x \<bullet> i\<bar>) integrable_on S"
using assms integrable_component [OF fcomp, where y=i] that by simp
then have "(\<lambda>x. f x \<bullet> 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
--- 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 \<Rightarrow> 'a::banach"
- assumes f: "f integrable_on {a..b}"
+ fixes f :: "real \<Rightarrow> 'a::banach"
+ assumes f: "f integrable_on {a..b}"
and x: "x \<in> {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="(\<lambda>u. f u - f x)"])
+ apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
using yx False d x y \<open>e>0\<close> assms by (auto simp: Idiff fux_int)
next
case True
@@ -6062,8 +6062,7 @@
have "norm (integral S f) \<le> integral S ((\<lambda>x. x \<bullet> k) \<circ> 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 \<subseteq> U"
by (rule \<open>convex U\<close>[unfolded convex_contains_segment, rule_format, OF \<open>x0 \<in> U\<close> \<open>x \<in> U\<close>])
from elim have [intro]: "x \<in> U" by auto
-
have "?F x - ?F x0 - ?dF (x - x0) =
integral (cbox a b) (\<lambda>y. f x y - f x0 y - fx x0 y (x - x0))"
(is "_ = ?id")
@@ -6217,7 +6215,7 @@
also have "\<dots> < e' * norm (x - x0)"
using \<open>e' > 0\<close>
apply (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])
- apply (auto simp: divide_simps e_def)
+ apply (auto simp: divide_simps e_def)
by (metis \<open>0 < e\<close> 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 \<longlongrightarrow> J) F"
proof cases
assume "content (cbox a b) = 0"
@@ -6461,19 +6457,17 @@
f integrable_continuous_real)+
have deriv: "(((\<lambda>x. integral {c..x} f) \<circ> g) has_vector_derivative g' x *\<^sub>R f (g x))
(at x within {a..b})" if "x \<in> {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 "((\<lambda>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 \<in> {a..b} - (s \<union> {a,b})" for x
using deriv[of x] that by (simp add: at_within_closed_interval o_def)
-
have "((\<lambda>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 \<union> {a,b}"]) simp_all
@@ -6805,20 +6799,21 @@
\<le> 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) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e"
+ have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e"
+ if "\<forall>x\<in>?CBOX. \<forall>x'\<in>?CBOX. norm (x' - x) < k \<longrightarrow> 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: "(\<lambda>x. ball x k) fine p"
+ using fine_division_exists \<open>0 < k\<close> by blast
+ show ?thesis
+ apply (rule op_acbd [OF division_of_tagged_division [OF ptag]])
+ using that fine ptag \<open>0 < k\<close> by (auto simp: *)
+ qed
+ then show "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> 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 \<open>0 < e\<close>
- 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 \<open>0 < e\<close> by (auto simp: zero_less_mult_iff)
qed
then show ?thesis
by simp
@@ -6861,7 +6856,6 @@
shows "((\<lambda>x::real. exp (-a*x)) has_integral exp (-a*c)/a) {c..}"
proof -
define f where "f = (\<lambda>k x. if x \<in> {c..real k} then exp (-a*x) else 0)"
-
{
fix k :: nat assume k: "of_nat k \<ge> c"
from k a
--- 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 "\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P (s \<union> t)"
- and "\<not> P (cbox a (b::'a))"
+ assumes emp: "P {}"
+ and Un: "\<And>S T. \<lbrakk>P S; P T; interior(S) \<inter> interior(T) = {}\<rbrakk> \<Longrightarrow> P (S \<union> T)"
+ and non: "\<not> P (cbox a (b::'a))"
obtains c d where "\<not> P (cbox c d)"
- and "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
+ and "\<And>i. i \<in> Basis \<Longrightarrow> a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
proof -
have "cbox a b \<noteq> {}"
- using assms(1,3) by metis
+ using emp non by metis
then have ab: "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
by (force simp: mem_box)
- have UN_cases: "\<lbrakk>finite f;
- \<And>s. s\<in>f \<Longrightarrow> P s;
- \<And>s. s\<in>f \<Longrightarrow> \<exists>a b. s = cbox a b;
- \<And>s t. s\<in>f \<Longrightarrow> t\<in>f \<Longrightarrow> s \<noteq> t \<Longrightarrow> interior s \<inter> interior t = {}\<rbrakk> \<Longrightarrow> P (\<Union>f)" for f
- proof (induct f rule: finite_induct)
- case empty
- show ?case
- using assms(1) by auto
+ have UN_cases: "\<lbrakk>finite \<F>;
+ \<And>S. S\<in>\<F> \<Longrightarrow> P S;
+ \<And>S. S\<in>\<F> \<Longrightarrow> \<exists>a b. S = cbox a b;
+ \<And>S T. S\<in>\<F> \<Longrightarrow> T\<in>\<F> \<Longrightarrow> S \<noteq> T \<Longrightarrow> interior S \<inter> interior T = {}\<rbrakk> \<Longrightarrow> P (\<Union>\<F>)" for \<F>
+ proof (induct \<F> 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. \<forall>i\<in>Basis. (c\<bullet>i = a\<bullet>i) \<and> (d\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<or>
- (c\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<and> (d\<bullet>i = b\<bullet>i)}"
- let ?PP = "\<lambda>c d. \<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
- {
- presume "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d) \<Longrightarrow> False"
- then show thesis
- unfolding atomize_not not_all
- by (blast intro: that)
- }
- assume as: "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d)"
- have "P (\<Union>?A)"
+ let ?ab = "\<lambda>i. (a\<bullet>i + b\<bullet>i) / 2"
+ let ?A = "{cbox c d | c d::'a. \<forall>i\<in>Basis. (c\<bullet>i = a\<bullet>i) \<and> (d\<bullet>i = ?ab i) \<or>
+ (c\<bullet>i = ?ab i) \<and> (d\<bullet>i = b\<bullet>i)}"
+ have "P (\<Union>?A)"
+ if "\<And>c d. \<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i \<Longrightarrow> P (cbox c d)"
proof (rule UN_cases)
- let ?B = "(\<lambda>s. cbox (\<Sum>i\<in>Basis. (if i \<in> s then a\<bullet>i else (a\<bullet>i + b\<bullet>i) / 2) *\<^sub>R i::'a)
- (\<Sum>i\<in>Basis. (if i \<in> s then (a\<bullet>i + b\<bullet>i) / 2 else b\<bullet>i) *\<^sub>R i)) ` {s. s \<subseteq> Basis}"
+ let ?B = "(\<lambda>S. cbox (\<Sum>i\<in>Basis. (if i \<in> S then a\<bullet>i else ?ab i) *\<^sub>R i::'a)
+ (\<Sum>i\<in>Basis. (if i \<in> S then ?ab i else b\<bullet>i) *\<^sub>R i)) ` {s. s \<subseteq> Basis}"
have "?A \<subseteq> ?B"
proof
fix x
assume "x \<in> ?A"
then obtain c d
where x: "x = cbox c d"
- "\<And>i. i \<in> Basis \<Longrightarrow>
- c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
- c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i" by blast
- show "x \<in> ?B"
- unfolding image_iff x
- apply (rule_tac x="{i. i\<in>Basis \<and> c\<bullet>i = a\<bullet>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
+ "\<And>i. i \<in> Basis \<Longrightarrow>
+ c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i"
+ by blast
+ have "c = (\<Sum>i\<in>Basis. (if c \<bullet> i = a \<bullet> i then a \<bullet> i else ?ab i) *\<^sub>R i)"
+ "d = (\<Sum>i\<in>Basis. (if c \<bullet> i = a \<bullet> i then ?ab i else b \<bullet> i) *\<^sub>R i)"
+ using x(2) ab by (fastforce simp add: euclidean_eq_iff[where 'a='a])+
+ then show "x \<in> ?B"
+ unfolding x by (rule_tac x="{i. i\<in>Basis \<and> c\<bullet>i = a\<bullet>i}" in image_eqI) auto
qed
then show "finite ?A"
by (rule finite_subset) auto
next
- fix s
- assume "s \<in> ?A"
+ fix S
+ assume "S \<in> ?A"
then obtain c d
- where s: "s = cbox c d"
- "\<And>i. i \<in> Basis \<Longrightarrow>
- c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
- c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
+ where s: "S = cbox c d"
+ "\<And>i. i \<in> Basis \<Longrightarrow> c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i"
by blast
- show "P s"
- unfolding s
- apply (rule as[rule_format])
- using ab s(2) by force
- show "\<exists>a b. s = cbox a b"
+ show "P S"
+ unfolding s using ab s(2) by (fastforce intro!: that)
+ show "\<exists>a b. S = cbox a b"
unfolding s by auto
- fix t
- assume "t \<in> ?A"
+ fix T
+ assume "T \<in> ?A"
then obtain e f where t:
- "t = cbox e f"
- "\<And>i. i \<in> Basis \<Longrightarrow>
- e \<bullet> i = a \<bullet> i \<and> f \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
- e \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> f \<bullet> i = b \<bullet> i"
+ "T = cbox e f"
+ "\<And>i. i \<in> Basis \<Longrightarrow> e \<bullet> i = a \<bullet> i \<and> f \<bullet> i = ?ab i \<or> e \<bullet> i = ?ab i \<and> f \<bullet> i = b \<bullet> i"
by blast
- assume "s \<noteq> t"
+ assume "S \<noteq> T"
then have "\<not> (c = e \<and> d = f)"
unfolding s t by auto
then obtain i where "c\<bullet>i \<noteq> e\<bullet>i \<or> d\<bullet>i \<noteq> f\<bullet>i" and i': "i \<in> Basis"
@@ -2011,24 +1993,15 @@
using t(2)[OF i'] \<open>c \<bullet> i \<noteq> e \<bullet> i \<or> d \<bullet> i \<noteq> f \<bullet> i\<close> i' s(2) t(2) by fastforce
have *: "\<And>s t. (\<And>a. a \<in> s \<Longrightarrow> a \<in> t \<Longrightarrow> False) \<Longrightarrow> s \<inter> t = {}"
by auto
- show "interior s \<inter> interior t = {}"
+ show "interior S \<inter> interior T = {}"
unfolding s t interior_cbox
proof (rule *)
fix x
assume "x \<in> box c d" "x \<in> box e f"
then have x: "c\<bullet>i < d\<bullet>i" "e\<bullet>i < f\<bullet>i" "c\<bullet>i < f\<bullet>i" "e\<bullet>i < d\<bullet>i"
- unfolding mem_box using i'
- by force+
- show False using s(2)[OF i']
- proof safe
- assume as: "c \<bullet> i = a \<bullet> i" "d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2"
- show False
- using t(2)[OF i'] and i x unfolding as by (fastforce simp add:field_simps)
- next
- assume as: "c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2" "d \<bullet> i = b \<bullet> 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 "\<Union>?A = cbox a b"
@@ -2037,48 +2010,30 @@
assume "x \<in> \<Union>?A"
then obtain c d where x:
"x \<in> cbox c d"
- "\<And>i. i \<in> Basis \<Longrightarrow>
- c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
- c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
+ "\<And>i. i \<in> Basis \<Longrightarrow> c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i"
by blast
- show "x\<in>cbox a b"
- unfolding mem_box
- proof safe
- fix i :: 'a
- assume i: "i \<in> Basis"
- then show "a \<bullet> i \<le> x \<bullet> i" "x \<bullet> i \<le> b \<bullet> i"
- using x(2)[OF i] x(1)[unfolded mem_box,THEN bspec, OF i] by auto
- qed
+ then show "x\<in>cbox a b"
+ unfolding mem_box by force
next
fix x
assume x: "x \<in> cbox a b"
- have "\<forall>i\<in>Basis.
- \<exists>c d. (c = a\<bullet>i \<and> d = (a\<bullet>i + b\<bullet>i) / 2 \<or> c = (a\<bullet>i + b\<bullet>i) / 2 \<and> d = b\<bullet>i) \<and> c\<le>x\<bullet>i \<and> x\<bullet>i \<le> d"
+ then have "\<forall>i\<in>Basis. \<exists>c d. (c = a\<bullet>i \<and> d = ?ab i \<or> c = ?ab i \<and> d = b\<bullet>i) \<and> c\<le>x\<bullet>i \<and> x\<bullet>i \<le> d"
(is "\<forall>i\<in>Basis. \<exists>c d. ?P i c d")
- unfolding mem_box
- proof
- fix i :: 'a
- assume i: "i \<in> Basis"
- have "?P i (a\<bullet>i) ((a \<bullet> i + b \<bullet> i) / 2) \<or> ?P i ((a \<bullet> i + b \<bullet> i) / 2) (b\<bullet>i)"
- using x[unfolded mem_box,THEN bspec, OF i] by auto
- then show "\<exists>c d. ?P i c d"
- by blast
- qed
- then obtain \<alpha> \<beta> where
- "\<forall>i\<in>Basis. (\<alpha> \<bullet> i = a \<bullet> i \<and> \<beta> \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
- \<alpha> \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> \<beta> \<bullet> i = b \<bullet> i) \<and> \<alpha> \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> \<beta> \<bullet> i"
+ unfolding mem_box by (metis linear)
+ then obtain \<alpha> \<beta> where "\<forall>i\<in>Basis. (\<alpha> \<bullet> i = a \<bullet> i \<and> \<beta> \<bullet> i = ?ab i \<or>
+ \<alpha> \<bullet> i = ?ab i \<and> \<beta> \<bullet> i = b \<bullet> i) \<and> \<alpha> \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> \<beta> \<bullet> i"
by (auto simp: choice_Basis_iff)
then show "x\<in>\<Union>?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 "(\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P(s \<union> t))"
+ and Un: "\<And>S T. \<lbrakk>P S; P T; interior(S) \<inter> interior(T) = {}\<rbrakk> \<Longrightarrow> P (S \<union> T)"
and "\<not> P (cbox a (b::'a))"
obtains x where "x \<in> cbox a b"
and "\<forall>e>0. \<exists>c d. x \<in> cbox c d \<and> cbox c d \<subseteq> ball x e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> 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 "\<not> P (cbox c d)"
- "\<forall>i\<in>Basis.
+ "\<And>i. i \<in> Basis \<Longrightarrow>
fst x \<bullet> i \<le> c \<bullet> i \<and>
c \<bullet> i \<le> d \<bullet> i \<and>
d \<bullet> i \<le> snd x \<bullet> i \<and>
2 * (d \<bullet> i - c \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> 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 \<times> ('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 "\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q"
proof -
- let ?P = "\<lambda>p. p tagged_partial_division_of (cbox a b) \<longrightarrow> gauge d \<longrightarrow>
- (\<exists>q. q tagged_division_of (\<Union>{k. \<exists>x. (x,k) \<in> p}) \<and> d fine q \<and>
- (\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q))"
- {
- have *: "finite p" "p tagged_partial_division_of (cbox a b)"
- using assms(1)
- unfolding tagged_division_of_def
- by auto
- presume "\<And>p. finite p \<Longrightarrow> ?P p"
- from this[rule_format,OF * assms(2)]
- obtain q where q: "q tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> p}" "d fine q" "(\<forall>(x, k)\<in>p. k \<subseteq> d x \<longrightarrow> (x, k) \<in> q)"
- by auto
- with that[of q] show ?thesis
- using assms(1) by auto
- }
- fix p :: "('a::euclidean_space \<times> ('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 "(\<exists>q. q tagged_division_of (\<Union>{k. \<exists>x. (x,k) \<in> p}) \<and> d fine q \<and> (\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> 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. \<exists>x. (x, k) \<in> 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 \<Union>{k. \<exists>x. (x, k) \<in> p}" "d fine q" "\<forall>(x, k)\<in>p. k \<subseteq> d x \<longrightarrow> (x, k) \<in> q"
+ by (meson \<open>gauge d\<close>)
+ with ptag that show ?thesis by auto
qed
subsubsection \<open>Covering lemma\<close>
--- 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 (
--- 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))
--- 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))
--- 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))
}
--- 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