# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1432906559 -3600
# Node ID f7e406aba90d7e8e86df1fb1fa9d70802f42ba56
# Parent  75e1aa7a450e79d2018b5bd7bd7e48c5c8777979
uncountability: open interval equivalences

diff -r 75e1aa7a450e -r f7e406aba90d src/HOL/Library/ContNotDenum.thy
--- a/src/HOL/Library/ContNotDenum.thy	Thu May 28 14:33:35 2015 +0100
+++ b/src/HOL/Library/ContNotDenum.thy	Fri May 29 14:35:59 2015 +0100
@@ -113,14 +113,35 @@
   using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan)
 
 lemma uncountable_open_interval:
-  fixes a b :: real assumes ab: "a < b"
-  shows "uncountable {a<..<b}"
-proof -
-  obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
-    using bij_betw_open_intervals[OF `a < b`, of "-pi/2" "pi/2"] by auto
-  then show ?thesis
-    by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
+  fixes a b :: real 
+  shows "uncountable {a<..<b} \<longleftrightarrow> a < b"
+proof
+  assume "uncountable {a<..<b}"
+  then show "a < b"
+    using uncountable_def by force
+next 
+  assume "a < b"
+  show "uncountable {a<..<b}"
+  proof -
+    obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
+      using bij_betw_open_intervals[OF `a < b`, of "-pi/2" "pi/2"] by auto
+    then show ?thesis
+      by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
+  qed
 qed
 
+lemma uncountable_half_open_interval_1:
+  fixes a :: real shows "uncountable {a..<b} \<longleftrightarrow> a<b"
+  apply auto
+  using atLeastLessThan_empty_iff apply fastforce
+  using uncountable_open_interval [of a b]
+  by (metis countable_Un_iff ivl_disj_un_singleton(3))
+
+lemma uncountable_half_open_interval_2:
+  fixes a :: real shows "uncountable {a<..b} \<longleftrightarrow> a<b"
+  apply auto
+  using atLeastLessThan_empty_iff apply fastforce
+  using uncountable_open_interval [of a b]
+  by (metis countable_Un_iff ivl_disj_un_singleton(4))
+
 end
-