# HG changeset patch # User paulson # Date 1457965146 0 # Node ID f7f2467ab85451b435a7c937a2ff6f5d7e280b43 # Parent b89d4b320464d665fe105b9fcc7b6f887c026ae1 Refactoring (moving theorems into better locations), plus a bit of new material diff -r b89d4b320464 -r f7f2467ab854 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Sun Mar 13 14:42:07 2016 +0100 +++ b/src/HOL/Finite_Set.thy Mon Mar 14 14:19:06 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) \ finite A" +using assms finite_imageD by blast + lemma finite_surj: "finite A \ B \ f ` A \ finite B" by (erule finite_subset) (rule finite_imageI) diff -r b89d4b320464 -r f7f2467ab854 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Sun Mar 13 14:42:07 2016 +0100 +++ b/src/HOL/Fun.thy Mon Mar 14 14:19:06 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) diff -r b89d4b320464 -r f7f2467ab854 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Sun Mar 13 14:42:07 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Mar 14 14:19:06 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\Segments via convex hulls\ - -lemma segments_subset_convex_hull: - "closed_segment a b \ (convex hull {a,b,c})" - "closed_segment a c \ (convex hull {a,b,c})" - "closed_segment b c \ (convex hull {a,b,c})" - "closed_segment b a \ (convex hull {a,b,c})" - "closed_segment c a \ (convex hull {a,b,c})" - "closed_segment c b \ (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 \ convex hull s" "y \ convex hull s" - shows "midpoint x y \ convex hull s" -proof - - have "(1 - inverse(2)) *\<^sub>R x + inverse(2) *\<^sub>R y \ 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 \ convex hull t \ convex hull s \ convex hull t" - by (simp add: convex_convex_hull subset_hull) - -lemma not_in_interior_convex_hull_3: - fixes a :: "complex" - shows "a \ interior(convex hull {a,b,c})" - "b \ interior(convex hull {a,b,c})" - "c \ interior(convex hull {a,b,c})" - by (auto simp: card_insert_le_m1 not_in_interior_convex_hull) - - text\Cauchy's theorem where there's a primitive\ lemma contour_integral_primitive_lemma: diff -r b89d4b320464 -r f7f2467ab854 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun Mar 13 14:42:07 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Mar 14 14:19:06 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 "\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 \ c" obtains x :: "'a::{real_normed_vector, perfect_space}" where "norm x = c" @@ -5759,7 +5769,7 @@ shows "is_interval s \ 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 \ u < 1})" - by (auto simp: open_segment_def closed_segment_def segment_degen_0 segment_degen_1) - lemma open_segment_bound1: assumes "x \ 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 \ 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\Betweenness\ +lemma rel_interior_closure_convex_segment: + fixes S :: "_::euclidean_space set" + assumes "convex S" "a \ rel_interior S" "b \ closure S" + shows "open_segment a b \ 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 \ open_segment a b" + then show "x \ rel_interior S" + unfolding closed_segment_def open_segment_def using assms + by (auto intro: rel_interior_closure_convex_shrink) +qed + +subsection\Betweenness\ lemma between_mem_segment: "between (a,b) x \ x \ closed_segment a b" unfolding between_def by auto diff -r b89d4b320464 -r f7f2467ab854 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Sun Mar 13 14:42:07 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Mar 14 14:19:06 2016 +0000 @@ -1193,13 +1193,8 @@ show ?thesis proof (cases "cbox a b \ 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 \cbox c d \ {}\ 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 \ cbox c d = cbox u v" @@ -1220,13 +1215,14 @@ finally have [simp]: "interior (cbox a b) \ interior (\(p - {cbox u v})) = {}" by simp have cbe: "cbox a b \ cbox c d = cbox a b \ \(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 \ \(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 \ \(p - {cbox u v})" + by (metis (no_types) Diff_subset \interior (cbox a b) \ interior (\(p - {cbox u v})) = {}\ 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 \ ?thesis" and "k' = cbox a b \ ?thesis" and "k \ cbox a b \ k' \ cbox a b \ ?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 \ cbox a b" "k' \ cbox a b" obtain c d where k: "k = cbox c d" using q(4)[OF x(2,1)] by blast have "interior k \ 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 \ 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' \ interior (cbox a b) = {}" - using as'(2) q(5) x' by auto + using as'(2) q(5) x' by blast then have "interior k' \ interior x'" by (metis as(2) c_d interior_subset_union_intervals q(2) x'(1) x'(2)) ultimately show ?thesis diff -r b89d4b320464 -r f7f2467ab854 src/HOL/Multivariate_Analysis/Path_Connected.thy --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Sun Mar 13 14:42:07 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Mar 14 14:19:06 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 \ b" - shows "arc (linepath a b)" + assumes "a \ 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\Segments via convex hulls\ + +lemma segments_subset_convex_hull: + "closed_segment a b \ (convex hull {a,b,c})" + "closed_segment a c \ (convex hull {a,b,c})" + "closed_segment b c \ (convex hull {a,b,c})" + "closed_segment b a \ (convex hull {a,b,c})" + "closed_segment c a \ (convex hull {a,b,c})" + "closed_segment c b \ (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 \ convex hull s" "y \ convex hull s" + shows "midpoint x y \ convex hull s" +proof - + have "(1 - inverse(2)) *\<^sub>R x + inverse(2) *\<^sub>R y \ 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 \ convex hull t \ convex hull s \ convex hull t" + by (simp add: convex_convex_hull subset_hull) + +lemma not_in_interior_convex_hull_3: + fixes a :: "complex" + shows "a \ interior(convex hull {a,b,c})" + "b \ interior(convex hull {a,b,c})" + "c \ 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 \ closed_segment a b" + using midpoints_in_convex_hull segment_convex_hull by blast + +lemma midpoint_in_open_segment [simp]: "midpoint a b \ open_segment a b \ a \ b" + by (simp add: midpoint_eq_endpoint(1) midpoint_eq_endpoint(2) open_segment_def) + subsection \Bounding a point away from a path\ diff -r b89d4b320464 -r f7f2467ab854 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Mar 13 14:42:07 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Mar 14 14:19:06 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 \ UNIV" "box a b \ 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]