summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | huffman |

Thu, 26 Sep 2013 08:44:43 -0700 | |

changeset 53930 | 896b642f2aab |

parent 53929 | 8c5aaf557421 |

child 53937 | f95765a28b1d |

tuned proofs

--- 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"