merged
authorpaulson
Sun Sep 16 17:58:59 2018 +0100 (2 months ago)
changeset 69001f108b3b67ada
parent 68999 2af022252782
parent 69000 7cb3ddd60fd6
child 69002 f0d4b1db0ea0
merged
     1.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Sun Sep 16 16:31:56 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Sun Sep 16 17:58:59 2018 +0100
     1.3 @@ -231,6 +231,16 @@
     1.4      and is_interval_cc: "is_interval {b..a}"
     1.5    by (force simp: is_interval_def eucl_le[where 'a='a])+
     1.6  
     1.7 +lemma connected_interval [simp]:
     1.8 +  fixes a b::"'a::ordered_euclidean_space"
     1.9 +  shows "connected {a..b}"
    1.10 +  using is_interval_cc is_interval_connected by blast
    1.11 +
    1.12 +lemma path_connected_interval [simp]:
    1.13 +  fixes a b::"'a::ordered_euclidean_space"
    1.14 +  shows "path_connected {a..b}"
    1.15 +  using is_interval_cc is_interval_path_connected by blast
    1.16 +
    1.17  lemma%unimportant is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
    1.18    by (auto simp: real_atLeastGreaterThan_eq)
    1.19  
     2.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Sep 16 16:31:56 2018 +0200
     2.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Sep 16 17:58:59 2018 +0100
     2.3 @@ -700,6 +700,10 @@
     2.4    assumes "finite \<F>" "\<F> \<noteq> {}" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (\<Inter>\<F>)"
     2.5    by (metis (full_types) assms openin_INT2 image_ident)
     2.6  
     2.7 +lemma openin_Int_Inter:
     2.8 +  assumes "finite \<F>" "openin T U" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (U \<inter> \<Inter>\<F>)"
     2.9 +  using openin_Inter [of "insert U \<F>"] assms by auto
    2.10 +
    2.11  
    2.12  subsubsection \<open>Closed sets\<close>
    2.13  
    2.14 @@ -824,6 +828,26 @@
    2.15    unfolding openin_subtopology
    2.16    by auto (metis IntD1 in_mono openin_subset)
    2.17  
    2.18 +lemma subtopology_subtopology:
    2.19 +   "subtopology (subtopology X S) T = subtopology X (S \<inter> T)"
    2.20 +proof -
    2.21 +  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)"
    2.22 +    by (metis inf_assoc)
    2.23 +  have "subtopology (subtopology X S) T = topology (\<lambda>Ta. \<exists>Sa. Ta = Sa \<inter> T \<and> openin (subtopology X S) Sa)"
    2.24 +    by (simp add: subtopology_def)
    2.25 +  also have "\<dots> = subtopology X (S \<inter> T)"
    2.26 +    by (simp add: openin_subtopology eq) (simp add: subtopology_def)
    2.27 +  finally show ?thesis .
    2.28 +qed
    2.29 +
    2.30 +lemma openin_subtopology_alt:
    2.31 +     "openin (subtopology X U) S \<longleftrightarrow> S \<in> (\<lambda>T. U \<inter> T) ` Collect (openin X)"
    2.32 +  by (simp add: image_iff inf_commute openin_subtopology)
    2.33 +
    2.34 +lemma closedin_subtopology_alt:
    2.35 +     "closedin (subtopology X U) S \<longleftrightarrow> S \<in> (\<lambda>T. U \<inter> T) ` Collect (closedin X)"
    2.36 +  by (simp add: image_iff inf_commute closedin_subtopology)
    2.37 +
    2.38  lemma subtopology_superset:
    2.39    assumes UV: "topspace U \<subseteq> V"
    2.40    shows "subtopology U V = U"
    2.41 @@ -869,6 +893,9 @@
    2.42     "closedin (subtopology U X) X \<longleftrightarrow> X \<subseteq> topspace U"
    2.43  by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology)
    2.44  
    2.45 +lemma closedin_topspace_empty: "topspace T = {} \<Longrightarrow> (closedin T S \<longleftrightarrow> S = {})"
    2.46 +  by (simp add: closedin_def)
    2.47 +
    2.48  lemma openin_imp_subset:
    2.49     "openin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
    2.50  by (metis Int_iff openin_subtopology subsetI)
    2.51 @@ -877,6 +904,14 @@
    2.52     "closedin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
    2.53  by (simp add: closedin_def topspace_subtopology)
    2.54  
    2.55 +lemma openin_open_subtopology:
    2.56 +     "openin X S \<Longrightarrow> openin (subtopology X S) T \<longleftrightarrow> openin X T \<and> T \<subseteq> S"
    2.57 +  by (metis inf.orderE openin_Int openin_imp_subset openin_subtopology)
    2.58 +
    2.59 +lemma closedin_closed_subtopology:
    2.60 +     "closedin X S \<Longrightarrow> (closedin (subtopology X S) T \<longleftrightarrow> closedin X T \<and> T \<subseteq> S)"
    2.61 +  by (metis closedin_Int closedin_imp_subset closedin_subtopology inf.orderE)
    2.62 +
    2.63  lemma openin_subtopology_Un:
    2.64      "\<lbrakk>openin (subtopology X T) S; openin (subtopology X U) S\<rbrakk>
    2.65       \<Longrightarrow> openin (subtopology X (T \<union> U)) S"
     3.1 --- a/src/HOL/Library/FuncSet.thy	Sun Sep 16 16:31:56 2018 +0200
     3.2 +++ b/src/HOL/Library/FuncSet.thy	Sun Sep 16 17:58:59 2018 +0100
     3.3 @@ -499,6 +499,41 @@
     3.4    shows "f(x := a) \<in> insert x S \<rightarrow>\<^sub>E  T"
     3.5    using assms unfolding extensional_funcset_def extensional_def by auto
     3.6  
     3.7 +lemma subset_PiE:
     3.8 +   "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")
     3.9 +proof (cases "PiE I S = {}")
    3.10 +  case False
    3.11 +  moreover have "?lhs = ?rhs"
    3.12 +  proof
    3.13 +    assume L: ?lhs
    3.14 +    have "\<And>i. i\<in>I \<Longrightarrow> S i \<noteq> {}"
    3.15 +      using False PiE_eq_empty_iff by blast
    3.16 +    with L show ?rhs
    3.17 +      by (simp add: PiE_Int PiE_eq_iff inf.absorb_iff2)
    3.18 +  qed auto
    3.19 +  ultimately show ?thesis
    3.20 +    by simp
    3.21 +qed simp
    3.22 +
    3.23 +lemma PiE_eq:
    3.24 +   "PiE I S = PiE I T \<longleftrightarrow> PiE I S = {} \<and> PiE I T = {} \<or> (\<forall>i \<in> I. S i = T i)"
    3.25 +  by (auto simp: PiE_eq_iff PiE_eq_empty_iff)
    3.26 +
    3.27 +lemma PiE_UNIV [simp]: "PiE UNIV (\<lambda>i. UNIV) = UNIV"
    3.28 +  by blast
    3.29 +
    3.30 +lemma image_projection_PiE:
    3.31 +  "(\<lambda>f. f i) ` (PiE I S) = (if PiE I S = {} then {} else if i \<in> I then S i else {undefined})"
    3.32 +proof -
    3.33 +  have "(\<lambda>f. f i) ` Pi\<^sub>E I S = S i" if "i \<in> I" "f \<in> PiE I S" for f
    3.34 +    using that apply auto
    3.35 +    by (rule_tac x="(\<lambda>k. if k=i then x else f k)" in image_eqI) auto
    3.36 +  moreover have "(\<lambda>f. f i) ` Pi\<^sub>E I S = {undefined}" if "f \<in> PiE I S" "i \<notin> I" for f
    3.37 +    using that by (blast intro: PiE_arb [OF that, symmetric])
    3.38 +  ultimately show ?thesis
    3.39 +    by auto
    3.40 +qed
    3.41 +
    3.42  
    3.43  subsubsection \<open>Injective Extensional Function Spaces\<close>
    3.44  
     4.1 --- a/src/HOL/Zorn.thy	Sun Sep 16 16:31:56 2018 +0200
     4.2 +++ b/src/HOL/Zorn.thy	Sun Sep 16 17:58:59 2018 +0100
     4.3 @@ -386,7 +386,7 @@
     4.4  subsubsection \<open>Zorn's lemma\<close>
     4.5  
     4.6  text \<open>If every chain has an upper bound, then there is a maximal set.\<close>
     4.7 -lemma subset_Zorn:
     4.8 +theorem subset_Zorn:
     4.9    assumes "\<And>C. subset.chain A C \<Longrightarrow> \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U"
    4.10    shows "\<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
    4.11  proof -
    4.12 @@ -487,7 +487,7 @@
    4.13  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"
    4.14    using subset_Zorn [of A] by (auto simp: chains_alt_def)
    4.15  
    4.16 -text \<open>Various other lemmas\<close>
    4.17 +subsection \<open>Other variants of Zorn's Lemma\<close>
    4.18  
    4.19  lemma chainsD: "c \<in> chains S \<Longrightarrow> x \<in> c \<Longrightarrow> y \<in> c \<Longrightarrow> x \<subseteq> y \<or> y \<subseteq> x"
    4.20    unfolding chains_def chain_subset_def by blast
    4.21 @@ -562,6 +562,67 @@
    4.22      by (auto simp: relation_of_def)
    4.23  qed
    4.24  
    4.25 +lemma Union_in_chain: "\<lbrakk>finite \<B>; \<B> \<noteq> {}; subset.chain \<A> \<B>\<rbrakk> \<Longrightarrow> \<Union>\<B> \<in> \<B>"
    4.26 +proof (induction \<B> rule: finite_induct)
    4.27 +  case (insert B \<B>)
    4.28 +  show ?case
    4.29 +  proof (cases "\<B> = {}")
    4.30 +    case False
    4.31 +    then show ?thesis
    4.32 +      using insert sup.absorb2 by (auto simp: subset_chain_insert dest!: bspec [where x="\<Union>\<B>"])
    4.33 +  qed auto
    4.34 +qed simp
    4.35 +
    4.36 +lemma Inter_in_chain: "\<lbrakk>finite \<B>; \<B> \<noteq> {}; subset.chain \<A> \<B>\<rbrakk> \<Longrightarrow> \<Inter>\<B> \<in> \<B>"
    4.37 +proof (induction \<B> rule: finite_induct)
    4.38 +  case (insert B \<B>)
    4.39 +  show ?case
    4.40 +  proof (cases "\<B> = {}")
    4.41 +    case False
    4.42 +    then show ?thesis
    4.43 +      using insert inf.absorb2 by (auto simp: subset_chain_insert dest!: bspec [where x="\<Inter>\<B>"])
    4.44 +  qed auto
    4.45 +qed simp
    4.46 +
    4.47 +lemma finite_subset_Union_chain:
    4.48 +  assumes "finite A" "A \<subseteq> \<Union>\<B>" "\<B> \<noteq> {}" and sub: "subset.chain \<A> \<B>"
    4.49 +  obtains B where "B \<in> \<B>" "A \<subseteq> B"
    4.50 +proof -
    4.51 +  obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<B>" "A \<subseteq> \<Union>\<F>"
    4.52 +    using assms by (auto intro: finite_subset_Union)
    4.53 +  show thesis
    4.54 +  proof (cases "\<F> = {}")
    4.55 +    case True
    4.56 +    then show ?thesis
    4.57 +      using \<open>A \<subseteq> \<Union>\<F>\<close> \<open>\<B> \<noteq> {}\<close> that by fastforce
    4.58 +  next
    4.59 +    case False
    4.60 +    show ?thesis
    4.61 +    proof
    4.62 +      show "\<Union>\<F> \<in> \<B>"
    4.63 +        using sub \<open>\<F> \<subseteq> \<B>\<close> \<open>finite \<F>\<close>
    4.64 +        by (simp add: Union_in_chain False subset.chain_def subset_iff)
    4.65 +      show "A \<subseteq> \<Union>\<F>"
    4.66 +        using \<open>A \<subseteq> \<Union>\<F>\<close> by blast
    4.67 +    qed
    4.68 +  qed
    4.69 +qed
    4.70 +
    4.71 +lemma subset_Zorn_nonempty:
    4.72 +  assumes "\<A> \<noteq> {}" and ch: "\<And>\<C>. \<lbrakk>\<C>\<noteq>{}; subset.chain \<A> \<C>\<rbrakk> \<Longrightarrow> \<Union>\<C> \<in> \<A>"
    4.73 +  shows "\<exists>M\<in>\<A>. \<forall>X\<in>\<A>. M \<subseteq> X \<longrightarrow> X = M"
    4.74 +proof (rule subset_Zorn)
    4.75 +  show "\<exists>U\<in>\<A>. \<forall>X\<in>\<C>. X \<subseteq> U" if "subset.chain \<A> \<C>" for \<C>
    4.76 +  proof (cases "\<C> = {}")
    4.77 +    case True
    4.78 +    then show ?thesis
    4.79 +      using \<open>\<A> \<noteq> {}\<close> by blast
    4.80 +  next
    4.81 +    case False
    4.82 +    show ?thesis
    4.83 +      by (blast intro!: ch False that Union_upper)
    4.84 +  qed
    4.85 +qed
    4.86  
    4.87  subsection \<open>The Well Ordering Theorem\<close>
    4.88