equal
deleted
inserted
replaced
1 (* Title: HOL/Ord.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 The type class for ordered types (* FIXME improve comment *) |
|
7 *) |
|
8 |
|
9 Ord = HOL + |
|
10 |
|
11 axclass |
|
12 ord < term |
|
13 |
|
14 consts |
|
15 "<", "<=" :: "['a::ord, 'a] => bool" (infixl 50) |
|
16 mono :: "['a::ord => 'b::ord] => bool" (*monotonicity*) |
|
17 min, max :: "['a::ord, 'a] => 'a" |
|
18 |
|
19 defs |
|
20 mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))" |
|
21 min_def "min(a, b) == if(a <= b, a, b)" |
|
22 max_def "max(a, b) == if(a <= b, b, a)" |
|
23 |
|
24 end |
|
25 |
|