author huffman Thu, 11 Jun 2009 09:03:24 -0700 changeset 31563 ded2364d14d4 parent 31562 10d0fb526643 child 31564 d2abf6f6f619
cleaned up some proofs
```--- a/src/HOL/Library/Product_Vector.thy	Thu Jun 11 08:26:08 2009 -0700
+++ b/src/HOL/Library/Product_Vector.thy	Thu Jun 11 09:03:24 2009 -0700
@@ -102,25 +102,21 @@
instance proof
fix x y :: "'a \<times> 'b"
show "dist x y = 0 \<longleftrightarrow> x = y"
-    unfolding dist_prod_def
+    unfolding dist_prod_def expand_prod_eq by simp
next
fix x y z :: "'a \<times> 'b"
show "dist x y \<le> dist x z + dist y z"
unfolding dist_prod_def
-    apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq])
-    apply (rule real_sqrt_le_mono)
-    apply (rule order_trans [OF add_mono])
-    apply (rule power_mono [OF dist_triangle2 [of _ _ "fst z"] zero_le_dist])
-    apply (rule power_mono [OF dist_triangle2 [of _ _ "snd z"] zero_le_dist])
-    apply (simp only: real_sum_squared_expand)
-    done
+    by (intro order_trans [OF _ real_sqrt_sum_squares_triangle_ineq]
+        real_sqrt_le_mono add_mono power_mono dist_triangle2 zero_le_dist)
next
(* FIXME: long proof! *)
(* Maybe it would be easier to define topological spaces *)
(* in terms of neighborhoods instead of open sets? *)
fix S :: "('a \<times> 'b) set"
show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+  proof
+    assume "open S" thus "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
unfolding open_prod_def open_dist
apply safe
apply (drule (1) bspec)
@@ -136,7 +132,11 @@
apply (erule le_less_trans [OF real_sqrt_sum_squares_ge1])
apply (drule spec, erule mp)
apply (erule le_less_trans [OF real_sqrt_sum_squares_ge2])
-
+    done
+  next
+    assume "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" thus "open S"
+    unfolding open_prod_def open_dist
+    apply safe
apply (drule (1) bspec)
apply clarify
apply (subgoal_tac "\<exists>r>0. \<exists>s>0. e = sqrt (r\<twosuperior> + s\<twosuperior>)")
@@ -147,14 +147,14 @@
apply clarify
apply (rule_tac x="r - dist x a" in exI, rule conjI, simp)
apply clarify
-    apply (rule le_less_trans [OF dist_triangle])
-    apply (erule less_le_trans [OF add_strict_right_mono], simp)
+    apply (erule le_less_trans [OF dist_triangle])
apply (rule conjI)
apply clarify
apply (rule_tac x="s - dist x b" in exI, rule conjI, simp)
apply clarify
-    apply (rule le_less_trans [OF dist_triangle])
-    apply (erule less_le_trans [OF add_strict_right_mono], simp)