# HG changeset patch
# User nipkow
# Date 1362474975 -3600
# Node ID fd531bd984d83b47cc56ed6019d33f33856bf108
# Parent  2cfd028a2fd987023175758a0cfe2019b72433af
more lemmas about intervals

diff -r 2cfd028a2fd9 -r fd531bd984d8 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Mar 04 17:32:10 2013 +0100
+++ b/src/HOL/Set.thy	Tue Mar 05 10:16:15 2013 +0100
@@ -639,6 +639,9 @@
 lemma UNIV_not_empty [iff]: "UNIV ~= {}"
   by (blast elim: equalityE)
 
+lemma empty_not_UNIV[simp]: "{} \<noteq> UNIV"
+by blast
+
 
 subsubsection {* The Powerset operator -- Pow *}
 
diff -r 2cfd028a2fd9 -r fd531bd984d8 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Mar 04 17:32:10 2013 +0100
+++ b/src/HOL/Set_Interval.thy	Tue Mar 05 10:16:15 2013 +0100
@@ -4,6 +4,11 @@
     Author:     Jeremy Avigad
 
 lessThan, greaterThan, atLeast, atMost and two-sided intervals
+
+Modern convention: Ixy stands for an interval where x and y
+describe the lower and upper bound and x,y : {c,o,i}
+where c = closed, o = open, i = infinite.
+Examples: Ico = {_ ..< _} and Ici = {_ ..}
 *)
 
 header {* Set intervals *}
@@ -256,6 +261,10 @@
    ((~ a <= b) | c <= a & b <= d & (c < a | b < d))  &  c <= d"
 by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans)
 
+lemma Icc_eq_Icc[simp]:
+  "{l..h} = {l'..h'} = (l=l' \<and> h=h' \<or> \<not> l\<le>h \<and> \<not> l'\<le>h')"
+by(simp add: order_class.eq_iff)(auto intro: order_trans)
+
 lemma atLeastAtMost_singleton_iff[simp]:
   "{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"
 proof
@@ -265,8 +274,105 @@
   ultimately show "a = b \<and> b = c" by auto
 qed simp
 
+lemma Icc_subset_Ici_iff[simp]:
+  "{l..h} \<subseteq> {l'..} = (~ l\<le>h \<or> l\<ge>l')"
+by(auto simp: subset_eq intro: order_trans)
+
+lemma Icc_subset_Iic_iff[simp]:
+  "{l..h} \<subseteq> {..h'} = (~ l\<le>h \<or> h\<le>h')"
+by(auto simp: subset_eq intro: order_trans)
+
+lemma not_Ici_eq_empty[simp]: "{l..} \<noteq> {}"
+by(auto simp: set_eq_iff)
+
+lemma not_Iic_eq_empty[simp]: "{..h} \<noteq> {}"
+by(auto simp: set_eq_iff)
+
+lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric]
+lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric]
+
 end
 
