author hoelzl Mon Dec 08 14:32:11 2014 +0100 (2014-12-08) changeset 59106 af691e67f71f parent 59105 18d4e100c267 child 59111 c85e018be3a3
instance bool and enat as topologies
 src/HOL/Library/Extended_Nat.thy file | annotate | diff | revisions src/HOL/Topological_Spaces.thy file | annotate | diff | revisions
```     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
```