src/HOL/SetInterval.thy
author ballarin
Thu Nov 28 10:50:42 2002 +0100 (2002-11-28)
changeset 13735 7de9342aca7a
parent 11609 3f3d1add4d94
child 13850 6d1bb3059818
permissions -rw-r--r--
HOL-Algebra partially ported to Isar.
nipkow@8924
     1
(*  Title:      HOL/SetInterval.thy
nipkow@8924
     2
    ID:         $Id$
ballarin@13735
     3
    Author:     Tobias Nipkow and Clemens Ballarin
paulson@8957
     4
    Copyright   2000  TU Muenchen
nipkow@8924
     5
ballarin@13735
     6
lessThan, greaterThan, atLeast, atMost and two-sided intervals
nipkow@8924
     7
*)
nipkow@8924
     8
ballarin@13735
     9
theory SetInterval = NatArith:
nipkow@8924
    10
nipkow@8924
    11
constdefs
wenzelm@11609
    12
  lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
wenzelm@11609
    13
  "{..u(} == {x. x<u}"
nipkow@8924
    14
wenzelm@11609
    15
  atMost      :: "('a::ord) => 'a set"	("(1{.._})")
wenzelm@11609
    16
  "{..u} == {x. x<=u}"
nipkow@8924
    17
wenzelm@11609
    18
  greaterThan :: "('a::ord) => 'a set"	("(1{')_..})")
wenzelm@11609
    19
  "{)l..} == {x. l<x}"
nipkow@8924
    20
wenzelm@11609
    21
  atLeast     :: "('a::ord) => 'a set"	("(1{_..})")
wenzelm@11609
    22
  "{l..} == {x. l<=x}"
nipkow@8924
    23
ballarin@13735
    24
  greaterThanLessThan :: "['a::ord, 'a] => 'a set"  ("(1{')_.._'(})")
ballarin@13735
    25
  "{)l..u(} == {)l..} Int {..u(}"
ballarin@13735
    26
ballarin@13735
    27
  atLeastLessThan :: "['a::ord, 'a] => 'a set"      ("(1{_.._'(})")
ballarin@13735
    28
  "{l..u(} == {l..} Int {..u(}"
ballarin@13735
    29
ballarin@13735
    30
  greaterThanAtMost :: "['a::ord, 'a] => 'a set"    ("(1{')_.._})")
ballarin@13735
    31
  "{)l..u} == {)l..} Int {..u}"
ballarin@13735
    32
ballarin@13735
    33
  atLeastAtMost :: "['a::ord, 'a] => 'a set"        ("(1{_.._})")
ballarin@13735
    34
  "{l..u} == {l..} Int {..u}"
ballarin@13735
    35
ballarin@13735
    36
(* Setup of transitivity reasoner *)
ballarin@13735
    37
ballarin@13735
    38
ML {*
ballarin@13735
    39
ballarin@13735
    40
structure Trans_Tac = Trans_Tac_Fun (
ballarin@13735
    41
  struct
ballarin@13735
    42
    val less_reflE = thm "order_less_irrefl" RS thm "notE";
ballarin@13735
    43
    val le_refl = thm "order_refl";
ballarin@13735
    44
    val less_imp_le = thm "order_less_imp_le";
ballarin@13735
    45
    val not_lessI = thm "linorder_not_less" RS thm "iffD2";
ballarin@13735
    46
    val not_leI = thm "linorder_not_less" RS thm "iffD2";
ballarin@13735
    47
    val not_lessD = thm "linorder_not_less" RS thm "iffD1";
ballarin@13735
    48
    val not_leD = thm "linorder_not_le" RS thm "iffD1";
ballarin@13735
    49
    val eqI = thm "order_antisym";
ballarin@13735
    50
    val eqD1 = thm "order_eq_refl";
ballarin@13735
    51
    val eqD2 = thm "sym" RS thm "order_eq_refl";
ballarin@13735
    52
    val less_trans = thm "order_less_trans";
ballarin@13735
    53
    val less_le_trans = thm "order_less_le_trans";
ballarin@13735
    54
    val le_less_trans = thm "order_le_less_trans";
ballarin@13735
    55
    val le_trans = thm "order_trans";
ballarin@13735
    56
    fun decomp (Trueprop $ t) =
ballarin@13735
    57
      let fun dec (Const ("Not", _) $ t) = (
ballarin@13735
    58
              case dec t of
ballarin@13735
    59
		None => None
ballarin@13735
    60
	      | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
ballarin@13735
    61
	    | dec (Const (rel, _) $ t1 $ t2) = 
ballarin@13735
    62
                Some (t1, implode (drop (3, explode rel)), t2)
ballarin@13735
    63
	    | dec _ = None
ballarin@13735
    64
      in dec t end
ballarin@13735
    65
      | decomp _ = None
ballarin@13735
    66
  end);
ballarin@13735
    67
ballarin@13735
    68
val trans_tac = Trans_Tac.trans_tac;
ballarin@13735
    69
ballarin@13735
    70
*}
ballarin@13735
    71
ballarin@13735
    72
method_setup trans =
ballarin@13735
    73
  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac)) *}
