src/HOL/WF_Rel.thy
 author wenzelm Thu Mar 11 13:20:35 1999 +0100 (1999-03-11) changeset 6349 f7750d816c21 parent 3296 2ee6c397003d child 8262 08ad0a986db2 permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
```     1 (*  Title:      HOL/WF_Rel
```
```     2     ID:         \$Id\$
```
```     3     Author:     Konrad Slind
```
```     4     Copyright   1995 TU Munich
```
```     5
```
```     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.
```
```    11 *)
```
```    12
```
```    13 WF_Rel = Finite +
```
```    14 consts
```
```    15   less_than :: "(nat*nat)set"
```
```    16   inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
```
```    17   measure   :: "('a => nat) => ('a * 'a)set"
```
```    18   "**"      :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
```
```    19   finite_psubset  :: "('a set * 'a set) set"
```
```    20
```
```    21
```
```    22 defs
```
```    23   less_than_def "less_than == trancl pred_nat"
```
```    24
```
```    25   inv_image_def "inv_image r f == {(x,y). (f(x), f(y)) : r}"
```
```    26
```
```    27   measure_def   "measure == inv_image less_than"
```
```    28
```
```    29   lex_prod_def  "ra**rb == {p. ? a a' b b'.
```
```    30                                 p = ((a,b),(a',b')) &
```
```    31                                ((a,a') : ra | a=a' & (b,b') : rb)}"
```
```    32
```
```    33   (* finite proper subset*)
```
```    34   finite_psubset_def "finite_psubset == {(A,B). A < B & finite B}"
```
```    35 end
```