|
7626
|
1 |
(* Title: HOL/BCV/Orders0.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1999 TUM
|
|
|
5 |
|
|
|
6 |
Orderings on various types.
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Orders0 = Main +
|
|
|
10 |
|
|
|
11 |
instance option :: (ord)ord
|
|
|
12 |
instance list :: (ord)ord
|
|
|
13 |
instance "*" :: (ord,ord)ord
|
|
|
14 |
|
|
|
15 |
defs
|
|
|
16 |
le_option "o1 <= o2 == case o2 of None => o1=None |
|
|
|
17 |
Some y => (case o1 of None => True | Some x => x<=y)"
|
|
|
18 |
less_option "(o1::('a::ord)option) < o2 == o1 <= o2 & o1 ~= o2"
|
|
|
19 |
|
|
|
20 |
le_list "xs <= ys == size xs = size ys & (!i. i<size xs --> xs!i <= ys!i)"
|
|
|
21 |
less_list "(xs::('a::ord)list) < ys == xs <= ys & xs ~= ys"
|
|
|
22 |
|
|
|
23 |
le_prod "p1 <= p2 == fst p1 <= fst p2 & snd p1 <= snd p2"
|
|
|
24 |
less_prod "(p1::('a::ord * 'b::ord)) < p2 == p1 <= p2 & p1 ~= p2"
|
|
|
25 |
|
|
|
26 |
end
|