--- a/src/HOL/Finite_Set.thy Mon Mar 14 12:31:05 2016 +0100
+++ b/src/HOL/Finite_Set.thy Mon Mar 14 14:25:11 2016 +0000
@@ -291,6 +291,11 @@
then show "finite A" by simp
qed
+lemma finite_image_iff:
+ assumes "inj_on f A"
+ shows "finite (f ` A) \<longleftrightarrow> finite A"
+using assms finite_imageD by blast
+
lemma finite_surj:
"finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> finite B"
by (erule finite_subset) (rule finite_imageI)
--- a/src/HOL/Fun.thy Mon Mar 14 12:31:05 2016 +0100
+++ b/src/HOL/Fun.thy Mon Mar 14 14:25:11 2016 +0000
@@ -210,7 +210,7 @@
lemma bij_id[simp]: "bij id"
by (simp add: bij_betw_def)
-lemma inj_onI:
+lemma inj_onI [intro?]:
"(!! x y. [| x:A; y:A; f(x) = f(y) |] ==> x=y) ==> inj_on f A"
by (simp add: inj_on_def)
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Mar 14 12:31:05 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Mar 14 14:25:11 2016 +0000
@@ -1175,12 +1175,6 @@
lemma Im_linepath: "Im(linepath (of_real a) (of_real b) x) = 0"
by (simp add: linepath_def)
-lemma linepath_of_real: "(linepath (of_real a) (of_real b) x) = of_real ((1 - x)*a + x*b)"
- by (simp add: scaleR_conv_of_real linepath_def)
-
-lemma of_real_linepath: "of_real (linepath a b x) = linepath (of_real a) (of_real b) x"
- by (metis linepath_of_real mult.right_neutral of_real_def real_scaleR_def)
-
lemma has_contour_integral_trivial [iff]: "(f has_contour_integral 0) (linepath a a)"
by (simp add: has_contour_integral_linepath)
@@ -1351,42 +1345,6 @@
by (simp add: contour_integral_def integral_def has_contour_integral contour_integrable_on)
-subsection\<open>Segments via convex hulls\<close>
-
-lemma segments_subset_convex_hull:
- "closed_segment a b \<subseteq> (convex hull {a,b,c})"
- "closed_segment a c \<subseteq> (convex hull {a,b,c})"
- "closed_segment b c \<subseteq> (convex hull {a,b,c})"
- "closed_segment b a \<subseteq> (convex hull {a,b,c})"
- "closed_segment c a \<subseteq> (convex hull {a,b,c})"
- "closed_segment c b \<subseteq> (convex hull {a,b,c})"
-by (auto simp: segment_convex_hull linepath_of_real elim!: rev_subsetD [OF _ hull_mono])
-
-lemma midpoints_in_convex_hull:
- assumes "x \<in> convex hull s" "y \<in> convex hull s"
- shows "midpoint x y \<in> convex hull s"
-proof -
- have "(1 - inverse(2)) *\<^sub>R x + inverse(2) *\<^sub>R y \<in> convex hull s"
- apply (rule convexD_alt)
- using assms
- apply (auto simp: convex_convex_hull)
- done
- then show ?thesis
- by (simp add: midpoint_def algebra_simps)
-qed
-
-lemma convex_hull_subset:
- "s \<subseteq> convex hull t \<Longrightarrow> convex hull s \<subseteq> convex hull t"
- by (simp add: convex_convex_hull subset_hull)
-
-lemma not_in_interior_convex_hull_3:
- fixes a :: "complex"
- shows "a \<notin> interior(convex hull {a,b,c})"
- "b \<notin> interior(convex hull {a,b,c})"
- "c \<notin> interior(convex hull {a,b,c})"
- by (auto simp: card_insert_le_m1 not_in_interior_convex_hull)
-
-
text\<open>Cauchy's theorem where there's a primitive\<close>
lemma contour_integral_primitive_lemma:
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Mar 14 12:31:05 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Mar 14 14:25:11 2016 +0000
@@ -324,6 +324,16 @@
shows "scaleR 2 x = x + x"
unfolding one_add_one [symmetric] scaleR_left_distrib by simp
+lemma scaleR_half_double [simp]:
+ fixes a :: "'a::real_normed_vector"
+ shows "(1 / 2) *\<^sub>R (a + a) = a"
+proof -
+ have "\<And>r. r *\<^sub>R (a + a) = (r * 2) *\<^sub>R a"
+ by (metis scaleR_2 scaleR_scaleR)
+ then show ?thesis
+ by simp
+qed
+
lemma vector_choose_size:
assumes "0 \<le> c"
obtains x :: "'a::{real_normed_vector, perfect_space}" where "norm x = c"
@@ -5759,7 +5769,7 @@
shows "is_interval s \<Longrightarrow> connected s"
using is_interval_convex convex_connected by auto
-lemma convex_box: "convex (cbox a b)" "convex (box a (b::'a::euclidean_space))"
+lemma convex_box [simp]: "convex (cbox a b)" "convex (box a (b::'a::euclidean_space))"
apply (rule_tac[!] is_interval_convex)+
using is_interval_box is_interval_cbox
apply auto
@@ -6573,15 +6583,12 @@
lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval
-lemma open_segment_eq: "open_segment a b = (if a=b then {} else {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 < u \<and> u < 1})"
- by (auto simp: open_segment_def closed_segment_def segment_degen_0 segment_degen_1)
-
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_eq split: if_split_asm)
+ 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)
@@ -6657,7 +6664,21 @@
shows "affine hull (open_segment a b) = (if a = b then {} else affine hull {a,b})"
by (metis affine_hull_convex_hull affine_hull_empty closure_open_segment closure_same_affine_hull segment_convex_hull)
-subsubsection\<open>Betweenness\<close>
+lemma rel_interior_closure_convex_segment:
+ fixes S :: "_::euclidean_space set"
+ assumes "convex S" "a \<in> rel_interior S" "b \<in> closure S"
+ shows "open_segment a b \<subseteq> rel_interior S"
+proof
+ fix x
+ have [simp]: "(1 - u) *\<^sub>R a + u *\<^sub>R b = b - (1 - u) *\<^sub>R (b - a)" for u
+ by (simp add: algebra_simps)
+ assume "x \<in> open_segment a b"
+ then show "x \<in> rel_interior S"
+ unfolding closed_segment_def open_segment_def using assms
+ by (auto intro: rel_interior_closure_convex_shrink)
+qed
+
+subsection\<open>Betweenness\<close>
lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
unfolding between_def by auto
--- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Mar 14 12:31:05 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Mar 14 14:25:11 2016 +0000
@@ -1193,13 +1193,8 @@
show ?thesis
proof (cases "cbox a b \<inter> cbox c d = {}")
case True
- show ?thesis
- apply (rule that[of "{cbox c d}"])
- apply (subst insert_is_Un)
- apply (rule division_disjoint_union)
- using \<open>cbox c d \<noteq> {}\<close> True assms interior_subset
- apply auto
- done
+ then show ?thesis
+ by (metis that False assms division_disjoint_union division_of_self insert_is_Un interior_Int interior_empty)
next
case False
obtain u v where uv: "cbox a b \<inter> cbox c d = cbox u v"
@@ -1220,13 +1215,14 @@
finally have [simp]: "interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}" by simp
have cbe: "cbox a b \<union> cbox c d = cbox a b \<union> \<Union>(p - {cbox u v})"
using p(8) unfolding uv[symmetric] by auto
- show ?thesis
- apply (rule that[of "p - {cbox u v}"])
- apply (simp add: cbe)
- apply (subst insert_is_Un)
- apply (rule division_disjoint_union)
- apply (simp_all add: assms division_of_self)
- by (metis Diff_subset division_of_subset p(1) p(8))
+ have "insert (cbox a b) (p - {cbox u v}) division_of cbox a b \<union> \<Union>(p - {cbox u v})"
+ proof -
+ have "{cbox a b} division_of cbox a b"
+ by (simp add: assms division_of_self)
+ then show "insert (cbox a b) (p - {cbox u v}) division_of cbox a b \<union> \<Union>(p - {cbox u v})"
+ by (metis (no_types) Diff_subset \<open>interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}\<close> division_disjoint_union division_of_subset insert_is_Un p(1) p(8))
+ qed
+ with that[of "p - {cbox u v}"] show ?thesis by (simp add: cbe)
qed
qed
@@ -1323,21 +1319,21 @@
presume "k = cbox a b \<Longrightarrow> ?thesis"
and "k' = cbox a b \<Longrightarrow> ?thesis"
and "k \<noteq> cbox a b \<Longrightarrow> k' \<noteq> cbox a b \<Longrightarrow> ?thesis"
- then show ?thesis by auto
+ then show ?thesis by linarith
next
assume as': "k = cbox a b"
show ?thesis
- using as' k' q(5) x' by auto
+ using as' k' q(5) x' by blast
next
assume as': "k' = cbox a b"
show ?thesis
- using as' k'(2) q(5) x by auto
+ using as' k'(2) q(5) x by blast
}
assume as': "k \<noteq> cbox a b" "k' \<noteq> cbox a b"
obtain c d where k: "k = cbox c d"
using q(4)[OF x(2,1)] by blast
have "interior k \<inter> interior (cbox a b) = {}"
- using as' k'(2) q(5) x by auto
+ using as' k'(2) q(5) x by blast
then have "interior k \<subseteq> interior x"
using interior_subset_union_intervals
by (metis as(2) k q(2) x interior_subset_union_intervals)
@@ -1345,7 +1341,7 @@
obtain c d where c_d: "k' = cbox c d"
using q(4)[OF x'(2,1)] by blast
have "interior k' \<inter> interior (cbox a b) = {}"
- using as'(2) q(5) x' by auto
+ using as'(2) q(5) x' by blast
then have "interior k' \<subseteq> interior x'"
by (metis as(2) c_d interior_subset_union_intervals q(2) x'(1) x'(2))
ultimately show ?thesis
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Mar 14 12:31:05 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Mar 14 14:25:11 2016 +0000
@@ -1152,7 +1152,7 @@
using continuous_linepath_at
by (auto intro!: continuous_at_imp_continuous_on)
-lemma path_linepath[intro]: "path (linepath a b)"
+lemma path_linepath[iff]: "path (linepath a b)"
unfolding path_def
by (rule continuous_on_linepath)
@@ -1168,8 +1168,7 @@
by (simp add: linepath_def)
lemma arc_linepath:
- assumes "a \<noteq> b"
- shows "arc (linepath a b)"
+ assumes "a \<noteq> b" shows [simp]: "arc (linepath a b)"
proof -
{
fix x y :: "real"
@@ -1193,6 +1192,54 @@
lemma subpath_refl: "subpath a a g = linepath (g a) (g a)"
by (simp add: subpath_def linepath_def algebra_simps)
+lemma linepath_of_real: "(linepath (of_real a) (of_real b) x) = of_real ((1 - x)*a + x*b)"
+ by (simp add: scaleR_conv_of_real linepath_def)
+
+lemma of_real_linepath: "of_real (linepath a b x) = linepath (of_real a) (of_real b) x"
+ by (metis linepath_of_real mult.right_neutral of_real_def real_scaleR_def)
+
+
+subsection\<open>Segments via convex hulls\<close>
+
+lemma segments_subset_convex_hull:
+ "closed_segment a b \<subseteq> (convex hull {a,b,c})"
+ "closed_segment a c \<subseteq> (convex hull {a,b,c})"
+ "closed_segment b c \<subseteq> (convex hull {a,b,c})"
+ "closed_segment b a \<subseteq> (convex hull {a,b,c})"
+ "closed_segment c a \<subseteq> (convex hull {a,b,c})"
+ "closed_segment c b \<subseteq> (convex hull {a,b,c})"
+by (auto simp: segment_convex_hull linepath_of_real elim!: rev_subsetD [OF _ hull_mono])
+
+lemma midpoints_in_convex_hull:
+ assumes "x \<in> convex hull s" "y \<in> convex hull s"
+ shows "midpoint x y \<in> convex hull s"
+proof -
+ have "(1 - inverse(2)) *\<^sub>R x + inverse(2) *\<^sub>R y \<in> convex hull s"
+ apply (rule convexD_alt)
+ using assms
+ apply (auto simp: convex_convex_hull)
+ done
+ then show ?thesis
+ by (simp add: midpoint_def algebra_simps)
+qed
+
+lemma convex_hull_subset:
+ "s \<subseteq> convex hull t \<Longrightarrow> convex hull s \<subseteq> convex hull t"
+ by (simp add: convex_convex_hull subset_hull)
+
+lemma not_in_interior_convex_hull_3:
+ fixes a :: "complex"
+ shows "a \<notin> interior(convex hull {a,b,c})"
+ "b \<notin> interior(convex hull {a,b,c})"
+ "c \<notin> interior(convex hull {a,b,c})"
+ by (auto simp: card_insert_le_m1 not_in_interior_convex_hull)
+
+lemma midpoint_in_closed_segment [simp]: "midpoint a b \<in> closed_segment a b"
+ using midpoints_in_convex_hull segment_convex_hull by blast
+
+lemma midpoint_in_open_segment [simp]: "midpoint a b \<in> open_segment a b \<longleftrightarrow> a \<noteq> b"
+ by (simp add: midpoint_eq_endpoint(1) midpoint_eq_endpoint(2) open_segment_def)
+
subsection \<open>Bounding a point away from a path\<close>
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Mar 14 12:31:05 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Mar 14 14:25:11 2016 +0000
@@ -7310,7 +7310,7 @@
finally show "closed (cbox a b)" .
qed
-lemma interior_cbox [intro]:
+lemma interior_cbox [simp]:
fixes a b :: "'a::euclidean_space"
shows "interior (cbox a b) = box a b" (is "?L = ?R")
proof(rule subset_antisym)
@@ -7376,7 +7376,7 @@
unfolding cbox_def bounded_iff by auto
qed
-lemma bounded_box:
+lemma bounded_box [simp]:
fixes a :: "'a::euclidean_space"
shows "bounded (box a b)"
using bounded_cbox[of a b]
@@ -7384,12 +7384,12 @@
using bounded_subset[of "cbox a b" "box a b"]
by simp
-lemma not_interval_univ:
+lemma not_interval_UNIV [simp]:
fixes a :: "'a::euclidean_space"
shows "cbox a b \<noteq> UNIV" "box a b \<noteq> UNIV"
- using bounded_box[of a b] bounded_cbox[of a b] by auto
-
-lemma compact_cbox:
+ using bounded_box[of a b] bounded_cbox[of a b] by force+
+
+lemma compact_cbox [simp]:
fixes a :: "'a::euclidean_space"
shows "compact (cbox a b)"
using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_cbox[of a b]