# HG changeset patch
# User huffman
# Date 1380210283 25200
# Node ID 896b642f2aab594fa49c2f71cc8a356443fce37e
# Parent  8c5aaf55742142c7a19c767539ec15a819804bb3
tuned proofs

diff -r 8c5aaf557421 -r 896b642f2aab src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Thu Sep 26 17:24:15 2013 +0200
+++ b/src/HOL/Library/Product_Vector.thy	Thu Sep 26 08:44:43 2013 -0700
@@ -231,12 +231,7 @@
   hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
     by (simp add: prod_eq_iff)
   thus "\<exists>U. open U \<and> (x \<in> U) \<noteq> (y \<in> U)"
-    apply (rule disjE)
-    apply (drule t0_space, erule exE, rule_tac x="U \<times> UNIV" in exI)
-    apply (simp add: open_Times mem_Times_iff)
-    apply (drule t0_space, erule exE, rule_tac x="UNIV \<times> U" in exI)
-    apply (simp add: open_Times mem_Times_iff)
-    done
+    by (fast dest: t0_space elim: open_vimage_fst open_vimage_snd)
 qed
 
 instance prod :: (t1_space, t1_space) t1_space
@@ -245,12 +240,7 @@
   hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
     by (simp add: prod_eq_iff)
   thus "\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
-    apply (rule disjE)
-    apply (drule t1_space, erule exE, rule_tac x="U \<times> UNIV" in exI)
-    apply (simp add: open_Times mem_Times_iff)
-    apply (drule t1_space, erule exE, rule_tac x="UNIV \<times> U" in exI)
-    apply (simp add: open_Times mem_Times_iff)
-    done
+    by (fast dest: t1_space elim: open_vimage_fst open_vimage_snd)
 qed
 
 instance prod :: (t2_space, t2_space) t2_space
@@ -259,14 +249,7 @@
   hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
     by (simp add: prod_eq_iff)
   thus "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
-    apply (rule disjE)
-    apply (drule hausdorff, clarify)
-    apply (rule_tac x="U \<times> UNIV" in exI, rule_tac x="V \<times> UNIV" in exI)
-    apply (simp add: open_Times mem_Times_iff disjoint_iff_not_equal)
-    apply (drule hausdorff, clarify)
-    apply (rule_tac x="UNIV \<times> U" in exI, rule_tac x="UNIV \<times> V" in exI)
-    apply (simp add: open_Times mem_Times_iff disjoint_iff_not_equal)
-    done
+    by (fast dest: hausdorff elim: open_vimage_fst open_vimage_snd)
 qed
 
 subsection {* Product is a metric space *}
@@ -281,10 +264,10 @@
   unfolding dist_prod_def by simp
 
 lemma dist_fst_le: "dist (fst x) (fst y) \<le> dist x y"
-unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge1)
+  unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge1)
 
 lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y"
-unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2)
+  unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2)
 
 instance proof
   fix x y :: "'a \<times> 'b"
@@ -362,10 +345,10 @@
 end
 
 lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
-unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
+  unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
 
 lemma Cauchy_snd: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. snd (X n))"
-unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_snd_le])
+  unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_snd_le])
 
 lemma Cauchy_Pair:
   assumes "Cauchy X" and "Cauchy Y"