new lemmas
authornipkow
Wed Aug 26 10:48:12 2009 +0200 (2009-08-26)
changeset 324006c62363cf0d7
parent 32389 cb3c5189ea85
child 32401 5ca6f9a344c0
new lemmas
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/SetInterval.thy	Fri Aug 21 19:06:12 2009 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Wed Aug 26 10:48:12 2009 +0200
     1.3 @@ -186,26 +186,60 @@
     1.4    seems to take forever (more than one hour). *}
     1.5  end
     1.6  
     1.7 -subsubsection{* Emptyness and singletons *}
     1.8 +subsubsection{* Emptyness, singletons, subset *}
     1.9  
    1.10  context order
    1.11  begin
    1.12  
    1.13 -lemma atLeastAtMost_empty [simp]: "n < m ==> {m..n} = {}";
    1.14 -by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
    1.15 +lemma atLeastatMost_empty[simp]:
    1.16 +  "b < a \<Longrightarrow> {a..b} = {}"
    1.17 +by(auto simp: atLeastAtMost_def atLeast_def atMost_def)
    1.18 +
    1.19 +lemma atLeastatMost_empty_iff[simp]:
    1.20 +  "{a..b} = {} \<longleftrightarrow> (~ a <= b)"
    1.21 +by auto (blast intro: order_trans)
    1.22 +
    1.23 +lemma atLeastatMost_empty_iff2[simp]:
    1.24 +  "{} = {a..b} \<longleftrightarrow> (~ a <= b)"
    1.25 +by auto (blast intro: order_trans)
    1.26 +
    1.27 +lemma atLeastLessThan_empty[simp]:
    1.28 +  "b <= a \<Longrightarrow> {a..<b} = {}"
    1.29 +by(auto simp: atLeastLessThan_def)
    1.30  
    1.31 -lemma atLeastLessThan_empty[simp]: "n \<le> m ==> {m..<n} = {}"
    1.32 -by (auto simp add: atLeastLessThan_def)
    1.33 +lemma atLeastLessThan_empty_iff[simp]:
    1.34 +  "{a..<b} = {} \<longleftrightarrow> (~ a < b)"
    1.35 +by auto (blast intro: le_less_trans)
    1.36 +
    1.37 +lemma atLeastLessThan_empty_iff2[simp]:
    1.38 +  "{} = {a..<b} \<longleftrightarrow> (~ a < b)"
    1.39 +by auto (blast intro: le_less_trans)
    1.40  
    1.41 -lemma greaterThanAtMost_empty[simp]:"l \<le> k ==> {k<..l} = {}"
    1.42 +lemma greaterThanAtMost_empty[simp]: "l \<le> k ==> {k<..l} = {}"
    1.43  by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)
    1.44  
    1.45 +lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \<longleftrightarrow> ~ k < l"
    1.46 +by auto (blast intro: less_le_trans)
    1.47 +
    1.48 +lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \<longleftrightarrow> ~ k < l"
    1.49 +by auto (blast intro: less_le_trans)
    1.50 +
    1.51  lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..<l} = {}"
    1.52  by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)
    1.53  
    1.54  lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"
    1.55  by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
    1.56  
    1.57 +lemma atLeastatMost_subset_iff[simp]:
    1.58 +  "{a..b} <= {c..d} \<longleftrightarrow> (~ a <= b) | c <= a & b <= d"
    1.59 +unfolding atLeastAtMost_def atLeast_def atMost_def
    1.60 +by (blast intro: order_trans)
    1.61 +
    1.62 +lemma atLeastatMost_psubset_iff:
    1.63 +  "{a..b} < {c..d} \<longleftrightarrow>
    1.64 +   ((~ a <= b) | c <= a & b <= d & (c < a | b < d))  &  c <= d"
    1.65 +by(simp add: psubset_eq expand_set_eq less_le_not_le)(blast intro: order_trans)
    1.66 +
    1.67  end
    1.68  
    1.69  subsection {* Intervals of natural numbers *}