1.1 --- a/src/HOL/SetInterval.thy	Mon Sep 24 13:53:26 2007 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Mon Sep 24 19:34:55 2007 +0200
     1.3 @@ -13,6 +13,42 @@
     1.4  imports IntArith
     1.5  begin
     1.6  
     1.7 +context ord
     1.8 +begin
     1.9 +definition
    1.10 +  lessThan    :: "'a => 'a set"	("(1\<^loc>{..<_})") where
    1.11 +  "\<^loc>{..<u} == {x. x \<sqsubset> u}"
    1.12 +
    1.13 +definition
    1.14 +  atMost      :: "'a => 'a set"	("(1\<^loc>{.._})") where
    1.15 +  "\<^loc>{..u} == {x. x \<sqsubseteq> u}"
    1.16 +
    1.17 +definition
    1.18 +  greaterThan :: "'a => 'a set"	("(1\<^loc>{_<..})") where
    1.19 +  "\<^loc>{l<..} == {x. l\<sqsubset>x}"
    1.20 +
    1.21 +definition
    1.22 +  atLeast     :: "'a => 'a set"	("(1\<^loc>{_..})") where
    1.23 +  "\<^loc>{l..} == {x. l\<sqsubseteq>x}"
    1.24 +
    1.25 +definition
    1.26 +  greaterThanLessThan :: "'a => 'a => 'a set"  ("(1\<^loc>{_<..<_})") where
    1.27 +  "\<^loc>{l<..<u} == \<^loc>{l<..} Int \<^loc>{..<u}"
    1.28 +
    1.29 +definition
    1.30 +  atLeastLessThan :: "'a => 'a => 'a set"      ("(1\<^loc>{_..<_})") where
    1.31 +  "\<^loc>{l..<u} == \<^loc>{l..} Int \<^loc>{..<u}"
    1.32 +
    1.33 +definition
    1.34 +  greaterThanAtMost :: "'a => 'a => 'a set"    ("(1\<^loc>{_<.._})") where
    1.35 +  "\<^loc>{l<..u} == \<^loc>{l<..} Int \<^loc>{..u}"
    1.36 +
    1.37 +definition
    1.38 +  atLeastAtMost :: "'a => 'a => 'a set"        ("(1\<^loc>{_.._})") where
    1.39 +  "\<^loc>{l..u} == \<^loc>{l..} Int \<^loc>{..u}"
    1.40 +
    1.41 +end
    1.42 +(*
    1.43  constdefs
    1.44    lessThan    :: "('a::ord) => 'a set"	("(1{..<_})")
    1.45    "{..<u} == {x. x<u}"
    1.46 @@ -37,6 +73,7 @@
    1.47  
    1.48    atLeastAtMost :: "['a::ord, 'a] => 'a set"        ("(1{_.._})")
    1.49    "{l..u} == {l..} Int {..u}"
    1.50 +*)
    1.51  
    1.52  text{* A note of warning when using @{term"{..<n}"} on type @{typ
    1.53  nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving
    1.54 @@ -69,7 +106,7 @@
    1.55  
    1.56  subsection {* Various equivalences *}
    1.57  
    1.58 -lemma lessThan_iff [iff]: "(i: lessThan k) = (i<k)"
    1.59 +lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i\<^loc><k)"
    1.60  by (simp add: lessThan_def)
    1.61  
    1.62  lemma Compl_lessThan [simp]:
    1.63 @@ -80,7 +117,7 @@
    1.64  lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}"
    1.65  by auto
    1.66  
    1.67 -lemma greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)"
    1.68 +lemma (in ord) greaterThan_iff [iff]: "(i: greaterThan k) = (k\<^loc><i)"
    1.69  by (simp add: greaterThan_def)
    1.70  
    1.71  lemma Compl_greaterThan [simp]:
    1.72 @@ -93,7 +130,7 @@
    1.73  apply (rule double_complement)
    1.74  done
    1.75  
    1.76 -lemma atLeast_iff [iff]: "(i: atLeast k) = (k<=i)"
    1.77 +lemma (in ord) atLeast_iff [iff]: "(i: atLeast k) = (k\<^loc><=i)"
    1.78  by (simp add: atLeast_def)
    1.79  
    1.80  lemma Compl_atLeast [simp]:
    1.81 @@ -101,7 +138,7 @@
    1.82  apply (simp add: lessThan_def atLeast_def le_def, auto)
    1.83  done
    1.84  
    1.85 -lemma atMost_iff [iff]: "(i: atMost k) = (i<=k)"
    1.86 +lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i\<^loc><=k)"
    1.87  by (simp add: atMost_def)
    1.88  
    1.89  lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
    1.90 @@ -153,42 +190,51 @@
    1.91  
    1.92  subsection {*Two-sided intervals*}
    1.93  
    1.94 +context ord
    1.95 +begin
    1.96 +
    1.97  lemma greaterThanLessThan_iff [simp,noatp]:
    1.98 -  "(i : {l<..<u}) = (l < i & i < u)"
    1.99 +  "(i : \<^loc>{l<..<u}) = (l \<^loc>< i & i \<^loc>< u)"
   1.100  by (simp add: greaterThanLessThan_def)
   1.101  
   1.102  lemma atLeastLessThan_iff [simp,noatp]:
   1.103 -  "(i : {l..<u}) = (l <= i & i < u)"
   1.104 +  "(i : \<^loc>{l..<u}) = (l \<^loc><= i & i \<^loc>< u)"
   1.105  by (simp add: atLeastLessThan_def)
   1.106  
   1.107  lemma greaterThanAtMost_iff [simp,noatp]:
   1.108 -  "(i : {l<..u}) = (l < i & i <= u)"
   1.109 +  "(i : \<^loc>{l<..u}) = (l \<^loc>< i & i \<^loc><= u)"
   1.110  by (simp add: greaterThanAtMost_def)
   1.111  
   1.112  lemma atLeastAtMost_iff [simp,noatp]:
   1.113 -  "(i : {l..u}) = (l <= i & i <= u)"
   1.114 +  "(i : \<^loc>{l..u}) = (l \<^loc><= i & i \<^loc><= u)"
   1.115  by (simp add: atLeastAtMost_def)
   1.116  
   1.117  text {* The above four lemmas could be declared as iffs.
   1.118    If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int}
   1.119    seems to take forever (more than one hour). *}
   1.120 +end
   1.121  
   1.122  subsubsection{* Emptyness and singletons *}
   1.123  
   1.124 -lemma atLeastAtMost_empty [simp]: "n < m ==> {m::'a::order..n} = {}";
   1.125 -  by (auto simp add: atLeastAtMost_def atMost_def atLeast_def);
   1.126 +context order
   1.127 +begin
   1.128  
   1.129 -lemma atLeastLessThan_empty[simp]: "n \<le> m ==> {m..<n::'a::order} = {}"
   1.130 +lemma atLeastAtMost_empty [simp]: "n \<^loc>< m ==> \<^loc>{m..n} = {}";
   1.131 +by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
   1.132 +
   1.133 +lemma atLeastLessThan_empty[simp]: "n \<^loc>\<le> m ==> \<^loc>{m..<n} = {}"
   1.134  by (auto simp add: atLeastLessThan_def)
   1.135  
   1.136 -lemma greaterThanAtMost_empty[simp]:"l \<le> k ==> {k<..(l::'a::order)} = {}"
   1.137 +lemma greaterThanAtMost_empty[simp]:"l \<^loc>\<le> k ==> \<^loc>{k<..l} = {}"
   1.138  by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)
   1.139  
   1.140 -lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..(l::'a::order)} = {}"
   1.141 +lemma greaterThanLessThan_empty[simp]:"l \<^loc>\<le> k ==> \<^loc>{k<..l} = {}"
   1.142  by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)
   1.143  
   1.144 -lemma atLeastAtMost_singleton [simp]: "{a::'a::order..a} = {a}";
   1.145 -by (auto simp add: atLeastAtMost_def atMost_def atLeast_def);
   1.146 +lemma atLeastAtMost_singleton [simp]: "\<^loc>{a..a} = {a}"
   1.147 +by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
   1.148 +
   1.149 +end
   1.150  
   1.151  subsection {* Intervals of natural numbers *}
   1.152