author huffman Mon Aug 15 14:09:39 2011 -0700 (2011-08-15) changeset 44213 6fb54701a11b parent 44212 4d10e7f342b1 child 44214 1e0414bda9af
add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
simplify and generalize some proofs;
1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Aug 15 12:18:34 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Aug 15 14:09:39 2011 -0700
1.3 @@ -1093,34 +1093,21 @@
1.4      done
1.5  qed
1.7 +lemma continuous_at_component: "continuous (at a) (\<lambda>x. x \$ i)"
1.8 +unfolding continuous_at by (intro tendsto_intros)
1.9 +
1.10 +lemma continuous_on_component: "continuous_on s (\<lambda>x. x \$ i)"
1.11 +unfolding continuous_on_def by (intro ballI tendsto_intros)
1.12 +
1.13  lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x\$i}"
1.14 -proof-
1.15 -  let ?U = "UNIV :: 'n set"
1.16 -  let ?O = "{x::real^'n. \<forall>i. x\$i\<ge>0}"
1.17 -  {fix x:: "real^'n" and i::'n assume H: "\<forall>e>0. \<exists>x'\<in>?O. x' \<noteq> x \<and> dist x' x < e"
1.18 -    and xi: "x\$i < 0"
1.19 -    from xi have th0: "-x\$i > 0" by arith
1.20 -    from H[rule_format, OF th0] obtain x' where x': "x' \<in>?O" "x' \<noteq> x" "dist x' x < -x \$ i" by blast
1.21 -      have th:" \<And>b a (x::real). abs x <= b \<Longrightarrow> b <= a ==> ~(a + x < 0)" by arith
1.22 -      have th': "\<And>x (y::real). x < 0 \<Longrightarrow> 0 <= y ==> abs x <= abs (y - x)" by arith
1.23 -      have th1: "\<bar>x\$i\<bar> \<le> \<bar>(x' - x)\$i\<bar>" using x'(1) xi
1.24 -        apply (simp only: vector_component)
1.25 -        by (rule th') auto
1.26 -      have th2: "\<bar>dist x x'\<bar> \<ge> \<bar>(x' - x)\$i\<bar>" using  component_le_norm_cart[of "x'-x" i]
1.27 -        apply (simp add: dist_norm) by norm
1.28 -      from th[OF th1 th2] x'(3) have False by (simp add: dist_commute) }
1.29 -  then show ?thesis unfolding closed_limpt islimpt_approachable
1.30 -    unfolding not_le[symmetric] by blast
1.31 -qed
1.32 +  unfolding Collect_all_eq
1.33 +  by (intro closed_INT ballI closed_Collect_le continuous_const
1.34 +    continuous_at_component)
1.35 +
1.36  lemma Lim_component_cart:
1.37    fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n"
1.38    shows "(f ---> l) net \<Longrightarrow> ((\<lambda>a. f a \$i) ---> l\$i) net"
1.39 -  unfolding tendsto_iff
1.40 -  apply (clarify)
1.41 -  apply (drule spec, drule (1) mp)
1.42 -  apply (erule eventually_elim1)
1.43 -  apply (erule le_less_trans [OF dist_vec_nth_le])
1.44 -  done
1.45 +  by (intro tendsto_intros)
1.47  lemma bounded_component_cart: "bounded s \<Longrightarrow> bounded ((\<lambda>x. x \$ i) ` s)"
1.48  unfolding bounded_def
1.49 @@ -1193,12 +1180,6 @@
1.50    with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" by auto
1.51  qed
1.53 -lemma continuous_at_component: "continuous (at a) (\<lambda>x. x \$ i)"
1.54 -unfolding continuous_at by (intro tendsto_intros)
1.55 -
1.56 -lemma continuous_on_component: "continuous_on s (\<lambda>x. x \$ i)"
1.57 -unfolding continuous_on_def by (intro ballI tendsto_intros)
1.58 -
1.59  lemma interval_cart: fixes a :: "'a::ord^'n" shows
1.60    "{a <..< b} = {x::'a^'n. \<forall>i. a\$i < x\$i \<and> x\$i < b\$i}" and
1.61    "{a .. b} = {x::'a^'n. \<forall>i. a\$i \<le> x\$i \<and> x\$i \<le> b\$i}"
1.62 @@ -1307,27 +1288,15 @@
1.64  lemma closed_interval_left_cart: fixes b::"real^'n"
1.65    shows "closed {x::real^'n. \<forall>i. x\$i \<le> b\$i}"
1.66 -proof-
1.67 -  { fix i
1.68 -    fix x::"real^'n" assume x:"\<forall>e>0. \<exists>x'\<in>{x. \<forall>i. x \$ i \<le> b \$ i}. x' \<noteq> x \<and> dist x' x < e"
1.69 -    { assume "x\$i > b\$i"
1.70 -      then obtain y where "y \$ i \<le> b \$ i"  "y \<noteq> x"  "dist y x < x\$i - b\$i" using x[THEN spec[where x="x\$i - b\$i"]] by auto
1.71 -      hence False using component_le_norm_cart[of "y - x" i] unfolding dist_norm and vector_minus_component by auto   }
1.72 -    hence "x\$i \<le> b\$i" by(rule ccontr)auto  }
1.73 -  thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
1.74 -qed
1.75 +  unfolding Collect_all_eq
1.76 +  by (intro closed_INT ballI closed_Collect_le continuous_const
1.77 +    continuous_at_component)
1.79  lemma closed_interval_right_cart: fixes a::"real^'n"
1.80    shows "closed {x::real^'n. \<forall>i. a\$i \<le> x\$i}"
1.81 -proof-
1.82 -  { fix i
1.83 -    fix x::"real^'n" assume x:"\<forall>e>0. \<exists>x'\<in>{x. \<forall>i. a \$ i \<le> x \$ i}. x' \<noteq> x \<and> dist x' x < e"
1.84 -    { assume "a\$i > x\$i"
1.85 -      then obtain y where "a \$ i \<le> y \$ i"  "y \<noteq> x"  "dist y x < a\$i - x\$i" using x[THEN spec[where x="a\$i - x\$i"]] by auto
1.86 -      hence False using component_le_norm_cart[of "y - x" i] unfolding dist_norm and vector_minus_component by auto   }
1.87 -    hence "a\$i \<le> x\$i" by(rule ccontr)auto  }
1.88 -  thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
1.89 -qed
1.90 +  unfolding Collect_all_eq
1.91 +  by (intro closed_INT ballI closed_Collect_le continuous_const
1.92 +    continuous_at_component)
1.94  lemma is_interval_cart:"is_interval (s::(real^'n) set) \<longleftrightarrow>
1.95    (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((a\$i \<le> x\$i \<and> x\$i \<le> b\$i) \<or> (b\$i \<le> x\$i \<and> x\$i \<le> a\$i))) \<longrightarrow> x \<in> s)"
1.96 @@ -1335,19 +1304,19 @@
1.98  lemma closed_halfspace_component_le_cart:
1.99    shows "closed {x::real^'n. x\$i \<le> a}"
1.100 -  using closed_halfspace_le[of "(cart_basis i)::real^'n" a] unfolding inner_basis[OF assms] by auto
1.101 +  by (intro closed_Collect_le continuous_at_component continuous_const)
1.103  lemma closed_halfspace_component_ge_cart:
1.104    shows "closed {x::real^'n. x\$i \<ge> a}"
1.105 -  using closed_halfspace_ge[of a "(cart_basis i)::real^'n"] unfolding inner_basis[OF assms] by auto
1.106 +  by (intro closed_Collect_le continuous_at_component continuous_const)
1.108  lemma open_halfspace_component_lt_cart:
1.109    shows "open {x::real^'n. x\$i < a}"
1.110 -  using open_halfspace_lt[of "(cart_basis i)::real^'n" a] unfolding inner_basis[OF assms] by auto
1.111 +  by (intro open_Collect_less continuous_at_component continuous_const)
1.113  lemma open_halfspace_component_gt_cart:
1.114    shows "open {x::real^'n. x\$i  > a}"
1.115 -  using open_halfspace_gt[of a "(cart_basis i)::real^'n"] unfolding inner_basis[OF assms] by auto
1.116 +  by (intro open_Collect_less continuous_at_component continuous_const)
1.118  lemma Lim_component_le_cart: fixes f :: "'a \<Rightarrow> real^'n"
1.119    assumes "(f ---> l) net" "\<not> (trivial_limit net)"  "eventually (\<lambda>x. f(x)\$i \<le> b) net"
1.120 @@ -1382,23 +1351,14 @@
1.121    unfolding subspace_def by auto
1.123  lemma closed_substandard_cart:
1.124 - "closed {x::real^'n. \<forall>i. P i --> x\$i = 0}" (is "closed ?A")
1.125 +  "closed {x::'a::real_normed_vector ^ 'n. \<forall>i. P i \<longrightarrow> x\$i = 0}"
1.126  proof-
1.127 -  let ?D = "{i. P i}"
1.128 -  let ?Bs = "{{x::real^'n. inner (cart_basis i) x = 0}| i. i \<in> ?D}"
1.129 -  { fix x
1.130 -    { assume "x\<in>?A"
1.131 -      hence x:"\<forall>i\<in>?D. x \$ i = 0" by auto
1.132 -      hence "x\<in> \<Inter> ?Bs" by(auto simp add: inner_basis x) }
1.133 -    moreover
1.134 -    { assume x:"x\<in>\<Inter>?Bs"
1.135 -      { fix i assume i:"i \<in> ?D"
1.136 -        then obtain B where BB:"B \<in> ?Bs" and B:"B = {x::real^'n. inner (cart_basis i) x = 0}" by auto
1.137 -        hence "x \$ i = 0" unfolding B using x unfolding inner_basis by auto  }
1.138 -      hence "x\<in>?A" by auto }
1.139 -    ultimately have "x\<in>?A \<longleftrightarrow> x\<in> \<Inter>?Bs" .. }
1.140 -  hence "?A = \<Inter> ?Bs" by auto
1.141 -  thus ?thesis by(auto simp add: closed_Inter closed_hyperplane)
1.142 +  { fix i::'n
1.143 +    have "closed {x::'a ^ 'n. P i \<longrightarrow> x\$i = 0}"
1.144 +      by (cases "P i", simp_all, intro closed_Collect_eq
1.145 +        continuous_at_component continuous_const) }
1.146 +  thus ?thesis
1.147 +    unfolding Collect_all_eq by (simp add: closed_INT)
1.148  qed
1.150  lemma dim_substandard_cart:
2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 12:18:34 2011 -0700
2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 15 14:09:39 2011 -0700
2.3 @@ -5152,6 +5152,52 @@
2.5  subsection {* Closure of halfspaces and hyperplanes *}
2.7 +lemma open_Collect_less:
2.8 +  fixes f g :: "'a::t2_space \<Rightarrow> real"
2.9 +  (* FIXME: generalize to topological_space *)
2.10 +  assumes f: "\<And>x. continuous (at x) f"
2.11 +  assumes g: "\<And>x. continuous (at x) g"
2.12 +  shows "open {x. f x < g x}"
2.13 +proof -
2.14 +  have "open ((\<lambda>x. g x - f x) -` {0<..})"
2.15 +    using continuous_sub [OF g f] open_real_greaterThan
2.16 +    by (rule continuous_open_vimage [rule_format])
2.17 +  also have "((\<lambda>x. g x - f x) -` {0<..}) = {x. f x < g x}"
2.18 +    by auto
2.19 +  finally show ?thesis .
2.20 +qed
2.21 +
2.22 +lemma closed_Collect_le:
2.23 +  fixes f g :: "'a::t2_space \<Rightarrow> real"
2.24 +  (* FIXME: generalize to topological_space *)
2.25 +  assumes f: "\<And>x. continuous (at x) f"
2.26 +  assumes g: "\<And>x. continuous (at x) g"
2.27 +  shows "closed {x. f x \<le> g x}"
2.28 +proof -
2.29 +  have "closed ((\<lambda>x. g x - f x) -` {0..})"
2.30 +    using continuous_sub [OF g f] closed_real_atLeast
2.31 +    by (rule continuous_closed_vimage [rule_format])
2.32 +  also have "((\<lambda>x. g x - f x) -` {0..}) = {x. f x \<le> g x}"
2.33 +    by auto
2.34 +  finally show ?thesis .
2.35 +qed
2.36 +
2.37 +lemma closed_Collect_eq:
2.38 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
2.39 +  (* FIXME: generalize 'a to topological_space *)
2.40 +  (* FIXME: generalize 'b to t2_space *)
2.41 +  assumes f: "\<And>x. continuous (at x) f"
2.42 +  assumes g: "\<And>x. continuous (at x) g"
2.43 +  shows "closed {x. f x = g x}"
2.44 +proof -
2.45 +  have "closed ((\<lambda>x. g x - f x) -` {0})"
2.46 +    using continuous_sub [OF g f] closed_singleton
2.47 +    by (rule continuous_closed_vimage [rule_format])
2.48 +  also have "((\<lambda>x. g x - f x) -` {0}) = {x. f x = g x}"
2.49 +    by auto
2.50 +  finally show ?thesis .
2.51 +qed
2.52 +
2.53  lemma Lim_inner:
2.54    assumes "(f ---> l) net"  shows "((\<lambda>y. inner a (f y)) ---> inner a l) net"
2.55    by (intro tendsto_intros assms)
2.56 @@ -5168,53 +5214,41 @@
2.57    unfolding continuous_on by (rule ballI) (intro tendsto_intros)
2.59  lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
2.60 -proof-
2.61 -  have "\<forall>x. continuous (at x) (inner a)"
2.62 -    unfolding continuous_at by (rule allI) (intro tendsto_intros)
2.63 -  hence "closed (inner a -` {..b})"
2.64 -    using closed_real_atMost by (rule continuous_closed_vimage)
2.65 -  moreover have "{x. inner a x \<le> b} = inner a -` {..b}" by auto
2.66 -  ultimately show ?thesis by simp
2.67 -qed
2.68 +  by (intro closed_Collect_le continuous_at_inner continuous_const)
2.70  lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
2.71 -  using closed_halfspace_le[of "-a" "-b"] unfolding inner_minus_left by auto
2.72 +  by (intro closed_Collect_le continuous_at_inner continuous_const)
2.74  lemma closed_hyperplane: "closed {x. inner a x = b}"
2.75 -proof-
2.76 -  have "{x. inner a x = b} = {x. inner a x \<ge> b} \<inter> {x. inner a x \<le> b}" by auto
2.77 -  thus ?thesis using closed_halfspace_le[of a b] and closed_halfspace_ge[of b a] using closed_Int by auto
2.78 -qed
2.79 +  by (intro closed_Collect_eq continuous_at_inner continuous_const)
2.81  lemma closed_halfspace_component_le:
2.82    shows "closed {x::'a::euclidean_space. x\$\$i \<le> a}"
2.83 -  using closed_halfspace_le[of "(basis i)::'a" a] unfolding euclidean_component_def .
2.84 +  by (intro closed_Collect_le continuous_at_euclidean_component
2.85 +    continuous_const)
2.87  lemma closed_halfspace_component_ge:
2.88    shows "closed {x::'a::euclidean_space. x\$\$i \<ge> a}"
2.89 -  using closed_halfspace_ge[of a "(basis i)::'a"] unfolding euclidean_component_def .
2.90 +  by (intro closed_Collect_le continuous_at_euclidean_component
2.91 +    continuous_const)
2.93  text {* Openness of halfspaces. *}
2.95  lemma open_halfspace_lt: "open {x. inner a x < b}"
2.96 -proof-
2.97 -  have "- {x. b \<le> inner a x} = {x. inner a x < b}" by auto
2.98 -  thus ?thesis using closed_halfspace_ge[unfolded closed_def, of b a] by auto
2.99 -qed
2.100 +  by (intro open_Collect_less continuous_at_inner continuous_const)
2.102  lemma open_halfspace_gt: "open {x. inner a x > b}"
2.103 -proof-
2.104 -  have "- {x. b \<ge> inner a x} = {x. inner a x > b}" by auto
2.105 -  thus ?thesis using closed_halfspace_le[unfolded closed_def, of a b] by auto
2.106 -qed
2.107 +  by (intro open_Collect_less continuous_at_inner continuous_const)
2.109  lemma open_halfspace_component_lt:
2.110    shows "open {x::'a::euclidean_space. x\$\$i < a}"
2.111 -  using open_halfspace_lt[of "(basis i)::'a" a] unfolding euclidean_component_def .
2.112 +  by (intro open_Collect_less continuous_at_euclidean_component
2.113 +    continuous_const)
2.115  lemma open_halfspace_component_gt:
2.116    shows "open {x::'a::euclidean_space. x\$\$i  > a}"
2.117 -  using open_halfspace_gt[of a "(basis i)::'a"] unfolding euclidean_component_def .
2.118 +  by (intro open_Collect_less continuous_at_euclidean_component
2.119 +    continuous_const)
2.121  text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
2.123 @@ -5252,23 +5286,15 @@
2.124    fixes a :: "'a\<Colon>ordered_euclidean_space"
2.125    shows "closed {.. a}"
2.126    unfolding eucl_atMost_eq_halfspaces
2.127 -proof (safe intro!: closed_INT)
2.128 -  fix i :: nat
2.129 -  have "- {x::'a. x \$\$ i \<le> a \$\$ i} = {x. a \$\$ i < x \$\$ i}" by auto
2.130 -  then show "closed {x::'a. x \$\$ i \<le> a \$\$ i}"
2.131 -    by (simp add: closed_def open_halfspace_component_gt)
2.132 -qed
2.133 +  by (intro closed_INT ballI closed_Collect_le
2.134 +    continuous_at_euclidean_component continuous_const)
2.136  lemma closed_eucl_atLeast[simp, intro]:
2.137    fixes a :: "'a\<Colon>ordered_euclidean_space"
2.138    shows "closed {a ..}"
2.139    unfolding eucl_atLeast_eq_halfspaces
2.140 -proof (safe intro!: closed_INT)
2.141 -  fix i :: nat
2.142 -  have "- {x::'a. a \$\$ i \<le> x \$\$ i} = {x. x \$\$ i < a \$\$ i}" by auto
2.143 -  then show "closed {x::'a. a \$\$ i \<le> x \$\$ i}"
2.144 -    by (simp add: closed_def open_halfspace_component_lt)
2.145 -qed
2.146 +  by (intro closed_INT ballI closed_Collect_le
2.147 +    continuous_at_euclidean_component continuous_const)
2.149  lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x \$\$ i) -` S)"
2.150    by (auto intro!: continuous_open_vimage)