# HG changeset patch
# User paulson
# Date 1537117139 -3600
# Node ID f108b3b67adac0d8930d5447f91edccf737692b6
# Parent  2af022252782f5b2605e25d395d70b4257084024# Parent  7cb3ddd60fd6c29286a40e59555dbf54e7894b43
merged

diff -r 2af022252782 -r f108b3b67ada src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Sun Sep 16 16:31:56 2018 +0200
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Sun Sep 16 17:58:59 2018 +0100
@@ -231,6 +231,16 @@
     and is_interval_cc: "is_interval {b..a}"
   by (force simp: is_interval_def eucl_le[where 'a='a])+
 
+lemma connected_interval [simp]:
+  fixes a b::"'a::ordered_euclidean_space"
+  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%unimportant is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
   by (auto simp: real_atLeastGreaterThan_eq)
 
diff -r 2af022252782 -r f108b3b67ada src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Sep 16 16:31:56 2018 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Sep 16 17:58:59 2018 +0100
@@ -700,6 +700,10 @@
   assumes "finite \<F>" "\<F> \<noteq> {}" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (\<Inter>\<F>)"
   by (metis (full_types) assms openin_INT2 image_ident)
 
+lemma openin_Int_Inter:
+  assumes "finite \<F>" "openin T U" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (U \<inter> \<Inter>\<F>)"
+  using openin_Inter [of "insert U \<F>"] assms by auto
+
 
 subsubsection \<open>Closed sets\<close>
 
@@ -824,6 +828,26 @@
   unfolding openin_subtopology
   by auto (metis IntD1 in_mono openin_subset)
 
+lemma subtopology_subtopology:
+   "subtopology (subtopology X S) T = subtopology X (S \<inter> T)"
+proof -
+  have eq: "\<And>T'. (\<exists>S'. T' = S' \<inter> T \<and> (\<exists>T. openin X T \<and> S' = T \<inter> S)) = (\<exists>Sa. T' = Sa \<inter> (S \<inter> T) \<and> openin X Sa)"
+    by (metis inf_assoc)
+  have "subtopology (subtopology X S) T = topology (\<lambda>Ta. \<exists>Sa. Ta = Sa \<inter> T \<and> openin (subtopology X S) Sa)"
+    by (simp add: subtopology_def)
+  also have "\<dots> = subtopology X (S \<inter> T)"
+    by (simp add: openin_subtopology eq) (simp add: subtopology_def)
+  finally show ?thesis .
+qed
+
+lemma openin_subtopology_alt:
+     "openin (subtopology X U) S \<longleftrightarrow> S \<in> (\<lambda>T. U \<inter> T) ` Collect (openin X)"
+  by (simp add: image_iff inf_commute openin_subtopology)
+
+lemma closedin_subtopology_alt:
+     "closedin (subtopology X U) S \<longleftrightarrow> S \<in> (\<lambda>T. U \<inter> T) ` Collect (closedin X)"
+  by (simp add: image_iff inf_commute closedin_subtopology)
+
 lemma subtopology_superset:
   assumes UV: "topspace U \<subseteq> V"
   shows "subtopology U V = U"
@@ -869,6 +893,9 @@
    "closedin (subtopology U X) X \<longleftrightarrow> X \<subseteq> topspace U"
 by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology)
 
+lemma closedin_topspace_empty: "topspace T = {} \<Longrightarrow> (closedin T S \<longleftrightarrow> S = {})"
+  by (simp add: closedin_def)
+
 lemma openin_imp_subset:
    "openin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
 by (metis Int_iff openin_subtopology subsetI)
@@ -877,6 +904,14 @@
    "closedin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
 by (simp add: closedin_def topspace_subtopology)
 
+lemma openin_open_subtopology:
+     "openin X S \<Longrightarrow> openin (subtopology X S) T \<longleftrightarrow> openin X T \<and> T \<subseteq> S"
+  by (metis inf.orderE openin_Int openin_imp_subset openin_subtopology)
+
+lemma closedin_closed_subtopology:
+     "closedin X S \<Longrightarrow> (closedin (subtopology X S) T \<longleftrightarrow> closedin X T \<and> T \<subseteq> S)"
+  by (metis closedin_Int closedin_imp_subset closedin_subtopology inf.orderE)
+
 lemma openin_subtopology_Un:
     "\<lbrakk>openin (subtopology X T) S; openin (subtopology X U) S\<rbrakk>
      \<Longrightarrow> openin (subtopology X (T \<union> U)) S"
diff -r 2af022252782 -r f108b3b67ada src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Sun Sep 16 16:31:56 2018 +0200
+++ b/src/HOL/Library/FuncSet.thy	Sun Sep 16 17:58:59 2018 +0100
@@ -499,6 +499,41 @@
   shows "f(x := a) \<in> insert x S \<rightarrow>\<^sub>E  T"
   using assms unfolding extensional_funcset_def extensional_def by auto
 
