|
7626
|
1 |
(* Title: HOL/BCV/Orders.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1999 TUM
|
|
|
5 |
|
|
|
6 |
Orderings and some sets.
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Orders = Orders0 +
|
|
|
10 |
|
|
|
11 |
instance option :: (order)order (le_option_refl,le_option_trans,
|
|
|
12 |
le_option_antisym,less_le_option)
|
|
|
13 |
instance list :: (order)order (le_list_refl,le_list_trans,
|
|
|
14 |
le_list_antisym,less_le_list)
|
|
|
15 |
instance "*" :: (order,order)order
|
|
|
16 |
(le_prod_refl,le_prod_trans,le_prod_antisym,less_le_prod)
|
|
|
17 |
|
|
|
18 |
constdefs
|
|
|
19 |
acc :: "'a::order set => bool"
|
|
|
20 |
"acc A == wf{(y,x) . x:A & y:A & x < y}"
|
|
|
21 |
|
|
|
22 |
option :: 'a set => 'a option set
|
|
|
23 |
"option A == insert None {x . ? y:A. x = Some y}"
|
|
|
24 |
|
|
|
25 |
listsn :: nat => 'a set => 'a list set
|
|
|
26 |
"listsn n A == {xs. length xs = n & set xs <= A}"
|
|
|
27 |
|
|
|
28 |
end
|