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