# HG changeset patch # User huffman # Date 1244775895 25200 # Node ID fd09da74183392de9e40ef9f835e2286f0cef730 # Parent 784decc70e07679eb90082dec396b8ebe91bf77d move lemma compact_Times; generalize more lemmas diff -r 784decc70e07 -r fd09da741833 src/HOL/Library/Convex_Euclidean_Space.thy --- a/src/HOL/Library/Convex_Euclidean_Space.thy Thu Jun 11 19:44:39 2009 -0700 +++ b/src/HOL/Library/Convex_Euclidean_Space.thy Thu Jun 11 20:04:55 2009 -0700 @@ -1228,27 +1228,6 @@ lemma continuous_dest_vec1: "continuous net f \ continuous net (\x. dest_vec1 (f x))" unfolding continuous_def by (rule tendsto_dest_vec1) -lemma mem_Times_iff: "x \ A \ B \ fst x \ A \ snd x \ B" -by (induct x) simp - -(* TODO: move *) -lemma compact_Times: "compact s \ compact t \ compact (s \ t)" -unfolding compact_def -apply clarify -apply (drule_tac x="fst \ f" in spec) -apply (drule mp, simp add: mem_Times_iff) -apply (clarify, rename_tac l1 r1) -apply (drule_tac x="snd \ f \ r1" in spec) -apply (drule mp, simp add: mem_Times_iff) -apply (clarify, rename_tac l2 r2) -apply (rule_tac x="(l1, l2)" in rev_bexI, simp) -apply (rule_tac x="r1 \ r2" in exI) -apply (rule conjI, simp add: subseq_def) -apply (drule_tac r=r2 in lim_subseq [COMP swap_prems_rl], assumption) -apply (drule (1) tendsto_Pair) back -apply (simp add: o_def) -done - (* TODO: move *) lemma compact_real_interval: fixes a b :: real shows "compact {a..b}" diff -r 784decc70e07 -r fd09da741833 src/HOL/Library/Topology_Euclidean_Space.thy --- a/src/HOL/Library/Topology_Euclidean_Space.thy Thu Jun 11 19:44:39 2009 -0700 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy Thu Jun 11 20:04:55 2009 -0700 @@ -4344,11 +4344,25 @@ shows "compact s \ compact t ==> compact {pastecart x y | x y . x \ s \ y \ t}" unfolding compact_eq_bounded_closed using bounded_pastecart[of s t] closed_pastecart[of s t] by auto -lemma compact_Times: - fixes s t :: "'a::heine_borel set" - shows "compact s \ compact t \ compact (s \ t)" - unfolding compact_eq_bounded_closed - using bounded_Times [of s t] closed_Times [of s t] by auto +lemma mem_Times_iff: "x \ A \ B \ fst x \ A \ snd x \ B" +by (induct x) simp + +lemma compact_Times: "compact s \ compact t \ compact (s \ t)" +unfolding compact_def +apply clarify +apply (drule_tac x="fst \ f" in spec) +apply (drule mp, simp add: mem_Times_iff) +apply (clarify, rename_tac l1 r1) +apply (drule_tac x="snd \ f \ r1" in spec) +apply (drule mp, simp add: mem_Times_iff) +apply (clarify, rename_tac l2 r2) +apply (rule_tac x="(l1, l2)" in rev_bexI, simp) +apply (rule_tac x="r1 \ r2" in exI) +apply (rule conjI, simp add: subseq_def) +apply (drule_tac r=r2 in lim_subseq [COMP swap_prems_rl], assumption) +apply (drule (1) tendsto_Pair) back +apply (simp add: o_def) +done text{* Hence some useful properties follow quite easily. *} @@ -4373,7 +4387,7 @@ using compact_scaleR_image [OF assms, of "- 1"] by auto lemma compact_sums: - fixes s t :: "'a::{heine_borel, real_normed_vector} set" + fixes s t :: "'a::real_normed_vector set" assumes "compact s" "compact t" shows "compact {x + y | x y. x \ s \ y \ t}" proof- have *:"{x + y | x y. x \ s \ y \ t} = (\z. fst z + snd z) ` (s \ t)" @@ -4384,7 +4398,7 @@ qed lemma compact_differences: - fixes s t :: "'a::{heine_borel, real_normed_vector} set" + fixes s t :: "'a::real_normed_vector set" assumes "compact s" "compact t" shows "compact {x - y | x y. x \ s \ y \ t}" proof- have "{x - y | x y. x\s \ y \ t} = {x + y | x y. x \ s \ y \ (uminus ` t)}" @@ -4393,7 +4407,7 @@ qed lemma compact_translation: - fixes s :: "'a::{heine_borel, real_normed_vector} set" + fixes s :: "'a::real_normed_vector set" assumes "compact s" shows "compact ((\x. a + x) ` s)" proof- have "{x + y |x y. x \ s \ y \ {a}} = (\x. a + x) ` s" by auto @@ -4411,7 +4425,7 @@ text{* Hence we get the following. *} lemma compact_sup_maxdistance: - fixes s :: "'a::{heine_borel, real_normed_vector} set" + fixes s :: "'a::real_normed_vector set" assumes "compact s" "s \ {}" shows "\x\s. \y\s. \u\s. \v\s. norm(u - v) \ norm(x - y)" proof- @@ -4462,11 +4476,11 @@ using diameter_bounded by blast lemma diameter_compact_attained: - fixes s :: "'a::{heine_borel, real_normed_vector} set" + fixes s :: "'a::real_normed_vector set" assumes "compact s" "s \ {}" shows "\x\s. \y\s. (norm(x - y) = diameter s)" proof- - have b:"bounded s" using assms(1) compact_eq_bounded_closed by auto + have b:"bounded s" using assms(1) by (rule compact_imp_bounded) then obtain x y where xys:"x\s" "y\s" and xy:"\u\s. \v\s. norm (u - v) \ norm (x - y)" using compact_sup_maxdistance[OF assms] by auto hence "diameter s \ norm (x - y)" using rsup_le[of "{norm (x - y) |x y. x \ s \ y \ s}" "norm (x - y)"] unfolding setle_def and diameter_def by auto @@ -5945,7 +5959,7 @@ subsection{* Edelstein fixed point theorem. *} lemma edelstein_fix: - fixes s :: "'a::{heine_borel, real_normed_vector} set" + fixes s :: "'a::real_normed_vector set" assumes s:"compact s" "s \ {}" and gs:"(g ` s) \ s" and dist:"\x\s. \y\s. x \ y \ dist (g x) (g y) < dist x y" shows "\! x\s. g x = x"