src/HOL/SetInterval.thy
author nipkow
Fri Mar 19 11:06:53 2004 +0100 (2004-03-19)
changeset 14478 bdf6b7adc3ec
parent 14418 b62323c85134
child 14485 ea2707645af8
permissions -rw-r--r--
added a few 0 and Suc lemmas
     1 (*  Title:      HOL/SetInterval.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Clemens Ballarin
     4     Copyright   2000  TU Muenchen
     5 
     6 lessThan, greaterThan, atLeast, atMost and two-sided intervals
     7 *)
     8 
     9 theory SetInterval = NatArith:
    10 
    11 constdefs
    12   lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
    13   "{..u(} == {x. x<u}"
    14 
    15   atMost      :: "('a::ord) => 'a set"	("(1{.._})")
    16   "{..u} == {x. x<=u}"
    17 
    18   greaterThan :: "('a::ord) => 'a set"	("(1{')_..})")
    19   "{)l..} == {x. l<x}"
    20 
    21   atLeast     :: "('a::ord) => 'a set"	("(1{_..})")
    22   "{l..} == {x. l<=x}"
    23 
    24   greaterThanLessThan :: "['a::ord, 'a] => 'a set"  ("(1{')_.._'(})")
    25   "{)l..u(} == {)l..} Int {..u(}"
    26 
    27   atLeastLessThan :: "['a::ord, 'a] => 'a set"      ("(1{_.._'(})")
    28   "{l..u(} == {l..} Int {..u(}"
    29 
    30   greaterThanAtMost :: "['a::ord, 'a] => 'a set"    ("(1{')_.._})")
    31   "{)l..u} == {)l..} Int {..u}"
    32 
    33   atLeastAtMost :: "['a::ord, 'a] => 'a set"        ("(1{_.._})")
    34   "{l..u} == {l..} Int {..u}"
    35 
    36 syntax
    37   "@UNION_le"   :: "nat => nat => 'b set => 'b set"       ("(3UN _<=_./ _)" 10)
    38   "@UNION_less" :: "nat => nat => 'b set => 'b set"       ("(3UN _<_./ _)" 10)
    39   "@INTER_le"   :: "nat => nat => 'b set => 'b set"       ("(3INT _<=_./ _)" 10)
    40   "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3INT _<_./ _)" 10)
    41 
    42 syntax (input)
    43   "@UNION_le"   :: "nat => nat => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" 10)
    44   "@UNION_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Union> _<_./ _)" 10)
    45   "@INTER_le"   :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" 10)
    46   "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
    47 
    48 syntax (xsymbols)
    49   "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>\<^bsub>_ \<le> _\<^esub>/ _)" 10)
    50   "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>\<^bsub>_ < _\<^esub>/ _)" 10)
    51   "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>\<^bsub>_ \<le> _\<^esub>/ _)" 10)
    52   "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>\<^bsub>_ < _\<^esub>/ _)" 10)
    53 
    54 translations
    55   "UN i<=n. A"  == "UN i:{..n}. A"
    56   "UN i<n. A"   == "UN i:{..n(}. A"
    57   "INT i<=n. A" == "INT i:{..n}. A"
    58   "INT i<n. A"  == "INT i:{..n(}. A"
    59 
    60 
    61 subsection {*lessThan*}
    62 
    63 lemma lessThan_iff [iff]: "(i: lessThan k) = (i<k)"
    64 by (simp add: lessThan_def)
    65 
    66 lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"
    67 by (simp add: lessThan_def)
    68 
    69 lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
    70 by (simp add: lessThan_def less_Suc_eq, blast)
    71 
    72 lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
    73 by (simp add: lessThan_def atMost_def less_Suc_eq_le)
    74 
    75 lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
    76 by blast
    77 
    78 lemma Compl_lessThan [simp]: 
    79     "!!k:: 'a::linorder. -lessThan k = atLeast k"
    80 apply (auto simp add: lessThan_def atLeast_def)
    81 done
    82 
    83 lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}"
    84 by auto
    85 
    86 subsection {*greaterThan*}
    87 
    88 lemma greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)"
    89 by (simp add: greaterThan_def)
    90 
    91 lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
    92 apply (simp add: greaterThan_def)
    93 apply (blast dest: gr0_conv_Suc [THEN iffD1])
    94 done
    95 
    96 lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"
    97 apply (simp add: greaterThan_def)
    98 apply (auto elim: linorder_neqE)
    99 done
   100 
   101 lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
   102 by blast
   103 
   104 lemma Compl_greaterThan [simp]: 
   105     "!!k:: 'a::linorder. -greaterThan k = atMost k"
   106 apply (simp add: greaterThan_def atMost_def le_def, auto)
   107 done
   108 
   109 lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k"
   110 apply (subst Compl_greaterThan [symmetric])
   111 apply (rule double_complement) 
   112 done
   113 
   114 
   115 subsection {*atLeast*}
   116 
   117 lemma atLeast_iff [iff]: "(i: atLeast k) = (k<=i)"
   118 by (simp add: atLeast_def)
   119 
   120 lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"
   121 by (unfold atLeast_def UNIV_def, simp)
   122 
   123 lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"
   124 apply (simp add: atLeast_def)
   125 apply (simp add: Suc_le_eq)
   126 apply (simp add: order_le_less, blast)
   127 done
   128 
   129 lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
   130 by blast
   131 
   132 lemma Compl_atLeast [simp]: 
   133     "!!k:: 'a::linorder. -atLeast k = lessThan k"
   134 apply (simp add: lessThan_def atLeast_def le_def, auto)
   135 done
   136 
   137 
   138 subsection {*atMost*}
   139 
   140 lemma atMost_iff [iff]: "(i: atMost k) = (i<=k)"
   141 by (simp add: atMost_def)
   142 
   143 lemma atMost_0 [simp]: "atMost (0::nat) = {0}"
   144 by (simp add: atMost_def)
   145 
   146 lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
   147 apply (simp add: atMost_def)
   148 apply (simp add: less_Suc_eq order_le_less, blast)
   149 done
   150 
   151 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
   152 by blast
   153 
   154 
   155 subsection {*Logical Equivalences for Set Inclusion and Equality*}
   156 
   157 lemma atLeast_subset_iff [iff]:
   158      "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))" 
   159 by (blast intro: order_trans) 
   160 
   161 lemma atLeast_eq_iff [iff]:
   162      "(atLeast x = atLeast y) = (x = (y::'a::linorder))" 
   163 by (blast intro: order_antisym order_trans)
   164 
   165 lemma greaterThan_subset_iff [iff]:
   166      "(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))" 
   167 apply (auto simp add: greaterThan_def) 
   168  apply (subst linorder_not_less [symmetric], blast) 
   169 done
   170 
   171 lemma greaterThan_eq_iff [iff]:
   172      "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" 
   173 apply (rule iffI) 
   174  apply (erule equalityE) 
   175  apply (simp add: greaterThan_subset_iff order_antisym, simp) 
   176 done
   177 
   178 lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))" 
   179 by (blast intro: order_trans)
   180 
   181 lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" 
   182 by (blast intro: order_antisym order_trans)
   183 
   184 lemma lessThan_subset_iff [iff]:
   185      "(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))" 
   186 apply (auto simp add: lessThan_def) 
   187  apply (subst linorder_not_less [symmetric], blast) 
   188 done
   189 
   190 lemma lessThan_eq_iff [iff]:
   191      "(lessThan x = lessThan y) = (x = (y::'a::linorder))" 
   192 apply (rule iffI) 
   193  apply (erule equalityE) 
   194  apply (simp add: lessThan_subset_iff order_antisym, simp) 
   195 done
   196 
   197 
   198 subsection {*Combined properties*}
   199 
   200 lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
   201 by (blast intro: order_antisym)
   202 
   203 subsection {*Two-sided intervals*}
   204 
   205 (* greaterThanLessThan *)
   206 
   207 lemma greaterThanLessThan_iff [simp]:
   208   "(i : {)l..u(}) = (l < i & i < u)"
   209 by (simp add: greaterThanLessThan_def)
   210 
   211 lemma greaterThanLessThan_0 [simp]: "{)l..0::nat(} == {}"
   212 by (simp add: greaterThanLessThan_def)
   213 
   214 lemma greaterThanLessThan_Suc_greaterThanAtMost:
   215   "{)l..Suc n(} = {)l..n}"
   216 by (auto simp add: greaterThanLessThan_def greaterThanAtMost_def)
   217 
   218 (* atLeastLessThan *)
   219 
   220 lemma atLeastLessThan_iff [simp]:
   221   "(i : {l..u(}) = (l <= i & i < u)"
   222 by (simp add: atLeastLessThan_def)
   223 
   224 lemma atLeastLessThan_0 [simp]: "{l..0::nat(} == {}"
   225 by (simp add: atLeastLessThan_def)
   226 
   227 lemma atLeastLessThan_Suc_atLeastAtMost: "{l..Suc n(} = {l..n}"
   228 by (auto simp add: atLeastLessThan_def atLeastAtMost_def)
   229 
   230 (* greaterThanAtMost *)
   231 
   232 lemma greaterThanAtMost_iff [simp]:
   233   "(i : {)l..u}) = (l < i & i <= u)"
   234 by (simp add: greaterThanAtMost_def)
   235 
   236 (* atLeastAtMost *)
   237 
   238 lemma atLeastAtMost_iff [simp]:
   239   "(i : {l..u}) = (l <= i & i <= u)"
   240 by (simp add: atLeastAtMost_def)
   241 
   242 
   243 (* The above four lemmas could be declared as iffs.
   244    If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int
   245    seems to take forever (more than one hour). *)
   246 
   247 subsection {*Lemmas useful with the summation operator setsum*}
   248 
   249 (* For examples, see Algebra/poly/UnivPoly.thy *)
   250 
   251 (** Disjoint Unions **)
   252 
   253 (* Singletons and open intervals *)
   254 
   255 lemma ivl_disj_un_singleton:
   256   "{l::'a::linorder} Un {)l..} = {l..}"
   257   "{..u(} Un {u::'a::linorder} = {..u}"
   258   "(l::'a::linorder) < u ==> {l} Un {)l..u(} = {l..u(}"
   259   "(l::'a::linorder) < u ==> {)l..u(} Un {u} = {)l..u}"
   260   "(l::'a::linorder) <= u ==> {l} Un {)l..u} = {l..u}"
   261   "(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}"
   262 by auto
   263 
   264 (* One- and two-sided intervals *)
   265 
   266 lemma ivl_disj_un_one:
   267   "(l::'a::linorder) < u ==> {..l} Un {)l..u(} = {..u(}"
   268   "(l::'a::linorder) <= u ==> {..l(} Un {l..u(} = {..u(}"
   269   "(l::'a::linorder) <= u ==> {..l} Un {)l..u} = {..u}"
   270   "(l::'a::linorder) <= u ==> {..l(} Un {l..u} = {..u}"
   271   "(l::'a::linorder) <= u ==> {)l..u} Un {)u..} = {)l..}"
   272   "(l::'a::linorder) < u ==> {)l..u(} Un {u..} = {)l..}"
   273   "(l::'a::linorder) <= u ==> {l..u} Un {)u..} = {l..}"
   274   "(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}"
   275 by auto
   276 
   277 (* Two- and two-sided intervals *)
   278 
   279 lemma ivl_disj_un_two:
   280   "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u(} = {)l..u(}"
   281   "[| (l::'a::linorder) <= m; m < u |] ==> {)l..m} Un {)m..u(} = {)l..u(}"
   282   "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u(} = {l..u(}"
   283   "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {)m..u(} = {l..u(}"
   284   "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u} = {)l..u}"
   285   "[| (l::'a::linorder) <= m; m <= u |] ==> {)l..m} Un {)m..u} = {)l..u}"
   286   "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u} = {l..u}"
   287   "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {)m..u} = {l..u}"
   288 by auto
   289 
   290 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
   291 
   292 (** Disjoint Intersections **)
   293 
   294 (* Singletons and open intervals *)
   295 
   296 lemma ivl_disj_int_singleton:
   297   "{l::'a::order} Int {)l..} = {}"
   298   "{..u(} Int {u} = {}"
   299   "{l} Int {)l..u(} = {}"
   300   "{)l..u(} Int {u} = {}"
   301   "{l} Int {)l..u} = {}"
   302   "{l..u(} Int {u} = {}"
   303   by simp+
   304 
   305 (* One- and two-sided intervals *)
   306 
   307 lemma ivl_disj_int_one:
   308   "{..l::'a::order} Int {)l..u(} = {}"
   309   "{..l(} Int {l..u(} = {}"
   310   "{..l} Int {)l..u} = {}"
   311   "{..l(} Int {l..u} = {}"
   312   "{)l..u} Int {)u..} = {}"
   313   "{)l..u(} Int {u..} = {}"
   314   "{l..u} Int {)u..} = {}"
   315   "{l..u(} Int {u..} = {}"
   316   by auto
   317 
   318 (* Two- and two-sided intervals *)
   319 
   320 lemma ivl_disj_int_two:
   321   "{)l::'a::order..m(} Int {m..u(} = {}"
   322   "{)l..m} Int {)m..u(} = {}"
   323   "{l..m(} Int {m..u(} = {}"
   324   "{l..m} Int {)m..u(} = {}"
   325   "{)l..m(} Int {m..u} = {}"
   326   "{)l..m} Int {)m..u} = {}"
   327   "{l..m(} Int {m..u} = {}"
   328   "{l..m} Int {)m..u} = {}"
   329   by auto
   330 
   331 lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
   332 
   333 end