ballarin@13735
    74
  {* simple transitivity reasoner *}
ballarin@13735
    75
ballarin@13735
    76
(*** lessThan ***)
ballarin@13735
    77
ballarin@13735
    78
lemma lessThan_iff: "(i: lessThan k) = (i<k)"
ballarin@13735
    79
ballarin@13735
    80
apply (unfold lessThan_def)
ballarin@13735
    81
apply blast
ballarin@13735
    82
done
ballarin@13735
    83
declare lessThan_iff [iff]
ballarin@13735
    84
ballarin@13735
    85
lemma lessThan_0: "lessThan (0::nat) = {}"
ballarin@13735
    86
apply (unfold lessThan_def)
ballarin@13735
    87
apply (simp (no_asm))
ballarin@13735
    88
done
ballarin@13735
    89
declare lessThan_0 [simp]
ballarin@13735
    90
ballarin@13735
    91
lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
ballarin@13735
    92
apply (unfold lessThan_def)
ballarin@13735
    93
apply (simp (no_asm) add: less_Suc_eq)
ballarin@13735
    94
apply blast
ballarin@13735
    95
done
ballarin@13735
    96
ballarin@13735
    97
lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
ballarin@13735
    98
apply (unfold lessThan_def atMost_def)
ballarin@13735
    99
apply (simp (no_asm) add: less_Suc_eq_le)
ballarin@13735
   100
done
ballarin@13735
   101
ballarin@13735
   102
lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
ballarin@13735
   103
apply blast
ballarin@13735
   104
done
ballarin@13735
   105
ballarin@13735
   106
lemma Compl_lessThan: 
ballarin@13735
   107
    "!!k:: 'a::linorder. -lessThan k = atLeast k"
ballarin@13735
   108
apply (unfold lessThan_def atLeast_def)
ballarin@13735
   109
apply auto
ballarin@13735
   110
apply (blast intro: linorder_not_less [THEN iffD1])
ballarin@13735
   111
apply (blast dest: order_le_less_trans)
ballarin@13735
   112
done
ballarin@13735
   113
ballarin@13735
   114
lemma single_Diff_lessThan: "!!k:: 'a::order. {k} - lessThan k = {k}"
ballarin@13735
   115
apply auto
ballarin@13735
   116
done
ballarin@13735
   117
declare single_Diff_lessThan [simp]
ballarin@13735
   118
ballarin@13735
   119
(*** greaterThan ***)
ballarin@13735
   120
ballarin@13735
   121
lemma greaterThan_iff: "(i: greaterThan k) = (k<i)"
ballarin@13735
   122
ballarin@13735
   123
apply (unfold greaterThan_def)
ballarin@13735
   124
apply blast
ballarin@13735
   125
done
ballarin@13735
   126
declare greaterThan_iff [iff]
ballarin@13735
   127
ballarin@13735
   128
lemma greaterThan_0: "greaterThan 0 = range Suc"
ballarin@13735
   129
apply (unfold greaterThan_def)
ballarin@13735
   130
apply (blast dest: gr0_conv_Suc [THEN iffD1])
ballarin@13735
   131
done
ballarin@13735
   132
