# HG changeset patch # User paulson # Date 1525261688 -3600 # Node ID d2daeef3ce4722d315a0574f7b0a5844d1e53d4c # Parent 539048827fe8ab4752f97a25f57682ad5018e054# Parent b249fab48c76ee1d3ed0d54ce3961b6bcbd4fae4 merged diff -r b249fab48c76 -r d2daeef3ce47 src/HOL/Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed May 02 12:47:56 2018 +0100 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed May 02 12:48:08 2018 +0100 @@ -1919,15 +1919,13 @@ definition "vector l = (\ i. foldr (\x f n. fun_upd (f (n+1)) n x) l (\n x. 0) 1 i)" -lemma vector_1: "(vector[x]) $1 = x" +lemma vector_1 [simp]: "(vector[x]) $1 = x" unfolding vector_def by simp -lemma vector_2: - "(vector[x,y]) $1 = x" - "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)" +lemma vector_2 [simp]: "(vector[x,y]) $1 = x" "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)" unfolding vector_def by simp_all -lemma vector_3: +lemma vector_3 [simp]: "(vector [x,y,z] ::('a::zero)^3)$1 = x" "(vector [x,y,z] ::('a::zero)^3)$2 = y" "(vector [x,y,z] ::('a::zero)^3)$3 = z" @@ -1958,7 +1956,7 @@ done lemma bounded_linear_component_cart[intro]: "bounded_linear (\x::real^'n. x $ k)" - apply (rule bounded_linearI[where K=1]) + apply (rule bounded_linear_intro[where K=1]) using component_le_norm_cart[of _ k] unfolding real_norm_def by auto lemma interval_split_cart: diff -r b249fab48c76 -r d2daeef3ce47 src/HOL/Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Wed May 02 12:47:56 2018 +0100 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Wed May 02 12:48:08 2018 +0100 @@ -837,15 +837,13 @@ qed } note ** = this show ?thesis - unfolding has_field_derivative_def + unfolding has_field_derivative_def proof (rule has_derivative_sequence [OF cvs _ _ x]) - show "\n. \x\s. (f n has_derivative (( * ) (f' n x))) (at x within s)" - by (metis has_field_derivative_def df) - next show "(\n. f n x) \ l" + show "(\n. f n x) \ l" by (rule tf) - next show "\e>0. \N. \n\N. \x\s. \h. cmod (f' n x * h - g' x * h) \ e * cmod h" + next show "\e. e > 0 \ \N. \n\N. \x\s. \h. cmod (f' n x * h - g' x * h) \ e * cmod h" by (blast intro: **) - qed + qed (metis has_field_derivative_def df) qed lemma has_complex_derivative_series: @@ -884,7 +882,7 @@ by (metis df has_field_derivative_def mult_commute_abs) next show " ((\n. f n x) sums l)" by (rule sf) - next show "\e>0. \N. \n\N. \x\s. \h. cmod ((\i e * cmod h" + next show "\e. e>0 \ \N. \n\N. \x\s. \h. cmod ((\i e * cmod h" by (blast intro: **) qed qed @@ -896,7 +894,7 @@ assumes "\n x. x \ s \ (f n has_field_derivative f' n x) (at x)" assumes "uniformly_convergent_on s (\n x. \i s" "summable (\n. f n x0)" and x: "x \ s" - shows "summable (\n. f n x)" and "(\x. \n. f n x) field_differentiable (at x)" + shows "(\x. \n. f n x) field_differentiable (at x)" proof - from assms(4) obtain g' where A: "uniform_limit s (\n x. \ix. x \ s \ (\n. f n x) sums g x" "\x. x \ s \ (g has_field_derivative g' x) (at x within s)" by blast - from g[OF x] show "summable (\n. f n x)" by (auto simp: summable_def) from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)" by (simp add: has_field_derivative_def s) have "((\x. \n. f n x) has_derivative ( * ) (g' x)) (at x)" @@ -915,15 +912,6 @@ by (auto simp: summable_def field_differentiable_def has_field_derivative_def) qed -lemma field_differentiable_series': - fixes f :: "nat \ 'a::{real_normed_field,banach} \ 'a" - assumes "convex s" "open s" - assumes "\n x. x \ s \ (f n has_field_derivative f' n x) (at x)" - assumes "uniformly_convergent_on s (\n x. \i s" "summable (\n. f n x0)" - shows "(\x. \n. f n x) field_differentiable (at x0)" - using field_differentiable_series[OF assms, of x0] \x0 \ s\ by blast+ - subsection\Bound theorem\ lemma field_differentiable_bound: diff -r b249fab48c76 -r d2daeef3ce47 src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed May 02 12:47:56 2018 +0100 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed May 02 12:48:08 2018 +0100 @@ -2470,8 +2470,8 @@ proof show "convex hull (s \ t) \ (convex hull s) \ (convex hull t)" by (intro hull_minimal Sigma_mono hull_subset convex_Times convex_convex_hull) - have "\x\convex hull s. \y\convex hull t. (x, y) \ convex hull (s \ t)" - proof (intro hull_induct) + have "(x, y) \ convex hull (s \ t)" if x: "x \ convex hull s" and y: "y \ convex hull t" for x y + proof (rule hull_induct [OF x], rule hull_induct [OF y]) fix x y assume "x \ s" and "y \ t" then show "(x, y) \ convex hull (s \ t)" by (simp add: hull_inc) @@ -2484,8 +2484,8 @@ by (auto simp: image_def Bex_def) finally show "convex {y. (x, y) \ convex hull (s \ t)}" . next - show "convex {x. \y\convex hull t. (x, y) \ convex hull (s \ t)}" - proof (unfold Collect_ball_eq, rule convex_INT [rule_format]) + show "convex {x. (x, y) \ convex hull s \ t}" + proof - fix y let ?S = "((\x. (x, 0)) -` (\p. (0, - y) + p) ` (convex hull s \ t))" have "convex ?S" by (intro convex_linear_vimage convex_translation convex_convex_hull, @@ -2496,7 +2496,7 @@ qed qed then show "(convex hull s) \ (convex hull t) \ convex hull (s \ t)" - unfolding subset_eq split_paired_Ball_Sigma . + unfolding subset_eq split_paired_Ball_Sigma by blast qed @@ -2512,16 +2512,13 @@ fixes S :: "'a::real_vector set" assumes "S \ {}" shows "convex hull (insert a S) = - {x. \u\0. \v\0. \b. (u + v = 1) \ b \ (convex hull S) \ (x = u *\<^sub>R a + v *\<^sub>R b)}" + {x. \u\0. \v\0. \b. (u + v = 1) \ b \ (convex hull S) \ (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "_ = ?hull") - apply (rule, rule hull_minimal, rule) +proof (intro equalityI hull_minimal subsetI) + fix x + assume "x \ insert a S" + then have "\u\0. \v\0. u + v = 1 \ (\b. b \ convex hull S \ x = u *\<^sub>R a + v *\<^sub>R b)" unfolding insert_iff - prefer 3 - apply rule -proof - - fix x - assume x: "x = a \ x \ S" - then have "\u\0. \v\0. u + v = 1 \ (\b. b \ convex hull S \ x = u *\<^sub>R a + v *\<^sub>R b)" proof assume "x = a" then show ?thesis @@ -2619,7 +2616,7 @@ lemma convex_hull_insert_alt: "convex hull (insert a S) = - (if S = {} then {a} + (if S = {} then {a} else {(1 - u) *\<^sub>R a + u *\<^sub>R x |x u. 0 \ u \ u \ 1 \ x \ convex hull S})" apply (auto simp: convex_hull_insert) using diff_eq_eq apply fastforce @@ -4371,7 +4368,7 @@ finally have "y \ S" apply (subst *) apply (rule assms(1)[unfolded convex_alt,rule_format]) - apply (rule d[unfolded subset_eq,rule_format]) + apply (rule d[THEN subsetD]) unfolding mem_ball using assms(3-5) ** apply auto @@ -4751,22 +4748,17 @@ lemma affine_hull_linear_image: assumes "bounded_linear f" shows "f ` (affine hull s) = affine hull f ` s" - apply rule - unfolding subset_eq ball_simps - apply (rule_tac[!] hull_induct, rule hull_inc) - prefer 3 - apply (erule imageE) - apply (rule_tac x=xa in image_eqI, assumption) - apply (rule hull_subset[unfolded subset_eq, rule_format], assumption) proof - interpret f: bounded_linear f by fact - show "affine {x. f x \ affine hull f ` s}" + have "affine {x. f x \ affine hull f ` s}" unfolding affine_def by (auto simp: f.scaleR f.add affine_affine_hull[unfolded affine_def, rule_format]) - show "affine {x. x \ f ` (affine hull s)}" + moreover have "affine {x. x \ f ` (affine hull s)}" using affine_affine_hull[unfolded affine_def, of s] unfolding affine_def by (auto simp: f.scaleR [symmetric] f.add [symmetric]) -qed auto + ultimately show ?thesis + by (auto simp: hull_inc elim!: hull_induct) +qed lemma rel_interior_injective_on_span_linear_image: @@ -4893,112 +4885,77 @@ subsection%unimportant \Openness and compactness are preserved by convex hull operation\ lemma open_convex_hull[intro]: - fixes s :: "'a::real_normed_vector set" - assumes "open s" - shows "open (convex hull s)" - unfolding open_contains_cball convex_hull_explicit - unfolding mem_Collect_eq ball_simps(8) -proof (rule, rule) - fix a - assume "\sa u. finite sa \ sa \ s \ (\x\sa. 0 \ u x) \ sum u sa = 1 \ (\v\sa. u v *\<^sub>R v) = a" - then obtain t u where obt: "finite t" "t\s" "\x\t. 0 \ u x" "sum u t = 1" "(\v\t. u v *\<^sub>R v) = a" - by auto + fixes S :: "'a::real_normed_vector set" + assumes "open S" + shows "open (convex hull S)" +proof (clarsimp simp: open_contains_cball convex_hull_explicit) + fix T and u :: "'a\real" + assume obt: "finite T" "T\S" "\x\T. 0 \ u x" "sum u T = 1" from assms[unfolded open_contains_cball] obtain b - where b: "\x\s. 0 < b x \ cball x (b x) \ s" - using bchoice[of s "\x e. e > 0 \ cball x e \ s"] by auto - have "b ` t \ {}" + where b: "\x. x\S \ 0 < b x \ cball x (b x) \ S" by metis + have "b ` T \ {}" using obt by auto - define i where "i = b ` t" - - show "\e > 0. - cball a e \ {y. \sa u. finite sa \ sa \ s \ (\x\sa. 0 \ u x) \ sum u sa = 1 \ (\v\sa. u v *\<^sub>R v) = y}" - apply (rule_tac x = "Min i" in exI) - unfolding subset_eq - apply rule - defer - apply rule - unfolding mem_Collect_eq - proof - + define i where "i = b ` T" + let ?\ = "\y. \F. finite F \ F \ S \ (\u. (\x\F. 0 \ u x) \ sum u F = 1 \ (\v\F. u v *\<^sub>R v) = y)" + let ?a = "\v\T. u v *\<^sub>R v" + show "\e > 0. cball ?a e \ {y. ?\ y}" + proof (intro exI subsetI conjI) show "0 < Min i" - unfolding i_def and Min_gr_iff[OF finite_imageI[OF obt(1)] \b ` t\{}\] - using b - apply simp - apply rule - apply (erule_tac x=x in ballE) - using \t\s\ - apply auto - done + unfolding i_def and Min_gr_iff[OF finite_imageI[OF obt(1)] \b ` T\{}\] + using b \T\S\ by auto next fix y - assume "y \ cball a (Min i)" - then have y: "norm (a - y) \ Min i" + assume "y \ cball ?a (Min i)" + then have y: "norm (?a - y) \ Min i" unfolding dist_norm[symmetric] by auto - { - fix x - assume "x \ t" + { fix x + assume "x \ T" then have "Min i \ b x" - unfolding i_def - apply (rule_tac Min_le) - using obt(1) - apply auto - done - then have "x + (y - a) \ cball x (b x)" + by (simp add: i_def obt(1)) + then have "x + (y - ?a) \ cball x (b x)" using y unfolding mem_cball dist_norm by auto - moreover from \x\t\ have "x \ s" - using obt(2) by auto - ultimately have "x + (y - a) \ s" - using y and b[THEN bspec[where x=x]] unfolding subset_eq by fast + moreover have "x \ S" + using \x\T\ \T\S\ by auto + ultimately have "x + (y - ?a) \ S" + using y b by blast } moreover - have *: "inj_on (\v. v + (y - a)) t" + have *: "inj_on (\v. v + (y - ?a)) T" unfolding inj_on_def by auto - have "(\v\(\v. v + (y - a)) ` t. u (v - (y - a))) = 1" - unfolding sum.reindex[OF *] o_def using obt(4) by auto - moreover have "(\v\(\v. v + (y - a)) ` t. u (v - (y - a)) *\<^sub>R v) = y" - unfolding sum.reindex[OF *] o_def using obt(4,5) + have "(\v\(\v. v + (y - ?a)) ` T. u (v - (y - ?a)) *\<^sub>R v) = y" + unfolding sum.reindex[OF *] o_def using obt(4) by (simp add: sum.distrib sum_subtractf scaleR_left.sum[symmetric] scaleR_right_distrib) - ultimately - show "\sa u. finite sa \ (\x\sa. x \ s) \ (\x\sa. 0 \ u x) \ sum u sa = 1 \ (\v\sa. u v *\<^sub>R v) = y" - apply (rule_tac x="(\v. v + (y - a)) ` t" in exI) - apply (rule_tac x="\v. u (v - (y - a))" in exI) - using obt(1, 3) - apply auto - done + ultimately show "y \ {y. ?\ y}" + proof (intro CollectI exI conjI) + show "finite ((\v. v + (y - ?a)) ` T)" + by (simp add: obt(1)) + show "sum (\v. u (v - (y - ?a))) ((\v. v + (y - ?a)) ` T) = 1" + unfolding sum.reindex[OF *] o_def using obt(4) by auto + qed (use obt(1, 3) in auto) qed qed lemma compact_convex_combinations: - fixes s t :: "'a::real_normed_vector set" - assumes "compact s" "compact t" - shows "compact { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \ u \ u \ 1 \ x \ s \ y \ t}" + fixes S T :: "'a::real_normed_vector set" + assumes "compact S" "compact T" + shows "compact { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \ u \ u \ 1 \ x \ S \ y \ T}" proof - - let ?X = "{0..1} \ s \ t" + let ?X = "{0..1} \ S \ T" let ?h = "(\z. (1 - fst z) *\<^sub>R fst (snd z) + fst z *\<^sub>R snd (snd z))" - have *: "{ (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \ u \ u \ 1 \ x \ s \ y \ t} = ?h ` ?X" - apply (rule set_eqI) - unfolding image_iff mem_Collect_eq - apply rule - apply auto - apply (rule_tac x=u in rev_bexI, simp) - apply (erule rev_bexI) - apply (erule rev_bexI, simp) - apply auto - done + have *: "{ (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \ u \ u \ 1 \ x \ S \ y \ T} = ?h ` ?X" + by force have "continuous_on ?X (\z. (1 - fst z) *\<^sub>R fst (snd z) + fst z *\<^sub>R snd (snd z))" unfolding continuous_on by (rule ballI) (intro tendsto_intros) - then show ?thesis - unfolding * - apply (rule compact_continuous_image) - apply (intro compact_Times compact_Icc assms) - done + with assms show ?thesis + by (simp add: * compact_Times compact_continuous_image) qed lemma finite_imp_compact_convex_hull: - fixes s :: "'a::real_normed_vector set" - assumes "finite s" - shows "compact (convex hull s)" -proof (cases "s = {}") + fixes S :: "'a::real_normed_vector set" + assumes "finite S" + shows "compact (convex hull S)" +proof (cases "S = {}") case True then show ?thesis by simp next @@ -5029,20 +4986,20 @@ qed lemma compact_convex_hull: - fixes s :: "'a::euclidean_space set" - assumes "compact s" - shows "compact (convex hull s)" -proof (cases "s = {}") + fixes S :: "'a::euclidean_space set" + assumes "compact S" + shows "compact (convex hull S)" +proof (cases "S = {}") case True then show ?thesis using compact_empty by simp next case False - then obtain w where "w \ s" by auto + then obtain w where "w \ S" by auto show ?thesis - unfolding caratheodory[of s] + unfolding caratheodory[of S] proof (induct ("DIM('a) + 1")) case 0 - have *: "{x.\sa. finite sa \ sa \ s \ card sa \ 0 \ x \ convex hull sa} = {}" + have *: "{x.\sa. finite sa \ sa \ S \ card sa \ 0 \ x \ convex hull sa} = {}" using compact_empty by auto from 0 show ?case unfolding * by simp next @@ -5050,27 +5007,27 @@ show ?case proof (cases "n = 0") case True - have "{x. \t. finite t \ t \ s \ card t \ Suc n \ x \ convex hull t} = s" + have "{x. \T. finite T \ T \ S \ card T \ Suc n \ x \ convex hull T} = S" unfolding set_eq_iff and mem_Collect_eq proof (rule, rule) fix x - assume "\t. finite t \ t \ s \ card t \ Suc n \ x \ convex hull t" - then obtain t where t: "finite t" "t \ s" "card t \ Suc n" "x \ convex hull t" + assume "\T. finite T \ T \ S \ card T \ Suc n \ x \ convex hull T" + then obtain T where T: "finite T" "T \ S" "card T \ Suc n" "x \ convex hull T" by auto - show "x \ s" - proof (cases "card t = 0") + show "x \ S" + proof (cases "card T = 0") case True then show ?thesis - using t(4) unfolding card_0_eq[OF t(1)] by simp + using T(4) unfolding card_0_eq[OF T(1)] by simp next case False - then have "card t = Suc 0" using t(3) \n=0\ by auto - then obtain a where "t = {a}" unfolding card_Suc_eq by auto - then show ?thesis using t(2,4) by simp + then have "card T = Suc 0" using T(3) \n=0\ by auto + then obtain a where "T = {a}" unfolding card_Suc_eq by auto + then show ?thesis using T(2,4) by simp qed next - fix x assume "x\s" - then show "\t. finite t \ t \ s \ card t \ Suc n \ x \ convex hull t" + fix x assume "x\S" + then show "\T. finite T \ T \ S \ card T \ Suc n \ x \ convex hull T" apply (rule_tac x="{x}" in exI) unfolding convex_hull_singleton apply auto @@ -5079,56 +5036,56 @@ then show ?thesis using assms by simp next case False - have "{x. \t. finite t \ t \ s \ card t \ Suc n \ x \ convex hull t} = + have "{x. \T. finite T \ T \ S \ card T \ Suc n \ x \ convex hull T} = {(1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. - 0 \ u \ u \ 1 \ x \ s \ y \ {x. \t. finite t \ t \ s \ card t \ n \ x \ convex hull t}}" + 0 \ u \ u \ 1 \ x \ S \ y \ {x. \T. finite T \ T \ S \ card T \ n \ x \ convex hull T}}" unfolding set_eq_iff and mem_Collect_eq proof (rule, rule) fix x assume "\u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \ - 0 \ c \ c \ 1 \ u \ s \ (\t. finite t \ t \ s \ card t \ n \ v \ convex hull t)" - then obtain u v c t where obt: "x = (1 - c) *\<^sub>R u + c *\<^sub>R v" - "0 \ c \ c \ 1" "u \ s" "finite t" "t \ s" "card t \ n" "v \ convex hull t" + 0 \ c \ c \ 1 \ u \ S \ (\T. finite T \ T \ S \ card T \ n \ v \ convex hull T)" + then obtain u v c T where obt: "x = (1 - c) *\<^sub>R u + c *\<^sub>R v" + "0 \ c \ c \ 1" "u \ S" "finite T" "T \ S" "card T \ n" "v \ convex hull T" by auto - moreover have "(1 - c) *\<^sub>R u + c *\<^sub>R v \ convex hull insert u t" + moreover have "(1 - c) *\<^sub>R u + c *\<^sub>R v \ convex hull insert u T" apply (rule convexD_alt) - using obt(2) and convex_convex_hull and hull_subset[of "insert u t" convex] - using obt(7) and hull_mono[of t "insert u t"] + using obt(2) and convex_convex_hull and hull_subset[of "insert u T" convex] + using obt(7) and hull_mono[of T "insert u T"] apply auto done - ultimately show "\t. finite t \ t \ s \ card t \ Suc n \ x \ convex hull t" - apply (rule_tac x="insert u t" in exI) + ultimately show "\T. finite T \ T \ S \ card T \ Suc n \ x \ convex hull T" + apply (rule_tac x="insert u T" in exI) apply (auto simp: card_insert_if) done next fix x - assume "\t. finite t \ t \ s \ card t \ Suc n \ x \ convex hull t" - then obtain t where t: "finite t" "t \ s" "card t \ Suc n" "x \ convex hull t" + assume "\T. finite T \ T \ S \ card T \ Suc n \ x \ convex hull T" + then obtain T where T: "finite T" "T \ S" "card T \ Suc n" "x \ convex hull T" by auto show "\u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \ - 0 \ c \ c \ 1 \ u \ s \ (\t. finite t \ t \ s \ card t \ n \ v \ convex hull t)" - proof (cases "card t = Suc n") + 0 \ c \ c \ 1 \ u \ S \ (\T. finite T \ T \ S \ card T \ n \ v \ convex hull T)" + proof (cases "card T = Suc n") case False - then have "card t \ n" using t(3) by auto + then have "card T \ n" using T(3) by auto then show ?thesis apply (rule_tac x=w in exI, rule_tac x=x in exI, rule_tac x=1 in exI) - using \w\s\ and t - apply (auto intro!: exI[where x=t]) + using \w\S\ and T + apply (auto intro!: exI[where x=T]) done next case True - then obtain a u where au: "t = insert a u" "a\u" + then obtain a u where au: "T = insert a u" "a\u" apply (drule_tac card_eq_SucD, auto) done show ?thesis proof (cases "u = {}") case True - then have "x = a" using t(4)[unfolded au] by auto + then have "x = a" using T(4)[unfolded au] by auto show ?thesis unfolding \x = a\ apply (rule_tac x=a in exI) apply (rule_tac x=a in exI) apply (rule_tac x=1 in exI) - using t and \n \ 0\ + using T and \n \ 0\ unfolding au apply (auto intro!: exI[where x="{a}"]) done @@ -5136,14 +5093,14 @@ case False obtain ux vx b where obt: "ux\0" "vx\0" "ux + vx = 1" "b \ convex hull u" "x = ux *\<^sub>R a + vx *\<^sub>R b" - using t(4)[unfolded au convex_hull_insert[OF False]] + using T(4)[unfolded au convex_hull_insert[OF False]] by auto have *: "1 - vx = ux" using obt(3) by auto show ?thesis apply (rule_tac x=a in exI) apply (rule_tac x=b in exI) apply (rule_tac x=vx in exI) - using obt and t(1-3) + using obt and T(1-3) unfolding au and * using card_insert_disjoint[OF _ au(2)] apply (auto intro!: exI[where x=u]) done @@ -5195,25 +5152,25 @@ using dist_increases_online[of d a 0] unfolding dist_norm by auto lemma simplex_furthest_lt: - fixes s :: "'a::real_inner set" - assumes "finite s" - shows "\x \ convex hull s. x \ s \ (\y \ convex hull s. norm (x - a) < norm(y - a))" + fixes S :: "'a::real_inner set" + assumes "finite S" + shows "\x \ convex hull S. x \ S \ (\y \ convex hull S. norm (x - a) < norm(y - a))" using assms proof induct - fix x s - assume as: "finite s" "x\s" "\x\convex hull s. x \ s \ (\y\convex hull s. norm (x - a) < norm (y - a))" - show "\xa\convex hull insert x s. xa \ insert x s \ - (\y\convex hull insert x s. norm (xa - a) < norm (y - a))" - proof (rule, rule, cases "s = {}") + fix x S + assume as: "finite S" "x\S" "\x\convex hull S. x \ S \ (\y\convex hull S. norm (x - a) < norm (y - a))" + show "\xa\convex hull insert x S. xa \ insert x S \ + (\y\convex hull insert x S. norm (xa - a) < norm (y - a))" + proof (intro impI ballI, cases "S = {}") case False fix y - assume y: "y \ convex hull insert x s" "y \ insert x s" - obtain u v b where obt: "u\0" "v\0" "u + v = 1" "b \ convex hull s" "y = u *\<^sub>R x + v *\<^sub>R b" + assume y: "y \ convex hull insert x S" "y \ insert x S" + obtain u v b where obt: "u\0" "v\0" "u + v = 1" "b \ convex hull S" "y = u *\<^sub>R x + v *\<^sub>R b" using y(1)[unfolded convex_hull_insert[OF False]] by auto - show "\z\convex hull insert x s. norm (y - a) < norm (z - a)" - proof (cases "y \ convex hull s") + show "\z\convex hull insert x S. norm (y - a) < norm (z - a)" + proof (cases "y \ convex hull S") case True - then obtain z where "z \ convex hull s" "norm (y - a) < norm (z - a)" + then obtain z where "z \ convex hull S" "norm (y - a) < norm (z - a)" using as(3)[THEN bspec[where x=y]] and y(2) by auto then show ?thesis apply (rule_tac x=z in bexI) @@ -5252,14 +5209,12 @@ unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: algebra_simps) - moreover have "(u + w) *\<^sub>R x + (v - w) *\<^sub>R b \ convex hull insert x s" - unfolding convex_hull_insert[OF \s\{}\] and mem_Collect_eq - apply (rule_tac x="u + w" in exI, rule) - defer - apply (rule_tac x="v - w" in exI) - using \u \ 0\ and w and obt(3,4) - apply auto - done + moreover have "(u + w) *\<^sub>R x + (v - w) *\<^sub>R b \ convex hull insert x S" + unfolding convex_hull_insert[OF \S\{}\] + proof (intro CollectI conjI exI) + show "u + w \ 0" "v - w \ 0" + using obt(1) w by auto + qed (use obt in auto) ultimately show ?thesis by auto next assume "dist a y < dist a (y - w *\<^sub>R (x - b))" @@ -5267,14 +5222,12 @@ unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: algebra_simps) - moreover have "(u - w) *\<^sub>R x + (v + w) *\<^sub>R b \ convex hull insert x s" - unfolding convex_hull_insert[OF \s\{}\] and mem_Collect_eq - apply (rule_tac x="u - w" in exI, rule) - defer - apply (rule_tac x="v + w" in exI) - using \u \ 0\ and w and obt(3,4) - apply auto - done + moreover have "(u - w) *\<^sub>R x + (v + w) *\<^sub>R b \ convex hull insert x S" + unfolding convex_hull_insert[OF \S\{}\] + proof (intro CollectI conjI exI) + show "u - w \ 0" "v + w \ 0" + using obt(1) w by auto + qed (use obt in auto) ultimately show ?thesis by auto qed qed auto @@ -5283,22 +5236,22 @@ qed (auto simp: assms) lemma simplex_furthest_le: - fixes s :: "'a::real_inner set" - assumes "finite s" - and "s \ {}" - shows "\y\s. \x\ convex hull s. norm (x - a) \ norm (y - a)" + fixes S :: "'a::real_inner set" + assumes "finite S" + and "S \ {}" + shows "\y\S. \x\ convex hull S. norm (x - a) \ norm (y - a)" proof - - have "convex hull s \ {}" - using hull_subset[of s convex] and assms(2) by auto - then obtain x where x: "x \ convex hull s" "\y\convex hull s. norm (y - a) \ norm (x - a)" - using distance_attains_sup[OF finite_imp_compact_convex_hull[OF assms(1)], of a] + have "convex hull S \ {}" + using hull_subset[of S convex] and assms(2) by auto + then obtain x where x: "x \ convex hull S" "\y\convex hull S. norm (y - a) \ norm (x - a)" + using distance_attains_sup[OF finite_imp_compact_convex_hull[OF \finite S\], of a] unfolding dist_commute[of a] unfolding dist_norm by auto show ?thesis - proof (cases "x \ s") + proof (cases "x \ S") case False - then obtain y where "y \ convex hull s" "norm (x - a) < norm (y - a)" + then obtain y where "y \ convex hull S" "norm (x - a) < norm (y - a)" using simplex_furthest_lt[OF assms(1), THEN bspec[where x=x]] and x(1) by auto then show ?thesis @@ -5310,34 +5263,34 @@ qed lemma simplex_furthest_le_exists: - fixes s :: "('a::real_inner) set" - shows "finite s \ \x\(convex hull s). \y\s. norm (x - a) \ norm (y - a)" - using simplex_furthest_le[of s] by (cases "s = {}") auto + fixes S :: "('a::real_inner) set" + shows "finite S \ \x\(convex hull S). \y\S. norm (x - a) \ norm (y - a)" + using simplex_furthest_le[of S] by (cases "S = {}") auto lemma simplex_extremal_le: - fixes s :: "'a::real_inner set" - assumes "finite s" - and "s \ {}" - shows "\u\s. \v\s. \x\convex hull s. \y \ convex hull s. norm (x - y) \ norm (u - v)" + fixes S :: "'a::real_inner set" + assumes "finite S" + and "S \ {}" + shows "\u\S. \v\S. \x\convex hull S. \y \ convex hull S. norm (x - y) \ norm (u - v)" proof - - have "convex hull s \ {}" - using hull_subset[of s convex] and assms(2) by auto - then obtain u v where obt: "u \ convex hull s" "v \ convex hull s" - "\x\convex hull s. \y\convex hull s. norm (x - y) \ norm (u - v)" + have "convex hull S \ {}" + using hull_subset[of S convex] and assms(2) by auto + then obtain u v where obt: "u \ convex hull S" "v \ convex hull S" + "\x\convex hull S. \y\convex hull S. norm (x - y) \ norm (u - v)" using compact_sup_maxdistance[OF finite_imp_compact_convex_hull[OF assms(1)]] by (auto simp: dist_norm) then show ?thesis - proof (cases "u\s \ v\s", elim disjE) - assume "u \ s" - then obtain y where "y \ convex hull s" "norm (u - v) < norm (y - v)" + proof (cases "u\S \ v\S", elim disjE) + assume "u \ S" + then obtain y where "y \ convex hull S" "norm (u - v) < norm (y - v)" using simplex_furthest_lt[OF assms(1), THEN bspec[where x=u]] and obt(1) by auto then show ?thesis using obt(3)[THEN bspec[where x=y], THEN bspec[where x=v]] and obt(2) by auto next - assume "v \ s" - then obtain y where "y \ convex hull s" "norm (v - u) < norm (y - u)" + assume "v \ S" + then obtain y where "y \ convex hull S" "norm (v - u) < norm (y - u)" using simplex_furthest_lt[OF assms(1), THEN bspec[where x=v]] and obt(2) by auto then show ?thesis @@ -5347,45 +5300,45 @@ qed lemma simplex_extremal_le_exists: - fixes s :: "'a::real_inner set" - shows "finite s \ x \ convex hull s \ y \ convex hull s \ - \u\s. \v\s. norm (x - y) \ norm (u - v)" - using convex_hull_empty simplex_extremal_le[of s] - by(cases "s = {}") auto + fixes S :: "'a::real_inner set" + shows "finite S \ x \ convex hull S \ y \ convex hull S \ + \u\S. \v\S. norm (x - y) \ norm (u - v)" + using convex_hull_empty simplex_extremal_le[of S] + by(cases "S = {}") auto subsection \Closest point of a convex set is unique, with a continuous projection\ definition%important closest_point :: "'a::{real_inner,heine_borel} set \ 'a \ 'a" - where "closest_point s a = (SOME x. x \ s \ (\y\s. dist a x \ dist a y))" + where "closest_point S a = (SOME x. x \ S \ (\y\S. dist a x \ dist a y))" lemma closest_point_exists: - assumes "closed s" - and "s \ {}" - shows "closest_point s a \ s" - and "\y\s. dist a (closest_point s a) \ dist a y" + assumes "closed S" + and "S \ {}" + shows "closest_point S a \ S" + and "\y\S. dist a (closest_point S a) \ dist a y" unfolding closest_point_def apply(rule_tac[!] someI2_ex) apply (auto intro: distance_attains_inf[OF assms(1,2), of a]) done -lemma closest_point_in_set: "closed s \ s \ {} \ closest_point s a \ s" +lemma closest_point_in_set: "closed S \ S \ {} \ closest_point S a \ S" by (meson closest_point_exists) -lemma closest_point_le: "closed s \ x \ s \ dist a (closest_point s a) \ dist a x" - using closest_point_exists[of s] by auto +lemma closest_point_le: "closed S \ x \ S \ dist a (closest_point S a) \ dist a x" + using closest_point_exists[of S] by auto lemma closest_point_self: - assumes "x \ s" - shows "closest_point s x = x" + assumes "x \ S" + shows "closest_point S x = x" unfolding closest_point_def apply (rule some1_equality, rule ex1I[of _ x]) using assms apply auto done -lemma closest_point_refl: "closed s \ s \ {} \ closest_point s x = x \ x \ s" - using closest_point_in_set[of s x] closest_point_self[of x s] +lemma closest_point_refl: "closed S \ S \ {} \ closest_point S x = x \ x \ S" + using closest_point_in_set[of S x] closest_point_self[of x S] by auto lemma closer_points_lemma: @@ -5417,14 +5370,14 @@ qed lemma any_closest_point_dot: - assumes "convex s" "closed s" "x \ s" "y \ s" "\z\s. dist a x \ dist a z" + assumes "convex S" "closed S" "x \ S" "y \ S" "\z\S. dist a x \ dist a z" shows "inner (a - x) (y - x) \ 0" proof (rule ccontr) assume "\ ?thesis" then obtain u where u: "u>0" "u\1" "dist (x + u *\<^sub>R (y - x)) a < dist x a" using closer_point_lemma[of a x y] by auto let ?z = "(1 - u) *\<^sub>R x + u *\<^sub>R y" - have "?z \ s" + have "?z \ S" using convexD_alt[OF assms(1,3,4), of u] using u by auto then show False using assms(5)[THEN bspec[where x="?z"]] and u(3) @@ -5433,30 +5386,30 @@ lemma any_closest_point_unique: fixes x :: "'a::real_inner" - assumes "convex s" "closed s" "x \ s" "y \ s" - "\z\s. dist a x \ dist a z" "\z\s. dist a y \ dist a z" + assumes "convex S" "closed S" "x \ S" "y \ S" + "\z\S. dist a x \ dist a z" "\z\S. dist a y \ dist a z" shows "x = y" using any_closest_point_dot[OF assms(1-4,5)] and any_closest_point_dot[OF assms(1-2,4,3,6)] unfolding norm_pths(1) and norm_le_square by (auto simp: algebra_simps) lemma closest_point_unique: - assumes "convex s" "closed s" "x \ s" "\z\s. dist a x \ dist a z" - shows "x = closest_point s a" - using any_closest_point_unique[OF assms(1-3) _ assms(4), of "closest_point s a"] + assumes "convex S" "closed S" "x \ S" "\z\S. dist a x \ dist a z" + shows "x = closest_point S a" + using any_closest_point_unique[OF assms(1-3) _ assms(4), of "closest_point S a"] using closest_point_exists[OF assms(2)] and assms(3) by auto lemma closest_point_dot: - assumes "convex s" "closed s" "x \ s" - shows "inner (a - closest_point s a) (x - closest_point s a) \ 0" + assumes "convex S" "closed S" "x \ S" + shows "inner (a - closest_point S a) (x - closest_point S a) \ 0" apply (rule any_closest_point_dot[OF assms(1,2) _ assms(3)]) using closest_point_exists[OF assms(2)] and assms(3) apply auto done lemma closest_point_lt: - assumes "convex s" "closed s" "x \ s" "x \ closest_point s a" - shows "dist a (closest_point s a) < dist a x" + assumes "convex S" "closed S" "x \ S" "x \ closest_point S a" + shows "dist a (closest_point S a) < dist a x" apply (rule ccontr) apply (rule_tac notE[OF assms(4)]) apply (rule closest_point_unique[OF assms(1-3), of a]) @@ -5465,34 +5418,34 @@ done lemma closest_point_lipschitz: - assumes "convex s" - and "closed s" "s \ {}" - shows "dist (closest_point s x) (closest_point s y) \ dist x y" + assumes "convex S" + and "closed S" "S \ {}" + shows "dist (closest_point S x) (closest_point S y) \ dist x y" proof - - have "inner (x - closest_point s x) (closest_point s y - closest_point s x) \ 0" - and "inner (y - closest_point s y) (closest_point s x - closest_point s y) \ 0" + have "inner (x - closest_point S x) (closest_point S y - closest_point S x) \ 0" + and "inner (y - closest_point S y) (closest_point S x - closest_point S y) \ 0" apply (rule_tac[!] any_closest_point_dot[OF assms(1-2)]) using closest_point_exists[OF assms(2-3)] apply auto done then show ?thesis unfolding dist_norm and norm_le - using inner_ge_zero[of "(x - closest_point s x) - (y - closest_point s y)"] + using inner_ge_zero[of "(x - closest_point S x) - (y - closest_point S y)"] by (simp add: inner_add inner_diff inner_commute) qed lemma continuous_at_closest_point: - assumes "convex s" - and "closed s" - and "s \ {}" - shows "continuous (at x) (closest_point s)" + assumes "convex S" + and "closed S" + and "S \ {}" + shows "continuous (at x) (closest_point S)" unfolding continuous_at_eps_delta using le_less_trans[OF closest_point_lipschitz[OF assms]] by auto lemma continuous_on_closest_point: - assumes "convex s" - and "closed s" - and "s \ {}" - shows "continuous_on t (closest_point s)" + assumes "convex S" + and "closed S" + and "S \ {}" + shows "continuous_on t (closest_point S)" by (metis continuous_at_imp_continuous_on continuous_at_closest_point[OF assms]) proposition closest_point_in_rel_interior: @@ -5543,119 +5496,84 @@ lemma supporting_hyperplane_closed_point: fixes z :: "'a::{real_inner,heine_borel}" - assumes "convex s" - and "closed s" - and "s \ {}" - and "z \ s" - shows "\a b. \y\s. inner a z < b \ inner a y = b \ (\x\s. inner a x \ b)" + assumes "convex S" + and "closed S" + and "S \ {}" + and "z \ S" + shows "\a b. \y\S. inner a z < b \ inner a y = b \ (\x\S. inner a x \ b)" proof - - obtain y where "y \ s" and y: "\x\s. dist z y \ dist z x" + obtain y where "y \ S" and y: "\x\S. dist z y \ dist z x" by (metis distance_attains_inf[OF assms(2-3)]) show ?thesis - apply (rule_tac x="y - z" in exI) - apply (rule_tac x="inner (y - z) y" in exI) - apply (rule_tac x=y in bexI, rule) - defer - apply rule - defer - apply rule - apply (rule ccontr) - using \y \ s\ - proof - - show "inner (y - z) z < inner (y - z) y" - apply (subst diff_gt_0_iff_gt [symmetric]) - unfolding inner_diff_right[symmetric] and inner_gt_zero_iff - using \y\s\ \z\s\ - apply auto - done - next - fix x - assume "x \ s" - have *: "\u. 0 \ u \ u \ 1 \ dist z y \ dist z ((1 - u) *\<^sub>R y + u *\<^sub>R x)" - using assms(1)[unfolded convex_alt] and y and \x\s\ and \y\s\ by auto - assume "\ inner (y - z) y \ inner (y - z) x" - then obtain v where "v > 0" "v \ 1" "dist (y + v *\<^sub>R (x - y)) z < dist y z" - using closer_point_lemma[of z y x] by (auto simp: inner_diff) - then show False - using *[THEN spec[where x=v]] by (auto simp: dist_commute algebra_simps) - qed auto + proof (intro exI bexI conjI ballI) + show "(y - z) \ z < (y - z) \ y" + by (metis \y \ S\ assms(4) diff_gt_0_iff_gt inner_commute inner_diff_left inner_gt_zero_iff right_minus_eq) + show "(y - z) \ y \ (y - z) \ x" if "x \ S" for x + proof (rule ccontr) + have *: "\u. 0 \ u \ u \ 1 \ dist z y \ dist z ((1 - u) *\<^sub>R y + u *\<^sub>R x)" + using assms(1)[unfolded convex_alt] and y and \x\S\ and \y\S\ by auto + assume "\ (y - z) \ y \ (y - z) \ x" + then obtain v where "v > 0" "v \ 1" "dist (y + v *\<^sub>R (x - y)) z < dist y z" + using closer_point_lemma[of z y x] by (auto simp: inner_diff) + then show False + using *[of v] by (auto simp: dist_commute algebra_simps) + qed + qed (use \y \ S\ in auto) qed lemma separating_hyperplane_closed_point: fixes z :: "'a::{real_inner,heine_borel}" - assumes "convex s" - and "closed s" - and "z \ s" - shows "\a b. inner a z < b \ (\x\s. inner a x > b)" -proof (cases "s = {}") + assumes "convex S" + and "closed S" + and "z \ S" + shows "\a b. inner a z < b \ (\x\S. inner a x > b)" +proof (cases "S = {}") case True then show ?thesis - apply (rule_tac x="-z" in exI) - apply (rule_tac x=1 in exI) - using less_le_trans[OF _ inner_ge_zero[of z]] - apply auto - done + by (simp add: gt_ex) next case False - obtain y where "y \ s" and y: "\x\s. dist z y \ dist z x" + obtain y where "y \ S" and y: "\x. x \ S \ dist z y \ dist z x" by (metis distance_attains_inf[OF assms(2) False]) show ?thesis - apply (rule_tac x="y - z" in exI) - apply (rule_tac x="inner (y - z) z + (norm (y - z))\<^sup>2 / 2" in exI) - apply rule - defer - apply rule - proof - + proof (intro exI conjI ballI) + show "(y - z) \ z < inner (y - z) z + (norm (y - z))\<^sup>2 / 2" + using \y\S\ \z\S\ by auto + next fix x - assume "x \ s" - have "\ 0 < inner (z - y) (x - y)" - apply (rule notI) - apply (drule closer_point_lemma) + assume "x \ S" + have "False" if *: "0 < inner (z - y) (x - y)" proof - - assume "\u>0. u \ 1 \ dist (y + u *\<^sub>R (x - y)) z < dist y z" - then obtain u where "u > 0" "u \ 1" "dist (y + u *\<^sub>R (x - y)) z < dist y z" - by auto - then show False using y[THEN bspec[where x="y + u *\<^sub>R (x - y)"]] - using assms(1)[unfolded convex_alt, THEN bspec[where x=y]] - using \x\s\ \y\s\ by (auto simp: dist_commute algebra_simps) + obtain u where "u > 0" "u \ 1" "dist (y + u *\<^sub>R (x - y)) z < dist y z" + using * closer_point_lemma by blast + then show False using y[of "y + u *\<^sub>R (x - y)"] convexD_alt [OF \convex S\] + using \x\S\ \y\S\ by (auto simp: dist_commute algebra_simps) qed moreover have "0 < (norm (y - z))\<^sup>2" - using \y\s\ \z\s\ by auto + using \y\S\ \z\S\ by auto then have "0 < inner (y - z) (y - z)" unfolding power2_norm_eq_inner by simp - ultimately show "inner (y - z) z + (norm (y - z))\<^sup>2 / 2 < inner (y - z) x" - unfolding power2_norm_eq_inner and not_less - by (auto simp: field_simps inner_commute inner_diff) - qed (insert \y\s\ \z\s\, auto) + ultimately show "(y - z) \ z + (norm (y - z))\<^sup>2 / 2 < (y - z) \ x" + by (force simp: field_simps power2_norm_eq_inner inner_commute inner_diff) + qed qed lemma separating_hyperplane_closed_0: - assumes "convex (s::('a::euclidean_space) set)" - and "closed s" - and "0 \ s" - shows "\a b. a \ 0 \ 0 < b \ (\x\s. inner a x > b)" -proof (cases "s = {}") + assumes "convex (S::('a::euclidean_space) set)" + and "closed S" + and "0 \ S" + shows "\a b. a \ 0 \ 0 < b \ (\x\S. inner a x > b)" +proof (cases "S = {}") case True - have "norm ((SOME i. i\Basis)::'a) = 1" "(SOME i. i\Basis) \ (0::'a)" - defer - apply (subst norm_le_zero_iff[symmetric]) - apply (auto simp: SOME_Basis) - done + have "(SOME i. i\Basis) \ (0::'a)" + by (metis Basis_zero SOME_Basis) then show ?thesis - apply (rule_tac x="SOME i. i\Basis" in exI) - apply (rule_tac x=1 in exI) - using True using DIM_positive[where 'a='a] - apply auto - done + using True zero_less_one by blast next case False then show ?thesis using False using separating_hyperplane_closed_point[OF assms] - apply (elim exE) - unfolding inner_zero_right - apply (rule_tac x=a in exI) - apply (rule_tac x=b in exI, auto) - done + by (metis all_not_in_conv inner_zero_left inner_zero_right less_eq_real_def not_le) qed @@ -5826,19 +5744,13 @@ assumes "convex S" shows "convex (interior S)" unfolding convex_alt Ball_def mem_interior - apply (rule,rule,rule,rule,rule,rule) - apply (elim exE conjE) -proof - +proof clarify fix x y u assume u: "0 \ u" "u \ (1::real)" fix e d assume ed: "ball x e \ S" "ball y d \ S" "0e>0. ball ((1 - u) *\<^sub>R x + u *\<^sub>R y) e \ S" - apply (rule_tac x="min d e" in exI, rule) - unfolding subset_eq - defer - apply rule - proof - + proof (intro exI conjI subsetI) fix z assume "z \ ball ((1 - u) *\<^sub>R x + u *\<^sub>R y) (min d e)" then have "(1- u) *\<^sub>R (z - u *\<^sub>R (y - x)) + u *\<^sub>R (z + (1 - u) *\<^sub>R (y - x)) \ S" @@ -6129,7 +6041,7 @@ and "\s\f. convex s" "\t\f. card t = DIM('a) + 1 \ \t \ {}" shows "\f \ {}" using assms -proof (induct n arbitrary: f) +proof (induction n arbitrary: f) case 0 then show ?case by auto next @@ -6137,45 +6049,39 @@ have "finite f" using \card f = Suc n\ by (auto intro: card_ge_0_finite) show "\f \ {}" - apply (cases "n = DIM('a)") - apply (rule Suc(5)[rule_format]) - unfolding \card f = Suc n\ - proof - - assume ng: "n \ DIM('a)" - then have "\X. \s\f. X s \ \(f - {s})" - apply (rule_tac bchoice) - unfolding ex_in_conv - apply (rule, rule Suc(1)[rule_format]) - unfolding card_Diff_singleton_if[OF \finite f\] \card f = Suc n\ - defer - defer - apply (rule Suc(4)[rule_format]) - defer - apply (rule Suc(5)[rule_format]) - using Suc(3) \finite f\ - apply auto - done - then obtain X where X: "\s\f. X s \ \(f - {s})" by auto + proof (cases "n = DIM('a)") + case True + then show ?thesis + by (simp add: Suc.prems(1) Suc.prems(4)) + next + case False + have "\(f - {s}) \ {}" if "s \ f" for s + proof (rule Suc.IH[rule_format]) + show "card (f - {s}) = n" + by (simp add: Suc.prems(1) \finite f\ that) + show "DIM('a) + 1 \ n" + using False Suc.prems(2) by linarith + show "\t. \t \ f - {s}; card t = DIM('a) + 1\ \ \t \ {}" + by (simp add: Suc.prems(4) subset_Diff_insert) + qed (use Suc in auto) + then have "\s\f. \x. x \ \(f - {s})" + by blast + then obtain X where X: "\s. s\f \ X s \ \(f - {s})" + by metis show ?thesis proof (cases "inj_on X f") case False - then obtain s t where st: "s\t" "s\f" "t\f" "X s = X t" + then obtain s t where "s\t" and st: "s\f" "t\f" "X s = X t" unfolding inj_on_def by auto then have *: "\f = \(f - {s}) \ \(f - {t})" by auto show ?thesis - unfolding * - unfolding ex_in_conv[symmetric] - apply (rule_tac x="X s" in exI, rule) - apply (rule X[rule_format]) - using X st - apply auto - done + by (metis "*" X disjoint_iff_not_equal st) next case True then obtain m p where mp: "m \ p = {}" "m \ p = X ` f" "convex hull m \ convex hull p \ {}" using radon_partition[of "X ` f"] and affine_dependent_biggerset[of "X ` f"] unfolding card_image[OF True] and \card f = Suc n\ - using Suc(3) \finite f\ and ng + using Suc(3) \finite f\ and False by auto have "m \ X ` f" "p \ X ` f" using mp(2) by auto @@ -6192,40 +6098,17 @@ using inj_on_image_Int[OF True gh(3,4)] by auto have "convex hull (X ` h) \ \g" "convex hull (X ` g) \ \h" - apply (rule_tac [!] hull_minimal) - using Suc gh(3-4) - unfolding subset_eq - apply (rule_tac [2] convex_Inter, rule_tac [4] convex_Inter) - prefer 3 - apply rule - proof - - fix x - assume "x \ X ` g" - then obtain y where "y \ g" "x = X y" - unfolding image_iff .. - then show "x \ \h" - using X[THEN bspec[where x=y]] using * f by auto - next - show "\x\X ` h. x \ \g" - proof - fix x - assume "x \ X ` h" - then obtain y where "y \ h" "x = X y" - unfolding image_iff .. - then show "x \ \g" - using X[THEN bspec[where x=y]] using * f by auto - qed - qed auto + by (rule hull_minimal; use X * f in \auto simp: Suc.prems(3) convex_Inter\)+ then show ?thesis unfolding f using mp(3)[unfolded gh] by blast qed - qed auto + qed qed theorem%important helly: fixes f :: "'a::euclidean_space set set" assumes "card f \ DIM('a) + 1" "\s\f. convex s" - and "\t\f. card t = DIM('a) + 1 \ \t \ {}" + and "\t. \t\f; card t = DIM('a) + 1\ \ \t \ {}" shows "\f \ {}" apply%unimportant (rule helly_induct) using assms @@ -6235,70 +6118,76 @@ subsection \Epigraphs of convex functions\ -definition%important "epigraph s (f :: _ \ real) = {xy. fst xy \ s \ f (fst xy) \ snd xy}" - -lemma mem_epigraph: "(x, y) \ epigraph s f \ x \ s \ f x \ y" +definition%important "epigraph S (f :: _ \ real) = {xy. fst xy \ S \ f (fst xy) \ snd xy}" + +lemma mem_epigraph: "(x, y) \ epigraph S f \ x \ S \ f x \ y" unfolding epigraph_def by auto -lemma convex_epigraph: "convex (epigraph s f) \ convex_on s f \ convex s" - unfolding convex_def convex_on_def - unfolding Ball_def split_paired_All epigraph_def - unfolding mem_Collect_eq fst_conv snd_conv fst_add snd_add fst_scaleR snd_scaleR Ball_def[symmetric] - apply safe - defer - apply (erule_tac x=x in allE) - apply (erule_tac x="f x" in allE, safe) - apply (erule_tac x=xa in allE) - apply (erule_tac x="f xa" in allE) - prefer 3 - apply (rule_tac y="u * f a + v * f aa" in order_trans) - defer - apply (auto intro!:mult_left_mono add_mono) - done - -lemma convex_epigraphI: "convex_on s f \ convex s \ convex (epigraph s f)" +lemma convex_epigraph: "convex (epigraph S f) \ convex_on S f \ convex S" +proof safe + assume L: "convex (epigraph S f)" + then show "convex_on S f" + by (auto simp: convex_def convex_on_def epigraph_def) + show "convex S" + using L + apply (clarsimp simp: convex_def convex_on_def epigraph_def) + apply (erule_tac x=x in allE) + apply (erule_tac x="f x" in allE, safe) + apply (erule_tac x=y in allE) + apply (erule_tac x="f y" in allE) + apply (auto simp: ) + done +next + assume "convex_on S f" "convex S" + then show "convex (epigraph S f)" + unfolding convex_def convex_on_def epigraph_def + apply safe + apply (rule_tac [2] y="u * f a + v * f aa" in order_trans) + apply (auto intro!:mult_left_mono add_mono) + done +qed + +lemma convex_epigraphI: "convex_on S f \ convex S \ convex (epigraph S f)" unfolding convex_epigraph by auto -lemma convex_epigraph_convex: "convex s \ convex_on s f \ convex(epigraph s f)" +lemma convex_epigraph_convex: "convex S \ convex_on S f \ convex(epigraph S f)" by (simp add: convex_epigraph) subsubsection%unimportant \Use this to derive general bound property of convex function\ lemma convex_on: - assumes "convex s" - shows "convex_on s f \ - (\k u x. (\i\{1..k::nat}. 0 \ u i \ x i \ s) \ sum u {1..k} = 1 \ + assumes "convex S" + shows "convex_on S f \ + (\k u x. (\i\{1..k::nat}. 0 \ u i \ x i \ S) \ sum u {1..k} = 1 \ f (sum (\i. u i *\<^sub>R x i) {1..k}) \ sum (\i. u i * f(x i)) {1..k})" + unfolding convex_epigraph_convex[OF assms] convex epigraph_def Ball_def mem_Collect_eq unfolding fst_sum snd_sum fst_scaleR snd_scaleR apply safe - apply (drule_tac x=k in spec) - apply (drule_tac x=u in spec) - apply (drule_tac x="\i. (x i, f (x i))" in spec) - apply simp - using assms[unfolded convex] - apply simp - apply (rule_tac y="\i = 1..k. u i * f (fst (x i))" in order_trans) - defer - apply (rule sum_mono) - apply (erule_tac x=i in allE) + apply (drule_tac x=k in spec) + apply (drule_tac x=u in spec) + apply (drule_tac x="\i. (x i, f (x i))" in spec) + apply simp + using assms[unfolded convex] apply simp + apply (rule_tac y="\i = 1..k. u i * f (fst (x i))" in order_trans, force) + apply (rule sum_mono) + apply (erule_tac x=i in allE) unfolding real_scaleR_def - apply (rule mult_left_mono) - using assms[unfolded convex] - apply auto + apply (rule mult_left_mono) + using assms[unfolded convex] apply auto done subsection%unimportant \Convexity of general and special intervals\ lemma is_interval_convex: - fixes s :: "'a::euclidean_space set" - assumes "is_interval s" - shows "convex s" + fixes S :: "'a::euclidean_space set" + assumes "is_interval S" + shows "convex S" proof (rule convexI) fix x y and u v :: real - assume as: "x \ s" "y \ s" "0 \ u" "0 \ v" "u + v = 1" + assume as: "x \ S" "y \ S" "0 \ u" "0 \ v" "u + v = 1" then have *: "u = 1 - v" "1 - v \ 0" and **: "v = 1 - u" "1 - u \ 0" by auto { @@ -6331,7 +6220,7 @@ using **(2) as(3) by (auto simp: field_simps intro!:mult_right_mono) } - ultimately show "u *\<^sub>R x + v *\<^sub>R y \ s" + ultimately show "u *\<^sub>R x + v *\<^sub>R y \ S" apply - apply (rule assms[unfolded is_interval_def, rule_format, OF as(1,2)]) using as(3-) DIM_positive[where 'a='a] @@ -6340,8 +6229,8 @@ qed lemma is_interval_connected: - fixes s :: "'a::euclidean_space set" - shows "is_interval s \ connected s" + fixes S :: "'a::euclidean_space set" + shows "is_interval S \ connected S" using is_interval_convex convex_connected by auto lemma convex_box [simp]: "convex (cbox a b)" "convex (box a (b::'a::euclidean_space))" @@ -6587,8 +6476,8 @@ show "convex (cbox x y)" by (rule convex_box) next - fix s assume "{x, y} \ s" and "convex s" - then show "cbox x y \ s" + fix S assume "{x, y} \ S" and "convex S" + then show "cbox x y \ S" unfolding is_interval_convex_1 [symmetric] is_interval_def Basis_real_def by - (clarify, simp (no_asm_use), fast) qed @@ -6619,66 +6508,53 @@ text \And this is a finite set of vertices.\ lemma unit_cube_convex_hull: - obtains s :: "'a::euclidean_space set" - where "finite s" and "cbox 0 (\Basis) = convex hull s" - apply (rule that[of "{x::'a. \i\Basis. x\i=0 \ x\i=1}"]) - apply (rule finite_subset[of _ "(\s. (\i\Basis. (if i\s then 1 else 0) *\<^sub>R i)::'a) ` Pow Basis"]) - prefer 3 - apply (rule unit_interval_convex_hull, rule) - unfolding mem_Collect_eq -proof - - fix x :: 'a - assume as: "\i\Basis. x \ i = 0 \ x \ i = 1" - show "x \ (\s. \i\Basis. (if i\s then 1 else 0) *\<^sub>R i) ` Pow Basis" - apply (rule image_eqI[where x="{i. i\Basis \ x\i = 1}"]) - using as - apply (subst euclidean_eq_iff, auto) - done -qed auto + obtains S :: "'a::euclidean_space set" + where "finite S" and "cbox 0 (\Basis) = convex hull S" +proof + show "finite {x::'a. \i\Basis. x \ i = 0 \ x \ i = 1}" + proof (rule finite_subset, clarify) + show "finite ((\S. \i\Basis. (if i \ S then 1 else 0) *\<^sub>R i) ` Pow Basis)" + using finite_Basis by blast + fix x :: 'a + assume as: "\i\Basis. x \ i = 0 \ x \ i = 1" + show "x \ (\S. \i\Basis. (if i\S then 1 else 0) *\<^sub>R i) ` Pow Basis" + apply (rule image_eqI[where x="{i. i\Basis \ x\i = 1}"]) + using as + apply (subst euclidean_eq_iff, auto) + done + qed + show "cbox 0 One = convex hull {x. \i\Basis. x \ i = 0 \ x \ i = 1}" + using unit_interval_convex_hull by blast +qed text \Hence any cube (could do any nonempty interval).\ lemma cube_convex_hull: assumes "d > 0" - obtains s :: "'a::euclidean_space set" where - "finite s" and "cbox (x - (\i\Basis. d*\<^sub>Ri)) (x + (\i\Basis. d*\<^sub>Ri)) = convex hull s" + obtains S :: "'a::euclidean_space set" where + "finite S" and "cbox (x - (\i\Basis. d*\<^sub>Ri)) (x + (\i\Basis. d*\<^sub>Ri)) = convex hull S" proof - - let ?d = "(\i\Basis. d*\<^sub>Ri)::'a" + let ?d = "(\i\Basis. d *\<^sub>R i)::'a" have *: "cbox (x - ?d) (x + ?d) = (\y. x - ?d + (2 * d) *\<^sub>R y) ` cbox 0 (\Basis)" - apply (rule set_eqI, rule) - unfolding image_iff - defer - apply (erule bexE) - proof - + proof (intro set_eqI iffI) fix y - assume as: "y\cbox (x - ?d) (x + ?d)" + assume "y \ cbox (x - ?d) (x + ?d)" then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \ cbox 0 (\Basis)" using assms by (simp add: mem_box field_simps inner_simps) - with \0 < d\ show "\z\cbox 0 (\Basis). y = x - ?d + (2 * d) *\<^sub>R z" - by (intro bexI[of _ "inverse (2 * d) *\<^sub>R (y - (x - ?d))"]) auto + with \0 < d\ show "y \ (\y. x - sum (( *\<^sub>R) d) Basis + (2 * d) *\<^sub>R y) ` cbox 0 One" + by (auto intro: image_eqI[where x= "inverse (2 * d) *\<^sub>R (y - (x - ?d))"]) next - fix y z - assume as: "z\cbox 0 (\Basis)" "y = x - ?d + (2*d) *\<^sub>R z" - have "\i. i\Basis \ 0 \ d * (z \ i) \ d * (z \ i) \ d" - using assms as(1)[unfolded mem_box] + fix y + assume "y \ (\y. x - ?d + (2 * d) *\<^sub>R y) ` cbox 0 One" + then obtain z where z: "z \ cbox 0 One" "y = x - ?d + (2*d) *\<^sub>R z" by auto then show "y \ cbox (x - ?d) (x + ?d)" - unfolding as(2) mem_box - apply - - apply rule - using as(1)[unfolded mem_box] - apply (erule_tac x=i in ballE) - using assms - apply (auto simp: inner_simps) - done + using z assms by (auto simp: mem_box inner_simps) qed - obtain s where "finite s" "cbox 0 (\Basis::'a) = convex hull s" + obtain S where "finite S" "cbox 0 (\Basis::'a) = convex hull S" using unit_cube_convex_hull by auto then show ?thesis - apply (rule_tac that[of "(\y. x - ?d + (2 * d) *\<^sub>R y)` s"]) - unfolding * and convex_hull_affinity - apply auto - done + by (rule_tac that[of "(\y. x - ?d + (2 * d) *\<^sub>R y)` S"]) (auto simp: convex_hull_affinity *) qed subsection%unimportant\Representation of any interval as a finite convex hull\ @@ -6738,18 +6614,18 @@ lemma closed_interval_as_convex_hull: fixes a :: "'a::euclidean_space" - obtains s where "finite s" "cbox a b = convex hull s" + obtains S where "finite S" "cbox a b = convex hull S" proof (cases "cbox a b = {}") case True with convex_hull_empty that show ?thesis by blast next case False - obtain s::"'a set" where "finite s" and eq: "cbox 0 One = convex hull s" + obtain S::"'a set" where "finite S" and eq: "cbox 0 One = convex hull S" by (blast intro: unit_cube_convex_hull) have lin: "linear (\x. \k\Basis. ((b \ k - a \ k) * (x \ k)) *\<^sub>R k)" by (rule linear_compose_sum) (auto simp: algebra_simps linearI) - have "finite ((+) a ` (\x. \k\Basis. ((b \ k - a \ k) * (x \ k)) *\<^sub>R k) ` s)" - by (rule finite_imageI \finite s\)+ + have "finite ((+) a ` (\x. \k\Basis. ((b \ k - a \ k) * (x \ k)) *\<^sub>R k) ` S)" + by (rule finite_imageI \finite S\)+ then show ?thesis apply (rule that) apply (simp add: convex_hull_translation convex_hull_linear_image [OF lin, symmetric]) @@ -6761,31 +6637,23 @@ subsection%unimportant \Bounded convex function on open set is continuous\ lemma convex_on_bounded_continuous: - fixes s :: "('a::real_normed_vector) set" - assumes "open s" - and "convex_on s f" - and "\x\s. \f x\ \ b" - shows "continuous_on s f" + fixes S :: "('a::real_normed_vector) set" + assumes "open S" + and "convex_on S f" + and "\x\S. \f x\ \ b" + shows "continuous_on S f" apply (rule continuous_at_imp_continuous_on) unfolding continuous_at_real_range proof (rule,rule,rule) fix x and e :: real - assume "x \ s" "e > 0" + assume "x \ S" "e > 0" define B where "B = \b\ + 1" - have B: "0 < B" "\x. x\s \ \f x\ \ B" - unfolding B_def - defer - apply (drule assms(3)[rule_format]) - apply auto - done - obtain k where "k > 0" and k: "cball x k \ s" - using assms(1)[unfolded open_contains_cball, THEN bspec[where x=x]] - using \x\s\ by auto + then have B: "0 < B""\x. x\S \ \f x\ \ B" + using assms(3) by auto + obtain k where "k > 0" and k: "cball x k \ S" + using \x \ S\ assms(1) open_contains_cball_eq by blast show "\d>0. \x'. norm (x' - x) < d \ \f x' - f x\ < e" - apply (rule_tac x="min (k / 2) (e / (2 * B) * k)" in exI) - apply rule - defer - proof (rule, rule) + proof (intro exI conjI allI impI) fix y assume as: "norm (y - x) < min (k / 2) (e / (2 * B) * k)" show "\f y - f x\ < e" @@ -6795,22 +6663,16 @@ have "2 < t" "0k>0\ by (auto simp:field_simps) - have "y \ s" - apply (rule k[unfolded subset_eq,rule_format]) + have "y \ S" + apply (rule k[THEN subsetD]) unfolding mem_cball dist_norm apply (rule order_trans[of _ "2 * norm (x - y)"]) using as by (auto simp: field_simps norm_minus_commute) { define w where "w = x + t *\<^sub>R (y - x)" - have "w \ s" - unfolding w_def - apply (rule k[unfolded subset_eq,rule_format]) - unfolding mem_cball dist_norm - unfolding t_def - using \k>0\ - apply auto - done + have "w \ S" + using \k>0\ by (auto simp: dist_norm t_def w_def k[THEN subsetD]) have "(1 / t) *\<^sub>R x + - x + ((t - 1) / t) *\<^sub>R x = (1 / t - 1 + (t - 1) / t) *\<^sub>R x" by (auto simp: algebra_simps) also have "\ = 0" @@ -6818,32 +6680,22 @@ finally have w: "(1 / t) *\<^sub>R w + ((t - 1) / t) *\<^sub>R x = y" unfolding w_def using False and \t > 0\ by (auto simp: algebra_simps) - have "2 * B < e * t" + have 2: "2 * B < e * t" unfolding t_def using \0 < e\ \0 < k\ \B > 0\ and as and False by (auto simp:field_simps) - then have "(f w - f x) / t < e" - using B(2)[OF \w\s\] and B(2)[OF \x\s\] - using \t > 0\ by (auto simp:field_simps) - then have th1: "f y - f x < e" - apply - - apply (rule le_less_trans) - defer - apply assumption + have "f y - f x \ (f w - f x) / t" using assms(2)[unfolded convex_on_def,rule_format,of w x "1/t" "(t - 1)/t", unfolded w] - using \0 < t\ \2 < t\ and \x \ s\ \w \ s\ + using \0 < t\ \2 < t\ and \x \ S\ \w \ S\ by (auto simp:field_simps) + also have "... < e" + using B(2)[OF \w\S\] and B(2)[OF \x\S\] 2 \t > 0\ by (auto simp: field_simps) + finally have th1: "f y - f x < e" . } moreover { define w where "w = x - t *\<^sub>R (y - x)" - have "w \ s" - unfolding w_def - apply (rule k[unfolded subset_eq,rule_format]) - unfolding mem_cball dist_norm - unfolding t_def - using \k > 0\ - apply auto - done + have "w \ S" + using \k > 0\ by (auto simp: dist_norm t_def w_def k[THEN subsetD]) have "(1 / (1 + t)) *\<^sub>R x + (t / (1 + t)) *\<^sub>R x = (1 / (1 + t) + t / (1 + t)) *\<^sub>R x" by (auto simp: algebra_simps) also have "\ = x" @@ -6856,12 +6708,12 @@ using \0 < e\ \0 < k\ \B > 0\ and as and False by (auto simp:field_simps) then have *: "(f w - f y) / t < e" - using B(2)[OF \w\s\] and B(2)[OF \y\s\] + using B(2)[OF \w\S\] and B(2)[OF \y\S\] using \t > 0\ by (auto simp:field_simps) have "f x \ 1 / (1 + t) * f w + (t / (1 + t)) * f y" using assms(2)[unfolded convex_on_def,rule_format,of w y "1/(1+t)" "t / (1+t)",unfolded w] - using \0 < t\ \2 < t\ and \y \ s\ \w \ s\ + using \0 < t\ \2 < t\ and \y \ S\ \w \ S\ by (auto simp:field_simps) also have "\ = (f w + t * f y) / (1 + t)" using \t > 0\ by (auto simp: divide_simps) @@ -6950,11 +6802,7 @@ by (simp add: dist_norm abs_le_iff algebra_simps) show "cball x d \ convex hull c" unfolding 2 - apply clarsimp - apply (simp only: dist_norm) - apply (subst inner_diff_left [symmetric], simp) - apply (erule (1) order_trans [OF Basis_le_norm]) - done + by (clarsimp simp: dist_norm) (metis inner_commute inner_diff_right norm_bound_Basis_le) have e': "e = (\(i::'a)\Basis. d)" by (simp add: d_def DIM_positive) show "convex hull c \ cball x e" diff -r b249fab48c76 -r d2daeef3ce47 src/HOL/Analysis/Derivative.thy --- a/src/HOL/Analysis/Derivative.thy Wed May 02 12:47:56 2018 +0100 +++ b/src/HOL/Analysis/Derivative.thy Wed May 02 12:48:08 2018 +0100 @@ -373,77 +373,76 @@ lemma frechet_derivative_unique_within: fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" - assumes "(f has_derivative f') (at x within s)" - and "(f has_derivative f'') (at x within s)" - and "\i\Basis. \e>0. \d. 0 < \d\ \ \d\ < e \ (x + d *\<^sub>R i) \ s" + assumes "(f has_derivative f') (at x within S)" + and "(f has_derivative f'') (at x within S)" + and "\i\Basis. \e>0. \d. 0 < \d\ \ \d\ < e \ (x + d *\<^sub>R i) \ S" shows "f' = f''" proof - note as = assms(1,2)[unfolded has_derivative_def] then interpret f': bounded_linear f' by auto from as interpret f'': bounded_linear f'' by auto - have "x islimpt s" unfolding islimpt_approachable + have "x islimpt S" unfolding islimpt_approachable proof (rule, rule) fix e :: real assume "e > 0" - obtain d where "0 < \d\" and "\d\ < e" and "x + d *\<^sub>R (SOME i. i \ Basis) \ s" + obtain d where "0 < \d\" and "\d\ < e" and "x + d *\<^sub>R (SOME i. i \ Basis) \ S" using assms(3) SOME_Basis \e>0\ by blast - then show "\x'\s. x' \ x \ dist x' x < e" + then show "\x'\S. x' \ x \ dist x' x < e" apply (rule_tac x="x + d *\<^sub>R (SOME i. i \ Basis)" in bexI) unfolding dist_norm apply (auto simp: SOME_Basis nonzero_Basis) done qed - then have *: "netlimit (at x within s) = x" + then have *: "netlimit (at x within S) = x" apply (auto intro!: netlimit_within) by (metis trivial_limit_within) show ?thesis - apply (rule linear_eq_stdbasis) - unfolding linear_conv_bounded_linear - apply (rule as(1,2)[THEN conjunct1])+ - proof (rule, rule ccontr) + proof (rule linear_eq_stdbasis) + show "linear f'" "linear f''" + unfolding linear_conv_bounded_linear using as by auto + next fix i :: 'a assume i: "i \ Basis" define e where "e = norm (f' i - f'' i)" - assume "f' i \ f'' i" - then have "e > 0" - unfolding e_def by auto - obtain d where d: - "0 < d" - "(\xa. xa\s \ 0 < dist xa x \ dist xa x < d \ - dist ((f xa - f x - f' (xa - x)) /\<^sub>R norm (xa - x) - - (f xa - f x - f'' (xa - x)) /\<^sub>R norm (xa - x)) (0 - 0) < e)" - using tendsto_diff [OF as(1,2)[THEN conjunct2]] - unfolding * Lim_within - using \e>0\ by blast - obtain c where c: "0 < \c\" "\c\ < d \ x + c *\<^sub>R i \ s" - using assms(3) i d(1) by blast - have *: "norm (- ((1 / \c\) *\<^sub>R f' (c *\<^sub>R i)) + (1 / \c\) *\<^sub>R f'' (c *\<^sub>R i)) = + show "f' i = f'' i" + proof (rule ccontr) + assume "f' i \ f'' i" + then have "e > 0" + unfolding e_def by auto + obtain d where d: + "0 < d" + "(\y. y\S \ 0 < dist y x \ dist y x < d \ + dist ((f y - f x - f' (y - x)) /\<^sub>R norm (y - x) - + (f y - f x - f'' (y - x)) /\<^sub>R norm (y - x)) (0 - 0) < e)" + using tendsto_diff [OF as(1,2)[THEN conjunct2]] + unfolding * Lim_within + using \e>0\ by blast + obtain c where c: "0 < \c\" "\c\ < d \ x + c *\<^sub>R i \ S" + using assms(3) i d(1) by blast + have *: "norm (- ((1 / \c\) *\<^sub>R f' (c *\<^sub>R i)) + (1 / \c\) *\<^sub>R f'' (c *\<^sub>R i)) = norm ((1 / \c\) *\<^sub>R (- (f' (c *\<^sub>R i)) + f'' (c *\<^sub>R i)))" - unfolding scaleR_right_distrib by auto - also have "\ = norm ((1 / \c\) *\<^sub>R (c *\<^sub>R (- (f' i) + f'' i)))" - unfolding f'.scaleR f''.scaleR - unfolding scaleR_right_distrib scaleR_minus_right - by auto - also have "\ = e" - unfolding e_def - using c(1) - using norm_minus_cancel[of "f' i - f'' i"] - by auto - finally show False - using c - using d(2)[of "x + c *\<^sub>R i"] - unfolding dist_norm - unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff - scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib - using i - by (auto simp: inverse_eq_divide) + unfolding scaleR_right_distrib by auto + also have "\ = norm ((1 / \c\) *\<^sub>R (c *\<^sub>R (- (f' i) + f'' i)))" + unfolding f'.scaleR f''.scaleR + unfolding scaleR_right_distrib scaleR_minus_right + by auto + also have "\ = e" + unfolding e_def + using c(1) + using norm_minus_cancel[of "f' i - f'' i"] + by auto + finally show False + using c + using d(2)[of "x + c *\<^sub>R i"] + unfolding dist_norm + unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff + scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib + using i + by (auto simp: inverse_eq_divide) + qed qed qed -lemma frechet_derivative_unique_at: - "(f has_derivative f') (at x) \ (f has_derivative f'') (at x) \ f' = f''" - by (rule has_derivative_unique) - lemma frechet_derivative_unique_within_closed_interval: fixes f::"'a::euclidean_space \ 'b::real_normed_vector" assumes "\i\Basis. a\i < b\i" @@ -506,12 +505,12 @@ from assms(1) have *: "at x within box a b = at x" by (metis at_within_interior interior_open open_box) from assms(2,3) [unfolded *] show "f' = f''" - by (rule frechet_derivative_unique_at) + by (rule has_derivative_unique) qed lemma frechet_derivative_at: "(f has_derivative f') (at x) \ f' = frechet_derivative f (at x)" - apply (rule frechet_derivative_unique_at[of f]) + apply (rule has_derivative_unique[of f]) apply assumption unfolding frechet_derivative_works[symmetric] using differentiable_def @@ -1197,13 +1196,13 @@ lemma has_derivative_inverse_basic: fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector" - assumes "(f has_derivative f') (at (g y))" - and "bounded_linear g'" + assumes derf: "(f has_derivative f') (at (g y))" + and ling': "bounded_linear g'" and "g' \ f' = id" - and "continuous (at y) g" - and "open t" - and "y \ t" - and "\z\t. f (g z) = z" + and contg: "continuous (at y) g" + and "open T" + and "y \ T" + and fg: "\z. z \ T \ f (g z) = z" shows "(g has_derivative g') (at y)" proof - interpret f': bounded_linear f' @@ -1214,70 +1213,48 @@ using bounded_linear.pos_bounded[OF assms(2)] by blast have lem1: "\e>0. \d>0. \z. norm (z - y) < d \ norm (g z - g y - g'(z - y)) \ e * norm (g z - g y)" - proof (rule, rule) + proof (intro allI impI) fix e :: real assume "e > 0" with C(1) have *: "e / C > 0" by auto - obtain d0 where d0: - "0 < d0" - "\ya. norm (ya - g y) < d0 \ norm (f ya - f (g y) - f' (ya - g y)) \ e / C * norm (ya - g y)" - using assms(1) - unfolding has_derivative_at_alt - using * by blast - obtain d1 where d1: - "0 < d1" - "\x. 0 < dist x y \ dist x y < d1 \ dist (g x) (g y) < d0" - using assms(4) - unfolding continuous_at Lim_at - using d0(1) by blast - obtain d2 where d2: - "0 < d2" - "\ya. dist ya y < d2 \ ya \ t" - using assms(5) - unfolding open_dist - using assms(6) by blast + obtain d0 where "0 < d0" and d0: + "\u. norm (u - g y) < d0 \ norm (f u - f (g y) - f' (u - g y)) \ e / C * norm (u - g y)" + using derf * unfolding has_derivative_at_alt by blast + obtain d1 where "0 < d1" and d1: "\x. \0 < dist x y; dist x y < d1\ \ dist (g x) (g y) < d0" + using contg \0 < d0\ unfolding continuous_at Lim_at by blast + obtain d2 where "0 < d2" and d2: "\u. dist u y < d2 \ u \ T" + using \open T\ \y \ T\ unfolding open_dist by blast obtain d where d: "0 < d" "d < d1" "d < d2" - using real_lbound_gt_zero[OF d1(1) d2(1)] by blast - then show "\d>0. \z. norm (z - y) < d \ norm (g z - g y - g' (z - y)) \ e * norm (g z - g y)" - apply (rule_tac x=d in exI) - apply rule - defer - apply rule - apply rule - proof - + using real_lbound_gt_zero[OF \0 < d1\ \0 < d2\] by blast + show "\d>0. \z. norm (z - y) < d \ norm (g z - g y - g' (z - y)) \ e * norm (g z - g y)" + proof (intro exI allI impI conjI) fix z assume as: "norm (z - y) < d" - then have "z \ t" + then have "z \ T" using d2 d unfolding dist_norm by auto have "norm (g z - g y - g' (z - y)) \ norm (g' (f (g z) - y - f' (g z - g y)))" unfolding g'.diff f'.diff - unfolding assms(3)[unfolded o_def id_def, THEN fun_cong] - unfolding assms(7)[rule_format,OF \z\t\] - apply (subst norm_minus_cancel[symmetric]) - apply auto - done + unfolding assms(3)[unfolded o_def id_def, THEN fun_cong] fg[OF \z\T\] + by (simp add: norm_minus_commute) also have "\ \ norm (f (g z) - y - f' (g z - g y)) * C" by (rule C(2)) also have "\ \ (e / C) * norm (g z - g y) * C" - apply (rule mult_right_mono) - apply (rule d0(2)[rule_format,unfolded assms(7)[rule_format,OF \y\t\]]) - apply (cases "z = y") - defer - apply (rule d1(2)[unfolded dist_norm,rule_format]) - using as d C d0 - apply auto - done + proof - + have "norm (g z - g y) < d0" + by (metis as cancel_comm_monoid_add_class.diff_cancel d(2) \0 < d0\ d1 diff_gt_0_iff_gt diff_strict_mono dist_norm dist_self zero_less_dist_iff) + then show ?thesis + by (metis C(1) \y \ T\ d0 fg real_mult_le_cancel_iff1) + qed also have "\ \ e * norm (g z - g y)" using C by (auto simp add: field_simps) finally show "norm (g z - g y - g' (z - y)) \ e * norm (g z - g y)" by simp - qed auto + qed (use d in auto) qed have *: "(0::real) < 1 / 2" by auto - obtain d where d: - "0 < d" - "\z. norm (z - y) < d \ norm (g z - g y - g' (z - y)) \ 1 / 2 * norm (g z - g y)" + obtain d where "0 < d" and d: + "\z. norm (z - y) < d \ norm (g z - g y - g' (z - y)) \ 1/2 * norm (g z - g y)" using lem1 * by blast define B where "B = C * 2" have "B > 0" @@ -1287,51 +1264,37 @@ have "norm (g z - g y) \ norm(g' (z - y)) + norm ((g z - g y) - g'(z - y))" by (rule norm_triangle_sub) also have "\ \ norm (g' (z - y)) + 1 / 2 * norm (g z - g y)" - apply (rule add_left_mono) - using d and z - apply auto - done + by (rule add_left_mono) (use d z in auto) also have "\ \ norm (z - y) * C + 1 / 2 * norm (g z - g y)" - apply (rule add_right_mono) - using C - apply auto - done + by (rule add_right_mono) (use C in auto) finally show "norm (g z - g y) \ B * norm (z - y)" unfolding B_def by (auto simp add: field_simps) qed show ?thesis unfolding has_derivative_at_alt - apply rule - apply (rule assms) - apply rule - apply rule - proof - + proof (intro conjI assms allI impI) fix e :: real assume "e > 0" then have *: "e / B > 0" by (metis \B > 0\ divide_pos_pos) - obtain d' where d': - "0 < d'" - "\z. norm (z - y) < d' \ norm (g z - g y - g' (z - y)) \ e / B * norm (g z - g y)" + obtain d' where "0 < d'" and d': + "\z. norm (z - y) < d' \ norm (g z - g y - g' (z - y)) \ e / B * norm (g z - g y)" using lem1 * by blast obtain k where k: "0 < k" "k < d" "k < d'" - using real_lbound_gt_zero[OF d(1) d'(1)] by blast + using real_lbound_gt_zero[OF \0 < d\ \0 < d'\] by blast show "\d>0. \ya. norm (ya - y) < d \ norm (g ya - g y - g' (ya - y)) \ e * norm (ya - y)" - apply (rule_tac x=k in exI) - apply auto - proof - + proof (intro exI allI impI conjI) fix z assume as: "norm (z - y) < k" then have "norm (g z - g y - g' (z - y)) \ e / B * norm(g z - g y)" using d' k by auto also have "\ \ e * norm (z - y)" unfolding times_divide_eq_left pos_divide_le_eq[OF \B>0\] - using lem2[of z] - using k as using \e > 0\ + using lem2[of z] k as \e > 0\ by (auto simp add: field_simps) finally show "norm (g z - g y - g' (z - y)) \ e * norm (z - y)" by simp - qed(insert k, auto) + qed (use k in auto) qed qed @@ -1344,25 +1307,22 @@ and "g' \ f' = id" and "continuous (at (f x)) g" and "g (f x) = x" - and "open t" - and "f x \ t" - and "\y\t. f (g y) = y" + and "open T" + and "f x \ T" + and "\y. y \ T \ f (g y) = y" shows "(g has_derivative g') (at (f x))" - apply (rule has_derivative_inverse_basic) - using assms - apply auto - done + by (rule has_derivative_inverse_basic) (use assms in auto) text \This is the version in Dieudonne', assuming continuity of f and g.\ lemma has_derivative_inverse_dieudonne: fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector" - assumes "open s" - and "open (f ` s)" - and "continuous_on s f" - and "continuous_on (f ` s) g" - and "\x\s. g (f x) = x" - and "x \ s" + assumes "open S" + and "open (f ` S)" + and "continuous_on S f" + and "continuous_on (f ` S) g" + and "\x. x \ S \ g (f x) = x" + and "x \ S" and "(f has_derivative f') (at x)" and "bounded_linear g'" and "g' \ f' = id" @@ -1377,11 +1337,11 @@ lemma has_derivative_inverse: fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector" - assumes "compact s" - and "x \ s" - and "f x \ interior (f ` s)" - and "continuous_on s f" - and "\y\s. g (f y) = y" + assumes "compact S" + and "x \ S" + and fx: "f x \ interior (f ` S)" + and "continuous_on S f" + and "\y. y \ S \ g (f y) = y" and "(f has_derivative f') (at x)" and "bounded_linear g'" and "g' \ f' = id" @@ -1389,20 +1349,17 @@ proof - { fix y - assume "y \ interior (f ` s)" - then obtain x where "x \ s" and *: "y = f x" - unfolding image_iff - using interior_subset - by auto + assume "y \ interior (f ` S)" + then obtain x where "x \ S" and *: "y = f x" + by (meson imageE interior_subset subsetCE) have "f (g y) = y" - unfolding * and assms(5)[rule_format,OF \x\s\] .. + unfolding * and assms(5)[rule_format,OF \x\S\] .. } note * = this show ?thesis - apply (rule has_derivative_inverse_basic_x[OF assms(6-8)]) - apply (rule continuous_on_interior[OF _ assms(3)]) - apply (rule continuous_on_inv[OF assms(4,1)]) - apply (rule assms(2,5) assms(5)[rule_format] open_interior assms(3))+ - apply (metis *) + apply (rule has_derivative_inverse_basic_x[OF assms(6-8), where T = "interior (f ` S)"]) + apply (rule continuous_on_interior[OF _ fx]) + apply (rule continuous_on_inv) + apply (simp_all add: assms *) done qed @@ -1411,13 +1368,13 @@ lemma brouwer_surjective: fixes f :: "'n::euclidean_space \ 'n" - assumes "compact t" - and "convex t" - and "t \ {}" - and "continuous_on t f" - and "\x\s. \y\t. x + (y - f y) \ t" - and "x \ s" - shows "\y\t. f y = x" + assumes "compact T" + and "convex T" + and "T \ {}" + and "continuous_on T f" + and "\x y. \x\S; y\T\ \ x + (y - f y) \ T" + and "x \ S" + shows "\y\T. f y = x" proof - have *: "\x y. f y = x \ x + (y - f y) = y" by (auto simp add: algebra_simps) @@ -1432,10 +1389,10 @@ lemma brouwer_surjective_cball: fixes f :: "'n::euclidean_space \ 'n" - assumes "e > 0" - and "continuous_on (cball a e) f" - and "\x\s. \y\cball a e. x + (y - f y) \ cball a e" - and "x \ s" + assumes "continuous_on (cball a e) f" + and "e > 0" + and "x \ S" + and "\x y. \x\S; y\cball a e\ \ x + (y - f y) \ cball a e" shows "\y\cball a e. f y = x" apply (rule brouwer_surjective) apply (rule compact_cball convex_cball)+ @@ -1448,14 +1405,14 @@ lemma sussmann_open_mapping: fixes f :: "'a::real_normed_vector \ 'b::euclidean_space" - assumes "open s" - and "continuous_on s f" - and "x \ s" + assumes "open S" + and "continuous_on S f" + and "x \ S" and "(f has_derivative f') (at x)" and "bounded_linear g'" "f' \ g' = id" - and "t \ s" - and "x \ interior t" - shows "f x \ interior (f ` t)" + and "T \ S" + and "x \ interior T" + shows "f x \ interior (f ` T)" proof - interpret f': bounded_linear f' using assms @@ -1473,31 +1430,17 @@ using assms(4) unfolding has_derivative_at_alt using * by blast - obtain e1 where e1: "0 < e1" "cball x e1 \ t" + obtain e1 where e1: "0 < e1" "cball x e1 \ T" using assms(8) unfolding mem_interior_cball by blast have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B" using real_lbound_gt_zero[OF *] by blast - have "\z\cball (f x) (e / 2). \y\cball (f x) e. f (x + g' (y - f x)) = z" - apply rule - apply (rule brouwer_surjective_cball[where s="cball (f x) (e/2)"]) - prefer 3 - apply rule - apply rule - proof- - show "continuous_on (cball (f x) e) (\y. f (x + g' (y - f x)))" - unfolding g'.diff - apply (rule continuous_on_compose[of _ _ f, unfolded o_def]) - apply (rule continuous_intros linear_continuous_on[OF assms(5)])+ - apply (rule continuous_on_subset[OF assms(2)]) - apply rule - apply (unfold image_iff) - apply (erule bexE) + have lem: "\y\cball (f x) e. f (x + g' (y - f x)) = z" if "z\cball (f x) (e / 2)" for z + proof (rule brouwer_surjective_cball) + have z: "z \ S" if as: "y \cball (f x) e" "z = x + (g' y - g' (f x))" for y z proof- - fix y z - assume as: "y \cball (f x) e" "z = x + (g' y - g' (f x))" have "dist x z = norm (g' (f x) - g' y)" unfolding as(2) and dist_norm by auto also have "\ \ norm (f x - y) * B" @@ -1516,9 +1459,16 @@ finally have "z \ cball x e1" unfolding mem_cball by force - then show "z \ s" + then show "z \ S" using e1 assms(7) by auto qed + show "continuous_on (cball (f x) e) (\y. f (x + g' (y - f x)))" + unfolding g'.diff + apply (rule continuous_on_compose[of _ _ f, unfolded o_def]) + apply (rule continuous_intros linear_continuous_on[OF assms(5)])+ + apply (rule continuous_on_subset[OF assms(2)]) + using z + by blast next fix y z assume as: "y \ cball (f x) (e / 2)" "z \ cball (f x) e" @@ -1528,7 +1478,7 @@ apply (rule mult_right_mono) using as(2)[unfolded mem_cball dist_norm] and B unfolding norm_minus_commute - apply auto + apply auto done also have "\ < e0" using e and B @@ -1563,7 +1513,7 @@ finally show "y + (z - f (x + g' (z - f x))) \ cball (f x) e" unfolding mem_cball dist_norm by auto - qed (insert e, auto) note lem = this + qed (use e that in auto) show ?thesis unfolding mem_interior apply (rule_tac x="e/2" in exI) @@ -1589,13 +1539,13 @@ done also have "\ \ e1" using e B unfolding less_divide_eq by auto - finally have "x + g'(z - f x) \ t" + finally have "x + g'(z - f x) \ T" apply - apply (rule e1(2)[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm apply auto done - then show "y \ f ` t" + then show "y \ f ` T" using z by auto qed (insert e, auto) qed @@ -1750,9 +1700,9 @@ fixes f :: "'n::euclidean_space \ 'm::euclidean_space" assumes "a \ s" and "open s" - and "bounded_linear g'" + and bling: "bounded_linear g'" and "g' \ f' a = id" - and "\x. x \ s \ (f has_derivative f' x) (at x)" + and derf: "\x. x \ s \ (f has_derivative f' x) (at x)" and "\e. e > 0 \ \d>0. \x. dist a x < d \ onorm (\v. f' x v - f' a v) < e" obtains r where "r > 0" "ball a r \ s" "inj_on f (ball a r)" proof - @@ -1760,11 +1710,7 @@ using assms by auto note f'g' = assms(4)[unfolded id_def o_def,THEN cong] have "g' (f' a (\Basis)) = (\Basis)" "(\Basis) \ (0::'n)" - defer - apply (subst euclidean_eq_iff) - using f'g' - apply auto - done + using f'g' by auto then have *: "0 < onorm g'" unfolding onorm_pos_lt[OF assms(3)] by fastforce @@ -1812,17 +1758,11 @@ have *: "(\v. v - g' (f' u v)) = g' \ (\w. f' a w - f' u w)" unfolding o_def and diff using f'g' by auto + have blin: "bounded_linear (f' a)" + using \a \ s\ derf by blast show "(ph has_derivative (\v. v - g' (f' u v))) (at u within ball a d)" - unfolding ph' * - apply (simp add: comp_def) - apply (rule bounded_linear.has_derivative[OF assms(3)]) - apply (rule derivative_intros) - defer - apply (rule has_derivative_sub[where g'="\x.0",unfolded diff_0_right]) - apply (rule has_derivative_at_withinI) - using assms(5) and \u \ s\ \a \ s\ - apply (auto intro!: derivative_intros bounded_linear.has_derivative[of _ "\x. x"] has_derivative_bounded_linear) - done + unfolding ph' * comp_def + by (rule \u \ s\ derivative_eq_intros has_derivative_at_withinI [OF derf] bounded_linear.has_derivative [OF blin] bounded_linear.has_derivative [OF bling] |simp)+ have **: "bounded_linear (\x. f' u x - f' a x)" "bounded_linear (\x. f' a x - f' u x)" apply (rule_tac[!] bounded_linear_sub) apply (rule_tac[!] has_derivative_bounded_linear) @@ -1896,21 +1836,20 @@ qed qed -lemma has_derivative_sequence_lipschitz: +lemma has_derivative_sequence_Lipschitz: fixes f :: "nat \ 'a::real_normed_vector \ 'b::real_normed_vector" - assumes "convex s" - and "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" - and "\e>0. \N. \n\N. \x\s. \h. norm (f' n x h - g' x h) \ e * norm h" - shows "\e>0. \N. \m\N. \n\N. \x\s. \y\s. + assumes "convex S" + and "\n x. x \ S \ ((f n) has_derivative (f' n x)) (at x within S)" + and "\e. e > 0 \ \N. \n\N. \x\S. \h. norm (f' n x h - g' x h) \ e * norm h" + and "e > 0" + shows "\N. \m\N. \n\N. \x\S. \y\S. norm ((f m x - f n x) - (f m y - f n y)) \ e * norm (x - y)" -proof (rule, rule) - fix e :: real - assume "e > 0" - then have *: "2 * (1/2* e) = e" "1/2 * e >0" - by auto - obtain N where "\n\N. \x\s. \h. norm (f' n x h - g' x h) \ 1 / 2 * e * norm h" +proof - + have *: "2 * (1/2* e) = e" "1/2 * e >0" + using \e>0\ by auto + obtain N where "\n\N. \x\S. \h. norm (f' n x h - g' x h) \ 1 / 2 * e * norm h" using assms(3) *(2) by blast - then show "\N. \m\N. \n\N. \x\s. \y\s. norm (f m x - f n x - (f m y - f n y)) \ e * norm (x - y)" + then show "\N. \m\N. \n\N. \x\S. \y\S. norm (f m x - f n x - (f m y - f n y)) \ e * norm (x - y)" apply (rule_tac x=N in exI) apply (rule has_derivative_sequence_lipschitz_lemma[where e="1/2 *e", unfolded *]) using assms \e > 0\ @@ -1920,22 +1859,22 @@ lemma has_derivative_sequence: fixes f :: "nat \ 'a::real_normed_vector \ 'b::banach" - assumes "convex s" - and "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" - and "\e>0. \N. \n\N. \x\s. \h. norm (f' n x h - g' x h) \ e * norm h" - and "x0 \ s" + assumes "convex S" + and "\n x. x \ S \ ((f n) has_derivative (f' n x)) (at x within S)" + and "\e. e > 0 \ \N. \n\N. \x\S. \h. norm (f' n x h - g' x h) \ e * norm h" + and "x0 \ S" and "((\n. f n x0) \ l) sequentially" - shows "\g. \x\s. ((\n. f n x) \ g x) sequentially \ (g has_derivative g'(x)) (at x within s)" + shows "\g. \x\S. ((\n. f n x) \ g x) sequentially \ (g has_derivative g'(x)) (at x within S)" proof - - have lem1: "\e>0. \N. \m\N. \n\N. \x\s. \y\s. + have lem1: "\e. e > 0 \ \N. \m\N. \n\N. \x\S. \y\S. norm ((f m x - f n x) - (f m y - f n y)) \ e * norm (x - y)" - using assms(1,2,3) by (rule has_derivative_sequence_lipschitz) - have "\g. \x\s. ((\n. f n x) \ g x) sequentially" + using assms(1,2,3) by (rule has_derivative_sequence_Lipschitz) + have "\g. \x\S. ((\n. f n x) \ g x) sequentially" apply (rule bchoice) unfolding convergent_eq_Cauchy proof fix x - assume "x \ s" + assume "x \ S" show "Cauchy (\n. f n x)" proof (cases "x = x0") case True @@ -1945,7 +1884,7 @@ case False show ?thesis unfolding Cauchy_def - proof (rule, rule) + proof (intro allI impI) fix e :: real assume "e > 0" hence *: "e / 2 > 0" "e / 2 / norm (x - x0) > 0" using False by auto @@ -1955,12 +1894,11 @@ using *(1) by blast obtain N where N: "\m\N. \n\N. - \xa\s. \y\s. norm (f m xa - f n xa - (f m y - f n y)) \ + \xa\S. \y\S. norm (f m xa - f n xa - (f m y - f n y)) \ e / 2 / norm (x - x0) * norm (xa - y)" using lem1 *(2) by blast show "\M. \m\M. \n\M. dist (f m x) (f n x) < e" - apply (rule_tac x="max M N" in exI) - proof rule+ + proof (intro exI allI impI) fix m n assume as: "max M N \m" "max M N\n" have "dist (f m x) (f n x) \ @@ -1968,7 +1906,7 @@ unfolding dist_norm by (rule norm_triangle_sub) also have "\ \ norm (f m x0 - f n x0) + e / 2" - using N[rule_format,OF _ _ \x\s\ \x0\s\, of m n] and as and False + using N[rule_format,OF _ _ \x\S\ \x0\S\, of m n] and as and False by auto also have "\ < e / 2 + e / 2" apply (rule add_strict_right_mono) @@ -1982,27 +1920,24 @@ qed qed qed - then obtain g where g: "\x\s. (\n. f n x) \ g x" .. - have lem2: "\e>0. \N. \n\N. \x\s. \y\s. norm ((f n x - f n y) - (g x - g y)) \ e * norm (x - y)" + then obtain g where g: "\x\S. (\n. f n x) \ g x" .. + have lem2: "\e>0. \N. \n\N. \x\S. \y\S. norm ((f n x - f n y) - (g x - g y)) \ e * norm (x - y)" proof (rule, rule) fix e :: real assume *: "e > 0" obtain N where - N: "\m\N. \n\N. \x\s. \y\s. norm (f m x - f n x - (f m y - f n y)) \ e * norm (x - y)" + N: "\m\N. \n\N. \x\S. \y\S. norm (f m x - f n x - (f m y - f n y)) \ e * norm (x - y)" using lem1 * by blast - show "\N. \n\N. \x\s. \y\s. norm (f n x - f n y - (g x - g y)) \ e * norm (x - y)" + show "\N. \n\N. \x\S. \y\S. norm (f n x - f n y - (g x - g y)) \ e * norm (x - y)" apply (rule_tac x=N in exI) proof rule+ fix n x y - assume as: "N \ n" "x \ s" "y \ s" + assume as: "N \ n" "x \ S" "y \ S" have "((\m. norm (f n x - f n y - (f m x - f m y))) \ norm (f n x - f n y - (g x - g y))) sequentially" by (intro tendsto_intros g[rule_format] as) moreover have "eventually (\m. norm (f n x - f n y - (f m x - f m y)) \ e * norm (x - y)) sequentially" unfolding eventually_sequentially - apply (rule_tac x=N in exI) - apply rule - apply rule - proof - + proof (intro exI allI impI) fix m assume "N \ m" then show "norm (f n x - f n y - (f m x - f m y)) \ e * norm (x - y)" @@ -2013,11 +1948,11 @@ by (simp add: tendsto_upperbound) qed qed - have "\x\s. ((\n. f n x) \ g x) sequentially \ (g has_derivative g' x) (at x within s)" + have "\x\S. ((\n. f n x) \ g x) sequentially \ (g has_derivative g' x) (at x within S)" unfolding has_derivative_within_alt2 proof (intro ballI conjI) fix x - assume "x \ s" + assume "x \ S" then show "((\n. f n x) \ g x) sequentially" by (simp add: g) have lem3: "\u. ((\n. f' n x u) \ g' x u) sequentially" @@ -2030,7 +1965,7 @@ proof (cases "u = 0") case True have "eventually (\n. norm (f' n x u - g' x u) \ e * norm u) sequentially" - using assms(3)[folded eventually_sequentially] and \0 < e\ and \x \ s\ + using assms(3)[folded eventually_sequentially] and \0 < e\ and \x \ S\ by (fast elim: eventually_mono) then show ?thesis using \u = 0\ and \0 < e\ by (auto elim: eventually_mono) @@ -2038,7 +1973,7 @@ case False with \0 < e\ have "0 < e / norm u" by simp then have "eventually (\n. norm (f' n x u - g' x u) \ e / norm u * norm u) sequentially" - using assms(3)[folded eventually_sequentially] and \x \ s\ + using assms(3)[folded eventually_sequentially] and \x \ S\ by (fast elim: eventually_mono) then show ?thesis using \u \ 0\ by simp @@ -2048,7 +1983,7 @@ proof fix x' y z :: 'a fix c :: real - note lin = assms(2)[rule_format,OF \x\s\,THEN has_derivative_bounded_linear] + note lin = assms(2)[rule_format,OF \x\S\,THEN has_derivative_bounded_linear] show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'" apply (rule tendsto_unique[OF trivial_limit_sequentially]) apply (rule lem3[rule_format]) @@ -2064,9 +1999,9 @@ apply (rule lem3[rule_format])+ done obtain N where N: "\h. norm (f' N x h - g' x h) \ 1 * norm h" - using assms(3) \x \ s\ by (fast intro: zero_less_one) + using assms(3) \x \ S\ by (fast intro: zero_less_one) have "bounded_linear (f' N x)" - using assms(2) \x \ s\ by fast + using assms(2) \x \ S\ by fast from bounded_linear.bounded [OF this] obtain K where K: "\h. norm (f' N x h) \ norm h * K" .. { @@ -2082,36 +2017,36 @@ } then show "\K. \h. norm (g' x h) \ norm h * K" by fast qed - show "\e>0. eventually (\y. norm (g y - g x - g' x (y - x)) \ e * norm (y - x)) (at x within s)" + show "\e>0. eventually (\y. norm (g y - g x - g' x (y - x)) \ e * norm (y - x)) (at x within S)" proof (rule, rule) fix e :: real assume "e > 0" then have *: "e / 3 > 0" by auto - obtain N1 where N1: "\n\N1. \x\s. \h. norm (f' n x h - g' x h) \ e / 3 * norm h" + obtain N1 where N1: "\n\N1. \x\S. \h. norm (f' n x h - g' x h) \ e / 3 * norm h" using assms(3) * by blast obtain N2 where - N2: "\n\N2. \x\s. \y\s. norm (f n x - f n y - (g x - g y)) \ e / 3 * norm (x - y)" + N2: "\n\N2. \x\S. \y\S. norm (f n x - f n y - (g x - g y)) \ e / 3 * norm (x - y)" using lem2 * by blast let ?N = "max N1 N2" - have "eventually (\y. norm (f ?N y - f ?N x - f' ?N x (y - x)) \ e / 3 * norm (y - x)) (at x within s)" - using assms(2)[unfolded has_derivative_within_alt2] and \x \ s\ and * by fast - moreover have "eventually (\y. y \ s) (at x within s)" + have "eventually (\y. norm (f ?N y - f ?N x - f' ?N x (y - x)) \ e / 3 * norm (y - x)) (at x within S)" + using assms(2)[unfolded has_derivative_within_alt2] and \x \ S\ and * by fast + moreover have "eventually (\y. y \ S) (at x within S)" unfolding eventually_at by (fast intro: zero_less_one) - ultimately show "\\<^sub>F y in at x within s. norm (g y - g x - g' x (y - x)) \ e * norm (y - x)" + ultimately show "\\<^sub>F y in at x within S. norm (g y - g x - g' x (y - x)) \ e * norm (y - x)" proof (rule eventually_elim2) fix y - assume "y \ s" + assume "y \ S" assume "norm (f ?N y - f ?N x - f' ?N x (y - x)) \ e / 3 * norm (y - x)" moreover have "norm (g y - g x - (f ?N y - f ?N x)) \ e / 3 * norm (y - x)" - using N2[rule_format, OF _ \y \ s\ \x \ s\] + using N2[rule_format, OF _ \y \ S\ \x \ S\] by (simp add: norm_minus_commute) ultimately have "norm (g y - g x - f' ?N x (y - x)) \ 2 * e / 3 * norm (y - x)" using norm_triangle_le[of "g y - g x - (f ?N y - f ?N x)" "f ?N y - f ?N x - f' ?N x (y - x)" "2 * e / 3 * norm (y - x)"] by (auto simp add: algebra_simps) moreover have " norm (f' ?N x (y - x) - g' x (y - x)) \ e / 3 * norm (y - x)" - using N1 \x \ s\ by auto + using N1 \x \ S\ by auto ultimately show "norm (g y - g x - g' x (y - x)) \ e * norm (y - x)" using norm_triangle_le[of "g y - g x - f' (max N1 N2) x (y - x)" "f' (max N1 N2) x (y - x) - g' x (y - x)"] by (auto simp add: algebra_simps) @@ -2125,77 +2060,63 @@ lemma has_antiderivative_sequence: fixes f :: "nat \ 'a::real_normed_vector \ 'b::banach" - assumes "convex s" - and "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" - and "\e>0. \N. \n\N. \x\s. \h. norm (f' n x h - g' x h) \ e * norm h" - shows "\g. \x\s. (g has_derivative g' x) (at x within s)" -proof (cases "s = {}") + assumes "convex S" + and der: "\n x. x \ S \ ((f n) has_derivative (f' n x)) (at x within S)" + and no: "\e. e > 0 \ \N. \n\N. \x\S. \h. norm (f' n x h - g' x h) \ e * norm h" + shows "\g. \x\S. (g has_derivative g' x) (at x within S)" +proof (cases "S = {}") case False - then obtain a where "a \ s" + then obtain a where "a \ S" by auto - have *: "\P Q. \g. \x\s. P g x \ Q g x \ \g. \x\s. Q g x" + have *: "\P Q. \g. \x\S. P g x \ Q g x \ \g. \x\S. Q g x" by auto show ?thesis apply (rule *) - apply (rule has_derivative_sequence[OF assms(1) _ assms(3), of "\n x. f n x + (f 0 a - f n a)"]) - apply (metis assms(2) has_derivative_add_const) - apply (rule \a \ s\) + apply (rule has_derivative_sequence [OF \convex S\ _ no, of "\n x. f n x + (f 0 a - f n a)"]) + apply (metis assms(2) has_derivative_add_const) + using \a \ S\ apply auto done qed auto lemma has_antiderivative_limit: fixes g' :: "'a::real_normed_vector \ 'a \ 'b::banach" - assumes "convex s" - and "\e>0. \f f'. \x\s. - (f has_derivative (f' x)) (at x within s) \ (\h. norm (f' x h - g' x h) \ e * norm h)" - shows "\g. \x\s. (g has_derivative g' x) (at x within s)" + assumes "convex S" + and "\e. e>0 \ \f f'. \x\S. + (f has_derivative (f' x)) (at x within S) \ (\h. norm (f' x h - g' x h) \ e * norm h)" + shows "\g. \x\S. (g has_derivative g' x) (at x within S)" proof - - have *: "\n. \f f'. \x\s. - (f has_derivative (f' x)) (at x within s) \ + have *: "\n. \f f'. \x\S. + (f has_derivative (f' x)) (at x within S) \ (\h. norm(f' x h - g' x h) \ inverse (real (Suc n)) * norm h)" by (simp add: assms(2)) obtain f where - *: "\x. \f'. \xa\s. (f x has_derivative f' xa) (at xa within s) \ - (\h. norm (f' xa h - g' xa h) \ inverse (real (Suc x)) * norm h)" - using *[THEN choice] .. + *: "\x. \f'. \xa\S. (f x has_derivative f' xa) (at xa within S) \ + (\h. norm (f' xa h - g' xa h) \ inverse (real (Suc x)) * norm h)" + using * by metis obtain f' where - f: "\x. \xa\s. (f x has_derivative f' x xa) (at xa within s) \ - (\h. norm (f' x xa h - g' xa h) \ inverse (real (Suc x)) * norm h)" - using *[THEN choice] .. + f': "\x. \z\S. (f x has_derivative f' x z) (at z within S) \ + (\h. norm (f' x z h - g' z h) \ inverse (real (Suc x)) * norm h)" + using * by metis show ?thesis - apply (rule has_antiderivative_sequence[OF assms(1), of f f']) - defer - apply rule - apply rule - proof - + proof (rule has_antiderivative_sequence[OF \convex S\, of f f']) fix e :: real assume "e > 0" obtain N where N: "inverse (real (Suc N)) < e" using reals_Archimedean[OF \e>0\] .. - show "\N. \n\N. \x\s. \h. norm (f' n x h - g' x h) \ e * norm h" - apply (rule_tac x=N in exI) - apply rule - apply rule - apply rule - apply rule - proof - + show "\N. \n\N. \x\S. \h. norm (f' n x h - g' x h) \ e * norm h" + proof (intro exI allI ballI impI) fix n x h - assume n: "N \ n" and x: "x \ s" + assume n: "N \ n" and x: "x \ S" have *: "inverse (real (Suc n)) \ e" apply (rule order_trans[OF _ N[THEN less_imp_le]]) using n apply (auto simp add: field_simps) done show "norm (f' n x h - g' x h) \ e * norm h" - using f[rule_format,THEN conjunct2, OF x, of n, THEN spec[where x=h]] - apply (rule order_trans) - using N * - apply (cases "h = 0") - apply auto - done + by (meson "*" mult_right_mono norm_ge_zero order.trans x f') qed - qed (insert f, auto) + qed (use f' in auto) qed @@ -2203,12 +2124,12 @@ lemma has_derivative_series: fixes f :: "nat \ 'a::real_normed_vector \ 'b::banach" - assumes "convex s" - and "\n x. x \ s \ ((f n) has_derivative (f' n x)) (at x within s)" - and "\e>0. \N. \n\N. \x\s. \h. norm (sum (\i. f' i x h) {.. e * norm h" - and "x \ s" + assumes "convex S" + and "\n x. x \ S \ ((f n) has_derivative (f' n x)) (at x within S)" + and "\e. e>0 \ \N. \n\N. \x\S. \h. norm (sum (\i. f' i x h) {.. e * norm h" + and "x \ S" and "(\n. f n x) sums l" - shows "\g. \x\s. (\n. f n x) sums (g x) \ (g has_derivative g' x) (at x within s)" + shows "\g. \x\S. (\n. f n x) sums (g x) \ (g has_derivative g' x) (at x within S)" unfolding sums_def apply (rule has_derivative_sequence[OF assms(1) _ assms(3)]) apply (metis assms(2) has_derivative_sum) @@ -2219,20 +2140,19 @@ lemma has_field_derivative_series: fixes f :: "nat \ ('a :: {real_normed_field,banach}) \ 'a" - assumes "convex s" - assumes "\n x. x \ s \ (f n has_field_derivative f' n x) (at x within s)" - assumes "uniform_limit s (\n x. \i s" "summable (\n. f n x0)" - shows "\g. \x\s. (\n. f n x) sums g x \ (g has_field_derivative g' x) (at x within s)" + assumes "convex S" + assumes "\n x. x \ S \ (f n has_field_derivative f' n x) (at x within S)" + assumes "uniform_limit S (\n x. \i S" "summable (\n. f n x0)" + shows "\g. \x\S. (\n. f n x) sums g x \ (g has_field_derivative g' x) (at x within S)" unfolding has_field_derivative_def proof (rule has_derivative_series) - show "\e>0. \N. \n\N. \x\s. \h. norm ((\i e * norm h" - proof (intro allI impI) - fix e :: real assume "e > 0" - with assms(3) obtain N where N: "\n x. n \ N \ x \ s \ norm ((\iN. \n\N. \x\S. \h. norm ((\i e * norm h" if "e > 0" for e + proof - + from that assms(3) obtain N where N: "\n x. n \ N \ x \ S \ norm ((\i N" "x \ s" + fix n :: nat and x h :: 'a assume nx: "n \ N" "x \ S" have "norm ((\iii e" by simp @@ -2240,55 +2160,55 @@ by (intro mult_right_mono) simp_all finally have "norm ((\i e * norm h" . } - thus "\N. \n\N. \x\s. \h. norm ((\i e * norm h" by blast + thus "\N. \n\N. \x\S. \h. norm ((\i e * norm h" by blast qed -qed (insert assms, auto simp: has_field_derivative_def) +qed (use assms in \auto simp: has_field_derivative_def\) lemma has_field_derivative_series': fixes f :: "nat \ ('a :: {real_normed_field,banach}) \ 'a" - assumes "convex s" - assumes "\n x. x \ s \ (f n has_field_derivative f' n x) (at x within s)" - assumes "uniformly_convergent_on s (\n x. \i s" "summable (\n. f n x0)" "x \ interior s" + assumes "convex S" + assumes "\n x. x \ S \ (f n has_field_derivative f' n x) (at x within S)" + assumes "uniformly_convergent_on S (\n x. \i S" "summable (\n. f n x0)" "x \ interior S" shows "summable (\n. f n x)" "((\x. \n. f n x) has_field_derivative (\n. f' n x)) (at x)" proof - - from \x \ interior s\ have "x \ s" using interior_subset by blast + from \x \ interior S\ have "x \ S" using interior_subset by blast define g' where [abs_def]: "g' x = (\i. f' i x)" for x - from assms(3) have "uniform_limit s (\n x. \in x. \ix. x \ s \ (\n. f n x) sums g x" - "\x. x \ s \ (g has_field_derivative g' x) (at x within s)" by blast - from g(1)[OF \x \ s\] show "summable (\n. f n x)" by (simp add: sums_iff) - from g(2)[OF \x \ s\] \x \ interior s\ have "(g has_field_derivative g' x) (at x)" - by (simp add: at_within_interior[of x s]) + "\x. x \ S \ (\n. f n x) sums g x" + "\x. x \ S \ (g has_field_derivative g' x) (at x within S)" by blast + from g(1)[OF \x \ S\] show "summable (\n. f n x)" by (simp add: sums_iff) + from g(2)[OF \x \ S\] \x \ interior S\ have "(g has_field_derivative g' x) (at x)" + by (simp add: at_within_interior[of x S]) also have "(g has_field_derivative g' x) (at x) \ ((\x. \n. f n x) has_field_derivative g' x) (at x)" - using eventually_nhds_in_nhd[OF \x \ interior s\] interior_subset[of s] g(1) + using eventually_nhds_in_nhd[OF \x \ interior S\] interior_subset[of S] g(1) by (intro DERIV_cong_ev) (auto elim!: eventually_mono simp: sums_iff) finally show "((\x. \n. f n x) has_field_derivative g' x) (at x)" . qed lemma differentiable_series: fixes f :: "nat \ ('a :: {real_normed_field,banach}) \ 'a" - assumes "convex s" "open s" - assumes "\n x. x \ s \ (f n has_field_derivative f' n x) (at x)" - assumes "uniformly_convergent_on s (\n x. \i s" "summable (\n. f n x0)" and x: "x \ s" + assumes "convex S" "open S" + assumes "\n x. x \ S \ (f n has_field_derivative f' n x) (at x)" + assumes "uniformly_convergent_on S (\n x. \i S" "summable (\n. f n x0)" and x: "x \ S" shows "summable (\n. f n x)" and "(\x. \n. f n x) differentiable (at x)" proof - - from assms(4) obtain g' where A: "uniform_limit s (\n x. \in x. \iopen s\ have s: "at x within s = at x" by (rule at_within_open) - have "\g. \x\s. (\n. f n x) sums g x \ (g has_field_derivative g' x) (at x within s)" - by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within) - then obtain g where g: "\x. x \ s \ (\n. f n x) sums g x" - "\x. x \ s \ (g has_field_derivative g' x) (at x within s)" by blast + from x and \open S\ have S: "at x within S = at x" by (rule at_within_open) + have "\g. \x\S. (\n. f n x) sums g x \ (g has_field_derivative g' x) (at x within S)" + by (intro has_field_derivative_series[of S f f' g' x0] assms A has_field_derivative_at_within) + then obtain g where g: "\x. x \ S \ (\n. f n x) sums g x" + "\x. x \ S \ (g has_field_derivative g' x) (at x within S)" by blast from g[OF x] show "summable (\n. f n x)" by (auto simp: summable_def) from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)" - by (simp add: has_field_derivative_def s) + by (simp add: has_field_derivative_def S) have "((\x. \n. f n x) has_derivative ( * ) (g' x)) (at x)" - by (rule has_derivative_transform_within_open[OF g' \open s\ x]) + by (rule has_derivative_transform_within_open[OF g' \open S\ x]) (insert g, auto simp: sums_iff) thus "(\x. \n. f n x) differentiable (at x)" unfolding differentiable_def by (auto simp: summable_def differentiable_def has_field_derivative_def) @@ -2296,32 +2216,32 @@ lemma differentiable_series': fixes f :: "nat \ ('a :: {real_normed_field,banach}) \ 'a" - assumes "convex s" "open s" - assumes "\n x. x \ s \ (f n has_field_derivative f' n x) (at x)" - assumes "uniformly_convergent_on s (\n x. \i s" "summable (\n. f n x0)" + assumes "convex S" "open S" + assumes "\n x. x \ S \ (f n has_field_derivative f' n x) (at x)" + assumes "uniformly_convergent_on S (\n x. \i S" "summable (\n. f n x0)" shows "(\x. \n. f n x) differentiable (at x0)" - using differentiable_series[OF assms, of x0] \x0 \ s\ by blast+ + using differentiable_series[OF assms, of x0] \x0 \ S\ by blast+ text \Considering derivative @{typ "real \ 'b::real_normed_vector"} as a vector.\ definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)" lemma vector_derivative_unique_within: - assumes not_bot: "at x within s \ bot" - and f': "(f has_vector_derivative f') (at x within s)" - and f'': "(f has_vector_derivative f'') (at x within s)" + assumes not_bot: "at x within S \ bot" + and f': "(f has_vector_derivative f') (at x within S)" + and f'': "(f has_vector_derivative f'') (at x within S)" shows "f' = f''" proof - have "(\x. x *\<^sub>R f') = (\x. x *\<^sub>R f'')" proof (rule frechet_derivative_unique_within) - show "\i\Basis. \e>0. \d. 0 < \d\ \ \d\ < e \ x + d *\<^sub>R i \ s" + show "\i\Basis. \e>0. \d. 0 < \d\ \ \d\ < e \ x + d *\<^sub>R i \ S" proof clarsimp fix e :: real assume "0 < e" - with islimpt_approachable_real[of x s] not_bot - obtain x' where "x' \ s" "x' \ x" "\x' - x\ < e" + with islimpt_approachable_real[of x S] not_bot + obtain x' where "x' \ S" "x' \ x" "\x' - x\ < e" by (auto simp add: trivial_limit_within) - then show "\d. d \ 0 \ \d\ < e \ x + d \ s" + then show "\d. d \ 0 \ \d\ < e \ x + d \ S" by (intro exI[of _ "x' - x"]) auto qed qed (insert f' f'', auto simp: has_vector_derivative_def) @@ -2351,8 +2271,8 @@ qed (auto simp: vector_derivative_def has_vector_derivative_def differentiable_def) lemma vector_derivative_within: - assumes not_bot: "at x within s \ bot" and y: "(f has_vector_derivative y) (at x within s)" - shows "vector_derivative f (at x within s) = y" + assumes not_bot: "at x within S \ bot" and y: "(f has_vector_derivative y) (at x within S)" + shows "vector_derivative f (at x within S) = y" using y by (intro vector_derivative_unique_within[OF not_bot vector_derivative_works[THEN iffD1] y]) (auto simp: differentiable_def has_vector_derivative_def) @@ -2381,11 +2301,11 @@ by (metis has_field_derivative_def has_real_derivative) lemma has_vector_derivative_cong_ev: - assumes *: "eventually (\x. x \ s \ f x = g x) (nhds x)" "f x = g x" - shows "(f has_vector_derivative f') (at x within s) = (g has_vector_derivative f') (at x within s)" + assumes *: "eventually (\x. x \ S \ f x = g x) (nhds x)" "f x = g x" + shows "(f has_vector_derivative f') (at x within S) = (g has_vector_derivative f') (at x within S)" unfolding has_vector_derivative_def has_derivative_def using * - apply (cases "at x within s \ bot") + apply (cases "at x within S \ bot") apply (intro refl conj_cong filterlim_cong) apply (auto simp: netlimit_within eventually_at_filter elim: eventually_mono) done diff -r b249fab48c76 -r d2daeef3ce47 src/HOL/Analysis/Fashoda_Theorem.thy --- a/src/HOL/Analysis/Fashoda_Theorem.thy Wed May 02 12:47:56 2018 +0100 +++ b/src/HOL/Analysis/Fashoda_Theorem.thy Wed May 02 12:48:08 2018 +0100 @@ -109,21 +109,16 @@ have lem1: "\z::real^2. infnorm (negatex z) = infnorm z" unfolding negatex_def infnorm_2 vector_2 by auto have lem2: "\z. z \ 0 \ infnorm (sqprojection z) = 1" - unfolding sqprojection_def - unfolding infnorm_mul[unfolded scalar_mult_eq_scaleR] - unfolding abs_inverse real_abs_infnorm - apply (subst infnorm_eq_0[symmetric]) - apply auto - done + unfolding sqprojection_def infnorm_mul[unfolded scalar_mult_eq_scaleR] + by (simp add: real_abs_infnorm infnorm_eq_0) let ?F = "\w::real^2. (f \ (\x. x$1)) w - (g \ (\x. x$2)) w" - have *: "\i. (\x::real^2. x $ i) ` cbox (- 1) 1 = {-1 .. 1}" - apply (rule set_eqI) - unfolding image_iff Bex_def mem_box_cart interval_cbox_cart - apply rule - defer - apply (rule_tac x="vec x" in exI) - apply auto - done + have *: "\i. (\x::real^2. x $ i) ` cbox (- 1) 1 = {-1..1}" + proof + show "(\x::real^2. x $ i) ` cbox (- 1) 1 \ {-1..1}" for i + by (auto simp: mem_box_cart) + show "{-1..1} \ (\x::real^2. x $ i) ` cbox (- 1) 1" for i + by (clarsimp simp: image_iff mem_box_cart Bex_def) (metis (no_types, hide_lams) vec_component) + qed { fix x assume "x \ (\w. (f \ (\x. x $ 1)) w - (g \ (\x. x $ 2)) w) ` (cbox (- 1) (1::real^2))" @@ -136,37 +131,19 @@ unfolding mem_box_cart atLeastAtMost_iff by auto } note x0 = this - have 21: "\i::2. i \ 1 \ i = 2" - using UNIV_2 by auto have 1: "box (- 1) (1::real^2) \ {}" unfolding interval_eq_empty_cart by auto - have 2: "continuous_on (cbox (- 1) 1) (negatex \ sqprojection \ ?F)" + have "negatex (x + y) $ i = (negatex x + negatex y) $ i \ negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i" + for i x y c + using exhaust_2 [of i] by (auto simp: negatex_def) + then have "bounded_linear negatex" + by (simp add: bounded_linearI' vec_eq_iff) + then have 2: "continuous_on (cbox (- 1) 1) (negatex \ sqprojection \ ?F)" apply (intro continuous_intros continuous_on_component) - unfolding * - apply (rule assms)+ - apply (subst sqprojection_def) - apply (intro continuous_intros) - apply (simp add: infnorm_eq_0 x0) - apply (rule linear_continuous_on) - proof - - show "bounded_linear negatex" - apply (rule bounded_linearI') - unfolding vec_eq_iff - proof (rule_tac[!] allI) - fix i :: 2 - fix x y :: "real^2" - fix c :: real - show "negatex (x + y) $ i = - (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i" - apply - - apply (case_tac[!] "i\1") - prefer 3 - apply (drule_tac[1-2] 21) - unfolding negatex_def - apply (auto simp add:vector_2) - done - qed - qed + unfolding * sqprojection_def + apply (intro assms continuous_intros)+ + apply (simp_all add: infnorm_eq_0 x0 linear_continuous_on) + done have 3: "(negatex \ sqprojection \ ?F) ` cbox (-1) 1 \ cbox (-1) 1" unfolding subset_eq proof (rule, goal_cases) @@ -176,29 +153,19 @@ "x = (negatex \ sqprojection \ (\w. (f \ (\x. x $ 1)) w - (g \ (\x. x $ 2)) w)) y" unfolding image_iff .. have "?F y \ 0" - apply (rule x0) - using y(1) - apply auto - done + by (rule x0) (use y in auto) then have *: "infnorm (sqprojection (?F y)) = 1" unfolding y o_def by - (rule lem2[rule_format]) - have "infnorm x = 1" + have inf1: "infnorm x = 1" unfolding *[symmetric] y o_def by (rule lem1[rule_format]) - then show "x \ cbox (-1) 1" + show "x \ cbox (-1) 1" unfolding mem_box_cart interval_cbox_cart infnorm_2 - apply - - apply rule - proof - + proof fix i - assume "max \x $ 1\ \x $ 2\ = 1" - then show "(- 1) $ i \ x $ i \ x $ i \ 1 $ i" - apply (cases "i = 1") - defer - apply (drule 21) - apply auto - done + show "(- 1) $ i \ x $ i \ x $ i \ 1 $ i" + using exhaust_2 [of i] inf1 by (auto simp: infnorm_2) qed qed obtain x :: "real^2" where x: @@ -211,10 +178,7 @@ apply blast done have "?F x \ 0" - apply (rule x0) - using x(1) - apply auto - done + by (rule x0) (use x in auto) then have *: "infnorm (sqprojection (?F x)) = 1" unfolding o_def by (rule lem2[rule_format]) @@ -223,109 +187,73 @@ unfolding *[symmetric] o_def apply (rule lem1[rule_format]) done - have "\x i. x \ 0 \ (0 < (sqprojection x)$i \ 0 < x$i)" - and "\x i. x \ 0 \ ((sqprojection x)$i < 0 \ x$i < 0)" - apply - - apply (rule_tac[!] allI impI)+ + have iff: "0 < sqprojection x$i \ 0 < x$i" "sqprojection x$i < 0 \ x$i < 0" if "x \ 0" for x i proof - - fix x :: "real^2" - fix i :: 2 - assume x: "x \ 0" have "inverse (infnorm x) > 0" - using x[unfolded infnorm_pos_lt[symmetric]] by auto + by (simp add: infnorm_pos_lt that) then show "(0 < sqprojection x $ i) = (0 < x $ i)" and "(sqprojection x $ i < 0) = (x $ i < 0)" unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def unfolding zero_less_mult_iff mult_less_0_iff by (auto simp add: field_simps) qed - note lem3 = this[rule_format] have x1: "x $ 1 \ {- 1..1::real}" "x $ 2 \ {- 1..1::real}" using x(1) unfolding mem_box_cart by auto then have nz: "f (x $ 1) - g (x $ 2) \ 0" - unfolding right_minus_eq - apply - - apply (rule as) - apply auto - done - have "x $ 1 = -1 \ x $ 1 = 1 \ x $ 2 = -1 \ x $ 2 = 1" + using as by auto + consider "x $ 1 = -1" | "x $ 1 = 1" | "x $ 2 = -1" | "x $ 2 = 1" using nx unfolding infnorm_eq_1_2 by auto then show False - proof - - fix P Q R S - presume "P \ Q \ R \ S" - and "P \ False" - and "Q \ False" - and "R \ False" - and "S \ False" - then show False by auto - next - assume as: "x$1 = 1" - then have *: "f (x $ 1) $ 1 = 1" - using assms(6) by auto - have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0" - using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] - unfolding as negatex_def vector_2 - by auto - moreover - from x1 have "g (x $ 2) \ cbox (-1) 1" - using assms(2) by blast - ultimately show False - unfolding lem3[OF nz] vector_component_simps * mem_box_cart - using not_le by auto - next - assume as: "x$1 = -1" + proof cases + case 1 then have *: "f (x $ 1) $ 1 = - 1" using assms(5) by auto have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0" using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] - unfolding as negatex_def vector_2 - by auto + by (auto simp: negatex_def 1) moreover from x1 have "g (x $ 2) \ cbox (-1) 1" using assms(2) by blast ultimately show False - unfolding lem3[OF nz] vector_component_simps * mem_box_cart + unfolding iff[OF nz] vector_component_simps * mem_box_cart using not_le by auto next - assume as: "x$2 = 1" + case 2 + then have *: "f (x $ 1) $ 1 = 1" + using assms(6) by auto + have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0" + using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] 2 + by (auto simp: negatex_def) + moreover have "g (x $ 2) \ cbox (-1) 1" + using assms(2) x1 by blast + ultimately show False + unfolding iff[OF nz] vector_component_simps * mem_box_cart + using not_le by auto + next + case 3 + then have *: "g (x $ 2) $ 2 = - 1" + using assms(7) by auto + have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0" + using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 3 by (auto simp: negatex_def) + moreover + from x1 have "f (x $ 1) \ cbox (-1) 1" + using assms(1) by blast + ultimately show False + unfolding iff[OF nz] vector_component_simps * mem_box_cart + by (erule_tac x=2 in allE) auto + next + case 4 then have *: "g (x $ 2) $ 2 = 1" using assms(8) by auto have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0" - using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] - unfolding as negatex_def vector_2 - by auto + using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 4 by (auto simp: negatex_def) moreover from x1 have "f (x $ 1) \ cbox (-1) 1" - apply - - apply (rule assms(1)[unfolded subset_eq,rule_format]) - apply auto - done + using assms(1) by blast ultimately show False - unfolding lem3[OF nz] vector_component_simps * mem_box_cart - apply (erule_tac x=2 in allE) - apply auto - done - next - assume as: "x$2 = -1" - then have *: "g (x $ 2) $ 2 = - 1" - using assms(7) by auto - have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0" - using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] - unfolding as negatex_def vector_2 - by auto - moreover - from x1 have "f (x $ 1) \ cbox (-1) 1" - apply - - apply (rule assms(1)[unfolded subset_eq,rule_format]) - apply auto - done - ultimately show False - unfolding lem3[OF nz] vector_component_simps * mem_box_cart - apply (erule_tac x=2 in allE) - apply auto - done - qed auto + unfolding iff[OF nz] vector_component_simps * mem_box_cart + by (erule_tac x=2 in allE) auto + qed qed lemma fashoda_unit_path: @@ -533,14 +461,12 @@ using as by auto show thesis - apply (rule_tac z="interval_bij (- 1,1) (a,b) z" in that) - apply (subst zf) - defer - apply (subst zg) - unfolding o_def interval_bij_bij_cart[OF *] path_image_def - using zf(1) zg(1) - apply auto - done + proof (rule_tac z="interval_bij (- 1,1) (a,b) z" in that) + show "interval_bij (- 1, 1) (a, b) z \ path_image f" + using zf by (simp add: interval_bij_bij_cart[OF *] path_image_def) + show "interval_bij (- 1, 1) (a, b) z \ path_image g" + using zg by (simp add: interval_bij_bij_cart[OF *] path_image_def) + qed qed @@ -714,8 +640,8 @@ fixes a :: "real^2" assumes "path f" and "path g" - and "path_image f \ cbox a b" - and "path_image g \ cbox a b" + and paf: "path_image f \ cbox a b" + and pag: "path_image g \ cbox a b" and "(pathstart f)$2 = a$2" and "(pathfinish f)$2 = a$2" and "(pathstart g)$2 = a$2" @@ -776,30 +702,9 @@ proof - show "path ?P1" and "path ?P2" using assms by auto - have "path_image ?P1 \ cbox ?a ?b" - unfolding P1P2 path_image_linepath - apply (rule Un_least)+ - defer 3 - apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format]) - unfolding mem_box_cart forall_2 vector_2 - using ab startfin abab assms(3) - using assms(9-) - unfolding assms - apply (auto simp add: field_simps box_def) - done - then show "path_image ?P1 \ cbox ?a ?b" . - have "path_image ?P2 \ cbox ?a ?b" - unfolding P1P2 path_image_linepath - apply (rule Un_least)+ - defer 2 - apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format]) - unfolding mem_box_cart forall_2 vector_2 - using ab startfin abab assms(4) - using assms(9-) - unfolding assms - apply (auto simp add: field_simps box_def) - done - then show "path_image ?P2 \ cbox ?a ?b" . + show "path_image ?P1 \ cbox ?a ?b" "path_image ?P2 \ cbox ?a ?b" + unfolding P1P2 path_image_linepath using startfin paf pag + by (auto simp: mem_box_cart segment_horizontal segment_vertical forall_2) show "a $ 1 - 2 = a $ 1 - 2" and "b $ 1 + 2 = b $ 1 + 2" and "pathstart g $ 2 - 3 = a $ 2 - 3" @@ -808,8 +713,7 @@ qed note z=this[unfolded P1P2 path_image_linepath] show thesis - apply (rule that[of z]) - proof - + proof (rule that[of z]) have "(z \ closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) \ z \ closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \ z \ closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \ @@ -838,32 +742,26 @@ using prems(2) using assms ab by (auto simp add: field_simps) ultimately have *: "z$2 = a$2 - 2" - using prems(1) - by auto + using prems(1) by auto have "z$1 \ pathfinish g$1" - using prems(2) - using assms ab + using prems(2) assms ab by (auto simp add: field_simps *) moreover have "pathstart g \ cbox a b" using assms(4) pathstart_in_path_image[of g] by auto note this[unfolded mem_box_cart forall_2] then have "z$1 \ pathstart g$1" - using prems(1) - using assms ab + using prems(1) assms ab by (auto simp add: field_simps *) ultimately have "a $ 2 - 1 \ z $ 2 \ z $ 2 \ b $ 2 + 3 \ b $ 2 + 3 \ z $ 2 \ z $ 2 \ a $ 2 - 1" - using prems(2) - unfolding * assms - by (auto simp add: field_simps) + using prems(2) unfolding * assms by (auto simp add: field_simps) then show False unfolding * using ab by auto qed then have "z \ path_image f \ z \ path_image g" using z unfolding Un_iff by blast then have z': "z \ cbox a b" - using assms(3-4) - by auto + using assms(3-4) by auto have "a $ 2 = z $ 2 \ (z $ 1 = pathstart f $ 1 \ z $ 1 = pathfinish f $ 1) \ z = pathstart f \ z = pathfinish f" unfolding vec_eq_iff forall_2 assms @@ -871,11 +769,7 @@ with z' show "z \ path_image f" using z(1) unfolding Un_iff mem_box_cart forall_2 - apply - - apply (simp only: segment_vertical segment_horizontal vector_2) - unfolding assms - apply auto - done + by (simp only: segment_vertical segment_horizontal vector_2) (auto simp: assms) have "a $ 2 = z $ 2 \ (z $ 1 = pathstart g $ 1 \ z $ 1 = pathfinish g $ 1) \ z = pathstart g \ z = pathfinish g" unfolding vec_eq_iff forall_2 assms @@ -883,10 +777,7 @@ with z' show "z \ path_image g" using z(2) unfolding Un_iff mem_box_cart forall_2 - apply (simp only: segment_vertical segment_horizontal vector_2) - unfolding assms - apply auto - done + by (simp only: segment_vertical segment_horizontal vector_2) (auto simp: assms) qed qed diff -r b249fab48c76 -r d2daeef3ce47 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed May 02 12:47:56 2018 +0100 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed May 02 12:48:08 2018 +0100 @@ -128,20 +128,13 @@ assumes "k \ Basis" shows "content (cbox a b) = content(cbox a b \ {x. x\k \ c}) + content(cbox a b \ {x. x\k \ c})" \ \Prove using measure theory\ -proof cases +proof (cases "\i\Basis. a \ i \ b \ i") + case True + have 1: "\X Y Z. (\i\Basis. Z i (if i = k then X else Y i)) = Z k X * (\i\Basis-{k}. Z i (Y i))" + by (simp add: if_distrib prod.delta_remove assms) note simps = interval_split[OF assms] content_cbox_cases - have *: "Basis = insert k (Basis - {k})" "\x. finite (Basis-{x})" "\x. x\Basis-{x}" - using assms by auto - have *: "\X Y Z. (\i\Basis. Z i (if i = k then X else Y i)) = Z k X * (\i\Basis-{k}. Z i (Y i))" - "(\i\Basis. b\i - a\i) = (\i\Basis-{k}. b\i - a\i) * (b\k - a\k)" - apply (subst *(1)) - defer - apply (subst *(1)) - unfolding prod.insert[OF *(2-)] - apply auto - done - assume as: "\i\Basis. a \ i \ b \ i" - moreover + have 2: "(\i\Basis. b\i - a\i) = (\i\Basis-{k}. b\i - a\i) * (b\k - a\k)" + by (metis (no_types, lifting) assms finite_Basis mult.commute prod.remove) have "\x. min (b \ k) c = max (a \ k) c \ x * (b\k - a\k) = x * (max (a \ k) c - a \ k) + x * (b \ k - max (a \ k) c)" by (auto simp add: field_simps) @@ -152,17 +145,12 @@ (\i\Basis. b \ i - (if i = k then max (a \ k) c else a \ i))" by (auto intro!: prod.cong) have "\ a \ k \ c \ \ c \ b \ k \ False" - unfolding not_le - using as[unfolded ,rule_format,of k] assms - by auto + unfolding not_le using True assms by auto ultimately show ?thesis - using assms - unfolding simps ** - unfolding *(1)[of "\i x. b\i - x"] *(1)[of "\i x. x - a\i"] - unfolding *(2) + using assms unfolding simps ** 1[of "\i x. b\i - x"] 1[of "\i x. x - a\i"] 2 by auto next - assume "\ (\i\Basis. a \ i \ b \ i)" + case False then have "cbox a b = {}" unfolding box_eq_empty by (auto simp: not_le) then show ?thesis @@ -2585,24 +2573,22 @@ norm (sum (\(x,k). content k *\<^sub>R f x) p - i) \ e * content (cbox a b)))" proof (cases "content (cbox a b) = 0") case True - show ?thesis + have "\e p. p tagged_division_of cbox a b \ norm ((\(x, k)\p. content k *\<^sub>R f x)) \ e * content (cbox a b)" + unfolding sum_content_null[OF True] True by force + moreover have "i = 0" + if "\e. e > 0 \ \d. gauge d \ + (\p. p tagged_division_of cbox a b \ + d fine p \ + norm ((\(x, k)\p. content k *\<^sub>R f x) - i) \ e * content (cbox a b))" + using that [of 1] + by (force simp add: True sum_content_null[OF True] intro: fine_division_exists[of _ a b]) + ultimately show ?thesis unfolding has_integral_null_eq[OF True] - apply safe - apply (rule, rule, rule gauge_trivial, safe) - unfolding sum_content_null[OF True] True - defer - apply (erule_tac x=1 in allE) - apply safe - defer - apply (rule fine_division_exists[of _ a b]) - apply assumption - apply (erule_tac x=p in allE) - unfolding sum_content_null[OF True] - apply auto - done + by (force simp add: ) next case False - note F = this[unfolded content_lt_nz[symmetric]] + then have F: "0 < content (cbox a b)" + using zero_less_measure_iff by blast let ?P = "\e opp. \d. gauge d \ (\p. p tagged_division_of (cbox a b) \ d fine p \ opp (norm ((\(x, k)\p. content k *\<^sub>R f x) - i)) e)" show ?thesis @@ -2610,28 +2596,18 @@ proof safe fix e :: real assume e: "e > 0" - { - assume "\e>0. ?P e (<)" + { assume "\e>0. ?P e (<)" then show "?P (e * content (cbox a b)) (\)" - apply (erule_tac x="e * content (cbox a b)" in allE) - apply (erule impE) - defer - apply (erule exE,rule_tac x=d in exI) - using F e - apply (auto simp add:field_simps) - done - } - { - assume "\e>0. ?P (e * content (cbox a b)) (\)" + apply (rule allE [where x="e * content (cbox a b)"]) + apply (elim impE ex_forward conj_forward) + using F e apply (auto simp add: algebra_simps) + done } + { assume "\e>0. ?P (e * content (cbox a b)) (\)" then show "?P e (<)" - apply (erule_tac x="e/2 / content (cbox a b)" in allE) - apply (erule impE) - defer - apply (erule exE,rule_tac x=d in exI) - using F e - apply (auto simp add: field_simps) - done - } + apply (rule allE [where x="e/2 / content (cbox a b)"]) + apply (elim impE ex_forward conj_forward) + using F e apply (auto simp add: algebra_simps) + done } qed qed @@ -2995,19 +2971,22 @@ lemma integrable_subinterval: fixes f :: "'b::euclidean_space \ 'a::banach" - assumes "f integrable_on cbox a b" - and "cbox c d \ cbox a b" + assumes f: "f integrable_on cbox a b" + and cd: "cbox c d \ cbox a b" shows "f integrable_on cbox c d" proof - interpret operative conj True "\i. f integrable_on i" using order_refl by (rule operative_integrableI) show ?thesis - apply (cases "cbox c d = {}") - defer - apply (rule partial_division_extend_1[OF assms(2)],assumption) - using division [symmetric] assms(1) - apply (auto simp: comm_monoid_set_F_and) - done + proof (cases "cbox c d = {}") + case True + then show ?thesis + using division [symmetric] f by (auto simp: comm_monoid_set_F_and) + next + case False + then show ?thesis + by (metis cd comm_monoid_set_F_and division division_of_finite f partial_division_extend_1) + qed qed lemma integrable_subinterval_real: @@ -4261,31 +4240,29 @@ lemma has_derivative_zero_unique_strong_interval: fixes f :: "real \ 'a::banach" assumes "finite k" - and "continuous_on {a..b} f" + and contf: "continuous_on {a..b} f" and "f a = y" - and "\x\({a..b} - k). (f has_derivative (\h. 0)) (at x within {a..b})" "x \ {a..b}" + and fder: "\x. x \ {a..b} - k \ (f has_derivative (\h. 0)) (at x within {a..b})" + and x: "x \ {a..b}" shows "f x = y" proof - - have ab: "a \ b" + have "a \ b" "a \ x" using assms by auto - have *: "a \ x" - using assms(5) by auto have "((\x. 0::'a) has_integral f x - f a) {a..x}" - apply (rule fundamental_theorem_of_calculus_interior_strong[OF assms(1) *]) - apply (rule continuous_on_subset[OF assms(2)]) - defer - apply safe - unfolding has_vector_derivative_def - apply (subst has_derivative_within_open[symmetric]) - apply assumption - apply (rule open_greaterThanLessThan) - apply (rule has_derivative_within_subset[where s="{a..b}"]) - using assms(4) assms(5) - apply (auto simp: mem_box) - done - note this[unfolded *] - note has_integral_unique[OF has_integral_0 this] - then show ?thesis + proof (rule fundamental_theorem_of_calculus_interior_strong[OF \finite k\ \a \ x\]; clarify?) + have "{a..x} \ {a..b}" + using x by auto + then show "continuous_on {a..x} f" + by (rule continuous_on_subset[OF contf]) + show "(f has_vector_derivative 0) (at z)" if z: "z \ {a<.. k" for z + unfolding has_vector_derivative_def + proof (simp add: has_derivative_within_open[OF z, symmetric]) + show "(f has_derivative (\x. 0)) (at z within {a<.. S" "f c = y" - and derf: "\x. x \ (S - K) \ (f has_derivative (\h. 0)) (at x within S)" + and derf: "\x. x \ S - K \ (f has_derivative (\h. 0)) (at x within S)" and "x \ S" shows "f x = y" proof (cases "x = c") @@ -4307,8 +4284,10 @@ case False let ?\ = "\u. (1 - u) *\<^sub>R c + u *\<^sub>R x" have contf': "continuous_on {0 ..1} (f \ ?\)" - apply (rule continuous_intros continuous_on_subset[OF contf])+ - using \convex S\ \x \ S\ \c \ S\ by (auto simp add: convex_alt algebra_simps) + proof (rule continuous_intros continuous_on_subset[OF contf])+ + show "(\u. (1 - u) *\<^sub>R c + u *\<^sub>R x) ` {0..1} \ S" + using \convex S\ \x \ S\ \c \ S\ by (auto simp add: convex_alt algebra_simps) + qed have "t = u" if "?\ t = ?\ u" for t u proof - from that have "(t - u) *\<^sub>R x = (t - u) *\<^sub>R c" @@ -4353,7 +4332,7 @@ and contf: "continuous_on S f" and "c \ S" and "f c = y" - and derf: "\x. x \ (S - K) \ (f has_derivative (\h. 0)) (at x within S)" + and derf: "\x. x \ S - K \ (f has_derivative (\h. 0)) (at x within S)" and "x \ S" shows "f x = y" proof - @@ -4486,10 +4465,7 @@ note has_integral_restrict_open_subinterval[OF assms] note * = has_integral_spike[OF negligible_frontier_interval _ this] show ?thesis - apply (rule *[of c d]) - using box_subset_cbox[of c d] - apply auto - done + by (rule *[of c d]) (use box_subset_cbox[of c d] in auto) qed lemma has_integral_restrict_closed_subintervals_eq: diff -r b249fab48c76 -r d2daeef3ce47 src/HOL/Analysis/Linear_Algebra.thy --- a/src/HOL/Analysis/Linear_Algebra.thy Wed May 02 12:47:56 2018 +0100 +++ b/src/HOL/Analysis/Linear_Algebra.thy Wed May 02 12:48:08 2018 +0100 @@ -27,13 +27,6 @@ show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR) qed -lemma bounded_linearI: - assumes "\x y. f (x + y) = f x + f y" - and "\r x. f (r *\<^sub>R x) = r *\<^sub>R f x" - and "\x. norm (f x) \ norm x * K" - shows "bounded_linear f" - using assms by (rule bounded_linear_intro) (* FIXME: duplicate *) - subsection \A generic notion of "hull" (convex, affine, conic hull and closure).\ definition%important hull :: "('a set \ bool) \ 'a set \ 'a set" (infixl "hull" 75) @@ -72,7 +65,7 @@ lemma hull_unique: "s \ t \ S t \ (\t'. s \ t' \ S t' \ t \ t') \ (S hull s = t)" unfolding hull_def by auto -lemma hull_induct: "(\x. x\ S \ P x) \ Q {x. P x} \ \x\ Q hull S. P x" +lemma hull_induct: "\a \ Q hull S; \x. x\ S \ P x; Q {x. P x}\ \ P a" using hull_minimal[of S "{x. P x}" Q] by (auto simp add: subset_eq) @@ -339,20 +332,12 @@ unfolding dependent_def by auto lemma (in real_vector) independent_mono: "independent A \ B \ A \ independent B" - apply (clarsimp simp add: dependent_def span_mono) - apply (subgoal_tac "span (B - {a}) \ span (A - {a})") - apply force - apply (rule span_mono) - apply auto - done + unfolding dependent_def span_mono + by (metis insert_Diff local.span_mono subsetCE subset_insert_iff) lemma (in real_vector) span_subspace: "A \ B \ B \ span A \ subspace B \ span A = B" by (metis order_antisym span_def hull_minimal) -lemma (in real_vector) span_induct': - "\x \ S. P x \ subspace {x. P x} \ \x \ span S. P x" - unfolding span_def by (rule hull_induct) auto - inductive_set (in real_vector) span_induct_alt_help for S :: "'a set" where span_induct_alt_help_0: "0 \ span_induct_alt_help S" @@ -1063,19 +1048,19 @@ done lemma linear_eq_0_span: - assumes lf: "linear f" and f0: "\x\B. f x = 0" - shows "\x \ span B. f x = 0" - using f0 subspace_kernel[OF lf] - by (rule span_induct') - -lemma linear_eq_0: "linear f \ S \ span B \ \x\B. f x = 0 \ \x\S. f x = 0" - using linear_eq_0_span[of f B] by auto - -lemma linear_eq_span: "linear f \ linear g \ \x\B. f x = g x \ \x \ span B. f x = g x" - using linear_eq_0_span[of "\x. f x - g x" B] by (auto simp: linear_compose_sub) - -lemma linear_eq: "linear f \ linear g \ S \ span B \ \x\B. f x = g x \ \x\S. f x = g x" - using linear_eq_span[of f g B] by auto + assumes x: "x \ span B" and lf: "linear f" and f0: "\x. x\B \ f x = 0" + shows "f x = 0" + using x f0 subspace_kernel[OF lf] span_induct + by blast + +lemma linear_eq_0: "\x \ S; linear f; S \ span B; \x. x\B \ f x = 0\ \ f x = 0" + using linear_eq_0_span[of x B f] by auto + +lemma linear_eq_span: "\x \ span B; linear f; linear g; \x. x\B \ f x = g x\ \ f x = g x" + using linear_eq_0_span[of x B "\x. f x - g x"] by (auto simp: linear_compose_sub) + +lemma linear_eq: "\x \ S; linear f; linear g; S \ span B; \x. x\B \ f x = g x\ \ f x = g x" + using linear_eq_span[of _ B f g] by auto text \The degenerate case of the Exchange Lemma.\ @@ -1174,13 +1159,13 @@ have fB: "inj_on f B" using fi by (auto simp: \span S = span B\ intro: subset_inj_on span_superset) - have "\x\span B. g (f x) = x" - proof (intro linear_eq_span) + have "g (f x) = x" if "x \ span B" for x + proof (rule linear_eq_span) show "linear (\x. x)" "linear (\x. g (f x))" using linear_id linear_compose[OF \linear f\ \linear g\] by (auto simp: id_def comp_def) - show "\x \ B. g (f x) = x" - using g fi \span S = span B\ by (auto simp: fB) - qed + show "g (f x) = x" if "x \ B" for x + using g fi \span S = span B\ by (simp add: fB that) + qed (rule that) moreover have "inv_into B f ` f ` B \ B" by (auto simp: fB) @@ -1210,8 +1195,7 @@ ultimately have "\x\B. f (g x) = x" by auto then have "\x\span B. f (g x) = x" - using linear_id linear_compose[OF \linear g\ \linear f\] - by (intro linear_eq_span) (auto simp: id_def comp_def) + using linear_id linear_compose[OF \linear g\ \linear f\] linear_eq_span by fastforce moreover have "inv_into (span S) f ` B \ span S" using \B \ T\ \span T \ f`span S\ by (auto intro: inv_into_into span_superset) then have "range g \ span S" @@ -2457,8 +2441,8 @@ done with a have a0:"?a \ 0" by auto - have "\x\span B. ?a \ x = 0" - proof (rule span_induct') + have "?a \ x = 0" if "x\span B" for x + proof (rule span_induct [OF that]) show "subspace {x. ?a \ x = 0}" by (auto simp add: subspace_def inner_add) next @@ -2481,9 +2465,9 @@ intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format]) done } - then show "\x \ B. ?a \ x = 0" - by blast - qed + then show "?a \ x = 0" if "x \ B" for x + using that by blast + qed with a0 show ?thesis unfolding sSB by (auto intro: exI[where x="?a"]) qed @@ -2523,35 +2507,27 @@ and fx: "f x = 0" shows "x = 0" using fB ifB fi xsB fx -proof (induct arbitrary: x rule: finite_induct[OF fB]) - case 1 +proof (induction B arbitrary: x rule: finite_induct) + case empty then show ?case by auto next - case (2 a b x) - have fb: "finite b" using "2.prems" by simp + case (insert a b x) have th0: "f ` b \ f ` (insert a b)" - apply (rule image_mono) - apply blast - done - from independent_mono[ OF "2.prems"(2) th0] - have ifb: "independent (f ` b)" . + by (simp add: subset_insertI) + have ifb: "independent (f ` b)" + using independent_mono insert.prems(1) th0 by blast have fib: "inj_on f b" - apply (rule subset_inj_on [OF "2.prems"(3)]) - apply blast - done - from span_breakdown[of a "insert a b", simplified, OF "2.prems"(4)] + using insert.prems(2) by blast + from span_breakdown[of a "insert a b", simplified, OF insert.prems(3)] obtain k where k: "x - k*\<^sub>R a \ span (b - {a})" by blast have "f (x - k*\<^sub>R a) \ span (f ` b)" unfolding span_linear_image[OF lf] - apply (rule imageI) - using k span_mono[of "b - {a}" b] - apply blast - done + using "insert.hyps"(2) k by auto then have "f x - k*\<^sub>R f a \ span (f ` b)" by (simp add: linear_diff[OF lf] linear_cmul[OF lf]) then have th: "-k *\<^sub>R f a \ span (f ` b)" - using "2.prems"(5) by simp + using insert.prems(4) by simp have xsb: "x \ span b" proof (cases "k = 0") case True @@ -2560,19 +2536,18 @@ by blast next case False - with span_mul[OF th, of "- 1/ k"] - have th1: "f a \ span (f ` b)" - by auto - from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric] - have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast - from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"] - have "f a \ span (f ` b)" using tha - using "2.hyps"(2) - "2.prems"(3) by auto - with th1 have False by blast + from inj_on_image_set_diff[OF insert.prems(2), of "insert a b " "{a}", symmetric] + have "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast + then have "f a \ span (f ` b)" + using dependent_def insert.hyps(2) insert.prems(1) by fastforce + moreover have "f a \ span (f ` b)" + using False span_mul[OF th, of "- 1/ k"] by auto + ultimately have False + by blast then show ?thesis by blast qed - from "2.hyps"(3)[OF fb ifb fib xsb "2.prems"(5)] show "x = 0" . + show "x = 0" + using ifb fib xsb insert.IH insert.prems(4) by blast qed text \Can construct an isomorphism between spaces of same dimension.\ @@ -2635,9 +2610,9 @@ fixes f :: "'a::euclidean_space \ _" assumes lf: "linear f" and lg: "linear g" - and fg: "\b\Basis. f b = g b" + and fg: "\b. b \ Basis \ f b = g b" shows "f = g" - using linear_eq[OF lf lg, of _ Basis] fg by auto + using linear_eq[OF _ lf lg, of _ _ Basis] fg by auto text \Similar results for bilinear functions.\ @@ -2646,36 +2621,36 @@ and bg: "bilinear g" and SB: "S \ span B" and TC: "T \ span C" - and fg: "\x\ B. \y\ C. f x y = g x y" - shows "\x\S. \y\T. f x y = g x y " + and "x\S" "y\T" + and fg: "\x y. \x \ B; y\ C\ \ f x y = g x y" + shows "f x y = g x y" proof - let ?P = "{x. \y\ span C. f x y = g x y}" from bf bg have sp: "subspace ?P" unfolding bilinear_def linear_iff subspace_def bf bg - by (auto simp add: span_0 bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def + by (auto simp add: bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add intro: bilinear_ladd[OF bf]) - - have "\x \ span B. \y\ span C. f x y = g x y" - apply (rule span_induct' [OF _ sp]) - apply (rule ballI) - apply (rule span_induct') - apply (simp add: fg) + have sfg: "\x. x \ B \ subspace {a. f x a = g x a}" apply (auto simp add: subspace_def) using bf bg unfolding bilinear_def linear_iff - apply (auto simp add: span_0 bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def + apply (auto simp add: bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add intro: bilinear_ladd[OF bf]) done + have "\y\ span C. f x y = g x y" if "x \ span B" for x + apply (rule span_induct [OF that sp]) + using fg sfg span_induct by blast then show ?thesis - using SB TC by auto + using SB TC assms by auto qed lemma bilinear_eq_stdbasis: fixes f :: "'a::euclidean_space \ 'b::euclidean_space \ _" assumes bf: "bilinear f" and bg: "bilinear g" - and fg: "\i\Basis. \j\Basis. f i j = g i j" + and fg: "\i j. i \ Basis \ j \ Basis \ f i j = g i j" shows "f = g" - using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis] fg] by blast + using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis]] fg + by blast text \An injective map @{typ "'a::euclidean_space \ 'b::euclidean_space"} is also surjective.\ @@ -2695,13 +2670,7 @@ apply (rule card_ge_dim_independent) apply blast apply (rule independent_injective_image[OF B(2) lf fi]) - apply (rule order_eq_refl) - apply (rule sym) - unfolding d - apply (rule card_image) - apply (rule subset_inj_on[OF fi]) - apply blast - done + by (metis card_image d fi inj_on_subset order_refl top_greatest) from th show ?thesis unfolding span_linear_image[OF lf] surj_def using B(3) by blast @@ -2718,11 +2687,8 @@ (is "?lhs \ ?rhs") proof assume h: "?lhs" - { - fix x y - assume x: "x \ S" - assume y: "y \ S" - assume f: "f x = f y" + { fix x y + assume x: "x \ S" and y: "y \ S" and f: "f x = f y" from x fS have S0: "card S \ 0" by auto have "x = y" @@ -2730,15 +2696,13 @@ assume xy: "\ ?thesis" have th: "card S \ card (f ` (S - {y}))" unfolding c - apply (rule card_mono) - apply (rule finite_imageI) - using fS apply simp - using h xy x y f unfolding subset_eq image_iff - apply auto - apply (case_tac "xa = f x") - apply (rule bexI[where x=x]) - apply auto - done + proof (rule card_mono) + show "finite (f ` (S - {y}))" + by (simp add: fS) + show "T \ f ` (S - {y})" + using h xy x y f unfolding subset_eq image_iff + by (metis member_remove remove_def) + qed also have " \ \ card (S - {y})" apply (rule card_image_le) using fS by simp @@ -2751,17 +2715,13 @@ next assume h: ?rhs have "f ` S = T" - apply (rule card_subset_eq[OF fT ST]) - unfolding card_image[OF h] - apply (rule c) - done + by (simp add: ST c card_image card_subset_eq fT h) then show ?lhs by blast qed lemma linear_surjective_imp_injective: fixes f :: "'a::euclidean_space \ 'a::euclidean_space" - assumes lf: "linear f" - and sf: "surj f" + assumes lf: "linear f" and sf: "surj f" shows "inj f" proof - let ?U = "UNIV :: 'a set" @@ -2770,46 +2730,29 @@ by blast { fix x - assume x: "x \ span B" - assume fx: "f x = 0" + assume x: "x \ span B" and fx: "f x = 0" from B(2) have fB: "finite B" using independent_bound by auto + have Uspan: "UNIV \ span (f ` B)" + by (simp add: B(3) lf sf spanning_surjective_image) have fBi: "independent (f ` B)" - apply (rule card_le_dim_spanning[of "f ` B" ?U]) - apply blast - using sf B(3) - unfolding span_linear_image[OF lf] surj_def subset_eq image_iff - apply blast - using fB apply blast - unfolding d[symmetric] - apply (rule card_image_le) - apply (rule fB) - done + proof (rule card_le_dim_spanning) + show "card (f ` B) \ dim ?U" + using card_image_le d fB by fastforce + qed (use fB Uspan in auto) have th0: "dim ?U \ card (f ` B)" - apply (rule span_card_ge_dim) - apply blast - unfolding span_linear_image[OF lf] - apply (rule subset_trans[where B = "f ` UNIV"]) - using sf unfolding surj_def - apply blast - apply (rule image_mono) - apply (rule B(3)) - apply (metis finite_imageI fB) - done + by (rule span_card_ge_dim) (use Uspan fB in auto) moreover have "card (f ` B) \ card B" by (rule card_image_le, rule fB) ultimately have th1: "card B = card (f ` B)" unfolding d by arith have fiB: "inj_on f B" - unfolding surjective_iff_injective_gen[OF fB finite_imageI[OF fB] th1 subset_refl, symmetric] - by blast + by (simp add: eq_card_imp_inj_on fB th1) from linear_indep_image_lemma[OF lf fB fBi fiB x] fx have "x = 0" by blast } then show ?thesis - unfolding linear_injective_0[OF lf] - using B(3) - by blast + unfolding linear_injective_0[OF lf] using B(3) by blast qed text \Hence either is enough for isomorphism.\ @@ -2865,9 +2808,7 @@ assume lf: "linear f" "linear f'" assume f: "f \ f' = id" from f have sf: "surj f" - apply (auto simp add: o_def id_def surj_def) - apply metis - done + by (auto simp add: o_def id_def surj_def) metis from linear_surjective_isomorphism[OF lf(1) sf] lf f have "f' \ f = id" unfolding fun_eq_iff o_def id_def by metis @@ -2885,18 +2826,13 @@ shows "linear g" proof - from gf have fi: "inj f" - apply (auto simp add: inj_on_def o_def id_def fun_eq_iff) - apply metis - done + by (auto simp add: inj_on_def o_def id_def fun_eq_iff) metis from linear_injective_isomorphism[OF lf fi] - obtain h :: "'a \ 'a" where h: "linear h" "\x. h (f x) = x" "\x. f (h x) = x" + obtain h :: "'a \ 'a" where "linear h" and h: "\x. h (f x) = x" "\x. f (h x) = x" by blast have "h = g" - apply (rule ext) using gf h(2,3) - apply (simp add: o_def id_def fun_eq_iff) - apply metis - done - with h(1) show ?thesis by blast + by (metis gf h isomorphism_expand left_right_inverse_eq) + with \linear h\ show ?thesis by blast qed lemma inj_linear_imp_inv_linear: @@ -2955,28 +2891,21 @@ by (simp add: infnorm_eq_0) lemma infnorm_neg: "infnorm (- x) = infnorm x" - unfolding infnorm_def - apply (rule cong[of "Sup" "Sup"]) - apply blast - apply auto - done + unfolding infnorm_def by simp lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)" -proof - - have "y - x = - (x - y)" by simp - then show ?thesis - by (metis infnorm_neg) -qed - -lemma real_abs_sub_infnorm: "\infnorm x - infnorm y\ \ infnorm (x - y)" + by (metis infnorm_neg minus_diff_eq) + +lemma absdiff_infnorm: "\infnorm x - infnorm y\ \ infnorm (x - y)" proof - - have th: "\(nx::real) n ny. nx \ n + ny \ ny \ n + nx \ \nx - ny\ \ n" + have *: "\(nx::real) n ny. nx \ n + ny \ ny \ n + nx \ \nx - ny\ \ n" by arith - from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"] - have ths: "infnorm x \ infnorm (x - y) + infnorm y" - "infnorm y \ infnorm (x - y) + infnorm x" - by (simp_all add: field_simps infnorm_neg) - from th[OF ths] show ?thesis . + show ?thesis + proof (rule *) + from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"] + show "infnorm x \ infnorm (x - y) + infnorm y" "infnorm y \ infnorm (x - y) + infnorm x" + by (simp_all add: field_simps infnorm_neg) + qed qed lemma real_abs_infnorm: "\infnorm x\ = infnorm x" @@ -2991,8 +2920,7 @@ unfolding infnorm_Max proof (safe intro!: Max_eqI) let ?B = "(\i. \x \ i\) ` Basis" - { - fix b :: 'a + { fix b :: 'a assume "b \ Basis" then show "\a *\<^sub>R x \ b\ \ \a\ * Max ?B" by (simp add: abs_mult mult_left_mono) @@ -3018,27 +2946,17 @@ lemma norm_le_infnorm: fixes x :: "'a::euclidean_space" shows "norm x \ sqrt DIM('a) * infnorm x" -proof - - let ?d = "DIM('a)" - have "real ?d \ 0" - by simp - then have d2: "(sqrt (real ?d))\<^sup>2 = real ?d" - by (auto intro: real_sqrt_pow2) - have th: "sqrt (real ?d) * infnorm x \ 0" + unfolding norm_eq_sqrt_inner id_def +proof (rule real_le_lsqrt[OF inner_ge_zero]) + show "sqrt DIM('a) * infnorm x \ 0" by (simp add: zero_le_mult_iff infnorm_pos_le) - have th1: "x \ x \ (sqrt (real ?d) * infnorm x)\<^sup>2" - unfolding power_mult_distrib d2 - apply (subst euclidean_inner) - apply (subst power2_abs[symmetric]) - apply (rule order_trans[OF sum_bounded_above[where K="\infnorm x\\<^sup>2"]]) - apply (auto simp add: power2_eq_square[symmetric]) - apply (subst power2_abs[symmetric]) - apply (rule power_mono) - apply (auto simp: infnorm_Max) - done - from real_le_lsqrt[OF inner_ge_zero th th1] - show ?thesis - unfolding norm_eq_sqrt_inner id_def . + have "x \ x \ (\b\Basis. x \ b * (x \ b))" + by (metis euclidean_inner order_refl) + also have "... \ DIM('a) * \infnorm x\\<^sup>2" + by (rule sum_bounded_above) (metis Basis_le_infnorm abs_le_square_iff power2_eq_square real_abs_infnorm) + also have "... \ (sqrt DIM('a) * infnorm x)\<^sup>2" + by (simp add: power_mult_distrib) + finally show "x \ x \ (sqrt DIM('a) * infnorm x)\<^sup>2" . qed lemma tendsto_infnorm [tendsto_intros]: @@ -3048,46 +2966,30 @@ fix r :: real assume "r > 0" then show "\s>0. \x. x \ a \ norm (x - a) < s \ norm (infnorm x - infnorm a) < r" - by (metis real_norm_def le_less_trans real_abs_sub_infnorm infnorm_le_norm) + by (metis real_norm_def le_less_trans absdiff_infnorm infnorm_le_norm) qed text \Equality in Cauchy-Schwarz and triangle inequalities.\ lemma norm_cauchy_schwarz_eq: "x \ y = norm x * norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x" (is "?lhs \ ?rhs") -proof - - { - assume h: "x = 0" - then have ?thesis by simp - } - moreover - { - assume h: "y = 0" - then have ?thesis by simp - } - moreover - { - assume x: "x \ 0" and y: "y \ 0" - from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"] - have "?rhs \ +proof (cases "x=0") + case True + then show ?thesis + by auto +next + case False + from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"] + have "?rhs \ (norm y * (norm y * norm x * norm x - norm x * (x \ y)) - norm x * (norm y * (y \ x) - norm x * norm y * norm y) = 0)" - using x y - unfolding inner_simps - unfolding power2_norm_eq_inner[symmetric] power2_eq_square right_minus_eq - apply (simp add: inner_commute) - apply (simp add: field_simps) - apply metis - done - also have "\ \ (2 * norm x * norm y * (norm x * norm y - x \ y) = 0)" using x y - by (simp add: field_simps inner_commute) - also have "\ \ ?lhs" using x y - apply simp - apply metis - done - finally have ?thesis by blast - } - ultimately show ?thesis by blast + using False unfolding inner_simps + by (auto simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps) + also have "\ \ (2 * norm x * norm y * (norm x * norm y - x \ y) = 0)" + using False by (simp add: field_simps inner_commute) + also have "\ \ ?lhs" + using False by auto + finally show ?thesis by metis qed lemma norm_cauchy_schwarz_abs_eq: @@ -3099,7 +3001,7 @@ by arith have "?rhs \ norm x *\<^sub>R y = norm y *\<^sub>R x \ norm (- x) *\<^sub>R y = norm y *\<^sub>R (- x)" by simp - also have "\ \(x \ y = norm x * norm y \ (- x) \ y = norm x * norm y)" + also have "\ \ (x \ y = norm x * norm y \ (- x) \ y = norm x * norm y)" unfolding norm_cauchy_schwarz_eq[symmetric] unfolding norm_minus_cancel norm_scaleR .. also have "\ \ ?lhs" @@ -3111,33 +3013,21 @@ lemma norm_triangle_eq: fixes x y :: "'a::real_inner" shows "norm (x + y) = norm x + norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x" -proof - - { - assume x: "x = 0 \ y = 0" - then have ?thesis - by (cases "x = 0") simp_all - } - moreover - { - assume x: "x \ 0" and y: "y \ 0" - then have "norm x \ 0" "norm y \ 0" - by simp_all - then have n: "norm x > 0" "norm y > 0" - using norm_ge_zero[of x] norm_ge_zero[of y] by arith+ - have th: "\(a::real) b c. a + b + c \ 0 \ a = b + c \ a\<^sup>2 = (b + c)\<^sup>2" - by algebra - have "norm (x + y) = norm x + norm y \ (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2" - apply (rule th) - using n norm_ge_zero[of "x + y"] - apply arith - done - also have "\ \ norm x *\<^sub>R y = norm y *\<^sub>R x" - unfolding norm_cauchy_schwarz_eq[symmetric] - unfolding power2_norm_eq_inner inner_simps - by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps) - finally have ?thesis . - } - ultimately show ?thesis by blast +proof (cases "x = 0 \ y = 0") + case True + then show ?thesis + by force +next + case False + then have n: "norm x > 0" "norm y > 0" + by auto + have "norm (x + y) = norm x + norm y \ (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2" + by simp + also have "\ \ norm x *\<^sub>R y = norm y *\<^sub>R x" + unfolding norm_cauchy_schwarz_eq[symmetric] + unfolding power2_norm_eq_inner inner_simps + by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps) + finally show ?thesis . qed @@ -3196,81 +3086,67 @@ lemma collinear_2 [iff]: "collinear {x, y}" apply (simp add: collinear_def) apply (rule exI[where x="x - y"]) - apply auto - apply (rule exI[where x=1], simp) - apply (rule exI[where x="- 1"], simp) - done + by (metis minus_diff_eq scaleR_left.minus scaleR_one) lemma collinear_lemma: "collinear {0, x, y} \ x = 0 \ y = 0 \ (\c. y = c *\<^sub>R x)" (is "?lhs \ ?rhs") -proof - - { - assume "x = 0 \ y = 0" - then have ?thesis - by (cases "x = 0") (simp_all add: collinear_2 insert_commute) - } - moreover - { - assume x: "x \ 0" and y: "y \ 0" - have ?thesis - proof - assume h: "?lhs" - then obtain u where u: "\ x\ {0,x,y}. \y\ {0,x,y}. \c. x - y = c *\<^sub>R u" - unfolding collinear_def by blast - from u[rule_format, of x 0] u[rule_format, of y 0] - obtain cx and cy where - cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u" - by auto - from cx x have cx0: "cx \ 0" by auto - from cy y have cy0: "cy \ 0" by auto - let ?d = "cy / cx" - from cx cy cx0 have "y = ?d *\<^sub>R x" - by simp - then show ?rhs using x y by blast - next - assume h: "?rhs" - then obtain c where c: "y = c *\<^sub>R x" - using x y by blast - show ?lhs - unfolding collinear_def c - apply (rule exI[where x=x]) - apply auto - apply (rule exI[where x="- 1"], simp) - apply (rule exI[where x= "-c"], simp) +proof (cases "x = 0 \ y = 0") + case True + then show ?thesis + by (auto simp: insert_commute) +next + case False + show ?thesis + proof + assume h: "?lhs" + then obtain u where u: "\ x\ {0,x,y}. \y\ {0,x,y}. \c. x - y = c *\<^sub>R u" + unfolding collinear_def by blast + from u[rule_format, of x 0] u[rule_format, of y 0] + obtain cx and cy where + cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u" + by auto + from cx cy False have cx0: "cx \ 0" and cy0: "cy \ 0" by auto + let ?d = "cy / cx" + from cx cy cx0 have "y = ?d *\<^sub>R x" + by simp + then show ?rhs using False by blast + next + assume h: "?rhs" + then obtain c where c: "y = c *\<^sub>R x" + using False by blast + show ?lhs + unfolding collinear_def c + apply (rule exI[where x=x]) + apply auto + apply (rule exI[where x="- 1"], simp) + apply (rule exI[where x= "-c"], simp) apply (rule exI[where x=1], simp) - apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib) - apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib) - done - qed - } - ultimately show ?thesis by blast + apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib) + apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib) + done + qed qed lemma norm_cauchy_schwarz_equal: "\x \ y\ = norm x * norm y \ collinear {0, x, y}" - unfolding norm_cauchy_schwarz_abs_eq - apply (cases "x=0", simp_all) - apply (cases "y=0", simp_all add: insert_commute) - unfolding collinear_lemma - apply simp - apply (subgoal_tac "norm x \ 0") - apply (subgoal_tac "norm y \ 0") - apply (rule iffI) - apply (cases "norm x *\<^sub>R y = norm y *\<^sub>R x") - apply (rule exI[where x="(1/norm x) * norm y"]) - apply (drule sym) - unfolding scaleR_scaleR[symmetric] - apply (simp add: field_simps) - apply (rule exI[where x="(1/norm x) * - norm y"]) - apply clarify - apply (drule sym) - unfolding scaleR_scaleR[symmetric] - apply (simp add: field_simps) - apply (erule exE) - apply (erule ssubst) - unfolding scaleR_scaleR - unfolding norm_scaleR - apply (subgoal_tac "norm x * c = \c\ * norm x \ norm x * c = - \c\ * norm x") - apply (auto simp add: field_simps) - done +proof (cases "x=0") + case True + then show ?thesis + by (auto simp: insert_commute) +next + case False + then have nnz: "norm x \ 0" + by auto + show ?thesis + proof + assume "\x \ y\ = norm x * norm y" + then show "collinear {0, x, y}" + unfolding norm_cauchy_schwarz_abs_eq collinear_lemma + by (meson eq_vector_fraction_iff nnz) + next + assume "collinear {0, x, y}" + with False show "\x \ y\ = norm x * norm y" + unfolding norm_cauchy_schwarz_abs_eq collinear_lemma by (auto simp: abs_if) + qed +qed end diff -r b249fab48c76 -r d2daeef3ce47 src/HOL/Analysis/Starlike.thy --- a/src/HOL/Analysis/Starlike.thy Wed May 02 12:47:56 2018 +0100 +++ b/src/HOL/Analysis/Starlike.thy Wed May 02 12:48:08 2018 +0100 @@ -19,10 +19,7 @@ where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)" lemma midpoint_idem [simp]: "midpoint x x = x" - unfolding midpoint_def - unfolding scaleR_right_distrib - unfolding scaleR_left_distrib[symmetric] - by auto + unfolding midpoint_def by simp lemma midpoint_sym: "midpoint a b = midpoint b a" unfolding midpoint_def by (auto simp add: scaleR_right_distrib) @@ -924,61 +921,49 @@ proof (cases "a = b") case True then show ?thesis - unfolding between_def split_conv - by (auto simp add: dist_commute) + by (auto simp add: between_def dist_commute) next case False then have Fal: "norm (a - b) \ 0" and Fal2: "norm (a - b) > 0" by auto have *: "\u. a - ((1 - u) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a - b)" by (auto simp add: algebra_simps) - show ?thesis - unfolding between_def split_conv closed_segment_def mem_Collect_eq - apply rule - apply (elim exE conjE) - apply (subst dist_triangle_eq) + 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 \ u" "u \ 1" for u proof - - fix u - assume as: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \ u" "u \ 1" - then have *: "a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)" - unfolding as(1) by (auto simp add:algebra_simps) + 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 as(2,3) + unfolding norm_minus_commute[of x a] * using \0 \ u\ \u \ 1\ by (auto simp add: field_simps) - next - assume as: "dist a b = dist a x + dist x b" - have "norm (a - x) / norm (a - b) \ 1" - using Fal2 unfolding as[unfolded dist_norm] norm_ge_zero by auto - then show "\u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \ 0 \ u \ u \ 1" - apply (rule_tac x="dist a x / dist a b" in exI) - unfolding dist_norm - apply (subst euclidean_eq_iff) - apply rule - defer - apply rule - prefer 3 - apply rule - proof - - fix i :: 'a - assume i: "i \ Basis" - have "((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) \ i = - ((norm (a - b) - norm (a - x)) * (a \ i) + norm (a - x) * (b \ i)) / norm (a - b)" - using Fal by (auto simp add: field_simps inner_simps) - also have "\ = x\i" - apply (rule divide_eq_imp[OF Fal]) - unfolding as[unfolded dist_norm] - using as[unfolded dist_triangle_eq] - apply - - apply (subst (asm) euclidean_eq_iff) - using i - apply (erule_tac x=i in ballE) - apply (auto simp add: field_simps inner_simps) - done - finally show "x \ i = - ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) \ i" - by auto - qed (insert Fal2, auto) qed + moreover have "\u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \ 0 \ u \ u \ 1" if "dist a b = dist a x + dist x b" + proof - + let ?\ = "norm (a - x) / norm (a - b)" + show "\u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \ 0 \ u \ u \ 1" + proof (intro exI conjI) + show "?\ \ 1" + using Fal2 unfolding that[unfolded dist_norm] norm_ge_zero by auto + show "x = (1 - ?\) *\<^sub>R a + (?\) *\<^sub>R b" + proof (subst euclidean_eq_iff; intro ballI) + fix i :: 'a + assume i: "i \ Basis" + have "((1 - ?\) *\<^sub>R a + (?\) *\<^sub>R b) \ i + = ((norm (a - b) - norm (a - x)) * (a \ i) + norm (a - x) * (b \ i)) / norm (a - b)" + using Fal by (auto simp add: field_simps inner_simps) + also have "\ = x\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 \ i = ((1 - ?\) *\<^sub>R a + (?\) *\<^sub>R b) \ 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: @@ -990,10 +975,7 @@ by auto show ?t1 ?t2 unfolding between midpoint_def dist_norm - apply(rule_tac[!] *) - unfolding euclidean_eq_iff[where 'a='a] - apply (auto simp add: field_simps inner_simps) - done + by (auto simp add: field_simps inner_simps euclidean_eq_iff[where 'a='a] intro!: *) qed lemma between_mem_convex_hull: @@ -1058,25 +1040,23 @@ subsection%unimportant \Shrinking towards the interior of a convex set\ lemma mem_interior_convex_shrink: - fixes s :: "'a::euclidean_space set" - assumes "convex s" - and "c \ interior s" - and "x \ s" + fixes S :: "'a::euclidean_space set" + assumes "convex S" + and "c \ interior S" + and "x \ S" and "0 < e" and "e \ 1" - shows "x - e *\<^sub>R (x - c) \ interior s" -proof - - obtain d where "d > 0" and d: "ball c d \ s" + shows "x - e *\<^sub>R (x - c) \ interior S" +proof - + obtain d where "d > 0" and d: "ball c d \ S" using assms(2) unfolding mem_interior by auto show ?thesis unfolding mem_interior - apply (rule_tac x="e*d" in exI) - apply rule - defer - unfolding subset_eq Ball_def mem_ball - proof (rule, rule) + proof (intro exI subsetI conjI) fix y - assume as: "dist (x - e *\<^sub>R (x - c)) y < e * d" + assume "y \ ball (x - e *\<^sub>R (x - c)) (e*d)" + then have as: "dist (x - e *\<^sub>R (x - c)) y < e * d" + by simp have *: "y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using \e > 0\ by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib) have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = \1/e\ * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)" @@ -1090,7 +1070,7 @@ also have "\ < d" using as[unfolded dist_norm] and \e > 0\ by (auto simp add:pos_divide_less_eq[OF \e > 0\] mult.commute) - finally show "y \ s" + finally show "y \ S" apply (subst *) apply (rule assms(1)[unfolded convex_alt,rule_format]) apply (rule d[unfolded subset_eq,rule_format]) @@ -1102,18 +1082,18 @@ qed lemma mem_interior_closure_convex_shrink: - fixes s :: "'a::euclidean_space set" - assumes "convex s" - and "c \ interior s" - and "x \ closure s" + fixes S :: "'a::euclidean_space set" + assumes "convex S" + and "c \ interior S" + and "x \ closure S" and "0 < e" and "e \ 1" - shows "x - e *\<^sub>R (x - c) \ interior s" -proof - - obtain d where "d > 0" and d: "ball c d \ s" + shows "x - e *\<^sub>R (x - c) \ interior S" +proof - + obtain d where "d > 0" and d: "ball c d \ S" using assms(2) unfolding mem_interior by auto - have "\y\s. norm (y - x) * (1 - e) < e * d" - proof (cases "x \ s") + have "\y\S. norm (y - x) * (1 - e) < e * d" + proof (cases "x \ S") case True then show ?thesis using \e > 0\ \d > 0\ @@ -1122,12 +1102,12 @@ done next case False - then have x: "x islimpt s" + then have x: "x islimpt S" using assms(3)[unfolded closure_def] by auto show ?thesis proof (cases "e = 1") case True - obtain y where "y \ s" "y \ x" "dist y x < 1" + obtain y where "y \ S" "y \ x" "dist y x < 1" using x[unfolded islimpt_approachable,THEN spec[where x=1]] by auto then show ?thesis apply (rule_tac x=y in bexI) @@ -1139,7 +1119,7 @@ case False then have "0 < e * d / (1 - e)" and *: "1 - e > 0" using \e \ 1\ \e > 0\ \d > 0\ by auto - then obtain y where "y \ s" "y \ x" "dist y x < e * d / (1 - e)" + then obtain y where "y \ S" "y \ x" "dist y x < e * d / (1 - e)" using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto then show ?thesis apply (rule_tac x=y in bexI) @@ -1149,24 +1129,20 @@ done qed qed - then obtain y where "y \ s" and y: "norm (y - x) * (1 - e) < e * d" + then obtain y where "y \ S" and y: "norm (y - x) * (1 - e) < e * d" by auto define z where "z = c + ((1 - e) / e) *\<^sub>R (x - y)" have *: "x - e *\<^sub>R (x - c) = y - e *\<^sub>R (y - z)" unfolding z_def using \e > 0\ by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib) - have "z \ interior s" + have "z \ interior S" apply (rule interior_mono[OF d,unfolded subset_eq,rule_format]) unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5) apply (auto simp add:field_simps norm_minus_commute) done then show ?thesis unfolding * - apply - - apply (rule mem_interior_convex_shrink) - using assms(1,4-5) \y\s\ - apply auto - done + using mem_interior_convex_shrink \y \ S\ assms by blast qed lemma in_interior_closure_convex_segment: @@ -1252,23 +1228,20 @@ subsection%unimportant \Some obvious but surprisingly hard simplex lemmas\ lemma simplex: - assumes "finite s" - and "0 \ s" - shows "convex hull (insert 0 s) = - {y. (\u. (\x\s. 0 \ u x) \ sum u s \ 1 \ sum (\x. u x *\<^sub>R x) s = y)}" - unfolding convex_hull_finite[OF finite.insertI[OF assms(1)]] - apply (rule set_eqI, rule) - unfolding mem_Collect_eq - apply (erule_tac[!] exE) - apply (erule_tac[!] conjE)+ - unfolding sum_clauses(2)[OF \finite s\] - apply (rule_tac x=u in exI) - defer - apply (rule_tac x="\x. if x = 0 then 1 - sum u s else u x" in exI) - using assms(2) - unfolding if_smult and sum_delta_notmem[OF assms(2)] - apply auto - done + assumes "finite S" + and "0 \ S" + shows "convex hull (insert 0 S) = {y. \u. (\x\S. 0 \ u x) \ sum u S \ 1 \ sum (\x. u x *\<^sub>R x) S = y}" +proof (simp add: convex_hull_finite set_eq_iff assms, safe) + fix x and u :: "'a \ real" + assume "0 \ u 0" "\x\S. 0 \ u x" "u 0 + sum u S = 1" + then show "\v. (\x\S. 0 \ v x) \ sum v S \ 1 \ (\x\S. v x *\<^sub>R x) = (\x\S. u x *\<^sub>R x)" + by force +next + fix x and u :: "'a \ real" + assume "\x\S. 0 \ u x" "sum u S \ 1" + then show "\v. 0 \ v 0 \ (\x\S. 0 \ v x) \ v 0 + sum v S = 1 \ (\x\S. v x *\<^sub>R x) = (\x\S. u x *\<^sub>R x)" + by (rule_tac x="\x. if x = 0 then 1 - sum u S else u x" in exI) (auto simp: sum_delta_notmem assms if_smult) +qed lemma substd_simplex: assumes d: "d \ Basis" @@ -1283,50 +1256,27 @@ by (blast intro: finite_subset finite_Basis) show ?thesis unfolding simplex[OF \finite d\ \0 \ ?p\] - apply (rule set_eqI) - unfolding mem_Collect_eq - apply rule - apply (elim exE conjE) - apply (erule_tac[2] conjE)+ - proof - - fix x :: "'a::euclidean_space" - fix u - assume as: "\x\?D. 0 \ u x" "sum u ?D \ 1" "(\x\?D. u x *\<^sub>R x) = x" - have *: "\i\Basis. i \ d \ u i = x\i" - and "(\i\Basis. i \ d \ x \ i = 0)" - using as(3) - unfolding substdbasis_expansion_unique[OF assms] - by auto - then have **: "sum u ?D = sum ((\) x) ?D" - apply - - apply (rule sum.cong) - using assms - apply auto - done - have "(\i\Basis. 0 \ x\i) \ sum ((\) x) ?D \ 1" - proof (rule,rule) - fix i :: 'a - assume i: "i \ Basis" - have "i \ d \ 0 \ x\i" - unfolding *[rule_format,OF i,symmetric] - apply (rule_tac as(1)[rule_format]) - apply auto - done - moreover have "i \ d \ 0 \ x\i" - using \(\i\Basis. i \ d \ x \ i = 0)\[rule_format, OF i] by auto - ultimately show "0 \ x\i" by auto - qed (insert as(2)[unfolded **], auto) - then show "(\i\Basis. 0 \ x\i) \ sum ((\) x) ?D \ 1 \ (\i\Basis. i \ d \ x \ i = 0)" - using \(\i\Basis. i \ d \ x \ i = 0)\ by auto + proof (intro set_eqI; safe) + fix u :: "'a \ real" + assume as: "\x\?D. 0 \ u x" "sum u ?D \ 1" + let ?x = "(\x\?D. u x *\<^sub>R x)" + have ind: "\i\Basis. i \ d \ u i = ?x \ i" + and notind: "(\i\Basis. i \ d \ ?x \ i = 0)" + using substdbasis_expansion_unique[OF assms] by blast+ + then have **: "sum u ?D = sum ((\) ?x) ?D" + using assms by (auto intro!: sum.cong) + show "0 \ ?x \ i" if "i \ Basis" for i + using as(1) ind notind that by fastforce + show "sum ((\) ?x) ?D \ 1" + using "**" as(2) by linarith + show "?x \ i = 0" if "i \ Basis" "i \ d" for i + using notind that by blast next - fix x :: "'a::euclidean_space" - assume as: "\i\Basis. 0 \ x \ i" "sum ((\) x) ?D \ 1" "(\i\Basis. i \ d \ x \ i = 0)" - show "\u. (\x\?D. 0 \ u x) \ sum u ?D \ 1 \ (\x\?D. u x *\<^sub>R x) = x" - using as d - unfolding substdbasis_expansion_unique[OF assms] - apply (rule_tac x="inner x" in exI) - apply auto - done + fix x + assume "\i\Basis. 0 \ x \ i" "sum ((\) x) ?D \ 1" "(\i\Basis. i \ d \ x \ i = 0)" + with d show "\u. (\x\?D. 0 \ u x) \ sum u ?D \ 1 \ (\x\?D. u x *\<^sub>R x) = x" + unfolding substdbasis_expansion_unique[OF assms] + by (rule_tac x="inner x" in exI) auto qed qed @@ -1338,27 +1288,18 @@ lemma interior_std_simplex: "interior (convex hull (insert 0 Basis)) = {x::'a::euclidean_space. (\i\Basis. 0 < x\i) \ sum (\i. x\i) Basis < 1}" - apply (rule set_eqI) - unfolding mem_interior std_simplex - unfolding subset_eq mem_Collect_eq Ball_def mem_ball - unfolding Ball_def[symmetric] - apply rule - apply (elim exE conjE) - defer - apply (erule conjE) -proof - + unfolding set_eq_iff mem_interior std_simplex +proof (intro allI iffI CollectI; clarify) fix x :: 'a fix e - assume "e > 0" and as: "\xa. dist x xa < e \ (\x\Basis. 0 \ xa \ x) \ sum ((\) xa) Basis \ 1" - show "(\xa\Basis. 0 < x \ xa) \ sum ((\) x) Basis < 1" - apply safe - proof - + assume "e > 0" and as: "ball x e \ {x. (\i\Basis. 0 \ x \ i) \ sum ((\) x) Basis \ 1}" + show "(\i\Basis. 0 < x \ i) \ sum ((\) x) Basis < 1" + proof safe fix i :: 'a assume i: "i \ Basis" then show "0 < x \ i" - using as[THEN spec[where x="x - (e / 2) *\<^sub>R i"]] and \e > 0\ - unfolding dist_norm - by (auto elim!: ballE[where x=i] simp: inner_simps) + using as[THEN subsetD[where c="x - (e / 2) *\<^sub>R i"]] and \e > 0\ + by (force simp add: inner_simps) next have **: "dist x (x + (e / 2) *\<^sub>R (SOME i. i\Basis)) < e" using \e > 0\ unfolding dist_norm @@ -1368,42 +1309,31 @@ by (auto simp: SOME_Basis inner_Basis inner_simps) then have *: "sum ((\) (x + (e / 2) *\<^sub>R (SOME i. i\Basis))) Basis = sum (\i. x\i + (if (SOME i. i\Basis) = i then e/2 else 0)) Basis" - apply (rule_tac sum.cong) - apply auto - done + by (auto simp: intro!: sum.cong) have "sum ((\) x) Basis < sum ((\) (x + (e / 2) *\<^sub>R (SOME i. i\Basis))) Basis" - unfolding * sum.distrib - using \e > 0\ DIM_positive[where 'a='a] - apply (subst sum.delta') - apply (auto simp: SOME_Basis) - done + using \e > 0\ DIM_positive by (auto simp: SOME_Basis sum.distrib *) also have "\ \ 1" - using ** - apply (drule_tac as[rule_format]) - apply auto - done + using ** as by force finally show "sum ((\) x) Basis < 1" by auto - qed + qed next fix x :: 'a assume as: "\i\Basis. 0 < x \ i" "sum ((\) x) Basis < 1" obtain a :: 'b where "a \ UNIV" using UNIV_witness .. let ?d = "(1 - sum ((\) x) Basis) / real (DIM('a))" - show "\e>0. \y. dist x y < e \ (\i\Basis. 0 \ y \ i) \ sum ((\) y) Basis \ 1" - proof (rule_tac x="min (Min (((\) x) ` Basis)) D" for D in exI, intro conjI impI allI) + show "\e>0. ball x e \ {x. (\i\Basis. 0 \ x \ i) \ sum ((\) x) Basis \ 1}" + proof (rule_tac x="min (Min (((\) x) ` Basis)) D" for D in exI, intro conjI subsetI CollectI) fix y - assume y: "dist x y < min (Min ((\) x ` Basis)) ?d" + assume y: "y \ ball x (min (Min ((\) x ` Basis)) ?d)" have "sum ((\) y) Basis \ sum (\i. x\i + ?d) Basis" proof (rule sum_mono) fix i :: 'a assume i: "i \ Basis" - then have "\y\i - x\i\ < ?d" - apply - - apply (rule le_less_trans) - using Basis_le_norm[OF i, of "y - x"] - using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] - apply (auto simp add: norm_minus_commute inner_diff_left) - done + have "\y\i - x\i\ \ norm (y - x)" + by (metis Basis_le_norm i inner_commute inner_diff_right) + also have "... < ?d" + using y by (simp add: dist_norm norm_minus_commute) + finally have "\y\i - x\i\ < ?d" . then show "y \ i \ x \ i + ?d" by auto qed also have "\ \ 1" @@ -1414,12 +1344,11 @@ proof safe fix i :: 'a assume i: "i \ Basis" - have "norm (x - y) < x\i" - apply (rule less_le_trans) - apply (rule y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]) - using i - apply auto - done + have "norm (x - y) < MINIMUM Basis ((\) x)" + using y by (auto simp: dist_norm less_eq_real_def) + also have "... \ x\i" + using i by auto + finally have "norm (x - y) < x\i" . then show "0 \ y\i" using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format, OF i] by (auto simp: inner_simps) @@ -1469,82 +1398,70 @@ qed lemma rel_interior_substd_simplex: - assumes d: "d \ Basis" - shows "rel_interior (convex hull (insert 0 d)) = - {x::'a::euclidean_space. (\i\d. 0 < x\i) \ (\i\d. x\i) < 1 \ (\i\Basis. i \ d \ x\i = 0)}" + assumes D: "D \ Basis" + shows "rel_interior (convex hull (insert 0 D)) = + {x::'a::euclidean_space. (\i\D. 0 < x\i) \ (\i\D. x\i) < 1 \ (\i\Basis. i \ D \ x\i = 0)}" (is "rel_interior (convex hull (insert 0 ?p)) = ?s") proof - - have "finite d" - apply (rule finite_subset) - using assms - apply auto - done + have "finite D" + using D finite_Basis finite_subset by blast show ?thesis - proof (cases "d = {}") + proof (cases "D = {}") case True then show ?thesis using rel_interior_sing using euclidean_eq_iff[of _ 0] by auto next case False have h0: "affine hull (convex hull (insert 0 ?p)) = - {x::'a::euclidean_space. (\i\Basis. i \ d \ x\i = 0)}" + {x::'a::euclidean_space. (\i\Basis. i \ D \ x\i = 0)}" using affine_hull_convex_hull affine_hull_substd_basis assms by auto - have aux: "\x::'a. \i\Basis. (\i\d. 0 \ x\i) \ (\i\Basis. i \ d \ x\i = 0) \ 0 \ x\i" + have aux: "\x::'a. \i\Basis. (\i\D. 0 \ x\i) \ (\i\Basis. i \ D \ x\i = 0) \ 0 \ x\i" by auto { fix x :: "'a::euclidean_space" assume x: "x \ rel_interior (convex hull (insert 0 ?p))" - then obtain e where e0: "e > 0" and - "ball x e \ {xa. (\i\Basis. i \ d \ xa\i = 0)} \ convex hull (insert 0 ?p)" + then obtain e where "e > 0" and + "ball x e \ {xa. (\i\Basis. i \ D \ xa\i = 0)} \ convex hull (insert 0 ?p)" using mem_rel_interior_ball[of x "convex hull (insert 0 ?p)"] h0 by auto - then have as: "\xa. dist x xa < e \ (\i\Basis. i \ d \ xa\i = 0) \ - (\i\d. 0 \ xa \ i) \ sum ((\) xa) d \ 1" + then have as [rule_format]: "\y. dist x y < e \ (\i\Basis. i \ D \ y\i = 0) \ + (\i\D. 0 \ y \ i) \ sum ((\) y) D \ 1" unfolding ball_def unfolding substd_simplex[OF assms] using assms by auto - have x0: "(\i\Basis. i \ d \ x\i = 0)" + have x0: "(\i\Basis. i \ D \ x\i = 0)" using x rel_interior_subset substd_simplex[OF assms] by auto - have "(\i\d. 0 < x \ i) \ sum ((\) x) d < 1 \ (\i\Basis. i \ d \ x\i = 0)" - apply rule - apply rule - proof - + have "(\i\D. 0 < x \ i) \ sum ((\) x) D < 1 \ (\i\Basis. i \ D \ x\i = 0)" + proof (intro conjI ballI) fix i :: 'a - assume "i \ d" - then have "\ia\d. 0 \ (x - (e / 2) *\<^sub>R i) \ ia" + assume "i \ D" + then have "\j\D. 0 \ (x - (e / 2) *\<^sub>R i) \ j" apply - - apply (rule as[rule_format,THEN conjunct1]) - unfolding dist_norm - using d \e > 0\ x0 - apply (auto simp: inner_simps inner_Basis) + apply (rule as[THEN conjunct1]) + using D \e > 0\ x0 + apply (auto simp: dist_norm inner_simps inner_Basis) done then show "0 < x \ i" - apply (erule_tac x=i in ballE) - using \e > 0\ \i \ d\ d - apply (auto simp: inner_simps inner_Basis) - done + using \e > 0\ \i \ D\ D by (force simp: inner_simps inner_Basis) next - obtain a where a: "a \ d" - using \d \ {}\ by auto + obtain a where a: "a \ D" + using \D \ {}\ by auto then have **: "dist x (x + (e / 2) *\<^sub>R a) < e" - using \e > 0\ norm_Basis[of a] d + using \e > 0\ norm_Basis[of a] D unfolding dist_norm by auto have "\i. i \ Basis \ (x + (e / 2) *\<^sub>R a) \ i = x\i + (if i = a then e/2 else 0)" - using a d by (auto simp: inner_simps inner_Basis) - then have *: "sum ((\) (x + (e / 2) *\<^sub>R a)) d = - sum (\i. x\i + (if a = i then e/2 else 0)) d" - using d by (intro sum.cong) auto + using a D by (auto simp: inner_simps inner_Basis) + then have *: "sum ((\) (x + (e / 2) *\<^sub>R a)) D = + sum (\i. x\i + (if a = i then e/2 else 0)) D" + using D by (intro sum.cong) auto have "a \ Basis" - using \a \ d\ d by auto - then have h1: "(\i\Basis. i \ d \ (x + (e / 2) *\<^sub>R a) \ i = 0)" - using x0 d \a\d\ by (auto simp add: inner_add_left inner_Basis) - have "sum ((\) x) d < sum ((\) (x + (e / 2) *\<^sub>R a)) d" - unfolding * sum.distrib - using \e > 0\ \a \ d\ - using \finite d\ - by (auto simp add: sum.delta') + using \a \ D\ D by auto + then have h1: "(\i\Basis. i \ D \ (x + (e / 2) *\<^sub>R a) \ i = 0)" + using x0 D \a\D\ by (auto simp add: inner_add_left inner_Basis) + have "sum ((\) x) D < sum ((\) (x + (e / 2) *\<^sub>R a)) D" + using \e > 0\ \a \ D\ \finite D\ by (auto simp add: * sum.distrib) also have "\ \ 1" using ** h1 as[rule_format, of "x + (e / 2) *\<^sub>R a"] by auto - finally show "sum ((\) x) d < 1 \ (\i\Basis. i \ d \ x\i = 0)" + finally show "sum ((\) x) D < 1" "\i. i\Basis \ i \ D \ x\i = 0" using x0 by auto qed } @@ -1554,63 +1471,62 @@ assume as: "x \ ?s" have "\i. 0 < x\i \ 0 = x\i \ 0 \ x\i" by auto - moreover have "\i. i \ d \ i \ d" by auto + moreover have "\i. i \ D \ i \ D" by auto ultimately - have "\i. (\i\d. 0 < x\i) \ (\i. i \ d \ x\i = 0) \ 0 \ x\i" + have "\i. (\i\D. 0 < x\i) \ (\i. i \ D \ x\i = 0) \ 0 \ x\i" by metis then have h2: "x \ convex hull (insert 0 ?p)" using as assms unfolding substd_simplex[OF assms] by fastforce - obtain a where a: "a \ d" - using \d \ {}\ by auto - let ?d = "(1 - sum ((\) x) d) / real (card d)" - have "0 < card d" using \d \ {}\ \finite d\ + obtain a where a: "a \ D" + using \D \ {}\ by auto + let ?d = "(1 - sum ((\) x) D) / real (card D)" + have "0 < card D" using \D \ {}\ \finite D\ by (simp add: card_gt_0_iff) - have "Min (((\) x) ` d) > 0" - using as \d \ {}\ \finite d\ by (simp add: Min_gr_iff) - moreover have "?d > 0" using as using \0 < card d\ by auto - ultimately have h3: "min (Min (((\) x) ` d)) ?d > 0" + have "Min (((\) x) ` D) > 0" + using as \D \ {}\ \finite D\ by (simp add: Min_gr_iff) + moreover have "?d > 0" using as using \0 < card D\ by auto + ultimately have h3: "min (Min (((\) x) ` D)) ?d > 0" by auto have "x \ rel_interior (convex hull (insert 0 ?p))" unfolding rel_interior_ball mem_Collect_eq h0 apply (rule,rule h2) unfolding substd_simplex[OF assms] - apply (rule_tac x="min (Min (((\) x) ` d)) ?d" in exI) + apply (rule_tac x="min (Min (((\) x) ` D)) ?d" in exI) apply (rule, rule h3) apply safe unfolding mem_ball proof - fix y :: 'a - assume y: "dist x y < min (Min ((\) x ` d)) ?d" - assume y2: "\i\Basis. i \ d \ y\i = 0" - have "sum ((\) y) d \ sum (\i. x\i + ?d) d" + assume y: "dist x y < min (Min ((\) x ` D)) ?d" + assume y2: "\i\Basis. i \ D \ y\i = 0" + have "sum ((\) y) D \ sum (\i. x\i + ?d) D" proof (rule sum_mono) fix i - assume "i \ d" - with d have i: "i \ Basis" + assume "i \ D" + with D have i: "i \ Basis" by auto - have "\y\i - x\i\ < ?d" - apply (rule le_less_trans) - using Basis_le_norm[OF i, of "y - x"] - using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] - apply (auto simp add: norm_minus_commute inner_simps) - done + have "\y\i - x\i\ \ norm (y - x)" + by (metis i inner_commute inner_diff_right norm_bound_Basis_le order_refl) + also have "... < ?d" + by (metis dist_norm min_less_iff_conj norm_minus_commute y) + finally have "\y\i - x\i\ < ?d" . then show "y \ i \ x \ i + ?d" by auto qed also have "\ \ 1" - unfolding sum.distrib sum_constant using \0 < card d\ + unfolding sum.distrib sum_constant using \0 < card D\ by auto - finally show "sum ((\) y) d \ 1" . + finally show "sum ((\) y) D \ 1" . fix i :: 'a assume i: "i \ Basis" then show "0 \ y\i" - proof (cases "i\d") + proof (cases "i\D") case True have "norm (x - y) < x\i" using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1] - using Min_gr_iff[of "(\) x ` d" "norm (x - y)"] \0 < card d\ \i \ d\ + using Min_gr_iff[of "(\) x ` D" "norm (x - y)"] \0 < card D\ \i \ D\ by (simp add: card_gt_0_iff) then show "0 \ y\i" using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format] @@ -1619,36 +1535,36 @@ qed } ultimately have - "\x. x \ rel_interior (convex hull insert 0 d) \ - x \ {x. (\i\d. 0 < x \ i) \ sum ((\) x) d < 1 \ (\i\Basis. i \ d \ x \ i = 0)}" + "\x. x \ rel_interior (convex hull insert 0 D) \ + x \ {x. (\i\D. 0 < x \ i) \ sum ((\) x) D < 1 \ (\i\Basis. i \ D \ x \ i = 0)}" by blast then show ?thesis by (rule set_eqI) qed qed lemma rel_interior_substd_simplex_nonempty: - assumes "d \ {}" - and "d \ Basis" + assumes "D \ {}" + and "D \ Basis" obtains a :: "'a::euclidean_space" - where "a \ rel_interior (convex hull (insert 0 d))" -proof - - let ?D = d - let ?a = "sum (\b::'a::euclidean_space. inverse (2 * real (card d)) *\<^sub>R b) ?D" - have "finite d" + where "a \ rel_interior (convex hull (insert 0 D))" +proof - + let ?D = D + let ?a = "sum (\b::'a::euclidean_space. inverse (2 * real (card D)) *\<^sub>R b) ?D" + have "finite D" apply (rule finite_subset) using assms(2) apply auto done - then have d1: "0 < real (card d)" - using \d \ {}\ by auto + then have d1: "0 < real (card D)" + using \D \ {}\ by auto { fix i - assume "i \ d" - have "?a \ i = inverse (2 * real (card d))" - apply (rule trans[of _ "sum (\j. if i = j then inverse (2 * real (card d)) else 0) ?D"]) + assume "i \ D" + have "?a \ i = inverse (2 * real (card D))" + apply (rule trans[of _ "sum (\j. if i = j then inverse (2 * real (card D)) else 0) ?D"]) unfolding inner_sum_left apply (rule sum.cong) - using \i \ d\ \finite d\ sum.delta'[of d i "(\k. inverse (2 * real (card d)))"] + using \i \ D\ \finite D\ sum.delta'[of D i "(\k. inverse (2 * real (card D)))"] d1 assms(2) by (auto simp: inner_Basis set_rev_mp[OF _ assms(2)]) } @@ -1658,14 +1574,14 @@ unfolding rel_interior_substd_simplex[OF assms(2)] mem_Collect_eq proof safe fix i - assume "i \ d" - have "0 < inverse (2 * real (card d))" + assume "i \ D" + have "0 < inverse (2 * real (card D))" using d1 by auto - also have "\ = ?a \ i" using **[of i] \i \ d\ + also have "\ = ?a \ i" using **[of i] \i \ D\ by auto finally show "0 < ?a \ i" by auto next - have "sum ((\) ?a) ?D = sum (\i. inverse (2 * real (card d))) ?D" + have "sum ((\) ?a) ?D = sum (\i. inverse (2 * real (card D))) ?D" by (rule sum.cong) (rule refl, rule **) also have "\ < 1" unfolding sum_constant divide_real_def[symmetric] @@ -1673,22 +1589,22 @@ finally show "sum ((\) ?a) ?D < 1" by auto next fix i - assume "i \ Basis" and "i \ d" - have "?a \ span d" - proof (rule span_sum[of d "(\b. b /\<^sub>R (2 * real (card d)))" d]) + assume "i \ Basis" and "i \ D" + have "?a \ span D" + proof (rule span_sum[of D "(\b. b /\<^sub>R (2 * real (card D)))" D]) { fix x :: "'a::euclidean_space" - assume "x \ d" - then have "x \ span d" - using span_superset[of _ "d"] by auto - then have "x /\<^sub>R (2 * real (card d)) \ span d" - using span_mul[of x "d" "(inverse (real (card d)) / 2)"] by auto + assume "x \ D" + then have "x \ span D" + using span_superset[of _ "D"] by auto + then have "x /\<^sub>R (2 * real (card D)) \ span D" + using span_mul[of x "D" "(inverse (real (card D)) / 2)"] by auto } - then show "\x. x\d \ x /\<^sub>R (2 * real (card d)) \ span d" + then show "\x. x\D \ x /\<^sub>R (2 * real (card D)) \ span D" by auto qed then show "?a \ i = 0 " - using \i \ d\ unfolding span_substd_basis[OF assms(2)] using \i \ Basis\ by auto + using \i \ D\ unfolding span_substd_basis[OF assms(2)] using \i \ Basis\ by auto qed qed @@ -1916,10 +1832,7 @@ proof - define e where "e = a / (a + b)" have "z = (1 / (a + b)) *\<^sub>R ((a + b) *\<^sub>R z)" - apply auto - using assms - apply simp - done + using assms by (simp add: eq_vector_fraction_iff) also have "\ = (1 / (a + b)) *\<^sub>R (a *\<^sub>R x + b *\<^sub>R y)" using assms scaleR_cancel_left[of "1/(a+b)" "(a + b) *\<^sub>R z" "a *\<^sub>R x + b *\<^sub>R y"] by auto @@ -2089,9 +2002,8 @@ lemma rel_frontier_eq_empty: fixes S :: "'n::euclidean_space set" shows "rel_frontier S = {} \ affine S" - apply (simp add: rel_frontier_def) - apply (simp add: rel_interior_eq_closure [symmetric]) - using rel_interior_subset_closure by blast + unfolding rel_frontier_def + using rel_interior_subset_closure by (auto simp add: rel_interior_eq_closure [symmetric]) lemma rel_frontier_sing [simp]: fixes a :: "'n::euclidean_space" @@ -2365,16 +2277,12 @@ shows "z \ interior S \ (\x. \e. e > 0 \ z + e *\<^sub>R x \ S)" proof (cases "aff_dim S = int DIM('n)") case False - { - assume "z \ interior S" + { assume "z \ interior S" then have False - using False interior_rel_interior_gen[of S] by auto - } + using False interior_rel_interior_gen[of S] by auto } moreover - { - assume r: "\x. \e. e > 0 \ z + e *\<^sub>R x \ S" - { - fix x + { assume r: "\x. \e. e > 0 \ z + e *\<^sub>R x \ S" + { fix x obtain e1 where e1: "e1 > 0 \ z + e1 *\<^sub>R (x - z) \ S" using r by auto obtain e2 where e2: "e2 > 0 \ z + e2 *\<^sub>R (z - x) \ S" @@ -3679,13 +3587,7 @@ then have "x = (\i\I. c i *\<^sub>R s i) \ sum c I = 1" using k by (simp add: sum_prod) then have "x \ ?rhs" - using k - apply auto - apply (rule_tac x = c in exI) - apply (rule_tac x = s in exI) - using cs - apply auto - done + using k cs by auto } moreover { @@ -3709,7 +3611,7 @@ done then have "x \ ?lhs" using K0_def C0_def rel_interior_convex_cone_aux[of C0 1 x] - by (auto simp add: convex_convex_hull) + by auto } ultimately show ?thesis by blast qed @@ -5105,10 +5007,7 @@ "S \ S'" "T \ T'" "S' \ T' = {}" proof (cases "S = {} \ T = {}") case True with that show ?thesis - apply safe - using UT closedin_subset apply blast - using US closedin_subset apply blast - done + using UT US by (blast dest: closedin_subset) next case False define f where "f \ \x. setdist {x} T - setdist {x} S" diff -r b249fab48c76 -r d2daeef3ce47 src/HOL/Library/Adhoc_Overloading.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Adhoc_Overloading.thy Wed May 02 12:48:08 2018 +0100 @@ -0,0 +1,15 @@ +(* Title: HOL/Library/Adhoc_Overloading.thy + Author: Alexander Krauss, TU Muenchen + Author: Christian Sternagel, University of Innsbruck +*) + +section \Adhoc overloading of constants based on their types\ + +theory Adhoc_Overloading + imports Main + keywords "adhoc_overloading" "no_adhoc_overloading" :: thy_decl +begin + +ML_file "adhoc_overloading.ML" + +end diff -r b249fab48c76 -r d2daeef3ce47 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Wed May 02 12:47:56 2018 +0100 +++ b/src/HOL/Library/Library.thy Wed May 02 12:48:08 2018 +0100 @@ -2,6 +2,7 @@ theory Library imports AList + Adhoc_Overloading BigO Bit BNF_Axiomatization diff -r b249fab48c76 -r d2daeef3ce47 src/HOL/Library/Monad_Syntax.thy --- a/src/HOL/Library/Monad_Syntax.thy Wed May 02 12:47:56 2018 +0100 +++ b/src/HOL/Library/Monad_Syntax.thy Wed May 02 12:48:08 2018 +0100 @@ -1,11 +1,12 @@ -(* Author: Alexander Krauss, TU Muenchen - Author: Christian Sternagel, University of Innsbruck +(* Title: HOL/Library/Monad_Syntax.thy + Author: Alexander Krauss, TU Muenchen + Author: Christian Sternagel, University of Innsbruck *) section \Monad notation for arbitrary types\ theory Monad_Syntax -imports Main "~~/src/Tools/Adhoc_Overloading" + imports Adhoc_Overloading begin text \ diff -r b249fab48c76 -r d2daeef3ce47 src/HOL/Library/adhoc_overloading.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/adhoc_overloading.ML Wed May 02 12:48:08 2018 +0100 @@ -0,0 +1,246 @@ +(* Author: Alexander Krauss, TU Muenchen + Author: Christian Sternagel, University of Innsbruck + +Adhoc overloading of constants based on their types. +*) + +signature ADHOC_OVERLOADING = +sig + val is_overloaded: Proof.context -> string -> bool + val generic_add_overloaded: string -> Context.generic -> Context.generic + val generic_remove_overloaded: string -> Context.generic -> Context.generic + val generic_add_variant: string -> term -> Context.generic -> Context.generic + (*If the list of variants is empty at the end of "generic_remove_variant", then + "generic_remove_overloaded" is called implicitly.*) + val generic_remove_variant: string -> term -> Context.generic -> Context.generic + val show_variants: bool Config.T +end + +structure Adhoc_Overloading: ADHOC_OVERLOADING = +struct + +val show_variants = Attrib.setup_config_bool @{binding show_variants} (K false); + + +(* errors *) + +fun err_duplicate_variant oconst = + error ("Duplicate variant of " ^ quote oconst); + +fun err_not_a_variant oconst = + error ("Not a variant of " ^ quote oconst); + +fun err_not_overloaded oconst = + error ("Constant " ^ quote oconst ^ " is not declared as overloaded"); + +fun err_unresolved_overloading ctxt0 (c, T) t instances = + let + val ctxt = Config.put show_variants true ctxt0 + val const_space = Proof_Context.const_space ctxt + val prt_const = + Pretty.block [Name_Space.pretty ctxt const_space c, Pretty.str " ::", Pretty.brk 1, + Pretty.quote (Syntax.pretty_typ ctxt T)] + in + error (Pretty.string_of (Pretty.chunks [ + Pretty.block [ + Pretty.str "Unresolved adhoc overloading of constant", Pretty.brk 1, + prt_const, Pretty.brk 1, Pretty.str "in term", Pretty.brk 1, + Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t)]], + Pretty.block ( + (if null instances then [Pretty.str "no instances"] + else Pretty.fbreaks ( + Pretty.str "multiple instances:" :: + map (Pretty.mark Markup.item o Syntax.pretty_term ctxt) instances)))])) + end; + + +(* generic data *) + +fun variants_eq ((v1, T1), (v2, T2)) = + Term.aconv_untyped (v1, v2) andalso T1 = T2; + +structure Overload_Data = Generic_Data +( + type T = + {variants : (term * typ) list Symtab.table, + oconsts : string Termtab.table}; + val empty = {variants = Symtab.empty, oconsts = Termtab.empty}; + val extend = I; + + fun merge + ({variants = vtab1, oconsts = otab1}, + {variants = vtab2, oconsts = otab2}) : T = + let + fun merge_oconsts _ (oconst1, oconst2) = + if oconst1 = oconst2 then oconst1 + else err_duplicate_variant oconst1; + in + {variants = Symtab.merge_list variants_eq (vtab1, vtab2), + oconsts = Termtab.join merge_oconsts (otab1, otab2)} + end; +); + +fun map_tables f g = + Overload_Data.map (fn {variants = vtab, oconsts = otab} => + {variants = f vtab, oconsts = g otab}); + +val is_overloaded = Symtab.defined o #variants o Overload_Data.get o Context.Proof; +val get_variants = Symtab.lookup o #variants o Overload_Data.get o Context.Proof; +val get_overloaded = Termtab.lookup o #oconsts o Overload_Data.get o Context.Proof; + +fun generic_add_overloaded oconst context = + if is_overloaded (Context.proof_of context) oconst then context + else map_tables (Symtab.update (oconst, [])) I context; + +fun generic_remove_overloaded oconst context = + let + fun remove_oconst_and_variants context oconst = + let + val remove_variants = + (case get_variants (Context.proof_of context) oconst of + NONE => I + | SOME vs => fold (Termtab.remove (op =) o rpair oconst o fst) vs); + in map_tables (Symtab.delete_safe oconst) remove_variants context end; + in + if is_overloaded (Context.proof_of context) oconst then remove_oconst_and_variants context oconst + else err_not_overloaded oconst + end; + +local + fun generic_variant add oconst t context = + let + val ctxt = Context.proof_of context; + val _ = if is_overloaded ctxt oconst then () else err_not_overloaded oconst; + val T = t |> fastype_of; + val t' = Term.map_types (K dummyT) t; + in + if add then + let + val _ = + (case get_overloaded ctxt t' of + NONE => () + | SOME oconst' => err_duplicate_variant oconst'); + in + map_tables (Symtab.cons_list (oconst, (t', T))) (Termtab.update (t', oconst)) context + end + else + let + val _ = + if member variants_eq (the (get_variants ctxt oconst)) (t', T) then () + else err_not_a_variant oconst; + in + map_tables (Symtab.map_entry oconst (remove1 variants_eq (t', T))) + (Termtab.delete_safe t') context + |> (fn context => + (case get_variants (Context.proof_of context) oconst of + SOME [] => generic_remove_overloaded oconst context + | _ => context)) + end + end; +in + val generic_add_variant = generic_variant true; + val generic_remove_variant = generic_variant false; +end; + + +(* check / uncheck *) + +fun unifiable_with thy T1 T2 = + let + val maxidx1 = Term.maxidx_of_typ T1; + val T2' = Logic.incr_tvar (maxidx1 + 1) T2; + val maxidx2 = Term.maxidx_typ T2' maxidx1; + in can (Sign.typ_unify thy (T1, T2')) (Vartab.empty, maxidx2) end; + +fun get_candidates ctxt (c, T) = + get_variants ctxt c + |> Option.map (map_filter (fn (t, T') => + if unifiable_with (Proof_Context.theory_of ctxt) T T' then SOME t + else NONE)); + +fun insert_variants ctxt t (oconst as Const (c, T)) = + (case get_candidates ctxt (c, T) of + SOME [] => err_unresolved_overloading ctxt (c, T) t [] + | SOME [variant] => variant + | _ => oconst) + | insert_variants _ _ oconst = oconst; + +fun insert_overloaded ctxt = + let + fun proc t = + Term.map_types (K dummyT) t + |> get_overloaded ctxt + |> Option.map (Const o rpair (Term.type_of t)); + in + Pattern.rewrite_term_top (Proof_Context.theory_of ctxt) [] [proc] + end; + +fun check ctxt = + map (fn t => Term.map_aterms (insert_variants ctxt t) t); + +fun uncheck ctxt ts = + if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of) ts then ts + else map (insert_overloaded ctxt) ts; + +fun reject_unresolved ctxt = + let + val the_candidates = the o get_candidates ctxt; + fun check_unresolved t = + (case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of + [] => t + | (cT :: _) => err_unresolved_overloading ctxt cT t (the_candidates cT)); + in map check_unresolved end; + + +(* setup *) + +val _ = Context.>> + (Syntax_Phases.term_check 0 "adhoc_overloading" check + #> Syntax_Phases.term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved + #> Syntax_Phases.term_uncheck 0 "adhoc_overloading" uncheck); + + +(* commands *) + +fun generic_adhoc_overloading_cmd add = + if add then + fold (fn (oconst, ts) => + generic_add_overloaded oconst + #> fold (generic_add_variant oconst) ts) + else + fold (fn (oconst, ts) => + fold (generic_remove_variant oconst) ts); + +fun adhoc_overloading_cmd' add args phi = + let val args' = args + |> map (apsnd (map_filter (fn t => + let val t' = Morphism.term phi t; + in if Term.aconv_untyped (t, t') then SOME t' else NONE end))); + in generic_adhoc_overloading_cmd add args' end; + +fun adhoc_overloading_cmd add raw_args lthy = + let + fun const_name ctxt = + fst o dest_Const o Proof_Context.read_const {proper = false, strict = false} ctxt; (* FIXME {proper = true, strict = true} (!?) *) + fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt; + val args = + raw_args + |> map (apfst (const_name lthy)) + |> map (apsnd (map (read_term lthy))); + in + Local_Theory.declaration {syntax = true, pervasive = false} + (adhoc_overloading_cmd' add args) lthy + end; + +val _ = + Outer_Syntax.local_theory @{command_keyword adhoc_overloading} + "add adhoc overloading for constants / fixed variables" + (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd true); + +val _ = + Outer_Syntax.local_theory @{command_keyword no_adhoc_overloading} + "delete adhoc overloading for constants / fixed variables" + (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd false); + +end; + diff -r b249fab48c76 -r d2daeef3ce47 src/HOL/Tools/SMT/z3_proof.ML --- a/src/HOL/Tools/SMT/z3_proof.ML Wed May 02 12:47:56 2018 +0100 +++ b/src/HOL/Tools/SMT/z3_proof.ML Wed May 02 12:48:08 2018 +0100 @@ -216,9 +216,15 @@ let val match = Sign.typ_match (Proof_Context.theory_of ctxt) + fun objT_of bound = + (case Symtab.lookup env bound of + SOME objT => objT + | NONE => raise Fail ("Replaying the proof trace produced by Z3 failed: " ^ + "the bound " ^ quote bound ^ " is undeclared; this indicates a bug in Z3")) + val t' = singleton (Variable.polymorphic ctxt) t val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t') - val objTs = map (the o Symtab.lookup env) bounds + val objTs = map objT_of bounds val subst = subst_of (fold match (patTs ~~ objTs) Vartab.empty) in Same.commit (Term_Subst.map_types_same (substTs_same subst)) t' end diff -r b249fab48c76 -r d2daeef3ce47 src/Tools/Adhoc_Overloading.thy --- a/src/Tools/Adhoc_Overloading.thy Wed May 02 12:47:56 2018 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,16 +0,0 @@ -(* Author: Alexander Krauss, TU Muenchen - Author: Christian Sternagel, University of Innsbruck -*) - -section \Adhoc overloading of constants based on their types\ - -theory Adhoc_Overloading -imports Pure -keywords - "adhoc_overloading" "no_adhoc_overloading" :: thy_decl -begin - -ML_file "adhoc_overloading.ML" - -end - diff -r b249fab48c76 -r d2daeef3ce47 src/Tools/adhoc_overloading.ML --- a/src/Tools/adhoc_overloading.ML Wed May 02 12:47:56 2018 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,246 +0,0 @@ -(* Author: Alexander Krauss, TU Muenchen - Author: Christian Sternagel, University of Innsbruck - -Adhoc overloading of constants based on their types. -*) - -signature ADHOC_OVERLOADING = -sig - val is_overloaded: Proof.context -> string -> bool - val generic_add_overloaded: string -> Context.generic -> Context.generic - val generic_remove_overloaded: string -> Context.generic -> Context.generic - val generic_add_variant: string -> term -> Context.generic -> Context.generic - (*If the list of variants is empty at the end of "generic_remove_variant", then - "generic_remove_overloaded" is called implicitly.*) - val generic_remove_variant: string -> term -> Context.generic -> Context.generic - val show_variants: bool Config.T -end - -structure Adhoc_Overloading: ADHOC_OVERLOADING = -struct - -val show_variants = Attrib.setup_config_bool @{binding show_variants} (K false); - - -(* errors *) - -fun err_duplicate_variant oconst = - error ("Duplicate variant of " ^ quote oconst); - -fun err_not_a_variant oconst = - error ("Not a variant of " ^ quote oconst); - -fun err_not_overloaded oconst = - error ("Constant " ^ quote oconst ^ " is not declared as overloaded"); - -fun err_unresolved_overloading ctxt0 (c, T) t instances = - let - val ctxt = Config.put show_variants true ctxt0 - val const_space = Proof_Context.const_space ctxt - val prt_const = - Pretty.block [Name_Space.pretty ctxt const_space c, Pretty.str " ::", Pretty.brk 1, - Pretty.quote (Syntax.pretty_typ ctxt T)] - in - error (Pretty.string_of (Pretty.chunks [ - Pretty.block [ - Pretty.str "Unresolved adhoc overloading of constant", Pretty.brk 1, - prt_const, Pretty.brk 1, Pretty.str "in term", Pretty.brk 1, - Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t)]], - Pretty.block ( - (if null instances then [Pretty.str "no instances"] - else Pretty.fbreaks ( - Pretty.str "multiple instances:" :: - map (Pretty.mark Markup.item o Syntax.pretty_term ctxt) instances)))])) - end; - - -(* generic data *) - -fun variants_eq ((v1, T1), (v2, T2)) = - Term.aconv_untyped (v1, v2) andalso T1 = T2; - -structure Overload_Data = Generic_Data -( - type T = - {variants : (term * typ) list Symtab.table, - oconsts : string Termtab.table}; - val empty = {variants = Symtab.empty, oconsts = Termtab.empty}; - val extend = I; - - fun merge - ({variants = vtab1, oconsts = otab1}, - {variants = vtab2, oconsts = otab2}) : T = - let - fun merge_oconsts _ (oconst1, oconst2) = - if oconst1 = oconst2 then oconst1 - else err_duplicate_variant oconst1; - in - {variants = Symtab.merge_list variants_eq (vtab1, vtab2), - oconsts = Termtab.join merge_oconsts (otab1, otab2)} - end; -); - -fun map_tables f g = - Overload_Data.map (fn {variants = vtab, oconsts = otab} => - {variants = f vtab, oconsts = g otab}); - -val is_overloaded = Symtab.defined o #variants o Overload_Data.get o Context.Proof; -val get_variants = Symtab.lookup o #variants o Overload_Data.get o Context.Proof; -val get_overloaded = Termtab.lookup o #oconsts o Overload_Data.get o Context.Proof; - -fun generic_add_overloaded oconst context = - if is_overloaded (Context.proof_of context) oconst then context - else map_tables (Symtab.update (oconst, [])) I context; - -fun generic_remove_overloaded oconst context = - let - fun remove_oconst_and_variants context oconst = - let - val remove_variants = - (case get_variants (Context.proof_of context) oconst of - NONE => I - | SOME vs => fold (Termtab.remove (op =) o rpair oconst o fst) vs); - in map_tables (Symtab.delete_safe oconst) remove_variants context end; - in - if is_overloaded (Context.proof_of context) oconst then remove_oconst_and_variants context oconst - else err_not_overloaded oconst - end; - -local - fun generic_variant add oconst t context = - let - val ctxt = Context.proof_of context; - val _ = if is_overloaded ctxt oconst then () else err_not_overloaded oconst; - val T = t |> fastype_of; - val t' = Term.map_types (K dummyT) t; - in - if add then - let - val _ = - (case get_overloaded ctxt t' of - NONE => () - | SOME oconst' => err_duplicate_variant oconst'); - in - map_tables (Symtab.cons_list (oconst, (t', T))) (Termtab.update (t', oconst)) context - end - else - let - val _ = - if member variants_eq (the (get_variants ctxt oconst)) (t', T) then () - else err_not_a_variant oconst; - in - map_tables (Symtab.map_entry oconst (remove1 variants_eq (t', T))) - (Termtab.delete_safe t') context - |> (fn context => - (case get_variants (Context.proof_of context) oconst of - SOME [] => generic_remove_overloaded oconst context - | _ => context)) - end - end; -in - val generic_add_variant = generic_variant true; - val generic_remove_variant = generic_variant false; -end; - - -(* check / uncheck *) - -fun unifiable_with thy T1 T2 = - let - val maxidx1 = Term.maxidx_of_typ T1; - val T2' = Logic.incr_tvar (maxidx1 + 1) T2; - val maxidx2 = Term.maxidx_typ T2' maxidx1; - in can (Sign.typ_unify thy (T1, T2')) (Vartab.empty, maxidx2) end; - -fun get_candidates ctxt (c, T) = - get_variants ctxt c - |> Option.map (map_filter (fn (t, T') => - if unifiable_with (Proof_Context.theory_of ctxt) T T' then SOME t - else NONE)); - -fun insert_variants ctxt t (oconst as Const (c, T)) = - (case get_candidates ctxt (c, T) of - SOME [] => err_unresolved_overloading ctxt (c, T) t [] - | SOME [variant] => variant - | _ => oconst) - | insert_variants _ _ oconst = oconst; - -fun insert_overloaded ctxt = - let - fun proc t = - Term.map_types (K dummyT) t - |> get_overloaded ctxt - |> Option.map (Const o rpair (Term.type_of t)); - in - Pattern.rewrite_term_top (Proof_Context.theory_of ctxt) [] [proc] - end; - -fun check ctxt = - map (fn t => Term.map_aterms (insert_variants ctxt t) t); - -fun uncheck ctxt ts = - if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of) ts then ts - else map (insert_overloaded ctxt) ts; - -fun reject_unresolved ctxt = - let - val the_candidates = the o get_candidates ctxt; - fun check_unresolved t = - (case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of - [] => t - | (cT :: _) => err_unresolved_overloading ctxt cT t (the_candidates cT)); - in map check_unresolved end; - - -(* setup *) - -val _ = Context.>> - (Syntax_Phases.term_check 0 "adhoc_overloading" check - #> Syntax_Phases.term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved - #> Syntax_Phases.term_uncheck 0 "adhoc_overloading" uncheck); - - -(* commands *) - -fun generic_adhoc_overloading_cmd add = - if add then - fold (fn (oconst, ts) => - generic_add_overloaded oconst - #> fold (generic_add_variant oconst) ts) - else - fold (fn (oconst, ts) => - fold (generic_remove_variant oconst) ts); - -fun adhoc_overloading_cmd' add args phi = - let val args' = args - |> map (apsnd (map_filter (fn t => - let val t' = Morphism.term phi t; - in if Term.aconv_untyped (t, t') then SOME t' else NONE end))); - in generic_adhoc_overloading_cmd add args' end; - -fun adhoc_overloading_cmd add raw_args lthy = - let - fun const_name ctxt = - fst o dest_Const o Proof_Context.read_const {proper = false, strict = false} ctxt; (* FIXME {proper = true, strict = true} (!?) *) - fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt; - val args = - raw_args - |> map (apfst (const_name lthy)) - |> map (apsnd (map (read_term lthy))); - in - Local_Theory.declaration {syntax = true, pervasive = false} - (adhoc_overloading_cmd' add args) lthy - end; - -val _ = - Outer_Syntax.local_theory @{command_keyword adhoc_overloading} - "add adhoc overloading for constants / fixed variables" - (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd true); - -val _ = - Outer_Syntax.local_theory @{command_keyword no_adhoc_overloading} - "delete adhoc overloading for constants / fixed variables" - (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd false); - -end; - diff -r b249fab48c76 -r d2daeef3ce47 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Wed May 02 12:47:56 2018 +0100 +++ b/src/Tools/jEdit/src/jedit_lib.scala Wed May 02 12:48:08 2018 +0100 @@ -129,6 +129,13 @@ def buffer_file(buffer: Buffer): Option[JFile] = check_file(buffer_name(buffer)) + def buffer_undo_in_progress[A](buffer: JEditBuffer, body: => A): A = + { + val undo_in_progress = buffer.isUndoInProgress + def set(b: Boolean) { Untyped.set[Boolean](buffer, "undoInProgress", b) } + try { set(true); body } finally { set(undo_in_progress) } + } + /* main jEdit components */ diff -r b249fab48c76 -r d2daeef3ce47 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Wed May 02 12:47:56 2018 +0100 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Wed May 02 12:48:08 2018 +0100 @@ -144,7 +144,7 @@ JEdit_Lib.buffer_edit(getBuffer) { rich_text_area.active_reset() getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering)) - setText(text) + JEdit_Lib.buffer_undo_in_progress(getBuffer, setText(text)) setCaretPosition(0) } }