# HG changeset patch
# User immler
# Date 1572905905 18000
# Node ID be8cec1abcbb113fd3e6c41413da9f82a47a0f29
# Parent  38bed2483e6a99283f42f2c99b1264f05881c876
reduce dependencies of Ordered_Euclidean_Space; move more general material from Cartesian_Euclidean_Space

diff -r 38bed2483e6a -r be8cec1abcbb src/HOL/Analysis/Arcwise_Connected.thy
--- a/src/HOL/Analysis/Arcwise_Connected.thy	Mon Nov 04 20:24:52 2019 +0100
+++ b/src/HOL/Analysis/Arcwise_Connected.thy	Mon Nov 04 17:18:25 2019 -0500
@@ -8,6 +8,11 @@
 imports Path_Connected Ordered_Euclidean_Space "HOL-Computational_Algebra.Primes"
 begin
 
+lemma path_connected_interval [simp]:
+  fixes a b::"'a::ordered_euclidean_space"
+  shows "path_connected {a..b}"
+  using is_interval_cc is_interval_path_connected by blast
+
 subsection \<open>The Brouwer reduction theorem\<close>
 
 theorem Brouwer_reduction_theorem_gen:
diff -r 38bed2483e6a -r be8cec1abcbb src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Mon Nov 04 20:24:52 2019 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy	Mon Nov 04 17:18:25 2019 -0500
@@ -10,6 +10,9 @@
   Measurable Derivative Ordered_Euclidean_Space Extended_Real_Limits
 begin
 
+lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
+  by (auto simp: real_atLeastGreaterThan_eq)
+
 lemma sets_Collect_eventually_sequentially[measurable]:
   "(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
   unfolding eventually_sequentially by simp
diff -r 38bed2483e6a -r be8cec1abcbb src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Nov 04 20:24:52 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Nov 04 17:18:25 2019 -0500
@@ -47,33 +47,6 @@
 
 subsection\<open>Closures and interiors of halfspaces\<close>
 
-lemma interior_halfspace_le [simp]:
-  assumes "a \<noteq> 0"
-    shows "interior {x. a \<bullet> x \<le> b} = {x. a \<bullet> x < b}"
-proof -
-  have *: "a \<bullet> x < b" if x: "x \<in> S" and S: "S \<subseteq> {x. a \<bullet> x \<le> b}" and "open S" for S x
-  proof -
-    obtain e where "e>0" and e: "cball x e \<subseteq> S"
-      using \<open>open S\<close> open_contains_cball x by blast
-    then have "x + (e / norm a) *\<^sub>R a \<in> cball x e"
-      by (simp add: dist_norm)
-    then have "x + (e / norm a) *\<^sub>R a \<in> S"
-      using e by blast
-    then have "x + (e / norm a) *\<^sub>R a \<in> {x. a \<bullet> x \<le> b}"
-      using S by blast
-    moreover have "e * (a \<bullet> a) / norm a > 0"
-      by (simp add: \<open>0 < e\<close> assms)
-    ultimately show ?thesis
-      by (simp add: algebra_simps)
-  qed
-  show ?thesis
-    by (rule interior_unique) (auto simp: open_halfspace_lt *)
-qed
-
-lemma interior_halfspace_ge [simp]:
-   "a \<noteq> 0 \<Longrightarrow> interior {x. a \<bullet> x \<ge> b} = {x. a \<bullet> x > b}"
-using interior_halfspace_le [of "-a" "-b"] by simp
-
 lemma interior_halfspace_component_le [simp]:
      "interior {x. x$k \<le> a} = {x :: (real^'n). x$k < a}" (is "?LE")
   and interior_halfspace_component_ge [simp]:
@@ -88,21 +61,6 @@
           interior_halfspace_ge [of "axis k (1::real)" a] by auto
 qed
 
