--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Feb 27 15:19:09 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Feb 27 16:07:21 2014 +0000
@@ -925,17 +925,10 @@
by (rule subspace_setsum, rule subspace_span)
lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
- apply (auto simp only: span_add span_sub)
- apply (subgoal_tac "(x + y) - x \<in> span S")
- apply simp
- apply (simp only: span_add span_sub)
- done
+ by (metis add_minus_cancel scaleR_minus1_left subspace_def subspace_span)
text {* Mapping under linear image. *}
-lemma image_subset_iff_subset_vimage: "f ` A \<subseteq> B \<longleftrightarrow> A \<subseteq> f -` B"
- by auto (* TODO: move *)
-
lemma span_linear_image:
assumes lf: "linear f"
shows "span (f ` S) = f ` (span S)"
@@ -1271,29 +1264,13 @@
assume i: ?rhs
show ?lhs
using i False
- apply simp
apply (auto simp add: dependent_def)
- apply (case_tac "aa = a")
- apply auto
- apply (subgoal_tac "insert a S - {aa} = insert a (S - {aa})")
- apply simp
- apply (subgoal_tac "a \<in> span (insert aa (S - {aa}))")
- apply (subgoal_tac "insert aa (S - {aa}) = S")
- apply simp
- apply blast
- apply (rule in_span_insert)
- apply assumption
- apply blast
- apply blast
- done
+ by (metis in_span_insert insert_Diff insert_Diff_if insert_iff)
qed
qed
text {* The degenerate case of the Exchange Lemma. *}
-lemma mem_delete: "x \<in> (A - {a}) \<longleftrightarrow> x \<noteq> a \<and> x \<in> A"
- by blast
-
lemma spanning_subset_independent:
assumes BA: "B \<subseteq> A"
and iA: "independent A"
@@ -1345,23 +1322,16 @@
let ?P = "\<lambda>t'. card t' = card t \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
let ?ths = "\<exists>t'. ?P t'"
{
- assume st: "s \<subseteq> t"
- from st ft span_mono[OF st]
- have ?ths
- apply -
- apply (rule exI[where x=t])
- apply (auto intro: span_superset)
- done
+ assume "s \<subseteq> t"
+ then have ?ths
+ by (metis ft Un_commute sp sup_ge1)
}
moreover
{
assume st: "t \<subseteq> s"
from spanning_subset_independent[OF st s sp] st ft span_mono[OF st]
have ?ths
- apply -
- apply (rule exI[where x=t])
- apply (auto intro: span_superset)
- done
+ by (metis Un_absorb sp)
}
moreover
{
@@ -3099,12 +3069,7 @@
unfolding scaleR_scaleR
unfolding norm_scaleR
apply (subgoal_tac "norm x * c = \<bar>c\<bar> * norm x \<or> norm x * c = - \<bar>c\<bar> * norm x")
- apply (case_tac "c \<le> 0", simp add: field_simps)
- apply (simp add: field_simps)
- apply (case_tac "c \<le> 0", simp add: field_simps)
- apply (simp add: field_simps)
- apply simp
- apply simp
+ apply (auto simp add: field_simps)
done
end
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Feb 27 15:19:09 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Feb 27 16:07:21 2014 +0000
@@ -569,10 +569,7 @@
fix K
assume K: "K \<subseteq> Collect ?L"
have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)"
- apply (rule set_eqI)
- apply (simp add: Ball_def image_iff)
- apply metis
- done
+ by blast
from K[unfolded th0 subset_image_iff]
obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk"
by blast
@@ -595,21 +592,11 @@
lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)"
unfolding closedin_def topspace_subtopology
- apply (simp add: openin_subtopology)
- apply (rule iffI)
- apply clarify
- apply (rule_tac x="topspace U - T" in exI)
- apply auto
- done
+ by (auto simp add: openin_subtopology)
lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U"
unfolding openin_subtopology
- apply (rule iffI, clarify)
- apply (frule openin_subset[of U])
- apply blast
- apply (rule exI[where x="topspace U"])
- apply auto
- done
+ by auto (metis IntD1 in_mono openin_subset)
lemma subtopology_superset:
assumes UV: "topspace U \<subseteq> V"
@@ -695,11 +682,7 @@
lemma closed_closedin_trans:
"closed S \<Longrightarrow> closed T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> closedin (subtopology euclidean S) T"
- apply (subgoal_tac "S \<inter> T = T" )
- apply auto
- apply (frule closedin_closed_Int[of T S])
- apply simp
- done
+ by (metis closedin_closed inf.absorb2)
lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
by (auto simp add: closedin_closed)
@@ -720,16 +703,10 @@
apply clarsimp
apply (rule_tac x="d - dist x a" in exI)
apply (clarsimp simp add: less_diff_eq)
- apply (erule rev_bexI)
- apply (rule_tac x=d in exI, clarify)
- apply (erule le_less_trans [OF dist_triangle])
- done
+ by (metis dist_commute dist_triangle_lt)
assume ?rhs then have 2: "S = U \<inter> T"
- unfolding T_def
- apply auto
- apply (drule (1) bspec, erule rev_bexI)
- apply auto
- done
+ unfolding T_def
+ by auto (metis dist_self)
from 1 2 show ?lhs
unfolding openin_open open_dist by fast
qed
@@ -811,12 +788,6 @@
"a - b \<ge> c \<longleftrightarrow> a \<ge> c + b"
by arith+
-lemma open_vimage: (* TODO: move to Topological_Spaces.thy *)
- assumes "open s" and "continuous_on UNIV f"
- shows "open (vimage f s)"
- using assms unfolding continuous_on_open_vimage [OF open_UNIV]
- by simp
-
lemma open_ball [intro, simp]: "open (ball x e)"
proof -
have "open (dist x -` {..<e})"
@@ -955,9 +926,7 @@
e1 \<noteq> {} \<and>
e2 \<noteq> {})"
unfolding connected_def openin_open
- apply safe
- apply blast+
- done
+ by blast
lemma exists_diff:
fixes P :: "'a set \<Rightarrow> bool"
@@ -984,9 +953,7 @@
have "\<not> connected S \<longleftrightarrow>
(\<exists>e1 e2. open e1 \<and> open (- e2) \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
unfolding connected_def openin_open closedin_closed
- apply (subst exists_diff)
- apply blast
- done
+ by (metis double_complement)
then have th0: "connected S \<longleftrightarrow>
\<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
(is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)")
@@ -1430,13 +1397,8 @@
next
assume "\<not> a islimpt S"
then show "trivial_limit (at a within S)"
- unfolding trivial_limit_def
- unfolding eventually_at_topological
- unfolding islimpt_def
- apply clarsimp
- apply (rule_tac x=T in exI)
- apply auto
- done
+ unfolding trivial_limit_def eventually_at_topological islimpt_def
+ by metis
qed
lemma trivial_limit_at_iff: "trivial_limit (at a) \<longleftrightarrow> \<not> a islimpt UNIV"
@@ -1926,9 +1888,7 @@
lemma closed_sequential_limits:
fixes S :: "'a::first_countable_topology set"
shows "closed S \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially \<longrightarrow> l \<in> S)"
- using closure_sequential [where 'a='a] closure_closed [where 'a='a]
- closed_limpt [where 'a='a] islimpt_sequential [where 'a='a] mem_delete [where 'a='a]
- by metis
+by (metis closure_sequential closure_subset_eq subset_iff)
lemma closure_approachable:
fixes S :: "'a::metric_space set"
@@ -2483,13 +2443,7 @@
lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
unfolding bounded_def
- apply safe
- apply (rule_tac x="dist a x + e" in exI)
- apply clarify
- apply (drule (1) bspec)
- apply (erule order_trans [OF dist_triangle add_left_mono])
- apply auto
- done
+ by auto (metis add_commute add_le_cancel_right dist_commute dist_triangle_le)
lemma bounded_iff: "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. norm x \<le> a)"
unfolding bounded_any_center [where a=0]
@@ -2499,10 +2453,7 @@
assumes "\<forall>x\<in>s. abs (x::real) \<le> B"
shows "bounded s"
unfolding bounded_def dist_real_def
- apply (rule_tac x=0 in exI)
- using assms
- apply auto
- done
+ by (metis abs_minus_commute assms diff_0_right)
lemma bounded_empty [simp]: "bounded {}"
by (simp add: bounded_def)
@@ -2550,17 +2501,7 @@
lemma bounded_Un[simp]: "bounded (S \<union> T) \<longleftrightarrow> bounded S \<and> bounded T"
apply (auto simp add: bounded_def)
- apply (rename_tac x y r s)
- apply (rule_tac x=x in exI)
- apply (rule_tac x="max r (dist x y + s)" in exI)
- apply (rule ballI)
- apply safe
- apply (drule (1) bspec)
- apply simp
- apply (drule (1) bspec)
- apply (rule max.coboundedI2)
- apply (erule order_trans [OF dist_triangle add_left_mono])
- done
+ by (metis Un_iff add_le_cancel_left dist_triangle le_max_iff_disj max.order_iff)
lemma bounded_Union[intro]: "finite F \<Longrightarrow> \<forall>S\<in>F. bounded S \<Longrightarrow> bounded (\<Union>F)"
by (induct rule: finite_induct[of F]) auto
@@ -3847,25 +3788,11 @@
lemma bounded_fst: "bounded s \<Longrightarrow> bounded (fst ` s)"
unfolding bounded_def
- apply clarify
- apply (rule_tac x="a" in exI)
- apply (rule_tac x="e" in exI)
- apply clarsimp
- apply (drule (1) bspec)
- apply (simp add: dist_Pair_Pair)
- apply (erule order_trans [OF real_sqrt_sum_squares_ge1])
- done
+ by (metis (erased, hide_lams) dist_fst_le image_iff order_trans)
lemma bounded_snd: "bounded s \<Longrightarrow> bounded (snd ` s)"
unfolding bounded_def
- apply clarify
- apply (rule_tac x="b" in exI)
- apply (rule_tac x="e" in exI)
- apply clarsimp
- apply (drule (1) bspec)
- apply (simp add: dist_Pair_Pair)
- apply (erule order_trans [OF real_sqrt_sum_squares_ge2])
- done
+ by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans)
instance prod :: (heine_borel, heine_borel) heine_borel
proof
@@ -3916,7 +3843,6 @@
using assms unfolding compact_def by blast
note lr' = seq_suble [OF lr(2)]
-
{
fix e :: real
assume "e > 0"
@@ -4434,10 +4360,8 @@
"continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s. dist x' x < d --> dist (f x') (f x) < e)"
unfolding continuous_within and Lim_within
apply auto
- unfolding dist_nz[symmetric]
- apply (auto del: allE elim!:allE)
- apply(rule_tac x=d in exI)
- apply auto
+ apply (metis dist_nz dist_self)
+ apply blast
done
lemma continuous_at_eps_delta:
@@ -4521,11 +4445,7 @@
"continuous_on s f \<longleftrightarrow>
(\<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
unfolding continuous_on_def Lim_within
- apply (intro ball_cong [OF refl] all_cong ex_cong)
- apply (rename_tac y, case_tac "y = x")
- apply simp
- apply (simp add: dist_nz)
- done
+ by (metis dist_pos_lt dist_self)
definition uniformly_continuous_on :: "'a set \<Rightarrow> ('a::metric_space \<Rightarrow> 'b::metric_space) \<Rightarrow> bool"
where "uniformly_continuous_on s f \<longleftrightarrow>
@@ -4552,10 +4472,7 @@
lemma continuous_on_interior:
"continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
- apply (erule interiorE)
- apply (drule (1) continuous_on_subset)
- apply (simp add: continuous_on_eq_continuous_at)
- done
+ by (metis continuous_on_eq_continuous_at continuous_on_subset interiorE)
lemma continuous_on_eq:
"(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
--- a/src/HOL/Set.thy Thu Feb 27 15:19:09 2014 +0100
+++ b/src/HOL/Set.thy Thu Feb 27 16:07:21 2014 +0000
@@ -1763,6 +1763,9 @@
lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f"
by blast
+lemma image_subset_iff_subset_vimage: "f ` A \<subseteq> B \<longleftrightarrow> A \<subseteq> f -` B"
+ by blast
+
lemma vimage_const [simp]: "((\<lambda>x. c) -` A) = (if c \<in> A then UNIV else {})"
by auto
--- a/src/HOL/Topological_Spaces.thy Thu Feb 27 15:19:09 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy Thu Feb 27 16:07:21 2014 +0000
@@ -1711,6 +1711,12 @@
shows "open (f -` B)"
by (metis assms continuous_on_open_vimage le_iff_inf)
+corollary open_vimage:
+ assumes "open s" and "continuous_on UNIV f"
+ shows "open (f -` s)"
+ using assms unfolding continuous_on_open_vimage [OF open_UNIV]
+ by simp
+
lemma continuous_on_closed_invariant:
"continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> (\<exists>A. closed A \<and> A \<inter> s = f -` B \<inter> s))"
proof -