src/HOL/Wellfounded_Relations.thy
 author oheimb Wed Jan 31 10:15:55 2001 +0100 (2001-01-31) changeset 11008 f7333f055ef6 parent 10213 01c2744a3786 child 11136 e34e7f6d9b57 permissions -rw-r--r--
improved theory reference in comment
```     1 (*  Title:      HOL/Wellfounded_Relations
```
```     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 Wellfounded_Relations = Finite +
```
```    14
```
```    15 (* actually belongs to theory Finite *)
```
```    16 instance unit :: finite                  (finite_unit)
```
```    17 instance "*" :: (finite,finite) finite   (finite_Prod)
```
```    18
```
```    19
```
```    20 constdefs
```
```    21  less_than :: "(nat*nat)set"
```
```    22 "less_than == trancl pred_nat"
```
```    23
```
```    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"
```
```    29
```
```    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}"
```
```    33
```
```    34  (* finite proper subset*)
```
```    35  finite_psubset  :: "('a set * 'a set) set"
```
```    36 "finite_psubset == {(A,B). A < B & finite B}"
```
```    37
```
```    38 (* For rec_defs where the first n parameters stay unchanged in the recursive
```
```    39    call. See Library/While_Combinator.thy 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}"
```
```    43
```
```    44 end
```