src/CCL/wfd.thy
 author lcp Fri Jan 14 12:42:49 1994 +0100 (1994-01-14) changeset 227 5415c6ad0028 parent 0 a5a9c433f639 child 289 78541329ff35 permissions -rw-r--r--
```     1 (*  Title: 	CCL/wfd.thy
```
```     2     ID:         \$Id\$
```
```     3     Author: 	Martin Coen, Cambridge University Computer Laboratory
```
```     4     Copyright   1993  University of Cambridge
```
```     5
```
```     6 Well-founded relations in CCL.
```
```     7 *)
```
```     8
```
```     9 Wfd = Trancl + Type +
```
```    10
```
```    11 consts
```
```    12       (*** Predicates ***)
```
```    13   Wfd        ::       "[i set] => o"
```
```    14       (*** Relations ***)
```
```    15   wf         ::       "[i set] => i set"
```
```    16   wmap       ::       "[i=>i,i set] => i set"
```
```    17   "**"       ::       "[i set,i set] => i set"      (infixl 70)
```
```    18   NatPR      ::       "i set"
```
```    19   ListPR     ::       "i set => i set"
```
```    20
```
```    21 rules
```
```    22
```
```    23   Wfd_def
```
```    24   "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a.a:P)"
```
```    25
```
```    26   wf_def         "wf(R) == {x.x:R & Wfd(R)}"
```
```    27
```
```    28   wmap_def       "wmap(f,R) == {p. EX x y. p=<x,y>  &  <f(x),f(y)> : R}"
```
```    29   lex_def
```
```    30   "ra**rb == {p. EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
```
```    31
```
```    32   NatPR_def      "NatPR == {p.EX x:Nat. p=<x,succ(x)>}"
```
```    33   ListPR_def     "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h.t>}"
```
```    34 end
```