-lemma closure_halfspace_lt [simp]:
-  assumes "a \<noteq> 0"
-    shows "closure {x. a \<bullet> x < b} = {x. a \<bullet> x \<le> b}"
-proof -
-  have [simp]: "-{x. a \<bullet> x < b} = {x. a \<bullet> x \<ge> b}"
-    by (force simp:)
-  then show ?thesis
-    using interior_halfspace_ge [of a b] assms
-    by (force simp: closure_interior)
-qed
-
-lemma closure_halfspace_gt [simp]:
-   "a \<noteq> 0 \<Longrightarrow> closure {x. a \<bullet> x > b} = {x. a \<bullet> x \<ge> b}"
-using closure_halfspace_lt [of "-a" "-b"] by simp
-
 lemma closure_halfspace_component_lt [simp]:
      "closure {x. x$k < a} = {x :: (real^'n). x$k \<le> a}" (is "?LE")
   and closure_halfspace_component_gt [simp]:
@@ -117,56 +75,6 @@
           closure_halfspace_gt [of "axis k (1::real)" a] by auto
 qed
 
-lemma interior_hyperplane [simp]:
-  assumes "a \<noteq> 0"
-    shows "interior {x. a \<bullet> x = b} = {}"
-proof -
-  have [simp]: "{x. a \<bullet> x = b} = {x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x \<ge> b}"
-    by (force simp:)
-  then show ?thesis
-    by (auto simp: assms)
-qed
-
-lemma frontier_halfspace_le:
-  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
-    shows "frontier {x. a \<bullet> x \<le> b} = {x. a \<bullet> x = b}"
-proof (cases "a = 0")
-  case True with assms show ?thesis by simp
-next
-  case False then show ?thesis
-    by (force simp: frontier_def closed_halfspace_le)
-qed
-
-lemma frontier_halfspace_ge:
-  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
-    shows "frontier {x. a \<bullet> x \<ge> b} = {x. a \<bullet> x = b}"
-proof (cases "a = 0")
-  case True with assms show ?thesis by simp
-next
-  case False then show ?thesis
-    by (force simp: frontier_def closed_halfspace_ge)
-qed
-
-lemma frontier_halfspace_lt:
-  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
-    shows "frontier {x. a \<bullet> x < b} = {x. a \<bullet> x = b}"
-proof (cases "a = 0")
-  case True with assms show ?thesis by simp
-next
-  case False then show ?thesis
-    by (force simp: frontier_def interior_open open_halfspace_lt)
-qed
-
-lemma frontier_halfspace_gt:
-  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
-    shows "frontier {x. a \<bullet> x > b} = {x. a \<bullet> x = b}"
-proof (cases "a = 0")
-  case True with assms show ?thesis by simp
-next
-  case False then show ?thesis
-    by (force simp: frontier_def interior_open open_halfspace_gt)
-qed
-
 lemma interior_standard_hyperplane:
    "interior {x :: (real^'n). x$k = a} = {}"
 proof -
@@ -623,6 +531,11 @@
   qed
 qed simp
 
+lemma vec_nth_real_1_iff_cbox [simp]:
+  fixes a b :: real
+  shows "(\<lambda>x::real^1. x $ 1) ` S = {a..b} \<longleftrightarrow> S = cbox (vec a) (vec b)"
+  using vec_nth_1_iff_cbox[of S a b]
+  by simp
 
 lemma interval_split_cart:
   "{a..b::real^'n} \<inter> {x. x$k \<le> c} = {a .. (\<chi> i. if i = k then min (b$k) c else b$i)}"
diff -r 38bed2483e6a -r be8cec1abcbb src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Nov 04 20:24:52 2019 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Nov 04 17:18:25 2019 -0500
@@ -5,7 +5,13 @@
 *)
 
 theory Equivalence_Lebesgue_Henstock_Integration
-  imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure Set_Integral Homeomorphism
+  imports
+    Lebesgue_Measure
+    Henstock_Kurzweil_Integration
+    Complete_Measure
+    Set_Integral
+    Homeomorphism
+    Cartesian_Euclidean_Space
 begin
 
 lemma le_left_mono: "x \<le> y \<Longrightarrow> y \<le> a \<longrightarrow> x \<le> (a::'a::preorder)"
diff -r 38bed2483e6a -r be8cec1abcbb src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Mon Nov 04 20:24:52 2019 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Mon Nov 04 17:18:25 2019 -0500
@@ -2,7 +2,7 @@
 
 theory Ordered_Euclidean_Space
 imports