declare greaterThan_0 [simp]
ballarin@13735
   133
ballarin@13735
   134
lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"
ballarin@13735
   135
apply (unfold greaterThan_def)
ballarin@13735
   136
apply (auto elim: linorder_neqE)
ballarin@13735
   137
done
ballarin@13735
   138
ballarin@13735
   139
lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
ballarin@13735
   140
apply blast
ballarin@13735
   141
done
ballarin@13735
   142
ballarin@13735
   143
lemma Compl_greaterThan: 
ballarin@13735
   144
    "!!k:: 'a::linorder. -greaterThan k = atMost k"
ballarin@13735
   145
apply (unfold greaterThan_def atMost_def le_def)
ballarin@13735
   146
apply auto
ballarin@13735
   147
apply (blast intro: linorder_not_less [THEN iffD1])
ballarin@13735
   148
apply (blast dest: order_le_less_trans)
ballarin@13735
   149
done
ballarin@13735
   150
ballarin@13735
   151
lemma Compl_atMost: "!!k:: 'a::linorder. -atMost k = greaterThan k"
ballarin@13735
   152
apply (simp (no_asm) add: Compl_greaterThan [symmetric])
ballarin@13735
   153
done
ballarin@13735
   154
ballarin@13735
   155
declare Compl_greaterThan [simp] Compl_atMost [simp]
ballarin@13735
   156
ballarin@13735
   157
(*** atLeast ***)
ballarin@13735
   158
ballarin@13735
   159
lemma atLeast_iff: "(i: atLeast k) = (k<=i)"
ballarin@13735
   160
ballarin@13735
   161
apply (unfold atLeast_def)
ballarin@13735
   162
apply blast
ballarin@13735
   163
done
ballarin@13735
   164
declare atLeast_iff [iff]
ballarin@13735
   165
ballarin@13735
   166
lemma atLeast_0: "atLeast (0::nat) = UNIV"
ballarin@13735
   167
apply (unfold atLeast_def UNIV_def)
ballarin@13735
   168
apply (simp (no_asm))
ballarin@13735
   169
done
ballarin@13735
   170
declare atLeast_0 [simp]
ballarin@13735
   171
ballarin@13735
   172
lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"
ballarin@13735
   173
apply (unfold atLeast_def)
ballarin@13735
   174
apply (simp (no_asm) add: Suc_le_eq)
ballarin@13735
   175
apply (simp (no_asm) add: order_le_less)
ballarin@13735
   176
apply blast
ballarin@13735
   177
done
ballarin@13735
   178
ballarin@13735
   179
lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
ballarin@13735
   180
apply blast
ballarin@13735
   181
done
ballarin@13735
   182
ballarin@13735
   183
lemma Compl_atLeast: 
ballarin@13735
   184
    "!!k:: 'a::linorder. -atLeast k = lessThan k"
ballarin@13735
   185
apply (unfold lessThan_def atLeast_def le_def)
ballarin@13735
   186
apply auto
ballarin@13735
   187
apply (blast intro: linorder_not_less [THEN iffD1])
ballarin@13735
   188
apply (blast dest: order_le_less_trans)
ballarin@13735
   189
done
ballarin@13735
   190
ballarin@13735
   191
declare Compl_lessThan [simp] Compl_atLeast [simp]
ballarin@13735
   192
ballarin@13735
   193
(*** atMost ***)
ballarin@13735
   194
ballarin@13735
   195
lemma atMost_iff: "(i: atMost k) = (i<=k)"
ballarin@13735
   196
ballarin@13735
   197
apply (unfold atMost_def)
ballarin@13735
   198
apply blast
ballarin@13735
   199
done
ballarin@13735
   200
declare atMost_iff [iff]
ballarin@13735
   201
ballarin@13735
   202
lemma atMost_0: "atMost (0::nat) = {0}"
ballarin@13735
   203
apply (unfold atMost_def)
ballarin@13735
   204
apply (simp (no_asm))
ballarin@13735
   205
done
ballarin@13735
   206
declare atMost_0 [simp]
ballarin@13735
   207
ballarin@13735
   208
lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
ballarin@13735
   209
apply (unfold atMost_def)
ballarin@13735
   210
