src/HOL/WF.thy
 author berghofe Tue, 30 May 2000 18:02:49 +0200 changeset 9001 93af64f54bf2 parent 8882 9df44a4f1bf7 permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
```
(*  Title:      HOL/wf.ML
ID:         \$Id\$
Author:     Tobias Nipkow

Well-founded Recursion
*)

WF = Trancl +

constdefs
wf         :: "('a * 'a)set => bool"
"wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"

acyclic :: "('a*'a)set => bool"
"acyclic r == !x. (x,x) ~: r^+"

cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
"cut f r x == (%y. if (y,x):r then f y else arbitrary)"

is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
"is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"

the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
"the_recfun r H a  == (@f. is_recfun r H a f)"

wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
"wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
r x)  x)"

end
```