-  Cartesian_Euclidean_Space Path_Connected
+  Convex_Euclidean_Space
   "HOL-Library.Product_Order"
 begin
 
@@ -205,11 +205,6 @@
     and eucl_le_atLeast: "{x. \<forall>i\<in>Basis. a \<bullet> i <= x \<bullet> i} = {a..}"
   by (auto simp: eucl_le[where 'a='a] eucl_less_def box_def cbox_def)
 
-lemma vec_nth_real_1_iff_cbox [simp]:
-  fixes a b :: real
-  shows "(\<lambda>x::real^1. x $ 1) ` S = {a..b} \<longleftrightarrow> S = cbox (vec a) (vec b)"
-  by (metis interval_cbox vec_nth_1_iff_cbox)
-
 lemma sums_vec_nth :
   assumes "f sums a"
   shows "(\<lambda>x. f x $ i) sums a $ i"
@@ -266,35 +261,6 @@
   shows "connected {a..b}"
   using is_interval_cc is_interval_connected by blast
 
-lemma path_connected_interval [simp]:
-  fixes a b::"'a::ordered_euclidean_space"
-  shows "path_connected {a..b}"
-  using is_interval_cc is_interval_path_connected by blast
-
-lemma path_connected_Ioi[simp]: "path_connected {a<..}" for a :: real
-  by (simp add: convex_imp_path_connected)
-
-lemma path_connected_Ici[simp]: "path_connected {a..}" for a :: real
-  by (simp add: convex_imp_path_connected)
-
-lemma path_connected_Iio[simp]: "path_connected {..<a}" for a :: real
-  by (simp add: convex_imp_path_connected)
-
-lemma path_connected_Iic[simp]: "path_connected {..a}" for a :: real
-  by (simp add: convex_imp_path_connected)
-
-lemma path_connected_Ioo[simp]: "path_connected {a<..<b}" for a b :: real
-  by (simp add: convex_imp_path_connected)
-
-lemma path_connected_Ioc[simp]: "path_connected {a<..b}" for a b :: real
-  by (simp add: convex_imp_path_connected)
-
-lemma path_connected_Ico[simp]: "path_connected {a..<b}" for a b :: real
-  by (simp add: convex_imp_path_connected)
-
-lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
-  by (auto simp: real_atLeastGreaterThan_eq)
-
 lemma compact_interval [simp]:
   fixes a b::"'a::ordered_euclidean_space"
   shows "compact {a .. b}"
diff -r 38bed2483e6a -r be8cec1abcbb src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Mon Nov 04 20:24:52 2019 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Mon Nov 04 17:18:25 2019 -0500
@@ -1826,6 +1826,27 @@
 lemma is_interval_path_connected: "is_interval S \<Longrightarrow> path_connected S"
   by (simp add: convex_imp_path_connected is_interval_convex)
 
+lemma path_connected_Ioi[simp]: "path_connected {a<..}" for a :: real
+  by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Ici[simp]: "path_connected {a..}" for a :: real
+  by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Iio[simp]: "path_connected {..<a}" for a :: real
+  by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Iic[simp]: "path_connected {..a}" for a :: real
+  by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Ioo[simp]: "path_connected {a<..<b}" for a b :: real
+  by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Ioc[simp]: "path_connected {a<..b}" for a b :: real
+  by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Ico[simp]: "path_connected {a..<b}" for a b :: real
+  by (simp add: convex_imp_path_connected)
+
 lemma path_connectedin_path_image:
   assumes "pathin X g" shows "path_connectedin X (g ` ({0..1}))"
   unfolding pathin_def
diff -r 38bed2483e6a -r be8cec1abcbb src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Nov 04 20:24:52 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Nov 04 17:18:25 2019 -0500
@@ -1175,7 +1175,7 @@
   shows "open {x. x <e a}" "open {x. a <e x}"
   by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
 
-subsection\<^marker>\<open>tag unimportant\<close> \<open>Closure of halfspaces and hyperplanes\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Closure and Interior of halfspaces and hyperplanes\<close>
 
 lemma continuous_at_inner: "continuous (at x) (inner a)"
   unfolding continuous_at by (intro tendsto_intros)
