author | wenzelm |
Tue, 20 May 1997 19:29:50 +0200 | |
changeset 3257 | 4e3724e0659f |
parent 3237 | 4da86d44de33 |
child 3296 | 2ee6c397003d |
permissions | -rw-r--r-- |
3193 | 1 |
(* Title: HOL/WF_Rel |
2 |
ID: $Id$ |
|
3 |
Author: Konrad Slind |
|
4 |
Copyright 1995 TU Munich |
|
5 |
||
6 |
Derived wellfounded relations: inverse image, relational product, measure, ... |
|
7 |
*) |
|
8 |
||
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
3193
diff
changeset
|
9 |
WF_Rel = Finite + |
3193 | 10 |
consts |
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset
|
11 |
less_than :: "(nat*nat)set" |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset
|
12 |
inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set" |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset
|
13 |
measure :: "('a => nat) => ('a * 'a)set" |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset
|
14 |
"**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70) |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset
|
15 |
rprod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset
|
16 |
finite_psubset :: "('a set * 'a set) set" |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset
|
17 |
|
3193 | 18 |
|
19 |
defs |
|
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset
|
20 |
less_than_def "less_than == trancl pred_nat" |
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset
|
21 |
|
3193 | 22 |
inv_image_def "inv_image r f == {(x,y). (f(x), f(y)) : r}" |
23 |
||
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset
|
24 |
measure_def "measure == inv_image less_than" |
3193 | 25 |
|
26 |
lex_prod_def "ra**rb == {p. ? a a' b b'. |
|
27 |
p = ((a,b),(a',b')) & |
|
28 |
((a,a') : ra | a=a' & (b,b') : rb)}" |
|
29 |
||
30 |
rprod_def "rprod ra rb == {p. ? a a' b b'. |
|
31 |
p = ((a,b),(a',b')) & |
|
32 |
((a,a') : ra & (b,b') : rb)}" |
|
33 |
||
34 |
(* finite proper subset*) |
|
35 |
finite_psubset_def "finite_psubset == {(A,B). A < B & finite B}" |
|
36 |
end |