|
4776
|
1 |
(* Title: HOL/UNITY/LessThan
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1998 University of Cambridge
|
|
|
5 |
|
|
|
6 |
lessThan, greaterThan, atLeast, atMost
|
|
5536
|
7 |
|
|
|
8 |
Could generalize to any linear ordering?
|
|
4776
|
9 |
*)
|
|
|
10 |
|
|
5232
|
11 |
LessThan = Main +
|
|
4776
|
12 |
|
|
|
13 |
constdefs
|
|
|
14 |
|
|
|
15 |
lessThan :: "nat => nat set"
|
|
|
16 |
"lessThan n == {i. i<n}"
|
|
|
17 |
|
|
|
18 |
atMost :: "nat => nat set"
|
|
|
19 |
"atMost n == {i. i<=n}"
|
|
|
20 |
|
|
|
21 |
greaterThan :: "nat => nat set"
|
|
|
22 |
"greaterThan n == {i. n<i}"
|
|
|
23 |
|
|
|
24 |
atLeast :: "nat => nat set"
|
|
|
25 |
"atLeast n == {i. n<=i}"
|
|
|
26 |
|
|
|
27 |
end
|