src/HOL/Set_Interval.thy
changeset 50999 3de230ed0547
parent 50417 f18b92f91818
child 51152 b52cc015429a
     1.1 --- a/src/HOL/Set_Interval.thy	Thu Jan 31 11:31:22 2013 +0100
     1.2 +++ b/src/HOL/Set_Interval.thy	Thu Jan 31 11:31:27 2013 +0100
     1.3 @@ -117,6 +117,11 @@
     1.4  lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
     1.5  by (blast intro: order_antisym)
     1.6  
     1.7 +lemma (in linorder) lessThan_Int_lessThan: "{ a <..} \<inter> { b <..} = { max a b <..}"
     1.8 +  by auto
     1.9 +
    1.10 +lemma (in linorder) greaterThan_Int_greaterThan: "{..< a} \<inter> {..< b} = {..< min a b}"
    1.11 +  by auto
    1.12  
    1.13  subsection {* Logical Equivalences for Set Inclusion and Equality *}
    1.14  
    1.15 @@ -190,6 +195,9 @@
    1.16  breaks many proofs. Since it only helps blast, it is better to leave well
    1.17  alone *}
    1.18  
    1.19 +lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \<inter> {..< b }"
    1.20 +  by auto
    1.21 +
    1.22  end
    1.23  
    1.24  subsubsection{* Emptyness, singletons, subset *}