diff -r c661dae1070a -r e7f46ee04809 src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Mon Sep 24 13:53:26 2007 +0200 +++ b/src/HOL/SetInterval.thy Mon Sep 24 19:34:55 2007 +0200 @@ -13,6 +13,42 @@ imports IntArith begin +context ord +begin +definition + lessThan :: "'a => 'a set" ("(1\<^loc>{..<_})") where + "\<^loc>{.. u}" + +definition + atMost :: "'a => 'a set" ("(1\<^loc>{.._})") where + "\<^loc>{..u} == {x. x \ u}" + +definition + greaterThan :: "'a => 'a set" ("(1\<^loc>{_<..})") where + "\<^loc>{l<..} == {x. l\x}" + +definition + atLeast :: "'a => 'a set" ("(1\<^loc>{_..})") where + "\<^loc>{l..} == {x. l\x}" + +definition + greaterThanLessThan :: "'a => 'a => 'a set" ("(1\<^loc>{_<..<_})") where + "\<^loc>{l<..{l<..} Int \<^loc>{.. 'a => 'a set" ("(1\<^loc>{_..<_})") where + "\<^loc>{l..{l..} Int \<^loc>{.. 'a => 'a set" ("(1\<^loc>{_<.._})") where + "\<^loc>{l<..u} == \<^loc>{l<..} Int \<^loc>{..u}" + +definition + atLeastAtMost :: "'a => 'a => 'a set" ("(1\<^loc>{_.._})") where + "\<^loc>{l..u} == \<^loc>{l..} Int \<^loc>{..u}" + +end +(* constdefs lessThan :: "('a::ord) => 'a set" ("(1{..<_})") "{.. 'a set" ("(1{_.._})") "{l..u} == {l..} Int {..u}" +*) text{* A note of warning when using @{term"{..<=i)" by (simp add: atLeast_def) lemma Compl_atLeast [simp]: @@ -101,7 +138,7 @@ apply (simp add: lessThan_def atLeast_def le_def, auto) done -lemma atMost_iff [iff]: "(i: atMost k) = (i<=k)" +lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i\<^loc><=k)" by (simp add: atMost_def) lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" @@ -153,42 +190,51 @@ subsection {*Two-sided intervals*} +context ord +begin + lemma greaterThanLessThan_iff [simp,noatp]: - "(i : {l<..{l<..< i & i \<^loc>< u)" by (simp add: greaterThanLessThan_def) lemma atLeastLessThan_iff [simp,noatp]: - "(i : {l..{l..<= i & i \<^loc>< u)" by (simp add: atLeastLessThan_def) lemma greaterThanAtMost_iff [simp,noatp]: - "(i : {l<..u}) = (l < i & i <= u)" + "(i : \<^loc>{l<..u}) = (l \<^loc>< i & i \<^loc><= u)" by (simp add: greaterThanAtMost_def) lemma atLeastAtMost_iff [simp,noatp]: - "(i : {l..u}) = (l <= i & i <= u)" + "(i : \<^loc>{l..u}) = (l \<^loc><= i & i \<^loc><= u)" by (simp add: atLeastAtMost_def) text {* The above four lemmas could be declared as iffs. If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int} seems to take forever (more than one hour). *} +end subsubsection{* Emptyness and singletons *} -lemma atLeastAtMost_empty [simp]: "n < m ==> {m::'a::order..n} = {}"; - by (auto simp add: atLeastAtMost_def atMost_def atLeast_def); +context order +begin -lemma atLeastLessThan_empty[simp]: "n \ m ==> {m..< m ==> \<^loc>{m..n} = {}"; +by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) + +lemma atLeastLessThan_empty[simp]: "n \<^loc>\ m ==> \<^loc>{m.. k ==> {k<..(l::'a::order)} = {}" +lemma greaterThanAtMost_empty[simp]:"l \<^loc>\ k ==> \<^loc>{k<..l} = {}" by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) -lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<..(l::'a::order)} = {}" +lemma greaterThanLessThan_empty[simp]:"l \<^loc>\ k ==> \<^loc>{k<..l} = {}" by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def) -lemma atLeastAtMost_singleton [simp]: "{a::'a::order..a} = {a}"; -by (auto simp add: atLeastAtMost_def atMost_def atLeast_def); +lemma atLeastAtMost_singleton [simp]: "\<^loc>{a..a} = {a}" +by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) + +end subsection {* Intervals of natural numbers *}