--- a/src/HOL/Analysis/Borel_Space.thy Fri Jun 23 13:16:04 2017 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy Fri Jun 23 15:01:06 2017 +0200
@@ -1379,6 +1379,13 @@
shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M"
using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
+lemma borel_measurable_uminus_eq [simp]:
+ fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
+ shows "(\<lambda>x. - f x) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r")
+proof
+ assume ?l from borel_measurable_uminus[OF this] show ?r by simp
+qed auto
+
lemma affine_borel_measurable_vector:
fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
assumes "f \<in> borel_measurable M"
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Fri Jun 23 13:16:04 2017 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Fri Jun 23 15:01:06 2017 +0200
@@ -1341,9 +1341,6 @@
using assms apply (blast intro: has_contour_integral_subpath)
done
-lemma has_integral_integrable_integral: "(f has_integral i) s \<longleftrightarrow> f integrable_on s \<and> integral s f = i"
- by blast
-
lemma has_integral_contour_integral_subpath:
assumes "f contour_integrable_on g" "valid_path g" "u \<in> {0..1}" "v \<in> {0..1}" "u \<le> v"
shows "(((\<lambda>x. f(g x) * vector_derivative g (at x)))
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Jun 23 13:16:04 2017 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Jun 23 15:01:06 2017 +0200
@@ -860,7 +860,7 @@
then have "(?f has_integral F b - F a) {a .. b}"
by (subst has_integral_cong[where g=f]) auto
then have "(?f has_integral F b - F a) UNIV"
- by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto
+ by (intro has_integral_on_superset[where T=UNIV and S="{a..b}"]) auto
ultimately show "integral\<^sup>L lborel ?f = F b - F a"
by (rule has_integral_unique)
qed
@@ -908,6 +908,7 @@
(infixr "absolutely'_integrable'_on" 46)
where "f absolutely_integrable_on s \<equiv> set_integrable lebesgue s f"
+
lemma absolutely_integrable_on_def:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and> (\<lambda>x. norm (f x)) integrable_on s"
@@ -933,6 +934,17 @@
by (auto simp: integrable_on_def nn_integral_completion)
qed
qed
+
+lemma absolutely_integrable_on_null [intro]:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "content (cbox a b) = 0 \<Longrightarrow> f absolutely_integrable_on (cbox a b)"
+ by (auto simp: absolutely_integrable_on_def)
+
+lemma absolutely_integrable_on_open_interval:
+ fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
+ shows "f absolutely_integrable_on box a b \<longleftrightarrow>
+ f absolutely_integrable_on cbox a b"
+ by (auto simp: integrable_on_open_interval absolutely_integrable_on_def)
lemma absolutely_integrable_restrict_UNIV:
"(\<lambda>x. if x \<in> s then f x else 0) absolutely_integrable_on UNIV \<longleftrightarrow> f absolutely_integrable_on s"
@@ -2075,7 +2087,7 @@
assumes "f integrable_on UNIV"
and "\<forall>d. d division_of (\<Union>d) \<longrightarrow> sum (\<lambda>k. norm (integral k f)) d \<le> B"
shows "f absolutely_integrable_on UNIV"
-proof (rule absolutely_integrable_onI, fact, rule)
+proof (rule absolutely_integrable_onI, fact)
let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of (\<Union>d)}"
have D_1: "?D \<noteq> {}"
by (rule elementary_interval) auto
@@ -2091,7 +2103,7 @@
apply (rule assms(2)[rule_format])
apply auto
done
- show "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
+ have "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
apply (subst has_integral_alt')
apply safe
proof goal_cases
@@ -2224,6 +2236,8 @@
qed
qed (insert K, auto)
qed
+ then show "(\<lambda>x. norm (f x)) integrable_on UNIV"
+ by blast
qed
lemma absolutely_integrable_add[intro]:
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Jun 23 13:16:04 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Jun 23 15:01:06 2017 +0200
@@ -273,13 +273,13 @@
definition "integral i f = (SOME y. (f has_integral y) i \<or> ~ f integrable_on i \<and> y=0)"
-lemma integrable_integral[dest]: "f integrable_on i \<Longrightarrow> (f has_integral (integral i f)) i"
+lemma integrable_integral[intro]: "f integrable_on i \<Longrightarrow> (f has_integral (integral i f)) i"
unfolding integrable_on_def integral_def by (metis (mono_tags, lifting) someI_ex)
lemma not_integrable_integral: "~ f integrable_on i \<Longrightarrow> integral i f = 0"
unfolding integrable_on_def integral_def by blast
-lemma has_integral_integrable[intro]: "(f has_integral i) s \<Longrightarrow> f integrable_on s"
+lemma has_integral_integrable[dest]: "(f has_integral i) s \<Longrightarrow> f integrable_on s"
unfolding integrable_on_def by auto
lemma has_integral_integral: "f integrable_on s \<longleftrightarrow> (f has_integral (integral s f)) s"
@@ -358,7 +358,6 @@
apply (rule someI_ex)
by blast
-
lemma has_integral_const [intro]:
fixes a b :: "'a::euclidean_space"
shows "((\<lambda>x. c) has_integral (content (cbox a b) *\<^sub>R c)) (cbox a b)"
@@ -372,6 +371,9 @@
shows "((\<lambda>x. c) has_integral (content {a .. b} *\<^sub>R c)) {a .. b}"
by (metis box_real(2) has_integral_const)
+lemma has_integral_integrable_integral: "(f has_integral i) s \<longleftrightarrow> f integrable_on s \<and> integral s f = i"
+ by blast
+
lemma integral_const [simp]:
fixes a b :: "'a::euclidean_space"
shows "integral (cbox a b) (\<lambda>x. c) = content (cbox a b) *\<^sub>R c"
@@ -408,17 +410,17 @@
by (subst has_integral_alt) (force simp add: *)
qed
-lemma has_integral_0[simp]: "((\<lambda>x::'n::euclidean_space. 0) has_integral 0) s"
+lemma has_integral_0[simp]: "((\<lambda>x::'n::euclidean_space. 0) has_integral 0) S"
by (rule has_integral_is_0) auto
-lemma has_integral_0_eq[simp]: "((\<lambda>x. 0) has_integral i) s \<longleftrightarrow> i = 0"
+lemma has_integral_0_eq[simp]: "((\<lambda>x. 0) has_integral i) S \<longleftrightarrow> i = 0"
using has_integral_unique[OF has_integral_0] by auto
lemma has_integral_linear:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
- assumes "(f has_integral y) s"
+ assumes "(f has_integral y) S"
and "bounded_linear h"
- shows "((h \<circ> f) has_integral ((h y))) s"
+ shows "((h \<circ> f) has_integral ((h y))) S"
proof -
interpret bounded_linear h
using assms(2) .
@@ -427,11 +429,11 @@
have lem: "\<And>a b y f::'n\<Rightarrow>'a. (f has_integral y) (cbox a b) \<Longrightarrow> ((h \<circ> f) has_integral h y) (cbox a b)"
unfolding has_integral_cbox by (drule tendsto) (simp add: sum scaleR split_beta')
{
- presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
+ presume "\<not> (\<exists>a b. S = cbox a b) \<Longrightarrow> ?thesis"
then show ?thesis
using assms(1) lem by blast
}
- assume as: "\<not> (\<exists>a b. s = cbox a b)"
+ assume as: "\<not> (\<exists>a b. S = cbox a b)"
then show ?thesis
proof (subst has_integral_alt, clarsimp)
fix e :: real
@@ -440,17 +442,17 @@
obtain M where M:
"M > 0"
"\<And>a b. ball 0 M \<subseteq> cbox a b \<Longrightarrow>
- \<exists>z. ((\<lambda>x. if x \<in> s then f x else 0) has_integral z) (cbox a b) \<and> norm (z - y) < e / B"
+ \<exists>z. ((\<lambda>x. if x \<in> S then f x else 0) has_integral z) (cbox a b) \<and> norm (z - y) < e / B"
using has_integral_altD[OF assms(1) as *] by blast
show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
- (\<exists>z. ((\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) has_integral z) (cbox a b) \<and> norm (z - h y) < e)"
+ (\<exists>z. ((\<lambda>x. if x \<in> S then (h \<circ> f) x else 0) has_integral z) (cbox a b) \<and> norm (z - h y) < e)"
proof (rule_tac x=M in exI, clarsimp simp add: M, goal_cases)
case prems: (1 a b)
obtain z where z:
- "((\<lambda>x. if x \<in> s then f x else 0) has_integral z) (cbox a b)"
+ "((\<lambda>x. if x \<in> S then f x else 0) has_integral z) (cbox a b)"
"norm (z - y) < e / B"
using M(2)[OF prems(1)] by blast
- have *: "(\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) = h \<circ> (\<lambda>x. if x \<in> s then f x else 0)"
+ have *: "(\<lambda>x. if x \<in> S then (h \<circ> f) x else 0) = h \<circ> (\<lambda>x. if x \<in> S then f x else 0)"
using zero by auto
show ?case
apply (rule_tac x="h z" in exI)
@@ -462,7 +464,7 @@
qed
lemma has_integral_scaleR_left:
- "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x *\<^sub>R c) has_integral (y *\<^sub>R c)) s"
+ "(f has_integral y) S \<Longrightarrow> ((\<lambda>x. f x *\<^sub>R c) has_integral (y *\<^sub>R c)) S"
using has_integral_linear[OF _ bounded_linear_scaleR_left] by (simp add: comp_def)
lemma integrable_on_scaleR_left:
@@ -472,27 +474,27 @@
lemma has_integral_mult_left:
fixes c :: "_ :: real_normed_algebra"
- shows "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x * c) has_integral (y * c)) s"
+ shows "(f has_integral y) S \<Longrightarrow> ((\<lambda>x. f x * c) has_integral (y * c)) S"
using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def)
-text\<open>The case analysis eliminates the condition @{term "f integrable_on s"} at the cost
+text\<open>The case analysis eliminates the condition @{term "f integrable_on S"} at the cost
of the type class constraint \<open>division_ring\<close>\<close>
corollary integral_mult_left [simp]:
fixes c:: "'a::{real_normed_algebra,division_ring}"
- shows "integral s (\<lambda>x. f x * c) = integral s f * c"
-proof (cases "f integrable_on s \<or> c = 0")
+ shows "integral S (\<lambda>x. f x * c) = integral S f * c"
+proof (cases "f integrable_on S \<or> c = 0")
case True then show ?thesis
by (force intro: has_integral_mult_left)
next
- case False then have "~ (\<lambda>x. f x * c) integrable_on s"
- using has_integral_mult_left [of "(\<lambda>x. f x * c)" _ s "inverse c"]
- by (force simp add: mult.assoc)
+ case False then have "~ (\<lambda>x. f x * c) integrable_on S"
+ using has_integral_mult_left [of "(\<lambda>x. f x * c)" _ S "inverse c"]
+ by (auto simp add: mult.assoc)
with False show ?thesis by (simp add: not_integrable_integral)
qed
corollary integral_mult_right [simp]:
fixes c:: "'a::{real_normed_field}"
- shows "integral s (\<lambda>x. c * f x) = c * integral s f"
+ shows "integral S (\<lambda>x. c * f x) = c * integral S f"
by (simp add: mult.commute [of c])
corollary integral_divide [simp]:
@@ -506,7 +508,7 @@
shows "(f has_integral y) i \<Longrightarrow> ((\<lambda>x. c * f x) has_integral (c * y)) i"
using has_integral_linear[OF _ bounded_linear_mult_right] by (simp add: comp_def)
-lemma has_integral_cmul: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
+lemma has_integral_cmul: "(f has_integral k) S \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) S"
unfolding o_def[symmetric]
by (metis has_integral_linear bounded_linear_scaleR_right)
@@ -523,17 +525,17 @@
unfolding real_scaleR_def .
qed
-lemma has_integral_neg: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral -k) s"
+lemma has_integral_neg: "(f has_integral k) S \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral -k) S"
by (drule_tac c="-1" in has_integral_cmul) auto
-lemma has_integral_neg_iff: "((\<lambda>x. - f x) has_integral k) s \<longleftrightarrow> (f has_integral - k) s"
+lemma has_integral_neg_iff: "((\<lambda>x. - f x) has_integral k) S \<longleftrightarrow> (f has_integral - k) S"
using has_integral_neg[of f "- k"] has_integral_neg[of "\<lambda>x. - f x" k] by auto
lemma has_integral_add:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
- assumes "(f has_integral k) s"
- and "(g has_integral l) s"
- shows "((\<lambda>x. f x + g x) has_integral (k + l)) s"
+ assumes "(f has_integral k) S"
+ and "(g has_integral l) S"
+ shows "((\<lambda>x. f x + g x) has_integral (k + l)) S"
proof -
have lem: "(f has_integral k) (cbox a b) \<Longrightarrow> (g has_integral l) (cbox a b) \<Longrightarrow>
((\<lambda>x. f x + g x) has_integral (k + l)) (cbox a b)"
@@ -541,11 +543,11 @@
unfolding has_integral_cbox
by (simp add: split_beta' scaleR_add_right sum.distrib[abs_def] tendsto_add)
{
- presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
+ presume "\<not> (\<exists>a b. S = cbox a b) \<Longrightarrow> ?thesis"
then show ?thesis
using assms lem by force
}
- assume as: "\<not> (\<exists>a b. s = cbox a b)"
+ assume as: "\<not> (\<exists>a b. S = cbox a b)"
then show ?thesis
proof (subst has_integral_alt, clarsimp, goal_cases)
case (1 e)
@@ -555,13 +557,13 @@
obtain B1 where B1:
"0 < B1"
"\<And>a b. ball 0 B1 \<subseteq> cbox a b \<Longrightarrow>
- \<exists>z. ((\<lambda>x. if x \<in> s then f x else 0) has_integral z) (cbox a b) \<and> norm (z - k) < e / 2"
+ \<exists>z. ((\<lambda>x. if x \<in> S then f x else 0) has_integral z) (cbox a b) \<and> norm (z - k) < e / 2"
by blast
from has_integral_altD[OF assms(2) as *]
obtain B2 where B2:
"0 < B2"
"\<And>a b. ball 0 B2 \<subseteq> (cbox a b) \<Longrightarrow>
- \<exists>z. ((\<lambda>x. if x \<in> s then g x else 0) has_integral z) (cbox a b) \<and> norm (z - l) < e / 2"
+ \<exists>z. ((\<lambda>x. if x \<in> S then g x else 0) has_integral z) (cbox a b) \<and> norm (z - l) < e / 2"
by blast
show ?case
proof (rule_tac x="max B1 B2" in exI, clarsimp simp add: max.strict_coboundedI1 B1)
@@ -570,17 +572,17 @@
then have *: "ball 0 B1 \<subseteq> cbox a (b::'n)" "ball 0 B2 \<subseteq> cbox a (b::'n)"
by auto
obtain w where w:
- "((\<lambda>x. if x \<in> s then f x else 0) has_integral w) (cbox a b)"
+ "((\<lambda>x. if x \<in> S then f x else 0) has_integral w) (cbox a b)"
"norm (w - k) < e / 2"
using B1(2)[OF *(1)] by blast
obtain z where z:
- "((\<lambda>x. if x \<in> s then g x else 0) has_integral z) (cbox a b)"
+ "((\<lambda>x. if x \<in> S then g x else 0) has_integral z) (cbox a b)"
"norm (z - l) < e / 2"
using B2(2)[OF *(2)] by blast
- have *: "\<And>x. (if x \<in> s then f x + g x else 0) =
- (if x \<in> s then f x else 0) + (if x \<in> s then g x else 0)"
+ have *: "\<And>x. (if x \<in> S then f x + g x else 0) =
+ (if x \<in> S then f x else 0) + (if x \<in> S then g x else 0)"
by auto
- show "\<exists>z. ((\<lambda>x. if x \<in> s then f x + g x else 0) has_integral z) (cbox a b) \<and> norm (z - (k + l)) < e"
+ show "\<exists>z. ((\<lambda>x. if x \<in> S then f x + g x else 0) has_integral z) (cbox a b) \<and> norm (z - (k + l)) < e"
apply (rule_tac x="w + z" in exI)
apply (simp add: lem[OF w(1) z(1), unfolded *[symmetric]])
using norm_triangle_ineq[of "w - k" "z - l"] w(2) z(2)
@@ -591,93 +593,92 @@
qed
lemma has_integral_diff:
- "(f has_integral k) s \<Longrightarrow> (g has_integral l) s \<Longrightarrow>
- ((\<lambda>x. f x - g x) has_integral (k - l)) s"
- using has_integral_add[OF _ has_integral_neg, of f k s g l]
+ "(f has_integral k) S \<Longrightarrow> (g has_integral l) S \<Longrightarrow>
+ ((\<lambda>x. f x - g x) has_integral (k - l)) S"
+ using has_integral_add[OF _ has_integral_neg, of f k S g l]
by (auto simp: algebra_simps)
lemma integral_0 [simp]:
- "integral s (\<lambda>x::'n::euclidean_space. 0::'m::real_normed_vector) = 0"
+ "integral S (\<lambda>x::'n::euclidean_space. 0::'m::real_normed_vector) = 0"
by (rule integral_unique has_integral_0)+
-lemma integral_add: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
- integral s (\<lambda>x. f x + g x) = integral s f + integral s g"
+lemma integral_add: "f integrable_on S \<Longrightarrow> g integrable_on S \<Longrightarrow>
+ integral S (\<lambda>x. f x + g x) = integral S f + integral S g"
by (rule integral_unique) (metis integrable_integral has_integral_add)
-lemma integral_cmul [simp]: "integral s (\<lambda>x. c *\<^sub>R f x) = c *\<^sub>R integral s f"
-proof (cases "f integrable_on s \<or> c = 0")
- case True with has_integral_cmul show ?thesis by force
+lemma integral_cmul [simp]: "integral S (\<lambda>x. c *\<^sub>R f x) = c *\<^sub>R integral S f"
+proof (cases "f integrable_on S \<or> c = 0")
+ case True with has_integral_cmul integrable_integral show ?thesis
+ by fastforce
next
- case False then have "~ (\<lambda>x. c *\<^sub>R f x) integrable_on s"
- using has_integral_cmul [of "(\<lambda>x. c *\<^sub>R f x)" _ s "inverse c"]
- by force
+ case False then have "~ (\<lambda>x. c *\<^sub>R f x) integrable_on S"
+ using has_integral_cmul [of "(\<lambda>x. c *\<^sub>R f x)" _ S "inverse c"] by auto
with False show ?thesis by (simp add: not_integrable_integral)
qed
-lemma integral_neg [simp]: "integral s (\<lambda>x. - f x) = - integral s f"
-proof (cases "f integrable_on s")
+lemma integral_neg [simp]: "integral S (\<lambda>x. - f x) = - integral S f"
+proof (cases "f integrable_on S")
case True then show ?thesis
by (simp add: has_integral_neg integrable_integral integral_unique)
next
- case False then have "~ (\<lambda>x. - f x) integrable_on s"
- using has_integral_neg [of "(\<lambda>x. - f x)" _ s ]
- by force
+ case False then have "~ (\<lambda>x. - f x) integrable_on S"
+ using has_integral_neg [of "(\<lambda>x. - f x)" _ S ] by auto
with False show ?thesis by (simp add: not_integrable_integral)
qed
-lemma integral_diff: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
- integral s (\<lambda>x. f x - g x) = integral s f - integral s g"
+lemma integral_diff: "f integrable_on S \<Longrightarrow> g integrable_on S \<Longrightarrow>
+ integral S (\<lambda>x. f x - g x) = integral S f - integral S g"
by (rule integral_unique) (metis integrable_integral has_integral_diff)
-lemma integrable_0: "(\<lambda>x. 0) integrable_on s"
+lemma integrable_0: "(\<lambda>x. 0) integrable_on S"
unfolding integrable_on_def using has_integral_0 by auto
-lemma integrable_add: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow> (\<lambda>x. f x + g x) integrable_on s"
+lemma integrable_add: "f integrable_on S \<Longrightarrow> g integrable_on S \<Longrightarrow> (\<lambda>x. f x + g x) integrable_on S"
unfolding integrable_on_def by(auto intro: has_integral_add)
-lemma integrable_cmul: "f integrable_on s \<Longrightarrow> (\<lambda>x. c *\<^sub>R f(x)) integrable_on s"
+lemma integrable_cmul: "f integrable_on S \<Longrightarrow> (\<lambda>x. c *\<^sub>R f(x)) integrable_on S"
unfolding integrable_on_def by(auto intro: has_integral_cmul)
lemma integrable_on_cmult_iff:
fixes c :: real
assumes "c \<noteq> 0"
- shows "(\<lambda>x. c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
- using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c] \<open>c \<noteq> 0\<close>
+ shows "(\<lambda>x. c * f x) integrable_on S \<longleftrightarrow> f integrable_on S"
+ using integrable_cmul[of "\<lambda>x. c * f x" S "1 / c"] integrable_cmul[of f S c] \<open>c \<noteq> 0\<close>
by auto
lemma integrable_on_cmult_left:
- assumes "f integrable_on s"
- shows "(\<lambda>x. of_real c * f x) integrable_on s"
- using integrable_cmul[of f s "of_real c"] assms
+ assumes "f integrable_on S"
+ shows "(\<lambda>x. of_real c * f x) integrable_on S"
+ using integrable_cmul[of f S "of_real c"] assms
by (simp add: scaleR_conv_of_real)
-lemma integrable_neg: "f integrable_on s \<Longrightarrow> (\<lambda>x. -f(x)) integrable_on s"
+lemma integrable_neg: "f integrable_on S \<Longrightarrow> (\<lambda>x. -f(x)) integrable_on S"
unfolding integrable_on_def by(auto intro: has_integral_neg)
lemma integrable_diff:
- "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow> (\<lambda>x. f x - g x) integrable_on s"
+ "f integrable_on S \<Longrightarrow> g integrable_on S \<Longrightarrow> (\<lambda>x. f x - g x) integrable_on S"
unfolding integrable_on_def by(auto intro: has_integral_diff)
lemma integrable_linear:
- "f integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> (h \<circ> f) integrable_on s"
+ "f integrable_on S \<Longrightarrow> bounded_linear h \<Longrightarrow> (h \<circ> f) integrable_on S"
unfolding integrable_on_def by(auto intro: has_integral_linear)
lemma integral_linear:
- "f integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> integral s (h \<circ> f) = h (integral s f)"
- apply (rule has_integral_unique [where i=s and f = "h \<circ> f"])
+ "f integrable_on S \<Longrightarrow> bounded_linear h \<Longrightarrow> integral S (h \<circ> f) = h (integral S f)"
+ apply (rule has_integral_unique [where i=S and f = "h \<circ> f"])
apply (simp_all add: integrable_integral integrable_linear has_integral_linear )
done
lemma integral_component_eq[simp]:
fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
- assumes "f integrable_on s"
- shows "integral s (\<lambda>x. f x \<bullet> k) = integral s f \<bullet> k"
+ assumes "f integrable_on S"
+ shows "integral S (\<lambda>x. f x \<bullet> k) = integral S f \<bullet> k"
unfolding integral_linear[OF assms(1) bounded_linear_inner_left,unfolded o_def] ..
lemma has_integral_sum:
assumes "finite t"
- and "\<forall>a\<in>t. ((f a) has_integral (i a)) s"
- shows "((\<lambda>x. sum (\<lambda>a. f a x) t) has_integral (sum i t)) s"
+ and "\<forall>a\<in>t. ((f a) has_integral (i a)) S"
+ shows "((\<lambda>x. sum (\<lambda>a. f a x) t) has_integral (sum i t)) S"
using assms(1) subset_refl[of t]
proof (induct rule: finite_subset_induct)
case empty
@@ -689,9 +690,9 @@
qed
lemma integral_sum:
- "\<lbrakk>finite t; \<forall>a\<in>t. (f a) integrable_on s\<rbrakk> \<Longrightarrow>
- integral s (\<lambda>x. sum (\<lambda>a. f a x) t) = sum (\<lambda>a. integral s (f a)) t"
- by (auto intro: has_integral_sum integrable_integral)
+ "\<lbrakk>finite I; \<And>a. a \<in> I \<Longrightarrow> f a integrable_on S\<rbrakk> \<Longrightarrow>
+ integral S (\<lambda>x. \<Sum>a\<in>I. f a x) = (\<Sum>a\<in>I. integral S (f a))"
+ by (simp add: has_integral_sum integrable_integral integral_unique)
lemma integrable_sum:
"\<lbrakk>finite I; \<And>a. a \<in> I \<Longrightarrow> f a integrable_on S\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>a\<in>I. f a x) integrable_on S"
@@ -927,7 +928,7 @@
by auto
from choice[OF this] guess d .. note d=conjunctD2[OF this[rule_format],rule_format]
have "\<And>n. gauge (\<lambda>x. \<Inter>{d i x |i. i \<in> {0..n}})"
- apply (rule gauge_inters)
+ apply (rule gauge_Inter)
using d(1)
apply auto
done
@@ -993,33 +994,33 @@
subsection \<open>Additivity of integral on abutting intervals.\<close>
lemma tagged_division_split_left_inj_content:
- assumes d: "d tagged_division_of i"
- and "(x1, k1) \<in> d" "(x2, k2) \<in> d" "k1 \<noteq> k2" "k1 \<inter> {x. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c}" "k \<in> Basis"
- shows "content (k1 \<inter> {x. x\<bullet>k \<le> c}) = 0"
+ assumes \<D>: "\<D> tagged_division_of S"
+ and "(x1, K1) \<in> \<D>" "(x2, K2) \<in> \<D>" "K1 \<noteq> K2" "K1 \<inter> {x. x\<bullet>k \<le> c} = K2 \<inter> {x. x\<bullet>k \<le> c}" "k \<in> Basis"
+ shows "content (K1 \<inter> {x. x\<bullet>k \<le> c}) = 0"
proof -
- from tagged_division_ofD(4)[OF d \<open>(x1, k1) \<in> d\<close>] obtain a b where k1: "k1 = cbox a b"
+ from tagged_division_ofD(4)[OF \<D> \<open>(x1, K1) \<in> \<D>\<close>] obtain a b where K1: "K1 = cbox a b"
by auto
- show ?thesis
- unfolding k1 interval_split[OF \<open>k \<in> Basis\<close>]
- unfolding content_eq_0_interior
- unfolding interval_split[OF \<open>k \<in> Basis\<close>, symmetric] k1[symmetric]
+ then have "interior (K1 \<inter> {x. x \<bullet> k \<le> c}) = {}"
by (metis tagged_division_split_left_inj assms)
+ then show ?thesis
+ unfolding K1 interval_split[OF \<open>k \<in> Basis\<close>] by (auto simp: content_eq_0_interior)
qed
lemma tagged_division_split_right_inj_content:
- assumes d: "d tagged_division_of i"
- and "(x1, k1) \<in> d" "(x2, k2) \<in> d" "k1 \<noteq> k2" "k1 \<inter> {x. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}" "k \<in> Basis"
- shows "content (k1 \<inter> {x. x\<bullet>k \<ge> c}) = 0"
+ assumes \<D>: "\<D> tagged_division_of S"
+ and "(x1, K1) \<in> \<D>" "(x2, K2) \<in> \<D>" "K1 \<noteq> K2" "K1 \<inter> {x. x\<bullet>k \<ge> c} = K2 \<inter> {x. x\<bullet>k \<ge> c}" "k \<in> Basis"
+ shows "content (K1 \<inter> {x. x\<bullet>k \<ge> c}) = 0"
proof -
- from tagged_division_ofD(4)[OF d \<open>(x1, k1) \<in> d\<close>] obtain a b where k1: "k1 = cbox a b"
+ from tagged_division_ofD(4)[OF \<D> \<open>(x1, K1) \<in> \<D>\<close>] obtain a b where K1: "K1 = cbox a b"
by auto
- show ?thesis
- unfolding k1 interval_split[OF \<open>k \<in> Basis\<close>]
- unfolding content_eq_0_interior
- unfolding interval_split[OF \<open>k \<in> Basis\<close>, symmetric] k1[symmetric]
+ then have "interior (K1 \<inter> {x. c \<le> x \<bullet> k}) = {}"
by (metis tagged_division_split_right_inj assms)
+ then show ?thesis
+ unfolding K1 interval_split[OF \<open>k \<in> Basis\<close>]
+ by (auto simp: content_eq_0_interior)
qed
+
lemma has_integral_split:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes fi: "(f has_integral i) (cbox a b \<inter> {x. x\<bullet>k \<le> c})"
@@ -1313,7 +1314,7 @@
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{real_normed_vector,complete_space}"
assumes f: "f integrable_on cbox a b"
and k: "k \<in> Basis"
- shows "f integrable_on (cbox a b \<inter> {x. x\<bullet>k \<le> c})" (is ?thesis1)
+ shows "f integrable_on (cbox a b \<inter> {x. x\<bullet>k \<le> c})" (is ?thesis1)
and "f integrable_on (cbox a b \<inter> {x. x\<bullet>k \<ge> c})" (is ?thesis2)
proof -
obtain y where y: "(f has_integral y) (cbox a b)"
@@ -1327,12 +1328,12 @@
if "e > 0" for e
proof -
have "e/2 > 0" using that by auto
- with has_integral_separate_sides[OF y this k, of c]
- obtain d
+ with has_integral_separate_sides[OF y this k, of c]
+ obtain d
where "gauge d"
- and d: "\<And>p1 p2. \<lbrakk>p1 tagged_division_of cbox a b \<inter> {x. x \<bullet> k \<le> c}; d fine p1;
- p2 tagged_division_of cbox a b \<inter> {x. c \<le> x \<bullet> k}; d fine p2\<rbrakk>
- \<Longrightarrow> norm ((\<Sum>(x,K)\<in>p1. content K *\<^sub>R f x) + (\<Sum>(x,K)\<in>p2. content K *\<^sub>R f x) - y) < e/2"
+ and d: "\<And>p1 p2. \<lbrakk>p1 tagged_division_of cbox a b \<inter> {x. x \<bullet> k \<le> c}; d fine p1;
+ p2 tagged_division_of cbox a b \<inter> {x. c \<le> x \<bullet> k}; d fine p2\<rbrakk>
+ \<Longrightarrow> norm ((\<Sum>(x,K)\<in>p1. content K *\<^sub>R f x) + (\<Sum>(x,K)\<in>p2. content K *\<^sub>R f x) - y) < e/2"
by metis
show ?thesis
proof (rule_tac x=d in exI, clarsimp simp add: \<open>gauge d\<close>)
@@ -1349,7 +1350,7 @@
by (auto simp add: algebra_simps)
qed
qed
- qed
+ qed
with f show ?thesis1
by (simp add: interval_split[OF k] integrable_cauchy)
have "\<exists>d. gauge d \<and>
@@ -1359,12 +1360,12 @@
if "e > 0" for e
proof -
have "e/2 > 0" using that by auto
- with has_integral_separate_sides[OF y this k, of c]
- obtain d
+ with has_integral_separate_sides[OF y this k, of c]
+ obtain d
where "gauge d"
- and d: "\<And>p1 p2. \<lbrakk>p1 tagged_division_of cbox a b \<inter> {x. x \<bullet> k \<le> c}; d fine p1;
- p2 tagged_division_of cbox a b \<inter> {x. c \<le> x \<bullet> k}; d fine p2\<rbrakk>
- \<Longrightarrow> norm ((\<Sum>(x,K)\<in>p1. content K *\<^sub>R f x) + (\<Sum>(x,K)\<in>p2. content K *\<^sub>R f x) - y) < e/2"
+ and d: "\<And>p1 p2. \<lbrakk>p1 tagged_division_of cbox a b \<inter> {x. x \<bullet> k \<le> c}; d fine p1;
+ p2 tagged_division_of cbox a b \<inter> {x. c \<le> x \<bullet> k}; d fine p2\<rbrakk>
+ \<Longrightarrow> norm ((\<Sum>(x,K)\<in>p1. content K *\<^sub>R f x) + (\<Sum>(x,K)\<in>p2. content K *\<^sub>R f x) - y) < e/2"
by metis
show ?thesis
proof (rule_tac x=d in exI, clarsimp simp add: \<open>gauge d\<close>)
@@ -1381,7 +1382,7 @@
by (auto simp add: algebra_simps)
qed
qed
- qed
+ qed
with f show ?thesis2
by (simp add: interval_split[OF k] integrable_cauchy)
qed
@@ -2272,10 +2273,11 @@
using fint gf
apply (subst has_integral_alt)
apply (subst (asm) has_integral_alt)
- apply (simp add: split: if_split_asm)
- apply (blast dest: *)
- apply (elim all_forward imp_forward ex_forward)
- apply (force dest: *[where f="\<lambda>x. if x\<in>T then f x else 0" and g="\<lambda>x. if x \<in> T then g x else 0"])+
+ apply (simp split: if_split_asm)
+ apply (blast dest: *)
+ apply (erule_tac V = "\<forall>a b. T \<noteq> cbox a b" in thin_rl)
+ apply (elim all_forward imp_forward ex_forward all_forward conj_forward asm_rl)
+ apply (auto dest!: *[where f="\<lambda>x. if x\<in>T then f x else 0" and g="\<lambda>x. if x \<in> T then g x else 0"])
done
qed
@@ -2764,7 +2766,7 @@
fixes a::real
assumes "a \<le> b"
shows "integral {a..b} (\<lambda>x. x) = (if a \<le> b then (b\<^sup>2 - a\<^sup>2) / 2 else 0)"
-using ident_has_integral integral_unique by fastforce
+ by (metis assms ident_has_integral integral_unique)
lemma ident_integrable_on:
fixes a::real
@@ -2881,7 +2883,8 @@
have "?sum a = (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a)"
by (rule sum.reindex_cong) (auto simp add: inj_on_def Dg_def one)
finally show c: ?case .
- case 2 show ?case using c integral_unique by force
+ case 2 show ?case using c integral_unique
+ by (metis (lifting) add.commute diff_eq_eq integral_unique)
case 3 show ?case using c by force
qed
@@ -3111,7 +3114,7 @@
shows "f integrable_on {a .. b}"
using assms
unfolding integrable_on_def
- by (fastforce intro!:has_integral_combine)
+ by (auto intro!:has_integral_combine)
subsection \<open>Reduce integrability to "local" integrability.\<close>
@@ -3181,7 +3184,7 @@
using False x by (simp add: algebra_simps integral_combine)
have fux_int: "((\<lambda>u. f u - f x) has_integral integral {x..y} f - (y - x) *\<^sub>R f x) {x..y}"
apply (rule has_integral_diff)
- using x y apply (force intro: integrable_integral [OF integrable_subinterval_real [OF f]])
+ using x y apply (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]])
using has_integral_const_real [of "f x" x y] False
apply (simp add: )
done
@@ -3199,7 +3202,7 @@
using True x y by (simp add: algebra_simps integral_combine)
have fux_int: "((\<lambda>u. f u - f x) has_integral integral {y..x} f - (x - y) *\<^sub>R f x) {y..x}"
apply (rule has_integral_diff)
- using x y apply (force intro: integrable_integral [OF integrable_subinterval_real [OF f]])
+ using x y apply (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]])
using has_integral_const_real [of "f x" y x] True
apply (simp add: )
done
@@ -5086,43 +5089,57 @@
text \<open>Hence a general restriction property.\<close>
-lemma has_integral_restrict[simp]:
- assumes "s \<subseteq> t"
- shows "((\<lambda>x. if x \<in> s then f x else (0::'a::banach)) has_integral i) t \<longleftrightarrow> (f has_integral i) s"
+lemma has_integral_restrict [simp]:
+ fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
+ assumes "S \<subseteq> T"
+ shows "((\<lambda>x. if x \<in> S then f x else 0) has_integral i) T \<longleftrightarrow> (f has_integral i) S"
proof -
- have *: "\<And>x. (if x \<in> t then if x \<in> s then f x else 0 else 0) = (if x\<in>s then f x else 0)"
+ have *: "\<And>x. (if x \<in> T then if x \<in> S then f x else 0 else 0) = (if x\<in>S then f x else 0)"
using assms by auto
show ?thesis
apply (subst(2) has_integral')
apply (subst has_integral')
- unfolding *
- apply rule
+ apply (simp add: *)
done
qed
-lemma has_integral_restrict_UNIV:
+corollary has_integral_restrict_UNIV:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
shows "((\<lambda>x. if x \<in> s then f x else 0) has_integral i) UNIV \<longleftrightarrow> (f has_integral i) s"
by auto
+lemma has_integral_restrict_Int:
+ fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
+ shows "((\<lambda>x. if x \<in> S then f x else 0) has_integral i) T \<longleftrightarrow> (f has_integral i) (S \<inter> T)"
+proof -
+ have "((\<lambda>x. if x \<in> T then if x \<in> S then f x else 0 else 0) has_integral i) UNIV =
+ ((\<lambda>x. if x \<in> S \<inter> T then f x else 0) has_integral i) UNIV"
+ by (rule has_integral_cong) auto
+ then show ?thesis
+ using has_integral_restrict_UNIV by fastforce
+qed
+
+lemma integral_restrict_Int:
+ fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
+ shows "integral T (\<lambda>x. if x \<in> S then f x else 0) = integral (S \<inter> T) f"
+ by (metis (no_types, lifting) has_integral_cong has_integral_restrict_Int integrable_integral integral_unique not_integrable_integral)
+
+lemma integrable_restrict_Int:
+ fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
+ shows "(\<lambda>x. if x \<in> S then f x else 0) integrable_on T \<longleftrightarrow> f integrable_on (S \<inter> T)"
+ using has_integral_restrict_Int by fastforce
+
lemma has_integral_on_superset:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes "\<forall>x. x \<notin> s \<longrightarrow> f x = 0"
- and "s \<subseteq> t"
- and "(f has_integral i) s"
- shows "(f has_integral i) t"
+ assumes f: "(f has_integral i) S"
+ and "\<And>x. x \<notin> S \<Longrightarrow> f x = 0"
+ and "S \<subseteq> T"
+ shows "(f has_integral i) T"
proof -
- have "(\<lambda>x. if x \<in> s then f x else 0) = (\<lambda>x. if x \<in> t then f x else 0)"
- apply rule
- using assms(1-2)
- apply auto
- done
- then show ?thesis
- using assms(3)
- apply (subst has_integral_restrict_UNIV[symmetric])
- apply (subst(asm) has_integral_restrict_UNIV[symmetric])
- apply auto
- done
+ have "(\<lambda>x. if x \<in> S then f x else 0) = (\<lambda>x. if x \<in> T then f x else 0)"
+ using assms by fastforce
+ with f show ?thesis
+ by (simp only: has_integral_restrict_UNIV [symmetric, of f])
qed
lemma integrable_on_superset:
@@ -5135,7 +5152,7 @@
unfolding integrable_on_def
by (auto intro:has_integral_on_superset)
-lemma integral_restrict_univ[intro]:
+lemma integral_restrict_UNIV [intro]:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
shows "f integrable_on s \<Longrightarrow> integral UNIV (\<lambda>x. if x \<in> s then f x else 0) = integral s f"
apply (rule integral_unique)
@@ -5149,6 +5166,20 @@
unfolding integrable_on_def
by auto
+lemma has_integral_subset_component_le:
+ fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+ assumes k: "k \<in> Basis"
+ and as: "S \<subseteq> T" "(f has_integral i) S" "(f has_integral j) T" "\<And>x. x\<in>T \<Longrightarrow> 0 \<le> f(x)\<bullet>k"
+ shows "i\<bullet>k \<le> j\<bullet>k"
+proof -
+ have "((\<lambda>x. if x \<in> S then f x else 0) has_integral i) UNIV"
+ "((\<lambda>x. if x \<in> T then f x else 0) has_integral j) UNIV"
+ by (simp_all add: assms)
+ then show ?thesis
+ apply (rule has_integral_component_le[OF k])
+ using as by auto
+qed
+
lemma negligible_on_intervals: "negligible s \<longleftrightarrow> (\<forall>a b. negligible(s \<inter> cbox a b))" (is "?l \<longleftrightarrow> ?r")
proof
assume ?r
@@ -5193,48 +5224,65 @@
lemma has_integral_spike_set_eq:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes "negligible ((s - t) \<union> (t - s))"
- shows "(f has_integral y) s \<longleftrightarrow> (f has_integral y) t"
+ assumes "negligible ((S - T) \<union> (T - S))"
+ shows "(f has_integral y) S \<longleftrightarrow> (f has_integral y) T"
unfolding has_integral_restrict_UNIV[symmetric,of f]
apply (rule has_integral_spike_eq[OF assms])
by (auto split: if_split_asm)
lemma has_integral_spike_set:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes "(f has_integral y) s" "negligible ((s - t) \<union> (t - s))"
- shows "(f has_integral y) t"
+ assumes "(f has_integral y) S" "negligible ((S - T) \<union> (T - S))"
+ shows "(f has_integral y) T"
using assms has_integral_spike_set_eq
by auto
lemma integrable_spike_set:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes "f integrable_on s" and "negligible ((s - t) \<union> (t - s))"
- shows "f integrable_on t"
+ assumes "f integrable_on S" and "negligible ((S - T) \<union> (T - S))"
+ shows "f integrable_on T"
using assms by (simp add: integrable_on_def has_integral_spike_set_eq)
lemma integrable_spike_set_eq:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes "negligible ((s - t) \<union> (t - s))"
- shows "f integrable_on s \<longleftrightarrow> f integrable_on t"
-by (blast intro: integrable_spike_set assms negligible_subset)
+ assumes "negligible ((S - T) \<union> (T - S))"
+ shows "f integrable_on S \<longleftrightarrow> f integrable_on T"
+ by (blast intro: integrable_spike_set assms negligible_subset)
+
+lemma has_integral_interior:
+ fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
+ shows "negligible(frontier S) \<Longrightarrow> (f has_integral y) (interior S) \<longleftrightarrow> (f has_integral y) S"
+ apply (rule has_integral_spike_set_eq)
+ apply (auto simp: frontier_def Un_Diff closure_def)
+ apply (metis Diff_eq_empty_iff interior_subset negligible_empty)
+ done
+
+lemma has_integral_closure:
+ fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
+ shows "negligible(frontier S) \<Longrightarrow> (f has_integral y) (closure S) \<longleftrightarrow> (f has_integral y) S"
+ apply (rule has_integral_spike_set_eq)
+ apply (auto simp: Un_Diff closure_Un_frontier negligible_diff)
+ by (simp add: Diff_eq closure_Un_frontier)
+
+lemma has_integral_open_interval:
+ fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
+ shows "(f has_integral y) (box a b) \<longleftrightarrow> (f has_integral y) (cbox a b)"
+ unfolding interior_cbox [symmetric]
+ by (metis frontier_cbox has_integral_interior negligible_frontier_interval)
+
+lemma integrable_on_open_interval:
+ fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
+ shows "f integrable_on box a b \<longleftrightarrow> f integrable_on cbox a b"
+ by (simp add: has_integral_open_interval integrable_on_def)
+
+lemma integral_open_interval:
+ fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
+ shows "integral(box a b) f = integral(cbox a b) f"
+ by (metis has_integral_integrable_integral has_integral_open_interval not_integrable_integral)
+
subsection \<open>More lemmas that are useful later\<close>
-lemma has_integral_subset_component_le:
- fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
- assumes k: "k \<in> Basis"
- and as: "s \<subseteq> t" "(f has_integral i) s" "(f has_integral j) t" "\<forall>x\<in>t. 0 \<le> f(x)\<bullet>k"
- shows "i\<bullet>k \<le> j\<bullet>k"
-proof -
- note has_integral_restrict_UNIV[symmetric, of f]
- note as(2-3)[unfolded this] note * = has_integral_component_le[OF k this]
- show ?thesis
- apply (rule *)
- using as(1,4)
- apply auto
- done
-qed
-
lemma has_integral_subset_le:
fixes f :: "'n::euclidean_space \<Rightarrow> real"
assumes "s \<subseteq> t"
@@ -5504,10 +5552,10 @@
have e: "e/3 > 0"
using that by auto
then obtain g h i j where ij: "\<bar>i - j\<bar> < e/3"
- and "(g has_integral i) (cbox a b)"
- and "(h has_integral j) (cbox a b)"
+ and "(g has_integral i) (cbox a b)"
+ and "(h has_integral j) (cbox a b)"
and fgh: "\<And>x. x \<in> cbox a b \<Longrightarrow> g x \<le> f x \<and> f x \<le> h x"
- using assms real_norm_def by metis
+ using assms real_norm_def by metis
then obtain d1 d2 where "gauge d1" "gauge d2"
and d1: "\<And>p. \<lbrakk>p tagged_division_of cbox a b; d1 fine p\<rbrakk> \<Longrightarrow>
\<bar>(\<Sum>(x,K)\<in>p. content K *\<^sub>R g x) - i\<bar> < e/3"
@@ -5515,10 +5563,10 @@
\<bar>(\<Sum>(x,K) \<in> p. content K *\<^sub>R h x) - j\<bar> < e/3"
by (metis e has_integral real_norm_def)
have "\<bar>(\<Sum>(x,K) \<in> p1. content K *\<^sub>R f x) - (\<Sum>(x,K) \<in> p2. content K *\<^sub>R f x)\<bar> < e"
- if p1: "p1 tagged_division_of cbox a b" and 11: "d1 fine p1" and 21: "d2 fine p1"
+ if p1: "p1 tagged_division_of cbox a b" and 11: "d1 fine p1" and 21: "d2 fine p1"
and p2: "p2 tagged_division_of cbox a b" and 12: "d1 fine p2" and 22: "d2 fine p2" for p1 p2
proof -
- have *: "\<And>g1 g2 h1 h2 f1 f2.
+ have *: "\<And>g1 g2 h1 h2 f1 f2.
\<lbrakk>\<bar>g2 - i\<bar> < e/3; \<bar>g1 - i\<bar> < e/3; \<bar>h2 - j\<bar> < e/3; \<bar>h1 - j\<bar> < e/3;
g1 - h2 \<le> f1 - f2; f1 - f2 \<le> h1 - g2\<rbrakk>
\<Longrightarrow> \<bar>f1 - f2\<bar> < e"
@@ -6617,9 +6665,9 @@
prefer 3
apply (subst abs_of_nonneg)
apply (rule *[OF assms(2) that(1)[THEN spec]])
- apply (subst integral_restrict_univ[symmetric,OF int])
+ apply (subst integral_restrict_UNIV[symmetric,OF int])
unfolding ifif
- unfolding integral_restrict_univ[OF int']
+ unfolding integral_restrict_UNIV[OF int']
apply (rule integral_subset_le[OF _ int' assms(2)])
using assms(1)
apply auto
@@ -6692,8 +6740,8 @@
next
case 1
show ?case
- apply (subst integral_restrict_univ[symmetric,OF int])
- unfolding ifif integral_restrict_univ[OF int']
+ apply (subst integral_restrict_UNIV[symmetric,OF int])
+ unfolding ifif integral_restrict_UNIV[OF int']
apply (rule integral_subset_le[OF _ int'])
using assms
apply auto
@@ -6795,7 +6843,7 @@
proof (intro monotone_convergence_increasing allI ballI assms)
show "bounded {integral s (f k) |k. True}"
unfolding x by (rule convergent_imp_bounded) fact
- qed (auto intro: f)
+ qed (use f in auto)
then have "integral s g = x'"
by (intro LIMSEQ_unique[OF _ \<open>x \<longlonglongrightarrow> x'\<close>]) (simp add: x_eq)
with * show ?thesis
@@ -7924,7 +7972,7 @@
hence "(f n has_integral (F n - F a)) {a..n}"
by (rule has_integral_eq [rotated]) (simp add: f_def)
thus "(f n has_integral (F n - F a)) {a..}"
- by (rule has_integral_on_superset [rotated 2]) (auto simp: f_def)
+ by (rule has_integral_on_superset) (auto simp: f_def)
qed
have integral_f: "integral {a..} (f n) = (if n \<ge> a then F n - F a else 0)" for n :: nat
proof (cases "n \<ge> a")
@@ -7934,7 +7982,7 @@
case False
have "(f n has_integral 0) {a}" by (rule has_integral_refl)
hence "(f n has_integral 0) {a..}"
- by (rule has_integral_on_superset [rotated 2]) (insert False, simp_all add: f_def)
+ by (rule has_integral_on_superset) (insert False, simp_all add: f_def)
with False show ?thesis by (simp add: integral_unique)
qed
--- a/src/HOL/Analysis/Interval_Integral.thy Fri Jun 23 13:16:04 2017 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Fri Jun 23 15:01:06 2017 +0200
@@ -660,7 +660,7 @@
(auto simp del: ereal_less_eq simp add: ereal_less_eq(3)[symmetric])
qed
have 2: "set_borel_measurable lborel (einterval a b) f"
- by (auto simp del: real_scaleR_def intro!: set_borel_measurable_continuous
+ by (auto simp del: real_scaleR_def intro!: borel_measurable_continuous_on_indicator
simp: continuous_on_eq_continuous_at einterval_iff f)
have 3: "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> B - A"
apply (subst FTCi)
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Fri Jun 23 13:16:04 2017 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Fri Jun 23 15:01:06 2017 +0200
@@ -387,6 +387,12 @@
and measurable_lborel2[simp]: "measurable lborel M = measurable borel M"
by (simp_all add: lborel_def)
+lemma sets_lebesgue_on_refl [iff]: "S \<in> sets (lebesgue_on S)"
+ by (metis inf_top.right_neutral sets.top space_borel space_completion space_lborel space_restrict_space)
+
+lemma Compl_in_sets_lebesgue: "-A \<in> sets lebesgue \<longleftrightarrow> A \<in> sets lebesgue"
+ by (metis Compl_eq_Diff_UNIV double_compl space_borel space_completion space_lborel Sigma_Algebra.sets.compl_sets)
+
context
begin
@@ -495,7 +501,11 @@
lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0"
using emeasure_lborel_cbox[of x x] nonempty_Basis
- by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: cbox_sing prod_constant)
+ by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: prod_constant)
+
+lemma fmeasurable_cbox [iff]: "cbox a b \<in> fmeasurable lborel"
+ and fmeasurable_box [iff]: "box a b \<in> fmeasurable lborel"
+ by (auto simp: fmeasurable_def emeasure_lborel_box_eq emeasure_lborel_cbox_eq)
lemma
fixes l u :: real
--- a/src/HOL/Analysis/Set_Integral.thy Fri Jun 23 13:16:04 2017 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy Fri Jun 23 15:01:06 2017 +0200
@@ -1840,22 +1840,10 @@
translations
"CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
-lemma set_borel_measurable_continuous:
- fixes f :: "_ \<Rightarrow> _::real_normed_vector"
- assumes "S \<in> sets borel" "continuous_on S f"
- shows "set_borel_measurable borel S f"
-proof -
- have "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable borel"
- by (intro assms borel_measurable_continuous_on_if continuous_on_const)
- also have "(\<lambda>x. if x \<in> S then f x else 0) = (\<lambda>x. indicator S x *\<^sub>R f x)"
- by auto
- finally show ?thesis .
-qed
-
lemma set_measurable_continuous_on_ivl:
assumes "continuous_on {a..b} (f :: real \<Rightarrow> real)"
shows "set_borel_measurable borel {a..b} f"
- by (rule set_borel_measurable_continuous[OF _ assms]) simp
+ by (rule borel_measurable_continuous_on_indicator[OF _ assms]) simp
text\<open>This notation is from Sébastien Gouëzel: His use is not directly in line with the
--- a/src/HOL/Analysis/Tagged_Division.thy Fri Jun 23 13:16:04 2017 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy Fri Jun 23 15:01:06 2017 +0200
@@ -275,9 +275,15 @@
lemma gauge_Int[intro]: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. d1 x \<inter> d2 x)"
unfolding gauge_def by auto
-lemma gauge_inters:
+lemma gauge_reflect:
+ fixes \<D> :: "'a::euclidean_space \<Rightarrow> 'a set"
+ shows "gauge \<D> \<Longrightarrow> gauge (\<lambda>x. uminus ` \<D> (- x))"
+ using equation_minus_iff
+ by (auto simp: gauge_def surj_def intro!: open_surjective_linear_image linear_uminus)
+
+lemma gauge_Inter:
assumes "finite s"
- and "\<forall>d\<in>s. gauge (f d)"
+ and "\<And>d. d\<in>s \<Longrightarrow> gauge (f d)"
shows "gauge (\<lambda>x. \<Inter>{f d x | d. d \<in> s})"
proof -
have *: "\<And>x. {f d x |d. d \<in> s} = (\<lambda>d. f d x) ` s"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Jun 23 13:16:04 2017 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Jun 23 15:01:06 2017 +0200
@@ -7537,6 +7537,23 @@
then show "f x \<in> interior (f ` S)"
by (meson assms imageI image_mono interiorI interior_subset open_bijective_linear_image_eq open_interior)
qed
+
+lemma interior_injective_linear_image:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
+ assumes "linear f" "inj f"
+ shows "interior(f ` S) = f ` (interior S)"
+ by (simp add: linear_injective_imp_surjective assms bijI interior_bijective_linear_image)
+
+lemma interior_surjective_linear_image:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
+ assumes "linear f" "surj f"
+ shows "interior(f ` S) = f ` (interior S)"
+ by (simp add: assms interior_injective_linear_image linear_surjective_imp_injective)
+
+lemma interior_negations:
+ fixes S :: "'a::euclidean_space set"
+ shows "interior(uminus ` S) = image uminus (interior S)"
+ by (simp add: bij_uminus interior_bijective_linear_image linear_uminus)
text \<open>Also bilinear functions, in composition form.\<close>
--- a/src/HOL/Nunchaku/Nunchaku.thy Fri Jun 23 13:16:04 2017 +0200
+++ b/src/HOL/Nunchaku/Nunchaku.thy Fri Jun 23 15:01:06 2017 +0200
@@ -11,7 +11,7 @@
The "$NUNCHAKU_HOME" environment variable must be set to the absolute path to
the directory containing the "nunchaku" executable. The Isabelle components
-for CVC4 and Kodkodi are necessary to use these backends.
+for CVC4 and Kodkodi are necessary to use these backend solvers.
*)
theory Nunchaku
--- a/src/HOL/Nunchaku/Tools/nunchaku.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku.ML Fri Jun 23 15:01:06 2017 +0200
@@ -12,7 +12,8 @@
datatype mode = Auto_Try | Try | Normal
type mode_of_operation_params =
- {falsify: bool,
+ {solvers: string list,
+ falsify: bool,
assms: bool,
spy: bool,
overlord: bool,
@@ -74,7 +75,8 @@
datatype mode = Auto_Try | Try | Normal;
type mode_of_operation_params =
- {falsify: bool,
+ {solvers: string list,
+ falsify: bool,
assms: bool,
spy: bool,
overlord: bool,
@@ -138,7 +140,7 @@
val timeout_slack = seconds 1.0;
fun run_chaku_on_prop state
- ({mode_of_operation_params = {falsify, assms, spy, overlord, expect},
+ ({mode_of_operation_params = {solvers, falsify, assms, spy, overlord, expect},
scope_of_search_params = {wfs, whacks, cards, monos},
output_format_params = {verbose, debug, evals, atomss, ...},
optimization_params = {specialize, ...},
@@ -157,8 +159,9 @@
val das_wort_Model = if falsify then "Countermodel" else "Model";
val das_wort_model = if falsify then "countermodel" else "model";
- val tool_params = {overlord = overlord, debug = debug, specialize = specialize,
- timeout = timeout};
+ val tool_params =
+ {solvers = solvers, overlord = overlord, debug = debug, specialize = specialize,
+ timeout = timeout};
fun run () =
let
--- a/src/HOL/Nunchaku/Tools/nunchaku_commands.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku_commands.ML Fri Jun 23 15:01:06 2017 +0200
@@ -27,6 +27,7 @@
("max_genuine", "1"),
("max_potential", "1"),
("overlord", "false"),
+ ("solvers", "cvc4 kodkod paradox smbc"),
("specialize", "true"),
("spy", "false"),
("timeout", "30"),
@@ -100,6 +101,7 @@
val raw_lookup = AList.lookup (op =) raw_params;
val lookup = Option.map stringify_raw_param_value o raw_lookup;
val lookup_string = the_default "" o lookup;
+ val lookup_strings = these o Option.map (space_explode " ") o lookup;
fun general_lookup_bool option default_value name =
(case lookup name of
@@ -161,28 +163,33 @@
Const x => x
| t => error ("Not a constant: " ^ Syntax.string_of_term ctxt t));
+ val solvers = lookup_strings "solvers";
+ val falsify = lookup_bool "falsify";
+ val assms = lookup_bool "assms";
+ val spy = getenv "NUNCHAKU_SPY" = "yes" orelse lookup_bool "spy";
+ val overlord = lookup_bool "overlord";
+ val expect = lookup_string "expect";
+
val wfs = lookup_bool_option_assigns read_const_polymorphic "wf";
val whacks = lookup_bool_assigns read_term_polymorphic "whack";
val cards = lookup_int_range_assigns read_type_polymorphic "card";
val monos = lookup_bool_option_assigns read_type_polymorphic "mono";
- val falsify = lookup_bool "falsify";
+
val debug = (mode <> Auto_Try andalso lookup_bool "debug");
val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose");
- val overlord = lookup_bool "overlord";
- val spy = getenv "NUNCHAKU_SPY" = "yes" orelse lookup_bool "spy";
- val assms = lookup_bool "assms";
+ val max_potential = if mode = Normal then Int.max (0, lookup_int "max_potential") else 0;
+ val max_genuine = Int.max (0, lookup_int "max_genuine");
+ val evals = these (lookup_term_list_option_polymorphic "eval");
+ val atomss = lookup_strings_assigns read_type_polymorphic "atoms";
+
val specialize = lookup_bool "specialize";
+ val multithread = mode = Normal andalso lookup_bool "multithread";
+
val timeout = lookup_time "timeout";
val wf_timeout = lookup_time "wf_timeout";
- val multithread = mode = Normal andalso lookup_bool "multithread";
- val evals = these (lookup_term_list_option_polymorphic "eval");
- val atomss = lookup_strings_assigns read_type_polymorphic "atoms";
- val max_potential = if mode = Normal then Int.max (0, lookup_int "max_potential") else 0;
- val max_genuine = Int.max (0, lookup_int "max_genuine");
- val expect = lookup_string "expect";
val mode_of_operation_params =
- {falsify = falsify, assms = assms, spy = spy, overlord = overlord,
+ {solvers = solvers, falsify = falsify, assms = assms, spy = spy, overlord = overlord,
expect = expect};
val scope_of_search_params =
--- a/src/HOL/Nunchaku/Tools/nunchaku_tool.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku_tool.ML Fri Jun 23 15:01:06 2017 +0200
@@ -12,7 +12,8 @@
type nun_problem = Nunchaku_Problem.nun_problem
type tool_params =
- {overlord: bool,
+ {solvers: string list,
+ overlord: bool,
debug: bool,
specialize: bool,
timeout: Time.time}
@@ -45,7 +46,8 @@
open Nunchaku_Problem;
type tool_params =
- {overlord: bool,
+ {solvers: string list,
+ overlord: bool,
debug: bool,
specialize: bool,
timeout: Time.time};
@@ -73,10 +75,10 @@
val nunchaku_home_env_var = "NUNCHAKU_HOME";
-val cached_outcome =
- Synchronized.var "Nunchaku_Tool.cached_outcome" (NONE : (nun_problem * nun_outcome) option);
+val cached_outcome = Synchronized.var "Nunchaku_Tool.cached_outcome"
+ (NONE : ((string list * nun_problem) * nun_outcome) option);
-fun uncached_solve_nun_problem ({overlord, specialize, timeout, ...} : tool_params)
+fun uncached_solve_nun_problem ({solvers, overlord, specialize, timeout, ...} : tool_params)
(problem as {sound, complete, ...}) =
with_tmp_or_overlord_file overlord "nunchaku" "nun" (fn prob_path =>
if getenv nunchaku_home_env_var = "" then
@@ -87,6 +89,7 @@
"PATH=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^
nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^
(if specialize then "" else "--no-specialize ") ^
+ "--solvers \"" ^ Bash_Syntax.string (space_implode " " solvers) ^ "\" " ^
"--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^
File.bash_path prob_path;
val comments =
@@ -114,23 +117,25 @@
simplify_spaces (elide_string 1000 (if error <> "" then error else output)))
end);
-fun solve_nun_problem (params as {overlord, debug, ...}) problem =
- (case (overlord orelse debug,
- AList.lookup (op =) (the_list (Synchronized.value cached_outcome)) problem) of
- (false, SOME outcome) => outcome
- | _ =>
- let
- val outcome = uncached_solve_nun_problem params problem;
+fun solve_nun_problem (params as {solvers, overlord, debug, ...}) problem =
+ let val key = (solvers, problem) in
+ (case (overlord orelse debug,
+ AList.lookup (op =) (the_list (Synchronized.value cached_outcome)) key) of
+ (false, SOME outcome) => outcome
+ | _ =>
+ let
+ val outcome = uncached_solve_nun_problem params problem;
- fun update_cache () =
- Synchronized.change cached_outcome (K (SOME (problem, outcome)));
- in
- (case outcome of
- Unsat => update_cache ()
- | Sat _ => update_cache ()
- | Unknown _ => update_cache ()
- | _ => ());
- outcome
- end);
+ fun update_cache () =
+ Synchronized.change cached_outcome (K (SOME (key, outcome)));
+ in
+ (case outcome of
+ Unsat => update_cache ()
+ | Sat _ => update_cache ()
+ | Unknown _ => update_cache ()
+ | _ => ());
+ outcome
+ end)
+ end;
end;
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Fri Jun 23 15:01:06 2017 +0200
@@ -959,7 +959,7 @@
| SOME {vcs, path, ...} =>
let
val (proved, unproved) = partition_vcs vcs;
- val _ = List.app Thm.consolidate (maps (#2 o snd) proved);
+ val _ = Thm.consolidate (maps (#2 o snd) proved);
val (proved', proved'') =
List.partition (fn (_, (_, thms, _, _)) =>
exists (#oracle o Thm.peek_status) thms) proved;
--- a/src/Pure/Concurrent/cache.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/Pure/Concurrent/cache.ML Fri Jun 23 15:01:06 2017 +0200
@@ -23,7 +23,7 @@
(case lookup tab x of
SOME y => (y, tab)
| NONE =>
- let val y = Lazy.lazy (fn () => f x)
+ let val y = Lazy.lazy_name "cache" (fn () => f x)
in (y, update (x, y) tab) end))
|> Lazy.force;
in apply end;
--- a/src/Pure/Concurrent/event_timer.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/Pure/Concurrent/event_timer.ML Fri Jun 23 15:01:06 2017 +0200
@@ -148,7 +148,7 @@
let
val req: request Single_Assignment.var = Single_Assignment.var "request";
fun abort () = ignore (cancel (Single_Assignment.await req));
- val promise: unit future = Future.promise abort;
+ val promise: unit future = Future.promise_name "event_timer" abort;
val _ = Single_Assignment.assign req (request time (Future.fulfill promise));
in promise end);
--- a/src/Pure/Concurrent/future.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/Pure/Concurrent/future.ML Fri Jun 23 15:01:06 2017 +0200
@@ -37,7 +37,7 @@
val value: 'a -> 'a future
val cond_forks: params -> (unit -> 'a) list -> 'a future list
val map: ('a -> 'b) -> 'a future -> 'b future
- val promise_group: group -> (unit -> unit) -> 'a future
+ val promise_name: string -> (unit -> unit) -> 'a future
val promise: (unit -> unit) -> 'a future
val fulfill_result: 'a future -> 'a Exn.result -> unit
val fulfill: 'a future -> 'a -> unit
@@ -599,8 +599,9 @@
(* promised futures -- fulfilled by external means *)
-fun promise_group group abort : 'a future =
+fun promise_name name abort : 'a future =
let
+ val group = worker_subgroup ();
val result = Single_Assignment.var "promise" : 'a result;
fun assign () = assign_result group result Exn.interrupt_exn
handle Fail _ => true
@@ -612,10 +613,10 @@
Thread_Attributes.with_attributes Thread_Attributes.no_interrupts
(fn _ => Exn.release (Exn.capture assign () before abort ()));
val task = SYNCHRONIZED "enqueue_passive" (fn () =>
- Unsynchronized.change_result queue (Task_Queue.enqueue_passive group job));
+ Unsynchronized.change_result queue (Task_Queue.enqueue_passive group name job));
in Future {promised = true, task = task, result = result} end;
-fun promise abort = promise_group (worker_subgroup ()) abort;
+fun promise abort = promise_name "passive" abort;
fun fulfill_result (Future {promised, task, result}) res =
if not promised then raise Fail "Not a promised future"
--- a/src/Pure/Concurrent/lazy.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/Pure/Concurrent/lazy.ML Fri Jun 23 15:01:06 2017 +0200
@@ -9,6 +9,7 @@
signature LAZY =
sig
type 'a lazy
+ val lazy_name: string -> (unit -> 'a) -> 'a lazy
val lazy: (unit -> 'a) -> 'a lazy
val value: 'a -> 'a lazy
val peek: 'a lazy -> 'a Exn.result option
@@ -16,6 +17,7 @@
val is_finished: 'a lazy -> bool
val force_result: 'a lazy -> 'a Exn.result
val force: 'a lazy -> 'a
+ val force_list: 'a lazy list -> 'a list
val map: ('a -> 'b) -> 'a lazy -> 'b lazy
val future: Future.params -> 'a lazy -> 'a future
end;
@@ -26,13 +28,14 @@
(* datatype *)
datatype 'a expr =
- Expr of unit -> 'a |
+ Expr of string * (unit -> 'a) |
Result of 'a future;
abstype 'a lazy = Lazy of 'a expr Synchronized.var
with
-fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
+fun lazy_name name e = Lazy (Synchronized.var "lazy" (Expr (name, e)));
+fun lazy e = lazy_name "lazy" e;
fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
fun peek (Lazy var) =
@@ -40,6 +43,12 @@
Expr _ => NONE
| Result res => Future.peek res);
+fun pending (Lazy var) =
+ (case Synchronized.value var of
+ Expr _ => true
+ | Result _ => false);
+
+
(* status *)
@@ -65,13 +74,13 @@
let
val (expr, x) =
Synchronized.change_result var
- (fn Expr e =>
- let val x = Future.promise I
- in ((SOME e, x), Result x) end
+ (fn Expr (name, e) =>
+ let val x = Future.promise_name name I
+ in ((SOME (name, e), x), Result x) end
| Result x => ((NONE, x), Result x));
in
(case expr of
- SOME e =>
+ SOME (name, e) =>
let
val res0 = Exn.capture (restore_attributes e) ();
val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
@@ -80,7 +89,7 @@
interrupt, until there is a fresh start*)
val _ =
if Exn.is_interrupt_exn res then
- Synchronized.change var (fn _ => Expr e)
+ Synchronized.change var (fn _ => Expr (name, e))
else ();
in res end
| NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
@@ -89,8 +98,13 @@
end;
-fun force r = Exn.release (force_result r);
-fun map f x = lazy (fn () => f (force x));
+fun force x = Exn.release (force_result x);
+
+fun force_list xs =
+ (List.app (fn x => if pending x then ignore (force_result x) else ()) xs;
+ map force xs);
+
+fun map f x = lazy_name "Lazy.map" (fn () => f (force x));
(* future evaluation *)
--- a/src/Pure/Concurrent/task_queue.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Fri Jun 23 15:01:06 2017 +0200
@@ -37,7 +37,7 @@
val cancel_all: queue -> group list * Thread.thread list
val finish: task -> queue -> bool * queue
val enroll: Thread.thread -> string -> group -> queue -> task * queue
- val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
+ val enqueue_passive: group -> string -> (unit -> bool) -> queue -> task * queue
val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
val extend: task -> (bool -> bool) -> queue -> queue option
val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue
@@ -312,9 +312,9 @@
(* enqueue *)
-fun enqueue_passive group abort (Queue {groups, jobs, urgent}) =
+fun enqueue_passive group name abort (Queue {groups, jobs, urgent}) =
let
- val task = new_task group "passive" NONE;
+ val task = new_task group name NONE;
val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
val jobs' = jobs |> Task_Graph.new_node (task, Passive abort);
in (task, make_queue groups' jobs' urgent) end;
--- a/src/Pure/Isar/code.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/Pure/Isar/code.ML Fri Jun 23 15:01:06 2017 +0200
@@ -142,7 +142,7 @@
"\nof constant " ^ quote c ^
"\nis too specific compared to declared type\n" ^
string_of_typ thy ty_decl)
- end;
+ end;
fun check_const thy = check_unoverload thy o check_bare_const thy;
@@ -411,7 +411,7 @@
fun get_abstype_spec thy tyco = case get_type_entry thy tyco
of SOME (vs, Abstractor spec) => (vs, spec)
| _ => error ("Not an abstract type: " ^ tyco);
-
+
fun get_type_of_constr_or_abstr thy c =
case (body_type o const_typ thy) c
of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco
@@ -463,7 +463,7 @@
^ "\nof constant " ^ quote c
^ "\nis too specific compared to declared type\n"
^ string_of_typ thy ty_decl)
- end;
+ end;
fun check_eqn thy { allow_nonlinear, allow_consts, allow_pats } thm (lhs, rhs) =
let
@@ -760,7 +760,7 @@
fun nothing_cert ctxt c = Nothing (dummy_thm ctxt c);
fun cert_of_eqns ctxt c [] = Equations (dummy_thm ctxt c, [])
- | cert_of_eqns ctxt c raw_eqns =
+ | cert_of_eqns ctxt c raw_eqns =
let
val thy = Proof_Context.theory_of ctxt;
val eqns = burrow_fst (canonize_thms thy) raw_eqns;
@@ -1104,7 +1104,7 @@
let
val thm = Thm.close_derivation raw_thm;
val c = const_eqn thy thm;
- fun update_subsume verbose (thm, proper) eqns =
+ fun update_subsume verbose (thm, proper) eqns =
let
val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
@@ -1118,13 +1118,13 @@
else false
end;
fun drop (thm', proper') = if (proper orelse not proper')
- andalso matches_args (args_of thm') then
+ andalso matches_args (args_of thm') then
(if verbose then warning ("Code generator: dropping subsumed code equation\n" ^
Thm.string_of_thm_global thy thm') else (); true)
else false;
in (thm, proper) :: filter_out drop eqns end;
fun natural_order eqns =
- (eqns, Lazy.lazy (fn () => fold (update_subsume false) eqns []))
+ (eqns, Lazy.lazy_name "code" (fn () => fold (update_subsume false) eqns []))
fun add_eqn' true Unimplemented = Eqns_Default (natural_order [(thm, proper)])
| add_eqn' true (Eqns_Default (eqns, _)) = Eqns_Default (natural_order ((thm, proper) :: eqns))
(*this restores the natural order and drops syntactic redundancies*)
--- a/src/Pure/Isar/toplevel.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/Pure/Isar/toplevel.ML Fri Jun 23 15:01:06 2017 +0200
@@ -648,14 +648,10 @@
val get_result = Result.get o Proof.context_of;
val put_result = Proof.map_context o Result.put;
-fun timing_estimate include_head elem =
- let val trs = Thy_Syntax.flat_element elem |> not include_head ? tl
+fun timing_estimate elem =
+ let val trs = tl (Thy_Syntax.flat_element elem)
in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
-fun priority estimate =
- if estimate = Time.zeroTime then ~1
- else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
-
fun proof_future_enabled estimate st =
(case try proof_of st of
NONE => false
@@ -670,8 +666,7 @@
val st' =
if Goal.future_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then
(Execution.fork
- {name = "Toplevel.diag", pos = pos_of tr,
- pri = priority (timing_estimate true (Thy_Syntax.atom tr))}
+ {name = "Toplevel.diag", pos = pos_of tr, pri = ~1}
(fn () => command tr st); st)
else command tr st;
in (Result (tr, st'), st') end;
@@ -683,7 +678,7 @@
let
val (head_result, st') = atom_result keywords head_tr st;
val (body_elems, end_tr) = element_rest;
- val estimate = timing_estimate false elem;
+ val estimate = timing_estimate elem;
in
if not (proof_future_enabled estimate st')
then
@@ -698,7 +693,7 @@
val future_proof =
Proof.future_proof (fn state =>
Execution.fork
- {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = priority estimate}
+ {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = ~1}
(fn () =>
let
val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
--- a/src/Pure/PIDE/active.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/Pure/PIDE/active.ML Fri Jun 23 15:01:06 2017 +0200
@@ -49,7 +49,7 @@
let
val i = serial ();
fun abort () = Synchronized.change dialogs (Inttab.delete_safe i);
- val promise = Future.promise abort : string future;
+ val promise = Future.promise_name "dialog" abort : string future;
val _ = Synchronized.change dialogs (Inttab.update_new (i, promise));
fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
in (result_markup, promise) end;
--- a/src/Pure/PIDE/command.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/Pure/PIDE/command.ML Fri Jun 23 15:01:06 2017 +0200
@@ -264,7 +264,7 @@
(fn () =>
read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) ();
in eval_state keywords span tr eval_state0 end;
- in Eval {exec_id = exec_id, eval_process = Lazy.lazy process} end;
+ in Eval {exec_id = exec_id, eval_process = Lazy.lazy_name "Command.eval" process} end;
end;
@@ -322,7 +322,7 @@
in
Print {
name = name, args = args, delay = delay, pri = pri, persistent = persistent,
- exec_id = exec_id, print_process = Lazy.lazy process}
+ exec_id = exec_id, print_process = Lazy.lazy_name "Command.print" process}
end;
fun bad_print name args exn =
--- a/src/Pure/PIDE/document.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/Pure/PIDE/document.ML Fri Jun 23 15:01:06 2017 +0200
@@ -371,7 +371,7 @@
let
val id = Document_ID.print command_id;
val span =
- Lazy.lazy (fn () =>
+ Lazy.lazy_name "Document.define_command" (fn () =>
Position.setmp_thread_data (Position.id_only id)
(fn () =>
let
--- a/src/Pure/Syntax/syntax.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/Pure/Syntax/syntax.ML Fri Jun 23 15:01:06 2017 +0200
@@ -540,7 +540,7 @@
else
let
val input' = new_xprods2 @ input1;
- val gram' = Lazy.lazy (fn () => Parser.make_gram input');
+ val gram' = Lazy.lazy_name "Syntax.merge_syntax" (fn () => Parser.make_gram input');
in (input', gram') end);
in
Syntax
--- a/src/Pure/System/invoke_scala.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/Pure/System/invoke_scala.ML Fri Jun 23 15:01:06 2017 +0200
@@ -31,7 +31,7 @@
let
val id = new_id ();
fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
- val promise = Future.promise abort : string future;
+ val promise = Future.promise_name "invoke_scala" abort : string future;
val _ = Synchronized.change promises (Symtab.update (id, promise));
val _ = Output.protocol_message (Markup.invoke_scala name id) [arg];
in promise end;
--- a/src/Pure/more_thm.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/Pure/more_thm.ML Fri Jun 23 15:01:06 2017 +0200
@@ -645,7 +645,7 @@
Proofs.map (fold (cons o Thm.trim_context) more_thms);
fun consolidate_theory thy =
- List.app (Thm.consolidate o Thm.transfer thy) (rev (Proofs.get thy));
+ Thm.consolidate (map (Thm.transfer thy) (rev (Proofs.get thy)));
--- a/src/Pure/proofterm.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/Pure/proofterm.ML Fri Jun 23 15:01:06 2017 +0200
@@ -43,7 +43,7 @@
val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
val fold_body_thms: ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
proof_body list -> 'a -> 'a
- val consolidate: proof_body -> unit
+ val consolidate: proof_body list -> unit
val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
val oracle_ord: oracle * oracle -> order
@@ -197,15 +197,16 @@
fun join_thms (thms: pthm list) =
Future.joins (map (thm_node_body o #2) thms);
-fun consolidate (PBody {thms, ...}) =
- List.app (Lazy.force o thm_node_consolidate o #2) thms;
+val consolidate =
+ maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
+ #> Lazy.force_list #> ignore;
fun make_thm_node name prop body =
Thm_Node {name = name, prop = prop, body = body,
consolidate =
- Lazy.lazy (fn () =>
+ Lazy.lazy_name "Proofterm.make_thm_node" (fn () =>
let val PBody {thms, ...} = Future.join body
- in List.app consolidate (join_thms thms) end)};
+ in consolidate (join_thms thms) end)};
(***** proof atoms *****)
@@ -1530,8 +1531,7 @@
fun fulfill_norm_proof thy ps body0 =
let
- val _ = List.app (consolidate o #2) ps;
- val _ = consolidate body0;
+ val _ = consolidate (map #2 ps @ [body0]);
val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
val oracles =
unions_oracles
--- a/src/Pure/thm.ML Fri Jun 23 13:16:04 2017 +0200
+++ b/src/Pure/thm.ML Fri Jun 23 15:01:06 2017 +0200
@@ -86,7 +86,7 @@
val proof_bodies_of: thm list -> proof_body list
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
- val consolidate: thm -> unit
+ val consolidate: thm list -> unit
val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool}
val future: thm future -> cterm -> thm
val derivation_closed: thm -> bool
@@ -598,7 +598,7 @@
val proof_body_of = singleton proof_bodies_of;
val proof_of = Proofterm.proof_of o proof_body_of;
-val consolidate = ignore o proof_bodies_of o single;
+val consolidate = ignore o proof_bodies_of;
(* derivation status *)