src/HOL/SetInterval.thy
 author nipkow Wed Jul 14 10:25:03 2004 +0200 (2004-07-14) changeset 15042 fa7d27ef7e59 parent 15041 a6b1f0cef7b3 child 15045 d59f7e2e18d3 permissions -rw-r--r--
```     1 (*  Title:      HOL/SetInterval.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Tobias Nipkow and Clemens Ballarin
```
```     4                 Additions by Jeremy Avigad in March 2004
```
```     5     Copyright   2000  TU Muenchen
```
```     6
```
```     7 lessThan, greaterThan, atLeast, atMost and two-sided intervals
```
```     8 *)
```
```     9
```
```    10 header {* Set intervals *}
```
```    11
```
```    12 theory SetInterval = IntArith:
```
```    13
```
```    14 constdefs
```
```    15   lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
```
```    16   "{..u(} == {x. x<u}"
```
```    17
```
```    18   atMost      :: "('a::ord) => 'a set"	("(1{.._})")
```
```    19   "{..u} == {x. x<=u}"
```
```    20
```
```    21   greaterThan :: "('a::ord) => 'a set"	("(1{')_..})")
```
```    22   "{)l..} == {x. l<x}"
```
```    23
```
```    24   atLeast     :: "('a::ord) => 'a set"	("(1{_..})")
```
```    25   "{l..} == {x. l<=x}"
```
```    26
```
```    27   greaterThanLessThan :: "['a::ord, 'a] => 'a set"  ("(1{')_.._'(})")
```
```    28   "{)l..u(} == {)l..} Int {..u(}"
```
```    29
```
```    30   atLeastLessThan :: "['a::ord, 'a] => 'a set"      ("(1{_.._'(})")
```
```    31   "{l..u(} == {l..} Int {..u(}"
```
```    32
```
```    33   greaterThanAtMost :: "['a::ord, 'a] => 'a set"    ("(1{')_.._})")
```
```    34   "{)l..u} == {)l..} Int {..u}"
```
```    35
```
```    36   atLeastAtMost :: "['a::ord, 'a] => 'a set"        ("(1{_.._})")
```
```    37   "{l..u} == {l..} Int {..u}"
```
```    38
```
```    39 syntax
```
```    40   "@UNION_le"   :: "nat => nat => 'b set => 'b set"       ("(3UN _<=_./ _)" 10)
```
```    41   "@UNION_less" :: "nat => nat => 'b set => 'b set"       ("(3UN _<_./ _)" 10)
```
```    42   "@INTER_le"   :: "nat => nat => 'b set => 'b set"       ("(3INT _<=_./ _)" 10)
```
```    43   "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3INT _<_./ _)" 10)
```
```    44
```
```    45 syntax (input)
```
```    46   "@UNION_le"   :: "nat => nat => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" 10)
```
```    47   "@UNION_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Union> _<_./ _)" 10)
```
```    48   "@INTER_le"   :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" 10)
```
```    49   "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
```
```    50
```
```    51 syntax (xsymbols)
```
```    52   "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10)
```
```    53   "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00\<^bsub>_ < _\<^esub>)/ _)" 10)
```
```    54   "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10)
```
```    55   "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00\<^bsub>_ < _\<^esub>)/ _)" 10)
```
```    56
```
```    57 translations
```
```    58   "UN i<=n. A"  == "UN i:{..n}. A"
```
```    59   "UN i<n. A"   == "UN i:{..n(}. A"
```
```    60   "INT i<=n. A" == "INT i:{..n}. A"
```
```    61   "INT i<n. A"  == "INT i:{..n(}. A"
```
```    62
```
```    63
```
```    64 subsection {* Various equivalences *}
```
```    65
```
```    66 lemma lessThan_iff [iff]: "(i: lessThan k) = (i<k)"
```
```    67 by (simp add: lessThan_def)
```
```    68
```
```    69 lemma Compl_lessThan [simp]:
```
```    70     "!!k:: 'a::linorder. -lessThan k = atLeast k"
```
```    71 apply (auto simp add: lessThan_def atLeast_def)
```
```    72 done
```
```    73
```
```    74 lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}"
```
```    75 by auto
```
```    76
```
```    77 lemma greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)"
```
```    78 by (simp add: greaterThan_def)
```
```    79
```
```    80 lemma Compl_greaterThan [simp]:
```
```    81     "!!k:: 'a::linorder. -greaterThan k = atMost k"
```
```    82 apply (simp add: greaterThan_def atMost_def le_def, auto)
```
```    83 done
```
```    84
```
```    85 lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k"
```
```    86 apply (subst Compl_greaterThan [symmetric])
```
```    87 apply (rule double_complement)
```
```    88 done
```
```    89
```
```    90 lemma atLeast_iff [iff]: "(i: atLeast k) = (k<=i)"
```
```    91 by (simp add: atLeast_def)
```
```    92
```
```    93 lemma Compl_atLeast [simp]:
```
```    94     "!!k:: 'a::linorder. -atLeast k = lessThan k"
```
```    95 apply (simp add: lessThan_def atLeast_def le_def, auto)
```
```    96 done
```
```    97
```
```    98 lemma atMost_iff [iff]: "(i: atMost k) = (i<=k)"
```
```    99 by (simp add: atMost_def)
```
```   100
```
```   101 lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
```
```   102 by (blast intro: order_antisym)
```
```   103
```
```   104
```
```   105 subsection {* Logical Equivalences for Set Inclusion and Equality *}
```
```   106
```
```   107 lemma atLeast_subset_iff [iff]:
```
```   108      "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))"
```
```   109 by (blast intro: order_trans)
```
```   110
```
```   111 lemma atLeast_eq_iff [iff]:
```
```   112      "(atLeast x = atLeast y) = (x = (y::'a::linorder))"
```
```   113 by (blast intro: order_antisym order_trans)
```
```   114
```
```   115 lemma greaterThan_subset_iff [iff]:
```
```   116      "(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))"
```
```   117 apply (auto simp add: greaterThan_def)
```
```   118  apply (subst linorder_not_less [symmetric], blast)
```
```   119 done
```
```   120
```
```   121 lemma greaterThan_eq_iff [iff]:
```
```   122      "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"
```
```   123 apply (rule iffI)
```
```   124  apply (erule equalityE)
```
```   125  apply (simp add: greaterThan_subset_iff order_antisym, simp)
```
```   126 done
```
```   127
```
```   128 lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))"
```
```   129 by (blast intro: order_trans)
```
```   130
```
```   131 lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"
```
```   132 by (blast intro: order_antisym order_trans)
```
```   133
```
```   134 lemma lessThan_subset_iff [iff]:
```
```   135      "(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))"
```
```   136 apply (auto simp add: lessThan_def)
```
```   137  apply (subst linorder_not_less [symmetric], blast)
```
```   138 done
```
```   139
```
```   140 lemma lessThan_eq_iff [iff]:
```
```   141      "(lessThan x = lessThan y) = (x = (y::'a::linorder))"
```
```   142 apply (rule iffI)
```
```   143  apply (erule equalityE)
```
```   144  apply (simp add: lessThan_subset_iff order_antisym, simp)
```
```   145 done
```
```   146
```
```   147
```
```   148 subsection {*Two-sided intervals*}
```
```   149
```
```   150 text {* @{text greaterThanLessThan} *}
```
```   151
```
```   152 lemma greaterThanLessThan_iff [simp]:
```
```   153   "(i : {)l..u(}) = (l < i & i < u)"
```
```   154 by (simp add: greaterThanLessThan_def)
```
```   155
```
```   156 text {* @{text atLeastLessThan} *}
```
```   157
```
```   158 lemma atLeastLessThan_iff [simp]:
```
```   159   "(i : {l..u(}) = (l <= i & i < u)"
```
```   160 by (simp add: atLeastLessThan_def)
```
```   161
```
```   162 text {* @{text greaterThanAtMost} *}
```
```   163
```
```   164 lemma greaterThanAtMost_iff [simp]:
```
```   165   "(i : {)l..u}) = (l < i & i <= u)"
```
```   166 by (simp add: greaterThanAtMost_def)
```
```   167
```
```   168 text {* @{text atLeastAtMost} *}
```
```   169
```
```   170 lemma atLeastAtMost_iff [simp]:
```
```   171   "(i : {l..u}) = (l <= i & i <= u)"
```
```   172 by (simp add: atLeastAtMost_def)
```
```   173
```
```   174 text {* The above four lemmas could be declared as iffs.
```
```   175   If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int}
```
```   176   seems to take forever (more than one hour). *}
```
```   177
```
```   178
```
```   179 subsection {* Intervals of natural numbers *}
```
```   180
```
```   181 lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"
```
```   182 by (simp add: lessThan_def)
```
```   183
```
```   184 lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
```
```   185 by (simp add: lessThan_def less_Suc_eq, blast)
```
```   186
```
```   187 lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
```
```   188 by (simp add: lessThan_def atMost_def less_Suc_eq_le)
```
```   189
```
```   190 lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
```
```   191 by blast
```
```   192
```
```   193 lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
```
```   194 apply (simp add: greaterThan_def)
```
```   195 apply (blast dest: gr0_conv_Suc [THEN iffD1])
```
```   196 done
```
```   197
```
```   198 lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"
```
```   199 apply (simp add: greaterThan_def)
```
```   200 apply (auto elim: linorder_neqE)
```
```   201 done
```
```   202
```
```   203 lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
```
```   204 by blast
```
```   205
```
```   206 lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"
```
```   207 by (unfold atLeast_def UNIV_def, simp)
```
```   208
```
```   209 lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"
```
```   210 apply (simp add: atLeast_def)
```
```   211 apply (simp add: Suc_le_eq)
```
```   212 apply (simp add: order_le_less, blast)
```
```   213 done
```
```   214
```
```   215 lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"
```
```   216   by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)
```
```   217
```
```   218 lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
```
```   219 by blast
```
```   220
```
```   221 lemma atMost_0 [simp]: "atMost (0::nat) = {0}"
```
```   222 by (simp add: atMost_def)
```
```   223
```
```   224 lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
```
```   225 apply (simp add: atMost_def)
```
```   226 apply (simp add: less_Suc_eq order_le_less, blast)
```
```   227 done
```
```   228
```
```   229 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
```
```   230 by blast
```
```   231
```
```   232 lemma atLeast0LessThan [simp]: "{0::nat..n(} = {..n(}"
```
```   233 by(simp add:lessThan_def atLeastLessThan_def)
```
```   234
```
```   235 text {* Intervals of nats with @{text Suc} *}
```
```   236
```
```   237 lemma atLeastLessThanSuc_atLeastAtMost: "{l..Suc u(} = {l..u}"
```
```   238   by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
```
```   239
```
```   240 lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {)l..u}"
```
```   241   by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def
```
```   242     greaterThanAtMost_def)
```
```   243
```
```   244 lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..u(} = {)l..u(}"
```
```   245   by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def
```
```   246     greaterThanLessThan_def)
```
```   247
```
```   248 subsubsection {* Finiteness *}
```
```   249
```
```   250 lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
```
```   251   by (induct k) (simp_all add: lessThan_Suc)
```
```   252
```
```   253 lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
```
```   254   by (induct k) (simp_all add: atMost_Suc)
```
```   255
```
```   256 lemma finite_greaterThanLessThan [iff]:
```
```   257   fixes l :: nat shows "finite {)l..u(}"
```
```   258 by (simp add: greaterThanLessThan_def)
```
```   259
```
```   260 lemma finite_atLeastLessThan [iff]:
```
```   261   fixes l :: nat shows "finite {l..u(}"
```
```   262 by (simp add: atLeastLessThan_def)
```
```   263
```
```   264 lemma finite_greaterThanAtMost [iff]:
```
```   265   fixes l :: nat shows "finite {)l..u}"
```
```   266 by (simp add: greaterThanAtMost_def)
```
```   267
```
```   268 lemma finite_atLeastAtMost [iff]:
```
```   269   fixes l :: nat shows "finite {l..u}"
```
```   270 by (simp add: atLeastAtMost_def)
```
```   271
```
```   272 lemma bounded_nat_set_is_finite:
```
```   273     "(ALL i:N. i < (n::nat)) ==> finite N"
```
```   274   -- {* A bounded set of natural numbers is finite. *}
```
```   275   apply (rule finite_subset)
```
```   276    apply (rule_tac [2] finite_lessThan, auto)
```
```   277   done
```
```   278
```
```   279 subsubsection {* Cardinality *}
```
```   280
```
```   281 lemma card_lessThan [simp]: "card {..u(} = u"
```
```   282   by (induct_tac u, simp_all add: lessThan_Suc)
```
```   283
```
```   284 lemma card_atMost [simp]: "card {..u} = Suc u"
```
```   285   by (simp add: lessThan_Suc_atMost [THEN sym])
```
```   286
```
```   287 lemma card_atLeastLessThan [simp]: "card {l..u(} = u - l"
```
```   288   apply (subgoal_tac "card {l..u(} = card {..u-l(}")
```
```   289   apply (erule ssubst, rule card_lessThan)
```
```   290   apply (subgoal_tac "(%x. x + l) ` {..u-l(} = {l..u(}")
```
```   291   apply (erule subst)
```
```   292   apply (rule card_image)
```
```   293   apply (rule finite_lessThan)
```
```   294   apply (simp add: inj_on_def)
```
```   295   apply (auto simp add: image_def atLeastLessThan_def lessThan_def)
```
```   296   apply arith
```
```   297   apply (rule_tac x = "x - l" in exI)
```
```   298   apply arith
```
```   299   done
```
```   300
```
```   301 lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"
```
```   302   by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp)
```
```   303
```
```   304 lemma card_greaterThanAtMost [simp]: "card {)l..u} = u - l"
```
```   305   by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp)
```
```   306
```
```   307 lemma card_greaterThanLessThan [simp]: "card {)l..u(} = u - Suc l"
```
```   308   by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
```
```   309
```
```   310 subsection {* Intervals of integers *}
```
```   311
```
```   312 lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..u+1(} = {l..(u::int)}"
```
```   313   by (auto simp add: atLeastAtMost_def atLeastLessThan_def)
```
```   314
```
```   315 lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {)l..(u::int)}"
```
```   316   by (auto simp add: atLeastAtMost_def greaterThanAtMost_def)
```
```   317
```
```   318 lemma atLeastPlusOneLessThan_greaterThanLessThan_int:
```
```   319     "{l+1..u(} = {)l..(u::int)(}"
```
```   320   by (auto simp add: atLeastLessThan_def greaterThanLessThan_def)
```
```   321
```
```   322 subsubsection {* Finiteness *}
```
```   323
```
```   324 lemma image_atLeastZeroLessThan_int: "0 \<le> u ==>
```
```   325     {(0::int)..u(} = int ` {..nat u(}"
```
```   326   apply (unfold image_def lessThan_def)
```
```   327   apply auto
```
```   328   apply (rule_tac x = "nat x" in exI)
```
```   329   apply (auto simp add: zless_nat_conj zless_nat_eq_int_zless [THEN sym])
```
```   330   done
```
```   331
```
```   332 lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..u(}"
```
```   333   apply (case_tac "0 \<le> u")
```
```   334   apply (subst image_atLeastZeroLessThan_int, assumption)
```
```   335   apply (rule finite_imageI)
```
```   336   apply auto
```
```   337   apply (subgoal_tac "{0..u(} = {}")
```
```   338   apply auto
```
```   339   done
```
```   340
```
```   341 lemma image_atLeastLessThan_int_shift:
```
```   342     "(%x. x + (l::int)) ` {0..u-l(} = {l..u(}"
```
```   343   apply (auto simp add: image_def atLeastLessThan_iff)
```
```   344   apply (rule_tac x = "x - l" in bexI)
```
```   345   apply auto
```
```   346   done
```
```   347
```
```   348 lemma finite_atLeastLessThan_int [iff]: "finite {l..(u::int)(}"
```
```   349   apply (subgoal_tac "(%x. x + l) ` {0..u-l(} = {l..u(}")
```
```   350   apply (erule subst)
```
```   351   apply (rule finite_imageI)
```
```   352   apply (rule finite_atLeastZeroLessThan_int)
```
```   353   apply (rule image_atLeastLessThan_int_shift)
```
```   354   done
```
```   355
```
```   356 lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}"
```
```   357   by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp)
```
```   358
```
```   359 lemma finite_greaterThanAtMost_int [iff]: "finite {)l..(u::int)}"
```
```   360   by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
```
```   361
```
```   362 lemma finite_greaterThanLessThan_int [iff]: "finite {)l..(u::int)(}"
```
```   363   by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
```
```   364
```
```   365 subsubsection {* Cardinality *}
```
```   366
```
```   367 lemma card_atLeastZeroLessThan_int: "card {(0::int)..u(} = nat u"
```
```   368   apply (case_tac "0 \<le> u")
```
```   369   apply (subst image_atLeastZeroLessThan_int, assumption)
```
```   370   apply (subst card_image)
```
```   371   apply (auto simp add: inj_on_def)
```
```   372   done
```
```   373
```
```   374 lemma card_atLeastLessThan_int [simp]: "card {l..u(} = nat (u - l)"
```
```   375   apply (subgoal_tac "card {l..u(} = card {0..u-l(}")
```
```   376   apply (erule ssubst, rule card_atLeastZeroLessThan_int)
```
```   377   apply (subgoal_tac "(%x. x + l) ` {0..u-l(} = {l..u(}")
```
```   378   apply (erule subst)
```
```   379   apply (rule card_image)
```
```   380   apply (rule finite_atLeastZeroLessThan_int)
```
```   381   apply (simp add: inj_on_def)
```
```   382   apply (rule image_atLeastLessThan_int_shift)
```
```   383   done
```
```   384
```
```   385 lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)"
```
```   386   apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym])
```
```   387   apply (auto simp add: compare_rls)
```
```   388   done
```
```   389
```
```   390 lemma card_greaterThanAtMost_int [simp]: "card {)l..u} = nat (u - l)"
```
```   391   by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
```
```   392
```
```   393 lemma card_greaterThanLessThan_int [simp]: "card {)l..u(} = nat (u - (l + 1))"
```
```   394   by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
```
```   395
```
```   396
```
```   397 subsection {*Lemmas useful with the summation operator setsum*}
```
```   398
```
```   399 text {* For examples, see Algebra/poly/UnivPoly.thy *}
```
```   400
```
```   401 subsubsection {* Disjoint Unions *}
```
```   402
```
```   403 text {* Singletons and open intervals *}
```
```   404
```
```   405 lemma ivl_disj_un_singleton:
```
```   406   "{l::'a::linorder} Un {)l..} = {l..}"
```
```   407   "{..u(} Un {u::'a::linorder} = {..u}"
```
```   408   "(l::'a::linorder) < u ==> {l} Un {)l..u(} = {l..u(}"
```
```   409   "(l::'a::linorder) < u ==> {)l..u(} Un {u} = {)l..u}"
```
```   410   "(l::'a::linorder) <= u ==> {l} Un {)l..u} = {l..u}"
```
```   411   "(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}"
```
```   412 by auto
```
```   413
```
```   414 text {* One- and two-sided intervals *}
```
```   415
```
```   416 lemma ivl_disj_un_one:
```
```   417   "(l::'a::linorder) < u ==> {..l} Un {)l..u(} = {..u(}"
```
```   418   "(l::'a::linorder) <= u ==> {..l(} Un {l..u(} = {..u(}"
```
```   419   "(l::'a::linorder) <= u ==> {..l} Un {)l..u} = {..u}"
```
```   420   "(l::'a::linorder) <= u ==> {..l(} Un {l..u} = {..u}"
```
```   421   "(l::'a::linorder) <= u ==> {)l..u} Un {)u..} = {)l..}"
```
```   422   "(l::'a::linorder) < u ==> {)l..u(} Un {u..} = {)l..}"
```
```   423   "(l::'a::linorder) <= u ==> {l..u} Un {)u..} = {l..}"
```
```   424   "(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}"
```
```   425 by auto
```
```   426
```
```   427 text {* Two- and two-sided intervals *}
```
```   428
```
```   429 lemma ivl_disj_un_two:
```
```   430   "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u(} = {)l..u(}"
```
```   431   "[| (l::'a::linorder) <= m; m < u |] ==> {)l..m} Un {)m..u(} = {)l..u(}"
```
```   432   "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u(} = {l..u(}"
```
```   433   "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {)m..u(} = {l..u(}"
```
```   434   "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u} = {)l..u}"
```
```   435   "[| (l::'a::linorder) <= m; m <= u |] ==> {)l..m} Un {)m..u} = {)l..u}"
```
```   436   "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u} = {l..u}"
```
```   437   "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {)m..u} = {l..u}"
```
```   438 by auto
```
```   439
```
```   440 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
```
```   441
```
```   442 subsubsection {* Disjoint Intersections *}
```
```   443
```
```   444 text {* Singletons and open intervals *}
```
```   445
```
```   446 lemma ivl_disj_int_singleton:
```
```   447   "{l::'a::order} Int {)l..} = {}"
```
```   448   "{..u(} Int {u} = {}"
```
```   449   "{l} Int {)l..u(} = {}"
```
```   450   "{)l..u(} Int {u} = {}"
```
```   451   "{l} Int {)l..u} = {}"
```
```   452   "{l..u(} Int {u} = {}"
```
```   453   by simp+
```
```   454
```
```   455 text {* One- and two-sided intervals *}
```
```   456
```
```   457 lemma ivl_disj_int_one:
```
```   458   "{..l::'a::order} Int {)l..u(} = {}"
```
```   459   "{..l(} Int {l..u(} = {}"
```
```   460   "{..l} Int {)l..u} = {}"
```
```   461   "{..l(} Int {l..u} = {}"
```
```   462   "{)l..u} Int {)u..} = {}"
```
```   463   "{)l..u(} Int {u..} = {}"
```
```   464   "{l..u} Int {)u..} = {}"
```
```   465   "{l..u(} Int {u..} = {}"
```
```   466   by auto
```
```   467
```
```   468 text {* Two- and two-sided intervals *}
```
```   469
```
```   470 lemma ivl_disj_int_two:
```
```   471   "{)l::'a::order..m(} Int {m..u(} = {}"
```
```   472   "{)l..m} Int {)m..u(} = {}"
```
```   473   "{l..m(} Int {m..u(} = {}"
```
```   474   "{l..m} Int {)m..u(} = {}"
```
```   475   "{)l..m(} Int {m..u} = {}"
```
```   476   "{)l..m} Int {)m..u} = {}"
```
```   477   "{l..m(} Int {m..u} = {}"
```
```   478   "{l..m} Int {)m..u} = {}"
```
```   479   by auto
```
```   480
```
```   481 lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
```
```   482
```
```   483
```
```   484 subsection {* Summation indexed over intervals *}
```
```   485
```
```   486 text{* We introduce the obvious syntax @{text"\<Sum>x=a..b. e"} for
```
```   487 @{term"\<Sum>x\<in>{a..b}. e"}. *}
```
```   488
```
```   489 syntax
```
```   490   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)
```
```   491 syntax (xsymbols)
```
```   492   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
```
```   493 syntax (HTML output)
```
```   494   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
```
```   495
```
```   496 translations "\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}"
```
```   497
```
```   498
```
```   499 subsection {* Summation up to *}
```
```   500
```
```   501 text{* Legacy, only used in HoareParallel and Isar-Examples. Really
```
```   502 needed? Probably better to replace it with above syntax. *}
```
```   503
```
```   504 syntax
```
```   505   "_Summation" :: "idt => 'a => 'b => 'b"    ("\<Sum>_<_. _" [0, 51, 10] 10)
```
```   506 translations
```
```   507   "\<Sum>i < n. b" == "setsum (\<lambda>i. b) {..n(}"
```
```   508
```
```   509 lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
```
```   510 by (simp add:lessThan_Suc)
```
```   511
```
```   512 end
```