# HG changeset patch
# User paulson
# Date 1554997795 -3600
# Node ID 538d9854ca2f721834237bd10352e892677f28bd
# Parent  af4f723823d82c2acc6b0b128a2c7835c978b751# Parent  e0ac5e71a964e5d478ad6350563d87df7f871838
merged

diff -r af4f723823d8 -r 538d9854ca2f NEWS
--- a/NEWS	Thu Apr 11 17:07:52 2019 +0200
+++ b/NEWS	Thu Apr 11 16:49:55 2019 +0100
@@ -254,10 +254,14 @@
 * Session HOL-Number_Theory: More material on residue rings in
 Carmichael's function, primitive roots, more properties for "ord".
 
-* Session HOL-Analysis: Better organization and much more material,
-including algebraic topology.
-
-* Session HOL-Algebra: Much more material on group theory.
+* Session HOL-Homology: New, a port of HOL Light's homology library,
+with new proofs of "invariance of domain" and related results.
+
+* Session HOL-Analysis: Better organization and much more material
+at the level of abstract topological spaces.
+
+* Session HOL-Algebra: Much more material on group theory, mostly ported
+from HOL Light.
 
 * Session HOL-SPARK: .prv files are no longer written to the
 file-system, but exported to the session database. Results may be
diff -r af4f723823d8 -r 538d9854ca2f src/HOL/Analysis/Finite_Function_Topology.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Finite_Function_Topology.thy	Thu Apr 11 16:49:55 2019 +0100
@@ -0,0 +1,145 @@
+section\<open>Poly Mappings as a Real Normed Vector\<close>
+
+(*  Author:  LC Paulson
+*)
+
+theory Finite_Function_Topology
+  imports Function_Topology  "HOL-Library.Poly_Mapping" 
+           
+begin
+
+instantiation "poly_mapping" :: (type, real_vector) real_vector
+begin
+
+definition scaleR_poly_mapping_def:
+  "scaleR r x \<equiv> Abs_poly_mapping (\<lambda>i. (scaleR r (Poly_Mapping.lookup x i)))"
+
+instance
+proof 
+qed (simp_all add: scaleR_poly_mapping_def plus_poly_mapping.abs_eq eq_onp_def lookup_add scaleR_add_left scaleR_add_right)
+
+end
+
+instantiation "poly_mapping" :: (type, real_normed_vector) metric_space
+begin
+
+definition dist_poly_mapping :: "['a \<Rightarrow>\<^sub>0 'b,'a \<Rightarrow>\<^sub>0 'b] \<Rightarrow> real"
+  where dist_poly_mapping_def:
+    "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))"
+
+definition uniformity_poly_mapping:: "(('a \<Rightarrow>\<^sub>0 'b) \<times> ('a \<Rightarrow>\<^sub>0 'b)) filter"
+  where uniformity_poly_mapping_def:
+    "uniformity_poly_mapping \<equiv> INF e\<in>{0<..}. principal {(x, y). dist (x::'a\<Rightarrow>\<^sub>0'b) y < e}"
+
+definition open_poly_mapping:: "('a \<Rightarrow>\<^sub>0 'b)set \<Rightarrow> bool"
+  where open_poly_mapping_def:
+    "open_poly_mapping U \<equiv> (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"
+
+instance
+proof
+  show "uniformity = (INF e\<in>{0<..}. principal {(x, y::'a \<Rightarrow>\<^sub>0 'b). dist x y < e})"
+    by (simp add: uniformity_poly_mapping_def)
+next
+  fix U :: "('a \<Rightarrow>\<^sub>0 'b) set"
+  show "open U = (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"
+    by (simp add: open_poly_mapping_def)
+next
+  fix x :: "'a \<Rightarrow>\<^sub>0 'b" and y :: "'a \<Rightarrow>\<^sub>0 'b"
+  show "dist x y = 0 \<longleftrightarrow> x = y"
+  proof
+    assume "dist x y = 0"
+    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"
+      by (simp add: dist_poly_mapping_def)
+    then have "poly_mapping.lookup x n = poly_mapping.lookup y n"
+      if "n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y" for n
+      using that by (simp add: ordered_comm_monoid_add_class.sum_nonneg_eq_0_iff)
+    then show "x = y"
+      by (metis Un_iff in_keys_iff poly_mapping_eqI)
+  qed (simp add: dist_poly_mapping_def)
+next
+  fix x :: "'a \<Rightarrow>\<^sub>0 'b" and y :: "'a \<Rightarrow>\<^sub>0 'b" and z :: "'a \<Rightarrow>\<^sub>0 'b"
+  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))"
+    by (force simp add: dist_poly_mapping_def in_keys_iff intro: sum.mono_neutral_left)
+  also have "... \<le> (\<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) + dist (Poly_Mapping.lookup y n) (Poly_Mapping.lookup z n))"
+    by (simp add: ordered_comm_monoid_add_class.sum_mono dist_triangle2)
+  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))
+                 + (\<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))"
+    by (simp add: sum.distrib)
+  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))
+                 + (\<Sum>n \<in> Poly_Mapping.keys y \<union> Poly_Mapping.keys z. dist (Poly_Mapping.lookup y n) (Poly_Mapping.lookup z n))"
+    by (force simp add: dist_poly_mapping_def in_keys_iff intro: sum.mono_neutral_right arg_cong2 [where f = "(+)"])
+  also have "... = dist x z + dist y z"
+    by (simp add: dist_poly_mapping_def)
+  finally show "dist x y \<le> dist x z + dist y z" .
+qed
+
+end
+
+instantiation "poly_mapping" :: (type, real_normed_vector) real_normed_vector
+begin
+
+definition norm_poly_mapping :: "('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> real"
+  where norm_poly_mapping_def:
+    "norm_poly_mapping \<equiv> \<lambda>x. dist x 0"
+
+definition sgn_poly_mapping :: "('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 'b)"
+  where sgn_poly_mapping_def:
+    "sgn_poly_mapping \<equiv> \<lambda>x. x /\<^sub>R norm x"
+
+instance
+proof 
+  fix x :: "'a \<Rightarrow>\<^sub>0 'b" and y :: "'a \<Rightarrow>\<^sub>0 'b"
+  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"
+    by (force simp add: dist_poly_mapping_def in_keys_iff intro: sum.mono_neutral_left)
+  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))"
+    by (simp add: dist_poly_mapping_def)  
+  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))"
+    by (simp add: dist_norm)
+  also have "... = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup (x-y) n))"
+    by (simp add: lookup_minus)
+  also have "... = (\<Sum>n \<in> Poly_Mapping.keys (x-y). norm (poly_mapping.lookup (x-y) n))"
+    by (simp add: "0" sum.mono_neutral_cong_right keys_diff)
+  also have "... = norm (x - y)"
+    by (simp add: norm_poly_mapping_def dist_poly_mapping_def)  
+  finally show "dist x y = norm (x - y)" .
+next
+  fix x :: "'a \<Rightarrow>\<^sub>0 'b"
+  show "sgn x = x /\<^sub>R norm x"
+    by (simp add: sgn_poly_mapping_def)
+next
+  fix x :: "'a \<Rightarrow>\<^sub>0 'b"
+  show "norm x = 0 \<longleftrightarrow> x = 0"
+    by (simp add: norm_poly_mapping_def)  
+next
+  fix x :: "'a \<Rightarrow>\<^sub>0 'b" and y :: "'a \<Rightarrow>\<^sub>0 'b"
+  have "norm (x + y) = (\<Sum>n \<in> Poly_Mapping.keys (x + y). norm (poly_mapping.lookup x n + poly_mapping.lookup y n))"
+    by (simp add: norm_poly_mapping_def dist_poly_mapping_def lookup_add)
+  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))"
+    by (auto simp: simp add: plus_poly_mapping.rep_eq in_keys_iff intro: sum.mono_neutral_left)
+  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))"
+    by (simp add: norm_triangle_ineq sum_mono)
+  also have "... = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup x n))
+                 + (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup y n))"
+    by (simp add: sum.distrib)
+  also have "... = (\<Sum>n \<in> Poly_Mapping.keys x. norm (poly_mapping.lookup x n))
+                 + (\<Sum>n \<in> Poly_Mapping.keys y. norm (poly_mapping.lookup y n))"
+    by (force simp add: in_keys_iff intro: arg_cong2 [where f = "(+)"] sum.mono_neutral_right)
+  also have "... = norm x + norm y"
+    by (simp add: norm_poly_mapping_def dist_poly_mapping_def)
+  finally show "norm (x + y) \<le> norm x + norm y" .
+next
+  fix a :: "real" and x :: "'a \<Rightarrow>\<^sub>0 'b"
+  show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
+  proof (cases "a = 0")
+    case False
+    then have [simp]: "Poly_Mapping.keys (a *\<^sub>R x) = Poly_Mapping.keys x"
+      by (auto simp add: scaleR_poly_mapping_def in_keys_iff)
+    then show ?thesis
+      by (simp add: norm_poly_mapping_def dist_poly_mapping_def scaleR_poly_mapping_def sum_distrib_left)
+  qed (simp add: norm_poly_mapping_def)
+qed
+
+end
+
+end
diff -r af4f723823d8 -r 538d9854ca2f src/HOL/Homology/Invariance_of_Domain.thy
--- a/src/HOL/Homology/Invariance_of_Domain.thy	Thu Apr 11 17:07:52 2019 +0200
+++ b/src/HOL/Homology/Invariance_of_Domain.thy	Thu Apr 11 16:49:55 2019 +0100
@@ -2970,4 +2970,63 @@
     using not_less by blast
 qed
 
