src/HOL/SetInterval.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8957 26b6e8f43305
child 10212 33fe2d701ddd
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
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$
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
8957
26b6e8f43305 added parent
paulson
parents: 8924
diff changeset
     4
    Copyright   2000  TU Muenchen
8924
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
     5
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
     6
lessThan, greaterThan, atLeast, atMost
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
     7
*)
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
     8
8957
26b6e8f43305 added parent
paulson
parents: 8924
diff changeset
     9
SetInterval = equalities + Arith + 
8924
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    10
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    11
constdefs
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    12
 lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    13
"{..u(} == {x. x<u}"
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    14
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    15
 atMost      :: "('a::ord) => 'a set"	("(1{.._})")
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    16
"{..u} == {x. x<=u}"
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    17
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    18
 greaterThan :: "('a::ord) => 'a set"	("(1{')_..})")
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    19
"{)l..} == {x. l<x}"
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    20
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    21
 atLeast     :: "('a::ord) => 'a set"	("(1{_..})")
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    22
"{l..} == {x. l<=x}"
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    23
c434283b4cfa Added SetInterval
nipkow
parents:
diff changeset
    24
end