Replaced vec1 and dest_vec1 by abbreviation.
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Jan 22 16:59:21 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Jan 25 16:56:24 2010 +0100
@@ -1460,8 +1460,7 @@
let ?F = "(\<lambda>w::real^2. (f \<circ> vec1 \<circ> (\<lambda>x. x$1)) w - (g \<circ> vec1 \<circ> (\<lambda>x. x$2)) w)"
have *:"\<And>i. vec1 ` (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real^1}"
apply(rule set_ext) unfolding image_iff Bex_def mem_interval apply rule defer
- apply(rule_tac x="dest_vec1 x" in exI) apply rule apply(rule_tac x="vec (dest_vec1 x)" in exI)
- by(auto simp add: dest_vec1_def[THEN sym])
+ apply(rule_tac x="dest_vec1 x" in exI) apply rule apply(rule_tac x="vec (dest_vec1 x)" in exI) by auto
{ fix x assume "x \<in> (\<lambda>w. (f \<circ> vec1 \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> vec1 \<circ> (\<lambda>x. x $ 2)) w) ` {- 1..1::real^2}"
then guess w unfolding image_iff .. note w = this
hence "x \<noteq> 0" using as[of "vec1 (w$1)" "vec1 (w$2)"] unfolding mem_interval by auto} note x0=this
@@ -1539,7 +1538,7 @@
obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
def iscale \<equiv> "\<lambda>z::real^1. inverse 2 *\<^sub>R (z + 1)"
- have isc:"iscale ` {- 1..1} \<subseteq> {0..1}" unfolding iscale_def by(auto simp add:dest_vec1_add dest_vec1_neg)
+ have isc:"iscale ` {- 1..1} \<subseteq> {0..1}" unfolding iscale_def by(auto)
have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" proof(rule fashoda_unit)
show "(f \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" "(g \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}"
using isc and assms(3-4) unfolding image_compose by auto
--- 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)
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri Jan 22 16:59:21 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Jan 25 16:56:24 2010 +0100
@@ -212,7 +212,7 @@
using assms[unfolded has_derivative_def Lim] by auto
thus "eventually (\<lambda>x. dist (1 / norm (x - netlimit net) * (c x $ k - (c (netlimit net) $ k + c' (x - netlimit net) $ k))) 0 < e) net"
proof (rule eventually_elim1)
- case goal1 thus ?case apply - unfolding vector_dist_norm vec1_vec apply(rule le_less_trans) prefer 2 apply assumption unfolding * ** and norm_vec1[unfolded vec1_vec]
+ case goal1 thus ?case apply - unfolding vector_dist_norm apply(rule le_less_trans) prefer 2 apply assumption unfolding * ** and norm_vec1
using component_le_norm[of "(1 / norm (x - netlimit net)) *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net))) - 0" k] by auto
qed
qed(insert assms[unfolded has_derivative_def], auto simp add:linear_conv_bounded_linear) qed
@@ -619,7 +619,7 @@
note deriv = assms(3)[unfolded has_derivative_at_vec1]
obtain e where e:"e>0" "ball x e \<subseteq> s" using assms(2)[unfolded open_contains_ball] and assms(1) by auto
hence **:"(jacobian (vec1 \<circ> f) (at x)) $ 1 = 0" using differential_zero_maxmin_component[of e x "\<lambda>x. vec1 (f x)" 1]
- unfolding dest_vec1_def[THEN sym] vec1_dest_vec1 using assms(4) and assms(3)[unfolded has_derivative_at_vec1 o_def]
+ using assms(4) and assms(3)[unfolded has_derivative_at_vec1 o_def]
unfolding differentiable_def o_def by auto
have *:"jacobian (vec1 \<circ> f) (at x) = matrix (vec1 \<circ> f')" unfolding jacobian_def and frechet_derivative_at[OF deriv] ..
have "vec1 \<circ> f' = (\<lambda>x. 0)" apply(rule) unfolding matrix_works[OF derivative_is_linear[OF deriv],THEN sym]
@@ -651,7 +651,7 @@
hence "f' x \<circ> dest_vec1 = (\<lambda>v. 0)" apply(rule_tac differential_zero_maxmin[of "vec1 x" "vec1 ` {a<..<b}" "f \<circ> dest_vec1" "(f' x) \<circ> dest_vec1"])
unfolding vec1_interval defer apply(rule open_interval)
apply(rule assms(4)[unfolded has_derivative_at_dest_vec1[THEN sym],THEN bspec[where x=x]],assumption)
- unfolding o_def apply(erule disjE,rule disjI2) by(auto simp add: vector_less_def dest_vec1_def)
+ unfolding o_def apply(erule disjE,rule disjI2) by(auto simp add: vector_less_def)
thus ?thesis apply(rule_tac x=x in bexI) unfolding o_def apply rule
apply(drule_tac x="vec1 v" in fun_cong) unfolding vec1_dest_vec1 using x(1) by auto qed
@@ -738,12 +738,14 @@
also have "\<dots> \<le> B * norm(y - x)" apply(rule **) using * and u by auto
finally show ?thesis by(auto simp add:norm_minus_commute) qed
+(** move this **)
+declare norm_vec1[simp]
+
lemma onorm_vec1: fixes f::"real \<Rightarrow> real"
shows "onorm (\<lambda>x. vec1 (f (dest_vec1 x))) = onorm f" proof-
- have "\<forall>x::real^1. norm x = 1 \<longleftrightarrow> x\<in>{vec1 -1, vec1 (1::real)}" unfolding forall_vec1 unfolding norm_vec1 by auto
+ have "\<forall>x::real^1. norm x = 1 \<longleftrightarrow> x\<in>{vec1 -1, vec1 (1::real)}" unfolding forall_vec1 by(auto simp add:Cart_eq)
hence 1:"{x. norm x = 1} = {vec1 -1, vec1 (1::real)}" by(auto simp add:norm_vec1)
have 2:"{norm (vec1 (f (dest_vec1 x))) |x. norm x = 1} = (\<lambda>x. norm (vec1 (f (dest_vec1 x)))) ` {x. norm x=1}" by auto
-
have "\<forall>x::real. norm x = 1 \<longleftrightarrow> x\<in>{-1, 1}" by auto hence 3:"{x. norm x = 1} = {-1, (1::real)}" by auto
have 4:"{norm (f x) |x. norm x = 1} = (\<lambda>x. norm (f x)) ` {x. norm x=1}" by auto
show ?thesis unfolding onorm_def 1 2 3 4 by(simp add:Sup_finite_Max norm_vec1) qed
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Jan 22 16:59:21 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Jan 25 16:56:24 2010 +0100
@@ -14,9 +14,12 @@
text{* Some common special cases.*}
-lemma forall_1: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
+lemma forall_1[simp]: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
by (metis num1_eq_iff)
+lemma ex_1[simp]: "(\<exists>x::1. P x) \<longleftrightarrow> P 1"
+ by auto (metis num1_eq_iff)
+
lemma exhaust_2:
fixes x :: 2 shows "x = 1 \<or> x = 2"
proof (induct x)
@@ -196,7 +199,6 @@
instance cart :: (semigroup_add,finite) semigroup_add
apply (intro_classes) by (vector add_assoc)
-
instance cart :: (monoid_add,finite) monoid_add
apply (intro_classes) by vector+
@@ -2418,87 +2420,65 @@
(* "lift" from 'a to 'a^1 and "drop" from 'a^1 to 'a -- FIXME: potential use of transfer *)
-definition vec1:: "'a \<Rightarrow> 'a ^ 1" where "vec1 x = (\<chi> i. x)"
-
-definition dest_vec1:: "'a ^1 \<Rightarrow> 'a"
- where "dest_vec1 x = (x$1)"
+abbreviation vec1:: "'a \<Rightarrow> 'a ^ 1" where "vec1 x \<equiv> vec x"
+
+abbreviation dest_vec1:: "'a ^1 \<Rightarrow> 'a"
+ where "dest_vec1 x \<equiv> (x$1)"
lemma vec1_component[simp]: "(vec1 x)$1 = x"
- by (simp add: vec1_def)
+ by (simp add: )
lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"
- by (simp_all add: vec1_def dest_vec1_def Cart_eq forall_1)
+ by (simp_all add: Cart_eq forall_1)
lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))" by (metis vec1_dest_vec1)
lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))" by (metis vec1_dest_vec1)
-lemma forall_dest_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P(dest_vec1 x))" by (metis vec1_dest_vec1)
-
-lemma exists_dest_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(dest_vec1 x))"by (metis vec1_dest_vec1)
-
lemma vec1_eq[simp]: "vec1 x = vec1 y \<longleftrightarrow> x = y" by (metis vec1_dest_vec1)
lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \<longleftrightarrow> x = y" by (metis vec1_dest_vec1)
-lemma vec1_in_image_vec1: "vec1 x \<in> (vec1 ` S) \<longleftrightarrow> x \<in> S" by auto
-
-lemma vec1_vec: "vec1 x = vec x" by (vector vec1_def)
-
-lemma vec1_add: "vec1(x + y) = vec1 x + vec1 y" by (vector vec1_def)
-lemma vec1_sub: "vec1(x - y) = vec1 x - vec1 y" by (vector vec1_def)
-lemma vec1_cmul: "vec1(c* x) = c *s vec1 x " by (vector vec1_def)
-lemma vec1_neg: "vec1(- x) = - vec1 x " by (vector vec1_def)
-
-lemma vec1_0[simp]:"vec1 0 = 0" unfolding vec1_def Cart_eq by auto
+lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
+
+lemma vec_add: "vec(x + y) = vec x + vec y" by (vector vec_def)
+lemma vec_sub: "vec(x - y) = vec x - vec y" by (vector vec_def)
+lemma vec_cmul: "vec(c* x) = c *s vec x " by (vector vec_def)
+lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def)
lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_ext,rule) unfolding image_iff defer
apply(rule_tac x="dest_vec1 x" in bexI) by auto
-lemma vec1_setsum: assumes fS: "finite S"
- shows "vec1(setsum f S) = setsum (vec1 o f) S"
+lemma vec_setsum: assumes fS: "finite S"
+ shows "vec(setsum f S) = setsum (vec o f) S"
apply (induct rule: finite_induct[OF fS])
- apply (simp add: vec1_vec)
- apply (auto simp add: vec1_add)
+ apply (simp)
+ apply (auto simp add: vec_add)
done
lemma dest_vec1_lambda: "dest_vec1(\<chi> i. x i) = x 1"
- by (simp add: dest_vec1_def)
+ by (simp)
lemma dest_vec1_vec: "dest_vec1(vec x) = x"
- by (simp add: vec1_vec[symmetric])
-
-lemma dest_vec1_add: "dest_vec1(x + y) = dest_vec1 x + dest_vec1 y"
- by (metis vec1_dest_vec1 vec1_add)
-
-lemma dest_vec1_sub: "dest_vec1(x - y) = dest_vec1 x - dest_vec1 y"
- by (metis vec1_dest_vec1 vec1_sub)
-
-lemma dest_vec1_cmul: "dest_vec1(c*sx) = c * dest_vec1 x"
- by (metis vec1_dest_vec1 vec1_cmul)
-
-lemma dest_vec1_neg: "dest_vec1(- x) = - dest_vec1 x"
- by (metis vec1_dest_vec1 vec1_neg)
-
-lemma dest_vec1_0[simp]: "dest_vec1 0 = 0" by (metis vec_0 dest_vec1_vec)
+ by (simp)
lemma dest_vec1_sum: assumes fS: "finite S"
shows "dest_vec1(setsum f S) = setsum (dest_vec1 o f) S"
apply (induct rule: finite_induct[OF fS])
apply (simp add: dest_vec1_vec)
- apply (auto simp add: dest_vec1_add)
+ apply (auto simp add:vector_minus_component)
done
lemma norm_vec1: "norm(vec1 x) = abs(x)"
- by (simp add: vec1_def norm_real)
+ by (simp add: vec_def norm_real)
lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)"
by (simp only: dist_real vec1_component)
lemma abs_dest_vec1: "norm x = \<bar>dest_vec1 x\<bar>"
by (metis vec1_dest_vec1 norm_vec1)
-lemmas vec1_dest_vec1_simps = forall_vec1 vec1_add[THEN sym] dist_vec1 vec1_sub[THEN sym] vec1_dest_vec1 norm_vec1 dest_vec1_cmul
- vec1_eq vec1_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def
+lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component
+ vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def
lemma bounded_linear_vec1:"bounded_linear (vec1::real\<Rightarrow>real^1)"
unfolding bounded_linear_def additive_def bounded_linear_axioms_def
@@ -2508,7 +2488,6 @@
lemma linear_vmul_dest_vec1:
fixes f:: "'a::semiring_1^_ \<Rightarrow> 'a^1"
shows "linear f \<Longrightarrow> linear (\<lambda>x. dest_vec1(f x) *s v)"
- unfolding dest_vec1_def
apply (rule linear_vmul_component)
by auto
@@ -2517,14 +2496,14 @@
shows "f = (\<lambda>x. dest_vec1 x *s column 1 (matrix f))"
apply (rule ext)
apply (subst matrix_works[OF lf, symmetric])
- apply (auto simp add: Cart_eq matrix_vector_mult_def dest_vec1_def column_def mult_commute UNIV_1)
+ apply (auto simp add: Cart_eq matrix_vector_mult_def column_def mult_commute UNIV_1)
done
lemma linear_to_scalars: assumes lf: "linear (f::'a::comm_ring_1 ^'n \<Rightarrow> 'a^1)"
shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"
apply (rule ext)
apply (subst matrix_works[OF lf, symmetric])
- apply (simp add: Cart_eq matrix_vector_mult_def vec1_def row_def dot_def mult_commute forall_1)
+ apply (simp add: Cart_eq matrix_vector_mult_def row_def dot_def mult_commute forall_1)
done
lemma dest_vec1_eq_0: "dest_vec1 x = 0 \<longleftrightarrow> x = 0"
@@ -2532,7 +2511,7 @@
lemma setsum_scalars: assumes fS: "finite S"
shows "setsum f S = vec1 (setsum (dest_vec1 o f) S)"
- unfolding vec1_setsum[OF fS] by simp
+ unfolding vec_setsum[OF fS] by simp
lemma dest_vec1_wlog_le: "(\<And>(x::'a::linorder ^ 1) y. P x y \<longleftrightarrow> P y x) \<Longrightarrow> (\<And>x y. dest_vec1 x <= dest_vec1 y ==> P x y) \<Longrightarrow> P x y"
apply (cases "dest_vec1 x \<le> dest_vec1 y")
@@ -2543,10 +2522,10 @@
text{* Pasting vectors. *}
-lemma linear_fstcart: "linear fstcart"
+lemma linear_fstcart[intro]: "linear fstcart"
by (auto simp add: linear_def Cart_eq)
-lemma linear_sndcart: "linear sndcart"
+lemma linear_sndcart[intro]: "linear sndcart"
by (auto simp add: linear_def Cart_eq)
lemma fstcart_vec[simp]: "fstcart(vec x) = vec x"
@@ -2690,7 +2669,7 @@
lemma hull_hull: "S hull (S hull s) = S hull s"
unfolding hull_def by blast
-lemma hull_subset: "s \<subseteq> (S hull s)"
+lemma hull_subset[intro]: "s \<subseteq> (S hull s)"
unfolding hull_def by blast
lemma hull_mono: " s \<subseteq> t ==> (S hull s) \<subseteq> (S hull t)"
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Jan 22 16:59:21 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Mon Jan 25 16:56:24 2010 +0100
@@ -77,13 +77,13 @@
lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \<union> range Inr"
by (auto, case_tac x, auto)
-lemma fstcart_pastecart: "fstcart (pastecart x y) = x"
+lemma fstcart_pastecart[simp]: "fstcart (pastecart x y) = x"
by (simp add: Cart_eq)
-lemma sndcart_pastecart: "sndcart (pastecart x y) = y"
+lemma sndcart_pastecart[simp]: "sndcart (pastecart x y) = y"
by (simp add: Cart_eq)
-lemma pastecart_fst_snd: "pastecart (fstcart z) (sndcart z) = z"
+lemma pastecart_fst_snd[simp]: "pastecart (fstcart z) (sndcart z) = z"
by (simp add: Cart_eq pastecart_def fstcart_def sndcart_def split: sum.split)
lemma pastecart_eq: "(x = y) \<longleftrightarrow> (fstcart x = fstcart y) \<and> (sndcart x = sndcart y)"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jan 22 16:59:21 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Jan 25 16:56:24 2010 +0100
@@ -9,8 +9,6 @@
imports SEQ Euclidean_Space Product_Vector
begin
-declare fstcart_pastecart[simp] sndcart_pastecart[simp]
-
subsection{* General notion of a topology *}
definition "istopology L \<longleftrightarrow> {} \<in> L \<and> (\<forall>S \<in>L. \<forall>T \<in>L. S \<inter> T \<in> L) \<and> (\<forall>K. K \<subseteq>L \<longrightarrow> \<Union> K \<in> L)"
@@ -947,7 +945,7 @@
lemma frontier_subset_closed: "closed S \<Longrightarrow> frontier S \<subseteq> S"
by (metis frontier_def closure_closed Diff_subset)
-lemma frontier_empty: "frontier {} = {}"
+lemma frontier_empty[simp]: "frontier {} = {}"
by (simp add: frontier_def closure_empty)
lemma frontier_subset_eq: "frontier S \<subseteq> S \<longleftrightarrow> closed S"
@@ -1038,7 +1036,7 @@
apply (simp add: norm_sgn)
done
-lemma trivial_limit_sequentially: "\<not> trivial_limit sequentially"
+lemma trivial_limit_sequentially[intro]: "\<not> trivial_limit sequentially"
by (auto simp add: trivial_limit_def Rep_net_sequentially)
subsection{* Some property holds "sufficiently close" to the limit point. *}
@@ -1248,10 +1246,9 @@
lemma Lim_ident_at: "((\<lambda>x. x) ---> a) (at a)"
unfolding tendsto_def Limits.eventually_at_topological by fast
-lemma Lim_const: "((\<lambda>x. a) ---> a) net"
- by (rule tendsto_const)
-
-lemma Lim_cmul:
+lemma Lim_const[intro]: "((\<lambda>x. a) ---> a) net" by (rule tendsto_const)
+
+lemma Lim_cmul[intro]:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
shows "(f ---> l) net ==> ((\<lambda>x. c *\<^sub>R f x) ---> c *\<^sub>R l) net"
by (intro tendsto_intros)
@@ -3417,6 +3414,7 @@
shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x - g x)"
by (auto simp add: continuous_def Lim_sub)
+
text{* Same thing for setwise continuity. *}
lemma continuous_on_const:
@@ -4219,6 +4217,8 @@
==> continuous net (\<lambda>x. c(x) *\<^sub>R f x) "
unfolding continuous_def by (intro tendsto_intros)
+lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul continuous_const continuous_sub continuous_at_id continuous_within_id continuous_mul
+
lemma continuous_on_vmul:
fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
shows "continuous_on s c ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R v)"
@@ -4231,6 +4231,10 @@
==> continuous_on s (\<lambda>x. c(x) *\<^sub>R f x)"
unfolding continuous_on_eq_continuous_within using continuous_mul[of _ c] by auto
+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
+ continuous_on_mul continuous_on_vmul
+
text{* And so we have continuity of inverse. *}
lemma Lim_inv:
@@ -4300,7 +4304,7 @@
using assms(1)[unfolded closed_sequential_limits, THEN spec[where x="\<lambda>n. fstcart (x n)"], THEN spec[where x="fstcart l"]]
using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="\<lambda>n. sndcart (x n)"], THEN spec[where x="sndcart l"]]
unfolding Lim_sequentially by auto
- hence "l \<in> {pastecart x y |x y. x \<in> s \<and> y \<in> t}" using pastecart_fst_snd[THEN sym, of l] by auto }
+ hence "l \<in> {pastecart x y |x y. x \<in> s \<and> y \<in> t}" apply- unfolding mem_Collect_eq apply(rule_tac x="fstcart l" in exI,rule_tac x="sndcart l" in exI) by auto }
thus ?thesis unfolding closed_sequential_limits by auto
qed
@@ -4636,13 +4640,13 @@
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 forall_1)
+by(simp_all add: Cart_eq vector_less_def vector_le_def forall_1)
lemma vec1_interval:fixes a::"real" shows
"vec1 ` {a .. b} = {vec1 a .. vec1 b}"
"vec1 ` {a<..<b} = {vec1 a<..<vec1 b}"
apply(rule_tac[!] set_ext) unfolding image_iff vector_less_def unfolding mem_interval
- unfolding forall_1 unfolding dest_vec1_def[THEN sym, of] unfolding vec1_dest_vec1_simps
+ unfolding forall_1 unfolding vec1_dest_vec1_simps
apply rule defer apply(rule_tac x="dest_vec1 x" in bexI) prefer 3 apply rule defer
apply(rule_tac x="dest_vec1 x" in bexI) by auto
@@ -4800,7 +4804,7 @@
"a < x \<Longrightarrow> x < b ==> (\<exists>d>0. \<forall>x'. abs(x' - x) < d --> a < x' \<and> x' < b)"
by(rule_tac x="min (x - a) (b - x)" in exI, auto)
-lemma open_interval: fixes a :: "real^'n" shows "open {a<..<b}"
+lemma open_interval[intro]: fixes a :: "real^'n" shows "open {a<..<b}"
proof-
{ fix x assume x:"x\<in>{a<..<b}"
{ fix i
@@ -4828,13 +4832,13 @@
thus ?thesis unfolding open_dist using open_interval_lemma by auto
qed
-lemma open_interval_real: fixes a :: "real" shows "open {a<..<b}"
+lemma open_interval_real[intro]: fixes a :: "real" shows "open {a<..<b}"
using open_interval[of "vec1 a" "vec1 b"] unfolding open_contains_ball
apply-apply(rule,erule_tac x="vec1 x" in ballE) apply(erule exE,rule_tac x=e in exI)
unfolding subset_eq mem_ball apply(rule) defer apply(rule,erule conjE,erule_tac x="vec1 xa" in ballE)
by(auto simp add: vec1_dest_vec1_simps vector_less_def forall_1)
-lemma closed_interval: fixes a :: "real^'n" shows "closed {a .. b}"
+lemma closed_interval[intro]: fixes a :: "real^'n" shows "closed {a .. b}"
proof-
{ fix x i assume as:"\<forall>e>0. \<exists>x'\<in>{a..b}. x' \<noteq> x \<and> dist x' x < e"(* and xab:"a$i > x$i \<or> b$i < x$i"*)
{ assume xa:"a$i > x$i"
@@ -4853,7 +4857,7 @@
thus ?thesis unfolding closed_limpt islimpt_approachable mem_interval by auto
qed
-lemma interior_closed_interval: fixes a :: "real^'n" shows
+lemma interior_closed_interval[intro]: fixes a :: "real^'n" shows
"interior {a .. b} = {a<..<b}" (is "?L = ?R")
proof(rule subset_antisym)
show "?R \<subseteq> ?L" using interior_maximal[OF interval_open_subset_closed open_interval] by auto
@@ -5025,25 +5029,19 @@
(* Some special cases for intervals in R^1. *)
-lemma all_1: "(\<forall>x::1. P x) \<longleftrightarrow> P 1"
- by (metis num1_eq_iff)
-
-lemma ex_1: "(\<exists>x::1. P x) \<longleftrightarrow> P 1"
- by auto (metis num1_eq_iff)
-
lemma interval_cases_1: fixes x :: "real^1" shows
"x \<in> {a .. b} ==> x \<in> {a<..<b} \<or> (x = a) \<or> (x = b)"
- by(simp add: Cart_eq vector_less_def vector_le_def all_1, auto)
+ unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq)
lemma in_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) \<and>
(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-by(simp add: Cart_eq vector_less_def vector_le_def all_1 dest_vec1_def)
+ unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq)
lemma interval_eq_empty_1: fixes a :: "real^1" shows
"{a .. b} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a"
"{a<..<b} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a"
- unfolding interval_eq_empty and ex_1 and dest_vec1_def by auto
+ unfolding interval_eq_empty and ex_1 by auto
lemma subset_interval_1: fixes a :: "real^1" shows
"({a .. b} \<subseteq> {c .. d} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or>
@@ -5054,30 +5052,30 @@
dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
"({a<..<b} \<subseteq> {c<..<d} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or>
dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
- unfolding subset_interval[of a b c d] unfolding all_1 and dest_vec1_def by auto
+ unfolding subset_interval[of a b c d] unfolding forall_1 by auto
lemma eq_interval_1: fixes a :: "real^1" shows
"{a .. b} = {c .. d} \<longleftrightarrow>
dest_vec1 b < dest_vec1 a \<and> dest_vec1 d < dest_vec1 c \<or>
dest_vec1 a = dest_vec1 c \<and> dest_vec1 b = dest_vec1 d"
-using set_eq_subset[of "{a .. b}" "{c .. d}"]
-using subset_interval_1(1)[of a b c d]
-using subset_interval_1(1)[of c d a b]
-by auto (* FIXME: slow *)
+unfolding set_eq_subset[of "{a .. b}" "{c .. d}"]
+unfolding subset_interval_1(1)[of a b c d]
+unfolding subset_interval_1(1)[of c d a b]
+by auto
lemma disjoint_interval_1: fixes a :: "real^1" shows
"{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d < dest_vec1 c \<or> dest_vec1 b < dest_vec1 c \<or> dest_vec1 d < dest_vec1 a"
"{a .. b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c \<or> dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
"{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d < dest_vec1 c \<or> dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
"{a<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c \<or> dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
- unfolding disjoint_interval and dest_vec1_def ex_1 by auto
+ unfolding disjoint_interval and ex_1 by auto
lemma open_closed_interval_1: fixes a :: "real^1" shows
"{a<..<b} = {a .. b} - {a, b}"
- unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and all_1 and dest_vec1_eq[THEN sym] and dest_vec1_def by auto
+ unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
lemma closed_open_interval_1: "dest_vec1 (a::real^1) \<le> dest_vec1 b ==> {a .. b} = {a<..<b} \<union> {a,b}"
- unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and all_1 and dest_vec1_eq[THEN sym] and dest_vec1_def by auto
+ unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
(* Some stuff for half-infinite intervals too; FIXME: notation? *)
@@ -5214,11 +5212,11 @@
lemma Lim_drop_le: fixes f :: "'a \<Rightarrow> real^1" shows
"(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. dest_vec1 (f x) \<le> b) net ==> dest_vec1 l \<le> b"
- using Lim_component_le[of f l net 1 b] unfolding dest_vec1_def by auto
+ using Lim_component_le[of f l net 1 b] by auto
lemma Lim_drop_ge: fixes f :: "'a \<Rightarrow> real^1" shows
"(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. b \<le> dest_vec1 (f x)) net ==> b \<le> dest_vec1 l"
- using Lim_component_ge[of f l net b 1] unfolding dest_vec1_def by auto
+ using Lim_component_ge[of f l net b 1] by auto
text{* Limits relative to a union. *}
@@ -5287,7 +5285,7 @@
hence "\<forall>m n. m \<le> n \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)" by auto
then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar>dest_vec1 (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a] unfolding monoseq_def by auto
thus ?thesis unfolding Lim_sequentially apply(rule_tac x="vec1 l" in exI)
- unfolding dist_norm unfolding abs_dest_vec1 and dest_vec1_sub by auto
+ unfolding dist_norm unfolding abs_dest_vec1 by auto
qed
subsection{* Basic homeomorphism definitions. *}