# HG changeset patch # User eberlm # Date 1498222866 -7200 # Node ID df70049d584dc6ddbf9c04d8626e7d2ea3987e68 # Parent 454abfe923fed6e1c09214e4aa73fb6546b025e1# Parent cad55bc7e37ddcaec63d5a75ef6edbc4a055ac93 Merged diff -r 454abfe923fe -r df70049d584d src/HOL/Analysis/Borel_Space.thy --- 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 "(\x. f x *\<^sub>R g x) \ borel_measurable M" using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) +lemma borel_measurable_uminus_eq [simp]: + fixes f :: "'a \ 'b::{second_countable_topology, real_normed_vector}" + shows "(\x. - f x) \ borel_measurable M \ f \ 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 \ 'x::real_normed_vector" assumes "f \ borel_measurable M" diff -r 454abfe923fe -r df70049d584d src/HOL/Analysis/Cauchy_Integral_Theorem.thy --- 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 \ f integrable_on s \ integral s f = i" - by blast - lemma has_integral_contour_integral_subpath: assumes "f contour_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "u \ v" shows "(((\x. f(g x) * vector_derivative g (at x))) diff -r 454abfe923fe -r df70049d584d src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- 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 \ set_integrable lebesgue s f" + lemma absolutely_integrable_on_def: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" shows "f absolutely_integrable_on s \ f integrable_on s \ (\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 \ 'b::euclidean_space" + shows "content (cbox a b) = 0 \ 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 \ 'b :: euclidean_space" + shows "f absolutely_integrable_on box a b \ + f absolutely_integrable_on cbox a b" + by (auto simp: integrable_on_open_interval absolutely_integrable_on_def) lemma absolutely_integrable_restrict_UNIV: "(\x. if x \ s then f x else 0) absolutely_integrable_on UNIV \ f absolutely_integrable_on s" @@ -2075,7 +2087,7 @@ assumes "f integrable_on UNIV" and "\d. d division_of (\d) \ sum (\k. norm (integral k f)) d \ B" shows "f absolutely_integrable_on UNIV" -proof (rule absolutely_integrable_onI, fact, rule) +proof (rule absolutely_integrable_onI, fact) let ?f = "\d. \k\d. norm (integral k f)" and ?D = "{d. d division_of (\d)}" have D_1: "?D \ {}" by (rule elementary_interval) auto @@ -2091,7 +2103,7 @@ apply (rule assms(2)[rule_format]) apply auto done - show "((\x. norm (f x)) has_integral ?S) UNIV" + have "((\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 "(\x. norm (f x)) integrable_on UNIV" + by blast qed lemma absolutely_integrable_add[intro]: diff -r 454abfe923fe -r df70049d584d src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- 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 \ ~ f integrable_on i \ y=0)" -lemma integrable_integral[dest]: "f integrable_on i \ (f has_integral (integral i f)) i" +lemma integrable_integral[intro]: "f integrable_on i \ (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 \ integral i f = 0" unfolding integrable_on_def integral_def by blast -lemma has_integral_integrable[intro]: "(f has_integral i) s \ f integrable_on s" +lemma has_integral_integrable[dest]: "(f has_integral i) s \ f integrable_on s" unfolding integrable_on_def by auto lemma has_integral_integral: "f integrable_on s \ (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 "((\x. c) has_integral (content (cbox a b) *\<^sub>R c)) (cbox a b)" @@ -372,6 +371,9 @@ shows "((\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 \ f integrable_on s \ integral s f = i" + by blast + lemma integral_const [simp]: fixes a b :: "'a::euclidean_space" shows "integral (cbox a b) (\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]: "((\x::'n::euclidean_space. 0) has_integral 0) s" +lemma has_integral_0[simp]: "((\x::'n::euclidean_space. 0) has_integral 0) S" by (rule has_integral_is_0) auto -lemma has_integral_0_eq[simp]: "((\x. 0) has_integral i) s \ i = 0" +lemma has_integral_0_eq[simp]: "((\x. 0) has_integral i) S \ i = 0" using has_integral_unique[OF has_integral_0] by auto lemma has_integral_linear: fixes f :: "'n::euclidean_space \ 'a::real_normed_vector" - assumes "(f has_integral y) s" + assumes "(f has_integral y) S" and "bounded_linear h" - shows "((h \ f) has_integral ((h y))) s" + shows "((h \ f) has_integral ((h y))) S" proof - interpret bounded_linear h using assms(2) . @@ -427,11 +429,11 @@ have lem: "\a b y f::'n\'a. (f has_integral y) (cbox a b) \ ((h \ f) has_integral h y) (cbox a b)" unfolding has_integral_cbox by (drule tendsto) (simp add: sum scaleR split_beta') { - presume "\ (\a b. s = cbox a b) \ ?thesis" + presume "\ (\a b. S = cbox a b) \ ?thesis" then show ?thesis using assms(1) lem by blast } - assume as: "\ (\a b. s = cbox a b)" + assume as: "\ (\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" "\a b. ball 0 M \ cbox a b \ - \z. ((\x. if x \ s then f x else 0) has_integral z) (cbox a b) \ norm (z - y) < e / B" + \z. ((\x. if x \ S then f x else 0) has_integral z) (cbox a b) \ norm (z - y) < e / B" using has_integral_altD[OF assms(1) as *] by blast show "\B>0. \a b. ball 0 B \ cbox a b \ - (\z. ((\x. if x \ s then (h \ f) x else 0) has_integral z) (cbox a b) \ norm (z - h y) < e)" + (\z. ((\x. if x \ S then (h \ f) x else 0) has_integral z) (cbox a b) \ 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: - "((\x. if x \ s then f x else 0) has_integral z) (cbox a b)" + "((\x. if x \ 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 *: "(\x. if x \ s then (h \ f) x else 0) = h \ (\x. if x \ s then f x else 0)" + have *: "(\x. if x \ S then (h \ f) x else 0) = h \ (\x. if x \ 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 \ ((\x. f x *\<^sub>R c) has_integral (y *\<^sub>R c)) s" + "(f has_integral y) S \ ((\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 \ ((\x. f x * c) has_integral (y * c)) s" + shows "(f has_integral y) S \ ((\x. f x * c) has_integral (y * c)) S" using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def) -text\The case analysis eliminates the condition @{term "f integrable_on s"} at the cost +text\The case analysis eliminates the condition @{term "f integrable_on S"} at the cost of the type class constraint \division_ring\\ corollary integral_mult_left [simp]: fixes c:: "'a::{real_normed_algebra,division_ring}" - shows "integral s (\x. f x * c) = integral s f * c" -proof (cases "f integrable_on s \ c = 0") + shows "integral S (\x. f x * c) = integral S f * c" +proof (cases "f integrable_on S \ c = 0") case True then show ?thesis by (force intro: has_integral_mult_left) next - case False then have "~ (\x. f x * c) integrable_on s" - using has_integral_mult_left [of "(\x. f x * c)" _ s "inverse c"] - by (force simp add: mult.assoc) + case False then have "~ (\x. f x * c) integrable_on S" + using has_integral_mult_left [of "(\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 (\x. c * f x) = c * integral s f" + shows "integral S (\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 \ ((\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 \ ((\x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s" +lemma has_integral_cmul: "(f has_integral k) S \ ((\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 \ ((\x. -(f x)) has_integral -k) s" +lemma has_integral_neg: "(f has_integral k) S \ ((\x. -(f x)) has_integral -k) S" by (drule_tac c="-1" in has_integral_cmul) auto -lemma has_integral_neg_iff: "((\x. - f x) has_integral k) s \ (f has_integral - k) s" +lemma has_integral_neg_iff: "((\x. - f x) has_integral k) S \ (f has_integral - k) S" using has_integral_neg[of f "- k"] has_integral_neg[of "\x. - f x" k] by auto lemma has_integral_add: fixes f :: "'n::euclidean_space \ 'a::real_normed_vector" - assumes "(f has_integral k) s" - and "(g has_integral l) s" - shows "((\x. f x + g x) has_integral (k + l)) s" + assumes "(f has_integral k) S" + and "(g has_integral l) S" + shows "((\x. f x + g x) has_integral (k + l)) S" proof - have lem: "(f has_integral k) (cbox a b) \ (g has_integral l) (cbox a b) \ ((\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 "\ (\a b. s = cbox a b) \ ?thesis" + presume "\ (\a b. S = cbox a b) \ ?thesis" then show ?thesis using assms lem by force } - assume as: "\ (\a b. s = cbox a b)" + assume as: "\ (\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" "\a b. ball 0 B1 \ cbox a b \ - \z. ((\x. if x \ s then f x else 0) has_integral z) (cbox a b) \ norm (z - k) < e / 2" + \z. ((\x. if x \ S then f x else 0) has_integral z) (cbox a b) \ norm (z - k) < e / 2" by blast from has_integral_altD[OF assms(2) as *] obtain B2 where B2: "0 < B2" "\a b. ball 0 B2 \ (cbox a b) \ - \z. ((\x. if x \ s then g x else 0) has_integral z) (cbox a b) \ norm (z - l) < e / 2" + \z. ((\x. if x \ S then g x else 0) has_integral z) (cbox a b) \ 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 \ cbox a (b::'n)" "ball 0 B2 \ cbox a (b::'n)" by auto obtain w where w: - "((\x. if x \ s then f x else 0) has_integral w) (cbox a b)" + "((\x. if x \ 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: - "((\x. if x \ s then g x else 0) has_integral z) (cbox a b)" + "((\x. if x \ 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 *: "\x. (if x \ s then f x + g x else 0) = - (if x \ s then f x else 0) + (if x \ s then g x else 0)" + have *: "\x. (if x \ S then f x + g x else 0) = + (if x \ S then f x else 0) + (if x \ S then g x else 0)" by auto - show "\z. ((\x. if x \ s then f x + g x else 0) has_integral z) (cbox a b) \ norm (z - (k + l)) < e" + show "\z. ((\x. if x \ S then f x + g x else 0) has_integral z) (cbox a b) \ 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 \ (g has_integral l) s \ - ((\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 \ (g has_integral l) S \ + ((\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 (\x::'n::euclidean_space. 0::'m::real_normed_vector) = 0" + "integral S (\x::'n::euclidean_space. 0::'m::real_normed_vector) = 0" by (rule integral_unique has_integral_0)+ -lemma integral_add: "f integrable_on s \ g integrable_on s \ - integral s (\x. f x + g x) = integral s f + integral s g" +lemma integral_add: "f integrable_on S \ g integrable_on S \ + integral S (\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 (\x. c *\<^sub>R f x) = c *\<^sub>R integral s f" -proof (cases "f integrable_on s \ c = 0") - case True with has_integral_cmul show ?thesis by force +lemma integral_cmul [simp]: "integral S (\x. c *\<^sub>R f x) = c *\<^sub>R integral S f" +proof (cases "f integrable_on S \ c = 0") + case True with has_integral_cmul integrable_integral show ?thesis + by fastforce next - case False then have "~ (\x. c *\<^sub>R f x) integrable_on s" - using has_integral_cmul [of "(\x. c *\<^sub>R f x)" _ s "inverse c"] - by force + case False then have "~ (\x. c *\<^sub>R f x) integrable_on S" + using has_integral_cmul [of "(\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 (\x. - f x) = - integral s f" -proof (cases "f integrable_on s") +lemma integral_neg [simp]: "integral S (\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 "~ (\x. - f x) integrable_on s" - using has_integral_neg [of "(\x. - f x)" _ s ] - by force + case False then have "~ (\x. - f x) integrable_on S" + using has_integral_neg [of "(\x. - f x)" _ S ] by auto with False show ?thesis by (simp add: not_integrable_integral) qed -lemma integral_diff: "f integrable_on s \ g integrable_on s \ - integral s (\x. f x - g x) = integral s f - integral s g" +lemma integral_diff: "f integrable_on S \ g integrable_on S \ + integral S (\x. f x - g x) = integral S f - integral S g" by (rule integral_unique) (metis integrable_integral has_integral_diff) -lemma integrable_0: "(\x. 0) integrable_on s" +lemma integrable_0: "(\x. 0) integrable_on S" unfolding integrable_on_def using has_integral_0 by auto -lemma integrable_add: "f integrable_on s \ g integrable_on s \ (\x. f x + g x) integrable_on s" +lemma integrable_add: "f integrable_on S \ g integrable_on S \ (\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 \ (\x. c *\<^sub>R f(x)) integrable_on s" +lemma integrable_cmul: "f integrable_on S \ (\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 \ 0" - shows "(\x. c * f x) integrable_on s \ f integrable_on s" - using integrable_cmul[of "\x. c * f x" s "1 / c"] integrable_cmul[of f s c] \c \ 0\ + shows "(\x. c * f x) integrable_on S \ f integrable_on S" + using integrable_cmul[of "\x. c * f x" S "1 / c"] integrable_cmul[of f S c] \c \ 0\ by auto lemma integrable_on_cmult_left: - assumes "f integrable_on s" - shows "(\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 "(\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 \ (\x. -f(x)) integrable_on s" +lemma integrable_neg: "f integrable_on S \ (\x. -f(x)) integrable_on S" unfolding integrable_on_def by(auto intro: has_integral_neg) lemma integrable_diff: - "f integrable_on s \ g integrable_on s \ (\x. f x - g x) integrable_on s" + "f integrable_on S \ g integrable_on S \ (\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 \ bounded_linear h \ (h \ f) integrable_on s" + "f integrable_on S \ bounded_linear h \ (h \ f) integrable_on S" unfolding integrable_on_def by(auto intro: has_integral_linear) lemma integral_linear: - "f integrable_on s \ bounded_linear h \ integral s (h \ f) = h (integral s f)" - apply (rule has_integral_unique [where i=s and f = "h \ f"]) + "f integrable_on S \ bounded_linear h \ integral S (h \ f) = h (integral S f)" + apply (rule has_integral_unique [where i=S and f = "h \ f"]) apply (simp_all add: integrable_integral integrable_linear has_integral_linear ) done lemma integral_component_eq[simp]: fixes f :: "'n::euclidean_space \ 'm::euclidean_space" - assumes "f integrable_on s" - shows "integral s (\x. f x \ k) = integral s f \ k" + assumes "f integrable_on S" + shows "integral S (\x. f x \ k) = integral S f \ k" unfolding integral_linear[OF assms(1) bounded_linear_inner_left,unfolded o_def] .. lemma has_integral_sum: assumes "finite t" - and "\a\t. ((f a) has_integral (i a)) s" - shows "((\x. sum (\a. f a x) t) has_integral (sum i t)) s" + and "\a\t. ((f a) has_integral (i a)) S" + shows "((\x. sum (\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: - "\finite t; \a\t. (f a) integrable_on s\ \ - integral s (\x. sum (\a. f a x) t) = sum (\a. integral s (f a)) t" - by (auto intro: has_integral_sum integrable_integral) + "\finite I; \a. a \ I \ f a integrable_on S\ \ + integral S (\x. \a\I. f a x) = (\a\I. integral S (f a))" + by (simp add: has_integral_sum integrable_integral integral_unique) lemma integrable_sum: "\finite I; \a. a \ I \ f a integrable_on S\ \ (\x. \a\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 "\n. gauge (\x. \{d i x |i. i \ {0..n}})" - apply (rule gauge_inters) + apply (rule gauge_Inter) using d(1) apply auto done @@ -993,33 +994,33 @@ subsection \Additivity of integral on abutting intervals.\ lemma tagged_division_split_left_inj_content: - assumes d: "d tagged_division_of i" - and "(x1, k1) \ d" "(x2, k2) \ d" "k1 \ k2" "k1 \ {x. x\k \ c} = k2 \ {x. x\k \ c}" "k \ Basis" - shows "content (k1 \ {x. x\k \ c}) = 0" + assumes \: "\ tagged_division_of S" + and "(x1, K1) \ \" "(x2, K2) \ \" "K1 \ K2" "K1 \ {x. x\k \ c} = K2 \ {x. x\k \ c}" "k \ Basis" + shows "content (K1 \ {x. x\k \ c}) = 0" proof - - from tagged_division_ofD(4)[OF d \(x1, k1) \ d\] obtain a b where k1: "k1 = cbox a b" + from tagged_division_ofD(4)[OF \ \(x1, K1) \ \\] obtain a b where K1: "K1 = cbox a b" by auto - show ?thesis - unfolding k1 interval_split[OF \k \ Basis\] - unfolding content_eq_0_interior - unfolding interval_split[OF \k \ Basis\, symmetric] k1[symmetric] + then have "interior (K1 \ {x. x \ k \ c}) = {}" by (metis tagged_division_split_left_inj assms) + then show ?thesis + unfolding K1 interval_split[OF \k \ Basis\] 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) \ d" "(x2, k2) \ d" "k1 \ k2" "k1 \ {x. x\k \ c} = k2 \ {x. x\k \ c}" "k \ Basis" - shows "content (k1 \ {x. x\k \ c}) = 0" + assumes \: "\ tagged_division_of S" + and "(x1, K1) \ \" "(x2, K2) \ \" "K1 \ K2" "K1 \ {x. x\k \ c} = K2 \ {x. x\k \ c}" "k \ Basis" + shows "content (K1 \ {x. x\k \ c}) = 0" proof - - from tagged_division_ofD(4)[OF d \(x1, k1) \ d\] obtain a b where k1: "k1 = cbox a b" + from tagged_division_ofD(4)[OF \ \(x1, K1) \ \\] obtain a b where K1: "K1 = cbox a b" by auto - show ?thesis - unfolding k1 interval_split[OF \k \ Basis\] - unfolding content_eq_0_interior - unfolding interval_split[OF \k \ Basis\, symmetric] k1[symmetric] + then have "interior (K1 \ {x. c \ x \ k}) = {}" by (metis tagged_division_split_right_inj assms) + then show ?thesis + unfolding K1 interval_split[OF \k \ Basis\] + by (auto simp: content_eq_0_interior) qed + lemma has_integral_split: fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" assumes fi: "(f has_integral i) (cbox a b \ {x. x\k \ c})" @@ -1313,7 +1314,7 @@ fixes f :: "'a::euclidean_space \ 'b::{real_normed_vector,complete_space}" assumes f: "f integrable_on cbox a b" and k: "k \ Basis" - shows "f integrable_on (cbox a b \ {x. x\k \ c})" (is ?thesis1) + shows "f integrable_on (cbox a b \ {x. x\k \ c})" (is ?thesis1) and "f integrable_on (cbox a b \ {x. x\k \ 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: "\p1 p2. \p1 tagged_division_of cbox a b \ {x. x \ k \ c}; d fine p1; - p2 tagged_division_of cbox a b \ {x. c \ x \ k}; d fine p2\ - \ norm ((\(x,K)\p1. content K *\<^sub>R f x) + (\(x,K)\p2. content K *\<^sub>R f x) - y) < e/2" + and d: "\p1 p2. \p1 tagged_division_of cbox a b \ {x. x \ k \ c}; d fine p1; + p2 tagged_division_of cbox a b \ {x. c \ x \ k}; d fine p2\ + \ norm ((\(x,K)\p1. content K *\<^sub>R f x) + (\(x,K)\p2. content K *\<^sub>R f x) - y) < e/2" by metis show ?thesis proof (rule_tac x=d in exI, clarsimp simp add: \gauge d\) @@ -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 "\d. gauge d \ @@ -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: "\p1 p2. \p1 tagged_division_of cbox a b \ {x. x \ k \ c}; d fine p1; - p2 tagged_division_of cbox a b \ {x. c \ x \ k}; d fine p2\ - \ norm ((\(x,K)\p1. content K *\<^sub>R f x) + (\(x,K)\p2. content K *\<^sub>R f x) - y) < e/2" + and d: "\p1 p2. \p1 tagged_division_of cbox a b \ {x. x \ k \ c}; d fine p1; + p2 tagged_division_of cbox a b \ {x. c \ x \ k}; d fine p2\ + \ norm ((\(x,K)\p1. content K *\<^sub>R f x) + (\(x,K)\p2. content K *\<^sub>R f x) - y) < e/2" by metis show ?thesis proof (rule_tac x=d in exI, clarsimp simp add: \gauge d\) @@ -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="\x. if x\T then f x else 0" and g="\x. if x \ T then g x else 0"])+ + apply (simp split: if_split_asm) + apply (blast dest: *) + apply (erule_tac V = "\a b. T \ 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="\x. if x\T then f x else 0" and g="\x. if x \ T then g x else 0"]) done qed @@ -2764,7 +2766,7 @@ fixes a::real assumes "a \ b" shows "integral {a..b} (\x. x) = (if a \ 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 = (\iR 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 \Reduce integrability to "local" integrability.\ @@ -3181,7 +3184,7 @@ using False x by (simp add: algebra_simps integral_combine) have fux_int: "((\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: "((\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 \Hence a general restriction property.\ -lemma has_integral_restrict[simp]: - assumes "s \ t" - shows "((\x. if x \ s then f x else (0::'a::banach)) has_integral i) t \ (f has_integral i) s" +lemma has_integral_restrict [simp]: + fixes f :: "'a :: euclidean_space \ 'b :: banach" + assumes "S \ T" + shows "((\x. if x \ S then f x else 0) has_integral i) T \ (f has_integral i) S" proof - - have *: "\x. (if x \ t then if x \ s then f x else 0 else 0) = (if x\s then f x else 0)" + have *: "\x. (if x \ T then if x \ S then f x else 0 else 0) = (if x\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 \ 'a::banach" shows "((\x. if x \ s then f x else 0) has_integral i) UNIV \ (f has_integral i) s" by auto +lemma has_integral_restrict_Int: + fixes f :: "'a :: euclidean_space \ 'b :: banach" + shows "((\x. if x \ S then f x else 0) has_integral i) T \ (f has_integral i) (S \ T)" +proof - + have "((\x. if x \ T then if x \ S then f x else 0 else 0) has_integral i) UNIV = + ((\x. if x \ S \ 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 \ 'b :: banach" + shows "integral T (\x. if x \ S then f x else 0) = integral (S \ 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 \ 'b :: banach" + shows "(\x. if x \ S then f x else 0) integrable_on T \ f integrable_on (S \ T)" + using has_integral_restrict_Int by fastforce + lemma has_integral_on_superset: fixes f :: "'n::euclidean_space \ 'a::banach" - assumes "\x. x \ s \ f x = 0" - and "s \ t" - and "(f has_integral i) s" - shows "(f has_integral i) t" + assumes f: "(f has_integral i) S" + and "\x. x \ S \ f x = 0" + and "S \ T" + shows "(f has_integral i) T" proof - - have "(\x. if x \ s then f x else 0) = (\x. if x \ 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 "(\x. if x \ S then f x else 0) = (\x. if x \ 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 \ 'a::banach" shows "f integrable_on s \ integral UNIV (\x. if x \ 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 \ 'm::euclidean_space" + assumes k: "k \ Basis" + and as: "S \ T" "(f has_integral i) S" "(f has_integral j) T" "\x. x\T \ 0 \ f(x)\k" + shows "i\k \ j\k" +proof - + have "((\x. if x \ S then f x else 0) has_integral i) UNIV" + "((\x. if x \ 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 \ (\a b. negligible(s \ cbox a b))" (is "?l \ ?r") proof assume ?r @@ -5193,48 +5224,65 @@ lemma has_integral_spike_set_eq: fixes f :: "'n::euclidean_space \ 'a::banach" - assumes "negligible ((s - t) \ (t - s))" - shows "(f has_integral y) s \ (f has_integral y) t" + assumes "negligible ((S - T) \ (T - S))" + shows "(f has_integral y) S \ (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 \ 'a::banach" - assumes "(f has_integral y) s" "negligible ((s - t) \ (t - s))" - shows "(f has_integral y) t" + assumes "(f has_integral y) S" "negligible ((S - T) \ (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 \ 'a::banach" - assumes "f integrable_on s" and "negligible ((s - t) \ (t - s))" - shows "f integrable_on t" + assumes "f integrable_on S" and "negligible ((S - T) \ (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 \ 'a::banach" - assumes "negligible ((s - t) \ (t - s))" - shows "f integrable_on s \ f integrable_on t" -by (blast intro: integrable_spike_set assms negligible_subset) + assumes "negligible ((S - T) \ (T - S))" + shows "f integrable_on S \ f integrable_on T" + by (blast intro: integrable_spike_set assms negligible_subset) + +lemma has_integral_interior: + fixes f :: "'a :: euclidean_space \ 'b :: banach" + shows "negligible(frontier S) \ (f has_integral y) (interior S) \ (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 \ 'b :: banach" + shows "negligible(frontier S) \ (f has_integral y) (closure S) \ (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 \ 'b :: banach" + shows "(f has_integral y) (box a b) \ (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 \ 'b :: banach" + shows "f integrable_on box a b \ 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 \ '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 \More lemmas that are useful later\ -lemma has_integral_subset_component_le: - fixes f :: "'n::euclidean_space \ 'm::euclidean_space" - assumes k: "k \ Basis" - and as: "s \ t" "(f has_integral i) s" "(f has_integral j) t" "\x\t. 0 \ f(x)\k" - shows "i\k \ j\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 \ real" assumes "s \ t" @@ -5504,10 +5552,10 @@ have e: "e/3 > 0" using that by auto then obtain g h i j where ij: "\i - j\ < 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: "\x. x \ cbox a b \ g x \ f x \ f x \ 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: "\p. \p tagged_division_of cbox a b; d1 fine p\ \ \(\(x,K)\p. content K *\<^sub>R g x) - i\ < e/3" @@ -5515,10 +5563,10 @@ \(\(x,K) \ p. content K *\<^sub>R h x) - j\ < e/3" by (metis e has_integral real_norm_def) have "\(\(x,K) \ p1. content K *\<^sub>R f x) - (\(x,K) \ p2. content K *\<^sub>R f x)\ < 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 *: "\g1 g2 h1 h2 f1 f2. + have *: "\g1 g2 h1 h2 f1 f2. \\g2 - i\ < e/3; \g1 - i\ < e/3; \h2 - j\ < e/3; \h1 - j\ < e/3; g1 - h2 \ f1 - f2; f1 - f2 \ h1 - g2\ \ \f1 - f2\ < 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 _ \x \ x'\]) (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 \ a then F n - F a else 0)" for n :: nat proof (cases "n \ 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 diff -r 454abfe923fe -r df70049d584d src/HOL/Analysis/Interval_Integral.thy --- 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: "(\i. LBINT x=l i..u i. f x) \ B - A" apply (subst FTCi) diff -r 454abfe923fe -r df70049d584d src/HOL/Analysis/Lebesgue_Measure.thy --- 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 \ 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 \ sets lebesgue \ A \ 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 \ fmeasurable lborel" + and fmeasurable_box [iff]: "box a b \ fmeasurable lborel" + by (auto simp: fmeasurable_def emeasure_lborel_box_eq emeasure_lborel_cbox_eq) lemma fixes l u :: real diff -r 454abfe923fe -r df70049d584d src/HOL/Analysis/Set_Integral.thy --- 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 (\x. f)" -lemma set_borel_measurable_continuous: - fixes f :: "_ \ _::real_normed_vector" - assumes "S \ sets borel" "continuous_on S f" - shows "set_borel_measurable borel S f" -proof - - have "(\x. if x \ S then f x else 0) \ borel_measurable borel" - by (intro assms borel_measurable_continuous_on_if continuous_on_const) - also have "(\x. if x \ S then f x else 0) = (\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 \ 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\This notation is from Sébastien Gouëzel: His use is not directly in line with the diff -r 454abfe923fe -r df70049d584d src/HOL/Analysis/Tagged_Division.thy --- 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 \ gauge d2 \ gauge (\x. d1 x \ d2 x)" unfolding gauge_def by auto -lemma gauge_inters: +lemma gauge_reflect: + fixes \ :: "'a::euclidean_space \ 'a set" + shows "gauge \ \ gauge (\x. uminus ` \ (- 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 "\d\s. gauge (f d)" + and "\d. d\s \ gauge (f d)" shows "gauge (\x. \{f d x | d. d \ s})" proof - have *: "\x. {f d x |d. d \ s} = (\d. f d x) ` s" diff -r 454abfe923fe -r df70049d584d src/HOL/Analysis/Topology_Euclidean_Space.thy --- 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 \ 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 \ '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 \ '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 \Also bilinear functions, in composition form.\ diff -r 454abfe923fe -r df70049d584d src/HOL/Nunchaku/Nunchaku.thy --- 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 diff -r 454abfe923fe -r df70049d584d src/HOL/Nunchaku/Tools/nunchaku.ML --- 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 diff -r 454abfe923fe -r df70049d584d src/HOL/Nunchaku/Tools/nunchaku_commands.ML --- 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 = diff -r 454abfe923fe -r df70049d584d src/HOL/Nunchaku/Tools/nunchaku_tool.ML --- 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; diff -r 454abfe923fe -r df70049d584d src/HOL/SPARK/Tools/spark_vcs.ML --- 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; diff -r 454abfe923fe -r df70049d584d src/Pure/Concurrent/cache.ML --- 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; diff -r 454abfe923fe -r df70049d584d src/Pure/Concurrent/event_timer.ML --- 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); diff -r 454abfe923fe -r df70049d584d src/Pure/Concurrent/future.ML --- 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" diff -r 454abfe923fe -r df70049d584d src/Pure/Concurrent/lazy.ML --- 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 *) diff -r 454abfe923fe -r df70049d584d src/Pure/Concurrent/task_queue.ML --- 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; diff -r 454abfe923fe -r df70049d584d src/Pure/Isar/code.ML --- 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*) diff -r 454abfe923fe -r df70049d584d src/Pure/Isar/toplevel.ML --- 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'; diff -r 454abfe923fe -r df70049d584d src/Pure/PIDE/active.ML --- 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; diff -r 454abfe923fe -r df70049d584d src/Pure/PIDE/command.ML --- 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 = diff -r 454abfe923fe -r df70049d584d src/Pure/PIDE/document.ML --- 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 diff -r 454abfe923fe -r df70049d584d src/Pure/Syntax/syntax.ML --- 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 diff -r 454abfe923fe -r df70049d584d src/Pure/System/invoke_scala.ML --- 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; diff -r 454abfe923fe -r df70049d584d src/Pure/more_thm.ML --- 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))); diff -r 454abfe923fe -r df70049d584d src/Pure/proofterm.ML --- 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 diff -r 454abfe923fe -r df70049d584d src/Pure/thm.ML --- 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 *)