merged
authorpaulson
Thu Apr 11 16:49:55 2019 +0100 (5 months ago)
changeset 70127538d9854ca2f
parent 70124 af4f723823d8
parent 70126 e0ac5e71a964
child 70128 f2f797260010
merged
NEWS
     1.1 --- a/NEWS	Thu Apr 11 17:07:52 2019 +0200
     1.2 +++ b/NEWS	Thu Apr 11 16:49:55 2019 +0100
     1.3 @@ -254,10 +254,14 @@
     1.4  * Session HOL-Number_Theory: More material on residue rings in
     1.5  Carmichael's function, primitive roots, more properties for "ord".
     1.6  
     1.7 -* Session HOL-Analysis: Better organization and much more material,
     1.8 -including algebraic topology.
     1.9 -
    1.10 -* Session HOL-Algebra: Much more material on group theory.
    1.11 +* Session HOL-Homology: New, a port of HOL Light's homology library,
    1.12 +with new proofs of "invariance of domain" and related results.
    1.13 +
    1.14 +* Session HOL-Analysis: Better organization and much more material
    1.15 +at the level of abstract topological spaces.
    1.16 +
    1.17 +* Session HOL-Algebra: Much more material on group theory, mostly ported
    1.18 +from HOL Light.
    1.19  
    1.20  * Session HOL-SPARK: .prv files are no longer written to the
    1.21  file-system, but exported to the session database. Results may be
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Analysis/Finite_Function_Topology.thy	Thu Apr 11 16:49:55 2019 +0100
     2.3 @@ -0,0 +1,145 @@
     2.4 +section\<open>Poly Mappings as a Real Normed Vector\<close>
     2.5 +
     2.6 +(*  Author:  LC Paulson
     2.7 +*)
     2.8 +
     2.9 +theory Finite_Function_Topology
    2.10 +  imports Function_Topology  "HOL-Library.Poly_Mapping" 
    2.11 +           
    2.12 +begin
    2.13 +
    2.14 +instantiation "poly_mapping" :: (type, real_vector) real_vector
    2.15 +begin
    2.16 +
    2.17 +definition scaleR_poly_mapping_def:
    2.18 +  "scaleR r x \<equiv> Abs_poly_mapping (\<lambda>i. (scaleR r (Poly_Mapping.lookup x i)))"
    2.19 +
    2.20 +instance
    2.21 +proof 
    2.22 +qed (simp_all add: scaleR_poly_mapping_def plus_poly_mapping.abs_eq eq_onp_def lookup_add scaleR_add_left scaleR_add_right)
    2.23 +
    2.24 +end
    2.25 +
    2.26 +instantiation "poly_mapping" :: (type, real_normed_vector) metric_space
    2.27 +begin
    2.28 +
    2.29 +definition dist_poly_mapping :: "['a \<Rightarrow>\<^sub>0 'b,'a \<Rightarrow>\<^sub>0 'b] \<Rightarrow> real"
    2.30 +  where dist_poly_mapping_def:
    2.31 +    "dist_poly_mapping \<equiv> \<lambda>x y. (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. dist (Poly_Mapping.lookup x n) (Poly_Mapping.lookup y n))"
    2.32 +
    2.33 +definition uniformity_poly_mapping:: "(('a \<Rightarrow>\<^sub>0 'b) \<times> ('a \<Rightarrow>\<^sub>0 'b)) filter"
    2.34 +  where uniformity_poly_mapping_def:
    2.35 +    "uniformity_poly_mapping \<equiv> INF e\<in>{0<..}. principal {(x, y). dist (x::'a\<Rightarrow>\<^sub>0'b) y < e}"
    2.36 +
    2.37 +definition open_poly_mapping:: "('a \<Rightarrow>\<^sub>0 'b)set \<Rightarrow> bool"
    2.38 +  where open_poly_mapping_def:
    2.39 +    "open_poly_mapping U \<equiv> (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"
    2.40 +
    2.41 +instance
    2.42 +proof
    2.43 +  show "uniformity = (INF e\<in>{0<..}. principal {(x, y::'a \<Rightarrow>\<^sub>0 'b). dist x y < e})"
    2.44 +    by (simp add: uniformity_poly_mapping_def)
    2.45 +next
    2.46 +  fix U :: "('a \<Rightarrow>\<^sub>0 'b) set"
    2.47 +  show "open U = (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"
    2.48 +    by (simp add: open_poly_mapping_def)
    2.49 +next
    2.50 +  fix x :: "'a \<Rightarrow>\<^sub>0 'b" and y :: "'a \<Rightarrow>\<^sub>0 'b"
    2.51 +  show "dist x y = 0 \<longleftrightarrow> x = y"
    2.52 +  proof
    2.53 +    assume "dist x y = 0"
    2.54 +    then have "(\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. dist (poly_mapping.lookup x n) (poly_mapping.lookup y n)) = 0"
    2.55 +      by (simp add: dist_poly_mapping_def)
    2.56 +    then have "poly_mapping.lookup x n = poly_mapping.lookup y n"
    2.57 +      if "n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y" for n
    2.58 +      using that by (simp add: ordered_comm_monoid_add_class.sum_nonneg_eq_0_iff)
    2.59 +    then show "x = y"
    2.60 +      by (metis Un_iff in_keys_iff poly_mapping_eqI)
    2.61 +  qed (simp add: dist_poly_mapping_def)
    2.62 +next
    2.63 +  fix x :: "'a \<Rightarrow>\<^sub>0 'b" and y :: "'a \<Rightarrow>\<^sub>0 'b" and z :: "'a \<Rightarrow>\<^sub>0 'b"
    2.64 +  have "dist x y = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y \<union> Poly_Mapping.keys z. dist (Poly_Mapping.lookup x n) (Poly_Mapping.lookup y n))"
    2.65 +    by (force simp add: dist_poly_mapping_def in_keys_iff intro: sum.mono_neutral_left)
    2.66 +  also have "... \<le> (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y \<union> Poly_Mapping.keys z. 
    2.67 +                     dist (Poly_Mapping.lookup x n) (Poly_Mapping.lookup z n) + dist (Poly_Mapping.lookup y n) (Poly_Mapping.lookup z n))"
    2.68 +    by (simp add: ordered_comm_monoid_add_class.sum_mono dist_triangle2)
    2.69 +  also have "... = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y \<union> Poly_Mapping.keys z. dist (Poly_Mapping.lookup x n) (Poly_Mapping.lookup z n))
    2.70 +                 + (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y \<union> Poly_Mapping.keys z. dist (Poly_Mapping.lookup y n) (Poly_Mapping.lookup z n))"
    2.71 +    by (simp add: sum.distrib)
    2.72 +  also have "... = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys z. dist (Poly_Mapping.lookup x n) (Poly_Mapping.lookup z n))
    2.73 +                 + (\<Sum>n \<in> Poly_Mapping.keys y \<union> Poly_Mapping.keys z. dist (Poly_Mapping.lookup y n) (Poly_Mapping.lookup z n))"
    2.74 +    by (force simp add: dist_poly_mapping_def in_keys_iff intro: sum.mono_neutral_right arg_cong2 [where f = "(+)"])
    2.75 +  also have "... = dist x z + dist y z"
    2.76 +    by (simp add: dist_poly_mapping_def)
    2.77 +  finally show "dist x y \<le> dist x z + dist y z" .
    2.78 +qed
    2.79 +
    2.80 +end
    2.81 +
    2.82 +instantiation "poly_mapping" :: (type, real_normed_vector) real_normed_vector
    2.83 +begin
    2.84 +
    2.85 +definition norm_poly_mapping :: "('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> real"
    2.86 +  where norm_poly_mapping_def:
    2.87 +    "norm_poly_mapping \<equiv> \<lambda>x. dist x 0"
    2.88 +
    2.89 +definition sgn_poly_mapping :: "('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 'b)"
    2.90 +  where sgn_poly_mapping_def:
    2.91 +    "sgn_poly_mapping \<equiv> \<lambda>x. x /\<^sub>R norm x"
    2.92 +
    2.93 +instance
    2.94 +proof 
    2.95 +  fix x :: "'a \<Rightarrow>\<^sub>0 'b" and y :: "'a \<Rightarrow>\<^sub>0 'b"
    2.96 +  have 0: "\<forall>i\<in>Poly_Mapping.keys x \<union> Poly_Mapping.keys y - Poly_Mapping.keys (x - y). norm (poly_mapping.lookup (x - y) i) = 0"
    2.97 +    by (force simp add: dist_poly_mapping_def in_keys_iff intro: sum.mono_neutral_left)
    2.98 +  have "dist x y = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. dist (poly_mapping.lookup x n) (poly_mapping.lookup y n))"
    2.99 +    by (simp add: dist_poly_mapping_def)  
   2.100 +  also have "... = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup x n - poly_mapping.lookup y n))"
   2.101 +    by (simp add: dist_norm)
   2.102 +  also have "... = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup (x-y) n))"
   2.103 +    by (simp add: lookup_minus)
   2.104 +  also have "... = (\<Sum>n \<in> Poly_Mapping.keys (x-y). norm (poly_mapping.lookup (x-y) n))"
   2.105 +    by (simp add: "0" sum.mono_neutral_cong_right keys_diff)
   2.106 +  also have "... = norm (x - y)"
   2.107 +    by (simp add: norm_poly_mapping_def dist_poly_mapping_def)  
   2.108 +  finally show "dist x y = norm (x - y)" .
   2.109 +next
   2.110 +  fix x :: "'a \<Rightarrow>\<^sub>0 'b"
   2.111 +  show "sgn x = x /\<^sub>R norm x"
   2.112 +    by (simp add: sgn_poly_mapping_def)
   2.113 +next
   2.114 +  fix x :: "'a \<Rightarrow>\<^sub>0 'b"
   2.115 +  show "norm x = 0 \<longleftrightarrow> x = 0"
   2.116 +    by (simp add: norm_poly_mapping_def)  
   2.117 +next
   2.118 +  fix x :: "'a \<Rightarrow>\<^sub>0 'b" and y :: "'a \<Rightarrow>\<^sub>0 'b"
   2.119 +  have "norm (x + y) = (\<Sum>n \<in> Poly_Mapping.keys (x + y). norm (poly_mapping.lookup x n + poly_mapping.lookup y n))"
   2.120 +    by (simp add: norm_poly_mapping_def dist_poly_mapping_def lookup_add)
   2.121 +  also have "... = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup x n + poly_mapping.lookup y n))"
   2.122 +    by (auto simp: simp add: plus_poly_mapping.rep_eq in_keys_iff intro: sum.mono_neutral_left)
   2.123 +  also have "... \<le> (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup x n) + norm (poly_mapping.lookup y n))"
   2.124 +    by (simp add: norm_triangle_ineq sum_mono)
   2.125 +  also have "... = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup x n))
   2.126 +                 + (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup y n))"
   2.127 +    by (simp add: sum.distrib)
   2.128 +  also have "... = (\<Sum>n \<in> Poly_Mapping.keys x. norm (poly_mapping.lookup x n))
   2.129 +                 + (\<Sum>n \<in> Poly_Mapping.keys y. norm (poly_mapping.lookup y n))"
   2.130 +    by (force simp add: in_keys_iff intro: arg_cong2 [where f = "(+)"] sum.mono_neutral_right)
   2.131 +  also have "... = norm x + norm y"
   2.132 +    by (simp add: norm_poly_mapping_def dist_poly_mapping_def)
   2.133 +  finally show "norm (x + y) \<le> norm x + norm y" .
   2.134 +next
   2.135 +  fix a :: "real" and x :: "'a \<Rightarrow>\<^sub>0 'b"
   2.136 +  show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
   2.137 +  proof (cases "a = 0")
   2.138 +    case False
   2.139 +    then have [simp]: "Poly_Mapping.keys (a *\<^sub>R x) = Poly_Mapping.keys x"
   2.140 +      by (auto simp add: scaleR_poly_mapping_def in_keys_iff)
   2.141 +    then show ?thesis
   2.142 +      by (simp add: norm_poly_mapping_def dist_poly_mapping_def scaleR_poly_mapping_def sum_distrib_left)
   2.143 +  qed (simp add: norm_poly_mapping_def)
   2.144 +qed
   2.145 +
   2.146 +end
   2.147 +
   2.148 +end
     3.1 --- a/src/HOL/Homology/Invariance_of_Domain.thy	Thu Apr 11 17:07:52 2019 +0200
     3.2 +++ b/src/HOL/Homology/Invariance_of_Domain.thy	Thu Apr 11 16:49:55 2019 +0100
     3.3 @@ -2970,4 +2970,63 @@
     3.4      using not_less by blast
     3.5  qed
     3.6  
     3.7 +lemma empty_interior_lowdim_gen:
     3.8 +  fixes S :: "'N::euclidean_space set" and T :: "'M::euclidean_space set"
     3.9 +  assumes dim: "DIM('M) < DIM('N)" and ST: "S homeomorphic T" 
    3.10 +  shows "interior S = {}"
    3.11 +proof -
    3.12 +  obtain h :: "'M \<Rightarrow> 'N" where "linear h" "\<And>x. norm(h x) = norm x"
    3.13 +    by (rule isometry_subset_subspace [OF subspace_UNIV subspace_UNIV, where ?'a = 'M and ?'b = 'N])
    3.14 +       (use dim in auto)
    3.15 +  then have "inj h"
    3.16 +    by (metis linear_inj_iff_eq_0 norm_eq_zero)
    3.17 +  then have "h ` T homeomorphic T"
    3.18 +    using \<open>linear h\<close> homeomorphic_sym linear_homeomorphic_image by blast
    3.19 +  then have "interior (h ` T) homeomorphic interior S"
    3.20 +    using homeomorphic_interiors_same_dimension
    3.21 +    by (metis ST homeomorphic_sym homeomorphic_trans)
    3.22 +  moreover   
    3.23 +  have "interior (range h) = {}"
    3.24 +    by (simp add: \<open>inj h\<close> \<open>linear h\<close> dim dim_image_eq empty_interior_lowdim)
    3.25 +  then have "interior (h ` T) = {}"
    3.26 +    by (metis image_mono interior_mono subset_empty top_greatest)
    3.27 +  ultimately show ?thesis
    3.28 +    by simp
    3.29 +qed
    3.30 +
    3.31 +lemma empty_interior_lowdim_gen_le:
    3.32 +  fixes S :: "'N::euclidean_space set" and T :: "'M::euclidean_space set"
    3.33 +  assumes "DIM('M) \<le> DIM('N)"  "interior T = {}" "S homeomorphic T" 
    3.34 +  shows "interior S = {}"
    3.35 +  by (metis assms empty_interior_lowdim_gen homeomorphic_empty(1) homeomorphic_interiors_same_dimension less_le)
    3.36 +
    3.37 +lemma homeomorphic_affine_sets_eq:
    3.38 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
    3.39 +  assumes "affine S" "affine T"
    3.40 +  shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
    3.41 +proof (cases "S = {} \<or> T = {}")
    3.42 +  case True
    3.43 +  then show ?thesis
    3.44 +    using assms homeomorphic_affine_sets by force
    3.45 +next
    3.46 +  case False
    3.47 +  then obtain a b where "a \<in> S" "b \<in> T"
    3.48 +    by blast
    3.49 +  then have "subspace ((+) (- a) ` S)" "subspace ((+) (- b) ` T)"
    3.50 +    using affine_diffs_subspace assms by blast+
    3.51 +  then show ?thesis
    3.52 +    by (metis affine_imp_convex assms homeomorphic_affine_sets homeomorphic_convex_sets)
    3.53 +qed
    3.54 +
    3.55 +lemma homeomorphic_hyperplanes_eq:
    3.56 +  fixes a :: "'M::euclidean_space" and c :: "'N::euclidean_space"
    3.57 +  assumes "a \<noteq> 0" "c \<noteq> 0" 
    3.58 +  shows "({x. a \<bullet> x = b} homeomorphic {x. c \<bullet> x = d} \<longleftrightarrow> DIM('M) = DIM('N))" (is "?lhs = ?rhs")
    3.59 +proof -
    3.60 +  have "(DIM('M) - Suc 0 = DIM('N) - Suc 0) \<longleftrightarrow> (DIM('M) = DIM('N))"
    3.61 +    by auto (metis DIM_positive Suc_pred)
    3.62 +  then show ?thesis
    3.63 +    using assms by (simp add: homeomorphic_affine_sets_eq affine_hyperplane)
    3.64 +qed
    3.65 +
    3.66  end
     4.1 --- a/src/HOL/Probability/Conditional_Expectation.thy	Thu Apr 11 17:07:52 2019 +0200
     4.2 +++ b/src/HOL/Probability/Conditional_Expectation.thy	Thu Apr 11 16:49:55 2019 +0100
     4.3 @@ -994,7 +994,7 @@
     4.4    moreover have "real_cond_exp M F f x \<ge> c" if "\<forall>n. real_cond_exp M F f x > u n" for x
     4.5    proof -
     4.6      have "real_cond_exp M F f x \<ge> u n" for n using that less_imp_le by auto
     4.7 -    then show ?thesis using u(2) LIMSEQ_le_const2 by blast
     4.8 +    then show ?thesis using u(2) LIMSEQ_le_const2 by metis
     4.9    qed
    4.10    ultimately show ?thesis by auto
    4.11  qed