# HG changeset patch # User huffman # Date 1244057049 25200 # Node ID b8bdef62bfa6e65d7256332f7e3207fad93688dd # Parent 1501fc26f11b724119939497f819243872b0b2aa# Parent f2e6b6526092904b10efe66b4bdecabee7a73a64 merged diff -r f2e6b6526092 -r b8bdef62bfa6 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Wed Jun 03 15:48:54 2009 +0200 +++ b/src/HOL/Complex.thy Wed Jun 03 12:24:09 2009 -0700 @@ -268,26 +268,28 @@ instantiation complex :: real_normed_field begin -definition - complex_norm_def: "norm z = sqrt ((Re z)\ + (Im z)\)" +definition complex_norm_def: + "norm z = sqrt ((Re z)\ + (Im z)\)" abbreviation cmod :: "complex \ real" where "cmod \ norm" -definition - complex_sgn_def: "sgn x = x /\<^sub>R cmod x" +definition complex_sgn_def: + "sgn x = x /\<^sub>R cmod x" -definition - dist_complex_def: "dist x y = cmod (x - y)" +definition dist_complex_def: + "dist x y = cmod (x - y)" + +definition topo_complex_def [code del]: + "topo = {S::complex set. \x\S. \e>0. \y. dist y x < e \ y \ S}" lemmas cmod_def = complex_norm_def lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\ + y\)" by (simp add: complex_norm_def) -instance -proof +instance proof fix r :: real and x y :: complex show "0 \ norm x" by (induct x) simp @@ -306,6 +308,8 @@ by (rule complex_sgn_def) show "dist x y = cmod (x - y)" by (rule dist_complex_def) + show "topo = {S::complex set. \x\S. \e>0. \y. dist y x < e \ y \ S}" + by (rule topo_complex_def) qed end diff -r f2e6b6526092 -r b8bdef62bfa6 src/HOL/Library/Convex_Euclidean_Space.thy --- a/src/HOL/Library/Convex_Euclidean_Space.thy Wed Jun 03 15:48:54 2009 +0200 +++ b/src/HOL/Library/Convex_Euclidean_Space.thy Wed Jun 03 12:24:09 2009 -0700 @@ -602,8 +602,8 @@ have "\x\0. x \ 1 \ (1 - x) *s x1 + x *s x2 \ e1 \ (1 - x) *s x1 + x *s x2 \ e2" apply(rule connected_real_lemma) apply (simp add: `x1\e1` `x2\e2` dist_commute)+ using * apply(simp add: dist_norm) - using as(1,2)[unfolded open_def] apply simp - using as(1,2)[unfolded open_def] apply simp + using as(1,2)[unfolded open_dist] apply simp + using as(1,2)[unfolded open_dist] apply simp using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2 using as(3) by auto then obtain x where "x\0" "x\1" "(1 - x) *s x1 + x *s x2 \ e1" "(1 - x) *s x1 + x *s x2 \ e2" by auto diff -r f2e6b6526092 -r b8bdef62bfa6 src/HOL/Library/Euclidean_Space.thy --- a/src/HOL/Library/Euclidean_Space.thy Wed Jun 03 15:48:54 2009 +0200 +++ b/src/HOL/Library/Euclidean_Space.thy Wed Jun 03 12:24:09 2009 -0700 @@ -506,6 +506,9 @@ definition dist_vector_def: "dist (x::'a^'b) (y::'a^'b) = setL2 (\i. dist (x$i) (y$i)) UNIV" +definition topo_vector_def: + "topo = {S::('a ^ 'b) set. \x\S. \e>0. \y. dist y x < e \ y \ S}" + instance proof fix x y :: "'a ^ 'b" show "dist x y = 0 \ x = y" @@ -518,6 +521,9 @@ apply (rule order_trans [OF _ setL2_triangle_ineq]) apply (simp add: setL2_mono dist_triangle2) done +next + show "topo = {S::('a ^ 'b) set. \x\S. \e>0. \y. dist y x < e \ y \ S}" + by (rule topo_vector_def) qed end diff -r f2e6b6526092 -r b8bdef62bfa6 src/HOL/Library/Inner_Product.thy --- a/src/HOL/Library/Inner_Product.thy Wed Jun 03 15:48:54 2009 +0200 +++ b/src/HOL/Library/Inner_Product.thy Wed Jun 03 12:24:09 2009 -0700 @@ -10,7 +10,7 @@ subsection {* Real inner product spaces *} -class real_inner = real_vector + sgn_div_norm + dist_norm + +class real_inner = real_vector + sgn_div_norm + dist_norm + topo_dist + fixes inner :: "'a \ 'a \ real" assumes inner_commute: "inner x y = inner y x" and inner_left_distrib: "inner (x + y) z = inner x z + inner y z" diff -r f2e6b6526092 -r b8bdef62bfa6 src/HOL/Library/Product_Vector.thy --- a/src/HOL/Library/Product_Vector.thy Wed Jun 03 15:48:54 2009 +0200 +++ b/src/HOL/Library/Product_Vector.thy Wed Jun 03 12:24:09 2009 -0700 @@ -39,6 +39,39 @@ end +subsection {* Product is a topological space *} + +instantiation + "*" :: (topological_space, topological_space) topological_space +begin + +definition topo_prod_def: + "topo = {S. \x\S. \A\topo. \B\topo. x \ A \ B \ A \ B \ S}" + +instance proof + show "(UNIV :: ('a \ 'b) set) \ topo" + unfolding topo_prod_def by (auto intro: topo_UNIV) +next + fix S T :: "('a \ 'b) set" + assume "S \ topo" "T \ topo" thus "S \ T \ topo" + unfolding topo_prod_def + apply clarify + apply (drule (1) bspec)+ + apply (clarify, rename_tac Sa Ta Sb Tb) + apply (rule_tac x="Sa \ Ta" in rev_bexI) + apply (simp add: topo_Int) + apply (rule_tac x="Sb \ Tb" in rev_bexI) + apply (simp add: topo_Int) + apply fast + done +next + fix T :: "('a \ 'b) set set" + assume "T \ topo" thus "\T \ topo" + unfolding topo_prod_def Bex_def by fast +qed + +end + subsection {* Product is a metric space *} instantiation @@ -67,6 +100,53 @@ apply (rule power_mono [OF dist_triangle2 [of _ _ "snd z"] zero_le_dist]) apply (simp only: real_sum_squared_expand) done +next + (* FIXME: long proof! *) + (* Maybe it would be easier to define topological spaces *) + (* in terms of neighborhoods instead of open sets? *) + show "topo = {S::('a \ 'b) set. \x\S. \e>0. \y. dist y x < e \ y \ S}" + unfolding topo_prod_def topo_dist + apply (safe, rename_tac S a b) + apply (drule (1) bspec) + apply clarify + apply (drule (1) bspec)+ + apply (clarify, rename_tac r s) + apply (rule_tac x="min r s" in exI, simp) + apply (clarify, rename_tac c d) + apply (erule subsetD) + apply (simp add: dist_Pair_Pair) + apply (rule conjI) + apply (drule spec, erule mp) + 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]) + + apply (rename_tac S a b) + apply (drule (1) bspec) + apply clarify + apply (subgoal_tac "\r>0. \s>0. e = sqrt (r\ + s\)") + apply clarify + apply (rule_tac x="{y. dist y a < r}" in rev_bexI) + 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 (rule_tac x="{y. dist y b < s}" in rev_bexI) + 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 (rule conjI) + apply simp + apply (clarify, rename_tac c d) + apply (drule spec, erule mp) + apply (simp add: dist_Pair_Pair add_strict_mono power_strict_mono) + apply (rule_tac x="e / sqrt 2" in exI, simp add: divide_pos_pos) + apply (rule_tac x="e / sqrt 2" in exI, simp add: divide_pos_pos) + apply (simp add: power_divide) + done qed end diff -r f2e6b6526092 -r b8bdef62bfa6 src/HOL/Library/Topology_Euclidean_Space.thy --- a/src/HOL/Library/Topology_Euclidean_Space.thy Wed Jun 03 15:48:54 2009 +0200 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy Wed Jun 03 12:24:09 2009 -0700 @@ -194,35 +194,30 @@ by (simp add: subtopology_superset) subsection{* The universal Euclidean versions are what we use most of the time *} + definition - "open" :: "'a::metric_space set \ bool" where - "open S \ (\x \ S. \e >0. \x'. dist x' x < e \ x' \ S)" -definition "closed S \ open(UNIV - S)" -definition "euclidean = topology open" - -lemma open_empty[intro,simp]: "open {}" by (simp add: open_def) + "open" :: "'a::topological_space set \ bool" where + "open S \ S \ topo" + +definition + closed :: "'a::topological_space set \ bool" where + "closed S \ open(UNIV - S)" + +definition + euclidean :: "'a::topological_space topology" where + "euclidean = topology open" + lemma open_UNIV[intro,simp]: "open UNIV" - by (simp add: open_def, rule exI[where x="1"], auto) - -lemma open_inter[intro]: assumes S: "open S" and T: "open T" - shows "open (S \ T)" -proof- - note thS = S[unfolded open_def, rule_format] - note thT = T[unfolded open_def, rule_format] - {fix x assume x: "x \ S\T" - hence xS: "x \ S" and xT: "x \ T" by simp_all - from thS[OF xS] obtain eS where eS: "eS > 0" "\x'. dist x' x < eS \ x' \ S" by blast - from thT[OF xT] obtain eT where eT: "eT > 0" "\x'. dist x' x < eT \ x' \ T" by blast - from real_lbound_gt_zero[OF eS(1) eT(1)] obtain e where e: "e > 0" "e < eS" "e < eT" by blast - { fix x' assume d: "dist x' x < e" - hence dS: "dist x' x < eS" and dT: "dist x' x < eT" using e by arith+ - from eS(2)[rule_format, OF dS] eT(2)[rule_format, OF dT] have "x' \ S\T" by blast} - hence "\e >0. \x'. dist x' x < e \ x' \ (S\T)" using e by blast} - then show ?thesis unfolding open_def by blast -qed + unfolding open_def by (rule topo_UNIV) + +lemma open_inter[intro]: "open S \ open T \ open (S \ T)" + unfolding open_def by (rule topo_Int) lemma open_Union[intro]: "(\S\K. open S) \ open (\ K)" - by (simp add: open_def) metis + unfolding open_def subset_eq [symmetric] by (rule topo_Union) + +lemma open_empty[intro,simp]: "open {}" + using open_Union [of "{}"] by simp lemma open_openin: "open S \ openin euclidean S" unfolding euclidean_def @@ -242,7 +237,9 @@ lemma closed_closedin: "closed S \ closedin euclidean S" by (simp add: closed_def closedin_def topspace_euclidean open_openin) -lemma open_Un[intro]: "open S \ open T \ open (S\T)" +lemma open_Un[intro]: + fixes S T :: "'a::topological_space set" + shows "open S \ open T \ open (S\T)" by (auto simp add: open_openin) lemma open_subopen: "open S \ (\x\S. \T. open T \ x \ T \ T \ S)" @@ -320,6 +317,11 @@ subsection{* Topological properties of open balls *} +lemma open_dist: + fixes S :: "'a::metric_space set" + shows "open S \ (\x\S. \e>0. \x'. dist x' x < e \ x' \ S)" + unfolding open_def topo_dist by simp + lemma diff_less_iff: "(a::real) - b > 0 \ a > b" "(a::real) - b < 0 \ a < b" "a - b < c \ a < c +b" "a - b > c \ a > c +b" by arith+ @@ -327,7 +329,7 @@ "a - b \ c \ a \ c +b" "a - b \ c \ a \ c +b" by arith+ lemma open_ball[intro, simp]: "open (ball x e)" - unfolding open_def ball_def Collect_def Ball_def mem_def + unfolding open_dist ball_def Collect_def Ball_def mem_def unfolding dist_commute apply clarify apply (rule_tac x="e - dist xa x" in exI) @@ -340,7 +342,7 @@ lemma centre_in_ball[simp]: "x \ ball x e \ e > 0" by (metis mem_ball dist_self) lemma open_contains_ball: "open S \ (\x\S. \e>0. ball x e \ S)" - unfolding open_def subset_eq mem_ball Ball_def dist_commute .. + unfolding open_dist subset_eq mem_ball Ball_def dist_commute .. lemma open_contains_ball_eq: "open S \ \x. x\S \ (\e>0. ball x e \ S)" by (metis open_contains_ball subset_eq centre_in_ball) @@ -382,11 +384,13 @@ lemma closed_subset: "S \ T \ closed S \ closedin (subtopology euclidean T) S" by (auto simp add: closedin_closed) -lemma openin_euclidean_subtopology_iff: "openin (subtopology euclidean U) S +lemma openin_euclidean_subtopology_iff: + fixes S U :: "'a::metric_space set" + shows "openin (subtopology euclidean U) S \ S \ U \ (\x\S. \e>0. \x'\U. dist x' x < e \ x'\ S)" (is "?lhs \ ?rhs") proof- {assume ?lhs hence ?rhs unfolding openin_subtopology open_openin[symmetric] - by (simp add: open_def) blast} + by (simp add: open_dist) blast} moreover {assume SU: "S \ U" and H: "\x. x \ S \ \e>0. \x'\U. dist x' x < e \ x' \ S" from H obtain d where d: "\x . x\ S \ d x > 0 \ (\x' \ U. dist x' x < d x \ x' \ S)" @@ -441,7 +445,7 @@ e1 \ e2 = {} \ ~(e1 = {}) \ ~(e2 = {}))" -unfolding connected_def openin_open by blast +unfolding connected_def openin_open by (safe, blast+) lemma exists_diff: "(\S. P(UNIV - S)) \ (\S. P S)" (is "?lhs \ ?rhs") proof- @@ -480,31 +484,61 @@ subsection{* Hausdorff and other separation properties *} -lemma hausdorff: - assumes xy: "x \ y" - shows "\U V. open U \ open V \ x\ U \ y \ V \ (U \ V = {})" (is "\U V. ?P U V") -proof- +axclass t0_space \ topological_space + t0_space: + "x \ y \ \U. open U \ \ (x \ U \ y \ U)" + +axclass t1_space \ topological_space + t1_space: + "x \ y \ \U V. open U \ open V \ x \ U \ y \ U \ x \ V \ y \ V" + +instance t1_space \ t0_space +by default (fast dest: t1_space) + +text {* T2 spaces are also known as Hausdorff spaces. *} + +axclass t2_space \ topological_space + hausdorff: + "x \ y \ \U V. open U \ open V \ x \ U \ y \ V \ U \ V = {}" + +instance t2_space \ t1_space +by default (fast dest: hausdorff) + +instance metric_space \ t2_space +proof + fix x y :: "'a::metric_space" + assume xy: "x \ y" let ?U = "ball x (dist x y / 2)" let ?V = "ball y (dist x y / 2)" have th0: "\d x y z. (d x z :: real) <= d x y + d y z \ d y z = d z y ==> ~(d x y * 2 < d x z \ d z y * 2 < d x z)" by arith - have "?P ?U ?V" using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_commute] - by (auto simp add: expand_set_eq less_divide_eq_number_of1) - then show ?thesis by blast -qed - -lemma separation_t2: "x \ y \ (\U V. open U \ open V \ x \ U \ y \ V \ U \ V = {})" + have "open ?U \ open ?V \ x \ ?U \ y \ ?V \ ?U \ ?V = {}" + using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_commute] + by (auto simp add: expand_set_eq) + then show "\U V. open U \ open V \ x \ U \ y \ V \ U \ V = {}" + by blast +qed + +lemma separation_t2: + fixes x y :: "'a::t2_space" + shows "x \ y \ (\U V. open U \ open V \ x \ U \ y \ V \ U \ V = {})" using hausdorff[of x y] by blast -lemma separation_t1: "x \ y \ (\U V. open U \ open V \ x \U \ y\ U \ x\V \ y\V)" - using separation_t2[of x y] by blast - -lemma separation_t0: "x \ y \ (\U. open U \ ~(x\U \ y\U))" by(metis separation_t1) +lemma separation_t1: + fixes x y :: "'a::t1_space" + shows "x \ y \ (\U V. open U \ open V \ x \U \ y\ U \ x\V \ y\V)" + using t1_space[of x y] by blast + +lemma separation_t0: + fixes x y :: "'a::t0_space" + shows "x \ y \ (\U. open U \ ~(x\U \ y\U))" + using t0_space[of x y] by blast subsection{* Limit points *} definition - islimpt:: "'a::metric_space \ 'a set \ bool" (infixr "islimpt" 60) where + islimpt:: "'a::topological_space \ 'a set \ bool" + (infixr "islimpt" 60) where "x islimpt S \ (\T. x\T \ open T \ (\y\S. y\T \ y\x))" (* FIXME: Sure this form is OK????*) @@ -513,23 +547,29 @@ using assms unfolding islimpt_def by auto lemma islimpt_subset: "x islimpt S \ S \ T ==> x islimpt T" by (auto simp add: islimpt_def) -lemma islimpt_approachable: "x islimpt S \ (\e>0. \x'\S. x' \ x \ dist x' x < e)" + +lemma islimpt_approachable: + fixes x :: "'a::metric_space" + shows "x islimpt S \ (\e>0. \x'\S. x' \ x \ dist x' x < e)" unfolding islimpt_def apply auto apply(erule_tac x="ball x e" in allE) apply auto apply(rule_tac x=y in bexI) apply (auto simp add: dist_commute) - apply (simp add: open_def, drule (1) bspec) + apply (simp add: open_dist, drule (1) bspec) apply (clarify, drule spec, drule (1) mp, auto) done -lemma islimpt_approachable_le: "x islimpt S \ (\e>0. \x'\ S. x' \ x \ dist x' x <= e)" +lemma islimpt_approachable_le: + fixes x :: "'a::metric_space" + shows "x islimpt S \ (\e>0. \x'\ S. x' \ x \ dist x' x <= e)" unfolding islimpt_approachable using approachable_lt_le[where f="\x'. dist x' x" and P="\x'. \ (x'\S \ x'\x)"] by metis (* FIXME: VERY slow! *) axclass perfect_space \ metric_space + (* FIXME: perfect_space should inherit from topological_space *) islimpt_UNIV [simp, intro]: "x islimpt UNIV" lemma perfect_choose_dist: @@ -544,7 +584,7 @@ apply (clarify, rule_tac x="x + e/2" in bexI) apply (auto simp add: dist_norm) done - + instance "^" :: (perfect_space, finite) perfect_space proof fix x :: "'a ^ 'b" @@ -576,7 +616,7 @@ by (metis DiffE DiffI UNIV_I insertCI insert_absorb mem_def) lemma islimpt_EMPTY[simp]: "\ x islimpt {}" - unfolding islimpt_approachable apply auto by ferrack + unfolding islimpt_def by auto lemma closed_positive_orthant: "closed {x::real^'n::finite. \i. 0 \x$i}" proof- @@ -616,7 +656,9 @@ ultimately show ?case by blast qed -lemma islimpt_finite: assumes fS: "finite S" shows "\ a islimpt S" +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) @@ -624,13 +666,14 @@ apply (rule iffI) defer apply (metis Un_upper1 Un_upper2 islimpt_subset) - unfolding islimpt_approachable - apply auto - apply (erule_tac x="min e ea" in allE) - apply auto + unfolding islimpt_def + apply (rule ccontr, clarsimp, rename_tac A B) + apply (drule_tac x="A \ B" in spec) + apply (auto simp add: open_inter) done lemma discrete_imp_closed: + fixes S :: "'a::metric_space set" assumes e: "0 < e" and d: "\x \ S. \y \ S. dist y x < e \ y = x" shows "closed S" proof- @@ -644,7 +687,7 @@ by (intro dist_triangle_lt [where z=x], simp) from d[rule_format, OF y(1) z(1) th] y z have False by (auto simp add: dist_commute)} - then show ?thesis by (metis islimpt_approachable closed_limpt) + then show ?thesis by (metis islimpt_approachable closed_limpt [where 'a='a]) qed subsection{* Interior of a Set *} @@ -652,7 +695,7 @@ lemma interior_eq: "interior S = S \ open S" apply (simp add: expand_set_eq interior_def) - apply (subst (2) open_subopen) by blast + apply (subst (2) open_subopen) by (safe, blast+) lemma interior_open: "open S ==> (interior S = S)" by (metis interior_eq) @@ -701,7 +744,6 @@ qed lemma interior_closed_Un_empty_interior: - fixes S T :: "'a::metric_space set" assumes cS: "closed S" and iT: "interior T = {}" shows "interior(S \ T) = interior S" proof @@ -861,7 +903,10 @@ unfolding closure_interior by auto -lemma open_inter_closure_subset: "open S \ (S \ (closure T)) \ closure(S \ T)" +lemma open_inter_closure_subset: + fixes S :: "'a::metric_space set" + (* FIXME: generalize to topological_space *) + shows "open S \ (S \ (closure T)) \ closure(S \ T)" proof fix x assume as: "open S" "x \ S \