| changeset 0 | 7949f97df77a |
| child 118 | 5b96b1252cdc |
| -1:000000000000 | 0:7949f97df77a |
|---|---|
1 Ord = HOL + |
|
2 classes |
|
3 ord < term |
|
4 consts |
|
5 "<", "<=" :: "['a::ord, 'a] => bool" (infixl 50) |
|
6 mono :: "['a::ord => 'b::ord] => bool" (*monotonicity*) |
|
7 min,max :: "['a::ord,'a] => 'a" |
|
8 |
|
9 rules |
|
10 |
|
11 mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))" |
|
12 min_def "min(a,b) == if(a <= b, a, b)" |
|
13 max_def "max(a,b) == if(a <= b, b, a)" |
|
14 |
|
15 end |