+context no_top
+begin
+
+(* also holds for no_bot but no_top should suffice *)
+lemma not_UNIV_le_Icc[simp]: "\<not> UNIV \<subseteq> {l..h}"
+using gt_ex[of h] by(auto simp: subset_eq less_le_not_le)
+
+lemma not_UNIV_le_Iic[simp]: "\<not> UNIV \<subseteq> {..h}"
+using gt_ex[of h] by(auto simp: subset_eq less_le_not_le)
+
+lemma not_Ici_le_Icc[simp]: "\<not> {l..} \<subseteq> {l'..h'}"
+using gt_ex[of h']
+by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)
+
+lemma not_Ici_le_Iic[simp]: "\<not> {l..} \<subseteq> {..h'}"
+using gt_ex[of h']
+by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)
+
+end
+
+context no_bot
+begin
+
+lemma not_UNIV_le_Ici[simp]: "\<not> UNIV \<subseteq> {l..}"
+using lt_ex[of l] by(auto simp: subset_eq less_le_not_le)
+
+lemma not_Iic_le_Icc[simp]: "\<not> {..h} \<subseteq> {l'..h'}"
+using lt_ex[of l']
+by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)
+
+lemma not_Iic_le_Ici[simp]: "\<not> {..h} \<subseteq> {l'..}"
+using lt_ex[of l']
+by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans)
+
+end
+
+
+context no_top
+begin
+
+(* also holds for no_bot but no_top should suffice *)
+lemma not_UNIV_eq_Icc[simp]: "\<not> UNIV = {l'..h'}"
+using gt_ex[of h'] by(auto simp: set_eq_iff  less_le_not_le)
+
+lemmas not_Icc_eq_UNIV[simp] = not_UNIV_eq_Icc[symmetric]
+
+lemma not_UNIV_eq_Iic[simp]: "\<not> UNIV = {..h'}"
+using gt_ex[of h'] by(auto simp: set_eq_iff  less_le_not_le)
+
+lemmas not_Iic_eq_UNIV[simp] = not_UNIV_eq_Iic[symmetric]
+
+lemma not_Icc_eq_Ici[simp]: "\<not> {l..h} = {l'..}"
+unfolding atLeastAtMost_def using not_Ici_le_Iic[of l'] by blast
+
+lemmas not_Ici_eq_Icc[simp] = not_Icc_eq_Ici[symmetric]
+
+(* also holds for no_bot but no_top should suffice *)
+lemma not_Iic_eq_Ici[simp]: "\<not> {..h} = {l'..}"
+using not_Ici_le_Iic[of l' h] by blast
+
+lemmas not_Ici_eq_Iic[simp] = not_Iic_eq_Ici[symmetric]
+
+end
+
+context no_bot
+begin
+
+lemma not_UNIV_eq_Ici[simp]: "\<not> UNIV = {l'..}"
+using lt_ex[of l'] by(auto simp: set_eq_iff  less_le_not_le)
+
+lemmas not_Ici_eq_UNIV[simp] = not_UNIV_eq_Ici[symmetric]
+
+lemma not_Icc_eq_Iic[simp]: "\<not> {l..h} = {..h'}"
+unfolding atLeastAtMost_def using not_Iic_le_Ici[of h'] by blast
+
+lemmas not_Iic_eq_Icc[simp] = not_Icc_eq_Iic[symmetric]
+
+end
+
+
 context inner_dense_linorder
 begin
 
@@ -313,7 +419,7 @@
 context no_top
 begin
 
-lemma greaterThan_non_empty: "{x <..} \<noteq> {}"
+lemma greaterThan_non_empty[simp]: "{x <..} \<noteq> {}"
   using gt_ex[of x] by auto
 
 end
@@ -321,7 +427,7 @@
 context no_bot
 begin
 
-lemma lessThan_non_empty: "{..< x} \<noteq> {}"
+lemma lessThan_non_empty[simp]: "{..< x} \<noteq> {}"
   using lt_ex[of x] by auto
 
 end
@@ -346,19 +452,16 @@
   shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d"
   using atLeastLessThan_inj assms by auto
 
-context complete_lattice
-begin
-
-lemma atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
-  by (auto simp: set_eq_iff intro: le_bot)
+lemma (in bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
+by (auto simp: set_eq_iff intro: le_bot)
 
-lemma atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top"
-  by (auto simp: set_eq_iff intro: top_le)
+lemma (in top) atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top"
+by (auto simp: set_eq_iff intro: top_le)
 
-lemma atLeastAtMost_eq_UNIV_iff: "{x..y} = UNIV \<longleftrightarrow> (x = bot \<and> y = top)"
-  by (auto simp: set_eq_iff intro: top_le le_bot)
+lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff:
+  "{x..y} = UNIV \<longleftrightarrow> (x = bot \<and> y = top)"
+by (auto simp: set_eq_iff intro: top_le le_bot)
 
-end
 
 subsubsection {* Intersection *}