# HG changeset patch # User wenzelm # Date 1358277721 -3600 # Node ID 8226f9a1273abf60f6669205305f6e9ffe4961bc # Parent ebd9b82537e08f9babe581120e60f11202eadaa9# Parent cb2b940e2fdf429827ccb1f49a6d42ec9190a4be merged diff -r cb2b940e2fdf -r 8226f9a1273a src/HOL/IMP/Abs_Int0.thy --- a/src/HOL/IMP/Abs_Int0.thy Tue Jan 15 17:28:46 2013 +0100 +++ b/src/HOL/IMP/Abs_Int0.thy Tue Jan 15 20:22:01 2013 +0100 @@ -242,9 +242,9 @@ and gamma_Top[simp]: "\ \ = UNIV" fixes num' :: "val \ 'av" and plus' :: "'av \ 'av \ 'av" - assumes gamma_num': "n : \(num' n)" + assumes gamma_num': "i : \(num' i)" and gamma_plus': - "n1 : \ a1 \ n2 : \ a2 \ n1+n2 : \(plus' a1 a2)" + "i1 : \ a1 \ i2 : \ a2 \ i1+i2 : \(plus' a1 a2)" type_synonym 'av st = "(vname \ 'av)" @@ -252,7 +252,7 @@ begin fun aval' :: "aexp \ 'av st \ 'av" where -"aval' (N n) S = num' n" | +"aval' (N i) S = num' i" | "aval' (V x) S = S x" | "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" diff -r cb2b940e2fdf -r 8226f9a1273a src/HOL/IMP/Abs_Int1.thy --- a/src/HOL/IMP/Abs_Int1.thy Tue Jan 15 17:28:46 2013 +0100 +++ b/src/HOL/IMP/Abs_Int1.thy Tue Jan 15 20:22:01 2013 +0100 @@ -44,7 +44,7 @@ begin fun aval' :: "aexp \ 'av st \ 'av" where -"aval' (N n) S = num' n" | +"aval' (N i) S = num' i" | "aval' (V x) S = fun S x" | "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" diff -r cb2b940e2fdf -r 8226f9a1273a src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Jan 15 17:28:46 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Jan 15 20:22:01 2013 +0100 @@ -917,21 +917,8 @@ ultimately show ?case by blast qed -lemma islimpt_finite: - fixes S :: "'a::metric_space set" - assumes fS: "finite S" shows "\ a islimpt S" - unfolding islimpt_approachable - using finite_set_avoid[OF fS, of a] by (metis dist_commute not_le) - lemma islimpt_Un: "x islimpt (S \ T) \ x islimpt S \ x islimpt T" - apply (rule iffI) - defer - apply (metis Un_upper1 Un_upper2 islimpt_subset) - unfolding islimpt_def - apply (rule ccontr, clarsimp, rename_tac A B) - apply (drule_tac x="A \ B" in spec) - apply (auto simp add: open_Int) - done + by (simp add: islimpt_iff_eventually eventually_conj_iff) lemma discrete_imp_closed: fixes S :: "'a::metric_space set" @@ -2352,6 +2339,16 @@ compact_eq_heine_borel: -- "This name is used for backwards compatibility" "compact S \ (\C. (\c\C. open c) \ S \ \C \ (\D\C. finite D \ S \ \D))" +lemma compactI: + assumes "\C. \t\C. open t \ s \ \ C \ \C'. C' \ C \ finite C' \ s \ \ C'" + shows "compact s" + unfolding compact_eq_heine_borel using assms by metis + +lemma compactE: + assumes "compact s" and "\t\C. open t" and "s \ \C" + obtains C' where "C' \ C" and "finite C'" and "s \ \C'" + using assms unfolding compact_eq_heine_borel by metis + subsubsection {* Bolzano-Weierstrass property *} lemma heine_borel_imp_bolzano_weierstrass: @@ -2497,11 +2494,16 @@ by (rule islimpt_subset) auto qed +lemma islimpt_finite: + fixes x :: "'a::t1_space" + shows "finite s \ \ x islimpt s" +by (induct set: finite, simp_all add: islimpt_insert) + lemma islimpt_union_finite: fixes x :: "'a::t1_space" shows "finite s \ x islimpt (s \ t) \ x islimpt t" -by (induct set: finite, simp_all add: islimpt_insert) - +by (simp add: islimpt_Un islimpt_finite) + lemma sequence_unique_limpt: fixes f :: "nat \ 'a::t2_space" assumes "(f ---> l) sequentially" and "l' islimpt (range f)" @@ -2545,14 +2547,32 @@ qed lemma compact_imp_closed: - fixes s :: "'a::{first_countable_topology, t2_space} set" - shows "compact s \ closed s" -proof - - assume "compact s" - hence "\t. infinite t \ t \ s \ (\x \ s. x islimpt t)" - using heine_borel_imp_bolzano_weierstrass[of s] by auto - thus "closed s" - by (rule bolzano_weierstrass_imp_closed) + fixes s :: "'a::t2_space set" + assumes "compact s" shows "closed s" +unfolding closed_def +proof (rule openI) + fix y assume "y \ - s" + let ?C = "\x\s. {u. open u \ x \ u \ eventually (\y. y \ u) (nhds y)}" + note `compact s` + moreover have "\u\?C. open u" by simp + moreover have "s \ \?C" + proof + fix x assume "x \ s" + with `y \ - s` have "x \ y" by clarsimp + hence "\u v. open u \ open v \ x \ u \ y \ v \ u \ v = {}" + by (rule hausdorff) + with `x \ s` show "x \ \?C" + unfolding eventually_nhds by auto + qed + ultimately obtain D where "D \ ?C" and "finite D" and "s \ \D" + by (rule compactE) + from `D \ ?C` have "\x\D. eventually (\y. y \ x) (nhds y)" by auto + with `finite D` have "eventually (\y. y \ \D) (nhds y)" + by (simp add: eventually_Ball_finite) + with `s \ \D` have "eventually (\y. y \ s) (nhds y)" + by (auto elim!: eventually_mono [rotated]) + thus "\t. open t \ y \ t \ t \ - s" + by (simp add: eventually_nhds subset_eq) qed text{* In particular, some common special cases. *} @@ -2564,9 +2584,8 @@ lemma compact_union [intro]: assumes "compact s" "compact t" shows " compact (s \ t)" - unfolding compact_eq_heine_borel -proof (intro allI impI) - fix f assume *: "Ball f open \ s \ t \ \f" +proof (rule compactI) + fix f assume *: "Ball f open" "s \ t \ \f" from * `compact s` obtain s' where "s' \ f \ finite s' \ s \ \s'" unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis moreover from * `compact t` obtain t' where "t' \ f \ finite t' \ t \ \t'" @@ -2585,8 +2604,7 @@ lemma compact_inter_closed [intro]: assumes "compact s" and "closed t" shows "compact (s \ t)" - unfolding compact_eq_heine_borel -proof safe +proof (rule compactI) fix C assume C: "\c\C. open c" and cover: "s \ t \ \C" from C `closed t` have "\c\C \ {-t}. open c" by auto moreover from cover have "s \ \(C \ {-t})" by auto @@ -2604,7 +2622,7 @@ by (simp add: Int_commute) lemma compact_inter [intro]: - fixes s t :: "'a :: {t2_space, first_countable_topology} set" + fixes s t :: "'a :: t2_space set" assumes "compact s" and "compact t" shows "compact (s \ t)" using assms by (intro compact_inter_closed compact_imp_closed) @@ -4629,35 +4647,41 @@ text {* Making a continuous function avoid some value in a neighbourhood. *} lemma continuous_within_avoid: - fixes f :: "'a::metric_space \ 'b::metric_space" (* FIXME: generalize *) - assumes "continuous (at x within s) f" "x \ s" "f x \ a" + fixes f :: "'a::metric_space \ 'b::t1_space" + assumes "continuous (at x within s) f" and "f x \ a" shows "\e>0. \y \ s. dist x y < e --> f y \ a" proof- - obtain d where "d>0" and d:"\xa\s. 0 < dist xa x \ dist xa x < d \ dist (f xa) (f x) < dist (f x) a" - using assms(1)[unfolded continuous_within Lim_within, THEN spec[where x="dist (f x) a"]] assms(3)[unfolded dist_nz] by auto - { fix y assume " y\s" "dist x y < d" - hence "f y \ a" using d[THEN bspec[where x=y]] assms(3)[unfolded dist_nz] - apply auto unfolding dist_nz[THEN sym] by (auto simp add: dist_commute) } - thus ?thesis using `d>0` by auto + obtain U where "open U" and "f x \ U" and "a \ U" + using t1_space [OF `f x \ a`] by fast + have "(f ---> f x) (at x within s)" + using assms(1) by (simp add: continuous_within) + hence "eventually (\y. f y \ U) (at x within s)" + using `open U` and `f x \ U` + unfolding tendsto_def by fast + hence "eventually (\y. f y \ a) (at x within s)" + using `a \ U` by (fast elim: eventually_mono [rotated]) + thus ?thesis + unfolding Limits.eventually_within Limits.eventually_at + by (rule ex_forward, cut_tac `f x \ a`, auto simp: dist_commute) qed lemma continuous_at_avoid: - fixes f :: "'a::metric_space \ 'b::metric_space" (* FIXME: generalize *) + fixes f :: "'a::metric_space \ 'b::t1_space" assumes "continuous (at x) f" and "f x \ a" shows "\e>0. \y. dist x y < e \ f y \ a" using assms continuous_within_avoid[of x UNIV f a] by simp lemma continuous_on_avoid: - fixes f :: "'a::metric_space \ 'b::metric_space" (* TODO: generalize *) + fixes f :: "'a::metric_space \ 'b::t1_space" assumes "continuous_on s f" "x \ s" "f x \ a" shows "\e>0. \y \ s. dist x y < e \ f y \ a" -using assms(1)[unfolded continuous_on_eq_continuous_within, THEN bspec[where x=x], OF assms(2)] continuous_within_avoid[of x s f a] assms(2,3) by auto +using assms(1)[unfolded continuous_on_eq_continuous_within, THEN bspec[where x=x], OF assms(2)] continuous_within_avoid[of x s f a] assms(3) by auto lemma continuous_on_open_avoid: - fixes f :: "'a::metric_space \ 'b::metric_space" (* TODO: generalize *) + fixes f :: "'a::metric_space \ 'b::t1_space" assumes "continuous_on s f" "open s" "x \ s" "f x \ a" shows "\e>0. \y. dist x y < e \ f y \ a" -using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)] continuous_at_avoid[of x f a] assms(3,4) by auto +using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)] continuous_at_avoid[of x f a] assms(4) by auto text {* Proving a function is constant by proving open-ness of level set. *} @@ -4798,23 +4822,83 @@ text {* Preservation of compactness and connectedness under continuous function. *} +lemma compact_eq_openin_cover: + "compact S \ + (\C. (\c\C. openin (subtopology euclidean S) c) \ S \ \C \ + (\D\C. finite D \ S \ \D))" +proof safe + fix C + assume "compact S" and "\c\C. openin (subtopology euclidean S) c" and "S \ \C" + hence "\c\{T. open T \ S \ T \ C}. open c" and "S \ \{T. open T \ S \ T \ C}" + unfolding openin_open by force+ + with `compact S` obtain D where "D \ {T. open T \ S \ T \ C}" and "finite D" and "S \ \D" + by (rule compactE) + hence "image (\T. S \ T) D \ C \ finite (image (\T. S \ T) D) \ S \ \(image (\T. S \ T) D)" + by auto + thus "\D\C. finite D \ S \ \D" .. +next + assume 1: "\C. (\c\C. openin (subtopology euclidean S) c) \ S \ \C \ + (\D\C. finite D \ S \ \D)" + show "compact S" + proof (rule compactI) + fix C + let ?C = "image (\T. S \ T) C" + assume "\t\C. open t" and "S \ \C" + hence "(\c\?C. openin (subtopology euclidean S) c) \ S \ \?C" + unfolding openin_open by auto + with 1 obtain D where "D \ ?C" and "finite D" and "S \ \D" + by metis + let ?D = "inv_into C (\T. S \ T) ` D" + have "?D \ C \ finite ?D \ S \ \?D" + proof (intro conjI) + from `D \ ?C` show "?D \ C" + by (fast intro: inv_into_into) + from `finite D` show "finite ?D" + by (rule finite_imageI) + from `S \ \D` show "S \ \?D" + apply (rule subset_trans) + apply clarsimp + apply (frule subsetD [OF `D \ ?C`, THEN f_inv_into_f]) + apply (erule rev_bexI, fast) + done + qed + thus "\D\C. finite D \ S \ \D" .. + qed +qed + lemma compact_continuous_image: - fixes f :: "'a :: metric_space \ 'b :: metric_space" - assumes "continuous_on s f" "compact s" - shows "compact(f ` s)" -proof- - { fix x assume x:"\n::nat. x n \ f ` s" - then obtain y where y:"\n. y n \ s \ x n = f (y n)" unfolding image_iff Bex_def using choice[of "\n xa. xa \ s \ x n = f xa"] by auto - then obtain l r where "l\s" and r:"subseq r" and lr:"((y \ r) ---> l) sequentially" using assms(2)[unfolded compact_def, THEN spec[where x=y]] by auto - { fix e::real assume "e>0" - then obtain d where "d>0" and d:"\x'\s. dist x' l < d \ dist (f x') (f l) < e" - using assms(1)[unfolded continuous_on_iff, THEN bspec[where x=l], OF `l\s`] by auto - then obtain N::nat where N:"\n\N. dist ((y \ r) n) l < d" using lr[unfolded LIMSEQ_def, THEN spec[where x=d]] by auto - { fix n::nat assume "n\N" hence "dist ((x \ r) n) (f l) < e" using N[THEN spec[where x=n]] d[THEN bspec[where x="y (r n)"]] y[THEN spec[where x="r n"]] by auto } - hence "\N. \n\N. dist ((x \ r) n) (f l) < e" by auto } - hence "\l\f ` s. \r. subseq r \ ((x \ r) ---> l) sequentially" unfolding LIMSEQ_def using r lr `l\s` by auto } - thus ?thesis unfolding compact_def by auto -qed + assumes "continuous_on s f" and "compact s" + shows "compact (f ` s)" +using assms (* FIXME: long unstructured proof *) +unfolding continuous_on_open +unfolding compact_eq_openin_cover +apply clarify +apply (drule_tac x="image (\t. {x \ s. f x \ t}) C" in spec) +apply (drule mp) +apply (rule conjI) +apply simp +apply clarsimp +apply (drule subsetD) +apply (erule imageI) +apply fast +apply (erule thin_rl) +apply clarify +apply (rule_tac x="image (inv_into C (\t. {x \ s. f x \ t})) D" in exI) +apply (intro conjI) +apply clarify +apply (rule inv_into_into) +apply (erule (1) subsetD) +apply (erule finite_imageI) +apply (clarsimp, rename_tac x) +apply (drule (1) subsetD, clarify) +apply (drule (1) subsetD, clarify) +apply (rule rev_bexI) +apply assumption +apply (subgoal_tac "{x \ s. f x \ t} \ (\t. {x \ s. f x \ t}) ` C") +apply (drule f_inv_into_f) +apply fast +apply (erule imageI) +done lemma connected_continuous_image: assumes "continuous_on s f" "connected s" @@ -4870,25 +4954,33 @@ text{* Continuity of inverse function on compact domain. *} lemma continuous_on_inv: - fixes f :: "'a::heine_borel \ 'b::heine_borel" - (* TODO: can this be generalized more? *) + fixes f :: "'a::topological_space \ 'b::t2_space" assumes "continuous_on s f" "compact s" "\x \ s. g (f x) = x" shows "continuous_on (f ` s) g" -proof- - have *:"g ` f ` s = s" using assms(3) by (auto simp add: image_iff) - { fix t assume t:"closedin (subtopology euclidean (g ` f ` s)) t" - then obtain T where T: "closed T" "t = s \ T" unfolding closedin_closed unfolding * by auto - have "continuous_on (s \ T) f" using continuous_on_subset[OF assms(1), of "s \ t"] - unfolding T(2) and Int_left_absorb by auto - moreover have "compact (s \ T)" - using assms(2) unfolding compact_eq_bounded_closed - using bounded_subset[of s "s \ T"] and T(1) by auto - ultimately have "closed (f ` t)" using T(1) unfolding T(2) - using compact_continuous_image [of "s \ T" f] unfolding compact_eq_bounded_closed by auto - moreover have "{x \ f ` s. g x \ t} = f ` s \ f ` t" using assms(3) unfolding T(2) by auto - ultimately have "closedin (subtopology euclidean (f ` s)) {x \ f ` s. g x \ t}" - unfolding closedin_closed by auto } - thus ?thesis unfolding continuous_on_closed by auto +unfolding continuous_on_topological +proof (clarsimp simp add: assms(3)) + fix x :: 'a and B :: "'a set" + assume "x \ s" and "open B" and "x \ B" + have 1: "\x\s. f x \ f ` (s - B) \ x \ s - B" + using assms(3) by (auto, metis) + have "continuous_on (s - B) f" + using `continuous_on s f` Diff_subset + by (rule continuous_on_subset) + moreover have "compact (s - B)" + using `open B` and `compact s` + unfolding Diff_eq by (intro compact_inter_closed closed_Compl) + ultimately have "compact (f ` (s - B))" + by (rule compact_continuous_image) + hence "closed (f ` (s - B))" + by (rule compact_imp_closed) + hence "open (- f ` (s - B))" + by (rule open_Compl) + moreover have "f x \ - f ` (s - B)" + using `x \ s` and `x \ B` by (simp add: 1) + moreover have "\y\s. f y \ - f ` (s - B) \ y \ B" + by (simp add: 1) + ultimately show "\A. open A \ f x \ A \ (\y\s. f y \ A \ y \ B)" + by fast qed text {* A uniformly convergent limit of continuous functions is continuous. *} @@ -6051,7 +6143,7 @@ (\y\t. (f(g y) = y)) \ (g ` t = s) \ continuous_on t g" definition - homeomorphic :: "'a::metric_space set \ 'b::metric_space set \ bool" + homeomorphic :: "'a::topological_space set \ 'b::topological_space set \ bool" (infixr "homeomorphic" 60) where homeomorphic_def: "s homeomorphic t \ (\f g. homeomorphism s t f g)" @@ -6103,8 +6195,7 @@ text {* Relatively weak hypotheses if a set is compact. *} lemma homeomorphism_compact: - fixes f :: "'a::heine_borel \ 'b::heine_borel" - (* class constraint due to continuous_on_inv *) + fixes f :: "'a::topological_space \ 'b::t2_space" assumes "compact s" "continuous_on s f" "f ` s = t" "inj_on f s" shows "\g. homeomorphism s t f g" proof- @@ -6131,8 +6222,7 @@ qed lemma homeomorphic_compact: - fixes f :: "'a::heine_borel \ 'b::heine_borel" - (* class constraint due to continuous_on_inv *) + fixes f :: "'a::topological_space \ 'b::t2_space" shows "compact s \ continuous_on s f \ (f ` s = t) \ inj_on f s \ s homeomorphic t" unfolding homeomorphic_def by (metis homeomorphism_compact) @@ -6174,12 +6264,11 @@ qed lemma homeomorphic_balls: - fixes a b ::"'a::real_normed_vector" (* FIXME: generalize to metric_space *) + fixes a b ::"'a::real_normed_vector" assumes "0 < d" "0 < e" shows "(ball a d) homeomorphic (ball b e)" (is ?th) "(cball a d) homeomorphic (cball b e)" (is ?cth) proof- - have *:"\e / d\ > 0" "\d / e\ >0" using assms using divide_pos_pos by auto show ?th unfolding homeomorphic_minimal apply(rule_tac x="\x. b + (e/d) *\<^sub>R (x - a)" in exI) apply(rule_tac x="\x. a + (d/e) *\<^sub>R (x - b)" in exI) @@ -6189,7 +6278,6 @@ unfolding continuous_on by (intro ballI tendsto_intros, simp)+ next - have *:"\e / d\ > 0" "\d / e\ >0" using assms using divide_pos_pos by auto show ?cth unfolding homeomorphic_minimal apply(rule_tac x="\x. b + (e/d) *\<^sub>R (x - a)" in exI) apply(rule_tac x="\x. a + (d/e) *\<^sub>R (x - b)" in exI)