# HG changeset patch # User haftmann # Date 1314428545 -7200 # Node ID 9ab8c88449a4c7b932f645b07d1db9969d536e15 # Parent ddfd934e19bbab5f892e054fe303aaca5cec0301# Parent c0fd385a41f40af2d6911440bc82f7020c693332 adapted to changes in Cset.thy diff -r c0fd385a41f4 -r 9ab8c88449a4 NEWS --- a/NEWS Fri Aug 26 23:02:00 2011 +0200 +++ b/NEWS Sat Aug 27 09:02:25 2011 +0200 @@ -200,6 +200,39 @@ tendsto_vector ~> vec_tendstoI Cauchy_vector ~> vec_CauchyI +* Session Multivariate_Analysis: Several duplicate theorems have been +removed, and other theorems have been renamed. INCOMPATIBILITY. + + eventually_conjI ~> eventually_conj + eventually_and ~> eventually_conj_iff + eventually_false ~> eventually_False + setsum_norm ~> norm_setsum + Lim_ident_at ~> LIM_ident + Lim_const ~> tendsto_const + Lim_cmul ~> tendsto_scaleR [OF tendsto_const] + Lim_neg ~> tendsto_minus + Lim_add ~> tendsto_add + Lim_sub ~> tendsto_diff + Lim_mul ~> tendsto_scaleR + Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const] + Lim_null_norm ~> tendsto_norm_zero_iff [symmetric] + Lim_linear ~> bounded_linear.tendsto + Lim_component ~> tendsto_euclidean_component + Lim_component_cart ~> tendsto_vec_nth + Lim_inner ~> tendsto_inner [OF tendsto_const] + dot_lsum ~> inner_setsum_left + dot_rsum ~> inner_setsum_right + continuous_on_neg ~> continuous_on_minus + continuous_on_sub ~> continuous_on_diff + continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const] + continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const] + continuous_on_mul ~> continuous_on_scaleR + continuous_on_mul_real ~> continuous_on_mult + continuous_on_inner ~> continuous_on_inner [OF continuous_on_const] + subset_interior ~> interior_mono + subset_closure ~> closure_mono + closure_univ ~> closure_UNIV + * Complex_Main: The locale interpretations for the bounded_linear and bounded_bilinear locales have been removed, in order to reduce the number of duplicate lemmas. Users must use the original names for @@ -213,6 +246,16 @@ mult_right.setsum ~> setsum_right_distrib mult_left.diff ~> left_diff_distrib +* Complex_Main: Several redundant theorems about real numbers have +been removed or generalized and renamed. INCOMPATIBILITY. + + real_0_le_divide_iff ~> zero_le_divide_iff + realpow_two_disj ~> power2_eq_iff + real_squared_diff_one_factored ~> square_diff_one_factored + realpow_two_diff ~> square_diff_square_factored + exp_ln_eq ~> ln_unique + lemma_DERIV_subst ~> DERIV_cong + *** Document preparation *** diff -r c0fd385a41f4 -r 9ab8c88449a4 src/HOL/Algebra/Congruence.thy --- a/src/HOL/Algebra/Congruence.thy Fri Aug 26 23:02:00 2011 +0200 +++ b/src/HOL/Algebra/Congruence.thy Sat Aug 27 09:02:25 2011 +0200 @@ -29,15 +29,15 @@ where "A {.=}\<^bsub>S\<^esub> B \ ((\x \ A. x .\\<^bsub>S\<^esub> B) \ (\x \ B. x .\\<^bsub>S\<^esub> A))" definition - eq_class_of :: "_ \ 'a \ 'a set" ("class'_of\ _") + eq_class_of :: "_ \ 'a \ 'a set" ("class'_of\") where "class_of\<^bsub>S\<^esub> x = {y \ carrier S. x .=\<^bsub>S\<^esub> y}" definition - eq_closure_of :: "_ \ 'a set \ 'a set" ("closure'_of\ _") + eq_closure_of :: "_ \ 'a set \ 'a set" ("closure'_of\") where "closure_of\<^bsub>S\<^esub> A = {y \ carrier S. y .\\<^bsub>S\<^esub> A}" definition - eq_is_closed :: "_ \ 'a set \ bool" ("is'_closed\ _") + eq_is_closed :: "_ \ 'a set \ bool" ("is'_closed\") where "is_closed\<^bsub>S\<^esub> A \ A \ carrier S \ closure_of\<^bsub>S\<^esub> A = A" abbreviation diff -r c0fd385a41f4 -r 9ab8c88449a4 src/HOL/Algebra/Group.thy --- a/src/HOL/Algebra/Group.thy Fri Aug 26 23:02:00 2011 +0200 +++ b/src/HOL/Algebra/Group.thy Sat Aug 27 09:02:25 2011 +0200 @@ -154,7 +154,7 @@ and G: "x \ Units G" "y \ carrier G" "z \ carrier G" then have "(inv x \ x) \ y = (inv x \ x) \ z" by (simp add: m_assoc Units_closed del: Units_l_inv) - with G show "y = z" by (simp add: Units_l_inv) + with G show "y = z" by simp next assume eq: "y = z" and G: "x \ Units G" "y \ carrier G" "z \ carrier G" @@ -332,7 +332,7 @@ proof - assume x: "x \ carrier G" then have "inv x \ (x \ inv x) = inv x \ \" - by (simp add: m_assoc [symmetric] l_inv) + by (simp add: m_assoc [symmetric]) with x show ?thesis by (simp del: r_one) qed @@ -372,7 +372,7 @@ proof - assume G: "x \ carrier G" "y \ carrier G" then have "inv (x \ y) \ (x \ y) = (inv y \ inv x) \ (x \ y)" - by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric]) + by (simp add: m_assoc) (simp add: m_assoc [symmetric]) with G show ?thesis by (simp del: l_inv Units_l_inv) qed @@ -446,7 +446,7 @@ lemma (in group) one_in_subset: "[| H \ carrier G; H \ {}; \a \ H. inv a \ H; \a\H. \b\H. a \ b \ H |] ==> \ \ H" -by (force simp add: l_inv) +by force text {* A characterization of subgroups: closed, non-empty subset. *} diff -r c0fd385a41f4 -r 9ab8c88449a4 src/HOL/Algebra/Lattice.thy --- a/src/HOL/Algebra/Lattice.thy Fri Aug 26 23:02:00 2011 +0200 +++ b/src/HOL/Algebra/Lattice.thy Sat Aug 27 09:02:25 2011 +0200 @@ -34,7 +34,8 @@ subsubsection {* The order relation *} -context weak_partial_order begin +context weak_partial_order +begin lemma le_cong_l [intro, trans]: "\ x .= y; y \ z; x \ carrier L; y \ carrier L; z \ carrier L \ \ x \ z" @@ -85,7 +86,7 @@ and yy': "y .= y'" and carr: "x \ carrier L" "y \ carrier L" "y' \ carrier L" shows "x \ y'" - using assms unfolding lless_def by (auto intro: trans sym) + using assms unfolding lless_def by (auto intro: trans sym) (*slow*) lemma (in weak_partial_order) lless_antisym: @@ -574,8 +575,7 @@ proof (cases "A = {}") case True with insert show ?thesis - by simp (simp add: least_cong [OF weak_sup_of_singleton] - sup_of_singleton_closed sup_of_singletonI) + by simp (simp add: least_cong [OF weak_sup_of_singleton] sup_of_singletonI) (* The above step is hairy; least_cong can make simp loop. Would want special version of simp to apply least_cong. *) next @@ -1282,7 +1282,7 @@ (is "complete_lattice ?L") proof (rule partial_order.complete_latticeI) show "partial_order ?L" - proof qed auto + by default auto next fix B assume B: "B \ carrier ?L" diff -r c0fd385a41f4 -r 9ab8c88449a4 src/HOL/Hoare_Parallel/OG_Hoare.thy --- a/src/HOL/Hoare_Parallel/OG_Hoare.thy Fri Aug 26 23:02:00 2011 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy Sat Aug 27 09:02:25 2011 +0200 @@ -436,10 +436,10 @@ apply(rule TrueI)+ --{* Parallel *} apply(simp add: SEM_def sem_def) - apply clarify + apply(clarify, rename_tac x y i Ts') apply(frule Parallel_length_post_PStar) apply clarify - apply(drule_tac j=xb in Parallel_Strong_Soundness) + apply(drule_tac j=i in Parallel_Strong_Soundness) apply clarify apply simp apply force diff -r c0fd385a41f4 -r 9ab8c88449a4 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Aug 26 23:02:00 2011 +0200 +++ b/src/HOL/IsaMakefile Sat Aug 27 09:02:25 2011 +0200 @@ -1175,6 +1175,7 @@ Multivariate_Analysis/L2_Norm.thy \ Multivariate_Analysis/Linear_Algebra.thy \ Multivariate_Analysis/Multivariate_Analysis.thy \ + Multivariate_Analysis/Norm_Arith.thy \ Multivariate_Analysis/Operator_Norm.thy \ Multivariate_Analysis/Path_Connected.thy \ Multivariate_Analysis/ROOT.ML \ diff -r c0fd385a41f4 -r 9ab8c88449a4 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Fri Aug 26 23:02:00 2011 +0200 +++ b/src/HOL/Library/Extended_Real.thy Sat Aug 27 09:02:25 2011 +0200 @@ -2391,8 +2391,6 @@ shows "limsup X \ limsup Y" using Limsup_mono[of X Y sequentially] eventually_sequentially assms by auto -declare trivial_limit_sequentially[simp] - lemma fixes X :: "nat \ ereal" shows ereal_incseq_uminus[simp]: "incseq (\i. - X i) = decseq X" diff -r c0fd385a41f4 -r 9ab8c88449a4 src/HOL/Lim.thy --- a/src/HOL/Lim.thy Fri Aug 26 23:02:00 2011 +0200 +++ b/src/HOL/Lim.thy Sat Aug 27 09:02:25 2011 +0200 @@ -444,46 +444,51 @@ subsection {* Relation of LIM and LIMSEQ *} +lemma sequentially_imp_eventually_within: + fixes a :: "'a::metric_space" + assumes "\f. (\n. f n \ s \ f n \ a) \ f ----> a \ + eventually (\n. P (f n)) sequentially" + shows "eventually P (at a within s)" +proof (rule ccontr) + let ?I = "\n. inverse (real (Suc n))" + def F \ "\n::nat. SOME x. x \ s \ x \ a \ dist x a < ?I n \ \ P x" + assume "\ eventually P (at a within s)" + hence P: "\d>0. \x. x \ s \ x \ a \ dist x a < d \ \ P x" + unfolding Limits.eventually_within Limits.eventually_at by fast + hence "\n. \x. x \ s \ x \ a \ dist x a < ?I n \ \ P x" by simp + hence F: "\n. F n \ s \ F n \ a \ dist (F n) a < ?I n \ \ P (F n)" + unfolding F_def by (rule someI_ex) + hence F0: "\n. F n \ s" and F1: "\n. F n \ a" + and F2: "\n. dist (F n) a < ?I n" and F3: "\n. \ P (F n)" + by fast+ + from LIMSEQ_inverse_real_of_nat have "F ----> a" + by (rule metric_tendsto_imp_tendsto, + simp add: dist_norm F2 less_imp_le) + hence "eventually (\n. P (F n)) sequentially" + using assms F0 F1 by simp + thus "False" by (simp add: F3) +qed + +lemma sequentially_imp_eventually_at: + fixes a :: "'a::metric_space" + assumes "\f. (\n. f n \ a) \ f ----> a \ + eventually (\n. P (f n)) sequentially" + shows "eventually P (at a)" + using assms sequentially_imp_eventually_within [where s=UNIV] + unfolding within_UNIV by simp + lemma LIMSEQ_SEQ_conv1: fixes f :: "'a::topological_space \ 'b::topological_space" assumes f: "f -- a --> l" shows "\S. (\n. S n \ a) \ S ----> a \ (\n. f (S n)) ----> l" using tendsto_compose_eventually [OF f, where F=sequentially] by simp -lemma LIMSEQ_SEQ_conv2_lemma: - fixes a :: "'a::metric_space" - assumes "\S. (\n. S n \ a) \ S ----> a \ eventually (\x. P (S x)) sequentially" - shows "eventually P (at a)" -proof (rule ccontr) - let ?I = "\n. inverse (real (Suc n))" - let ?F = "\n::nat. SOME x. x \ a \ dist x a < ?I n \ \ P x" - assume "\ eventually P (at a)" - hence P: "\d>0. \x. x \ a \ dist x a < d \ \ P x" - unfolding eventually_at by simp - hence "\n. \x. x \ a \ dist x a < ?I n \ \ P x" by simp - hence F: "\n. ?F n \ a \ dist (?F n) a < ?I n \ \ P (?F n)" - by (rule someI_ex) - hence F1: "\n. ?F n \ a" - and F2: "\n. dist (?F n) a < ?I n" - and F3: "\n. \ P (?F n)" - by fast+ - have "?F ----> a" - using LIMSEQ_inverse_real_of_nat - by (rule metric_tendsto_imp_tendsto, - simp add: dist_norm F2 [THEN less_imp_le]) - moreover have "\n. ?F n \ a" - by (rule allI) (rule F1) - ultimately have "eventually (\n. P (?F n)) sequentially" - using assms by simp - thus "False" by (simp add: F3) -qed - lemma LIMSEQ_SEQ_conv2: fixes f :: "'a::metric_space \ 'b::topological_space" assumes "\S. (\n. S n \ a) \ S ----> a \ (\n. f (S n)) ----> l" shows "f -- a --> l" using assms unfolding tendsto_def [where l=l] - by (simp add: LIMSEQ_SEQ_conv2_lemma) + by (simp add: sequentially_imp_eventually_at) lemma LIMSEQ_SEQ_conv: "(\S. (\n. S n \ a) \ S ----> (a::'a::metric_space) \ (\n. X (S n)) ----> L) = diff -r c0fd385a41f4 -r 9ab8c88449a4 src/HOL/List.thy --- a/src/HOL/List.thy Fri Aug 26 23:02:00 2011 +0200 +++ b/src/HOL/List.thy Sat Aug 27 09:02:25 2011 +0200 @@ -4703,7 +4703,7 @@ qed -text{* Accessible part of @{term listrel1} relations: *} +text{* Accessible part and wellfoundedness: *} lemma Cons_acc_listrel1I [intro!]: "x \ acc r \ xs \ acc (listrel1 r) \ (x # xs) \ acc (listrel1 r)" @@ -4729,6 +4729,9 @@ apply (fastsimp dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def) done +lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r" +by(metis wf_acc_iff in_lists_conv_set lists_accI lists_accD Cons_in_lists_iff) + subsubsection {* Lifting Relations to Lists: all elements *} diff -r c0fd385a41f4 -r 9ab8c88449a4 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 26 23:02:00 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sat Aug 27 09:02:25 2011 +0200 @@ -792,7 +792,7 @@ have "subspace ?P" by (auto simp add: subspace_def) ultimately show ?thesis - using x span_induct[of ?B ?P x] iS by blast + using x span_induct[of x ?B ?P] iS by blast qed lemma independent_stdbasis: "independent {cart_basis i ::real^'n |i. i\ (UNIV :: 'n set)}" @@ -2001,8 +2001,4 @@ apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe) apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed -text {* Legacy theorem names *} - -lemmas Lim_component_cart = tendsto_vec_nth - end diff -r c0fd385a41f4 -r 9ab8c88449a4 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Aug 26 23:02:00 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat Aug 27 09:02:25 2011 +0200 @@ -229,12 +229,18 @@ from g(1) gS giS gBC show ?thesis by blast qed +lemma closure_bounded_linear_image: + assumes f: "bounded_linear f" + shows "f ` (closure S) \ closure (f ` S)" + using linear_continuous_on [OF f] closed_closure closure_subset + by (rule image_closure_subset) + lemma closure_linear_image: fixes f :: "('m::euclidean_space) => ('n::real_normed_vector)" assumes "linear f" shows "f ` (closure S) <= closure (f ` S)" -using image_closure_subset[of S f "closure (f ` S)"] assms linear_conv_bounded_linear[of f] -linear_continuous_on[of f "closure S"] closed_closure[of "f ` S"] closure_subset[of "f ` S"] by auto + using assms unfolding linear_conv_bounded_linear + by (rule closure_bounded_linear_image) lemma closure_injective_linear_image: fixes f :: "('n::euclidean_space) => ('n::euclidean_space)" @@ -254,23 +260,16 @@ shows "closure (S <*> T) = closure S <*> closure T" by (rule closure_Times) -lemma closure_scaleR: (* TODO: generalize to real_normed_vector *) -fixes S :: "('n::euclidean_space) set" -shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)" -proof- -{ assume "c ~= 0" hence ?thesis using closure_injective_linear_image[of "(op *\<^sub>R c)" S] - linear_scaleR injective_scaleR by auto -} -moreover -{ assume zero: "c=0 & S ~= {}" - hence "closure S ~= {}" using closure_subset by auto - hence "op *\<^sub>R c ` (closure S) = {0}" using zero by auto - moreover have "op *\<^sub>R 0 ` S = {0}" using zero by auto - ultimately have ?thesis using zero by auto -} -moreover -{ assume "S={}" hence ?thesis by auto } -ultimately show ?thesis by blast +lemma closure_scaleR: + fixes S :: "('a::real_normed_vector) set" + shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)" +proof + show "(op *\<^sub>R c) ` (closure S) \ closure ((op *\<^sub>R c) ` S)" + using bounded_linear_scaleR_right + by (rule closure_bounded_linear_image) + show "closure ((op *\<^sub>R c) ` S) \ (op *\<^sub>R c) ` (closure S)" + by (intro closure_minimal image_mono closure_subset + closed_scaling closed_closure) qed lemma fst_linear: "linear fst" unfolding linear_def by (simp add: algebra_simps) @@ -859,9 +858,8 @@ qed lemma cone_closure: -fixes S :: "('m::euclidean_space) set" -assumes "cone S" -shows "cone (closure S)" + fixes S :: "('a::real_normed_vector) set" + assumes "cone S" shows "cone (closure S)" proof- { assume "S = {}" hence ?thesis by auto } moreover @@ -2310,12 +2308,7 @@ lemma closure_affine_hull: fixes S :: "('n::euclidean_space) set" shows "closure S <= affine hull S" -proof- -have "closure S <= closure (affine hull S)" using subset_closure by auto -moreover have "closure (affine hull S) = affine hull S" - using affine_affine_hull affine_closed[of "affine hull S"] closure_eq by auto -ultimately show ?thesis by auto -qed + by (intro closure_minimal hull_subset affine_closed affine_affine_hull) lemma closure_same_affine_hull: fixes S :: "('n::euclidean_space) set" @@ -2580,6 +2573,37 @@ done 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 = {}") + case True thus ?thesis by simp +next + case False with assms show ?thesis + proof (induct rule: finite_ne_induct) + case (singleton x) show ?case by simp + next + case (insert x A) + let ?f = "\(u, y::'a). u *\<^sub>R x + (1 - u) *\<^sub>R y" + let ?T = "{0..1::real} \ (convex hull A)" + have "continuous_on ?T ?f" + unfolding split_def continuous_on by (intro ballI tendsto_intros) + moreover have "compact ?T" + by (intro compact_Times compact_interval insert) + ultimately have "compact (?f ` ?T)" + by (rule compact_continuous_image) + also have "?f ` ?T = convex hull (insert x A)" + unfolding convex_hull_insert [OF `A \ {}`] + apply safe + apply (rule_tac x=a in exI, simp) + apply (rule_tac x="1 - a" in exI, simp) + apply fast + apply (rule_tac x="(u, b)" in image_eqI, simp_all) + done + finally show "compact (convex hull (insert x A))" . + qed +qed + lemma compact_convex_hull: fixes s::"('a::euclidean_space) set" assumes "compact s" shows "compact(convex hull s)" proof(cases "s={}") @@ -2654,11 +2678,6 @@ qed qed -lemma finite_imp_compact_convex_hull: - fixes s :: "('a::euclidean_space) set" - shows "finite s \ compact(convex hull s)" -by (metis compact_convex_hull finite_imp_compact) - subsection {* Extremal points of a simplex are some vertices. *} lemma dist_increases_online: @@ -2738,7 +2757,7 @@ qed (auto simp add: assms) lemma simplex_furthest_le: - fixes s :: "('a::euclidean_space) set" + fixes s :: "('a::real_inner) set" assumes "finite s" "s \ {}" shows "\y\s. \x\(convex hull s). norm(x - a) \ norm(y - a)" proof- @@ -2754,12 +2773,12 @@ qed lemma simplex_furthest_le_exists: - fixes s :: "('a::euclidean_space) set" + 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::euclidean_space) set" + fixes s :: "('a::real_inner) set" assumes "finite s" "s \ {}" shows "\u\s. \v\s. \x\convex hull s. \y \ convex hull s. norm(x - y) \ norm(u - v)" proof- @@ -2780,7 +2799,7 @@ qed lemma simplex_extremal_le_exists: - fixes s :: "('a::euclidean_space) set" + 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 @@ -3094,7 +3113,6 @@ subsection {* Convexity of cone hulls *} lemma convex_cone_hull: -fixes S :: "('m::euclidean_space) set" assumes "convex S" shows "convex (cone hull S)" proof- @@ -3126,7 +3144,6 @@ qed lemma cone_convex_hull: -fixes S :: "('m::euclidean_space) set" assumes "cone S" shows "cone (convex hull S)" proof- @@ -3453,22 +3470,27 @@ ultimately show ?thesis using injpi by auto qed qed qed auto qed -lemma homeomorphic_convex_compact_lemma: fixes s::"('a::euclidean_space) set" - assumes "convex s" "compact s" "cball 0 1 \ s" +lemma homeomorphic_convex_compact_lemma: + fixes s :: "('a::euclidean_space) set" + assumes "convex s" and "compact s" and "cball 0 1 \ s" shows "s homeomorphic (cball (0::'a) 1)" - apply(rule starlike_compact_projective[OF assms(2-3)]) proof(rule,rule,rule,erule conjE) - fix x u assume as:"x \ s" "0 \ u" "u < (1::real)" - hence "u *\<^sub>R x \ interior s" unfolding interior_def mem_Collect_eq - apply(rule_tac x="ball (u *\<^sub>R x) (1 - u)" in exI) apply(rule, rule open_ball) - unfolding centre_in_ball apply rule defer apply(rule) unfolding mem_ball proof- - fix y assume "dist (u *\<^sub>R x) y < 1 - u" - hence "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \ s" - using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm - unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR - apply (rule mult_left_le_imp_le[of "1 - u"]) - unfolding mult_assoc[symmetric] using `u<1` by auto - thus "y \ s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u] - using as unfolding scaleR_scaleR by auto qed auto +proof (rule starlike_compact_projective[OF assms(2-3)], clarify) + fix x u assume "x \ s" and "0 \ u" and "u < (1::real)" + have "open (ball (u *\<^sub>R x) (1 - u))" by (rule open_ball) + moreover have "u *\<^sub>R x \ ball (u *\<^sub>R x) (1 - u)" + unfolding centre_in_ball using `u < 1` by simp + moreover have "ball (u *\<^sub>R x) (1 - u) \ s" + proof + fix y assume "y \ ball (u *\<^sub>R x) (1 - u)" + hence "dist (u *\<^sub>R x) y < 1 - u" unfolding mem_ball . + with `u < 1` have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \ cball 0 1" + by (simp add: dist_norm inverse_eq_divide norm_minus_commute) + with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \ s" .. + with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \ s" + using `x \ s` `0 \ u` `u < 1` [THEN less_imp_le] by (rule mem_convex) + thus "y \ s" using `u < 1` by simp + qed + ultimately have "u *\<^sub>R x \ interior s" .. thus "u *\<^sub>R x \ s - frontier s" using frontier_def and interior_subset by auto qed lemma homeomorphic_convex_compact_cball: fixes e::real and s::"('a::euclidean_space) set" @@ -3621,8 +3643,8 @@ assumes "a \ b" "continuous_on {a .. b} f" "(f b)$$k \ y" "y \ (f a)$$k" shows "\x\{a..b}. (f x)$$k = y" apply(subst neg_equal_iff_equal[THEN sym]) - using ivt_increasing_component_on_1[of a b "\x. - f x" k "- y"] using assms using continuous_on_neg - by auto + using ivt_increasing_component_on_1[of a b "\x. - f x" k "- y"] + using assms using continuous_on_minus by auto lemma ivt_decreasing_component_1: fixes f::"real \ 'a::euclidean_space" shows "a \ b \ \x\{a .. b}. continuous (at x) f @@ -4042,7 +4064,7 @@ then obtain y where "y\s" and y:"norm (y - x) * (1 - e) < e * d" by auto def 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" apply(rule subset_interior[OF d,unfolded subset_eq,rule_format]) + 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) by(auto simp add:field_simps norm_minus_commute) thus ?thesis unfolding * apply - apply(rule mem_interior_convex_shrink) @@ -4380,7 +4402,7 @@ shows "closure(rel_interior S) = closure S" proof- have h1: "closure(rel_interior S) <= closure S" - using subset_closure[of "rel_interior S" S] rel_interior_subset[of S] by auto + using closure_mono[of "rel_interior S" S] rel_interior_subset[of S] by auto { assume "S ~= {}" from this obtain a where a_def: "a : rel_interior S" using rel_interior_convex_nonempty assms by auto { fix x assume x_def: "x : closure S" @@ -4517,7 +4539,7 @@ proof- have "?A --> ?B" by (metis assms closure_subset convex_rel_interior_closure rel_interior_subset) moreover have "?B --> (closure S1 <= closure S2)" - by (metis assms(1) convex_closure_rel_interior subset_closure) + by (metis assms(1) convex_closure_rel_interior closure_mono) moreover have "?B --> (closure S1 >= closure S2)" by (metis closed_closure closure_minimal) ultimately show ?thesis by blast qed @@ -4777,7 +4799,7 @@ using convex_closure_rel_interior_inter assms by auto moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)" using rel_interior_inter_aux - subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto + closure_mono[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto ultimately show ?thesis using closure_inter[of I] by auto qed @@ -4790,7 +4812,7 @@ using convex_closure_rel_interior_inter assms by auto moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)" using rel_interior_inter_aux - subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto + closure_mono[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto ultimately show ?thesis using closure_inter[of I] by auto qed @@ -4886,7 +4908,7 @@ proof- have *: "S Int closure T = S" using assms by auto have "~(rel_interior S <= rel_frontier T)" - using subset_closure[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T] + using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T] closure_closed convex_closure_rel_interior[of S] closure_subset[of S] assms by auto hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}" using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto @@ -4911,8 +4933,8 @@ also have "... = f ` (closure (rel_interior S))" using convex_closure_rel_interior assms by auto also have "... <= closure (f ` (rel_interior S))" using closure_linear_image assms by auto finally have "closure (f ` S) = closure (f ` rel_interior S)" - using subset_closure[of "f ` S" "closure (f ` rel_interior S)"] closure_closure - subset_closure[of "f ` rel_interior S" "f ` S"] * by auto + using closure_mono[of "f ` S" "closure (f ` rel_interior S)"] closure_closure + closure_mono[of "f ` rel_interior S" "f ` S"] * by auto hence "rel_interior (f ` S) = rel_interior (f ` rel_interior S)" using assms convex_rel_interior linear_conv_bounded_linear[of f] convex_linear_image[of S] convex_linear_image[of "rel_interior S"] closure_eq_rel_interior_eq[of "f ` S" "f ` rel_interior S"] by auto diff -r c0fd385a41f4 -r 9ab8c88449a4 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri Aug 26 23:02:00 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Sat Aug 27 09:02:25 2011 +0200 @@ -785,7 +785,7 @@ have "\x\{a<..xa. f' x xa - (f b - f a) / (b - a) * xa) = (\v. 0)" apply(rule rolle[OF assms(1), of "\x. f x - (f b - f a) / (b - a) * x"]) defer - apply(rule continuous_on_intros assms(2) continuous_on_cmul[where 'b=real, unfolded real_scaleR_def])+ + apply(rule continuous_on_intros assms(2))+ proof fix x assume x:"x \ {a<..x. f x - (f b - f a) / (b - a) * x) has_derivative (\xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)" @@ -869,7 +869,7 @@ unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib by (auto simp add: algebra_simps) hence 1:"continuous_on {0..1} (f \ ?p)" apply- - apply(rule continuous_on_intros continuous_on_vmul)+ + apply(rule continuous_on_intros)+ unfolding continuous_on_eq_continuous_within apply(rule,rule differentiable_imp_continuous_within) unfolding differentiable_def apply(rule_tac x="f' xa" in exI) diff -r c0fd385a41f4 -r 9ab8c88449a4 src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Aug 26 23:02:00 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sat Aug 27 09:02:25 2011 +0200 @@ -149,7 +149,7 @@ assumes "\i. i < DIM('a) \ x $$ i = y $$ i" shows "x = y" proof - from assms have "\i sqprojection \ ?F)" apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+ prefer 2 apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+ unfolding * apply(rule assms)+ apply(rule continuous_on_compose,subst sqprojection_def) - apply(rule continuous_on_mul ) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def]) + apply(rule continuous_on_scaleR) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def]) apply(rule continuous_at_infnorm) unfolding infnorm_eq_0 defer apply(rule continuous_on_id) 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 and x y::"real^2" and c::real show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i" diff -r c0fd385a41f4 -r 9ab8c88449a4 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Aug 26 23:02:00 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Sat Aug 27 09:02:25 2011 +0200 @@ -378,7 +378,7 @@ interior(x1 \ y1) \ interior(x1) \ interior(x1 \ y1) \ interior(y1) \ interior(x2 \ y2) \ interior(x2) \ interior(x2 \ y2) \ interior(y2) \ interior(x1 \ y1) \ interior(x2 \ y2) = {}" by auto - show "interior k1 \ interior k2 = {}" unfolding k1 k2 apply(rule *) defer apply(rule_tac[1-4] subset_interior) + show "interior k1 \ interior k2 = {}" unfolding k1 k2 apply(rule *) defer apply(rule_tac[1-4] interior_mono) using division_ofD(5)[OF assms(1) k1(2) k2(2)] using division_ofD(5)[OF assms(2) k1(3) k2(3)] using th by auto qed qed @@ -407,9 +407,9 @@ show "finite (p1 \ p2)" using d1(1) d2(1) by auto show "\(p1 \ p2) = s1 \ s2" using d1(6) d2(6) by auto { fix k1 k2 assume as:"k1 \ p1 \ p2" "k2 \ p1 \ p2" "k1 \ k2" moreover let ?g="interior k1 \ interior k2 = {}" - { assume as:"k1\p1" "k2\p2" have ?g using subset_interior[OF d1(2)[OF as(1)]] subset_interior[OF d2(2)[OF as(2)]] + { assume as:"k1\p1" "k2\p2" have ?g using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]] using assms(3) by blast } moreover - { assume as:"k1\p2" "k2\p1" have ?g using subset_interior[OF d1(2)[OF as(2)]] subset_interior[OF d2(2)[OF as(1)]] + { assume as:"k1\p2" "k2\p1" have ?g using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]] using assms(3) by blast} ultimately show ?g using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto } fix k assume k:"k \ p1 \ p2" show "k \ s1 \ s2" using k d1(2) d2(2) by auto @@ -573,7 +573,7 @@ show "finite (q k - {k})" "open (interior k)" "\t\q k - {k}. \a b. t = {a..b}" using qk by auto show "\t\q k - {k}. interior k \ interior t = {}" using qk(5) using q(2)[OF k] by auto have *:"\x s. x \ s \ \s \ x" by auto show "interior (\(\i. \(q i - {i})) ` p) \ interior (\(q k - {k}))" - apply(rule subset_interior *)+ using k by auto qed qed qed auto qed + apply(rule interior_mono *)+ using k by auto qed qed qed auto qed lemma elementary_bounded[dest]: "p division_of s \ bounded (s::('a::ordered_euclidean_space) set)" unfolding division_of_def by(metis bounded_Union bounded_interval) @@ -823,7 +823,7 @@ fix x k assume xk:"(x,k)\p1\p2" show "x\k" "\a b. k = {a..b}" using xk p1(2,4) p2(2,4) by auto show "k\s1\s2" using xk p1(3) p2(3) by blast fix x' k' assume xk':"(x',k')\p1\p2" "(x,k) \ (x',k')" - have *:"\a b. a\ s1 \ b\ s2 \ interior a \ interior b = {}" using assms(3) subset_interior by blast + have *:"\a b. a\ s1 \ b\ s2 \ interior a \ interior b = {}" using assms(3) interior_mono by blast show "interior k \ interior k' = {}" apply(cases "(x,k)\p1", case_tac[!] "(x',k')\p1") apply(rule p1(5)) prefer 4 apply(rule *) prefer 6 apply(subst Int_commute,rule *) prefer 8 apply(rule p2(5)) using p1(3) p2(3) using xk xk' by auto qed @@ -842,7 +842,7 @@ show "x\k" "\a b. k = {a..b}" "k \ \iset" using assm(2-4)[OF i] using i(1) by auto fix x' k' assume xk':"(x',k')\\pfn ` iset" "(x, k) \ (x', k')" then obtain i' where i':"i' \ iset" "(x', k') \ pfn i'" by auto have *:"\a b. i\i' \ a\ i \ b\ i' \ interior a \ interior b = {}" using i(1) i'(1) - using assms(3)[rule_format] subset_interior by blast + using assms(3)[rule_format] interior_mono by blast show "interior k \ interior k' = {}" apply(cases "i=i'") using assm(5)[OF i _ xk'(2)] i'(2) using assm(3)[OF i] assm(3)[OF i'] defer apply-apply(rule *) by auto qed @@ -1703,7 +1703,7 @@ by(rule le_less_trans[OF norm_le_l1]) hence "x + (\\ i. if i = k then e/2 else 0) \ {x. x$$k = c}" using e by auto thus False unfolding mem_Collect_eq using e x k by auto - qed ultimately have "content b = 0" unfolding uv content_eq_0_interior apply-apply(drule subset_interior) by auto + qed ultimately have "content b = 0" unfolding uv content_eq_0_interior apply-apply(drule interior_mono) by auto thus "content b *\<^sub>R f a = 0" by auto qed auto also have "\ < e" by(rule k d(2) p12 fine_union p1 p2)+ @@ -2563,7 +2563,7 @@ proof(rule,rule,rule,rule,rule,rule,rule,erule conjE) fix m n u v assume as:"{m..n} \ snd ` p" "{u..v} \ snd ` p" "{m..n} \ {u..v}" "{m..n} \ {x. \x $$ k - c\ \