--- a/src/HOL/Analysis/Borel_Space.thy Thu Jun 22 21:44:15 2017 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy Thu Jun 22 21:48:57 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 Thu Jun 22 21:44:15 2017 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Jun 22 21:48:57 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 Thu Jun 22 21:44:15 2017 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Jun 22 21:48:57 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 Thu Jun 22 21:44:15 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Jun 22 21:48:57 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 Thu Jun 22 21:44:15 2017 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Thu Jun 22 21:48:57 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 Thu Jun 22 21:44:15 2017 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Thu Jun 22 21:48:57 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 Thu Jun 22 21:44:15 2017 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy Thu Jun 22 21:48:57 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 Thu Jun 22 21:44:15 2017 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy Thu Jun 22 21:48:57 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 Thu Jun 22 21:44:15 2017 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Jun 22 21:48:57 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/Filter.thy Thu Jun 22 21:44:15 2017 +0200
+++ b/src/HOL/Filter.thy Thu Jun 22 21:48:57 2017 +0200
@@ -556,6 +556,116 @@
by (subst (1 2) eventually_INF) auto
qed
+
+subsubsection \<open>Contravariant map function for filters\<close>
+
+definition filtercomap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter" where
+ "filtercomap f F = Abs_filter (\<lambda>P. \<exists>Q. eventually Q F \<and> (\<forall>x. Q (f x) \<longrightarrow> P x))"
+
+lemma eventually_filtercomap:
+ "eventually P (filtercomap f F) \<longleftrightarrow> (\<exists>Q. eventually Q F \<and> (\<forall>x. Q (f x) \<longrightarrow> P x))"
+ unfolding filtercomap_def
+proof (intro eventually_Abs_filter, unfold_locales, goal_cases)
+ case 1
+ show ?case by (auto intro!: exI[of _ "\<lambda>_. True"])
+next
+ case (2 P Q)
+ from 2(1) guess P' by (elim exE conjE) note P' = this
+ from 2(2) guess Q' by (elim exE conjE) note Q' = this
+ show ?case
+ by (rule exI[of _ "\<lambda>x. P' x \<and> Q' x"])
+ (insert P' Q', auto intro!: eventually_conj)
+next
+ case (3 P Q)
+ thus ?case by blast
+qed
+
+lemma filtercomap_ident: "filtercomap (\<lambda>x. x) F = F"
+ by (auto simp: filter_eq_iff eventually_filtercomap elim!: eventually_mono)
+
+lemma filtercomap_filtercomap: "filtercomap f (filtercomap g F) = filtercomap (\<lambda>x. g (f x)) F"
+ unfolding filter_eq_iff by (auto simp: eventually_filtercomap)
+
+lemma filtercomap_mono: "F \<le> F' \<Longrightarrow> filtercomap f F \<le> filtercomap f F'"
+ by (auto simp: eventually_filtercomap le_filter_def)
+
+lemma filtercomap_bot [simp]: "filtercomap f bot = bot"
+ by (auto simp: filter_eq_iff eventually_filtercomap)
+
+lemma filtercomap_top [simp]: "filtercomap f top = top"
+ by (auto simp: filter_eq_iff eventually_filtercomap)
+
+lemma filtercomap_inf: "filtercomap f (inf F1 F2) = inf (filtercomap f F1) (filtercomap f F2)"
+ unfolding filter_eq_iff
+proof safe
+ fix P
+ assume "eventually P (filtercomap f (F1 \<sqinter> F2))"
+ then obtain Q R S where *:
+ "eventually Q F1" "eventually R F2" "\<And>x. Q x \<Longrightarrow> R x \<Longrightarrow> S x" "\<And>x. S (f x) \<Longrightarrow> P x"
+ unfolding eventually_filtercomap eventually_inf by blast
+ from * have "eventually (\<lambda>x. Q (f x)) (filtercomap f F1)"
+ "eventually (\<lambda>x. R (f x)) (filtercomap f F2)"
+ by (auto simp: eventually_filtercomap)
+ with * show "eventually P (filtercomap f F1 \<sqinter> filtercomap f F2)"
+ unfolding eventually_inf by blast
+next
+ fix P
+ assume "eventually P (inf (filtercomap f F1) (filtercomap f F2))"
+ then obtain Q Q' R R' where *:
+ "eventually Q F1" "eventually R F2" "\<And>x. Q (f x) \<Longrightarrow> Q' x" "\<And>x. R (f x) \<Longrightarrow> R' x"
+ "\<And>x. Q' x \<Longrightarrow> R' x \<Longrightarrow> P x"
+ unfolding eventually_filtercomap eventually_inf by blast
+ from * have "eventually (\<lambda>x. Q x \<and> R x) (F1 \<sqinter> F2)" by (auto simp: eventually_inf)
+ with * show "eventually P (filtercomap f (F1 \<sqinter> F2))"
+ by (auto simp: eventually_filtercomap)
+qed
+
+lemma filtercomap_sup: "filtercomap f (sup F1 F2) \<ge> sup (filtercomap f F1) (filtercomap f F2)"
+ unfolding le_filter_def
+proof safe
+ fix P
+ assume "eventually P (filtercomap f (sup F1 F2))"
+ thus "eventually P (sup (filtercomap f F1) (filtercomap f F2))"
+ by (auto simp: filter_eq_iff eventually_filtercomap eventually_sup)
+qed
+
+lemma filtercomap_INF: "filtercomap f (INF b:B. F b) = (INF b:B. filtercomap f (F b))"
+proof -
+ have *: "filtercomap f (INF b:B. F b) = (INF b:B. filtercomap f (F b))" if "finite B" for B
+ using that by induction (simp_all add: filtercomap_inf)
+ show ?thesis unfolding filter_eq_iff
+ proof
+ fix P
+ have "eventually P (INF b:B. filtercomap f (F b)) \<longleftrightarrow>
+ (\<exists>X. (X \<subseteq> B \<and> finite X) \<and> eventually P (\<Sqinter>b\<in>X. filtercomap f (F b)))"
+ by (subst eventually_INF) blast
+ also have "\<dots> \<longleftrightarrow> (\<exists>X. (X \<subseteq> B \<and> finite X) \<and> eventually P (filtercomap f (INF b:X. F b)))"
+ by (rule ex_cong) (simp add: *)
+ also have "\<dots> \<longleftrightarrow> eventually P (filtercomap f (INFIMUM B F))"
+ unfolding eventually_filtercomap by (subst eventually_INF) blast
+ finally show "eventually P (filtercomap f (INFIMUM B F)) =
+ eventually P (\<Sqinter>b\<in>B. filtercomap f (F b))" ..
+ qed
+qed
+
+lemma filtercomap_SUP_finite:
+ "finite B \<Longrightarrow> filtercomap f (SUP b:B. F b) \<ge> (SUP b:B. filtercomap f (F b))"
+ by (induction B rule: finite_induct)
+ (auto intro: order_trans[OF _ order_trans[OF _ filtercomap_sup]] filtercomap_mono)
+
+lemma eventually_filtercomapI [intro]:
+ assumes "eventually P F"
+ shows "eventually (\<lambda>x. P (f x)) (filtercomap f F)"
+ using assms by (auto simp: eventually_filtercomap)
+
+lemma filtermap_filtercomap: "filtermap f (filtercomap f F) \<le> F"
+ by (auto simp: le_filter_def eventually_filtermap eventually_filtercomap)
+
+lemma filtercomap_filtermap: "filtercomap f (filtermap f F) \<ge> F"
+ unfolding le_filter_def eventually_filtermap eventually_filtercomap
+ by (auto elim!: eventually_mono)
+
+
subsubsection \<open>Standard filters\<close>
definition principal :: "'a set \<Rightarrow> 'a filter" where
@@ -605,6 +715,9 @@
lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
+
+lemma filtercomap_principal[simp]: "filtercomap f (principal A) = principal (f -` A)"
+ unfolding filter_eq_iff eventually_filtercomap eventually_principal by fast
subsubsection \<open>Order filters\<close>
@@ -618,6 +731,10 @@
unfolding at_top_def
by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
+lemma eventually_filtercomap_at_top_linorder:
+ "eventually P (filtercomap f at_top) \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>x. f x \<ge> N \<longrightarrow> P x)"
+ by (auto simp: eventually_filtercomap eventually_at_top_linorder)
+
lemma eventually_at_top_linorderI:
fixes c::"'a::linorder"
assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
@@ -637,6 +754,10 @@
by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex)
finally show ?thesis .
qed
+
+lemma eventually_filtercomap_at_top_dense:
+ "eventually P (filtercomap f at_top) \<longleftrightarrow> (\<exists>N::'a::{no_top, linorder}. \<forall>x. f x > N \<longrightarrow> P x)"
+ by (auto simp: eventually_filtercomap eventually_at_top_dense)
lemma eventually_at_top_not_equal [simp]: "eventually (\<lambda>x::'a::{no_top, linorder}. x \<noteq> c) at_top"
unfolding eventually_at_top_dense by auto
@@ -664,6 +785,10 @@
unfolding at_bot_def
by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
+lemma eventually_filtercomap_at_bot_linorder:
+ "eventually P (filtercomap f at_bot) \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>x. f x \<le> N \<longrightarrow> P x)"
+ by (auto simp: eventually_filtercomap eventually_at_bot_linorder)
+
lemma eventually_le_at_bot [simp]:
"eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
unfolding eventually_at_bot_linorder by auto
@@ -678,6 +803,10 @@
finally show ?thesis .
qed
+lemma eventually_filtercomap_at_bot_dense:
+ "eventually P (filtercomap f at_bot) \<longleftrightarrow> (\<exists>N::'a::{no_bot, linorder}. \<forall>x. f x < N \<longrightarrow> P x)"
+ by (auto simp: eventually_filtercomap eventually_at_bot_dense)
+
lemma eventually_at_bot_not_equal [simp]: "eventually (\<lambda>x::'a::{no_bot, linorder}. x \<noteq> c) at_bot"
unfolding eventually_at_bot_dense by auto
@@ -1201,6 +1330,9 @@
fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
+
+lemma filterlim_filtercomap [intro]: "filterlim f F (filtercomap f F)"
+ unfolding filterlim_def by (rule filtermap_filtercomap)
subsection \<open>Setup @{typ "'a filter"} for lifting and transfer\<close>
@@ -1390,6 +1522,25 @@
show "rel_filter A (principal S) (principal S')"
by(simp add: rel_filter_eventually eventually_principal) transfer_prover
qed
+
+lemma filtermap_parametric [transfer_rule]:
+ "((A ===> B) ===> rel_filter A ===> rel_filter B) filtermap filtermap"
+proof (intro rel_funI)
+ fix f g F G assume [transfer_rule]: "(A ===> B) f g" "rel_filter A F G"
+ show "rel_filter B (filtermap f F) (filtermap g G)"
+ unfolding rel_filter_eventually eventually_filtermap by transfer_prover
+qed
+
+(* TODO: Are those assumptions needed? *)
+lemma filtercomap_parametric [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique B" "bi_total A"
+ shows "((A ===> B) ===> rel_filter B ===> rel_filter A) filtercomap filtercomap"
+proof (intro rel_funI)
+ fix f g F G assume [transfer_rule]: "(A ===> B) f g" "rel_filter B F G"
+ show "rel_filter A (filtercomap f F) (filtercomap g G)"
+ unfolding rel_filter_eventually eventually_filtercomap by transfer_prover
+qed
+
context
fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
@@ -1443,6 +1594,7 @@
declare filterlim_principal [code]
declare principal_prod_principal [code]
declare filtermap_principal [code]
+declare filtercomap_principal [code]
declare eventually_principal [code]
declare inf_principal [code]
declare sup_principal [code]
--- a/src/HOL/Nunchaku/Nunchaku.thy Thu Jun 22 21:44:15 2017 +0200
+++ b/src/HOL/Nunchaku/Nunchaku.thy Thu Jun 22 21:48:57 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 Thu Jun 22 21:44:15 2017 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku.ML Thu Jun 22 21:48:57 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 Thu Jun 22 21:44:15 2017 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku_commands.ML Thu Jun 22 21:48:57 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 Thu Jun 22 21:44:15 2017 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku_tool.ML Thu Jun 22 21:48:57 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/Topological_Spaces.thy Thu Jun 22 21:44:15 2017 +0200
+++ b/src/HOL/Topological_Spaces.thy Thu Jun 22 21:48:57 2017 +0200
@@ -662,6 +662,17 @@
shows "eventually P (at_right a)"
using assms unfolding eventually_at_topological by (intro exI[of _ "{..<b}"]) auto
+lemma eventually_filtercomap_nhds:
+ "eventually P (filtercomap f (nhds x)) \<longleftrightarrow> (\<exists>S. open S \<and> x \<in> S \<and> (\<forall>x. f x \<in> S \<longrightarrow> P x))"
+ unfolding eventually_filtercomap eventually_nhds by auto
+
+lemma eventually_filtercomap_at_topological:
+ "eventually P (filtercomap f (at A within B)) \<longleftrightarrow>
+ (\<exists>S. open S \<and> A \<in> S \<and> (\<forall>x. f x \<in> S \<inter> B - {A} \<longrightarrow> P x))" (is "?lhs = ?rhs")
+ unfolding at_within_def filtercomap_inf eventually_inf_principal filtercomap_principal
+ eventually_filtercomap_nhds eventually_principal by blast
+
+
subsubsection \<open>Tendsto\<close>