apply (simp (no_asm) add: less_Suc_eq order_le_less)
ballarin@13735
   211
apply blast
ballarin@13735
   212
done
ballarin@13735
   213
ballarin@13735
   214
lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
ballarin@13735
   215
apply blast
ballarin@13735
   216
done
ballarin@13735
   217
ballarin@13735
   218
ballarin@13735
   219
(*** Combined properties ***)
ballarin@13735
   220
ballarin@13735
   221
lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
ballarin@13735
   222
apply (blast intro: order_antisym)
ballarin@13735
   223
done
ballarin@13735
   224
ballarin@13735
   225
(*** Two-sided intervals ***)
ballarin@13735
   226
ballarin@13735
   227
(* greaterThanLessThan *)
ballarin@13735
   228
ballarin@13735
   229
lemma greaterThanLessThan_iff [simp]:
ballarin@13735
   230
  "(i : {)l..u(}) = (l < i & i < u)"
ballarin@13735
   231
by (simp add: greaterThanLessThan_def)
ballarin@13735
   232
ballarin@13735
   233
(* atLeastLessThan *)
ballarin@13735
   234
ballarin@13735
   235
lemma atLeastLessThan_iff [simp]:
ballarin@13735
   236
  "(i : {l..u(}) = (l <= i & i < u)"
ballarin@13735
   237
by (simp add: atLeastLessThan_def)
ballarin@13735
   238
ballarin@13735
   239
(* greaterThanAtMost *)
ballarin@13735
   240
ballarin@13735
   241
lemma greaterThanAtMost_iff [simp]:
ballarin@13735
   242
  "(i : {)l..u}) = (l < i & i <= u)"
ballarin@13735
   243
by (simp add: greaterThanAtMost_def)
ballarin@13735
   244
ballarin@13735
   245
(* atLeastAtMost *)
ballarin@13735
   246
ballarin@13735
   247
lemma atLeastAtMost_iff [simp]:
ballarin@13735
   248
  "(i : {l..u}) = (l <= i & i <= u)"
ballarin@13735
   249
by (simp add: atLeastAtMost_def)
ballarin@13735
   250
ballarin@13735
   251
(* The above four lemmas could be declared as iffs.
ballarin@13735
   252
   If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int
ballarin@13735
   253
   seems to take forever (more than one hour). *)
ballarin@13735
   254
ballarin@13735
   255
(*** The following lemmas are useful with the summation operator setsum ***)
ballarin@13735
   256
(* For examples, see Algebra/poly/UnivPoly.thy *)
ballarin@13735
   257
ballarin@13735
   258
(** Disjoint Unions **)
ballarin@13735
   259
ballarin@13735
   260
(* Singletons and open intervals *)
ballarin@13735
   261
ballarin@13735
   262
lemma ivl_disj_un_singleton:
ballarin@13735
   263
  "{l::'a::linorder} Un {)l..} = {l..}"
ballarin@13735
   264
  "{..u(} Un {u::'a::linorder} = {..u}"
ballarin@13735
   265
  "(l::'a::linorder) < u ==> {l} Un {)l..u(} = {l..u(}"
ballarin@13735
   266
  "(l::'a::linorder) < u ==> {)l..u(} Un {u} = {)l..u}"
ballarin@13735
   267
  "(l::'a::linorder) <= u ==> {l} Un {)l..u} = {l..u}"
ballarin@13735
   268
  "(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}"
ballarin@13735
   269
by auto (elim linorder_neqE | trans+)+
ballarin@13735
   270
ballarin@13735
   271
(* One- and two-sided intervals *)
ballarin@13735
   272
ballarin@13735
   273
lemma ivl_disj_un_one:
ballarin@13735
   274
  "(l::'a::linorder) < u ==> {..l} Un {)l..u(} = {..u(}"
ballarin@13735
   275
  "(l::'a::linorder) <= u ==> {..l(} Un {l..u(} = {..u(}"
ballarin@13735
   276
  "(l::'a::linorder) <= u ==> {..l} Un {)l..u} = {..u}"
ballarin@13735
   277
  "(l::'a::linorder) <= u ==> {..l(} Un {l..u} = {..u}"