+lemma subset_PiE:
+   "PiE I S \<subseteq> PiE I T \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. S i \<subseteq> T i)" (is "?lhs \<longleftrightarrow> _ \<or> ?rhs")
+proof (cases "PiE I S = {}")
+  case False
+  moreover have "?lhs = ?rhs"
+  proof
+    assume L: ?lhs
+    have "\<And>i. i\<in>I \<Longrightarrow> S i \<noteq> {}"
+      using False PiE_eq_empty_iff by blast
+    with L show ?rhs
+      by (simp add: PiE_Int PiE_eq_iff inf.absorb_iff2)
+  qed auto
+  ultimately show ?thesis
+    by simp
+qed simp
+
+lemma PiE_eq:
+   "PiE I S = PiE I T \<longleftrightarrow> PiE I S = {} \<and> PiE I T = {} \<or> (\<forall>i \<in> I. S i = T i)"
+  by (auto simp: PiE_eq_iff PiE_eq_empty_iff)
+
+lemma PiE_UNIV [simp]: "PiE UNIV (\<lambda>i. UNIV) = UNIV"
+  by blast
+
+lemma image_projection_PiE:
+  "(\<lambda>f. f i) ` (PiE I S) = (if PiE I S = {} then {} else if i \<in> I then S i else {undefined})"
+proof -
+  have "(\<lambda>f. f i) ` Pi\<^sub>E I S = S i" if "i \<in> I" "f \<in> PiE I S" for f
+    using that apply auto
+    by (rule_tac x="(\<lambda>k. if k=i then x else f k)" in image_eqI) auto
+  moreover have "(\<lambda>f. f i) ` Pi\<^sub>E I S = {undefined}" if "f \<in> PiE I S" "i \<notin> I" for f
+    using that by (blast intro: PiE_arb [OF that, symmetric])
+  ultimately show ?thesis
+    by auto
+qed
+
 
 subsubsection \<open>Injective Extensional Function Spaces\<close>
 
diff -r 2af022252782 -r f108b3b67ada src/HOL/Zorn.thy
--- a/src/HOL/Zorn.thy	Sun Sep 16 16:31:56 2018 +0200
+++ b/src/HOL/Zorn.thy	Sun Sep 16 17:58:59 2018 +0100
@@ -386,7 +386,7 @@
 subsubsection \<open>Zorn's lemma\<close>
 
 text \<open>If every chain has an upper bound, then there is a maximal set.\<close>
-lemma subset_Zorn:
+theorem subset_Zorn:
   assumes "\<And>C. subset.chain A C \<Longrightarrow> \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U"
   shows "\<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
 proof -
@@ -487,7 +487,7 @@
 lemma Zorn_Lemma2: "\<forall>C\<in>chains A. \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
   using subset_Zorn [of A] by (auto simp: chains_alt_def)
 
-text \<open>Various other lemmas\<close>
+subsection \<open>Other variants of Zorn's Lemma\<close>
 
 lemma chainsD: "c \<in> chains S \<Longrightarrow> x \<in> c \<Longrightarrow> y \<in> c \<Longrightarrow> x \<subseteq> y \<or> y \<subseteq> x"
   unfolding chains_def chain_subset_def by blast
@@ -562,6 +562,67 @@
     by (auto simp: relation_of_def)
 qed
 
+lemma Union_in_chain: "\<lbrakk>finite \<B>; \<B> \<noteq> {}; subset.chain \<A> \<B>\<rbrakk> \<Longrightarrow> \<Union>\<B> \<in> \<B>"
+proof (induction \<B> rule: finite_induct)
+  case (insert B \<B>)
+  show ?case
+  proof (cases "\<B> = {}")
+    case False
+    then show ?thesis
+      using insert sup.absorb2 by (auto simp: subset_chain_insert dest!: bspec [where x="\<Union>\<B>"])
+  qed auto
+qed simp
+
+lemma Inter_in_chain: "\<lbrakk>finite \<B>; \<B> \<noteq> {}; subset.chain \<A> \<B>\<rbrakk> \<Longrightarrow> \<Inter>\<B> \<in> \<B>"
+proof (induction \<B> rule: finite_induct)
+  case (insert B \<B>)
+  show ?case
+  proof (cases "\<B> = {}")
+    case False
+    then show ?thesis
+      using insert inf.absorb2 by (auto simp: subset_chain_insert dest!: bspec [where x="\<Inter>\<B>"])
+  qed auto
+qed simp
+
+lemma finite_subset_Union_chain:
+  assumes "finite A" "A \<subseteq> \<Union>\<B>" "\<B> \<noteq> {}" and sub: "subset.chain \<A> \<B>"
+  obtains B where "B \<in> \<B>" "A \<subseteq> B"
+proof -
+  obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<B>" "A \<subseteq> \<Union>\<F>"
+    using assms by (auto intro: finite_subset_Union)
+  show thesis
+  proof (cases "\<F> = {}")
+    case True
+    then show ?thesis
+      using \<open>A \<subseteq> \<Union>\<F>\<close> \<open>\<B> \<noteq> {}\<close> that by fastforce
+  next
+    case False
+    show ?thesis
+    proof
+      show "\<Union>\<F> \<in> \<B>"
+        using sub \<open>\<F> \<subseteq> \<B>\<close> \<open>finite \<F>\<close>
+        by (simp add: Union_in_chain False subset.chain_def subset_iff)
+      show "A \<subseteq> \<Union>\<F>"
+        using \<open>A \<subseteq> \<Union>\<F>\<close> by blast
+    qed
+  qed
+qed
+
+lemma subset_Zorn_nonempty:
+  assumes "\<A> \<noteq> {}" and ch: "\<And>\<C>. \<lbrakk>\<C>\<noteq>{}; subset.chain \<A> \<C>\<rbrakk> \<Longrightarrow> \<Union>\<C> \<in> \<A>"
+  shows "\<exists>M\<in>\<A>. \<forall>X\<in>\<A>. M \<subseteq> X \<longrightarrow> X = M"
+proof (rule subset_Zorn)
+  show "\<exists>U\<in>\<A>. \<forall>X\<in>\<C>. X \<subseteq> U" if "subset.chain \<A> \<C>" for \<C>
+  proof (cases "\<C> = {}")
+    case True
+    then show ?thesis
+      using \<open>\<A> \<noteq> {}\<close> by blast
+  next
+    case False
+    show ?thesis
+      by (blast intro!: ch False that Union_upper)
+  qed
+qed
 
 subsection \<open>The Well Ordering Theorem\<close>