# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1393517241 0
# Node ID 1557a391a8584729c71e11b591bfacdd523de134
# Parent  f13a762f7d9695bac3a1e398b9d93bc71bceff26
A bit of tidying up

diff -r f13a762f7d96 -r 1557a391a858 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- 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
diff -r f13a762f7d96 -r 1557a391a858 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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"
diff -r f13a762f7d96 -r 1557a391a858 src/HOL/Set.thy
--- 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
 
diff -r f13a762f7d96 -r 1557a391a858 src/HOL/Topological_Spaces.thy
--- 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 -