ballarin@13735
   278
  "(l::'a::linorder) <= u ==> {)l..u} Un {)u..} = {)l..}"
ballarin@13735
   279
  "(l::'a::linorder) < u ==> {)l..u(} Un {u..} = {)l..}"
ballarin@13735
   280
  "(l::'a::linorder) <= u ==> {l..u} Un {)u..} = {l..}"
ballarin@13735
   281
  "(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}"
ballarin@13735
   282
by auto trans+
ballarin@13735
   283
ballarin@13735
   284
(* Two- and two-sided intervals *)
ballarin@13735
   285
ballarin@13735
   286
lemma ivl_disj_un_two:
ballarin@13735
   287
  "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u(} = {)l..u(}"
ballarin@13735
   288
  "[| (l::'a::linorder) <= m; m < u |] ==> {)l..m} Un {)m..u(} = {)l..u(}"
ballarin@13735
   289
  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u(} = {l..u(}"
ballarin@13735
   290
  "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {)m..u(} = {l..u(}"
ballarin@13735
   291
  "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u} = {)l..u}"
ballarin@13735
   292
  "[| (l::'a::linorder) <= m; m <= u |] ==> {)l..m} Un {)m..u} = {)l..u}"
ballarin@13735
   293
  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u} = {l..u}"
ballarin@13735
   294
  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {)m..u} = {l..u}"
ballarin@13735
   295
by auto trans+
ballarin@13735
   296
ballarin@13735
   297
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
ballarin@13735
   298
ballarin@13735
   299
(** Disjoint Intersections **)
ballarin@13735
   300
ballarin@13735
   301
(* Singletons and open intervals *)
ballarin@13735
   302
ballarin@13735
   303
lemma ivl_disj_int_singleton:
ballarin@13735
   304
  "{l::'a::order} Int {)l..} = {}"
ballarin@13735
   305
  "{..u(} Int {u} = {}"
ballarin@13735
   306
  "{l} Int {)l..u(} = {}"
ballarin@13735
   307
  "{)l..u(} Int {u} = {}"
ballarin@13735
   308
  "{l} Int {)l..u} = {}"
ballarin@13735
   309
  "{l..u(} Int {u} = {}"
ballarin@13735
   310
  by simp+
ballarin@13735
   311
ballarin@13735
   312
(* One- and two-sided intervals *)
ballarin@13735
   313
ballarin@13735
   314
lemma ivl_disj_int_one:
ballarin@13735
   315
  "{..l::'a::order} Int {)l..u(} = {}"
ballarin@13735
   316
  "{..l(} Int {l..u(} = {}"
ballarin@13735
   317
  "{..l} Int {)l..u} = {}"
ballarin@13735
   318
  "{..l(} Int {l..u} = {}"
ballarin@13735
   319
  "{)l..u} Int {)u..} = {}"
ballarin@13735
   320
  "{)l..u(} Int {u..} = {}"
ballarin@13735
   321
  "{l..u} Int {)u..} = {}"
ballarin@13735
   322
  "{l..u(} Int {u..} = {}"
ballarin@13735
   323
  by auto trans+
ballarin@13735
   324
ballarin@13735
   325
(* Two- and two-sided intervals *)
ballarin@13735
   326
ballarin@13735
   327
lemma ivl_disj_int_two:
ballarin@13735
   328
  "{)l::'a::order..m(} Int {m..u(} = {}"
ballarin@13735
   329
  "{)l..m} Int {)m..u(} = {}"
ballarin@13735
   330
  "{l..m(} Int {m..u(} = {}"
ballarin@13735
   331
  "{l..m} Int {)m..u(} = {}"
ballarin@13735
   332
  "{)l..m(} Int {m..u} = {}"
ballarin@13735
   333
  "{)l..m} Int {)m..u} = {}"
ballarin@13735
   334
  "{l..m(} Int {m..u} = {}"
ballarin@13735
   335
  "{l..m} Int {)m..u} = {}"
ballarin@13735
   336
  by auto trans+
ballarin@13735
   337
ballarin@13735
   338
lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
ballarin@13735
   339
nipkow@8924
   340
end