src/HOL/SetInterval.thy
changeset 15045 d59f7e2e18d3
parent 15042 fa7d27ef7e59
child 15047 fa62de5862b9
     1.1 --- a/src/HOL/SetInterval.thy	Thu Jul 15 08:38:37 2004 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Thu Jul 15 13:11:34 2004 +0200
     1.3 @@ -12,30 +12,44 @@
     1.4  theory SetInterval = IntArith:
     1.5  
     1.6  constdefs
     1.7 -  lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
     1.8 -  "{..u(} == {x. x<u}"
     1.9 +  lessThan    :: "('a::ord) => 'a set"	("(1{..<_})")
    1.10 +  "{..<u} == {x. x<u}"
    1.11  
    1.12    atMost      :: "('a::ord) => 'a set"	("(1{.._})")
    1.13    "{..u} == {x. x<=u}"
    1.14  
    1.15 -  greaterThan :: "('a::ord) => 'a set"	("(1{')_..})")
    1.16 -  "{)l..} == {x. l<x}"
    1.17 +  greaterThan :: "('a::ord) => 'a set"	("(1{_<..})")
    1.18 +  "{l<..} == {x. l<x}"
    1.19  
    1.20    atLeast     :: "('a::ord) => 'a set"	("(1{_..})")
    1.21    "{l..} == {x. l<=x}"
    1.22  
    1.23 -  greaterThanLessThan :: "['a::ord, 'a] => 'a set"  ("(1{')_.._'(})")
    1.24 -  "{)l..u(} == {)l..} Int {..u(}"
    1.25 +  greaterThanLessThan :: "['a::ord, 'a] => 'a set"  ("(1{_<..<_})")
    1.26 +  "{l<..<u} == {l<..} Int {..<u}"
    1.27  
    1.28 -  atLeastLessThan :: "['a::ord, 'a] => 'a set"      ("(1{_.._'(})")
    1.29 -  "{l..u(} == {l..} Int {..u(}"
    1.30 +  atLeastLessThan :: "['a::ord, 'a] => 'a set"      ("(1{_..<_})")
    1.31 +  "{l..<u} == {l..} Int {..<u}"
    1.32  
    1.33 -  greaterThanAtMost :: "['a::ord, 'a] => 'a set"    ("(1{')_.._})")
    1.34 -  "{)l..u} == {)l..} Int {..u}"
    1.35 +  greaterThanAtMost :: "['a::ord, 'a] => 'a set"    ("(1{_<.._})")
    1.36 +  "{l<..u} == {l<..} Int {..u}"
    1.37  
    1.38    atLeastAtMost :: "['a::ord, 'a] => 'a set"        ("(1{_.._})")
    1.39    "{l..u} == {l..} Int {..u}"
    1.40  
    1.41 +(* Old syntax, will disappear! *)
    1.42 +syntax
    1.43 +  "_lessThan"    :: "('a::ord) => 'a set"	("(1{.._'(})")
    1.44 +  "_greaterThan" :: "('a::ord) => 'a set"	("(1{')_..})")
    1.45 +  "_greaterThanLessThan" :: "['a::ord, 'a] => 'a set"  ("(1{')_.._'(})")
    1.46 +  "_atLeastLessThan" :: "['a::ord, 'a] => 'a set"      ("(1{_.._'(})")
    1.47 +  "_greaterThanAtMost" :: "['a::ord, 'a] => 'a set"    ("(1{')_.._})")
    1.48 +translations
    1.49 +  "{..m(}" => "{..<m}"
    1.50 +  "{)m..}" => "{m<..}"
    1.51 +  "{)m..n(}" => "{m<..<n}"
    1.52 +  "{m..n(}" => "{m..<n}"
    1.53 +  "{)m..n}" => "{m<..n}"
    1.54 +
    1.55  syntax
    1.56    "@UNION_le"   :: "nat => nat => 'b set => 'b set"       ("(3UN _<=_./ _)" 10)
    1.57    "@UNION_less" :: "nat => nat => 'b set => 'b set"       ("(3UN _<_./ _)" 10)
    1.58 @@ -56,9 +70,9 @@
    1.59  
    1.60  translations
    1.61    "UN i<=n. A"  == "UN i:{..n}. A"
    1.62 -  "UN i<n. A"   == "UN i:{..n(}. A"
    1.63 +  "UN i<n. A"   == "UN i:{..<n}. A"
    1.64    "INT i<=n. A" == "INT i:{..n}. A"
    1.65 -  "INT i<n. A"  == "INT i:{..n(}. A"
    1.66 +  "INT i<n. A"  == "INT i:{..<n}. A"
    1.67  
    1.68  
    1.69  subsection {* Various equivalences *}
    1.70 @@ -150,19 +164,19 @@
    1.71  text {* @{text greaterThanLessThan} *}
    1.72  
    1.73  lemma greaterThanLessThan_iff [simp]:
    1.74 -  "(i : {)l..u(}) = (l < i & i < u)"
    1.75 +  "(i : {l<..<u}) = (l < i & i < u)"
    1.76  by (simp add: greaterThanLessThan_def)
    1.77  
    1.78  text {* @{text atLeastLessThan} *}
    1.79  
    1.80  lemma atLeastLessThan_iff [simp]:
    1.81 -  "(i : {l..u(}) = (l <= i & i < u)"
    1.82 +  "(i : {l..<u}) = (l <= i & i < u)"
    1.83  by (simp add: atLeastLessThan_def)
    1.84  
    1.85  text {* @{text greaterThanAtMost} *}
    1.86  
    1.87  lemma greaterThanAtMost_iff [simp]:
    1.88 -  "(i : {)l..u}) = (l < i & i <= u)"
    1.89 +  "(i : {l<..u}) = (l < i & i <= u)"
    1.90  by (simp add: greaterThanAtMost_def)
    1.91  
    1.92  text {* @{text atLeastAtMost} *}
    1.93 @@ -229,40 +243,40 @@
    1.94  lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
    1.95  by blast
    1.96  
    1.97 -lemma atLeast0LessThan [simp]: "{0::nat..n(} = {..n(}"
    1.98 +lemma atLeast0LessThan [simp]: "{0::nat..<n} = {..<n}"
    1.99  by(simp add:lessThan_def atLeastLessThan_def)
   1.100  
   1.101  text {* Intervals of nats with @{text Suc} *}
   1.102  
   1.103 -lemma atLeastLessThanSuc_atLeastAtMost: "{l..Suc u(} = {l..u}"
   1.104 +lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}"
   1.105    by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
   1.106  
   1.107 -lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {)l..u}"  
   1.108 +lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}"  
   1.109    by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
   1.110      greaterThanAtMost_def)
   1.111  
   1.112 -lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..u(} = {)l..u(}"  
   1.113 +lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}"  
   1.114    by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
   1.115      greaterThanLessThan_def)
   1.116  
   1.117  subsubsection {* Finiteness *}
   1.118  
   1.119 -lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
   1.120 +lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"
   1.121    by (induct k) (simp_all add: lessThan_Suc)
   1.122  
   1.123  lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
   1.124    by (induct k) (simp_all add: atMost_Suc)
   1.125  
   1.126  lemma finite_greaterThanLessThan [iff]:
   1.127 -  fixes l :: nat shows "finite {)l..u(}"
   1.128 +  fixes l :: nat shows "finite {l<..<u}"
   1.129  by (simp add: greaterThanLessThan_def)
   1.130  
   1.131  lemma finite_atLeastLessThan [iff]:
   1.132 -  fixes l :: nat shows "finite {l..u(}"
   1.133 +  fixes l :: nat shows "finite {l..<u}"
   1.134  by (simp add: atLeastLessThan_def)
   1.135  
   1.136  lemma finite_greaterThanAtMost [iff]:
   1.137 -  fixes l :: nat shows "finite {)l..u}"
   1.138 +  fixes l :: nat shows "finite {l<..u}"
   1.139  by (simp add: greaterThanAtMost_def)
   1.140  
   1.141  lemma finite_atLeastAtMost [iff]:
   1.142 @@ -278,16 +292,16 @@
   1.143  
   1.144  subsubsection {* Cardinality *}
   1.145  
   1.146 -lemma card_lessThan [simp]: "card {..u(} = u"
   1.147 +lemma card_lessThan [simp]: "card {..<u} = u"
   1.148    by (induct_tac u, simp_all add: lessThan_Suc)
   1.149  
   1.150  lemma card_atMost [simp]: "card {..u} = Suc u"
   1.151    by (simp add: lessThan_Suc_atMost [THEN sym])
   1.152  
   1.153 -lemma card_atLeastLessThan [simp]: "card {l..u(} = u - l"
   1.154 -  apply (subgoal_tac "card {l..u(} = card {..u-l(}")
   1.155 +lemma card_atLeastLessThan [simp]: "card {l..<u} = u - l"
   1.156 +  apply (subgoal_tac "card {l..<u} = card {..<u-l}")
   1.157    apply (erule ssubst, rule card_lessThan)
   1.158 -  apply (subgoal_tac "(%x. x + l) ` {..u-l(} = {l..u(}")
   1.159 +  apply (subgoal_tac "(%x. x + l) ` {..<u-l} = {l..<u}")
   1.160    apply (erule subst)
   1.161    apply (rule card_image)
   1.162    apply (rule finite_lessThan)
   1.163 @@ -301,52 +315,52 @@
   1.164  lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"
   1.165    by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp)
   1.166  
   1.167 -lemma card_greaterThanAtMost [simp]: "card {)l..u} = u - l" 
   1.168 +lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l" 
   1.169    by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp)
   1.170  
   1.171 -lemma card_greaterThanLessThan [simp]: "card {)l..u(} = u - Suc l"
   1.172 +lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
   1.173    by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
   1.174  
   1.175  subsection {* Intervals of integers *}
   1.176  
   1.177 -lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..u+1(} = {l..(u::int)}"
   1.178 +lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}"
   1.179    by (auto simp add: atLeastAtMost_def atLeastLessThan_def)
   1.180  
   1.181 -lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {)l..(u::int)}"  
   1.182 +lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}"  
   1.183    by (auto simp add: atLeastAtMost_def greaterThanAtMost_def)
   1.184  
   1.185  lemma atLeastPlusOneLessThan_greaterThanLessThan_int: 
   1.186 -    "{l+1..u(} = {)l..(u::int)(}"  
   1.187 +    "{l+1..<u} = {l<..<u::int}"  
   1.188    by (auto simp add: atLeastLessThan_def greaterThanLessThan_def)
   1.189  
   1.190  subsubsection {* Finiteness *}
   1.191  
   1.192  lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
   1.193 -    {(0::int)..u(} = int ` {..nat u(}"
   1.194 +    {(0::int)..<u} = int ` {..<nat u}"
   1.195    apply (unfold image_def lessThan_def)
   1.196    apply auto
   1.197    apply (rule_tac x = "nat x" in exI)
   1.198    apply (auto simp add: zless_nat_conj zless_nat_eq_int_zless [THEN sym])
   1.199    done
   1.200  
   1.201 -lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..u(}"
   1.202 +lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}"
   1.203    apply (case_tac "0 \<le> u")
   1.204    apply (subst image_atLeastZeroLessThan_int, assumption)
   1.205    apply (rule finite_imageI)
   1.206    apply auto
   1.207 -  apply (subgoal_tac "{0..u(} = {}")
   1.208 +  apply (subgoal_tac "{0..<u} = {}")
   1.209    apply auto
   1.210    done
   1.211  
   1.212  lemma image_atLeastLessThan_int_shift: 
   1.213 -    "(%x. x + (l::int)) ` {0..u-l(} = {l..u(}"
   1.214 +    "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
   1.215    apply (auto simp add: image_def atLeastLessThan_iff)
   1.216    apply (rule_tac x = "x - l" in bexI)
   1.217    apply auto
   1.218    done
   1.219  
   1.220 -lemma finite_atLeastLessThan_int [iff]: "finite {l..(u::int)(}"
   1.221 -  apply (subgoal_tac "(%x. x + l) ` {0..u-l(} = {l..u(}")
   1.222 +lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}"
   1.223 +  apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}")
   1.224    apply (erule subst)
   1.225    apply (rule finite_imageI)
   1.226    apply (rule finite_atLeastZeroLessThan_int)
   1.227 @@ -356,25 +370,25 @@
   1.228  lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}" 
   1.229    by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp)
   1.230  
   1.231 -lemma finite_greaterThanAtMost_int [iff]: "finite {)l..(u::int)}" 
   1.232 +lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}" 
   1.233    by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
   1.234  
   1.235 -lemma finite_greaterThanLessThan_int [iff]: "finite {)l..(u::int)(}" 
   1.236 +lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}" 
   1.237    by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
   1.238  
   1.239  subsubsection {* Cardinality *}
   1.240  
   1.241 -lemma card_atLeastZeroLessThan_int: "card {(0::int)..u(} = nat u"
   1.242 +lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u"
   1.243    apply (case_tac "0 \<le> u")
   1.244    apply (subst image_atLeastZeroLessThan_int, assumption)
   1.245    apply (subst card_image)
   1.246    apply (auto simp add: inj_on_def)
   1.247    done
   1.248  
   1.249 -lemma card_atLeastLessThan_int [simp]: "card {l..u(} = nat (u - l)"
   1.250 -  apply (subgoal_tac "card {l..u(} = card {0..u-l(}")
   1.251 +lemma card_atLeastLessThan_int [simp]: "card {l..<u} = nat (u - l)"
   1.252 +  apply (subgoal_tac "card {l..<u} = card {0..<u-l}")
   1.253    apply (erule ssubst, rule card_atLeastZeroLessThan_int)
   1.254 -  apply (subgoal_tac "(%x. x + l) ` {0..u-l(} = {l..u(}")
   1.255 +  apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}")
   1.256    apply (erule subst)
   1.257    apply (rule card_image)
   1.258    apply (rule finite_atLeastZeroLessThan_int)
   1.259 @@ -387,10 +401,10 @@
   1.260    apply (auto simp add: compare_rls)
   1.261    done
   1.262  
   1.263 -lemma card_greaterThanAtMost_int [simp]: "card {)l..u} = nat (u - l)" 
   1.264 +lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)" 
   1.265    by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
   1.266  
   1.267 -lemma card_greaterThanLessThan_int [simp]: "card {)l..u(} = nat (u - (l + 1))"
   1.268 +lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u - (l + 1))"
   1.269    by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
   1.270  
   1.271  
   1.272 @@ -403,38 +417,38 @@
   1.273  text {* Singletons and open intervals *}
   1.274  
   1.275  lemma ivl_disj_un_singleton:
   1.276 -  "{l::'a::linorder} Un {)l..} = {l..}"
   1.277 -  "{..u(} Un {u::'a::linorder} = {..u}"
   1.278 -  "(l::'a::linorder) < u ==> {l} Un {)l..u(} = {l..u(}"
   1.279 -  "(l::'a::linorder) < u ==> {)l..u(} Un {u} = {)l..u}"
   1.280 -  "(l::'a::linorder) <= u ==> {l} Un {)l..u} = {l..u}"
   1.281 -  "(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}"
   1.282 +  "{l::'a::linorder} Un {l<..} = {l..}"
   1.283 +  "{..<u} Un {u::'a::linorder} = {..u}"
   1.284 +  "(l::'a::linorder) < u ==> {l} Un {l<..<u} = {l..<u}"
   1.285 +  "(l::'a::linorder) < u ==> {l<..<u} Un {u} = {l<..u}"
   1.286 +  "(l::'a::linorder) <= u ==> {l} Un {l<..u} = {l..u}"
   1.287 +  "(l::'a::linorder) <= u ==> {l..<u} Un {u} = {l..u}"
   1.288  by auto
   1.289  
   1.290  text {* One- and two-sided intervals *}
   1.291  
   1.292  lemma ivl_disj_un_one:
   1.293 -  "(l::'a::linorder) < u ==> {..l} Un {)l..u(} = {..u(}"
   1.294 -  "(l::'a::linorder) <= u ==> {..l(} Un {l..u(} = {..u(}"
   1.295 -  "(l::'a::linorder) <= u ==> {..l} Un {)l..u} = {..u}"
   1.296 -  "(l::'a::linorder) <= u ==> {..l(} Un {l..u} = {..u}"
   1.297 -  "(l::'a::linorder) <= u ==> {)l..u} Un {)u..} = {)l..}"
   1.298 -  "(l::'a::linorder) < u ==> {)l..u(} Un {u..} = {)l..}"
   1.299 -  "(l::'a::linorder) <= u ==> {l..u} Un {)u..} = {l..}"
   1.300 -  "(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}"
   1.301 +  "(l::'a::linorder) < u ==> {..l} Un {l<..<u} = {..<u}"
   1.302 +  "(l::'a::linorder) <= u ==> {..<l} Un {l..<u} = {..<u}"
   1.303 +  "(l::'a::linorder) <= u ==> {..l} Un {l<..u} = {..u}"
   1.304 +  "(l::'a::linorder) <= u ==> {..<l} Un {l..u} = {..u}"
   1.305 +  "(l::'a::linorder) <= u ==> {l<..u} Un {u<..} = {l<..}"
   1.306 +  "(l::'a::linorder) < u ==> {l<..<u} Un {u..} = {l<..}"
   1.307 +  "(l::'a::linorder) <= u ==> {l..u} Un {u<..} = {l..}"
   1.308 +  "(l::'a::linorder) <= u ==> {l..<u} Un {u..} = {l..}"
   1.309  by auto
   1.310  
   1.311  text {* Two- and two-sided intervals *}
   1.312  
   1.313  lemma ivl_disj_un_two:
   1.314 -  "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u(} = {)l..u(}"
   1.315 -  "[| (l::'a::linorder) <= m; m < u |] ==> {)l..m} Un {)m..u(} = {)l..u(}"
   1.316 -  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u(} = {l..u(}"
   1.317 -  "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {)m..u(} = {l..u(}"
   1.318 -  "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u} = {)l..u}"
   1.319 -  "[| (l::'a::linorder) <= m; m <= u |] ==> {)l..m} Un {)m..u} = {)l..u}"
   1.320 -  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u} = {l..u}"
   1.321 -  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {)m..u} = {l..u}"
   1.322 +  "[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..<u} = {l<..<u}"
   1.323 +  "[| (l::'a::linorder) <= m; m < u |] ==> {l<..m} Un {m<..<u} = {l<..<u}"
   1.324 +  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..<u} = {l..<u}"
   1.325 +  "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {m<..<u} = {l..<u}"
   1.326 +  "[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..u} = {l<..u}"
   1.327 +  "[| (l::'a::linorder) <= m; m <= u |] ==> {l<..m} Un {m<..u} = {l<..u}"
   1.328 +  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..u} = {l..u}"
   1.329 +  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m<..u} = {l..u}"
   1.330  by auto
   1.331  
   1.332  lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
   1.333 @@ -444,38 +458,38 @@
   1.334  text {* Singletons and open intervals *}
   1.335  
   1.336  lemma ivl_disj_int_singleton:
   1.337 -  "{l::'a::order} Int {)l..} = {}"
   1.338 -  "{..u(} Int {u} = {}"
   1.339 -  "{l} Int {)l..u(} = {}"
   1.340 -  "{)l..u(} Int {u} = {}"
   1.341 -  "{l} Int {)l..u} = {}"
   1.342 -  "{l..u(} Int {u} = {}"
   1.343 +  "{l::'a::order} Int {l<..} = {}"
   1.344 +  "{..<u} Int {u} = {}"
   1.345 +  "{l} Int {l<..<u} = {}"
   1.346 +  "{l<..<u} Int {u} = {}"
   1.347 +  "{l} Int {l<..u} = {}"
   1.348 +  "{l..<u} Int {u} = {}"
   1.349    by simp+
   1.350  
   1.351  text {* One- and two-sided intervals *}
   1.352  
   1.353  lemma ivl_disj_int_one:
   1.354 -  "{..l::'a::order} Int {)l..u(} = {}"
   1.355 -  "{..l(} Int {l..u(} = {}"
   1.356 -  "{..l} Int {)l..u} = {}"
   1.357 -  "{..l(} Int {l..u} = {}"
   1.358 -  "{)l..u} Int {)u..} = {}"
   1.359 -  "{)l..u(} Int {u..} = {}"
   1.360 -  "{l..u} Int {)u..} = {}"
   1.361 -  "{l..u(} Int {u..} = {}"
   1.362 +  "{..l::'a::order} Int {l<..<u} = {}"
   1.363 +  "{..<l} Int {l..<u} = {}"
   1.364 +  "{..l} Int {l<..u} = {}"
   1.365 +  "{..<l} Int {l..u} = {}"
   1.366 +  "{l<..u} Int {u<..} = {}"
   1.367 +  "{l<..<u} Int {u..} = {}"
   1.368 +  "{l..u} Int {u<..} = {}"
   1.369 +  "{l..<u} Int {u..} = {}"
   1.370    by auto
   1.371  
   1.372  text {* Two- and two-sided intervals *}
   1.373  
   1.374  lemma ivl_disj_int_two:
   1.375 -  "{)l::'a::order..m(} Int {m..u(} = {}"
   1.376 -  "{)l..m} Int {)m..u(} = {}"
   1.377 -  "{l..m(} Int {m..u(} = {}"
   1.378 -  "{l..m} Int {)m..u(} = {}"
   1.379 -  "{)l..m(} Int {m..u} = {}"
   1.380 -  "{)l..m} Int {)m..u} = {}"
   1.381 -  "{l..m(} Int {m..u} = {}"
   1.382 -  "{l..m} Int {)m..u} = {}"
   1.383 +  "{l::'a::order<..<m} Int {m..<u} = {}"
   1.384 +  "{l<..m} Int {m<..<u} = {}"
   1.385 +  "{l..<m} Int {m..<u} = {}"
   1.386 +  "{l..m} Int {m<..<u} = {}"
   1.387 +  "{l<..<m} Int {m..u} = {}"
   1.388 +  "{l<..m} Int {m<..u} = {}"
   1.389 +  "{l..<m} Int {m..u} = {}"
   1.390 +  "{l..m} Int {m<..u} = {}"
   1.391    by auto
   1.392  
   1.393  lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
   1.394 @@ -504,7 +518,7 @@
   1.395  syntax
   1.396    "_Summation" :: "idt => 'a => 'b => 'b"    ("\<Sum>_<_. _" [0, 51, 10] 10)
   1.397  translations
   1.398 -  "\<Sum>i < n. b" == "setsum (\<lambda>i. b) {..n(}"
   1.399 +  "\<Sum>i < n. b" == "setsum (\<lambda>i. b) {..<n}"
   1.400  
   1.401  lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
   1.402  by (simp add:lessThan_Suc)