@@ -1205,6 +1205,97 @@
   shows "closed {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i}"
   by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
 
+lemma interior_halfspace_le [simp]:
+  assumes "a \<noteq> 0"
+    shows "interior {x. a \<bullet> x \<le> b} = {x. a \<bullet> x < b}"
+proof -
+  have *: "a \<bullet> x < b" if x: "x \<in> S" and S: "S \<subseteq> {x. a \<bullet> x \<le> b}" and "open S" for S x
+  proof -
+    obtain e where "e>0" and e: "cball x e \<subseteq> S"
+      using \<open>open S\<close> open_contains_cball x by blast
+    then have "x + (e / norm a) *\<^sub>R a \<in> cball x e"
+      by (simp add: dist_norm)
+    then have "x + (e / norm a) *\<^sub>R a \<in> S"
+      using e by blast
+    then have "x + (e / norm a) *\<^sub>R a \<in> {x. a \<bullet> x \<le> b}"
+      using S by blast
+    moreover have "e * (a \<bullet> a) / norm a > 0"
+      by (simp add: \<open>0 < e\<close> assms)
+    ultimately show ?thesis
+      by (simp add: algebra_simps)
+  qed
+  show ?thesis
+    by (rule interior_unique) (auto simp: open_halfspace_lt *)
+qed
+
+lemma interior_halfspace_ge [simp]:
+   "a \<noteq> 0 \<Longrightarrow> interior {x. a \<bullet> x \<ge> b} = {x. a \<bullet> x > b}"
+using interior_halfspace_le [of "-a" "-b"] by simp
+
+lemma closure_halfspace_lt [simp]:
+  assumes "a \<noteq> 0"
+    shows "closure {x. a \<bullet> x < b} = {x. a \<bullet> x \<le> b}"
+proof -
+  have [simp]: "-{x. a \<bullet> x < b} = {x. a \<bullet> x \<ge> b}"
+    by (force simp:)
+  then show ?thesis
+    using interior_halfspace_ge [of a b] assms
+    by (force simp: closure_interior)
+qed
+
+lemma closure_halfspace_gt [simp]:
+   "a \<noteq> 0 \<Longrightarrow> closure {x. a \<bullet> x > b} = {x. a \<bullet> x \<ge> b}"
+using closure_halfspace_lt [of "-a" "-b"] by simp
+
+lemma interior_hyperplane [simp]:
+  assumes "a \<noteq> 0"
+    shows "interior {x. a \<bullet> x = b} = {}"
+proof -
+  have [simp]: "{x. a \<bullet> x = b} = {x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x \<ge> b}"
+    by (force simp:)
+  then show ?thesis
+    by (auto simp: assms)
+qed
+
+lemma frontier_halfspace_le:
+  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
+    shows "frontier {x. a \<bullet> x \<le> b} = {x. a \<bullet> x = b}"
+proof (cases "a = 0")
+  case True with assms show ?thesis by simp
+next
+  case False then show ?thesis
+    by (force simp: frontier_def closed_halfspace_le)
+qed
+
+lemma frontier_halfspace_ge:
+  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
+    shows "frontier {x. a \<bullet> x \<ge> b} = {x. a \<bullet> x = b}"
+proof (cases "a = 0")
+  case True with assms show ?thesis by simp
+next
+  case False then show ?thesis
+    by (force simp: frontier_def closed_halfspace_ge)
+qed
+
+lemma frontier_halfspace_lt:
+  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
+    shows "frontier {x. a \<bullet> x < b} = {x. a \<bullet> x = b}"
+proof (cases "a = 0")
+  case True with assms show ?thesis by simp
+next
+  case False then show ?thesis
+    by (force simp: frontier_def interior_open open_halfspace_lt)
+qed
+
+lemma frontier_halfspace_gt:
+  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
+    shows "frontier {x. a \<bullet> x > b} = {x. a \<bullet> x = b}"
+proof (cases "a = 0")
+  case True with assms show ?thesis by simp
+next
+  case False then show ?thesis
+    by (force simp: frontier_def interior_open open_halfspace_gt)
+qed
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Some more convenient intermediate-value theorem formulations\<close>