instance bool and enat as topologies
authorhoelzl
Mon Dec 08 14:32:11 2014 +0100 (2014-12-08)
changeset 59106af691e67f71f
parent 59105 18d4e100c267
child 59111 c85e018be3a3
instance bool and enat as topologies
src/HOL/Library/Extended_Nat.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Mon Dec 08 12:30:47 2014 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Mon Dec 08 14:32:11 2014 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  section {* Extended natural numbers (i.e. with infinity) *}
     1.5  
     1.6  theory Extended_Nat
     1.7 -imports Main Countable
     1.8 +imports Complex_Main Countable
     1.9  begin
    1.10  
    1.11  class infinity =
    1.12 @@ -615,8 +615,6 @@
    1.13  
    1.14  subsection {* Complete Lattice *}
    1.15  
    1.16 -text {* TODO: enat as order topology? *}
    1.17 -
    1.18  instantiation enat :: complete_lattice
    1.19  begin
    1.20  
    1.21 @@ -649,6 +647,17 @@
    1.22  
    1.23  instance enat :: complete_linorder ..
    1.24  
    1.25 +instantiation enat :: linorder_topology
    1.26 +begin
    1.27 +
    1.28 +definition open_enat :: "enat set \<Rightarrow> bool" where
    1.29 +  "open_enat = generate_topology (range lessThan \<union> range greaterThan)"
    1.30 +
    1.31 +instance
    1.32 +  proof qed (rule open_enat_def)
    1.33 +
    1.34 +end
    1.35 +
    1.36  subsection {* Traditional theorem names *}
    1.37  
    1.38  lemmas enat_defs = zero_enat_def one_enat_def eSuc_def
     2.1 --- a/src/HOL/Topological_Spaces.thy	Mon Dec 08 12:30:47 2014 +0100
     2.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Dec 08 14:32:11 2014 +0100
     2.3 @@ -297,6 +297,31 @@
     2.4    case (Basis S) then show ?case by (fastforce intro: exI[of _ y] lt_ex)
     2.5  qed blast+
     2.6  
     2.7 +subsubsection {* Boolean is an order topology *}
     2.8 +
     2.9 +text {* It also is a discrete topology, but don't have a type class for it (yet). *}
    2.10 +
    2.11 +instantiation bool :: order_topology
    2.12 +begin
    2.13 +
    2.14 +definition open_bool :: "bool set \<Rightarrow> bool" where
    2.15 +  "open_bool = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>a. {a <..}))"
    2.16 +
    2.17 +instance
    2.18 +  proof qed (rule open_bool_def)
    2.19 +
    2.20 +end
    2.21 +
    2.22 +lemma open_bool[simp, intro!]: "open (A::bool set)"
    2.23 +proof -
    2.24 +  have *: "{False <..} = {True}" "{..< True} = {False}"
    2.25 +    by auto
    2.26 +  have "A = UNIV \<or> A = {} \<or> A = {False <..} \<or> A = {..< True}"
    2.27 +    using subset_UNIV[of A] unfolding UNIV_bool * by auto
    2.28 +  then show "open A"
    2.29 +    by auto
    2.30 +qed
    2.31 +
    2.32  subsection {* Filters *}
    2.33  
    2.34  text {*
    2.35 @@ -2476,6 +2501,55 @@
    2.36  
    2.37  end
    2.38  
    2.39 +lemma connected_iff_const:
    2.40 +  fixes S :: "'a::topological_space set"
    2.41 +  shows "connected S \<longleftrightarrow> (\<forall>P::'a \<Rightarrow> bool. continuous_on S P \<longrightarrow> (\<exists>c. \<forall>s\<in>S. P s = c))"
    2.42 +proof safe
    2.43 +  fix P :: "'a \<Rightarrow> bool" assume "connected S" "continuous_on S P"
    2.44 +  then have "\<And>b. \<exists>A. open A \<and> A \<inter> S = P -` {b} \<inter> S"
    2.45 +    unfolding continuous_on_open_invariant by simp
    2.46 +  from this[of True] this[of False]
    2.47 +  obtain t f where "open t" "open f" and *: "f \<inter> S = P -` {False} \<inter> S" "t \<inter> S = P -` {True} \<inter> S"
    2.48 +    by auto
    2.49 +  then have "t \<inter> S = {} \<or> f \<inter> S = {}"
    2.50 +    by (intro connectedD[OF `connected S`])  auto
    2.51 +  then show "\<exists>c. \<forall>s\<in>S. P s = c"
    2.52 +  proof (rule disjE)
    2.53 +    assume "t \<inter> S = {}" then show ?thesis
    2.54 +      unfolding * by (intro exI[of _ False]) auto
    2.55 +  next
    2.56 +    assume "f \<inter> S = {}" then show ?thesis
    2.57 +      unfolding * by (intro exI[of _ True]) auto
    2.58 +  qed
    2.59 +next
    2.60 +  assume P: "\<forall>P::'a \<Rightarrow> bool. continuous_on S P \<longrightarrow> (\<exists>c. \<forall>s\<in>S. P s = c)"
    2.61 +  show "connected S"
    2.62 +  proof (rule connectedI)
    2.63 +    fix A B assume *: "open A" "open B" "A \<inter> S \<noteq> {}" "B \<inter> S \<noteq> {}" "A \<inter> B \<inter> S = {}" "S \<subseteq> A \<union> B"
    2.64 +    have "continuous_on S (\<lambda>x. x \<in> A)"
    2.65 +      unfolding continuous_on_open_invariant
    2.66 +    proof safe
    2.67 +      fix C :: "bool set"
    2.68 +      have "C = UNIV \<or> C = {True} \<or> C = {False} \<or> C = {}"
    2.69 +        using subset_UNIV[of C] unfolding UNIV_bool by auto
    2.70 +      with * show "\<exists>T. open T \<and> T \<inter> S = (\<lambda>x. x \<in> A) -` C \<inter> S"
    2.71 +        by (intro exI[of _ "(if True \<in> C then A else {}) \<union> (if False \<in> C then B else {})"]) auto
    2.72 +    qed
    2.73 +    from P[rule_format, OF this] obtain c where "\<And>s. s \<in> S \<Longrightarrow> (s \<in> A) = c" by blast
    2.74 +    with * show False
    2.75 +      by (cases c) auto
    2.76 +  qed
    2.77 +qed
    2.78 +
    2.79 +lemma connectedD_const:
    2.80 +  fixes P :: "'a::topological_space \<Rightarrow> bool"
    2.81 +  shows "connected S \<Longrightarrow> continuous_on S P \<Longrightarrow> \<exists>c. \<forall>s\<in>S. P s = c"
    2.82 +  unfolding connected_iff_const by auto
    2.83 +
    2.84 +lemma connectedI_const:
    2.85 +  "(\<And>P::'a::topological_space \<Rightarrow> bool. continuous_on S P \<Longrightarrow> \<exists>c. \<forall>s\<in>S. P s = c) \<Longrightarrow> connected S"
    2.86 +  unfolding connected_iff_const by auto
    2.87 +
    2.88  lemma connected_local_const:
    2.89    assumes "connected A" "a \<in> A" "b \<in> A"
    2.90    assumes *: "\<forall>a\<in>A. eventually (\<lambda>b. f a = f b) (at a within A)"
    2.91 @@ -2522,27 +2596,14 @@
    2.92    assumes *: "continuous_on s f"
    2.93    assumes "connected s"
    2.94    shows "connected (f ` s)"
    2.95 -proof (rule connectedI)
    2.96 -  fix A B assume A: "open A" "A \<inter> f ` s \<noteq> {}" and B: "open B" "B \<inter> f ` s \<noteq> {}" and
    2.97 -    AB: "A \<inter> B \<inter> f ` s = {}" "f ` s \<subseteq> A \<union> B"
    2.98 -  obtain A' where A': "open A'" "f -` A \<inter> s = A' \<inter> s"
    2.99 -    using * `open A` unfolding continuous_on_open_invariant by metis
   2.100 -  obtain B' where B': "open B'" "f -` B \<inter> s = B' \<inter> s"
   2.101 -    using * `open B` unfolding continuous_on_open_invariant by metis
   2.102 -
   2.103 -  have "\<exists>A B. open A \<and> open B \<and> s \<subseteq> A \<union> B \<and> A \<inter> B \<inter> s = {} \<and> A \<inter> s \<noteq> {} \<and> B \<inter> s \<noteq> {}"
   2.104 -  proof (rule exI[of _ A'], rule exI[of _ B'], intro conjI)
   2.105 -    have "s \<subseteq> (f -` A \<inter> s) \<union> (f -` B \<inter> s)" using AB by auto
   2.106 -    then show "s \<subseteq> A' \<union> B'" using A' B' by auto
   2.107 -  next
   2.108 -    have "(f -` A \<inter> s) \<inter> (f -` B \<inter> s) = {}" using AB by auto
   2.109 -    then show "A' \<inter> B' \<inter> s = {}" using A' B' by auto
   2.110 -  qed (insert A' B' A B, auto)
   2.111 -  with `connected s` show False
   2.112 -    unfolding connected_def by blast
   2.113 +proof (rule connectedI_const)
   2.114 +  fix P :: "'b \<Rightarrow> bool" assume "continuous_on (f ` s) P"
   2.115 +  then have "continuous_on s (P \<circ> f)"
   2.116 +    by (rule continuous_on_compose[OF *])
   2.117 +  from connectedD_const[OF `connected s` this] show "\<exists>c. \<forall>s\<in>f ` s. P s = c"
   2.118 +    by auto
   2.119  qed
   2.120  
   2.121 -
   2.122  section {* Connectedness *}
   2.123  
   2.124  class linear_continuum_topology = linorder_topology + linear_continuum