src/HOL/WF.thy
 author clasohm Fri Mar 03 12:02:25 1995 +0100 (1995-03-03) changeset 923 ff1574a81019 child 965 24eef3860714 permissions -rw-r--r--
new version of HOL with curried function application
```     1 (*  Title: 	HOL/wf.ML
```
```     2     ID:         \$Id\$
```
```     3     Author: 	Tobias Nipkow
```
```     4     Copyright   1992  University of Cambridge
```
```     5
```
```     6 Well-founded Recursion
```
```     7 *)
```
```     8
```
```     9 WF = Trancl +
```
```    10 consts
```
```    11    wf		:: "('a * 'a)set => bool"
```
```    12    cut		:: "['a => 'b, ('a * 'a)set, 'a] => 'a => 'b"
```
```    13    wftrec,wfrec	:: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b] => 'b"
```
```    14    is_recfun	:: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b, 'a=>'b] => bool"
```
```    15    the_recfun	:: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b] => 'a=>'b"
```
```    16
```
```    17 defs
```
```    18   wf_def  "wf(r) == (!P. (!x. (!y. <y,x>:r --> P(y)) --> P(x)) --> (!x.P(x)))"
```
```    19
```
```    20   cut_def 	 "cut f r x == (%y. if (<y,x>:r) (f y) (@z.True))"
```
```    21
```
```    22   is_recfun_def  "is_recfun r a H f == (f = cut (%x.(H x (cut f r x))) r a)"
```
```    23
```
```    24   the_recfun_def "the_recfun r a H == (@f.is_recfun r a H f)"
```
```    25
```
```    26   wftrec_def     "wftrec r a H == H a (the_recfun r a H)"
```
```    27
```
```    28   (*version not requiring transitivity*)
```
```    29   wfrec_def	"wfrec r a H == wftrec (trancl r) a (%x f.(H x (cut f r x)))"
```
```    30 end
```