--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jan 22 16:59:21 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Jan 25 16:56:24 2010 +0100
@@ -19,21 +19,14 @@
declare dot_lmult[simp] dot_rmult[simp] dot_lneg[simp] dot_rneg[simp]
declare UNIV_1[simp]
-lemma dim1in[intro]:"Suc 0 \<in> {1::nat .. CARD(1)}" by auto
-
-lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_le_def Cart_lambda_beta dest_vec1_def basis_component vector_uminus_component
-
-lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul continuous_const continuous_sub continuous_at_id continuous_within_id
-
-lemmas continuous_on_intros = continuous_on_add continuous_on_const continuous_on_id continuous_on_compose continuous_on_cmul continuous_on_neg continuous_on_sub
- uniformly_continuous_on_add uniformly_continuous_on_const uniformly_continuous_on_id uniformly_continuous_on_compose uniformly_continuous_on_cmul uniformly_continuous_on_neg uniformly_continuous_on_sub
+(*lemma dim1in[intro]:"Suc 0 \<in> {1::nat .. CARD(1)}" by auto*)
+
+lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_le_def Cart_lambda_beta basis_component vector_uminus_component
lemma dest_vec1_simps[simp]: fixes a::"real^1"
shows "a$1 = 0 \<longleftrightarrow> a = 0" (*"a \<le> 1 \<longleftrightarrow> dest_vec1 a \<le> 1" "0 \<le> a \<longleftrightarrow> 0 \<le> dest_vec1 a"*)
"a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1"
- by(auto simp add:vector_component_simps all_1 Cart_eq)
-
-lemma nequals0I:"x\<in>A \<Longrightarrow> A \<noteq> {}" by auto
+ by(auto simp add:vector_component_simps forall_1 Cart_eq)
lemma norm_not_0:"(x::real^'n)\<noteq>0 \<Longrightarrow> norm x \<noteq> 0" by auto
@@ -59,7 +52,7 @@
lemma mem_interval_1: fixes x :: "real^1" shows
"(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
"(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-by(simp_all add: Cart_eq vector_less_def vector_le_def dest_vec1_def all_1)
+by(simp_all add: Cart_eq vector_less_def vector_le_def forall_1)
lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::real^'n)) ` {a..b} =
(if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})"
@@ -75,8 +68,8 @@
apply(rule_tac [!] allI)apply(rule_tac [!] impI)
apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI)
apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI)
- by (auto simp add: vector_less_def vector_le_def all_1 dest_vec1_def
- vec1_dest_vec1[unfolded dest_vec1_def One_nat_def])
+ by (auto simp add: vector_less_def vector_le_def forall_1
+ vec1_dest_vec1[unfolded One_nat_def])
lemma dest_vec1_setsum: assumes "finite S"
shows " dest_vec1 (setsum f S) = setsum (\<lambda>x. dest_vec1 (f x)) S"
@@ -611,7 +604,7 @@
subsection {* One rather trivial consequence. *}
-lemma connected_UNIV: "connected (UNIV :: 'a::real_normed_vector set)"
+lemma connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)"
by(simp add: convex_connected convex_UNIV)
subsection {* Convex functions into the reals. *}
@@ -624,7 +617,7 @@
lemma convex_on_subset: "convex_on t f \<Longrightarrow> s \<subseteq> t \<Longrightarrow> convex_on s f"
unfolding convex_on_def by auto
-lemma convex_add:
+lemma convex_add[intro]:
assumes "convex_on s f" "convex_on s g"
shows "convex_on s (\<lambda>x. f x + g x)"
proof-
@@ -638,7 +631,7 @@
thus ?thesis unfolding convex_on_def by auto
qed
-lemma convex_cmul:
+lemma convex_cmul[intro]:
assumes "0 \<le> (c::real)" "convex_on s f"
shows "convex_on s (\<lambda>x. c * f x)"
proof-
@@ -680,7 +673,7 @@
ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto
qed
-lemma convex_distance:
+lemma convex_distance[intro]:
fixes s :: "'a::real_normed_vector set"
shows "convex_on s (\<lambda>x. dist a x)"
proof(auto simp add: convex_on_def dist_norm)
@@ -1248,7 +1241,7 @@
subsection {* Openness and compactness are preserved by convex hull operation. *}
-lemma open_convex_hull:
+lemma open_convex_hull[intro]:
fixes s :: "'a::real_normed_vector set"
assumes "open s"
shows "open(convex hull s)"
@@ -1287,8 +1280,7 @@
qed
lemma open_dest_vec1_vimage: "open S \<Longrightarrow> open (dest_vec1 -` S)"
-unfolding open_vector_def all_1
-by (auto simp add: dest_vec1_def)
+unfolding open_vector_def forall_1 by auto
lemma tendsto_dest_vec1 [tendsto_intros]:
"(f ---> l) net \<Longrightarrow> ((\<lambda>x. dest_vec1 (f x)) ---> dest_vec1 l) net"
@@ -1837,7 +1829,7 @@
using ed(1,2) and u unfolding subset_eq mem_ball Ball_def dist_norm by(auto simp add: algebra_simps)
thus "z \<in> s" using u by (auto simp add: algebra_simps) qed(insert u ed(3-4), auto) qed
-lemma convex_hull_eq_empty: "convex hull s = {} \<longleftrightarrow> s = {}"
+lemma convex_hull_eq_empty[simp]: "convex hull s = {} \<longleftrightarrow> s = {}"
using hull_subset[of s convex] convex_hull_empty by auto
subsection {* Moving and scaling convex hulls. *}
@@ -2247,12 +2239,19 @@
lemma mem_epigraph: "(pastecart x (vec1 y)) \<in> epigraph s f \<longleftrightarrow> x \<in> s \<and> f x \<le> y" unfolding epigraph_def by auto
+(** move this**)
+lemma forall_dest_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P(dest_vec1 x))"
+ apply safe defer apply(erule_tac x="vec1 x" in allE) by auto
+
+(** This might break sooner or later. In fact it did already once. **)
lemma convex_epigraph:
"convex(epigraph s f) \<longleftrightarrow> convex_on s f \<and> convex s"
unfolding convex_def convex_on_def unfolding Ball_def forall_pastecart epigraph_def
- unfolding mem_Collect_eq fstcart_pastecart sndcart_pastecart sndcart_add sndcart_cmul [where 'a=real, unfolded smult_conv_scaleR] fstcart_add fstcart_cmul [where 'a=real, unfolded smult_conv_scaleR]
- unfolding Ball_def[symmetric] unfolding dest_vec1_add dest_vec1_cmul [where 'a=real, unfolded smult_conv_scaleR]
- apply(subst forall_dest_vec1[THEN sym])+ by(meson real_le_refl real_le_trans add_mono mult_left_mono)
+ unfolding mem_Collect_eq fstcart_pastecart sndcart_pastecart sndcart_add sndcart_cmul [where 'a=real, unfolded smult_conv_scaleR] fstcart_add fstcart_cmul [where 'a=real, unfolded smult_conv_scaleR] Ball_def[symmetric] unfolding vector_add_component vector_scaleR_component
+ apply(subst forall_dest_vec1[THEN sym])+
+ apply safe defer apply(erule_tac x=x in allE,erule_tac x="f x" in allE) apply safe
+ apply(erule_tac x=xa in allE,erule_tac x="f xa" in allE) prefer 3
+ apply(rule_tac y="u * f x + v * f xb" in order_trans) defer by(auto intro!:mult_left_mono add_mono)
lemma convex_epigraphI: assumes "convex_on s f" "convex s"
shows "convex(epigraph s f)" using assms unfolding convex_epigraph by auto
@@ -2284,13 +2283,13 @@
f (setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} ) \<le> setsum (\<lambda>i. u i * f(x i)) {1..k} ) "
unfolding convex_epigraph_convex[OF assms] convex epigraph_def Ball_def mem_Collect_eq
unfolding sndcart_setsum[OF finite_atLeastAtMost] fstcart_setsum[OF finite_atLeastAtMost] dest_vec1_setsum[OF finite_atLeastAtMost]
- unfolding fstcart_pastecart sndcart_pastecart sndcart_add sndcart_cmul [where 'a=real, unfolded smult_conv_scaleR] fstcart_add fstcart_cmul [where 'a=real, unfolded smult_conv_scaleR]
- unfolding dest_vec1_add dest_vec1_cmul [where 'a=real, unfolded smult_conv_scaleR] apply(subst forall_of_pastecart)+ apply(subst forall_of_dest_vec1)+ apply rule
+ unfolding fstcart_pastecart sndcart_pastecart sndcart_add sndcart_cmul [where 'a=real, unfolded smult_conv_scaleR] fstcart_add fstcart_cmul [where 'a=real, unfolded smult_conv_scaleR] unfolding vector_scaleR_component
+ apply(subst forall_of_pastecart)+ apply(subst forall_of_dest_vec1)+ apply rule
using assms[unfolded convex] apply simp apply(rule,rule,rule)
apply(erule_tac x=k in allE, erule_tac x=u in allE, erule_tac x=x in allE) apply rule apply rule apply rule defer
apply(rule_tac j="\<Sum>i = 1..k. u i * f (x i)" in real_le_trans)
- defer apply(rule setsum_mono) apply(erule conjE)+ apply(erule_tac x=i in allE)apply(rule mult_left_mono)
- using assms[unfolded convex] by auto
+ defer apply(rule setsum_mono) apply(erule conjE)+ apply(erule_tac x=i in allE) unfolding real_scaleR_def
+ apply(rule mult_left_mono)using assms[unfolded convex] by auto
subsection {* Convexity of general and special intervals. *}
@@ -2324,7 +2323,7 @@
lemma is_interval_1:
"is_interval s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b \<longrightarrow> x \<in> s)"
- unfolding is_interval_def dest_vec1_def forall_1 by auto
+ unfolding is_interval_def forall_1 by auto
lemma is_interval_connected_1: "is_interval s \<longleftrightarrow> connected (s::(real^1) set)"
apply(rule, rule is_interval_connected, assumption) unfolding is_interval_1
@@ -2333,8 +2332,8 @@
hence *:"dest_vec1 a < dest_vec1 x" "dest_vec1 x < dest_vec1 b" apply(rule_tac [!] ccontr) unfolding not_less by auto
let ?halfl = "{z. inner (basis 1) z < dest_vec1 x} " and ?halfr = "{z. inner (basis 1) z > dest_vec1 x} "
{ fix y assume "y \<in> s" have "y \<in> ?halfr \<union> ?halfl" apply(rule ccontr)
- using as(6) `y\<in>s` by (auto simp add: inner_vector_def dest_vec1_eq [unfolded dest_vec1_def] dest_vec1_def) }
- moreover have "a\<in>?halfl" "b\<in>?halfr" using * by (auto simp add: inner_vector_def dest_vec1_def)
+ using as(6) `y\<in>s` by (auto simp add: inner_vector_def dest_vec1_eq) }
+ moreover have "a\<in>?halfl" "b\<in>?halfr" using * by (auto simp add: inner_vector_def)
hence "?halfl \<inter> s \<noteq> {}" "?halfr \<inter> s \<noteq> {}" using as(2-3) by auto
ultimately show False apply(rule_tac notE[OF as(1)[unfolded connected_def]])
apply(rule_tac x="?halfl" in exI, rule_tac x="?halfr" in exI)
@@ -2355,7 +2354,7 @@
assumes "dest_vec1 a \<le> dest_vec1 b" "continuous_on {a .. b} f" "(f a)$k \<le> y" "y \<le> (f b)$k"
shows "\<exists>x\<in>{a..b}. (f x)$k = y"
proof- have "f a \<in> f ` {a..b}" "f b \<in> f ` {a..b}" apply(rule_tac[!] imageI)
- using assms(1) by(auto simp add: vector_le_def dest_vec1_def)
+ using assms(1) by(auto simp add: vector_le_def)
thus ?thesis using connected_ivt_component[of "f ` {a..b}" "f a" "f b" k y]
using connected_continuous_image[OF assms(2) convex_connected[OF convex_interval(1)]]
using assms by(auto intro!: imageI) qed
@@ -2919,8 +2918,7 @@
have *:"\<And>g. path g \<Longrightarrow> path(reversepath g)" unfolding path_def reversepath_def
apply(rule continuous_on_compose[unfolded o_def, of _ "\<lambda>x. 1 - x"])
apply(rule continuous_on_sub, rule continuous_on_const, rule continuous_on_id)
- apply(rule continuous_on_subset[of "{0..1}"], assumption)
- by (auto, auto simp add:vector_le_def vector_component_simps elim!:ballE)
+ apply(rule continuous_on_subset[of "{0..1}"], assumption) by auto
show ?thesis using *[of g] *[of "reversepath g"] unfolding reversepath_reversepath by auto qed
lemmas reversepath_simps = path_reversepath path_image_reversepath pathstart_reversepath pathfinish_reversepath
@@ -2931,7 +2929,7 @@
have *:"g1 = (\<lambda>x. g1 (2 *\<^sub>R x)) \<circ> (\<lambda>x. (1/2) *\<^sub>R x)"
"g2 = (\<lambda>x. g2 (2 *\<^sub>R x - 1)) \<circ> (\<lambda>x. (1/2) *\<^sub>R (x + 1))" unfolding o_def by auto
have "op *\<^sub>R (1 / 2) ` {0::real^1..1} \<subseteq> {0..1}" "(\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {(0::real^1)..1} \<subseteq> {0..1}"
- unfolding image_smult_interval by (auto, auto simp add:vector_le_def vector_component_simps elim!:ballE)
+ unfolding image_smult_interval by auto
thus "continuous_on {0..1} g1 \<and> continuous_on {0..1} g2" apply -apply rule
apply(subst *) defer apply(subst *) apply (rule_tac[!] continuous_on_compose)
apply (rule continuous_on_cmul, rule continuous_on_add, rule continuous_on_id, rule continuous_on_const) defer
@@ -3000,9 +2998,8 @@
apply(erule_tac x="1-x" in ballE, erule_tac x="1-y" in ballE)
unfolding mem_interval_1 by(auto simp add:vector_component_simps)
-lemma dest_vec1_scaleR [simp]:
- "dest_vec1 (scaleR a x) = scaleR a (dest_vec1 x)"
-unfolding dest_vec1_def by simp
+(** move this **)
+declare vector_scaleR_component[simp]
lemma simple_path_join_loop:
assumes "injective_path g1" "injective_path g2" "pathfinish g2 = pathstart g1"
@@ -3013,14 +3010,13 @@
fix x y::"real^1" assume xy:"x \<in> {0..1}" "y \<in> {0..1}" "?g x = ?g y"
show "x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0" proof(case_tac "x$1 \<le> 1/2",case_tac[!] "y$1 \<le> 1/2", unfold not_le)
assume as:"x $ 1 \<le> 1 / 2" "y $ 1 \<le> 1 / 2"
- hence "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)" using xy(3) unfolding joinpaths_def dest_vec1_def by auto
+ hence "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)" using xy(3) unfolding joinpaths_def by auto
moreover have "2 *\<^sub>R x \<in> {0..1}" "2 *\<^sub>R y \<in> {0..1}" using xy(1,2) as
- unfolding mem_interval_1 dest_vec1_def by(auto simp add:vector_component_simps)
+ unfolding mem_interval_1 by(auto simp add:vector_component_simps)
ultimately show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] by auto
next assume as:"x $ 1 > 1 / 2" "y $ 1 > 1 / 2"
- hence "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)" using xy(3) unfolding joinpaths_def dest_vec1_def by auto
- moreover have "2 *\<^sub>R x - 1 \<in> {0..1}" "2 *\<^sub>R y - 1 \<in> {0..1}" using xy(1,2) as
- unfolding mem_interval_1 dest_vec1_def by(auto simp add:vector_component_simps)
+ hence "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)" using xy(3) unfolding joinpaths_def by auto
+ moreover have "2 *\<^sub>R x - 1 \<in> {0..1}" "2 *\<^sub>R y - 1 \<in> {0..1}" using xy(1,2) as unfolding mem_interval_1 by(auto simp add:vector_component_simps)
ultimately show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by auto
next assume as:"x $ 1 \<le> 1 / 2" "y $ 1 > 1 / 2"
hence "?g x \<in> path_image g1" "?g y \<in> path_image g2" unfolding path_image_def joinpaths_def
@@ -3055,6 +3051,7 @@
shows "injective_path(g1 +++ g2)"
unfolding injective_path_def proof(rule,rule,rule) let ?g = "g1 +++ g2"
note inj = assms(1,2)[unfolded injective_path_def, rule_format]
+ have *:"\<And>x y::real^1. 2 *\<^sub>R x = 1 \<Longrightarrow> 2 *\<^sub>R y = 1 \<Longrightarrow> x = y" unfolding Cart_eq forall_1 by(auto simp del:dest_vec1_eq)
fix x y assume xy:"x \<in> {0..1}" "y \<in> {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y"
show "x = y" proof(cases "x$1 \<le> 1/2", case_tac[!] "y$1 \<le> 1/2", unfold not_le)
assume "x $ 1 \<le> 1 / 2" "y $ 1 \<le> 1 / 2" thus ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy
@@ -3067,14 +3064,14 @@
hence "?g x = pathfinish g1" "?g y = pathstart g2" using assms(4) unfolding assms(3) xy(3) by auto
thus ?thesis using as and inj(1)[of "2 *\<^sub>R x" 1] inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(1,2)
unfolding pathstart_def pathfinish_def joinpaths_def mem_interval_1
- by(auto simp add:vector_component_simps Cart_eq forall_1)
+ by(auto simp add:vector_component_simps intro:*)
next assume as:"x $ 1 > 1 / 2" "y $ 1 \<le> 1 / 2"
hence "?g x \<in> path_image g2" "?g y \<in> path_image g1" unfolding path_image_def joinpaths_def
using xy(1,2)[unfolded mem_interval_1] by(auto simp add:vector_component_simps intro!: imageI)
hence "?g x = pathstart g2" "?g y = pathfinish g1" using assms(4) unfolding assms(3) xy(3) by auto
thus ?thesis using as and inj(2)[of "2 *\<^sub>R x - 1" 0] inj(1)[of "2 *\<^sub>R y" 1] and xy(1,2)
unfolding pathstart_def pathfinish_def joinpaths_def mem_interval_1
- by(auto simp add:vector_component_simps forall_1 Cart_eq) qed qed
+ by(auto simp add:vector_component_simps intro:*) qed qed
lemmas join_paths_simps = path_join path_image_join pathstart_join pathfinish_join
@@ -3345,6 +3342,7 @@
next case True hence d:"1\<in>{1..CARD('n)}" "2\<in>{1..CARD('n)}" using Suc(2) by auto
have ***:"Suc 1 = 2" by auto
have **:"\<And>s t P Q. s \<union> t \<union> {x. P x \<or> Q x} = (s \<union> {x. P x}) \<union> (t \<union> {x. Q x})" by auto
+ have nequals0I:"\<And>x A. x\<in>A \<Longrightarrow> A \<noteq> {}" by auto
have "\<psi> 2 \<noteq> \<psi> (Suc 0)" apply(rule ccontr) using \<psi>[unfolded bij_betw_def inj_on_def, THEN conjunct1, THEN bspec[where x=2]] using assms by auto
thus ?thesis unfolding * True unfolding ** neq_iff bex_disj_distrib apply -
apply(rule path_connected_Un, rule_tac[1-2] path_connected_Un) defer 3 apply(rule_tac[1-4] convex_imp_path_connected)