--- 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
- by (simp add: expand_prod_eq)
+ 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 (simp add: less_diff_eq)
+ 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)
+ apply (simp add: less_diff_eq)
+ apply (erule le_less_trans [OF dist_triangle])
apply (rule conjI)
apply simp
apply (clarify, rename_tac c d)
@@ -164,6 +164,7 @@
apply (rule_tac x="e / sqrt 2" in exI, simp add: divide_pos_pos)
apply (simp add: power_divide)
done
+ qed
qed
end