+lemma empty_interior_lowdim_gen:
+  fixes S :: "'N::euclidean_space set" and T :: "'M::euclidean_space set"
+  assumes dim: "DIM('M) < DIM('N)" and ST: "S homeomorphic T" 
+  shows "interior S = {}"
+proof -
+  obtain h :: "'M \<Rightarrow> 'N" where "linear h" "\<And>x. norm(h x) = norm x"
+    by (rule isometry_subset_subspace [OF subspace_UNIV subspace_UNIV, where ?'a = 'M and ?'b = 'N])
+       (use dim in auto)
+  then have "inj h"
+    by (metis linear_inj_iff_eq_0 norm_eq_zero)
+  then have "h ` T homeomorphic T"
+    using \<open>linear h\<close> homeomorphic_sym linear_homeomorphic_image by blast
+  then have "interior (h ` T) homeomorphic interior S"
+    using homeomorphic_interiors_same_dimension
+    by (metis ST homeomorphic_sym homeomorphic_trans)
+  moreover   
+  have "interior (range h) = {}"
+    by (simp add: \<open>inj h\<close> \<open>linear h\<close> dim dim_image_eq empty_interior_lowdim)
+  then have "interior (h ` T) = {}"
+    by (metis image_mono interior_mono subset_empty top_greatest)
+  ultimately show ?thesis
+    by simp
+qed
+
+lemma empty_interior_lowdim_gen_le:
+  fixes S :: "'N::euclidean_space set" and T :: "'M::euclidean_space set"
+  assumes "DIM('M) \<le> DIM('N)"  "interior T = {}" "S homeomorphic T" 
+  shows "interior S = {}"
+  by (metis assms empty_interior_lowdim_gen homeomorphic_empty(1) homeomorphic_interiors_same_dimension less_le)
+
+lemma homeomorphic_affine_sets_eq:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "affine S" "affine T"
+  shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
+proof (cases "S = {} \<or> T = {}")
+  case True
+  then show ?thesis
+    using assms homeomorphic_affine_sets by force
+next
+  case False
+  then obtain a b where "a \<in> S" "b \<in> T"
+    by blast
+  then have "subspace ((+) (- a) ` S)" "subspace ((+) (- b) ` T)"
+    using affine_diffs_subspace assms by blast+
+  then show ?thesis
+    by (metis affine_imp_convex assms homeomorphic_affine_sets homeomorphic_convex_sets)
+qed
+
+lemma homeomorphic_hyperplanes_eq:
+  fixes a :: "'M::euclidean_space" and c :: "'N::euclidean_space"
+  assumes "a \<noteq> 0" "c \<noteq> 0" 
+  shows "({x. a \<bullet> x = b} homeomorphic {x. c \<bullet> x = d} \<longleftrightarrow> DIM('M) = DIM('N))" (is "?lhs = ?rhs")
+proof -
+  have "(DIM('M) - Suc 0 = DIM('N) - Suc 0) \<longleftrightarrow> (DIM('M) = DIM('N))"
+    by auto (metis DIM_positive Suc_pred)
+  then show ?thesis
+    using assms by (simp add: homeomorphic_affine_sets_eq affine_hyperplane)
+qed
+
 end
diff -r af4f723823d8 -r 538d9854ca2f src/HOL/Probability/Conditional_Expectation.thy
--- a/src/HOL/Probability/Conditional_Expectation.thy	Thu Apr 11 17:07:52 2019 +0200
+++ b/src/HOL/Probability/Conditional_Expectation.thy	Thu Apr 11 16:49:55 2019 +0100
@@ -994,7 +994,7 @@
   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
   proof -
     have "real_cond_exp M F f x \<ge> u n" for n using that less_imp_le by auto
-    then show ?thesis using u(2) LIMSEQ_le_const2 by blast
+    then show ?thesis using u(2) LIMSEQ_le_const2 by metis
   qed
   ultimately show ?thesis by auto
 qed