author | wenzelm |
Mon, 04 Sep 2000 21:20:14 +0200 | |
changeset 9833 | 193dc80eaee9 |
parent 9443 | 3c2fc90d4e8a |
permissions | -rw-r--r-- |
3193 | 1 |
(* Title: HOL/WF_Rel |
2 |
ID: $Id$ |
|
3 |
Author: Konrad Slind |
|
4 |
Copyright 1995 TU Munich |
|
5 |
||
3296 | 6 |
Derived WF relations: inverse image, lexicographic product, measure, ... |
7 |
||
8 |
The simple relational product, in which (x',y')<(x,y) iff x'<x and y'<y, is a |
|
9 |
subset of the lexicographic product, and therefore does not need to be defined |
|
10 |
separately. |
|
3193 | 11 |
*) |
12 |
||
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
3193
diff
changeset
|
13 |
WF_Rel = Finite + |
8262 | 14 |
|
9833 | 15 |
(* actually belongs to theory Finite *) |
9361 | 16 |
instance unit :: finite (finite_unit) |
17 |
instance "*" :: (finite,finite) finite (finite_Prod) |
|
18 |
||
8262 | 19 |
|
9443 | 20 |
constdefs |
21 |
less_than :: "(nat*nat)set" |
|
22 |
"less_than == trancl pred_nat" |
|
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset
|
23 |
|
9443 | 24 |
inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set" |
25 |
"inv_image r f == {(x,y). (f(x), f(y)) : r}" |
|
26 |
||
27 |
measure :: "('a => nat) => ('a * 'a)set" |
|
28 |
"measure == inv_image less_than" |
|
3193 | 29 |
|
9443 | 30 |
lex_prod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" |
31 |
(infixr "<*lex*>" 80) |
|
32 |
"ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}" |
|
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset
|
33 |
|
9443 | 34 |
(* finite proper subset*) |
35 |
finite_psubset :: "('a set * 'a set) set" |
|
36 |
"finite_psubset == {(A,B). A < B & finite B}" |
|
3193 | 37 |
|
9443 | 38 |
(* For rec_defs where the first n parameters stay unchanged in the recursive |
39 |
call. See While for an application. |
|
40 |
*) |
|
41 |
same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set" |
|
42 |
"same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}" |
|
3193 | 43 |
|
44 |
end |