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 *}
```