src/HOL/UNITY/LessThan.thy
author wenzelm
Tue, 17 Nov 1998 14:07:25 +0100
changeset 5906 1f58694fc3e2
parent 5536 130f3d891fb2
child 7878 43b03d412b82
permissions -rw-r--r--
Drule.rev_triv_goal;

(*  Title:      HOL/UNITY/LessThan
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

lessThan, greaterThan, atLeast, atMost

Could generalize to any linear ordering?
*)

LessThan = Main +

constdefs

  lessThan   :: "nat => nat set"
     "lessThan n == {i. i<n}"

  atMost   :: "nat => nat set"
     "atMost n == {i. i<=n}"
 
  greaterThan   :: "nat => nat set"
     "greaterThan n == {i. n<i}"

  atLeast   :: "nat => nat set"
     "atLeast n == {i. n<=i}"

end