--- a/src/HOL/Analysis/Arcwise_Connected.thy Mon Nov 04 17:06:18 2019 +0000
+++ b/src/HOL/Analysis/Arcwise_Connected.thy Tue Nov 05 12:00:23 2019 +0000
@@ -8,6 +8,25 @@
imports Path_Connected Ordered_Euclidean_Space "HOL-Computational_Algebra.Primes"
begin
+lemma path_connected_interval [simp]:
+ fixes a b::"'a::ordered_euclidean_space"
+ shows "path_connected {a..b}"
+ using is_interval_cc is_interval_path_connected by blast
+
+lemma segment_to_closest_point:
+ fixes S :: "'a :: euclidean_space set"
+ shows "\<lbrakk>closed S; S \<noteq> {}\<rbrakk> \<Longrightarrow> open_segment a (closest_point S a) \<inter> S = {}"
+ apply (subst disjoint_iff_not_equal)
+ apply (clarify dest!: dist_in_open_segment)
+ by (metis closest_point_le dist_commute le_less_trans less_irrefl)
+
+lemma segment_to_point_exists:
+ fixes S :: "'a :: euclidean_space set"
+ assumes "closed S" "S \<noteq> {}"
+ obtains b where "b \<in> S" "open_segment a b \<inter> S = {}"
+ by (metis assms segment_to_closest_point closest_point_exists that)
+
+
subsection \<open>The Brouwer reduction theorem\<close>
theorem Brouwer_reduction_theorem_gen:
--- a/src/HOL/Analysis/Borel_Space.thy Mon Nov 04 17:06:18 2019 +0000
+++ b/src/HOL/Analysis/Borel_Space.thy Tue Nov 05 12:00:23 2019 +0000
@@ -10,6 +10,9 @@
Measurable Derivative Ordered_Euclidean_Space Extended_Real_Limits
begin
+lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
+ by (auto simp: real_atLeastGreaterThan_eq)
+
lemma sets_Collect_eventually_sequentially[measurable]:
"(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
unfolding eventually_sequentially by simp
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Mon Nov 04 17:06:18 2019 +0000
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Tue Nov 05 12:00:23 2019 +0000
@@ -47,33 +47,6 @@
subsection\<open>Closures and interiors of halfspaces\<close>
-lemma interior_halfspace_le [simp]:
- assumes "a \<noteq> 0"
- shows "interior {x. a \<bullet> x \<le> b} = {x. a \<bullet> x < b}"
-proof -
- have *: "a \<bullet> x < b" if x: "x \<in> S" and S: "S \<subseteq> {x. a \<bullet> x \<le> b}" and "open S" for S x
- proof -
- obtain e where "e>0" and e: "cball x e \<subseteq> S"
- using \<open>open S\<close> open_contains_cball x by blast
- then have "x + (e / norm a) *\<^sub>R a \<in> cball x e"
- by (simp add: dist_norm)
- then have "x + (e / norm a) *\<^sub>R a \<in> S"
- using e by blast
- then have "x + (e / norm a) *\<^sub>R a \<in> {x. a \<bullet> x \<le> b}"
- using S by blast
- moreover have "e * (a \<bullet> a) / norm a > 0"
- by (simp add: \<open>0 < e\<close> assms)
- ultimately show ?thesis
- by (simp add: algebra_simps)
- qed
- show ?thesis
- by (rule interior_unique) (auto simp: open_halfspace_lt *)
-qed
-
-lemma interior_halfspace_ge [simp]:
- "a \<noteq> 0 \<Longrightarrow> interior {x. a \<bullet> x \<ge> b} = {x. a \<bullet> x > b}"
-using interior_halfspace_le [of "-a" "-b"] by simp
-
lemma interior_halfspace_component_le [simp]:
"interior {x. x$k \<le> a} = {x :: (real^'n). x$k < a}" (is "?LE")
and interior_halfspace_component_ge [simp]:
@@ -88,21 +61,6 @@
interior_halfspace_ge [of "axis k (1::real)" a] by auto
qed
-lemma closure_halfspace_lt [simp]:
- assumes "a \<noteq> 0"
- shows "closure {x. a \<bullet> x < b} = {x. a \<bullet> x \<le> b}"
-proof -
- have [simp]: "-{x. a \<bullet> x < b} = {x. a \<bullet> x \<ge> b}"
- by (force simp:)
- then show ?thesis
- using interior_halfspace_ge [of a b] assms
- by (force simp: closure_interior)
-qed
-
-lemma closure_halfspace_gt [simp]:
- "a \<noteq> 0 \<Longrightarrow> closure {x. a \<bullet> x > b} = {x. a \<bullet> x \<ge> b}"
-using closure_halfspace_lt [of "-a" "-b"] by simp
-
lemma closure_halfspace_component_lt [simp]:
"closure {x. x$k < a} = {x :: (real^'n). x$k \<le> a}" (is "?LE")
and closure_halfspace_component_gt [simp]:
@@ -117,56 +75,6 @@
closure_halfspace_gt [of "axis k (1::real)" a] by auto
qed
-lemma interior_hyperplane [simp]:
- assumes "a \<noteq> 0"
- shows "interior {x. a \<bullet> x = b} = {}"
-proof -
- have [simp]: "{x. a \<bullet> x = b} = {x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x \<ge> b}"
- by (force simp:)
- then show ?thesis
- by (auto simp: assms)
-qed
-
-lemma frontier_halfspace_le:
- assumes "a \<noteq> 0 \<or> b \<noteq> 0"
- shows "frontier {x. a \<bullet> x \<le> b} = {x. a \<bullet> x = b}"
-proof (cases "a = 0")
- case True with assms show ?thesis by simp
-next
- case False then show ?thesis
- by (force simp: frontier_def closed_halfspace_le)
-qed
-
-lemma frontier_halfspace_ge:
- assumes "a \<noteq> 0 \<or> b \<noteq> 0"
- shows "frontier {x. a \<bullet> x \<ge> b} = {x. a \<bullet> x = b}"
-proof (cases "a = 0")
- case True with assms show ?thesis by simp
-next
- case False then show ?thesis
- by (force simp: frontier_def closed_halfspace_ge)
-qed
-
-lemma frontier_halfspace_lt:
- assumes "a \<noteq> 0 \<or> b \<noteq> 0"
- shows "frontier {x. a \<bullet> x < b} = {x. a \<bullet> x = b}"
-proof (cases "a = 0")
- case True with assms show ?thesis by simp
-next
- case False then show ?thesis
- by (force simp: frontier_def interior_open open_halfspace_lt)
-qed
-
-lemma frontier_halfspace_gt:
- assumes "a \<noteq> 0 \<or> b \<noteq> 0"
- shows "frontier {x. a \<bullet> x > b} = {x. a \<bullet> x = b}"
-proof (cases "a = 0")
- case True with assms show ?thesis by simp
-next
- case False then show ?thesis
- by (force simp: frontier_def interior_open open_halfspace_gt)
-qed
-
lemma interior_standard_hyperplane:
"interior {x :: (real^'n). x$k = a} = {}"
proof -
@@ -623,6 +531,11 @@
qed
qed simp
+lemma vec_nth_real_1_iff_cbox [simp]:
+ fixes a b :: real
+ shows "(\<lambda>x::real^1. x $ 1) ` S = {a..b} \<longleftrightarrow> S = cbox (vec a) (vec b)"
+ using vec_nth_1_iff_cbox[of S a b]
+ by simp
lemma interval_split_cart:
"{a..b::real^'n} \<inter> {x. x$k \<le> c} = {a .. (\<chi> i. if i = k then min (b$k) c else b$i)}"
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Mon Nov 04 17:06:18 2019 +0000
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Tue Nov 05 12:00:23 2019 +0000
@@ -145,13 +145,13 @@
by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
from assms show "Re z = Re a" by (auto simp: u)
from u(1) show "Im z \<in> closed_segment (Im a) (Im b)"
- by (intro closed_segmentI[of u]) (auto simp: u algebra_simps)
+ by (force simp: u closed_segment_def algebra_simps)
next
fix z assume [simp]: "Re z = Re a" and "Im z \<in> closed_segment (Im a) (Im b)"
then obtain u where u: "u \<in> {0..1}" "Im z = Im a + of_real u * (Im b - Im a)"
by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
from u(1) show "z \<in> closed_segment a b" using assms
- by (intro closed_segmentI[of u]) (auto simp: u algebra_simps scaleR_conv_of_real complex_eq_iff)
+ by (force simp: u closed_segment_def algebra_simps scaleR_conv_of_real complex_eq_iff)
qed
lemma closed_segment_same_Im:
@@ -163,13 +163,13 @@
by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
from assms show "Im z = Im a" by (auto simp: u)
from u(1) show "Re z \<in> closed_segment (Re a) (Re b)"
- by (intro closed_segmentI[of u]) (auto simp: u algebra_simps)
+ by (force simp: u closed_segment_def algebra_simps)
next
fix z assume [simp]: "Im z = Im a" and "Re z \<in> closed_segment (Re a) (Re b)"
then obtain u where u: "u \<in> {0..1}" "Re z = Re a + of_real u * (Re b - Re a)"
by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
from u(1) show "z \<in> closed_segment a b" using assms
- by (intro closed_segmentI[of u]) (auto simp: u algebra_simps scaleR_conv_of_real complex_eq_iff)
+ by (force simp: u closed_segment_def algebra_simps scaleR_conv_of_real complex_eq_iff)
qed
subsection\<open>Holomorphic functions\<close>
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Nov 04 17:06:18 2019 +0000
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Nov 05 12:00:23 2019 +0000
@@ -16,249 +16,6 @@
subsection\<^marker>\<open>tag unimportant\<close> \<open>Topological Properties of Convex Sets and Functions\<close>
-lemma convex_supp_sum:
- assumes "convex S" and 1: "supp_sum u I = 1"
- and "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> u i \<and> (u i = 0 \<or> f i \<in> S)"
- shows "supp_sum (\<lambda>i. u i *\<^sub>R f i) I \<in> S"
-proof -
- have fin: "finite {i \<in> I. u i \<noteq> 0}"
- using 1 sum.infinite by (force simp: supp_sum_def support_on_def)
- then have eq: "supp_sum (\<lambda>i. u i *\<^sub>R f i) I = sum (\<lambda>i. u i *\<^sub>R f i) {i \<in> I. u i \<noteq> 0}"
- by (force intro: sum.mono_neutral_left simp: supp_sum_def support_on_def)
- show ?thesis
- apply (simp add: eq)
- apply (rule convex_sum [OF fin \<open>convex S\<close>])
- using 1 assms apply (auto simp: supp_sum_def support_on_def)
- done
-qed
-
-lemma closure_bounded_linear_image_subset:
- assumes f: "bounded_linear f"
- shows "f ` closure S \<subseteq> closure (f ` S)"
- using linear_continuous_on [OF f] closed_closure closure_subset
- by (rule image_closure_subset)
-
-lemma closure_linear_image_subset:
- fixes f :: "'m::euclidean_space \<Rightarrow> 'n::real_normed_vector"
- assumes "linear f"
- shows "f ` (closure S) \<subseteq> closure (f ` S)"
- using assms unfolding linear_conv_bounded_linear
- by (rule closure_bounded_linear_image_subset)
-
-lemma closed_injective_linear_image:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes S: "closed S" and f: "linear f" "inj f"
- shows "closed (f ` S)"
-proof -
- obtain g where g: "linear g" "g \<circ> f = id"
- using linear_injective_left_inverse [OF f] by blast
- then have confg: "continuous_on (range f) g"
- using linear_continuous_on linear_conv_bounded_linear by blast
- have [simp]: "g ` f ` S = S"
- using g by (simp add: image_comp)
- have cgf: "closed (g ` f ` S)"
- by (simp add: \<open>g \<circ> f = id\<close> S image_comp)
- have [simp]: "(range f \<inter> g -` S) = f ` S"
- using g unfolding o_def id_def image_def by auto metis+
- show ?thesis
- proof (rule closedin_closed_trans [of "range f"])
- show "closedin (top_of_set (range f)) (f ` S)"
- using continuous_closedin_preimage [OF confg cgf] by simp
- show "closed (range f)"
- apply (rule closed_injective_image_subspace)
- using f apply (auto simp: linear_linear linear_injective_0)
- done
- qed
-qed
-
-lemma closed_injective_linear_image_eq:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes f: "linear f" "inj f"
- shows "(closed(image f s) \<longleftrightarrow> closed s)"
- by (metis closed_injective_linear_image closure_eq closure_linear_image_subset closure_subset_eq f(1) f(2) inj_image_subset_iff)
-
-lemma closure_injective_linear_image:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- shows "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)"
- apply (rule subset_antisym)
- apply (simp add: closure_linear_image_subset)
- by (simp add: closure_minimal closed_injective_linear_image closure_subset image_mono)
-
-lemma closure_bounded_linear_image:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- shows "\<lbrakk>linear f; bounded S\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)"
- apply (rule subset_antisym, simp add: closure_linear_image_subset)
- apply (rule closure_minimal, simp add: closure_subset image_mono)
- by (meson bounded_closure closed_closure compact_continuous_image compact_eq_bounded_closed linear_continuous_on linear_conv_bounded_linear)
-
-lemma closure_scaleR:
- fixes S :: "'a::real_normed_vector set"
- shows "((*\<^sub>R) c) ` (closure S) = closure (((*\<^sub>R) c) ` S)"
-proof
- show "((*\<^sub>R) c) ` (closure S) \<subseteq> closure (((*\<^sub>R) c) ` S)"
- using bounded_linear_scaleR_right
- by (rule closure_bounded_linear_image_subset)
- show "closure (((*\<^sub>R) c) ` S) \<subseteq> ((*\<^sub>R) c) ` (closure S)"
- by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure)
-qed
-
-lemma sphere_eq_empty [simp]:
- fixes a :: "'a::{real_normed_vector, perfect_space}"
- shows "sphere a r = {} \<longleftrightarrow> r < 0"
-by (auto simp: sphere_def dist_norm) (metis dist_norm le_less_linear vector_choose_dist)
-
-lemma cone_closure:
- fixes S :: "'a::real_normed_vector set"
- assumes "cone S"
- shows "cone (closure S)"
-proof (cases "S = {}")
- case True
- then show ?thesis by auto
-next
- case False
- then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)"
- using cone_iff[of S] assms by auto
- then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` closure S = closure S)"
- using closure_subset by (auto simp: closure_scaleR)
- then show ?thesis
- using False cone_iff[of "closure S"] by auto
-qed
-
-corollary component_complement_connected:
- fixes S :: "'a::real_normed_vector set"
- assumes "connected S" "C \<in> components (-S)"
- shows "connected(-C)"
- using component_diff_connected [of S UNIV] assms
- by (auto simp: Compl_eq_Diff_UNIV)
-
-proposition clopen:
- fixes S :: "'a :: real_normed_vector set"
- shows "closed S \<and> open S \<longleftrightarrow> S = {} \<or> S = UNIV"
- by (force intro!: connected_UNIV [unfolded connected_clopen, rule_format])
-
-corollary compact_open:
- fixes S :: "'a :: euclidean_space set"
- shows "compact S \<and> open S \<longleftrightarrow> S = {}"
- by (auto simp: compact_eq_bounded_closed clopen)
-
-corollary finite_imp_not_open:
- fixes S :: "'a::{real_normed_vector, perfect_space} set"
- shows "\<lbrakk>finite S; open S\<rbrakk> \<Longrightarrow> S={}"
- using clopen [of S] finite_imp_closed not_bounded_UNIV by blast
-
-corollary empty_interior_finite:
- fixes S :: "'a::{real_normed_vector, perfect_space} set"
- shows "finite S \<Longrightarrow> interior S = {}"
- by (metis interior_subset finite_subset open_interior [of S] finite_imp_not_open)
-
-text \<open>Balls, being convex, are connected.\<close>
-
-lemma convex_local_global_minimum:
- fixes s :: "'a::real_normed_vector set"
- assumes "e > 0"
- and "convex_on s f"
- and "ball x e \<subseteq> s"
- and "\<forall>y\<in>ball x e. f x \<le> f y"
- shows "\<forall>y\<in>s. f x \<le> f y"
-proof (rule ccontr)
- have "x \<in> s" using assms(1,3) by auto
- assume "\<not> ?thesis"
- then obtain y where "y\<in>s" and y: "f x > f y" by auto
- then have xy: "0 < dist x y" by auto
- then obtain u where "0 < u" "u \<le> 1" and u: "u < e / dist x y"
- using field_lbound_gt_zero[of 1 "e / dist x y"] xy \<open>e>0\<close> by auto
- then have "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y"
- using \<open>x\<in>s\<close> \<open>y\<in>s\<close>
- using assms(2)[unfolded convex_on_def,
- THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]]
- by auto
- moreover
- have *: "x - ((1 - u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x - y)"
- by (simp add: algebra_simps)
- have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> ball x e"
- unfolding mem_ball dist_norm
- unfolding * and norm_scaleR and abs_of_pos[OF \<open>0<u\<close>]
- unfolding dist_norm[symmetric]
- using u
- unfolding pos_less_divide_eq[OF xy]
- by auto
- then have "f x \<le> f ((1 - u) *\<^sub>R x + u *\<^sub>R y)"
- using assms(4) by auto
- ultimately show False
- using mult_strict_left_mono[OF y \<open>u>0\<close>]
- unfolding left_diff_distrib
- by auto
-qed
-
-lemma convex_ball [iff]:
- fixes x :: "'a::real_normed_vector"
- shows "convex (ball x e)"
-proof (auto simp: convex_def)
- fix y z
- assume yz: "dist x y < e" "dist x z < e"
- fix u v :: real
- assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
- have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
- using uv yz
- using convex_on_dist [of "ball x e" x, unfolded convex_on_def,
- THEN bspec[where x=y], THEN bspec[where x=z]]
- by auto
- then show "dist x (u *\<^sub>R y + v *\<^sub>R z) < e"
- using convex_bound_lt[OF yz uv] by auto
-qed
-
-lemma convex_cball [iff]:
- fixes x :: "'a::real_normed_vector"
- shows "convex (cball x e)"
-proof -
- {
- fix y z
- assume yz: "dist x y \<le> e" "dist x z \<le> e"
- fix u v :: real
- assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
- have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
- using uv yz
- using convex_on_dist [of "cball x e" x, unfolded convex_on_def,
- THEN bspec[where x=y], THEN bspec[where x=z]]
- by auto
- then have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e"
- using convex_bound_le[OF yz uv] by auto
- }
- then show ?thesis by (auto simp: convex_def Ball_def)
-qed
-
-lemma connected_ball [iff]:
- fixes x :: "'a::real_normed_vector"
- shows "connected (ball x e)"
- using convex_connected convex_ball by auto
-
-lemma connected_cball [iff]:
- fixes x :: "'a::real_normed_vector"
- shows "connected (cball x e)"
- using convex_connected convex_cball by auto
-
-
-lemma bounded_convex_hull:
- fixes s :: "'a::real_normed_vector set"
- assumes "bounded s"
- shows "bounded (convex hull s)"
-proof -
- from assms obtain B where B: "\<forall>x\<in>s. norm x \<le> B"
- unfolding bounded_iff by auto
- show ?thesis
- apply (rule bounded_subset[OF bounded_cball, of _ 0 B])
- unfolding subset_hull[of convex, OF convex_cball]
- unfolding subset_eq mem_cball dist_norm using B
- apply auto
- done
-qed
-
-lemma finite_imp_bounded_convex_hull:
- fixes s :: "'a::real_normed_vector set"
- shows "finite s \<Longrightarrow> bounded (convex hull s)"
- using bounded_convex_hull finite_imp_bounded
- by auto
-
lemma aff_dim_cball:
fixes a :: "'n::euclidean_space"
assumes "e > 0"
@@ -2059,9 +1816,6 @@
shows "is_interval s \<longleftrightarrow> convex s"
by (metis is_interval_convex convex_connected is_interval_connected_1)
-lemma is_interval_ball_real: "is_interval (ball a b)" for a b::real
- by (metis connected_ball is_interval_connected_1)
-
lemma connected_compact_interval_1:
"connected S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = {a..b::real})"
by (auto simp: is_interval_connected_1 [symmetric] is_interval_compact)
@@ -2087,9 +1841,6 @@
by (metis connected_convex_1 convex_linear_vimage linf convex_connected connected_linear_image)
qed
-lemma is_interval_cball_1[intro, simp]: "is_interval (cball a b)" for a b::real
- by (simp add: is_interval_convex_1)
-
lemma [simp]:
fixes r s::real
shows is_interval_io: "is_interval {..<r}"
@@ -2521,613 +2272,4 @@
using \<open>d > 0\<close> by auto
qed
-
-section \<open>Line Segments\<close>
-
-subsection \<open>Midpoint\<close>
-
-definition\<^marker>\<open>tag important\<close> midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
- where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
-
-lemma midpoint_idem [simp]: "midpoint x x = x"
- unfolding midpoint_def by simp
-
-lemma midpoint_sym: "midpoint a b = midpoint b a"
- unfolding midpoint_def by (auto simp add: scaleR_right_distrib)
-
-lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c"
-proof -
- have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c"
- by simp
- then show ?thesis
- unfolding midpoint_def scaleR_2 [symmetric] by simp
-qed
-
-lemma
- fixes a::real
- assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b"
- and le_midpoint_1: "midpoint a b \<le> b"
- by (simp_all add: midpoint_def assms)
-
-lemma dist_midpoint:
- fixes a b :: "'a::real_normed_vector" shows
- "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
- "dist b (midpoint a b) = (dist a b) / 2" (is ?t2)
- "dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
- "dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
-proof -
- have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2"
- unfolding equation_minus_iff by auto
- have **: "\<And>x y::'a. 2 *\<^sub>R x = y \<Longrightarrow> norm x = (norm y) / 2"
- by auto
- note scaleR_right_distrib [simp]
- show ?t1
- unfolding midpoint_def dist_norm
- apply (rule **)
- apply (simp add: scaleR_right_diff_distrib)
- apply (simp add: scaleR_2)
- done
- show ?t2
- unfolding midpoint_def dist_norm
- apply (rule *)
- apply (simp add: scaleR_right_diff_distrib)
- apply (simp add: scaleR_2)
- done
- show ?t3
- unfolding midpoint_def dist_norm
- apply (rule *)
- apply (simp add: scaleR_right_diff_distrib)
- apply (simp add: scaleR_2)
- done
- show ?t4
- unfolding midpoint_def dist_norm
- apply (rule **)
- apply (simp add: scaleR_right_diff_distrib)
- apply (simp add: scaleR_2)
- done
-qed
-
-lemma midpoint_eq_endpoint [simp]:
- "midpoint a b = a \<longleftrightarrow> a = b"
- "midpoint a b = b \<longleftrightarrow> a = b"
- unfolding midpoint_eq_iff by auto
-
-lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b"
- using midpoint_eq_iff by metis
-
-lemma midpoint_linear_image:
- "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
-by (simp add: linear_iff midpoint_def)
-
-
-subsection \<open>Line segments\<close>
-
-definition\<^marker>\<open>tag important\<close> closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
- where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
-
-definition\<^marker>\<open>tag important\<close> open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
- "open_segment a b \<equiv> closed_segment a b - {a,b}"
-
-lemmas segment = open_segment_def closed_segment_def
-
-lemma in_segment:
- "x \<in> closed_segment a b \<longleftrightarrow> (\<exists>u. 0 \<le> u \<and> u \<le> 1 \<and> x = (1 - u) *\<^sub>R a + u *\<^sub>R b)"
- "x \<in> open_segment a b \<longleftrightarrow> a \<noteq> b \<and> (\<exists>u. 0 < u \<and> u < 1 \<and> x = (1 - u) *\<^sub>R a + u *\<^sub>R b)"
- using less_eq_real_def by (auto simp: segment algebra_simps)
-
-lemma closed_segmentI:
- "u \<in> {0..1} \<Longrightarrow> z = (1 - u) *\<^sub>R a + u *\<^sub>R b \<Longrightarrow> z \<in> closed_segment a b"
- by (auto simp: closed_segment_def)
-
-lemma closed_segment_linear_image:
- "closed_segment (f a) (f b) = f ` (closed_segment a b)" if "linear f"
-proof -
- interpret linear f by fact
- show ?thesis
- by (force simp add: in_segment add scale)
-qed
-
-lemma open_segment_linear_image:
- "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> open_segment (f a) (f b) = f ` (open_segment a b)"
- by (force simp: open_segment_def closed_segment_linear_image inj_on_def)
-
-lemma closed_segment_translation:
- "closed_segment (c + a) (c + b) = image (\<lambda>x. c + x) (closed_segment a b)"
-apply safe
-apply (rule_tac x="x-c" in image_eqI)
-apply (auto simp: in_segment algebra_simps)
-done
-
-lemma open_segment_translation:
- "open_segment (c + a) (c + b) = image (\<lambda>x. c + x) (open_segment a b)"
-by (simp add: open_segment_def closed_segment_translation translation_diff)
-
-lemma closed_segment_of_real:
- "closed_segment (of_real x) (of_real y) = of_real ` closed_segment x y"
- apply (auto simp: image_iff in_segment scaleR_conv_of_real)
- apply (rule_tac x="(1-u)*x + u*y" in bexI)
- apply (auto simp: in_segment)
- done
-
-lemma open_segment_of_real:
- "open_segment (of_real x) (of_real y) = of_real ` open_segment x y"
- apply (auto simp: image_iff in_segment scaleR_conv_of_real)
- apply (rule_tac x="(1-u)*x + u*y" in bexI)
- apply (auto simp: in_segment)
- done
-
-lemma closed_segment_Reals:
- "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> closed_segment x y = of_real ` closed_segment (Re x) (Re y)"
- by (metis closed_segment_of_real of_real_Re)
-
-lemma open_segment_Reals:
- "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> open_segment x y = of_real ` open_segment (Re x) (Re y)"
- by (metis open_segment_of_real of_real_Re)
-
-lemma open_segment_PairD:
- "(x, x') \<in> open_segment (a, a') (b, b')
- \<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> a' = b')"
- by (auto simp: in_segment)
-
-lemma closed_segment_PairD:
- "(x, x') \<in> closed_segment (a, a') (b, b') \<Longrightarrow> x \<in> closed_segment a b \<and> x' \<in> closed_segment a' b'"
- by (auto simp: closed_segment_def)
-
-lemma closed_segment_translation_eq [simp]:
- "d + x \<in> closed_segment (d + a) (d + b) \<longleftrightarrow> x \<in> closed_segment a b"
-proof -
- have *: "\<And>d x a b. x \<in> closed_segment a b \<Longrightarrow> d + x \<in> closed_segment (d + a) (d + b)"
- apply (simp add: closed_segment_def)
- apply (erule ex_forward)
- apply (simp add: algebra_simps)
- done
- show ?thesis
- using * [where d = "-d"] *
- by (fastforce simp add:)
-qed
-
-lemma open_segment_translation_eq [simp]:
- "d + x \<in> open_segment (d + a) (d + b) \<longleftrightarrow> x \<in> open_segment a b"
- by (simp add: open_segment_def)
-
-lemma of_real_closed_segment [simp]:
- "of_real x \<in> closed_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> closed_segment a b"
- apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward)
- using of_real_eq_iff by fastforce
-
-lemma of_real_open_segment [simp]:
- "of_real x \<in> open_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> open_segment a b"
- apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE)
- using of_real_eq_iff by fastforce
-
-lemma convex_contains_segment:
- "convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)"
- unfolding convex_alt closed_segment_def by auto
-
-lemma closed_segment_in_Reals:
- "\<lbrakk>x \<in> closed_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals"
- by (meson subsetD convex_Reals convex_contains_segment)
-
-lemma open_segment_in_Reals:
- "\<lbrakk>x \<in> open_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals"
- by (metis Diff_iff closed_segment_in_Reals open_segment_def)
-
-lemma closed_segment_subset: "\<lbrakk>x \<in> S; y \<in> S; convex S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> S"
- by (simp add: convex_contains_segment)
-
-lemma closed_segment_subset_convex_hull:
- "\<lbrakk>x \<in> convex hull S; y \<in> convex hull S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull S"
- using convex_contains_segment by blast
-
-lemma segment_convex_hull:
- "closed_segment a b = convex hull {a,b}"
-proof -
- have *: "\<And>x. {x} \<noteq> {}" by auto
- show ?thesis
- unfolding segment convex_hull_insert[OF *] convex_hull_singleton
- by (safe; rule_tac x="1 - u" in exI; force)
-qed
-
-lemma open_closed_segment: "u \<in> open_segment w z \<Longrightarrow> u \<in> closed_segment w z"
- by (auto simp add: closed_segment_def open_segment_def)
-
-lemma segment_open_subset_closed:
- "open_segment a b \<subseteq> closed_segment a b"
- by (auto simp: closed_segment_def open_segment_def)
-
-lemma bounded_closed_segment:
- fixes a :: "'a::euclidean_space" shows "bounded (closed_segment a b)"
- by (simp add: segment_convex_hull compact_convex_hull compact_imp_bounded)
-
-lemma bounded_open_segment:
- fixes a :: "'a::euclidean_space" shows "bounded (open_segment a b)"
- by (rule bounded_subset [OF bounded_closed_segment segment_open_subset_closed])
-
-lemmas bounded_segment = bounded_closed_segment open_closed_segment
-
-lemma ends_in_segment [iff]: "a \<in> closed_segment a b" "b \<in> closed_segment a b"
- unfolding segment_convex_hull
- by (auto intro!: hull_subset[unfolded subset_eq, rule_format])
-
-lemma eventually_closed_segment:
- fixes x0::"'a::real_normed_vector"
- assumes "open X0" "x0 \<in> X0"
- shows "\<forall>\<^sub>F x in at x0 within U. closed_segment x0 x \<subseteq> X0"
-proof -
- from openE[OF assms]
- obtain e where e: "0 < e" "ball x0 e \<subseteq> X0" .
- then have "\<forall>\<^sub>F x in at x0 within U. x \<in> ball x0 e"
- by (auto simp: dist_commute eventually_at)
- then show ?thesis
- proof eventually_elim
- case (elim x)
- have "x0 \<in> ball x0 e" using \<open>e > 0\<close> by simp
- from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim]
- have "closed_segment x0 x \<subseteq> ball x0 e" .
- also note \<open>\<dots> \<subseteq> X0\<close>
- finally show ?case .
- qed
-qed
-
-lemma segment_furthest_le:
- fixes a b x y :: "'a::euclidean_space"
- assumes "x \<in> closed_segment a b"
- shows "norm (y - x) \<le> norm (y - a) \<or> norm (y - x) \<le> norm (y - b)"
-proof -
- obtain z where "z \<in> {a, b}" "norm (x - y) \<le> norm (z - y)"
- using simplex_furthest_le[of "{a, b}" y]
- using assms[unfolded segment_convex_hull]
- by auto
- then show ?thesis
- by (auto simp add:norm_minus_commute)
-qed
-
-lemma closed_segment_commute: "closed_segment a b = closed_segment b a"
-proof -
- have "{a, b} = {b, a}" by auto
- thus ?thesis
- by (simp add: segment_convex_hull)
-qed
-
-lemma segment_bound1:
- assumes "x \<in> closed_segment a b"
- shows "norm (x - a) \<le> norm (b - a)"
-proof -
- obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1"
- using assms by (auto simp add: closed_segment_def)
- then show "norm (x - a) \<le> norm (b - a)"
- apply clarify
- apply (auto simp: algebra_simps)
- apply (simp add: scaleR_diff_right [symmetric] mult_left_le_one_le)
- done
-qed
-
-lemma segment_bound:
- assumes "x \<in> closed_segment a b"
- shows "norm (x - a) \<le> norm (b - a)" "norm (x - b) \<le> norm (b - a)"
-apply (simp add: assms segment_bound1)
-by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1)
-
-lemma open_segment_commute: "open_segment a b = open_segment b a"
-proof -
- have "{a, b} = {b, a}" by auto
- thus ?thesis
- by (simp add: closed_segment_commute open_segment_def)
-qed
-
-lemma closed_segment_idem [simp]: "closed_segment a a = {a}"
- unfolding segment by (auto simp add: algebra_simps)
-
-lemma open_segment_idem [simp]: "open_segment a a = {}"
- by (simp add: open_segment_def)
-
-lemma closed_segment_eq_open: "closed_segment a b = open_segment a b \<union> {a,b}"
- using open_segment_def by auto
-
-lemma convex_contains_open_segment:
- "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. open_segment a b \<subseteq> s)"
- by (simp add: convex_contains_segment closed_segment_eq_open)
-
-lemma closed_segment_eq_real_ivl:
- fixes a b::real
- shows "closed_segment a b = (if a \<le> b then {a .. b} else {b .. a})"
-proof -
- have "b \<le> a \<Longrightarrow> closed_segment b a = {b .. a}"
- and "a \<le> b \<Longrightarrow> closed_segment a b = {a .. b}"
- by (auto simp: convex_hull_eq_real_cbox segment_convex_hull)
- thus ?thesis
- by (auto simp: closed_segment_commute)
-qed
-
-lemma open_segment_eq_real_ivl:
- fixes a b::real
- shows "open_segment a b = (if a \<le> b then {a<..<b} else {b<..<a})"
-by (auto simp: closed_segment_eq_real_ivl open_segment_def split: if_split_asm)
-
-lemma closed_segment_real_eq:
- fixes u::real shows "closed_segment u v = (\<lambda>x. (v - u) * x + u) ` {0..1}"
- by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl)
-
-lemma dist_in_closed_segment:
- fixes a :: "'a :: euclidean_space"
- assumes "x \<in> closed_segment a b"
- shows "dist x a \<le> dist a b \<and> dist x b \<le> dist a b"
-proof (intro conjI)
- obtain u where u: "0 \<le> u" "u \<le> 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
- using assms by (force simp: in_segment algebra_simps)
- have "dist x a = u * dist a b"
- apply (simp add: dist_norm algebra_simps x)
- by (metis \<open>0 \<le> u\<close> abs_of_nonneg norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib)
- also have "... \<le> dist a b"
- by (simp add: mult_left_le_one_le u)
- finally show "dist x a \<le> dist a b" .
- have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)"
- by (simp add: dist_norm algebra_simps x)
- also have "... = (1-u) * dist a b"
- proof -
- have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
- using \<open>u \<le> 1\<close> by force
- then show ?thesis
- by (simp add: dist_norm real_vector.scale_right_diff_distrib)
- qed
- also have "... \<le> dist a b"
- by (simp add: mult_left_le_one_le u)
- finally show "dist x b \<le> dist a b" .
-qed
-
-lemma dist_in_open_segment:
- fixes a :: "'a :: euclidean_space"
- assumes "x \<in> open_segment a b"
- shows "dist x a < dist a b \<and> dist x b < dist a b"
-proof (intro conjI)
- obtain u where u: "0 < u" "u < 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
- using assms by (force simp: in_segment algebra_simps)
- have "dist x a = u * dist a b"
- apply (simp add: dist_norm algebra_simps x)
- by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib \<open>0 < u\<close>)
- also have *: "... < dist a b"
- by (metis (no_types) assms dist_eq_0_iff dist_not_less_zero in_segment(2) linorder_neqE_linordered_idom mult.left_neutral real_mult_less_iff1 \<open>u < 1\<close>)
- finally show "dist x a < dist a b" .
- have ab_ne0: "dist a b \<noteq> 0"
- using * by fastforce
- have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)"
- by (simp add: dist_norm algebra_simps x)
- also have "... = (1-u) * dist a b"
- proof -
- have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
- using \<open>u < 1\<close> by force
- then show ?thesis
- by (simp add: dist_norm real_vector.scale_right_diff_distrib)
- qed
- also have "... < dist a b"
- using ab_ne0 \<open>0 < u\<close> by simp
- finally show "dist x b < dist a b" .
-qed
-
-lemma dist_decreases_open_segment_0:
- fixes x :: "'a :: euclidean_space"
- assumes "x \<in> open_segment 0 b"
- shows "dist c x < dist c 0 \<or> dist c x < dist c b"
-proof (rule ccontr, clarsimp simp: not_less)
- obtain u where u: "0 \<noteq> b" "0 < u" "u < 1" and x: "x = u *\<^sub>R b"
- using assms by (auto simp: in_segment)
- have xb: "x \<bullet> b < b \<bullet> b"
- using u x by auto
- assume "norm c \<le> dist c x"
- then have "c \<bullet> c \<le> (c - x) \<bullet> (c - x)"
- by (simp add: dist_norm norm_le)
- moreover have "0 < x \<bullet> b"
- using u x by auto
- ultimately have less: "c \<bullet> b < x \<bullet> b"
- by (simp add: x algebra_simps inner_commute u)
- assume "dist c b \<le> dist c x"
- then have "(c - b) \<bullet> (c - b) \<le> (c - x) \<bullet> (c - x)"
- by (simp add: dist_norm norm_le)
- then have "(b \<bullet> b) * (1 - u*u) \<le> 2 * (b \<bullet> c) * (1-u)"
- by (simp add: x algebra_simps inner_commute)
- then have "(1+u) * (b \<bullet> b) * (1-u) \<le> 2 * (b \<bullet> c) * (1-u)"
- by (simp add: algebra_simps)
- then have "(1+u) * (b \<bullet> b) \<le> 2 * (b \<bullet> c)"
- using \<open>u < 1\<close> by auto
- with xb have "c \<bullet> b \<ge> x \<bullet> b"
- by (auto simp: x algebra_simps inner_commute)
- with less show False by auto
-qed
-
-proposition dist_decreases_open_segment:
- fixes a :: "'a :: euclidean_space"
- assumes "x \<in> open_segment a b"
- shows "dist c x < dist c a \<or> dist c x < dist c b"
-proof -
- have *: "x - a \<in> open_segment 0 (b - a)" using assms
- by (metis diff_self open_segment_translation_eq uminus_add_conv_diff)
- show ?thesis
- using dist_decreases_open_segment_0 [OF *, of "c-a"] assms
- by (simp add: dist_norm)
-qed
-
-corollary open_segment_furthest_le:
- fixes a b x y :: "'a::euclidean_space"
- assumes "x \<in> open_segment a b"
- shows "norm (y - x) < norm (y - a) \<or> norm (y - x) < norm (y - b)"
- by (metis assms dist_decreases_open_segment dist_norm)
-
-corollary dist_decreases_closed_segment:
- fixes a :: "'a :: euclidean_space"
- assumes "x \<in> closed_segment a b"
- shows "dist c x \<le> dist c a \<or> dist c x \<le> dist c b"
-apply (cases "x \<in> open_segment a b")
- using dist_decreases_open_segment less_eq_real_def apply blast
-by (metis DiffI assms empty_iff insertE open_segment_def order_refl)
-
-lemma convex_intermediate_ball:
- fixes a :: "'a :: euclidean_space"
- shows "\<lbrakk>ball a r \<subseteq> T; T \<subseteq> cball a r\<rbrakk> \<Longrightarrow> convex T"
-apply (simp add: convex_contains_open_segment, clarify)
-by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment)
-
-lemma csegment_midpoint_subset: "closed_segment (midpoint a b) b \<subseteq> closed_segment a b"
- apply (clarsimp simp: midpoint_def in_segment)
- apply (rule_tac x="(1 + u) / 2" in exI)
- apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib)
- by (metis field_sum_of_halves scaleR_left.add)
-
-lemma notin_segment_midpoint:
- fixes a :: "'a :: euclidean_space"
- shows "a \<noteq> b \<Longrightarrow> a \<notin> closed_segment (midpoint a b) b"
-by (auto simp: dist_midpoint dest!: dist_in_closed_segment)
-
-lemma segment_to_closest_point:
- fixes S :: "'a :: euclidean_space set"
- shows "\<lbrakk>closed S; S \<noteq> {}\<rbrakk> \<Longrightarrow> open_segment a (closest_point S a) \<inter> S = {}"
- apply (subst disjoint_iff_not_equal)
- apply (clarify dest!: dist_in_open_segment)
- by (metis closest_point_le dist_commute le_less_trans less_irrefl)
-
-lemma segment_to_point_exists:
- fixes S :: "'a :: euclidean_space set"
- assumes "closed S" "S \<noteq> {}"
- obtains b where "b \<in> S" "open_segment a b \<inter> S = {}"
- by (metis assms segment_to_closest_point closest_point_exists that)
-
-subsubsection\<open>More lemmas, especially for working with the underlying formula\<close>
-
-lemma segment_eq_compose:
- fixes a :: "'a :: real_vector"
- shows "(\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) = (\<lambda>x. a + x) o (\<lambda>u. u *\<^sub>R (b - a))"
- by (simp add: o_def algebra_simps)
-
-lemma segment_degen_1:
- fixes a :: "'a :: real_vector"
- shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = b \<longleftrightarrow> a=b \<or> u=1"
-proof -
- { assume "(1 - u) *\<^sub>R a + u *\<^sub>R b = b"
- then have "(1 - u) *\<^sub>R a = (1 - u) *\<^sub>R b"
- by (simp add: algebra_simps)
- then have "a=b \<or> u=1"
- by simp
- } then show ?thesis
- by (auto simp: algebra_simps)
-qed
-
-lemma segment_degen_0:
- fixes a :: "'a :: real_vector"
- shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = a \<longleftrightarrow> a=b \<or> u=0"
- using segment_degen_1 [of "1-u" b a]
- by (auto simp: algebra_simps)
-
-lemma add_scaleR_degen:
- fixes a b ::"'a::real_vector"
- assumes "(u *\<^sub>R b + v *\<^sub>R a) = (u *\<^sub>R a + v *\<^sub>R b)" "u \<noteq> v"
- shows "a=b"
- by (metis (no_types, hide_lams) add.commute add_diff_eq diff_add_cancel real_vector.scale_cancel_left real_vector.scale_left_diff_distrib assms)
-
-lemma closed_segment_image_interval:
- "closed_segment a b = (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}"
- by (auto simp: set_eq_iff image_iff closed_segment_def)
-
-lemma open_segment_image_interval:
- "open_segment a b = (if a=b then {} else (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1})"
- by (auto simp: open_segment_def closed_segment_def segment_degen_0 segment_degen_1)
-
-lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval
-
-lemma open_segment_bound1:
- assumes "x \<in> open_segment a b"
- shows "norm (x - a) < norm (b - a)"
-proof -
- obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 < u" "u < 1" "a \<noteq> b"
- using assms by (auto simp add: open_segment_image_interval split: if_split_asm)
- then show "norm (x - a) < norm (b - a)"
- apply clarify
- apply (auto simp: algebra_simps)
- apply (simp add: scaleR_diff_right [symmetric])
- done
-qed
-
-lemma compact_segment [simp]:
- fixes a :: "'a::real_normed_vector"
- shows "compact (closed_segment a b)"
- by (auto simp: segment_image_interval intro!: compact_continuous_image continuous_intros)
-
-lemma closed_segment [simp]:
- fixes a :: "'a::real_normed_vector"
- shows "closed (closed_segment a b)"
- by (simp add: compact_imp_closed)
-
-lemma closure_closed_segment [simp]:
- fixes a :: "'a::real_normed_vector"
- shows "closure(closed_segment a b) = closed_segment a b"
- by simp
-
-lemma open_segment_bound:
- assumes "x \<in> open_segment a b"
- shows "norm (x - a) < norm (b - a)" "norm (x - b) < norm (b - a)"
-apply (simp add: assms open_segment_bound1)
-by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute)
-
-lemma closure_open_segment [simp]:
- "closure (open_segment a b) = (if a = b then {} else closed_segment a b)"
- for a :: "'a::euclidean_space"
-proof (cases "a = b")
- case True
- then show ?thesis
- by simp
-next
- case False
- have "closure ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1}) = (\<lambda>u. u *\<^sub>R (b - a)) ` closure {0<..<1}"
- apply (rule closure_injective_linear_image [symmetric])
- apply (use False in \<open>auto intro!: injI\<close>)
- done
- then have "closure
- ((\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1}) =
- (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b) ` closure {0<..<1}"
- using closure_translation [of a "((\<lambda>x. x *\<^sub>R b - x *\<^sub>R a) ` {0<..<1})"]
- by (simp add: segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right image_image)
- then show ?thesis
- by (simp add: segment_image_interval closure_greaterThanLessThan [symmetric] del: closure_greaterThanLessThan)
-qed
-
-lemma closed_open_segment_iff [simp]:
- fixes a :: "'a::euclidean_space" shows "closed(open_segment a b) \<longleftrightarrow> a = b"
- by (metis open_segment_def DiffE closure_eq closure_open_segment ends_in_segment(1) insert_iff segment_image_interval(2))
-
-lemma compact_open_segment_iff [simp]:
- fixes a :: "'a::euclidean_space" shows "compact(open_segment a b) \<longleftrightarrow> a = b"
- by (simp add: bounded_open_segment compact_eq_bounded_closed)
-
-lemma convex_closed_segment [iff]: "convex (closed_segment a b)"
- unfolding segment_convex_hull by(rule convex_convex_hull)
-
-lemma convex_open_segment [iff]: "convex (open_segment a b)"
-proof -
- have "convex ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})"
- by (rule convex_linear_image) auto
- then have "convex ((+) a ` (\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})"
- by (rule convex_translation)
- then show ?thesis
- by (simp add: image_image open_segment_image_interval segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right)
-qed
-
-lemmas convex_segment = convex_closed_segment convex_open_segment
-
-lemma connected_segment [iff]:
- fixes x :: "'a :: real_normed_vector"
- shows "connected (closed_segment x y)"
- by (simp add: convex_connected)
-
-lemma is_interval_closed_segment_1[intro, simp]: "is_interval (closed_segment a b)" for a b::real
- by (auto simp: is_interval_convex_1)
-
-lemma IVT'_closed_segment_real:
- fixes f :: "real \<Rightarrow> real"
- assumes "y \<in> closed_segment (f a) (f b)"
- assumes "continuous_on (closed_segment a b) f"
- shows "\<exists>x \<in> closed_segment a b. f x = y"
- using IVT'[of f a y b]
- IVT'[of "-f" a "-y" b]
- IVT'[of f b y a]
- IVT'[of "-f" b "-y" a] assms
- by (cases "a \<le> b"; cases "f b \<ge> f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus)
-
end
--- a/src/HOL/Analysis/Derivative.thy Mon Nov 04 17:06:18 2019 +0000
+++ b/src/HOL/Analysis/Derivative.thy Tue Nov 05 12:00:23 2019 +0000
@@ -7,11 +7,12 @@
theory Derivative
imports
- Convex_Euclidean_Space
+ Convex_Euclidean_Space
Abstract_Limits
Operator_Norm
Uniform_Limit
Bounded_Linear_Function
+ Line_Segment
begin
declare bounded_linear_inner_left [intro]
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Mon Nov 04 17:06:18 2019 +0000
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Tue Nov 05 12:00:23 2019 +0000
@@ -179,11 +179,21 @@
shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)"
by (auto simp: dist_real_def field_simps mem_cball)
+lemma cball_eq_atLeastAtMost:
+ fixes a b::real
+ shows "cball a b = {a - b .. a + b}"
+ by (auto simp: dist_real_def)
+
lemma greaterThanLessThan_eq_ball:
fixes a b::real
shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"
by (auto simp: dist_real_def field_simps mem_ball)
+lemma ball_eq_greaterThanLessThan:
+ fixes a b::real
+ shows "ball a b = {a - b <..< a + b}"
+ by (auto simp: dist_real_def)
+
lemma interior_ball [simp]: "interior (ball x e) = ball x e"
by (simp add: interior_open)
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon Nov 04 17:06:18 2019 +0000
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Tue Nov 05 12:00:23 2019 +0000
@@ -5,7 +5,13 @@
*)
theory Equivalence_Lebesgue_Henstock_Integration
- imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure Set_Integral Homeomorphism
+ imports
+ Lebesgue_Measure
+ Henstock_Kurzweil_Integration
+ Complete_Measure
+ Set_Integral
+ Homeomorphism
+ Cartesian_Euclidean_Space
begin
lemma le_left_mono: "x \<le> y \<Longrightarrow> y \<le> a \<longrightarrow> x \<le> (a::'a::preorder)"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Line_Segment.thy Tue Nov 05 12:00:23 2019 +0000
@@ -0,0 +1,1018 @@
+(* Title: HOL/Analysis/Line_Segment.thy
+ Author: L C Paulson, University of Cambridge
+ Author: Robert Himmelmann, TU Muenchen
+ Author: Bogdan Grechuk, University of Edinburgh
+ Author: Armin Heller, TU Muenchen
+ Author: Johannes Hoelzl, TU Muenchen
+*)
+
+section \<open>Line Segment\<close>
+
+theory Line_Segment
+imports
+ Convex
+ Topology_Euclidean_Space
+begin
+
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Topological Properties of Convex Sets and Functions\<close>
+
+lemma convex_supp_sum:
+ assumes "convex S" and 1: "supp_sum u I = 1"
+ and "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> u i \<and> (u i = 0 \<or> f i \<in> S)"
+ shows "supp_sum (\<lambda>i. u i *\<^sub>R f i) I \<in> S"
+proof -
+ have fin: "finite {i \<in> I. u i \<noteq> 0}"
+ using 1 sum.infinite by (force simp: supp_sum_def support_on_def)
+ then have eq: "supp_sum (\<lambda>i. u i *\<^sub>R f i) I = sum (\<lambda>i. u i *\<^sub>R f i) {i \<in> I. u i \<noteq> 0}"
+ by (force intro: sum.mono_neutral_left simp: supp_sum_def support_on_def)
+ show ?thesis
+ apply (simp add: eq)
+ apply (rule convex_sum [OF fin \<open>convex S\<close>])
+ using 1 assms apply (auto simp: supp_sum_def support_on_def)
+ done
+qed
+
+lemma closure_bounded_linear_image_subset:
+ assumes f: "bounded_linear f"
+ shows "f ` closure S \<subseteq> closure (f ` S)"
+ using linear_continuous_on [OF f] closed_closure closure_subset
+ by (rule image_closure_subset)
+
+lemma closure_linear_image_subset:
+ fixes f :: "'m::euclidean_space \<Rightarrow> 'n::real_normed_vector"
+ assumes "linear f"
+ shows "f ` (closure S) \<subseteq> closure (f ` S)"
+ using assms unfolding linear_conv_bounded_linear
+ by (rule closure_bounded_linear_image_subset)
+
+lemma closed_injective_linear_image:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes S: "closed S" and f: "linear f" "inj f"
+ shows "closed (f ` S)"
+proof -
+ obtain g where g: "linear g" "g \<circ> f = id"
+ using linear_injective_left_inverse [OF f] by blast
+ then have confg: "continuous_on (range f) g"
+ using linear_continuous_on linear_conv_bounded_linear by blast
+ have [simp]: "g ` f ` S = S"
+ using g by (simp add: image_comp)
+ have cgf: "closed (g ` f ` S)"
+ by (simp add: \<open>g \<circ> f = id\<close> S image_comp)
+ have [simp]: "(range f \<inter> g -` S) = f ` S"
+ using g unfolding o_def id_def image_def by auto metis+
+ show ?thesis
+ proof (rule closedin_closed_trans [of "range f"])
+ show "closedin (top_of_set (range f)) (f ` S)"
+ using continuous_closedin_preimage [OF confg cgf] by simp
+ show "closed (range f)"
+ apply (rule closed_injective_image_subspace)
+ using f apply (auto simp: linear_linear linear_injective_0)
+ done
+ qed
+qed
+
+lemma closed_injective_linear_image_eq:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes f: "linear f" "inj f"
+ shows "(closed(image f s) \<longleftrightarrow> closed s)"
+ by (metis closed_injective_linear_image closure_eq closure_linear_image_subset closure_subset_eq f(1) f(2) inj_image_subset_iff)
+
+lemma closure_injective_linear_image:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)"
+ apply (rule subset_antisym)
+ apply (simp add: closure_linear_image_subset)
+ by (simp add: closure_minimal closed_injective_linear_image closure_subset image_mono)
+
+lemma closure_bounded_linear_image:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "\<lbrakk>linear f; bounded S\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)"
+ apply (rule subset_antisym, simp add: closure_linear_image_subset)
+ apply (rule closure_minimal, simp add: closure_subset image_mono)
+ by (meson bounded_closure closed_closure compact_continuous_image compact_eq_bounded_closed linear_continuous_on linear_conv_bounded_linear)
+
+lemma closure_scaleR:
+ fixes S :: "'a::real_normed_vector set"
+ shows "((*\<^sub>R) c) ` (closure S) = closure (((*\<^sub>R) c) ` S)"
+proof
+ show "((*\<^sub>R) c) ` (closure S) \<subseteq> closure (((*\<^sub>R) c) ` S)"
+ using bounded_linear_scaleR_right
+ by (rule closure_bounded_linear_image_subset)
+ show "closure (((*\<^sub>R) c) ` S) \<subseteq> ((*\<^sub>R) c) ` (closure S)"
+ by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure)
+qed
+
+lemma sphere_eq_empty [simp]:
+ fixes a :: "'a::{real_normed_vector, perfect_space}"
+ shows "sphere a r = {} \<longleftrightarrow> r < 0"
+by (auto simp: sphere_def dist_norm) (metis dist_norm le_less_linear vector_choose_dist)
+
+lemma cone_closure:
+ fixes S :: "'a::real_normed_vector set"
+ assumes "cone S"
+ shows "cone (closure S)"
+proof (cases "S = {}")
+ case True
+ then show ?thesis by auto
+next
+ case False
+ then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)"
+ using cone_iff[of S] assms by auto
+ then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` closure S = closure S)"
+ using closure_subset by (auto simp: closure_scaleR)
+ then show ?thesis
+ using False cone_iff[of "closure S"] by auto
+qed
+
+
+corollary component_complement_connected:
+ fixes S :: "'a::real_normed_vector set"
+ assumes "connected S" "C \<in> components (-S)"
+ shows "connected(-C)"
+ using component_diff_connected [of S UNIV] assms
+ by (auto simp: Compl_eq_Diff_UNIV)
+
+proposition clopen:
+ fixes S :: "'a :: real_normed_vector set"
+ shows "closed S \<and> open S \<longleftrightarrow> S = {} \<or> S = UNIV"
+ by (force intro!: connected_UNIV [unfolded connected_clopen, rule_format])
+
+corollary compact_open:
+ fixes S :: "'a :: euclidean_space set"
+ shows "compact S \<and> open S \<longleftrightarrow> S = {}"
+ by (auto simp: compact_eq_bounded_closed clopen)
+
+corollary finite_imp_not_open:
+ fixes S :: "'a::{real_normed_vector, perfect_space} set"
+ shows "\<lbrakk>finite S; open S\<rbrakk> \<Longrightarrow> S={}"
+ using clopen [of S] finite_imp_closed not_bounded_UNIV by blast
+
+corollary empty_interior_finite:
+ fixes S :: "'a::{real_normed_vector, perfect_space} set"
+ shows "finite S \<Longrightarrow> interior S = {}"
+ by (metis interior_subset finite_subset open_interior [of S] finite_imp_not_open)
+
+text \<open>Balls, being convex, are connected.\<close>
+
+lemma convex_local_global_minimum:
+ fixes s :: "'a::real_normed_vector set"
+ assumes "e > 0"
+ and "convex_on s f"
+ and "ball x e \<subseteq> s"
+ and "\<forall>y\<in>ball x e. f x \<le> f y"
+ shows "\<forall>y\<in>s. f x \<le> f y"
+proof (rule ccontr)
+ have "x \<in> s" using assms(1,3) by auto
+ assume "\<not> ?thesis"
+ then obtain y where "y\<in>s" and y: "f x > f y" by auto
+ then have xy: "0 < dist x y" by auto
+ then obtain u where "0 < u" "u \<le> 1" and u: "u < e / dist x y"
+ using field_lbound_gt_zero[of 1 "e / dist x y"] xy \<open>e>0\<close> by auto
+ then have "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y"
+ using \<open>x\<in>s\<close> \<open>y\<in>s\<close>
+ using assms(2)[unfolded convex_on_def,
+ THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]]
+ by auto
+ moreover
+ have *: "x - ((1 - u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x - y)"
+ by (simp add: algebra_simps)
+ have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> ball x e"
+ unfolding mem_ball dist_norm
+ unfolding * and norm_scaleR and abs_of_pos[OF \<open>0<u\<close>]
+ unfolding dist_norm[symmetric]
+ using u
+ unfolding pos_less_divide_eq[OF xy]
+ by auto
+ then have "f x \<le> f ((1 - u) *\<^sub>R x + u *\<^sub>R y)"
+ using assms(4) by auto
+ ultimately show False
+ using mult_strict_left_mono[OF y \<open>u>0\<close>]
+ unfolding left_diff_distrib
+ by auto
+qed
+
+lemma convex_ball [iff]:
+ fixes x :: "'a::real_normed_vector"
+ shows "convex (ball x e)"
+proof (auto simp: convex_def)
+ fix y z
+ assume yz: "dist x y < e" "dist x z < e"
+ fix u v :: real
+ assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
+ have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
+ using uv yz
+ using convex_on_dist [of "ball x e" x, unfolded convex_on_def,
+ THEN bspec[where x=y], THEN bspec[where x=z]]
+ by auto
+ then show "dist x (u *\<^sub>R y + v *\<^sub>R z) < e"
+ using convex_bound_lt[OF yz uv] by auto
+qed
+
+lemma convex_cball [iff]:
+ fixes x :: "'a::real_normed_vector"
+ shows "convex (cball x e)"
+proof -
+ {
+ fix y z
+ assume yz: "dist x y \<le> e" "dist x z \<le> e"
+ fix u v :: real
+ assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
+ have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
+ using uv yz
+ using convex_on_dist [of "cball x e" x, unfolded convex_on_def,
+ THEN bspec[where x=y], THEN bspec[where x=z]]
+ by auto
+ then have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e"
+ using convex_bound_le[OF yz uv] by auto
+ }
+ then show ?thesis by (auto simp: convex_def Ball_def)
+qed
+
+lemma connected_ball [iff]:
+ fixes x :: "'a::real_normed_vector"
+ shows "connected (ball x e)"
+ using convex_connected convex_ball by auto
+
+lemma connected_cball [iff]:
+ fixes x :: "'a::real_normed_vector"
+ shows "connected (cball x e)"
+ using convex_connected convex_cball by auto
+
+lemma bounded_convex_hull:
+ fixes s :: "'a::real_normed_vector set"
+ assumes "bounded s"
+ shows "bounded (convex hull s)"
+proof -
+ from assms obtain B where B: "\<forall>x\<in>s. norm x \<le> B"
+ unfolding bounded_iff by auto
+ show ?thesis
+ apply (rule bounded_subset[OF bounded_cball, of _ 0 B])
+ unfolding subset_hull[of convex, OF convex_cball]
+ unfolding subset_eq mem_cball dist_norm using B
+ apply auto
+ done
+qed
+
+lemma finite_imp_bounded_convex_hull:
+ fixes s :: "'a::real_normed_vector set"
+ shows "finite s \<Longrightarrow> bounded (convex hull s)"
+ using bounded_convex_hull finite_imp_bounded
+ by auto
+
+
+section \<open>Line Segments\<close>
+
+subsection \<open>Midpoint\<close>
+
+definition\<^marker>\<open>tag important\<close> midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
+ where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
+
+lemma midpoint_idem [simp]: "midpoint x x = x"
+ unfolding midpoint_def by simp
+
+lemma midpoint_sym: "midpoint a b = midpoint b a"
+ unfolding midpoint_def by (auto simp add: scaleR_right_distrib)
+
+lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c"
+proof -
+ have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c"
+ by simp
+ then show ?thesis
+ unfolding midpoint_def scaleR_2 [symmetric] by simp
+qed
+
+lemma
+ fixes a::real
+ assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b"
+ and le_midpoint_1: "midpoint a b \<le> b"
+ by (simp_all add: midpoint_def assms)
+
+lemma dist_midpoint:
+ fixes a b :: "'a::real_normed_vector" shows
+ "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
+ "dist b (midpoint a b) = (dist a b) / 2" (is ?t2)
+ "dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
+ "dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
+proof -
+ have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2"
+ unfolding equation_minus_iff by auto
+ have **: "\<And>x y::'a. 2 *\<^sub>R x = y \<Longrightarrow> norm x = (norm y) / 2"
+ by auto
+ note scaleR_right_distrib [simp]
+ show ?t1
+ unfolding midpoint_def dist_norm
+ apply (rule **)
+ apply (simp add: scaleR_right_diff_distrib)
+ apply (simp add: scaleR_2)
+ done
+ show ?t2
+ unfolding midpoint_def dist_norm
+ apply (rule *)
+ apply (simp add: scaleR_right_diff_distrib)
+ apply (simp add: scaleR_2)
+ done
+ show ?t3
+ unfolding midpoint_def dist_norm
+ apply (rule *)
+ apply (simp add: scaleR_right_diff_distrib)
+ apply (simp add: scaleR_2)
+ done
+ show ?t4
+ unfolding midpoint_def dist_norm
+ apply (rule **)
+ apply (simp add: scaleR_right_diff_distrib)
+ apply (simp add: scaleR_2)
+ done
+qed
+
+lemma midpoint_eq_endpoint [simp]:
+ "midpoint a b = a \<longleftrightarrow> a = b"
+ "midpoint a b = b \<longleftrightarrow> a = b"
+ unfolding midpoint_eq_iff by auto
+
+lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b"
+ using midpoint_eq_iff by metis
+
+lemma midpoint_linear_image:
+ "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
+by (simp add: linear_iff midpoint_def)
+
+
+subsection \<open>Line segments\<close>
+
+definition\<^marker>\<open>tag important\<close> closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
+ where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
+
+definition\<^marker>\<open>tag important\<close> open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
+ "open_segment a b \<equiv> closed_segment a b - {a,b}"
+
+lemmas segment = open_segment_def closed_segment_def
+
+lemma in_segment:
+ "x \<in> closed_segment a b \<longleftrightarrow> (\<exists>u. 0 \<le> u \<and> u \<le> 1 \<and> x = (1 - u) *\<^sub>R a + u *\<^sub>R b)"
+ "x \<in> open_segment a b \<longleftrightarrow> a \<noteq> b \<and> (\<exists>u. 0 < u \<and> u < 1 \<and> x = (1 - u) *\<^sub>R a + u *\<^sub>R b)"
+ using less_eq_real_def by (auto simp: segment algebra_simps)
+
+lemma closed_segment_linear_image:
+ "closed_segment (f a) (f b) = f ` (closed_segment a b)" if "linear f"
+proof -
+ interpret linear f by fact
+ show ?thesis
+ by (force simp add: in_segment add scale)
+qed
+
+lemma open_segment_linear_image:
+ "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> open_segment (f a) (f b) = f ` (open_segment a b)"
+ by (force simp: open_segment_def closed_segment_linear_image inj_on_def)
+
+lemma closed_segment_translation:
+ "closed_segment (c + a) (c + b) = image (\<lambda>x. c + x) (closed_segment a b)"
+apply safe
+apply (rule_tac x="x-c" in image_eqI)
+apply (auto simp: in_segment algebra_simps)
+done
+
+lemma open_segment_translation:
+ "open_segment (c + a) (c + b) = image (\<lambda>x. c + x) (open_segment a b)"
+by (simp add: open_segment_def closed_segment_translation translation_diff)
+
+lemma closed_segment_of_real:
+ "closed_segment (of_real x) (of_real y) = of_real ` closed_segment x y"
+ apply (auto simp: image_iff in_segment scaleR_conv_of_real)
+ apply (rule_tac x="(1-u)*x + u*y" in bexI)
+ apply (auto simp: in_segment)
+ done
+
+lemma open_segment_of_real:
+ "open_segment (of_real x) (of_real y) = of_real ` open_segment x y"
+ apply (auto simp: image_iff in_segment scaleR_conv_of_real)
+ apply (rule_tac x="(1-u)*x + u*y" in bexI)
+ apply (auto simp: in_segment)
+ done
+
+lemma closed_segment_Reals:
+ "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> closed_segment x y = of_real ` closed_segment (Re x) (Re y)"
+ by (metis closed_segment_of_real of_real_Re)
+
+lemma open_segment_Reals:
+ "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> open_segment x y = of_real ` open_segment (Re x) (Re y)"
+ by (metis open_segment_of_real of_real_Re)
+
+lemma open_segment_PairD:
+ "(x, x') \<in> open_segment (a, a') (b, b')
+ \<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> a' = b')"
+ by (auto simp: in_segment)
+
+lemma closed_segment_PairD:
+ "(x, x') \<in> closed_segment (a, a') (b, b') \<Longrightarrow> x \<in> closed_segment a b \<and> x' \<in> closed_segment a' b'"
+ by (auto simp: closed_segment_def)
+
+lemma closed_segment_translation_eq [simp]:
+ "d + x \<in> closed_segment (d + a) (d + b) \<longleftrightarrow> x \<in> closed_segment a b"
+proof -
+ have *: "\<And>d x a b. x \<in> closed_segment a b \<Longrightarrow> d + x \<in> closed_segment (d + a) (d + b)"
+ apply (simp add: closed_segment_def)
+ apply (erule ex_forward)
+ apply (simp add: algebra_simps)
+ done
+ show ?thesis
+ using * [where d = "-d"] *
+ by (fastforce simp add:)
+qed
+
+lemma open_segment_translation_eq [simp]:
+ "d + x \<in> open_segment (d + a) (d + b) \<longleftrightarrow> x \<in> open_segment a b"
+ by (simp add: open_segment_def)
+
+lemma of_real_closed_segment [simp]:
+ "of_real x \<in> closed_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> closed_segment a b"
+ apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward)
+ using of_real_eq_iff by fastforce
+
+lemma of_real_open_segment [simp]:
+ "of_real x \<in> open_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> open_segment a b"
+ apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE)
+ using of_real_eq_iff by fastforce
+
+lemma convex_contains_segment:
+ "convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)"
+ unfolding convex_alt closed_segment_def by auto
+
+lemma closed_segment_in_Reals:
+ "\<lbrakk>x \<in> closed_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals"
+ by (meson subsetD convex_Reals convex_contains_segment)
+
+lemma open_segment_in_Reals:
+ "\<lbrakk>x \<in> open_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals"
+ by (metis Diff_iff closed_segment_in_Reals open_segment_def)
+
+lemma closed_segment_subset: "\<lbrakk>x \<in> S; y \<in> S; convex S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> S"
+ by (simp add: convex_contains_segment)
+
+lemma closed_segment_subset_convex_hull:
+ "\<lbrakk>x \<in> convex hull S; y \<in> convex hull S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull S"
+ using convex_contains_segment by blast
+
+lemma segment_convex_hull:
+ "closed_segment a b = convex hull {a,b}"
+proof -
+ have *: "\<And>x. {x} \<noteq> {}" by auto
+ show ?thesis
+ unfolding segment convex_hull_insert[OF *] convex_hull_singleton
+ by (safe; rule_tac x="1 - u" in exI; force)
+qed
+
+lemma open_closed_segment: "u \<in> open_segment w z \<Longrightarrow> u \<in> closed_segment w z"
+ by (auto simp add: closed_segment_def open_segment_def)
+
+lemma segment_open_subset_closed:
+ "open_segment a b \<subseteq> closed_segment a b"
+ by (auto simp: closed_segment_def open_segment_def)
+
+lemma bounded_closed_segment:
+ fixes a :: "'a::real_normed_vector" shows "bounded (closed_segment a b)"
+ by (rule boundedI[where B="max (norm a) (norm b)"])
+ (auto simp: closed_segment_def max_def convex_bound_le intro!: norm_triangle_le)
+
+lemma bounded_open_segment:
+ fixes a :: "'a::real_normed_vector" shows "bounded (open_segment a b)"
+ by (rule bounded_subset [OF bounded_closed_segment segment_open_subset_closed])
+
+lemmas bounded_segment = bounded_closed_segment open_closed_segment
+
+lemma ends_in_segment [iff]: "a \<in> closed_segment a b" "b \<in> closed_segment a b"
+ unfolding segment_convex_hull
+ by (auto intro!: hull_subset[unfolded subset_eq, rule_format])
+
+
+lemma eventually_closed_segment:
+ fixes x0::"'a::real_normed_vector"
+ assumes "open X0" "x0 \<in> X0"
+ shows "\<forall>\<^sub>F x in at x0 within U. closed_segment x0 x \<subseteq> X0"
+proof -
+ from openE[OF assms]
+ obtain e where e: "0 < e" "ball x0 e \<subseteq> X0" .
+ then have "\<forall>\<^sub>F x in at x0 within U. x \<in> ball x0 e"
+ by (auto simp: dist_commute eventually_at)
+ then show ?thesis
+ proof eventually_elim
+ case (elim x)
+ have "x0 \<in> ball x0 e" using \<open>e > 0\<close> by simp
+ from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim]
+ have "closed_segment x0 x \<subseteq> ball x0 e" .
+ also note \<open>\<dots> \<subseteq> X0\<close>
+ finally show ?case .
+ qed
+qed
+
+lemma closed_segment_commute: "closed_segment a b = closed_segment b a"
+proof -
+ have "{a, b} = {b, a}" by auto
+ thus ?thesis
+ by (simp add: segment_convex_hull)
+qed
+
+lemma segment_bound1:
+ assumes "x \<in> closed_segment a b"
+ shows "norm (x - a) \<le> norm (b - a)"
+proof -
+ obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1"
+ using assms by (auto simp add: closed_segment_def)
+ then show "norm (x - a) \<le> norm (b - a)"
+ apply clarify
+ apply (auto simp: algebra_simps)
+ apply (simp add: scaleR_diff_right [symmetric] mult_left_le_one_le)
+ done
+qed
+
+lemma segment_bound:
+ assumes "x \<in> closed_segment a b"
+ shows "norm (x - a) \<le> norm (b - a)" "norm (x - b) \<le> norm (b - a)"
+apply (simp add: assms segment_bound1)
+by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1)
+
+lemma open_segment_commute: "open_segment a b = open_segment b a"
+proof -
+ have "{a, b} = {b, a}" by auto
+ thus ?thesis
+ by (simp add: closed_segment_commute open_segment_def)
+qed
+
+lemma closed_segment_idem [simp]: "closed_segment a a = {a}"
+ unfolding segment by (auto simp add: algebra_simps)
+
+lemma open_segment_idem [simp]: "open_segment a a = {}"
+ by (simp add: open_segment_def)
+
+lemma closed_segment_eq_open: "closed_segment a b = open_segment a b \<union> {a,b}"
+ using open_segment_def by auto
+
+lemma convex_contains_open_segment:
+ "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. open_segment a b \<subseteq> s)"
+ by (simp add: convex_contains_segment closed_segment_eq_open)
+
+lemma closed_segment_eq_real_ivl1:
+ fixes a b::real
+ assumes "a \<le> b"
+ shows "closed_segment a b = {a .. b}"
+proof safe
+ fix x
+ assume "x \<in> closed_segment a b"
+ then obtain u where u: "0 \<le> u" "u \<le> 1" and x_def: "x = (1 - u) * a + u * b"
+ by (auto simp: closed_segment_def)
+ have "u * a \<le> u * b" "(1 - u) * a \<le> (1 - u) * b"
+ by (auto intro!: mult_left_mono u assms)
+ then show "x \<in> {a .. b}"
+ unfolding x_def by (auto simp: algebra_simps)
+qed (auto simp: closed_segment_def divide_simps algebra_simps
+ intro!: exI[where x="(x - a) / (b - a)" for x])
+
+lemma closed_segment_eq_real_ivl:
+ fixes a b::real
+ shows "closed_segment a b = (if a \<le> b then {a .. b} else {b .. a})"
+ using closed_segment_eq_real_ivl1[of a b] closed_segment_eq_real_ivl1[of b a]
+ by (auto simp: closed_segment_commute)
+
+lemma open_segment_eq_real_ivl:
+ fixes a b::real
+ shows "open_segment a b = (if a \<le> b then {a<..<b} else {b<..<a})"
+by (auto simp: closed_segment_eq_real_ivl open_segment_def split: if_split_asm)
+
+lemma closed_segment_real_eq:
+ fixes u::real shows "closed_segment u v = (\<lambda>x. (v - u) * x + u) ` {0..1}"
+ by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl)
+
+lemma dist_in_closed_segment:
+ fixes a :: "'a :: euclidean_space"
+ assumes "x \<in> closed_segment a b"
+ shows "dist x a \<le> dist a b \<and> dist x b \<le> dist a b"
+proof (intro conjI)
+ obtain u where u: "0 \<le> u" "u \<le> 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
+ using assms by (force simp: in_segment algebra_simps)
+ have "dist x a = u * dist a b"
+ apply (simp add: dist_norm algebra_simps x)
+ by (metis \<open>0 \<le> u\<close> abs_of_nonneg norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib)
+ also have "... \<le> dist a b"
+ by (simp add: mult_left_le_one_le u)
+ finally show "dist x a \<le> dist a b" .
+ have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)"
+ by (simp add: dist_norm algebra_simps x)
+ also have "... = (1-u) * dist a b"
+ proof -
+ have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
+ using \<open>u \<le> 1\<close> by force
+ then show ?thesis
+ by (simp add: dist_norm real_vector.scale_right_diff_distrib)
+ qed
+ also have "... \<le> dist a b"
+ by (simp add: mult_left_le_one_le u)
+ finally show "dist x b \<le> dist a b" .
+qed
+
+lemma dist_in_open_segment:
+ fixes a :: "'a :: euclidean_space"
+ assumes "x \<in> open_segment a b"
+ shows "dist x a < dist a b \<and> dist x b < dist a b"
+proof (intro conjI)
+ obtain u where u: "0 < u" "u < 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
+ using assms by (force simp: in_segment algebra_simps)
+ have "dist x a = u * dist a b"
+ apply (simp add: dist_norm algebra_simps x)
+ by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib \<open>0 < u\<close>)
+ also have *: "... < dist a b"
+ by (metis (no_types) assms dist_eq_0_iff dist_not_less_zero in_segment(2) linorder_neqE_linordered_idom mult.left_neutral real_mult_less_iff1 \<open>u < 1\<close>)
+ finally show "dist x a < dist a b" .
+ have ab_ne0: "dist a b \<noteq> 0"
+ using * by fastforce
+ have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)"
+ by (simp add: dist_norm algebra_simps x)
+ also have "... = (1-u) * dist a b"
+ proof -
+ have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
+ using \<open>u < 1\<close> by force
+ then show ?thesis
+ by (simp add: dist_norm real_vector.scale_right_diff_distrib)
+ qed
+ also have "... < dist a b"
+ using ab_ne0 \<open>0 < u\<close> by simp
+ finally show "dist x b < dist a b" .
+qed
+
+lemma dist_decreases_open_segment_0:
+ fixes x :: "'a :: euclidean_space"
+ assumes "x \<in> open_segment 0 b"
+ shows "dist c x < dist c 0 \<or> dist c x < dist c b"
+proof (rule ccontr, clarsimp simp: not_less)
+ obtain u where u: "0 \<noteq> b" "0 < u" "u < 1" and x: "x = u *\<^sub>R b"
+ using assms by (auto simp: in_segment)
+ have xb: "x \<bullet> b < b \<bullet> b"
+ using u x by auto
+ assume "norm c \<le> dist c x"
+ then have "c \<bullet> c \<le> (c - x) \<bullet> (c - x)"
+ by (simp add: dist_norm norm_le)
+ moreover have "0 < x \<bullet> b"
+ using u x by auto
+ ultimately have less: "c \<bullet> b < x \<bullet> b"
+ by (simp add: x algebra_simps inner_commute u)
+ assume "dist c b \<le> dist c x"
+ then have "(c - b) \<bullet> (c - b) \<le> (c - x) \<bullet> (c - x)"
+ by (simp add: dist_norm norm_le)
+ then have "(b \<bullet> b) * (1 - u*u) \<le> 2 * (b \<bullet> c) * (1-u)"
+ by (simp add: x algebra_simps inner_commute)
+ then have "(1+u) * (b \<bullet> b) * (1-u) \<le> 2 * (b \<bullet> c) * (1-u)"
+ by (simp add: algebra_simps)
+ then have "(1+u) * (b \<bullet> b) \<le> 2 * (b \<bullet> c)"
+ using \<open>u < 1\<close> by auto
+ with xb have "c \<bullet> b \<ge> x \<bullet> b"
+ by (auto simp: x algebra_simps inner_commute)
+ with less show False by auto
+qed
+
+proposition dist_decreases_open_segment:
+ fixes a :: "'a :: euclidean_space"
+ assumes "x \<in> open_segment a b"
+ shows "dist c x < dist c a \<or> dist c x < dist c b"
+proof -
+ have *: "x - a \<in> open_segment 0 (b - a)" using assms
+ by (metis diff_self open_segment_translation_eq uminus_add_conv_diff)
+ show ?thesis
+ using dist_decreases_open_segment_0 [OF *, of "c-a"] assms
+ by (simp add: dist_norm)
+qed
+
+corollary open_segment_furthest_le:
+ fixes a b x y :: "'a::euclidean_space"
+ assumes "x \<in> open_segment a b"
+ shows "norm (y - x) < norm (y - a) \<or> norm (y - x) < norm (y - b)"
+ by (metis assms dist_decreases_open_segment dist_norm)
+
+corollary dist_decreases_closed_segment:
+ fixes a :: "'a :: euclidean_space"
+ assumes "x \<in> closed_segment a b"
+ shows "dist c x \<le> dist c a \<or> dist c x \<le> dist c b"
+apply (cases "x \<in> open_segment a b")
+ using dist_decreases_open_segment less_eq_real_def apply blast
+by (metis DiffI assms empty_iff insertE open_segment_def order_refl)
+
+corollary segment_furthest_le:
+ fixes a b x y :: "'a::euclidean_space"
+ assumes "x \<in> closed_segment a b"
+ shows "norm (y - x) \<le> norm (y - a) \<or> norm (y - x) \<le> norm (y - b)"
+ by (metis assms dist_decreases_closed_segment dist_norm)
+
+lemma convex_intermediate_ball:
+ fixes a :: "'a :: euclidean_space"
+ shows "\<lbrakk>ball a r \<subseteq> T; T \<subseteq> cball a r\<rbrakk> \<Longrightarrow> convex T"
+apply (simp add: convex_contains_open_segment, clarify)
+by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment)
+
+lemma csegment_midpoint_subset: "closed_segment (midpoint a b) b \<subseteq> closed_segment a b"
+ apply (clarsimp simp: midpoint_def in_segment)
+ apply (rule_tac x="(1 + u) / 2" in exI)
+ apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib)
+ by (metis field_sum_of_halves scaleR_left.add)
+
+lemma notin_segment_midpoint:
+ fixes a :: "'a :: euclidean_space"
+ shows "a \<noteq> b \<Longrightarrow> a \<notin> closed_segment (midpoint a b) b"
+by (auto simp: dist_midpoint dest!: dist_in_closed_segment)
+
+subsubsection\<open>More lemmas, especially for working with the underlying formula\<close>
+
+lemma segment_eq_compose:
+ fixes a :: "'a :: real_vector"
+ shows "(\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) = (\<lambda>x. a + x) o (\<lambda>u. u *\<^sub>R (b - a))"
+ by (simp add: o_def algebra_simps)
+
+lemma segment_degen_1:
+ fixes a :: "'a :: real_vector"
+ shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = b \<longleftrightarrow> a=b \<or> u=1"
+proof -
+ { assume "(1 - u) *\<^sub>R a + u *\<^sub>R b = b"
+ then have "(1 - u) *\<^sub>R a = (1 - u) *\<^sub>R b"
+ by (simp add: algebra_simps)
+ then have "a=b \<or> u=1"
+ by simp
+ } then show ?thesis
+ by (auto simp: algebra_simps)
+qed
+
+lemma segment_degen_0:
+ fixes a :: "'a :: real_vector"
+ shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = a \<longleftrightarrow> a=b \<or> u=0"
+ using segment_degen_1 [of "1-u" b a]
+ by (auto simp: algebra_simps)
+
+lemma add_scaleR_degen:
+ fixes a b ::"'a::real_vector"
+ assumes "(u *\<^sub>R b + v *\<^sub>R a) = (u *\<^sub>R a + v *\<^sub>R b)" "u \<noteq> v"
+ shows "a=b"
+ by (metis (no_types, hide_lams) add.commute add_diff_eq diff_add_cancel real_vector.scale_cancel_left real_vector.scale_left_diff_distrib assms)
+
+lemma closed_segment_image_interval:
+ "closed_segment a b = (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}"
+ by (auto simp: set_eq_iff image_iff closed_segment_def)
+
+lemma open_segment_image_interval:
+ "open_segment a b = (if a=b then {} else (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1})"
+ by (auto simp: open_segment_def closed_segment_def segment_degen_0 segment_degen_1)
+
+lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval
+
+lemma open_segment_bound1:
+ assumes "x \<in> open_segment a b"
+ shows "norm (x - a) < norm (b - a)"
+proof -
+ obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 < u" "u < 1" "a \<noteq> b"
+ using assms by (auto simp add: open_segment_image_interval split: if_split_asm)
+ then show "norm (x - a) < norm (b - a)"
+ apply clarify
+ apply (auto simp: algebra_simps)
+ apply (simp add: scaleR_diff_right [symmetric])
+ done
+qed
+
+lemma compact_segment [simp]:
+ fixes a :: "'a::real_normed_vector"
+ shows "compact (closed_segment a b)"
+ by (auto simp: segment_image_interval intro!: compact_continuous_image continuous_intros)
+
+lemma closed_segment [simp]:
+ fixes a :: "'a::real_normed_vector"
+ shows "closed (closed_segment a b)"
+ by (simp add: compact_imp_closed)
+
+lemma closure_closed_segment [simp]:
+ fixes a :: "'a::real_normed_vector"
+ shows "closure(closed_segment a b) = closed_segment a b"
+ by simp
+
+lemma open_segment_bound:
+ assumes "x \<in> open_segment a b"
+ shows "norm (x - a) < norm (b - a)" "norm (x - b) < norm (b - a)"
+apply (simp add: assms open_segment_bound1)
+by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute)
+
+lemma closure_open_segment [simp]:
+ "closure (open_segment a b) = (if a = b then {} else closed_segment a b)"
+ for a :: "'a::euclidean_space"
+proof (cases "a = b")
+ case True
+ then show ?thesis
+ by simp
+next
+ case False
+ have "closure ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1}) = (\<lambda>u. u *\<^sub>R (b - a)) ` closure {0<..<1}"
+ apply (rule closure_injective_linear_image [symmetric])
+ apply (use False in \<open>auto intro!: injI\<close>)
+ done
+ then have "closure
+ ((\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1}) =
+ (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b) ` closure {0<..<1}"
+ using closure_translation [of a "((\<lambda>x. x *\<^sub>R b - x *\<^sub>R a) ` {0<..<1})"]
+ by (simp add: segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right image_image)
+ then show ?thesis
+ by (simp add: segment_image_interval closure_greaterThanLessThan [symmetric] del: closure_greaterThanLessThan)
+qed
+
+lemma closed_open_segment_iff [simp]:
+ fixes a :: "'a::euclidean_space" shows "closed(open_segment a b) \<longleftrightarrow> a = b"
+ by (metis open_segment_def DiffE closure_eq closure_open_segment ends_in_segment(1) insert_iff segment_image_interval(2))
+
+lemma compact_open_segment_iff [simp]:
+ fixes a :: "'a::euclidean_space" shows "compact(open_segment a b) \<longleftrightarrow> a = b"
+ by (simp add: bounded_open_segment compact_eq_bounded_closed)
+
+lemma convex_closed_segment [iff]: "convex (closed_segment a b)"
+ unfolding segment_convex_hull by(rule convex_convex_hull)
+
+lemma convex_open_segment [iff]: "convex (open_segment a b)"
+proof -
+ have "convex ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})"
+ by (rule convex_linear_image) auto
+ then have "convex ((+) a ` (\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})"
+ by (rule convex_translation)
+ then show ?thesis
+ by (simp add: image_image open_segment_image_interval segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right)
+qed
+
+lemmas convex_segment = convex_closed_segment convex_open_segment
+
+lemma connected_segment [iff]:
+ fixes x :: "'a :: real_normed_vector"
+ shows "connected (closed_segment x y)"
+ by (simp add: convex_connected)
+
+lemma is_interval_closed_segment_1[intro, simp]: "is_interval (closed_segment a b)" for a b::real
+ unfolding closed_segment_eq_real_ivl
+ by (auto simp: is_interval_def)
+
+lemma IVT'_closed_segment_real:
+ fixes f :: "real \<Rightarrow> real"
+ assumes "y \<in> closed_segment (f a) (f b)"
+ assumes "continuous_on (closed_segment a b) f"
+ shows "\<exists>x \<in> closed_segment a b. f x = y"
+ using IVT'[of f a y b]
+ IVT'[of "-f" a "-y" b]
+ IVT'[of f b y a]
+ IVT'[of "-f" b "-y" a] assms
+ by (cases "a \<le> b"; cases "f b \<ge> f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus)
+
+subsection \<open>Betweenness\<close>
+
+definition\<^marker>\<open>tag important\<close> "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
+
+lemma betweenI:
+ assumes "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
+ shows "between (a, b) x"
+using assms unfolding between_def closed_segment_def by auto
+
+lemma betweenE:
+ assumes "between (a, b) x"
+ obtains u where "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
+using assms unfolding between_def closed_segment_def by auto
+
+lemma between_implies_scaled_diff:
+ assumes "between (S, T) X" "between (S, T) Y" "S \<noteq> Y"
+ obtains c where "(X - Y) = c *\<^sub>R (S - Y)"
+proof -
+ from \<open>between (S, T) X\<close> obtain u\<^sub>X where X: "X = u\<^sub>X *\<^sub>R S + (1 - u\<^sub>X) *\<^sub>R T"
+ by (metis add.commute betweenE eq_diff_eq)
+ from \<open>between (S, T) Y\<close> obtain u\<^sub>Y where Y: "Y = u\<^sub>Y *\<^sub>R S + (1 - u\<^sub>Y) *\<^sub>R T"
+ by (metis add.commute betweenE eq_diff_eq)
+ have "X - Y = (u\<^sub>X - u\<^sub>Y) *\<^sub>R (S - T)"
+ proof -
+ from X Y have "X - Y = u\<^sub>X *\<^sub>R S - u\<^sub>Y *\<^sub>R S + ((1 - u\<^sub>X) *\<^sub>R T - (1 - u\<^sub>Y) *\<^sub>R T)" by simp
+ also have "\<dots> = (u\<^sub>X - u\<^sub>Y) *\<^sub>R S - (u\<^sub>X - u\<^sub>Y) *\<^sub>R T" by (simp add: scaleR_left.diff)
+ finally show ?thesis by (simp add: real_vector.scale_right_diff_distrib)
+ qed
+ moreover from Y have "S - Y = (1 - u\<^sub>Y) *\<^sub>R (S - T)"
+ by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
+ moreover note \<open>S \<noteq> Y\<close>
+ ultimately have "(X - Y) = ((u\<^sub>X - u\<^sub>Y) / (1 - u\<^sub>Y)) *\<^sub>R (S - Y)" by auto
+ from this that show thesis by blast
+qed
+
+lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
+ unfolding between_def by auto
+
+lemma between: "between (a, b) (x::'a::euclidean_space) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)"
+proof (cases "a = b")
+ case True
+ then show ?thesis
+ by (auto simp add: between_def dist_commute)
+next
+ case False
+ then have Fal: "norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0"
+ by auto
+ have *: "\<And>u. a - ((1 - u) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a - b)"
+ by (auto simp add: algebra_simps)
+ have "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)" if "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1" for u
+ proof -
+ have *: "a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)"
+ unfolding that(1) by (auto simp add:algebra_simps)
+ show "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)"
+ unfolding norm_minus_commute[of x a] * using \<open>0 \<le> u\<close> \<open>u \<le> 1\<close>
+ by simp
+ qed
+ moreover have "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" if "dist a b = dist a x + dist x b"
+ proof -
+ let ?\<beta> = "norm (a - x) / norm (a - b)"
+ show "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1"
+ proof (intro exI conjI)
+ show "?\<beta> \<le> 1"
+ using Fal2 unfolding that[unfolded dist_norm] norm_ge_zero by auto
+ show "x = (1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b"
+ proof (subst euclidean_eq_iff; intro ballI)
+ fix i :: 'a
+ assume i: "i \<in> Basis"
+ have "((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> i
+ = ((norm (a - b) - norm (a - x)) * (a \<bullet> i) + norm (a - x) * (b \<bullet> i)) / norm (a - b)"
+ using Fal by (auto simp add: field_simps inner_simps)
+ also have "\<dots> = x\<bullet>i"
+ apply (rule divide_eq_imp[OF Fal])
+ unfolding that[unfolded dist_norm]
+ using that[unfolded dist_triangle_eq] i
+ apply (subst (asm) euclidean_eq_iff)
+ apply (auto simp add: field_simps inner_simps)
+ done
+ finally show "x \<bullet> i = ((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> i"
+ by auto
+ qed
+ qed (use Fal2 in auto)
+ qed
+ ultimately show ?thesis
+ by (force simp add: between_def closed_segment_def dist_triangle_eq)
+qed
+
+lemma between_midpoint:
+ fixes a :: "'a::euclidean_space"
+ shows "between (a,b) (midpoint a b)" (is ?t1)
+ and "between (b,a) (midpoint a b)" (is ?t2)
+proof -
+ have *: "\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y"
+ by auto
+ show ?t1 ?t2
+ unfolding between midpoint_def dist_norm
+ by (auto simp add: field_simps inner_simps euclidean_eq_iff[where 'a='a] intro!: *)
+qed
+
+lemma between_mem_convex_hull:
+ "between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}"
+ unfolding between_mem_segment segment_convex_hull ..
+
+lemma between_triv_iff [simp]: "between (a,a) b \<longleftrightarrow> a=b"
+ by (auto simp: between_def)
+
+lemma between_triv1 [simp]: "between (a,b) a"
+ by (auto simp: between_def)
+
+lemma between_triv2 [simp]: "between (a,b) b"
+ by (auto simp: between_def)
+
+lemma between_commute:
+ "between (a,b) = between (b,a)"
+by (auto simp: between_def closed_segment_commute)
+
+lemma between_antisym:
+ fixes a :: "'a :: euclidean_space"
+ shows "\<lbrakk>between (b,c) a; between (a,c) b\<rbrakk> \<Longrightarrow> a = b"
+by (auto simp: between dist_commute)
+
+lemma between_trans:
+ fixes a :: "'a :: euclidean_space"
+ shows "\<lbrakk>between (b,c) a; between (a,c) d\<rbrakk> \<Longrightarrow> between (b,c) d"
+ using dist_triangle2 [of b c d] dist_triangle3 [of b d a]
+ by (auto simp: between dist_commute)
+
+lemma between_norm:
+ fixes a :: "'a :: euclidean_space"
+ shows "between (a,b) x \<longleftrightarrow> norm(x - a) *\<^sub>R (b - x) = norm(b - x) *\<^sub>R (x - a)"
+ by (auto simp: between dist_triangle_eq norm_minus_commute algebra_simps)
+
+lemma between_swap:
+ fixes A B X Y :: "'a::euclidean_space"
+ assumes "between (A, B) X"
+ assumes "between (A, B) Y"
+ shows "between (X, B) Y \<longleftrightarrow> between (A, Y) X"
+using assms by (auto simp add: between)
+
+lemma between_translation [simp]: "between (a + y,a + z) (a + x) \<longleftrightarrow> between (y,z) x"
+ by (auto simp: between_def)
+
+lemma between_trans_2:
+ fixes a :: "'a :: euclidean_space"
+ shows "\<lbrakk>between (b,c) a; between (a,b) d\<rbrakk> \<Longrightarrow> between (c,d) a"
+ by (metis between_commute between_swap between_trans)
+
+lemma between_scaleR_lift [simp]:
+ fixes v :: "'a::euclidean_space"
+ shows "between (a *\<^sub>R v, b *\<^sub>R v) (c *\<^sub>R v) \<longleftrightarrow> v = 0 \<or> between (a, b) c"
+ by (simp add: between dist_norm scaleR_left_diff_distrib [symmetric] distrib_right [symmetric])
+
+lemma between_1:
+ fixes x::real
+ shows "between (a,b) x \<longleftrightarrow> (a \<le> x \<and> x \<le> b) \<or> (b \<le> x \<and> x \<le> a)"
+ by (auto simp: between_mem_segment closed_segment_eq_real_ivl)
+
+end
\ No newline at end of file
--- a/src/HOL/Analysis/Multivariate_Analysis.thy Mon Nov 04 17:06:18 2019 +0000
+++ b/src/HOL/Analysis/Multivariate_Analysis.thy Tue Nov 05 12:00:23 2019 +0000
@@ -5,6 +5,7 @@
Determinants
Cross3
Lipschitz
+ Starlike
begin
text \<open>Entry point excluding integration and complex analysis.\<close>
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Mon Nov 04 17:06:18 2019 +0000
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Tue Nov 05 12:00:23 2019 +0000
@@ -2,7 +2,7 @@
theory Ordered_Euclidean_Space
imports
- Cartesian_Euclidean_Space Path_Connected
+ Convex_Euclidean_Space
"HOL-Library.Product_Order"
begin
@@ -205,11 +205,6 @@
and eucl_le_atLeast: "{x. \<forall>i\<in>Basis. a \<bullet> i <= x \<bullet> i} = {a..}"
by (auto simp: eucl_le[where 'a='a] eucl_less_def box_def cbox_def)
-lemma vec_nth_real_1_iff_cbox [simp]:
- fixes a b :: real
- shows "(\<lambda>x::real^1. x $ 1) ` S = {a..b} \<longleftrightarrow> S = cbox (vec a) (vec b)"
- by (metis interval_cbox vec_nth_1_iff_cbox)
-
lemma sums_vec_nth :
assumes "f sums a"
shows "(\<lambda>x. f x $ i) sums a $ i"
@@ -266,35 +261,6 @@
shows "connected {a..b}"
using is_interval_cc is_interval_connected by blast
-lemma path_connected_interval [simp]:
- fixes a b::"'a::ordered_euclidean_space"
- shows "path_connected {a..b}"
- using is_interval_cc is_interval_path_connected by blast
-
-lemma path_connected_Ioi[simp]: "path_connected {a<..}" for a :: real
- by (simp add: convex_imp_path_connected)
-
-lemma path_connected_Ici[simp]: "path_connected {a..}" for a :: real
- by (simp add: convex_imp_path_connected)
-
-lemma path_connected_Iio[simp]: "path_connected {..<a}" for a :: real
- by (simp add: convex_imp_path_connected)
-
-lemma path_connected_Iic[simp]: "path_connected {..a}" for a :: real
- by (simp add: convex_imp_path_connected)
-
-lemma path_connected_Ioo[simp]: "path_connected {a<..<b}" for a b :: real
- by (simp add: convex_imp_path_connected)
-
-lemma path_connected_Ioc[simp]: "path_connected {a<..b}" for a b :: real
- by (simp add: convex_imp_path_connected)
-
-lemma path_connected_Ico[simp]: "path_connected {a..<b}" for a b :: real
- by (simp add: convex_imp_path_connected)
-
-lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
- by (auto simp: real_atLeastGreaterThan_eq)
-
lemma compact_interval [simp]:
fixes a b::"'a::ordered_euclidean_space"
shows "compact {a .. b}"
--- a/src/HOL/Analysis/Path_Connected.thy Mon Nov 04 17:06:18 2019 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy Tue Nov 05 12:00:23 2019 +0000
@@ -1826,6 +1826,27 @@
lemma is_interval_path_connected: "is_interval S \<Longrightarrow> path_connected S"
by (simp add: convex_imp_path_connected is_interval_convex)
+lemma path_connected_Ioi[simp]: "path_connected {a<..}" for a :: real
+ by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Ici[simp]: "path_connected {a..}" for a :: real
+ by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Iio[simp]: "path_connected {..<a}" for a :: real
+ by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Iic[simp]: "path_connected {..a}" for a :: real
+ by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Ioo[simp]: "path_connected {a<..<b}" for a b :: real
+ by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Ioc[simp]: "path_connected {a<..b}" for a b :: real
+ by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Ico[simp]: "path_connected {a..<b}" for a b :: real
+ by (simp add: convex_imp_path_connected)
+
lemma path_connectedin_path_image:
assumes "pathin X g" shows "path_connectedin X (g ` ({0..1}))"
unfolding pathin_def
--- a/src/HOL/Analysis/Starlike.thy Mon Nov 04 17:06:18 2019 +0000
+++ b/src/HOL/Analysis/Starlike.thy Tue Nov 05 12:00:23 2019 +0000
@@ -8,7 +8,10 @@
chapter \<open>Unsorted\<close>
theory Starlike
-imports Convex_Euclidean_Space Abstract_Limits
+ imports
+ Convex_Euclidean_Space
+ Abstract_Limits
+ Line_Segment
begin
subsection\<open>Starlike sets\<close>
@@ -296,164 +299,6 @@
lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment
-subsection\<open>Betweenness\<close>
-
-definition\<^marker>\<open>tag important\<close> "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
-
-lemma betweenI:
- assumes "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
- shows "between (a, b) x"
-using assms unfolding between_def closed_segment_def by auto
-
-lemma betweenE:
- assumes "between (a, b) x"
- obtains u where "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
-using assms unfolding between_def closed_segment_def by auto
-
-lemma between_implies_scaled_diff:
- assumes "between (S, T) X" "between (S, T) Y" "S \<noteq> Y"
- obtains c where "(X - Y) = c *\<^sub>R (S - Y)"
-proof -
- from \<open>between (S, T) X\<close> obtain u\<^sub>X where X: "X = u\<^sub>X *\<^sub>R S + (1 - u\<^sub>X) *\<^sub>R T"
- by (metis add.commute betweenE eq_diff_eq)
- from \<open>between (S, T) Y\<close> obtain u\<^sub>Y where Y: "Y = u\<^sub>Y *\<^sub>R S + (1 - u\<^sub>Y) *\<^sub>R T"
- by (metis add.commute betweenE eq_diff_eq)
- have "X - Y = (u\<^sub>X - u\<^sub>Y) *\<^sub>R (S - T)"
- proof -
- from X Y have "X - Y = u\<^sub>X *\<^sub>R S - u\<^sub>Y *\<^sub>R S + ((1 - u\<^sub>X) *\<^sub>R T - (1 - u\<^sub>Y) *\<^sub>R T)" by simp
- also have "\<dots> = (u\<^sub>X - u\<^sub>Y) *\<^sub>R S - (u\<^sub>X - u\<^sub>Y) *\<^sub>R T" by (simp add: scaleR_left.diff)
- finally show ?thesis by (simp add: real_vector.scale_right_diff_distrib)
- qed
- moreover from Y have "S - Y = (1 - u\<^sub>Y) *\<^sub>R (S - T)"
- by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
- moreover note \<open>S \<noteq> Y\<close>
- ultimately have "(X - Y) = ((u\<^sub>X - u\<^sub>Y) / (1 - u\<^sub>Y)) *\<^sub>R (S - Y)" by auto
- from this that show thesis by blast
-qed
-
-lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
- unfolding between_def by auto
-
-lemma between: "between (a, b) (x::'a::euclidean_space) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)"
-proof (cases "a = b")
- case True
- then show ?thesis
- by (auto simp add: between_def dist_commute)
-next
- case False
- then have Fal: "norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0"
- by auto
- have *: "\<And>u. a - ((1 - u) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a - b)"
- by (auto simp add: algebra_simps)
- have "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)" if "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1" for u
- proof -
- have *: "a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)"
- unfolding that(1) by (auto simp add:algebra_simps)
- show "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)"
- unfolding norm_minus_commute[of x a] * using \<open>0 \<le> u\<close> \<open>u \<le> 1\<close>
- by simp
- qed
- moreover have "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" if "dist a b = dist a x + dist x b"
- proof -
- let ?\<beta> = "norm (a - x) / norm (a - b)"
- show "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1"
- proof (intro exI conjI)
- show "?\<beta> \<le> 1"
- using Fal2 unfolding that[unfolded dist_norm] norm_ge_zero by auto
- show "x = (1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b"
- proof (subst euclidean_eq_iff; intro ballI)
- fix i :: 'a
- assume i: "i \<in> Basis"
- have "((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> i
- = ((norm (a - b) - norm (a - x)) * (a \<bullet> i) + norm (a - x) * (b \<bullet> i)) / norm (a - b)"
- using Fal by (auto simp add: field_simps inner_simps)
- also have "\<dots> = x\<bullet>i"
- apply (rule divide_eq_imp[OF Fal])
- unfolding that[unfolded dist_norm]
- using that[unfolded dist_triangle_eq] i
- apply (subst (asm) euclidean_eq_iff)
- apply (auto simp add: field_simps inner_simps)
- done
- finally show "x \<bullet> i = ((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> i"
- by auto
- qed
- qed (use Fal2 in auto)
- qed
- ultimately show ?thesis
- by (force simp add: between_def closed_segment_def dist_triangle_eq)
-qed
-
-lemma between_midpoint:
- fixes a :: "'a::euclidean_space"
- shows "between (a,b) (midpoint a b)" (is ?t1)
- and "between (b,a) (midpoint a b)" (is ?t2)
-proof -
- have *: "\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y"
- by auto
- show ?t1 ?t2
- unfolding between midpoint_def dist_norm
- by (auto simp add: field_simps inner_simps euclidean_eq_iff[where 'a='a] intro!: *)
-qed
-
-lemma between_mem_convex_hull:
- "between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}"
- unfolding between_mem_segment segment_convex_hull ..
-
-lemma between_triv_iff [simp]: "between (a,a) b \<longleftrightarrow> a=b"
- by (auto simp: between_def)
-
-lemma between_triv1 [simp]: "between (a,b) a"
- by (auto simp: between_def)
-
-lemma between_triv2 [simp]: "between (a,b) b"
- by (auto simp: between_def)
-
-lemma between_commute:
- "between (a,b) = between (b,a)"
-by (auto simp: between_def closed_segment_commute)
-
-lemma between_antisym:
- fixes a :: "'a :: euclidean_space"
- shows "\<lbrakk>between (b,c) a; between (a,c) b\<rbrakk> \<Longrightarrow> a = b"
-by (auto simp: between dist_commute)
-
-lemma between_trans:
- fixes a :: "'a :: euclidean_space"
- shows "\<lbrakk>between (b,c) a; between (a,c) d\<rbrakk> \<Longrightarrow> between (b,c) d"
- using dist_triangle2 [of b c d] dist_triangle3 [of b d a]
- by (auto simp: between dist_commute)
-
-lemma between_norm:
- fixes a :: "'a :: euclidean_space"
- shows "between (a,b) x \<longleftrightarrow> norm(x - a) *\<^sub>R (b - x) = norm(b - x) *\<^sub>R (x - a)"
- by (auto simp: between dist_triangle_eq norm_minus_commute algebra_simps)
-
-lemma between_swap:
- fixes A B X Y :: "'a::euclidean_space"
- assumes "between (A, B) X"
- assumes "between (A, B) Y"
- shows "between (X, B) Y \<longleftrightarrow> between (A, Y) X"
-using assms by (auto simp add: between)
-
-lemma between_translation [simp]: "between (a + y,a + z) (a + x) \<longleftrightarrow> between (y,z) x"
- by (auto simp: between_def)
-
-lemma between_trans_2:
- fixes a :: "'a :: euclidean_space"
- shows "\<lbrakk>between (b,c) a; between (a,b) d\<rbrakk> \<Longrightarrow> between (c,d) a"
- by (metis between_commute between_swap between_trans)
-
-lemma between_scaleR_lift [simp]:
- fixes v :: "'a::euclidean_space"
- shows "between (a *\<^sub>R v, b *\<^sub>R v) (c *\<^sub>R v) \<longleftrightarrow> v = 0 \<or> between (a, b) c"
- by (simp add: between dist_norm scaleR_left_diff_distrib [symmetric] distrib_right [symmetric])
-
-lemma between_1:
- fixes x::real
- shows "between (a,b) x \<longleftrightarrow> (a \<le> x \<and> x \<le> b) \<or> (b \<le> x \<and> x \<le> a)"
- by (auto simp: between_mem_segment closed_segment_eq_real_ivl)
-
-
subsection\<^marker>\<open>tag unimportant\<close> \<open>Shrinking towards the interior of a convex set\<close>
lemma mem_interior_convex_shrink:
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Nov 04 17:06:18 2019 +0000
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Nov 05 12:00:23 2019 +0000
@@ -1120,6 +1120,12 @@
using is_interval_translation[of "-c" X]
by (metis image_cong uminus_add_conv_diff)
+lemma is_interval_cball_1[intro, simp]: "is_interval (cball a b)" for a b::real
+ by (simp add: cball_eq_atLeastAtMost is_interval_def)
+
+lemma is_interval_ball_real: "is_interval (ball a b)" for a b::real
+ by (simp add: ball_eq_greaterThanLessThan is_interval_def)
+
subsection\<^marker>\<open>tag unimportant\<close> \<open>Bounded Projections\<close>
@@ -1187,7 +1193,7 @@
shows "open {x. x <e a}" "open {x. a <e x}"
by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
-subsection\<^marker>\<open>tag unimportant\<close> \<open>Closure of halfspaces and hyperplanes\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Closure and Interior of halfspaces and hyperplanes\<close>
lemma continuous_at_inner: "continuous (at x) (inner a)"
unfolding continuous_at by (intro tendsto_intros)
@@ -1217,6 +1223,97 @@
shows "closed {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i}"
by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
+lemma interior_halfspace_le [simp]:
+ assumes "a \<noteq> 0"
+ shows "interior {x. a \<bullet> x \<le> b} = {x. a \<bullet> x < b}"
+proof -
+ have *: "a \<bullet> x < b" if x: "x \<in> S" and S: "S \<subseteq> {x. a \<bullet> x \<le> b}" and "open S" for S x
+ proof -
+ obtain e where "e>0" and e: "cball x e \<subseteq> S"
+ using \<open>open S\<close> open_contains_cball x by blast
+ then have "x + (e / norm a) *\<^sub>R a \<in> cball x e"
+ by (simp add: dist_norm)
+ then have "x + (e / norm a) *\<^sub>R a \<in> S"
+ using e by blast
+ then have "x + (e / norm a) *\<^sub>R a \<in> {x. a \<bullet> x \<le> b}"
+ using S by blast
+ moreover have "e * (a \<bullet> a) / norm a > 0"
+ by (simp add: \<open>0 < e\<close> assms)
+ ultimately show ?thesis
+ by (simp add: algebra_simps)
+ qed
+ show ?thesis
+ by (rule interior_unique) (auto simp: open_halfspace_lt *)
+qed
+
+lemma interior_halfspace_ge [simp]:
+ "a \<noteq> 0 \<Longrightarrow> interior {x. a \<bullet> x \<ge> b} = {x. a \<bullet> x > b}"
+using interior_halfspace_le [of "-a" "-b"] by simp
+
+lemma closure_halfspace_lt [simp]:
+ assumes "a \<noteq> 0"
+ shows "closure {x. a \<bullet> x < b} = {x. a \<bullet> x \<le> b}"
+proof -
+ have [simp]: "-{x. a \<bullet> x < b} = {x. a \<bullet> x \<ge> b}"
+ by (force simp:)
+ then show ?thesis
+ using interior_halfspace_ge [of a b] assms
+ by (force simp: closure_interior)
+qed
+
+lemma closure_halfspace_gt [simp]:
+ "a \<noteq> 0 \<Longrightarrow> closure {x. a \<bullet> x > b} = {x. a \<bullet> x \<ge> b}"
+using closure_halfspace_lt [of "-a" "-b"] by simp
+
+lemma interior_hyperplane [simp]:
+ assumes "a \<noteq> 0"
+ shows "interior {x. a \<bullet> x = b} = {}"
+proof -
+ have [simp]: "{x. a \<bullet> x = b} = {x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x \<ge> b}"
+ by (force simp:)
+ then show ?thesis
+ by (auto simp: assms)
+qed
+
+lemma frontier_halfspace_le:
+ assumes "a \<noteq> 0 \<or> b \<noteq> 0"
+ shows "frontier {x. a \<bullet> x \<le> b} = {x. a \<bullet> x = b}"
+proof (cases "a = 0")
+ case True with assms show ?thesis by simp
+next
+ case False then show ?thesis
+ by (force simp: frontier_def closed_halfspace_le)
+qed
+
+lemma frontier_halfspace_ge:
+ assumes "a \<noteq> 0 \<or> b \<noteq> 0"
+ shows "frontier {x. a \<bullet> x \<ge> b} = {x. a \<bullet> x = b}"
+proof (cases "a = 0")
+ case True with assms show ?thesis by simp
+next
+ case False then show ?thesis
+ by (force simp: frontier_def closed_halfspace_ge)
+qed
+
+lemma frontier_halfspace_lt:
+ assumes "a \<noteq> 0 \<or> b \<noteq> 0"
+ shows "frontier {x. a \<bullet> x < b} = {x. a \<bullet> x = b}"
+proof (cases "a = 0")
+ case True with assms show ?thesis by simp
+next
+ case False then show ?thesis
+ by (force simp: frontier_def interior_open open_halfspace_lt)
+qed
+
+lemma frontier_halfspace_gt:
+ assumes "a \<noteq> 0 \<or> b \<noteq> 0"
+ shows "frontier {x. a \<bullet> x > b} = {x. a \<bullet> x = b}"
+proof (cases "a = 0")
+ case True with assms show ?thesis by simp
+next
+ case False then show ?thesis
+ by (force simp: frontier_def interior_open open_halfspace_gt)
+qed
subsection\<^marker>\<open>tag unimportant\<close>\<open>Some more convenient intermediate-value theorem formulations\<close>
--- a/src/HOL/Proofs/ex/XML_Data.thy Mon Nov 04 17:06:18 2019 +0000
+++ b/src/HOL/Proofs/ex/XML_Data.thy Tue Nov 05 12:00:23 2019 +0000
@@ -12,10 +12,9 @@
subsection \<open>Export and re-import of global proof terms\<close>
ML \<open>
- fun export_proof thy thm =
- Proofterm.encode (Sign.consts_of thy)
- (Proofterm.reconstruct_proof thy (Thm.prop_of thm)
- (Thm.standard_proof_of {full = true, expand_name = Thm.expand_name thm} thm));
+ fun export_proof thy thm = thm
+ |> Thm.standard_proof_of {full = true, expand_name = Thm.expand_name thm}
+ |> Proofterm.encode (Sign.consts_of thy);
fun import_proof thy xml =
let
@@ -51,7 +50,9 @@
ML_val \<open>
val xml = export_proof thy1 @{thm abs_less_iff};
val thm = import_proof thy1 xml;
- \<^assert> (size (YXML.string_of_body xml) > 500000);
+
+ val xml_size = size (YXML.string_of_body xml);
+ \<^assert> (xml_size > 400000);
\<close>
end
--- a/src/Pure/Isar/class_declaration.ML Mon Nov 04 17:06:18 2019 +0000
+++ b/src/Pure/Isar/class_declaration.ML Tue Nov 05 12:00:23 2019 +0000
@@ -84,7 +84,6 @@
in
Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'')
(fn {context = ctxt, ...} => ALLGOALS (Proof_Context.fact_tac ctxt [thm'']))
- |> tap (Thm.expose_proof thy)
end;
val some_assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
@@ -103,9 +102,7 @@
REPEAT (SOMEGOAL
(match_tac ctxt (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
ORELSE' assume_tac ctxt));
- val of_class =
- Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context)
- |> tap (Thm.expose_proof thy);
+ val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context);
in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end;
--- a/src/Pure/Isar/element.ML Mon Nov 04 17:06:18 2019 +0000
+++ b/src/Pure/Isar/element.ML Tue Nov 05 12:00:23 2019 +0000
@@ -275,7 +275,7 @@
Witness (t,
Goal.prove ctxt [] [] (mark_witness t)
(fn _ => resolve_tac ctxt [Drule.protectI] 1 THEN tac)
- |> Thm.expose_derivation \<^here>);
+ |> Thm.close_derivation \<^here>);
local
@@ -290,7 +290,7 @@
(map o map) (fn prop => (mark_witness prop, [])) wit_propss @
[map (rpair []) eq_props];
fun after_qed' thmss =
- let val (wits, eqs) = split_last ((map o map) (Thm.expose_derivation \<^here>) thmss);
+ let val (wits, eqs) = split_last ((map o map) (Thm.close_derivation \<^here>) thmss);
in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
in proof after_qed' propss #> refine_witness end;
@@ -324,7 +324,7 @@
fun conclude_witness ctxt (Witness (_, th)) =
Goal.conclude th
|> Raw_Simplifier.norm_hhf_protect ctxt
- |> Thm.expose_derivation \<^here>;
+ |> Thm.close_derivation \<^here>;
fun pretty_witness ctxt witn =
let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in
--- a/src/Pure/Isar/expression.ML Mon Nov 04 17:06:18 2019 +0000
+++ b/src/Pure/Isar/expression.ML Tue Nov 05 12:00:23 2019 +0000
@@ -720,8 +720,7 @@
compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
compose_tac defs_ctxt
(false,
- Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1)
- |> tap (Thm.expose_proof defs_thy);
+ Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1);
val conjuncts =
(Drule.equal_elim_rule2 OF
@@ -753,13 +752,13 @@
val ((statement, intro, axioms), thy') =
thy
|> def_pred abinding parms defs' exts exts';
- val (_, thy'') =
+ val ((_, [intro']), thy'') =
thy'
|> Sign.qualified_path true abinding
|> Global_Theory.note_thms ""
((Binding.name introN, []), [([intro], [Locale.unfold_add])])
||> Sign.restore_naming thy';
- in (SOME statement, SOME intro, axioms, thy'') end;
+ in (SOME statement, SOME intro', axioms, thy'') end;
val (b_pred, b_intro, b_axioms, thy'''') =
if null ints then (NONE, NONE, [], thy'')
else
@@ -768,7 +767,7 @@
thy''
|> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
val ctxt''' = Proof_Context.init_global thy''';
- val (_, thy'''') =
+ val ([(_, [intro']), _], thy'''') =
thy'''
|> Sign.qualified_path true binding
|> Global_Theory.note_thmss ""
@@ -777,7 +776,7 @@
[(map (Drule.export_without_context o Element.conclude_witness ctxt''') axioms,
[])])]
||> Sign.restore_naming thy''';
- in (SOME statement, SOME intro, axioms, thy'''') end;
+ in (SOME statement, SOME intro', axioms, thy'''') end;
in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end;
end;
--- a/src/Pure/Isar/toplevel.ML Mon Nov 04 17:06:18 2019 +0000
+++ b/src/Pure/Isar/toplevel.ML Tue Nov 05 12:00:23 2019 +0000
@@ -294,7 +294,9 @@
let
val State ((node', pr_ctxt), _) =
node |> apply
- (fn _ => node_presentation (Theory (Context.Theory (Theory.end_theory thy))))
+ (fn _ =>
+ node_presentation
+ (Theory (Context.Theory (tap Thm.expose_theory (Theory.end_theory thy)))))
(K ());
in State ((Toplevel, pr_ctxt), get_theory node') end
| (Keep f, node) =>
--- a/src/Pure/PIDE/protocol.ML Mon Nov 04 17:06:18 2019 +0000
+++ b/src/Pure/PIDE/protocol.ML Tue Nov 05 12:00:23 2019 +0000
@@ -62,7 +62,8 @@
tokens = toks ~~ sources}
end;
-fun commands_accepted ids = Output.protocol_message Markup.commands_accepted [XML.Text (commas ids)];
+fun commands_accepted ids =
+ Output.protocol_message Markup.commands_accepted [XML.Text (space_implode "," ids)];
val _ =
Isabelle_Process.protocol_command "Document.define_command"
--- a/src/Pure/Thy/export_theory.ML Mon Nov 04 17:06:18 2019 +0000
+++ b/src/Pure/Thy/export_theory.ML Tue Nov 05 12:00:23 2019 +0000
@@ -275,9 +275,7 @@
else MinProof;
val (prop, SOME proof) =
standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0);
- val _ =
- if Proofterm.export_proof_boxes_required thy
- then Proofterm.export_proof_boxes [proof] else ();
+ val _ = Thm.expose_proofs thy [thm];
in
(prop, deps, proof) |>
let
--- a/src/Pure/global_theory.ML Mon Nov 04 17:06:18 2019 +0000
+++ b/src/Pure/global_theory.ML Tue Nov 05 12:00:23 2019 +0000
@@ -288,11 +288,7 @@
fold_map (Thm.theory_attributes atts) (map (Thm.transfer thy) thms) thy);
fun apply_facts name_flags1 name_flags2 (b, facts) thy =
- if Binding.is_empty b then
- let
- val (thms, thy') = app_facts facts thy;
- val _ = Thm.expose_proofs thy' thms;
- in register_proofs thms thy' end
+ if Binding.is_empty b then app_facts facts thy |-> register_proofs
else
let
val name_pos = bind_name thy b;
--- a/src/Pure/more_thm.ML Mon Nov 04 17:06:18 2019 +0000
+++ b/src/Pure/more_thm.ML Tue Nov 05 12:00:23 2019 +0000
@@ -118,6 +118,7 @@
thm -> Proofterm.proof
val register_proofs: thm list lazy -> theory -> theory
val consolidate_theory: theory -> unit
+ val expose_theory: theory -> unit
val show_consts: bool Config.T
val show_hyps: bool Config.T
val show_tags: bool Config.T
@@ -681,10 +682,13 @@
fun register_proofs ths =
(Proofs.map o cons) (Lazy.map_finished (map Thm.trim_context) ths);
-fun consolidate_theory thy =
- rev (Proofs.get thy)
- |> maps (map (Thm.transfer thy) o Lazy.force)
- |> Thm.consolidate;
+fun force_proofs thy = rev (Proofs.get thy) |> maps (map (Thm.transfer thy) o Lazy.force);
+
+val consolidate_theory = Thm.consolidate o force_proofs;
+
+fun expose_theory thy =
+ if Proofterm.export_enabled ()
+ then Thm.expose_proofs thy (force_proofs thy) else ();
--- a/src/Pure/proofterm.ML Mon Nov 04 17:06:18 2019 +0000
+++ b/src/Pure/proofterm.ML Tue Nov 05 12:00:23 2019 +0000
@@ -46,7 +46,6 @@
val thm_node_body: thm_node -> proof_body future
val thm_node_thms: thm_node -> thm list
val join_thms: thm list -> proof_body list
- val consolidate: proof_body list -> unit
val make_thm: thm_header -> thm_body -> thm
val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
val fold_body_thms:
@@ -176,7 +175,7 @@
val export_enabled: unit -> bool
val export_standard_enabled: unit -> bool
val export_proof_boxes_required: theory -> bool
- val export_proof_boxes: proof list -> unit
+ val export_proof_boxes: proof_body list -> unit
val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
val thm_proof: theory -> (class * class -> proof) ->
(string * class list list * class -> proof) -> string * Position.T -> sort list ->
@@ -223,10 +222,10 @@
thms: (serial * thm_node) Ord_List.T,
proof: proof}
and thm_body =
- Thm_Body of {export_proof: unit lazy, open_proof: proof -> proof, body: proof_body future}
+ Thm_Body of {open_proof: proof -> proof, body: proof_body future}
and thm_node =
Thm_Node of {theory_name: string, name: string, prop: term,
- body: proof_body future, consolidate: unit lazy};
+ body: proof_body future, export: unit lazy, consolidate: unit lazy};
type oracle = string * term option;
val oracle_ord = prod_ord fast_string_ord (option_ord Term_Ord.fast_term_ord);
@@ -246,11 +245,7 @@
fun thm_header serial pos theory_name name prop types : thm_header =
{serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types};
-val no_export_proof = Lazy.value ();
-
-fun thm_body body =
- Thm_Body {export_proof = no_export_proof, open_proof = I, body = Future.value body};
-fun thm_body_export_proof (Thm_Body {export_proof, ...}) = export_proof;
+fun thm_body body = Thm_Body {open_proof = I, body = Future.value body};
fun thm_body_proof_raw (Thm_Body {body, ...}) = join_proof body;
fun thm_body_proof_open (Thm_Body {open_proof, body, ...}) = open_proof (join_proof body);
@@ -260,24 +255,31 @@
val thm_node_prop = #prop o rep_thm_node;
val thm_node_body = #body o rep_thm_node;
val thm_node_thms = thm_node_body #> Future.join #> (fn PBody {thms, ...} => thms);
+val thm_node_export = #export o rep_thm_node;
val thm_node_consolidate = #consolidate o rep_thm_node;
fun join_thms (thms: thm list) =
Future.joins (map (thm_node_body o #2) thms);
-val consolidate =
+val consolidate_bodies =
maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
#> Lazy.consolidate #> map Lazy.force #> ignore;
-fun make_thm_node theory_name name prop body =
- Thm_Node {theory_name = theory_name, name = name, prop = prop, body = body,
- consolidate =
+fun make_thm_node theory_name name prop body export =
+ let
+ val consolidate =
Lazy.lazy_name "Proofterm.make_thm_node" (fn () =>
let val PBody {thms, ...} = Future.join body
- in consolidate (join_thms thms) end)};
+ in consolidate_bodies (join_thms thms) end);
+ in
+ Thm_Node {theory_name = theory_name, name = name, prop = prop, body = body,
+ export = export, consolidate = consolidate}
+ end;
+
+val no_export = Lazy.value ();
fun make_thm ({serial, theory_name, name, prop, ...}: thm_header) (Thm_Body {body, ...}) =
- (serial, make_thm_node theory_name name prop body);
+ (serial, make_thm_node theory_name name prop body no_export);
(* proof atoms *)
@@ -339,10 +341,10 @@
| no_body_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_body_proofs prf)
| no_body_proofs (prf % t) = no_body_proofs prf % t
| no_body_proofs (prf1 %% prf2) = no_body_proofs prf1 %% no_body_proofs prf2
- | no_body_proofs (PThm (header, Thm_Body {export_proof, open_proof, body})) =
+ | no_body_proofs (PThm (header, Thm_Body {open_proof, body})) =
let
val body' = Future.value (no_proof_body (join_proof body));
- val thm_body' = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'};
+ val thm_body' = Thm_Body {open_proof = open_proof, body = body'};
in PThm (header, thm_body') end
| no_body_proofs a = a;
@@ -443,7 +445,7 @@
let
val (a, (b, (c, (d, e)))) =
pair int (pair string (pair string (pair (term consts) (proof_body consts)))) x
- in (a, make_thm_node b c d (Future.value e)) end;
+ in (a, make_thm_node b c d (Future.value e) no_export) end;
in
@@ -1959,7 +1961,7 @@
fun fulfill_norm_proof thy ps body0 =
let
- val _ = consolidate (map #2 ps @ [body0]);
+ val _ = consolidate_bodies (map #2 ps @ [body0]);
val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
val oracles =
unions_oracles
@@ -2090,6 +2092,11 @@
(* PThm nodes *)
+fun prune_body body =
+ if Options.default_bool "prune_proofs"
+ then (Future.map o map_proof_of) (K MinProof) body
+ else body;
+
fun export_enabled () = Options.default_bool "export_proofs";
fun export_standard_enabled () = Options.default_bool "export_standard_proofs";
@@ -2097,24 +2104,19 @@
Context.theory_name thy = Context.PureN orelse
(export_enabled () andalso not (export_standard_enabled ()));
-fun export_proof_boxes proofs =
+fun export_proof_boxes bodies =
let
- fun export_boxes (AbsP (_, _, prf)) = export_boxes prf
- | export_boxes (Abst (_, _, prf)) = export_boxes prf
- | export_boxes (prf1 %% prf2) = export_boxes prf1 #> export_boxes prf2
- | export_boxes (prf % _) = export_boxes prf
- | export_boxes (PThm ({serial = i, ...}, thm_body)) =
- (fn boxes =>
- if Inttab.defined boxes i then boxes
- else
- let
- val prf' = thm_body_proof_raw thm_body;
- val export = thm_body_export_proof thm_body;
- val boxes' = Inttab.update (i, export) boxes;
- in export_boxes prf' boxes' end)
- | export_boxes _ = I;
- val boxes = (proofs, Inttab.empty) |-> fold export_boxes |> Inttab.dest;
- in List.app (Lazy.force o #2) boxes end;
+ fun export_thm (i, thm_node) boxes =
+ if Inttab.defined boxes i then boxes
+ else
+ boxes
+ |> Inttab.update (i, thm_node_export thm_node)
+ |> fold export_thm (thm_node_thms thm_node);
+
+ fun export_body (PBody {thms, ...}) = fold export_thm thms;
+
+ val exports = (bodies, Inttab.empty) |-> fold export_body |> Inttab.dest;
+ in List.app (Lazy.force o #2) exports end;
local
@@ -2160,18 +2162,6 @@
strict = false} xml
end;
-fun export thy i prop prf =
- if export_enabled () then
- let
- val _ = export_proof_boxes [prf];
- val _ = export_proof thy i prop prf;
- in () end
- else ();
-
-fun prune proof =
- if Options.default_bool "prune_proofs" then MinProof
- else proof;
-
fun prepare_thm_proof unconstrain thy classrel_proof arity_proof
(name, pos) shyps hyps concl promises body =
let
@@ -2188,45 +2178,46 @@
(PBody {oracles = oracles0, thms = thms0,
proof = if proofs_enabled () then fold_rev implies_intr_proof hyps prf else MinProof});
- fun publish i = map_proof_of (rew_proof thy #> tap (export thy i prop1) #> prune);
- val open_proof = not named ? rew_proof thy;
-
fun new_prf () =
let
val i = serial ();
val unconstrainT =
unconstrainT_proof (Sign.classes_of thy) classrel_proof arity_proof ucontext;
- val postproc = map_proof_of unconstrainT #> named ? publish i;
+ val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy);
in (i, fulfill_proof_future thy promises postproc body0) end;
val (i, body') =
- (*non-deterministic, depends on unknown promises*)
- (case strip_combt (fst (strip_combP prf)) of
- (PThm ({serial = ser, name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
- if (a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then
- let
- val Thm_Body {body = body', ...} = thm_body';
- val i = if a = "" andalso named then serial () else ser;
- in (i, body' |> ser <> i ? Future.map (publish i)) end
- else new_prf ()
- | _ => new_prf ());
+ (*somewhat non-deterministic proof boxes!*)
+ if export_enabled () then new_prf ()
+ else
+ (case strip_combt (fst (strip_combP prf)) of
+ (PThm ({serial = ser, name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
+ if (a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then
+ let
+ val Thm_Body {body = body', ...} = thm_body';
+ val i = if a = "" andalso named then serial () else ser;
+ in (i, body' |> ser <> i ? Future.map (map_proof_of (rew_proof thy))) end
+ else new_prf ()
+ | _ => new_prf ());
- val export_proof =
- if named orelse not (export_enabled ()) then no_export_proof
- else
+ val open_proof = not named ? rew_proof thy;
+
+ val export =
+ if export_enabled () then
Lazy.lazy (fn () =>
join_proof body' |> open_proof |> export_proof thy i prop1 handle exn =>
if Exn.is_interrupt exn then
raise Fail ("Interrupt: potential resource problems while exporting proof " ^
string_of_int i)
- else Exn.reraise exn);
+ else Exn.reraise exn)
+ else no_export;
+ val thm_body = prune_body body';
val theory_name = Context.theory_long_name thy;
- val thm = (i, make_thm_node theory_name name prop1 body');
+ val thm = (i, make_thm_node theory_name name prop1 thm_body export);
val header = thm_header i ([pos, Position.thread_data ()]) theory_name name prop1 NONE;
- val thm_body = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'};
- val head = PThm (header, thm_body);
+ val head = PThm (header, Thm_Body {open_proof = open_proof, body = thm_body});
val proof =
if unconstrain then
proof_combt' (head, (map o Option.map o Term.map_types) (#map_atyps ucontext) args)
--- a/src/Pure/thm.ML Mon Nov 04 17:06:18 2019 +0000
+++ b/src/Pure/thm.ML Tue Nov 05 12:00:23 2019 +0000
@@ -113,7 +113,6 @@
val expand_name: thm -> Proofterm.thm_header -> string option
val name_derivation: string * Position.T -> thm -> thm
val close_derivation: Position.T -> thm -> thm
- val expose_derivation: Position.T -> thm -> thm
val trim_context: thm -> thm
val axiom: theory -> string -> thm
val all_axioms_of: theory -> (string * thm) list
@@ -765,7 +764,7 @@
fun expose_proofs thy thms =
if Proofterm.export_proof_boxes_required thy then
- Proofterm.export_proof_boxes (map (proof_of o transfer thy) thms)
+ Proofterm.export_proof_boxes (proof_bodies_of (map (transfer thy) thms))
else ();
fun expose_proof thy = expose_proofs thy o single;
@@ -1044,10 +1043,6 @@
if not (null (tpairs_of thm)) orelse derivation_closed thm then thm
else name_derivation ("", pos) thm);
-fun expose_derivation pos thm =
- close_derivation pos thm
- |> tap (expose_proof (theory_of_thm thm));
-
val trim_context = solve_constraints #> trim_context_thm;
@@ -2253,7 +2248,8 @@
|> (map_classrels o Symreltab.update) ((c1, c2),
(the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
|> standard_tvars
- |> expose_derivation \<^here>
+ |> close_derivation \<^here>
+ |> tap (expose_proof thy2)
|> trim_context));
val proven = is_classrel thy1;
@@ -2286,7 +2282,8 @@
val th1 =
(th RS the_classrel thy (c, c1))
|> standard_tvars
- |> expose_derivation \<^here>
+ |> close_derivation \<^here>
+ |> tap (expose_proof thy)
|> trim_context;
in SOME ((t, Ss, c1), (th1, thy_name, ser)) end);
val finished' = finished andalso null completions;